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

Goal state before:
pp: case inr
Λ : ℂ → ℂ
hf : ∀ (s : ℂ), s ≠ 0 → s ≠ 1 → DifferentiableAt ℂ Λ s
L : ℂ
h_lim : Tendsto (fun s ↦ s * Λ s) (𝓝[≠] 0) (𝓝 L)
claim : ∀ (t : ℂ), t ≠ 0 → t ≠ 1 → DifferentiableAt ℂ (fun u ↦ Λ u / u.Gammaℝ) t
claim2 : Tendsto (fun s ↦ Λ s / s.Gammaℝ) (𝓝[≠] 0) (𝓝 (L / 2))
hs' : 0 ≠ 1
S_nhds : {1}ᶜ ∈ 𝓝 0
⊢ (fun _x ↦ 1) =o[𝓝[≠] 0] fun z ↦ z⁻¹

Tactic:
rw [isLittleO_iff_tendsto']

Goal state after:
case inr
Λ : ℂ → ℂ
hf : ∀ (s : ℂ), s ≠ 0 → s ≠ 1 → DifferentiableAt ℂ Λ s
L : ℂ
h_lim : Tendsto (fun s ↦ s * Λ s) (𝓝[≠] 0) (𝓝 L)
claim : ∀ (t : ℂ), t ≠ 0 → t ≠ 1 → DifferentiableAt ℂ (fun u ↦ Λ u / u.Gammaℝ) t
claim2 : Tendsto (fun s ↦ Λ s / s.Gammaℝ) (𝓝[≠] 0) (𝓝 (L / 2))
hs' : 0 ≠ 1
S_nhds : {1}ᶜ ∈ 𝓝 0
⊢ Tendsto (fun x ↦ 1 / x⁻¹) (𝓝[≠] 0) (𝓝 0)

case inr
Λ : ℂ → ℂ
hf : ∀ (s : ℂ), s ≠ 0 → s ≠ 1 → DifferentiableAt ℂ Λ s
L : ℂ
h_lim : Tendsto (fun s ↦ s * Λ s) (𝓝[≠] 0) (𝓝 L)
claim : ∀ (t : ℂ), t ≠ 0 → t ≠ 1 → DifferentiableAt ℂ (fun u ↦ Λ u / u.Gammaℝ) t
claim2 : Tendsto (fun s ↦ Λ s / s.Gammaℝ) (𝓝[≠] 0) (𝓝 (L / 2))
hs' : 0 ≠ 1
S_nhds : {1}ᶜ ∈ 𝓝 0
⊢ ∀ᶠ (x : ℂ) in 𝓝[≠] 0, x⁻¹ = 0 → 1 = 0
Module: Mathlib.NumberTheory.FLT.Four

Goal state before:
pp: a b c : ℤ
h : Fermat42 a b c
⊢ 0 < a ^ 4 + b ^ 4

Tactic:
(by ring : a ^ 4 + b ^ 4 = (a ^ 2) ^ 2 + (b ^ 2) ^ 2)

Goal state after:
a b c : ℤ
h : Fermat42 a b c
⊢ 0 < (a ^ 2) ^ 2 + (b ^ 2) ^ 2
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: a : ℝ
s : ℂ
hs : 1 < s.re
n : ℤ
⊢ 0 < (s + 1).re

Tactic:
add_re,

Goal state after:
a : ℝ
s : ℂ
hs : 1 < s.re
n : ℤ
⊢ 0 < s.re + re 1
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
⊢ False

Tactic:
have h4 : 0 < m := by
    apply lt_of_le_of_ne ht6
    rintro rfl
    lia

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
⊢ False
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
⊢ 0 < x ^ 2 + y ^ 2

Tactic:
have hc' : Int.gcd x y ≠ 0 := by
    rw [hc]
    exact one_ne_zero

Goal state after:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hc' : x.gcd y ≠ 0
⊢ 0 < x ^ 2 + y ^ 2
Module: Mathlib.RingTheory.Polynomial.Wronskian

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a : R[X]
⊢ wronskian 0 a = 0

Tactic:
rw [← wronskianBilin_apply 0 a, map_zero]

Goal state after:
R : Type u_1
inst✝ : CommRing R
a : R[X]
⊢ 0 a = 0
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
ha : IsRadical a
⊢ (normalizedFactors a).toFinset.val = normalizedFactors a

Tactic:
Multiset.toFinset_val,

Goal state after:
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
ha : IsRadical a
⊢ (normalizedFactors a).dedup = normalizedFactors a
Module: Mathlib.NumberTheory.PythagoreanTriples

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

Tactic:
let q := (circleEquivGen hQ).symm ⟨⟨v, w⟩, hp⟩

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

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

Tactic:
mul_eq_zero_iff_left (C_ne_zero.mpr hw),

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

Tactic:
ch0

Goal state after:
k : Type u_1
inst✝ : Field k
p q r : ℕ
a b c : k[X]
u v w : k
heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0
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
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
ch0 : ringChar k = 0
da : derivative a = 0
n : ℕ
⊢ 0 ∣ n → n = 0
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✝² : IsDomain K
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ R
I : FractionalIdeal R⁰ K
bI : Basis ι ℤ ↥↑I
⊢ |(Basis.localizationLocalization ℚ ℤ⁰ K b).det (Subtype.val ∘ ⇑bI)| = absNorm I

Tactic:
have := IsFractionRing.nontrivial R K
  let b₀ : Basis ι ℚ K := b.localizationLocalization ℚ ℤ⁰ K
  let bI.num : Basis ι ℤ I.num := bI.map
      ((equivNum (nonZeroDivisors.coe_ne_zero _)).restrictScalars ℤ)
  rw [absNorm_eq, ← Ideal.natAbs_det_basis_change b I.num bI.num, Nat.cast_natAbs, Int.cast_abs,
    Int.cast_abs, Basis.det_apply, Basis.det_apply]
  change _ = |algebraMap ℤ ℚ _| / _
  rw [RingHom.map_det, show RingHom.mapMatrix (algebraMap ℤ ℚ) (b.toMatrix ((↑) ∘ bI.num)) =
      b₀.toMatrix ((algebraMap R K (den I : R)) • ((↑) ∘ bI)) by
    ext : 2
    simp_rw [bI.num, RingHom.mapMatrix_apply, Matrix.map_apply, Basis.toMatrix_apply,
      ← Basis.localizationLocalization_repr_algebraMap ℚ ℤ⁰ K, Function.comp_apply,
      Basis.map_apply, LinearEquiv.restrictScalars_apply, equivNum_apply, Submonoid.smul_def,
      Algebra.smul_def]
    rfl]
  rw [Basis.toMatrix_smul, Matrix.det_mul, abs_mul, ← Algebra.norm_eq_matrix_det,
    Algebra.norm_localization ℤ ℤ⁰, show (Algebra.norm ℤ (den I : R) : ℚ) =
    algebraMap ℤ ℚ (Algebra.norm ℤ (den I : R)) by rfl, mul_div_assoc, mul_div_cancel₀ _ (by
    rw [ne_eq, abs_eq_zero, IsFractionRing.to_map_eq_zero_iff, Algebra.norm_eq_zero_iff_of_basis b]
    exact nonZeroDivisors.coe_ne_zero _)]

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

Goal state before:
pp: 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 : 1 ≤ ↑|(Algebra.norm ℚ) ↑a|
⊢ 1 ≤ w ↑a

Tactic:
contrapose! this
    rw [← InfinitePlace.prod_eq_abs_norm, ← Finset.prod_const_one]
    refine Finset.prod_lt_prod_of_nonempty (fun _ _ ↦ ?_) (fun z _ ↦ ?_) Finset.univ_nonempty
    · exact pow_pos (pos_iff.mpr ((Subalgebra.coe_eq_zero _).not.mpr ha)) _
    · refine pow_lt_one₀ (apply_nonneg _ _) ?_ (by rw [mult]; split_ifs <;> norm_num)
      by_cases hz : z = w
      · rwa [hz]
      · 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
this : orderOf ⟨-1, ⋯⟩ = 2
⊢ Even (torsionOrder K)

Tactic:
rw [even_iff_two_dvd, ← this]
    apply orderOf_dvd_natCard

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

Goal state before:
pp: case e'_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : w.IsComplex
⊢ card { x // mkComplex x = ⟨w, hw⟩ } = card { x // mk x = w }

Tactic:
refine Fintype.card_congr (Equiv.ofBijective ?_ ⟨fun _ _ h => ?_, fun ⟨φ, hφ⟩ => ?_⟩)

Goal state after:
case e'_2.refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : w.IsComplex
⊢ { x // mkComplex x = ⟨w, hw⟩ } → { x // mk x = w }

case e'_2.refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : w.IsComplex
x✝¹ x✝ : { x // mkComplex x = ⟨w, hw⟩ }
h : ?e'_2.refine_1 x✝¹ = ?e'_2.refine_1 x✝
⊢ x✝¹ = x✝

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
⊢ ∃ a, ?e'_2.refine_1 a = ⟨φ, hφ⟩
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝ : Field K
f : InfinitePlace K → ℝ≥0
x : K
⊢ (mixedEmbedding K) x ∈ convexBodyLT K f ↔ ∀ (w : InfinitePlace K), w x < ↑(f w)

Tactic:
mixedEmbedding,

Goal state after:
K : Type u_1
inst✝ : Field K
f : InfinitePlace K → ℝ≥0
x : K
⊢ ((RingHom.pi fun w ↦ embedding_of_isReal ⋯).prod (RingHom.pi fun w ↦ (↑w).embedding)) x ∈ convexBodyLT K f ↔
    ∀ (w : InfinitePlace K), w x < ↑(f w)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
inst✝ : NumberField K
⊢ ↑(convexBodyLTFactor K) * ((∏ x, ENNReal.ofReal ↑(f ↑x)) * ∏ x, ENNReal.ofReal ↑(f ↑x) ^ 2) =
    ↑(convexBodyLTFactor K) * ↑(∏ w, f w ^ w.mult)

Tactic:
by
      simp_rw [prod_eq_prod_mul_prod, coe_mul, ofNNReal_finsetProd, mult_isReal, mult_isComplex,
        pow_one, ENNReal.coe_pow, ofReal_coe_nnreal]

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 }
x : K
⊢ (mixedEmbedding K) x ∈ convexBodyLT' K f w₀ ↔
    (∀ (w : InfinitePlace K), w ≠ ↑w₀ → w x < ↑(f w)) ∧
      |((↑w₀).embedding x).re| < 1 ∧ |((↑w₀).embedding x).im| < ↑(f ↑w₀) ^ 2

Tactic:
mixedEmbedding,

Goal state after:
K : Type u_1
inst✝ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
x : K
⊢ ((RingHom.pi fun w ↦ embedding_of_isReal ⋯).prod (RingHom.pi fun w ↦ (↑w).embedding)) x ∈ convexBodyLT' K f w₀ ↔
    (∀ (w : InfinitePlace K), w ≠ ↑w₀ → w x < ↑(f w)) ∧
      |((↑w₀).embedding x).re| < 1 ∧ |((↑w₀).embedding x).im| < ↑(f ↑w₀) ^ 2
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
a' b' : k[X]
d : k[X] := gcd a b
heq : d ^ n * (a' ^ n + b' ^ n) = c ^ n
eq_a : a = d * a'
eq_b : b = d * b'
hd : d ≠ 0
⊢ ∃ d a' b' c', (a = a' * d ∧ b = b' * d ∧ c = c' * d) ∧ IsUnit a' ∧ IsUnit b' ∧ IsUnit c'

Tactic:
obtain ⟨c', eq_c⟩ : ∃ c', c = d * c' :=
    (IsIntegrallyClosed.pow_dvd_pow_iff (by lia)).mp ⟨_, heq.symm⟩

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
a' b' : k[X]
d : k[X] := gcd a b
heq : d ^ n * (a' ^ n + b' ^ n) = c ^ n
eq_a : a = d * a'
eq_b : b = d * b'
hd : d ≠ 0
c' : k[X]
eq_c : c = d * c'
⊢ ∃ d a' b' c', (a = a' * d ∧ b = b' * d ∧ c = c' * d) ∧ IsUnit a' ∧ IsUnit b' ∧ IsUnit c'
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: case inl.refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
r : ℝ
hr : r < 0
φ : K →+* ℂ
⊢ ¬∀ (φ : K →+* ℂ), ‖φ x‖ ≤ r

Tactic:
· exact fun h => hr.not_ge (le_trans (norm_nonneg _) (h φ))

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
x : K
w : { w // w.IsReal }
⊢ ((mixedEmbedding K) x).1 w = (embedding_of_isReal ⋯) x

Tactic:
mixedEmbedding,

Goal state after:
K : Type u_1
inst✝ : Field K
x : K
w : { w // w.IsReal }
⊢ (((RingHom.pi fun w ↦ embedding_of_isReal ⋯).prod (RingHom.pi fun w ↦ (↑w).embedding)) x).1 w =
    (embedding_of_isReal ⋯) x
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
x : K
w : { w // w.IsComplex }
⊢ ((mixedEmbedding K) x).2 w = (↑w).embedding x

Tactic:
mixedEmbedding,

Goal state after:
K : Type u_1
inst✝ : Field K
x : K
w : { w // w.IsComplex }
⊢ (((RingHom.pi fun w ↦ embedding_of_isReal ⋯).prod (RingHom.pi fun w ↦ (↑w).embedding)) x).2 w = (↑w).embedding x
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
w w' : InfinitePlace K
⊢ w' ∈ MulAction.orbit Gal(K/k) w ↔ w.comap (algebraMap k K) = w'.comap (algebraMap k K)

Tactic:
refine ⟨?_, exists_smul_eq_of_comap_eq⟩

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
w w' : InfinitePlace K
⊢ w' ∈ MulAction.orbit Gal(K/k) w → w.comap (algebraMap k K) = w'.comap (algebraMap k K)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
w : InfinitePlace K
x : K
⊢ (if hw : w.IsReal then ‖((mixedEmbedding K) x).1 ⟨w, hw⟩‖ else ‖((mixedEmbedding K) x).2 ⟨w, ⋯⟩‖) = w x

Tactic:
mixedEmbedding,

Goal state after:
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
x : K
⊢ (if hw : w.IsReal then
      ‖(((RingHom.pi fun w ↦ embedding_of_isReal ⋯).prod (RingHom.pi fun w ↦ (↑w).embedding)) x).1 ⟨w, hw⟩‖
    else ‖(((RingHom.pi fun w ↦ embedding_of_isReal ⋯).prod (RingHom.pi fun w ↦ (↑w).embedding)) x).2 ⟨w, ⋯⟩‖) =
    w x
Module: Mathlib.RingTheory.Invariant.Galois

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Field K
inst✝¹² : Field L
inst✝¹¹ : Algebra A K
inst✝¹⁰ : Algebra B L
inst✝⁹ : IsFractionRing A K
inst✝⁸ : IsFractionRing B L
inst✝⁷ : Algebra A B
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra A L
inst✝⁴ : IsScalarTower A K L
inst✝³ : IsScalarTower A B L
inst✝² : IsIntegrallyClosed A
inst✝¹ : IsIntegralClosure B A L
inst✝ : FiniteDimensional K L
h✝ : IsGalois K L
h : IntermediateField.fixedField ⊤ = ⊥
this : MulSemiringAction Gal(L/K) B := IsIntegralClosure.MulSemiringAction A K L B
b : B
hb : (algebraMap B L) b ∈ IntermediateField.fixedField ⊤
⊢ ∃ a, (algebraMap A B) a = b

Tactic:
rw [h, IntermediateField.mem_bot] at hb

Goal state after:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Field K
inst✝¹² : Field L
inst✝¹¹ : Algebra A K
inst✝¹⁰ : Algebra B L
inst✝⁹ : IsFractionRing A K
inst✝⁸ : IsFractionRing B L
inst✝⁷ : Algebra A B
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra A L
inst✝⁴ : IsScalarTower A K L
inst✝³ : IsScalarTower A B L
inst✝² : IsIntegrallyClosed A
inst✝¹ : IsIntegralClosure B A L
inst✝ : FiniteDimensional K L
h✝ : IsGalois K L
h : IntermediateField.fixedField ⊤ = ⊥
this : MulSemiringAction Gal(L/K) B := IsIntegralClosure.MulSemiringAction A K L B
b : B
hb : (algebraMap B L) b ∈ Set.range ⇑(algebraMap K L)
⊢ ∃ a, (algebraMap A B) a = b
Module: Mathlib.RingTheory.DedekindDomain.PID

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
I : (FractionalIdeal S A)ˣ
v : A
hv : v ∈ ↑I⁻¹
hinv : ↑I * ↑I⁻¹ = 1
J : Submodule R R := Submodule.comap (Algebra.linearMap R A) (↑↑I * (R ∙ v))
h : J = ⊤
hJ : IsLocalization.coeSubmodule A J = ↑↑I * (R ∙ v)
this : 1 ∈ ↑↑I * (R ∙ v)
w : A
hw : w ∈ ↑↑I
hvw : w * v = 1
⊢ ↑↑I = R ∙ w

Tactic:
rw [← FractionalIdeal.coe_spanSingleton S, ← inv_inv I, eq_comm]

Goal state after:
R : Type u_2
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
I : (FractionalIdeal S A)ˣ
v : A
hv : v ∈ ↑I⁻¹
hinv : ↑I * ↑I⁻¹ = 1
J : Submodule R R := Submodule.comap (Algebra.linearMap R A) (↑↑I * (R ∙ v))
h : J = ⊤
hJ : IsLocalization.coeSubmodule A J = ↑↑I * (R ∙ v)
this : 1 ∈ ↑↑I * (R ∙ v)
w : A
hw : w ∈ ↑↑I
hvw : w * v = 1
⊢ ↑(spanSingleton S w) = ↑↑I⁻¹⁻¹
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
⊢ IsScalarTower Rₚ Sₚ Tₚ

Tactic:
refine ⟨fun a b c ↦ a.ind fun ⟨a₁, a₂⟩ ↦ ?_⟩
  have : a₂.val ≠ 0 := nonZeroDivisors.ne_zero <| Ideal.primeCompl_le_nonZeroDivisors P <| a₂.prop
  rw [← smul_right_inj this, ← _root_.smul_assoc (M := R) (N := Sₚ), ← _root_.smul_assoc (M := R)
    (α := Sₚ), ← _root_.smul_assoc (M := R) (α := Tₚ), Localization.smul_mk, smul_eq_mul,
    Localization.mk_eq_mk', IsLocalization.mk'_mul_cancel_left, algebraMap_smul, algebraMap_smul,
    _root_.smul_assoc]

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

Goal state before:
pp: case refine_3
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
⊢ (↑(FractionalIdeal.dual ℤ ℚ 1)).toAddSubgroup = AddSubgroup.closure (Set.range ⇑b')

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'.det ⇑b| = |↑(discr K)|

Tactic:
· apply AddSubgroup.toIntSubmodule.injective
    rw [AddSubgroup.toIntSubmodule_closure, ← LinearMap.BilinForm.dualSubmodule_span_of_basis, hb]
    simp

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'.det ⇑b| = |↑(discr K)|
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 𝒪
this✝¹ : IsDedekindDomain 𝒪
this✝ : IsFractionRing 𝒪 K
this : Module.Finite ℤ 𝒪
⊢ ¬p ∣ discr K ↔ ∀ (P : Ideal 𝒪) (x : P.IsMaximal), P.LiesOver (Ideal.span {p}) → Algebra.IsUnramifiedAt ℤ P

Tactic:
have := CharZero.of_module (R := 𝒪) 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 𝒪
this✝¹ : IsFractionRing 𝒪 K
this✝ : Module.Finite ℤ 𝒪
this : CharZero 𝒪
⊢ ¬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 𝒪
this : IsDedekindDomain 𝒪
⊢ ¬p ∣ discr K ↔ Algebra.IsUnramifiedIn 𝒪 (Ideal.span {p})

Tactic:
have := CharZero.of_module (R := 𝒪) 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 𝒪
this : CharZero 𝒪
⊢ ¬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 𝒪
this : IsDedekindDomain 𝒪
⊢ ¬p ∣ discr K ↔ ∀ (P : Ideal 𝒪) (x : P.IsPrime), ↑p ∈ P → Algebra.IsUnramifiedAt ℤ P

Tactic:
have := CharZero.of_module (R := 𝒪) 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 𝒪
this : CharZero 𝒪
⊢ ¬p ∣ discr K ↔ ∀ (P : Ideal 𝒪) (x : P.IsPrime), ↑p ∈ P → Algebra.IsUnramifiedAt ℤ P