awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Span (goal)
Goal:
α : Type u_1
R : Type u_5
inst : Semiring R
β : Type u_7
u : α → β
f g : α →₀ R
hf :
  Membership.mem (α := β →₀ R) (γ := Submodule R (β →₀ R)) (span R (Set.range fun (x : α) ↦ single (u x) 1))
    ((lmapDomain R R u : (a : α →₀ R) → β →₀ R) f : β →₀ R)
hg :
  Membership.mem (α := β →₀ R) (γ := Submodule R (β →₀ R)) (span R (Set.range fun (x : α) ↦ single (u x) 1))
    ((lmapDomain R R u : (a : α →₀ R) → β →₀ R) g : β →₀ R)
⊢ Membership.mem (α := β →₀ R) (γ := Submodule R (β →₀ R)) (span R (Set.range fun (x : α) ↦ single (u x) 1))
    ((lmapDomain R R u : (a : α →₀ R) → β →₀ R) (f + g) : β →₀ R)
have refine_1 : Membership.mem (γ := Submodule R (β →₀ R)) (span R (Set.range fun (x : α) ↦ single (u x) 1))
  (HAdd.hAdd (α := β →₀ R) (β := β →₀ R) ((lmapDomain R R u : (a : α →₀ R) → β →₀ R) f : β →₀ R)
    ((lmapDomain R R u : (a : α →₀ R) → β →₀ R) g : β →₀ R))
Tactic: rw [map_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Span (goal)
Goal:
α : Type u_1
R : Type u_5
inst : Semiring R
β : Type u_7
u : α → β
x : α →₀ R
⊢ Membership.mem (α := β →₀ R) (γ := Submodule R (β →₀ R)) (span R (Set.range fun (x : α) ↦ single (u x) 1))
    ((lmapDomain R R u : (a : α →₀ R) → β →₀ R) x : β →₀ R)
have refine_1 : ∀ (i : α) (s : R),
  Membership.mem (α := β →₀ R) (γ := Submodule R (β →₀ R)) (span R (Set.range fun (x : α) ↦ single (u x) 1))
    ((lmapDomain R R u : (a : α →₀ R) → β →₀ R) (single i s) : β →₀ R)
Tactic: induction x using induction_linear with
    | single i s =>
        rw [lmapDomain_apply, mapDomain_single, ← Finsupp.smul_single_one]
        exact Submodule.smul_mem _ _ (Submodule.subset_span ⟨i, rfl⟩)
    | zero => simp
    | add f g hf hg =>
        rw [map_add]
        exact Submodule.add_mem _ hf hg
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Span (goal)
Goal:
α : Type u_1
R : Type u_5
inst : Semiring R
β : Type u_7
u : α → β
x : α →₀ R
refine_1 :
  ∀ (i : α) (s : R),
    Membership.mem (α := β →₀ R) (γ := Submodule R (β →₀ R)) (span R (Set.range fun (x : α) ↦ single (u x) 1))
      ((lmapDomain R R u : (a : α →₀ R) → β →₀ R) (single i s) : β →₀ R)
⊢ Membership.mem (α := β →₀ R) (γ := Submodule R (β →₀ R)) (span R (Set.range fun (x : α) ↦ single (u x) 1))
    ((lmapDomain R R u : (a : α →₀ R) → β →₀ R) x : β →₀ R)
have refine_1₁ : Membership.mem (γ := Submodule R (β →₀ R)) (span R (Set.range fun (x : α) ↦ single (u x) 1))
  ((lmapDomain R R u : (a : α →₀ R) → β →₀ R) 0)
Tactic: induction x using induction_linear with
    | single i s =>
        rw [lmapDomain_apply, mapDomain_single, ← Finsupp.smul_single_one]
        exact Submodule.smul_mem _ _ (Submodule.subset_span ⟨i, rfl⟩)
    | zero => simp
    | add f g hf hg =>
        rw [map_add]
        exact Submodule.add_mem _ hf hg
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Span (goal)
Goal:
α : Type u_1
R : Type u_5
inst : Semiring R
β : Type u_7
u : α → β
x : α →₀ R
refine_1 :
  ∀ (i : α) (s : R),
    Membership.mem (α := β →₀ R) (γ := Submodule R (β →₀ R)) (span R (Set.range fun (x : α) ↦ single (u x) 1))
      ((lmapDomain R R u : (a : α →₀ R) → β →₀ R) (single i s) : β →₀ R)
refine_1₁ :
  Membership.mem (γ := Submodule R (β →₀ R)) (span R (Set.range fun (x : α) ↦ single (u x) 1))
    ((lmapDomain R R u : (a : α →₀ R) → β →₀ R) 0)
⊢ Membership.mem (α := β →₀ R) (γ := Submodule R (β →₀ R)) (span R (Set.range fun (x : α) ↦ single (u x) 1))
    ((lmapDomain R R u : (a : α →₀ R) → β →₀ R) x : β →₀ R)
have refine_1₂ : ∀ (f g : α →₀ R)
  (hf :
    Membership.mem (α := β →₀ R) (γ := Submodule R (β →₀ R)) (span R (Set.range fun (x : α) ↦ single (u x) 1))
      ((lmapDomain R R u : (a : α →₀ R) → β →₀ R) f : β →₀ R))
  (hg :
    Membership.mem (α := β →₀ R) (γ := Submodule R (β →₀ R)) (span R (Set.range fun (x : α) ↦ single (u x) 1))
      ((lmapDomain R R u : (a : α →₀ R) → β →₀ R) g : β →₀ R)),
  Membership.mem (α := β →₀ R) (γ := Submodule R (β →₀ R)) (span R (Set.range fun (x : α) ↦ single (u x) 1))
    ((lmapDomain R R u : (a : α →₀ R) → β →₀ R) (f + g) : β →₀ R)
Tactic: induction x using induction_linear with
    | single i s =>
        rw [lmapDomain_apply, mapDomain_single, ← Finsupp.smul_single_one]
        exact Submodule.smul_mem _ _ (Submodule.subset_span ⟨i, rfl⟩)
    | zero => simp
    | add f g hf hg =>
        rw [map_add]
        exact Submodule.add_mem _ hf hg
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Span (goal)
Goal:
α : Type u_1
R : Type u_5
inst : Semiring R
β : Type u_7
u : α → β
⊢ LE.le (α := Submodule R (β →₀ R)) (span R (Set.range fun (x : α) ↦ single (u x) 1))
    (LinearMap.range (lmapDomain R R u))
have refine_2 : ∀ (y : α), single (u y) 1 ∈ (↑(LinearMap.range (lmapDomain R R u)) : Set (β →₀ R))
Tactic: rw [Submodule.span_le, Set.range_subset_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Span (goal)
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Eq (α := Submodule R (α →₀ M)) (span R {x : α →₀ M | ∃ (i : α) (x_1 : M), single i x_1 = x}) ⊤
have refine : ∀ (x : α →₀ M),
  Membership.mem (γ := Submodule R (α →₀ M)) (span R {x : α →₀ M | ∃ (i : α) (x_1 : M), single i x_1 = x}) x
Tactic: refine eq_top_iff'.mpr fun x ↦ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Span (goal)
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : α →₀ M
⊢ Membership.mem (γ := Submodule R (α →₀ M)) (span R {x : α →₀ M | ∃ (i : α) (x_1 : M), single i x_1 = x}) x
have zero : Membership.mem (γ := Submodule R (α →₀ M)) (span R {x : α →₀ M | ∃ (i : α) (x_1 : M), single i x_1 = x}) 0
Tactic: induction x using Finsupp.induction_linear with
  | zero => exact Submodule.zero_mem ..
  | add f g f_in g_in => exact add_mem f_in g_in
  | single a b => exact mem_span_of_mem ⟨a, b, rfl⟩
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Span (goal)
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : α →₀ M
zero : Membership.mem (γ := Submodule R (α →₀ M)) (span R {x : α →₀ M | ∃ (i : α) (x_1 : M), single i x_1 = x}) 0
⊢ Membership.mem (γ := Submodule R (α →₀ M)) (span R {x : α →₀ M | ∃ (i : α) (x_1 : M), single i x_1 = x}) x
have add : ∀ (f g : α →₀ M)
  (f_in : Membership.mem (γ := Submodule R (α →₀ M)) (span R {x : α →₀ M | ∃ (i : α) (x_1 : M), single i x_1 = x}) f)
  (g_in : Membership.mem (γ := Submodule R (α →₀ M)) (span R {x : α →₀ M | ∃ (i : α) (x_1 : M), single i x_1 = x}) g),
  Membership.mem (γ := Submodule R (α →₀ M)) (span R {x : α →₀ M | ∃ (i : α) (x_1 : M), single i x_1 = x}) (f + g)
Tactic: induction x using Finsupp.induction_linear with
  | zero => exact Submodule.zero_mem ..
  | add f g f_in g_in => exact add_mem f_in g_in
  | single a b => exact mem_span_of_mem ⟨a, b, rfl⟩
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Span (goal)
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : α →₀ M
zero : Membership.mem (γ := Submodule R (α →₀ M)) (span R {x : α →₀ M | ∃ (i : α) (x_1 : M), single i x_1 = x}) 0
add :
  ∀ (f g : α →₀ M)
    (f_in : Membership.mem (γ := Submodule R (α →₀ M)) (span R {x : α →₀ M | ∃ (i : α) (x_1 : M), single i x_1 = x}) f)
    (g_in : Membership.mem (γ := Submodule R (α →₀ M)) (span R {x : α →₀ M | ∃ (i : α) (x_1 : M), single i x_1 = x}) g),
    Membership.mem (γ := Submodule R (α →₀ M)) (span R {x : α →₀ M | ∃ (i : α) (x_1 : M), single i x_1 = x}) (f + g)
⊢ Membership.mem (γ := Submodule R (α →₀ M)) (span R {x : α →₀ M | ∃ (i : α) (x_1 : M), single i x_1 = x}) x
have single : ∀ (a : α) (b : M),
  Membership.mem (γ := Submodule R (α →₀ M)) (span R {x : α →₀ M | ∃ (i : α) (x_1 : M), single i x_1 = x}) (single a b)
Tactic: induction x using Finsupp.induction_linear with
  | zero => exact Submodule.zero_mem ..
  | add f g f_in g_in => exact add_mem f_in g_in
  | single a b => exact mem_span_of_mem ⟨a, b, rfl⟩
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Span (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_4
p : ι → Submodule R M
m : M
hm : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) m
⊢ ∃ (s : Finset ι), Membership.mem (γ := Submodule R M) (⨆ i ∈ s, p i) m
have this : ∀ (h : LE.le (α := Submodule R M) (R ∙ m) (⨆ (i : ι), p i)),
  ∃ (s : Finset ι), LE.le (α := Submodule R M) (R ∙ m) (⨆ i ∈ s, p i)
Tactic: have :=
    CompleteLattice.IsCompactElement.exists_finset_of_le_iSup (Submodule R M)
      (Submodule.singleton_span_isCompactElement m) p
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Span (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_4
p : ι → Submodule R M
m : M
hm : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) m
this :
  ∀ (h : LE.le (α := Submodule R M) (R ∙ m) (⨆ (i : ι), p i)),
    ∃ (s : Finset ι), LE.le (α := Submodule R M) (R ∙ m) (⨆ i ∈ s, p i)
⊢ ∃ (s : Finset ι), Membership.mem (γ := Submodule R M) (⨆ i ∈ s, p i) m
have this₁ : ∀ (h : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) m),
  ∃ (s : Finset ι), Membership.mem (γ := Submodule R M) (⨆ i ∈ s, p i) m
Tactic: simp only [Submodule.span_singleton_le_iff_mem] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Span (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Set (Submodule R M)
m : M
⊢ m ∈ sSup S ↔
    ∃ (s : Finset (Submodule R M)), (↑s : Set (Submodule R M)) ⊆ S ∧ Membership.mem (γ := Submodule R M) (⨆ i ∈ s, i) m
have rw : (∃ (s : Finset (Subtype (Membership.mem S))), Membership.mem (γ := Submodule R M) (⨆ i ∈ s, (↑i : Submodule R M)) m) ↔
  ∃ (s : Finset (Submodule R M)), (↑s : Set (Submodule R M)) ⊆ S ∧ Membership.mem (γ := Submodule R M) (⨆ i ∈ s, i) m
Tactic: rw [sSup_eq_iSup, iSup_subtype', Submodule.mem_iSup_iff_exists_finset]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Span (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Set (Submodule R M)
m : M
⊢ (∃ (s : Finset (Subtype (Membership.mem S))), Membership.mem (γ := Submodule R M) (⨆ i ∈ s, (↑i : Submodule R M)) m) ↔
    ∃ (s : Finset (Submodule R M)), (↑s : Set (Submodule R M)) ⊆ S ∧ Membership.mem (γ := Submodule R M) (⨆ i ∈ s, i) m
have refine_1 : (∃ (s : Finset (Subtype (Membership.mem S))), Membership.mem (γ := Submodule R M) (⨆ i ∈ s, (↑i : Submodule R M)) m) →
  ∀ (s : Finset (Subtype (Membership.mem S)))
    (hs : Membership.mem (γ := Submodule R M) (⨆ i ∈ s, (↑i : Submodule R M)) m),
    (↑(Finset.map (Function.Embedding.subtype fun (x : Submodule R M) ↦ x ∈ S) s) : Set (Submodule R M)) ⊆ S
Tactic: refine ⟨fun ⟨s, hs⟩ ↦ ⟨s.map (Function.Embedding.subtype (· ∈ S)), ?_, ?_⟩,
          fun ⟨s, hsS, hs⟩ ↦ ⟨s.preimage (↑) Subtype.coe_injective.injOn, ?_⟩⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Span (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Set (Submodule R M)
m : M
refine_1 :
  (∃ (s : Finset (Subtype (Membership.mem S))), Membership.mem (γ := Submodule R M) (⨆ i ∈ s, (↑i : Submodule R M)) m) →
    ∀ (s : Finset (Subtype (Membership.mem S)))
      (hs : Membership.mem (γ := Submodule R M) (⨆ i ∈ s, (↑i : Submodule R M)) m),
      (↑(Finset.map (Function.Embedding.subtype fun (x : Submodule R M) ↦ x ∈ S) s) : Set (Submodule R M)) ⊆ S
⊢ (∃ (s : Finset (Subtype (Membership.mem S))), Membership.mem (γ := Submodule R M) (⨆ i ∈ s, (↑i : Submodule R M)) m) ↔
    ∃ (s : Finset (Submodule R M)), (↑s : Set (Submodule R M)) ⊆ S ∧ Membership.mem (γ := Submodule R M) (⨆ i ∈ s, i) m
have refine_2 : (∃ (s : Finset (Subtype (Membership.mem S))), Membership.mem (γ := Submodule R M) (⨆ i ∈ s, (↑i : Submodule R M)) m) →
  ∀ (s : Finset (Subtype (Membership.mem S)))
    (hs : Membership.mem (γ := Submodule R M) (⨆ i ∈ s, (↑i : Submodule R M)) m),
    Membership.mem (γ := Submodule R M)
      (⨆ i ∈ Finset.map (Function.Embedding.subtype fun (x : Submodule R M) ↦ x ∈ S) s, i) m
Tactic: refine ⟨fun ⟨s, hs⟩ ↦ ⟨s.map (Function.Embedding.subtype (· ∈ S)), ?_, ?_⟩,
          fun ⟨s, hsS, hs⟩ ↦ ⟨s.preimage (↑) Subtype.coe_injective.injOn, ?_⟩⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Span (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Set (Submodule R M)
m : M
refine_1 :
  (∃ (s : Finset (Subtype (Membership.mem S))), Membership.mem (γ := Submodule R M) (⨆ i ∈ s, (↑i : Submodule R M)) m) →
    ∀ (s : Finset (Subtype (Membership.mem S)))
      (hs : Membership.mem (γ := Submodule R M) (⨆ i ∈ s, (↑i : Submodule R M)) m),
      (↑(Finset.map (Function.Embedding.subtype fun (x : Submodule R M) ↦ x ∈ S) s) : Set (Submodule R M)) ⊆ S
refine_2 :
  (∃ (s : Finset (Subtype (Membership.mem S))), Membership.mem (γ := Submodule R M) (⨆ i ∈ s, (↑i : Submodule R M)) m) →
    ∀ (s : Finset (Subtype (Membership.mem S)))
      (hs : Membership.mem (γ := Submodule R M) (⨆ i ∈ s, (↑i : Submodule R M)) m),
      Membership.mem (γ := Submodule R M)
        (⨆ i ∈ Finset.map (Function.Embedding.subtype fun (x : Submodule R M) ↦ x ∈ S) s, i) m
⊢ (∃ (s : Finset (Subtype (Membership.mem S))), Membership.mem (γ := Submodule R M) (⨆ i ∈ s, (↑i : Submodule R M)) m) ↔
    ∃ (s : Finset (Submodule R M)), (↑s : Set (Submodule R M)) ⊆ S ∧ Membership.mem (γ := Submodule R M) (⨆ i ∈ s, i) m
have refine_3 : (∃ (s : Finset (Submodule R M)), (↑s : Set (Submodule R M)) ⊆ S ∧ Membership.mem (γ := Submodule R M) (⨆ i ∈ s, i) m) →
  ∀ (s : Finset (Submodule R M)) (hsS : (↑s : Set (Submodule R M)) ⊆ S)
    (hs : Membership.mem (γ := Submodule R M) (⨆ i ∈ s, i) m),
    Membership.mem (γ := Submodule R M)
      (⨆ (i : Subtype (Membership.mem S)),
        ⨆ (_ :
          Membership.mem (γ := Finset (Subtype (Membership.mem S)))
            (s.preimage (Subtype.val (p := fun (x : Submodule R M) ↦ x ∈ S)) sorry) i),
          (↑i : Submodule R M))
      m
Tactic: refine ⟨fun ⟨s, hs⟩ ↦ ⟨s.map (Function.Embedding.subtype (· ∈ S)), ?_, ?_⟩,
          fun ⟨s, hsS, hs⟩ ↦ ⟨s.preimage (↑) Subtype.coe_injective.injOn, ?_⟩⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Span (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Set (Submodule R M)
m : M
h : ∃ (s : Finset (Subtype (Membership.mem S))), Membership.mem (γ := Submodule R M) (⨆ i ∈ s, (↑i : Submodule R M)) m
s : Finset (Subtype (Membership.mem S))
hs : Membership.mem (γ := Submodule R M) (⨆ i ∈ s, (↑i : Submodule R M)) m
⊢ Membership.mem (γ := Submodule R M)
    (⨆ i ∈ Finset.map (Function.Embedding.subtype fun (x : Submodule R M) ↦ x ∈ S) s, i) m
have refine_2 : Membership.mem (γ := Submodule R M)
  (⨆ (i : Submodule R M), ⨆ (hi : i ∈ S), ⨆ (_ : Subtype.mk (p := Membership.mem S) i hi ∈ s), i) m
Tactic: suffices m ∈ ⨆ (i) (hi : i ∈ S) (_ : ⟨i, hi⟩ ∈ s), i by simpa
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Span (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Set (Submodule R M)
m : M
h : ∃ (s : Finset (Submodule R M)), (↑s : Set (Submodule R M)) ⊆ S ∧ Membership.mem (γ := Submodule R M) (⨆ i ∈ s, i) m
s : Finset (Submodule R M)
hsS : (↑s : Set (Submodule R M)) ⊆ S
hs : Membership.mem (γ := Submodule R M) (⨆ i ∈ s, i) m
⊢ Eq.{u_2 + 1} (α := Submodule R M) (⨆ (i : Submodule R M), ⨆ (_ : i ∈ S ∧ i ∈ s), i) (⨆ i ∈ s, i)
have h : ∀ (x : Submodule R M), x ∈ s ↔ x ∈ S ∧ x ∈ s
Tactic: convert! rfl
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Span (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Set (Submodule R M)
m : M
h : ∃ (s : Finset (Submodule R M)), (↑s : Set (Submodule R M)) ⊆ S ∧ Membership.mem (γ := Submodule R M) (⨆ i ∈ s, i) m
s : Finset (Submodule R M)
hsS : (↑s : Set (Submodule R M)) ⊆ S
hs : Membership.mem (γ := Submodule R M) (⨆ i ∈ s, i) m
⊢ Membership.mem (γ := Submodule R M)
    (⨆ (i : Subtype (Membership.mem S)),
      ⨆ (_ :
        Membership.mem (γ := Finset (Subtype (Membership.mem S)))
          (s.preimage (Subtype.val (p := fun (x : Submodule R M) ↦ x ∈ S)) ⋯) i),
        (↑i : Submodule R M))
    m
have this : Eq.{u_2 + 1} (α := Submodule R M) (⨆ (i : Submodule R M), ⨆ (_ : i ∈ S ∧ i ∈ s), i) (⨆ i ∈ s, i)
Tactic: have : ⨆ (i) (_ : i ∈ S ∧ i ∈ s), i = ⨆ (i) (_ : i ∈ s), i := by convert! rfl; grind
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Span (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
φ : M →ₗ[R] N
f : σ → R
⊢ LinearMap.range (R := R) (M := σ →₀ M) (τ₁₂ := RingHom.id R)
      ((lsum R : (a : σ → M →ₗ[R] N) → (σ →₀ M) →ₗ[R] N) fun (x : σ) ↦ f x • φ) =
    Set.range f • φ.range
have simp_rw : Eq (α := Submodule R N)
  (span R
    (image (α := σ →₀ M) (⇑((lsum R : (a : σ → M →ₗ[R] N) → (σ →₀ M) →ₗ[R] N) fun (x : σ) ↦ f x • φ) : (a : σ →₀ M) → N)
      {x : σ →₀ M | ∃ (i : σ) (x_1 : M), single i x_1 = x}))
  (span R (HSMul.hSMul (β := Set N) (Set.range f) (image.{u_2, u_3} (α := M) (⇑φ : (a : M) → N) univ)))
Tactic: simp_rw [range_eq_map, ← span_single_eq_top, ← span_univ, map_span, set_smul_span]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Span (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
φ : M →ₗ[R] N
f : σ → R
⊢ Eq (α := Submodule R N)
    (span R
      (image (α := σ →₀ M)
        (⇑((lsum R : (a : σ → M →ₗ[R] N) → (σ →₀ M) →ₗ[R] N) fun (x : σ) ↦ f x • φ) : (a : σ →₀ M) → N)
        {x : σ →₀ M | ∃ (i : σ) (x_1 : M), single i x_1 = x}))
    (span R (HSMul.hSMul (β := Set N) (Set.range f) (image.{u_2, u_3} (α := M) (⇑φ : (a : M) → N) univ)))
have e_s : image (α := σ →₀ M) (⇑((lsum R : (a : σ → M →ₗ[R] N) → (σ →₀ M) →ₗ[R] N) fun (x : σ) ↦ f x • φ) : (a : σ →₀ M) → N)
    {x : σ →₀ M | ∃ (i : σ) (x_1 : M), single i x_1 = x} =
  HSMul.hSMul (β := Set N) (Set.range f) (image.{u_2, u_3} (α := M) (⇑φ : (a : M) → N) univ)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.SumProd (goal)
Goal:
α_1 : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
S : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : AddCommMonoid P
inst_7 : Module R P
α : Type u_7
β : Type u_8
m : R
x : α ⊕ β →₀ M
⊢ Equiv.toFun (AddEquiv.toEquiv sumFinsuppAddEquivProdFinsupp) (m • x) =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) m : R)
      (Equiv.toFun (AddEquiv.toEquiv sumFinsuppAddEquivProdFinsupp) x)
have fst : ∀ (a : α),
  Eq.{u_2 + 1} (α := M) (((Equiv.toFun (AddEquiv.toEquiv sumFinsuppAddEquivProdFinsupp) (m • x)).1 : (a : α) → M) a : M)
    (((HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) m : R)
              (Equiv.toFun (AddEquiv.toEquiv sumFinsuppAddEquivProdFinsupp) x)).1 :
          (a : α) → M)
        a :
      M)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.SumProd (goal)
Goal:
α_1 : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
S : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : AddCommMonoid P
inst_7 : Module R P
α : Type u_7
β : Type u_8
m : R
x : α ⊕ β →₀ M
fst :
  ∀ (a : α),
    Eq.{u_2 + 1} (α := M)
      (((Equiv.toFun (AddEquiv.toEquiv sumFinsuppAddEquivProdFinsupp) (m • x)).1 : (a : α) → M) a : M)
      (((HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) m : R)
                (Equiv.toFun (AddEquiv.toEquiv sumFinsuppAddEquivProdFinsupp) x)).1 :
            (a : α) → M)
          a :
        M)
⊢ Equiv.toFun (AddEquiv.toEquiv sumFinsuppAddEquivProdFinsupp) (m • x) =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) m : R)
      (Equiv.toFun (AddEquiv.toEquiv sumFinsuppAddEquivProdFinsupp) x)
have snd : ∀ (a : β),
  Eq.{u_2 + 1} (α := M) (((Equiv.toFun (AddEquiv.toEquiv sumFinsuppAddEquivProdFinsupp) (m • x)).2 : (a : β) → M) a : M)
    (((HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) m : R)
              (Equiv.toFun (AddEquiv.toEquiv sumFinsuppAddEquivProdFinsupp) x)).2 :
          (a : β) → M)
        a :
      M)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.SumProd (goal)
Goal:
α : Type u_1
M_1 : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
S : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M_1
inst_3 : Module R M_1
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : AddCommMonoid P
inst_7 : Module R P
η : Type u_7
inst_8 : Fintype η
ιs_1 : η → Type u_8
inst_9 : Zero α
M : Type u_9
ιs : η → Type u_10
inst_10 : AddCommMonoid M
inst_11 : Module R M
c : R
f : (j : η) × ιs j →₀ M
⊢ Equiv.toFun (AddEquiv.toEquiv (sigmaFinsuppAddEquivPiFinsupp (ιs := ιs))) (c • f) =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) c : R)
      (Equiv.toFun (AddEquiv.toEquiv (sigmaFinsuppAddEquivPiFinsupp (ιs := ιs))) f)
have h : ∀ (x : η) (a : ιs x),
  Eq.{u_9 + 1} (α := M)
    ((Equiv.toFun (AddEquiv.toEquiv (sigmaFinsuppAddEquivPiFinsupp (ιs := ιs))) (c • f) x : (a : ιs x) → M) a : M)
    ((HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) c : R)
            (Equiv.toFun (AddEquiv.toEquiv (sigmaFinsuppAddEquivPiFinsupp (ιs := ιs))) f) x :
          (a : ιs x) → M)
        a :
      M)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Supported (goal)
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
S : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : AddCommMonoid P
inst_7 : Module R P
s : Set α
p q : α →₀ M
hp : Membership.mem (γ := Set (α →₀ M)) {p : α →₀ M | (↑p.support : Set α) ⊆ s} p
hq : Membership.mem (γ := Set (α →₀ M)) {p : α →₀ M | (↑p.support : Set α) ⊆ s} q
⊢ Membership.mem (γ := Set (α →₀ M)) {p : α →₀ M | (↑p.support : Set α) ⊆ s} (p + q)
have refine : (↑(p.support ∪ q.support) : Set α) ⊆ (↑p.support : Set α) ∪ (↑q.support : Set α)
Tactic: refine Subset.trans (Subset.trans (Finset.coe_subset.2 support_add) ?_) (union_subset hp hq)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Supported (goal)
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
S : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : AddCommMonoid P
inst_7 : Module R P
s : Set α
p q : α →₀ M
hp : Membership.mem (γ := Set (α →₀ M)) {p : α →₀ M | (↑p.support : Set α) ⊆ s} p
hq : Membership.mem (γ := Set (α →₀ M)) {p : α →₀ M | (↑p.support : Set α) ⊆ s} q
⊢ (↑(p.support ∪ q.support) : Set α) ⊆ (↑p.support : Set α) ∪ (↑q.support : Set α)
have rw : (↑p.support : Set α) ∪ (↑q.support : Set α) ⊆ (↑p.support : Set α) ∪ (↑q.support : Set α)
Tactic: rw [Finset.coe_union]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Supported (goal)
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
S : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : AddCommMonoid P
inst_7 : Module R P
s : Set α
p q : α →₀ M
hp : Membership.mem (γ := Set (α →₀ M)) {p : α →₀ M | (↑p.support : Set α) ⊆ s} p
hq : Membership.mem (γ := Set (α →₀ M)) {p : α →₀ M | (↑p.support : Set α) ⊆ s} q
⊢ Membership.mem (γ := Set (α →₀ M)) {p : α →₀ M | (↑p.support : Set α) ⊆ s} (p + q)
have refine : (↑(p.support ∪ q.support) : Set α) ⊆ (↑p.support : Set α) ∪ (↑q.support : Set α)
Tactic: classical
    refine Subset.trans (Subset.trans (Finset.coe_subset.2 support_add) ?_) (union_subset hp hq)
    rw [Finset.coe_union]