awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
S_1 : Type v
S' : Type w
inst : CommRing R
inst_1 : CommSemiring S_1
inst_2 : Algebra S_1 R
inst_3 : CommSemiring S'
inst_4 : Algebra S' R
inst_5 : Algebra S_1 S'
inst_6 : IsScalarTower S_1 S' R
I_1 : Ideal R
A : Type u_1
B : Type u_2
inst_7 : CommRing A
inst_8 : CommRing B
inst_9 : Algebra R A
inst_10 : Algebra R B
S : Type u_3
inst_11 : CommRing S
inst_12 : Algebra R S
I : Ideal S
M : Type u_4
inst_13 : AddCommGroup M
inst_14 : Module R M
f : LinearMap.{u, u, u_3, u_4} (RingHom.id R) (↥I) M
hf : ∀ (x y : ↥I), Eq.{u_4 + 1} (α := M) ((f : (a : ↥I) → M) (x * y) : M) (0 : M)
x : ↥I
hx : x ∈ HSMul.hSMul (β := Submodule S ↥I) I ⊤
refine :
  ∀ (x y : ↥I) (hx : Eq.{u_4 + 1} (α := M) ((f.toAddMonoidHom : (a : ↥I) → M) x : M) (0 : M))
    (hy : Eq.{u_4 + 1} (α := M) ((f.toAddMonoidHom : (a : ↥I) → M) y : M) (0 : M)),
    Eq.{u_4 + 1} (α := M) ((f.toAddMonoidHom : (a : ↥I) → M) (x + y) : M) (0 : M)
⊢ Eq.{u_4 + 1} (α := M) ((f.toAddMonoidHom : (a : ↥I) → M) x : M) (0 : M)

Tactic:
refine Submodule.smul_induction_on hx (fun r hr y _ ↦ hf ⟨r, hr⟩ y) fun x y hx hy ↦ ?_
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
S_1 : Type v
S' : Type w
inst : CommRing R
inst_1 : CommSemiring S_1
inst_2 : Algebra S_1 R
inst_3 : CommSemiring S'
inst_4 : Algebra S' R
inst_5 : Algebra S_1 S'
inst_6 : IsScalarTower S_1 S' R
I_1 : Ideal R
A : Type u_1
B : Type u_2
inst_7 : CommRing A
inst_8 : CommRing B
inst_9 : Algebra R A
inst_10 : Algebra R B
S : Type u_3
inst_11 : CommRing S
inst_12 : Algebra R S
I : Ideal S
M : Type u_4
inst_13 : AddCommGroup M
inst_14 : Module R M
f : LinearMap.{u, u, u_3, u_4} (RingHom.id R) (↥I) M
hf : ∀ (x y : ↥I), Eq.{u_4 + 1} (α := M) ((f : (a : ↥I) → M) (x * y) : M) (0 : M)
x_1 : ↥I
hx_1 : x_1 ∈ HSMul.hSMul (β := Submodule S ↥I) I ⊤
x y : ↥I
hx : Eq.{u_4 + 1} (α := M) ((f.toAddMonoidHom : (a : ↥I) → M) x : M) (0 : M)
hy : Eq.{u_4 + 1} (α := M) ((f.toAddMonoidHom : (a : ↥I) → M) y : M) (0 : M)
⊢ Eq.{u_4 + 1} (α := M) ((f.toAddMonoidHom : (a : ↥I) → M) (x + y) : M) (0 : M)

Tactic:
simp only [map_add, hx, hy, add_zero]

Premises used: map_add, add_zero
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
S_1 : Type v
S' : Type w
inst : CommRing R
inst_1 : CommSemiring S_1
inst_2 : Algebra S_1 R
inst_3 : CommSemiring S'
inst_4 : Algebra S' R
inst_5 : Algebra S_1 S'
inst_6 : IsScalarTower S_1 S' R
I_1 : Ideal R
A : Type u_1
B : Type u_2
inst_7 : CommRing A
inst_8 : CommRing B
inst_9 : Algebra R A
inst_10 : Algebra R B
S : Type u_3
inst_11 : CommRing S
inst_12 : Algebra R S
I : Ideal S
M : Type u_4
inst_13 : AddCommGroup M
inst_14 : Module R M
f : LinearMap.{u, u, u_3, u_4} (RingHom.id R) (↥I) M
hf : ∀ (x y : ↥I), Eq.{u_4 + 1} (α := M) ((f : (a : ↥I) → M) (x * y) : M) (0 : M)
r : R
x : I.Cotangent
obtain :
  ∀ (x : ↥I),
    ZeroHom.toFun
        (↑(QuotientAddGroup.lift (HSMul.hSMul (β := Submodule S ↥I) I ⊤).toAddSubgroup f.toAddMonoidHom ⋯) :
          ZeroHom (↥I ⧸ (I • ⊤).toAddSubgroup) M)
        (HSMul.hSMul (β := I.Cotangent) r ((I.toCotangent : (a : ↥I) → I.Cotangent) x : I.Cotangent)) =
      HSMul.hSMul (α := R) (β := M) ((RingHom.id R : (a : R) → R) r : R)
        (ZeroHom.toFun.{u_3, u_4} (M :=
          HasQuotient.Quotient ↥I (B := AddSubgroup ↥I) (HSMul.hSMul (β := Submodule S ↥I) I ⊤).toAddSubgroup)
          (↑(QuotientAddGroup.lift (HSMul.hSMul (β := Submodule S ↥I) I ⊤).toAddSubgroup f.toAddMonoidHom ⋯) :
            ZeroHom (↥I ⧸ (I • ⊤).toAddSubgroup) M)
          ((I.toCotangent : (a : ↥I) → I.Cotangent) x))
⊢ ZeroHom.toFun
      (↑(QuotientAddGroup.lift (HSMul.hSMul (β := Submodule S ↥I) I ⊤).toAddSubgroup f.toAddMonoidHom ⋯) :
        ZeroHom (↥I ⧸ (I • ⊤).toAddSubgroup) M)
      (r • x) =
    HSMul.hSMul (α := R) (β := M) ((RingHom.id R : (a : R) → R) r : R)
      (ZeroHom.toFun
        (↑(QuotientAddGroup.lift (HSMul.hSMul (β := Submodule S ↥I) I ⊤).toAddSubgroup f.toAddMonoidHom ⋯) :
          ZeroHom (↥I ⧸ (I • ⊤).toAddSubgroup) M)
        x)

Tactic:
obtain ⟨x, rfl⟩ := I.toCotangent_surjective x

Premises used: Ideal.toCotangent_surjective, rfl
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
S_1 : Type v
S' : Type w
inst : CommRing R
inst_1 : CommSemiring S_1
inst_2 : Algebra S_1 R
inst_3 : CommSemiring S'
inst_4 : Algebra S' R
inst_5 : Algebra S_1 S'
inst_6 : IsScalarTower S_1 S' R
I_1 : Ideal R
A : Type u_1
B : Type u_2
inst_7 : CommRing A
inst_8 : CommRing B
inst_9 : Algebra R A
inst_10 : Algebra R B
S : Type u_3
inst_11 : CommRing S
inst_12 : Algebra R S
I : Ideal S
M : Type u_4
inst_13 : AddCommGroup M
inst_14 : Module R M
f : LinearMap.{u, u, u_3, u_4} (RingHom.id R) (↥I) M
hf : ∀ (x y : ↥I), Eq.{u_4 + 1} (α := M) ((f : (a : ↥I) → M) (x * y) : M) (0 : M)
r : R
x : ↥I
⊢ ZeroHom.toFun
      (↑(QuotientAddGroup.lift (HSMul.hSMul (β := Submodule S ↥I) I ⊤).toAddSubgroup f.toAddMonoidHom ⋯) :
        ZeroHom (↥I ⧸ (I • ⊤).toAddSubgroup) M)
      (HSMul.hSMul (β := I.Cotangent) r ((I.toCotangent : (a : ↥I) → I.Cotangent) x : I.Cotangent)) =
    HSMul.hSMul (α := R) (β := M) ((RingHom.id R : (a : R) → R) r : R)
      (ZeroHom.toFun.{u_3, u_4} (M :=
        HasQuotient.Quotient ↥I (B := AddSubgroup ↥I) (HSMul.hSMul (β := Submodule S ↥I) I ⊤).toAddSubgroup)
        (↑(QuotientAddGroup.lift (HSMul.hSMul (β := Submodule S ↥I) I ⊤).toAddSubgroup f.toAddMonoidHom ⋯) :
          ZeroHom (↥I ⧸ (I • ⊤).toAddSubgroup) M)
        ((I.toCotangent : (a : ↥I) → I.Cotangent) x))

Tactic:
map_smul f _ _

Premises used: Quotient.liftOn', AddCon.liftOn, map_smul
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
S_1 : Type v
S' : Type w
inst : CommRing R
inst_1 : CommSemiring S_1
inst_2 : Algebra S_1 R
inst_3 : CommSemiring S'
inst_4 : Algebra S' R
inst_5 : Algebra S_1 S'
inst_6 : IsScalarTower S_1 S' R
I_1 : Ideal R
A : Type u_1
B : Type u_2
inst_7 : CommRing A
inst_8 : CommRing B
inst_9 : Algebra R A
inst_10 : Algebra R B
S : Type u_3
inst_11 : CommRing S
inst_12 : Algebra R S
I : Ideal S
M : Type u_4
inst_13 : AddCommGroup M
inst_14 : Module R M
f : LinearMap.{u, u, u_3, u_4} (RingHom.id R) (↥I) M
hf : ∀ (x y : ↥I), Eq.{u_4 + 1} (α := M) ((f : (a : ↥I) → M) (x * y) : M) (0 : M)
r : R
x : ↥I
⊢ ZeroHom.toFun
      (↑(QuotientAddGroup.lift (HSMul.hSMul (β := Submodule S ↥I) I ⊤).toAddSubgroup f.toAddMonoidHom ⋯) :
        ZeroHom (↥I ⧸ (I • ⊤).toAddSubgroup) M)
      (HSMul.hSMul (β := I.Cotangent) r ((I.toCotangent : (a : ↥I) → I.Cotangent) x : I.Cotangent)) =
    HSMul.hSMul (α := R) (β := M) ((RingHom.id R : (a : R) → R) r : R)
      (ZeroHom.toFun.{u_3, u_4} (M :=
        HasQuotient.Quotient ↥I (B := AddSubgroup ↥I) (HSMul.hSMul (β := Submodule S ↥I) I ⊤).toAddSubgroup)
        (↑(QuotientAddGroup.lift (HSMul.hSMul (β := Submodule S ↥I) I ⊤).toAddSubgroup f.toAddMonoidHom ⋯) :
          ZeroHom (↥I ⧸ (I • ⊤).toAddSubgroup) M)
        ((I.toCotangent : (a : ↥I) → I.Cotangent) x))

Tactic:
exact map_smul f _ _

Premises used: map_smul
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
inst : CommRing R
S : Type u_3
inst_1 : CommRing S
inst_2 : Algebra R S
I : Ideal S
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
f : LinearMap.{u, u, u_3, u_4} (RingHom.id R) (↥I) M
hf : ∀ (x y : ↥I), Eq.{u_4 + 1} (α := M) ((f : (a : ↥I) → M) (x * y) : M) (0 : M)
x : ↥I
⊢ Eq.{u_4 + 1} (α := M)
    ((lift f hf : (a : I.Cotangent) → M) ((I.toCotangent : (a : ↥I) → I.Cotangent) x : I.Cotangent) : M)
    ((f : (a : ↥I) → M) x : M)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, rfl
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
inst : CommRing R
S : Type u_3
inst_1 : CommRing S
inst_2 : Algebra R S
I : Ideal S
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
f : LinearMap.{u, u, u_3, u_4} (RingHom.id R) (↥I) M
hf : ∀ (x y : ↥I), Eq.{u_4 + 1} (α := M) ((f : (a : ↥I) → M) (x * y) : M) (0 : M)
⊢ lift f hf ∘ₗ
      (↑R :
          {S M M₂ : Type u_3} →
            [inst : Semiring R] →
              [inst_5 : Semiring S] →
                [inst_6 : AddCommMonoid M] →
                  [inst_7 : AddCommMonoid M₂] →
                    [inst_8 : Module R M] →
                      [inst_9 : Module R M₂] →
                        [inst_10 : Module S M] →
                          [inst_11 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        I.toCotangent =
    f

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, rfl
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
inst : CommRing R
S : Type u_3
inst_1 : CommRing S
inst_2 : Algebra R S
I : Ideal S
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
f : LinearMap.{u, u, u_3, u_4} (RingHom.id R) (↥I) M
hf : ∀ (x y : ↥I), Eq.{u_4 + 1} (α := M) ((f : (a : ↥I) → M) (x * y) : M) (0 : M)
⊢ Function.Surjective.{u_3 + 1, u_4 + 1} (α := I.Cotangent) (β := M) (⇑(lift f hf) : (a : I.Cotangent) → M) ↔
    Function.Surjective.{u_3 + 1, u_4 + 1} (α := ↥I) (β := M) (⇑f : (a : ↥I) → M)

Tactic:
⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
inst : CommRing R
S : Type u_3
inst_1 : CommRing S
inst_2 : Algebra R S
I : Ideal S
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
f : LinearMap.{u, u, u_3, u_4} (RingHom.id R) (↥I) M
hf : ∀ (x y : ↥I), Eq.{u_4 + 1} (α := M) ((f : (a : ↥I) → M) (x * y) : M) (0 : M)
refine_1 :
  ∀ (h : Function.Surjective.{u_3 + 1, u_4 + 1} (α := I.Cotangent) (β := M) (⇑(lift f hf) : (a : I.Cotangent) → M)),
    Function.Surjective.{u_3 + 1, u_4 + 1} (α := ↥I) (β := M) (⇑f : (a : ↥I) → M)
refine_2 :
  ∀ (h : Function.Surjective.{u_3 + 1, u_4 + 1} (α := ↥I) (β := M) (⇑f : (a : ↥I) → M)),
    Function.Surjective.{u_3 + 1, u_4 + 1} (α := I.Cotangent) (β := M) (⇑(lift f hf) : (a : I.Cotangent) → M)
⊢ Function.Surjective.{u_3 + 1, u_4 + 1} (α := I.Cotangent) (β := M) (⇑(lift f hf) : (a : I.Cotangent) → M) ↔
    Function.Surjective.{u_3 + 1, u_4 + 1} (α := ↥I) (β := M) (⇑f : (a : ↥I) → M)

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
inst : CommRing R
S : Type u_3
inst_1 : CommRing S
inst_2 : Algebra R S
I : Ideal S
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
f : LinearMap.{u, u, u_3, u_4} (RingHom.id R) (↥I) M
hf : ∀ (x y : ↥I), Eq.{u_4 + 1} (α := M) ((f : (a : ↥I) → M) (x * y) : M) (0 : M)
h : Function.Surjective.{u_3 + 1, u_4 + 1} (α := I.Cotangent) (β := M) (⇑(lift f hf) : (a : I.Cotangent) → M)
refine_1 :
  Function.Surjective.{u_3 + 1, u_4 + 1} (α := ↥I) (β := M)
    (Function.comp (β := I.Cotangent) (⇑(lift f hf) : (a : I.Cotangent) → M)
      (⇑((↑R :
              {S M M₂ : Type u_3} →
                [inst : Semiring R] →
                  [inst_5 : Semiring S] →
                    [inst_6 : AddCommMonoid M] →
                      [inst_7 : AddCommMonoid M₂] →
                        [inst_8 : Module R M] →
                          [inst_9 : Module R M₂] →
                            [inst_10 : Module S M] →
                              [inst_11 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            I.toCotangent) :
        (a : ↥I) → I.Cotangent))
⊢ Function.Surjective.{u_3 + 1, u_4 + 1} (α := ↥I) (β := M) (⇑f : (a : ↥I) → M)

Tactic:
rw [← Cotangent.lift_comp_toCotangent f hf, LinearMap.coe_comp]

Premises used: Ideal.Cotangent.lift_comp_toCotangent, LinearMap.coe_comp
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
inst : CommRing R
S : Type u_3
inst_1 : CommRing S
inst_2 : Algebra R S
I : Ideal S
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
f : LinearMap.{u, u, u_3, u_4} (RingHom.id R) (↥I) M
hf : ∀ (x y : ↥I), Eq.{u_4 + 1} (α := M) ((f : (a : ↥I) → M) (x * y) : M) (0 : M)
h : Function.Surjective.{u_3 + 1, u_4 + 1} (α := I.Cotangent) (β := M) (⇑(lift f hf) : (a : I.Cotangent) → M)
⊢ Function.Surjective.{u_3 + 1, u_4 + 1} (α := ↥I) (β := M)
    (Function.comp (β := I.Cotangent) (⇑(lift f hf) : (a : I.Cotangent) → M)
      (⇑((↑R :
              {S M M₂ : Type u_3} →
                [inst : Semiring R] →
                  [inst_5 : Semiring S] →
                    [inst_6 : AddCommMonoid M] →
                      [inst_7 : AddCommMonoid M₂] →
                        [inst_8 : Module R M] →
                          [inst_9 : Module R M₂] →
                            [inst_10 : Module S M] →
                              [inst_11 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            I.toCotangent) :
        (a : ↥I) → I.Cotangent))

Tactic:
Function.Surjective.comp h (toCotangent_surjective I)

Premises used: Function.Surjective.comp, Ideal.toCotangent_surjective
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
inst : CommRing R
S : Type u_3
inst_1 : CommRing S
inst_2 : Algebra R S
I : Ideal S
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
f : LinearMap.{u, u, u_3, u_4} (RingHom.id R) (↥I) M
hf : ∀ (x y : ↥I), Eq.{u_4 + 1} (α := M) ((f : (a : ↥I) → M) (x * y) : M) (0 : M)
h : Function.Surjective.{u_3 + 1, u_4 + 1} (α := I.Cotangent) (β := M) (⇑(lift f hf) : (a : I.Cotangent) → M)
⊢ Function.Surjective.{u_3 + 1, u_4 + 1} (α := ↥I) (β := M)
    (Function.comp (β := I.Cotangent) (⇑(lift f hf) : (a : I.Cotangent) → M)
      (⇑((↑R :
              {S M M₂ : Type u_3} →
                [inst : Semiring R] →
                  [inst_5 : Semiring S] →
                    [inst_6 : AddCommMonoid M] →
                      [inst_7 : AddCommMonoid M₂] →
                        [inst_8 : Module R M] →
                          [inst_9 : Module R M₂] →
                            [inst_10 : Module S M] →
                              [inst_11 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            I.toCotangent) :
        (a : ↥I) → I.Cotangent))

Tactic:
exact Function.Surjective.comp h (toCotangent_surjective I)

Premises used: Function.Surjective.comp, Ideal.toCotangent_surjective
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
inst : CommRing R
S : Type u_3
inst_1 : CommRing S
inst_2 : Algebra R S
I : Ideal S
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
f : LinearMap.{u, u, u_3, u_4} (RingHom.id R) (↥I) M
hf : ∀ (x y : ↥I), Eq.{u_4 + 1} (α := M) ((f : (a : ↥I) → M) (x * y) : M) (0 : M)
h : Function.Surjective.{u_3 + 1, u_4 + 1} (α := ↥I) (β := M) (⇑f : (a : ↥I) → M)
refine_2 :
  Function.Surjective.{u_3 + 1, u_4 + 1} (α := I.Cotangent) (β := M)
    (⇑(QuotientAddGroup.lift (HSMul.hSMul (β := Submodule S ↥I) I ⊤).toAddSubgroup f.toAddMonoidHom ⋯) :
      (a : ↥I ⧸ (I • ⊤).toAddSubgroup) → M)
⊢ Function.Surjective.{u_3 + 1, u_4 + 1} (α := I.Cotangent) (β := M) (⇑(lift f hf) : (a : I.Cotangent) → M)

Tactic:
dsimp [Cotangent.lift]

Premises used: Ideal.Cotangent.lift
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
inst : CommRing R
S : Type u_3
inst_1 : CommRing S
inst_2 : Algebra R S
I : Ideal S
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
f : LinearMap.{u, u, u_3, u_4} (RingHom.id R) (↥I) M
hf : ∀ (x y : ↥I), Eq.{u_4 + 1} (α := M) ((f : (a : ↥I) → M) (x * y) : M) (0 : M)
h : Function.Surjective.{u_3 + 1, u_4 + 1} (α := ↥I) (β := M) (⇑f : (a : ↥I) → M)
⊢ Function.Surjective.{u_3 + 1, u_4 + 1} (α := I.Cotangent) (β := M)
    (⇑(QuotientAddGroup.lift (HSMul.hSMul (β := Submodule S ↥I) I ⊤).toAddSubgroup f.toAddMonoidHom ⋯) :
      (a : ↥I ⧸ (I • ⊤).toAddSubgroup) → M)

Tactic:
QuotientAddGroup.lift_surjective_of_surjective _ _ h _

Premises used: Ideal.Cotangent, QuotientAddGroup.lift_surjective_of_surjective, Submodule.quotientRel
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
inst : CommRing R
S : Type u_3
inst_1 : CommRing S
inst_2 : Algebra R S
I : Ideal S
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
f : LinearMap.{u, u, u_3, u_4} (RingHom.id R) (↥I) M
hf : ∀ (x y : ↥I), Eq.{u_4 + 1} (α := M) ((f : (a : ↥I) → M) (x * y) : M) (0 : M)
h : Function.Surjective.{u_3 + 1, u_4 + 1} (α := ↥I) (β := M) (⇑f : (a : ↥I) → M)
⊢ Function.Surjective.{u_3 + 1, u_4 + 1} (α := I.Cotangent) (β := M)
    (⇑(QuotientAddGroup.lift (HSMul.hSMul (β := Submodule S ↥I) I ⊤).toAddSubgroup f.toAddMonoidHom ⋯) :
      (a : ↥I ⧸ (I • ⊤).toAddSubgroup) → M)

Tactic:
exact QuotientAddGroup.lift_surjective_of_surjective _ _ h _

Premises used: QuotientAddGroup.lift_surjective_of_surjective
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
S : Type v
S' : Type w
inst : CommRing R
inst_1 : CommSemiring S
inst_2 : Algebra S R
inst_3 : CommSemiring S'
inst_4 : Algebra S' R
inst_5 : Algebra S S'
inst_6 : IsScalarTower S S' R
I_1 : Ideal R
A : Type u_1
B : Type u_2
inst_7 : CommRing A
inst_8 : CommRing B
inst_9 : Algebra R A
inst_10 : Algebra R B
I J : Ideal R
hIJ : I = J
x y : ↥I
⊢ Eq (α := J.Cotangent)
    ((J.toCotangent ∘ₗ (↑(LinearEquiv.ofEq I J hIJ) : ↥I →ₗ[R] ↥J) : (a : ↥I) → J.Cotangent) (x * y) : J.Cotangent)
    (0 : J.Cotangent)

Tactic:
simp [toCotangent_eq_zero, ← hIJ, sq, mul_mem_mul]

Premises used: sq, Ideal.mul_mem_mul, Ideal.toCotangent_eq_zero
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
S : Type v
S' : Type w
inst : CommRing R
inst_1 : CommSemiring S
inst_2 : Algebra S R
inst_3 : CommSemiring S'
inst_4 : Algebra S' R
inst_5 : Algebra S S'
inst_6 : IsScalarTower S S' R
I_1 : Ideal R
A : Type u_1
B : Type u_2
inst_7 : CommRing A
inst_8 : CommRing B
inst_9 : Algebra R A
inst_10 : Algebra R B
I J : Ideal R
hIJ : I = J
x y : ↥J
⊢ Eq (α := I.Cotangent)
    ((I.toCotangent ∘ₗ (↑(LinearEquiv.ofEq J I ⋯) : ↥J →ₗ[R] ↥I) : (a : ↥J) → I.Cotangent) (x * y) : I.Cotangent)
    (0 : I.Cotangent)

Tactic:
simp [toCotangent_eq_zero, hIJ, sq, mul_mem_mul]

Premises used: sq, Ideal.mul_mem_mul, Ideal.toCotangent_eq_zero
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
S : Type v
S' : Type w
inst : CommRing R
inst_1 : CommSemiring S
inst_2 : Algebra S R
inst_3 : CommSemiring S'
inst_4 : Algebra S' R
inst_5 : Algebra S S'
inst_6 : IsScalarTower S S' R
I_1 : Ideal R
A : Type u_1
B : Type u_2
inst_7 : CommRing A
inst_8 : CommRing B
inst_9 : Algebra R A
inst_10 : Algebra R B
I J : Ideal R
hIJ : I = J
x : I.Cotangent
subst :
  (lift (I.toCotangent ∘ₗ (↑(LinearEquiv.ofEq I I ⋯) : ↥I →ₗ[R] ↥I)) ⋯ : (a : I.Cotangent) → I.Cotangent)
      ((lift (I.toCotangent ∘ₗ (↑(LinearEquiv.ofEq I I ⋯) : ↥I →ₗ[R] ↥I)) ⋯).toFun x) =
    x
⊢ (lift (I.toCotangent ∘ₗ (↑(LinearEquiv.ofEq J I ⋯) : ↥J →ₗ[R] ↥I)) ⋯ : (a : J.Cotangent) → I.Cotangent)
      ((lift (J.toCotangent ∘ₗ (↑(LinearEquiv.ofEq I J hIJ) : ↥I →ₗ[R] ↥J)) ⋯).toFun x) =
    x

Tactic:
subst hIJ
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
S : Type v
S' : Type w
inst : CommRing R
inst_1 : CommSemiring S
inst_2 : Algebra S R
inst_3 : CommSemiring S'
inst_4 : Algebra S' R
inst_5 : Algebra S S'
inst_6 : IsScalarTower S S' R
I_1 : Ideal R
A : Type u_1
B : Type u_2
inst_7 : CommRing A
inst_8 : CommRing B
inst_9 : Algebra R A
inst_10 : Algebra R B
I : Ideal R
x : I.Cotangent
__spread.0 : I.Cotangent →ₗ[R] I.Cotangent := lift (I.toCotangent ∘ₗ (↑(LinearEquiv.ofEq I I ⋯) : ↥I →ₗ[R] ↥I)) ⋯
obtain :
  ∀ (x : ↥I),
    Eq (α := I.Cotangent)
      ((lift (I.toCotangent ∘ₗ (↑(LinearEquiv.ofEq I I ⋯) : ↥I →ₗ[R] ↥I)) ⋯ : (a : I.Cotangent) → I.Cotangent)
          ((lift (I.toCotangent ∘ₗ (↑(LinearEquiv.ofEq I I ⋯) : ↥I →ₗ[R] ↥I)) ⋯).toFun
            ((I.toCotangent : (a : ↥I) → I.Cotangent) x)) :
        I.Cotangent)
      ((I.toCotangent : (a : ↥I) → I.Cotangent) x : I.Cotangent)
⊢ (lift (I.toCotangent ∘ₗ (↑(LinearEquiv.ofEq I I ⋯) : ↥I →ₗ[R] ↥I)) ⋯ : (a : I.Cotangent) → I.Cotangent)
      ((lift (I.toCotangent ∘ₗ (↑(LinearEquiv.ofEq I I ⋯) : ↥I →ₗ[R] ↥I)) ⋯).toFun x) =
    x

Tactic:
obtain ⟨x, rfl⟩ := I.toCotangent_surjective x

Premises used: Ideal.toCotangent_surjective, rfl
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
S : Type v
S' : Type w
inst : CommRing R
inst_1 : CommSemiring S
inst_2 : Algebra S R
inst_3 : CommSemiring S'
inst_4 : Algebra S' R
inst_5 : Algebra S S'
inst_6 : IsScalarTower S S' R
I_1 : Ideal R
A : Type u_1
B : Type u_2
inst_7 : CommRing A
inst_8 : CommRing B
inst_9 : Algebra R A
inst_10 : Algebra R B
I : Ideal R
__spread.0 : I.Cotangent →ₗ[R] I.Cotangent := lift (I.toCotangent ∘ₗ (↑(LinearEquiv.ofEq I I ⋯) : ↥I →ₗ[R] ↥I)) ⋯
x : ↥I
⊢ Eq (α := I.Cotangent)
    ((lift (I.toCotangent ∘ₗ (↑(LinearEquiv.ofEq I I ⋯) : ↥I →ₗ[R] ↥I)) ⋯ : (a : I.Cotangent) → I.Cotangent)
        ((lift (I.toCotangent ∘ₗ (↑(LinearEquiv.ofEq I I ⋯) : ↥I →ₗ[R] ↥I)) ⋯).toFun
          ((I.toCotangent : (a : ↥I) → I.Cotangent) x)) :
      I.Cotangent)
    ((I.toCotangent : (a : ↥I) → I.Cotangent) x : I.Cotangent)

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
S : Type v
S' : Type w
inst : CommRing R
inst_1 : CommSemiring S
inst_2 : Algebra S R
inst_3 : CommSemiring S'
inst_4 : Algebra S' R
inst_5 : Algebra S S'
inst_6 : IsScalarTower S S' R
I_1 : Ideal R
A : Type u_1
B : Type u_2
inst_7 : CommRing A
inst_8 : CommRing B
inst_9 : Algebra R A
inst_10 : Algebra R B
I J : Ideal R
hIJ : I = J
x : J.Cotangent
subst :
  ∀ (x : I.Cotangent),
    (lift (I.toCotangent ∘ₗ (↑(LinearEquiv.ofEq I I ⋯) : ↥I →ₗ[R] ↥I)) ⋯).toFun
        ((lift (I.toCotangent ∘ₗ (↑(LinearEquiv.ofEq I I ⋯) : ↥I →ₗ[R] ↥I)) ⋯ : (a : I.Cotangent) → I.Cotangent) x) =
      x
⊢ (lift (J.toCotangent ∘ₗ (↑(LinearEquiv.ofEq I J hIJ) : ↥I →ₗ[R] ↥J)) ⋯).toFun
      ((lift (I.toCotangent ∘ₗ (↑(LinearEquiv.ofEq J I ⋯) : ↥J →ₗ[R] ↥I)) ⋯ : (a : J.Cotangent) → I.Cotangent) x) =
    x

Tactic:
subst hIJ
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
S : Type v
S' : Type w
inst : CommRing R
inst_1 : CommSemiring S
inst_2 : Algebra S R
inst_3 : CommSemiring S'
inst_4 : Algebra S' R
inst_5 : Algebra S S'
inst_6 : IsScalarTower S S' R
I_1 : Ideal R
A : Type u_1
B : Type u_2
inst_7 : CommRing A
inst_8 : CommRing B
inst_9 : Algebra R A
inst_10 : Algebra R B
I : Ideal R
__spread.0 : I.Cotangent →ₗ[R] I.Cotangent := lift (I.toCotangent ∘ₗ (↑(LinearEquiv.ofEq I I ⋯) : ↥I →ₗ[R] ↥I)) ⋯
x : I.Cotangent
obtain :
  ∀ (x : ↥I),
    (lift (I.toCotangent ∘ₗ (↑(LinearEquiv.ofEq I I ⋯) : ↥I →ₗ[R] ↥I)) ⋯).toFun
        ((lift (I.toCotangent ∘ₗ (↑(LinearEquiv.ofEq I I ⋯) : ↥I →ₗ[R] ↥I)) ⋯ : (a : I.Cotangent) → I.Cotangent)
          ((I.toCotangent : (a : ↥I) → I.Cotangent) x)) =
      (I.toCotangent : (a : ↥I) → I.Cotangent) x
⊢ (lift (I.toCotangent ∘ₗ (↑(LinearEquiv.ofEq I I ⋯) : ↥I →ₗ[R] ↥I)) ⋯).toFun
      ((lift (I.toCotangent ∘ₗ (↑(LinearEquiv.ofEq I I ⋯) : ↥I →ₗ[R] ↥I)) ⋯ : (a : I.Cotangent) → I.Cotangent) x) =
    x

Tactic:
obtain ⟨x, rfl⟩ := I.toCotangent_surjective x

Premises used: Ideal.toCotangent_surjective, rfl
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
S : Type v
S' : Type w
inst : CommRing R
inst_1 : CommSemiring S
inst_2 : Algebra S R
inst_3 : CommSemiring S'
inst_4 : Algebra S' R
inst_5 : Algebra S S'
inst_6 : IsScalarTower S S' R
I_1 : Ideal R
A : Type u_1
B : Type u_2
inst_7 : CommRing A
inst_8 : CommRing B
inst_9 : Algebra R A
inst_10 : Algebra R B
I : Ideal R
__spread.0 : I.Cotangent →ₗ[R] I.Cotangent := lift (I.toCotangent ∘ₗ (↑(LinearEquiv.ofEq I I ⋯) : ↥I →ₗ[R] ↥I)) ⋯
x : ↥I
⊢ (lift (I.toCotangent ∘ₗ (↑(LinearEquiv.ofEq I I ⋯) : ↥I →ₗ[R] ↥I)) ⋯).toFun
      ((lift (I.toCotangent ∘ₗ (↑(LinearEquiv.ofEq I I ⋯) : ↥I →ₗ[R] ↥I)) ⋯ : (a : I.Cotangent) → I.Cotangent)
        ((I.toCotangent : (a : ↥I) → I.Cotangent) x)) =
    (I.toCotangent : (a : ↥I) → I.Cotangent) x

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
inst : CommRing R
I J : Ideal R
hIJ : I = J
x : ↥I
⊢ Eq (α := J.Cotangent)
    ((equivOfEq I J hIJ : (a : I.Cotangent) → J.Cotangent) ((I.toCotangent : (a : ↥I) → I.Cotangent) x) : J.Cotangent)
    ((J.toCotangent : (a : ↥J) → J.Cotangent) ((LinearEquiv.ofEq I J hIJ : (a : ↥I) → ↥J) x) : J.Cotangent)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, rfl