awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : α
rw : y ≤ x ∨ y ≈ x ↔ y ≤ x ∨ x ≈ y
⊢ ⟦y⟧ ≤ ⟦x⟧ ↔ y ≤ x ∨ x ≈ y
have rw₁ : y ≤ x ∨ x ≈ y ↔ y ≤ x ∨ x ≈ y
Tactic: rw [mk_le_mk, comm_of (· ≈ ·)]
-- 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! : ¬⟦x⟧ < ⟦y⟧ ↔ ¬(x < y ∧ ¬x ≈ y)
Tactic: classical
  contrapose! +distrib
  rw [mk_le_mk, comm_of (· ≈ ·)]
-- 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 : α
contrapose! contrapose!₁ : ¬⟦x⟧ < ⟦y⟧ ↔ ¬(x < y ∧ ¬x ≈ y)
⊢ ⟦x⟧ < ⟦y⟧ ↔ x < y ∧ ¬x ≈ y
have contrapose!₂ : ⟦y⟧ ≤ ⟦x⟧ ↔ y ≤ x ∨ x ≈ y
Tactic: classical
  contrapose! +distrib
  rw [mk_le_mk, comm_of (· ≈ ·)]
-- Lean 4 proof step from Mathlib.Order.Radical (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
β : Type u_2
inst_1 : CompleteLattice β
f : α ≃o β
⊢ (f : (a : α) → β) (Order.radical α) = Order.radical β
have unfold : Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) (⨅ (a : α), ⨅ (_ : Membership.mem (γ := Set α) {H : α | IsCoatom H} a), a) : β)
  (⨅ (a : β), ⨅ (_ : Membership.mem (γ := Set β) {H : β | IsCoatom H} a), a : β)
Tactic: unfold Order.radical
-- Lean 4 proof step from Mathlib.Order.Radical (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
β : Type u_2
inst_1 : CompleteLattice β
f : α ≃o β
⊢ Eq.{u_2 + 1} (α := β)
    ((f : (a : α) → β) (⨅ (a : α), ⨅ (_ : Membership.mem (γ := Set α) {H : α | IsCoatom H} a), a) : β)
    (⨅ (a : β), ⨅ (_ : Membership.mem (γ := Set β) {H : β | IsCoatom H} a), a : β)
have simp : Eq.{u_2 + 1} (α := β) (⨅ (i : α), ⨅ (_ : Membership.mem (γ := Set α) {H : α | IsCoatom H} i), (f : (a : α) → β) i)
  (⨅ (a : β), ⨅ (_ : Membership.mem (γ := Set β) {H : β | IsCoatom H} a), a)
Tactic: simp only [OrderIso.map_iInf]
-- Lean 4 proof step from Mathlib.Order.Radical (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
β : Type u_2
inst_1 : CompleteLattice β
f : α ≃o β
⊢ Eq.{u_2 + 1} (α := β) (⨅ (i : α), ⨅ (_ : Membership.mem (γ := Set α) {H : α | IsCoatom H} i), (f : (a : α) → β) i)
    (⨅ (a : β), ⨅ (_ : Membership.mem (γ := Set β) {H : β | IsCoatom H} a), a)
have e : α ≃ β
Tactic: fapply Equiv.iInf_congr
-- Lean 4 proof step from Mathlib.Order.Radical (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
β : Type u_2
inst_1 : CompleteLattice β
f : α ≃o β
e : α ≃ β
⊢ Eq.{u_2 + 1} (α := β) (⨅ (i : α), ⨅ (_ : Membership.mem (γ := Set α) {H : α | IsCoatom H} i), (f : (a : α) → β) i)
    (⨅ (a : β), ⨅ (_ : Membership.mem (γ := Set β) {H : β | IsCoatom H} a), a)
have h : ∀ (x : α),
  Eq.{u_2 + 1} (α := β)
    (⨅ (_ :
      Membership.mem.{u_2, u_2} (α := β) (γ := Set β) {H : β | IsCoatom H}
        ((f.toEquiv (r := fun (x1 x2 : α) ↦ x1 ≤ x2) (s := fun (x1 x2 : β) ↦ x1 ≤ x2) : (a : α) → β) x : β)),
      (f.toEquiv (r := fun (x1 x2 : α) ↦ x1 ≤ x2) (s := fun (x1 x2 : β) ↦ x1 ≤ x2) : (a : α) → β) x)
    (⨅ (_ : Membership.mem (γ := Set α) {H : α | IsCoatom H} x), (f : (a : α) → β) x)
Tactic: fapply Equiv.iInf_congr
-- Lean 4 proof step from Mathlib.Order.Radical (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
inst_1 : IsCoatomic α
a : α
h : a ⊔ radical α = ⊤
⊢ a = ⊤
have inl : ∀ (h : ⊤ ⊔ radical α = ⊤), Eq.{u_1 + 1} (α := α) ⊤ ⊤
Tactic: obtain (rfl | w) := eq_top_or_exists_le_coatom a
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Order.Radical (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
inst_1 : IsCoatomic α
a : α
h : a ⊔ radical α = ⊤
inl : ∀ (h : ⊤ ⊔ radical α = ⊤), Eq.{u_1 + 1} (α := α) ⊤ ⊤
⊢ a = ⊤
have inr : ∀ (w : ∃ (a_1 : α), IsCoatom a_1 ∧ a ≤ a_1), a = ⊤
Tactic: obtain (rfl | w) := eq_top_or_exists_le_coatom a
-- Lean 4 proof step from Mathlib.Order.Radical (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
inst_1 : IsCoatomic α
a : α
h : a ⊔ radical α = ⊤
w : ∃ (a_1 : α), IsCoatom a_1 ∧ a ≤ a_1
⊢ a = ⊤
have inr : ∀ (m : α) (c : IsCoatom m) (le : a ≤ m), a = ⊤
Tactic: obtain ⟨m, c, le⟩ := w
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.Order.Radical (hypothesis)
Goal:
α : Type u_1
inst : CompleteLattice α
inst_1 : IsCoatomic α
a : α
h : a ⊔ radical α = ⊤
m : α
c : IsCoatom m
le : a ≤ m
⊢ a = ⊤
have q : a ⊔ radical α ≤ m
Tactic: have q : a ⊔ radical α ≤ m := sup_le le (radical_le_coatom c)
-- Lean 4 proof step from Mathlib.Order.Radical (hypothesis)
Goal:
α : Type u_1
inst : CompleteLattice α
inst_1 : IsCoatomic α
a : α
h : a ⊔ radical α = ⊤
m : α
c : IsCoatom m
le : a ≤ m
q : a ⊔ radical α ≤ m
⊢ a = ⊤
have q₁ : m = ⊤
Tactic: rw [h, top_le_iff] at q
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Order.Rel.GaloisConnection (goal)
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
J : Set α
⊢ R.leftDual J ∈ R.rightFixedPoints
have a : R.leftDual (R.rightDual (R.leftDual J)) ≤ R.leftDual J
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.Rel.GaloisConnection (goal)
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
J : Set α
a : R.leftDual (R.rightDual (R.leftDual J)) ≤ R.leftDual J
⊢ R.leftDual J ∈ R.rightFixedPoints
have a₁ : R.leftDual J ≤ R.leftDual (R.rightDual (R.leftDual J))
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.Rel.GaloisConnection (goal)
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
J : Set α
⊢ R.leftDual (R.rightDual (R.leftDual J)) ≤ R.leftDual J
have a : J ≤ R.rightDual (R.leftDual J)
Tactic: apply R.gc_leftDual_rightDual.monotone_l
-- Lean 4 proof step from Mathlib.Order.Rel.GaloisConnection (goal)
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
I : Set β
⊢ R.rightDual I ∈ R.leftFixedPoints
have a : R.rightDual (R.leftDual (R.rightDual I)) ≤ R.rightDual I
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.Rel.GaloisConnection (goal)
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
I : Set β
a : R.rightDual (R.leftDual (R.rightDual I)) ≤ R.rightDual I
⊢ R.rightDual I ∈ R.leftFixedPoints
have a₁ : R.rightDual I ≤ R.rightDual (R.leftDual (R.rightDual I))
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.Rel.GaloisConnection (goal)
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
I : Set β
⊢ R.rightDual (R.leftDual (R.rightDual I)) ≤ R.rightDual I
have a : (fun (b : β) ↦ ∀ ⦃a : α⦄, a ∈ R.rightDual I → (a, b) ∈ R) ≤ I
Tactic: apply R.gc_leftDual_rightDual.monotone_u
-- Lean 4 proof step from Mathlib.Order.Rel.GaloisConnection (goal)
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
J : (↑R.leftFixedPoints : Type u_1)
⊢ (fun (x : (↑R.rightFixedPoints : Type u_2)) ↦
        (match (motive := (↑R.rightFixedPoints : Type u_2) → (↑R.leftFixedPoints : Type u_1)) x with
          | ⟨I, property⟩ => Subtype.mk (p := fun (x : Set α) ↦ x ∈ R.leftFixedPoints) (R.rightDual I) ⋯ :
          (↑R.leftFixedPoints : Type u_1)))
      ((fun (x : (↑R.leftFixedPoints : Type u_1)) ↦
          (match (motive := (↑R.leftFixedPoints : Type u_1) → (↑R.rightFixedPoints : Type u_2)) x with
            | ⟨J, property⟩ => Subtype.mk (p := fun (x : Set β) ↦ x ∈ R.rightFixedPoints) (R.leftDual J) ⋯ :
            (↑R.rightFixedPoints : Type u_2)))
        J) =
    J
have obtain : ∀ (J : Set α) (hJ : J ∈ R.leftFixedPoints),
  (fun (x : (↑R.rightFixedPoints : Type u_2)) ↦
        (match (motive := (↑R.rightFixedPoints : Type u_2) → (↑R.leftFixedPoints : Type u_1)) x with
          | ⟨I, property⟩ => Subtype.mk (p := fun (x : Set α) ↦ x ∈ R.leftFixedPoints) (R.rightDual I) sorry :
          (↑R.leftFixedPoints : Type u_1)))
      ((fun (x : (↑R.leftFixedPoints : Type u_1)) ↦
          (match (motive := (↑R.leftFixedPoints : Type u_1) → (↑R.rightFixedPoints : Type u_2)) x with
            | ⟨J, property⟩ => Subtype.mk (p := fun (x : Set β) ↦ x ∈ R.rightFixedPoints) (R.leftDual J) sorry :
            (↑R.rightFixedPoints : Type u_2)))
        (Subtype.mk (p := fun (x : Set α) ↦ x ∈ R.leftFixedPoints) J hJ)) =
    Subtype.mk (p := fun (x : Set α) ↦ x ∈ R.leftFixedPoints) J hJ
Tactic: obtain ⟨J, hJ⟩ := J
Cleared hypotheses: J
-- Lean 4 proof step from Mathlib.Order.Rel.GaloisConnection (goal)
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
J : Set α
hJ : J ∈ R.leftFixedPoints
⊢ (fun (x : (↑R.rightFixedPoints : Type u_2)) ↦
        (match (motive := (↑R.rightFixedPoints : Type u_2) → (↑R.leftFixedPoints : Type u_1)) x with
          | ⟨I, property⟩ => Subtype.mk (p := fun (x : Set α) ↦ x ∈ R.leftFixedPoints) (R.rightDual I) ⋯ :
          (↑R.leftFixedPoints : Type u_1)))
      ((fun (x : (↑R.leftFixedPoints : Type u_1)) ↦
          (match (motive := (↑R.leftFixedPoints : Type u_1) → (↑R.rightFixedPoints : Type u_2)) x with
            | ⟨J, property⟩ => Subtype.mk (p := fun (x : Set β) ↦ x ∈ R.rightFixedPoints) (R.leftDual J) ⋯ :
            (↑R.rightFixedPoints : Type u_2)))
        (Subtype.mk (p := fun (x : Set α) ↦ x ∈ R.leftFixedPoints) J hJ)) =
    Subtype.mk (p := fun (x : Set α) ↦ x ∈ R.leftFixedPoints) J hJ
have rw : R.rightDual (R.leftDual J) = J
Tactic: rw [Subtype.mk.injEq, hJ]
-- Lean 4 proof step from Mathlib.Order.Rel.GaloisConnection (goal)
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
J : Set α
hJ : J ∈ R.leftFixedPoints
rw : R.rightDual (R.leftDual J) = J
⊢ (fun (x : (↑R.rightFixedPoints : Type u_2)) ↦
        (match (motive := (↑R.rightFixedPoints : Type u_2) → (↑R.leftFixedPoints : Type u_1)) x with
          | ⟨I, property⟩ => Subtype.mk (p := fun (x : Set α) ↦ x ∈ R.leftFixedPoints) (R.rightDual I) ⋯ :
          (↑R.leftFixedPoints : Type u_1)))
      ((fun (x : (↑R.leftFixedPoints : Type u_1)) ↦
          (match (motive := (↑R.leftFixedPoints : Type u_1) → (↑R.rightFixedPoints : Type u_2)) x with
            | ⟨J, property⟩ => Subtype.mk (p := fun (x : Set β) ↦ x ∈ R.rightFixedPoints) (R.leftDual J) ⋯ :
            (↑R.rightFixedPoints : Type u_2)))
        (Subtype.mk (p := fun (x : Set α) ↦ x ∈ R.leftFixedPoints) J hJ)) =
    Subtype.mk (p := fun (x : Set α) ↦ x ∈ R.leftFixedPoints) J hJ
have rw₁ : J = J
Tactic: rw [Subtype.mk.injEq, hJ]
-- Lean 4 proof step from Mathlib.Order.Rel.GaloisConnection (goal)
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
I : (↑R.rightFixedPoints : Type u_2)
⊢ (fun (x : (↑R.leftFixedPoints : Type u_1)) ↦
        (match (motive := (↑R.leftFixedPoints : Type u_1) → (↑R.rightFixedPoints : Type u_2)) x with
          | ⟨J, property⟩ => Subtype.mk (p := fun (x : Set β) ↦ x ∈ R.rightFixedPoints) (R.leftDual J) ⋯ :
          (↑R.rightFixedPoints : Type u_2)))
      ((fun (x : (↑R.rightFixedPoints : Type u_2)) ↦
          (match (motive := (↑R.rightFixedPoints : Type u_2) → (↑R.leftFixedPoints : Type u_1)) x with
            | ⟨I, property⟩ => Subtype.mk (p := fun (x : Set α) ↦ x ∈ R.leftFixedPoints) (R.rightDual I) ⋯ :
            (↑R.leftFixedPoints : Type u_1)))
        I) =
    I
have obtain : ∀ (I : Set β) (hI : I ∈ R.rightFixedPoints),
  (fun (x : (↑R.leftFixedPoints : Type u_1)) ↦
        (match (motive := (↑R.leftFixedPoints : Type u_1) → (↑R.rightFixedPoints : Type u_2)) x with
          | ⟨J, property⟩ => Subtype.mk (p := fun (x : Set β) ↦ x ∈ R.rightFixedPoints) (R.leftDual J) sorry :
          (↑R.rightFixedPoints : Type u_2)))
      ((fun (x : (↑R.rightFixedPoints : Type u_2)) ↦
          (match (motive := (↑R.rightFixedPoints : Type u_2) → (↑R.leftFixedPoints : Type u_1)) x with
            | ⟨I, property⟩ => Subtype.mk (p := fun (x : Set α) ↦ x ∈ R.leftFixedPoints) (R.rightDual I) sorry :
            (↑R.leftFixedPoints : Type u_1)))
        (Subtype.mk (p := fun (x : Set β) ↦ x ∈ R.rightFixedPoints) I hI)) =
    Subtype.mk (p := fun (x : Set β) ↦ x ∈ R.rightFixedPoints) I hI
Tactic: obtain ⟨I, hI⟩ := I
Cleared hypotheses: I
-- Lean 4 proof step from Mathlib.Order.Rel.GaloisConnection (goal)
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
I : Set β
hI : I ∈ R.rightFixedPoints
⊢ (fun (x : (↑R.leftFixedPoints : Type u_1)) ↦
        (match (motive := (↑R.leftFixedPoints : Type u_1) → (↑R.rightFixedPoints : Type u_2)) x with
          | ⟨J, property⟩ => Subtype.mk (p := fun (x : Set β) ↦ x ∈ R.rightFixedPoints) (R.leftDual J) ⋯ :
          (↑R.rightFixedPoints : Type u_2)))
      ((fun (x : (↑R.rightFixedPoints : Type u_2)) ↦
          (match (motive := (↑R.rightFixedPoints : Type u_2) → (↑R.leftFixedPoints : Type u_1)) x with
            | ⟨I, property⟩ => Subtype.mk (p := fun (x : Set α) ↦ x ∈ R.leftFixedPoints) (R.rightDual I) ⋯ :
            (↑R.leftFixedPoints : Type u_1)))
        (Subtype.mk (p := fun (x : Set β) ↦ x ∈ R.rightFixedPoints) I hI)) =
    Subtype.mk (p := fun (x : Set β) ↦ x ∈ R.rightFixedPoints) I hI
have rw : R.leftDual (R.rightDual I) = I
Tactic: rw [Subtype.mk.injEq, hI]
-- Lean 4 proof step from Mathlib.Order.Rel.GaloisConnection (goal)
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
I : Set β
hI : I ∈ R.rightFixedPoints
rw : R.leftDual (R.rightDual I) = I
⊢ (fun (x : (↑R.leftFixedPoints : Type u_1)) ↦
        (match (motive := (↑R.leftFixedPoints : Type u_1) → (↑R.rightFixedPoints : Type u_2)) x with
          | ⟨J, property⟩ => Subtype.mk (p := fun (x : Set β) ↦ x ∈ R.rightFixedPoints) (R.leftDual J) ⋯ :
          (↑R.rightFixedPoints : Type u_2)))
      ((fun (x : (↑R.rightFixedPoints : Type u_2)) ↦
          (match (motive := (↑R.rightFixedPoints : Type u_2) → (↑R.leftFixedPoints : Type u_1)) x with
            | ⟨I, property⟩ => Subtype.mk (p := fun (x : Set α) ↦ x ∈ R.leftFixedPoints) (R.rightDual I) ⋯ :
            (↑R.leftFixedPoints : Type u_1)))
        (Subtype.mk (p := fun (x : Set β) ↦ x ∈ R.rightFixedPoints) I hI)) =
    Subtype.mk (p := fun (x : Set β) ↦ x ∈ R.rightFixedPoints) I hI
have rw₁ : I = I
Tactic: rw [Subtype.mk.injEq, hI]
-- Lean 4 proof step from Mathlib.Order.Rel.GaloisConnection (goal)
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
J J' : Set α
h : J' ∈ R.leftFixedPoints
h₁ : J ≤ J'
⊢ R.rightDual (R.leftDual J) ≤ J'
have rw : R.rightDual (R.leftDual J) ≤ R.rightDual (R.leftDual J')
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.Order.Rel.GaloisConnection (goal)
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
J J' : Set α
h : J' ∈ R.leftFixedPoints
h₁ : J ≤ J'
⊢ R.rightDual (R.leftDual J) ≤ R.rightDual (R.leftDual J')
have a : LE.le.{u_2} (α := (Set β)ᵒᵈ) (fun (b : β) ↦ ∀ ⦃a : α⦄, a ∈ J → (a, b) ∈ R) fun (b : β) ↦ ∀ ⦃a : α⦄, a ∈ J' → (a, b) ∈ R
Tactic: apply R.gc_leftDual_rightDual.monotone_u
-- Lean 4 proof step from Mathlib.Order.Rel.GaloisConnection (goal)
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
I I' : Set β
h : I' ∈ R.rightFixedPoints
h₁ : I ≤ I'
⊢ R.leftDual (R.rightDual I) ≤ I'
have rw : R.leftDual (R.rightDual I) ≤ R.leftDual (R.rightDual I')
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.Order.Rel.GaloisConnection (goal)
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
I I' : Set β
h : I' ∈ R.rightFixedPoints
h₁ : I ≤ I'
⊢ R.leftDual (R.rightDual I) ≤ R.leftDual (R.rightDual I')
have a : R.rightDual I' ≤ R.rightDual I
Tactic: apply R.gc_leftDual_rightDual.monotone_l
-- Lean 4 proof step from Mathlib.Order.Rel.GaloisConnection (goal)
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
I I' : Set β
h : I' ∈ R.rightFixedPoints
h₁ : I ≤ I'
⊢ R.rightDual I' ≤ R.rightDual I
have a : I' ≤ I
Tactic: apply R.gc_leftDual_rightDual.monotone_u
-- Lean 4 proof step from Mathlib.Order.RelClasses (hypothesis)
Goal:
α : Type u
β : Type v
r_1 : α → α → Prop
s : β → β → Prop
r : α → α → Prop
inst : IsStrictOrder α r
x y : α
h : r x y
e : y = x
⊢ False
have h₁ : r x x
Tactic: rw [e] at h
Cleared hypotheses: h, e
-- Lean 4 proof step from Mathlib.Order.RelClasses (goal)
Goal:
α : Type u
β : Type v
r_1 : α → α → Prop
s : β → β → Prop
r : α → α → Prop
inst : IsWellOrder α r
a b c : α
hab : r a b
hbc : r b c
⊢ r a c
have inl : ∀ (hac : r a c), r a c
Tactic: rcases trichotomous_of r a c with (hac | rfl | hca)
-- Lean 4 proof step from Mathlib.Order.RelClasses (goal)
Goal:
α : Type u
β : Type v
r_1 : α → α → Prop
s : β → β → Prop
r : α → α → Prop
inst : IsWellOrder α r
a b c : α
hab : r a b
hbc : r b c
inl : ∀ (hac : r a c), r a c
⊢ r a c
have inr : ∀ (hbc : r b a), r a a
Tactic: rcases trichotomous_of r a c with (hac | rfl | hca)
Cleared hypotheses: c, hbc
-- Lean 4 proof step from Mathlib.Order.RelClasses (goal)
Goal:
α : Type u
β : Type v
r_1 : α → α → Prop
s : β → β → Prop
r : α → α → Prop
inst : IsWellOrder α r
a b c : α
hab : r a b
hbc : r b c
inl : ∀ (hac : r a c), r a c
inr : ∀ (hbc : r b a), r a a
⊢ r a c
have inr₁ : ∀ (hca : r c a), r a c
Tactic: rcases trichotomous_of r a c with (hac | rfl | hca)
-- Lean 4 proof step from Mathlib.Order.RelClasses (goal)
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
x x_1 : α × β
a₁ : α
a₂ : β
b₁ : α
b₂ : β
hab : ¬Prod.Lex r s (a₁, a₂) (b₁, b₂)
hba : ¬Prod.Lex r s (b₁, b₂) (a₁, a₂)
⊢ (a₁, a₂) = (b₁, b₂)
have obtain : ∀ (hab : ¬Prod.Lex r s (a₁, a₂) (a₁, b₂)) (hba : ¬Prod.Lex r s (a₁, b₂) (a₁, a₂)), (a₁, a₂) = (a₁, b₂)
Tactic: obtain rfl := Std.Trichotomous.trichotomous a₁ b₁
      (mt (Prod.Lex.left a₂ b₂) hab) (mt (Prod.Lex.left b₂ a₂) hba)
Cleared hypotheses: b₁, hab, hba
-- Lean 4 proof step from Mathlib.Order.RelClasses (goal)
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
x x_1 : α × β
a₁ : α
a₂ b₂ : β
hab : ¬Prod.Lex r s (a₁, a₂) (a₁, b₂)
hba : ¬Prod.Lex r s (a₁, b₂) (a₁, a₂)
⊢ (a₁, a₂) = (a₁, b₂)
have obtain : ∀ (hab hba : ¬Prod.Lex r s (a₁, a₂) (a₁, a₂)), (a₁, a₂) = (a₁, a₂)
Tactic: obtain rfl := Std.Trichotomous.trichotomous a₂ b₂
      (mt (Prod.Lex.right a₁) hab) (mt (Prod.Lex.right a₁) hba)
Cleared hypotheses: b₂, hab, hba
-- Lean 4 proof step from Mathlib.Order.RelClasses (goal)
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst : Preorder α
inst_1 : WellFoundedLT α
inst_2 : Preorder β
inst_3 : WellFoundedLT β
⊢ WellFounded fun (x1 x2 : α × β) ↦ x1 < x2
have suffices : ∀ (a a' : α), a' ≤ a → ∀ (b : β), Acc (fun (x1 x2 : α × β) ↦ x1 < x2) (a', b)
Tactic: suffices h : ∀ a, ∀ a' ≤ a, ∀ b, Acc (· < ·) (a', b) from ⟨fun x => h x.1 x.1 le_rfl x.2⟩
-- Lean 4 proof step from Mathlib.Order.RelClasses (goal)
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst : Preorder α
inst_1 : WellFoundedLT α
inst_2 : Preorder β
inst_3 : WellFoundedLT β
a a' : α
ha : a' ≤ a
b : β
⊢ Acc (fun (x1 x2 : α × β) ↦ x1 < x2) (a', b)
have ind : ∀ (a : α) (iha : ∀ (y : α), y < a → ∀ (a' : α) (ha : a' ≤ y) (b : β), Acc (fun (x1 x2 : α × β) ↦ x1 < x2) (a', b))
  (a' : α) (ha : a' ≤ a) (b : β), Acc (fun (x1 x2 : α × β) ↦ x1 < x2) (a', b)
Tactic: induction a using WellFoundedLT.induction generalizing a' b with | ind a iha
Cleared hypotheses: a, a', ha, b
-- Lean 4 proof step from Mathlib.Order.RelClasses (goal)
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst : Preorder α
inst_1 : WellFoundedLT α
inst_2 : Preorder β
inst_3 : WellFoundedLT β
a : α
iha : ∀ (y : α), y < a → ∀ (a' : α) (ha : a' ≤ y) (b : β), Acc (fun (x1 x2 : α × β) ↦ x1 < x2) (a', b)
a' : α
ha : a' ≤ a
b : β
⊢ Acc (fun (x1 x2 : α × β) ↦ x1 < x2) (a', b)
have ind : ∀ (b : β) (ihb : ∀ (y : β), y < b → ∀ (a' : α) (ha : a' ≤ a), Acc (fun (x1 x2 : α × β) ↦ x1 < x2) (a', y)) (a' : α)
  (ha : a' ≤ a), Acc (fun (x1 x2 : α × β) ↦ x1 < x2) (a', b)
Tactic: induction b using WellFoundedLT.induction generalizing a' with | ind b ihb
Cleared hypotheses: a', ha, b
-- Lean 4 proof step from Mathlib.Order.RelClasses (goal)
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst : Preorder α
inst_1 : WellFoundedLT α
inst_2 : Preorder β
inst_3 : WellFoundedLT β
a : α
iha : ∀ (y : α), y < a → ∀ (a' : α) (ha : a' ≤ y) (b : β), Acc (fun (x1 x2 : α × β) ↦ x1 < x2) (a', b)
b : β
ihb : ∀ (y : β), y < b → ∀ (a' : α) (ha : a' ≤ a), Acc (fun (x1 x2 : α × β) ↦ x1 < x2) (a', y)
a' : α
ha : a' ≤ a
⊢ Acc (fun (x1 x2 : α × β) ↦ x1 < x2) (a', b)
have ind : ∀ (x : α × β) (hx : x < (a', b)), Acc (fun (x1 x2 : α × β) ↦ x1 < x2) x
Tactic: refine Acc.intro (a', b) fun x hx => ?_
-- Lean 4 proof step from Mathlib.Order.RelClasses (goal)
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst : Preorder α
inst_1 : WellFoundedLT α
inst_2 : Preorder β
inst_3 : WellFoundedLT β
a : α
iha : ∀ (y : α), y < a → ∀ (a' : α) (ha : a' ≤ y) (b : β), Acc (fun (x1 x2 : α × β) ↦ x1 < x2) (a', b)
b : β
ihb : ∀ (y : β), y < b → ∀ (a' : α) (ha : a' ≤ a), Acc (fun (x1 x2 : α × β) ↦ x1 < x2) (a', y)
a' : α
ha : a' ≤ a
x : α × β
hx : x < (a', b)
⊢ Acc (fun (x1 x2 : α × β) ↦ x1 < x2) x
have ind : ∀ (ha' : x.fst < (a', b).fst) (hb : x.snd ≤ (a', b).snd), Acc (fun (x1 x2 : α × β) ↦ x1 < x2) x
Tactic: obtain ⟨ha', hb⟩ | ⟨ha', hb⟩ := Prod.lt_iff.1 hx
-- Lean 4 proof step from Mathlib.Order.RelClasses (goal)
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst : Preorder α
inst_1 : WellFoundedLT α
inst_2 : Preorder β
inst_3 : WellFoundedLT β
a : α
iha : ∀ (y : α), y < a → ∀ (a' : α) (ha : a' ≤ y) (b : β), Acc (fun (x1 x2 : α × β) ↦ x1 < x2) (a', b)
b : β
ihb : ∀ (y : β), y < b → ∀ (a' : α) (ha : a' ≤ a), Acc (fun (x1 x2 : α × β) ↦ x1 < x2) (a', y)
a' : α
ha : a' ≤ a
x : α × β
hx : x < (a', b)
ind : ∀ (ha' : x.fst < (a', b).fst) (hb : x.snd ≤ (a', b).snd), Acc (fun (x1 x2 : α × β) ↦ x1 < x2) x
⊢ Acc (fun (x1 x2 : α × β) ↦ x1 < x2) x
have ind₁ : ∀ (ha' : x.fst ≤ (a', b).fst) (hb : x.snd < (a', b).snd), Acc (fun (x1 x2 : α × β) ↦ x1 < x2) x
Tactic: obtain ⟨ha', hb⟩ | ⟨ha', hb⟩ := Prod.lt_iff.1 hx
-- Lean 4 proof step from Mathlib.Order.RelClasses (goal)
Goal:
α : Type u
r : α → α → Prop
s : Set α
⊢ ¬Unbounded r s ↔ Bounded r s
have rw : ¬Bounded r s ↔ Unbounded r s
Tactic: rw [not_iff_comm, not_bounded_iff]
-- Lean 4 proof step from Mathlib.Order.RelClasses (goal)
Goal:
α : Type u
r : α → α → Prop
s : Set α
rw : ¬Bounded r s ↔ Unbounded r s
⊢ ¬Unbounded r s ↔ Bounded r s
have rw₁ : Unbounded r s ↔ Unbounded r s
Tactic: rw [not_iff_comm, not_bounded_iff]
-- Lean 4 proof step from Mathlib.Order.RelIso.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
F : Type u_5
inst : FunLike F α β
inst_1 : RelHomClass F r s
f : F
a : α
⊢ Acc s ((f : (a : α) → β) a) → Acc r a
have generalize : ∀ (b : β) (h : (f : (a : α) → β) a = b), Acc s b → Acc r a
Tactic: generalize h : f a = b
-- Lean 4 proof step from Mathlib.Order.RelIso.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
F : Type u_5
inst : FunLike F α β
inst_1 : RelHomClass F r s
f : F
a : α
b : β
h : (f : (a : α) → β) a = b
ac : Acc s b
⊢ Acc r a
have intro : ∀ (x : β) (H : ∀ (y : β), s y x → Acc s y) (IH : ∀ (y : β), s y x → ∀ (a : α) (h : (f : (a : α) → β) a = y), Acc r a)
  (a : α) (h : (f : (a : α) → β) a = x), Acc r a
Tactic: induction ac generalizing a with | intro _ H IH => ?_
Cleared hypotheses: a, h, ac
-- Lean 4 proof step from Mathlib.Order.RelIso.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
F : Type u_5
inst : FunLike F α β
inst_1 : RelHomClass F r s
f : F
b x : β
H : ∀ (y : β), s y x → Acc s y
IH : ∀ (y : β), s y x → ∀ (a : α) (h : (f : (a : α) → β) a = y), Acc r a
a : α
h : (f : (a : α) → β) a = x
⊢ Acc r a
have H₁ : ∀ (y : β), s y ((f : (a : α) → β) a) → Acc s y
Tactic: subst h
Cleared hypotheses: x, H, IH, h
-- Lean 4 proof step from Mathlib.Order.RelIso.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
F : Type u_5
inst : FunLike F α β
inst_1 : RelHomClass F r s
f : F
b x : β
H : ∀ (y : β), s y x → Acc s y
IH : ∀ (y : β), s y x → ∀ (a : α) (h : (f : (a : α) → β) a = y), Acc r a
a : α
h : (f : (a : α) → β) a = x
H₁ : ∀ (y : β), s y ((f : (a : α) → β) a) → Acc s y
⊢ Acc r a
have IH₁ : ∀ (y : β), s y ((f : (a : α) → β) a) → ∀ (a : α) (h : (f : (a : α) → β) a = y), Acc r a
Tactic: subst h
Cleared hypotheses: x, H, IH, h