mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: m : Type u → Type v
σ : Type u
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ ω✝ γ✝ : Type u
cmd✝ : StateT σ m α✝
next✝ : Label ω✝ (StateT σ m) γ✝ → α✝ → StateT σ m ω✝
s✝ : σ
⊢ (StateT.mk fun r ↦ do
          let x ← cmd✝.run r
          callCC fun f ↦ (next✝ (StateT.mkLabel f) x.fst).run x.snd).run
      s✝ =
    (do
          let x ← cmd✝
          StateT.mk fun r ↦ callCC fun f' ↦ (next✝ (StateT.mkLabel f') x).run r).run
      s✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: m : Type u → Type v
σ : Type u
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
x✝ : α✝
dead✝ : Label α✝ (StateT σ m) β✝ → β✝ → StateT σ m α✝
s✝ : σ
⊢ (StateT.mk fun r ↦ pure (x✝, r)).run s✝ = (pure x✝).run s✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: m : Type u → Type v
σ : Type u
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
dummy✝ : StateT σ m α✝
s✝ : σ
⊢ (StateT.mk fun r ↦ dummy✝.run r).run s✝ = dummy✝.run s✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: case mk
m : Type u → Type v
α : Type u_1
ρ β : Type u
i : α
apply✝ : α → m β
⊢ goto (mkLabel ρ { apply := apply✝ }) i = monadLift (goto { apply := apply✝ } i)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: case zero
β : Type u_1
α : TypeVec.{u_1} 0
⊢ (α ::: β).repeatEq = splitFun α.repeatEq (uncurry Eq)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: case succ
β : Type u_1
n✝ : ℕ
a✝ : ∀ (α : TypeVec.{u_1} n✝), (α ::: β).repeatEq = splitFun α.repeatEq (uncurry Eq)
α : TypeVec.{u_1} (n✝ + 1)
⊢ (α ::: β).repeatEq = splitFun α.repeatEq (uncurry Eq)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: case fz
n : ℕ
p : Prop
n✝ : ℕ
α : TypeVec.{u_1} (n✝ + 1)
x : α Fin2.fz
⊢ ofRepeat (TypeVec.const p α Fin2.fz x) ↔ p

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: m : Type u → Type v
ρ : Type u
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ ω✝ γ✝ : Type u
cmd✝ : ReaderT ρ m α✝
next✝ : Label ω✝ (ReaderT ρ m) γ✝ → α✝ → ReaderT ρ m ω✝
ctx✝ : ρ
⊢ (ReaderT.mk fun r ↦ do
          let x ← cmd✝.run r
          callCC fun f ↦ (next✝ (ReaderT.mkLabel ρ f) x).run r).run
      ctx✝ =
    (do
          let x ← cmd✝
          ReaderT.mk fun r ↦ callCC fun f' ↦ (next✝ (ReaderT.mkLabel ρ f') x).run r).run
      ctx✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: m : Type u → Type v
ρ : Type u
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
x✝ : α✝
dead✝ : Label α✝ (ReaderT ρ m) β✝ → β✝ → ReaderT ρ m α✝
ctx✝ : ρ
⊢ (ReaderT.mk fun r ↦ pure x✝).run ctx✝ = (pure x✝).run ctx✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: m : Type u → Type v
ρ : Type u
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
dummy✝ : ReaderT ρ m α✝
ctx✝ : ρ
⊢ (ReaderT.mk fun r ↦ dummy✝.run r).run ctx✝ = dummy✝.run ctx✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: case neg
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
hh : ∀ (i : ℕ) (b : β x), b ∉ approx (⇑f) i x
b' : β x
i : ℕ
h' : b' ∈ approx (⇑f) i x
⊢ b' ∈ approx (⇑f) 0 x

Tactic:
cases hh _ _ h'

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: case fz
n n✝ : ℕ
α α' β β' : TypeVec.{u_1} (n✝ + 1)
f : α ⟹ β
g : α' ⟹ β'
⊢ (prod.fst ⊚ (f ⊗' g)) Fin2.fz = (f ⊚ prod.fst) Fin2.fz

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: case fz
n n✝ : ℕ
α α' β β' : TypeVec.{u_1} (n✝ + 1)
f : α ⟹ β
g : α' ⟹ β'
⊢ (prod.snd ⊚ (f ⊗' g)) Fin2.fz = (g ⊚ prod.snd) Fin2.fz

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: case fz
n n✝ : ℕ
α : TypeVec.{u_1} (n✝ + 1)
⊢ (prod.fst ⊚ prod.diag) Fin2.fz = id Fin2.fz

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: case fz
n n✝ : ℕ
α : TypeVec.{u_1} (n✝ + 1)
⊢ (prod.snd ⊚ prod.diag) Fin2.fz = id Fin2.fz

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: case fz
n n✝ : ℕ
α : TypeVec.{u_1} (n✝ + 1)
x y : α Fin2.fz
⊢ ofRepeat (α.repeatEq Fin2.fz (prod.mk Fin2.fz x y)) ↔ x = y

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
i : ℕ
hx : Part.fix (⇑f) x ≤ approx (⇑f) i x
⊢ f (approx (⇑f) i) x ≤ (Pi.evalOrderHom x) ((approxChain f) (i + 1))

Tactic:
rfl

Goal state after:
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: S : Type u_1
T : Type u_2
X : Type u_3
π : T → S × Option X
hπ : Function.Surjective π
σ : Option X → S → T
hσ : ∀ (x : Option X) (s : S), (π (σ x s)).1 = s
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
s : S
y : T
hy : π y = (s, none)
⊢ y ∈ fibres π σ

Tactic:
grind

Goal state after:
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: S : Type u_1
T : Type u_2
X : Type u_3
π : T → S × Option X
hπ : Function.Surjective π
σ : Option X → S → T
hσ : ∀ (x : Option X) (s : S), (π (σ x s)).1 = s
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
s : S
x : X
⊢ ((fun x ↦ π ↑x) ⟨σ (Option.some x) s, ⋯⟩).1 = (s, Option.some x).1

Tactic:
grind

Goal state after:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: α : Type u_1
β : α → Type u_2
g : ((a : α) → Part (β a)) → (a : α) → Part (β a)
hc : ωScottContinuous g
⊢ Part.fix g = Part.fix ⇑{ toFun := g, monotone' := ⋯ }

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: case fz.mk
n✝¹ n✝ : ℕ
α✝ β✝ : TypeVec.{u} (n✝ + 1)
fst✝ : α✝.last
snd✝ : β✝.last
⊢ (id ⊗' id) Fin2.fz (fst✝, snd✝) = id Fin2.fz (fst✝, snd✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: S : Type u_1
T : Type u_2
X : Type u_3
π : T → S × Option X
hπ : Function.Surjective π
σ : Option X → S → T
hσ : ∀ (x : Option X) (s : S), (π (σ x s)).1 = s
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
s : S
x : X
⊢ ((fun x ↦ π ↑x) ⟨σ (Option.some x) s, ⋯⟩).2 = (s, Option.some x).2

Tactic:
grind

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: case fz.mk
n : ℕ
α α' β β' : TypeVec.{u} n
φ φ' ψ ψ' : Type u
f₀ : α ⟹ α'
g₀ : β ⟹ β'
f₁ : φ → φ'
g₁ : ψ → ψ'
fst✝ : φ
snd✝ : ψ
⊢ (f₀ ⊗' g₀ ::: Prod.map f₁ g₁) Fin2.fz (fst✝, snd✝) = ((f₀ ::: f₁) ⊗' (g₀ ::: g₁)) Fin2.fz (fst✝, snd✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: case fs
n : ℕ
α α' β β' : TypeVec.{u} n
φ φ' ψ ψ' : Type u
f₀ : α ⟹ α'
g₀ : β ⟹ β'
f₁ : φ → φ'
g₁ : ψ → ψ'
a✝ : Fin2 n
a : ((α ⊗ β) ::: (φ × ψ)) a✝.fs
⊢ (f₀ ⊗' g₀ ::: Prod.map f₁ g₁) a✝.fs a = ((f₀ ::: f₁) ⊗' (g₀ ::: g₁)) a✝.fs a

Tactic:
rfl

Goal state after:
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: S : Type u_1
T : Type u_2
X : Type u_3
π : T → S × Option X
σ : Option X → S → T
hσ : ∀ (x : Option X) (s : S), (π (σ x s)).1 = s
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
t : T
ht : t ∈ fibres π σ
t' : T
ht' : t' ∈ fibres π σ
property✝ : π_r π σ (⟨t, ht⟩, ⟨t', ht'⟩).1 = π_r π σ (⟨t, ht⟩, ⟨t', ht'⟩).2
h : (π t).2 = none
⊢ ⟨t, ht⟩ ∈ Prod.snd ∘ π_r π σ ⁻¹' {none}

Tactic:
grind

Goal state after:
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: S : Type u_1
T : Type u_2
X : Type u_3
π : T → S × Option X
σ : Option X → S → T
hσ : ∀ (x : Option X) (s : S), (π (σ x s)).1 = s
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
t : T
ht : t ∈ fibres π σ
t' : T
ht' : t' ∈ fibres π σ
property✝ : π_r π σ (⟨t, ht⟩, ⟨t', ht'⟩).1 = π_r π σ (⟨t, ht⟩, ⟨t', ht'⟩).2
h : (π t).2 = none
⊢ ⟨t', ht'⟩ ∈ Prod.snd ∘ π_r π σ ⁻¹' {none}

Tactic:
grind

Goal state after:
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: S : Type u_1
T : Type u_2
X : Type u_3
π : T → S × Option X
σ : Option X → S → T
hσ : ∀ (x : Option X) (s : S), (π (σ x s)).1 = s
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
t : T
ht : t ∈ fibres π σ
t' : T
ht' : t' ∈ fibres π σ
property✝ : π_r π σ (⟨t, ht⟩, ⟨t', ht'⟩).1 = π_r π σ (⟨t, ht⟩, ⟨t', ht'⟩).2
h : (π t).2 = none
⊢ π_r π σ (fibreIncl π σ (⟨⟨t, ht⟩, ⋯⟩, ⟨⟨t', ht'⟩, ⋯⟩).1) = π_r π σ (fibreIncl π σ (⟨⟨t, ht⟩, ⋯⟩, ⟨⟨t', ht'⟩, ⋯⟩).2)

Tactic:
grind

Goal state after:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: α : Type u_1
f : Part α → Part α
hc : ωScottContinuous f
x✝ : Chain (Unit → Part α)
⊢ ωSup (x✝.map ({ toFun := f, monotone' := ⋯ }.comp (Pi.evalOrderHom PUnit.unit))) =
    Part.ωSup ((x✝.map (toUnitMono { toFun := f, monotone' := ⋯ })).map (Pi.evalOrderHom PUnit.unit))

Tactic:
rfl

Goal state after:
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: S : Type u_1
T : Type u_2
X : Type u_3
π : T → S × Option X
σ : Option X → S → T
hσ : ∀ (x : Option X) (s : S), (π (σ x s)).1 = s
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
t : T
ht : t ∈ fibres π σ
t' : T
ht' : t' ∈ fibres π σ
property✝ : π_r π σ (⟨t, ht⟩, ⟨t', ht'⟩).1 = π_r π σ (⟨t, ht⟩, ⟨t', ht'⟩).2
h : (π t).2 = none
⊢ coverToFun (fibreIncl π σ) (π_r π σ) (Sum.inr ⟨(⟨⟨t, ht⟩, ⋯⟩, ⟨⟨t', ht'⟩, ⋯⟩), ⋯⟩) = ⟨(⟨t, ht⟩, ⟨t', ht'⟩), property✝⟩

Tactic:
grind

Goal state after:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: α : Type u_1
β : α → Type u_2
f : Part α → Part α
hc : ωScottContinuous f
⊢ (toUnitMono { toFun := f, monotone' := ⋯ }) (Part.fix ⇑(toUnitMono { toFun := f, monotone' := ⋯ })) () = f (Fix.fix f)

Tactic:
rfl

Goal state after:
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: S : Type u_1
T : Type u_2
X : Type u_3
π : T → S × Option X
σ : Option X → S → T
hσ : ∀ (x : Option X) (s : S), (π (σ x s)).1 = s
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
t : T
ht : t ∈ fibres π σ
t' : T
ht' : t' ∈ fibres π σ
property✝ : π_r π σ (⟨t, ht⟩, ⟨t', ht'⟩).1 = π_r π σ (⟨t, ht⟩, ⟨t', ht'⟩).2
h : ¬(π t).2 = none
n : X
hn : (π t).2 = Option.some n
⊢ σ (Option.some n) (π t).1 ∈ fibres π σ

Tactic:
grind

Goal state after:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst✝ : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
c : Chain ((x : (a : α) × β a) → γ x.fst x.snd)
x : α
y : β x
⊢ (monotoneCurry α β γ) (fun a ↦ ωSup (c.map (evalOrderHom a))) x y =
    ωSup (c.map (((evalOrderHom y).comp (evalOrderHom x)).comp (monotoneCurry α β γ)))

Tactic:
rfl

Goal state after:
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: S : Type u_1
T : Type u_2
X : Type u_3
π : T → S × Option X
σ : Option X → S → T
hσ : ∀ (x : Option X) (s : S), (π (σ x s)).1 = s
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
t : T
ht : t ∈ fibres π σ
t' : T
ht' : t' ∈ fibres π σ
property✝ : π_r π σ (⟨t, ht⟩, ⟨t', ht'⟩).1 = π_r π σ (⟨t, ht⟩, ⟨t', ht'⟩).2
h : ¬(π t).2 = none
n : X
hn : (π t).2 = Option.some n
⊢ coverToFun (fibreIncl π σ) (π_r π σ) (Sum.inl ⟨σ (Option.some n) (π t).1, ⋯⟩) = ⟨(⟨t, ht⟩, ⟨t', ht'⟩), property✝⟩

Tactic:
grind

Goal state after:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst✝ : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
c : Chain ((a : α) → (b : β a) → γ a b)
x : α
y : β x
⊢ ωSup (c.map ((evalOrderHom y).comp (evalOrderHom x))) =
    ωSup (c.map ((evalOrderHom ⟨x, y⟩).comp (monotoneUncurry α β γ)))

Tactic:
rfl

Goal state after:
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: R : Type
inst✝ : CommRing R
S : Type u_1
T : Type u_2
X : Type u_3
π : T → S × Option X
σ : Option X → S → T
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
s : S
⊢ σ none s ∈ fibres π σ

Tactic:
grind

Goal state after:
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: R : Type
inst✝ : CommRing R
S : Type u_1
T : Type u_2
X : Type u_3
π : T → S × Option X
σ : Option X → S → T
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
s : S
⊢ ⟨σ none s, ⋯⟩ ∈ Prod.snd ∘ π_r π σ ⁻¹' {none}

Tactic:
grind

Goal state after:
Module: Mathlib.Control.Traversable.Equiv

Goal state before:
pp: case mk.e_map
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝¹ : Functor t
inst✝ : LawfulFunctor t
map✝ : {α β : Type u} → (α → β) → t' α → t' β
mapConst✝ : {α β : Type u} → α → t' β → t' α
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
x✝³ x✝² : Type u
x✝¹ : x✝³ → x✝²
x✝ : t' x✝³
⊢ map✝ x✝¹ x✝ = x✝¹ <$> x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Traversable.Equiv

Goal state before:
pp: case mk.e_mapConst
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝¹ : Functor t
inst✝ : LawfulFunctor t
map✝ : {α β : Type u} → (α → β) → t' α → t' β
mapConst✝ : {α β : Type u} → α → t' β → t' α
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
x✝³ x✝² : Type u
x✝¹ : x✝³
x✝ : t' x✝²
⊢ mapConst✝ x✝¹ x✝ = mapConst x✝¹ x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst✝¹ : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
inst✝ : LawfulFix ((x : Sigma β) → γ x.fst x.snd)
_f : ((x : α) → (y : β x) → γ x y) → (x : α) → (y : β x) → γ x y
hc : ωScottContinuous _f
⊢ curry
      (((monotoneUncurry α β γ).comp ({ toFun := _f, monotone' := ⋯ }.comp (monotoneCurry α β γ)))
        (fix ⇑((monotoneUncurry α β γ).comp ({ toFun := _f, monotone' := ⋯ }.comp (monotoneCurry α β γ))))) =
    _f (curry (fix (uncurry ∘ _f ∘ curry)))

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Traversable.Equiv

Goal state before:
pp: t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
α β : Type u
f : α → β
x : t' α
⊢ ⇑(eqv β) <$> pure (f <$> (eqv α).symm x) = pure (Equiv.map eqv f x)

Tactic:
rfl

Goal state after:
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: S : Type u_1
T : Type u_2
X : Type u_3
π : T → S × OnePoint X
hπ : Function.Surjective π
s : S
p : S → OnePoint X → T := fun s n ↦ ⋯.choose
hp : ∀ (s : S) (n : OnePoint X), π (p s n) = (s, n)
n : OnePoint X
⊢ p s n ∈ Prod.snd ∘ π ⁻¹' {n}

Tactic:
grind

Goal state after:
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: S : Type u_1
T : Type u_2
X : Type u_3
π : T → S × OnePoint X
hπ : Function.Surjective π
s : S
p : S → OnePoint X → T := fun s n ↦ ⋯.choose
hp : ∀ (s : S) (n : OnePoint X), π (p s n) = (s, n)
⊢ (fun n ↦ ⟨p s n, ⋯⟩) ∈ S' π

Tactic:
grind

Goal state after:
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: S : Type u_1
T : Type u_2
X : Type u_3
π : T → S × OnePoint X
hπ : Function.Surjective π
s : S
p : S → OnePoint X → T := fun s n ↦ ⋯.choose
hp : ∀ (s : S) (n : OnePoint X), π (p s n) = (s, n)
⊢ y π ⟨fun n ↦ ⟨p s n, ⋯⟩, ⋯⟩ = s

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Analysis.Filter

Goal state before:
pp: case mk
α : Type u_1
σ : Type u_3
τ : Type u_4
inst✝ : PartialOrder α
E : σ ≃ τ
a : τ
f✝ : σ → α
pt✝ : σ
inf✝ : σ → σ → σ
inf_le_left✝ : ∀ (a b : σ), f✝ (inf✝ a b) ≤ f✝ a
inf_le_right✝ : ∀ (a b : σ), f✝ (inf✝ a b) ≤ f✝ b
⊢ (ofEquiv E { f := f✝, pt := pt✝, inf := inf✝, inf_le_left := inf_le_left✝, inf_le_right := inf_le_right✝ }).f a =
    { f := f✝, pt := pt✝, inf := inf✝, inf_le_left := inf_le_left✝, inf_le_right := inf_le_right✝ }.f (E.symm a)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Analysis.Filter

Goal state before:
pp: case mk
α : Type u_1
a : Set α
σ✝ : Type u_5
F✝ : CFilter (Set α) σ✝
⊢ a ∈ F✝.toFilter ↔ ∃ b, { σ := σ✝, F := F✝, eq := ⋯ }.F.f b ⊆ a

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Analysis.Topology

Goal state before:
pp: case mk
α : Type u_1
σ : Type u_3
τ : Type u_4
E : σ ≃ τ
a : τ
f✝ : σ → Set α
top✝ : α → σ
top_mem✝ : ∀ (x : α), x ∈ f✝ (top✝ x)
inter✝ : (a b : σ) → (x : α) → x ∈ f✝ a ∩ f✝ b → σ
inter_mem✝ : ∀ (a b : σ) (x : α) (h : x ∈ f✝ a ∩ f✝ b), x ∈ f✝ (inter✝ a b x h)
inter_sub✝ : ∀ (a b : σ) (x : α) (h : x ∈ f✝ a ∩ f✝ b), f✝ (inter✝ a b x h) ⊆ f✝ a ∩ f✝ b
⊢ (ofEquiv E
          { f := f✝, top := top✝, top_mem := top_mem✝, inter := inter✝, inter_mem := inter_mem✝,
            inter_sub := inter_sub✝ }).f
      a =
    { f := f✝, top := top✝, top_mem := top_mem✝, inter := inter✝, inter_mem := inter_mem✝, inter_sub := inter_sub✝ }.f
      (E.symm a)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Analysis.Filter

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f : α → Filter β
F : (i : α) → (f i).Realizer
⊢ ∀ (x : Set β), x ∈ (⊤.bind f).sets ↔ x ∈ (⨆ i, f i).sets

Tactic:
simp [Filter.bind, iSup_sets_eq]

Goal state after:
Module: Mathlib.Data.Bool.Count

Goal state before:
pp: l : List Bool
b : Bool
⊢ count b l + count (!b) l = l.length

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Bool.Count

Goal state before:
pp: case nil
b : Bool
hl : IsChain (fun x1 x2 ↦ x1 ≠ x2) []
h2 : Even [].length
⊢ count (!b) [] = count b []

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.DFinsupp.Interval

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → DecidableEq (α i)
inst✝² : (i : ι) → PartialOrder (α i)
inst✝¹ : (i : ι) → Zero (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
f g x : Π₀ (i : ι), α i
⊢ ((∀ (x_1 : ι), f x_1 ≤ x x_1) ∧ ∀ (x_1 : ι), x x_1 ≤ g x_1) ↔ f ≤ x ∧ x ≤ g

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Semiquot

Goal state before:
pp: α : Type u_1
β : Type u_2
q : Semiquot α
f : α → β
a : α
aq : a ∈ q
h✝ : ∀ a_1 ∈ mk aq, ∀ b ∈ mk aq, f a_1 = f b
⊢ (mk aq).liftOn f h✝ = f a

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Curry

Goal state before:
pp: case zero
τ : Type u
p : Fin 0 → Type u
f : FromTypes p τ
⊢ curry f.uncurry = f

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Take

Goal state before:
pp: n : ℕ
α : Fin n → Sort u_1
m : ℕ
h : m ≤ n
v : (i : Fin n) → α i
i : Fin n
hi : ↑i ≥ m
x : α i
j : Fin m
⊢ ↑(castLE h j) ≠ ↑i

Tactic:
simp only [val_castLE]

Goal state after:
n : ℕ
α : Fin n → Sort u_1
m : ℕ
h : m ≤ n
v : (i : Fin n) → α i
i : Fin n
hi : ↑i ≥ m
x : α i
j : Fin m
⊢ ↑j ≠ ↑i
Module: Mathlib.Data.FinEnum.Option

Goal state before:
pp: case h_2
P : Type u → Sort v
finChoice : (n : ℕ) → Fin (n + 1)
congr : {α β : Type u} → (x : FinEnum α) → (x_1 : FinEnum β) → card β = card α → P α → P β
empty : P PEmpty.{u + 1}
option : {α : Type u} → FinEnum α → P α → P (Option α)
α : Type u
inst✝ : FinEnum α
h : 0 < card α
heq✝ : card α = (card α).pred.succ
⊢ (let fN := ULift.instFinEnum;
    have this := ⋯;
    congr (insertNone (ULift.{u, 0} (Fin (card α).pred)) ↑↑(finChoice (card α).pred)) inst✝ ⋯
      (option fN
        (recEmptyOption finChoice (fun {α β} ↦ congr) empty (fun {α} ↦ option) (ULift.{u, 0} (Fin (card α).pred))))) =
    congr (insertNone (ULift.{u, 0} (Fin (card α - 1))) ↑↑(finChoice (card α - 1))) inst✝ ⋯
      (option ULift.instFinEnum
        (recEmptyOption finChoice (fun {α β} ↦ congr) empty (fun {α} ↦ option) (ULift.{u, 0} (Fin (card α - 1)))))

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.List.Lookmap

Goal state before:
pp: case cons.none
α : Type u_1
f : α → Option α
acc : Array α
hd : α
tl : List α
⊢ acc.toList ++ ([hd] ++ lookmap f tl) = acc.toList ++ ([] ++ ([hd] ++ lookmap f tl))

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.List.AList

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a
s : AList β
⊢ a' ∈ (replace a b s).keys ↔ a' ∈ s

Tactic:
keys_replace,

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a
s : AList β
⊢ a' ∈ s.keys ↔ a' ∈ s
Module: Mathlib.Data.List.Lookmap

Goal state before:
pp: case trans
α : Type u_1
f : α → Option α
l₁ l₂ l₁✝ l₂✝ l₃✝ : List α
p₁ : l₁✝ ~ l₂✝
a✝ : l₂✝ ~ l₃✝
IH₁ : Pairwise (fun a b ↦ ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₁✝ → lookmap f l₁✝ ~ lookmap f l₂✝
IH₂ : Pairwise (fun a b ↦ ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₂✝ → lookmap f l₂✝ ~ lookmap f l₃✝
H : Pairwise (fun a b ↦ ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₁✝
⊢ ∀ {x y : α},
    (∀ (c : α), c ∈ f x → ∀ (d : α), d ∈ f y → x = y ∧ c = d) → ∀ (c : α), c ∈ f y → ∀ (d : α), d ∈ f x → y = x ∧ c = d

Tactic:
grind

Goal state after:
Module: Mathlib.Data.List.AList

Goal state before:
pp: case left
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : AList β
⊢ dlookup a s.entries = lookup a s

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.List.AList

Goal state before:
pp: case right
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : AList β
⊢ { entries := kerase a s.entries, nodupKeys := ⋯ } = erase a s

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
a : α
l : List (Sigma β)
h : a ∈ l.keys
this : ∃ a_1, a_1 ∈ l ∧ a_1.fst = a
⊢ ∃ b, ⟨a, b⟩ ∈ l

Tactic:
grind

Goal state after:
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
a : α
l : List (Sigma β)
⊢ ¬a ∈ l.keys ↔ ∀ (b : β a), ¬⟨a, b⟩ ∈ l

Tactic:
grind

Goal state after:
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
a : α
l : List (Sigma β)
⊢ ¬a ∈ l.keys ↔ ∀ (s : Sigma β), s ∈ l → a ≠ s.fst

Tactic:
grind

Goal state after:
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
s : Sigma β
l : List (Sigma β)
h : (s :: l).NodupKeys
⊢ ¬s.fst ∈ l.keys

Tactic:
grind

Goal state after:
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : Sigma β
tail✝ : List (Sigma β)
tail_ih✝ : (dlookup a tail✝).isSome = true ↔ a ∈ tail✝.keys
h✝ : a = s.fst
⊢ (dlookup a (s :: tail✝)).isSome = true ↔ a ∈ (s :: tail✝).keys

Tactic:
grind

Goal state after:
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : Sigma β
tail✝ : List (Sigma β)
tail_ih✝ : (dlookup a tail✝).isSome = true ↔ a ∈ tail✝.keys
h✝ : ¬a = s.fst
⊢ (dlookup a (s :: tail✝)).isSome = true ↔ a ∈ (s :: tail✝).keys

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: case mk
α : Type u
β : α → Type v
m : Multiset ((a : α) × β a)
l : List ((a : α) × β a)
⊢ (keys (Quot.mk (⇑(isSetoid ((a : α) × β a))) l)).Nodup ↔ NodupKeys (Quot.mk (⇑(isSetoid ((a : α) × β a))) l)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case nil
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
⊢ b ∈ dlookup a [] → ⟨a, b⟩ ∈ []

Tactic:
grind

Goal state after:
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s : Sigma β
tail✝ : List (Sigma β)
tail_ih✝ : b ∈ dlookup a tail✝ → ⟨a, b⟩ ∈ tail✝
h✝ : a = s.fst
⊢ b ∈ dlookup a (s :: tail✝) → ⟨a, b⟩ ∈ s :: tail✝

Tactic:
grind

Goal state after:
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s : Sigma β
tail✝ : List (Sigma β)
tail_ih✝ : b ∈ dlookup a tail✝ → ⟨a, b⟩ ∈ tail✝
h✝ : ¬a = s.fst
⊢ b ∈ dlookup a (s :: tail✝) → ⟨a, b⟩ ∈ s :: tail✝

Tactic:
grind

Goal state after:
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case nil
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
⊢ Option.map (Sigma.mk a) (dlookup a []) = find? (fun s ↦ decide (a = s.fst)) []

Tactic:
grind

Goal state after:
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : Sigma β
tail✝ : List (Sigma β)
tail_ih✝ : Option.map (Sigma.mk a) (dlookup a tail✝) = find? (fun s ↦ decide (a = s.fst)) tail✝
h✝ : s.fst = a
⊢ Option.map (Sigma.mk a) (dlookup a (s :: tail✝)) = find? (fun s ↦ decide (a = s.fst)) (s :: tail✝)

Tactic:
grind

Goal state after: