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) }
⊢ { l := some (ret q), var := v, Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L)) } ∈
    TM1.step (tr M) { l := some (ret q), var := v, Tape := (Tape.move Dir.right)^[n + 1] (Tape.mk' ∅ (addBottom L)) }

Tactic:
simp only [Option.mem_def, TM1.step]

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) }
⊢ some (TM1.stepAux (tr M (ret q)) v ((Tape.move Dir.right)^[n + 1] (Tape.mk' ∅ (addBottom L)))) =
    some { l := some (ret q), var := v, Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L)) }
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 : σ
L : ListBlank ((k : K) → Option (Γ k))
n : ℕ
⊢ 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) }

Tactic:
induction n with

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

Goal state before:
pp: f : Code
k : Cont
v : List ℕ
fok : f.Ok
x : Cfg
this :
  ∀ (c : Cfg),
    x ∈ eval step c →
      ∀ (v : List ℕ) (c' : Cfg),
        c = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
h : x ∈ eval step (stepNormal f (Cont.fix f k) v)
v₁ : List ℕ
hv₁ : v₁ ∈ f.eval v
v₂ : List ℕ
hv₂ : v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail
h₃ : x ∈ eval step (Cfg.ret k v₂)
⊢ ∃ a ∈ f.fix.eval v, x ∈ eval step (Cfg.ret k a)

Tactic:
refine ⟨v₂, PFun.mem_fix_iff.2 ?_, h₃⟩

Goal state after:
f : Code
k : Cont
v : List ℕ
fok : f.Ok
x : Cfg
this :
  ∀ (c : Cfg),
    x ∈ eval step c →
      ∀ (v : List ℕ) (c' : Cfg),
        c = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
h : x ∈ eval step (stepNormal f (Cont.fix f k) v)
v₁ : List ℕ
hv₁ : v₁ ∈ f.eval v
v₂ : List ℕ
hv₂ : v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail
h₃ : x ∈ eval step (Cfg.ret k v₂)
⊢ Sum.inl v₂ ∈ Part.map (fun v ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v) ∨
    ∃ a',
      Sum.inr a' ∈ Part.map (fun v ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v) ∧
        v₂ ∈ PFun.fix (fun v ↦ Part.map (fun v ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v)) a'
Module: Mathlib.Topology.Category.CompHaus.EffectiveEpi

Goal state before:
pp: α : Type
inst✝ : Finite α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
tfae_2_to_1 : Epi (Sigma.desc π) → EffectiveEpiFamily X π
tfae_1_to_2 : EffectiveEpiFamily X π → Epi (Sigma.desc π)
tfae_3_to_2 : (∀ (b : ↑B.toTop), ∃ a x, (ConcreteCategory.hom (π a)) x = b) → Epi (Sigma.desc π)
x✝ : Epi (Sigma.desc π)
e : Function.Surjective ⇑(ConcreteCategory.hom (Sigma.desc π))
i : ∐ X ≅ finiteCoproduct X :=
  (colimit.isColimit (Discrete.functor X)).coconePointUniqueUpToIso (finiteCoproduct.isColimit X)
t : ↑(∐ X).toTop
q : (fun X ↦ ↑X.toTop) (finiteCoproduct X) := (ConcreteCategory.hom i.hom) t
⊢ ∃ a x, (ConcreteCategory.hom (π a)) x = (ConcreteCategory.hom (Sigma.desc π)) t

Tactic:
refine ⟨q.1,q.2,?_⟩

Goal state after:
α : Type
inst✝ : Finite α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
tfae_2_to_1 : Epi (Sigma.desc π) → EffectiveEpiFamily X π
tfae_1_to_2 : EffectiveEpiFamily X π → Epi (Sigma.desc π)
tfae_3_to_2 : (∀ (b : ↑B.toTop), ∃ a x, (ConcreteCategory.hom (π a)) x = b) → Epi (Sigma.desc π)
x✝ : Epi (Sigma.desc π)
e : Function.Surjective ⇑(ConcreteCategory.hom (Sigma.desc π))
i : ∐ X ≅ finiteCoproduct X :=
  (colimit.isColimit (Discrete.functor X)).coconePointUniqueUpToIso (finiteCoproduct.isColimit X)
t : ↑(∐ X).toTop
q : (fun X ↦ ↑X.toTop) (finiteCoproduct X) := (ConcreteCategory.hom i.hom) t
⊢ (ConcreteCategory.hom (π q.fst)) q.snd = (ConcreteCategory.hom (Sigma.desc π)) t
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: 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 ⊆ S, IsChain (fun x1 x2 ↦ x1 ⊆ x2) C → ∃ s ∈ S, ∀ c ∈ C, s ⊆ c

Tactic:
intro C

Goal state after:
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 ⊆ S → IsChain (fun x1 x2 ↦ x1 ⊆ x2) C → ∃ s ∈ S, ∀ c ∈ C, s ⊆ c
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: case pos
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:
refine eq_univ_of_forall fun a => inter_nonempty_iff_exists_left.mp ?_

Goal state after:
case pos
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
a : A
⊢ ((⋂ c, ↑c) ∩ fun a_1 ↦ X a_1 = a).Nonempty
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case cons
q : Λ'
c : List Γ'
x : Γ'
b : List Γ'
IH :
  ∀ (s : Option Γ') (a d : List Γ'),
    Reaches₁ (TM2.step tr) { l := some q.copy, var := s, stk := elim a b c d }
      { l := some q, var := none, stk := elim (b.reverseAux a) [] c (b.reverseAux d) }
s : Option Γ'
a d : List Γ'
⊢ Reaches₁ (TM2.step tr) { l := some q.copy, var := s, stk := elim a (x :: b) c d }
    { l := some q, var := none, stk := elim ((x :: b).reverseAux a) [] c ((x :: b).reverseAux d) }

Tactic:
| cons x b IH =>

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

Goal state before:
pp: case nil
q : Λ'
s : Option Γ'
L₁ : List ℕ
L₃ : List Γ'
⊢ Reaches₁ (TM2.step tr)
    { l := some (head stack q), var := s, stk := elim (trList L₁) [] [] (trList [] ++ Γ'.consₗ :: L₃) }
    { l := some q, var := none, stk := elim (trList ([].headI :: L₁)) [] [] L₃ }

Tactic:
refine
      TransGen.trans
        (move_ok (by decide)
          (splitAtPred_eq _ _ [] (some Γ'.consₗ) L₃ (by rintro _ ⟨⟩) ⟨rfl, rfl⟩))
        (TransGen.head rfl (TransGen.head rfl ?_))

Goal state after:
case nil
q : Λ'
s : Option Γ'
L₁ : List ℕ
L₃ : List Γ'
⊢ TransGen (fun a b ↦ b ∈ TM2.step tr a)
    (TM2.stepAux
      (tr
        ((fun x ↦
            Λ'.read fun s ↦
              (if s = some Γ'.consₗ then id else Λ'.clear (fun x ↦ decide (x = Γ'.consₗ)) stack) (unrev q))
          (some Γ'.consₗ)))
      (some Γ'.consₗ)
      (update
        (update (update (elim (trList L₁) [] [] (trList [] ++ Γ'.consₗ :: L₃)) stack L₃) rev
          ([].reverseAux (elim (trList L₁) [] [] (trList [] ++ Γ'.consₗ :: L₃) rev)))
        rev
        ((fun s ↦ ((fun x ↦ some Γ'.cons) s).getD default) (some Γ'.consₗ) ::
          update (update (elim (trList L₁) [] [] (trList [] ++ Γ'.consₗ :: L₃)) stack L₃) rev
            ([].reverseAux (elim (trList L₁) [] [] (trList [] ++ Γ'.consₗ :: L₃) rev)) rev)))
    { l := some q, var := none, stk := elim (trList ([].headI :: L₁)) [] [] L₃ }
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:
| succ q q_ih =>

Goal state after:
case succ
q' q : Λ'
q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
⊢ q' ∈ trStmts₁ q.succ → trStmts₁ q' ⊆ trStmts₁ q.succ
Module: Mathlib.Topology.Category.Profinite.CofilteredLimit

Goal state before:
pp: case refine_3.refine_2.mpr
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
x : ↑C.pt.toTop
s : ↑S
hs : s ∈ G
hx :
  x ∈
    ⇑(ConcreteCategory.hom (C.π.app j0)) ⁻¹'
      if h : s ∈ G then ⇑(ConcreteCategory.hom (F.map (f s ⋯))) ⁻¹' V s else Set.univ
⊢ x ∈ ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s

Tactic:
rwa [dif_pos hs, ← Set.preimage_comp, ← CompHausLike.coe_comp, C.w] at hx

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

Goal state before:
pp: case succ
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
q : Λ'
q_ih : Λ'.Supports S q → trStmts₁ q ⊆ S → Supports (trStmts₁ q) S
H₁ : Λ'.Supports S q.succ
HS₁ : trStmts₁ q.succ ⊆ S
⊢ Supports (trStmts₁ q.succ) S

Tactic:
| succ q q_ih =>

Goal state after:
case succ
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
q : Λ'
q_ih : Λ'.Supports S q → trStmts₁ q ⊆ S → Supports (trStmts₁ q) S
H₁ : Λ'.Supports S q.succ
HS₁ : trStmts₁ q.succ ⊆ S
⊢ Supports (trStmts₁ q.succ) S
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case pred.refine_1
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
q₁ q₂ : Λ'
q₁_ih : Λ'.Supports S q₁ → trStmts₁ q₁ ⊆ S → Supports (trStmts₁ q₁) S
q₂_ih : Λ'.Supports S q₂ → trStmts₁ q₂ ⊆ S → Supports (trStmts₁ q₂) S
H₁ : Λ'.Supports S (q₁.pred q₂)
HS₁ : insert (q₁.pred q₂) (insert (unrev q₂) (trStmts₁ q₁ ∪ trStmts₁ q₂)) ⊆ S
h₁ : q₁.pred q₂ ∈ S
h₂ : unrev q₂ ∈ S ∧ ∀ (a : Λ'), a ∈ trStmts₁ q₁ ∨ a ∈ trStmts₁ q₂ → a ∈ S
⊢ Supports (trStmts₁ q₁) S

Tactic:
exact q₁_ih H₁.1 fun _ h => h₂.2 _ (Or.inl h)

Goal state after:
Module: Mathlib.Condensed.TopCatAdjunction

Goal state before:
pp: X✝ : CondensedSet
X : TopCat
inst✝ : UCompactlyGeneratedSpace ↑X
⊢ Continuous (topCatAdjunctionCounitEquiv X).invFun

Tactic:
by
    apply continuous_from_uCompactlyGeneratedSpace
    exact fun _ _ ↦ continuous_coinducingCoprod X.toCondensedSet _

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

Goal state before:
pp: n : ℕ
i : Fin2 n
⊢ i.rev.rev = i

Tactic:
by
  induction i <;> simp_all [rev]

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

Goal state before:
pp: n : ℕ
i : Fin2 n
⊢ ofFin i.toFin = i

Tactic:
by
  induction i with
  | fz => rfl
  | fs _ ih => exact congrArg fs ih

Goal state after:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: case a
α : Type u_1
β : α → Type u_2
g : ((a : α) → Part (β a)) → (a : α) → Part (β a)
hc : ωScottContinuous g
⊢ ωSup ((approxChain { toFun := g, monotone' := ⋯ }).map { toFun := g, monotone' := ⋯ }) ≤
    ωSup (approxChain { toFun := g, monotone' := ⋯ })

Tactic:
· apply ωSup_le_ωSup_of_le _
    intro i
    exists i.succ

Goal state after:
Module: Mathlib.Data.BitVec

Goal state before:
pp: w : ℕ
x : BitVec w
n : ℕ
⊢ (x ^ n).toFin = x.toFin ^ n

Tactic:
induction n with

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
x : α
s : Set α
⊢ s ∈ 𝓝 x ↔ s ∈ 𝓝 x

Tactic:
rw [mem_nhds_toTopsp, H]

Goal state after:
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 : σ✝¹
t : σ✝
h : F✝¹.f s ∩ F✝.f t ⊆ s✝
⊢ 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 := ⋯ }

Tactic:
apply mem_inf_of_inter _ _ h

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

α : 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 := ⋯ }
Module: Mathlib.Data.DFinsupp.Interval

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → DecidableEq (α i)
inst✝² : (i : ι) → PartialOrder (α i)
inst✝¹ : (i : ι) → Zero (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
f g x : Π₀ (i : ι), α i
⊢ (∀ (i : ι), f i ≤ x i ∧ x i ≤ g i) ↔ f ≤ x ∧ x ≤ g

Tactic:
forall_and

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → DecidableEq (α i)
inst✝² : (i : ι) → PartialOrder (α i)
inst✝¹ : (i : ι) → Zero (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
f g x : Π₀ (i : ι), α i
⊢ ((∀ (x_1 : ι), f x_1 ≤ x x_1) ∧ ∀ (x_1 : ι), x x_1 ≤ g x_1) ↔ f ≤ x ∧ x ≤ g
Module: Mathlib.Data.Semiquot

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

Tactic:
mem_pure

Goal state after:
α : Type u_1
a b : α
ab : b = a
c : α
ac : c = a
⊢ b = c
Module: Mathlib.Data.Fin.Tuple.Curry

Goal state before:
pp: n : ℕ
p : Fin n → Type u
τ : Type u
f : FromTypes p τ
⊢ curry f.uncurry = f

Tactic:
induction n with

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

Goal state before:
pp: n : ℕ
p : Fin n → Type u
τ : Type u
f : ((i : Fin n) → p i) → τ
args : (i : Fin n) → p i
⊢ (curry f).uncurry args = f args

Tactic:
induction n with

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

Goal state before:
pp: α : Type u_1
f : α → Option α
l : List α
⊢ (lookmap f l).length = l.length

Tactic:
← length_map,

Goal state after:
α : Type u_1
f : α → Option α
l : List α
⊢ (map ?m.9 (lookmap f l)).length = l.length

α : Type u_1
f : α → Option α
l : List α
⊢ α → ?m.7

α : Type u_1
f : α → Option α
l : List α
⊢ Type ?u.14
Module: Mathlib.Data.Multiset.Functor

Goal state before:
pp: case swap
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
x y : α'
l : List α'
⊢ ofList <$> Traversable.traverse f (y :: x :: l) = ofList <$> Traversable.traverse f (x :: y :: l)

Tactic:
have :
      (fun a b (l : List β') ↦ (↑(a :: b :: l) : Multiset β')) <$> f y <*> f x =
        (fun a b l ↦ ↑(a :: b :: l)) <$> f x <*> f y := by
      rw [CommApplicative.commutative_map]
      congr 2
      funext a b l
      simpa [flip] using! Perm.swap a b l
    simp [Function.comp_def, this, functor_norm]

Goal state after:
Module: Mathlib.Data.Finmap

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

Tactic:
mem_erase,

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : Finmap β
⊢ ¬(a ≠ a ∧ a ∈ s)
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
x y z : Finmap β
⊢ x.Disjoint y ∧ z.Disjoint x ↔ x.Disjoint y ∧ x.Disjoint z

Tactic:
Disjoint.symm_iff _ x

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
x y z : Finmap β
⊢ x.Disjoint y ∧ x.Disjoint z ↔ x.Disjoint y ∧ x.Disjoint z
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case pos.refl.refl
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l₁ l₂ : List (Sigma β)
nd : l₁.NodupKeys
x y : Sigma β
h : x.fst ≠ y.fst
h_2 : a = x.fst
h_1 : a = y.fst
⊢ x = y ∧ ⟨a, b⟩ = ⟨a, b⟩

Tactic:
exact (h (h_2.symm.trans h_1)).elim

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
    by_cases h₁ : a = ah <;> by_cases h₂ : a' = ah
    · subst h₁ h₂
      cases Ne.irrefl h
    · subst h₁
      simp [h₂]
    · subst h₂
      simp [h]
    · simp [h₁, h₂, ih]

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

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
b : α
m : M
hb : f b = m ∧ ¬m = 0
n : M
hc : f b = n ∧ ¬n = 0
⊢ (b, m) = (b, n)

Tactic:
rw [← hc.1, hb.1]

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

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddZeroClass M
l : List (ι →₀ M)
⊢ l.sum.support ⊆ foldr (fun x1 x2 ↦ x1.support ⊔ x2) ∅ l

Tactic:
induction l with
  | nil => simp
  | cons hd tl IH =>
    simp only [List.sum_cons]
    exact Finsupp.support_add.trans (Finset.union_subset_union Finset.Subset.rfl IH)

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

Goal state before:
pp: m n : ℤ
⊢ (m + n).bodd = (m.bodd ^^ n.bodd)

Tactic:
rcases m with m | m

Goal state after:
case ofNat
n : ℤ
m : ℕ
⊢ (ofNat m + n).bodd = ((ofNat m).bodd ^^ n.bodd)

case negSucc
n : ℤ
m : ℕ
⊢ (-[m+1] + n).bodd = (-[m+1].bodd ^^ n.bodd)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: m n : ℤ
⊢ (m * n).bodd = (m.bodd && n.bodd)

Tactic:
rcases m with m | m

Goal state after:
case ofNat
n : ℤ
m : ℕ
⊢ (ofNat m * n).bodd = ((ofNat m).bodd && n.bodd)

case negSucc
n : ℤ
m : ℕ
⊢ (-[m+1] * n).bodd = (-[m+1].bodd && n.bodd)
Module: Mathlib.Data.Int.Fib.Lemmas

Goal state before:
pp: n : ℕ
⊢ fib (↑n + 1) * fib (↑n - 1) - fib ↑n ^ 2 = (-1) ^ n

Tactic:
induction n with

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

Goal state before:
pp: case true
n : ℕ
⊢ 0 + 2 * -[n.div2+1] = -[1 + 2 * n.div2+1]

Tactic:
· rw [zero_add, add_comm]
      rfl

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

Goal state before:
pp: m n : ℤ
⊢ bitwise or m n = m.lor n

Tactic:
rcases m with m | m

Goal state after:
case ofNat
n : ℤ
m : ℕ
⊢ bitwise or (ofNat m) n = (ofNat m).lor n

case negSucc
n : ℤ
m : ℕ
⊢ bitwise or -[m+1] n = -[m+1].lor n
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: m n : ℤ
⊢ bitwise and m n = m.land n

Tactic:
rcases m with m | m

Goal state after:
case ofNat
n : ℤ
m : ℕ
⊢ bitwise and (ofNat m) n = (ofNat m).land n

case negSucc
n : ℤ
m : ℕ
⊢ bitwise and -[m+1] n = -[m+1].land n
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: m n : ℤ
⊢ bitwise (fun a b ↦ a && !b) m n = m.ldiff n

Tactic:
rcases m with m | m

Goal state after:
case ofNat
n : ℤ
m : ℕ
⊢ bitwise (fun a b ↦ a && !b) (ofNat m) n = (ofNat m).ldiff n

case negSucc
n : ℤ
m : ℕ
⊢ bitwise (fun a b ↦ a && !b) -[m+1] n = -[m+1].ldiff n
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: m n : ℤ
⊢ bitwise xor m n = m.xor n

Tactic:
rcases m with m | m

Goal state after:
case ofNat
n : ℤ
m : ℕ
⊢ bitwise xor (ofNat m) n = (ofNat m).xor n

case negSucc
n : ℤ
m : ℕ
⊢ bitwise xor -[m+1] n = -[m+1].xor n
Module: Mathlib.Data.LawfulXor.Basic

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

Tactic:
by
  rw [← xor_assoc, LawfulXor.xor_self, zero_xor]

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

Goal state before:
pp: f : Bool → Bool → Bool
a : Bool
m : ℤ
b : Bool
n : ℤ
⊢ bitwise f (bit a m) (bit b n) = bit (f a b) (bitwise f m n)

Tactic:
rcases m with m | m

Goal state after:
case ofNat
f : Bool → Bool → Bool
a b : Bool
n : ℤ
m : ℕ
⊢ bitwise f (bit a (ofNat m)) (bit b n) = bit (f a b) (bitwise f (ofNat m) n)

case negSucc
f : Bool → Bool → Bool
a b : Bool
n : ℤ
m : ℕ
⊢ bitwise f (bit a -[m+1]) (bit b n) = bit (f a b) (bitwise f -[m+1] n)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case negSucc.ofNat
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
⊢ (match
      bif f (!false) false then -[Nat.bitwise (fun x y ↦ !f (!x) y) a✝¹ a✝+1]
      else ↑(Nat.bitwise (fun x y ↦ f (!x) y) a✝¹ a✝),
      k with
    | ofNat m, n => m.testBit n
    | -[m+1], n => !m.testBit n) =
    f (!a✝¹.testBit k) (a✝.testBit k)

pp: case negSucc.negSucc
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
⊢ (match
      bif f (!false) !false then -[Nat.bitwise (fun x y ↦ !f (!x) !y) a✝¹ a✝+1]
      else ↑(Nat.bitwise (fun x y ↦ f (!x) !y) a✝¹ a✝),
      k with
    | ofNat m, n => m.testBit n
    | -[m+1], n => !m.testBit n) =
    f (!a✝¹.testBit k) !a✝.testBit k

Tactic:
· by_cases h : f true false <;> simp [h]

Goal state after:
case negSucc.negSucc
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
⊢ (match
      bif f (!false) !false then -[Nat.bitwise (fun x y ↦ !f (!x) !y) a✝¹ a✝+1]
      else ↑(Nat.bitwise (fun x y ↦ f (!x) !y) a✝¹ a✝),
      k with
    | ofNat m, n => m.testBit n
    | -[m+1], n => !m.testBit n) =
    f (!a✝¹.testBit k) !a✝.testBit k
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: m n : ℕ
⊢ ↑m >>> ↑n = ↑(m >>> n)

Tactic:
by cases n <;> rfl

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

Goal state before:
pp: m n : ℕ
⊢ -[m+1] >>> ↑n = -[m >>> n+1]

Tactic:
by cases n <;> rfl

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

Goal state before:
pp: case cons.nil
α : Type u_1
f : α → α
l₁ : List α
hd : α
x✝ : [hd] ≠ []
⊢ modifyLast.go f (l₁ ++ [hd]) #[] = l₁ ++ [f hd]

Tactic:
exact modifyLast_concat _ hd _

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

Goal state before:
pp: α : Type u_1
w : List α
⊢ w.HasPeriod 0

Tactic:
simp [HasPeriod]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.DualNumber

Goal state before:
pp: case h1
R n : Type
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A B : Matrix n n (DualNumber R)
i✝ j✝ : n
⊢ fst (of fun i j ↦ fst ((A * B) i j), of fun i j ↦ snd ((A * B) i j)) i✝ j✝ =
    fst ((of fun i j ↦ fst (A i j), of fun i j ↦ snd (A i j)) * (of fun i j ↦ fst (B i j), of fun i j ↦ snd (B i j))) i✝
      j✝

pp: case h2
R n : Type
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A B : Matrix n n (DualNumber R)
i✝ j✝ : n
⊢ snd (of fun i j ↦ fst ((A * B) i j), of fun i j ↦ snd ((A * B) i j)) i✝ j✝ =
    snd ((of fun i j ↦ fst (A i j), of fun i j ↦ snd (A i j)) * (of fun i j ↦ fst (B i j), of fun i j ↦ snd (B i j))) i✝
      j✝

Tactic:
· dsimp [mul_apply]
      simp_rw [fst_sum]
      rfl

Goal state after:
case h2
R n : Type
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A B : Matrix n n (DualNumber R)
i✝ j✝ : n
⊢ snd (of fun i j ↦ fst ((A * B) i j), of fun i j ↦ snd ((A * B) i j)) i✝ j✝ =
    snd ((of fun i j ↦ fst (A i j), of fun i j ↦ snd (A i j)) * (of fun i j ↦ fst (B i j), of fun i j ↦ snd (B i j))) i✝
      j✝