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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
w : V
hcyc : G.IsCycles
_x : (v : V) ×' (p : G.Walk v w) ×' p.IsPath
a✝² :
  ∀ (y : (v : V) ×' (p : G.Walk v w) ×' p.IsPath),
    InvImage (fun x1 x2 ↦ x1 < x2)
        (fun x ↦ PSigma.casesOn x fun v p ↦ PSigma.casesOn p fun p hp ↦ Nat.card V + 1 - p.length) y _x →
      (G \ y.2.1.toSubgraph.spanningCoe).Reachable w y.1
v : V
p✝ : (p : G.Walk v w) ×' p.IsPath
a✝¹ :
  ∀ (y : (v : V) ×' (p : G.Walk v w) ×' p.IsPath),
    InvImage (fun x1 x2 ↦ x1 < x2)
        (fun x ↦ PSigma.casesOn x fun v p ↦ PSigma.casesOn p fun p hp ↦ Nat.card V + 1 - p.length) y ⟨v, p✝⟩ →
      (G \ y.2.1.toSubgraph.spanningCoe).Reachable w y.1
p : G.Walk v w
hp : p.IsPath
a✝ :
  ∀ (y : (v : V) ×' (p : G.Walk v w) ×' p.IsPath),
    InvImage (fun x1 x2 ↦ x1 < x2)
        (fun x ↦ PSigma.casesOn x fun v p ↦ PSigma.casesOn p fun p hp ↦ Nat.card V + 1 - p.length) y ⟨v, ⟨p, hp⟩⟩ →
      (G \ y.2.1.toSubgraph.spanningCoe).Reachable w y.1
hvw : ¬v = w
hpn : ¬p.Nil
w' : V
h✝ : (fun w' ↦ p.snd ≠ w' ∧ G.Adj v w') w' ∧ ∀ (y : V), p.snd ≠ y ∧ G.Adj v y → y = w'
left✝ : p.snd ≠ w' ∧ G.Adj v w'
hwu : ∀ (y : V), p.snd ≠ y ∧ G.Adj v y → y = w'
hw'1 : p.snd ≠ w'
hw'2 : G.Adj v w'
hnpvw' : ¬p.toSubgraph.Adj v w'
hww' : ¬w = w'
hle : G \ (Walk.cons ⋯ p).toSubgraph.spanningCoe ≤ G \ p.toSubgraph.spanningCoe
hp'p : (Walk.cons ⋯ p).IsPath
this✝ : (G \ p.toSubgraph.spanningCoe).Adj w' v
this : Fintype V
⊢ Fintype.card V - p.length < Fintype.card V + 1 - p.length

Tactic:
have := Walk.IsPath.length_lt hp

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
w : V
hcyc : G.IsCycles
_x : (v : V) ×' (p : G.Walk v w) ×' p.IsPath
a✝² :
  ∀ (y : (v : V) ×' (p : G.Walk v w) ×' p.IsPath),
    InvImage (fun x1 x2 ↦ x1 < x2)
        (fun x ↦ PSigma.casesOn x fun v p ↦ PSigma.casesOn p fun p hp ↦ Nat.card V + 1 - p.length) y _x →
      (G \ y.2.1.toSubgraph.spanningCoe).Reachable w y.1
v : V
p✝ : (p : G.Walk v w) ×' p.IsPath
a✝¹ :
  ∀ (y : (v : V) ×' (p : G.Walk v w) ×' p.IsPath),
    InvImage (fun x1 x2 ↦ x1 < x2)
        (fun x ↦ PSigma.casesOn x fun v p ↦ PSigma.casesOn p fun p hp ↦ Nat.card V + 1 - p.length) y ⟨v, p✝⟩ →
      (G \ y.2.1.toSubgraph.spanningCoe).Reachable w y.1
p : G.Walk v w
hp : p.IsPath
a✝ :
  ∀ (y : (v : V) ×' (p : G.Walk v w) ×' p.IsPath),
    InvImage (fun x1 x2 ↦ x1 < x2)
        (fun x ↦ PSigma.casesOn x fun v p ↦ PSigma.casesOn p fun p hp ↦ Nat.card V + 1 - p.length) y ⟨v, ⟨p, hp⟩⟩ →
      (G \ y.2.1.toSubgraph.spanningCoe).Reachable w y.1
hvw : ¬v = w
hpn : ¬p.Nil
w' : V
h✝ : (fun w' ↦ p.snd ≠ w' ∧ G.Adj v w') w' ∧ ∀ (y : V), p.snd ≠ y ∧ G.Adj v y → y = w'
left✝ : p.snd ≠ w' ∧ G.Adj v w'
hwu : ∀ (y : V), p.snd ≠ y ∧ G.Adj v y → y = w'
hw'1 : p.snd ≠ w'
hw'2 : G.Adj v w'
hnpvw' : ¬p.toSubgraph.Adj v w'
hww' : ¬w = w'
hle : G \ (Walk.cons ⋯ p).toSubgraph.spanningCoe ≤ G \ p.toSubgraph.spanningCoe
hp'p : (Walk.cons ⋯ p).IsPath
this✝¹ : (G \ p.toSubgraph.spanningCoe).Adj w' v
this✝ : Fintype V
this : p.length < Fintype.card V
⊢ Fintype.card V - p.length < Fintype.card V + 1 - p.length
Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular

Goal state before:
pp: case convert_3
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 : V
⊢ ∀ a ∈ G.neighborFinset v, #(bipartiteAbove G.Adj (Gᶜ.neighborFinset v) a) = k - ℓ - 1

Tactic:
intro w hw

Goal state after:
case convert_3
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 : w ∈ G.neighborFinset v
⊢ #(bipartiteAbove G.Adj (Gᶜ.neighborFinset v) w) = k - ℓ - 1
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 : V
⊢ ∀ b ∈ Gᶜ.neighborFinset v, #(bipartiteBelow G.Adj (G.neighborFinset v) b) = μ

Tactic:
intro w hw

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 : w ∈ Gᶜ.neighborFinset v
⊢ #(bipartiteBelow G.Adj (G.neighborFinset v) w) = μ
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: case neg
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
hM : M.IsPerfectMatching
hG' : G'.IsAlternating M.spanningCoe
hG'cyc : G'.IsCycles
v w : V
hw : (fun w ↦ M.Adj v w) w ∧ ∀ (y : V), (fun w ↦ M.Adj v w) y → y = w
h : ¬G'.Adj v w
⊢ ∃! w, ⊤.Adj v w

Tactic:
use w
    simp only [Subgraph.top_adj, SimpleGraph.sup_adj, sdiff_adj, Subgraph.spanningCoe_adj, hw.1, h,
      not_false_eq_true, and_self, not_true_eq_false, or_false, true_and]
    rintro y (hl | hr)
    · exact hw.2 _ hl.1
    · have ⟨w', hw'⟩ := hG'cyc.other_adj_of_adj hr.1
      simp_all [show M.Adj v y ↔ ¬M.Adj v w' by simpa using hG' hw'.1 hr.1 hw'.2]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
h : ¬G.IsTutteViolator G.universalVerts
h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp
hrep :
  ConnectedComponent.Represents (Quot.out '' G.deleteUniversalVerts.coe.oddComponents)
    G.deleteUniversalVerts.coe.oddComponents
t : Set V
ht : t ⊆ G.universalVerts
M1 : G.Subgraph
hM1 : M1.verts = Subtype.val '' Quot.out '' G.deleteUniversalVerts.coe.oddComponents ∪ t ∧ M1.IsMatching
complMatch : G.deleteUniversalVerts.coe.ConnectedComponent → G.Subgraph
hcomplMatch_compl :
  ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), (complMatch K).verts = Subtype.val '' K.supp \ M1.verts
hcomplMatch_match : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), (complMatch K).IsMatching
M2 : G.Subgraph := ⨆ K, complMatch K
i j : G.deleteUniversalVerts.coe.ConnectedComponent
hij : i ≠ j
⊢ Disjoint (Subtype.val '' i.supp \ M1.verts) (complMatch j).verts

Tactic:
hcomplMatch_compl j

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
h : ¬G.IsTutteViolator G.universalVerts
h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp
hrep :
  ConnectedComponent.Represents (Quot.out '' G.deleteUniversalVerts.coe.oddComponents)
    G.deleteUniversalVerts.coe.oddComponents
t : Set V
ht : t ⊆ G.universalVerts
M1 : G.Subgraph
hM1 : M1.verts = Subtype.val '' Quot.out '' G.deleteUniversalVerts.coe.oddComponents ∪ t ∧ M1.IsMatching
complMatch : G.deleteUniversalVerts.coe.ConnectedComponent → G.Subgraph
hcomplMatch_compl :
  ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), (complMatch K).verts = Subtype.val '' K.supp \ M1.verts
hcomplMatch_match : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), (complMatch K).IsMatching
M2 : G.Subgraph := ⨆ K, complMatch K
i j : G.deleteUniversalVerts.coe.ConnectedComponent
hij : i ≠ j
⊢ Disjoint (Subtype.val '' i.supp \ M1.verts) (Subtype.val '' j.supp \ M1.verts)
Module: Mathlib.Combinatorics.SimpleGraph.Tutte

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
h : ¬G.IsTutteViolator G.universalVerts
h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp
hrep :
  ConnectedComponent.Represents (Quot.out '' G.deleteUniversalVerts.coe.oddComponents)
    G.deleteUniversalVerts.coe.oddComponents
t : Set V
ht : t ⊆ G.universalVerts
M1 : G.Subgraph
hM1 : M1.verts = Subtype.val '' Quot.out '' G.deleteUniversalVerts.coe.oddComponents ∪ t ∧ M1.IsMatching
complMatch : G.deleteUniversalVerts.coe.ConnectedComponent → G.Subgraph
hcomplMatch_compl :
  ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), (complMatch K).verts = Subtype.val '' K.supp \ M1.verts
hcomplMatch_match : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), (complMatch K).IsMatching
M2 : G.Subgraph := ⨆ K, complMatch K
hM2 : M2.IsMatching
disjointM12 : Disjoint M1.support M2.support
⊢ (M1.verts ∪ M2.verts)ᶜ ⊆ G.universalVerts

Tactic:
rw [Set.compl_subset_comm, Set.compl_eq_univ_sdiff]

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
h : ¬G.IsTutteViolator G.universalVerts
h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp
hrep :
  ConnectedComponent.Represents (Quot.out '' G.deleteUniversalVerts.coe.oddComponents)
    G.deleteUniversalVerts.coe.oddComponents
t : Set V
ht : t ⊆ G.universalVerts
M1 : G.Subgraph
hM1 : M1.verts = Subtype.val '' Quot.out '' G.deleteUniversalVerts.coe.oddComponents ∪ t ∧ M1.IsMatching
complMatch : G.deleteUniversalVerts.coe.ConnectedComponent → G.Subgraph
hcomplMatch_compl :
  ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), (complMatch K).verts = Subtype.val '' K.supp \ M1.verts
hcomplMatch_match : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), (complMatch K).IsMatching
M2 : G.Subgraph := ⨆ K, complMatch K
hM2 : M2.IsMatching
disjointM12 : Disjoint M1.support M2.support
⊢ Set.univ \ G.universalVerts ⊆ M1.verts ∪ M2.verts
Module: Mathlib.Combinatorics.SimpleGraph.Tutte

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
x a b c : V
M1 : (G ⊔ edge x b).Subgraph
M2 : (G ⊔ edge a c).Subgraph
hxa : G.Adj x a
hab : G.Adj a b
hnGxb : ¬G.Adj x b
hnGac : ¬G.Adj a c
hnxb : x ≠ b
hnxc : x ≠ c
hnac : a ≠ c
hnbc : b ≠ c
hM1 : M1.IsPerfectMatching
hM2 : M2.IsPerfectMatching
hM1xb : M1.Adj x b
hM2ac : M2.Adj a c
hM1nac : ¬M1.Adj a c
hsupG : G ⊔ edge x b ⊔ (G ⊔ edge a c) = G ⊔ edge a c ⊔ edge x b
cycles : SimpleGraph V := M1.spanningCoe ∆ M2.spanningCoe
hcalt : cycles.IsAlternating M2.spanningCoe
hcycles : (M1.spanningCoe ∆ M2.spanningCoe).IsCycles
hcac : cycles.Adj a c
hM1sub : M1.spanningCoe ≤ G ⊔ edge x b
hM2sub : M2.spanningCoe ≤ G ⊔ edge a c
⊢ (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe ≤ G ⊔ edge a c ⊔ edge x b

Tactic:
refine le_trans (spanningCoe_induce_le cycles (cycles.connectedComponentMk c).supp) ?_

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
x a b c : V
M1 : (G ⊔ edge x b).Subgraph
M2 : (G ⊔ edge a c).Subgraph
hxa : G.Adj x a
hab : G.Adj a b
hnGxb : ¬G.Adj x b
hnGac : ¬G.Adj a c
hnxb : x ≠ b
hnxc : x ≠ c
hnac : a ≠ c
hnbc : b ≠ c
hM1 : M1.IsPerfectMatching
hM2 : M2.IsPerfectMatching
hM1xb : M1.Adj x b
hM2ac : M2.Adj a c
hM1nac : ¬M1.Adj a c
hsupG : G ⊔ edge x b ⊔ (G ⊔ edge a c) = G ⊔ edge a c ⊔ edge x b
cycles : SimpleGraph V := M1.spanningCoe ∆ M2.spanningCoe
hcalt : cycles.IsAlternating M2.spanningCoe
hcycles : (M1.spanningCoe ∆ M2.spanningCoe).IsCycles
hcac : cycles.Adj a c
hM1sub : M1.spanningCoe ≤ G ⊔ edge x b
hM2sub : M2.spanningCoe ≤ G ⊔ edge a c
⊢ cycles ≤ G ⊔ edge a c ⊔ edge x b
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: case zero
p : ℕ
⊢ Nat.rec 1 (fun y IH ↦ IH * (unpair p).1) 0 = (unpair p).1 ^ 0

Tactic:
simp [*, Nat.pow_succ]

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

Goal state before:
pp: case succ
p n✝ : ℕ
a✝ : Nat.rec 1 (fun y IH ↦ IH * (unpair p).1) n✝ = (unpair p).1 ^ n✝
⊢ Nat.rec 1 (fun y IH ↦ IH * (unpair p).1) (n✝ + 1) = (unpair p).1 ^ (n✝ + 1)

Tactic:
simp [*, Nat.pow_succ]

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

Goal state before:
pp: α : Type u_1
inst✝ : Primcodable α
n : ℕ
⊢ (Nat.casesOn (encode (decode n)) 0 fun n ↦ n.succ.succ) = encode (Option.map some (decode n))

Tactic:
by
    cases @decode α _ n <;> simp

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

Goal state before:
pp: this : PrimrecRel fun a b ↦ a.2 = 0 ∧ b = 0 ∨ 0 < a.2 ∧ b * a.2 ≤ a.1 ∧ a.1 < (b + 1) * a.2
a k q : ℕ
H : k = 0
⊢ (a, k).2 = 0 ∧ q = 0 ∨ 0 < (a, k).2 ∧ q * (a, k).2 ≤ (a, k).1 ∧ (a, k).1 < (q + 1) * (a, k).2 ↔
    (fun x1 x2 ↦ x1 / x2) (a, k).1 (a, k).2 = q

Tactic:
simp [H, eq_comm]

Goal state after:
Module: Mathlib.Computability.Ackermann

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

Tactic:
rw [ack_succ_succ]
    apply one_lt_ack_succ_left

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

Goal state before:
pp: f : ℝ → ℝ
hf✝ : GrowsPolynomially f
hf' : ∃ᶠ (x : ℝ) in atTop, f x = 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 : ℝ) in atTop, f x = 0

Tactic:
frequently_atTop

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 : ℝ) in atTop, f x = 0
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
h' : ∃ K, ¬Gmax.deleteUniversalVerts.coe.IsClique K.supp
⊢ False

Tactic:
obtain ⟨K, hK⟩ := h'
    obtain ⟨x, y, hxy⟩ := (not_isClique_iff _).mp hK
    obtain ⟨p, hp⟩ := Reachable.exists_path_of_dist (K.connected_toSimpleGraph x y)
    obtain ⟨x, a, b, hxa, hxb, hnadjxb, hnxb⟩ := Walk.exists_adj_adj_not_adj_ne hp.2
      (p.reachable.one_lt_dist_of_ne_of_not_adj hxy.1 hxy.2)
    simp only [ConnectedComponent.toSimpleGraph, deleteUniversalVerts, universalVerts,
      Subgraph.verts_top, comap_adj, Function.Embedding.coe_subtype,
      Subgraph.coe_adj, Subgraph.induce_adj, Subtype.coe_prop, Subgraph.top_adj, true_and]
      at hxa hxb hnadjxb
    obtain ⟨c, hc⟩ : ∃ (c : V), (a : V) ≠ c ∧ ¬ Gmax.Adj a c := by
      simpa [universalVerts, IsUniversal] using a.1.2.2
    have hbnec : b.val.val ≠ c := by rintro rfl; exact hc.2 hxb
    obtain ⟨_, hG1⟩ := hMaximal _ <| left_lt_sup.mpr (by
      rw [edge_le_iff (v := x.1.1) (w := b.1.1)]
      simp [hnadjxb, Subtype.val_injective.ne <| Subtype.val_injective.ne hnxb])
    obtain ⟨_, hG2⟩ := hMaximal _ <| left_lt_sup.mpr (by
      rwa [edge_le_iff (v := a.1.1) (w := c), not_or])
    have hcnex : x.val.val ≠ c := by rintro rfl; exact hc.2 hxa.symm
    obtain ⟨Mcon, hMcon⟩ := tutte_exists_isPerfectMatching_of_near_matchings hxa
      hxb hnadjxb (fun hadj ↦ hc.2 hadj) (by lia) hcnex hc.1 hbnec hG1 hG2
    exact hMatchingFree Mcon hMcon

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 : ℝ
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), C ≤ ↑(r i n)

Tactic:
by
  obtain ⟨c, hc_mem, hc⟩ := R.exists_eventually_const_mul_le_r
  filter_upwards [eventually_ge_atTop ⌈C / c⌉₊, hc] with n hn₁ hn₂ i
  have h₁ := hc_mem.1
  calc C
    _ = c * (C / c) := by
      rw [← mul_div_assoc]
      exact (mul_div_cancel_left₀ _ (by positivity)).symm
    _ ≤ c * ⌈C / c⌉₊ := by gcongr; simp [Nat.le_ceil]
    _ ≤ c * n := by gcongr
    _ ≤ r i n := hn₂ i

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
i : α
n : ℕ
hn : n ≠ 0
⊢ (log ↑n - log (b i * ↑n)) / (log (b i * ↑n) * log ↑n) =
    (log ↑n - log (b i) - log ↑n) / ((log (b i) + log ↑n) * log ↑n)

Tactic:
have : 0 < b i := R.b_pos i

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
n : ℕ
hn : n ≠ 0
this : 0 < b i
⊢ (log ↑n - log (b i * ↑n)) / (log (b i * ↑n) * log ↑n) =
    (log ↑n - log (b i) - log ↑n) / ((log (b i) + log ↑n) * log ↑n)
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)‖
⊢ (fun n ↦ ‖b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)‖) =ᶠ[atTop] fun n ↦
    b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)

Tactic:
by
        filter_upwards [eventually_gt_atTop ⌈(b i)⁻¹⌉₊, eventually_gt_atTop 1] with n hn hn'
        refine norm_of_nonneg ?_
        have h₁ := R.b_pos i
        have h₂ : 0 ≤ ε (b i * n) - ε n := by
          refine sub_nonneg_of_le <|
            (strictAntiOn_smoothingFn.le_iff_ge ?n_gt_one ?bn_gt_one).mpr ?le
          case n_gt_one =>
            change 1 < (n : ℝ)
            rw [Nat.one_lt_cast]
            exact hn'
          case bn_gt_one =>
            calc 1 = b i * (b i)⁻¹ := by rw [mul_inv_cancel₀ (by positivity)]
                _ ≤ b i * ⌈(b i)⁻¹⌉₊ := by gcongr; exact Nat.le_ceil _
                _ < b i * n := by gcongr
          case le => calc b i * n
            _ ≤ 1 * n := by have := R.b_lt_one i; gcongr
            _ = n := by rw [one_mul]
        positivity

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case neg.succ
k : ℕ
cf : Code
hf : ∀ (n x : ℕ), x ∈ evaln (k + 1) cf n → x ∈ cf.eval n
n : ℕ
left✝ : n ≤ k
m : ℕ
h₁ : evaln (k + 1) cf n = some m
m0 : ¬m = 0
y : ℕ
hy₁ : 0 ∈ cf.eval (Nat.pair (unpair n).1 (y + ((unpair n).2 + 1)))
hy₂ : ∀ {m : ℕ}, m < y → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m + ((unpair n).2 + 1))), ¬a = 0
h₂ : evaln k cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1)) = some (y + ((unpair n).2 + 1))
i : ℕ
im : i + 1 < y + 1
⊢ ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (i + 1 + (unpair n).2)), ¬a = 0

Tactic:
rcases hy₂ (Nat.lt_of_succ_lt_succ im) with ⟨z, hz, z0⟩

Goal state after:
case neg.succ
k : ℕ
cf : Code
hf : ∀ (n x : ℕ), x ∈ evaln (k + 1) cf n → x ∈ cf.eval n
n : ℕ
left✝ : n ≤ k
m : ℕ
h₁ : evaln (k + 1) cf n = some m
m0 : ¬m = 0
y : ℕ
hy₁ : 0 ∈ cf.eval (Nat.pair (unpair n).1 (y + ((unpair n).2 + 1)))
hy₂ : ∀ {m : ℕ}, m < y → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m + ((unpair n).2 + 1))), ¬a = 0
h₂ : evaln k cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1)) = some (y + ((unpair n).2 + 1))
i : ℕ
im : i + 1 < y + 1
z : ℕ
hz : z ∈ cf.eval (Nat.pair (unpair n).1 (i + ((unpair n).2 + 1)))
z0 : ¬z = 0
⊢ ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (i + 1 + (unpair n).2)), ¬a = 0
Module: Mathlib.Computability.ContextFreeGrammar

Goal state before:
pp: T : Type u_1
g : ContextFreeGrammar T
v w : List (Symbol T g.NT)
hvw : g.Derives v w
p : List (Symbol T g.NT)
⊢ g.Derives (v ++ p) (w ++ p)

Tactic:
by
  induction hvw with
  | refl => rfl
  | tail _ last ih => exact ih.trans_produces <| last.append_right p

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

Goal state before:
pp: case pos.false
m n : ℕ
IH : shiftLeft' false m n ≠ 0 → (shiftLeft' false m n).size = m.size + n
h : ¬bit false 0 = 0
s0 : shiftLeft' false m n = 0
⊢ (size 0).succ = (m.size + n).succ

pp: case pos.true
m n : ℕ
IH : shiftLeft' true m n ≠ 0 → (shiftLeft' true m n).size = m.size + n
h : ¬bit true 0 = 0
s0 : shiftLeft' true m n = 0
⊢ (size 0).succ = (m.size + n).succ

Tactic:
· exact absurd rfl h

Goal state after:
case pos.true
m n : ℕ
IH : shiftLeft' true m n ≠ 0 → (shiftLeft' true m n).size = m.size + n
h : ¬bit true 0 = 0
s0 : shiftLeft' true m n = 0
⊢ (size 0).succ = (m.size + n).succ
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: a b c : ℕ
v : ℕ := a ^^^ b ^^^ c
h : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
⊢ c ^^^ a = b ^^^ v

Tactic:
hv,

Goal state after:
a b c : ℕ
v : ℕ := a ^^^ b ^^^ c
h : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
⊢ c ^^^ a = b ^^^ (a ^^^ b ^^^ c)
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case succ.comp
x✝ : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf cg : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode (cf.comp cg)) →
      lup
          (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair k (encode (cf.comp cg)))))
          (k', c') n =
        evaln k' c' n
⊢ ((lup
          (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair (k' + 1) (encode (cf.comp cg)))))
          (k' + 1, cg) n).bind
      fun x ↦
      lup
        (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
          (List.range (Nat.pair (k' + 1) (encode (cf.comp cg)))))
        (k' + 1, cf) x) =
    (evaln (k' + 1) cg n).bind fun x ↦ evaln (k' + 1) cf x

Tactic:
obtain ⟨lf, lg⟩ := encode_lt_comp cf cg

Goal state after:
case succ.comp
x✝ : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf cg : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode (cf.comp cg)) →
      lup
          (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair k (encode (cf.comp cg)))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode (cf.comp cg)
lg : encode cg < encode (cf.comp cg)
⊢ ((lup
          (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair (k' + 1) (encode (cf.comp cg)))))
          (k' + 1, cg) n).bind
      fun x ↦
      lup
        (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
          (List.range (Nat.pair (k' + 1) (encode (cf.comp cg)))))
        (k' + 1, cf) x) =
    (evaln (k' + 1) cg n).bind fun x ↦ evaln (k' + 1) cf x
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: case succ
n : ℕ
ih :
  List.foldl (fun x1 x2 ↦ x1 ^^^ x2) 0 (List.range (n + 1)) =
    match Fin.ofNat 4 n with
    | 0 => n
    | 1 => 1
    | 2 => n + 1
    | 3 => 0
⊢ (match Fin.ofNat 4 n with
      | 0 => n
      | 1 => 1
      | 2 => n + 1
      | 3 => 0) ^^^
      n + 1 =
    match Fin.ofNat 4 n + Fin.ofNat 4 1 with
    | 0 => n + 1
    | 1 => 1
    | 2 => n + 1 + 1
    | 3 => 0

Tactic:
match h : Fin.ofNat 4 n with
    | 0 =>
      rw [Fin.zero_add, ← xor_one_of_even <| even_iff.mpr ?_, xor_xor_cancel_left]
      rw [← @mod_mod_of_dvd _ 4 _ <| by simp, ← Fin.val_ofNat 4, h]
      rfl
    | 1 =>
      rw [Nat.xor_comm]
      refine xor_one_of_even <| even_iff.mpr ?_
      rw [add_mod, ← @mod_mod_of_dvd _ 4 n <| by simp, ← Fin.val_ofNat 4, h]
      rfl
    | 2 =>
      apply Nat.xor_self
    | 3 =>
      apply zero_xor

Goal state after:
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: α : Type u_1
l : List (Option α)
x : α
⊢ some x ∈ l ↔ x ∈ l.reduceOption

Tactic:
reduceOption_mem_iff

Goal state after:
α : Type u_1
l : List (Option α)
x : α
⊢ some x ∈ l ↔ some x ∈ l
Module: Mathlib.Computability.MyhillNerode

Goal state before:
pp: α : Type u
L : Language α
x : List α
⊢ x ∈ L.toDFA.accepts ↔ x ∈ L

Tactic:
rw [DFA.mem_accepts]

Goal state after:
α : Type u
L : Language α
x : List α
⊢ L.toDFA.eval x ∈ L.toDFA.accept ↔ x ∈ L
Module: Mathlib.Computability.RE

Goal state before:
pp: case inr.some
cf : Code
hf : Nat.Partrec cf.eval
cg : Code
hg : Nat.Partrec cg.eval
this✝ : Nat.Partrec fun n ↦ rfindOpt fun k ↦ Code.evaln k cf n <|> Code.evaln k cg n
n : ℕ
this : ∀ x ∈ rfindOpt fun k ↦ Code.evaln k cf n <|> Code.evaln k cg n, x ∈ cf.eval n ∨ x ∈ cg.eval n
x k : ℕ
e : Code.evaln k cg n = Option.some x
y : ℕ
⊢ ∃ a, a ∈ (Option.some y <|> Code.evaln k cg n)

Tactic:
exact ⟨y, by simp⟩

Goal state after: