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

Goal state before:
pp: s : Type u₀
s' : Type u₁
r : Type u_1
r' : Type u_2
w : Type u_3
w' : Type u_4
ε : Type u₀
α✝ : Type v₁
β✝ : Type v₂
e : α✝ ≃ β✝
f : Except ε α✝
⊢ Except.map (⇑e.symm) (Except.map (⇑e) f) = f

Tactic:
by

Goal state after:
Module: Mathlib.Control.ULiftable

Goal state before:
pp: s : Type u₀
s' : Type u₁
r : Type u_1
r' : Type u_2
w : Type u_3
w' : Type u_4
ε : Type u₀
α✝ : Type v₁
β✝ : Type v₂
e : α✝ ≃ β✝
f : Except ε β✝
⊢ Except.map (⇑e) (Except.map (⇑e.symm) f) = f

Tactic:
by

Goal state after:
Module: Mathlib.Control.ULiftable

Goal state before:
pp: s : Type u₀
s' : Type u₁
r : Type u_1
r' : Type u_2
w : Type u_3
w' : Type u_4
α✝ : Type u₀
β✝ : Type u₁
e : α✝ ≃ β✝
f : Option α✝
⊢ Option.map (⇑e.symm) (Option.map (⇑e) f) = f

Tactic:
by

Goal state after:
Module: Mathlib.Control.ULiftable

Goal state before:
pp: s : Type u₀
s' : Type u₁
r : Type u_1
r' : Type u_2
w : Type u_3
w' : Type u_4
α✝ : Type u₀
β✝ : Type u₁
e : α✝ ≃ β✝
f : Option β✝
⊢ Option.map (⇑e) (Option.map (⇑e.symm) f) = f

Tactic:
by

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)).2 = x
⊢ (fibres π σ)ᶜ = ⋃ i, (Set.range (σ (Option.some i)))ᶜ ∩ Prod.snd ∘ π ⁻¹' {↑i}

Tactic:
by

Goal state after:
Module: Mathlib.Data.TypeVec

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

Tactic:
by

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
α : TypeVec.{u_1} n
⊢ prod.fst ⊚ prod.diag = id

Tactic:
by

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
α : TypeVec.{u_1} n
⊢ prod.snd ⊚ prod.diag = id

Tactic:
by

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
i : X
h : ∞ ∈ {↑i}
⊢ IsCompact (OnePoint.some ⁻¹' {↑i})ᶜ

Tactic:
by

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
i : X
⊢ IsOpen (OnePoint.some ⁻¹' {↑i})

Tactic:
by

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)
⊢ Part.fix ⇑f = ωSup (approxChain f)

Tactic:
by

Goal state after:
Module: Mathlib.Data.TypeVec

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

Tactic:
by

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 (fibres π σ)ᶜ

Tactic:
by

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n✝¹ n : ℕ
α✝ : TypeVec.{u} n
p✝ : α✝ ⊗ α✝ ⟹ «repeat» n Prop
n✝ : ℕ
α : TypeVec.{u} (n✝ + 1)
p : α ⊗ α ⟹ «repeat» (n✝ + 1) Prop
x : (fun i ↦ { x // ofRepeat (p i (prod.mk i x.1 x.2)) }) Fin2.fz
⊢ ofRepeat (p Fin2.fz (prod.mk Fin2.fz (↑x).1 (↑x).2)) = p Fin2.fz ↑x

Tactic:
by

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n✝¹ n : ℕ
α✝ : TypeVec.{u} n
p✝ : α✝ ⊗ α✝ ⟹ «repeat» n Prop
n✝ : ℕ
α : TypeVec.{u} (n✝ + 1)
p : α ⊗ α ⟹ «repeat» (n✝ + 1) Prop
x : Subtype_ p Fin2.fz
⊢ p Fin2.fz ↑x = ofRepeat (p Fin2.fz (prod.mk Fin2.fz (↑x).1 (↑x).2))

Tactic:
by

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: α : TypeVec.{u} 0
ps : α ⟹ «repeat» 0 Prop
⊢ ∀ (x : Fin2 0), subtypeVal ps x = nilFun x

Tactic:
by

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:
by

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
α : TypeVec.{u} n
⊢ subtypeVal α.repeatEq ⊚ diagSub = prod.diag

Tactic:
by

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
⊢ σ (Option.some x) s ∈ fibres π σ

Tactic:
by

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 : (a : α) → Part (β a)
hX : f X ≤ X
⊢ Part.fix ⇑f ≤ X

Tactic:
by

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:
by

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 = ωSup (approxChain { toFun := g, monotone' := ⋯ })

Tactic:
by

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:
by

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: ⊢ ∀ {n : ℕ} {α β : TypeVec.{u} n}, (id ⊗' id) = id

Tactic:
by

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
⊢ Function.Surjective fun x ↦ π ↑x

Tactic:
by

Goal state after:
Module: Mathlib.Data.TypeVec

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

Tactic:
by

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 = g (Part.fix g)

Tactic:
by

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:
by

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:
by

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:
by

Goal state after:
Module: Mathlib.Control.LawfulFix

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

Tactic:
by

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:
by

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
α : TypeVec.{u_1} n
p : α ⟹ «repeat» n Prop
⊢ toSubtype p ⊚ ofSubtype p = id

Tactic:
by

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)
⊢ (monotoneCurry α β γ) (ωSup c) = ωSup (c.map (monotoneCurry α β γ))

Tactic:
by

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

Goal state before:
pp: t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝¹ : Functor t
inst✝ : LawfulFunctor t
α : Type u
x : t' α
⊢ Equiv.map eqv id x = x

Tactic:
by

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

Goal state before:
pp: t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝¹ : Functor t
inst✝ : LawfulFunctor t
α β γ : Type u
g : α → β
h : β → γ
x : t' α
⊢ Equiv.map eqv (h ∘ g) x = Equiv.map eqv h (Equiv.map eqv g x)

Tactic:
by

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:
by

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
α : TypeVec.{u_1} n
p : α ⟹ «repeat» n Prop
⊢ subtypeVal p ⊚ toSubtype p = fun x ↦ Subtype.val

Tactic:
by

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:
by

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)
⊢ (monotoneUncurry α β γ) (ωSup c) = ωSup (c.map (monotoneUncurry α β γ))

Tactic:
by

Goal state after:
Module: Mathlib.Data.TypeVec

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

Tactic:
by

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
⊢ Function.Surjective (coverToFun (fibreIncl π σ) (π_r π σ))

Tactic:
by

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:
by

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:
by

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

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

Tactic:
by

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
π : T → S × OnePoint X
hπ : Continuous π
⊢ Continuous Subtype.val

Tactic:
by

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

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

Tactic:
by

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
x : t' α
⊢ Equiv.traverse eqv pure x = pure x

Tactic:
by

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
⊢ fix _f = _f (fix _f)

Tactic:
by

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' α
⊢ Equiv.traverse eqv (pure ∘ f) x = pure (Equiv.map eqv f x)

Tactic:
by

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:
by

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:
by

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:
by

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
α : TypeVec.{u_1} n
r : α ⊗ α ⟹ «repeat» n Prop
⊢ toSubtype' r ⊚ ofSubtype' r = id

Tactic:
by

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 π
⊢ Function.Surjective (y π)

Tactic:
by

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✝⁴ : T2Space S
inst✝³ : TopologicalSpace T
inst✝² : CompactSpace T
inst✝¹ : TopologicalSpace X
inst✝ : T1Space (OnePoint X)
π : T → S × OnePoint X
hπ : Continuous π
x : OnePoint X
⊢ Continuous (Prod.snd ∘ π)

Tactic:
by

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' α
⊢ Equiv.traverse eqv (Comp.mk ∘ map f ∘ g) x = Comp.mk (Equiv.traverse eqv f <$> Equiv.traverse eqv g x)

Tactic:
by

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✝⁴ : T2Space S
inst✝³ : TopologicalSpace T
inst✝² : CompactSpace T
inst✝¹ : TopologicalSpace X
inst✝ : T1Space (OnePoint X)
π : T → S × OnePoint X
hπ : Continuous π
⊢ CompactSpace ↑(S' π)

Tactic:
by

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
η : ApplicativeTransformation F G
α β : Type u
f : α → F β
x : t' α
⊢ (fun {α} ↦ η.app α) (Equiv.traverse eqv f x) = Equiv.traverse eqv ((fun {α} ↦ η.app α) ∘ f) x

Tactic:
by

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

Goal state before:
pp: R : Type
inst✝ : CommRing R
S T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
⊢ Continuous (coverToFun (⇑(LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞})).hom.hom') π.hom.hom'.1)

Tactic:
by

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

Tactic:
by

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
α : TypeVec.{u_1} n
r : α ⊗ α ⟹ «repeat» n Prop
⊢ subtypeVal r ⊚ toSubtype' r = fun i x ↦ prod.mk i (↑x).1 (↑x).2

Tactic:
by

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' α✝
⊢ traverse (Comp.mk ∘ map x✝² ∘ x✝¹) x✝ = Comp.mk (traverse x✝² <$> traverse x✝¹ x✝)

Tactic:
by

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' α✝
⊢ traverse (pure ∘ x✝¹) x✝ = pure (x✝¹ <$> x✝)

Tactic:
by

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✝³
⊢ (fun {α} ↦ x✝⁴.app α) (traverse x✝¹ x✝) = traverse ((fun {α} ↦ x✝⁴.app α) ∘ x✝¹) x✝

Tactic:
by

Goal state after:
Module: Mathlib.Data.BitVec

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

Tactic:
by

Goal state after:
Module: Mathlib.Data.BitVec

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

Tactic:
by

Goal state after:
Module: Mathlib.Data.BitVec

Goal state before:
pp: w : ℕ
z : ℤ
⊢ (↑z).toFin = ↑z

Tactic:
by

Goal state after:
Module: Mathlib.Data.BitVec

Goal state before:
pp: w n : ℕ
x : BitVec w
⊢ (↑n).toFin * x.toFin = n • x.toFin

Tactic:
by

Goal state after:
Module: Mathlib.Data.BitVec

Goal state before:
pp: w : ℕ
z : ℤ
x : BitVec w
⊢ (↑z).toFin * x.toFin = z • x.toFin

Tactic:
by

Goal state after:
Module: Mathlib.Data.BitVec

Goal state before:
pp: w : ℕ
x : BitVec w
n : ℕ
⊢ (x ^ n).toFin = x.toFin ^ n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
inst✝ : PartialOrder α
F : CFilter α σ
E : σ ≃ τ
f : σ → α
p : σ
g : σ → σ → σ
h₁ : ∀ (a b : σ), f (g a b) ≤ f a
h₂ : ∀ (a b : σ), f (g a b) ≤ f b
a b : τ
⊢ f (E.symm (E (g (E.symm a) (E.symm b)))) ≤ f (E.symm a)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
inst✝ : PartialOrder α
F : CFilter α σ
E : σ ≃ τ
f : σ → α
p : σ
g : σ → σ → σ
h₁ : ∀ (a b : σ), f (g a b) ≤ f a
h₂ : ∀ (a b : σ), f (g a b) ≤ f b
a b : τ
⊢ f (E.symm (E (g (E.symm a) (E.symm b)))) ≤ f (E.symm b)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
σ : Type u_3
τ : Type u_4
inst✝ : PartialOrder α
E : σ ≃ τ
F : CFilter α σ
a : τ
⊢ (ofEquiv E F).f a = F.f (E.symm a)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
f : Filter α
F : f.Realizer
a : Set α
⊢ a ∈ f ↔ ∃ b, F.F.f b ⊆ a

Tactic:
by

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 α
x✝ : Set α
⊢ x✝ ∈
      { f := Subtype.val, pt := ⟨univ, ⋯⟩,
            inf := fun x x_1 ↦
              match x with
              | ⟨val, h₁⟩ =>
                match x_1 with
                | ⟨val_1, h₂⟩ => ⟨val ∩ val_1, ⋯⟩,
            inf_le_left := ⋯, inf_le_right := ⋯ }.toFilter.sets ↔
    x✝ ∈ f.sets

Tactic:
by

Goal state after: