awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.PrimeSeparator (goal)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : BoundedOrder α
F : PFilter α
I : Ideal α
hFI : Disjoint (↑F : Set α) (↑I : Set α)
S : Set (Set α) := {J : Set α | IsIdeal J ∧ (↑I : Set α) ≤ J ∧ Disjoint (↑F : Set α) J}
Jset : Set α
left : (↑I : Set α) ⊆ Jset
hmax : Maximal (fun (x : Set α) ↦ x ∈ S) Jset
Jidl : IsIdeal Jset
IJ : (↑I : Set α) ≤ Jset
J : Ideal α := Jidl.toIdeal (I := Jset)
IJ' : I ≤ J
Jpr : J.IsProper
a₁ a₂ : α
ha₁ : a₁ ∉ J
ha₂ : a₂ ∉ J
J₁ : Ideal α := J ⊔ principal a₁
J₂ : Ideal α := J ⊔ principal a₂
a₁J₁ : a₁ ∈ J₁
a₂J₂ : a₂ ∈ J₂
J₁J : (↑J₁ : Set α) ≠ Jset
J₂J : (↑J₂ : Set α) ≠ Jset
J₁S : (↑J₁ : Set α) ∉ S
J₂S : (↑J₂ : Set α) ∉ S
J₁F : ¬Disjoint (↑F : Set α) (↑J₁ : Set α)
J₂F : ¬Disjoint (↑F : Set α) (↑J₂ : Set α)
c₁ : α
c₁F : c₁ ∈ (↑F : Set α)
c₁J₁ : c₁ ∈ (↑J₁ : Set α)
c₂ : α
c₂F : c₂ ∈ (↑F : Set α)
c₂J₂ : c₂ ∈ (↑J₂ : Set α)
b₁ : α
b₁J : b₁ ∈ J
cba₁ : c₁ ≤ b₁ ⊔ a₁
b₂ : α
b₂J : b₂ ∈ J
cba₂ : c₂ ≤ b₂ ⊔ a₂
b : α := b₁ ⊔ b₂
bJ : b ∈ J
ineq : c₁ ⊓ c₂ ≤ b ⊔ a₁ ⊓ a₂
ba₁a₂F : b ⊔ a₁ ⊓ a₂ ∈ F
ha₁a₂ : a₁ ⊓ a₂ ∈ J
⊢ ¬Disjoint (↑F : Set α) Jset
have h : ∃ x ∈ (↑F : Set α), x ∈ Jset
Tactic: rw [Set.not_disjoint_iff]
-- Lean 4 proof step from Mathlib.Order.PrimeSeparator (goal)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : BoundedOrder α
F : PFilter α
I : Ideal α
hFI : Disjoint (↑F : Set α) (↑I : Set α)
S : Set (Set α) := {J : Set α | IsIdeal J ∧ (↑I : Set α) ≤ J ∧ Disjoint (↑F : Set α) J}
Jset : Set α
left : (↑I : Set α) ⊆ Jset
hmax : Maximal (fun (x : Set α) ↦ x ∈ S) Jset
Jidl : IsIdeal Jset
IJ : (↑I : Set α) ≤ Jset
J : Ideal α := Jidl.toIdeal (I := Jset)
IJ' : I ≤ J
Jpr : J.IsProper
a₁ a₂ : α
ha₁ : a₁ ∉ J
ha₂ : a₂ ∉ J
J₁ : Ideal α := J ⊔ principal a₁
J₂ : Ideal α := J ⊔ principal a₂
a₁J₁ : a₁ ∈ J₁
a₂J₂ : a₂ ∈ J₂
J₁J : (↑J₁ : Set α) ≠ Jset
J₂J : (↑J₂ : Set α) ≠ Jset
J₁S : (↑J₁ : Set α) ∉ S
J₂S : (↑J₂ : Set α) ∉ S
J₁F : ¬Disjoint (↑F : Set α) (↑J₁ : Set α)
J₂F : ¬Disjoint (↑F : Set α) (↑J₂ : Set α)
c₁ : α
c₁F : c₁ ∈ (↑F : Set α)
c₁J₁ : c₁ ∈ (↑J₁ : Set α)
c₂ : α
c₂F : c₂ ∈ (↑F : Set α)
c₂J₂ : c₂ ∈ (↑J₂ : Set α)
b₁ : α
b₁J : b₁ ∈ J
cba₁ : c₁ ≤ b₁ ⊔ a₁
b₂ : α
b₂J : b₂ ∈ J
cba₂ : c₂ ≤ b₂ ⊔ a₂
b : α := b₁ ⊔ b₂
bJ : b ∈ J
ineq : c₁ ⊓ c₂ ≤ b ⊔ a₁ ⊓ a₂
ba₁a₂F : b ⊔ a₁ ⊓ a₂ ∈ F
ha₁a₂ : a₁ ⊓ a₂ ∈ J
⊢ ∃ x ∈ (↑F : Set α), x ∈ Jset
have h : b ⊔ a₁ ⊓ a₂ ∈ (↑F : Set α) ∧ b ⊔ a₁ ⊓ a₂ ∈ Jset
Tactic: use b ⊔ (a₁ ⊓ a₂)
-- Lean 4 proof step from Mathlib.Order.PropInstances (goal)
Goal:
p q : Prop
⊢ p ≤ q ∨ q ≤ p
have pos : ∀ (h : q), p ≤ q ∨ q ≤ p
Tactic: by_cases h : q
-- Lean 4 proof step from Mathlib.Order.PropInstances (goal)
Goal:
p q : Prop
pos : ∀ (h : q), p ≤ q ∨ q ≤ p
⊢ p ≤ q ∨ q ≤ p
have neg : ∀ (h : ¬q), p ≤ q ∨ q ≤ p
Tactic: by_cases h : q
-- Lean 4 proof step from Mathlib.Order.PropInstances (goal)
Goal:
ι : Type u_1
α' : ι → Type u_3
inst : (i : ι) → PartialOrder (α' i)
inst_1 : (i : ι) → OrderBot (α' i)
f g : (i : ι) → α' i
⊢ Disjoint f g ↔ ∀ (i : ι), Disjoint (f i) (g i)
have mp : Disjoint f g → ∀ (i : ι), Disjoint (f i) (g i)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.PropInstances (goal)
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)
⊢ Disjoint f g ↔ ∀ (i : ι), Disjoint (f i) (g i)
have mpr : (∀ (i : ι), Disjoint (f i) (g i)) → Disjoint f g
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.PropInstances (goal)
Goal:
ι : Type u_1
α' : ι → Type u_3
inst : (i : ι) → PartialOrder (α' i)
inst_1 : (i : ι) → OrderBot (α' i)
f g : (i : ι) → α' i
⊢ Disjoint f g ↔ ∀ (i : ι), Disjoint (f i) (g i)
have mp : 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)
-- Lean 4 proof step from Mathlib.Order.PropInstances (goal)
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)
⊢ Disjoint f g ↔ ∀ (i : ι), Disjoint (f i) (g i)
have mpr : (∀ (i : ι), Disjoint (f i) (g i)) → Disjoint f g
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)
-- Lean 4 proof step from Mathlib.Order.PropInstances (goal)
Goal:
ι : Type u_1
α' : ι → Type u_3
inst : (i : ι) → PartialOrder (α' i)
inst_1 : (i : ι) → BoundedOrder (α' i)
f g : (i : ι) → α' i
⊢ IsCompl f g ↔ ∀ (i : ι), IsCompl (f i) (g i)
have simp_rw : Disjoint f g ∧ Codisjoint f g ↔ ∀ (i : ι), Disjoint (f i) (g i) ∧ Codisjoint (f i) (g i)
Tactic: simp_rw [_root_.isCompl_iff, disjoint_iff, codisjoint_iff, forall_and]
-- Lean 4 proof step from Mathlib.Order.PropInstances (goal)
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)
⊢ IsCompl f g ↔ ∀ (i : ι), IsCompl (f i) (g i)
have simp_rw₁ : (∀ (i : ι), Disjoint (f i) (g i)) ∧ Codisjoint f g ↔ ∀ (i : ι), Disjoint (f i) (g i) ∧ Codisjoint (f i) (g i)
Tactic: simp_rw [_root_.isCompl_iff, disjoint_iff, codisjoint_iff, forall_and]
-- Lean 4 proof step from Mathlib.Order.PropInstances (goal)
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)
⊢ IsCompl f g ↔ ∀ (i : ι), IsCompl (f i) (g i)
have 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)
Tactic: simp_rw [_root_.isCompl_iff, disjoint_iff, codisjoint_iff, forall_and]
-- Lean 4 proof step from Mathlib.Order.PropInstances (goal)
Goal:
P Q : Prop
⊢ IsCompl P Q ↔ ¬(P ↔ Q)
have rw : ¬(P ∧ Q) ∧ (P ∨ Q) ↔ (¬P ↔ Q)
Tactic: rw [_root_.isCompl_iff, Prop.disjoint_iff, Prop.codisjoint_iff, not_iff]
-- Lean 4 proof step from Mathlib.Order.PropInstances (goal)
Goal:
P Q : Prop
⊢ ¬(P ∧ Q) ∧ (P ∨ Q) ↔ (¬P ↔ Q)
have pos : P → (¬(P ∧ Q) ∧ (P ∨ Q) ↔ (¬P ↔ Q))
Tactic: by_cases P
-- Lean 4 proof step from Mathlib.Order.PropInstances (goal)
Goal:
P Q : Prop
pos : P → (¬(P ∧ Q) ∧ (P ∨ Q) ↔ (¬P ↔ Q))
⊢ ¬(P ∧ Q) ∧ (P ∨ Q) ↔ (¬P ↔ Q)
have neg : ¬P → (¬(P ∧ Q) ∧ (P ∨ Q) ↔ (¬P ↔ Q))
Tactic: by_cases P
-- Lean 4 proof step from Mathlib.Order.PropInstances (goal)
Goal:
P Q : Prop
h : P
⊢ ¬(P ∧ Q) ∧ (P ∨ Q) ↔ (¬P ↔ Q)
have pos : Q → (¬(P ∧ Q) ∧ (P ∨ Q) ↔ (¬P ↔ Q))
Tactic: by_cases Q
-- Lean 4 proof step from Mathlib.Order.PropInstances (goal)
Goal:
P Q : Prop
h : P
pos : Q → (¬(P ∧ Q) ∧ (P ∨ Q) ↔ (¬P ↔ Q))
⊢ ¬(P ∧ Q) ∧ (P ∨ Q) ↔ (¬P ↔ Q)
have neg : ¬Q → (¬(P ∧ Q) ∧ (P ∨ Q) ↔ (¬P ↔ Q))
Tactic: by_cases Q
-- Lean 4 proof step from Mathlib.Order.PropInstances (goal)
Goal:
P Q : Prop
h : ¬P
⊢ ¬(P ∧ Q) ∧ (P ∨ Q) ↔ (¬P ↔ Q)
have pos : Q → (¬(P ∧ Q) ∧ (P ∨ Q) ↔ (¬P ↔ Q))
Tactic: by_cases Q
-- Lean 4 proof step from Mathlib.Order.PropInstances (goal)
Goal:
P Q : Prop
h : ¬P
pos : Q → (¬(P ∧ Q) ∧ (P ∨ Q) ↔ (¬P ↔ Q))
⊢ ¬(P ∧ Q) ∧ (P ∨ Q) ↔ (¬P ↔ Q)
have neg : ¬Q → (¬(P ∧ Q) ∧ (P ∨ Q) ↔ (¬P ↔ Q))
Tactic: by_cases Q
-- Lean 4 proof step from Mathlib.Order.Quotient (goal)
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₂
have 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₂
Tactic: refine fun x₁ x₂ y₁ y₂ hx hy ↦ propext ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Quotient (goal)
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₂
⊢ ∀ (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₂
have 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₂
Tactic: refine fun x₁ x₂ y₁ y₂ hx hy ↦ propext ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Quotient (goal)
Goal:
α : Type u_1
s : Setoid α
inst : LE α
x : Quotient s
⊢ x ≤ x
have h : ∀ (x : α), ⟦x⟧ ≤ ⟦x⟧
Tactic: induction x using Quotient.inductionOn with | h x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.Quotient (goal)
Goal:
α : Type u_1
s : Setoid α
inst : LE α
x y z : Quotient s
h₁ : x ≤ y
h₂ : y ≤ z
⊢ x ≤ z
have h : ∀ (x : α) (h₁ : ⟦x⟧ ≤ y), ⟦x⟧ ≤ z
Tactic: induction x using Quotient.inductionOn with | h x
Cleared hypotheses: x, h₁
-- Lean 4 proof step from Mathlib.Order.Quotient (goal)
Goal:
α : Type u_1
s : Setoid α
inst : LE α
y z : Quotient s
h₂ : y ≤ z
x : α
h₁ : ⟦x⟧ ≤ y
⊢ ⟦x⟧ ≤ z
have h : ∀ (y : α) (h₂ : ⟦y⟧ ≤ z) (h₁ : ⟦x⟧ ≤ ⟦y⟧), ⟦x⟧ ≤ z
Tactic: induction y using Quotient.inductionOn with | h y
Cleared hypotheses: y, h₂, h₁
-- Lean 4 proof step from Mathlib.Order.Quotient (goal)
Goal:
α : Type u_1
s : Setoid α
inst : LE α
z : Quotient s
x y : α
h₂ : ⟦y⟧ ≤ z
h₁ : ⟦x⟧ ≤ ⟦y⟧
⊢ ⟦x⟧ ≤ z
have h : ∀ (z : α) (h₂ : ⟦y⟧ ≤ ⟦z⟧), ⟦x⟧ ≤ ⟦z⟧
Tactic: induction z using Quotient.inductionOn with | h z
Cleared hypotheses: z, h₂
-- Lean 4 proof step from Mathlib.Order.Quotient (goal)
Goal:
α : Type u_1
s : Setoid α
inst : LE α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
x y : Quotient s
⊢ x ≤ y ∨ y ≤ x
have h : ∀ (x : α), ⟦x⟧ ≤ y ∨ y ≤ ⟦x⟧
Tactic: induction x using Quotient.inductionOn with | h x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.Quotient (goal)
Goal:
α : Type u_1
s : Setoid α
inst : LE α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
y : Quotient s
x : α
⊢ ⟦x⟧ ≤ y ∨ y ≤ ⟦x⟧
have h : ∀ (y : α), ⟦x⟧ ≤ ⟦y⟧ ∨ ⟦y⟧ ≤ ⟦x⟧
Tactic: induction y using Quotient.inductionOn with | h y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Order.Quotient (goal)
Goal:
α : Type u_1
s : Setoid α
inst : LE α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
x y : α
⊢ ⟦x⟧ ≤ ⟦y⟧ ∨ ⟦y⟧ ≤ ⟦x⟧
have h : ∀ (h : x ≤ y), ⟦x⟧ ≤ ⟦y⟧ ∨ ⟦y⟧ ≤ ⟦x⟧
Tactic: obtain h | h := total_of (· ≤ ·) x y
-- Lean 4 proof step from Mathlib.Order.Quotient (goal)
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⟧
⊢ ⟦x⟧ ≤ ⟦y⟧ ∨ ⟦y⟧ ≤ ⟦x⟧
have h₁ : ∀ (h : y ≤ x), ⟦x⟧ ≤ ⟦y⟧ ∨ ⟦y⟧ ≤ ⟦x⟧
Tactic: obtain h | h := total_of (· ≤ ·) x y
-- Lean 4 proof step from Mathlib.Order.Quotient (goal)
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
⊢ Quotient.lift f H x ≤ Quotient.lift f H y
have h₁ : ∀ (x : α) (h : ⟦x⟧ ≤ y), Quotient.lift f H ⟦x⟧ ≤ Quotient.lift f H y
Tactic: induction x using Quotient.inductionOn with | h x
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Order.Quotient (goal)
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
⊢ Quotient.lift f H ⟦x⟧ ≤ Quotient.lift f H y
have h₁ : ∀ (y : α) (h : ⟦x⟧ ≤ ⟦y⟧), Quotient.lift f H ⟦x⟧ ≤ Quotient.lift f H ⟦y⟧
Tactic: induction y using Quotient.inductionOn with | h y
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.Order.Quotient (goal)
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⟧
⊢ Quotient.lift f H ⟦x⟧ ≤ Quotient.lift f H ⟦y⟧
have h₁ : ∀ {b : α}, x ≤ b ∨ x ≈ b → Quotient.lift f H ⟦x⟧ ≤ Quotient.lift f H ⟦b⟧
Tactic: induction h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Quotient (goal)
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⟧
⊢ Quotient.lift f H ⟦x⟧ ≤ Quotient.lift f H ⟦y⟧
have 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⟧
Tactic: induction h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Quotient (goal)
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 : Relation.TransGen (fun (x y : α) ↦ x ≤ y ∨ x ≈ y) x b
h_1 : b ≤ c ∨ b ≈ c
IH : Quotient.lift f H ⟦x⟧ ≤ Quotient.lift f H ⟦b⟧
⊢ Quotient.lift f H ⟦x⟧ ≤ Quotient.lift f H ⟦c⟧
have h : Quotient.lift f H ⟦b⟧ ≤ Quotient.lift f H ⟦c⟧
Tactic: apply IH.trans
-- Lean 4 proof step from Mathlib.Order.Quotient (goal)
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 : Relation.TransGen (fun (x y : α) ↦ x ≤ y ∨ x ≈ y) x b
h_1 : b ≤ c ∨ b ≈ c
a_ih : Quotient.lift f H ⟦x⟧ ≤ Quotient.lift f H ⟦b⟧
⊢ Quotient.lift f H ⟦x⟧ ≤ Quotient.lift f H ⟦c⟧
have h : Quotient.lift f H ⟦b⟧ ≤ Quotient.lift f H ⟦c⟧
Tactic: on_goal 2 => rename_i IH; apply IH.trans
-- Lean 4 proof step from Mathlib.Order.Quotient (goal)
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
⊢ Quotient.lift f H ⟦x⟧ ≤ Quotient.lift f H ⟦b⟧
have h₁ : ∀ (h : x ≤ 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Quotient (goal)
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⟧
⊢ Quotient.lift f H ⟦x⟧ ≤ Quotient.lift f H ⟦b⟧
have h₂ : ∀ (h : x ≈ 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Quotient (goal)
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⟧
⊢ Quotient.lift f H ⟦b⟧ ≤ Quotient.lift f H ⟦c⟧
have h₁ : ∀ (h : b ≤ 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Quotient (goal)
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⟧
⊢ Quotient.lift f H ⟦b⟧ ≤ Quotient.lift f H ⟦c⟧
have h₂ : ∀ (h : b ≈ 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Quotient (goal)
Goal:
α : Type u_1
s : Setoid α
inst : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
x y : α
⊢ ⟦x⟧ ≤ ⟦y⟧ ↔ x ≤ y ∨ x ≈ y
have rw : (⟦x⟧ ≤ ⟦y⟧) = (x ≤ y ∨ x ≈ y)
Tactic: rw [← propext_iff]
-- Lean 4 proof step from Mathlib.Order.Quotient (goal)
Goal:
α : Type u_1
s : Setoid α
inst : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
x y : α
⊢ (⟦x⟧ ≤ ⟦y⟧) = (x ≤ y ∨ x ≈ y)
have revert : ∀ {x y : α}, (⟦x⟧ ≤ ⟦y⟧) = (x ≤ y ∨ x ≈ y)
Tactic: revert x y
Cleared hypotheses: x, y
-- Lean 4 proof step from Mathlib.Order.Quotient (goal)
Goal:
α : Type u_1
s : Setoid α
inst : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
⊢ ∀ {x y : α}, (⟦x⟧ ≤ ⟦y⟧) = (x ≤ y ∨ x ≈ y)
have apply : ∀ (x y z : α) (h₁ : x ≤ y ∨ x ≈ y) (h₂ : y ≤ z ∨ y ≈ z), x ≤ z ∨ x ≈ z
Tactic: apply congrFun₂ <| @Relation.transGen_eq_self α _ ⟨fun x y z h₁ h₂ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.Quotient (goal)
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
⊢ x ≤ z ∨ x ≈ z
have inl : x ≤ y → x ≤ z ∨ x ≈ z
Tactic: cases h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Order.Quotient (goal)
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
⊢ x ≤ z ∨ x ≈ z
have inr : x ≈ y → x ≤ z ∨ x ≈ z
Tactic: cases h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Order.Quotient (goal)
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
⊢ x ≤ z ∨ x ≈ z
have inl : y ≤ z → x ≤ z ∨ x ≈ z
Tactic: cases h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Order.Quotient (goal)
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
⊢ x ≤ z ∨ x ≈ z
have inl₁ : y ≈ z → x ≤ z ∨ x ≈ z
Tactic: cases h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Order.Quotient (goal)
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
⊢ x ≤ z ∨ x ≈ z
have inr : y ≤ z → x ≤ z ∨ x ≈ z
Tactic: cases h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Order.Quotient (goal)
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
⊢ x ≤ z ∨ x ≈ z
have inr₁ : y ≈ z → x ≤ z ∨ x ≈ z
Tactic: cases h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Order.Quotient (goal)
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
have inl : z < x → x ≈ z
Tactic: rw [or_iff_not_imp_left, not_le]
-- Lean 4 proof step from Mathlib.Order.Quotient (goal)
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
have inl : ∀ (h₂ : ⟦y⟧ = ⟦z⟧), z < x → ⟦x⟧ = ⟦z⟧
Tactic: rw [← Quotient.eq_iff_equiv] at *
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Order.Quotient (goal)
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
have inr : z < x → x ≈ z
Tactic: rw [or_iff_not_imp_left, not_le]
-- Lean 4 proof step from Mathlib.Order.Quotient (goal)
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
have inr : ∀ (h₁ : ⟦x⟧ = ⟦y⟧) (h₂ : y ≤ z), z < x → ⟦x⟧ = ⟦z⟧
Tactic: rw [← Quotient.eq_iff_equiv] at *
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Order.Quotient (goal)
Goal:
α : Type u_1
s : Setoid α
inst : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
inst_1 : DecidableRel fun (x1 x2 : α) ↦ x1 ≈ x2
x y : Quotient s
h₁ : x ≤ y
h₂ : y ≤ x
⊢ x = y
have h : ∀ (x : α) (h₁ : ⟦x⟧ ≤ y) (h₂ : y ≤ ⟦x⟧), ⟦x⟧ = y
Tactic: induction x using Quotient.inductionOn with | h x
Cleared hypotheses: x, h₁, h₂
-- Lean 4 proof step from Mathlib.Order.Quotient (goal)
Goal:
α : Type u_1
s : Setoid α
inst : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
inst_1 : DecidableRel fun (x1 x2 : α) ↦ x1 ≈ x2
y : Quotient s
x : α
h₁ : ⟦x⟧ ≤ y
h₂ : y ≤ ⟦x⟧
⊢ ⟦x⟧ = y
have h : ∀ (y : α) (h₁ : ⟦x⟧ ≤ ⟦y⟧) (h₂ : ⟦y⟧ ≤ ⟦x⟧), ⟦x⟧ = ⟦y⟧
Tactic: induction y using Quotient.inductionOn with | h y
Cleared hypotheses: y, h₁, h₂
-- Lean 4 proof step from Mathlib.Order.Quotient (hypothesis)
Goal:
α : Type u_1
s : Setoid α
inst : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
inst_1 : DecidableRel fun (x1 x2 : α) ↦ x1 ≈ x2
x y : α
h₁ : ⟦x⟧ ≤ ⟦y⟧
h₂ : ⟦y⟧ ≤ ⟦x⟧
⊢ ⟦x⟧ = ⟦y⟧
have h₃ : x ≤ y ∨ x ≈ y
Tactic: rw [mk_le_mk] at h₁ h₂
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Order.Quotient (hypothesis)
Goal:
α : Type u_1
s : Setoid α
inst : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
inst_1 : DecidableRel fun (x1 x2 : α) ↦ x1 ≈ x2
x y : α
h₁ : ⟦x⟧ ≤ ⟦y⟧
h₂ : ⟦y⟧ ≤ ⟦x⟧
h₃ : x ≤ y ∨ x ≈ y
⊢ ⟦x⟧ = ⟦y⟧
have h₄ : y ≤ x ∨ y ≈ x
Tactic: rw [mk_le_mk] at h₁ h₂
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Order.Quotient (goal)
Goal:
α : Type u_1
s : Setoid α
inst : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
inst_1 : DecidableRel fun (x1 x2 : α) ↦ x1 ≈ x2
x y : α
h₂ : y ≤ x ∨ y ≈ x
h₁ : x ≤ y
⊢ ⟦x⟧ = ⟦y⟧
have h : ∀ (h : y ≈ x), ⟦x⟧ = ⟦y⟧
Tactic: cases h₂ with
      | inr h => exact (Quotient.sound h).symm
      | inl h₂ => exact congrArg _ (h₁.antisymm h₂)
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Order.Quotient (goal)
Goal:
α : Type u_1
s : Setoid α
inst : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
inst_1 : DecidableRel fun (x1 x2 : α) ↦ x1 ≈ x2
x y : α
h₂ : y ≤ x ∨ y ≈ x
h₁ : x ≤ y
h : ∀ (h : y ≈ x), ⟦x⟧ = ⟦y⟧
⊢ ⟦x⟧ = ⟦y⟧
have h₃ : ∀ (h₂ : y ≤ x), ⟦x⟧ = ⟦y⟧
Tactic: cases h₂ with
      | inr h => exact (Quotient.sound h).symm
      | inl h₂ => exact congrArg _ (h₁.antisymm h₂)
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Order.Quotient (goal)
Goal:
α : Type u_1
s : Setoid α
inst : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
inst_1 : DecidableRel fun (x1 x2 : α) ↦ x1 ≈ x2
x y : α
h₁ : x ≤ y ∨ x ≈ y
h₂ : y ≤ x ∨ y ≈ x
⊢ ⟦x⟧ = ⟦y⟧
have h : ∀ (h : x ≈ y), ⟦x⟧ = ⟦y⟧
Tactic: cases h₁ with
    | inr h => exact Quotient.sound h
    | inl h₁ =>
      cases h₂ with
      | inr h => exact (Quotient.sound h).symm
      | inl h₂ => exact congrArg _ (h₁.antisymm h₂)
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Order.Quotient (goal)
Goal:
α : Type u_1
s : Setoid α
inst : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
inst_1 : DecidableRel fun (x1 x2 : α) ↦ x1 ≈ x2
x y : α
h₁ : x ≤ y ∨ x ≈ y
h₂ : y ≤ x ∨ y ≈ x
h : ∀ (h : x ≈ y), ⟦x⟧ = ⟦y⟧
⊢ ⟦x⟧ = ⟦y⟧
have h₃ : ∀ (h₁ : x ≤ y), ⟦x⟧ = ⟦y⟧
Tactic: cases h₁ with
    | inr h => exact Quotient.sound h
    | inl h₁ =>
      cases h₂ with
      | inr h => exact (Quotient.sound h).symm
      | inl h₂ => exact congrArg _ (h₁.antisymm h₂)
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Order.Quotient (goal)
Goal:
α : Type u_1
s : Setoid α
inst : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
x y : α
⊢ ⟦x⟧ < ⟦y⟧ ↔ x < y ∧ ¬x ≈ y
have contrapose! : ⟦y⟧ ≤ ⟦x⟧ ↔ y ≤ x ∨ x ≈ y
Tactic: contrapose! +distrib
-- Lean 4 proof step from Mathlib.Order.Quotient (goal)
Goal:
α : Type u_1
s : Setoid α
inst : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
x y : α
⊢ ⟦y⟧ ≤ ⟦x⟧ ↔ y ≤ x ∨ x ≈ y
have rw : y ≤ x ∨ y ≈ x ↔ y ≤ x ∨ x ≈ y
Tactic: rw [mk_le_mk, comm_of (· ≈ ·)]