internlm/Lean-Github huggingface dataset:
Theorem: DividedPowerAlgebra.liftAlgHom_unique
Proof state before:
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
I : Ideal A
hI : DividedPowers I
φ : M →ₗ[R] A
hφ : ∀ (m : M), φ m ∈ I
f : DividedPowerAlgebra R M →ₐ[R] A
hf : ∀ (n : ℕ) (m : M), f (dp R n m) = hI.dpow n (φ m)
⊢ f = lift hI φ hφ
Tactic:
apply DividedPowerAlgebra.ext
Proof state after:
case h
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
I : Ideal A
hI : DividedPowers I
φ : M →ₗ[R] A
hφ : ∀ (m : M), φ m ∈ I
f : DividedPowerAlgebra R M →ₐ[R] A
hf : ∀ (n : ℕ) (m : M), f (dp R n m) = hI.dpow n (φ m)
⊢ ∀ (n : ℕ) (m : M), f (dp R n m) = (lift hI φ hφ) (dp R n m)
Theorem: DividedPowerAlgebra.liftAlgHom_unique
Proof state before:
case h
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
I : Ideal A
hI : DividedPowers I
φ : M →ₗ[R] A
hφ : ∀ (m : M), φ m ∈ I
f : DividedPowerAlgebra R M →ₐ[R] A
hf : ∀ (n : ℕ) (m : M), f (dp R n m) = hI.dpow n (φ m)
⊢ ∀ (n : ℕ) (m : M), f (dp R n m) = (lift hI φ hφ) (dp R n m)
Tactic:
intro n m
Proof state after:
case h
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
I : Ideal A
hI : DividedPowers I
φ : M →ₗ[R] A
hφ : ∀ (m : M), φ m ∈ I
f : DividedPowerAlgebra R M →ₐ[R] A
hf : ∀ (n : ℕ) (m : M), f (dp R n m) = hI.dpow n (φ m)
n : ℕ
m : M
⊢ f (dp R n m) = (lift hI φ hφ) (dp R n m)
Theorem: DividedPowerAlgebra.liftAlgHom_unique
Proof state before:
case h
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
I : Ideal A
hI : DividedPowers I
φ : M →ₗ[R] A
hφ : ∀ (m : M), φ m ∈ I
f : DividedPowerAlgebra R M →ₐ[R] A
hf : ∀ (n : ℕ) (m : M), f (dp R n m) = hI.dpow n (φ m)
n : ℕ
m : M
⊢ f (dp R n m) = (lift hI φ hφ) (dp R n m)
Tactic:
rw [liftAlgHom_apply_dp, hf]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.LinearMap.dp_smul
Proof state before:
R : Type u_1
M : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
S : Type u_3
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
N : Type u_4
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
r : R
n : ℕ
a : M
⊢ dp S n (f (r • a)) = r ^ n • dp S n (f a)
Tactic:
rw [f.map_smul, algebra_compatible_smul S r (f a)]
Proof state after:
R : Type u_1
M : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
S : Type u_3
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
N : Type u_4
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
r : R
n : ℕ
a : M
⊢ dp S n ((algebraMap R S) r • f a) = r ^ n • dp S n (f a)
Theorem: DividedPowerAlgebra.LinearMap.dp_smul
Proof state before:
R : Type u_1
M : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
S : Type u_3
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
N : Type u_4
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
r : R
n : ℕ
a : M
⊢ dp S n ((algebraMap R S) r • f a) = r ^ n • dp S n (f a)
Tactic:
rw [DividedPowerAlgebra.dp_smul S ((algebraMap R S) r) n (f a)]
Proof state after:
R : Type u_1
M : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
S : Type u_3
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
N : Type u_4
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
r : R
n : ℕ
a : M
⊢ (algebraMap R S) r ^ n • dp S n (f a) = r ^ n • dp S n (f a)
Theorem: DividedPowerAlgebra.LinearMap.dp_smul
Proof state before:
R : Type u_1
M : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
S : Type u_3
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
N : Type u_4
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
r : R
n : ℕ
a : M
⊢ (algebraMap R S) r ^ n • dp S n (f a) = r ^ n • dp S n (f a)
Tactic:
rw [← map_pow, algebraMap_smul]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.LinearMap.dp_add
Proof state before:
R : Type u_1
M : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
S : Type u_3
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
N : Type u_4
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
n : ℕ
a b : M
⊢ dp S n (f (a + b)) = ∑ k ∈ antidiagonal n, dp S k.1 (f a) * dp S k.2 (f b)
Tactic:
rw [map_add, DividedPowerAlgebra.dp_add]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.LinearMap.liftAlgHom_apply
Proof state before:
R : Type u_1
M : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
S : Type u_3
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
N : Type u_4
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
p : MvPolynomial (ℕ × M) R
⊢ (lift R S f) (mk p) = (aeval fun nm => dp S nm.1 (f nm.2)) p
Tactic:
rw [LinearMap.lift, lift'AlgHom_apply]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.LinearMap.liftAlgHom_dp
Proof state before:
R : Type u_1
M : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
S : Type u_3
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
N : Type u_4
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
n : ℕ
a : M
⊢ (lift R S f) (dp R n a) = dp S n (f a)
Tactic:
rw [LinearMap.lift, lift'AlgHom_apply_dp]
Proof state after:
no goals
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)
F : ι → Type u_5
inst✝¹ : (i : ι) → FunLike (F i) (β i) (γ i)
inst✝ : ∀ (i : ι), AddMonoidHomClass (F i) (β i) (γ i)
h : (i : ι) → F i
i : ι
x : β i
⊢ (map h) ((of β i) x) = (of γ i) ((h i) x)
Tactic:
simp only [map, toAddMonoid_of, AddMonoidHom.coe_comp, AddMonoidHom.coe_coe]
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)
F : ι → Type u_5
inst✝¹ : (i : ι) → FunLike (F i) (β i) (γ i)
inst✝ : ∀ (i : ι), AddMonoidHomClass (F i) (β i) (γ i)
h : (i : ι) → F 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)
F : ι → Type u_5
inst✝¹ : (i : ι) → FunLike (F i) (β i) (γ i)
inst✝ : ∀ (i : ι), AddMonoidHomClass (F i) (β i) (γ i)
h : (i : ι) → F 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.map_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)
F : ι → Type u_5
inst✝¹ : (i : ι) → FunLike (F i) (β i) (γ i)
inst✝ : ∀ (i : ι), AddMonoidHomClass (F i) (β i) (γ i)
h : (i : ι) → F i
x : DirectSum ι β
i : ι
⊢ ((map h) x) i = (h i) (x i)
Tactic:
let f : DirectSum ι β →+ γ i :=
{ toFun := fun x => map h x i
  map_zero' := by simp only [map_zero, zero_apply]
  map_add' := by simp only [map_add, add_apply, forall_const] }
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)
F : ι → Type u_5
inst✝¹ : (i : ι) → FunLike (F i) (β i) (γ i)
inst✝ : ∀ (i : ι), AddMonoidHomClass (F i) (β i) (γ i)
h : (i : ι) → F i
x : DirectSum ι β
i : ι
f : DirectSum ι β →+ γ i := { toFun := fun x => ((map h) x) i, map_zero' := ⋯, map_add' := ⋯ }
⊢ ((map h) x) i = (h i) (x i)
Theorem: DirectSum.map_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)
F : ι → Type u_5
inst✝¹ : (i : ι) → FunLike (F i) (β i) (γ i)
inst✝ : ∀ (i : ι), AddMonoidHomClass (F i) (β i) (γ i)
h : (i : ι) → F i
x : DirectSum ι β
i : ι
f : DirectSum ι β →+ γ i := { toFun := fun x => ((map h) x) i, map_zero' := ⋯, map_add' := ⋯ }
⊢ ((map h) x) i = (h i) (x i)
Tactic:
let g : DirectSum ι β →+ γ i :=
{ toFun := fun y => h i (y i)
  map_zero' := by simp only [zero_apply, map_zero]
  map_add' := by simp only [add_apply, map_add, forall_const] }
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)
F : ι → Type u_5
inst✝¹ : (i : ι) → FunLike (F i) (β i) (γ i)
inst✝ : ∀ (i : ι), AddMonoidHomClass (F i) (β i) (γ i)
h : (i : ι) → F i
x : DirectSum ι β
i : ι
f : DirectSum ι β →+ γ i := { toFun := fun x => ((map h) x) i, map_zero' := ⋯, map_add' := ⋯ }
g : DirectSum ι β →+ γ i := { toFun := fun y => (h i) (y i), map_zero' := ⋯, map_add' := ⋯ }
⊢ ((map h) x) i = (h i) (x i)
Theorem: DirectSum.map_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)
F : ι → Type u_5
inst✝¹ : (i : ι) → FunLike (F i) (β i) (γ i)
inst✝ : ∀ (i : ι), AddMonoidHomClass (F i) (β i) (γ i)
h : (i : ι) → F i
x : DirectSum ι β
i : ι
f : DirectSum ι β →+ γ i := { toFun := fun x => ((map h) x) i, map_zero' := ⋯, map_add' := ⋯ }
g : DirectSum ι β →+ γ i := { toFun := fun y => (h i) (y i), map_zero' := ⋯, map_add' := ⋯ }
⊢ ((map h) x) i = (h i) (x i)
Tactic:
change f x = g x
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)
F : ι → Type u_5
inst✝¹ : (i : ι) → FunLike (F i) (β i) (γ i)
inst✝ : ∀ (i : ι), AddMonoidHomClass (F i) (β i) (γ i)
h : (i : ι) → F i
x : DirectSum ι β
i : ι
f : DirectSum ι β →+ γ i := { toFun := fun x => ((map h) x) i, map_zero' := ⋯, map_add' := ⋯ }
g : DirectSum ι β →+ γ i := { toFun := fun y => (h i) (y i), map_zero' := ⋯, map_add' := ⋯ }
⊢ f x = g x
Theorem: DirectSum.map_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)
F : ι → Type u_5
inst✝¹ : (i : ι) → FunLike (F i) (β i) (γ i)
inst✝ : ∀ (i : ι), AddMonoidHomClass (F i) (β i) (γ i)
h : (i : ι) → F i
x : DirectSum ι β
i : ι
f : DirectSum ι β →+ γ i := { toFun := fun x => ((map h) x) i, map_zero' := ⋯, map_add' := ⋯ }
g : DirectSum ι β →+ γ i := { toFun := fun y => (h i) (y i), map_zero' := ⋯, map_add' := ⋯ }
⊢ f x = g x
Tactic:
suffices f = g by
  rw [this]
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)
F : ι → Type u_5
inst✝¹ : (i : ι) → FunLike (F i) (β i) (γ i)
inst✝ : ∀ (i : ι), AddMonoidHomClass (F i) (β i) (γ i)
h : (i : ι) → F i
x : DirectSum ι β
i : ι
f : DirectSum ι β →+ γ i := { toFun := fun x => ((map h) x) i, map_zero' := ⋯, map_add' := ⋯ }
g : DirectSum ι β →+ γ i := { toFun := fun y => (h i) (y i), map_zero' := ⋯, map_add' := ⋯ }
⊢ f = g
Theorem: DirectSum.map_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)
F : ι → Type u_5
inst✝¹ : (i : ι) → FunLike (F i) (β i) (γ i)
inst✝ : ∀ (i : ι), AddMonoidHomClass (F i) (β i) (γ i)
h : (i : ι) → F i
x : DirectSum ι β
i : ι
f : DirectSum ι β →+ γ i := { toFun := fun x => ((map h) x) i, map_zero' := ⋯, map_add' := ⋯ }
g : DirectSum ι β →+ γ i := { toFun := fun y => (h i) (y i), map_zero' := ⋯, map_add' := ⋯ }
⊢ f = g
Tactic:
apply addHom_ext
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)
F : ι → Type u_5
inst✝¹ : (i : ι) → FunLike (F i) (β i) (γ i)
inst✝ : ∀ (i : ι), AddMonoidHomClass (F i) (β i) (γ i)
h : (i : ι) → F i
x : DirectSum ι β
i : ι
f : DirectSum ι β →+ γ i := { toFun := fun x => ((map h) x) i, map_zero' := ⋯, map_add' := ⋯ }
g : DirectSum ι β →+ γ i := { toFun := fun y => (h i) (y i), map_zero' := ⋯, map_add' := ⋯ }
⊢ ∀ (i_1 : ι) (y : β i_1), f ((of (fun i => β i) i_1) y) = g ((of (fun i => β i) i_1) y)
Theorem: DirectSum.map_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)
F : ι → Type u_5
inst✝¹ : (i : ι) → FunLike (F i) (β i) (γ i)
inst✝ : ∀ (i : ι), AddMonoidHomClass (F i) (β i) (γ i)
h : (i : ι) → F i
x : DirectSum ι β
i : ι
f : DirectSum ι β →+ γ i := { toFun := fun x => ((map h) x) i, map_zero' := ⋯, map_add' := ⋯ }
g : DirectSum ι β →+ γ i := { toFun := fun y => (h i) (y i), map_zero' := ⋯, map_add' := ⋯ }
⊢ ∀ (i_1 : ι) (y : β i_1), f ((of (fun i => β i) i_1) y) = g ((of (fun i => β i) i_1) y)
Tactic:
intros j y
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)
F : ι → Type u_5
inst✝¹ : (i : ι) → FunLike (F i) (β i) (γ i)
inst✝ : ∀ (i : ι), AddMonoidHomClass (F i) (β i) (γ i)
h : (i : ι) → F i
x : DirectSum ι β
i : ι
f : DirectSum ι β →+ γ i := { toFun := fun x => ((map h) x) i, map_zero' := ⋯, map_add' := ⋯ }
g : DirectSum ι β →+ γ i := { toFun := fun y => (h i) (y i), map_zero' := ⋯, map_add' := ⋯ }
j : ι
y : β j
⊢ f ((of (fun i => β i) j) y) = g ((of (fun i => β i) j) y)
Theorem: DirectSum.map_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)
F : ι → Type u_5
inst✝¹ : (i : ι) → FunLike (F i) (β i) (γ i)
inst✝ : ∀ (i : ι), AddMonoidHomClass (F i) (β i) (γ i)
h : (i : ι) → F i
x : DirectSum ι β
i : ι
f : DirectSum ι β →+ γ i := { toFun := fun x => ((map h) x) i, map_zero' := ⋯, map_add' := ⋯ }
g : DirectSum ι β →+ γ i := { toFun := fun y => (h i) (y i), map_zero' := ⋯, map_add' := ⋯ }
j : ι
y : β j
⊢ f ((of (fun i => β i) j) y) = g ((of (fun i => β i) j) y)
Tactic:
simp only [AddMonoidHom.coe_mk, ZeroHom.coe_mk, map_of, f, g]
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)
F : ι → Type u_5
inst✝¹ : (i : ι) → FunLike (F i) (β i) (γ i)
inst✝ : ∀ (i : ι), AddMonoidHomClass (F i) (β i) (γ i)
h : (i : ι) → F i
x : DirectSum ι β
i : ι
f : DirectSum ι β →+ γ i := { toFun := fun x => ((map h) x) i, map_zero' := ⋯, map_add' := ⋯ }
g : DirectSum ι β →+ γ i := { toFun := fun y => (h i) (y i), map_zero' := ⋯, map_add' := ⋯ }
j : ι
y : β j
⊢ ((of (fun i => γ i) j) ((h j) y)) i = (h i) (((of (fun i => β i) j) y) i)
Theorem: DirectSum.map_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)
F : ι → Type u_5
inst✝¹ : (i : ι) → FunLike (F i) (β i) (γ i)
inst✝ : ∀ (i : ι), AddMonoidHomClass (F i) (β i) (γ i)
h : (i : ι) → F i
x : DirectSum ι β
i : ι
f : DirectSum ι β →+ γ i := { toFun := fun x => ((map h) x) i, map_zero' := ⋯, map_add' := ⋯ }
g : DirectSum ι β →+ γ i := { toFun := fun y => (h i) (y i), map_zero' := ⋯, map_add' := ⋯ }
j : ι
y : β j
⊢ ((of (fun i => γ i) j) ((h j) y)) i = (h i) (((of (fun i => β i) j) y) i)
Tactic:
by_cases hj : 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)
F : ι → Type u_5
inst✝¹ : (i : ι) → FunLike (F i) (β i) (γ i)
inst✝ : ∀ (i : ι), AddMonoidHomClass (F i) (β i) (γ i)
h : (i : ι) → F i
x : DirectSum ι β
i : ι
f : DirectSum ι β →+ γ i := { toFun := fun x => ((map h) x) i, map_zero' := ⋯, map_add' := ⋯ }
g : DirectSum ι β →+ γ i := { toFun := fun y => (h i) (y i), map_zero' := ⋯, map_add' := ⋯ }
j : ι
y : β j
hj : 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)
F : ι → Type u_5
inst✝¹ : (i : ι) → FunLike (F i) (β i) (γ i)
inst✝ : ∀ (i : ι), AddMonoidHomClass (F i) (β i) (γ i)
h : (i : ι) → F i
x : DirectSum ι β
i : ι
f : DirectSum ι β →+ γ i := { toFun := fun x => ((map h) x) i, map_zero' := ⋯, map_add' := ⋯ }
g : DirectSum ι β →+ γ i := { toFun := fun y => (h i) (y i), map_zero' := ⋯, map_add' := ⋯ }
j : ι
y : β j
hj : ¬j = i
⊢ ((of (fun i => γ i) j) ((h j) y)) i = (h i) (((of (fun i => β i) j) y) i)
Theorem: DirectSum.map_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)
F : ι → Type u_5
inst✝¹ : (i : ι) → FunLike (F i) (β i) (γ i)
inst✝ : ∀ (i : ι), AddMonoidHomClass (F i) (β i) (γ i)
h : (i : ι) → F i
x : DirectSum ι β
i : ι
⊢ (fun x => ((map h) x) i) 0 = 0
Tactic:
simp only [map_zero, zero_apply]
Proof state after:
no goals
Theorem: DirectSum.map_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)
F : ι → Type u_5
inst✝¹ : (i : ι) → FunLike (F i) (β i) (γ i)
inst✝ : ∀ (i : ι), AddMonoidHomClass (F i) (β i) (γ i)
h : (i : ι) → F i
x : DirectSum ι β
i : ι
⊢ ∀ (x y : DirectSum ι β),
    { toFun := fun x => ((map h) x) i, map_zero' := ⋯ }.toFun (x + y) =
      { toFun := fun x => ((map h) x) i, map_zero' := ⋯ }.toFun x +
        { toFun := fun x => ((map h) x) i, map_zero' := ⋯ }.toFun y
Tactic:
simp only [map_add, add_apply, forall_const]
Proof state after:
no goals
Theorem: DirectSum.map_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)
F : ι → Type u_5
inst✝¹ : (i : ι) → FunLike (F i) (β i) (γ i)
inst✝ : ∀ (i : ι), AddMonoidHomClass (F i) (β i) (γ i)
h : (i : ι) → F i
x : DirectSum ι β
i : ι
f : DirectSum ι β →+ γ i := { toFun := fun x => ((map h) x) i, map_zero' := ⋯, map_add' := ⋯ }
⊢ (fun y => (h i) (y i)) 0 = 0
Tactic:
simp only [zero_apply, map_zero]
Proof state after:
no goals
Theorem: DirectSum.map_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)
F : ι → Type u_5
inst✝¹ : (i : ι) → FunLike (F i) (β i) (γ i)
inst✝ : ∀ (i : ι), AddMonoidHomClass (F i) (β i) (γ i)
h : (i : ι) → F i
x : DirectSum ι β
i : ι
f : DirectSum ι β →+ γ i := { toFun := fun x => ((map h) x) i, map_zero' := ⋯, map_add' := ⋯ }
⊢ ∀ (x y : DirectSum ι β),
    { toFun := fun y => (h i) (y i), map_zero' := ⋯ }.toFun (x + y) =
      { toFun := fun y => (h i) (y i), map_zero' := ⋯ }.toFun x +
        { toFun := fun y => (h i) (y i), map_zero' := ⋯ }.toFun y
Tactic:
simp only [add_apply, map_add, forall_const]
Proof state after:
no goals
Theorem: DirectSum.map_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)
F : ι → Type u_5
inst✝¹ : (i : ι) → FunLike (F i) (β i) (γ i)
inst✝ : ∀ (i : ι), AddMonoidHomClass (F i) (β i) (γ i)
h : (i : ι) → F i
x : DirectSum ι β
i : ι
f : DirectSum ι β →+ γ i := { toFun := fun x => ((map h) x) i, map_zero' := ⋯, map_add' := ⋯ }
g : DirectSum ι β →+ γ i := { toFun := fun y => (h i) (y i), map_zero' := ⋯, map_add' := ⋯ }
this : f = g
⊢ f x = g x
Tactic:
rw [this]
Proof state after:
no goals
Theorem: DirectSum.map_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)
F : ι → Type u_5
inst✝¹ : (i : ι) → FunLike (F i) (β i) (γ i)
inst✝ : ∀ (i : ι), AddMonoidHomClass (F i) (β i) (γ i)
h : (i : ι) → F i
x : DirectSum ι β
i : ι
f : DirectSum ι β →+ γ i := { toFun := fun x => ((map h) x) i, map_zero' := ⋯, map_add' := ⋯ }
g : DirectSum ι β →+ γ i := { toFun := fun y => (h i) (y i), map_zero' := ⋯, map_add' := ⋯ }
j : ι
y : β j
hj : j = i
⊢ ((of (fun i => γ i) j) ((h j) y)) i = (h i) (((of (fun i => β i) j) y) i)
Tactic:
rw [← hj]
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)
F : ι → Type u_5
inst✝¹ : (i : ι) → FunLike (F i) (β i) (γ i)
inst✝ : ∀ (i : ι), AddMonoidHomClass (F i) (β i) (γ i)
h : (i : ι) → F i
x : DirectSum ι β
i : ι
f : DirectSum ι β →+ γ i := { toFun := fun x => ((map h) x) i, map_zero' := ⋯, map_add' := ⋯ }
g : DirectSum ι β →+ γ i := { toFun := fun y => (h i) (y i), map_zero' := ⋯, map_add' := ⋯ }
j : ι
y : β j
hj : j = i
⊢ ((of (fun i => γ i) j) ((h j) y)) j = (h j) (((of (fun i => β i) j) y) j)
Theorem: DirectSum.map_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)
F : ι → Type u_5
inst✝¹ : (i : ι) → FunLike (F i) (β i) (γ i)
inst✝ : ∀ (i : ι), AddMonoidHomClass (F i) (β i) (γ i)
h : (i : ι) → F i
x : DirectSum ι β
i : ι
f : DirectSum ι β →+ γ i := { toFun := fun x => ((map h) x) i, map_zero' := ⋯, map_add' := ⋯ }
g : DirectSum ι β →+ γ i := { toFun := fun y => (h i) (y i), map_zero' := ⋯, map_add' := ⋯ }
j : ι
y : β j
hj : 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.map_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)
F : ι → Type u_5
inst✝¹ : (i : ι) → FunLike (F i) (β i) (γ i)
inst✝ : ∀ (i : ι), AddMonoidHomClass (F i) (β i) (γ i)
h : (i : ι) → F i
x : DirectSum ι β
i : ι
f : DirectSum ι β →+ γ i := { toFun := fun x => ((map h) x) i, map_zero' := ⋯, map_add' := ⋯ }
g : DirectSum ι β →+ γ i := { toFun := fun y => (h i) (y i), map_zero' := ⋯, map_add' := ⋯ }
j : ι
y : β j
hj : ¬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 _ hj, map_zero]
Proof state after:
no goals