mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Category.Profinite.Basic

Goal state before:
pp: case mpr
X Y : Profinite
f : X ⟶ Y
⊢ Function.Surjective ⇑(ConcreteCategory.hom f) → Epi f

Tactic:
rw [← CategoryTheory.ofHom_epi_iff_surjective]

Goal state after:
case mpr
X Y : Profinite
f : X ⟶ Y
⊢ Epi (↾⇑(ConcreteCategory.hom f)) → Epi f
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: case neg
A E : Type u
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalSpace E
ρ : E → A
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
zorn_subset : ∀ (E₀ : Set E), E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ
G : Set E
hG : IsOpen G
G_empty : ¬G = ∅
a : A
ha : a ∈ ρ '' G
⊢ a ∈ closure (ρ '' Gᶜ)ᶜ

Tactic:
rw [mem_closure_iff]

Goal state after:
case neg
A E : Type u
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalSpace E
ρ : E → A
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
zorn_subset : ∀ (E₀ : Set E), E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ
G : Set E
hG : IsOpen G
G_empty : ¬G = ∅
a : A
ha : a ∈ ρ '' G
⊢ ∀ (o : Set A), IsOpen o → a ∈ o → (o ∩ (ρ '' Gᶜ)ᶜ).Nonempty
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: A E : Type u
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalSpace E
ρ : E → A
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
zorn_subset : ∀ (E₀ : Set E), E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ
G : Set E
hG : IsOpen G
G_empty : ¬G = ∅
N : Set A
N_open : IsOpen N
e : E
he : e ∈ G
ha : ρ e ∈ ρ '' G
hN : ρ e ∈ N
nonempty : (G ∩ ρ ⁻¹' N).Nonempty
is_open : IsOpen (G ∩ ρ ⁻¹' N)
ne_univ : ρ '' (G ∩ ρ ⁻¹' N)ᶜ ≠ univ
y : E
hx : ρ y ∈ (ρ '' (G ∩ ρ ⁻¹' N)ᶜ)ᶜ
hx' : ρ y ∈ (ρ '' Gᶜ)ᶜ
⊢ y ∈ G ∩ ρ ⁻¹' N

Tactic:
simpa using mt (mem_image_of_mem ρ) <| mem_compl hx

Goal state after:
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: A E : Type u
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSpace E
inst✝³ : ExtremallyDisconnected A
inst✝² : T2Space A
inst✝¹ : T2Space E
inst✝ : CompactSpace E
ρ : E → A
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
zorn_subset : ∀ (E₀ : Set E), E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ
x₁ x₂ : E
hρx : ρ x₁ = ρ x₂
hx : ¬x₁ = x₂
G₁ G₂ : Set E
G₁_open : IsOpen G₁
G₂_open : IsOpen G₂
hx₁ : x₁ ∈ G₁
hx₂ : x₂ ∈ G₂
disj : Disjoint G₁ G₂
G₁_comp : IsCompact G₁ᶜ
⊢ False

Tactic:
have G₂_comp : IsCompact G₂ᶜ := IsClosed.isCompact G₂_open.isClosed_compl

Goal state after:
A E : Type u
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSpace E
inst✝³ : ExtremallyDisconnected A
inst✝² : T2Space A
inst✝¹ : T2Space E
inst✝ : CompactSpace E
ρ : E → A
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
zorn_subset : ∀ (E₀ : Set E), E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ
x₁ x₂ : E
hρx : ρ x₁ = ρ x₂
hx : ¬x₁ = x₂
G₁ G₂ : Set E
G₁_open : IsOpen G₁
G₂_open : IsOpen G₂
hx₁ : x₁ ∈ G₁
hx₂ : x₂ ∈ G₂
disj : Disjoint G₁ G₂
G₁_comp : IsCompact G₁ᶜ
G₂_comp : IsCompact G₂ᶜ
⊢ False
Module: Mathlib.Topology.Category.Stonean.Basic

Goal state before:
pp: X : CompHaus
inst✝⁶ : Projective X
A B : Type u
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSpace B
inst✝³ : CompactSpace A
inst✝² : T2Space A
inst✝¹ : CompactSpace B
inst✝ : T2Space B
f : ↑X.toTop → B
g : A → B
hf : Continuous[_, inst✝⁴] f
hg : Continuous[inst✝⁵, inst✝⁴] g
⊢ Function.Surjective g → ∃ h, Continuous[_, inst✝⁵] h ∧ g ∘ h = f

Tactic:
hsurj

Goal state after:
X : CompHaus
inst✝⁶ : Projective X
A B : Type u
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSpace B
inst✝³ : CompactSpace A
inst✝² : T2Space A
inst✝¹ : CompactSpace B
inst✝ : T2Space B
f : ↑X.toTop → B
g : A → B
hf : Continuous[_, inst✝⁴] f
hg : Continuous[inst✝⁵, inst✝⁴] g
hsurj : Function.Surjective g
⊢ ∃ h, Continuous[_, inst✝⁵] h ∧ g ∘ h = f
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case tail
k : Cont
v : List ℕ
s : Option Γ'
⊢ ∃ b₂,
    TrCfg (stepNormal Code.tail k v) b₂ ∧
      Reaches₁ (TM2.step tr)
        { l := some (trNormal Code.tail (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) } b₂

Tactic:
let o : Option Γ' := List.casesOn v none fun _ _ => some Γ'.cons

Goal state after:
case tail
k : Cont
v : List ℕ
s : Option Γ'
o : Option Γ' := List.casesOn v none fun x x_1 ↦ some Γ'.cons
⊢ ∃ b₂,
    TrCfg (stepNormal Code.tail k v) b₂ ∧
      Reaches₁ (TM2.step tr)
        { l := some (trNormal Code.tail (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) } b₂
Module: Mathlib.Topology.DiscreteQuotient

Goal state before:
pp: X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
⊢ Injective (finsetClopens X)

Tactic:
apply Function.Injective.of_comp (f := Set.image (fun (t : Clopens X) ↦ t.carrier) ∘ (↑))

Goal state after:
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
⊢ Injective (((image fun t ↦ t.carrier) ∘ SetLike.coe) ∘ finsetClopens X)
Module: Mathlib.Topology.Category.TopCat.Limits.Cofiltered

Goal state before:
pp: case e'_3.mpr.refine_2
J : Type v
inst✝¹ : Category.{w, v} J
inst✝ : IsCofiltered J
F : J ⥤ TopCat
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j), ∀ V ∈ T j, ⇑(ConcreteCategory.hom (F.map f)) ⁻¹' V ∈ T i
U0 : Set ↑C.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ i ∈ G, U i ∈ T i
h2 : U0 = ⋂ i ∈ G, (fun x ↦ (ConcreteCategory.hom (C.π.app i)) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he ↦ ⋯.some
Vs : J → Set ↑(F.obj j) := fun e ↦ if h : e ∈ G then ⇑(ConcreteCategory.hom (F.map (g e h))) ⁻¹' U e else Set.univ
V : Set ↑(F.obj j) := ⋂ e ∈ G, Vs e
⊢ U0 = ⇑(ConcreteCategory.hom (C.π.app j)) ⁻¹' V

Tactic:
rw [h2]

Goal state after:
case e'_3.mpr.refine_2
J : Type v
inst✝¹ : Category.{w, v} J
inst✝ : IsCofiltered J
F : J ⥤ TopCat
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j), ∀ V ∈ T j, ⇑(ConcreteCategory.hom (F.map f)) ⁻¹' V ∈ T i
U0 : Set ↑C.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ i ∈ G, U i ∈ T i
h2 : U0 = ⋂ i ∈ G, (fun x ↦ (ConcreteCategory.hom (C.π.app i)) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he ↦ ⋯.some
Vs : J → Set ↑(F.obj j) := fun e ↦ if h : e ∈ G then ⇑(ConcreteCategory.hom (F.map (g e h))) ⁻¹' U e else Set.univ
V : Set ↑(F.obj j) := ⋂ e ∈ G, Vs e
⊢ ⋂ i ∈ G, (fun x ↦ (ConcreteCategory.hom (C.π.app i)) x) ⁻¹' U i = ⇑(ConcreteCategory.hom (C.π.app j)) ⁻¹' V
Module: Mathlib.Topology.Category.Profinite.CofilteredLimit

Goal state before:
pp: case refine_3.refine_2.mp
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toTop
hC : IsLimit C
hU : IsClopen U
S : Set (Set ↑(toTopCat.mapCone C).pt)
hS : S ⊆ {U | ∃ j, ∃ V ∈ {W | IsClopen W}, U = ⇑(ConcreteCategory.hom ((toTopCat.mapCone C).π.app j)) ⁻¹' V}
h : U = ⋃₀ S
j : ↑S → J := fun s ↦ Exists.choose ⋯
V : (s : ↑S) → Set ↑(F.obj (j s)).toTop := fun s ↦ ⋯.choose
hV : ∀ (s : ↑S), IsClopen (V s) ∧ ↑s = ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s
hUo : ∀ (i : ↑S), IsOpen ((fun s ↦ ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s) i)
hsU : U ⊆ ⋃ i, (fun s ↦ ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s) i
G : Finset ↑S
hG : U ⊆ ⋃ i ∈ G, ⇑(ConcreteCategory.hom (C.π.app (j i))) ⁻¹' V i
j0 : J
hj0 : ∀ {X : J}, X ∈ Finset.image j G → Nonempty (j0 ⟶ X)
f : (s : ↑S) → s ∈ G → (j0 ⟶ j s) := fun s hs ↦ ⋯.some
W : ↑S → Set ↑(F.obj j0).toTop :=
  fun s ↦ if hs : s ∈ G then ⇑(ConcreteCategory.hom (F.map (f s hs))) ⁻¹' V s else Set.univ
x : ↑C.pt.toTop
hx : x ∈ U
⊢ ∃ i,
    ∃ (_ : i ∈ G),
      x ∈
        ⇑(ConcreteCategory.hom (C.π.app j0)) ⁻¹'
          if h : i ∈ G then ⇑(ConcreteCategory.hom (F.map (f i ⋯))) ⁻¹' V i else Set.univ

Tactic:
obtain ⟨_, ⟨s, rfl⟩, _, ⟨hs, rfl⟩, hh⟩ := hG hx

Goal state after:
case refine_3.refine_2.mp
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toTop
hC : IsLimit C
hU : IsClopen U
S : Set (Set ↑(toTopCat.mapCone C).pt)
hS : S ⊆ {U | ∃ j, ∃ V ∈ {W | IsClopen W}, U = ⇑(ConcreteCategory.hom ((toTopCat.mapCone C).π.app j)) ⁻¹' V}
h : U = ⋃₀ S
j : ↑S → J := fun s ↦ Exists.choose ⋯
V : (s : ↑S) → Set ↑(F.obj (j s)).toTop := fun s ↦ ⋯.choose
hV : ∀ (s : ↑S), IsClopen (V s) ∧ ↑s = ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s
hUo : ∀ (i : ↑S), IsOpen ((fun s ↦ ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s) i)
hsU : U ⊆ ⋃ i, (fun s ↦ ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s) i
G : Finset ↑S
hG : U ⊆ ⋃ i ∈ G, ⇑(ConcreteCategory.hom (C.π.app (j i))) ⁻¹' V i
j0 : J
hj0 : ∀ {X : J}, X ∈ Finset.image j G → Nonempty (j0 ⟶ X)
f : (s : ↑S) → s ∈ G → (j0 ⟶ j s) := fun s hs ↦ ⋯.some
W : ↑S → Set ↑(F.obj j0).toTop :=
  fun s ↦ if hs : s ∈ G then ⇑(ConcreteCategory.hom (F.map (f s hs))) ⁻¹' V s else Set.univ
x : ↑C.pt.toTop
hx : x ∈ U
s : ↑S
hs : s ∈ G
hh : x ∈ (fun h ↦ ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s) hs
⊢ ∃ i,
    ∃ (_ : i ∈ G),
      x ∈
        ⇑(ConcreteCategory.hom (C.π.app j0)) ⁻¹'
          if h : i ∈ G then ⇑(ConcreteCategory.hom (F.map (f i ⋯))) ⁻¹' V i else Set.univ
Module: Mathlib.Topology.Category.LightProfinite.Basic

Goal state before:
pp: case mpr
X Y : LightProfinite
f : X ⟶ Y
⊢ Function.Surjective ⇑(ConcreteCategory.hom f) → Epi f

Tactic:
rw [← CategoryTheory.ofHom_epi_iff_surjective]

Goal state after:
case mpr
X Y : LightProfinite
f : X ⟶ Y
⊢ Epi (↾⇑(ConcreteCategory.hom f)) → Epi f
Module: Mathlib.Topology.Category.TopCat.Yoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F : C ⥤ TopCat
Y : Type w'
inst✝ : TopologicalSpace Y
x✝ : ℕ
K : Discrete (Fin x✝) ⥤ TopCatᵒᵖ
α✝ : Type
X : α✝ → TopCat
⊢ IsIso (piComparison (yonedaPresheaf' Y) fun x ↦ op (X x))

Tactic:
by rw [piComparison_fac]; infer_instance

Goal state after:
Module: Mathlib.Topology.Category.Profinite.CofilteredLimit

Goal state before:
pp: case intro
J : Type v
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y ↦ if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toTop) (Fin 2) := (LocallyConstant.map ι f).flip
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap (TopCat.Hom.hom (C.π.app (j a)).hom) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a ↦ ⋯.some
gg : α → LocallyConstant (↑(F.obj j0).toTop) (Fin 2) :=
  fun a ↦ LocallyConstant.comap (TopCat.Hom.hom (F.map (fs a)).hom) (g a)
ggg : LocallyConstant (↑(F.obj j0).toTop) (α → Fin 2) := LocallyConstant.unflip gg
this : LocallyConstant.map ι f = LocallyConstant.unflip (LocallyConstant.map ι f).flip
⊢ LocallyConstant.map (fun a b ↦ if a = b then 0 else 1) f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j0).hom) ggg

Tactic:
rw [this]

Goal state after:
case intro
J : Type v
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y ↦ if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toTop) (Fin 2) := (LocallyConstant.map ι f).flip
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap (TopCat.Hom.hom (C.π.app (j a)).hom) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a ↦ ⋯.some
gg : α → LocallyConstant (↑(F.obj j0).toTop) (Fin 2) :=
  fun a ↦ LocallyConstant.comap (TopCat.Hom.hom (F.map (fs a)).hom) (g a)
ggg : LocallyConstant (↑(F.obj j0).toTop) (α → Fin 2) := LocallyConstant.unflip gg
this : LocallyConstant.map ι f = LocallyConstant.unflip (LocallyConstant.map ι f).flip
⊢ LocallyConstant.unflip (LocallyConstant.map ι f).flip = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j0).hom) ggg
Module: Mathlib.Topology.Category.Profinite.CofilteredLimit

Goal state before:
pp: case intro
J : Type v
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y ↦ if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toTop) (Fin 2) := (LocallyConstant.map ι f).flip
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap (TopCat.Hom.hom (C.π.app (j a)).hom) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a ↦ ⋯.some
gg : α → LocallyConstant (↑(F.obj j0).toTop) (Fin 2) :=
  fun a ↦ LocallyConstant.comap (TopCat.Hom.hom (F.map (fs a)).hom) (g a)
ggg : LocallyConstant (↑(F.obj j0).toTop) (α → Fin 2) := LocallyConstant.unflip gg
this :
  LocallyConstant.comap (TopCat.Hom.hom (C.π.app j0).hom) ggg =
    LocallyConstant.unflip (LocallyConstant.comap (TopCat.Hom.hom (C.π.app j0).hom) ggg).flip
⊢ LocallyConstant.unflip (LocallyConstant.map ι f).flip = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j0).hom) ggg

Tactic:
rw [this]

Goal state after:
case intro
J : Type v
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y ↦ if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toTop) (Fin 2) := (LocallyConstant.map ι f).flip
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap (TopCat.Hom.hom (C.π.app (j a)).hom) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a ↦ ⋯.some
gg : α → LocallyConstant (↑(F.obj j0).toTop) (Fin 2) :=
  fun a ↦ LocallyConstant.comap (TopCat.Hom.hom (F.map (fs a)).hom) (g a)
ggg : LocallyConstant (↑(F.obj j0).toTop) (α → Fin 2) := LocallyConstant.unflip gg
this :
  LocallyConstant.comap (TopCat.Hom.hom (C.π.app j0).hom) ggg =
    LocallyConstant.unflip (LocallyConstant.comap (TopCat.Hom.hom (C.π.app j0).hom) ggg).flip
⊢ LocallyConstant.unflip (LocallyConstant.map ι f).flip =
    LocallyConstant.unflip (LocallyConstant.comap (TopCat.Hom.hom (C.π.app j0).hom) ggg).flip
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case fix.false
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
a✝¹ : Code
a✝ : Cont'
H₁ : codeSupp a✝¹ (Cont'.fix a✝¹ a✝) ⊆ S
L : ∀ {α : Type ?u.19} [inst : DecidableEq α] {s : Finset α} {a : α} (t : Finset α), a ∈ s → a ∈ s ∪ t
R : ∀ {α : Type ?u.21} [inst : DecidableEq α] {t : Finset α} {a : α} (s : Finset α), a ∈ t → a ∈ s ∪ t
s : Option Γ'
⊢ (bif false then Λ'.ret a✝ else Λ'.clear natEnd main (trNormal a✝¹ (Cont'.fix a✝¹ a✝))) ∈ S

pp: case fix.true
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
a✝¹ : Code
a✝ : Cont'
H₁ : codeSupp a✝¹ (Cont'.fix a✝¹ a✝) ⊆ S
L : ∀ {α : Type ?u.19} [inst : DecidableEq α] {s : Finset α} {a : α} (t : Finset α), a ∈ s → a ∈ s ∪ t
R : ∀ {α : Type ?u.21} [inst : DecidableEq α] {t : Finset α} {a : α} (s : Finset α), a ∈ t → a ∈ s ∪ t
s : Option Γ'
⊢ (bif true then Λ'.ret a✝ else Λ'.clear natEnd main (trNormal a✝¹ (Cont'.fix a✝¹ a✝))) ∈ S

Tactic:
· refine H₁ (R _ <| L _ <| R _ <| R _ <| L _ W)

Goal state after:
case fix.true
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
a✝¹ : Code
a✝ : Cont'
H₁ : codeSupp a✝¹ (Cont'.fix a✝¹ a✝) ⊆ S
L : ∀ {α : Type} [inst : DecidableEq α] {s : Finset α} {a : α} (t : Finset α), a ∈ s → a ∈ s ∪ t
R : ∀ {α : Type} [inst : DecidableEq α] {t : Finset α} {a : α} (s : Finset α), a ∈ t → a ∈ s ∪ t
s : Option Γ'
⊢ (bif true then Λ'.ret a✝ else Λ'.clear natEnd main (trNormal a✝¹ (Cont'.fix a✝¹ a✝))) ∈ S
Module: Mathlib.Condensed.Light.Epi

Goal state before:
pp: n : ℕ
R : Type u
inst✝¹ : Ring R
M N : ℕ → LightCondMod R
f✝ : (n : ℕ) → M n ⟶ N n
inst✝ : ∀ (n : ℕ), Epi (f✝ n)
X✝ Y✝ : Discrete ℕ ⥤ LightCondMod R
f : X✝ ⟶ Y✝
x✝ : Epi f
this : lim.map f = (Pi.isoLimit X✝).inv ≫ (Limits.Pi.map fun x ↦ f.app { as := x }) ≫ (Pi.isoLimit Y✝).hom
⊢ Epi (lim.map f)

Tactic:
rw [this]

Goal state after:
n : ℕ
R : Type u
inst✝¹ : Ring R
M N : ℕ → LightCondMod R
f✝ : (n : ℕ) → M n ⟶ N n
inst✝ : ∀ (n : ℕ), Epi (f✝ n)
X✝ Y✝ : Discrete ℕ ⥤ LightCondMod R
f : X✝ ⟶ Y✝
x✝ : Epi f
this : lim.map f = (Pi.isoLimit X✝).inv ≫ (Limits.Pi.map fun x ↦ f.app { as := x }) ≫ (Pi.isoLimit Y✝).hom
⊢ Epi ((Pi.isoLimit X✝).inv ≫ (Limits.Pi.map fun x ↦ f.app { as := x }) ≫ (Pi.isoLimit Y✝).hom)
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
⊢ ∃ k, Continuous[inst✝⁸, inst✝⁴] k ∧ f' ∘ k = g' ∧ k ∘ f = g

Tactic:
have h_glue (i j : S) (x : Y) (hxi : x ∈ C i) (hxj : x ∈ C j) : i = j := by
    rw [Set.pairwiseDisjoint_iff] at C_disj
    exact C_disj (by simp) (by simp) ⟨x, by grind⟩

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
⊢ ∃ k, Continuous[inst✝⁸, inst✝⁴] k ∧ f' ∘ k = g' ∧ k ∘ f = g
Module: Mathlib.Data.Nat.Upto

Goal state before:
pp: p : ℕ → Prop
x : ℕ
h : p x
this : Upto.GT p = InvImage (fun x1 x2 ↦ x1 < x2) fun y ↦ x - ↑y
⊢ WellFounded (Upto.GT p)

Tactic:
rw [this]

Goal state after:
p : ℕ → Prop
x : ℕ
h : p x
this : Upto.GT p = InvImage (fun x1 x2 ↦ x1 < x2) fun y ↦ x - ↑y
⊢ WellFounded (InvImage (fun x1 x2 ↦ x1 < x2) fun y ↦ x - ↑y)
Module: Mathlib.Control.Bitraversable.Instances

Goal state before:
pp: case bitraverse_eq_bimap_id
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F G : Type u → Type u
inst✝⁴ : Traversable F
inst✝³ : Traversable G
inst✝² : LawfulTraversable F
inst✝¹ : LawfulTraversable G
inst✝ : LawfulBitraversable t
α✝ α'✝ β✝ β'✝ : Type u
f✝ : α✝ → β✝
f'✝ : α'✝ → β'✝
x✝ : bicompl t F G α✝ α'✝
⊢ bitraverse (traverse (pure ∘ f✝)) (traverse (pure ∘ f'✝)) x✝ = pure (bimap (Functor.map f✝) (Functor.map f'✝) x✝)

Tactic:
simp [traverse_eq_map_id', bitraverse_eq_bimap_id]

Goal state after:
Module: Mathlib.Control.Bitraversable.Instances

Goal state before:
pp: case binaturality
t : Type u → Type u → Type u
inst✝⁷ : Bitraversable t
F : Type u → Type u
inst✝⁶ : Traversable F
inst✝⁵ : LawfulTraversable F
inst✝⁴ : LawfulBitraversable 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✝ β✝
f'✝ : α'✝ → F✝ β'✝
x✝ : bicompr F t α✝ α'✝
⊢ η✝.app (bicompr F t β✝ β'✝) (traverse (bitraverse f✝ f'✝) x✝) =
    traverse (bitraverse (η✝.app β✝ ∘ f✝) (η✝.app β'✝ ∘ f'✝)) x✝

Tactic:
dsimp only [bicompr]

Goal state after:
case binaturality
t : Type u → Type u → Type u
inst✝⁷ : Bitraversable t
F : Type u → Type u
inst✝⁶ : Traversable F
inst✝⁵ : LawfulTraversable F
inst✝⁴ : LawfulBitraversable 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✝ β✝
f'✝ : α'✝ → F✝ β'✝
x✝ : bicompr F t α✝ α'✝
⊢ η✝.app (F (t β✝ β'✝)) (traverse (bitraverse f✝ f'✝) x✝) = traverse (bitraverse (η✝.app β✝ ∘ f✝) (η✝.app β'✝ ∘ f'✝)) x✝
Module: Mathlib.Control.Functor.Multivariate

Goal state before:
pp: 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) }
this : (fun i ↦ Subtype.val) = fun i x ↦ ↑(f P n α i x)
⊢ (fun i ↦ Subtype.val) <$$> u✝ = x ↔ (fun i x ↦ ↑(f P n α i x)) <$$> u✝ = x

Tactic:
rw [this]

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
α : TypeVec.{u_1} (n + 1)
α' : TypeVec.{u_2} (n + 1)
f f' : α.drop ⟹ α'.drop
g g' : α.last → α'.last
H : splitFun f g = splitFun f' g'
⊢ f = f' ∧ g = g'

Tactic:
by
  rw [← dropFun_splitFun f g, H, ← lastFun_splitFun f g, H]; simp

Goal state after:
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} (dummy : OptionT m α), (callCC fun x ↦ dummy) = dummy

Tactic:
intros; ext; simp [callCC, OptionT.callCC, @callCC_dummy m _]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
f : Π₀ (i : ι), Finset (α i)
i : ι
x✝ : i ∈ f.support
⊢ #(f i) = (fun i ↦ ↑(#(f i))) i (f i)

Tactic:
simp only [Pi.natCast_apply, Nat.cast_id]

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

Goal state before:
pp: l : List Bool
hl : IsChain (fun x1 x2 ↦ x1 ≠ x2) l
b : Bool
⊢ l.length - 1 ≤ 2 * count b l

Tactic:
grind [hl.two_mul_count_bool_eq_ite]

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

Goal state before:
pp: l : List Bool
hl : IsChain (fun x1 x2 ↦ x1 ≠ x2) l
b : Bool
⊢ 2 * count b l ≤ l.length + 1

Tactic:
grind [hl.two_mul_count_bool_eq_ite]

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

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_2
v : (i : Fin (n + 1)) → α i
⊢ take 1 ⋯ v = fun i ↦ v (castLE ⋯ i)

Tactic:
ext i
  simp only [take]

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

Goal state before:
pp: α : Type u_1
f : α → Option α
h : ∀ (a b : α), b ∈ f a → a = b
l : List α
⊢ lookmap f l = l

Tactic:
← map_id (l.lookmap f),

Goal state after:
α : Type u_1
f : α → Option α
h : ∀ (a b : α), b ∈ f a → a = b
l : List α
⊢ map id (lookmap f l) = l