mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f : ℝ → ℝ
hf✝¹ : GrowsPolynomially f
hf_pos_or_neg : (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
hf✝ : GrowsPolynomially fun x ↦ |f x|
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_pos : 0 < b
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x, (fun x ↦ |f x|) u ∈ Set.Icc (c₁ * (fun x ↦ |f x|) x) (c₂ * (fun x ↦ |f x|) x)
x : ℝ
hx : ∀ u ∈ Set.Icc (b * x) x, |f u| ∈ Set.Icc (c₁ * |f x|) (c₂ * |f x|)
hx' : f x ≠ 0
hx'' : ∀ (y : ℝ), b * id x ≤ y → f y ≠ 0
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ f u ≠ 0

Tactic:
;

Goal state after:
f : ℝ → ℝ
hf✝¹ : GrowsPolynomially f
hf_pos_or_neg : (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
hf✝ : GrowsPolynomially fun x ↦ |f x|
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_pos : 0 < b
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x, (fun x ↦ |f x|) u ∈ Set.Icc (c₁ * (fun x ↦ |f x|) x) (c₂ * (fun x ↦ |f x|) x)
x : ℝ
hx : ∀ u ∈ Set.Icc (b * x) x, |f u| ∈ Set.Icc (c₁ * |f x|) (c₂ * |f x|)
hx' : f x ≠ 0
hx'' : ∀ (y : ℝ), b * id x ≤ y → f y ≠ 0
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ f u ≠ 0
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n x : ℕ
⊢ (1 + 2 * x) / 2 = x

Tactic:
;

Goal state after:
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n x : ℕ
⊢ (1 + 2 * x) / 2 = x
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:
;

Goal state after:
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

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.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
x✝ : ℝ
⊢ f x✝ / g x✝ = f x✝ * (g x✝)⁻¹

Tactic:
;

Goal state after:
f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
x✝ : ℝ
⊢ f x✝ / g x✝ = f x✝ * (g x✝)⁻¹
Module: Mathlib.Data.Nat.Size

Goal state before:
pp: n : ℕ
⊢ 2 ^ 0 ≤ n ↔ 0 < n

Tactic:
;

Goal state after:
n : ℕ
⊢ 2 ^ 0 ≤ n ↔ 0 < n
Module: Mathlib.Data.Num.Basic

Goal state before:
pp: a b : PosNum
⊢ Decidable (a.cmp b = lt)

Tactic:
;

Goal state after:
a b : PosNum
⊢ Decidable (a.cmp b = lt)
Module: Mathlib.Data.Num.Basic

Goal state before:
pp: a b : PosNum
⊢ Decidable ¬b < a

Tactic:
;

Goal state after:
a b : PosNum
⊢ Decidable ¬b < a
Module: Mathlib.Data.Num.Basic

Goal state before:
pp: a b : Num
⊢ Decidable (a.cmp b = lt)

Tactic:
;

Goal state after:
a b : Num
⊢ Decidable (a.cmp b = lt)
Module: Mathlib.Data.Num.Basic

Goal state before:
pp: a b : Num
⊢ Decidable ¬b < a

Tactic:
;

Goal state after:
a b : Num
⊢ Decidable ¬b < a
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg✝ : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : b ∈ Set.Ioo 0 1
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
hc₂p : 0 < c₂ ^ p
h✝ : 0 ≤ p
x : ℝ
a✝ : 0 < x
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hf_nonneg : 0 ≤ f x
hf_nonneg₂ : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
fu_nonneg : 0 ≤ f u
⊢ c₁ ^ p * f x ^ p = (c₁ * f x) ^ p

Tactic:
mul_rpow (le_of_lt hc₁_mem) hf_nonneg

Goal state after:
f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg✝ : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : b ∈ Set.Ioo 0 1
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
hc₂p : 0 < c₂ ^ p
h✝ : 0 ≤ p
x : ℝ
a✝ : 0 < x
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hf_nonneg : 0 ≤ f x
hf_nonneg₂ : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
fu_nonneg : 0 ≤ f u
⊢ c₁ ^ p * f x ^ p = c₁ ^ p * f x ^ p
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: case h₁
f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg✝ : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : b ∈ Set.Ioo 0 1
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
hc₂p : 0 < c₂ ^ p
h✝ : 0 ≤ p
x : ℝ
a✝ : 0 < x
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hf_nonneg : 0 ≤ f x
hf_nonneg₂ : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
fu_nonneg : 0 ≤ f u
⊢ c₁ * f x ≤ f u

Tactic:
;

Goal state after:
case h₁
f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg✝ : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : b ∈ Set.Ioo 0 1
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
hc₂p : 0 < c₂ ^ p
h✝ : 0 ≤ p
x : ℝ
a✝ : 0 < x
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hf_nonneg : 0 ≤ f x
hf_nonneg₂ : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
fu_nonneg : 0 ≤ f u
⊢ c₁ * f x ≤ f u
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: case h₁
f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg✝ : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : b ∈ Set.Ioo 0 1
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
hc₂p : 0 < c₂ ^ p
h✝ : 0 ≤ p
x : ℝ
a✝ : 0 < x
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hf_nonneg : 0 ≤ f x
hf_nonneg₂ : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
fu_nonneg : 0 ≤ f u
⊢ f u ≤ c₂ * f x

Tactic:
;

Goal state after:
case h₁
f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg✝ : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : b ∈ Set.Ioo 0 1
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
hc₂p : 0 < c₂ ^ p
h✝ : 0 ≤ p
x : ℝ
a✝ : 0 < x
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hf_nonneg : 0 ≤ f x
hf_nonneg₂ : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
fu_nonneg : 0 ≤ f u
⊢ f u ≤ c₂ * f x
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg✝ : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : b ∈ Set.Ioo 0 1
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
hc₂p : 0 < c₂ ^ p
h✝ : 0 ≤ p
x : ℝ
a✝ : 0 < x
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hf_nonneg : 0 ≤ f x
hf_nonneg₂ : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
fu_nonneg : 0 ≤ f u
⊢ (c₂ * f x) ^ p = c₂ ^ p * f x ^ p

Tactic:
rw [← mul_rpow (le_of_lt hc₂_mem) hf_nonneg]

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

Goal state before:
pp: C : SNum → Sort u_1
z : (b : Bool) → C (zero b)
s : (b : Bool) → (p : SNum) → C p → C (b::p)
b : Bool
⊢ C (b::zero (decide ¬b = true))

Tactic:
;

Goal state after:
C : SNum → Sort u_1
z : (b : Bool) → C (zero b)
s : (b : Bool) → (p : SNum) → C p → C (b::p)
b : Bool
⊢ C (b::zero (decide ¬b = true))
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: 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
k : ℕ
hk : n.testBit k = true
hk' : ∀ (j : ℕ), k < j → n.testBit j = false
j : ℕ
hj : k + 1 < j
x : j = 0
⊢ False

Tactic:
;

Goal state after:
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
k : ℕ
hk : n.testBit k = true
hk' : ∀ (j : ℕ), k < j → n.testBit j = false
j : ℕ
hj : k + 1 < j
x : j = 0
⊢ False
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: 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
k : ℕ
hk : n.testBit k = true
hk' : ∀ (j : ℕ), k < j → n.testBit j = false
hj : k + 1 < 0
⊢ False

Tactic:
;

Goal state after:
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
k : ℕ
hk : n.testBit k = true
hk' : ∀ (j : ℕ), k < j → n.testBit j = false
hj : k + 1 < 0
⊢ False
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: n i : ℕ
⊢ n &&& 2 ^ i = (n.testBit i).toNat * 2 ^ i

Tactic:
refine eq_of_testBit_eq fun j => ?_
  obtain rfl | hij := Decidable.eq_or_ne i j <;> cases h : n.testBit i
  · simp [h]
  · simp [h]
  · simp [testBit_two_pow_of_ne hij]
  · simp [testBit_two_pow_of_ne hij]

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

Goal state before:
pp: f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : b ∈ Set.Ioo 0 1
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
hc₂p : 0 < c₂ ^ p
hp : p < 0
hneg : ∀ᶠ (x : ℝ) in atTop, f x < 0
x : ℝ
hx : 0 ≤ f x
hx' : f x < 0
⊢ False

Tactic:
;

Goal state after:
f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : b ∈ Set.Ioo 0 1
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
hc₂p : 0 < c₂ ^ p
hp : p < 0
hneg : ∀ᶠ (x : ℝ) in atTop, f x < 0
x : ℝ
hx : 0 ≤ f x
hx' : f x < 0
⊢ False
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: case inl
a b c : ℕ
v : ℕ := ⋯
h✝ : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
i : ℕ
hi : v.testBit i = true
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
h : a.testBit i = true
⊢ b ^^^ c < a

Tactic:
;

Goal state after:
case inl
a b c : ℕ
v : ℕ := ⋯
h✝ : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
i : ℕ
hi : v.testBit i = true
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
h : a.testBit i = true
⊢ b ^^^ c < a
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: case inr.inl
a b c : ℕ
v : ℕ := ⋯
h✝ : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
i : ℕ
hi : v.testBit i = true
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
h : b.testBit i = true
⊢ c ^^^ a < b ∨ a ^^^ b < c

Tactic:
;

Goal state after:
case inr.inl
a b c : ℕ
v : ℕ := ⋯
h✝ : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
i : ℕ
hi : v.testBit i = true
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
h : b.testBit i = true
⊢ c ^^^ a < b ∨ a ^^^ b < c
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: case inr.inl
a b c : ℕ
v : ℕ := ⋯
h✝ : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
i : ℕ
hi : v.testBit i = true
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
h : b.testBit i = true
⊢ c ^^^ a < b

Tactic:
;

Goal state after:
case inr.inl
a b c : ℕ
v : ℕ := ⋯
h✝ : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
i : ℕ
hi : v.testBit i = true
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
h : b.testBit i = true
⊢ c ^^^ a < b
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f : ℝ → ℝ
p : ℤ
hf : GrowsPolynomially f
hf_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
⊢ GrowsPolynomially fun x ↦ f x ^ p

Tactic:
← rpow_intCast

Goal state after:
f : ℝ → ℝ
p : ℤ
hf : GrowsPolynomially f
hf_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
⊢ GrowsPolynomially fun x ↦ f x ^ ↑p
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: case inr.inr
a b c : ℕ
v : ℕ := ⋯
h✝ : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
i : ℕ
hi : v.testBit i = true
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
h : c.testBit i = true
⊢ c ^^^ a < b ∨ a ^^^ b < c

Tactic:
;

Goal state after:
case inr.inr
a b c : ℕ
v : ℕ := ⋯
h✝ : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
i : ℕ
hi : v.testBit i = true
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
h : c.testBit i = true
⊢ c ^^^ a < b ∨ a ^^^ b < c
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: case inr.inr
a b c : ℕ
v : ℕ := ⋯
h✝ : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
i : ℕ
hi : v.testBit i = true
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
h : c.testBit i = true
⊢ a ^^^ b < c

Tactic:
;

Goal state after:
case inr.inr
a b c : ℕ
v : ℕ := ⋯
h✝ : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
i : ℕ
hi : v.testBit i = true
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
h : c.testBit i = true
⊢ a ^^^ b < c
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: case hxy
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb₀ : 0 < b
h_tendsto : Tendsto (fun x ↦ 1 / 2 * log x) atTop atTop
x : ℝ
hx_pos : 1 < x
hx : ∀ (y : ℝ), b * id x ≤ y → -log b < 1 / 2 * log y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ b * x ≤ u

Tactic:
;

Goal state after:
case hxy
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb₀ : 0 < b
h_tendsto : Tendsto (fun x ↦ 1 / 2 * log x) atTop atTop
x : ℝ
hx_pos : 1 < x
hx : ∀ (y : ℝ), b * id x ≤ y → -log b < 1 / 2 * log y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ b * x ≤ u
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: c : Code
n✝ x a m n : ℕ
hl : m ≤ n
⊢ a ∈ evaln m c n✝ → a ∈ evaln n c n✝

Tactic:
;

Goal state after:
c : Code
n✝ x a m n : ℕ
hl : m ≤ n
⊢ a ∈ evaln m c n✝ → a ∈ evaln n c n✝
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: c : Code
n✝ x a m n : ℕ
hl : m ≤ n
⊢ a ∈ evaln m c n✝ → a ∈ evaln n c n✝

Tactic:
apply evaln_mono hl

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: f : ℕ →. ℕ
hf : Partrec f
⊢ ∃ a, (fun c ↦ ⟨c.eval, ⋯⟩) a = ⟨f, hf⟩

Tactic:
;

Goal state after:
f : ℕ →. ℕ
hf : Partrec f
⊢ ∃ a, (fun c ↦ ⟨c.eval, ⋯⟩) a = ⟨f, hf⟩
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : AddMonoidWithOne α
p : PosNum
⊢ ↑(↑p + ↑p) = ↑p + ↑p

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : AddMonoidWithOne α
p : PosNum
⊢ ↑(↑p + ↑p) = ↑p + ↑p
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : AddMonoidWithOne α
p : PosNum
⊢ ↑(↑p + ↑p + 1) = ↑p + ↑p + 1

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : AddMonoidWithOne α
p : PosNum
⊢ ↑(↑p + ↑p + 1) = ↑p + ↑p + 1
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: a b : PosNum
⊢ ↑a + ↑b + (↑a + ↑b) + 1 = ↑a + ↑a + 1 + (↑b + ↑b)

Tactic:
simp [add_comm, add_left_comm]

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

Goal state before:
pp: a b : PosNum
⊢ ↑a + ↑b + 1 + (↑a + ↑b + 1) = ↑a + ↑a + 1 + (↑b + ↑b + 1)

Tactic:
;

Goal state after:
a b : PosNum
⊢ ↑a + ↑b + 1 + (↑a + ↑b + 1) = ↑a + ↑a + 1 + (↑b + ↑b + 1)
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: case left
x y n m : ℕ
hx : x < 2 ^ n
hy : y < 2 ^ m
⊢ y <<< n < 2 ^ (m + n)

Tactic:
;

Goal state after:
case left
x y n m : ℕ
hx : x < 2 ^ n
hy : y < 2 ^ m
⊢ y <<< n < 2 ^ (m + n)
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
S : Set σ
⊢ (∃ s ∈ M.accept, s ∈ S) ↔ ∃ s ∈ S, s ∈ M.accept

Tactic:
;

Goal state after:
α : Type u
σ : Type v
M : NFA α σ
S : Set σ
⊢ (∃ s ∈ M.accept, s ∈ S) ↔ ∃ s ∈ S, s ∈ M.accept
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: m n : PosNum
h : ↑m < ↑n
⊢ ↑m + ↑m + 1 + 1 ≤ ↑n + ↑n

Tactic:
;

Goal state after:
m n : PosNum
h : ↑m < ↑n
⊢ ↑m + ↑m + 1 + 1 ≤ ↑n + ↑n
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: m n : PosNum
h : ↑m < ↑n
⊢ ↑m + 1 + (↑m + 1) ≤ ↑n + ↑n

Tactic:
;

Goal state after:
m n : PosNum
h : ↑m < ↑n
⊢ ↑m + 1 + (↑m + 1) ≤ ↑n + ↑n
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: case hbc
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
⊢ b ≤ 1

Tactic:
;

Goal state after:
case hbc
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
⊢ b ≤ 1
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
S : Set σ
a : α
x : List α
⊢ x ∈ (fun x ↦ a :: x) ⁻¹' M.acceptsFrom S ↔ x ∈ M.acceptsFrom (M.stepSet S a)

Tactic:
;

Goal state after:
α : Type u
σ : Type v
M : NFA α σ
S : Set σ
a : α
x : List α
⊢ x ∈ (fun x ↦ a :: x) ⁻¹' M.acceptsFrom S ↔ x ∈ M.acceptsFrom (M.stepSet S a)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case one.one
⊢ (one.cmp one).swap = one.cmp one

Tactic:
unfold cmp

Goal state after:
case one.one
⊢ Ordering.eq.swap = Ordering.eq
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
S : Set σ
x y : List α
⊢ y ∈ (fun x_1 ↦ x ++ x_1) ⁻¹' M.acceptsFrom S ↔ y ∈ M.acceptsFrom (M.evalFrom S x)

Tactic:
;

Goal state after:
α : Type u
σ : Type v
M : NFA α σ
S : Set σ
x y : List α
⊢ y ∈ (fun x_1 ↦ x ++ x_1) ⁻¹' M.acceptsFrom S ↔ y ∈ M.acceptsFrom (M.evalFrom S x)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case one.bit1
n : PosNum
⊢ (one.cmp n.bit1).swap = n.bit1.cmp one

Tactic:
unfold cmp

Goal state after:
case one.bit1
n : PosNum
⊢ Ordering.lt.swap = Ordering.gt
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case one.bit0
n : PosNum
⊢ (one.cmp n.bit0).swap = n.bit0.cmp one

Tactic:
unfold cmp

Goal state after:
case one.bit0
n : PosNum
⊢ Ordering.lt.swap = Ordering.gt
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case bit1.one
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
⊢ (m.bit1.cmp one).swap = one.cmp m.bit1

Tactic:
unfold cmp

Goal state after:
case bit1.one
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
⊢ Ordering.gt.swap = Ordering.lt
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case bit1.bit1
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (m.bit1.cmp n.bit1).swap = n.bit1.cmp m.bit1

Tactic:
unfold cmp

Goal state after:
case bit1.bit1
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (m.cmp n).swap = n.cmp m
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case bit1.bit0
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (m.bit1.cmp n.bit0).swap = n.bit0.cmp m.bit1

Tactic:
unfold cmp

Goal state after:
case bit1.bit0
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (Ordering.casesOn (m.cmp n) Ordering.lt Ordering.gt Ordering.gt).swap =
    Ordering.casesOn (n.cmp m) Ordering.lt Ordering.lt Ordering.gt
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case bit0.one
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
⊢ (m.bit0.cmp one).swap = one.cmp m.bit0

Tactic:
unfold cmp

Goal state after:
case bit0.one
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
⊢ Ordering.gt.swap = Ordering.lt
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case bit0.bit1
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (m.bit0.cmp n.bit1).swap = n.bit1.cmp m.bit0

Tactic:
unfold cmp

Goal state after:
case bit0.bit1
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (Ordering.casesOn (m.cmp n) Ordering.lt Ordering.lt Ordering.gt).swap =
    Ordering.casesOn (n.cmp m) Ordering.lt Ordering.gt Ordering.gt
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case bit0.bit0
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (m.bit0.cmp n.bit0).swap = n.bit0.cmp m.bit0

Tactic:
unfold cmp

Goal state after:
case bit0.bit0
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (m.cmp n).swap = n.cmp m
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
S T : Set σ
⊢ M.acceptsFrom (S ∪ T) = M.acceptsFrom S ∪ M.acceptsFrom T

Tactic:
;

Goal state after:
α : Type u
σ : Type v
M : NFA α σ
S T : Set σ
⊢ M.acceptsFrom (S ∪ T) = M.acceptsFrom S ∪ M.acceptsFrom T
Module: Mathlib.Computability.NFA

Goal state before:
pp: case mp.inl
α : Type u
σ : Type v
M : NFA α σ
S T : Set σ
x : List α
s : σ
hs : s ∈ M.accept
h : s ∈ M.evalFrom S x
⊢ x ∈ M.acceptsFrom S

Tactic:
;

Goal state after:
case mp.inl
α : Type u
σ : Type v
M : NFA α σ
S T : Set σ
x : List α
s : σ
hs : s ∈ M.accept
h : s ∈ M.evalFrom S x
⊢ x ∈ M.acceptsFrom S
Module: Mathlib.Computability.NFA

Goal state before:
pp: case mp.inr
α : Type u
σ : Type v
M : NFA α σ
S T : Set σ
x : List α
s : σ
hs : s ∈ M.accept
h : s ∈ M.evalFrom T x
⊢ x ∈ M.acceptsFrom T

Tactic:
;

Goal state after:
case mp.inr
α : Type u
σ : Type v
M : NFA α σ
S T : Set σ
x : List α
s : σ
hs : s ∈ M.accept
h : s ∈ M.evalFrom T x
⊢ x ∈ M.acceptsFrom T
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: a b : PosNum
this : Ordering.casesOn (a.cmp b) (↑a < ↑b) (a = b) (↑b < ↑a)
⊢ Ordering.rec (↑a + ↑a < ↑b + ↑b) (a.bit0 = b.bit0) (↑b + ↑b < ↑a + ↑a) (a.cmp b)

Tactic:
;

Goal state after:
a b : PosNum
this : Ordering.casesOn (a.cmp b) (↑a < ↑b) (a = b) (↑b < ↑a)
⊢ Ordering.rec (↑a + ↑a < ↑b + ↑b) (a.bit0 = b.bit0) (↑b + ↑b < ↑a + ↑a) (a.cmp b)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: a b : PosNum
⊢ Ordering.casesOn (a.cmp b) (↑a < ↑b) (a = b) (↑b < ↑a) →
    Ordering.rec (↑a + ↑a < ↑b + ↑b) (a.bit0 = b.bit0) (↑b + ↑b < ↑a + ↑a) (a.cmp b)

Tactic:
;

Goal state after:
a b : PosNum
⊢ Ordering.casesOn (a.cmp b) (↑a < ↑b) (a = b) (↑b < ↑a) →
    Ordering.rec (↑a + ↑a < ↑b + ↑b) (a.bit0 = b.bit0) (↑b + ↑b < ↑a + ↑a) (a.cmp b)