awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Finsupp.Span
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
⊢ Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) m ↔
    ∃ (s : Finset ι), Membership.mem (γ := Submodule R M) (⨆ i ∈ s, p i) m

Tactic:
⟨Submodule.exists_finset_of_mem_iSup p, fun ⟨_, hs⟩ =>
    iSup_mono (fun i => (iSup_const_le : _ ≤ p i)) hs⟩

Premises used: Submodule.exists_finset_of_mem_iSup, iSup, _private.0.Submodule.mem_iSup_iff_exists_finset.match_1, Membership.mem, Iff.intro, iSup_const_le, iSup_mono
-- Module: Mathlib.LinearAlgebra.Finsupp.Span
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
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
⊢ m ∈ sSup S ↔
    ∃ (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]

Premises used: iSup_subtype', sSup_eq_iSup, Submodule.mem_iSup_iff_exists_finset
-- Module: Mathlib.LinearAlgebra.Finsupp.Span
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

Tactic:
⟨fun ⟨s, hs⟩ ↦ ⟨s.map (Function.Embedding.subtype (· ∈ S)), ?_, ?_⟩,
          fun ⟨s, hsS, hs⟩ ↦ ⟨s.preimage (↑) Subtype.coe_injective.injOn, ?_⟩⟩

Premises used: _private.0.Submodule.mem_sSup_iff_exists_finset.match_1, iSup, Function.Injective.injOn, Finset.map, Membership.mem, Exists, HasSubset.Subset, Subtype.coe_injective, And, SetLike.coe, Finset.preimage, And.intro, Iff.intro, Exists.intro, Function.Embedding.subtype, Subtype.val, _private.0.Submodule.mem_sSup_iff_exists_finset.match_2
-- Module: Mathlib.LinearAlgebra.Finsupp.Span
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
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)) ⋯) i),
            (↑i : Submodule R 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

Tactic:
refine ⟨fun ⟨s, hs⟩ ↦ ⟨s.map (Function.Embedding.subtype (· ∈ S)), ?_, ?_⟩,
          fun ⟨s, hsS, hs⟩ ↦ ⟨s.preimage (↑) Subtype.coe_injective.injOn, ?_⟩⟩
-- Module: Mathlib.LinearAlgebra.Finsupp.Span
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
⊢ (↑(Finset.map (Function.Embedding.subtype fun (x : Submodule R M) ↦ x ∈ S) s) : Set (Submodule R M)) ⊆ S

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Finsupp.Span
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
this :
  Membership.mem (γ := Submodule R M)
    (⨆ (i : Submodule R M), ⨆ (hi : i ∈ S), ⨆ (_ : Subtype.mk (p := Membership.mem S) i hi ∈ s), i) m
⊢ Membership.mem (γ := Submodule R M)
    (⨆ i ∈ Finset.map (Function.Embedding.subtype fun (x : Submodule R M) ↦ x ∈ S) s, i) m

Tactic:
simpa
-- Module: Mathlib.LinearAlgebra.Finsupp.Span
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
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
⊢ Membership.mem (γ := Submodule R M)
    (⨆ i ∈ Finset.map (Function.Embedding.subtype fun (x : Submodule R M) ↦ x ∈ S) s, i) m

Tactic:
suffices m ∈ ⨆ (i) (hi : i ∈ S) (_ : ⟨i, hi⟩ ∈ s), i by simpa
-- Module: Mathlib.LinearAlgebra.Finsupp.Span
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
refine_2 refine_2₁ refine_2₂ refine_2₃ :
  Membership.mem (γ := Submodule R M)
    (⨆ (x : Subtype (Membership.mem S)),
      ⨆ (_ : Subtype.mk (p := Membership.mem S) (↑x : Submodule R M) ⋯ ∈ s), (↑x : Submodule R M))
    m
⊢ Membership.mem (γ := Submodule R M)
    (⨆ (i : Submodule R M), ⨆ (hi : i ∈ S), ⨆ (_ : Subtype.mk (p := Membership.mem S) i hi ∈ s), i) m

Tactic:
rwa [iSup_subtype']

Premises used: iSup_subtype'
-- Module: Mathlib.LinearAlgebra.Finsupp.Span
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 : Submodule R M), ⨆ (_ : i ∈ S ∧ i ∈ s), i)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Finsupp.Span
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_1 :
  ∃ (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
h : ∀ (x : Submodule R M), x ∈ s ↔ x ∈ S ∧ x ∈ s
⊢ Eq.{u_2 + 1} (α := Submodule R M) (⨆ (i : Submodule R M), ⨆ (_ : i ∈ S ∧ i ∈ s), i) (⨆ i ∈ s, i)

Tactic:
convert! rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Finsupp.Span
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
x : Submodule R M
⊢ x ∈ s ↔ x ∈ S ∧ x ∈ s

Tactic:
grind
-- Module: Mathlib.LinearAlgebra.Finsupp.Span
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)

Tactic:
have : ⨆ (i) (_ : i ∈ S ∧ i ∈ s), i = ⨆ (i) (_ : i ∈ s), i := by convert! rfl; grind
-- Module: Mathlib.LinearAlgebra.Finsupp.Span
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
this : Eq.{u_2 + 1} (α := Submodule R M) (⨆ (i : Submodule R M), ⨆ (_ : i ∈ S ∧ i ∈ s), i) (⨆ i ∈ s, i)
⊢ 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

Tactic:
simpa only [Finset.mem_preimage, iSup_subtype, iSup_and', this]

Premises used: iSup_and', iSup_subtype, Finset.mem_preimage
-- Module: Mathlib.LinearAlgebra.Finsupp.Span
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
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)))
⊢ 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

Tactic:
simp_rw [range_eq_map, ← span_single_eq_top, ← span_univ, map_span, set_smul_span]

Premises used: Submodule.set_smul_span, Finsupp.span_single_eq_top, Submodule.span_univ, LinearMap.range_eq_map, Submodule.map_span
-- Module: Mathlib.LinearAlgebra.Finsupp.Span
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
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)
⊢ 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:
congr 1
-- Module: Mathlib.LinearAlgebra.Finsupp.Span
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
⊢ 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:
aesop (add simp Set.mem_smul)

Premises used: Set.mem_smul
-- Module: Mathlib.LinearAlgebra.Finsupp.Span
Goal:
R : Type u_1
M : Type u_2
σ : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set σ
f : σ → R
⊢ HSMul.hSMul (β := Submodule R M) (f '' s) ⊤ =
    LinearMap.range (R := R) (M := Finsupp.{u_4, u_2} (↑s : Type u_4) M) (τ₁₂ := RingHom.id R)
      ((lsum R : (a : (↑s : Type u_4) → M →ₗ[R] M) → ((↑s : Type u_4) →₀ M) →ₗ[R] M) fun (i : (↑s : Type u_4)) ↦
        HSMul.hSMul (β := M →ₗ[R] M) (f (↑i : σ)) LinearMap.id)

Tactic:
simpa [Set.range_comp] using (range_lsum_smul (.id (R := R) (M := M)) (f ∘ (↑) : s → R)).symm

Premises used: LinearMap.id, Set.range_comp, Function.comp, Submodule.range_lsum_smul, Eq.symm, Subtype.val
-- Module: Mathlib.LinearAlgebra.Finsupp.Span
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set R
⊢ HSMul.hSMul (β := Submodule R M) s ⊤ =
    LinearMap.range (R := R) (M := Finsupp.{u_1, u_2} (↑s : Type u_1) M) (τ₁₂ := RingHom.id R)
      ((lsum R : (a : (↑s : Type u_1) → M →ₗ[R] M) → ((↑s : Type u_1) →₀ M) →ₗ[R] M) fun (i : (↑s : Type u_1)) ↦
        HSMul.hSMul (β := M →ₗ[R] M) (↑i : R) LinearMap.id)

Tactic:
simpa using image_smul_top_eq_range_lsum (M := M) s id

Premises used: id, Submodule.image_smul_top_eq_range_lsum
-- Module: Mathlib.LinearAlgebra.Finsupp.SumProd
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)
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)
⊢ Equiv.toFun (AddEquiv.toEquiv sumFinsuppAddEquivProdFinsupp) (m • x) =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) m : R)
      (Equiv.toFun (AddEquiv.toEquiv sumFinsuppAddEquivProdFinsupp) x)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Finsupp.SumProd
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
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:
simp only [AddEquiv.toFun_eq_coe, Prod.smul_fst, Prod.smul_snd, smul_apply,
          snd_sumFinsuppAddEquivProdFinsupp, fst_sumFinsuppAddEquivProdFinsupp,
          RingHom.id_apply]

Premises used: RingHom.id_apply, Finsupp.snd_sumFinsuppAddEquivProdFinsupp, Finsupp.smul_apply, Finsupp.fst_sumFinsuppAddEquivProdFinsupp, Prod.smul_snd, AddEquiv.toFun_eq_coe, Prod.smul_fst
-- Module: Mathlib.LinearAlgebra.Finsupp.SumProd
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
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:
simp only [AddEquiv.toFun_eq_coe, Prod.smul_fst, Prod.smul_snd, smul_apply,
          snd_sumFinsuppAddEquivProdFinsupp, fst_sumFinsuppAddEquivProdFinsupp,
          RingHom.id_apply]

Premises used: RingHom.id_apply, Finsupp.snd_sumFinsuppAddEquivProdFinsupp, Finsupp.smul_apply, Finsupp.fst_sumFinsuppAddEquivProdFinsupp, Prod.smul_snd, AddEquiv.toFun_eq_coe, Prod.smul_fst
-- Module: Mathlib.LinearAlgebra.Finsupp.SumProd
Goal:
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
α : Type u_7
β : Type u_8
f : α ⊕ β →₀ M
x : α
⊢ Eq.{u_2 + 1} (α := M)
    ((((sumFinsuppLEquivProdFinsupp R : (a : α ⊕ β →₀ M) → (α →₀ M) × (β →₀ M)) f).1 : (a : α) → M) x : M)
    ((f : (a : α ⊕ β) → M) (Sum.inl x) : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Finsupp.SumProd
Goal:
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
α : Type u_7
β : Type u_8
f : α ⊕ β →₀ M
y : β
⊢ Eq.{u_2 + 1} (α := M)
    ((((sumFinsuppLEquivProdFinsupp R : (a : α ⊕ β →₀ M) → (α →₀ M) × (β →₀ M)) f).2 : (a : β) → M) y : M)
    ((f : (a : α ⊕ β) → M) (Sum.inr y) : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Finsupp.SumProd
Goal:
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
α : Type u_7
β : Type u_8
fg : (α →₀ M) × (β →₀ M)
x : α
⊢ Eq.{u_2 + 1} (α := M)
    ((((LinearEquiv.symm (sumFinsuppLEquivProdFinsupp R) : (a : (α →₀ M) × (β →₀ M)) → α ⊕ β →₀ M) fg : α ⊕ β →₀ M) :
          (a : α ⊕ β) → M)
        (Sum.inl x) :
      M)
    ((fg.1 : (a : α) → M) x : M)

Tactic:
rfl

Premises used: rfl, Sum.elim
-- Module: Mathlib.LinearAlgebra.Finsupp.SumProd
Goal:
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
α : Type u_7
β : Type u_8
fg : (α →₀ M) × (β →₀ M)
y : β
⊢ Eq.{u_2 + 1} (α := M)
    ((((LinearEquiv.symm (sumFinsuppLEquivProdFinsupp R) : (a : (α →₀ M) × (β →₀ M)) → α ⊕ β →₀ M) fg : α ⊕ β →₀ M) :
          (a : α ⊕ β) → M)
        (Sum.inr y) :
      M)
    ((fg.2 : (a : β) → M) y : M)

Tactic:
rfl

Premises used: rfl, Sum.elim
-- Module: Mathlib.LinearAlgebra.Finsupp.SumProd
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
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)
⊢ 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)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Finsupp.SumProd
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
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:
simp
-- Module: Mathlib.LinearAlgebra.Finsupp.SumProd
Goal:
R : Type u_5
inst : Semiring R
η : Type u_7
inst_1 : Fintype η
M : Type u_9
ιs : η → Type u_10
inst_2 : AddCommMonoid M
inst_3 : Module R M
f : (j : η) × ιs j →₀ M
j : η
i : ιs j
⊢ Eq.{u_9 + 1} (α := M)
    ((((sigmaFinsuppLEquivPiFinsupp R (ιs := ιs) : (a : (j : η) × ιs j →₀ M) → (j : η) → ιs j →₀ M) f j :
            Finsupp.{u_10, u_9} (ιs j) M) :
          (a : ιs j) → M)
        i :
      M)
    ((f : (a : (j : η) × ιs j) → M) (Sigma.mk (β := fun (j : η) ↦ ιs j) j i) : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Finsupp.SumProd
Goal:
R : Type u_5
inst : Semiring R
η : Type u_7
inst_1 : Fintype η
M : Type u_9
ιs : η → Type u_10
inst_2 : AddCommMonoid M
inst_3 : Module R M
f : (j : η) → Finsupp.{u_10, u_9} (ιs j) M
ji : (j : η) × ιs j
⊢ Eq.{u_9 + 1} (α := M)
    ((((LinearEquiv.symm (sigmaFinsuppLEquivPiFinsupp R (ιs := ιs)) : (a : (j : η) → ιs j →₀ M) → (j : η) × ιs j →₀ M)
              f :
            (j : η) × ιs j →₀ M) :
          (a : (j : η) × ιs j) → M)
        ji :
      M)
    ((f (ji.fst (β := fun (j : η) ↦ ιs j)) : (a : ιs ji.fst) → M) (ji.snd (β := fun (j : η) ↦ ιs j)) : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
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)

Tactic:
Subset.trans (Subset.trans (Finset.coe_subset.2 support_add) ?_) (union_subset hp hq)

Premises used: Iff.mpr, Set.Mem, Set.Subset.trans, setOf, Set.union_subset, Finsupp.support_add, Finset.coe_subset
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
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
refine : (↑(p.support ∪ q.support) : Set α) ⊆ (↑p.support : Set α) ∪ (↑q.support : Set α)
⊢ Membership.mem (γ := Set (α →₀ M)) {p : α →₀ M | (↑p.support : Set α) ⊆ s} (p + q)

Tactic:
refine Subset.trans (Subset.trans (Finset.coe_subset.2 support_add) ?_) (union_subset hp hq)

Premises used: Iff.mpr, Set.Subset.trans, Set.union_subset, Finsupp.support_add, Finset.coe_subset