case h
k : Type u_1
V1 : Type u_2
P1 : Type ?u.585564
V2 : Type u_3
P2 : Type ?u.585570
V3 : Type ?u.585573
P3 : Type ?u.585576
V4 : Type ?u.585579
P4 : Type ?u.585582
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
f : V1 →ᵃ[k] V2
x : V1
⊢ ↑f x = (↑f.linear + fun x => ↑f 0) x
k : Type u_1
V1 : Type u_2
P1 : Type ?u.585564
V2 : Type u_3
P2 : Type ?u.585570
V3 : Type ?u.585573
P3 : Type ?u.585576
V4 : Type ?u.585579
P4 : Type ?u.585582
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
f : V1 →ᵃ[k] V2
⊢ ↑f = ↑f.linear + fun x => ↑f 0
ext x
no goals
case h
k : Type u_1
V1 : Type u_2
P1 : Type ?u.585564
V2 : Type u_3
P2 : Type ?u.585570
V3 : Type ?u.585573
P3 : Type ?u.585576
V4 : Type ?u.585579
P4 : Type ?u.585582
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
f : V1 →ᵃ[k] V2
x : V1
⊢ ↑f x = (↑f.linear + fun x => ↑f 0) x
calc
  f x = f.linear x +ᵥ f 0 := by rw [← f.map_vadd, vadd_eq_add, add_zero]
  _ = (f.linear + fun _ : V1 => f 0) x := rfl
no goals
k : Type u_1
V1 : Type u_2
P1 : Type ?u.585564
V2 : Type u_3
P2 : Type ?u.585570
V3 : Type ?u.585573
P3 : Type ?u.585576
V4 : Type ?u.585579
P4 : Type ?u.585582
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
f : V1 →ᵃ[k] V2
x : V1
⊢ ↑f x = ↑f.linear x +ᵥ ↑f 0
rw [← f.map_vadd, vadd_eq_add, add_zero]