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

Goal state before:
pp: case succ
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
q : TM2.Stmt Γ Λ σ
v : σ
L : ListBlank ((k : K) → Option (Γ k))
n : ℕ
IH :
  Reaches₀ (TM1.step (tr M))
    { l := some (ret q), var := v, Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L)) }
    { l := some (ret q), var := v, Tape := Tape.mk' ∅ (addBottom L) }
⊢ (bif false then TM1.stepAux (trNormal q) v ((Tape.move Dir.right)^[n + 1] (Tape.mk' ∅ (addBottom L)))
    else
      TM1.stepAux (move Dir.left (goto fun x x_1 ↦ ret q)) v
        ((Tape.move Dir.right)^[n + 1] (Tape.mk' ∅ (addBottom L)))) =
    { l := some (ret q), var := v, Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L)) }

Tactic:
TM1.stepAux,

Goal state after:
case succ
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
q : TM2.Stmt Γ Λ σ
v : σ
L : ListBlank ((k : K) → Option (Γ k))
n : ℕ
IH :
  Reaches₀ (TM1.step (tr M))
    { l := some (ret q), var := v, Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L)) }
    { l := some (ret q), var := v, Tape := Tape.mk' ∅ (addBottom L) }
⊢ (bif false then TM1.stepAux (trNormal q) v ((Tape.move Dir.right)^[n + 1] (Tape.mk' ∅ (addBottom L)))
    else
      TM1.stepAux (goto fun x x_1 ↦ ret q) v
        (Tape.move Dir.left ((Tape.move Dir.right)^[n + 1] (Tape.mk' ∅ (addBottom L))))) =
    { l := some (ret q), var := v, Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L)) }
Module: Mathlib.Topology.Separation.Profinite

Goal state before:
pp: case mp
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : T2Space X
inst✝¹ : CompactSpace X
inst✝ : TotallyDisconnectedSpace X
x : X
U : Set X
hx : ⋂ s, ↑s = {x}
hU : U ∈ 𝓝 x
N : Type (max 0 u_1) := { s // IsClopen s ∧ x ∈ s }
s : Set X
hs : IsClopen s
hs' : x ∈ s
hs'' : ↑⟨s, ⋯⟩ ⊆ U
⊢ ∃ i, (x ∈ i ∧ IsClopen i) ∧ id i ⊆ U

Tactic:
exact ⟨s, ⟨hs', hs⟩, hs''⟩

Goal state after:
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
⊢ univ ⊆ closure U ∪ (closure U)ᶜ

Tactic:
simp only [Set.union_compl_self, Set.subset_univ]

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

Goal state before:
pp: case e'_2
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
s : Option Γ'
L₁ L₂ : List Γ'
S : K' → List Γ'
h₁ : k₁ ≠ rev ∧ k₂ ≠ rev ∧ k₁ ≠ k₂
h₂ : S rev = []
val✝ : Γ'
e : splitAtPred p (S k₁) = (L₁, some val✝, L₂)
⊢ update (update S k₁ (val✝ :: L₂)) k₂ (L₁ ++ S k₂) =
    update
      (update
        (update (update (update S k₁ L₂) rev (L₁.reverseAux (S rev))) k₁
          (val✝ :: update (update S k₁ L₂) rev (L₁.reverseAux (S rev)) k₁))
        rev [])
      k₂
      ((update (update (update S k₁ L₂) rev (L₁.reverseAux (S rev))) k₁
            (val✝ :: update (update S k₁ L₂) rev (L₁.reverseAux (S rev)) k₁) rev).reverseAux
        (update (update (update S k₁ L₂) rev (L₁.reverseAux (S rev))) k₁
          (val✝ :: update (update S k₁ L₂) rev (L₁.reverseAux (S rev)) k₁) k₂))

Tactic:
simp only [h₂, Function.update_comm h₁.1, List.reverseAux_eq, Function.update_self,
      List.append_nil, Function.update_idem]

Goal state after:
case e'_2
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
s : Option Γ'
L₁ L₂ : List Γ'
S : K' → List Γ'
h₁ : k₁ ≠ rev ∧ k₂ ≠ rev ∧ k₁ ≠ k₂
h₂ : S rev = []
val✝ : Γ'
e : splitAtPred p (S k₁) = (L₁, some val✝, L₂)
⊢ update (update S k₁ (val✝ :: L₂)) k₂ (L₁ ++ S k₂) =
    update (update (update S rev []) k₁ (val✝ :: L₂)) k₂
      ((update (update S rev L₁.reverse) k₁ (val✝ :: L₂) rev).reverse ++
        update (update S rev L₁.reverse) k₁ (val✝ :: L₂) k₂)
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: case refine_1
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := Uᶜ ×ˢ {true}
Z₂ : Set (X × Bool) := closure U ×ˢ {false}
Z : Set (X × Bool) := Z₁ ∪ Z₂
hZ₁₂ : Disjoint Z₁ Z₂
hZ₁ : IsClosed Z₁
hZ₂ : IsClosed Z₂
hZ : IsClosed Z
f : ↑Z → X := Prod.fst ∘ Subtype.val
f_cont : Continuous f
f_sur : Surjective f
this : CompactSpace ↑Z
g : X → ↑Z
hg : Continuous g
g_sec : f ∘ g = id
φ : X → X × Bool := Subtype.val ∘ g
hφ : Continuous φ
hφ₁ : ∀ (x : X), (φ x).1 = x
⊢ U ⊆ φ ⁻¹' Z₂

pp: case refine_2
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := Uᶜ ×ˢ {true}
Z₂ : Set (X × Bool) := closure U ×ˢ {false}
Z : Set (X × Bool) := Z₁ ∪ Z₂
hZ₁₂ : Disjoint Z₁ Z₂
hZ₁ : IsClosed Z₁
hZ₂ : IsClosed Z₂
hZ : IsClosed Z
f : ↑Z → X := Prod.fst ∘ Subtype.val
f_cont : Continuous f
f_sur : Surjective f
this : CompactSpace ↑Z
g : X → ↑Z
hg : Continuous g
g_sec : f ∘ g = id
φ : X → X × Bool := Subtype.val ∘ g
hφ : Continuous φ
hφ₁ : ∀ (x : X), (φ x).1 = x
x : X
hx : x ∈ φ ⁻¹' Z₂
⊢ x ∈ closure U

Tactic:
· intro x hx
    have : φ x ∈ Z₁ ∪ Z₂ := (g x).2
    rcases this with hφ | hφ
    · exact ((hφ₁ x ▸ hφ.1) hx).elim
    · exact hφ

Goal state after:
case refine_2
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := Uᶜ ×ˢ {true}
Z₂ : Set (X × Bool) := closure U ×ˢ {false}
Z : Set (X × Bool) := Z₁ ∪ Z₂
hZ₁₂ : Disjoint Z₁ Z₂
hZ₁ : IsClosed Z₁
hZ₂ : IsClosed Z₂
hZ : IsClosed Z
f : ↑Z → X := Prod.fst ∘ Subtype.val
f_cont : Continuous f
f_sur : Surjective f
this : CompactSpace ↑Z
g : X → ↑Z
hg : Continuous g
g_sec : f ∘ g = id
φ : X → X × Bool := Subtype.val ∘ g
hφ : Continuous φ
hφ₁ : ∀ (x : X), (φ x).1 = x
x : X
hx : x ∈ φ ⁻¹' Z₂
⊢ x ∈ closure U
Module: Mathlib.Topology.ExtremallyDisconnected

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

Tactic:
← compl_union,

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

Goal state before:
pp: X : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
disc : TotallyDisconnectedSpace X
x y : X
h : ∀ (Q : DiscreteQuotient X), Q.proj x = Q.proj y
⊢ x = y

Tactic:
← mem_singleton_iff,

Goal state after:
X : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
disc : TotallyDisconnectedSpace X
x y : X
h : ∀ (Q : DiscreteQuotient X), Q.proj x = Q.proj y
⊢ x ∈ {y}
Module: Mathlib.Topology.Category.Profinite.AsLimit

Goal state before:
pp: case refine_1
X : Profinite
a b : (fun X ↦ ↑X.toTop) X.asLimitCone.pt
h :
  (ConcreteCategory.hom ((limitConeIsLimit X.diagram).lift X.asLimitCone)) a =
    (ConcreteCategory.hom ((limitConeIsLimit X.diagram).lift X.asLimitCone)) b
S : DiscreteQuotient ((fun X ↦ ↑X.toTop) X.asLimitCone.pt)
⊢ S.proj a = S.proj b

Tactic:
apply_fun fun f : (limitCone.{u, u} X.diagram).pt => f.val S at h

Goal state after:
case refine_1
X : Profinite
a b : (fun X ↦ ↑X.toTop) X.asLimitCone.pt
S : DiscreteQuotient ((fun X ↦ ↑X.toTop) X.asLimitCone.pt)
h :
  ↑((ConcreteCategory.hom ((limitConeIsLimit X.diagram).lift X.asLimitCone)) a) S =
    ↑((ConcreteCategory.hom ((limitConeIsLimit X.diagram).lift X.asLimitCone)) b) S
⊢ S.proj a = S.proj b
Module: Mathlib.Topology.Category.Profinite.CofilteredLimit

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) (Fin 2)
⊢ ∃ j g, f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g

Tactic:
by
  let U := f ⁻¹' {0}
  have hU : IsClopen U := f.isLocallyConstant.isClopen_fiber _
  obtain ⟨j, V, hV, h⟩ := exists_isClopen_of_cofiltered C hC hU
  classical
  use j, LocallyConstant.ofIsClopen hV
  apply LocallyConstant.locallyConstant_eq_of_fiber_zero_eq
  simp only [Fin.isValue, LocallyConstant.coe_comap, Set.preimage_comp,
    LocallyConstant.ofIsClopen_fiber_zero]
  exact h

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

Goal state before:
pp: case inr
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✝ : Nonempty (Quotient S.toSetoid)
f' : LocallyConstant (↑C.pt.toTop) (Quotient S.toSetoid) := { toFun := S.proj, isLocallyConstant := ⋯ }
j : J
g' : LocallyConstant (↑(F.obj j).toTop) (Quotient S.toSetoid)
hj : f' = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g'
⊢ f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) { toFun := ff ∘ ⇑g', isLocallyConstant := ⋯ }

Tactic:
ext1 t

Goal state after:
case inr
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✝ : Nonempty (Quotient S.toSetoid)
f' : LocallyConstant (↑C.pt.toTop) (Quotient S.toSetoid) := { toFun := S.proj, isLocallyConstant := ⋯ }
j : J
g' : LocallyConstant (↑(F.obj j).toTop) (Quotient S.toSetoid)
hj : f' = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g'
t : ↑C.pt.toTop
⊢ f t = (LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) { toFun := ff ∘ ⇑g', isLocallyConstant := ⋯ }) t
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: case refine_2
I : Type u
inst✝² : Category.{u, u} I
inst✝¹ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
X : Type (u + 1)
hc : IsLimit c
inst✝ : ∀ (i : I), Epi (c.π.app i)
i j : I
fi : LocallyConstant (↑((F ⋙ toProfinite).obj (Opposite.unop (Opposite.op i))).toTop) X
fj : LocallyConstant (↑((F ⋙ toProfinite).obj (Opposite.unop (Opposite.op j))).toTop) X
⊢ (ConcreteCategory.hom (((locallyConstantPresheaf X).mapCocone c.op).ι.app (Opposite.op i))) fi =
      (ConcreteCategory.hom (((locallyConstantPresheaf X).mapCocone c.op).ι.app (Opposite.op j))) fj →
    ∃ k f g,
      (ConcreteCategory.hom (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).map f)) fi =
        (ConcreteCategory.hom (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).map g)) fj

Tactic:
(h : fi.comap (c.π.app i).hom.hom = fj.comap (c.π.app j).hom.hom)

Goal state after:
case refine_2
I : Type u
inst✝² : Category.{u, u} I
inst✝¹ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
X : Type (u + 1)
hc : IsLimit c
inst✝ : ∀ (i : I), Epi (c.π.app i)
i j : I
fi : LocallyConstant (↑((F ⋙ toProfinite).obj (Opposite.unop (Opposite.op i))).toTop) X
fj : LocallyConstant (↑((F ⋙ toProfinite).obj (Opposite.unop (Opposite.op j))).toTop) X
h :
  LocallyConstant.comap (TopCat.Hom.hom (c.π.app i).hom) fi = LocallyConstant.comap (TopCat.Hom.hom (c.π.app j).hom) fj
⊢ ∃ k f g,
    (ConcreteCategory.hom (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).map f)) fi =
      (ConcreteCategory.hom (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).map g)) fj
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: case refine_2
F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
X : Type u
hc : IsLimit c
inst✝ : ∀ (i : ℕᵒᵖ), Epi (c.π.app i)
i j : ℕᵒᵖ
fi : LocallyConstant (↑((F ⋙ toLightProfinite).obj (Opposite.unop (Opposite.op i))).toTop) X
fj : LocallyConstant (↑((F ⋙ toLightProfinite).obj (Opposite.unop (Opposite.op j))).toTop) X
⊢ (ConcreteCategory.hom (((locallyConstantPresheaf X).mapCocone c.op).ι.app (Opposite.op i))) fi =
      (ConcreteCategory.hom (((locallyConstantPresheaf X).mapCocone c.op).ι.app (Opposite.op j))) fj →
    ∃ k f g,
      (ConcreteCategory.hom (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).map f)) fi =
        (ConcreteCategory.hom (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).map g)) fj

Tactic:
(h : fi.comap (c.π.app i).hom.hom = fj.comap (c.π.app j).hom.hom)

Goal state after:
case refine_2
F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
X : Type u
hc : IsLimit c
inst✝ : ∀ (i : ℕᵒᵖ), Epi (c.π.app i)
i j : ℕᵒᵖ
fi : LocallyConstant (↑((F ⋙ toLightProfinite).obj (Opposite.unop (Opposite.op i))).toTop) X
fj : LocallyConstant (↑((F ⋙ toLightProfinite).obj (Opposite.unop (Opposite.op j))).toTop) X
h :
  LocallyConstant.comap (TopCat.Hom.hom (c.π.app i).hom) fi = LocallyConstant.comap (TopCat.Hom.hom (c.π.app j).hom) fj
⊢ ∃ k f g,
    (ConcreteCategory.hom (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).map f)) fi =
      (ConcreteCategory.hom (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).map g)) fj
Module: Mathlib.Condensed.Light.InternallyProjective

Goal state before:
pp: case refine_2
R : Type u
inst✝ : CommRing R
P : LightProfinite
h :
  ∀ {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
A B : LightCondMod R
e : A ⟶ B
he : Epi e
S : LightProfinite
g : (free R).obj (P.toCondensed ⊗ S.toCondensed) ⟶ B
⊢ ∃ S' π,
    ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
      ∃ g', (free R).map (P.toCondensed ◁ lightProfiniteToLightCondSet.map π) ≫ g = g' ≫ e

Tactic:
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.Data.Fin.Fin2

Goal state before:
pp: case zero
⊢ last.rev = fz

Tactic:
simp_all [rev, castSucc, last]

Goal state after:
Module: Mathlib.Data.Fin.Fin2

Goal state before:
pp: case succ
n✝ : ℕ
a✝ : last.rev = fz
⊢ last.rev = fz

Tactic:
simp_all [rev, castSucc, last]

Goal state after:
Module: Mathlib.Data.Fin.Fin2

Goal state before:
pp: case fz
n n✝ : ℕ
⊢ fz.castSucc.rev = fz.rev.fs

Tactic:
simp_all [rev, castSucc, last]

Goal state after:
Module: Mathlib.Data.Fin.Fin2

Goal state before:
pp: case fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ : a✝.castSucc.rev = a✝.rev.fs
⊢ a✝.fs.castSucc.rev = a✝.fs.rev.fs

Tactic:
simp_all [rev, castSucc, last]

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

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
P : β → Prop
x : F (α ::: β)
u✝ : F fun i ↦ { p_1 // ofRepeat (α.PredLast' P i p_1) }
this : (fun i ↦ Subtype.val) = fun i x ↦ ↑(f P n α i x)
⊢ (fun i ↦ Subtype.val) <$$> u✝ = x ↔ (fun i x ↦ ↑(f P n α i x)) <$$> u✝ = x

Tactic:
by rw [this]

Goal state after:
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} (β : Type u) (x : α) (dead : Label α (ReaderT ρ m) β → β → ReaderT ρ m α),
    (callCC fun f ↦ goto f x >>= dead f) = pure x

Tactic:
by
    intros; simp only [callCC, ReaderT.callCC, ReaderT.goto_mkLabel, ReaderT.run_bind,
      ReaderT.run_monadLift, monadLift_self, callCC_bind_left]
    ext; rfl

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

Goal state before:
pp: S : Type u_1
T : Type u_2
X : Type u_3
π : T → S × Option X
σ : Option X → S → T
hσ : ∀ (x : Option X) (s : S), (π (σ x s)).1 = s
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
t : T
ht : t ∈ fibres π σ
t' : T
ht' : t' ∈ fibres π σ
property✝ : π_r π σ (⟨t, ht⟩, ⟨t', ht'⟩).1 = π_r π σ (⟨t, ht⟩, ⟨t', ht'⟩).2
⊢ ∃ a, coverToFun (fibreIncl π σ) (π_r π σ) a = ⟨(⟨t, ht⟩, ⟨t', ht'⟩), property✝⟩

Tactic:
by_cases h : (π t).2 = none

Goal state after:
case pos
S : Type u_1
T : Type u_2
X : Type u_3
π : T → S × Option X
σ : Option X → S → T
hσ : ∀ (x : Option X) (s : S), (π (σ x s)).1 = s
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
t : T
ht : t ∈ fibres π σ
t' : T
ht' : t' ∈ fibres π σ
property✝ : π_r π σ (⟨t, ht⟩, ⟨t', ht'⟩).1 = π_r π σ (⟨t, ht⟩, ⟨t', ht'⟩).2
h : (π t).2 = none
⊢ ∃ a, coverToFun (fibreIncl π σ) (π_r π σ) a = ⟨(⟨t, ht⟩, ⟨t', ht'⟩), property✝⟩

case neg
S : Type u_1
T : Type u_2
X : Type u_3
π : T → S × Option X
σ : Option X → S → T
hσ : ∀ (x : Option X) (s : S), (π (σ x s)).1 = s
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
t : T
ht : t ∈ fibres π σ
t' : T
ht' : t' ∈ fibres π σ
property✝ : π_r π σ (⟨t, ht⟩, ⟨t', ht'⟩).1 = π_r π σ (⟨t, ht⟩, ⟨t', ht'⟩).2
h : ¬(π t).2 = none
⊢ ∃ a, coverToFun (fibreIncl π σ) (π_r π σ) a = ⟨(⟨t, ht⟩, ⟨t', ht'⟩), property✝⟩
Module: Mathlib.Control.Traversable.Equiv

Goal state before:
pp: t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝⁶ : Traversable t
inst✝⁵ : LawfulTraversable t
inst✝⁴ : Traversable t'
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
h₂ :
  ∀ {F : Type u → Type u} [inst : Applicative F] [LawfulApplicative F] {α β : Type u} (f : α → F β),
    traverse f = Equiv.traverse eqv f
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
x✝⁴ : ApplicativeTransformation F✝ G✝
x✝³ x✝² : Type u
x✝¹ : x✝³ → F✝ x✝²
x✝ : t' x✝³
⊢ (fun {α} ↦ x✝⁴.app α) (traverse x✝¹ x✝) = traverse ((fun {α} ↦ x✝⁴.app α) ∘ x✝¹) x✝

Tactic:
by rw [h₂, Equiv.naturality, h₂]

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
⊢ (¬∃ 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

Tactic:
simp [not_exists, not_and, not_forall, and_comm]

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

Goal state before:
pp: case refine_2
S T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
inst✝ : Epi π
this✝ : CompactSpace ↑(S' ⇑(ConcreteCategory.hom π))
S'π : (n : ↑ℕ∪{∞}.toTop) →
  LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⟶ LightProfinite.fibre n (π ≫ snd S ℕ∪{∞}) := ⋯
y' : LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⟶ S := ⋯
π' : pullback π (y' ▷ ℕ∪{∞}) ⟶ LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⊗ ℕ∪{∞} := ⋯
σ' : ↑ℕ∪{∞}.toTop → ↑(LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))).toTop → ↑(pullback π (y' ▷ ℕ∪{∞})).toTop := ⋯
hσ :
  ∀ (x : ↑ℕ∪{∞}.toTop) (s : ↑(LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))).toTop),
    ((ConcreteCategory.hom π') (σ' x s)).1 = s
hσ' :
  ∀ (x : ↑ℕ∪{∞}.toTop) (s : ↑(LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))).toTop),
    ((ConcreteCategory.hom π') (σ' x s)).2 = x
this : CompactSpace ↑(fibres (⇑(ConcreteCategory.hom π')) σ')
⊢ Function.Surjective ⇑(ConcreteCategory.hom π)

Tactic:
rwa [← LightProfinite.epi_iff_surjective]

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

Goal state before:
pp: C : FloatCfg
n d : ℕ+
e₁ : ℤ := ↑(↑n).size - ↑(↑d).size - ↑prec
d₁ n₁ : ℕ
e₂ : ℤ := if n₁ < d₁ then e₁ - 1 else e₁
e₃ : ℤ := max e₂ emin
d₂ n₂ : ℕ
⊢ Float × Bool

Tactic:
let r := mkRat n₂ d₂

Goal state after:
C : FloatCfg
n d : ℕ+
e₁ : ℤ := ↑(↑n).size - ↑(↑d).size - ↑prec
d₁ n₁ : ℕ
e₂ : ℤ := if n₁ < d₁ then e₁ - 1 else e₁
e₃ : ℤ := max e₂ emin
d₂ n₂ : ℕ
r : ℚ := mkRat (↑n₂) d₂
⊢ Float × Bool
Module: Mathlib.Data.Semiquot

Goal state before:
pp: α : Type u_1
a b : α
ab : b = a
c : α
ac : c = a
⊢ b = c

Tactic:
← ac

Goal state after:
α : Type u_1
a b c : α
ab : b = c
ac : c = a
⊢ b = c
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:
Perm.ext_iff

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.List.Lookmap

Goal state before:
pp: α : Type u_1
f : α → Option α
l : List α
acc : Array α
⊢ go f l acc = acc.toListAppend (lookmap f l)

Tactic:
cases l with
  | nil => simp [go, lookmap]
  | cons hd tl =>
    rw [lookmap, go, go]
    cases f hd with
    | none =>
      simp only [go_append tl _, Array.toListAppend_eq, append_assoc, Array.toList_push]
      rfl
    | some a => simp

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

Goal state before:
pp: case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
tail✝ : List (Sigma β)
l_ih : dlookup a tail✝.dedupKeys = dlookup a tail✝
a' : α
b : β a'
h : ¬a = a'
⊢ dlookup a (⟨a', b⟩ :: tail✝).dedupKeys = dlookup a (⟨a', b⟩ :: tail✝)

Tactic:
rw [dedupKeys_cons, dlookup_kinsert_ne h, l_ih, dlookup_cons_ne]
      exact h

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

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
l : List (ι →₀ M)
hn : l.Nodup
hs : (↑l.toFinset).PairwiseDisjoint Finsupp.support
⊢ Multiset.Pairwise (Disjoint on Finsupp.support) l.toFinset.val

Tactic:
rwa [List.toFinset_val, List.dedup_eq_self.mpr hn, Multiset.pairwise_coe_iff_pairwise,
    ← List.pairwiseDisjoint_iff_coe_toFinset_pairwise_disjoint hn]

Goal state after:
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case false.false
n : ℤ
⊢ (2 * n + bif false then 1 else 0).bodd = false

Tactic:
simp [(show bodd 2 = false by rfl)]

Goal state after:
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case false.true
n : ℤ
⊢ (2 * n + bif false then 1 else 0).bodd = false

Tactic:
simp [(show bodd 2 = false by rfl)]

Goal state after:
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case true.false
n : ℤ
⊢ (2 * n + bif true then 1 else 0).bodd = true

Tactic:
simp [(show bodd 2 = false by rfl)]

Goal state after:
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case true.true
n : ℤ
⊢ (2 * n + bif true then 1 else 0).bodd = true

Tactic:
simp [(show bodd 2 = false by rfl)]

Goal state after:
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: b : Bool
n : ℕ
⊢ (bit b ↑n).testBit 0 = b

Tactic:
bit_coe_nat

Goal state after:
b : Bool
n : ℕ
⊢ (↑(Nat.bit b n)).testBit 0 = b
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: m : ℕ
b : Bool
n : ℕ
⊢ (bit b ↑n).testBit m.succ = (↑n).testBit m

Tactic:
bit_coe_nat

Goal state after:
m : ℕ
b : Bool
n : ℕ
⊢ (↑(Nat.bit b n)).testBit m.succ = (↑n).testBit m
Module: Mathlib.Data.Int.Lemmas

Goal state before:
pp: a b : ℤ
ha : 0 ≤ a
hb : b ≤ 0
⊢ a.natAbs = b.natAbs ↔ a = -b

Tactic:
by
  simpa only [Int.natAbs_neg] using natAbs_inj_of_nonneg_of_nonneg ha (neg_nonneg_of_nonpos hb)

Goal state after:
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
inst✝ : Semiring α
d : ℕ
ds : List ℕ
x : Holor α (d :: ds)
h_summands : ∀ (i : ↥(Finset.range d)), CPRankMax ds.prod (unitVec d ↑i ⊗ x.slice ↑i ⋯)
h_dds_prod : (d :: ds).prod = (Finset.range d).card * ds.prod
this : CPRankMax ((Finset.range d).attach.card * ds.prod) (∑ i ∈ (Finset.range d).attach, unitVec d ↑i ⊗ x.slice ↑i ⋯)
⊢ CPRankMax ((Finset.range d).card * ds.prod) (∑ i ∈ (Finset.range d).attach, unitVec d ↑i ⊗ x.slice ↑i ⋯)

Tactic:
rwa [Finset.card_attach] at this

Goal state after: