case mk
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module R V
inst✝⁵ : TopologicalSpace P
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup W
inst✝² : Module R W
inst✝¹ : TopologicalSpace Q
inst✝ : AddTorsor W Q
g : P →A[R] Q
toAffineMap✝ : P →ᵃ[R] Q
cont✝ : Continuous toAffineMap✝.toFun
h : { toAffineMap := toAffineMap✝, cont := cont✝ }.toAffineMap = g.toAffineMap
⊢ { toAffineMap := toAffineMap✝, cont := cont✝ } = g
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module R V
inst✝⁵ : TopologicalSpace P
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup W
inst✝² : Module R W
inst✝¹ : TopologicalSpace Q
inst✝ : AddTorsor W Q
f g : P →A[R] Q
h : f.toAffineMap = g.toAffineMap
⊢ f = g
cases f
case mk.mk
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module R V
inst✝⁵ : TopologicalSpace P
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup W
inst✝² : Module R W
inst✝¹ : TopologicalSpace Q
inst✝ : AddTorsor W Q
toAffineMap✝¹ : P →ᵃ[R] Q
cont✝¹ : Continuous toAffineMap✝¹.toFun
toAffineMap✝ : P →ᵃ[R] Q
cont✝ : Continuous toAffineMap✝.toFun
h :
  { toAffineMap := toAffineMap✝¹, cont := cont✝¹ }.toAffineMap =
    { toAffineMap := toAffineMap✝, cont := cont✝ }.toAffineMap
⊢ { toAffineMap := toAffineMap✝¹, cont := cont✝¹ } = { toAffineMap := toAffineMap✝, cont := cont✝ }
case mk
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module R V
inst✝⁵ : TopologicalSpace P
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup W
inst✝² : Module R W
inst✝¹ : TopologicalSpace Q
inst✝ : AddTorsor W Q
g : P →A[R] Q
toAffineMap✝ : P →ᵃ[R] Q
cont✝ : Continuous toAffineMap✝.toFun
h : { toAffineMap := toAffineMap✝, cont := cont✝ }.toAffineMap = g.toAffineMap
⊢ { toAffineMap := toAffineMap✝, cont := cont✝ } = g
cases g
no goals
case mk.mk
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module R V
inst✝⁵ : TopologicalSpace P
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup W
inst✝² : Module R W
inst✝¹ : TopologicalSpace Q
inst✝ : AddTorsor W Q
toAffineMap✝¹ : P →ᵃ[R] Q
cont✝¹ : Continuous toAffineMap✝¹.toFun
toAffineMap✝ : P →ᵃ[R] Q
cont✝ : Continuous toAffineMap✝.toFun
h :
  { toAffineMap := toAffineMap✝¹, cont := cont✝¹ }.toAffineMap =
    { toAffineMap := toAffineMap✝, cont := cont✝ }.toAffineMap
⊢ { toAffineMap := toAffineMap✝¹, cont := cont✝¹ } = { toAffineMap := toAffineMap✝, cont := cont✝ }
congr