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

Goal state before:
pp: case branch.false
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
l : Λ
p : σ → Bool
q₁ q₂ : TM2.Stmt Γ Λ σ
IH₁ :
  ∀ {v : σ} {S : (k : K) → List (Γ k)} (L : ListBlank ((k : K) → Option (Γ k))),
    (∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse) →
      ∃ b,
        TrCfg (TM2.stepAux q₁ v S) b ∧
          Reaches (TM1.step (tr M)) (TM1.stepAux (trNormal q₁) v (Tape.mk' ∅ (addBottom L))) b
IH₂ :
  ∀ {v : σ} {S : (k : K) → List (Γ k)} (L : ListBlank ((k : K) → Option (Γ k))),
    (∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse) →
      ∃ b,
        TrCfg (TM2.stepAux q₂ v S) b ∧
          Reaches (TM1.step (tr M)) (TM1.stepAux (trNormal q₂) v (Tape.mk' ∅ (addBottom L))) b
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hT : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse
⊢ ∃ b,
    TrCfg (bif false then TM2.stepAux q₁ v S else TM2.stepAux q₂ v S) b ∧
      Reaches (TM1.step (tr M))
        (bif false then TM1.stepAux (trNormal q₁) v (Tape.mk' ∅ (addBottom L))
        else TM1.stepAux (trNormal q₂) v (Tape.mk' ∅ (addBottom L)))
        b

Tactic:
exact IH₂ _ hT

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

Goal state before:
pp: case refine_3
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝¹ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst✝ : Inhabited Λ
S : Finset Λ
ss : TM2.Supports M S
⊢ ∀ (p : σ → Bool) (q₁ q₂ : TM2.Stmt Γ Λ σ),
    (TM2.SupportsStmt S q₁ →
        (∀ x ∈ trStmts₁ q₁, x ∈ trSupp M S) →
          TM1.SupportsStmt (trSupp M S) (trNormal q₁) ∧ ∀ l' ∈ trStmts₁ q₁, TM1.SupportsStmt (trSupp M S) (tr M l')) →
      (TM2.SupportsStmt S q₂ →
          (∀ x ∈ trStmts₁ q₂, x ∈ trSupp M S) →
            TM1.SupportsStmt (trSupp M S) (trNormal q₂) ∧ ∀ l' ∈ trStmts₁ q₂, TM1.SupportsStmt (trSupp M S) (tr M l')) →
        TM2.SupportsStmt S (TM2.Stmt.branch p q₁ q₂) →
          (∀ x ∈ trStmts₁ (TM2.Stmt.branch p q₁ q₂), x ∈ trSupp M S) →
            TM1.SupportsStmt (trSupp M S) (trNormal (TM2.Stmt.branch p q₁ q₂)) ∧
              ∀ l' ∈ trStmts₁ (TM2.Stmt.branch p q₁ q₂), TM1.SupportsStmt (trSupp M S) (tr M l')

pp: case refine_4
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝¹ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst✝ : Inhabited Λ
S : Finset Λ
ss : TM2.Supports M S
⊢ ∀ (l : σ → Λ),
    TM2.SupportsStmt S (TM2.Stmt.goto l) →
      (∀ x ∈ trStmts₁ (TM2.Stmt.goto l), x ∈ trSupp M S) →
        TM1.SupportsStmt (trSupp M S) (trNormal (TM2.Stmt.goto l)) ∧
          ∀ l' ∈ trStmts₁ (TM2.Stmt.goto l), TM1.SupportsStmt (trSupp M S) (tr M l')

pp: case refine_5
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝¹ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst✝ : Inhabited Λ
S : Finset Λ
ss : TM2.Supports M S
⊢ TM2.SupportsStmt S TM2.Stmt.halt →
    (∀ x ∈ trStmts₁ TM2.Stmt.halt, x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal TM2.Stmt.halt) ∧
        ∀ l' ∈ trStmts₁ TM2.Stmt.halt, TM1.SupportsStmt (trSupp M S) (tr M l')

Tactic:
· intro _ _ _ IH₁ IH₂ ss' sub -- branch
      unfold TM2to1.trStmts₁ at sub
      obtain ⟨IH₁₁, IH₁₂⟩ := IH₁ ss'.1 fun x hx ↦ sub x <| Finset.mem_union_left _ hx
      obtain ⟨IH₂₁, IH₂₂⟩ := IH₂ ss'.2 fun x hx ↦ sub x <| Finset.mem_union_right _ hx
      refine ⟨⟨IH₁₁, IH₂₁⟩, fun l h ↦ ?_⟩
      rw [trStmts₁] at h
      rcases Finset.mem_union.1 h with (h | h) <;> [exact IH₁₂ _ h; exact IH₂₂ _ h]

Goal state after:
case refine_4
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝¹ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst✝ : Inhabited Λ
S : Finset Λ
ss : TM2.Supports M S
⊢ ∀ (l : σ → Λ),
    TM2.SupportsStmt S (TM2.Stmt.goto l) →
      (∀ x ∈ trStmts₁ (TM2.Stmt.goto l), x ∈ trSupp M S) →
        TM1.SupportsStmt (trSupp M S) (trNormal (TM2.Stmt.goto l)) ∧
          ∀ l' ∈ trStmts₁ (TM2.Stmt.goto l), TM1.SupportsStmt (trSupp M S) (tr M l')

case refine_5
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝¹ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst✝ : Inhabited Λ
S : Finset Λ
ss : TM2.Supports M S
⊢ TM2.SupportsStmt S TM2.Stmt.halt →
    (∀ x ∈ trStmts₁ TM2.Stmt.halt, x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal TM2.Stmt.halt) ∧
        ∀ l' ∈ trStmts₁ TM2.Stmt.halt, TM1.SupportsStmt (trSupp M S) (tr M l')
Module: Mathlib.Topology.Category.LightProfinite.Basic

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
inst✝ : CountableCategory J
F : J ⥤ LightProfinite
S : Cone F
x✝ : S.pt ⟶ (limitCone F).pt
h : ∀ (j : J), x✝ ≫ (limitCone F).π.app j = S.π.app j
⊢ x✝ =
    ConcreteCategory.ofHom
      (TopCat.Hom.hom
        ((CompHaus.limitConeIsLimit (F ⋙ lightProfiniteToCompHaus)).lift (lightProfiniteToCompHaus.mapCone S)).hom)

Tactic:
apply lightProfiniteToCompHaus.map_injective

Goal state after:
J : Type v
inst✝¹ : SmallCategory J
inst✝ : CountableCategory J
F : J ⥤ LightProfinite
S : Cone F
x✝ : S.pt ⟶ (limitCone F).pt
h : ∀ (j : J), x✝ ≫ (limitCone F).π.app j = S.π.app j
⊢ lightProfiniteToCompHaus.map x✝ =
    lightProfiniteToCompHaus.map
      (ConcreteCategory.ofHom
        (TopCat.Hom.hom
          ((CompHaus.limitConeIsLimit (F ⋙ lightProfiniteToCompHaus)).lift (lightProfiniteToCompHaus.mapCone S)).hom))
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 π π)))
x y : ↑(G.obj Z)
hxy : (ConcreteCategory.hom (G.map π)) x = (ConcreteCategory.hom (G.map π)) y
xy : ↑(G.obj (pullback π π)) :=
  (ConcreteCategory.hom (PreservesPullback.iso G π π).inv)
    ((ConcreteCategory.hom (TopCat.pullbackIsoProdSubtype (G.map π) (G.map π)).inv) ⟨(x, y), hxy⟩)
ha' :
  a ((ConcreteCategory.hom (G.map (pullback.fst π π))) xy) = a ((ConcreteCategory.hom (G.map (pullback.snd π π))) xy)
h₁ :
  ∀ (y : ↑(pullback (G.map π) (G.map π))),
    (ConcreteCategory.hom (G.map (pullback.fst π π))) ((ConcreteCategory.hom (PreservesPullback.iso G π π).inv) y) =
      (ConcreteCategory.hom (pullback.fst (G.map π) (G.map π))) y
h₂ :
  ∀ (y : ↑(pullback (G.map π) (G.map π))),
    (ConcreteCategory.hom (G.map (pullback.snd π π))) ((ConcreteCategory.hom (PreservesPullback.iso G π π).inv) y) =
      (ConcreteCategory.hom (pullback.snd (G.map π) (G.map π))) y
⊢ a x = a y

Tactic:
rw [h₁, h₂, TopCat.pullbackIsoProdSubtype_inv_fst_apply,
    TopCat.pullbackIsoProdSubtype_inv_snd_apply] at ha'

Goal state after:
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 π π)))
x y : ↑(G.obj Z)
hxy : (ConcreteCategory.hom (G.map π)) x = (ConcreteCategory.hom (G.map π)) y
xy : ↑(G.obj (pullback π π)) :=
  (ConcreteCategory.hom (PreservesPullback.iso G π π).inv)
    ((ConcreteCategory.hom (TopCat.pullbackIsoProdSubtype (G.map π) (G.map π)).inv) ⟨(x, y), hxy⟩)
ha' : a (↑⟨(x, y), hxy⟩).1 = a (↑⟨(x, y), hxy⟩).2
h₁ :
  ∀ (y : ↑(pullback (G.map π) (G.map π))),
    (ConcreteCategory.hom (G.map (pullback.fst π π))) ((ConcreteCategory.hom (PreservesPullback.iso G π π).inv) y) =
      (ConcreteCategory.hom (pullback.fst (G.map π) (G.map π))) y
h₂ :
  ∀ (y : ↑(pullback (G.map π) (G.map π))),
    (ConcreteCategory.hom (G.map (pullback.snd π π))) ((ConcreteCategory.hom (PreservesPullback.iso G π π).inv) y) =
      (ConcreteCategory.hom (pullback.snd (G.map π) (G.map π))) y
⊢ a x = a y
Module: Mathlib.Topology.Category.Profinite.Extend

Goal state before:
pp: I : Type u
inst✝¹ : SmallCategory I
inst✝ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
hc : IsLimit c
X : FintypeCat
f : c.pt ⟶ toProfinite.obj X
this : DiscreteTopology ↑(toProfinite.obj X).toTop
f' : LocallyConstant ↑c.pt.toTop ↑(toProfinite.obj X).toTop :=
  { toFun := ⇑(ConcreteCategory.hom f), isLocallyConstant := ⋯ }
⊢ ∃ i g, f = c.π.app i ≫ toProfinite.map g

Tactic:
obtain ⟨i, g, h⟩ := exists_locallyConstant.{_, u} c hc f'

Goal state after:
I : Type u
inst✝¹ : SmallCategory I
inst✝ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
hc : IsLimit c
X : FintypeCat
f : c.pt ⟶ toProfinite.obj X
this : DiscreteTopology ↑(toProfinite.obj X).toTop
f' : LocallyConstant ↑c.pt.toTop ↑(toProfinite.obj X).toTop :=
  { toFun := ⇑(ConcreteCategory.hom f), isLocallyConstant := ⋯ }
i : I
g : LocallyConstant ↑((F ⋙ toProfinite).obj i).toTop ↑(toProfinite.obj X).toTop
h : f' = LocallyConstant.comap (TopCat.Hom.hom (c.π.app i).hom) g
⊢ ∃ i g, f = c.π.app i ≫ toProfinite.map g
Module: Mathlib.Topology.Category.LightProfinite.Extend

Goal state before:
pp: F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
hc : IsLimit c
inst✝ : ∀ (i : ℕᵒᵖ), Epi (c.π.app i)
this✝¹ : (functor c).Initial
this✝ : (StructuredArrow.toCostructuredArrow toLightProfinite c.pt).IsEquivalence
this : (functor c).rightOp.Final
⊢ (functorOp c).Final

Tactic:
exact Functor.final_comp (functor c).rightOp _

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

Goal state before:
pp: X : CondensedSet
tfae_1_iff_2 : Condensed.IsDiscrete X ↔ IsIso ((discreteUnderlyingAdj (Type (u + 1))).counit.app X)
tfae_1_iff_3 : Condensed.IsDiscrete X ↔ (discrete (Type (u + 1))).essImage X
tfae_1_iff_4 : Condensed.IsDiscrete X ↔ LocallyConstant.functor.essImage X
tfae_1_iff_5 : Condensed.IsDiscrete X ↔ IsIso (LocallyConstant.adjunction.counit.app X)
tfae_1_iff_6 :
  Condensed.IsDiscrete X ↔
    Sheaf.IsConstant (coherentTopology Profinite) ((ProfiniteCompHaus.equivalence (Type (u + 1))).inverse.obj X)
tfae_7_to_4 :
  (∀ (S : Profinite), Nonempty (IsColimit ((profiniteToCompHaus.op ⋙ X.obj).mapCocone S.asLimitCone.op))) →
    LocallyConstant.functor.essImage X
⊢ [Condensed.IsDiscrete X, IsIso ((discreteUnderlyingAdj (Type (u + 1))).counit.app X),
      (discrete (Type (u + 1))).essImage X, LocallyConstant.functor.essImage X,
      IsIso (LocallyConstant.adjunction.counit.app X),
      Sheaf.IsConstant (coherentTopology Profinite) ((ProfiniteCompHaus.equivalence (Type (u + 1))).inverse.obj X),
      ∀ (S : Profinite), Nonempty (IsColimit ((profiniteToCompHaus.op ⋙ X.obj).mapCocone S.asLimitCone.op))].TFAE

Tactic:
tfae_have 4 → 7 := fun ⟨Y, ⟨i⟩⟩ S ↦
    ⟨IsColimit.mapCoconeEquiv (isoWhiskerLeft profiniteToCompHaus.op
      ((sheafToPresheaf _ _).mapIso i))
      (Condensed.isColimitLocallyConstantPresheafDiagram Y S)⟩

Goal state after:
X : CondensedSet
tfae_1_iff_2 : Condensed.IsDiscrete X ↔ IsIso ((discreteUnderlyingAdj (Type (u + 1))).counit.app X)
tfae_1_iff_3 : Condensed.IsDiscrete X ↔ (discrete (Type (u + 1))).essImage X
tfae_1_iff_4 : Condensed.IsDiscrete X ↔ LocallyConstant.functor.essImage X
tfae_1_iff_5 : Condensed.IsDiscrete X ↔ IsIso (LocallyConstant.adjunction.counit.app X)
tfae_1_iff_6 :
  Condensed.IsDiscrete X ↔
    Sheaf.IsConstant (coherentTopology Profinite) ((ProfiniteCompHaus.equivalence (Type (u + 1))).inverse.obj X)
tfae_7_to_4 :
  (∀ (S : Profinite), Nonempty (IsColimit ((profiniteToCompHaus.op ⋙ X.obj).mapCocone S.asLimitCone.op))) →
    LocallyConstant.functor.essImage X
tfae_4_to_7 :
  LocallyConstant.functor.essImage X →
    ∀ (S : Profinite), Nonempty (IsColimit ((profiniteToCompHaus.op ⋙ X.obj).mapCocone S.asLimitCone.op))
⊢ [Condensed.IsDiscrete X, IsIso ((discreteUnderlyingAdj (Type (u + 1))).counit.app X),
      (discrete (Type (u + 1))).essImage X, LocallyConstant.functor.essImage X,
      IsIso (LocallyConstant.adjunction.counit.app X),
      Sheaf.IsConstant (coherentTopology Profinite) ((ProfiniteCompHaus.equivalence (Type (u + 1))).inverse.obj X),
      ∀ (S : Profinite), Nonempty (IsColimit ((profiniteToCompHaus.op ⋙ X.obj).mapCocone S.asLimitCone.op))].TFAE
Module: Mathlib.Condensed.Light.Epi

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
X Y : LightCondMod R
f : X ⟶ Y
inst✝ : Epi f
S : LightProfinite
p : (LightCondensed.free R).obj S.toCondensed ⟶ Y
this :
  ∀ (S : LightProfinite) (y : ((LightCondensed.forget R).obj Y).obj.obj (Opposite.op S)),
    ∃ S' φ,
      ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom φ)),
        ∃ x,
          (ConcreteCategory.hom (((LightCondensed.forget R).map f).hom.app (Opposite.op S'))) x =
            (ConcreteCategory.hom (((LightCondensed.forget R).obj Y).obj.map (Opposite.op φ))) y
⊢ ∃ T π g, Epi π ∧ (lightProfiniteToLightCondSet ⋙ LightCondensed.free R).map π ≫ p = g ≫ f

Tactic:
obtain ⟨T, π, hπ, x, hx⟩ := this S <| (coherentTopology LightProfinite).yonedaEquiv <|
    (LightCondensed.freeForgetAdjunction R).homEquiv S.toCondensed Y p

Goal state after:
R : Type u
inst✝¹ : Ring R
X Y : LightCondMod R
f : X ⟶ Y
inst✝ : Epi f
S : LightProfinite
p : (LightCondensed.free R).obj S.toCondensed ⟶ Y
this :
  ∀ (S : LightProfinite) (y : ((LightCondensed.forget R).obj Y).obj.obj (Opposite.op S)),
    ∃ S' φ,
      ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom φ)),
        ∃ x,
          (ConcreteCategory.hom (((LightCondensed.forget R).map f).hom.app (Opposite.op S'))) x =
            (ConcreteCategory.hom (((LightCondensed.forget R).obj Y).obj.map (Opposite.op φ))) y
T : LightProfinite
π : T ⟶ S
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
x : ((LightCondensed.forget R).obj X).obj.obj (Opposite.op T)
hx :
  (ConcreteCategory.hom (((LightCondensed.forget R).map f).hom.app (Opposite.op T))) x =
    (ConcreteCategory.hom (((LightCondensed.forget R).obj Y).obj.map (Opposite.op π)))
      ((coherentTopology LightProfinite).yonedaEquiv
        (((LightCondensed.freeForgetAdjunction R).homEquiv S.toCondensed Y) p))
⊢ ∃ T π g, Epi π ∧ (lightProfiniteToLightCondSet ⋙ LightCondensed.free R).map π ≫ p = g ≫ f
Module: Mathlib.Condensed.Light.Epi

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
X Y : LightCondMod R
f : X ⟶ Y
inst✝ : Epi f
S : LightProfinite
p : (LightCondensed.free R).obj S.toCondensed ⟶ Y
this :
  ∀ (S : LightProfinite) (y : ((LightCondensed.forget R).obj Y).obj.obj (Opposite.op S)),
    ∃ S' φ,
      ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom φ)),
        ∃ x,
          (ConcreteCategory.hom (((LightCondensed.forget R).map f).hom.app (Opposite.op S'))) x =
            (ConcreteCategory.hom (((LightCondensed.forget R).obj Y).obj.map (Opposite.op φ))) y
T : LightProfinite
π : T ⟶ S
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
x : ((LightCondensed.forget R).obj X).obj.obj (Opposite.op T)
hx :
  (ConcreteCategory.hom (((LightCondensed.forget R).map f).hom.app (Opposite.op T))) x =
    (ConcreteCategory.hom (((LightCondensed.forget R).obj Y).obj.map (Opposite.op π)))
      ((coherentTopology LightProfinite).yonedaEquiv
        (((LightCondensed.freeForgetAdjunction R).homEquiv S.toCondensed Y) p))
⊢ ∃ T π g, Epi π ∧ (lightProfiniteToLightCondSet ⋙ LightCondensed.free R).map π ≫ p = g ≫ f

Tactic:
refine ⟨T, π, ((LightCondensed.freeForgetAdjunction R).homEquiv T.toCondensed X).symm
    ((coherentTopology LightProfinite).yonedaEquiv.symm x),
    (LightProfinite.epi_iff_surjective π).mpr hπ, ?_⟩

Goal state after:
R : Type u
inst✝¹ : Ring R
X Y : LightCondMod R
f : X ⟶ Y
inst✝ : Epi f
S : LightProfinite
p : (LightCondensed.free R).obj S.toCondensed ⟶ Y
this :
  ∀ (S : LightProfinite) (y : ((LightCondensed.forget R).obj Y).obj.obj (Opposite.op S)),
    ∃ S' φ,
      ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom φ)),
        ∃ x,
          (ConcreteCategory.hom (((LightCondensed.forget R).map f).hom.app (Opposite.op S'))) x =
            (ConcreteCategory.hom (((LightCondensed.forget R).obj Y).obj.map (Opposite.op φ))) y
T : LightProfinite
π : T ⟶ S
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
x : ((LightCondensed.forget R).obj X).obj.obj (Opposite.op T)
hx :
  (ConcreteCategory.hom (((LightCondensed.forget R).map f).hom.app (Opposite.op T))) x =
    (ConcreteCategory.hom (((LightCondensed.forget R).obj Y).obj.map (Opposite.op π)))
      ((coherentTopology LightProfinite).yonedaEquiv
        (((LightCondensed.freeForgetAdjunction R).homEquiv S.toCondensed Y) p))
⊢ (lightProfiniteToLightCondSet ⋙ LightCondensed.free R).map π ≫ p =
    ((LightCondensed.freeForgetAdjunction R).homEquiv T.toCondensed X).symm
        ((coherentTopology LightProfinite).yonedaEquiv.symm x) ≫
      f
Module: Mathlib.Condensed.TopCatAdjunction

Goal state before:
pp: X Y : CondensedSet
f : X ⟶ Y
⊢ Continuous ⇑(ConcreteCategory.hom (f.hom.app (Opposite.op (of PUnit.{u + 1}))))

Tactic:
by
      rw [continuous_coinduced_dom]
      apply continuous_sigma
      intro ⟨S, x⟩
      simp only [Function.comp_apply, coinducingCoprod]
      rw [show (fun (a : S) ↦
          f.hom.app ⟨of PUnit⟩ (X.obj.map ((of PUnit.{u + 1}).const a).op x)) = _
        from funext fun a ↦ NatTrans.naturality_apply f.hom ((of PUnit.{u + 1}).const a).op x]
      exact continuous_coinducingCoprod Y _

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

Goal state before:
pp: t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
α β γ : Type u
g : α → F β
f : β → γ
x : t α
⊢ map f <$> traverse g x = traverse (map f ∘ g) x

Tactic:
by
  rw [map_eq_traverse_id f]
  refine (comp_traverse (pure ∘ f) g x).symm.trans ?_
  congr 1; apply Comp.applicative_comp_id

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

Goal state before:
pp: t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
G : Type u → Type u
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
g : α → β
h : β → G γ
x✝ : t α
⊢ traverse (h ∘ g) x✝ = (traverse h ∘ map g) x✝

Tactic:
rw [comp_apply, traverse_map]

Goal state after:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: case pos
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
i : ℕ
b : β x
hb : b ∈ approx (⇑f) i x
⊢ Part.fix (⇑f) x ≤ approx (⇑f) i x

Tactic:
intro b' h'

Goal state after:
case pos
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
i : ℕ
b : β x
hb : b ∈ approx (⇑f) i x
b' : β x
h' : b' ∈ Part.fix (⇑f) x
⊢ b' ∈ approx (⇑f) i x
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: m : Type u → Type v
m₁ : Type u₀ → Type v₀
m₂ : Type u₁ → Type v₁
α₁ r₁ : Type u₀
α₂ r₂ : Type u₁
F : m₁ r₁ ≃ m₂ r₂
G : α₁ ≃ α₂
f : ContT r₁ m₁ α₁
⊢ (fun f r ↦ F.symm (f fun x ↦ F (r (G.symm x)))) ((fun f r ↦ F (f fun x ↦ F.symm (r (G x)))) f) = f

Tactic:
funext r; simp

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)
x : α
hh : ∀ (i : ℕ) (b : β x), b ∉ approx (⇑f) i x
⊢ Part.fix (⇑f) x ≤ approx (⇑f) 0 x

Tactic:
intro b' h'

Goal state after:
case neg
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
hh : ∀ (i : ℕ) (b : β x), b ∉ approx (⇑f) i x
b' : β x
h' : b' ∈ Part.fix (⇑f) x
⊢ b' ∈ approx (⇑f) 0 x
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: m : Type u → Type v
m₁ : Type u₀ → Type v₀
m₂ : Type u₁ → Type v₁
α₁ r₁ : Type u₀
α₂ r₂ : Type u₁
F : m₁ r₁ ≃ m₂ r₂
G : α₁ ≃ α₂
f : ContT r₂ m₂ α₂
⊢ (fun f r ↦ F (f fun x ↦ F.symm (r (G x)))) ((fun f r ↦ F.symm (f fun x ↦ F (r (G.symm x)))) f) = f

Tactic:
funext r; simp

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
f : Π₀ (i : ι), α i
t : (i : ι) → Finset (α i)
inst✝ : (i : ι) → DecidableEq (α i)
⊢ f ∈ s.dfinsupp t ↔ f.support ⊆ s ∧ ∀ i ∈ s, f i ∈ t i

Tactic:
refine mem_map.trans ⟨?_, ?_⟩
  · rintro ⟨f, hf, rfl⟩
    rw [Function.Embedding.coeFn_mk]
    refine ⟨support_mk_subset, fun i hi => ?_⟩
    convert! mem_pi.1 hf i hi
    exact mk_of_mem hi
  · refine fun h => ⟨fun i _ => f i, mem_pi.2 h.2, ?_⟩
    ext i
    dsimp
    exact ite_eq_left_iff.2 fun hi => (notMem_support_iff.1 fun H => hi <| h.1 H).symm

Goal state after:
Module: Mathlib.Data.FP.Basic

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

Tactic:
by
      rw [← Int.ofNat_le] at this
      rw [← sub_nonneg] at *
      simp only [emin, emax] at *
      lia

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

Goal state before:
pp: case pos
R : Type
inst✝ : CommRing R
X Y : LightCondMod R
p : X ⟶ Y
hp : Epi p
S : LightProfinite
f : (free R).obj (S ⊗ ℕ∪{∞}).toCondensed ⟶ Y
T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
g : (free R).obj T.toCondensed ⟶ X
hπ : Epi π
comm : (lightProfiniteToLightCondSet ⋙ free R).map π ≫ f = g ≫ p
S' T' : LightProfinite
y' : S' ⟶ S
π' : T' ⟶ S' ⊗ ℕ∪{∞}
g' : T' ⟶ T
hπ'✝ : Epi π'
hy' : Epi y'
comp : π' ≫ y' ▷ ℕ∪{∞} = g' ≫ π
epi : Epi (cover π')
split : SplitEpi (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π' ≫ fst S' ℕ∪{∞})
hS' : Nonempty ↑S'.toTop
this✝¹ : Mono (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}))
this✝ : Nonempty ↑(LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞})).toTop
r_inf : T' ⟶ LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞})
hr : LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ r_inf = 𝟙 (LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞}))
hπ'' : RegularEpi (lightProfiniteToLightCondSet.map π') := regularEpiOfEpi (lightProfiniteToLightCondSet.map π')
this : EffectiveEpi π'
hπ' : RegularEpi (lightProfiniteToLightCondSet.map π') :=
  regularEpiOfPreserves π' lightProfiniteToLightCondSet (pullback.cone π' π') (pullback.isLimit π' π')
hc : Limits.IsColimit ((free R).mapCocone (Limits.Cofork.ofπ (lightProfiniteToLightCondSet.map π') ⋯))
⊢ (lightProfiniteToLightCondSet ⋙ free R).map (π' ≫ y' ▷ ℕ∪{∞}) ≫ f =
    (((free R).mapCocone (Limits.Cofork.ofπ (lightProfiniteToLightCondSet.map π') ⋯)).ι.app
          Limits.WalkingParallelPair.one ≫
        hc.desc (cocone R π' ((lightProfiniteToLightCondSet ⋙ free R).map g' ≫ g) r_inf split.section_ hr)) ≫
      p

Tactic:
hc.fac

Goal state after:
case pos
R : Type
inst✝ : CommRing R
X Y : LightCondMod R
p : X ⟶ Y
hp : Epi p
S : LightProfinite
f : (free R).obj (S ⊗ ℕ∪{∞}).toCondensed ⟶ Y
T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
g : (free R).obj T.toCondensed ⟶ X
hπ : Epi π
comm : (lightProfiniteToLightCondSet ⋙ free R).map π ≫ f = g ≫ p
S' T' : LightProfinite
y' : S' ⟶ S
π' : T' ⟶ S' ⊗ ℕ∪{∞}
g' : T' ⟶ T
hπ'✝ : Epi π'
hy' : Epi y'
comp : π' ≫ y' ▷ ℕ∪{∞} = g' ≫ π
epi : Epi (cover π')
split : SplitEpi (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π' ≫ fst S' ℕ∪{∞})
hS' : Nonempty ↑S'.toTop
this✝¹ : Mono (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}))
this✝ : Nonempty ↑(LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞})).toTop
r_inf : T' ⟶ LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞})
hr : LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ r_inf = 𝟙 (LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞}))
hπ'' : RegularEpi (lightProfiniteToLightCondSet.map π') := regularEpiOfEpi (lightProfiniteToLightCondSet.map π')
this : EffectiveEpi π'
hπ' : RegularEpi (lightProfiniteToLightCondSet.map π') :=
  regularEpiOfPreserves π' lightProfiniteToLightCondSet (pullback.cone π' π') (pullback.isLimit π' π')
hc : Limits.IsColimit ((free R).mapCocone (Limits.Cofork.ofπ (lightProfiniteToLightCondSet.map π') ⋯))
⊢ (lightProfiniteToLightCondSet ⋙ free R).map (π' ≫ y' ▷ ℕ∪{∞}) ≫ f =
    (cocone R π' ((lightProfiniteToLightCondSet ⋙ free R).map g' ≫ g) r_inf split.section_ hr).ι.app
        Limits.WalkingParallelPair.one ≫
      p
Module: Mathlib.Data.List.AList

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a
s : AList β
⊢ a' ∈ replace a b s ↔ a' ∈ s

Tactic:
mem_keys,

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a
s : AList β
⊢ a' ∈ (replace a b s).keys ↔ a' ∈ s
Module: Mathlib.Data.List.AList

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
s : AList β
⊢ a' ∈ erase a s ↔ a' ≠ a ∧ a' ∈ s

Tactic:
mem_keys,

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
s : AList β
⊢ a' ∈ (erase a s).keys ↔ a' ≠ a ∧ a' ∈ s