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

Goal state before:
pp: case e_a
n r : ℕ
⊢ (((∑ x ∈ range r, ∑ w ∈ range n, if (n + x) % r ≠ w % r then 1 else 0) +
        ∑ x ∈ range n, ∑ w ∈ range r, if x % r ≠ (n + w) % r then 1 else 0) +
      ∑ x ∈ range r, ∑ w ∈ range r, if (n + x) % r ≠ (n + w) % r then 1 else 0) =
    2 * (n * (r - 1)) + 2 * r.choose 2

Tactic:
sum_comm

Goal state after:
case e_a
n r : ℕ
⊢ (((∑ y ∈ range n, ∑ x ∈ range r, if (n + x) % r ≠ y % r then 1 else 0) +
        ∑ x ∈ range n, ∑ w ∈ range r, if x % r ≠ (n + w) % r then 1 else 0) +
      ∑ x ∈ range r, ∑ w ∈ range r, if (n + x) % r ≠ (n + w) % r then 1 else 0) =
    2 * (n * (r - 1)) + 2 * r.choose 2
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: case pos
α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
h : G.diam = 0
⊢ ∃ u v, G.dist u v = G.diam

pp: case neg
α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
h : ¬G.diam = 0
⊢ ∃ u v, G.dist u v = G.diam

Tactic:
· simp [h]

Goal state after:
case neg
α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
h : ¬G.diam = 0
⊢ ∃ u v, G.dist u v = G.diam
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: α : Type u_1
⊢ ⊥.diam = 0

Tactic:
rw [diam, ENat.toNat_eq_zero]
  cases subsingleton_or_nontrivial α
  · exact Or.inl ediam_eq_zero_of_subsingleton
  · exact Or.inr ediam_bot

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs

Goal state before:
pp: V : Type u
G : SimpleGraph V
K L M : Set V
β : Sort u_1
f : ⦃v : V⦄ → v ∉ K → β
h : ∀ ⦃v w : V⦄ (hv : v ∉ K) (hw : w ∉ K), G.Adj v w → f hv = f hw
v w : ↑Kᶜ
p : (induce Kᶜ G).Walk v w
⊢ p.IsPath → f ⋯ = f ⋯

Tactic:
induction p with

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs

Goal state before:
pp: V : Type u
G : SimpleGraph V
K L M : Set V
β : Sort u_1
f : ⦃v : V⦄ → v ∉ K → β
h : ∀ ⦃v w : V⦄ (hv : v ∉ K) (hw : w ∉ K), G.Adj v w → f hv = f hw
v w : ↑Kᶜ
p : (induce Kᶜ G).Walk v w
⊢ p.IsPath → f ⋯ = f ⋯

Tactic:
induction p with
    | nil => rintro _; rfl
    | cons a q ih => rename_i u v w; rintro h'; exact (h u.prop v.prop a).trans (ih h'.of_cons)

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs

Goal state before:
pp: V : Type u
G : SimpleGraph V
K : (Finset V)ᵒᵖ
C : G.componentComplFunctor.obj K
⊢ (ComponentCompl.supp C).Infinite ↔ C ∈ G.componentComplFunctor.eventualRange K

Tactic:
simp only [C.infinite_iff_in_all_ranges, CategoryTheory.Functor.eventualRange, Set.mem_iInter,
    Set.mem_range, componentComplFunctor_map]
  exact
    ⟨fun h Lop KL => h Lop.unop (le_of_op_hom KL), fun h L KL =>
      h (Opposite.op L) (opHomOfLE KL)⟩

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

Goal state before:
pp: V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : G.Subgraph) → G'.verts.Finite → G'.coe →g F
val✝ : Fintype W
this✝¹ : ∀ (G' : G.Finsubgraphᵒᵖ), Nonempty ((G.finsubgraphHomFunctor F).obj G')
G' : G.Finsubgraphᵒᵖ
this✝ : Fintype ↑(↑(Opposite.unop G')).verts
this : Fintype (↑(↑(Opposite.unop G')).verts → W)
⊢ Fintype ((G.finsubgraphHomFunctor F).obj G')

Tactic:
exact Fintype.ofInjective (fun f => f.toFun) RelHom.coe_fn_injective

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

Goal state before:
pp: m n s t : ℕ
V : Type u_1
W : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : Fintype V
inst✝² : Fintype W
inst✝¹ : Fintype α
inst✝ : Fintype β
hm : Fintype.card V = m
hn : Fintype.card W = n
hs : Fintype.card α = s
ht : Fintype.card β = t
⊢ zarankiewicz m n s t =
    {G | G ≤ completeBipartiteGraph V W ∧ (completeBipartiteGraph α β).Free G}.sup fun x ↦ #x.edgeFinset

Tactic:
by
  let e₁ := completeBipartiteGraphCongr
    (Fintype.equivFinOfCardEq hm) (Fintype.equivFinOfCardEq hn)
  let K := completeBipartiteGraph (Fin s) (Fin t)
  let e₂ := completeBipartiteGraphCongr
    (Fintype.equivFinOfCardEq hs) (Fintype.equivFinOfCardEq ht)
  rw [zarankiewicz, le_antisymm_iff]
  and_intros
  on_goal 1 =>
    let e₁ := e₁.symm
    let K := completeBipartiteGraph α β
    let e₂ := e₂.symm
  all_goals
    simp_rw [Finset.sup_le_iff, mem_filter, mem_univ, true_and]
    intro G ⟨h_le, h_free⟩
    simp_rw [Iso.card_edgeFinset_eq (.map e₁.toEquiv G)]
    have h' : G.map e₁.toEquiv.toEmbedding ∈ univ.filter fun G ↦
        G ≤ completeBipartiteGraph _ _ ∧ K.Free G := by
      rw [mem_filter_univ, map_le_iff_le_comap]
      refine ⟨fun _ _ hadj ↦ ?_, ?_⟩
      · replace h_le := h_le hadj
        rw [← Embedding.map_adj_iff e₁.toEmbedding, ← comap_adj] at h_le
        exact h_le
      · rw [Function.Embedding.coeFn_mk, ← free_congr e₂ (.map e₁.toEquiv G)]
        exact h_free
    have h_le_sup := @le_sup _ _ _ _ _ (#·.edgeFinset) (G.map e₁.toEquiv.toEmbedding) h'
    simp_rw [← card_coe, mem_edgeFinset] at h_le_sup ⊢
    exact h_le_sup

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
G : SimpleGraph α
G' : SimpleGraph β
h : G ⊑ G'
hacyc : ¬G.IsAcyclic
a : α
w : G.Walk a a
hw : w.IsCycle
hwl : G.egirth = ↑w.length
⊢ G'.egirth ≤ G.egirth

Tactic:
rw [hwl, ← w.length_map h.some.toHom]

Goal state after:
case neg
α : Type u_1
β : Type u_2
G : SimpleGraph α
G' : SimpleGraph β
h : G ⊑ G'
hacyc : ¬G.IsAcyclic
a : α
w : G.Walk a a
hw : w.IsCycle
hwl : G.egirth = ↑w.length
⊢ G'.egirth ≤ ↑(Walk.map (Nonempty.some h).toHom w).length
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: case pos
α : Type u_1
s : Set α
hs : s.Infinite
h : 1 = 0
⊢ ∑ᶠ (i : α) (_ : i ∈ s), 1 = 0

pp: case neg
α : Type u_1
s : Set α
hs : s.Infinite
h : ¬1 = 0
⊢ ∑ᶠ (i : α) (_ : i ∈ s), 1 = 0

Tactic:
· simp [h]

Goal state after:
case neg
α : Type u_1
s : Set α
hs : s.Infinite
h : ¬1 = 0
⊢ ∑ᶠ (i : α) (_ : i ∈ s), 1 = 0
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits

Goal state before:
pp: n : ℕ
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
ε : ℝ
r t t' : ℕ
K : G.CompleteEquipartiteSubgraph r t'
hr_pos : 0 < r
ht'_pos : 0 < t'
ht_lt_t' : t < t'
hδ : ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n
hN : (↑(t'.choose t) ^ r * ↑t + ↑r * ↑t') * (↑t' - ↑t) ≤ ↑n * (↑r * ↑t' * ε - ↑t)
p : Finset (Fin n)
⊢ p ∈ K.parts → t ≤ #p

Tactic:
hp

Goal state after:
n : ℕ
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
ε : ℝ
r t t' : ℕ
K : G.CompleteEquipartiteSubgraph r t'
hr_pos : 0 < r
ht'_pos : 0 < t'
ht_lt_t' : t < t'
hδ : ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n
hN : (↑(t'.choose t) ^ r * ↑t + ↑r * ↑t') * (↑t' - ↑t) ≤ ↑n * (↑r * ↑t' * ε - ↑t)
p : Finset (Fin n)
hp : p ∈ K.parts
⊢ t ≤ #p
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 : α
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
⊢ ∃ a b, G.IsFiveWheelLike r (k + 1) v w₁ w₂ (insert x (s.erase a)) (insert x (t.erase b))

Tactic:
let W := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))

Goal state after:
α : 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)))
⊢ ∃ a b, G.IsFiveWheelLike r (k + 1) v w₁ w₂ (insert x (s.erase a)) (insert x (t.erase b))
Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
inst✝ : Fintype α
hG : G.IsHamiltonian
a b : α
⊢ G.Reachable a b

Tactic:
obtain rfl | hab := eq_or_ne a b

Goal state after:
case inl
α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
inst✝ : Fintype α
hG : G.IsHamiltonian
a : α
⊢ G.Reachable a a

case inr
α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
inst✝ : Fintype α
hG : G.IsHamiltonian
a b : α
hab : a ≠ b
⊢ G.Reachable a b
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Goal state before:
pp: α : 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}
⊢ G.minDegree ≤ (2 * r + k) * ‖α‖ / (2 * r + k + 3)

Tactic:
let W := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))

Goal state after:
α : 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)))
⊢ G.minDegree ≤ (2 * r + k) * ‖α‖ / (2 * r + k + 3)
Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular

Goal state before:
pp: case convert_3.e_a.e_a
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
s : {v} ⊆ G.neighborFinset w \ G.neighborFinset v
⊢ #(G.neighborFinset w) = k

Tactic:
simp [h.regular w]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : G.Walk u v
ht : p.IsTrail
x : V
⊢ Even (List.countP (fun e ↦ decide (x ∈ e)) p.edges) ↔ u ≠ v → x ≠ u ∧ x ≠ v

Tactic:
induction p with

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

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → Option β
g : α → β → σ
hf : Primrec f
hg : Primrec₂ g
x : α
⊢ ((f x).bind fun b ↦ some (g x b)) = Option.map (g x) (f x)

Tactic:
cases f x

Goal state after:
case none
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → Option β
g : α → β → σ
hf : Primrec f
hg : Primrec₂ g
x : α
⊢ (none.bind fun b ↦ some (g x b)) = Option.map (g x) none

case some
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → Option β
g : α → β → σ
hf : Primrec f
hg : Primrec₂ g
x : α
val✝ : β
⊢ ((some val✝).bind fun b ↦ some (g x b)) = Option.map (g x) (some val✝)
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case succ.refine_2
α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
n : ℕ
b : σ
H : b ∈ Nat.rec (Part.some (g a)) (fun n n_ih ↦ h a n) (n + 1)
⊢ b ∈ Nat.rec (Part.some (g a)) (fun y IH ↦ IH.bind fun i ↦ h a (n + 1 - 1)) (n + 1)

Tactic:
· have : ∀ m, (Nat.rec (motive := fun _ => Part σ)
            (Part.some (g a)) (fun y IH => IH.bind fun _ => h a n) m).Dom := by
          intro m
          induction m <;> simp [*, H.fst]
        exact ⟨⟨this n, H.fst⟩, H.snd⟩

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case refine_2
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun a n ↦ Nat.rec (Part.some (Sum.inr a)) (fun x IH ↦ IH.bind fun s ↦ Sum.casesOn s (fun x ↦ Part.some s) f) n
h : b ∈ f.fix a
a₁ : α
⊢ b ∈ f.fix a₁ → ∀ (k : ℕ), Sum.inr a₁ ∈ F a k → ∃ n, Sum.inl b ∈ F a n ∧ ∀ m < n, k ≤ m → ∃ a₂, Sum.inr a₂ ∈ F a m

Tactic:
h₁

Goal state after:
case refine_2
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun a n ↦ Nat.rec (Part.some (Sum.inr a)) (fun x IH ↦ IH.bind fun s ↦ Sum.casesOn s (fun x ↦ Part.some s) f) n
h : b ∈ f.fix a
a₁ : α
h₁ : b ∈ f.fix a₁
⊢ ∀ (k : ℕ), Sum.inr a₁ ∈ F a k → ∃ n, Sum.inl b ∈ F a n ∧ ∀ m < n, k ≤ m → ∃ a₂, Sum.inr a₂ ∈ F a m
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
h₁ : -1 + (-↑k - 1) = -↑k - 2
h₂ : -(↑k + 1) - 1 = -↑k - 2
⊢ 2 ^ (-1 + (-↑k - 1)) * x₀ ≤ z

Tactic:
h₁

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
h₁ : -1 + (-↑k - 1) = -↑k - 2
h₂ : -(↑k + 1) - 1 = -↑k - 2
⊢ 2 ^ (-↑k - 2) * x₀ ≤ z
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: case inr.inl
f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
this : GrowsPolynomially fun x ↦ |f x| * |g x|
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
hg' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ g x
⊢ GrowsPolynomially fun x ↦ f x * g x

Tactic:
have hmain : (fun x => f x * g x) =ᶠ[atTop] fun x => -|f x| * |g x| := by
          filter_upwards [hf', hg'] with x hx₁ hx₂
          rw [abs_of_nonpos hx₁, abs_of_nonneg hx₂, neg_neg]
        simp only [iff_eventuallyEq hmain, neg_mul]
        exact this.neg

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

Goal state before:
pp: case refine_3
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
b' : ℝ := b (min_bi b) / 2
hb_pos : 0 < b'
⊢ ∀ᶠ (n₀ : ℕ) in atTop,
    ∃ C₀,
      ∀ᶠ (n : ℕ) in atTop,
        ∀ C ≥ C₀,
          (∀ m ∈ Ico n₀ n, T m ≤ C * ((1 - ε ↑m) * asympBound g a b m)) → T n ≤ C * ((1 - ε ↑n) * asympBound g a b n)

Tactic:
obtain ⟨c₁, hc₁, h_sumTransform_aux⟩ := R.eventually_atTop_sumTransform_ge

Goal state after:
case refine_3
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
b' : ℝ := b (min_bi b) / 2
hb_pos : 0 < b'
c₁ : ℝ
hc₁ : c₁ > 0
h_sumTransform_aux : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * g ↑n ≤ sumTransform (p a b) g (r i n) n
⊢ ∀ᶠ (n₀ : ℕ) in atTop,
    ∃ C₀,
      ∀ᶠ (n : ℕ) in atTop,
        ∀ C ≥ C₀,
          (∀ m ∈ Ico n₀ n, T m ≤ C * ((1 - ε ↑m) * asympBound g a b m)) → T n ≤ C * ((1 - ε ↑n) * asympBound g a b n)
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: c₁ c₂ : Code
n₁ n₂ : ℕ
h₁ : c₁ = c₂
h₃ : Code.const n₁ = Code.const n₂
h₄ : Code.id = Code.id
⊢ n₁ = n₂

Tactic:
exact const_inj h₃

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case zero
k k₂ : ℕ
hl : k + 1 ≤ k₂ + 1
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₂
n x : ℕ
h :
  (fun n ↦ do
        guard (n ≤ k)
        pure 0)
      n =
    some x
⊢ (fun n ↦ do
        guard (n ≤ k₂)
        pure 0)
      n =
    some x

Tactic:
refine this hl' (fun h => ?_) h

Goal state after:
case zero
k k₂ : ℕ
hl : k + 1 ≤ k₂ + 1
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₂
n x : ℕ
h✝ :
  (fun n ↦ do
        guard (n ≤ k)
        pure 0)
      n =
    some x
h : x ∈ pure 0
⊢ x ∈ pure 0
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case succ
k k₂ : ℕ
hl : k + 1 ≤ k₂ + 1
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₂
n x : ℕ
h :
  (fun n ↦ do
        guard (n ≤ k)
        pure n.succ)
      n =
    some x
⊢ (fun n ↦ do
        guard (n ≤ k₂)
        pure n.succ)
      n =
    some x

Tactic:
refine this hl' (fun h => ?_) h

Goal state after:
case succ
k k₂ : ℕ
hl : k + 1 ≤ k₂ + 1
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₂
n x : ℕ
h✝ :
  (fun n ↦ do
        guard (n ≤ k)
        pure n.succ)
      n =
    some x
h : x ∈ pure n.succ
⊢ x ∈ pure n.succ
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case left
k k₂ : ℕ
hl : k + 1 ≤ k₂ + 1
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₂
n x : ℕ
h :
  (fun n ↦ do
        guard (n ≤ k)
        pure (unpair n).1)
      n =
    some x
⊢ (fun n ↦ do
        guard (n ≤ k₂)
        pure (unpair n).1)
      n =
    some x

Tactic:
refine this hl' (fun h => ?_) h

Goal state after:
case left
k k₂ : ℕ
hl : k + 1 ≤ k₂ + 1
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₂
n x : ℕ
h✝ :
  (fun n ↦ do
        guard (n ≤ k)
        pure (unpair n).1)
      n =
    some x
h : x ∈ pure (unpair n).1
⊢ x ∈ pure (unpair n).1
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case right
k k₂ : ℕ
hl : k + 1 ≤ k₂ + 1
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₂
n x : ℕ
h :
  (fun n ↦ do
        guard (n ≤ k)
        pure (unpair n).2)
      n =
    some x
⊢ (fun n ↦ do
        guard (n ≤ k₂)
        pure (unpair n).2)
      n =
    some x

Tactic:
refine this hl' (fun h => ?_) h

Goal state after:
case right
k k₂ : ℕ
hl : k + 1 ≤ k₂ + 1
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₂
n x : ℕ
h✝ :
  (fun n ↦ do
        guard (n ≤ k)
        pure (unpair n).2)
      n =
    some x
h : x ∈ pure (unpair n).2
⊢ x ∈ pure (unpair n).2
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case pair
k k₂ : ℕ
hl : k + 1 ≤ k₂ + 1
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₂
a✝¹ a✝ : Code
a_ih✝¹ : ∀ (n x : ℕ), evaln (k + 1) a✝¹ n = some x → evaln (k₂ + 1) a✝¹ n = some x
a_ih✝ : ∀ (n x : ℕ), evaln (k + 1) a✝ n = some x → evaln (k₂ + 1) a✝ n = some x
n x : ℕ
h :
  (fun n ↦ do
        guard (n ≤ k)
        Nat.pair <$> evaln (k + 1) a✝¹ n <*> evaln (k + 1) a✝ n)
      n =
    some x
⊢ (fun n ↦ do
        guard (n ≤ k₂)
        Nat.pair <$> evaln (k₂ + 1) a✝¹ n <*> evaln (k₂ + 1) a✝ n)
      n =
    some x

Tactic:
refine this hl' (fun h => ?_) h

Goal state after:
case pair
k k₂ : ℕ
hl : k + 1 ≤ k₂ + 1
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₂
a✝¹ a✝ : Code
a_ih✝¹ : ∀ (n x : ℕ), evaln (k + 1) a✝¹ n = some x → evaln (k₂ + 1) a✝¹ n = some x
a_ih✝ : ∀ (n x : ℕ), evaln (k + 1) a✝ n = some x → evaln (k₂ + 1) a✝ n = some x
n x : ℕ
h✝ :
  (fun n ↦ do
        guard (n ≤ k)
        Nat.pair <$> evaln (k + 1) a✝¹ n <*> evaln (k + 1) a✝ n)
      n =
    some x
h : x ∈ Nat.pair <$> evaln (k + 1) a✝¹ n <*> evaln (k + 1) a✝ n
⊢ x ∈ Nat.pair <$> evaln (k₂ + 1) a✝¹ n <*> evaln (k₂ + 1) a✝ n
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case comp
k k₂ : ℕ
hl : k + 1 ≤ k₂ + 1
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₂
a✝¹ a✝ : Code
a_ih✝¹ : ∀ (n x : ℕ), evaln (k + 1) a✝¹ n = some x → evaln (k₂ + 1) a✝¹ n = some x
a_ih✝ : ∀ (n x : ℕ), evaln (k + 1) a✝ n = some x → evaln (k₂ + 1) a✝ n = some x
n x : ℕ
h :
  (fun n ↦ do
        guard (n ≤ k)
        let x ← evaln (k + 1) a✝ n
        evaln (k + 1) a✝¹ x)
      n =
    some x
⊢ (fun n ↦ do
        guard (n ≤ k₂)
        let x ← evaln (k₂ + 1) a✝ n
        evaln (k₂ + 1) a✝¹ x)
      n =
    some x

Tactic:
refine this hl' (fun h => ?_) h

Goal state after:
case comp
k k₂ : ℕ
hl : k + 1 ≤ k₂ + 1
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₂
a✝¹ a✝ : Code
a_ih✝¹ : ∀ (n x : ℕ), evaln (k + 1) a✝¹ n = some x → evaln (k₂ + 1) a✝¹ n = some x
a_ih✝ : ∀ (n x : ℕ), evaln (k + 1) a✝ n = some x → evaln (k₂ + 1) a✝ n = some x
n x : ℕ
h✝ :
  (fun n ↦ do
        guard (n ≤ k)
        let x ← evaln (k + 1) a✝ n
        evaln (k + 1) a✝¹ x)
      n =
    some x
h :
  x ∈ do
    let x ← evaln (k + 1) a✝ n
    evaln (k + 1) a✝¹ x
⊢ x ∈ do
    let x ← evaln (k₂ + 1) a✝ n
    evaln (k₂ + 1) a✝¹ x