internlm/Lean-Github huggingface dataset:
Theorem: DirectSum.map'_of
Proof state before:
ι : Type u_1
inst✝³ : DecidableEq ι
R : Type u_2
inst✝² : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝¹ : (i : ι) → AddCommMonoid (β i)
inst✝ : (i : ι) → AddCommMonoid (γ i)
h : (i : ι) → β i →+ γ i
i : ι
x : β i
⊢ (map' h) ((of β i) x) = (of γ i) ((h i) x)
Tactic:
simp only [map', toAddMonoid_of, AddMonoidHom.coe_comp]
Proof state after:
ι : Type u_1
inst✝³ : DecidableEq ι
R : Type u_2
inst✝² : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝¹ : (i : ι) → AddCommMonoid (β i)
inst✝ : (i : ι) → AddCommMonoid (γ i)
h : (i : ι) → β i →+ γ i
i : ι
x : β i
⊢ (⇑(of (fun i => γ i) i) ∘ ⇑(h i)) x = (of γ i) ((h i) x)
Theorem: DirectSum.map'_of
Proof state before:
ι : Type u_1
inst✝³ : DecidableEq ι
R : Type u_2
inst✝² : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝¹ : (i : ι) → AddCommMonoid (β i)
inst✝ : (i : ι) → AddCommMonoid (γ i)
h : (i : ι) → β i →+ γ i
i : ι
x : β i
⊢ (⇑(of (fun i => γ i) i) ∘ ⇑(h i)) x = (of γ i) ((h i) x)
Tactic:
rfl
Proof state after:
no goals
Theorem: DirectSum.lmap'_lof
Proof state before:
ι : Type u_1
inst✝⁵ : DecidableEq ι
R : Type u_2
inst✝⁴ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝³ : (i : ι) → AddCommMonoid (β i)
inst✝² : (i : ι) → AddCommMonoid (γ i)
inst✝¹ : (i : ι) → Module R (β i)
inst✝ : (i : ι) → Module R (γ i)
h : (i : ι) → β i →ₗ[R] γ i
i : ι
x : β i
⊢ (lmap' h) ((lof R ι β i) x) = (lof R ι γ i) ((h i) x)
Tactic:
simp only [lmap', toModule_lof, LinearMap.coe_comp]
Proof state after:
ι : Type u_1
inst✝⁵ : DecidableEq ι
R : Type u_2
inst✝⁴ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝³ : (i : ι) → AddCommMonoid (β i)
inst✝² : (i : ι) → AddCommMonoid (γ i)
inst✝¹ : (i : ι) → Module R (β i)
inst✝ : (i : ι) → Module R (γ i)
h : (i : ι) → β i →ₗ[R] γ i
i : ι
x : β i
⊢ (⇑(lof R ι (fun i => γ i) i) ∘ ⇑(h i)) x = (lof R ι γ i) ((h i) x)
Theorem: DirectSum.lmap'_lof
Proof state before:
ι : Type u_1
inst✝⁵ : DecidableEq ι
R : Type u_2
inst✝⁴ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝³ : (i : ι) → AddCommMonoid (β i)
inst✝² : (i : ι) → AddCommMonoid (γ i)
inst✝¹ : (i : ι) → Module R (β i)
inst✝ : (i : ι) → Module R (γ i)
h : (i : ι) → β i →ₗ[R] γ i
i : ι
x : β i
⊢ (⇑(lof R ι (fun i => γ i) i) ∘ ⇑(h i)) x = (lof R ι γ i) ((h i) x)
Tactic:
rfl
Proof state after:
no goals
Theorem: DirectSum.lmap'_surjective
Proof state before:
ι : Type u_1
inst✝⁵ : DecidableEq ι
R : Type u_2
inst✝⁴ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝³ : (i : ι) → AddCommMonoid (β i)
inst✝² : (i : ι) → Module R (β i)
inst✝¹ : (i : ι) → AddCommMonoid (γ i)
inst✝ : (i : ι) → Module R (γ i)
f : (i : ι) → β i →ₗ[R] γ i
h : ∀ (i : ι), Surjective ⇑(f i)
⊢ Surjective ⇑(lmap' f)
Tactic:
intro c
Proof state after:
ι : Type u_1
inst✝⁵ : DecidableEq ι
R : Type u_2
inst✝⁴ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝³ : (i : ι) → AddCommMonoid (β i)
inst✝² : (i : ι) → Module R (β i)
inst✝¹ : (i : ι) → AddCommMonoid (γ i)
inst✝ : (i : ι) → Module R (γ i)
f : (i : ι) → β i →ₗ[R] γ i
h : ∀ (i : ι), Surjective ⇑(f i)
c : ⨁ (i : ι), γ i
⊢ ∃ a, (lmap' f) a = c
Theorem: DirectSum.lmap'_surjective
Proof state before:
ι : Type u_1
inst✝⁵ : DecidableEq ι
R : Type u_2
inst✝⁴ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝³ : (i : ι) → AddCommMonoid (β i)
inst✝² : (i : ι) → Module R (β i)
inst✝¹ : (i : ι) → AddCommMonoid (γ i)
inst✝ : (i : ι) → Module R (γ i)
f : (i : ι) → β i →ₗ[R] γ i
h : ∀ (i : ι), Surjective ⇑(f i)
c : ⨁ (i : ι), γ i
⊢ ∃ a, (lmap' f) a = c
Tactic:
induction' c using DirectSum.induction_on with i xi x y hx hy
Proof state after:
case H_zero
ι : Type u_1
inst✝⁵ : DecidableEq ι
R : Type u_2
inst✝⁴ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝³ : (i : ι) → AddCommMonoid (β i)
inst✝² : (i : ι) → Module R (β i)
inst✝¹ : (i : ι) → AddCommMonoid (γ i)
inst✝ : (i : ι) → Module R (γ i)
f : (i : ι) → β i →ₗ[R] γ i
h : ∀ (i : ι), Surjective ⇑(f i)
⊢ ∃ a, (lmap' f) a = 0

case H_basic
ι : Type u_1
inst✝⁵ : DecidableEq ι
R : Type u_2
inst✝⁴ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝³ : (i : ι) → AddCommMonoid (β i)
inst✝² : (i : ι) → Module R (β i)
inst✝¹ : (i : ι) → AddCommMonoid (γ i)
inst✝ : (i : ι) → Module R (γ i)
f : (i : ι) → β i →ₗ[R] γ i
h : ∀ (i : ι), Surjective ⇑(f i)
i : ι
xi : γ i
⊢ ∃ a, (lmap' f) a = (of (fun i => γ i) i) xi

case H_plus
ι : Type u_1
inst✝⁵ : DecidableEq ι
R : Type u_2
inst✝⁴ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝³ : (i : ι) → AddCommMonoid (β i)
inst✝² : (i : ι) → Module R (β i)
inst✝¹ : (i : ι) → AddCommMonoid (γ i)
inst✝ : (i : ι) → Module R (γ i)
f : (i : ι) → β i →ₗ[R] γ i
h : ∀ (i : ι), Surjective ⇑(f i)
x y : ⨁ (i : ι), γ i
hx : ∃ a, (lmap' f) a = x
hy : ∃ a, (lmap' f) a = y
⊢ ∃ a, (lmap' f) a = x + y
Theorem: DirectSum.lmap'_surjective
Proof state before:
case H_zero
ι : Type u_1
inst✝⁵ : DecidableEq ι
R : Type u_2
inst✝⁴ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝³ : (i : ι) → AddCommMonoid (β i)
inst✝² : (i : ι) → Module R (β i)
inst✝¹ : (i : ι) → AddCommMonoid (γ i)
inst✝ : (i : ι) → Module R (γ i)
f : (i : ι) → β i →ₗ[R] γ i
h : ∀ (i : ι), Surjective ⇑(f i)
⊢ ∃ a, (lmap' f) a = 0

case H_basic
ι : Type u_1
inst✝⁵ : DecidableEq ι
R : Type u_2
inst✝⁴ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝³ : (i : ι) → AddCommMonoid (β i)
inst✝² : (i : ι) → Module R (β i)
inst✝¹ : (i : ι) → AddCommMonoid (γ i)
inst✝ : (i : ι) → Module R (γ i)
f : (i : ι) → β i →ₗ[R] γ i
h : ∀ (i : ι), Surjective ⇑(f i)
i : ι
xi : γ i
⊢ ∃ a, (lmap' f) a = (of (fun i => γ i) i) xi

case H_plus
ι : Type u_1
inst✝⁵ : DecidableEq ι
R : Type u_2
inst✝⁴ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝³ : (i : ι) → AddCommMonoid (β i)
inst✝² : (i : ι) → Module R (β i)
inst✝¹ : (i : ι) → AddCommMonoid (γ i)
inst✝ : (i : ι) → Module R (γ i)
f : (i : ι) → β i →ₗ[R] γ i
h : ∀ (i : ι), Surjective ⇑(f i)
x y : ⨁ (i : ι), γ i
hx : ∃ a, (lmap' f) a = x
hy : ∃ a, (lmap' f) a = y
⊢ ∃ a, (lmap' f) a = x + y
Tactic:
. exact ⟨0, map_zero _⟩
Proof state after:
case H_basic
ι : Type u_1
inst✝⁵ : DecidableEq ι
R : Type u_2
inst✝⁴ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝³ : (i : ι) → AddCommMonoid (β i)
inst✝² : (i : ι) → Module R (β i)
inst✝¹ : (i : ι) → AddCommMonoid (γ i)
inst✝ : (i : ι) → Module R (γ i)
f : (i : ι) → β i →ₗ[R] γ i
h : ∀ (i : ι), Surjective ⇑(f i)
i : ι
xi : γ i
⊢ ∃ a, (lmap' f) a = (of (fun i => γ i) i) xi

case H_plus
ι : Type u_1
inst✝⁵ : DecidableEq ι
R : Type u_2
inst✝⁴ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝³ : (i : ι) → AddCommMonoid (β i)
inst✝² : (i : ι) → Module R (β i)
inst✝¹ : (i : ι) → AddCommMonoid (γ i)
inst✝ : (i : ι) → Module R (γ i)
f : (i : ι) → β i →ₗ[R] γ i
h : ∀ (i : ι), Surjective ⇑(f i)
x y : ⨁ (i : ι), γ i
hx : ∃ a, (lmap' f) a = x
hy : ∃ a, (lmap' f) a = y
⊢ ∃ a, (lmap' f) a = x + y
Theorem: DirectSum.lmap'_surjective
Proof state before:
case H_basic
ι : Type u_1
inst✝⁵ : DecidableEq ι
R : Type u_2
inst✝⁴ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝³ : (i : ι) → AddCommMonoid (β i)
inst✝² : (i : ι) → Module R (β i)
inst✝¹ : (i : ι) → AddCommMonoid (γ i)
inst✝ : (i : ι) → Module R (γ i)
f : (i : ι) → β i →ₗ[R] γ i
h : ∀ (i : ι), Surjective ⇑(f i)
i : ι
xi : γ i
⊢ ∃ a, (lmap' f) a = (of (fun i => γ i) i) xi

case H_plus
ι : Type u_1
inst✝⁵ : DecidableEq ι
R : Type u_2
inst✝⁴ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝³ : (i : ι) → AddCommMonoid (β i)
inst✝² : (i : ι) → Module R (β i)
inst✝¹ : (i : ι) → AddCommMonoid (γ i)
inst✝ : (i : ι) → Module R (γ i)
f : (i : ι) → β i →ₗ[R] γ i
h : ∀ (i : ι), Surjective ⇑(f i)
x y : ⨁ (i : ι), γ i
hx : ∃ a, (lmap' f) a = x
hy : ∃ a, (lmap' f) a = y
⊢ ∃ a, (lmap' f) a = x + y
Tactic:
. use of _ i (h i xi).choose
  rw [← lof_eq_of R, lmap'_lof, lof_eq_of, (h i xi).choose_spec]
Proof state after:
case H_plus
ι : Type u_1
inst✝⁵ : DecidableEq ι
R : Type u_2
inst✝⁴ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝³ : (i : ι) → AddCommMonoid (β i)
inst✝² : (i : ι) → Module R (β i)
inst✝¹ : (i : ι) → AddCommMonoid (γ i)
inst✝ : (i : ι) → Module R (γ i)
f : (i : ι) → β i →ₗ[R] γ i
h : ∀ (i : ι), Surjective ⇑(f i)
x y : ⨁ (i : ι), γ i
hx : ∃ a, (lmap' f) a = x
hy : ∃ a, (lmap' f) a = y
⊢ ∃ a, (lmap' f) a = x + y
Theorem: DirectSum.lmap'_surjective
Proof state before:
case H_plus
ι : Type u_1
inst✝⁵ : DecidableEq ι
R : Type u_2
inst✝⁴ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝³ : (i : ι) → AddCommMonoid (β i)
inst✝² : (i : ι) → Module R (β i)
inst✝¹ : (i : ι) → AddCommMonoid (γ i)
inst✝ : (i : ι) → Module R (γ i)
f : (i : ι) → β i →ₗ[R] γ i
h : ∀ (i : ι), Surjective ⇑(f i)
x y : ⨁ (i : ι), γ i
hx : ∃ a, (lmap' f) a = x
hy : ∃ a, (lmap' f) a = y
⊢ ∃ a, (lmap' f) a = x + y
Tactic:
. obtain ⟨a, ha, rfl⟩ := hx
  obtain ⟨b, hb, rfl⟩ := hy
  exact ⟨a + b, map_add _ _ _⟩
Proof state after:
no goals
Theorem: DirectSum.lmap'_surjective
Proof state before:
case H_zero
ι : Type u_1
inst✝⁵ : DecidableEq ι
R : Type u_2
inst✝⁴ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝³ : (i : ι) → AddCommMonoid (β i)
inst✝² : (i : ι) → Module R (β i)
inst✝¹ : (i : ι) → AddCommMonoid (γ i)
inst✝ : (i : ι) → Module R (γ i)
f : (i : ι) → β i →ₗ[R] γ i
h : ∀ (i : ι), Surjective ⇑(f i)
⊢ ∃ a, (lmap' f) a = 0
Tactic:
exact ⟨0, map_zero _⟩
Proof state after:
no goals
Theorem: DirectSum.lmap'_surjective
Proof state before:
case H_basic
ι : Type u_1
inst✝⁵ : DecidableEq ι
R : Type u_2
inst✝⁴ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝³ : (i : ι) → AddCommMonoid (β i)
inst✝² : (i : ι) → Module R (β i)
inst✝¹ : (i : ι) → AddCommMonoid (γ i)
inst✝ : (i : ι) → Module R (γ i)
f : (i : ι) → β i →ₗ[R] γ i
h : ∀ (i : ι), Surjective ⇑(f i)
i : ι
xi : γ i
⊢ ∃ a, (lmap' f) a = (of (fun i => γ i) i) xi
Tactic:
use of _ i (h i xi).choose
Proof state after:
case h
ι : Type u_1
inst✝⁵ : DecidableEq ι
R : Type u_2
inst✝⁴ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝³ : (i : ι) → AddCommMonoid (β i)
inst✝² : (i : ι) → Module R (β i)
inst✝¹ : (i : ι) → AddCommMonoid (γ i)
inst✝ : (i : ι) → Module R (γ i)
f : (i : ι) → β i →ₗ[R] γ i
h : ∀ (i : ι), Surjective ⇑(f i)
i : ι
xi : γ i
⊢ (lmap' f) ((of (fun i => β i) i) ⋯.choose) = (of (fun i => γ i) i) xi
Theorem: DirectSum.lmap'_surjective
Proof state before:
case h
ι : Type u_1
inst✝⁵ : DecidableEq ι
R : Type u_2
inst✝⁴ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝³ : (i : ι) → AddCommMonoid (β i)
inst✝² : (i : ι) → Module R (β i)
inst✝¹ : (i : ι) → AddCommMonoid (γ i)
inst✝ : (i : ι) → Module R (γ i)
f : (i : ι) → β i →ₗ[R] γ i
h : ∀ (i : ι), Surjective ⇑(f i)
i : ι
xi : γ i
⊢ (lmap' f) ((of (fun i => β i) i) ⋯.choose) = (of (fun i => γ i) i) xi
Tactic:
rw [← lof_eq_of R, lmap'_lof, lof_eq_of, (h i xi).choose_spec]
Proof state after:
no goals
Theorem: DirectSum.lmap'_surjective
Proof state before:
case H_plus
ι : Type u_1
inst✝⁵ : DecidableEq ι
R : Type u_2
inst✝⁴ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝³ : (i : ι) → AddCommMonoid (β i)
inst✝² : (i : ι) → Module R (β i)
inst✝¹ : (i : ι) → AddCommMonoid (γ i)
inst✝ : (i : ι) → Module R (γ i)
f : (i : ι) → β i →ₗ[R] γ i
h : ∀ (i : ι), Surjective ⇑(f i)
x y : ⨁ (i : ι), γ i
hx : ∃ a, (lmap' f) a = x
hy : ∃ a, (lmap' f) a = y
⊢ ∃ a, (lmap' f) a = x + y
Tactic:
obtain ⟨a, ha, rfl⟩ := hx
Proof state after:
case H_plus.intro.refl
ι : Type u_1
inst✝⁵ : DecidableEq ι
R : Type u_2
inst✝⁴ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝³ : (i : ι) → AddCommMonoid (β i)
inst✝² : (i : ι) → Module R (β i)
inst✝¹ : (i : ι) → AddCommMonoid (γ i)
inst✝ : (i : ι) → Module R (γ i)
f : (i : ι) → β i →ₗ[R] γ i
h : ∀ (i : ι), Surjective ⇑(f i)
y : ⨁ (i : ι), γ i
hy : ∃ a, (lmap' f) a = y
a : ⨁ (i : ι), β i
⊢ ∃ a_1, (lmap' f) a_1 = (lmap' f) a + y
Theorem: DirectSum.lmap'_surjective
Proof state before:
case H_plus.intro.refl
ι : Type u_1
inst✝⁵ : DecidableEq ι
R : Type u_2
inst✝⁴ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝³ : (i : ι) → AddCommMonoid (β i)
inst✝² : (i : ι) → Module R (β i)
inst✝¹ : (i : ι) → AddCommMonoid (γ i)
inst✝ : (i : ι) → Module R (γ i)
f : (i : ι) → β i →ₗ[R] γ i
h : ∀ (i : ι), Surjective ⇑(f i)
y : ⨁ (i : ι), γ i
hy : ∃ a, (lmap' f) a = y
a : ⨁ (i : ι), β i
⊢ ∃ a_1, (lmap' f) a_1 = (lmap' f) a + y
Tactic:
obtain ⟨b, hb, rfl⟩ := hy
Proof state after:
case H_plus.intro.refl.intro.refl
ι : Type u_1
inst✝⁵ : DecidableEq ι
R : Type u_2
inst✝⁴ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝³ : (i : ι) → AddCommMonoid (β i)
inst✝² : (i : ι) → Module R (β i)
inst✝¹ : (i : ι) → AddCommMonoid (γ i)
inst✝ : (i : ι) → Module R (γ i)
f : (i : ι) → β i →ₗ[R] γ i
h : ∀ (i : ι), Surjective ⇑(f i)
a b : ⨁ (i : ι), β i
⊢ ∃ a_1, (lmap' f) a_1 = (lmap' f) a + (lmap' f) b
Theorem: DirectSum.lmap'_surjective
Proof state before:
case H_plus.intro.refl.intro.refl
ι : Type u_1
inst✝⁵ : DecidableEq ι
R : Type u_2
inst✝⁴ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝³ : (i : ι) → AddCommMonoid (β i)
inst✝² : (i : ι) → Module R (β i)
inst✝¹ : (i : ι) → AddCommMonoid (γ i)
inst✝ : (i : ι) → Module R (γ i)
f : (i : ι) → β i →ₗ[R] γ i
h : ∀ (i : ι), Surjective ⇑(f i)
a b : ⨁ (i : ι), β i
⊢ ∃ a_1, (lmap' f) a_1 = (lmap' f) a + (lmap' f) b
Tactic:
exact ⟨a + b, map_add _ _ _⟩
Proof state after:
no goals
Theorem: DirectSum.lmap'_apply
Proof state before:
ι : Type u_1
inst✝⁵ : DecidableEq ι
R : Type u_2
inst✝⁴ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝³ : (i : ι) → AddCommMonoid (β i)
inst✝² : (i : ι) → AddCommMonoid (γ i)
inst✝¹ : (i : ι) → Module R (β i)
inst✝ : (i : ι) → Module R (γ i)
h : (i : ι) → β i →ₗ[R] γ i
x : ⨁ (i : ι), β i
i : ι
⊢ ((lmap' h) x) i = (h i) (x i)
Tactic:
simp only [apply_eq_component R, ← LinearMap.comp_apply]
Proof state after:
ι : Type u_1
inst✝⁵ : DecidableEq ι
R : Type u_2
inst✝⁴ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝³ : (i : ι) → AddCommMonoid (β i)
inst✝² : (i : ι) → AddCommMonoid (γ i)
inst✝¹ : (i : ι) → Module R (β i)
inst✝ : (i : ι) → Module R (γ i)
h : (i : ι) → β i →ₗ[R] γ i
x : ⨁ (i : ι), β i
i : ι
⊢ (component R ι (fun i => γ i) i ∘ₗ lmap' h) x = (h i ∘ₗ component R ι (fun i => β i) i) x
Theorem: DirectSum.lmap'_apply
Proof state before:
ι : Type u_1
inst✝⁵ : DecidableEq ι
R : Type u_2
inst✝⁴ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝³ : (i : ι) → AddCommMonoid (β i)
inst✝² : (i : ι) → AddCommMonoid (γ i)
inst✝¹ : (i : ι) → Module R (β i)
inst✝ : (i : ι) → Module R (γ i)
h : (i : ι) → β i →ₗ[R] γ i
x : ⨁ (i : ι), β i
i : ι
⊢ (component R ι (fun i => γ i) i ∘ₗ lmap' h) x = (h i ∘ₗ component R ι (fun i => β i) i) x
Tactic:
apply LinearMap.congr_fun
Proof state after:
case h
ι : Type u_1
inst✝⁵ : DecidableEq ι
R : Type u_2
inst✝⁴ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝³ : (i : ι) → AddCommMonoid (β i)
inst✝² : (i : ι) → AddCommMonoid (γ i)
inst✝¹ : (i : ι) → Module R (β i)
inst✝ : (i : ι) → Module R (γ i)
h : (i : ι) → β i →ₗ[R] γ i
x : ⨁ (i : ι), β i
i : ι
⊢ component R ι (fun i => γ i) i ∘ₗ lmap' h = h i ∘ₗ component R ι (fun i => β i) i
Theorem: DirectSum.lmap'_apply
Proof state before:
case h
ι : Type u_1
inst✝⁵ : DecidableEq ι
R : Type u_2
inst✝⁴ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝³ : (i : ι) → AddCommMonoid (β i)
inst✝² : (i : ι) → AddCommMonoid (γ i)
inst✝¹ : (i : ι) → Module R (β i)
inst✝ : (i : ι) → Module R (γ i)
h : (i : ι) → β i →ₗ[R] γ i
x : ⨁ (i : ι), β i
i : ι
⊢ component R ι (fun i => γ i) i ∘ₗ lmap' h = h i ∘ₗ component R ι (fun i => β i) i
Tactic:
ext j y
Proof state after:
case h.H.h
ι : Type u_1
inst✝⁵ : DecidableEq ι
R : Type u_2
inst✝⁴ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝³ : (i : ι) → AddCommMonoid (β i)
inst✝² : (i : ι) → AddCommMonoid (γ i)
inst✝¹ : (i : ι) → Module R (β i)
inst✝ : (i : ι) → Module R (γ i)
h : (i : ι) → β i →ₗ[R] γ i
x : ⨁ (i : ι), β i
i j : ι
y : β j
⊢ ((component R ι (fun i => γ i) i ∘ₗ lmap' h) ∘ₗ lof R ι (fun i => β i) j) y =
    ((h i ∘ₗ component R ι (fun i => β i) i) ∘ₗ lof R ι (fun i => β i) j) y
Theorem: DirectSum.lmap'_apply
Proof state before:
case h.H.h
ι : Type u_1
inst✝⁵ : DecidableEq ι
R : Type u_2
inst✝⁴ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝³ : (i : ι) → AddCommMonoid (β i)
inst✝² : (i : ι) → AddCommMonoid (γ i)
inst✝¹ : (i : ι) → Module R (β i)
inst✝ : (i : ι) → Module R (γ i)
h : (i : ι) → β i →ₗ[R] γ i
x : ⨁ (i : ι), β i
i j : ι
y : β j
⊢ ((component R ι (fun i => γ i) i ∘ₗ lmap' h) ∘ₗ lof R ι (fun i => β i) j) y =
    ((h i ∘ₗ component R ι (fun i => β i) i) ∘ₗ lof R ι (fun i => β i) j) y
Tactic:
simp only [LinearMap.comp_apply, lmap'_lof]
Proof state after:
case h.H.h
ι : Type u_1
inst✝⁵ : DecidableEq ι
R : Type u_2
inst✝⁴ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝³ : (i : ι) → AddCommMonoid (β i)
inst✝² : (i : ι) → AddCommMonoid (γ i)
inst✝¹ : (i : ι) → Module R (β i)
inst✝ : (i : ι) → Module R (γ i)
h : (i : ι) → β i →ₗ[R] γ i
x : ⨁ (i : ι), β i
i j : ι
y : β j
⊢ (component R ι (fun i => γ i) i) ((lof R ι (fun i => γ i) j) ((h j) y)) =
    (h i) ((component R ι (fun i => β i) i) ((lof R ι (fun i => β i) j) y))
Theorem: DirectSum.lmap'_apply
Proof state before:
case h.H.h
ι : Type u_1
inst✝⁵ : DecidableEq ι
R : Type u_2
inst✝⁴ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝³ : (i : ι) → AddCommMonoid (β i)
inst✝² : (i : ι) → AddCommMonoid (γ i)
inst✝¹ : (i : ι) → Module R (β i)
inst✝ : (i : ι) → Module R (γ i)
h : (i : ι) → β i →ₗ[R] γ i
x : ⨁ (i : ι), β i
i j : ι
y : β j
⊢ (component R ι (fun i => γ i) i) ((lof R ι (fun i => γ i) j) ((h j) y)) =
    (h i) ((component R ι (fun i => β i) i) ((lof R ι (fun i => β i) j) y))
Tactic:
simp only [lof_eq_of, ← apply_eq_component]
Proof state after:
case h.H.h
ι : Type u_1
inst✝⁵ : DecidableEq ι
R : Type u_2
inst✝⁴ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝³ : (i : ι) → AddCommMonoid (β i)
inst✝² : (i : ι) → AddCommMonoid (γ i)
inst✝¹ : (i : ι) → Module R (β i)
inst✝ : (i : ι) → Module R (γ i)
h : (i : ι) → β i →ₗ[R] γ i
x : ⨁ (i : ι), β i
i j : ι
y : β j
⊢ ((of (fun i => γ i) j) ((h j) y)) i = (h i) (((of (fun i => β i) j) y) i)
Theorem: DirectSum.lmap'_apply
Proof state before:
case h.H.h
ι : Type u_1
inst✝⁵ : DecidableEq ι
R : Type u_2
inst✝⁴ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝³ : (i : ι) → AddCommMonoid (β i)
inst✝² : (i : ι) → AddCommMonoid (γ i)
inst✝¹ : (i : ι) → Module R (β i)
inst✝ : (i : ι) → Module R (γ i)
h : (i : ι) → β i →ₗ[R] γ i
x : ⨁ (i : ι), β i
i j : ι
y : β j
⊢ ((of (fun i => γ i) j) ((h j) y)) i = (h i) (((of (fun i => β i) j) y) i)
Tactic:
by_cases hji : j = i
Proof state after:
case pos
ι : Type u_1
inst✝⁵ : DecidableEq ι
R : Type u_2
inst✝⁴ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝³ : (i : ι) → AddCommMonoid (β i)
inst✝² : (i : ι) → AddCommMonoid (γ i)
inst✝¹ : (i : ι) → Module R (β i)
inst✝ : (i : ι) → Module R (γ i)
h : (i : ι) → β i →ₗ[R] γ i
x : ⨁ (i : ι), β i
i j : ι
y : β j
hji : j = i
⊢ ((of (fun i => γ i) j) ((h j) y)) i = (h i) (((of (fun i => β i) j) y) i)

case neg
ι : Type u_1
inst✝⁵ : DecidableEq ι
R : Type u_2
inst✝⁴ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝³ : (i : ι) → AddCommMonoid (β i)
inst✝² : (i : ι) → AddCommMonoid (γ i)
inst✝¹ : (i : ι) → Module R (β i)
inst✝ : (i : ι) → Module R (γ i)
h : (i : ι) → β i →ₗ[R] γ i
x : ⨁ (i : ι), β i
i j : ι
y : β j
hji : ¬j = i
⊢ ((of (fun i => γ i) j) ((h j) y)) i = (h i) (((of (fun i => β i) j) y) i)
Theorem: DirectSum.lmap'_apply
Proof state before:
case pos
ι : Type u_1
inst✝⁵ : DecidableEq ι
R : Type u_2
inst✝⁴ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝³ : (i : ι) → AddCommMonoid (β i)
inst✝² : (i : ι) → AddCommMonoid (γ i)
inst✝¹ : (i : ι) → Module R (β i)
inst✝ : (i : ι) → Module R (γ i)
h : (i : ι) → β i →ₗ[R] γ i
x : ⨁ (i : ι), β i
i j : ι
y : β j
hji : j = i
⊢ ((of (fun i => γ i) j) ((h j) y)) i = (h i) (((of (fun i => β i) j) y) i)
Tactic:
rw [← hji]
Proof state after:
case pos
ι : Type u_1
inst✝⁵ : DecidableEq ι
R : Type u_2
inst✝⁴ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝³ : (i : ι) → AddCommMonoid (β i)
inst✝² : (i : ι) → AddCommMonoid (γ i)
inst✝¹ : (i : ι) → Module R (β i)
inst✝ : (i : ι) → Module R (γ i)
h : (i : ι) → β i →ₗ[R] γ i
x : ⨁ (i : ι), β i
i j : ι
y : β j
hji : j = i
⊢ ((of (fun i => γ i) j) ((h j) y)) j = (h j) (((of (fun i => β i) j) y) j)
Theorem: DirectSum.lmap'_apply
Proof state before:
case pos
ι : Type u_1
inst✝⁵ : DecidableEq ι
R : Type u_2
inst✝⁴ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝³ : (i : ι) → AddCommMonoid (β i)
inst✝² : (i : ι) → AddCommMonoid (γ i)
inst✝¹ : (i : ι) → Module R (β i)
inst✝ : (i : ι) → Module R (γ i)
h : (i : ι) → β i →ₗ[R] γ i
x : ⨁ (i : ι), β i
i j : ι
y : β j
hji : j = i
⊢ ((of (fun i => γ i) j) ((h j) y)) j = (h j) (((of (fun i => β i) j) y) j)
Tactic:
simp only [of_eq_same]
Proof state after:
no goals
Theorem: DirectSum.lmap'_apply
Proof state before:
case neg
ι : Type u_1
inst✝⁵ : DecidableEq ι
R : Type u_2
inst✝⁴ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝³ : (i : ι) → AddCommMonoid (β i)
inst✝² : (i : ι) → AddCommMonoid (γ i)
inst✝¹ : (i : ι) → Module R (β i)
inst✝ : (i : ι) → Module R (γ i)
h : (i : ι) → β i →ₗ[R] γ i
x : ⨁ (i : ι), β i
i j : ι
y : β j
hji : ¬j = i
⊢ ((of (fun i => γ i) j) ((h j) y)) i = (h i) (((of (fun i => β i) j) y) i)
Tactic:
simp only [of_eq_of_ne _ j i _ hji, map_zero]
Proof state after:
no goals
Theorem: DirectSum.toModule_comp_lmap'_eq
Proof state before:
ι : Type u_1
inst✝⁷ : DecidableEq ι
R : Type u_2
inst✝⁶ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
δ : Type u_5
inst✝⁵ : (i : ι) → AddCommMonoid (β i)
inst✝⁴ : (i : ι) → AddCommMonoid (γ i)
inst✝³ : AddCommMonoid δ
inst✝² : (i : ι) → Module R (β i)
inst✝¹ : (i : ι) → Module R (γ i)
inst✝ : Module R δ
h : (i : ι) → β i →ₗ[R] γ i
f : (i : ι) → γ i →ₗ[R] δ
x : ⨁ (i : ι), β i
⊢ (toModule R ι δ f) ((lmap' h) x) = (toModule R ι δ fun i => f i ∘ₗ h i) x
Tactic:
rw [← LinearMap.comp_apply]
Proof state after:
ι : Type u_1
inst✝⁷ : DecidableEq ι
R : Type u_2
inst✝⁶ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
δ : Type u_5
inst✝⁵ : (i : ι) → AddCommMonoid (β i)
inst✝⁴ : (i : ι) → AddCommMonoid (γ i)
inst✝³ : AddCommMonoid δ
inst✝² : (i : ι) → Module R (β i)
inst✝¹ : (i : ι) → Module R (γ i)
inst✝ : Module R δ
h : (i : ι) → β i →ₗ[R] γ i
f : (i : ι) → γ i →ₗ[R] δ
x : ⨁ (i : ι), β i
⊢ (toModule R ι δ f ∘ₗ lmap' h) x = (toModule R ι δ fun i => f i ∘ₗ h i) x
Theorem: DirectSum.toModule_comp_lmap'_eq
Proof state before:
ι : Type u_1
inst✝⁷ : DecidableEq ι
R : Type u_2
inst✝⁶ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
δ : Type u_5
inst✝⁵ : (i : ι) → AddCommMonoid (β i)
inst✝⁴ : (i : ι) → AddCommMonoid (γ i)
inst✝³ : AddCommMonoid δ
inst✝² : (i : ι) → Module R (β i)
inst✝¹ : (i : ι) → Module R (γ i)
inst✝ : Module R δ
h : (i : ι) → β i →ₗ[R] γ i
f : (i : ι) → γ i →ₗ[R] δ
x : ⨁ (i : ι), β i
⊢ (toModule R ι δ f ∘ₗ lmap' h) x = (toModule R ι δ fun i => f i ∘ₗ h i) x
Tactic:
apply LinearMap.congr_fun
Proof state after:
case h
ι : Type u_1
inst✝⁷ : DecidableEq ι
R : Type u_2
inst✝⁶ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
δ : Type u_5
inst✝⁵ : (i : ι) → AddCommMonoid (β i)
inst✝⁴ : (i : ι) → AddCommMonoid (γ i)
inst✝³ : AddCommMonoid δ
inst✝² : (i : ι) → Module R (β i)
inst✝¹ : (i : ι) → Module R (γ i)
inst✝ : Module R δ
h : (i : ι) → β i →ₗ[R] γ i
f : (i : ι) → γ i →ₗ[R] δ
x : ⨁ (i : ι), β i
⊢ toModule R ι δ f ∘ₗ lmap' h = toModule R ι δ fun i => f i ∘ₗ h i
Theorem: DirectSum.toModule_comp_lmap'_eq
Proof state before:
case h
ι : Type u_1
inst✝⁷ : DecidableEq ι
R : Type u_2
inst✝⁶ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
δ : Type u_5
inst✝⁵ : (i : ι) → AddCommMonoid (β i)
inst✝⁴ : (i : ι) → AddCommMonoid (γ i)
inst✝³ : AddCommMonoid δ
inst✝² : (i : ι) → Module R (β i)
inst✝¹ : (i : ι) → Module R (γ i)
inst✝ : Module R δ
h : (i : ι) → β i →ₗ[R] γ i
f : (i : ι) → γ i →ₗ[R] δ
x : ⨁ (i : ι), β i
⊢ toModule R ι δ f ∘ₗ lmap' h = toModule R ι δ fun i => f i ∘ₗ h i
Tactic:
ext i y
Proof state after:
case h.H.h
ι : Type u_1
inst✝⁷ : DecidableEq ι
R : Type u_2
inst✝⁶ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
δ : Type u_5
inst✝⁵ : (i : ι) → AddCommMonoid (β i)
inst✝⁴ : (i : ι) → AddCommMonoid (γ i)
inst✝³ : AddCommMonoid δ
inst✝² : (i : ι) → Module R (β i)
inst✝¹ : (i : ι) → Module R (γ i)
inst✝ : Module R δ
h : (i : ι) → β i →ₗ[R] γ i
f : (i : ι) → γ i →ₗ[R] δ
x : ⨁ (i : ι), β i
i : ι
y : β i
⊢ ((toModule R ι δ f ∘ₗ lmap' h) ∘ₗ lof R ι (fun i => β i) i) y =
    ((toModule R ι δ fun i => f i ∘ₗ h i) ∘ₗ lof R ι (fun i => β i) i) y