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

Goal state before:
pp: case pop.nil
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
k : K
q : TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse
f : σ → Option (Γ k) → σ
e : S k = []
⊢ ∃ L',
    (∀ (k : K), ListBlank.map (proj k) L' = ListBlank.mk (List.map some (S k)).reverse) ∧
      (bif (addBottom L).head.1 then TM1.stepAux q (f v none) (Tape.mk' ∅ (addBottom L))
        else
          TM1.stepAux q (f v (∅.head.2 k))
            (Tape.write (∅.head.1, update ∅.head.2 k none) (Tape.mk' ∅.tail (ListBlank.cons ∅.head (addBottom L))))) =
        TM1.stepAux q (f v none) (Tape.mk' ∅ (addBottom L'))

Tactic:
exact ⟨L, hL, by rw [addBottom_head_fst, cond]⟩

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

Goal state before:
pp: K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
q : TM2.Stmt Γ Λ σ
v : σ
T : ListBlank ((i : K) → Option (Γ i))
k : K
S : (k : K) → List (Γ k)
hT : ∀ (k : K), ListBlank.map (proj k) T = ListBlank.mk (List.map some (S k)).reverse
o : StAct K Γ σ k
IH :
  ∀ {v : σ} {S : (k : K) → List (Γ k)} {T : ListBlank ((k : K) → Option (Γ k))},
    (∀ (k : K), ListBlank.map (proj k) T = 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 T))) b
⊢ ∃ b,
    TrCfg (TM2.stepAux (stRun o q) v S) b ∧
      Reaches (TM1.step (tr M)) (TM1.stepAux (trNormal (stRun o q)) v (Tape.mk' ∅ (addBottom T))) b

Tactic:
simp only [trNormal_run, step_run]

Goal state after:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
q : TM2.Stmt Γ Λ σ
v : σ
T : ListBlank ((i : K) → Option (Γ i))
k : K
S : (k : K) → List (Γ k)
hT : ∀ (k : K), ListBlank.map (proj k) T = ListBlank.mk (List.map some (S k)).reverse
o : StAct K Γ σ k
IH :
  ∀ {v : σ} {S : (k : K) → List (Γ k)} {T : ListBlank ((k : K) → Option (Γ k))},
    (∀ (k : K), ListBlank.map (proj k) T = 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 T))) b
⊢ ∃ b,
    TrCfg (TM2.stepAux q (stVar v (S k) o) (update S k (stWrite v (S k) o))) b ∧
      Reaches (TM1.step (tr M)) (TM1.stepAux (goto fun x x_1 ↦ go k o q) v (Tape.mk' ∅ (addBottom T))) b
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
⊢ Respects (TM2.step M) (TM1.step (tr M)) TrCfg

Tactic:
intro c₁ c₂ h

Goal state after:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
c₁ : TM2.Cfg Γ Λ σ
c₂ : TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ
h : TrCfg c₁ c₂
⊢ match TM2.step M c₁ with
  | some b₁ => ∃ b₂, TrCfg b₁ b₂ ∧ Reaches₁ (TM1.step (tr M)) c₂ b₂
  | none => TM1.step (tr M) c₂ = none
Module: Mathlib.Topology.Separation.Profinite

Goal state before:
pp: H : Type u_3
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
x : H
U : Set H
memU : x ∈ U
hU : IsOpen[inst✝³] U
s : Set H
comp : IsCompact s
xs : x ∈ interior s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
u_open_in_s : IsOpen[instTopologicalSpaceSubtype] u
⊢ ∃ v ∈ {s | IsClopen s}, x ∈ v ∧ v ⊆ U

Tactic:
lift x to s using interior_subset xs

Goal state after:
H : Type u_3
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen[inst✝³] U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
u_open_in_s : IsOpen[instTopologicalSpaceSubtype] u
x : { x // x ∈ s }
memU : ↑x ∈ U
xs : ↑x ∈ interior s
⊢ ∃ v ∈ {s | IsClopen s}, ↑x ∈ v ∧ v ⊆ U
Module: Mathlib.Topology.Separation.Profinite

Goal state before:
pp: H : Type u_3
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen[inst✝³] U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
u_open_in_s : IsOpen[instTopologicalSpaceSubtype] u
x : { x // x ∈ s }
memU : ↑x ∈ U
xs : ↑x ∈ interior s
this : CompactSpace ↑s
V : Set ↑s
VisClopen : IsClopen V
Vx : x ∈ V
V_sub : V ⊆ u
⊢ ∃ v ∈ {s | IsClopen s}, ↑x ∈ v ∧ v ⊆ U

Tactic:
have VisClopen' : IsClopen (((↑) : s → H) '' V) := by
    refine ⟨comp.isClosed.isClosedEmbedding_subtypeVal.isClosed_iff_image_isClosed.1 VisClopen.1,
      ?_⟩
    let v : Set u := ((↑) : u → s) ⁻¹' V
    have : ((↑) : u → H) = ((↑) : s → H) ∘ ((↑) : u → s) := rfl
    have f0 : IsEmbedding ((↑) : u → H) := IsEmbedding.subtypeVal.comp IsEmbedding.subtypeVal
    have f1 : IsOpenEmbedding ((↑) : u → H) := by
      refine ⟨f0, ?_⟩
      · have : Set.range ((↑) : u → H) = interior s := by
          rw [this, Set.range_comp, Subtype.range_coe, Subtype.image_preimage_coe]
          apply Set.inter_eq_self_of_subset_right interior_subset
        rw [this]
        apply isOpen_interior
    have f2 : IsOpen v := VisClopen.2.preimage continuous_subtype_val
    have f3 : ((↑) : s → H) '' V = ((↑) : u → H) '' v := by
      rw [this, image_comp, Subtype.image_preimage_coe, inter_eq_self_of_subset_right V_sub]
    rw [f3]
    apply f1.isOpenMap v f2

Goal state after:
H : Type u_3
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen[inst✝³] U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
u_open_in_s : IsOpen[instTopologicalSpaceSubtype] u
x : { x // x ∈ s }
memU : ↑x ∈ U
xs : ↑x ∈ interior s
this : CompactSpace ↑s
V : Set ↑s
VisClopen : IsClopen V
Vx : x ∈ V
V_sub : V ⊆ u
VisClopen' : IsClopen (Subtype.val '' V)
⊢ ∃ v ∈ {s | IsClopen s}, ↑x ∈ v ∧ v ⊆ U
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: case neg
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
⊢ X '' ⋂ c, ↑c = univ

Tactic:
· rw [@iInter_of_empty _ _ <| not_nonempty_iff.mp hC, image_univ_of_surjective X_surj]

Goal state after:
Module: Mathlib.Topology.Category.Stonean.Basic

Goal state before:
pp: X : Profinite
⊢ Epi (π X)

Tactic:
by
  have := (profiniteToCompHaus.obj X).projectivePresentation.epi
  rw [CompHaus.epi_iff_surjective] at this
  rw [epi_iff_surjective]
  exact this

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
⊢ A.proj ⁻¹' {A.proj a} ⊆ B.proj ⁻¹' {ofLE h (A.proj a)}

Tactic:
fiber_eq,

Goal state after:
X : Type u_2
inst✝ : TopologicalSpace X
A B : DiscreteQuotient X
h : A ≤ B
a : X
⊢ ofPred (A.toSetoid a) ⊆ B.proj ⁻¹' {ofLE h (A.proj a)}
Module: Mathlib.Topology.Category.Profinite.AsLimit

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

Tactic:
apply funext

Goal state after:
case h
X : Profinite
a : (fun X ↦ ↑X.toTop) (limitCone X.diagram).pt
b : ↑X.toTop
hb : ∀ (Q : DiscreteQuotient ↑X.toTop), Q.proj b = ↑a Q
⊢ ∀ (x : DiscreteQuotient ↑X.toTop),
    ↑((ConcreteCategory.hom ((limitConeIsLimit X.diagram).lift X.asLimitCone)) b) x = ↑a x
Module: Mathlib.Topology.ClopenBox

Goal state before:
pp: X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : TotallyDisconnectedSpace X
h✝ : SecondCountableTopology X
this : ∀ (s : Clopens X), ∃ t, s.carrier = ⋃₀ (Subtype.val '' ↑t)
f : Clopens X → Finset ↑(countableBasis X) := fun s ↦ ⋯.choose
s t : Clopens X
h : ⋯.choose = ⋯.choose
⊢ s.carrier = t.carrier

Tactic:
(this s).choose_spec,

Goal state after:
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : TotallyDisconnectedSpace X
h✝ : SecondCountableTopology X
this : ∀ (s : Clopens X), ∃ t, s.carrier = ⋃₀ (Subtype.val '' ↑t)
f : Clopens X → Finset ↑(countableBasis X) := fun s ↦ ⋯.choose
s t : Clopens X
h : ⋯.choose = ⋯.choose
⊢ ⋃₀ (Subtype.val '' ↑⋯.choose) = t.carrier
Module: Mathlib.Topology.Category.Profinite.CofilteredLimit

Goal state before:
pp: case refine_3.refine_1
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toTop
hC : IsLimit C
hU : IsClopen U
S : Set (Set ↑(toTopCat.mapCone C).pt)
hS : S ⊆ {U | ∃ j, ∃ V ∈ {W | IsClopen W}, U = ⇑(ConcreteCategory.hom ((toTopCat.mapCone C).π.app j)) ⁻¹' V}
h : U = ⋃₀ S
j : ↑S → J := fun s ↦ Exists.choose ⋯
V : (s : ↑S) → Set ↑(F.obj (j s)).toTop := fun s ↦ ⋯.choose
hV : ∀ (s : ↑S), IsClopen (V s) ∧ ↑s = ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s
hUo : ∀ (i : ↑S), IsOpen ((fun s ↦ ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s) i)
hsU : U ⊆ ⋃ i, (fun s ↦ ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s) i
G : Finset ↑S
hG : U ⊆ ⋃ i ∈ G, ⇑(ConcreteCategory.hom (C.π.app (j i))) ⁻¹' V i
j0 : J
hj0 : ∀ {X : J}, X ∈ Finset.image j G → Nonempty (j0 ⟶ X)
f : (s : ↑S) → s ∈ G → (j0 ⟶ j s) := fun s hs ↦ ⋯.some
W : ↑S → Set ↑(F.obj j0).toTop :=
  fun s ↦ if hs : s ∈ G then ⇑(ConcreteCategory.hom (F.map (f s hs))) ⁻¹' V s else Set.univ
s : ↑S
hs : s ∈ G
⊢ IsClopen (W s)

Tactic:
dsimp [W]

Goal state after:
case refine_3.refine_1
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toTop
hC : IsLimit C
hU : IsClopen U
S : Set (Set ↑(toTopCat.mapCone C).pt)
hS : S ⊆ {U | ∃ j, ∃ V ∈ {W | IsClopen W}, U = ⇑(ConcreteCategory.hom ((toTopCat.mapCone C).π.app j)) ⁻¹' V}
h : U = ⋃₀ S
j : ↑S → J := fun s ↦ Exists.choose ⋯
V : (s : ↑S) → Set ↑(F.obj (j s)).toTop := fun s ↦ ⋯.choose
hV : ∀ (s : ↑S), IsClopen (V s) ∧ ↑s = ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s
hUo : ∀ (i : ↑S), IsOpen ((fun s ↦ ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s) i)
hsU : U ⊆ ⋃ i, (fun s ↦ ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s) i
G : Finset ↑S
hG : U ⊆ ⋃ i ∈ G, ⇑(ConcreteCategory.hom (C.π.app (j i))) ⁻¹' V i
j0 : J
hj0 : ∀ {X : J}, X ∈ Finset.image j G → Nonempty (j0 ⟶ X)
f : (s : ↑S) → s ∈ G → (j0 ⟶ j s) := fun s hs ↦ ⋯.some
W : ↑S → Set ↑(F.obj j0).toTop :=
  fun s ↦ if hs : s ∈ G then ⇑(ConcreteCategory.hom (F.map (f s hs))) ⁻¹' V s else Set.univ
s : ↑S
hs : s ∈ G
⊢ IsClopen (if hs : s ∈ G then ⇑(ConcreteCategory.hom (F.map (f s hs))) ⁻¹' V s else Set.univ)
Module: Mathlib.Condensed.Epi

Goal state before:
pp: A : Type u'
inst✝⁸ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type v'
inst✝⁷ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝⁶ : ConcreteCategory A FA
inst✝⁵ : HasFunctorialSurjectiveInjectiveFactorization A
X Y : Condensed A
f : X ⟶ Y
inst✝⁴ : (coherentTopology CompHaus).WEqualsLocallyBijective A
inst✝³ : HasSheafify (coherentTopology CompHaus) A
inst✝² : (coherentTopology CompHaus).HasSheafCompose (CategoryTheory.forget A)
inst✝¹ : Balanced (Sheaf (coherentTopology CompHaus) A)
inst✝ : PreservesFiniteProducts (CategoryTheory.forget A)
⊢ (∀ (X_1 : CompHaus) (y : ToType (Y.obj.obj (op X_1))),
      ∃ X' φ, ∃ (_ : EffectiveEpi φ), ∃ x, (hom (f.hom.app (op X'))) x = (hom (Y.obj.map (op φ))) y) ↔
    ∀ (S : CompHaus) (y : ToType (Y.obj.obj (op S))),
      ∃ S' φ, ∃ (_ : Function.Surjective ⇑(hom φ)), ∃ x, (hom (f.hom.app (op S'))) x = (hom (Y.obj.map (op φ))) y

Tactic:
simp_rw [((CompHaus.effectiveEpi_tfae _).out 0 2 :)]

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))
⊢ (ihomPoints R P B S) ((ConcreteCategory.hom (((ihom P).map e).hom.app (Opposite.op S))) x) =
    (ihomPoints R P B S) ((ihomPoints R P B S).symm ((ihomPoints R P A S) x ≫ e))

Tactic:
simp only [ihomPoints_apply, ← MonoidalClosed.uncurry_natural_right,
    ← Adjunction.homEquiv_naturality_right_symm, Equiv.apply_symm_apply]

Goal state after:
R : Type u
inst✝ : CommRing R
A B P : LightCondMod R
S : LightProfinite
e : A ⟶ B
x : ↑((P ⟹ A).obj.obj (Opposite.op S))
⊢ MonoidalClosed.uncurry
      (((freeForgetAdjunction R).homEquiv ((coherentTopology LightProfinite).yoneda.obj S) (P ⟹ B)).symm
        ((coherentTopology LightProfinite).yonedaEquiv.symm
          ((ConcreteCategory.hom (((ihom P).map e).hom.app (Opposite.op S))) x))) =
    MonoidalClosed.uncurry
      (((freeForgetAdjunction R).homEquiv ((coherentTopology LightProfinite).yoneda.obj S) (P ⟹ B)).symm
        ((coherentTopology LightProfinite).yonedaEquiv.symm x ≫ (forget R).map ((ihom P).map e)))
Module: Mathlib.Control.Bitraversable.Instances

Goal state before:
pp: t : Type u → Type u → Type u
inst✝³ : Bitraversable t
F : Type u → Type u
inst✝² : Traversable F
inst✝¹ : LawfulTraversable F
inst✝ : LawfulBitraversable t
⊢ LawfulBitraversable (bicompr F t)

Tactic:
by
  constructor <;> intros <;>
    simp [bitraverse, Bicompr.bitraverse, bitraverse_id_id, functor_norm]
  · simp only [bitraverse_eq_bimap_id', traverse_eq_map_id', Function.comp_apply]; rfl
  · dsimp only [bicompr]
    simp [naturality, binaturality']

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

Goal state before:
pp: F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative G
η : ApplicativeTransformation F G
inst✝ : LawfulApplicative F
α : Type u_1
β : Type u
f : α → F β
x : Option α
⊢ (fun {α} ↦ η.app α) (Option.traverse f x) = Option.traverse ((fun {α} ↦ η.app α) ∘ f) x

Tactic:
by
  rcases x with - | x <;> simp! [*, functor_norm, Option.traverse]

Goal state after:
Module: Mathlib.Control.Fold

Goal state before:
pp: α β γ : Type u
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
m : Type u → Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
g : β → γ
f : γ → α → m α
a : α
l : t β
⊢ foldrm f a (g <$> l) = foldrm (f ∘ g) a l

Tactic:
simp only [foldrm, foldMap_map, Function.comp_def]

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

Goal state before:
pp: case pos
α : 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 [hi, hj]

Goal state after:
Module: Mathlib.Data.FinEnum.Option

Goal state before:
pp: case h_2
P : Type u → Sort v
finChoice : (n : ℕ) → Fin (n + 1)
congr : {α β : Type u} → (x : FinEnum α) → (x_1 : FinEnum β) → card β = card α → P α → P β
empty : P PEmpty.{u + 1}
option : {α : Type u} → FinEnum α → P α → P (Option α)
α : Type u
inst✝ : FinEnum α
h : 0 < card α
n✝ : ℕ
heq✝ : card α = n✝.succ
⊢ (let fN := ULift.instFinEnum;
    have this := ⋯;
    congr (insertNone (ULift.{u, 0} (Fin n✝)) ↑↑(finChoice n✝)) inst✝ ⋯
      (option fN (recEmptyOption finChoice (fun {α β} ↦ congr) empty (fun {α} ↦ option) (ULift.{u, 0} (Fin n✝))))) =
    congr (insertNone (ULift.{u, 0} (Fin (card α - 1))) ↑↑(finChoice (card α - 1))) inst✝ ⋯
      (option ULift.instFinEnum
        (recEmptyOption finChoice (fun {α β} ↦ congr) empty (fun {α} ↦ option) (ULift.{u, 0} (Fin (card α - 1)))))

Tactic:
rcases Nat.succ.inj <| (card α).succ_pred_eq_of_pos h |>.trans ‹_› with rfl

Goal state after:
case h_2
P : Type u → Sort v
finChoice : (n : ℕ) → Fin (n + 1)
congr : {α β : Type u} → (x : FinEnum α) → (x_1 : FinEnum β) → card β = card α → P α → P β
empty : P PEmpty.{u + 1}
option : {α : Type u} → FinEnum α → P α → P (Option α)
α : Type u
inst✝ : FinEnum α
h : 0 < card α
heq✝ : card α = (card α).pred.succ
⊢ (let fN := ULift.instFinEnum;
    have this := ⋯;
    congr (insertNone (ULift.{u, 0} (Fin (card α).pred)) ↑↑(finChoice (card α).pred)) inst✝ ⋯
      (option fN
        (recEmptyOption finChoice (fun {α β} ↦ congr) empty (fun {α} ↦ option) (ULift.{u, 0} (Fin (card α).pred))))) =
    congr (insertNone (ULift.{u, 0} (Fin (card α - 1))) ↑↑(finChoice (card α - 1))) inst✝ ⋯
      (option ULift.instFinEnum
        (recEmptyOption finChoice (fun {α β} ↦ congr) empty (fun {α} ↦ option) (ULift.{u, 0} (Fin (card α - 1)))))
Module: Mathlib.Data.List.AList

Goal state before:
pp: case mp.inl
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint s₂
x✝ : α
y✝ : β x✝
h' : dlookup x✝ s₁.entries = some y✝
⊢ dlookup x✝ s₂.entries = some y✝ ∨ ¬x✝ ∈ s₂.entries.keys ∧ dlookup x✝ s₁.entries = some y✝

pp: case mp.inr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint s₂
x✝ : α
y✝ : β x✝
h' : ¬x✝ ∈ s₁.entries.keys ∧ dlookup x✝ s₂.entries = some y✝
⊢ dlookup x✝ s₂.entries = some y✝ ∨ ¬x✝ ∈ s₂.entries.keys ∧ dlookup x✝ s₁.entries = some y✝

Tactic:
· right
          refine ⟨?_, h'⟩
          apply h
          rw [keys, ← List.dlookup_isSome, h']
          exact rfl

Goal state after:
case mp.inr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint s₂
x✝ : α
y✝ : β x✝
h' : ¬x✝ ∈ s₁.entries.keys ∧ dlookup x✝ s₂.entries = some y✝
⊢ dlookup x✝ s₂.entries = some y✝ ∨ ¬x✝ ∈ s₂.entries.keys ∧ dlookup x✝ s₁.entries = some y✝
Module: Mathlib.Data.List.AList

Goal state before:
pp: case mp.inr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint s₂
x✝ : α
y✝ : β x✝
h' : ¬x✝ ∈ s₁.entries.keys ∧ dlookup x✝ s₂.entries = some y✝
⊢ dlookup x✝ s₂.entries = some y✝ ∨ ¬x✝ ∈ s₂.entries.keys ∧ dlookup x✝ s₁.entries = some y✝

Tactic:
left

Goal state after:
case mp.inr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint s₂
x✝ : α
y✝ : β x✝
h' : ¬x✝ ∈ s₁.entries.keys ∧ dlookup x✝ s₂.entries = some y✝
⊢ dlookup x✝ s₂.entries = some y✝
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
l₁ l₂ : List (Sigma β)
a : α
⊢ dlookup a (l₁ ++ l₂) = (dlookup a l₁).or (dlookup a l₂)

Tactic:
induction l₁ with
  | nil => rfl
  | cons s _ _ => by_cases a = s.fst <;> grind

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

Goal state before:
pp: case mpr.inr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint s₂
x✝ : α
y✝ : β x✝
h' : ¬x✝ ∈ s₂.entries.keys ∧ dlookup x✝ s₁.entries = some y✝
⊢ dlookup x✝ s₁.entries = some y✝ ∨ ¬x✝ ∈ s₁.entries.keys ∧ dlookup x✝ s₂.entries = some y✝

Tactic:
left

Goal state after:
case mpr.inr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint s₂
x✝ : α
y✝ : β x✝
h' : ¬x✝ ∈ s₂.entries.keys ∧ dlookup x✝ s₁.entries = some y✝
⊢ dlookup x✝ s₁.entries = some y✝
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : Finmap β
⊢ a = a ∨ a ∉ s

Tactic:
left

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : Finmap β
⊢ a = a
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case neg.inl
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih : a ∈ tl.keys → ∃ b l₁ l₂, ¬a ∈ l₁.keys ∧ tl = l₁ ++ ⟨a, b⟩ :: l₂ ∧ kerase a tl = l₁ ++ l₂
e : ¬a = hd.fst
h : a = hd.fst
⊢ ∃ b l₁ l₂, ¬a ∈ l₁.keys ∧ hd :: tl = l₁ ++ ⟨a, b⟩ :: l₂ ∧ kerase a (hd :: tl) = l₁ ++ l₂

pp: case neg.inr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih : a ∈ tl.keys → ∃ b l₁ l₂, ¬a ∈ l₁.keys ∧ tl = l₁ ++ ⟨a, b⟩ :: l₂ ∧ kerase a tl = l₁ ++ l₂
e : ¬a = hd.fst
h : a ∈ tl.keys
⊢ ∃ b l₁ l₂, ¬a ∈ l₁.keys ∧ hd :: tl = l₁ ++ ⟨a, b⟩ :: l₂ ∧ kerase a (hd :: tl) = l₁ ++ l₂

Tactic:
· exact absurd h e

Goal state after:
case neg.inr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih : a ∈ tl.keys → ∃ b l₁ l₂, ¬a ∈ l₁.keys ∧ tl = l₁ ++ ⟨a, b⟩ :: l₂ ∧ kerase a tl = l₁ ++ l₂
e : ¬a = hd.fst
h : a ∈ tl.keys
⊢ ∃ b l₁ l₂, ¬a ∈ l₁.keys ∧ hd :: tl = l₁ ++ ⟨a, b⟩ :: l₂ ∧ kerase a (hd :: tl) = l₁ ++ l₂
Module: Mathlib.Data.Finsupp.BigOperators

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

Tactic:
convert! Multiset.support_sum_subset s.1; simp

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

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Zero M
s : Multiset (ι →₀ M)
x : ι
x✝ : List (ι →₀ M)
⊢ x ∈ (map Finsupp.support (Quot.mk (⇑(List.isSetoid (ι →₀ M))) x✝)).sup ↔
    ∃ f ∈ Quot.mk (⇑(List.isSetoid (ι →₀ M))) x✝, x ∈ f.support

Tactic:
by
    simpa only [Multiset.quot_mk_to_coe'', Multiset.map_coe, Multiset.sup_coe, List.foldr_map]
    using! List.mem_foldr_sup_support_iff

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

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Finset (ι →₀ M)
hs : (↑s).PairwiseDisjoint Finsupp.support
⊢ (s.sum id).support = s.sup Finsupp.support

Tactic:
suffices s.1.Pairwise (_root_.Disjoint on Finsupp.support) by
    convert! Multiset.support_sum_eq s.1 this
    exact (Finset.sum_val _).symm
  obtain ⟨l, hl, hn⟩ : ∃ l : List (ι →₀ M), l.toFinset = s ∧ l.Nodup := by
    refine ⟨s.toList, ?_, Finset.nodup_toList _⟩
    simp
  subst hl
  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.Holor

Goal state before:
pp: α : Type
ds : List ℕ
inst✝ : NonUnitalNonAssocSemiring α
β : Type u_1
n : ℕ
s✝ : Finset β
f : β → Holor α ds
this : DecidableEq β := Classical.decEq β
x : β
s : Finset β
h_x_notin_s : x ∉ s
ih : (∀ x ∈ s, CPRankMax n (f x)) → CPRankMax (s.card * n) (∑ x ∈ s, f x)
h_cprank : ∀ x_1 ∈ insert x s, CPRankMax n (f x_1)
⊢ CPRankMax (s.card * n + 1 * n) (f x + ∑ x ∈ s, f x)

Tactic:
simp only [Nat.one_mul, Nat.add_comm]

Goal state after:
α : Type
ds : List ℕ
inst✝ : NonUnitalNonAssocSemiring α
β : Type u_1
n : ℕ
s✝ : Finset β
f : β → Holor α ds
this : DecidableEq β := Classical.decEq β
x : β
s : Finset β
h_x_notin_s : x ∉ s
ih : (∀ x ∈ s, CPRankMax n (f x)) → CPRankMax (s.card * n) (∑ x ∈ s, f x)
h_cprank : ∀ x_1 ∈ insert x s, CPRankMax n (f x_1)
⊢ CPRankMax (n + s.card * n) (f x + ∑ x ∈ s, f x)
Module: Mathlib.Data.Int.Lemmas

Goal state before:
pp: case mpr.left
a b r q : ℤ
h : b ≠ 0
hz : 0 ≤ r
hb : r < |b|
⊢ (r + b * q) / b = q

Tactic:
rw [Int.add_mul_ediv_left r q h, ediv_eq_zero_of_lt_abs hz hb]

Goal state after:
case mpr.left
a b r q : ℤ
h : b ≠ 0
hz : 0 ≤ r
hb : r < |b|
⊢ 0 + q = q
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
x : α
⊢ rdropWhile p (l ++ [x]) = if p x = true then rdropWhile p l else l ++ [x]

Tactic:
simp only [rdropWhile, dropWhile, reverse_append, reverse_singleton, singleton_append]
  split_ifs with h <;> simp [h]

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

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
⊢ (rdropWhile p l).reverse <:+ l.reverse

Tactic:
rdropWhile,

Goal state after:
α : Type u_1
p : α → Bool
l : List α
⊢ (dropWhile p l.reverse).reverse.reverse <:+ l.reverse
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
⊢ rdropWhile p l.reverse = (dropWhile p l).reverse

Tactic:
rdropWhile,

Goal state after:
α : Type u_1
p : α → Bool
l : List α
⊢ (dropWhile p l.reverse.reverse).reverse = (dropWhile p l).reverse
Module: Mathlib.Data.List.DropRight

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

Tactic:
simp [rtakeWhile, reverse_eq_iff]

Goal state after: