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

Goal state before:
pp: V : Type u_1
w : V
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
hw : w ∈ t
v : V
⊢ v ∈ G.neighborSet w ↔ v ∈ {v | v ∈ s ∧ G.Adj v w}

Tactic:
rw [mem_neighborSet, adj_comm, Set.mem_ofPred_eq, iff_and_self]

Goal state after:
V : Type u_1
w : V
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
hw : w ∈ t
v : V
⊢ G.Adj v w → v ∈ s
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
H : G.Subgraph
hc : H.Connected
h : ∀ v ∈ H.verts, ∀ (w : V), G.Adj v w → H.Adj v w
⊢ ∃ c, H.verts = c.supp

Tactic:
by
  rw [SimpleGraph.ConnectedComponent.exists]
  obtain ⟨v, hv⟩ := hc.nonempty
  use v
  ext w
  simp only [ConnectedComponent.mem_supp_iff, ConnectedComponent.eq]
  exact ⟨fun hw ↦ by simpa using (hc ⟨w, hw⟩ ⟨v, hv⟩).map H.hom,
    fun a ↦ a.symm.mem_subgraphVerts h hv⟩

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

Goal state before:
pp: case left
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
inst✝ : DecidableEq V
⊢ p.bypass.toSubgraph.verts ⊆ p.toSubgraph.verts

pp: case right
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
inst✝ : DecidableEq V
⊢ ∀ ⦃v_1 w : V⦄, p.bypass.toSubgraph.Adj v_1 w → p.toSubgraph.Adj v_1 w

Tactic:
· simpa using! p.support_bypass_subset_support

Goal state after:
case right
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
inst✝ : DecidableEq V
⊢ ∀ ⦃v_1 w : V⦄, p.bypass.toSubgraph.Adj v_1 w → p.toSubgraph.Adj v_1 w
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v w : V ⊕ V
val✝¹ val✝ : V
he : G.bipartiteDoubleCover.Adj (Sum.inl val✝¹) (Sum.inl val✝)
⊢ ∃ a,
    ∃ (ha :
      a ∈
        {x |
          match x with
          | (x, y) => G.Adj x y}),
      (match a, ha with
        | (v, w), x => s(Sum.inl v, Sum.inr w)) =
        s(Sum.inl val✝¹, Sum.inl val✝)

Tactic:
simp at he

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v w : V ⊕ V
val✝¹ val✝ : V
he : G.bipartiteDoubleCover.Adj (Sum.inr val✝¹) (Sum.inr val✝)
⊢ ∃ a,
    ∃ (ha :
      a ∈
        {x |
          match x with
          | (x, y) => G.Adj x y}),
      (match a, ha with
        | (v, w), x => s(Sum.inl v, Sum.inr w)) =
        s(Sum.inr val✝¹, Sum.inr val✝)

Tactic:
simp at he

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
hconn : G.Connected
⊢ G.dist u v = 0 ↔ u = v

Tactic:
by simp [hconn u v]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
V : Type u_4
V₁ : Type u_5
V₂ : Type u_6
W : Type u_7
W₁ : Type u_8
W₂ : Type u_9
G : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
x y : (α × β) × γ
⊢ (G □ (H □ I)).Adj ((Equiv.prodAssoc α β γ) x) ((Equiv.prodAssoc α β γ) y) ↔ (G □ H □ I).Adj x y

Tactic:
simp only [boxProd_adj, Equiv.prodAssoc_apply, or_and_right, or_assoc, Prod.ext_iff,
      and_assoc, @and_comm (x.fst.fst = _)]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x : α × β
inst✝² : Fintype ↑(G.neighborSet x.1)
inst✝¹ : Fintype ↑(H.neighborSet x.2)
inst✝ : Fintype ↑((G □ H).neighborSet x)
⊢ ((G □ H).neighborFinset x).card = (G.neighborFinset x.1).card + (H.neighborFinset x.2).card

Tactic:
neighborFinset_boxProd,

Goal state after:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x : α × β
inst✝² : Fintype ↑(G.neighborSet x.1)
inst✝¹ : Fintype ↑(H.neighborSet x.2)
inst✝ : Fintype ↑((G □ H).neighborSet x)
⊢ ((G.neighborFinset x.1 ×ˢ {x.2}).disjUnion ({x.1} ×ˢ H.neighborFinset x.2) ⋯).card =
    (G.neighborFinset x.1).card + (H.neighborFinset x.2).card
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : H.Free G
⊢ #G.edgeFinset ≤ extremalNumber (Fintype.card V) H

Tactic:
extremalNumber_of_fintypeCard_eq rfl

Goal state after:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : H.Free G
⊢ #G.edgeFinset ≤ {G | H.Free G}.sup fun x ↦ #x.edgeFinset
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: V : Type u_1
W : Type u_2
inst✝³ : Fintype V
R : Type u_3
inst✝² : Semiring R
inst✝¹ : LinearOrder R
inst✝ : FloorSemiring R
H : SimpleGraph W
m : R
h : 0 ≤ m
⊢ ↑(extremalNumber (Fintype.card V) H) ≤ m ↔
    ∀ ⦃G : SimpleGraph V⦄ [inst : DecidableRel G.Adj], H.Free G → ↑(#G.edgeFinset) ≤ m

Tactic:
by
  simp_rw [← Nat.le_floor_iff h]
  exact extremalNumber_le_iff H ⌊m⌋₊

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✝³ : DecidableEq V
inst✝² : DecidableEq α
inst✝¹ : AddMonoid α
inst✝ : One α
⊢ 1 + adjMatrix α G + (adjMatrix α G).compl = of 1

Tactic:
aesop (add simp [add_assoc])

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: case inr
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
s t : V
hn : ¬G.Adj s t
h : G.degree s ≠ G.degree t
cf : G.CliqueFree (r + 1)
this :
  ∀ {G : SimpleGraph V} [inst : DecidableRel G.Adj] {s t : V},
    ¬G.Adj s t →
      G.degree s ≠ G.degree t →
        G.CliqueFree (r + 1) →
          G.degree t < G.degree s → ∃ G' inst_1, G'.CliqueFree (r + 1) ∧ #G.edgeFinset < #G'.edgeFinset
hd : ¬G.degree t < G.degree s
⊢ ∃ G' inst, G'.CliqueFree (r + 1) ∧ #G.edgeFinset < #G'.edgeFinset

Tactic:
replace hd : G.degree s < G.degree t := lt_of_le_of_ne (le_of_not_gt hd) h

Goal state after:
case inr
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
s t : V
hn : ¬G.Adj s t
h : G.degree s ≠ G.degree t
cf : G.CliqueFree (r + 1)
this :
  ∀ {G : SimpleGraph V} [inst : DecidableRel G.Adj] {s t : V},
    ¬G.Adj s t →
      G.degree s ≠ G.degree t →
        G.CliqueFree (r + 1) →
          G.degree t < G.degree s → ∃ G' inst_1, G'.CliqueFree (r + 1) ∧ #G.edgeFinset < #G'.edgeFinset
hd : G.degree s < G.degree t
⊢ ∃ G' inst, G'.CliqueFree (r + 1) ∧ #G.edgeFinset < #G'.edgeFinset
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions

Goal state before:
pp: case neg.inl
n✝ n : ℕ
h : 2 ≤ n + 2
u v : Fin (n + 2)
hu : ¬↑u = n + 2 - 1
h✝ : ¬↑v = n + 2 - 1
hu' : ↑u + ↑1 < n + 2
hv' : ↑v + ↑1 < n + 2
huv : u - v = 1
⊢ ¬(Even (↑v + 1) ↔ Even ↑v)

Tactic:
Nat.even_add

Goal state after:
case neg.inl
n✝ n : ℕ
h : 2 ≤ n + 2
u v : Fin (n + 2)
hu : ¬↑u = n + 2 - 1
h✝ : ¬↑v = n + 2 - 1
hu' : ↑u + ↑1 < n + 2
hv' : ↑v + ↑1 < n + 2
huv : u - v = 1
⊢ ¬((Even ↑v ↔ Even 1) ↔ Even ↑v)
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions

Goal state before:
pp: case neg.inr
n✝ n : ℕ
h : 2 ≤ n + 2
u v : Fin (n + 2)
hu : ¬↑u = n + 2 - 1
h✝ : ¬↑v = n + 2 - 1
hu' : ↑u + ↑1 < n + 2
hv' : ↑v + ↑1 < n + 2
huv : v - u = 1
⊢ ¬(Even ↑u ↔ Even (↑u + 1))

Tactic:
Nat.even_add

Goal state after:
case neg.inr
n✝ n : ℕ
h : 2 ≤ n + 2
u v : Fin (n + 2)
hu : ¬↑u = n + 2 - 1
h✝ : ¬↑v = n + 2 - 1
hu' : ↑u + ↑1 < n + 2
hv' : ↑v + ↑1 < n + 2
huv : v - u = 1
⊢ ¬(Even ↑u ↔ (Even ↑u ↔ Even 1))
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: case neg
V : Type u_1
G : SimpleGraph V
h : G.IsTree
inst✝² : Fintype V
inst✝¹ : Nontrivial V
inst✝ : DecidableRel G.Adj
q : ¬2 ≤ G.minDegree
⊢ G.minDegree = 1

Tactic:
have := h.preconnected.minDegree_pos_of_nontrivial

Goal state after:
case neg
V : Type u_1
G : SimpleGraph V
h : G.IsTree
inst✝² : Fintype V
inst✝¹ : Nontrivial V
inst✝ : DecidableRel G.Adj
q : ¬2 ≤ G.minDegree
this : 0 < G.minDegree
⊢ G.minDegree = 1
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
hconn : G.Connected
v : V
inst✝ : Fintype ↑(G.neighborSet v)
hdeg : G.degree v = 1
u : V
adj_vu : G.Adj v u
hu : ∀ (y : V), (fun w ↦ G.Adj v w) y → y = u
w x : ↑{v}ᶜ
pwu : G.Walk (↑w) u
hpwu : pwu.IsPath
pux : G.Walk u ↑x
hpux : pux.IsPath
⊢ (induce {v}ᶜ G).Reachable w x

Tactic:
rw [Reachable, ← exists_true_iff_nonempty]

Goal state after:
V : Type u_1
G : SimpleGraph V
hconn : G.Connected
v : V
inst✝ : Fintype ↑(G.neighborSet v)
hdeg : G.degree v = 1
u : V
adj_vu : G.Adj v u
hu : ∀ (y : V), (fun w ↦ G.Adj v w) y → y = u
w x : ↑{v}ᶜ
pwu : G.Walk (↑w) u
hpwu : pwu.IsPath
pux : G.Walk u ↑x
hpux : pux.IsPath
⊢ ∃ x, True
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝¹ : Finite V
inst✝ : Nontrivial V
hconn : G.Connected
T : SimpleGraph V
left✝ : T ≤ G
T_isTree : T.IsTree
hT : T.Connected
isAcyclic✝ : T.IsAcyclic
this : Fintype V
v : V
hv : T.degree v = 1
⊢ ∃ v, (induce {v}ᶜ G).Connected

Tactic:
exact ⟨v, (hT.induce_compl_singleton_of_degree_eq_one hv).mono (by tauto)⟩

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
h : G.IsAcyclic
n : ℕ
hn : 3 ≤ n
hle : completeGraph (Fin n) ⊑ G
⊢ False

Tactic:
exact isAcyclic_iff_free_cycleGraph.mp h n hn <| hle.trans' <| .of_le le_top

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

Goal state before:
pp: case inl
α : Type u_1
G : SimpleGraph α
h : ¬G.Preconnected
h✝ : IsEmpty α
⊢ G.ediam = ⊤

Tactic:
exfalso
    exact h <| IsEmpty.forall_iff.mpr trivial

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v : V
inst✝ : G.LocallyFinite
u : V
p : G.Walk u u
hp : p.IsCycle
hcyc : G.IsCycles
hv : v ∈ p.toSubgraph.verts
w : V
this : (p.toSubgraph.neighborSet v).ncard = 2
⊢ ↑(G.neighborSet v).ncard = ↑(p.toSubgraph.neighborSet v).ncard

Tactic:
hcyc
      (Set.Nonempty.mono (p.toSubgraph.neighborSet_subset v) <|
        Set.nonempty_of_ncard_ne_zero <| by simp [this]),

Goal state after:
V : Type u_1
G : SimpleGraph V
v : V
inst✝ : G.LocallyFinite
u : V
p : G.Walk u u
hp : p.IsCycle
hcyc : G.IsCycles
hv : v ∈ p.toSubgraph.verts
w : V
this : (p.toSubgraph.neighborSet v).ncard = 2
⊢ ↑2 = ↑(p.toSubgraph.neighborSet v).ncard
Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular

Goal state before:
pp: case convert_4
n k ℓ μ : ℕ
V : Type u
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.IsSRGWith n k ℓ μ
this : DecidableEq V := Classical.decEq V
v w : V
hw : ¬G.Adj v w ∧ w ≠ v
⊢ #(G.neighborSet v ∩ G.neighborSet w).toFinset = μ

Tactic:
← h.of_not_adj hw.2.symm hw.1,

Goal state after:
case convert_4
n k ℓ μ : ℕ
V : Type u
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.IsSRGWith n k ℓ μ
this : DecidableEq V := Classical.decEq V
v w : V
hw : ¬G.Adj v w ∧ w ≠ v
⊢ #(G.neighborSet v ∩ G.neighborSet w).toFinset = Fintype.card ↑(G.commonNeighbors v w)
Module: Mathlib.Combinatorics.SimpleGraph.Trails

Goal state before:
pp: case pos
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v x u✝ v✝ w✝ : V
huv : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : Even (List.countP (fun e ↦ decide (x ∈ e)) p.edges) ↔ v✝ ≠ w✝ → x ≠ v✝ ∧ x ≠ w✝
ht : p.IsTrail ∧ s(u✝, v✝) ∉ p.edges
h : decide (x = u✝ ∨ x = v✝) = true
⊢ Even (List.countP (fun e ↦ decide (x ∈ e)) p.edges + 1) ↔ ¬u✝ = w✝ → ¬x = u✝ ∧ ¬x = w✝

pp: case neg
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v x u✝ v✝ w✝ : V
huv : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : Even (List.countP (fun e ↦ decide (x ∈ e)) p.edges) ↔ v✝ ≠ w✝ → x ≠ v✝ ∧ x ≠ w✝
ht : p.IsTrail ∧ s(u✝, v✝) ∉ p.edges
h : ¬decide (x = u✝ ∨ x = v✝) = true
⊢ Even (List.countP (fun e ↦ decide (x ∈ e)) p.edges + 0) ↔ ¬u✝ = w✝ → ¬x = u✝ ∧ ¬x = w✝

Tactic:
· rw [decide_eq_true_eq] at h
      obtain (rfl | rfl) := h
      · rw [Nat.even_add_one, ih]
        simp only [huv.ne, imp_false, Ne, not_false_iff, true_and, not_forall,
          Classical.not_not, exists_prop, not_true, false_and,
          and_iff_right_iff_imp]
        rintro rfl rfl
        exact G.loopless.irrefl _ huv
      · have := huv.ne; grind

Goal state after:
case neg
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v x u✝ v✝ w✝ : V
huv : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : Even (List.countP (fun e ↦ decide (x ∈ e)) p.edges) ↔ v✝ ≠ w✝ → x ≠ v✝ ∧ x ≠ w✝
ht : p.IsTrail ∧ s(u✝, v✝) ∉ p.edges
h : ¬decide (x = u✝ ∨ x = v✝) = true
⊢ Even (List.countP (fun e ↦ decide (x ∈ e)) p.edges + 0) ↔ ¬u✝ = w✝ → ¬x = u✝ ∧ ¬x = w✝
Module: Mathlib.Data.Nat.PSub

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

Tactic:
rw [psub']

Goal state after:
m n : ℕ
⊢ (if n ≤ m then some (m - n) else none) = m.psub n
Module: Mathlib.Data.Nat.PSub

Goal state before:
pp: case neg
m n : ℕ
h : ¬n ≤ m
⊢ none = m.psub n

Tactic:
· exact (psub_eq_none.2 (not_le.1 h)).symm

Goal state after:
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: m n : ℕ
⊢ ack m (n + 1) ≤ ack (m + 1) n

Tactic:
by
  rcases n with - | n
  · simp
  · rw [ack_succ_succ]
    apply ack_mono_right m (le_trans _ <| add_add_one_le_ack _ n)
    lia

Goal state after:
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: n : ℕ
⊢ n ^ 2 ≤ 2 ^ (n + 1) - 3

Tactic:
by
  induction n with
  | zero => simp
  | succ k => cases k <;> lia

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

Goal state before:
pp: f : ℝ → ℝ
b : ℝ
hb : b ∈ Set.Ioo 0 1
hf : GrowsPolynomially f
⊢ ∃ c > 0, ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, c * f x ≤ f u

Tactic:
by
  obtain ⟨c₁, hc₁, c₂, _, h⟩ := hf b hb
  refine ⟨c₁, hc₁, ?_⟩
  filter_upwards [h]
  exact fun _ H u hu => (H u hu).1

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

Goal state before:
pp: 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 : f (2 ^ (-↑k - 1) * x₀) = 0
z : ℝ
hxz : x ≤ z
hz : z ∈ Set.Icc (2 ^ (-(↑k + 1) - 1) * x₀) (2 ^ (-(↑k + 1)) * x₀)
hx' : x ≤ 2 ^ (-↑k - 1) * x₀
hx : z ∈ Set.Icc (1 / 2 * (2 ^ (-↑k - 1) * x₀)) (2 ^ (-↑k - 1) * x₀) → f z = 0
⊢ 2⁻¹ * (2 ^ (-↑k - 1) * x₀) ≤ z

Tactic:
← zpow_neg_one,

Goal state after:
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 : f (2 ^ (-↑k - 1) * x₀) = 0
z : ℝ
hxz : x ≤ z
hz : z ∈ Set.Icc (2 ^ (-(↑k + 1) - 1) * x₀) (2 ^ (-(↑k + 1)) * x₀)
hx' : x ≤ 2 ^ (-↑k - 1) * x₀
hx : z ∈ Set.Icc (1 / 2 * (2 ^ (-↑k - 1) * x₀)) (2 ^ (-↑k - 1) * x₀) → f z = 0
⊢ 2 ^ (-1) * (2 ^ (-↑k - 1) * x₀) ≤ z
Module: Mathlib.Computability.AkraBazzi.AkraBazzi

Goal state before:
pp: case inl
p : ℝ
hp : p = 0
h₁ : (fun x ↦ ‖deriv (fun z ↦ z ^ p * (1 - ε z)) x‖) =ᶠ[atTop] fun z ↦ z⁻¹ / log z ^ 2
⊢ GrowsPolynomially fun z ↦ z⁻¹ / log z ^ 2

Tactic:
refine GrowsPolynomially.div (GrowsPolynomially.inv growsPolynomially_id)
      (GrowsPolynomially.pow 2 growsPolynomially_log ?_)

Goal state after:
case inl
p : ℝ
hp : p = 0
h₁ : (fun x ↦ ‖deriv (fun z ↦ z ^ p * (1 - ε z)) x‖) =ᶠ[atTop] fun z ↦ z⁻¹ / log z ^ 2
⊢ ∀ᶠ (x : ℝ) in atTop, 0 ≤ log x
Module: Mathlib.Computability.AkraBazzi.AkraBazzi

Goal state before:
pp: case inl
p : ℝ
hp : p = 0
h₁ : (fun x ↦ ‖deriv (fun z ↦ z ^ p * (1 + ε z)) x‖) =ᶠ[atTop] fun z ↦ z⁻¹ / log z ^ 2
⊢ GrowsPolynomially fun z ↦ z⁻¹ / log z ^ 2

Tactic:
refine GrowsPolynomially.div (GrowsPolynomially.inv growsPolynomially_id)
      (GrowsPolynomially.pow 2 growsPolynomially_log ?_)

Goal state after:
case inl
p : ℝ
hp : p = 0
h₁ : (fun x ↦ ‖deriv (fun z ↦ z ^ p * (1 + ε z)) x‖) =ᶠ[atTop] fun z ↦ z⁻¹ / log z ^ 2
⊢ ∀ᶠ (x : ℝ) in atTop, 0 ≤ log x
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: case hab
α : 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, g u ≤ c₂ * g ↑n
hc₁_pos : 0 < c₁
n : ℕ
hn₁ : ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
hn₂ : ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, g u ≤ c₂ * g ↑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 : 0 ≤ p a b + 1
u : ℕ
hu : u ∈ Ico (r i n) n
⊢ g ↑u ≤ c₂ * g ↑n

Tactic:
rw [Finset.mem_Ico] at hu

Goal state after:
case hab
α : 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, g u ≤ c₂ * g ↑n
hc₁_pos : 0 < c₁
n : ℕ
hn₁ : ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
hn₂ : ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, g u ≤ c₂ * g ↑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 : 0 ≤ p a b + 1
u : ℕ
hu : r i n ≤ u ∧ u < n
⊢ g ↑u ≤ c₂ * g ↑n
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: case a
α : 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, g u ≤ c₂ * g ↑n
hc₁_pos : 0 < c₁
n : ℕ
hn₁ : ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
hn₂ : ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, g u ≤ c₂ * g ↑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 : 0 ≤ p a b + 1
u : ℕ
hu : u ∈ Ico (r i n) n
⊢ r i n ≤ u

Tactic:
rw [Finset.mem_Ico] at hu

Goal state after:
case a
α : 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, g u ≤ c₂ * g ↑n
hc₁_pos : 0 < c₁
n : ℕ
hn₁ : ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
hn₂ : ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, g u ≤ c₂ * g ↑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 : 0 ≤ p a b + 1
u : ℕ
hu : r i n ≤ u ∧ u < n
⊢ r i n ≤ u
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: case hab
α : 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, g u ≤ c₂ * g ↑n
hc₁_pos : 0 < c₁
n : ℕ
hn₁ : ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
hn₂ : ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, g u ≤ c₂ * g ↑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
u : ℕ
hu : u ∈ Ico (r i n) n
⊢ g ↑u ≤ c₂ * g ↑n

Tactic:
rw [Finset.mem_Ico] at hu

Goal state after:
case hab
α : 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, g u ≤ c₂ * g ↑n
hc₁_pos : 0 < c₁
n : ℕ
hn₁ : ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
hn₂ : ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, g u ≤ c₂ * g ↑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
u : ℕ
hu : r i n ≤ u ∧ u < n
⊢ g ↑u ≤ c₂ * g ↑n
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: case hdb
α : 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, g u ≤ c₂ * g ↑n
hc₁_pos : 0 < c₁
n : ℕ
hn₁ : ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
hn₂ : ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, g u ≤ c₂ * g ↑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
u : ℕ
hu : u ∈ Ico (r i n) n
⊢ ↑n ^ (p a b + 1) ≤ ↑u ^ (p a b + 1)

Tactic:
rw [Finset.mem_Ico] at hu

Goal state after:
case hdb
α : 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, g u ≤ c₂ * g ↑n
hc₁_pos : 0 < c₁
n : ℕ
hn₁ : ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
hn₂ : ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, g u ≤ c₂ * g ↑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
u : ℕ
hu : r i n ≤ u ∧ u < n
⊢ ↑n ^ (p a b + 1) ≤ ↑u ^ (p a b + 1)
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: case hab
α : 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 : 0 ≤ p a b + 1
u : ℕ
hu : u ∈ Ico (r i n) n
⊢ c₂ * g ↑n ≤ g ↑u

Tactic:
rw [Finset.mem_Ico] at hu

Goal state after:
case hab
α : 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 : 0 ≤ p a b + 1
u : ℕ
hu : r i n ≤ u ∧ u < n
⊢ c₂ * g ↑n ≤ g ↑u