awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module S M₂
f : M →+ M₂
as : List R
bs : List S
hf : Surjective.{u_3 + 1, u_4 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
h :
  AddSubgroup.map f (HSMul.hSMul.{u_1, u_3, u_3} (α := Ideal R) (β := Submodule R M) ⊥ ⊤).toAddSubgroup =
    AddSubgroup.map f ⊥
⊢ AddSubgroup.map f
      (HSMul.hSMul.{u_1, u_3, u_3} (α := Ideal R) (β := Submodule R M) (Ideal.ofList []) ⊤).toAddSubgroup =
    AddSubgroup.map f ⊥
have h₁ : AddSubgroup.map f (toAddSubgroup.{u_1, u_3} (R := R) (module_M := inst_4) ⊥) = AddSubgroup.map f ⊥
Tactic: rw [Ideal.ofList_nil, bot_smul, bot_toAddSubgroup]
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module S M₂
f : M →+ M₂
as : List R
bs : List S
hf : Surjective.{u_3 + 1, u_4 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
h :
  AddSubgroup.map f (HSMul.hSMul.{u_1, u_3, u_3} (α := Ideal R) (β := Submodule R M) ⊥ ⊤).toAddSubgroup =
    AddSubgroup.map f ⊥
h₁ : AddSubgroup.map f (toAddSubgroup.{u_1, u_3} (R := R) (module_M := inst_4) ⊥) = AddSubgroup.map f ⊥
⊢ AddSubgroup.map f
      (HSMul.hSMul.{u_1, u_3, u_3} (α := Ideal R) (β := Submodule R M) (Ideal.ofList []) ⊤).toAddSubgroup =
    AddSubgroup.map f ⊥
have h₂ : AddSubgroup.map f ⊥ = AddSubgroup.map f ⊥
Tactic: rw [Ideal.ofList_nil, bot_smul, bot_toAddSubgroup]
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module S M₂
f : M →+ M₂
as : List R
bs : List S
hf : Surjective.{u_3 + 1, u_4 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
⊢ (HSMul.hSMul.{u_2, u_4, u_4} (α := Ideal S) (β := Submodule S M₂) (Ideal.ofList []) ⊤).toAddSubgroup = ⊥
have h : (HSMul.hSMul.{u_2, u_4, u_4} (α := Ideal S) (β := Submodule S M₂) ⊥ ⊤).toAddSubgroup = ⊥
Tactic: rw [Ideal.ofList_nil, bot_smul, bot_toAddSubgroup]
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module S M₂
f : M →+ M₂
as : List R
bs : List S
hf : Surjective.{u_3 + 1, u_4 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
h : (HSMul.hSMul.{u_2, u_4, u_4} (α := Ideal S) (β := Submodule S M₂) ⊥ ⊤).toAddSubgroup = ⊥
⊢ (HSMul.hSMul.{u_2, u_4, u_4} (α := Ideal S) (β := Submodule S M₂) (Ideal.ofList []) ⊤).toAddSubgroup = ⊥
have h₁ : Eq.{u_4 + 1} (α := AddSubgroup M₂) (toAddSubgroup.{u_2, u_4} (R := S) (module_M := inst_5) ⊥) ⊥
Tactic: rw [Ideal.ofList_nil, bot_smul, bot_toAddSubgroup]
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module S M₂
f : M →+ M₂
as : List R
bs : List S
hf : Surjective.{u_3 + 1, u_4 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
h : (HSMul.hSMul.{u_2, u_4, u_4} (α := Ideal S) (β := Submodule S M₂) ⊥ ⊤).toAddSubgroup = ⊥
h₁ : Eq.{u_4 + 1} (α := AddSubgroup M₂) (toAddSubgroup.{u_2, u_4} (R := S) (module_M := inst_5) ⊥) ⊥
⊢ (HSMul.hSMul.{u_2, u_4, u_4} (α := Ideal S) (β := Submodule S M₂) (Ideal.ofList []) ⊤).toAddSubgroup = ⊥
have h₂ : Eq.{u_4 + 1} (α := AddSubgroup M₂) ⊥ ⊥
Tactic: rw [Ideal.ofList_nil, bot_smul, bot_toAddSubgroup]
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module S M₂
f : M →+ M₂
as : List R
bs : List S
hf : Surjective.{u_3 + 1, u_4 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
r : R
s : S
l₁ : List R
l₂ : List S
h : ∀ (x : M), (f : (a : M) → M₂) (r • x) = HSMul.hSMul (β := M₂) s ((f : (a : M) → M₂) x : M₂)
h_1 :
  List.Forall₂
    (fun (r : R) (s : S) ↦ ∀ (x : M), (f : (a : M) → M₂) (r • x) = HSMul.hSMul (β := M₂) s ((f : (a : M) → M₂) x : M₂))
    l₁ l₂
ih :
  AddSubgroup.map f (HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList l₁) ⊤).toAddSubgroup =
    (HSMul.hSMul (α := Ideal S) (β := Submodule S M₂) (Ideal.ofList l₂) ⊤).toAddSubgroup
| AddSubgroup.map f (HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: l₁)) ⊤).toAddSubgroup =
    (HSMul.hSMul (α := Ideal S) (β := Submodule S M₂) (Ideal.ofList (s :: l₂)) ⊤).toAddSubgroup
have a : AddSubgroup.map f (HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: l₁)) ⊤).toAddSubgroup
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module S M₂
f : M →+ M₂
as : List R
bs : List S
hf : Surjective.{u_3 + 1, u_4 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
r : R
s : S
l₁ : List R
l₂ : List S
h : ∀ (x : M), (f : (a : M) → M₂) (r • x) = HSMul.hSMul (β := M₂) s ((f : (a : M) → M₂) x : M₂)
h_1 :
  List.Forall₂
    (fun (r : R) (s : S) ↦ ∀ (x : M), (f : (a : M) → M₂) (r • x) = HSMul.hSMul (β := M₂) s ((f : (a : M) → M₂) x : M₂))
    l₁ l₂
ih :
  AddSubgroup.map f (HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList l₁) ⊤).toAddSubgroup =
    (HSMul.hSMul (α := Ideal S) (β := Submodule S M₂) (Ideal.ofList l₂) ⊤).toAddSubgroup
a : AddSubgroup.map f (HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: l₁)) ⊤).toAddSubgroup
| AddSubgroup.map f (HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: l₁)) ⊤).toAddSubgroup =
    (HSMul.hSMul (α := Ideal S) (β := Submodule S M₂) (Ideal.ofList (s :: l₂)) ⊤).toAddSubgroup
have a₁ : (HSMul.hSMul (α := Ideal S) (β := Submodule S M₂) (Ideal.ofList (s :: l₂)) ⊤).toAddSubgroup
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module S M₂
f : M →+ M₂
as : List R
bs : List S
hf : Surjective.{u_3 + 1, u_4 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
r : R
s : S
l₁ : List R
l₂ : List S
h : ∀ (x : M), (f : (a : M) → M₂) (r • x) = HSMul.hSMul (β := M₂) s ((f : (a : M) → M₂) x : M₂)
h_1 :
  List.Forall₂
    (fun (r : R) (s : S) ↦ ∀ (x : M), (f : (a : M) → M₂) (r • x) = HSMul.hSMul (β := M₂) s ((f : (a : M) → M₂) x : M₂))
    l₁ l₂
ih :
  AddSubgroup.map f (HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList l₁) ⊤).toAddSubgroup =
    (HSMul.hSMul (α := Ideal S) (β := Submodule S M₂) (Ideal.ofList l₂) ⊤).toAddSubgroup
| AddSubgroup.map f (HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: l₁)) ⊤).toAddSubgroup
have a : AddSubgroup.map f
  (AddSubgroup.map (G := M)
      (((toAddMonoidEnd R M : MonoidHom.{u_1, u_3} R (AddMonoid.End M)) : (a : R) → AddMonoid.End M) r) ⊤ ⊔
    (HSMul.hSMul (α := Submodule R R) (β := Submodule R M) (Ideal.ofList l₁) ⊤).toAddSubgroup)
Tactic: rw [Ideal.ofList_cons, sup_smul, sup_toAddSubgroup,
      ideal_span_singleton_smul, pointwise_smul_toAddSubgroup,
      top_toAddSubgroup, AddSubgroup.pointwise_smul_def]
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module S M₂
f : M →+ M₂
as : List R
bs : List S
hf : Surjective.{u_3 + 1, u_4 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
r : R
s : S
l₁ : List R
l₂ : List S
h : ∀ (x : M), (f : (a : M) → M₂) (r • x) = HSMul.hSMul (β := M₂) s ((f : (a : M) → M₂) x : M₂)
h_1 :
  List.Forall₂
    (fun (r : R) (s : S) ↦ ∀ (x : M), (f : (a : M) → M₂) (r • x) = HSMul.hSMul (β := M₂) s ((f : (a : M) → M₂) x : M₂))
    l₁ l₂
ih :
  AddSubgroup.map f (HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList l₁) ⊤).toAddSubgroup =
    (HSMul.hSMul (α := Ideal S) (β := Submodule S M₂) (Ideal.ofList l₂) ⊤).toAddSubgroup
| (HSMul.hSMul (α := Ideal S) (β := Submodule S M₂) (Ideal.ofList (s :: l₂)) ⊤).toAddSubgroup
have a : AddSubgroup.map (G := M₂)
    (((toAddMonoidEnd S M₂ : MonoidHom.{u_2, u_4} S (AddMonoid.End M₂)) : (a : S) → AddMonoid.End M₂) s) ⊤ ⊔
  (HSMul.hSMul (α := Submodule S S) (β := Submodule S M₂) (Ideal.ofList l₂) ⊤).toAddSubgroup
Tactic: rw [Ideal.ofList_cons, sup_smul, sup_toAddSubgroup,
      ideal_span_singleton_smul, pointwise_smul_toAddSubgroup,
      top_toAddSubgroup, AddSubgroup.pointwise_smul_def]
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module S M₂
f : M →+ M₂
as : List R
bs : List S
hf : Surjective.{u_3 + 1, u_4 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
r : R
s : S
l₁ : List R
l₂ : List S
h : ∀ (x : M), (f : (a : M) → M₂) (r • x) = HSMul.hSMul (β := M₂) s ((f : (a : M) → M₂) x : M₂)
h_1 :
  List.Forall₂
    (fun (r : R) (s : S) ↦ ∀ (x : M), (f : (a : M) → M₂) (r • x) = HSMul.hSMul (β := M₂) s ((f : (a : M) → M₂) x : M₂))
    l₁ l₂
ih :
  AddSubgroup.map f (HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList l₁) ⊤).toAddSubgroup =
    (HSMul.hSMul (α := Ideal S) (β := Submodule S M₂) (Ideal.ofList l₂) ⊤).toAddSubgroup
| AddSubgroup.map f (HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: l₁)) ⊤).toAddSubgroup =
    (HSMul.hSMul (α := Ideal S) (β := Submodule S M₂) (Ideal.ofList (s :: l₂)) ⊤).toAddSubgroup
have a : AddSubgroup.map f
  (AddSubgroup.map (G := M)
      (((toAddMonoidEnd R M : MonoidHom.{u_1, u_3} R (AddMonoid.End M)) : (a : R) → AddMonoid.End M) r) ⊤ ⊔
    (HSMul.hSMul (α := Submodule R R) (β := Submodule R M) (Ideal.ofList l₁) ⊤).toAddSubgroup)
Tactic: congr <;> rw [Ideal.ofList_cons, sup_smul, sup_toAddSubgroup,
      ideal_span_singleton_smul, pointwise_smul_toAddSubgroup,
      top_toAddSubgroup, AddSubgroup.pointwise_smul_def]
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module S M₂
f : M →+ M₂
as : List R
bs : List S
hf : Surjective.{u_3 + 1, u_4 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
r : R
s : S
l₁ : List R
l₂ : List S
h : ∀ (x : M), (f : (a : M) → M₂) (r • x) = HSMul.hSMul (β := M₂) s ((f : (a : M) → M₂) x : M₂)
h_1 :
  List.Forall₂
    (fun (r : R) (s : S) ↦ ∀ (x : M), (f : (a : M) → M₂) (r • x) = HSMul.hSMul (β := M₂) s ((f : (a : M) → M₂) x : M₂))
    l₁ l₂
ih :
  AddSubgroup.map f (HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList l₁) ⊤).toAddSubgroup =
    (HSMul.hSMul (α := Ideal S) (β := Submodule S M₂) (Ideal.ofList l₂) ⊤).toAddSubgroup
a :
  AddSubgroup.map f
    (AddSubgroup.map (G := M)
        (((toAddMonoidEnd R M : MonoidHom.{u_1, u_3} R (AddMonoid.End M)) : (a : R) → AddMonoid.End M) r) ⊤ ⊔
      (HSMul.hSMul (α := Submodule R R) (β := Submodule R M) (Ideal.ofList l₁) ⊤).toAddSubgroup)
| AddSubgroup.map f (HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: l₁)) ⊤).toAddSubgroup =
    (HSMul.hSMul (α := Ideal S) (β := Submodule S M₂) (Ideal.ofList (s :: l₂)) ⊤).toAddSubgroup
have a₁ : AddSubgroup.map (G := M₂)
    (((toAddMonoidEnd S M₂ : MonoidHom.{u_2, u_4} S (AddMonoid.End M₂)) : (a : S) → AddMonoid.End M₂) s) ⊤ ⊔
  (HSMul.hSMul (α := Submodule S S) (β := Submodule S M₂) (Ideal.ofList l₂) ⊤).toAddSubgroup
Tactic: congr <;> rw [Ideal.ofList_cons, sup_smul, sup_toAddSubgroup,
      ideal_span_singleton_smul, pointwise_smul_toAddSubgroup,
      top_toAddSubgroup, AddSubgroup.pointwise_smul_def]
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module S M₂
f : M →+ M₂
as : List R
bs : List S
hf : Surjective.{u_3 + 1, u_4 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
r : R
s : S
l₁ : List R
l₂ : List S
h : ∀ (x : M), (f : (a : M) → M₂) (r • x) = HSMul.hSMul (β := M₂) s ((f : (a : M) → M₂) x : M₂)
h_1 :
  List.Forall₂
    (fun (r : R) (s : S) ↦ ∀ (x : M), (f : (a : M) → M₂) (r • x) = HSMul.hSMul (β := M₂) s ((f : (a : M) → M₂) x : M₂))
    l₁ l₂
ih :
  AddSubgroup.map f (HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList l₁) ⊤).toAddSubgroup =
    (HSMul.hSMul (α := Ideal S) (β := Submodule S M₂) (Ideal.ofList l₂) ⊤).toAddSubgroup
⊢ AddSubgroup.map f (HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: l₁)) ⊤).toAddSubgroup =
    (HSMul.hSMul (α := Ideal S) (β := Submodule S M₂) (Ideal.ofList (s :: l₂)) ⊤).toAddSubgroup
have cons : AddSubgroup.map f
    (AddSubgroup.map (G := M)
        (((toAddMonoidEnd R M : MonoidHom.{u_1, u_3} R (AddMonoid.End M)) : (a : R) → AddMonoid.End M) r) ⊤ ⊔
      (HSMul.hSMul (α := Submodule R R) (β := Submodule R M) (Ideal.ofList l₁) ⊤).toAddSubgroup) =
  AddSubgroup.map (G := M₂)
      (((toAddMonoidEnd S M₂ : MonoidHom.{u_2, u_4} S (AddMonoid.End M₂)) : (a : S) → AddMonoid.End M₂) s) ⊤ ⊔
    (HSMul.hSMul (α := Submodule S S) (β := Submodule S M₂) (Ideal.ofList l₂) ⊤).toAddSubgroup
Tactic: conv => congr <;> rw [Ideal.ofList_cons, sup_smul, sup_toAddSubgroup,
      ideal_span_singleton_smul, pointwise_smul_toAddSubgroup,
      top_toAddSubgroup, AddSubgroup.pointwise_smul_def]
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (hypothesis)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module S M₂
f : M →+ M₂
as : List R
bs : List S
hf : Surjective.{u_3 + 1, u_4 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
r : R
s : S
l₁ : List R
l₂ : List S
h : ∀ (x : M), (f : (a : M) → M₂) (r • x) = HSMul.hSMul (β := M₂) s ((f : (a : M) → M₂) x : M₂)
h_1 :
  List.Forall₂
    (fun (r : R) (s : S) ↦ ∀ (x : M), (f : (a : M) → M₂) (r • x) = HSMul.hSMul (β := M₂) s ((f : (a : M) → M₂) x : M₂))
    l₁ l₂
ih :
  AddSubgroup.map f (HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList l₁) ⊤).toAddSubgroup =
    (HSMul.hSMul (α := Ideal S) (β := Submodule S M₂) (Ideal.ofList l₂) ⊤).toAddSubgroup
⊢ AddSubgroup.map f
      (AddSubgroup.map (G := M)
          (((toAddMonoidEnd R M : MonoidHom.{u_1, u_3} R (AddMonoid.End M)) : (a : R) → AddMonoid.End M) r) ⊤ ⊔
        (HSMul.hSMul (α := Submodule R R) (β := Submodule R M) (Ideal.ofList l₁) ⊤).toAddSubgroup) =
    AddSubgroup.map (G := M₂)
        (((toAddMonoidEnd S M₂ : MonoidHom.{u_2, u_4} S (AddMonoid.End M₂)) : (a : S) → AddMonoid.End M₂) s) ⊤ ⊔
      (HSMul.hSMul (α := Submodule S S) (β := Submodule S M₂) (Ideal.ofList l₂) ⊤).toAddSubgroup
have h₁ : f.comp (((toAddMonoidEnd R M : MonoidHom.{u_1, u_3} R (AddMonoid.End M)) : (a : R) → AddMonoid.End M) r) =
  AddMonoidHom.comp (((toAddMonoidEnd S M₂ : MonoidHom.{u_2, u_4} S (AddMonoid.End M₂)) : (a : S) → AddMonoid.End M₂) s)
    f
Tactic: apply DFunLike.ext (f.comp (toAddMonoidEnd R M r))
      ((toAddMonoidEnd S M₂ s).comp f) at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module S M₂
f : M →+ M₂
as : List R
bs : List S
hf : Surjective.{u_3 + 1, u_4 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
r : R
s : S
l₁ : List R
l₂ : List S
h_1 :
  List.Forall₂
    (fun (r : R) (s : S) ↦ ∀ (x : M), (f : (a : M) → M₂) (r • x) = HSMul.hSMul (β := M₂) s ((f : (a : M) → M₂) x : M₂))
    l₁ l₂
ih :
  AddSubgroup.map f (HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList l₁) ⊤).toAddSubgroup =
    (HSMul.hSMul (α := Ideal S) (β := Submodule S M₂) (Ideal.ofList l₂) ⊤).toAddSubgroup
h :
  f.comp (((toAddMonoidEnd R M : MonoidHom.{u_1, u_3} R (AddMonoid.End M)) : (a : R) → AddMonoid.End M) r) =
    AddMonoidHom.comp
      (((toAddMonoidEnd S M₂ : MonoidHom.{u_2, u_4} S (AddMonoid.End M₂)) : (a : S) → AddMonoid.End M₂) s) f
⊢ AddSubgroup.map f
      (AddSubgroup.map (G := M)
          (((toAddMonoidEnd R M : MonoidHom.{u_1, u_3} R (AddMonoid.End M)) : (a : R) → AddMonoid.End M) r) ⊤ ⊔
        (HSMul.hSMul (α := Submodule R R) (β := Submodule R M) (Ideal.ofList l₁) ⊤).toAddSubgroup) =
    AddSubgroup.map (G := M₂)
        (((toAddMonoidEnd S M₂ : MonoidHom.{u_2, u_4} S (AddMonoid.End M₂)) : (a : S) → AddMonoid.End M₂) s) ⊤ ⊔
      (HSMul.hSMul (α := Submodule S S) (β := Submodule S M₂) (Ideal.ofList l₂) ⊤).toAddSubgroup
have cons : AddSubgroup.map f
      (AddSubgroup.map (G := M)
        (((toAddMonoidEnd R M : MonoidHom.{u_1, u_3} R (AddMonoid.End M)) : (a : R) → AddMonoid.End M) r) ⊤) ⊔
    AddSubgroup.map f (HSMul.hSMul (α := Submodule R R) (β := Submodule R M) (Ideal.ofList l₁) ⊤).toAddSubgroup =
  AddSubgroup.map (G := M₂)
      (((toAddMonoidEnd S M₂ : MonoidHom.{u_2, u_4} S (AddMonoid.End M₂)) : (a : S) → AddMonoid.End M₂) s) ⊤ ⊔
    (HSMul.hSMul (α := Submodule S S) (β := Submodule S M₂) (Ideal.ofList l₂) ⊤).toAddSubgroup
Tactic: rw [AddSubgroup.map_sup, ih, map_map, h, ← map_map,
      map_top_of_surjective f hf]
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module S M₂
f : M →+ M₂
as : List R
bs : List S
hf : Surjective.{u_3 + 1, u_4 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
r : R
s : S
l₁ : List R
l₂ : List S
h_1 :
  List.Forall₂
    (fun (r : R) (s : S) ↦ ∀ (x : M), (f : (a : M) → M₂) (r • x) = HSMul.hSMul (β := M₂) s ((f : (a : M) → M₂) x : M₂))
    l₁ l₂
ih :
  AddSubgroup.map f (HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList l₁) ⊤).toAddSubgroup =
    (HSMul.hSMul (α := Ideal S) (β := Submodule S M₂) (Ideal.ofList l₂) ⊤).toAddSubgroup
h :
  f.comp (((toAddMonoidEnd R M : MonoidHom.{u_1, u_3} R (AddMonoid.End M)) : (a : R) → AddMonoid.End M) r) =
    AddMonoidHom.comp
      (((toAddMonoidEnd S M₂ : MonoidHom.{u_2, u_4} S (AddMonoid.End M₂)) : (a : S) → AddMonoid.End M₂) s) f
cons :
  AddSubgroup.map f
        (AddSubgroup.map (G := M)
          (((toAddMonoidEnd R M : MonoidHom.{u_1, u_3} R (AddMonoid.End M)) : (a : R) → AddMonoid.End M) r) ⊤) ⊔
      AddSubgroup.map f (HSMul.hSMul (α := Submodule R R) (β := Submodule R M) (Ideal.ofList l₁) ⊤).toAddSubgroup =
    AddSubgroup.map (G := M₂)
        (((toAddMonoidEnd S M₂ : MonoidHom.{u_2, u_4} S (AddMonoid.End M₂)) : (a : S) → AddMonoid.End M₂) s) ⊤ ⊔
      (HSMul.hSMul (α := Submodule S S) (β := Submodule S M₂) (Ideal.ofList l₂) ⊤).toAddSubgroup
⊢ AddSubgroup.map f
      (AddSubgroup.map (G := M)
          (((toAddMonoidEnd R M : MonoidHom.{u_1, u_3} R (AddMonoid.End M)) : (a : R) → AddMonoid.End M) r) ⊤ ⊔
        (HSMul.hSMul (α := Submodule R R) (β := Submodule R M) (Ideal.ofList l₁) ⊤).toAddSubgroup) =
    AddSubgroup.map (G := M₂)
        (((toAddMonoidEnd S M₂ : MonoidHom.{u_2, u_4} S (AddMonoid.End M₂)) : (a : S) → AddMonoid.End M₂) s) ⊤ ⊔
      (HSMul.hSMul (α := Submodule S S) (β := Submodule S M₂) (Ideal.ofList l₂) ⊤).toAddSubgroup
have cons₁ : AddSubgroup.map f
      (AddSubgroup.map (G := M)
        (((toAddMonoidEnd R M : MonoidHom.{u_1, u_3} R (AddMonoid.End M)) : (a : R) → AddMonoid.End M) r) ⊤) ⊔
    (HSMul.hSMul (α := Ideal S) (β := Submodule S M₂) (Ideal.ofList l₂) ⊤).toAddSubgroup =
  AddSubgroup.map (G := M₂)
      (((toAddMonoidEnd S M₂ : MonoidHom.{u_2, u_4} S (AddMonoid.End M₂)) : (a : S) → AddMonoid.End M₂) s) ⊤ ⊔
    (HSMul.hSMul (α := Submodule S S) (β := Submodule S M₂) (Ideal.ofList l₂) ⊤).toAddSubgroup
Tactic: rw [AddSubgroup.map_sup, ih, map_map, h, ← map_map,
      map_top_of_surjective f hf]
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module S M₂
f : M →+ M₂
as : List R
bs : List S
hf : Surjective.{u_3 + 1, u_4 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
r : R
s : S
l₁ : List R
l₂ : List S
h_1 :
  List.Forall₂
    (fun (r : R) (s : S) ↦ ∀ (x : M), (f : (a : M) → M₂) (r • x) = HSMul.hSMul (β := M₂) s ((f : (a : M) → M₂) x : M₂))
    l₁ l₂
ih :
  AddSubgroup.map f (HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList l₁) ⊤).toAddSubgroup =
    (HSMul.hSMul (α := Ideal S) (β := Submodule S M₂) (Ideal.ofList l₂) ⊤).toAddSubgroup
h :
  f.comp (((toAddMonoidEnd R M : MonoidHom.{u_1, u_3} R (AddMonoid.End M)) : (a : R) → AddMonoid.End M) r) =
    AddMonoidHom.comp
      (((toAddMonoidEnd S M₂ : MonoidHom.{u_2, u_4} S (AddMonoid.End M₂)) : (a : S) → AddMonoid.End M₂) s) f
cons :
  AddSubgroup.map f
        (AddSubgroup.map (G := M)
          (((toAddMonoidEnd R M : MonoidHom.{u_1, u_3} R (AddMonoid.End M)) : (a : R) → AddMonoid.End M) r) ⊤) ⊔
      AddSubgroup.map f (HSMul.hSMul (α := Submodule R R) (β := Submodule R M) (Ideal.ofList l₁) ⊤).toAddSubgroup =
    AddSubgroup.map (G := M₂)
        (((toAddMonoidEnd S M₂ : MonoidHom.{u_2, u_4} S (AddMonoid.End M₂)) : (a : S) → AddMonoid.End M₂) s) ⊤ ⊔
      (HSMul.hSMul (α := Submodule S S) (β := Submodule S M₂) (Ideal.ofList l₂) ⊤).toAddSubgroup
cons₁ :
  AddSubgroup.map f
        (AddSubgroup.map (G := M)
          (((toAddMonoidEnd R M : MonoidHom.{u_1, u_3} R (AddMonoid.End M)) : (a : R) → AddMonoid.End M) r) ⊤) ⊔
      (HSMul.hSMul (α := Ideal S) (β := Submodule S M₂) (Ideal.ofList l₂) ⊤).toAddSubgroup =
    AddSubgroup.map (G := M₂)
        (((toAddMonoidEnd S M₂ : MonoidHom.{u_2, u_4} S (AddMonoid.End M₂)) : (a : S) → AddMonoid.End M₂) s) ⊤ ⊔
      (HSMul.hSMul (α := Submodule S S) (β := Submodule S M₂) (Ideal.ofList l₂) ⊤).toAddSubgroup
⊢ AddSubgroup.map f
      (AddSubgroup.map (G := M)
          (((toAddMonoidEnd R M : MonoidHom.{u_1, u_3} R (AddMonoid.End M)) : (a : R) → AddMonoid.End M) r) ⊤ ⊔
        (HSMul.hSMul (α := Submodule R R) (β := Submodule R M) (Ideal.ofList l₁) ⊤).toAddSubgroup) =
    AddSubgroup.map (G := M₂)
        (((toAddMonoidEnd S M₂ : MonoidHom.{u_2, u_4} S (AddMonoid.End M₂)) : (a : S) → AddMonoid.End M₂) s) ⊤ ⊔
      (HSMul.hSMul (α := Submodule S S) (β := Submodule S M₂) (Ideal.ofList l₂) ⊤).toAddSubgroup
have cons₂ : AddSubgroup.map (G := M)
      (f.comp (((toAddMonoidEnd R M : MonoidHom.{u_1, u_3} R (AddMonoid.End M)) : (a : R) → AddMonoid.End M) r)) ⊤ ⊔
    (HSMul.hSMul (α := Ideal S) (β := Submodule S M₂) (Ideal.ofList l₂) ⊤).toAddSubgroup =
  AddSubgroup.map (G := M₂)
      (((toAddMonoidEnd S M₂ : MonoidHom.{u_2, u_4} S (AddMonoid.End M₂)) : (a : S) → AddMonoid.End M₂) s) ⊤ ⊔
    (HSMul.hSMul (α := Submodule S S) (β := Submodule S M₂) (Ideal.ofList l₂) ⊤).toAddSubgroup
Tactic: rw [AddSubgroup.map_sup, ih, map_map, h, ← map_map,
      map_top_of_surjective f hf]