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

Goal state before:
pp: case prim.prec.succ.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))
b : ℕ
IH :
  ∀ (a : ℕ),
    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).tail ∈
        PFun.fix
          (fun v ↦
            (cg.eval (v.headI :: v.tail.tail)).bind 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)
                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).tail)
a : ℕ
e : a + (b + 1) = n
⊢ n.succ :: 0 :: g (n ::ᵥ Nat.rec (f v.tail) (fun y IH ↦ g (y ::ᵥ IH ::ᵥ v.tail)) n ::ᵥ v.tail) :: (↑v).tail ∈
    PFun.fix
      (fun v ↦
        (cg.eval (v.headI :: v.tail.tail)).bind 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)
            else Sum.inr (v.headI.succ :: v.tail.headI.pred :: x.headI :: v.tail.tail.tail)))
      (a :: (b + 1) :: Nat.rec (f v.tail) (fun y IH ↦ g (y ::ᵥ IH ::ᵥ v.tail)) a :: (↑v).tail)

Tactic:
| succ b IH =>

Goal state after:
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))
a b : ℕ
e : 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).tail ∈
    PFun.fix
      (fun v ↦
        (cg.eval (v.headI :: v.tail.tail)).bind 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)
            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).tail)

Tactic:
induction b generalizing a with

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

Goal state before:
pp: case peek
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
k : K
q : TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse
f : σ → Option (Γ k) → σ
⊢ ∃ L',
    (∀ (k_1 : K), ListBlank.map (proj k_1) L' = ListBlank.mk (List.map some (update S k (S k) k_1)).reverse) ∧
      TM1.stepAux q
          (f v ((Tape.move Dir.left ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom L)))).head.2 k))
          (Tape.move Dir.right (Tape.move Dir.left ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom L))))) =
        TM1.stepAux q (f v (S k).head?) ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom L')))

Tactic:
rw [Function.update_eq_self]
    use L, hL; rw [Tape.move_left_right]; congr
    cases e : S k; · rfl
    rw [List.length_cons, iterate_succ', Function.comp, Tape.move_right_left,
      Tape.move_right_n_head, Tape.mk'_nth_nat, addBottom_nth_snd, stk_nth_val _ (hL k), e,
      List.reverse_cons, ← List.length_reverse, List.getElem?_concat_length]
    rfl

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

Goal state before:
pp: K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝¹ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst✝ : Inhabited Λ
S : Finset Λ
ss : TM2.Supports M S
l' : Λ' K Γ Λ σ
h : l' ∈ trSupp M S
this :
  ∀ (q : TM2.Stmt Γ Λ σ),
    TM2.SupportsStmt S q →
      (∀ x ∈ trStmts₁ q, x ∈ trSupp M S) →
        TM1.SupportsStmt (trSupp M S) (trNormal q) ∧ ∀ l' ∈ trStmts₁ q, TM1.SupportsStmt (trSupp M S) (tr M l')
⊢ TM1.SupportsStmt (trSupp M S) (tr M l')

Tactic:
by
      rcases Finset.mem_biUnion.1 h with ⟨l, lS, h⟩
      have :=
        this _ (ss.2 l lS) fun x hx ↦ Finset.mem_biUnion.2 ⟨_, lS, Finset.mem_insert_of_mem hx⟩
      rcases Finset.mem_insert.1 h with (rfl | h) <;> [exact this.1; exact this.2 _ h]

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

Goal state before:
pp: case refine_1
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝¹ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst✝ : Inhabited Λ
S : Finset Λ
ss : TM2.Supports M S
k✝ : K
s : StAct K Γ σ k✝
q✝ : TM2.Stmt Γ Λ σ
IH :
  TM2.SupportsStmt S q✝ →
    (∀ x ∈ trStmts₁ q✝, x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q✝) ∧ ∀ l' ∈ trStmts₁ q✝, TM1.SupportsStmt (trSupp M S) (tr M l')
ss' : TM2.SupportsStmt S q✝
sub : ∀ x ∈ trStmts₁ (stRun s q✝), x ∈ trSupp M S
⊢ TM1.SupportsStmt (trSupp M S) (trNormal (stRun s q✝)) ∧
    ∀ l' ∈ trStmts₁ (stRun s q✝), TM1.SupportsStmt (trSupp M S) (tr M l')

Tactic:
simp only [TM2to1.trStmts₁_run, Finset.mem_union, Finset.mem_insert, Finset.mem_singleton]
        at sub

Goal state after:
case refine_1
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝¹ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst✝ : Inhabited Λ
S : Finset Λ
ss : TM2.Supports M S
k✝ : K
s : StAct K Γ σ k✝
q✝ : TM2.Stmt Γ Λ σ
IH :
  TM2.SupportsStmt S q✝ →
    (∀ x ∈ trStmts₁ q✝, x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q✝) ∧ ∀ l' ∈ trStmts₁ q✝, TM1.SupportsStmt (trSupp M S) (tr M l')
ss' : TM2.SupportsStmt S q✝
sub : ∀ (x : Λ' K Γ Λ σ), (x = go k✝ s q✝ ∨ x = ret q✝) ∨ x ∈ trStmts₁ q✝ → x ∈ trSupp M S
⊢ TM1.SupportsStmt (trSupp M S) (trNormal (stRun s q✝)) ∧
    ∀ l' ∈ trStmts₁ (stRun s q✝), TM1.SupportsStmt (trSupp M S) (tr M l')
Module: Mathlib.Computability.TuringMachine.Config

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

Tactic:
rw [Cont.eval, stepRet, code_is_ok]
    simp only [← bind_pure_comp, bind_assoc]; congr; funext v'
    rw [reaches_eval]; swap
    · exact ReflTransGen.single rfl
    rw [stepRet, IH, bind_pure_comp]

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

Goal state before:
pp: k : Cont
v : List ℕ
⊢ eval step (stepRet k v) = Cfg.halt <$> k.eval v

Tactic:
by
  induction k generalizing v with
  | halt =>
    simp only [Cont.eval, map_pure]
    exact Part.eq_some_iff.2 (mem_eval.2 ⟨ReflTransGen.refl, rfl⟩)
  | cons₁ fs as k IH =>
    rw [Cont.eval, stepRet, code_is_ok]
    simp only [← bind_pure_comp, bind_assoc]; congr; funext v'
    rw [reaches_eval]; swap
    · exact ReflTransGen.single rfl
    rw [stepRet, IH, bind_pure_comp]
  | cons₂ ns k IH => rw [Cont.eval, stepRet]; exact IH
  | comp f k IH =>
    rw [Cont.eval, stepRet, code_is_ok]
    simp only [← bind_pure_comp, bind_assoc]; congr; funext v'
    rw [reaches_eval]; swap
    · exact ReflTransGen.single rfl
    rw [IH, bind_pure_comp]
  | fix f k IH =>
    rw [Cont.eval, stepRet]; simp only
    split_ifs; · exact IH
    simp only [← bind_pure_comp, bind_assoc, cont_eval_fix (code_is_ok _)]
    congr; funext; rw [bind_pure_comp, ← IH]
    exact reaches_eval (ReflTransGen.single rfl)

Goal state after:
Module: Mathlib.Topology.DiscreteQuotient

Goal state before:
pp: α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S : DiscreteQuotient X
x : X
⊢ IsOpen {S.proj x}

Tactic:
by
    rw [← S.proj_isQuotientMap.isOpen_preimage, fiber_eq]
    exact S.isOpen_setOfPred_rel _

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

Goal state before:
pp: case refine_1
c✝ : Code
v : List ℕ
i : Cfg'
h₁ : TrCfg (stepNormal c✝ Cont.halt v) i
h₂ : Reaches₁ (TM2.step tr) (init c✝ v) i
x : TM2.Cfg (fun x ↦ Γ') Λ' (Option Γ')
h : x ∈ eval (TM2.step tr) i
c : Cfg
hc₁ : TrCfg c x
hc₂ : ∃ a ∈ c✝.eval v, Cfg.halt a = c
⊢ ∃ a ∈ c✝.eval v, halt a = x

Tactic:
obtain ⟨v', hv, rfl⟩ := hc₂

Goal state after:
case refine_1
c : Code
v : List ℕ
i : Cfg'
h₁ : TrCfg (stepNormal c Cont.halt v) i
h₂ : Reaches₁ (TM2.step tr) (init c v) i
x : TM2.Cfg (fun x ↦ Γ') Λ' (Option Γ')
h : x ∈ eval (TM2.step tr) i
v' : List ℕ
hv : v' ∈ c.eval v
hc₁ : TrCfg (Cfg.halt v') x
⊢ ∃ a ∈ c.eval v, halt a = x
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)
s : Option Γ'
h : q' ∈ trStmts₁ (q s)
x : Λ'
h' : x ∈ trStmts₁ q'
⊢ x ∈ insert (Λ'.read q) (Finset.univ.biUnion fun s ↦ trStmts₁ (q s))

Tactic:
simp only [Finset.mem_biUnion, Finset.mem_univ, true_and, Finset.mem_insert]

Goal state after:
case read
q' : Λ'
q : Option Γ' → Λ'
q_ih : ∀ (a : Option Γ'), q' ∈ trStmts₁ (q a) → trStmts₁ q' ⊆ trStmts₁ (q a)
s : Option Γ'
h : q' ∈ trStmts₁ (q s)
x : Λ'
h' : x ∈ trStmts₁ q'
⊢ x = Λ'.read q ∨ ∃ a, x ∈ trStmts₁ (q a)
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case cons₂
S : Finset Λ'
k : Cont'
IH : contSupp k ⊆ S → Supports (contSupp k) S
H : contSupp k.cons₂ ⊆ S
⊢ Supports (contSupp k.cons₂) S

Tactic:
| cons₂ k IH =>

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

Goal state before:
pp: S : Profinite
F : Profiniteᵒᵖ ⥤ Type (u + 1)
hF : (S : Profinite) → IsColimit (F.mapCocone S.asLimitCone.op)
X✝ Y✝ : Profiniteᵒᵖ
x✝ : X✝ ⟶ Y✝
⊢ (lanPresheaf F).map x✝ ≫
      (match Y✝ with
        | Opposite.op S => lanPresheafIso (hF S)).hom =
    (match X✝ with
        | Opposite.op S => lanPresheafIso (hF S)).hom ≫
      F.map x✝

Tactic:
simpa using colimit.hom_ext fun _ ↦ (by simp)

Goal state after:
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
f : β → F γ
g : α → β
x : t α
⊢ traverse f ((Id.run ∘ traverse (pure ∘ g)) x) = traverse (f ∘ g) x

Tactic:
refine (comp_traverse (G := Id) f (pure ∘ g) x).symm.trans ?_

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
f : β → F γ
g : α → β
x : t α
⊢ traverse (Comp.mk ∘ map f ∘ pure ∘ g) x = traverse (f ∘ g) x
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: α' β' : Type u
f : α' → Set β'
a : α'
as : List α'
b : β'
bs : List β'
⊢ b :: bs ∈ traverse f (a :: as) ↔ Forall₂ (fun b a ↦ b ∈ f a) (b :: bs) (a :: as)

Tactic:
simp [mem_traverse as bs]

Goal state after:
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 = ωSup (approxChain { toFun := g, monotone' := ⋯ })

Tactic:
rw [← fix_eq_ωSup]

Goal state after:
α : Type u_1
β : α → Type u_2
g : ((a : α) → Part (β a)) → (a : α) → Part (β a)
hc : ωScottContinuous g
⊢ Part.fix g = Part.fix ⇑{ toFun := g, monotone' := ⋯ }
Module: Mathlib.Data.DFinsupp.Interval

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
t : (i : ι) → Finset (α i)
inst✝ : (i : ι) → DecidableEq (α i)
f : (a : ι) → a ∈ s → α a
hf : f ∈ s.pi t
i : ι
hi : i ∈ s
⊢ (DFinsupp.mk s fun i ↦ f ↑i ⋯) i = f i hi

Tactic:
exact mk_of_mem hi

Goal state after:
Module: Mathlib.Data.Bool.Count

Goal state before:
pp: l : List Bool
hl : IsChain (fun x1 x2 ↦ x1 ≠ x2) l
h2 : Even l.length
b : Bool
⊢ count (!b) l = count b l

Tactic:
rcases l with - | ⟨x, l⟩
  · rfl
  grind [count_cons_of_ne x.not_ne_self.symm, hl.count_not_cons]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : BoundedOrder α
n : ℕ
f : Fin (n + 1) → α
h0 : f 0 = ⊥
hlast : f (Fin.last n) = ⊤
hcovBy : ∀ (k : Fin n), f k.castSucc ⩿ f k.succ
⊢ IsMaxChain (fun x1 x2 ↦ x1 ≤ x2) (range f)

Tactic:
have hmono : Monotone f := Fin.monotone_iff_le_succ.2 fun k ↦ (hcovBy k).1
  refine ⟨hmono.isChain_range, fun t htc hbt ↦ hbt.antisymm fun x hx ↦ ?_⟩
  rw [mem_range]; by_contra! h
  suffices ∀ k, f k < x by simpa [hlast] using this (.last _)
  intro k
  induction k using Fin.induction with
  | zero => simpa [h0, bot_lt_iff_ne_bot] using (h 0).symm
  | succ k ihk =>
    rw [range_subset_iff] at hbt
    exact (htc.lt_of_le (hbt k.succ) hx (h _)).resolve_right ((hcovBy k).2 ihk)

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

Goal state before:
pp: case refine_3
S T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
inst✝ : Epi π
this✝ : CompactSpace ↑(S' ⇑(ConcreteCategory.hom π))
S'π : (n : ↑ℕ∪{∞}.toTop) →
  LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⟶ LightProfinite.fibre n (π ≫ snd S ℕ∪{∞}) :=
  fun n ↦ { hom := TopCat.ofHom { toFun := fun x ↦ ↑x n, continuous_toFun := ⋯ } }
y' : LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⟶ S :=
  ConcreteCategory.ofHom { toFun := y ⇑(ConcreteCategory.hom π), continuous_toFun := ⋯ }
π' : pullback π (y' ▷ ℕ∪{∞}) ⟶ LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⊗ ℕ∪{∞} := pullback.snd π (y' ▷ ℕ∪{∞})
σ' : ↑ℕ∪{∞}.toTop → ↑(LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))).toTop → ↑(pullback π (y' ▷ ℕ∪{∞})).toTop :=
  fun n ↦
    ⇑(ConcreteCategory.hom
        (pullback.lift π (y' ▷ ℕ∪{∞}) (S'π n ≫ LightProfinite.fibreIncl n (π ≫ snd S ℕ∪{∞}))
          (lift (𝟙 (LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))))
            (CompHausLike.const (LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))) n))
          ⋯))
hσ :
  ∀ (x : ↑ℕ∪{∞}.toTop) (s : ↑(LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))).toTop),
    ((ConcreteCategory.hom π') (σ' x s)).1 = s
hσ' :
  ∀ (x : ↑ℕ∪{∞}.toTop) (s : ↑(LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))).toTop),
    ((ConcreteCategory.hom π') (σ' x s)).2 = x
this : CompactSpace ↑(fibres (⇑(ConcreteCategory.hom π')) σ')
⊢ ({ hom := TopCat.ofHom { toFun := Subtype.val, continuous_toFun := ⋯ } } ≫ π') ≫ y' ▷ ℕ∪{∞} =
    ({ hom := TopCat.ofHom { toFun := Subtype.val, continuous_toFun := ⋯ } } ≫ pullback.fst π (y' ▷ ℕ∪{∞})) ≫ π

Tactic:
simp [π', pullback.condition]

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
c : Sigma β
l : List (Sigma β)
h : (c :: l).NodupKeys
⊢ { entries := c :: l, nodupKeys := h } = insert c.fst c.snd { entries := l, nodupKeys := ⋯ }

Tactic:
simpa [insert] using (kerase_of_notMem_keys <| notMem_keys_of_nodupKeys_cons h).symm

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ s₃ : Finmap β
h : s₁.Disjoint s₃
h' : s₂.Disjoint s₃
h'' : s₁ ∪ s₃ = s₂ ∪ s₃
x : α
this : lookup x (s₁ ∪ s₃) = lookup x (s₂ ∪ s₃)
hs₁ : x ∉ s₁
⊢ lookup x s₁ = lookup x s₂

Tactic:
by_cases hs₂ : x ∈ s₂
      · rwa [lookup_union_left_of_not_in (h' _ hs₂), lookup_union_left hs₂] at this
      · rw [lookup_eq_none.mpr hs₁, lookup_eq_none.mpr hs₂]

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a₁ a₂ : α
l : List (Sigma β)
h : a₁ ≠ a₂
p : a₁ ∈ l.keys
q : ¬a₂ ∈ l.keys
⊢ a₁ ∈ (kerase a₂ l).keys

Tactic:
by simp [q, p]

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
head✝ : Sigma β
l₁ : List (Sigma β)
l₂ : List (Sigma β)
h : ¬a ∈ (head✝ :: l₁).keys
⊢ kerase a (head✝ :: l₁ ++ l₂) = head✝ :: l₁ ++ kerase a l₂

Tactic:
simp only [keys_cons, mem_cons, not_or] at h

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
head✝ : Sigma β
l₁ : List (Sigma β)
l₂ : List (Sigma β)
h : ¬a = head✝.fst ∧ ¬a ∈ l₁.keys
⊢ kerase a (head✝ :: l₁ ++ l₂) = head✝ :: l₁ ++ kerase a l₂
Module: Mathlib.Data.Finsupp.Sigma

Goal state before:
pp: κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst✝ : Zero M
k k' : κ
f : ι k →₀ M
hk : k' ≠ k
⊢ f.embSigma.split k' = 0

Tactic:
ext i
  simp [split_apply, embSigma_apply_of_ne _ hk]

Goal state after:
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
ds₁ ds₂ ds₃ : List ℕ
inst✝ : Semigroup α
x : Holor α ds₁
y : Holor α ds₂
z : Holor α ds₃
⊢ x ⊗ y ⊗ z ≍ x ⊗ (y ⊗ z)

Tactic:
simp [cast_heq, mul_assoc0, assocLeft]

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
⊢ (∑ x_1 ∈ (Finset.range d).attach, if i = ↑x_1 then x.slice ↑x_1 ⋯ else 0) = x.slice i hid

Tactic:
rw [Finset.sum_eq_single (Subtype.mk i <| Finset.mem_range.2 hid)]

Goal state after:
α : Type
d : ℕ
ds : List ℕ
inst✝ : Semiring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
⊢ (if i = ↑⟨i, ⋯⟩ then x.slice ↑⟨i, ⋯⟩ ⋯ else 0) = x.slice i hid

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

case h₁
α : Type
d : ℕ
ds : List ℕ
inst✝ : Semiring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
⊢ ⟨i, ⋯⟩ ∉ (Finset.range d).attach → (if i = ↑⟨i, ⋯⟩ then x.slice ↑⟨i, ⋯⟩ ⋯ else 0) = 0
Module: Mathlib.Data.List.TakeWhile

Goal state before:
pp: case cons
α : Type u_1
p : α → Bool
l : List α
x hd : α
tl : List α
IH : x ∈ takeWhile p tl → p x = true
hx :
  x ∈
    match p hd with
    | true => hd :: takeWhile p tl
    | false => []
⊢ p x = true

Tactic:
cases hp : p hd

Goal state after:
case cons.false
α : Type u_1
p : α → Bool
l : List α
x hd : α
tl : List α
IH : x ∈ takeWhile p tl → p x = true
hx :
  x ∈
    match p hd with
    | true => hd :: takeWhile p tl
    | false => []
hp : p hd = false
⊢ p x = true

case cons.true
α : Type u_1
p : α → Bool
l : List α
x hd : α
tl : List α
IH : x ∈ takeWhile p tl → p x = true
hx :
  x ∈
    match p hd with
    | true => hd :: takeWhile p tl
    | false => []
hp : p hd = true
⊢ p x = true
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: n m : ℕ
⊢ (Ico n m).Nodup

Tactic:
dsimp [Ico]
  simp [nodup_range']

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

Goal state before:
pp: case cons
α : Type u_1
f : α → α
a head✝ : α
tl : List α
⊢ modifyLast.go f (tl ++ [a]) (#[].push head✝) = head✝ :: (tl ++ [f a])

pp: case cons.x_3
α : Type u_1
f : α → α
a head✝ : α
tl : List α
⊢ tl ++ [a] = [] → False

Tactic:
case x_3 => exact append_ne_nil_of_right_ne_nil tl (cons_ne_nil a [])

Goal state after:
case cons
α : Type u_1
f : α → α
a head✝ : α
tl : List α
⊢ modifyLast.go f (tl ++ [a]) (#[].push head✝) = head✝ :: (tl ++ [f a])
Module: Mathlib.Data.List.Palindrome

Goal state before:
pp: α : Type u_1
l : List α
⊢ ∀ (a : α) (l : List α) (b : α),
    (l.reverse = l → l.Palindrome) → (a :: (l ++ [b])).reverse = a :: (l ++ [b]) → (a :: (l ++ [b])).Palindrome

Tactic:
intro x l y hp hr

Goal state after:
α : Type u_1
l✝ : List α
x : α
l : List α
y : α
hp : l.reverse = l → l.Palindrome
hr : (x :: (l ++ [y])).reverse = x :: (l ++ [y])
⊢ (x :: (l ++ [y])).Palindrome
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst✝ : Semiring R
⊢ fromRows 0 0 = 0

Tactic:
ext (_ | _) _ <;> simp

Goal state after:
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
inst✝ : Star R
A₁ : Matrix m n₁ R
A₂ : Matrix m n₂ R
⊢ (A₁.fromCols A₂)ᴴ = A₁ᴴ.fromRows A₂ᴴ

Tactic:
ext (_ | _) _ <;> simp

Goal state after:
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
M N : Multiset α
⊢ M.OneStep N → M.IsDershowitzMannaLT N

Tactic:
rintro ⟨X, Y, a, M_def, N_def, ys_lt_a⟩

Goal state after:
α : Type u_1
inst✝ : Preorder α
M N X Y : Multiset α
a : α
M_def : M = X + Y
N_def : N = X + {a}
ys_lt_a : ∀ (y : α), y ∈ Y → y < a
⊢ M.IsDershowitzMannaLT N
Module: Mathlib.Data.Nat.Factorization.Root

Goal state before:
pp: case neg
n a : ℕ
h : ¬(n = 0 ∨ a = 0)
⊢ ((a.factorization ⌈/⌉ n).prod fun x1 x2 ↦ x1 ^ x2).factorization = a.factorization ⌈/⌉ n

Tactic:
refine prod_pow_factorization_eq_self fun p hp ↦ ?_

Goal state after:
case neg
n a : ℕ
h : ¬(n = 0 ∨ a = 0)
p : ℕ
hp : p ∈ (a.factorization ⌈/⌉ n).support
⊢ Prime p
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: n : ℕ
h : IsPrimePow n
ne_zero : (Icc 1 (n - 1)).gcd n.choose ≠ 0
isPrime : Nat.Prime n.minFac
⊢ ∀ x ∈ ((Icc 1 (n - 1)).gcd n.choose).primeFactors, x = n.minFac

Tactic:
intro p hp

Goal state after:
n : ℕ
h : IsPrimePow n
ne_zero : (Icc 1 (n - 1)).gcd n.choose ≠ 0
isPrime : Nat.Prime n.minFac
p : ℕ
hp : p ∈ ((Icc 1 (n - 1)).gcd n.choose).primeFactors
⊢ p = n.minFac
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
m n : ℕ
h0 : ∀ k < m, ¬p k
h : nth p n ≠ 0
⊢ nth (fun i ↦ p (i + m)) n = nth p n - m

Tactic:
by
  rw [← nth_add h0 h, Nat.add_sub_cancel]

Goal state after:
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: F : PFunctor.{uA, uB}
X : Type u_1
f : X → ↑F X
a : F.A
x : F.B a → F.M
i : F.B (M.mk ⟨a, x⟩).head
⊢ F.B (M.mk ⟨a, x⟩).head = F.B a

Tactic:
head_mk

Goal state after:
F : PFunctor.{uA, uB}
X : Type u_1
f : X → ↑F X
a : F.A
x : F.B a → F.M
i : F.B (M.mk ⟨a, x⟩).head
⊢ F.B ⟨a, x⟩.fst = F.B a
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
x : α
t : Ordnode α
⊢ Any (Eq x) t ↔ x ∈ t.toList

Tactic:
induction t

Goal state after:
case nil
α : Type u_1
x : α
⊢ Any (Eq x) nil ↔ x ∈ nil.toList

case node
α : Type u_1
x : α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
l_ih✝ : Any (Eq x) l✝ ↔ x ∈ l✝.toList
r_ih✝ : Any (Eq x) r✝ ↔ x ∈ r✝.toList
⊢ Any (Eq x) (node size✝ l✝ x✝ r✝) ↔ x ∈ (node size✝ l✝ x✝ r✝).toList
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
inst✝¹ : LE α
inst✝ : DecidableLE α
x : α
t : Ordnode α
h : t.Sized
h_mem : x ∈ t
⊢ 0 < t.size

Tactic:
by cases t; · { contradiction }; · { simp [h.1] }

Goal state after:
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: P : PFunctor.{uA, uB}
R : P.M → P.M → Prop
h : ∀ (x y : P.M), R x y → ∃ a f f', x.dest = ⟨a, f⟩ ∧ y.dest = ⟨a, f'⟩ ∧ ∀ (i : P.B a), R (f i) (f' i)
this : Inhabited P.A
⊢ IsBisimulation R

Tactic:
constructor <;> introv ih <;> rcases h _ _ ih with ⟨a'', g, g', h₀, h₁, h₂⟩ <;> clear h

Goal state after:
case head
P : PFunctor.{uA, uB}
R : P.M → P.M → Prop
this : Inhabited P.A
a a' : P.A
f : P.B a → P.M
f' : P.B a' → P.M
ih : R (M.mk ⟨a, f⟩) (M.mk ⟨a', f'⟩)
a'' : P.A
g g' : P.B a'' → P.M
h₀ : (M.mk ⟨a, f⟩).dest = ⟨a'', g⟩
h₁ : (M.mk ⟨a', f'⟩).dest = ⟨a'', g'⟩
h₂ : ∀ (i : P.B a''), R (g i) (g' i)
⊢ a = a'

case tail
P : PFunctor.{uA, uB}
R : P.M → P.M → Prop
this : Inhabited P.A
a : P.A
f f' : P.B a → P.M
ih : R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩)
i : P.B a
a'' : P.A
g g' : P.B a'' → P.M
h₀ : (M.mk ⟨a, f⟩).dest = ⟨a'', g⟩
h₁ : (M.mk ⟨a, f'⟩).dest = ⟨a'', g'⟩
h₂ : ∀ (i : P.B a''), R (g i) (g' i)
⊢ R (f i) (f' i)