awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 α
⊢ Membership.mem (γ := Set (α →₀ M)) {p : α →₀ M | (↑p.support : Set α) ⊆ s} 0
have simp : ∀ (x : α), Ne.{u_2 + 1} (α := M) 0 0 → x ∈ s
Tactic: simp only [subset_def, Finset.mem_coe, Set.mem_setOf_eq, mem_support_iff, zero_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Supported (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
p : α →₀ M
⊢ Membership.mem (γ := Submodule R (α →₀ M)) (supported M R (↑p.support : Set α)) p
have rw : (↑p.support : Set α) ⊆ (↑p.support : Set α)
Tactic: rw [Finsupp.mem_supported]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Supported (goal)
Goal:
α : Type u_1
R : Type u_5
inst : Semiring R
s : Set α
⊢ Eq (α := Submodule R (α →₀ R)) (supported R R s) (span R ((fun (i : α) ↦ single i 1) '' s))
have refine_1 : (fun (i : α) ↦ single i 1) '' s ⊆ (↑(supported R R s) : Set (α →₀ R))
Tactic: refine (span_eq_of_le _ ?_ (SetLike.le_def.2 fun l hl => ?_)).symm
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Supported (goal)
Goal:
α : Type u_1
R : Type u_5
inst : Semiring R
s : Set α
refine_1 : (fun (i : α) ↦ single i 1) '' s ⊆ (↑(supported R R s) : Set (α →₀ R))
⊢ Eq (α := Submodule R (α →₀ R)) (supported R R s) (span R ((fun (i : α) ↦ single i 1) '' s))
have refine_2 : ∀ (l : α →₀ R) (hl : Membership.mem (γ := Submodule R (α →₀ R)) (supported R R s) l),
  Membership.mem (γ := Submodule R (α →₀ R)) (span R ((fun (i : α) ↦ single i 1) '' s)) l
Tactic: refine (span_eq_of_le _ ?_ (SetLike.le_def.2 fun l hl => ?_)).symm
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Supported (goal)
Goal:
α : Type u_1
R : Type u_5
inst : Semiring R
s : Set α
l : α →₀ R
hl : Membership.mem (γ := Submodule R (α →₀ R)) (supported R R s) l
⊢ Membership.mem (γ := Submodule R (α →₀ R)) (span R ((fun (i : α) ↦ single i 1) '' s)) l
have refine_2 : Membership.mem (γ := Submodule R (α →₀ R)) (span R ((fun (i : α) ↦ single i 1) '' s)) (l.sum single)
Tactic: rw [← l.sum_single]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Supported (goal)
Goal:
α : Type u_1
R : Type u_5
inst : Semiring R
s : Set α
l : α →₀ R
hl : Membership.mem (γ := Submodule R (α →₀ R)) (supported R R s) l
⊢ Membership.mem (γ := Submodule R (α →₀ R)) (span R ((fun (i : α) ↦ single i 1) '' s)) (l.sum single)
have refine_2 : ∀ (i : α) (il : i ∈ l.support),
  Membership.mem (α := α →₀ R) (γ := Submodule R (α →₀ R)) (span R ((fun (i : α) ↦ single i 1) '' s))
    (single i ((l : (a : α) → R) i) : α →₀ R)
Tactic: refine sum_mem fun i il => ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Supported (goal)
Goal:
α : Type u_1
R : Type u_5
inst : Semiring R
s : Set α
l : α →₀ R
hl : Membership.mem (γ := Submodule R (α →₀ R)) (supported R R s) l
i : α
il : i ∈ l.support
⊢ Membership.mem (α := α →₀ R) (γ := Submodule R (α →₀ R)) (span R ((fun (i : α) ↦ single i 1) '' s))
    (single i ((l : (a : α) → R) i) : α →₀ R)
have refine_2 : Membership.mem (γ := Submodule R (α →₀ R)) (span R ((fun (i : α) ↦ single i 1) '' s))
  (HSMul.hSMul (α := R) (β := α →₀ R) ((l : (a : α) → R) i : R) (single i 1))
Tactic: rw [show single i (l i) = l i • single i 1 by simp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Supported (goal)
Goal:
α : Type u_1
R : Type u_5
inst : Semiring R
inst_1 : Nontrivial R
a : α
s : Set α
⊢ Membership.mem (γ := Submodule R (α →₀ R)) (span R ((fun (x : α) ↦ single x 1) '' s)) (single a 1) ↔ a ∈ s
have refine : ∀ (h : Membership.mem (γ := Submodule R (α →₀ R)) (span R ((fun (x : α) ↦ single x 1) '' s)) (single a 1)), a ∈ s
Tactic: refine ⟨fun h => ?_, fun h => Submodule.subset_span <| Set.mem_image_of_mem _ h⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Supported (hypothesis)
Goal:
α : Type u_1
R : Type u_5
inst : Semiring R
inst_1 : Nontrivial R
a : α
s : Set α
h : Membership.mem (γ := Submodule R (α →₀ R)) (span R ((fun (x : α) ↦ single x 1) '' s)) (single a 1)
⊢ a ∈ s
have h₁ : (↑{a} : Set α) ⊆ s
Tactic: rw [← Finsupp.supported_eq_span_single, Finsupp.mem_supported,
    Finsupp.support_single _ (one_ne_zero' R)] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Supported (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
s : Set α
inst_3 : DecidablePred fun (x : α) ↦ x ∈ s
⊢ Eq (α := ↥(supported M R s) →ₗ[R] ↥(supported M R s)) (restrictDom M R s ∘ₗ Submodule.subtype (supported M R s))
    LinearMap.id
have h : ∀ (l : ↥(supported M R s)) (a : α),
  Eq.{u_2 + 1} (α := M)
    (((↑((restrictDom M R s ∘ₗ Submodule.subtype (supported M R s) : (a : ↥(supported M R s)) → ↥(supported M R s)) l) :
            α →₀ M) :
          (a : α) → M)
        a :
      M)
    (((↑((LinearMap.id : (a : ↥(supported M R s)) → ↥(supported M R s)) l) : α →₀ M) : (a : α) → M) a : M)
Tactic: ext l a
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Supported (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
s : Set α
inst_3 : DecidablePred fun (x : α) ↦ x ∈ s
l : ↥(supported M R s)
a : α
⊢ Eq.{u_2 + 1} (α := M)
    (((↑((restrictDom M R s ∘ₗ Submodule.subtype (supported M R s) : (a : ↥(supported M R s)) → ↥(supported M R s)) l) :
            α →₀ M) :
          (a : α) → M)
        a :
      M)
    (((↑((LinearMap.id : (a : ↥(supported M R s)) → ↥(supported M R s)) l) : α →₀ M) : (a : α) → M) a : M)
have pos : ∀ (h : a ∈ s),
  Eq.{u_2 + 1} (α := M)
    (((↑((restrictDom M R s ∘ₗ Submodule.subtype (supported M R s) : (a : ↥(supported M R s)) → ↥(supported M R s)) l) :
            α →₀ M) :
          (a : α) → M)
        a :
      M)
    (((↑((LinearMap.id : (a : ↥(supported M R s)) → ↥(supported M R s)) l) : α →₀ M) : (a : α) → M) a : M)
Tactic: by_cases h : a ∈ s
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Supported (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
s : Set α
inst_3 : DecidablePred fun (x : α) ↦ x ∈ s
l : ↥(supported M R s)
a : α
pos :
  ∀ (h : a ∈ s),
    Eq.{u_2 + 1} (α := M)
      (((↑((restrictDom M R s ∘ₗ Submodule.subtype (supported M R s) : (a : ↥(supported M R s)) → ↥(supported M R s))
                  l) :
              α →₀ M) :
            (a : α) → M)
          a :
        M)
      (((↑((LinearMap.id : (a : ↥(supported M R s)) → ↥(supported M R s)) l) : α →₀ M) : (a : α) → M) a : M)
⊢ Eq.{u_2 + 1} (α := M)
    (((↑((restrictDom M R s ∘ₗ Submodule.subtype (supported M R s) : (a : ↥(supported M R s)) → ↥(supported M R s)) l) :
            α →₀ M) :
          (a : α) → M)
        a :
      M)
    (((↑((LinearMap.id : (a : ↥(supported M R s)) → ↥(supported M R s)) l) : α →₀ M) : (a : α) → M) a : M)
have neg : ∀ (h : a ∉ s),
  Eq.{u_2 + 1} (α := M)
    (((↑((restrictDom M R s ∘ₗ Submodule.subtype (supported M R s) : (a : ↥(supported M R s)) → ↥(supported M R s)) l) :
            α →₀ M) :
          (a : α) → M)
        a :
      M)
    (((↑((LinearMap.id : (a : ↥(supported M R s)) → ↥(supported M R s)) l) : α →₀ M) : (a : α) → M) a : M)
Tactic: by_cases h : a ∈ s
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Supported (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
l : α →₀ M
h : Membership.mem (γ := Submodule R (α →₀ M)) (supported M R ∅) l
⊢ l = 0
have h₁ : ∀ (a : α), Eq.{u_2 + 1} (α := M) ((l : (a : α) → M) a : M) ((0 : (a : α) → M) a : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Supported (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
δ : Type u_7
s : δ → Set α
⊢ Eq (α := Submodule R (α →₀ M)) (supported M R (⋃ (i : δ), s i)) (⨆ (i : δ), supported M R (s i))
have refine : LE.le (α := Submodule R (α →₀ M)) (supported M R (⋃ (i : δ), s i)) (⨆ (i : δ), supported M R (s i))
Tactic: refine le_antisymm ?_ (iSup_le fun i => supported_mono <| Set.subset_iUnion _ _)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Supported (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
δ : Type u_7
s : δ → Set α
⊢ LE.le (α := Submodule R (α →₀ M)) (supported M R (⋃ (i : δ), s i)) (⨆ (i : δ), supported M R (s i))
have haveI : ∀ (this : DecidablePred fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : δ), s i) x),
  LE.le (α := Submodule R (α →₀ M)) (supported M R (⋃ (i : δ), s i)) (⨆ (i : δ), supported M R (s i))
Tactic: haveI := Classical.decPred fun x => x ∈ ⋃ i, s i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Supported (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
δ : Type u_7
s : δ → Set α
this_1 : DecidablePred fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : δ), s i) x
this :
  LE.le (α := Submodule R (α →₀ M))
    (LinearMap.range (Submodule.subtype (supported M R (⋃ (i : δ), s i)) ∘ₗ restrictDom M R (⋃ (i : δ), s i)))
    (⨆ (i : δ), supported M R (s i))
⊢ LE.le (α := Submodule R (α →₀ M)) (supported M R (⋃ (i : δ), s i)) (⨆ (i : δ), supported M R (s i))
have rwa : ∀
  (this :
    LE.le (α := Submodule R (α →₀ M))
      (map (M := ↥(supported M R (⋃ (i : δ), s i))) (Submodule.subtype (supported M R (⋃ (i : δ), s i)))
        (LinearMap.range (restrictDom M R (⋃ (i : δ), s i))))
      (⨆ (i : δ), supported M R (s i))),
  LE.le (α := Submodule R (α →₀ M)) (supported M R (⋃ (i : δ), s i)) (⨆ (i : δ), supported M R (s i))
Tactic: rwa [LinearMap.range_comp, range_restrictDom, Submodule.map_top, range_subtype] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Supported (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
δ : Type u_7
s : δ → Set α
this_1 : DecidablePred fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : δ), s i) x
this :
  LE.le (α := Submodule R (α →₀ M))
    (LinearMap.range (Submodule.subtype (supported M R (⋃ (i : δ), s i)) ∘ₗ restrictDom M R (⋃ (i : δ), s i)))
    (⨆ (i : δ), supported M R (s i))
rwa :
  ∀
    (this :
      LE.le (α := Submodule R (α →₀ M))
        (map (M := ↥(supported M R (⋃ (i : δ), s i))) (Submodule.subtype (supported M R (⋃ (i : δ), s i)))
          (LinearMap.range (restrictDom M R (⋃ (i : δ), s i))))
        (⨆ (i : δ), supported M R (s i))),
    LE.le (α := Submodule R (α →₀ M)) (supported M R (⋃ (i : δ), s i)) (⨆ (i : δ), supported M R (s i))
⊢ LE.le (α := Submodule R (α →₀ M)) (supported M R (⋃ (i : δ), s i)) (⨆ (i : δ), supported M R (s i))
have rwa₁ : ∀
  (this :
    LE.le (α := Submodule R (α →₀ M))
      (map (M := ↥(supported M R (⋃ (i : δ), s i))) (Submodule.subtype (supported M R (⋃ (i : δ), s i))) ⊤)
      (⨆ (i : δ), supported M R (s i))),
  LE.le (α := Submodule R (α →₀ M)) (supported M R (⋃ (i : δ), s i)) (⨆ (i : δ), supported M R (s i))
Tactic: rwa [LinearMap.range_comp, range_restrictDom, Submodule.map_top, range_subtype] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Supported (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
δ : Type u_7
s : δ → Set α
this_1 : DecidablePred fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : δ), s i) x
this :
  LE.le (α := Submodule R (α →₀ M))
    (LinearMap.range (Submodule.subtype (supported M R (⋃ (i : δ), s i)) ∘ₗ restrictDom M R (⋃ (i : δ), s i)))
    (⨆ (i : δ), supported M R (s i))
rwa :
  ∀
    (this :
      LE.le (α := Submodule R (α →₀ M))
        (map (M := ↥(supported M R (⋃ (i : δ), s i))) (Submodule.subtype (supported M R (⋃ (i : δ), s i)))
          (LinearMap.range (restrictDom M R (⋃ (i : δ), s i))))
        (⨆ (i : δ), supported M R (s i))),
    LE.le (α := Submodule R (α →₀ M)) (supported M R (⋃ (i : δ), s i)) (⨆ (i : δ), supported M R (s i))
rwa₁ :
  ∀
    (this :
      LE.le (α := Submodule R (α →₀ M))
        (map (M := ↥(supported M R (⋃ (i : δ), s i))) (Submodule.subtype (supported M R (⋃ (i : δ), s i))) ⊤)
        (⨆ (i : δ), supported M R (s i))),
    LE.le (α := Submodule R (α →₀ M)) (supported M R (⋃ (i : δ), s i)) (⨆ (i : δ), supported M R (s i))
⊢ LE.le (α := Submodule R (α →₀ M)) (supported M R (⋃ (i : δ), s i)) (⨆ (i : δ), supported M R (s i))
have rwa₂ : ∀
  (this :
    LE.le (α := Submodule R (α →₀ M))
      (LinearMap.range (M := ↥(supported M R (⋃ (i : δ), s i))) (Submodule.subtype (supported M R (⋃ (i : δ), s i))))
      (⨆ (i : δ), supported M R (s i))),
  LE.le (α := Submodule R (α →₀ M)) (supported M R (⋃ (i : δ), s i)) (⨆ (i : δ), supported M R (s i))
Tactic: rwa [LinearMap.range_comp, range_restrictDom, Submodule.map_top, range_subtype] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Supported (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
δ : Type u_7
s : δ → Set α
this_1 : DecidablePred fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : δ), s i) x
this :
  LE.le (α := Submodule R (α →₀ M))
    (LinearMap.range (Submodule.subtype (supported M R (⋃ (i : δ), s i)) ∘ₗ restrictDom M R (⋃ (i : δ), s i)))
    (⨆ (i : δ), supported M R (s i))
rwa :
  ∀
    (this :
      LE.le (α := Submodule R (α →₀ M))
        (map (M := ↥(supported M R (⋃ (i : δ), s i))) (Submodule.subtype (supported M R (⋃ (i : δ), s i)))
          (LinearMap.range (restrictDom M R (⋃ (i : δ), s i))))
        (⨆ (i : δ), supported M R (s i))),
    LE.le (α := Submodule R (α →₀ M)) (supported M R (⋃ (i : δ), s i)) (⨆ (i : δ), supported M R (s i))
rwa₁ :
  ∀
    (this :
      LE.le (α := Submodule R (α →₀ M))
        (map (M := ↥(supported M R (⋃ (i : δ), s i))) (Submodule.subtype (supported M R (⋃ (i : δ), s i))) ⊤)
        (⨆ (i : δ), supported M R (s i))),
    LE.le (α := Submodule R (α →₀ M)) (supported M R (⋃ (i : δ), s i)) (⨆ (i : δ), supported M R (s i))
rwa₂ :
  ∀
    (this :
      LE.le (α := Submodule R (α →₀ M))
        (LinearMap.range (M := ↥(supported M R (⋃ (i : δ), s i))) (Submodule.subtype (supported M R (⋃ (i : δ), s i))))
        (⨆ (i : δ), supported M R (s i))),
    LE.le (α := Submodule R (α →₀ M)) (supported M R (⋃ (i : δ), s i)) (⨆ (i : δ), supported M R (s i))
⊢ LE.le (α := Submodule R (α →₀ M)) (supported M R (⋃ (i : δ), s i)) (⨆ (i : δ), supported M R (s i))
have rwa₃ : ∀ (this : LE.le (α := Submodule R (α →₀ M)) (supported M R (⋃ (i : δ), s i)) (⨆ (i : δ), supported M R (s i))),
  LE.le (α := Submodule R (α →₀ M)) (supported M R (⋃ (i : δ), s i)) (⨆ (i : δ), supported M R (s i))
Tactic: rwa [LinearMap.range_comp, range_restrictDom, Submodule.map_top, range_subtype] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Supported (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
δ : Type u_7
s : δ → Set α
this : DecidablePred fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : δ), s i) x
⊢ LE.le (α := Submodule R (α →₀ M)) (supported M R (⋃ (i : δ), s i)) (⨆ (i : δ), supported M R (s i))
have M₁ : LE.le (α := Submodule R (α →₀ M))
  (LinearMap.range (Submodule.subtype (supported M R (⋃ (i : δ), s i)) ∘ₗ restrictDom M R (⋃ (i : δ), s i)))
  (⨆ (i : δ), supported M R (s i))
Tactic: suffices
    LinearMap.range ((Submodule.subtype _).comp (restrictDom M R (⋃ i, s i))) ≤
      ⨆ i, supported M R (s i) by
    rwa [LinearMap.range_comp, range_restrictDom, Submodule.map_top, range_subtype] at this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Supported (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
δ : Type u_7
s : δ → Set α
this : DecidablePred fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : δ), s i) x
⊢ LE.le (α := Submodule R (α →₀ M))
    (LinearMap.range (Submodule.subtype (supported M R (⋃ (i : δ), s i)) ∘ₗ restrictDom M R (⋃ (i : δ), s i)))
    (⨆ (i : δ), supported M R (s i))
have rw : LE.le (α := Submodule R (α →₀ M)) ⊤
  (comap (Submodule.subtype (supported M R (⋃ (i : δ), s i)) ∘ₗ restrictDom M R (⋃ (i : δ), s i))
    (⨆ (i : δ), supported M R (s i)))
Tactic: rw [range_le_iff_comap, eq_top_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Supported (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
δ : Type u_7
s : δ → Set α
this : DecidablePred fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : δ), s i) x
x : α
a : M
l : α →₀ M
h : x ∉ l.support
h_1 : a ≠ 0
ih :
  Membership.mem (γ := Submodule R (α →₀ M))
    (comap (Submodule.subtype (supported M R (⋃ (i : δ), s i)) ∘ₗ restrictDom M R (⋃ (i : δ), s i))
      (⨆ (i : δ), supported M R (s i)))
    l
⊢ Membership.mem (γ := Submodule R (α →₀ M))
    (comap (Submodule.subtype (supported M R (⋃ (i : δ), s i)) ∘ₗ restrictDom M R (⋃ (i : δ), s i))
      (⨆ (i : δ), supported M R (s i)))
    (single x a + l)
have single_add : Membership.mem (γ := Submodule R (α →₀ M))
  (comap (Submodule.subtype (supported M R (⋃ (i : δ), s i)) ∘ₗ restrictDom M R (⋃ (i : δ), s i))
    (⨆ (i : δ), supported M R (s i)))
  (single x a)
Tactic: refine add_mem ?_ ih
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Supported (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
δ : Type u_7
s : δ → Set α
this : DecidablePred fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : δ), s i) x
x : α
a : M
l : α →₀ M
h : x ∉ l.support
h_1 : a ≠ 0
ih :
  Membership.mem (γ := Submodule R (α →₀ M))
    (comap (Submodule.subtype (supported M R (⋃ (i : δ), s i)) ∘ₗ restrictDom M R (⋃ (i : δ), s i))
      (⨆ (i : δ), supported M R (s i)))
    l
⊢ Membership.mem (γ := Submodule R (α →₀ M))
    (comap (Submodule.subtype (supported M R (⋃ (i : δ), s i)) ∘ₗ restrictDom M R (⋃ (i : δ), s i))
      (⨆ (i : δ), supported M R (s i)))
    (single x a)
have pos : ∀ (h : ∃ (i : δ), x ∈ s i),
  Membership.mem (γ := Submodule R (α →₀ M))
    (comap (Submodule.subtype (supported M R (⋃ (i : δ), s i)) ∘ₗ restrictDom M R (⋃ (i : δ), s i))
      (⨆ (i : δ), supported M R (s i)))
    (single x a)
Tactic: by_cases h : ∃ i, x ∈ s i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Supported (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
δ : Type u_7
s : δ → Set α
this : DecidablePred fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : δ), s i) x
x : α
a : M
l : α →₀ M
h : x ∉ l.support
h_1 : a ≠ 0
ih :
  Membership.mem (γ := Submodule R (α →₀ M))
    (comap (Submodule.subtype (supported M R (⋃ (i : δ), s i)) ∘ₗ restrictDom M R (⋃ (i : δ), s i))
      (⨆ (i : δ), supported M R (s i)))
    l
pos :
  ∀ (h : ∃ (i : δ), x ∈ s i),
    Membership.mem (γ := Submodule R (α →₀ M))
      (comap (Submodule.subtype (supported M R (⋃ (i : δ), s i)) ∘ₗ restrictDom M R (⋃ (i : δ), s i))
        (⨆ (i : δ), supported M R (s i)))
      (single x a)
⊢ Membership.mem (γ := Submodule R (α →₀ M))
    (comap (Submodule.subtype (supported M R (⋃ (i : δ), s i)) ∘ₗ restrictDom M R (⋃ (i : δ), s i))
      (⨆ (i : δ), supported M R (s i)))
    (single x a)
have neg : ∀ (h : ¬∃ (i : δ), x ∈ s i),
  Membership.mem (γ := Submodule R (α →₀ M))
    (comap (Submodule.subtype (supported M R (⋃ (i : δ), s i)) ∘ₗ restrictDom M R (⋃ (i : δ), s i))
      (⨆ (i : δ), supported M R (s i)))
    (single x a)
Tactic: by_cases h : ∃ i, x ∈ s i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Supported (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
δ : Type u_7
s : δ → Set α
this : DecidablePred fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : δ), s i) x
x : α
a : M
l : α →₀ M
h_1 : x ∉ l.support
h_2 : a ≠ 0
ih :
  Membership.mem (γ := Submodule R (α →₀ M))
    (comap (Submodule.subtype (supported M R (⋃ (i : δ), s i)) ∘ₗ restrictDom M R (⋃ (i : δ), s i))
      (⨆ (i : δ), supported M R (s i)))
    l
h : ∃ (i : δ), x ∈ s i
⊢ Membership.mem (γ := Submodule R (α →₀ M))
    (comap (Submodule.subtype (supported M R (⋃ (i : δ), s i)) ∘ₗ restrictDom M R (⋃ (i : δ), s i))
      (⨆ (i : δ), supported M R (s i)))
    (single x a)
have pos : Membership.mem (γ := Submodule R (α →₀ M)) (⨆ (i : δ), supported M R (s i)) (single x a)
Tactic: simp only [mem_comap, coe_comp, coe_subtype, Function.comp_apply, restrictDom_apply,
        mem_iUnion, h, filter_single_of_pos]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Supported (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
δ : Type u_7
s : δ → Set α
this : DecidablePred fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : δ), s i) x
x : α
a : M
l : α →₀ M
h_1 : x ∉ l.support
h_2 : a ≠ 0
ih :
  Membership.mem (γ := Submodule R (α →₀ M))
    (comap (Submodule.subtype (supported M R (⋃ (i : δ), s i)) ∘ₗ restrictDom M R (⋃ (i : δ), s i))
      (⨆ (i : δ), supported M R (s i)))
    l
h : ∃ (i : δ), x ∈ s i
⊢ Membership.mem (γ := Submodule R (α →₀ M)) (⨆ (i : δ), supported M R (s i)) (single x a)
have pos : ∀ (i : δ) (hi : x ∈ s i), Membership.mem (γ := Submodule R (α →₀ M)) (⨆ (i : δ), supported M R (s i)) (single x a)
Tactic: obtain ⟨i, hi⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Supported (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
δ : Type u_7
s : δ → Set α
this : DecidablePred fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : δ), s i) x
l : α →₀ M
⊢ Membership.mem (γ := Submodule R (α →₀ M))
    (comap (Submodule.subtype (supported M R (⋃ (i : δ), s i)) ∘ₗ restrictDom M R (⋃ (i : δ), s i))
      (⨆ (i : δ), supported M R (s i)))
    l
have zero : Membership.mem (γ := Submodule R (α →₀ M))
  (comap (Submodule.subtype (supported M R (⋃ (i : δ), s i)) ∘ₗ restrictDom M R (⋃ (i : δ), s i))
    (⨆ (i : δ), supported M R (s i)))
  0
Tactic: induction l using Finsupp.induction with
  | zero => exact zero_mem _
  | single_add x a l _ _ ih =>
    refine add_mem ?_ ih
    by_cases h : ∃ i, x ∈ s i
    · simp only [mem_comap, coe_comp, coe_subtype, Function.comp_apply, restrictDom_apply,
        mem_iUnion, h, filter_single_of_pos]
      obtain ⟨i, hi⟩ := h
      exact le_iSup (fun i => supported M R (s i)) i (single_mem_supported R _ hi)
    · simp [h]
Cleared hypotheses: l