Theorem: Equiv.exists_bijOn (Matroid/ForMathlib/Other.lean)

State before:
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
inst✝ : Nonempty β
s : Set α
t : Set β
e : ↑s ≃ ↑t
⊢ ∃ f, BijOn f s t ∧ ∀ (x : ↑s), ↑(e x) = f ↑x
Tactic:
use fun x ↦ if hx : x ∈ s then e ⟨x,hx⟩ else Classical.arbitrary β
State after:
case h
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
inst✝ : Nonempty β
s : Set α
t : Set β
e : ↑s ≃ ↑t
⊢ BijOn (fun x => if hx : x ∈ s then ↑(e ⟨x, hx⟩) else Classical.arbitrary β) s t ∧
    ∀ (x : ↑s), ↑(e x) = if hx : ↑x ∈ s then ↑(e ⟨↑x, hx⟩) else Classical.arbitrary β

State before:
case h
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
inst✝ : Nonempty β
s : Set α
t : Set β
e : ↑s ≃ ↑t
⊢ BijOn (fun x => if hx : x ∈ s then ↑(e ⟨x, hx⟩) else Classical.arbitrary β) s t ∧
    ∀ (x : ↑s), ↑(e x) = if hx : ↑x ∈ s then ↑(e ⟨↑x, hx⟩) else Classical.arbitrary β
Tactic:
refine ⟨BijOn.mk (fun x hx ↦ ?_) (fun x hx y hy hxy ↦ ?_) (fun y hy ↦ ⟨e.symm ⟨y, hy⟩, by simp⟩),
  by simp⟩
State after:
case h.refine_1
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
inst✝ : Nonempty β
s : Set α
t : Set β
e : ↑s ≃ ↑t
x : α
hx : x ∈ s
⊢ (if hx : x ∈ s then ↑(e ⟨x, hx⟩) else Classical.arbitrary β) ∈ t

case h.refine_2
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
inst✝ : Nonempty β
s : Set α
t : Set β
e : ↑s ≃ ↑t
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy :
  (if hx : x ∈ s then ↑(e ⟨x, hx⟩) else Classical.arbitrary β) =
    if hx : y ∈ s then ↑(e ⟨y, hx⟩) else Classical.arbitrary β
⊢ x = y

State before:
case h.refine_2
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
inst✝ : Nonempty β
s : Set α
t : Set β
e : ↑s ≃ ↑t
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy :
  (if hx : x ∈ s then ↑(e ⟨x, hx⟩) else Classical.arbitrary β) =
    if hx : y ∈ s then ↑(e ⟨y, hx⟩) else Classical.arbitrary β
⊢ x = y
Tactic:
simpa [dif_pos hx, dif_pos hy, Subtype.coe_inj] using hxy
State after:
no goals

State before:
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
inst✝ : Nonempty β
s : Set α
t : Set β
e : ↑s ≃ ↑t
y : β
hy : y ∈ t
⊢ ↑(e.symm ⟨y, hy⟩) ∈ s ∧ (fun x => if hx : x ∈ s then ↑(e ⟨x, hx⟩) else Classical.arbitrary β) ↑(e.symm ⟨y, hy⟩) = y
Tactic:
simp
State after:
no goals

State before:
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
inst✝ : Nonempty β
s : Set α
t : Set β
e : ↑s ≃ ↑t
⊢ ∀ (x : ↑s), ↑(e x) = if hx : ↑x ∈ s then ↑(e ⟨↑x, hx⟩) else Classical.arbitrary β
Tactic:
simp
State after:
no goals

State before:
case h.refine_1
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
inst✝ : Nonempty β
s : Set α
t : Set β
e : ↑s ≃ ↑t
x : α
hx : x ∈ s
⊢ (if hx : x ∈ s then ↑(e ⟨x, hx⟩) else Classical.arbitrary β) ∈ t
Tactic:
rw [dif_pos hx]
State after:
case h.refine_1
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
inst✝ : Nonempty β
s : Set α
t : Set β
e : ↑s ≃ ↑t
x : α
hx : x ∈ s
⊢ ↑(e ⟨x, hx⟩) ∈ t

State before:
case h.refine_1
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
inst✝ : Nonempty β
s : Set α
t : Set β
e : ↑s ≃ ↑t
x : α
hx : x ∈ s
⊢ ↑(e ⟨x, hx⟩) ∈ t
Tactic:
exact Subtype.prop _
State after:
no goals