harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/FLT/Basic.lean
lemma fermatLastTheoremWith_nat_int_rat_tfae (n : ℕ) :
    TFAE [FermatLastTheoremWith ℕ n, FermatLastTheoremWith ℤ n, FermatLastTheoremWith ℚ n]

Proof state:
n : ℕ
tfae_1_to_2 : FermatLastTheoremWith ℕ n → FermatLastTheoremWith ℤ n
h : FermatLastTheoremWith ℤ n
a b c : ℚ
ha : a.num ≠ 0
hb : b.num ≠ 0
hc : c.num ≠ 0
habc : a ^ n + b ^ n = c ^ n
this : (↑a.den * ↑b.den * ↑c.den) ^ n ≠ 0
⊢ ↑((a.num * ↑b.den * ↑c.den) ^ n + (↑a.den * b.num * ↑c.den) ^ n) / (↑a.den * ↑b.den * ↑c.den) ^ n =
    ↑((↑a.den * ↑b.den * c.num) ^ n) / (↑a.den * ↑b.den * ↑c.den) ^ n

Tactic:
push_cast

Result:
n : ℕ
tfae_1_to_2 : FermatLastTheoremWith ℕ n → FermatLastTheoremWith ℤ n
h : FermatLastTheoremWith ℤ n
a b c : ℚ
ha : a.num ≠ 0
hb : b.num ≠ 0
hc : c.num ≠ 0
habc : a ^ n + b ^ n = c ^ n
this : (↑a.den * ↑b.den * ↑c.den) ^ n ≠ 0
⊢ ((↑a.num * ↑b.den * ↑c.den) ^ n + (↑a.den * ↑b.num * ↑c.den) ^ n) / (↑a.den * ↑b.den * ↑c.den) ^ n =
    (↑a.den * ↑b.den * ↑c.num) ^ n / (↑a.den * ↑b.den * ↑c.den) ^ n

Proof state:
case inr.inr.inr.inr
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha✝ : a ≠ 0
hb✝ : b ≠ 0
hc✝ : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : 0 < a
hb : 0 < b
hc : 0 < c
⊢ |a| ^ n + |b| ^ n = |c| ^ n

Tactic:
simp only [abs_of_pos, habc, *]

Result:
no goals

Proof state:
case inr.inr.inl.inr
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha✝ : a ≠ 0
hb✝ : b ≠ 0
hc✝ : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : 0 < a
hb : b < 0
hc : 0 < c
⊢ False

Tactic:
refine h c.natAbs b.natAbs a.natAbs (by positivity) (by positivity) (by positivity)
  (Int.natCast_inj.1 ?_)

Result:
case inr.inr.inl.inr
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha✝ : a ≠ 0
hb✝ : b ≠ 0
hc✝ : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : 0 < a
hb : b < 0
hc : 0 < c
⊢ ↑(c.natAbs ^ n + b.natAbs ^ n) = ↑(a.natAbs ^ n)

Proof state:
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha✝ : a ≠ 0
hb✝ : b ≠ 0
hc✝ : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : 0 < a
hb : 0 < b
hc : 0 < c
⊢ b.natAbs ≠ 0

Tactic:
positivity

Result:
no goals

Proof state:
case inr.inl.inl.inl
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha✝ : a ≠ 0
hb✝ : b ≠ 0
hc✝ : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : a < 0
hb : b < 0
hc : c < 0
⊢ False

Tactic:
refine h a.natAbs b.natAbs c.natAbs (by positivity) (by positivity) (by positivity)
  (Int.natCast_inj.1 ?_)

Result:
case inr.inl.inl.inl
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha✝ : a ≠ 0
hb✝ : b ≠ 0
hc✝ : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : a < 0
hb : b < 0
hc : c < 0
⊢ ↑(a.natAbs ^ n + b.natAbs ^ n) = ↑(c.natAbs ^ n)
-- Mathlib/Algebra/ContinuedFractions/ConvergentsEquiv.lean
theorem squashSeq_nth_of_lt {m : ℕ} (m_lt_n : m < n) : (squashSeq s n).get? m = s.get? m

Proof state:
case some.intro.intro
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
m : ℕ
m_lt_n : m < n
val✝ : Pair K
s_succ_nth_eq : s.get? (n + 1) = some val✝
gp_n : Pair K
s_nth_eq : s.get? n = some gp_n
gp_m : Pair K
s_mth_eq : s.get? m = some gp_m
⊢ (squashSeq s n).get? m = s.get? m

Tactic:
simp [*, squashSeq, m_lt_n.ne]

Result:
no goals

Proof state:
case none
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
m : ℕ
m_lt_n : m < n
s_succ_nth_eq : s.get? (n + 1) = none
⊢ (squashSeq s n).get? m = s.get? m

Tactic:
rw [squashSeq_eq_self_of_terminated s_succ_nth_eq]

Result:
no goals

Proof state:
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
m : ℕ
m_lt_n : m < n
⊢ (squashSeq s n).get? m = s.get? m

Tactic:
cases s_succ_nth_eq : s.get? (n + 1) with
| none => rw [squashSeq_eq_self_of_terminated s_succ_nth_eq]
| some =>
  obtain ⟨gp_n, s_nth_eq⟩ : ∃ gp_n, s.get? n = some gp_n :=
    s.ge_stable n.le_succ s_succ_nth_eq
  obtain ⟨gp_m, s_mth_eq⟩ : ∃ gp_m, s.get? m = some gp_m :=
    s.ge_stable (le_of_lt m_lt_n) s_nth_eq
  simp [*, squashSeq, m_lt_n.ne]

Result:
no goals

Proof state:
case some
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
m : ℕ
m_lt_n : m < n
val✝ : Pair K
s_succ_nth_eq : s.get? (n + 1) = some val✝
⊢ (squashSeq s n).get? m = s.get? m

Tactic:
obtain ⟨gp_n, s_nth_eq⟩ : ∃ gp_n, s.get? n = some gp_n :=
  s.ge_stable n.le_succ s_succ_nth_eq

Result:
case some.intro
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
m : ℕ
m_lt_n : m < n
val✝ : Pair K
s_succ_nth_eq : s.get? (n + 1) = some val✝
gp_n : Pair K
s_nth_eq : s.get? n = some gp_n
⊢ (squashSeq s n).get? m = s.get? m

Proof state:
case some.intro
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
m : ℕ
m_lt_n : m < n
val✝ : Pair K
s_succ_nth_eq : s.get? (n + 1) = some val✝
gp_n : Pair K
s_nth_eq : s.get? n = some gp_n
⊢ (squashSeq s n).get? m = s.get? m

Tactic:
obtain ⟨gp_m, s_mth_eq⟩ : ∃ gp_m, s.get? m = some gp_m :=
  s.ge_stable (le_of_lt m_lt_n) s_nth_eq

Result:
case some.intro.intro
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
m : ℕ
m_lt_n : m < n
val✝ : Pair K
s_succ_nth_eq : s.get? (n + 1) = some val✝
gp_n : Pair K
s_nth_eq : s.get? n = some gp_n
gp_m : Pair K
s_mth_eq : s.get? m = some gp_m
⊢ (squashSeq s n).get? m = s.get? m
-- Mathlib/Analysis/InnerProductSpace/EuclideanDist.lean
theorem closure_ball (x : E) {r : ℝ} (h : r ≠ 0) : closure (ball x r) = closedBall x r

Proof state:
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : T2Space E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
r : ℝ
h : r ≠ 0
⊢ closure (ball x r) = closedBall x r

Tactic:
rw [ball_eq_preimage, ← toEuclidean.preimage_closure, closure_ball (toEuclidean x) h,
  closedBall_eq_preimage]

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem cosh_three_mul : cosh (3 * x) = 4 * cosh x ^ 3 - 3 * cosh x

Proof state:
x : ℂ
h1 : x + 2 * x = 3 * x
⊢ cosh x * (cosh x ^ 2 + sinh x ^ 2) + sinh x * (2 * sinh x * cosh x) = 4 * cosh x ^ 3 - 3 * cosh x

Tactic:
have h2 : sinh x * (2 * sinh x * cosh x) = 2 * cosh x * sinh x ^ 2 := by ring

Result:
x : ℂ
h1 : x + 2 * x = 3 * x
h2 : sinh x * (2 * sinh x * cosh x) = 2 * cosh x * sinh x ^ 2
⊢ cosh x * (cosh x ^ 2 + sinh x ^ 2) + sinh x * (2 * sinh x * cosh x) = 4 * cosh x ^ 3 - 3 * cosh x

Proof state:
x : ℂ
h1 : x + 2 * x = 3 * x
⊢ sinh x * (2 * sinh x * cosh x) = 2 * cosh x * sinh x ^ 2

Tactic:
ring

Result:
no goals

Proof state:
x : ℂ
⊢ x + 2 * x = 3 * x

Tactic:
ring

Result:
no goals

Proof state:
x : ℂ
h1 : x + 2 * x = 3 * x
h2 : sinh x * (2 * sinh x * cosh x) = 2 * cosh x * sinh x ^ 2
⊢ cosh x * (cosh x ^ 2 + (cosh x ^ 2 - 1)) + 2 * cosh x * (cosh x ^ 2 - 1) = 4 * cosh x ^ 3 - 3 * cosh x

Tactic:
ring

Result:
no goals

Proof state:
x : ℂ
⊢ cosh (3 * x) = 4 * cosh x ^ 3 - 3 * cosh x

Tactic:
have h1 : x + 2 * x = 3 * x := by ring

Result:
x : ℂ
h1 : x + 2 * x = 3 * x
⊢ cosh (3 * x) = 4 * cosh x ^ 3 - 3 * cosh x

Proof state:
x : ℂ
h1 : x + 2 * x = 3 * x
⊢ cosh (3 * x) = 4 * cosh x ^ 3 - 3 * cosh x

Tactic:
rw [← h1, cosh_add x (2 * x)]

Result:
x : ℂ
h1 : x + 2 * x = 3 * x
⊢ cosh x * cosh (2 * x) + sinh x * sinh (2 * x) = 4 * cosh x ^ 3 - 3 * cosh x

Proof state:
x : ℂ
h1 : x + 2 * x = 3 * x
h2 : sinh x * (2 * sinh x * cosh x) = 2 * cosh x * sinh x ^ 2
⊢ cosh x * (cosh x ^ 2 + sinh x ^ 2) + sinh x * (2 * sinh x * cosh x) = 4 * cosh x ^ 3 - 3 * cosh x

Tactic:
rw [h2, sinh_sq]

Result:
x : ℂ
h1 : x + 2 * x = 3 * x
h2 : sinh x * (2 * sinh x * cosh x) = 2 * cosh x * sinh x ^ 2
⊢ cosh x * (cosh x ^ 2 + (cosh x ^ 2 - 1)) + 2 * cosh x * (cosh x ^ 2 - 1) = 4 * cosh x ^ 3 - 3 * cosh x

Proof state:
x : ℂ
h1 : x + 2 * x = 3 * x
⊢ cosh x * cosh (2 * x) + sinh x * sinh (2 * x) = 4 * cosh x ^ 3 - 3 * cosh x

Tactic:
simp only [cosh_two_mul, sinh_two_mul]

Result:
x : ℂ
h1 : x + 2 * x = 3 * x
⊢ cosh x * (cosh x ^ 2 + sinh x ^ 2) + sinh x * (2 * sinh x * cosh x) = 4 * cosh x ^ 3 - 3 * cosh x
-- Mathlib/Data/Int/Init.lean
lemma toNat_lt_toNat {a b : ℤ} (hb : 0 < b) : toNat a < toNat b ↔ a < b where
  mp h

Proof state:
a b : ℤ
hb : 0 < b
h : a < b
⊢ ↑a.toNat < b

Tactic:
cases a

Result:
case ofNat
b : ℤ
hb : 0 < b
a✝ : ℕ
h : ofNat a✝ < b
⊢ ↑(ofNat a✝).toNat < b

case negSucc
b : ℤ
hb : 0 < b
a✝ : ℕ
h : -[a✝+1] < b
⊢ ↑-[a✝+1].toNat < b

Proof state:
case ofNat
b : ℤ
hb : 0 < b
a✝ : ℕ
h : ofNat a✝ < b
⊢ ↑(ofNat a✝).toNat < b

case negSucc
b : ℤ
hb : 0 < b
a✝ : ℕ
h : -[a✝+1] < b
⊢ ↑-[a✝+1].toNat < b

Tactic:
exacts [h, hb]

Result:
no goals

Proof state:
case ofNat
b : ℤ
hb : 0 < b
a✝ : ℕ
h : (ofNat a✝).toNat < b.toNat
⊢ ofNat a✝ < b

case negSucc
b : ℤ
hb : 0 < b
a✝ : ℕ
h : -[a✝+1].toNat < b.toNat
⊢ -[a✝+1] < b

Tactic:
exacts [lt_toNat.1 h, Int.lt_trans (neg_of_sign_eq_neg_one rfl) hb]

Result:
no goals

Proof state:
a b : ℤ
hb : 0 < b
h : a < b
⊢ a.toNat < b.toNat

Tactic:
rw [lt_toNat]

Result:
a b : ℤ
hb : 0 < b
h : a < b
⊢ ↑a.toNat < b

Proof state:
a b : ℤ
hb : 0 < b
h : a.toNat < b.toNat
⊢ a < b

Tactic:
cases a

Result:
case ofNat
b : ℤ
hb : 0 < b
a✝ : ℕ
h : (ofNat a✝).toNat < b.toNat
⊢ ofNat a✝ < b

case negSucc
b : ℤ
hb : 0 < b
a✝ : ℕ
h : -[a✝+1].toNat < b.toNat
⊢ -[a✝+1] < b
-- Mathlib/Analysis/Convex/Hull.lean
theorem convexHull_neg (s : Set E) : convexHull 𝕜 (-s) = -convexHull 𝕜 s

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
⊢ (convexHull 𝕜) ((fun x => -x) '' s) = (fun x => -x) '' (convexHull 𝕜) s

Tactic:
exact AffineMap.image_convexHull (-1) _ |>.symm

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
⊢ (convexHull 𝕜) (-s) = -(convexHull 𝕜) s

Tactic:
simp_rw [← image_neg_eq_neg]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
⊢ (convexHull 𝕜) ((fun x => -x) '' s) = (fun x => -x) '' (convexHull 𝕜) s
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem size_insertMany_list [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
    {l : List ((a : α) × β a)} (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) :
    (∀ (a : α), m.contains a → (l.map Sigma.fst).contains a = false) →
    (m.insertMany l).1.1.size = m.1.size + l.length

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
l : List ((a : α) × β a)
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
⊢ (∀ (a : α), m.contains a = true → (List.map Sigma.fst l).contains a = false) →
    (m.insertMany l).val.val.size = m.val.size + l.length

Tactic:
simp_to_model [insertMany] using List.length_insertList

Result:
no goals
-- Mathlib/MeasureTheory/Measure/WithDensity.lean
theorem withDensity_zero : μ.withDensity 0 = 0

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
⊢ μ.withDensity 0 = 0

Tactic:
ext1 s hs

Result:
case h
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
⊢ (μ.withDensity 0) s = 0 s

Proof state:
case h
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
⊢ (μ.withDensity 0) s = 0 s

Tactic:
simp [withDensity_apply _ hs]

Result:
no goals
-- Mathlib/RingTheory/WittVector/Truncated.lean
theorem coeff_out (x : TruncatedWittVector p n R) (i : Fin n) : x.out.coeff i = x.coeff i

Proof state:
p n : ℕ
R : Type u_1
inst✝ : CommRing R
x : TruncatedWittVector p n R
i : Fin n
⊢ (if h : ↑i < n then coeff ⟨↑i, h⟩ x else 0) = coeff i x

Tactic:
rw [dif_pos i.is_lt, Fin.eta]

Result:
no goals

Proof state:
p n : ℕ
R : Type u_1
inst✝ : CommRing R
x : TruncatedWittVector p n R
i : Fin n
⊢ { coeff := fun i => if h : i < n then coeff ⟨i, h⟩ x else 0 }.coeff ↑i = coeff i x

Tactic:
dsimp only

Result:
p n : ℕ
R : Type u_1
inst✝ : CommRing R
x : TruncatedWittVector p n R
i : Fin n
⊢ (if h : ↑i < n then coeff ⟨↑i, h⟩ x else 0) = coeff i x

Proof state:
p n : ℕ
R : Type u_1
inst✝ : CommRing R
x : TruncatedWittVector p n R
i : Fin n
⊢ x.out.coeff ↑i = coeff i x

Tactic:
rw [out]

Result:
p n : ℕ
R : Type u_1
inst✝ : CommRing R
x : TruncatedWittVector p n R
i : Fin n
⊢ { coeff := fun i => if h : i < n then coeff ⟨i, h⟩ x else 0 }.coeff ↑i = coeff i x
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey?_eq_some_getKey [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} {h} :
    m.getKey? a = some (m.getKey a h)

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h✝ : m.WF
a : α
h : a ∈ m
⊢ m.getKey? a = some (m.getKey a h)

Tactic:
simp_to_raw using Raw₀.getKey?_eq_some_getKey

Result:
no goals
-- Mathlib/Algebra/BigOperators/Intervals.lean
theorem prod_Ico_add_right_sub_eq [OrderedCancelAddCommMonoid α] [ExistsAddOfLE α]
    [LocallyFiniteOrder α] [Sub α] [OrderedSub α] (a b c : α) :
    ∏ x ∈ Ico (a + c) (b + c), f (x - c) = ∏ x ∈ Ico a b, f x

Proof state:
α : Type u_1
M : Type u_2
inst✝⁵ : CommMonoid M
f : α → M
inst✝⁴ : OrderedCancelAddCommMonoid α
inst✝³ : ExistsAddOfLE α
inst✝² : LocallyFiniteOrder α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
⊢ ∏ x ∈ Ico (a + c) (b + c), f (x - c) = ∏ x ∈ Ico a b, f x

Tactic:
simp only [← map_add_right_Ico, prod_map, addRightEmbedding_apply, add_tsub_cancel_right]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Finite.lean
lemma edgeFinset_nonempty : G.edgeFinset.Nonempty ↔ G ≠ ⊥

Proof state:
V : Type u_1
G : SimpleGraph V
inst✝ : Fintype ↑G.edgeSet
⊢ G.edgeFinset.Nonempty ↔ G ≠ ⊥

Tactic:
rw [Finset.nonempty_iff_ne_empty, edgeFinset_eq_empty.ne]

Result:
no goals
-- Mathlib/NumberTheory/FLT/Three.lean
private lemma formula1 : S.X^3*S.u₁*λ^(3*S.multiplicity-2)+S.Y^3*S.u₂*λ*η+S.Z^3*S.u₃*λ*η^2 = 0

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ S.a + S.b + ↑η ^ 2 * S.b - S.a + ↑η ^ 2 * S.b + 2 * ↑η * S.b + S.b = 0

Tactic:
rw [eta_sq]

Result:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ S.a + S.b + (-↑η - 1) * S.b - S.a + (-↑η - 1) * S.b + 2 * ↑η * S.b + S.b = 0

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ S.a + S.b + (S.a + ↑η * S.b) * ↑η + (S.a + (-↑η - 1) * S.b) * (-↑η - 1) =
    S.a + S.b + ↑η ^ 2 * S.b - S.a + ↑η ^ 2 * S.b + 2 * ↑η * S.b + S.b

Tactic:
ring

Result:
no goals

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ S.a + S.b + (S.a + ↑η * S.b) * ↑η + (S.a + (-↑η - 1) * S.b) * (-↑η - 1) = 0

Tactic:
calc _ = S.a+S.b+η^2*S.b-S.a+η^2*S.b+2*η*S.b+S.b := by ring
_ = 0 := by rw [eta_sq]; ring

Result:
no goals

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ S.a + S.b + (-↑η - 1) * S.b - S.a + (-↑η - 1) * S.b + 2 * ↑η * S.b + S.b = 0

Tactic:
ring

Result:
no goals

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ FermatLastTheoremForThreeGen.Solution.X S ^ 3 * ↑(FermatLastTheoremForThreeGen.Solution.u₁ S) *
          λ ^ (3 * S.multiplicity - 2) +
        FermatLastTheoremForThreeGen.Solution.Y S ^ 3 * ↑(FermatLastTheoremForThreeGen.Solution.u₂ S) * λ * ↑η +
      FermatLastTheoremForThreeGen.Solution.Z S ^ 3 * ↑(FermatLastTheoremForThreeGen.Solution.u₃ S) * λ * ↑η ^ 2 =
    0

Tactic:
rw [X_u₁_spec, Y_u₂_spec, Z_u₃_spec, mul_comm S.x, ← x_spec, mul_comm S.y, ← y_spec, mul_comm S.z,
  ← z_spec, eta_sq]

Result:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ S.a + S.b + (S.a + ↑η * S.b) * ↑η + (S.a + (-↑η - 1) * S.b) * (-↑η - 1) = 0
-- Mathlib/GroupTheory/CosetCover.lean
theorem leftCoset_cover_filter_FiniteIndex_aux
    [DecidablePred (FiniteIndex : Subgroup G → Prop)] :
    (⋃ k ∈ s.filter (fun i => (H i).FiniteIndex), g k • (H k : Set G) = Set.univ) ∧
      (1 ≤ ∑ i ∈ s, ((H i).index : ℚ)⁻¹) ∧
      (∑ i ∈ s, ((H i).index : ℚ)⁻¹ = 1 → Set.PairwiseDisjoint
        (s.filter (fun i => (H i).FiniteIndex)) (fun i ↦ g i • (H i : Set G)))

Proof state:
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
inst✝ : DecidablePred FiniteIndex
D : Subgroup G := ⨅ k ∈ Finset.filter (fun i => (H i).FiniteIndex) s, H k
hD : D.FiniteIndex
hD_le : ∀ {i : ι}, i ∈ s → (H i).FiniteIndex → D ≤ H i
t : (i : ι) → i ∈ s → (H i).FiniteIndex → Finset ↥(H i)
ht :
  ∀ (i : ι) (hi : i ∈ s) (hfi : (H i).FiniteIndex),
    IsComplement ↑(t i hi hfi) ↑(D.subgroupOf (H i)) ∧ ⋃ g ∈ t i hi hfi, ↑g • ↑D = ↑(H i)
κ : Type (max u_2 u_1) := (i : { x // x ∈ s }) × { x // x ∈ if h : (H ↑i).FiniteIndex then t ↑i ⋯ h else {1} }
f : κ → G := fun k => g ↑k.fst * ↑↑k.snd
K : κ → Subgroup G := fun k => if (H ↑k.fst).FiniteIndex then D else H ↑k.fst
hcovers' : ⋃ k ∈ Finset.univ, f k • ↑(K k) = Set.univ
k : κ
hkfi : (H ↑k.fst).FiniteIndex
hk : K k = D
h : ⋃ i ∈ Finset.filter (fun x => K x = K k) Finset.univ, f i • ↑(K i) ≠ Set.univ
⊢ False

Tactic:
obtain ⟨i, -, hi⟩ :=
  exists_finiteIndex_of_leftCoset_cover_aux hcovers' k (Finset.mem_univ k) h

Result:
case intro.intro
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
inst✝ : DecidablePred FiniteIndex
D : Subgroup G := ⨅ k ∈ Finset.filter (fun i => (H i).FiniteIndex) s, H k
hD : D.FiniteIndex
hD_le : ∀ {i : ι}, i ∈ s → (H i).FiniteIndex → D ≤ H i
t : (i : ι) → i ∈ s → (H i).FiniteIndex → Finset ↥(H i)
ht :
  ∀ (i : ι) (hi : i ∈ s) (hfi : (H i).FiniteIndex),
    IsComplement ↑(t i hi hfi) ↑(D.subgroupOf (H i)) ∧ ⋃ g ∈ t i hi hfi, ↑g • ↑D = ↑(H i)
κ : Type (max u_2 u_1) := (i : { x // x ∈ s }) × { x // x ∈ if h : (H ↑i).FiniteIndex then t ↑i ⋯ h else {1} }
f : κ → G := fun k => g ↑k.fst * ↑↑k.snd
K : κ → Subgroup G := fun k => if (H ↑k.fst).FiniteIndex then D else H ↑k.fst
hcovers' : ⋃ k ∈ Finset.univ, f k • ↑(K k) = Set.univ
k : κ
hkfi : (H ↑k.fst).FiniteIndex
hk : K k = D
h : ⋃ i ∈ Finset.filter (fun x => K x = K k) Finset.univ, f i • ↑(K i) ≠ Set.univ
i : κ
hi : K i ≠ K k ∧ (K i).FiniteIndex
⊢ False
-- Mathlib/Data/Multiset/Sort.lean
theorem sort_cons (a : α) (s : Multiset α) :
    (∀ b ∈ s, r a b) → sort r (a ::ₘ s) = a :: sort r s

Proof state:
α : Type u_1
r : α → α → Prop
inst✝³ : DecidableRel r
inst✝² : IsTrans α r
inst✝¹ : IsAntisymm α r
inst✝ : IsTotal α r
a : α
s : Multiset α
l : List α
⊢ (∀ b ∈ Quot.mk (⇑(isSetoid α)) l, r a b) →
    sort r (a ::ₘ Quot.mk (⇑(isSetoid α)) l) = a :: sort r (Quot.mk (⇑(isSetoid α)) l)

Tactic:
simpa [mergeSort_eq_insertionSort] using insertionSort_cons r (a := a) (l := l)

Result:
no goals

Proof state:
α : Type u_1
r : α → α → Prop
inst✝³ : DecidableRel r
inst✝² : IsTrans α r
inst✝¹ : IsAntisymm α r
inst✝ : IsTotal α r
a : α
s : Multiset α
⊢ (∀ b ∈ s, r a b) → sort r (a ::ₘ s) = a :: sort r s

Tactic:
refine Quot.inductionOn s fun l => ?_

Result:
α : Type u_1
r : α → α → Prop
inst✝³ : DecidableRel r
inst✝² : IsTrans α r
inst✝¹ : IsAntisymm α r
inst✝ : IsTotal α r
a : α
s : Multiset α
l : List α
⊢ (∀ b ∈ Quot.mk (⇑(isSetoid α)) l, r a b) →
    sort r (a ::ₘ Quot.mk (⇑(isSetoid α)) l) = a :: sort r (Quot.mk (⇑(isSetoid α)) l)
-- Mathlib/GroupTheory/GroupAction/Hom.lean
theorem comp_id (f : X →ₑ[φ] Y) :
    f.comp (MulActionHom.id M) = f :=
  ext fun x => by rw [comp_apply, id_apply]

Proof state:
M : Type u_2
N : Type u_3
φ : M → N
X : Type u_5
inst✝¹ : SMul M X
Y : Type u_6
inst✝ : SMul N Y
f : X →ₑ[φ] Y
x : X
⊢ (f.comp (MulActionHom.id M)) x = f x

Tactic:
rw [comp_apply, id_apply]

Result:
no goals
-- Mathlib/Order/WellFoundedSet.lean
theorem partiallyWellOrderedOn_sup (s : Finset ι) {f : ι → Set α} :
    (s.sup f).PartiallyWellOrderedOn r ↔ ∀ i ∈ s, (f i).PartiallyWellOrderedOn r :=
  Finset.cons_induction_on s (by simp) fun a s ha hs => by simp [-sup_set_eq_biUnion, hs]

Proof state:
ι : Type u_1
α : Type u_2
r : α → α → Prop
s✝ : Finset ι
f : ι → Set α
a : ι
s : Finset ι
ha : a ∉ s
hs : (s.sup f).PartiallyWellOrderedOn r ↔ ∀ i ∈ s, (f i).PartiallyWellOrderedOn r
⊢ ((cons a s ha).sup f).PartiallyWellOrderedOn r ↔ ∀ i ∈ cons a s ha, (f i).PartiallyWellOrderedOn r

Tactic:
simp [-sup_set_eq_biUnion, hs]

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_2
r : α → α → Prop
s : Finset ι
f : ι → Set α
⊢ (∅.sup f).PartiallyWellOrderedOn r ↔ ∀ i ∈ ∅, (f i).PartiallyWellOrderedOn r

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/Polynomial.lean
lemma comap_C_surjective : Function.Surjective (comap (R := R) (C (σ := σ)))

Proof state:
R : Type u_2
inst✝ : CommRing R
σ : Type u_1
x : PrimeSpectrum R
⊢ (eval₂Hom (RingHom.id R) 0).comp C = RingHom.id R

Tactic:
ext

Result:
case a
R : Type u_2
inst✝ : CommRing R
σ : Type u_1
x : PrimeSpectrum R
x✝ : R
⊢ ((eval₂Hom (RingHom.id R) 0).comp C) x✝ = (RingHom.id R) x✝

Proof state:
case a
R : Type u_2
inst✝ : CommRing R
σ : Type u_1
x : PrimeSpectrum R
x✝ : R
⊢ ((eval₂Hom (RingHom.id R) 0).comp C) x✝ = (RingHom.id R) x✝

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_2
inst✝ : CommRing R
σ : Type u_1
x : PrimeSpectrum R
⊢ (comap C) ((comap (eval₂Hom (RingHom.id R) 0)) x) = x

Tactic:
rw [← comap_comp_apply, (show (eval₂Hom (.id _) 0).comp C = .id R by ext; simp),
  comap_id, ContinuousMap.id_apply]

Result:
no goals

Proof state:
R : Type u_2
inst✝ : CommRing R
σ : Type u_1
⊢ Function.Surjective ⇑(comap C)

Tactic:
intro x

Result:
R : Type u_2
inst✝ : CommRing R
σ : Type u_1
x : PrimeSpectrum R
⊢ ∃ a, (comap C) a = x

Proof state:
R : Type u_2
inst✝ : CommRing R
σ : Type u_1
x : PrimeSpectrum R
⊢ ∃ a, (comap C) a = x

Tactic:
refine ⟨comap (eval₂Hom (.id _) 0) x, ?_⟩

Result:
R : Type u_2
inst✝ : CommRing R
σ : Type u_1
x : PrimeSpectrum R
⊢ (comap C) ((comap (eval₂Hom (RingHom.id R) 0)) x) = x
-- Mathlib/Topology/UrysohnsLemma.lean
theorem approx_nonneg (c : CU P) (n : ℕ) (x : X) : 0 ≤ c.approx n x

Proof state:
case succ
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), 0 ≤ approx n c x
c : CU P
⊢ 0 ≤ 2⁻¹ • (approx n c.left x + approx n c.right x)

Tactic:
refine mul_nonneg (inv_nonneg.2 zero_le_two) (add_nonneg ?_ ?_) <;> apply ihn

Result:
no goals

Proof state:
case succ
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), 0 ≤ approx n c x
c : CU P
⊢ 0 ≤ approx (n + 1) c x

Tactic:
simp only [approx, midpoint_eq_smul_add, invOf_eq_inv]

Result:
case succ
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), 0 ≤ approx n c x
c : CU P
⊢ 0 ≤ 2⁻¹ • (approx n c.left x + approx n c.right x)

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
c : CU P
n : ℕ
x : X
⊢ 0 ≤ approx n c x

Tactic:
induction n generalizing c with
| zero => exact indicator_nonneg (fun _ _ => zero_le_one) _
| succ n ihn =>
  simp only [approx, midpoint_eq_smul_add, invOf_eq_inv]
  refine mul_nonneg (inv_nonneg.2 zero_le_two) (add_nonneg ?_ ?_) <;> apply ihn

Result:
no goals

Proof state:
case zero
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
x : X
c : CU P
⊢ 0 ≤ approx 0 c x

Tactic:
exact indicator_nonneg (fun _ _ => zero_le_one) _

Result:
no goals
-- Mathlib/Algebra/Ring/Ext.lean
theorem toNonUnitalNonAssocring_injective :
    Function.Injective (@toNonUnitalNonAssocRing R)

Proof state:
R : Type u
⊢ Function.Injective (@toNonUnitalNonAssocRing R)

Tactic:
intro _ _ _

Result:
R : Type u
a₁✝ a₂✝ : NonUnitalRing R
a✝ : toNonUnitalNonAssocRing = toNonUnitalNonAssocRing
⊢ a₁✝ = a₂✝

Proof state:
R : Type u
a₁✝ a₂✝ : NonUnitalRing R
a✝ : toNonUnitalNonAssocRing = toNonUnitalNonAssocRing
⊢ a₁✝ = a₂✝

Tactic:
ext <;> congr

Result:
no goals