J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
inst✝ : Nonempty J
j₀ : J
h : ∀ (p : Set J), j₀ ∈ p → (∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)) → ∀ (j : J), j ∈ p
α : Type u₁
F : J → α
a : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → F j₁ = F j₂
w : ∀ (j : J), j ∈ {j | F j = F j₀}
⊢ ∀ (j j' : J), F j = F j'
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
inst✝ : Nonempty J
j₀ : J
h : ∀ (p : Set J), j₀ ∈ p → (∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)) → ∀ (j : J), j ∈ p
α : Type u₁
F : J → α
a : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → F j₁ = F j₂
⊢ ∀ (j j' : J), F j = F j'
have w := h { j | F j = F j₀ } rfl (fun {j₁} {j₂} f => by
  change F j₁ = F j₀ ↔ F j₂ = F j₀
  simp [a f];)
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
inst✝ : Nonempty J
j₀ : J
h : ∀ (p : Set J), j₀ ∈ p → (∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)) → ∀ (j : J), j ∈ p
α : Type u₁
F : J → α
a : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → F j₁ = F j₂
w : ∀ (j : J), j ∈ {j | F j = F j₀}
⊢ ∀ (j j' : J), F j = F j'
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
inst✝ : Nonempty J
j₀ : J
h : ∀ (p : Set J), j₀ ∈ p → (∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)) → ∀ (j : J), j ∈ p
α : Type u₁
F : J → α
a : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → F j₁ = F j₂
w : ∀ (j : J), j ∈ {j | F j = F j₀}
⊢ ∀ (j j' : J), F j = F j'
dsimp at w
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
inst✝ : Nonempty J
j₀ : J
h : ∀ (p : Set J), j₀ ∈ p → (∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)) → ∀ (j : J), j ∈ p
α : Type u₁
F : J → α
a : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → F j₁ = F j₂
w : ∀ (j : J), j ∈ {j | F j = F j₀}
j j' : J
⊢ F j = F j'
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
inst✝ : Nonempty J
j₀ : J
h : ∀ (p : Set J), j₀ ∈ p → (∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)) → ∀ (j : J), j ∈ p
α : Type u₁
F : J → α
a : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → F j₁ = F j₂
w : ∀ (j : J), j ∈ {j | F j = F j₀}
⊢ ∀ (j j' : J), F j = F j'
intro j j'
no goals
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
inst✝ : Nonempty J
j₀ : J
h : ∀ (p : Set J), j₀ ∈ p → (∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)) → ∀ (j : J), j ∈ p
α : Type u₁
F : J → α
a : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → F j₁ = F j₂
w : ∀ (j : J), j ∈ {j | F j = F j₀}
j j' : J
⊢ F j = F j'
rw [w j, w j']
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
inst✝ : Nonempty J
j₀ : J
h : ∀ (p : Set J), j₀ ∈ p → (∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)) → ∀ (j : J), j ∈ p
α : Type u₁
F : J → α
a : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → F j₁ = F j₂
j₁ j₂ : J
f : j₁ ⟶ j₂
⊢ F j₁ = F j₀ ↔ F j₂ = F j₀
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
inst✝ : Nonempty J
j₀ : J
h : ∀ (p : Set J), j₀ ∈ p → (∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)) → ∀ (j : J), j ∈ p
α : Type u₁
F : J → α
a : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → F j₁ = F j₂
j₁ j₂ : J
f : j₁ ⟶ j₂
⊢ j₁ ∈ {j | F j = F j₀} ↔ j₂ ∈ {j | F j = F j₀}
change F j₁ = F j₀ ↔ F j₂ = F j₀
no goals
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
inst✝ : Nonempty J
j₀ : J
h : ∀ (p : Set J), j₀ ∈ p → (∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)) → ∀ (j : J), j ∈ p
α : Type u₁
F : J → α
a : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → F j₁ = F j₂
j₁ j₂ : J
f : j₁ ⟶ j₂
⊢ F j₁ = F j₀ ↔ F j₂ = F j₀
simp [a f]