ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>L : FirstOrder.Language<VAR>α : Type u'<VAR>β : Type v'<VAR>n : ℕ<VAR>g : α → β ⊕ Fin n<VAR>k : ℕ<GOAL>FirstOrder.Language.BoundedFormula.relabel g FirstOrder.Language.BoundedFormula.falsum = FirstOrder.Language.BoundedFormula.falsum
<VAR>L : FirstOrder.Language<VAR>α : Type u'<VAR>β : Type v'<VAR>n : ℕ<VAR>g : α → β ⊕ Fin n<VAR>k : ℕ<GOAL>FirstOrder.Language.BoundedFormula.relabel g ⊥ = ⊥
<VAR>L : FirstOrder.Language<VAR>α : Type u'<VAR>β : Type v'<VAR>n : ℕ<VAR>g : α → β ⊕ Fin n<VAR>k : ℕ<VAR>φ ψ : L.BoundedFormula α k<GOAL>FirstOrder.Language.BoundedFormula.relabel g (φ.imp ψ) = (FirstOrder.Language.BoundedFormula.relabel g φ).imp (FirstOrder.Language.BoundedFormula.relabel g ψ)
<VAR>L : FirstOrder.Language<VAR>α : Type u'<VAR>β : Type v'<VAR>n : ℕ<VAR>g : α → β ⊕ Fin n<VAR>k : ℕ<VAR>φ : L.BoundedFormula α k<GOAL>FirstOrder.Language.BoundedFormula.relabel g φ.not = (FirstOrder.Language.BoundedFormula.relabel g φ).not
<VAR>L : FirstOrder.Language<VAR>α : Type u'<VAR>β : Type v'<VAR>n : ℕ<VAR>g : α → β ⊕ Fin n<VAR>k : ℕ<VAR>φ : L.BoundedFormula α (k + 1)<GOAL>FirstOrder.Language.BoundedFormula.relabel g φ.all = (FirstOrder.Language.BoundedFormula.relabel g φ).all
<VAR>L : FirstOrder.Language<VAR>α : Type u'<VAR>β : Type v'<VAR>n : ℕ<VAR>g : α → β ⊕ Fin n<VAR>k : ℕ<VAR>φ : L.BoundedFormula α (k + 1)<GOAL>FirstOrder.Language.BoundedFormula.relabel g φ.ex = (FirstOrder.Language.BoundedFormula.relabel g φ).ex
<VAR>L : FirstOrder.Language<VAR>α : Type u'<VAR>n : ℕ<VAR>φ : L.BoundedFormula α n<GOAL>FirstOrder.Language.BoundedFormula.relabel Sum.inl φ = FirstOrder.Language.BoundedFormula.castLE ⋯ φ
<VAR>L : FirstOrder.Language<VAR>α : Type u'<VAR>n : ℕ<GOAL>(FirstOrder.Language.LHom.id L).onBoundedFormula = id
<VAR>L : FirstOrder.Language<VAR>L' : FirstOrder.Language<VAR>α : Type u'<VAR>n : ℕ<VAR>L'' : FirstOrder.Language<VAR>φ : L' →ᴸ L''<VAR>ψ : L →ᴸ L'<GOAL>(φ.comp ψ).onBoundedFormula = φ.onBoundedFormula ∘ ψ.onBoundedFormula
<VAR>L : FirstOrder.Language<VAR>L' : FirstOrder.Language<VAR>g : L →ᴸ L'<VAR>T : L.Theory<VAR>φ : L'.Sentence<GOAL>φ ∈ g.onTheory T ↔ ∃ φ₀ ∈ T, g.onSentence φ₀ = φ
<VAR>L : FirstOrder.Language<VAR>L' : FirstOrder.Language<VAR>α : Type u'<VAR>n : ℕ<VAR>φ : L ≃ᴸ L'<GOAL>∀ (a : L'.BoundedFormula α n), φ.onBoundedFormula.symm a = φ.invLHom.onBoundedFormula a
<VAR>L : FirstOrder.Language<VAR>L' : FirstOrder.Language<VAR>α : Type u'<VAR>n : ℕ<VAR>φ : L ≃ᴸ L'<GOAL>∀ (a : L.BoundedFormula α n), φ.onBoundedFormula a = φ.toLHom.onBoundedFormula a
<VAR>L : FirstOrder.Language<VAR>L' : FirstOrder.Language<VAR>α : Type u'<VAR>n : ℕ<VAR>φ : L ≃ᴸ L'<GOAL>φ.onBoundedFormula.symm = φ.symm.onBoundedFormula
<VAR>L : FirstOrder.Language<VAR>L' : FirstOrder.Language<VAR>α : Type u'<VAR>φ : L ≃ᴸ L'<GOAL>⇑φ.onFormula = φ.toLHom.onFormula
<VAR>L : FirstOrder.Language<VAR>L' : FirstOrder.Language<VAR>α : Type u'<VAR>φ : L ≃ᴸ L'<GOAL>φ.onFormula.symm = φ.symm.onFormula
<VAR>L : FirstOrder.Language<VAR>L' : FirstOrder.Language<VAR>φ : L ≃ᴸ L'<GOAL>∀ (a : L'.BoundedFormula Empty 0), φ.onSentence.symm a = φ.invLHom.onBoundedFormula a
<VAR>L : FirstOrder.Language<VAR>L' : FirstOrder.Language<VAR>φ : L ≃ᴸ L'<GOAL>∀ (a : L.BoundedFormula Empty 0), φ.onSentence a = φ.toLHom.onBoundedFormula a
<VAR>L : FirstOrder.Language<VAR>α : Type u'<VAR>φ : L.Formula α<GOAL>FirstOrder.Language.Formula.equivSentence φ.not = FirstOrder.Language.Formula.not (FirstOrder.Language.Formula.equivSentence φ)
<VAR>L : FirstOrder.Language<VAR>α : Type u'<VAR>φ ψ : L.Formula α<GOAL>FirstOrder.Language.Formula.equivSentence (φ ⊓ ψ) = FirstOrder.Language.Formula.equivSentence φ ⊓ FirstOrder.Language.Formula.equivSentence ψ
<VAR>L : FirstOrder.Language<VAR>α : Type u'<VAR>s t : Set α<VAR>h : s ⊆ t<GOAL>L.distinctConstantsTheory s ⊆ L.distinctConstantsTheory t
<VAR>L : FirstOrder.Language<VAR>α : Type u'<GOAL>Monotone L.distinctConstantsTheory
<VAR>L : FirstOrder.Language<VAR>α : Type u'<GOAL>Directed (fun x x_1 => x ⊆ x_1) L.distinctConstantsTheory
<VAR>L : FirstOrder.Language<VAR>α : Type u'<VAR>s : Set α<GOAL>L.distinctConstantsTheory s = ⋃ t, L.distinctConstantsTheory ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ s) t)
<VAR>n : ZMod 9<GOAL>(ZMod.castHom ⋯ (ZMod 3)) n ≠ 0 → n ^ 3 = 1 ∨ n ^ 3 = 8
<VAR>a b c : ℤ<VAR>ha : a ≠ 0<VAR>h3a : 3 ∣ a<VAR>Hgcd : {a, b, c}.gcd id = 1<VAR>H : ∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3<GOAL>a ^ 3 + b ^ 3 + c ^ 3 ≠ 0
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<GOAL>FermatLastTheoremForThreeGen hζ → FermatLastTheoremFor 3
<VAR>K : Type u_1<VAR>Field K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>self : FermatLastTheoremForThreeGen.Solution' hζ<GOAL>self.c ≠ 0
<VAR>K : Type u_1<VAR>Field K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>self : FermatLastTheoremForThreeGen.Solution' hζ<GOAL>¬hζ.toInteger - 1 ∣ self.a
<VAR>K : Type u_1<VAR>Field K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>self : FermatLastTheoremForThreeGen.Solution' hζ<GOAL>IsCoprime self.a self.b
<VAR>K : Type u_1<VAR>Field K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>self : FermatLastTheoremForThreeGen.Solution' hζ<GOAL>¬hζ.toInteger - 1 ∣ self.b
<VAR>K : Type u_1<VAR>Field K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>self : FermatLastTheoremForThreeGen.Solution' hζ<GOAL>hζ.toInteger - 1 ∣ self.c
<VAR>K : Type u_1<VAR>Field K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>self : FermatLastTheoremForThreeGen.Solution' hζ<GOAL>self.a ^ 3 + self.b ^ 3 = ↑self.u * self.c ^ 3
<VAR>K : Type u_1<VAR>Field K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>self : FermatLastTheoremForThreeGen.Solution hζ<GOAL>(hζ.toInteger - 1) ^ 2 ∣ self.a + self.b
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S' : FermatLastTheoremForThreeGen.Solution' hζ<GOAL>multiplicity.Finite (hζ.toInteger - 1) S'.c
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : FermatLastTheoremForThreeGen.Solution hζ<VAR>DecidableRel fun a b => a ∣ b<GOAL>∃ S₁, S₁.isMinimal
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S' : FermatLastTheoremForThreeGen.Solution' hζ<GOAL>(hζ.toInteger - 1) ^ 4 ∣ S'.a ^ 3 - 1 ∧ (hζ.toInteger - 1) ^ 4 ∣ S'.b ^ 3 + 1 ∨ (hζ.toInteger - 1) ^ 4 ∣ S'.a ^ 3 + 1 ∧ (hζ.toInteger - 1) ^ 4 ∣ S'.b ^ 3 - 1
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S' : FermatLastTheoremForThreeGen.Solution' hζ<GOAL>(hζ.toInteger - 1) ^ 4 ∣ S'.c ^ 3
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S' : FermatLastTheoremForThreeGen.Solution' hζ<VAR>DecidableRel fun a b => a ∣ b<GOAL>(hζ.toInteger - 1) ^ 2 ∣ S'.c
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S' : FermatLastTheoremForThreeGen.Solution' hζ<VAR>DecidableRel fun a b => a ∣ b<GOAL>2 ≤ S'.multiplicity
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : FermatLastTheoremForThreeGen.Solution hζ<VAR>DecidableRel fun a b => a ∣ b<GOAL>2 ≤ S.multiplicity
<VAR>K : Type u_1<VAR>Field K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S' : FermatLastTheoremForThreeGen.Solution' hζ<GOAL>S'.a ^ 3 + S'.b ^ 3 = (S'.a + S'.b) * (S'.a + ↑⋯.unit * S'.b) * (S'.a + ↑⋯.unit ^ 2 * S'.b)
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S' : FermatLastTheoremForThreeGen.Solution' hζ<VAR>DecidableRel fun a b => a ∣ b<GOAL>(hζ.toInteger - 1) ^ 2 ∣ S'.a + S'.b ∨ (hζ.toInteger - 1) ^ 2 ∣ S'.a + ↑⋯.unit * S'.b ∨ (hζ.toInteger - 1) ^ 2 ∣ S'.a + ↑⋯.unit ^ 2 * S'.b
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S' : FermatLastTheoremForThreeGen.Solution' hζ<VAR>DecidableRel fun a b => a ∣ b<GOAL>∃ a' b', a' ^ 3 + b' ^ 3 = ↑S'.u * S'.c ^ 3 ∧ IsCoprime a' b' ∧ ¬hζ.toInteger - 1 ∣ a' ∧ ¬hζ.toInteger - 1 ∣ b' ∧ (hζ.toInteger - 1) ^ 2 ∣ a' + b'
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S' : FermatLastTheoremForThreeGen.Solution' hζ<VAR>DecidableRel fun a b => a ∣ b<GOAL>∃ S₁, S₁.multiplicity = S'.multiplicity
<VAR>K : Type u_1<VAR>Field K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : FermatLastTheoremForThreeGen.Solution hζ<GOAL>S.a + ↑⋯.unit * S.b = S.a + S.b + (hζ.toInteger - 1) * S.b
<VAR>K : Type u_1<VAR>Field K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : FermatLastTheoremForThreeGen.Solution hζ<GOAL>hζ.toInteger - 1 ∣ S.a + ↑⋯.unit * S.b
<VAR>K : Type u_1<VAR>Field K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : FermatLastTheoremForThreeGen.Solution hζ<GOAL>hζ.toInteger - 1 ∣ S.a + ↑⋯.unit ^ 2 * S.b
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : FermatLastTheoremForThreeGen.Solution hζ<GOAL>¬(hζ.toInteger - 1) ^ 2 ∣ S.a + ↑⋯.unit * S.b
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : FermatLastTheoremForThreeGen.Solution hζ<GOAL>¬(hζ.toInteger - 1) ^ 2 ∣ S.a + ↑⋯.unit ^ 2 * S.b
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : FermatLastTheoremForThreeGen.Solution hζ<VAR>p : NumberField.RingOfIntegers K<VAR>hp : Prime p<VAR>hpab : p ∣ S.a + S.b<VAR>hpaηb : p ∣ S.a + ↑⋯.unit * S.b<GOAL>Associated p (hζ.toInteger - 1)
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : FermatLastTheoremForThreeGen.Solution hζ<VAR>p : NumberField.RingOfIntegers K<VAR>hp : Prime p<VAR>hpab : p ∣ S.a + S.b<VAR>hpaηsqb : p ∣ S.a + ↑⋯.unit ^ 2 * S.b<GOAL>Associated p (hζ.toInteger - 1)
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : FermatLastTheoremForThreeGen.Solution hζ<VAR>p : NumberField.RingOfIntegers K<VAR>hp : Prime p<VAR>hpaηb : p ∣ S.a + ↑⋯.unit * S.b<VAR>hpaηsqb : p ∣ S.a + ↑⋯.unit ^ 2 * S.b<GOAL>Associated p (hζ.toInteger - 1)
<VAR>K : Type u_1<VAR>Field K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : FermatLastTheoremForThreeGen.Solution hζ<GOAL>S.a + ↑⋯.unit * S.b = (hζ.toInteger - 1) * FermatLastTheoremForThreeGen.Solution.y S
<VAR>K : Type u_1<VAR>Field K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : FermatLastTheoremForThreeGen.Solution hζ<GOAL>S.a + ↑⋯.unit ^ 2 * S.b = (hζ.toInteger - 1) * FermatLastTheoremForThreeGen.Solution.z S
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : FermatLastTheoremForThreeGen.Solution hζ<GOAL>¬hζ.toInteger - 1 ∣ FermatLastTheoremForThreeGen.Solution.y S
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : FermatLastTheoremForThreeGen.Solution hζ<GOAL>¬hζ.toInteger - 1 ∣ FermatLastTheoremForThreeGen.Solution.z S
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : FermatLastTheoremForThreeGen.Solution hζ<VAR>DecidableRel fun a b => a ∣ b<GOAL>(hζ.toInteger - 1) ^ (3 * S.multiplicity - 2) ∣ S.a + S.b
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : FermatLastTheoremForThreeGen.Solution hζ<VAR>DecidableRel fun a b => a ∣ b<GOAL>S.a + S.b = (hζ.toInteger - 1) ^ (3 * S.multiplicity - 2) * FermatLastTheoremForThreeGen.Solution.x S
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : FermatLastTheoremForThreeGen.Solution hζ<VAR>DecidableRel fun a b => a ∣ b<GOAL>S.c = (hζ.toInteger - 1) ^ S.multiplicity * FermatLastTheoremForThreeGen.Solution.w S
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : FermatLastTheoremForThreeGen.Solution hζ<VAR>DecidableRel fun a b => a ∣ b<GOAL>¬hζ.toInteger - 1 ∣ FermatLastTheoremForThreeGen.Solution.w S
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : FermatLastTheoremForThreeGen.Solution hζ<VAR>DecidableRel fun a b => a ∣ b<GOAL>¬hζ.toInteger - 1 ∣ FermatLastTheoremForThreeGen.Solution.x S
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>r s t w : NumberField.RingOfIntegers K<VAR>hr : ¬hζ.toInteger - 1 ∣ r<VAR>hs : ¬hζ.toInteger - 1 ∣ s<VAR>Hp : ∀ {p : NumberField.RingOfIntegers K}, Prime p → p ∣ t → p ∣ w → Associated p (hζ.toInteger - 1)<VAR>H₁ : ∀ {q : NumberField.RingOfIntegers K}, q ∣ r → q ∣ t<VAR>H₂ : ∀ {q : NumberField.RingOfIntegers K}, q ∣ s → q ∣ w<GOAL>IsCoprime r s
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : FermatLastTheoremForThreeGen.Solution hζ<VAR>DecidableRel fun a b => a ∣ b<GOAL>IsCoprime (FermatLastTheoremForThreeGen.Solution.x S) (FermatLastTheoremForThreeGen.Solution.y S)
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : FermatLastTheoremForThreeGen.Solution hζ<VAR>DecidableRel fun a b => a ∣ b<GOAL>IsCoprime (FermatLastTheoremForThreeGen.Solution.x S) (FermatLastTheoremForThreeGen.Solution.z S)
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : FermatLastTheoremForThreeGen.Solution hζ<GOAL>IsCoprime (FermatLastTheoremForThreeGen.Solution.y S) (FermatLastTheoremForThreeGen.Solution.z S)
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : FermatLastTheoremForThreeGen.Solution hζ<VAR>DecidableRel fun a b => a ∣ b<GOAL>FermatLastTheoremForThreeGen.Solution.x S * FermatLastTheoremForThreeGen.Solution.y S * FermatLastTheoremForThreeGen.Solution.z S = ↑S.u * FermatLastTheoremForThreeGen.Solution.w S ^ 3
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : FermatLastTheoremForThreeGen.Solution hζ<VAR>DecidableRel fun a b => a ∣ b<GOAL>(∃ X, Associated (X ^ 3) (FermatLastTheoremForThreeGen.Solution.x S)) ∧ (∃ Y, Associated (Y ^ 3) (FermatLastTheoremForThreeGen.Solution.y S)) ∧ ∃ Z, Associated (Z ^ 3) (FermatLastTheoremForThreeGen.Solution.z S)
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : FermatLastTheoremForThreeGen.Solution hζ<VAR>DecidableRel fun a b => a ∣ b<GOAL>FermatLastTheoremForThreeGen.Solution.X S ^ 3 * ↑(FermatLastTheoremForThreeGen.Solution.u₁ S) = FermatLastTheoremForThreeGen.Solution.x S
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : FermatLastTheoremForThreeGen.Solution hζ<VAR>DecidableRel fun a b => a ∣ b<GOAL>FermatLastTheoremForThreeGen.Solution.Y S ^ 3 * ↑(FermatLastTheoremForThreeGen.Solution.u₂ S) = FermatLastTheoremForThreeGen.Solution.y S
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : FermatLastTheoremForThreeGen.Solution hζ<VAR>DecidableRel fun a b => a ∣ b<GOAL>FermatLastTheoremForThreeGen.Solution.Z S ^ 3 * ↑(FermatLastTheoremForThreeGen.Solution.u₃ S) = FermatLastTheoremForThreeGen.Solution.z S
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : FermatLastTheoremForThreeGen.Solution hζ<VAR>DecidableRel fun a b => a ∣ b<GOAL>FermatLastTheoremForThreeGen.Solution.X S ≠ 0
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : FermatLastTheoremForThreeGen.Solution hζ<VAR>DecidableRel fun a b => a ∣ b<GOAL>¬hζ.toInteger - 1 ∣ FermatLastTheoremForThreeGen.Solution.X S
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : FermatLastTheoremForThreeGen.Solution hζ<VAR>DecidableRel fun a b => a ∣ b<GOAL>¬hζ.toInteger - 1 ∣ FermatLastTheoremForThreeGen.Solution.Y S
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : FermatLastTheoremForThreeGen.Solution hζ<VAR>DecidableRel fun a b => a ∣ b<GOAL>¬hζ.toInteger - 1 ∣ FermatLastTheoremForThreeGen.Solution.Z S
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : FermatLastTheoremForThreeGen.Solution hζ<VAR>DecidableRel fun a b => a ∣ b<GOAL>IsCoprime (FermatLastTheoremForThreeGen.Solution.Y S) (FermatLastTheoremForThreeGen.Solution.Z S)
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : FermatLastTheoremForThreeGen.Solution hζ<VAR>DecidableRel fun a b => a ∣ b<GOAL>FermatLastTheoremForThreeGen.Solution.X S ^ 3 * ↑(FermatLastTheoremForThreeGen.Solution.u₁ S) * (hζ.toInteger - 1) ^ (3 * S.multiplicity - 2) + FermatLastTheoremForThreeGen.Solution.Y S ^ 3 * ↑(FermatLastTheoremForThreeGen.Solution.u₂ S) * (hζ.toInteger - 1) * ↑⋯.unit + FermatLastTheoremForThreeGen.Solution.Z S ^ 3 * ↑(FermatLastTheoremForThreeGen.Solution.u₃ S) * (hζ.toInteger - 1) * ↑⋯.unit ^ 2 = 0
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : FermatLastTheoremForThreeGen.Solution hζ<VAR>DecidableRel fun a b => a ∣ b<GOAL>FermatLastTheoremForThreeGen.Solution.u₄ S = ⋯.unit * FermatLastTheoremForThreeGen.Solution.u₃ S * (FermatLastTheoremForThreeGen.Solution.u₂ S)⁻¹
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : FermatLastTheoremForThreeGen.Solution hζ<VAR>DecidableRel fun a b => a ∣ b<GOAL>FermatLastTheoremForThreeGen.Solution.u₅ S = -⋯.unit ^ 2 * FermatLastTheoremForThreeGen.Solution.u₁ S * (FermatLastTheoremForThreeGen.Solution.u₂ S)⁻¹
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : FermatLastTheoremForThreeGen.Solution hζ<VAR>DecidableRel fun a b => a ∣ b<GOAL>FermatLastTheoremForThreeGen.Solution.Y S ^ 3 + ↑(FermatLastTheoremForThreeGen.Solution.u₄ S) * FermatLastTheoremForThreeGen.Solution.Z S ^ 3 = ↑(FermatLastTheoremForThreeGen.Solution.u₅ S) * ((hζ.toInteger - 1) ^ (S.multiplicity - 1) * FermatLastTheoremForThreeGen.Solution.X S) ^ 3
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : FermatLastTheoremForThreeGen.Solution hζ<VAR>DecidableRel fun a b => a ∣ b<GOAL>(hζ.toInteger - 1) ^ 2 ∣ ↑(FermatLastTheoremForThreeGen.Solution.u₅ S) * ((hζ.toInteger - 1) ^ (S.multiplicity - 1) * FermatLastTheoremForThreeGen.Solution.X S) ^ 3
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : FermatLastTheoremForThreeGen.Solution hζ<VAR>DecidableRel fun a b => a ∣ b<GOAL>FermatLastTheoremForThreeGen.Solution.u₄ S = 1 ∨ FermatLastTheoremForThreeGen.Solution.u₄ S = -1
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : FermatLastTheoremForThreeGen.Solution hζ<VAR>DecidableRel fun a b => a ∣ b<GOAL>FermatLastTheoremForThreeGen.Solution.u₄ S ^ 2 = 1
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : FermatLastTheoremForThreeGen.Solution hζ<VAR>DecidableRel fun a b => a ∣ b<GOAL>FermatLastTheoremForThreeGen.Solution.Y S ^ 3 + (↑(FermatLastTheoremForThreeGen.Solution.u₄ S) * FermatLastTheoremForThreeGen.Solution.Z S) ^ 3 = ↑(FermatLastTheoremForThreeGen.Solution.u₅ S) * ((hζ.toInteger - 1) ^ (S.multiplicity - 1) * FermatLastTheoremForThreeGen.Solution.X S) ^ 3
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : FermatLastTheoremForThreeGen.Solution hζ<VAR>DecidableRel fun a b => a ∣ b<GOAL>S.Solution'_descent.multiplicity = S.multiplicity - 1
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : FermatLastTheoremForThreeGen.Solution hζ<VAR>DecidableRel fun a b => a ∣ b<GOAL>S.Solution'_descent.multiplicity < S.multiplicity
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : FermatLastTheoremForThreeGen.Solution hζ<VAR>DecidableRel fun a b => a ∣ b<GOAL>∃ S₁, S₁.multiplicity < S.multiplicity
<VAR>K : Type u_1<VAR>CommRing K<VAR>FirstOrder.Ring.CompatibleRing K<VAR>n : ℕ<VAR>v : Empty → K<GOAL>FirstOrder.Language.Formula.Realize (FirstOrder.Field.eqZero n) v ↔ ↑n = 0
<VAR>p : ℕ<VAR>K : Type u_1<VAR>Field K<VAR>FirstOrder.Ring.CompatibleRing K<GOAL>K ⊨ FirstOrder.Language.Theory.fieldOfChar p ↔ CharP K p
<VAR>p : ℕ<VAR>K : Type u_1<VAR>Field K<VAR>FirstOrder.Ring.CompatibleRing K<VAR>h : K ⊨ FirstOrder.Language.Theory.fieldOfChar p<GOAL>CharP K p
<VAR>α : Type u_1<VAR>M : α → Type u_2<VAR>u : Ultrafilter α<VAR>L : FirstOrder.Language<VAR>(a : α) → L.Structure (M a)<VAR>n : ℕ<VAR>f : L.Functions n<VAR>x : Fin n → (a : α) → M a<GOAL>(FirstOrder.Language.Structure.funMap f fun i => Quotient.mk' (x i)) = Quotient.mk' fun a => FirstOrder.Language.Structure.funMap f fun i => x i a
<VAR>α : Type u_1<VAR>M : α → Type u_2<VAR>u : Ultrafilter α<VAR>L : FirstOrder.Language<VAR>(a : α) → L.Structure (M a)<VAR>β : Type u_3<VAR>x : β → (a : α) → M a<VAR>t : L.Term β<GOAL>FirstOrder.Language.Term.realize (fun i => Quotient.mk' (x i)) t = Quotient.mk' fun a => FirstOrder.Language.Term.realize (fun i => x i a) t
<VAR>α : Type u_1<VAR>M : α → Type u_2<VAR>u : Ultrafilter α<VAR>L : FirstOrder.Language<VAR>(a : α) → L.Structure (M a)<VAR>∀ (a : α), Nonempty (M a)<VAR>β : Type u_3<VAR>n : ℕ<VAR>φ : L.BoundedFormula β n<VAR>x : β → (a : α) → M a<VAR>v : Fin n → (a : α) → M a<GOAL>(φ.Realize (fun i => Quotient.mk' (x i)) fun i => Quotient.mk' (v i)) ↔ ∀ᶠ (a : α) in ↑u, φ.Realize (fun i => x i a) fun i => v i a
<VAR>α : Type u_1<VAR>M : α → Type u_2<VAR>u : Ultrafilter α<VAR>L : FirstOrder.Language<VAR>(a : α) → L.Structure (M a)<VAR>∀ (a : α), Nonempty (M a)<VAR>β : Type u_3<VAR>φ : L.Formula β<VAR>x : β → (a : α) → M a<GOAL>(φ.Realize fun i => Quotient.mk' (x i)) ↔ ∀ᶠ (a : α) in ↑u, φ.Realize fun i => x i a
<VAR>α : Type u_1<VAR>M : α → Type u_2<VAR>u : Ultrafilter α<VAR>L : FirstOrder.Language<VAR>(a : α) → L.Structure (M a)<VAR>∀ (a : α), Nonempty (M a)<VAR>φ : L.Sentence<GOAL>(↑u).Product M ⊨ φ ↔ ∀ᶠ (a : α) in ↑u, M a ⊨ φ
<VAR>α : Type u_1<VAR>p : FreeCommRing α<GOAL>∃ t, FirstOrder.Language.Term.realize FreeCommRing.of t = p
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>CommRing R<VAR>FirstOrder.Ring.CompatibleRing R<VAR>p : FreeCommRing α<VAR>v : α → R<GOAL>FirstOrder.Language.Term.realize v (FirstOrder.Ring.termOfFreeCommRing p) = (FreeCommRing.lift v) p
<VAR>α : Type u_2<GOAL>0 = FirstOrder.Language.Constants.term FirstOrder.Ring.zeroFunc
<VAR>α : Type u_2<GOAL>1 = FirstOrder.Language.Constants.term FirstOrder.Ring.oneFunc
<VAR>α : Type u_2<VAR>t₁ t₂ : FirstOrder.Language.ring.Term α<GOAL>t₁ + t₂ = FirstOrder.Ring.addFunc.apply₂ t₁ t₂
<VAR>α : Type u_2<VAR>t₁ t₂ : FirstOrder.Language.ring.Term α<GOAL>t₁ * t₂ = FirstOrder.Ring.mulFunc.apply₂ t₁ t₂
<VAR>α : Type u_2<VAR>t : FirstOrder.Language.ring.Term α<GOAL>-t = FirstOrder.Ring.negFunc.apply₁ t