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

Goal state before:
pp: case e_a
fs : Code
as : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v v' : List ℕ
⊢ Reaches step (Cfg.ret (Cont.cons₂ v k) v') ?m.89

pp: case e_a
fs : Code
as : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v v' : List ℕ
⊢ eval step ?m.89 = do
    let a ← k.eval (v.headI :: v')
    pure (Cfg.halt a)

pp: fs : Code
as : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v v' : List ℕ
⊢ Cfg

Tactic:
· exact ReflTransGen.single rfl

Goal state after:
case e_a
fs : Code
as : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v v' : List ℕ
⊢ eval step (stepRet (Cont.cons₂ v k) v') = do
    let a ← k.eval (v.headI :: v')
    pure (Cfg.halt a)
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case e_a
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v v' : List ℕ
⊢ Reaches step (Cfg.ret k v') ?m.167

pp: case e_a
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v v' : List ℕ
⊢ eval step ?m.167 = do
    let a ← k.eval v'
    pure (Cfg.halt a)

pp: f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v v' : List ℕ
⊢ Cfg

Tactic:
· exact ReflTransGen.single rfl

Goal state after:
case e_a
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v v' : List ℕ
⊢ eval step (stepRet k v') = do
    let a ← k.eval v'
    pure (Cfg.halt a)
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 = []
e : splitAtPred p (S k₁) = (L₁, none, L₂)
⊢ update (update S k₁ L₂) k₂ (L₁ ++ S k₂) =
    update (update S k₁ L₂) k₂
      ((update (update S rev (L₁.reverseAux (S rev))) k₁ L₂ rev).reverseAux
        (update (update S rev (L₁.reverseAux (S rev))) k₁ L₂ k₂))

Tactic:
simp only [Function.update_of_ne h₁.2.2.symm, Function.update_of_ne h₁.2.1,
      Function.update_of_ne h₁.1.symm, List.reverseAux_eq, h₂, Function.update_self,
      List.append_nil, List.reverse_reverse]

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

Goal state before:
pp: X : Type u_1
inst✝² : Finite X
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
⊢ ExtremallyDisconnected ↑(CompHaus.of X).toTop

Tactic:
by
    dsimp
    constructor
    intro U _
    apply isOpen_discrete (closure U)

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

Goal state before:
pp: X Y Z : Stonean
f : X ⟶ Z
i : Y ⟶ Z
hi : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
this : ExtremallyDisconnected ↑(⇑(ConcreteCategory.hom i) ⁻¹' Set.range ⇑(ConcreteCategory.hom f))
e : ↑(⇑(ConcreteCategory.hom i) ⁻¹' Set.range ⇑(ConcreteCategory.hom f)) ≃ₜ
  { p // (ConcreteCategory.hom i) p.1 = (ConcreteCategory.hom f) p.2 } :=
  (TopCat.pullbackHomeoPreimage ⇑(ConcreteCategory.hom i) ⋯ ⇑(ConcreteCategory.hom f) ⋯).symm
⊢ ↑{xy | (ConcreteCategory.hom f) xy.1 = (ConcreteCategory.hom i) xy.2} ≃ₜ
    ↑{xy | (ConcreteCategory.hom i) xy.1 = (ConcreteCategory.hom f) xy.2}

Tactic:
by
    exact TopCat.homeoOfIso
      ((TopCat.pullbackIsoProdSubtype f.hom i.hom).symm ≪≫ pullbackSymmetry _ _ ≪≫
        (TopCat.pullbackIsoProdSubtype i.hom f.hom))

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

Goal state before:
pp: case zero'
k : Cont
v : List ℕ
s : Option Γ'
⊢ ∃ b₂,
    TrCfg (stepNormal Code.zero' k v) b₂ ∧
      Reaches₁ (TM2.step tr)
        { l := some (trNormal Code.zero' (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) } b₂

Tactic:
refine ⟨_, ⟨s, rfl⟩, TransGen.single ?_⟩; simp

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

Goal state before:
pp: case cons₂
ns : List ℕ
k : Cont
IH :
  ∀ (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepRet k v) b₂ ∧
        Reaches₁ (TM2.step tr) { l := some (Λ'.ret (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) }
          b₂
v : List ℕ
s : Option Γ'
c : Cfg'
h₁ : TrCfg (stepRet k (ns.headI :: v)) c
h₂ :
  Reaches₁ (TM2.step tr)
    { l := some (Λ'.ret (trCont k)), var := none, stk := elim (trList (ns.headI :: v)) [] [] (trContStack k) } c
⊢ ∃ b₂,
    TrCfg (stepRet (Cont.cons₂ ns k) v) b₂ ∧
      Reaches₁ (TM2.step tr)
        { l := some (Λ'.ret (trCont (Cont.cons₂ ns k))), var := s,
          stk := elim (trList v) [] [] (trContStack (Cont.cons₂ ns k)) }
        b₂

Tactic:
exact ⟨c, h₁, TransGen.head rfl <| head_stack_ok.trans h₂⟩

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

Goal state before:
pp: case move
q' : Λ'
p✝ : Γ' → Bool
k₁✝ k₂✝ : K'
q : Λ'
q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
⊢ q' ∈ trStmts₁ (Λ'.move p✝ k₁✝ k₂✝ q) → trStmts₁ q' ⊆ trStmts₁ (Λ'.move p✝ k₁✝ k₂✝ q)

Tactic:
all_goals
    simp +contextual only [trStmts₁, Finset.mem_insert, Finset.mem_union,
      or_imp, Finset.mem_singleton, Finset.Subset.refl, imp_true_iff, true_and]
    repeat exact fun h => Finset.Subset.trans (q_ih h) (Finset.subset_insert _ _)

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

Goal state before:
pp: case clear
q' : Λ'
p✝ : Γ' → Bool
k✝ : K'
q : Λ'
q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
⊢ q' ∈ trStmts₁ (Λ'.clear p✝ k✝ q) → trStmts₁ q' ⊆ trStmts₁ (Λ'.clear p✝ k✝ q)

Tactic:
all_goals
    simp +contextual only [trStmts₁, Finset.mem_insert, Finset.mem_union,
      or_imp, Finset.mem_singleton, Finset.Subset.refl, imp_true_iff, true_and]
    repeat exact fun h => Finset.Subset.trans (q_ih h) (Finset.subset_insert _ _)

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

Goal state before:
pp: case copy
q' q : Λ'
q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
⊢ q' ∈ trStmts₁ q.copy → trStmts₁ q' ⊆ trStmts₁ q.copy

Tactic:
all_goals
    simp +contextual only [trStmts₁, Finset.mem_insert, Finset.mem_union,
      or_imp, Finset.mem_singleton, Finset.Subset.refl, imp_true_iff, true_and]
    repeat exact fun h => Finset.Subset.trans (q_ih h) (Finset.subset_insert _ _)

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

Goal state before:
pp: case push
q' : Λ'
k✝ : K'
s✝ : Option Γ' → Option Γ'
q : Λ'
q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
⊢ q' ∈ trStmts₁ (Λ'.push k✝ s✝ q) → trStmts₁ q' ⊆ trStmts₁ (Λ'.push k✝ s✝ q)

Tactic:
all_goals
    simp +contextual only [trStmts₁, Finset.mem_insert, Finset.mem_union,
      or_imp, Finset.mem_singleton, Finset.Subset.refl, imp_true_iff, true_and]
    repeat exact fun h => Finset.Subset.trans (q_ih h) (Finset.subset_insert _ _)

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

Goal state before:
pp: case read
q' : Λ'
q : Option Γ' → Λ'
q_ih : ∀ (a : Option Γ'), q' ∈ trStmts₁ (q a) → trStmts₁ q' ⊆ trStmts₁ (q a)
⊢ q' ∈ trStmts₁ (Λ'.read q) → trStmts₁ q' ⊆ trStmts₁ (Λ'.read q)

Tactic:
all_goals
    simp +contextual only [trStmts₁, Finset.mem_insert, Finset.mem_union,
      or_imp, Finset.mem_singleton, Finset.Subset.refl, imp_true_iff, true_and]
    repeat exact fun h => Finset.Subset.trans (q_ih h) (Finset.subset_insert _ _)

Goal state after:
case read
q' : Λ'
q : Option Γ' → Λ'
q_ih : ∀ (a : Option Γ'), q' ∈ trStmts₁ (q a) → trStmts₁ q' ⊆ trStmts₁ (q a)
⊢ (q' ∈ Finset.univ.biUnion fun s ↦ trStmts₁ (q s)) →
    trStmts₁ q' ⊆ insert (Λ'.read q) (Finset.univ.biUnion fun s ↦ trStmts₁ (q s))
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case succ
q' q : Λ'
q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
⊢ q' ∈ trStmts₁ q.succ → trStmts₁ q' ⊆ trStmts₁ q.succ

Tactic:
all_goals
    simp +contextual only [trStmts₁, Finset.mem_insert, Finset.mem_union,
      or_imp, Finset.mem_singleton, Finset.Subset.refl, imp_true_iff, true_and]
    repeat exact fun h => Finset.Subset.trans (q_ih h) (Finset.subset_insert _ _)

Goal state after:
case succ
q' q : Λ'
q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
⊢ (q' = unrev q → trStmts₁ (unrev q) ⊆ insert q.succ (insert (unrev q) (trStmts₁ q))) ∧
    (q' ∈ trStmts₁ q → trStmts₁ q' ⊆ insert q.succ (insert (unrev q) (trStmts₁ q)))
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case pred
q' q₁ q₂ : Λ'
q₁_ih : q' ∈ trStmts₁ q₁ → trStmts₁ q' ⊆ trStmts₁ q₁
q₂_ih : q' ∈ trStmts₁ q₂ → trStmts₁ q' ⊆ trStmts₁ q₂
⊢ q' ∈ trStmts₁ (q₁.pred q₂) → trStmts₁ q' ⊆ trStmts₁ (q₁.pred q₂)

Tactic:
all_goals
    simp +contextual only [trStmts₁, Finset.mem_insert, Finset.mem_union,
      or_imp, Finset.mem_singleton, Finset.Subset.refl, imp_true_iff, true_and]
    repeat exact fun h => Finset.Subset.trans (q_ih h) (Finset.subset_insert _ _)

Goal state after:
case pred
q' q₁ q₂ : Λ'
q₁_ih : q' ∈ trStmts₁ q₁ → trStmts₁ q' ⊆ trStmts₁ q₁
q₂_ih : q' ∈ trStmts₁ q₂ → trStmts₁ q' ⊆ trStmts₁ q₂
⊢ (q' ∈ trStmts₁ q₁ → trStmts₁ q' ⊆ insert (q₁.pred q₂) (trStmts₁ q₁ ∪ insert (unrev q₂) (trStmts₁ q₂))) ∧
    (q' = unrev q₂ → trStmts₁ (unrev q₂) ⊆ insert (q₁.pred q₂) (trStmts₁ q₁ ∪ insert (unrev q₂) (trStmts₁ q₂))) ∧
      (q' ∈ trStmts₁ q₂ → trStmts₁ q' ⊆ insert (q₁.pred q₂) (trStmts₁ q₁ ∪ insert (unrev q₂) (trStmts₁ q₂)))
Module: Mathlib.Computability.TuringMachine.ToPartrec

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

Tactic:
all_goals
    simp +contextual only [trStmts₁, Finset.mem_insert, Finset.mem_union,
      or_imp, Finset.mem_singleton, Finset.Subset.refl, imp_true_iff, true_and]
    repeat exact fun h => Finset.Subset.trans (q_ih h) (Finset.subset_insert _ _)

Goal state after:
Module: Mathlib.Condensed.TopComparison

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
G : C ⥤ TopCat
X : Type w'
inst✝¹ : TopologicalSpace X
inst✝ : ∀ (Z B : C) (π : Z ⟶ B) [EffectiveEpi π], PreservesLimit (cospan π π) G
hq : ∀ (Z B : C) (π : Z ⟶ B) [EffectiveEpi π], IsQuotientMap ⇑(ConcreteCategory.hom (G.map π))
⊢ ∀ (X_1 B : C) (π : X_1 ⟶ B) [EffectiveEpi π] [inst : HasPullback π π],
    Function.Bijective
      ⇑(ConcreteCategory.hom (mapToEqualizer (yonedaPresheaf G X) π (pullback.fst π π) (pullback.snd π π) ⋯))

Tactic:
intro Z B π _ _

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
G : C ⥤ TopCat
X : Type w'
inst✝³ : TopologicalSpace X
inst✝² : ∀ (Z B : C) (π : Z ⟶ B) [EffectiveEpi π], PreservesLimit (cospan π π) G
hq : ∀ (Z B : C) (π : Z ⟶ B) [EffectiveEpi π], IsQuotientMap ⇑(ConcreteCategory.hom (G.map π))
Z B : C
π : Z ⟶ B
inst✝¹ : EffectiveEpi π
inst✝ : HasPullback π π
⊢ Function.Bijective
    ⇑(ConcreteCategory.hom (mapToEqualizer (yonedaPresheaf G X) π (pullback.fst π π) (pullback.snd π π) ⋯))
Module: Mathlib.Condensed.EffectiveEpi

Goal state before:
pp: X✝ Y✝ : CompHaus
f : X✝ ⟶ Y✝
hf : Epi f
⊢ Epi (compHausToCondensed.map f)

Tactic:
rw [CondensedSet.epi_iff_locallySurjective_on_compHaus]

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

Goal state before:
pp: X Y : LightCondSet
f : X ⟶ Y
S : LightProfinite
x : X.obj.obj (Opposite.op S)
⊢ Continuous fun a ↦
    (⇑(ConcreteCategory.hom (f.hom.app (Opposite.op (of PUnit.{u + 1})))) ∘ LightCondSet.coinducingCoprod✝ X)
      ⟨⟨S, x⟩, a⟩

Tactic:
simp only [Function.comp_apply, coinducingCoprod]

Goal state after:
X Y : LightCondSet
f : X ⟶ Y
S : LightProfinite
x : X.obj.obj (Opposite.op S)
⊢ Continuous fun a ↦
    (ConcreteCategory.hom (f.hom.app (Opposite.op (of PUnit.{u + 1}))))
      ((ConcreteCategory.hom (X.obj.map (CompHausLike.const (of PUnit.{u + 1}) a).op)) x)
Module: Mathlib.Condensed.Light.TopCatAdjunction

Goal state before:
pp: X✝ Y : LightCondSet
f : X✝ ⟶ Y
X : TopCat
⊢ Epi (topCatAdjunction.counit.app X)

Tactic:
rw [TopCat.epi_iff_surjective]

Goal state after:
X✝ Y : LightCondSet
f : X✝ ⟶ Y
X : TopCat
⊢ Function.Surjective ⇑(ConcreteCategory.hom (topCatAdjunction.counit.app X))
Module: Mathlib.Condensed.TopCatAdjunction

Goal state before:
pp: X Y : CondensedSet
f : X ⟶ Y
S : CompHaus
x : X.obj.obj (Opposite.op S)
⊢ Continuous fun a ↦
    (⇑(ConcreteCategory.hom (f.hom.app (Opposite.op (of PUnit.{u + 1})))) ∘ CondensedSet.coinducingCoprod✝ X)
      ⟨⟨S, x⟩, a⟩

Tactic:
simp only [Function.comp_apply, coinducingCoprod]

Goal state after:
X Y : CondensedSet
f : X ⟶ Y
S : CompHaus
x : X.obj.obj (Opposite.op S)
⊢ Continuous fun a ↦
    (ConcreteCategory.hom (f.hom.app (Opposite.op (of PUnit.{u + 1}))))
      ((ConcreteCategory.hom (X.obj.map (CompHausLike.const (of PUnit.{u + 1}) a).op)) x)
Module: Mathlib.Condensed.TopCatAdjunction

Goal state before:
pp: X✝ : CondensedSet
X : TopCat
⊢ Epi (topCatAdjunction.counit.app X)

Tactic:
rw [TopCat.epi_iff_surjective]

Goal state after:
X✝ : CondensedSet
X : TopCat
⊢ Function.Surjective ⇑(ConcreteCategory.hom (topCatAdjunction.counit.app X))
Module: Mathlib.Control.Traversable.Lemmas

Goal state before:
pp: t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
α : Type u
x : t α
this : traverse pure x = pure (traverse pure x)
⊢ traverse pure x = pure x

Tactic:
id_traverse

Goal state after:
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
α : Type u
x : t α
this : traverse pure x = pure (pure x)
⊢ traverse pure x = pure x
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: α : Type u_1
β : α → Type u_2
g : ((a : α) → Part (β a)) → (a : α) → Part (β a)
hc : ωScottContinuous g
⊢ Part.fix g = g (Part.fix g)

Tactic:
by
  rw [fix_eq_ωSup_of_ωScottContinuous hc, hc.map_ωSup]
  apply le_antisymm
  · apply ωSup_le_ωSup_of_le _
    intro i
    exists i
    apply le_f_of_mem_approx _ ⟨i, rfl⟩
  · apply ωSup_le_ωSup_of_le _
    intro i
    exists i.succ

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

Goal state before:
pp: α : 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 : σ✝¹
t : σ✝
h : F✝¹.f s ∩ F✝.f t ⊆ s✝
⊢ F✝.f t ∈ { sets := {a | ∃ b, F✝.f b ⊆ a}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }

Tactic:
· use t

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

Goal state before:
pp: α : 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
⊢ i = j

Tactic:
by_cases hi : i = 0

Goal state after:
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
⊢ i = j

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
⊢ i = j
Module: Mathlib.Data.Fin.Tuple.Embedding

Goal state before:
pp: α : Type u_1
e : Fin 2 ↪ α
i : Fin 2
⊢ ((fun x ↦
          match x with
          | ⟨(a, b), h⟩ => { toFun := fun i ↦ if i = 0 then a else b, inj' := ⋯ })
        ((fun e ↦ ⟨(e 0, e 1), ⋯⟩) e))
      i =
    e i

Tactic:
by_cases hi : i = 0

Goal state after:
case pos
α : Type u_1
e : Fin 2 ↪ α
i : Fin 2
hi : i = 0
⊢ ((fun x ↦
          match x with
          | ⟨(a, b), h⟩ => { toFun := fun i ↦ if i = 0 then a else b, inj' := ⋯ })
        ((fun e ↦ ⟨(e 0, e 1), ⋯⟩) e))
      i =
    e i

case neg
α : Type u_1
e : Fin 2 ↪ α
i : Fin 2
hi : ¬i = 0
⊢ ((fun x ↦
          match x with
          | ⟨(a, b), h⟩ => { toFun := fun i ↦ if i = 0 then a else b, inj' := ⋯ })
        ((fun e ↦ ⟨(e 0, e 1), ⋯⟩) e))
      i =
    e i
Module: Mathlib.Data.Fin.Tuple.Take

Goal state before:
pp: case pos
n n' : ℕ
motive : Fin (n + n') → Sort u_2
m : ℕ
h : m ≤ n'
u : (i : Fin n) → motive (castAdd n' i)
v : (i : Fin n') → motive (natAdd n i)
i : Fin (n + m)
h' : ↑i < n
⊢ (if h_1 : ↑i < n then u ((castLE ⋯ i).castLT ⋯) else ⋯ ▸ v (subNat n (Fin.cast ⋯ (castLE ⋯ i)) ⋯)) =
    if h : ↑i < n then u (i.castLT ⋯) else ⋯ ▸ v (castLE h (subNat n (Fin.cast ⋯ i) ⋯))

Tactic:
simp only [h', ↓reduceDIte]

Goal state after:
case pos
n n' : ℕ
motive : Fin (n + n') → Sort u_2
m : ℕ
h : m ≤ n'
u : (i : Fin n) → motive (castAdd n' i)
v : (i : Fin n') → motive (natAdd n i)
i : Fin (n + m)
h' : ↑i < n
⊢ u ((castLE ⋯ i).castLT ⋯) = u (i.castLT ⋯)
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type u_1
β' : α → Type u_2
f : (a : α) → β a → β' a
l : List ((a : α) × β a)
⊢ (map (Sigma.map id f) l).keys = l.keys

Tactic:
by
  induction l <;> grind [Sigma.map]

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : Sigma β
l : List (Sigma β)
h : a = s.fst
⊢ kerase a (s :: l) = l

Tactic:
by simp [kerase, h]

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : Sigma β
l : List (Sigma β)
h : a ≠ s.fst
⊢ kerase a (s :: l) = s :: kerase a l

Tactic:
by simp [kerase, h]

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

Goal state before:
pp: case cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
h : a ≠ a'
hd : Sigma β
tl : List (Sigma β)
ih : dlookup a (kerase a' tl) = dlookup a tl
⊢ dlookup a (kerase a' (hd :: tl)) = dlookup a (hd :: tl)

Tactic:
obtain ⟨ah, bh⟩ := hd

Goal state after:
case cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
h : a ≠ a'
tl : List (Sigma β)
ih : dlookup a (kerase a' tl) = dlookup a tl
ah : α
bh : β ah
⊢ dlookup a (kerase a' (⟨ah, bh⟩ :: tl)) = dlookup a (⟨ah, bh⟩ :: tl)
Module: Mathlib.Data.Finset.Lattice.Pi

Goal state before:
pp: case insert.refine_1
α : Type u_1
ι : Type u_2
inst✝² : DistribLattice α
inst✝¹ : BoundedOrder α
inst✝ : DecidableEq ι
κ : ι → Type u_3
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → α
i : ι
s : Finset ι
hi : i ∉ s
ih : (s.inf fun i ↦ (t i).sup (f i)) = (s.pi t).sup fun g ↦ s.attach.inf fun i ↦ f (↑i) (g ↑i ⋯)
c : α
h :
  ∀ (b : (a : ι) → a ∈ insert i s → κ a),
    (∀ (a : ι) (h : a ∈ insert i s), b a h ∈ t a) →
      f i (b i ⋯) ⊓ s.attach.inf ((fun i_1 ↦ f (↑i_1) (b ↑i_1 ⋯)) ∘ fun x ↦ ⟨↑x, ⋯⟩) ≤ c
a : κ i
g : (a : ι) → a ∈ s → κ a
ha : a ∈ t i
hg : ∀ (a : ι) (h : a ∈ s), g a h ∈ t a
aux : ∀ (j : ↥s), ↑j ≠ i
j : ι
hj : j ∈ insert i s
⊢ (if hji : j = i then cast ⋯ a else g j ⋯) ∈ t j

Tactic:
mem_insert

Goal state after:
case insert.refine_1
α : Type u_1
ι : Type u_2
inst✝² : DistribLattice α
inst✝¹ : BoundedOrder α
inst✝ : DecidableEq ι
κ : ι → Type u_3
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → α
i : ι
s : Finset ι
hi : i ∉ s
ih : (s.inf fun i ↦ (t i).sup (f i)) = (s.pi t).sup fun g ↦ s.attach.inf fun i ↦ f (↑i) (g ↑i ⋯)
c : α
h :
  ∀ (b : (a : ι) → a ∈ insert i s → κ a),
    (∀ (a : ι) (h : a ∈ insert i s), b a h ∈ t a) →
      f i (b i ⋯) ⊓ s.attach.inf ((fun i_1 ↦ f (↑i_1) (b ↑i_1 ⋯)) ∘ fun x ↦ ⟨↑x, ⋯⟩) ≤ c
a : κ i
g : (a : ι) → a ∈ s → κ a
ha : a ∈ t i
hg : ∀ (a : ι) (h : a ∈ s), g a h ∈ t a
aux : ∀ (j : ↥s), ↑j ≠ i
j : ι
hj✝ : j ∈ insert i s
hj : j = i ∨ j ∈ s
⊢ (if hji : j = i then cast ⋯ a else g j ⋯) ∈ t j
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
l : List (Sigma β)
l' : List (Sigma β)
hl : [] = l'
⊢ [].NodupKeys

Tactic:
apply nodup_nil

Goal state after:
Module: Mathlib.Data.Holor

Goal state before:
pp: case h₀
α : Type
d : ℕ
ds : List ℕ
inst✝ : Semiring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
b : ↥(Finset.range d)
a✝ : b ∈ (Finset.range d).attach
hbi : b ≠ ⟨i, ⋯⟩
⊢ (if i = ↑b then x.slice ↑b ⋯ else 0) = 0

Tactic:
have hbi' : i ≠ b := by simpa only [Ne, Subtype.ext_iff, Subtype.coe_mk] using hbi.symm

Goal state after:
case h₀
α : Type
d : ℕ
ds : List ℕ
inst✝ : Semiring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
b : ↥(Finset.range d)
a✝ : b ∈ (Finset.range d).attach
hbi : b ≠ ⟨i, ⋯⟩
hbi' : i ≠ ↑b
⊢ (if i = ↑b then x.slice ↑b ⋯ else 0) = 0
Module: Mathlib.Data.Int.Order.Lemmas

Goal state before:
pp: a b : ℤ
⊢ a.natAbs < b.natAbs ↔ a * a < b * b

Tactic:
← abs_lt_iff_mul_self_lt,

Goal state after:
a b : ℤ
⊢ a.natAbs < b.natAbs ↔ |a| < |b|
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case ofNat.negSucc.e_f.false
m n : ℕ
y : Bool
⊢ (!(y || !false)) = (false && !y)

Tactic:
cases y

Goal state after:
case ofNat.negSucc.e_f.false.false
m n : ℕ
⊢ (!(false || !false)) = (false && !false)

case ofNat.negSucc.e_f.false.true
m n : ℕ
⊢ (!(true || !false)) = (false && !true)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case ofNat.negSucc.e_f.true
m n : ℕ
y : Bool
⊢ (!(y || !true)) = (true && !y)

Tactic:
cases y

Goal state after:
case ofNat.negSucc.e_f.true.false
m n : ℕ
⊢ (!(false || !true)) = (true && !false)

case ofNat.negSucc.e_f.true.true
m n : ℕ
⊢ (!(true || !true)) = (true && !true)
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 β
⊢ ∀ (a : β) (s : Finset β),
    a ∉ s →
      ((∀ x ∈ s, CPRankMax n (f x)) → CPRankMax (s.card * n) (∑ x ∈ s, f x)) →
        (∀ x ∈ insert a s, CPRankMax n (f x)) → CPRankMax ((insert a s).card * n) (∑ x ∈ insert a s, f x)

Tactic:
intro x s (h_x_notin_s : x ∉ s) ih h_cprank
      simp only [Finset.sum_insert h_x_notin_s, Finset.card_insert_of_notMem h_x_notin_s]
      rw [Nat.right_distrib]
      simp only [Nat.one_mul, Nat.add_comm]
      have ih' : CPRankMax (Finset.card s * n) (∑ x ∈ s, f x) := by grind
      exact cprankMax_add (h_cprank x (Finset.mem_insert_self x s)) ih'

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

Goal state before:
pp: case negSucc.ofNat.e_f.false
m n : ℕ
y : Bool
⊢ (!y && false) = (false && !y)

Tactic:
cases y

Goal state after:
case negSucc.ofNat.e_f.false.false
m n : ℕ
⊢ (!false && false) = (false && !false)

case negSucc.ofNat.e_f.false.true
m n : ℕ
⊢ (!true && false) = (false && !true)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case negSucc.ofNat.e_f.true
m n : ℕ
y : Bool
⊢ (!y && true) = (true && !y)

Tactic:
cases y

Goal state after:
case negSucc.ofNat.e_f.true.false
m n : ℕ
⊢ (!false && true) = (true && !false)

case negSucc.ofNat.e_f.true.true
m n : ℕ
⊢ (!true && true) = (true && !true)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case negSucc.negSucc.e_f.false
m n : ℕ
y : Bool
⊢ (!y && !!false) = (false && !y)

Tactic:
cases y

Goal state after:
case negSucc.negSucc.e_f.false.false
m n : ℕ
⊢ (!false && !!false) = (false && !false)

case negSucc.negSucc.e_f.false.true
m n : ℕ
⊢ (!true && !!false) = (false && !true)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case negSucc.negSucc.e_f.true
m n : ℕ
y : Bool
⊢ (!y && !!true) = (true && !y)

Tactic:
cases y

Goal state after:
case negSucc.negSucc.e_f.true.false
m n : ℕ
⊢ (!false && !!true) = (true && !false)

case negSucc.negSucc.e_f.true.true
m n : ℕ
⊢ (!true && !!true) = (true && !true)
Module: Mathlib.Data.Int.NatPrime

Goal state before:
pp: p : ℕ
p_prime : Nat.Prime p
m n : ℤ
k l : ℕ
hpm : ↑(p ^ k) ∣ m
hpn : ↑(p ^ l) ∣ n
hpmn : ↑(p ^ (k + l + 1)) ∣ m * n
hpm' : p ^ k ∣ m.natAbs
hpn' : p ^ l ∣ n.natAbs
hpmn' : p ^ (k + l + 1) ∣ m.natAbs * n.natAbs
hsd : p ^ (k + 1) ∣ m.natAbs ∨ p ^ (l + 1) ∣ n.natAbs :=
  Nat.succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul p_prime hpm' hpn' hpmn'
hsd2 : p ^ (l + 1) ∣ n.natAbs
⊢ ↑(p ^ (l + 1)) ∣ n

Tactic:
by apply Int.dvd_natAbs.1; apply Int.natCast_dvd_natCast.2 hsd2

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

Goal state before:
pp: case mpr
a b r v : ℕ
x : ℤ
⊢ (↑a ≤ x ∧ x < ↑b) ∧ x ≡ ↑v [ZMOD ↑r] → ∃ a_2, ((a ≤ a_2 ∧ a_2 < b) ∧ a_2 ≡ v [MOD r]) ∧ ↑a_2 = x

Tactic:
intro h; lift x to ℕ using (by omega); exact ⟨x, by simp_all [natCast_modEq_iff]⟩

Goal state after: