[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x y : P
R : ℝ
hR : R ≠ 0
hx : x ≠ c
hy : y ≠ c
⊢ inversion c R x ∈ perpBisector c (inversion c R y) ↔ dist x y = dist y c
[PROOFSTEP]
rw [mem_perpBisector_iff_dist_eq, dist_inversion_inversion hx hy, dist_inversion_center]
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x y : P
R : ℝ
hR : R ≠ 0
hx : x ≠ c
hy : y ≠ c
⊢ R ^ 2 / dist x c = R ^ 2 / (dist x c * dist y c) * dist x y ↔ dist x y = dist y c
[PROOFSTEP]
have hx' := dist_ne_zero.2 hx
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x y : P
R : ℝ
hR : R ≠ 0
hx : x ≠ c
hy : y ≠ c
hx' : dist x c ≠ 0
⊢ R ^ 2 / dist x c = R ^ 2 / (dist x c * dist y c) * dist x y ↔ dist x y = dist y c
[PROOFSTEP]
have hy' := dist_ne_zero.2 hy
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x y : P
R : ℝ
hR : R ≠ 0
hx : x ≠ c
hy : y ≠ c
hx' : dist x c ≠ 0
hy' : dist y c ≠ 0
⊢ R ^ 2 / dist x c = R ^ 2 / (dist x c * dist y c) * dist x y ↔ dist x y = dist y c
[PROOFSTEP]
field_simp [mul_assoc, mul_comm, hx, hx.symm, eq_comm]
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x y : P
R : ℝ
hR : R ≠ 0
hy : y ≠ c
⊢ inversion c R x ∈ perpBisector c (inversion c R y) ↔ dist x y = dist y c ∧ x ≠ c
[PROOFSTEP]
rcases eq_or_ne x c with rfl | hx
[GOAL]
case inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
x y : P
R : ℝ
hR : R ≠ 0
hy : y ≠ x
⊢ inversion x R x ∈ perpBisector x (inversion x R y) ↔ dist x y = dist y x ∧ x ≠ x
[PROOFSTEP]
simp [*]
[GOAL]
case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x y : P
R : ℝ
hR : R ≠ 0
hy : y ≠ c
hx : x ≠ c
⊢ inversion c R x ∈ perpBisector c (inversion c R y) ↔ dist x y = dist y c ∧ x ≠ c
[PROOFSTEP]
simp [inversion_mem_perpBisector_inversion_iff hR hx hy, hx]
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x y : P
R : ℝ
hR : R ≠ 0
hy : y ≠ c
⊢ inversion c R ⁻¹' ↑(perpBisector c y) = sphere (inversion c R y) (R ^ 2 / dist y c) \ {c}
[PROOFSTEP]
rw [← dist_inversion_center, ← preimage_inversion_perpBisector_inversion hR, inversion_inversion]
[GOAL]
case hR
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x y : P
R : ℝ
hR : R ≠ 0
hy : y ≠ c
⊢ R ≠ 0
[PROOFSTEP]
simp [*]
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x y : P
R : ℝ
hR : R ≠ 0
hy : y ≠ c
⊢ inversion c R y ≠ c
[PROOFSTEP]
simp [*]
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x y : P
R : ℝ
hR : R ≠ 0
hy : y ≠ c
⊢ inversion c R '' ↑(perpBisector c y) = sphere (inversion c R y) (R ^ 2 / dist y c) \ {c}
[PROOFSTEP]
rw [image_eq_preimage_of_inverse (inversion_involutive _ hR) (inversion_involutive _ hR),
  preimage_inversion_perpBisector hR hy]
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x y : P
R : ℝ
hR : R ≠ 0
hy : y ≠ c
⊢ inversion c R ⁻¹' sphere y (dist y c) = insert c ↑(perpBisector c (inversion c R y))
[PROOFSTEP]
ext x
[GOAL]
case h
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x✝ y : P
R : ℝ
hR : R ≠ 0
hy : y ≠ c
x : P
⊢ x ∈ inversion c R ⁻¹' sphere y (dist y c) ↔ x ∈ insert c ↑(perpBisector c (inversion c R y))
[PROOFSTEP]
rcases eq_or_ne x c with rfl | hx
[GOAL]
case h.inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
x✝ y : P
R : ℝ
hR : R ≠ 0
x : P
hy : y ≠ x
⊢ x ∈ inversion x R ⁻¹' sphere y (dist y x) ↔ x ∈ insert x ↑(perpBisector x (inversion x R y))
[PROOFSTEP]
simp [dist_comm]
[GOAL]
case h.inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x✝ y : P
R : ℝ
hR : R ≠ 0
hy : y ≠ c
x : P
hx : x ≠ c
⊢ x ∈ inversion c R ⁻¹' sphere y (dist y c) ↔ x ∈ insert c ↑(perpBisector c (inversion c R y))
[PROOFSTEP]
rw [mem_preimage, mem_sphere, ← inversion_mem_perpBisector_inversion_iff hR]
[GOAL]
case h.inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x✝ y : P
R : ℝ
hR : R ≠ 0
hy : y ≠ c
x : P
hx : x ≠ c
⊢ inversion c R (inversion c R x) ∈ perpBisector c (inversion c R y) ↔ x ∈ insert c ↑(perpBisector c (inversion c R y))
[PROOFSTEP]
simp [*]
[GOAL]
case h.inr.hx
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x✝ y : P
R : ℝ
hR : R ≠ 0
hy : y ≠ c
x : P
hx : x ≠ c
⊢ inversion c R x ≠ c
[PROOFSTEP]
simp [*]
[GOAL]
case h.inr.hy
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x✝ y : P
R : ℝ
hR : R ≠ 0
hy : y ≠ c
x : P
hx : x ≠ c
⊢ y ≠ c
[PROOFSTEP]
simp [*]
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x y : P
R : ℝ
hR : R ≠ 0
hy : y ≠ c
⊢ inversion c R '' sphere y (dist y c) = insert c ↑(perpBisector c (inversion c R y))
[PROOFSTEP]
rw [image_eq_preimage_of_inverse (inversion_involutive _ hR) (inversion_involutive _ hR),
  preimage_inversion_sphere_dist_center hR hy]


[GOAL]
V : Type u_2
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c c₁ c₂ p₁ p₂ : P
⊢ c ∈ perpBisector p₁ p₂ ↔ inner (↑(Equiv.pointReflection c) p₁ -ᵥ p₂) (p₂ -ᵥ p₁) = 0
[PROOFSTEP]
rw [mem_perpBisector_iff_inner_eq_zero, Equiv.pointReflection_apply, vsub_midpoint, invOf_eq_inv, ← smul_add,
  real_inner_smul_left, vadd_vsub_assoc]
[GOAL]
V : Type u_2
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c c₁ c₂ p₁ p₂ : P
⊢ 2⁻¹ * inner (c -ᵥ p₁ + (c -ᵥ p₂)) (p₂ -ᵥ p₁) = 0 ↔ inner (c -ᵥ p₁ + (c -ᵥ p₂)) (p₂ -ᵥ p₁) = 0
[PROOFSTEP]
simp
[GOAL]
V : Type u_2
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c c₁ c₂ p₁ p₂ : P
⊢ c ∈ perpBisector p₁ (↑(Equiv.pointReflection p₂) p₁) ↔ inner (c -ᵥ p₂) (p₁ -ᵥ p₂) = 0
[PROOFSTEP]
rw [mem_perpBisector_iff_inner_eq_zero, midpoint_pointReflection_right, Equiv.pointReflection_apply, vadd_vsub_assoc,
  inner_add_right, add_self_eq_zero, ← neg_eq_zero, ← inner_neg_right, neg_vsub_eq_vsub_rev]
[GOAL]
V : Type u_2
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c c₁ c₂ p₁✝ p₂✝ p₁ p₂ : P
⊢ midpoint ℝ p₁ p₂ ∈ perpBisector p₁ p₂
[PROOFSTEP]
simp [mem_perpBisector_iff_inner_eq_zero]
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c c₁ c₂ p₁✝ p₂✝ p₁ p₂ : P
⊢ direction (perpBisector p₁ p₂) = (Submodule.span ℝ {p₂ -ᵥ p₁})ᗮ
[PROOFSTEP]
erw [perpBisector, comap_symm, map_direction, Submodule.map_id, Submodule.toAffineSubspace_direction]
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c c₁ c₂ p₁✝ p₂✝ p₁ p₂ : P
⊢ LinearMap.ker (↑(innerₛₗ ℝ) (p₂ -ᵥ p₁)) = (Submodule.span ℝ {p₂ -ᵥ p₁})ᗮ
[PROOFSTEP]
ext x
[GOAL]
case h
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c c₁ c₂ p₁✝ p₂✝ p₁ p₂ : P
x : V
⊢ x ∈ LinearMap.ker (↑(innerₛₗ ℝ) (p₂ -ᵥ p₁)) ↔ x ∈ (Submodule.span ℝ {p₂ -ᵥ p₁})ᗮ
[PROOFSTEP]
exact Submodule.mem_orthogonal_singleton_iff_inner_right.symm
[GOAL]
V : Type u_2
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c c₁ c₂ p₁ p₂ : P
⊢ c ∈ perpBisector p₁ p₂ ↔ inner (c -ᵥ p₁) (p₂ -ᵥ p₁) = inner (c -ᵥ p₂) (p₁ -ᵥ p₂)
[PROOFSTEP]
rw [Iff.comm, mem_perpBisector_iff_inner_eq_zero, ← add_neg_eq_zero, ← inner_neg_right, neg_vsub_eq_vsub_rev, ←
  inner_add_left, vsub_midpoint, invOf_eq_inv, ← smul_add, real_inner_smul_left]
[GOAL]
V : Type u_2
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c c₁ c₂ p₁ p₂ : P
⊢ inner (c -ᵥ p₁ + (c -ᵥ p₂)) (p₂ -ᵥ p₁) = 0 ↔ 2⁻¹ * inner (c -ᵥ p₁ + (c -ᵥ p₂)) (p₂ -ᵥ p₁) = 0
[PROOFSTEP]
simp
[GOAL]
V : Type u_2
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c c₁ c₂ p₁ p₂ : P
⊢ c ∈ perpBisector p₁ p₂ ↔ inner (c -ᵥ p₁) (p₂ -ᵥ p₁) = dist p₁ p₂ ^ 2 / 2
[PROOFSTEP]
rw [mem_perpBisector_iff_inner_eq_zero, ← vsub_sub_vsub_cancel_right _ _ p₁, inner_sub_left, sub_eq_zero,
  midpoint_vsub_left, invOf_eq_inv, real_inner_smul_left, real_inner_self_eq_norm_sq, dist_eq_norm_vsub' V,
  div_eq_inv_mul]
[GOAL]
V : Type u_2
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c c₁ c₂ p₁ p₂ : P
⊢ c ∈ perpBisector p₁ p₂ ↔ dist c p₁ = dist c p₂
[PROOFSTEP]
rw [dist_eq_norm_vsub V, dist_eq_norm_vsub V, ← real_inner_add_sub_eq_zero_iff, vsub_sub_vsub_cancel_left,
  inner_add_left, add_eq_zero_iff_eq_neg, ← inner_neg_right, neg_vsub_eq_vsub_rev, mem_perpBisector_iff_inner_eq_inner]
[GOAL]
V : Type u_2
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c c₁ c₂ p₁ p₂ : P
⊢ c ∈ perpBisector p₁ p₂ ↔ dist p₁ c = dist p₂ c
[PROOFSTEP]
simp only [mem_perpBisector_iff_dist_eq, dist_comm]
[GOAL]
V : Type u_2
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c c₁ c₂ p₁✝ p₂✝ p₁ p₂ : P
⊢ perpBisector p₁ p₂ = perpBisector p₂ p₁
[PROOFSTEP]
ext c
[GOAL]
case h
V : Type u_2
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c✝ c₁ c₂ p₁✝ p₂✝ p₁ p₂ c : P
⊢ c ∈ perpBisector p₁ p₂ ↔ c ∈ perpBisector p₂ p₁
[PROOFSTEP]
simp only [mem_perpBisector_iff_dist_eq, eq_comm]
[GOAL]
V : Type u_2
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c c₁ c₂ p₁ p₂ : P
⊢ p₂ ∈ perpBisector p₁ p₂ ↔ p₁ = p₂
[PROOFSTEP]
simpa [mem_perpBisector_iff_inner_eq_inner] using eq_comm
[GOAL]
V : Type u_2
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c c₁ c₂ p₁ p₂ : P
⊢ p₁ ∈ perpBisector p₁ p₂ ↔ p₁ = p₂
[PROOFSTEP]
rw [perpBisector_comm, right_mem_perpBisector, eq_comm]
[GOAL]
V : Type u_2
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c c₁ c₂ p₁ p₂ p x✝ : P
⊢ x✝ ∈ ↑⊤ → x✝ ∈ ↑(perpBisector p p)
[PROOFSTEP]
simp [mem_perpBisector_iff_inner_eq_inner]
[GOAL]
V : Type u_2
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c c₁ c₂ p₁ p₂ : P
⊢ perpBisector p₁ p₂ = ⊤ ↔ p₁ = p₂
[PROOFSTEP]
refine ⟨fun h ↦ ?_, fun h ↦ h ▸ perpBisector_self _⟩
[GOAL]
V : Type u_2
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c c₁ c₂ p₁ p₂ : P
h : perpBisector p₁ p₂ = ⊤
⊢ p₁ = p₂
[PROOFSTEP]
rw [← left_mem_perpBisector, h]
[GOAL]
V : Type u_2
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c c₁ c₂ p₁ p₂ : P
h : perpBisector p₁ p₂ = ⊤
⊢ p₁ ∈ ⊤
[PROOFSTEP]
trivial
[GOAL]
V : Type u_2
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c c₁ c₂ p₁ p₂ : P
⊢ perpBisector p₁ p₂ ≠ ⊥
[PROOFSTEP]
rw [← nonempty_iff_ne_bot]
[GOAL]
V : Type u_2
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c c₁ c₂ p₁ p₂ : P
⊢ Set.Nonempty ↑(perpBisector p₁ p₂)
[PROOFSTEP]
exact perpBisector_nonempty
[GOAL]
V : Type u_2
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c₁ c₂ p₁ p₂ : P
hc₁ : dist p₁ c₁ = dist p₂ c₁
hc₂ : dist p₁ c₂ = dist p₂ c₂
⊢ inner (c₂ -ᵥ c₁) (p₂ -ᵥ p₁) = 0
[PROOFSTEP]
rw [← Submodule.mem_orthogonal_singleton_iff_inner_left, ← direction_perpBisector]
[GOAL]
V : Type u_2
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c₁ c₂ p₁ p₂ : P
hc₁ : dist p₁ c₁ = dist p₂ c₁
hc₂ : dist p₁ c₂ = dist p₂ c₂
⊢ c₂ -ᵥ c₁ ∈ direction (perpBisector p₁ p₂)
[PROOFSTEP]
apply vsub_mem_direction
[GOAL]
case hp1
V : Type u_2
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c₁ c₂ p₁ p₂ : P
hc₁ : dist p₁ c₁ = dist p₂ c₁
hc₂ : dist p₁ c₂ = dist p₂ c₂
⊢ c₂ ∈ perpBisector p₁ p₂
[PROOFSTEP]
rwa [mem_perpBisector_iff_dist_eq']
[GOAL]
case hp2
V : Type u_2
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c₁ c₂ p₁ p₂ : P
hc₁ : dist p₁ c₁ = dist p₂ c₁
hc₂ : dist p₁ c₂ = dist p₂ c₂
⊢ c₁ ∈ perpBisector p₁ p₂
[PROOFSTEP]
rwa [mem_perpBisector_iff_dist_eq']
[GOAL]
V : Type u_4
P : Type u_1
V' : Type u_3
P' : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MetricSpace P
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddCommGroup V'
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : MetricSpace P'
inst✝ : NormedAddTorsor V' P'
f : P → P'
h : Isometry f
p₁ p₂ : P
⊢ f ⁻¹' ↑(perpBisector (f p₁) (f p₂)) = ↑(perpBisector p₁ p₂)
[PROOFSTEP]
ext x
[GOAL]
case h
V : Type u_4
P : Type u_1
V' : Type u_3
P' : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MetricSpace P
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddCommGroup V'
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : MetricSpace P'
inst✝ : NormedAddTorsor V' P'
f : P → P'
h : Isometry f
p₁ p₂ x : P
⊢ x ∈ f ⁻¹' ↑(perpBisector (f p₁) (f p₂)) ↔ x ∈ ↑(perpBisector p₁ p₂)
[PROOFSTEP]
simp [mem_perpBisector_iff_dist_eq, h.dist_eq]


[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
inst✝ : Category.{?u.41, u_3} E
F G : Karoubi C ⥤ D
φ : F ⟶ G
P : Karoubi C
⊢ NatTrans.app φ P = F.map (decompId_i P) ≫ NatTrans.app φ (Karoubi.mk P.X (𝟙 P.X)) ≫ G.map (decompId_p P)
[PROOFSTEP]
rw [← φ.naturality, ← assoc, ← F.map_comp]
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
inst✝ : Category.{?u.41, u_3} E
F G : Karoubi C ⥤ D
φ : F ⟶ G
P : Karoubi C
⊢ NatTrans.app φ P = F.map (decompId_i P ≫ decompId_p P) ≫ NatTrans.app φ P
[PROOFSTEP]
conv =>
  lhs
  rw [← id_comp (φ.app P), ← F.map_id]
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
inst✝ : Category.{?u.41, u_3} E
F G : Karoubi C ⥤ D
φ : F ⟶ G
P : Karoubi C
| NatTrans.app φ P = F.map (decompId_i P ≫ decompId_p P) ≫ NatTrans.app φ P
[PROOFSTEP]
  lhs
  rw [← id_comp (φ.app P), ← F.map_id]
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
inst✝ : Category.{?u.41, u_3} E
F G : Karoubi C ⥤ D
φ : F ⟶ G
P : Karoubi C
| NatTrans.app φ P = F.map (decompId_i P ≫ decompId_p P) ≫ NatTrans.app φ P
[PROOFSTEP]
  lhs
  rw [← id_comp (φ.app P), ← F.map_id]
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
inst✝ : Category.{?u.41, u_3} E
F G : Karoubi C ⥤ D
φ : F ⟶ G
P : Karoubi C
| NatTrans.app φ P = F.map (decompId_i P ≫ decompId_p P) ≫ NatTrans.app φ P
[PROOFSTEP]
lhs
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
inst✝ : Category.{?u.41, u_3} E
F G : Karoubi C ⥤ D
φ : F ⟶ G
P : Karoubi C
| NatTrans.app φ P
[PROOFSTEP]
rw [← id_comp (φ.app P), ← F.map_id]
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
inst✝ : Category.{?u.41, u_3} E
F G : Karoubi C ⥤ D
φ : F ⟶ G
P : Karoubi C
⊢ F.map (𝟙 P) ≫ NatTrans.app φ P = F.map (decompId_i P ≫ decompId_p P) ≫ NatTrans.app φ P
[PROOFSTEP]
congr
[GOAL]
case e_a.e_a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
inst✝ : Category.{?u.41, u_3} E
F G : Karoubi C ⥤ D
φ : F ⟶ G
P : Karoubi C
⊢ 𝟙 P = decompId_i P ≫ decompId_p P
[PROOFSTEP]
apply decompId
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.1588, u_1} C
inst✝¹ : Category.{?u.1592, u_2} D
inst✝ : Category.{?u.1596, u_3} E
F : C ⥤ Karoubi D
P : Karoubi C
⊢ (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
[PROOFSTEP]
simpa only [F.map_comp, hom_ext_iff] using F.congr_map P.idem
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.1588, u_1} C
inst✝¹ : Category.{?u.1592, u_2} D
inst✝ : Category.{?u.1596, u_3} E
F : C ⥤ Karoubi D
X✝ Y✝ : Karoubi C
f : X✝ ⟶ Y✝
⊢ (F.map f.f).f =
    ((fun P => Karoubi.mk (F.obj P.X).X (F.map P.p).f) X✝).p ≫
      (F.map f.f).f ≫ ((fun P => Karoubi.mk (F.obj P.X).X (F.map P.p).f) Y✝).p
[PROOFSTEP]
simpa only [F.map_comp, hom_ext_iff] using F.congr_map f.comm
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.7089, u_1} C
inst✝¹ : Category.{?u.7093, u_2} D
inst✝ : Category.{?u.7097, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
P : Karoubi C
⊢ (F.map P.p).f ≫ (NatTrans.app φ P.X).f =
    ((obj F).obj P).p ≫ ((F.map P.p).f ≫ (NatTrans.app φ P.X).f) ≫ ((obj G).obj P).p
[PROOFSTEP]
have h := φ.naturality P.p
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.7089, u_1} C
inst✝¹ : Category.{?u.7093, u_2} D
inst✝ : Category.{?u.7097, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
P : Karoubi C
h : F.map P.p ≫ NatTrans.app φ P.X = NatTrans.app φ P.X ≫ G.map P.p
⊢ (F.map P.p).f ≫ (NatTrans.app φ P.X).f =
    ((obj F).obj P).p ≫ ((F.map P.p).f ≫ (NatTrans.app φ P.X).f) ≫ ((obj G).obj P).p
[PROOFSTEP]
have h' := F.congr_map P.idem
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.7089, u_1} C
inst✝¹ : Category.{?u.7093, u_2} D
inst✝ : Category.{?u.7097, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
P : Karoubi C
h : F.map P.p ≫ NatTrans.app φ P.X = NatTrans.app φ P.X ≫ G.map P.p
h' : F.map (P.p ≫ P.p) = F.map P.p
⊢ (F.map P.p).f ≫ (NatTrans.app φ P.X).f =
    ((obj F).obj P).p ≫ ((F.map P.p).f ≫ (NatTrans.app φ P.X).f) ≫ ((obj G).obj P).p
[PROOFSTEP]
simp only [hom_ext_iff, Karoubi.comp_f, F.map_comp] at h h'
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.7089, u_1} C
inst✝¹ : Category.{?u.7093, u_2} D
inst✝ : Category.{?u.7097, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
P : Karoubi C
h : (F.map P.p).f ≫ (NatTrans.app φ P.X).f = (NatTrans.app φ P.X).f ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
⊢ (F.map P.p).f ≫ (NatTrans.app φ P.X).f =
    ((obj F).obj P).p ≫ ((F.map P.p).f ≫ (NatTrans.app φ P.X).f) ≫ ((obj G).obj P).p
[PROOFSTEP]
simp only [obj_obj_p, assoc, ← h]
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.7089, u_1} C
inst✝¹ : Category.{?u.7093, u_2} D
inst✝ : Category.{?u.7097, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
P : Karoubi C
h : (F.map P.p).f ≫ (NatTrans.app φ P.X).f = (NatTrans.app φ P.X).f ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
⊢ (F.map P.p).f ≫ (NatTrans.app φ P.X).f = (F.map P.p).f ≫ (F.map P.p).f ≫ (F.map P.p).f ≫ (NatTrans.app φ P.X).f
[PROOFSTEP]
slice_rhs 1 3 => rw [h', h']
[GOAL]
case a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.7089, u_1} C
inst✝¹ : Category.{?u.7093, u_2} D
inst✝ : Category.{?u.7097, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
P : Karoubi C
h : (F.map P.p).f ≫ (NatTrans.app φ P.X).f = (NatTrans.app φ P.X).f ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
| (F.map P.p).f ≫ (F.map P.p).f ≫ (F.map P.p).f
case a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.7089, u_1} C
inst✝¹ : Category.{?u.7093, u_2} D
inst✝ : Category.{?u.7097, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
P : Karoubi C
h : (F.map P.p).f ≫ (NatTrans.app φ P.X).f = (NatTrans.app φ P.X).f ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
| (NatTrans.app φ P.X).f
[PROOFSTEP]
rw [h', h']
[GOAL]
case a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.7089, u_1} C
inst✝¹ : Category.{?u.7093, u_2} D
inst✝ : Category.{?u.7097, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
P : Karoubi C
h : (F.map P.p).f ≫ (NatTrans.app φ P.X).f = (NatTrans.app φ P.X).f ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
| (F.map P.p).f ≫ (F.map P.p).f ≫ (F.map P.p).f
case a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.7089, u_1} C
inst✝¹ : Category.{?u.7093, u_2} D
inst✝ : Category.{?u.7097, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
P : Karoubi C
h : (F.map P.p).f ≫ (NatTrans.app φ P.X).f = (NatTrans.app φ P.X).f ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
| (NatTrans.app φ P.X).f
[PROOFSTEP]
rw [h', h']
[GOAL]
case a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.7089, u_1} C
inst✝¹ : Category.{?u.7093, u_2} D
inst✝ : Category.{?u.7097, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
P : Karoubi C
h : (F.map P.p).f ≫ (NatTrans.app φ P.X).f = (NatTrans.app φ P.X).f ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
| (F.map P.p).f ≫ (F.map P.p).f ≫ (F.map P.p).f
case a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.7089, u_1} C
inst✝¹ : Category.{?u.7093, u_2} D
inst✝ : Category.{?u.7097, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
P : Karoubi C
h : (F.map P.p).f ≫ (NatTrans.app φ P.X).f = (NatTrans.app φ P.X).f ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
| (NatTrans.app φ P.X).f
[PROOFSTEP]
rw [h', h']
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.7089, u_1} C
inst✝¹ : Category.{?u.7093, u_2} D
inst✝ : Category.{?u.7097, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
x✝¹ x✝ : Karoubi C
f : x✝¹ ⟶ x✝
⊢ (obj F).map f ≫ (fun P => Hom.mk ((F.map P.p).f ≫ (NatTrans.app φ P.X).f)) x✝ =
    (fun P => Hom.mk ((F.map P.p).f ≫ (NatTrans.app φ P.X).f)) x✝¹ ≫ (obj G).map f
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.7089, u_1} C
inst✝¹ : Category.{?u.7093, u_2} D
inst✝ : Category.{?u.7097, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
x✝¹ x✝ : Karoubi C
f : x✝¹ ⟶ x✝
⊢ ((obj F).map f ≫ (fun P => Hom.mk ((F.map P.p).f ≫ (NatTrans.app φ P.X).f)) x✝).f =
    ((fun P => Hom.mk ((F.map P.p).f ≫ (NatTrans.app φ P.X).f)) x✝¹ ≫ (obj G).map f).f
[PROOFSTEP]
dsimp [obj]
[GOAL]
case h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.7089, u_1} C
inst✝¹ : Category.{?u.7093, u_2} D
inst✝ : Category.{?u.7097, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
x✝¹ x✝ : Karoubi C
f : x✝¹ ⟶ x✝
⊢ (F.map f.f).f ≫ (F.map x✝.p).f ≫ (NatTrans.app φ x✝.X).f =
    ((F.map x✝¹.p).f ≫ (NatTrans.app φ x✝¹.X).f) ≫ (G.map f.f).f
[PROOFSTEP]
have h := φ.naturality f.f
[GOAL]
case h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.7089, u_1} C
inst✝¹ : Category.{?u.7093, u_2} D
inst✝ : Category.{?u.7097, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
x✝¹ x✝ : Karoubi C
f : x✝¹ ⟶ x✝
h : F.map f.f ≫ NatTrans.app φ x✝.X = NatTrans.app φ x✝¹.X ≫ G.map f.f
⊢ (F.map f.f).f ≫ (F.map x✝.p).f ≫ (NatTrans.app φ x✝.X).f =
    ((F.map x✝¹.p).f ≫ (NatTrans.app φ x✝¹.X).f) ≫ (G.map f.f).f
[PROOFSTEP]
have h' := F.congr_map (comp_p f)
[GOAL]
case h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.7089, u_1} C
inst✝¹ : Category.{?u.7093, u_2} D
inst✝ : Category.{?u.7097, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
x✝¹ x✝ : Karoubi C
f : x✝¹ ⟶ x✝
h : F.map f.f ≫ NatTrans.app φ x✝.X = NatTrans.app φ x✝¹.X ≫ G.map f.f
h' : F.map (f.f ≫ x✝.p) = F.map f.f
⊢ (F.map f.f).f ≫ (F.map x✝.p).f ≫ (NatTrans.app φ x✝.X).f =
    ((F.map x✝¹.p).f ≫ (NatTrans.app φ x✝¹.X).f) ≫ (G.map f.f).f
[PROOFSTEP]
have h'' := F.congr_map (p_comp f)
[GOAL]
case h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.7089, u_1} C
inst✝¹ : Category.{?u.7093, u_2} D
inst✝ : Category.{?u.7097, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
x✝¹ x✝ : Karoubi C
f : x✝¹ ⟶ x✝
h : F.map f.f ≫ NatTrans.app φ x✝.X = NatTrans.app φ x✝¹.X ≫ G.map f.f
h' : F.map (f.f ≫ x✝.p) = F.map f.f
h'' : F.map (x✝¹.p ≫ f.f) = F.map f.f
⊢ (F.map f.f).f ≫ (F.map x✝.p).f ≫ (NatTrans.app φ x✝.X).f =
    ((F.map x✝¹.p).f ≫ (NatTrans.app φ x✝¹.X).f) ≫ (G.map f.f).f
[PROOFSTEP]
simp only [hom_ext_iff, Functor.map_comp, comp_f] at h h' h'' ⊢
[GOAL]
case h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.7089, u_1} C
inst✝¹ : Category.{?u.7093, u_2} D
inst✝ : Category.{?u.7097, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
x✝¹ x✝ : Karoubi C
f : x✝¹ ⟶ x✝
h : (F.map f.f).f ≫ (NatTrans.app φ x✝.X).f = (NatTrans.app φ x✝¹.X).f ≫ (G.map f.f).f
h' : (F.map f.f).f ≫ (F.map x✝.p).f = (F.map f.f).f
h'' : (F.map x✝¹.p).f ≫ (F.map f.f).f = (F.map f.f).f
⊢ (F.map f.f).f ≫ (F.map x✝.p).f ≫ (NatTrans.app φ x✝.X).f =
    ((F.map x✝¹.p).f ≫ (NatTrans.app φ x✝¹.X).f) ≫ (G.map f.f).f
[PROOFSTEP]
slice_rhs 2 3 => rw [← h]
[GOAL]
case a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.7089, u_1} C
inst✝¹ : Category.{?u.7093, u_2} D
inst✝ : Category.{?u.7097, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
x✝¹ x✝ : Karoubi C
f : x✝¹ ⟶ x✝
h : (F.map f.f).f ≫ (NatTrans.app φ x✝.X).f = (NatTrans.app φ x✝¹.X).f ≫ (G.map f.f).f
h' : (F.map f.f).f ≫ (F.map x✝.p).f = (F.map f.f).f
h'' : (F.map x✝¹.p).f ≫ (F.map f.f).f = (F.map f.f).f
| (NatTrans.app φ x✝¹.X).f ≫ (G.map f.f).f
case a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.7089, u_1} C
inst✝¹ : Category.{?u.7093, u_2} D
inst✝ : Category.{?u.7097, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
x✝¹ x✝ : Karoubi C
f : x✝¹ ⟶ x✝
h : (F.map f.f).f ≫ (NatTrans.app φ x✝.X).f = (NatTrans.app φ x✝¹.X).f ≫ (G.map f.f).f
h' : (F.map f.f).f ≫ (F.map x✝.p).f = (F.map f.f).f
h'' : (F.map x✝¹.p).f ≫ (F.map f.f).f = (F.map f.f).f
| (F.map x✝¹.p).f
[PROOFSTEP]
rw [← h]
[GOAL]
case a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.7089, u_1} C
inst✝¹ : Category.{?u.7093, u_2} D
inst✝ : Category.{?u.7097, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
x✝¹ x✝ : Karoubi C
f : x✝¹ ⟶ x✝
h : (F.map f.f).f ≫ (NatTrans.app φ x✝.X).f = (NatTrans.app φ x✝¹.X).f ≫ (G.map f.f).f
h' : (F.map f.f).f ≫ (F.map x✝.p).f = (F.map f.f).f
h'' : (F.map x✝¹.p).f ≫ (F.map f.f).f = (F.map f.f).f
| (NatTrans.app φ x✝¹.X).f ≫ (G.map f.f).f
case a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.7089, u_1} C
inst✝¹ : Category.{?u.7093, u_2} D
inst✝ : Category.{?u.7097, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
x✝¹ x✝ : Karoubi C
f : x✝¹ ⟶ x✝
h : (F.map f.f).f ≫ (NatTrans.app φ x✝.X).f = (NatTrans.app φ x✝¹.X).f ≫ (G.map f.f).f
h' : (F.map f.f).f ≫ (F.map x✝.p).f = (F.map f.f).f
h'' : (F.map x✝¹.p).f ≫ (F.map f.f).f = (F.map f.f).f
| (F.map x✝¹.p).f
[PROOFSTEP]
rw [← h]
[GOAL]
case a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.7089, u_1} C
inst✝¹ : Category.{?u.7093, u_2} D
inst✝ : Category.{?u.7097, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
x✝¹ x✝ : Karoubi C
f : x✝¹ ⟶ x✝
h : (F.map f.f).f ≫ (NatTrans.app φ x✝.X).f = (NatTrans.app φ x✝¹.X).f ≫ (G.map f.f).f
h' : (F.map f.f).f ≫ (F.map x✝.p).f = (F.map f.f).f
h'' : (F.map x✝¹.p).f ≫ (F.map f.f).f = (F.map f.f).f
| (NatTrans.app φ x✝¹.X).f ≫ (G.map f.f).f
case a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.7089, u_1} C
inst✝¹ : Category.{?u.7093, u_2} D
inst✝ : Category.{?u.7097, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
x✝¹ x✝ : Karoubi C
f : x✝¹ ⟶ x✝
h : (F.map f.f).f ≫ (NatTrans.app φ x✝.X).f = (NatTrans.app φ x✝¹.X).f ≫ (G.map f.f).f
h' : (F.map f.f).f ≫ (F.map x✝.p).f = (F.map f.f).f
h'' : (F.map x✝¹.p).f ≫ (F.map f.f).f = (F.map f.f).f
| (F.map x✝¹.p).f
[PROOFSTEP]
rw [← h]
[GOAL]
case h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.7089, u_1} C
inst✝¹ : Category.{?u.7093, u_2} D
inst✝ : Category.{?u.7097, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
x✝¹ x✝ : Karoubi C
f : x✝¹ ⟶ x✝
h : (F.map f.f).f ≫ (NatTrans.app φ x✝.X).f = (NatTrans.app φ x✝¹.X).f ≫ (G.map f.f).f
h' : (F.map f.f).f ≫ (F.map x✝.p).f = (F.map f.f).f
h'' : (F.map x✝¹.p).f ≫ (F.map f.f).f = (F.map f.f).f
⊢ (F.map f.f).f ≫ (F.map x✝.p).f ≫ (NatTrans.app φ x✝.X).f = (F.map x✝¹.p).f ≫ (F.map f.f).f ≫ (NatTrans.app φ x✝.X).f
[PROOFSTEP]
slice_lhs 1 2 => rw [h']
[GOAL]
case a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.7089, u_1} C
inst✝¹ : Category.{?u.7093, u_2} D
inst✝ : Category.{?u.7097, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
x✝¹ x✝ : Karoubi C
f : x✝¹ ⟶ x✝
h : (F.map f.f).f ≫ (NatTrans.app φ x✝.X).f = (NatTrans.app φ x✝¹.X).f ≫ (G.map f.f).f
h' : (F.map f.f).f ≫ (F.map x✝.p).f = (F.map f.f).f
h'' : (F.map x✝¹.p).f ≫ (F.map f.f).f = (F.map f.f).f
| (F.map f.f).f ≫ (F.map x✝.p).f
case a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.7089, u_1} C
inst✝¹ : Category.{?u.7093, u_2} D
inst✝ : Category.{?u.7097, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
x✝¹ x✝ : Karoubi C
f : x✝¹ ⟶ x✝
h : (F.map f.f).f ≫ (NatTrans.app φ x✝.X).f = (NatTrans.app φ x✝¹.X).f ≫ (G.map f.f).f
h' : (F.map f.f).f ≫ (F.map x✝.p).f = (F.map f.f).f
h'' : (F.map x✝¹.p).f ≫ (F.map f.f).f = (F.map f.f).f
| (NatTrans.app φ x✝.X).f
[PROOFSTEP]
rw [h']
[GOAL]
case a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.7089, u_1} C
inst✝¹ : Category.{?u.7093, u_2} D
inst✝ : Category.{?u.7097, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
x✝¹ x✝ : Karoubi C
f : x✝¹ ⟶ x✝
h : (F.map f.f).f ≫ (NatTrans.app φ x✝.X).f = (NatTrans.app φ x✝¹.X).f ≫ (G.map f.f).f
h' : (F.map f.f).f ≫ (F.map x✝.p).f = (F.map f.f).f
h'' : (F.map x✝¹.p).f ≫ (F.map f.f).f = (F.map f.f).f
| (F.map f.f).f ≫ (F.map x✝.p).f
case a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.7089, u_1} C
inst✝¹ : Category.{?u.7093, u_2} D
inst✝ : Category.{?u.7097, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
x✝¹ x✝ : Karoubi C
f : x✝¹ ⟶ x✝
h : (F.map f.f).f ≫ (NatTrans.app φ x✝.X).f = (NatTrans.app φ x✝¹.X).f ≫ (G.map f.f).f
h' : (F.map f.f).f ≫ (F.map x✝.p).f = (F.map f.f).f
h'' : (F.map x✝¹.p).f ≫ (F.map f.f).f = (F.map f.f).f
| (NatTrans.app φ x✝.X).f
[PROOFSTEP]
rw [h']
[GOAL]
case a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.7089, u_1} C
inst✝¹ : Category.{?u.7093, u_2} D
inst✝ : Category.{?u.7097, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
x✝¹ x✝ : Karoubi C
f : x✝¹ ⟶ x✝
h : (F.map f.f).f ≫ (NatTrans.app φ x✝.X).f = (NatTrans.app φ x✝¹.X).f ≫ (G.map f.f).f
h' : (F.map f.f).f ≫ (F.map x✝.p).f = (F.map f.f).f
h'' : (F.map x✝¹.p).f ≫ (F.map f.f).f = (F.map f.f).f
| (F.map f.f).f ≫ (F.map x✝.p).f
case a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.7089, u_1} C
inst✝¹ : Category.{?u.7093, u_2} D
inst✝ : Category.{?u.7097, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
x✝¹ x✝ : Karoubi C
f : x✝¹ ⟶ x✝
h : (F.map f.f).f ≫ (NatTrans.app φ x✝.X).f = (NatTrans.app φ x✝¹.X).f ≫ (G.map f.f).f
h' : (F.map f.f).f ≫ (F.map x✝.p).f = (F.map f.f).f
h'' : (F.map x✝¹.p).f ≫ (F.map f.f).f = (F.map f.f).f
| (NatTrans.app φ x✝.X).f
[PROOFSTEP]
rw [h']
[GOAL]
case h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.7089, u_1} C
inst✝¹ : Category.{?u.7093, u_2} D
inst✝ : Category.{?u.7097, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
x✝¹ x✝ : Karoubi C
f : x✝¹ ⟶ x✝
h : (F.map f.f).f ≫ (NatTrans.app φ x✝.X).f = (NatTrans.app φ x✝¹.X).f ≫ (G.map f.f).f
h' : (F.map f.f).f ≫ (F.map x✝.p).f = (F.map f.f).f
h'' : (F.map x✝¹.p).f ≫ (F.map f.f).f = (F.map f.f).f
⊢ (F.map f.f).f ≫ (NatTrans.app φ x✝.X).f = (F.map x✝¹.p).f ≫ (F.map f.f).f ≫ (NatTrans.app φ x✝.X).f
[PROOFSTEP]
slice_rhs 1 2 => rw [h'']
[GOAL]
case a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.7089, u_1} C
inst✝¹ : Category.{?u.7093, u_2} D
inst✝ : Category.{?u.7097, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
x✝¹ x✝ : Karoubi C
f : x✝¹ ⟶ x✝
h : (F.map f.f).f ≫ (NatTrans.app φ x✝.X).f = (NatTrans.app φ x✝¹.X).f ≫ (G.map f.f).f
h' : (F.map f.f).f ≫ (F.map x✝.p).f = (F.map f.f).f
h'' : (F.map x✝¹.p).f ≫ (F.map f.f).f = (F.map f.f).f
| (F.map x✝¹.p).f ≫ (F.map f.f).f
case a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.7089, u_1} C
inst✝¹ : Category.{?u.7093, u_2} D
inst✝ : Category.{?u.7097, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
x✝¹ x✝ : Karoubi C
f : x✝¹ ⟶ x✝
h : (F.map f.f).f ≫ (NatTrans.app φ x✝.X).f = (NatTrans.app φ x✝¹.X).f ≫ (G.map f.f).f
h' : (F.map f.f).f ≫ (F.map x✝.p).f = (F.map f.f).f
h'' : (F.map x✝¹.p).f ≫ (F.map f.f).f = (F.map f.f).f
| (NatTrans.app φ x✝.X).f
[PROOFSTEP]
rw [h'']
[GOAL]
case a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.7089, u_1} C
inst✝¹ : Category.{?u.7093, u_2} D
inst✝ : Category.{?u.7097, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
x✝¹ x✝ : Karoubi C
f : x✝¹ ⟶ x✝
h : (F.map f.f).f ≫ (NatTrans.app φ x✝.X).f = (NatTrans.app φ x✝¹.X).f ≫ (G.map f.f).f
h' : (F.map f.f).f ≫ (F.map x✝.p).f = (F.map f.f).f
h'' : (F.map x✝¹.p).f ≫ (F.map f.f).f = (F.map f.f).f
| (F.map x✝¹.p).f ≫ (F.map f.f).f
case a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.7089, u_1} C
inst✝¹ : Category.{?u.7093, u_2} D
inst✝ : Category.{?u.7097, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
x✝¹ x✝ : Karoubi C
f : x✝¹ ⟶ x✝
h : (F.map f.f).f ≫ (NatTrans.app φ x✝.X).f = (NatTrans.app φ x✝¹.X).f ≫ (G.map f.f).f
h' : (F.map f.f).f ≫ (F.map x✝.p).f = (F.map f.f).f
h'' : (F.map x✝¹.p).f ≫ (F.map f.f).f = (F.map f.f).f
| (NatTrans.app φ x✝.X).f
[PROOFSTEP]
rw [h'']
[GOAL]
case a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.7089, u_1} C
inst✝¹ : Category.{?u.7093, u_2} D
inst✝ : Category.{?u.7097, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
x✝¹ x✝ : Karoubi C
f : x✝¹ ⟶ x✝
h : (F.map f.f).f ≫ (NatTrans.app φ x✝.X).f = (NatTrans.app φ x✝¹.X).f ≫ (G.map f.f).f
h' : (F.map f.f).f ≫ (F.map x✝.p).f = (F.map f.f).f
h'' : (F.map x✝¹.p).f ≫ (F.map f.f).f = (F.map f.f).f
| (F.map x✝¹.p).f ≫ (F.map f.f).f
case a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.7089, u_1} C
inst✝¹ : Category.{?u.7093, u_2} D
inst✝ : Category.{?u.7097, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
x✝¹ x✝ : Karoubi C
f : x✝¹ ⟶ x✝
h : (F.map f.f).f ≫ (NatTrans.app φ x✝.X).f = (NatTrans.app φ x✝¹.X).f ≫ (G.map f.f).f
h' : (F.map f.f).f ≫ (F.map x✝.p).f = (F.map f.f).f
h'' : (F.map x✝¹.p).f ≫ (F.map f.f).f = (F.map f.f).f
| (NatTrans.app φ x✝.X).f
[PROOFSTEP]
rw [h'']
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.20838, u_1} C
inst✝¹ : Category.{?u.20842, u_2} D
inst✝ : Category.{?u.20846, u_3} E
F : C ⥤ Karoubi D
⊢ { obj := FunctorExtension₁.obj, map := fun {X Y} => FunctorExtension₁.map }.map (𝟙 F) =
    𝟙 ({ obj := FunctorExtension₁.obj, map := fun {X Y} => FunctorExtension₁.map }.obj F)
[PROOFSTEP]
ext P
[GOAL]
case w.h.h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.20838, u_1} C
inst✝¹ : Category.{?u.20842, u_2} D
inst✝ : Category.{?u.20846, u_3} E
F : C ⥤ Karoubi D
P : Karoubi C
⊢ (NatTrans.app ({ obj := FunctorExtension₁.obj, map := fun {X Y} => FunctorExtension₁.map }.map (𝟙 F)) P).f =
    (NatTrans.app (𝟙 ({ obj := FunctorExtension₁.obj, map := fun {X Y} => FunctorExtension₁.map }.obj F)) P).f
[PROOFSTEP]
exact comp_p (F.map P.p)
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.20838, u_1} C
inst✝¹ : Category.{?u.20842, u_2} D
inst✝ : Category.{?u.20846, u_3} E
F G H : C ⥤ Karoubi D
φ : F ⟶ G
φ' : G ⟶ H
⊢ { obj := FunctorExtension₁.obj, map := fun {X Y} => FunctorExtension₁.map }.map (φ ≫ φ') =
    { obj := FunctorExtension₁.obj, map := fun {X Y} => FunctorExtension₁.map }.map φ ≫
      { obj := FunctorExtension₁.obj, map := fun {X Y} => FunctorExtension₁.map }.map φ'
[PROOFSTEP]
ext P
[GOAL]
case w.h.h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.20838, u_1} C
inst✝¹ : Category.{?u.20842, u_2} D
inst✝ : Category.{?u.20846, u_3} E
F G H : C ⥤ Karoubi D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi C
⊢ (NatTrans.app ({ obj := FunctorExtension₁.obj, map := fun {X Y} => FunctorExtension₁.map }.map (φ ≫ φ')) P).f =
    (NatTrans.app
        ({ obj := FunctorExtension₁.obj, map := fun {X Y} => FunctorExtension₁.map }.map φ ≫
          { obj := FunctorExtension₁.obj, map := fun {X Y} => FunctorExtension₁.map }.map φ')
        P).f
[PROOFSTEP]
simp only [comp_f, FunctorExtension₁.map_app_f, NatTrans.comp_app, assoc]
[GOAL]
case w.h.h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.20838, u_1} C
inst✝¹ : Category.{?u.20842, u_2} D
inst✝ : Category.{?u.20846, u_3} E
F G H : C ⥤ Karoubi D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi C
⊢ (F.map P.p).f ≫ (NatTrans.app φ P.X).f ≫ (NatTrans.app φ' P.X).f =
    (F.map P.p).f ≫ (NatTrans.app φ P.X).f ≫ (G.map P.p).f ≫ (NatTrans.app φ' P.X).f
[PROOFSTEP]
have h := φ.naturality P.p
[GOAL]
case w.h.h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.20838, u_1} C
inst✝¹ : Category.{?u.20842, u_2} D
inst✝ : Category.{?u.20846, u_3} E
F G H : C ⥤ Karoubi D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi C
h : F.map P.p ≫ NatTrans.app φ P.X = NatTrans.app φ P.X ≫ G.map P.p
⊢ (F.map P.p).f ≫ (NatTrans.app φ P.X).f ≫ (NatTrans.app φ' P.X).f =
    (F.map P.p).f ≫ (NatTrans.app φ P.X).f ≫ (G.map P.p).f ≫ (NatTrans.app φ' P.X).f
[PROOFSTEP]
have h' := F.congr_map P.idem
[GOAL]
case w.h.h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.20838, u_1} C
inst✝¹ : Category.{?u.20842, u_2} D
inst✝ : Category.{?u.20846, u_3} E
F G H : C ⥤ Karoubi D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi C
h : F.map P.p ≫ NatTrans.app φ P.X = NatTrans.app φ P.X ≫ G.map P.p
h' : F.map (P.p ≫ P.p) = F.map P.p
⊢ (F.map P.p).f ≫ (NatTrans.app φ P.X).f ≫ (NatTrans.app φ' P.X).f =
    (F.map P.p).f ≫ (NatTrans.app φ P.X).f ≫ (G.map P.p).f ≫ (NatTrans.app φ' P.X).f
[PROOFSTEP]
simp only [hom_ext_iff, comp_f, F.map_comp] at h h'
[GOAL]
case w.h.h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.20838, u_1} C
inst✝¹ : Category.{?u.20842, u_2} D
inst✝ : Category.{?u.20846, u_3} E
F G H : C ⥤ Karoubi D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi C
h : (F.map P.p).f ≫ (NatTrans.app φ P.X).f = (NatTrans.app φ P.X).f ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
⊢ (F.map P.p).f ≫ (NatTrans.app φ P.X).f ≫ (NatTrans.app φ' P.X).f =
    (F.map P.p).f ≫ (NatTrans.app φ P.X).f ≫ (G.map P.p).f ≫ (NatTrans.app φ' P.X).f
[PROOFSTEP]
slice_rhs 2 3 => rw [← h]
[GOAL]
case a.a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.20838, u_1} C
inst✝¹ : Category.{?u.20842, u_2} D
inst✝ : Category.{?u.20846, u_3} E
F G H : C ⥤ Karoubi D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi C
h : (F.map P.p).f ≫ (NatTrans.app φ P.X).f = (NatTrans.app φ P.X).f ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
| (NatTrans.app φ P.X).f ≫ (G.map P.p).f
case a.a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.20838, u_1} C
inst✝¹ : Category.{?u.20842, u_2} D
inst✝ : Category.{?u.20846, u_3} E
F G H : C ⥤ Karoubi D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi C
h : (F.map P.p).f ≫ (NatTrans.app φ P.X).f = (NatTrans.app φ P.X).f ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
| (NatTrans.app φ' P.X).f
case a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.20838, u_1} C
inst✝¹ : Category.{?u.20842, u_2} D
inst✝ : Category.{?u.20846, u_3} E
F G H : C ⥤ Karoubi D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi C
h : (F.map P.p).f ≫ (NatTrans.app φ P.X).f = (NatTrans.app φ P.X).f ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
| (F.map P.p).f
[PROOFSTEP]
rw [← h]
[GOAL]
case a.a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.20838, u_1} C
inst✝¹ : Category.{?u.20842, u_2} D
inst✝ : Category.{?u.20846, u_3} E
F G H : C ⥤ Karoubi D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi C
h : (F.map P.p).f ≫ (NatTrans.app φ P.X).f = (NatTrans.app φ P.X).f ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
| (NatTrans.app φ P.X).f ≫ (G.map P.p).f
case a.a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.20838, u_1} C
inst✝¹ : Category.{?u.20842, u_2} D
inst✝ : Category.{?u.20846, u_3} E
F G H : C ⥤ Karoubi D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi C
h : (F.map P.p).f ≫ (NatTrans.app φ P.X).f = (NatTrans.app φ P.X).f ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
| (NatTrans.app φ' P.X).f
case a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.20838, u_1} C
inst✝¹ : Category.{?u.20842, u_2} D
inst✝ : Category.{?u.20846, u_3} E
F G H : C ⥤ Karoubi D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi C
h : (F.map P.p).f ≫ (NatTrans.app φ P.X).f = (NatTrans.app φ P.X).f ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
| (F.map P.p).f
[PROOFSTEP]
rw [← h]
[GOAL]
case a.a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.20838, u_1} C
inst✝¹ : Category.{?u.20842, u_2} D
inst✝ : Category.{?u.20846, u_3} E
F G H : C ⥤ Karoubi D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi C
h : (F.map P.p).f ≫ (NatTrans.app φ P.X).f = (NatTrans.app φ P.X).f ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
| (NatTrans.app φ P.X).f ≫ (G.map P.p).f
case a.a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.20838, u_1} C
inst✝¹ : Category.{?u.20842, u_2} D
inst✝ : Category.{?u.20846, u_3} E
F G H : C ⥤ Karoubi D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi C
h : (F.map P.p).f ≫ (NatTrans.app φ P.X).f = (NatTrans.app φ P.X).f ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
| (NatTrans.app φ' P.X).f
case a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.20838, u_1} C
inst✝¹ : Category.{?u.20842, u_2} D
inst✝ : Category.{?u.20846, u_3} E
F G H : C ⥤ Karoubi D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi C
h : (F.map P.p).f ≫ (NatTrans.app φ P.X).f = (NatTrans.app φ P.X).f ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
| (F.map P.p).f
[PROOFSTEP]
rw [← h]
[GOAL]
case w.h.h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.20838, u_1} C
inst✝¹ : Category.{?u.20842, u_2} D
inst✝ : Category.{?u.20846, u_3} E
F G H : C ⥤ Karoubi D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi C
h : (F.map P.p).f ≫ (NatTrans.app φ P.X).f = (NatTrans.app φ P.X).f ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
⊢ (F.map P.p).f ≫ (NatTrans.app φ P.X).f ≫ (NatTrans.app φ' P.X).f =
    (F.map P.p).f ≫ ((F.map P.p).f ≫ (NatTrans.app φ P.X).f) ≫ (NatTrans.app φ' P.X).f
[PROOFSTEP]
slice_rhs 1 2 => rw [h']
[GOAL]
case a.a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.20838, u_1} C
inst✝¹ : Category.{?u.20842, u_2} D
inst✝ : Category.{?u.20846, u_3} E
F G H : C ⥤ Karoubi D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi C
h : (F.map P.p).f ≫ (NatTrans.app φ P.X).f = (NatTrans.app φ P.X).f ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
| (F.map P.p).f ≫ (F.map P.p).f
case a.a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.20838, u_1} C
inst✝¹ : Category.{?u.20842, u_2} D
inst✝ : Category.{?u.20846, u_3} E
F G H : C ⥤ Karoubi D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi C
h : (F.map P.p).f ≫ (NatTrans.app φ P.X).f = (NatTrans.app φ P.X).f ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
| (NatTrans.app φ P.X).f
case a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.20838, u_1} C
inst✝¹ : Category.{?u.20842, u_2} D
inst✝ : Category.{?u.20846, u_3} E
F G H : C ⥤ Karoubi D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi C
h : (F.map P.p).f ≫ (NatTrans.app φ P.X).f = (NatTrans.app φ P.X).f ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
| (NatTrans.app φ' P.X).f
[PROOFSTEP]
rw [h']
[GOAL]
case a.a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.20838, u_1} C
inst✝¹ : Category.{?u.20842, u_2} D
inst✝ : Category.{?u.20846, u_3} E
F G H : C ⥤ Karoubi D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi C
h : (F.map P.p).f ≫ (NatTrans.app φ P.X).f = (NatTrans.app φ P.X).f ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
| (F.map P.p).f ≫ (F.map P.p).f
case a.a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.20838, u_1} C
inst✝¹ : Category.{?u.20842, u_2} D
inst✝ : Category.{?u.20846, u_3} E
F G H : C ⥤ Karoubi D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi C
h : (F.map P.p).f ≫ (NatTrans.app φ P.X).f = (NatTrans.app φ P.X).f ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
| (NatTrans.app φ P.X).f
case a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.20838, u_1} C
inst✝¹ : Category.{?u.20842, u_2} D
inst✝ : Category.{?u.20846, u_3} E
F G H : C ⥤ Karoubi D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi C
h : (F.map P.p).f ≫ (NatTrans.app φ P.X).f = (NatTrans.app φ P.X).f ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
| (NatTrans.app φ' P.X).f
[PROOFSTEP]
rw [h']
[GOAL]
case a.a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.20838, u_1} C
inst✝¹ : Category.{?u.20842, u_2} D
inst✝ : Category.{?u.20846, u_3} E
F G H : C ⥤ Karoubi D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi C
h : (F.map P.p).f ≫ (NatTrans.app φ P.X).f = (NatTrans.app φ P.X).f ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
| (F.map P.p).f ≫ (F.map P.p).f
case a.a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.20838, u_1} C
inst✝¹ : Category.{?u.20842, u_2} D
inst✝ : Category.{?u.20846, u_3} E
F G H : C ⥤ Karoubi D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi C
h : (F.map P.p).f ≫ (NatTrans.app φ P.X).f = (NatTrans.app φ P.X).f ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
| (NatTrans.app φ P.X).f
case a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.20838, u_1} C
inst✝¹ : Category.{?u.20842, u_2} D
inst✝ : Category.{?u.20846, u_3} E
F G H : C ⥤ Karoubi D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi C
h : (F.map P.p).f ≫ (NatTrans.app φ P.X).f = (NatTrans.app φ P.X).f ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
| (NatTrans.app φ' P.X).f
[PROOFSTEP]
rw [h']
[GOAL]
case w.h.h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.20838, u_1} C
inst✝¹ : Category.{?u.20842, u_2} D
inst✝ : Category.{?u.20846, u_3} E
F G H : C ⥤ Karoubi D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi C
h : (F.map P.p).f ≫ (NatTrans.app φ P.X).f = (NatTrans.app φ P.X).f ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
⊢ (F.map P.p).f ≫ (NatTrans.app φ P.X).f ≫ (NatTrans.app φ' P.X).f =
    ((F.map P.p).f ≫ (NatTrans.app φ P.X).f) ≫ (NatTrans.app φ' P.X).f
[PROOFSTEP]
simp only [assoc]
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
inst✝ : Category.{?u.29797, u_3} E
⊢ functorExtension₁ C D ⋙ (whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C) = 𝟭 (C ⥤ Karoubi D)
[PROOFSTEP]
refine' Functor.ext _ _
[GOAL]
case refine'_1
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
inst✝ : Category.{?u.29797, u_3} E
⊢ ∀ (X : C ⥤ Karoubi D),
    (functorExtension₁ C D ⋙ (whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C)).obj X =
      (𝟭 (C ⥤ Karoubi D)).obj X
[PROOFSTEP]
intro F
[GOAL]
case refine'_1
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
inst✝ : Category.{?u.29797, u_3} E
F : C ⥤ Karoubi D
⊢ (functorExtension₁ C D ⋙ (whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C)).obj F =
    (𝟭 (C ⥤ Karoubi D)).obj F
[PROOFSTEP]
refine' Functor.ext _ _
[GOAL]
case refine'_1.refine'_1
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
inst✝ : Category.{?u.29797, u_3} E
F : C ⥤ Karoubi D
⊢ ∀ (X : C),
    ((functorExtension₁ C D ⋙ (whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C)).obj F).obj X =
      ((𝟭 (C ⥤ Karoubi D)).obj F).obj X
[PROOFSTEP]
intro X
[GOAL]
case refine'_1.refine'_1
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
inst✝ : Category.{?u.29797, u_3} E
F : C ⥤ Karoubi D
X : C
⊢ ((functorExtension₁ C D ⋙ (whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C)).obj F).obj X =
    ((𝟭 (C ⥤ Karoubi D)).obj F).obj X
[PROOFSTEP]
ext
[GOAL]
case refine'_1.refine'_1.h_X
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
inst✝ : Category.{?u.29797, u_3} E
F : C ⥤ Karoubi D
X : C
⊢ (((functorExtension₁ C D ⋙ (whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C)).obj F).obj X).X =
    (((𝟭 (C ⥤ Karoubi D)).obj F).obj X).X
[PROOFSTEP]
simp
[GOAL]
case refine'_1.refine'_1.h_p
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
inst✝ : Category.{?u.29797, u_3} E
F : C ⥤ Karoubi D
X : C
⊢ (((functorExtension₁ C D ⋙ (whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C)).obj F).obj X).p ≫
      eqToHom (_ : (F.obj X).X = (F.obj X).X) =
    eqToHom (_ : (F.obj X).X = (F.obj X).X) ≫ (((𝟭 (C ⥤ Karoubi D)).obj F).obj X).p
[PROOFSTEP]
simp
[GOAL]
case refine'_1.refine'_2
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
inst✝ : Category.{?u.29797, u_3} E
F : C ⥤ Karoubi D
⊢ ∀ (X Y : C) (f : X ⟶ Y),
    ((functorExtension₁ C D ⋙ (whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C)).obj F).map f =
      eqToHom
          (_ :
            ((functorExtension₁ C D ⋙ (whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C)).obj F).obj X =
              ((𝟭 (C ⥤ Karoubi D)).obj F).obj X) ≫
        ((𝟭 (C ⥤ Karoubi D)).obj F).map f ≫
          eqToHom
            (_ :
              ((𝟭 (C ⥤ Karoubi D)).obj F).obj Y =
                ((functorExtension₁ C D ⋙ (whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C)).obj F).obj Y)
[PROOFSTEP]
aesop_cat
[GOAL]
case refine'_2
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
inst✝ : Category.{?u.29797, u_3} E
⊢ ∀ (X Y : C ⥤ Karoubi D) (f : X ⟶ Y),
    (functorExtension₁ C D ⋙ (whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C)).map f =
      eqToHom
          (_ :
            (functorExtension₁ C D ⋙ (whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C)).obj X =
              (𝟭 (C ⥤ Karoubi D)).obj X) ≫
        (𝟭 (C ⥤ Karoubi D)).map f ≫
          eqToHom
            (_ :
              (𝟭 (C ⥤ Karoubi D)).obj Y =
                (functorExtension₁ C D ⋙ (whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C)).obj Y)
[PROOFSTEP]
intro F G φ
[GOAL]
case refine'_2
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
inst✝ : Category.{?u.29797, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
⊢ (functorExtension₁ C D ⋙ (whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C)).map φ =
    eqToHom
        (_ :
          (functorExtension₁ C D ⋙ (whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C)).obj F =
            (𝟭 (C ⥤ Karoubi D)).obj F) ≫
      (𝟭 (C ⥤ Karoubi D)).map φ ≫
        eqToHom
          (_ :
            (𝟭 (C ⥤ Karoubi D)).obj G =
              (functorExtension₁ C D ⋙ (whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C)).obj G)
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.49904, u_1} C
inst✝¹ : Category.{?u.49908, u_2} D
inst✝ : Category.{?u.49912, u_3} E
G : Karoubi C ⥤ Karoubi D
P : Karoubi C
⊢ (G.map (decompId_p P)).f =
    ((((whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C) ⋙ functorExtension₁ C D).obj G).obj P).p ≫
      (G.map (decompId_p P)).f ≫ (((𝟭 (Karoubi C ⥤ Karoubi D)).obj G).obj P).p
[PROOFSTEP]
simpa only [hom_ext_iff, G.map_comp, G.map_id] using
  G.congr_map (show P.decompId_p = (toKaroubi C).map P.p ≫ P.decompId_p ≫ 𝟙 _ by simp)
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.49904, u_1} C
inst✝¹ : Category.{?u.49908, u_2} D
inst✝ : Category.{?u.49912, u_3} E
G : Karoubi C ⥤ Karoubi D
P : Karoubi C
⊢ decompId_p P = (toKaroubi C).map P.p ≫ decompId_p P ≫ 𝟙 P
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.49904, u_1} C
inst✝¹ : Category.{?u.49908, u_2} D
inst✝ : Category.{?u.49912, u_3} E
G : Karoubi C ⥤ Karoubi D
P Q : Karoubi C
f : P ⟶ Q
⊢ (((whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C) ⋙ functorExtension₁ C D).obj G).map f ≫
      (fun P => Hom.mk (G.map (decompId_p P)).f) Q =
    (fun P => Hom.mk (G.map (decompId_p P)).f) P ≫ ((𝟭 (Karoubi C ⥤ Karoubi D)).obj G).map f
[PROOFSTEP]
simpa only [hom_ext_iff, G.map_comp] using (G.congr_map (decompId_p_naturality f)).symm
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.49904, u_1} C
inst✝¹ : Category.{?u.49908, u_2} D
inst✝ : Category.{?u.49912, u_3} E
G : Karoubi C ⥤ Karoubi D
P : Karoubi C
⊢ (G.map (decompId_i P)).f =
    (((𝟭 (Karoubi C ⥤ Karoubi D)).obj G).obj P).p ≫
      (G.map (decompId_i P)).f ≫
        ((((whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C) ⋙ functorExtension₁ C D).obj G).obj P).p
[PROOFSTEP]
simpa only [hom_ext_iff, G.map_comp, G.map_id] using
  G.congr_map (show P.decompId_i = 𝟙 _ ≫ P.decompId_i ≫ (toKaroubi C).map P.p by simp)
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.49904, u_1} C
inst✝¹ : Category.{?u.49908, u_2} D
inst✝ : Category.{?u.49912, u_3} E
G : Karoubi C ⥤ Karoubi D
P : Karoubi C
⊢ decompId_i P = 𝟙 P ≫ decompId_i P ≫ (toKaroubi C).map P.p
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.49904, u_1} C
inst✝¹ : Category.{?u.49908, u_2} D
inst✝ : Category.{?u.49912, u_3} E
G : Karoubi C ⥤ Karoubi D
P Q : Karoubi C
f : P ⟶ Q
⊢ ((𝟭 (Karoubi C ⥤ Karoubi D)).obj G).map f ≫ (fun P => Hom.mk (G.map (decompId_i P)).f) Q =
    (fun P => Hom.mk (G.map (decompId_i P)).f) P ≫
      (((whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C) ⋙ functorExtension₁ C D).obj G).map f
[PROOFSTEP]
simpa only [hom_ext_iff, G.map_comp] using G.congr_map (decompId_i_naturality f)
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.49904, u_1} C
inst✝¹ : Category.{?u.49908, u_2} D
inst✝ : Category.{?u.49912, u_3} E
G : Karoubi C ⥤ Karoubi D
⊢ ((NatTrans.mk fun P => Hom.mk (G.map (decompId_p P)).f) ≫ NatTrans.mk fun P => Hom.mk (G.map (decompId_i P)).f) =
    𝟙 (((whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C) ⋙ functorExtension₁ C D).obj G)
[PROOFSTEP]
ext P
[GOAL]
case w.h.h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.49904, u_1} C
inst✝¹ : Category.{?u.49908, u_2} D
inst✝ : Category.{?u.49912, u_3} E
G : Karoubi C ⥤ Karoubi D
P : Karoubi C
⊢ (NatTrans.app
        ((NatTrans.mk fun P => Hom.mk (G.map (decompId_p P)).f) ≫ NatTrans.mk fun P => Hom.mk (G.map (decompId_i P)).f)
        P).f =
    (NatTrans.app (𝟙 (((whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C) ⋙ functorExtension₁ C D).obj G))
        P).f
[PROOFSTEP]
simpa only [hom_ext_iff, G.map_comp, G.map_id] using G.congr_map P.decomp_p.symm
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.49904, u_1} C
inst✝¹ : Category.{?u.49908, u_2} D
inst✝ : Category.{?u.49912, u_3} E
G : Karoubi C ⥤ Karoubi D
⊢ ((NatTrans.mk fun P => Hom.mk (G.map (decompId_i P)).f) ≫ NatTrans.mk fun P => Hom.mk (G.map (decompId_p P)).f) =
    𝟙 ((𝟭 (Karoubi C ⥤ Karoubi D)).obj G)
[PROOFSTEP]
ext P
[GOAL]
case w.h.h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.49904, u_1} C
inst✝¹ : Category.{?u.49908, u_2} D
inst✝ : Category.{?u.49912, u_3} E
G : Karoubi C ⥤ Karoubi D
P : Karoubi C
⊢ (NatTrans.app
        ((NatTrans.mk fun P => Hom.mk (G.map (decompId_i P)).f) ≫ NatTrans.mk fun P => Hom.mk (G.map (decompId_p P)).f)
        P).f =
    (NatTrans.app (𝟙 ((𝟭 (Karoubi C ⥤ Karoubi D)).obj G)) P).f
[PROOFSTEP]
simpa only [hom_ext_iff, G.map_comp, G.map_id] using G.congr_map P.decompId.symm
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.49904, u_1} C
inst✝¹ : Category.{?u.49908, u_2} D
inst✝ : Category.{?u.49912, u_3} E
X Y : Karoubi C ⥤ Karoubi D
φ : X ⟶ Y
⊢ ((whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C) ⋙ functorExtension₁ C D).map φ ≫
      ((fun G =>
            Iso.mk (NatTrans.mk fun P => Hom.mk (G.map (decompId_p P)).f)
              (NatTrans.mk fun P => Hom.mk (G.map (decompId_i P)).f))
          Y).hom =
    ((fun G =>
            Iso.mk (NatTrans.mk fun P => Hom.mk (G.map (decompId_p P)).f)
              (NatTrans.mk fun P => Hom.mk (G.map (decompId_i P)).f))
          X).hom ≫
      (𝟭 (Karoubi C ⥤ Karoubi D)).map φ
[PROOFSTEP]
ext P
[GOAL]
case w.h.h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.49904, u_1} C
inst✝¹ : Category.{?u.49908, u_2} D
inst✝ : Category.{?u.49912, u_3} E
X Y : Karoubi C ⥤ Karoubi D
φ : X ⟶ Y
P : Karoubi C
⊢ (NatTrans.app
        (((whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C) ⋙ functorExtension₁ C D).map φ ≫
          ((fun G =>
                Iso.mk (NatTrans.mk fun P => Hom.mk (G.map (decompId_p P)).f)
                  (NatTrans.mk fun P => Hom.mk (G.map (decompId_i P)).f))
              Y).hom)
        P).f =
    (NatTrans.app
        (((fun G =>
                Iso.mk (NatTrans.mk fun P => Hom.mk (G.map (decompId_p P)).f)
                  (NatTrans.mk fun P => Hom.mk (G.map (decompId_i P)).f))
              X).hom ≫
          (𝟭 (Karoubi C ⥤ Karoubi D)).map φ)
        P).f
[PROOFSTEP]
dsimp
[GOAL]
case w.h.h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.49904, u_1} C
inst✝¹ : Category.{?u.49908, u_2} D
inst✝ : Category.{?u.49912, u_3} E
X Y : Karoubi C ⥤ Karoubi D
φ : X ⟶ Y
P : Karoubi C
⊢ ((X.map ((toKaroubi C).map P.p)).f ≫ (NatTrans.app φ ((toKaroubi C).obj P.X)).f) ≫ (Y.map (decompId_p P)).f =
    (X.map (decompId_p P)).f ≫ (NatTrans.app φ P).f
[PROOFSTEP]
rw [natTrans_eq φ P, P.decomp_p]
[GOAL]
case w.h.h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.49904, u_1} C
inst✝¹ : Category.{?u.49908, u_2} D
inst✝ : Category.{?u.49912, u_3} E
X Y : Karoubi C ⥤ Karoubi D
φ : X ⟶ Y
P : Karoubi C
⊢ ((X.map (decompId_p P ≫ decompId_i P)).f ≫ (NatTrans.app φ ((toKaroubi C).obj P.X)).f) ≫ (Y.map (decompId_p P)).f =
    (X.map (decompId_p P)).f ≫ (X.map (decompId_i P) ≫ NatTrans.app φ (Karoubi.mk P.X (𝟙 P.X)) ≫ Y.map (decompId_p P)).f
[PROOFSTEP]
simp only [Functor.map_comp, comp_f, assoc]
[GOAL]
case w.h.h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.49904, u_1} C
inst✝¹ : Category.{?u.49908, u_2} D
inst✝ : Category.{?u.49912, u_3} E
X Y : Karoubi C ⥤ Karoubi D
φ : X ⟶ Y
P : Karoubi C
⊢ (X.map (decompId_p P)).f ≫
      (X.map (decompId_i P)).f ≫ (NatTrans.app φ ((toKaroubi C).obj P.X)).f ≫ (Y.map (decompId_p P)).f =
    (X.map (decompId_p P)).f ≫
      (X.map (decompId_i P)).f ≫ (NatTrans.app φ (Karoubi.mk P.X (𝟙 P.X))).f ≫ (Y.map (decompId_p P)).f
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.61683, u_1} C
inst✝¹ : Category.{?u.61687, u_2} D
inst✝ : Category.{?u.61691, u_3} E
F : C ⥤ Karoubi D
⊢ (functorExtension₁ C D).map (NatTrans.app (functorExtension₁_comp_whiskeringLeft_toKaroubi_iso C D).symm.hom F) ≫
      NatTrans.app (KaroubiUniversal₁.counitIso C D).hom ((functorExtension₁ C D).obj F) =
    𝟙 ((functorExtension₁ C D).obj F)
[PROOFSTEP]
ext P
[GOAL]
case w.h.h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.61683, u_1} C
inst✝¹ : Category.{?u.61687, u_2} D
inst✝ : Category.{?u.61691, u_3} E
F : C ⥤ Karoubi D
P : Karoubi C
⊢ (NatTrans.app
        ((functorExtension₁ C D).map
            (NatTrans.app (functorExtension₁_comp_whiskeringLeft_toKaroubi_iso C D).symm.hom F) ≫
          NatTrans.app (KaroubiUniversal₁.counitIso C D).hom ((functorExtension₁ C D).obj F))
        P).f =
    (NatTrans.app (𝟙 ((functorExtension₁ C D).obj F)) P).f
[PROOFSTEP]
dsimp [FunctorExtension₁.map, KaroubiUniversal₁.counitIso]
[GOAL]
case w.h.h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.61683, u_1} C
inst✝¹ : Category.{?u.61687, u_2} D
inst✝ : Category.{?u.61691, u_3} E
F : C ⥤ Karoubi D
P : Karoubi C
⊢ ((F.map P.p).f ≫
        (NatTrans.app
            (NatTrans.app
              (eqToHom
                (_ :
                  𝟭 (C ⥤ Karoubi D) =
                    functorExtension₁ C D ⋙ (whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C)))
              F)
            P.X).f) ≫
      (F.map P.p).f =
    (F.map P.p).f
[PROOFSTEP]
simp only [eqToHom_app, Functor.id_obj, Functor.comp_obj, functorExtension₁_obj, whiskeringLeft_obj_obj, eqToHom_f,
  FunctorExtension₁.obj_obj_X, toKaroubi_obj_X, eqToHom_refl, comp_id, comp_p, ← comp_f, ← F.map_comp, P.idem]
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
inst✝ : Category.{u_6, u_3} E
F : C ⥤ Karoubi D
G : D ⥤ Karoubi E
⊢ (functorExtension₁ C E).obj (F ⋙ (functorExtension₁ D E).obj G) =
    (functorExtension₁ C D).obj F ⋙ (functorExtension₁ D E).obj G
[PROOFSTEP]
refine' Functor.ext _ _
[GOAL]
case refine'_1
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
inst✝ : Category.{u_6, u_3} E
F : C ⥤ Karoubi D
G : D ⥤ Karoubi E
⊢ ∀ (X : Karoubi C),
    ((functorExtension₁ C E).obj (F ⋙ (functorExtension₁ D E).obj G)).obj X =
      ((functorExtension₁ C D).obj F ⋙ (functorExtension₁ D E).obj G).obj X
[PROOFSTEP]
aesop_cat
[GOAL]
case refine'_2
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
inst✝ : Category.{u_6, u_3} E
F : C ⥤ Karoubi D
G : D ⥤ Karoubi E
⊢ ∀ (X Y : Karoubi C) (f : X ⟶ Y),
    ((functorExtension₁ C E).obj (F ⋙ (functorExtension₁ D E).obj G)).map f =
      eqToHom
          (_ :
            ((functorExtension₁ C E).obj (F ⋙ (functorExtension₁ D E).obj G)).obj X =
              ((functorExtension₁ C D).obj F ⋙ (functorExtension₁ D E).obj G).obj X) ≫
        ((functorExtension₁ C D).obj F ⋙ (functorExtension₁ D E).obj G).map f ≫
          eqToHom
            (_ :
              ((functorExtension₁ C D).obj F ⋙ (functorExtension₁ D E).obj G).obj Y =
                ((functorExtension₁ C E).obj (F ⋙ (functorExtension₁ D E).obj G)).obj Y)
[PROOFSTEP]
intro X Y f
[GOAL]
case refine'_2
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
inst✝ : Category.{u_6, u_3} E
F : C ⥤ Karoubi D
G : D ⥤ Karoubi E
X Y : Karoubi C
f : X ⟶ Y
⊢ ((functorExtension₁ C E).obj (F ⋙ (functorExtension₁ D E).obj G)).map f =
    eqToHom
        (_ :
          ((functorExtension₁ C E).obj (F ⋙ (functorExtension₁ D E).obj G)).obj X =
            ((functorExtension₁ C D).obj F ⋙ (functorExtension₁ D E).obj G).obj X) ≫
      ((functorExtension₁ C D).obj F ⋙ (functorExtension₁ D E).obj G).map f ≫
        eqToHom
          (_ :
            ((functorExtension₁ C D).obj F ⋙ (functorExtension₁ D E).obj G).obj Y =
              ((functorExtension₁ C E).obj (F ⋙ (functorExtension₁ D E).obj G)).obj Y)
[PROOFSTEP]
ext
[GOAL]
case refine'_2.h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
inst✝ : Category.{u_6, u_3} E
F : C ⥤ Karoubi D
G : D ⥤ Karoubi E
X Y : Karoubi C
f : X ⟶ Y
⊢ (((functorExtension₁ C E).obj (F ⋙ (functorExtension₁ D E).obj G)).map f).f =
    (eqToHom
          (_ :
            ((functorExtension₁ C E).obj (F ⋙ (functorExtension₁ D E).obj G)).obj X =
              ((functorExtension₁ C D).obj F ⋙ (functorExtension₁ D E).obj G).obj X) ≫
        ((functorExtension₁ C D).obj F ⋙ (functorExtension₁ D E).obj G).map f ≫
          eqToHom
            (_ :
              ((functorExtension₁ C D).obj F ⋙ (functorExtension₁ D E).obj G).obj Y =
                ((functorExtension₁ C E).obj (F ⋙ (functorExtension₁ D E).obj G)).obj Y)).f
[PROOFSTEP]
simp only [eqToHom_refl, id_comp, comp_id]
[GOAL]
case refine'_2.h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
inst✝ : Category.{u_6, u_3} E
F : C ⥤ Karoubi D
G : D ⥤ Karoubi E
X Y : Karoubi C
f : X ⟶ Y
⊢ (((functorExtension₁ C E).obj (F ⋙ (functorExtension₁ D E).obj G)).map f).f =
    (((functorExtension₁ C D).obj F ⋙ (functorExtension₁ D E).obj G).map f).f
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
inst✝ : Category.{?u.72126, u_3} E
⊢ functorExtension₂ C D ⋙ (whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C) =
    (whiskeringRight C D (Karoubi D)).obj (toKaroubi D)
[PROOFSTEP]
simp only [functorExtension₂, Functor.assoc, functorExtension₁_comp_whiskeringLeft_toKaroubi, Functor.comp_id]
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝³ : Category.{?u.76565, u_1} C
inst✝² : Category.{?u.76569, u_2} D
inst✝¹ : Category.{?u.76573, u_3} E
inst✝ : IsIdempotentComplete D
⊢ IsEquivalence (functorExtension₂ C D)
[PROOFSTEP]
rw [← karoubiUniversal₂_functor_eq]
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝³ : Category.{?u.76565, u_1} C
inst✝² : Category.{?u.76569, u_2} D
inst✝¹ : Category.{?u.76573, u_3} E
inst✝ : IsIdempotentComplete D
⊢ IsEquivalence (karoubiUniversal₂ C D).functor
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝³ : Category.{?u.81595, u_1} C
inst✝² : Category.{?u.81599, u_2} D
inst✝¹ : Category.{?u.81603, u_3} E
inst✝ : IsIdempotentComplete D
⊢ IsEquivalence (functorExtension C D)
[PROOFSTEP]
rw [← karoubiUniversal_functor_eq]
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝³ : Category.{?u.81595, u_1} C
inst✝² : Category.{?u.81599, u_2} D
inst✝¹ : Category.{?u.81603, u_3} E
inst✝ : IsIdempotentComplete D
⊢ IsEquivalence (karoubiUniversal C D).functor
[PROOFSTEP]
infer_instance
  -- porting note: added to avoid a timeout in the following definition
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_5, u_2} D
inst✝¹ : Category.{?u.82137, u_3} E
inst✝ : IsIdempotentComplete D
⊢ (whiskeringLeft C (Karoubi C) D).obj (toKaroubi C) ⋙
      (whiskeringRight C D (Karoubi D)).obj (toKaroubi D) ⋙
        (whiskeringRight C (Karoubi D) D).obj (Functor.inv (toKaroubi D)) =
    (karoubiUniversal C D).inverse
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝³ : Category.{?u.84023, u_1} C
inst✝² : Category.{?u.84027, u_2} D
inst✝¹ : Category.{?u.84031, u_3} E
inst✝ : IsIdempotentComplete D
⊢ IsEquivalence
    ((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C) ⋙
      (whiskeringRight C D (Karoubi D)).obj (toKaroubi D) ⋙
        (whiskeringRight C (Karoubi D) D).obj (Functor.inv (toKaroubi D)))
[PROOFSTEP]
rw [isEquivalence_whiskeringLeft_obj_toKaroubi_aux]
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝³ : Category.{?u.84023, u_1} C
inst✝² : Category.{?u.84027, u_2} D
inst✝¹ : Category.{?u.84031, u_3} E
inst✝ : IsIdempotentComplete D
⊢ IsEquivalence (karoubiUniversal C D).inverse
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_5, u_2} D
inst✝¹ : Category.{?u.87671, u_3} E
inst✝ : IsIdempotentComplete D
F G : Karoubi C ⥤ D
τ : toKaroubi C ⋙ F ⟶ toKaroubi C ⋙ G
P : Karoubi C
⊢ NatTrans.app (((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).preimage τ) P =
    F.map (decompId_i P) ≫ NatTrans.app τ P.X ≫ G.map (decompId_p P)
[PROOFSTEP]
rw [natTrans_eq]
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_5, u_2} D
inst✝¹ : Category.{?u.87671, u_3} E
inst✝ : IsIdempotentComplete D
F G : Karoubi C ⥤ D
τ : toKaroubi C ⋙ F ⟶ toKaroubi C ⋙ G
P : Karoubi C
⊢ F.map (decompId_i P) ≫
      NatTrans.app (((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).preimage τ) (Karoubi.mk P.X (𝟙 P.X)) ≫
        G.map (decompId_p P) =
    F.map (decompId_i P) ≫ NatTrans.app τ P.X ≫ G.map (decompId_p P)
[PROOFSTEP]
congr 2
[GOAL]
case e_a.e_a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_5, u_2} D
inst✝¹ : Category.{?u.87671, u_3} E
inst✝ : IsIdempotentComplete D
F G : Karoubi C ⥤ D
τ : toKaroubi C ⋙ F ⟶ toKaroubi C ⋙ G
P : Karoubi C
⊢ NatTrans.app (((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).preimage τ) (Karoubi.mk P.X (𝟙 P.X)) =
    NatTrans.app τ P.X
[PROOFSTEP]
rw [← congr_app (((whiskeringLeft _ _ _).obj (toKaroubi _)).image_preimage τ) P.X]
[GOAL]
case e_a.e_a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_5, u_2} D
inst✝¹ : Category.{?u.87671, u_3} E
inst✝ : IsIdempotentComplete D
F G : Karoubi C ⥤ D
τ : toKaroubi C ⋙ F ⟶ toKaroubi C ⋙ G
P : Karoubi C
⊢ NatTrans.app (((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).preimage τ) (Karoubi.mk P.X (𝟙 P.X)) =
    NatTrans.app
      (((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).map
        (((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).preimage τ))
      P.X
[PROOFSTEP]
dsimp
[GOAL]
case e_a.e_a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_5, u_2} D
inst✝¹ : Category.{?u.87671, u_3} E
inst✝ : IsIdempotentComplete D
F G : Karoubi C ⥤ D
τ : toKaroubi C ⋙ F ⟶ toKaroubi C ⋙ G
P : Karoubi C
⊢ NatTrans.app (((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).preimage τ) (Karoubi.mk P.X (𝟙 P.X)) =
    NatTrans.app (((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).preimage τ) ((toKaroubi C).obj P.X)
[PROOFSTEP]
congr