mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.LSeries.Dirichlet

Goal state before:
pp: case refine_2
N : ℕ
R : Type u_1
inst✝ : CommMonoidWithZero R
χ : DirichletCharacter R N
m n : ℕ
hm : m ≠ 0
hn : n ≠ 0
x✝ : m.Coprime n
⊢ (toArithmeticFunction fun x ↦ χ ↑x) (m * n) =
    (toArithmeticFunction fun x ↦ χ ↑x) m * (toArithmeticFunction fun x ↦ χ ↑x) n

Tactic:
simp [toArithmeticFunction, hm, hn]

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) = χ (↑p.1 * ↑p.2) * (f p.1 * g p.2)

Tactic:
map_mul

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
⊢ DifferentiableAt ℂ (fun s ↦ (completedHurwitzZetaEven a s - 1 / (s - 1)) * s.Gammaℝ⁻¹) 1

Tactic:
refine DifferentiableAt.mul ?_ differentiable_Gammaℝ_inv.differentiableAt

Goal state after:
a : UnitAddCircle
⊢ DifferentiableAt ℂ (fun s ↦ completedHurwitzZetaEven a s - 1 / (s - 1)) 1
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case inr.inr
z x0 y0 : ℤ
hx : (x0 * 2 + 1) % 2 = 1
hy : (y0 * 2 + 1) % 2 = 1
h : PythagoreanTriple (x0 * 2 + 1) (y0 * 2 + 1) z
hc : (x0 * 2 + 1).gcd (y0 * 2 + 1) = 1
⊢ False

Tactic:
apply Int.sq_ne_two_mod_four z

Goal state after:
case inr.inr
z x0 y0 : ℤ
hx : (x0 * 2 + 1) % 2 = 1
hy : (y0 * 2 + 1) % 2 = 1
h : PythagoreanTriple (x0 * 2 + 1) (y0 * 2 + 1) z
hc : (x0 * 2 + 1).gcd (y0 * 2 + 1) = 1
⊢ z * z % 4 = 2
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: z x0 y0 : ℤ
hx : (x0 * 2 + 1) % 2 = 1
hy : (y0 * 2 + 1) % 2 = 1
h : PythagoreanTriple (x0 * 2 + 1) (y0 * 2 + 1) z
hc : (x0 * 2 + 1).gcd (y0 * 2 + 1) = 1
⊢ z * z = 4 * (x0 * x0 + x0 + y0 * y0 + y0) + 2

Tactic:
← h.eq

Goal state after:
z x0 y0 : ℤ
hx : (x0 * 2 + 1) % 2 = 1
hy : (y0 * 2 + 1) % 2 = 1
h : PythagoreanTriple (x0 * 2 + 1) (y0 * 2 + 1) z
hc : (x0 * 2 + 1).gcd (y0 * 2 + 1) = 1
⊢ (x0 * 2 + 1) * (x0 * 2 + 1) + (y0 * 2 + 1) * (y0 * 2 + 1) = 4 * (x0 * x0 + x0 + y0 * y0 + y0) + 2
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case neg
z : ℤ
k : ℕ
x0 y0 : ℤ
left✝ : 0 < k
h2 : x0.gcd y0 = 1
h : PythagoreanTriple (x0 * ↑k) (y0 * ↑k) z
h0 : ¬(x0 * ↑k).gcd (y0 * ↑k) = 0
⊢ ↑k ^ 2 ∣ z * z

Tactic:
← h.eq

Goal state after:
case neg
z : ℤ
k : ℕ
x0 y0 : ℤ
left✝ : 0 < k
h2 : x0.gcd y0 = 1
h : PythagoreanTriple (x0 * ↑k) (y0 * ↑k) z
h0 : ¬(x0 * ↑k).gcd (y0 * ↑k) = 0
⊢ ↑k ^ 2 ∣ x0 * ↑k * (x0 * ↑k) + y0 * ↑k * (y0 * ↑k)
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
⊢ m.gcd (r * s) = 1

Tactic:
htt3

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
⊢ (r ^ 2 + s ^ 2).gcd (r * s) = 1
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:
← mul_dvd_mul_iff_left radical_ne_zero,

Goal state after:
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
p : k[X]
hp : Prime p
i : ℕ
⊢ radical ?m.103 * divRadical (p ^ (i + 1)) ∣ radical ?m.103 * derivative (p ^ (i + 1))

k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
p : k[X]
hp : Prime p
i : ℕ
⊢ k[X]
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))
⊢ 2 ∣ (m0 * 2 + 1) ^ 2 + (n0 * 2 + 1) ^ 2 ∧
    2 ∣ (m0 * 2 + 1) ^ 2 - (n0 * 2 + 1) ^ 2 ∧
      ((m0 * 2 + 1) ^ 2 - (n0 * 2 + 1) ^ 2) / 2 % 2 = 0 ∧
        (((m0 * 2 + 1) ^ 2 - (n0 * 2 + 1) ^ 2) / 2).gcd (((m0 * 2 + 1) ^ 2 + (n0 * 2 + 1) ^ 2) / 2) = 1

Tactic:
have h3 : ((m0 * 2 + 1) ^ 2 - (n0 * 2 + 1) ^ 2) / 2 % 2 = 0 := by
    rw [h2, Int.mul_ediv_cancel_left, Int.mul_emod_right]
    decide

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
⊢ 2 ∣ (m0 * 2 + 1) ^ 2 + (n0 * 2 + 1) ^ 2 ∧
    2 ∣ (m0 * 2 + 1) ^ 2 - (n0 * 2 + 1) ^ 2 ∧
      ((m0 * 2 + 1) ^ 2 - (n0 * 2 + 1) ^ 2) / 2 % 2 = 0 ∧
        (((m0 * 2 + 1) ^ 2 - (n0 * 2 + 1) ^ 2) / 2).gcd (((m0 * 2 + 1) ^ 2 + (n0 * 2 + 1) ^ 2) / 2) = 1
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: E : Type u_1
inst✝² : EuclideanDomain E
inst✝¹ : NormalizationMonoid E
inst✝ : UniqueFactorizationMonoid E
a : E
⊢ radical a * divRadical a = a

Tactic:
divRadical,

Goal state after:
E : Type u_1
inst✝² : EuclideanDomain E
inst✝¹ : NormalizationMonoid E
inst✝ : UniqueFactorizationMonoid E
a : E
⊢ radical a * (a / radical a) = a
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: E : Type u_1
inst✝² : EuclideanDomain E
inst✝¹ : NormalizationMonoid E
inst✝ : UniqueFactorizationMonoid E
u : E
hu : IsUnit u
⊢ IsUnit (divRadical u)

Tactic:
divRadical,

Goal state after:
E : Type u_1
inst✝² : EuclideanDomain E
inst✝¹ : NormalizationMonoid E
inst✝ : UniqueFactorizationMonoid E
u : E
hu : IsUnit u
⊢ IsUnit (u / radical u)
Module: Mathlib.NumberTheory.NumberField.Norm

Goal state before:
pp: K : Type u_2
inst✝⁴ : Field K
F : Type u_3
inst✝³ : Field F
inst✝² : Algebra K F
inst✝¹ : FiniteDimensional K F
inst✝ : CharZero K
x : 𝓞 F
this✝¹ : Algebra K (AlgebraicClosure K) := AlgebraicClosure.instAlgebra K
L : IntermediateField K (AlgebraicClosure F) := normalClosure K F (AlgebraicClosure F)
this✝ : FiniteDimensional F ↥L
this : IsGalois F ↥L
⊢ IsUnit ((norm K) x ^ finrank F ↥L) ↔ IsUnit ((norm K) ((algebraMap (𝓞 F) (𝓞 ↥L)) x))

Tactic:
← norm_norm K F (algebraMap (𝓞 F) (𝓞 L) x),

Goal state after:
K : Type u_2
inst✝⁴ : Field K
F : Type u_3
inst✝³ : Field F
inst✝² : Algebra K F
inst✝¹ : FiniteDimensional K F
inst✝ : CharZero K
x : 𝓞 F
this✝¹ : Algebra K (AlgebraicClosure K) := AlgebraicClosure.instAlgebra K
L : IntermediateField K (AlgebraicClosure F) := normalClosure K F (AlgebraicClosure F)
this✝ : FiniteDimensional F ↥L
this : IsGalois F ↥L
⊢ IsUnit ((norm K) x ^ finrank F ↥L) ↔ IsUnit ((norm K) ((norm F) ((algebraMap (𝓞 F) (𝓞 ↥L)) x)))
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: z k m n : ℤ
right✝ : m.gcd n = 1
h : PythagoreanTriple (k * (m ^ 2 - n ^ 2)) (k * (2 * m * n)) z
⊢ z * z = (k * (m ^ 2 + n ^ 2)) ^ 2

Tactic:
← h.eq

Goal state after:
z k m n : ℤ
right✝ : m.gcd n = 1
h : PythagoreanTriple (k * (m ^ 2 - n ^ 2)) (k * (2 * m * n)) z
⊢ k * (m ^ 2 - n ^ 2) * (k * (m ^ 2 - n ^ 2)) + k * (2 * m * n) * (k * (2 * m * n)) = (k * (m ^ 2 + n ^ 2)) ^ 2
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: z k m n : ℤ
right✝ : m.gcd n = 1
h : PythagoreanTriple (k * (2 * m * n)) (k * (m ^ 2 - n ^ 2)) z
⊢ z * z = (k * (m ^ 2 + n ^ 2)) ^ 2

Tactic:
← h.eq

Goal state after:
z k m n : ℤ
right✝ : m.gcd n = 1
h : PythagoreanTriple (k * (2 * m * n)) (k * (m ^ 2 - n ^ 2)) z
⊢ k * (2 * m * n) * (k * (2 * m * n)) + k * (m ^ 2 - n ^ 2) * (k * (m ^ 2 - n ^ 2)) = (k * (m ^ 2 + n ^ 2)) ^ 2
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
a : 𝓞 K
ha : a ≠ 0
h : ∀ ⦃z : InfinitePlace K⦄, z ≠ w → z ↑a < 1
this : w ↑a < 1
z : InfinitePlace K
x✝ : z ∈ Finset.univ
hz : ¬z = w
⊢ z ↑a < 1

Tactic:
· exact h hz

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Finite ↥(torsion K)

Tactic:
by
  refine Set.Finite.of_finite_image ?_ (coe_injective K).injOn
  refine (Embeddings.finite_of_norm_le K ℂ 1).subset
    (fun a ⟨u, ⟨h_tors, h_ua⟩⟩ => ⟨?_, fun φ => ?_⟩)
  · rw [← h_ua]
    exact u.val.prop
  · rw [← h_ua]
    exact le_of_eq ((eq_iff_eq _ 1).mp ((mem_torsion K).mp h_tors) φ)

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

Goal state before:
pp: 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))

Tactic:
let e := ((torsion K).equivMapOfInjective (Units.complexEmbedding φ)
      (Units.complexEmbedding_injective φ)).symm.toEquiv

Goal state after:
case hcard
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
φ : K →+* ℂ
e : ↥(Subgroup.map (Units.complexEmbedding φ) (torsion K)) ≃ ↥(torsion K) :=
  ((torsion K).equivMapOfInjective (Units.complexEmbedding φ) ⋯).symm.toEquiv
⊢ Nat.card ↥(rootsOfUnity (torsionOrder K) ℂ) ≤ Nat.card ↥(Subgroup.map (Units.complexEmbedding φ) (torsion K))
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
w : InfinitePlace K
h₁ : x ≠ 0
h₂ : ∀ ⦃w' : InfinitePlace K⦄, w' ≠ w → w' ↑x < 1
h₃ : w.IsReal ∨ |(w.embedding ↑x).re| < 1
⊢ ∀ (ψ : K →ₐ[ℚ] ℂ), w.embedding.toRatAlgHom ↑x = ψ ↑x → w.embedding.toRatAlgHom = ψ

Tactic:
intro ψ hψ
    have h : 1 ≤ w x := one_le_of_lt_one h₁ h₂
    have main : w = InfinitePlace.mk ψ.toRingHom := by
      simp only [RingHom.toRatAlgHom_apply] at hψ
      rw [← norm_embedding_eq, hψ] at h
      contrapose! h
      exact h₂ h.symm
    rw [(mk_embedding w).symm, mk_eq_iff] at main
    cases h₃ with
    | inl hw =>
      rw [conjugate_embedding_eq_of_isReal hw, or_self] at main
      exact congr_arg RingHom.toRatAlgHom main
    | inr hw =>
      refine congr_arg RingHom.toRatAlgHom (main.resolve_right fun h' ↦ hw.not_ge ?_)
      have : (embedding w x).im = 0 := by
        rw [← Complex.conj_eq_iff_im]
        have := RingHom.congr_fun h' x
        simp only [ComplexEmbedding.conjugate_coe_eq, AlgHom.toRingHom_eq_coe,
          RingHom.coe_coe] at this
        rw [this]
        exact hψ.symm
      rwa [← norm_embedding_eq, ← Complex.re_add_im (embedding w x), this, Complex.ofReal_zero,
        zero_mul, add_zero, Complex.norm_real] at h

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

Goal state before:
pp: case e'_2.refine_3
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : w.IsComplex
x✝ : { x // mk x = w }
φ : K →+* ℂ
hφ : mk φ = w
⊢ mkComplex ⟨φ, ⋯⟩ = ⟨w, hw⟩

Tactic:
Subtype.ext_iff,

Goal state after:
case e'_2.refine_3
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : w.IsComplex
x✝ : { x // mk x = w }
φ : K →+* ℂ
hφ : mk φ = w
⊢ ↑(mkComplex ⟨φ, ⋯⟩) = ↑⟨w, hw⟩
Module: Mathlib.NumberTheory.FLT.Polynomial

Goal state before:
pp: case refine_3
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
heq' : C v * b ^ q + C w * c ^ r + C u * a ^ p = 0
hca : IsCoprime c a
⊢ c.natDegree = 0

Tactic:
rw [← add_rotate] at heq hineq

Goal state after:
case refine_3
k : Type u_1
inst✝ : Field k
p q r : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : p * q + q * r + r * p ≤ 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 w * c ^ r + C u * a ^ p + C v * b ^ q = 0
hbc : IsCoprime b c
heq' : C v * b ^ q + C w * c ^ r + C u * a ^ p = 0
hca : IsCoprime c a
⊢ c.natDegree = 0
Module: Mathlib.NumberTheory.FLT.Polynomial

Goal state before:
pp: k : Type u_1
inst✝ : Field k
n : ℕ
hn : 3 ≤ n
chn : ↑n ≠ 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
heq : 1 * a ^ n + 1 * b ^ n - c ^ n = 0
hn' : 0 < n
⊢ a.natDegree = 0 ∧ b.natDegree = 0 ∧ c.natDegree = 0

Tactic:
← one_mul (c ^ n),

Goal state after:
k : Type u_1
inst✝ : Field k
n : ℕ
hn : 3 ≤ n
chn : ↑n ≠ 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
heq : 1 * a ^ n + 1 * b ^ n - 1 * c ^ n = 0
hn' : 0 < n
⊢ a.natDegree = 0 ∧ b.natDegree = 0 ∧ c.natDegree = 0
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
K : Type u_2
inst✝ : Field K
v : InfinitePlace ℚ
⊢ v.IsReal

Tactic:
Subsingleton.elim v Rat.infinitePlace

Goal state after:
F : Type u_1
inst✝¹ : Field F
K : Type u_2
inst✝ : Field K
v : InfinitePlace ℚ
⊢ Rat.infinitePlace.IsReal
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: case refine_4
K : Type u_1
inst✝ : Field K
x : (K →+* ℂ) → ℂ
φ : K →+* ℂ
hx✝ : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
a : ℝ
x✝¹ : (K →+* ℂ) → ℂ
x✝ : x✝¹ ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
hx : (starRingEnd ℂ) (x✝¹ φ) = x✝¹ (ComplexEmbedding.conjugate φ)
⊢ (starRingEnd ℂ) ((a • x✝¹) φ) = (a • x✝¹) (ComplexEmbedding.conjugate φ)

Tactic:
rw [Pi.smul_apply, Complex.real_smul, map_mul, Complex.conj_ofReal]
    exact congrArg ((a : ℂ) * ·) hx

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
F : Type u_3
inst✝⁴ : Field F
inst✝³ : Algebra k K
inst✝² : Algebra k F
inst✝¹ : Algebra K F
inst✝ : IsScalarTower k K F
w : InfinitePlace F
h : IsUnramified k w
⊢ IsUnramified K w

Tactic:
by
  rw [InfinitePlace.isUnramified_iff_mult_le, ← h.eq, IsScalarTower.algebraMap_eq k K F,
    InfinitePlace.comap_comp]
  exact InfinitePlace.mult_comap_le _ _

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

Goal state before:
pp: case refine_1
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
φ : K →+* ℂ
h : IsRamified k (mk φ)
⊢ IsMixed k φ

pp: case refine_2
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
φ : K →+* ℂ
h : IsMixed k φ
⊢ IsRamified k (mk φ)

Tactic:
· rcases embedding_mk_eq φ with (hl | hr)
    · exact hl ▸ h.isMixed_embedding
    · rw [← star_star φ]; simpa [← congrArg conjugate hr] using h.isMixed_conjugate_embedding

Goal state after:
case refine_2
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
φ : K →+* ℂ
h : IsMixed k φ
⊢ IsRamified k (mk φ)
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: case refine_1.inl
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
φ : K →+* ℂ
h : IsUnramified k (mk φ)
hl : (mk φ).embedding = φ
⊢ IsUnmixed k φ

pp: case refine_1.inr
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
φ : K →+* ℂ
h : IsUnramified k (mk φ)
hr : (mk φ).embedding = conjugate φ
⊢ IsUnmixed k φ

Tactic:
· exact hl ▸ h.isUnmixed

Goal state after:
case refine_1.inr
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
φ : K →+* ℂ
h : IsUnramified k (mk φ)
hr : (mk φ).embedding = conjugate φ
⊢ IsUnmixed k φ
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB : B ≤ 0
⊢ 0 = ↑(convexBodySumFactor K) * 0

pp: case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB : B ≤ 0
⊢ finrank ℚ K ≠ 0

Tactic:
mul_zero

Goal state after:
case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB : B ≤ 0
⊢ 0 = 0

case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB : B ≤ 0
⊢ finrank ℚ K ≠ 0
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✝² : NumberField K
inst✝¹ : NumberField k
inst✝ : IsGalois k K
w : InfinitePlace K
hw : IsUnramifiedIn K ((fun x ↦ x.comap (algebraMap k K)) w)
w' : InfinitePlace K
e : (fun x ↦ x.comap (algebraMap k K)) w = w'.comap (algebraMap k K)
⊢ IsUnramified k w'

Tactic:
rwa [← isUnramifiedIn_comap, ← e]

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
inst✝² : NumberField K
inst✝¹ : NumberField k
inst✝ : IsGalois k K
w : InfinitePlace K
hw : ¬IsUnramifiedIn K ((fun x ↦ x.comap (algebraMap k K)) w)
w' : InfinitePlace K
e : (fun x ↦ x.comap (algebraMap k K)) w = w'.comap (algebraMap k K)
⊢ ¬IsUnramified k w'

Tactic:
rwa [← isUnramifiedIn_comap, ← e]

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
inst✝² : NumberField K
inst✝¹ : NumberField k
inst✝ : IsGalois k K
⊢ #{w | IsUnramified k w}ᶜ = #{w | IsUnramifiedIn K w}ᶜ * (finrank k K / 2)

Tactic:
rw [← IsGalois.card_aut_eq_finrank,
    Finset.card_eq_sum_card_fiberwise (f := (comap · (algebraMap k K)))
    (t := ({w : InfinitePlace k | w.IsUnramifiedIn K} : Finset _)ᶜ), ← smul_eq_mul, ← sum_const]
  · refine sum_congr rfl (fun w hw ↦ ?_)
    obtain ⟨w, rfl⟩ := comap_surjective (K := K) w
    rw [compl_filter, mem_filter_univ] at hw
    trans Finset.card (MulAction.orbit Gal(K/k) w).toFinset
    · congr; ext w'
      rw [mem_filter, compl_filter, mem_filter_univ, @eq_comm _ (comap w' _), Set.mem_toFinset,
        mem_orbit_iff, and_iff_right_iff_imp]
      intro e; rwa [← isUnramifiedIn_comap, ← e]
    · rw [Nat.card_eq_fintype_card,
        ← MulAction.card_orbit_mul_card_stabilizer_eq_card_group _ w,
        ← Nat.card_eq_fintype_card (α := Stab w), InfinitePlace.card_stabilizer, if_neg,
        Nat.mul_div_cancel _ zero_lt_two, Set.toFinset_card]
      rwa [← isUnramifiedIn_comap]
  · simp [Set.MapsTo, isUnramifiedIn_comap]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
x : mixedSpace K
⊢ ↑(Submodule.span ℤ (Set.range ⇑(basisOfFractionalIdeal K I))) = ↑↑I

Tactic:
ext; simp [mem_span_basisOfFractionalIdeal]

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsTotallyComplex K
h : 0 < ↑(finrank ℚ K)
⊢ ↑(finrank ℚ K) ^ 2 / (4 / π * ↑(finrank ℚ K).factorial ^ (2 * (↑(finrank ℚ K))⁻¹)) ≤ ↑|discr K| ^ (↑(finrank ℚ K))⁻¹

Tactic:
rw [← Real.rpow_le_rpow_iff (z := finrank ℚ K) (by positivity) (by positivity) h, Real.div_rpow
    (by positivity) (by positivity), ← Real.rpow_mul (by positivity), inv_mul_cancel₀ h.ne',
    Real.rpow_one, Real.mul_rpow (by positivity) (by positivity), Real.rpow_natCast,
    Real.rpow_natCast, ← pow_mul, ← Real.rpow_mul (by positivity),
    inv_mul_cancel_right₀ h.ne', Real.rpow_two]

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsTotallyComplex K
h : 0 < ↑(finrank ℚ K)
⊢ ↑(finrank ℚ K) ^ (2 * finrank ℚ K) / ((4 / π) ^ finrank ℚ K * ↑(finrank ℚ K).factorial ^ 2) ≤ ↑|discr K|
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
x✝ : realSpace K
h : mixedSpaceOfRealSpace x✝ = 0
⊢ x✝ = 0

Tactic:
mixedSpaceOfRealSpace_apply,

Goal state after:
K : Type u_1
inst✝ : Field K
x✝ : realSpace K
h : (fun w ↦ x✝ ↑w, fun w ↦ ↑(x✝ ↑w)) = 0
⊢ x✝ = 0
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: case inr
K : Type u_1
inst✝ : Field K
x : realSpace K
hx : ∀ (w : InfinitePlace K), w.IsComplex → 0 ≤ x w
w : InfinitePlace K
hw : w.IsComplex
⊢ ‖(mixedSpaceOfRealSpace x).2 ⟨w, hw⟩‖ = x w

Tactic:
mixedSpaceOfRealSpace_apply,

Goal state after:
case inr
K : Type u_1
inst✝ : Field K
x : realSpace K
hx : ∀ (w : InfinitePlace K), w.IsComplex → 0 ≤ x w
w : InfinitePlace K
hw : w.IsComplex
⊢ ‖(fun w ↦ x ↑w, fun w ↦ ↑(x ↑w)).2 ⟨w, hw⟩‖ = x w
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

Goal state before:
pp: A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
p : IntermediateField ℚ A → Prop
S : Set { F // p F }
T : Set A
hT : Finite ↑T
h : ∀ F ∈ S, ∃ x ∈ T, ↑F = ℚ⟮x⟯
x✝¹ x✝ : ↑S
h_eq :
  (fun x ↦
        match x with
        | ⟨F, hF⟩ => ⟨⋯.choose, ⋯⟩)
      x✝¹ =
    (fun x ↦
        match x with
        | ⟨F, hF⟩ => ⟨⋯.choose, ⋯⟩)
      x✝
⊢ x✝¹ = x✝

Tactic:
Subtype.ext_iff,

Goal state after:
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
p : IntermediateField ℚ A → Prop
S : Set { F // p F }
T : Set A
hT : Finite ↑T
h : ∀ F ∈ S, ∃ x ∈ T, ↑F = ℚ⟮x⟯
x✝¹ x✝ : ↑S
h_eq :
  (fun x ↦
        match x with
        | ⟨F, hF⟩ => ⟨⋯.choose, ⋯⟩)
      x✝¹ =
    (fun x ↦
        match x with
        | ⟨F, hF⟩ => ⟨⋯.choose, ⋯⟩)
      x✝
⊢ ↑x✝¹ = ↑x✝
Module: Mathlib.NumberTheory.RamificationInertia.Galois

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹⁶ : CommRing A
inst✝¹⁵ : CommRing B
inst✝¹⁴ : Algebra A B
p : Ideal A
G : Type u_3
inst✝¹³ : Group G
inst✝¹² : MulSemiringAction G B
inst✝¹¹ : SMulCommClass G A B
K : Type u_4
L : Type u_5
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra A K
inst✝⁷ : IsFractionRing A K
inst✝⁶ : Algebra B L
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra A L
inst✝³ : IsScalarTower A B L
inst✝² : IsScalarTower A K L
inst✝¹ : IsIntegralClosure B A L
inst✝ : FiniteDimensional K L
σ τ : Gal(L/K)
Q : ↑(p.primesOver B)
⊢ map ((galRestrict A K L B) (σ * τ)) ↑Q = map ((galRestrict A K L B) σ) (map ((galRestrict A K L B) τ) ↑Q)

Tactic:
map_mul

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹⁶ : CommRing A
inst✝¹⁵ : CommRing B
inst✝¹⁴ : Algebra A B
p : Ideal A
G : Type u_3
inst✝¹³ : Group G
inst✝¹² : MulSemiringAction G B
inst✝¹¹ : SMulCommClass G A B
K : Type u_4
L : Type u_5
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra A K
inst✝⁷ : IsFractionRing A K
inst✝⁶ : Algebra B L
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra A L
inst✝³ : IsScalarTower A B L
inst✝² : IsScalarTower A K L
inst✝¹ : IsIntegralClosure B A L
inst✝ : FiniteDimensional K L
σ τ : Gal(L/K)
Q : ↑(p.primesOver B)
⊢ map ((galRestrict A K L B) σ * (galRestrict A K L B) τ) ↑Q =
    map ((galRestrict A K L B) σ) (map ((galRestrict A K L B) τ) ↑Q)
Module: Mathlib.NumberTheory.RamificationInertia.Galois

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹⁶ : CommRing A
inst✝¹⁵ : CommRing B
inst✝¹⁴ : Algebra A B
p : Ideal A
G : Type u_3
inst✝¹³ : Group G
inst✝¹² : MulSemiringAction G B
inst✝¹¹ : SMulCommClass G A B
K : Type u_4
L : Type u_5
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra A K
inst✝⁷ : IsFractionRing A K
inst✝⁶ : Algebra B L
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra A L
inst✝³ : IsScalarTower A B L
inst✝² : IsScalarTower A K L
inst✝¹ : IsIntegralClosure B A L
inst✝ : FiniteDimensional K L
Q : ↑(p.primesOver B)
⊢ map ((galRestrict A K L B) 1) ↑Q = ↑Q

Tactic:
simpa only [map_one] using! map_id Q.1

Goal state after: