mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: case pos
a : ℝ
ha : 0 ≤ a
h : a = 0
this : (fun t ↦ F_nat 0 0 t - 1) =O[atTop] fun t ↦ rexp (-π * t) / (1 - rexp (-π * t))
⊢ (fun t ↦ rexp (-π * t) / (1 - rexp (-π * t))) =O[atTop] fun t ↦ rexp (-π * t)

Tactic:
simpa using! (isBigO_refl (fun t ↦ rexp (-π * t)) _).mul isBigO_one_aux

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx : 0 < x
⊢ ContinuousAt (fun x ↦ (P.ε * ↑(x ^ (-P.k))) • P.g₀) x

Tactic:
have : x ≠ 0 ∨ 0 ≤ -P.k := Or.inl hx.ne'

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx : 0 < x
this : x ≠ 0 ∨ 0 ≤ -P.k
⊢ ContinuousAt (fun x ↦ (P.ε * ↑(x ^ (-P.k))) • P.g₀) x
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
⊢ (Summable fun x ↦ jacobiTheta₂_term_fderiv x z τ) ↔ 0 < τ.im

Tactic:
constructor

Goal state after:
case mp
z τ : ℂ
⊢ (Summable fun x ↦ jacobiTheta₂_term_fderiv x z τ) → 0 < τ.im

case mpr
z τ : ℂ
⊢ 0 < τ.im → Summable fun x ↦ jacobiTheta₂_term_fderiv x z τ
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
⊢ (Summable fun x ↦ jacobiTheta₂'_term x z τ) ↔ 0 < τ.im

Tactic:
constructor

Goal state after:
case mp
z τ : ℂ
⊢ (Summable fun x ↦ jacobiTheta₂'_term x z τ) → 0 < τ.im

case mpr
z τ : ℂ
⊢ 0 < τ.im → Summable fun x ↦ jacobiTheta₂'_term x z τ
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a t : ℝ
ht : 0 < t
this : (a : Prop) → Decidable a
⊢ HasSum (fun n ↦ if ↑n + a = 0 then 0 else rexp (-π * (↑n + a) ^ 2 * t))
    (evenKernel (↑a) t - if ∃ n, n • 1 = a then 1 else 0)

Tactic:
zsmul_one

Goal state after:
a t : ℝ
ht : 0 < t
this : (a : Prop) → Decidable a
⊢ HasSum (fun n ↦ if ↑n + a = 0 then 0 else rexp (-π * (↑n + a) ^ 2 * t))
    (evenKernel (↑a) t - if ∃ n, ↑n = a then 1 else 0)
Module: Mathlib.NumberTheory.SumPrimeReciprocals

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
f : ℕ → M
⊢ (fun n ↦ if Nat.Prime n then f n else 1) = {n | Nat.Prime n}.mulIndicator f

Tactic:
ext

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
f : ℕ → M
x✝ : ℕ
⊢ (if Nat.Prime x✝ then f x✝ else 1) = {n | Nat.Prime n}.mulIndicator f x✝
Module: Mathlib.NumberTheory.SumPrimeReciprocals

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
inst✝ : TopologicalSpace M
f : ℕ → M
⊢ ∏' (p : Primes), f ↑p = ∏' (n : ℕ), if Prime n then f n else 1

Tactic:
rw [ite_prime_eq_mulIndicator]; exact tprod_subtype {n | n.Prime} f

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

Goal state before:
pp: ⊢ (fun n ↦ 1 n) = δ

Tactic:
ext

Goal state after:
x✝ : ℕ
⊢ 1 x✝ = δ x✝
Module: Mathlib.NumberTheory.LSeries.Dirichlet

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
χ : DirichletCharacter R 1
⊢ (fun x ↦ χ ↑x) = 1

Tactic:
ext

Goal state after:
R : Type u_1
inst✝ : CommMonoidWithZero R
χ : DirichletCharacter R 1
x✝ : ℕ
⊢ χ ↑x✝ = 1 x✝
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: Λ : ℂ → ℂ
hf : ∀ (s : ℂ), s ≠ 0 → s ≠ 1 → DifferentiableAt ℂ Λ s
L : ℂ
h_lim : Tendsto (fun s ↦ s * Λ s) (𝓝[≠] 0) (𝓝 L)
s : ℂ
hs' : s ≠ 1
claim : ∀ (t : ℂ), t ≠ 0 → t ≠ 1 → DifferentiableAt ℂ (fun u ↦ Λ u / u.Gammaℝ) t
⊢ Tendsto (fun s ↦ Λ s / s.Gammaℝ) (𝓝[≠] 0) (𝓝 (L / 2))

Tactic:
refine Tendsto.congr' ?_ (h_lim.div Gammaℝ_residue_zero two_ne_zero)

Goal state after:
Λ : ℂ → ℂ
hf : ∀ (s : ℂ), s ≠ 0 → s ≠ 1 → DifferentiableAt ℂ Λ s
L : ℂ
h_lim : Tendsto (fun s ↦ s * Λ s) (𝓝[≠] 0) (𝓝 L)
s : ℂ
hs' : s ≠ 1
claim : ∀ (t : ℂ), t ≠ 0 → t ≠ 1 → DifferentiableAt ℂ (fun u ↦ Λ u / u.Gammaℝ) t
⊢ ((fun s ↦ s * Λ s) / fun s ↦ s * s.Gammaℝ) =ᶠ[𝓝[≠] 0] fun s ↦ Λ s / s.Gammaℝ
Module: Mathlib.NumberTheory.FLT.Four

Goal state before:
pp: a b c k : ℤ
hk0 : k ≠ 0
⊢ a ≠ 0 ∧ b ≠ 0 ∧ a ^ 4 + b ^ 4 = c ^ 2 ↔ k * a ≠ 0 ∧ k * b ≠ 0 ∧ (k * a) ^ 4 + (k * b) ^ 4 = (k ^ 2 * c) ^ 2

Tactic:
constructor

Goal state after:
case mp
a b c k : ℤ
hk0 : k ≠ 0
⊢ a ≠ 0 ∧ b ≠ 0 ∧ a ^ 4 + b ^ 4 = c ^ 2 → k * a ≠ 0 ∧ k * b ≠ 0 ∧ (k * a) ^ 4 + (k * b) ^ 4 = (k ^ 2 * c) ^ 2

case mpr
a b c k : ℤ
hk0 : k ≠ 0
⊢ k * a ≠ 0 ∧ k * b ≠ 0 ∧ (k * a) ^ 4 + (k * b) ^ 4 = (k ^ 2 * c) ^ 2 → a ≠ 0 ∧ b ≠ 0 ∧ a ^ 4 + b ^ 4 = c ^ 2
Module: Mathlib.NumberTheory.FLT.Four

Goal state before:
pp: case mpr
a b c k : ℤ
hk0 : k ≠ 0
f42 : k * a ≠ 0 ∧ k * b ≠ 0 ∧ (k * a) ^ 4 + (k * b) ^ 4 = (k ^ 2 * c) ^ 2
⊢ a ≠ 0 ∧ b ≠ 0 ∧ a ^ 4 + b ^ 4 = c ^ 2

Tactic:
constructor

Goal state after:
case mpr.left
a b c k : ℤ
hk0 : k ≠ 0
f42 : k * a ≠ 0 ∧ k * b ≠ 0 ∧ (k * a) ^ 4 + (k * b) ^ 4 = (k ^ 2 * c) ^ 2
⊢ a ≠ 0

case mpr.right
a b c k : ℤ
hk0 : k ≠ 0
f42 : k * a ≠ 0 ∧ k * b ≠ 0 ∧ (k * a) ^ 4 + (k * b) ^ 4 = (k ^ 2 * c) ^ 2
⊢ b ≠ 0 ∧ a ^ 4 + b ^ 4 = c ^ 2
Module: Mathlib.NumberTheory.FLT.Four

Goal state before:
pp: case mpr.right
a b c k : ℤ
hk0 : k ≠ 0
f42 : k * a ≠ 0 ∧ k * b ≠ 0 ∧ (k * a) ^ 4 + (k * b) ^ 4 = (k ^ 2 * c) ^ 2
⊢ b ≠ 0 ∧ a ^ 4 + b ^ 4 = c ^ 2

Tactic:
constructor

Goal state after:
case mpr.right.left
a b c k : ℤ
hk0 : k ≠ 0
f42 : k * a ≠ 0 ∧ k * b ≠ 0 ∧ (k * a) ^ 4 + (k * b) ^ 4 = (k ^ 2 * c) ^ 2
⊢ b ≠ 0

case mpr.right.right
a b c k : ℤ
hk0 : k ≠ 0
f42 : k * a ≠ 0 ∧ k * b ≠ 0 ∧ (k * a) ^ 4 + (k * b) ^ 4 = (k ^ 2 * c) ^ 2
⊢ a ^ 4 + b ^ 4 = c ^ 2
Module: Mathlib.NumberTheory.FLT.Four

Goal state before:
pp: a b c : ℤ
h2 : ∀ (a1 b1 c1 : ℤ), Fermat42 a1 b1 c1 → c.natAbs ≤ c1.natAbs
ha : a ≠ 0
hb : b ≠ 0
heq : a ^ 4 + b ^ 4 = c ^ 2
⊢ Minimal a b (-c)

Tactic:
constructor

Goal state after:
case left
a b c : ℤ
h2 : ∀ (a1 b1 c1 : ℤ), Fermat42 a1 b1 c1 → c.natAbs ≤ c1.natAbs
ha : a ≠ 0
hb : b ≠ 0
heq : a ^ 4 + b ^ 4 = c ^ 2
⊢ Fermat42 a b (-c)

case right
a b c : ℤ
h2 : ∀ (a1 b1 c1 : ℤ), Fermat42 a1 b1 c1 → c.natAbs ≤ c1.natAbs
ha : a ≠ 0
hb : b ≠ 0
heq : a ^ 4 + b ^ 4 = c ^ 2
⊢ ∀ (a1 b1 c1 : ℤ), Fermat42 a1 b1 c1 → (-c).natAbs ≤ c1.natAbs
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
⊢ y.gcd z = 1

Tactic:
by
  by_contra H
  obtain ⟨p, hp, hpy, hpz⟩ := Nat.Prime.not_coprime_iff_dvd.mp H
  apply hp.not_dvd_one
  rw [← hc]
  apply Nat.dvd_gcd (Int.Prime.dvd_natAbs_of_coe_dvd_sq hp _ _) hpy
  rw [sq, eq_sub_of_add_eq h]
  rw [← Int.natCast_dvd] at hpy hpz
  exact dvd_sub (hpz.mul_right _) (hpy.mul_right _)

Goal state after:
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: K : Type u_1
inst✝ : Field K
hk : ∀ (x : K), 1 + x ^ 2 ≠ 0
x✝ : { p // p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1 }
x y : K
hy : (x, y).2 ≠ -1
hxy : x ^ 2 + y ^ 2 = 1
h2 : y + 1 ≠ 0
h3 : (y + 1) ^ 2 + x ^ 2 = 2 * (y + 1)
h4 : 2 ≠ 0
⊢ 2 * (x / (y + 1)) / (1 + (x / (y + 1)) ^ 2) = x ∧ (1 - (x / (y + 1)) ^ 2) / (1 + (x / (y + 1)) ^ 2) = y

Tactic:
constructor

Goal state after:
case left
K : Type u_1
inst✝ : Field K
hk : ∀ (x : K), 1 + x ^ 2 ≠ 0
x✝ : { p // p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1 }
x y : K
hy : (x, y).2 ≠ -1
hxy : x ^ 2 + y ^ 2 = 1
h2 : y + 1 ≠ 0
h3 : (y + 1) ^ 2 + x ^ 2 = 2 * (y + 1)
h4 : 2 ≠ 0
⊢ 2 * (x / (y + 1)) / (1 + (x / (y + 1)) ^ 2) = x

case right
K : Type u_1
inst✝ : Field K
hk : ∀ (x : K), 1 + x ^ 2 ≠ 0
x✝ : { p // p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1 }
x y : K
hy : (x, y).2 ≠ -1
hxy : x ^ 2 + y ^ 2 = 1
h2 : y + 1 ≠ 0
h3 : (y + 1) ^ 2 + x ^ 2 = 2 * (y + 1)
h4 : 2 ≠ 0
⊢ (1 - (x / (y + 1)) ^ 2) / (1 + (x / (y + 1)) ^ 2) = y
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 ∧ (derivative a * b).degree < a.degree + b.degree

Tactic:
constructor

Goal state after:
case left
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

case right
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
Module: Mathlib.RingTheory.Polynomial.Wronskian

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
a b : R[X]
hc : IsCoprime a b
hw : a * derivative b = derivative a * b
⊢ derivative a = 0 ∧ derivative b = 0

Tactic:
constructor

Goal state after:
case left
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
a b : R[X]
hc : IsCoprime a b
hw : a * derivative b = derivative a * b
⊢ derivative a = 0

case right
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
a b : R[X]
hc : IsCoprime a b
hw : a * derivative b = derivative a * b
⊢ derivative b = 0
Module: Mathlib.RingTheory.Polynomial.Radical

Goal state before:
pp: case zero
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
p : k[X]
hp : Prime p
⊢ divRadical 1 ∣ derivative 1

Tactic:
derivative_one

Goal state after:
case zero
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
p : k[X]
hp : Prime p
⊢ divRadical 1 ∣ 0
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:
rw [← mul_dvd_mul_iff_left radical_ne_zero, radical_mul_divRadical,
        radical_pow_of_prime hp i.succ_ne_zero, derivative_pow_succ, ← mul_assoc]

Goal state after:
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
p : k[X]
hp : Prime p
i : ℕ
⊢ p ^ (i + 1) ∣ normalize p * (C (↑i + 1) * p ^ i) * derivative p
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a b : M
ha : Irreducible a
hb : b ≠ 0
⊢ a ∣ radical b ↔ a ∣ b

Tactic:
constructor

Goal state after:
case mp
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a b : M
ha : Irreducible a
hb : b ≠ 0
⊢ a ∣ radical b → a ∣ b

case mpr
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a b : M
ha : Irreducible a
hb : b ≠ 0
⊢ a ∣ b → a ∣ radical b
Module: Mathlib.NumberTheory.NumberField.FractionalIdeal

Goal state before:
pp: case e_6
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
e : Free.ChooseBasisIndex ℤ (𝓞 K) ≃ Free.ChooseBasisIndex ℤ ↥↑↑I
⊢ ⇑((basisOfFractionalIdeal K I).reindex e.symm) = Subtype.val ∘ ⇑((fractionalIdealBasis K ↑I).reindex e.symm)

Tactic:
ext

Goal state after:
case e_6
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
e : Free.ChooseBasisIndex ℤ (𝓞 K) ≃ Free.ChooseBasisIndex ℤ ↥↑↑I
x✝ : Free.ChooseBasisIndex ℤ (𝓞 K)
⊢ ((basisOfFractionalIdeal K I).reindex e.symm) x✝ = (Subtype.val ∘ ⇑((fractionalIdealBasis K ↑I).reindex e.symm)) x✝
Module: Mathlib.NumberTheory.NumberField.Norm

Goal state before:
pp: L : Type u_1
K : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : 𝓞 K
⊢ (algebraMap (𝓞 K) K) ((norm K) ((algebraMap (𝓞 K) (𝓞 L)) x)) = ↑(x ^ finrank K L)

Tactic:
RingOfIntegers.algebraMap_norm_algebraMap,

Goal state after:
L : Type u_1
K : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : 𝓞 K
⊢ (Algebra.norm K) ((algebraMap K L) ((algebraMap (𝓞 K) K) x)) = ↑(x ^ finrank K L)
Module: Mathlib.NumberTheory.NumberField.Norm

Goal state before:
pp: L : Type u_1
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
x : 𝓞 L
hint : IsIntegral ℤ (∏ σ ∈ univ.erase AlgEquiv.refl, σ ↑x)
⊢ (algebraMap (𝓞 K) (𝓞 L)) ((norm K) x) = x * ⟨∏ σ ∈ univ.erase AlgEquiv.refl, σ ↑x, hint⟩

Tactic:
ext

Goal state after:
L : Type u_1
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
x : 𝓞 L
hint : IsIntegral ℤ (∏ σ ∈ univ.erase AlgEquiv.refl, σ ↑x)
⊢ ↑((algebraMap (𝓞 K) (𝓞 L)) ((norm K) x)) = ↑(x * ⟨∏ σ ∈ univ.erase AlgEquiv.refl, σ ↑x, hint⟩)
Module: Mathlib.RingTheory.FractionalIdeal.Norm

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : IsDedekindDomain R
inst✝⁵ : Free ℤ R
inst✝⁴ : Module.Finite ℤ R
K : Type u_2
inst✝³ : CommRing K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDomain K
I : FractionalIdeal R⁰ K
h : ↑(Ideal.absNorm I.num) / ↑|(Algebra.norm ℤ) ↑I.den| = 0
⊢ I.num = ⊥

Tactic:
div_eq_zero_iff

Goal state after:
R : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : IsDedekindDomain R
inst✝⁵ : Free ℤ R
inst✝⁴ : Module.Finite ℤ R
K : Type u_2
inst✝³ : CommRing K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDomain K
I : FractionalIdeal R⁰ K
h : ↑(Ideal.absNorm I.num) = 0 ∨ ↑|(Algebra.norm ℤ) ↑I.den| = 0
⊢ I.num = ⊥
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: x y z : ℤ
⊢ PythagoreanTriple x y z ∧ x.gcd y = 1 ↔
    ∃ m n,
      (x = m ^ 2 - n ^ 2 ∧ y = 2 * m * n ∨ x = 2 * m * n ∧ y = m ^ 2 - n ^ 2) ∧
        (z = m ^ 2 + n ^ 2 ∨ z = -(m ^ 2 + n ^ 2)) ∧ m.gcd n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0)

Tactic:
constructor

Goal state after:
case mp
x y z : ℤ
⊢ PythagoreanTriple x y z ∧ x.gcd y = 1 →
    ∃ m n,
      (x = m ^ 2 - n ^ 2 ∧ y = 2 * m * n ∨ x = 2 * m * n ∧ y = m ^ 2 - n ^ 2) ∧
        (z = m ^ 2 + n ^ 2 ∨ z = -(m ^ 2 + n ^ 2)) ∧ m.gcd n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0)

case mpr
x y z : ℤ
⊢ (∃ m n,
      (x = m ^ 2 - n ^ 2 ∧ y = 2 * m * n ∨ x = 2 * m * n ∧ y = m ^ 2 - n ^ 2) ∧
        (z = m ^ 2 + n ^ 2 ∨ z = -(m ^ 2 + n ^ 2)) ∧ m.gcd n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0)) →
    PythagoreanTriple x y z ∧ x.gcd y = 1
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case mpr.inl.inl
m n : ℤ
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
⊢ (m ^ 2 - n ^ 2) * (m ^ 2 - n ^ 2) + 2 * m * n * (2 * m * n) = (m ^ 2 + n ^ 2) * (m ^ 2 + n ^ 2) ∧
    (m ^ 2 - n ^ 2).gcd (2 * m * n) = 1

Tactic:
constructor

Goal state after:
case mpr.inl.inl.left
m n : ℤ
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
⊢ (m ^ 2 - n ^ 2) * (m ^ 2 - n ^ 2) + 2 * m * n * (2 * m * n) = (m ^ 2 + n ^ 2) * (m ^ 2 + n ^ 2)

case mpr.inl.inl.right
m n : ℤ
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
⊢ (m ^ 2 - n ^ 2).gcd (2 * m * n) = 1
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case mpr.inl.inr
m n : ℤ
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
⊢ (m ^ 2 - n ^ 2) * (m ^ 2 - n ^ 2) + 2 * m * n * (2 * m * n) = -(m ^ 2 + n ^ 2) * -(m ^ 2 + n ^ 2) ∧
    (m ^ 2 - n ^ 2).gcd (2 * m * n) = 1

Tactic:
constructor

Goal state after:
case mpr.inl.inr.left
m n : ℤ
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
⊢ (m ^ 2 - n ^ 2) * (m ^ 2 - n ^ 2) + 2 * m * n * (2 * m * n) = -(m ^ 2 + n ^ 2) * -(m ^ 2 + n ^ 2)

case mpr.inl.inr.right
m n : ℤ
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
⊢ (m ^ 2 - n ^ 2).gcd (2 * m * n) = 1
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case mpr.inr.inl
m n : ℤ
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
⊢ 2 * m * n * (2 * m * n) + (m ^ 2 - n ^ 2) * (m ^ 2 - n ^ 2) = (m ^ 2 + n ^ 2) * (m ^ 2 + n ^ 2) ∧
    (2 * m * n).gcd (m ^ 2 - n ^ 2) = 1

Tactic:
constructor

Goal state after:
case mpr.inr.inl.left
m n : ℤ
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
⊢ 2 * m * n * (2 * m * n) + (m ^ 2 - n ^ 2) * (m ^ 2 - n ^ 2) = (m ^ 2 + n ^ 2) * (m ^ 2 + n ^ 2)

case mpr.inr.inl.right
m n : ℤ
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
⊢ (2 * m * n).gcd (m ^ 2 - n ^ 2) = 1
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case mpr.inr.inr
m n : ℤ
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
⊢ 2 * m * n * (2 * m * n) + (m ^ 2 - n ^ 2) * (m ^ 2 - n ^ 2) = -(m ^ 2 + n ^ 2) * -(m ^ 2 + n ^ 2) ∧
    (2 * m * n).gcd (m ^ 2 - n ^ 2) = 1

Tactic:
constructor

Goal state after:
case mpr.inr.inr.left
m n : ℤ
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
⊢ 2 * m * n * (2 * m * n) + (m ^ 2 - n ^ 2) * (m ^ 2 - n ^ 2) = -(m ^ 2 + n ^ 2) * -(m ^ 2 + n ^ 2)

case mpr.inr.inr.right
m n : ℤ
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
⊢ (2 * m * n).gcd (m ^ 2 - n ^ 2) = 1
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
⊢ mk φ = mk ψ ↔ φ = ψ ∨ ComplexEmbedding.conjugate φ = ψ

Tactic:
constructor

Goal state after:
case mp
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
⊢ mk φ = mk ψ → φ = ψ ∨ ComplexEmbedding.conjugate φ = ψ

case mpr
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
⊢ φ = ψ ∨ ComplexEmbedding.conjugate φ = ψ → mk φ = mk ψ
Module: Mathlib.RingTheory.FractionalIdeal.Norm

Goal state before:
pp: R : Type u_1
inst✝⁹ : CommRing R
inst✝⁸ : IsDedekindDomain R
inst✝⁷ : Free ℤ R
inst✝⁶ : Module.Finite ℤ R
K : Type u_2
inst✝⁵ : CommRing K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst✝¹ : Algebra ℚ K
inst✝ : Module.Finite ℚ K
x : K
this : IsDomain K
d : ↥R⁰
r : R
hr : (algebraMap R K) r = ↑d • x
⊢ d • ↑(spanSingleton R⁰ x) = Submodule.map (Algebra.linearMap R K) (Ideal.span {r})

Tactic:
ext

Goal state after:
R : Type u_1
inst✝⁹ : CommRing R
inst✝⁸ : IsDedekindDomain R
inst✝⁷ : Free ℤ R
inst✝⁶ : Module.Finite ℤ R
K : Type u_2
inst✝⁵ : CommRing K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst✝¹ : Algebra ℚ K
inst✝ : Module.Finite ℚ K
x : K
this : IsDomain K
d : ↥R⁰
r : R
hr : (algebraMap R K) r = ↑d • x
x✝ : K
⊢ x✝ ∈ d • ↑(spanSingleton R⁰ x) ↔ x✝ ∈ Submodule.map (Algebra.linearMap R K) (Ideal.span {r})
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case h.inl
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
h_pos : 0 < z
m n : ℤ
ht2 : z = m ^ 2 + n ^ 2 ∨ z = -(m ^ 2 + n ^ 2)
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : m < 0
h_odd : x = m ^ 2 - n ^ 2 ∧ y = 2 * m * n
⊢ y = 2 * -m * -n ∧ z = m ^ 2 + n ^ 2 ∧ (-m).gcd (-n) = 1 ∧ (-m % 2 = 0 ∧ -n % 2 = 1 ∨ -m % 2 = 1 ∧ -n % 2 = 0) ∧ 0 ≤ -m

Tactic:
constructor

Goal state after:
case h.inl.left
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
h_pos : 0 < z
m n : ℤ
ht2 : z = m ^ 2 + n ^ 2 ∨ z = -(m ^ 2 + n ^ 2)
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : m < 0
h_odd : x = m ^ 2 - n ^ 2 ∧ y = 2 * m * n
⊢ y = 2 * -m * -n

case h.inl.right
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
h_pos : 0 < z
m n : ℤ
ht2 : z = m ^ 2 + n ^ 2 ∨ z = -(m ^ 2 + n ^ 2)
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : m < 0
h_odd : x = m ^ 2 - n ^ 2 ∧ y = 2 * m * n
⊢ z = m ^ 2 + n ^ 2 ∧ (-m).gcd (-n) = 1 ∧ (-m % 2 = 0 ∧ -n % 2 = 1 ∨ -m % 2 = 1 ∧ -n % 2 = 0) ∧ 0 ≤ -m
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case h.inl.right.inl
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
h_pos✝ : 0 < z
m n : ℤ
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : m < 0
h_odd : x = m ^ 2 - n ^ 2 ∧ y = 2 * m * n
h_pos : z = m ^ 2 + n ^ 2
⊢ (-m).gcd (-n) = 1 ∧ (-m % 2 = 0 ∧ -n % 2 = 1 ∨ -m % 2 = 1 ∧ -n % 2 = 0) ∧ 0 ≤ -m

Tactic:
constructor

Goal state after:
case h.inl.right.inl.left
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
h_pos✝ : 0 < z
m n : ℤ
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : m < 0
h_odd : x = m ^ 2 - n ^ 2 ∧ y = 2 * m * n
h_pos : z = m ^ 2 + n ^ 2
⊢ (-m).gcd (-n) = 1

case h.inl.right.inl.right
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
h_pos✝ : 0 < z
m n : ℤ
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : m < 0
h_odd : x = m ^ 2 - n ^ 2 ∧ y = 2 * m * n
h_pos : z = m ^ 2 + n ^ 2
⊢ (-m % 2 = 0 ∧ -n % 2 = 1 ∨ -m % 2 = 1 ∧ -n % 2 = 0) ∧ 0 ≤ -m
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: case s.p
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
| fun φ ↦ mk φ = w

pp: case s.s
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
| Finset.univ

pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
⊢ DecidablePred ?m.24

Tactic:
ext

Goal state after:
case s.p
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
x✝ : K →+* ℂ
| mk x✝ = w

case s.s
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
| Finset.univ

K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
⊢ DecidablePred ?m.24
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: x y z : ℤ
⊢ PythagoreanTriple x y z ↔
    ∃ k m n,
      (x = k * (m ^ 2 - n ^ 2) ∧ y = k * (2 * m * n) ∨ x = k * (2 * m * n) ∧ y = k * (m ^ 2 - n ^ 2)) ∧
        (z = k * (m ^ 2 + n ^ 2) ∨ z = -k * (m ^ 2 + n ^ 2))

Tactic:
constructor

Goal state after:
case mp
x y z : ℤ
⊢ PythagoreanTriple x y z →
    ∃ k m n,
      (x = k * (m ^ 2 - n ^ 2) ∧ y = k * (2 * m * n) ∨ x = k * (2 * m * n) ∧ y = k * (m ^ 2 - n ^ 2)) ∧
        (z = k * (m ^ 2 + n ^ 2) ∨ z = -k * (m ^ 2 + n ^ 2))

case mpr
x y z : ℤ
⊢ (∃ k m n,
      (x = k * (m ^ 2 - n ^ 2) ∧ y = k * (2 * m * n) ∨ x = k * (2 * m * n) ∧ y = k * (m ^ 2 - n ^ 2)) ∧
        (z = k * (m ^ 2 + n ^ 2) ∨ z = -k * (m ^ 2 + n ^ 2))) →
    PythagoreanTriple x y z
Module: Mathlib.NumberTheory.NumberField.Units.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (𝓞 K)ˣ
h : ∀ (φ : K →+* ℂ), ‖φ ((algebraMap (𝓞 K) K) ↑x)‖ = 1
n : ℕ
hn : 0 < n
hx : (algebraMap (𝓞 K) K) ↑x ^ n = 1
⊢ x ^ n = 1

Tactic:
ext

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (𝓞 K)ˣ
h : ∀ (φ : K →+* ℂ), ‖φ ((algebraMap (𝓞 K) K) ↑x)‖ = 1
n : ℕ
hn : 0 < n
hx : (algebraMap (𝓞 K) K) ↑x ^ n = 1
⊢ ↑↑(x ^ n) = ↑↑1
Module: Mathlib.NumberTheory.NumberField.Units.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
φ : K →+* ℂ
⊢ Subgroup.map (Units.complexEmbedding φ) (torsion K) = rootsOfUnity (torsionOrder K) ℂ

Tactic:
apply Subgroup.eq_of_le_of_card_ge

Goal state after:
case hle
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
φ : K →+* ℂ
⊢ Subgroup.map (Units.complexEmbedding φ) (torsion K) ≤ rootsOfUnity (torsionOrder K) ℂ

case hcard
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
φ : K →+* ℂ
⊢ Nat.card ↥(rootsOfUnity (torsionOrder K) ℂ) ≤ Nat.card ↥(Subgroup.map (Units.complexEmbedding φ) (torsion K))
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: a b : InfinitePlace ℚ
⊢ a = b

Tactic:
ext

Goal state after:
a b : InfinitePlace ℚ
k✝ : ℚ
⊢ a k✝ = b k✝
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: ⊢ ComplexEmbedding.IsReal (castHom ℂ)

Tactic:
ext

Goal state after:
x✝ : ℚ
⊢ (star (castHom ℂ)) x✝ = (castHom ℂ) x✝
Module: Mathlib.NumberTheory.NumberField.EquivReindex

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ basisMatrix K =
    Algebra.embeddingsMatrixReindex ℚ ℂ (⇑(integralBasis K) ∘ ⇑(equivReindex K)) (RingHom.equivRatAlgHom K ℂ)

Tactic:
ext

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
i✝ j✝ : K →+* ℂ
⊢ basisMatrix K i✝ j✝ =
    Algebra.embeddingsMatrixReindex ℚ ℂ (⇑(integralBasis K) ∘ ⇑(equivReindex K)) (RingHom.equivRatAlgHom K ℂ) i✝ j✝
Module: Mathlib.NumberTheory.NumberField.EquivReindex

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ (basisMatrix K).map ⇑(starRingEnd ℂ) =
    (reindex (Equiv.refl (K →+* ℂ)) (Function.Involutive.toPerm ComplexEmbedding.conjugate ⋯)) (basisMatrix K)

Tactic:
ext

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
i✝ j✝ : K →+* ℂ
⊢ (basisMatrix K).map (⇑(starRingEnd ℂ)) i✝ j✝ =
    (reindex (Equiv.refl (K →+* ℂ)) (Function.Involutive.toPerm ComplexEmbedding.conjugate ⋯)) (basisMatrix K) i✝ j✝