mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: case fs
n : ℕ
p : Prop
n✝ : ℕ
a✝ : Fin2 n✝
ih : ∀ {α : TypeVec.{u_1} n✝} {x : α a✝}, ofRepeat (TypeVec.const p α a✝ x) ↔ p
α : TypeVec.{u_1} (n✝ + 1)
x : α a✝.fs
⊢ ofRepeat
      ((match (motive := (x : ℕ) → (x_1 : TypeVec.{u_1} x) → (x_2 : Fin2 x) → x_1 x_2 → «repeat» x Prop x_2) n✝.succ, α,
          a✝.fs with
        | n.succ, α, a.fs => TypeVec.const p α.drop a
        | n.succ, x, Fin2.fz => fun x ↦ p)
        x) ↔
    p

Tactic:
]

Goal state after:
case fs
n : ℕ
p : Prop
n✝ : ℕ
a✝ : Fin2 n✝
ih : ∀ {α : TypeVec.{u_1} n✝} {x : α a✝}, ofRepeat (TypeVec.const p α a✝ x) ↔ p
α : TypeVec.{u_1} (n✝ + 1)
x : α a✝.fs
⊢ ofRepeat
      ((match (motive := (x : ℕ) → (x_1 : TypeVec.{u_1} x) → (x_2 : Fin2 x) → x_1 x_2 → «repeat» x Prop x_2) n✝.succ, α,
          a✝.fs with
        | n.succ, α, a.fs => TypeVec.const p α.drop a
        | n.succ, x, Fin2.fz => fun x ↦ p)
        x) ↔
    p
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
α β : TypeVec.{u_1} n
i : Fin2 n
a : α i
b : β i
⊢ prod.fst i (prod.mk i a b) = a

Tactic:
by
  induction i with
  | fz => simp_all only [prod.fst, prod.mk]
  | fs _ i_ih => apply i_ih

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

Goal state before:
pp: case refine_2
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
x : T
x✝ : ∃ i, (∀ (x_1 : S), ¬σ (Option.some i) x_1 = x) ∧ (π x).2 = ↑i
n : X
hn : ∀ (x_1 : S), ¬σ (Option.some n) x_1 = x
i : X
s : S
hn' : Option.some i = ↑n
h : σ (Option.some i) s = x
⊢ σ (Option.some n) s = x

Tactic:
]

Goal state after:
case refine_2
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
x : T
x✝ : ∃ i, (∀ (x_1 : S), ¬σ (Option.some i) x_1 = x) ∧ (π x).2 = ↑i
n : X
hn : ∀ (x_1 : S), ¬σ (Option.some n) x_1 = x
i : X
s : S
hn' : Option.some i = ↑n
h : σ (Option.some i) s = x
⊢ σ (Option.some n) s = x
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: case refine_2
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
x : T
x✝ : ∃ i, (∀ (x_1 : S), ¬σ (Option.some i) x_1 = x) ∧ (π x).2 = ↑i
n : X
hn : ∀ (x_1 : S), ¬σ (Option.some n) x_1 = x
i : X
s : S
hn' : Option.some i = ↑n
h : σ (Option.some i) s = x
⊢ σ (Option.some i) s = σ (Option.some i) s

Tactic:
]

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

Goal state before:
pp: S : Type u_1
T : Type u_2
X : Type u_3
inst✝⁵ : TopologicalSpace S
inst✝⁴ : TopologicalSpace T
inst✝³ : TopologicalSpace X
inst✝² : DiscreteTopology X
inst✝¹ : T2Space T
inst✝ : CompactSpace S
π : T → S × OnePoint X
hπ : Continuous π
σ : Option X → S → T
hσ : ∀ (x : Option X), Continuous (σ x)
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
⊢ IsOpen (⋃ i, (Set.range (σ (Option.some i)))ᶜ ∩ Prod.snd ∘ π ⁻¹' {↑i})

Tactic:
]

Goal state after:
S : Type u_1
T : Type u_2
X : Type u_3
inst✝⁵ : TopologicalSpace S
inst✝⁴ : TopologicalSpace T
inst✝³ : TopologicalSpace X
inst✝² : DiscreteTopology X
inst✝¹ : T2Space T
inst✝ : CompactSpace S
π : T → S × OnePoint X
hπ : Continuous π
σ : Option X → S → T
hσ : ∀ (x : Option X), Continuous (σ x)
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
⊢ IsOpen (⋃ i, (Set.range (σ (Option.some i)))ᶜ ∩ Prod.snd ∘ π ⁻¹' {↑i})
Module: Mathlib.Data.TypeVec

Goal state before:
pp: case fs
n n✝ : ℕ
a✝ : Fin2 n✝
i_ih : ∀ {α : TypeVec.{u_1} n✝} {x y : α a✝}, ofRepeat (α.repeatEq a✝ (prod.mk a✝ x y)) ↔ x = y
α : TypeVec.{u_1} (n✝ + 1)
x y : α a✝.fs
⊢ ofRepeat ((α.drop.repeatEq ::: uncurry Eq) a✝.fs (prod.mk a✝.fs x y)) ↔ x = y

Tactic:
]

Goal state after:
case fs
n n✝ : ℕ
a✝ : Fin2 n✝
i_ih : ∀ {α : TypeVec.{u_1} n✝} {x y : α a✝}, ofRepeat (α.repeatEq a✝ (prod.mk a✝ x y)) ↔ x = y
α : TypeVec.{u_1} (n✝ + 1)
x y : α a✝.fs
⊢ ofRepeat ((α.drop.repeatEq ::: uncurry Eq) a✝.fs (prod.mk a✝.fs x y)) ↔ x = y
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
X : (a : α) → Part (β a)
hX : f X ≤ X
⊢ ωSup (approxChain f) ≤ X

Tactic:
]

Goal state after:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
X : (a : α) → Part (β a)
hX : f X ≤ X
⊢ ωSup (approxChain f) ≤ X
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:
]

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

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

Tactic:
]

Goal state after:
α : Type u_1
β : α → Type u_2
g : ((a : α) → Part (β a)) → (a : α) → Part (β a)
hc : ωScottContinuous g
⊢ ωSup (approxChain { toFun := g, monotone' := ⋯ }) =
    ωSup ((approxChain { toFun := g, monotone' := ⋯ }).map { toFun := g, monotone' := ⋯ })
Module: Mathlib.Control.LawfulFix

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

Tactic:
]

Goal state after:
α : Type u_1
f : Part α → Part α
hc : ωScottContinuous f
x✝ : Chain (Unit → Part α)
⊢ ωSup ((x✝.map (Pi.evalOrderHom PUnit.unit)).map { toFun := f, monotone' := ⋯ }) =
    Part.ωSup ((x✝.map (toUnitMono { toFun := f, monotone' := ⋯ })).map (Pi.evalOrderHom PUnit.unit))
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:
]

Goal state after:
α : 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))
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:
]

Goal state after:
α : 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)
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:
]

Goal state after:
α : 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 α β γ)))
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:
]

Goal state after:
α : 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 α β γ)))
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
α : TypeVec.{u_1} n
β : TypeVec.{u_2} n
p : α ⟹ «repeat» n Prop
f : β ⟹ Subtype_ p
⊢ id ⊚ f = f

Tactic:
]

Goal state after:
n : ℕ
α : TypeVec.{u_1} n
β : TypeVec.{u_2} n
p : α ⟹ «repeat» n Prop
f : β ⟹ Subtype_ p
⊢ id ⊚ f = f
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:
]

Goal state after:
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✝
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:
]

Goal state after:
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✝
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
x : t' α
⊢ pure x = pure x

Tactic:
]

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
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β γ : Type u
f : β → F γ
g : α → G β
x : t' α
⊢ Comp.mk ((fun x ↦ ⇑(eqv γ) <$> x) <$> traverse f <$> traverse g ((eqv α).symm x)) =
    Comp.mk (Equiv.traverse eqv f <$> Equiv.traverse eqv g x)

Tactic:
]

Goal state after:
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β γ : Type u
f : β → F γ
g : α → G β
x : t' α
⊢ Comp.mk ((fun x ↦ ⇑(eqv γ) <$> x) <$> traverse f <$> traverse g ((eqv α).symm x)) =
    Comp.mk (Equiv.traverse eqv f <$> Equiv.traverse eqv g x)
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: S : Type u_1
T : Type u_2
X : Type u_3
inst✝⁵ : TopologicalSpace S
inst✝⁴ : T2Space S
inst✝³ : TopologicalSpace T
inst✝² : CompactSpace T
inst✝¹ : TopologicalSpace X
inst✝ : T1Space (OnePoint X)
π : T → S × OnePoint X
hπ : Continuous π
⊢ IsCompact (⋂ n, ⋂ m, {x | (π ↑(x n)).1 = (π ↑(x m)).1})

Tactic:
]

Goal state after:
S : Type u_1
T : Type u_2
X : Type u_3
inst✝⁵ : TopologicalSpace S
inst✝⁴ : T2Space S
inst✝³ : TopologicalSpace T
inst✝² : CompactSpace T
inst✝¹ : TopologicalSpace X
inst✝ : T1Space (OnePoint X)
π : T → S × OnePoint X
hπ : Continuous π
⊢ IsCompact (⋂ n, ⋂ m, {x | (π ↑(x n)).1 = (π ↑(x m)).1})
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
inst✝ : Traversable t'
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
h₂ :
  ∀ {F : Type u → Type u} [inst : Applicative F] [LawfulApplicative F] {α β : Type u} (f : α → F β),
    traverse f = Equiv.traverse eqv f
α✝ : Type u
x✝ : t' α✝
⊢ pure x✝ = pure x✝

Tactic:
]

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
inst✝⁴ : Traversable t'
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
h₂ :
  ∀ {F : Type u → Type u} [inst : Applicative F] [LawfulApplicative F] {α β : Type u} (f : α → F β),
    traverse f = Equiv.traverse eqv f
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ β✝ γ✝ : Type u
x✝² : β✝ → F✝ γ✝
x✝¹ : α✝ → G✝ β✝
x✝ : t' α✝
⊢ Comp.mk (Equiv.traverse eqv x✝² <$> Equiv.traverse eqv x✝¹ x✝) = Comp.mk (Equiv.traverse eqv x✝² <$> traverse x✝¹ x✝)

Tactic:
]

Goal state after:
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝⁶ : Traversable t
inst✝⁵ : LawfulTraversable t
inst✝⁴ : Traversable t'
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
h₂ :
  ∀ {F : Type u → Type u} [inst : Applicative F] [LawfulApplicative F] {α β : Type u} (f : α → F β),
    traverse f = Equiv.traverse eqv f
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ β✝ γ✝ : Type u
x✝² : β✝ → F✝ γ✝
x✝¹ : α✝ → G✝ β✝
x✝ : t' α✝
⊢ Comp.mk (Equiv.traverse eqv x✝² <$> Equiv.traverse eqv x✝¹ x✝) = Comp.mk (Equiv.traverse eqv x✝² <$> traverse x✝¹ x✝)
Module: Mathlib.Control.Traversable.Equiv

Goal state before:
pp: case e_a
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝⁶ : Traversable t
inst✝⁵ : LawfulTraversable t
inst✝⁴ : Traversable t'
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
h₂ :
  ∀ {F : Type u → Type u} [inst : Applicative F] [LawfulApplicative F] {α β : Type u} (f : α → F β),
    traverse f = Equiv.traverse eqv f
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ β✝ γ✝ : Type u
x✝² : β✝ → F✝ γ✝
x✝¹ : α✝ → G✝ β✝
x✝ : t' α✝
⊢ Equiv.traverse eqv x✝¹ x✝ = Equiv.traverse eqv x✝¹ x✝

Tactic:
]

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
inst✝ : Traversable t'
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
h₂ :
  ∀ {F : Type u → Type u} [inst : Applicative F] [LawfulApplicative F] {α β : Type u} (f : α → F β),
    traverse f = Equiv.traverse eqv f
α✝ β✝ : Type u
x✝¹ : α✝ → β✝
x✝ : t' α✝
⊢ pure (Equiv.map eqv x✝¹ x✝) = pure (Equiv.map eqv x✝¹ x✝)

Tactic:
]

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
inst✝⁴ : Traversable t'
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
h₂ :
  ∀ {F : Type u → Type u} [inst : Applicative F] [LawfulApplicative F] {α β : Type u} (f : α → F β),
    traverse f = Equiv.traverse eqv f
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
x✝⁴ : ApplicativeTransformation F✝ G✝
x✝³ x✝² : Type u
x✝¹ : x✝³ → F✝ x✝²
x✝ : t' x✝³
⊢ Equiv.traverse eqv ((fun {α} ↦ x✝⁴.app α) ∘ x✝¹) x✝ = Equiv.traverse eqv ((fun {α} ↦ x✝⁴.app α) ∘ x✝¹) x✝

Tactic:
]

Goal state after:
Module: Mathlib.Data.BitVec

Goal state before:
pp: z : ℤ
w : ℕ
⊢ (max (z % 2 ^ (w + 1)) 0).bmod (2 ^ (w + 1)) = z.bmod (2 ^ (w + 1))

Tactic:
]

Goal state after:
z : ℤ
w : ℕ
⊢ (max (z % 2 ^ (w + 1)) 0).bmod (2 ^ (w + 1)) = z.bmod (2 ^ (w + 1))
Module: Mathlib.Data.BitVec

Goal state before:
pp: z : ℤ
w : ℕ
⊢ (z % 2 ^ (w + 1)).bmod (2 ^ (w + 1)) = z.bmod (2 ^ (w + 1))

pp: z : ℤ
w : ℕ
⊢ 0 ≤ z % 2 ^ (w + 1)

Tactic:
]

Goal state after:
z : ℤ
w : ℕ
⊢ (z % 2 ^ (w + 1)).bmod (2 ^ (w + 1)) = z.bmod (2 ^ (w + 1))

z : ℤ
w : ℕ
⊢ 0 ≤ z % 2 ^ (w + 1)
Module: Mathlib.Data.BitVec

Goal state before:
pp: z : ℤ
w : ℕ
h : 2 ^ (w + 1) = ↑(2 ^ (w + 1))
⊢ z.bmod (2 ^ (w + 1)) = z.bmod (2 ^ (w + 1))

Tactic:
]

Goal state after:
Module: Mathlib.Data.BitVec

Goal state before:
pp: w : ℕ
z : ℤ
⊢ { toFin := ↑z }.toFin = ↑z

Tactic:
]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
m : α → β
f : Filter α
F : f.Realizer
x✝ : Set β
⊢ (∃ b, F.F.f b ⊆ m ⁻¹' x✝) ↔ ∃ b, F.F.f b ⊆ m ⁻¹' x✝

Tactic:
]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
m : α → β
f : Filter β
F : f.Realizer
x✝ : Set α
⊢ x✝ ∈ { f := fun s ↦ m ⁻¹' F.F.f s, pt := F.F.pt, inf := F.F.inf, inf_le_left := ⋯, inf_le_right := ⋯ }.toFilter.sets ↔
    x✝ ∈ (comap m f).sets

Tactic:
cases F; subst f
      exact ⟨fun ⟨s, h⟩ ↦ ⟨_, ⟨s, Subset.refl _⟩, h⟩,
        fun ⟨_, ⟨s, h⟩, h₂⟩ ↦ ⟨s, Subset.trans (preimage_mono h) h₂⟩⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
m : α → β
f : Filter β
F : f.Realizer
x✝ : Set α
⊢ x✝ ∈ { f := fun s ↦ m ⁻¹' F.F.f s, pt := F.F.pt, inf := F.F.inf, inf_le_left := ⋯, inf_le_right := ⋯ }.toFilter.sets ↔
    x✝ ∈ (comap m f).sets

Tactic:
by
      cases F; subst f
      exact ⟨fun ⟨s, h⟩ ↦ ⟨_, ⟨s, Subset.refl _⟩, h⟩,
        fun ⟨_, ⟨s, h⟩, h₂⟩ ↦ ⟨s, Subset.trans (preimage_mono h) h₂⟩⟩

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

Goal state before:
pp: α : Type u_1
T : TopologicalSpace α
F : Realizer α
this : TopologicalSpace.IsTopologicalBasis (range F.F.f)
⊢ TopologicalSpace.IsTopologicalBasis (range F.F.f)

Tactic:
]

Goal state after:
α : Type u_1
T : TopologicalSpace α
F : Realizer α
this : TopologicalSpace.IsTopologicalBasis (range F.F.f)
⊢ TopologicalSpace.IsTopologicalBasis (range F.F.f)
Module: Mathlib.Data.Analysis.Topology

Goal state before:
pp: α : Type u_1
T : TopologicalSpace α
F : Realizer α
s : Set α
a : α
this : s ∈ 𝓝 a ↔ ∃ b, a ∈ F.F.f b ∧ F.F.f b ⊆ s
⊢ s ∈ 𝓝 a ↔ ∃ b, a ∈ F.F.f b ∧ F.F.f b ⊆ s

Tactic:
]

Goal state after:
α : Type u_1
T : TopologicalSpace α
F : Realizer α
s : Set α
a : α
this : s ∈ 𝓝 a ↔ ∃ b, a ∈ F.F.f b ∧ F.F.f b ⊆ s
⊢ s ∈ 𝓝 a ↔ ∃ b, a ∈ F.F.f b ∧ F.F.f b ⊆ s
Module: Mathlib.Data.Analysis.Topology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
F : Realizer α
s : Set α
a : α
this : (a : Prop) → Decidable a
⊢ (¬∃ b, a ∈ F.F.f b ∧ ∀ z ∈ F.F.f b, z ∉ s) → a ∈ s ↔ (∀ (b : F.σ), a ∈ F.F.f b → ∃ z, z ∈ F.F.f b ∩ s) → a ∈ s

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
F : Realizer α
s : Set α
a : α
this : (a : Prop) → Decidable a
⊢ (¬∃ b, a ∈ F.F.f b ∧ ∀ z ∈ F.F.f b, z ∉ s) → a ∈ s ↔ (∀ (b : F.σ), a ∈ F.F.f b → ∃ z, z ∈ F.F.f b ∩ s) → a ∈ s
Module: Mathlib.Data.Analysis.Topology

Goal state before:
pp: α : Type u_1
T : TopologicalSpace α
σ : Type u_5
F : Ctop α σ
H : ∀ (a : α) (s : Set α), s ∈ 𝓝 a ↔ ∃ b, a ∈ F.f b ∧ F.f b ⊆ s
x : α
s : Set α
⊢ (∃ b, x ∈ F.f b ∧ F.f b ⊆ s) ↔ ∃ b, x ∈ F.f b ∧ F.f b ⊆ s

Tactic:
]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
inst✝ : TopologicalSpace α
f : Filter α
F : f.Realizer
x : F.σ
h : f ≠ ⊥
hF : F.F.f x ⊆ ∅
⊢ F.F.toFilter ≤ ⊥

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
inst✝ : TopologicalSpace α
f : Filter α
F : f.Realizer
x : F.σ
h : f ≠ ⊥
hF : F.F.f x ⊆ ∅
⊢ F.F.toFilter ≤ ⊥
Module: Mathlib.Data.Analysis.Filter

Goal state before:
pp: α : Type u_1
f : Filter α
F : f.Realizer
⊢ (∃ x, ¬(F.F.f x).Nonempty) ↔ ∀ (b : Realizer.bot.σ), ∃ a, F.F.f a ⊆ Realizer.bot.F.f b

Tactic:
]

Goal state after:
α : Type u_1
f : Filter α
F : f.Realizer
⊢ (∃ x, ¬(F.F.f x).Nonempty) ↔ ∀ (b : Realizer.bot.σ), ∃ a, F.F.f a ⊆ Realizer.bot.F.f b
Module: Mathlib.Data.DFinsupp.Interval

Goal state before:
pp: case refine_1
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
t : (i : ι) → Finset (α i)
inst✝ : (i : ι) → DecidableEq (α i)
f : (a : ι) → a ∈ s → α a
hf : f ∈ s.pi t
⊢ (DFinsupp.mk s fun i ↦ f ↑i ⋯).support ⊆ s ∧ ∀ i ∈ s, (DFinsupp.mk s fun i ↦ f ↑i ⋯) i ∈ t i

Tactic:
]

Goal state after:
case refine_1
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
t : (i : ι) → Finset (α i)
inst✝ : (i : ι) → DecidableEq (α i)
f : (a : ι) → a ∈ s → α a
hf : f ∈ s.pi t
⊢ (DFinsupp.mk s fun i ↦ f ↑i ⋯).support ⊆ s ∧ ∀ i ∈ s, (DFinsupp.mk s fun i ↦ f ↑i ⋯) i ∈ t i
Module: Mathlib.Data.DFinsupp.Interval

Goal state before:
pp: case neg
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
f : Π₀ (i : ι), α i
inst✝ : (i : ι) → DecidableEq (α i)
t : Π₀ (i : ι), Finset (α i)
ht : t.support ⊆ s
i : ι
h : (i ∈ f.support → i ∈ s) ∧ (i ∈ s → f i ∈ t i)
hi : i ∉ s
⊢ 0 ∈ 0

Tactic:
]

Goal state after:
case neg
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
f : Π₀ (i : ι), α i
inst✝ : (i : ι) → DecidableEq (α i)
t : Π₀ (i : ι), Finset (α i)
ht : t.support ⊆ s
i : ι
h : (i ∈ f.support → i ∈ s) ∧ (i ∈ s → f i ∈ t i)
hi : i ∉ s
⊢ 0 ∈ 0
Module: Mathlib.Data.DFinsupp.Interval

Goal state before:
pp: case refine_2
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
f : Π₀ (i : ι), α i
inst✝ : (i : ι) → DecidableEq (α i)
t : Π₀ (i : ι), Finset (α i)
ht : t.support ⊆ s
i : ι
h : f i = 0
hi : i ∈ f.support
H : t i = 0
⊢ f i = 0

Tactic:
]

Goal state after:
case refine_2
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
f : Π₀ (i : ι), α i
inst✝ : (i : ι) → DecidableEq (α i)
t : Π₀ (i : ι), Finset (α i)
ht : t.support ⊆ s
i : ι
h : f i = 0
hi : i ∈ f.support
H : t i = 0
⊢ f i = 0
Module: Mathlib.Data.Bool.Count

Goal state before:
pp: l : List Bool
hl : IsChain (fun x1 x2 ↦ x1 ≠ x2) l
h2 : Even l.length
b : Bool
⊢ count b l + count b l = count b l + count b l

Tactic:
]

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

Goal state before:
pp: case pos
l : List Bool
hl : IsChain (fun x1 x2 ↦ x1 ≠ x2) l
b : Bool
h2 : Even l.length
⊢ l.length = l.length

Tactic:
]

Goal state after: