IMO 2012 P4

[Seasawher]

No description provided.

[Seasawher]

@dwrensha Please review this PR.

[dwrensha]

Thanks! If you want to claim credit for this work, please add your name(s) to the Authors: field in the copyright header at the top of the file. (You may delete my name, as I did not contribute to this solution.)

[dwrensha]

odd_const, mod4_cycle, square_set, sub_sq', Int.lt_of_ns_lt_ns and myInduction should be inside of snip begin ... snip end.

compfiles/ProblemExtraction.lean

Lines 187 to 191 in 7b57a0d

	/-- Starts a group of commands that will be discarded by problem extraction. -/
	syntax (name := snipBegin) "snip begin" : command
	/-- Ends a group of commands that will be discarded by problem extraction. -/
	syntax (name := snipEnd) "snip end" : command

For example:

compfiles/Compfiles/Imo1965P2.lean

Lines 33 to 72 in 7b57a0d

	snip begin
	abbrev propEqs (x : Fin 3 → ℝ) (a : Fin 3 → Fin 3 → ℝ) : Prop :=
	∀ i, ∑ j : Fin 3, (a i j * x j) = 0
	lemma lemma0 (x : Fin 3 → ℝ) (a : Fin 3 → Fin 3 → ℝ) (p : Fin 3 → Fin 3)
	(hp : p.Bijective)
	(he : propEqs x a) : propEqs (x ∘ p) (fun i j ↦ a (p i) (p j)) := by
	intro i
	dsimp
	have hi := he (p i)
	rwa [Function.Bijective.sum_comp hp (fun j ↦ a (p i) j * x j)]
	abbrev propsAB (a : Fin 3 → Fin 3 → ℝ) : Prop :=
	∀ i j, if i = j then 0 < a i j else a i j < 0
	lemma lemma1 (a : Fin 3 → Fin 3 → ℝ) (p : Fin 3 → Fin 3)
	(hp : p.Bijective)
	(hab : propsAB a) :
	propsAB (fun i j ↦ a (p i) (p j)) := by
	intro i j
	have h0 := hab (p i) (p j)
	split_ifs with h1
	· subst h1
	simp only [reduceIte] at h0
	exact h0
	· have h2 : p i ≠ p j := fun a ↦ h1 (hp.1 a)
	simp only [h2] at h0
	exact h0
	lemma lemma2 (a : Fin 3 → Fin 3 → ℝ)
	(p : Fin 3 → Fin 3)
	(hp : p.Bijective)
	(hc : ∀ i, 0 < ∑ j : Fin 3, a i j) :
	∀ i, 0 < ∑ j : Fin 3, a (p i) (p j) := by
	intro i
	rw [Function.Bijective.sum_comp hp]
	exact hc (p i)
	snip end

[dwrensha]

This will make it so that the problem web page (https://dwrensha.github.io/compfiles/problems/Compfiles.Imo2012P4.html) does not show any information about the solution.

[Seasawher]

done!

[dwrensha]

Thanks! I moved the determine outside of the snip here: c81da56