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

Goal state before:
pp: case hbc
f g : ℝ → ℝ
hg✝ : GrowsPolynomially g
hf : f =Θ[atTop] g
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_pos : 0 < b
c₁ : ℝ
hc₁_pos : 0 < c₁
hf_lb : ∀ᶠ (x : ℝ) in atTop, c₁ * ‖g x‖ ≤ ‖f x‖
c₂ : ℝ
hc₂_pos : 0 < c₂
hf_ub : ∀ᶠ (x : ℝ) in atTop, ‖f x‖ ≤ c₂ * ‖g x‖
c₃ : ℝ
hc₃_pos : 0 < c₃
c₄ : ℝ
hc₄_pos : 0 < c₄
hg :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x, (fun x ↦ ‖g x‖) u ∈ Set.Icc (c₃ * (fun x ↦ ‖g x‖) x) (c₄ * (fun x ↦ ‖g x‖) x)
h_lb_pos : 0 < c₁ * c₂⁻¹ * c₃
h_ub_pos : 0 < c₂ * c₄ * c₁⁻¹
c₂_cancel : c₂⁻¹ * c₂ = 1
c₁_cancel : c₁⁻¹ * c₁ = 1
x : ℝ
hf_pos : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
h_lb : ∀ (y : ℝ), b * id x ≤ y → c₁ * ‖g y‖ ≤ ‖f y‖
h_ub : ∀ (y : ℝ), b * id x ≤ y → ‖f y‖ ≤ c₂ * ‖g y‖
hg_bound✝ : ∀ (y : ℝ), b * id x ≤ y → ∀ u ∈ Set.Icc (b * y) y, ‖g u‖ ∈ Set.Icc (c₃ * ‖g y‖) (c₄ * ‖g y‖)
hx_pos : 0 ≤ x
u : ℝ
hu : u ∈ Set.Icc (b * x) x
hbx : b * x ≤ x
hg_bound : ∀ u ∈ Set.Icc (b * x) x, ‖g u‖ ∈ Set.Icc (c₃ * ‖g x‖) (c₄ * ‖g x‖)
⊢ c₁ * ‖g x‖ ≤ f x

Tactic:
rw [← Real.norm_of_nonneg (hf_pos x hbx)]

Goal state after:
case hbc
f g : ℝ → ℝ
hg✝ : GrowsPolynomially g
hf : f =Θ[atTop] g
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_pos : 0 < b
c₁ : ℝ
hc₁_pos : 0 < c₁
hf_lb : ∀ᶠ (x : ℝ) in atTop, c₁ * ‖g x‖ ≤ ‖f x‖
c₂ : ℝ
hc₂_pos : 0 < c₂
hf_ub : ∀ᶠ (x : ℝ) in atTop, ‖f x‖ ≤ c₂ * ‖g x‖
c₃ : ℝ
hc₃_pos : 0 < c₃
c₄ : ℝ
hc₄_pos : 0 < c₄
hg :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x, (fun x ↦ ‖g x‖) u ∈ Set.Icc (c₃ * (fun x ↦ ‖g x‖) x) (c₄ * (fun x ↦ ‖g x‖) x)
h_lb_pos : 0 < c₁ * c₂⁻¹ * c₃
h_ub_pos : 0 < c₂ * c₄ * c₁⁻¹
c₂_cancel : c₂⁻¹ * c₂ = 1
c₁_cancel : c₁⁻¹ * c₁ = 1
x : ℝ
hf_pos : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
h_lb : ∀ (y : ℝ), b * id x ≤ y → c₁ * ‖g y‖ ≤ ‖f y‖
h_ub : ∀ (y : ℝ), b * id x ≤ y → ‖f y‖ ≤ c₂ * ‖g y‖
hg_bound✝ : ∀ (y : ℝ), b * id x ≤ y → ∀ u ∈ Set.Icc (b * y) y, ‖g u‖ ∈ Set.Icc (c₃ * ‖g y‖) (c₄ * ‖g y‖)
hx_pos : 0 ≤ x
u : ℝ
hu : u ∈ Set.Icc (b * x) x
hbx : b * x ≤ x
hg_bound : ∀ u ∈ Set.Icc (b * x) x, ‖g u‖ ∈ Set.Icc (c₃ * ‖g x‖) (c₄ * ‖g x‖)
⊢ c₁ * ‖g x‖ ≤ ‖f x‖
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: case h
Γ : Type u_1
inst✝ : Inhabited Γ
l₁ l₂ : List Γ
i j : ℕ
e : l₁ ++ List.replicate i default = l₂ ++ List.replicate j default
h : l₁.length ≤ l₂.length
⊢ l₁ ++ List.replicate i default = l₁ ++ List.replicate (i - j + j) default

Tactic:
Nat.sub_add_cancel

Goal state after:
case h
Γ : Type u_1
inst✝ : Inhabited Γ
l₁ l₂ : List Γ
i j : ℕ
e : l₁ ++ List.replicate i default = l₂ ++ List.replicate j default
h : l₁.length ≤ l₂.length
⊢ l₁ ++ List.replicate i default = l₁ ++ List.replicate i default

case h
Γ : Type u_1
inst✝ : Inhabited Γ
l₁ l₂ : List Γ
i j : ℕ
e : l₁ ++ List.replicate i default = l₂ ++ List.replicate j default
h : l₁.length ≤ l₂.length
⊢ j ≤ i
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case some.write
Γ : Type u_1
inst✝³ : Inhabited Γ
Γ' : Type u_2
inst✝² : Inhabited Γ'
Λ : Type u_3
inst✝¹ : Inhabited Λ
Λ' : Type u_4
inst✝ : Inhabited Λ'
M : Machine Γ Λ
f₁ : PointedMap Γ Γ'
f₂ : PointedMap Γ' Γ
g₁ : Λ → Λ'
g₂ : Λ' → Λ
S : Set Λ
f₂₁ : Function.RightInverse f₁.f f₂.f
g₂₁ : ∀ q ∈ S, g₂ (g₁ q) = q
q : Λ
T : Tape Γ
h : { q := q, Tape := T }.q ∈ S
q' : Λ
a : Γ
⊢ Option.map (fun x ↦ { q := g₁ x.q, Tape := Tape.map f₁ x.Tape })
      (Option.map
        (fun x ↦
          { q := x.1,
            Tape :=
              match x.2 with
              | Stmt.move d => Tape.move d T
              | Stmt.write a => Tape.write a T })
        (some (q', Stmt.write a))) =
    Option.map
      (fun x ↦
        { q := x.1,
          Tape :=
            match x.2 with
            | Stmt.move d => Tape.move d (Tape.map f₁ T)
            | Stmt.write a => Tape.write a (Tape.map f₁ T) })
      (Option.map (Prod.map g₁ (Stmt.map f₁)) (some (q', Stmt.write a)))

Tactic:
simp only [Option.map_some, Tape.map_write]
      rfl

Goal state after:
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case mpr.cons.cons.cons.refine_1
α : Type u_1
inst✝ : DecidableEq α
P : RegularExpression α
a : α
x : List α
IH :
  ∀ (t : List α),
    t.length < (a :: x).length → (P.star.rmatch t = true ↔ ∃ S, t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true)
U : List (List α)
b : α
t : List α
helem : b :: t ≠ [] ∧ (P.deriv b).rmatch t = true
hsum : a = b ∧ x = t ++ U.flatten
⊢ (P.deriv a).rmatch t = true

Tactic:
convert! helem.2

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
P : RegularExpression α
a : α
x : List α
IH :
  ∀ (t : List α),
    t.length < (a :: x).length → (P.star.rmatch t = true ↔ ∃ S, t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true)
U : List (List α)
b : α
t : List α
helem : b :: t ≠ [] ∧ (P.deriv b).rmatch t = true
hsum : a = b ∧ x = t ++ U.flatten
⊢ a = b
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case epsilon
α : Type u_1
inst✝ : DecidableEq α
x : List α
⊢ x = [] ↔ x ∈ matches' 1

Tactic:
matches'_epsilon,

Goal state after:
case epsilon
α : Type u_1
inst✝ : DecidableEq α
x : List α
⊢ x = [] ↔ x ∈ 1
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case comp
n : ℕ
f : List.Vector ℕ n →. ℕ
m✝ n✝ : ℕ
f✝ : List.Vector ℕ n✝ →. ℕ
g : Fin n✝ → List.Vector ℕ m✝ →. ℕ
a✝¹ : Nat.Partrec' f✝
a✝ : ∀ (i : Fin n✝), Nat.Partrec' (g i)
IHf : ∃ c, ∀ (v : List.Vector ℕ n✝), c.eval ↑v = pure <$> f✝ v
IHg : ∀ (i : Fin n✝), ∃ c, ∀ (v : List.Vector ℕ m✝), c.eval ↑v = pure <$> g i v
⊢ ∃ c, ∀ (v : List.Vector ℕ m✝), c.eval ↑v = pure <$> (fun v ↦ (Vector.mOfFn fun i ↦ g i v) >>= f✝) v

Tactic:
exact exists_code.comp IHf IHg

Goal state after:
Module: Mathlib.Topology.Category.CompHausLike.Limits

Goal state before:
pp: P : TopCat → Prop
X Y B : CompHausLike P
f : X ⟶ B
g : Y ⟶ B
inst✝ : HasExplicitPullback f g
Z : CompHausLike P
a : Z ⟶ X
b : Z ⟶ Y
w : a ≫ f = b ≫ g
z : ↑Z.toTop
⊢ ((ConcreteCategory.hom a) z, (ConcreteCategory.hom b) z) ∈
    {xy | (ConcreteCategory.hom f) xy.1 = (ConcreteCategory.hom g) xy.2}

Tactic:
by apply_fun (fun q ↦ q z) at w; exact w

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

Goal state before:
pp: f : Code
k : Cont
v : List ℕ
fok : f.Ok
x : Cfg
this :
  ∀ (c : Cfg),
    x ∈ eval step c →
      ∀ (v : List ℕ) (c' : Cfg),
        c = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
h : x ∈ eval step (stepNormal f (Cont.fix f k) v)
v₁ : List ℕ
hv₁ : v₁ ∈ f.eval v
v₂ : List ℕ
hv₂ : v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail
h₃ : x ∈ eval step (Cfg.ret k v₂)
⊢ Sum.inl v₂ ∈ Part.some (if v₁.headI = 0 then Sum.inl v₁.tail else Sum.inr v₁.tail) ∨
    ∃ a',
      Sum.inr a' ∈ Part.some (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₂ ⊢

Goal state after:
case pos
f : Code
k : Cont
v : List ℕ
fok : f.Ok
x : Cfg
this :
  ∀ (c : Cfg),
    x ∈ eval step c →
      ∀ (v : List ℕ) (c' : Cfg),
        c = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
h : x ∈ eval step (stepNormal f (Cont.fix f k) v)
v₁ : List ℕ
hv₁ : v₁ ∈ f.eval v
v₂ : List ℕ
h₃ : x ∈ eval step (Cfg.ret k v₂)
h✝ : v₁.headI = 0
hv₂ : v₂ ∈ pure v₁.tail
⊢ Sum.inl v₂ ∈ Part.some (Sum.inl v₁.tail) ∨
    ∃ a',
      Sum.inr a' ∈ Part.some (Sum.inl 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'

case neg
f : Code
k : Cont
v : List ℕ
fok : f.Ok
x : Cfg
this :
  ∀ (c : Cfg),
    x ∈ eval step c →
      ∀ (v : List ℕ) (c' : Cfg),
        c = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
h : x ∈ eval step (stepNormal f (Cont.fix f k) v)
v₁ : List ℕ
hv₁ : v₁ ∈ f.eval v
v₂ : List ℕ
h₃ : x ∈ eval step (Cfg.ret k v₂)
h✝ : ¬v₁.headI = 0
hv₂ : v₂ ∈ f.fix.eval v₁.tail
⊢ Sum.inl v₂ ∈ Part.some (Sum.inr v₁.tail) ∨
    ∃ a',
      Sum.inr a' ∈ Part.some (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'
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case pos
f : Code
k : Cont
v : List ℕ
fok : f.Ok
x : Cfg
this :
  ∀ (c : Cfg),
    x ∈ eval step c →
      ∀ (v : List ℕ) (c' : Cfg),
        c = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
h : x ∈ eval step (stepNormal f (Cont.fix f k) v)
v₁ : List ℕ
hv₁ : v₁ ∈ f.eval v
v₂ : List ℕ
h₃ : x ∈ eval step (Cfg.ret k v₂)
h✝ : v₁.headI = 0
hv₂ : v₂ ∈ pure v₁.tail
⊢ Sum.inl v₁.tail ∈ Part.some (Sum.inl v₁.tail) ∨
    ∃ a',
      Sum.inr a' ∈ Part.some (Sum.inl v₁.tail) ∧
        v₁.tail ∈
          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:
exact Or.inl (Part.mem_some _)

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

Goal state before:
pp: case cons
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v : List ℕ
⊢ eval step ((fun k v ↦ stepNormal f (Cont.cons₁ fs v k) v) k v) = do
    let v ← (f.cons fs).eval v
    eval step (Cfg.ret k v)

Tactic:
| cons f fs IHf IHfs =>

Goal state after:
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: case refine_1.inl
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := Uᶜ ×ˢ {true}
Z₂ : Set (X × Bool) := closure U ×ˢ {false}
Z : Set (X × Bool) := Z₁ ∪ Z₂
hZ₁₂ : Disjoint Z₁ Z₂
hZ₁ : IsClosed Z₁
hZ₂ : IsClosed Z₂
hZ : IsClosed Z
f : ↑Z → X := Prod.fst ∘ Subtype.val
f_cont : Continuous f
f_sur : Surjective f
this : CompactSpace ↑Z
g : X → ↑Z
hg : Continuous g
g_sec : f ∘ g = id
φ : X → X × Bool := Subtype.val ∘ g
hφ✝ : Continuous φ
hφ₁ : ∀ (x : X), (φ x).1 = x
x : X
hx : x ∈ U
hφ : φ x ∈ Z₁
⊢ x ∈ φ ⁻¹' Z₂

Tactic:
exact ((hφ₁ x ▸ hφ.1) hx).elim

Goal state after:
Module: Mathlib.Logic.Function.FiberPartition

Goal state before:
pp: Y : Type u_2
Z : Type u_3
f : Y → Z
a : Fiber f
x : ↑↑a
⊢ f ↑x = image f a

Tactic:
by
  have := a.2.choose_spec
  rw [← Set.mem_singleton_iff, ← Set.mem_preimage]
  convert! x.prop

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

Goal state before:
pp: J : Type v
inst✝³ : SmallCategory J
inst✝² : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toTop) (α → Fin 2)
h : LocallyConstant.map (fun a b ↦ if a = b then 0 else 1) f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) gg
ι : α → α → Fin 2 := fun a b ↦ if a = b then 0 else 1
σ : (α → Fin 2) → α := fun f ↦ if h : ∃ a, ι a = f then h.choose else default
x : ↑C.pt.toTop
h1 : ι (f x) = gg ((ConcreteCategory.hom (C.π.app j)) x)
⊢ f x = if h : ∃ a, ι a = gg ((TopCat.Hom.hom (C.π.app j).hom) x) then h.choose else default

Tactic:
have h2 : ∃ a : α, ι a = gg (C.π.app j x) := ⟨f x, h1⟩

Goal state after:
J : Type v
inst✝³ : SmallCategory J
inst✝² : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toTop) (α → Fin 2)
h : LocallyConstant.map (fun a b ↦ if a = b then 0 else 1) f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) gg
ι : α → α → Fin 2 := fun a b ↦ if a = b then 0 else 1
σ : (α → Fin 2) → α := fun f ↦ if h : ∃ a, ι a = f then h.choose else default
x : ↑C.pt.toTop
h1 : ι (f x) = gg ((ConcreteCategory.hom (C.π.app j)) x)
h2 : ∃ a, ι a = gg ((ConcreteCategory.hom (C.π.app j)) x)
⊢ f x = if h : ∃ a, ι a = gg ((TopCat.Hom.hom (C.π.app j).hom) x) then h.choose else default
Module: Mathlib.Topology.Category.LightProfinite.Extend

Goal state before:
pp: F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
C : Type u_1
inst✝ : Category.{v_1, u_1} C
G : LightProfiniteᵒᵖ ⥤ C
S : LightProfinite
x✝¹ x✝ : CostructuredArrow toLightProfinite.op (Opposite.op S)
f : x✝¹ ⟶ x✝
⊢ (CostructuredArrow.proj toLightProfinite.op (Opposite.op S) ⋙ toLightProfinite.op ⋙ G).map f ≫ G.map x✝.hom =
    G.map x✝¹.hom ≫ ((const (CostructuredArrow toLightProfinite.op (Opposite.op S))).obj (G.obj (Opposite.op S))).map f

Tactic:
have := f.w
      simp only [op_obj, const_obj_obj, op_map, CostructuredArrow.right_eq_id, const_obj_map,
        Category.comp_id] at this
      simp only [comp_obj, CostructuredArrow.proj_obj, op_obj, const_obj_obj, Functor.comp_map,
        CostructuredArrow.proj_map, op_map, ← map_comp, this, const_obj_map, Category.comp_id]

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

Goal state before:
pp: case right
I : Type u
inst✝² : SmallCategory I
inst✝¹ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
hc : IsLimit c
inst✝ : ∀ (i : I), Epi (c.π.app i)
e : I ≌ ULiftHom (ULift.{w, u} I) := ⋯
⊢ ∀ {d : StructuredArrow c.pt toProfinite} {c_1 : ULiftHom (ULift.{w, u} I)}
    (s s' : (e.inverse ⋙ functor c).obj c_1 ⟶ d),
    ∃ c' t, (e.inverse ⋙ functor c).map t ≫ s = (e.inverse ⋙ functor c).map t ≫ s'

Tactic:
· intro ⟨_, X, (f : c.pt ⟶ _)⟩ ⟨i⟩ ⟨_, (s : F.obj i ⟶ X), (w : f = c.π.app i ≫ _)⟩
      ⟨_, (s' : F.obj i ⟶ X), (w' : f = c.π.app i ≫ _)⟩
    simp only [StructuredArrow.hom_eq_iff,
      StructuredArrow.comp_right]
    refine ⟨⟨i⟩, 𝟙 _, ?_⟩
    simp only [CategoryTheory.Functor.map_id]
    rw [w] at w'
    exact toProfinite.map_injective <| Epi.left_cancellation _ _ w'

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

Goal state before:
pp: case cons
S : Finset Λ'
f fs : Code
IHf : ∀ {k : Cont'}, codeSupp f k ⊆ S → Supports (codeSupp' f k) S
IHfs : ∀ {k : Cont'}, codeSupp fs k ⊆ S → Supports (codeSupp' fs k) S
k : Cont'
H : codeSupp (f.cons fs) k ⊆ S
⊢ Supports (codeSupp' (f.cons fs) k) S

Tactic:
| cons f fs IHf IHfs =>

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

Goal state before:
pp: b x : Bool
l : List Bool
h : IsChain (fun x1 x2 ↦ x1 ≠ x2) (b :: x :: l)
⊢ count (!b) (x :: l) = count b (x :: l) + (x :: l).length % 2

Tactic:
grind [h.of_cons.count_not_cons]

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
xs : List α
h : ∀ (x : α), x ∈ xs
h' : xs.Nodup
i : Fin xs.length
⊢ (fun x ↦ ⟨List.idxOf x xs, ⋯⟩) (xs.get i) = i

Tactic:
by ext; simp [h'.idxOf_getElem]

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

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

Tactic:
by
  by_cases h : a = a'
  · subst a'; rfl
  induction l with
  | nil => rfl
  | cons x xs =>
    by_cases a' = x.1
    · subst a'
      simp [kerase_cons_ne h, kerase_cons_eq rfl]
    by_cases h' : a = x.1
    · subst a
      simp [kerase_cons_eq rfl, kerase_cons_ne (Ne.symm h)]
    · simp [kerase_cons_ne, *]

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

Goal state before:
pp: α : Type u_1
N : Type u_3
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : AddGroup N
f g : α →₀ N
⊢ (f - g).neLocus f = g.support

Tactic:
rw [neLocus_comm, neLocus_self_sub_right]

Goal state after:
Module: Mathlib.Data.Holor

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

Tactic:
apply slice_eq _ _ _

Goal state after:
α : Type
d : ℕ
ds : List ℕ
inst✝ : Semiring α
x : Holor α (d :: ds)
⊢ (∑ i ∈ (Finset.range d).attach, unitVec d ↑i ⊗ x.slice ↑i ⋯).slice = x.slice
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:
by
   rw [xor_eq_iff_left_eq, xor_self a]

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

Goal state before:
pp: a b r v x : ℤ
⊢ (a ≤ x ∧ x < b) ∧ x ≡ v [ZMOD r] ↔ (a - v ≤ x - v ∧ x - v < b - v) ∧ r ∣ x - v

Tactic:
modEq_comm,

Goal state after:
a b r v x : ℤ
⊢ (a ≤ x ∧ x < b) ∧ v ≡ x [ZMOD r] ↔ (a - v ≤ x - v ∧ x - v < b - v) ∧ r ∣ x - v
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: a b r v x : ℤ
⊢ (a < x ∧ x ≤ b) ∧ x ≡ v [ZMOD r] ↔ (a - v < x - v ∧ x - v ≤ b - v) ∧ r ∣ x - v

Tactic:
modEq_comm,

Goal state after:
a b r v x : ℤ
⊢ (a < x ∧ x ≤ b) ∧ v ≡ x [ZMOD r] ↔ (a - v < x - v ∧ x - v ≤ b - v) ∧ r ∣ x - v
Module: Mathlib.Data.List.TakeWhile

Goal state before:
pp: case pos
α : Type u_1
p q : α → Bool
hd : α
tl : List α
IH : takeWhile p (takeWhile q tl) = takeWhile (fun a ↦ decide (p a = true ∧ q a = true)) tl
hp : p hd = true
hq : q hd = true
⊢ takeWhile p (takeWhile q (hd :: tl)) = takeWhile (fun a ↦ decide (p a = true ∧ q a = true)) (hd :: tl)

Tactic:
simp [takeWhile, hp, hq, IH]

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

Goal state before:
pp: case neg
α : Type u_1
p q : α → Bool
hd : α
tl : List α
IH : takeWhile p (takeWhile q tl) = takeWhile (fun a ↦ decide (p a = true ∧ q a = true)) tl
hp : p hd = true
hq : ¬q hd = true
⊢ takeWhile p (takeWhile q (hd :: tl)) = takeWhile (fun a ↦ decide (p a = true ∧ q a = true)) (hd :: tl)

Tactic:
simp [takeWhile, hp, hq, IH]

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

Goal state before:
pp: case pos
α : Type u_1
p q : α → Bool
hd : α
tl : List α
IH : takeWhile p (takeWhile q tl) = takeWhile (fun a ↦ decide (p a = true ∧ q a = true)) tl
hp : ¬p hd = true
hq : q hd = true
⊢ takeWhile p (takeWhile q (hd :: tl)) = takeWhile (fun a ↦ decide (p a = true ∧ q a = true)) (hd :: tl)

Tactic:
simp [takeWhile, hp, hq, IH]

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

Goal state before:
pp: case neg
α : Type u_1
p q : α → Bool
hd : α
tl : List α
IH : takeWhile p (takeWhile q tl) = takeWhile (fun a ↦ decide (p a = true ∧ q a = true)) tl
hp : ¬p hd = true
hq : ¬q hd = true
⊢ takeWhile p (takeWhile q (hd :: tl)) = takeWhile (fun a ↦ decide (p a = true ∧ q a = true)) (hd :: tl)

Tactic:
simp [takeWhile, hp, hq, IH]

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α → β → γ
a : α
as : List α
b : β
bs : List β
⊢ zipWith (flip f) (b :: bs) (a :: as) = zipWith f (a :: as) (b :: bs)

Tactic:
simp! [zipWith_flip]

Goal state after:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
a : α
as : List α
b : β
bs : List β
⊢ flip f b a = f a b
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: case mpr
α : Type u_1
p : ℕ
w : List α
mod : ∀ i < w.length, w[i]? = w[i % p]?
i : ℕ
less : i < w.length - p
⊢ w[i]? = w[(i + p) % p]?

Tactic:
add_mod_right,

Goal state after:
case mpr
α : Type u_1
p : ℕ
w : List α
mod : ∀ i < w.length, w[i]? = w[i % p]?
i : ℕ
less : i < w.length - p
⊢ w[i]? = w[i % p]?
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: case nil
α : Type u_1
m : List α
r : α → α → Bool
g : List α
a : α
h : IsChain (fun x y ↦ r x y = true) (g.reverse ++ [a])
ha : ∀ (x : α), x ∈ m.head? → r ([a].getLast ⋯) x = false
⊢ splitBy.loop r ([] ++ m) a g [] = (g.reverse ++ [a]) :: splitBy r m

Tactic:
rw [nil_append]

Goal state after:
case nil
α : Type u_1
m : List α
r : α → α → Bool
g : List α
a : α
h : IsChain (fun x y ↦ r x y = true) (g.reverse ++ [a])
ha : ∀ (x : α), x ∈ m.head? → r ([a].getLast ⋯) x = false
⊢ splitBy.loop r m a g [] = (g.reverse ++ [a]) :: splitBy r m
Module: Mathlib.Data.NNRat.BigOperators

Goal state before:
pp: α : Type u_1
s : Finset α
f : α → ℚ
hf : ∀ a ∈ s, 0 ≤ f a
x : α
hxs : x ∈ s
⊢ f x = ↑(f x).toNNRat

Tactic:
by rw [Rat.coe_toNNRat _ (hf x hxs)]

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

Goal state before:
pp: case mk
ι : Type u_1
a s : ι → ℕ
l : List ι
nod : Multiset.Nodup (Quot.mk (⇑(List.isSetoid ι)) l)
hs : ∀ i ∈ Quot.mk (⇑(List.isSetoid ι)) l, s i ≠ 0
pp : {x | x ∈ Quot.mk (⇑(List.isSetoid ι)) l}.Pairwise (Coprime on s)
⊢ ↑(chineseRemainderOfMultiset a s nod hs pp) < (Multiset.map s (Quot.mk (⇑(List.isSetoid ι)) l)).prod

Tactic:
| _ l
   => 

Goal state after:
case mk
ι : Type u_1
a s : ι → ℕ
l : List ι
nod : Multiset.Nodup (Quot.mk (⇑(List.isSetoid ι)) l)
hs : ∀ i ∈ Quot.mk (⇑(List.isSetoid ι)) l, s i ≠ 0
pp : {x | x ∈ Quot.mk (⇑(List.isSetoid ι)) l}.Pairwise (Coprime on s)
⊢ ↑(chineseRemainderOfMultiset a s nod hs pp) < (Multiset.map s (Quot.mk (⇑(List.isSetoid ι)) l)).prod
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: case refine_2
p : ℕ → Prop
x : ℕ
hf : (Set.ofPred p).Infinite
n : ℕ
hx : nth p n = x
⊢ ∃ n, (∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset) ∧ nth p n = x

Tactic:
exact ⟨n, fun hf' => absurd hf' hf, hx⟩

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

Goal state before:
pp: case mp
P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
x : ↑P α
y : ↑P (Subtype p)
hy : Subtype.val <$> y = x
⊢ ∃ a f, x = ⟨a, f⟩ ∧ ∀ (i : P.B a), p (f i)

Tactic:
rcases h : y with ⟨a, f⟩

Goal state after:
case mp
P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
x : ↑P α
y : ↑P (Subtype p)
hy : Subtype.val <$> y = x
a : P.A
f : P.B a → Subtype p
h : y = ⟨a, f⟩
⊢ ∃ a f, x = ⟨a, f⟩ ∧ ∀ (i : P.B a), p (f i)
Module: Mathlib.Data.PFunctor.Univariate.Basic

Goal state before:
pp: case h.right.left
P : PFunctor.{uA, uB}
α : Type u
r : α → α → Prop
x y : ↑P α
u : ↑P { p // r p.1 p.2 }
xeq : (fun t ↦ (↑t).1) <$> u = x
yeq : (fun t ↦ (↑t).2) <$> u = y
a : P.A
f : P.B a → { p // r p.1 p.2 }
h : u = ⟨a, f⟩
⊢ y = ⟨a, fun i ↦ (↑(f i)).2⟩

Tactic:
← yeq,

Goal state after:
case h.right.left
P : PFunctor.{uA, uB}
α : Type u
r : α → α → Prop
x y : ↑P α
u : ↑P { p // r p.1 p.2 }
xeq : (fun t ↦ (↑t).1) <$> u = x
yeq : (fun t ↦ (↑t).2) <$> u = y
a : P.A
f : P.B a → { p // r p.1 p.2 }
h : u = ⟨a, f⟩
⊢ (fun t ↦ (↑t).2) <$> u = ⟨a, fun i ↦ (↑(f i)).2⟩
Module: Mathlib.Data.PFunctor.Multivariate.Basic

Goal state before:
pp: case mp
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : ↑P α
y : ↑P fun i ↦ Subtype p
hy : (fun i ↦ Subtype.val) <$$> y = x
⊢ ∃ a f, x = ⟨a, f⟩ ∧ ∀ (i : Fin2 n) (j : P.B a i), p (f i j)

Tactic:
rcases h : y with ⟨a, f⟩

Goal state after:
case mp
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : ↑P α
y : ↑P fun i ↦ Subtype p
hy : (fun i ↦ Subtype.val) <$$> y = x
a : P.A
f : P.B a ⟹ fun i ↦ Subtype p
h : y = ⟨a, f⟩
⊢ ∃ a f, x = ⟨a, f⟩ ∧ ∀ (i : Fin2 n) (j : P.B a i), p (f i j)
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
⊢ (l.node3L x m y r).dual = r.dual.node3R y m.dual x l.dual

Tactic:
simp [node3L, node3R, add_comm]

Goal state after:
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
⊢ (l.node3R x m y r).dual = r.dual.node3L y m.dual x l.dual

Tactic:
simp [node3L, node3R, add_comm]

Goal state after:
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case nil
α : Type u_1
l : Ordnode α
x y : α
r : Ordnode α
⊢ (l.node4R x nil y r).dual = r.dual.node4L y nil.dual x l.dual

Tactic:
simp [node4L, node4R, node3L, dual_node3R, add_comm]

Goal state after:
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case node
α : Type u_1
l : Ordnode α
x y : α
r : Ordnode α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ (l.node4R x (node size✝ l✝ x✝ r✝) y r).dual = r.dual.node4L y (node size✝ l✝ x✝ r✝).dual x l.dual

Tactic:
simp [node4L, node4R, node3L, dual_node3R, add_comm]

Goal state after: