mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: a b c d b' : List Γ'
⊢ update (elim a b c d) rev b' = elim a b' c d

Tactic:
funext x

Goal state after:
a b c d b' : List Γ'
x : K'
⊢ update (elim a b c d) rev b' x = elim a b' c d x
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: a b c d c' : List Γ'
⊢ update (elim a b c d) aux c' = elim a b c' d

Tactic:
funext x

Goal state after:
a b c d c' : List Γ'
x : K'
⊢ update (elim a b c d) aux c' x = elim a b c' d x
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: a b c d d' : List Γ'
⊢ update (elim a b c d) stack d' = elim a b c d'

Tactic:
funext x

Goal state after:
a b c d d' : List Γ'
x : K'
⊢ update (elim a b c d) stack d' x = elim a b c d' x
Module: Mathlib.Topology.Separation.Profinite

Goal state before:
pp: X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : T2Space X
inst✝¹ : CompactSpace X
inst✝ : TotallyDisconnectedSpace X
⊢ IsTopologicalBasis {s | IsClopen s}

Tactic:
by
  apply isTopologicalBasis_of_isOpen_of_nhds fun U (hU : IsClopen U) => hU.2
  intro x U hxU U_op
  have : U ∈ 𝓝 x := IsOpen.mem_nhds U_op hxU
  rcases (nhds_basis_clopen x).mem_iff.mp this with ⟨V, ⟨hxV, hV⟩, hVU : V ⊆ U⟩
  use V
  tauto

Goal state after:
Module: Mathlib.Topology.Separation.Profinite

Goal state before:
pp: X : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : TotallyDisconnectedSpace X
Z U : Set X
hZ : IsClosed[inst✝³] Z
hU : IsOpen[inst✝³] U
hZU : Z ⊆ U
⊢ ∃ C, IsClopen C ∧ Z ⊆ C ∧ C ⊆ U

Tactic:
choose V hV using fun (z : Z) ↦ compact_exists_isClopen_in_isOpen hU (hZU z.property)
  -- the `V z` cover `Z`
  have V_cover : Z ⊆ ⋃ z, V z := fun z hz ↦ mem_iUnion.mpr ⟨⟨z, hz⟩, (hV ⟨z, hz⟩).2.1⟩
  -- choose a finite subcover
  choose I hI using hZ.isCompact.elim_finite_subcover V (fun z ↦ (hV z).1.isOpen) V_cover
  -- the union of this finite subcover does the job
  exact ⟨⋃ (i ∈ I), V i, I.finite_toSet.isClopen_biUnion (fun i _ ↦ (hV i).1), hI, by simp_all⟩

Goal state after:
Module: Mathlib.Topology.Separation.Profinite

Goal state before:
pp: X : Type u_4
I✝ : Type u_5
inst✝⁵ : TopologicalSpace X
inst✝⁴ : CompactSpace X
inst✝³ : T2Space X
inst✝² : TotallyDisconnectedSpace X
inst✝¹ : Finite I✝
I : Type u_5
inst✝ : Fintype I
IH :
  ∀ {Z D : I → Set X},
    (∀ (i : I), IsClosed[inst✝⁵] (Z i)) →
      (∀ (i : I), IsClopen (D i)) →
        (∀ (i : I), Z i ⊆ D i) →
          univ.PairwiseDisjoint Z →
            ∃ C,
              (∀ (i : I), IsClopen (C i)) ∧
                (∀ (i : I), Z i ⊆ C i) ∧ (∀ (i : I), C i ⊆ D i) ∧ ⋃ i, D i ⊆ ⋃ i, C i ∧ univ.PairwiseDisjoint C
Z D : Option I → Set X
Z_closed : ∀ (i : Option I), IsClosed[inst✝⁵] (Z i)
D_clopen : ∀ (i : Option I), IsClopen (D i)
Z_subset_D : ∀ (i : Option I), Z i ⊆ D i
Z_disj : univ.PairwiseDisjoint Z
Z' : I → Set X := fun i ↦ Z (some i)
Z'_closed : ∀ (i : I), IsClosed[inst✝⁵] (Z (some i))
Z'_disj : univ.PairwiseDisjoint (Z ∘ some)
U : Set X := D none \ ⋃ i, Z (some i)
U_open : IsOpen[inst✝⁵] U
i : I
⊢ Disjoint (Z none) (Z (some i))

Tactic:
by apply Z_disj; all_goals simp

Goal state after:
Module: Mathlib.Topology.Category.CompHaus.Projective

Goal state before:
pp: X : Type u_1
Y Z : CompHaus
f : of (Ultrafilter X) ⟶ Z
g : Y ⟶ Z
hg : Surjective ⇑(ConcreteCategory.hom g)
g' : (fun X ↦ ↑X.toTop) Z → (fun X ↦ ↑X.toTop) Y
hg' : RightInverse g' ⇑(ConcreteCategory.hom g)
t : X → ↑Y.toTop := g' ∘ ⇑(ConcreteCategory.hom f) ∘ pure
h : Ultrafilter X → ↑Y.toTop := Ultrafilter.extend t
⊢ ∃ f', f' ≫ g = f

Tactic:
have hh : Continuous h := continuous_ultrafilter_extend _

Goal state after:
X : Type u_1
Y Z : CompHaus
f : of (Ultrafilter X) ⟶ Z
g : Y ⟶ Z
hg : Surjective ⇑(ConcreteCategory.hom g)
g' : (fun X ↦ ↑X.toTop) Z → (fun X ↦ ↑X.toTop) Y
hg' : RightInverse g' ⇑(ConcreteCategory.hom g)
t : X → ↑Y.toTop := g' ∘ ⇑(ConcreteCategory.hom f) ∘ pure
h : Ultrafilter X → ↑Y.toTop := Ultrafilter.extend t
hh : Continuous h
⊢ ∃ f', f' ≫ g = f
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₁ : E
⊢ ∀ ⦃a₂ : E⦄, ρ x₁ = ρ a₂ → x₁ = a₂

Tactic:
x₂

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
⊢ ρ x₁ = ρ x₂ → x₁ = x₂
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: X✝ : Type u
inst✝¹ : TopologicalSpace X✝
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
h₀ : ∀ (i : ι), ExtremallyDisconnected (X i)
s : Set ((i : ι) × X i)
⊢ IsOpen s → IsOpen (closure s)

Tactic:
hs

Goal state after:
X✝ : Type u
inst✝¹ : TopologicalSpace X✝
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
h₀ : ∀ (i : ι), ExtremallyDisconnected (X i)
s : Set ((i : ι) × X i)
hs : IsOpen s
⊢ IsOpen (closure s)
Module: Mathlib.Topology.Category.TopCat.Limits.Cofiltered

Goal state before:
pp: case insert
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
S : Set (Set ↑(F.obj j))
a : J
E : Finset J
_ha : a ∉ E
hh1 :
  ∀ (P : J → Set ↑(F.obj j)),
    Set.univ ∈ S → (∀ (A B : Set ↑(F.obj j)), A ∈ S → B ∈ S → A ∩ B ∈ S) → (∀ e ∈ E, P e ∈ S) → ⋂ e ∈ E, P e ∈ S
⊢ ∀ (P : J → Set ↑(F.obj j)),
    Set.univ ∈ S →
      (∀ (A B : Set ↑(F.obj j)), A ∈ S → B ∈ S → A ∩ B ∈ S) → (∀ e ∈ insert a E, P e ∈ S) → ⋂ e ∈ insert a E, P e ∈ S

Tactic:
intro hh2 hh3 hh4 hh5

Goal state after:
case insert
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
S : Set (Set ↑(F.obj j))
a : J
E : Finset J
_ha : a ∉ E
hh1 :
  ∀ (P : J → Set ↑(F.obj j)),
    Set.univ ∈ S → (∀ (A B : Set ↑(F.obj j)), A ∈ S → B ∈ S → A ∩ B ∈ S) → (∀ e ∈ E, P e ∈ S) → ⋂ e ∈ E, P e ∈ S
hh2 : J → Set ↑(F.obj j)
hh3 : Set.univ ∈ S
hh4 : ∀ (A B : Set ↑(F.obj j)), A ∈ S → B ∈ S → A ∩ B ∈ S
hh5 : ∀ e ∈ insert a E, hh2 e ∈ S
⊢ ⋂ e ∈ insert a E, hh2 e ∈ S
Module: Mathlib.Topology.Category.Profinite.CofilteredLimit

Goal state before:
pp: case refine_3.refine_1
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
s : ↑S
⊢ s ∈ G → IsClopen (W s)

Tactic:
hs

Goal state after:
case refine_3.refine_1
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
s : ↑S
hs : s ∈ G
⊢ IsClopen (W s)
Module: Mathlib.Topology.Category.LightProfinite.Limits

Goal state before:
pp: X Y Z : LightProfinite
f : X ⟶ Z
g : Y ⟶ Z
h : Function.Surjective ⇑(ConcreteCategory.hom g)
x : ↑X.toTop
y : ↑Y.toTop
hy : (ConcreteCategory.hom g) y = (ConcreteCategory.hom f) x
⊢ ∃ a, (ConcreteCategory.hom (CompHausLike.pullback.fst f g)) a = x

Tactic:
exact ⟨⟨⟨x, y⟩, hy.symm⟩, rfl⟩

Goal state after:
Module: Mathlib.Condensed.TopComparison

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
G : C ⥤ TopCat
X : Type w'
inst✝² : TopologicalSpace X
Z B : C
π : Z ⟶ B
inst✝¹ : HasPullback π π
inst✝ : PreservesLimit (cospan π π) G
a : C(↑(G.obj Z), X)
ha : ⇑a ∘ ⇑(ConcreteCategory.hom (G.map (pullback.fst π π))) = ⇑a ∘ ⇑(ConcreteCategory.hom (G.map (pullback.snd π π)))
⊢ Function.FactorsThrough ⇑a ⇑(ConcreteCategory.hom (G.map π))

Tactic:
intro x y hxy
  let xy : G.obj (pullback π π) := (PreservesPullback.iso G π π).inv <|
    (TopCat.pullbackIsoProdSubtype (G.map π) (G.map π)).inv ⟨(x, y), hxy⟩
  have ha' := congr_fun ha xy
  dsimp at ha'
  have h₁ : ∀ y, G.map (pullback.fst _ _) ((PreservesPullback.iso G π π).inv y) =
      pullback.fst (G.map π) (G.map π) y := by
    simp only [← PreservesPullback.iso_inv_fst]; intro y; rfl
  have h₂ : ∀ y, G.map (pullback.snd _ _) ((PreservesPullback.iso G π π).inv y) =
      pullback.snd (G.map π) (G.map π) y := by
    simp only [← PreservesPullback.iso_inv_snd]; intro y; rfl
  rw [h₁, h₂, TopCat.pullbackIsoProdSubtype_inv_fst_apply,
    TopCat.pullbackIsoProdSubtype_inv_snd_apply] at ha'
  simpa using ha'

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: q : Λ'
⊢ q ∈ trStmts₁ q

Tactic:
induction q

Goal state after:
case move
p✝ : Γ' → Bool
k₁✝ k₂✝ : K'
q✝ : Λ'
q_ih✝ : q✝ ∈ trStmts₁ q✝
⊢ Λ'.move p✝ k₁✝ k₂✝ q✝ ∈ trStmts₁ (Λ'.move p✝ k₁✝ k₂✝ q✝)

case clear
p✝ : Γ' → Bool
k✝ : K'
q✝ : Λ'
q_ih✝ : q✝ ∈ trStmts₁ q✝
⊢ Λ'.clear p✝ k✝ q✝ ∈ trStmts₁ (Λ'.clear p✝ k✝ q✝)

case copy
q✝ : Λ'
q_ih✝ : q✝ ∈ trStmts₁ q✝
⊢ q✝.copy ∈ trStmts₁ q✝.copy

case push
k✝ : K'
s✝ : Option Γ' → Option Γ'
q✝ : Λ'
q_ih✝ : q✝ ∈ trStmts₁ q✝
⊢ Λ'.push k✝ s✝ q✝ ∈ trStmts₁ (Λ'.push k✝ s✝ q✝)

case read
f✝ : Option Γ' → Λ'
f_ih✝ : ∀ (a : Option Γ'), f✝ a ∈ trStmts₁ (f✝ a)
⊢ Λ'.read f✝ ∈ trStmts₁ (Λ'.read f✝)

case succ
q✝ : Λ'
q_ih✝ : q✝ ∈ trStmts₁ q✝
⊢ q✝.succ ∈ trStmts₁ q✝.succ

case pred
q₁✝ q₂✝ : Λ'
q₁_ih✝ : q₁✝ ∈ trStmts₁ q₁✝
q₂_ih✝ : q₂✝ ∈ trStmts₁ q₂✝
⊢ q₁✝.pred q₂✝ ∈ trStmts₁ (q₁✝.pred q₂✝)

case ret
k✝ : Cont'
⊢ Λ'.ret k✝ ∈ trStmts₁ (Λ'.ret k✝)
Module: Mathlib.Topology.Category.Profinite.CofilteredLimit

Goal state before:
pp: case refine_1
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) α
S : DiscreteQuotient ↑C.pt.toTop := f.discreteQuotient
ff : Quotient S.toSetoid → α := ⇑f.lift
h✝ : IsEmpty (Quotient S.toSetoid)
this : ∃ j, IsEmpty ↑(F.obj j).toTop
j : J
hj : IsEmpty ↑(F.obj j).toTop
A : Set α
⊢ IsOpen ((fun a ↦ hj.elim a) ⁻¹' A)

pp: case refine_2
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) α
S : DiscreteQuotient ↑C.pt.toTop := f.discreteQuotient
ff : Quotient S.toSetoid → α := ⇑f.lift
h✝ : IsEmpty (Quotient S.toSetoid)
this : ∃ j, IsEmpty ↑(F.obj j).toTop
j : J
hj : IsEmpty ↑(F.obj j).toTop
⊢ f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) { toFun := fun a ↦ hj.elim a, isLocallyConstant := ⋯ }

Tactic:
· convert! isOpen_empty
        ext x
        exact hj.elim x

Goal state after:
case refine_2
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) α
S : DiscreteQuotient ↑C.pt.toTop := f.discreteQuotient
ff : Quotient S.toSetoid → α := ⇑f.lift
h✝ : IsEmpty (Quotient S.toSetoid)
this : ∃ j, IsEmpty ↑(F.obj j).toTop
j : J
hj : IsEmpty ↑(F.obj j).toTop
⊢ f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) { toFun := fun a ↦ hj.elim a, isLocallyConstant := ⋯ }
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case cons.refine_2
S : Finset Λ'
f fs : Code
IHf : ∀ {k : Cont'}, codeSupp f k ⊆ S → Supports (codeSupp' f k) S
IHfs : ∀ {k : Cont'}, codeSupp fs k ⊆ S → Supports (codeSupp' fs k) S
k : Cont'
H : codeSupp (f.cons fs) k ⊆ S
H' : trStmts₁ (trNormal (f.cons fs) k) ⊆ S ∧ codeSupp f (Cont'.cons₁ fs k) ⊆ S
h✝ :
  codeSupp' f (Cont'.cons₁ fs k) ∪
      (trStmts₁
          (move₂ (fun x ↦ false) main aux
            (move₂ (fun s ↦ decide (s = Γ'.consₗ)) stack main
              (move₂ (fun x ↦ false) aux stack (trNormal fs k.cons₂)))) ∪
        (codeSupp' fs k.cons₂ ∪ trStmts₁ (head stack (Λ'.ret k)))) ⊆
    S
h : codeSupp' fs k.cons₂ ∪ trStmts₁ (head stack (Λ'.ret k)) ⊆ S
⊢ Supports (codeSupp' fs k.cons₂ ∪ trStmts₁ (head stack (Λ'.ret k))) S

Tactic:
refine supports_union.2 ⟨IHfs ?_, ?_⟩

Goal state after:
case cons.refine_2.refine_1
S : Finset Λ'
f fs : Code
IHf : ∀ {k : Cont'}, codeSupp f k ⊆ S → Supports (codeSupp' f k) S
IHfs : ∀ {k : Cont'}, codeSupp fs k ⊆ S → Supports (codeSupp' fs k) S
k : Cont'
H : codeSupp (f.cons fs) k ⊆ S
H' : trStmts₁ (trNormal (f.cons fs) k) ⊆ S ∧ codeSupp f (Cont'.cons₁ fs k) ⊆ S
h✝ :
  codeSupp' f (Cont'.cons₁ fs k) ∪
      (trStmts₁
          (move₂ (fun x ↦ false) main aux
            (move₂ (fun s ↦ decide (s = Γ'.consₗ)) stack main
              (move₂ (fun x ↦ false) aux stack (trNormal fs k.cons₂)))) ∪
        (codeSupp' fs k.cons₂ ∪ trStmts₁ (head stack (Λ'.ret k)))) ⊆
    S
h : codeSupp' fs k.cons₂ ∪ trStmts₁ (head stack (Λ'.ret k)) ⊆ S
⊢ codeSupp fs k.cons₂ ⊆ S

case cons.refine_2.refine_2
S : Finset Λ'
f fs : Code
IHf : ∀ {k : Cont'}, codeSupp f k ⊆ S → Supports (codeSupp' f k) S
IHfs : ∀ {k : Cont'}, codeSupp fs k ⊆ S → Supports (codeSupp' fs k) S
k : Cont'
H : codeSupp (f.cons fs) k ⊆ S
H' : trStmts₁ (trNormal (f.cons fs) k) ⊆ S ∧ codeSupp f (Cont'.cons₁ fs k) ⊆ S
h✝ :
  codeSupp' f (Cont'.cons₁ fs k) ∪
      (trStmts₁
          (move₂ (fun x ↦ false) main aux
            (move₂ (fun s ↦ decide (s = Γ'.consₗ)) stack main
              (move₂ (fun x ↦ false) aux stack (trNormal fs k.cons₂)))) ∪
        (codeSupp' fs k.cons₂ ∪ trStmts₁ (head stack (Λ'.ret k)))) ⊆
    S
h : codeSupp' fs k.cons₂ ∪ trStmts₁ (head stack (Λ'.ret k)) ⊆ S
⊢ Supports (trStmts₁ (head stack (Λ'.ret k))) S
Module: Mathlib.Condensed.Discrete.Characterization

Goal state before:
pp: R : Type (u + 1)
inst✝ : Ring R
M : CondensedMod R
tfae_1_iff_2 : Condensed.IsDiscrete M ↔ IsIso ((Condensed.discreteUnderlyingAdj (ModuleCat R)).counit.app M)
tfae_1_iff_3 : Condensed.IsDiscrete M ↔ (Condensed.discrete (ModuleCat R)).essImage M
tfae_1_iff_4 : Condensed.IsDiscrete M ↔ (functor R).essImage M
tfae_1_iff_5 : Condensed.IsDiscrete M ↔ IsIso ((LocallyConstant.adjunction R).counit.app M)
tfae_1_iff_6 :
  Condensed.IsDiscrete M ↔
    Sheaf.IsConstant (coherentTopology Profinite)
      ((Condensed.ProfiniteCompHaus.equivalence (ModuleCat R)).inverse.obj M)
tfae_7_to_1 :
  (∀ (S : Profinite), Nonempty (IsColimit ((profiniteToCompHaus.op ⋙ M.obj).mapCocone S.asLimitCone.op))) →
    Condensed.IsDiscrete M
h : Condensed.IsDiscrete M
S : Profinite
⊢ Nonempty (IsColimit ((profiniteToCompHaus.op ⋙ M.obj).mapCocone S.asLimitCone.op))

Tactic:
rw [isDiscrete_iff_isDiscrete_forget, ((CondensedSet.isDiscrete_tfae _).out 0 6 :)] at h

Goal state after:
R : Type (u + 1)
inst✝ : Ring R
M : CondensedMod R
tfae_1_iff_2 : Condensed.IsDiscrete M ↔ IsIso ((Condensed.discreteUnderlyingAdj (ModuleCat R)).counit.app M)
tfae_1_iff_3 : Condensed.IsDiscrete M ↔ (Condensed.discrete (ModuleCat R)).essImage M
tfae_1_iff_4 : Condensed.IsDiscrete M ↔ (functor R).essImage M
tfae_1_iff_5 : Condensed.IsDiscrete M ↔ IsIso ((LocallyConstant.adjunction R).counit.app M)
tfae_1_iff_6 :
  Condensed.IsDiscrete M ↔
    Sheaf.IsConstant (coherentTopology Profinite)
      ((Condensed.ProfiniteCompHaus.equivalence (ModuleCat R)).inverse.obj M)
tfae_7_to_1 :
  (∀ (S : Profinite), Nonempty (IsColimit ((profiniteToCompHaus.op ⋙ M.obj).mapCocone S.asLimitCone.op))) →
    Condensed.IsDiscrete M
h :
  ∀ (S : Profinite),
    Nonempty (IsColimit ((profiniteToCompHaus.op ⋙ ((Condensed.forget R).obj M).obj).mapCocone S.asLimitCone.op))
S : Profinite
⊢ Nonempty (IsColimit ((profiniteToCompHaus.op ⋙ M.obj).mapCocone S.asLimitCone.op))
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: S : Profinite
F : Profiniteᵒᵖ ⥤ Type (u + 1)
hF : IsColimit (F.mapCocone S.asLimitCone.op)
⊢ (lanPresheafIso hF).hom =
    colimit.desc (CostructuredArrow.proj toProfinite.op (Opposite.op S) ⋙ toProfinite.op ⋙ F)
      (Profinite.Extend.cocone F S)

Tactic:
by
  simp [lanPresheafIso, Final.colimitIso]
  rfl

Goal state after:
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: S : LightProfinite
F : LightProfiniteᵒᵖ ⥤ Type u
hF : IsColimit (F.mapCocone (coconeRightOpOfCone S.asLimitCone))
⊢ (lanPresheafIso hF).hom =
    colimit.desc (CostructuredArrow.proj toLightProfinite.op (Opposite.op S) ⋙ toLightProfinite.op ⋙ F)
      (LightProfinite.Extend.cocone F S)

Tactic:
by
  simp [lanPresheafIso, Final.colimitIso]
  rfl

Goal state after:
Module: Mathlib.Control.Fold

Goal state before:
pp: α β : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
f : α → β → β
xs : t α
x : β
⊢ foldr f x xs = (TypeCat.Hom.hom ((Foldr.ofFreeMonoid f) (FreeMonoid.ofList (toList xs)))) x

Tactic:
rw [toList_spec, foldr, Foldr.get, FreeMonoid.ofList_toList, foldMap_hom_free,
    foldr.ofFreeMonoid_comp_of]

Goal state after:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: case neg
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∀ (x : ℕ) (x_1 : β a), x_1 ∉ approx (⇑f) x a
x✝ : ℕ
⊢ b ∉ approx (⇑f) x✝ a

Tactic:
apply h₀

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

Goal state before:
pp: case succ
τ : Type u
n : ℕ
ih : ∀ {p : Fin n → Type u} (f : ((i : Fin n) → p i) → τ) (args : (i : Fin n) → p i), (curry f).uncurry args = f args
p : Fin (n + 1) → Type u
f : ((i : Fin (n + 1)) → p i) → τ
args : (i : Fin (n + 1)) → p i
⊢ (curry f).uncurry args = f args

Tactic:
exact Eq.trans (ih _ _) (congrArg f (Fin.cons_self_tail args))

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: case e_4
α : Type u
β : α → Type v
inst✝ : IsEmpty α
e : FinEnum α
⊢ (fun a b ↦ decEq a b) = fun a b ↦ decidableEq_of_subsingleton a b

Tactic:
funext x

Goal state after:
case e_4
α : Type u
β : α → Type v
inst✝ : IsEmpty α
e : FinEnum α
x : α
⊢ (fun b ↦ decEq x b) = fun b ↦ decidableEq_of_subsingleton x b
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
xs : List (Sigma β)
⊢ a ∈ xs.toFinmap ↔ ∃ b, ⟨a, b⟩ ∈ xs

Tactic:
by
  induction xs with
  | nil => simp only [toFinmap_nil, notMem_empty, not_mem_nil, exists_false]
  | cons x xs =>
    obtain ⟨fst_i, snd_i⟩ := x
    simp only [toFinmap_cons, *, exists_or, mem_cons, mem_insert, exists_and_left, Sigma.mk.inj_iff]
    refine (or_congr_left <| and_iff_left_of_imp ?_).symm
    rintro rfl
    simp only [exists_eq, heq_iff_eq]

Goal state after:
Module: Mathlib.Data.Finset.Functor

Goal state before:
pp: α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
s : Finset α✝
t : Finset β✝
⊢ s <* t = const β✝ <$> s <*> t

Tactic:
rw [seq_def, fmap_def, seqLeft_def]
      obtain rfl | ht := t.eq_empty_or_nonempty
      · simp_rw [image_empty, if_true]
        exact (sup_bot _).symm
      · ext a
        rw [if_neg ht.ne_empty, mem_sup]
        refine ⟨fun ha => ⟨const _ a, mem_image_of_mem _ ha, mem_image_const_self.2 ht⟩, ?_⟩
        rintro ⟨f, hf, ha⟩
        rw [mem_image] at hf ha
        obtain ⟨b, hb, rfl⟩ := hf
        obtain ⟨_, _, rfl⟩ := ha
        exact hb

Goal state after:
Module: Mathlib.Data.Finsupp.BigOperators

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Multiset (ι →₀ M)
⊢ s.sum.support ⊆ (map Finsupp.support s).sup

Tactic:
by
  induction s using Quot.inductionOn
  simpa only [Multiset.quot_mk_to_coe'', Multiset.sum_coe, Multiset.map_coe, Multiset.sup_coe,
    List.foldr_map] using! List.support_sum_subset _

Goal state after:
Module: Mathlib.Data.Finsupp.NeLocus

Goal state before:
pp: α : Type u_1
N : Type u_3
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : AddGroup N
f₁ f₂ g : α →₀ N
⊢ (f₁ - g).neLocus (f₂ - g) = f₁.neLocus f₂

Tactic:
by
  simpa only [sub_eq_add_neg] using neLocus_add_right _ _ _

Goal state after:
Module: Mathlib.Data.Holor

Goal state before:
pp: case refine_2
α : Type
d : ℕ
ds : List ℕ
inst✝ : AddCommMonoid α
β : Type
i : ℕ
hid : i < d
s : Finset β
f : β → Holor α (d :: ds)
this : DecidableEq β := Classical.decEq β
⊢ ∀ (a : β) (s : Finset β),
    a ∉ s →
      ∑ x ∈ s, (f x).slice i hid = (∑ x ∈ s, f x).slice i hid →
        ∑ x ∈ insert a s, (f x).slice i hid = (∑ x ∈ insert a s, f x).slice i hid

Tactic:
intro _ _ h_not_in ih
    rw [Finset.sum_insert h_not_in, ih, slice_add, Finset.sum_insert h_not_in]

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

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
⊢ takeWhile p l = l ↔ ∀ (x : α), x ∈ l → p x = true

Tactic:
induction l with
  | nil => simp
  | cons x xs IH => by_cases hp : p x <;> simp [hp, IH]

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

Goal state before:
pp: case append_singleton.succ
α : Type u_1
xs : List α
x : α
IH : ∀ (n : ℕ), drop (xs.length - n) xs = (take n xs.reverse).reverse
n✝ : ℕ
⊢ drop ((xs ++ [x]).length - (n✝ + 1)) (xs ++ [x]) = (take (n✝ + 1) (xs ++ [x]).reverse).reverse

Tactic:
simp [drop_append, IH]

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

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
⊢ (l₁ ++ l₂).rdrop l₂.length = l₁

Tactic:
by
  rw [rdrop_eq_reverse_drop_reverse, ← length_reverse,
      reverse_append, drop_left, reverse_reverse]

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

Goal state before:
pp: case inr
n m l : ℕ
hlm : l ≤ m
hln : l ≤ n
⊢ filter (fun x ↦ decide (x < l)) (Ico n m) = Ico n l

Tactic:
rw [eq_nil_of_le hln, filter_lt_of_le_bot hln]

Goal state after: