[GOAL]
I : Type u
f : I → Type v
x y : (i : I) → f i
i✝ : I
α : Type u_1
inst✝² : (i : I) → SMul α (f i)
inst✝¹ : ∀ (i : I), Nonempty (f i)
i : I
inst✝ : FaithfulSMul α (f i)
m₁✝ m₂✝ : α
h : ∀ (a : (i : I) → f i), m₁✝ • a = m₂✝ • a
a : f i
⊢ m₁✝ • a = m₂✝ • a
[PROOFSTEP]
classical
have := congr_fun (h <| Function.update (fun j => Classical.choice (‹∀ i, Nonempty (f i)› j)) i a) i
simpa using this
[GOAL]
I : Type u
f : I → Type v
x y : (i : I) → f i
i✝ : I
α : Type u_1
inst✝² : (i : I) → SMul α (f i)
inst✝¹ : ∀ (i : I), Nonempty (f i)
i : I
inst✝ : FaithfulSMul α (f i)
m₁✝ m₂✝ : α
h : ∀ (a : (i : I) → f i), m₁✝ • a = m₂✝ • a
a : f i
⊢ m₁✝ • a = m₂✝ • a
[PROOFSTEP]
have := congr_fun (h <| Function.update (fun j => Classical.choice (‹∀ i, Nonempty (f i)› j)) i a) i
[GOAL]
I : Type u
f : I → Type v
x y : (i : I) → f i
i✝ : I
α : Type u_1
inst✝² : (i : I) → SMul α (f i)
inst✝¹ : ∀ (i : I), Nonempty (f i)
i : I
inst✝ : FaithfulSMul α (f i)
m₁✝ m₂✝ : α
h : ∀ (a : (i : I) → f i), m₁✝ • a = m₂✝ • a
a : f i
this :
  (m₁✝ • Function.update (fun j => Classical.choice (_ : Nonempty (f j))) i a) i =
    (m₂✝ • Function.update (fun j => Classical.choice (_ : Nonempty (f j))) i a) i
⊢ m₁✝ • a = m₂✝ • a
[PROOFSTEP]
simpa using this
[GOAL]
I : Type u
f : I → Type v
x y : (i : I) → f i
i : I
g : I → Type u_1
n : (i : I) → Zero (g i)
inst✝ : (i : I) → SMulZeroClass (f i) (g i)
⊢ ∀ (a : (i : I) → f i), a • 0 = 0
[PROOFSTEP]
intros
[GOAL]
I : Type u
f : I → Type v
x y : (i : I) → f i
i : I
g : I → Type u_1
n : (i : I) → Zero (g i)
inst✝ : (i : I) → SMulZeroClass (f i) (g i)
a✝ : (i : I) → f i
⊢ a✝ • 0 = 0
[PROOFSTEP]
ext x
[GOAL]
case h
I : Type u
f : I → Type v
x✝ y : (i : I) → f i
i : I
g : I → Type u_1
n : (i : I) → Zero (g i)
inst✝ : (i : I) → SMulZeroClass (f i) (g i)
a✝ : (i : I) → f i
x : I
⊢ (a✝ • 0) x = OfNat.ofNat 0 x
[PROOFSTEP]
exact smul_zero _
[GOAL]
I : Type u
f : I → Type v
x y : (i : I) → f i
i : I
g : I → Type u_1
n : (i : I) → AddZeroClass (g i)
inst✝ : (i : I) → DistribSMul (f i) (g i)
⊢ ∀ (a : (i : I) → f i), a • 0 = 0
[PROOFSTEP]
intros
[GOAL]
I : Type u
f : I → Type v
x y : (i : I) → f i
i : I
g : I → Type u_1
n : (i : I) → AddZeroClass (g i)
inst✝ : (i : I) → DistribSMul (f i) (g i)
a✝ : (i : I) → f i
⊢ a✝ • 0 = 0
[PROOFSTEP]
ext x
[GOAL]
case h
I : Type u
f : I → Type v
x✝ y : (i : I) → f i
i : I
g : I → Type u_1
n : (i : I) → AddZeroClass (g i)
inst✝ : (i : I) → DistribSMul (f i) (g i)
a✝ : (i : I) → f i
x : I
⊢ (a✝ • 0) x = OfNat.ofNat 0 x
[PROOFSTEP]
exact smul_zero _
[GOAL]
I : Type u
f : I → Type v
x y : (i : I) → f i
i : I
g : I → Type u_1
n : (i : I) → AddZeroClass (g i)
inst✝ : (i : I) → DistribSMul (f i) (g i)
⊢ ∀ (a : (i : I) → f i) (x y : (i : I) → g i), a • (x + y) = a • x + a • y
[PROOFSTEP]
intros
[GOAL]
I : Type u
f : I → Type v
x y : (i : I) → f i
i : I
g : I → Type u_1
n : (i : I) → AddZeroClass (g i)
inst✝ : (i : I) → DistribSMul (f i) (g i)
a✝ : (i : I) → f i
x✝ y✝ : (i : I) → g i
⊢ a✝ • (x✝ + y✝) = a✝ • x✝ + a✝ • y✝
[PROOFSTEP]
ext x
[GOAL]
case h
I : Type u
f : I → Type v
x✝¹ y : (i : I) → f i
i : I
g : I → Type u_1
n : (i : I) → AddZeroClass (g i)
inst✝ : (i : I) → DistribSMul (f i) (g i)
a✝ : (i : I) → f i
x✝ y✝ : (i : I) → g i
x : I
⊢ (a✝ • (x✝ + y✝)) x = (a✝ • x✝ + a✝ • y✝) x
[PROOFSTEP]
exact smul_add _ _ _
[GOAL]
I : Type u
f : I → Type v
x y : (i : I) → f i
i : I
g : I → Type u_1
m : (i : I) → Monoid (f i)
n : (i : I) → Monoid (g i)
inst✝ : (i : I) → MulDistribMulAction (f i) (g i)
⊢ ∀ (r : (i : I) → f i) (x y : (i : I) → g i), r • (x * y) = r • x * r • y
[PROOFSTEP]
intros
[GOAL]
I : Type u
f : I → Type v
x y : (i : I) → f i
i : I
g : I → Type u_1
m : (i : I) → Monoid (f i)
n : (i : I) → Monoid (g i)
inst✝ : (i : I) → MulDistribMulAction (f i) (g i)
r✝ : (i : I) → f i
x✝ y✝ : (i : I) → g i
⊢ r✝ • (x✝ * y✝) = r✝ • x✝ * r✝ • y✝
[PROOFSTEP]
ext x
[GOAL]
case h
I : Type u
f : I → Type v
x✝¹ y : (i : I) → f i
i : I
g : I → Type u_1
m : (i : I) → Monoid (f i)
n : (i : I) → Monoid (g i)
inst✝ : (i : I) → MulDistribMulAction (f i) (g i)
r✝ : (i : I) → f i
x✝ y✝ : (i : I) → g i
x : I
⊢ (r✝ • (x✝ * y✝)) x = (r✝ • x✝ * r✝ • y✝) x
[PROOFSTEP]
apply smul_mul'
[GOAL]
I : Type u
f : I → Type v
x y : (i : I) → f i
i : I
g : I → Type u_1
m : (i : I) → Monoid (f i)
n : (i : I) → Monoid (g i)
inst✝ : (i : I) → MulDistribMulAction (f i) (g i)
⊢ ∀ (r : (i : I) → f i), r • 1 = 1
[PROOFSTEP]
intros
[GOAL]
I : Type u
f : I → Type v
x y : (i : I) → f i
i : I
g : I → Type u_1
m : (i : I) → Monoid (f i)
n : (i : I) → Monoid (g i)
inst✝ : (i : I) → MulDistribMulAction (f i) (g i)
r✝ : (i : I) → f i
⊢ r✝ • 1 = 1
[PROOFSTEP]
ext x
[GOAL]
case h
I : Type u
f : I → Type v
x✝ y : (i : I) → f i
i : I
g : I → Type u_1
m : (i : I) → Monoid (f i)
n : (i : I) → Monoid (g i)
inst✝ : (i : I) → MulDistribMulAction (f i) (g i)
r✝ : (i : I) → f i
x : I
⊢ (r✝ • 1) x = OfNat.ofNat 1 x
[PROOFSTEP]
apply smul_one
[GOAL]
I : Type u
f✝ : I → Type v
x✝ y : (i : I) → f✝ i
i : I
R : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : SMul R γ
r : R
f : α → β
g : α → γ
e : β → γ
x : β
⊢ extend f (r • g) (r • e) x = (r • extend f g e) x
[PROOFSTEP]
haveI : Decidable (∃ a : α, f a = x) := Classical.propDecidable _
[GOAL]
I : Type u
f✝ : I → Type v
x✝ y : (i : I) → f✝ i
i : I
R : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : SMul R γ
r : R
f : α → β
g : α → γ
e : β → γ
x : β
this : Decidable (∃ a, f a = x)
⊢ extend f (r • g) (r • e) x = (r • extend f g e) x
[PROOFSTEP]
rw [extend_def, Pi.smul_apply, Pi.smul_apply, extend_def]
[GOAL]
I : Type u
f✝ : I → Type v
x✝ y : (i : I) → f✝ i
i : I
R : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : SMul R γ
r : R
f : α → β
g : α → γ
e : β → γ
x : β
this : Decidable (∃ a, f a = x)
⊢ (if h : ∃ a, f a = x then (r • g) (Classical.choose h) else r • e x) =
    r • if h : ∃ a, f a = x then g (Classical.choose h) else e x
[PROOFSTEP]
split_ifs
[GOAL]
case pos
I : Type u
f✝ : I → Type v
x✝ y : (i : I) → f✝ i
i : I
R : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : SMul R γ
r : R
f : α → β
g : α → γ
e : β → γ
x : β
this : Decidable (∃ a, f a = x)
h✝ : ∃ a, f a = x
⊢ (r • g) (Classical.choose h✝) = r • g (Classical.choose h✝)
[PROOFSTEP]
rfl
  -- convert (apply_dite (fun c : γ => r • c) _ _ _).symm
[GOAL]
case neg
I : Type u
f✝ : I → Type v
x✝ y : (i : I) → f✝ i
i : I
R : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : SMul R γ
r : R
f : α → β
g : α → γ
e : β → γ
x : β
this : Decidable (∃ a, f a = x)
h✝ : ¬∃ a, f a = x
⊢ r • e x = r • e x
[PROOFSTEP]
rfl
  -- convert (apply_dite (fun c : γ => r • c) _ _ _).symm
