mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
p : HolorIndex (d :: ds) → Prop
t : HolorIndex (d :: ds)
i : ℕ
is : List ℕ
h : ↑t = i :: is
⊢ Forall₂ (fun x1 x2 ↦ x1 < x2) (↑t) (d :: ds)

Tactic:
]

Goal state after:
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
p : HolorIndex (d :: ds) → Prop
t : HolorIndex (d :: ds)
i : ℕ
is : List ℕ
h : ↑t = i :: is
⊢ Forall₂ (fun x1 x2 ↦ x1 < x2) (↑t) (d :: ds)
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
d : ℕ
ds : List ℕ
x y : Holor α (d :: ds)
h : x.slice = y.slice
t : HolorIndex (d :: ds)
i : ℕ
is : List ℕ
hiis : ↑t = i :: is
⊢ Forall₂ (fun x1 x2 ↦ x1 < x2) (↑t) (d :: ds)

Tactic:
]

Goal state after:
α : Type
d : ℕ
ds : List ℕ
x y : Holor α (d :: ds)
h : x.slice = y.slice
t : HolorIndex (d :: ds)
i : ℕ
is : List ℕ
hiis : ↑t = i :: is
⊢ Forall₂ (fun x1 x2 ↦ x1 < x2) (↑t) (d :: ds)
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
d : ℕ
ds : List ℕ
x y : Holor α (d :: ds)
h : x.slice = y.slice
t : HolorIndex (d :: ds)
i : ℕ
is : List ℕ
hiis : ↑t = i :: is
hiisdds : Forall₂ (fun x1 x2 ↦ x1 < x2) (i :: is) (d :: ds)
hid : i < d
hisds : Forall₂ (fun x1 x2 ↦ x1 < x2) is ds
⊢ y.slice i hid ⟨is, hisds⟩ = y.slice i hid ⟨is, hisds⟩

Tactic:
]

Goal state after:
Module: Mathlib.Data.Holor

Goal state before:
pp: case refine_2
α : Type
d : ℕ
ds : List ℕ
inst✝ : AddCommMonoid α
β : Type
i : ℕ
hid : i < d
s : Finset β
f : β → Holor α (d :: ds)
this : DecidableEq β := Classical.decEq β
a✝ : β
s✝ : Finset β
h_not_in : a✝ ∉ s✝
ih : ∑ x ∈ s✝, (f x).slice i hid = (∑ x ∈ s✝, f x).slice i hid
⊢ (f a✝ + ∑ x ∈ s✝, f x).slice i hid = (f a✝ + ∑ x ∈ s✝, f x).slice i hid

Tactic:
]

Goal state after:
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
d : ℕ
ds : List ℕ
inst✝ : Semiring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
⊢ ∑ x_1 ∈ (Finset.range d).attach, (unitVec d ↑x_1 ⊗ x.slice ↑x_1 ⋯).slice i hid = x.slice i hid

Tactic:
]

Goal state after:
α : Type
d : ℕ
ds : List ℕ
inst✝ : Semiring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
⊢ ∑ x_1 ∈ (Finset.range d).attach, (unitVec d ↑x_1 ⊗ x.slice ↑x_1 ⋯).slice i hid = x.slice i hid
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
d : ℕ
ds : List ℕ
inst✝ : Semiring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
⊢ (if i = ↑⟨i, ⋯⟩ then x.slice ↑⟨i, ⋯⟩ ⋯ else 0) = x.slice i hid

pp: case h₀
α : Type
d : ℕ
ds : List ℕ
inst✝ : Semiring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
⊢ ∀ b ∈ (Finset.range d).attach, b ≠ ⟨i, ⋯⟩ → (if i = ↑b then x.slice ↑b ⋯ else 0) = 0

pp: case h₁
α : Type
d : ℕ
ds : List ℕ
inst✝ : Semiring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
⊢ ⟨i, ⋯⟩ ∉ (Finset.range d).attach → (if i = ↑⟨i, ⋯⟩ then x.slice ↑⟨i, ⋯⟩ ⋯ else 0) = 0

Tactic:
]

Goal state after:
α : Type
d : ℕ
ds : List ℕ
inst✝ : Semiring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
⊢ (if i = ↑⟨i, ⋯⟩ then x.slice ↑⟨i, ⋯⟩ ⋯ else 0) = x.slice i hid

case h₀
α : Type
d : ℕ
ds : List ℕ
inst✝ : Semiring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
⊢ ∀ b ∈ (Finset.range d).attach, b ≠ ⟨i, ⋯⟩ → (if i = ↑b then x.slice ↑b ⋯ else 0) = 0

case h₁
α : Type
d : ℕ
ds : List ℕ
inst✝ : Semiring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
⊢ ⟨i, ⋯⟩ ∉ (Finset.range d).attach → (if i = ↑⟨i, ⋯⟩ then x.slice ↑⟨i, ⋯⟩ ⋯ else 0) = 0
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
inst✝¹ : Mul α
inst✝ : AddMonoid α
x : Holor α []
h : CPRankMax 1 x
⊢ CPRankMax 1 x

Tactic:
]

Goal state after:
α : Type
inst✝¹ : Mul α
inst✝ : AddMonoid α
x : Holor α []
h : CPRankMax 1 x
⊢ CPRankMax 1 x
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
ds : List ℕ
inst✝¹ : Mul α
inst✝ : AddMonoid α
x : Holor α ds
h : x.CPRankMax1
h' : CPRankMax 1 x
⊢ CPRankMax 1 x

Tactic:
]

Goal state after:
α : Type
ds : List ℕ
inst✝¹ : Mul α
inst✝ : AddMonoid α
x : Holor α ds
h : x.CPRankMax1
h' : CPRankMax 1 x
⊢ CPRankMax 1 x
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: n : ℕ
⊢ ↑(bif (↑n).bodd then 1 else 0) + 2 * (↑n).div2 = ↑n

Tactic:
]

Goal state after:
n : ℕ
⊢ ↑(bif (↑n).bodd then 1 else 0) + 2 * (↑n).div2 = ↑n
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case false
n : ℕ
⊢ -[2 * n.div2+1] = -[2 * n.div2+1]

Tactic:
]

Goal state after:
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
d : ℕ
ds : List ℕ
inst✝ : NonUnitalNonAssocSemiring α
n : ℕ
x : Holor α [d]
y₁ y₂ : Holor α ds
hy₁ : y₁.CPRankMax1
hy₂ : CPRankMax n y₂
⊢ CPRankMax (n + 1) (x ⊗ y₁ + x ⊗ y₂)

Tactic:
]

Goal state after:
α : Type
d : ℕ
ds : List ℕ
inst✝ : NonUnitalNonAssocSemiring α
n : ℕ
x : Holor α [d]
y₁ y₂ : Holor α ds
hy₁ : y₁.CPRankMax1
hy₂ : CPRankMax n y₂
⊢ CPRankMax (n + 1) (x ⊗ y₁ + x ⊗ y₂)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case true
n : ℕ
⊢ 2 * -[n.div2+1] = -[2 * n.div2 + 1+1]

Tactic:
]

Goal state after:
case true
n : ℕ
⊢ 2 * -[n.div2+1] = -[2 * n.div2 + 1+1]
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
d : ℕ
ds : List ℕ
inst✝ : NonUnitalNonAssocSemiring α
n : ℕ
x : Holor α [d]
y₁ y₂ : Holor α ds
hy₁ : y₁.CPRankMax1
hy₂ : CPRankMax n y₂
⊢ CPRankMax (1 + n) (x ⊗ y₁ + x ⊗ y₂)

Tactic:
]

Goal state after:
α : Type
d : ℕ
ds : List ℕ
inst✝ : NonUnitalNonAssocSemiring α
n : ℕ
x : Holor α [d]
y₁ y₂ : Holor α ds
hy₁ : y₁.CPRankMax1
hy₂ : CPRankMax n y₂
⊢ CPRankMax (1 + n) (x ⊗ y₁ + x ⊗ y₂)
Module: Mathlib.Data.Int.Fib.Lemmas

Goal state before:
pp: x a : ℤ
⊢ fib (a + x) ^ 2 - fib x * fib (x + 2 * a) =
    (fib x * fib (a + 1) + fib (x - 1) * fib a) ^ 2 -
      fib x * (fib x * (fib (a + 1) ^ 2 + fib a ^ 2) + fib (x - 1) * (fib a * fib (a + 1) + fib (a - 1) * fib a))

Tactic:
]

Goal state after:
x a : ℤ
⊢ fib (a + x) ^ 2 - fib x * fib (x + 2 * a) =
    (fib x * fib (a + 1) + fib (x - 1) * fib a) ^ 2 -
      fib x * (fib x * (fib (a + 1) ^ 2 + fib a ^ 2) + fib (x - 1) * (fib a * fib (a + 1) + fib (a - 1) * fib a))
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: C : ℤ → Sort u
n : ℤ
h : (b : Bool) → (n : ℤ) → C (bit b n)
⊢ C (bit n.bodd n.div2)

Tactic:
]

Goal state after:
C : ℤ → Sort u
n : ℤ
h : (b : Bool) → (n : ℤ) → C (bit b n)
⊢ C (bit n.bodd n.div2)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: C : ℤ → Sort u
n : ℤ
h : (b : Bool) → (n : ℤ) → C (bit b n)
⊢ C n

Tactic:
rw [← bit_decomp n]
  apply h

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

Goal state before:
pp: b : Bool
n : ℕ
⊢ (2 * ↑n + bif b then 1 else 0) = ↑(2 * n + b.toNat)

Tactic:
]

Goal state after:
b : Bool
n : ℕ
⊢ (2 * ↑n + bif b then 1 else 0) = ↑(2 * n + b.toNat)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: b : Bool
n : ℕ
⊢ (2 * -[n+1] + bif b then 1 else 0) = -[2 * n + (!b).toNat+1]

Tactic:
]

Goal state after:
b : Bool
n : ℕ
⊢ (2 * -[n+1] + bif b then 1 else 0) = -[2 * n + (!b).toNat+1]
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: b : Bool
n : ℤ
⊢ (2 * n + bif b then 1 else 0).bodd = b

Tactic:
]

Goal state after:
b : Bool
n : ℤ
⊢ (2 * n + bif b then 1 else 0).bodd = b
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: b : Bool
n : ℕ
⊢ (↑(Nat.bit b n)).testBit 0 = b

Tactic:
]

Goal state after:
b : Bool
n : ℕ
⊢ (↑(Nat.bit b n)).testBit 0 = b
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: b : Bool
n : ℕ
⊢ -[Nat.bit (!b) n+1].testBit 0 = b

Tactic:
]

Goal state after:
b : Bool
n : ℕ
⊢ -[Nat.bit (!b) n+1].testBit 0 = b
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: b : Bool
n : ℕ
⊢ b = b

Tactic:
]

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

Goal state before:
pp: m : ℕ
b : Bool
n : ℕ
⊢ (↑(Nat.bit b n)).testBit m.succ = (↑n).testBit m

Tactic:
]

Goal state after:
m : ℕ
b : Bool
n : ℕ
⊢ (↑(Nat.bit b n)).testBit m.succ = (↑n).testBit m
Module: Mathlib.Data.Int.Order.Lemmas

Goal state before:
pp: a b : ℤ
⊢ a.natAbs = b.natAbs ↔ ↑a.natAbs = ↑b.natAbs

Tactic:
]

Goal state after:
a b : ℤ
⊢ a.natAbs = b.natAbs ↔ ↑a.natAbs = ↑b.natAbs
Module: Mathlib.Data.Int.Order.Lemmas

Goal state before:
pp: a b : ℤ
⊢ a.natAbs < b.natAbs ↔ ↑a.natAbs < ↑b.natAbs

Tactic:
]

Goal state after:
a b : ℤ
⊢ a.natAbs < b.natAbs ↔ ↑a.natAbs < ↑b.natAbs
Module: Mathlib.Data.Int.Order.Lemmas

Goal state before:
pp: a b : ℤ
⊢ a.natAbs ≤ b.natAbs ↔ ↑a.natAbs ≤ ↑b.natAbs

Tactic:
]

Goal state after:
a b : ℤ
⊢ a.natAbs ≤ b.natAbs ↔ ↑a.natAbs ≤ ↑b.natAbs
Module: Mathlib.Data.Int.Order.Lemmas

Goal state before:
pp: a b : ℤ
hn : 0 ≤ b
⊢ |a|.toNat * |a|.toNat ≤ b.toNat ↔ |a|.toNat * |a|.toNat ≤ b.toNat

Tactic:
]

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

Goal state before:
pp: a b : ℤ
⊢ a.natAbs = b.natAbs ↔ a * a = b * b

Tactic:
]

Goal state after:
a b : ℤ
⊢ a.natAbs = b.natAbs ↔ a * a = b * b
Module: Mathlib.Data.Int.Lemmas

Goal state before:
pp: a b : ℤ
⊢ a.natAbs < b.natAbs ↔ a * a < b * b

Tactic:
]

Goal state after:
a b : ℤ
⊢ a.natAbs < b.natAbs ↔ a * a < b * b
Module: Mathlib.Data.Int.Lemmas

Goal state before:
pp: a b : ℤ
⊢ a.natAbs ≤ b.natAbs ↔ a * a ≤ b * b

Tactic:
]

Goal state after:
a b : ℤ
⊢ a.natAbs ≤ b.natAbs ↔ a * a ≤ b * b
Module: Mathlib.Data.Int.Lemmas

Goal state before:
pp: a b : ℤ
ha : 0 ≤ a
hb : 0 ≤ b
⊢ a.natAbs = b.natAbs ↔ a.natAbs = b.natAbs

Tactic:
]

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

Goal state before:
pp: a b n : ℕ
a_le_n : a ≤ n
b_le_n : b ≤ n
⊢ |↑a - ↑b| ≤ ↑n

Tactic:
]

Goal state after:
a b n : ℕ
a_le_n : a ≤ n
b_le_n : b ≤ n
⊢ |↑a - ↑b| ≤ ↑n
Module: Mathlib.Data.Int.Lemmas

Goal state before:
pp: a b n : ℕ
a_lt_n : a < n
b_lt_n : b < n
⊢ |↑a - ↑b| < ↑n

Tactic:
]

Goal state after:
a b n : ℕ
a_lt_n : a < n
b_lt_n : b < n
⊢ |↑a - ↑b| < ↑n
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
ds : List ℕ
inst✝ : NonUnitalNonAssocSemiring α
β : Type u_1
n : ℕ
s✝ : Finset β
f : β → Holor α ds
this : DecidableEq β := Classical.decEq β
x : β
s : Finset β
h_x_notin_s : x ∉ s
ih : (∀ x ∈ s, CPRankMax n (f x)) → CPRankMax (s.card * n) (∑ x ∈ s, f x)
h_cprank : ∀ x_1 ∈ insert x s, CPRankMax n (f x_1)
⊢ CPRankMax (s.card * n + 1 * n) (f x + ∑ x ∈ s, f x)

Tactic:
]

Goal state after:
α : Type
ds : List ℕ
inst✝ : NonUnitalNonAssocSemiring α
β : Type u_1
n : ℕ
s✝ : Finset β
f : β → Holor α ds
this : DecidableEq β := Classical.decEq β
x : β
s : Finset β
h_x_notin_s : x ∉ s
ih : (∀ x ∈ s, CPRankMax n (f x)) → CPRankMax (s.card * n) (∑ x ∈ s, f x)
h_cprank : ∀ x_1 ∈ insert x s, CPRankMax n (f x_1)
⊢ CPRankMax (s.card * n + 1 * n) (f x + ∑ x ∈ s, f x)
Module: Mathlib.Data.Int.Lemmas

Goal state before:
pp: b : Bool
n : ℤ
⊢ n = n

pp: b : Bool
n : ℤ
⊢ (bif b then 1 else 0) / 2 = 0

pp: case H
b : Bool
n : ℤ
⊢ 2 ≠ 0

Tactic:
]

Goal state after:
b : Bool
n : ℤ
⊢ (bif b then 1 else 0) / 2 = 0

case H
b : Bool
n : ℤ
⊢ 2 ≠ 0
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case ofNat.negSucc
m n : ℕ
⊢ Nat.bitwise (fun y x ↦ !(x || !y)) n m = Nat.bitwise (fun a b ↦ a && !b) n m

Tactic:
]

Goal state after:
case ofNat.negSucc
m n : ℕ
⊢ Nat.bitwise (fun y x ↦ !(x || !y)) n m = Nat.bitwise (fun a b ↦ a && !b) n m
Module: Mathlib.Data.Int.Lemmas

Goal state before:
pp: case true
n : ℤ
⊢ ofNat 0 = 0

pp: case true
n : ℤ
⊢ 1 < 2

Tactic:
]

Goal state after:
case true
n : ℤ
⊢ ofNat 0 = 0

case true
n : ℤ
⊢ 1 < 2
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
inst✝ : Semiring α
d : ℕ
ds : List ℕ
x : Holor α (d :: ds)
h_summands : ∀ (i : ↥(Finset.range d)), CPRankMax ds.prod (unitVec d ↑i ⊗ x.slice ↑i ⋯)
h_dds_prod : (d :: ds).prod = (Finset.range d).card * ds.prod
this : CPRankMax ((Finset.range d).card * ds.prod) (∑ i ∈ (Finset.range d).attach, unitVec d ↑i ⊗ x.slice ↑i ⋯)
⊢ CPRankMax ((Finset.range d).card * ds.prod) (∑ i ∈ (Finset.range d).attach, unitVec d ↑i ⊗ x.slice ↑i ⋯)

Tactic:
]

Goal state after:
α : Type
inst✝ : Semiring α
d : ℕ
ds : List ℕ
x : Holor α (d :: ds)
h_summands : ∀ (i : ↥(Finset.range d)), CPRankMax ds.prod (unitVec d ↑i ⊗ x.slice ↑i ⋯)
h_dds_prod : (d :: ds).prod = (Finset.range d).card * ds.prod
this : CPRankMax ((Finset.range d).card * ds.prod) (∑ i ∈ (Finset.range d).attach, unitVec d ↑i ⊗ x.slice ↑i ⋯)
⊢ CPRankMax ((Finset.range d).card * ds.prod) (∑ i ∈ (Finset.range d).attach, unitVec d ↑i ⊗ x.slice ↑i ⋯)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case negSucc.ofNat
m n : ℕ
⊢ ↑(Nat.bitwise (fun y x ↦ !x && y) n m) = -[m+1].land (ofNat n)

Tactic:
]

Goal state after:
case negSucc.ofNat
m n : ℕ
⊢ ↑(Nat.bitwise (fun y x ↦ !x && y) n m) = -[m+1].land (ofNat n)
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
inst✝ : Semiring α
d : ℕ
ds : List ℕ
x : Holor α (d :: ds)
h_summands : ∀ (i : ↥(Finset.range d)), CPRankMax ds.prod (unitVec d ↑i ⊗ x.slice ↑i ⋯)
h_dds_prod : (d :: ds).prod = (Finset.range d).card * ds.prod
this : CPRankMax ((Finset.range d).attach.card * ds.prod) (∑ i ∈ (Finset.range d).attach, unitVec d ↑i ⊗ x.slice ↑i ⋯)
h_cprankMax_sum :
  CPRankMax ((Finset.range d).card * ds.prod) (∑ i ∈ (Finset.range d).attach, unitVec d ↑i ⊗ x.slice ↑i ⋯)
⊢ CPRankMax (d :: ds).prod (∑ i ∈ (Finset.range d).attach, unitVec d ↑i ⊗ x.slice ↑i ⋯)

Tactic:
]

Goal state after:
α : Type
inst✝ : Semiring α
d : ℕ
ds : List ℕ
x : Holor α (d :: ds)
h_summands : ∀ (i : ↥(Finset.range d)), CPRankMax ds.prod (unitVec d ↑i ⊗ x.slice ↑i ⋯)
h_dds_prod : (d :: ds).prod = (Finset.range d).card * ds.prod
this : CPRankMax ((Finset.range d).attach.card * ds.prod) (∑ i ∈ (Finset.range d).attach, unitVec d ↑i ⊗ x.slice ↑i ⋯)
h_cprankMax_sum :
  CPRankMax ((Finset.range d).card * ds.prod) (∑ i ∈ (Finset.range d).attach, unitVec d ↑i ⊗ x.slice ↑i ⋯)
⊢ CPRankMax (d :: ds).prod (∑ i ∈ (Finset.range d).attach, unitVec d ↑i ⊗ x.slice ↑i ⋯)
Module: Mathlib.Data.Int.Lemmas

Goal state before:
pp: case mpr.left
a b r q : ℤ
h : b ≠ 0
hz : 0 ≤ r
hb : r < |b|
⊢ 0 + q = q

Tactic:
]

Goal state after:
case mpr.left
a b r q : ℤ
h : b ≠ 0
hz : 0 ≤ r
hb : r < |b|
⊢ 0 + q = q
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
inst✝ : Semiring α
d : ℕ
ds : List ℕ
x : Holor α (d :: ds)
h_summands : ∀ (i : ↥(Finset.range d)), CPRankMax ds.prod (unitVec d ↑i ⊗ x.slice ↑i ⋯)
h_dds_prod : (d :: ds).prod = (Finset.range d).card * ds.prod
this : CPRankMax ((Finset.range d).attach.card * ds.prod) (∑ i ∈ (Finset.range d).attach, unitVec d ↑i ⊗ x.slice ↑i ⋯)
h_cprankMax_sum :
  CPRankMax ((Finset.range d).card * ds.prod) (∑ i ∈ (Finset.range d).attach, unitVec d ↑i ⊗ x.slice ↑i ⋯)
⊢ CPRankMax ((Finset.range d).card * ds.prod) (∑ i ∈ (Finset.range d).attach, unitVec d ↑i ⊗ x.slice ↑i ⋯)

Tactic:
]

Goal state after:
α : Type
inst✝ : Semiring α
d : ℕ
ds : List ℕ
x : Holor α (d :: ds)
h_summands : ∀ (i : ↥(Finset.range d)), CPRankMax ds.prod (unitVec d ↑i ⊗ x.slice ↑i ⋯)
h_dds_prod : (d :: ds).prod = (Finset.range d).card * ds.prod
this : CPRankMax ((Finset.range d).attach.card * ds.prod) (∑ i ∈ (Finset.range d).attach, unitVec d ↑i ⊗ x.slice ↑i ⋯)
h_cprankMax_sum :
  CPRankMax ((Finset.range d).card * ds.prod) (∑ i ∈ (Finset.range d).attach, unitVec d ↑i ⊗ x.slice ↑i ⋯)
⊢ CPRankMax ((Finset.range d).card * ds.prod) (∑ i ∈ (Finset.range d).attach, unitVec d ↑i ⊗ x.slice ↑i ⋯)
Module: Mathlib.Data.Int.Lemmas

Goal state before:
pp: case mpr.right
a b r q : ℤ
h : b ≠ 0
hz : 0 ≤ r
hb : r < |b|
⊢ r = r

Tactic:
]

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

Goal state before:
pp: case negSucc.negSucc
m n : ℕ
⊢ ↑(Nat.bitwise (fun y x ↦ !x && !!y) n m) = ↑(Nat.bitwise (fun a b ↦ a && !b) n m)

Tactic:
]

Goal state after:
case negSucc.negSucc
m n : ℕ
⊢ ↑(Nat.bitwise (fun y x ↦ !x && !!y) n m) = ↑(Nat.bitwise (fun a b ↦ a && !b) n m)
Module: Mathlib.Data.Int.NatPrime

Goal state before:
pp: p : ℕ
p_prime : Nat.Prime p
m n : ℤ
k l : ℕ
hpm : ↑(p ^ k) ∣ m
hpn : ↑(p ^ l) ∣ n
hpmn : ↑(p ^ (k + l + 1)) ∣ m * n
hpm' : p ^ k ∣ m.natAbs
hpn' : p ^ l ∣ n.natAbs
⊢ p ^ (k + l + 1) ∣ (m * n).natAbs

Tactic:
]

Goal state after:
p : ℕ
p_prime : Nat.Prime p
m n : ℤ
k l : ℕ
hpm : ↑(p ^ k) ∣ m
hpn : ↑(p ^ l) ∣ n
hpmn : ↑(p ^ (k + l + 1)) ∣ m * n
hpm' : p ^ k ∣ m.natAbs
hpn' : p ^ l ∣ n.natAbs
⊢ p ^ (k + l + 1) ∣ (m * n).natAbs
Module: Mathlib.Data.Int.NatPrime

Goal state before:
pp: p : ℕ
hp : Nat.Prime p
k : ℤ
h : ↑p ∣ k ^ 2
⊢ ↑p ∣ k ^ 2

Tactic:
]

Goal state after:
p : ℕ
hp : Nat.Prime p
k : ℤ
h : ↑p ∣ k ^ 2
⊢ ↑p ∣ k ^ 2
Module: Mathlib.Data.LawfulXor.Basic

Goal state before:
pp: α : Type u_1
inst✝² : XorOp α
inst✝¹ : Zero α
inst✝ : LawfulXor α
a : α
⊢ a = a

Tactic:
]

Goal state after:
Module: Mathlib.Data.LawfulXor.Basic

Goal state before:
pp: α : Type u_1
inst✝² : XorOp α
inst✝¹ : Zero α
inst✝ : LawfulXor α
a b : α
⊢ b = b

Tactic:
]

Goal state after:
Module: Mathlib.Data.LawfulXor.Basic

Goal state before:
pp: α : Type u_1
inst✝² : XorOp α
inst✝¹ : Zero α
inst✝ : LawfulXor α
a b : α
⊢ a = a

Tactic:
]

Goal state after:
Module: Mathlib.Data.LawfulXor.Basic

Goal state before:
pp: α : Type u_1
inst✝² : XorOp α
inst✝¹ : Zero α
inst✝ : LawfulXor α
a b : α
⊢ a = b ↔ a = b

Tactic:
]

Goal state after:
Module: Mathlib.Data.LawfulXor.Basic

Goal state before:
pp: α : Type u_1
inst✝² : XorOp α
inst✝¹ : Zero α
inst✝ : LawfulXor α
a b : α
⊢ b = 0 ↔ b = 0

Tactic:
]

Goal state after:
Module: Mathlib.Data.LawfulXor.Basic

Goal state before:
pp: α : Type u_1
inst✝² : XorOp α
inst✝¹ : Zero α
inst✝ : LawfulXor α
a : α
⊢ a = 0 ↔ a = 0

Tactic:
]

Goal state after:
Module: Mathlib.Data.LawfulXor.Basic

Goal state before:
pp: α : Type u_1
inst✝² : XorOp α
inst✝¹ : Zero α
inst✝ : LawfulXor α
a b : α
⊢ a = 0 ↔ a = 0

Tactic:
]

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

Goal state before:
pp: m n : ℤ
⊢ bitwise xor m n = m.xor n

Tactic:
rcases m with m | m <;> rcases n with n | n <;> try {rfl}
    <;> simp only [bitwise, natBitwise, Bool.not_false, Bool.bne_eq_xor,
      cond_false, cond_true, negSucc.injEq, Bool.false_xor,
      Bool.true_xor, Bool.not_true,
      Int.xor, HXor.hXor, XorOp.xor, Nat.xor]

Goal state after:
case ofNat.negSucc
m n : ℕ
⊢ Nat.bitwise (fun x y ↦ !(x ^^ !y)) m n = Nat.bitwise xor m n

case negSucc.ofNat
m n : ℕ
⊢ Nat.bitwise (fun x y ↦ !(!x ^^ y)) m n = Nat.bitwise xor m n

case negSucc.negSucc
m n : ℕ
⊢ ↑(Nat.bitwise (fun x y ↦ !x ^^ !y) m n) = ↑(Nat.bitwise xor m n)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: a : Bool
m : ℤ
b : Bool
n : ℤ
⊢ bit (a || b) (bitwise or m n) = bit (a || b) (bitwise or m n)

Tactic:
]

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

Goal state before:
pp: a : Bool
m : ℤ
b : Bool
n : ℤ
⊢ bit (a && b) (bitwise and m n) = bit (a && b) (bitwise and m n)

Tactic:
]

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

Goal state before:
pp: a : Bool
m : ℤ
b : Bool
n : ℤ
⊢ bit (a && !b) (bitwise (fun a b ↦ a && !b) m n) = bit (a && !b) (bitwise (fun a b ↦ a && !b) m n)

Tactic:
]

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

Goal state before:
pp: a : Bool
m : ℤ
b : Bool
n : ℤ
⊢ bit (a ^^ b) (bitwise xor m n) = bit (a ^^ b) (bitwise xor m n)

Tactic:
]

Goal state after:
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: a b r : ℤ
hr : 0 < r
⊢ max (⌈↑b / ↑r⌉ - ⌈↑a / ↑r⌉) 0 = max (⌈↑b / ↑r⌉ - ⌈↑a / ↑r⌉) 0

Tactic:
]

Goal state after:
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: a b r : ℤ
hr : 0 < r
⊢ max (⌊↑b / ↑r⌋ - ⌊↑a / ↑r⌋) 0 = max (⌊↑b / ↑r⌋ - ⌊↑a / ↑r⌋) 0

Tactic:
]

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

Goal state before:
pp: m n : ℤ
k : ℕ
⊢ (m.testBit k || n.testBit k) = (m.testBit k || n.testBit k)

Tactic:
]

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

Goal state before:
pp: m n : ℤ
k : ℕ
⊢ (m.testBit k && n.testBit k) = (m.testBit k && n.testBit k)

Tactic:
]

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

Goal state before:
pp: m n : ℤ
k : ℕ
⊢ (m.testBit k && !n.testBit k) = (m.testBit k && !n.testBit k)

Tactic:
]

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

Goal state before:
pp: m n : ℤ
k : ℕ
⊢ (m.testBit k ^^ n.testBit k) = (m.testBit k ^^ n.testBit k)

Tactic:
]

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

Goal state before:
pp: m n : ℤ
⊢ m <<< n = m <<< n

Tactic:
]

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

Goal state before:
pp: m n k : ℕ
⊢ ↑(m >>> n >>> k) = ↑(m >>> n >>> k)

Tactic:
]

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

Goal state before:
pp: m n k : ℕ
⊢ -[m >>> n >>> k+1] = -[m >>> n >>> k+1]

Tactic:
]

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

Goal state before:
pp: m : ℤ
n : ℕ
⊢ m <<< ↑n = m * ↑(2 ^ n)

Tactic:
]

Goal state after:
m : ℤ
n : ℕ
⊢ m <<< ↑n = m * ↑(2 ^ n)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: m n✝ k i n : ℕ
⊢ Nat.shiftLeft' true m i = Nat.shiftLeft' true m i

pp: case a
m n✝ k i n : ℕ
⊢ n ≤ n + i

Tactic:
]

Goal state after:
case a
m n✝ k i n : ℕ
⊢ n ≤ n + i
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: m n✝ k i n : ℕ
⊢ m >>> i.succ = m >>> (i + 1)

Tactic:
]

Goal state after:
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
⊢ ⌈(↑b - ↑v) / ↑r⌉ - ⌈(↑0 - ↑v) / ↑r⌉ = ⌈(↑b - ↑(v % r)) / ↑r⌉

Tactic:
]

Goal state after:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
⊢ ⌈(↑b - ↑v) / ↑r⌉ - ⌈(↑0 - ↑v) / ↑r⌉ = ⌈(↑b - ↑(v % r)) / ↑r⌉
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
⊢ ⌈(↑b - ↑(v % r)) / ↑r - ↑r * ↑(v / r) / ↑r⌉ - ⌈(↑0 - ↑(v % r)) / ↑r - ↑r * ↑(v / r) / ↑r⌉ = ?m.91

Tactic:
mul_div_cancel_left₀ _ hr'.ne',

Goal state after:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
⊢ ⌈(↑b - ↑(v % r)) / ↑r - ↑(v / r)⌉ - ⌈(↑0 - ↑(v % r)) / ↑r - ↑(v / r)⌉ = ?m.91
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
⊢ v % r < r ∧ -↑(v % r) ≤ 0

Tactic:
]

Goal state after:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
⊢ v % r < r ∧ -↑(v % r) ≤ 0
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
⊢ ⌈(↑b - ↑(v % r)) / ↑r⌉ = ↑(b / r) + ↑(if v % r < b % r then 1 else 0)

Tactic:
]

Goal state after:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
⊢ ⌈(↑b - ↑(v % r)) / ↑r⌉ = ↑(b / r) + ↑(if v % r < b % r then 1 else 0)
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
| ⌈↑r * ↑(b / r) / ↑r + (↑(b % r) - ↑(v % r)) / ↑r⌉

Tactic:
mul_div_cancel_left₀ _ hr'.ne',

Goal state after:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
| ⌈↑(b / r) + (↑(b % r) - ↑(v % r)) / ↑r⌉
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
⊢ ⌈(↑(b % r) - ↑(v % r)) / ↑r⌉ = ↑(if v % r < b % r then 1 else 0)

Tactic:
]

Goal state after:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
⊢ ⌈(↑(b % r) - ↑(v % r)) / ↑r⌉ = ↑(if v % r < b % r then 1 else 0)
Module: Mathlib.Data.List.TakeWhile

Goal state before:
pp: case cons
α : Type u_1
p : α → Bool
hd : α
tl : List α
⊢ (match p hd with
      | true => dropWhile p tl
      | false => hd :: tl) =
      hd :: tl ↔
    ∀ (hl : 0 < (hd :: tl).length), ¬p (hd :: tl)[0] = true

Tactic:
]

Goal state after:
case cons
α : Type u_1
p : α → Bool
hd : α
tl : List α
⊢ (match p hd with
      | true => dropWhile p tl
      | false => hd :: tl) =
      hd :: tl ↔
    ∀ (hl : 0 < (hd :: tl).length), ¬p (hd :: tl)[0] = true
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: case pos
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
h : v % r < b % r
⊢ v % r < b % r ∧ b % r ≤ r + v % r

Tactic:
]

Goal state after:
case pos
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
h : v % r < b % r
⊢ v % r < b % r ∧ b % r ≤ r + v % r
Module: Mathlib.Data.List.Fold

Goal state before:
pp: α : Type u_1
β : Type u_2
l : List α
v : β → α → β
a : α
b : β
hv : RightCommutative v
⊢ foldl v (v b a) l = v (foldl v b l) a

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
l : List α
v : β → α → β
a : α
b : β
hv : RightCommutative v
⊢ foldl v (v b a) l = v (foldl v b l) a
Module: Mathlib.Data.List.Fold

Goal state before:
pp: α : Type u_1
β : Type u_2
l : List α
f : α → β → β
a : α
b : β
hf : LeftCommutative f
⊢ f a (foldr f b l) = foldr f (f a b) l

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
l : List α
f : α → β → β
a : α
b : β
hf : LeftCommutative f
⊢ f a (foldr f b l) = foldr f (f a b) l