k : Type u_2
V1 : Type u_3
P1 : Type u_1
V2 : Type ?u.538087
P2 : Type ?u.538090
V3 : Type ?u.538093
P3 : Type ?u.538096
V4 : Type ?u.538099
P4 : Type ?u.538102
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
p₀ p₁ : P1
c : k
⊢ ↑(lineMap p₁ p₀) (↑(lineMap 1 0) (1 - c)) = ↑(lineMap p₁ p₀) c
k : Type u_2
V1 : Type u_3
P1 : Type u_1
V2 : Type ?u.538087
P2 : Type ?u.538090
V3 : Type ?u.538093
P3 : Type ?u.538096
V4 : Type ?u.538099
P4 : Type ?u.538102
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
p₀ p₁ : P1
c : k
⊢ ↑(lineMap p₀ p₁) (1 - c) = ↑(lineMap p₁ p₀) c
rw [lineMap_symm p₀, comp_apply]
case h.e_6.h
k : Type u_2
V1 : Type u_3
P1 : Type u_1
V2 : Type ?u.538087
P2 : Type ?u.538090
V3 : Type ?u.538093
P3 : Type ?u.538096
V4 : Type ?u.538099
P4 : Type ?u.538102
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
p₀ p₁ : P1
c : k
⊢ ↑(lineMap 1 0) (1 - c) = c
k : Type u_2
V1 : Type u_3
P1 : Type u_1
V2 : Type ?u.538087
P2 : Type ?u.538090
V3 : Type ?u.538093
P3 : Type ?u.538096
V4 : Type ?u.538099
P4 : Type ?u.538102
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
p₀ p₁ : P1
c : k
⊢ ↑(lineMap p₁ p₀) (↑(lineMap 1 0) (1 - c)) = ↑(lineMap p₁ p₀) c
congr
no goals
case h.e_6.h
k : Type u_2
V1 : Type u_3
P1 : Type u_1
V2 : Type ?u.538087
P2 : Type ?u.538090
V3 : Type ?u.538093
P3 : Type ?u.538096
V4 : Type ?u.538099
P4 : Type ?u.538102
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
p₀ p₁ : P1
c : k
⊢ ↑(lineMap 1 0) (1 - c) = c
simp [lineMap_apply]