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
S : Type u_7
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring S
inst_4 : SMul R S
inst_5 : Module S M
inst_6 : IsScalarTower R S M
p : Submodule R M
q : Submodule S M
h₁ : p ≤ restrictScalars R q
h₂ : q ≤ span S (↑p : Set M)
⊢ map q.subtype (span S (range (ι := ↥p) (⇑(inclusion h₁) : (a : ↥p) → ↥(restrictScalars R q)))) = q
have rw : span S
    (image (α := ↥q) (⇑q.subtype : (a : ↥q) → M)
      (range (ι := ↥p) (⇑(inclusion h₁) : (a : ↥p) → ↥(restrictScalars R q)))) =
  q
Tactic: rw [map_span]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_1
M : Type u_4
S : Type u_7
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring S
inst_4 : SMul R S
inst_5 : Module S M
inst_6 : IsScalarTower R S M
p : Submodule R M
q : Submodule S M
h₁ : p ≤ restrictScalars R q
h₂ : q ≤ span S (↑p : Set M)
this : (⇑q.subtype : (a : ↥q) → M) '' (↑(inclusion h₁).range : Set ↥(restrictScalars R q)) = (↑p : Set M)
⊢ span S
      (image (α := ↥q) (⇑q.subtype : (a : ↥q) → M)
        (range (ι := ↥p) (⇑(inclusion h₁) : (a : ↥p) → ↥(restrictScalars R q)))) =
    q
have refine : span S (↑p : Set M) ≤ q
Tactic: refine this ▸ le_antisymm ?_ h₂
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_1
M : Type u_4
S : Type u_7
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring S
inst_4 : SMul R S
inst_5 : Module S M
inst_6 : IsScalarTower R S M
p : Submodule R M
q : Submodule S M
h₁ : p ≤ restrictScalars R q
h₂ : q ≤ span S (↑p : Set M)
⊢ span S
      (image (α := ↥q) (⇑q.subtype : (a : ↥q) → M)
        (range (ι := ↥p) (⇑(inclusion h₁) : (a : ↥p) → ↥(restrictScalars R q)))) =
    q
have suffices : (⇑q.subtype : (a : ↥q) → M) '' (↑(inclusion h₁).range : Set ↥(restrictScalars R q)) = (↑p : Set M)
Tactic: suffices q.subtype '' ((LinearMap.range (inclusion h₁)) : Set <| q.restrictScalars R) = p by
    refine this ▸ le_antisymm ?_ h₂
    simpa using span_mono (R := S) h₁
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_1
M : Type u_4
S : Type u_7
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring S
inst_4 : SMul R S
inst_5 : Module S M
inst_6 : IsScalarTower R S M
p : Submodule R M
q : Submodule S M
h₁ : p ≤ restrictScalars R q
h₂ : q ≤ span S (↑p : Set M)
⊢ (⇑q.subtype : (a : ↥q) → M) '' (↑(inclusion h₁).range : Set ↥(restrictScalars R q)) = (↑p : Set M)
have h : ∀ (x : M),
  Membership.mem (γ := Set M) ((⇑q.subtype : (a : ↥q) → M) '' (↑(inclusion h₁).range : Set ↥(restrictScalars R q))) x ↔
    x ∈ (↑p : Set M)
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_8
M : Type u_9
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.IsTorsionFree R M
x y : M
⊢ Eq (α := Submodule R M) (R ∙ x) (R ∙ y) ↔ ∃ (z : Rˣ), z • x = y
have mp : Eq (α := Submodule R M) (R ∙ x) (R ∙ y) → ∃ (z : Rˣ), z • x = y
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_8
M : Type u_9
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.IsTorsionFree R M
x y : M
mp : Eq (α := Submodule R M) (R ∙ x) (R ∙ y) → ∃ (z : Rˣ), z • x = y
⊢ Eq (α := Submodule R M) (R ∙ x) (R ∙ y) ↔ ∃ (z : Rˣ), z • x = y
have mpr : (∃ (z : Rˣ), z • x = y) → Eq (α := Submodule R M) (R ∙ x) (R ∙ y)
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_8
M : Type u_9
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.IsTorsionFree R M
x y : M
⊢ Eq (α := Submodule R M) (R ∙ x) (R ∙ y) → ∃ (z : Rˣ), z • x = y
have mp : ((∃ (a : R), a • y = x) ∧ ∃ (a : R), a • x = y) → ∃ (z : Rˣ), z • x = y
Tactic: simp only [le_antisymm_iff, span_singleton_le_iff_mem, mem_span_singleton]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_8
M : Type u_9
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.IsTorsionFree R M
y : M
a b : R
hb : b • a • y = y
⊢ ∃ (z : Rˣ), z • a • y = y
have mp : ∀ (hb : b • HSMul.hSMul (β := M) a 0 = 0), ∃ (z : Rˣ), z • HSMul.hSMul (β := M) a 0 = 0
Tactic: rcases eq_or_ne y 0 with rfl | hy
Cleared hypotheses: y, hb
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_8
M : Type u_9
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.IsTorsionFree R M
y : M
a b : R
hb : b • a • y = y
mp : ∀ (hb : b • HSMul.hSMul (β := M) a 0 = 0), ∃ (z : Rˣ), z • HSMul.hSMul (β := M) a 0 = 0
⊢ ∃ (z : Rˣ), z • a • y = y
have mp₁ : ∀ (hy : y ≠ 0), ∃ (z : Rˣ), z • a • y = y
Tactic: rcases eq_or_ne y 0 with rfl | hy
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_8
M : Type u_9
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.IsTorsionFree R M
y : M
a b : R
hb : b • a • y = y
hy : y ≠ 0
⊢ ∃ (z : Rˣ), z • a • y = y
have mp : b * a = 1
Tactic: refine ⟨⟨b, a, ?_, ?_⟩, hb⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_8
M : Type u_9
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.IsTorsionFree R M
y : M
a b : R
hb : b • a • y = y
hy : y ≠ 0
mp : b * a = 1
⊢ ∃ (z : Rˣ), z • a • y = y
have mp₁ : a * b = 1
Tactic: refine ⟨⟨b, a, ?_, ?_⟩, hb⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_8
M : Type u_9
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.IsTorsionFree R M
y : M
a b : R
hb : b • a • y = y
hy : y ≠ 0
⊢ b * a = 1
have mp : Eq.{u_9 + 1} (α := M) ((fun (x : R) ↦ x • y) (b * a)) ((fun (x : R) ↦ x • y) 1)
Tactic: apply smul_left_injective R hy
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (hypothesis)
Goal:
R : Type u_8
M : Type u_9
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.IsTorsionFree R M
y : M
a b : R
hb : b • a • y = y
hy : y ≠ 0
⊢ a * b = 1
have hy₁ : b • a • y ≠ 0
Tactic: rw [← hb] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_8
M : Type u_9
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.IsTorsionFree R M
y : M
a b : R
hb : b • a • y = y
hy : b • a • y ≠ 0
⊢ a * b = 1
have mp : Eq.{u_9 + 1} (α := M) ((fun (x : R) ↦ x • a • y) (a * b)) ((fun (x : R) ↦ x • a • y) 1)
Tactic: apply smul_left_injective R (smul_ne_zero_iff.1 hy).2
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring R₂
σ₁₂ : R →+* R₂
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
inst_6 : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
x : M
s : Set M
h : Membership.mem (γ := Submodule R M) (span R s) x
⊢ Membership.mem.{u_5, u_5} (α := M₂) (γ := Submodule R₂ M₂) (span R₂ ((⇑f : (a : M) → M₂) '' s))
    ((f : (a : M) → M₂) x : M₂)
have rw : Membership.mem (α := M₂) (map f (span R s)) ((f : (a : M) → M₂) x : M₂)
Tactic: rw [Submodule.span_image]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring R₂
σ₁₂ : R →+* R₂
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
inst_6 : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
x : M
s : Set M
hf : Injective.{u_4 + 1, u_5 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
⊢ Membership.mem.{u_5, u_5} (α := M₂) (γ := Submodule R₂ M₂) (span R₂ ((⇑f : (a : M) → M₂) '' s))
      ((f : (a : M) → M₂) x : M₂) ↔
    Membership.mem (γ := Submodule R M) (span R s) x
have rw : x ∈ comap f (span R₂ ((⇑f : (a : M) → M₂) '' s)) ↔ Membership.mem (γ := Submodule R M) (span R s) x
Tactic: rw [← Submodule.mem_comap, ← Submodule.map_span, Submodule.comap_map_eq_of_injective hf]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring R₂
σ₁₂ : R →+* R₂
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
inst_6 : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
x : M
s : Set M
hf : Injective.{u_4 + 1, u_5 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
rw : x ∈ comap f (span R₂ ((⇑f : (a : M) → M₂) '' s)) ↔ Membership.mem (γ := Submodule R M) (span R s) x
⊢ Membership.mem.{u_5, u_5} (α := M₂) (γ := Submodule R₂ M₂) (span R₂ ((⇑f : (a : M) → M₂) '' s))
      ((f : (a : M) → M₂) x : M₂) ↔
    Membership.mem (γ := Submodule R M) (span R s) x
have rw₁ : x ∈ comap f (map f (span R s)) ↔ Membership.mem (γ := Submodule R M) (span R s) x
Tactic: rw [← Submodule.mem_comap, ← Submodule.map_span, Submodule.comap_map_eq_of_injective hf]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring R₂
σ₁₂ : R →+* R₂
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
inst_6 : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
x : M
s : Set M
hf : Injective.{u_4 + 1, u_5 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
rw : x ∈ comap f (span R₂ ((⇑f : (a : M) → M₂) '' s)) ↔ Membership.mem (γ := Submodule R M) (span R s) x
rw₁ : x ∈ comap f (map f (span R s)) ↔ Membership.mem (γ := Submodule R M) (span R s) x
⊢ Membership.mem.{u_5, u_5} (α := M₂) (γ := Submodule R₂ M₂) (span R₂ ((⇑f : (a : M) → M₂) '' s))
      ((f : (a : M) → M₂) x : M₂) ↔
    Membership.mem (γ := Submodule R M) (span R s) x
have rw₂ : Membership.mem (γ := Submodule R M) (span R s) x ↔ Membership.mem (γ := Submodule R M) (span R s) x
Tactic: rw [← Submodule.mem_comap, ← Submodule.map_span, Submodule.comap_map_eq_of_injective hf]
-- 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
α : Type u_8
inst_3 : Monoid α
inst_4 : DistribMulAction α M
inst_5 : SMulCommClass α R M
s : Set α
t : Set M
⊢ HSMul.hSMul (β := Submodule R M) s (span R t) = span R (s • t)
have simp_rw : Eq (α := Submodule R M) (⨆ a ∈ s, HSMul.hSMul (β := Submodule R M) a (span R t)) (span R (s • t))
Tactic: simp_rw [set_smul_eq_iSup, smul_span, iSup_span, Set.iUnion_smul_set]
-- 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
α : Type u_8
inst_3 : Monoid α
inst_4 : DistribMulAction α M
inst_5 : SMulCommClass α R M
s : Set α
t : Set M
simp_rw : Eq (α := Submodule R M) (⨆ a ∈ s, HSMul.hSMul (β := Submodule R M) a (span R t)) (span R (s • t))
⊢ HSMul.hSMul (β := Submodule R M) s (span R t) = span R (s • t)
have simp_rw₁ : Eq (α := Submodule R M) (⨆ a ∈ s, span R (a • t)) (span R (s • t))
Tactic: simp_rw [set_smul_eq_iSup, smul_span, iSup_span, Set.iUnion_smul_set]
-- 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
α : Type u_8
inst_3 : Monoid α
inst_4 : DistribMulAction α M
inst_5 : SMulCommClass α R M
s : Set α
t : Set M
simp_rw : Eq (α := Submodule R M) (⨆ a ∈ s, HSMul.hSMul (β := Submodule R M) a (span R t)) (span R (s • t))
simp_rw₁ : Eq (α := Submodule R M) (⨆ a ∈ s, span R (a • t)) (span R (s • t))
⊢ HSMul.hSMul (β := Submodule R M) s (span R t) = span R (s • t)
have simp_rw₂ : Eq (α := Submodule R M) (span R (⋃ i ∈ s, i • t)) (span R (s • t))
Tactic: simp_rw [set_smul_eq_iSup, smul_span, iSup_span, Set.iUnion_smul_set]
-- 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
⊢ Eq.{u_4 + 1} (α := AddSubmonoid M) (toAddSubmonoid.{u_1, u_4} (R := R) (⨆ (i : ι), p i))
    (⨆ (i : ι), (p i).toAddSubmonoid)
have refine : ∀ (x : M),
  Membership.mem (γ := AddSubmonoid M) (toAddSubmonoid.{u_1, u_4} (R := R) (⨆ (i : ι), p i)) x →
    Membership.mem (γ := AddSubmonoid M) (⨆ (i : ι), (p i).toAddSubmonoid) x
Tactic: refine le_antisymm (fun x => ?_) (iSup_le fun i => toAddSubmonoid_mono <| le_iSup _ i)
-- 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
x : M
⊢ Membership.mem (γ := AddSubmonoid M) (toAddSubmonoid.{u_1, u_4} (R := R) (⨆ (i : ι), p i)) x →
    Membership.mem (γ := AddSubmonoid M) (⨆ (i : ι), (p i).toAddSubmonoid) x
have simp_rw : Membership.mem (γ := Submodule R M) (span R (⋃ (i : ι), (↑(p i) : Set M))) x →
  Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) x
Tactic: simp_rw [iSup_eq_span, AddSubmonoid.iSup_eq_closure, mem_toAddSubmonoid, coe_toAddSubmonoid]
-- 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
x : M
hx : Membership.mem (γ := Submodule R M) (span R (⋃ (i : ι), (↑(p i) : Set M))) x
⊢ Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) x
have refine_1 : ∀ (x : M) (hx : Membership.mem (γ := Set M) (⋃ (i : ι), (↑(p i) : Set M)) x),
  Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) x
Tactic: refine Submodule.span_induction (fun x hx => ?_) ?_ (fun x y _ _ hx hy => ?_)
    (fun r x _ hx => ?_) hx
-- 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
x : M
hx : Membership.mem (γ := Submodule R M) (span R (⋃ (i : ι), (↑(p i) : Set M))) x
refine_1 :
  ∀ (x : M) (hx : Membership.mem (γ := Set M) (⋃ (i : ι), (↑(p i) : Set M)) x),
    Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) x
⊢ Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) x
have refine_2 : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) 0
Tactic: refine Submodule.span_induction (fun x hx => ?_) ?_ (fun x y _ _ hx hy => ?_)
    (fun r x _ hx => ?_) hx
-- 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
x : M
hx : Membership.mem (γ := Submodule R M) (span R (⋃ (i : ι), (↑(p i) : Set M))) x
refine_1 :
  ∀ (x : M) (hx : Membership.mem (γ := Set M) (⋃ (i : ι), (↑(p i) : Set M)) x),
    Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) x
refine_2 : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) 0
⊢ Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) x
have refine_3 : ∀ (x y : M),
  Membership.mem (γ := Submodule R M) (span R (⋃ (i : ι), (↑(p i) : Set M))) x →
    Membership.mem (γ := Submodule R M) (span R (⋃ (i : ι), (↑(p i) : Set M))) y →
      ∀ (hx : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) x)
        (hy : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) y),
        Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) (x + y)
Tactic: refine Submodule.span_induction (fun x hx => ?_) ?_ (fun x y _ _ hx hy => ?_)
    (fun r x _ hx => ?_) hx
-- 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
x : M
hx : Membership.mem (γ := Submodule R M) (span R (⋃ (i : ι), (↑(p i) : Set M))) x
refine_1 :
  ∀ (x : M) (hx : Membership.mem (γ := Set M) (⋃ (i : ι), (↑(p i) : Set M)) x),
    Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) x
refine_2 : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) 0
refine_3 :
  ∀ (x y : M),
    Membership.mem (γ := Submodule R M) (span R (⋃ (i : ι), (↑(p i) : Set M))) x →
      Membership.mem (γ := Submodule R M) (span R (⋃ (i : ι), (↑(p i) : Set M))) y →
        ∀ (hx : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) x)
          (hy : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) y),
          Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) (x + y)
⊢ Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) x
have refine_4 : ∀ (r : R) (x : M),
  Membership.mem (γ := Submodule R M) (span R (⋃ (i : ι), (↑(p i) : Set M))) x →
    ∀ (hx : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) x),
      Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) (r • x)
Tactic: refine Submodule.span_induction (fun x hx => ?_) ?_ (fun x y _ _ hx hy => ?_)
    (fun r x _ hx => ?_) hx
-- 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
x_1 : M
hx_1 : Membership.mem (γ := Submodule R M) (span R (⋃ (i : ι), (↑(p i) : Set M))) x_1
r : R
x : M
h : Membership.mem (γ := Submodule R M) (span R (⋃ (i : ι), (↑(p i) : Set M))) x
hx : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) x
⊢ Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) (r • x)
have refine_4 : ∀ (x : M) (h : Membership.mem (γ := Set M) (⋃ (i : ι), (↑(p i) : Set M)) x),
  Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) (r • x)
Tactic: refine AddSubmonoid.closure_induction ?_ ?_ ?_ hx
-- 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
x_1 : M
hx_1 : Membership.mem (γ := Submodule R M) (span R (⋃ (i : ι), (↑(p i) : Set M))) x_1
r : R
x : M
h : Membership.mem (γ := Submodule R M) (span R (⋃ (i : ι), (↑(p i) : Set M))) x
hx : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) x
refine_4 :
  ∀ (x : M) (h : Membership.mem (γ := Set M) (⋃ (i : ι), (↑(p i) : Set M)) x),
    Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) (r • x)
⊢ Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) (r • x)
have refine_4₁ : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) (HSMul.hSMul (β := M) r 0)
Tactic: refine AddSubmonoid.closure_induction ?_ ?_ ?_ hx
-- 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
x_1 : M
hx_1 : Membership.mem (γ := Submodule R M) (span R (⋃ (i : ι), (↑(p i) : Set M))) x_1
r : R
x : M
h : Membership.mem (γ := Submodule R M) (span R (⋃ (i : ι), (↑(p i) : Set M))) x
hx : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) x
refine_4 :
  ∀ (x : M) (h : Membership.mem (γ := Set M) (⋃ (i : ι), (↑(p i) : Set M)) x),
    Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) (r • x)
refine_4₁ :
  Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) (HSMul.hSMul (β := M) r 0)
⊢ Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) (r • x)
have refine_4₂ : ∀ (x y : M) (hx : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) x)
  (hy : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) y),
  Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) (r • x) →
    Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) (r • y) →
      Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) (r • (x + y))
Tactic: refine AddSubmonoid.closure_induction ?_ ?_ ?_ hx
-- 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
x_1 : M
hx_1 : Membership.mem (γ := Submodule R M) (span R (⋃ (i : ι), (↑(p i) : Set M))) x_1
r : R
x_2 : M
h : Membership.mem (γ := Submodule R M) (span R (⋃ (i : ι), (↑(p i) : Set M))) x_2
hx : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) x_2
x : M
i : ι
hix : x ∈ p i
⊢ Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) (r • x)
have apply : r • x ∈ (↑(p i) : Set M)
Tactic: apply AddSubmonoid.subset_closure (Set.mem_iUnion.mpr ⟨i, _⟩)
-- 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
x_1 : M
hx_1 : Membership.mem (γ := Submodule R M) (span R (⋃ (i : ι), (↑(p i) : Set M))) x_1
r : R
x : M
h : Membership.mem (γ := Submodule R M) (span R (⋃ (i : ι), (↑(p i) : Set M))) x
hx : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) x
⊢ Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) (HSMul.hSMul (β := M) r 0)
have refine_4 : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) 0
Tactic: rw [smul_zero]
-- 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
x_1 : M
hx_1 : Membership.mem (γ := Submodule R M) (span R (⋃ (i : ι), (↑(p i) : Set M))) x_1
r : R
x_2 : M
h : Membership.mem (γ := Submodule R M) (span R (⋃ (i : ι), (↑(p i) : Set M))) x_2
hx_2 : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) x_2
x y : M
hx_3 : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) x
hy_1 : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) y
hx : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) (r • x)
hy : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) (r • y)
⊢ Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) (r • (x + y))
have refine_4 : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure (⋃ (i : ι), (↑(p i) : Set M))) (r • x + r • y)
Tactic: rw [smul_add]
-- 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
ι : Sort u_8
p : ι → Submodule R M
motive : M → Prop
x : M
hx : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) x
mem : ∀ (i : ι), ∀ x ∈ p i, motive x
zero : motive 0
add : ∀ (x y : M), motive x → motive y → motive (x + y)
⊢ motive x
have hx₁ : Membership.mem (γ := AddSubmonoid M) (⨆ (i : ι), (p i).toAddSubmonoid) x
Tactic: rw [← mem_toAddSubmonoid, iSup_toAddSubmonoid] at hx
Cleared hypotheses: hx, mem, zero, add