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

Goal state before:
pp: x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hzpos : 0 < z
m n : ℤ
hm2n2 : 0 < m ^ 2 + n ^ 2
hv2 : ↑x / ↑z = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hw2 : ↑y / ↑z = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
H : (m ^ 2 - n ^ 2).gcd (m ^ 2 + n ^ 2) = 1
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
⊢ h.IsPrimitiveClassified

Tactic:
by
  have hz : z ≠ 0 := ne_of_gt hzpos
  have h2 : y = m ^ 2 - n ^ 2 ∧ z = m ^ 2 + n ^ 2 := by
    apply Rat.div_int_inj hzpos hm2n2 (h.coprime_of_coprime hc) H
    rw [hw2]
    norm_cast
  use m, n
  apply And.intro _ (And.intro co pp)
  right
  refine ⟨?_, h2.left⟩
  rw [← Rat.intCast_inj, ← div_left_inj' (mt Rat.intCast_inj.mp hz), hv2, h2.right]
  norm_cast

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

Goal state before:
pp: k : Type u_1
inst✝ : Field k
p q r : ℕ
a b c : k[X]
u v w : k
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0
hab : IsCoprime a b
hCu : IsUnit (C u)
⊢ IsCoprime b c

Tactic:
have hCv : IsUnit (C v) := hv.isUnit_C

Goal state after:
k : Type u_1
inst✝ : Field k
p q r : ℕ
a b c : k[X]
u v w : k
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0
hab : IsCoprime a b
hCu : IsUnit (C u)
hCv : IsUnit (C v)
⊢ IsCoprime b c
Module: Mathlib.NumberTheory.NumberField.FractionalIdeal

Goal state before:
pp: case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
x : K
a : 𝓞 K
d : ℤ
hd : d ∈ ↑ℤ⁰
h :
  x * (algebraMap (𝓞 K) K) ↑(a, ⟨(algebraMap ℤ (𝓞 K)) d, ⋯⟩).2 = (algebraMap (𝓞 K) K) (a, ⟨(algebraMap ℤ (𝓞 K)) d, ⋯⟩).1
⊢ ↑(Ideal.absNorm (↑I).num) * (algebraMap (𝓞 K) K) a ∈ ↑(↑I).num

Tactic:
refine (IsLocalization.mem_coeSubmodule _ _).mpr ⟨Ideal.absNorm I.1.num * a, ?_, ?_⟩
      · exact Ideal.mul_mem_right _ _ I.1.num.absNorm_mem
      · rw [map_mul, map_natCast]

Goal state after:
Module: Mathlib.Topology.Instances.Complex

Goal state before:
pp: case e'_2
K : Subfield ℂ
ψ : ↥K →+* ℂ
hc : UniformContinuous ⇑ψ
this✝¹ : IsTopologicalDivisionRing ℂ :=
  { toIsTopologicalRing := NormedDivisionRing.to_isTopologicalDivisionRing.toIsTopologicalRing,
    toContinuousInv₀ := NormedDivisionRing.to_isTopologicalDivisionRing.toContinuousInv₀ }
this✝ : IsTopologicalRing ↥K.topologicalClosure := Subring.instIsTopologicalRing K.topologicalClosure.toSubring
ι : ↥K → ↥K.topologicalClosure := ⇑(Subfield.inclusion ⋯)
ui : IsUniformInducing ι
di : IsDenseInducing ι := IsUniformInducing.isDenseInducing ui ?refine_1
extψ : ↥K.topologicalClosure →+* ℂ := IsDenseInducing.extendRingHom ui ⋯ hc
hψ : Continuous (⋯.extend ⇑ψ)
h : K.topologicalClosure = ofRealHom.fieldRange
j : ↥K.topologicalClosure ≃+* ↥ofRealHom.fieldRange := RingEquiv.subfieldCongr h
ψ₁ : ℝ →+* ℂ := extψ.comp (j.symm.toRingHom.comp ofRealHom.rangeRestrictField)
hψ₁ : Continuous ⇑ψ₁
x : ↥K
r : ℝ
hr : ofRealHom.rangeRestrictField r = j (ι x)
this : extψ (↑j.symm (j (ι x))) = ofRealHom r
⊢ (↑↑ψ).toFun x = extψ (↑j.symm (j (ι x)))

Tactic:
exact (IsDenseInducing.extend_eq di hc.continuous _).symm

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

Goal state before:
pp: k : Type u_1
inst✝ : Field k
a : k[X]
ha : a ≠ 0
hda : derivative a = 0
chn0 : ringChar k ≠ 0
⊢ ∃ ca, ca ≠ 0 ∧ a = (expand k (ringChar k)) ca ∧ a.natDegree = ca.natDegree * ringChar k

Tactic:
by
  have heq := (expand_contract (ringChar k) hda chn0).symm
  refine ⟨contract (ringChar k) a, ?_, heq, ?_⟩
  · intro h
    rw [h, map_zero] at heq
    exact ha heq
  · rw [← natDegree_expand, ← heq]

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

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

Tactic:
rintro (⟨h⟩ | ⟨h⟩)

Goal state after:
case mpr.inl
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h : φ = ψ
⊢ mk φ = mk ψ

case mpr.inr
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h : ComplexEmbedding.conjugate φ = ψ
⊢ mk φ = mk ψ
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
hw : ¬w.IsReal
⊢ #({w.embedding} ∪ {ComplexEmbedding.conjugate w.embedding}) = 2

Tactic:
refine Finset.card_pair ?_
    rwa [Ne, eq_comm, ← ComplexEmbedding.isReal_iff, ← isReal_iff]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℝ≥0
hf : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0
S : ℝ≥0 := ∏ w ∈ Finset.univ.erase w₁, f w ^ w.mult
w : InfinitePlace K
hw : w ∈ Finset.univ.erase w₁
⊢ Function.update f w₁ ((B * S⁻¹) ^ (↑w₁.mult)⁻¹) w ^ w.mult = ?m.102 w

Tactic:
Function.update_of_ne (Finset.ne_of_mem_erase hw)

Goal state after:
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℝ≥0
hf : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0
S : ℝ≥0 := ∏ w ∈ Finset.univ.erase w₁, f w ^ w.mult
w : InfinitePlace K
hw : w ∈ Finset.univ.erase w₁
⊢ f w ^ w.mult = ?m.102 w
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
K : Type u_2
inst✝ : Field K
a✝ b✝ : K
hx : a✝ ∈ {x | ∀ (φ : K →+* ℂ), star (φ x) = φ x}
hy : b✝ ∈ {x | ∀ (φ : K →+* ℂ), star (φ x) = φ x}
x✝ : K →+* ℂ
⊢ star (x✝ (a✝ + b✝)) = x✝ (a✝ + b✝)

Tactic:
map_add,

Goal state after:
F : Type u_1
inst✝¹ : Field F
K : Type u_2
inst✝ : Field K
a✝ b✝ : K
hx : a✝ ∈ {x | ∀ (φ : K →+* ℂ), star (φ x) = φ x}
hy : b✝ ∈ {x | ∀ (φ : K →+* ℂ), star (φ x) = φ x}
x✝ : K →+* ℂ
⊢ star (x✝ a✝ + x✝ b✝) = x✝ a✝ + x✝ b✝
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex

Goal state before:
pp: K : Type u_2
inst✝¹ : Field K
E : Subfield K
inst✝ : IsTotallyReal ↥E
⊢ E ≤ maximalRealSubfield K

Tactic:
intro x hx φ

Goal state after:
K : Type u_2
inst✝¹ : Field K
E : Subfield K
inst✝ : IsTotallyReal ↥E
x : K
hx : x ∈ E
φ : K →+* ℂ
⊢ star (φ x) = φ x
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

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

Tactic:
rw [Pi.zero_apply, Pi.zero_apply, map_zero]

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

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

Tactic:
map_add,

Goal state after:
case refine_3
K : Type u_1
inst✝ : Field K
x : (K →+* ℂ) → ℂ
φ : K →+* ℂ
hx✝ : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
x✝³ x✝² : (K →+* ℂ) → ℂ
x✝¹ : x✝³ ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
x✝ : x✝² ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
hx : (starRingEnd ℂ) (x✝³ φ) = x✝³ (ComplexEmbedding.conjugate φ)
hy : (starRingEnd ℂ) (x✝² φ) = x✝² (ComplexEmbedding.conjugate φ)
⊢ (starRingEnd ℂ) (x✝³ φ) + (starRingEnd ℂ) (x✝² φ) =
    x✝³ (ComplexEmbedding.conjugate φ) + x✝² (ComplexEmbedding.conjugate φ)
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 φ)
⊢ ↑a * (starRingEnd ℂ) (x✝¹ φ) = (a • x✝¹) (ComplexEmbedding.conjugate φ)

Tactic:
exact congrArg ((a : ℂ) * ·) hx

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
inst✝ : NumberField K
B : ℝ≥0
⊢ 2 * (2 * ↑B ^ 2) = 4 * ↑B ^ 2

Tactic:
← mul_assoc,

Goal state after:
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
inst✝ : NumberField K
B : ℝ≥0
⊢ 2 * 2 * ↑B ^ 2 = 4 * ↑B ^ 2
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
c : ℝ
x : mixedSpace K
⊢ ∑ x_1, ↑x_1.mult * (|c| * (normAtPlace x_1) x) = |c| * ∑ w, ↑w.mult * (normAtPlace w) x

Tactic:
← mul_assoc,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
c : ℝ
x : mixedSpace K
⊢ ∑ x_1, ↑x_1.mult * |c| * (normAtPlace x_1) x = |c| * ∑ w, ↑w.mult * (normAtPlace w) x
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: case e'_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB : 0 < B
this : volume (convexBodySum K 1) = ↑(convexBodySumFactor K)
⊢ convexBodySum K B = {a | ∑ x, ↑x.mult * (B⁻¹ * (normAtPlace x) a) ≤ 1}

Tactic:
← mul_assoc,

Goal state after:
case e'_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB : 0 < B
this : volume (convexBodySum K 1) = ↑(convexBodySumFactor K)
⊢ convexBodySum K B = {a | ∑ x, ↑x.mult * B⁻¹ * (normAtPlace x) a ≤ 1}
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
w : InfinitePlace K
h : ∀ (σ : Gal(K/k)), ¬ComplexEmbedding.IsConj w.embedding σ
⊢ Nat.card ↑↑(Stab (mk w.embedding)) = Nat.card ↑{1}

pp: k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
h : ∀ (σ : Gal(K/k)), ¬ComplexEmbedding.IsConj w.embedding σ
⊢ Nat.card ↑{1} = 1

Tactic:
· congr with x
      simp only [SetLike.mem_coe, mem_stabilizer_mk_iff, Set.mem_singleton_iff, or_iff_left_iff_imp,
        h x, IsEmpty.forall_iff]

Goal state after:
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
h : ∀ (σ : Gal(K/k)), ¬ComplexEmbedding.IsConj w.embedding σ
⊢ Nat.card ↑{1} = 1
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 →+* ℂ
x : Gal(K/k)
hx : x ∈ Stab (mk φ)
y : Gal(K/k)
hy : y ∈ Stab (mk φ)
h₁ : ⟨x, hx⟩ ≠ ⟨y, hy⟩
⊢ ∃ σ, ComplexEmbedding.IsConj φ σ

Tactic:
mem_stabilizer_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 →+* ℂ
x : Gal(K/k)
hx✝ : x ∈ Stab (mk φ)
hx : x = 1 ∨ ComplexEmbedding.IsConj φ x
y : Gal(K/k)
hy✝ : y ∈ Stab (mk φ)
hy : y = 1 ∨ ComplexEmbedding.IsConj φ y
h₁ : ⟨x, hx✝⟩ ≠ ⟨y, hy✝⟩
⊢ ∃ σ, ComplexEmbedding.IsConj φ σ
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: case neg
K : Type u_1
inst✝ : Field K
s : Set { w // w.IsReal }
x : mixedSpace K
w : { w // w.IsReal }
hw : w ∉ s
⊢ ((negAt s).symm x).1 w = ((negAt s) x).1 w

Tactic:
· simp_rw [negAt_apply_isReal_and_notMem _ hw, negAt, prodCongr_symm,
        prodCongr_apply, piCongrRight_symm_apply, if_neg hw, refl_symm,
        refl_apply]

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
this :
  ↑(finrank ℚ K) ^ (2 * finrank ℚ K) / ((4 / π) ^ (2 * nrComplexPlaces K) * ↑(finrank ℚ K).factorial ^ 2) ≤ ↑|discr K|
⊢ ↑(finrank ℚ K) ^ (2 * finrank ℚ K) / ((4 / π) ^ finrank ℚ K * ↑(finrank ℚ K).factorial ^ 2) ≤ ↑|discr K|

Tactic:
← IsTotallyComplex.finrank

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsTotallyComplex K
this : ↑(finrank ℚ K) ^ (2 * finrank ℚ K) / ((4 / π) ^ finrank ℚ K * ↑(finrank ℚ K).factorial ^ 2) ≤ ↑|discr 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
A : Set (mixedSpace K)
hA : ∀ (x : mixedSpace K), x ∈ A ↔ (fun w ↦ ‖x.1 w‖, x.2) ∈ A
inst✝ : NumberField K
⊢ ⋃ s, ⇑(negAt s) '' plusPart A =ᵐ[volume] A

Tactic:
← iUnion_negAt_plusPart_union A hA

Goal state after:
K : Type u_1
inst✝¹ : Field K
A : Set (mixedSpace K)
hA : ∀ (x : mixedSpace K), x ∈ A ↔ (fun w ↦ ‖x.1 w‖, x.2) ∈ A
inst✝ : NumberField K
⊢ ⋃ s, ⇑(negAt s) '' plusPart A =ᵐ[volume] (⋃ s, ⇑(negAt s) '' plusPart A) ∪ A ∩ ⋃ w, {x | x.1 w = 0}
Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_6
inst✝¹⁹ : CommRing A
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
inst✝¹⁶ : Field K
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra A K
inst✝¹³ : IsFractionRing A K
inst✝¹² : Algebra K L
inst✝¹¹ : Algebra A L
inst✝¹⁰ : IsScalarTower A K L
inst✝⁹ : Algebra B L
inst✝⁸ : IsScalarTower A B L
inst✝⁷ : IsIntegralClosure B A L
inst✝⁶ : FiniteDimensional K L
inst✝⁵ : IsIntegrallyClosed A
inst✝⁴ : IsDomain A
inst✝³ : IsDomain B
inst✝² : IsIntegrallyClosed B
inst✝¹ : Algebra.IsIntegral A B
inst✝ : IsTorsionFree A B
x : B
this : IsFractionRing B L
⊢ (norm (FractionRing A)) ((algebraMap B (FractionRing B)) x) =
    (FractionRing.algEquiv A K).symm ((norm K) ((FractionRing.algEquiv B L) ((algebraMap B (FractionRing B)) x)))

Tactic:
apply Algebra.norm_eq_of_equiv_equiv (FractionRing.algEquiv A K).toRingEquiv
    (FractionRing.algEquiv B L).toRingEquiv

Goal state after:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_6
inst✝¹⁹ : CommRing A
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
inst✝¹⁶ : Field K
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra A K
inst✝¹³ : IsFractionRing A K
inst✝¹² : Algebra K L
inst✝¹¹ : Algebra A L
inst✝¹⁰ : IsScalarTower A K L
inst✝⁹ : Algebra B L
inst✝⁸ : IsScalarTower A B L
inst✝⁷ : IsIntegralClosure B A L
inst✝⁶ : FiniteDimensional K L
inst✝⁵ : IsIntegrallyClosed A
inst✝⁴ : IsDomain A
inst✝³ : IsDomain B
inst✝² : IsIntegrallyClosed B
inst✝¹ : Algebra.IsIntegral A B
inst✝ : IsTorsionFree A B
x : B
this : IsFractionRing B L
⊢ (algebraMap K L).comp ↑(FractionRing.algEquiv A K).toRingEquiv =
    (↑(FractionRing.algEquiv B L).toRingEquiv).comp (algebraMap (FractionRing A) (FractionRing B))
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: case inr
K : Type u_1
inst✝ : Field K
x✝ : realSpace K
h : (∀ (x : { w // w.IsReal }), x✝ ↑x = 0 x) ∧ ∀ (x : { w // w.IsComplex }), ↑(x✝ ↑x) = 0 x
w : InfinitePlace K
hw : w.IsComplex
⊢ x✝ w = 0 w

Tactic:
· exact Complex.ofReal_inj.mp <| h.2 ⟨w, hw⟩

Goal state after:
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
P Q : Ideal B
hPp : P.IsPrime
hp : P.LiesOver p
hQp : Q.IsPrime
inst✝⁴ : Q.LiesOver p
G : Type u_3
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : MulSemiringAction G B
inst✝ : IsGaloisGroup G A B
⊢ P.ramificationIdx A = Q.ramificationIdx A

Tactic:
by
  rcases exists_smul_eq_of_isGaloisGroup p P Q G with ⟨σ, rfl⟩
  rw [ramificationIdx_smul]

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

Goal state before:
pp: case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
h_nz : N ≠ 0
h₂ : 1 < 3 * π / 4
h✝ : 1 < finrank ℚ K
h : Real.logb (3 * π / 4) (9 / 4 * ↑N) < ↑(finrank ℚ K)
⊢ ↑↑N ≤ 4 / 9 * (9 / 4 * ↑N)

Tactic:
← mul_assoc,

Goal state after:
case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
h_nz : N ≠ 0
h₂ : 1 < 3 * π / 4
h✝ : 1 < finrank ℚ K
h : Real.logb (3 * π / 4) (9 / 4 * ↑N) < ↑(finrank ℚ K)
⊢ ↑↑N ≤ 4 / 9 * (9 / 4) * ↑N
Module: Mathlib.RingTheory.Ideal.Quotient.Index

Goal state before:
pp: case intro
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Ideal R
N : Submodule R M
inst✝ : Finite (R ⧸ I)
s : Finset M
hs : span R ↑s = N
val✝ : Fintype (R ⧸ I)
⊢ (I • N).toAddSubgroup.index ≤ (toAddSubgroup I).index ^ s.card * N.toAddSubgroup.index

Tactic:
rw [← AddSubgroup.relIndex_mul_index
    (H := (I • N).toAddSubgroup) (K := N.toAddSubgroup) Submodule.smul_le_right]

Goal state after:
case intro
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Ideal R
N : Submodule R M
inst✝ : Finite (R ⧸ I)
s : Finset M
hs : span R ↑s = N
val✝ : Fintype (R ⧸ I)
⊢ (I • N).toAddSubgroup.relIndex N.toAddSubgroup * N.toAddSubgroup.index ≤
    (toAddSubgroup I).index ^ s.card * N.toAddSubgroup.index
Module: Mathlib.RingTheory.Ideal.Quotient.Index

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Ideal R
N : Submodule R M
inst✝ : Finite (R ⧸ I)
s : Finset M
hs : span R ↑s = N
val✝ : Fintype (R ⧸ I)
e : (↥N ⧸ comap N.subtype (I • N)) ≃ₗ[R] (R ⧸ I) ⊗[R] ↥N :=
  (comap N.subtype (I • N)).quotEquivOfEq (I • ⊤) ⋯ ≪≫ₗ (quotTensorEquivQuotSMul (↥N) I).symm
H : (Finsupp.linearCombination R Subtype.val).range = N
c : ↥s →₀ R
⊢ ∃ y, (Finsupp.linearCombination R Subtype.val) y = (Finsupp.linearCombination R Subtype.val) c

Tactic:
exact exists_apply_eq_apply _ _

Goal state after:
Module: Mathlib.RingTheory.FractionalIdeal.Extended

Goal state before:
pp: case refine_2
A : Type u_1
inst✝⁷ : CommRing A
B : Type u_2
inst✝⁶ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝² : CommRing L
inst✝¹ : Algebra B L
inst✝ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I J : FractionalIdeal M K
i : K
hi : i ∈ ↑I
j : K
hj : j ∈ ↑J
h :
  (IsLocalization.map L f hf) i * (IsLocalization.map L f hf) j ∈
    ⇑(IsLocalization.map L f hf) '' ↑I * ⇑(IsLocalization.map L f hf) '' ↑J
⊢ (IsLocalization.map L f hf) i * (IsLocalization.map L f hf) j ∈ ↑(span B (⇑(IsLocalization.map L f hf) '' ↑(I * J)))

Tactic:
exact Submodule.subset_span ⟨i * j, mul_mem_mul hi hj, by simp⟩

Goal state after:
Module: Mathlib.RingTheory.Ideal.Int

Goal state before:
pp: n : ℕ
⊢ Nat.card (ℤ ⧸ Ideal.span {↑n}) = n

Tactic:
by
  simp [← Submodule.cardQuot_apply, ← Ideal.absNorm_apply]

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Instances

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : CommRing T
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : IsDomain T
inst✝⁸ : Algebra R S
P : Ideal R
inst✝⁷ : P.IsPrime
inst✝⁶ : FaithfulSMul R S
inst✝⁵ : Algebra S T
inst✝⁴ : Algebra R T
inst✝³ : IsScalarTower R S T
inst✝² : IsTorsionFree R T
inst✝¹ : IsTorsionFree S T
inst✝ : Algebra.IsSeparable L F
⊢ P.primeCompl ≤ R⁰

Tactic:
exact fun _ h ↦ mem_nonZeroDivisors_of_ne_zero <| ne_of_mem_of_not_mem h <| by simp

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

Goal state before:
pp: case refine_4
K : Type u_1
𝒪 : Type u_2
inst✝⁷ : Field K
inst✝⁶ : NumberField K
inst✝⁵ : CommRing 𝒪
inst✝⁴ : Algebra 𝒪 K
inst✝³ : IsFractionRing 𝒪 K
inst✝² : IsDedekindDomain 𝒪
inst✝¹ : CharZero 𝒪
inst✝ : Module.Finite ℤ 𝒪
this✝ :
  (↥↑1 ⧸ Submodule.comap (↑1).subtype ↑↑(differentIdeal ℤ 𝒪)) ≃ₗ[𝒪]
    ↥↑(↑(differentIdeal ℤ 𝒪))⁻¹ ⧸ Submodule.comap (↑(↑(differentIdeal ℤ 𝒪))⁻¹).subtype ↑1
this :
  Nat.card (↥↑1 ⧸ Submodule.comap (↑1).subtype ↑↑(differentIdeal ℤ 𝒪)) =
    Nat.card (↥↑(↑(differentIdeal ℤ 𝒪))⁻¹ ⧸ Submodule.comap (↑(↑(differentIdeal ℤ 𝒪))⁻¹).subtype ↑1)
b : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K := integralBasis K
b' : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K := (Algebra.traceForm ℚ K).dualBasis ⋯ b
hb : Submodule.span ℤ (Set.range ⇑b) = Submodule.restrictScalars ℤ 1
⊢ |(b'.toMatrix ⇑b).det| = |↑(Algebra.traceMatrix ℤ ⇑(RingOfIntegers.basis K)).det|

Tactic:
← eq_intCast (algebraMap ℤ ℚ),

Goal state after:
case refine_4
K : Type u_1
𝒪 : Type u_2
inst✝⁷ : Field K
inst✝⁶ : NumberField K
inst✝⁵ : CommRing 𝒪
inst✝⁴ : Algebra 𝒪 K
inst✝³ : IsFractionRing 𝒪 K
inst✝² : IsDedekindDomain 𝒪
inst✝¹ : CharZero 𝒪
inst✝ : Module.Finite ℤ 𝒪
this✝ :
  (↥↑1 ⧸ Submodule.comap (↑1).subtype ↑↑(differentIdeal ℤ 𝒪)) ≃ₗ[𝒪]
    ↥↑(↑(differentIdeal ℤ 𝒪))⁻¹ ⧸ Submodule.comap (↑(↑(differentIdeal ℤ 𝒪))⁻¹).subtype ↑1
this :
  Nat.card (↥↑1 ⧸ Submodule.comap (↑1).subtype ↑↑(differentIdeal ℤ 𝒪)) =
    Nat.card (↥↑(↑(differentIdeal ℤ 𝒪))⁻¹ ⧸ Submodule.comap (↑(↑(differentIdeal ℤ 𝒪))⁻¹).subtype ↑1)
b : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K := integralBasis K
b' : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K := (Algebra.traceForm ℚ K).dualBasis ⋯ b
hb : Submodule.span ℤ (Set.range ⇑b) = Submodule.restrictScalars ℤ 1
⊢ |(b'.toMatrix ⇑b).det| = |(algebraMap ℤ ℚ) (Algebra.traceMatrix ℤ ⇑(RingOfIntegers.basis K)).det|
Module: Mathlib.NumberTheory.NumberField.Discriminant.Different

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
L : Type u_3
inst✝² : Field L
inst✝¹ : NumberField L
inst✝ : Algebra K L
⊢ discr K ^ finrank K L ∣
    ↑(Ideal.absNorm (differentIdeal (𝓞 K) (𝓞 L))) * (discr K ^ finrank K L * (discr K).sign ^ finrank K L)

Tactic:
← mul_assoc,

Goal state after:
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
L : Type u_3
inst✝² : Field L
inst✝¹ : NumberField L
inst✝ : Algebra K L
⊢ discr K ^ finrank K L ∣
    ↑(Ideal.absNorm (differentIdeal (𝓞 K) (𝓞 L))) * discr K ^ finrank K L * (discr K).sign ^ finrank K L
Module: Mathlib.NumberTheory.NumberField.Discriminant.Different

Goal state before:
pp: K : Type u_1
𝒪 : Type u_2
inst✝⁴ : Field K
inst✝³ : NumberField K
inst✝² : CommRing 𝒪
inst✝¹ : Algebra 𝒪 K
inst✝ : IsIntegralClosure 𝒪 ℤ K
p : ℤ
hp : Prime p
this : IsDomain 𝒪
⊢ ¬p ∣ discr K ↔ ∀ (P : Ideal 𝒪) (x : P.IsMaximal), P.LiesOver (Ideal.span {p}) → Algebra.IsUnramifiedAt ℤ P

Tactic:
have := IsIntegralClosure.isDedekindDomain ℤ ℚ K 𝒪

Goal state after:
K : Type u_1
𝒪 : Type u_2
inst✝⁴ : Field K
inst✝³ : NumberField K
inst✝² : CommRing 𝒪
inst✝¹ : Algebra 𝒪 K
inst✝ : IsIntegralClosure 𝒪 ℤ K
p : ℤ
hp : Prime p
this✝ : IsDomain 𝒪
this : IsDedekindDomain 𝒪
⊢ ¬p ∣ discr K ↔ ∀ (P : Ideal 𝒪) (x : P.IsMaximal), P.LiesOver (Ideal.span {p}) → Algebra.IsUnramifiedAt ℤ P
Module: Mathlib.NumberTheory.NumberField.Discriminant.Different

Goal state before:
pp: K : Type u_1
𝒪 : Type u_2
inst✝⁴ : Field K
inst✝³ : NumberField K
inst✝² : CommRing 𝒪
inst✝¹ : Algebra 𝒪 K
inst✝ : IsIntegralClosure 𝒪 ℤ K
p : ℤ
hp : Prime p
this : IsDomain 𝒪
⊢ ¬p ∣ discr K ↔ Algebra.IsUnramifiedIn 𝒪 (Ideal.span {p})

Tactic:
have := IsIntegralClosure.isDedekindDomain ℤ ℚ K 𝒪

Goal state after:
K : Type u_1
𝒪 : Type u_2
inst✝⁴ : Field K
inst✝³ : NumberField K
inst✝² : CommRing 𝒪
inst✝¹ : Algebra 𝒪 K
inst✝ : IsIntegralClosure 𝒪 ℤ K
p : ℤ
hp : Prime p
this✝ : IsDomain 𝒪
this : IsDedekindDomain 𝒪
⊢ ¬p ∣ discr K ↔ Algebra.IsUnramifiedIn 𝒪 (Ideal.span {p})
Module: Mathlib.NumberTheory.NumberField.Discriminant.Different

Goal state before:
pp: K : Type u_1
𝒪 : Type u_2
inst✝⁴ : Field K
inst✝³ : NumberField K
inst✝² : CommRing 𝒪
inst✝¹ : Algebra 𝒪 K
inst✝ : IsIntegralClosure 𝒪 ℤ K
p : ℤ
hp : Prime p
this : IsDomain 𝒪
⊢ ¬p ∣ discr K ↔ ∀ (P : Ideal 𝒪) (x : P.IsPrime), ↑p ∈ P → Algebra.IsUnramifiedAt ℤ P

Tactic:
have := IsIntegralClosure.isDedekindDomain ℤ ℚ K 𝒪

Goal state after:
K : Type u_1
𝒪 : Type u_2
inst✝⁴ : Field K
inst✝³ : NumberField K
inst✝² : CommRing 𝒪
inst✝¹ : Algebra 𝒪 K
inst✝ : IsIntegralClosure 𝒪 ℤ K
p : ℤ
hp : Prime p
this✝ : IsDomain 𝒪
this : IsDedekindDomain 𝒪
⊢ ¬p ∣ discr K ↔ ∀ (P : Ideal 𝒪) (x : P.IsPrime), ↑p ∈ P → Algebra.IsUnramifiedAt ℤ P