awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
R_1 R₁_1 R₂_1 : SetRel α β
S_1 : SetRel β γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
a_1 a₁_1 a₂_1 : α
b_1 : β
c_1 : γ
R R₁ R₂ : SetRel α α
S : SetRel β β
a b c : α
f : α → β
inst : R.IsSymm
a₁ a₂ : α
ha : (a₁, a₂) ∈ R
⊢ ∃ (a : α), ∃ (b : α), (a, b) ∈ R ∧ f a = f a₂ ∧ f b = f a₁

Tactic:
exact ⟨_, _, R.symm ha, rfl, rfl⟩
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
R_1 R₁_1 R₂_1 : SetRel α β
S_1 : SetRel β γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
a_1 a₁ a₂ : α
b_1 : β
c_1 : γ
R R₁ R₂ : SetRel α α
S : SetRel β β
a_2 b_2 c_2 a c b : α
hab : (a, b) ∈ R
hbc : (b, c) ∈ R.inv
⊢ (c, a) ∈ R ○ R.inv

Tactic:
⟨b, hbc, hab⟩

Premises used: Set.Mem, setOf, SetRel.comp, And.intro, Exists.intro
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
R_1 R₁_1 R₂_1 : SetRel α β
S_1 : SetRel β γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
a_1 a₁ a₂ : α
b_1 : β
c_1 : γ
R R₁ R₂ : SetRel α α
S : SetRel β β
a_2 b_2 c_2 a c b : α
hab : (a, b) ∈ R
hbc : (b, c) ∈ R.inv
⊢ (c, a) ∈ R ○ R.inv

Tactic:
exact ⟨b, hbc, hab⟩
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
R_1 R₁_1 R₂_1 : SetRel α β
S_1 : SetRel β γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
a_1 a₁ a₂ : α
b_1 : β
c_1 : γ
R R₁ R₂ : SetRel α α
S : SetRel β β
a b c : α
⊢ (R.inv ○ R).IsSymm

Tactic:
isSymm_comp_inv

Premises used: Set.Mem, SetRel.inv, setOf, SetRel.isSymm_comp_inv, Set.preimage, Prod.swap
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
R_1 R₁_1 R₂_1 : SetRel α β
S_1 : SetRel β γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
a_1 a₁ a₂ : α
b_1 : β
c_1 : γ
R R₁ R₂ : SetRel α α
S : SetRel β β
a b c : α
inst : R.IsSymm
⊢ (R ○ R).IsSymm

Tactic:
simpa using R.isSymm_comp_inv

Premises used: SetRel.isSymm_comp_inv
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
s₁ s₂ : Set α
R : SetRel α α
inst : R.IsSymm
rw : s₁ ×ˢ s₂ ⊆ R.inv ↔ s₂ ×ˢ s₁ ⊆ R.inv
rw₁ : s₁ ×ˢ s₂ ⊆ Prod.swap ⁻¹' R ↔ s₂ ×ˢ s₁ ⊆ Prod.swap ⁻¹' R
rw₂ : Prod.swap '' s₁ ×ˢ s₂ ⊆ R ↔ s₂ ×ˢ s₁ ⊆ Prod.swap ⁻¹' R
rw₃ : s₂ ×ˢ s₁ ⊆ R ↔ s₂ ×ˢ s₁ ⊆ Prod.swap ⁻¹' R
rw₄ : s₂ ×ˢ s₁ ⊆ R ↔ s₂ ×ˢ s₁ ⊆ R.inv
rw₅ rw₆ : s₂ ×ˢ s₁ ⊆ R ↔ s₂ ×ˢ s₁ ⊆ R
⊢ s₁ ×ˢ s₂ ⊆ R ↔ s₂ ×ˢ s₁ ⊆ R

Tactic:
rw [← R.inv_eq_self, SetRel.inv, ← Set.image_subset_iff, Set.image_swap_prod, ← SetRel.inv,
    R.inv_eq_self]

Premises used: SetRel.inv, Set.image_swap_prod, SetRel.inv_eq_self, Set.image_subset_iff
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
s : Set α
R : SetRel α α
inst : R.IsSymm
rw : R.preimage s = R.inv.preimage s
rw₁ rw₂ : R.preimage s = R.preimage s
⊢ R.preimage s = R.image s

Tactic:
rw [← preimage_inv, inv_eq_self]

Premises used: SetRel.inv_eq_self, SetRel.preimage_inv
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
R : SetRel α α
⊢ R.symmetrize ⊆ R

Tactic:
Set.inter_subset_left

Premises used: SetRel.symmetrize, Set.inter_subset_left
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
R : SetRel α α
⊢ R.symmetrize ⊆ R.inv

Tactic:
Set.inter_subset_right

Premises used: SetRel.symmetrize, Set.inter_subset_right
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
R S : SetRel α α
⊢ S ⊆ R.symmetrize ↔ S ⊆ R ∧ S ⊆ R.inv

Tactic:
Set.subset_inter_iff

Premises used: SetRel.symmetrize, Set.subset_inter_iff
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
R₁ R₂ : SetRel α α
h : R₁ ⊆ R₂
⊢ R₁.symmetrize ⊆ R₂.symmetrize

Tactic:
Set.inter_subset_inter h <| Set.preimage_mono h

Premises used: SetRel.symmetrize, Set.inter_subset_inter, Set.preimage_mono
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
R : SetRel α α
a b c : α
inst : R.IsTrans
hab : (a, b) ∈ R
hbc : (b, c) ∈ R
⊢ (a, c) ∈ R

Tactic:
trans_of (· ~[R] ·) hab hbc

Premises used: Membership.mem, Prod.mk, trans_of
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
R : SetRel α α
inst : R.IsTrans
⊢ R ○ R ⊆ R

Tactic:
fun ⟨_, _⟩ ⟨_, hab, hbc⟩ ↦ R.trans hab hbc

Premises used: SetRel.trans, _private.0.SetRel.comp_subset_self.match_1, Membership.mem, Prod.mk, Set.Subset, _private.0.SetRel.comp_subset_self.match_2
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
R : SetRel α α
inst : R.IsRefl
inst_1 : R.IsTrans
⊢ R ○ R = R

Tactic:
subset_antisymm comp_subset_self left_subset_comp

Premises used: SetRel.left_subset_comp, subset_antisymm, SetRel.comp_subset_self
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
R_1 R₁_1 R₂_1 : SetRel α β
S_1 : SetRel β γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
a_1 a₁ a₂ : α
b_1 : β
c_1 : γ
R R₁ R₂ : SetRel α α
S : SetRel β β
a b c x x_1 x_2 : α
⊢ Membership.mem (γ := SetRel α α) ∅ (x, x_1) →
    Membership.mem (γ := SetRel α α) ∅ (x_1, x_2) → Membership.mem (γ := SetRel α α) ∅ (x, x_2)

Tactic:
simp
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
R_1 R₁_1 R₂_1 : SetRel α β
S_1 : SetRel β γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
a_1 a₁ a₂ : α
b_1 : β
c_1 : γ
R R₁ R₂ : SetRel α α
S : SetRel β β
a b c x x_1 x_2 : α
⊢ Membership.mem (γ := SetRel α α) Set.univ (x, x_1) →
    Membership.mem (γ := SetRel α α) Set.univ (x_1, x_2) → Membership.mem (γ := SetRel α α) Set.univ (x, x_2)

Tactic:
simp
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
R_1 R₁_1 R₂_1 : SetRel α β
S_1 : SetRel β γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
a_1 a₁ a₂ : α
b_1 : β
c_1 : γ
R R₁ R₂ : SetRel α α
S : SetRel β β
a b c : α
x : α × α
x_1 x_2 x_3 : α
⊢ Membership.mem (γ := SetRel α α) {x} (x_1, x_2) →
    Membership.mem (γ := SetRel α α) {x} (x_2, x_3) → Membership.mem (γ := SetRel α α) {x} (x_1, x_3)

Tactic:
aesop
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
R_1 R₁_1 R₂_1 : SetRel α β
S_1 : SetRel β γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
a_1 a₁ a₂ : α
b_1 : β
c_1 : γ
R_2 R₁ R₂ : SetRel α α
S : SetRel β β
a b c : α
R : ι → SetRel α α
inst : ∀ (i : ι), (R i).IsTrans
⊢ ∀ (R_3 : SetRel α α), Membership.mem (γ := Set (SetRel α α)) (Set.range fun (i : ι) ↦ R i) R_3 → R_3.IsTrans

Tactic:
simpa
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
R : SetRel α α
a : α
inst : R.IsIrrefl
⊢ ¬(a, a) ∈ R

Tactic:
irrefl_of (· ~[R] ·) _

Premises used: irrefl_of, Membership.mem, Prod.mk
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
f : α → β
a : α
b : β
⊢ (a, b) ∈ graph f ↔ f a = b

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Function.graph
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
⊢ Injective (α := α → β) graph

Tactic:
aesop (add simp [Injective, Set.ext_iff])

Premises used: Set.ext_iff, Function.Injective
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
f g : α → β
⊢ graph f = graph g ↔ f = g

Tactic:
graph_injective.eq_iff

Premises used: Function.Injective.eq_iff, Function.graph_injective
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := SetRel α α) (graph id) SetRel.id

Tactic:
aesop
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → γ
g : α → β
⊢ graph (f ∘ g) = graph g ○ graph f

Tactic:
aesop
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
f : α ≃ β
⊢ Eq (α := SetRel β α) (Function.graph (⇑f.symm : (a : β) → α)) (SetRel.inv (Function.graph (⇑f : (a : α) → β)))

Tactic:
aesop
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
mp : (∃! f : α → β, Function.graph f = R) → ∀ (a : α), ∃! b : β, (a, b) ∈ R
mpr : (∀ (a : α), ∃! b : β, (a, b) ∈ R) → ∃! f : α → β, Function.graph f = R
⊢ (∃! f : α → β, Function.graph f = R) ↔ ∀ (a : α), ∃! b : β, (a, b) ∈ R

Tactic:
constructor
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
f : α → β
right : ∀ (y : α → β), (fun (f_1 : α → β) ↦ Function.graph f_1 = Function.graph f) y → y = f
x : α
⊢ ∃! b : β, (x, b) ∈ Function.graph f

Tactic:
simp
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
h : ∀ (a : α), ∃! b : β, (a, b) ∈ R
mpr : ∀ (f : (x : α) → β) (hf : ∀ (x : α), (x, f x) ∈ R), ∃! f : α → β, Function.graph f = R
⊢ ∃! f : α → β, Function.graph f = R

Tactic:
choose f hf using fun x ↦ (h x).exists

Premises used: ExistsUnique.exists
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
h : ∀ (a : α), ∃! b : β, (a, b) ∈ R
f : (x : α) → β
hf : ∀ (x : α), (x, f x) ∈ R
⊢ ∀ (y : α → β), (fun (f : α → β) ↦ Function.graph f = R) y → y = f

Tactic:
aesop
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
h : ∀ (a : α), ∃! b : β, (a, b) ∈ R
f : (x : α) → β
hf : ∀ (x : α), (x, f x) ∈ R
mpr : (fun (f : α → β) ↦ Function.graph f = R) f
⊢ ∃! f : α → β, Function.graph f = R

Tactic:
refine ⟨f, ?_, by aesop⟩
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
h : ∀ (a : α), ∃! b : β, (a, b) ∈ R
f : (x : α) → β
hf : ∀ (x : α), (x, f x) ∈ R
mpr : ∀ (a : α) (b : β), (a, b) ∈ Function.graph f ↔ (a, b) ∈ R
⊢ (fun (f : α → β) ↦ Function.graph f = R) f

Tactic:
ext ⟨a, b⟩
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
h : ∀ (a : α), ∃! b : β, (a, b) ∈ R
f : (x : α) → β
hf : ∀ (x : α), (x, f x) ∈ R
a : α
b : β
mpr : (a, b) ∈ Function.graph f → (a, b) ∈ R
mpr₁ : (a, b) ∈ R → (a, b) ∈ Function.graph f
⊢ (a, b) ∈ Function.graph f ↔ (a, b) ∈ R

Tactic:
constructor
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
h : ∀ (a : α), ∃! b : β, (a, b) ∈ R
f : (x : α) → β
hf : ∀ (x : α), (x, f x) ∈ R
a : α
b : β
⊢ (a, b) ∈ Function.graph f → (a, b) ∈ R

Tactic:
aesop
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
h : ∀ (a : α), ∃! b : β, (a, b) ∈ R
f : (x : α) → β
hf : ∀ (x : α), (x, f x) ∈ R
a : α
b : β
⊢ (a, b) ∈ R → (a, b) ∈ Function.graph f

Tactic:
(h _).unique (hf _)

Premises used: Set.Mem, setOf, Function.graph, ExistsUnique.unique
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
h : ∀ (a : α), ∃! b : β, (a, b) ∈ R
f : (x : α) → β
hf : ∀ (x : α), (x, f x) ∈ R
a : α
b : β
⊢ (a, b) ∈ R → (a, b) ∈ Function.graph f

Tactic:
exact (h _).unique (hf _)

Premises used: ExistsUnique.unique
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
⊢ f '' s = (Function.graph f).image s

Tactic:
rfl
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ f ⁻¹' s = (Function.graph f).preimage s

Tactic:
simp [Set.preimage, SetRel.preimage]

Premises used: Set.preimage, SetRel.preimage
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ f ⁻¹' s = (Function.graph f).core s

Tactic:
simp [Set.preimage, SetRel.core]

Premises used: SetRel.core, Set.preimage
-- Module: Mathlib.Data.Semiquot
Goal:
α : Type u_1
q₁ q₂ : Semiquot α
⊢ q₁ = q₂ ↔ q₁.s = q₂.s

Tactic:
⟨congr_arg _, fun h => ?_⟩

Premises used: congr_arg, Iff.intro
-- Module: Mathlib.Data.Semiquot
Goal:
α : Type u_1
q₁ q₂ : Semiquot α
refine : ∀ (h : q₁.s = q₂.s), q₁ = q₂
⊢ q₁ = q₂ ↔ q₁.s = q₂.s

Tactic:
refine ⟨congr_arg _, fun h => ?_⟩
-- Module: Mathlib.Data.Semiquot
Goal:
α : Type u_1
q₁ q₂ : Semiquot α
h : q₁.s = q₂.s
obtain :
  ∀ (s : Set α) (v₁ : Trunc (↑s : Type u_1)) (h : { s := s, val := v₁ : Semiquot α }.s = q₂.s),
    { s := s, val := v₁ : Semiquot α } = q₂
⊢ q₁ = q₂

Tactic:
obtain ⟨_, v₁⟩ := q₁
-- Module: Mathlib.Data.Semiquot
Goal:
α : Type u_1
q₂ : Semiquot α
s : Set α
v₁ : Trunc (↑s : Type u_1)
h : { s := s, val := v₁ : Semiquot α }.s = q₂.s
obtain :
  ∀ (s_1 : Set α) (v₂ : Trunc (↑s_1 : Type u_1)) (h : { s := s, val := v₁ : Semiquot α }.s = { s := s_1, val := v₂ }.s),
    { s := s, val := v₁ : Semiquot α } = { s := s_1, val := v₂ }
⊢ { s := s, val := v₁ : Semiquot α } = q₂

Tactic:
obtain ⟨_, v₂⟩ := q₂
-- Module: Mathlib.Data.Semiquot
Goal:
α : Type u_1
s : Set α
v₁ : Trunc (↑s : Type u_1)
s_1 : Set α
v₂ : Trunc (↑s_1 : Type u_1)
h : { s := s, val := v₁ : Semiquot α }.s = { s := s_1, val := v₂ }.s
h₁ : v₁ ≍ v₂
⊢ { s := s, val := v₁ : Semiquot α } = { s := s_1, val := v₂ }

Tactic:
congr
-- Module: Mathlib.Data.Semiquot
Goal:
α : Type u_1
s : Set α
v₁ : Trunc (↑s : Type u_1)
s_1 : Set α
v₂ : Trunc (↑s_1 : Type u_1)
h : { s := s, val := v₁ : Semiquot α }.s = { s := s_1, val := v₂ }.s
⊢ v₁ ≍ v₂

Tactic:
Subsingleton.helim (congrArg Trunc (congrArg Set.Elem h)) v₁ v₂

Premises used: congrArg, Set.Elem, Subsingleton.helim, Trunc
-- Module: Mathlib.Data.Semiquot
Goal:
α : Type u_1
s : Set α
v₁ : Trunc (↑s : Type u_1)
s_1 : Set α
v₂ : Trunc (↑s_1 : Type u_1)
h : { s := s, val := v₁ : Semiquot α }.s = { s := s_1, val := v₂ }.s
⊢ v₁ ≍ v₂

Tactic:
exact Subsingleton.helim (congrArg Trunc (congrArg Set.Elem h)) v₁ v₂

Premises used: congrArg, Set.Elem, Subsingleton.helim, Trunc
-- Module: Mathlib.Data.Semiquot
Goal:
α : Type u_1
q₁ q₂ : Semiquot α
⊢ q₁ = q₂ ↔ ∀ (a : α), a ∈ q₁ ↔ a ∈ q₂

Tactic:
ext_s.trans Set.ext_iff

Premises used: Semiquot.ext_s, Iff.trans, Set.ext_iff
-- Module: Mathlib.Data.Semiquot
Goal:
α : Type u_1
q : Semiquot α
⊢ ∃ (a : α), a ∈ q

Tactic:
let ⟨⟨a, h⟩, _⟩ := q.2.exists_rep
  ⟨a, h⟩

Premises used: Trunc.exists_rep, _private.0.Semiquot.exists_mem.match_1, Membership.mem, Exists, Exists.intro, Semiquot.val
-- Module: Mathlib.Data.Semiquot
Goal:
α : Type u_1
q : Semiquot α
a : α
h : a ∈ q
⊢ q = mk (s := q.s) h

Tactic:
ext_s.2 rfl

Premises used: Iff.mpr, Semiquot.ext_s, rfl
-- Module: Mathlib.Data.Semiquot
Goal:
α : Type u_1
q : Semiquot α
⊢ q.s.Nonempty

Tactic:
q.exists_mem

Premises used: Set.Nonempty, Semiquot.exists_mem
-- Module: Mathlib.Data.Semiquot
Goal:
α : Type u_1
a b : α
⊢ a ∈ Semiquot.pure b ↔ a = b

Tactic:
Set.mem_singleton_iff

Premises used: Set.Mem, Set.mem_singleton_iff
-- Module: Mathlib.Data.Semiquot
Goal:
α : Type u_1
q : Semiquot α
s : Set α
h : q.s ⊆ s
e_s : s ∪ q.s = s
⊢ q.blur' (s := s ∪ q.s) ⋯ = q.blur' (s := s) h

Tactic:
congr
-- Module: Mathlib.Data.Semiquot
Goal:
α : Type u_1
q : Semiquot α
s : Set α
h : q.s ⊆ s
⊢ s ∪ q.s = s

Tactic:
Set.union_eq_self_of_subset_right h

Premises used: Set.union_eq_self_of_subset_right
-- Module: Mathlib.Data.Semiquot
Goal:
α : Type u_1
q : Semiquot α
s : Set α
h : q.s ⊆ s
⊢ s ∪ q.s = s

Tactic:
exact Set.union_eq_self_of_subset_right h

Premises used: Set.union_eq_self_of_subset_right
-- Module: Mathlib.Data.Semiquot
Goal:
α : Type u_1
q : Semiquot α
s : Set α
h : q.s ⊆ s
a : α
⊢ a ∈ q.blur' (s := s) h ↔ a ∈ s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Data.Semiquot
Goal:
α : Type u_1
β : Type u_2
q : Semiquot α
f : α → β
h : ∀ a ∈ q, ∀ b ∈ q, f a = f b
a : α
aq : a ∈ q
revert : ∀ (h : ∀ a ∈ q, ∀ b ∈ q, f a = f b), q.liftOn f h = f a
⊢ q.liftOn f h = f a

Tactic:
revert h
-- Module: Mathlib.Data.Semiquot
Goal:
α : Type u_1
β : Type u_2
q : Semiquot α
f : α → β
a : α
aq : a ∈ q
rw : ∀ (h : ∀ a_1 ∈ mk (s := q.s) aq, ∀ b ∈ mk (s := q.s) aq, f a_1 = f b), (mk (s := q.s) aq).liftOn f h = f a
⊢ ∀ (h : ∀ a ∈ q, ∀ b ∈ q, f a = f b), q.liftOn f h = f a

Tactic:
rw [eq_mk_of_mem aq]

Premises used: Semiquot.eq_mk_of_mem
-- Module: Mathlib.Data.Semiquot
Goal:
α : Type u_1
β : Type u_2
q : Semiquot α
f : α → β
a : α
aq : a ∈ q
h : ∀ a_1 ∈ mk (s := q.s) aq, ∀ b ∈ mk (s := q.s) aq, f a_1 = f b
⊢ (mk (s := q.s) aq).liftOn f h = f a

Tactic:
rfl
-- Module: Mathlib.Data.Semiquot
Goal:
α : Type u_1
β : Type u_2
f : α → β
q : Semiquot α
b : β
⊢ b ∈ map f q ↔ ∃ a ∈ q, f a = b

Tactic:
Set.mem_image _ _ _

Premises used: Set.Mem, setOf, Set.mem_image, Set.image
-- Module: Mathlib.Data.Semiquot
Goal:
α : Type u_1
β : Type u_2
q : Semiquot α
f : α → Semiquot β
b : β
simp_rw : b ∈ q.bind f ↔ ∃ (a : α) (_ : a ∈ q), b ∈ f a
⊢ b ∈ q.bind f ↔ ∃ a ∈ q, b ∈ f a

Tactic:
simp_rw [← exists_prop]

Premises used: exists_prop
-- Module: Mathlib.Data.Semiquot
Goal:
α : Type u_1
β : Type u_2
q : Semiquot α
f : α → Semiquot β
b : β
⊢ b ∈ q.bind f ↔ ∃ (a : α) (_ : a ∈ q), b ∈ f a

Tactic:
Set.mem_iUnion₂

Premises used: Set.Mem, iSup, Set.mem_iUnion₂, Set.iUnion
-- Module: Mathlib.Data.Semiquot
Goal:
α : Type u_1
β : Type u_2
q : Semiquot α
f : α → Semiquot β
b : β
⊢ b ∈ q.bind f ↔ ∃ (a : α) (_ : a ∈ q), b ∈ f a

Tactic:
exact Set.mem_iUnion₂

Premises used: Set.mem_iUnion₂
-- Module: Mathlib.Data.Semiquot
Goal:
α β : Type u_1
⊢ Eq.{u_1 + 1} (α := (α → β) → Semiquot α → Semiquot β) (fun (x1 : α → β) (x2 : Semiquot α) ↦ x1 <$> x2) map

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Semiquot
Goal:
α β : Type u_1
⊢ Eq.{u_1 + 1} (α := Semiquot α → (α → Semiquot β) → Semiquot β)
    (fun (x1 : Semiquot α) (x2 : α → Semiquot β) ↦ x1 >>= x2) bind

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Semiquot
Goal:
α : Type u_1
a b : α
⊢ Membership.mem (γ := Semiquot α) (pure b) a ↔ a = b

Tactic:
Set.mem_singleton_iff

Premises used: Set.Mem, Set.mem_singleton_iff
-- Module: Mathlib.Data.Semiquot
Goal:
α : Type u_1
a : α
⊢ Membership.mem (γ := Semiquot α) (pure a) a

Tactic:
Set.mem_singleton a

Premises used: Set.mem_singleton, Set.Mem
-- Module: Mathlib.Data.Semiquot
Goal:
α : Type u_1
a b : α
⊢ Eq (α := Semiquot α) (pure a) (pure b) ↔ a = b

Tactic:
ext_s.trans Set.singleton_eq_singleton_iff

Premises used: Semiquot.ext_s, Set.singleton_eq_singleton_iff, Iff.trans
-- Module: Mathlib.Data.Semiquot
Goal:
α_1 : Type u_1
β : Type u_2
α : Type u_3
q : Semiquot α
⊢ ∀ (a : α), a ∈ id <$> q ↔ a ∈ q

Tactic:
simp
-- Module: Mathlib.Data.Semiquot
Goal:
α_1 : Type u_1
β_1 : Type u_2
α β : Type u_3
x : α
f : α → Semiquot β
⊢ ∀ (a : β), a ∈ pure x >>= f ↔ a ∈ f x

Tactic:
simp
-- Module: Mathlib.Data.Semiquot
Goal:
α_1 : Type u_1
β_1 : Type u_2
α β γ : Type u_3
s : Semiquot α
f : α → Semiquot β
g : β → Semiquot γ
simp : ∀ (a : γ), (∃ (a_1 : β), (∃ a ∈ s, a_1 ∈ f a) ∧ a ∈ g a_1) ↔ ∃ a_1 ∈ s, ∃ a_2 ∈ f a_1, a ∈ g a_2
⊢ ∀ (a : γ), a ∈ s >>= f >>= g ↔ Membership.mem (γ := Semiquot γ) (s >>= fun (x : α) ↦ f x >>= g) a

Tactic:
simp only [bind_def, mem_bind]

Premises used: Semiquot.bind_def, Semiquot.mem_bind
-- Module: Mathlib.Data.Semiquot
Goal:
α_1 : Type u_1
β_1 : Type u_2
α β γ : Type u_3
s : Semiquot α
f : α → Semiquot β
g : β → Semiquot γ
⊢ ∀ (a : γ), (∃ (a_1 : β), (∃ a ∈ s, a_1 ∈ f a) ∧ a ∈ g a_1) ↔ ∃ a_1 ∈ s, ∃ a_2 ∈ f a_1, a ∈ g a_2

Tactic:
fun c => ⟨fun ⟨b, ⟨a, as, bf⟩, cg⟩ => ⟨a, as, b, bf, cg⟩,
      fun ⟨a, as, b, bf, cg⟩ => ⟨b, ⟨a, as, bf⟩, cg⟩⟩

Premises used: Membership.mem, Exists, And, _private.0.Semiquot.instLawfulMonad.match_1, And.intro, Iff.intro, Exists.intro, _private.0.Semiquot.instLawfulMonad.match_2
-- Module: Mathlib.Data.Semiquot
Goal:
α_1 : Type u_1
β_1 : Type u_2
α β γ : Type u_3
s : Semiquot α
f : α → Semiquot β
g : β → Semiquot γ
⊢ ∀ (a : γ), (∃ (a_1 : β), (∃ a ∈ s, a_1 ∈ f a) ∧ a ∈ g a_1) ↔ ∃ a_1 ∈ s, ∃ a_2 ∈ f a_1, a ∈ g a_2

Tactic:
exact fun c => ⟨fun ⟨b, ⟨a, as, bf⟩, cg⟩ => ⟨a, as, b, bf, cg⟩,
      fun ⟨a, as, b, bf, cg⟩ => ⟨b, ⟨a, as, bf⟩, cg⟩⟩
-- Module: Mathlib.Data.Semiquot
Goal:
α_1 : Type u_1
β_1 : Type u_2
α β : Type u_3
f : α → β
s : Semiquot α
⊢ ∀ (a : β),
    Membership.mem (γ := Semiquot β)
        (do
          let y ← s
          pure (f y))
        a ↔
      a ∈ f <$> s

Tactic:
simp [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Data.Semiquot
Goal:
α : Type u_1
a : α
s : Semiquot α
⊢ pure a ≤ s ↔ a ∈ s

Tactic:
Set.singleton_subset_iff

Premises used: Set.singleton_subset_iff, Set.Mem, Set.Subset
-- Module: Mathlib.Data.Semiquot
Goal:
α : Type u_1
q : Semiquot α
p : q.IsPure
let : ∀ (a : α) (h : a ∈ q), q.get p ∈ q
⊢ q.get p ∈ q

Tactic:
let ⟨a, h⟩ := exists_mem q
-- Module: Mathlib.Data.Semiquot
Goal:
α : Type u_1
q : Semiquot α
p : q.IsPure
a : α
h : a ∈ q
unfold : q.liftOn id p ∈ q
⊢ q.get p ∈ q

Tactic:
unfold get

Premises used: Semiquot.get
-- Module: Mathlib.Data.Semiquot
Goal:
α : Type u_1
q : Semiquot α
p : q.IsPure
a : α
h : a ∈ q
rw : id a ∈ q
⊢ q.liftOn id p ∈ q

Tactic:
rw [liftOn_ofMem q _ _ a h]

Premises used: Semiquot.liftOn_ofMem
-- Module: Mathlib.Data.Semiquot
Goal:
α : Type u_1
q : Semiquot α
p : q.IsPure
a : α
h : a ∈ q
⊢ id a ∈ q

Tactic:
h

Premises used: Set.Mem
-- Module: Mathlib.Data.Semiquot
Goal:
α : Type u_1
q : Semiquot α
p : q.IsPure
a : α
h : a ∈ q
⊢ id a ∈ q

Tactic:
exact h
-- Module: Mathlib.Data.Semiquot
Goal:
α : Type u_1
q : Semiquot α
p : q.IsPure
a : α
⊢ a ∈ q ↔ Membership.mem (γ := Semiquot α) (pure (q.get p)) a

Tactic:
simpa using ⟨fun h => p _ h _ (get_mem _), fun e => e.symm ▸ get_mem _⟩
-- Module: Mathlib.Data.Semiquot
Goal:
α : Type u_1
a b : α
ab : Membership.mem (γ := Semiquot α) (pure a) b
c : α
ac : Membership.mem (γ := Semiquot α) (pure a) c
rw : ∀ (ab : b = a) (c : α) (ac : c = a), b = c
⊢ b = c

Tactic:
rw [mem_pure] at ab ac

Premises used: Semiquot.mem_pure
-- Module: Mathlib.Data.Semiquot
Goal:
α : Type u_1
a b : α
ab : b = a
c : α
ac : c = a
rwa rwa₁ rwa₂ rwa₃ : ∀ (ab : b = c) (ac : c = a), b = c
⊢ b = c

Tactic:
rwa [← ac] at ab
-- Module: Mathlib.Data.Semiquot
Goal:
α : Type u_1
s : Semiquot α
⊢ s.IsPure ↔ ∃ (a : α), s = pure a

Tactic:
⟨fun h => ⟨_, eq_pure h⟩, fun ⟨_, e⟩ => e.symm ▸ pure_isPure _⟩

Premises used: _private.0.Semiquot.isPure_iff.match_1, Semiquot.IsPure, Eq.rec, Semiquot.get, Semiquot.eq_pure, Iff.intro, Exists.intro, Semiquot.pure_isPure, Eq.symm
-- Module: Mathlib.Data.Semiquot
Goal:
α : Type u_1
s t : Semiquot α
h : t.IsPure
st : s ≤ t
rw : LE.le (α := Semiquot α) (pure (t.get h)) (pure (s.get ⋯))
⊢ t ≤ s

Tactic:
rw [eq_pure h, eq_pure (h.mono st)]

Premises used: Semiquot.IsPure.mono, Semiquot.eq_pure
-- Module: Mathlib.Data.Semiquot
Goal:
α : Type u_1
s t : Semiquot α
h : t.IsPure
st : s ≤ t
⊢ LE.le (α := Semiquot α) (pure (t.get h)) (pure (s.get ⋯))

Tactic:
simpa using h _ (get_mem _) _ (st <| get_mem _)

Premises used: Semiquot.get_mem
-- Module: Mathlib.Data.Semiquot
Goal:
α : Type u_1
inst : Inhabited α
⊢ ∀ (a : α), Membership.mem (γ := Semiquot α) univ a

Tactic:
@Set.mem_univ α

Premises used: Set.Mem, Set.univ, setOf, Set.mem_univ
-- Module: Mathlib.Data.Semiquot
Goal:
α : Type u_1
I J : Inhabited α
⊢ Eq.{u_1 + 1} (α := Semiquot α) univ univ

Tactic:
ext.2 fun a => refl (a ∈ univ)

Premises used: Iff.mpr, Membership.mem, Semiquot.univ, Semiquot.ext, refl
-- Module: Mathlib.Data.Semiquot
Goal:
α : Type u_1
inst : Inhabited α
⊢ IsPure.{u_1} (α := α) univ ↔ Subsingleton α

Tactic:
⟨fun h => ⟨fun a b => h a trivial b trivial⟩, fun ⟨h⟩ a _ b _ => h a b⟩

Premises used: trivial, _private.0.Semiquot.isPure_univ.match_1, Subsingleton.intro, Iff.intro, Eq
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
h : s.Terminates
⊢ s.length' = (↑(s.length h) : ℕ∞)

Tactic:
simp [length', h]

Premises used: Stream'.Seq.length'
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
h : ¬s.Terminates
⊢ s.length' = ⊤

Tactic:
simp [length', h]

Premises used: Stream'.Seq.length'
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
simp : TerminatedAt.{u} (α := α) nil 0
⊢ length.{u} (α := α) nil ⋯ = 0

Tactic:
simp [length]

Premises used: Stream'.Seq.length
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
⊢ TerminatedAt.{u} (α := α) nil 0

Tactic:
rfl

Premises used: Stream'.Seq.TerminatedAt, Stream'.const, rfl, Stream'.Seq.get?
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
⊢ TerminatedAt.{u} (α := α) nil 0

Tactic:
exact rfl

Premises used: rfl
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
⊢ length'.{u} (α := α) nil = 0

Tactic:
simp -implicitDefEqProofs [length']

Premises used: Stream'.Seq.length'
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
x : α
s : Seq α
h : s.Terminates
h0 : ¬(cons x s).TerminatedAt 0
⊢ (cons x s).length ⋯ = s.length h + 1

Tactic:
apply Nat.find_comp_succ

Premises used: Nat.find_comp_succ
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
x : α
s : Seq α
h : s.Terminates
⊢ ¬(cons x s).TerminatedAt 0

Tactic:
simp
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
x : α
s : Seq α
pos : ∀ (h : (cons x s).Terminates), (cons x s).length' = s.length' + 1
neg : ∀ (h : ¬(cons x s).Terminates), (cons x s).length' = s.length' + 1
⊢ (cons x s).length' = s.length' + 1

Tactic:
by_cases h : (cons x s).Terminates

Premises used: Stream'.Seq.Terminates, Stream'.Seq.cons
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
x : α
s : Seq α
h : (cons x s).Terminates
⊢ (cons x s).Terminates

Tactic:
have h' := h
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
x : α
s : Seq α
h : ¬(cons x s).Terminates
⊢ ¬(cons x s).Terminates

Tactic:
have h' := h