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

Goal state before:
pp: case neg.refine_5
α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
f : (completeEquipartiteGraph r t).Copy G
ht : ¬t = 0
x✝³ x✝² : Finset V
x✝¹ x✝ : V
w✝³ : Fin r
h₁ : map { toFun := fun j ↦ f (w✝³, j), inj' := ⋯ } univ = x✝³
w✝² : Fin r
h₂ : map { toFun := fun j ↦ f (w✝², j), inj' := ⋯ } univ = x✝²
w✝¹ : Fin t
h₁' : f (w✝³, w✝¹) = x✝¹
w✝ : Fin t
h₂' : f (w✝², w✝) = x✝
heq : w✝³ = w✝²
⊢ x✝³ = x✝²

Tactic:
← h₁,

Goal state after:
case neg.refine_5
α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
f : (completeEquipartiteGraph r t).Copy G
ht : ¬t = 0
x✝³ x✝² : Finset V
x✝¹ x✝ : V
w✝³ : Fin r
h₁ : map { toFun := fun j ↦ f (w✝³, j), inj' := ⋯ } univ = x✝³
w✝² : Fin r
h₂ : map { toFun := fun j ↦ f (w✝², j), inj' := ⋯ } univ = x✝²
w✝¹ : Fin t
h₁' : f (w✝³, w✝¹) = x✝¹
w✝ : Fin t
h₂' : f (w✝², w✝) = x✝
heq : w✝³ = w✝²
⊢ map { toFun := fun j ↦ f (w✝³, j), inj' := ⋯ } univ = x✝²
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: case neg.refine_5
α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
f : (completeEquipartiteGraph r t).Copy G
ht : ¬t = 0
x✝³ : Finset V
h₁ : x✝³ ∈ ↑(map { toFun := fun i ↦ map { toFun := fun j ↦ f (i, j), inj' := ⋯ } univ, inj' := ⋯ } univ)
x✝² : Finset V
h₂ : x✝² ∈ ↑(map { toFun := fun i ↦ map { toFun := fun j ↦ f (i, j), inj' := ⋯ } univ, inj' := ⋯ } univ)
hne : x✝³ ≠ x✝²
x✝¹ : V
h₁' : x✝¹ ∈ ↑x✝³
x✝ : V
h₂' : x✝ ∈ ↑x✝²
⊢ G.Adj x✝¹ x✝

Tactic:
· simp_rw [coe_map, Embedding.coeFn_mk, coe_univ, Set.image_univ, Set.mem_range] at h₁ h₂
      replace ⟨_, h₁⟩ := h₁
      replace ⟨_, h₂⟩ := h₂
      rw [← h₁] at h₁'
      rw [← h₂] at h₂'
      simp_rw [coe_map, Embedding.coeFn_mk, coe_univ, Set.image_univ, Set.mem_range] at h₁' h₂'
      replace ⟨_, h₁'⟩ := h₁'
      replace ⟨_, h₂'⟩ := h₂'
      rw [← h₁', ← h₂']
      apply f.toHom.map_adj
      simp_rw [completeEquipartiteGraph_adj]
      contrapose hne with heq
      simp_rw [← h₁, ← h₂, heq]

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

Goal state before:
pp: n r : ℕ
⊢ 2 * r * (n % r * (n % r - 1) / 2) ≤ (n % r) ^ 2 * (r - 1)

Tactic:
← Nat.mul_div_assoc _ (Nat.even_mul_pred_self _).two_dvd,

Goal state after:
n r : ℕ
⊢ 2 * r * (n % r * (n % r - 1)) / 2 ≤ (n % r) ^ 2 * (r - 1)
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'
hδ : ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n
N : ℕ
hN : (↑N + ↑r * ↑t') * (↑t' - ↑t) ≤ ↑n * (↑r * ↑t' * ε - ↑t)
⊢ ↑n * (↑r * ↑t' * ε - ↑t) - ↑r * ↑t' * (↑t' - ↑t) =
    ↑(#K.verts) * ((1 - 1 / ↑r + ε) * ↑n - ↑(#K.verts)) - (↑n - ↑(#K.verts)) * (↑(#K.verts) - (↑t' - ↑t))

Tactic:
by
        conv_rhs => rw [sub_eq_add_neg, ← neg_mul, neg_sub, sub_mul, mul_sub, ← add_sub_assoc,
          mul_sub, ← add_sub_assoc, sub_add_cancel, sub_right_comm, ← mul_assoc, ← mul_rotate,
          mul_assoc, ← mul_sub, mul_add, mul_sub (#K.verts : ℝ) _ _, mul_one,
          sub_add_eq_add_sub, add_sub_assoc, add_sub_sub_cancel, K.card_verts, Nat.cast_mul,
          mul_one_div, mul_div_cancel_left₀ (t' : ℝ) (mod_cast hr_pos.ne'), sub_add_sub_cancel]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
G' : G.Subgraph
M : G'.coe.Subgraph
hM : M.IsMatching
⊢ (Subgraph.coeSubgraph M).IsMatching

Tactic:
by
  intro _ hv
  obtain ⟨w, hw⟩ := hM <| Set.mem_of_mem_image_val <| (Subgraph.verts_coeSubgraph M).symm ▸ hv
  use w
  refine ⟨?_, fun y hy => ?_⟩
  · obtain ⟨v, hv⟩ := (Set.mem_image _ _ _).mp <| (Subgraph.verts_coeSubgraph M).symm ▸ hv
    simp only [coeSubgraph_adj, Subtype.coe_eta, Subtype.coe_prop, exists_const]
    exact ⟨hv.2 ▸ v.2, hw.1⟩
  · obtain ⟨_, hw', hvw⟩ := (coeSubgraph_adj _ _ _).mp hy
    rw [← hw.2 ⟨y, hw'⟩ hvw]

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

Goal state before:
pp: R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝⁴ : NonAssocSemiring R
inst✝³ : DecidableEq α
inst✝² : DecidableRel G.Adj
a : α
inst✝¹ : Fintype (Sym2 α)
inst✝ : Fintype ↑(G.neighborSet a)
⊢ ∑ e, incMatrix R G a e = ↑(G.degree a)

Tactic:
simp [incMatrix_apply', sum_boole, Set.filter_mem_univ_eq_toFinset, card_incidenceSet_eq_degree]

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
R : Type u_3
inst✝ : AddCommMonoidWithOne R
i : V
⊢ ↑(G.degree i) = ∑ j, if G.Adj i j then 1 else 0

Tactic:
by
  unfold degree neighborFinset neighborSet
  rw [sum_boole, Set.toFinset_ofPred]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
P : G.Partition
v✝ w✝ : V
hvw : G.Adj v✝ w✝
⊢ ¬P.partOfVertex v✝ = P.partOfVertex w✝

Tactic:
exact P.partOfVertex_ne_of_adj hvw

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

Goal state before:
pp: case a
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : Nontrivial V
h : G.IsSRGWith n k ℓ μ
ht : G ≠ ⊤
hm : μ ≠ 0
⊢ 2 ≤ G.ediam

Tactic:
by_contra
    have := not_subsingleton V
    simp_all [Order.le_one_iff]

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

Goal state before:
pp: case neg.inl.inr
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'
hl : G.Adj v w
h2 : (v = u ∧ w' = x ∨ v = x ∧ w' = u) ∧ v ≠ w'
⊢ G'.Adj v w ↔ ¬G'.Adj v w'

Tactic:
G'.adj_congr_of_sym2 (by grind : s(v, w') = s(u, x))

Goal state after:
case neg.inl.inr
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'
hl : G.Adj v w
h2 : (v = u ∧ w' = x ∨ v = x ∧ w' = u) ∧ v ≠ w'
⊢ G'.Adj v w ↔ ¬G'.Adj u x
Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular

Goal state before:
pp: V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
ha : v ≠ w ∧ ¬G.Adj v w
hne : v ≠ w
⊢ Fintype.card V - #(G.neighborFinset v ∪ G.neighborFinset w) - (1 + 1) = n - (2 * k - μ) - 2

Tactic:
h.card_neighborFinset_union_of_not_adj hne ha.2,

Goal state after:
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
ha : v ≠ w ∧ ¬G.Adj v w
hne : v ≠ w
⊢ Fintype.card V - (2 * k - μ) - (1 + 1) = n - (2 * k - μ) - 2
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

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

Tactic:
rw [hap, ← add_mul, card_add_card_compl, mul_comm, two_mul, ← add_assoc]

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

Tactic:
calc
    _ ≤ ∑ w ∈ W, G.degree w + 2 * ∑ w ∈ s ∩ t, G.degree w := by
      simp_rw [add_assoc, add_comm k, ← add_assoc, ← Wc, add_assoc, ← two_mul, mul_add,
               ← hw.card_inter, card_eq_sum_ones, ← mul_assoc, mul_sum, mul_one, mul_comm 2]
      gcongr with i <;> exact minDegree_le_degree ..
    _ ≤ (#X * (#W - 3) + #Xᶜ * (#W - 1)) + 2 * (#X * #(s ∩ t) + #Xᶜ * (#(s ∩ t) - 1)) := by gcongr
    _ = #X * (#W - 3 + 2 * k) + #Xᶜ * ((#W - 1) + 2 * (k - 1)) := by grind
    _ ≤ _ := by
        by_cases hk : k = 0 -- so `s ∩ t = ∅` and hence `Xᶜ = ∅`
        · have Xu : X = univ := by
            rw [← hw.card_inter, card_eq_zero] at hk
            exact eq_univ_of_forall fun _ ↦ by simp [X, hk]
          subst k
          rw [add_zero] at Wc
          simp [Xu, Wc, mul_comm]
        have w3 : 3 ≤ #W := two_lt_card.2 ⟨_, mem_insert_self .., _, by simp [W], _, by simp [W],
          hw.isPathGraph3Compl.ne_fst, hw.isPathGraph3Compl.ne_snd, hw.isPathGraph3Compl.fst_ne_snd⟩
        have hap : #W - 1 + 2 * (k - 1) = #W - 3 + 2 * k := by lia
        rw [hap, ← add_mul, card_add_card_compl, mul_comm, two_mul, ← add_assoc]
        gcongr
        lia

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
hodd : Odd (Nat.card V)
⊢ G.IsTutteViolator ∅

Tactic:
by
  rw [IsTutteViolator, Set.ncard_empty]
  exact ((odd_ncard_oddComponents _).mpr <| by simpa using hodd).pos

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
M : G.Subgraph
hM : M.IsPerfectMatching
u : Set V
f : ↑(⊤.deleteVerts u).coe.oddComponents → V
hf : ∀ (c : ↑(⊤.deleteVerts u).coe.oddComponents), f c ∈ u
g : ↑(⊤.deleteVerts u).coe.oddComponents → ↑(⊤.deleteVerts u).verts
hgf : ∀ (c : ↑(⊤.deleteVerts u).coe.oddComponents), M.Adj (↑(g c)) (f c)
hg : ∀ (c : ↑(⊤.deleteVerts u).coe.oddComponents), g c ∈ (↑c).supp
c d : ↑(⊤.deleteVerts u).coe.oddComponents
hcd : f c = f d
⊢ c = d

Tactic:
replace hcd : g c = g d := Subtype.val_injective <| hM.1.eq_of_adj_right (hgf c) (hcd ▸ hgf d)
    exact Subtype.val_injective <| ConnectedComponent.eq_of_common_vertex (hg c) (hcd ▸ hg d)

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
M : G.Subgraph
hM : M.IsPerfectMatching
u : Set V
⊢ ¬G.IsTutteViolator u

Tactic:
choose f hf g hgf hg using ConnectedComponent.odd_matches_node_outside hM (u := u)
  have hfinj : f.Injective := fun c d hcd ↦ by
    replace hcd : g c = g d := Subtype.val_injective <| hM.1.eq_of_adj_right (hgf c) (hcd ▸ hgf d)
    exact Subtype.val_injective <| ConnectedComponent.eq_of_common_vertex (hg c) (hcd ▸ hg d)
  simpa [IsTutteViolator] using!
    Nat.card_le_card_of_injective (fun c ↦ ⟨f c, hf c⟩) (fun c d ↦ by simp [hfinj.eq_iff])

Goal state after:
Module: Mathlib.Combinatorics.Young.YoungDiagram

Goal state before:
pp: w : List ℕ
hw : w.SortedGE
i2 j2 i1 j1 : ℕ
hi : i1 ≤ i2
hj : j1 ≤ j2
hcell : (i2, j2) ∈ YoungDiagram.cellsOfRowLens w
⊢ (i1, j1) ∈ YoungDiagram.cellsOfRowLens w

Tactic:
YoungDiagram.mem_cellsOfRowLens

Goal state after:
w : List ℕ
hw : w.SortedGE
i2 j2 i1 j1 : ℕ
hi : i1 ≤ i2
hj : j1 ≤ j2
hcell : ∃ (h : (i2, j2).1 < w.length), (i2, j2).2 < w[(i2, j2).1]
⊢ ∃ (h : (i1, j1).1 < w.length), (i1, j1).2 < w[(i1, j1).1]
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case inl
p : ℕ →. Bool
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
n : ℕ
h₁ : true ∈ p n
h₂ : ∀ k < n, (p k).Dom
h₃ : m < n
⊢ (p m).Dom

Tactic:
exact h₂ _ h₃

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
x✝¹ : Fin 0 → α → σ
x✝ : ∀ (i : Fin 0), Computable (x✝¹ i)
⊢ Computable fun a ↦ List.ofFn fun i ↦ x✝¹ i a

Tactic:
by
    simp only [List.ofFn_zero]
    exact const []

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
hvOdd : ¬Odd (Nat.card V)
⊢ ∃ u, G.IsTutteViolator u

Tactic:
· exact exists_isTutteViolator h (Nat.not_odd_iff_even.mp hvOdd)

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

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

Tactic:
case two => calc
        (fun z => z ^ (p - 1) / (log z ^ 2)) =o[atTop] fun z => z ^ (p - 1) / 1 := by
          simp_rw [div_eq_mul_inv]
          refine IsBigO.mul_isLittleO (isBigO_refl _ _)
            (IsLittleO.inv_rev ?_ (by simp))
          rw [isLittleO_const_left]
          refine Or.inr <| Tendsto.comp tendsto_norm_atTop_atTop ?_
          exact Tendsto.comp (g := fun z => z ^ 2)
            (tendsto_pow_atTop (by norm_num)) tendsto_log_atTop
        _ = fun z => z ^ (p - 1) := by ext; simp
        _ =Θ[atTop] fun z => p * z ^ (p - 1) := IsTheta.const_mul_right hp <| isTheta_refl _ _

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 ↑(r i n) - q (b i * ↑n)) ≤ᶠ[atTop] fun n ↦ b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)
n : ℕ
hn : q ↑(r i n) - q (b 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)
⊢ q ↑(r i n) ≤ b i ^ p a b * ↑n ^ p a b * (1 - ε ↑n)

Tactic:
← h₁,

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 ↑(r i n) - q (b i * ↑n)) ≤ᶠ[atTop] fun n ↦ b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)
n : ℕ
hn : q ↑(r i n) - q (b 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)
⊢ q ↑(r i n) ≤ q (b i * ↑n) + b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : c₁ ∈ Set.Ioo 0 1
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, 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
hu' : u ∈ Set.Icc (r i n) n
⊢ ↑(r i n) ≤ ↑u

Tactic:
exact_mod_cast hu'.1

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) ≤ q ↑(r i n)

Tactic:
← h₁,

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)
⊢ q (b i * ↑n) - b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n) ≤ q ↑(r i n)
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : c₁ ∈ Set.Ioo 0 1
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, 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
hu' : u ∈ Set.Icc (r i n) n
⊢ ↑(r i n) ≤ ↑u

Tactic:
exact_mod_cast hu'.1

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

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

Tactic:
exact_mod_cast hu'.1

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

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

Tactic:
exact_mod_cast hu'.1

Goal state after:
Module: Mathlib.Computability.Language

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m✝ : Language α
a b x : List α
l m : Language α
h : m * l ≤ m
⊢ m * ⨆ i, l ^ i ≤ m

Tactic:
mul_iSup

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m✝ : Language α
a b x : List α
l m : Language α
h : m * l ≤ m
⊢ ⨆ i, m * l ^ i ≤ m