awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Lattice (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set (Submodule R M)
t : R
m : M
h : m ∈ (sSup (toAddSubmonoid '' s)).carrier
⊢ t • m ∈ (sSup (toAddSubmonoid '' s)).carrier
have simp_rw : ∀ (h : Membership.mem (γ := AddSubmonoid M) (⨆ (a : (↑(toAddSubmonoid '' s) : Type u_3)), (↑a : AddSubmonoid M)) m),
  Membership.mem (γ := AddSubmonoid M) (⨆ (a : (↑(toAddSubmonoid '' s) : Type u_3)), (↑a : AddSubmonoid M)) (t • m)
Tactic: simp_rw [AddSubsemigroup.mem_carrier, AddSubmonoid.mem_toSubsemigroup, sSup_eq_iSup'] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Lattice (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set (Submodule R M)
t : R
m : M
p : (↑(toAddSubmonoid '' s) : Type u_3)
x : M
hx : x ∈ (↑p : AddSubmonoid M)
⊢ Membership.mem (γ := AddSubmonoid M) (⨆ (a : (↑(toAddSubmonoid '' s) : Type u_3)), (↑a : AddSubmonoid M)) (t • x)
have mem : ∀ (p : Submodule R M) (hp : p ∈ s)
  (hx :
    x ∈ (↑(Subtype.mk (p := fun (x : AddSubmonoid M) ↦ x ∈ toAddSubmonoid '' s) p.toAddSubmonoid sorry) : AddSubmonoid M)),
  Membership.mem (γ := AddSubmonoid M) (⨆ (a : (↑(toAddSubmonoid '' s) : Type u_3)), (↑a : AddSubmonoid M)) (t • x)
Tactic: obtain ⟨-, ⟨p : Submodule R M, hp : p ∈ s, rfl⟩⟩ := p
Cleared hypotheses: p, hx
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Lattice (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set (Submodule R M)
t : R
m x : M
p : Submodule R M
hp : p ∈ s
hx : x ∈ (↑(Subtype.mk (p := fun (x : AddSubmonoid M) ↦ x ∈ toAddSubmonoid '' s) p.toAddSubmonoid ⋯) : AddSubmonoid M)
⊢ Membership.mem (γ := AddSubmonoid M) (⨆ (a : (↑(toAddSubmonoid '' s) : Type u_3)), (↑a : AddSubmonoid M)) (t • x)
have mem : p.toAddSubmonoid ≤ ⨆ (q : (↑(toAddSubmonoid '' s) : Type u_3)), (↑q : AddSubmonoid M)
Tactic: suffices p.toAddSubmonoid ≤ ⨆ q : toAddSubmonoid '' s, (q : AddSubmonoid M) by
            exact this (smul_mem p t hx)
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Lattice (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set (Submodule R M)
t : R
m x : M
p : Submodule R M
hp : p ∈ s
hx : x ∈ (↑(Subtype.mk (p := fun (x : AddSubmonoid M) ↦ x ∈ toAddSubmonoid '' s) p.toAddSubmonoid ⋯) : AddSubmonoid M)
⊢ p.toAddSubmonoid ≤ ⨆ (q : (↑(toAddSubmonoid '' s) : Type u_3)), (↑q : AddSubmonoid M)
have mem : Membership.mem (γ := Set (AddSubmonoid M))
  (Set.range fun (q : (↑(toAddSubmonoid '' s) : Type u_3)) ↦ (↑q : AddSubmonoid M)) p.toAddSubmonoid
Tactic: apply le_sSup
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Lattice (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set (Submodule R M)
t : R
m x : M
p : Submodule R M
hp : p ∈ s
hx : x ∈ (↑(Subtype.mk (p := fun (x : AddSubmonoid M) ↦ x ∈ toAddSubmonoid '' s) p.toAddSubmonoid ⋯) : AddSubmonoid M)
⊢ Membership.mem (γ := Set (AddSubmonoid M))
    (Set.range fun (q : (↑(toAddSubmonoid '' s) : Type u_3)) ↦ (↑q : AddSubmonoid M)) p.toAddSubmonoid
have mem : Membership.mem (γ := Set (AddSubmonoid M)) {x : AddSubmonoid M | x ∈ toAddSubmonoid '' s} p.toAddSubmonoid
Tactic: rw [Subtype.range_coe_subtype]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Lattice (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set (Submodule R M)
t : R
m x y : M
hx : Membership.mem (γ := AddSubmonoid M) (⨆ (i : (↑(toAddSubmonoid '' s) : Type u_3)), (↑i : AddSubmonoid M)) x
hy : Membership.mem (γ := AddSubmonoid M) (⨆ (i : (↑(toAddSubmonoid '' s) : Type u_3)), (↑i : AddSubmonoid M)) y
mx : Membership.mem (γ := AddSubmonoid M) (⨆ (a : (↑(toAddSubmonoid '' s) : Type u_3)), (↑a : AddSubmonoid M)) (t • x)
my : Membership.mem (γ := AddSubmonoid M) (⨆ (a : (↑(toAddSubmonoid '' s) : Type u_3)), (↑a : AddSubmonoid M)) (t • y)
⊢ Membership.mem (γ := AddSubmonoid M) (⨆ (a : (↑(toAddSubmonoid '' s) : Type u_3)), (↑a : AddSubmonoid M))
    (t • (x + y))
have add : ∀
  (mx :
    Membership.mem (γ := AddSubmonoid M) (⨆ (a : (↑(toAddSubmonoid '' s) : Type u_3)), (↑a : AddSubmonoid M)) (t • x))
  (my :
    Membership.mem (γ := AddSubmonoid M) (⨆ (a : (↑(toAddSubmonoid '' s) : Type u_3)), (↑a : AddSubmonoid M)) (t • y)),
  Membership.mem (γ := AddSubmonoid M) (⨆ (a : (↑(toAddSubmonoid '' s) : Type u_3)), (↑a : AddSubmonoid M))
    (t • (x + y))
Tactic: revert mx my
Cleared hypotheses: mx, my
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Lattice (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set (Submodule R M)
t : R
m x y : M
hx : Membership.mem (γ := AddSubmonoid M) (⨆ (i : (↑(toAddSubmonoid '' s) : Type u_3)), (↑i : AddSubmonoid M)) x
hy : Membership.mem (γ := AddSubmonoid M) (⨆ (i : (↑(toAddSubmonoid '' s) : Type u_3)), (↑i : AddSubmonoid M)) y
⊢ ∀
    (mx :
      Membership.mem (γ := AddSubmonoid M) (⨆ (a : (↑(toAddSubmonoid '' s) : Type u_3)), (↑a : AddSubmonoid M)) (t • x))
    (my :
      Membership.mem (γ := AddSubmonoid M) (⨆ (a : (↑(toAddSubmonoid '' s) : Type u_3)), (↑a : AddSubmonoid M))
        (t • y)),
    Membership.mem (γ := AddSubmonoid M) (⨆ (a : (↑(toAddSubmonoid '' s) : Type u_3)), (↑a : AddSubmonoid M))
      (t • (x + y))
have add : ∀
  (mx :
    Membership.mem (γ := AddSubmonoid M) (⨆ (a : (↑(toAddSubmonoid '' s) : Type u_3)), (↑a : AddSubmonoid M)) (t • x))
  (my :
    Membership.mem (γ := AddSubmonoid M) (⨆ (a : (↑(toAddSubmonoid '' s) : Type u_3)), (↑a : AddSubmonoid M)) (t • y)),
  Membership.mem (γ := AddSubmonoid M) (⨆ (a : (↑(toAddSubmonoid '' s) : Type u_3)), (↑a : AddSubmonoid M))
    (t • x + t • y)
Tactic: simp_rw [smul_add]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Lattice (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set (Submodule R M)
t : R
m : M
h : Membership.mem (γ := AddSubmonoid M) (⨆ (a : (↑(toAddSubmonoid '' s) : Type u_3)), (↑a : AddSubmonoid M)) m
⊢ Membership.mem (γ := AddSubmonoid M) (⨆ (a : (↑(toAddSubmonoid '' s) : Type u_3)), (↑a : AddSubmonoid M)) (t • m)
have mem : ∀ (p : (↑(toAddSubmonoid '' s) : Type u_3)) (x : M) (hx : x ∈ (↑p : AddSubmonoid M)),
  Membership.mem (γ := AddSubmonoid M) (⨆ (a : (↑(toAddSubmonoid '' s) : Type u_3)), (↑a : AddSubmonoid M)) (t • x)
Tactic: induction h using AddSubmonoid.iSup_induction' with
        | mem p x hx =>
          obtain ⟨-, ⟨p : Submodule R M, hp : p ∈ s, rfl⟩⟩ := p
          suffices p.toAddSubmonoid ≤ ⨆ q : toAddSubmonoid '' s, (q : AddSubmonoid M) by
            exact this (smul_mem p t hx)
          apply le_sSup
          rw [Subtype.range_coe_subtype]
          exact ⟨p, hp, rfl⟩
        | zero => simpa only [smul_zero] using zero_mem _
        | add _ _ _ _ mx my => revert mx my; simp_rw [smul_add]; exact add_mem
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Lattice (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set (Submodule R M)
t : R
m : M
h : Membership.mem (γ := AddSubmonoid M) (⨆ (a : (↑(toAddSubmonoid '' s) : Type u_3)), (↑a : AddSubmonoid M)) m
mem :
  ∀ (p : (↑(toAddSubmonoid '' s) : Type u_3)) (x : M) (hx : x ∈ (↑p : AddSubmonoid M)),
    Membership.mem (γ := AddSubmonoid M) (⨆ (a : (↑(toAddSubmonoid '' s) : Type u_3)), (↑a : AddSubmonoid M)) (t • x)
⊢ Membership.mem (γ := AddSubmonoid M) (⨆ (a : (↑(toAddSubmonoid '' s) : Type u_3)), (↑a : AddSubmonoid M)) (t • m)
have zero : Membership.mem (γ := AddSubmonoid M) (⨆ (a : (↑(toAddSubmonoid '' s) : Type u_3)), (↑a : AddSubmonoid M))
  (HSMul.hSMul (β := M) t 0)
Tactic: induction h using AddSubmonoid.iSup_induction' with
        | mem p x hx =>
          obtain ⟨-, ⟨p : Submodule R M, hp : p ∈ s, rfl⟩⟩ := p
          suffices p.toAddSubmonoid ≤ ⨆ q : toAddSubmonoid '' s, (q : AddSubmonoid M) by
            exact this (smul_mem p t hx)
          apply le_sSup
          rw [Subtype.range_coe_subtype]
          exact ⟨p, hp, rfl⟩
        | zero => simpa only [smul_zero] using zero_mem _
        | add _ _ _ _ mx my => revert mx my; simp_rw [smul_add]; exact add_mem
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Lattice (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set (Submodule R M)
t : R
m : M
h : Membership.mem (γ := AddSubmonoid M) (⨆ (a : (↑(toAddSubmonoid '' s) : Type u_3)), (↑a : AddSubmonoid M)) m
mem :
  ∀ (p : (↑(toAddSubmonoid '' s) : Type u_3)) (x : M) (hx : x ∈ (↑p : AddSubmonoid M)),
    Membership.mem (γ := AddSubmonoid M) (⨆ (a : (↑(toAddSubmonoid '' s) : Type u_3)), (↑a : AddSubmonoid M)) (t • x)
zero :
  Membership.mem (γ := AddSubmonoid M) (⨆ (a : (↑(toAddSubmonoid '' s) : Type u_3)), (↑a : AddSubmonoid M))
    (HSMul.hSMul (β := M) t 0)
⊢ Membership.mem (γ := AddSubmonoid M) (⨆ (a : (↑(toAddSubmonoid '' s) : Type u_3)), (↑a : AddSubmonoid M)) (t • m)
have add : ∀ (x y : M),
  Membership.mem (γ := AddSubmonoid M) (⨆ (i : (↑(toAddSubmonoid '' s) : Type u_3)), (↑i : AddSubmonoid M)) x →
    Membership.mem (γ := AddSubmonoid M) (⨆ (i : (↑(toAddSubmonoid '' s) : Type u_3)), (↑i : AddSubmonoid M)) y →
      ∀
        (mx :
          Membership.mem (γ := AddSubmonoid M) (⨆ (a : (↑(toAddSubmonoid '' s) : Type u_3)), (↑a : AddSubmonoid M))
            (t • x))
        (my :
          Membership.mem (γ := AddSubmonoid M) (⨆ (a : (↑(toAddSubmonoid '' s) : Type u_3)), (↑a : AddSubmonoid M))
            (t • y)),
        Membership.mem (γ := AddSubmonoid M) (⨆ (a : (↑(toAddSubmonoid '' s) : Type u_3)), (↑a : AddSubmonoid M))
          (t • (x + y))
Tactic: induction h using AddSubmonoid.iSup_induction' with
        | mem p x hx =>
          obtain ⟨-, ⟨p : Submodule R M, hp : p ∈ s, rfl⟩⟩ := p
          suffices p.toAddSubmonoid ≤ ⨆ q : toAddSubmonoid '' s, (q : AddSubmonoid M) by
            exact this (smul_mem p t hx)
          apply le_sSup
          rw [Subtype.range_coe_subtype]
          exact ⟨p, hp, rfl⟩
        | zero => simpa only [smul_zero] using zero_mem _
        | add _ _ _ _ mx my => revert mx my; simp_rw [smul_add]; exact add_mem
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Lattice (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set (Submodule R M)
p : Submodule R M :=
  let __AddSubmonoid := sSup (toAddSubmonoid '' s);
  { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ }
⊢ (sSup s).toAddSubmonoid = sSup (toAddSubmonoid '' s)
have refine_1 : sSup s ≤ p
Tactic: refine le_antisymm (?_ : sSup s ≤ p) ?_
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Lattice (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set (Submodule R M)
p : Submodule R M :=
  let __AddSubmonoid := sSup (toAddSubmonoid '' s);
  { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ }
refine_1 : sSup s ≤ p
⊢ (sSup s).toAddSubmonoid = sSup (toAddSubmonoid '' s)
have refine_2 : sSup (toAddSubmonoid '' s) ≤ (sSup s).toAddSubmonoid
Tactic: refine le_antisymm (?_ : sSup s ≤ p) ?_
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Lattice (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Subsingleton.{u_3 + 1} (Submodule R M) ↔ Subsingleton.{u_3 + 1} (AddSubmonoid M)
have rw : Eq.{u_3 + 1} (α := Submodule R M) ⊥ ⊤ ↔ Subsingleton.{u_3 + 1} (AddSubmonoid M)
Tactic: rw [← subsingleton_iff_bot_eq_top, ← subsingleton_iff_bot_eq_top, ← toAddSubmonoid_inj,
      bot_toAddSubmonoid, top_toAddSubmonoid]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Lattice (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
rw : Eq.{u_3 + 1} (α := Submodule R M) ⊥ ⊤ ↔ Subsingleton.{u_3 + 1} (AddSubmonoid M)
⊢ Subsingleton.{u_3 + 1} (Submodule R M) ↔ Subsingleton.{u_3 + 1} (AddSubmonoid M)
have rw₁ : Eq.{u_3 + 1} (α := Submodule R M) ⊥ ⊤ ↔ Eq.{u_3 + 1} (α := AddSubmonoid M) ⊥ ⊤
Tactic: rw [← subsingleton_iff_bot_eq_top, ← subsingleton_iff_bot_eq_top, ← toAddSubmonoid_inj,
      bot_toAddSubmonoid, top_toAddSubmonoid]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Lattice (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
rw : Eq.{u_3 + 1} (α := Submodule R M) ⊥ ⊤ ↔ Subsingleton.{u_3 + 1} (AddSubmonoid M)
rw₁ : Eq.{u_3 + 1} (α := Submodule R M) ⊥ ⊤ ↔ Eq.{u_3 + 1} (α := AddSubmonoid M) ⊥ ⊤
⊢ Subsingleton.{u_3 + 1} (Submodule R M) ↔ Subsingleton.{u_3 + 1} (AddSubmonoid M)
have rw₂ : Eq.{u_3 + 1} (α := AddSubmonoid M) (toAddSubmonoid.{u_1, u_3} (R := R) ⊥) (toAddSubmonoid.{u_1, u_3} (R := R) ⊤) ↔
  Eq.{u_3 + 1} (α := AddSubmonoid M) ⊥ ⊤
Tactic: rw [← subsingleton_iff_bot_eq_top, ← subsingleton_iff_bot_eq_top, ← toAddSubmonoid_inj,
      bot_toAddSubmonoid, top_toAddSubmonoid]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Lattice (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
rw : Eq.{u_3 + 1} (α := Submodule R M) ⊥ ⊤ ↔ Subsingleton.{u_3 + 1} (AddSubmonoid M)
rw₁ : Eq.{u_3 + 1} (α := Submodule R M) ⊥ ⊤ ↔ Eq.{u_3 + 1} (α := AddSubmonoid M) ⊥ ⊤
rw₂ :
  Eq.{u_3 + 1} (α := AddSubmonoid M) (toAddSubmonoid.{u_1, u_3} (R := R) ⊥) (toAddSubmonoid.{u_1, u_3} (R := R) ⊤) ↔
    Eq.{u_3 + 1} (α := AddSubmonoid M) ⊥ ⊤
⊢ Subsingleton.{u_3 + 1} (Submodule R M) ↔ Subsingleton.{u_3 + 1} (AddSubmonoid M)
have rw₃ : Eq.{u_3 + 1} (α := AddSubmonoid M) ⊥ (toAddSubmonoid.{u_1, u_3} (R := R) ⊤) ↔ Eq.{u_3 + 1} (α := AddSubmonoid M) ⊥ ⊤
Tactic: rw [← subsingleton_iff_bot_eq_top, ← subsingleton_iff_bot_eq_top, ← toAddSubmonoid_inj,
      bot_toAddSubmonoid, top_toAddSubmonoid]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Lattice (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
rw : Eq.{u_3 + 1} (α := Submodule R M) ⊥ ⊤ ↔ Subsingleton.{u_3 + 1} (AddSubmonoid M)
rw₁ : Eq.{u_3 + 1} (α := Submodule R M) ⊥ ⊤ ↔ Eq.{u_3 + 1} (α := AddSubmonoid M) ⊥ ⊤
rw₂ :
  Eq.{u_3 + 1} (α := AddSubmonoid M) (toAddSubmonoid.{u_1, u_3} (R := R) ⊥) (toAddSubmonoid.{u_1, u_3} (R := R) ⊤) ↔
    Eq.{u_3 + 1} (α := AddSubmonoid M) ⊥ ⊤
rw₃ :
  Eq.{u_3 + 1} (α := AddSubmonoid M) ⊥ (toAddSubmonoid.{u_1, u_3} (R := R) ⊤) ↔ Eq.{u_3 + 1} (α := AddSubmonoid M) ⊥ ⊤
⊢ Subsingleton.{u_3 + 1} (Submodule R M) ↔ Subsingleton.{u_3 + 1} (AddSubmonoid M)
have rw₄ : Eq.{u_3 + 1} (α := AddSubmonoid M) ⊥ ⊤ ↔ Eq.{u_3 + 1} (α := AddSubmonoid M) ⊥ ⊤
Tactic: rw [← subsingleton_iff_bot_eq_top, ← subsingleton_iff_bot_eq_top, ← toAddSubmonoid_inj,
      bot_toAddSubmonoid, top_toAddSubmonoid]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Lattice (hypothesis)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module S M
inst_5 : SMul S R
inst_6 : IsScalarTower S R M
p q : Submodule R M
inst_7 : Subsingleton R
⊢ Unique (Submodule R M)
have this : Subsingleton M
Tactic: haveI := Module.subsingleton R M
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.LinearMap (goal)
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
ι : Type u_9
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M₁
inst_5 : AddCommMonoid M₂
inst_6 : AddCommMonoid M₃
inst_7 : Module R M
inst_8 : Module R M₁
inst_9 : Module R₂ M₂
inst_10 : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst_11 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f : M →ₛₗ[σ₁₂] M₂
g : M₂ →ₛₗ[σ₂₃] M₃
M₂' : Type u_10
inst_12 : AddCommMonoid M₂'
inst_13 : Module R₂ M₂'
p : M₂' →ₗ[R₂] M₂
hp : Injective.{u_10 + 1, u_7 + 1} (α := M₂') (β := M₂) (⇑p : (a : M₂') → M₂)
h :
  ∀ (c : M),
    Membership.mem.{u_7, u_7} (α := M₂) (γ := Set M₂) (range.{u_7, u_10 + 1} (ι := M₂') (⇑p : (a : M₂') → M₂))
      ((f : (a : M) → M₂) c : M₂)
b c : M
⊢ Exists.choose (p := fun (y : M₂') ↦
      Eq.{u_7 + 1} (α := M₂) ((p : (a : M₂') → M₂) y : M₂) ((f : (a : M) → M₂) (b + c) : M₂)) ⋯ =
    Exists.choose (p := fun (y : M₂') ↦
        Eq.{u_7 + 1} (α := M₂) ((p : (a : M₂') → M₂) y : M₂) ((f : (a : M) → M₂) b : M₂)) ⋯ +
      Exists.choose (p := fun (y : M₂') ↦
        Eq.{u_7 + 1} (α := M₂) ((p : (a : M₂') → M₂) y : M₂) ((f : (a : M) → M₂) c : M₂)) ⋯
have a : Eq.{u_7 + 1} (α := M₂)
  ((p : (a : M₂') → M₂)
      (Exists.choose (p := fun (y : M₂') ↦
        Eq.{u_7 + 1} (α := M₂) ((p : (a : M₂') → M₂) y : M₂) ((f : (a : M) → M₂) (b + c) : M₂)) sorry) :
    M₂)
  ((p : (a : M₂') → M₂)
      (Exists.choose (p := fun (y : M₂') ↦
          Eq.{u_7 + 1} (α := M₂) ((p : (a : M₂') → M₂) y : M₂) ((f : (a : M) → M₂) b : M₂)) sorry +
        Exists.choose (p := fun (y : M₂') ↦
          Eq.{u_7 + 1} (α := M₂) ((p : (a : M₂') → M₂) y : M₂) ((f : (a : M) → M₂) c : M₂)) sorry) :
    M₂)
Tactic: apply hp
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.LinearMap (goal)
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
ι : Type u_9
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M₁
inst_5 : AddCommMonoid M₂
inst_6 : AddCommMonoid M₃
inst_7 : Module R M
inst_8 : Module R M₁
inst_9 : Module R₂ M₂
inst_10 : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst_11 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f : M →ₛₗ[σ₁₂] M₂
g : M₂ →ₛₗ[σ₂₃] M₃
M₂' : Type u_10
inst_12 : AddCommMonoid M₂'
inst_13 : Module R₂ M₂'
p : M₂' →ₗ[R₂] M₂
hp : Injective.{u_10 + 1, u_7 + 1} (α := M₂') (β := M₂) (⇑p : (a : M₂') → M₂)
h :
  ∀ (c : M),
    Membership.mem.{u_7, u_7} (α := M₂) (γ := Set M₂) (range.{u_7, u_10 + 1} (ι := M₂') (⇑p : (a : M₂') → M₂))
      ((f : (a : M) → M₂) c : M₂)
b c : M
⊢ Eq.{u_7 + 1} (α := M₂)
    ((p : (a : M₂') → M₂)
        (Exists.choose (p := fun (y : M₂') ↦
          Eq.{u_7 + 1} (α := M₂) ((p : (a : M₂') → M₂) y : M₂) ((f : (a : M) → M₂) (b + c) : M₂)) ⋯) :
      M₂)
    ((p : (a : M₂') → M₂)
        (Exists.choose (p := fun (y : M₂') ↦
            Eq.{u_7 + 1} (α := M₂) ((p : (a : M₂') → M₂) y : M₂) ((f : (a : M) → M₂) b : M₂)) ⋯ +
          Exists.choose (p := fun (y : M₂') ↦
            Eq.{u_7 + 1} (α := M₂) ((p : (a : M₂') → M₂) y : M₂) ((f : (a : M) → M₂) c : M₂)) ⋯) :
      M₂)
have a : (p : (a : M₂') → M₂)
    (Exists.choose (p := fun (y : M₂') ↦
      (p : (a : M₂') → M₂) y = HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : M) → M₂) b : M₂) ((f : (a : M) → M₂) c : M₂))
      sorry) =
  HAdd.hAdd (α := M₂) (β := M₂)
    ((p : (a : M₂') → M₂)
        (Exists.choose (p := fun (y : M₂') ↦
          Eq.{u_7 + 1} (α := M₂) ((p : (a : M₂') → M₂) y : M₂) ((f : (a : M) → M₂) b : M₂)) sorry) :
      M₂)
    ((p : (a : M₂') → M₂)
        (Exists.choose (p := fun (y : M₂') ↦
          Eq.{u_7 + 1} (α := M₂) ((p : (a : M₂') → M₂) y : M₂) ((f : (a : M) → M₂) c : M₂)) sorry) :
      M₂)
Tactic: simp_rw [map_add, (h _).choose_spec, ← map_add, (h _).choose_spec]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.LinearMap (goal)
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
ι : Type u_9
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M₁
inst_5 : AddCommMonoid M₂
inst_6 : AddCommMonoid M₃
inst_7 : Module R M
inst_8 : Module R M₁
inst_9 : Module R₂ M₂
inst_10 : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst_11 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f : M →ₛₗ[σ₁₂] M₂
g : M₂ →ₛₗ[σ₂₃] M₃
M₂' : Type u_10
inst_12 : AddCommMonoid M₂'
inst_13 : Module R₂ M₂'
p : M₂' →ₗ[R₂] M₂
hp : Injective.{u_10 + 1, u_7 + 1} (α := M₂') (β := M₂) (⇑p : (a : M₂') → M₂)
h :
  ∀ (c : M),
    Membership.mem.{u_7, u_7} (α := M₂) (γ := Set M₂) (range.{u_7, u_10 + 1} (ι := M₂') (⇑p : (a : M₂') → M₂))
      ((f : (a : M) → M₂) c : M₂)
b c : M
a :
  (p : (a : M₂') → M₂)
      (Exists.choose (p := fun (y : M₂') ↦
        (p : (a : M₂') → M₂) y = HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : M) → M₂) b : M₂) ((f : (a : M) → M₂) c : M₂))
        ⋯) =
    HAdd.hAdd (α := M₂) (β := M₂)
      ((p : (a : M₂') → M₂)
          (Exists.choose (p := fun (y : M₂') ↦
            Eq.{u_7 + 1} (α := M₂) ((p : (a : M₂') → M₂) y : M₂) ((f : (a : M) → M₂) b : M₂)) ⋯) :
        M₂)
      ((p : (a : M₂') → M₂)
          (Exists.choose (p := fun (y : M₂') ↦
            Eq.{u_7 + 1} (α := M₂) ((p : (a : M₂') → M₂) y : M₂) ((f : (a : M) → M₂) c : M₂)) ⋯) :
        M₂)
⊢ Eq.{u_7 + 1} (α := M₂)
    ((p : (a : M₂') → M₂)
        (Exists.choose (p := fun (y : M₂') ↦
          Eq.{u_7 + 1} (α := M₂) ((p : (a : M₂') → M₂) y : M₂) ((f : (a : M) → M₂) (b + c) : M₂)) ⋯) :
      M₂)
    ((p : (a : M₂') → M₂)
        (Exists.choose (p := fun (y : M₂') ↦
            Eq.{u_7 + 1} (α := M₂) ((p : (a : M₂') → M₂) y : M₂) ((f : (a : M) → M₂) b : M₂)) ⋯ +
          Exists.choose (p := fun (y : M₂') ↦
            Eq.{u_7 + 1} (α := M₂) ((p : (a : M₂') → M₂) y : M₂) ((f : (a : M) → M₂) c : M₂)) ⋯) :
      M₂)
have a₁ : (p : (a : M₂') → M₂)
    (Exists.choose (p := fun (y : M₂') ↦
      (p : (a : M₂') → M₂) y = HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : M) → M₂) b : M₂) ((f : (a : M) → M₂) c : M₂))
      sorry) =
  HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : M) → M₂) b : M₂) ((f : (a : M) → M₂) c : M₂)
Tactic: simp_rw [map_add, (h _).choose_spec, ← map_add, (h _).choose_spec]