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

Goal state before:
pp: V : Type u_1
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
α : Type u_2
inst✝¹ : Fintype α
inst✝ : Nontrivial α
⊢ G.IsExtremal ⊤.Free ↔ G.IsExtremal fun x ↦ x.CliqueFree (Fintype.card α - 1 + 1)

Tactic:
IsExtremal,

Goal state after:
V : Type u_1
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
α : Type u_2
inst✝¹ : Fintype α
inst✝ : Nontrivial α
⊢ (⊤.Free G ∧ ∀ ⦃G' : SimpleGraph V⦄ [inst : DecidableRel G'.Adj], ⊤.Free G' → #G'.edgeFinset ≤ #G.edgeFinset) ↔
    G.CliqueFree (Fintype.card α - 1 + 1) ∧
      ∀ ⦃G' : SimpleGraph V⦄ [inst : DecidableRel G'.Adj],
        G'.CliqueFree (Fintype.card α - 1 + 1) → #G'.edgeFinset ≤ #G.edgeFinset
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity

Goal state before:
pp: W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
G : SimpleGraph (Fin (n + 1))
inst✝ : DecidableRel G.Adj
h : H.Free G
⊢ ↑(n.choose 2) * ↑(#G.edgeFinset) ≤ ↑((n + 1).choose 2) * ↑(extremalNumber n H)

Tactic:
Nat.cast_choose_two,

Goal state after:
W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
G : SimpleGraph (Fin (n + 1))
inst✝ : DecidableRel G.Adj
h : H.Free G
⊢ ↑n * (↑n - 1) / 2 * ↑(#G.edgeFinset) ≤ ↑((n + 1).choose 2) * ↑(extremalNumber n H)
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity

Goal state before:
pp: W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
G : SimpleGraph (Fin (n + 1))
inst✝ : DecidableRel G.Adj
h : H.Free G
⊢ ↑n * (↑n - 1) / 2 * ↑(#G.edgeFinset) ≤ ↑((n + 1).choose 2) * ↑(extremalNumber n H)

Tactic:
Nat.cast_choose_two,

Goal state after:
W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
G : SimpleGraph (Fin (n + 1))
inst✝ : DecidableRel G.Adj
h : H.Free G
⊢ ↑n * (↑n - 1) / 2 * ↑(#G.edgeFinset) ≤ ↑(n + 1) * (↑(n + 1) - 1) / 2 * ↑(extremalNumber n H)
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: case neg
α : Type u_1
ι : Type u_2
t : Set ι
ht : t.Finite
s : ι → Set α
hs : t.PairwiseDisjoint s
i : ι
hi : i ∈ t
hn : (s i).Infinite
⊢ (⋃ i ∈ t, s i).encard = ∑ᶠ (i : ι) (_ : i ∈ t), (s i).encard

Tactic:
← Set.insert_sdiff_self_of_mem hi,

Goal state after:
case neg
α : Type u_1
ι : Type u_2
t : Set ι
ht : t.Finite
s : ι → Set α
hs : t.PairwiseDisjoint s
i : ι
hi : i ∈ t
hn : (s i).Infinite
⊢ (⋃ i_1 ∈ insert i (t \ {i}), s i_1).encard = ∑ᶠ (i_1 : ι) (_ : i_1 ∈ insert i (t \ {i})), (s i_1).encard
Module: Mathlib.Combinatorics.SimpleGraph.Hall

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
p : Set V
inst✝ : DecidablePred fun x ↦ x ∈ p
f : ↑p → V
h₁ : ∀ (x : ↑p), f x ∉ p
h₂ : ∀ (x : ↑p), G.Adj (↑x) (f x)
v w : V
h✝ : v ∈ p
h : f ⟨v, h✝⟩ = w
⊢ v ∈ p

Tactic:
by assumption

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
p : Set V
inst✝ : DecidablePred fun x ↦ x ∈ p
f : ↑p → V
h₁ : ∀ (x : ↑p), f x ∉ p
h₂ : ∀ (x : ↑p), G.Adj (↑x) (f x)
v w : V
h✝¹ : v ∉ p
h✝ : w ∈ p
h : f ⟨w, h✝⟩ = v
⊢ w ∈ p

Tactic:
by assumption

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
r : ℕ
inst✝ : DecidableEq α
h : Maximal (fun H ↦ H.CliqueFree (r + 2)) G
hnc : ¬G.IsCompleteMultipartite
w✝² w✝¹ w✝ : α
s t : Finset α
hw : G.IsFiveWheelLike r (#(s ∩ t)) w✝² w✝¹ w✝ s t
⊢ ∃ k v w₁ w₂ s t, G.IsFiveWheelLike r k v w₁ w₂ s t ∧ k < r ∧ ∀ (j : ℕ), k < j → G.FiveWheelLikeFree r j

Tactic:
let P : ℕ → Prop := fun k ↦ ∃ v w₁ w₂ s t, G.IsFiveWheelLike r k v w₁ w₂ s t

Goal state after:
α : Type u_1
G : SimpleGraph α
r : ℕ
inst✝ : DecidableEq α
h : Maximal (fun H ↦ H.CliqueFree (r + 2)) G
hnc : ¬G.IsCompleteMultipartite
w✝² w✝¹ w✝ : α
s t : Finset α
hw : G.IsFiveWheelLike r (#(s ∩ t)) w✝² w✝¹ w✝ s t
P : ℕ → Prop := fun k ↦ ∃ v w₁ w₂ s t, G.IsFiveWheelLike r k v w₁ w₂ s t
⊢ ∃ k v w₁ w₂ s t, G.IsFiveWheelLike r k v w₁ w₂ s t ∧ k < r ∧ ∀ (j : ℕ), k < j → G.FiveWheelLikeFree r j
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits

Goal state before:
pp: case inr
ε : ℝ
hε : 0 < ε
r t : ℕ
hr_pos : 0 < r
ht_pos : 0 < t
ε' : ℝ := 1 / (↑(r - 1) * ↑r) + ε
⊢ ∀ᶠ (n : ℕ) in atTop,
    ∀ {G : SimpleGraph (Fin n)} [inst : DecidableRel G.Adj],
      ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n → completeEquipartiteGraph (r + 1) t ⊑ G

Tactic:
have hε' : 0 < ε' := by positivity

Goal state after:
case inr
ε : ℝ
hε : 0 < ε
r t : ℕ
hr_pos : 0 < r
ht_pos : 0 < t
ε' : ℝ := 1 / (↑(r - 1) * ↑r) + ε
hε' : 0 < ε'
⊢ ∀ᶠ (n : ℕ) in atTop,
    ∀ {G : SimpleGraph (Fin n)} [inst : DecidableRel G.Adj],
      ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n → completeEquipartiteGraph (r + 1) t ⊑ G
Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
G : SimpleGraph α
a : α
p : G.Walk a a
⊢ p.IsHamiltonianCycle ↔ p.IsCycle ∧ ∀ (a_1 : α), List.count a_1 p.support.tail = 1

Tactic:
simp +contextual [isHamiltonianCycle_isCycle_and_isHamiltonian_tail,
    IsHamiltonian, support_tail_of_not_nil, IsCycle.not_nil]

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

Goal state before:
pp: V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
x : V → ℝ
⊢ lapMatrix ℝ G *ᵥ x = 0 ↔ ∀ (i j : V), G.Adj i j → x i = x j

Tactic:
rw [← (posSemidef_lapMatrix ℝ G).toLinearMap₂'_zero_iff, star_trivial,
      lapMatrix_toLinearMap₂'_apply'_eq_zero_iff_forall_adj]

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

Goal state before:
pp: V : Type u_1
G G' : SimpleGraph V
u x : V
halt : G.IsAlternating G'
hnadj : ¬G'.Adj u x
hu' : ∀ (u' : V), u' ≠ u → G.Adj x u' → G'.Adj x u'
hx' : ∀ (x' : V), x' ≠ x → G.Adj x' u → G'.Adj x' u
⊢ (G ⊔ edge u x).IsAlternating G'

Tactic:
by
  by_cases hadj : G.Adj u x
  · rwa [sup_edge_of_adj G hadj]
  intro v w w' hww' hvw hvv'
  simp only [sup_adj, edge_adj] at hvw hvv'
  obtain hl | hr := hvw <;> obtain h1 | h2 := hvv'
  · exact halt hww' hl h1
  · rw [G'.adj_congr_of_sym2 (by grind : s(v, w') = s(u, x))]
    simp only [hnadj, not_false_eq_true, iff_true]
    rcases h2.1 with ⟨rfl, rfl⟩ | ⟨h2r1, h2r2⟩
    · exact (hx' _ hww' hl.symm).symm
    · simp_all
  · rw [G'.adj_congr_of_sym2 (by grind : s(v, w) = s(u, x))]
    simp only [hnadj, false_iff, not_not]
    rcases hr.1 with ⟨rfl, rfl⟩ | ⟨hrr1, hrr2⟩
    · exact (hx' _ hww'.symm h1.symm).symm
    · grind
  · grind

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

Goal state before:
pp: case mpr
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : G.Walk u v
⊢ (p.IsTrail ∧ ∀ e ∈ G.edgeSet, e ∈ p.edges) → p.IsEulerian

Tactic:
rintro ⟨h, hl⟩

Goal state after:
case mpr
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : G.Walk u v
h : p.IsTrail
hl : ∀ e ∈ G.edgeSet, e ∈ p.edges
⊢ p.IsEulerian
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case false.inr
p : ℕ →. Bool
H : ∃ n, true ∈ p n ∧ ∀ k < n, (p k).Dom
m : ℕ
IH : (y : ℕ) → lbp p y m → (∀ n < y, false ∈ p n) → { n // true ∈ p n ∧ ∀ m < n, false ∈ p m }
al : ∀ n < m, false ∈ p n
pm : (p m).Dom
e : (p m).get pm = false
n : ℕ
h✝ : n ≤ m
h : n = m
⊢ false ∈ p m

Tactic:
exact ⟨_, e⟩

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case zero
f : ℕ → ℕ
⊢ Nat.Partrec ↑fun x ↦ 0

Tactic:
exact zero

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → σ
hf : Primrec f
n : ℕ
⊢ (do
      let n ← (↑fun n ↦ encode (Option.map f (decode n))) n
      ↑n.ppred) =
    (↑(decode n)).bind fun a ↦ map encode (↑f a)

Tactic:
simp; cases decode (α := α) n <;> simp

Goal state after:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: case pair
n : ℕ
f✝¹ : List.Vector ℕ n → ℕ
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
hf : Primrec' fun v ↦ f✝ v.head
hg : Primrec' fun v ↦ g✝ v.head
⊢ Primrec' fun v ↦ (fun n ↦ pair (f✝ n) (g✝ n)) v.head

Tactic:
| pair _ _ hf hg =>

Goal state after:
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: case succ
n : ℕ
IH : ack 3 n = 2 ^ (n + 3) - 3
⊢ 2 * 2 ^ (n + 3) - 2 * 3 + 3 = 2 * 2 ^ (n + 3) - 3

Tactic:
← Nat.sub_add_comm,

Goal state after:
case succ
n : ℕ
IH : ack 3 n = 2 ^ (n + 3) - 3
⊢ 2 * 2 ^ (n + 3) + 3 - 2 * 3 = 2 * 2 ^ (n + 3) - 3

case succ
n : ℕ
IH : ack 3 n = 2 ^ (n + 3) - 3
⊢ 2 * 3 ≤ 2 * 2 ^ (n + 3)
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: case succ
k : ℕ
a✝ : k ^ 2 ≤ 2 ^ (k + 1) - 3
⊢ (k + 1) ^ 2 ≤ 2 ^ (k + 1 + 1) - 3

Tactic:
cases k

Goal state after:
case succ.zero
a✝ : 0 ^ 2 ≤ 2 ^ (0 + 1) - 3
⊢ (0 + 1) ^ 2 ≤ 2 ^ (0 + 1 + 1) - 3

case succ.succ
n✝ : ℕ
a✝ : (n✝ + 1) ^ 2 ≤ 2 ^ (n✝ + 1 + 1) - 3
⊢ (n✝ + 1 + 1) ^ 2 ≤ 2 ^ (n✝ + 1 + 1 + 1) - 3
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: this : Primrec fun t ↦ Nat.rec succ (fun x c ↦ pappAck.step c) t
⊢ Primrec pappAck

Tactic:
convert! this using 2 with n; induction n <;> simp [pappAck, *]

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

Goal state before:
pp: case h₂
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
n : ℕ
hn : ∀ (i : α), ‖↑(r i n) - b i * ↑n‖ ≤ ↑n / log ↑n ^ 2
i : α
⊢ ↑(r i n) - b i * ↑n ≤ ‖↑(r i n) - b i * ↑n‖

Tactic:
exact Real.le_norm_self _

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: cf cg : Code
a k : ℕ
⊢ (cf.prec cg).eval (Nat.pair a k.succ) = do
    let ih ← (cf.prec cg).eval (Nat.pair a k)
    cg.eval (Nat.pair a (Nat.pair k ih))

Tactic:
rw [eval, Nat.unpaired, Part.bind_eq_bind, Nat.unpair_pair]

Goal state after:
cf cg : Code
a k : ℕ
⊢ Nat.rec (cf.eval (a, k.succ).1)
      (fun y IH ↦ do
        let i ← IH
        cg.eval (Nat.pair (a, k.succ).1 (Nat.pair y i)))
      (a, k.succ).2 =
    (unpaired
          (fun a n ↦
            Nat.rec (cf.eval a)
              (fun y IH ↦ do
                let i ← IH
                cg.eval (Nat.pair a (Nat.pair y i)))
              n)
          (Nat.pair a k)).bind
      fun ih ↦ cg.eval (Nat.pair a (Nat.pair k ih))
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: case lb
f g : ℝ → ℝ
hf✝ : GrowsPolynomially f
hfg : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 1 / 2 * ‖f x‖
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_ub : b < 1
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : 0 < c₂
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hfg' : ∀ (y : ℝ), b * id x ≤ y → ‖g y‖ ≤ 1 / 2 * ‖f y‖
hf₂ : ∀ (y : ℝ), b * id x ≤ y → f y ≤ 0
hx_nonneg : 0 ≤ x
hbx : b * x ≤ x
hfg₂ : ‖g x‖ ≤ -1 / 2 * f x
hx_ub : f x + g x ≤ 1 / 2 * f x
hx_lb : 3 / 2 * f x ≤ f x + g x
u : ℝ
hu_lb : b * x ≤ u
hu_ub : u ≤ x
hfu_nonpos : f u ≤ 0
hfg₃ : ‖g u‖ ≤ -1 / 2 * f u
⊢ 3 * c₁ * (f x + g x) ≤ f u + g u

pp: case ub
f g : ℝ → ℝ
hf✝ : GrowsPolynomially f
hfg : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 1 / 2 * ‖f x‖
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_ub : b < 1
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : 0 < c₂
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hfg' : ∀ (y : ℝ), b * id x ≤ y → ‖g y‖ ≤ 1 / 2 * ‖f y‖
hf₂ : ∀ (y : ℝ), b * id x ≤ y → f y ≤ 0
hx_nonneg : 0 ≤ x
hbx : b * x ≤ x
hfg₂ : ‖g x‖ ≤ -1 / 2 * f x
hx_ub : f x + g x ≤ 1 / 2 * f x
hx_lb : 3 / 2 * f x ≤ f x + g x
u : ℝ
hu_lb : b * x ≤ u
hu_ub : u ≤ x
hfu_nonpos : f u ≤ 0
hfg₃ : ‖g u‖ ≤ -1 / 2 * f u
⊢ f u + g u ≤ c₂ / 3 * (f x + g x)

Tactic:
case lb =>
      calc f u + g u ≥ f u - ‖g u‖ := by
                  rw [sub_eq_add_neg, norm_eq_abs]; gcongr; exact neg_abs_le _
           _ ≥ f u + 1 / 2 * f u := by
                  rw [sub_eq_add_neg]
                  gcongr
                  refine le_of_neg_le_neg ?_
                  rwa [neg_neg, ← neg_mul, ← neg_div]
           _ = 3 / 2 * f u := by ring
           _ ≥ 3 / 2 * (c₁ * f x) := by gcongr; exact (hf₁ u ⟨hu_lb, hu_ub⟩).1
           _ = 3 * c₁ * (1 / 2 * f x) := by ring
           _ ≥ 3 * c₁ * (f x + g x) := by gcongr

Goal state after:
case ub
f g : ℝ → ℝ
hf✝ : GrowsPolynomially f
hfg : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 1 / 2 * ‖f x‖
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_ub : b < 1
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : 0 < c₂
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hfg' : ∀ (y : ℝ), b * id x ≤ y → ‖g y‖ ≤ 1 / 2 * ‖f y‖
hf₂ : ∀ (y : ℝ), b * id x ≤ y → f y ≤ 0
hx_nonneg : 0 ≤ x
hbx : b * x ≤ x
hfg₂ : ‖g x‖ ≤ -1 / 2 * f x
hx_ub : f x + g x ≤ 1 / 2 * f x
hx_lb : 3 / 2 * f x ≤ f x + g x
u : ℝ
hu_lb : b * x ≤ u
hu_ub : u ≤ x
hfu_nonpos : f u ≤ 0
hfg₃ : ‖g u‖ ≤ -1 / 2 * f u
⊢ f u + g u ≤ c₂ / 3 * (f x + g x)
Module: Mathlib.Computability.Language

Goal state before:
pp: case a.h.inl
α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m * l + n
a : List α
ha : a ∈ m
b : List α
hb : b ∈ l
ih : b ∈ m∗ * n
hx : a ++ b ∈ m * l
hal : 0 < a.length
⊢ a ++ b ∈ m∗ * n

Tactic:
← one_add_self_mul_kstar_eq_kstar,

Goal state after:
case a.h.inl
α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m * l + n
a : List α
ha : a ∈ m
b : List α
hb : b ∈ l
ih : b ∈ m∗ * n
hx : a ++ b ∈ m * l
hal : 0 < a.length
⊢ a ++ b ∈ (1 + m * m∗) * n
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f : ℝ → ℝ
hf : GrowsPolynomially f
this : GrowsPolynomially fun x ↦ |(f x)⁻¹|
hf' : ∀ᶠ (x : ℝ) in atTop, 0 < f x
⊢ (fun x ↦ (f x)⁻¹) =ᶠ[atTop] fun x ↦ |(f x)⁻¹|

Tactic:
filter_upwards [hf'] with x hx₁

Goal state after:
f : ℝ → ℝ
hf : GrowsPolynomially f
this : GrowsPolynomially fun x ↦ |(f x)⁻¹|
hf' : ∀ᶠ (x : ℝ) in atTop, 0 < f x
x : ℝ
hx₁ : 0 < f x
⊢ (f x)⁻¹ = |(f x)⁻¹|
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f : ℝ → ℝ
hf : GrowsPolynomially f
this : GrowsPolynomially fun x ↦ |(f x)⁻¹|
hf' : ∀ᶠ (x : ℝ) in atTop, f x < 0
⊢ (fun x ↦ (f x)⁻¹) =ᶠ[atTop] fun x ↦ -|(f x)⁻¹|

Tactic:
filter_upwards [hf'] with x hx₁

Goal state after:
f : ℝ → ℝ
hf : GrowsPolynomially f
this : GrowsPolynomially fun x ↦ |(f x)⁻¹|
hf' : ∀ᶠ (x : ℝ) in atTop, f x < 0
x : ℝ
hx₁ : f x < 0
⊢ (f x)⁻¹ = -|(f x)⁻¹|
Module: Mathlib.Computability.DFA

Goal state before:
pp: case append_singleton
α : Type u
σ : Type v
M : DFA α σ
α' : Type u_1
f : α' → α
s : σ
x : List α'
a : α'
ih : (comap f M).evalFrom s x = M.evalFrom s (List.map f x)
⊢ (comap f M).evalFrom s (x ++ [a]) = M.evalFrom s (List.map f (x ++ [a]))

Tactic:
simp [ih]

Goal state after:
Module: Mathlib.Computability.DFA

Goal state before:
pp: case append_singleton
α : Type u
σ : Type v
M : DFA α σ
σ' : Type u_2
g : σ ≃ σ'
s : σ'
x : List α
a : α
ih : ((reindex g) M).evalFrom s x = g (M.evalFrom (g.symm s) x)
⊢ ((reindex g) M).evalFrom s (x ++ [a]) = g (M.evalFrom (g.symm s) (x ++ [a]))

Tactic:
simp [ih]

Goal state after:
Module: Mathlib.Computability.DFA

Goal state before:
pp: α : Type u
σ1 σ2 : Type v
M1 : DFA α σ1
M2 : DFA α σ2
s1 : σ1
s2 : σ2
x : List α
⊢ (M1.union M2).evalFrom (s1, s2) x ∈ (M1.union M2).accept ↔ M1.evalFrom s1 x ∈ M1.accept ∨ M2.evalFrom s2 x ∈ M2.accept

Tactic:
induction x generalizing s1 s2 with
  | nil => simp
  | cons a x ih => simp only [evalFrom_cons, union_step, ih]

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

Goal state before:
pp: case bit
b✝ : Bool
n✝ : ℕ
h : n✝ = 0 → b✝ = true
ih : n✝.bits.length = n✝.size
⊢ (b✝ :: n✝.bits).length = n✝.size.succ

Tactic:
simp [ih]

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

Goal state before:
pp: case bit
f : Bool → Bool → Bool
bm : Bool
m : ℕ
hm : m = 0 → bm = true
ihm : ∀ (n : ℕ), bitwise (swap f) m n = bitwise f n m
n : ℕ
⊢ bitwise (swap f) (bit bm m) n = bitwise f n (bit bm m)

Tactic:
| bit bm m hm ihm =>

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

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
n : PosNum
⊢ ↑↑n = ↑n

Tactic:
by
  rw [← to_nat_to_int, Int.cast_natCast, cast_to_nat]

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
a : α
⊢ M.stepSet ∅ a = ∅

Tactic:
by simp [stepSet]

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: case cons
α : Type u
σ : Type v
M : NFA α σ
a : α
x : List α
ih : ∀ (S T : Set σ), M.evalFrom (S ∪ T) x = M.evalFrom S x ∪ M.evalFrom T x
S T : Set σ
⊢ M.evalFrom (S ∪ T) (a :: x) = M.evalFrom S (a :: x) ∪ M.evalFrom T (a :: x)

Tactic:
simp [ih]

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
s t : σ
x✝ : List α
a : α
x : List α
h : t ∈ M.evalFrom (M.stepSet {s} a) x
⊢ ∃ s' ∈ M.step s a, t ∈ M.evalFrom {s'} x

Tactic:
mem_evalFrom_iff_exists,

Goal state after:
α : Type u
σ : Type v
M : NFA α σ
s t : σ
x✝ : List α
a : α
x : List α
h : ∃ t_1 ∈ M.stepSet {s} a, t ∈ M.evalFrom {t_1} x
⊢ ∃ s' ∈ M.step s a, t ∈ M.evalFrom {s'} x
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: case nil
α : Type u
σ : Type v
M : εNFA α σ
⊢ M.εClosure ∅ = ∅

Tactic:
εClosure_empty

Goal state after:
case nil
α : Type u
σ : Type v
M : εNFA α σ
⊢ ∅ = ∅
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: x✝² x✝¹ x✝ : Num
⊢ (x✝² + x✝¹) * x✝ = x✝² * x✝ + x✝¹ * x✝

Tactic:
by simp only [← to_nat_inj, mul_to_nat, add_to_nat, add_mul]

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

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
n : Num
⊢ ↑↑n = ↑n

Tactic:
by
  rw [← to_nat_to_int, Int.cast_natCast, cast_to_nat]

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

Goal state before:
pp: m n : PosNum
h : ↑m = ↑n
⊢ pos m = pos n

Tactic:
rw [← PosNum.of_to_nat, ← PosNum.of_to_nat, h]

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

Goal state before:
pp: n : PosNum
⊢ (↑n).size + 1 = (Nat.bit false ↑n).size

Tactic:
Nat.size_bit

Goal state after:
n : PosNum
⊢ (↑n).size + 1 = (↑n).size.succ

n : PosNum
⊢ Nat.bit false ↑n ≠ 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: n : PosNum
⊢ (↑n).size + 1 = (Nat.bit true ↑n).size

Tactic:
Nat.size_bit

Goal state after:
n : PosNum
⊢ (↑n).size + 1 = (↑n).size.succ

n : PosNum
⊢ Nat.bit true ↑n ≠ 0
Module: Mathlib.Computability.PartrecBasis

Goal state before:
pp: n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
hf : Partrec' ↑f
v : List.Vector ℕ n
b : ℕ
⊢ (b ∈ (Nat.rfind fun n_1 ↦ Part.some (decide (1 - f (n_1 ::ᵥ v) = 0))).bind fun a ↦ ↑pred (f (a ::ᵥ v))) ↔
    b ∈ Nat.rfindOpt fun a ↦ ofNat (Option ℕ) (f (a ::ᵥ v))

Tactic:
by
      simp only [Nat.rfindOpt, Nat.sub_eq_zero_iff_le, PFun.coe_val, Part.mem_bind_iff,
        Part.mem_some_iff, Option.mem_def, Part.mem_coe]
      refine
        exists_congr fun a => (and_congr (iff_of_eq ?_) Iff.rfl).trans (and_congr_right fun h => ?_)
      · congr
        funext n
        cases f (n ::ᵥ v) <;> simp <;> rfl
      · have := Nat.rfind_spec h
        simp only [Part.coe_some, Part.mem_some_iff] at this
        revert this; rcases f (a ::ᵥ v) with - | c <;> intro this
        · cases this
        rw [← Option.some_inj, eq_comm]
        rfl

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

Goal state before:
pp: ⊢ ∀ (m n : Num), ↑(m.ldiff n) = (↑m).ldiff ↑n

Tactic:
apply castNum_eq_bitwise PosNum.ldiff <;> intros

Goal state after:
case gff
⊢ (false && !false) = false

case f00
⊢ ldiff 0 0 = 0

case f0n
n✝ : PosNum
⊢ ldiff 0 (pos n✝) = bif false && !true then pos n✝ else 0

case fn0
n✝ : PosNum
⊢ (pos n✝).ldiff 0 = bif true && !false then pos n✝ else 0

case fnn
m✝ n✝ : PosNum
⊢ (pos m✝).ldiff (pos n✝) = m✝.ldiff n✝

case p11
⊢ PosNum.ldiff 1 1 = bif true && !true then 1 else 0

case p1b
b✝ : Bool
n✝ : PosNum
⊢ PosNum.ldiff 1 (PosNum.bit b✝ n✝) = bit (true && !b✝) (bif false && !true then pos n✝ else 0)

case pb1
a✝ : Bool
m✝ : PosNum
⊢ (PosNum.bit a✝ m✝).ldiff 1 = bit (a✝ && !true) (bif true && !false then pos m✝ else 0)

case pbb
a✝ b✝ : Bool
m✝ n✝ : PosNum
⊢ (PosNum.bit a✝ m✝).ldiff (PosNum.bit b✝ n✝) = bit (a✝ && !b✝) (m✝.ldiff n✝)
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
this :
  ∀ (L R : ListBlank (Γ' K Γ)) (n : ℕ),
    Tape.write ((R.nth n).1, update (R.nth n).2 k (some (f v))) ((Tape.move Dir.right)^[n] (Tape.mk' L R)) =
      (Tape.move Dir.right)^[n] (Tape.mk' L (ListBlank.modifyNth (fun a ↦ (a.1, update a.2 k (some (f v)))) n R))
k' : K
i : ℕ
⊢ (proj k').f ((ListBlank.modifyNth (fun a ↦ update a k (some (f v))) (S k).length L).nth i) =
    (ListBlank.mk (List.map some (update S k (f v :: S k) k')).reverse).nth i

Tactic:
ListBlank.nth_modifyNth,

Goal state after:
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
this :
  ∀ (L R : ListBlank (Γ' K Γ)) (n : ℕ),
    Tape.write ((R.nth n).1, update (R.nth n).2 k (some (f v))) ((Tape.move Dir.right)^[n] (Tape.mk' L R)) =
      (Tape.move Dir.right)^[n] (Tape.mk' L (ListBlank.modifyNth (fun a ↦ (a.1, update a.2 k (some (f v)))) n R))
k' : K
i : ℕ
⊢ (proj k').f (if i = (S k).length then update (L.nth i) k (some (f v)) else L.nth i) =
    (ListBlank.mk (List.map some (update S k (f v :: S k) k')).reverse).nth i
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case pop.cons
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
k : K
q : TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse
f : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
k' : K
i : ℕ
⊢ (proj k').f ((ListBlank.modifyNth (fun a ↦ update a k none) tl.length L).nth i) =
    (ListBlank.mk (List.map some (update S k (hd :: tl).tail k')).reverse).nth i

Tactic:
ListBlank.nth_modifyNth,

Goal state after:
case pop.cons
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
k : K
q : TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse
f : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
k' : K
i : ℕ
⊢ (proj k').f (if i = tl.length then update (L.nth i) k none else L.nth i) =
    (ListBlank.mk (List.map some (update S k (hd :: tl).tail k')).reverse).nth i
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case cons₁
k' : Cont
a✝² : Code
a✝¹ : List ℕ
a✝ : Cont
a_ih✝ : ∀ {v : List ℕ}, stepRet (a✝.then k') v = (stepRet a✝ v).then k'
v : List ℕ
⊢ stepNormal a✝² (Cont.cons₂ v (a✝.then k')) a✝¹ = (stepNormal a✝² (Cont.cons₂ v a✝) a✝¹).then k'

Tactic:
← stepNormal_then

Goal state after:
case cons₁
k' : Cont
a✝² : Code
a✝¹ : List ℕ
a✝ : Cont
a_ih✝ : ∀ {v : List ℕ}, stepRet (a✝.then k') v = (stepRet a✝ v).then k'
v : List ℕ
⊢ stepNormal a✝² (Cont.cons₂ v (a✝.then k')) a✝¹ = stepNormal a✝² ((Cont.cons₂ v a✝).then k') a✝¹
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case comp
k' : Cont
a✝¹ : Code
a✝ : Cont
a_ih✝ : ∀ {v : List ℕ}, stepRet (a✝.then k') v = (stepRet a✝ v).then k'
v : List ℕ
⊢ stepNormal a✝¹ (a✝.then k') v = (stepNormal a✝¹ a✝ v).then k'

Tactic:
← stepNormal_then

Goal state after:
case comp
k' : Cont
a✝¹ : Code
a✝ : Cont
a_ih✝ : ∀ {v : List ℕ}, stepRet (a✝.then k') v = (stepRet a✝ v).then k'
v : List ℕ
⊢ stepNormal a✝¹ (a✝.then k') v = stepNormal a✝¹ (a✝.then k') v