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

Goal state before:
pp: case refl.some
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
b₂ a₂ : σ₂
aa : tr a₁ a₂
ab✝ : b₂ ∈ eval f₂ a₂
ab : Reaches f₂ a₂ b₂
b0 : f₂ b₂ = none
c₁ : σ₁
ac : Reaches f₁ a₁ c₁
bc : Reaches f₂ b₂ b₂
cc : tr c₁ b₂
this :
  match f₁ c₁ with
  | some b₁ => ∃ b₂_1, tr b₁ b₂_1 ∧ Reaches₁ f₂ b₂ b₂_1
  | none => f₂ b₂ = none
d₁ : σ₁
hfc : f₁ c₁ = some d₁
⊢ some d₁ = none

Tactic:
rw [hfc] at this

Goal state after:
case refl.some
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
b₂ a₂ : σ₂
aa : tr a₁ a₂
ab✝ : b₂ ∈ eval f₂ a₂
ab : Reaches f₂ a₂ b₂
b0 : f₂ b₂ = none
c₁ : σ₁
ac : Reaches f₁ a₁ c₁
bc : Reaches f₂ b₂ b₂
cc : tr c₁ b₂
d₁ : σ₁
this :
  match some d₁ with
  | some b₁ => ∃ b₂_1, tr b₁ b₂_1 ∧ Reaches₁ f₂ b₂ b₂_1
  | none => f₂ b₂ = none
hfc : f₁ c₁ = some d₁
⊢ some d₁ = none
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case some.write
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
x✝ : Cfg Γ Λ σ
f : Γ → σ → Γ
q : Stmt Γ Λ σ
IH :
  ∀ (v : σ) (L R : ListBlank Γ),
    Reaches (step (tr enc dec M)) (stepAux (trNormal dec q) v (trTape' enc0 L R))
      (trCfg enc enc0 (stepAux q v (Tape.mk' L R)))
v : σ
L : ListBlank Γ
a : Γ
R : ListBlank Γ
⊢ ReflTransGen (fun a b ↦ b ∈ step (tr enc dec M) a)
    (stepAux (move n Dir.left (trNormal dec q)) v (trTape' enc0 (ListBlank.cons (f (ListBlank.cons a R).head v) L) R))
    (trCfg enc enc0 (stepAux q v (Tape.write (f (ListBlank.cons a R).head v) (Tape.mk' L (ListBlank.cons a R)))))

Tactic:
ListBlank.head_cons,

Goal state after:
case some.write
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
x✝ : Cfg Γ Λ σ
f : Γ → σ → Γ
q : Stmt Γ Λ σ
IH :
  ∀ (v : σ) (L R : ListBlank Γ),
    Reaches (step (tr enc dec M)) (stepAux (trNormal dec q) v (trTape' enc0 L R))
      (trCfg enc enc0 (stepAux q v (Tape.mk' L R)))
v : σ
L : ListBlank Γ
a : Γ
R : ListBlank Γ
⊢ ReflTransGen (fun a b ↦ b ∈ step (tr enc dec M) a)
    (stepAux (move n Dir.left (trNormal dec q)) v (trTape' enc0 (ListBlank.cons (f a v) L) R))
    (trCfg enc enc0 (stepAux q v (Tape.write (f a v) (Tape.mk' L (ListBlank.cons a R)))))
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case prim.prec.succ
n✝² : ℕ
f✝¹ : List.Vector ℕ n✝² →. ℕ
n✝¹ : ℕ
f✝ : List.Vector ℕ n✝¹ → ℕ
n✝ : ℕ
f : List.Vector ℕ n✝ → ℕ
g : List.Vector ℕ (n✝ + 2) → ℕ
a✝² : Nat.Primrec' f
a✝¹ : Nat.Primrec' g
cf cg : Code
v : List.Vector ℕ (n✝ + 1)
hf : cf.eval (↑v).tail = pure (pure (f v.tail))
hg : ∀ (a b : ℕ), cg.eval (a :: b :: (↑v).tail) = pure (pure (g (a ::ᵥ b ::ᵥ v.tail)))
n : ℕ
a✝ :
  (cf.prec cg).eval (n :: (↑v).tail) =
    pure (pure (Nat.rec (f (n ::ᵥ v.tail).tail) (fun y IH ↦ g (y ::ᵥ IH ::ᵥ (n ::ᵥ v.tail).tail)) (n ::ᵥ v.tail).head))
⊢ (cf.prec cg).eval ((n + 1) :: (↑v).tail) =
    pure
      (pure
        (Nat.rec (f ((n + 1) ::ᵥ v.tail).tail) (fun y IH ↦ g (y ::ᵥ IH ::ᵥ ((n + 1) ::ᵥ v.tail).tail))
          ((n + 1) ::ᵥ v.tail).head))

Tactic:
suffices ∀ a b, a + b = n →
        (n.succ :: 0 ::
          g (n ::ᵥ Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) n ::ᵥ v.tail) ::
              v.val.tail : List ℕ) ∈
          PFun.fix
            (fun v : List ℕ => Part.bind (cg.eval (v.headI :: v.tail.tail))
              (fun x => Part.some (if v.tail.headI = 0
                then Sum.inl
                  (v.headI.succ :: v.tail.headI.pred :: x.headI :: v.tail.tail.tail : List ℕ)
                else Sum.inr
                  (v.headI.succ :: v.tail.headI.pred :: x.headI :: v.tail.tail.tail))))
            (a :: b :: Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) a :: v.val.tail) by
        have := Part.eq_some_iff.mpr (this _ _ (zero_add _))
        simp [prec, Part.bind_assoc, Bind.bind]
        simp_all
      intro a b e
      induction b generalizing a with
      | zero =>
        refine PFun.mem_fix_iff.2 (Or.inl <| Part.eq_some_iff.1 ?_)
        simp only [hg, ← e, Part.bind_some, List.tail_cons, pure]
        rfl
      | succ b IH =>
        refine PFun.mem_fix_iff.2 (Or.inr ⟨_, ?_, IH (a + 1) (by rwa [add_right_comm])⟩)
        simp only [hg, Part.bind_some, List.tail_cons, pure]
        exact Part.mem_some_iff.2 rfl

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

Goal state before:
pp: case zero'
k : Cont
v : List ℕ
⊢ ∃ k' v', stepNormal Code.zero' k v = Cfg.ret k' v'

Tactic:
exact ⟨_, _, rfl⟩

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

Goal state before:
pp: case succ
k : Cont
v : List ℕ
⊢ ∃ k' v', stepNormal Code.succ k v = Cfg.ret k' v'

Tactic:
exact ⟨_, _, rfl⟩

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

Goal state before:
pp: case tail
k : Cont
v : List ℕ
⊢ ∃ k' v', stepNormal Code.tail k v = Cfg.ret k' v'

Tactic:
exact ⟨_, _, rfl⟩

Goal state after:
Module: Mathlib.Topology.Separation.Profinite

Goal state before:
pp: X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : T2Space X
inst✝¹ : CompactSpace X
inst✝ : TotallyDisconnectedSpace X
x : X
U : Set X
hxU : x ∈ U
U_op : IsOpen[inst✝³] U
this : U ∈ 𝓝 x
⊢ ∃ v ∈ fun U ↦ IsClosed[inst✝³] U ∧ IsOpen[inst✝³] U, x ∈ v ∧ v ⊆ U

Tactic:
rcases (nhds_basis_clopen x).mem_iff.mp this with ⟨V, ⟨hxV, hV⟩, hVU : V ⊆ U⟩

Goal state after:
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : T2Space X
inst✝¹ : CompactSpace X
inst✝ : TotallyDisconnectedSpace X
x : X
U : Set X
hxU : x ∈ U
U_op : IsOpen[inst✝³] U
this : U ∈ 𝓝 x
V : Set X
hVU : V ⊆ U
hxV : x ∈ V
hV : IsClopen V
⊢ ∃ v ∈ fun U ↦ IsClosed[inst✝³] U ∧ IsOpen[inst✝³] U, x ∈ v ∧ v ⊆ U
Module: Mathlib.Topology.Category.Profinite.Basic

Goal state before:
pp: case mp
X Y : Profinite
f : X ⟶ Y
y : ↑Y.toTop
hy : ∀ (a : ↑X.toTop), (ConcreteCategory.hom f) a ≠ y
hf : Epi f
⊢ False

Tactic:
let C := Set.range f

Goal state after:
case mp
X Y : Profinite
f : X ⟶ Y
y : ↑Y.toTop
hy : ∀ (a : ↑X.toTop), (ConcreteCategory.hom f) a ≠ y
hf : Epi f
C : Set ((fun X ↦ ↑X.toTop) Y) := Set.range ⇑(ConcreteCategory.hom f)
⊢ False
Module: Mathlib.Topology.Category.Stonean.Basic

Goal state before:
pp: X Y : Stonean
f : X ⟶ Y
h : Epi f
y : ↑Y.toTop
hy : ∀ (a : ↑X.toTop), (ConcreteCategory.hom f) a ≠ y
⊢ False

Tactic:
let C := Set.range f

Goal state after:
X Y : Stonean
f : X ⟶ Y
h : Epi f
y : ↑Y.toTop
hy : ∀ (a : ↑X.toTop), (ConcreteCategory.hom f) a ≠ y
C : Set ((fun X ↦ ↑X.toTop) Y) := Set.range ⇑(ConcreteCategory.hom f)
⊢ False
Module: Mathlib.Topology.Category.Stonean.Basic

Goal state before:
pp: X B C : Stonean
φ : X ⟶ C
f : B ⟶ C
inst✝ : Epi f
this : ExtremallyDisconnected ↑X.toTop
⊢ Function.Surjective ⇑(ConcreteCategory.hom f)

Tactic:
← Stonean.epi_iff_surjective

Goal state after:
X B C : Stonean
φ : X ⟶ C
f : B ⟶ C
inst✝ : Epi f
this : ExtremallyDisconnected ↑X.toTop
⊢ Epi f
Module: Mathlib.Topology.Category.LightProfinite.Basic

Goal state before:
pp: case mp
X Y : LightProfinite
f : X ⟶ Y
y : ↑Y.toTop
hy : ∀ (a : ↑X.toTop), (ConcreteCategory.hom f) a ≠ y
hf : Epi f
⊢ False

Tactic:
let C := Set.range f

Goal state after:
case mp
X Y : LightProfinite
f : X ⟶ Y
y : ↑Y.toTop
hy : ∀ (a : ↑X.toTop), (ConcreteCategory.hom f) a ≠ y
hf : Epi f
C : Set ((fun X ↦ ↑X.toTop) Y) := Set.range ⇑(ConcreteCategory.hom f)
⊢ False
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: f fs : Code
k : Cont'
⊢ codeSupp (f.cons fs) k = trStmts₁ (trNormal (f.cons fs) k) ∪ codeSupp f (Cont'.cons₁ fs k)

Tactic:
simp [codeSupp, codeSupp', contSupp, Finset.union_assoc]

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

Goal state before:
pp: case fix
S : Finset Λ'
f : Code
IHf : ∀ {k : Cont'}, codeSupp f k ⊆ S → Λ'.Supports S (trNormal f k)
k : Cont'
Hk : codeSupp f.fix k ⊆ S
⊢ codeSupp f (Cont'.fix f k) ⊆ S

Tactic:
rw [codeSupp_fix] at Hk

Goal state after:
case fix
S : Finset Λ'
f : Code
IHf : ∀ {k : Cont'}, codeSupp f k ⊆ S → Λ'.Supports S (trNormal f k)
k : Cont'
Hk : trStmts₁ (trNormal f.fix k) ∪ codeSupp f (Cont'.fix f k) ⊆ S
⊢ codeSupp f (Cont'.fix f k) ⊆ S
Module: Mathlib.Condensed.Light.InternallyProjective

Goal state before:
pp: case refine_2
R : Type u
inst✝ : CommRing R
P : LightProfinite
h :
  ∀ {A B : LightCondMod R} (e : A ⟶ B) [Epi e] (S : LightProfinite) (g : (free R).obj (S ⊗ P).toCondensed ⟶ B),
    ∃ S' π,
      ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
        ∃ g', (free R).map (lightProfiniteToLightCondSet.map (π ▷ P)) ≫ g = g' ≫ e
A B : LightCondMod R
e : A ⟶ B
he : Epi e
S : LightProfinite
g : (free R).obj (S.toCondensed ⊗ P.toCondensed) ⟶ B
⊢ ∃ S' π,
    ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
      ∃ g', (free R).map (lightProfiniteToLightCondSet.map π ▷ P.toCondensed) ≫ g = g' ≫ e

Tactic:
specialize h e S ((free R).map (μIso lightProfiniteToLightCondSet _ _).inv ≫ g)
    obtain ⟨S', π, hπ, g', hh⟩ := h
    refine ⟨S', π, hπ, (free R).map
      (μIso lightProfiniteToLightCondSet _ _).hom ≫ g', ?_⟩
    rw [assoc, ← hh]
    simp [-map_comp, ← map_comp_assoc, ← μ_natural_left_assoc]

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

Goal state before:
pp: σ : Type u
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
f : β → F γ
g : α → G β
x : σ ⊕ α
⊢ Sum.traverse (Comp.mk ∘ (fun x ↦ f <$> x) ∘ g) x = Comp.mk (Sum.traverse f <$> Sum.traverse g x)

Tactic:
cases x <;> (simp! [Sum.traverse, map_id, functor_norm] <;> rfl)

Goal state after:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: case pos
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (⇑f) i a).Dom
⊢ b ∈ approx (⇑f) (Nat.find h₀).succ a ↔ ∃ i, b ∈ approx (⇑f) i a

Tactic:
constructor <;> intro hh

Goal state after:
case pos.mp
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (⇑f) i a).Dom
hh : b ∈ approx (⇑f) (Nat.find h₀).succ a
⊢ ∃ i, b ∈ approx (⇑f) i a

case pos.mpr
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (⇑f) i a).Dom
hh : ∃ i, b ∈ approx (⇑f) i a
⊢ b ∈ approx (⇑f) (Nat.find h₀).succ a
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
α α' β β' : TypeVec.{u_1} n
f : α ⟹ β
g : α' ⟹ β'
⊢ prod.fst ⊚ (f ⊗' g) = f ⊚ prod.fst

Tactic:
by
  funext i; induction i with
  | fz => rfl
  | fs _ i_ih => apply i_ih

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
α α' β β' : TypeVec.{u_1} n
f : α ⟹ β
g : α' ⟹ β'
⊢ prod.snd ⊚ (f ⊗' g) = g ⊚ prod.snd

Tactic:
by
  funext i; induction i with
  | fz => rfl
  | fs _ i_ih => apply i_ih

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
α : TypeVec.{u_1} n
⊢ prod.fst ⊚ prod.diag = id

Tactic:
by
  funext i; induction i with
  | fz => rfl
  | fs _ i_ih => apply i_ih

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
α : TypeVec.{u_1} n
⊢ prod.snd ⊚ prod.diag = id

Tactic:
by
  funext i; induction i with
  | fz => rfl
  | fs _ i_ih => apply i_ih

Goal state after:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
⊢ Part.fix ⇑f = ωSup (approxChain f)

Tactic:
by
  apply le_antisymm
  · intro x
    obtain ⟨i, hx⟩ := exists_fix_le_approx f x
    trans approx f i.succ x
    · trans
      · apply hx
      · apply approx_mono' f
    apply le_ωSup_of_le i.succ
    dsimp [approx]
    rfl
  · apply ωSup_le _ _ _
    simp only [Fix.approxChain]
    intro y x
    apply approx_le_fix f

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
f : (free R).obj (S ⊗ ℕ∪{∞}).toCondensed ⟶ Y
T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
g : (free R).obj T.toCondensed ⟶ X
hπ : Epi π
comm : (lightProfiniteToLightCondSet ⋙ free R).map π ≫ f = g ≫ p
S' T' : LightProfinite
y' : S' ⟶ S
π' : T' ⟶ S' ⊗ ℕ∪{∞}
g' : T' ⟶ T
hπ' : Epi π'
hy' : Epi y'
comp : π' ≫ y' ▷ ℕ∪{∞} = g' ≫ π
epi : Epi (cover π')
split : SplitEpi (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π' ≫ fst S' ℕ∪{∞})
hS' : Nonempty ↑S'.toTop
this : Mono (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}))
x : ↑T'.toTop
hx : (⇑(ConcreteCategory.hom (snd S' ℕ∪{∞})) ∘ ⇑(ConcreteCategory.hom π')) x = ∞
⊢ x ∈ ⇑(ConcreteCategory.hom (π' ≫ snd S' ℕ∪{∞})) ⁻¹' {∞}

Tactic:
by simpa using hx

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

Goal state before:
pp: case e'_1.e'_3
α : Type u
β : α → Type v
inst✝ : DecidableEq α
C : AList β → Sort u_1
H0 : C ∅
IH : (a : α) → (b : β a) → (l : AList β) → ¬a ∈ l → C l → C (insert a b l)
l : List (Sigma β)
hl : l.NodupKeys
fst✝ : α
snd✝ : β fst✝
h : ¬⟨fst✝, snd✝⟩.fst ∈ { entries := l, nodupKeys := hl }
this :
  insertRec H0 IH { entries := ⟨fst✝, snd✝⟩ :: l, nodupKeys := ⋯ } ≍
    IH ⟨fst✝, snd✝⟩.fst ⟨fst✝, snd✝⟩.snd { entries := l, nodupKeys := hl } h
      (insertRec H0 IH { entries := l, nodupKeys := hl })
⊢ (insert ⟨fst✝, snd✝⟩.fst ⟨fst✝, snd✝⟩.snd { entries := l, nodupKeys := hl }).entries = ⟨fst✝, snd✝⟩ :: l

Tactic:
insert_of_notMem h

Goal state after:
case e'_1.e'_3
α : Type u
β : α → Type v
inst✝ : DecidableEq α
C : AList β → Sort u_1
H0 : C ∅
IH : (a : α) → (b : β a) → (l : AList β) → ¬a ∈ l → C l → C (insert a b l)
l : List (Sigma β)
hl : l.NodupKeys
fst✝ : α
snd✝ : β fst✝
h : ¬⟨fst✝, snd✝⟩.fst ∈ { entries := l, nodupKeys := hl }
this :
  insertRec H0 IH { entries := ⟨fst✝, snd✝⟩ :: l, nodupKeys := ⋯ } ≍
    IH ⟨fst✝, snd✝⟩.fst ⟨fst✝, snd✝⟩.snd { entries := l, nodupKeys := hl } h
      (insertRec H0 IH { entries := l, nodupKeys := hl })
⊢ { entries := ⟨⟨fst✝, snd✝⟩.fst, ⟨fst✝, snd✝⟩.snd⟩ :: { entries := l, nodupKeys := hl }.entries,
        nodupKeys := ⋯ }.entries =
    ⟨fst✝, snd✝⟩ :: l
Module: Mathlib.Data.List.AList

Goal state before:
pp: case e'_2.e'_3
α : Type u
β : α → Type v
inst✝ : DecidableEq α
C : AList β → Sort u_1
H0 : C ∅
IH : (a : α) → (b : β a) → (l : AList β) → ¬a ∈ l → C l → C (insert a b l)
l : List (Sigma β)
hl : l.NodupKeys
fst✝ : α
snd✝ : β fst✝
h : ¬⟨fst✝, snd✝⟩.fst ∈ { entries := l, nodupKeys := hl }
this :
  insertRec H0 IH { entries := ⟨fst✝, snd✝⟩ :: l, nodupKeys := ⋯ } ≍
    IH ⟨fst✝, snd✝⟩.fst ⟨fst✝, snd✝⟩.snd { entries := l, nodupKeys := hl } h
      (insertRec H0 IH { entries := l, nodupKeys := hl })
e_1✝ :
  C (insert ⟨fst✝, snd✝⟩.fst ⟨fst✝, snd✝⟩.snd { entries := l, nodupKeys := hl }) =
    C { entries := ⟨fst✝, snd✝⟩ :: l, nodupKeys := ⋯ }
⊢ (insert ⟨fst✝, snd✝⟩.fst ⟨fst✝, snd✝⟩.snd { entries := l, nodupKeys := hl }).entries = ⟨fst✝, snd✝⟩ :: l

Tactic:
insert_of_notMem h

Goal state after:
case e'_2.e'_3
α : Type u
β : α → Type v
inst✝ : DecidableEq α
C : AList β → Sort u_1
H0 : C ∅
IH : (a : α) → (b : β a) → (l : AList β) → ¬a ∈ l → C l → C (insert a b l)
l : List (Sigma β)
hl : l.NodupKeys
fst✝ : α
snd✝ : β fst✝
h : ¬⟨fst✝, snd✝⟩.fst ∈ { entries := l, nodupKeys := hl }
this :
  insertRec H0 IH { entries := ⟨fst✝, snd✝⟩ :: l, nodupKeys := ⋯ } ≍
    IH ⟨fst✝, snd✝⟩.fst ⟨fst✝, snd✝⟩.snd { entries := l, nodupKeys := hl } h
      (insertRec H0 IH { entries := l, nodupKeys := hl })
e_1✝ :
  C (insert ⟨fst✝, snd✝⟩.fst ⟨fst✝, snd✝⟩.snd { entries := l, nodupKeys := hl }) =
    C { entries := ⟨fst✝, snd✝⟩ :: l, nodupKeys := ⋯ }
⊢ { entries := ⟨⟨fst✝, snd✝⟩.fst, ⟨fst✝, snd✝⟩.snd⟩ :: { entries := l, nodupKeys := hl }.entries,
        nodupKeys := ⋯ }.entries =
    ⟨fst✝, snd✝⟩ :: l
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : l.NodupKeys
h : ⟨a, b⟩ ∈ l
⊢ b ∈ dlookup a l

Tactic:
obtain ⟨b', h'⟩ := Option.isSome_iff_exists.mp (dlookup_isSome.mpr (mem_keys_of_mem h))
  cases nd.eq_of_mk_mem h (of_mem_dlookup h')
  exact h'

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

Goal state before:
pp: case mpr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint s₂
x✝ : α
y✝ : β x✝
h' : dlookup x✝ s₂.entries = some y✝ ∨ ¬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:
· rcases h' with h' | h'
        · right
          refine ⟨?_, h'⟩
          intro h''
          apply h _ h''
          rw [keys, ← List.dlookup_isSome, h']
          exact rfl
        · left
          rw [h'.2]

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys
⊢ (lookupAll a l).length ≤ 1

Tactic:
by
  have := Nodup.sublist ((lookupAll_sublist a l).map _) h
  rw [map_map] at this
  rwa [← nodup_replicate, ← map_const]

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s₁ s₂ : Finmap β
h : a ∉ s₂
h' : a ∉ s₁
⊢ lookup a s₂ = lookup a s₁

Tactic:
lookup_eq_none.mpr h,

Goal state after:
case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s₁ s₂ : Finmap β
h : a ∉ s₂
h' : a ∉ s₁
⊢ none = lookup a s₁
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case pos
α : 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₂
h : a ∈ (hd :: tl).keys
e : a = hd.fst
⊢ ∃ b l₁ l₂, ¬a ∈ l₁.keys ∧ hd :: tl = l₁ ++ ⟨a, b⟩ :: l₂ ∧ kerase a (hd :: tl) = l₁ ++ l₂

Tactic:
subst e
      exact ⟨hd.2, [], tl, by simp, by cases hd; rfl, by simp⟩

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

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

Tactic:
rw [keys, kerase, erase_eq_eraseP, eraseP_map, Function.comp_def]

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
⊢ map Sigma.fst (eraseP (fun s ↦ decide (a = s.fst)) l) = map Sigma.fst (eraseP (fun x ↦ a == x.fst) l)
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
inst✝¹ : DecidableEq α
inst✝ : SizeOf (Sigma β)
x : α
xs : List (Sigma β)
⊢ sizeOf (kerase x xs) ≤ sizeOf xs

Tactic:
induction xs with
  | nil => simp
  | cons y ys => by_cases x = y.1 <;> simp [*]

Goal state after:
Module: Mathlib.Data.Holor

Goal state before:
pp: ds₁ ds₂ ds₃ is : List ℕ
h : Forall₂ (fun x1 x2 ↦ x1 < x2) is (ds₁ ++ ds₂ ++ ds₃)
⊢ ↑(assocRight ⟨is, h⟩).drop.take = ↑(take ⟨is, h⟩).drop

Tactic:
simp [assocRight, take, drop, cast_type, List.drop_take]

Goal state after:
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
d : ℕ
ds : List ℕ
inst✝ : Semiring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
⊢ (∑ i ∈ (Finset.range d).attach, unitVec d ↑i ⊗ x.slice ↑i ⋯).slice i hid = x.slice i hid

Tactic:
← slice_sum

Goal state after:
α : Type
d : ℕ
ds : List ℕ
inst✝ : Semiring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
⊢ ∑ x_1 ∈ (Finset.range d).attach, (unitVec d ↑x_1 ⊗ x.slice ↑x_1 ⋯).slice i hid = x.slice i hid
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case zero
⊢ (negOfNat 0).bodd = Nat.bodd 0

Tactic:
simp +decide

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

Goal state before:
pp: case succ
n✝ : ℕ
⊢ (negOfNat (n✝ + 1)).bodd = (n✝ + 1).bodd

Tactic:
simp +decide

Goal state after:
case succ
n✝ : ℕ
⊢ (negOfNat (n✝ + 1)).bodd = !n✝.bodd
Module: Mathlib.Data.Int.Lemmas

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

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

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

Goal state before:
pp: case pos
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
h : v % r < b % r
⊢ v % r < b % r ∧ ↑(b % r - v % r) ≤ ↑r

Tactic:
cast_le,

Goal state after:
case pos
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
h : v % r < b % r
⊢ v % r < b % r ∧ b % r - v % r ≤ r
Module: Mathlib.Data.List.Fold

Goal state before:
pp: α : Type u_1
β : Type u_2
l : List α
v : β → α → β
a : α
b : β
hv : RightCommutative v
⊢ foldl v b (a :: l) = v (foldl v b l) a

Tactic:
rw [foldl_cons]
  induction l generalizing a b <;> simp [*, hv.right_comm]

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

Goal state before:
pp: α : Type u_1
l : List α
f : α → α → α
ha : Std.Associative f
a b : α
⊢ f (foldl f a l) b = f a (foldr f b l)

Tactic:
by
  induction l generalizing a <;> simp [*, ha.assoc]

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

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

Tactic:
simp_rw [rtakeWhile, reverse_reverse]

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

Goal state before:
pp: case neg.inr
α : Type u_1
p i : ℕ
w : List α
per : w.HasPeriod p
less : i < w.length
p_zero : ¬p = 0
large : p ≤ i
len' : i - p < w.length
IH : w[(i - p) % p]? = w[i - p]?
⊢ w[i % p]? = w[i]?

Tactic:
rw [hasPeriod_iff_getElem?] at per

Goal state after:
case neg.inr
α : Type u_1
p i : ℕ
w : List α
per : ∀ i < w.length - p, w[i]? = w[i + p]?
less : i < w.length
p_zero : ¬p = 0
large : p ≤ i
len' : i - p < w.length
IH : w[(i - p) % p]? = w[i - p]?
⊢ w[i % p]? = w[i]?
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: case intro
α : Type u_1
inst✝ : Preorder α
a✝ a : α
h✝ : ∀ (y : α), y < a → Acc LT.lt y
ha : ∀ (y : α), y < a → ∀ {M : Multiset α}, Acc OneStep M → Acc OneStep (y ::ₘ M)
M : Multiset α
hM : Acc OneStep M
⊢ Acc OneStep (a ::ₘ M)

Tactic:
induction hM with

Goal state after:
case intro.intro
α : Type u_1
inst✝ : Preorder α
a✝ a : α
h✝ : ∀ (y : α), y < a → Acc LT.lt y
ha : ∀ (y : α), y < a → ∀ {M : Multiset α}, Acc OneStep M → Acc OneStep (y ::ₘ M)
M✝ M : Multiset α
hM : ∀ (y : Multiset α), y.OneStep M → Acc OneStep y
ihM : ∀ (y : Multiset α), y.OneStep M → Acc OneStep (a ::ₘ y)
⊢ Acc OneStep (a ::ₘ M)
Module: Mathlib.Data.Nat.ChineseRemainder

Goal state before:
pp: case nil
a b : ℕ
co : List.Pairwise Coprime []
⊢ a ≡ b [MOD [].prod] ↔ ∀ (i : Fin [].length), a ≡ b [MOD [].get i]

Tactic:
simp [modEq_one]

Goal state after:
Module: Mathlib.Data.Nat.ChineseRemainder

Goal state before:
pp: case nil
ι : Type u_1
a b : ℕ
s : ι → ℕ
co : List.Pairwise (Coprime on s) []
⊢ a ≡ b [MOD (List.map s []).prod] ↔ ∀ i ∈ [], a ≡ b [MOD s i]

Tactic:
simp [modEq_one]

Goal state after:
Module: Mathlib.Data.Nat.ChineseRemainder

Goal state before:
pp: case nil
ι : Type u_1
a s : ι → ℕ
z : ℕ
co : List.Pairwise (Coprime on s) []
hz : ∀ i ∈ [], z ≡ a i [MOD s i]
⊢ z ≡ ↑(chineseRemainderOfList a s [] co) [MOD (List.map s []).prod]

Tactic:
simp [modEq_one]

Goal state after:
Module: Mathlib.Data.Nat.ChineseRemainder

Goal state before:
pp: case cons
ι : Type u_1
a s : ι → ℕ
z : ℕ
i : ι
l : List ι
ih :
  ∀ (co : List.Pairwise (Coprime on s) l),
    (∀ i ∈ l, z ≡ a i [MOD s i]) → z ≡ ↑(chineseRemainderOfList a s l co) [MOD (List.map s l).prod]
co : List.Pairwise (Coprime on s) (i :: l)
hz : ∀ i_1 ∈ i :: l, z ≡ a i_1 [MOD s i_1]
⊢ z ≡ ↑(chineseRemainderOfList a s (i :: l) co) [MOD (List.map s (i :: l)).prod]

Tactic:
simp only [List.map_cons, List.prod_cons, chineseRemainderOfList]
    have : Coprime (s i) (l.map s).prod := by
      simp only [coprime_list_prod_right_iff, List.mem_map, forall_exists_index, and_imp,
        forall_apply_eq_imp_iff₂]
      intro j hj
      exact (List.pairwise_cons.mp co).1 j hj
    exact chineseRemainder_modEq_unique this
      (hz i List.mem_cons_self) (ih co.of_cons (fun j hj => hz j (List.mem_cons_of_mem _ hj)))

Goal state after: