[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
f : α → β
s t : Set α
⊢ restrict s f '' (Subtype.val ⁻¹' t) = f '' (t ∩ s)
[PROOFSTEP]
rw [restrict_eq, image_comp, image_preimage_eq_inter_range, Subtype.range_coe]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
f : α → β
g : α → γ
g' : β → γ
⊢ restrict (range f) (extend f g g') = fun x => g (Exists.choose (_ : ↑x ∈ range f))
[PROOFSTEP]
classical exact restrict_dite _ _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
f : α → β
g : α → γ
g' : β → γ
⊢ restrict (range f) (extend f g g') = fun x => g (Exists.choose (_ : ↑x ∈ range f))
[PROOFSTEP]
exact restrict_dite _ _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
f : α → β
g : α → γ
g' : β → γ
⊢ restrict (range f)ᶜ (extend f g g') = g' ∘ Subtype.val
[PROOFSTEP]
classical exact restrict_dite_compl _ _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
f : α → β
g : α → γ
g' : β → γ
⊢ restrict (range f)ᶜ (extend f g g') = g' ∘ Subtype.val
[PROOFSTEP]
exact restrict_dite_compl _ _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
f : α → β
g : α → γ
g' : β → γ
⊢ range (extend f g g') ⊆ range g ∪ g' '' (range f)ᶜ
[PROOFSTEP]
classical
rintro _ ⟨y, rfl⟩
rw [extend_def]
split_ifs with h
exacts [Or.inl (mem_range_self _), Or.inr (mem_image_of_mem _ h)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
f : α → β
g : α → γ
g' : β → γ
⊢ range (extend f g g') ⊆ range g ∪ g' '' (range f)ᶜ
[PROOFSTEP]
rintro _ ⟨y, rfl⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
f : α → β
g : α → γ
g' : β → γ
y : β
⊢ extend f g g' y ∈ range g ∪ g' '' (range f)ᶜ
[PROOFSTEP]
rw [extend_def]
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
f : α → β
g : α → γ
g' : β → γ
y : β
⊢ (if h : ∃ a, f a = y then g (Classical.choose h) else g' y) ∈ range g ∪ g' '' (range f)ᶜ
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
f : α → β
g : α → γ
g' : β → γ
y : β
h : ∃ a, f a = y
⊢ g (Classical.choose h) ∈ range g ∪ g' '' (range f)ᶜ
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
f : α → β
g : α → γ
g' : β → γ
y : β
h : ¬∃ a, f a = y
⊢ g' y ∈ range g ∪ g' '' (range f)ᶜ
[PROOFSTEP]
exacts [Or.inl (mem_range_self _), Or.inr (mem_image_of_mem _ h)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
f : α → β
hf : Injective f
g : α → γ
g' : β → γ
⊢ range (extend f g g') = range g ∪ g' '' (range f)ᶜ
[PROOFSTEP]
refine' (range_extend_subset _ _ _).antisymm _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
f : α → β
hf : Injective f
g : α → γ
g' : β → γ
⊢ range g ∪ g' '' (range f)ᶜ ⊆ range (extend f g g')
[PROOFSTEP]
rintro z (⟨x, rfl⟩ | ⟨y, hy, rfl⟩)
[GOAL]
case inl.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
f : α → β
hf : Injective f
g : α → γ
g' : β → γ
x : α
⊢ g x ∈ range (extend f g g')
case inr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
f : α → β
hf : Injective f
g : α → γ
g' : β → γ
y : β
hy : y ∈ (range f)ᶜ
⊢ g' y ∈ range (extend f g g')
[PROOFSTEP]
exacts [⟨f x, hf.extend_apply _ _ _⟩, ⟨y, extend_apply' _ _ _ hy⟩]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
f : ι → α
s : Set α
h : ∀ (x : ι), f x ∈ s
⊢ Injective (codRestrict f s h) ↔ Injective f
[PROOFSTEP]
simp only [Injective, Subtype.ext_iff, val_codRestrict_apply]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
⊢ EqOn f₁ f₂ {a} ↔ f₁ a = f₂ a
[PROOFSTEP]
simp [Set.EqOn]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s s₁ s₂ : Set α
t✝ t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
heq : EqOn f₁ f₂ s
t : Set β
x : α
hx : x ∈ s
⊢ x ∈ f₁ ⁻¹' t ↔ x ∈ f₂ ⁻¹' t
[PROOFSTEP]
rw [mem_preimage, mem_preimage, heq hx]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
inst✝¹ : Preorder α
inst✝ : Preorder β
h₁ : MonotoneOn f₁ s
h : EqOn f₁ f₂ s
⊢ MonotoneOn f₂ s
[PROOFSTEP]
intro a ha b hb hab
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a✝ : α
b✝ : β
inst✝¹ : Preorder α
inst✝ : Preorder β
h₁ : MonotoneOn f₁ s
h : EqOn f₁ f₂ s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a ≤ b
⊢ f₂ a ≤ f₂ b
[PROOFSTEP]
rw [← h ha, ← h hb]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a✝ : α
b✝ : β
inst✝¹ : Preorder α
inst✝ : Preorder β
h₁ : MonotoneOn f₁ s
h : EqOn f₁ f₂ s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a ≤ b
⊢ f₁ a ≤ f₁ b
[PROOFSTEP]
exact h₁ ha hb hab
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
inst✝¹ : Preorder α
inst✝ : Preorder β
h₁ : StrictMonoOn f₁ s
h : EqOn f₁ f₂ s
⊢ StrictMonoOn f₂ s
[PROOFSTEP]
intro a ha b hb hab
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a✝ : α
b✝ : β
inst✝¹ : Preorder α
inst✝ : Preorder β
h₁ : StrictMonoOn f₁ s
h : EqOn f₁ f₂ s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a < b
⊢ f₂ a < f₂ b
[PROOFSTEP]
rw [← h ha, ← h hb]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a✝ : α
b✝ : β
inst✝¹ : Preorder α
inst✝ : Preorder β
h₁ : StrictMonoOn f₁ s
h : EqOn f₁ f₂ s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a < b
⊢ f₁ a < f₁ b
[PROOFSTEP]
exact h₁ ha hb hab
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g✝ g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
x✝ : ∃ g, ∀ (x : ↑s), f ↑x = ↑(g x)
x : α
hx : x ∈ s
g : ↑s → ↑t
hg : ∀ (x : ↑s), f ↑x = ↑(g x)
⊢ f x ∈ t
[PROOFSTEP]
erw [hg ⟨x, hx⟩]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g✝ g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
x✝ : ∃ g, ∀ (x : ↑s), f ↑x = ↑(g x)
x : α
hx : x ∈ s
g : ↑s → ↑t
hg : ∀ (x : ↑s), f ↑x = ↑(g x)
⊢ ↑(g { val := x, property := hx }) ∈ t
[PROOFSTEP]
apply Subtype.coe_prop
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s✝ s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f✝ f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
f : α → α
s : Set α
h : MapsTo f s s
n : ℕ
⊢ (restrict f s s h)^[n] = restrict f^[n] s s (_ : MapsTo f^[n] s s)
[PROOFSTEP]
funext x
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s✝ s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f✝ f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
f : α → α
s : Set α
h : MapsTo f s s
n : ℕ
x : ↑s
⊢ (restrict f s s h)^[n] x = restrict f^[n] s s (_ : MapsTo f^[n] s s) x
[PROOFSTEP]
rw [Subtype.ext_iff, MapsTo.val_restrict_apply]
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s✝ s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f✝ f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
f : α → α
s : Set α
h : MapsTo f s s
n : ℕ
x : ↑s
⊢ ↑((restrict f s s h)^[n] x) = f^[n] ↑x
[PROOFSTEP]
induction' n with n ihn generalizing x
[GOAL]
case h.zero
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s✝ s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f✝ f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
f : α → α
s : Set α
h : MapsTo f s s
x✝ x : ↑s
⊢ ↑((restrict f s s h)^[Nat.zero] x) = f^[Nat.zero] ↑x
[PROOFSTEP]
rfl
[GOAL]
case h.succ
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s✝ s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f✝ f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
f : α → α
s : Set α
h : MapsTo f s s
x✝ : ↑s
n : ℕ
ihn : ∀ (x : ↑s), ↑((restrict f s s h)^[n] x) = f^[n] ↑x
x : ↑s
⊢ ↑((restrict f s s h)^[Nat.succ n] x) = f^[Nat.succ n] ↑x
[PROOFSTEP]
simp [Nat.iterate, ihn]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s✝ s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f✝ f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
f : α → β
s : Set α
⊢ MapsTo f s (f '' s)
[PROOFSTEP]
rw [mapsTo']
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s✝ s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f✝ f₁ f₂ f₃ : α → β
g✝ g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
f : α → β
g : γ → α
s : Set β
⊢ MapsTo f (range g) s ↔ MapsTo (f ∘ g) univ s
[PROOFSTEP]
rw [← image_univ, maps_image_to]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
⊢ range (restrictPreimage t f) = Subtype.val ⁻¹' range f
[PROOFSTEP]
delta Set.restrictPreimage
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
⊢ range (MapsTo.restrict f (f ⁻¹' t) t (_ : MapsTo f (f ⁻¹' t) t)) = Subtype.val ⁻¹' range f
[PROOFSTEP]
rw [MapsTo.range_restrict, Set.image_preimage_eq_inter_range, Set.preimage_inter, Subtype.coe_preimage_self,
  Set.univ_inter]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
h : Disjoint s₁ s₂
⊢ InjOn f (s₁ ∪ s₂) ↔ InjOn f s₁ ∧ InjOn f s₂ ∧ ∀ (x : α), x ∈ s₁ → ∀ (y : α), y ∈ s₂ → f x ≠ f y
[PROOFSTEP]
refine' ⟨fun H => ⟨H.mono <| subset_union_left _ _, H.mono <| subset_union_right _ _, _⟩, _⟩
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
h : Disjoint s₁ s₂
H : InjOn f (s₁ ∪ s₂)
⊢ ∀ (x : α), x ∈ s₁ → ∀ (y : α), y ∈ s₂ → f x ≠ f y
[PROOFSTEP]
intro x hx y hy hxy
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
h : Disjoint s₁ s₂
H : InjOn f (s₁ ∪ s₂)
x : α
hx : x ∈ s₁
y : α
hy : y ∈ s₂
hxy : f x = f y
⊢ False
[PROOFSTEP]
obtain rfl : x = y := H (Or.inl hx) (Or.inr hy) hxy
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
h : Disjoint s₁ s₂
H : InjOn f (s₁ ∪ s₂)
x : α
hx : x ∈ s₁
hy : x ∈ s₂
hxy : f x = f x
⊢ False
[PROOFSTEP]
exact h.le_bot ⟨hx, hy⟩
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
h : Disjoint s₁ s₂
⊢ (InjOn f s₁ ∧ InjOn f s₂ ∧ ∀ (x : α), x ∈ s₁ → ∀ (y : α), y ∈ s₂ → f x ≠ f y) → InjOn f (s₁ ∪ s₂)
[PROOFSTEP]
rintro ⟨h₁, h₂, h₁₂⟩
[GOAL]
case refine'_2.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
h : Disjoint s₁ s₂
h₁ : InjOn f s₁
h₂ : InjOn f s₂
h₁₂ : ∀ (x : α), x ∈ s₁ → ∀ (y : α), y ∈ s₂ → f x ≠ f y
⊢ InjOn f (s₁ ∪ s₂)
[PROOFSTEP]
rintro x (hx | hx) y (hy | hy) hxy
[GOAL]
case refine'_2.intro.intro.inl.inl
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
h : Disjoint s₁ s₂
h₁ : InjOn f s₁
h₂ : InjOn f s₂
h₁₂ : ∀ (x : α), x ∈ s₁ → ∀ (y : α), y ∈ s₂ → f x ≠ f y
x : α
hx : x ∈ s₁
y : α
hy : y ∈ s₁
hxy : f x = f y
⊢ x = y
case refine'_2.intro.intro.inl.inr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
h : Disjoint s₁ s₂
h₁ : InjOn f s₁
h₂ : InjOn f s₂
h₁₂ : ∀ (x : α), x ∈ s₁ → ∀ (y : α), y ∈ s₂ → f x ≠ f y
x : α
hx : x ∈ s₁
y : α
hy : y ∈ s₂
hxy : f x = f y
⊢ x = y
case refine'_2.intro.intro.inr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
h : Disjoint s₁ s₂
h₁ : InjOn f s₁
h₂ : InjOn f s₂
h₁₂ : ∀ (x : α), x ∈ s₁ → ∀ (y : α), y ∈ s₂ → f x ≠ f y
x : α
hx : x ∈ s₂
y : α
hy : y ∈ s₁
hxy : f x = f y
⊢ x = y
case refine'_2.intro.intro.inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
h : Disjoint s₁ s₂
h₁ : InjOn f s₁
h₂ : InjOn f s₂
h₁₂ : ∀ (x : α), x ∈ s₁ → ∀ (y : α), y ∈ s₂ → f x ≠ f y
x : α
hx : x ∈ s₂
y : α
hy : y ∈ s₂
hxy : f x = f y
⊢ x = y
[PROOFSTEP]
exacts [h₁ hx hy hxy, (h₁₂ _ hx _ hy hxy).elim, (h₁₂ _ hy _ hx hxy.symm).elim, h₂ hx hy hxy]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s✝ s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f✝ f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a✝ : α
b : β
f : α → β
s : Set α
a : α
has : ¬a ∈ s
⊢ InjOn f (insert a s) ↔ InjOn f s ∧ ¬f a ∈ f '' s
[PROOFSTEP]
have : Disjoint s { a } := disjoint_iff_inf_le.mpr fun x ⟨hxs, (hxa : x = a)⟩ => has (hxa ▸ hxs)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s✝ s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f✝ f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a✝ : α
b : β
f : α → β
s : Set α
a : α
has : ¬a ∈ s
this : Disjoint s {a}
⊢ InjOn f (insert a s) ↔ InjOn f s ∧ ¬f a ∈ f '' s
[PROOFSTEP]
rw [← union_singleton, injOn_union this]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s✝ s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f✝ f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a✝ : α
b : β
f : α → β
s : Set α
a : α
has : ¬a ∈ s
this : Disjoint s {a}
⊢ (InjOn f s ∧ InjOn f {a} ∧ ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ {a} → f x ≠ f y) ↔ InjOn f s ∧ ¬f a ∈ f '' s
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
h : Injective (g ∘ f)
⊢ InjOn g (range f)
[PROOFSTEP]
rintro _ ⟨x, rfl⟩ _ ⟨y, rfl⟩ H
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
h : Injective (g ∘ f)
x y : α
H : g (f x) = g (f y)
⊢ f x = f y
[PROOFSTEP]
exact congr_arg f (h H)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
h : MapsTo f s t
⊢ Injective (restrict f s t h) ↔ InjOn f s
[PROOFSTEP]
rw [h.restrict_eq_codRestrict, injective_codRestrict, injOn_iff_injective]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f✝ f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
inst✝ : Nonempty β
x✝ : ∃ f, Injective f
f : ↑s → β
hf : Injective f
⊢ ∃ f, InjOn f s
[PROOFSTEP]
lift f to α → β using trivial
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f✝ f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
inst✝ : Nonempty β
x✝ : ∃ f, Injective f
f : α → β
hf : Injective fun i => f ↑i
⊢ ∃ f, InjOn f s
[PROOFSTEP]
exact ⟨f, injOn_iff_injective.2 hf⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s✝ s₁ s₂ : Set α
t✝ t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
s t u : Set α
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
⊢ f '' (s ∩ t) = f '' s ∩ f '' t
[PROOFSTEP]
apply Subset.antisymm (image_inter_subset _ _ _)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s✝ s₁ s₂ : Set α
t✝ t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
s t u : Set α
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
⊢ f '' s ∩ f '' t ⊆ f '' (s ∩ t)
[PROOFSTEP]
intro x ⟨⟨y, ys, hy⟩, ⟨z, zt, hz⟩⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s✝ s₁ s₂ : Set α
t✝ t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
s t u : Set α
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
x : β
y : α
ys : y ∈ s
hy : f y = x
z : α
zt : z ∈ t
hz : f z = x
⊢ x ∈ f '' (s ∩ t)
[PROOFSTEP]
have : y = z := by
  apply hf (hs ys) (ht zt)
  rwa [← hz] at hy 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s✝ s₁ s₂ : Set α
t✝ t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
s t u : Set α
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
x : β
y : α
ys : y ∈ s
hy : f y = x
z : α
zt : z ∈ t
hz : f z = x
⊢ y = z
[PROOFSTEP]
apply hf (hs ys) (ht zt)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s✝ s₁ s₂ : Set α
t✝ t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
s t u : Set α
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
x : β
y : α
ys : y ∈ s
hy : f y = x
z : α
zt : z ∈ t
hz : f z = x
⊢ f y = f z
[PROOFSTEP]
rwa [← hz] at hy 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s✝ s₁ s₂ : Set α
t✝ t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
s t u : Set α
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
x : β
y : α
ys : y ∈ s
hy : f y = x
z : α
zt : z ∈ t
hz : f z = x
this : y = z
⊢ x ∈ f '' (s ∩ t)
[PROOFSTEP]
rw [← this] at zt 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s✝ s₁ s₂ : Set α
t✝ t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
s t u : Set α
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
x : β
y : α
ys : y ∈ s
hy : f y = x
z : α
zt : y ∈ t
hz : f z = x
this : y = z
⊢ x ∈ f '' (s ∩ t)
[PROOFSTEP]
exact ⟨y, ⟨ys, zt⟩, hy⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s✝ s₁ s₂ : Set α
t✝ t₁ t₂ : Set β
p : Set γ
f✝ f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
s t u : Set α
f : α → β
h : Disjoint s t
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
⊢ Disjoint (f '' s) (f '' t)
[PROOFSTEP]
rw [disjoint_iff_inter_eq_empty] at h ⊢
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s✝ s₁ s₂ : Set α
t✝ t₁ t₂ : Set β
p : Set γ
f✝ f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
s t u : Set α
f : α → β
h : s ∩ t = ∅
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
⊢ f '' s ∩ f '' t = ∅
[PROOFSTEP]
rw [← hf.image_inter hs ht, h, image_empty]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g✝ g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
x✝ : ∃ t' g, t ⊆ t' ∧ Surjective g ∧ ∀ (x : ↑s), f ↑x = ↑(g x)
y : β
hy : y ∈ t
t' : Set β
g : ↑s → ↑t'
htt' : t ⊆ t'
hg : Surjective g
hfg : ∀ (x : ↑s), f ↑x = ↑(g x)
x : ↑s
hx : g x = { val := y, property := (_ : y ∈ t') }
⊢ f ↑x = y
[PROOFSTEP]
rw [hfg, hx, Subtype.coe_mk]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
h : SurjOn f₁ s t
H : EqOn f₁ f₂ s
⊢ SurjOn f₂ s t
[PROOFSTEP]
rwa [SurjOn, ← H.image_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
h₁ : SurjOn f s₁ t₁
h₂ : SurjOn f s₂ t₂
h : InjOn f (s₁ ∪ s₂)
⊢ SurjOn f (s₁ ∩ s₂) (t₁ ∩ t₂)
[PROOFSTEP]
intro y hy
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
h₁ : SurjOn f s₁ t₁
h₂ : SurjOn f s₂ t₂
h : InjOn f (s₁ ∪ s₂)
y : β
hy : y ∈ t₁ ∩ t₂
⊢ y ∈ f '' (s₁ ∩ s₂)
[PROOFSTEP]
rcases h₁ hy.1 with ⟨x₁, hx₁, rfl⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
h₁ : SurjOn f s₁ t₁
h₂ : SurjOn f s₂ t₂
h : InjOn f (s₁ ∪ s₂)
x₁ : α
hx₁ : x₁ ∈ s₁
hy : f x₁ ∈ t₁ ∩ t₂
⊢ f x₁ ∈ f '' (s₁ ∩ s₂)
[PROOFSTEP]
rcases h₂ hy.2 with ⟨x₂, hx₂, heq⟩
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
h₁ : SurjOn f s₁ t₁
h₂ : SurjOn f s₂ t₂
h : InjOn f (s₁ ∪ s₂)
x₁ : α
hx₁ : x₁ ∈ s₁
hy : f x₁ ∈ t₁ ∩ t₂
x₂ : α
hx₂ : x₂ ∈ s₂
heq : f x₂ = f x₁
⊢ f x₁ ∈ f '' (s₁ ∩ s₂)
[PROOFSTEP]
obtain rfl : x₁ = x₂ := h (Or.inl hx₁) (Or.inr hx₂) heq.symm
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
h₁ : SurjOn f s₁ t₁
h₂ : SurjOn f s₂ t₂
h : InjOn f (s₁ ∪ s₂)
x₁ : α
hx₁ : x₁ ∈ s₁
hy : f x₁ ∈ t₁ ∩ t₂
hx₂ : x₁ ∈ s₂
heq : f x₁ = f x₁
⊢ f x₁ ∈ f '' (s₁ ∩ s₂)
[PROOFSTEP]
exact mem_image_of_mem f ⟨hx₁, hx₂⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s✝ s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
s : Set α
⊢ SurjOn id s s
[PROOFSTEP]
simp [SurjOn, subset_rfl]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g✝ g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
hf : SurjOn f s t
g : β → γ
⊢ SurjOn (g ∘ f) s (g '' t)
[PROOFSTEP]
rw [SurjOn, image_comp g f]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g✝ g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
hf : SurjOn f s t
g : β → γ
⊢ g '' t ⊆ g '' (f '' s)
[PROOFSTEP]
exact image_subset _ hf
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s✝ s₁ s₂ : Set α
t✝ t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
s : Set β
t : Set γ
hf : Surjective f
hg : SurjOn g s t
⊢ SurjOn (g ∘ f) (f ⁻¹' s) t
[PROOFSTEP]
rwa [SurjOn, image_comp g f, image_preimage_eq _ hf]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
⊢ Surjective f ↔ SurjOn f univ univ
[PROOFSTEP]
simp [Surjective, SurjOn, subset_def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
⊢ f '' s = t ↔ SurjOn f s t ∧ MapsTo f s t
[PROOFSTEP]
refine' ⟨_, fun h => h.1.image_eq_of_mapsTo h.2⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
⊢ f '' s = t → SurjOn f s t ∧ MapsTo f s t
[PROOFSTEP]
rintro rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s s₁ s₂ : Set α
t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
⊢ SurjOn f s (f '' s) ∧ MapsTo f s (f '' s)
[PROOFSTEP]
exact ⟨s.surjOn_image f, s.mapsTo_image f⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
hf : EqOn (g₁ ∘ f) (g₂ ∘ f) s
hf' : SurjOn f s t
⊢ EqOn g₁ g₂ t
[PROOFSTEP]
intro b hb
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b✝ : β
hf : EqOn (g₁ ∘ f) (g₂ ∘ f) s
hf' : SurjOn f s t
b : β
hb : b ∈ t
⊢ g₁ b = g₂ b
[PROOFSTEP]
obtain ⟨a, ha, rfl⟩ := hf' hb
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a✝ : α
b : β
hf : EqOn (g₁ ∘ f) (g₂ ∘ f) s
hf' : SurjOn f s t
a : α
ha : a ∈ s
hb : f a ∈ t
⊢ g₁ (f a) = g₂ (f a)
[PROOFSTEP]
exact hf ha
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
⊢ BijOn f {a} {b} ↔ f a = b
[PROOFSTEP]
simp [BijOn, eq_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
h : LeftInvOn f' f s
hf : SurjOn f s t
y : β
hy : y ∈ t
⊢ f' y ∈ s
[PROOFSTEP]
let ⟨x, hs, hx⟩ := hf hy
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
h : LeftInvOn f' f s
hf : SurjOn f s t
y : β
hy : y ∈ t
x : α
hs : x ∈ s
hx : f x = y
⊢ f' y ∈ s
[PROOFSTEP]
rwa [← hx, h hs]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
hf : LeftInvOn f' f s
⊢ f '' (s₁ ∩ s) = f' ⁻¹' s₁ ∩ f '' s
[PROOFSTEP]
apply Subset.antisymm
[GOAL]
case h₁
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
hf : LeftInvOn f' f s
⊢ f '' (s₁ ∩ s) ⊆ f' ⁻¹' s₁ ∩ f '' s
[PROOFSTEP]
rintro _ ⟨x, ⟨h₁, h⟩, rfl⟩
[GOAL]
case h₁.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
hf : LeftInvOn f' f s
x : α
h₁ : x ∈ s₁
h : x ∈ s
⊢ f x ∈ f' ⁻¹' s₁ ∩ f '' s
[PROOFSTEP]
exact ⟨by rwa [mem_preimage, hf h], mem_image_of_mem _ h⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
hf : LeftInvOn f' f s
x : α
h₁ : x ∈ s₁
h : x ∈ s
⊢ f x ∈ f' ⁻¹' s₁
[PROOFSTEP]
rwa [mem_preimage, hf h]
[GOAL]
case h₂
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
hf : LeftInvOn f' f s
⊢ f' ⁻¹' s₁ ∩ f '' s ⊆ f '' (s₁ ∩ s)
[PROOFSTEP]
rintro _ ⟨h₁, ⟨x, h, rfl⟩⟩
[GOAL]
case h₂.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
hf : LeftInvOn f' f s
x : α
h : x ∈ s
h₁ : f x ∈ f' ⁻¹' s₁
⊢ f x ∈ f '' (s₁ ∩ s)
[PROOFSTEP]
exact mem_image_of_mem _ ⟨by rwa [← hf h], h⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
hf : LeftInvOn f' f s
x : α
h : x ∈ s
h₁ : f x ∈ f' ⁻¹' s₁
⊢ x ∈ s₁
[PROOFSTEP]
rwa [← hf h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
hf : LeftInvOn f' f s
⊢ f '' (s₁ ∩ s) = f' ⁻¹' (s₁ ∩ s) ∩ f '' s
[PROOFSTEP]
rw [hf.image_inter']
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
hf : LeftInvOn f' f s
⊢ f' ⁻¹' s₁ ∩ f '' s = f' ⁻¹' (s₁ ∩ s) ∩ f '' s
[PROOFSTEP]
refine' Subset.antisymm _ (inter_subset_inter_left _ (preimage_mono <| inter_subset_left _ _))
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
hf : LeftInvOn f' f s
⊢ f' ⁻¹' s₁ ∩ f '' s ⊆ f' ⁻¹' (s₁ ∩ s) ∩ f '' s
[PROOFSTEP]
rintro _ ⟨h₁, x, hx, rfl⟩
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
hf : LeftInvOn f' f s
x : α
hx : x ∈ s
h₁ : f x ∈ f' ⁻¹' s₁
⊢ f x ∈ f' ⁻¹' (s₁ ∩ s) ∩ f '' s
[PROOFSTEP]
exact ⟨⟨h₁, by rwa [hf hx]⟩, mem_image_of_mem _ hx⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
hf : LeftInvOn f' f s
x : α
hx : x ∈ s
h₁ : f x ∈ f' ⁻¹' s₁
⊢ f' (f x) ∈ s
[PROOFSTEP]
rwa [hf hx]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
hf : LeftInvOn f' f s
⊢ f' '' (f '' s) = s
[PROOFSTEP]
rw [Set.image_image, image_congr hf, image_id']
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
hf : SurjOn f s t
hf' : RightInvOn f f' s
y : β
hy : y ∈ t
⊢ f (f' y) = y
[PROOFSTEP]
let ⟨x, hx, heq⟩ := hf hy
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
hf : SurjOn f s t
hf' : RightInvOn f f' s
y : β
hy : y ∈ t
x : α
hx : x ∈ s
heq : f x = y
⊢ f (f' y) = y
[PROOFSTEP]
rw [← heq, hf' hx]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
inst✝ : Nonempty α
s : Set α
f : α → β
a : α
b : β
h : ∃ a, a ∈ s ∧ f a = b
⊢ invFunOn f s b ∈ s ∧ f (invFunOn f s b) = b
[PROOFSTEP]
rw [invFunOn, dif_pos h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
inst✝ : Nonempty α
s : Set α
f : α → β
a : α
b : β
h : ∃ a, a ∈ s ∧ f a = b
⊢ Classical.choose h ∈ s ∧ f (Classical.choose h) = b
[PROOFSTEP]
exact Classical.choose_spec h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
inst✝ : Nonempty α
s : Set α
f : α → β
a : α
b : β
h : ¬∃ a, a ∈ s ∧ f a = b
⊢ invFunOn f s b = Classical.choice inst✝
[PROOFSTEP]
rw [invFunOn, dif_neg h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s s₁ s₂ : Set α
t : Set β
f : α → β
inst✝ : Nonempty α
h : s ⊆ invFunOn f s '' (f '' s)
x : α
hx : x ∈ s
⊢ invFunOn f s (f x) = x
[PROOFSTEP]
obtain ⟨-, ⟨x, hx', rfl⟩, rfl⟩ := h hx
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s s₁ s₂ : Set α
t : Set β
f : α → β
inst✝ : Nonempty α
h : s ⊆ invFunOn f s '' (f '' s)
x : α
hx' : x ∈ s
hx : invFunOn f s (f x) ∈ s
⊢ invFunOn f s (f (invFunOn f s (f x))) = invFunOn f s (f x)
[PROOFSTEP]
rw [invFunOn_apply_eq (f := f) hx']
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s✝ s₁ s₂ : Set α
t : Set β
f✝ : α → β
inst✝ : Nonempty α
f : α → β
s : Set α
⊢ InjOn (invFunOn f s) (f '' s)
[PROOFSTEP]
rintro _ ⟨x, hx, rfl⟩ _ ⟨x', hx', rfl⟩ he
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s✝ s₁ s₂ : Set α
t : Set β
f✝ : α → β
inst✝ : Nonempty α
f : α → β
s : Set α
x : α
hx : x ∈ s
x' : α
hx' : x' ∈ s
he : invFunOn f s (f x) = invFunOn f s (f x')
⊢ f x = f x'
[PROOFSTEP]
rw [← invFunOn_apply_eq (f := f) hx, he, invFunOn_apply_eq (f := f) hx']
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s✝ s₁ s₂ : Set α
t : Set β
f✝ : α → β
inst✝ : Nonempty α
f : α → β
s : Set α
⊢ invFunOn f s '' (f '' s) ⊆ s
[PROOFSTEP]
rintro _ ⟨_, ⟨x, hx, rfl⟩, rfl⟩
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s✝ s₁ s₂ : Set α
t : Set β
f✝ : α → β
inst✝ : Nonempty α
f : α → β
s : Set α
x : α
hx : x ∈ s
⊢ invFunOn f s (f x) ∈ s
[PROOFSTEP]
exact invFunOn_apply_mem hx
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s s₁ s₂ : Set α
t : Set β
f : α → β
inst✝ : Nonempty α
h : SurjOn f s t
⊢ InvOn (invFunOn f s) f (invFunOn f s '' t) t
[PROOFSTEP]
refine' ⟨_, h.rightInvOn_invFunOn⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s s₁ s₂ : Set α
t : Set β
f : α → β
inst✝ : Nonempty α
h : SurjOn f s t
⊢ LeftInvOn (invFunOn f s) f (invFunOn f s '' t)
[PROOFSTEP]
rintro _ ⟨y, hy, rfl⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s s₁ s₂ : Set α
t : Set β
f : α → β
inst✝ : Nonempty α
h : SurjOn f s t
y : β
hy : y ∈ t
⊢ invFunOn f s (f (invFunOn f s y)) = invFunOn f s y
[PROOFSTEP]
rw [h.rightInvOn_invFunOn hy]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s s₁ s₂ : Set α
t : Set β
f : α → β
inst✝ : Nonempty α
h : SurjOn f s t
⊢ BijOn f (invFunOn f s '' t) t
[PROOFSTEP]
refine' h.invOn_invFunOn.bijOn _ (mapsTo_image _ _)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s s₁ s₂ : Set α
t : Set β
f : α → β
inst✝ : Nonempty α
h : SurjOn f s t
⊢ MapsTo f (invFunOn f s '' t) t
[PROOFSTEP]
rintro _ ⟨y, hy, rfl⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s s₁ s₂ : Set α
t : Set β
f : α → β
inst✝ : Nonempty α
h : SurjOn f s t
y : β
hy : y ∈ t
⊢ f (invFunOn f s y) ∈ t
[PROOFSTEP]
rwa [h.rightInvOn_invFunOn hy]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s s₁ s₂ : Set α
t : Set β
f : α → β
⊢ SurjOn f s t ↔ ∃ s' x, BijOn f s' t
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s s₁ s₂ : Set α
t : Set β
f : α → β
⊢ SurjOn f s t → ∃ s' x, BijOn f s' t
[PROOFSTEP]
rcases eq_empty_or_nonempty t with (rfl | ht)
[GOAL]
case mp.inl
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s s₁ s₂ : Set α
f : α → β
⊢ SurjOn f s ∅ → ∃ s' x, BijOn f s' ∅
[PROOFSTEP]
exact fun _ => ⟨∅, empty_subset _, bijOn_empty f⟩
[GOAL]
case mp.inr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s s₁ s₂ : Set α
t : Set β
f : α → β
ht : Set.Nonempty t
⊢ SurjOn f s t → ∃ s' x, BijOn f s' t
[PROOFSTEP]
intro h
[GOAL]
case mp.inr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s s₁ s₂ : Set α
t : Set β
f : α → β
ht : Set.Nonempty t
h : SurjOn f s t
⊢ ∃ s' x, BijOn f s' t
[PROOFSTEP]
haveI : Nonempty α := ⟨Classical.choose (h.comap_nonempty ht)⟩
[GOAL]
case mp.inr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s s₁ s₂ : Set α
t : Set β
f : α → β
ht : Set.Nonempty t
h : SurjOn f s t
this : Nonempty α
⊢ ∃ s' x, BijOn f s' t
[PROOFSTEP]
exact ⟨_, h.mapsTo_invFunOn.image_subset, h.bijOn_subset⟩
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s s₁ s₂ : Set α
t : Set β
f : α → β
⊢ (∃ s' x, BijOn f s' t) → SurjOn f s t
[PROOFSTEP]
rintro ⟨s', hs', hfs'⟩
[GOAL]
case mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s s₁ s₂ : Set α
t : Set β
f : α → β
s' : Set α
hs' : s' ⊆ s
hfs' : BijOn f s' t
⊢ SurjOn f s t
[PROOFSTEP]
exact hfs'.surjOn.mono hs' (Subset.refl _)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s✝ s₁ s₂ : Set α
t : Set β
f✝ : α → β
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : Classical.choice n ∈ s
⊢ Function.invFun f ⁻¹' s = f '' s ∪ (range f)ᶜ
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s✝ s₁ s₂ : Set α
t : Set β
f✝ : α → β
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : Classical.choice n ∈ s
x : β
⊢ x ∈ Function.invFun f ⁻¹' s ↔ x ∈ f '' s ∪ (range f)ᶜ
[PROOFSTEP]
rcases em (x ∈ range f) with (⟨a, rfl⟩ | hx)
[GOAL]
case h.inl.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s✝ s₁ s₂ : Set α
t : Set β
f✝ : α → β
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : Classical.choice n ∈ s
a : α
⊢ f a ∈ Function.invFun f ⁻¹' s ↔ f a ∈ f '' s ∪ (range f)ᶜ
[PROOFSTEP]
simp only [mem_preimage, mem_union, mem_compl_iff, mem_range_self, not_true, or_false, leftInverse_invFun hf _,
  hf.mem_set_image]
[GOAL]
case h.inr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s✝ s₁ s₂ : Set α
t : Set β
f✝ : α → β
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : Classical.choice n ∈ s
x : β
hx : ¬x ∈ range f
⊢ x ∈ Function.invFun f ⁻¹' s ↔ x ∈ f '' s ∪ (range f)ᶜ
[PROOFSTEP]
simp only [mem_preimage, invFun_neg hx, h, hx, mem_union, mem_compl_iff, not_false_iff, or_true]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s✝ s₁ s₂ : Set α
t : Set β
f✝ : α → β
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : ¬Classical.choice n ∈ s
⊢ Function.invFun f ⁻¹' s = f '' s
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s✝ s₁ s₂ : Set α
t : Set β
f✝ : α → β
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : ¬Classical.choice n ∈ s
x : β
⊢ x ∈ Function.invFun f ⁻¹' s ↔ x ∈ f '' s
[PROOFSTEP]
rcases em (x ∈ range f) with (⟨a, rfl⟩ | hx)
[GOAL]
case h.inl.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s✝ s₁ s₂ : Set α
t : Set β
f✝ : α → β
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : ¬Classical.choice n ∈ s
a : α
⊢ f a ∈ Function.invFun f ⁻¹' s ↔ f a ∈ f '' s
[PROOFSTEP]
rw [mem_preimage, leftInverse_invFun hf, hf.mem_set_image]
[GOAL]
case h.inr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s✝ s₁ s₂ : Set α
t : Set β
f✝ : α → β
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : ¬Classical.choice n ∈ s
x : β
hx : ¬x ∈ range f
⊢ x ∈ Function.invFun f ⁻¹' s ↔ x ∈ f '' s
[PROOFSTEP]
have : x ∉ f '' s := fun h' => hx (image_subset_range _ _ h')
[GOAL]
case h.inr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
s✝ s₁ s₂ : Set α
t : Set β
f✝ : α → β
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : ¬Classical.choice n ∈ s
x : β
hx : ¬x ∈ range f
this : ¬x ∈ f '' s
⊢ x ∈ Function.invFun f ⁻¹' s ↔ x ∈ f '' s
[PROOFSTEP]
simp only [mem_preimage, invFun_neg hx, h, this]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
δ : α → Sort u_6
s : Set α
f g : (i : α) → δ i
inst✝ : (i : α) → Decidable (i ∈ ∅)
⊢ piecewise ∅ f g = g
[PROOFSTEP]
ext i
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
δ : α → Sort u_6
s : Set α
f g : (i : α) → δ i
inst✝ : (i : α) → Decidable (i ∈ ∅)
i : α
⊢ piecewise ∅ f g i = g i
[PROOFSTEP]
simp [piecewise]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
δ : α → Sort u_6
s : Set α
f g : (i : α) → δ i
inst✝ : (i : α) → Decidable (i ∈ univ)
⊢ piecewise univ f g = f
[PROOFSTEP]
ext i
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
δ : α → Sort u_6
s : Set α
f g : (i : α) → δ i
inst✝ : (i : α) → Decidable (i ∈ univ)
i : α
⊢ piecewise univ f g i = f i
[PROOFSTEP]
simp [piecewise]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
δ : α → Sort u_6
s : Set α
f g : (i : α) → δ i
j : α
inst✝ : (i : α) → Decidable (i ∈ insert j s)
⊢ piecewise (insert j s) f g j = f j
[PROOFSTEP]
simp [piecewise]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
δ : α → Sort u_6
s : Set α
f g : (i : α) → δ i
inst✝² : (j : α) → Decidable (j ∈ s)
inst✝¹ : DecidableEq α
j : α
inst✝ : (i : α) → Decidable (i ∈ insert j s)
⊢ piecewise (insert j s) f g = update (piecewise s f g) j (f j)
[PROOFSTEP]
simp [piecewise]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
δ : α → Sort u_6
s : Set α
f g : (i : α) → δ i
inst✝² : (j : α) → Decidable (j ∈ s)
inst✝¹ : DecidableEq α
j : α
inst✝ : (i : α) → Decidable (i ∈ insert j s)
⊢ (fun i => if i = j ∨ i ∈ s then f i else g i) = update (fun i => if i ∈ s then f i else g i) j (f j)
[PROOFSTEP]
ext i
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
δ : α → Sort u_6
s : Set α
f g : (i : α) → δ i
inst✝² : (j : α) → Decidable (j ∈ s)
inst✝¹ : DecidableEq α
j : α
inst✝ : (i : α) → Decidable (i ∈ insert j s)
i : α
⊢ (if i = j ∨ i ∈ s then f i else g i) = update (fun i => if i ∈ s then f i else g i) j (f j) i
[PROOFSTEP]
by_cases h : i = j
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
δ : α → Sort u_6
s : Set α
f g : (i : α) → δ i
inst✝² : (j : α) → Decidable (j ∈ s)
inst✝¹ : DecidableEq α
j : α
inst✝ : (i : α) → Decidable (i ∈ insert j s)
i : α
h : i = j
⊢ (if i = j ∨ i ∈ s then f i else g i) = update (fun i => if i ∈ s then f i else g i) j (f j) i
[PROOFSTEP]
rw [h]
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
δ : α → Sort u_6
s : Set α
f g : (i : α) → δ i
inst✝² : (j : α) → Decidable (j ∈ s)
inst✝¹ : DecidableEq α
j : α
inst✝ : (i : α) → Decidable (i ∈ insert j s)
i : α
h : i = j
⊢ (if j = j ∨ j ∈ s then f j else g j) = update (fun i => if i ∈ s then f i else g i) j (f j) j
[PROOFSTEP]
simp
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
δ : α → Sort u_6
s : Set α
f g : (i : α) → δ i
inst✝² : (j : α) → Decidable (j ∈ s)
inst✝¹ : DecidableEq α
j : α
inst✝ : (i : α) → Decidable (i ∈ insert j s)
i : α
h : ¬i = j
⊢ (if i = j ∨ i ∈ s then f i else g i) = update (fun i => if i ∈ s then f i else g i) j (f j) i
[PROOFSTEP]
by_cases h' : i ∈ s
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
δ : α → Sort u_6
s : Set α
f g : (i : α) → δ i
inst✝² : (j : α) → Decidable (j ∈ s)
inst✝¹ : DecidableEq α
j : α
inst✝ : (i : α) → Decidable (i ∈ insert j s)
i : α
h : ¬i = j
h' : i ∈ s
⊢ (if i = j ∨ i ∈ s then f i else g i) = update (fun i => if i ∈ s then f i else g i) j (f j) i
[PROOFSTEP]
simp [h, h']
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
δ : α → Sort u_6
s : Set α
f g : (i : α) → δ i
inst✝² : (j : α) → Decidable (j ∈ s)
inst✝¹ : DecidableEq α
j : α
inst✝ : (i : α) → Decidable (i ∈ insert j s)
i : α
h : ¬i = j
h' : ¬i ∈ s
⊢ (if i = j ∨ i ∈ s then f i else g i) = update (fun i => if i ∈ s then f i else g i) j (f j) i
[PROOFSTEP]
simp [h, h']
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
δ : α → Sort u_6
s : Set α
f✝ g✝ : (i : α) → δ i
inst✝² : (j : α) → Decidable (j ∈ s)
x : α
inst✝¹ : (y : α) → Decidable (y ∈ {x})
inst✝ : DecidableEq α
f g : α → β
⊢ piecewise {x} f g = update g x (f x)
[PROOFSTEP]
ext y
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
δ : α → Sort u_6
s : Set α
f✝ g✝ : (i : α) → δ i
inst✝² : (j : α) → Decidable (j ∈ s)
x : α
inst✝¹ : (y : α) → Decidable (y ∈ {x})
inst✝ : DecidableEq α
f g : α → β
y : α
⊢ piecewise {x} f g y = update g x (f x) y
[PROOFSTEP]
by_cases hy : y = x
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
δ : α → Sort u_6
s : Set α
f✝ g✝ : (i : α) → δ i
inst✝² : (j : α) → Decidable (j ∈ s)
x : α
inst✝¹ : (y : α) → Decidable (y ∈ {x})
inst✝ : DecidableEq α
f g : α → β
y : α
hy : y = x
⊢ piecewise {x} f g y = update g x (f x) y
[PROOFSTEP]
subst y
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
δ : α → Sort u_6
s : Set α
f✝ g✝ : (i : α) → δ i
inst✝² : (j : α) → Decidable (j ∈ s)
x : α
inst✝¹ : (y : α) → Decidable (y ∈ {x})
inst✝ : DecidableEq α
f g : α → β
⊢ piecewise {x} f g x = update g x (f x) x
[PROOFSTEP]
simp
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
δ : α → Sort u_6
s : Set α
f✝ g✝ : (i : α) → δ i
inst✝² : (j : α) → Decidable (j ∈ s)
x : α
inst✝¹ : (y : α) → Decidable (y ∈ {x})
inst✝ : DecidableEq α
f g : α → β
y : α
hy : ¬y = x
⊢ piecewise {x} f g y = update g x (f x) y
[PROOFSTEP]
simp [hy]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
δ✝ : α → Sort u_6
s✝ : Set α
f g✝ : (i : α) → δ✝ i
inst✝² : (j : α) → Decidable (j ∈ s✝)
δ : α → Type u_7
inst✝¹ : (i : α) → Preorder (δ i)
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f₁ f₂ g : (i : α) → δ i
h₁ : ∀ (i : α), i ∈ s → f₁ i ≤ g i
h₂ : ∀ (i : α), ¬i ∈ s → f₂ i ≤ g i
i : α
h : i ∈ s
⊢ piecewise s f₁ f₂ i ≤ g i
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
δ✝ : α → Sort u_6
s✝ : Set α
f g✝ : (i : α) → δ✝ i
inst✝² : (j : α) → Decidable (j ∈ s✝)
δ : α → Type u_7
inst✝¹ : (i : α) → Preorder (δ i)
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f₁ f₂ g : (i : α) → δ i
h₁ : ∀ (i : α), i ∈ s → f₁ i ≤ g i
h₂ : ∀ (i : α), ¬i ∈ s → f₂ i ≤ g i
i : α
h : ¬i ∈ s
⊢ piecewise s f₁ f₂ i ≤ g i
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
δ✝ : α → Sort u_6
s✝ : Set α
f g : (i : α) → δ✝ i
inst✝² : (j : α) → Decidable (j ∈ s✝)
δ : α → Type u_7
inst✝¹ : (i : α) → Preorder (δ i)
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f₁ f₂ g₁ g₂ : (i : α) → δ i
h₁ : ∀ (i : α), i ∈ s → f₁ i ≤ g₁ i
h₂ : ∀ (i : α), ¬i ∈ s → f₂ i ≤ g₂ i
⊢ piecewise s f₁ f₂ ≤ piecewise s g₁ g₂
[PROOFSTEP]
apply piecewise_le
[GOAL]
case h₁
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
δ✝ : α → Sort u_6
s✝ : Set α
f g : (i : α) → δ✝ i
inst✝² : (j : α) → Decidable (j ∈ s✝)
δ : α → Type u_7
inst✝¹ : (i : α) → Preorder (δ i)
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f₁ f₂ g₁ g₂ : (i : α) → δ i
h₁ : ∀ (i : α), i ∈ s → f₁ i ≤ g₁ i
h₂ : ∀ (i : α), ¬i ∈ s → f₂ i ≤ g₂ i
⊢ ∀ (i : α), i ∈ s → f₁ i ≤ piecewise s g₁ g₂ i
[PROOFSTEP]
intros
[GOAL]
case h₂
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
δ✝ : α → Sort u_6
s✝ : Set α
f g : (i : α) → δ✝ i
inst✝² : (j : α) → Decidable (j ∈ s✝)
δ : α → Type u_7
inst✝¹ : (i : α) → Preorder (δ i)
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f₁ f₂ g₁ g₂ : (i : α) → δ i
h₁ : ∀ (i : α), i ∈ s → f₁ i ≤ g₁ i
h₂ : ∀ (i : α), ¬i ∈ s → f₂ i ≤ g₂ i
⊢ ∀ (i : α), ¬i ∈ s → f₂ i ≤ piecewise s g₁ g₂ i
[PROOFSTEP]
intros
[GOAL]
case h₁
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
δ✝ : α → Sort u_6
s✝ : Set α
f g : (i : α) → δ✝ i
inst✝² : (j : α) → Decidable (j ∈ s✝)
δ : α → Type u_7
inst✝¹ : (i : α) → Preorder (δ i)
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f₁ f₂ g₁ g₂ : (i : α) → δ i
h₁ : ∀ (i : α), i ∈ s → f₁ i ≤ g₁ i
h₂ : ∀ (i : α), ¬i ∈ s → f₂ i ≤ g₂ i
i✝ : α
a✝ : i✝ ∈ s
⊢ f₁ i✝ ≤ piecewise s g₁ g₂ i✝
[PROOFSTEP]
simp [*]
[GOAL]
case h₂
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
δ✝ : α → Sort u_6
s✝ : Set α
f g : (i : α) → δ✝ i
inst✝² : (j : α) → Decidable (j ∈ s✝)
δ : α → Type u_7
inst✝¹ : (i : α) → Preorder (δ i)
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f₁ f₂ g₁ g₂ : (i : α) → δ i
h₁ : ∀ (i : α), i ∈ s → f₁ i ≤ g₁ i
h₂ : ∀ (i : α), ¬i ∈ s → f₂ i ≤ g₂ i
i✝ : α
x✝ : ¬i✝ ∈ s
⊢ f₂ i✝ ≤ piecewise s g₁ g₂ i✝
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
δ : α → Sort u_6
s : Set α
f g : (i : α) → δ i
inst✝¹ : (j : α) → Decidable (j ∈ s)
i j : α
h : i ≠ j
inst✝ : (i : α) → Decidable (i ∈ insert j s)
⊢ piecewise (insert j s) f g i = piecewise s f g i
[PROOFSTEP]
simp [piecewise, h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
δ : α → Sort u_6
s : Set α
f g : (i : α) → δ i
inst✝¹ : (j : α) → Decidable (j ∈ s)
inst✝ : (i : α) → Decidable (i ∈ sᶜ)
x : α
hx : x ∈ s
⊢ piecewise sᶜ f g x = piecewise s g f x
[PROOFSTEP]
simp [hx]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
δ : α → Sort u_6
s : Set α
f g : (i : α) → δ i
inst✝¹ : (j : α) → Decidable (j ∈ s)
inst✝ : (i : α) → Decidable (i ∈ sᶜ)
x : α
hx : ¬x ∈ s
⊢ piecewise sᶜ f g x = piecewise s g f x
[PROOFSTEP]
simp [hx]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
δ : α → Sort u_6
s✝ : Set α
f g : (i : α) → δ i
inst✝¹ : (j : α) → Decidable (j ∈ s✝)
s s₁ s₂ : Set α
t t₁ t₂ : Set β
f₁ f₂ : α → β
inst✝ : (i : α) → Decidable (i ∈ s)
h₁ : MapsTo f₁ (s₁ ∩ s) (t₁ ∩ t)
h₂ : MapsTo f₂ (s₂ ∩ sᶜ) (t₂ ∩ tᶜ)
⊢ MapsTo (piecewise s f₁ f₂) (Set.ite s s₁ s₂) (Set.ite t t₁ t₂)
[PROOFSTEP]
refine' (h₁.congr _).union_union (h₂.congr _)
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
δ : α → Sort u_6
s✝ : Set α
f g : (i : α) → δ i
inst✝¹ : (j : α) → Decidable (j ∈ s✝)
s s₁ s₂ : Set α
t t₁ t₂ : Set β
f₁ f₂ : α → β
inst✝ : (i : α) → Decidable (i ∈ s)
h₁ : MapsTo f₁ (s₁ ∩ s) (t₁ ∩ t)
h₂ : MapsTo f₂ (s₂ ∩ sᶜ) (t₂ ∩ tᶜ)
⊢ EqOn f₁ (piecewise s f₁ f₂) (s₁ ∩ s)
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
δ : α → Sort u_6
s✝ : Set α
f g : (i : α) → δ i
inst✝¹ : (j : α) → Decidable (j ∈ s✝)
s s₁ s₂ : Set α
t t₁ t₂ : Set β
f₁ f₂ : α → β
inst✝ : (i : α) → Decidable (i ∈ s)
h₁ : MapsTo f₁ (s₁ ∩ s) (t₁ ∩ t)
h₂ : MapsTo f₂ (s₂ ∩ sᶜ) (t₂ ∩ tᶜ)
⊢ EqOn f₂ (piecewise s f₁ f₂) (s₂ ∩ sᶜ)
[PROOFSTEP]
exacts [(piecewise_eqOn s f₁ f₂).symm.mono (inter_subset_right _ _),
  (piecewise_eqOn_compl s f₁ f₂).symm.mono (inter_subset_right _ _)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
δ : α → Sort u_6
s : Set α
f✝ g✝ : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
f f' g : α → β
t : Set α
⊢ EqOn (piecewise s f f') g t ↔ EqOn f g (t ∩ s) ∧ EqOn f' g (t ∩ sᶜ)
[PROOFSTEP]
simp only [EqOn, ← forall_and]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
δ : α → Sort u_6
s : Set α
f✝ g✝ : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
f f' g : α → β
t : Set α
⊢ (∀ ⦃x : α⦄, x ∈ t → piecewise s f f' x = g x) ↔ ∀ (x : α), (x ∈ t ∩ s → f x = g x) ∧ (x ∈ t ∩ sᶜ → f' x = g x)
[PROOFSTEP]
refine' forall_congr' fun a => _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
δ : α → Sort u_6
s : Set α
f✝ g✝ : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
f f' g : α → β
t : Set α
a : α
⊢ a ∈ t → piecewise s f f' a = g a ↔ (a ∈ t ∩ s → f a = g a) ∧ (a ∈ t ∩ sᶜ → f' a = g a)
[PROOFSTEP]
by_cases a ∈ s
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
δ : α → Sort u_6
s : Set α
f✝ g✝ : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
f f' g : α → β
t : Set α
a : α
⊢ a ∈ t → piecewise s f f' a = g a ↔ (a ∈ t ∩ s → f a = g a) ∧ (a ∈ t ∩ sᶜ → f' a = g a)
[PROOFSTEP]
by_cases a ∈ s
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
δ : α → Sort u_6
s : Set α
f✝ g✝ : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
f f' g : α → β
t : Set α
a : α
h : a ∈ s
⊢ a ∈ t → piecewise s f f' a = g a ↔ (a ∈ t ∩ s → f a = g a) ∧ (a ∈ t ∩ sᶜ → f' a = g a)
[PROOFSTEP]
simp [*]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
δ : α → Sort u_6
s : Set α
f✝ g✝ : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
f f' g : α → β
t : Set α
a : α
h : ¬a ∈ s
⊢ a ∈ t → piecewise s f f' a = g a ↔ (a ∈ t ∩ s → f a = g a) ∧ (a ∈ t ∩ sᶜ → f' a = g a)
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
δ : α → Sort u_6
s : Set α
f✝ g✝ : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
f f' g : α → β
t t' : Set α
h : EqOn f g (t ∩ s)
h' : EqOn f' g (t' ∩ sᶜ)
⊢ EqOn (piecewise s f f') g (Set.ite s t t')
[PROOFSTEP]
simp [eqOn_piecewise, *]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
δ : α → Sort u_6
s : Set α
f✝ g✝ : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
t : Set β
x : α
⊢ x ∈ piecewise s f g ⁻¹' t ↔ x ∈ Set.ite s (f ⁻¹' t) (g ⁻¹' t)
[PROOFSTEP]
by_cases x ∈ s
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
δ : α → Sort u_6
s : Set α
f✝ g✝ : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
t : Set β
x : α
⊢ x ∈ piecewise s f g ⁻¹' t ↔ x ∈ Set.ite s (f ⁻¹' t) (g ⁻¹' t)
[PROOFSTEP]
by_cases x ∈ s
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
δ : α → Sort u_6
s : Set α
f✝ g✝ : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
t : Set β
x : α
h : x ∈ s
⊢ x ∈ piecewise s f g ⁻¹' t ↔ x ∈ Set.ite s (f ⁻¹' t) (g ⁻¹' t)
[PROOFSTEP]
simp [*, Set.ite]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
δ : α → Sort u_6
s : Set α
f✝ g✝ : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
t : Set β
x : α
h : ¬x ∈ s
⊢ x ∈ piecewise s f g ⁻¹' t ↔ x ∈ Set.ite s (f ⁻¹' t) (g ⁻¹' t)
[PROOFSTEP]
simp [*, Set.ite]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
δ : α → Sort u_6
s : Set α
f g : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
δ' : α → Sort u_7
h : (i : α) → δ i → δ' i
x : α
⊢ h x (piecewise s f g x) = piecewise s (fun x => h x (f x)) (fun x => h x (g x)) x
[PROOFSTEP]
by_cases hx : x ∈ s
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
δ : α → Sort u_6
s : Set α
f g : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
δ' : α → Sort u_7
h : (i : α) → δ i → δ' i
x : α
hx : x ∈ s
⊢ h x (piecewise s f g x) = piecewise s (fun x => h x (f x)) (fun x => h x (g x)) x
[PROOFSTEP]
simp [hx]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
δ : α → Sort u_6
s : Set α
f g : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
δ' : α → Sort u_7
h : (i : α) → δ i → δ' i
x : α
hx : ¬x ∈ s
⊢ h x (piecewise s f g x) = piecewise s (fun x => h x (f x)) (fun x => h x (g x)) x
[PROOFSTEP]
simp [hx]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
δ : α → Sort u_6
s : Set α
f g : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
δ' : α → Sort u_7
δ'' : α → Sort u_8
f' g' : (i : α) → δ' i
h : (i : α) → δ i → δ' i → δ'' i
x : α
⊢ h x (piecewise s f g x) (piecewise s f' g' x) = piecewise s (fun x => h x (f x) (f' x)) (fun x => h x (g x) (g' x)) x
[PROOFSTEP]
by_cases hx : x ∈ s
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
δ : α → Sort u_6
s : Set α
f g : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
δ' : α → Sort u_7
δ'' : α → Sort u_8
f' g' : (i : α) → δ' i
h : (i : α) → δ i → δ' i → δ'' i
x : α
hx : x ∈ s
⊢ h x (piecewise s f g x) (piecewise s f' g' x) = piecewise s (fun x => h x (f x) (f' x)) (fun x => h x (g x) (g' x)) x
[PROOFSTEP]
simp [hx]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
δ : α → Sort u_6
s : Set α
f g : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
δ' : α → Sort u_7
δ'' : α → Sort u_8
f' g' : (i : α) → δ' i
h : (i : α) → δ i → δ' i → δ'' i
x : α
hx : ¬x ∈ s
⊢ h x (piecewise s f g x) (piecewise s f' g' x) = piecewise s (fun x => h x (f x) (f' x)) (fun x => h x (g x) (g' x)) x
[PROOFSTEP]
simp [hx]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
δ : α → Sort u_6
s : Set α
f g : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
⊢ piecewise s f f = f
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
δ : α → Sort u_6
s : Set α
f g : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
x : α
⊢ piecewise s f f x = f x
[PROOFSTEP]
by_cases hx : x ∈ s
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
δ : α → Sort u_6
s : Set α
f g : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
x : α
hx : x ∈ s
⊢ piecewise s f f x = f x
[PROOFSTEP]
simp [hx]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
δ : α → Sort u_6
s : Set α
f g : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
x : α
hx : ¬x ∈ s
⊢ piecewise s f f x = f x
[PROOFSTEP]
simp [hx]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
δ : α → Sort u_6
s : Set α
f✝ g✝ : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
⊢ range (piecewise s f g) = f '' s ∪ g '' sᶜ
[PROOFSTEP]
ext y
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
δ : α → Sort u_6
s : Set α
f✝ g✝ : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
y : β
⊢ y ∈ range (piecewise s f g) ↔ y ∈ f '' s ∪ g '' sᶜ
[PROOFSTEP]
constructor
[GOAL]
case h.mp
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
δ : α → Sort u_6
s : Set α
f✝ g✝ : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
y : β
⊢ y ∈ range (piecewise s f g) → y ∈ f '' s ∪ g '' sᶜ
[PROOFSTEP]
rintro ⟨x, rfl⟩
[GOAL]
case h.mp.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
δ : α → Sort u_6
s : Set α
f✝ g✝ : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
⊢ piecewise s f g x ∈ f '' s ∪ g '' sᶜ
[PROOFSTEP]
by_cases h : x ∈ s <;> [left; right]
[GOAL]
case h.mp.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
δ : α → Sort u_6
s : Set α
f✝ g✝ : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
⊢ piecewise s f g x ∈ f '' s ∪ g '' sᶜ
[PROOFSTEP]
by_cases h : x ∈ s
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
δ : α → Sort u_6
s : Set α
f✝ g✝ : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
h : x ∈ s
⊢ piecewise s f g x ∈ f '' s ∪ g '' sᶜ
[PROOFSTEP]
left
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
δ : α → Sort u_6
s : Set α
f✝ g✝ : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
h : ¬x ∈ s
⊢ piecewise s f g x ∈ f '' s ∪ g '' sᶜ
[PROOFSTEP]
right
[GOAL]
case pos.h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
δ : α → Sort u_6
s : Set α
f✝ g✝ : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
h : x ∈ s
⊢ piecewise s f g x ∈ f '' s
[PROOFSTEP]
use x
[GOAL]
case neg.h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
δ : α → Sort u_6
s : Set α
f✝ g✝ : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
h : ¬x ∈ s
⊢ piecewise s f g x ∈ g '' sᶜ
[PROOFSTEP]
use x
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
δ : α → Sort u_6
s : Set α
f✝ g✝ : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
h : x ∈ s
⊢ x ∈ s ∧ f x = piecewise s f g x
[PROOFSTEP]
simp [h]
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
δ : α → Sort u_6
s : Set α
f✝ g✝ : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
h : ¬x ∈ s
⊢ x ∈ sᶜ ∧ g x = piecewise s f g x
[PROOFSTEP]
simp [h]
[GOAL]
case h.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
δ : α → Sort u_6
s : Set α
f✝ g✝ : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
y : β
⊢ y ∈ f '' s ∪ g '' sᶜ → y ∈ range (piecewise s f g)
[PROOFSTEP]
rintro (⟨x, hx, rfl⟩ | ⟨x, hx, rfl⟩)
[GOAL]
case h.mpr.inl.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
δ : α → Sort u_6
s : Set α
f✝ g✝ : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
hx : x ∈ s
⊢ f x ∈ range (piecewise s f g)
[PROOFSTEP]
use x
[GOAL]
case h.mpr.inr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
δ : α → Sort u_6
s : Set α
f✝ g✝ : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
hx : x ∈ sᶜ
⊢ g x ∈ range (piecewise s f g)
[PROOFSTEP]
use x
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
δ : α → Sort u_6
s : Set α
f✝ g✝ : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
hx : x ∈ s
⊢ piecewise s f g x = f x
[PROOFSTEP]
simp_all
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
δ : α → Sort u_6
s : Set α
f✝ g✝ : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
hx : x ∈ sᶜ
⊢ piecewise s f g x = g x
[PROOFSTEP]
simp_all
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
δ : α → Sort u_6
s : Set α
f✝ g✝ : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
⊢ Injective (piecewise s f g) ↔ InjOn f s ∧ InjOn g sᶜ ∧ ∀ (x : α), x ∈ s → ∀ (y : α), ¬y ∈ s → f x ≠ g y
[PROOFSTEP]
rw [injective_iff_injOn_univ, ← union_compl_self s, injOn_union (@disjoint_compl_right _ _ s),
  (piecewise_eqOn s f g).injOn_iff, (piecewise_eqOn_compl s f g).injOn_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
δ : α → Sort u_6
s : Set α
f✝ g✝ : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
⊢ (InjOn f s ∧ InjOn g sᶜ ∧ ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ sᶜ → piecewise s f g x ≠ piecewise s f g y) ↔
    InjOn f s ∧ InjOn g sᶜ ∧ ∀ (x : α), x ∈ s → ∀ (y : α), ¬y ∈ s → f x ≠ g y
[PROOFSTEP]
refine' and_congr Iff.rfl (and_congr Iff.rfl <| forall₄_congr fun x hx y hy => _)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
δ : α → Sort u_6
s : Set α
f✝ g✝ : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
hx : x ∈ s
y : α
hy : y ∈ sᶜ
⊢ piecewise s f g x ≠ piecewise s f g y ↔ f x ≠ g y
[PROOFSTEP]
rw [piecewise_eq_of_mem s f g hx, piecewise_eq_of_not_mem s f g hy]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
δ✝ : α → Sort u_6
s : Set α
f✝ g✝ : (i : α) → δ✝ i
inst✝ : (j : α) → Decidable (j ∈ s)
δ : α → Type u_7
t : Set α
t' : (i : α) → Set (δ i)
f g : (i : α) → δ i
hf : f ∈ pi t t'
hg : g ∈ pi t t'
⊢ piecewise s f g ∈ pi t t'
[PROOFSTEP]
intro i ht
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
δ✝ : α → Sort u_6
s : Set α
f✝ g✝ : (i : α) → δ✝ i
inst✝ : (j : α) → Decidable (j ∈ s)
δ : α → Type u_7
t : Set α
t' : (i : α) → Set (δ i)
f g : (i : α) → δ i
hf : f ∈ pi t t'
hg : g ∈ pi t t'
i : α
ht : i ∈ t
⊢ piecewise s f g i ∈ t' i
[PROOFSTEP]
by_cases hs : i ∈ s
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
δ✝ : α → Sort u_6
s : Set α
f✝ g✝ : (i : α) → δ✝ i
inst✝ : (j : α) → Decidable (j ∈ s)
δ : α → Type u_7
t : Set α
t' : (i : α) → Set (δ i)
f g : (i : α) → δ i
hf : f ∈ pi t t'
hg : g ∈ pi t t'
i : α
ht : i ∈ t
hs : i ∈ s
⊢ piecewise s f g i ∈ t' i
[PROOFSTEP]
simp [hf i ht, hg i ht, hs]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
δ✝ : α → Sort u_6
s : Set α
f✝ g✝ : (i : α) → δ✝ i
inst✝ : (j : α) → Decidable (j ∈ s)
δ : α → Type u_7
t : Set α
t' : (i : α) → Set (δ i)
f g : (i : α) → δ i
hf : f ∈ pi t t'
hg : g ∈ pi t t'
i : α
ht : i ∈ t
hs : ¬i ∈ s
⊢ piecewise s f g i ∈ t' i
[PROOFSTEP]
simp [hf i ht, hg i ht, hs]
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι✝ : Sort u_4
π : α✝ → Type u_5
δ : α✝ → Sort u_6
s✝ : Set α✝
f g : (i : α✝) → δ i
inst✝¹ : (j : α✝) → Decidable (j ∈ s✝)
ι : Type u_7
α : ι → Type u_8
s : Set ι
t t' : (i : ι) → Set (α i)
inst✝ : (x : ι) → Decidable (x ∈ s)
⊢ pi univ (piecewise s t t') = pi s t ∩ pi sᶜ t'
[PROOFSTEP]
simp [compl_eq_univ_diff]
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι✝ : Sort u_4
π : α✝ → Type u_5
δ : α✝ → Sort u_6
s✝ : Set α✝
f g : (i : α✝) → δ i
inst✝¹ : (j : α✝) → Decidable (j ∈ s✝)
ι : Type u_7
α : ι → Type u_8
s : Set ι
t : (i : ι) → Set (α i)
inst✝ : (x : ι) → Decidable (x ∈ s)
⊢ pi univ (piecewise s t fun x => univ) = pi s t
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
⊢ StrictMono (restrict s f) ↔ StrictMonoOn f s
[PROOFSTEP]
simp [Set.restrict, StrictMono, StrictMonoOn]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
fa : α → α
fb : β → β
f : α → β
g : β → γ
s t : Set α
h : Semiconj f fa fb
ha : SurjOn fa s t
⊢ SurjOn fb (f '' s) (f '' t)
[PROOFSTEP]
rintro y ⟨x, hxt, rfl⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
fa : α → α
fb : β → β
f : α → β
g : β → γ
s t : Set α
h : Semiconj f fa fb
ha : SurjOn fa s t
x : α
hxt : x ∈ t
⊢ f x ∈ fb '' (f '' s)
[PROOFSTEP]
rcases ha hxt with ⟨x, hxs, rfl⟩
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
fa : α → α
fb : β → β
f : α → β
g : β → γ
s t : Set α
h : Semiconj f fa fb
ha : SurjOn fa s t
x : α
hxs : x ∈ s
hxt : fa x ∈ t
⊢ f (fa x) ∈ fb '' (f '' s)
[PROOFSTEP]
rw [h x]
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
fa : α → α
fb : β → β
f : α → β
g : β → γ
s t : Set α
h : Semiconj f fa fb
ha : SurjOn fa s t
x : α
hxs : x ∈ s
hxt : fa x ∈ t
⊢ fb (f x) ∈ fb '' (f '' s)
[PROOFSTEP]
exact mem_image_of_mem _ (mem_image_of_mem _ hxs)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
fa : α → α
fb : β → β
f : α → β
g : β → γ
s t : Set α
h : Semiconj f fa fb
ha : Surjective fa
⊢ SurjOn fb (range f) (range f)
[PROOFSTEP]
rw [← image_univ]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
fa : α → α
fb : β → β
f : α → β
g : β → γ
s t : Set α
h : Semiconj f fa fb
ha : Surjective fa
⊢ SurjOn fb (f '' univ) (f '' univ)
[PROOFSTEP]
exact h.surjOn_image (ha.surjOn univ)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
fa : α → α
fb : β → β
f : α → β
g : β → γ
s t : Set α
h : Semiconj f fa fb
ha : InjOn fa s
hf : InjOn f (fa '' s)
⊢ InjOn fb (f '' s)
[PROOFSTEP]
rintro _ ⟨x, hx, rfl⟩ _ ⟨y, hy, rfl⟩ H
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
fa : α → α
fb : β → β
f : α → β
g : β → γ
s t : Set α
h : Semiconj f fa fb
ha : InjOn fa s
hf : InjOn f (fa '' s)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
H : fb (f x) = fb (f y)
⊢ f x = f y
[PROOFSTEP]
simp only [← h.eq] at H 
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
fa : α → α
fb : β → β
f : α → β
g : β → γ
s t : Set α
h : Semiconj f fa fb
ha : InjOn fa s
hf : InjOn f (fa '' s)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
H : f (fa x) = f (fa y)
⊢ f x = f y
[PROOFSTEP]
exact congr_arg f (ha hx hy <| hf (mem_image_of_mem fa hx) (mem_image_of_mem fa hy) H)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
fa : α → α
fb : β → β
f : α → β
g : β → γ
s t : Set α
h : Semiconj f fa fb
ha : Injective fa
hf : InjOn f (range fa)
⊢ InjOn fb (range f)
[PROOFSTEP]
rw [← image_univ] at *
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
fa : α → α
fb : β → β
f : α → β
g : β → γ
s t : Set α
h : Semiconj f fa fb
ha : Injective fa
hf : InjOn f (fa '' univ)
⊢ InjOn fb (f '' univ)
[PROOFSTEP]
exact h.injOn_image (ha.injOn univ) hf
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
fa : α → α
fb : β → β
f : α → β
g : β → γ
s t : Set α
h : Semiconj f fa fb
ha : Bijective fa
hf : Injective f
⊢ BijOn fb (range f) (range f)
[PROOFSTEP]
rw [← image_univ]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
fa : α → α
fb : β → β
f : α → β
g : β → γ
s t : Set α
h : Semiconj f fa fb
ha : Bijective fa
hf : Injective f
⊢ BijOn fb (f '' univ) (f '' univ)
[PROOFSTEP]
exact h.bijOn_image (bijective_iff_bijOn_univ.1 ha) (hf.injOn univ)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
fa : α → α
fb : β → β
f : α → β
g : β → γ
s✝ t✝ : Set α
h : Semiconj f fa fb
s t : Set β
hb : MapsTo fb s t
x : α
hx : x ∈ f ⁻¹' s
⊢ fa x ∈ f ⁻¹' t
[PROOFSTEP]
simp only [mem_preimage, h x, hb hx]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
fa : α → α
fb : β → β
f : α → β
g : β → γ
s✝ t : Set α
h : Semiconj f fa fb
s : Set β
hb : InjOn fb s
hf : InjOn f (f ⁻¹' s)
⊢ InjOn fa (f ⁻¹' s)
[PROOFSTEP]
intro x hx y hy H
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
fa : α → α
fb : β → β
f : α → β
g : β → γ
s✝ t : Set α
h : Semiconj f fa fb
s : Set β
hb : InjOn fb s
hf : InjOn f (f ⁻¹' s)
x : α
hx : x ∈ f ⁻¹' s
y : α
hy : y ∈ f ⁻¹' s
H : fa x = fa y
⊢ x = y
[PROOFSTEP]
have := congr_arg f H
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
fa : α → α
fb : β → β
f : α → β
g : β → γ
s✝ t : Set α
h : Semiconj f fa fb
s : Set β
hb : InjOn fb s
hf : InjOn f (f ⁻¹' s)
x : α
hx : x ∈ f ⁻¹' s
y : α
hy : y ∈ f ⁻¹' s
H : fa x = fa y
this : f (fa x) = f (fa y)
⊢ x = y
[PROOFSTEP]
rw [h.eq, h.eq] at this 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
fa : α → α
fb : β → β
f : α → β
g : β → γ
s✝ t : Set α
h : Semiconj f fa fb
s : Set β
hb : InjOn fb s
hf : InjOn f (f ⁻¹' s)
x : α
hx : x ∈ f ⁻¹' s
y : α
hy : y ∈ f ⁻¹' s
H : fa x = fa y
this : fb (f x) = fb (f y)
⊢ x = y
[PROOFSTEP]
exact hf hx hy (hb hx hy this)
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
ι : Sort u_4
π : α✝ → Type u_5
fa : α✝ → α✝
fb : β✝ → β✝
f : α✝ → β✝
g : β✝ → γ
s✝ t✝ : Set α✝
α : Type u_6
β : Type u_7
inst✝¹ : PartialOrder α
inst✝ : LinearOrder β
φ : β → α
ψ : α → β
t : Set β
s : Set α
hφ : MonotoneOn φ t
φψs : RightInvOn ψ φ s
ψts : MapsTo ψ s t
⊢ MonotoneOn ψ s
[PROOFSTEP]
rintro x xs y ys l
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
ι : Sort u_4
π : α✝ → Type u_5
fa : α✝ → α✝
fb : β✝ → β✝
f : α✝ → β✝
g : β✝ → γ
s✝ t✝ : Set α✝
α : Type u_6
β : Type u_7
inst✝¹ : PartialOrder α
inst✝ : LinearOrder β
φ : β → α
ψ : α → β
t : Set β
s : Set α
hφ : MonotoneOn φ t
φψs : RightInvOn ψ φ s
ψts : MapsTo ψ s t
x : α
xs : x ∈ s
y : α
ys : y ∈ s
l : x ≤ y
⊢ ψ x ≤ ψ y
[PROOFSTEP]
rcases le_total (ψ x) (ψ y) with (ψxy | ψyx)
[GOAL]
case inl
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
ι : Sort u_4
π : α✝ → Type u_5
fa : α✝ → α✝
fb : β✝ → β✝
f : α✝ → β✝
g : β✝ → γ
s✝ t✝ : Set α✝
α : Type u_6
β : Type u_7
inst✝¹ : PartialOrder α
inst✝ : LinearOrder β
φ : β → α
ψ : α → β
t : Set β
s : Set α
hφ : MonotoneOn φ t
φψs : RightInvOn ψ φ s
ψts : MapsTo ψ s t
x : α
xs : x ∈ s
y : α
ys : y ∈ s
l : x ≤ y
ψxy : ψ x ≤ ψ y
⊢ ψ x ≤ ψ y
[PROOFSTEP]
exact ψxy
[GOAL]
case inr
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
ι : Sort u_4
π : α✝ → Type u_5
fa : α✝ → α✝
fb : β✝ → β✝
f : α✝ → β✝
g : β✝ → γ
s✝ t✝ : Set α✝
α : Type u_6
β : Type u_7
inst✝¹ : PartialOrder α
inst✝ : LinearOrder β
φ : β → α
ψ : α → β
t : Set β
s : Set α
hφ : MonotoneOn φ t
φψs : RightInvOn ψ φ s
ψts : MapsTo ψ s t
x : α
xs : x ∈ s
y : α
ys : y ∈ s
l : x ≤ y
ψyx : ψ y ≤ ψ x
⊢ ψ x ≤ ψ y
[PROOFSTEP]
have := hφ (ψts ys) (ψts xs) ψyx
[GOAL]
case inr
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
ι : Sort u_4
π : α✝ → Type u_5
fa : α✝ → α✝
fb : β✝ → β✝
f : α✝ → β✝
g : β✝ → γ
s✝ t✝ : Set α✝
α : Type u_6
β : Type u_7
inst✝¹ : PartialOrder α
inst✝ : LinearOrder β
φ : β → α
ψ : α → β
t : Set β
s : Set α
hφ : MonotoneOn φ t
φψs : RightInvOn ψ φ s
ψts : MapsTo ψ s t
x : α
xs : x ∈ s
y : α
ys : y ∈ s
l : x ≤ y
ψyx : ψ y ≤ ψ x
this : φ (ψ y) ≤ φ (ψ x)
⊢ ψ x ≤ ψ y
[PROOFSTEP]
rw [φψs.eq ys, φψs.eq xs] at this 
[GOAL]
case inr
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
ι : Sort u_4
π : α✝ → Type u_5
fa : α✝ → α✝
fb : β✝ → β✝
f : α✝ → β✝
g : β✝ → γ
s✝ t✝ : Set α✝
α : Type u_6
β : Type u_7
inst✝¹ : PartialOrder α
inst✝ : LinearOrder β
φ : β → α
ψ : α → β
t : Set β
s : Set α
hφ : MonotoneOn φ t
φψs : RightInvOn ψ φ s
ψts : MapsTo ψ s t
x : α
xs : x ∈ s
y : α
ys : y ∈ s
l : x ≤ y
ψyx : ψ y ≤ ψ x
this : y ≤ x
⊢ ψ x ≤ ψ y
[PROOFSTEP]
induction le_antisymm l this
[GOAL]
case inr.refl
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
ι : Sort u_4
π : α✝ → Type u_5
fa : α✝ → α✝
fb : β✝ → β✝
f : α✝ → β✝
g : β✝ → γ
s✝ t✝ : Set α✝
α : Type u_6
β : Type u_7
inst✝¹ : PartialOrder α
inst✝ : LinearOrder β
φ : β → α
ψ : α → β
t : Set β
s : Set α
hφ : MonotoneOn φ t
φψs : RightInvOn ψ φ s
ψts : MapsTo ψ s t
x : α
xs : x ∈ s
y : α
ys : x ∈ s
l : x ≤ x
ψyx : ψ x ≤ ψ x
this : x ≤ x
⊢ ψ x ≤ ψ x
[PROOFSTEP]
exact le_refl _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g g₁ g₂ : Perm α
s t : Set α
h : MapsTo (↑g) s t
⊢ MapsTo (↑(extendDomain g f)) (Subtype.val ∘ ↑f '' s) (Subtype.val ∘ ↑f '' t)
[PROOFSTEP]
rintro _ ⟨a, ha, rfl⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g g₁ g₂ : Perm α
s t : Set α
h : MapsTo (↑g) s t
a : α
ha : a ∈ s
⊢ ↑(extendDomain g f) ((Subtype.val ∘ ↑f) a) ∈ Subtype.val ∘ ↑f '' t
[PROOFSTEP]
exact ⟨_, h ha, by simp_rw [Function.comp_apply, extendDomain_apply_image]⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g g₁ g₂ : Perm α
s t : Set α
h : MapsTo (↑g) s t
a : α
ha : a ∈ s
⊢ (Subtype.val ∘ ↑f) (↑g a) = ↑(extendDomain g f) ((Subtype.val ∘ ↑f) a)
[PROOFSTEP]
simp_rw [Function.comp_apply, extendDomain_apply_image]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g g₁ g₂ : Perm α
s t : Set α
h : SurjOn (↑g) s t
⊢ SurjOn (↑(extendDomain g f)) (Subtype.val ∘ ↑f '' s) (Subtype.val ∘ ↑f '' t)
[PROOFSTEP]
rintro _ ⟨a, ha, rfl⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g g₁ g₂ : Perm α
s t : Set α
h : SurjOn (↑g) s t
a : α
ha : a ∈ t
⊢ (Subtype.val ∘ ↑f) a ∈ ↑(extendDomain g f) '' (Subtype.val ∘ ↑f '' s)
[PROOFSTEP]
obtain ⟨b, hb, rfl⟩ := h ha
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g g₁ g₂ : Perm α
s t : Set α
h : SurjOn (↑g) s t
b : α
hb : b ∈ s
ha : ↑g b ∈ t
⊢ (Subtype.val ∘ ↑f) (↑g b) ∈ ↑(extendDomain g f) '' (Subtype.val ∘ ↑f '' s)
[PROOFSTEP]
exact ⟨_, ⟨_, hb, rfl⟩, by simp_rw [Function.comp_apply, extendDomain_apply_image]⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g g₁ g₂ : Perm α
s t : Set α
h : SurjOn (↑g) s t
b : α
hb : b ∈ s
ha : ↑g b ∈ t
⊢ ↑(extendDomain g f) ((Subtype.val ∘ ↑f) b) = (Subtype.val ∘ ↑f) (↑g b)
[PROOFSTEP]
simp_rw [Function.comp_apply, extendDomain_apply_image]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g g₁ g₂ : Perm α
s t : Set α
h : LeftInvOn (↑g₁) (↑g₂) s
⊢ LeftInvOn (↑(extendDomain g₁ f)) (↑(extendDomain g₂ f)) (Subtype.val ∘ ↑f '' s)
[PROOFSTEP]
rintro _ ⟨a, ha, rfl⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g g₁ g₂ : Perm α
s t : Set α
h : LeftInvOn (↑g₁) (↑g₂) s
a : α
ha : a ∈ s
⊢ ↑(extendDomain g₁ f) (↑(extendDomain g₂ f) ((Subtype.val ∘ ↑f) a)) = (Subtype.val ∘ ↑f) a
[PROOFSTEP]
simp_rw [Function.comp_apply, extendDomain_apply_image, h ha]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g g₁ g₂ : Perm α
s t : Set α
h : RightInvOn (↑g₁) (↑g₂) t
⊢ RightInvOn (↑(extendDomain g₁ f)) (↑(extendDomain g₂ f)) (Subtype.val ∘ ↑f '' t)
[PROOFSTEP]
rintro _ ⟨a, ha, rfl⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g g₁ g₂ : Perm α
s t : Set α
h : RightInvOn (↑g₁) (↑g₂) t
a : α
ha : a ∈ t
⊢ ↑(extendDomain g₂ f) (↑(extendDomain g₁ f) ((Subtype.val ∘ ↑f) a)) = (Subtype.val ∘ ↑f) a
[PROOFSTEP]
simp_rw [Function.comp_apply, extendDomain_apply_image, h ha]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
e : α ≃ β
s : Set α
t : Set β
h : ∀ (a : α), ↑e a ∈ t ↔ a ∈ s
b : β
hb : b ∈ t
⊢ ↑e (↑e.symm b) ∈ t
[PROOFSTEP]
rwa [apply_symm_apply]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
e : α ≃ β
s : Set α
t : Set β
inst✝ : DecidableEq α
a b : α
ha : a ∈ s
hb : b ∈ s
x : α
⊢ ↑(swap a b) x ∈ s ↔ x ∈ s
[PROOFSTEP]
obtain rfl | hxa := eq_or_ne x a
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
e : α ≃ β
s : Set α
t : Set β
inst✝ : DecidableEq α
b : α
hb : b ∈ s
x : α
ha : x ∈ s
⊢ ↑(swap x b) x ∈ s ↔ x ∈ s
[PROOFSTEP]
obtain rfl | hxb := eq_or_ne x b
[GOAL]
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
e : α ≃ β
s : Set α
t : Set β
inst✝ : DecidableEq α
a b : α
ha : a ∈ s
hb : b ∈ s
x : α
hxa : x ≠ a
⊢ ↑(swap a b) x ∈ s ↔ x ∈ s
[PROOFSTEP]
obtain rfl | hxb := eq_or_ne x b
[GOAL]
case inl.inl
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
e : α ≃ β
s : Set α
t : Set β
inst✝ : DecidableEq α
x : α
ha hb : x ∈ s
⊢ ↑(swap x x) x ∈ s ↔ x ∈ s
[PROOFSTEP]
simp [*, swap_apply_of_ne_of_ne]
[GOAL]
case inl.inr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
e : α ≃ β
s : Set α
t : Set β
inst✝ : DecidableEq α
b : α
hb : b ∈ s
x : α
ha : x ∈ s
hxb : x ≠ b
⊢ ↑(swap x b) x ∈ s ↔ x ∈ s
[PROOFSTEP]
simp [*, swap_apply_of_ne_of_ne]
[GOAL]
case inr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
e : α ≃ β
s : Set α
t : Set β
inst✝ : DecidableEq α
a : α
ha : a ∈ s
x : α
hxa : x ≠ a
hb : x ∈ s
⊢ ↑(swap a x) x ∈ s ↔ x ∈ s
[PROOFSTEP]
simp [*, swap_apply_of_ne_of_ne]
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : α → Type u_5
e : α ≃ β
s : Set α
t : Set β
inst✝ : DecidableEq α
a b : α
ha : a ∈ s
hb : b ∈ s
x : α
hxa : x ≠ a
hxb : x ≠ b
⊢ ↑(swap a b) x ∈ s ↔ x ∈ s
[PROOFSTEP]
simp [*, swap_apply_of_ne_of_ne]
