awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.PropInstances
Goal:
p q : Prop
h : q
⊢ p ≤ q ∨ q ≤ p

Tactic:
simp [h]
-- Module: Mathlib.Order.PropInstances
Goal:
p q : Prop
h : ¬q
⊢ p ≤ q ∨ q ≤ p

Tactic:
simp [h]
-- Module: Mathlib.Order.PropInstances
Goal:
⊢ LinearOrder Prop

Tactic:
exact Lattice.toLinearOrder Prop

Premises used: Lattice.toLinearOrder
-- Module: Mathlib.Order.PropInstances
Goal:
⊢ LinearOrder Prop

Tactic:
classical
  exact Lattice.toLinearOrder Prop

Premises used: Lattice.toLinearOrder
-- Module: Mathlib.Order.PropInstances
Goal:
⊢ Eq (α := Prop → Prop → Prop) (fun (x1 x2 : Prop) ↦ max x1 x2) fun (x1 x2 : Prop) ↦ x1 ∨ x2

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.PropInstances
Goal:
⊢ Eq (α := Prop → Prop → Prop) (fun (x1 x2 : Prop) ↦ min x1 x2) fun (x1 x2 : Prop) ↦ x1 ∧ x2

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.PropInstances
Goal:
ι : Type u_1
α' : ι → Type u_3
inst : (i : ι) → PartialOrder (α' i)
inst_1 : (i : ι) → OrderBot (α' i)
f g : (i : ι) → α' i
mp : Disjoint f g → ∀ (i : ι), Disjoint (f i) (g i)
mpr : (∀ (i : ι), Disjoint (f i) (g i)) → Disjoint f g
⊢ Disjoint f g ↔ ∀ (i : ι), Disjoint (f i) (g i)

Tactic:
constructor
-- Module: Mathlib.Order.PropInstances
Goal:
ι : Type u_1
α' : ι → Type u_3
inst : (i : ι) → PartialOrder (α' i)
inst_1 : (i : ι) → OrderBot (α' i)
f g : (i : ι) → α' i
h : Disjoint f g
i : ι
x : α' i
hf : x ≤ f i
hg : x ≤ g i
⊢ x ≤ ⊥

Tactic:
(update_le_iff.mp <| h (update_le_iff.mpr ⟨hf, fun _ _ => bot_le⟩)
      (update_le_iff.mpr ⟨hg, fun _ _ => bot_le⟩)).1

Premises used: Iff.mpr, And.left, update_le_iff, And.intro, Iff.mp, bot_le
-- Module: Mathlib.Order.PropInstances
Goal:
ι : Type u_1
α' : ι → Type u_3
inst : (i : ι) → PartialOrder (α' i)
inst_1 : (i : ι) → OrderBot (α' i)
f g : (i : ι) → α' i
h : Disjoint f g
i : ι
x : α' i
hf : x ≤ f i
hg : x ≤ g i
⊢ x ≤ ⊥

Tactic:
exact (update_le_iff.mp <| h (update_le_iff.mpr ⟨hf, fun _ _ => bot_le⟩)
      (update_le_iff.mpr ⟨hg, fun _ _ => bot_le⟩)).1

Premises used: Iff.mpr, And.left, update_le_iff, And.intro, Iff.mp, bot_le
-- Module: Mathlib.Order.PropInstances
Goal:
ι : Type u_1
α' : ι → Type u_3
inst : (i : ι) → PartialOrder (α' i)
inst_1 : (i : ι) → OrderBot (α' i)
f g : (i : ι) → α' i
h : ∀ (i : ι), Disjoint (f i) (g i)
x : (i : ι) → α' i
hf : x ≤ f
hg : x ≤ g
i : ι
⊢ x i ≤ ⊥ i

Tactic:
apply h i (hf i) (hg i)
-- Module: Mathlib.Order.PropInstances
Goal:
ι : Type u_1
α' : ι → Type u_3
inst : (i : ι) → PartialOrder (α' i)
inst_1 : (i : ι) → OrderBot (α' i)
f g : (i : ι) → α' i
mp : Disjoint f g → ∀ (i : ι), Disjoint (f i) (g i)
mpr mpr₁ : (∀ (i : ι), Disjoint (f i) (g i)) → Disjoint f g
⊢ Disjoint f g ↔ ∀ (i : ι), Disjoint (f i) (g i)

Tactic:
classical
  constructor
  · intro h i x hf hg
    exact (update_le_iff.mp <| h (update_le_iff.mpr ⟨hf, fun _ _ => bot_le⟩)
      (update_le_iff.mpr ⟨hg, fun _ _ => bot_le⟩)).1
  · intro h x hf hg i
    apply h i (hf i) (hg i)
-- Module: Mathlib.Order.PropInstances
Goal:
ι : Type u_1
α' : ι → Type u_3
inst : (i : ι) → PartialOrder (α' i)
inst_1 : (i : ι) → OrderTop (α' i)
f g : (i : ι) → α' i
⊢ Codisjoint f g ↔ ∀ (i : ι), Codisjoint (f i) (g i)

Tactic:
@disjoint_iff _ (fun i => (α' i)ᵒᵈ) _ _ _ _

Premises used: Codisjoint, OrderDual, Pi.disjoint_iff
-- Module: Mathlib.Order.PropInstances
Goal:
ι : Type u_1
α' : ι → Type u_3
inst : (i : ι) → PartialOrder (α' i)
inst_1 : (i : ι) → BoundedOrder (α' i)
f g : (i : ι) → α' i
simp_rw : Disjoint f g ∧ Codisjoint f g ↔ ∀ (i : ι), Disjoint (f i) (g i) ∧ Codisjoint (f i) (g i)
simp_rw₁ : (∀ (i : ι), Disjoint (f i) (g i)) ∧ Codisjoint f g ↔ ∀ (i : ι), Disjoint (f i) (g i) ∧ Codisjoint (f i) (g i)
simp_rw₂ :
  ((∀ (i : ι), Disjoint (f i) (g i)) ∧ ∀ (i : ι), Codisjoint (f i) (g i)) ↔
    ∀ (i : ι), Disjoint (f i) (g i) ∧ Codisjoint (f i) (g i)
⊢ IsCompl f g ↔ ∀ (i : ι), IsCompl (f i) (g i)

Tactic:
simp_rw [_root_.isCompl_iff, disjoint_iff, codisjoint_iff, forall_and]

Premises used: isCompl_iff, Pi.codisjoint_iff, Pi.disjoint_iff, forall_and
-- Module: Mathlib.Order.PropInstances
Goal:
α : Type u_2
inst : Subsingleton α
r : α → α → Prop
h : r = ⊤
⊢ ∀ (a : α), r a a

Tactic:
simp [h]
-- Module: Mathlib.Order.PropInstances
Goal:
α : Type u_2
inst : Subsingleton α
r : α → α → Prop
h : Std.Refl r
⊢ ∀ (a b : α), r a b = ⊤ a b

Tactic:
simp [rel_of_subsingleton]

Premises used: rel_of_subsingleton
-- Module: Mathlib.Order.PropInstances
Goal:
α : Type u_2
inst : Subsingleton α
r : α → α → Prop
h : r = ⊥
⊢ ∀ (a : α), ¬r a a

Tactic:
simp [h]
-- Module: Mathlib.Order.PropInstances
Goal:
α : Type u_2
inst : Subsingleton α
r : α → α → Prop
h : Std.Irrefl r
⊢ ∀ (a b : α), r a b = ⊥ a b

Tactic:
simp [not_rel_of_subsingleton]

Premises used: not_rel_of_subsingleton
-- Module: Mathlib.Order.PropInstances
Goal:
P Q : Prop
⊢ Disjoint P Q ↔ ¬(P ∧ Q)

Tactic:
disjoint_iff_inf_le

Premises used: disjoint_iff_inf_le, Not
-- Module: Mathlib.Order.PropInstances
Goal:
P Q : Prop
⊢ Codisjoint P Q ↔ P ∨ Q

Tactic:
codisjoint_iff_le_sup.trans <| forall_const True

Premises used: codisjoint_iff_le_sup, True, Iff.trans, forall_const
-- Module: Mathlib.Order.PropInstances
Goal:
P Q : Prop
rw : ¬(P ∧ Q) ∧ (P ∨ Q) ↔ (¬P ↔ Q)
⊢ IsCompl P Q ↔ ¬(P ↔ Q)

Tactic:
rw [_root_.isCompl_iff, Prop.disjoint_iff, Prop.codisjoint_iff, not_iff]

Premises used: Prop.codisjoint_iff, isCompl_iff, not_iff, Prop.disjoint_iff
-- Module: Mathlib.Order.PropInstances
Goal:
P Q : Prop
pos : P → (¬(P ∧ Q) ∧ (P ∨ Q) ↔ (¬P ↔ Q))
neg : ¬P → (¬(P ∧ Q) ∧ (P ∨ Q) ↔ (¬P ↔ Q))
⊢ ¬(P ∧ Q) ∧ (P ∨ Q) ↔ (¬P ↔ Q)

Tactic:
by_cases P
-- Module: Mathlib.Order.PropInstances
Goal:
P Q : Prop
h : P
pos : Q → (¬(P ∧ Q) ∧ (P ∨ Q) ↔ (¬P ↔ Q))
neg : ¬Q → (¬(P ∧ Q) ∧ (P ∨ Q) ↔ (¬P ↔ Q))
⊢ ¬(P ∧ Q) ∧ (P ∨ Q) ↔ (¬P ↔ Q)

Tactic:
by_cases Q
-- Module: Mathlib.Order.PropInstances
Goal:
P Q : Prop
h : ¬P
pos : Q → (¬(P ∧ Q) ∧ (P ∨ Q) ↔ (¬P ↔ Q))
neg : ¬Q → (¬(P ∧ Q) ∧ (P ∨ Q) ↔ (¬P ↔ Q))
⊢ ¬(P ∧ Q) ∧ (P ∨ Q) ↔ (¬P ↔ Q)

Tactic:
by_cases Q
-- Module: Mathlib.Order.PropInstances
Goal:
P Q : Prop
h : P
h_1 : Q
⊢ ¬(P ∧ Q) ∧ (P ∨ Q) ↔ (¬P ↔ Q)

Tactic:
simp [*]
-- Module: Mathlib.Order.PropInstances
Goal:
P Q : Prop
h : P
h_1 : ¬Q
⊢ ¬(P ∧ Q) ∧ (P ∨ Q) ↔ (¬P ↔ Q)

Tactic:
simp [*]
-- Module: Mathlib.Order.PropInstances
Goal:
P Q : Prop
h : ¬P
h_1 : Q
⊢ ¬(P ∧ Q) ∧ (P ∨ Q) ↔ (¬P ↔ Q)

Tactic:
simp [*]
-- Module: Mathlib.Order.PropInstances
Goal:
P Q : Prop
h : ¬P
h_1 : ¬Q
⊢ ¬(P ∧ Q) ∧ (P ∨ Q) ↔ (¬P ↔ Q)

Tactic:
simp [*]
-- Module: Mathlib.Order.Quotient
Goal:
α : Type u_1
s : Setoid α
inst : LE α
⊢ ∀ (a₁ b₁ a₂ b₂ : α),
    a₁ ≈ a₂ →
      b₁ ≈ b₂ →
        Relation.TransGen (fun (x y : α) ↦ x ≤ y ∨ x ≈ y) a₁ b₁ =
          Relation.TransGen (fun (x y : α) ↦ x ≤ y ∨ x ≈ y) a₂ b₂

Tactic:
fun x₁ x₂ y₁ y₂ hx hy ↦ propext ⟨?_, ?_⟩

Premises used: Iff.intro, propext
-- Module: Mathlib.Order.Quotient
Goal:
α : Type u_1
s : Setoid α
inst : LE α
refine_1 :
  ∀ (x₁ x₂ y₁ y₂ : α) (hx : x₁ ≈ y₁) (hy : x₂ ≈ y₂),
    Relation.TransGen (fun (x y : α) ↦ x ≤ y ∨ x ≈ y) x₁ x₂ → Relation.TransGen (fun (x y : α) ↦ x ≤ y ∨ x ≈ y) y₁ y₂
refine_2 :
  ∀ (x₁ x₂ y₁ y₂ : α) (hx : x₁ ≈ y₁) (hy : x₂ ≈ y₂),
    Relation.TransGen (fun (x y : α) ↦ x ≤ y ∨ x ≈ y) y₁ y₂ → Relation.TransGen (fun (x y : α) ↦ x ≤ y ∨ x ≈ y) x₁ x₂
⊢ ∀ (a₁ b₁ a₂ b₂ : α),
    a₁ ≈ a₂ →
      b₁ ≈ b₂ →
        Relation.TransGen (fun (x y : α) ↦ x ≤ y ∨ x ≈ y) a₁ b₁ =
          Relation.TransGen (fun (x y : α) ↦ x ≤ y ∨ x ≈ y) a₂ b₂

Tactic:
refine fun x₁ x₂ y₁ y₂ hx hy ↦ propext ⟨?_, ?_⟩

Premises used: Iff.intro, propext
-- Module: Mathlib.Order.Quotient
Goal:
α : Type u_1
s : Setoid α
inst : LE α
x₁ x₂ y₁ y₂ : α
hx : x₁ ≈ y₁
hy : x₂ ≈ y₂
h : Relation.TransGen (fun (x y : α) ↦ x ≤ y ∨ x ≈ y) x₁ x₂
⊢ Relation.TransGen (fun (x y : α) ↦ x ≤ y ∨ x ≈ y) y₁ y₂

Tactic:
.trans (.single <| .inr (symm hx)) <| .trans h (.single <| .inr hy)

Premises used: Relation.TransGen.trans, Relation.TransGen.single, symm, Or.inr
-- Module: Mathlib.Order.Quotient
Goal:
α : Type u_1
s : Setoid α
inst : LE α
x₁ x₂ y₁ y₂ : α
hx : x₁ ≈ y₁
hy : x₂ ≈ y₂
h : Relation.TransGen (fun (x y : α) ↦ x ≤ y ∨ x ≈ y) x₁ x₂
⊢ Relation.TransGen (fun (x y : α) ↦ x ≤ y ∨ x ≈ y) y₁ y₂

Tactic:
exact .trans (.single <| .inr (symm hx)) <| .trans h (.single <| .inr hy)
-- Module: Mathlib.Order.Quotient
Goal:
α : Type u_1
s : Setoid α
inst : LE α
x₁ x₂ y₁ y₂ : α
hx : x₁ ≈ y₁
hy : x₂ ≈ y₂
h : Relation.TransGen (fun (x y : α) ↦ x ≤ y ∨ x ≈ y) y₁ y₂
⊢ Relation.TransGen (fun (x y : α) ↦ x ≤ y ∨ x ≈ y) x₁ x₂

Tactic:
.trans (.single <| .inr hx) <| .trans h (.single <| .inr (symm hy))

Premises used: Relation.TransGen.trans, Relation.TransGen.single, symm, Or.inr
-- Module: Mathlib.Order.Quotient
Goal:
α : Type u_1
s : Setoid α
inst : LE α
x₁ x₂ y₁ y₂ : α
hx : x₁ ≈ y₁
hy : x₂ ≈ y₂
h : Relation.TransGen (fun (x y : α) ↦ x ≤ y ∨ x ≈ y) y₁ y₂
⊢ Relation.TransGen (fun (x y : α) ↦ x ≤ y ∨ x ≈ y) x₁ x₂

Tactic:
exact .trans (.single <| .inr hx) <| .trans h (.single <| .inr (symm hy))
-- Module: Mathlib.Order.Quotient
Goal:
α : Type u_1
s : Setoid α
inst : LE α
x y : α
⊢ ⟦x⟧ ≤ ⟦y⟧ ↔ Relation.TransGen (fun (x y : α) ↦ x ≤ y ∨ x ≈ y) x y

Tactic:
.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Order.Quotient
Goal:
α : Type u_1
s : Setoid α
inst : LE α
x : Quotient s
h : ∀ (x : α), ⟦x⟧ ≤ ⟦x⟧
⊢ x ≤ x

Tactic:
induction x using Quotient.inductionOn with | h x
-- Module: Mathlib.Order.Quotient
Goal:
α : Type u_1
s : Setoid α
inst : LE α
x : α
⊢ ⟦x⟧ ≤ ⟦x⟧

Tactic:
.single <| .inr (refl x)

Premises used: Relation.TransGen.single, refl, Or.inr
-- Module: Mathlib.Order.Quotient
Goal:
α : Type u_1
s : Setoid α
inst : LE α
x : α
⊢ ⟦x⟧ ≤ ⟦x⟧

Tactic:
exact .single <| .inr (refl x)
-- Module: Mathlib.Order.Quotient
Goal:
α : Type u_1
s : Setoid α
inst : LE α
x y z : Quotient s
h₁ : x ≤ y
h₂ : y ≤ z
h : ∀ (x : α) (h₁ : ⟦x⟧ ≤ y), ⟦x⟧ ≤ z
⊢ x ≤ z

Tactic:
induction x using Quotient.inductionOn with | h x
-- Module: Mathlib.Order.Quotient
Goal:
α : Type u_1
s : Setoid α
inst : LE α
y z : Quotient s
h₂ : y ≤ z
x : α
h₁ : ⟦x⟧ ≤ y
h : ∀ (y : α) (h₂ : ⟦y⟧ ≤ z) (h₁ : ⟦x⟧ ≤ ⟦y⟧), ⟦x⟧ ≤ z
⊢ ⟦x⟧ ≤ z

Tactic:
induction y using Quotient.inductionOn with | h y
-- Module: Mathlib.Order.Quotient
Goal:
α : Type u_1
s : Setoid α
inst : LE α
z : Quotient s
x y : α
h₂ : ⟦y⟧ ≤ z
h₁ : ⟦x⟧ ≤ ⟦y⟧
h : ∀ (z : α) (h₂ : ⟦y⟧ ≤ ⟦z⟧), ⟦x⟧ ≤ ⟦z⟧
⊢ ⟦x⟧ ≤ z

Tactic:
induction z using Quotient.inductionOn with | h z
-- Module: Mathlib.Order.Quotient
Goal:
α : Type u_1
s : Setoid α
inst : LE α
x y : α
h₁ : ⟦x⟧ ≤ ⟦y⟧
z : α
h₂ : ⟦y⟧ ≤ ⟦z⟧
⊢ ⟦x⟧ ≤ ⟦z⟧

Tactic:
Relation.TransGen.trans h₁ h₂

Premises used: Relation.TransGen.trans
-- Module: Mathlib.Order.Quotient
Goal:
α : Type u_1
s : Setoid α
inst : LE α
x y : α
h₁ : ⟦x⟧ ≤ ⟦y⟧
z : α
h₂ : ⟦y⟧ ≤ ⟦z⟧
⊢ ⟦x⟧ ≤ ⟦z⟧

Tactic:
exact Relation.TransGen.trans h₁ h₂

Premises used: Relation.TransGen.trans
-- Module: Mathlib.Order.Quotient
Goal:
α : Type u_1
s : Setoid α
inst : LE α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
x y : Quotient s
h : ∀ (x : α), ⟦x⟧ ≤ y ∨ y ≤ ⟦x⟧
⊢ x ≤ y ∨ y ≤ x

Tactic:
induction x using Quotient.inductionOn with | h x
-- Module: Mathlib.Order.Quotient
Goal:
α : Type u_1
s : Setoid α
inst : LE α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
y : Quotient s
x : α
h : ∀ (y : α), ⟦x⟧ ≤ ⟦y⟧ ∨ ⟦y⟧ ≤ ⟦x⟧
⊢ ⟦x⟧ ≤ y ∨ y ≤ ⟦x⟧

Tactic:
induction y using Quotient.inductionOn with | h y
-- Module: Mathlib.Order.Quotient
Goal:
α : Type u_1
s : Setoid α
inst : LE α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
x y : α
h : ∀ (h : x ≤ y), ⟦x⟧ ≤ ⟦y⟧ ∨ ⟦y⟧ ≤ ⟦x⟧
h₁ : ∀ (h : y ≤ x), ⟦x⟧ ≤ ⟦y⟧ ∨ ⟦y⟧ ≤ ⟦x⟧
⊢ ⟦x⟧ ≤ ⟦y⟧ ∨ ⟦y⟧ ≤ ⟦x⟧

Tactic:
obtain h | h := total_of (· ≤ ·) x y

Premises used: LE.le, total_of
-- Module: Mathlib.Order.Quotient
Goal:
α : Type u_1
s : Setoid α
inst : LE α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
x y : α
h : x ≤ y
⊢ ⟦x⟧ ≤ ⟦y⟧ ∨ ⟦y⟧ ≤ ⟦x⟧

Tactic:
.inl <| .single <| .inl h

Premises used: Relation.TransGen.single, Or.inl
-- Module: Mathlib.Order.Quotient
Goal:
α : Type u_1
s : Setoid α
inst : LE α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
x y : α
h : x ≤ y
⊢ ⟦x⟧ ≤ ⟦y⟧ ∨ ⟦y⟧ ≤ ⟦x⟧

Tactic:
exact .inl <| .single <| .inl h
-- Module: Mathlib.Order.Quotient
Goal:
α : Type u_1
s : Setoid α
inst : LE α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
x y : α
h : y ≤ x
⊢ ⟦x⟧ ≤ ⟦y⟧ ∨ ⟦y⟧ ≤ ⟦x⟧

Tactic:
.inr <| .single <| .inl h

Premises used: Relation.TransGen.single, Or.inl, Or.inr
-- Module: Mathlib.Order.Quotient
Goal:
α : Type u_1
s : Setoid α
inst : LE α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
x y : α
h : y ≤ x
⊢ ⟦x⟧ ≤ ⟦y⟧ ∨ ⟦y⟧ ≤ ⟦x⟧

Tactic:
exact .inr <| .single <| .inl h
-- Module: Mathlib.Order.Quotient
Goal:
α : Type u_1
s : Setoid α
inst : Preorder α
⊢ Monotone (Quotient.mk s)

Tactic:
fun _ _ h ↦ .single (.inl h)

Premises used: Monotone, Relation.TransGen.single, Or.inl
-- Module: Mathlib.Order.Quotient
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
s : Setoid α
inst_1 : Preorder β
f : α → β
hf : Monotone f
H : ∀ (x₁ x₂ : α), x₁ ≈ x₂ → f x₁ = f x₂
x y : Quotient s
h : x ≤ y
h₁ : ∀ (x : α) (h : ⟦x⟧ ≤ y), Quotient.lift f H ⟦x⟧ ≤ Quotient.lift f H y
⊢ Quotient.lift f H x ≤ Quotient.lift f H y

Tactic:
induction x using Quotient.inductionOn with | h x
-- Module: Mathlib.Order.Quotient
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
s : Setoid α
inst_1 : Preorder β
f : α → β
hf : Monotone f
H : ∀ (x₁ x₂ : α), x₁ ≈ x₂ → f x₁ = f x₂
y : Quotient s
x : α
h : ⟦x⟧ ≤ y
h₁ : ∀ (y : α) (h : ⟦x⟧ ≤ ⟦y⟧), Quotient.lift f H ⟦x⟧ ≤ Quotient.lift f H ⟦y⟧
⊢ Quotient.lift f H ⟦x⟧ ≤ Quotient.lift f H y

Tactic:
induction y using Quotient.inductionOn with | h y
-- Module: Mathlib.Order.Quotient
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
s : Setoid α
inst_1 : Preorder β
f : α → β
hf : Monotone f
H : ∀ (x₁ x₂ : α), x₁ ≈ x₂ → f x₁ = f x₂
x y : α
h : ⟦x⟧ ≤ ⟦y⟧
h₁ : ∀ {b : α}, x ≤ b ∨ x ≈ b → Quotient.lift f H ⟦x⟧ ≤ Quotient.lift f H ⟦b⟧
h₂ :
  ∀ {b c : α},
    Relation.TransGen (fun (x y : α) ↦ x ≤ y ∨ x ≈ y) x b →
      b ≤ c ∨ b ≈ c → Quotient.lift f H ⟦x⟧ ≤ Quotient.lift f H ⟦b⟧ → Quotient.lift f H ⟦x⟧ ≤ Quotient.lift f H ⟦c⟧
⊢ Quotient.lift f H ⟦x⟧ ≤ Quotient.lift f H ⟦y⟧

Tactic:
induction h
-- Module: Mathlib.Order.Quotient
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
s : Setoid α
inst_1 : Preorder β
f : α → β
hf : Monotone f
H : ∀ (x₁ x₂ : α), x₁ ≈ x₂ → f x₁ = f x₂
x y b c : α
h_1 : Relation.TransGen (fun (x y : α) ↦ x ≤ y ∨ x ≈ y) x b
h_2 : b ≤ c ∨ b ≈ c
IH : Quotient.lift f H ⟦x⟧ ≤ Quotient.lift f H ⟦b⟧
h : Quotient.lift f H ⟦b⟧ ≤ Quotient.lift f H ⟦c⟧
⊢ Quotient.lift f H ⟦x⟧ ≤ Quotient.lift f H ⟦c⟧

Tactic:
apply IH.trans

Premises used: LE.le.trans
-- Module: Mathlib.Order.Quotient
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
s : Setoid α
inst_1 : Preorder β
f : α → β
hf : Monotone f
H : ∀ (x₁ x₂ : α), x₁ ≈ x₂ → f x₁ = f x₂
x y b c : α
h_1 : Relation.TransGen (fun (x y : α) ↦ x ≤ y ∨ x ≈ y) x b
h_2 : b ≤ c ∨ b ≈ c
a_ih : Quotient.lift f H ⟦x⟧ ≤ Quotient.lift f H ⟦b⟧
h : Quotient.lift f H ⟦b⟧ ≤ Quotient.lift f H ⟦c⟧
⊢ Quotient.lift f H ⟦x⟧ ≤ Quotient.lift f H ⟦c⟧

Tactic:
on_goal 2 => rename_i IH; apply IH.trans
-- Module: Mathlib.Order.Quotient
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
s : Setoid α
inst_1 : Preorder β
f : α → β
hf : Monotone f
H : ∀ (x₁ x₂ : α), x₁ ≈ x₂ → f x₁ = f x₂
x y b : α
h : x ≤ b
⊢ Quotient.lift f H ⟦x⟧ ≤ Quotient.lift f H ⟦b⟧

Tactic:
hf h
-- Module: Mathlib.Order.Quotient
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
s : Setoid α
inst_1 : Preorder β
f : α → β
hf : Monotone f
H : ∀ (x₁ x₂ : α), x₁ ≈ x₂ → f x₁ = f x₂
x y b : α
h : x ≤ b
⊢ Quotient.lift f H ⟦x⟧ ≤ Quotient.lift f H ⟦b⟧

Tactic:
exact hf h
-- Module: Mathlib.Order.Quotient
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
s : Setoid α
inst_1 : Preorder β
f : α → β
hf : Monotone f
H : ∀ (x₁ x₂ : α), x₁ ≈ x₂ → f x₁ = f x₂
x y b : α
h : x ≈ b
⊢ Quotient.lift f H ⟦x⟧ ≤ Quotient.lift f H ⟦b⟧

Tactic:
(H _ _ h).le

Premises used: Eq.le
-- Module: Mathlib.Order.Quotient
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
s : Setoid α
inst_1 : Preorder β
f : α → β
hf : Monotone f
H : ∀ (x₁ x₂ : α), x₁ ≈ x₂ → f x₁ = f x₂
x y b : α
h : x ≈ b
⊢ Quotient.lift f H ⟦x⟧ ≤ Quotient.lift f H ⟦b⟧

Tactic:
exact (H _ _ h).le

Premises used: Eq.le
-- Module: Mathlib.Order.Quotient
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
s : Setoid α
inst_1 : Preorder β
f : α → β
hf : Monotone f
H : ∀ (x₁ x₂ : α), x₁ ≈ x₂ → f x₁ = f x₂
x y b : α
h : x ≤ b ∨ x ≈ b
h₁ : ∀ (h : x ≤ b), Quotient.lift f H ⟦x⟧ ≤ Quotient.lift f H ⟦b⟧
h₂ : ∀ (h : x ≈ b), Quotient.lift f H ⟦x⟧ ≤ Quotient.lift f H ⟦b⟧
⊢ Quotient.lift f H ⟦x⟧ ≤ Quotient.lift f H ⟦b⟧

Tactic:
cases h with
    | inl h => exact hf h
    | inr h => exact (H _ _ h).le

Premises used: Eq.le
-- Module: Mathlib.Order.Quotient
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
s : Setoid α
inst_1 : Preorder β
f : α → β
hf : Monotone f
H : ∀ (x₁ x₂ : α), x₁ ≈ x₂ → f x₁ = f x₂
x y b c : α
h_1 : Relation.TransGen (fun (x y : α) ↦ x ≤ y ∨ x ≈ y) x b
IH : Quotient.lift f H ⟦x⟧ ≤ Quotient.lift f H ⟦b⟧
h : b ≤ c
⊢ Quotient.lift f H ⟦b⟧ ≤ Quotient.lift f H ⟦c⟧

Tactic:
hf h
-- Module: Mathlib.Order.Quotient
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
s : Setoid α
inst_1 : Preorder β
f : α → β
hf : Monotone f
H : ∀ (x₁ x₂ : α), x₁ ≈ x₂ → f x₁ = f x₂
x y b c : α
h_1 : Relation.TransGen (fun (x y : α) ↦ x ≤ y ∨ x ≈ y) x b
IH : Quotient.lift f H ⟦x⟧ ≤ Quotient.lift f H ⟦b⟧
h : b ≤ c
⊢ Quotient.lift f H ⟦b⟧ ≤ Quotient.lift f H ⟦c⟧

Tactic:
exact hf h
-- Module: Mathlib.Order.Quotient
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
s : Setoid α
inst_1 : Preorder β
f : α → β
hf : Monotone f
H : ∀ (x₁ x₂ : α), x₁ ≈ x₂ → f x₁ = f x₂
x y b c : α
h_1 : Relation.TransGen (fun (x y : α) ↦ x ≤ y ∨ x ≈ y) x b
IH : Quotient.lift f H ⟦x⟧ ≤ Quotient.lift f H ⟦b⟧
h : b ≈ c
⊢ Quotient.lift f H ⟦b⟧ ≤ Quotient.lift f H ⟦c⟧

Tactic:
(H _ _ h).le

Premises used: Eq.le
-- Module: Mathlib.Order.Quotient
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
s : Setoid α
inst_1 : Preorder β
f : α → β
hf : Monotone f
H : ∀ (x₁ x₂ : α), x₁ ≈ x₂ → f x₁ = f x₂
x y b c : α
h_1 : Relation.TransGen (fun (x y : α) ↦ x ≤ y ∨ x ≈ y) x b
IH : Quotient.lift f H ⟦x⟧ ≤ Quotient.lift f H ⟦b⟧
h : b ≈ c
⊢ Quotient.lift f H ⟦b⟧ ≤ Quotient.lift f H ⟦c⟧

Tactic:
exact (H _ _ h).le

Premises used: Eq.le
-- Module: Mathlib.Order.Quotient
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
s : Setoid α
inst_1 : Preorder β
f : α → β
hf : Monotone f
H : ∀ (x₁ x₂ : α), x₁ ≈ x₂ → f x₁ = f x₂
x y b c : α
h_1 : Relation.TransGen (fun (x y : α) ↦ x ≤ y ∨ x ≈ y) x b
h : b ≤ c ∨ b ≈ c
IH : Quotient.lift f H ⟦x⟧ ≤ Quotient.lift f H ⟦b⟧
h₁ : ∀ (h : b ≤ c), Quotient.lift f H ⟦b⟧ ≤ Quotient.lift f H ⟦c⟧
h₂ : ∀ (h : b ≈ c), Quotient.lift f H ⟦b⟧ ≤ Quotient.lift f H ⟦c⟧
⊢ Quotient.lift f H ⟦b⟧ ≤ Quotient.lift f H ⟦c⟧

Tactic:
cases h with
    | inl h => exact hf h
    | inr h => exact (H _ _ h).le

Premises used: Eq.le
-- Module: Mathlib.Order.Quotient
Goal:
α : Type u_1
s : Setoid α
inst : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
x y : α
rw : (⟦x⟧ ≤ ⟦y⟧) = (x ≤ y ∨ x ≈ y)
⊢ ⟦x⟧ ≤ ⟦y⟧ ↔ x ≤ y ∨ x ≈ y

Tactic:
rw [← propext_iff]

Premises used: propext_iff
-- Module: Mathlib.Order.Quotient
Goal:
α : Type u_1
s : Setoid α
inst : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
x y : α
revert : ∀ {x y : α}, (⟦x⟧ ≤ ⟦y⟧) = (x ≤ y ∨ x ≈ y)
⊢ (⟦x⟧ ≤ ⟦y⟧) = (x ≤ y ∨ x ≈ y)

Tactic:
revert x y
-- Module: Mathlib.Order.Quotient
Goal:
α : Type u_1
s : Setoid α
inst : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
apply : ∀ (x y z : α) (h₁ : x ≤ y ∨ x ≈ y) (h₂ : y ≤ z ∨ y ≈ z), x ≤ z ∨ x ≈ z
⊢ ∀ {x y : α}, (⟦x⟧ ≤ ⟦y⟧) = (x ≤ y ∨ x ≈ y)

Tactic:
apply congrFun₂ <| @Relation.transGen_eq_self α _ ⟨fun x y z h₁ h₂ ↦ ?_⟩

Premises used: congrFun₂, Relation.transGen_eq_self
-- Module: Mathlib.Order.Quotient
Goal:
α : Type u_1
s : Setoid α
inst : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
x y z : α
h₁ : x ≤ y ∨ x ≈ y
h₂ : y ≤ z ∨ y ≈ z
inl : x ≤ y → x ≤ z ∨ x ≈ z
inr : x ≈ y → x ≤ z ∨ x ≈ z
⊢ x ≤ z ∨ x ≈ z

Tactic:
cases h₁
-- Module: Mathlib.Order.Quotient
Goal:
α : Type u_1
s : Setoid α
inst : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
x y z : α
h₂ : y ≤ z ∨ y ≈ z
h : x ≤ y
inl : y ≤ z → x ≤ z ∨ x ≈ z
inl₁ : y ≈ z → x ≤ z ∨ x ≈ z
⊢ x ≤ z ∨ x ≈ z

Tactic:
cases h₂
-- Module: Mathlib.Order.Quotient
Goal:
α : Type u_1
s : Setoid α
inst : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
x y z : α
h₂ : y ≤ z ∨ y ≈ z
h : x ≈ y
inr : y ≤ z → x ≤ z ∨ x ≈ z
inr₁ : y ≈ z → x ≤ z ∨ x ≈ z
⊢ x ≤ z ∨ x ≈ z

Tactic:
cases h₂
-- Module: Mathlib.Order.Quotient
Goal:
α : Type u_1
s : Setoid α
inst : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
x y z : α
h₁ : x ≤ y
h₂ : y ≤ z
⊢ x ≤ z ∨ x ≈ z

Tactic:
.inl <| h₁.trans h₂

Premises used: Or.inl, LE.le.trans
-- Module: Mathlib.Order.Quotient
Goal:
α : Type u_1
s : Setoid α
inst : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
x y z : α
h₁ : x ≤ y
h₂ : y ≤ z
⊢ x ≤ z ∨ x ≈ z

Tactic:
exact .inl <| h₁.trans h₂

Premises used: LE.le.trans
-- Module: Mathlib.Order.Quotient
Goal:
α : Type u_1
s : Setoid α
inst : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
x y z : α
h₁ : x ≤ y
h₂ : y ≈ z
inl : z < x → x ≈ z
⊢ x ≤ z ∨ x ≈ z

Tactic:
rw [or_iff_not_imp_left, not_le]

Premises used: not_le, Classical.or_iff_not_imp_left
-- Module: Mathlib.Order.Quotient
Goal:
α : Type u_1
s : Setoid α
inst : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
x y z : α
h₁ : x ≤ y
h₂ : y ≈ z
inl : ∀ (h₂ : ⟦y⟧ = ⟦z⟧), z < x → ⟦x⟧ = ⟦z⟧
⊢ z < x → x ≈ z

Tactic:
rw [← Quotient.eq_iff_equiv] at *

Premises used: Quotient.eq_iff_equiv
-- Module: Mathlib.Order.Quotient
Goal:
α : Type u_1
s : Setoid α
inst : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
x y z : α
h₁ : x ≤ y
h₂ : ⟦y⟧ = ⟦z⟧
⊢ z < x → ⟦x⟧ = ⟦z⟧

Tactic:
fun h ↦ ((H _).out h₂.symm rfl ⟨h.le, h₁⟩).trans h₂

Premises used: Set.OrdConnected.out, LT.lt.le, Quotient.mk, And.intro, Eq.symm, rfl, Eq.trans
-- Module: Mathlib.Order.Quotient
Goal:
α : Type u_1
s : Setoid α
inst : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
x y z : α
h₁ : x ≤ y
h₂ : ⟦y⟧ = ⟦z⟧
⊢ z < x → ⟦x⟧ = ⟦z⟧

Tactic:
exact fun h ↦ ((H _).out h₂.symm rfl ⟨h.le, h₁⟩).trans h₂

Premises used: Set.OrdConnected.out, Quotient.mk, And.intro, Eq.symm, rfl, Eq.trans
-- Module: Mathlib.Order.Quotient
Goal:
α : Type u_1
s : Setoid α
inst : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
x y z : α
h₁ : x ≈ y
h₂ : y ≤ z
inr : z < x → x ≈ z
⊢ x ≤ z ∨ x ≈ z

Tactic:
rw [or_iff_not_imp_left, not_le]

Premises used: not_le, Classical.or_iff_not_imp_left
-- Module: Mathlib.Order.Quotient
Goal:
α : Type u_1
s : Setoid α
inst : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
x y z : α
h₁ : x ≈ y
h₂ : y ≤ z
inr : ∀ (h₁ : ⟦x⟧ = ⟦y⟧) (h₂ : y ≤ z), z < x → ⟦x⟧ = ⟦z⟧
⊢ z < x → x ≈ z

Tactic:
rw [← Quotient.eq_iff_equiv] at *

Premises used: Quotient.eq_iff_equiv
-- Module: Mathlib.Order.Quotient
Goal:
α : Type u_1
s : Setoid α
inst : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
x y z : α
h₁ : ⟦x⟧ = ⟦y⟧
h₂ : y ≤ z
⊢ z < x → ⟦x⟧ = ⟦z⟧

Tactic:
fun h ↦ ((H _).out h₁.symm rfl ⟨h₂, h.le⟩).symm

Premises used: Set.OrdConnected.out, LT.lt.le, Quotient.mk, And.intro, Eq.symm, rfl
-- Module: Mathlib.Order.Quotient
Goal:
α : Type u_1
s : Setoid α
inst : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
x y z : α
h₁ : ⟦x⟧ = ⟦y⟧
h₂ : y ≤ z
⊢ z < x → ⟦x⟧ = ⟦z⟧

Tactic:
exact fun h ↦ ((H _).out h₁.symm rfl ⟨h₂, h.le⟩).symm

Premises used: Set.OrdConnected.out, Quotient.mk, And.intro, Eq.symm, rfl
-- Module: Mathlib.Order.Quotient
Goal:
α : Type u_1
s : Setoid α
inst : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
x y z : α
h₁ : x ≈ y
h₂ : y ≈ z
⊢ x ≤ z ∨ x ≈ z

Tactic:
.inr (_root_.trans h₁ h₂)

Premises used: trans, Or.inr
-- Module: Mathlib.Order.Quotient
Goal:
α : Type u_1
s : Setoid α
inst : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
x y z : α
h₁ : x ≈ y
h₂ : y ≈ z
⊢ x ≤ z ∨ x ≈ z

Tactic:
exact .inr (_root_.trans h₁ h₂)