mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.Cyclotomic.Discriminant

Goal state before:
pp: p k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ k} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ k)
hirr : Irreducible (cyclotomic (p ^ k) K)
heven : ¬Even (φ (p ^ k) / 2)
⊢ (-1) ^ (φ (p ^ k) / 2) * ↑p ^ (p ^ (k - 1) * ((p - 1) * k - 1)) = ↑↑(-1) * ↑p ^ (p ^ (k - 1) * ((p - 1) * k - 1))

Tactic:
by
      rw [(not_even_iff_odd.1 heven).neg_one_pow]; simp

Goal state after:
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ˣ)
H : Subgroup Mˣ
χ : MulChar M R
⊢ χ ∈ OrderDual.ofDual ((subgroupOrderIsoSubgroupMulChar M R) H) ↔ ∀ m ∈ H, χ ↑m = 1

Tactic:
rw [subgroupOrderIsoSubgroupMulChar, OrderIso.trans_apply, OrderIso.dual_apply,
    MulEquiv.coe_mapSubgroup, OrderDual.ofDual_toDual, Subgroup.mem_map_equiv]

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ˣ)
H : Subgroup Mˣ
χ : MulChar M R
⊢ mulEquivToUnitHom.symm.symm χ ∈ OrderDual.ofDual ((CommGroup.subgroupOrderIsoSubgroupMonoidHom Mˣ R) H) ↔
    ∀ m ∈ H, χ ↑m = 1
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
i j n : ℕ
ipos : 0 < i
hin : i ≤ n
h : xn a1 j ≡ xn a1 i [MOD xn a1 n]
j' : ℕ := j % (4 * n)
n4 : 0 < 4 * n
jl : j' < 4 * n
jj : j ≡ j' [MOD 4 * n]
⊢ ∀ (j q : ℕ), xn a1 (j + 4 * n * q) ≡ xn a1 j [MOD xn a1 n]

Tactic:
by
    intro j q; induction q with
    | zero => simp [ModEq.refl]
    | succ q IH =>
      rw [Nat.mul_succ, ← add_assoc, add_comm]
      exact (xn_modEq_x4n_add _ _ _).trans IH

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a k x✝¹ y✝ : ℕ
x✝ : ∃ (a1 : 1 < a), xn a1 k = x✝¹ ∧ yn a1 k = y✝
a1 : 1 < a
hx : xn a1 k = x✝¹
hy : yn a1 k = y✝
kpos : k > 0
x : ℕ := xn a1 k
y : ℕ := yn a1 k
m : ℕ := 2 * (k * y)
u : ℕ := xn a1 m
v : ℕ := yn a1 m
ky : k ≤ y
yv : y * y ∣ v
uco : u.Coprime (4 * y)
b : ℕ
ba : b ≡ a [MOD u]
bm1 : b ≡ 1 [MOD 4 * y]
m1 : 1 < m
vp : 0 < v
this✝ : xn a1 1 < u
this : a < u
⊢ a ≤ b

Tactic:
delta ModEq at ba

Goal state after:
a k x✝¹ y✝ : ℕ
x✝ : ∃ (a1 : 1 < a), xn a1 k = x✝¹ ∧ yn a1 k = y✝
a1 : 1 < a
hx : xn a1 k = x✝¹
hy : yn a1 k = y✝
kpos : k > 0
x : ℕ := xn a1 k
y : ℕ := yn a1 k
m : ℕ := 2 * (k * y)
u : ℕ := xn a1 m
v : ℕ := yn a1 m
ky : k ≤ y
yv : y * y ∣ v
uco : u.Coprime (4 * y)
b : ℕ
ba : b % u = a % u
bm1 : b ≡ 1 [MOD 4 * y]
m1 : 1 < m
vp : 0 < v
this✝ : xn a1 1 < u
this : a < u
⊢ a ≤ b
Module: Mathlib.NumberTheory.LSeries.Convergence

Goal state before:
pp: f : ℕ → ℂ
x : EReal
h : ∀ (y : ℝ), x < ↑y → LSeriesSummable f ↑y
⊢ abscissaOfAbsConv f ≤ x

Tactic:
cases x with
  | coe => exact abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable <| mod_cast h
  | top => exact le_top
  | bot =>
    refine le_of_eq <| sInf_eq_bot.mpr fun y hy ↦ ?_
    cases y with
    | bot => simp at hy
    | coe y => exact ⟨_, ⟨_, h _ <| EReal.bot_lt_coe _, rfl⟩, mod_cast sub_one_lt y⟩
    | top => exact ⟨_, ⟨_, h _ <| EReal.bot_lt_coe 0, rfl⟩, EReal.zero_lt_top⟩

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

Goal state before:
pp: case pos.right
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
⊢ HasSum (fun m ↦ f ↑m) (∏ x ∈ insert p ({p ∈ s | Nat.Prime p}), ∑' (n : ℕ), f (x ^ n))

Tactic:
have hp' : p ∉ {p ∈ s | p.Prime} := mt (mem_of_mem_filter p) hp
        rw [prod_insert hp', ← (equivProdNatFactoredNumbers hpp hp).hasSum_iff, Function.comp_def]
        conv =>
          enter [1, x]
          rw [equivProdNatFactoredNumbers_apply', factoredNumbers.map_prime_pow_mul hmul hpp hp]
        have : T3Space R := instT3Space -- speeds up the following
        apply (hsum hpp).of_norm.hasSum.mul ih.2
        -- `exact summable_mul_of_summable_norm (hsum hpp) ih.1` gives a time-out
        apply summable_mul_of_summable_norm (hsum hpp) ih.1

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: case mpr
m n k : ℕ
⊢ k = 0 ∧ m = 1 ∨
      0 < k ∧
        (n = 0 ∧ m = 0 ∨
          0 < n ∧
            ∃ w a t z,
              ∃ (a1 : 1 < a),
                xn a1 k ≡ yn a1 k * (a - n) + m [MOD t] ∧
                  2 * a * n = t + (n * n + 1) ∧
                    m < t ∧ n ≤ w ∧ k ≤ w ∧ a * a - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1) →
    n ^ k = m

Tactic:
· rintro (⟨rfl, rfl⟩ | ⟨hk0, ⟨rfl, rfl⟩ | ⟨hn0, w, a, t, z, a1, tm, ta, mt, nw, kw, zp⟩⟩)
    · exact _root_.pow_zero n
    · exact zero_pow hk0.ne'
    have hw0 : 0 < w := hn0.trans_le nw
    have hw1 : 1 < w + 1 := Nat.succ_lt_succ hw0
    rcases eq_pell hw1 zp with ⟨j, rfl, yj⟩
    have hj0 : 0 < j := by
      apply Nat.pos_of_ne_zero
      rintro rfl
      exact lt_irrefl 1 a1
    have wj : w ≤ j :=
      Nat.le_of_dvd hj0
        (modEq_zero_iff_dvd.1 <|
          (yn_modEq_a_sub_one hw1 j).symm.trans <| modEq_zero_iff_dvd.2 ⟨z, yj.symm⟩)
    have hnka : n ^ k < xn hw1 j := calc
      n ^ k ≤ n ^ j := Nat.pow_le_pow_right hn0 (le_trans kw wj)
      _ < (w + 1) ^ j := Nat.pow_lt_pow_left (Nat.lt_succ_of_le nw) hj0.ne'
      _ ≤ xn hw1 j := xn_ge_a_pow hw1 j
    have nt : (↑(n ^ k) : ℤ) < 2 * xn hw1 j * n - n * n - 1 :=
      eq_pow_of_pell_lem hn0.ne' hk0.ne' hnka
    have na : n ≤ xn hw1 j := (Nat.le_self_pow hk0.ne' _).trans hnka.le
    have te : (t : ℤ) = 2 * xn hw1 j * n - n * n - 1 := by
      rw [sub_sub, eq_sub_iff_add_eq]
      exact mod_cast ta.symm
    have : xn a1 k ≡ yn a1 k * (xn hw1 j - n) + n ^ k [MOD t] := by
      apply modEq_of_dvd
      rw [te, Nat.cast_add, Nat.cast_mul, Int.ofNat_sub na]
      exact x_sub_y_dvd_pow a1 n k
    have : n ^ k % t = m % t := (this.symm.trans tm).add_left_cancel' _
    rw [← te] at nt
    rwa [Nat.mod_eq_of_lt (Nat.cast_lt.1 nt), Nat.mod_eq_of_lt mt] at this

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: case refine_2
z τ : ℂ
h : Summable fun x ↦ jacobiTheta₂_term x z τ
⊢ 0 < τ.im

Tactic:
· by_contra! hτ
    rcases lt_or_eq_of_le hτ with hτ | hτ
    · -- easy case `im τ < 0`
      suffices Tendsto (fun n : ℕ ↦ ‖jacobiTheta₂_term ↑n z τ‖) atTop atTop by
        replace h := (h.comp_injective (fun a b ↦ Int.ofNat_inj.mp)).tendsto_atTop_zero.norm
        exact atTop_neBot.ne (disjoint_self.mp <| h.disjoint (disjoint_nhds_atTop _) this)
      simp only [norm_jacobiTheta₂_term, Int.cast_natCast]
      conv =>
        enter [1, n]
        rw [show -π * n ^ 2 * τ.im - 2 * π * n * z.im =
              n * (n * (-π * τ.im) - 2 * π * z.im) by ring]
      refine tendsto_exp_atTop.comp (tendsto_natCast_atTop_atTop.atTop_mul_atTop₀ ?_)
      exact tendsto_atTop_add_const_right _ _ (tendsto_natCast_atTop_atTop.atTop_mul_const
        (mul_pos_of_neg_of_neg (neg_lt_zero.mpr pi_pos) hτ))
    · -- case im τ = 0: 3-way split according to `im z`
      simp_rw [← summable_norm_iff (E := ℂ), norm_jacobiTheta₂_term, hτ, mul_zero, zero_sub] at h
      rcases lt_trichotomy (im z) 0 with hz | hz | hz
      · replace h := (h.comp_injective (fun a b ↦ Int.ofNat_inj.mp)).tendsto_atTop_zero
        simp_rw [Function.comp_def, Int.cast_natCast] at h
        refine atTop_neBot.ne (disjoint_self.mp <| h.disjoint (disjoint_nhds_atTop 0) ?_)
        refine tendsto_exp_atTop.comp ?_
        simp only [tendsto_neg_atTop_iff, mul_assoc]
        apply Filter.Tendsto.const_mul_atBot two_pos
        exact (tendsto_natCast_atTop_atTop.atTop_mul_const_of_neg hz).const_mul_atBot pi_pos
      · revert h
        simpa only [hz, mul_zero, neg_zero, Real.exp_zero, summable_const_iff] using one_ne_zero
      · have : ((-↑·) : ℕ → ℤ).Injective := fun _ _ ↦ by simp only [neg_inj, Nat.cast_inj, imp_self]
        replace h := (h.comp_injective this).tendsto_atTop_zero
        simp_rw [Function.comp_def, Int.cast_neg, Int.cast_natCast, mul_neg, neg_mul, neg_neg] at h
        refine atTop_neBot.ne (disjoint_self.mp <| h.disjoint (disjoint_nhds_atTop 0) ?_)
        exact tendsto_exp_atTop.comp ((tendsto_natCast_atTop_atTop.const_mul_atTop
          (mul_pos two_pos pi_pos)).atTop_mul_const hz)

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
r : ℝ
⊢ (fun x ↦ P.f x - P.f₀) =ᶠ[atTop] fun x ↦ P.f_modif x - 0

Tactic:
filter_upwards [eventually_gt_atTop 1] with x hx

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
r x : ℝ
hx : 1 < x
⊢ P.f x - P.f₀ = P.f_modif x - 0
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : UnitAddCircle
x : ℝ
hx : x ≤ 0
⊢ evenKernel a x = 0

Tactic:
induction a using QuotientAddGroup.induction_on with
  | H a' => simp [← ofReal_inj, evenKernel_def, jacobiTheta₂_undef _ (by simpa : (I * ↑x).im ≤ 0)]

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

Goal state before:
pp: a x : ℝ
⊢ ↑(oddKernel (↑a) x) =
    cexp (-↑π * ↑a ^ 2 * ↑x) *
      (jacobiTheta₂' (↑a * I * ↑x) (I * ↑x) / (2 * ↑π * I) + ↑a * jacobiTheta₂ (↑a * I * ↑x) (I * ↑x))

Tactic:
rw [oddKernel_def, jacobiTheta₂'', ← mul_assoc ↑a I x,
    (by ring : ↑π * I * ↑a ^ 2 * (I * ↑x) = I ^ 2 * ↑π * ↑a ^ 2 * x), I_sq, neg_one_mul]

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

Goal state before:
pp: s : ℂ
hs : 1 < s.re
⊢ L (fun n ↦ ↑(ζ n)) s = riemannZeta s

Tactic:
suffices ∑' n, term (fun n ↦ if n = 0 then 0 else 1) s n = ∑' n : ℕ, 1 / (n : ℂ) ^ s by
    simpa [LSeries, zeta_eq_tsum_one_div_nat_cpow hs]

Goal state after:
s : ℂ
hs : 1 < s.re
⊢ ∑' (n : ℕ), term (fun n ↦ if n = 0 then 0 else 1) s n = ∑' (n : ℕ), 1 / ↑n ^ s
Module: Mathlib.NumberTheory.LSeries.Dirichlet

Goal state before:
pp: s : ℂ
hs : 1 < s.re
⊢ LSeriesSummable (fun n ↦ ↑(Λ n)) s

Tactic:
have hf := LSeriesSummable_logMul_of_lt_re
    (show abscissaOfAbsConv 1 < s.re by rw [abscissaOfAbsConv_one]; exact_mod_cast hs)

Goal state after:
s : ℂ
hs : 1 < s.re
hf : LSeriesSummable (logMul 1) s
⊢ LSeriesSummable (fun n ↦ ↑(Λ n)) s
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: x y z : ℤ
⊢ PythagoreanTriple x y z ↔ PythagoreanTriple y x z

Tactic:
delta PythagoreanTriple
  rw [add_comm]

Goal state after:
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
H : ¬y.gcd z = 1
p : ℕ
hp : Nat.Prime p
hpy : p ∣ y.natAbs
hpz : p ∣ z.natAbs
⊢ ↑p ∣ z * z - y * y

Tactic:
← Int.natCast_dvd

Goal state after:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
H : ¬y.gcd z = 1
p : ℕ
hp : Nat.Prime p
hpy : ↑p ∣ y
hpz : ↑p ∣ z
⊢ ↑p ∣ z * z - y * y
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬(m ^ 2 - n ^ 2).gcd (m ^ 2 + n ^ 2) = 1
p : ℕ
hp : Nat.Prime p
hp1 : p ∣ (m ^ 2 - n ^ 2).natAbs
hp2 : p ∣ (m ^ 2 + n ^ 2).natAbs
⊢ False

Tactic:
← Int.natCast_dvd

Goal state after:
m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬(m ^ 2 - n ^ 2).gcd (m ^ 2 + n ^ 2) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ m ^ 2 + n ^ 2
⊢ False
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬(m ^ 2 - n ^ 2).gcd (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp1 : p ∣ (m ^ 2 - n ^ 2).natAbs
hp2 : p ∣ (2 * m * n).natAbs
⊢ False

Tactic:
← Int.natCast_dvd

Goal state after:
m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬(m ^ 2 - n ^ 2).gcd (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ 2 * m * n
⊢ False
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 : ℕ
⊢ p ^ (i + 1) ∣ p ^ i * normalize p

Tactic:
pow_succ,

Goal state after:
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
p : k[X]
hp : Prime p
i : ℕ
⊢ p ^ i * p ∣ p ^ i * normalize p
Module: Mathlib.NumberTheory.FLT.Four

Goal state before:
pp: a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
⊢ a ^ 4 + b ^ 4 ≠ c ^ 2

Tactic:
by
  intro h
  obtain ⟨a0, b0, c0, ⟨hf, h2, hp⟩⟩ :=
    Fermat42.exists_pos_odd_minimal (And.intro ha (And.intro hb h))
  apply Fermat42.not_minimal hf h2 hp

Goal state after:
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: m0 n0 : ℤ
hm : (m0 * 2 + 1) % 2 = 1
hn : (n0 * 2 + 1) % 2 = 1
h : (m0 * 2 + 1).gcd (n0 * 2 + 1) = 1
h1 : (m0 * 2 + 1) ^ 2 + (n0 * 2 + 1) ^ 2 = 2 * (2 * (m0 ^ 2 + n0 ^ 2 + m0 + n0) + 1)
h2 : (m0 * 2 + 1) ^ 2 - (n0 * 2 + 1) ^ 2 = 2 * (2 * (m0 ^ 2 - n0 ^ 2 + m0 - n0))
h3 : ((m0 * 2 + 1) ^ 2 - (n0 * 2 + 1) ^ 2) / 2 % 2 = 0
h20 : 2 ≠ 0
h4 : ¬(2 * (m0 ^ 2 - n0 ^ 2 + m0 - n0)).gcd (2 * (m0 ^ 2 + n0 ^ 2 + m0 + n0) + 1) = 1
p : ℕ
hp : Nat.Prime p
hp1 : p ∣ (2 * (m0 ^ 2 - n0 ^ 2 + m0 - n0)).natAbs
hp2 : p ∣ (2 * (m0 ^ 2 + n0 ^ 2 + m0 + n0) + 1).natAbs
⊢ p ∣ (m0 * 2 + 1).gcd (n0 * 2 + 1)

Tactic:
← Int.natCast_dvd

Goal state after:
m0 n0 : ℤ
hm : (m0 * 2 + 1) % 2 = 1
hn : (n0 * 2 + 1) % 2 = 1
h : (m0 * 2 + 1).gcd (n0 * 2 + 1) = 1
h1 : (m0 * 2 + 1) ^ 2 + (n0 * 2 + 1) ^ 2 = 2 * (2 * (m0 ^ 2 + n0 ^ 2 + m0 + n0) + 1)
h2 : (m0 * 2 + 1) ^ 2 - (n0 * 2 + 1) ^ 2 = 2 * (2 * (m0 ^ 2 - n0 ^ 2 + m0 - n0))
h3 : ((m0 * 2 + 1) ^ 2 - (n0 * 2 + 1) ^ 2) / 2 % 2 = 0
h20 : 2 ≠ 0
h4 : ¬(2 * (m0 ^ 2 - n0 ^ 2 + m0 - n0)).gcd (2 * (m0 ^ 2 + n0 ^ 2 + m0 + n0) + 1) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ 2 * (m0 ^ 2 - n0 ^ 2 + m0 - n0)
hp2 : ↑p ∣ 2 * (m0 ^ 2 + n0 ^ 2 + m0 + n0) + 1
⊢ p ∣ (m0 * 2 + 1).gcd (n0 * 2 + 1)
Module: Mathlib.NumberTheory.FLT.MasonStothers

Goal state before:
pp: case neg.refine_2
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
⊢ b.natDegree + 1 ≤ (radical (a * b * c)).natDegree

Tactic:
rw [← mul_rotate] at abc_dr_dvd_w ⊢
      apply abc_subcall wca <;> assumption

Goal state after:
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case h.inl.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 : 0 ≤ m
h_odd : x = m ^ 2 - n ^ 2 ∧ y = 2 * m * n
h_pos : 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) ∧ 0 ≤ m

Tactic:
apply And.intro h_pos (And.intro ht3 (And.intro ht4 hm))

Goal state after:
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
w : InfinitePlace K
⊢ ¬w.IsComplex ↔ w.IsReal

Tactic:
rw [isComplex_iff, isReal_iff, not_not]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.EquivReindex

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (K →+* ℂ)
⊢ (basisMatrix K).det ≠ 0

Tactic:
rw [basisMatrix_eq_embeddingsMatrixReindex, ← pow_ne_zero_iff two_ne_zero]
  convert!
    (map_ne_zero_iff _ (algebraMap ℚ ℂ).injective).mpr
      (Algebra.discr_not_zero_of_basis ℚ (integralBasis K))
  rw [← Algebra.discr_reindex ℚ (integralBasis K) (equivReindex K).symm]
  exact (Algebra.discr_eq_det_embeddingsMatrixReindex_pow_two ℚ ℂ
    (integralBasis K ∘ (equivReindex K)) (RingHom.equivRatAlgHom K ℂ)).symm

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis (K →+* ℂ) ℂ ((K →+* ℂ) → ℂ) := Pi.basisFun ℂ (K →+* ℂ)
e : (K →+* ℂ) ≃ Free.ChooseBasisIndex ℤ (𝓞 K) := Fintype.equivOfCardEq ⋯
M : Matrix (K →+* ℂ) (K →+* ℂ) ℂ := B.toMatrix fun i ↦ (canonicalEmbedding K) ((integralBasis K) (e i))
N : Matrix (K →+* ℂ) (K →+* ℂ) ℂ :=
  Algebra.embeddingsMatrixReindex ℚ ℂ (fun i ↦ (integralBasis K) (e i)) (RingHom.equivRatAlgHom K ℂ)
⊢ N.det ^ 2 = (algebraMap ℚ ℂ) (Algebra.discr ℚ ⇑(integralBasis K))

Tactic:
rw [← Algebra.discr_reindex ℚ (integralBasis K) e.symm]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis (K →+* ℂ) ℂ ((K →+* ℂ) → ℂ) := Pi.basisFun ℂ (K →+* ℂ)
e : (K →+* ℂ) ≃ Free.ChooseBasisIndex ℤ (𝓞 K) := Fintype.equivOfCardEq ⋯
M : Matrix (K →+* ℂ) (K →+* ℂ) ℂ := B.toMatrix fun i ↦ (canonicalEmbedding K) ((integralBasis K) (e i))
N : Matrix (K →+* ℂ) (K →+* ℂ) ℂ :=
  Algebra.embeddingsMatrixReindex ℚ ℂ (fun i ↦ (integralBasis K) (e i)) (RingHom.equivRatAlgHom K ℂ)
⊢ N.det ^ 2 = (algebraMap ℚ ℂ) (Algebra.discr ℚ (⇑(integralBasis K) ∘ ⇑e.symm.symm))
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: k : Type u_1
inst✝¹ : Field k
K : Type u_2
inst✝ : Field K
f : k ≃+* K
w : InfinitePlace K
⊢ (mk (w.embedding.comp ↑f)).IsReal ↔ (mk w.embedding).IsReal

Tactic:
isReal_mk_iff,

Goal state after:
k : Type u_1
inst✝¹ : Field k
K : Type u_2
inst✝ : Field K
f : k ≃+* K
w : InfinitePlace K
⊢ ComplexEmbedding.IsReal (w.embedding.comp ↑f) ↔ (mk w.embedding).IsReal
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: k : Type u_1
inst✝¹ : Field k
K : Type u_2
inst✝ : Field K
f : k ≃+* K
w : InfinitePlace K
⊢ ComplexEmbedding.IsReal (w.embedding.comp ↑f) ↔ (mk w.embedding).IsReal

Tactic:
isReal_mk_iff,

Goal state after:
k : Type u_1
inst✝¹ : Field k
K : Type u_2
inst✝ : Field K
f : k ≃+* K
w : InfinitePlace K
⊢ ComplexEmbedding.IsReal (w.embedding.comp ↑f) ↔ ComplexEmbedding.IsReal w.embedding
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: case pos.a
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
h_zero : (commMap K) x = 0
h_mem : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
φ : K →+* ℂ
hφ : ComplexEmbedding.IsReal φ
⊢ (x φ).re = Complex.re 0

Tactic:
← embedding_mk_eq_of_isReal hφ,

Goal state after:
case pos.a
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
h_zero : (commMap K) x = 0
h_mem : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
φ : K →+* ℂ
hφ : ComplexEmbedding.IsReal φ
⊢ (x (InfinitePlace.mk φ).embedding).re = Complex.re 0
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
w : InfinitePlace K
x y : mixedSpace K
⊢ (normAtPlace w) (x + y) ≤ (normAtPlace w) x + (normAtPlace w) y

Tactic:
rw [normAtPlace, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk]
  split_ifs <;> exact norm_add_le _ _

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
w : InfinitePlace K
hw : w.IsReal
x : mixedSpace K
⊢ (normAtPlace w) x = ‖x.1 ⟨w, hw⟩‖

Tactic:
rw [normAtPlace, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk, dif_pos]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
σ : Gal(K/k)
φ : K →+* ℂ
h : ComplexEmbedding.IsConj φ σ
⊢ ¬(mk φ).IsReal ∧ (mk (φ.comp (algebraMap k K))).IsReal ↔ ¬ComplexEmbedding.IsReal φ

Tactic:
isReal_mk_iff,

Goal state after:
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
σ : Gal(K/k)
φ : K →+* ℂ
h : ComplexEmbedding.IsConj φ σ
⊢ ¬ComplexEmbedding.IsReal φ ∧ (mk (φ.comp (algebraMap k K))).IsReal ↔ ¬ComplexEmbedding.IsReal φ
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
σ : Gal(K/k)
φ : K →+* ℂ
h : ComplexEmbedding.IsConj φ σ
⊢ ¬ComplexEmbedding.IsReal φ ∧ (mk (φ.comp (algebraMap k K))).IsReal ↔ ¬ComplexEmbedding.IsReal φ

Tactic:
isReal_mk_iff,

Goal state after:
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
σ : Gal(K/k)
φ : K →+* ℂ
h : ComplexEmbedding.IsConj φ σ
⊢ ¬ComplexEmbedding.IsReal φ ∧ ComplexEmbedding.IsReal (φ.comp (algebraMap k K)) ↔ ¬ComplexEmbedding.IsReal φ
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
φ : K →+* ℂ
H : ∀ (σ : Gal(K/k)), ComplexEmbedding.IsConj φ σ → σ = 1
hφ : (mk φ).IsComplex ∧ (mk (φ.comp (algebraMap k K))).IsReal
⊢ False

Tactic:
isReal_mk_iff,

Goal state after:
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
φ : K →+* ℂ
H : ∀ (σ : Gal(K/k)), ComplexEmbedding.IsConj φ σ → σ = 1
hφ : (mk φ).IsComplex ∧ ComplexEmbedding.IsReal (φ.comp (algebraMap k K))
⊢ False
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
φ : K →+* ℂ
H : ∀ (σ : Gal(K/k)), ComplexEmbedding.IsConj φ σ → σ = 1
hφ : ¬(mk φ).IsReal ∧ ComplexEmbedding.IsReal (φ.comp (algebraMap k K))
⊢ False

Tactic:
isReal_mk_iff,

Goal state after:
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
φ : K →+* ℂ
H : ∀ (σ : Gal(K/k)), ComplexEmbedding.IsConj φ σ → σ = 1
hφ : ¬ComplexEmbedding.IsReal φ ∧ ComplexEmbedding.IsReal (φ.comp (algebraMap k K))
⊢ False
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ (volume (fundamentalDomain (latticeBasis K))).toReal = 2⁻¹ ^ nrComplexPlaces K * √|↑(discr K)|

Tactic:
volume_fundamentalDomain_latticeBasis,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ (2⁻¹ ^ nrComplexPlaces K * ↑(sqrt ‖discr K‖₊)).toReal = 2⁻¹ ^ nrComplexPlaces K * √|↑(discr K)|
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
⊢ (ENNReal.ofReal ↑(FractionalIdeal.absNorm ↑I) * volume (fundamentalDomain (latticeBasis K))).toReal =
    ↑(FractionalIdeal.absNorm ↑I) * 2⁻¹ ^ nrComplexPlaces K * √|↑(discr K)|

Tactic:
volume_fundamentalDomain_latticeBasis,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
⊢ (ENNReal.ofReal ↑(FractionalIdeal.absNorm ↑I) * (2⁻¹ ^ nrComplexPlaces K * ↑(sqrt ‖discr K‖₊))).toReal =
    ↑(FractionalIdeal.absNorm ↑I) * 2⁻¹ ^ nrComplexPlaces K * √|↑(discr K)|