mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
w : V
hcyc : G.IsCycles
_x : (v : V) ×' (p : G.Walk v w) ×' p.IsPath
a✝² :
  ∀ (y : (v : V) ×' (p : G.Walk v w) ×' p.IsPath),
    InvImage (fun x1 x2 ↦ x1 < x2)
        (fun x ↦ PSigma.casesOn x fun v p ↦ PSigma.casesOn p fun p hp ↦ Nat.card V + 1 - p.length) y _x →
      (G \ y.2.1.toSubgraph.spanningCoe).Reachable w y.1
v : V
p✝ : (p : G.Walk v w) ×' p.IsPath
a✝¹ :
  ∀ (y : (v : V) ×' (p : G.Walk v w) ×' p.IsPath),
    InvImage (fun x1 x2 ↦ x1 < x2)
        (fun x ↦ PSigma.casesOn x fun v p ↦ PSigma.casesOn p fun p hp ↦ Nat.card V + 1 - p.length) y ⟨v, p✝⟩ →
      (G \ y.2.1.toSubgraph.spanningCoe).Reachable w y.1
p : G.Walk v w
hp : p.IsPath
a✝ :
  ∀ (y : (v : V) ×' (p : G.Walk v w) ×' p.IsPath),
    InvImage (fun x1 x2 ↦ x1 < x2)
        (fun x ↦ PSigma.casesOn x fun v p ↦ PSigma.casesOn p fun p hp ↦ Nat.card V + 1 - p.length) y ⟨v, ⟨p, hp⟩⟩ →
      (G \ y.2.1.toSubgraph.spanningCoe).Reachable w y.1
hvw : ¬v = w
hpn : ¬p.Nil
w' : V
h✝ : (fun w' ↦ p.snd ≠ w' ∧ G.Adj v w') w' ∧ ∀ (y : V), p.snd ≠ y ∧ G.Adj v y → y = w'
left✝ : p.snd ≠ w' ∧ G.Adj v w'
hwu : ∀ (y : V), p.snd ≠ y ∧ G.Adj v y → y = w'
hw'1 : p.snd ≠ w'
hw'2 : G.Adj v w'
hnpvw' : ¬p.toSubgraph.Adj v w'
hww' : ¬w = w'
hle : G \ (Walk.cons ⋯ p).toSubgraph.spanningCoe ≤ G \ p.toSubgraph.spanningCoe
hp'p : (Walk.cons ⋯ p).IsPath
this : (G \ p.toSubgraph.spanningCoe).Adj w' v
⊢ Nat.card V + 1 - (Walk.cons ⋯ p).length < Nat.card V + 1 - p.length

Tactic:
have := Fintype.ofFinite V
  simp_wf
  have := Walk.IsPath.length_lt hp
  lia

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
r k : ℕ
x v w₁ w₂ : α
s t : Finset α
inst✝¹ : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst✝ : DecidableRel G.Adj
hW : ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y
h2 : #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z}) ≤ 2
a b c d : α
haj : ¬G.Adj x a
hbj : ¬G.Adj x b
hab : a ≠ b
hat : a ∉ t
hbs : b ∉ s
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
hcj : ¬G.Adj x a
hbc : b ≠ a
hca : True
hdj : ¬G.Adj x b
had : a ≠ b
hdb : True
ha : a = w₁ ∨ a ∈ s
hb : b = w₂ ∨ b ∈ t
hc : a = v ∨ a ∈ s
hd : b = v ∨ b ∈ t
has : a ∈ s
hbt : b ∈ t
hav : a ≠ v
hbv : b ≠ v
haw : a ≠ w₂
hbw : b ≠ w₁
hxv : v ≠ x
hxw₁ : w₁ ≠ x
hxw₂ : w₂ ≠ x
wa : ∀ ⦃w : α⦄, w ∈ W → w ≠ a → w ≠ b → G.Adj w x
h1s : insert w₁ s ⊆ W
h2t : insert w₂ t ⊆ W
⊢ #(insert x (s.erase a) ∩ insert x (t.erase b)) = k + 1

Tactic:
rw [← insert_inter_distrib, erase_inter, inter_erase, erase_eq_of_notMem <|
        notMem_mono inter_subset_left hbs, erase_eq_of_notMem <| notMem_mono inter_subset_right hat,
        card_insert_of_notMem (fun h ↦ G.irrefl (hW h)), hw.card_inter]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Goal state before:
pp: case neg
α : Type u_1
G : SimpleGraph α
r k : ℕ
v w₁ w₂ : α
s t : Finset α
inst✝² : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst✝¹ : DecidableRel G.Adj
inst✝ : Fintype α
hm : G.FiveWheelLikeFree r (k + 1)
X : Finset α := {x | ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y}
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
dXle : ∀ x ∈ X, 3 ≤ #({z ∈ W | ¬G.Adj x z})
one_le : ∀ (x : α), 1 ≤ #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z})
bdW : ∑ w ∈ W, G.degree w ≤ #X * (#W - 3) + #Xᶜ * (#W - 1)
xcle : ∀ x ∈ Xᶜ, 1 ≤ #({z ∈ s ∩ t | ¬G.Adj x z})
bdX : ∑ w ∈ s ∩ t, G.degree w ≤ #X * #(s ∩ t) + #Xᶜ * (#(s ∩ t) - 1)
Wc : #W + k = 2 * r + 3
hk : ¬k = 0
⊢ #X * (#W - 3 + 2 * k) + #Xᶜ * (#W - 1 + 2 * (k - 1)) ≤ (2 * r + k) * ‖α‖

Tactic:
have w3 : 3 ≤ #W := two_lt_card.2 ⟨_, mem_insert_self .., _, by simp [W], _, by simp [W],
          hw.isPathGraph3Compl.ne_fst, hw.isPathGraph3Compl.ne_snd, hw.isPathGraph3Compl.fst_ne_snd⟩

Goal state after:
case neg
α : Type u_1
G : SimpleGraph α
r k : ℕ
v w₁ w₂ : α
s t : Finset α
inst✝² : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst✝¹ : DecidableRel G.Adj
inst✝ : Fintype α
hm : G.FiveWheelLikeFree r (k + 1)
X : Finset α := {x | ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y}
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
dXle : ∀ x ∈ X, 3 ≤ #({z ∈ W | ¬G.Adj x z})
one_le : ∀ (x : α), 1 ≤ #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z})
bdW : ∑ w ∈ W, G.degree w ≤ #X * (#W - 3) + #Xᶜ * (#W - 1)
xcle : ∀ x ∈ Xᶜ, 1 ≤ #({z ∈ s ∩ t | ¬G.Adj x z})
bdX : ∑ w ∈ s ∩ t, G.degree w ≤ #X * #(s ∩ t) + #Xᶜ * (#(s ∩ t) - 1)
Wc : #W + k = 2 * r + 3
hk : ¬k = 0
w3 : 3 ≤ #W
⊢ #X * (#W - 3 + 2 * k) + #Xᶜ * (#W - 1 + 2 * (k - 1)) ≤ (2 * r + k) * ‖α‖
Module: Mathlib.Combinatorics.SimpleGraph.VertexCover

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
⊢ ∃ s, s.encard = G.vertexCoverNum ∧ G.IsVertexCover s

Tactic:
have : Nonempty {s : Set V // IsVertexCover G s} := nonempty_subtype.mpr ⟨Set.univ, by simp⟩

Goal state after:
V : Type u_1
G : SimpleGraph V
this : Nonempty { s // G.IsVertexCover s }
⊢ ∃ s, s.encard = G.vertexCoverNum ∧ G.IsVertexCover s
Module: Mathlib.Combinatorics.SimpleGraph.Tutte

Goal state before:
pp: case neg
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
x a b c : V
M1 : (G ⊔ edge x b).Subgraph
M2 : (G ⊔ edge a c).Subgraph
hxa : G.Adj x a
hab : G.Adj a b
hnGxb : ¬G.Adj x b
hnGac : ¬G.Adj a c
hnxb : x ≠ b
hnxc : x ≠ c
hnac : a ≠ c
hnbc : b ≠ c
hM1 : M1.IsPerfectMatching
hM2 : M2.IsPerfectMatching
hM1xb : M1.Adj x b
hM2ac : M2.Adj a c
⊢ ∃ M, M.IsPerfectMatching

Tactic:
have hM1nac : ¬M1.Adj a c := fun h ↦ by simpa [hnGac, edge_adj, hnac, hxa.ne, hnbc.symm, hab.ne]
    using h.adj_sub

Goal state after:
case neg
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
x a b c : V
M1 : (G ⊔ edge x b).Subgraph
M2 : (G ⊔ edge a c).Subgraph
hxa : G.Adj x a
hab : G.Adj a b
hnGxb : ¬G.Adj x b
hnGac : ¬G.Adj a c
hnxb : x ≠ b
hnxc : x ≠ c
hnac : a ≠ c
hnbc : b ≠ c
hM1 : M1.IsPerfectMatching
hM2 : M2.IsPerfectMatching
hM1xb : M1.Adj x b
hM2ac : M2.Adj a c
hM1nac : ¬M1.Adj a c
⊢ ∃ M, M.IsPerfectMatching
Module: Mathlib.Combinatorics.Tiling.Tile

Goal state before:
pp: case refine_2
G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G X
ps : Protoset G X ιₚ
g : G
i₁ : ιₚ
g₁ : G ⧸ Subgroup.map (MulAction.stabilizer G ↑(↑ps i₁)).subtype (↑ps i₁).symmetries
hg₁ : ⟦g⟧ = { index := i₁, groupElts := g₁ }.groupElts
i₂ : ιₚ
g₂ : G ⧸ Subgroup.map (MulAction.stabilizer G ↑(↑ps i₂)).subtype (↑ps i₂).symmetries
hg₂ : ⟦g⟧ = { index := i₂, groupElts := g₂ }.groupElts
x✝ :
  { index := i₁, groupElts := g₁ }.index = { index := i₂, groupElts := g₂ }.index ∧
    ∃ g, ⟦g⟧ = { index := i₁, groupElts := g₁ }.groupElts ∧ ⟦g⟧ = { index := i₂, groupElts := g₂ }.groupElts
h : { index := i₁, groupElts := g₁ }.index = { index := i₂, groupElts := g₂ }.index
⊢ { index := i₁, groupElts := g₁ } = { index := i₂, groupElts := g₂ }

Tactic:
dsimp only at h

Goal state after:
case refine_2
G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G X
ps : Protoset G X ιₚ
g : G
i₁ : ιₚ
g₁ : G ⧸ Subgroup.map (MulAction.stabilizer G ↑(↑ps i₁)).subtype (↑ps i₁).symmetries
hg₁ : ⟦g⟧ = { index := i₁, groupElts := g₁ }.groupElts
i₂ : ιₚ
g₂ : G ⧸ Subgroup.map (MulAction.stabilizer G ↑(↑ps i₂)).subtype (↑ps i₂).symmetries
hg₂ : ⟦g⟧ = { index := i₂, groupElts := g₂ }.groupElts
x✝ :
  { index := i₁, groupElts := g₁ }.index = { index := i₂, groupElts := g₂ }.index ∧
    ∃ g, ⟦g⟧ = { index := i₁, groupElts := g₁ }.groupElts ∧ ⟦g⟧ = { index := i₂, groupElts := g₂ }.groupElts
h : i₁ = i₂
⊢ { index := i₁, groupElts := g₁ } = { index := i₂, groupElts := g₂ }
Module: Mathlib.Combinatorics.SimpleGraph.Tutte

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
x a b c : V
M1 : (G ⊔ edge x b).Subgraph
M2 : (G ⊔ edge a c).Subgraph
hxa : G.Adj x a
hab : G.Adj a b
hnGxb : ¬G.Adj x b
hnGac : ¬G.Adj a c
hnxb : x ≠ b
hnxc : x ≠ c
hnac : a ≠ c
hnbc : b ≠ c
hM1 : M1.IsPerfectMatching
hM2 : M2.IsPerfectMatching
hM1xb : M1.Adj x b
hM2ac : M2.Adj a c
hM1nac : ¬M1.Adj a c
hsupG : G ⊔ edge x b ⊔ (G ⊔ edge a c) = G ⊔ edge a c ⊔ edge x b
cycles : SimpleGraph V := M1.spanningCoe ∆ M2.spanningCoe
hcalt : cycles.IsAlternating M2.spanningCoe
hcycles : (M1.spanningCoe ∆ M2.spanningCoe).IsCycles
⊢ cycles.Adj a c

Tactic:
simp [cycles, symmDiff_def, hM2ac, hM1nac]

Goal state after:
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: case case1
n : ℕ
⊢ (pappAck 0).eval n = Part.some (ack 0 n)

Tactic:
| case1 n =>

Goal state after:
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: x : ℝ
hx : x * 1 = 0
⊢ -x * log x ^ 2 = 0

Tactic:
rw [mul_one] at hx; simp [hx]

Goal state after:
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left✝¹ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
heq : c₁ = c₂
c : ℝ
hc : ∀ᶠ (x : ℝ) in atTop, f x = c
⊢ (∀ᶠ (x : ℝ) in atTop, 0 ≤ f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x ≤ 0

Tactic:
cases le_or_gt 0 c with
    | inl hpos =>
      exact Or.inl <| by filter_upwards [hc] with _ hc; simpa only [hc]
    | inr hneg =>
      right
      filter_upwards [hc] with x hc
      exact le_of_lt <| by simpa only [hc]

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: f : ℕ →. ℕ
⊢ Nat.Partrec f ↔ ∃ c, c.eval = f

Tactic:
refine ⟨fun h => ?_, ?_⟩

Goal state after:
case refine_1
f : ℕ →. ℕ
h : Nat.Partrec f
⊢ ∃ c, c.eval = f

case refine_2
f : ℕ →. ℕ
⊢ (∃ c, c.eval = f) → Nat.Partrec f
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case refine_1.prec
f f✝ g✝ : ℕ →. ℕ
pf : Nat.Partrec f✝
pg : Nat.Partrec g✝
hf : ∃ c, c.eval = f✝
hg : ∃ c, c.eval = g✝
⊢ ∃ c,
    c.eval =
      unpaired fun a n ↦
        Nat.rec (f✝ a)
          (fun y IH ↦ do
            let i ← IH
            g✝ (Nat.pair a (Nat.pair y i)))
          n

Tactic:
| prec pf pg hf hg =>

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: k k₂ : ℕ
c : Code
n x : ℕ
hl : k + 1 ≤ k₂ + 1
h : x ∈ evaln (k + 1) c n
hl' : k ≤ k₂
⊢ x ∈ evaln (k₂ + 1) c n

Tactic:
have :
      ∀ {k k₂ n x : ℕ} {o₁ o₂ : Option ℕ},
        k ≤ k₂ → (x ∈ o₁ → x ∈ o₂) →
          x ∈ do { guard (n ≤ k); o₁ } → x ∈ do { guard (n ≤ k₂); o₂ } := by
      simp only [Option.mem_def, bind, Option.bind_eq_some_iff, Option.guard_eq_some',
        exists_and_left, exists_const, and_imp]
      introv h h₁ h₂ h₃
      exact ⟨le_trans h₂ h, h₁ h₃⟩

Goal state after:
k k₂ : ℕ
c : Code
n x : ℕ
hl : k + 1 ≤ k₂ + 1
h : x ∈ evaln (k + 1) c n
hl' : k ≤ k₂
this :
  ∀ {k k₂ n x : ℕ} {o₁ o₂ : Option ℕ},
    k ≤ k₂ →
      (x ∈ o₁ → x ∈ o₂) →
        (x ∈ do
            guard (n ≤ k)
            o₁) →
          x ∈ do
            guard (n ≤ k₂)
            o₂
⊢ x ∈ evaln (k₂ + 1) c n
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : c₁ ∈ Set.Ioo 0 1
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, c₂ * g ↑n ≤ g u
c₃ : ℝ
hc₃_mem : c₃ ∈ Set.Ioo 0 1
hc₃ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), ↑(r i n) ≤ c₃ * ↑n
hc₁_pos : 0 < c₁
hc₃' : 0 < 1 - c₃
n : ℕ
hn₁ : ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
hn₂ : ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, c₂ * g ↑n ≤ g u
hn₃ : ∀ (i : α), ↑(r i n) ≤ c₃ * ↑n
hrpos : ∀ (i : α), 0 < r i n
hr_lt_n : ∀ (i : α), r i n < n
hn_pos : 0 < n
i : α
hrpos_i : 0 < r i n
g_nonneg : 0 ≤ g ↑n
hp : p a b + 1 < 0
⊢ ↑n ^ p a b * ↑(#(Ico (r i n) n)) * (c₂ * g ↑n / ↑(r i n) ^ (p a b + 1)) ≥
    ↑n ^ p a b * ↑(#(Ico (r i n) n)) * (c₂ * g ↑n / (c₁ * ↑n) ^ (p a b + 1))

Tactic:
by
          gcongr n ^ p a b * #(Ico (r i n) n) * (c₂ * g n / ?_)
          exact rpow_le_rpow_of_nonpos (by positivity) (hn₁ i) (le_of_lt hp)

Goal state after:
Module: Mathlib.Computability.AkraBazzi.AkraBazzi

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ (fun n ↦ 1 * asympBound g a b n) ~[atTop] fun n ↦ (1 + ε ↑n) * asympBound g a b n

Tactic:
refine IsEquivalent.mul (IsEquivalent.symm ?_) IsEquivalent.refl
      rw [Function.const_def, isEquivalent_const_iff_tendsto one_ne_zero,
        ← Function.comp_def (fun n => 1 + ε n) Nat.cast]
      exact Tendsto.comp isEquivalent_one_add_smoothingFn_one.tendsto_const
        tendsto_natCast_atTop_atTop

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case hrf
a : Primrec fun a ↦ ofNat (ℕ × Code) a.length
k✝ : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.length).1
n✝ : Primrec Prod.snd
k : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.length).1
n : Primrec fun a ↦ a.1.2
k' : Primrec Prod.snd
c : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.length).2
L : Primrec fun a ↦ a.1.1.1
⊢ Primrec fun a ↦
    have z := (unpair a.1.1.2).1;
    have m := (unpair a.1.1.2).2;
    do
    let x ← lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.1) (Nat.pair z m)
    Nat.casesOn x (some m) fun x ↦ lup a.1.1.1 (a.1.2, (ofNat (ℕ × Code) a.1.1.1.length).2) (Nat.pair z (m + 1))

Tactic:
have k := k.comp (Primrec.fst (β := Code × Option ℕ))

Goal state after:
case hrf
a : Primrec fun a ↦ ofNat (ℕ × Code) a.length
k✝¹ : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.length).1
n✝ : Primrec Prod.snd
k✝ : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.length).1
n : Primrec fun a ↦ a.1.2
k' : Primrec Prod.snd
c : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.length).2
L : Primrec fun a ↦ a.1.1.1
k : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.1.length).1
⊢ Primrec fun a ↦
    have z := (unpair a.1.1.2).1;
    have m := (unpair a.1.1.2).2;
    do
    let x ← lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.1) (Nat.pair z m)
    Nat.casesOn x (some m) fun x ↦ lup a.1.1.1 (a.1.2, (ofNat (ℕ × Code) a.1.1.1.length).2) (Nat.pair z (m + 1))
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : b ∈ Set.Ioo 0 1
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
hc₂p : 0 < c₂ ^ p
hp : p < 0
hzero : ∀ᶠ (x : ℝ) in atTop, f x = 0
x : ℝ
hx : f x = 0
u : ℝ
hu : u ∈ Set.Icc (b * x) x
hx' : ∀ u ∈ Set.Icc (b * x) x, f u = 0
⊢ 0 ^ p = 0

Tactic:
zero_rpow (ne_of_lt hp)

Goal state after:
f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : b ∈ Set.Ioo 0 1
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
hc₂p : 0 < c₂ ^ p
hp : p < 0
hzero : ∀ᶠ (x : ℝ) in atTop, f x = 0
x : ℝ
hx : f x = 0
u : ℝ
hu : u ∈ Set.Icc (b * x) x
hx' : ∀ u ∈ Set.Icc (b * x) x, f u = 0
⊢ 0 = 0
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: case zero
m i : ℕ
hn : testBit 0 i = false
hm : m.testBit i = true
hnm : ∀ (j : ℕ), i < j → testBit 0 j = m.testBit j
⊢ 0 < m

Tactic:
rw [Nat.pos_iff_ne_zero]
    rintro rfl
    simp at hm

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: f : Code → Code
hf : Computable f
g : ℕ → ℕ → Part ℕ :=
  fun x y ↦ do
    let b ← (ofNat Code x).eval x
    (ofNat Code b).eval y
this : Partrec₂ g
cg : Code
eg : cg.eval = fun n ↦ (↑(decode n)).bind fun a ↦ Part.map encode ((fun p ↦ g p.1 p.2) a)
⊢ ∀ (a n : ℕ), cg.eval (Nat.pair a n) = Part.map encode (g a n)

Tactic:
simp [eg]

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
x : List α
⊢ x ∈ M.accepts ↔ ∃ s ∈ M.start, ∃ t ∈ M.accept, Nonempty (M.Path s t x)

Tactic:
simp only [← mem_evalFrom_iff_nonempty_path, mem_accepts, mem_evalFrom_iff_exists (S := M.start)]
  tauto

Goal state after:
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case true
n : ℕ
ih : ofNat' (n + 1) = ofNat' n + 1
⊢ ofNat' (Nat.bit true n + 1) = ofNat' (Nat.bit true n) + 1

Tactic:
rw [show n.bit true + 1 = (n + 1).bit false by simp [Nat.bit, mul_add],
        ofNat'_bit, ofNat'_bit, ih]
      simp only [cond, add_one, bit1_succ]

Goal state after:
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: α : Type u_1
a b : PosNum
⊢ ∀ (c : PosNum), a ≤ b → b ≤ c → a ≤ c

Tactic:
c

Goal state after:
α : Type u_1
a b c : PosNum
⊢ a ≤ b → b ≤ c → a ≤ c
Module: Mathlib.Computability.RE

Goal state before:
pp: α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ x ∈ k a,
        (x ∈ (↑(decode₂ α a)).bind fun a ↦ Part.map encode (f a)) ∨
          x ∈ (↑(decode₂ α a)).bind fun a ↦ Part.map encode (g a)) ∧
      ((k a).Dom ↔
        ((↑(decode₂ α a)).bind fun a ↦ Part.map encode (f a)).Dom ∨
          ((↑(decode₂ α a)).bind fun a ↦ Part.map encode (g a)).Dom)
k' : α → Part σ := fun a ↦ (k (encode a)).bind fun n ↦ ↑(decode n)
a : α
this : ∀ x ∈ k' a, x ∈ f a ∨ x ∈ g a
h : (f a).Dom ∨ (g a).Dom
⊢ ((↑(decode₂ α (encode a))).bind fun a ↦ Part.map encode (f a)).Dom ∨
    ((↑(decode₂ α (encode a))).bind fun a ↦ Part.map encode (g a)).Dom

Tactic:
simpa only [encodek₂, bind_some, coe_some] using! h

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

Goal state before:
pp: Γ : Type ?u.5
inst✝ : Inhabited Γ
l₁ l₂ : List Γ
h : BlankRel l₁ l₂
⊢ { l // BlankExtends l₁ l ∧ BlankExtends l₂ l }

Tactic:
refine
    if hl : l₁.length ≤ l₂.length then ⟨l₂, Or.elim h id fun h' ↦ ?_, BlankExtends.refl _⟩
    else ⟨l₁, BlankExtends.refl _, Or.elim h (fun h' ↦ ?_) id⟩
  · exact (BlankExtends.refl _).above_of_le h' hl
  · exact (BlankExtends.refl _).above_of_le h' (le_of_not_ge hl)

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

Goal state before:
pp: Γ : Type u_1
inst✝ : Inhabited Γ
a : Γ
L R : ListBlank Γ
n : ℕ
⊢ (move Dir.left { head := a, left := L, right := R }).nth (↑(n + 1) + 1) =
    { head := a, left := L, right := R }.nth (↑(n + 1) + 1 - 1)

Tactic:
add_sub_cancel_right

Goal state after:
Γ : Type u_1
inst✝ : Inhabited Γ
a : Γ
L R : ListBlank Γ
n : ℕ
⊢ (move Dir.left { head := a, left := L, right := R }).nth (↑(n + 1) + 1) =
    { head := a, left := L, right := R }.nth ↑(n + 1)
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: Γ : Type u_1
inst✝ : Inhabited Γ
T : Tape Γ
i : ℤ
⊢ (move Dir.right T).nth i = (move Dir.right T).nth (i + 1 - 1)

Tactic:
add_sub_cancel_right

Goal state after:
Γ : Type u_1
inst✝ : Inhabited Γ
T : Tape Γ
i : ℤ
⊢ (move Dir.right T).nth i = (move Dir.right T).nth i
Module: Mathlib.Computability.Reduce

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
p : α → Prop
f : α → β
c : Computable f
g : β → Bool
hg : Computable g
h₂ : ComputablePred fun a ↦ g a = true
hf : ∀ (a : α), p a ↔ (fun a ↦ g a = true) (f a)
⊢ Computable fun a ↦ decide ((fun a ↦ (fun a ↦ g a = true) (f a)) a)

Tactic:
by simpa using hg.comp c

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

Goal state before:
pp: case branch
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
q₁✝ : Stmt Γ Λ σ
p : Γ → σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ : q₁✝ ∈ stmts₁ q₁ → SupportsStmt S q₁ → SupportsStmt S q₁✝
IH₂ : q₁✝ ∈ stmts₁ q₂ → SupportsStmt S q₂ → SupportsStmt S q₁✝
hs : SupportsStmt S q₁ ∧ SupportsStmt S q₂
h : q₁✝ = branch p q₁ q₂ ∨ q₁✝ ∈ stmts₁ q₁ ∨ q₁✝ ∈ stmts₁ q₂
⊢ SupportsStmt S q₁✝

Tactic:
rcases h with (rfl | h | h); exacts [hs, IH₁ h hs.1, IH₂ h hs.2]

Goal state after:
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case mp.nil
α : Type u_1
inst✝ : DecidableEq α
P : RegularExpression α
IH :
  ∀ (t : List α),
    t.length < [].length → (P.star.rmatch t = true ↔ ∃ S, t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true)
⊢ P.star.rmatch [] = true → ∃ S, [] = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true

pp: case mp.cons
α : 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)
⊢ P.star.rmatch (a :: x) = true → ∃ S, a :: x = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true

Tactic:
· intro _h
        use []; dsimp; tauto

Goal state after:
case mp.cons
α : 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)
⊢ P.star.rmatch (a :: x) = true → ∃ S, a :: x = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case branch
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
q₁✝ : Stmt Γ Λ σ
f : σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ : q₁✝ ∈ stmts₁ q₁ → SupportsStmt S q₁ → SupportsStmt S q₁✝
IH₂ : q₁✝ ∈ stmts₁ q₂ → SupportsStmt S q₂ → SupportsStmt S q₁✝
hs : SupportsStmt S q₁ ∧ SupportsStmt S q₂
h : q₁✝ = branch f q₁ q₂ ∨ q₁✝ ∈ stmts₁ q₁ ∨ q₁✝ ∈ stmts₁ q₂
⊢ SupportsStmt S q₁✝

Tactic:
rcases h with (rfl | h | h); exacts [hs, IH₁ h hs.1, IH₂ h hs.2]

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
S : Finset Λ
k : K
s : StAct K Γ σ k
q : TM2.Stmt Γ Λ σ
⊢ TM2.SupportsStmt S (stRun s q) ↔ TM2.SupportsStmt S q

Tactic:
cases s <;> 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
k : K
s : StAct K Γ σ k
q : TM2.Stmt Γ Λ σ
⊢ trNormal (stRun s q) = goto fun x x_1 ↦ go k s q

Tactic:
cases s <;> rfl

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

Goal state before:
pp: Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst✝¹ : Fintype Γ
inst✝ : Inhabited Λ
S : Finset Λ
ss : Supports M S
q✝ : Λ' Γ Λ σ
h : q✝ ∈ trSupp M S
q : Stmt Γ Λ σ
hs : SupportsStmt S q
hw : ∀ q' ∈ writes q, q' ∈ trSupp M S
⊢ SupportsStmt (trSupp M S) (trNormal dec q) ∧ ∀ q' ∈ writes q, SupportsStmt (trSupp M S) (tr enc dec M q')

Tactic:
induction q with
    | move d q IH =>
      unfold writes at hw ⊢
      replace IH := IH hs hw; refine ⟨?_, IH.2⟩
      cases d <;> simp only [trNormal, supportsStmt_move, IH]
    | write f q IH =>
      unfold writes at hw ⊢
      simp only [Finset.mem_image, Finset.mem_union, Finset.mem_univ, true_and]
        at hw ⊢
      replace IH := IH hs fun q hq ↦ hw q (Or.inr hq)
      refine ⟨supportsStmt_read _ fun a _ s ↦ hw _ (Or.inl ⟨_, rfl⟩), fun q' hq ↦ ?_⟩
      rcases hq with (⟨a, q₂, rfl⟩ | hq)
      · simp only [tr, supportsStmt_write, supportsStmt_move, IH.1]
      · exact IH.2 _ hq
    | load a q IH =>
      unfold writes at hw ⊢
      replace IH := IH hs hw
      exact ⟨supportsStmt_read _ fun _ ↦ IH.1, IH.2⟩
    | branch p q₁ q₂ IH₁ IH₂ =>
      unfold writes at hw ⊢
      simp only [Finset.mem_union] at hw ⊢
      replace IH₁ := IH₁ hs.1 fun q hq ↦ hw q (Or.inl hq)
      replace IH₂ := IH₂ hs.2 fun q hq ↦ hw q (Or.inr hq)
      exact ⟨supportsStmt_read _ fun _ ↦ ⟨IH₁.1, IH₂.1⟩, fun q ↦ Or.rec (IH₁.2 _) (IH₂.2 _)⟩
    | goto l =>
      simp only [writes, Finset.notMem_empty]; refine ⟨?_, fun _ ↦ False.elim⟩
      refine supportsStmt_read _ fun a _ s ↦ ?_
      exact Finset.mem_biUnion.2 ⟨_, hs _ _, Finset.mem_insert_self _ _⟩
    | halt =>
      simp only [writes, Finset.notMem_empty]; refine ⟨?_, fun _ ↦ False.elim⟩
      simp only [SupportsStmt, trNormal]

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

Goal state before:
pp: Γ : Type u_1
inst✝¹ : Inhabited Γ
Λ : Type u_2
inst✝ : Inhabited Λ
M : TM0.Machine Γ Λ
x✝ : TM0.Cfg Γ Λ
q : Λ
T : Tape Γ
q' : Λ
s : TM0.Stmt Γ
⊢ TM1.step (tr M) { l := some (Λ'.act s q'), var := (), Tape := T } =
    some
      { l := some (Λ'.normal q'), var := (),
        Tape :=
          match s with
          | TM0.Stmt.move d => Tape.move d T
          | TM0.Stmt.write a => Tape.write a T }

Tactic:
cases s <;> rfl

Goal state after: