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

Goal state before:
pp: 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✝¹ : IsFractionRing (A ⧸ P) K
inst✝ : IsFractionRing (B ⧸ Q) L
f : Gal(L/K)
val✝ : Fintype G
this✝ : P.IsPrime
this : Algebra.IsIntegral A B
x y : B ⧸ Q
hx :
  ∀ (g : ↥(MulAction.stabilizer G Q)),
    ((IsFractionRing.stabilizerHom G P Q K L) g) ((algebraMap (B ⧸ Q) L) x / (algebraMap (B ⧸ Q) L) y) =
      (algebraMap (B ⧸ Q) L) x / (algebraMap (B ⧸ Q) L) y
b : B ⧸ Q
a : A ⧸ P
h : a • x = b * y
ha : (algebraMap (A ⧸ P) L) a ≠ 0
hy : (algebraMap (B ⧸ Q) L) y ≠ 0
⊢ (algebraMap (B ⧸ Q) L) x / (algebraMap (B ⧸ Q) L) y = (algebraMap (B ⧸ Q) L) b / (algebraMap (A ⧸ P) L) a

Tactic:
Algebra.smul_def,

Goal state after:
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✝¹ : IsFractionRing (A ⧸ P) K
inst✝ : IsFractionRing (B ⧸ Q) L
f : Gal(L/K)
val✝ : Fintype G
this✝ : P.IsPrime
this : Algebra.IsIntegral A B
x y : B ⧸ Q
hx :
  ∀ (g : ↥(MulAction.stabilizer G Q)),
    ((IsFractionRing.stabilizerHom G P Q K L) g) ((algebraMap (B ⧸ Q) L) x / (algebraMap (B ⧸ Q) L) y) =
      (algebraMap (B ⧸ Q) L) x / (algebraMap (B ⧸ Q) L) y
b : B ⧸ Q
a : A ⧸ P
h : (algebraMap (A ⧸ P) (B ⧸ Q)) a * x = b * y
ha : (algebraMap (A ⧸ P) L) a ≠ 0
hy : (algebraMap (B ⧸ Q) L) y ≠ 0
⊢ (algebraMap (B ⧸ Q) L) x / (algebraMap (B ⧸ Q) L) y = (algebraMap (B ⧸ Q) L) b / (algebraMap (A ⧸ P) L) a
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: case inr.inr
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 : 1 ≤ a
⊢ a ^ p ^ k ≡ 1 [MOD p ^ k]

Tactic:
rw [← Nat.cast_one, ← Nat.cast_sub ha0, ZMod.isUnit_iff_coprime, hn] at h

Goal state after:
case inr.inr
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 : ¬(a - 1).Coprime (p ^ k)
ha0 : 1 ≤ a
⊢ a ^ p ^ k ≡ 1 [MOD p ^ k]
Module: Mathlib.LinearAlgebra.FreeModule.Finite.Quotient

Goal state before:
pp: case mp
ι : 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 ι
N : Submodule R M
b : Basis ι R M
h : finrank R ↥N = finrank R M
this : Fintype ι
a : ι → R := ⋯
b' : Basis ι R M := ⋯
ab : Basis ι R ↥N := ⋯
ab_eq : ∀ (i : ι), ↑((smithNormalFormBotBasis b h) i) = smithNormalFormCoeffs b h i • (smithNormalFormTopBasis b h) i
mem_I_iff : ∀ (x : M), x ∈ N ↔ ∀ (i : ι), a i ∣ (b'.repr x) i
N' : Submodule R (ι → R) := ⋯
x : ι → R
⊢ (∃ y, (∀ (i : ι), a i ∣ (b'.repr y) i) ∧ ⇑(b'.repr y) = x) → ∀ (i : ι), ∃ a_2, x i = a i * a_2

Tactic:
rintro ⟨y, hy, rfl⟩ i

Goal state after:
case mp
ι : 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 ι
N : Submodule R M
b : Basis ι R M
h : finrank R ↥N = finrank R M
this : Fintype ι
a : ι → R := smithNormalFormCoeffs b h
b' : Basis ι R M := smithNormalFormTopBasis b h
ab : Basis ι R ↥N := smithNormalFormBotBasis b h
ab_eq : ∀ (i : ι), ↑((smithNormalFormBotBasis b h) i) = smithNormalFormCoeffs b h i • (smithNormalFormTopBasis b h) i
mem_I_iff : ∀ (x : M), x ∈ N ↔ ∀ (i : ι), a i ∣ (b'.repr x) i
N' : Submodule R (ι → R) := pi Set.univ fun i ↦ R ∙ a i
y : M
hy : ∀ (i : ι), a i ∣ (b'.repr y) i
i : ι
⊢ ∃ a_1, (b'.repr y) i = a i * a_1
Module: Mathlib.RingTheory.Invariant.Basic

Goal state before:
pp: G : Type u_1
A : Type u_2
B : Type u_3
K : Type u_4
L : Type u_5
inst✝¹⁸ : Group G
inst✝¹⁷ : CommRing A
inst✝¹⁶ : CommRing B
inst✝¹⁵ : Algebra A B
inst✝¹⁴ : Field K
inst✝¹³ : Field L
inst✝¹² : Algebra K L
inst✝¹¹ : Algebra A K
inst✝¹⁰ : Algebra B L
inst✝⁹ : Algebra A L
inst✝⁸ : IsFractionRing A K
inst✝⁷ : IsFractionRing B L
inst✝⁶ : IsScalarTower A K L
inst✝⁵ : IsScalarTower A B L
inst✝⁴ : MulSemiringAction G B
inst✝³ : MulSemiringAction G L
inst✝² : SMulDistribClass G B L
hAB : Algebra.IsInvariant A B G
inst✝¹ : SMulCommClass G A B
inst✝ : Algebra.IsIntegral A B
hc : ∀ (a : A), (algebraMap K L) ((algebraMap A K) a) = (algebraMap B L) ((algebraMap A B) a)
this✝ : Nontrivial A
this : Nontrivial B
x y : B
hy : y ∈ nonZeroDivisors B
h : ∀ (g : G), g • ((algebraMap B L) x / (algebraMap B L) y) = (algebraMap B L) x / (algebraMap B L) y
hy' : (algebraMap B L) y ≠ 0
b : B
a : A
ha : a ≠ 0
hb : a • x = b * y
⊢ ∃ a, (algebraMap K L) a = (algebraMap B L) x / (algebraMap B L) y

Tactic:
Algebra.smul_def,

Goal state after:
G : Type u_1
A : Type u_2
B : Type u_3
K : Type u_4
L : Type u_5
inst✝¹⁸ : Group G
inst✝¹⁷ : CommRing A
inst✝¹⁶ : CommRing B
inst✝¹⁵ : Algebra A B
inst✝¹⁴ : Field K
inst✝¹³ : Field L
inst✝¹² : Algebra K L
inst✝¹¹ : Algebra A K
inst✝¹⁰ : Algebra B L
inst✝⁹ : Algebra A L
inst✝⁸ : IsFractionRing A K
inst✝⁷ : IsFractionRing B L
inst✝⁶ : IsScalarTower A K L
inst✝⁵ : IsScalarTower A B L
inst✝⁴ : MulSemiringAction G B
inst✝³ : MulSemiringAction G L
inst✝² : SMulDistribClass G B L
hAB : Algebra.IsInvariant A B G
inst✝¹ : SMulCommClass G A B
inst✝ : Algebra.IsIntegral A B
hc : ∀ (a : A), (algebraMap K L) ((algebraMap A K) a) = (algebraMap B L) ((algebraMap A B) a)
this✝ : Nontrivial A
this : Nontrivial B
x y : B
hy : y ∈ nonZeroDivisors B
h : ∀ (g : G), g • ((algebraMap B L) x / (algebraMap B L) y) = (algebraMap B L) x / (algebraMap B L) y
hy' : (algebraMap B L) y ≠ 0
b : B
a : A
ha : a ≠ 0
hb : (algebraMap A B) a * x = b * y
⊢ ∃ a, (algebraMap K L) a = (algebraMap B L) x / (algebraMap B L) y
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : DecidableEq α
s : Finset α
i : α → ℕ
p : α
hps : p ∉ s
is_prime : ∀ q ∈ insert p s, Prime q
is_coprime : ∀ q ∈ insert p s, ∀ q' ∈ insert p s, q ∣ q' → q = q'
hp : Prime p
d : α
hdprod : d ∣ ∏ p' ∈ s, p' ^ i p'
hd : Prime d
hdp : d ∣ p
q : α
q_mem : q ∈ s.val
q_mem' : q ^ i q ∈ Multiset.map (fun p' ↦ p' ^ i p') s.val
hdq : d ∣ q ^ i q
⊢ p ∈ s

Tactic:
replace hdq := hd.dvd_of_dvd_pow hdq

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : DecidableEq α
s : Finset α
i : α → ℕ
p : α
hps : p ∉ s
is_prime : ∀ q ∈ insert p s, Prime q
is_coprime : ∀ q ∈ insert p s, ∀ q' ∈ insert p s, q ∣ q' → q = q'
hp : Prime p
d : α
hdprod : d ∣ ∏ p' ∈ s, p' ^ i p'
hd : Prime d
hdp : d ∣ p
q : α
q_mem : q ∈ s.val
q_mem' : q ^ i q ∈ Multiset.map (fun p' ↦ p' ^ i p') s.val
hdq : d ∣ q
⊢ p ∈ s
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 : R
m : ↥M
e : z * (algebraMap R S) ↑(r, m).2 = (algebraMap R S) r
⊢ z = r • ↑((toInvSubmonoid M S) m)

Tactic:
Algebra.smul_def,

Goal state after:
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 : R
m : ↥M
e : z * (algebraMap R S) ↑(r, m).2 = (algebraMap R S) r
⊢ z = (algebraMap R S) r * ↑((toInvSubmonoid M S) m)
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.leftInv
⊢ ↑((S.leftInvEquiv hS) x) * ↑x = 1

Tactic:
by
  simpa only [leftInvEquiv_apply, fromCommLeftInv] using fromLeftInv_mul S x

Goal state after:
Module: Mathlib.RingTheory.HopkinsLevitzki

Goal state before:
pp: case zero
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
hn : Jac ^ 0 ≤ Module.annihilator R M
⊢ P M

Tactic:
Jac.pow_zero,

Goal state after:
case zero
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
hn : 1 ≤ Module.annihilator R M
⊢ P M
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
inst✝ : CharZero S
n : ℕ
⊢ {I | absNorm I = n}.Finite

Tactic:
by
  obtain hn | hn := Nat.eq_zero_or_pos n
  · simp only [hn, absNorm_eq_zero_iff, Set.ofPred_eq_eq_singleton, Set.finite_singleton]
  · let f := fun I : Ideal S => Ideal.map (Ideal.Quotient.mk (@Ideal.span S _ {↑n})) I
    refine Set.Finite.of_finite_image (f := f) ?_ ?_
    · suffices Finite (S ⧸ @Ideal.span S _ {↑n}) by
        let g := ((↑) : Ideal (S ⧸ @Ideal.span S _ {↑n}) → Set (S ⧸ @Ideal.span S _ {↑n}))
        refine Set.Finite.of_finite_image (f := g) ?_ SetLike.coe_injective.injOn
        exact Set.Finite.subset Set.finite_univ (Set.subset_univ _)
      rw [← absNorm_ne_zero_iff, absNorm_span_singleton]
      simpa only [Ne, Int.natAbs_eq_zero, Algebra.norm_eq_zero_iff, Nat.cast_eq_zero] using
        ne_of_gt hn
    · intro I hI J hJ h
      rw [← comap_map_mk (span_singleton_absNorm_le I), ← hI.symm, ←
        comap_map_mk (span_singleton_absNorm_le J), ← hJ.symm]
      congr

Goal state after:
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
p : Ideal R
S₁ : Type u_1
inst✝¹ : CommRing S₁
inst✝ : Algebra R S₁
e : S ≃ₐ[R] S₁
P : Ideal S₁
n : ℕ
⊢ p ≤ comap f (map (↑e.toRingEquiv.symm) (P ^ n)) ↔ p ≤ comap (algebraMap R S₁) (P ^ n)

Tactic:
map_comap_of_equiv,

Goal state after:
R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal R
S₁ : Type u_1
inst✝¹ : CommRing S₁
inst✝ : Algebra R S₁
e : S ≃ₐ[R] S₁
P : Ideal S₁
n : ℕ
⊢ p ≤ comap f (comap e.toRingEquiv.symm.symm (P ^ n)) ↔ p ≤ comap (algebraMap R S₁) (P ^ n)
Module: Mathlib.RingTheory.Ideal.IdempotentFG

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
h : I.FG
⊢ IsIdempotentElem I ↔ I = ⊥ ∨ I = ⊤

Tactic:
by
  constructor
  · intro H
    obtain ⟨e, he, rfl⟩ := (I.isIdempotentElem_iff_of_fg h).mp H
    simp only [Ideal.submodule_span_eq, Ideal.span_singleton_eq_bot]
    apply Or.imp id _ (IsIdempotentElem.iff_eq_zero_or_one.mp he)
    rintro rfl
    simp
  · rintro (rfl | rfl) <;> simp [IsIdempotentElem]

Goal state after:
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
inst✝¹ : IsDedekindDomain R
v : Ideal R
w : Ideal S
p : Ideal R
hv : Irreducible v
hp : Prime p
hvp : v ≠ p
inst✝ : w.LiesOver v
⊢ emultiplicity w (map f p) = 0

Tactic:
refine emultiplicity_eq_zero.2 fun h ↦ hvp.symm ?_

Goal state after:
R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsDedekindDomain S
inst✝¹ : IsDedekindDomain R
v : Ideal R
w : Ideal S
p : Ideal R
hv : Irreducible v
hp : Prime p
hvp : v ≠ p
inst✝ : w.LiesOver v
h : w ∣ map f p
⊢ p = v
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
inst✝² : FormallyUnramified R A
f : A →ₐ[R] B
H : Function.Surjective ⇑f
Q : Type u_3
inst✝¹ : CommRing Q
inst✝ : Algebra R Q
I : Ideal Q
hI : I ^ 2 = ⊥
f₁ f₂ : B →ₐ[R] Q
e : (Ideal.Quotient.mkₐ R I).comp f₁ = (Ideal.Quotient.mkₐ R I).comp f₂
x : A
⊢ f₁ (f x) = f₂ (f x)

Tactic:
← AlgHom.comp_apply,

Goal state after:
R : Type u_1
inst✝⁷ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
inst✝² : FormallyUnramified R A
f : A →ₐ[R] B
H : Function.Surjective ⇑f
Q : Type u_3
inst✝¹ : CommRing Q
inst✝ : Algebra R Q
I : Ideal Q
hI : I ^ 2 = ⊥
f₁ f₂ : B →ₐ[R] Q
e : (Ideal.Quotient.mkₐ R I).comp f₁ = (Ideal.Quotient.mkₐ R I).comp f₂
x : A
⊢ (f₁.comp f) x = f₂ (f x)
Module: Mathlib.RingTheory.Unramified.Finite

Goal state before:
pp: case e_g
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
I : Type u_4
inst✝ : DecidableEq I
b : Basis I R S
f : I →₀ S
x : S
a : I → I →₀ R := fun i ↦ b.repr (b i * x)
i j : I
s : S
⊢ ((b.repr s).sum fun i_1 a_1 ↦ ((a j) i * a_1) • b i_1 ⊗ₜ[R] b i) =
    (b.repr s).sum fun j_1 z ↦ (a j) i • z • b j_1 ⊗ₜ[R] b i

Tactic:
simp only [mul_smul, Finsupp.sum, ← Finset.smul_sum]

Goal state after:
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
g : A →ₐ[R] P.Ring ⧸ RingHom.ker (IsScalarTower.toAlgHom R P.Ring A).toRingHom ^ 2
hg : (IsScalarTower.toAlgHom R P.Ring A).kerSquareLift.comp g = AlgHom.id R A
σ : B ⧸ I → B := Function.surjInv ⋯
x : P.Ring
⊢ (aeval ((⇑(algebraMap B (B ⧸ I)) ∘ σ) ∘ ⇑f)) x = (aeval fun i ↦ f (P.val i)) x

Tactic:
Function.comp_surjInv,

Goal state after:
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
g : A →ₐ[R] P.Ring ⧸ RingHom.ker (IsScalarTower.toAlgHom R P.Ring A).toRingHom ^ 2
hg : (IsScalarTower.toAlgHom R P.Ring A).kerSquareLift.comp g = AlgHom.id R A
σ : B ⧸ I → B := Function.surjInv ⋯
x : P.Ring
⊢ (aeval (_root_.id ∘ ⇑f)) x = (aeval fun i ↦ f (P.val i)) x
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
C : Type u_4
inst✝² : CommRing C
inst✝¹ : Algebra R C
inst✝ : FormallySmooth R A
f : A →ₐ[R] C
g : B →ₐ[R] C
hg : Function.Surjective ⇑g
hg' : IsNilpotent (RingHom.ker g)
x : A
| ↑(Ideal.quotientKerAlgEquivOfSurjective hg).symm (f x)

Tactic:
← AlgHom.comp_apply,

Goal state after:
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
C : Type u_4
inst✝² : CommRing C
inst✝¹ : Algebra R C
inst✝ : FormallySmooth R A
f : A →ₐ[R] C
g : B →ₐ[R] C
hg : Function.Surjective ⇑g
hg' : IsNilpotent (RingHom.ker g)
x : A
| ((↑(Ideal.quotientKerAlgEquivOfSurjective hg).symm).comp f) x
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: case h2.refine_1
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 σ
x : (Q.comp P).Ring
hx' : x ∈ (Q.comp P).toExtension.ker
y : (Q.comp P).Ring
hy : y ∈ (Q.comp P).ker * (Q.comp P).ker
e : x - y ∈ Ideal.map (Q.toComp P).toAlgHom P.ker
z : ↥(Q.comp P).ker := ⟨x - y, ⋯⟩
hz : ↑z ∈ Ideal.map (Q.toComp P).toAlgHom.toRingHom P.ker
this : Extension.Cotangent.mk ⟨x, hx'⟩ = Extension.Cotangent.mk z
w : P.Ring
hw : w ∈ P.ker
⊢ (Q.toComp P).toAlgHom w ∈ (Q.comp P).toExtension.ker

Tactic:
simp only [ker_eq_ker_aeval_val, RingHom.mem_ker, Hom.algebraMap_toAlgHom]

Goal state after:
case h2.refine_1
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 σ
x : (Q.comp P).Ring
hx' : x ∈ (Q.comp P).toExtension.ker
y : (Q.comp P).Ring
hy : y ∈ (Q.comp P).ker * (Q.comp P).ker
e : x - y ∈ Ideal.map (Q.toComp P).toAlgHom P.ker
z : ↥(Q.comp P).ker := ⟨x - y, ⋯⟩
hz : ↑z ∈ Ideal.map (Q.toComp P).toAlgHom.toRingHom P.ker
this : Extension.Cotangent.mk ⟨x, hx'⟩ = Extension.Cotangent.mk z
w : P.Ring
hw : w ∈ P.ker
⊢ (algebraMap S T) ((aeval P.val) w) = 0
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: case h2.refine_1
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 σ
x : (Q.comp P).Ring
hx' : x ∈ (Q.comp P).toExtension.ker
y : (Q.comp P).Ring
hy : y ∈ (Q.comp P).ker * (Q.comp P).ker
e : x - y ∈ Ideal.map (Q.toComp P).toAlgHom P.ker
z : ↥(Q.comp P).ker := ⟨x - y, ⋯⟩
hz : ↑z ∈ Ideal.map (Q.toComp P).toAlgHom.toRingHom P.ker
this : Extension.Cotangent.mk ⟨x, hx'⟩ = Extension.Cotangent.mk z
w : P.Ring
hw : w ∈ P.ker
⊢ (Q.toComp P).toAlgHom w ∈ (Q.comp P).toExtension.ker

pp: case h2.refine_2
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 σ
x : (Q.comp P).Ring
hx' : x ∈ (Q.comp P).toExtension.ker
y : (Q.comp P).Ring
hy : y ∈ (Q.comp P).ker * (Q.comp P).ker
e : x - y ∈ Ideal.map (Q.toComp P).toAlgHom P.ker
z : ↥(Q.comp P).ker := ⟨x - y, ⋯⟩
hz : ↑z ∈ Ideal.map (Q.toComp P).toAlgHom.toRingHom P.ker
this : Extension.Cotangent.mk ⟨x, hx'⟩ = Extension.Cotangent.mk z
w : P.Ring
hw : w ∈ P.ker
⊢ (Extension.Cotangent.map (Q.toComp P).toExtensionHom) (Extension.Cotangent.mk ⟨w, hw⟩) =
    Extension.Cotangent.mk ⟨(Q.toComp P).toAlgHom w, ⋯⟩

Tactic:
· simp only [ker_eq_ker_aeval_val, RingHom.mem_ker, Hom.algebraMap_toAlgHom]
      rw [aeval_val_eq_zero hw, map_zero]

Goal state after:
case h2.refine_2
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 σ
x : (Q.comp P).Ring
hx' : x ∈ (Q.comp P).toExtension.ker
y : (Q.comp P).Ring
hy : y ∈ (Q.comp P).ker * (Q.comp P).ker
e : x - y ∈ Ideal.map (Q.toComp P).toAlgHom P.ker
z : ↥(Q.comp P).ker := ⟨x - y, ⋯⟩
hz : ↑z ∈ Ideal.map (Q.toComp P).toAlgHom.toRingHom P.ker
this : Extension.Cotangent.mk ⟨x, hx'⟩ = Extension.Cotangent.mk z
w : P.Ring
hw : w ∈ P.ker
⊢ (Extension.Cotangent.map (Q.toComp P).toExtensionHom) (Extension.Cotangent.mk ⟨w, hw⟩) =
    Extension.Cotangent.mk ⟨(Q.toComp P).toAlgHom w, ⋯⟩
Module: Mathlib.RingTheory.Unramified.Field

Goal state before:
pp: K : Type u_1
L : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FormallyUnramified K L
inst✝¹ : EssFiniteType K L
inst✝ : IsPurelyInseparable K L
this : Nontrivial (L ⊗[K] L)
x : L
a✝ : x ∈ ⊤
⊢ x ∈ (algebraMap K L).range

Tactic:
obtain ⟨n, hn⟩ := IsPurelyInseparable.pow_mem K (ringExpChar K) x

Goal state after:
K : Type u_1
L : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FormallyUnramified K L
inst✝¹ : EssFiniteType K L
inst✝ : IsPurelyInseparable K L
this : Nontrivial (L ⊗[K] L)
x : L
a✝ : x ∈ ⊤
n : ℕ
hn : x ^ ringExpChar K ^ n ∈ (algebraMap K L).range
⊢ x ∈ (algebraMap K L).range
Module: Mathlib.RingTheory.Unramified.LocalRing

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalRing R
inst✝³ : IsLocalRing S
inst✝² : IsLocalHom (algebraMap R S)
inst✝¹ : EssFiniteType R S
inst✝ : FormallyUnramified R S
mR : Ideal S := Ideal.map (algebraMap R S) (maximalIdeal R)
hmR : mR ≤ maximalIdeal S
this✝¹ : Algebra (ResidueField R) (S ⧸ mR) :=
  { smul := Quotient.lift₂ (fun x1 x2 ↦ ⟦x1 • x2⟧) ⋯,
    algebraMap := Ideal.quotientMap (Ideal.map (algebraMap R S) (maximalIdeal R)) (algebraMap R S) ⋯, commutes' := ⋯,
    smul_def' := ⋯ }
this✝ : IsScalarTower R (ResidueField R) (S ⧸ mR)
this : FormallyUnramified (ResidueField R) (S ⧸ mR)
⊢ IsField (S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R))

Tactic:
have : EssFiniteType (ResidueField R) (S ⧸ mR) := .of_comp R _ _

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalRing R
inst✝³ : IsLocalRing S
inst✝² : IsLocalHom (algebraMap R S)
inst✝¹ : EssFiniteType R S
inst✝ : FormallyUnramified R S
mR : Ideal S := Ideal.map (algebraMap R S) (maximalIdeal R)
hmR : mR ≤ maximalIdeal S
this✝² : Algebra (ResidueField R) (S ⧸ mR) :=
  { smul := Quotient.lift₂ (fun x1 x2 ↦ ⟦x1 • x2⟧) ⋯,
    algebraMap := Ideal.quotientMap (Ideal.map (algebraMap R S) (maximalIdeal R)) (algebraMap R S) ⋯, commutes' := ⋯,
    smul_def' := ⋯ }
this✝¹ : IsScalarTower R (ResidueField R) (S ⧸ mR)
this✝ : FormallyUnramified (ResidueField R) (S ⧸ mR)
this : EssFiniteType (ResidueField R) (S ⧸ mR)
⊢ IsField (S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R))