mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d x y z w : ℕ
xy : { re := ↑x, im := -↑y }.Nonneg
zw : { re := -↑z, im := ↑w }.Nonneg
⊢ ({ re := ↑x, im := -↑y } + { re := -↑z, im := ↑w }).Nonneg

Tactic:
by
  have : Nonneg ⟨Int.subNatNat x z, Int.subNatNat w y⟩ :=
    Int.subNatNat_elim x z
      (fun m n i => SqLe y d m 1 → SqLe n 1 w d → Nonneg ⟨i, Int.subNatNat w y⟩)
      (fun j k =>
        Int.subNatNat_elim w y
          (fun m n i => SqLe n d (k + j) 1 → SqLe k 1 m d → Nonneg ⟨Int.ofNat j, i⟩)
          (fun _ _ _ _ => trivial) fun m n xy zw => sqLe_cancel zw xy)
      (fun j k =>
        Int.subNatNat_elim w y
          (fun m n i => SqLe n d k 1 → SqLe (k + j + 1) 1 m d → Nonneg ⟨-[j+1], i⟩)
          (fun m n xy zw => sqLe_cancel xy zw) fun m n xy zw =>
          let t := Nat.le_trans zw (sqLe_of_le (Nat.le_add_right n (m + 1)) le_rfl xy)
          have : k + j + 1 ≤ k :=
            Nat.mul_self_le_mul_self_iff.1 (by simpa [one_mul] using t)
          absurd this (not_le_of_gt <| Nat.succ_le_succ <| Nat.le_add_right _ _))
      (nonnegg_pos_neg.1 xy) (nonnegg_neg_pos.1 zw)
  rw [add_def, neg_add_eq_sub]
  rwa [Int.subNatNat_eq_coe, Int.subNatNat_eq_coe] at this

Goal state after:
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d x y : ℕ
ha : { re := ↑x, im := -↑y }.Nonneg
z w : ℕ
hb : { re := ↑z, im := ↑w }.Nonneg
i : ℕ
h : -↑y + ↑w = -↑i
⊢ -↑y + ↑w = -↑i

Tactic:
by simp [*]

Goal state after:
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: case inr.inr.inr.inl
d x y : ℕ
ha : { re := -↑x, im := ↑y }.Nonneg
z w : ℕ
hb : { re := ↑z, im := -↑w }.Nonneg
⊢ ({ re := -↑x, im := ↑y } + { re := ↑z, im := -↑w }).Nonneg

Tactic:
dsimp
    rw [add_comm, add_comm (y : ℤ)]
    exact nonneg_add_lem hb ha

Goal state after:
Module: Mathlib.NumberTheory.Cyclotomic.Discriminant

Goal state before:
pp: case pos
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
k : ℕ
hp : Fact (Nat.Prime 2)
hcycl : IsCyclotomicExtension {2 ^ (k + 1)} K L
hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))
hirr : Irreducible (cyclotomic (2 ^ (k + 1)) K)
hk : 2 ^ (k + 1) = 2 ^ 1
⊢ discr K ⇑(IsPrimitiveRoot.powerBasis K hζ).basis =
    (-1) ^ (φ (2 ^ (k + 1)) / 2) * ↑2 ^ (2 ^ (k + 1 - 1) * ((2 - 1) * (k + 1) - 1))

Tactic:
replace hk := Nat.pow_right_injective rfl.le hk

Goal state after:
case pos
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
k : ℕ
hp : Fact (Nat.Prime 2)
hcycl : IsCyclotomicExtension {2 ^ (k + 1)} K L
hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))
hirr : Irreducible (cyclotomic (2 ^ (k + 1)) K)
hk : k + 1 = 1
⊢ discr K ⇑(IsPrimitiveRoot.powerBasis K hζ).basis =
    (-1) ^ (φ (2 ^ (k + 1)) / 2) * ↑2 ^ (2 ^ (k + 1 - 1) * ((2 - 1) * (k + 1) - 1))
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: case pos
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun m ↦ ⌊fract (ξ * ↑m) * (↑n + 1)⌋
hn : 0 < ↑n + 1
hfu : ∀ (m : ℤ), fract (ξ * ↑m) * (↑n + 1) < ↑n + 1
D : Finset ℤ := Icc 0 ↑n
m : ℤ
hm : m ∈ D
hf : f m = ↑n
hf' : ↑↑n ≤ fract (ξ * ↑m) * (↑n + 1)
hm₀ : 0 < m
⊢ ∃ j k, 0 < k ∧ k ≤ ↑n ∧ |(ξ * ↑k - ↑j) * (↑n + 1)| ≤ 1

Tactic:
refine ⟨⌊ξ * m⌋ + 1, m, hm₀, (mem_Icc.mp hm).2, ?_⟩

Goal state after:
case pos
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun m ↦ ⌊fract (ξ * ↑m) * (↑n + 1)⌋
hn : 0 < ↑n + 1
hfu : ∀ (m : ℤ), fract (ξ * ↑m) * (↑n + 1) < ↑n + 1
D : Finset ℤ := Icc 0 ↑n
m : ℤ
hm : m ∈ D
hf : f m = ↑n
hf' : ↑↑n ≤ fract (ξ * ↑m) * (↑n + 1)
hm₀ : 0 < m
⊢ |(ξ * ↑m - ↑(⌊ξ * ↑m⌋ + 1)) * (↑n + 1)| ≤ 1
Module: Mathlib.NumberTheory.MulChar.Duality

Goal state before:
pp: M : Type u_1
R : Type u_2
inst✝³ : CommMonoid M
inst✝² : CommRing R
inst✝¹ : Finite M
inst✝ : HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)
N : Submonoid M
χ : MulChar (↥N) R
ψ : Mˣ →* Rˣ
hψ : ψ.domRestrict N.units = χ.toUnitHom.comp ↑N.unitsEquivUnitsType
x✝ : (↥N)ˣ
⊢ ((domRestrictHom N R) (ofUnitHom ψ)) ↑x✝ = χ ↑x✝

Tactic:
domRestrictHom_apply,

Goal state after:
M : Type u_1
R : Type u_2
inst✝³ : CommMonoid M
inst✝² : CommRing R
inst✝¹ : Finite M
inst✝ : HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)
N : Submonoid M
χ : MulChar (↥N) R
ψ : Mˣ →* Rˣ
hψ : ψ.domRestrict N.units = χ.toUnitHom.comp ↑N.unitsEquivUnitsType
x✝ : (↥N)ˣ
⊢ (domRestrict N (ofUnitHom ψ)) ↑x✝ = χ ↑x✝
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: s : Finset ℕ
m : ℕ
hm : m ≠ 0
hp : m.primeFactors ⊆ s
⊢ m ∈ factoredNumbers s

Tactic:
rw [mem_factoredNumbers]

Goal state after:
s : Finset ℕ
m : ℕ
hm : m ≠ 0
hp : m.primeFactors ⊆ s
⊢ m ≠ 0 ∧ ∀ p ∈ m.primeFactorsList, p ∈ s
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: n : ℕ
⊢ n.smoothNumbers = factoredNumbers n.primesBelow

Tactic:
smoothNumbers_eq_factoredNumbers

Goal state after:
n : ℕ
⊢ factoredNumbers (Finset.range n) = factoredNumbers n.primesBelow
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: m₁ m₂ n : ℕ
hm1 : m₁ ∈ n.smoothNumbers
hm2 : m₂ ∈ n.smoothNumbers
⊢ m₁ * m₂ ∈ n.smoothNumbers

Tactic:
smoothNumbers_eq_factoredNumbers

Goal state after:
m₁ m₂ n : ℕ
hm1 : m₁ ∈ factoredNumbers (Finset.range n)
hm2 : m₂ ∈ factoredNumbers (Finset.range n)
⊢ m₁ * m₂ ∈ factoredNumbers (Finset.range n)
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: N k : ℕ
⊢ #({n ∈ Finset.range (N + 1) | n ∈ k.smoothNumbers} ∪ {n ∈ Finset.range (N + 1) | n ≠ 0 ∧ n ∉ k.smoothNumbers}) = N

Tactic:
Finset.filter_union_right

Goal state after:
N k : ℕ
⊢ #({x ∈ Finset.range (N + 1) | x ∈ k.smoothNumbers ∨ x ≠ 0 ∧ x ∉ k.smoothNumbers}) = N
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: case inl
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
this : Dioph {v | v &2 = 0 ∧ v &0 = 0 ∨ v &0 * v &2 ≤ v &1 ∧ v &1 < (v &0 + 1) * v &2}
z x : ℕ
⊢ 0 = 0 ∧ z = 0 ∨ z * 0 ≤ x ∧ x < (z + 1) * 0 ↔ x / 0 = z

Tactic:
simp [eq_comm]

Goal state after:
Module: Mathlib.NumberTheory.EulerProduct.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : ∀ {p : ℕ}, Nat.Prime p → Summable fun n ↦ ‖f (p ^ n)‖
p : ℕ
s : Finset ℕ
hp : p ∉ s
ih : (Summable fun m ↦ ‖f ↑m‖) ∧ HasSum (fun m ↦ f ↑m) (∏ p ∈ s with Nat.Prime p, ∑' (n : ℕ), f (p ^ n))
hpp : Nat.Prime p
hp' : p ∉ {p ∈ s | Nat.Prime p}
x : ℕ × ↑(factoredNumbers s)
| f ↑((equivProdNatFactoredNumbers hpp hp) x)

Tactic:
rw [equivProdNatFactoredNumbers_apply', factoredNumbers.map_prime_pow_mul hmul hpp hp]

Goal state after:
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : ∀ {p : ℕ}, Nat.Prime p → Summable fun n ↦ ‖f (p ^ n)‖
p : ℕ
s : Finset ℕ
hp : p ∉ s
ih : (Summable fun m ↦ ‖f ↑m‖) ∧ HasSum (fun m ↦ f ↑m) (∏ p ∈ s with Nat.Prime p, ∑' (n : ℕ), f (p ^ n))
hpp : Nat.Prime p
hp' : p ∉ {p ∈ s | Nat.Prime p}
x : ℕ × ↑(factoredNumbers s)
| f (p ^ x.1) * f ↑x.2
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
⊢ 0 < u - ⌊ξ⌋ * v ∧ u - ⌊ξ⌋ * v < v

Tactic:
by
  obtain ⟨hcop, _, h⟩ := h
  obtain ⟨hv₀, hv₀'⟩ := aux₀ (zero_lt_two.trans_le hv)
  have hv₁ : 0 < 2 * v - 1 := by linarith only [hv]
  rw [← one_div, lt_div_iff₀ (mul_pos hv₀ hv₀'), ← abs_of_pos (mul_pos hv₀ hv₀'), ← abs_mul,
    sub_mul, ← mul_assoc, ← mul_assoc, div_mul_cancel₀ _ hv₀.ne', abs_sub_comm, abs_lt,
    lt_sub_iff_add_lt, sub_lt_iff_lt_add, mul_assoc] at h
  have hu₀ : 0 ≤ u - ⌊ξ⌋ * v := by
    refine (mul_nonneg_iff_of_pos_right hv₁).mp ?_
    rw [← sub_one_lt_iff, zero_sub]
    replace h := h.1
    rw [← lt_sub_iff_add_lt, ← mul_assoc, ← sub_mul] at h
    exact mod_cast
      h.trans_le
        ((mul_le_mul_iff_left₀ <| hv₀').mpr <|
          (sub_le_sub_iff_left (u : ℝ)).mpr ((mul_le_mul_iff_left₀ hv₀).mpr (floor_le ξ)))
  have hu₁ : u - ⌊ξ⌋ * v ≤ v := by
    refine _root_.le_of_mul_le_mul_right (le_of_lt_add_one ?_) hv₁
    replace h := h.2
    rw [← sub_lt_iff_lt_add, ← mul_assoc, ← sub_mul, ← add_lt_add_iff_right (v * (2 * v - 1) : ℝ),
      add_comm (1 : ℝ)] at h
    have :=
      flip mul_lt_mul_of_pos_right hv₀' <| (sub_lt_sub_iff_left (u : ℝ)).mpr <|
          flip mul_lt_mul_of_pos_right hv₀ <| sub_right_lt_of_lt_add <| lt_floor_add_one ξ
    rw [sub_mul ξ, one_mul, ← sub_add, add_mul] at this
    exact mod_cast this.trans h
  have huv_cop : IsCoprime (u - ⌊ξ⌋ * v) v := by
    rwa [sub_eq_add_neg, ← neg_mul, IsCoprime.add_mul_right_left_iff]
  refine ⟨lt_of_le_of_ne' hu₀ fun hf => ?_, lt_of_le_of_ne hu₁ fun hf => ?_⟩ <;>
    · rw [hf] at huv_cop
      simp only [isCoprime_zero_left, isCoprime_self, isUnit_iff] at huv_cop
      rcases huv_cop with huv_cop | huv_cop <;> linarith only [hv, huv_cop]

Goal state after:
Module: Mathlib.NumberTheory.EulerProduct.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hsum : Summable f
hf₀ : f 0 = 0
ε : ℝ
εpos : 0 < ε
N₀ N : ℕ
| N ≥ N₀ → ‖∑' (m : ℕ), f m - ∑' (m : ↑N.smoothNumbers), f ↑m‖ < ε

Tactic:
smoothNumbers_eq_factoredNumbers

Goal state after:
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hsum : Summable f
hf₀ : f 0 = 0
ε : ℝ
εpos : 0 < ε
N₀ N : ℕ
| N ≥ N₀ → ‖∑' (m : ℕ), f m - ∑' (m : ↑(factoredNumbers (range N))), f ↑m‖ < ε
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / |r i| ^ s.re
⊢ HasSum (fun i ↦ (s + 1).Gammaℝ * a i * ↑(SignType.sign (r i)) / ↑|r i| ^ s) (mellin F ((s + 1) / 2))

Tactic:
have hs₁ : s ≠ 0 := fun h ↦ lt_irrefl _ (zero_re ▸ h ▸ hs)

Goal state after:
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / |r i| ^ s.re
hs₁ : s ≠ 0
⊢ HasSum (fun i ↦ (s + 1).Gammaℝ * a i * ↑(SignType.sign (r i)) / ↑|r i| ^ s) (mellin F ((s + 1) / 2))
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ if r i = 0 then 0 else a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / |r i| ^ s.re
hs₁ : s ≠ 0
hs₂ : 0 < (s + 1).re
hs₃ : s + 1 ≠ 0
this :
  ∀ (i : ι) (t : ℝ),
    a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t)) = if r i = 0 then 0 else a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))
⊢ Summable fun i ↦ ‖a i * ↑(r i)‖ / |r i| ^ (s + 1).re

Tactic:
convert! h_sum using 2 with i

Goal state after:
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ if r i = 0 then 0 else a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / |r i| ^ s.re
hs₁ : s ≠ 0
hs₂ : 0 < (s + 1).re
hs₃ : s + 1 ≠ 0
this :
  ∀ (i : ι) (t : ℝ),
    a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t)) = if r i = 0 then 0 else a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))
i : ι
⊢ ‖a i * ↑(r i)‖ / |r i| ^ (s + 1).re = ‖a i‖ / |r i| ^ s.re
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : UnitAddCircle
⊢ hurwitzEvenFEPair (-a) = hurwitzEvenFEPair a

Tactic:
unfold hurwitzEvenFEPair
  congr 1 <;> simp [Function.comp_def]

Goal state after:
Module: Mathlib.NumberTheory.LSeries.Dirichlet

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
n✝ : ℕ
χ : DirichletCharacter R n✝
f g : ℕ → R
n : ℕ
p : ℕ × ℕ
hp : p ∈ n.divisorsAntidiagonal
⊢ χ ↑p.1 * f p.1 * (χ ↑p.2 * g p.2) = χ ↑n * (f p.1 * g p.2)

Tactic:
(mem_divisorsAntidiagonal.mp hp).1.symm,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
n✝ : ℕ
χ : DirichletCharacter R n✝
f g : ℕ → R
n : ℕ
p : ℕ × ℕ
hp : p ∈ n.divisorsAntidiagonal
⊢ χ ↑p.1 * f p.1 * (χ ↑p.2 * g p.2) = χ ↑(p.1 * p.2) * (f p.1 * g p.2)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : UnitAddCircle
n : ℕ
this : -2 * (↑n + 1) ≠ 0
⊢ Function.update (fun s ↦ completedHurwitzZetaEven a s / s.Gammaℝ) 0 (if a = 0 then -1 / 2 else 0) (-2 * (↑n + 1)) = 0

Tactic:
Function.update_of_ne this,

Goal state after:
a : UnitAddCircle
n : ℕ
this : -2 * (↑n + 1) ≠ 0
⊢ completedHurwitzZetaEven a (-2 * (↑n + 1)) / (-2 * (↑n + 1)).Gammaℝ = 0
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: n : ℕ
tfae_1_to_2 : FermatLastTheoremWith ℕ n → FermatLastTheoremWith ℤ n
tfae_2_to_3 : FermatLastTheoremWith ℤ n → FermatLastTheoremWith ℚ n
⊢ [FermatLastTheoremWith ℕ n, FermatLastTheoremWith ℤ n, FermatLastTheoremWith ℚ n].TFAE

Tactic:
tfae_have 3 → 1
  | h, a, b, c => mod_cast h a b c

Goal state after:
n : ℕ
tfae_1_to_2 : FermatLastTheoremWith ℕ n → FermatLastTheoremWith ℤ n
tfae_2_to_3 : FermatLastTheoremWith ℤ n → FermatLastTheoremWith ℚ n
tfae_3_to_1 : FermatLastTheoremWith ℚ n → FermatLastTheoremWith ℕ n
⊢ [FermatLastTheoremWith ℕ n, FermatLastTheoremWith ℤ n, FermatLastTheoremWith ℚ n].TFAE
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : UnitAddCircle
n : ℕ
this : -2 * (↑n + 1) ≠ 0
⊢ Function.update (fun s ↦ completedCosZeta a s / s.Gammaℝ) 0 (-1 / 2) (-2 * (↑n + 1)) = 0

Tactic:
Function.update_of_ne this,

Goal state after:
a : UnitAddCircle
n : ℕ
this : -2 * (↑n + 1) ≠ 0
⊢ completedCosZeta a (-2 * (↑n + 1)) / (-2 * (↑n + 1)).Gammaℝ = 0
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : UnitAddCircle
n : ℕ
this : -2 * (↑n + 1) ≠ 0
⊢ -2 * (↑n + 1) = -(2 * ↑(n + 1))

Tactic:
rw [neg_mul, Nat.cast_add_one]

Goal state after:
Module: Mathlib.NumberTheory.FLT.Four

Goal state before:
pp: case inl.inl
a b c : ℤ
h : Fermat42 a b c
a0 b0 c0 : ℤ
hf : Minimal a0 b0 c0
hap : a0 % 2 = 0
hbp : b0 % 2 = 0
h1 : 2 ∣ ↑(a0.gcd b0)
⊢ False

Tactic:
Int.isCoprime_iff_gcd_eq_one.mp (coprime_of_minimal hf)

Goal state after:
case inl.inl
a b c : ℤ
h : Fermat42 a b c
a0 b0 c0 : ℤ
hf : Minimal a0 b0 c0
hap : a0 % 2 = 0
hbp : b0 % 2 = 0
h1 : 2 ∣ ↑1
⊢ False
Module: Mathlib.NumberTheory.FLT.Four

Goal state before:
pp: a b c : ℤ
h : Minimal a b c
ha2 : a % 2 = 1
hc : 0 < c
ht : PythagoreanTriple (a ^ 2) (b ^ 2) c
h2 : (a ^ 2).gcd (b ^ 2) = 1
ha22 : a ^ 2 % 2 = 1
m n : ℤ
ht1 : a ^ 2 = m ^ 2 - n ^ 2
ht2 : b ^ 2 = 2 * m * n
ht3 : c = m ^ 2 + n ^ 2
ht4 : m.gcd n = 1
ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
ht6 : 0 ≤ m
htt : PythagoreanTriple a n m
⊢ False

Tactic:
have h3 : Int.gcd a n = 1 := by
    apply Int.isCoprime_iff_gcd_eq_one.mp
    apply @IsCoprime.of_mul_left_left _ _ _ a
    rw [← sq, ht1, (by ring : m ^ 2 - n ^ 2 = m ^ 2 + -n * n)]
    exact (Int.isCoprime_iff_gcd_eq_one.mpr ht4).pow_left.add_mul_right_left (-n)

Goal state after:
a b c : ℤ
h : Minimal a b c
ha2 : a % 2 = 1
hc : 0 < c
ht : PythagoreanTriple (a ^ 2) (b ^ 2) c
h2 : (a ^ 2).gcd (b ^ 2) = 1
ha22 : a ^ 2 % 2 = 1
m n : ℤ
ht1 : a ^ 2 = m ^ 2 - n ^ 2
ht2 : b ^ 2 = 2 * m * n
ht3 : c = m ^ 2 + n ^ 2
ht4 : m.gcd n = 1
ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
ht6 : 0 ≤ m
htt : PythagoreanTriple a n m
h3 : a.gcd n = 1
⊢ False
Module: Mathlib.NumberTheory.FLT.Four

Goal state before:
pp: a b c : ℤ
h : Minimal a b c
ha2 : a % 2 = 1
hc : 0 < c
ht : PythagoreanTriple (a ^ 2) (b ^ 2) c
h2 : (a ^ 2).gcd (b ^ 2) = 1
ha22 : a ^ 2 % 2 = 1
m n : ℤ
ht1 : a ^ 2 = m ^ 2 - n ^ 2
ht2 : b ^ 2 = 2 * m * n
ht3 : c = m ^ 2 + n ^ 2
ht4 : m.gcd n = 1
ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
ht6 : 0 ≤ m
htt : PythagoreanTriple a n m
h3 : a.gcd n = 1
hb20 : b ^ 2 ≠ 0
h4 : 0 < m
r s : ℤ
left✝ : a = r ^ 2 - s ^ 2
htt2 : n = 2 * r * s
htt3 : m = r ^ 2 + s ^ 2
htt4 : r.gcd s = 1
htt5 : r % 2 = 0 ∧ s % 2 = 1 ∨ r % 2 = 1 ∧ s % 2 = 0
htt6 : 0 ≤ r
hcp : m.gcd (r * s) = 1
b' : ℤ
hb2' : b = 2 * b'
hs : b' ^ 2 = m * (r * s)
hrsz : r * s ≠ 0
h2b0 : b' ≠ 0
i : ℤ
hi' : ¬m = -i ^ 2
hi : m = i ^ 2
⊢ False

Tactic:
rw [mul_comm] at hs

Goal state after:
a b c : ℤ
h : Minimal a b c
ha2 : a % 2 = 1
hc : 0 < c
ht : PythagoreanTriple (a ^ 2) (b ^ 2) c
h2 : (a ^ 2).gcd (b ^ 2) = 1
ha22 : a ^ 2 % 2 = 1
m n : ℤ
ht1 : a ^ 2 = m ^ 2 - n ^ 2
ht2 : b ^ 2 = 2 * m * n
ht3 : c = m ^ 2 + n ^ 2
ht4 : m.gcd n = 1
ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
ht6 : 0 ≤ m
htt : PythagoreanTriple a n m
h3 : a.gcd n = 1
hb20 : b ^ 2 ≠ 0
h4 : 0 < m
r s : ℤ
left✝ : a = r ^ 2 - s ^ 2
htt2 : n = 2 * r * s
htt3 : m = r ^ 2 + s ^ 2
htt4 : r.gcd s = 1
htt5 : r % 2 = 0 ∧ s % 2 = 1 ∨ r % 2 = 1 ∧ s % 2 = 0
htt6 : 0 ≤ r
hcp : m.gcd (r * s) = 1
b' : ℤ
hb2' : b = 2 * b'
hs : b' ^ 2 = r * s * m
hrsz : r * s ≠ 0
h2b0 : b' ≠ 0
i : ℤ
hi' : ¬m = -i ^ 2
hi : m = i ^ 2
⊢ False
Module: Mathlib.RingTheory.Polynomial.Wronskian

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : R[X]
ha : a ≠ 0
hb : b ≠ 0
⊢ (a * derivative b).degree < a.degree + b.degree

Tactic:
case =>

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Wronskian

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : R[X]
ha : a ≠ 0
hb : b ≠ 0
⊢ (derivative a * b).degree < a.degree + b.degree

Tactic:
case =>

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Radical

Goal state before:
pp: k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
⊢ divRadical 0 ∣ derivative 0

Tactic:
case =>

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Radical

Goal state before:
pp: k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a : k[X]
ha : IsUnit a
⊢ divRadical a ∣ derivative a

Tactic:
case =>

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Radical

Goal state before:
pp: k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
p : k[X]
hp : Prime p
i : ℕ
⊢ divRadical (p ^ (i + 1)) ∣ derivative (p ^ (i + 1))

Tactic:
case =>

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Radical

Goal state before:
pp: k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
p : k[X]
i : ℕ
hp : Prime p
⊢ divRadical (p ^ i) ∣ derivative (p ^ i)

Tactic:
case =>

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Radical

Goal state before:
pp: k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
x y : k[X]
hpxy : IsRelPrime x y
hx : divRadical x ∣ derivative x
hy : divRadical y ∣ derivative y
⊢ divRadical (x * y) ∣ derivative (x * y)

Tactic:
case =>

Goal state after:
Module: Mathlib.NumberTheory.FLT.MasonStothers

Goal state before:
pp: case neg.refine_3
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hsum : a + b + c = 0
w : k[X] := a.wronskian b
wab : w = a.wronskian b
hbc : IsCoprime b c
hsum' : b + c + a = 0
hca : IsCoprime c a
wbc : w = b.wronskian c
wca : w = c.wronskian a
abc_dr_dvd_w : divRadical (a * b * c) ∣ w
hw : ¬w = 0
⊢ c.natDegree + 1 ≤ (radical (a * b * c)).natDegree

Tactic:
apply abc_subcall wab

Goal state after:
case neg.refine_3.ha
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hsum : a + b + c = 0
w : k[X] := ⋯
wab : w = a.wronskian b
hbc : IsCoprime b c
hsum' : b + c + a = 0
hca : IsCoprime c a
wbc : w = b.wronskian c
wca : w = c.wronskian a
abc_dr_dvd_w : divRadical (a * b * c) ∣ w
hw : ¬w = 0
⊢ a ≠ 0

case neg.refine_3.hb
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hsum : a + b + c = 0
w : k[X] := ⋯
wab : w = a.wronskian b
hbc : IsCoprime b c
hsum' : b + c + a = 0
hca : IsCoprime c a
wbc : w = b.wronskian c
wca : w = c.wronskian a
abc_dr_dvd_w : divRadical (a * b * c) ∣ w
hw : ¬w = 0
⊢ b ≠ 0

case neg.refine_3.hc
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hsum : a + b + c = 0
w : k[X] := ⋯
wab : w = a.wronskian b
hbc : IsCoprime b c
hsum' : b + c + a = 0
hca : IsCoprime c a
wbc : w = b.wronskian c
wca : w = c.wronskian a
abc_dr_dvd_w : divRadical (a * b * c) ∣ w
hw : ¬w = 0
⊢ c ≠ 0

case neg.refine_3.abc_dr_dvd_w
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hsum : a + b + c = 0
w : k[X] := ⋯
wab : w = a.wronskian b
hbc : IsCoprime b c
hsum' : b + c + a = 0
hca : IsCoprime c a
wbc : w = b.wronskian c
wca : w = c.wronskian a
abc_dr_dvd_w : divRadical (a * b * c) ∣ w
hw : ¬w = 0
⊢ divRadical (a * b * c) ∣ w

k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hsum : a + b + c = 0
w : k[X] := ⋯
wab : w = a.wronskian b
hbc : IsCoprime b c
hsum' : b + c + a = 0
hca : IsCoprime c a
wbc : w = b.wronskian c
wca : w = c.wronskian a
abc_dr_dvd_w : divRadical (a * b * c) ∣ w
hw : ¬w = 0
⊢ w ≠ 0
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hyo : y % 2 = 1
hzpos : 0 < z
⊢ h.IsPrimitiveClassified

Tactic:
by_cases h0 : x = 0

Goal state after:
case pos
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : x = 0
⊢ h.IsPrimitiveClassified

case neg
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
⊢ h.IsPrimitiveClassified
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case neg
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1}
q : ℚ := (circleEquivGen hQ).symm ⟨(v, w), hp⟩
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
⊢ h.IsPrimitiveClassified

Tactic:
let m := (q.den : ℤ)

Goal state after:
case neg
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1}
q : ℚ := (circleEquivGen hQ).symm ⟨(v, w), hp⟩
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
⊢ h.IsPrimitiveClassified
Module: Mathlib.Topology.Instances.Complex

Goal state before:
pp: K : Subfield ℂ
hc : IsClosed ↑K
⊢ range ofReal ⊆ ofReal '' closure (range Rat.cast)

Tactic:
rw [DenseRange.closure_range Rat.isDenseEmbedding_coe_real.dense]

Goal state after:
K : Subfield ℂ
hc : IsClosed ↑K
⊢ range ofReal ⊆ ofReal '' univ
Module: Mathlib.NumberTheory.FLT.Polynomial

Goal state before:
pp: case inr
k : Type u_1
inst✝ : Field k
p q r : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
chp : ↑p ≠ 0
chq : ↑q ≠ 0
chr : ↑r ≠ 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
u v w : k
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0
hbc : IsCoprime b c
hca : IsCoprime c a
hCu : C u ≠ 0
hCv : C v ≠ 0
hCw : C w ≠ 0
hap : a ^ p ≠ 0
hbq : b ^ q ≠ 0
hcr : c ^ r ≠ 0
habp : IsCoprime (C u * a ^ p) (C v * b ^ q)
hbcp : IsCoprime (C v * b ^ q) (C w * c ^ r)
hcap : IsCoprime (C w * c ^ r) (C u * a ^ p)
habcp : IsCoprime (C u * a ^ p * (C v * b ^ q)) (C w * c ^ r)
dr0 : C u * derivative (a ^ p) = 0 ∧ C v * derivative (b ^ q) = 0 ∧ C w * derivative (c ^ r) = 0
⊢ derivative a = 0 ∧ derivative b = 0 ∧ derivative c = 0

Tactic:
mul_eq_zero_iff_left (C_ne_zero.mpr hu),

Goal state after:
case inr
k : Type u_1
inst✝ : Field k
p q r : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
chp : ↑p ≠ 0
chq : ↑q ≠ 0
chr : ↑r ≠ 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
u v w : k
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0
hbc : IsCoprime b c
hca : IsCoprime c a
hCu : C u ≠ 0
hCv : C v ≠ 0
hCw : C w ≠ 0
hap : a ^ p ≠ 0
hbq : b ^ q ≠ 0
hcr : c ^ r ≠ 0
habp : IsCoprime (C u * a ^ p) (C v * b ^ q)
hbcp : IsCoprime (C v * b ^ q) (C w * c ^ r)
hcap : IsCoprime (C w * c ^ r) (C u * a ^ p)
habcp : IsCoprime (C u * a ^ p * (C v * b ^ q)) (C w * c ^ r)
dr0 : derivative (a ^ p) = 0 ∧ C v * derivative (b ^ q) = 0 ∧ C w * derivative (c ^ r) = 0
⊢ derivative a = 0 ∧ derivative b = 0 ∧ derivative c = 0