awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
h :
  ∀ ⦃α : Type u⦄ (x : (↑(P F) : (α : Type u) → Type (max u u_1)) α),
    Eq.{u + 1} (α := Set α) {y : α | ∀ ⦃p : α → Prop⦄, Liftp p (abs x) → p y}
      {y : α | ∀ ⦃p : α → Prop⦄, Liftp p x → p y}
α : Type u
p : α → Prop
a : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → α
h' : IsUniform.{u, u_1} (F := F)
mp : (∀ u ∈ f '' univ, p u) ↔ ∀ (i : (P F).B a), p (f i)
⊢ Liftp p (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f)) ↔
    Liftp (F := (↑(P F) : (α : Type u) → Type (max u u_1))) p
      (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f)

Tactic:
rw [liftp_iff_of_isUniform h', supp_eq_of_isUniform h', PFunctor.liftp_iff']

Premises used: QPF.liftp_iff_of_isUniform, QPF.supp_eq_of_isUniform, PFunctor.liftp_iff'
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
h :
  ∀ ⦃α : Type u⦄ (x : (↑(P F) : (α : Type u) → Type (max u u_1)) α),
    Eq.{u + 1} (α := Set α) {y : α | ∀ ⦃p : α → Prop⦄, Liftp p (abs x) → p y}
      {y : α | ∀ ⦃p : α → Prop⦄, Liftp p x → p y}
α : Type u
p : α → Prop
a : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → α
h' : IsUniform.{u, u_1} (F := F)
⊢ (∀ u ∈ f '' univ, p u) ↔ ∀ (i : (P F).B a), p (f i)

Tactic:
simp
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
h : ∀ ⦃α : Type u⦄ (p : α → Prop) (x : (↑(P F) : (α : Type u) → Type (max u u_1)) α), Liftp p (abs x) ↔ Liftp p x
α : Type u
a : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → α
⊢ Eq (α := Set α) (supp (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f)))
    (supp (F := (↑(P F) : (α : Type u) → Type (max u u_1)))
      (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f))

Tactic:
simp only [supp, h]

Premises used: Functor.supp
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
rw : SuppPreservation.{u, u_1} (F := F) ↔ IsUniform.{u, u_1} (F := F)
rw₁ rw₂ : IsUniform.{u, u_1} (F := F) ↔ IsUniform.{u, u_1} (F := F)
⊢ LiftpPreservation.{u, u_1} (F := F) ↔ IsUniform.{u, u_1} (F := F)

Tactic:
rw [← suppPreservation_iff_liftpPreservation, suppPreservation_iff_uniform]

Premises used: QPF.suppPreservation_iff_uniform, QPF.suppPreservation_iff_liftpPreservation
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_3
r : α → α → Prop
iseqv : Equivalence r
p : α → α → Prop
iseqv_1 : Equivalence p
Eq : ∀ (a b : α), ({ r := r, iseqv := iseqv } : α → α → Prop) a b ↔ ({ r := p, iseqv := iseqv_1 } : α → α → Prop) a b
⊢ _root_.Eq.{max 1 u_3} r p

Tactic:
have : r = p := funext fun a ↦ funext fun b ↦ propext <| Eq a b
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_3
r : α → α → Prop
iseqv : Equivalence r
p : α → α → Prop
iseqv_1 : Equivalence p
Eq : ∀ (a b : α), ({ r := r, iseqv := iseqv } : α → α → Prop) a b ↔ ({ r := p, iseqv := iseqv_1 } : α → α → Prop) a b
this : _root_.Eq.{max 1 u_3} r p
subst :
  ∀ (iseqv_2 : Equivalence r)
    (Eq :
      ∀ (a b : α), ({ r := r, iseqv := iseqv } : α → α → Prop) a b ↔ ({ r := r, iseqv := iseqv_2 } : α → α → Prop) a b),
    _root_.Eq.{max 1 u_3} { r := r, iseqv := iseqv : Setoid α } { r := r, iseqv := iseqv_2 }
⊢ _root_.Eq.{max 1 u_3} { r := r, iseqv := iseqv : Setoid α } { r := p, iseqv := iseqv_1 }

Tactic:
subst this
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_3
r : α → α → Prop
iseqv iseqv_1 : Equivalence r
Eq : ∀ (a b : α), ({ r := r, iseqv := iseqv } : α → α → Prop) a b ↔ ({ r := r, iseqv := iseqv_1 } : α → α → Prop) a b
⊢ _root_.Eq.{max 1 u_3} { r := r, iseqv := iseqv : Setoid α } { r := r, iseqv := iseqv_1 }

Tactic:
rfl
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_4
r : α → α → Prop
β : Quot r → Prop
q : Quot r
h : ∀ (a : α), β ⟦a⟧
⊢ β q

Tactic:
ind h q

Premises used: Quot.ind
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_1
β : Sort u_2
ra : α → α → Prop
rb : β → β → Prop
φ : Quot ra → Quot rb → Sort u_3
inst : Subsingleton α
⊢ Subsingleton.{u_1} (Quot ra)

Tactic:
⟨fun x ↦ Quot.induction_on x fun _ ↦ Quot.ind fun _ ↦ congr_arg _ (Subsingleton.elim _ _)⟩

Premises used: Quot.induction_on, Subsingleton.intro
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_1
β : Sort u_2
ra : α → α → Prop
rb : β → β → Prop
φ : Quot ra → Quot rb → Sort u_3
qa : Quot ra
qb : Quot rb
f : (a : α) → (b : β) → φ ⟦a⟧ ⟦b⟧
ca : ∀ {b : β} {a₁ a₂ : α}, ra a₁ a₂ → f a₁ b ≍ f a₂ b
cb : ∀ {a : α} {b₁ b₂ : β}, rb b₁ b₂ → f a b₁ ≍ f a b₂
a₁ a₂ : α
pa : ra a₁ a₂
b : β
⊢ Quot.hrecOn (r := rb) (motive := φ ⟦a₁⟧) ⟦b⟧ (f a₁) ⋯ ≍ f a₁ b

Tactic:
simp
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_1
β : Sort u_2
ra : α → α → Prop
rb : β → β → Prop
φ : Quot ra → Quot rb → Sort u_3
qa : Quot ra
qb : Quot rb
f : (a : α) → (b : β) → φ ⟦a⟧ ⟦b⟧
ca : ∀ {b : β} {a₁ a₂ : α}, ra a₁ a₂ → f a₁ b ≍ f a₂ b
cb : ∀ {a : α} {b₁ b₂ : β}, rb b₁ b₂ → f a b₁ ≍ f a b₂
a₁ a₂ : α
pa : ra a₁ a₂
b : β
h₁ : Quot.hrecOn (r := rb) (motive := φ ⟦a₁⟧) ⟦b⟧ (f a₁) ⋯ ≍ f a₁ b
⊢ f a₂ b ≍ Quot.hrecOn (r := rb) (motive := φ ⟦a₂⟧) ⟦b⟧ (f a₂) ⋯

Tactic:
simp
-- Module: Mathlib.Data.Quot
Goal:
α : Type u_4
r s : α → α → Prop
h : ∀ (x y : α), r x y → s x y
⊢ factor r s h ∘ mk r = mk s

Tactic:
rfl

Premises used: Quot.factor, rfl
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_1
γ : Sort u_4
r : α → α → Prop
f : α → γ
h : ∀ (a₁ a₂ : α), r a₁ a₂ → f a₁ = f a₂
a : α
⊢ lift (r := r) f h ⟦a⟧ = f a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_1
γ : Sort u_4
r : α → α → Prop
a : α
f : α → γ
h : ∀ (a₁ a₂ : α), r a₁ a₂ → f a₁ = f a₂
⊢ ⟦a⟧.liftOn (r := r) f h = f a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_1
γ : Sort u_4
r : α → α → Prop
f : α → γ
h : ∀ (a₁ a₂ : α), r a₁ a₂ → f a₁ = f a₂
⊢ Function.Surjective (lift (r := r) f h) ↔ Function.Surjective f

Tactic:
⟨fun hf => hf.comp Quot.exists_rep, fun hf y => let ⟨x, hx⟩ := hf y; ⟨Quot.mk _ x, hx⟩⟩

Premises used: Exists, Quot.exists_rep, Quot.lift, _private.0.Quot.surjective_lift.match_1, Iff.intro, Exists.intro, Function.Surjective.comp, Eq, Quot.mk
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_4
r : α → α → Prop
s : β → β → Prop
f : α → β → γ
hr : ∀ (a : α) (b₁ b₂ : β), s b₁ b₂ → f a b₁ = f a b₂
hs : ∀ (a₁ a₂ : α) (b : β), r a₁ a₂ → f a₁ b = f a₂ b
a : α
b : β
⊢ Quot.lift₂ (r := r) (s := s) f hr hs ⟦a⟧ ⟦b⟧ = f a b

Tactic:
rfl

Premises used: Quot.lift₂, rfl
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_4
r : α → α → Prop
s : β → β → Prop
a : α
b : β
f : α → β → γ
hr : ∀ (a : α) (b₁ b₂ : β), s b₁ b₂ → f a b₁ = f a b₂
hs : ∀ (a₁ a₂ : α) (b : β), r a₁ a₂ → f a₁ b = f a₂ b
⊢ ⟦a⟧.liftOn₂ (r := r) (s := s) ⟦b⟧ f hr hs = f a b

Tactic:
rfl

Premises used: Quot.lift₂, Quot.liftOn₂, rfl
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : α → β → γ
hr : ∀ (a : α) (b₁ b₂ : β), s b₁ b₂ → t (f a b₁) (f a b₂)
hs : ∀ (a₁ a₂ : α) (b : β), r a₁ a₂ → t (f a₁ b) (f a₂ b)
a : α
b : β
⊢ Quot.map₂ (r := r) (s := s) (t := t) f hr hs ⟦a⟧ ⟦b⟧ = ⟦f a b⟧

Tactic:
rfl

Premises used: Quot.map₂, Quot.lift₂, rfl
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_1
β : Sort u_2
r : α → α → Prop
s : β → β → Prop
δ : Quot r → Quot s → Prop
q₁ : Quot r
q₂ : Quot s
h : ∀ (a : α) (b : β), δ ⟦a⟧ ⟦b⟧
⊢ δ q₁ q₂

Tactic:
Quot.ind (β := fun a ↦ δ a q₂) (fun a₁ ↦ Quot.ind (fun a₂ ↦ h a₁ a₂) q₂) q₁

Premises used: Quot.ind
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
δ : Quot r → Quot s → Quot t → Prop
q₁ : Quot r
q₂ : Quot s
q₃ : Quot t
h : ∀ (a : α) (b : β) (c : γ), δ ⟦a⟧ ⟦b⟧ ⟦c⟧
⊢ δ q₁ q₂ q₃

Tactic:
Quot.ind (β := fun a ↦ δ a q₂ q₃) (fun a₁ ↦ Quot.ind (β := fun b ↦ δ _ b q₃)
    (fun a₂ ↦ Quot.ind (fun a₃ ↦ h a₁ a₂ a₃) q₃) q₂) q₁

Premises used: Quot.ind
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_1
β : Sort u_2
sa : Setoid α
sb : Setoid β
φ : Quotient sa → Quotient sb → Sort u_3
s : Setoid α
inst : Subsingleton α
⊢ Subsingleton.{u_1} (Quotient s)

Tactic:
Quot.Subsingleton

Premises used: Quotient, Quot.Subsingleton
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_1
β : Sort u_2
sa : Setoid α
sb : Setoid β
f : α → β
h : ∀ ⦃a b : α⦄, a ≈ b → f a ≈ f b
x : α
⊢ Quotient.map f h ⟦x⟧ = ⟦f x⟧

Tactic:
rfl

Premises used: Quotient.map, rfl
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_1
β : Sort u_2
sa : Setoid α
sb : Setoid β
γ : Sort u_4
sc : Setoid γ
f : α → β → γ
h : ∀ ⦃a₁ a₂ : α⦄, a₁ ≈ a₂ → ∀ ⦃b₁ b₂ : β⦄, b₁ ≈ b₂ → f a₁ b₁ ≈ f a₂ b₂
x : α
y : β
⊢ Quotient.map₂ f h ⟦x⟧ ⟦y⟧ = ⟦f x y⟧

Tactic:
rfl

Premises used: Quotient.map₂, rfl
-- Module: Mathlib.Data.Quot
Goal:
α : Type u_3
r : α → α → Prop
x y : α
⊢ mk r x = mk r y ↔ Relation.EqvGen r x y

Tactic:
⟨Quot.eqvGen_exact, Quot.eqvGen_sound⟩

Premises used: Quot.eqvGen_sound, Iff.intro, Quot.eqvGen_exact
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_1
r : Setoid α
x y : α
⊢ ⟦x⟧ = ⟦y⟧ ↔ (r : α → α → Prop) x y

Tactic:
⟨Quotient.exact, Quotient.sound⟩

Premises used: Iff.intro, Quotient.exact, Quotient.sound
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_1
r : Setoid α
x y : α
⊢ ⟦x⟧ = ⟦y⟧ ↔ x ≈ y

Tactic:
Quotient.eq

Premises used: Quotient.eq
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_3
s : Setoid α
p : Quotient s → Prop
⊢ (∀ (a : Quotient s), p a) ↔ ∀ (a : α), p ⟦a⟧

Tactic:
⟨fun h _ ↦ h _, fun h a ↦ a.ind h⟩

Premises used: Quotient.ind, Quotient.mk, Iff.intro
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_3
s : Setoid α
p : Quotient s → Prop
⊢ (∃ (a : Quotient s), p a) ↔ ∃ (a : α), p ⟦a⟧

Tactic:
⟨fun ⟨q, hq⟩ ↦ q.ind (motive := (p · → _)) .intro hq, fun ⟨a, ha⟩ ↦ ⟨⟦a⟧, ha⟩⟩

Premises used: _private.0.Quotient.exists.match_2, Exists, Quotient.ind, Quotient.mk, Iff.intro, _private.0.Quotient.exists.match_1, Exists.intro
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_1
β : Sort u_2
s : Setoid α
f : α → β
h : ∀ (a b : α), a ≈ b → f a = f b
x : α
⊢ Quotient.lift f h ⟦x⟧ = f x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_1
β : Sort u_2
x : Setoid α
f : α → β
h : ∀ (a b : α), a ≈ b → f a = f b
⊢ Quotient.lift f h ∘ Quotient.mk x = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_3
β : Sort u_4
s : Setoid α
f : α → β
h : ∀ (a b : α), a ≈ b → f a = f b
⊢ Function.Surjective (Quotient.lift f h) ↔ Function.Surjective f

Tactic:
Quot.surjective_lift h

Premises used: Quot.surjective_lift, Quotient
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_3
β : Sort u_4
s : Setoid α
f : α → β
h : ∀ (a b : α), a ≈ b → f a = f b
hf : Function.Surjective f
⊢ Function.Surjective (Quotient.lift f h)

Tactic:
(Quot.surjective_lift h).mpr hf

Premises used: Iff.mpr, Quot.surjective_lift, Quotient
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_3
β : Sort u_4
γ : Sort u_5
x : Setoid α
x_1 : Setoid β
f : α → β → γ
h : ∀ (a₁ : α) (a₂ : β) (b₁ : α) (b₂ : β), a₁ ≈ b₁ → a₂ ≈ b₂ → f a₁ a₂ = f b₁ b₂
a : α
b : β
⊢ Quotient.lift₂ f h ⟦a⟧ ⟦b⟧ = f a b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_1
β : Sort u_2
s : Setoid α
f : α → β
h : ∀ (a b : α), a ≈ b → f a = f b
x : α
⊢ ⟦x⟧.liftOn f h = f x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_3
β : Sort u_4
γ : Sort u_5
x_1 : Setoid α
x_2 : Setoid β
f : α → β → γ
h : ∀ (a₁ : α) (b₁ : β) (a₂ : α) (b₂ : β), a₁ ≈ a₂ → b₁ ≈ b₂ → f a₁ b₁ = f a₂ b₂
x : α
y : β
⊢ ⟦x⟧.liftOn₂ ⟦y⟧ f h = f x y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_1
r : α → α → Prop
⊢ Function.Surjective (mk r)

Tactic:
Quot.exists_rep

Premises used: Quot.exists_rep, Function.Surjective
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_1
s : Setoid α
⊢ Function.Surjective (Quotient.mk s)

Tactic:
Quot.mk_surjective

Premises used: Quotient, Quot.mk_surjective
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_1
s : Setoid α
⊢ Function.Surjective.{u_1, u_1} (α := α) (β := Quotient s) Quotient.mk'

Tactic:
Quot.mk_surjective

Premises used: Quotient, Quotient.mk', Quot.mk_surjective
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_1
β : Sort u_2
ra : α → α → Prop
rb : β → β → Prop
f : α → β
h : ∀ ⦃a b : α⦄, ra a b → rb (f a) (f b)
hf : Function.Surjective f
⊢ Function.Surjective (Quot.map (ra := ra) (rb := rb) f h)

Tactic:
surjective_lift _ |>.mpr <| .comp Quot.mk_surjective hf

Premises used: Iff.mpr, Quot.surjective_lift, Quot.map, Function.Surjective.comp, Quot.mk_surjective
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_1
β : Sort u_2
sa : Setoid α
sb : Setoid β
f : α → β
h : ∀ ⦃a b : α⦄, a ≈ b → f a ≈ f b
hf : Function.Surjective f
⊢ Function.Surjective (Quotient.map f h)

Tactic:
lift_surjective _ _ <| .comp Quot.mk_surjective hf

Premises used: Quotient.map, Quotient.lift_surjective, Quotient, Quot.map, Function.Surjective.comp, Quot.mk_surjective
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_1
r : α → α → Prop
q : Quot r
⊢ mk r (q.out (r := r)) = q

Tactic:
Classical.choose_spec (Quot.exists_rep q)

Premises used: Quot.out, Quot.exists_rep, Classical.choose_spec
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_1
s : Setoid α
q : Quotient s
⊢ ⟦q.out⟧ = q

Tactic:
Quot.out_eq q

Premises used: Quot.out_eq, Quotient.out, Quotient
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_1
s : Setoid α
a : α
⊢ (s : α → α → Prop) ⟦a⟧.out a

Tactic:
Quotient.exact (Quotient.out_eq _)

Premises used: Quotient.exact, Quotient.out_eq
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_1
s : Setoid α
x : α
y : Quotient s
⊢ ⟦x⟧ = y ↔ x ≈ y.out

Tactic:
Iff.trans ?_ Quotient.eq

Premises used: Iff.trans, Quotient.eq
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_1
s : Setoid α
x : α
y : Quotient s
refine : ⟦x⟧ = y ↔ ⟦x⟧ = ⟦y.out⟧
⊢ ⟦x⟧ = y ↔ x ≈ y.out

Tactic:
refine Iff.trans ?_ Quotient.eq

Premises used: Iff.trans, Quotient.eq
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_1
s : Setoid α
x : α
y : Quotient s
rw rw₁ : ⟦x⟧ = y ↔ ⟦x⟧ = y
⊢ ⟦x⟧ = y ↔ ⟦x⟧ = ⟦y.out⟧

Tactic:
rw [Quotient.out_eq y]

Premises used: Quotient.out_eq
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_1
s : Setoid α
x : Quotient s
y : α
⊢ x = ⟦y⟧ ↔ x.out ≈ y

Tactic:
Iff.trans ?_ Quotient.eq

Premises used: Iff.trans, Quotient.eq
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_1
s : Setoid α
x : Quotient s
y : α
refine : x = ⟦y⟧ ↔ ⟦x.out⟧ = ⟦y⟧
⊢ x = ⟦y⟧ ↔ x.out ≈ y

Tactic:
refine Iff.trans ?_ Quotient.eq

Premises used: Iff.trans, Quotient.eq
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_1
s : Setoid α
x : Quotient s
y : α
rw rw₁ : x = ⟦y⟧ ↔ x = ⟦y⟧
⊢ x = ⟦y⟧ ↔ ⟦x.out⟧ = ⟦y⟧

Tactic:
rw [Quotient.out_eq x]

Premises used: Quotient.out_eq
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_1
s : Setoid α
x y : Quotient s
rw : x = ⟦y.out⟧ ↔ x = y
rw₁ rw₂ : x = y ↔ x = y
⊢ x.out ≈ y.out ↔ x = y

Tactic:
rw [← Quotient.eq_mk_iff_out, Quotient.out_eq]

Premises used: Quotient.eq_mk_iff_out, Quotient.out_eq
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_1
s : Setoid α
⊢ Function.Injective.{u_1, u_1} (α := Quotient s) out

Tactic:
fun _ _ h ↦ Quotient.out_equiv_out.1 <| h ▸ Setoid.refl _

Premises used: Quotient.out_equiv_out, Eq.rec, Quotient.out, Iff.mp, Setoid.refl, Function.Injective
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_1
s : Setoid α
x y : Quotient s
⊢ x.out = y.out ↔ x = y

Tactic:
⟨fun h ↦ Quotient.out_injective h, fun h ↦ h ▸ rfl⟩

Premises used: Quotient.out_injective, Eq.rec, Iff.intro, rfl
-- Module: Mathlib.Data.Quot
Goal:
α_1 : Sort u_1
β : Sort u_2
ι : Type u_3
α : ι → Sort u_4
S : (i : ι) → Setoid.{u_4} (α i)
⊢ Setoid ((i : ι) → α i)

Tactic:
infer_instance
-- Module: Mathlib.Data.Quot
Goal:
α_1 : Sort u_1
β : Sort u_2
ι : Type u_3
α : ι → Sort u_4
S : (i : ι) → Setoid.{u_4} (α i)
q : Quotient (α := (i : ι) → α i) inferInstance
i : ι
x x_1 : (i : ι) → α i
h : x ≈ x_1
⊢ HasEquiv.Equiv.{u_4, 0} (α := α i) ((fun (x : (i : ι) → α i) ↦ x i) x) ((fun (x : (i : ι) → α i) ↦ x i) x_1)

Tactic:
h i
-- Module: Mathlib.Data.Quot
Goal:
α_1 : Sort u_1
β : Sort u_2
ι : Type u_3
α : ι → Sort u_4
S : (i : ι) → Setoid.{u_4} (α i)
q : Quotient (α := (i : ι) → α i) inferInstance
i : ι
x x_1 : (i : ι) → α i
h : x ≈ x_1
⊢ HasEquiv.Equiv.{u_4, 0} (α := α i) ((fun (x : (i : ι) → α i) ↦ x i) x) ((fun (x : (i : ι) → α i) ↦ x i) x_1)

Tactic:
exact h i
-- Module: Mathlib.Data.Quot
Goal:
ι : Type u_3
α : ι → Type u_4
S : (i : ι) → Setoid (α i)
f : (i : ι) → α i
⊢ Eq (α := (i : ι) → Quotient (S i)) (eval (α := α) ⟦f⟧) fun (i : ι) ↦ ⟦f i⟧

Tactic:
rfl

Premises used: Quotient.map, Quotient.eval, rfl
-- Module: Mathlib.Data.Quot
Goal:
α_1 : Sort u_1
β : Sort u_2
ι : Type u_3
α : ι → Type u_4
S : (i : ι) → Setoid (α i)
f : (i : ι) → Quotient (S i)
⊢ Setoid ((i : ι) → α i)

Tactic:
infer_instance
-- Module: Mathlib.Data.Quot
Goal:
ι : Type u_3
α : ι → Type u_4
S : (i : ι) → Setoid (α i)
f : (i : ι) → α i
⊢ Eq (α := Quotient (α := (i : ι) → α i) inferInstance) (choice (α := α) fun (i : ι) ↦ ⟦f i⟧) ⟦f⟧

Tactic:
Quotient.sound fun _ ↦ Quotient.mk_out _

Premises used: Quotient.choice, Quotient.sound, Quotient.mk_out
-- Module: Mathlib.Data.Quot
Goal:
ι : Type u_3
α : ι → Sort u_4
s : (i : ι) → Setoid.{u_4} (α i)
p : ((i : ι) → Quotient (s i)) → Prop
f : (i : ι) → Quotient (s i)
h : ∀ (a : (i : ι) → α i), p fun (i : ι) ↦ ⟦a i⟧
rw : p fun (i : ι) ↦ ⟦(f i).out⟧
⊢ p f

Tactic:
rw [← (funext fun i ↦ Quotient.out_eq (f i) : (fun i ↦ ⟦(f i).out⟧) = f)]

Premises used: funext, Quotient.out_eq
-- Module: Mathlib.Data.Quot
Goal:
ι : Type u_3
α : ι → Sort u_4
s : (i : ι) → Setoid.{u_4} (α i)
p : ((i : ι) → Quotient (s i)) → Prop
f : (i : ι) → Quotient (s i)
h : ∀ (a : (i : ι) → α i), p fun (i : ι) ↦ ⟦a i⟧
⊢ p fun (i : ι) ↦ ⟦(f i).out⟧

Tactic:
apply h
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_1
s : Setoid α
⊢ Nonempty.{u_1} (Quotient s) ↔ Nonempty α

Tactic:
⟨fun ⟨a⟩ ↦ Quotient.inductionOn a Nonempty.intro, fun ⟨a⟩ ↦ ⟨⟦a⟧⟩⟩

Premises used: _private.0.nonempty_quotient_iff.match_2, Nonempty.intro, Quotient.inductionOn, Quotient.mk, Quotient, _private.0.nonempty_quotient_iff.match_1, Iff.intro, Nonempty
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_1
⊢ Equivalence fun (x x_1 : α) ↦ True

Tactic:
⟨fun _ ↦ trivial, fun _ ↦ trivial, fun _ _ ↦ trivial⟩

Premises used: trivial, Equivalence.mk
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_1
β : Trunc α → Prop
⊢ (∀ (a : α), β (mk a)) → ∀ (q : Trunc α), β q

Tactic:
Quot.ind

Premises used: Quot.ind, Trunc.mk, Quotient, Trunc
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
c : ∀ (a b : α), f a = f b
a : α
⊢ lift f c (mk a) = f a

Tactic:
rfl

Premises used: rfl, Trunc.lift
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_1
β : Trunc α → Prop
q : Trunc α
h : ∀ (a : α), β (mk a)
⊢ β q

Tactic:
ind h q

Premises used: Trunc.ind
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_1
q : Trunc α
⊢ ∃ (a : α), mk a = q

Tactic:
Quot.exists_rep q

Premises used: Quot.exists_rep, Trunc.mk, Quotient, Trunc
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_1
β : Sort u_2
C : Trunc α → Trunc β → Prop
q₁ : Trunc α
q₂ : Trunc β
h : ∀ (a : α) (b : β), C (mk a) (mk b)
⊢ C q₁ q₂

Tactic:
Trunc.induction_on q₁ fun a₁ ↦ Trunc.induction_on q₂ (h a₁)

Premises used: Trunc.induction_on
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_1
a b : Trunc α
⊢ a = b

Tactic:
Trunc.induction_on₂ a b fun _ _ ↦ Quot.sound trivial

Premises used: Trunc.induction_on₂
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_1
β : Sort u_2
⊢ Subsingleton.{u_1} (Trunc α)

Tactic:
⟨Trunc.eq⟩

Premises used: Subsingleton.intro, Trunc.eq
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_1
q : Trunc α
⊢ mk q.out = q

Tactic:
Trunc.eq _ _

Premises used: Trunc.eq
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_1
q : Trunc α
⊢ Nonempty α

Tactic:
q.exists_rep.nonempty

Premises used: Trunc.exists_rep, Exists.nonempty
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_1
s₁ : Setoid α
⊢ Function.Surjective.{u_1, u_1} (α := α) (β := Quotient s₁) Quotient.mk''

Tactic:
Quot.exists_rep

Premises used: Quot.exists_rep, Quotient, Function.Surjective
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_1
φ : Sort u_4
s₁ : Setoid α
f : α → φ
h : ∀ (a b : α), (s₁ : α → α → Prop) a b → f a = f b
x : α
⊢ Quotient.liftOn' (Quotient.mk'' x) f h = f x

Tactic:
rfl

Premises used: Quotient.liftOn', rfl
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_1
φ : Sort u_4
s₁ : Setoid α
f : α → φ
h : ∀ (a b : α), (s₁ : α → α → Prop) a b → f a = f b
⊢ (Function.Surjective.{u_1, u_4} (β := φ) fun (x : Quotient s₁) ↦ x.liftOn' f h) ↔ Function.Surjective f

Tactic:
Quot.surjective_lift _

Premises used: Quotient.liftOn', Quot.surjective_lift, Quotient
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s₁ : Setoid α
s₂ : Setoid β
f : α → β → γ
h : ∀ (a₁ : α) (a₂ : β) (b₁ : α) (b₂ : β), (s₁ : α → α → Prop) a₁ b₁ → (s₂ : β → β → Prop) a₂ b₂ → f a₁ a₂ = f b₁ b₂
a : α
b : β
⊢ Quotient.liftOn₂' (Quotient.mk'' a) (Quotient.mk'' b) f h = f a b

Tactic:
rfl

Premises used: rfl, Quotient.liftOn₂'
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_1
s₁ : Setoid α
p : Quotient s₁ → Prop
h : ∀ (a : α), p (Quotient.mk'' a)
q : Quotient s₁
⊢ p q

Tactic:
Quotient.ind h q

Premises used: Quotient.ind
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_1
β : Sort u_2
s₁ : Setoid α
s₂ : Setoid β
p : Quotient s₁ → Quotient s₂ → Prop
h : ∀ (a₁ : α) (a₂ : β), p (Quotient.mk'' a₁) (Quotient.mk'' a₂)
q₁ : Quotient s₁
q₂ : Quotient s₂
⊢ p q₁ q₂

Tactic:
Quotient.ind₂ h q₁ q₂

Premises used: Quotient.ind₂
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_1
s₁ : Setoid α
p : Quotient s₁ → Prop
q : Quotient s₁
h : ∀ (a : α), p (Quotient.mk'' a)
⊢ p q

Tactic:
Quotient.inductionOn q h

Premises used: Quotient.inductionOn
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_1
β : Sort u_2
s₁ : Setoid α
s₂ : Setoid β
p : Quotient s₁ → Quotient s₂ → Prop
q₁ : Quotient s₁
q₂ : Quotient s₂
h : ∀ (a₁ : α) (a₂ : β), p (Quotient.mk'' a₁) (Quotient.mk'' a₂)
⊢ p q₁ q₂

Tactic:
Quotient.inductionOn₂ q₁ q₂ h

Premises used: Quotient.inductionOn₂
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s₁ : Setoid α
s₂ : Setoid β
s₃ : Setoid γ
p : Quotient s₁ → Quotient s₂ → Quotient s₃ → Prop
q₁ : Quotient s₁
q₂ : Quotient s₂
q₃ : Quotient s₃
h : ∀ (a₁ : α) (a₂ : β) (a₃ : γ), p (Quotient.mk'' a₁) (Quotient.mk'' a₂) (Quotient.mk'' a₃)
⊢ p q₁ q₂ q₃

Tactic:
Quotient.inductionOn₃ q₁ q₂ q₃ h

Premises used: Quotient.inductionOn₃
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_1
s₁ : Setoid α
φ : Quotient s₁ → Sort u_5
f : (a : α) → φ (Quotient.mk'' a)
c : ∀ (a₁ a₂ : α), a₁ ≈ a₂ → f a₁ ≍ f a₂
x : α
⊢ Quotient.hrecOn' (φ := φ) (Quotient.mk'' x) f c = f x

Tactic:
rfl

Premises used: Quotient.hrecOn', rfl
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_1
β : Sort u_2
s₁ : Setoid α
s₂ : Setoid β
φ : Quotient s₁ → Quotient s₂ → Sort u_5
f : (a : α) → (b : β) → φ (Quotient.mk'' a) (Quotient.mk'' b)
c : ∀ (a₁ : α) (b₁ : β) (a₂ : α) (b₂ : β), a₁ ≈ a₂ → b₁ ≈ b₂ → f a₁ b₁ ≍ f a₂ b₂
x : α
qb : Quotient s₂
⊢ Quotient.hrecOn₂' (φ := φ) (Quotient.mk'' x) qb f c = qb.hrecOn' (φ := φ (Quotient.mk'' x)) (f x) ⋯

Tactic:
rfl

Premises used: Quotient.hrecOn', Quotient.hrecOn₂', Quot.hrecOn₂, rfl
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_1
β : Sort u_2
s₁ : Setoid α
s₂ : Setoid β
f : α → β
h : ∀ (a b : α), (s₁ : α → α → Prop) a b → (s₂ : β → β → Prop) (f a) (f b)
x : α
⊢ Quotient.map' f h (Quotient.mk'' x) = Quotient.mk'' (f x)

Tactic:
rfl

Premises used: Quotient.map', rfl
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s₁ : Setoid α
s₂ : Setoid β
s₃ : Setoid γ
f : α → β → γ
h :
  ∀ ⦃a₁ a₂ : α⦄,
    (s₁ : α → α → Prop) a₁ a₂ → ∀ ⦃b₁ b₂ : β⦄, (s₂ : β → β → Prop) b₁ b₂ → (s₃ : γ → γ → Prop) (f a₁ b₁) (f a₂ b₂)
x : α
⊢ Quotient.map₂' f h (Quotient.mk'' x) = Quotient.map' (f x) ⋯

Tactic:
rfl

Premises used: Quotient.map₂', Quotient, Quot.map, Quotient.map', rfl
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_1
s₁ : Setoid α
a b : α
⊢ Eq (α := Quotient s₁) (Quotient.mk'' a) (Quotient.mk'' b) → (s₁ : α → α → Prop) a b

Tactic:
Quotient.exact

Premises used: Quotient.exact
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_1
s₁ : Setoid α
a b : α
⊢ (s₁ : α → α → Prop) a b → Eq (α := Quotient s₁) (Quotient.mk'' a) (Quotient.mk'' b)

Tactic:
Quotient.sound

Premises used: Quotient.sound
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_1
s₁ : Setoid α
a b : α
⊢ Eq (α := Quotient s₁) (Quotient.mk' a) (Quotient.mk' b) ↔ (s₁ : α → α → Prop) a b

Tactic:
Quotient.eq

Premises used: Quotient.mk', Quotient.eq