awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
Goal:
R : Type u
ι : Type x
inst : Semiring R
φ : ι → Type i
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, i} R (φ i)
inst_3 : DecidableEq ι
I J : Set ι
h : Disjoint I J
i : ι
hi : i ∈ I
b : φ i
j : ι
hj : j ∈ J
⊢ Eq (α := φ j) ((proj (φ := φ) j ∘ₗ single R φ i : (a : φ i) → φ j) b : φ j) (0 : φ j)
have rw : j ≠ i
Tactic: rw [proj_comp_single_ne R φ j i, zero_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (hypothesis)
Goal:
R : Type u
ι : Type x
inst : Semiring R
φ : ι → Type i
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, i} R (φ i)
inst_3 : DecidableEq ι
I : Finset ι
J : Set ι
hu : Set.univ ⊆ (↑I : Set ι) ∪ J
b : (i : ι) → φ i
hb : Membership.mem (γ := Submodule R ((i : ι) → φ i)) (⨅ i ∈ J, ker (proj (φ := φ) i)) b
⊢ Membership.mem (γ := Submodule R ((i : ι) → φ i)) (⨆ i ∈ I, range (single R φ i)) b
have hb₁ : ∀ (i : ι) (i_1 : i ∈ J), b i = 0
Tactic: simp only [mem_iInf, mem_ker, proj_apply] at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
Goal:
R : Type u
ι : Type x
inst : Semiring R
φ : ι → Type i
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, i} R (φ i)
inst_3 : DecidableEq ι
I : Finset ι
J : Set ι
hu : Set.univ ⊆ (↑I : Set ι) ∪ J
b : (i : ι) → φ i
hb : ∀ (i : ι) (i_1 : i ∈ J), b i = 0
⊢ ∑ i ∈ I, Pi.single (M := φ) i (b i) = b
have h : ∀ (i : ι), (∑ i ∈ I, Pi.single (M := φ) i (b i)) i = b i
Tactic: ext i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
Goal:
R : Type u
ι : Type x
inst : Semiring R
φ : ι → Type i
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, i} R (φ i)
inst_3 : DecidableEq ι
I : Finset ι
J : Set ι
hu : Set.univ ⊆ (↑I : Set ι) ∪ J
b : (i : ι) → φ i
hb : ∀ (i : ι) (i_1 : i ∈ J), b i = 0
i : ι
⊢ (∑ i ∈ I, Pi.single (M := φ) i (b i)) i = b i
have h : ∑ c ∈ I, Pi.single (M := φ) c (b c) i = Pi.single (M := φ) i (b i) i
Tactic: rw [Finset.sum_apply, ← Pi.single_eq_same i (b i)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
Goal:
R : Type u
ι : Type x
inst : Semiring R
φ : ι → Type i
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, i} R (φ i)
inst_3 : DecidableEq ι
I : Finset ι
J : Set ι
hu : Set.univ ⊆ (↑I : Set ι) ∪ J
b : (i : ι) → φ i
hb : ∀ (i : ι) (i_1 : i ∈ J), b i = 0
i : ι
⊢ ∑ c ∈ I, Pi.single (M := φ) c (b c) i = Pi.single (M := φ) i (b i) i
have h : i ∉ I → Pi.single (M := φ) i (b i) i = 0
Tactic: refine Finset.sum_eq_single i (fun j _ ne => Pi.single_eq_of_ne ne.symm _) ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
Goal:
R : Type u
ι : Type x
inst : Semiring R
φ : ι → Type i
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, i} R (φ i)
inst_3 : DecidableEq ι
I : Finset ι
J : Set ι
hu : Set.univ ⊆ (↑I : Set ι) ∪ J
b : (i : ι) → φ i
hb : ∀ (i : ι) (i_1 : i ∈ J), b i = 0
i : ι
hiI : i ∉ I
⊢ Pi.single (M := φ) i (b i) i = 0
have h : b i = 0
Tactic: rw [Pi.single_eq_same]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
Goal:
R : Type u
ι : Type x
inst : Semiring R
φ : ι → Type i
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, i} R (φ i)
inst_3 : DecidableEq ι
I : Finset ι
J : Set ι
hu : Set.univ ⊆ (↑I : Set ι) ∪ J
b : (i : ι) → φ i
hb : ∀ (i : ι) (i_1 : i ∈ J), b i = 0
⊢ Membership.mem (γ := Submodule R ((i : ι) → φ i)) (⨆ i ∈ I, range (single R φ i)) b
have rw : Membership.mem (γ := Submodule R ((i : ι) → φ i)) (⨆ i ∈ I, range (single R φ i)) (∑ i ∈ I, Pi.single (M := φ) i (b i))
Tactic: rw [←
        show (∑ i ∈ I, Pi.single i (b i)) = b by
          ext i
          rw [Finset.sum_apply, ← Pi.single_eq_same i (b i)]
          refine Finset.sum_eq_single i (fun j _ ne => Pi.single_eq_of_ne ne.symm _) ?_
          intro hiI
          rw [Pi.single_eq_same]
          exact hb _ ((hu trivial).resolve_left hiI)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
Goal:
R : Type u
ι : Type x
inst : Semiring R
φ : ι → Type i
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, i} R (φ i)
inst_3 : DecidableEq ι
I J : Set ι
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
hI : I.Finite
⊢ Eq (α := Submodule R ((i : ι) → φ i)) (⨆ i ∈ I, range (single R φ i)) (⨅ i ∈ J, ker (proj (φ := φ) i))
have refine : LE.le (α := Submodule R ((i : ι) → φ i)) (⨅ i ∈ J, ker (proj (φ := φ) i)) (⨆ i ∈ I, range (single R φ i))
Tactic: refine le_antisymm (iSup_range_single_le_iInf_ker_proj _ _ _ _ hd) ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (hypothesis)
Goal:
R : Type u
ι : Type x
inst : Semiring R
φ : ι → Type i
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, i} R (φ i)
inst_3 : DecidableEq ι
I J : Set ι
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
hI : I.Finite
⊢ LE.le (α := Submodule R ((i : ι) → φ i)) (⨅ i ∈ J, ker (proj (φ := φ) i)) (⨆ i ∈ I, range (single R φ i))
have this : Set.univ ⊆ (↑(hI.toFinset (s := I)) : Set ι) ∪ J
Tactic: have : Set.univ ⊆ ↑hI.toFinset ∪ J := by rwa [hI.coe_toFinset]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
Goal:
R : Type u
ι : Type x
inst : Semiring R
φ : ι → Type i
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, i} R (φ i)
inst_3 : DecidableEq ι
I J : Set ι
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
hI : I.Finite
this : Set.univ ⊆ (↑(hI.toFinset (s := I)) : Set ι) ∪ J
⊢ LE.le (α := Submodule R ((i : ι) → φ i)) (⨅ i ∈ J, ker (proj (φ := φ) i)) (⨆ i ∈ I, range (single R φ i))
have refine : ∀ (i : ι),
  LE.le (α := Submodule R ((i : ι) → φ i)) (⨆ (_ : i ∈ hI.toFinset (s := I)), range (single R φ i))
    (⨆ (_ : i ∈ I), range (single R φ i))
Tactic: refine le_trans (iInf_ker_proj_le_iSup_range_single R φ this) (iSup_mono fun i => ?_)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
Goal:
R : Type u
ι : Type x
inst : Semiring R
φ : ι → Type i
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, i} R (φ i)
inst_3 : DecidableEq ι
I J : Set ι
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
hI : I.Finite
this : Set.univ ⊆ (↑(hI.toFinset (s := I)) : Set ι) ∪ J
i : ι
⊢ LE.le (α := Submodule R ((i : ι) → φ i)) (⨆ (_ : i ∈ hI.toFinset (s := I)), range (single R φ i))
    (⨆ (_ : i ∈ I), range (single R φ i))
have rw : LE.le (α := Submodule R ((i : ι) → φ i)) (⨆ (_ : i ∈ I), range (single R φ i)) (⨆ (_ : i ∈ I), range (single R φ i))
Tactic: rw [Set.Finite.mem_toFinset]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
Goal:
R : Type u
ι : Type x
inst : Semiring R
φ : ι → Type i
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, i} R (φ i)
inst_3 : DecidableEq ι
inst_4 : Finite ι
⊢ Eq (α := Submodule R ((i : ι) → φ i)) (⨆ (i : ι), range (single R φ i)) ⊤
have intro : ∀ (val : Fintype ι), Eq (α := Submodule R ((i : ι) → φ i)) (⨆ (i : ι), range (single R φ i)) ⊤
Tactic: cases nonempty_fintype ι
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
Goal:
R : Type u
ι : Type x
inst : Semiring R
φ : ι → Type i
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, i} R (φ i)
inst_3 : DecidableEq ι
inst_4 : Finite ι
val : Fintype ι
⊢ Eq (α := Submodule R ((i : ι) → φ i)) (⨆ (i : ι), range (single R φ i)) ⊤
have h : ∀ (x : ι),
  Eq (α := Submodule R ((i : ι) → φ i)) (range (single R φ x))
    (⨆ (_ : Membership.mem (γ := Finset ι) Finset.univ x), range (single R φ x))
Tactic: convert! top_unique (iInf_emptyset.ge.trans <| iInf_ker_proj_le_iSup_range_single R φ _)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
Goal:
R : Type u
ι : Type x
inst : Semiring R
φ : ι → Type i
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, i} R (φ i)
inst_3 : DecidableEq ι
inst_4 : Finite ι
val : Fintype ι
h :
  ∀ (x : ι),
    Eq (α := Submodule R ((i : ι) → φ i)) (range (single R φ x))
      (⨆ (_ : Membership.mem (γ := Finset ι) Finset.univ x), range (single R φ x))
⊢ Eq (α := Submodule R ((i : ι) → φ i)) (⨆ (i : ι), range (single R φ i)) ⊤
have intro : Finset ι
Tactic: convert! top_unique (iInf_emptyset.ge.trans <| iInf_ker_proj_le_iSup_range_single R φ _)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
Goal:
R : Type u
ι : Type x
inst : Semiring R
φ : ι → Type i
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, i} R (φ i)
inst_3 : DecidableEq ι
inst_4 : Finite ι
val : Fintype ι
h :
  ∀ (x : ι),
    Eq (α := Submodule R ((i : ι) → φ i)) (range (single R φ x))
      (⨆ (_ : Membership.mem (γ := Finset ι) Finset.univ x), range (single R φ x))
intro : Finset ι
⊢ Eq (α := Submodule R ((i : ι) → φ i)) (⨆ (i : ι), range (single R φ i)) ⊤
have intro₁ : Set.univ ⊆ (↑Finset.univ : Set ι) ∪ ∅
Tactic: convert! top_unique (iInf_emptyset.ge.trans <| iInf_ker_proj_le_iSup_range_single R φ _)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
Goal:
R : Type u
ι : Type x
inst : Semiring R
φ : ι → Type i
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, i} R (φ i)
inst_3 : DecidableEq ι
inst_4 : Finite ι
val : Fintype ι
⊢ Set.univ ⊆ (↑Finset.univ : Set ι) ∪ ∅
have intro : Subset.{x} (α := Set ι) Set.univ (Set.univ ∪ ∅)
Tactic: rw [Finset.coe_univ, Set.union_empty]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
Goal:
R : Type u
ι : Type x
inst : Semiring R
φ : ι → Type i
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, i} R (φ i)
inst_3 : DecidableEq ι
inst_4 : Finite ι
val : Fintype ι
intro : Subset.{x} (α := Set ι) Set.univ (Set.univ ∪ ∅)
⊢ Set.univ ⊆ (↑Finset.univ : Set ι) ∪ ∅
have intro₁ : Subset.{x} (α := Set ι) Set.univ Set.univ
Tactic: rw [Finset.coe_univ, Set.union_empty]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
Goal:
R : Type u
ι : Type x
inst : Semiring R
φ : ι → Type i
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, i} R (φ i)
inst_3 : DecidableEq ι
I J : Set ι
h : Disjoint I J
⊢ Disjoint (α := Submodule R ((i : ι) → φ i)) (⨆ i ∈ I, range (single R φ i)) (⨆ i ∈ J, range (single R φ i))
have _ : Disjoint (α := Submodule R ((i : ι) → φ i)) (⨅ i ∈ Iᶜ, ker (proj (φ := φ) i)) (⨅ i ∈ Jᶜ, ker (proj (φ := φ) i))
Tactic: refine
    Disjoint.mono (iSup_range_single_le_iInf_ker_proj _ _ _ _ <| disjoint_compl_right)
      (iSup_range_single_le_iInf_ker_proj _ _ _ _ <| disjoint_compl_right) ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
Goal:
R : Type u
ι : Type x
inst : Semiring R
φ : ι → Type i
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, i} R (φ i)
inst_3 : DecidableEq ι
I J : Set ι
h : Disjoint I J
⊢ Disjoint (α := Submodule R ((i : ι) → φ i)) (⨅ i ∈ Iᶜ, ker (proj (φ := φ) i)) (⨅ i ∈ Jᶜ, ker (proj (φ := φ) i))
have simp : ∀ ⦃x : (i : ι) → φ i⦄,
  ((∀ (i : ι) (i_1 : i ∈ Iᶜ), x i = 0) ∧ ∀ (i : ι) (i_1 : i ∈ Jᶜ), x i = 0) → ∀ (x_1 : ι), x x_1 = 0 x_1
Tactic: simp only [disjoint_iff_inf_le, SetLike.le_def, mem_iInf, mem_inf, mem_ker, mem_bot, proj_apply,
    funext_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
Goal:
R : Type u
ι : Type x
inst : Semiring R
φ : ι → Type i
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, i} R (φ i)
inst_3 : DecidableEq ι
I J : Set ι
h : Disjoint I J
b : (i : ι) → φ i
hI : ∀ (i : ι) (i_1 : i ∈ Iᶜ), b i = 0
hJ : ∀ (i : ι) (i_1 : i ∈ Jᶜ), b i = 0
i : ι
⊢ b i = 0 i
have pos : ∀ (hiI : i ∈ I), b i = 0 i
Tactic: by_cases hiI : i ∈ I
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
Goal:
R : Type u
ι : Type x
inst : Semiring R
φ : ι → Type i
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, i} R (φ i)
inst_3 : DecidableEq ι
I J : Set ι
h : Disjoint I J
b : (i : ι) → φ i
hI : ∀ (i : ι) (i_1 : i ∈ Iᶜ), b i = 0
hJ : ∀ (i : ι) (i_1 : i ∈ Jᶜ), b i = 0
i : ι
pos : ∀ (hiI : i ∈ I), b i = 0 i
⊢ b i = 0 i
have neg : ∀ (hiI : i ∉ I), b i = 0 i
Tactic: by_cases hiI : i ∈ I
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
Goal:
R : Type u
ι : Type x
inst : Semiring R
φ : ι → Type i
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, i} R (φ i)
inst_3 : DecidableEq ι
I J : Set ι
h : Disjoint I J
b : (i : ι) → φ i
hI : ∀ (i : ι) (i_1 : i ∈ Iᶜ), b i = 0
hJ : ∀ (i : ι) (i_1 : i ∈ Jᶜ), b i = 0
i : ι
hiI : i ∈ I
⊢ b i = 0 i
have pos : ∀ (hiJ : i ∈ J), b i = 0 i
Tactic: by_cases hiJ : i ∈ J
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
Goal:
R : Type u
ι : Type x
inst : Semiring R
φ : ι → Type i
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, i} R (φ i)
inst_3 : DecidableEq ι
I J : Set ι
h : Disjoint I J
b : (i : ι) → φ i
hI : ∀ (i : ι) (i_1 : i ∈ Iᶜ), b i = 0
hJ : ∀ (i : ι) (i_1 : i ∈ Jᶜ), b i = 0
i : ι
hiI : i ∈ I
pos : ∀ (hiJ : i ∈ J), b i = 0 i
⊢ b i = 0 i
have neg : ∀ (hiJ : i ∉ J), b i = 0 i
Tactic: by_cases hiJ : i ∈ J
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
Goal:
R : Type u
ι : Type x
inst : Semiring R
φ : ι → Type i
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, i} R (φ i)
inst_3 : DecidableEq ι
I J : Set ι
h : Disjoint I J
b : (i : ι) → φ i
hI : ∀ (i : ι) (i_1 : i ∈ Iᶜ), b i = 0
hJ : ∀ (i : ι) (i_1 : i ∈ Jᶜ), b i = 0
i : ι
⊢ b i = 0 i
have pos : ∀ (hiI : i ∈ I), b i = 0 i
Tactic: classical
    by_cases hiI : i ∈ I
    · by_cases hiJ : i ∈ J
      · exact (h.le_bot ⟨hiI, hiJ⟩).elim
      · exact hJ i hiJ
    · exact hI i hiI
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
Goal:
R : Type u
ι : Type x
inst : Semiring R
φ : ι → Type i
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, i} R (φ i)
inst_3 : DecidableEq ι
I J : Set ι
h : Disjoint I J
b : (i : ι) → φ i
hI : ∀ (i : ι) (i_1 : i ∈ Iᶜ), b i = 0
hJ : ∀ (i : ι) (i_1 : i ∈ Jᶜ), b i = 0
i : ι
pos : ∀ (hiI : i ∈ I), b i = 0 i
⊢ b i = 0 i
have neg : ∀ (hiI : i ∉ I), b i = 0 i
Tactic: classical
    by_cases hiI : i ∈ I
    · by_cases hiJ : i ∈ J
      · exact (h.le_bot ⟨hiI, hiJ⟩).elim
      · exact hJ i hiJ
    · exact hI i hiI
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
Goal:
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst : Semiring R
inst_1 : AddCommMonoid M₂
inst_2 : Module R M₂
inst_3 : AddCommMonoid M₃
inst_4 : Module R M₃
φ : ι → Type i
inst_5 : (i : ι) → AddCommMonoid (φ i)
inst_6 : (i : ι) → Module.{u, i} R (φ i)
inst_7 : DecidableEq ι
S : Type u_1
inst_8 : AddCommMonoid M
inst_9 : Module R M
inst_10 : Fintype ι
inst_11 : Semiring S
inst_12 : Module S M
inst_13 : SMulCommClass R S M
f : (i : ι) → LinearMap.{u, u, i, v} (RingHom.id R) (φ i) M
⊢ (fun (f : ((i : ι) → φ i) →ₗ[R] M) (i : ι) ↦ f ∘ₗ single R φ i)
      ((fun (f : (i : ι) → LinearMap.{u, u, i, v} (RingHom.id R) (φ i) M) ↦
          (∑ i : ι, f i ∘ₗ proj (φ := φ) i : ((i : ι) → φ i) →ₗ[R] M))
        f) =
    f
have h : ∀ (i : ι) (x : φ i),
  Eq.{v + 1} (α := M)
    (((fun (f : ((i : ι) → φ i) →ₗ[R] M) (i : ι) ↦ f ∘ₗ single R φ i)
            ((fun (f : (i : ι) → LinearMap.{u, u, i, v} (RingHom.id R) (φ i) M) ↦
                (∑ i : ι, f i ∘ₗ proj (φ := φ) i : ((i : ι) → φ i) →ₗ[R] M))
              f)
            i :
          (a : φ i) → M)
        x :
      M)
    ((f i : (a : φ i) → M) x : M)
Tactic: ext i x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
Goal:
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst : Semiring R
inst_1 : AddCommMonoid M₂
inst_2 : Module R M₂
inst_3 : AddCommMonoid M₃
inst_4 : Module R M₃
φ : ι → Type i
inst_5 : (i : ι) → AddCommMonoid (φ i)
inst_6 : (i : ι) → Module.{u, i} R (φ i)
inst_7 : DecidableEq ι
S : Type u_1
inst_8 : AddCommMonoid M
inst_9 : Module R M
inst_10 : Fintype ι
inst_11 : Semiring S
inst_12 : Module S M
inst_13 : SMulCommClass R S M
f : ((i : ι) → φ i) →ₗ[R] M
⊢ (fun (f : (i : ι) → LinearMap.{u, u, i, v} (RingHom.id R) (φ i) M) ↦
        (∑ i : ι, f i ∘ₗ proj (φ := φ) i : ((i : ι) → φ i) →ₗ[R] M))
      ((fun (f : ((i : ι) → φ i) →ₗ[R] M) (i : ι) ↦ f ∘ₗ single R φ i) f) =
    f
have h : ∀ (x : (i : ι) → φ i),
  Eq.{v + 1} (α := M)
    (((fun (f : (i : ι) → LinearMap.{u, u, i, v} (RingHom.id R) (φ i) M) ↦
              (∑ i : ι, f i ∘ₗ proj (φ := φ) i : ((i : ι) → φ i) →ₗ[R] M))
            ((fun (f : ((i : ι) → φ i) →ₗ[R] M) (i : ι) ↦ f ∘ₗ single R φ i) f) :
          (a : (i : ι) → φ i) → M)
        x :
      M)
    ((f : (a : (i : ι) → φ i) → M) x : M)
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
Goal:
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst : Semiring R
inst_1 : AddCommMonoid M₂
inst_2 : Module R M₂
inst_3 : AddCommMonoid M₃
inst_4 : Module R M₃
φ : ι → Type i
inst_5 : (i : ι) → AddCommMonoid (φ i)
inst_6 : (i : ι) → Module.{u, i} R (φ i)
inst_7 : DecidableEq ι
S : Type u_1
inst_8 : AddCommMonoid M
inst_9 : Module R M
inst_10 : Fintype ι
inst_11 : Semiring S
inst_12 : Module S M
inst_13 : SMulCommClass R S M
f : ((i : ι) → φ i) →ₗ[R] M
x : (i : ι) → φ i
⊢ Eq.{v + 1} (α := M)
    (((fun (f : (i : ι) → LinearMap.{u, u, i, v} (RingHom.id R) (φ i) M) ↦
              (∑ i : ι, f i ∘ₗ proj (φ := φ) i : ((i : ι) → φ i) →ₗ[R] M))
            ((fun (f : ((i : ι) → φ i) →ₗ[R] M) (i : ι) ↦ f ∘ₗ single R φ i) f) :
          (a : (i : ι) → φ i) → M)
        x :
      M)
    ((f : (a : (i : ι) → φ i) → M) x : M)
have h : Eq.{v + 1} (α := M) ((f : (a : (i : ι) → φ i) → M) (∑ j : ι, Pi.single (M := φ) j (x j)) : M)
  ((f : (a : (i : ι) → φ i) → M) x : M)
Tactic: suffices f (∑ j, Pi.single j (x j)) = f x by simpa [apply_single]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
Goal:
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst : Semiring R
inst_1 : AddCommMonoid M₂
inst_2 : Module R M₂
inst_3 : AddCommMonoid M₃
inst_4 : Module R M₃
φ : ι → Type i
inst_5 : (i : ι) → AddCommMonoid (φ i)
inst_6 : (i : ι) → Module.{u, i} R (φ i)
inst_7 : DecidableEq ι
S : Type u_1
inst_8 : AddCommMonoid M
inst_9 : Module R M
inst_10 : Fintype ι
inst_11 : Semiring S
inst_12 : Module S M
inst_13 : SMulCommClass R S M
f : ((i : ι) → φ i) →ₗ[R] M
x : (i : ι) → φ i
⊢ Eq.{v + 1} (α := M) ((f : (a : (i : ι) → φ i) → M) (∑ j : ι, Pi.single (M := φ) j (x j)) : M)
    ((f : (a : (i : ι) → φ i) → M) x : M)
have h : Eq.{v + 1} (α := M) ((f : (a : (i : ι) → φ i) → M) x : M) ((f : (a : (i : ι) → φ i) → M) x : M)
Tactic: rw [Finset.univ_sum_single]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
Goal:
R : Type u
M : Type v
ι : Type x
inst : Semiring R
φ : ι → Type i
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, i} R (φ i)
inst_3 : DecidableEq ι
S : Type u_1
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : Fintype ι
inst_7 : Semiring S
inst_8 : Module S M
inst_9 : SMulCommClass R S M
f : (i : ι) → LinearMap.{u, u, i, v} (RingHom.id R) (φ i) M
i : ι
x : φ i
⊢ Eq.{v + 1} (α := M)
    ((((lsum R φ S : (a : (i : ι) → φ i →ₗ[R] M) → ((i : ι) → φ i) →ₗ[R] M) f : ((i : ι) → φ i) →ₗ[R] M) :
          (a : (i : ι) → φ i) → M)
        (Pi.single (M := φ) i x) :
      M)
    ((f i : (a : φ i) → M) x : M)
have simp_rw : Eq.{v + 1} (α := M) ((∑ i : ι, f i ∘ₗ proj (φ := φ) i : (a : (i : ι) → φ i) → M) (Pi.single (M := φ) i x) : M)
  ((f i : (a : φ i) → M) x : M)
Tactic: simp_rw [lsum_apply, sum_apply, comp_apply, proj_apply, apply_single, Fintype.sum_pi_single']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
Goal:
R : Type u
M : Type v
ι : Type x
inst : Semiring R
φ : ι → Type i
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, i} R (φ i)
inst_3 : DecidableEq ι
S : Type u_1
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : Fintype ι
inst_7 : Semiring S
inst_8 : Module S M
inst_9 : SMulCommClass R S M
f : (i : ι) → LinearMap.{u, u, i, v} (RingHom.id R) (φ i) M
i : ι
x : φ i
simp_rw :
  Eq.{v + 1} (α := M) ((∑ i : ι, f i ∘ₗ proj (φ := φ) i : (a : (i : ι) → φ i) → M) (Pi.single (M := φ) i x) : M)
    ((f i : (a : φ i) → M) x : M)
⊢ Eq.{v + 1} (α := M)
    ((((lsum R φ S : (a : (i : ι) → φ i →ₗ[R] M) → ((i : ι) → φ i) →ₗ[R] M) f : ((i : ι) → φ i) →ₗ[R] M) :
          (a : (i : ι) → φ i) → M)
        (Pi.single (M := φ) i x) :
      M)
    ((f i : (a : φ i) → M) x : M)
have simp_rw₁ : Eq.{v + 1} (α := M) (∑ d : ι, (f d ∘ₗ proj (φ := φ) d : (a : (i : ι) → φ i) → M) (Pi.single (M := φ) i x) : M)
  ((f i : (a : φ i) → M) x : M)
Tactic: simp_rw [lsum_apply, sum_apply, comp_apply, proj_apply, apply_single, Fintype.sum_pi_single']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
Goal:
R : Type u
M : Type v
ι : Type x
inst : Semiring R
φ : ι → Type i
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, i} R (φ i)
inst_3 : DecidableEq ι
S : Type u_1
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : Fintype ι
inst_7 : Semiring S
inst_8 : Module S M
inst_9 : SMulCommClass R S M
f : (i : ι) → LinearMap.{u, u, i, v} (RingHom.id R) (φ i) M
i : ι
x : φ i
simp_rw :
  Eq.{v + 1} (α := M) ((∑ i : ι, f i ∘ₗ proj (φ := φ) i : (a : (i : ι) → φ i) → M) (Pi.single (M := φ) i x) : M)
    ((f i : (a : φ i) → M) x : M)
simp_rw₁ :
  Eq.{v + 1} (α := M) (∑ d : ι, (f d ∘ₗ proj (φ := φ) d : (a : (i : ι) → φ i) → M) (Pi.single (M := φ) i x) : M)
    ((f i : (a : φ i) → M) x : M)
⊢ Eq.{v + 1} (α := M)
    ((((lsum R φ S : (a : (i : ι) → φ i →ₗ[R] M) → ((i : ι) → φ i) →ₗ[R] M) f : ((i : ι) → φ i) →ₗ[R] M) :
          (a : (i : ι) → φ i) → M)
        (Pi.single (M := φ) i x) :
      M)
    ((f i : (a : φ i) → M) x : M)
have simp_rw₂ : Eq.{v + 1} (α := M)
  (∑ x_1 : ι,
      (f x_1 : (a : φ x_1) → M) ((proj (φ := φ) x_1 : (a : (i : ι) → φ i) → φ x_1) (Pi.single (M := φ) i x) : φ x_1) :
    M)
  ((f i : (a : φ i) → M) x : M)
Tactic: simp_rw [lsum_apply, sum_apply, comp_apply, proj_apply, apply_single, Fintype.sum_pi_single']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
Goal:
R : Type u
M : Type v
ι : Type x
inst : Semiring R
φ : ι → Type i
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, i} R (φ i)
inst_3 : DecidableEq ι
S : Type u_1
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : Fintype ι
inst_7 : Semiring S
inst_8 : Module S M
inst_9 : SMulCommClass R S M
f : (i : ι) → LinearMap.{u, u, i, v} (RingHom.id R) (φ i) M
i : ι
x : φ i
simp_rw :
  Eq.{v + 1} (α := M) ((∑ i : ι, f i ∘ₗ proj (φ := φ) i : (a : (i : ι) → φ i) → M) (Pi.single (M := φ) i x) : M)
    ((f i : (a : φ i) → M) x : M)
simp_rw₁ :
  Eq.{v + 1} (α := M) (∑ d : ι, (f d ∘ₗ proj (φ := φ) d : (a : (i : ι) → φ i) → M) (Pi.single (M := φ) i x) : M)
    ((f i : (a : φ i) → M) x : M)
simp_rw₂ :
  Eq.{v + 1} (α := M)
    (∑ x_1 : ι,
        (f x_1 : (a : φ x_1) → M) ((proj (φ := φ) x_1 : (a : (i : ι) → φ i) → φ x_1) (Pi.single (M := φ) i x) : φ x_1) :
      M)
    ((f i : (a : φ i) → M) x : M)
⊢ Eq.{v + 1} (α := M)
    ((((lsum R φ S : (a : (i : ι) → φ i →ₗ[R] M) → ((i : ι) → φ i) →ₗ[R] M) f : ((i : ι) → φ i) →ₗ[R] M) :
          (a : (i : ι) → φ i) → M)
        (Pi.single (M := φ) i x) :
      M)
    ((f i : (a : φ i) → M) x : M)
have simp_rw₃ : Eq.{v + 1} (α := M) (∑ x_1 : ι, (f x_1 : (a : φ x_1) → M) (Pi.single (M := φ) i x x_1) : M)
  ((f i : (a : φ i) → M) x : M)
Tactic: simp_rw [lsum_apply, sum_apply, comp_apply, proj_apply, apply_single, Fintype.sum_pi_single']