no goals
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
classical
  have :=
    congr_fun (h <| Function.update (fun j => Classical.choice (‹∀ i, Nonempty (f i)› j)) i a)
      i
  simpa using this
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
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
have :=
  congr_fun (h <| Function.update (fun j => Classical.choice (‹∀ i, Nonempty (f i)› j)) i a)
    i
no goals
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
simpa using this