mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : ExtremallyDisconnected X
inst✝ : T2Space X
x : X
a✝¹ : x ∈ univ
y : X
a✝ : y ∈ univ
hxy : x ≠ y
U V : Set X
hUV : IsOpen U ∧ IsOpen V ∧ x ∈ U ∧ y ∈ V ∧ Disjoint U V
⊢ y ∉ closure U

Tactic:
mem_closure_iff

Goal state after:
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : ExtremallyDisconnected X
inst✝ : T2Space X
x : X
a✝¹ : x ∈ univ
y : X
a✝ : y ∈ univ
hxy : x ≠ y
U V : Set X
hUV : IsOpen U ∧ IsOpen V ∧ x ∈ U ∧ y ∈ V ∧ Disjoint U V
⊢ ¬∀ (o : Set X), IsOpen o → y ∈ o → (o ∩ U).Nonempty
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
Y Z : Type u
_tsY : TopologicalSpace Y
_tsZ : TopologicalSpace Z
_csY : CompactSpace Y
_t2Y : T2Space Y
_csZ✝ : CompactSpace Z
_csZ : T2Space Z
f : StoneCech X → Z
⊢ ∀ {g : Y → Z}, Continuous f → Continuous g → Surjective g → ∃ h, Continuous h ∧ g ∘ h = f

Tactic:
g

Goal state after:
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
Y Z : Type u
_tsY : TopologicalSpace Y
_tsZ : TopologicalSpace Z
_csY : CompactSpace Y
_t2Y : T2Space Y
_csZ✝ : CompactSpace Z
_csZ : T2Space Z
f : StoneCech X → Z
g : Y → Z
⊢ Continuous f → Continuous g → Surjective g → ∃ h, Continuous h ∧ g ∘ h = f
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: case pos.refine_2
A D : Type u
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace D
inst✝¹ : T1Space A
inst✝ : CompactSpace D
X : D → A
X_cont : Continuous X
X_surj : Surjective X
S : Set (Set D) := {E | IsClosed E ∧ X '' E = univ}
C : Set (Set D)
C_sub : C ⊆ S
C_chain : IsChain (fun x1 x2 ↦ x1 ⊆ x2) C
hC : Nonempty ↑C
a : A
c : ↑C
⊢ (↑c ∩ X ⁻¹' {a}).Nonempty

Tactic:
rw [← image_inter_nonempty_iff, (C_sub c.mem).right, univ_inter]

Goal state after:
case pos.refine_2
A D : Type u
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace D
inst✝¹ : T1Space A
inst✝ : CompactSpace D
X : D → A
X_cont : Continuous X
X_surj : Surjective X
S : Set (Set D) := {E | IsClosed E ∧ X '' E = univ}
C : Set (Set D)
C_sub : C ⊆ S
C_chain : IsChain (fun x1 x2 ↦ x1 ⊆ x2) C
hC : Nonempty ↑C
a : A
c : ↑C
⊢ {a}.Nonempty
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:
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.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case cons
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
a : Γ'
L₁ : List Γ'
IH :
  ∀ {s : Option Γ'} {S : K' → List Γ'},
    splitAtPred p (S k) = (L₁, o, L₂) →
      Reaches₁ (TM2.step tr) { l := some (Λ'.clear p k q), var := s, stk := S }
        { l := some q, var := o, stk := update S k L₂ }
s : Option Γ'
S : K' → List Γ'
e : splitAtPred p (S k) = (a :: L₁, o, L₂)
⊢ TransGen
    (fun a b ↦
      (match a with
        | { l := none, var := var, stk := stk } => none
        | { l := some l, var := v, stk := S } => some (TM2.stepAux (tr l) v S)) =
        some b)
    (bif
        match (S k).head?, true, p with
        | some x, x_1, f => f x
        | none, y, x => y then
      { l := some q, var := (S k).head?, stk := update S k (S k).tail }
    else { l := some (Λ'.clear p k q), var := (S k).head?, stk := update S k (S k).tail })
    { l := some q, var := o, stk := update S k L₂ }

Tactic:
rcases e₁ : S k with - | ⟨a', Sk⟩

Goal state after:
case cons.nil
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
a : Γ'
L₁ : List Γ'
IH :
  ∀ {s : Option Γ'} {S : K' → List Γ'},
    splitAtPred p (S k) = (L₁, o, L₂) →
      Reaches₁ (TM2.step tr) { l := some (Λ'.clear p k q), var := s, stk := S }
        { l := some q, var := o, stk := update S k L₂ }
s : Option Γ'
S : K' → List Γ'
e : splitAtPred p (S k) = (a :: L₁, o, L₂)
e₁ : S k = []
⊢ TransGen
    (fun a b ↦
      (match a with
        | { l := none, var := var, stk := stk } => none
        | { l := some l, var := v, stk := S } => some (TM2.stepAux (tr l) v S)) =
        some b)
    (bif
        match [].head?, true, p with
        | some x, x_1, f => f x
        | none, y, x => y then
      { l := some q, var := [].head?, stk := update S k [].tail }
    else { l := some (Λ'.clear p k q), var := [].head?, stk := update S k [].tail })
    { l := some q, var := o, stk := update S k L₂ }

case cons.cons
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
a : Γ'
L₁ : List Γ'
IH :
  ∀ {s : Option Γ'} {S : K' → List Γ'},
    splitAtPred p (S k) = (L₁, o, L₂) →
      Reaches₁ (TM2.step tr) { l := some (Λ'.clear p k q), var := s, stk := S }
        { l := some q, var := o, stk := update S k L₂ }
s : Option Γ'
S : K' → List Γ'
e : splitAtPred p (S k) = (a :: L₁, o, L₂)
a' : Γ'
Sk : List Γ'
e₁ : S k = a' :: Sk
⊢ TransGen
    (fun a b ↦
      (match a with
        | { l := none, var := var, stk := stk } => none
        | { l := some l, var := v, stk := S } => some (TM2.stepAux (tr l) v S)) =
        some b)
    (bif
        match (a' :: Sk).head?, true, p with
        | some x, x_1, f => f x
        | none, y, x => y then
      { l := some q, var := (a' :: Sk).head?, stk := update S k (a' :: Sk).tail }
    else { l := some (Λ'.clear p k q), var := (a' :: Sk).head?, stk := update S k (a' :: Sk).tail })
    { l := some q, var := o, stk := update S k L₂ }
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},
    Continuous[_, inst✝⁴] f →
      Continuous[inst✝⁵, inst✝⁴] g → Function.Surjective g → ∃ h, Continuous[_, inst✝⁵] h ∧ g ∘ h = f

Tactic:
g

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
⊢ Continuous[_, inst✝⁴] f →
    Continuous[inst✝⁵, inst✝⁴] g → Function.Surjective g → ∃ h, Continuous[_, inst✝⁵] h ∧ g ∘ h = f
Module: Mathlib.Topology.Category.TopCat.Limits.Cofiltered

Goal state before:
pp: case e'_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
⊢ C.pt.str = ⨅ i, induced (fun x ↦ (ConcreteCategory.hom (C.π.app i)) x) (F.obj i).str

pp: case e'_3
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
⊢ {U | ∃ j, ∃ V ∈ T j, U = ⇑(ConcreteCategory.hom (C.π.app j)) ⁻¹' V} =
    {S | ∃ U F_1, (∀ i ∈ F_1, U i ∈ T i) ∧ S = ⋂ i ∈ F_1, (fun x ↦ (ConcreteCategory.hom (C.π.app i)) x) ⁻¹' U i}

Tactic:
· exact induced_of_isLimit C hC

Goal state after:
case e'_3
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
⊢ {U | ∃ j, ∃ V ∈ T j, U = ⇑(ConcreteCategory.hom (C.π.app j)) ⁻¹' V} =
    {S | ∃ U F_1, (∀ i ∈ F_1, U i ∈ T i) ∧ S = ⋂ i ∈ F_1, (fun x ↦ (ConcreteCategory.hom (C.π.app i)) x) ⁻¹' U i}
Module: Mathlib.Topology.Category.Profinite.CofilteredLimit

Goal state before:
pp: case inl
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)
⊢ ∃ j g, f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g

Tactic:
suffices ∃ j, IsEmpty (F.obj j) by
      refine this.imp fun j hj => ?_
      refine ⟨⟨hj.elim, fun A => ?_⟩, ?_⟩
      · convert! isOpen_empty
        ext x
        exact hj.elim x
      · ext x
        exact hj.elim' (C.π.app j x)

Goal state after:
case inl
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)
⊢ ∃ j, IsEmpty ↑(F.obj j).toTop
Module: Mathlib.Condensed.Discrete.LocallyConstant

Goal state before:
pp: P : TopCat → Prop
inst✝³ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
S✝ : CompHausLike P
Y✝ : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝² : HasProp P PUnit.{u + 1}
f : LocallyConstant (↑S✝.toTop) (Y✝.obj (op (of P PUnit.{u + 1})))
T✝ : CompHausLike P
g : T✝ ⟶ S✝
inst✝¹ : HasExplicitFiniteCoproducts P
Y : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝ : PreservesFiniteProducts Y
S T : (CompHausLike P)ᵒᵖ
⊢ ∀ (f : S ⟶ T),
    ((functorToPresheaves.obj (Y.obj (op (of P PUnit.{u + 1})))).map f ≫
        match T with
        | op S => counitAppApp S Y) =
      (match S with
        | op S => counitAppApp S Y) ≫
        Y.map f

Tactic:
g

Goal state after:
P : TopCat → Prop
inst✝³ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
S✝ : CompHausLike P
Y✝ : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝² : HasProp P PUnit.{u + 1}
f : LocallyConstant (↑S✝.toTop) (Y✝.obj (op (of P PUnit.{u + 1})))
T✝ : CompHausLike P
g✝ : T✝ ⟶ S✝
inst✝¹ : HasExplicitFiniteCoproducts P
Y : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝ : PreservesFiniteProducts Y
S T : (CompHausLike P)ᵒᵖ
g : S ⟶ T
⊢ ((functorToPresheaves.obj (Y.obj (op (of P PUnit.{u + 1})))).map g ≫
      match T with
      | op S => counitAppApp S Y) =
    (match S with
      | op S => counitAppApp S Y) ≫
      Y.map g
Module: Mathlib.Condensed.EffectiveEpi

Goal state before:
pp: X✝ Y✝ : CompHaus
f : X✝ ⟶ Y✝
hf : Epi f
S : CompHaus
⊢ ∀ (y : (compHausToCondensed.obj Y✝).obj.obj (Opposite.op S)),
    ∃ S' φ,
      ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom φ)),
        ∃ x,
          (ConcreteCategory.hom ((compHausToCondensed.map f).hom.app (Opposite.op S'))) x =
            (ConcreteCategory.hom ((compHausToCondensed.obj Y✝).obj.map (Opposite.op φ))) y

Tactic:
g

Goal state after:
X✝ Y✝ : CompHaus
f : X✝ ⟶ Y✝
hf : Epi f
S : CompHaus
g : (compHausToCondensed.obj Y✝).obj.obj (Opposite.op S)
⊢ ∃ S' φ,
    ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom φ)),
      ∃ x,
        (ConcreteCategory.hom ((compHausToCondensed.map f).hom.app (Opposite.op S'))) x =
          (ConcreteCategory.hom ((compHausToCondensed.obj Y✝).obj.map (Opposite.op φ))) g
Module: Mathlib.Condensed.Light.EffectiveEpi

Goal state before:
pp: X✝ Y✝ : LightProfinite
f : X✝ ⟶ Y✝
hf : Epi f
S : LightProfinite
⊢ ∀ (y : (lightProfiniteToLightCondSet.obj Y✝).obj.obj (Opposite.op S)),
    ∃ S' φ,
      ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom φ)),
        ∃ x,
          (ConcreteCategory.hom ((lightProfiniteToLightCondSet.map f).hom.app (Opposite.op S'))) x =
            (ConcreteCategory.hom ((lightProfiniteToLightCondSet.obj Y✝).obj.map (Opposite.op φ))) y

Tactic:
g

Goal state after:
X✝ Y✝ : LightProfinite
f : X✝ ⟶ Y✝
hf : Epi f
S : LightProfinite
g : (lightProfiniteToLightCondSet.obj Y✝).obj.obj (Opposite.op S)
⊢ ∃ S' φ,
    ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom φ)),
      ∃ x,
        (ConcreteCategory.hom ((lightProfiniteToLightCondSet.map f).hom.app (Opposite.op S'))) x =
          (ConcreteCategory.hom ((lightProfiniteToLightCondSet.obj Y✝).obj.map (Opposite.op φ))) g
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)
⊢ ∀ ⦃i : S⦄, i ∈ univ → ∀ ⦃j : S⦄, j ∈ univ → (Z i ∩ Z j).Nonempty → i = j

Tactic:
simp only [image_inter_nonempty_iff, Z]

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)
⊢ ∀ ⦃i : S⦄, i ∈ univ → ∀ ⦃j : S⦄, j ∈ univ → (g ⁻¹' {i} ∩ f ⁻¹' f '' g ⁻¹' {j}).Nonempty → i = j
Module: Mathlib.Condensed.Light.InternallyProjective

Goal state before:
pp: case refine_2
R : Type u
inst✝ : CommRing R
P : LightCondMod R
h :
  ∀ {A B : LightCondMod R} (e : A ⟶ B) [Epi e] (S : LightProfinite) (g : P ⊗ (free R).obj S.toCondensed ⟶ B),
    ∃ S' π,
      ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
        ∃ g', P ◁ (lightProfiniteToLightCondSet ⋙ free R).map π ≫ g = g' ≫ e
A B : LightCondMod R
e : A ⟶ B
he : Epi e
S : LightProfinite
⊢ ∀ (y : ↑((P ⟹ B).obj.obj (Opposite.op S))),
    ∃ S' φ,
      ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom φ)),
        ∃ x,
          (ConcreteCategory.hom (((ihom P).map e).hom.app (Opposite.op S'))) x =
            (ConcreteCategory.hom ((P ⟹ B).obj.map (Opposite.op φ))) y

Tactic:
g

Goal state after:
case refine_2
R : Type u
inst✝ : CommRing R
P : LightCondMod R
h :
  ∀ {A B : LightCondMod R} (e : A ⟶ B) [Epi e] (S : LightProfinite) (g : P ⊗ (free R).obj S.toCondensed ⟶ B),
    ∃ S' π,
      ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
        ∃ g', P ◁ (lightProfiniteToLightCondSet ⋙ free R).map π ≫ g = g' ≫ e
A B : LightCondMod R
e : A ⟶ B
he : Epi e
S : LightProfinite
g : ↑((P ⟹ B).obj.obj (Opposite.op S))
⊢ ∃ S' φ,
    ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom φ)),
      ∃ x,
        (ConcreteCategory.hom (((ihom P).map e).hom.app (Opposite.op S'))) x =
          (ConcreteCategory.hom ((P ⟹ B).obj.map (Opposite.op φ))) g
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n✝ n : ℕ
β : (v : TypeVec.{?u.30} (n + 1)) → (v' : TypeVec.{?u.32} (n + 1)) → v ⟹ v' → Sort u_1
F :
  (t : Type ?u.30) →
    (t' : Type ?u.32) →
      (f : t → t') →
        (v : TypeVec.{?u.30} n) → (v' : TypeVec.{?u.32} n) → (fs : v ⟹ v') → β (v ::: t) (v' ::: t') (fs ::: f)
v : TypeVec.{?u.30} (n + 1)
v' : TypeVec.{?u.32} (n + 1)
fs : v.drop ::: v.last ⟹ v'.drop ::: v'.last
⊢ β (v.drop ::: v.last) (v'.drop ::: v'.last) fs

Tactic:
← split_dropFun_lastFun fs

Goal state after:
n✝ n : ℕ
β : (v : TypeVec.{?u.30} (n + 1)) → (v' : TypeVec.{?u.32} (n + 1)) → v ⟹ v' → Sort u_1
F :
  (t : Type ?u.30) →
    (t' : Type ?u.32) →
      (f : t → t') →
        (v : TypeVec.{?u.30} n) → (v' : TypeVec.{?u.32} n) → (fs : v ⟹ v') → β (v ::: t) (v' ::: t') (fs ::: f)
v : TypeVec.{?u.30} (n + 1)
v' : TypeVec.{?u.32} (n + 1)
fs : v.drop ::: v.last ⟹ v'.drop ::: v'.last
⊢ β (v.drop ::: v.last) (v'.drop ::: v'.last) (splitFun (dropFun fs) (lastFun fs))
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n✝ n : ℕ
t : Type u_1
t' : Type u_2
v : TypeVec.{u_1} n
v' : TypeVec.{u_2} n
β : v ::: t ⟹ v' ::: t' → Sort u_3
F : (f : t → t') → (fs : v ⟹ v') → β (fs ::: f)
fs : v ::: t ⟹ v' ::: t'
⊢ β fs

Tactic:
← split_dropFun_lastFun fs

Goal state after:
n✝ n : ℕ
t : Type u_1
t' : Type u_2
v : TypeVec.{u_1} n
v' : TypeVec.{u_2} n
β : v ::: t ⟹ v' ::: t' → Sort u_3
F : (f : t → t') → (fs : v ⟹ v') → β (fs ::: f)
fs : v ::: t ⟹ v' ::: t'
⊢ β (splitFun (dropFun fs) (lastFun fs))
Module: Mathlib.Control.Monad.Cont

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

Tactic:
simp only [callCC, StateT.callCC, StateT.run_bind, callCC_bind_right]

Goal state after:
m : Type u → Type v
σ : Type u
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ ω✝ γ✝ : Type u
cmd✝ : StateT σ m α✝
next✝ : Label ω✝ (StateT σ m) γ✝ → α✝ → StateT σ m ω✝
⊢ (StateT.mk fun r ↦ do
      let x ← cmd✝.run r
      callCC fun f ↦ (next✝ (StateT.mkLabel f) x.fst).run x.snd) =
    do
    let x ← cmd✝
    StateT.mk fun r ↦ callCC fun f' ↦ (next✝ (StateT.mkLabel f') x).run r
Module: Mathlib.Data.ENat.BigOperators

Goal state before:
pp: α : Type u_1
s : Finset α
f : α → ℕ∞
hf : ∀ a ∈ s, f a ≠ ⊤
⊢ (∑ a ∈ s, f a).toNat = ∑ a ∈ s, (f a).toNat

Tactic:
rw [← natCast_inj, natCast_toNat (sum_ne_top.2 hf), Nat.cast_sum]

Goal state after:
α : Type u_1
s : Finset α
f : α → ℕ∞
hf : ∀ a ∈ s, f a ≠ ⊤
⊢ ∑ a ∈ s, f a = ∑ x ∈ s, ↑(f x).toNat
Module: Mathlib.Data.Finite.Perm

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
h : ∀ (a b : Perm α), a * b = b * a
a b c : α
left✝² : a ∈ _root_.Set.univ
left✝¹ : b ∈ _root_.Set.univ
left✝ : c ∈ _root_.Set.univ
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
⊢ b = c

Tactic:
simp_rw [Perm.ext_iff] at h

Goal state after:
α : Type u_1
inst✝ : Finite α
a b c : α
left✝² : a ∈ _root_.Set.univ
left✝¹ : b ∈ _root_.Set.univ
left✝ : c ∈ _root_.Set.univ
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
h : ∀ (a b : Perm α) (x : α), (a * b) x = (b * a) x
⊢ b = c
Module: Mathlib.Data.Finsupp.AList

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
l : AList fun _x ↦ M
⊢ Finset α

Tactic:
haveI := Classical.decEq α

Goal state after:
α : Type u_1
M : Type u_2
inst✝ : Zero M
l : AList fun _x ↦ M
this : DecidableEq α
⊢ Finset α
Module: Mathlib.Data.Finsupp.Sigma

Goal state before:
pp: κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst✝ : Zero M
k : κ
f : ι k →₀ M
i : ι k
⊢ f.embSigma ⟨k, i⟩ = f i

Tactic:
by
  rw [embSigma]
  exact embDomain_apply_self (Embedding.sigmaMk k) f i

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

Goal state before:
pp: κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst✝ : Zero M
k : κ
f : ι k →₀ M
⊢ ∀ ⦃a₂ : ι k →₀ M⦄, f.embSigma = a₂.embSigma → f = a₂

Tactic:
g

Goal state after:
κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst✝ : Zero M
k : κ
f g : ι k →₀ M
⊢ f.embSigma = g.embSigma → f = g
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
ds : List ℕ
inst✝¹ : Mul α
inst✝ : AddMonoid α
n : ℕ
x y : Holor α ds
hx : CPRankMax 0 x
hy : CPRankMax n y
⊢ CPRankMax (0 + n) (0 + y)

Tactic:
| =>

Goal state after:
α : Type
ds : List ℕ
inst✝¹ : Mul α
inst✝ : AddMonoid α
n : ℕ
x y : Holor α ds
hx : CPRankMax 0 x
hy : CPRankMax n y
⊢ CPRankMax (0 + n) (0 + y)
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: a b r v : ℤ
⊢ {x ∈ Ioc a b | x ≡ v [ZMOD r]} = map { toFun := fun x ↦ x + v, inj' := ⋯ } ({x ∈ Ioc (a - v) (b - v) | r ∣ x})

Tactic:
by
  ext x
  simp_rw [mem_map, mem_filter, mem_Ioc, Function.Embedding.coeFn_mk, ← eq_sub_iff_add_eq,
    exists_eq_right, modEq_comm, modEq_iff_dvd, sub_lt_sub_iff_right, sub_le_sub_iff_right]

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

Goal state before:
pp: case cons
α : Type u_1
p : α → Bool
l : List α
x : α
xs : List α
IH : dropWhile p xs = [] ↔ ∀ (x : α), x ∈ xs → p x = true
⊢ dropWhile p (x :: xs) = [] ↔ ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1 = true

Tactic:
by_cases hp : p x <;> simp [hp, IH]

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

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

Tactic:
by_cases hp : p x <;> simp [hp, IH]

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

Goal state before:
pp: case nil
α : Type u_1
p : α → Bool
l : List α
⊢ takeWhile p [] = [] ↔ ∀ (hl : 0 < [].length), ¬p ([].get ⟨0, hl⟩) = true

Tactic:
simp only [takeWhile_nil, Bool.not_eq_true, true_iff]
    intro h
    simp at h

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

Goal state before:
pp: case cons.succ.succ
α : Type u_1
x hd : α
tl : List α
IH :
  ¬x ∈ tl →
    ∀ ⦃n : ℕ⦄,
      n ∈ {n | n ≤ tl.length} →
        ∀ ⦃m : ℕ⦄, m ∈ {n | n ≤ tl.length} → (fun k ↦ tl.insertIdx k x) n = (fun k ↦ tl.insertIdx k x) m → n = m
hx : ¬x = hd ∧ ¬x ∈ tl
n✝¹ : ℕ
hn : n✝¹ + 1 ≤ tl.length + 1
n✝ : ℕ
hm : n✝ + 1 ≤ tl.length + 1
h : (fun k ↦ (hd :: tl).insertIdx k x) (n✝¹ + 1) = (fun k ↦ (hd :: tl).insertIdx k x) (n✝ + 1)
⊢ n✝¹ + 1 = n✝ + 1

Tactic:
· simp only [insertIdx_succ_cons, cons.injEq, true_and] at h
      rw [Nat.succ_inj]
      refine IH hx.right ?_ ?_ h
      · simpa [Nat.succ_le_succ_iff] using hn
      · simpa [Nat.succ_le_succ_iff] using hm

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

Goal state before:
pp: case cons
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → α → α
g : γ → α → α
hfg : Set.range f ⊆ Set.range g
a : α
b : β
l : List β
c : γ
hgf : g c = f b
m : List γ
hgf' : foldr g a m = foldr f a l
⊢ f b (foldr f a l) ∈ Set.range (foldr g a)

Tactic:
← hgf,

Goal state after:
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → α → α
g : γ → α → α
hfg : Set.range f ⊆ Set.range g
a : α
b : β
l : List β
c : γ
hgf : g c = f b
m : List γ
hgf' : foldr g a m = foldr f a l
⊢ g c (foldr f a l) ∈ Set.range (foldr g a)
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: case nil
α : Type u_1
r : α → α → Bool
a : α
g : List α
gs : List (List α)
⊢ splitBy.loop r [] a g gs = gs.reverse ++ splitBy.loop r [] a g []

Tactic:
simp [splitBy.loop]

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

Goal state before:
pp: α : Type u_1
l : List α
sz : List ℕ
i : ℕ
hi : i < sz.length
h : (take (i + 1) sz).sum ≤ l.length
⊢ (sz.splitLengths l)[i].length = sz[i]

Tactic:
rw [List.getElem_take' (hj := i.lt_add_one)]
  simp only [take_splitLength]
  conv_rhs =>
    rw [List.getElem_take' (hj := i.lt_add_one)]
    simp +singlePass only [← map_splitLengths_length l _ h]
    rw [getElem_map]

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

Goal state before:
pp: case nil
α : Type u_1
r : α → α → Bool
a : α
g : List α
⊢ (splitBy.loop r [] a g []).flatten = g.reverse ++ [a]

Tactic:
simp [splitBy.loop]

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

Goal state before:
pp: α : Type u_1
r : α → α → Bool
l : List α
a : α
g : List α
⊢ (splitBy.loop r l a g []).flatten = g.reverse ++ a :: l

Tactic:
induction l generalizing a g with
  | nil => simp [splitBy.loop]
  | cons b l IH =>
    rw [splitBy.loop, splitByLoop_eq_append [_]]
    split <;> simp [IH]

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

Goal state before:
pp: case nil
α : Type u_1
r : α → α → Bool
a : α
g : List α
⊢ ¬[] ∈ splitBy.loop r [] a g []

Tactic:
simp [splitBy.loop]

Goal state after: