α : Type u_1
β : Type u_2
γ : Type ?u.300743
ι : Sort ?u.300746
ι' : Sort ?u.300749
ι₂ : Sort ?u.300752
κ : ι → Sort ?u.300757
κ₁ : ι → Sort ?u.300762
κ₂ : ι → Sort ?u.300767
κ' : ι' → Sort ?u.300772
t : α → Set β
h : ∀ (i j : α), i ≠ j → Disjoint (t i) (t j)
a₁ : α
b₁ : β
h₁ : b₁ ∈ t a₁
a₂ : α
a_eq : a₁ = a₂
h₂ : b₁ ∈ t a₂
eq :
  sigmaToiUnion t { fst := a₁, snd := { val := b₁, property := h₁ } } =
    sigmaToiUnion t { fst := a₂, snd := { val := b₁, property := h₂ } }
⊢ ↑(Eq.recOn a_eq { fst := a₁, snd := { val := b₁, property := h₁ } }.snd) =
    ↑{ fst := a₂, snd := { val := b₁, property := h₂ } }.snd
α : Type u_1
β : Type u_2
γ : Type ?u.300743
ι : Sort ?u.300746
ι' : Sort ?u.300749
ι₂ : Sort ?u.300752
κ : ι → Sort ?u.300757
κ₁ : ι → Sort ?u.300762
κ₂ : ι → Sort ?u.300767
κ' : ι' → Sort ?u.300772
t : α → Set β
h : ∀ (i j : α), i ≠ j → Disjoint (t i) (t j)
a₁ : α
b₁ : β
h₁ : b₁ ∈ t a₁
a₂ : α
b₂ : β
h₂ : b₂ ∈ t a₂
eq :
  sigmaToiUnion t { fst := a₁, snd := { val := b₁, property := h₁ } } =
    sigmaToiUnion t { fst := a₂, snd := { val := b₂, property := h₂ } }
b_eq : b₁ = b₂
a_eq : a₁ = a₂
⊢ ↑(Eq.recOn a_eq { fst := a₁, snd := { val := b₁, property := h₁ } }.snd) =
    ↑{ fst := a₂, snd := { val := b₂, property := h₂ } }.snd
subst b_eq
α : Type u_1
β : Type u_2
γ : Type ?u.300743
ι : Sort ?u.300746
ι' : Sort ?u.300749
ι₂ : Sort ?u.300752
κ : ι → Sort ?u.300757
κ₁ : ι → Sort ?u.300762
κ₂ : ι → Sort ?u.300767
κ' : ι' → Sort ?u.300772
t : α → Set β
h : ∀ (i j : α), i ≠ j → Disjoint (t i) (t j)
a₁ : α
b₁ : β
h₁ h₂ : b₁ ∈ t a₁
eq :
  sigmaToiUnion t { fst := a₁, snd := { val := b₁, property := h₁ } } =
    sigmaToiUnion t { fst := a₁, snd := { val := b₁, property := h₂ } }
⊢ ↑(Eq.recOn (_ : a₁ = a₁) { fst := a₁, snd := { val := b₁, property := h₁ } }.snd) =
    ↑{ fst := a₁, snd := { val := b₁, property := h₂ } }.snd
α : Type u_1
β : Type u_2
γ : Type ?u.300743
ι : Sort ?u.300746
ι' : Sort ?u.300749
ι₂ : Sort ?u.300752
κ : ι → Sort ?u.300757
κ₁ : ι → Sort ?u.300762
κ₂ : ι → Sort ?u.300767
κ' : ι' → Sort ?u.300772
t : α → Set β
h : ∀ (i j : α), i ≠ j → Disjoint (t i) (t j)
a₁ : α
b₁ : β
h₁ : b₁ ∈ t a₁
a₂ : α
a_eq : a₁ = a₂
h₂ : b₁ ∈ t a₂
eq :
  sigmaToiUnion t { fst := a₁, snd := { val := b₁, property := h₁ } } =
    sigmaToiUnion t { fst := a₂, snd := { val := b₁, property := h₂ } }
⊢ ↑(Eq.recOn a_eq { fst := a₁, snd := { val := b₁, property := h₁ } }.snd) =
    ↑{ fst := a₂, snd := { val := b₁, property := h₂ } }.snd
subst a_eq
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.300743
ι : Sort ?u.300746
ι' : Sort ?u.300749
ι₂ : Sort ?u.300752
κ : ι → Sort ?u.300757
κ₁ : ι → Sort ?u.300762
κ₂ : ι → Sort ?u.300767
κ' : ι' → Sort ?u.300772
t : α → Set β
h : ∀ (i j : α), i ≠ j → Disjoint (t i) (t j)
a₁ : α
b₁ : β
h₁ h₂ : b₁ ∈ t a₁
eq :
  sigmaToiUnion t { fst := a₁, snd := { val := b₁, property := h₁ } } =
    sigmaToiUnion t { fst := a₁, snd := { val := b₁, property := h₂ } }
⊢ ↑(Eq.recOn (_ : a₁ = a₁) { fst := a₁, snd := { val := b₁, property := h₁ } }.snd) =
    ↑{ fst := a₁, snd := { val := b₁, property := h₂ } }.snd
rfl