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

Goal state before:
pp: case zero
α : Type u_1
inst✝ : DecidableEq α
x : List α
⊢ false = true ↔ x ∈ matches' 0

Tactic:
tauto

Goal state after:
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case comp
α : Type u_1
inst✝ : DecidableEq α
P Q : RegularExpression α
ih₁ : ∀ (x : List α), P.rmatch x = true ↔ x ∈ P.matches'
ih₂ : ∀ (x : List α), Q.rmatch x = true ↔ x ∈ Q.matches'
x : List α
⊢ (∃ t u, x = t ++ u ∧ t ∈ P.matches' ∧ u ∈ Q.matches') ↔ ∃ a ∈ P.matches', ∃ b ∈ Q.matches', a ++ b = x

Tactic:
tauto

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

Goal state before:
pp: case neg
n✝¹ : ℕ
f✝ : List.Vector ℕ n✝¹ →. ℕ
n✝ : ℕ
f : List.Vector ℕ (n✝ + 1) → ℕ
a✝ : Nat.Partrec' ↑f
cf : Code
v : List.Vector ℕ n✝
hf : ∀ (a : ℕ), cf.eval (a :: ↑v) = Part.some [f (a ::ᵥ v)]
v' v₀ : List ℕ
n : ℕ
h2 :
  v' ∈
    PFun.fix
      (fun v ↦
        (cf.eval v).bind fun y ↦
          Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
      (n :: ↑v)
IH :
  ∀ (a'' : List ℕ),
    (Sum.inr a'' ∈
        (cf.eval (n :: ↑v)).bind fun y ↦
          Part.some
            (if y.headI = 0 then Sum.inl ((n :: ↑v).headI.succ :: (n :: ↑v).tail)
            else Sum.inr ((n :: ↑v).headI.succ :: (n :: ↑v).tail))) →
      ∀ (n : ℕ),
        a'' = n :: ↑v →
          (∀ m < n, ¬f (m ::ᵥ v) = 0) →
            ∃ a, (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ [a] = [v'.headI.pred]
hm : ∀ m < n, ¬f (m ::ᵥ v) = 0
h : ¬[f (n ::ᵥ v)].headI = 0
this :
  Sum.inl v' ∈ Part.some (Sum.inr ((n :: ↑v).headI.succ :: (n :: ↑v).tail)) ∨
    ∃ a',
      Sum.inr a' ∈ Part.some (Sum.inr ((n :: ↑v).headI.succ :: (n :: ↑v).tail)) ∧
        v' ∈
          PFun.fix
            (fun v ↦
              (cf.eval v).bind fun y ↦
                Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
            a'
⊢ ∃ a, (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ [a] = [v'.headI.pred]

Tactic:
· refine IH (n.succ::v.val) (by simp_all) _ rfl fun m h' => ?_
        obtain h | rfl := Nat.lt_succ_iff_lt_or_eq.1 h'
        exacts [hm _ h, h]

Goal state after:
Module: Mathlib.Topology.Category.CompHausLike.Limits

Goal state before:
pp: P : TopCat → Prop
α : Type w
inst✝¹ : Finite α
X : α → CompHausLike P
inst✝ : HasExplicitFiniteCoproduct X
B : CompHausLike P
π : (a : α) → X a ⟶ B
a : α
⊢ ∀ (x : (fun X ↦ ↑X.toTop) (X a)),
    (ConcreteCategory.hom (desc X π)) ((ConcreteCategory.hom (ι X a)) x) = (ConcreteCategory.hom (π a)) x

Tactic:
tauto

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

Goal state before:
pp: case h
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : T2Space X
inst✝¹ : CompactSpace X
inst✝ : TotallyDisconnectedSpace X
x : X
U : Set X
hxU : x ∈ U
U_op : IsOpen[inst✝³] U
this : U ∈ 𝓝 x
V : Set X
hVU : V ⊆ U
hxV : x ∈ V
hV : IsClopen V
⊢ (V ∈ fun U ↦ IsClosed[inst✝³] U ∧ IsOpen[inst✝³] U) ∧ x ∈ V ∧ V ⊆ U

Tactic:
tauto

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

Goal state before:
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')

Tactic:
intro _ ss' _

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✝ : σ → Λ
ss' : TM2.SupportsStmt S (TM2.Stmt.goto l✝)
x✝ : ∀ 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')
Module: Mathlib.Topology.Category.Profinite.Basic

Goal state before:
pp: case mp
X Y : Profinite
f : X ⟶ Y
y : ↑Y.toTop
hy : ∀ (a : ↑X.toTop), (ConcreteCategory.hom f) a ≠ y
hf : Epi f
C : Set ((fun X ↦ ↑X.toTop) Y) := Set.range ⇑(ConcreteCategory.hom f)
hC : IsClosed C
U : Set ((fun X ↦ ↑X.toTop) Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ 𝓝 y
V : Set ↑Y.toTop
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
Z : Profinite := of (ULift.{u, 0} (Fin 2))
⊢ False

Tactic:
let g : Y ⟶ Z := ofHom _
        ⟨(LocallyConstant.ofIsClopen hV).map ULift.up, LocallyConstant.continuous _⟩

Goal state after:
case mp
X Y : Profinite
f : X ⟶ Y
y : ↑Y.toTop
hy : ∀ (a : ↑X.toTop), (ConcreteCategory.hom f) a ≠ y
hf : Epi f
C : Set ((fun X ↦ ↑X.toTop) Y) := Set.range ⇑(ConcreteCategory.hom f)
hC : IsClosed C
U : Set ((fun X ↦ ↑X.toTop) Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ 𝓝 y
V : Set ↑Y.toTop
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
Z : Profinite := of (ULift.{u, 0} (Fin 2))
g : Y ⟶ Z :=
  ofHom (fun X ↦ TotallyDisconnectedSpace ↑X)
    { toFun := ⇑(LocallyConstant.map ULift.up (LocallyConstant.ofIsClopen hV)), continuous_toFun := ⋯ }
⊢ False
Module: Mathlib.Topology.Category.Stonean.Basic

Goal state before:
pp: case mp
X : CompHaus
⊢ Projective X → ExtremallyDisconnected ↑X.toTop

Tactic:
intro h
    change ExtremallyDisconnected X.toStonean
    infer_instance

Goal state after:
Module: Mathlib.Topology.DiscreteQuotient

Goal state before:
pp: α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S a : DiscreteQuotient X
⊢ a ≤ { toSetoid := ⊤, isOpen_setOfPred_rel := ⋯ }

Tactic:
tauto

Goal state after:
Module: Mathlib.Topology.DiscreteQuotient

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : C(X, Y)
A B : DiscreteQuotient Y
h : A ≤ B
⊢ comap f A ≤ comap f B

Tactic:
tauto

Goal state after:
Module: Mathlib.Topology.DiscreteQuotient

Goal state before:
pp: X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : C(X, Y)
A : DiscreteQuotient X
B : DiscreteQuotient Y
g : C(Y, Z)
C : DiscreteQuotient Z
⊢ LEComap g B C → LEComap f A B → LEComap (g.comp f) A C

Tactic:
tauto

Goal state after:
Module: Mathlib.Topology.DiscreteQuotient

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
A B : DiscreteQuotient X
h : A ≤ B
a : X
⊢ ofPred (A.toSetoid a) ⊆ ofPred (B.toSetoid a)

Tactic:
exact fun _ h' => h h'

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

Goal state before:
pp: F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
C : Type u_1
inst✝ : Category.{v_1, u_1} C
G : LightProfiniteᵒᵖ ⥤ C
S : LightProfinite
x✝¹ x✝ : CostructuredArrow toLightProfinite.op (Opposite.op S)
f : x✝¹ ⟶ x✝
this : toLightProfinite.op.map f.left ≫ x✝.hom = x✝¹.hom ≫ (fromPUnit (Opposite.op S)).map f.right
⊢ (CostructuredArrow.proj toLightProfinite.op (Opposite.op S) ⋙ toLightProfinite.op ⋙ G).map f ≫ G.map x✝.hom =
    G.map x✝¹.hom ≫ ((const (CostructuredArrow toLightProfinite.op (Opposite.op S))).obj (G.obj (Opposite.op S))).map f

Tactic:
simp only [op_obj, const_obj_obj, op_map, CostructuredArrow.right_eq_id, const_obj_map,
        Category.comp_id] at this

Goal state after:
F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
C : Type u_1
inst✝ : Category.{v_1, u_1} C
G : LightProfiniteᵒᵖ ⥤ C
S : LightProfinite
x✝¹ x✝ : CostructuredArrow toLightProfinite.op (Opposite.op S)
f : x✝¹ ⟶ x✝
this : (toLightProfinite.map f.left.unop).op ≫ x✝.hom = x✝¹.hom
⊢ (CostructuredArrow.proj toLightProfinite.op (Opposite.op S) ⋙ toLightProfinite.op ⋙ G).map f ≫ G.map x✝.hom =
    G.map x✝¹.hom ≫ ((const (CostructuredArrow toLightProfinite.op (Opposite.op S))).obj (G.obj (Opposite.op S))).map f
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: 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

Tactic:
rw [codeSupp, contSupp_cons₁] at H'

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) ∪
        (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₂) ⊆
      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
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)
C : Type u_1
inst✝ : Category.{v_1, u_1} C
G : Profiniteᵒᵖ ⥤ C
S : Profinite
x✝¹ x✝ : CostructuredArrow toProfinite.op (Opposite.op S)
f : x✝¹ ⟶ x✝
this : toProfinite.op.map f.left ≫ x✝.hom = x✝¹.hom ≫ (fromPUnit (Opposite.op S)).map f.right
⊢ (CostructuredArrow.proj toProfinite.op (Opposite.op S) ⋙ toProfinite.op ⋙ G).map f ≫ G.map x✝.hom =
    G.map x✝¹.hom ≫ ((const (CostructuredArrow toProfinite.op (Opposite.op S))).obj (G.obj (Opposite.op S))).map f

Tactic:
simp only [op_obj, const_obj_obj, op_map, CostructuredArrow.right_eq_id, const_obj_map,
        Category.comp_id] at this

Goal state after:
I : Type u
inst✝² : SmallCategory I
inst✝¹ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
C : Type u_1
inst✝ : Category.{v_1, u_1} C
G : Profiniteᵒᵖ ⥤ C
S : Profinite
x✝¹ x✝ : CostructuredArrow toProfinite.op (Opposite.op S)
f : x✝¹ ⟶ x✝
this : (toProfinite.map f.left.unop).op ≫ x✝.hom = x✝¹.hom
⊢ (CostructuredArrow.proj toProfinite.op (Opposite.op S) ⋙ toProfinite.op ⋙ G).map f ≫ G.map x✝.hom =
    G.map x✝¹.hom ≫ ((const (CostructuredArrow toProfinite.op (Opposite.op S))).obj (G.obj (Opposite.op S))).map f
Module: Mathlib.Condensed.Explicit

Goal state before:
pp: A : Type u_1
inst✝² : Category.{v_1, u_1} A
inst✝¹ : ∀ (X : CompHausᵒᵖ), HasLimitsOfShape (StructuredArrow X Stonean.toCompHaus.op) A
F : Stoneanᵒᵖ ⥤ A
inst✝ : PreservesFiniteProducts F
⊢ IsSheaf (coherentTopology Stonean) F

Tactic:
by
      rw [isSheaf_iff_preservesFiniteProducts_of_projective F]
      exact ⟨fun _ ↦ inferInstance⟩

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

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

Tactic:
by
  apply (ihomPoints R P B S).injective
  simp only [ihomPoints_apply, ← MonoidalClosed.uncurry_natural_right,
    ← Adjunction.homEquiv_naturality_right_symm, Equiv.apply_symm_apply]
  congr
  apply (coherentTopology LightProfinite.{u}).yonedaEquiv.injective
  simp [dsimp% GrothendieckTopology.yonedaEquiv_comp]

Goal state after:
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
⊢ Epi ((ihom P).map e)

Tactic:
rw [LightCondMod.epi_iff_locallySurjective_on_lightProfinite]

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) (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
Module: Mathlib.Condensed.Light.InternallyProjective

Goal state before:
pp: R : Type u
inst✝ : CommRing R
P : LightProfinite
⊢ InternallyProjective ((free R).obj P.toCondensed) ↔
    ∀ {A B : LightCondMod R} (e : A ⟶ B) [Epi e] (S : LightProfinite) (g : (free R).obj (P ⊗ S).toCondensed ⟶ B),
      ∃ S' π,
        ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
          ∃ g', (free R).map (lightProfiniteToLightCondSet.map (P ◁ π)) ≫ g = g' ≫ e

Tactic:
by
  rw [free_internallyProjective_iff_tensor_condition]
  refine ⟨fun h A B e he S g ↦ ?_, fun h A B e he S g ↦ ?_⟩
  · specialize h e S ((free R).map (μIso lightProfiniteToLightCondSet _ _).hom ≫ g)
    obtain ⟨S', π, hπ, g', hh⟩ := h
    refine ⟨S', π, hπ, (free R).map (μIso
        lightProfiniteToLightCondSet _ _).inv ≫ g', ?_⟩
    rw [assoc, ← hh]
    simp [-map_comp, ← map_comp_assoc]
  · specialize h e S ((free R).map (μIso lightProfiniteToLightCondSet _ _).inv ≫ g)
    obtain ⟨S', π, hπ, g', hh⟩ := h
    refine ⟨S', π, hπ, (free R).map
      (μIso lightProfiniteToLightCondSet _ _).hom ≫ g', ?_⟩
    rw [assoc, ← hh]
    simp [-map_comp, ← map_comp_assoc, ← μ_natural_right_assoc]

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
P : LightProfinite
⊢ InternallyProjective ((free R).obj P.toCondensed) ↔
    ∀ {A B : LightCondMod R} (e : A ⟶ B) [Epi e] (S : LightProfinite) (g : (free R).obj (S ⊗ P).toCondensed ⟶ B),
      ∃ S' π,
        ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
          ∃ g', (free R).map (lightProfiniteToLightCondSet.map (π ▷ P)) ≫ g = g' ≫ e

Tactic:
rw [free_internallyProjective_iff_tensor_condition']
  refine ⟨fun h A B e he S g ↦ ?_, fun h A B e he S g ↦ ?_⟩
  · specialize h e S ((free R).map (μIso lightProfiniteToLightCondSet _ _).hom ≫ g)
    obtain ⟨S', π, hπ, g', hh⟩ := h
    refine ⟨S', π, hπ, (free R).map (μIso
        lightProfiniteToLightCondSet _ _).inv ≫ g', ?_⟩
    rw [assoc, ← hh]
    simp [-map_comp, ← map_comp_assoc]
  · specialize h e S ((free R).map (μIso lightProfiniteToLightCondSet _ _).inv ≫ g)
    obtain ⟨S', π, hπ, g', hh⟩ := h
    refine ⟨S', π, hπ, (free R).map
      (μIso lightProfiniteToLightCondSet _ _).hom ≫ g', ?_⟩
    rw [assoc, ← hh]
    simp [-map_comp, ← map_comp_assoc, ← μ_natural_left_assoc]

Goal state after:
Module: Mathlib.Control.Functor.Multivariate

Goal state before:
pp: case h₁
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
rr : β → β → Prop
x y : F (α ::: β)
⊢ ∀ (u : F fun i ↦ { p_1 // ofRepeat (α.RelLast' rr i (prod.mk i p_1.1 p_1.2)) }),
    (fun i t ↦ (↑t).1) <$$> u = x ∧ (fun i t ↦ (↑t).2) <$$> u = y ↔
      (fun i t ↦ (↑t).1) <$$> f' rr n α <$$> u = x ∧ (fun i t ↦ (↑t).2) <$$> f' rr n α <$$> u = y

Tactic:
intros
    simp +unfoldPartialApp only [map_map, TypeVec.comp]
    apply iff_of_eq -- Switch to `eq` so we can use `ext`
    congr <;> ext i ⟨x, _⟩ <;> cases i <;> rfl

Goal state after:
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: r : Type u
m : Type u → Type v
α : Type w
x y : ContT r m α
h : ∀ (f : α → m r), x.run f = y.run f
⊢ x = y

Tactic:
unfold ContT; ext; apply h

Goal state after:
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: m : Type u → Type v
inst✝² : Monad m
ε : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
⊢ ∀ {α : Type u} (β : Type u) (x : α) (dead : Label α (ExceptT ε m) β → β → ExceptT ε m α),
    (callCC fun f ↦ goto f x >>= dead f) = pure x

Tactic:
by
    intros
    simp only [callCC, ExceptT.callCC, ExceptT.goto_mkLabel, map_eq_bind_pure_comp, Function.comp,
      ExceptT.run_bind, ExceptT.run_mk, bind_assoc, pure_bind, @callCC_bind_left m _]
    ext; rfl

Goal state after:
Module: Mathlib.Data.Analysis.Topology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
F : Realizer α
s : Set α
a : α
this : (a : Prop) → Decidable a
⊢ (a ∉ s → ∃ b, a ∈ F.F.f b ∧ ∀ z ∈ F.F.f b, z ∉ s) ↔ (∀ (b : F.σ), a ∈ F.F.f b → ∃ z, z ∈ F.F.f b ∩ s) → a ∈ s

Tactic:
rw [not_imp_comm]

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
F : Realizer α
s : Set α
a : α
this : (a : Prop) → Decidable a
⊢ (¬∃ b, a ∈ F.F.f b ∧ ∀ z ∈ F.F.f b, z ∉ s) → a ∈ s ↔ (∀ (b : F.σ), a ∈ F.F.f b → ∃ z, z ∈ F.F.f b ∩ s) → a ∈ s
Module: Mathlib.Data.FP.Basic

Goal state before:
pp: C : FloatCfg
n d : ℕ+
e₁ : ℤ := ↑(↑n).size - ↑(↑d).size - ↑prec
d₁ n₁ : ℕ
⊢ Float × Bool

Tactic:
let e₂ := if n₁ < d₁ then e₁ - 1 else e₁

Goal state after:
C : FloatCfg
n d : ℕ+
e₁ : ℤ := ↑(↑n).size - ↑(↑d).size - ↑prec
d₁ n₁ : ℕ
e₂ : ℤ := if n₁ < d₁ then e₁ - 1 else e₁
⊢ Float × Bool
Module: Mathlib.Data.Fin.FlagRange

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : BoundedOrder α
n : ℕ
f : Fin (n + 1) → α
h0 : f 0 = ⊥
hlast : f (Fin.last n) = ⊤
hcovBy : ∀ (k : Fin n), f k.castSucc ⩿ f k.succ
⊢ IsMaxChain (fun x1 x2 ↦ x1 ≤ x2) (range f)

Tactic:
by
  have hmono : Monotone f := Fin.monotone_iff_le_succ.2 fun k ↦ (hcovBy k).1
  refine ⟨hmono.isChain_range, fun t htc hbt ↦ hbt.antisymm fun x hx ↦ ?_⟩
  rw [mem_range]; by_contra! h
  suffices ∀ k, f k < x by simpa [hlast] using this (.last _)
  intro k
  induction k using Fin.induction with
  | zero => simpa [h0, bot_lt_iff_ne_bot] using (h 0).symm
  | succ k ihk =>
    rw [range_subset_iff] at hbt
    exact (htc.lt_of_le (hbt k.succ) hx (h _)).resolve_right ((hcovBy k).2 ihk)

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

Goal state before:
pp: case neg
α : Type u_1
x✝ : ↑{(a, b) | a ≠ b}
a b : α
h : (a, b) ∈ {(a, b) | a ≠ b}
i j : Fin 2
hij : (fun i ↦ if i = 0 then a else b) i = (fun i ↦ if i = 0 then a else b) j
hi : i = 0
hj : ¬j = 0
⊢ i = j

Tactic:
simp only [if_pos hi, eq_one_of_ne_zero j hj,
          if_neg (Ne.symm Fin.zero_ne_one)] at hij
          apply (h hij).elim

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

Goal state before:
pp: α : Type u_2
m : ℕ
l : List α
h : m ≤ l.length
⊢ (List.take m l).get = take m h l.get ∘ Fin.cast ⋯

Tactic:
by
  ext i
  simp only [List.get_eq_getElem, List.getElem_take, comp_apply, take_apply, val_castLE, val_cast]

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

Goal state before:
pp: case swap.none.some
α : Type u_1
f : α → Option α
l₁ l₂ : List α
a b : α
l : List α
H : Pairwise (fun a b ↦ ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) (b :: a :: l)
h₁ : f a = none
d : α
h₂ : f b = some d
⊢ lookmap f (b :: a :: l) ~ lookmap f (a :: b :: l)

pp: case swap.some.none
α : Type u_1
f : α → Option α
l₁ l₂ : List α
a b : α
l : List α
H : Pairwise (fun a b ↦ ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) (b :: a :: l)
c : α
h₁ : f a = some c
h₂ : f b = none
⊢ lookmap f (b :: a :: l) ~ lookmap f (a :: b :: l)

pp: case swap.some.some
α : Type u_1
f : α → Option α
l₁ l₂ : List α
a b : α
l : List α
H : Pairwise (fun a b ↦ ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) (b :: a :: l)
c : α
h₁ : f a = some c
d : α
h₂ : f b = some d
⊢ lookmap f (b :: a :: l) ~ lookmap f (a :: b :: l)

Tactic:
· simpa [h₁, lookmap_cons_some _ _ h₂] using Perm.swap _ _ _

Goal state after:
case swap.some.none
α : Type u_1
f : α → Option α
l₁ l₂ : List α
a b : α
l : List α
H : Pairwise (fun a b ↦ ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) (b :: a :: l)
c : α
h₁ : f a = some c
h₂ : f b = none
⊢ lookmap f (b :: a :: l) ~ lookmap f (a :: b :: l)

case swap.some.some
α : Type u_1
f : α → Option α
l₁ l₂ : List α
a b : α
l : List α
H : Pairwise (fun a b ↦ ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) (b :: a :: l)
c : α
h₁ : f a = some c
d : α
h₂ : f b = some d
⊢ lookmap f (b :: a :: l) ~ lookmap f (a :: b :: l)
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b b' : β a
s✝ : Finmap β
s : AList β
⊢ insert a b' (insert a b ⟦s⟧) = insert a b' ⟦s⟧

Tactic:
by simp only [insert_toFinmap, AList.insert_insert]

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

Goal state before:
pp: case nil
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
h : a ∈ [].keys
⊢ ∃ b l₁ l₂, ¬a ∈ l₁.keys ∧ [] = l₁ ++ ⟨a, b⟩ :: l₂ ∧ kerase a [] = l₁ ++ l₂

Tactic:
cases h

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
x✝ : List (Sigma β)
h : a ∈ [].keys
⊢ kerase a ([] ++ x✝) = kerase a [] ++ x✝

Tactic:
cases h

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

Goal state before:
pp: case intro.a.inr
ι : Type u_1
α : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)
p : ((i : ι) → Finset (α i)) → Prop
h0 : p fun x ↦ ∅
step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), r i x (g i) → p g → p (update g i (insert x (g i)))
val✝ : Fintype ι
f : (i : ι) → Finset (α i)
ihs : ∀ t ⊂ univ.sigma f, ∀ (f : (i : ι) → Finset (α i)), univ.sigma f = t → p f
hne : (univ.sigma f).Nonempty
i : ι
hi : (f i).Nonempty
⊢ p f

Tactic:
rcases H_ex i (f i) hi with ⟨x, x_mem, hr⟩

Goal state after:
case intro.a.inr
ι : Type u_1
α : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)
p : ((i : ι) → Finset (α i)) → Prop
h0 : p fun x ↦ ∅
step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), r i x (g i) → p g → p (update g i (insert x (g i)))
val✝ : Fintype ι
f : (i : ι) → Finset (α i)
ihs : ∀ t ⊂ univ.sigma f, ∀ (f : (i : ι) → Finset (α i)), univ.sigma f = t → p f
hne : (univ.sigma f).Nonempty
i : ι
hi : (f i).Nonempty
x : α i
x_mem : x ∈ f i
hr : r i x ((f i).erase x)
⊢ p f
Module: Mathlib.Data.Finsupp.BigOperators

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Zero M
l : List (ι →₀ M)
x : ι
⊢ x ∈ foldr (fun x1 x2 ↦ x1.support ⊔ x2) ∅ l ↔ ∃ f ∈ l, x ∈ f.support

Tactic:
simp only [Finset.sup_eq_union, Finsupp.mem_support_iff]

Goal state after:
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Zero M
l : List (ι →₀ M)
x : ι
⊢ x ∈ foldr (fun x1 x2 ↦ x1.support ∪ x2) ∅ l ↔ ∃ f ∈ l, f x ≠ 0
Module: Mathlib.Data.Finsupp.AList

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
a : α
h : ¬f a = 0
this : lookup a f.toAList = some (f a)
⊢ f.toAList.lookupFinsupp a = f a

Tactic:
simp [this]

Goal state after:
Module: Mathlib.Data.Holor

Goal state before:
pp: case eq
α : Type
ds₁ ds₂ ds₃ : List ℕ
inst✝ : Semigroup α
x : Holor α ds₁
y : Holor α ds₂
z : Holor α ds₃
t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)
⊢ ds₁ ++ (ds₂ ++ ds₃) = ds₁ ++ ds₂ ++ ds₃

Tactic:
append_assoc

Goal state after:
case eq
α : Type
ds₁ ds₂ ds₃ : List ℕ
inst✝ : Semigroup α
x : Holor α ds₁
y : Holor α ds₂
z : Holor α ds₃
t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)
⊢ ds₁ ++ (ds₂ ++ ds₃) = ds₁ ++ (ds₂ ++ ds₃)