case refine'_1
α : Type u_1
β : Type u_2
γ : Type ?u.28155
ι : Sort ?u.28158
π : α → Type ?u.28163
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

case refine'_2
α : Type u_1
β : Type u_2
γ : Type ?u.28155
ι : Sort ?u.28158
π : α → Type ?u.28163
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₂)
α : Type u_1
β : Type u_2
γ : Type ?u.28155
ι : Sort ?u.28158
π : α → Type ?u.28163
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
refine' ⟨fun H => ⟨H.mono <| subset_union_left _ _, H.mono <| subset_union_right _ _, _⟩, _⟩
case refine'_1
α : Type u_1
β : Type u_2
γ : Type ?u.28155
ι : Sort ?u.28158
π : α → Type ?u.28163
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
case refine'_1
α : Type u_1
β : Type u_2
γ : Type ?u.28155
ι : Sort ?u.28158
π : α → Type ?u.28163
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
intro x hx y hy hxy
case refine'_1
α : Type u_1
β : Type u_2
γ : Type ?u.28155
ι : Sort ?u.28158
π : α → Type ?u.28163
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
case refine'_1
α : Type u_1
β : Type u_2
γ : Type ?u.28155
ι : Sort ?u.28158
π : α → Type ?u.28163
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
obtain rfl : x = y := H (Or.inl hx) (Or.inr hy) hxy
no goals
case refine'_1
α : Type u_1
β : Type u_2
γ : Type ?u.28155
ι : Sort ?u.28158
π : α → Type ?u.28163
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
exact h.le_bot ⟨hx, hy⟩
case refine'_2.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.28155
ι : Sort ?u.28158
π : α → Type ?u.28163
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₂)
case refine'_2
α : Type u_1
β : Type u_2
γ : Type ?u.28155
ι : Sort ?u.28158
π : α → Type ?u.28163
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₂)
rintro ⟨h₁, h₂, h₁₂⟩
case refine'_2.intro.intro.inl.inl
α : Type u_1
β : Type u_2
γ : Type ?u.28155
ι : Sort ?u.28158
π : α → Type ?u.28163
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.28155
ι : Sort ?u.28158
π : α → Type ?u.28163
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.28155
ι : Sort ?u.28158
π : α → Type ?u.28163
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.28155
ι : Sort ?u.28158
π : α → Type ?u.28163
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
α : Type u_1
β : Type u_2
γ : Type ?u.28155
ι : Sort ?u.28158
π : α → Type ?u.28163
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₂)
rintro x (hx | hx) y (hy | hy) hxy
no goals
case refine'_2.intro.intro.inl.inl
α : Type u_1
β : Type u_2
γ : Type ?u.28155
ι : Sort ?u.28158
π : α → Type ?u.28163
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.28155
ι : Sort ?u.28158
π : α → Type ?u.28163
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.28155
ι : Sort ?u.28158
π : α → Type ?u.28163
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.28155
ι : Sort ?u.28158
π : α → Type ?u.28163
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
exacts [h₁ hx hy hxy, (h₁₂ _ hx _ hy hxy).elim, (h₁₂ _ hy _ hx hxy.symm).elim, h₂ hx hy hxy]