-- Mathlib/Data/Set/Pairwise/Basic.lean
theorem Pairwise.disjoint_extend_bot [PartialOrder γ] [OrderBot γ]
    {e : α → β} {f : α → γ} (hf : Pairwise (Disjoint on f)) (he : FactorsThrough f e) :
    Pairwise (Disjoint on extend e f ⊥)

Proof state:
case inl.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PartialOrder γ
inst✝ : OrderBot γ
e : α → β
f : α → γ
hf : Pairwise (Disjoint on f)
he : FactorsThrough f e
b₂ : β
a₁ : α
hne : e a₁ ≠ b₂
⊢ (Disjoint on extend e f ⊥) (e a₁) b₂

Tactic:
rcases em (∃ a₂, e a₂ = b₂) with ⟨a₂, rfl⟩ | hb₂

Result:
case inl.intro.inl.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PartialOrder γ
inst✝ : OrderBot γ
e : α → β
f : α → γ
hf : Pairwise (Disjoint on f)
he : FactorsThrough f e
a₁ a₂ : α
hne : e a₁ ≠ e a₂
⊢ (Disjoint on extend e f ⊥) (e a₁) (e a₂)

case inl.intro.inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PartialOrder γ
inst✝ : OrderBot γ
e : α → β
f : α → γ
hf : Pairwise (Disjoint on f)
he : FactorsThrough f e
b₂ : β
a₁ : α
hne : e a₁ ≠ b₂
hb₂ : ¬∃ a₂, e a₂ = b₂
⊢ (Disjoint on extend e f ⊥) (e a₁) b₂

Proof state:
case inl.intro.inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PartialOrder γ
inst✝ : OrderBot γ
e : α → β
f : α → γ
hf : Pairwise (Disjoint on f)
he : FactorsThrough f e
b₂ : β
a₁ : α
hne : e a₁ ≠ b₂
hb₂ : ¬∃ a₂, e a₂ = b₂
⊢ (Disjoint on extend e f ⊥) (e a₁) b₂

Tactic:
simpa only [onFun, extend_apply' _ _ _ hb₂] using disjoint_bot_right

Result:
no goals

Proof state:
case inl.intro.inl.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PartialOrder γ
inst✝ : OrderBot γ
e : α → β
f : α → γ
hf : Pairwise (Disjoint on f)
he : FactorsThrough f e
a₁ a₂ : α
hne : e a₁ ≠ e a₂
⊢ (Disjoint on extend e f ⊥) (e a₁) (e a₂)

Tactic:
simpa only [onFun, he.extend_apply] using hf (ne_of_apply_ne e hne)

Result:
no goals

Proof state:
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PartialOrder γ
inst✝ : OrderBot γ
e : α → β
f : α → γ
hf : Pairwise (Disjoint on f)
he : FactorsThrough f e
b₁ b₂ : β
hne : b₁ ≠ b₂
hb₁ : ¬∃ a₁, e a₁ = b₁
⊢ (Disjoint on extend e f ⊥) b₁ b₂

Tactic:
simpa only [onFun, extend_apply' _ _ _ hb₁] using disjoint_bot_left

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PartialOrder γ
inst✝ : OrderBot γ
e : α → β
f : α → γ
hf : Pairwise (Disjoint on f)
he : FactorsThrough f e
⊢ Pairwise (Disjoint on extend e f ⊥)

Tactic:
intro b₁ b₂ hne

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PartialOrder γ
inst✝ : OrderBot γ
e : α → β
f : α → γ
hf : Pairwise (Disjoint on f)
he : FactorsThrough f e
b₁ b₂ : β
hne : b₁ ≠ b₂
⊢ (Disjoint on extend e f ⊥) b₁ b₂

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PartialOrder γ
inst✝ : OrderBot γ
e : α → β
f : α → γ
hf : Pairwise (Disjoint on f)
he : FactorsThrough f e
b₁ b₂ : β
hne : b₁ ≠ b₂
⊢ (Disjoint on extend e f ⊥) b₁ b₂

Tactic:
rcases em (∃ a₁, e a₁ = b₁) with ⟨a₁, rfl⟩ | hb₁

Result:
case inl.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PartialOrder γ
inst✝ : OrderBot γ
e : α → β
f : α → γ
hf : Pairwise (Disjoint on f)
he : FactorsThrough f e
b₂ : β
a₁ : α
hne : e a₁ ≠ b₂
⊢ (Disjoint on extend e f ⊥) (e a₁) b₂

case inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PartialOrder γ
inst✝ : OrderBot γ
e : α → β
f : α → γ
hf : Pairwise (Disjoint on f)
he : FactorsThrough f e
b₁ b₂ : β
hne : b₁ ≠ b₂
hb₁ : ¬∃ a₁, e a₁ = b₁
⊢ (Disjoint on extend e f ⊥) b₁ b₂