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

Goal state before:
pp: case pos
f : Code
k : Cont
IH :
  ∀ (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepRet k v) b₂ ∧
        Reaches₁ (TM2.step tr) { l := some (Λ'.ret (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) }
          b₂
v : List ℕ
s : Option Γ'
h : v.headI = 0
this : natEnd ((trList v).head?.getD default) = true ∧ (trList v).tail = trList v.tail
c : Cfg'
h₁ : TrCfg (stepRet k v.tail) c
h₂ :
  Reaches₁ (TM2.step tr)
    { l := some (Λ'.ret (trCont k)), var := (trList v).head?, stk := elim (trList v.tail) [] [] (trContStack k) } c
⊢ TransGen (fun a b ↦ b ∈ TM2.step tr a)
    (TM2.stepAux
      (pop' main
        (goto fun s ↦
          bif natEnd (s.getD default) then Λ'.ret (trCont k)
          else Λ'.clear natEnd main (trNormal f (Cont'.fix f (trCont k)))))
      s (elim (trList v) [] [] (trContStack (Cont.fix f k))))
    c

Tactic:
simp only [pop', TM2.stepAux, elim_main, this, elim_update_main]

Goal state after:
case pos
f : Code
k : Cont
IH :
  ∀ (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepRet k v) b₂ ∧
        Reaches₁ (TM2.step tr) { l := some (Λ'.ret (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) }
          b₂
v : List ℕ
s : Option Γ'
h : v.headI = 0
this : natEnd ((trList v).head?.getD default) = true ∧ (trList v).tail = trList v.tail
c : Cfg'
h₁ : TrCfg (stepRet k v.tail) c
h₂ :
  Reaches₁ (TM2.step tr)
    { l := some (Λ'.ret (trCont k)), var := (trList v).head?, stk := elim (trList v.tail) [] [] (trContStack k) } c
⊢ TransGen (fun a b ↦ b ∈ TM2.step tr a)
    { l := some (bif true then Λ'.ret (trCont k) else Λ'.clear natEnd main (trNormal f (Cont'.fix f (trCont k)))),
      var := (trList v).head?, stk := elim (trList v.tail) [] [] (trContStack (Cont.fix f k)) }
    c
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
C : Set ((fun X ↦ ↑X.toTop) Y) := Set.range ⇑(ConcreteCategory.hom f)
hC : IsClosed C
U : Set ((fun X ↦ ↑X.toTop) Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ 𝓝 y
V : Set ↑Y.toTop
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
Z : LightProfinite := of (ULift.{u, 0} (Fin 2))
g : Y ⟶ Z :=
  ofHom (fun X ↦ TotallyDisconnectedSpace ↑X ∧ SecondCountableTopology ↑X)
    { toFun := ⇑(LocallyConstant.map ULift.up (LocallyConstant.ofIsClopen hV)), continuous_toFun := ⋯ }
h : Y ⟶ Z :=
  ofHom (fun X ↦ TotallyDisconnectedSpace ↑X ∧ SecondCountableTopology ↑X)
    { toFun := fun x ↦ { down := 1 }, continuous_toFun := ⋯ }
H : ((ConcreteCategory.hom h).toFun y).down = { down := if y ∈ V then 0 else 1 }.down
⊢ False

Tactic:
if_pos hyV

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)
hC : IsClosed C
U : Set ((fun X ↦ ↑X.toTop) Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ 𝓝 y
V : Set ↑Y.toTop
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
Z : LightProfinite := of (ULift.{u, 0} (Fin 2))
g : Y ⟶ Z :=
  ofHom (fun X ↦ TotallyDisconnectedSpace ↑X ∧ SecondCountableTopology ↑X)
    { toFun := ⇑(LocallyConstant.map ULift.up (LocallyConstant.ofIsClopen hV)), continuous_toFun := ⋯ }
h : Y ⟶ Z :=
  ofHom (fun X ↦ TotallyDisconnectedSpace ↑X ∧ SecondCountableTopology ↑X)
    { toFun := fun x ↦ { down := 1 }, continuous_toFun := ⋯ }
H : ((ConcreteCategory.hom h).toFun y).down = { down := 0 }.down
⊢ False
Module: Mathlib.Topology.Category.LightProfinite.AsLimit

Goal state before:
pp: S : LightProfinite
n m : ℕ
h : n ≤ m
⊢ ⇑(ConcreteCategory.hom (S.transitionMapLE h)) ∘ ⇑(ConcreteCategory.hom (S.proj m)) =
    ⇑(ConcreteCategory.hom (S.proj n))

Tactic:
rw [← S.proj_comp_transitionMapLE h]
  rfl

Goal state after:
Module: Mathlib.Condensed.EffectiveEpi

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

Tactic:
by
    rw [CondensedSet.epi_iff_locallySurjective_on_compHaus]
    intro S g
    refine ⟨pullback f g.down, pullback.snd _ _, fun y ↦ ?_, ⟨pullback.fst _ _⟩,
      ULift.ext _ _ <| pullback.condition _ _⟩
    rw [CompHaus.epi_iff_surjective] at hf
    obtain ⟨x, hx⟩ := hf (g.down.hom y)
    exact ⟨⟨⟨x, y⟩, hx⟩, rfl⟩

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

Goal state before:
pp: P : TopCat → Prop
R : Type u
inst✝ : Ring R
X✝ Y✝ : ModuleCat R
f : X✝ ⟶ Y✝
⊢ (functor R).map f ≫ (functorIsoDiscreteComponents R Y✝).symm.hom =
    (functorIsoDiscreteComponents R X✝).symm.hom ≫ (discrete (ModuleCat R)).map f

Tactic:
dsimp
    rw [Iso.eq_inv_comp, ← Category.assoc, Iso.comp_inv_eq]
    dsimp [functorIsoDiscreteComponents]
    rw [Category.assoc, ← Iso.eq_inv_comp,
      ← (discreteUnderlyingAdj (ModuleCat R)).counit_naturality]
    simp only [← assoc]
    congr 1
    rw [← Iso.comp_inv_eq]
    apply Sheaf.hom_ext
    simp [functorIsoDiscreteAux₂, ← Functor.map_comp]
    rfl

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

Goal state before:
pp: t : Type u → Type u
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α : Type u
η : ApplicativeTransformation F G
x : t (F α)
⊢ (fun {α} ↦ η.app α) (sequence x) = sequence ((fun {α} ↦ η.app α) <$> x)

Tactic:
by simp [sequence, naturality, traverse_map]

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

Goal state before:
pp: case binaturality
t : Type u → Type u → Type u
inst✝⁹ : Bitraversable t
F G : Type u → Type u
inst✝⁸ : Traversable F
inst✝⁷ : Traversable G
inst✝⁶ : LawfulTraversable F
inst✝⁵ : LawfulTraversable G
inst✝⁴ : LawfulBitraversable t
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
η✝ : ApplicativeTransformation F✝ G✝
α✝ α'✝ β✝ β'✝ : Type u
f✝ : α✝ → F✝ β✝
f'✝ : α'✝ → F✝ β'✝
x✝ : bicompl t F G α✝ α'✝
⊢ η✝.app (bicompl t F G β✝ β'✝) (bitraverse (traverse f✝) (traverse f'✝) x✝) =
    bitraverse (traverse (η✝.app β✝ ∘ f✝)) (traverse (η✝.app β'✝ ∘ f'✝)) x✝

Tactic:
· dsimp only [bicompl]
    simp [binaturality, naturality_pf]

Goal state after:
Module: Mathlib.Control.Fold

Goal state before:
pp: α β : Type u
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
m : Type u → Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m α
x : α
xs : t β
⊢ foldlm f x xs = unop ((foldlM.ofFreeMonoid f) (FreeMonoid.ofList (toList xs))) x

Tactic:
simp only [foldlm, toList_spec, foldMap_hom_free (foldlM.ofFreeMonoid f),
        foldlm.ofFreeMonoid_comp_of, foldlM.get, FreeMonoid.ofList_toList]

Goal state after:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: 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

Tactic:
have h₁ := Nat.find_spec h₀

Goal state after:
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
h₁ : (approx (⇑f) (Nat.find h₀) a).Dom
⊢ b ∈ approx (⇑f) (Nat.find h₀).succ a
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: r : Type u
m : Type u → Type v
α β : Type w
⊢ ∀ {α β : Type u_1} (x : α) (f : α → ContT r m β), pure x >>= f = f x

Tactic:
by intros; ext; rfl

Goal state after:
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: r : Type u
m : Type u → Type v
α β : Type w
⊢ ∀ {α β γ : Type u_1} (x : ContT r m α) (f : α → ContT r m β) (g : β → ContT r m γ),
    x >>= f >>= g = x >>= fun x ↦ f x >>= g

Tactic:
by intros; ext; rfl

Goal state after:
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: r : Type u
m : Type u → Type v
α β : Type w
⊢ ∀ {α ω γ : Type u_1} (cmd : ContT r m α) (next : Label ω (ContT r m) γ → α → ContT r m ω),
    (callCC fun f ↦ cmd >>= next f) = do
      let x ← cmd
      callCC fun f ↦ next f x

Tactic:
by intros; ext; rfl

Goal state after:
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: r : Type u
m : Type u → Type v
α β : Type w
⊢ ∀ {α : Type u_1} (β : Type u_1) (x : α) (dead : Label α (ContT r m) β → β → ContT r m α),
    (callCC fun f ↦ goto f x >>= dead f) = pure x

Tactic:
by intros; ext; rfl

Goal state after:
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: r : Type u
m : Type u → Type v
α β : Type w
⊢ ∀ {α β : Type u_1} (dummy : ContT r m α), (callCC fun x ↦ dummy) = dummy

Tactic:
by intros; ext; rfl

Goal state after:
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: m : Type u → Type v
inst✝² : Monad m
ε : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
x✝ : α✝
dead✝ : Label α✝ (ExceptT ε m) β✝ → β✝ → ExceptT ε m α✝
⊢ (callCC fun f ↦ goto f x✝ >>= dead✝ f) = pure x✝

Tactic:
simp only [callCC, ExceptT.callCC, ExceptT.goto_mkLabel, map_eq_bind_pure_comp, Function.comp,
      ExceptT.run_bind, ExceptT.run_mk, bind_assoc, pure_bind, @callCC_bind_left m _]

Goal state after:
m : Type u → Type v
inst✝² : Monad m
ε : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
x✝ : α✝
dead✝ : Label α✝ (ExceptT ε m) β✝ → β✝ → ExceptT ε m α✝
⊢ ExceptT.mk (pure (Except.ok x✝)) = pure x✝
Module: Mathlib.Data.TypeVec

Goal state before:
pp: α : TypeVec.{u_1} 0
⊢ α.repeatEq = nilFun

Tactic:
ext i

Goal state after:
α : TypeVec.{u_1} 0
i : Fin2 0
x✝ : (α ⊗ α) i
⊢ α.repeatEq i x✝ = nilFun i x✝
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
α : TypeVec.{u_1} n
i : Fin2 n
x : α i
p : Prop
⊢ ofRepeat (TypeVec.const p α i x) ↔ p

Tactic:
induction i with
  | fz => rfl
  | fs _ ih =>
    rw [TypeVec.const]
    exact ih

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

Goal state before:
pp: case none
S : Type u_1
T : Type u_2
X : Type u_3
π : T → S × Option X
hπ : Function.Surjective π
σ : Option X → S → T
hσ : ∀ (x : Option X) (s : S), (π (σ x s)).1 = s
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
s : S
y : T
hy : π y = (s, none)
⊢ ∃ a, (fun x ↦ π ↑x) a = (s, none)

Tactic:
exact ⟨⟨y, by grind⟩, hy⟩

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: case fs
n n✝ : ℕ
a✝ : Fin2 n✝
i_ih : ∀ {α : TypeVec.{u} n✝} (x : α a✝), (subtypeVal α.repeatEq ⊚ diagSub) a✝ x = prod.diag a✝ x
α : TypeVec.{u} (n✝ + 1)
x : α a✝.fs
⊢ (subtypeVal α.repeatEq ⊚ diagSub) a✝.fs x = prod.diag a✝.fs x

Tactic:
apply @i_ih (drop α)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f : Filter α
m : α → Filter β
F : f.Realizer
G : (i : α) → (m i).Realizer
x✝ : Set β
⊢ x✝ ∈
      {
            f := fun x ↦
              match x with
              | ⟨s, f_1⟩ => ⋃ i, ⋃ (h : i ∈ F.F.f s), (G i).F.f (f_1 i h),
            pt := ⟨F.F.pt, fun i x ↦ (G i).F.pt⟩,
            inf := fun x x_1 ↦
              match x with
              | ⟨a, f_1⟩ =>
                match x_1 with
                | ⟨b, f'⟩ => ⟨F.F.inf a b, fun i h ↦ (G i).F.inf (f_1 i ⋯) (f' i ⋯)⟩,
            inf_le_left := ⋯, inf_le_right := ⋯ }.toFilter.sets ↔
    x✝ ∈ (f.bind m).sets

Tactic:
obtain ⟨_, F, _⟩ := F; subst f
      simp only [CFilter.toFilter, iUnion_subset_iff, Sigma.exists, Filter.mem_sets, mem_bind]
      exact
        ⟨fun ⟨s, f, h⟩ ↦
          ⟨F s, ⟨s, Subset.refl _⟩, fun i H ↦ (G i).mem_sets.2 ⟨f i H, fun _ h' ↦ h i H h'⟩⟩,
          fun ⟨_, ⟨s, h⟩, f⟩ ↦
          let ⟨f', h'⟩ := Classical.axiom_of_choice fun i : F s ↦ (G i).mem_sets.1 (f i (h i.2))
          ⟨s, fun i h ↦ f' ⟨i, h⟩, fun _ H _ m ↦ h' ⟨_, H⟩ m⟩⟩

Goal state after:
Module: Mathlib.Data.DFinsupp.Interval

Goal state before:
pp: case refine_2
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
f : Π₀ (i : ι), α i
t : (i : ι) → Finset (α i)
inst✝ : (i : ι) → DecidableEq (α i)
h : f.support ⊆ s ∧ ∀ i ∈ s, f i ∈ t i
⊢ ({ toFun := fun f ↦ DFinsupp.mk s fun i ↦ f ↑i ⋯, inj' := ⋯ } fun i x ↦ f i) = f

Tactic:
ext i

Goal state after:
case refine_2
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
f : Π₀ (i : ι), α i
t : (i : ι) → Finset (α i)
inst✝ : (i : ι) → DecidableEq (α i)
h : f.support ⊆ s ∧ ∀ i ∈ s, f i ∈ t i
i : ι
⊢ ({ toFun := fun f ↦ DFinsupp.mk s fun i ↦ f ↑i ⋯, inj' := ⋯ } fun i x ↦ f i) i = f i
Module: Mathlib.Data.DFinsupp.Multiset

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
n : ℕ
⊢ toDFinsupp (replicate n a) = DFinsupp.single a n

Tactic:
ext i

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
n : ℕ
i : α
⊢ (toDFinsupp (replicate n a)) i = (DFinsupp.single a n) i
Module: Mathlib.Data.DFinsupp.Multiset

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ toDFinsupp (s ∩ t) = toDFinsupp s ⊓ toDFinsupp t

Tactic:
ext i

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
i : α
⊢ (toDFinsupp (s ∩ t)) i = (toDFinsupp s ⊓ toDFinsupp t) i
Module: Mathlib.Data.DFinsupp.Multiset

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ toDFinsupp (s ∪ t) = toDFinsupp s ⊔ toDFinsupp t

Tactic:
ext i

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
i : α
⊢ (toDFinsupp (s ∪ t)) i = (toDFinsupp s ⊔ toDFinsupp t) i
Module: Mathlib.Data.ENat.BigOperators

Goal state before:
pp: case singleton
α : Type u_1
s : Finset α
f g : α → ℕ∞
a✝ : α
Hlt : ∀ i ∈ {a✝}, f i < g i
⊢ ∑ i ∈ {a✝}, f i < ∑ i ∈ {a✝}, g i

Tactic:
| singleton =>

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

Goal state before:
pp: m : ℕ
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Fin m → α
⊢ Fintype.card ↑(Set.range f) ≤ m

Tactic:
by
  simpa using Fintype.card_range_le f

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

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

Tactic:
ext i

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

Goal state before:
pp: n : ℕ
α : Fin n → Sort u_1
v : (i : Fin n) → α i
⊢ take 0 ⋯ v = fun i ↦ i.elim0

Tactic:
ext i

Goal state after:
n : ℕ
α : Fin n → Sort u_1
v : (i : Fin n) → α i
i : Fin 0
⊢ take 0 ⋯ v i = i.elim0
Module: Mathlib.Data.Fin.Tuple.Take

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_2
v : (i : Fin (n + 1)) → α i
⊢ take 1 ⋯ v = fun i ↦ v (castLE ⋯ i)

Tactic:
ext i

Goal state after:
n : ℕ
α : Fin (n + 1) → Sort u_2
v : (i : Fin (n + 1)) → α i
i : Fin 1
⊢ take 1 ⋯ v i = v (castLE ⋯ i)
Module: Mathlib.Data.Fin.Tuple.Take

Goal state before:
pp: n : ℕ
α : Fin n → Sort u_1
v : (i : Fin n) → α i
⊢ take n ⋯ v = v

Tactic:
ext i

Goal state after:
n : ℕ
α : Fin n → Sort u_1
v : (i : Fin n) → α i
i : Fin n
⊢ take n ⋯ v i = v i
Module: Mathlib.Data.Fin.Tuple.Take

Goal state before:
pp: n : ℕ
α : Type u_2
n' m : ℕ
h : m ≤ n
a : Fin n' → α
⊢ take (m * n') ⋯ («repeat» n a) = «repeat» m a

Tactic:
ext i

Goal state after:
n : ℕ
α : Type u_2
n' m : ℕ
h : m ≤ n
a : Fin n' → α
i : Fin (m * n')
⊢ take (m * n') ⋯ («repeat» n a) i = «repeat» m a i
Module: Mathlib.Data.Fin.Tuple.Take

Goal state before:
pp: n : ℕ
α : Fin n → Sort u_1
m : ℕ
h : m < n
v : (i : Fin n) → α i
⊢ take m.succ h v = snoc (take m ⋯ v) (v ⟨m, h⟩)

Tactic:
ext i

Goal state after:
n : ℕ
α : Fin n → Sort u_1
m : ℕ
h : m < n
v : (i : Fin n) → α i
i : Fin m.succ
⊢ take m.succ h v i = snoc (take m ⋯ v) (v ⟨m, h⟩) i
Module: Mathlib.Data.Fin.Tuple.Take

Goal state before:
pp: n n' : ℕ
motive : Fin (n + n') → Sort u_2
m : ℕ
h : m ≤ n
u : (i : Fin n) → motive (castAdd n' i)
v : (i : Fin n') → motive (natAdd n i)
⊢ (take m ⋯ fun i ↦ addCases u v i) = take m h u

Tactic:
ext i

Goal state after:
n n' : ℕ
motive : Fin (n + n') → Sort u_2
m : ℕ
h : m ≤ n
u : (i : Fin n) → motive (castAdd n' i)
v : (i : Fin n') → motive (natAdd n i)
i : Fin m
⊢ take m ⋯ (fun i ↦ addCases u v i) i = take m h u i
Module: Mathlib.Data.Fin.Tuple.Take

Goal state before:
pp: n n' : ℕ
motive : Fin (n + n') → Sort u_2
m : ℕ
h : m ≤ n'
u : (i : Fin n) → motive (castAdd n' i)
v : (i : Fin n') → motive (natAdd n i)
⊢ (take (n + m) ⋯ fun i ↦ addCases u v i) = fun i ↦ addCases u (take m h v) i

Tactic:
ext i

Goal state after:
n n' : ℕ
motive : Fin (n + n') → Sort u_2
m : ℕ
h : m ≤ n'
u : (i : Fin n) → motive (castAdd n' i)
v : (i : Fin n') → motive (natAdd n i)
i : Fin (n + m)
⊢ take (n + m) ⋯ (fun i ↦ addCases u v i) i = addCases u (take m h v) i
Module: Mathlib.Data.Fin.Tuple.Take

Goal state before:
pp: α : Type u_2
m : ℕ
l : List α
h : m ≤ l.length
⊢ (List.take m l).get = take m h l.get ∘ Fin.cast ⋯

Tactic:
ext i

Goal state after:
α : Type u_2
m : ℕ
l : List α
h : m ≤ l.length
i : Fin (List.take m l).length
⊢ (List.take m l).get i = (take m h l.get ∘ Fin.cast ⋯) i
Module: Mathlib.Data.Fin.Tuple.Take

Goal state before:
pp: n : ℕ
α : Type u_2
m : ℕ
v : Fin n → α
h : m ≤ n
⊢ (List.take m (List.ofFn v)).get = take m h v ∘ Fin.cast ⋯

Tactic:
ext i

Goal state after:
n : ℕ
α : Type u_2
m : ℕ
v : Fin n → α
h : m ≤ n
i : Fin (List.take m (List.ofFn v)).length
⊢ (List.take m (List.ofFn v)).get i = (take m h v ∘ Fin.cast ⋯) i
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
f : (x : α) → β x → Bool
s : Finmap β
x✝³ : Bool
x✝² : α
x✝¹ : β x✝²
x✝ : α
⊢ ∀ (b₂ : β x✝), (x✝³ || f x✝² x✝¹ || f x✝ b₂) = (x✝³ || f x✝ b₂ || f x✝² x✝¹)

Tactic:
Bool.or_assoc,

Goal state after:
α : Type u
β : α → Type v
f : (x : α) → β x → Bool
s : Finmap β
x✝³ : Bool
x✝² : α
x✝¹ : β x✝²
x✝ : α
⊢ ∀ (b₂ : β x✝), (x✝³ || (f x✝² x✝¹ || f x✝ b₂)) = (x✝³ || (f x✝ b₂ || f x✝² x✝¹))
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
⊢ dlookup a (kinsert a b l) = some b

Tactic:
simp only [kinsert, dlookup_cons_eq]

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

Goal state before:
pp: κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst✝ : Zero M
k : κ
f g : ι k →₀ M
h : f.embSigma = g.embSigma
⊢ f = g

Tactic:
ext i

Goal state after:
κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst✝ : Zero M
k : κ
f g : ι k →₀ M
h : f.embSigma = g.embSigma
i : ι k
⊢ f i = g i
Module: Mathlib.Data.Finsupp.Sigma

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

Tactic:
ext i

Goal state after:
κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst✝ : Zero M
k : κ
f : ι k →₀ M
i : ι k
⊢ (f.embSigma.split k) i = f i
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

Goal state after:
κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst✝ : Zero M
k k' : κ
f : ι k →₀ M
hk : k' ≠ k
i : ι k'
⊢ (f.embSigma.split k') i = 0 i
Module: Mathlib.Data.Int.Lemmas

Goal state before:
pp: a b n : ℕ
a_lt_n : a < n
b_lt_n : b < n
⊢ (↑a - ↑b).natAbs < n

Tactic:
rw [← Nat.cast_lt (α := ℤ), natCast_natAbs]
  exact abs_sub_lt_of_nonneg_of_lt (natCast_nonneg a) (ofNat_lt.mpr a_lt_n)
    (natCast_nonneg b) (ofNat_lt.mpr b_lt_n)

Goal state after:
Module: Mathlib.Data.LawfulXor.Basic

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

Tactic:
rw [xor_eq_iff_left_eq, xor_self a]

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

Goal state before:
pp: m n✝ k i n : ℕ
⊢ Nat.shiftLeft' true m i = Nat.shiftLeft' true m (n + i) >>> n

Tactic:
rw [← Nat.shiftLeft'_sub, Nat.add_sub_cancel_left]

Goal state after:
case a
m n✝ k i n : ℕ
⊢ n ≤ n + i
Module: Mathlib.Data.List.Fold

Goal state before:
pp: α : Type u_1
β : Type u_2
l : List α
f : α → β → β
a : α
b : β
hf : LeftCommutative f
⊢ foldr f b (a :: l) = foldr f (f a b) l

Tactic:
rw [foldr_cons]

Goal state after:
α : Type u_1
β : Type u_2
l : List α
f : α → β → β
a : α
b : β
hf : LeftCommutative f
⊢ f a (foldr f b l) = foldr f (f a b) l
Module: Mathlib.Data.List.TakeWhile

Goal state before:
pp: 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 true with
    | true => hd :: takeWhile p tl
    | false => []
hp : p hd = true
⊢ p x = true

Tactic:
mem_cons

Goal state after:
case cons.true
α : Type u_1
p : α → Bool
l : List α
x hd : α
tl : List α
IH : x ∈ takeWhile p tl → p x = true
hx : x = hd ∨ x ∈ takeWhile p tl
hp : p hd = true
⊢ p x = true
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
l : List α
i j : ℕ
⊢ (drop j (drop i l.reverse).reverse.reverse).reverse = (drop (i + j) l.reverse).reverse

Tactic:
reverse_reverse,

Goal state after:
α : Type u_1
l : List α
i j : ℕ
⊢ (drop j (drop i l.reverse)).reverse = (drop (i + j) l.reverse).reverse
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
k : ℕ
hk : k ≤ l₂.reverse.length
⊢ l₁.reverse.reverse ++ (drop k l₂.reverse).reverse = l₁ ++ l₂.rdrop k

Tactic:
reverse_reverse,

Goal state after:
α : Type u_1
l₁ l₂ : List α
k : ℕ
hk : k ≤ l₂.reverse.length
⊢ l₁ ++ (drop k l₂.reverse).reverse = l₁ ++ l₂.rdrop k
Module: Mathlib.Data.List.ModifyLast

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

Tactic:
List.toList_toArray,

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

Goal state before:
pp: case inl
α : Type u_1
r : α → α → Prop
s₁ s₂ t : List α
h : Shortlex r s₁ s₂
h1 : s₁.length < s₂.length
⊢ Shortlex r s₁ (s₂ ++ t)

Tactic:
apply of_length_lt
    rw [List.length_append]
    lia

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

Goal state before:
pp: case mp
α : Type u_1
p : ℕ
w : List α
⊢ w.HasPeriod p → ∀ i < w.length - p, w[i]? = w[i + p]?

Tactic:
rw [HasPeriod]

Goal state after:
case mp
α : Type u_1
p : ℕ
w : List α
⊢ w <+: take p w ++ w → ∀ i < w.length - p, w[i]? = w[i + p]?
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: case mpr
α : Type u_1
p : ℕ
w : List α
lhs : ∀ i < w.length - p, w[i]? = w[i + p]?
⊢ w.HasPeriod p

Tactic:
rw [HasPeriod]

Goal state after:
case mpr
α : Type u_1
p : ℕ
w : List α
lhs : ∀ i < w.length - p, w[i]? = w[i + p]?
⊢ w <+: take p w ++ w
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: α : Type u_1
w : List α
p : ℕ
large : w.length ≤ p
⊢ w.HasPeriod p

Tactic:
rw [HasPeriod]

Goal state after:
α : Type u_1
w : List α
p : ℕ
large : w.length ≤ p
⊢ w <+: take p w ++ w
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: case neg
p : ℕ → Prop
n : ℕ
hn : ∃ (h : (Set.ofPred p).Finite), #⋯.toFinset ≤ n
⊢ nth p n = sInf {x | p x ∧ ∀ k < n, nth p k < x}

Tactic:
· rcases hn with ⟨hf, hn⟩
    rw [nth_of_card_le _ hn]
    refine ((congr_arg sInf <| Set.eq_empty_of_forall_notMem fun k hk => ?_).trans sInf_empty).symm
    rcases exists_lt_card_nth_eq hk.1 with ⟨k, hlt, rfl⟩
    exact (hk.2 _ ((hlt hf).trans_le hn)).false

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

Goal state before:
pp: case inl.inr
p : ℕ → Prop
k : ℕ
hf : (Set.ofPred p).Finite
n : ℕ
hn : n < #hf.toFinset
h : nth p n < nth p (k + 1)
ha : p (nth p n)
hk : #hf.toFinset ≤ k + 1
⊢ nth p n ≤ nth p k

Tactic:
nth_of_card_le _ hk

Goal state after:
case inl.inr
p : ℕ → Prop
k : ℕ
hf : (Set.ofPred p).Finite
n : ℕ
hn : n < #hf.toFinset
h : nth p n < 0
ha : p (nth p n)
hk : #hf.toFinset ≤ k + 1
⊢ nth p n ≤ nth p k