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

Goal state before:
pp: case push
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 : σ → Γ k
⊢ ∃ L',
    (∀ (k_1 : K), ListBlank.map (proj k_1) L' = ListBlank.mk (List.map some (update S k (f v :: S k) k_1)).reverse) ∧
      TM1.stepAux q v
          (Tape.move Dir.right
            (Tape.write
              (((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom L))).head.1,
                update ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom L))).head.2 k (some (f v)))
              ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom L))))) =
        TM1.stepAux q v ((Tape.move Dir.right)^[(f v :: S k).length] (Tape.mk' ∅ (addBottom L')))

Tactic:
have := Tape.write_move_right_n fun a : Γ' K Γ ↦ (a.1, update a.2 k (some (f v)))
    refine
      ⟨_, fun k' ↦ ?_, by
        -- Porting note: `rw [...]` to `erw [...]; rfl`.
        -- https://github.com/leanprover-community/mathlib4/issues/5164
        rw [Tape.move_right_n_head, List.length, Tape.mk'_nth_nat, this]
        erw [addBottom_modifyNth fun a ↦ update a k (some (f v))]
        rw [Nat.add_one, iterate_succ']
        rfl⟩
    refine ListBlank.ext fun i ↦ ?_
    rw [ListBlank.nth_map, ListBlank.nth_modifyNth, proj, PointedMap.mk_val]
    by_cases h' : k' = k
    · subst k'
      split_ifs with h
        <;> simp only [List.reverse_cons, Function.update_self, ListBlank.nth_mk, List.map]
      · rw [List.getI_eq_getElem _, List.getElem_append_right] <;>
        simp only [List.length_append, List.length_reverse, List.length_map, ← h,
          Nat.sub_self, List.length_singleton, List.getElem_singleton,
          le_refl, Nat.lt_succ_self]
      rw [← proj_map_nth, hL, ListBlank.nth_mk]
      rcases lt_or_gt_of_ne h with h | h
      · rw [List.getI_append]
        simpa only [List.length_map, List.length_reverse] using h
      · rw [List.getI_eq_default, List.getI_eq_default] <;>
          simp only [Nat.add_one_le_iff, h, List.length, le_of_lt, List.length_reverse,
            List.length_append, List.length_map]
    · split_ifs <;> rw [Function.update_of_ne h', ← proj_map_nth, hL]
      rw [Function.update_of_ne h']

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

Goal state before:
pp: case e_a
c : Code
h : c.Ok
v✝ v : List ℕ
⊢ StateTransition.eval step (Cfg.ret Cont.halt v) = pure (Cfg.halt v)

Tactic:
exact Part.eq_some_iff.2 (mem_eval.2 ⟨ReflTransGen.single rfl, rfl⟩)

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

Goal state before:
pp: case neg
f : Code
k : Cont
v✝ : List ℕ
fok : f.Ok
x c : Cfg
he✝ : x ∈ eval step c
v v' : List ℕ
IH :
  ∀ (a' : Cfg),
    step (stepRet (Cont.fix f k) v') = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = 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₂)
hr : Reaches step (stepNormal f Cont.halt v) (Cfg.halt v')
h₁ : v' ∈ f.eval v
h₂✝ : Cfg.halt v' ∈ eval step (Cfg.ret Cont.halt v')
h₂ : Cfg.halt v' ∈ eval step (stepRet Cont.halt v')
he : ¬v'.headI = 0
h : x ∈ eval step (stepNormal f (Cont.fix f k) v'.tail)
k₀ : Cont
v₀ : List ℕ
e₀ : stepNormal f Cont.halt v'.tail = Cfg.ret k₀ v₀
e₁ : stepNormal f (Cont.fix f k) v'.tail = Cfg.ret (k₀.then (Cont.fix f k)) v₀
v₁ : List ℕ
hv₁ : v₁ ∈ f.eval v'.tail
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₂ = if v₁.headI = 0 then Sum.inl v₁.tail else Sum.inr v₁.tail) ∨
    ∃ a',
      (Sum.inr a' = if v₁.headI = 0 then Sum.inl v₁.tail else Sum.inr v₁.tail) ∧
        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'

Tactic:
split_ifs at hv₂ ⊢ <;> [exact Or.inl (congr_arg Sum.inl (Part.mem_some_iff.1 hv₂));
          exact Or.inr ⟨_, rfl, hv₂⟩]

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

Goal state before:
pp: case mp
H : Type u_3
inst✝² : TopologicalSpace H
inst✝¹ : LocallyCompactSpace H
inst✝ : T2Space H
⊢ TotallyDisconnectedSpace H → TotallySeparatedSpace H

pp: case mpr
H : Type u_3
inst✝² : TopologicalSpace H
inst✝¹ : LocallyCompactSpace H
inst✝ : T2Space H
⊢ TotallySeparatedSpace H → TotallyDisconnectedSpace H

Tactic:
· intro h
    exact totallySeparatedSpace_of_t0_of_basis_clopen loc_compact_Haus_tot_disc_of_zero_dim

Goal state after:
case mpr
H : Type u_3
inst✝² : TopologicalSpace H
inst✝¹ : LocallyCompactSpace H
inst✝ : T2Space H
⊢ TotallySeparatedSpace H → TotallyDisconnectedSpace H
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 Λ
inst✝ : Inhabited σ
k : K
L : List (Γ k)
L₁ : ListBlank (Γ' K Γ)
L₂ : List (Γ k)
H₁ : L₁ ∈ TM1.eval (tr M) (trInit k L)
H₂ : L₂ ∈ TM2.eval M k L
⊢ ∃ S L',
    addBottom L' = L₁ ∧ (∀ (k : K), ListBlank.map (proj k) L' = ListBlank.mk (List.map some (S k)).reverse) ∧ S k = L₂

Tactic:
by
  obtain ⟨c₁, h₁, rfl⟩ := (Part.mem_map_iff _).1 H₁
  obtain ⟨c₂, h₂, rfl⟩ := (Part.mem_map_iff _).1 H₂
  obtain ⟨_, ⟨L', hT⟩, h₃⟩ := StateTransition.tr_eval (tr_respects M) (trCfg_init k L) h₂
  cases Part.mem_unique h₁ h₃
  exact ⟨_, L', by simp only [Tape.mk'_right₀], hT, rfl⟩

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

Goal state before:
pp: α : Type
inst✝ : Finite α
B : Profinite
X : α → Profinite
π : (a : α) → X a ⟶ B
tfae_2_to_1 : Epi (Sigma.desc π) → EffectiveEpiFamily X π
tfae_1_to_2 : EffectiveEpiFamily X π → Epi (Sigma.desc π)
⊢ (∀ (b : ↑B.toTop), ∃ a x, (ConcreteCategory.hom (π a)) x = b) ↔ EffectiveEpiFamily X π

Tactic:
((CompHaus.effectiveEpiFamily_tfae
      (fun a ↦ profiniteToCompHaus.obj (X a)) (fun a ↦ profiniteToCompHaus.map (π a))).out 2 0 :)

Goal state after:
α : Type
inst✝ : Finite α
B : Profinite
X : α → Profinite
π : (a : α) → X a ⟶ B
tfae_2_to_1 : Epi (Sigma.desc π) → EffectiveEpiFamily X π
tfae_1_to_2 : EffectiveEpiFamily X π → Epi (Sigma.desc π)
⊢ (EffectiveEpiFamily (fun a ↦ profiniteToCompHaus.obj (X a)) fun a ↦ profiniteToCompHaus.map (π a)) ↔
    EffectiveEpiFamily X π
Module: Mathlib.Topology.Separation.Profinite

Goal state before:
pp: case h_option.refine_5
X : Type u_4
I✝ : Type u_5
inst✝⁵ : TopologicalSpace X
inst✝⁴ : CompactSpace X
inst✝³ : T2Space X
inst✝² : TotallyDisconnectedSpace X
inst✝¹ : Finite I✝
I : Type u_5
inst✝ : Fintype I
IH :
  ∀ {Z D : I → Set X},
    (∀ (i : I), IsClosed[inst✝⁵] (Z i)) →
      (∀ (i : I), IsClopen (D i)) →
        (∀ (i : I), Z i ⊆ D i) →
          univ.PairwiseDisjoint Z →
            ∃ C,
              (∀ (i : I), IsClopen (C i)) ∧
                (∀ (i : I), Z i ⊆ C i) ∧ (∀ (i : I), C i ⊆ D i) ∧ ⋃ i, D i ⊆ ⋃ i, C i ∧ univ.PairwiseDisjoint C
Z D : Option I → Set X
Z_closed : ∀ (i : Option I), IsClosed[inst✝⁵] (Z i)
D_clopen : ∀ (i : Option I), IsClopen (D i)
Z_subset_D : ∀ (i : Option I), Z i ⊆ D i
Z_disj : univ.PairwiseDisjoint Z
Z' : I → Set X := fun i ↦ Z (some i)
Z'_closed : ∀ (i : I), IsClosed[inst✝⁵] (Z (some i))
Z'_disj : univ.PairwiseDisjoint (Z ∘ some)
U : Set X := D none \ ⋃ i, Z (some i)
U_open : IsOpen[inst✝⁵] U
Z0_subset_U : Z none ⊆ U
V : Set X
V_clopen : IsClopen V
Z0_subset_V : Z none ⊆ V
V_subset_U : V ⊆ U
V_subset_D0 : V ⊆ D none
D' : I → Set X := fun i ↦ D (some i) \ V
D'_clopen : ∀ (i : I), IsClopen (D' i)
Z'_subset_D' : ∀ (i : I), Z' i ⊆ D' i
C' : I → Set X
C'_clopen : ∀ (i : I), IsClopen (C' i)
Z'_subset_C' : ∀ (i : I), Z (some i) ⊆ C' i
C'_subset_D' : ∀ (i : I), C' i ⊆ D' i
C'_cover_D' : ⋃ i, D' i ⊆ ⋃ i, C' i
C'_disj : univ.PairwiseDisjoint C'
C0 : Set X := D none \ ⋃ i, C' i
this✝ : IsClopen C0
this : Z none ⊆ C0
C : Option I → Set X := fun i ↦ Option.casesOn i C0 C'
⊢ univ.PairwiseDisjoint C

Tactic:
rw [Set.pairwiseDisjoint_iff]
      rintro (_ | i) _ (_ | j) _
      · simp
      · simpa [C, C0, Set.not_nonempty_iff_eq_empty, ← Set.disjoint_iff_inter_eq_empty] using
          Disjoint.mono_right (subset_iUnion C' j) disjoint_sdiff_left
      · simpa [C, C0, Set.not_nonempty_iff_eq_empty, ← Set.disjoint_iff_inter_eq_empty] using
          Disjoint.mono_left (subset_iUnion C' i) disjoint_sdiff_right
      · simpa using (Set.pairwiseDisjoint_iff.mp C'_disj) (by trivial) (by trivial)

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

Goal state before:
pp: case pred
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 (insert (q₁.pred q₂) (insert (unrev q₂) (trStmts₁ q₁ ∪ trStmts₁ q₂))) S

Tactic:
refine -- pred
      supports_insert.2 ⟨⟨fun _ => h₁, fun _ => h₂.2 _ (Or.inl W),
                          fun _ => h₂.1, fun _ => h₂.1⟩, ?_⟩

Goal state after:
case pred
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 (insert (unrev q₂) (trStmts₁ q₁ ∪ trStmts₁ q₂)) S
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case succ
S : Finset Λ'
k : Cont'
Hk : codeSupp Code.succ k ⊆ S
⊢ ∀ (s : Option Γ'),
    Λ'.Supports S
      ((if s = some Γ'.consₗ then id else Λ'.clear (fun x ↦ decide (x = Γ'.consₗ)) main) (unrev (Λ'.ret k).succ))

Tactic:
intro; split_ifs <;> exact Finset.union_subset_right Hk

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
⊢ Λ'.Supports S (trNormal f (Cont'.fix f k))

Tactic:
apply IHf; rw [codeSupp_fix] at Hk; exact Finset.union_subset_right Hk

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

Goal state before:
pp: case cons₁
S : Finset Λ'
f : Code
k : Cont'
IH : contSupp k ⊆ S → Supports (contSupp k) S
H : contSupp (Cont'.cons₁ f k) ⊆ S
H₁ :
  trStmts₁
        (move₂ (fun x ↦ false) main aux
          (move₂ (fun s ↦ decide (s = Γ'.consₗ)) stack main (move₂ (fun x ↦ false) aux stack (trNormal f k.cons₂)))) ∪
      codeSupp f k.cons₂ ⊆
    S
⊢ Supports (contSupp (Cont'.cons₁ f k)) S

Tactic:
have H₂ := Finset.union_subset_right H₁

Goal state after:
case cons₁
S : Finset Λ'
f : Code
k : Cont'
IH : contSupp k ⊆ S → Supports (contSupp k) S
H : contSupp (Cont'.cons₁ f k) ⊆ S
H₁ :
  trStmts₁
        (move₂ (fun x ↦ false) main aux
          (move₂ (fun s ↦ decide (s = Γ'.consₗ)) stack main (move₂ (fun x ↦ false) aux stack (trNormal f k.cons₂)))) ∪
      codeSupp f k.cons₂ ⊆
    S
H₂ : codeSupp f k.cons₂ ⊆ S
⊢ Supports (contSupp (Cont'.cons₁ f k)) S
Module: Mathlib.Topology.LocallyConstant.Algebra

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
α : Type u_3
R✝ : Type u_4
R : Type u_5
inst✝² : CommSemiring R
inst✝¹ : Semiring Y
inst✝ : Algebra R Y
⊢ ∀ (r : R) (x : LocallyConstant X Y),
    (constRingHom.comp (algebraMap R Y)) r * x = x * (constRingHom.comp (algebraMap R Y)) r

Tactic:
intros
    ext
    exact Algebra.commutes' _ _

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

Goal state before:
pp: F : Profiniteᵒᵖ ⥤ Type (u + 1)
hF : (S : Profinite) → IsColimit (F.mapCocone S.asLimitCone.op)
S : Profiniteᵒᵖ
⊢ (lanPresheafNatIso hF).hom.app S =
    colimit.desc (CostructuredArrow.proj toProfinite.op (Opposite.op (Opposite.unop S)) ⋙ toProfinite.op ⋙ F)
      (Profinite.Extend.cocone F (Opposite.unop S))

Tactic:
simp [lanPresheafNatIso]

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

Goal state before:
pp: S : Profinite
F : Profiniteᵒᵖ ⥤ Type (u + 1)
X : Type (u + 1)
⊢ Presheaf.IsSheaf (coherentTopology Profinite) (lanPresheaf (locallyConstantPresheaf X))

Tactic:
rw [Presheaf.isSheaf_of_iso_iff (lanPresheafNatIso
      fun _ ↦ isColimitLocallyConstantPresheafDiagram _ _)]
    exact ((CompHausLike.LocallyConstant.functor.{u, u + 1}
      (hs := fun _ _ _ ↦ ((Profinite.effectiveEpi_tfae _).out 0 2).mp)).obj X).property

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

Goal state before:
pp: F : LightProfiniteᵒᵖ ⥤ Type u
hF : (S : LightProfinite) → IsColimit (F.mapCocone (coconeRightOpOfCone S.asLimitCone))
S : LightProfiniteᵒᵖ
⊢ (lanPresheafNatIso hF).hom.app S =
    colimit.desc (CostructuredArrow.proj toLightProfinite.op (Opposite.op (Opposite.unop S)) ⋙ toLightProfinite.op ⋙ F)
      (LightProfinite.Extend.cocone F (Opposite.unop S))

Tactic:
simp [lanPresheafNatIso]

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

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

Tactic:
cases x <;> simp [Sum.traverse, functor_norm] <;> congr

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
β : (v : TypeVec.{?u.4} 0) → (v' : TypeVec.{?u.7} 0) → v ⟹ v' → Sort u_1
f : β Fin2.elim0 Fin2.elim0 nilFun
v : TypeVec.{?u.4} 0
v' : TypeVec.{?u.7} 0
fs : v ⟹ v'
i : Fin2 0
⊢ v i = i.elim0

Tactic:
contradiction

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
β : (v : TypeVec.{?u.4} 0) → (v' : TypeVec.{?u.7} 0) → v ⟹ v' → Sort u_1
f : β Fin2.elim0 Fin2.elim0 nilFun
v : TypeVec.{?u.4} 0
v' : TypeVec.{?u.7} 0
fs : v ⟹ v'
eq₁ : v = Fin2.elim0
i : Fin2 0
⊢ v' i = i.elim0

Tactic:
contradiction

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
β : (v : TypeVec.{?u.4} 0) → (v' : TypeVec.{?u.7} 0) → v ⟹ v' → Sort u_1
f : β Fin2.elim0 Fin2.elim0 nilFun
v : TypeVec.{?u.4} 0
v' : TypeVec.{?u.7} 0
fs : v ⟹ v'
eq₁ : v = Fin2.elim0
eq₂ : v' = Fin2.elim0
i : Fin2 0
⊢ fs i = nilFun i

Tactic:
contradiction

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n✝ : ℕ
α✝ β✝ : TypeVec.{u} n✝
⊢ (id ⊗' id) = id

Tactic:
ext i a

Goal state after:
n✝ : ℕ
α✝ β✝ : TypeVec.{u} n✝
i : Fin2 n✝
a : (α✝ ⊗ β✝) i
⊢ (id ⊗' id) i a = id i a
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:
by
  rw [← fix_eq_ωSup]
  rfl

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
α α' β β' : TypeVec.{u} n
φ φ' ψ ψ' : Type u
f₀ : α ⟹ α'
g₀ : β ⟹ β'
f₁ : φ → φ'
g₁ : ψ → ψ'
⊢ (f₀ ⊗' g₀ ::: Prod.map f₁ g₁) = ((f₀ ::: f₁) ⊗' (g₀ ::: g₁))

Tactic:
ext i a

Goal state after:
n : ℕ
α α' β β' : TypeVec.{u} n
φ φ' ψ ψ' : Type u
f₀ : α ⟹ α'
g₀ : β ⟹ β'
f₁ : φ → φ'
g₁ : ψ → ψ'
i : Fin2 (n + 1)
a : ((α ⊗ β) ::: (φ × ψ)) i
⊢ (f₀ ⊗' g₀ ::: Prod.map f₁ g₁) i a = ((f₀ ::: f₁) ⊗' (g₀ ::: g₁)) i a
Module: Mathlib.Data.BitVec

Goal state before:
pp: w : ℕ
z : ℤ
⊢ (↑z).toFin = ↑z

Tactic:
rw [← ofFin_intCast]

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

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

Tactic:
exact h'

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

Goal state before:
pp: case pos
α : Type u
α' : Type u'
β : α → Type v
β' : α' → Type v'
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f : α → α'
hf : Function.Injective f
g : (a : α) → β a → β' (f a)
a : α
s : Sigma β
tail✝ : List (Sigma β)
tail_ih✝ : dlookup (f a) (map (Sigma.map f g) tail✝) = Option.map (g a) (dlookup a tail✝)
this : a ≠ s.fst → ¬f a = ⟨f s.fst, g s.fst s.snd⟩.fst
h✝ : a = s.fst
⊢ dlookup (f a) (map (Sigma.map f g) (s :: tail✝)) = Option.map (g a) (dlookup a (s :: tail✝))

Tactic:
grind [Sigma.map]

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

Goal state before:
pp: case neg
α : Type u
α' : Type u'
β : α → Type v
β' : α' → Type v'
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f : α → α'
hf : Function.Injective f
g : (a : α) → β a → β' (f a)
a : α
s : Sigma β
tail✝ : List (Sigma β)
tail_ih✝ : dlookup (f a) (map (Sigma.map f g) tail✝) = Option.map (g a) (dlookup a tail✝)
this : a ≠ s.fst → ¬f a = ⟨f s.fst, g s.fst s.snd⟩.fst
h✝ : ¬a = s.fst
⊢ dlookup (f a) (map (Sigma.map f g) (s :: tail✝)) = Option.map (g a) (dlookup a (s :: tail✝))

Tactic:
grind [Sigma.map]

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

Goal state before:
pp: case nil
α : Type u
β : α → Type u_1
β' : α → Type u_2
f : (a : α) → β a → β' a
⊢ (map (Sigma.map id f) []).keys = [].keys

Tactic:
grind [Sigma.map]

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

Goal state before:
pp: case cons
α : Type u
β : α → Type u_1
β' : α → Type u_2
f : (a : α) → β a → β' a
head✝ : (a : α) × β a
tail✝ : List ((a : α) × β a)
tail_ih✝ : (map (Sigma.map id f) tail✝).keys = tail✝.keys
⊢ (map (Sigma.map id f) (head✝ :: tail✝)).keys = (head✝ :: tail✝).keys

Tactic:
grind [Sigma.map]

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁✝ s₂✝ : Finmap β
s₁ s₂ : AList β
h : ∀ (x : α), dlookup x s₁.entries = dlookup x s₂.entries
⊢ ⟦s₁⟧ = ⟦s₂⟧

Tactic:
AList.toFinmap_eq

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁✝ s₂✝ : Finmap β
s₁ s₂ : AList β
h : ∀ (x : α), dlookup x s₁.entries = dlookup x s₂.entries
⊢ s₁.entries ~ s₂.entries
Module: Mathlib.Data.Finmap

Goal state before:
pp: case fst
α : Type u
β : α → Type v
inst✝ : DecidableEq α
x✝ : { f // ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1 }
s : Finset α
f : (a : α) → Option (β a)
hf : ∀ (i : α), (f i).isSome = true ↔ i ∈ s
a✝ : α
⊢ a✝ ∈
      (↑((fun s ↦ ⟨(s.keys, fun i ↦ lookup i s), ⋯⟩)
            ((fun f ↦ { entries := ((↑f).1.sigma fun i ↦ ((↑f).2 i).toFinset).val, nodupKeys := ⋯ }) ⟨(s, f), hf⟩))).1 ↔
    a✝ ∈ (↑⟨(s, f), hf⟩).1

pp: case snd
α : Type u
β : α → Type v
inst✝ : DecidableEq α
x✝¹ : { f // ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1 }
s : Finset α
f : (a : α) → Option (β a)
hf : ∀ (i : α), (f i).isSome = true ↔ i ∈ s
x✝ : α
a✝ : β x✝
⊢ (↑((fun s ↦ ⟨(s.keys, fun i ↦ lookup i s), ⋯⟩)
              ((fun f ↦ { entries := ((↑f).1.sigma fun i ↦ ((↑f).2 i).toFinset).val, nodupKeys := ⋯ }) ⟨(s, f), hf⟩))).2
        x✝ =
      some a✝ ↔
    (↑⟨(s, f), hf⟩).2 x✝ = some a✝

Tactic:
· simp [keys, Multiset.keys, ← hf, Option.isSome_iff_exists]

Goal state after:
case snd
α : Type u
β : α → Type v
inst✝ : DecidableEq α
x✝¹ : { f // ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1 }
s : Finset α
f : (a : α) → Option (β a)
hf : ∀ (i : α), (f i).isSome = true ↔ i ∈ s
x✝ : α
a✝ : β x✝
⊢ (↑((fun s ↦ ⟨(s.keys, fun i ↦ lookup i s), ⋯⟩)
              ((fun f ↦ { entries := ((↑f).1.sigma fun i ↦ ((↑f).2 i).toFinset).val, nodupKeys := ⋯ }) ⟨(s, f), hf⟩))).2
        x✝ =
      some a✝ ↔
    (↑⟨(s, f), hf⟩).2 x✝ = some a✝
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l₁ l₂ : List (Sigma β)
nd : l₁.NodupKeys
⊢ Pairwise
    (fun a_1 b_1 ↦
      ∀ (c : Sigma β),
        (c ∈ if a = a_1.fst then some ⟨a, b⟩ else none) →
          ∀ (d : Sigma β), (d ∈ if a = b_1.fst then some ⟨a, b⟩ else none) → a_1 = b_1 ∧ c = d)
    l₁

Tactic:
refine nd.pairwise_ne.imp ?_

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l₁ l₂ : List (Sigma β)
nd : l₁.NodupKeys
⊢ ∀ {a_1 b_1 : Sigma β},
    a_1.fst ≠ b_1.fst →
      ∀ (c : Sigma β),
        (c ∈ if a = a_1.fst then some ⟨a, b⟩ else none) →
          ∀ (d : Sigma β), (d ∈ if a = b_1.fst then some ⟨a, b⟩ else none) → a_1 = b_1 ∧ c = d
Module: Mathlib.Data.Finset.Functor

Goal state before:
pp: α✝ β✝ : Type u
inst✝ : (P : Prop) → Decidable P
α β : Type u_1
⊢ Functor.mapConst = Functor.map ∘ const β

Tactic:
simp only [Functor.mapConst, Functor.map]

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

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

Tactic:
rcases n with n | n

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

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

Goal state before:
pp: case negSucc
n : ℤ
m : ℕ
⊢ (-[m+1] + n).bodd = (-[m+1].bodd ^^ n.bodd)

Tactic:
rcases n with n | n

Goal state after:
case negSucc.ofNat
m n : ℕ
⊢ (-[m+1] + ofNat n).bodd = (-[m+1].bodd ^^ (ofNat n).bodd)

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

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

Tactic:
rcases n with n | n

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

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

Goal state before:
pp: case negSucc
n : ℤ
m : ℕ
⊢ (-[m+1] * n).bodd = (-[m+1].bodd && n.bodd)

Tactic:
rcases n with n | n

Goal state after:
case negSucc.ofNat
m n : ℕ
⊢ (-[m+1] * ofNat n).bodd = (-[m+1].bodd && (ofNat n).bodd)

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

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

Tactic:
rcases n with n | n

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

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

Goal state before:
pp: case negSucc
n : ℤ
m : ℕ
⊢ bitwise or -[m+1] n = -[m+1].lor n

Tactic:
rcases n with n | n

Goal state after:
case negSucc.ofNat
m n : ℕ
⊢ bitwise or -[m+1] (ofNat n) = -[m+1].lor (ofNat n)

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

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

Tactic:
rcases n with n | n

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

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

Goal state before:
pp: case negSucc
n : ℤ
m : ℕ
⊢ bitwise and -[m+1] n = -[m+1].land n

Tactic:
rcases n with n | n

Goal state after:
case negSucc.ofNat
m n : ℕ
⊢ bitwise and -[m+1] (ofNat n) = -[m+1].land (ofNat n)

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

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

Tactic:
rcases n with n | n

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

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

Goal state before:
pp: case negSucc
n : ℤ
m : ℕ
⊢ bitwise (fun a b ↦ a && !b) -[m+1] n = -[m+1].ldiff n

Tactic:
rcases n with n | n

Goal state after:
case negSucc.ofNat
m n : ℕ
⊢ bitwise (fun a b ↦ a && !b) -[m+1] (ofNat n) = -[m+1].ldiff (ofNat n)

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