case h
α : Type u_1
β : Type u_2
γ : Type ?u.38357
f : α → β
b : β
x y : α
⊢ b ∈ map f (Quotient.mk (Rel.setoid α) (x, y)) ↔ ∃ a, a ∈ Quotient.mk (Rel.setoid α) (x, y) ∧ f a = b
α : Type u_1
β : Type u_2
γ : Type ?u.38357
f : α → β
b : β
z : Sym2 α
⊢ b ∈ map f z ↔ ∃ a, a ∈ z ∧ f a = b
induction' z using Sym2.ind with x y
case h
α : Type u_1
β : Type u_2
γ : Type ?u.38357
f : α → β
b : β
x y : α
⊢ b = f x ∨ b = f y ↔ ∃ a, (a = x ∨ a = y) ∧ f a = b
case h
α : Type u_1
β : Type u_2
γ : Type ?u.38357
f : α → β
b : β
x y : α
⊢ b ∈ map f (Quotient.mk (Rel.setoid α) (x, y)) ↔ ∃ a, a ∈ Quotient.mk (Rel.setoid α) (x, y) ∧ f a = b
simp only [map, Quotient.map_mk, Prod.map_mk, mem_iff]
case h.mp
α : Type u_1
β : Type u_2
γ : Type ?u.38357
f : α → β
b : β
x y : α
⊢ b = f x ∨ b = f y → ∃ a, (a = x ∨ a = y) ∧ f a = b

case h.mpr
α : Type u_1
β : Type u_2
γ : Type ?u.38357
f : α → β
b : β
x y : α
⊢ (∃ a, (a = x ∨ a = y) ∧ f a = b) → b = f x ∨ b = f y
case h
α : Type u_1
β : Type u_2
γ : Type ?u.38357
f : α → β
b : β
x y : α
⊢ b = f x ∨ b = f y ↔ ∃ a, (a = x ∨ a = y) ∧ f a = b
constructor
case h.mp.inl
α : Type u_1
β : Type u_2
γ : Type ?u.38357
f : α → β
x y : α
⊢ ∃ a, (a = x ∨ a = y) ∧ f a = f x

case h.mp.inr
α : Type u_1
β : Type u_2
γ : Type ?u.38357
f : α → β
x y : α
⊢ ∃ a, (a = x ∨ a = y) ∧ f a = f y
case h.mp
α : Type u_1
β : Type u_2
γ : Type ?u.38357
f : α → β
b : β
x y : α
⊢ b = f x ∨ b = f y → ∃ a, (a = x ∨ a = y) ∧ f a = b
rintro (rfl | rfl)
no goals
case h.mp.inl
α : Type u_1
β : Type u_2
γ : Type ?u.38357
f : α → β
x y : α
⊢ ∃ a, (a = x ∨ a = y) ∧ f a = f x
exact ⟨x, by simp⟩
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.38357
f : α → β
x y : α
⊢ (x = x ∨ x = y) ∧ f x = f x
simp
no goals
case h.mp.inr
α : Type u_1
β : Type u_2
γ : Type ?u.38357
f : α → β
x y : α
⊢ ∃ a, (a = x ∨ a = y) ∧ f a = f y
exact ⟨y, by simp⟩
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.38357
f : α → β
x y : α
⊢ (y = x ∨ y = y) ∧ f y = f y
simp
no goals
case h.mpr
α : Type u_1
β : Type u_2
γ : Type ?u.38357
f : α → β
b : β
x y : α
⊢ (∃ a, (a = x ∨ a = y) ∧ f a = b) → b = f x ∨ b = f y
rintro ⟨w, rfl | rfl, rfl⟩ <;> simp