[GOAL]
α✝ : Sort u_1
β : Sort u_2
α : Sort u_3
r : α → α → Prop
iseqv✝¹ : Equivalence r
p : α → α → Prop
iseqv✝ : Equivalence p
Eq : ∀ (a b : α), Setoid.r a b ↔ Setoid.r a b
⊢ { r := r, iseqv := iseqv✝¹ } = { r := p, iseqv := iseqv✝ }
[PROOFSTEP]
have : r = p := funext fun a ↦ funext fun b ↦ propext <| Eq a b
[GOAL]
α✝ : Sort u_1
β : Sort u_2
α : Sort u_3
r : α → α → Prop
iseqv✝¹ : Equivalence r
p : α → α → Prop
iseqv✝ : Equivalence p
Eq : ∀ (a b : α), Setoid.r a b ↔ Setoid.r a b
this : r = p
⊢ { r := r, iseqv := iseqv✝¹ } = { r := p, iseqv := iseqv✝ }
[PROOFSTEP]
subst this
[GOAL]
α✝ : Sort u_1
β : Sort u_2
α : Sort u_3
r : α → α → Prop
iseqv✝¹ iseqv✝ : Equivalence r
Eq : ∀ (a b : α), Setoid.r a b ↔ Setoid.r a b
⊢ { r := r, iseqv := iseqv✝¹ } = { r := r, iseqv := iseqv✝ }
[PROOFSTEP]
rfl
[GOAL]
α : Sort u_1
β : Sort u_2
ra : α → α → Prop
rb : β → β → Prop
φ : Quot ra → Quot rb → Sort u_3
qa : Quot ra
qb : Quot rb
f : (a : α) → (b : β) → φ (mk ra a) (mk rb b)
ca : ∀ {b : β} {a₁ a₂ : α}, ra a₁ a₂ → HEq (f a₁ b) (f a₂ b)
cb : ∀ {a : α} {b₁ b₂ : β}, rb b₁ b₂ → HEq (f a b₁) (f a b₂)
a₁ a₂ : α
pa : ra a₁ a₂
b : β
⊢ HEq (Quot.hrecOn (mk rb b) (f a₁) (_ : ∀ {b₁ b₂ : β}, rb b₁ b₂ → HEq (f a₁ b₁) (f a₁ b₂))) (f a₁ b)
[PROOFSTEP]
simp [heq_self_iff_true]
[GOAL]
α : Sort u_1
β : Sort u_2
ra : α → α → Prop
rb : β → β → Prop
φ : Quot ra → Quot rb → Sort u_3
qa : Quot ra
qb : Quot rb
f : (a : α) → (b : β) → φ (mk ra a) (mk rb b)
ca : ∀ {b : β} {a₁ a₂ : α}, ra a₁ a₂ → HEq (f a₁ b) (f a₂ b)
cb : ∀ {a : α} {b₁ b₂ : β}, rb b₁ b₂ → HEq (f a b₁) (f a b₂)
a₁ a₂ : α
pa : ra a₁ a₂
b : β
h₁ : HEq (Quot.hrecOn (mk rb b) (f a₁) (_ : ∀ {b₁ b₂ : β}, rb b₁ b₂ → HEq (f a₁ b₁) (f a₁ b₂))) (f a₁ b)
⊢ HEq (f a₂ b) (Quot.hrecOn (mk rb b) (f a₂) (_ : ∀ {b₁ b₂ : β}, rb b₁ b₂ → HEq (f a₂ b₁) (f a₂ b₂)))
[PROOFSTEP]
simp [heq_self_iff_true]
[GOAL]
α : Sort u_1
β : Sort u_2
s : Setoid α
x : α
y : Quotient s
⊢ Quotient.mk s x = y ↔ x ≈ out y
[PROOFSTEP]
refine' Iff.trans _ Quotient.eq
[GOAL]
α : Sort u_1
β : Sort u_2
s : Setoid α
x : α
y : Quotient s
⊢ Quotient.mk s x = y ↔ Quotient.mk s x = Quotient.mk s (out y)
[PROOFSTEP]
rw [Quotient.out_eq y]
[GOAL]
α : Sort u_1
β : Sort u_2
s : Setoid α
x : Quotient s
y : α
⊢ x = Quotient.mk s y ↔ out x ≈ y
[PROOFSTEP]
refine' Iff.trans _ Quotient.eq
[GOAL]
α : Sort u_1
β : Sort u_2
s : Setoid α
x : Quotient s
y : α
⊢ x = Quotient.mk s y ↔ Quotient.mk s (out x) = Quotient.mk s y
[PROOFSTEP]
rw [Quotient.out_eq x]
[GOAL]
α : Sort u_1
β : Sort u_2
s : Setoid α
x y : Quotient s
⊢ out x ≈ out y ↔ x = y
[PROOFSTEP]
rw [← Quotient.eq_mk_iff_out, Quotient.out_eq]
[GOAL]
α✝ : Sort u_1
β : Sort u_2
ι : Type u_3
α : ι → Type u_4
S : (i : ι) → Setoid (α i)
f : (i : ι) → Quotient (S i)
⊢ Setoid ((i : ι) → α i)
[PROOFSTEP]
infer_instance
[GOAL]
α✝ : Sort u_1
β : Sort u_2
ι : Type u_3
α : ι → Sort u_4
s : (i : ι) → Setoid (α i)
p : ((i : ι) → Quotient (s i)) → Prop
f : (i : ι) → Quotient (s i)
h : ∀ (a : (i : ι) → α i), p fun i => Quotient.mk (s i) (a i)
⊢ p f
[PROOFSTEP]
rw [← (funext fun i ↦ Quotient.out_eq (f i) : (fun i ↦ ⟦(f i).out⟧) = f)]
[GOAL]
α✝ : Sort u_1
β : Sort u_2
ι : Type u_3
α : ι → Sort u_4
s : (i : ι) → Setoid (α i)
p : ((i : ι) → Quotient (s i)) → Prop
f : (i : ι) → Quotient (s i)
h : ∀ (a : (i : ι) → α i), p fun i => Quotient.mk (s i) (a i)
⊢ p fun i => Quotient.mk (s i) (out (f i))
[PROOFSTEP]
apply h
