awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Sort u_8
p : ι → Submodule R M
motive : (x : M) → Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) x → Prop
mem : ∀ (i : ι) (x : M) (hx : x ∈ p i), motive x ⋯
zero : motive 0 ⋯
add :
  ∀ (x y : M) (hx : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) x)
    (hy : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) y), motive x hx → motive y hy → motive (x + y) ⋯
x : M
hx : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) x
⊢ motive x hx
have refine : ∃ (x_1 : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) x), motive x x_1
Tactic: refine Exists.elim ?_ fun (hx : x ∈ ⨆ i, p i) (hc : motive x hx) => hc
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Sort u_8
p : ι → Submodule R M
motive : (x : M) → Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) x → Prop
mem : ∀ (i : ι) (x : M) (hx : x ∈ p i), motive x ⋯
zero : motive 0 ⋯
add :
  ∀ (x y : M) (hx : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) x)
    (hy : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) y), motive x hx → motive y hy → motive (x + y) ⋯
x : M
hx : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) x
⊢ ∃ (x_1 : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) x), motive x x_1
have refine_1 : ∀ (i : ι) (x : M) (hx : x ∈ p i),
  (fun (x : M) ↦ ∃ (hx : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) x), motive x hx) x
Tactic: refine iSup_induction p (motive := fun x : M ↦ ∃ (hx : x ∈ ⨆ i, p i), motive x hx) hx
    (fun i x hx => ?_) ?_ fun x y => ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Sort u_8
p : ι → Submodule R M
motive : (x : M) → Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) x → Prop
mem : ∀ (i : ι) (x : M) (hx : x ∈ p i), motive x ⋯
zero : motive 0 ⋯
add :
  ∀ (x y : M) (hx : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) x)
    (hy : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) y), motive x hx → motive y hy → motive (x + y) ⋯
x : M
hx : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) x
refine_1 :
  ∀ (i : ι) (x : M) (hx : x ∈ p i),
    (fun (x : M) ↦ ∃ (hx : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) x), motive x hx) x
⊢ ∃ (x_1 : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) x), motive x x_1
have refine_2 : (fun (x : M) ↦ ∃ (hx : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) x), motive x hx) 0
Tactic: refine iSup_induction p (motive := fun x : M ↦ ∃ (hx : x ∈ ⨆ i, p i), motive x hx) hx
    (fun i x hx => ?_) ?_ fun x y => ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Sort u_8
p : ι → Submodule R M
motive : (x : M) → Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) x → Prop
mem : ∀ (i : ι) (x : M) (hx : x ∈ p i), motive x ⋯
zero : motive 0 ⋯
add :
  ∀ (x y : M) (hx : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) x)
    (hy : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) y), motive x hx → motive y hy → motive (x + y) ⋯
x : M
hx : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) x
refine_1 :
  ∀ (i : ι) (x : M) (hx : x ∈ p i),
    (fun (x : M) ↦ ∃ (hx : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) x), motive x hx) x
refine_2 : ∃ (hx : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) 0), motive 0 hx
⊢ ∃ (x_1 : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) x), motive x x_1
have refine_3 : ∀ (x y : M),
  (fun (x : M) ↦ ∃ (hx : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) x), motive x hx) x →
    (fun (x : M) ↦ ∃ (hx : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) x), motive x hx) y →
      (fun (x : M) ↦ ∃ (hx : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) x), motive x hx) (x + y)
Tactic: refine iSup_induction p (motive := fun x : M ↦ ∃ (hx : x ∈ ⨆ i, p i), motive x hx) hx
    (fun i x hx => ?_) ?_ fun x y => ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
⊢ IsCompactElement (α := Submodule R M) (R ∙ x)
have rw : ∀ (s : Set (Submodule R M)),
  s.Nonempty → DirectedOn (fun (x1 x2 : Submodule R M) ↦ x1 ≤ x2) s → R ∙ x ≤ sSup s → ∃ x_1 ∈ s, R ∙ x ≤ x_1
Tactic: rw [CompleteLattice.isCompactElement_iff_le_of_directed_sSup_le]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (hypothesis)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
d : Set (Submodule R M)
hemp : d.Nonempty
hdir : DirectedOn (fun (x1 x2 : Submodule R M) ↦ x1 ≤ x2) d
hsup : R ∙ x ≤ sSup d
⊢ ∃ x_1 ∈ d, R ∙ x ≤ x_1
have this : x ∈ sSup d
Tactic: have : x ∈ (sSup d) := (SetLike.le_def.mp hsup) (mem_span_singleton_self x)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
d : Set (Submodule R M)
hemp : d.Nonempty
hdir : DirectedOn (fun (x1 x2 : Submodule R M) ↦ x1 ≤ x2) d
hsup : R ∙ x ≤ sSup d
this : x ∈ sSup d
⊢ ∃ x_1 ∈ d, R ∙ x ≤ x_1
have obtain : ∀ (y : Submodule R M) (hyd : y ∈ d) (hxy : x ∈ y), ∃ x_1 ∈ d, R ∙ x ≤ x_1
Tactic: obtain ⟨y, ⟨hyd, hxy⟩⟩ := (mem_sSup_of_directed hemp hdir).mp this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Finset M
⊢ IsCompactElement (α := Submodule R M) (span R (↑S : Set M))
have rw : IsCompactElement.{u_4} (α := Submodule R M) (⨆ x ∈ (↑S : Set M), R ∙ x)
Tactic: rw [span_eq_iSup_of_singleton_spans]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Finset M
⊢ IsCompactElement.{u_4} (α := Submodule R M) (⨆ x ∈ S, R ∙ x)
have rw : IsCompactElement (α := Submodule R M) (S.sup fun (x : M) ↦ R ∙ x)
Tactic: rw [← Finset.sup_eq_iSup]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_1
R₂ : Type u_2
K : Type u_3
M : Type u_4
M₂ : Type u_5
V : Type u_6
S : Type u_7
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
p p' : Submodule R M
inst_3 : Semiring R₂
σ₁₂ : R →+* R₂
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
s_1 t_1 : Set M
s t : Submodule R M
ht : Membership.mem (γ := Set (Submodule R M)) ((fun (x : M) ↦ R ∙ x) '' (↑s : Set M)) t
⊢ IsCompactElement t
have rcases : ∀ x ∈ (↑s : Set M),
  ∀ (ht : Membership.mem (γ := Set (Submodule R M)) ((fun (x : M) ↦ R ∙ x) '' (↑s : Set M)) (R ∙ x)),
    IsCompactElement (α := Submodule R M) (R ∙ x)
Tactic: rcases (Set.mem_image _ _ _).1 ht with ⟨x, _, rfl⟩
Cleared hypotheses: t, ht
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_1
R₂ : Type u_2
K : Type u_3
M : Type u_4
M₂ : Type u_5
V : Type u_6
S : Type u_7
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
p p' : Submodule R M
inst_3 : Semiring R₂
σ₁₂ : R →+* R₂
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
s_1 t : Set M
s : Submodule R M
⊢ sSup ((fun (x : M) ↦ R ∙ x) '' (↑s : Set M)) = s
have rw : ⨆ (a : Submodule R M), ⨆ (_ : Membership.mem (γ := Set (Submodule R M)) ((fun (x : M) ↦ R ∙ x) '' (↑s : Set M)) a), a =
  s
Tactic: rw [sSup_eq_iSup, iSup_image, ← span_eq_iSup_of_singleton_spans, span_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_1
R₂ : Type u_2
K : Type u_3
M : Type u_4
M₂ : Type u_5
V : Type u_6
S : Type u_7
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
p p' : Submodule R M
inst_3 : Semiring R₂
σ₁₂ : R →+* R₂
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
s_1 t : Set M
s : Submodule R M
rw :
  ⨆ (a : Submodule R M),
      ⨆ (_ : Membership.mem (γ := Set (Submodule R M)) ((fun (x : M) ↦ R ∙ x) '' (↑s : Set M)) a), a =
    s
⊢ sSup ((fun (x : M) ↦ R ∙ x) '' (↑s : Set M)) = s
have rw₁ : ⨆ b ∈ (↑s : Set M), R ∙ b = s
Tactic: rw [sSup_eq_iSup, iSup_image, ← span_eq_iSup_of_singleton_spans, span_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_1
R₂ : Type u_2
K : Type u_3
M : Type u_4
M₂ : Type u_5
V : Type u_6
S : Type u_7
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
p p' : Submodule R M
inst_3 : Semiring R₂
σ₁₂ : R →+* R₂
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
s_1 t : Set M
s : Submodule R M
rw :
  ⨆ (a : Submodule R M),
      ⨆ (_ : Membership.mem (γ := Set (Submodule R M)) ((fun (x : M) ↦ R ∙ x) '' (↑s : Set M)) a), a =
    s
rw₁ : ⨆ b ∈ (↑s : Set M), R ∙ b = s
⊢ sSup ((fun (x : M) ↦ R ∙ x) '' (↑s : Set M)) = s
have rw₂ : span R (↑s : Set M) = s
Tactic: rw [sSup_eq_iSup, iSup_image, ← span_eq_iSup_of_singleton_spans, span_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_1
R₂ : Type u_2
K : Type u_3
M : Type u_4
M₂ : Type u_5
V : Type u_6
S : Type u_7
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
p p' : Submodule R M
inst_3 : Semiring R₂
σ₁₂ : R →+* R₂
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
s_1 t : Set M
s : Submodule R M
rw :
  ⨆ (a : Submodule R M),
      ⨆ (_ : Membership.mem (γ := Set (Submodule R M)) ((fun (x : M) ↦ R ∙ x) '' (↑s : Set M)) a), a =
    s
rw₁ : ⨆ b ∈ (↑s : Set M), R ∙ b = s
rw₂ : span R (↑s : Set M) = s
⊢ sSup ((fun (x : M) ↦ R ∙ x) '' (↑s : Set M)) = s
have rw₃ : s = s
Tactic: rw [sSup_eq_iSup, iSup_image, ← span_eq_iSup_of_singleton_spans, span_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_8
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
⊢ Eq (α := Submodule R (M × M')) (prod ⊤ ⊤) ⊤
have h : ∀ (x : M × M'), Membership.mem (γ := Submodule R (M × M')) (prod ⊤ ⊤) x ↔ Membership.mem (γ := Submodule R (M × M')) ⊤ x
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_8
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
⊢ Eq (α := Submodule R (M × M')) (prod ⊥ ⊥) ⊥
have h : ∀ (x : M) (y : M'),
  Membership.mem (γ := Submodule R (M × M')) (prod ⊥ ⊥) (x, y) ↔ Membership.mem (γ := Submodule R (M × M')) ⊥ (x, y)
Tactic: ext ⟨x, y⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p p' : Submodule R M
M' : Type u_8
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
q₁ q₁' : Submodule R M'
⊢ p.prod q₁ ⊔ p'.prod q₁' = (p ⊔ p').prod (q₁ ⊔ q₁')
have refine : (p ⊔ p').prod (q₁ ⊔ q₁') ≤ p.prod q₁ ⊔ p'.prod q₁'
Tactic: refine le_antisymm
    (sup_le (prod_mono le_sup_left le_sup_left) (prod_mono le_sup_right le_sup_right)) ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p p' : Submodule R M
M' : Type u_8
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
q₁ q₁' : Submodule R M'
⊢ (p ⊔ p').prod (q₁ ⊔ q₁') ≤ p.prod q₁ ⊔ p'.prod q₁'
have simp : ∀ (a : M) (b : M'), a ∈ p ⊔ p' → b ∈ q₁ ⊔ q₁' → (a, b) ∈ p.prod q₁ ⊔ p'.prod q₁'
Tactic: simp only [SetLike.le_def, mem_prod, and_imp, Prod.forall]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p p' : Submodule R M
M' : Type u_8
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
q₁ q₁' : Submodule R M'
xx : M
yy : M'
hxx : xx ∈ p ⊔ p'
hyy : yy ∈ q₁ ⊔ q₁'
⊢ (xx, yy) ∈ p.prod q₁ ⊔ p'.prod q₁'
have rcases : ∀ (x : M) (hx : x ∈ p) (x' : M) (hx' : x' ∈ p') (hxx : x + x' ∈ p ⊔ p'), (x + x', yy) ∈ p.prod q₁ ⊔ p'.prod q₁'
Tactic: rcases mem_sup.1 hxx with ⟨x, hx, x', hx', rfl⟩
Cleared hypotheses: xx, hxx
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p p' : Submodule R M
M' : Type u_8
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
q₁ q₁' : Submodule R M'
yy : M'
hyy : yy ∈ q₁ ⊔ q₁'
x : M
hx : x ∈ p
x' : M
hx' : x' ∈ p'
hxx : x + x' ∈ p ⊔ p'
⊢ (x + x', yy) ∈ p.prod q₁ ⊔ p'.prod q₁'
have rcases : ∀ (y : M') (hy : y ∈ q₁) (y' : M') (hy' : y' ∈ q₁') (hyy : y + y' ∈ q₁ ⊔ q₁'),
  (x + x', y + y') ∈ p.prod q₁ ⊔ p'.prod q₁'
Tactic: rcases mem_sup.1 hyy with ⟨y, hy, y', hy', rfl⟩
Cleared hypotheses: yy, hyy
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_9
M : Type u_10
N : Type u_11
P : Type u_12
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
P' : Submodule R P
s : Set M
t : Set N
B : M →ₗ[R] N →ₗ[R] P
hB : ∀ x ∈ s, ∀ y ∈ t, Membership.mem (α := P) P' ((((B : (a : M) → N →ₗ[R] P) x : N →ₗ[R] P) : (a : N) → P) y : P)
x : M
y : N
hx : Membership.mem (γ := Submodule R M) (span R s) x
hy : Membership.mem (γ := Submodule R N) (span R t) y
⊢ Membership.mem (α := P) P' ((((B : (a : M) → N →ₗ[R] P) x : N →ₗ[R] P) : (a : N) → P) y : P)
have mem_mem : ∀ (u : M) (v : N) (hu : u ∈ s) (hv : v ∈ t),
  Membership.mem (α := P) P' ((((B : (a : M) → N →ₗ[R] P) u : N →ₗ[R] P) : (a : N) → P) v : P)
Tactic: induction hx, hy using span_induction₂ with
  | mem_mem u v hu hv => exact hB u hu v hv
  | zero_left v hv => simp
  | zero_right u hu => simp
  | add_left u₁ u₂ v hu₁ hu₂ hv huv₁ huv₂ => simpa using add_mem huv₁ huv₂
  | add_right u v₁ v₂ hu hv₁ hv₂ huv₁ huv₂ => simpa using add_mem huv₁ huv₂
  | smul_left t u v hu hv huv => simpa using Submodule.smul_mem _ _ huv
  | smul_right t u v hu hv huv => simpa using Submodule.smul_mem _ _ huv
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_9
M : Type u_10
N : Type u_11
P : Type u_12
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
P' : Submodule R P
s : Set M
t : Set N
B : M →ₗ[R] N →ₗ[R] P
hB : ∀ x ∈ s, ∀ y ∈ t, Membership.mem (α := P) P' ((((B : (a : M) → N →ₗ[R] P) x : N →ₗ[R] P) : (a : N) → P) y : P)
x : M
y : N
hx : Membership.mem (γ := Submodule R M) (span R s) x
hy : Membership.mem (γ := Submodule R N) (span R t) y
mem_mem :
  ∀ (u : M) (v : N) (hu : u ∈ s) (hv : v ∈ t),
    Membership.mem (α := P) P' ((((B : (a : M) → N →ₗ[R] P) u : N →ₗ[R] P) : (a : N) → P) v : P)
⊢ Membership.mem (α := P) P' ((((B : (a : M) → N →ₗ[R] P) x : N →ₗ[R] P) : (a : N) → P) y : P)
have zero_left : ∀ (v : N) (hv : Membership.mem (γ := Submodule R N) (span R t) v),
  Membership.mem (α := P) P' (((B : (a : M) → N →ₗ[R] P) 0 : (a : N) → P) v : P)
Tactic: induction hx, hy using span_induction₂ with
  | mem_mem u v hu hv => exact hB u hu v hv
  | zero_left v hv => simp
  | zero_right u hu => simp
  | add_left u₁ u₂ v hu₁ hu₂ hv huv₁ huv₂ => simpa using add_mem huv₁ huv₂
  | add_right u v₁ v₂ hu hv₁ hv₂ huv₁ huv₂ => simpa using add_mem huv₁ huv₂
  | smul_left t u v hu hv huv => simpa using Submodule.smul_mem _ _ huv
  | smul_right t u v hu hv huv => simpa using Submodule.smul_mem _ _ huv
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_9
M : Type u_10
N : Type u_11
P : Type u_12
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
P' : Submodule R P
s : Set M
t : Set N
B : M →ₗ[R] N →ₗ[R] P
hB : ∀ x ∈ s, ∀ y ∈ t, Membership.mem (α := P) P' ((((B : (a : M) → N →ₗ[R] P) x : N →ₗ[R] P) : (a : N) → P) y : P)
x : M
y : N
hx : Membership.mem (γ := Submodule R M) (span R s) x
hy : Membership.mem (γ := Submodule R N) (span R t) y
mem_mem :
  ∀ (u : M) (v : N) (hu : u ∈ s) (hv : v ∈ t),
    Membership.mem (α := P) P' ((((B : (a : M) → N →ₗ[R] P) u : N →ₗ[R] P) : (a : N) → P) v : P)
zero_left :
  ∀ (v : N) (hv : Membership.mem (γ := Submodule R N) (span R t) v),
    Membership.mem (α := P) P' (((B : (a : M) → N →ₗ[R] P) 0 : (a : N) → P) v : P)
⊢ Membership.mem (α := P) P' ((((B : (a : M) → N →ₗ[R] P) x : N →ₗ[R] P) : (a : N) → P) y : P)
have zero_right : ∀ (u : M) (hu : Membership.mem (γ := Submodule R M) (span R s) u),
  Membership.mem (α := P) P' ((((B : (a : M) → N →ₗ[R] P) u : N →ₗ[R] P) : (a : N) → P) 0 : P)
Tactic: induction hx, hy using span_induction₂ with
  | mem_mem u v hu hv => exact hB u hu v hv
  | zero_left v hv => simp
  | zero_right u hu => simp
  | add_left u₁ u₂ v hu₁ hu₂ hv huv₁ huv₂ => simpa using add_mem huv₁ huv₂
  | add_right u v₁ v₂ hu hv₁ hv₂ huv₁ huv₂ => simpa using add_mem huv₁ huv₂
  | smul_left t u v hu hv huv => simpa using Submodule.smul_mem _ _ huv
  | smul_right t u v hu hv huv => simpa using Submodule.smul_mem _ _ huv
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_9
M : Type u_10
N : Type u_11
P : Type u_12
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
P' : Submodule R P
s : Set M
t : Set N
B : M →ₗ[R] N →ₗ[R] P
hB : ∀ x ∈ s, ∀ y ∈ t, Membership.mem (α := P) P' ((((B : (a : M) → N →ₗ[R] P) x : N →ₗ[R] P) : (a : N) → P) y : P)
x : M
y : N
hx : Membership.mem (γ := Submodule R M) (span R s) x
hy : Membership.mem (γ := Submodule R N) (span R t) y
mem_mem :
  ∀ (u : M) (v : N) (hu : u ∈ s) (hv : v ∈ t),
    Membership.mem (α := P) P' ((((B : (a : M) → N →ₗ[R] P) u : N →ₗ[R] P) : (a : N) → P) v : P)
zero_left :
  ∀ (v : N) (hv : Membership.mem (γ := Submodule R N) (span R t) v),
    Membership.mem (α := P) P' (((B : (a : M) → N →ₗ[R] P) 0 : (a : N) → P) v : P)
zero_right :
  ∀ (u : M) (hu : Membership.mem (γ := Submodule R M) (span R s) u),
    Membership.mem (α := P) P' ((((B : (a : M) → N →ₗ[R] P) u : N →ₗ[R] P) : (a : N) → P) 0 : P)
⊢ Membership.mem (α := P) P' ((((B : (a : M) → N →ₗ[R] P) x : N →ₗ[R] P) : (a : N) → P) y : P)
have add_left : ∀ (u₁ u₂ : M) (v : N) (hu₁ : Membership.mem (γ := Submodule R M) (span R s) u₁)
  (hu₂ : Membership.mem (γ := Submodule R M) (span R s) u₂) (hv : Membership.mem (γ := Submodule R N) (span R t) v)
  (huv₁ : Membership.mem (α := P) P' ((((B : (a : M) → N →ₗ[R] P) u₁ : N →ₗ[R] P) : (a : N) → P) v : P))
  (huv₂ : Membership.mem (α := P) P' ((((B : (a : M) → N →ₗ[R] P) u₂ : N →ₗ[R] P) : (a : N) → P) v : P)),
  Membership.mem (α := P) P' ((((B : (a : M) → N →ₗ[R] P) (u₁ + u₂) : N →ₗ[R] P) : (a : N) → P) v : P)
Tactic: induction hx, hy using span_induction₂ with
  | mem_mem u v hu hv => exact hB u hu v hv
  | zero_left v hv => simp
  | zero_right u hu => simp
  | add_left u₁ u₂ v hu₁ hu₂ hv huv₁ huv₂ => simpa using add_mem huv₁ huv₂
  | add_right u v₁ v₂ hu hv₁ hv₂ huv₁ huv₂ => simpa using add_mem huv₁ huv₂
  | smul_left t u v hu hv huv => simpa using Submodule.smul_mem _ _ huv
  | smul_right t u v hu hv huv => simpa using Submodule.smul_mem _ _ huv
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_9
M : Type u_10
N : Type u_11
P : Type u_12
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
P' : Submodule R P
s : Set M
t : Set N
B : M →ₗ[R] N →ₗ[R] P
hB : ∀ x ∈ s, ∀ y ∈ t, Membership.mem (α := P) P' ((((B : (a : M) → N →ₗ[R] P) x : N →ₗ[R] P) : (a : N) → P) y : P)
x : M
y : N
hx : Membership.mem (γ := Submodule R M) (span R s) x
hy : Membership.mem (γ := Submodule R N) (span R t) y
mem_mem :
  ∀ (u : M) (v : N) (hu : u ∈ s) (hv : v ∈ t),
    Membership.mem (α := P) P' ((((B : (a : M) → N →ₗ[R] P) u : N →ₗ[R] P) : (a : N) → P) v : P)
zero_left :
  ∀ (v : N) (hv : Membership.mem (γ := Submodule R N) (span R t) v),
    Membership.mem (α := P) P' (((B : (a : M) → N →ₗ[R] P) 0 : (a : N) → P) v : P)
zero_right :
  ∀ (u : M) (hu : Membership.mem (γ := Submodule R M) (span R s) u),
    Membership.mem (α := P) P' ((((B : (a : M) → N →ₗ[R] P) u : N →ₗ[R] P) : (a : N) → P) 0 : P)
add_left :
  ∀ (u₁ u₂ : M) (v : N) (hu₁ : Membership.mem (γ := Submodule R M) (span R s) u₁)
    (hu₂ : Membership.mem (γ := Submodule R M) (span R s) u₂) (hv : Membership.mem (γ := Submodule R N) (span R t) v)
    (huv₁ : Membership.mem (α := P) P' ((((B : (a : M) → N →ₗ[R] P) u₁ : N →ₗ[R] P) : (a : N) → P) v : P))
    (huv₂ : Membership.mem (α := P) P' ((((B : (a : M) → N →ₗ[R] P) u₂ : N →ₗ[R] P) : (a : N) → P) v : P)),
    Membership.mem (α := P) P' ((((B : (a : M) → N →ₗ[R] P) (u₁ + u₂) : N →ₗ[R] P) : (a : N) → P) v : P)
⊢ Membership.mem (α := P) P' ((((B : (a : M) → N →ₗ[R] P) x : N →ₗ[R] P) : (a : N) → P) y : P)
have add_right : ∀ (u : M) (v₁ v₂ : N) (hu : Membership.mem (γ := Submodule R M) (span R s) u)
  (hv₁ : Membership.mem (γ := Submodule R N) (span R t) v₁) (hv₂ : Membership.mem (γ := Submodule R N) (span R t) v₂)
  (huv₁ : Membership.mem (α := P) P' ((((B : (a : M) → N →ₗ[R] P) u : N →ₗ[R] P) : (a : N) → P) v₁ : P))
  (huv₂ : Membership.mem (α := P) P' ((((B : (a : M) → N →ₗ[R] P) u : N →ₗ[R] P) : (a : N) → P) v₂ : P)),
  Membership.mem (α := P) P' ((((B : (a : M) → N →ₗ[R] P) u : N →ₗ[R] P) : (a : N) → P) (v₁ + v₂) : P)
Tactic: induction hx, hy using span_induction₂ with
  | mem_mem u v hu hv => exact hB u hu v hv
  | zero_left v hv => simp
  | zero_right u hu => simp
  | add_left u₁ u₂ v hu₁ hu₂ hv huv₁ huv₂ => simpa using add_mem huv₁ huv₂
  | add_right u v₁ v₂ hu hv₁ hv₂ huv₁ huv₂ => simpa using add_mem huv₁ huv₂
  | smul_left t u v hu hv huv => simpa using Submodule.smul_mem _ _ huv
  | smul_right t u v hu hv huv => simpa using Submodule.smul_mem _ _ huv
Cleared hypotheses: hx, hy