mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Polynomial.GaussLemma

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
f : R[X]
hf : f.Monic
g : K[X]
hg : g ∣ map (algebraMap R K) f
⊢ ∃ g', map (algebraMap R K) g' * C g.leadingCoeff = g

Tactic:
by
  have g_ne_0 : g ≠ 0 := ne_zero_of_dvd_ne_zero (Monic.ne_zero <| hf.map (algebraMap R K)) hg
  suffices lem : ∃ g' : R[X], g'.map (algebraMap R K) = g * C g.leadingCoeff⁻¹ by
    obtain ⟨g', hg'⟩ := lem
    use g'
    rw [hg', mul_assoc, ← C_mul, inv_mul_cancel₀ (leadingCoeff_ne_zero.mpr g_ne_0), C_1, mul_one]
  have g_mul_dvd : g * C g.leadingCoeff⁻¹ ∣ f.map (algebraMap R K) := by
    rwa [Associated.dvd_iff_dvd_left (show Associated (g * C g.leadingCoeff⁻¹) g from _)]
    rw [associated_mul_isUnit_left_iff]
    exact isUnit_C.mpr (inv_ne_zero <| leadingCoeff_ne_zero.mpr g_ne_0).isUnit
  let algeq :=
    (Subalgebra.equivOfEq _ _ <| integralClosure_eq_bot R _).trans
      (Algebra.botEquivOfInjective <| IsFractionRing.injective R <| K)
  have :
    (algebraMap R _).comp algeq.toAlgHom.toRingHom = (integralClosure R _).toSubring.subtype := by
    ext x; (conv_rhs => rw [← algeq.symm_apply_apply x]); rfl
  have H :=
    (mem_lifts _).1
      (integralClosure.mem_lifts_of_monic_of_dvd_map K hf (monic_mul_leadingCoeff_inv g_ne_0)
        g_mul_dvd)
  refine ⟨map algeq.toAlgHom.toRingHom ?_, ?_⟩
  · use! Classical.choose H
  · rw [map_map, this]
    exact Classical.choose_spec H

Goal state after:
Module: Mathlib.RingTheory.Polynomial.GaussLemma

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : IsGCDMonoid R
f : R[X]
hf : f.IsPrimitive
g : K[X]
this : NormalizedGCDMonoid R := ⋯.some
x✝ : g * map (algebraMap R K) f ∈ lifts (algebraMap R K)
k : R[X]
hk : map (algebraMap R K) k = g * map (algebraMap R K) f
g' : R[X] := integerNormalization R⁰ g
b : R
hb₁ : b ∈ R⁰
hb₂ : map (algebraMap R K) g' = b • g
g'_mul_f : g' * f = b • k
⊢ g ∈ lifts (algebraMap R K)

Tactic:
apply_fun content at g'_mul_f

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : IsGCDMonoid R
f : R[X]
hf : f.IsPrimitive
g : K[X]
this : NormalizedGCDMonoid R := ⋯.some
x✝ : g * map (algebraMap R K) f ∈ lifts (algebraMap R K)
k : R[X]
hk : map (algebraMap R K) k = g * map (algebraMap R K) f
g' : R[X] := integerNormalization R⁰ g
b : R
hb₁ : b ∈ R⁰
hb₂ : map (algebraMap R K) g' = b • g
g'_mul_f : (g' * f).content = (b • k).content
⊢ g ∈ lifts (algebraMap R K)
Module: Mathlib.RingTheory.Trace.Defs

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✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Free R S
inst✝² : Free R T
inst✝¹ : Module.Finite R S
inst✝ : Module.Finite R T
x : S × T
⊢ (trace R (S × T)) x = (trace R S) x.1 + (trace R T) x.2

Tactic:
by
  let f := (lmul R S).toLinearMap.prodMap (lmul R T).toLinearMap
  have : (lmul R (S × T)).toLinearMap = (prodMapLinear R S T S T R).comp f :=
    LinearMap.ext₂ Prod.mul_def
  simp_rw [trace, this]
  exact trace_prodMap' _ _

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: F : Type u
E : Type v
inst✝⁵ : Field F
inst✝⁴ : Field E
inst✝³ : Algebra F E
L : Type w
inst✝² : Field L
inst✝¹ : IsAlgClosed L
inst✝ : Nonempty (E →+* L)
h : Function.Injective fun f ↦ f.comp (algebraMap F E)
⊢ Subsingleton (Emb F E) ∧ Nonempty (Emb F E)

Tactic:
let := (Classical.arbitrary (E →+* L)).toAlgebra

Goal state after:
F : Type u
E : Type v
inst✝⁵ : Field F
inst✝⁴ : Field E
inst✝³ : Algebra F E
L : Type w
inst✝² : Field L
inst✝¹ : IsAlgClosed L
inst✝ : Nonempty (E →+* L)
h : Function.Injective fun f ↦ f.comp (algebraMap F E)
this : Algebra E L := (Classical.arbitrary (E →+* L)).toAlgebra
⊢ Subsingleton (Emb F E) ∧ Nonempty (Emb F E)
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
x : ZMod n
⊢ x = ↑x.valMinAbs ∧ x.valMinAbs * 2 ∈ Set.Ioc (-↑n) ↑n

Tactic:
exact ⟨x.coe_valMinAbs.symm, x.valMinAbs_mem_Ioc⟩

Goal state after:
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: n : ℕ
a : ZMod n
ha : 2 * a.val ≠ n
⊢ (-a).valMinAbs = -a.valMinAbs

Tactic:
by
  rcases eq_zero_or_neZero n with rfl | h
  · rfl
  refine (valMinAbs_spec _ _).2 ⟨?_, ?_, ?_⟩
  · rw [Int.cast_neg, coe_valMinAbs]
  · rw [neg_mul, neg_lt_neg_iff]
    exact a.valMinAbs_mem_Ioc.2.lt_of_ne (mt a.valMinAbs_mul_two_eq_iff.1 ha)
  · linarith only [a.valMinAbs_mem_Ioc.1]

Goal state after:
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype R
f g : R[X]
hf2 : f.degree = 2
hg2 : g.degree = 2
hR : Fintype.card R % 2 = 1
this : DecidableEq R := Classical.decEq R
hd : Disjoint (image (fun x ↦ eval x f) univ) (image (fun x ↦ eval x (-g)) univ)
⊢ f.natDegree * #(image (fun x ↦ eval x f) univ) + (-g).natDegree * #(image (fun x ↦ eval x (-g)) univ) =
    2 * #(image (fun x ↦ eval x f) univ ∪ image (fun x ↦ eval x (-g)) univ)

Tactic:
by
        rw [card_union_of_disjoint hd]
        simp [natDegree_eq_of_degree_eq_some hf2, natDegree_eq_of_degree_eq_some hg2, mul_add]

Goal state after:
Module: Mathlib.FieldTheory.Galois.IsGaloisGroup

Goal state before:
pp: case inl
G : Type u_1
K : Type u_3
L : Type u_4
inst✝⁵ : Group G
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : MulSemiringAction G L
inst✝ : IsGaloisGroup G K L
val✝ : Fintype G
⊢ Nat.card G = finrank K L

pp: case inr
G : Type u_1
K : Type u_3
L : Type u_4
inst✝⁵ : Group G
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : MulSemiringAction G L
inst✝ : IsGaloisGroup G K L
hG : Infinite G
⊢ Nat.card G = finrank K L

Tactic:
· have : FaithfulSMul G L := faithful K
    rw [← IntermediateField.finrank_bot', ← fixedPoints_eq_bot G, Nat.card_eq_fintype_card]
    exact (FixedPoints.finrank_eq_card G L).symm

Goal state after:
case inr
G : Type u_1
K : Type u_3
L : Type u_4
inst✝⁵ : Group G
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : MulSemiringAction G L
inst✝ : IsGaloisGroup G K L
hG : Infinite G
⊢ Nat.card G = finrank K L
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: κ : Type w
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Fintype κ
b : κ → B
P : Matrix κ κ A
⊢ (traceMatrix A (b ᵥ* Pᵀ.map ⇑(algebraMap A B)))ᵀ = (P * traceMatrix A b * Pᵀ)ᵀ

Tactic:
traceMatrix_of_matrix_vecMul,

Goal state after:
κ : Type w
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Fintype κ
b : κ → B
P : Matrix κ κ A
⊢ (Pᵀᵀ * traceMatrix A b * Pᵀ)ᵀ = (P * traceMatrix A b * Pᵀ)ᵀ
Module: Mathlib.RingTheory.ZMod

Goal state before:
pp: n : ℕ
x✝ : ℤ
⊢ x✝ ∈ RingHom.ker (Int.castRingHom (ZMod n)) ↔ x✝ ∈ Ideal.span {↑n}

Tactic:
Ideal.mem_span_singleton,

Goal state after:
n : ℕ
x✝ : ℤ
⊢ x✝ ∈ RingHom.ker (Int.castRingHom (ZMod n)) ↔ ↑n ∣ x✝
Module: Mathlib.LinearAlgebra.Quotient.Pi

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝⁴ : CommRing R
Ms : ι → Type u_3
inst✝³ : (i : ι) → AddCommGroup (Ms i)
inst✝² : (i : ι) → Module R (Ms i)
p : (i : ι) → Submodule R (Ms i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : ((i : ι) → Ms i) ⧸ pi Set.univ p
x' : (i : ι) → Ms i
⊢ Quotient.mk (((lsum R Ms R) (single R Ms)) x') = Quotient.mk x'

Tactic:
lsum_single,

Goal state after:
ι : Type u_1
R : Type u_2
inst✝⁴ : CommRing R
Ms : ι → Type u_3
inst✝³ : (i : ι) → AddCommGroup (Ms i)
inst✝² : (i : ι) → Module R (Ms i)
p : (i : ι) → Submodule R (Ms i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : ((i : ι) → Ms i) ⧸ pi Set.univ p
x' : (i : ι) → Ms i
⊢ Quotient.mk (LinearMap.id x') = Quotient.mk x'
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: n p k : ℕ
inst✝ : Fact (Nat.Prime p)
hn : n = p ^ k
hn0 : n ≠ 0
this : NeZero n
a : ℕ
ha : (orderOf ↑a).Coprime n
h : ¬IsUnit (↑a - 1)
ha0 : a < 1
⊢ ↑a = 0

Tactic:
Nat.lt_one_iff.mp ha0,

Goal state after:
n p k : ℕ
inst✝ : Fact (Nat.Prime p)
hn : n = p ^ k
hn0 : n ≠ 0
this : NeZero n
a : ℕ
ha : (orderOf ↑a).Coprime n
h : ¬IsUnit (↑a - 1)
ha0 : a < 1
⊢ ↑0 = 0
Module: Mathlib.RingTheory.Norm.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Ring S
inst✝³ : Algebra R S
inst✝² : Nontrivial S
inst✝¹ : Free R S
inst✝ : Module.Finite R S
a✝ : Nontrivial R
⊢ (norm R) 0 = 0

Tactic:
rw [norm_apply, coe_lmul_eq_mul, map_zero, LinearMap.det_zero' (Module.Free.chooseBasis R S)]

Goal state after:
Module: Mathlib.RingTheory.Artinian.Ring

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst✝² : CommSemiring L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
⊢ Function.Surjective ⇑(algebraMap R L)

Tactic:
intro r'
  obtain ⟨r₁, s, rfl⟩ := IsLocalization.exists_mk'_eq S r'
  rsuffices ⟨r₂, h⟩ : ∃ r : R, IsLocalization.mk' L 1 s = algebraMap R L r
  · exact ⟨r₁ * r₂, by rw [IsLocalization.mk'_eq_mul_mk'_one, map_mul, h]⟩
  obtain ⟨n, r, hr⟩ := IsArtinian.exists_pow_succ_smul_dvd (s : R) (1 : R)
  use r
  rw [smul_eq_mul, smul_eq_mul, pow_succ, mul_assoc] at hr
  apply_fun algebraMap R L at hr
  simp only [map_mul] at hr
  rw [← IsLocalization.mk'_one (M := S) L, IsLocalization.mk'_eq_iff_eq, mul_one,
    Submonoid.coe_one, ← (IsLocalization.map_units L (s ^ n)).mul_left_cancel hr, map_mul]

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Noetherian

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
p : Ideal R
inst✝ : p.IsPrime
r : R
hr : (toPiLocalization R) r = Pi.single { asIdeal := p, isPrime := ⋯ } 1
this : (algebraMap R (Localization p.primeCompl)) r = 1
⊢ r ∉ p

Tactic:
rw [← IsLocalization.AtPrime.to_map_mem_maximal_iff (Localization.AtPrime p) p, this]
    simp

Goal state after:
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: S : Type u_1
inst✝¹ : CommRing S
P : Ideal S
P_prime : P.IsPrime
inst✝ : IsDedekindDomain S
hP : P ≠ ⊥
i : ℕ
⊢ cardQuot (P ^ i) = cardQuot P ^ i

Tactic:
induction i with
  | zero => simp
  | succ i ih => ?_
  have : P ^ (i + 1) < P ^ i := Ideal.pow_succ_lt_pow hP i
  suffices hquot : map (P ^ i.succ).mkQ (P ^ i) ≃ S ⧸ P by
    rw [pow_succ' (cardQuot P), ← ih, cardQuot_apply (P ^ i.succ), ←
      card_quotient_mul_card_quotient (P ^ i) (P ^ i.succ) this.le, cardQuot_apply (P ^ i),
      cardQuot_apply P, Nat.card_congr hquot]
  choose a a_mem a_notMem using SetLike.exists_of_lt this
  choose f g hg hf using fun c (hc : c ∈ P ^ i) =>
    Ideal.exists_mul_add_mem_pow_succ hP a c a_mem a_notMem hc
  choose k hk_mem hk_eq using fun c' (hc' : c' ∈ map (mkQ (P ^ i.succ)) (P ^ i)) =>
    Submodule.mem_map.mp hc'
  refine Equiv.ofBijective (fun c' => Quotient.mk'' (f (k c' c'.prop) (hk_mem c' c'.prop))) ⟨?_, ?_⟩
  · rintro ⟨c₁', hc₁'⟩ ⟨c₂', hc₂'⟩ h
    rw [Subtype.mk_eq_mk, ← hk_eq _ hc₁', ← hk_eq _ hc₂', mkQ_apply, mkQ_apply,
      Submodule.Quotient.eq, ← hf _ (hk_mem _ hc₁'), ← hf _ (hk_mem _ hc₂')]
    refine Ideal.mul_add_mem_pow_succ_inj _ _ _ _ _ _ a_mem (hg _ _) (hg _ _) ?_
    simpa only [Submodule.Quotient.mk''_eq_mk, Submodule.Quotient.mk''_eq_mk,
      Submodule.Quotient.eq] using h
  · intro d'
    induction d' using Quotient.inductionOn with | _ d
    have hd' := (mem_map (f := mkQ (P ^ i.succ))).mpr ⟨a * d, Ideal.mul_mem_right d _ a_mem, rfl⟩
    refine ⟨⟨_, hd'⟩, ?_⟩
    simp only [Submodule.Quotient.mk''_eq_mk, Ideal.Quotient.mk_eq_mk, Ideal.Quotient.eq]
    refine
      Ideal.mul_add_mem_pow_succ_unique hP a _ _ _ _ a_notMem (hg _ (hk_mem _ hd')) (zero_mem _) ?_
    rw [hf, add_zero]
    exact (Submodule.Quotient.eq _).mp (hk_eq _ hd')

Goal state after:
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDedekindDomain S
inst✝ : Free ℤ S
⊢ absNorm ⊤ = 1

Tactic:
← Ideal.one_eq_top,

Goal state after:
S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDedekindDomain S
inst✝ : Free ℤ S
⊢ absNorm 1 = 1
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
I : Ideal S
hI : I ≠ ⊥
⊢ ¬absNorm I = 0

Tactic:
absNorm_eq_zero_iff

Goal state after:
S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
I : Ideal S
hI : I ≠ ⊥
⊢ ¬I = ⊥
Module: Mathlib.RingTheory.Localization.InvSubmonoid

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
z : S
⊢ ∃ r m, z = r • ↑((toInvSubmonoid M S) m)

Tactic:
by
  rcases IsLocalization.surj M z with ⟨⟨r, m⟩, e : z * _ = algebraMap R S r⟩
  refine ⟨r, m, ?_⟩
  rw [Algebra.smul_def, ← e, mul_assoc]
  simp

Goal state after:
Module: Mathlib.GroupTheory.Submonoid.Inverses

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : ↥S
⊢ ↑x * ↑((S.leftInvEquiv hS).symm x) = 1

Tactic:
by
  convert! S.leftInvEquiv_mul hS ((S.leftInvEquiv hS).symm x)
  simp

Goal state after:
Module: Mathlib.RingTheory.HopkinsLevitzki

Goal state before:
pp: case refine_1
R₀ : Type u_1
R : Type u_2
M✝ : Type u
inst✝⁹ : Ring R₀
inst✝⁸ : Ring R
inst✝⁷ : Module R₀ R
inst✝⁶ : AddCommGroup M✝
inst✝⁵ : Module R₀ M✝
inst✝⁴ : Module R M✝
inst✝³ : IsScalarTower R₀ R M✝
inst✝² : IsSemiprimaryRing R
inst✝¹ : IsScalarTower R₀ R R
inst✝ : Module.Finite R₀ (R ⧸ Ring.jacobson R)
M : Type u
x✝⁴ : AddCommGroup M
x✝³ : Module R₀ M
x✝² : Module R M
x✝¹ : IsScalarTower R₀ R M
x✝ : IsSemisimpleModule R M
hJ : Module.IsTorsionBySet R M ↑(Ring.jacobson R)
h : IsNoetherian R M ∨ IsArtinian R M
⊢ Module.Finite R₀ M

Tactic:
let _ := hJ.module

Goal state after:
case refine_1
R₀ : Type u_1
R : Type u_2
M✝ : Type u
inst✝⁹ : Ring R₀
inst✝⁸ : Ring R
inst✝⁷ : Module R₀ R
inst✝⁶ : AddCommGroup M✝
inst✝⁵ : Module R₀ M✝
inst✝⁴ : Module R M✝
inst✝³ : IsScalarTower R₀ R M✝
inst✝² : IsSemiprimaryRing R
inst✝¹ : IsScalarTower R₀ R R
inst✝ : Module.Finite R₀ (R ⧸ Ring.jacobson R)
M : Type u
x✝⁵ : AddCommGroup M
x✝⁴ : Module R₀ M
x✝³ : Module R M
x✝² : IsScalarTower R₀ R M
x✝¹ : IsSemisimpleModule R M
hJ : Module.IsTorsionBySet R M ↑(Ring.jacobson R)
h : IsNoetherian R M ∨ IsArtinian R M
x✝ : Module (R ⧸ Ring.jacobson R) M := hJ.module
⊢ Module.Finite R₀ M
Module: Mathlib.Topology.JacobsonSpace

Goal state before:
pp: case inr
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : JacobsonSpace X
S : Set X
hS : IsLocallyClosed S
hf₁ : Continuous[inst✝², inst✝¹] f
hf₂ : IsClosedMap f
hfS : (f '' S).Finite
hS'' : S.Nonempty
hS' : IsIrreducible S
H₁ : IsIrreducible (S ∩ closedPoints X)
H₂ : f '' (S ∩ closedPoints X) ⊆ closedPoints Y
H₃ : (f '' (S ∩ closedPoints X)).Subsingleton
H₄ : IsClosed[inst✝¹] (f '' (S ∩ closedPoints X))
⊢ (f '' closure[inst✝²] S).Subsingleton

Tactic:
have := image_closure_subset_closure_image (s := S ∩ closedPoints X) hf₁

Goal state after:
case inr
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : JacobsonSpace X
S : Set X
hS : IsLocallyClosed S
hf₁ : Continuous[inst✝², inst✝¹] f
hf₂ : IsClosedMap f
hfS : (f '' S).Finite
hS'' : S.Nonempty
hS' : IsIrreducible S
H₁ : IsIrreducible (S ∩ closedPoints X)
H₂ : f '' (S ∩ closedPoints X) ⊆ closedPoints Y
H₃ : (f '' (S ∩ closedPoints X)).Subsingleton
H₄ : IsClosed[inst✝¹] (f '' (S ∩ closedPoints X))
this : f '' closure[inst✝²] (S ∩ closedPoints X) ⊆ closure[inst✝¹] (f '' (S ∩ closedPoints X))
⊢ (f '' closure[inst✝²] S).Subsingleton
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDedekindDomain S
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
n : ℕ
inst✝ : CharZero S
this✝ : Finite { I // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n }
this : Finite { I // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n }
e : { I // absNorm I ≤ n } ≃ { I // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n } ⊕ { I // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n } :=
  (Equiv.subtypeEquivRight ⋯).trans
    (subtypeOrEquiv (fun I ↦ I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n) (fun I ↦ I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n) ⋯)
I : Ideal S
| absNorm I = 0

Tactic:
absNorm_eq_zero_iff

Goal state after:
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDedekindDomain S
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
n : ℕ
inst✝ : CharZero S
this✝ : Finite { I // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n }
this : Finite { I // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n }
e : { I // absNorm I ≤ n } ≃ { I // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n } ⊕ { I // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n } :=
  (Equiv.subtypeEquivRight ⋯).trans
    (subtypeOrEquiv (fun I ↦ I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n) (fun I ↦ I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n) ⋯)
I : Ideal S
| I = ⊥
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
x : S
hx : Prime ((Algebra.norm ℤ) x)
y : ℤ
⊢ (Algebra.norm ℤ) x ∣ y ↔ y ∈ span {↑(absNorm (span {x}))}

pp: S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
x : S
hx : Prime ((Algebra.norm ℤ) x)
y : ℤ
⊢ Nat.Prime (absNorm (span {x}))

Tactic:
Ideal.mem_span_singleton,

Goal state after:
S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
x : S
hx : Prime ((Algebra.norm ℤ) x)
y : ℤ
⊢ (Algebra.norm ℤ) x ∣ y ↔ ↑(absNorm (span {x})) ∣ y

S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
x : S
hx : Prime ((Algebra.norm ℤ) x)
y : ℤ
⊢ Nat.Prime (absNorm (span {x}))
Module: Mathlib.NumberTheory.RamificationInertia.Ramification

Goal state before:
pp: case h₂
R : Type u
inst✝⁶ : CommRing R
S : Type v
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDedekindDomain S
inst✝² : IsDedekindDomain R
inst✝¹ : FaithfulSMul R S
v : Ideal R
w : Ideal S
hv : Irreducible v
hw : Irreducible w
hw_bot : w ≠ ⊥
inst✝ : w.LiesOver v
hI : IsUnit ⊤
h : ⊤ ≠ ⊥
⊢ ↑(Multiset.count (normalize w) (normalizedFactors ⊤)) =
    ↑(v.ramificationIdx' w) * ↑(Multiset.count (normalize v) (normalizedFactors ⊤))

Tactic:
← Ideal.one_eq_top,

Goal state after:
case h₂
R : Type u
inst✝⁶ : CommRing R
S : Type v
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDedekindDomain S
inst✝² : IsDedekindDomain R
inst✝¹ : FaithfulSMul R S
v : Ideal R
w : Ideal S
hv : Irreducible v
hw : Irreducible w
hw_bot : w ≠ ⊥
inst✝ : w.LiesOver v
hI : IsUnit ⊤
h : ⊤ ≠ ⊥
⊢ ↑(Multiset.count (normalize w) (normalizedFactors 1)) =
    ↑(v.ramificationIdx' w) * ↑(Multiset.count (normalize v) (normalizedFactors 1))
Module: Mathlib.RingTheory.QuasiFinite.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
p : Ideal S
inst✝⁴ : p.IsPrime
inst✝³ : QuasiFiniteAt R p
A : Type u_4
inst✝² : CommRing A
inst✝¹ : Algebra R A
q : Ideal (A ⊗[R] S)
inst✝ : q.IsPrime
hq : p = Ideal.comap TensorProduct.includeRight.toRingHom q
f : A ⊗[R] Localization.AtPrime p →ₐ[A] Localization.AtPrime q :=
  TensorProduct.lift (ofId A (Localization.AtPrime q))
    { toRingHom := Localization.localRingHom p q TensorProduct.includeRight.toRingHom hq, commutes' := ⋯ } ⋯
g : A ⊗[R] S →ₐ[A] A ⊗[R] Localization.AtPrime p :=
  TensorProduct.map (AlgHom.id A A) (IsScalarTower.toAlgHom R S (Localization.AtPrime p))
this : ∀ (x : A ⊗[R] S), f (g x) = (algebraMap (A ⊗[R] S) (Localization.AtPrime q)) x
x s : A ⊗[R] S
hs : s ∈ q.primeCompl
⊢ ∃ s_1, IsUnit (f s_1) ∧ IsLocalization.mk' (Localization.AtPrime q) x ⟨s, hs⟩ * f s_1 ∈ f.range

Tactic:
refine ⟨g s, this s ▸ IsLocalization.map_units _ ⟨s, hs⟩, ?_⟩

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
p : Ideal S
inst✝⁴ : p.IsPrime
inst✝³ : QuasiFiniteAt R p
A : Type u_4
inst✝² : CommRing A
inst✝¹ : Algebra R A
q : Ideal (A ⊗[R] S)
inst✝ : q.IsPrime
hq : p = Ideal.comap TensorProduct.includeRight.toRingHom q
f : A ⊗[R] Localization.AtPrime p →ₐ[A] Localization.AtPrime q :=
  TensorProduct.lift (ofId A (Localization.AtPrime q))
    { toRingHom := Localization.localRingHom p q TensorProduct.includeRight.toRingHom hq, commutes' := ⋯ } ⋯
g : A ⊗[R] S →ₐ[A] A ⊗[R] Localization.AtPrime p :=
  TensorProduct.map (AlgHom.id A A) (IsScalarTower.toAlgHom R S (Localization.AtPrime p))
this : ∀ (x : A ⊗[R] S), f (g x) = (algebraMap (A ⊗[R] S) (Localization.AtPrime q)) x
x s : A ⊗[R] S
hs : s ∈ q.primeCompl
⊢ IsLocalization.mk' (Localization.AtPrime q) x ⟨s, hs⟩ * f (g s) ∈ f.range
Module: Mathlib.RingTheory.Smooth.Basic

Goal state before:
pp: R : Type u
A : Type v
inst✝⁹ : CommRing R
inst✝⁸ : CommRing A
inst✝⁷ : Algebra R A
B : Type u_1
P : Type u_2
C : Type u_3
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R B
inst✝⁴ : CommRing C
inst✝³ : Algebra R C
inst✝² : CommRing P
inst✝¹ : Algebra R P
P₁ : Extension R A
P₂ : Extension R A
inst✝ : FormallySmooth R P₁.Ring
⊢ P₂.infinitesimal.ker ^ 2 = ⊥

Tactic:
rw [ker_infinitesimal]; exact Ideal.cotangentIdeal_square _

Goal state after:
Module: Mathlib.RingTheory.Unramified.Finite

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
inst✝¹ : FormallyUnramified R S
inst✝ : EssFiniteType R S
r : S
m : M
⊢ (TensorProduct.AlgebraTensorModule.map LinearMap.id ((lsmul R R M).toLinearMap.flip m)) (1 ⊗ₜ[R] r * elem R S) =
    r • (TensorProduct.AlgebraTensorModule.map LinearMap.id ((lsmul R R M).toLinearMap.flip m)) (elem R S)

Tactic:
have := one_tmul_sub_tmul_one_mul_elem (R := R) r
      rw [sub_mul, sub_eq_zero] at this
      rw [this]
      induction elem R S using TensorProduct.induction_on
      · simp
      · simp [TensorProduct.smul_tmul']
      · simp only [map_add, smul_add, mul_add, *]

Goal state after:
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: R : Type u₁
S : Type u₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u₃
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
i : ι ⊕ σ
j : ι
⊢ (Q.cotangentSpaceBasis.repr
        ((Q.cotangentSpaceBasis.prod (Basis.baseChange T P.cotangentSpaceBasis)).repr.symm (Finsupp.single i 1)).1)
      j =
    (aeval Q.val) ((pderiv j) (Sum.elim X (⇑C ∘ P.val) i))

Tactic:
obtain (i | i) := i <;>
    simp only [Basis.repr_symm_apply, Finsupp.linearCombination_single, Basis.prod_apply,
      LinearMap.coe_inl, LinearMap.coe_inr, Sum.elim_inl, Function.comp_apply, one_smul,
      Basis.repr_self, Finsupp.single_apply, pderiv_X, Pi.single_apply,
      Sum.elim_inr, Function.comp_apply, Basis.baseChange_apply, one_smul,
      MonoidWithZeroHom.map_ite_one_zero, map_zero, Finsupp.coe_zero, Pi.zero_apply, derivation_C]

Goal state after:
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: case monomial.monomial
R : Type u₁
S : Type u₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u₃
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
ι : Type w₁
Q : Generators S T ι
n : ι →₀ ℕ
r : S
m : ι →₀ ℕ
s : S
⊢ (δAux R Q) ((monomial n) r * (monomial m) s) =
    (monomial n) r • (δAux R Q) ((monomial m) s) + (monomial m) s • (δAux R Q) ((monomial n) r)

Tactic:
| monomial m s =>

Goal state after: