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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
x✝ : Nonempty (G.CompleteEquipartiteSubgraph (r + 1) t)
K' : G.CompleteEquipartiteSubgraph (r + 1) t
parts : Finset (Finset V)
hparts_sub : parts ⊆ K'.parts
hparts_card : #parts = (#K'.parts).pred
⊢ #parts = r ∨ t = 0

Tactic:
rw [hparts_card, K'.card_parts.resolve_right ht]

Goal state after:
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
x✝ : Nonempty (G.CompleteEquipartiteSubgraph (r + 1) t)
K' : G.CompleteEquipartiteSubgraph (r + 1) t
parts : Finset (Finset V)
hparts_sub : parts ⊆ K'.parts
hparts_card : #parts = (#K'.parts).pred
⊢ (r + 1).pred = r ∨ t = 0
Module: Mathlib.Combinatorics.SimpleGraph.Girth

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
⊢ (∃ a w, w.IsCycle ∧ G.egirth = ↑w.length) ↔ ¬G.IsAcyclic

Tactic:
by
  refine ⟨?_, fun h ↦ ?_⟩
  · rintro ⟨a, w, hw, _⟩ hG
    exact hG _ hw
  · simp_rw [← egirth_eq_top, ← Ne.eq_def, egirth, iInf_subtype', iInf_sigma',
      ENat.iInf_natCast_ne_top, ← exists_prop, Subtype.exists', Sigma.exists', eq_comm] at h ⊢
    exact ciInf_mem _

Goal state after:
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: α : Type u_1
s : Set α
h : s.Infinite
⊢ ∃ t u, t ∪ u = s ∧ Disjoint t u ∧ #↑t = #↑u

Tactic:
by
  have := h.to_subtype
  obtain ⟨f⟩ : Nonempty (s ≃ s ⊕ s) := by
    rw [← Cardinal.eq, ← add_def, add_mk_eq_self]
  refine ⟨Subtype.val '' f ⁻¹' (range .inl), Subtype.val '' f ⁻¹' (range .inr), ?_, ?_, ?_⟩
  · simp [← image_union, ← preimage_union]
  · exact disjoint_image_of_injective Subtype.val_injective
      (isCompl_range_inl_range_inr.disjoint.preimage f)
  · simp [mk_image_eq Subtype.val_injective]

Goal state after:
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)
| ↑(#K.verts) * ((1 - 1 / ↑r + ε) * ↑n - ↑(#K.verts)) +
    (↑(#K.verts) * (↑(#K.verts) - (↑t' - ↑t)) - ↑n * (↑(#K.verts) - (↑t' - ↑t)))

Tactic:
mul_sub,

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

Tactic:
mul_sub,

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'
hδ : ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n
N : ℕ
hN : (↑N + ↑r * ↑t') * (↑t' - ↑t) ≤ ↑n * (↑r * ↑t' * ε - ↑t)
| ↑(#K.verts) * ((1 - 1 / ↑r + ε) * ↑n) - ↑(#K.verts) * ↑(#K.verts) +
      (↑(#K.verts) * ↑(#K.verts) - ↑(#K.verts) * (↑t' - ↑t)) -
    ↑n * (↑(#K.verts) - (↑t' - ↑t))
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: case inr
V : Type u_1
G : SimpleGraph V
M M' : G.Subgraph
hM : M.IsMatching
hM' : M'.IsMatching
hd : Disjoint M.support M'.support
v : V
hv : v ∈ (M ⊔ M').verts
aux : ∀ {N N' : G.Subgraph}, N.IsMatching → Disjoint N.support N'.support → v ∈ N.verts → ∃! w, (N ⊔ N').Adj v w
hmM' : v ∈ M'.verts
⊢ ∃! w, (M ⊔ M').Adj v w

Tactic:
rw [sup_comm]
    exact aux hM' (Disjoint.symm hd) hmM'

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
G : SimpleGraph α
a b : α
p : G.Walk a b
hp : p.IsHamiltonian
⊢ Finite α

Tactic:
have := hp.fintype; infer_instance

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

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
a b : α
p : G.Walk a b
inst✝ : Fintype α
h✝ : Nonempty α
x✝ : p.IsPath ∧ p.length = Fintype.card α - 1
hp : p.IsPath
h : p.length = Fintype.card α - 1
this : Injective fun x ↦ p.support.get x
⊢ p.IsHamiltonian

Tactic:
refine isHamiltonian_iff_support_get_bijective.mpr ⟨this, this.surjective_of_finite ?_⟩

Goal state after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
a b : α
p : G.Walk a b
inst✝ : Fintype α
h✝ : Nonempty α
x✝ : p.IsPath ∧ p.length = Fintype.card α - 1
hp : p.IsPath
h : p.length = Fintype.card α - 1
this : Injective fun x ↦ p.support.get x
⊢ Fin p.support.length ≃ α
Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
G : SimpleGraph α
a : α
p : G.Walk a a
hp : p.IsHamiltonianCycle
⊢ List.count a p.support.tail + 1 = 2

Tactic:
← support_tail_of_not_nil _ hp.1.not_nil,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
G : SimpleGraph α
a : α
p : G.Walk a a
hp : p.IsHamiltonianCycle
⊢ List.count a p.tail.support + 1 = 2
Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian

Goal state before:
pp: case h
α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
inst✝ : Fintype α
u v : α
he : G.IsBridge s(u, v)
this : Nontrivial α
hG : G.IsHamiltonian
⊢ False

Tactic:
obtain ⟨p, hp⟩ := hG.exists_isHamiltonianCycle u

Goal state after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
inst✝ : Fintype α
u v : α
he : G.IsBridge s(u, v)
this : Nontrivial α
hG : G.IsHamiltonian
p : G.Walk u u
hp : p.IsHamiltonianCycle
⊢ False
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 w : V
hw : w ∈ G.neighborFinset v
⊢ #(bipartiteAbove G.Adj (Gᶜ.neighborFinset v) w) = k - ℓ - 1

Tactic:
mem_neighborFinset

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 : G.Adj v w
⊢ #(bipartiteAbove G.Adj (Gᶜ.neighborFinset v) w) = k - ℓ - 1
Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular

Goal state before:
pp: 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
⊢ v ∈ G.neighborFinset w ∧ v ∉ G.neighborFinset v

Tactic:
mem_neighborFinset

Goal state after:
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
⊢ G.Adj w v ∧ v ∉ G.neighborFinset v
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 w : V
hw : G.Adj v w
s : {v} ⊆ G.neighborFinset w \ G.neighborFinset v
⊢ #(Gᶜ.neighborFinset v ∩ G.neighborFinset w) = k - ℓ - 1

Tactic:
rw [inter_comm, neighborFinset_compl, ← inter_sdiff_assoc, ← sdiff_eq_inter_compl,
      card_sdiff_of_subset s, card_singleton, ← sdiff_inter_self_left,
      card_sdiff_of_subset inter_subset_left]

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 : G.Adj v w
s : {v} ⊆ G.neighborFinset w \ G.neighborFinset v
⊢ #(G.neighborFinset w) - #(G.neighborFinset w ∩ G.neighborFinset v) - 1 = k - ℓ - 1
Module: Mathlib.Combinatorics.SimpleGraph.Trails

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

Tactic:
rw [Nat.even_add_one, ih]

Goal state after:
case pos.inl
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v x v✝ w✝ : V
p : G.Walk v✝ w✝
ih : Even (List.countP (fun e ↦ decide (x ∈ e)) p.edges) ↔ v✝ ≠ w✝ → x ≠ v✝ ∧ x ≠ w✝
huv : G.Adj x v✝
ht : p.IsTrail ∧ s(x, v✝) ∉ p.edges
⊢ ¬(v✝ ≠ w✝ → x ≠ v✝ ∧ x ≠ w✝) ↔ ¬x = w✝ → ¬x = x ∧ ¬x = w✝
Module: Mathlib.Combinatorics.SimpleGraph.Trails

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝¹ : DecidableEq V
inst✝ : Fintype ↑G.edgeSet
u v : V
p : G.Walk u v
h : p.IsEulerian
e : Sym2 V
⊢ e ∈ ⋯.edgesFinset ↔ e ∈ G.edgeFinset

Tactic:
simp [h.mem_edges_iff]

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
h : (⊤.deleteVerts G.universalVerts).coe.oddComponents.ncard ≤ G.universalVerts.ncard
⊢ (Subtype.val '' ?m.40).ncard ≤ (universalVerts ?m.39).ncard

Tactic:
Set.ncard_image_of_injective _ Subtype.val_injective,

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
h : (⊤.deleteVerts G.universalVerts).coe.oddComponents.ncard ≤ G.universalVerts.ncard
⊢ Set.ncard ?m.60 ≤ (universalVerts ?m.39).ncard

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
⊢ Type ?u.46

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
⊢ Set { x // x ∈ (deleteUniversalVerts ?m.39).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
exists_complMatch :
  ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), ∃ M, M.verts = Subtype.val '' K.supp \ M1.verts ∧ M.IsMatching
⊢ ∃ M, M.IsMatching ∧ M.vertsᶜ ⊆ G.universalVerts

Tactic:
choose complMatch hcomplMatch_compl hcomplMatch_match using exists_complMatch

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
⊢ ∃ M, M.IsMatching ∧ M.vertsᶜ ⊆ G.universalVerts
Module: Mathlib.Data.Nat.PSub

Goal state before:
pp: n : ℕ
⊢ (n + 1).ppred = none ↔ n + 1 = 0

Tactic:
constructor <;> intro

Goal state after:
case mp
n : ℕ
a✝ : (n + 1).ppred = none
⊢ n + 1 = 0

case mpr
n : ℕ
a✝ : n + 1 = 0
⊢ (n + 1).ppred = none
Module: Mathlib.Computability.Primrec.Basic

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

Tactic:
Option.map_some

Goal state after:
α : Type u_1
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable σ
inst✝ : Finite α
f : α → σ
l : List α
left✝ : l.Nodup
m : ∀ (x : α), x ∈ l
this : DecidableEq α
a : α
⊢ some (f a) = some (f a)
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : 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
n : ℕ
h₂ : Sum.inl b ∈ F a n
_x : ∃ b', Sum.inl b' ∈ F a n
h₁ : ∀ {m : ℕ}, m < n → ∃ b, Sum.inr b ∈ F a m
m : ℕ
a' : α
am : Sum.inr a' ∈ F a m
ba : b ∈ f.fix a'
⊢ b ∈ f.fix a

Tactic:
induction m generalizing a' with

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

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

Tactic:
div_eq_mul_inv,

Goal state after:
⊢ (fun x ↦ -(x⁻¹ * (log x ^ 2)⁻¹)) = fun x ↦ (-x * log x ^ 2)⁻¹
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: c : Code
n x : ℕ
h : x ∈ evaln 0 c n
⊢ n < 0

Tactic:
by simp [evaln] at h

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: k₂ : ℕ
c : Code
n x : ℕ
x✝ : 0 ≤ k₂
h : x ∈ evaln 0 c n
⊢ x ∈ evaln k₂ c n

Tactic:
by simp [evaln] at h

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: x✝ : Code
n x : ℕ
h : x ∈ evaln 0 x✝ n
⊢ x ∈ x✝.eval n

Tactic:
by simp [evaln] at h

Goal state after:
Module: Mathlib.Computability.Language

Goal state before:
pp: case mp
α : Type u_1
l : Language α
S : List (List α)
h : ∀ y ∈ S, y ∈ l
⊢ ∃ S_1, S.flatten = S_1.flatten ∧ ∀ y ∈ S_1, y ∈ l ∧ y ≠ []

Tactic:
refine ⟨S.filter fun l ↦ !List.isEmpty l,
      by simp [List.flatten_filter_not_isEmpty], fun y hy ↦ ?_⟩

Goal state after:
case mp
α : Type u_1
l : Language α
S : List (List α)
h : ∀ y ∈ S, y ∈ l
y : List α
hy : y ∈ filter (fun l ↦ !l.isEmpty) S
⊢ y ∈ l ∧ y ≠ []
Module: Mathlib.Computability.Language

Goal state before:
pp: α : Type u_1
l : Language α
⊢ l∗ * l = l * l∗

Tactic:
simp only [kstar_eq_iSup_pow, mul_iSup, iSup_mul, ← pow_succ, ← pow_succ']

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

Goal state before:
pp: case bit
b : Bool
n : ℕ
hn : n ≠ 0 → ∃ i, n.testBit i = true ∧ ∀ (j : ℕ), i < j → n.testBit j = false
h : bit b n ≠ 0
⊢ ∃ i, (bit b n).testBit i = true ∧ ∀ (j : ℕ), i < j → (bit b n).testBit j = false

Tactic:
by_cases h' : n = 0

Goal state after:
case pos
b : Bool
n : ℕ
hn : n ≠ 0 → ∃ i, n.testBit i = true ∧ ∀ (j : ℕ), i < j → n.testBit j = false
h : bit b n ≠ 0
h' : n = 0
⊢ ∃ i, (bit b n).testBit i = true ∧ ∀ (j : ℕ), i < j → (bit b n).testBit j = false

case neg
b : Bool
n : ℕ
hn : n ≠ 0 → ∃ i, n.testBit i = true ∧ ∀ (j : ℕ), i < j → n.testBit j = false
h : bit b n ≠ 0
h' : ¬n = 0
⊢ ∃ i, (bit b n).testBit i = true ∧ ∀ (j : ℕ), i < j → (bit b n).testBit j = false
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: case zero
m i : ℕ
hn : testBit 0 i = false
hm : m.testBit i = true
hnm : ∀ (j : ℕ), i < j → testBit 0 j = m.testBit j
⊢ 0 < m

Tactic:
Nat.pos_iff_ne_zero

Goal state after:
case zero
m i : ℕ
hn : testBit 0 i = false
hm : m.testBit i = true
hnm : ∀ (j : ℕ), i < j → testBit 0 j = m.testBit j
⊢ m ≠ 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: x✝¹ x✝ : Num
⊢ x✝¹ * x✝ = x✝ * x✝¹

Tactic:
by simp_rw [← to_nat_inj, mul_to_nat, mul_comm]

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

Goal state before:
pp: f g : ℝ → ℝ
hg✝ : GrowsPolynomially g
hf : f =Θ[atTop] g
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_pos : 0 < b
c₁ : ℝ
hc₁_pos : 0 < c₁
hf_lb : ∀ᶠ (x : ℝ) in atTop, c₁ * ‖g x‖ ≤ ‖f x‖
c₂ : ℝ
hc₂_pos : 0 < c₂
hf_ub : ∀ᶠ (x : ℝ) in atTop, ‖f x‖ ≤ c₂ * ‖g x‖
c₃ : ℝ
hc₃_pos : 0 < c₃
c₄ : ℝ
hc₄_pos : 0 < c₄
hg :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x, (fun x ↦ ‖g x‖) u ∈ Set.Icc (c₃ * (fun x ↦ ‖g x‖) x) (c₄ * (fun x ↦ ‖g x‖) x)
h_lb_pos : 0 < c₁ * c₂⁻¹ * c₃
h_ub_pos : 0 < c₂ * c₄ * c₁⁻¹
c₂_cancel : c₂⁻¹ * c₂ = 1
c₁_cancel : c₁⁻¹ * c₁ = 1
x : ℝ
hf_pos : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
h_lb : ∀ (y : ℝ), b * id x ≤ y → c₁ * ‖g y‖ ≤ ‖f y‖
h_ub : ∀ (y : ℝ), b * id x ≤ y → ‖f y‖ ≤ c₂ * ‖g y‖
hg_bound✝ : ∀ (y : ℝ), b * id x ≤ y → ∀ u ∈ Set.Icc (b * y) y, ‖g u‖ ∈ Set.Icc (c₃ * ‖g y‖) (c₄ * ‖g y‖)
hx_pos : 0 ≤ x
u : ℝ
hu : u ∈ Set.Icc (b * x) x
hbx : b * x ≤ x
hg_bound : ∀ u ∈ Set.Icc (b * x) x, ‖g u‖ ∈ Set.Icc (c₃ * ‖g x‖) (c₄ * ‖g x‖)
⊢ c₂⁻¹ * c₂ * c₁ * (c₃ * ‖g x‖) = c₁ * (c₃ * ‖g x‖)

Tactic:
simp [c₂_cancel]

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

Goal state before:
pp: case zero.zero
f : Num → Num → Num
g : Bool → Bool → Bool
p : PosNum → PosNum → Num
gff : g false false = false
f00 : f 0 0 = 0
f0n : ∀ (n : PosNum), f 0 (pos n) = bif g false true then pos n else 0
fn0 : ∀ (n : PosNum), f (pos n) 0 = bif g true false then pos n else 0
fnn : ∀ (m n : PosNum), f (pos m) (pos n) = p m n
p11 : p 1 1 = bif g true true then 1 else 0
p1b : ∀ (b : Bool) (n : PosNum), p 1 (PosNum.bit b n) = bit (g true b) (bif g false true then pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then pos m else 0)
pbb : ∀ (a b : Bool) (m n : PosNum), p (PosNum.bit a m) (PosNum.bit b n) = bit (g a b) (p m n)
⊢ ↑(f zero zero) = Nat.bitwise g ↑zero ↑zero

Tactic:
simp only [show zero = 0 from rfl, show ((0 : Num) : ℕ) = 0 from rfl]

Goal state after:
case zero.zero
f : Num → Num → Num
g : Bool → Bool → Bool
p : PosNum → PosNum → Num
gff : g false false = false
f00 : f 0 0 = 0
f0n : ∀ (n : PosNum), f 0 (pos n) = bif g false true then pos n else 0
fn0 : ∀ (n : PosNum), f (pos n) 0 = bif g true false then pos n else 0
fnn : ∀ (m n : PosNum), f (pos m) (pos n) = p m n
p11 : p 1 1 = bif g true true then 1 else 0
p1b : ∀ (b : Bool) (n : PosNum), p 1 (PosNum.bit b n) = bit (g true b) (bif g false true then pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then pos m else 0)
pbb : ∀ (a b : Bool) (m n : PosNum), p (PosNum.bit a m) (PosNum.bit b n) = bit (g a b) (p m n)
⊢ ↑(f 0 0) = Nat.bitwise g 0 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case zero.pos
f : Num → Num → Num
g : Bool → Bool → Bool
p : PosNum → PosNum → Num
gff : g false false = false
f00 : f 0 0 = 0
f0n : ∀ (n : PosNum), f 0 (pos n) = bif g false true then pos n else 0
fn0 : ∀ (n : PosNum), f (pos n) 0 = bif g true false then pos n else 0
fnn : ∀ (m n : PosNum), f (pos m) (pos n) = p m n
p11 : p 1 1 = bif g true true then 1 else 0
p1b : ∀ (b : Bool) (n : PosNum), p 1 (PosNum.bit b n) = bit (g true b) (bif g false true then pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then pos m else 0)
pbb : ∀ (a b : Bool) (m n : PosNum), p (PosNum.bit a m) (PosNum.bit b n) = bit (g a b) (p m n)
n : PosNum
⊢ ↑(f zero (pos n)) = Nat.bitwise g ↑zero ↑(pos n)

Tactic:
simp only [show zero = 0 from rfl, show ((0 : Num) : ℕ) = 0 from rfl]

Goal state after:
case zero.pos
f : Num → Num → Num
g : Bool → Bool → Bool
p : PosNum → PosNum → Num
gff : g false false = false
f00 : f 0 0 = 0
f0n : ∀ (n : PosNum), f 0 (pos n) = bif g false true then pos n else 0
fn0 : ∀ (n : PosNum), f (pos n) 0 = bif g true false then pos n else 0
fnn : ∀ (m n : PosNum), f (pos m) (pos n) = p m n
p11 : p 1 1 = bif g true true then 1 else 0
p1b : ∀ (b : Bool) (n : PosNum), p 1 (PosNum.bit b n) = bit (g true b) (bif g false true then pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then pos m else 0)
pbb : ∀ (a b : Bool) (m n : PosNum), p (PosNum.bit a m) (PosNum.bit b n) = bit (g a b) (p m n)
n : PosNum
⊢ ↑(f 0 (pos n)) = Nat.bitwise g 0 ↑(pos n)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pos.zero
f : Num → Num → Num
g : Bool → Bool → Bool
p : PosNum → PosNum → Num
gff : g false false = false
f00 : f 0 0 = 0
f0n : ∀ (n : PosNum), f 0 (pos n) = bif g false true then pos n else 0
fn0 : ∀ (n : PosNum), f (pos n) 0 = bif g true false then pos n else 0
fnn : ∀ (m n : PosNum), f (pos m) (pos n) = p m n
p11 : p 1 1 = bif g true true then 1 else 0
p1b : ∀ (b : Bool) (n : PosNum), p 1 (PosNum.bit b n) = bit (g true b) (bif g false true then pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then pos m else 0)
pbb : ∀ (a b : Bool) (m n : PosNum), p (PosNum.bit a m) (PosNum.bit b n) = bit (g a b) (p m n)
m : PosNum
⊢ ↑(f (pos m) zero) = Nat.bitwise g ↑(pos m) ↑zero

Tactic:
simp only [show zero = 0 from rfl, show ((0 : Num) : ℕ) = 0 from rfl]

Goal state after:
case pos.zero
f : Num → Num → Num
g : Bool → Bool → Bool
p : PosNum → PosNum → Num
gff : g false false = false
f00 : f 0 0 = 0
f0n : ∀ (n : PosNum), f 0 (pos n) = bif g false true then pos n else 0
fn0 : ∀ (n : PosNum), f (pos n) 0 = bif g true false then pos n else 0
fnn : ∀ (m n : PosNum), f (pos m) (pos n) = p m n
p11 : p 1 1 = bif g true true then 1 else 0
p1b : ∀ (b : Bool) (n : PosNum), p 1 (PosNum.bit b n) = bit (g true b) (bif g false true then pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then pos m else 0)
pbb : ∀ (a b : Bool) (m n : PosNum), p (PosNum.bit a m) (PosNum.bit b n) = bit (g a b) (p m n)
m : PosNum
⊢ ↑(f (pos m) 0) = Nat.bitwise g (↑(pos m)) 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pos.pos
f : Num → Num → Num
g : Bool → Bool → Bool
p : PosNum → PosNum → Num
gff : g false false = false
f00 : f 0 0 = 0
f0n : ∀ (n : PosNum), f 0 (pos n) = bif g false true then pos n else 0
fn0 : ∀ (n : PosNum), f (pos n) 0 = bif g true false then pos n else 0
fnn : ∀ (m n : PosNum), f (pos m) (pos n) = p m n
p11 : p 1 1 = bif g true true then 1 else 0
p1b : ∀ (b : Bool) (n : PosNum), p 1 (PosNum.bit b n) = bit (g true b) (bif g false true then pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then pos m else 0)
pbb : ∀ (a b : Bool) (m n : PosNum), p (PosNum.bit a m) (PosNum.bit b n) = bit (g a b) (p m n)
m n : PosNum
⊢ ↑(f (pos m) (pos n)) = Nat.bitwise g ↑(pos m) ↑(pos n)

Tactic:
simp only [show zero = 0 from rfl, show ((0 : Num) : ℕ) = 0 from rfl]

Goal state after:
case pos.pos
f : Num → Num → Num
g : Bool → Bool → Bool
p : PosNum → PosNum → Num
gff : g false false = false
f00 : f 0 0 = 0
f0n : ∀ (n : PosNum), f 0 (pos n) = bif g false true then pos n else 0
fn0 : ∀ (n : PosNum), f (pos n) 0 = bif g true false then pos n else 0
fnn : ∀ (m n : PosNum), f (pos m) (pos n) = p m n
p11 : p 1 1 = bif g true true then 1 else 0
p1b : ∀ (b : Bool) (n : PosNum), p 1 (PosNum.bit b n) = bit (g true b) (bif g false true then pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then pos m else 0)
pbb : ∀ (a b : Bool) (m n : PosNum), p (PosNum.bit a m) (PosNum.bit b n) = bit (g a b) (p m n)
m n : PosNum
⊢ ↑(f (pos m) (pos n)) = Nat.bitwise g ↑(pos m) ↑(pos n)