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

Goal state before:
pp: case neg
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : NoZeroDivisors B
b : B
i j : ℕ
p : A[X]
h : map (algebraMap A B) p = (X - C b) ^ i * X ^ j
f : B ≃ₐ[A] B
hi : i ≠ 0
ha : ¬b = 0
hf : 0 = (b - ↑↑f b) ^ i * b ^ j
⊢ f b = b

Tactic:
zero_eq_mul,

Goal state after:
case neg
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : NoZeroDivisors B
b : B
i j : ℕ
p : A[X]
h : map (algebraMap A B) p = (X - C b) ^ i * X ^ j
f : B ≃ₐ[A] B
hi : i ≠ 0
ha : ¬b = 0
hf : (b - ↑↑f b) ^ i = 0 ∨ b ^ j = 0
⊢ f b = b
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: K : Type u_1
inst✝³ : Ring K
inst✝² : NoZeroDivisors K
inst✝¹ : Nontrivial K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
⊢ ↑(Fintype.card ↥G) ≠ 0

Tactic:
by
  let n := Fintype.card G
  intro nzero
  have ⟨p, char_p⟩ := CharP.exists K
  have hd : p ∣ n := (CharP.cast_eq_zero_iff K p n).mp nzero
  cases CharP.char_is_prime_or_zero K p with
  | inr pzero =>
    exact (Fintype.card_pos).ne' <| Nat.eq_zero_of_zero_dvd <| pzero ▸ hd
  | inl pprime =>
    have fact_pprime := Fact.mk pprime
    -- G has an element x of order p by Cauchy's theorem
    have ⟨x, hx⟩ := exists_prime_orderOf_dvd_card p hd
    -- F has an element u (= ↑↑x) of order p
    let u := ((x : Kˣ) : K)
    have hu : orderOf u = p := by rwa [orderOf_units, Subgroup.orderOf_coe]
    -- u ^ p = 1 implies (u - 1) ^ p = 0 and hence u = 1 ...
    have h : u = 1 := by
      rw [← sub_left_inj, sub_self 1]
      apply eq_zero_of_pow_eq_zero (n := p)
      rw [sub_pow_char_of_commute, one_pow, ← hu, pow_orderOf_eq_one, sub_self]
      exact Commute.one_right u
    -- ... meaning x didn't have order p after all, contradiction
    apply pprime.one_lt.ne
    rw [← hu, h, orderOf_one]

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

Goal state before:
pp: case succ
K : Type u_1
inst✝¹ : GroupWithZero K
inst✝ : Fintype K
a : K
n : ℕ
ih : a ^ q ^ n = a
⊢ a ^ q ^ (n + 1) = a

Tactic:
simp [pow_succ, pow_mul, ih, pow_card]

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

Goal state before:
pp: K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
pb : PowerBasis K L
i j : Fin pb.dim
this :
  ∑ x, x pb.gen ^ ↑j / x ((aeval pb.gen) (derivative (minpoly K pb.gen))) * x ((minpolyDiv K pb.gen).coeff ↑i) =
    if j = i then 1 else 0
σ : L →ₐ[K] AlgebraicClosure K
a✝ : σ ∈ Finset.univ
⊢ σ ((minpolyDiv K pb.gen).coeff ↑i) / σ ((aeval pb.gen) (derivative (minpoly K pb.gen))) * σ pb.gen ^ ↑j =
    σ pb.gen ^ ↑j / σ ((aeval pb.gen) (derivative (minpoly K pb.gen))) * σ ((minpolyDiv K pb.gen).coeff ↑i)

Tactic:
ring

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

Goal state before:
pp: a b c : ℤ
h : a.gcd b = 1
heq : a * b = c ^ 2
⊢ IsUnit ↑1

Tactic:
Int.ofNat_one

Goal state after:
a b c : ℤ
h : a.gcd b = 1
heq : a * b = c ^ 2
⊢ IsUnit 1
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: case neg
K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : DecidableEq K
i : ℕ
φ : Kˣ →* K := { toFun := fun x ↦ ↑x ^ i, map_one' := ⋯, map_mul' := ⋯ }
this✝ : Decidable (φ = 1)
this : q - 1 ∣ i ↔ φ = 1
h✝ : ¬φ = 1
⊢ ↑0 = 0

Tactic:
exact Nat.cast_zero

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

Goal state before:
pp: m n : ℤ
p : ℕ
hp : Nat.Prime p
h : ↑p ∣ m * n
⊢ p ∣ m.natAbs ∨ p ∣ n.natAbs

Tactic:
exact Int.Prime.dvd_mul hp h

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

Goal state before:
pp: case refine_1
K : Type u_1
inst✝⁴ : Field K
inst✝³ : Fintype K
L : Type u_3
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Finite L
this : Fintype L
x : L
⊢ x ^ q ^ Module.finrank K L = x

Tactic:
← Module.card_eq_pow_finrank,

Goal state after:
case refine_1
K : Type u_1
inst✝⁴ : Field K
inst✝³ : Fintype K
L : Type u_3
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Finite L
this : Fintype L
x : L
⊢ x ^ Fintype.card L = x
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: case inl
hp : Fact (Nat.Prime 2)
x : ZMod 2
⊢ ∃ a b, a ^ 2 + b ^ 2 = x

Tactic:
change Fin 2 at x

Goal state after:
case inl
hp : Fact (Nat.Prime 2)
x : Fin 2
⊢ ∃ a b, a ^ 2 + b ^ 2 = x
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: case succ
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ZMod p
n : ℕ
ih : x ^ p ^ n = x
⊢ x ^ p ^ (n + 1) = x

Tactic:
simp [pow_succ, pow_mul, ih, pow_card]

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

Goal state before:
pp: case refine_2
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Free ℤ M
inst✝ : Module.Finite ℤ M
N : Submodule ℤ M
h : Finite (M ⧸ N)
⊢ Function.Injective ⇑(LinearMap.codRestrict N ((LinearMap.lsmul ℤ M) ↑(Nat.card (M ⧸ N))) ⋯)

Tactic:
· refine (LinearMap.lsmul_injective ?_).codRestrict _
    exact Int.ofNat_ne_zero.mpr <| Nat.card_ne_zero.mpr
      ⟨Set.nonempty_iff_univ_nonempty.mpr Set.univ_nonempty, h⟩

Goal state after:
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
⊢ LinearMap.det 0 = 0

Tactic:
LinearMap.det_zero' (Module.Free.chooseBasis R S)

Goal state after:
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
⊢ 0 = 0
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
this : a * d - a * d' ∈ P ^ (i + 1)
⊢ a * d + e - (a * d' + e') = a * d - a * d' + (e - e')

Tactic:
ring

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 : ℕ
a d d' e e' : S
a_notMem : a ∉ P ^ (i + 1)
e_mem : e ∈ P ^ (i + 1)
e'_mem : e' ∈ P ^ (i + 1)
h : a * d + e - (a * d' + e') ∈ P ^ (i + 1)
⊢ a * (d - d') = a * d + e - (a * d' + e') + (e' - e)

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

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

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
inst✝ : Module.Finite ℤ S
p : ℤ
hp✝ : Prime p
this✝¹ : IsAddTorsionFree S
this✝ : CharZero S
hpMax : (span {p}).IsMaximal
I P : Ideal S
hI' : I ≠ 0
hP : Prime P
IH : p ∣ ↑(absNorm I) → ∃ P, P.IsMaximal ∧ under ℤ P = span {p} ∧ P ∣ I
this : P.IsMaximal
q n : ℕ
hn : 0 < n
hqP : ↑q ∈ P
hq : Nat.Prime q
H : absNorm P = q ^ n
m : ℕ
hmn : m ≤ n
hp : Associated p (↑q ^ m)
h : m = 0
⊢ IsUnit p

Tactic:
by simpa [h] using hp

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
P : Ideal S
n : ℕ
hle : map f p ≤ P ^ n
hgt : ¬map f p ≤ P ^ (n + 1)
Q : ℕ → Prop := fun m ↦ ∀ (k : ℕ), map f p ≤ P ^ k → k ≤ m
this : Q n
⊢ Nat.find ⋯ = n

Tactic:
refine le_antisymm (Nat.find_min' _ this) (le_of_not_gt fun h : Nat.find _ < n => ?_)

Goal state after:
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : Ideal R
P : Ideal S
n : ℕ
hle : map f p ≤ P ^ n
hgt : ¬map f p ≤ P ^ (n + 1)
Q : ℕ → Prop := fun m ↦ ∀ (k : ℕ), map f p ≤ P ^ k → k ≤ m
this : Q n
h : Nat.find ⋯ < n
⊢ False
Module: Mathlib.RingTheory.LocalRing.Length

Goal state before:
pp: A : Type u_1
B : Type u_2
M : Type u_3
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : IsLocalRing A
inst✝⁵ : IsLocalRing B
inst✝⁴ : Algebra A B
inst✝³ : IsLocalHom (algebraMap A B)
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Flat A B
h : IsFiniteLength A M
s : CompositionSeries (Submodule A M)
hs_bot : RelSeries.head s = ⊥
hs_top : RelSeries.last s = ⊤
this :
  ∀ (k : Fin (s.length + 1)),
    length B ↥(Submodule.baseChange B (s.toFun k)) = ↑↑k * length B (B ⧸ Ideal.map (algebraMap A B) (maximalIdeal A))
⊢ length B (B ⊗[A] M) = length B ↥(Submodule.baseChange B (RelSeries.last s))

Tactic:
hs_top,

Goal state after:
A : Type u_1
B : Type u_2
M : Type u_3
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : IsLocalRing A
inst✝⁵ : IsLocalRing B
inst✝⁴ : Algebra A B
inst✝³ : IsLocalHom (algebraMap A B)
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Flat A B
h : IsFiniteLength A M
s : CompositionSeries (Submodule A M)
hs_bot : RelSeries.head s = ⊥
hs_top : RelSeries.last s = ⊤
this :
  ∀ (k : Fin (s.length + 1)),
    length B ↥(Submodule.baseChange B (s.toFun k)) = ↑↑k * length B (B ⧸ Ideal.map (algebraMap A B) (maximalIdeal A))
⊢ length B (B ⊗[A] M) = length B ↥(Submodule.baseChange B ⊤)
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
R : Type u_4
k : Type u_5
inst✝⁴ : CommRing R
inst✝³ : IsLocalRing R
inst✝² : Field k
inst✝¹ : Algebra R k
inst✝ : Module.Finite R k
⊢ Ideal.comap (algebraMap R k) ⊥ = RingHom.ker (algebraMap R k)

Tactic:
RingHom.ker

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
R : Type u_4
k : Type u_5
inst✝⁴ : CommRing R
inst✝³ : IsLocalRing R
inst✝² : Field k
inst✝¹ : Algebra R k
inst✝ : Module.Finite R k
⊢ Ideal.comap (algebraMap R k) ⊥ = Ideal.comap (algebraMap R k) ⊥
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
I p : Ideal R
hI : I ≠ 0
hp : Prime p
IH : I ≠ ⊥ → emultiplicity w (map f I) = ↑(v.ramificationIdx' w) * emultiplicity v I
h : p * I ≠ ⊥
⊢ emultiplicity w (map f p * map f I) = ↑(v.ramificationIdx' w) * emultiplicity v (p * I)

Tactic:
emultiplicity_mul hw.prime,

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
I p : Ideal R
hI : I ≠ 0
hp : Prime p
IH : I ≠ ⊥ → emultiplicity w (map f I) = ↑(v.ramificationIdx' w) * emultiplicity v I
h : p * I ≠ ⊥
⊢ emultiplicity w (map f p) + emultiplicity w (map f I) = ↑(v.ramificationIdx' w) * emultiplicity v (p * 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
inst✝² : IsDedekindDomain R
inst✝¹ : FaithfulSMul R S
v : Ideal R
w : Ideal S
I : Ideal R
h : I ≠ ⊥
hv : Irreducible v
hw : Irreducible w
hw_bot : w ≠ ⊥
inst✝ : w.LiesOver v
⊢ emultiplicity w (map f I) = ↑(v.ramificationIdx' w) * emultiplicity v I

Tactic:
by
  induction I using induction_on_prime with
  | h₁ => aesop
  | h₂ I hI =>
    obtain rfl : I = ⊤ := by simpa using hI
    simp_rw [Ideal.map_top, emultiplicity_eq_count_normalizedFactors hw top_ne_bot,
      emultiplicity_eq_count_normalizedFactors hv h, ← Ideal.one_eq_top, normalizedFactors_one]
    simp
  | h₃ I p hI hp IH =>
    rw [Ideal.map_mul, emultiplicity_mul hw.prime, emultiplicity_mul hv.prime, IH hI, mul_add,
      emultiplicity_map_eq_ramificationIdx'_mul_of_prime hv hp hw hw_bot]

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

Goal state before:
pp: case pos
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : QuasiFinite R S
I : Ideal R
h : I.IsPrime
⊢ I.primesOver S ⊆ PrimeSpectrum.asIdeal '' PrimeSpectrum.comap (algebraMap R S) ⁻¹' {{ asIdeal := I, isPrime := h }}

Tactic:
exact fun J hJ ↦ ⟨⟨_, hJ.1⟩, PrimeSpectrum.ext hJ.2.1.symm, rfl⟩

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

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✝⁴ : Algebra S T
inst✝³ : IsScalarTower R S T
inst✝² : Algebra.IsIntegral R S
inst✝¹ : FiniteType R T
s : S
inst✝ : IsLocalization.Away s T
A : Subalgebra R S := R[s]
sA : ↥A := ⟨s, ⋯⟩
f : Localization.Away sA →+* T := IsLocalization.Away.lift sA ⋯
this✝⁶ : Algebra (Localization.Away sA) T := f.toAlgebra
this✝⁵ : Algebra (↥A) (Localization.Away sA) := OreLocalization.instAlgebra
this✝⁴ : SMul (↥A) (Localization.Away sA) := this✝⁵.toSMul
this✝³ : MulAction (↥A) (Localization.Away sA) := toModule.toMulAction
this✝² : IsScalarTower R (↥A) (Localization.Away sA)
this✝¹ : IsScalarTower (↥A) (Localization.Away sA) T
this✝ : IsScalarTower R (Localization.Away sA) T
x : S
n : ℕ
this : IsIntegral (Localization.Away sA) ((algebraMap S T) x)
⊢ (algebraMap S T) s ^ n * (algebraMap (Localization.Away ⟨s, ⋯⟩) T) (Localization.Away.invSelf ⟨s, ⋯⟩) ^ n *
      (algebraMap S T) x =
    (algebraMap (Localization.Away ⟨s, ⋯⟩) T) (Localization.Away.invSelf ⟨s, ⋯⟩) ^ n *
      ((algebraMap S T) x * (algebraMap S T) s ^ n)

Tactic:
ring

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
inst✝² : FormallyUnramified R S
inst✝¹ : EssFiniteType R S
inst✝ : Free R S
I : Type u_2 := ⋯
b : Basis I R S := ⋯
f : I →₀ S
hf : elem R S = f.sum fun i x ↦ x ⊗ₜ[R] b i
x : S
a : I → I →₀ R := ⋯
F : I →₀ I →₀ R := ⋯
hG : ∀ j ∉ f.support.biUnion fun i ↦ (a i).support, b.repr (f.sum fun i y ↦ (a i) j • y) = 0
G : I →₀ I →₀ R := ⋯
this : ∀ (i : I), ((b.repr (x * f i)).sum fun j k ↦ k • b j ⊗ₜ[R] b i) = (x * f i) ⊗ₜ[R] b i
⊢ x ⊗ₜ[R] 1 * elem R S =
    ∑ a_1 ∈ f.support.biUnion fun i ↦ (a i).support,
      (b.repr (f.sum fun i y ↦ (a i) a_1 • y)).sum fun b' c ↦ c • b b' ⊗ₜ[R] b a_1

Tactic:
← one_tmul_mul_elem,

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : FormallyUnramified R S
inst✝¹ : EssFiniteType R S
inst✝ : Free R S
I : Type u_2 := Free.ChooseBasisIndex R S
b : Basis I R S := Free.chooseBasis R S
f : I →₀ S
hf : elem R S = f.sum fun i x ↦ x ⊗ₜ[R] b i
x : S
a : I → I →₀ R := fun i ↦ b.repr (b i * x)
F : I →₀ I →₀ R := Finsupp.onFinset f.support (fun j ↦ b.repr (x * f j)) ⋯
hG : ∀ j ∉ f.support.biUnion fun i ↦ (a i).support, b.repr (f.sum fun i y ↦ (a i) j • y) = 0
G : I →₀ I →₀ R :=
  Finsupp.onFinset (f.support.biUnion fun i ↦ (a i).support) (fun j ↦ b.repr (f.sum fun i y ↦ (a i) j • y)) ⋯
this : ∀ (i : I), ((b.repr (x * f i)).sum fun j k ↦ k • b j ⊗ₜ[R] b i) = (x * f i) ⊗ₜ[R] b i
⊢ 1 ⊗ₜ[R] x * elem R S =
    ∑ a_1 ∈ f.support.biUnion fun i ↦ (a i).support,
      (b.repr (f.sum fun i y ↦ (a i) a_1 • y)).sum fun b' c ↦ c • b b' ⊗ₜ[R] b a_1
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 = ⊥
⊢ Function.Surjective (Ideal.Quotient.mkₐ R I).comp

Tactic:
by
  intro f
  let P : Algebra.Generators R A A := Generators.self R A
  have hP : Function.Injective P.toExtension.cotangentComplex := by
    rw [← LinearMap.ker_eq_bot, ← Submodule.subsingleton_iff_eq_bot]
    exact FormallySmooth.subsingleton_h1Cotangent
  obtain ⟨l, hl⟩ := ((P.toExtension.exact_cotangentComplex_toKaehler.split_tfae'.out 0 1 rfl rfl).mp
    ⟨P.toExtension.subsingleton_h1Cotangent.mp FormallySmooth.subsingleton_h1Cotangent,
      Module.projective_lifting_property _ _ P.toExtension.toKaehler_surjective⟩).2
  obtain ⟨g, hg⟩ := retractionKerCotangentToTensorEquivSection (R := R) P.algebraMap_surjective
    ⟨⟨⟨Cotangent.val, by simp⟩, by simpa using! Cotangent.val_smul' (P := P.toExtension)⟩ ∘ₗ
      l.restrictScalars P.toExtension.Ring, LinearMap.ext fun x ↦ congr($hl x)⟩
  let σ := Function.surjInv (f := algebraMap B (B ⧸ I)) Ideal.Quotient.mk_surjective
  have H (x : P.Ring) : ↑(aeval (σ ∘ f) x) = f (algebraMap _ A x) := by
    rw [← Ideal.Quotient.algebraMap_eq, ← aeval_algebraMap_apply, P.algebraMap_eq,
      AlgHom.coe_toRingHom, comp_aeval_apply, ← Function.comp_assoc, Function.comp_surjInv,]
    simp [P]
  let l : P.Ring ⧸ (RingHom.ker (algebraMap P.Ring A)) ^ 2 →ₐ[R] B :=
    Ideal.Quotient.liftₐ _ (aeval (σ ∘ f)) <|
      have : RingHom.ker (algebraMap P.Ring A) ≤ I.comap (aeval (σ ∘ f)).toRingHom := fun x hx ↦ by
        simp_all [← Ideal.Quotient.eq_zero_iff_mem (I := I), -map_aeval]
      show RingHom.ker _ ^ 2 ≤ RingHom.ker _ from
        (Ideal.pow_right_mono this 2).trans ((Ideal.le_comap_pow _ _).trans_eq (hI ▸ rfl))
  have : f.comp (IsScalarTower.toAlgHom R P.Ring A).kerSquareLift =
      (Ideal.Quotient.mkₐ R _).comp l := by
    refine Ideal.Quotient.algHom_ext _ (MvPolynomial.algHom_ext fun i ↦ ?_)
    change f (algebraMap P.Ring A (.X i)) = algebraMap _ _ (MvPolynomial.aeval (σ ∘ f) (.X i))
    simpa using! (Function.surjInv_eq _ _).symm
  exact ⟨l.comp g, by rw [← AlgHom.comp_assoc, ← this, AlgHom.comp_assoc, hg, AlgHom.comp_id]⟩

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
P : Type u_2
inst✝⁴ : CommRing P
inst✝³ : Algebra R P
inst✝² : FormallySmooth R P
inst✝¹ : Algebra P A
inst✝ : IsScalarTower R P A
hf : Function.Surjective ⇑(algebraMap P A)
⊢ FormallySmooth R A ↔ ∃ l, l ∘ₗ kerCotangentToTensor R P A = LinearMap.id

Tactic:
by
  rw [formallySmooth_iff, and_comm,
    Module.Projective.iff_split_of_projective (KaehlerDifferential.mapBaseChange R P A)
      (mapBaseChange_surjective R P A hf), ← kerCotangentToTensor_injective_iff hf]
  convert!
    (((exact_kerCotangentToTensor_mapBaseChange R _ _ hf).split_tfae' (g :=
          (KaehlerDifferential.mapBaseChange R P A).restrictScalars P)).out
      0 1) using 2
  · rw [← (LinearMap.extendScalarsOfSurjectiveEquiv hf).exists_congr_right]
    simp [LinearMap.ext_iff]
  · rw [and_iff_right (by exact mapBaseChange_surjective R P A hf)]

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

Goal state before:
pp: R : Type u_1
P : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
g✝ : S →ₐ[R] P
f : P →ₐ[R] S
hf' : RingHom.ker f ^ 2 = ⊥
g : S →ₐ[R] P
hg : f.comp g = AlgHom.id R S
x y : P
⊢ x + y - (g (f x) + g (f y)) = x - g (f x) + (y - g (f y))

Tactic:
ring

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

Goal state before:
pp: R : Type u_1
P : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
g✝ : S →ₐ[R] P
f : P →ₐ[R] S
hf' : RingHom.ker f ^ 2 = ⊥
g : S →ₐ[R] P
hg : f.comp g = AlgHom.id R S
x : R
y : P
⊢ (algebraMap R P) x * y - (algebraMap R P) x * g (f y) = (algebraMap R P) x * (y - g (f y))

Tactic:
ring

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

Goal state before:
pp: R : Type u_1
P : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
g✝ : S →ₐ[R] P
f : P →ₐ[R] S
hf' : RingHom.ker f ^ 2 = ⊥
g : S →ₐ[R] P
hg : f.comp g = AlgHom.id R S
a b : P
this : (a - g (f a)) * (b - g (f b)) = 0
⊢ a * b - g (f a) * g (f b) - (a * b - a * g (f b) + (b * a - b * g (f a))) =
    a * g (f b) - g (f a) * g (f b) - (a * b - g (f a) * b)

Tactic:
ring

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

Goal state before:
pp: R : Type u_1
P : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))
hl : l ∘ₗ kerToTensor R P S = LinearMap.id
σ : S → P
hσ : ∀ (x : S), (algebraMap P S) (σ x) = x
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
a b : S
this : ∀ (x y : S ⊗[P] Ω[P⁄R]), ↑(l x) * ↑(l y) = 0
⊢ σ a * σ b - (σ a * ↑(l (1 ⊗ₜ[P] (D R P) (σ b))) + σ b * ↑(l (1 ⊗ₜ[P] (D R P) (σ a)))) =
    σ a * σ b - ↑(l (1 ⊗ₜ[P] (D R P) (σ a))) * σ b - σ a * ↑(l (1 ⊗ₜ[P] (D R P) (σ b)))

Tactic:
ring

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

Goal state before:
pp: R : Type u_1
P : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))
hl : l ∘ₗ kerToTensor R P S = LinearMap.id
σ : S → P
hσ : ∀ (x : S), (algebraMap P S) (σ x) = x
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
r : R
⊢ σ ((algebraMap R S) r) - ↑(l (1 ⊗ₜ[P] (D R P) (σ ((algebraMap R S) r)))) = (algebraMap R P) r

Tactic:
simp [sectionOfRetractionKerToTensorAux_prop l hl
      (σ (algebraMap R S r)) (algebraMap R P r) (by simp [hσ, ← IsScalarTower.algebraMap_apply])]

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

Goal state before:
pp: case tmul.tmul
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✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
P : Extension R S
Q : Extension R T
f : P.Hom Q
alg : Algebra P.Ring Q.Ring
halg : algebraMap P.Ring Q.Ring = f.toRingHom
H : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))
this✝¹ : Algebra P.Ring T := ((algebraMap S T).comp (algebraMap P.Ring S)).toAlgebra
this✝ : IsScalarTower P.Ring S T
this : IsScalarTower P.Ring Q.Ring T
e : Q.Ring ⊗[P.Ring] ↥P.ker ≃ₗ[Q.Ring] ↥Q.ker :=
  LinearEquiv.ofBijective (LinearMap.liftBaseChange Q.Ring (f.mapKer halg)) H
f' : ↥Q.ker →ₗ[Q.Ring] T ⊗[S] P.Cotangent :=
  LinearMap.liftBaseChange Q.Ring (↑P.Ring ((TensorProduct.mk S T P.Cotangent) 1) ∘ₗ Cotangent.mk) ∘ₗ ↑e.symm
a : Q.Ring
b : ↥P.ker
c : Q.Ring
d : ↥P.ker
h₂ : ↑b • Cotangent.mk d = 0
⊢ a • 0 = 0

Tactic:
smul_zero

Goal state after:
case tmul.tmul
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✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
P : Extension R S
Q : Extension R T
f : P.Hom Q
alg : Algebra P.Ring Q.Ring
halg : algebraMap P.Ring Q.Ring = f.toRingHom
H : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))
this✝¹ : Algebra P.Ring T := ((algebraMap S T).comp (algebraMap P.Ring S)).toAlgebra
this✝ : IsScalarTower P.Ring S T
this : IsScalarTower P.Ring Q.Ring T
e : Q.Ring ⊗[P.Ring] ↥P.ker ≃ₗ[Q.Ring] ↥Q.ker :=
  LinearEquiv.ofBijective (LinearMap.liftBaseChange Q.Ring (f.mapKer halg)) H
f' : ↥Q.ker →ₗ[Q.Ring] T ⊗[S] P.Cotangent :=
  LinearMap.liftBaseChange Q.Ring (↑P.Ring ((TensorProduct.mk S T P.Cotangent) 1) ∘ₗ Cotangent.mk) ∘ₗ ↑e.symm
a : Q.Ring
b : ↥P.ker
c : Q.Ring
d : ↥P.ker
h₂ : ↑b • Cotangent.mk d = 0
⊢ 0 = 0