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

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : G.Walk u v
s : Finset V
h✝ : {x ∈ s | x ∈ p.support}.Nonempty
x : V
hxs : x ∈ s
hx : x ∈ p.support
h : {t ∈ s.erase x | t ∈ (p.takeUntil x hx).support} = ∅
this : {t ∈ s | t ∈ (p.takeUntil x hx).support} ⊆ {x}
⊢ ∀ t ∈ s, t ∈ (p.takeUntil x hx).support → t = x

Tactic:
simpa [Finset.subset_iff] using this

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Preorder α
a b : α
⊢ ∀ {a b : αᵒᵈ}, (hasse α).Adj (ofDual a) (ofDual b) ↔ (hasse αᵒᵈ).Adj a b

Tactic:
simp [or_comm]

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

Goal state before:
pp: α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : Semiring α
n : ℕ
u v : V
⊢ (adjMatrix α G ^ n) u v = ↑(#(G.finsetWalkLength n u v))

Tactic:
induction n generalizing u v with
  | zero => obtain rfl | h := eq_or_ne u v <;> simp [finsetWalkLength, *]
  | succ n ih =>
    simp only [pow_succ', finsetWalkLength, ih, adjMatrix_mul_apply]
    rw [Finset.card_biUnion]
    · norm_cast
      simp only [Nat.cast_sum, card_map, neighborFinset_def]
      apply Finset.sum_toFinset_eq_subtype
    -- Disjointness for card_bUnion
    · rintro ⟨x, hx⟩ - ⟨y, hy⟩ - hxy
      rw [Function.onFun, disjoint_iff_inf_le]
      intro p hp
      simp only [inf_eq_inter, mem_inter, mem_map] at hp
      obtain ⟨⟨px, _, rfl⟩, ⟨py, hpy, hp⟩⟩ := hp
      cases hp
      simp at hxy

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions

Goal state before:
pp: n : ℕ
h : 2 ≤ n
hOdd : Odd n
⊢ (cycleGraph n).chromaticNumber = 3

Tactic:
by
  have hc := (cycleGraph.tricoloring n h).colorable
  apply le_antisymm
  · apply hc.chromaticNumber_le
  · have hn3 : n - 3 + 3 = n := by
      refine Nat.sub_add_cancel (Nat.succ_le_of_lt (Nat.lt_of_le_of_ne h ?_))
      intro h2
      rw [← h2] at hOdd
      exact (Nat.not_odd_iff.mpr rfl) hOdd
    let w : (cycleGraph (n - 3 + 3)).Walk 0 0 := cycleGraph.cycle (n - 3)
    have hOdd' : Odd w.length := by
      rw [cycleGraph.length_cycle, hn3]
      exact hOdd
    rw [← hn3]
    exact Walk.three_le_chromaticNumber_of_odd_loop w hOdd'

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
⊢ G.Reachable u v ↔ ∃ n, (G.finsetWalkLength (↑n) u v).Nonempty

Tactic:
constructor
  · intro r
    refine r.elim_path fun p => ?_
    refine ⟨⟨_, p.isPath.length_lt⟩, p, ?_⟩
    simp [mem_finsetWalkLength_iff]
  · rintro ⟨_, p, _⟩
    exact ⟨p⟩

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

Goal state before:
pp: case refine_2.a
α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v : Fin r × Fin t
⊢ ↑⟨↑v.2 * r + ↑v.1, ⋯⟩ ≤ r * ↑v.2 + (r - 1)

Tactic:
mul_comm r ↑v.2

Goal state after:
case refine_2.a
α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v : Fin r × Fin t
⊢ ↑⟨↑v.2 * r + ↑v.1, ⋯⟩ ≤ ↑v.2 * r + (r - 1)
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: case h₁.inl
n : ℕ
⊢ (n % 0 - 1) * 0 ≤ (0 - 1) * (n % 0)

pp: case h₁.inr
n r : ℕ
hr : r > 0
⊢ (n % r - 1) * r ≤ (r - 1) * (n % r)

Tactic:
· lia

Goal state after:
case h₁.inr
n r : ℕ
hr : r > 0
⊢ (n % r - 1) * r ≤ (r - 1) * (n % r)
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Zarankiewicz

Goal state before:
pp: case hb
n s t : ℕ
α : Type u_3
β : Type u_4
inst✝⁴ : Fintype α
inst✝³ : Fintype β
inst✝² : Nonempty α
inst✝¹ : Nonempty β
hs : Fintype.card α = s
ht : Fintype.card β = t
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
h : (completeBipartiteGraph α β).Free G
⊢ G.bipartiteDoubleCover ∈
    {G | G ≤ completeBipartiteGraph (Fin n) (Fin n) ∧ (completeBipartiteGraph (Fin s) (Fin t)).Free G}

Tactic:
simp_rw [mem_filter, mem_univ, true_and]
    refine ⟨bipartiteDoubleCover_le, ?_⟩
    contrapose! h
    refine completeBipartiteGraph_isContained_bipartiteDoubleCover.mp <|
      h.trans' ⟨Iso.toCopy ?_⟩
    exact completeBipartiteGraphCongr
      (Fintype.equivFinOfCardEq hs) (Fintype.equivFinOfCardEq ht)

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

Goal state before:
pp: case refine_3
V : Type u_1
G : SimpleGraph V
inst✝ : G.LocallyFinite
p₁ p₂ : Set V
h₁ : G.IsBipartiteWith p₁ p₂
h₂ : ∀ (s : Set V), s.ncard ≤ (⋃ x ∈ s, G.neighborSet x).ncard
f : V → V
hf₁ : Injective f
hf₂ : ∀ (x : V), f x ∈ G.neighborFinset x
this✝¹ : ∀ x ∈ p₁, f x ∉ p₁
this✝ : ∀ x ∈ p₂, f x ∉ p₂
this : ∀ (x : V), f x ∈ p₁ ∨ f x ∈ p₂
f' : ↑p₁ → ↑p₂ := fun x ↦ ⟨f ↑x, ⋯⟩
g' : ↑p₂ → ↑p₁ := fun x ↦ ⟨f ↑x, ⋯⟩
⊢ ∀ (a : ↑p₁), G.Adj ↑a ↑(f' a)

Tactic:
exact fun v ↦ mem_neighborFinset _ _ _ |>.mp (hf₂ v)

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

Goal state before:
pp: case neg
α : 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 : α
ha : a ∈ insert w₁ s
haj : ¬G.Adj x a
hb : b ∈ insert w₂ t
hbj : ¬G.Adj x b
hc : c ∈ insert v s
hcj : ¬G.Adj x c
hd : d ∈ insert v t
hdj : ¬G.Adj x d
hab : a ≠ b
had : a ≠ d
hbc : b ≠ c
hat : a ∉ t
hbs : b ∉ s
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
hf : c = a → d ≠ b
h : ¬a = c
⊢ ∃ a b c,
    a ∈ {z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z} ∧
      b ∈ {z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z} ∧
        c ∈ {z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z} ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c

Tactic:
exact ⟨a, b, c, by grind⟩

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

Goal state before:
pp: case mp
V : Type u
G : SimpleGraph V
n : ℕ
⊢ G.Partitionable n → G.Colorable n

Tactic:
rintro ⟨P, hf, hc⟩
    have : Fintype P.parts := hf.fintype
    rw [Set.Finite.card_toFinset hf] at hc
    apply P.colorable.mono hc

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

Goal state before:
pp: V : Type u_1
G G' : SimpleGraph V
halt : G.IsAlternating G'
H : G.Subgraph
v w w' : V
hww' : w ≠ w'
hvw : H.spanningCoe.Adj v w
⊢ H.spanningCoe.Adj v w' → (G'.Adj v w ↔ ¬G'.Adj v w')

Tactic:
hvv'

Goal state after:
V : Type u_1
G G' : SimpleGraph V
halt : G.IsAlternating G'
H : G.Subgraph
v w w' : V
hww' : w ≠ w'
hvw : H.spanningCoe.Adj v w
hvv' : H.spanningCoe.Adj v w'
⊢ G'.Adj v w ↔ ¬G'.Adj v w'
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: case neg
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
hadj : ¬G.Adj u x
v w w' : V
hww' : w ≠ w'
hvw : (G ⊔ edge u x).Adj v w
⊢ (G ⊔ edge u x).Adj v w' → (G'.Adj v w ↔ ¬G'.Adj v w')

Tactic:
hvv'

Goal state after:
case neg
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
hadj : ¬G.Adj u x
v w w' : V
hww' : w ≠ w'
hvw : (G ⊔ edge u x).Adj v w
hvv' : (G ⊔ edge u x).Adj v w'
⊢ G'.Adj v w ↔ ¬G'.Adj v w'
Module: Mathlib.Combinatorics.SimpleGraph.Trails

Goal state before:
pp: case inr.convert_2
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
p : G.Walk u v
ht : p.IsEulerian
hn : u ≠ v
⊢ {x | ¬u = v ∧ (¬x = u → x = v)}.card = {u, v}.card

Tactic:
· congr
      ext x
      simp [hn, imp_iff_not_or]

Goal state after:
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) + ε
hε' : 0 < ε'
t' : ℕ := ⌊↑t / (↑r * ε)⌋₊ + 1
ht_lt_rt'ε : ↑t < ↑r * ↑t' * ε
ht'_pos : 0 < t'
N' : ℕ
N : ℕ := max (max 1 N') ⌈(↑(t'.choose t) ^ r * ↑t + ↑r * ↑t') * (↑t' - ↑t) / (↑r * ↑t' * ε - ↑t)⌉₊
n : ℕ
hn : N ≤ n
G : SimpleGraph (Fin n)
x✝ : DecidableRel G.Adj
hδ : ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n
this : Nonempty (Fin n)
hrε_lt_1 : ↑r * ε < 1
ht_lt_t' : t < t'
ih : completeEquipartiteGraph r t' ⊑ G
K : G.CompleteEquipartiteSubgraph r t'
y : (a : Finset (Fin n)) → a ∈ K.parts → Finset (Fin n)
hy✝ : y ∈ K.parts.pi fun x ↦ powersetCard t x
hy : ∀ (a : Finset (Fin n)) (h : a ∈ K.parts), y a h ∈ powersetCard t a
ht_le_card_filter : t ≤ #{w | ErdosStone.filter.pi K w = ⟨y, hy✝⟩}
s : Finset ↥(ErdosStone.filter K t)
hs_subset : s ⊆ {w | ErdosStone.filter.pi K w = ⟨y, hy✝⟩}
hcards : #s = t
K' : G.CompleteEquipartiteSubgraph r t :=
  { parts := Finset.map { toFun := fun p ↦ y ↑p ⋯, inj' := ⋯ } univ, card_parts := ⋯, card_mem_parts := ⋯,
    isCompleteBetween := ⋯ }
p' : Finset (Fin n)
v : Fin n
hv : v ∈ ↑p'
w : Fin n
hw : w ∈ ↑(Finset.map (Function.Embedding.subtype fun x ↦ x ∈ ErdosStone.filter K t) s)
w' : ↥(ErdosStone.filter K t)
hw'_eq : ↑w' = w
p : Finset (Fin n)
hp : p ∈ K.parts
hp'_eq : y p hp = p'
hw'_mem : w' ∈ {w | ErdosStone.filter.pi K w = ⟨y, hy✝⟩}
⊢ G.Adj v w

Tactic:
simp_rw [mem_filter, mem_univ, true_and, ErdosStone.filter.pi, Subtype.mk.injEq] at hw'_mem

Goal state after:
case inr
ε : ℝ
hε : 0 < ε
r t : ℕ
hr_pos : 0 < r
ht_pos : 0 < t
ε' : ℝ := 1 / (↑(r - 1) * ↑r) + ε
hε' : 0 < ε'
t' : ℕ := ⌊↑t / (↑r * ε)⌋₊ + 1
ht_lt_rt'ε : ↑t < ↑r * ↑t' * ε
ht'_pos : 0 < t'
N' : ℕ
N : ℕ := max (max 1 N') ⌈(↑(t'.choose t) ^ r * ↑t + ↑r * ↑t') * (↑t' - ↑t) / (↑r * ↑t' * ε - ↑t)⌉₊
n : ℕ
hn : N ≤ n
G : SimpleGraph (Fin n)
x✝ : DecidableRel G.Adj
hδ : ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n
this : Nonempty (Fin n)
hrε_lt_1 : ↑r * ε < 1
ht_lt_t' : t < t'
ih : completeEquipartiteGraph r t' ⊑ G
K : G.CompleteEquipartiteSubgraph r t'
y : (a : Finset (Fin n)) → a ∈ K.parts → Finset (Fin n)
hy✝ : y ∈ K.parts.pi fun x ↦ powersetCard t x
hy : ∀ (a : Finset (Fin n)) (h : a ∈ K.parts), y a h ∈ powersetCard t a
ht_le_card_filter : t ≤ #{w | ErdosStone.filter.pi K w = ⟨y, hy✝⟩}
s : Finset ↥(ErdosStone.filter K t)
hs_subset : s ⊆ {w | ErdosStone.filter.pi K w = ⟨y, hy✝⟩}
hcards : #s = t
K' : G.CompleteEquipartiteSubgraph r t :=
  { parts := Finset.map { toFun := fun p ↦ y ↑p ⋯, inj' := ⋯ } univ, card_parts := ⋯, card_mem_parts := ⋯,
    isCompleteBetween := ⋯ }
p' : Finset (Fin n)
v : Fin n
hv : v ∈ ↑p'
w : Fin n
hw : w ∈ ↑(Finset.map (Function.Embedding.subtype fun x ↦ x ∈ ErdosStone.filter K t) s)
w' : ↥(ErdosStone.filter K t)
hw'_eq : ↑w' = w
p : Finset (Fin n)
hp : p ∈ K.parts
hp'_eq : y p hp = p'
hw'_mem : (fun p hp ↦ ⋯.choose) = y
⊢ G.Adj v w
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: case none
α : Type ?u.4
β : Type ?u.9
inst✝ : Primcodable α
e : β ≃ α
n : ℕ
⊢ encode none = encode (Option.map (⇑e.symm) none)

Tactic:
simp [encode_ofEquiv]

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

Goal state before:
pp: case some
α : Type ?u.4
β : Type ?u.9
inst✝ : Primcodable α
e : β ≃ α
n : ℕ
val✝ : α
⊢ encode (some val✝) = encode (Option.map (⇑e.symm) (some val✝))

Tactic:
simp [encode_ofEquiv]

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

Goal state before:
pp: m n : ℕ
⊢ m.psub' n = m.psub n

Tactic:
rw [psub']
  split_ifs with h
  · exact (psub_eq_sub h).symm
  · exact (psub_eq_none.2 (not_le.1 h)).symm

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

Goal state before:
pp: α : Type u_1
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable σ
inst✝ : Finite α
f : α → σ
l : List α
left✝ : l.Nodup
m : ∀ (x : α), x ∈ l
⊢ Primrec fun a ↦ some (f a)

Tactic:
by
    have := decidableEqOfEncodable α
    refine ((list_getElem?₁ (l.map f)).comp (list_idxOf₁ l)).of_eq fun a => ?_
    rw [List.getElem?_map, List.getElem?_idxOf (m a), Option.map_some]

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

Goal state before:
pp: case neg
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
h : ∀ (M : G.Subgraph), ¬M.IsPerfectMatching
hvEven : Even (Nat.card V)
val✝ : Fintype V
Gmax : SimpleGraph V
hSubgraph : G ≤ Gmax
hMatchingFree : Gmax.IsMatchingFree
hMaximal : ∀ G' > Gmax, ∃ M, M.IsPerfectMatching
hc : ¬Fintype.card ↑Gmax.universalVerts < Fintype.card ↑(⊤.deleteVerts Gmax.universalVerts).coe.oddComponents
K : Gmax.deleteUniversalVerts.coe.ConnectedComponent
hK : ¬Gmax.deleteUniversalVerts.coe.IsClique K.supp
x y : ↑K.supp
hxy : x ≠ y ∧ ¬Gmax.deleteUniversalVerts.coe.Adj ↑x ↑y
⊢ False

Tactic:
obtain ⟨p, hp⟩ := Reachable.exists_path_of_dist (K.connected_toSimpleGraph x y)

Goal state after:
case neg
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
h : ∀ (M : G.Subgraph), ¬M.IsPerfectMatching
hvEven : Even (Nat.card V)
val✝ : Fintype V
Gmax : SimpleGraph V
hSubgraph : G ≤ Gmax
hMatchingFree : Gmax.IsMatchingFree
hMaximal : ∀ G' > Gmax, ∃ M, M.IsPerfectMatching
hc : ¬Fintype.card ↑Gmax.universalVerts < Fintype.card ↑(⊤.deleteVerts Gmax.universalVerts).coe.oddComponents
K : Gmax.deleteUniversalVerts.coe.ConnectedComponent
hK : ¬Gmax.deleteUniversalVerts.coe.IsClique K.supp
x y : ↑K.supp
hxy : x ≠ y ∧ ¬Gmax.deleteUniversalVerts.coe.Adj ↑x ↑y
p : K.toSimpleGraph.Walk x y
hp : p.IsPath ∧ p.length = K.toSimpleGraph.dist x y
⊢ False
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: ⊢ (fun n ↦ ↑n / log ↑n ^ 2) = fun n ↦ ↑n * (log ↑n ^ 2)⁻¹

Tactic:
div_eq_mul_inv

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

Goal state before:
pp: case hmn
f : ℝ → ℝ
hf✝ : GrowsPolynomially f
hf' : ∀ (a : ℝ), ∃ b, a ≤ b ∧ f b = 0
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hx_pos : 0 < x
x₀ : ℝ
hx₀_ge : max x 1 ≤ x₀
hx₀ : f x₀ = 0
x₀_pos : 0 < x₀
k : ℕ
ih : ∀ (z : ℝ), x ≤ z → z ∈ Set.Icc (2 ^ (-↑k - 1) * x₀) (2 ^ (-↑k) * x₀) → f z = 0
z : ℝ
hx :
  z ∈ Set.Icc (1 / 2 * (2 ^ (-↑k - 1) * x₀)) (2 ^ (-↑k - 1) * x₀) →
    f z ∈ Set.Icc (c₁ * f (2 ^ (-↑k - 1) * x₀)) (c₂ * f (2 ^ (-↑k - 1) * x₀))
hxz : x ≤ z
hz : z ∈ Set.Icc (2 ^ (-(↑k + 1) - 1) * x₀) (2 ^ (-(↑k + 1)) * x₀)
hx' : x ≤ 2 ^ (-↑k - 1) * x₀
⊢ -↑k - 1 ≤ -↑k

Tactic:
· lia

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

Goal state before:
pp: p : ℝ
hp : p ≠ 0
⊢ (fun z ↦ z ^ (p - 1) / log z ^ 2) =o[atTop] fun z ↦ z ^ (p - 1) / 1

Tactic:
div_eq_mul_inv

Goal state after:
p : ℝ
hp : p ≠ 0
⊢ (fun z ↦ z ^ (p - 1) * (log z ^ 2)⁻¹) =o[atTop] fun z ↦ z ^ (p - 1) * 1⁻¹
Module: Mathlib.Computability.AkraBazzi.AkraBazzi

Goal state before:
pp: p : ℝ
hp : p ≠ 0
⊢ (fun x ↦ x ^ (p - 1) / log x ^ 2) =o[atTop] fun z ↦ z ^ (p - 1) / 1

Tactic:
div_eq_mul_inv

Goal state after:
p : ℝ
hp : p ≠ 0
⊢ (fun x ↦ x ^ (p - 1) * (log x ^ 2)⁻¹) =o[atTop] fun z ↦ z ^ (p - 1) * 1⁻¹
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
i : α
q : ℝ → ℝ := fun x ↦ x ^ p a b * (1 - ε x)
h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)
⊢ (fun x ↦ deriv (fun z ↦ z ^ p a b) x * (1 - ε x)) =O[atTop] fun x ↦ x ^ (p a b - 1)

Tactic:
calc (fun x => deriv (fun z => z ^ (p a b)) x * (1 - ε x))
        _ =O[atTop] fun x => x ^ ((p a b) - 1) * (1 - ε x) :=
          IsBigO.mul (isBigO_deriv_rpow_const_atTop (p a b)) (isBigO_refl _ _)
        _ =O[atTop] fun x => x ^ ((p a b) - 1) * 1 :=
          IsBigO.mul (isBigO_refl _ _) isEquivalent_one_sub_smoothingFn_one.isBigO
        _ = fun x => x ^ ((p a b) - 1) := by ext; rw [mul_one]

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
i : α
q : ℝ → ℝ := fun x ↦ x ^ p a b * (1 + ε x)
h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)
h_deriv_q : deriv q =O[atTop] fun x ↦ x ^ (p a b - 1)
h_main_norm : (fun n ↦ ‖q ↑(r i n) - q (b i * ↑n)‖) ≤ᶠ[atTop] fun n ↦ ‖b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)‖
h_main : (fun n ↦ q (b i * ↑n) - q ↑(r i n)) ≤ᶠ[atTop] fun n ↦ b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)
n : ℕ
hn : q (b i * ↑n) - q ↑(r i n) ≤ b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)
h₁ : q (b i * ↑n) - b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n) = b i ^ p a b * ↑n ^ p a b * (1 + ε ↑n)
⊢ b i ^ p a b * ↑n ^ p a b * (1 + ε ↑n) ≤ ↑(r i n) ^ p a b * (1 + ε ↑(r i n))

Tactic:
change (b i) ^ (p a b) * n ^ (p a b) * (1 + ε n) ≤ q (r i n)

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
q : ℝ → ℝ := fun x ↦ x ^ p a b * (1 + ε x)
h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)
h_deriv_q : deriv q =O[atTop] fun x ↦ x ^ (p a b - 1)
h_main_norm : (fun n ↦ ‖q ↑(r i n) - q (b i * ↑n)‖) ≤ᶠ[atTop] fun n ↦ ‖b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)‖
h_main : (fun n ↦ q (b i * ↑n) - q ↑(r i n)) ≤ᶠ[atTop] fun n ↦ b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)
n : ℕ
hn : q (b i * ↑n) - q ↑(r i n) ≤ b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)
h₁ : q (b i * ↑n) - b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n) = b i ^ p a b * ↑n ^ p a b * (1 + ε ↑n)
⊢ b i ^ p a b * ↑n ^ p a b * (1 + ε ↑n) ≤ q ↑(r i n)
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:

Tactic:
|f u| * |g u| ≤ (c₂ * |f x|) * (c₄ * |g x|) := by
           gcongr
           · exact (hf u hu).2
           · exact (hg u hu).2
    _ = c₂ * c₄ * (|f x| * |g x|) := by ring

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case succ
k : ℕ
cf cg : Code
hf : ∀ (n x : ℕ), x ∈ evaln (k + 1) cf n → x ∈ cf.eval n
hg : ∀ (n x : ℕ), x ∈ evaln (k + 1) cg n → x ∈ cg.eval n
n : ℕ
left✝ : n ≤ k
m : ℕ
IH :
  ∀ (x : ℕ),
    Nat.rec (evaln (k + 1) cf (unpair n).1)
          (fun n_1 n_ih ↦
            (evaln k (cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind fun i ↦
              evaln (k + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
          m =
        some x →
      x ∈ Nat.rec (cf.eval (unpair n).1) (fun y IH ↦ IH.bind fun i ↦ cg.eval (Nat.pair (unpair n).1 (Nat.pair y i))) m
x : ℕ
⊢ ∀ (x_1 : ℕ),
    evaln k (cf.prec cg) (Nat.pair (unpair n).1 m) = some x_1 →
      evaln (k + 1) cg (Nat.pair (unpair n).1 (Nat.pair m x_1)) = some x →
        ∃
          a ∈
            Nat.rec (cf.eval (unpair n).1) (fun y IH ↦ IH.bind fun i ↦ cg.eval (Nat.pair (unpair n).1 (Nat.pair y i)))
              m,
          x ∈ cg.eval (Nat.pair (unpair n).1 (Nat.pair m a))

Tactic:
refine fun y h₁ h₂ => ⟨y, IH _ ?_, ?_⟩

Goal state after:
case succ.refine_1
k : ℕ
cf cg : Code
hf : ∀ (n x : ℕ), x ∈ evaln (k + 1) cf n → x ∈ cf.eval n
hg : ∀ (n x : ℕ), x ∈ evaln (k + 1) cg n → x ∈ cg.eval n
n : ℕ
left✝ : n ≤ k
m : ℕ
IH :
  ∀ (x : ℕ),
    Nat.rec (evaln (k + 1) cf (unpair n).1)
          (fun n_1 n_ih ↦
            (evaln k (cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind fun i ↦
              evaln (k + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
          m =
        some x →
      x ∈ Nat.rec (cf.eval (unpair n).1) (fun y IH ↦ IH.bind fun i ↦ cg.eval (Nat.pair (unpair n).1 (Nat.pair y i))) m
x y : ℕ
h₁ : evaln k (cf.prec cg) (Nat.pair (unpair n).1 m) = some y
h₂ : evaln (k + 1) cg (Nat.pair (unpair n).1 (Nat.pair m y)) = some x
⊢ Nat.rec (evaln (k + 1) cf (unpair n).1)
      (fun n_1 n_ih ↦
        (evaln k (cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind fun i ↦
          evaln (k + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
      m =
    some y

case succ.refine_2
k : ℕ
cf cg : Code
hf : ∀ (n x : ℕ), x ∈ evaln (k + 1) cf n → x ∈ cf.eval n
hg : ∀ (n x : ℕ), x ∈ evaln (k + 1) cg n → x ∈ cg.eval n
n : ℕ
left✝ : n ≤ k
m : ℕ
IH :
  ∀ (x : ℕ),
    Nat.rec (evaln (k + 1) cf (unpair n).1)
          (fun n_1 n_ih ↦
            (evaln k (cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind fun i ↦
              evaln (k + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
          m =
        some x →
      x ∈ Nat.rec (cf.eval (unpair n).1) (fun y IH ↦ IH.bind fun i ↦ cg.eval (Nat.pair (unpair n).1 (Nat.pair y i))) m
x y : ℕ
h₁ : evaln k (cf.prec cg) (Nat.pair (unpair n).1 m) = some y
h₂ : evaln (k + 1) cg (Nat.pair (unpair n).1 (Nat.pair m y)) = some x
⊢ x ∈ cg.eval (Nat.pair (unpair n).1 (Nat.pair m y))
Module: Mathlib.Computability.Language

Goal state before:
pp: case succ
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m✝ : Language α
a b x : List α
l m : Language α
h : m * l ≤ m
n : ℕ
ih : m * l ^ n ≤ m
⊢ m * l ^ (n + 1) ≤ m

Tactic:
grw [pow_succ, ← mul_assoc m (l ^ n) l, ih, h]

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

Goal state before:
pp: case inr
f : ℝ → ℝ
hf : GrowsPolynomially f
H : ∀ᶠ (x : ℝ) in atTop, f x < 0
⊢ ∀ᶠ (x : ℝ) in atTop, f x ≠ 0

Tactic:
| inr H =>

Goal state after:
Module: Mathlib.Computability.DFA

Goal state before:
pp: α : Type u
σ : Type v
M : DFA α σ
x : List α
s : σ
hx : M.evalFrom s x = s
S : List (List α)
hS : ∀ y ∈ S, y ∈ {x}
⊢ M.evalFrom s S.flatten = s

Tactic:
induction S with
  | nil => rfl
  | cons a S ih =>
    have ha := hS a List.mem_cons_self
    rw [Set.mem_singleton_iff] at ha
    rw [List.flatten_cons, evalFrom_of_append, ha, hx]
    apply ih
    intro z hz
    exact hS z (List.mem_cons_of_mem a hz)

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

Goal state before:
pp: f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
x✝ : ℝ
⊢ f x✝ / g x✝ = f x✝ * (g x✝)⁻¹

Tactic:
div_eq_mul_inv

Goal state after:
f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
x✝ : ℝ
⊢ f x✝ * (g x✝)⁻¹ = f x✝ * (g x✝)⁻¹
Module: Mathlib.Data.Num.Basic

Goal state before:
pp: a b : PosNum
⊢ Decidable (a < b)

Tactic:
dsimp [LT.lt]

Goal state after:
a b : PosNum
⊢ Decidable (a.cmp b = lt)
Module: Mathlib.Data.Num.Basic

Goal state before:
pp: a b : Num
⊢ Decidable (a < b)

Tactic:
dsimp [LT.lt]

Goal state after:
a b : Num
⊢ Decidable (a.cmp b = lt)
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
hpos : ∀ᶠ (x : ℝ) in atTop, 0 < f x
x : ℝ
a✝ : 0 < x
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hf_pos : 0 < f x
hf_pos₂ : ∀ (y : ℝ), b * id x ≤ y → 0 < f y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ c₂ ^ p * f x ^ p = (c₂ * f x) ^ p

Tactic:
rw [mul_rpow (le_of_lt hc₂_mem) (le_of_lt hf_pos)]

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

Goal state before:

Tactic:
1 / 2 * Real.log x = Real.log x + (-1 / 2) * Real.log x := by ring
      _ ≤ Real.log x + Real.log b := by grind
      _ = Real.log (b * x) := by rw [← Real.log_mul (by positivity) (by positivity), mul_comm]
      _ ≤ Real.log u := by gcongr; exact hu.1

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
s : σ
S : Set σ
x : List α
⊢ s ∈ M.evalFrom S x ↔ ∃ t ∈ S, s ∈ M.evalFrom {t} x

Tactic:
by
  rw [evalFrom_eq_biUnion_singleton]
  simp

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

Goal state before:
pp: case lt
a b : PosNum
⊢ ↑a < ↑b → ↑a + ↑a < ↑b + ↑b

Tactic:
intro this

Goal state after:
case lt
a b : PosNum
this : ↑a < ↑b
⊢ ↑a + ↑a < ↑b + ↑b
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case eq
a b : PosNum
⊢ a = b → a.bit0 = b.bit0

Tactic:
intro this

Goal state after:
case eq
a b : PosNum
this : a = b
⊢ a.bit0 = b.bit0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case gt
a b : PosNum
⊢ ↑b < ↑a → ↑b + ↑b < ↑a + ↑a

Tactic:
intro this

Goal state after:
case gt
a b : PosNum
this : ↑b < ↑a
⊢ ↑b + ↑b < ↑a + ↑a
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case lt
a b : PosNum
⊢ ↑a < ↑b → ↑a + ↑a < ↑b + ↑b + 1

Tactic:
intro this

Goal state after:
case lt
a b : PosNum
this : ↑a < ↑b
⊢ ↑a + ↑a < ↑b + ↑b + 1