mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: S : Profinite
F : Profiniteᵒᵖ ⥤ Type (u + 1)
hF : (S : Profinite) → IsColimit (F.mapCocone S.asLimitCone.op)
X✝ Y✝ : Profiniteᵒᵖ
x✝ : X✝ ⟶ Y✝
⊢ (lanPresheaf F).map x✝ ≫
      (match Y✝ with
        | Opposite.op S => lanPresheafIso (hF S)).hom =
    (match X✝ with
        | Opposite.op S => lanPresheafIso (hF S)).hom ≫
      F.map x✝

Tactic:
simpa using

Goal state after:
S : Profinite
F : Profiniteᵒᵖ ⥤ Type (u + 1)
hF : (S : Profinite) → IsColimit (F.mapCocone S.asLimitCone.op)
X✝ Y✝ : Profiniteᵒᵖ
x✝ : X✝ ⟶ Y✝
⊢ colimit.desc (CostructuredArrow.proj toProfinite.op X✝ ⋙ toProfinite.op ⋙ F)
        { pt := colimit (CostructuredArrow.proj toProfinite.op Y✝ ⋙ toProfinite.op ⋙ F),
          ι :=
            {
              app := fun g ↦
                colimit.ι (CostructuredArrow.proj toProfinite.op Y✝ ⋙ toProfinite.op ⋙ F)
                  ((CostructuredArrow.map x✝).obj g),
              naturality := ⋯ } } ≫
      colimit.desc (CostructuredArrow.proj toProfinite.op Y✝ ⋙ toProfinite.op ⋙ F)
        (Profinite.Extend.cocone F (Opposite.unop Y✝)) =
    colimit.desc (CostructuredArrow.proj toProfinite.op X✝ ⋙ toProfinite.op ⋙ F)
        (Profinite.Extend.cocone F (Opposite.unop X✝)) ≫
      F.map x✝
Module: Mathlib.Condensed.Light.InternallyProjective

Goal state before:
pp: case e_6
R : Type u
inst✝ : CommRing R
A B P : LightCondMod R
S : LightProfinite
e : A ⟶ B
x : ↑((P ⟹ A).obj.obj (Opposite.op S))
⊢ (coherentTopology LightProfinite).yonedaEquiv
      ((coherentTopology LightProfinite).yonedaEquiv.symm
        ((ConcreteCategory.hom (((ihom P).map e).hom.app (Opposite.op S))) x)) =
    (coherentTopology LightProfinite).yonedaEquiv
      ((coherentTopology LightProfinite).yonedaEquiv.symm x ≫ (forget R).map ((ihom P).map e))

Tactic:
simp [dsimp% GrothendieckTopology.yonedaEquiv_comp]

Goal state after:
Module: Mathlib.Topology.Category.LightProfinite.Injective

Goal state before:
pp: case refine_2
X : Type u_1
Y : Type u_2
S : Type u_3
T : Type u_4
inst✝¹⁰ : TopologicalSpace X
inst✝⁹ : CompactSpace X
inst✝⁸ : TopologicalSpace Y
inst✝⁷ : CompactSpace Y
inst✝⁶ : T2Space Y
inst✝⁵ : TotallyDisconnectedSpace Y
inst✝⁴ : TopologicalSpace S
inst✝³ : T2Space S
inst✝² : Finite S
inst✝¹ : TopologicalSpace T
inst✝ : T2Space T
f : X → Y
hf : Continuous[inst✝¹⁰, inst✝⁸] f
f_inj : Function.Injective f
f' : S → T
f'_surj : Function.Surjective f'
g : X → S
hg : Continuous[inst✝¹⁰, inst✝⁴] g
g' : Y → T
hg' : Continuous[inst✝⁸, inst✝¹] g'
h_comm : g' ∘ f = f' ∘ g
this : Finite T
Z : S → Set Y := fun i ↦ f '' g ⁻¹' {i}
Z_closed : ∀ (i : S), IsClosed[inst✝⁸] (Z i)
Z_disj : univ.PairwiseDisjoint Z
D : S → Set Y := fun i ↦ g' ⁻¹' {f' i}
D_clopen : ∀ (i : S), IsClopen (D i)
Z_subset_D : ∀ (i : S), Z i ⊆ D i
C : S → Set Y
C_clopen : ∀ (i : S), IsClopen (C i)
Z_subset_C : ∀ (i : S), Z i ⊆ C i
C_subset_D : ∀ (i : S), C i ⊆ D i
C_cover_D : ⋃ i, D i ⊆ ⋃ i, C i
C_disj : univ.PairwiseDisjoint C
D_cover_univ : univ ⊆ ⋃ i, D i
C_cover_univ : ⋃ i, C i = univ
h_glue : ∀ (i j : S), ∀ x ∈ C i, x ∈ C j → i = j
y : Y
hy : y ∈ ⋃ i, C i
i : S
hi : y ∈ C i
⊢ (f' ∘ liftCover C (fun i x ↦ i) h_glue C_cover_univ) y = g' y

Tactic:
simpa using

Goal state after:
case refine_2
X : Type u_1
Y : Type u_2
S : Type u_3
T : Type u_4
inst✝¹⁰ : TopologicalSpace X
inst✝⁹ : CompactSpace X
inst✝⁸ : TopologicalSpace Y
inst✝⁷ : CompactSpace Y
inst✝⁶ : T2Space Y
inst✝⁵ : TotallyDisconnectedSpace Y
inst✝⁴ : TopologicalSpace S
inst✝³ : T2Space S
inst✝² : Finite S
inst✝¹ : TopologicalSpace T
inst✝ : T2Space T
f : X → Y
hf : Continuous[inst✝¹⁰, inst✝⁸] f
f_inj : Function.Injective f
f' : S → T
f'_surj : Function.Surjective f'
g : X → S
hg : Continuous[inst✝¹⁰, inst✝⁴] g
g' : Y → T
hg' : Continuous[inst✝⁸, inst✝¹] g'
h_comm : g' ∘ f = f' ∘ g
this : Finite T
Z : S → Set Y := fun i ↦ f '' g ⁻¹' {i}
Z_closed : ∀ (i : S), IsClosed[inst✝⁸] (Z i)
Z_disj : univ.PairwiseDisjoint Z
D : S → Set Y := fun i ↦ g' ⁻¹' {f' i}
D_clopen : ∀ (i : S), IsClopen (D i)
Z_subset_D : ∀ (i : S), Z i ⊆ D i
C : S → Set Y
C_clopen : ∀ (i : S), IsClopen (C i)
Z_subset_C : ∀ (i : S), Z i ⊆ C i
C_subset_D : ∀ (i : S), C i ⊆ D i
C_cover_D : ⋃ i, D i ⊆ ⋃ i, C i
C_disj : univ.PairwiseDisjoint C
D_cover_univ : univ ⊆ ⋃ i, D i
C_cover_univ : ⋃ i, C i = univ
h_glue : ∀ (i j : S), ∀ x ∈ C i, x ∈ C j → i = j
y : Y
hy : y ∈ ⋃ i, C i
i : S
hi : y ∈ C i
⊢ f' i = g' y
Module: Mathlib.Topology.Category.LightProfinite.Injective

Goal state before:
pp: X : Type u_1
Y : Type u_2
S : Type u_3
T : Type u_4
inst✝¹⁰ : TopologicalSpace X
inst✝⁹ : CompactSpace X
inst✝⁸ : TopologicalSpace Y
inst✝⁷ : CompactSpace Y
inst✝⁶ : T2Space Y
inst✝⁵ : TotallyDisconnectedSpace Y
inst✝⁴ : TopologicalSpace S
inst✝³ : T2Space S
inst✝² : Finite S
inst✝¹ : TopologicalSpace T
inst✝ : T2Space T
f : X → Y
hf : Continuous[inst✝¹⁰, inst✝⁸] f
f_inj : Function.Injective f
f' : S → T
f'_surj : Function.Surjective f'
g : X → S
hg : Continuous[inst✝¹⁰, inst✝⁴] g
g' : Y → T
hg' : Continuous[inst✝⁸, inst✝¹] g'
h_comm : g' ∘ f = f' ∘ g
this : Finite T
Z : S → Set Y := fun i ↦ f '' g ⁻¹' {i}
Z_closed : ∀ (i : S), IsClosed[inst✝⁸] (Z i)
Z_disj : univ.PairwiseDisjoint Z
D : S → Set Y := fun i ↦ g' ⁻¹' {f' i}
D_clopen : ∀ (i : S), IsClopen (D i)
Z_subset_D : ∀ (i : S), Z i ⊆ D i
C : S → Set Y
C_clopen : ∀ (i : S), IsClopen (C i)
Z_subset_C : ∀ (i : S), Z i ⊆ C i
C_subset_D : ∀ (i : S), C i ⊆ D i
C_cover_D : ⋃ i, D i ⊆ ⋃ i, C i
C_disj : univ.PairwiseDisjoint C
D_cover_univ : univ ⊆ ⋃ i, D i
C_cover_univ : ⋃ i, C i = univ
h_glue : ∀ (i j : S), ∀ x ∈ C i, x ∈ C j → i = j
x : X
⊢ ?m.505 ∈ Z (g x)

Tactic:
simpa using

Goal state after:
X : Type u_1
Y : Type u_2
S : Type u_3
T : Type u_4
inst✝¹⁰ : TopologicalSpace X
inst✝⁹ : CompactSpace X
inst✝⁸ : TopologicalSpace Y
inst✝⁷ : CompactSpace Y
inst✝⁶ : T2Space Y
inst✝⁵ : TotallyDisconnectedSpace Y
inst✝⁴ : TopologicalSpace S
inst✝³ : T2Space S
inst✝² : Finite S
inst✝¹ : TopologicalSpace T
inst✝ : T2Space T
f : X → Y
hf : Continuous[inst✝¹⁰, inst✝⁸] f
f_inj : Function.Injective f
f' : S → T
f'_surj : Function.Surjective f'
g : X → S
hg : Continuous[inst✝¹⁰, inst✝⁴] g
g' : Y → T
hg' : Continuous[inst✝⁸, inst✝¹] g'
h_comm : g' ∘ f = f' ∘ g
this : Finite T
Z : S → Set Y := fun i ↦ f '' g ⁻¹' {i}
Z_closed : ∀ (i : S), IsClosed[inst✝⁸] (Z i)
Z_disj : univ.PairwiseDisjoint Z
D : S → Set Y := fun i ↦ g' ⁻¹' {f' i}
D_clopen : ∀ (i : S), IsClopen (D i)
Z_subset_D : ∀ (i : S), Z i ⊆ D i
C : S → Set Y
C_clopen : ∀ (i : S), IsClopen (C i)
Z_subset_C : ∀ (i : S), Z i ⊆ C i
C_subset_D : ∀ (i : S), C i ⊆ D i
C_cover_D : ⋃ i, D i ⊆ ⋃ i, C i
C_disj : univ.PairwiseDisjoint C
D_cover_univ : univ ⊆ ⋃ i, D i
C_cover_univ : ⋃ i, C i = univ
h_glue : ∀ (i j : S), ∀ x ∈ C i, x ∈ C j → i = j
x : X
⊢ ?m.505 ∈ Z (g x)
Module: Mathlib.Control.Functor.Multivariate

Goal state before:
pp: case h₁
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
P : β → Prop
x : F (α ::: β)
u✝ : F fun i ↦ { p_1 // ofRepeat (α.PredLast' P i p_1) }
⊢ (fun i ↦ Subtype.val) <$$> u✝ = x ↔ (fun i x ↦ ↑(f P n α i x)) <$$> u✝ = x

Tactic:
suffices (fun i => Subtype.val) = (fun i x => (MvFunctor.f P n α i x).val) by rw [this]

Goal state after:
case h₁
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
P : β → Prop
x : F (α ::: β)
u✝ : F fun i ↦ { p_1 // ofRepeat (α.PredLast' P i p_1) }
⊢ (fun i ↦ Subtype.val) = fun i x ↦ ↑(f P n α i x)
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: m : Type u → Type v
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ ω✝ γ✝ : Type u
x✝¹ : OptionT m α✝
x✝ : Label ω✝ (OptionT m) γ✝ → α✝ → OptionT m ω✝
⊢ (callCC fun f ↦ x✝¹ >>= x✝ f).run =
    (do
        let x ← x✝¹
        callCC fun f ↦ x✝ f x).run

Tactic:
simpa using

Goal state after:
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ ω✝ γ✝ : Type u
x✝¹ : OptionT m α✝
x✝ : Label ω✝ (OptionT m) γ✝ → α✝ → OptionT m ω✝
⊢ (do
      let x ← x✝¹.run
      callCC fun f ↦ x.elim (pure none) fun x ↦ (x✝ (OptionT.mkLabel f) x).run) =
    do
    let __do_lift ← x✝¹.run
    __do_lift.elim (pure none) fun x ↦ callCC fun x_1 ↦ (x✝ (OptionT.mkLabel x_1) x).run
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
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
hn' : (π x).2 = ↑n
⊢ ¬(π x).2 = none

Tactic:
simpa using

Goal state after:
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
hn' : (π x).2 = ↑n
⊢ ¬↑n = none
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: case refine_1
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 (Set.range (σ (Option.some i)))ᶜ

Tactic:
simpa using

Goal state after:
case refine_1
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
⊢ IsClosed (Set.range (σ (Option.some i)))
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: case a
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
⊢ ωSup (approxChain f) ≤ Part.fix ⇑f

Tactic:
apply ωSup_le _ _ _
    simp only [Fix.approxChain]
    intro y x
    apply approx_le_fix f

Goal state after:
Module: Mathlib.Control.LawfulFix

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

Tactic:
rw [Part.fix_eq_of_ωScottContinuous (ωScottContinuous_toUnitMono f hc)]; rfl

Goal state after:
Module: Mathlib.Data.TypeVec

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

Tactic:
induction i
  <;> dsimp only [id, toSubtype', comp, ofSubtype'] at *

Goal state after:
case fz
n n✝ : ℕ
α : TypeVec.{u_1} (n✝ + 1)
r : α ⊗ α ⟹ «repeat» (n✝ + 1) Prop
x : Subtype_ r Fin2.fz
⊢ ⟨↑x, ⋯⟩ = x

case fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ :
  ∀ {α : TypeVec.{u_1} n✝} (r : α ⊗ α ⟹ «repeat» n✝ Prop) (x : Subtype_ r a✝), toSubtype' r a✝ (ofSubtype' r a✝ x) = x
α : TypeVec.{u_1} (n✝ + 1)
r : α ⊗ α ⟹ «repeat» (n✝ + 1) Prop
x : Subtype_ r a✝.fs
⊢ toSubtype' (dropFun r) a✝ (ofSubtype' (dropFun r) a✝ x) = x
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:
simpa using

Goal state after:
α : 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 (g (E.symm a) (E.symm b)) ≤ f (E.symm a)
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:
simpa using

Goal state after:
α : 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 (g (E.symm a) (E.symm b)) ≤ f (E.symm b)
Module: Mathlib.Data.Analysis.Filter

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f : Filter α
F : f.Realizer
E : F.σ ≃ τ
x✝¹ : Set α
x✝ : x✝¹ ∈ (CFilter.ofEquiv E F.F).toFilter.sets
s : τ
h : (CFilter.ofEquiv E F.F).f s ⊆ x✝¹
⊢ F.F.f (E.symm s) ⊆ x✝¹

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f : Filter α
F : f.Realizer
E : F.σ ≃ τ
x✝¹ : Set α
x✝ : x✝¹ ∈ (CFilter.ofEquiv E F.F).toFilter.sets
s : τ
h : (CFilter.ofEquiv E F.F).f s ⊆ x✝¹
⊢ F.F.f (E.symm s) ⊆ x✝¹
Module: Mathlib.Data.Analysis.Topology

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
F : Ctop α σ
E : σ ≃ τ
f : σ → Set α
T : α → σ
h₁ : ∀ (x : α), x ∈ f (T x)
I : (a b : σ) → (x : α) → x ∈ f a ∩ f b → σ
h₂ : ∀ (a b : σ) (x : α) (h : x ∈ f a ∩ f b), x ∈ f (I a b x h)
h₃ : ∀ (a b : σ) (x : α) (h : x ∈ f a ∩ f b), f (I a b x h) ⊆ f a ∩ f b
x : α
⊢ x ∈ f (E.symm (E (T x)))

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
F : Ctop α σ
E : σ ≃ τ
f : σ → Set α
T : α → σ
h₁ : ∀ (x : α), x ∈ f (T x)
I : (a b : σ) → (x : α) → x ∈ f a ∩ f b → σ
h₂ : ∀ (a b : σ) (x : α) (h : x ∈ f a ∩ f b), x ∈ f (I a b x h)
h₃ : ∀ (a b : σ) (x : α) (h : x ∈ f a ∩ f b), f (I a b x h) ⊆ f a ∩ f b
x : α
⊢ x ∈ f (T x)
Module: Mathlib.Data.Analysis.Topology

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
F : Ctop α σ
E : σ ≃ τ
f : σ → Set α
T : α → σ
h₁ : ∀ (x : α), x ∈ f (T x)
I : (a b : σ) → (x : α) → x ∈ f a ∩ f b → σ
h₂ : ∀ (a b : σ) (x : α) (h : x ∈ f a ∩ f b), x ∈ f (I a b x h)
h₃ : ∀ (a b : σ) (x : α) (h : x ∈ f a ∩ f b), f (I a b x h) ⊆ f a ∩ f b
a b : τ
x : α
h : x ∈ f (E.symm a) ∩ f (E.symm b)
⊢ x ∈ f (E.symm (E (I (E.symm a) (E.symm b) x h)))

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
F : Ctop α σ
E : σ ≃ τ
f : σ → Set α
T : α → σ
h₁ : ∀ (x : α), x ∈ f (T x)
I : (a b : σ) → (x : α) → x ∈ f a ∩ f b → σ
h₂ : ∀ (a b : σ) (x : α) (h : x ∈ f a ∩ f b), x ∈ f (I a b x h)
h₃ : ∀ (a b : σ) (x : α) (h : x ∈ f a ∩ f b), f (I a b x h) ⊆ f a ∩ f b
a b : τ
x : α
h : x ∈ f (E.symm a) ∩ f (E.symm b)
⊢ x ∈ f (I (E.symm a) (E.symm b) x h)
Module: Mathlib.Data.Analysis.Topology

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
F : Ctop α σ
E : σ ≃ τ
f : σ → Set α
T : α → σ
h₁ : ∀ (x : α), x ∈ f (T x)
I : (a b : σ) → (x : α) → x ∈ f a ∩ f b → σ
h₂ : ∀ (a b : σ) (x : α) (h : x ∈ f a ∩ f b), x ∈ f (I a b x h)
h₃ : ∀ (a b : σ) (x : α) (h : x ∈ f a ∩ f b), f (I a b x h) ⊆ f a ∩ f b
a b : τ
x : α
h : x ∈ f (E.symm a) ∩ f (E.symm b)
⊢ f (E.symm (E (I (E.symm a) (E.symm b) x h))) ⊆ f (E.symm a) ∩ f (E.symm b)

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
F : Ctop α σ
E : σ ≃ τ
f : σ → Set α
T : α → σ
h₁ : ∀ (x : α), x ∈ f (T x)
I : (a b : σ) → (x : α) → x ∈ f a ∩ f b → σ
h₂ : ∀ (a b : σ) (x : α) (h : x ∈ f a ∩ f b), x ∈ f (I a b x h)
h₃ : ∀ (a b : σ) (x : α) (h : x ∈ f a ∩ f b), f (I a b x h) ⊆ f a ∩ f b
a b : τ
x : α
h : x ∈ f (E.symm a) ∩ f (E.symm b)
⊢ f (I (E.symm a) (E.symm b) x h) ⊆ f (E.symm a) ∧ f (I (E.symm a) (E.symm b) x h) ⊆ f (E.symm b)
Module: Mathlib.Data.Analysis.Topology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
F : Realizer α
s : F.σ
a : α
m : a ∈ F.F.f s
⊢ 𝓝 a ≤ 𝓟 (F.F.f s)

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
F : Realizer α
s : F.σ
a : α
m : a ∈ F.F.f s
⊢ F.F.f s ∈ 𝓝 a
Module: Mathlib.Data.Analysis.Topology

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
inst✝ : TopologicalSpace α
F : Realizer α
E : F.σ ≃ τ
a : α
s✝ : Set α
x✝ : ∃ b, a ∈ F.F.f b ∧ F.F.f b ⊆ s✝
s : F.σ
h : a ∈ F.F.f s ∧ F.F.f s ⊆ s✝
⊢ a ∈ (Ctop.ofEquiv E F.F).f (E s) ∧ (Ctop.ofEquiv E F.F).f (E s) ⊆ s✝

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
inst✝ : TopologicalSpace α
F : Realizer α
E : F.σ ≃ τ
a : α
s✝ : Set α
x✝ : ∃ b, a ∈ F.F.f b ∧ F.F.f b ⊆ s✝
s : F.σ
h : a ∈ F.F.f s ∧ F.F.f s ⊆ s✝
⊢ a ∈ F.F.f s ∧ F.F.f s ⊆ s✝
Module: Mathlib.Data.Analysis.Topology

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
inst✝ : TopologicalSpace α
F : Realizer α
E : F.σ ≃ τ
a : α
s : Set α
x✝ : ∃ b, a ∈ (Ctop.ofEquiv E F.F).f b ∧ (Ctop.ofEquiv E F.F).f b ⊆ s
t : τ
h : a ∈ (Ctop.ofEquiv E F.F).f t ∧ (Ctop.ofEquiv E F.F).f t ⊆ s
⊢ a ∈ F.F.f (E.symm t) ∧ F.F.f (E.symm t) ⊆ s

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
inst✝ : TopologicalSpace α
F : Realizer α
E : F.σ ≃ τ
a : α
s : Set α
x✝ : ∃ b, a ∈ (Ctop.ofEquiv E F.F).f b ∧ (Ctop.ofEquiv E F.F).f b ⊆ s
t : τ
h : a ∈ (Ctop.ofEquiv E F.F).f t ∧ (Ctop.ofEquiv E F.F).f t ⊆ s
⊢ a ∈ F.F.f (E.symm t) ∧ F.F.f (E.symm t) ⊆ s
Module: Mathlib.Data.Erased

Goal state before:
pp: α : Sort u_1
a b : Erased α
h : a.out = b.out
⊢ a = b

Tactic:
simpa using

Goal state after:
α : Sort u_1
a b : Erased α
h : a.out = b.out
⊢ a = b
Module: Mathlib.Data.FP.Basic

Goal state before:
pp: C : FloatCfg
this : prec ≤ 2 * emax
⊢ emin + ↑prec - 1 ≤ ↑emax

Tactic:
← Int.ofNat_le

Goal state after:
C : FloatCfg
this : ↑prec ≤ ↑(2 * emax)
⊢ emin + ↑prec - 1 ≤ ↑emax
Module: Mathlib.Data.Fin.FlagRange

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : BoundedOrder α
n : ℕ
f : Fin (n + 1) → α
h0 : f 0 = ⊥
hlast : f (Fin.last n) = ⊤
hcovBy : ∀ (k : Fin n), f k.castSucc ⩿ f k.succ
hmono : Monotone f
t : Set α
htc : IsChain (fun x1 x2 ↦ x1 ≤ x2) t
hbt : range f ⊆ t
x : α
hx : x ∈ t
h : ∀ (y : Fin (n + 1)), f y ≠ x
this : ∀ (k : Fin (n + 1)), f k < x
⊢ False

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : BoundedOrder α
n : ℕ
f : Fin (n + 1) → α
h0 : f 0 = ⊥
hlast : f (Fin.last n) = ⊤
hcovBy : ∀ (k : Fin n), f k.castSucc ⩿ f k.succ
hmono : Monotone f
t : Set α
htc : IsChain (fun x1 x2 ↦ x1 ≤ x2) t
hbt : range f ⊆ t
x : α
hx : x ∈ t
h : ∀ (y : Fin (n + 1)), f y ≠ x
this : ∀ (k : Fin (n + 1)), f k < x
⊢ False
Module: Mathlib.Data.Fin.FlagRange

Goal state before:
pp: case zero
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : BoundedOrder α
n : ℕ
f : Fin (n + 1) → α
h0 : f 0 = ⊥
hlast : f (Fin.last n) = ⊤
hcovBy : ∀ (k : Fin n), f k.castSucc ⩿ f k.succ
hmono : Monotone f
t : Set α
htc : IsChain (fun x1 x2 ↦ x1 ≤ x2) t
hbt : range f ⊆ t
x : α
hx : x ∈ t
h : ∀ (y : Fin (n + 1)), f y ≠ x
⊢ f 0 < x

Tactic:
simpa using

Goal state after:
case zero
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : BoundedOrder α
n : ℕ
f : Fin (n + 1) → α
h0 : f 0 = ⊥
hlast : f (Fin.last n) = ⊤
hcovBy : ∀ (k : Fin n), f k.castSucc ⩿ f k.succ
hmono : Monotone f
t : Set α
htc : IsChain (fun x1 x2 ↦ x1 ≤ x2) t
hbt : range f ⊆ t
x : α
hx : x ∈ t
h : ∀ (y : Fin (n + 1)), f y ≠ x
⊢ ¬x = ⊥
Module: Mathlib.Data.Semiquot

Goal state before:
pp: α : Type u_1
q : Semiquot α
p : q.IsPure
a : α
⊢ a ∈ q ↔ a ∈ pure (q.get p)

Tactic:
simpa using

Goal state after:
α : Type u_1
q : Semiquot α
p : q.IsPure
a : α
⊢ a ∈ q ↔ a = q.get p
Module: Mathlib.Data.Semiquot

Goal state before:
pp: α : Type u_1
s t : Semiquot α
h : t.IsPure
st : s ≤ t
⊢ pure (t.get h) ≤ pure (s.get ⋯)

Tactic:
simpa using

Goal state after:
α : Type u_1
s t : Semiquot α
h : t.IsPure
st : s ≤ t
⊢ t.get h = s.get ⋯
Module: Mathlib.Data.Fin.Pigeonhole

Goal state before:
pp: m n : ℕ
f : Fin m → Fin n
hf : Function.Injective f
⊢ m ≤ n

Tactic:
simpa using

Goal state after:
m n : ℕ
f : Fin m → Fin n
hf : Function.Injective f
⊢ m ≤ n
Module: Mathlib.Data.Fin.Pigeonhole

Goal state before:
pp: m n : ℕ
f : Fin m ↪ Fin n
⊢ m ≤ n

Tactic:
simpa using

Goal state after:
m n : ℕ
f : Fin m ↪ Fin n
⊢ m ≤ n
Module: Mathlib.Data.Fin.Pigeonhole

Goal state before:
pp: m n : ℕ
f : Fin m → Fin n
hf : Function.Injective f
b : Fin n
hb : b ∉ Set.range f
⊢ m < n

Tactic:
simpa using

Goal state after:
m n : ℕ
f : Fin m → Fin n
hf : Function.Injective f
b : Fin n
hb : b ∉ Set.range f
⊢ m < n
Module: Mathlib.Data.Fin.Pigeonhole

Goal state before:
pp: m n : ℕ
f : Fin m → Fin n
hf : Function.Surjective f
⊢ n ≤ m

Tactic:
simpa using

Goal state after:
m n : ℕ
f : Fin m → Fin n
hf : Function.Surjective f
⊢ n ≤ m
Module: Mathlib.Data.Fin.Pigeonhole

Goal state before:
pp: m : ℕ
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Fin m → α
⊢ Fintype.card ↑(Set.range f) ≤ m

Tactic:
simpa using

Goal state after:
m : ℕ
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Fin m → α
⊢ (Finset.image f Finset.univ).card ≤ m
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: S T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
inst✝ : Epi π
⊢ ∃ S' T' y' π' g',
    Epi π' ∧
      Epi y' ∧
        π' ≫ y' ▷ ℕ∪{∞} = g' ≫ π ∧
          IsSplitEpi (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π' ≫ fst S' ℕ∪{∞}) ∧ Epi (cover π')

Tactic:
by
  -- Construct the space `S'` space which has functions `σ'` we can plug into
  -- `fibres`.
  have := S'_compactSpace π (by fun_prop)
  let S'π (n : ℕ∪{∞}) : LightProfinite.of (S' π) ⟶ LightProfinite.fibre n (π ≫ snd _ _) :=
    ⟨TopCat.ofHom {
      toFun x := x.val n,
      continuous_toFun := by refine (continuous_apply _).comp ?_; fun_prop }⟩
  let y' : LightProfinite.of (S' π) ⟶ S := ConcreteCategory.ofHom ⟨y π, y_continuous π⟩
  let π' := pullback.snd π (y' ▷ ℕ∪{∞})
  let σ' : ℕ∪{∞} → LightProfinite.of (S' π) → pullback π (y' ▷ ℕ∪{∞}) := fun n ↦
    pullback.lift _ _ (S'π n ≫ LightProfinite.fibreIncl _ _) (lift (𝟙 _) (const _ n)) <| by
      apply CartesianMonoidalCategory.hom_ext<;> ext x; exacts [x.prop n ∞, (x.val n).prop]
  have hσ (x : ℕ∪{∞}) (s : LightProfinite.of (S' π)) : (π' (σ' x s)).1 = s := rfl
  have hσ' (x : ℕ∪{∞}) (s : LightProfinite.of (S' π)) : (π' (σ' x s)).2 = x := rfl
  -- The space `T'` is given by the union of the images of the `σ'` together
  -- with the whole fibre over `∞`. Here `cover` is an epimorphism
  -- because the projection is an isomorphism away from the fibre at `∞`.
  have : CompactSpace (fibres π' σ') := isCompact_iff_compactSpace.mp
    (fibres_closed π' (by fun_prop) σ' (by fun_prop) hσ').isCompact
  refine ⟨LightProfinite.of (S' π), LightProfinite.of (fibres π' σ'), y',
    ⟨TopCat.ofHom ⟨Subtype.val, by fun_prop⟩⟩ ≫ π',
    ⟨TopCat.ofHom ⟨Subtype.val, by fun_prop⟩⟩ ≫ pullback.fst _ _, ?_, ?_, ?_, ?_, ?_⟩
  · rw [LightProfinite.epi_iff_surjective]
    refine fibres_surjective _ ?_ _ hσ hσ'
    rw [← LightProfinite.epi_iff_surjective]
    dsimp [π']
    infer_instance
  · rw [LightProfinite.epi_iff_surjective]
    apply y_surjective
    rwa [← LightProfinite.epi_iff_surjective]
  · simp [π', pullback.condition]
  · exact ⟨ConcreteCategory.ofHom ⟨(sectionOfFibreIncl π' σ' hσ'),
      (.subtype_mk (by fun_prop) _)⟩, rfl⟩
  · rw [LightProfinite.epi_iff_surjective]
    exact coverToFun_surjective _ _ hσ hσ'

Goal state after: