awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Antisymmetrization
Goal:
α : Type u_1
a b : α
inst : Preorder α
h : AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
⊢ ¬a < b

Tactic:
h.ge.not_gt

Premises used: AntisymmRel.ge, LE.le.not_gt
-- Module: Mathlib.Order.Antisymmetrization
Goal:
α : Type u_1
a b : α
inst : Preorder α
h : AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
⊢ ¬b < a

Tactic:
h.le.not_gt

Premises used: AntisymmRel.le, LE.le.not_gt
-- Module: Mathlib.Order.Antisymmetrization
Goal:
α : Type u_1
a b : α
inst : Preorder α
⊢ a < b → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b

Tactic:
imp_not_comm.1 not_lt_of_antisymmRel

Premises used: imp_not_comm, not_lt_of_antisymmRel, Iff.mp
-- Module: Mathlib.Order.Antisymmetrization
Goal:
α : Type u_1
a b : α
inst : Preorder α
⊢ b < a → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b

Tactic:
imp_not_comm.1 not_gt_of_antisymmRel

Premises used: not_gt_of_antisymmRel, imp_not_comm, Iff.mp
-- Module: Mathlib.Order.Antisymmetrization
Goal:
α : Type u_1
a b c : α
inst : Preorder α
h : AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
⊢ a ≤ c ↔ b ≤ c

Tactic:
h.le_congr .rfl

Premises used: AntisymmRel.rfl, AntisymmRel.le_congr
-- Module: Mathlib.Order.Antisymmetrization
Goal:
α : Type u_1
a b c : α
inst : Preorder α
h : AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) b c
⊢ a ≤ b ↔ a ≤ c

Tactic:
AntisymmRel.rfl.le_congr h

Premises used: AntisymmRel.rfl, AntisymmRel.le_congr
-- Module: Mathlib.Order.Antisymmetrization
Goal:
α : Type u_1
a b c : α
inst : Preorder α
h : AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
⊢ a < c ↔ b < c

Tactic:
h.lt_congr .rfl

Premises used: AntisymmRel.rfl, AntisymmRel.lt_congr
-- Module: Mathlib.Order.Antisymmetrization
Goal:
α : Type u_1
a b c : α
inst : Preorder α
h : AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) b c
⊢ a < b ↔ a < c

Tactic:
AntisymmRel.rfl.lt_congr h

Premises used: AntisymmRel.rfl, AntisymmRel.lt_congr
-- Module: Mathlib.Order.Antisymmetrization
Goal:
α : Type u_1
a b c d : α
inst : Preorder α
h₁ : AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
h₂ : AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) c d
⊢ AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a c ↔ AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) b d

Tactic:
rel_congr h₁ h₂

Premises used: rel_congr
-- Module: Mathlib.Order.Antisymmetrization
Goal:
α : Type u_1
a b c : α
inst : Preorder α
h : AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
⊢ AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a c ↔ AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) b c

Tactic:
rel_congr_left h

Premises used: rel_congr_left
-- Module: Mathlib.Order.Antisymmetrization
Goal:
α : Type u_1
a b c : α
inst : Preorder α
h : AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) b c
⊢ AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ↔ AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a c

Tactic:
rel_congr_right h

Premises used: rel_congr_right
-- Module: Mathlib.Order.Antisymmetrization
Goal:
α : Type u_1
β : Type u_2
a b : α
inst : Preorder α
inst_1 : Preorder β
h : AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
f : α → β
hf : Monotone f
⊢ AntisymmRel (fun (x1 x2 : β) ↦ x1 ≤ x2) (f a) (f b)

Tactic:
⟨hf h.1, hf h.2⟩

Premises used: And.right, And.left, And.intro, AntisymmRel
-- Module: Mathlib.Order.Antisymmetrization
Goal:
α : Type u_1
inst : Preorder α
a : α
b_1 : Antisymmetrization α fun (x1 x2 : α) ↦ x1 ≤ x2
b : α
h :
  LT.lt (α := Antisymmetrization α fun (x1 x2 : α) ↦ x1 ≤ x2)
    (Quot.mk (⇑(AntisymmRel.setoid α fun (x1 x2 : α) ↦ x1 ≤ x2) : α → α → Prop) b)
    (toAntisymmetrization (fun (x1 x2 : α) ↦ x1 ≤ x2) a)
⊢ ∃ (a' : α),
    (fun (x1 x2 : α) ↦ x1 < x2) a' a ∧
      Eq (α := Antisymmetrization α fun (x1 x2 : α) ↦ x1 ≤ x2) (toAntisymmetrization (fun (x1 x2 : α) ↦ x1 ≤ x2) a')
        (Quot.mk (⇑(AntisymmRel.setoid α fun (x1 x2 : α) ↦ x1 ≤ x2) : α → α → Prop) b)

Tactic:
⟨b, h, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Order.Antisymmetrization
Goal:
α : Type u_1
inst : Preorder α
a : α
b_1 : Antisymmetrization α fun (x1 x2 : α) ↦ x1 ≤ x2
b : α
h :
  LT.lt (α := Antisymmetrization α fun (x1 x2 : α) ↦ x1 ≤ x2)
    (Quot.mk (⇑(AntisymmRel.setoid α fun (x1 x2 : α) ↦ x1 ≤ x2) : α → α → Prop) b)
    (toAntisymmetrization (fun (x1 x2 : α) ↦ x1 ≤ x2) a)
⊢ ∃ (a' : α),
    (fun (x1 x2 : α) ↦ x1 < x2) a' a ∧
      Eq (α := Antisymmetrization α fun (x1 x2 : α) ↦ x1 ≤ x2) (toAntisymmetrization (fun (x1 x2 : α) ↦ x1 ≤ x2) a')
        (Quot.mk (⇑(AntisymmRel.setoid α fun (x1 x2 : α) ↦ x1 ≤ x2) : α → α → Prop) b)

Tactic:
exact ⟨b, h, rfl⟩
-- Module: Mathlib.Order.Antisymmetrization
Goal:
α : Type u_1
a : α
inst : Preorder α
⊢ Acc (fun (x1 x2 : Antisymmetrization α fun (x1 x2 : α) ↦ x1 ≤ x2) ↦ x1 < x2)
      (toAntisymmetrization (fun (x1 x2 : α) ↦ x1 ≤ x2) a) ↔
    Acc (fun (x1 x2 : α) ↦ x1 < x2) a

Tactic:
acc_lift₂_iff

Premises used: acc_lift₂_iff, Antisymmetrization, toAntisymmetrization
-- Module: Mathlib.Order.Antisymmetrization
Goal:
α : Type u_1
inst : Preorder α
⊢ WellFounded.{u_1 + 1} (α := Antisymmetrization α fun (x1 x2 : α) ↦ x1 ≤ x2) LT.lt ↔
    WellFounded.{u_1 + 1} (α := α) LT.lt

Tactic:
wellFounded_lift₂_iff

Premises used: wellFounded_lift₂_iff, Antisymmetrization
-- Module: Mathlib.Order.Antisymmetrization
Goal:
α : Type u_1
inst : Preorder α
simp_rw :
  (WellFounded fun (x1 x2 : Antisymmetrization α fun (x1 x2 : α) ↦ x1 ≤ x2) ↦ x1 < x2) ↔
    WellFounded fun (x1 x2 : α) ↦ x1 < x2
⊢ WellFoundedLT.{u_1} (Antisymmetrization α fun (x1 x2 : α) ↦ x1 ≤ x2) ↔ WellFoundedLT α

Tactic:
simp_rw [isWellFounded_iff, wellFounded_antisymmetrization_iff]

Premises used: isWellFounded_iff, wellFounded_antisymmetrization_iff
-- Module: Mathlib.Order.Antisymmetrization
Goal:
α : Type u_1
inst : Preorder α
simp_rw :
  (WellFounded fun (x1 x2 : Antisymmetrization α fun (x1 x2 : α) ↦ x1 ≤ x2) ↦ x2 < x1) ↔
    WellFounded fun (x1 x2 : α) ↦ x2 < x1
⊢ WellFoundedGT.{u_1} (Antisymmetrization α fun (x1 x2 : α) ↦ x1 ≤ x2) ↔ WellFoundedGT α

Tactic:
simp_rw [isWellFounded_iff]

Premises used: isWellFounded_iff
-- Module: Mathlib.Order.Antisymmetrization
Goal:
α : Type u_1
inst : Preorder α
⊢ (WellFounded fun (x y : Quotient (AntisymmRel.setoid α fun (x1 x2 : α) ↦ x1 ≤ x2)) ↦
      x.liftOn₂' y (fun (a a_1 : α) ↦ a_1 < a) ⋯) ↔
    WellFounded fun (a a_1 : α) ↦ a_1 < a

Tactic:
wellFounded_liftOn₂'_iff

Premises used: wellFounded_liftOn₂'_iff
-- Module: Mathlib.Order.Antisymmetrization
Goal:
α : Type u_1
inst : Preorder α
convert_4 :
  ∀ (a₁ a₂ b₁ b₂ : α),
    (AntisymmRel.setoid α fun (x1 x2 : α) ↦ x1 ≤ x2 : α → α → Prop) a₁ b₁ →
      (AntisymmRel.setoid α fun (x1 x2 : α) ↦ x1 ≤ x2 : α → α → Prop) a₂ b₂ → (a₂ < a₁) = (b₂ < b₁)
⊢ (WellFounded fun (x1 x2 : Antisymmetrization α fun (x1 x2 : α) ↦ x1 ≤ x2) ↦ x2 < x1) ↔
    WellFounded fun (x1 x2 : α) ↦ x2 < x1

Tactic:
convert! wellFounded_liftOn₂'_iff with ⟨_⟩ ⟨_⟩

Premises used: wellFounded_liftOn₂'_iff
-- Module: Mathlib.Order.Antisymmetrization
Goal:
α : Type u_1
inst : Preorder α
⊢ ∀ (a₁ a₂ b₁ b₂ : α),
    (AntisymmRel.setoid α fun (x1 x2 : α) ↦ x1 ≤ x2 : α → α → Prop) a₁ b₁ →
      (AntisymmRel.setoid α fun (x1 x2 : α) ↦ x1 ≤ x2 : α → α → Prop) a₂ b₂ → (a₂ < a₁) = (b₂ < b₁)

Tactic:
fun _ _ _ _ h₁ h₂ ↦ propext
    ⟨fun h ↦ (h₂.2.trans_lt h).trans_le h₁.1, fun h ↦ (h₂.1.trans_lt h).trans_le h₁.2⟩

Premises used: And.right, And.left, LT.lt.trans_le, Iff.intro, propext, LE.le.trans_lt
-- Module: Mathlib.Order.Antisymmetrization
Goal:
α : Type u_1
inst : Preorder α
⊢ ∀ (a₁ a₂ b₁ b₂ : α),
    (AntisymmRel.setoid α fun (x1 x2 : α) ↦ x1 ≤ x2 : α → α → Prop) a₁ b₁ →
      (AntisymmRel.setoid α fun (x1 x2 : α) ↦ x1 ≤ x2 : α → α → Prop) a₂ b₂ → (a₂ < a₁) = (b₂ < b₁)

Tactic:
exact fun _ _ _ _ h₁ h₂ ↦ propext
    ⟨fun h ↦ (h₂.2.trans_lt h).trans_le h₁.1, fun h ↦ (h₂.1.trans_lt h).trans_le h₁.2⟩

Premises used: Iff.intro, propext
-- Module: Mathlib.Order.Antisymmetrization
Goal:
α : Type u_1
β : Type u_2
a b c d : α
inst : Preorder α
inst_1 : Preorder β
inst_2 : WellFoundedLT α
⊢ WellFoundedLT.{u_1} (Antisymmetrization α fun (x1 x2 : α) ↦ x1 ≤ x2)

Tactic:
wellFoundedLT_antisymmetrization_iff.mpr ‹_›

Premises used: Iff.mpr, wellFoundedLT_antisymmetrization_iff
-- Module: Mathlib.Order.Antisymmetrization
Goal:
α : Type u_1
β : Type u_2
a b c d : α
inst : Preorder α
inst_1 : Preorder β
inst_2 : WellFoundedGT α
⊢ WellFoundedGT.{u_1} (Antisymmetrization α fun (x1 x2 : α) ↦ x1 ≤ x2)

Tactic:
wellFoundedGT_antisymmetrization_iff.mpr ‹_›

Premises used: Iff.mpr, wellFoundedGT_antisymmetrization_iff
-- Module: Mathlib.Order.Antisymmetrization
Goal:
α : Type u_1
a b : α
inst : Preorder α
⊢ LE.le (α := Antisymmetrization α fun (x1 x2 : α) ↦ x1 ≤ x2) (toAntisymmetrization (fun (x1 x2 : α) ↦ x1 ≤ x2) a)
      (toAntisymmetrization (fun (x1 x2 : α) ↦ x1 ≤ x2) b) ↔
    a ≤ b

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Order.Antisymmetrization
Goal:
α : Type u_1
a b : α
inst : Preorder α
⊢ LT.lt (α := Antisymmetrization α fun (x1 x2 : α) ↦ x1 ≤ x2) (toAntisymmetrization (fun (x1 x2 : α) ↦ x1 ≤ x2) a)
      (toAntisymmetrization (fun (x1 x2 : α) ↦ x1 ≤ x2) b) ↔
    a < b

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Order.Antisymmetrization
Goal:
α : Type u_1
inst : Preorder α
a b : Antisymmetrization α fun (x1 x2 : α) ↦ x1 ≤ x2
⊢ ofAntisymmetrization (fun (x1 x2 : α) ↦ x1 ≤ x2) a ≤ ofAntisymmetrization (fun (x1 x2 : α) ↦ x1 ≤ x2) b ↔ a ≤ b

Tactic:
(Quotient.outRelEmbedding _).map_rel_iff

Premises used: Quot.out, ofAntisymmetrization, Quotient.out, RelEmbedding.map_rel_iff, Quotient.outRelEmbedding, Classical.choose
-- Module: Mathlib.Order.Antisymmetrization
Goal:
α : Type u_1
inst : Preorder α
a b : Antisymmetrization α fun (x1 x2 : α) ↦ x1 ≤ x2
⊢ ofAntisymmetrization (fun (x1 x2 : α) ↦ x1 ≤ x2) a < ofAntisymmetrization (fun (x1 x2 : α) ↦ x1 ≤ x2) b ↔ a < b

Tactic:
(Quotient.outRelEmbedding _).map_rel_iff

Premises used: Quot.out, ofAntisymmetrization, Quotient.out, RelEmbedding.map_rel_iff, Quotient.outRelEmbedding, Classical.choose
-- Module: Mathlib.Order.Antisymmetrization
Goal:
α : Type u_1
inst : Preorder α
⊢ Monotone.{u_1, u_1} (α := α) (β := Antisymmetrization α fun (x1 x2 : α) ↦ x1 ≤ x2)
    (toAntisymmetrization fun (x1 x2 : α) ↦ x1 ≤ x2)

Tactic:
fun _ _ => id

Premises used: Monotone, id
-- Module: Mathlib.Order.Antisymmetrization
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α →o β
⊢ Relator.LiftFun.{u_1 + 1, u_1 + 1, u_2 + 1, u_2 + 1} (α := α) (γ := β)
    (⇑(AntisymmRel.setoid α fun (x1 x2 : α) ↦ x1 ≤ x2) : α → α → Prop)
    (⇑(AntisymmRel.setoid β fun (x1 x2 : β) ↦ x1 ≤ x2) : β → β → Prop) (⇑f : (a : α) → β) (⇑f : (a : α) → β)

Tactic:
fun _ _ h =>
  ⟨f.mono h.1, f.mono h.2⟩

Premises used: OrderHom.mono, And.right, And.left, And.intro, AntisymmRel, Relator.LiftFun
-- Module: Mathlib.Order.Antisymmetrization
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α →o β
⊢ (⇑f.antisymmetrization :
      (a : Antisymmetrization α fun (x1 x2 : α) ↦ x1 ≤ x2) → Antisymmetrization β fun (x1 x2 : β) ↦ x1 ≤ x2) =
    Quotient.map' (⇑f : (a : α) → β) ⋯

Tactic:
rfl

Premises used: Quot.map, Quotient.map', rfl
-- Module: Mathlib.Order.Antisymmetrization
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α →o β
a : Antisymmetrization α fun (x1 x2 : α) ↦ x1 ≤ x2
⊢ (f.antisymmetrization :
        (a : Antisymmetrization α fun (x1 x2 : α) ↦ x1 ≤ x2) → Antisymmetrization β fun (x1 x2 : β) ↦ x1 ≤ x2)
      a =
    Quotient.map' (⇑f : (a : α) → β) ⋯ a

Tactic:
rfl

Premises used: Quot.map, Quotient.map', rfl
-- Module: Mathlib.Order.Antisymmetrization
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α →o β
a : α
⊢ Eq.{u_2 + 1} (α := Antisymmetrization β fun (x1 x2 : β) ↦ x1 ≤ x2)
    ((f.antisymmetrization :
          (a : Antisymmetrization α fun (x1 x2 : α) ↦ x1 ≤ x2) → Antisymmetrization β fun (x1 x2 : β) ↦ x1 ≤ x2)
        (toAntisymmetrization (fun (x1 x2 : α) ↦ x1 ≤ x2) a) :
      Antisymmetrization β fun (x1 x2 : β) ↦ x1 ≤ x2)
    (toAntisymmetrization (fun (x1 x2 : β) ↦ x1 ≤ x2) ((f : (a : α) → β) a) :
      Antisymmetrization β fun (x1 x2 : β) ↦ x1 ≤ x2)

Tactic:
@Quotient.map_mk _ _ (_root_.id _) (_root_.id _) f (liftFun_antisymmRel f) _

Premises used: Quotient.map_mk, Quotient.map, Antisymmetrization, Quot.map, Quotient.map', DFunLike.coe, liftFun_antisymmRel, toAntisymmetrization
-- Module: Mathlib.Order.Antisymmetrization
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ Eq (α := Antisymmetrization αᵒᵈ fun (x1 x2 : αᵒᵈ) ↦ x1 ≤ x2)
    ((dualAntisymmetrization α :
          (a : (Antisymmetrization α fun (x1 x2 : α) ↦ x1 ≤ x2)ᵒᵈ) → Antisymmetrization αᵒᵈ fun (x1 x2 : αᵒᵈ) ↦ x1 ≤ x2)
        ((toDual :
            (a : Antisymmetrization α fun (x1 x2 : α) ↦ x1 ≤ x2) → (Antisymmetrization α fun (x1 x2 : α) ↦ x1 ≤ x2)ᵒᵈ)
          (toAntisymmetrization (fun (x1 x2 : α) ↦ x1 ≤ x2) a)) :
      Antisymmetrization αᵒᵈ fun (x1 x2 : αᵒᵈ) ↦ x1 ≤ x2)
    (toAntisymmetrization (fun (x1 x2 : αᵒᵈ) ↦ x1 ≤ x2) ((toDual : (a : α) → αᵒᵈ) a) :
      Antisymmetrization αᵒᵈ fun (x1 x2 : αᵒᵈ) ↦ x1 ≤ x2)

Tactic:
rfl

Premises used: Quot.map, Quotient.map', OrderDual, rfl, toAntisymmetrization
-- Module: Mathlib.Order.Antisymmetrization
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ Eq (α := (Antisymmetrization α fun (x1 x2 : α) ↦ x1 ≤ x2)ᵒᵈ)
    ((symm (dualAntisymmetrization α) :
          (a : Antisymmetrization αᵒᵈ fun (x1 x2 : αᵒᵈ) ↦ x1 ≤ x2) → (Antisymmetrization α fun (x1 x2 : α) ↦ x1 ≤ x2)ᵒᵈ)
        (toAntisymmetrization (fun (x1 x2 : αᵒᵈ) ↦ x1 ≤ x2) ((toDual : (a : α) → αᵒᵈ) a)) :
      (Antisymmetrization α fun (x1 x2 : α) ↦ x1 ≤ x2)ᵒᵈ)
    ((toDual :
          (a : Antisymmetrization α fun (x1 x2 : α) ↦ x1 ≤ x2) → (Antisymmetrization α fun (x1 x2 : α) ↦ x1 ≤ x2)ᵒᵈ)
        (toAntisymmetrization (fun (x1 x2 : α) ↦ x1 ≤ x2) a) :
      (Antisymmetrization α fun (x1 x2 : α) ↦ x1 ≤ x2)ᵒᵈ)

Tactic:
rfl

Premises used: Quot.map, Quotient.map', OrderDual, rfl, toAntisymmetrization
-- Module: Mathlib.Order.Antisymmetrization
Goal:
α : Type u_1
a b : α
r : α → α → Prop
h : AntisymmRel r a b
⊢ SymmGen r a b

Tactic:
Or.inl h.1

Premises used: And.left, Or.inl, Relation.SymmGen
-- Module: Mathlib.Order.Antisymmetrization
Goal:
α : Type u_1
a b : α
inst : Preorder α
h : a < b
⊢ SymmGen (fun (x1 x2 : α) ↦ x1 ≤ x2) a b

Tactic:
h.le.symmGen

Premises used: LT.lt.le, LE.le.symmGen
-- Module: Mathlib.Order.Antisymmetrization
Goal:
α : Type u_1
a b : α
inst : Preorder α
h : b < a
⊢ SymmGen (fun (x1 x2 : α) ↦ x1 ≤ x2) a b

Tactic:
h.le.symmGen_symm

Premises used: LT.lt.le, LE.le.symmGen_symm
-- Module: Mathlib.Order.Antisymmetrization
Goal:
α : Type u_1
a b c : α
inst : Preorder α
h₁ : SymmGen (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
h₂ : AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) b c
inl : ∀ (h : a ≤ b), SymmGen (fun (x1 x2 : α) ↦ x1 ≤ x2) a c
inr : ∀ (h : b ≤ a), SymmGen (fun (x1 x2 : α) ↦ x1 ≤ x2) a c
⊢ SymmGen (fun (x1 x2 : α) ↦ x1 ≤ x2) a c

Tactic:
obtain (h | h) := h₁
-- Module: Mathlib.Order.Antisymmetrization
Goal:
α : Type u_1
a b c : α
inst : Preorder α
h₂ : AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) b c
h : a ≤ b
⊢ SymmGen (fun (x1 x2 : α) ↦ x1 ≤ x2) a c

Tactic:
(h.trans h₂.le).symmGen

Premises used: AntisymmRel.le, LE.le.trans, LE.le.symmGen
-- Module: Mathlib.Order.Antisymmetrization
Goal:
α : Type u_1
a b c : α
inst : Preorder α
h₂ : AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) b c
h : a ≤ b
⊢ SymmGen (fun (x1 x2 : α) ↦ x1 ≤ x2) a c

Tactic:
exact (h.trans h₂.le).symmGen

Premises used: AntisymmRel.le, LE.le.trans, LE.le.symmGen
-- Module: Mathlib.Order.Antisymmetrization
Goal:
α : Type u_1
a b c : α
inst : Preorder α
h₂ : AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) b c
h : b ≤ a
⊢ SymmGen (fun (x1 x2 : α) ↦ x1 ≤ x2) a c

Tactic:
(h₂.ge.trans h).symmGen_symm

Premises used: AntisymmRel.ge, LE.le.trans, LE.le.symmGen_symm
-- Module: Mathlib.Order.Antisymmetrization
Goal:
α : Type u_1
a b c : α
inst : Preorder α
h₂ : AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) b c
h : b ≤ a
⊢ SymmGen (fun (x1 x2 : α) ↦ x1 ≤ x2) a c

Tactic:
exact (h₂.ge.trans h).symmGen_symm

Premises used: AntisymmRel.ge, LE.le.trans, LE.le.symmGen_symm
-- Module: Mathlib.Order.Antisymmetrization
Goal:
α : Type u_1
a b c : α
inst : Preorder α
h₁ : AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
h₂ : SymmGen (fun (x1 x2 : α) ↦ x1 ≤ x2) b c
⊢ SymmGen (fun (x1 x2 : α) ↦ x1 ≤ x2) a c

Tactic:
(h₂.symm.trans_antisymmRel h₁.symm).symm

Premises used: Relation.SymmGen.symm, Relation.SymmGen.trans_antisymmRel, AntisymmRel.symm
-- Module: Mathlib.Order.Antisymmetrization
Goal:
α : Type u_1
a b c : α
inst : Preorder α
h : AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
⊢ SymmGen (fun (x1 x2 : α) ↦ x1 ≤ x2) a c ↔ SymmGen (fun (x1 x2 : α) ↦ x1 ≤ x2) b c

Tactic:
h.symmGen_congr .rfl

Premises used: AntisymmRel.rfl, AntisymmRel.symmGen_congr
-- Module: Mathlib.Order.Antisymmetrization
Goal:
α : Type u_1
a b c : α
inst : Preorder α
h : AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) b c
⊢ SymmGen (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ↔ SymmGen (fun (x1 x2 : α) ↦ x1 ≤ x2) a c

Tactic:
AntisymmRel.rfl.symmGen_congr h

Premises used: AntisymmRel.rfl, AntisymmRel.symmGen_congr
-- Module: Mathlib.Order.Antisymmetrization
Goal:
α : Type u_1
β : Type u_2
a b c d : α
inst : Preorder α
inst_1 : Preorder β
x : Antisymmetrization (α × β) fun (x1 x2 : α × β) ↦ x1 ≤ x2
a_1 : α × β
⊢ Eq (α := Antisymmetrization (α × β) fun (x1 x2 : α × β) ↦ x1 ≤ x2)
    (uncurry (α := Antisymmetrization α fun (x1 x2 : α) ↦ x1 ≤ x2) (β := Antisymmetrization β fun (x1 x2 : β) ↦ x1 ≤ x2)
      (Quotient.lift₂ (fun (a : α) (b : β) ↦ ⟦(a, b)⟧) ⋯)
      (Quotient.lift (s := AntisymmRel.setoid (α × β) fun (x1 x2 : α × β) ↦ x1 ≤ x2)
        (fun (ab : α × β) ↦ (⟦ab.1⟧, ⟦ab.2⟧)) ⋯
        (Quot.mk (⇑(AntisymmRel.setoid (α × β) fun (x1 x2 : α × β) ↦ x1 ≤ x2) : α × β → α × β → Prop) a_1)))
    (Quot.mk (⇑(AntisymmRel.setoid (α × β) fun (x1 x2 : α × β) ↦ x1 ≤ x2) : α × β → α × β → Prop) a_1)

Tactic:
rfl
-- Module: Mathlib.Order.Antisymmetrization
Goal:
α : Type u_1
β : Type u_2
a b c d : α
inst : Preorder α
inst_1 : Preorder β
fst : Antisymmetrization α fun (x1 x2 : α) ↦ x1 ≤ x2
snd : Antisymmetrization β fun (x1 x2 : β) ↦ x1 ≤ x2
a_1 : α
a_2 : β
⊢ Eq (α :=
    Prod.{u_1, u_2} (Antisymmetrization α fun (x1 x2 : α) ↦ x1 ≤ x2) (Antisymmetrization β fun (x1 x2 : β) ↦ x1 ≤ x2))
    (Quotient.lift (s := AntisymmRel.setoid (α × β) fun (x1 x2 : α × β) ↦ x1 ≤ x2) (fun (ab : α × β) ↦ (⟦ab.1⟧, ⟦ab.2⟧))
      ⋯
      (uncurry (α := Antisymmetrization α fun (x1 x2 : α) ↦ x1 ≤ x2) (β :=
        Antisymmetrization β fun (x1 x2 : β) ↦ x1 ≤ x2) (Quotient.lift₂ (fun (a : α) (b : β) ↦ ⟦(a, b)⟧) ⋯)
        (Quot.mk (⇑(AntisymmRel.setoid α fun (x1 x2 : α) ↦ x1 ≤ x2) : α → α → Prop) a_1,
          Quot.mk (⇑(AntisymmRel.setoid β fun (x1 x2 : β) ↦ x1 ≤ x2) : β → β → Prop) a_2)))
    (Quot.mk (⇑(AntisymmRel.setoid α fun (x1 x2 : α) ↦ x1 ≤ x2) : α → α → Prop) a_1,
      Quot.mk (⇑(AntisymmRel.setoid β fun (x1 x2 : β) ↦ x1 ≤ x2) : β → β → Prop) a_2)

Tactic:
rfl
-- Module: Mathlib.Order.Antisymmetrization
Goal:
α : Type u_1
β : Type u_2
a b c d : α
inst : Preorder α
inst_1 : Preorder β
a_1 : Antisymmetrization (α × β) fun (x1 x2 : α × β) ↦ x1 ≤ x2
a_2 : α × β
b_1 : Antisymmetrization (α × β) fun (x1 x2 : α × β) ↦ x1 ≤ x2
a_3 : α × β
⊢ LE.le (α :=
      Prod.{u_1, u_2} (Antisymmetrization α fun (x1 x2 : α) ↦ x1 ≤ x2) (Antisymmetrization β fun (x1 x2 : β) ↦ x1 ≤ x2))
      (({ toFun := Quotient.lift (fun (ab : α × β) ↦ (⟦ab.1⟧, ⟦ab.2⟧)) ⋯,
              invFun := uncurry (Quotient.lift₂ (fun (a : α) (b : β) ↦ ⟦(a, b)⟧) ⋯), left_inv := ⋯, right_inv := ⋯ } :
            (a : Antisymmetrization (α × β) fun (x1 x2 : α × β) ↦ x1 ≤ x2) →
              (Antisymmetrization α fun (x1 x2 : α) ↦ x1 ≤ x2) × Antisymmetrization β fun (x1 x2 : β) ↦ x1 ≤ x2)
          (Quot.mk (⇑(AntisymmRel.setoid (α × β) fun (x1 x2 : α × β) ↦ x1 ≤ x2) : α × β → α × β → Prop) a_2) :
        Prod.{u_1, u_2} (Antisymmetrization α fun (x1 x2 : α) ↦ x1 ≤ x2)
          (Antisymmetrization β fun (x1 x2 : β) ↦ x1 ≤ x2))
      (({ toFun := Quotient.lift (fun (ab : α × β) ↦ (⟦ab.1⟧, ⟦ab.2⟧)) ⋯,
              invFun := uncurry (Quotient.lift₂ (fun (a : α) (b : β) ↦ ⟦(a, b)⟧) ⋯), left_inv := ⋯, right_inv := ⋯ } :
            (a : Antisymmetrization (α × β) fun (x1 x2 : α × β) ↦ x1 ≤ x2) →
              (Antisymmetrization α fun (x1 x2 : α) ↦ x1 ≤ x2) × Antisymmetrization β fun (x1 x2 : β) ↦ x1 ≤ x2)
          (Quot.mk (⇑(AntisymmRel.setoid (α × β) fun (x1 x2 : α × β) ↦ x1 ≤ x2) : α × β → α × β → Prop) a_3) :
        Prod.{u_1, u_2} (Antisymmetrization α fun (x1 x2 : α) ↦ x1 ≤ x2)
          (Antisymmetrization β fun (x1 x2 : β) ↦ x1 ≤ x2)) ↔
    LE.le (α := Antisymmetrization (α × β) fun (x1 x2 : α × β) ↦ x1 ≤ x2)
      (Quot.mk (⇑(AntisymmRel.setoid (α × β) fun (x1 x2 : α × β) ↦ x1 ≤ x2) : α × β → α × β → Prop) a_2)
      (Quot.mk (⇑(AntisymmRel.setoid (α × β) fun (x1 x2 : α × β) ↦ x1 ≤ x2) : α × β → α × β → Prop) a_3)

Tactic:
rfl
-- Module: Mathlib.Order.Antisymmetrization
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
ab : α × β
⊢ (prodEquiv α β :
        (a : Antisymmetrization (α × β) fun (x1 x2 : α × β) ↦ x1 ≤ x2) →
          (Antisymmetrization α fun (x1 x2 : α) ↦ x1 ≤ x2) × Antisymmetrization β fun (x1 x2 : β) ↦ x1 ≤ x2)
      ⟦ab⟧ =
    (⟦ab.1⟧, ⟦ab.2⟧)

Tactic:
rfl

Premises used: Antisymmetrization, rfl
-- Module: Mathlib.Order.Antisymmetrization
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
a : α
b : β
⊢ Eq (α := Antisymmetrization (α × β) fun (x1 x2 : α × β) ↦ x1 ≤ x2)
    ((OrderIso.symm (prodEquiv α β) :
          (a : (Antisymmetrization α fun (x1 x2 : α) ↦ x1 ≤ x2) × Antisymmetrization β fun (x1 x2 : β) ↦ x1 ≤ x2) →
            Antisymmetrization (α × β) fun (x1 x2 : α × β) ↦ x1 ≤ x2)
        (⟦a⟧, ⟦b⟧) :
      Antisymmetrization (α × β) fun (x1 x2 : α × β) ↦ x1 ≤ x2)
    (⟦(a, b)⟧ : Quotient (α := α × β) (AntisymmRel.setoid (α × β) fun (x1 x2 : α × β) ↦ x1 ≤ x2))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Atoms.Finite
Goal:
α : Type u_1
β : Type u_2
inst : LE α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
⊢ Finite α

Tactic:
infer_instance
-- Module: Mathlib.Order.Atoms.Finite
Goal:
α : Type u_1
β : Type u_2
inst : LE α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
⊢ Finite α

Tactic:
classical infer_instance
-- Module: Mathlib.Order.Atoms.Finite
Goal:
α : Type u_1
inst : LE α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
inst_3 : DecidableEq α
h : ∀ (a : α), Membership.mem (γ := Finset α) Finset.univ a ↔ Membership.mem (γ := Finset α) {⊤, ⊥} a
⊢ Eq (α := Finset α) Finset.univ {⊤, ⊥}

Tactic:
ext
-- Module: Mathlib.Order.Atoms.Finite
Goal:
α : Type u_1
inst : LE α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
inst_3 : DecidableEq α
a : α
⊢ Membership.mem (γ := Finset α) Finset.univ a ↔ Membership.mem (γ := Finset α) {⊤, ⊥} a

Tactic:
simpa using (eq_bot_or_eq_top _).symm

Premises used: Or.symm, IsSimpleOrder.eq_bot_or_eq_top
-- Module: Mathlib.Order.Atoms.Finite
Goal:
α : Type u_1
inst : LE α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
inst_3 : DecidableEq α
⊢ Fintype.card α = 2

Tactic:
(Fintype.ofEquiv_card _).trans Fintype.card_bool

Premises used: Fintype.ofEquiv_card, Eq.trans, Fintype.card_bool
-- Module: Mathlib.Order.Atoms.Finite
Goal:
α : Type u_1
β : Type u_2
a : Bool
rw : Membership.mem (γ := Finset Bool) Finset.univ a
⊢ a = ⊥ ∨ a = ⊤

Tactic:
rw [← Finset.mem_singleton, Or.comm, ← Finset.mem_insert, top_eq_true, bot_eq_false, ←
      Fintype.univ_bool]

Premises used: Finset.mem_singleton, Or.comm, Finset.mem_insert, Fintype.univ_bool, bot_eq_false, top_eq_true
-- Module: Mathlib.Order.Atoms.Finite
Goal:
α : Type u_1
β : Type u_2
a : Bool
⊢ Membership.mem (γ := Finset Bool) Finset.univ a

Tactic:
apply Finset.mem_univ

Premises used: Finset.mem_univ
-- Module: Mathlib.Order.Atoms.Finite
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : OrderTop α
inst_2 : Finite α
⊢ IsCoatomic α

Tactic:
IsStronglyCoatomic.toIsCoatomic α

Premises used: IsStronglyCoatomic.toIsCoatomic
-- Module: Mathlib.Order.Atoms.Finite
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : OrderBot α
inst_2 : Finite α
⊢ IsAtomic α

Tactic:
isCoatomic_dual_iff_isAtomic.mp Finite.to_isCoatomic

Premises used: isCoatomic_dual_iff_isAtomic, Finite.to_isCoatomic, Iff.mp