awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.SetLike.Basic
Goal:
A : Type u_1
B : Type u_2
inst : SetLike A B
inst_1 : PartialOrder A
inst_2 : IsConcreteLE A B
⊢ StrictMono.{u_1, u_2} (α := A) SetLike.coe

Tactic:
fun _ _ => coe_ssubset_coe.mpr

Premises used: Iff.mpr, StrictMono, SetLike.coe_ssubset_coe
-- Module: Mathlib.Data.SetLike.Basic
Goal:
A : Type u_1
B : Type u_2
inst : SetLike A B
inst_1 : PartialOrder A
inst_2 : IsConcreteLE A B
p q : A
⊢ p < q → ∃ (x : B), x ∈ q ∧ ¬x ∈ p

Tactic:
simpa [← coe_ssubset_coe] using Set.exists_of_ssubset

Premises used: Set.exists_of_ssubset, SetLike.coe_ssubset_coe
-- Module: Mathlib.Data.SetLike.Basic
Goal:
A : Type u_1
B : Type u_2
inst : SetLike A B
inst_1 : PartialOrder A
inst_2 : IsConcreteLE A B
p q : A
rw : p ≤ q ∧ ¬q ≤ p ↔ p ≤ q ∧ ∃ (x : B), x ∈ q ∧ ¬x ∈ p
rw₁ rw₂ : (p ≤ q ∧ ∃ (x : B), x ∈ q ∧ ¬x ∈ p) ↔ p ≤ q ∧ ∃ (x : B), x ∈ q ∧ ¬x ∈ p
⊢ p < q ↔ p ≤ q ∧ ∃ (x : B), x ∈ q ∧ ¬x ∈ p

Tactic:
rw [lt_iff_le_not_ge, not_le_iff_exists]

Premises used: lt_iff_le_not_ge, SetLike.not_le_iff_exists
-- Module: Mathlib.Data.SetLike.Basic
Goal:
X : Type u_3
p : Set X → Prop
U : Set X
h : p U
x : X
⊢ x ∈ Subtype.mk (p := p) U h ↔ x ∈ U

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Data.SetLike.Basic
Goal:
X : Type u_3
S : Type u_4
inst : SetLike S X
p : S → Prop
U : S
h : p U
x : X
⊢ x ∈ Subtype.mk (p := p) U h ↔ x ∈ U

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Data.SetLike.Fintype
Goal:
A : Type u_1
B : Type u_2
inst : SetLike A B
inst_1 : Finite B
⊢ Finite A

Tactic:
Finite.of_injective SetLike.coe SetLike.coe_injective

Premises used: SetLike.coe_injective, SetLike.coe, Finite.of_injective
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
r₁ r₂ : Setoid α
⊢ r₁ = r₂ ↔ Eq.{u_1 + 1} (α := α → α → Prop) (⇑r₁ : α → α → Prop) (⇑r₂ : α → α → Prop)

Tactic:
⟨fun h => h ▸ rfl, fun h => Setoid.ext fun _ _ => h ▸ Iff.rfl⟩

Premises used: Iff.rfl, Eq.rec, Setoid.ext, Iff.intro, rfl
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
r s : Setoid α
⊢ r ≤ s ↔ ∀ {x y : α}, (r : α → α → Prop) x y → (s : α → α → Prop) x y

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
r : Setoid α
x : α
⊢ (r : α → α → Prop) x x

Tactic:
r.iseqv.refl x

Premises used: Equivalence.refl, Setoid.iseqv
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
r : Setoid α
x y : α
⊢ (r : α → α → Prop) x y → (r : α → α → Prop) y x

Tactic:
r.iseqv.symm

Premises used: Equivalence.symm, Setoid.iseqv
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
r : Setoid α
x y z : α
⊢ (r : α → α → Prop) x y → (r : α → α → Prop) y z → (r : α → α → Prop) x z

Tactic:
r.iseqv.trans

Premises used: Equivalence.trans, Setoid.iseqv
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
s : Setoid α
x y : α
⊢ (s : α → α → Prop) x y ↔ (s : α → α → Prop) y x

Tactic:
⟨s.symm', s.symm'⟩

Premises used: Setoid.symm', Iff.intro
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
r : Setoid α
⊢ ker (β := Quotient r) Quotient.mk'' = r

Tactic:
ext fun _ _ => Quotient.eq

Premises used: Setoid.ext, Quotient.eq
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
a : α
⊢ f ⟦a⟧.out = f a

Tactic:
@Quotient.mk_out _ (Setoid.ker f) a

Premises used: Quotient.mk_out
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
x y : α
⊢ (ker f : α → α → Prop) x y ↔ f x = f y

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
β : Type u_2
r : Setoid α
s : Setoid β
x₁ x₂ : α
y₁ y₂ : β
⊢ (r.prod s : α × β → α × β → Prop) (x₁, y₁) (x₂, y₂) ↔ (r : α → α → Prop) x₁ x₂ ∧ (s : β → β → Prop) y₁ y₂

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Data.Setoid.Basic
Goal:
ι : Sort u_3
α : ι → Sort u_4
r : (i : ι) → Setoid.{u_4} (α i)
x y : (i : ι) → α i
⊢ (piSetoid : ((i : ι) → α i) → ((i : ι) → α i) → Prop) x y ↔ ∀ (i : ι), (r i : α i → α i → Prop) (x i) (y i)

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
β : Type u_2
r : Setoid α
s : Setoid β
q : Quotient (r.prod s)
x y : α × β
hxy : (r.prod s : α × β → α × β → Prop) x y
⊢ Eq.{u_1 + 1} (α := Quotient r)
    ((fun (xy : α × β) ↦ ((Quotient.mk'' xy.1, Quotient.mk'' xy.2) : Prod.{u_1, u_2} (Quotient r) (Quotient s))) x).1
    ((fun (xy : α × β) ↦ ((Quotient.mk'' xy.1, Quotient.mk'' xy.2) : Prod.{u_1, u_2} (Quotient r) (Quotient s))) y).1

Tactic:
simpa [Quotient.eq] using hxy.1

Premises used: And.left, Quotient.eq
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
β : Type u_2
r : Setoid α
s : Setoid β
q : Quotient (r.prod s)
x y : α × β
hxy : (r.prod s : α × β → α × β → Prop) x y
⊢ Eq.{u_2 + 1} (α := Quotient s)
    ((fun (xy : α × β) ↦ ((Quotient.mk'' xy.1, Quotient.mk'' xy.2) : Prod.{u_1, u_2} (Quotient r) (Quotient s))) x).2
    ((fun (xy : α × β) ↦ ((Quotient.mk'' xy.1, Quotient.mk'' xy.2) : Prod.{u_1, u_2} (Quotient r) (Quotient s))) y).2

Tactic:
simpa [Quotient.eq] using hxy.2

Premises used: And.right, Quotient.eq
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
β : Type u_2
r : Setoid α
s : Setoid β
q : Prod.{u_1, u_2} (Quotient r) (Quotient s)
rcases :
  ∀ (qa : Quotient r) (qb : Quotient s),
    (fun (q : Quotient (r.prod s)) ↦
          (q.liftOn' (fun (xy : α × β) ↦ (Quotient.mk'' xy.1, Quotient.mk'' xy.2)) ⋯ :
            Prod.{u_1, u_2} (Quotient r) (Quotient s)))
        ((fun (x : Prod.{u_1, u_2} (Quotient r) (Quotient s)) ↦
            (match (motive := Prod.{u_1, u_2} (Quotient r) (Quotient s) → Quotient (r.prod s)) x with
              | (x, y) => Quotient.map₂ Prod.mk ⋯ x y :
              Quotient (r.prod s)))
          (qa, qb)) =
      (qa, qb)
⊢ (fun (q : Quotient (r.prod s)) ↦
        (q.liftOn' (fun (xy : α × β) ↦ (Quotient.mk'' xy.1, Quotient.mk'' xy.2)) ⋯ :
          Prod.{u_1, u_2} (Quotient r) (Quotient s)))
      ((fun (x : Prod.{u_1, u_2} (Quotient r) (Quotient s)) ↦
          (match (motive := Prod.{u_1, u_2} (Quotient r) (Quotient s) → Quotient (r.prod s)) x with
            | (x, y) => Quotient.map₂ Prod.mk ⋯ x y :
            Quotient (r.prod s)))
        q) =
    q

Tactic:
rcases q with ⟨qa, qb⟩
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
β : Type u_2
r : Setoid α
s : Setoid β
qa : Quotient r
qb : Quotient s
h :
  ∀ (a₁ : α) (a₂ : β),
    Eq (α := Prod.{u_1, u_2} (Quotient r) (Quotient s))
      ((fun (q : Quotient (r.prod s)) ↦
          (q.liftOn' (fun (xy : α × β) ↦ (Quotient.mk'' xy.1, Quotient.mk'' xy.2)) ⋯ :
            Prod.{u_1, u_2} (Quotient r) (Quotient s)))
        ((fun (x : Prod.{u_1, u_2} (Quotient r) (Quotient s)) ↦
            (match (motive := Prod.{u_1, u_2} (Quotient r) (Quotient s) → Quotient (r.prod s)) x with
              | (x, y) => Quotient.map₂ Prod.mk ⋯ x y :
              Quotient (r.prod s)))
          (Quotient.mk'' a₁, Quotient.mk'' a₂)))
      (Quotient.mk'' a₁, Quotient.mk'' a₂)
⊢ (fun (q : Quotient (r.prod s)) ↦
        (q.liftOn' (fun (xy : α × β) ↦ (Quotient.mk'' xy.1, Quotient.mk'' xy.2)) ⋯ :
          Prod.{u_1, u_2} (Quotient r) (Quotient s)))
      ((fun (x : Prod.{u_1, u_2} (Quotient r) (Quotient s)) ↦
          (match (motive := Prod.{u_1, u_2} (Quotient r) (Quotient s) → Quotient (r.prod s)) x with
            | (x, y) => Quotient.map₂ Prod.mk ⋯ x y :
            Quotient (r.prod s)))
        (qa, qb)) =
    (qa, qb)

Tactic:
induction qa, qb using Quotient.inductionOn₂'
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
β : Type u_2
r : Setoid α
s : Setoid β
a₁ : α
a₂ : β
⊢ Eq (α := Prod.{u_1, u_2} (Quotient r) (Quotient s))
    ((fun (q : Quotient (r.prod s)) ↦
        (q.liftOn' (fun (xy : α × β) ↦ (Quotient.mk'' xy.1, Quotient.mk'' xy.2)) ⋯ :
          Prod.{u_1, u_2} (Quotient r) (Quotient s)))
      ((fun (x : Prod.{u_1, u_2} (Quotient r) (Quotient s)) ↦
          (match (motive := Prod.{u_1, u_2} (Quotient r) (Quotient s) → Quotient (r.prod s)) x with
            | (x, y) => Quotient.map₂ Prod.mk ⋯ x y :
            Quotient (r.prod s)))
        (Quotient.mk'' a₁, Quotient.mk'' a₂)))
    (Quotient.mk'' a₁, Quotient.mk'' a₂)

Tactic:
rfl
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
β : Type u_2
r : Setoid α
s : Setoid β
q : Quotient (r.prod s)
h :
  ∀ (a : α × β),
    Eq (α := Quotient (r.prod s))
      ((fun (x : Prod.{u_1, u_2} (Quotient r) (Quotient s)) ↦
          (match (motive := Prod.{u_1, u_2} (Quotient r) (Quotient s) → Quotient (r.prod s)) x with
            | (x, y) => Quotient.map₂ Prod.mk ⋯ x y :
            Quotient (r.prod s)))
        ((fun (q : Quotient (r.prod s)) ↦
            (q.liftOn' (fun (xy : α × β) ↦ (Quotient.mk'' xy.1, Quotient.mk'' xy.2)) ⋯ :
              Prod.{u_1, u_2} (Quotient r) (Quotient s)))
          (Quotient.mk'' a)))
      (Quotient.mk'' a)
⊢ (fun (x : Prod.{u_1, u_2} (Quotient r) (Quotient s)) ↦
        (match (motive := Prod.{u_1, u_2} (Quotient r) (Quotient s) → Quotient (r.prod s)) x with
          | (x, y) => Quotient.map₂ Prod.mk ⋯ x y :
          Quotient (r.prod s)))
      ((fun (q : Quotient (r.prod s)) ↦
          (q.liftOn' (fun (xy : α × β) ↦ (Quotient.mk'' xy.1, Quotient.mk'' xy.2)) ⋯ :
            Prod.{u_1, u_2} (Quotient r) (Quotient s)))
        q) =
    q

Tactic:
induction q using Quotient.inductionOn'
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
β : Type u_2
r : Setoid α
s : Setoid β
a : α × β
⊢ Eq (α := Quotient (r.prod s))
    ((fun (x : Prod.{u_1, u_2} (Quotient r) (Quotient s)) ↦
        (match (motive := Prod.{u_1, u_2} (Quotient r) (Quotient s) → Quotient (r.prod s)) x with
          | (x, y) => Quotient.map₂ Prod.mk ⋯ x y :
          Quotient (r.prod s)))
      ((fun (q : Quotient (r.prod s)) ↦
          (q.liftOn' (fun (xy : α × β) ↦ (Quotient.mk'' xy.1, Quotient.mk'' xy.2)) ⋯ :
            Prod.{u_1, u_2} (Quotient r) (Quotient s)))
        (Quotient.mk'' a)))
    (Quotient.mk'' a)

Tactic:
rfl
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α_1 : Type u_1
β : Type u_2
ι : Sort u_3
α : ι → Sort u_4
r : (i : ι) → Setoid.{u_4} (α i)
q : Quotient (α := (i : ι) → α i) (piSetoid (α := α))
x y : (i : ι) → α i
hxy : (piSetoid : ((i : ι) → α i) → ((i : ι) → α i) → Prop) x y
h :
  ∀ (i : ι),
    Eq.{u_4} (α := Quotient (r i)) ((fun (x : (i : ι) → α i) (i : ι) ↦ (Quotient.mk'' (x i) : Quotient (r i))) x i)
      ((fun (x : (i : ι) → α i) (i : ι) ↦ (Quotient.mk'' (x i) : Quotient (r i))) y i)
⊢ Eq (α := (i : ι) → Quotient (r i)) ((fun (x : (i : ι) → α i) (i : ι) ↦ (Quotient.mk'' (x i) : Quotient (r i))) x)
    ((fun (x : (i : ι) → α i) (i : ι) ↦ (Quotient.mk'' (x i) : Quotient (r i))) y)

Tactic:
ext i
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α_1 : Type u_1
β : Type u_2
ι : Sort u_3
α : ι → Sort u_4
r : (i : ι) → Setoid.{u_4} (α i)
q : Quotient (α := (i : ι) → α i) (piSetoid (α := α))
x y : (i : ι) → α i
hxy : (piSetoid : ((i : ι) → α i) → ((i : ι) → α i) → Prop) x y
i : ι
⊢ Eq.{u_4} (α := Quotient (r i)) ((fun (x : (i : ι) → α i) (i : ι) ↦ (Quotient.mk'' (x i) : Quotient (r i))) x i)
    ((fun (x : (i : ι) → α i) (i : ι) ↦ (Quotient.mk'' (x i) : Quotient (r i))) y i)

Tactic:
simpa [Quotient.eq] using hxy i

Premises used: Quotient.eq
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α_1 : Type u_1
β : Type u_2
ι : Sort u_3
α : ι → Sort u_4
r : (i : ι) → Setoid.{u_4} (α i)
q : (i : ι) → Quotient (r i)
h :
  ∀ (i : ι),
    (fun (q : Quotient (α := (i : ι) → α i) (piSetoid (α := α))) ↦
          (q.liftOn' (fun (x : (i : ι) → α i) (i : ι) ↦ Quotient.mk'' (x i)) ⋯ : (i : ι) → Quotient (r i)))
        ((fun (x : (i : ι) → Quotient (r i)) ↦
            (Quotient.mk'' fun (i : ι) ↦ (x i).out : Quotient (α := (i : ι) → α i) (piSetoid (α := α))))
          q)
        i =
      q i
⊢ (fun (q : Quotient (α := (i : ι) → α i) (piSetoid (α := α))) ↦
        (q.liftOn' (fun (x : (i : ι) → α i) (i : ι) ↦ Quotient.mk'' (x i)) ⋯ : (i : ι) → Quotient (r i)))
      ((fun (x : (i : ι) → Quotient (r i)) ↦
          (Quotient.mk'' fun (i : ι) ↦ (x i).out : Quotient (α := (i : ι) → α i) (piSetoid (α := α))))
        q) =
    q

Tactic:
ext i
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α_1 : Type u_1
β : Type u_2
ι : Sort u_3
α : ι → Sort u_4
r : (i : ι) → Setoid.{u_4} (α i)
q : (i : ι) → Quotient (r i)
i : ι
⊢ (fun (q : Quotient (α := (i : ι) → α i) (piSetoid (α := α))) ↦
        (q.liftOn' (fun (x : (i : ι) → α i) (i : ι) ↦ Quotient.mk'' (x i)) ⋯ : (i : ι) → Quotient (r i)))
      ((fun (x : (i : ι) → Quotient (r i)) ↦
          (Quotient.mk'' fun (i : ι) ↦ (x i).out : Quotient (α := (i : ι) → α i) (piSetoid (α := α))))
        q)
      i =
    q i

Tactic:
simp
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α_1 : Type u_1
β : Type u_2
ι : Sort u_3
α : ι → Sort u_4
r : (i : ι) → Setoid.{u_4} (α i)
q : Quotient (α := (i : ι) → α i) (piSetoid (α := α))
h :
  ∀ (a : (i : ι) → α i),
    Eq (α := Quotient (α := (i : ι) → α i) (piSetoid (α := α)))
      ((fun (x : (i : ι) → Quotient (r i)) ↦
          (Quotient.mk'' fun (i : ι) ↦ (x i).out : Quotient (α := (i : ι) → α i) (piSetoid (α := α))))
        ((fun (q : Quotient (α := (i : ι) → α i) (piSetoid (α := α))) ↦
            (q.liftOn' (fun (x : (i : ι) → α i) (i : ι) ↦ Quotient.mk'' (x i)) ⋯ : (i : ι) → Quotient (r i)))
          (Quotient.mk'' a)))
      (Quotient.mk'' a)
⊢ (fun (x : (i : ι) → Quotient (r i)) ↦
        (Quotient.mk'' fun (i : ι) ↦ (x i).out : Quotient (α := (i : ι) → α i) (piSetoid (α := α))))
      ((fun (q : Quotient (α := (i : ι) → α i) (piSetoid (α := α))) ↦
          (q.liftOn' (fun (x : (i : ι) → α i) (i : ι) ↦ Quotient.mk'' (x i)) ⋯ : (i : ι) → Quotient (r i)))
        q) =
    q

Tactic:
induction q using Quotient.inductionOn'
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α_1 : Type u_1
β : Type u_2
ι : Sort u_3
α : ι → Sort u_4
r : (i : ι) → Setoid.{u_4} (α i)
a : (i : ι) → α i
h :
  (piSetoid : ((i : ι) → α i) → ((i : ι) → α i) → Prop) (fun (i : ι) ↦ Quotient.out (s := r i) (Quotient.mk'' (a i))) a
⊢ Eq (α := Quotient (α := (i : ι) → α i) (piSetoid (α := α)))
    ((fun (x : (i : ι) → Quotient (r i)) ↦
        (Quotient.mk'' fun (i : ι) ↦ (x i).out : Quotient (α := (i : ι) → α i) (piSetoid (α := α))))
      ((fun (q : Quotient (α := (i : ι) → α i) (piSetoid (α := α))) ↦
          (q.liftOn' (fun (x : (i : ι) → α i) (i : ι) ↦ Quotient.mk'' (x i)) ⋯ : (i : ι) → Quotient (r i)))
        (Quotient.mk'' a)))
    (Quotient.mk'' a)

Tactic:
simp only [Quotient.liftOn'_mk'', Quotient.eq'']

Premises used: Quotient.liftOn'_mk'', Quotient.eq''
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α_1 : Type u_1
β : Type u_2
ι : Sort u_3
α : ι → Sort u_4
r : (i : ι) → Setoid.{u_4} (α i)
a : (i : ι) → α i
i : ι
h : (r i : α i → α i → Prop) ((fun (i : ι) ↦ Quotient.out (s := r i) (Quotient.mk'' (a i))) i) (a i)
⊢ (fun (i : ι) ↦ Quotient.out (s := r i) (Quotient.mk'' (a i))) i ≈ a i

Tactic:
change Setoid.r _ _

Premises used: Setoid.r
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α_1 : Type u_1
β : Type u_2
ι : Sort u_3
α : ι → Sort u_4
r : (i : ι) → Setoid.{u_4} (α i)
a : (i : ι) → α i
i : ι
h :
  Eq (α := Quotient (r i)) (Quotient.mk'' ((fun (i : ι) ↦ Quotient.out (s := r i) (Quotient.mk'' (a i))) i))
    (Quotient.mk'' (a i))
⊢ (r i : α i → α i → Prop) ((fun (i : ι) ↦ Quotient.out (s := r i) (Quotient.mk'' (a i))) i) (a i)

Tactic:
rw [← Quotient.eq'']

Premises used: Quotient.eq''
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α_1 : Type u_1
β : Type u_2
ι : Sort u_3
α : ι → Sort u_4
r : (i : ι) → Setoid.{u_4} (α i)
a : (i : ι) → α i
i : ι
⊢ Eq (α := Quotient (r i)) (Quotient.mk'' ((fun (i : ι) ↦ Quotient.out (s := r i) (Quotient.mk'' (a i))) i))
    (Quotient.mk'' (a i))

Tactic:
simp
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
r s : Setoid α
⊢ Eq.{u_1 + 1} (α := α → α → Prop) (⇑(r ⊓ s) : α → α → Prop) ((⇑r : α → α → Prop) ⊓ (⇑s : α → α → Prop))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
r s : Setoid α
x y : α
⊢ (r ⊓ s : α → α → Prop) x y ↔ (r : α → α → Prop) x y ∧ (s : α → α → Prop) x y

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
s : Set (Setoid α)
h : ∀ (x x_1 : α), (sInf s : α → α → Prop) x x_1 ↔ sInf (@r α '' s) x x_1
⊢ (⇑(sInf s) : α → α → Prop) = sInf (@r α '' s)

Tactic:
ext
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
s : Set (Setoid α)
x x_1 : α
h : (sInf s : α → α → Prop) x x_1 ↔ ∀ (i : Setoid α) (i_1 : i ∈ s), (i : α → α → Prop) x x_1
⊢ (sInf s : α → α → Prop) x x_1 ↔ sInf (@r α '' s) x x_1

Tactic:
simp only [sInf_image, iInf_apply, iInf_Prop_eq]

Premises used: iInf_apply, sInf_image, iInf_Prop_eq
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
s : Set (Setoid α)
x x_1 : α
⊢ (sInf s : α → α → Prop) x x_1 ↔ ∀ (i : Setoid α) (i_1 : i ∈ s), (i : α → α → Prop) x x_1

Tactic:
rfl
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := α → α → Prop) (⇑⊤ : α → α → Prop) ⊤

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := α → α → Prop) (⇑⊥ : α → α → Prop) fun (x1 x2 : α) ↦ x1 = x2

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
r : α → α → Prop
iseqv : Equivalence r
⊢ { r := r, iseqv := iseqv : Setoid α } = ⊤ ↔ r = ⊤

Tactic:
simp [eq_iff_rel_eq]

Premises used: Setoid.eq_iff_rel_eq
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
r : α → α → Prop
iseqv : Equivalence r
⊢ { r := r, iseqv := iseqv : Setoid α } = ⊥ ↔ r = fun (x1 x2 : α) ↦ x1 = x2

Tactic:
simp [eq_iff_rel_eq]

Premises used: Setoid.eq_iff_rel_eq
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
s : Setoid α
rw : (∀ {x y : α}, ⊤ x y → (s : α → α → Prop) x y) ↔ ∀ (x y : α), (s : α → α → Prop) x y
⊢ s = ⊤ ↔ ∀ (x y : α), (s : α → α → Prop) x y

Tactic:
rw [_root_.eq_top_iff, Setoid.le_def, Setoid.top_def]

Premises used: eq_top_iff, Setoid.top_def, Setoid.le_def
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
s : Setoid α
⊢ (∀ {x y : α}, ⊤ x y → (s : α → α → Prop) x y) ↔ ∀ (x y : α), (s : α → α → Prop) x y

Tactic:
simp only [Pi.top_apply, Prop.top_eq_true, forall_true_left]

Premises used: forall_true_left, Pi.top_apply, Prop.top_eq_true
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
S : Set (Setoid α)
x y : α
⊢ x ≈ y ↔ ∀ s ∈ S, (s : α → α → Prop) x y

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
S : Set (Setoid α)
x y : α
⊢ (sInf S : α → α → Prop) x y ↔ ∀ s ∈ S, (s : α → α → Prop) x y

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
S : Set (Setoid α)
x y : α
⊢ ⟦x⟧ = ⟦y⟧ ↔ ∀ s ∈ S, (s : α → α → Prop) x y

Tactic:
simp [sInf_iff, Quotient.eq]

Premises used: Setoid.sInf_iff, Quotient.eq
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
r : α → α → Prop
⊢ EqvGen.setoid r = sInf {s : Setoid α | ∀ ⦃x y : α⦄, r x y → (s : α → α → Prop) x y}

Tactic:
le_antisymm
    (fun _ _ H =>
      EqvGen.rec (fun _ _ h _ hs => hs h) (refl' _) (fun _ _ _ => symm' _)
        (fun _ _ _ _ _ => trans' _) H)
    (sInf_le fun _ _ h => EqvGen.rel _ _ h)

Premises used: le_antisymm, sInf_le, Relation.EqvGen.rel
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
r s : Setoid α
rw :
  r ⊔ s =
    sInf {s_1 : Setoid α | ∀ ⦃x y : α⦄, (r : α → α → Prop) x y ∨ (s : α → α → Prop) x y → (s_1 : α → α → Prop) x y}
⊢ r ⊔ s = EqvGen.setoid fun (x y : α) ↦ (r : α → α → Prop) x y ∨ (s : α → α → Prop) x y

Tactic:
rw [eqvGen_eq]

Premises used: Setoid.eqvGen_eq
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
r s : Setoid α
apply :
  Eq.{u_1 + 1} (α := Set (Setoid α)) {x : Setoid α | r ≤ x ∧ s ≤ x}
    {s_1 : Setoid α | ∀ ⦃x y : α⦄, (r : α → α → Prop) x y ∨ (s : α → α → Prop) x y → (s_1 : α → α → Prop) x y}
⊢ r ⊔ s =
    sInf {s_1 : Setoid α | ∀ ⦃x y : α⦄, (r : α → α → Prop) x y ∨ (s : α → α → Prop) x y → (s_1 : α → α → Prop) x y}

Tactic:
apply congr_arg sInf

Premises used: congr_arg, InfSet.sInf
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
r s : Setoid α
⊢ Eq.{u_1 + 1} (α := Set (Setoid α)) {x : Setoid α | r ≤ x ∧ s ≤ x}
    {s_1 : Setoid α | ∀ ⦃x y : α⦄, (r : α → α → Prop) x y ∨ (s : α → α → Prop) x y → (s_1 : α → α → Prop) x y}

Tactic:
simp only [le_def, or_imp, ← forall_and]

Premises used: or_imp, Setoid.le_def, forall_and
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
r s : Setoid α
rw :
  Eq.{u_1 + 1} (α := Setoid α) (EqvGen.setoid fun (x y : α) ↦ (r : α → α → Prop) x y ∨ (s : α → α → Prop) x y)
    (EqvGen.setoid ((⇑r : α → α → Prop) ⊔ (⇑s : α → α → Prop)))
⊢ r ⊔ s = EqvGen.setoid ((⇑r : α → α → Prop) ⊔ (⇑s : α → α → Prop))

Tactic:
rw [sup_eq_eqvGen]

Premises used: Setoid.sup_eq_eqvGen
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
r s : Setoid α
⊢ Eq.{u_1 + 1} (α := Setoid α) (EqvGen.setoid fun (x y : α) ↦ (r : α → α → Prop) x y ∨ (s : α → α → Prop) x y)
    (EqvGen.setoid ((⇑r : α → α → Prop) ⊔ (⇑s : α → α → Prop)))

Tactic:
rfl
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
S : Set (Setoid α)
rw : sSup S = sInf {s : Setoid α | ∀ ⦃x y : α⦄, (∃ r ∈ S, (r : α → α → Prop) x y) → (s : α → α → Prop) x y}
⊢ sSup S = EqvGen.setoid fun (x y : α) ↦ ∃ r ∈ S, (r : α → α → Prop) x y

Tactic:
rw [eqvGen_eq]

Premises used: Setoid.eqvGen_eq
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
S : Set (Setoid α)
apply : upperBounds S = {s : Setoid α | ∀ ⦃x y : α⦄, (∃ r ∈ S, (r : α → α → Prop) x y) → (s : α → α → Prop) x y}
⊢ sSup S = sInf {s : Setoid α | ∀ ⦃x y : α⦄, (∃ r ∈ S, (r : α → α → Prop) x y) → (s : α → α → Prop) x y}

Tactic:
apply congr_arg sInf

Premises used: congr_arg, InfSet.sInf
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
S : Set (Setoid α)
simp :
  Eq.{u_1 + 1} (α := Set (Setoid α))
    {x : Setoid α | ∀ ⦃a : Setoid α⦄, a ∈ S → ∀ {x_1 y : α}, (a : α → α → Prop) x_1 y → (x : α → α → Prop) x_1 y}
    {s : Setoid α | ∀ ⦃x y : α⦄, ∀ x_1 ∈ S, (x_1 : α → α → Prop) x y → (s : α → α → Prop) x y}
⊢ upperBounds S = {s : Setoid α | ∀ ⦃x y : α⦄, (∃ r ∈ S, (r : α → α → Prop) x y) → (s : α → α → Prop) x y}

Tactic:
simp only [upperBounds, le_def, and_imp, exists_imp]

Premises used: and_imp, upperBounds, Setoid.le_def, exists_imp
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
S : Set (Setoid α)
h :
  ∀ (x : Setoid α),
    Membership.mem (γ := Set (Setoid α))
        {x : Setoid α | ∀ ⦃a : Setoid α⦄, a ∈ S → ∀ {x_1 y : α}, (a : α → α → Prop) x_1 y → (x : α → α → Prop) x_1 y}
        x ↔
      Membership.mem (γ := Set (Setoid α))
        {s : Setoid α | ∀ ⦃x y : α⦄, ∀ x_1 ∈ S, (x_1 : α → α → Prop) x y → (s : α → α → Prop) x y} x
⊢ Eq.{u_1 + 1} (α := Set (Setoid α))
    {x : Setoid α | ∀ ⦃a : Setoid α⦄, a ∈ S → ∀ {x_1 y : α}, (a : α → α → Prop) x_1 y → (x : α → α → Prop) x_1 y}
    {s : Setoid α | ∀ ⦃x y : α⦄, ∀ x_1 ∈ S, (x_1 : α → α → Prop) x y → (s : α → α → Prop) x y}

Tactic:
ext
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
S : Set (Setoid α)
x : Setoid α
⊢ Membership.mem (γ := Set (Setoid α))
      {x : Setoid α | ∀ ⦃a : Setoid α⦄, a ∈ S → ∀ {x_1 y : α}, (a : α → α → Prop) x_1 y → (x : α → α → Prop) x_1 y} x ↔
    Membership.mem (γ := Set (Setoid α))
      {s : Setoid α | ∀ ⦃x y : α⦄, ∀ x_1 ∈ S, (x_1 : α → α → Prop) x y → (s : α → α → Prop) x y} x

Tactic:
⟨fun H x y r hr => H hr, fun H r hr x y => H r hr⟩

Premises used: Iff.intro
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
S : Set (Setoid α)
x : Setoid α
⊢ Membership.mem (γ := Set (Setoid α))
      {x : Setoid α | ∀ ⦃a : Setoid α⦄, a ∈ S → ∀ {x_1 y : α}, (a : α → α → Prop) x_1 y → (x : α → α → Prop) x_1 y} x ↔
    Membership.mem (γ := Set (Setoid α))
      {s : Setoid α | ∀ ⦃x y : α⦄, ∀ x_1 ∈ S, (x_1 : α → α → Prop) x y → (s : α → α → Prop) x y} x

Tactic:
exact ⟨fun H x y r hr => H hr, fun H r hr x y => H r hr⟩
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
s : Set (Setoid α)
rw :
  Eq.{u_1 + 1} (α := Setoid α) (EqvGen.setoid fun (x y : α) ↦ ∃ r ∈ s, (r : α → α → Prop) x y)
    (EqvGen.setoid (⨆ a ∈ s, (⇑a : α → α → Prop)))
⊢ sSup s = EqvGen.setoid (sSup (@r α '' s))

Tactic:
rw [sSup_eq_eqvGen, sSup_image]

Premises used: Setoid.sSup_eq_eqvGen, sSup_image