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

Goal state before:
pp: case ret
q' : Λ'
k✝ : Cont'
⊢ q' ∈ trStmts₁ (Λ'.ret k✝) → trStmts₁ q' ⊆ trStmts₁ (Λ'.ret k✝)

Tactic:
simp +contextual only [trStmts₁, Finset.mem_insert, Finset.mem_union,
      or_imp, Finset.mem_singleton, Finset.Subset.refl, imp_true_iff, true_and]

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

Goal state before:
pp: case left
I : Type u
inst✝² : SmallCategory I
inst✝¹ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
hc : IsLimit c
inst✝ : ∀ (i : I), Epi (c.π.app i)
e : I ≌ ULiftHom (ULift.{w, u} I) := ULiftHomULiftCategory.equiv I
left✝ : Discrete PUnit.{1}
X : FintypeCat
f : c.pt ⟶ toProfinite.obj X
⊢ ∃ c_1, Nonempty ((e.inverse ⋙ functor c).obj c_1 ⟶ { left := left✝, right := X, hom := f })

Tactic:
obtain ⟨i, g, h⟩ := exists_hom c hc f

Goal state after:
case left
I : Type u
inst✝² : SmallCategory I
inst✝¹ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
hc : IsLimit c
inst✝ : ∀ (i : I), Epi (c.π.app i)
e : I ≌ ULiftHom (ULift.{w, u} I) := ULiftHomULiftCategory.equiv I
left✝ : Discrete PUnit.{1}
X : FintypeCat
f : c.pt ⟶ toProfinite.obj X
i : I
g : F.obj i ⟶ X
h : f = c.π.app i ≫ toProfinite.map g
⊢ ∃ c_1, Nonempty ((e.inverse ⋙ functor c).obj c_1 ⟶ { left := left✝, right := X, hom := f })
Module: Mathlib.Topology.Category.Profinite.Extend

Goal state before:
pp: case right
I : Type u
inst✝² : SmallCategory I
inst✝¹ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
hc : IsLimit c
inst✝ : ∀ (i : I), Epi (c.π.app i)
e : I ≌ ULiftHom (ULift.{w, u} I) := ULiftHomULiftCategory.equiv I
left✝² : Discrete PUnit.{1}
X : FintypeCat
f : c.pt ⟶ toProfinite.obj X
i : I
left✝¹ : ((e.inverse ⋙ functor c).obj { down := i }).left ⟶ { left := left✝², right := X, hom := f }.left
s : F.obj i ⟶ X
w : f = c.π.app i ≫ toProfinite.map s
left✝ : ((e.inverse ⋙ functor c).obj { down := i }).left ⟶ { left := left✝², right := X, hom := f }.left
s' : F.obj i ⟶ X
w' : f = c.π.app i ≫ toProfinite.map s'
⊢ ∃ c' t,
    StructuredArrow.Hom.right ((e.inverse ⋙ functor c).map t) ≫
        StructuredArrow.Hom.right { left := left✝¹, right := s, w := w } =
      StructuredArrow.Hom.right ((e.inverse ⋙ functor c).map t) ≫
        StructuredArrow.Hom.right { left := left✝, right := s', w := w' }

Tactic:
refine ⟨⟨i⟩, 𝟙 _, ?_⟩

Goal state after:
case right
I : Type u
inst✝² : SmallCategory I
inst✝¹ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
hc : IsLimit c
inst✝ : ∀ (i : I), Epi (c.π.app i)
e : I ≌ ULiftHom (ULift.{w, u} I) := ULiftHomULiftCategory.equiv I
left✝² : Discrete PUnit.{1}
X : FintypeCat
f : c.pt ⟶ toProfinite.obj X
i : I
left✝¹ : ((e.inverse ⋙ functor c).obj { down := i }).left ⟶ { left := left✝², right := X, hom := f }.left
s : F.obj i ⟶ X
w : f = c.π.app i ≫ toProfinite.map s
left✝ : ((e.inverse ⋙ functor c).obj { down := i }).left ⟶ { left := left✝², right := X, hom := f }.left
s' : F.obj i ⟶ X
w' : f = c.π.app i ≫ toProfinite.map s'
⊢ StructuredArrow.Hom.right ((e.inverse ⋙ functor c).map (𝟙 { down := i })) ≫
      StructuredArrow.Hom.right { left := left✝¹, right := s, w := w } =
    StructuredArrow.Hom.right ((e.inverse ⋙ functor c).map (𝟙 { down := i })) ≫
      StructuredArrow.Hom.right { left := left✝, right := s', w := w' }
Module: Mathlib.Condensed.Discrete.Module

Goal state before:
pp: case e_a
P : TopCat → Prop
R : Type (u + 1)
inst✝ : Ring R
X✝ Y✝ : ModuleCat R
f : X✝ ⟶ Y✝
⊢ (discrete (ModuleCat R)).map ((underlying (ModuleCat R)).map ((functor R).map f)) =
    ((functorIsoDiscreteAux₂ R X✝).inv ≫
        (presheafToSheaf (coherentTopology CompHaus) (ModuleCat R)).map ((Functor.const CompHausᵒᵖ).map f)) ≫
      (functorIsoDiscreteAux₂ R Y✝).hom

Tactic:
← Iso.comp_inv_eq

Goal state after:
case e_a
P : TopCat → Prop
R : Type (u + 1)
inst✝ : Ring R
X✝ Y✝ : ModuleCat R
f : X✝ ⟶ Y✝
⊢ (discrete (ModuleCat R)).map ((underlying (ModuleCat R)).map ((functor R).map f)) ≫
      (functorIsoDiscreteAux₂ R Y✝).inv =
    (functorIsoDiscreteAux₂ R X✝).inv ≫
      (presheafToSheaf (coherentTopology CompHaus) (ModuleCat R)).map ((Functor.const CompHausᵒᵖ).map f)
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
X✝ : TopCat
inst✝² : HasExplicitFiniteCoproducts P
inst✝¹ : HasExplicitPullbacks P
hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Surjective ⇑(ConcreteCategory.hom f)
inst✝ : HasExplicitFiniteCoproducts P
X : Type (max u w)
⊢ ((functor P hs).map ((unit P hs).app X) ≫ (counit P hs).app ((functor P hs).obj X)).hom =
    (𝟙 ((functor P hs).obj X)).hom

Tactic:
exact adjunction_left_triangle P hs X

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

Goal state before:
pp: case e_a
P : TopCat → Prop
R : Type u
inst✝ : Ring R
X✝ Y✝ : ModuleCat R
f : X✝ ⟶ Y✝
⊢ (discrete (ModuleCat R)).map ((underlying (ModuleCat R)).map ((functor R).map f)) =
    ((functorIsoDiscreteAux₂ R X✝).inv ≫
        (presheafToSheaf (coherentTopology LightProfinite) (ModuleCat R)).map
          ((Functor.const LightProfiniteᵒᵖ).map f)) ≫
      (functorIsoDiscreteAux₂ R Y✝).hom

Tactic:
← Iso.comp_inv_eq

Goal state after:
case e_a
P : TopCat → Prop
R : Type u
inst✝ : Ring R
X✝ Y✝ : ModuleCat R
f : X✝ ⟶ Y✝
⊢ (discrete (ModuleCat R)).map ((underlying (ModuleCat R)).map ((functor R).map f)) ≫
      (functorIsoDiscreteAux₂ R Y✝).inv =
    (functorIsoDiscreteAux₂ R X✝).inv ≫
      (presheafToSheaf (coherentTopology LightProfinite) (ModuleCat R)).map ((Functor.const LightProfiniteᵒᵖ).map f)
Module: Mathlib.Topology.Category.LightProfinite.Sequence

Goal state before:
pp: case refine_1
⊢ Function.Injective ⇑natUnionInftyEmbedding

Tactic:
rintro (_ | n) (_ | m) h

Goal state after:
case refine_1.none.none
h : natUnionInftyEmbedding none = natUnionInftyEmbedding none
⊢ none = none

case refine_1.none.some
m : ℕ
h : natUnionInftyEmbedding none = natUnionInftyEmbedding (Option.some m)
⊢ none = Option.some m

case refine_1.some.none
n : ℕ
h : natUnionInftyEmbedding (Option.some n) = natUnionInftyEmbedding none
⊢ Option.some n = none

case refine_1.some.some
n m : ℕ
h : natUnionInftyEmbedding (Option.some n) = natUnionInftyEmbedding (Option.some m)
⊢ Option.some n = Option.some m
Module: Mathlib.Condensed.TopCatAdjunction

Goal state before:
pp: X✝ X : CondensedSet
Y : Type (u + 1)
tY✝ : TopologicalSpace Y
⊢ ∀ (f : ↑X.toTopCat → Y), (∀ (S : CompHaus) (g : C(↑S.toTop, ↑X.toTopCat)), Continuous (f ∘ ⇑g)) → Continuous f

Tactic:
f

Goal state after:
X✝ X : CondensedSet
Y : Type (u + 1)
tY✝ : TopologicalSpace Y
f : ↑X.toTopCat → Y
⊢ (∀ (S : CompHaus) (g : C(↑S.toTop, ↑X.toTopCat)), Continuous (f ∘ ⇑g)) → Continuous f
Module: Mathlib.Control.Bitraversable.Instances

Goal state before:
pp: case id_bitraverse
t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
α✝ β✝ : Type u_1
x✝ : α✝ × β✝
⊢ bitraverse pure pure x✝ = pure x✝

Tactic:
casesm _ × _

Goal state after:
case id_bitraverse
t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
α✝ β✝ : Type u_1
fst✝ : α✝
snd✝ : β✝
⊢ bitraverse pure pure (fst✝, snd✝) = pure (fst✝, snd✝)
Module: Mathlib.Control.Bitraversable.Instances

Goal state before:
pp: case comp_bitraverse
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F : Type u → Type u
inst✝⁴ : Applicative F
F✝ G✝ : Type u_1 → Type u_1
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ α'✝ β✝ β'✝ γ✝ γ'✝ : Type u_1
f✝ : β✝ → F✝ γ✝
f'✝ : β'✝ → F✝ γ'✝
g✝ : α✝ → G✝ β✝
g'✝ : α'✝ → G✝ β'✝
x✝ : α✝ × α'✝
⊢ bitraverse (Functor.Comp.mk ∘ Functor.map f✝ ∘ g✝) (Functor.Comp.mk ∘ Functor.map f'✝ ∘ g'✝) x✝ =
    Functor.Comp.mk (bitraverse f✝ f'✝ <$> bitraverse g✝ g'✝ x✝)

Tactic:
casesm _ × _

Goal state after:
case comp_bitraverse
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F : Type u → Type u
inst✝⁴ : Applicative F
F✝ G✝ : Type u_1 → Type u_1
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ α'✝ β✝ β'✝ γ✝ γ'✝ : Type u_1
f✝ : β✝ → F✝ γ✝
f'✝ : β'✝ → F✝ γ'✝
g✝ : α✝ → G✝ β✝
g'✝ : α'✝ → G✝ β'✝
fst✝ : α✝
snd✝ : α'✝
⊢ bitraverse (Functor.Comp.mk ∘ Functor.map f✝ ∘ g✝) (Functor.Comp.mk ∘ Functor.map f'✝ ∘ g'✝) (fst✝, snd✝) =
    Functor.Comp.mk (bitraverse f✝ f'✝ <$> bitraverse g✝ g'✝ (fst✝, snd✝))
Module: Mathlib.Control.Bitraversable.Instances

Goal state before:
pp: case bitraverse_eq_bimap_id
t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
α✝ α'✝ β✝ β'✝ : Type u_1
f✝ : α✝ → β✝
f'✝ : α'✝ → β'✝
x✝ : α✝ × α'✝
⊢ bitraverse (pure ∘ f✝) (pure ∘ f'✝) x✝ = pure (bimap f✝ f'✝ x✝)

Tactic:
casesm _ × _

Goal state after:
case bitraverse_eq_bimap_id
t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
α✝ α'✝ β✝ β'✝ : Type u_1
f✝ : α✝ → β✝
f'✝ : α'✝ → β'✝
fst✝ : α✝
snd✝ : α'✝
⊢ bitraverse (pure ∘ f✝) (pure ∘ f'✝) (fst✝, snd✝) = pure (bimap f✝ f'✝ (fst✝, snd✝))
Module: Mathlib.Control.Bitraversable.Instances

Goal state before:
pp: case binaturality
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F : Type u → Type u
inst✝⁴ : Applicative F
F✝ G✝ : Type u_1 → Type u_1
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
η✝ : ApplicativeTransformation F✝ G✝
α✝ α'✝ β✝ β'✝ : Type u_1
f✝ : α✝ → F✝ β✝
f'✝ : α'✝ → F✝ β'✝
x✝ : α✝ × α'✝
⊢ (fun {α} ↦ η✝.app α) (bitraverse f✝ f'✝ x✝) = bitraverse ((fun {α} ↦ η✝.app α) ∘ f✝) ((fun {α} ↦ η✝.app α) ∘ f'✝) x✝

Tactic:
casesm _ × _

Goal state after:
case binaturality
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F : Type u → Type u
inst✝⁴ : Applicative F
F✝ G✝ : Type u_1 → Type u_1
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
η✝ : ApplicativeTransformation F✝ G✝
α✝ α'✝ β✝ β'✝ : Type u_1
f✝ : α✝ → F✝ β✝
f'✝ : α'✝ → F✝ β'✝
fst✝ : α✝
snd✝ : α'✝
⊢ (fun {α} ↦ η✝.app α) (bitraverse f✝ f'✝ (fst✝, snd✝)) =
    bitraverse ((fun {α} ↦ η✝.app α) ∘ f✝) ((fun {α} ↦ η✝.app α) ∘ f'✝) (fst✝, snd✝)
Module: Mathlib.Control.Fold

Goal state before:
pp: α : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
xs : t α
⊢ length xs = (toList xs).length

Tactic:
unfold length

Goal state after:
α : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
xs : t α
⊢ (foldl (fun l x ↦ { down := l.down + 1 }) { down := 0 } xs).down = (toList xs).length
Module: Mathlib.Data.Analysis.Topology

Goal state before:
pp: α : Type u_1
T : TopologicalSpace α
F : Realizer α
s : Set α
a : α
⊢ s ∈ 𝓝 a ↔ ∃ b, a ∈ F.F.f b ∧ F.F.f b ⊆ s

Tactic:
by
  have := @mem_nhds_toTopsp _ _ F.F s a; rwa [F.eq] at this

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

Goal state before:
pp: α : Type u_1
T : TopologicalSpace α
σ : Type u_5
F : Ctop α σ
H : ∀ (a : α) (s : Set α), s ∈ 𝓝 a ↔ ∃ b, a ∈ F.f b ∧ F.f b ⊆ s
⊢ F.toTopsp = T

Tactic:
refine TopologicalSpace.ext_nhds fun x ↦ ?_

Goal state after:
α : Type u_1
T : TopologicalSpace α
σ : Type u_5
F : Ctop α σ
H : ∀ (a : α) (s : Set α), s ∈ 𝓝 a ↔ ∃ b, a ∈ F.f b ∧ F.f b ⊆ s
x : α
⊢ 𝓝 x = 𝓝 x
Module: Mathlib.Data.Analysis.Filter

Goal state before:
pp: case mk.mk.mp
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
σ✝¹ : Type ?u.88
F✝¹ : CFilter (Set α) σ✝¹
σ✝ : Type ?u.92
F✝ : CFilter (Set α) σ✝
s✝ : Set α
⊢ s✝ ∈ { sets := {a | ∃ a_1 b, F✝¹.f a_1 ∩ F✝.f b ⊆ a}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ } →
    s✝ ∈
      { sets := {a | ∃ b, F✝¹.f b ⊆ a}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ } ⊓
        { sets := {a | ∃ b, F✝.f b ⊆ a}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }

pp: case mk.mk.mpr
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
σ✝¹ : Type ?u.88
F✝¹ : CFilter (Set α) σ✝¹
σ✝ : Type ?u.92
F✝ : CFilter (Set α) σ✝
s✝ : Set α
⊢ s✝ ∈
      { sets := {a | ∃ b, F✝¹.f b ⊆ a}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ } ⊓
        { sets := {a | ∃ b, F✝.f b ⊆ a}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ } →
    s✝ ∈ { sets := {a | ∃ a_1 b, F✝¹.f a_1 ∩ F✝.f b ⊆ a}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }

Tactic:
· rintro ⟨s, t, h⟩
        apply mem_inf_of_inter _ _ h
        · use s
        · use t

Goal state after:
case mk.mk.mpr
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
σ✝¹ : Type ?u.88
F✝¹ : CFilter (Set α) σ✝¹
σ✝ : Type ?u.92
F✝ : CFilter (Set α) σ✝
s✝ : Set α
⊢ s✝ ∈
      { sets := {a | ∃ b, F✝¹.f b ⊆ a}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ } ⊓
        { sets := {a | ∃ b, F✝.f b ⊆ a}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ } →
    s✝ ∈ { sets := {a | ∃ a_1 b, F✝¹.f a_1 ∩ F✝.f b ⊆ a}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }
Module: Mathlib.Data.Erased

Goal state before:
pp: α : Sort u_1
β : Sort u_2
f : α → β
a : Erased α
⊢ (map f a).out = f a.out

Tactic:
by simp [map]

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

Goal state before:
pp: R : Type
inst✝ : CommRing R
X Y : LightCondMod R
p : X ⟶ Y
hp : Epi p
S : LightProfinite
⊢ ∀ (g : (free R).obj (S ⊗ ℕ∪{∞}).toCondensed ⟶ Y),
    ∃ S' π,
      ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
        ∃ g', (free R).map (lightProfiniteToLightCondSet.map (π ▷ ℕ∪{∞})) ≫ g = g' ≫ p

Tactic:
f

Goal state after:
R : Type
inst✝ : CommRing R
X Y : LightCondMod R
p : X ⟶ Y
hp : Epi p
S : LightProfinite
f : (free R).obj (S ⊗ ℕ∪{∞}).toCondensed ⟶ Y
⊢ ∃ S' π,
    ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
      ∃ g', (free R).map (lightProfiniteToLightCondSet.map (π ▷ ℕ∪{∞})) ≫ f = g' ≫ p
Module: Mathlib.Data.List.Lookmap

Goal state before:
pp: case swap
α : 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)
⊢ lookmap f (b :: a :: l) ~ lookmap f (a :: b :: l)

Tactic:
rcases h₁ : f a with - | c <;> rcases h₂ : f b with - | d

Goal state after:
case swap.none.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)
h₁ : f a = none
h₂ : f b = none
⊢ lookmap f (b :: a :: l) ~ lookmap f (a :: b :: l)

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)

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

Goal state before:
pp: α : Type u
β : α → Type v
s₁ s₂ : AList β
h : s₁.entries ⊆ s₂.entries
k : α
hk : k ∈ s₁.keys
this✝ : DecidableEq α := Classical.decEq α
this : lookup k s₂ = some ((lookup k s₁).get ⋯)
⊢ (some ((lookup k s₁).get ⋯)).isSome = true

Tactic:
exact Option.isSome_some

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : AList β
⊢ (kextract a s.entries).snd.NodupKeys

Tactic:
kextract_eq_dlookup_kerase

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : AList β
⊢ (dlookup a s.entries, kerase a s.entries).snd.NodupKeys
Module: Mathlib.Data.Finset.Functor

Goal state before:
pp: case inr
α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
s : Finset α✝
t : Finset β✝
hs : s.Nonempty
a : β✝
⊢ (a ∈ if s = ∅ then ∅ else t) ↔ a ∈ (image (const α✝ id) s).sup fun f ↦ image f t

Tactic:
rw [if_neg hs.ne_empty, mem_sup]

Goal state after:
case inr
α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
s : Finset α✝
t : Finset β✝
hs : s.Nonempty
a : β✝
⊢ a ∈ t ↔ ∃ i ∈ image (const α✝ id) s, a ∈ image i t
Module: Mathlib.Data.Finset.PImage

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
s : Finset α
f : α → β
inst✝ : (x : α) → Decidable (Part.some (f x)).Dom
⊢ pimage (fun x ↦ Part.some (f x)) s = image f s

Tactic:
ext
  simp [eq_comm]

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

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
⊢ ∀ x ∈ f.graph.toList, ∀ y ∈ f.graph.toList, x.1 = y.1 → x = y

Tactic:
rintro ⟨b, m⟩ hb ⟨c, n⟩ hc (rfl : b = c)
        rw [Finset.mem_toList, Finsupp.mem_graph_iff] at hb hc
        dsimp at hb hc
        rw [← hc.1, hb.1]

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

Goal state before:
pp: α : Type u_1
N : Type u_3
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : Zero N
f g : α →₀ N
⊢ f.neLocus g = g.neLocus f

Tactic:
by
  simp_rw [neLocus, Finset.union_comm, ne_comm]

Goal state after:
Module: Mathlib.Data.Holor

Goal state before:
pp: case refine_2
α : Type
d : ℕ
ds : List ℕ
inst✝ : AddCommMonoid α
β : Type
i : ℕ
hid : i < d
s : Finset β
f : β → Holor α (d :: ds)
this : DecidableEq β := Classical.decEq β
a✝ : β
s✝ : Finset β
h_not_in : a✝ ∉ s✝
⊢ ∑ x ∈ s✝, (f x).slice i hid = (∑ x ∈ s✝, f x).slice i hid →
    ∑ x ∈ insert a✝ s✝, (f x).slice i hid = (∑ x ∈ insert a✝ s✝, f x).slice i hid

Tactic:
ih

Goal state after:
case refine_2
α : Type
d : ℕ
ds : List ℕ
inst✝ : AddCommMonoid α
β : Type
i : ℕ
hid : i < d
s : Finset β
f : β → Holor α (d :: ds)
this : DecidableEq β := Classical.decEq β
a✝ : β
s✝ : Finset β
h_not_in : a✝ ∉ s✝
ih : ∑ x ∈ s✝, (f x).slice i hid = (∑ x ∈ s✝, f x).slice i hid
⊢ ∑ x ∈ insert a✝ s✝, (f x).slice i hid = (∑ x ∈ insert a✝ s✝, f x).slice i hid
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: b : Bool
n : ℤ
⊢ bit b n = 2 * n + bif b then 1 else 0

Tactic:
by
  cases b
  · apply (add_zero _).symm
  · rfl

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
⊢ ((∀ x ∈ s, CPRankMax n (f x)) → CPRankMax (s.card * n) (∑ x ∈ s, f x)) →
    (∀ x_1 ∈ insert x s, CPRankMax n (f x_1)) → CPRankMax ((insert x s).card * n) (∑ x ∈ insert x s, f x)

Tactic:
ih

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)
⊢ (∀ x_1 ∈ insert x s, CPRankMax n (f x_1)) → CPRankMax ((insert x s).card * n) (∑ x ∈ insert x s, f x)
Module: Mathlib.Data.LawfulXor.Basic

Goal state before:
pp: α : Type u_1
inst✝² : XorOp α
inst✝¹ : Zero α
inst✝ : LawfulXor α
a b : α
⊢ a ^^^ b = 0 ↔ a = b

Tactic:
by
  rw [ xor_eq_iff_left_eq, zero_xor]

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

Goal state before:
pp: m : ℤ
n : ℕ
⊢ m <<< ↑n = m <<< n

Tactic:
rw [Int.shiftLeft_eq']
  unfold_projs; cases m <;> simp only [Nat.shiftLeft'_false, natCast_shiftLeft, ofNat_eq_natCast,
    Nat.pow_eq, Int.natCast_pow, Nat.cast_ofNat, mul_def]
  · grind [Int.shiftLeft_eq']
  · simp only [negSucc_eq, ← natCast_add_one, Nat.shiftLeft'_true_eq_mul_pow]
    grind

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

Goal state before:
pp: case cons
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit
head✝ : α
tail : List α
ih : ∀ (arr : Array PUnit), mapIdxMAux' f arr.size tail = mapIdxM.go f tail arr *> pure PUnit.unit
arr : Array PUnit
head : m PUnit
this : (arr.push PUnit.unit).size = arr.size + 1
⊢ (do
      head
      mapIdxMAux' f (arr.push PUnit.unit).size tail) =
    do
    let x ← head
    let x ← mapIdxM.go f tail (arr.push x)
    pure (const (List PUnit) id x PUnit.unit)

Tactic:
ih

Goal state after:
case cons
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit
head✝ : α
tail : List α
ih : ∀ (arr : Array PUnit), mapIdxMAux' f arr.size tail = mapIdxM.go f tail arr *> pure PUnit.unit
arr : Array PUnit
head : m PUnit
this : (arr.push PUnit.unit).size = arr.size + 1
⊢ (do
      head
      mapIdxM.go f tail (arr.push PUnit.unit) *> pure PUnit.unit) =
    do
    let x ← head
    let x ← mapIdxM.go f tail (arr.push x)
    pure (const (List PUnit) id x PUnit.unit)
Module: Mathlib.Data.List.Shortlex

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a b : α
⊢ Shortlex r [a] [b] ↔ r a b

Tactic:
by
  simp only [shortlex_def, length_singleton, lt_self_iff_false, lex_singleton_iff, true_and,
    false_or]

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

Goal state before:
pp: case inr.nil
α : Type u_1
r : α → α → Prop
t₁ t₂ : List α
h : Shortlex r t₁ t₂
h2 : t₁.length = t₂.length ∧ Lex r t₁ t₂
⊢ Shortlex r ([] ++ t₁) ([] ++ t₂)

Tactic:
List.nil_append,

Goal state after:
case inr.nil
α : Type u_1
r : α → α → Prop
t₁ t₂ : List α
h : Shortlex r t₁ t₂
h2 : t₁.length = t₂.length ∧ Lex r t₁ t₂
⊢ Shortlex r t₁ ([] ++ t₂)
Module: Mathlib.Data.List.SplitLengths

Goal state before:
pp: α : Type u_1
head : ℕ
tail : List ℕ
ih : ∀ (l : List α), tail.sum ≤ l.length → map length (tail.splitLengths l) = tail
l : List α
h : head + tail.sum ≤ l.length
⊢ head ≤ l.length ∧ map length (tail.splitLengths (drop head l)) = tail

Tactic:
ih

Goal state after:
α : Type u_1
head : ℕ
tail : List ℕ
ih : ∀ (l : List α), tail.sum ≤ l.length → map length (tail.splitLengths l) = tail
l : List α
h : head + tail.sum ≤ l.length
⊢ head ≤ l.length ∧ tail = tail

case h
α : Type u_1
head : ℕ
tail : List ℕ
ih : ∀ (l : List α), tail.sum ≤ l.length → map length (tail.splitLengths l) = tail
l : List α
h : head + tail.sum ≤ l.length
⊢ tail.sum ≤ (drop head l).length
Module: Mathlib.Data.List.Shortlex

Goal state before:
pp: case intro.intro.inr.rel
α : Type u_1
r : α → α → Prop
a xa : α
h✝¹ : ∀ (y : α), r y xa → Acc r y
iha :
  ∀ (y : α),
    r y xa →
      ∀ {b : List α},
        Acc (Shortlex r) b →
          (∀ (s : List α), s.length < (y :: b).length → Acc (Shortlex r) s) → Acc (Shortlex r) (y :: b)
b xb : List α
h✝ : ∀ (y : List α), Shortlex r y xb → Acc (Shortlex r) y
ihb :
  ∀ (y : List α),
    Shortlex r y xb → (∀ (s : List α), s.length < (xa :: y).length → Acc (Shortlex r) s) → Acc (Shortlex r) (xa :: y)
ih : ∀ (s : List α), s.length < (xa :: xb).length → Acc (Shortlex r) s
x : α
xs : List α
lt : Shortlex r (x :: xs) (xa :: xb)
h : r x xa
h2len : xs.length = xb.length
⊢ Acc (Shortlex r) (x :: xs)

Tactic:
refine iha _ h (ih xs (by rw [h2len]; simp)) fun l hl => ?_

Goal state after:
case intro.intro.inr.rel
α : Type u_1
r : α → α → Prop
a xa : α
h✝¹ : ∀ (y : α), r y xa → Acc r y
iha :
  ∀ (y : α),
    r y xa →
      ∀ {b : List α},
        Acc (Shortlex r) b →
          (∀ (s : List α), s.length < (y :: b).length → Acc (Shortlex r) s) → Acc (Shortlex r) (y :: b)
b xb : List α
h✝ : ∀ (y : List α), Shortlex r y xb → Acc (Shortlex r) y
ihb :
  ∀ (y : List α),
    Shortlex r y xb → (∀ (s : List α), s.length < (xa :: y).length → Acc (Shortlex r) s) → Acc (Shortlex r) (xa :: y)
ih : ∀ (s : List α), s.length < (xa :: xb).length → Acc (Shortlex r) s
x : α
xs : List α
lt : Shortlex r (x :: xs) (xa :: xb)
h : r x xa
h2len : xs.length = xb.length
l : List α
hl : l.length < (x :: xs).length
⊢ Acc (Shortlex r) l