awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.PowerSeries.Derivative
Goal:
A : Type u_1
inst : CommRing A
f g : A⟦X⟧
hg : HasSubst g
n m : ℕ
hm : ∀ b ≥ m, ∀ n' ≤ n + 1, Eq (α := A) ((coeff n' : (a : A⟦X⟧) → A) (g ^ b) : A) (0 : A)
this :
  Eq (α := A) ((coeff (n + 1) : (a : A⟦X⟧) → A) (subst g f) : A)
    ((coeff (n + 1) : (a : A⟦X⟧) → A) (subst (R := A) g (↑((trunc (m + 1) : (a : A⟦X⟧) → A[X]) f) : A⟦X⟧)) : A)
x : ℕ × ℕ
i j : ℕ
hij : (i, j) ∈ @Finset.antidiagonal _ instAddMonoid _ n
h :
  Eq.{u_1 + 1} (α := A)
    (∑ᶠ (d : ℕ),
      HSMul.hSMul (β := A)
        (HMul.hMul (α := A) (if d + 1 < m + 1 then (coeff (d + 1) : (a : A⟦X⟧) → A) f else 0 : A)
          (HAdd.hAdd (α := A) (↑d : A) 1))
        ((coeff i : (a : A⟦X⟧) → A) (g ^ d) : A))
    (∑ᶠ (d : ℕ),
      HSMul.hSMul (β := A) (HMul.hMul (α := A) ((coeff (d + 1) : (a : A⟦X⟧) → A) f : A) (HAdd.hAdd (α := A) (↑d : A) 1))
        ((coeff i : (a : A⟦X⟧) → A) (g ^ d) : A))
⊢ Eq (α := A)
    ((coeff (i, j).1 : (a : A⟦X⟧) → A)
        (subst (R := A) g ((d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) (↑((trunc (m + 1) : (a : A⟦X⟧) → A[X]) f) : A⟦X⟧))) :
      A)
    ((coeff (i, j).1 : (a : A⟦X⟧) → A) (subst (R := A) g ((d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) f)) : A)

Tactic:
simp only [coeff_subst' hg, coeff_derivative, coeff_coe, coeff_trunc]

Premises used: PowerSeries.coeff_trunc, PowerSeries.coeff_derivative, PowerSeries.coeff_subst', Polynomial.coeff_coe
-- Module: Mathlib.RingTheory.PowerSeries.Derivative
Goal:
A : Type u_1
inst : CommRing A
f g : A⟦X⟧
hg : HasSubst g
n m : ℕ
hm : ∀ b ≥ m, ∀ n' ≤ n + 1, Eq (α := A) ((coeff n' : (a : A⟦X⟧) → A) (g ^ b) : A) (0 : A)
this :
  Eq (α := A) ((coeff (n + 1) : (a : A⟦X⟧) → A) (subst g f) : A)
    ((coeff (n + 1) : (a : A⟦X⟧) → A) (subst (R := A) g (↑((trunc (m + 1) : (a : A⟦X⟧) → A[X]) f) : A⟦X⟧)) : A)
x : ℕ × ℕ
i j : ℕ
hij : (i, j) ∈ @Finset.antidiagonal _ instAddMonoid _ n
d : ℕ
pos :
  d + 1 < m + 1 →
    HSMul.hSMul (β := A) (HMul.hMul (α := A) ((coeff (d + 1) : (a : A⟦X⟧) → A) f : A) (HAdd.hAdd (α := A) (↑d : A) 1))
        ((coeff i : (a : A⟦X⟧) → A) (g ^ d) : A) =
      HSMul.hSMul (β := A) (HMul.hMul (α := A) ((coeff (d + 1) : (a : A⟦X⟧) → A) f : A) (HAdd.hAdd (α := A) (↑d : A) 1))
        ((coeff i : (a : A⟦X⟧) → A) (g ^ d) : A)
neg :
  ¬d + 1 < m + 1 →
    HSMul.hSMul (β := A) (0 * HAdd.hAdd (α := A) (↑d : A) 1) ((coeff i : (a : A⟦X⟧) → A) (g ^ d) : A) =
      HSMul.hSMul (β := A) (HMul.hMul (α := A) ((coeff (d + 1) : (a : A⟦X⟧) → A) f : A) (HAdd.hAdd (α := A) (↑d : A) 1))
        ((coeff i : (a : A⟦X⟧) → A) (g ^ d) : A)
⊢ HSMul.hSMul (β := A)
      (HMul.hMul (α := A) (if d + 1 < m + 1 then (coeff (d + 1) : (a : A⟦X⟧) → A) f else 0 : A)
        (HAdd.hAdd (α := A) (↑d : A) 1))
      ((coeff i : (a : A⟦X⟧) → A) (g ^ d) : A) =
    HSMul.hSMul (β := A) (HMul.hMul (α := A) ((coeff (d + 1) : (a : A⟦X⟧) → A) f : A) (HAdd.hAdd (α := A) (↑d : A) 1))
      ((coeff i : (a : A⟦X⟧) → A) (g ^ d) : A)

Tactic:
split_ifs
-- Module: Mathlib.RingTheory.PowerSeries.Derivative
Goal:
A : Type u_1
inst : CommRing A
f g : A⟦X⟧
hg : HasSubst g
n m : ℕ
hm : ∀ b ≥ m, ∀ n' ≤ n + 1, Eq (α := A) ((coeff n' : (a : A⟦X⟧) → A) (g ^ b) : A) (0 : A)
this :
  Eq (α := A) ((coeff (n + 1) : (a : A⟦X⟧) → A) (subst g f) : A)
    ((coeff (n + 1) : (a : A⟦X⟧) → A) (subst (R := A) g (↑((trunc (m + 1) : (a : A⟦X⟧) → A[X]) f) : A⟦X⟧)) : A)
x : ℕ × ℕ
i j : ℕ
hij : (i, j) ∈ @Finset.antidiagonal _ instAddMonoid _ n
d : ℕ
h : d + 1 < m + 1
⊢ HSMul.hSMul (β := A) (HMul.hMul (α := A) ((coeff (d + 1) : (a : A⟦X⟧) → A) f : A) (HAdd.hAdd (α := A) (↑d : A) 1))
      ((coeff i : (a : A⟦X⟧) → A) (g ^ d) : A) =
    HSMul.hSMul (β := A) (HMul.hMul (α := A) ((coeff (d + 1) : (a : A⟦X⟧) → A) f : A) (HAdd.hAdd (α := A) (↑d : A) 1))
      ((coeff i : (a : A⟦X⟧) → A) (g ^ d) : A)

Tactic:
simp (disch := grind [Finset.mem_antidiagonal]) [hm]

Premises used: Finset.HasAntidiagonal.mem_antidiagonal
-- Module: Mathlib.RingTheory.PowerSeries.Derivative
Goal:
A : Type u_1
inst : CommRing A
f g : A⟦X⟧
hg : HasSubst g
n m : ℕ
hm : ∀ b ≥ m, ∀ n' ≤ n + 1, Eq (α := A) ((coeff n' : (a : A⟦X⟧) → A) (g ^ b) : A) (0 : A)
this :
  Eq (α := A) ((coeff (n + 1) : (a : A⟦X⟧) → A) (subst g f) : A)
    ((coeff (n + 1) : (a : A⟦X⟧) → A) (subst (R := A) g (↑((trunc (m + 1) : (a : A⟦X⟧) → A[X]) f) : A⟦X⟧)) : A)
x : ℕ × ℕ
i j : ℕ
hij : (i, j) ∈ @Finset.antidiagonal _ instAddMonoid _ n
d : ℕ
h : ¬d + 1 < m + 1
⊢ HSMul.hSMul (β := A) (0 * HAdd.hAdd (α := A) (↑d : A) 1) ((coeff i : (a : A⟦X⟧) → A) (g ^ d) : A) =
    HSMul.hSMul (β := A) (HMul.hMul (α := A) ((coeff (d + 1) : (a : A⟦X⟧) → A) f : A) (HAdd.hAdd (α := A) (↑d : A) 1))
      ((coeff i : (a : A⟦X⟧) → A) (g ^ d) : A)

Tactic:
simp (disch := grind [Finset.mem_antidiagonal]) [hm]

Premises used: Finset.HasAntidiagonal.mem_antidiagonal
-- Module: Mathlib.RingTheory.PowerSeries.Derivative
Goal:
A : Type u_1
inst : CommRing A
f g : A⟦X⟧
hg : HasSubst g
n m : ℕ
hm : ∀ b ≥ m, ∀ n' ≤ n + 1, Eq (α := A) ((coeff n' : (a : A⟦X⟧) → A) (g ^ b) : A) (0 : A)
this :
  Eq (α := A) ((coeff (n + 1) : (a : A⟦X⟧) → A) (subst g f) : A)
    ((coeff (n + 1) : (a : A⟦X⟧) → A) (subst (R := A) g (↑((trunc (m + 1) : (a : A⟦X⟧) → A[X]) f) : A⟦X⟧)) : A)
x : ℕ × ℕ
i j : ℕ
hij : (i, j) ∈ @Finset.antidiagonal _ instAddMonoid _ n
⊢ Eq.{u_1 + 1} (α := A)
    (∑ᶠ (d : ℕ),
      HSMul.hSMul (β := A)
        (HMul.hMul (α := A) (if d + 1 < m + 1 then (coeff (d + 1) : (a : A⟦X⟧) → A) f else 0 : A)
          (HAdd.hAdd (α := A) (↑d : A) 1))
        ((coeff i : (a : A⟦X⟧) → A) (g ^ d) : A))
    (∑ᶠ (d : ℕ),
      HSMul.hSMul (β := A) (HMul.hMul (α := A) ((coeff (d + 1) : (a : A⟦X⟧) → A) f : A) (HAdd.hAdd (α := A) (↑d : A) 1))
        ((coeff i : (a : A⟦X⟧) → A) (g ^ d) : A))

Tactic:
exact finsum_congr fun d ↦ by split_ifs <;> simp (disch := grind [Finset.mem_antidiagonal]) [hm]

Premises used: finsum_congr
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
P : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing P
inst_2 : CommRing S
inst_3 : Algebra R P
inst_4 : Algebra P S
inst_5 : Algebra R S
inst_6 : IsScalarTower R P S
g_1 : S →ₐ[R] P
f : P →ₐ[R] S
hf' : HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker f) 2 = ⊥
g : S →ₐ[R] P
hg : f.comp g = AlgHom.id R S
x : P
⊢ Membership.mem (γ := Ideal P) (RingHom.ker f) (HSub.hSub (β := P) x ((g : (a : S) → P) ((f : (a : P) → S) x : S) : P))

Tactic:
simpa [RingHom.mem_ker, sub_eq_zero] using AlgHom.congr_fun hg.symm (f x)

Premises used: sub_eq_zero, RingHom.mem_ker, AlgHom.congr_fun, Eq.symm, DFunLike.coe
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
P : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing P
inst_2 : CommRing S
inst_3 : Algebra R P
inst_4 : Algebra P S
inst_5 : Algebra R S
inst_6 : IsScalarTower R P S
g_1 : S →ₐ[R] P
f : P →ₐ[R] S
hf' : HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker f) 2 = ⊥
g : S →ₐ[R] P
hg : f.comp g = AlgHom.id R S
x y : P
simp :
  x + y -
      HAdd.hAdd (α := P) (β := P) ((g : (a : S) → P) ((f : (a : P) → S) x : S) : P)
        ((g : (a : S) → P) ((f : (a : P) → S) y : S) : P) =
    HSub.hSub (β := P) x ((g : (a : S) → P) ((f : (a : P) → S) x : S) : P) +
      HSub.hSub (β := P) y ((g : (a : S) → P) ((f : (a : P) → S) y : S) : P)
⊢ Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := Ideal P) (RingHom.ker f) x)
      (HSub.hSub (β := P) (x + y) ((g : (a : S) → P) ((f : (a : P) → S) (x + y) : S) : P)) ⋯ =
    Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := Ideal P) (RingHom.ker f) x)
        (HSub.hSub (β := P) x ((g : (a : S) → P) ((f : (a : P) → S) x : S) : P)) ⋯ +
      Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := Ideal P) (RingHom.ker f) x)
        (HSub.hSub (β := P) y ((g : (a : S) → P) ((f : (a : P) → S) y : S) : P)) ⋯

Tactic:
simp only [map_add, AddMemClass.mk_add_mk, Subtype.mk.injEq]

Premises used: map_add, Subtype.mk.injEq, AddMemClass.mk_add_mk
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
P : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing P
inst_2 : CommRing S
inst_3 : Algebra R P
inst_4 : Algebra P S
inst_5 : Algebra R S
inst_6 : IsScalarTower R P S
g_1 : S →ₐ[R] P
f : P →ₐ[R] S
hf' : HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker f) 2 = ⊥
g : S →ₐ[R] P
hg : f.comp g = AlgHom.id R S
x y : P
⊢ x + y -
      HAdd.hAdd (α := P) (β := P) ((g : (a : S) → P) ((f : (a : P) → S) x : S) : P)
        ((g : (a : S) → P) ((f : (a : P) → S) y : S) : P) =
    HSub.hSub (β := P) x ((g : (a : S) → P) ((f : (a : P) → S) x : S) : P) +
      HSub.hSub (β := P) y ((g : (a : S) → P) ((f : (a : P) → S) y : S) : P)

Tactic:
ring
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
P : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing P
inst_2 : CommRing S
inst_3 : Algebra R P
inst_4 : Algebra P S
inst_5 : Algebra R S
inst_6 : IsScalarTower R P S
g_1 : S →ₐ[R] P
f : P →ₐ[R] S
hf' : HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker f) 2 = ⊥
g : S →ₐ[R] P
hg : f.comp g = AlgHom.id R S
x : R
y : P
a :
  (↑(Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := Ideal P) (RingHom.ker f) x)
          (HSub.hSub (β := P) (x • y) ((g : (a : S) → P) ((f : (a : P) → S) (x • y) : S) : P)) ⋯) :
      P) =
    (↑(HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) x : R)
          (Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := Ideal P) (RingHom.ker f) x)
            (HSub.hSub (β := P) y ((g : (a : S) → P) ((f : (a : P) → S) y : S) : P)) ⋯)) :
      P)
⊢ Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := Ideal P) (RingHom.ker f) x)
      (HSub.hSub (β := P) (x • y) ((g : (a : S) → P) ((f : (a : P) → S) (x • y) : S) : P)) ⋯ =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) x : R)
      (Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := Ideal P) (RingHom.ker f) x)
        (HSub.hSub (β := P) y ((g : (a : S) → P) ((f : (a : P) → S) y : S) : P)) ⋯)

Tactic:
ext
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
P : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing P
inst_2 : CommRing S
inst_3 : Algebra R P
inst_4 : Algebra P S
inst_5 : Algebra R S
inst_6 : IsScalarTower R P S
g_1 : S →ₐ[R] P
f : P →ₐ[R] S
hf' : HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker f) 2 = ⊥
g : S →ₐ[R] P
hg : f.comp g = AlgHom.id R S
x : R
y : P
a :
  HMul.hMul (α := P) ((algebraMap R P : (a : R) → P) x : P) y -
      HMul.hMul (α := P) (β := P) ((algebraMap R P : (a : R) → P) x : P)
        ((g : (a : S) → P) ((f : (a : P) → S) y : S) : P) =
    HMul.hMul (α := P) ((algebraMap R P : (a : R) → P) x : P)
      (HSub.hSub (β := P) y ((g : (a : S) → P) ((f : (a : P) → S) y : S) : P))
⊢ (↑(Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := Ideal P) (RingHom.ker f) x)
          (HSub.hSub (β := P) (x • y) ((g : (a : S) → P) ((f : (a : P) → S) (x • y) : S) : P)) ⋯) :
      P) =
    (↑(HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) x : R)
          (Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := Ideal P) (RingHom.ker f) x)
            (HSub.hSub (β := P) y ((g : (a : S) → P) ((f : (a : P) → S) y : S) : P)) ⋯)) :
      P)

Tactic:
simp only [Algebra.smul_def, map_mul, AlgHom.commutes,
      RingHom.id_apply, Submodule.coe_smul_of_tower]

Premises used: RingHom.id_apply, map_mul, Submodule.coe_smul_of_tower, AlgHom.commutes, Algebra.smul_def
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
P : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing P
inst_2 : CommRing S
inst_3 : Algebra R P
inst_4 : Algebra P S
inst_5 : Algebra R S
inst_6 : IsScalarTower R P S
g_1 : S →ₐ[R] P
f : P →ₐ[R] S
hf' : HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker f) 2 = ⊥
g : S →ₐ[R] P
hg : f.comp g = AlgHom.id R S
x : R
y : P
⊢ HMul.hMul (α := P) ((algebraMap R P : (a : R) → P) x : P) y -
      HMul.hMul (α := P) (β := P) ((algebraMap R P : (a : R) → P) x : P)
        ((g : (a : S) → P) ((f : (a : P) → S) y : S) : P) =
    HMul.hMul (α := P) ((algebraMap R P : (a : R) → P) x : P)
      (HSub.hSub (β := P) y ((g : (a : S) → P) ((f : (a : P) → S) y : S) : P))

Tactic:
ring
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
P : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing P
inst_2 : CommRing S
inst_3 : Algebra R P
inst_4 : Algebra P S
inst_5 : Algebra R S
inst_6 : IsScalarTower R P S
g_1 : S →ₐ[R] P
f : P →ₐ[R] S
hf' : HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker f) 2 = ⊥
g : S →ₐ[R] P
hg : f.comp g = AlgHom.id R S
⊢ Eq.{u_2 + 1} (α := ↥(RingHom.ker f))
    (({
          toFun := fun (x : P) ↦
            Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := Ideal P) (RingHom.ker f) x)
              (HSub.hSub (β := P) x ((g : (a : S) → P) ((f : (a : P) → S) x : S) : P)) ⋯,
          map_add' := ⋯, map_smul' := ⋯ } :
        (a : P) → ↥(RingHom.ker f))
      1)
    0

Tactic:
simp only [LinearMap.coe_mk, AddHom.coe_mk, map_one, sub_self,
    Submodule.mk_eq_zero]

Premises used: LinearMap.coe_mk, sub_self, map_one, AddHom.coe_mk, Submodule.mk_eq_zero
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
P : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing P
inst_2 : CommRing S
inst_3 : Algebra R P
inst_4 : Algebra P S
inst_5 : Algebra R S
inst_6 : IsScalarTower R P S
g_1 : S →ₐ[R] P
f : P →ₐ[R] S
hf' : HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker f) 2 = ⊥
g : S →ₐ[R] P
hg : f.comp g = AlgHom.id R S
a b : P
rw :
  HSub.hSub (β := P) a ((g : (a : S) → P) ((f : (a : P) → S) a : S) : P) *
      HSub.hSub (β := P) b ((g : (a : S) → P) ((f : (a : P) → S) b : S) : P) ∈
    HMul.hMul (α := Ideal P) (RingHom.ker f) (RingHom.ker f)
⊢ HSub.hSub (β := P) a ((g : (a : S) → P) ((f : (a : P) → S) a : S) : P) *
      HSub.hSub (β := P) b ((g : (a : S) → P) ((f : (a : P) → S) b : S) : P) =
    0

Tactic:
rw [← Ideal.mem_bot, ← hf', pow_two]

Premises used: Ideal.mem_bot, pow_two
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
P : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing P
inst_2 : CommRing S
inst_3 : Algebra R P
inst_4 : Algebra P S
inst_5 : Algebra R S
inst_6 : IsScalarTower R P S
g_1 : S →ₐ[R] P
f : P →ₐ[R] S
hf' : HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker f) 2 = ⊥
g : S →ₐ[R] P
hg : f.comp g = AlgHom.id R S
a b : P
hr :
  Membership.mem (γ := Ideal P) (RingHom.ker f) (HSub.hSub (β := P) a ((g : (a : S) → P) ((f : (a : P) → S) a : S) : P))
hs :
  Membership.mem (γ := Ideal P) (RingHom.ker f) (HSub.hSub (β := P) b ((g : (a : S) → P) ((f : (a : P) → S) b : S) : P))
⊢ HSub.hSub (β := P) a ((g : (a : S) → P) ((f : (a : P) → S) a : S) : P) *
      HSub.hSub (β := P) b ((g : (a : S) → P) ((f : (a : P) → S) b : S) : P) ∈
    HMul.hMul (α := Ideal P) (RingHom.ker f) (RingHom.ker f)

Tactic:
apply Ideal.mul_mem_mul

Premises used: Ideal.mul_mem_mul
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
P : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing P
inst_2 : CommRing S
inst_3 : Algebra R P
inst_4 : Algebra P S
inst_5 : Algebra R S
inst_6 : IsScalarTower R P S
g_1 : S →ₐ[R] P
f : P →ₐ[R] S
hf' : HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker f) 2 = ⊥
g : S →ₐ[R] P
hg : f.comp g = AlgHom.id R S
a b : P
⊢ Membership.mem (γ := Ideal P) (RingHom.ker f) (HSub.hSub (β := P) a ((g : (a : S) → P) ((f : (a : P) → S) a : S) : P))

Tactic:
simpa [RingHom.mem_ker, sub_eq_zero] using AlgHom.congr_fun hg.symm (f a)

Premises used: sub_eq_zero, RingHom.mem_ker, AlgHom.congr_fun, Eq.symm, DFunLike.coe
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
P : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing P
inst_2 : CommRing S
inst_3 : Algebra R P
inst_4 : Algebra P S
inst_5 : Algebra R S
inst_6 : IsScalarTower R P S
g_1 : S →ₐ[R] P
f : P →ₐ[R] S
hf' : HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker f) 2 = ⊥
g : S →ₐ[R] P
hg : f.comp g = AlgHom.id R S
a b : P
⊢ Membership.mem (γ := Ideal P) (RingHom.ker f) (HSub.hSub (β := P) b ((g : (a : S) → P) ((f : (a : P) → S) b : S) : P))

Tactic:
simpa [RingHom.mem_ker, sub_eq_zero] using AlgHom.congr_fun hg.symm (f b)

Premises used: sub_eq_zero, RingHom.mem_ker, AlgHom.congr_fun, Eq.symm, DFunLike.coe
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
P : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing P
inst_2 : CommRing S
inst_3 : Algebra R P
inst_4 : Algebra P S
inst_5 : Algebra R S
inst_6 : IsScalarTower R P S
g_1 : S →ₐ[R] P
f : P →ₐ[R] S
hf' : HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker f) 2 = ⊥
g : S →ₐ[R] P
hg : f.comp g = AlgHom.id R S
a b : P
⊢ HSub.hSub (β := P) a ((g : (a : S) → P) ((f : (a : P) → S) a : S) : P) *
      HSub.hSub (β := P) b ((g : (a : S) → P) ((f : (a : P) → S) b : S) : P) =
    0

Tactic:
have : (a - g (f a)) * (b - g (f b)) = 0 := by
      rw [← Ideal.mem_bot, ← hf', pow_two]
      apply Ideal.mul_mem_mul
      · simpa [RingHom.mem_ker, sub_eq_zero] using AlgHom.congr_fun hg.symm (f a)
      · simpa [RingHom.mem_ker, sub_eq_zero] using AlgHom.congr_fun hg.symm (f b)
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
P : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing P
inst_2 : CommRing S
inst_3 : Algebra R P
inst_4 : Algebra P S
inst_5 : Algebra R S
inst_6 : IsScalarTower R P S
g_1 : S →ₐ[R] P
f : P →ₐ[R] S
hf' : HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker f) 2 = ⊥
g : S →ₐ[R] P
hg : f.comp g = AlgHom.id R S
a b : P
this :
  HSub.hSub (β := P) a ((g : (a : S) → P) ((f : (a : P) → S) a : S) : P) *
      HSub.hSub (β := P) b ((g : (a : S) → P) ((f : (a : P) → S) b : S) : P) =
    0
a₁ :
  (↑(({
              toFun := fun (x : P) ↦
                Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := Ideal P) (RingHom.ker f) x)
                  (HSub.hSub (β := P) x ((g : (a : S) → P) ((f : (a : P) → S) x : S) : P)) ⋯,
              map_add' := ⋯, map_smul' := ⋯ } :
            (a : P) → ↥(RingHom.ker f))
          (a * b)) :
      P) =
    (↑(HSMul.hSMul (β := ↥(RingHom.ker f)) a
            (({
                    toFun := fun (x : P) ↦
                      Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := Ideal P) (RingHom.ker f) x)
                        (HSub.hSub (β := P) x ((g : (a : S) → P) ((f : (a : P) → S) x : S) : P)) ⋯,
                    map_add' := ⋯, map_smul' := ⋯ : P →ₗ[R] ↥(RingHom.ker f) } :
                  (a : P) → ↥(RingHom.ker f))
                b :
              ↥(RingHom.ker f)) +
          HSMul.hSMul (β := ↥(RingHom.ker f)) b
            (({
                    toFun := fun (x : P) ↦
                      Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := Ideal P) (RingHom.ker f) x)
                        (HSub.hSub (β := P) x ((g : (a : S) → P) ((f : (a : P) → S) x : S) : P)) ⋯,
                    map_add' := ⋯, map_smul' := ⋯ : P →ₗ[R] ↥(RingHom.ker f) } :
                  (a : P) → ↥(RingHom.ker f))
                a :
              ↥(RingHom.ker f))) :
      P)
⊢ ({
          toFun := fun (x : P) ↦
            Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := Ideal P) (RingHom.ker f) x)
              (HSub.hSub (β := P) x ((g : (a : S) → P) ((f : (a : P) → S) x : S) : P)) ⋯,
          map_add' := ⋯, map_smul' := ⋯ } :
        (a : P) → ↥(RingHom.ker f))
      (a * b) =
    HSMul.hSMul (β := ↥(RingHom.ker f)) a
        (({
                toFun := fun (x : P) ↦
                  Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := Ideal P) (RingHom.ker f) x)
                    (HSub.hSub (β := P) x ((g : (a : S) → P) ((f : (a : P) → S) x : S) : P)) ⋯,
                map_add' := ⋯, map_smul' := ⋯ : P →ₗ[R] ↥(RingHom.ker f) } :
              (a : P) → ↥(RingHom.ker f))
            b :
          ↥(RingHom.ker f)) +
      HSMul.hSMul (β := ↥(RingHom.ker f)) b
        (({
                toFun := fun (x : P) ↦
                  Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := Ideal P) (RingHom.ker f) x)
                    (HSub.hSub (β := P) x ((g : (a : S) → P) ((f : (a : P) → S) x : S) : P)) ⋯,
                map_add' := ⋯, map_smul' := ⋯ : P →ₗ[R] ↥(RingHom.ker f) } :
              (a : P) → ↥(RingHom.ker f))
            a :
          ↥(RingHom.ker f))

Tactic:
ext
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
P : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing P
inst_2 : CommRing S
inst_3 : Algebra R P
inst_4 : Algebra P S
inst_5 : Algebra R S
inst_6 : IsScalarTower R P S
g_1 : S →ₐ[R] P
f : P →ₐ[R] S
hf' : HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker f) 2 = ⊥
g : S →ₐ[R] P
hg : f.comp g = AlgHom.id R S
a b : P
this :
  HSub.hSub (β := P) a ((g : (a : S) → P) ((f : (a : P) → S) a : S) : P) *
      HSub.hSub (β := P) b ((g : (a : S) → P) ((f : (a : P) → S) b : S) : P) =
    0
rw :
  -(HSub.hSub (β := P) a ((g : (a : S) → P) ((f : (a : P) → S) a : S) : P) *
      HSub.hSub (β := P) b ((g : (a : S) → P) ((f : (a : P) → S) b : S) : P))
| 0

Tactic:
rw [← neg_zero, ← this]

Premises used: neg_zero
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
P : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing P
inst_2 : CommRing S
inst_3 : Algebra R P
inst_4 : Algebra P S
inst_5 : Algebra R S
inst_6 : IsScalarTower R P S
g_1 : S →ₐ[R] P
f : P →ₐ[R] S
hf' : HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker f) 2 = ⊥
g : S →ₐ[R] P
hg : f.comp g = AlgHom.id R S
a b : P
this :
  HSub.hSub (β := P) a ((g : (a : S) → P) ((f : (a : P) → S) a : S) : P) *
      HSub.hSub (β := P) b ((g : (a : S) → P) ((f : (a : P) → S) b : S) : P) =
    0
a₁ :
  a * b -
        HMul.hMul (α := P) (β := P) ((g : (a : S) → P) ((f : (a : P) → S) a : S) : P)
          ((g : (a : S) → P) ((f : (a : P) → S) b : S) : P) -
      (a * b - HMul.hMul (β := P) a ((g : (a : S) → P) ((f : (a : P) → S) b : S) : P) +
        (b * a - HMul.hMul (β := P) b ((g : (a : S) → P) ((f : (a : P) → S) a : S) : P))) =
    HMul.hMul (β := P) a ((g : (a : S) → P) ((f : (a : P) → S) b : S) : P) -
        HMul.hMul (α := P) (β := P) ((g : (a : S) → P) ((f : (a : P) → S) a : S) : P)
          ((g : (a : S) → P) ((f : (a : P) → S) b : S) : P) -
      (a * b - HMul.hMul (α := P) ((g : (a : S) → P) ((f : (a : P) → S) a : S) : P) b)
⊢ (↑(({
                toFun := fun (x : P) ↦
                  Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := Ideal P) (RingHom.ker f) x)
                    (HSub.hSub (β := P) x ((g : (a : S) → P) ((f : (a : P) → S) x : S) : P)) ⋯,
                map_add' := ⋯, map_smul' := ⋯ : P →ₗ[R] ↥(RingHom.ker f) } :
              (a : P) → ↥(RingHom.ker f))
            (a * b)) :
        P) -
      (↑(HSMul.hSMul (β := ↥(RingHom.ker f)) a
              (({
                      toFun := fun (x : P) ↦
                        Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := Ideal P) (RingHom.ker f) x)
                          (HSub.hSub (β := P) x ((g : (a : S) → P) ((f : (a : P) → S) x : S) : P)) ⋯,
                      map_add' := ⋯, map_smul' := ⋯ : P →ₗ[R] ↥(RingHom.ker f) } :
                    (a : P) → ↥(RingHom.ker f))
                  b :
                ↥(RingHom.ker f)) +
            HSMul.hSMul (β := ↥(RingHom.ker f)) b
              (({
                      toFun := fun (x : P) ↦
                        Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := Ideal P) (RingHom.ker f) x)
                          (HSub.hSub (β := P) x ((g : (a : S) → P) ((f : (a : P) → S) x : S) : P)) ⋯,
                      map_add' := ⋯, map_smul' := ⋯ : P →ₗ[R] ↥(RingHom.ker f) } :
                    (a : P) → ↥(RingHom.ker f))
                  a :
                ↥(RingHom.ker f))) :
        P) =
    -(HSub.hSub (β := P) a ((g : (a : S) → P) ((f : (a : P) → S) a : S) : P) *
        HSub.hSub (β := P) b ((g : (a : S) → P) ((f : (a : P) → S) b : S) : P))

Tactic:
simp only [LinearMap.coe_mk, AddHom.coe_mk, map_mul, SetLike.mk_smul_mk, smul_eq_mul, mul_sub,
      AddMemClass.mk_add_mk, sub_mul, neg_sub]

Premises used: LinearMap.coe_mk, neg_sub, mul_sub, sub_mul, map_mul, AddMemClass.mk_add_mk, smul_eq_mul, AddHom.coe_mk, SetLike.mk_smul_mk