awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
inst : CommRing R
A : Type u_1
B : Type u_2
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A →ₐ[R] B
a : RingHom.ker f.kerSquareLift.toRingHom ≤ cotangentIdeal (RingHom.ker f.toRingHom)
a₁ : cotangentIdeal (RingHom.ker f.toRingHom) ≤ RingHom.ker f.kerSquareLift.toRingHom
⊢ RingHom.ker f.kerSquareLift.toRingHom = cotangentIdeal (RingHom.ker f.toRingHom)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
inst : CommRing R
A : Type u_1
B : Type u_2
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A →ₐ[R] B
x : A ⧸ HPow.hPow (α := Ideal A) (β := ℕ) (RingHom.ker f.toRingHom) 2
hx :
  Membership.mem (γ :=
    Submodule (A ⧸ HPow.hPow (α := Ideal A) (β := ℕ) (RingHom.ker f.toRingHom) 2)
      (A ⧸ HPow.hPow (α := Ideal A) (β := ℕ) (RingHom.ker f.toRingHom) 2))
    (RingHom.ker f.kerSquareLift.toRingHom) x
a :
  ∀ (x : A)
    (hx :
      Membership.mem (α := A ⧸ HPow.hPow (α := Ideal A) (β := ℕ) (RingHom.ker f.toRingHom) 2) (γ :=
        Submodule (A ⧸ HPow.hPow (α := Ideal A) (β := ℕ) (RingHom.ker f.toRingHom) 2)
          (A ⧸ HPow.hPow (α := Ideal A) (β := ℕ) (RingHom.ker f.toRingHom) 2))
        (RingHom.ker f.kerSquareLift.toRingHom)
        ((Quotient.mk (HPow.hPow (α := Ideal A) (β := ℕ) (RingHom.ker f.toRingHom) 2) :
              (a : A) → A ⧸ RingHom.ker f.toRingHom ^ 2)
            x :
          A ⧸ HPow.hPow (α := Ideal A) (β := ℕ) (RingHom.ker f.toRingHom) 2)),
    Membership.mem (α := A ⧸ HPow.hPow (α := Ideal A) (β := ℕ) (RingHom.ker f.toRingHom) 2) (γ :=
      Submodule (A ⧸ HPow.hPow (α := Ideal A) (β := ℕ) (RingHom.ker f.toRingHom) 2)
        (A ⧸ HPow.hPow (α := Ideal A) (β := ℕ) (RingHom.ker f.toRingHom) 2))
      (cotangentIdeal (RingHom.ker f.toRingHom))
      ((Quotient.mk (HPow.hPow (α := Ideal A) (β := ℕ) (RingHom.ker f.toRingHom) 2) :
            (a : A) → A ⧸ RingHom.ker f.toRingHom ^ 2)
          x :
        A ⧸ HPow.hPow (α := Ideal A) (β := ℕ) (RingHom.ker f.toRingHom) 2)
⊢ Membership.mem (γ :=
    Submodule (A ⧸ HPow.hPow (α := Ideal A) (β := ℕ) (RingHom.ker f.toRingHom) 2)
      (A ⧸ HPow.hPow (α := Ideal A) (β := ℕ) (RingHom.ker f.toRingHom) 2))
    (cotangentIdeal (RingHom.ker f.toRingHom)) x

Tactic:
obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x

Premises used: Ideal.Quotient.mk_surjective, rfl
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
inst : CommRing R
A : Type u_1
B : Type u_2
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A →ₐ[R] B
x : A
hx :
  Membership.mem (α := A ⧸ HPow.hPow (α := Ideal A) (β := ℕ) (RingHom.ker f.toRingHom) 2) (γ :=
    Submodule (A ⧸ HPow.hPow (α := Ideal A) (β := ℕ) (RingHom.ker f.toRingHom) 2)
      (A ⧸ HPow.hPow (α := Ideal A) (β := ℕ) (RingHom.ker f.toRingHom) 2))
    (RingHom.ker f.kerSquareLift.toRingHom)
    ((Quotient.mk (HPow.hPow (α := Ideal A) (β := ℕ) (RingHom.ker f.toRingHom) 2) :
          (a : A) → A ⧸ RingHom.ker f.toRingHom ^ 2)
        x :
      A ⧸ HPow.hPow (α := Ideal A) (β := ℕ) (RingHom.ker f.toRingHom) 2)
⊢ Membership.mem (α := A ⧸ HPow.hPow (α := Ideal A) (β := ℕ) (RingHom.ker f.toRingHom) 2) (γ :=
    Submodule (A ⧸ HPow.hPow (α := Ideal A) (β := ℕ) (RingHom.ker f.toRingHom) 2)
      (A ⧸ HPow.hPow (α := Ideal A) (β := ℕ) (RingHom.ker f.toRingHom) 2))
    (cotangentIdeal (RingHom.ker f.toRingHom))
    ((Quotient.mk (HPow.hPow (α := Ideal A) (β := ℕ) (RingHom.ker f.toRingHom) 2) :
          (a : A) → A ⧸ RingHom.ker f.toRingHom ^ 2)
        x :
      A ⧸ HPow.hPow (α := Ideal A) (β := ℕ) (RingHom.ker f.toRingHom) 2)

Tactic:
⟨x, hx, rfl⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, Set.image, rfl
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
inst : CommRing R
A : Type u_1
B : Type u_2
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A →ₐ[R] B
x : A
hx :
  Membership.mem (α := A ⧸ HPow.hPow (α := Ideal A) (β := ℕ) (RingHom.ker f.toRingHom) 2) (γ :=
    Submodule (A ⧸ HPow.hPow (α := Ideal A) (β := ℕ) (RingHom.ker f.toRingHom) 2)
      (A ⧸ HPow.hPow (α := Ideal A) (β := ℕ) (RingHom.ker f.toRingHom) 2))
    (RingHom.ker f.kerSquareLift.toRingHom)
    ((Quotient.mk (HPow.hPow (α := Ideal A) (β := ℕ) (RingHom.ker f.toRingHom) 2) :
          (a : A) → A ⧸ RingHom.ker f.toRingHom ^ 2)
        x :
      A ⧸ HPow.hPow (α := Ideal A) (β := ℕ) (RingHom.ker f.toRingHom) 2)
⊢ Membership.mem (α := A ⧸ HPow.hPow (α := Ideal A) (β := ℕ) (RingHom.ker f.toRingHom) 2) (γ :=
    Submodule (A ⧸ HPow.hPow (α := Ideal A) (β := ℕ) (RingHom.ker f.toRingHom) 2)
      (A ⧸ HPow.hPow (α := Ideal A) (β := ℕ) (RingHom.ker f.toRingHom) 2))
    (cotangentIdeal (RingHom.ker f.toRingHom))
    ((Quotient.mk (HPow.hPow (α := Ideal A) (β := ℕ) (RingHom.ker f.toRingHom) 2) :
          (a : A) → A ⧸ RingHom.ker f.toRingHom ^ 2)
        x :
      A ⧸ HPow.hPow (α := Ideal A) (β := ℕ) (RingHom.ker f.toRingHom) 2)

Tactic:
exact ⟨x, hx, rfl⟩
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
inst : CommRing R
A : Type u_1
B : Type u_2
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A →ₐ[R] B
x : A
hx : x ∈ (↑(RingHom.ker f.toRingHom) : Set A)
⊢ Membership.mem (α := A ⧸ HPow.hPow (α := Ideal A) (β := ℕ) (RingHom.ker f.toRingHom) 2) (γ :=
    Submodule (A ⧸ HPow.hPow (α := Ideal A) (β := ℕ) (RingHom.ker f.toRingHom) 2)
      (A ⧸ HPow.hPow (α := Ideal A) (β := ℕ) (RingHom.ker f.toRingHom) 2))
    (RingHom.ker f.kerSquareLift.toRingHom)
    ((RingHom.toSemilinearMap (Quotient.mk (HPow.hPow (α := Ideal A) (β := ℕ) (RingHom.ker f.toRingHom) 2)) :
          (a : A) → A ⧸ RingHom.ker f.toRingHom ^ 2)
        x :
      A ⧸ HPow.hPow (α := Ideal A) (β := ℕ) (RingHom.ker f.toRingHom) 2)

Tactic:
hx

Premises used: Quotient.liftOn', Set.Mem, AddCon.liftOn, setOf, Quotient, Set.preimage, AddCon.Quotient
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
inst : CommRing R
A : Type u_1
B : Type u_2
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A →ₐ[R] B
x : A
hx : x ∈ (↑(RingHom.ker f.toRingHom) : Set A)
⊢ Membership.mem (α := A ⧸ HPow.hPow (α := Ideal A) (β := ℕ) (RingHom.ker f.toRingHom) 2) (γ :=
    Submodule (A ⧸ HPow.hPow (α := Ideal A) (β := ℕ) (RingHom.ker f.toRingHom) 2)
      (A ⧸ HPow.hPow (α := Ideal A) (β := ℕ) (RingHom.ker f.toRingHom) 2))
    (RingHom.ker f.kerSquareLift.toRingHom)
    ((RingHom.toSemilinearMap (Quotient.mk (HPow.hPow (α := Ideal A) (β := ℕ) (RingHom.ker f.toRingHom) 2)) :
          (a : A) → A ⧸ RingHom.ker f.toRingHom ^ 2)
        x :
      A ⧸ HPow.hPow (α := Ideal A) (β := ℕ) (RingHom.ker f.toRingHom) 2)

Tactic:
exact hx
-- 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 : 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
inst_11 : Algebra A B
inst_12 : IsScalarTower R A B
⊢ IsScalarTower.{u, u_1, u_2} R (A ⧸ HPow.hPow (α := Ideal A) (β := ℕ) (RingHom.ker (F := A →+* B) (algebraMap A B)) 2)
    B

Tactic:
IsScalarTower.of_algebraMap_eq'
    (IsScalarTower.toAlgHom R A B).kerSquareLift.comp_algebraMap.symm

Premises used: AlgHom.comp_algebraMap, IsScalarTower.toAlgHom, IsScalarTower.of_algebraMap_eq', AlgHom.kerSquareLift, Eq.symm
-- 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 : 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
refine :
  HasQuotient.Quotient (R ⧸ HPow.hPow (β := ℕ) I 2) (B := Ideal (R ⧸ HPow.hPow (β := ℕ) I 2))
      (map (F := R →+* R ⧸ HPow.hPow (β := ℕ) I 2) (Quotient.mk (HPow.hPow (β := ℕ) I 2)) I) ≃+*
    R ⧸ I
⊢ (R ⧸ HPow.hPow (β := ℕ) I 2) ⧸ I.cotangentIdeal ≃+* R ⧸ I

Tactic:
refine (Ideal.quotEquivOfEq (Ideal.map_eq_submodule_map _ _).symm).trans ?_

Premises used: Ideal.quotEquivOfEq, Ideal.map_eq_submodule_map, RingEquiv.trans, Eq.symm
-- 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 : 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
refine : R ⧸ HPow.hPow (β := ℕ) I 2 ⊔ I ≃+* R ⧸ I
⊢ HasQuotient.Quotient (R ⧸ HPow.hPow (β := ℕ) I 2) (B := Ideal (R ⧸ HPow.hPow (β := ℕ) I 2))
      (map (F := R →+* R ⧸ HPow.hPow (β := ℕ) I 2) (Quotient.mk (HPow.hPow (β := ℕ) I 2)) I) ≃+*
    R ⧸ I

Tactic:
refine (DoubleQuot.quotQuotEquivQuotSup _ _).trans ?_

Premises used: RingEquiv.trans, DoubleQuot.quotQuotEquivQuotSup
-- 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 : 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
⊢ R ⧸ HPow.hPow (β := ℕ) I 2 ⊔ I ≃+* R ⧸ I

Tactic:
exact Ideal.quotEquivOfEq (sup_eq_right.mpr <| Ideal.pow_le_self two_ne_zero)

Premises used: Iff.mpr, Ideal.quotEquivOfEq, sup_eq_right
-- 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 : 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 A
I₂ : Ideal B
f : A →ₐ[R] B
h : I₁ ≤ comap f I₂
refine_1 : LinearMap.{u, u, u_1, u_2} (RingHom.id R) ↥I₁ ↥I₂
refine_2 :
  LE.le (α := Submodule R ↥I₁) (Submodule.restrictScalars R (HSMul.hSMul (β := Submodule A ↥I₁) I₁ ⊤))
    (Submodule.comap (σ₁₂ := RingHom.id R) (f.toLinearMap.restrict h)
      (Submodule.restrictScalars R (HSMul.hSMul (β := Submodule B ↥I₂) I₂ ⊤)))
⊢ LinearMap.{u, u, u_1, u_2} (RingHom.id R) I₁.Cotangent I₂.Cotangent

Tactic:
refine Submodule.mapQ ((I₁ • ⊤ : Submodule A I₁).restrictScalars R)
    ((I₂ • ⊤ : Submodule B I₂).restrictScalars R) ?_ ?_

Premises used: Submodule.restrictScalars, Submodule.mapQ, HSMul.hSMul, Top.top
-- 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 : 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 A
I₂ : Ideal B
f : A →ₐ[R] B
h : I₁ ≤ comap f I₂
⊢ LinearMap.{u, u, u_1, u_2} (RingHom.id R) ↥I₁ ↥I₂

Tactic:
exact f.toLinearMap.restrict (p := I₁.restrictScalars R) (q := I₂.restrictScalars R) h

Premises used: AlgHom.toLinearMap, LinearMap.restrict
-- 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 : 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 A
I₂ : Ideal B
f : A →ₐ[R] B
h : I₁ ≤ comap f I₂
x : ↥I₁
hx : Membership.mem (γ := Submodule R ↥I₁) (Submodule.restrictScalars R (HSMul.hSMul (β := Submodule A ↥I₁) I₁ ⊤)) x
⊢ x ∈ HSMul.hSMul (β := Submodule A ↥I₁) I₁ ⊤

Tactic:
rw [Submodule.restrictScalars_mem] at hx

Premises used: Submodule.restrictScalars_mem
-- 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 : 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 A
I₂ : Ideal B
f : A →ₐ[R] B
h : I₁ ≤ comap f I₂
x : ↥I₁
hx : x ∈ HSMul.hSMul (β := Submodule A ↥I₁) I₁ ⊤
⊢ Membership.mem (γ := Submodule R ↥I₁)
    (Submodule.comap (σ₁₂ := RingHom.id R) (f.toLinearMap.restrict h)
        (Submodule.restrictScalars R (HSMul.hSMul (β := Submodule B ↥I₂) I₂ ⊤)) :
      Submodule R ↥I₁)
    x

Tactic:
Submodule.smul_induction_on hx ?_ (fun _ _ ↦ add_mem)

Premises used: Submodule.smul_induction_on
-- 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 : 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 A
I₂ : Ideal B
f : A →ₐ[R] B
h : I₁ ≤ comap f I₂
x : ↥I₁
hx : x ∈ HSMul.hSMul (β := Submodule A ↥I₁) I₁ ⊤
refine_2 :
  ∀ r ∈ I₁,
    ∀ (n : ↥I₁),
      Membership.mem (γ := Submodule A ↥I₁) ⊤ n →
        Membership.mem (γ := Submodule R ↥I₁)
          (Submodule.comap (σ₁₂ := RingHom.id R) (f.toLinearMap.restrict h)
              (Submodule.restrictScalars R (HSMul.hSMul (β := Submodule B ↥I₂) I₂ ⊤)) :
            Submodule R ↥I₁)
          (r • n)
⊢ Membership.mem (γ := Submodule R ↥I₁)
    (Submodule.comap (σ₁₂ := RingHom.id R) (f.toLinearMap.restrict h)
        (Submodule.restrictScalars R (HSMul.hSMul (β := Submodule B ↥I₂) I₂ ⊤)) :
      Submodule R ↥I₁)
    x

Tactic:
refine Submodule.smul_induction_on hx ?_ (fun _ _ ↦ add_mem)
-- 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 : 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 A
I₂ : Ideal B
f : A →ₐ[R] B
h : I₁ ≤ comap f I₂
x : ↥I₁
hx : x ∈ HSMul.hSMul (β := Submodule A ↥I₁) I₁ ⊤
a : A
ha : a ∈ I₁
b : A
hb : b ∈ I₁
refine_2 :
  Membership.mem (α := ↥I₂) (HSMul.hSMul (β := Submodule B ↥I₂) I₂ ⊤)
    (((f.toLinearMap.restrict h :
            LinearMap.{u, u, u_1, u_2} (RingHom.id R) ↥(Submodule.restrictScalars R I₁)
              ↥(Submodule.restrictScalars R I₂)) :
          (a : ↥I₁) → ↥I₂)
        (Subtype.mk (p := fun (x : A) ↦ x ∈ I₁) (a * b) ⋯) :
      ↥I₂)
⊢ Membership.mem (γ := Submodule R ↥I₁)
    (Submodule.comap (σ₁₂ := RingHom.id R) (f.toLinearMap.restrict h)
        (Submodule.restrictScalars R (HSMul.hSMul (β := Submodule B ↥I₂) I₂ ⊤)) :
      Submodule R ↥I₁)
    (a • Subtype.mk (p := fun (x : A) ↦ x ∈ I₁) b hb)

Tactic:
simp only [SetLike.mk_smul_mk, smul_eq_mul, Submodule.mem_comap, Submodule.restrictScalars_mem]

Premises used: Submodule.mem_comap, Submodule.restrictScalars_mem, smul_eq_mul, SetLike.mk_smul_mk
-- 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 : 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 A
I₂ : Ideal B
f : A →ₐ[R] B
h : I₁ ≤ comap f I₂
x : ↥I₁
hx : x ∈ HSMul.hSMul (β := Submodule A ↥I₁) I₁ ⊤
a : A
ha : a ∈ I₁
b : A
hb : b ∈ I₁
⊢ HSMul.hSMul (α := B) (β := ↥I₂) ((f : (a : A) → B) a : B)
      (Subtype.mk (p := fun (x : B) ↦ x ∈ I₂) ((f : (a : A) → B) b) ⋯ : ↥I₂) ∈
    HSMul.hSMul (β := Submodule B ↥I₂) I₂ ⊤

Tactic:
(Submodule.smul_mem_smul (M := I₂) (r := f a) (n := ⟨f b, h hb⟩) (h ha)
        (Submodule.mem_top))

Premises used: Submodule.smul_mem_smul, Submodule.mem_top
-- 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 : 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 A
I₂ : Ideal B
f : A →ₐ[R] B
h : I₁ ≤ comap f I₂
x : ↥I₁
hx : x ∈ HSMul.hSMul (β := Submodule A ↥I₁) I₁ ⊤
a : A
ha : a ∈ I₁
b : A
hb : b ∈ I₁
h₁ :
  ((f.toLinearMap.restrict h :
          LinearMap.{u, u, u_1, u_2} (RingHom.id R) ↥(Submodule.restrictScalars R I₁)
            ↥(Submodule.restrictScalars R I₂)) :
        (a : ↥I₁) → ↥I₂)
      (Subtype.mk (p := fun (x : A) ↦ x ∈ I₁) (a * b) ⋯) =
    HSMul.hSMul (α := B) (β := ↥I₂) ((f : (a : A) → B) a : B)
      (Subtype.mk (p := fun (x : B) ↦ x ∈ I₂) ((f : (a : A) → B) b) ⋯ : ↥I₂)
⊢ Membership.mem (α := ↥I₂) (HSMul.hSMul (β := Submodule B ↥I₂) I₂ ⊤)
    (((f.toLinearMap.restrict h :
            LinearMap.{u, u, u_1, u_2} (RingHom.id R) ↥(Submodule.restrictScalars R I₁)
              ↥(Submodule.restrictScalars R I₂)) :
          (a : ↥I₁) → ↥I₂)
        (Subtype.mk (p := fun (x : A) ↦ x ∈ I₁) (a * b) ⋯) :
      ↥I₂)

Tactic:
convert!
      (Submodule.smul_mem_smul (M := I₂) (r := f a) (n := ⟨f b, h hb⟩) (h ha)
        (Submodule.mem_top)) using 1

Premises used: Submodule.smul_mem_smul, Submodule.mem_top
-- 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 : 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 A
I₂ : Ideal B
f : A →ₐ[R] B
h : I₁ ≤ comap f I₂
x : ↥I₁
hx : x ∈ HSMul.hSMul (β := Submodule A ↥I₁) I₁ ⊤
a : A
ha : a ∈ I₁
b : A
hb : b ∈ I₁
h₁ :
  (↑(((f.toLinearMap.restrict h :
              LinearMap.{u, u, u_1, u_2} (RingHom.id R) ↥(Submodule.restrictScalars R I₁)
                ↥(Submodule.restrictScalars R I₂)) :
            (a : ↥I₁) → ↥I₂)
          (Subtype.mk (p := fun (x : A) ↦ x ∈ I₁) (a * b) ⋯)) :
      B) =
    (↑(HSMul.hSMul (α := B) (β := ↥I₂) ((f : (a : A) → B) a : B)
          (Subtype.mk (p := fun (x : B) ↦ x ∈ I₂) ((f : (a : A) → B) b) ⋯ : ↥I₂)) :
      B)
⊢ ((f.toLinearMap.restrict h :
          LinearMap.{u, u, u_1, u_2} (RingHom.id R) ↥(Submodule.restrictScalars R I₁)
            ↥(Submodule.restrictScalars R I₂)) :
        (a : ↥I₁) → ↥I₂)
      (Subtype.mk (p := fun (x : A) ↦ x ∈ I₁) (a * b) ⋯) =
    HSMul.hSMul (α := B) (β := ↥I₂) ((f : (a : A) → B) a : B)
      (Subtype.mk (p := fun (x : B) ↦ x ∈ I₂) ((f : (a : A) → B) b) ⋯ : ↥I₂)

Tactic:
ext
-- 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 : 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 A
I₂ : Ideal B
f : A →ₐ[R] B
h : I₁ ≤ comap f I₂
x : ↥I₁
hx : x ∈ HSMul.hSMul (β := Submodule A ↥I₁) I₁ ⊤
a : A
ha : a ∈ I₁
b : A
hb : b ∈ I₁
⊢ (↑(((f.toLinearMap.restrict h :
              LinearMap.{u, u, u_1, u_2} (RingHom.id R) ↥(Submodule.restrictScalars R I₁)
                ↥(Submodule.restrictScalars R I₂)) :
            (a : ↥I₁) → ↥I₂)
          (Subtype.mk (p := fun (x : A) ↦ x ∈ I₁) (a * b) ⋯)) :
      B) =
    (↑(HSMul.hSMul (α := B) (β := ↥I₂) ((f : (a : A) → B) a : B)
          (Subtype.mk (p := fun (x : B) ↦ x ∈ I₂) ((f : (a : A) → B) b) ⋯ : ↥I₂)) :
      B)

Tactic:
map_mul f a b

Premises used: map_mul
-- 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 : 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 A
I₂ : Ideal B
f : A →ₐ[R] B
h : I₁ ≤ comap f I₂
x : ↥I₁
hx : x ∈ HSMul.hSMul (β := Submodule A ↥I₁) I₁ ⊤
a : A
ha : a ∈ I₁
b : A
hb : b ∈ I₁
⊢ (↑(((f.toLinearMap.restrict h :
              LinearMap.{u, u, u_1, u_2} (RingHom.id R) ↥(Submodule.restrictScalars R I₁)
                ↥(Submodule.restrictScalars R I₂)) :
            (a : ↥I₁) → ↥I₂)
          (Subtype.mk (p := fun (x : A) ↦ x ∈ I₁) (a * b) ⋯)) :
      B) =
    (↑(HSMul.hSMul (α := B) (β := ↥I₂) ((f : (a : A) → B) a : B)
          (Subtype.mk (p := fun (x : B) ↦ x ∈ I₂) ((f : (a : A) → B) b) ⋯ : ↥I₂)) :
      B)

Tactic:
exact map_mul f a b

Premises used: map_mul
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
inst : CommRing R
A : Type u_1
B : Type u_2
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
I₁ : Ideal A
I₂ : Ideal B
f : A →ₐ[R] B
h : I₁ ≤ comap f I₂
x : ↥I₁
⊢ Eq.{u_2 + 1} (α := I₂.Cotangent)
    ((I₁.mapCotangent I₂ f h : (a : I₁.Cotangent) → I₂.Cotangent) ((I₁.toCotangent : (a : ↥I₁) → I₁.Cotangent) x) :
      I₂.Cotangent)
    ((I₂.toCotangent : (a : ↥I₂) → I₂.Cotangent)
        (Subtype.mk (p := fun (x : B) ↦ x ∈ I₂) ((f : (a : A) → B) (↑x : A)) ⋯) :
      I₂.Cotangent)

Tactic:
rfl

Premises used: iInf, Quotient.liftOn', Set.Mem, iSup, AddCon.liftOn, Set.iInter, Submodule.Quotient.mk, Submodule.restrictScalars, setOf, 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)
x : ↥I
hx : Membership.mem (γ := AddSubgroup ↥I) (HSMul.hSMul (β := Submodule S ↥I) I ⊤).toAddSubgroup x
simp :
  ∀ (hx : x ∈ HSMul.hSMul (β := Submodule S ↥I) I ⊤),
    Eq.{u_4 + 1} (α := M) ((f.toAddMonoidHom : (a : ↥I) → M) x : M) (0 : M)
⊢ Membership.mem (γ := AddSubgroup ↥I) f.toAddMonoidHom.ker x

Tactic:
simp only [Submodule.mem_toAddSubgroup, AddMonoidHom.mem_ker] at hx ⊢

Premises used: Submodule.mem_toAddSubgroup, AddMonoidHom.mem_ker
-- 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 ⊤
⊢ Eq.{u_4 + 1} (α := M) ((f.toAddMonoidHom : (a : ↥I) → M) x : M) (0 : M)

Tactic:
Submodule.smul_induction_on hx (fun r hr y _ ↦ hf ⟨r, hr⟩ y) fun x y hx hy ↦ ?_

Premises used: Submodule.smul_induction_on