awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Quotient
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
h : ∀ (x : α) (h₁ : ⟦x⟧ ≤ y) (h₂ : y ≤ ⟦x⟧), ⟦x⟧ = y
⊢ x = y

Tactic:
induction x using Quotient.inductionOn with | h x
-- Module: Mathlib.Order.Quotient
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⟧
h : ∀ (y : α) (h₁ : ⟦x⟧ ≤ ⟦y⟧) (h₂ : ⟦y⟧ ≤ ⟦x⟧), ⟦x⟧ = ⟦y⟧
⊢ ⟦x⟧ = y

Tactic:
induction y using Quotient.inductionOn with | h y
-- Module: Mathlib.Order.Quotient
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 ∨ x ≈ y

Tactic:
rw [mk_le_mk] at h₁ h₂

Premises used: Quotient.mk_le_mk
-- Module: Mathlib.Order.Quotient
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
⊢ y ≤ x ∨ y ≈ x

Tactic:
rw [mk_le_mk] at h₁ h₂

Premises used: Quotient.mk_le_mk
-- Module: Mathlib.Order.Quotient
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⟧

Tactic:
Quotient.sound h

Premises used: Quotient.sound
-- Module: Mathlib.Order.Quotient
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⟧

Tactic:
exact Quotient.sound h

Premises used: Quotient.sound
-- Module: Mathlib.Order.Quotient
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⟧

Tactic:
(Quotient.sound h).symm

Premises used: Quotient.sound, Eq.symm
-- Module: Mathlib.Order.Quotient
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⟧

Tactic:
exact (Quotient.sound h).symm

Premises used: Quotient.sound, Eq.symm
-- Module: Mathlib.Order.Quotient
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⟧

Tactic:
congrArg _ (h₁.antisymm h₂)

Premises used: congrArg, LE.le.antisymm
-- Module: Mathlib.Order.Quotient
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⟧

Tactic:
exact congrArg _ (h₁.antisymm h₂)

Premises used: congrArg, LE.le.antisymm
-- Module: Mathlib.Order.Quotient
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⟧
h₃ : ∀ (h₂ : y ≤ x), ⟦x⟧ = ⟦y⟧
⊢ ⟦x⟧ = ⟦y⟧

Tactic:
cases h₂ with
      | inr h => exact (Quotient.sound h).symm
      | inl h₂ => exact congrArg _ (h₁.antisymm h₂)
-- Module: Mathlib.Order.Quotient
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⟧
h₃ : ∀ (h₁ : x ≤ y), ⟦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₂)
-- Module: Mathlib.Order.Quotient
Goal:
α : Type u_1
s : Setoid α
inst : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
x y : α
contrapose! : ⟦y⟧ ≤ ⟦x⟧ ↔ y ≤ x ∨ x ≈ y
⊢ ⟦x⟧ < ⟦y⟧ ↔ x < y ∧ ¬x ≈ y

Tactic:
contrapose! +distrib
-- Module: Mathlib.Order.Quotient
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
rw₁ rw₂ : y ≤ x ∨ x ≈ y ↔ y ≤ x ∨ x ≈ y
⊢ ⟦y⟧ ≤ ⟦x⟧ ↔ y ≤ x ∨ x ≈ y

Tactic:
rw [mk_le_mk, comm_of (· ≈ ·)]

Premises used: comm_of, HasEquiv.Equiv, Quotient.mk_le_mk
-- Module: Mathlib.Order.Quotient
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)
contrapose!₂ : ⟦y⟧ ≤ ⟦x⟧ ↔ y ≤ x ∨ x ≈ y
⊢ ⟦x⟧ < ⟦y⟧ ↔ x < y ∧ ¬x ≈ y

Tactic:
classical
  contrapose! +distrib
  rw [mk_le_mk, comm_of (· ≈ ·)]

Premises used: comm_of, HasEquiv.Equiv, Quotient.mk_le_mk
-- Module: Mathlib.Order.Quotient
Goal:
α : Type u_1
s : Setoid α
inst : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
x y : α
h : ⟦x⟧ < ⟦y⟧
⊢ x < y

Tactic:
(mk_lt_mk.1 h).1

Premises used: Quotient.mk_lt_mk, And.left, Iff.mp
-- Module: Mathlib.Order.Radical
Goal:
α : Type u_1
inst : CompleteLattice α
a : α
h : IsCoatom a
⊢ radical α ≤ a

Tactic:
biInf_le _ h

Premises used: Order.radical, biInf_le
-- Module: Mathlib.Order.Radical
Goal:
α : Type u_1
inst : CompleteLattice α
β : Type u_2
inst_1 : CompleteLattice β
f : α ≃o β
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 : β)
⊢ (f : (a : α) → β) (Order.radical α) = Order.radical β

Tactic:
unfold Order.radical

Premises used: Order.radical
-- Module: Mathlib.Order.Radical
Goal:
α : Type u_1
inst : CompleteLattice α
β : Type u_2
inst_1 : CompleteLattice β
f : α ≃o β
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)
⊢ 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:
simp only [OrderIso.map_iInf]

Premises used: OrderIso.map_iInf
-- Module: Mathlib.Order.Radical
Goal:
α : Type u_1
inst : CompleteLattice α
β : Type u_2
inst_1 : CompleteLattice β
f : α ≃o β
e : α ≃ β
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)
⊢ 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:
fapply Equiv.iInf_congr

Premises used: Equiv.iInf_congr
-- Module: Mathlib.Order.Radical
Goal:
α : Type u_1
inst : CompleteLattice α
β : Type u_2
inst_1 : CompleteLattice β
f : α ≃o β
⊢ α ≃ β

Tactic:
exact f.toEquiv

Premises used: RelIso.toEquiv
-- Module: Mathlib.Order.Radical
Goal:
α : Type u_1
inst : CompleteLattice α
β : Type u_2
inst_1 : CompleteLattice β
f : α ≃o β
⊢ ∀ (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:
simp
-- Module: Mathlib.Order.Radical
Goal:
α : Type u_1
inst : CompleteLattice α
inst_1 : IsCoatomic α
a : α
h : a ⊔ radical α = ⊤
inl : ∀ (h : ⊤ ⊔ radical α = ⊤), Eq.{u_1 + 1} (α := α) ⊤ ⊤
inr : ∀ (w : ∃ (a_1 : α), IsCoatom a_1 ∧ a ≤ a_1), a = ⊤
⊢ a = ⊤

Tactic:
obtain (rfl | w) := eq_top_or_exists_le_coatom a

Premises used: IsCoatomic.eq_top_or_exists_le_coatom, rfl
-- Module: Mathlib.Order.Radical
Goal:
α : Type u_1
inst : CompleteLattice α
inst_1 : IsCoatomic α
h : ⊤ ⊔ radical α = ⊤
⊢ Eq.{u_1 + 1} (α := α) ⊤ ⊤

Tactic:
rfl
-- Module: Mathlib.Order.Radical
Goal:
α : Type u_1
inst : CompleteLattice α
inst_1 : IsCoatomic α
a : α
h : a ⊔ radical α = ⊤
w : ∃ (a_1 : α), IsCoatom a_1 ∧ a ≤ a_1
inr : ∀ (m : α) (c : IsCoatom m) (le : a ≤ m), a = ⊤
⊢ a = ⊤

Tactic:
obtain ⟨m, c, le⟩ := w
-- Module: Mathlib.Order.Radical
Goal:
α : Type u_1
inst : CompleteLattice α
inst_1 : IsCoatomic α
a : α
h : a ⊔ radical α = ⊤
m : α
c : IsCoatom m
le : a ≤ m
⊢ a ⊔ radical α ≤ m

Tactic:
have q : a ⊔ radical α ≤ m := sup_le le (radical_le_coatom c)
-- Module: Mathlib.Order.Radical
Goal:
α : Type u_1
inst : CompleteLattice α
inst_1 : IsCoatomic α
a : α
h : a ⊔ radical α = ⊤
m : α
c : IsCoatom m
le : a ≤ m
q : a ⊔ radical α ≤ m
⊢ m = ⊤

Tactic:
rw [h, top_le_iff] at q

Premises used: top_le_iff
-- Module: Mathlib.Order.Radical
Goal:
α : Type u_1
inst : CompleteLattice α
inst_1 : IsCoatomic α
a : α
h : a ⊔ radical α = ⊤
m : α
c : IsCoatom m
le : a ≤ m
q : m = ⊤
⊢ a = ⊤

Tactic:
simpa using c.1 q

Premises used: And.left
-- Module: Mathlib.Order.Rel.GaloisConnection
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
x : Set α
x_1 : (Set β)ᵒᵈ
h : ((⇑toDual : (a : Set β) → (Set β)ᵒᵈ) ∘ R.leftDual) x ≤ x_1
x_2 : α
ha : x_2 ∈ x
x_3 : β
hb : Membership.mem (γ := Set β) ((ofDual : (a : (Set β)ᵒᵈ) → Set β) x_1 : Set β) x_3
⊢ x_3 ∈ x_1

Tactic:
simpa
-- Module: Mathlib.Order.Rel.GaloisConnection
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
x : Set α
x_1 : (Set β)ᵒᵈ
h : x ≤ (R.rightDual ∘ (⇑ofDual : (a : (Set β)ᵒᵈ) → Set β)) x_1
x_2 : β
hb : x_2 ∈ x_1
x_3 : α
ha : x_3 ∈ x
⊢ x_3 ∈ x

Tactic:
simpa
-- Module: Mathlib.Order.Rel.GaloisConnection
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
J : Set α
a : R.leftDual (R.rightDual (R.leftDual J)) ≤ R.leftDual J
a₁ : R.leftDual J ≤ R.leftDual (R.rightDual (R.leftDual J))
⊢ R.leftDual J ∈ R.rightFixedPoints

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Order.Rel.GaloisConnection
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
J : Set α
a : J ≤ R.rightDual (R.leftDual J)
⊢ R.leftDual (R.rightDual (R.leftDual J)) ≤ R.leftDual J

Tactic:
apply R.gc_leftDual_rightDual.monotone_l

Premises used: SetRel.gc_leftDual_rightDual, GaloisConnection.monotone_l
-- Module: Mathlib.Order.Rel.GaloisConnection
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
J : Set α
⊢ J ≤ R.rightDual (R.leftDual J)

Tactic:
R.gc_leftDual_rightDual.le_u_l J

Premises used: Set.Mem, setOf, GaloisConnection.le_u_l, SetRel.leftDual, SetRel.rightDual, SetRel.gc_leftDual_rightDual
-- Module: Mathlib.Order.Rel.GaloisConnection
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
J : Set α
⊢ J ≤ R.rightDual (R.leftDual J)

Tactic:
exact R.gc_leftDual_rightDual.le_u_l J

Premises used: GaloisConnection.le_u_l, SetRel.gc_leftDual_rightDual
-- Module: Mathlib.Order.Rel.GaloisConnection
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
J : Set α
⊢ R.leftDual J ≤ R.leftDual (R.rightDual (R.leftDual J))

Tactic:
R.gc_leftDual_rightDual.l_u_le (R.leftDual J)

Premises used: Set.Mem, setOf, SetRel.leftDual, SetRel.rightDual, SetRel.gc_leftDual_rightDual, GaloisConnection.l_u_le
-- Module: Mathlib.Order.Rel.GaloisConnection
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
J : Set α
⊢ R.leftDual J ≤ R.leftDual (R.rightDual (R.leftDual J))

Tactic:
exact R.gc_leftDual_rightDual.l_u_le (R.leftDual J)

Premises used: SetRel.leftDual, SetRel.gc_leftDual_rightDual, GaloisConnection.l_u_le
-- Module: Mathlib.Order.Rel.GaloisConnection
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
I : Set β
a : R.rightDual (R.leftDual (R.rightDual I)) ≤ R.rightDual I
a₁ : R.rightDual I ≤ R.rightDual (R.leftDual (R.rightDual I))
⊢ R.rightDual I ∈ R.leftFixedPoints

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Order.Rel.GaloisConnection
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
I : Set β
a : (fun (b : β) ↦ ∀ ⦃a : α⦄, a ∈ R.rightDual I → (a, b) ∈ R) ≤ I
⊢ R.rightDual (R.leftDual (R.rightDual I)) ≤ R.rightDual I

Tactic:
apply R.gc_leftDual_rightDual.monotone_u

Premises used: GaloisConnection.monotone_u, SetRel.gc_leftDual_rightDual
-- Module: Mathlib.Order.Rel.GaloisConnection
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
I : Set β
⊢ (fun (b : β) ↦ ∀ ⦃a : α⦄, a ∈ R.rightDual I → (a, b) ∈ R) ≤ I

Tactic:
R.gc_leftDual_rightDual.l_u_le I

Premises used: Set.Mem, setOf, SetRel.leftDual, SetRel.rightDual, SetRel.gc_leftDual_rightDual, GaloisConnection.l_u_le
-- Module: Mathlib.Order.Rel.GaloisConnection
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
I : Set β
⊢ (fun (b : β) ↦ ∀ ⦃a : α⦄, a ∈ R.rightDual I → (a, b) ∈ R) ≤ I

Tactic:
exact R.gc_leftDual_rightDual.l_u_le I

Premises used: SetRel.gc_leftDual_rightDual, GaloisConnection.l_u_le
-- Module: Mathlib.Order.Rel.GaloisConnection
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
I : Set β
⊢ R.rightDual I ≤ R.rightDual (R.leftDual (R.rightDual I))

Tactic:
R.gc_leftDual_rightDual.le_u_l (R.rightDual I)

Premises used: Set.Mem, setOf, GaloisConnection.le_u_l, SetRel.leftDual, SetRel.rightDual, SetRel.gc_leftDual_rightDual
-- Module: Mathlib.Order.Rel.GaloisConnection
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
I : Set β
⊢ R.rightDual I ≤ R.rightDual (R.leftDual (R.rightDual I))

Tactic:
exact R.gc_leftDual_rightDual.le_u_l (R.rightDual I)

Premises used: GaloisConnection.le_u_l, SetRel.rightDual, SetRel.gc_leftDual_rightDual
-- Module: Mathlib.Order.Rel.GaloisConnection
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
J : (↑R.leftFixedPoints : Type u_1)
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) ⋯ :
            (↑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
⊢ (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

Tactic:
obtain ⟨J, hJ⟩ := J
-- Module: Mathlib.Order.Rel.GaloisConnection
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
J : Set α
hJ : J ∈ R.leftFixedPoints
rw : R.rightDual (R.leftDual J) = J
rw₁ rw₂ : 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

Tactic:
rw [Subtype.mk.injEq, hJ]

Premises used: Subtype.mk.injEq
-- Module: Mathlib.Order.Rel.GaloisConnection
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
I : (↑R.rightFixedPoints : Type u_2)
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) ⋯ :
            (↑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
⊢ (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

Tactic:
obtain ⟨I, hI⟩ := I
-- Module: Mathlib.Order.Rel.GaloisConnection
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
I : Set β
hI : I ∈ R.rightFixedPoints
rw : R.leftDual (R.rightDual I) = I
rw₁ rw₂ : 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

Tactic:
rw [Subtype.mk.injEq, hI]

Premises used: Subtype.mk.injEq
-- Module: Mathlib.Order.Rel.GaloisConnection
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
J J' : Set α
h : J' ∈ R.leftFixedPoints
h₁ : J ≤ J'
rw : R.rightDual (R.leftDual J) ≤ R.rightDual (R.leftDual J')
⊢ R.rightDual (R.leftDual J) ≤ J'

Tactic:
rw [← h]
-- Module: Mathlib.Order.Rel.GaloisConnection
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
J J' : Set α
h : J' ∈ R.leftFixedPoints
h₁ : J ≤ J'
a :
  LE.le.{u_2} (α := (Set β)ᵒᵈ) (fun (b : β) ↦ ∀ ⦃a : α⦄, a ∈ J → (a, b) ∈ R) fun (b : β) ↦
    ∀ ⦃a : α⦄, a ∈ J' → (a, b) ∈ R
⊢ R.rightDual (R.leftDual J) ≤ R.rightDual (R.leftDual J')

Tactic:
apply R.gc_leftDual_rightDual.monotone_u

Premises used: GaloisConnection.monotone_u, SetRel.gc_leftDual_rightDual
-- Module: Mathlib.Order.Rel.GaloisConnection
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
J J' : Set α
h : J' ∈ R.leftFixedPoints
h₁ : J ≤ J'
a : J ≤ J'
⊢ 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_l

Premises used: SetRel.gc_leftDual_rightDual, GaloisConnection.monotone_l
-- Module: Mathlib.Order.Rel.GaloisConnection
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
J J' : Set α
h : J' ∈ R.leftFixedPoints
h₁ : J ≤ J'
⊢ J ≤ J'

Tactic:
h₁
-- Module: Mathlib.Order.Rel.GaloisConnection
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
J J' : Set α
h : J' ∈ R.leftFixedPoints
h₁ : J ≤ J'
⊢ J ≤ J'

Tactic:
exact h₁
-- Module: Mathlib.Order.Rel.GaloisConnection
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
I I' : Set β
h : I' ∈ R.rightFixedPoints
h₁ : I ≤ I'
rw : R.leftDual (R.rightDual I) ≤ R.leftDual (R.rightDual I')
⊢ R.leftDual (R.rightDual I) ≤ I'

Tactic:
rw [← h]
-- Module: Mathlib.Order.Rel.GaloisConnection
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
I I' : Set β
h : I' ∈ R.rightFixedPoints
h₁ : I ≤ I'
a : R.rightDual I' ≤ R.rightDual I
⊢ R.leftDual (R.rightDual I) ≤ R.leftDual (R.rightDual I')

Tactic:
apply R.gc_leftDual_rightDual.monotone_l

Premises used: SetRel.gc_leftDual_rightDual, GaloisConnection.monotone_l
-- Module: Mathlib.Order.Rel.GaloisConnection
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
I I' : Set β
h : I' ∈ R.rightFixedPoints
h₁ : I ≤ I'
a : I' ≤ I
⊢ R.rightDual I' ≤ R.rightDual I

Tactic:
apply R.gc_leftDual_rightDual.monotone_u

Premises used: GaloisConnection.monotone_u, SetRel.gc_leftDual_rightDual
-- Module: Mathlib.Order.Rel.GaloisConnection
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
I I' : Set β
h : I' ∈ R.rightFixedPoints
h₁ : I ≤ I'
⊢ I' ≤ I

Tactic:
h₁
-- Module: Mathlib.Order.Rel.GaloisConnection
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
I I' : Set β
h : I' ∈ R.rightFixedPoints
h₁ : I ≤ I'
⊢ I' ≤ I

Tactic:
exact h₁
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
r : α → α → Prop
inst : Refl r
⊢ Refl (Function.swap (φ := fun (a a_1 : α) ↦ Prop) r)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
r : α → α → Prop
inst : Irrefl r
⊢ Irrefl (Function.swap (φ := fun (a a_1 : α) ↦ Prop) r)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
r : α → α → Prop
inst : IsTrans α r
⊢ IsTrans α (Function.swap (φ := fun (a a_1 : α) ↦ Prop) r)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
r : α → α → Prop
inst : Antisymm r
⊢ Antisymm (Function.swap (φ := fun (a a_1 : α) ↦ Prop) r)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
r : α → α → Prop
inst : Asymm r
⊢ Asymm (Function.swap (φ := fun (a a_1 : α) ↦ Prop) r)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
r : α → α → Prop
inst : Total r
⊢ Total (Function.swap (φ := fun (a a_1 : α) ↦ Prop) r)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
r : α → α → Prop
inst : Trichotomous r
⊢ Trichotomous (Function.swap (φ := fun (a a_1 : α) ↦ Prop) r)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
r : α → α → Prop
inst : IsPreorder α r
⊢ IsPreorder α (Function.swap (φ := fun (a a_1 : α) ↦ Prop) r)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
r : α → α → Prop
inst : IsStrictOrder α r
⊢ IsStrictOrder α (Function.swap (φ := fun (a a_1 : α) ↦ Prop) r)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
r : α → α → Prop
inst : IsPartialOrder α r
⊢ IsPartialOrder α (Function.swap (φ := fun (a a_1 : α) ↦ Prop) r)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
r : α → α → Prop
inst : Std.Irrefl r
inst_1 : Subsingleton α
⊢ ∀ (a b : α), r a b = emptyRelation a b

Tactic:
simpa using not_rel_of_subsingleton r

Premises used: not_rel_of_subsingleton