awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basis (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ_1 : Type u_3
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
⊢ ∀ (a : MvPolynomial ι R),
    Membership.mem (γ := Ideal (MvPolynomial ι R))
        (Ideal.span
          (Set.range (ι := σ)
            (Subtype.val (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) ∘
              D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent))))
        a →
      Eq.{u_2 + 1} (α := S) ((aeval P.val : (a : MvPolynomial ι R) → S) a : S) (0 : S)
have simp_rw : ∀ (y : σ),
  (Subtype.val (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) ∘
        D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent))
      y ∈
    (↑(RingHom.ker (F := MvPolynomial ι R →ₐ[R] S) (aeval P.val)) : Set P.toExtension.Ring)
Tactic: simp_rw [← RingHom.mem_ker, ← SetLike.le_def, Ideal.span_le, Set.range_subset_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basis (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ_1 : Type u_3
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
⊢ IsScalarTower P.Ring D.T S
have refine : ∀ (x : P.Ring) (y : D.T) (z : S), (x • y) • z = x • y • z
Tactic: refine ⟨fun x y z ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basis (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ_1 : Type u_3
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
x : P.Ring
y : D.T
z : S
⊢ (x • y) • z = x • y • z
have obtain : ∀ (y : MvPolynomial ι R),
  HSMul.hSMul (β := D.T) x
        ((Ideal.Quotient.mk
                (Ideal.span
                  (Set.range (ι := σ)
                    (Subtype.val (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) ∘
                      D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent)))) :
              (a : MvPolynomial ι R) →
                MvPolynomial ι R ⧸
                  Ideal.span (Set.range (Subtype.val ∘ D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent))))
            y :
          HasQuotient.Quotient (MvPolynomial ι R) (B := Ideal (MvPolynomial ι R))
            (Ideal.span
              (Set.range (ι := σ)
                (Subtype.val (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) ∘
                  D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent))))) •
      z =
    x •
      HSMul.hSMul (α := D.T)
        ((Ideal.Quotient.mk
                (Ideal.span
                  (Set.range (ι := σ)
                    (Subtype.val (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) ∘
                      D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent)))) :
              (a : MvPolynomial ι R) →
                MvPolynomial ι R ⧸
                  Ideal.span (Set.range (Subtype.val ∘ D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent))))
            y :
          HasQuotient.Quotient (MvPolynomial ι R) (B := Ideal (MvPolynomial ι R))
            (Ideal.span
              (Set.range (ι := σ)
                (Subtype.val (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) ∘
                  D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent)))))
        z
Tactic: obtain ⟨y, rfl⟩ := Ideal.Quotient.mk_surjective y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basis (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ_1 : Type u_3
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
⊢ IsLocalization.Away D.gbar S
have refine_1 : Function.Surjective (α := D.T) (β := S) (⇑(algebraMap D.T S) : (a : D.T) → S)
Tactic: refine .of_surjective_of_isScalarTower (n := 1) ?_ ?_ _ ?_ (by simpa using D.hg)
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basis (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ_1 : Type u_3
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
refine_1 : Function.Surjective (α := D.T) (β := S) (⇑(algebraMap D.T S) : (a : D.T) → S)
⊢ IsLocalization.Away D.gbar S
have refine_2 : Function.Surjective (α := P.Ring) (β := D.T) (⇑(algebraMap P.Ring D.T) : (a : P.Ring) → D.T)
Tactic: refine .of_surjective_of_isScalarTower (n := 1) ?_ ?_ _ ?_ (by simpa using D.hg)
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basis (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ_1 : Type u_3
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
refine_1 : Function.Surjective (α := D.T) (β := S) (⇑(algebraMap D.T S) : (a : D.T) → S)
refine_2 : Function.Surjective (α := P.Ring) (β := D.T) (⇑(algebraMap P.Ring D.T) : (a : P.Ring) → D.T)
⊢ IsLocalization.Away D.gbar S
have refine_3 : IsUnit.{u_2} (M := S) ((algebraMap P.Ring S : (a : P.Ring) → S) D.g : S)
Tactic: refine .of_surjective_of_isScalarTower (n := 1) ?_ ?_ _ ?_ (by simpa using D.hg)
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basis (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ_1 : Type u_3
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
⊢ Function.Surjective (α := D.T) (β := S) (⇑(algebraMap D.T S) : (a : D.T) → S)
have refine_1 : Function.Surjective (α := P.Ring) (β := S)
  (Function.comp (β := D.T) (⇑(algebraMap D.T S) : (a : D.T) → S) (⇑(algebraMap P.Ring D.T) : (a : P.Ring) → D.T))
Tactic: refine .of_comp (g := algebraMap P.Ring D.T) ?_
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basis (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ_1 : Type u_3
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
⊢ Function.Surjective (α := P.Ring) (β := S)
    (Function.comp (β := D.T) (⇑(algebraMap D.T S) : (a : D.T) → S) (⇑(algebraMap P.Ring D.T) : (a : P.Ring) → D.T))
have h : Eq (α := P.Ring → S)
  (Function.comp (β := D.T) (⇑(algebraMap D.T S) : (a : D.T) → S) (⇑(algebraMap P.Ring D.T) : (a : P.Ring) → D.T))
  (⇑(algebraMap P.Ring S) : (a : P.Ring) → S)
Tactic: convert! P.algebraMap_surjective
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basis (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ_1 : Type u_3
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
⊢ Eq (α := P.Ring → S)
    (Function.comp (β := D.T) (⇑(algebraMap D.T S) : (a : D.T) → S) (⇑(algebraMap P.Ring D.T) : (a : P.Ring) → D.T))
    (⇑(algebraMap P.Ring S) : (a : P.Ring) → S)
have h : ∀ (x : P.Ring),
  Eq.{u_2 + 1} (α := S)
    (Function.comp (β := D.T) (⇑(algebraMap D.T S) : (a : D.T) → S) (⇑(algebraMap P.Ring D.T) : (a : P.Ring) → D.T) x :
      S)
    ((algebraMap P.Ring S : (a : P.Ring) → S) x : S)
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basis (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ_1 : Type u_3
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
⊢ IsUnit.{u_2} (M := S) ((algebraMap P.Ring S : (a : P.Ring) → S) D.g : S)
have refine_3 : Eq.{u_2 + 1} (α := S) ((algebraMap P.Ring S : (a : P.Ring) → S) D.g : S) (1 : S)
Tactic: suffices h : (algebraMap P.Ring S) D.g = 1 by simp [h]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basis (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ_1 : Type u_3
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
⊢ Eq.{u_2 + 1} (α := S) ((algebraMap P.Ring S : (a : P.Ring) → S) D.g : S) (1 : S)
have refine_3 : Membership.mem (γ := Ideal P.Ring) (RingHom.ker (F := P.Ring →+* S) (algebraMap P.Ring S)) (D.g - 1)
Tactic: rw [← map_one (algebraMap P.Ring S), ← sub_eq_zero, ← map_sub, ← RingHom.mem_ker]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basis (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ_1 : Type u_3
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
x :
  HasQuotient.Quotient (MvPolynomial ι R) (B := Ideal (MvPolynomial ι R))
    (Ideal.span
      (Set.range (ι := σ)
        (Subtype.val (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) ∘
          D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent))))
⊢ (Ideal.Quotient.mk
          (Ideal.span
            (Set.range (ι := σ)
              (Subtype.val (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) ∘
                D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent)))) :
        (a : MvPolynomial ι R) →
          MvPolynomial ι R ⧸ Ideal.span (Set.range (Subtype.val ∘ D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent))))
      (if x = 0 then 0
      else
        if x = -1 then -1
        else
          Function.surjInv (f :=
            (⇑(Ideal.Quotient.mk
                  (Ideal.span
                    (Set.range (ι := σ)
                      (Subtype.val (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) ∘
                        D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent))))) :
              (a : MvPolynomial ι R) →
                MvPolynomial ι R ⧸
                  Ideal.span (Set.range (Subtype.val ∘ D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent)))))
            ⋯ x) =
    x
have pos : x = 0 →
  (Ideal.Quotient.mk
          (Ideal.span
            (Set.range (ι := σ)
              (Subtype.val (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) ∘
                D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent)))) :
        (a : MvPolynomial ι R) →
          MvPolynomial ι R ⧸ Ideal.span (Set.range (Subtype.val ∘ D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent))))
      0 =
    x
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basis (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ_1 : Type u_3
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
x :
  HasQuotient.Quotient (MvPolynomial ι R) (B := Ideal (MvPolynomial ι R))
    (Ideal.span
      (Set.range (ι := σ)
        (Subtype.val (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) ∘
          D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent))))
pos :
  x = 0 →
    (Ideal.Quotient.mk
            (Ideal.span
              (Set.range (ι := σ)
                (Subtype.val (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) ∘
                  D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent)))) :
          (a : MvPolynomial ι R) →
            MvPolynomial ι R ⧸ Ideal.span (Set.range (Subtype.val ∘ D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent))))
        0 =
      x
⊢ (Ideal.Quotient.mk
          (Ideal.span
            (Set.range (ι := σ)
              (Subtype.val (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) ∘
                D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent)))) :
        (a : MvPolynomial ι R) →
          MvPolynomial ι R ⧸ Ideal.span (Set.range (Subtype.val ∘ D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent))))
      (if x = 0 then 0
      else
        if x = -1 then -1
        else
          Function.surjInv (f :=
            (⇑(Ideal.Quotient.mk
                  (Ideal.span
                    (Set.range (ι := σ)
                      (Subtype.val (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) ∘
                        D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent))))) :
              (a : MvPolynomial ι R) →
                MvPolynomial ι R ⧸
                  Ideal.span (Set.range (Subtype.val ∘ D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent)))))
            ⋯ x) =
    x
have pos₁ : ¬x = 0 →
  x = -1 →
    (Ideal.Quotient.mk
            (Ideal.span
              (Set.range (ι := σ)
                (Subtype.val (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) ∘
                  D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent)))) :
          (a : MvPolynomial ι R) →
            MvPolynomial ι R ⧸ Ideal.span (Set.range (Subtype.val ∘ D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent))))
        (-1) =
      x
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basis (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ_1 : Type u_3
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
x :
  HasQuotient.Quotient (MvPolynomial ι R) (B := Ideal (MvPolynomial ι R))
    (Ideal.span
      (Set.range (ι := σ)
        (Subtype.val (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) ∘
          D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent))))
h : x = 0
⊢ (Ideal.Quotient.mk
          (Ideal.span
            (Set.range (ι := σ)
              (Subtype.val (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) ∘
                D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent)))) :
        (a : MvPolynomial ι R) →
          MvPolynomial ι R ⧸ Ideal.span (Set.range (Subtype.val ∘ D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent))))
      0 =
    x
have subst : Eq (α :=
  HasQuotient.Quotient (MvPolynomial ι R) (B := Ideal (MvPolynomial ι R))
    (Ideal.span
      (Set.range (ι := σ)
        (Subtype.val (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) ∘
          D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent)))))
  ((Ideal.Quotient.mk
        (Ideal.span
          (Set.range (ι := σ)
            (Subtype.val (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) ∘
              D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent)))) :
      (a : MvPolynomial ι R) →
        MvPolynomial ι R ⧸ Ideal.span (Set.range (Subtype.val ∘ D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent))))
    0)
  0
Tactic: subst h
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basis (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ_1 : Type u_3
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
x :
  HasQuotient.Quotient (MvPolynomial ι R) (B := Ideal (MvPolynomial ι R))
    (Ideal.span
      (Set.range (ι := σ)
        (Subtype.val (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) ∘
          D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent))))
h_1 : ¬x = 0
h : x = -1
⊢ (Ideal.Quotient.mk
          (Ideal.span
            (Set.range (ι := σ)
              (Subtype.val (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) ∘
                D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent)))) :
        (a : MvPolynomial ι R) →
          MvPolynomial ι R ⧸ Ideal.span (Set.range (Subtype.val ∘ D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent))))
      (-1) =
    x
have subst : ¬Eq (α :=
      HasQuotient.Quotient (MvPolynomial ι R) (B := Ideal (MvPolynomial ι R))
        (Ideal.span
          (Set.range (ι := σ)
            (Subtype.val (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) ∘
              D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent)))))
      (-1) 0 →
  Eq (α :=
    HasQuotient.Quotient (MvPolynomial ι R) (B := Ideal (MvPolynomial ι R))
      (Ideal.span
        (Set.range (ι := σ)
          (Subtype.val (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) ∘
            D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent)))))
    ((Ideal.Quotient.mk
          (Ideal.span
            (Set.range (ι := σ)
              (Subtype.val (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) ∘
                D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent)))) :
        (a : MvPolynomial ι R) →
          MvPolynomial ι R ⧸ Ideal.span (Set.range (Subtype.val ∘ D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent))))
      (-1))
    (-1)
Tactic: subst h
Cleared hypotheses: x, h_1, h
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basis (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
⊢ D.fhom.toAlgHom = AlgHom.id R P.Ring
have hf : ∀ (i : ι),
  Eq (α := P.Ring) ((D.fhom.toAlgHom : (a : MvPolynomial ι R) → P.Ring) (X i) : P.Ring)
    ((AlgHom.id R P.Ring : (a : MvPolynomial ι R) → P.Ring) (X i) : P.Ring)
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basis (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
⊢ Eq (α := Submodule D.T D.presLeft.toExtension.Cotangent)
    (Submodule.span D.T
      (Set.range fun (i : σ) ↦
        (Extension.Cotangent.mk : (a : ↥D.presLeft.toExtension.ker) → D.presLeft.toExtension.Cotangent) (D.kerGen i)))
    ⊤
have refine : Ideal.span (Set.range fun (i : σ) ↦ (↑(D.f ((b : (a : σ) → P.toExtension.Cotangent) i)) : P.toExtension.Ring)) =
  D.presLeft.toExtension.ker
Tactic: refine Extension.Cotangent.span_eq_top_of_span_eq_ker _ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basis (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ_1 : Type u_3
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
⊢ S ⊗[D.T] D.presLeft.toExtension.Cotangent ≃ₗ[S] P.toExtension.Cotangent
have refine_1 : D.tensorCotangentHom ∘ₗ D.tensorCotangentInv = LinearMap.id
Tactic: refine LinearEquiv.ofLinear D.tensorCotangentHom D.tensorCotangentInv ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basis (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ_1 : Type u_3
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
refine_1 : D.tensorCotangentHom ∘ₗ D.tensorCotangentInv = LinearMap.id
⊢ S ⊗[D.T] D.presLeft.toExtension.Cotangent ≃ₗ[S] P.toExtension.Cotangent
have refine_2 : D.tensorCotangentInv ∘ₗ D.tensorCotangentHom = LinearMap.id
Tactic: refine LinearEquiv.ofLinear D.tensorCotangentHom D.tensorCotangentInv ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basis (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ_1 : Type u_3
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
⊢ D.tensorCotangentHom ∘ₗ D.tensorCotangentInv = LinearMap.id
have refine_1 : ∀ (i : σ),
  Eq (α := P.toExtension.Cotangent)
    ((D.tensorCotangentHom ∘ₗ D.tensorCotangentInv : (a : P.toExtension.Cotangent) → P.toExtension.Cotangent)
        ((b : (a : σ) → P.toExtension.Cotangent) i) :
      P.toExtension.Cotangent)
    ((LinearMap.id : (a : P.toExtension.Cotangent) → P.toExtension.Cotangent)
        ((b : (a : σ) → P.toExtension.Cotangent) i) :
      P.toExtension.Cotangent)
Tactic: refine b.ext fun i ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basis (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ_1 : Type u_3
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
⊢ D.tensorCotangentInv ∘ₗ D.tensorCotangentHom = LinearMap.id
have refine_2 : Eq (α :=
  LinearMap (R := D.T) (RingHom.id D.T) D.presLeft.toExtension.Cotangent (S ⊗[D.T] D.presLeft.toExtension.Cotangent))
  (((AlgebraTensorModule.curry (D.tensorCotangentInv ∘ₗ D.tensorCotangentHom) :
        S →ₗ[S]
          LinearMap (R := D.T) (RingHom.id D.T) D.presLeft.toExtension.Cotangent
            (S ⊗[D.T] D.presLeft.toExtension.Cotangent)) :
      (a : S) → D.presLeft.toExtension.Cotangent →ₗ[D.T] S ⊗[D.T] D.presLeft.toExtension.Cotangent)
    1)
  (((AlgebraTensorModule.curry LinearMap.id :
        S →ₗ[S]
          LinearMap (R := D.T) (RingHom.id D.T) D.presLeft.toExtension.Cotangent
            (S ⊗[D.T] D.presLeft.toExtension.Cotangent)) :
      (a : S) → D.presLeft.toExtension.Cotangent →ₗ[D.T] S ⊗[D.T] D.presLeft.toExtension.Cotangent)
    1)
Tactic: ext : 2
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basis (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ_1 : Type u_3
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
⊢ Eq (α :=
    LinearMap (R := D.T) (RingHom.id D.T) D.presLeft.toExtension.Cotangent (S ⊗[D.T] D.presLeft.toExtension.Cotangent))
    (((AlgebraTensorModule.curry (D.tensorCotangentInv ∘ₗ D.tensorCotangentHom) :
          S →ₗ[S]
            LinearMap (R := D.T) (RingHom.id D.T) D.presLeft.toExtension.Cotangent
              (S ⊗[D.T] D.presLeft.toExtension.Cotangent)) :
        (a : S) → D.presLeft.toExtension.Cotangent →ₗ[D.T] S ⊗[D.T] D.presLeft.toExtension.Cotangent)
      1)
    (((AlgebraTensorModule.curry LinearMap.id :
          S →ₗ[S]
            LinearMap (R := D.T) (RingHom.id D.T) D.presLeft.toExtension.Cotangent
              (S ⊗[D.T] D.presLeft.toExtension.Cotangent)) :
        (a : S) → D.presLeft.toExtension.Cotangent →ₗ[D.T] S ⊗[D.T] D.presLeft.toExtension.Cotangent)
      1)
have refine_2 : ∀ (i : σ),
  Eq (α := S ⊗[D.T] D.presLeft.toExtension.Cotangent)
    ((((AlgebraTensorModule.curry (D.tensorCotangentInv ∘ₗ D.tensorCotangentHom) :
                S →ₗ[S]
                  LinearMap (R := D.T) (RingHom.id D.T) D.presLeft.toExtension.Cotangent
                    (S ⊗[D.T] D.presLeft.toExtension.Cotangent)) :
              (a : S) → D.presLeft.toExtension.Cotangent →ₗ[D.T] S ⊗[D.T] D.presLeft.toExtension.Cotangent)
            1 :
          (a : D.presLeft.toExtension.Cotangent) → S ⊗[D.T] D.presLeft.toExtension.Cotangent)
        ((Extension.Cotangent.mk : (a : ↥D.presLeft.toExtension.ker) → D.presLeft.toExtension.Cotangent) (D.kerGen i)) :
      S ⊗[D.T] D.presLeft.toExtension.Cotangent)
    ((((AlgebraTensorModule.curry LinearMap.id :
                S →ₗ[S]
                  LinearMap (R := D.T) (RingHom.id D.T) D.presLeft.toExtension.Cotangent
                    (S ⊗[D.T] D.presLeft.toExtension.Cotangent)) :
              (a : S) → D.presLeft.toExtension.Cotangent →ₗ[D.T] S ⊗[D.T] D.presLeft.toExtension.Cotangent)
            1 :
          (a : D.presLeft.toExtension.Cotangent) → S ⊗[D.T] D.presLeft.toExtension.Cotangent)
        ((Extension.Cotangent.mk : (a : ↥D.presLeft.toExtension.ker) → D.presLeft.toExtension.Cotangent) (D.kerGen i)) :
      S ⊗[D.T] D.presLeft.toExtension.Cotangent)
Tactic: refine LinearMap.ext_on_range D.span_range_mk_kerGen fun i ↦ ?_