mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Invariant.Basic

Goal state before:
pp: case intro
A : Type u_1
B : Type u_2
inst✝¹⁸ : CommRing A
inst✝¹⁷ : CommRing B
inst✝¹⁶ : Algebra A B
G : Type u_3
inst✝¹⁵ : Group G
inst✝¹⁴ : Finite G
inst✝¹³ : MulSemiringAction G B
inst✝¹² : SMulCommClass G A B
P : Ideal A
Q : Ideal B
inst✝¹¹ : Q.IsPrime
inst✝¹⁰ : Q.LiesOver P
K : Type u_4
L : Type u_5
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra (A ⧸ P) K
inst✝⁶ : Algebra (B ⧸ Q) L
inst✝⁵ : Algebra (A ⧸ P) L
inst✝⁴ : IsScalarTower (A ⧸ P) (B ⧸ Q) L
inst✝³ : Algebra K L
inst✝² : IsScalarTower (A ⧸ P) K L
inst✝¹ : Algebra.IsInvariant A B G
inst✝ : Module.IsTorsionFree (B ⧸ Q) L
f : Gal(L/K)
val✝ : Fintype G
b₀ : B
hx :
  ∀ (g : ↥(MulAction.stabilizer G Q)),
    ((Ideal.Quotient.stabilizerHom Q P G) g) ((Ideal.Quotient.mk Q) b₀) = (Ideal.Quotient.mk Q) b₀
a b : B
ha1 : ∀ (g : G), g • a = a
ha2 : a ∉ Q
hb : ∀ (g : G), (algebraMap B (B ⧸ Q)) (g • b) = (algebraMap B (B ⧸ Q)) (if g • Q = Q then a * b₀ else 0)
M : A[X]
key : map (algebraMap A B) M = MulSemiringAction.charpoly G b
⊢ f ((algebraMap (B ⧸ Q) L) ((algebraMap B (B ⧸ Q)) b₀)) = (algebraMap (B ⧸ Q) L) ((algebraMap B (B ⧸ Q)) b₀)

Tactic:
replace key := congrArg (map (algebraMap B (B ⧸ Q))) key

Goal state after:
case intro
A : Type u_1
B : Type u_2
inst✝¹⁸ : CommRing A
inst✝¹⁷ : CommRing B
inst✝¹⁶ : Algebra A B
G : Type u_3
inst✝¹⁵ : Group G
inst✝¹⁴ : Finite G
inst✝¹³ : MulSemiringAction G B
inst✝¹² : SMulCommClass G A B
P : Ideal A
Q : Ideal B
inst✝¹¹ : Q.IsPrime
inst✝¹⁰ : Q.LiesOver P
K : Type u_4
L : Type u_5
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra (A ⧸ P) K
inst✝⁶ : Algebra (B ⧸ Q) L
inst✝⁵ : Algebra (A ⧸ P) L
inst✝⁴ : IsScalarTower (A ⧸ P) (B ⧸ Q) L
inst✝³ : Algebra K L
inst✝² : IsScalarTower (A ⧸ P) K L
inst✝¹ : Algebra.IsInvariant A B G
inst✝ : Module.IsTorsionFree (B ⧸ Q) L
f : Gal(L/K)
val✝ : Fintype G
b₀ : B
hx :
  ∀ (g : ↥(MulAction.stabilizer G Q)),
    ((Ideal.Quotient.stabilizerHom Q P G) g) ((Ideal.Quotient.mk Q) b₀) = (Ideal.Quotient.mk Q) b₀
a b : B
ha1 : ∀ (g : G), g • a = a
ha2 : a ∉ Q
hb : ∀ (g : G), (algebraMap B (B ⧸ Q)) (g • b) = (algebraMap B (B ⧸ Q)) (if g • Q = Q then a * b₀ else 0)
M : A[X]
key : map (algebraMap B (B ⧸ Q)) (map (algebraMap A B) M) = map (algebraMap B (B ⧸ Q)) (MulSemiringAction.charpoly G b)
⊢ f ((algebraMap (B ⧸ Q) L) ((algebraMap B (B ⧸ Q)) b₀)) = (algebraMap (B ⧸ Q) L) ((algebraMap B (B ⧸ Q)) b₀)
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : GroupWithZero K
inst✝ : Fintype K
a : K
ha : a ≠ 0
⊢ ↑(Units.mk0 a ha ^ (q - 1)) = 1

Tactic:
classical
        rw [← Fintype.card_units, pow_card_eq_one]
        rfl

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
h : i < q - 1
hi : ¬i = 0
hiq : ¬q - 1 ∣ i
φ : Kˣ ↪ K := { toFun := fun x ↦ ↑x, inj' := ⋯ }
x : K
⊢ x ∈ map φ univ ↔ x ∈ univ \ {0}

Tactic:
simpa only [mem_map, mem_univ, Function.Embedding.coeFn_mk, true_and, mem_sdiff,
        mem_singleton, φ] using! isUnit_iff_ne_zero

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

Goal state before:
pp: case inr.inl
n p k : ℕ
inst✝ : Fact (Nat.Prime p)
hn : n = p ^ k
hn0 : n ≠ 0
ha : (orderOf 0).Coprime n
⊢ 0 = 1 ∨ IsUnit (0 - 1)

pp: case inr.inr
n p k : ℕ
inst✝ : Fact (Nat.Prime p)
hn : n = p ^ k
a : ZMod n
ha : (orderOf a).Coprime n
hn0 : n ≠ 0
ha0 : a ≠ 0
⊢ a = 1 ∨ IsUnit (a - 1)

Tactic:
· exact Or.inr (zero_sub (1 : ZMod n) ▸ isUnit_neg_one)

Goal state after:
case inr.inr
n p k : ℕ
inst✝ : Fact (Nat.Prime p)
hn : n = p ^ k
a : ZMod n
ha : (orderOf a).Coprime n
hn0 : n ≠ 0
ha0 : a ≠ 0
⊢ a = 1 ∨ IsUnit (a - 1)
Module: Mathlib.LinearAlgebra.FreeModule.Finite.Quotient

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : IsDomain R
inst✝⁵ : IsPrincipalIdealRing R
inst✝⁴ : Finite ι
F : Type u_4
inst✝³ : CommRing F
inst✝² : Algebra F R
inst✝¹ : Module F M
inst✝ : IsScalarTower F R M
b : Basis ι R M
N : Submodule R M
h : finrank R ↥N = finrank R M
⊢ (M ⧸ N) ≃ₗ[F] ⨁ (i : ι), R ⧸ Ideal.span {smithNormalFormCoeffs b h i}

Tactic:
by
  haveI := Fintype.ofFinite ι
  exact ((N.quotientEquivPiSpan b _).restrictScalars F).trans
    (DirectSum.linearEquivFunOnFintype _ _ _).symm

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient

Goal state before:
pp: case calc_1
M : Type u_1
inst✝⁴ : AddCommGroup M
inst✝³ : Free ℤ M
inst✝² : Module.Finite ℤ M
N : Submodule ℤ M
E : Type u_2
inst✝¹ : EquivLike E M ↥N
inst✝ : AddEquivClass E M ↥N
e : E
b : Basis (Free.ChooseBasisIndex ℤ M) ℤ M := Free.chooseBasis ℤ M
h : finrank ℤ ↥N = finrank ℤ M
a : Free.ChooseBasisIndex ℤ M → ℤ := smithNormalFormCoeffs b h
b' : Basis (Free.ChooseBasisIndex ℤ M) ℤ M := smithNormalFormTopBasis b h
ab : Basis (Free.ChooseBasisIndex ℤ M) ℤ ↥N := smithNormalFormBotBasis b h
ab_eq :
  ∀ (i : Free.ChooseBasisIndex ℤ M),
    ↑((smithNormalFormBotBasis b h) i) = smithNormalFormCoeffs b h i • (smithNormalFormTopBasis b h) i
e' : M ≃ₗ[ℤ] ↥N := b'.equiv ab (Equiv.refl (Free.ChooseBasisIndex ℤ M))
f : M →ₗ[ℤ] M := N.subtype ∘ₗ ↑e'
f_apply : ∀ (x : M), f x = ↑((b'.equiv ab (Equiv.refl (Free.ChooseBasisIndex ℤ M))) x) := fun x ↦ rfl
ha : ∀ (i : Free.ChooseBasisIndex ℤ M), f (b' i) = a i • b' i
i j : Free.ChooseBasisIndex ℤ M
⊢ (b'.repr (f (b' j))) i = Matrix.diagonal a i j

Tactic:
ha,

Goal state after:
case calc_1
M : Type u_1
inst✝⁴ : AddCommGroup M
inst✝³ : Free ℤ M
inst✝² : Module.Finite ℤ M
N : Submodule ℤ M
E : Type u_2
inst✝¹ : EquivLike E M ↥N
inst✝ : AddEquivClass E M ↥N
e : E
b : Basis (Free.ChooseBasisIndex ℤ M) ℤ M := Free.chooseBasis ℤ M
h : finrank ℤ ↥N = finrank ℤ M
a : Free.ChooseBasisIndex ℤ M → ℤ := smithNormalFormCoeffs b h
b' : Basis (Free.ChooseBasisIndex ℤ M) ℤ M := smithNormalFormTopBasis b h
ab : Basis (Free.ChooseBasisIndex ℤ M) ℤ ↥N := smithNormalFormBotBasis b h
ab_eq :
  ∀ (i : Free.ChooseBasisIndex ℤ M),
    ↑((smithNormalFormBotBasis b h) i) = smithNormalFormCoeffs b h i • (smithNormalFormTopBasis b h) i
e' : M ≃ₗ[ℤ] ↥N := b'.equiv ab (Equiv.refl (Free.ChooseBasisIndex ℤ M))
f : M →ₗ[ℤ] M := N.subtype ∘ₗ ↑e'
f_apply : ∀ (x : M), f x = ↑((b'.equiv ab (Equiv.refl (Free.ChooseBasisIndex ℤ M))) x) := fun x ↦ rfl
ha : ∀ (i : Free.ChooseBasisIndex ℤ M), f (b' i) = a i • b' i
i j : Free.ChooseBasisIndex ℤ M
⊢ (b'.repr (a j • b' j)) i = Matrix.diagonal a i j
Module: Mathlib.NumberTheory.RamificationInertia.Inertia

Goal state before:
pp: R : Type u
inst✝⁸ : CommRing R
S : Type u_1
inst✝⁷ : CommRing S
inst✝⁶ : IsDedekindDomain S
inst✝⁵ : Free ℤ S
inst✝⁴ : IsDedekindDomain R
inst✝³ : Free ℤ R
inst✝² : Algebra S R
inst✝¹ : Module.Finite S R
P : Ideal R
p : Ideal S
inst✝ : P.LiesOver p
hp : p.IsPrime
hp_ne_bot : p ≠ ⊥
⊢ absNorm P = absNorm p ^ p.inertiaDeg' P

Tactic:
have : p.IsMaximal := hp.isMaximal hp_ne_bot

Goal state after:
R : Type u
inst✝⁸ : CommRing R
S : Type u_1
inst✝⁷ : CommRing S
inst✝⁶ : IsDedekindDomain S
inst✝⁵ : Free ℤ S
inst✝⁴ : IsDedekindDomain R
inst✝³ : Free ℤ R
inst✝² : Algebra S R
inst✝¹ : Module.Finite S R
P : Ideal R
p : Ideal S
inst✝ : P.LiesOver p
hp : p.IsPrime
hp_ne_bot : p ≠ ⊥
this : p.IsMaximal
⊢ absNorm P = absNorm p ^ p.inertiaDeg' P
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: S : Type u_1
inst✝ : CommRing S
P : Ideal S
i : ℕ
a d d' e e' : S
a_mem : a ∈ P ^ i
e_mem : e ∈ P ^ (i + 1)
e'_mem : e' ∈ P ^ (i + 1)
h : d - d' ∈ P
⊢ a * d + e - (a * d' + e') ∈ P ^ (i + 1)

Tactic:
by
  have : a * d - a * d' ∈ P ^ (i + 1) := by
    simp only [← mul_sub]
    exact Ideal.mul_mem_mul a_mem h
  convert! Ideal.add_mem _ this (Ideal.sub_mem _ e_mem e'_mem) using 1
  ring

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
⊢ ↑((S.leftInvEquiv hS).symm x) * ↑x = 1

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

Goal state after:
Module: Mathlib.RingTheory.HopkinsLevitzki

Goal state before:
pp: case succ.succ.refine_2
R₀ : Type u_1
R : Type u_2
inst✝⁷ : Ring R₀
inst✝⁶ : Ring R
inst✝⁵ : Module R₀ R
inst✝⁴ : IsSemiprimaryRing R
P : (M : Type u) → [inst : AddCommGroup M] → [Module R₀ M] → [Module R M] → Prop
ss : IsSemisimpleRing (R ⧸ Ring.jacobson R)
Jac : Ideal R := Ring.jacobson R
h0 :
  ∀ (M : Type u) [inst : AddCommGroup M] [inst_1 : Module R₀ M] [inst_2 : Module R M] [IsScalarTower R₀ R M]
    [IsSemisimpleModule R M], Module.IsTorsionBySet R M ↑Jac → P M
h1 :
  ∀ (M : Type u) [inst : AddCommGroup M] [inst_1 : Module R₀ M] [inst_2 : Module R M] [inst_3 : IsScalarTower R₀ R M],
    let N := Jac • ⊤;
    P ↥N → P (M ⧸ N) → P M
this :
  ∀ {M : Type u} [inst : AddCommGroup M] [inst_1 : Module R₀ M] [inst_2 : Module R M] [IsScalarTower R₀ R M],
    Jac ≤ Module.annihilator R M → P M
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R₀ M
inst✝¹ : Module R M
inst✝ : IsScalarTower R₀ R M
n : ℕ
ih :
  ∀ (M : Type u) [inst : AddCommGroup M] [inst_1 : Module R₀ M] [inst_2 : Module R M] [IsScalarTower R₀ R M],
    Jac ^ (n + 1) ≤ Module.annihilator R M → P M
hn : Jac ^ (n + 1 + 1) ≤ Module.annihilator R M
⊢ Jac ^ (n + 1) ≤ Module.annihilator R (M ⧸ Jac • ⊤)

Tactic:
rw [← SetLike.coe_subset_coe, ← Module.isTorsionBySet_iff_subset_annihilator,
      Module.isTorsionBySet_quotient_iff]
    exact fun m i hi ↦ Submodule.smul_mem_smul (Ideal.pow_le_self n.succ_ne_zero hi) trivial

Goal state after:
Module: Mathlib.RingTheory.HopkinsLevitzki

Goal state before:
pp: M : Type u
inst✝⁴ : AddCommGroup M
R : Type u_3
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : IsArtinian R M
s : Set M
fin : Finite ↑s
span : ⨆ i, R ∙ ↑i = ⊤
⊢ IsNoetherian R ↥(⨆ i, R ∙ ↑i)

Tactic:
have _ (i : M) : IsNoetherian R (Submodule.span R {i}) := by
    rw [LinearMap.span_singleton_eq_range, ← (LinearMap.quotKerEquivRange _).isNoetherian_iff]
    let e (I : Ideal R) : R ⧸ I →ₛₗ[Ideal.Quotient.mk I] R ⧸ I := ⟨.id _, fun _ _ ↦ rfl⟩
    rw [(e _).isNoetherian_iff_of_bijective Function.bijective_id]
    refine @instIsNoetherianRingOfIsArtinianRing _ _ ?_
    rw [IsArtinianRing, ← (e _).isArtinian_iff_of_bijective Function.bijective_id,
      (LinearMap.quotKerEquivRange _).isArtinian_iff]
    infer_instance

Goal state after:
M : Type u
inst✝⁴ : AddCommGroup M
R : Type u_3
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : IsArtinian R M
s : Set M
fin : Finite ↑s
span : ⨆ i, R ∙ ↑i = ⊤
x✝ : ∀ (i : M), IsNoetherian R ↥(R ∙ i)
⊢ IsNoetherian R ↥(⨆ i, R ∙ ↑i)
Module: Mathlib.RingTheory.HopkinsLevitzki

Goal state before:
pp: R : Type u_3
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
⊢ IsArtinianRing R ↔ IsNilpotent (IsLocalRing.maximalIdeal R)

Tactic:
rw [isArtinianRing_iff_krullDimLE_zero,
    Ideal.FG.isNilpotent_iff_le_nilradical (IsNoetherian.noetherian _),
    ← and_iff_left (a := Ring.KrullDimLE 0 R) ‹IsLocalRing R›,
    (Ring.krullDimLE_zero_and_isLocalRing_tfae R).out 0 3 rfl rfl,
    IsLocalRing.isMaximal_iff, le_antisymm_iff, and_iff_right]

Goal state after:
R : Type u_3
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
⊢ nilradical R ≤ IsLocalRing.maximalIdeal R
Module: Mathlib.RingTheory.LocalRing.ResidueField.Instances

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹² : CommRing R
inst✝¹¹ : CommRing A
inst✝¹⁰ : CommRing B
inst✝⁹ : Algebra R A
inst✝⁸ : Algebra A B
inst✝⁷ : Algebra R B
inst✝⁶ : IsScalarTower R A B
p : Ideal A
q : Ideal B
inst✝⁵ : q.LiesOver p
inst✝⁴ : p.IsMaximal
inst✝³ : q.IsMaximal
inst✝² : Algebra (Localization.AtPrime p) (Localization.AtPrime q)
inst✝¹ : Localization.AtPrime.IsLiesOverAlgebra p q
inst✝ : Algebra.IsSeparable (A ⧸ p) (B ⧸ q)
⊢ Algebra.IsSeparable p.ResidueField q.ResidueField

Tactic:
by
  refine Algebra.IsSeparable.of_equiv_equiv
    (.ofBijective _ p.bijective_algebraMap_quotient_residueField)
    (.ofBijective _ q.bijective_algebraMap_quotient_residueField) ?_
  ext x
  simp [RingHom.algebraMap_toAlgebra, ← IsScalarTower.algebraMap_apply]

Goal state after:
Module: Mathlib.RingTheory.LocalRing.ResidueField.Instances

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹² : CommRing R
inst✝¹¹ : CommRing A
inst✝¹⁰ : CommRing B
inst✝⁹ : Algebra R A
inst✝⁸ : Algebra A B
inst✝⁷ : Algebra R B
inst✝⁶ : IsScalarTower R A B
p : Ideal A
q : Ideal B
inst✝⁵ : q.LiesOver p
inst✝⁴ : p.IsMaximal
inst✝³ : q.IsMaximal
inst✝² : Algebra (Localization.AtPrime p) (Localization.AtPrime q)
inst✝¹ : Localization.AtPrime.IsLiesOverAlgebra p q
inst✝ : Algebra.IsSeparable p.ResidueField q.ResidueField
x : p.ResidueField
⊢ ((algebraMap (A ⧸ p) (B ⧸ q)).comp ↑(RingEquiv.ofBijective (algebraMap (A ⧸ p) p.ResidueField) ⋯).symm) x =
    ((↑(RingEquiv.ofBijective (algebraMap (B ⧸ q) q.ResidueField) ⋯).symm).comp
        (algebraMap p.ResidueField q.ResidueField))
      x

Tactic:
obtain ⟨x, rfl⟩ :=
    (RingEquiv.ofBijective _ p.bijective_algebraMap_quotient_residueField).surjective x

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹² : CommRing R
inst✝¹¹ : CommRing A
inst✝¹⁰ : CommRing B
inst✝⁹ : Algebra R A
inst✝⁸ : Algebra A B
inst✝⁷ : Algebra R B
inst✝⁶ : IsScalarTower R A B
p : Ideal A
q : Ideal B
inst✝⁵ : q.LiesOver p
inst✝⁴ : p.IsMaximal
inst✝³ : q.IsMaximal
inst✝² : Algebra (Localization.AtPrime p) (Localization.AtPrime q)
inst✝¹ : Localization.AtPrime.IsLiesOverAlgebra p q
inst✝ : Algebra.IsSeparable p.ResidueField q.ResidueField
x : A ⧸ p
⊢ ((algebraMap (A ⧸ p) (B ⧸ q)).comp ↑(RingEquiv.ofBijective (algebraMap (A ⧸ p) p.ResidueField) ⋯).symm)
      ((RingEquiv.ofBijective (algebraMap (A ⧸ p) p.ResidueField) ⋯) x) =
    ((↑(RingEquiv.ofBijective (algebraMap (B ⧸ q) q.ResidueField) ⋯).symm).comp
        (algebraMap p.ResidueField q.ResidueField))
      ((RingEquiv.ofBijective (algebraMap (A ⧸ p) p.ResidueField) ⋯) x)
Module: Mathlib.RingTheory.Ideal.IdempotentFG

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I.FG
e : IsIdempotentElem I
⊢ I ≤ I • I

Tactic:
rw [smul_eq_mul]

Goal state after:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I.FG
e : IsIdempotentElem I
⊢ I ≤ I * I
Module: Mathlib.NumberTheory.RamificationInertia.Ramification

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsDedekindDomain S
p : Ideal R
P : Ideal S
inst✝ : P.IsPrime
hp : P ≠ ⊥
hpP : map f p ≤ P
Sₚ : Type v := Localization.AtPrime P
H₁ : ¬map f p ≤ P * P
a : Ideal S
ha : map f p = P * a
ha' : ¬a ≤ P
⊢ map (algebraMap S (Localization.AtPrime P)) (map f p) = maximalIdeal (Localization.AtPrime P)

Tactic:
ha,

Goal state after:
R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsDedekindDomain S
p : Ideal R
P : Ideal S
inst✝ : P.IsPrime
hp : P ≠ ⊥
hpP : map f p ≤ P
Sₚ : Type v := Localization.AtPrime P
H₁ : ¬map f p ≤ P * P
a : Ideal S
ha : map f p = P * a
ha' : ¬a ≤ P
⊢ map (algebraMap S (Localization.AtPrime P)) (P * a) = maximalIdeal (Localization.AtPrime P)
Module: Mathlib.RingTheory.Unramified.Finite

Goal state before:
pp: case mpr
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : EssFiniteType R S
this : ∀ (t : S ⊗[R] S), (TensorProduct.lmul' R) t = 1 ↔ 1 - t ∈ KaehlerDifferential.ideal R S
⊢ (∃ t, (∀ (s : S), (1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) * t = 0) ∧ 1 - t ∈ Ideal.span (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)) →
    ∃ e, IsIdempotentElem e ∧ Ideal.span (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) = S ⊗[R] S ∙ e

Tactic:
rintro ⟨t, ht₁, ht₂⟩

Goal state after:
case mpr
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : EssFiniteType R S
this : ∀ (t : S ⊗[R] S), (TensorProduct.lmul' R) t = 1 ↔ 1 - t ∈ KaehlerDifferential.ideal R S
t : S ⊗[R] S
ht₁ : ∀ (s : S), (1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) * t = 0
ht₂ : 1 - t ∈ Ideal.span (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)
⊢ ∃ e, IsIdempotentElem e ∧ Ideal.span (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) = S ⊗[R] S ∙ e
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
inst✝ : FiniteType R S
⊢ (∀ (x : PrimeSpectrum R), (PrimeSpectrum.comap (algebraMap R S) ⁻¹' {x}).Finite) ↔
    ∀ (I : Ideal R), I.IsPrime → (I.primesOver S).Finite

Tactic:
(PrimeSpectrum.equivSubtype R).forall_congr_left,

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : FiniteType R S
⊢ (∀ (b : { I // I.IsPrime }),
      (PrimeSpectrum.comap (algebraMap R S) ⁻¹' {(PrimeSpectrum.equivSubtype R).symm b}).Finite) ↔
    ∀ (I : Ideal R), I.IsPrime → (I.primesOver S).Finite
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
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FormallySmooth R A
I : Ideal B
hI : I ^ 2 = ⊥
f : A →ₐ[R] B ⧸ I
P : Generators R A A := Generators.self R A
hP : Function.Injective ⇑P.toExtension.cotangentComplex
l : P.toExtension.CotangentSpace →ₗ[A] P.toExtension.Cotangent
hl : l ∘ₗ P.toExtension.cotangentComplex = LinearMap.id
⊢ ∀ (m : P.Ring) (x : P.toExtension.Cotangent),
    { toFun := Cotangent.val, map_add' := ⋯ }.toFun (m • x) =
      (RingHom.id P.Ring) m • { toFun := Cotangent.val, map_add' := ⋯ }.toFun x

Tactic:
simpa using! Cotangent.val_smul' (P := P.toExtension)

Goal state after:
Module: Mathlib.RingTheory.RamificationInertia.Basic

Goal state before:
pp: R : Type u_1
inst✝¹¹ : CommRing R
p : Ideal R
inst✝¹⁰ : p.IsPrime
S : Type u_2
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
inst✝⁷ : IsDomain R
inst✝⁶ : IsDomain S
inst✝⁵ : Module.Finite R S
inst✝⁴ : Module.Flat R S
inst✝³ : Fintype ↑(p.primesOver S)
G : Type u_3
inst✝² : Group G
inst✝¹ : MulSemiringAction G S
inst✝ : IsGaloisGroup G R S
this : Finite G := IsGaloisGroup.finite G R S
⊢ ∑ q, (↑q).ramificationIdx R * (↑q).inertiaDeg R = Nat.card G

Tactic:
sum_ramification_inertia_eq_finrank,

Goal state after:
R : Type u_1
inst✝¹¹ : CommRing R
p : Ideal R
inst✝¹⁰ : p.IsPrime
S : Type u_2
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
inst✝⁷ : IsDomain R
inst✝⁶ : IsDomain S
inst✝⁵ : Module.Finite R S
inst✝⁴ : Module.Flat R S
inst✝³ : Fintype ↑(p.primesOver S)
G : Type u_3
inst✝² : Group G
inst✝¹ : MulSemiringAction G S
inst✝ : IsGaloisGroup G R S
this : Finite G := IsGaloisGroup.finite G R S
⊢ Module.finrank R S = Nat.card G
Module: Mathlib.RingTheory.RamificationInertia.Ramification

Goal state before:
pp: case pos
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
q : Ideal S
G : Type u_4
inst✝² : Group G
inst✝¹ : MulSemiringAction G S
inst✝ : SMulCommClass G R S
g : G
hq : q.IsPrime
⊢ (g • q).ramificationIdx R = q.ramificationIdx R

Tactic:
let p := q.under R
    let f₀ := MulSemiringAction.toAlgAut G R S g
    have hg : g • q = q.map f₀ := q.pointwise_smul_def
    let Sq := Localization.AtPrime q
    let Sq' := Localization.AtPrime (q.map f₀)
    let f : Sq ≃ₐ[R] Sq' :=
      Localization.localAlgEquiv q (q.map f₀) f₀ (comap_map_of_bijective f₀ f₀.bijective).symm
    let : Algebra Sq Sq' := f.toRingHom.toAlgebra
    have : IsScalarTower R Sq Sq' := IsScalarTower.of_algHom f.toAlgHom
    let e : (Sq ⧸ p.map (algebraMap R Sq)) ≃ₐ[Sq] Sq' ⧸ p.map (algebraMap R Sq') :=
      Ideal.quotientEquivAlg _ _ (AlgEquiv.ofBijective (Algebra.ofId Sq Sq') f.bijective)
        (by rw [IsScalarTower.algebraMap_eq R Sq Sq', Ideal.map_map,
          ← AlgEquiv.toAlgHom_toRingHom, AlgEquiv.toAlgHom_ofBijective, Algebra.toRingHom_ofId])
    rw [hg, ramificationIdx_eq p q, ramificationIdx_eq p (q.map f₀),
      e.toLinearEquiv.length_eq, Module.length_eq_of_surjective f.surjective]

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: A : Type u_1
M : Type u_2
inst✝³ : CommRing A
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : IsDedekindDomain A
h : IsTorsion A M
⊢ ⨆ P, primaryComponent M P.asIdeal = ⊤

Tactic:
eq_top_iff'

Goal state after:
A : Type u_1
M : Type u_2
inst✝³ : CommRing A
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : IsDedekindDomain A
h : IsTorsion A M
⊢ ∀ (x : M), x ∈ ⨆ P, primaryComponent M P.asIdeal
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
this : ∀ (d : ℕ), BddAbove {m | ∃ y ∈ s, ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d} ∧ ∀ z ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d}, z ≤ f d
hf₁ : ∀ n > 0, ∃ y ∈ s, ↑(↑(f n) / ↑n) ≤ y
n : ℕ
n0 : n > 0
y : ℝ
yS : y ∈ s
⊢ y - (↑n)⁻¹ < ↑(↑(f n) / ↑n)

Tactic:
have := (Int.sub_one_lt_floor _).trans_le (Int.cast_le.2 <| (hf n).2 _ ⟨y, yS, Int.floor_le _⟩)

Goal state after:
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
this✝ : ∀ (d : ℕ), BddAbove {m | ∃ y ∈ s, ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d} ∧ ∀ z ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d}, z ≤ f d
hf₁ : ∀ n > 0, ∃ y ∈ s, ↑(↑(f n) / ↑n) ≤ y
n : ℕ
n0 : n > 0
y : ℝ
yS : y ∈ s
this : y * ↑n - 1 < ↑(f n)
⊢ y - (↑n)⁻¹ < ↑(↑(f n) / ↑n)
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: A : Type u_1
M : Type u_2
inst✝³ : CommRing A
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : IsDedekindDomain A
h : IsTorsion A M
x : M
a : A
ha : a ∈ A⁰
hmem : x ∈ torsionBySet A M ↑(⨅ i, i.maxPowDividing (span {a}))
ha0 : span {a} ≠ ⊥
this✝ : Fintype ↑(mulSupport fun v ↦ v.maxPowDividing (span {a})) := Finite.fintype ⋯
S : Finset (HeightOneSpectrum A) := (mulSupport fun v ↦ v.maxPowDividing (span {a})).toFinset
this : ⨅ i, i.maxPowDividing (span {a}) = ⨅ i ∈ S, i.maxPowDividing (span {a})
hPairwise : (↑S).Pairwise fun i j ↦ i.maxPowDividing (span {a}) ⊔ j.maxPowDividing (span {a}) = ⊤
⊢ x ∈ ⨆ P, primaryComponent M P.asIdeal

Tactic:
rw [this, ← iSup_torsionBySet_ideal_eq_torsionBySet_iInf hPairwise] at hmem

Goal state after:
A : Type u_1
M : Type u_2
inst✝³ : CommRing A
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : IsDedekindDomain A
h : IsTorsion A M
x : M
a : A
ha : a ∈ A⁰
ha0 : span {a} ≠ ⊥
this✝ : Fintype ↑(mulSupport fun v ↦ v.maxPowDividing (span {a})) := Finite.fintype ⋯
S : Finset (HeightOneSpectrum A) := (mulSupport fun v ↦ v.maxPowDividing (span {a})).toFinset
hmem : x ∈ ⨆ i ∈ S, torsionBySet A M ↑(i.maxPowDividing (span {a}))
this : ⨅ i, i.maxPowDividing (span {a}) = ⨅ i ∈ S, i.maxPowDividing (span {a})
hPairwise : (↑S).Pairwise fun i j ↦ i.maxPowDividing (span {a}) ⊔ j.maxPowDividing (span {a}) = ⊤
⊢ x ∈ ⨆ P, primaryComponent M P.asIdeal
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: case refine_1
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
this : ∀ (d : ℕ), BddAbove {m | ∃ y ∈ s, ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d} ∧ ∀ z ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d}, z ≤ f d
hf₁ : ∀ n > 0, ∃ y ∈ s, ↑(↑(f n) / ↑n) ≤ y
hf₂ : ∀ n > 0, ∀ y ∈ s, y - (↑n)⁻¹ < ↑(↑(f n) / ↑n)
hg : IsCauSeq abs fun n ↦ ↑(f n) / ↑n
g : CauSeq ℚ abs := ⟨fun n ↦ ↑(f n) / ↑n, hg⟩
x : ℝ
xS : x ∈ s
z : ℝ
K n : ℕ
nK : n ≥ K
xz : 0 < x - z
hK : (x - z)⁻¹ ≤ ↑n
n0 : 0 < n
⊢ z ≤ x - (↑n)⁻¹

Tactic:
le_sub_comm,

Goal state after:
case refine_1
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
this : ∀ (d : ℕ), BddAbove {m | ∃ y ∈ s, ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d} ∧ ∀ z ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d}, z ≤ f d
hf₁ : ∀ n > 0, ∃ y ∈ s, ↑(↑(f n) / ↑n) ≤ y
hf₂ : ∀ n > 0, ∀ y ∈ s, y - (↑n)⁻¹ < ↑(↑(f n) / ↑n)
hg : IsCauSeq abs fun n ↦ ↑(f n) / ↑n
g : CauSeq ℚ abs := ⟨fun n ↦ ↑(f n) / ↑n, hg⟩
x : ℝ
xS : x ∈ s
z : ℝ
K n : ℕ
nK : n ≥ K
xz : 0 < x - z
hK : (x - z)⁻¹ ≤ ↑n
n0 : 0 < n
⊢ (↑n)⁻¹ ≤ x - z
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: case neg
s : Set ℝ
hn : s.Nonempty
hb : ¬BddBelow s
⊢ sSup (-s) = -sInf s

Tactic:
· rw [csInf_of_not_bddBelow hb, Real.sInf_empty, csSup_of_not_bddAbove (bddAbove_neg.not.2 hb),
      Real.sSup_empty, neg_zero]

Goal state after: