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

Goal state before:
pp: case inl
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝² : Semiring R
inst✝¹ : Fintype n₁
inst✝ : Fintype n₂
A₁ : Matrix n₁ n R
A₂ : Matrix n₂ n R
B₁₁ : Matrix m₁ n₁ R
B₁₂ : Matrix m₁ n₂ R
B₂₁ : Matrix m₂ n₁ R
B₂₂ : Matrix m₂ n₂ R
val✝ : m₁
j✝ : n
⊢ (fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ * A₁.fromRows A₂) (Sum.inl val✝) j✝ =
    (B₁₁ * A₁ + B₁₂ * A₂).fromRows (B₂₁ * A₁ + B₂₂ * A₂) (Sum.inl val✝) j✝

pp: case inr
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝² : Semiring R
inst✝¹ : Fintype n₁
inst✝ : Fintype n₂
A₁ : Matrix n₁ n R
A₂ : Matrix n₂ n R
B₁₁ : Matrix m₁ n₁ R
B₁₂ : Matrix m₁ n₂ R
B₂₁ : Matrix m₂ n₁ R
B₂₂ : Matrix m₂ n₂ R
val✝ : m₂
j✝ : n
⊢ (fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ * A₁.fromRows A₂) (Sum.inr val✝) j✝ =
    (B₁₁ * A₁ + B₁₂ * A₂).fromRows (B₂₁ * A₁ + B₂₂ * A₂) (Sum.inr val✝) j✝

Tactic:
<;>

Goal state after:
case inl
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝² : Semiring R
inst✝¹ : Fintype n₁
inst✝ : Fintype n₂
A₁ : Matrix n₁ n R
A₂ : Matrix n₂ n R
B₁₁ : Matrix m₁ n₁ R
B₁₂ : Matrix m₁ n₂ R
B₂₁ : Matrix m₂ n₁ R
B₂₂ : Matrix m₂ n₂ R
val✝ : m₁
j✝ : n
⊢ (fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ * A₁.fromRows A₂) (Sum.inl val✝) j✝ =
    (B₁₁ * A₁ + B₁₂ * A₂).fromRows (B₂₁ * A₁ + B₂₂ * A₂) (Sum.inl val✝) j✝

case inr
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝² : Semiring R
inst✝¹ : Fintype n₁
inst✝ : Fintype n₂
A₁ : Matrix n₁ n R
A₂ : Matrix n₂ n R
B₁₁ : Matrix m₁ n₁ R
B₁₂ : Matrix m₁ n₂ R
B₂₁ : Matrix m₂ n₁ R
B₂₂ : Matrix m₂ n₂ R
val✝ : m₂
j✝ : n
⊢ (fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ * A₁.fromRows A₂) (Sum.inr val✝) j✝ =
    (B₁₁ * A₁ + B₁₂ * A₂).fromRows (B₂₁ * A₁ + B₂₂ * A₂) (Sum.inr val✝) j✝
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: case inl
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
inst✝ : Star R
A₁ : Matrix m n₁ R
A₂ : Matrix m n₂ R
val✝ : n₁
j✝ : m
⊢ (A₁.fromCols A₂)ᴴ (Sum.inl val✝) j✝ = A₁ᴴ.fromRows A₂ᴴ (Sum.inl val✝) j✝

pp: case inr
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
inst✝ : Star R
A₁ : Matrix m n₁ R
A₂ : Matrix m n₂ R
val✝ : n₂
j✝ : m
⊢ (A₁.fromCols A₂)ᴴ (Sum.inr val✝) j✝ = A₁ᴴ.fromRows A₂ᴴ (Sum.inr val✝) j✝

Tactic:
<;>

Goal state after:
case inl
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
inst✝ : Star R
A₁ : Matrix m n₁ R
A₂ : Matrix m n₂ R
val✝ : n₁
j✝ : m
⊢ (A₁.fromCols A₂)ᴴ (Sum.inl val✝) j✝ = A₁ᴴ.fromRows A₂ᴴ (Sum.inl val✝) j✝

case inr
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
inst✝ : Star R
A₁ : Matrix m n₁ R
A₂ : Matrix m n₂ R
val✝ : n₂
j✝ : m
⊢ (A₁.fromCols A₂)ᴴ (Sum.inr val✝) j✝ = A₁ᴴ.fromRows A₂ᴴ (Sum.inr val✝) j✝
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: case inl
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst✝ : Star R
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
i✝ : n
val✝ : m₁
⊢ (A₁.fromRows A₂)ᴴ i✝ (Sum.inl val✝) = A₁ᴴ.fromCols A₂ᴴ i✝ (Sum.inl val✝)

pp: case inr
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst✝ : Star R
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
i✝ : n
val✝ : m₂
⊢ (A₁.fromRows A₂)ᴴ i✝ (Sum.inr val✝) = A₁ᴴ.fromCols A₂ᴴ i✝ (Sum.inr val✝)

Tactic:
<;>

Goal state after:
case inl
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst✝ : Star R
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
i✝ : n
val✝ : m₁
⊢ (A₁.fromRows A₂)ᴴ i✝ (Sum.inl val✝) = A₁ᴴ.fromCols A₂ᴴ i✝ (Sum.inl val✝)

case inr
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst✝ : Star R
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
i✝ : n
val✝ : m₂
⊢ (A₁.fromRows A₂)ᴴ i✝ (Sum.inr val✝) = A₁ᴴ.fromCols A₂ᴴ i✝ (Sum.inr val✝)
Module: Mathlib.Data.NNRat.Floor

Goal state before:
pp: a : ℚ≥0
n : ℕ
h : 0 ≤ a
⊢ ↑n ≤ ↑a ↔ ↑↑n ≤ ↑a

pp: a : ℚ≥0
n : ℕ
h : 0 ≤ a
⊢ 0 ≤ ↑a

Tactic:
<;>

Goal state after:
a : ℚ≥0
n : ℕ
h : 0 ≤ a
⊢ ↑n ≤ ↑a ↔ ↑↑n ≤ ↑a

a : ℚ≥0
n : ℕ
h : 0 ≤ a
⊢ 0 ≤ ↑a
Module: Mathlib.Data.NNRat.Floor

Goal state before:
pp: case inr.refine_1
K : Type u_1
inst✝³ : Semifield K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorSemiring K
x : ℚ≥0
hx : x ≠ 0
⊢ ⌈x⌉₊ ≠ 0

pp: case inr.refine_2
K : Type u_1
inst✝³ : Semifield K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorSemiring K
x : ℚ≥0
hx : x ≠ 0
⊢ ⌈x⌉₊ ≠ 0

Tactic:
<;>

Goal state after:
case inr.refine_1
K : Type u_1
inst✝³ : Semifield K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorSemiring K
x : ℚ≥0
hx : x ≠ 0
⊢ ⌈x⌉₊ ≠ 0

case inr.refine_2
K : Type u_1
inst✝³ : Semifield K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorSemiring K
x : ℚ≥0
hx : x ≠ 0
⊢ ⌈x⌉₊ ≠ 0
Module: Mathlib.Data.NNRat.Floor

Goal state before:
pp: case inr
K : Type u_1
inst✝³ : Semifield K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorSemiring K
x : ℚ≥0
hx : x ≠ 0
⊢ ⌈↑x⌉₊ = ⌈x⌉₊

Tactic:
· refine (Nat.ceil_eq_iff ?_).2 (mod_cast (Nat.ceil_eq_iff ?_).1 (Eq.refl ⌈x⌉₊)) <;> simpa

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

Goal state before:
pp: case e'_2
q₁ q₂ : ℚ≥0
⊢ ↑(q₁ * q₂).num = (↑q₁ * ↑q₂).num

pp: case e'_3.e'_5.e'_5
q₁ q₂ : ℚ≥0
⊢ ↑q₁.num = (↑q₁).num

pp: case e'_3.e'_5.e'_6
q₁ q₂ : ℚ≥0
⊢ ↑q₂.num = (↑q₂).num

pp: case e'_3.e'_6.e'_1
q₁ q₂ : ℚ≥0
⊢ q₁.num * q₂.num = ((↑q₁).num * (↑q₂).num).natAbs

Tactic:
<;>

Goal state after:
case e'_2
q₁ q₂ : ℚ≥0
⊢ ↑(q₁ * q₂).num = (↑q₁ * ↑q₂).num

case e'_3.e'_5.e'_5
q₁ q₂ : ℚ≥0
⊢ ↑q₁.num = (↑q₁).num

case e'_3.e'_5.e'_6
q₁ q₂ : ℚ≥0
⊢ ↑q₂.num = (↑q₂).num

case e'_3.e'_6.e'_1
q₁ q₂ : ℚ≥0
⊢ q₁.num * q₂.num = ((↑q₁).num * (↑q₂).num).natAbs
Module: Mathlib.Data.NNRat.Lemmas

Goal state before:
pp: case e'_2.e'_5
q₁ q₂ : ℚ≥0
⊢ ↑q₁.num = (↑q₁).num

pp: case e'_2.e'_6
q₁ q₂ : ℚ≥0
⊢ ↑q₂.num = (↑q₂).num

pp: case e'_3.e'_5
q₁ q₂ : ℚ≥0
⊢ ↑(q₁ * q₂).num = (↑q₁ * ↑q₂).num

pp: case e'_3.e'_6.e'_3.e'_1
q₁ q₂ : ℚ≥0
⊢ q₁.num * q₂.num = ((↑q₁).num * (↑q₂).num).natAbs

Tactic:
<;>

Goal state after:
case e'_2.e'_5
q₁ q₂ : ℚ≥0
⊢ ↑q₁.num = (↑q₁).num

case e'_2.e'_6
q₁ q₂ : ℚ≥0
⊢ ↑q₂.num = (↑q₂).num

case e'_3.e'_5
q₁ q₂ : ℚ≥0
⊢ ↑(q₁ * q₂).num = (↑q₁ * ↑q₂).num

case e'_3.e'_6.e'_3.e'_1
q₁ q₂ : ℚ≥0
⊢ q₁.num * q₂.num = ((↑q₁).num * (↑q₂).num).natAbs
Module: Mathlib.Data.Nat.ChineseRemainder

Goal state before:
pp: case cons.mp.zero
a b m : ℕ
l : List ℕ
ih : List.Pairwise Coprime l → (a ≡ b [MOD l.prod] ↔ ∀ (i : Fin l.length), a ≡ b [MOD l.get i])
co : List.Pairwise Coprime (m :: l)
this : m.Coprime l.prod
h0 : a ≡ b [MOD m]
hs : ∀ (i : Fin l.length), a ≡ b [MOD l.get i]
⊢ a ≡ b [MOD (m :: l).get 0]

pp: case cons.mp.succ
a b m : ℕ
l : List ℕ
ih : List.Pairwise Coprime l → (a ≡ b [MOD l.prod] ↔ ∀ (i : Fin l.length), a ≡ b [MOD l.get i])
co : List.Pairwise Coprime (m :: l)
this : m.Coprime l.prod
h0 : a ≡ b [MOD m]
hs : ∀ (i : Fin l.length), a ≡ b [MOD l.get i]
i✝ : Fin l.length
⊢ a ≡ b [MOD (m :: l).get i✝.succ]

Tactic:
<;>

Goal state after:
case cons.mp.zero
a b m : ℕ
l : List ℕ
ih : List.Pairwise Coprime l → (a ≡ b [MOD l.prod] ↔ ∀ (i : Fin l.length), a ≡ b [MOD l.get i])
co : List.Pairwise Coprime (m :: l)
this : m.Coprime l.prod
h0 : a ≡ b [MOD m]
hs : ∀ (i : Fin l.length), a ≡ b [MOD l.get i]
⊢ a ≡ b [MOD (m :: l).get 0]

case cons.mp.succ
a b m : ℕ
l : List ℕ
ih : List.Pairwise Coprime l → (a ≡ b [MOD l.prod] ↔ ∀ (i : Fin l.length), a ≡ b [MOD l.get i])
co : List.Pairwise Coprime (m :: l)
this : m.Coprime l.prod
h0 : a ≡ b [MOD m]
hs : ∀ (i : Fin l.length), a ≡ b [MOD l.get i]
i✝ : Fin l.length
⊢ a ≡ b [MOD (m :: l).get i✝.succ]
Module: Mathlib.Data.Nat.Factorial.NatCast

Goal state before:
pp: case h
A : Type u_1
inst✝ : CommSemiring A
k : ℕ × ℕ
hm : IsUnit ↑(k.1 + k.2)!
⊢ IsUnit ↑k.1!

pp: case h
A : Type u_1
inst✝ : CommSemiring A
k : ℕ × ℕ
hm : IsUnit ↑(k.1 + k.2)!
⊢ IsUnit ↑k.2!

Tactic:
<;>

Goal state after:
case h
A : Type u_1
inst✝ : CommSemiring A
k : ℕ × ℕ
hm : IsUnit ↑(k.1 + k.2)!
⊢ IsUnit ↑k.1!

case h
A : Type u_1
inst✝ : CommSemiring A
k : ℕ × ℕ
hm : IsUnit ↑(k.1 + k.2)!
⊢ IsUnit ↑k.2!
Module: Mathlib.Data.Nat.Dist

Goal state before:
pp: case inl
i j : ℕ
h✝ : i ≤ j
⊢ i.dist j = max i j - min i j

pp: case inr
i j : ℕ
h✝ : j ≤ i
⊢ i.dist j = max i j - min i j

Tactic:
<;>

Goal state after:
case inl
i j : ℕ
h✝ : i ≤ j
⊢ i.dist j = max i j - min i j

case inr
i j : ℕ
h✝ : j ≤ i
⊢ i.dist j = max i j - min i j
Module: Mathlib.Data.Nat.Factorization.Root

Goal state before:
pp: case pos
a n : ℕ
h : n = 0 ∨ a = 0
⊢ 0 = 0

pp: case neg
a n : ℕ
h : ¬(n = 0 ∨ a = 0)
⊢ (a.factorization.prod fun p k ↦ p ^ (k / n)) = (a.factorization ⌊/⌋ n).prod fun x1 x2 ↦ x1 ^ x2

Tactic:
<;>

Goal state after:
case pos
a n : ℕ
h : n = 0 ∨ a = 0
⊢ 0 = 0

case neg
a n : ℕ
h : ¬(n = 0 ∨ a = 0)
⊢ (a.factorization.prod fun p k ↦ p ^ (k / n)) = (a.factorization ⌊/⌋ n).prod fun x1 x2 ↦ x1 ^ x2
Module: Mathlib.Data.Nat.Factorization.Root

Goal state before:
pp: case pos
a : ℕ
h✝ : a = 0
⊢ 0 = a

pp: case neg
a : ℕ
h✝ : ¬a = 0
⊢ (a.factorization.prod fun p k ↦ p ^ k) = a

Tactic:
<;>

Goal state after:
case pos
a : ℕ
h✝ : a = 0
⊢ 0 = a

case neg
a : ℕ
h✝ : ¬a = 0
⊢ (a.factorization.prod fun p k ↦ p ^ k) = a
Module: Mathlib.Data.Nat.Factorization.Root

Goal state before:
pp: case pos
n : ℕ
hn : n ≠ 0
a : ℕ
h✝ : a = 0
⊢ 0 = a

pp: case neg
n : ℕ
hn : n ≠ 0
a : ℕ
h✝ : ¬a = 0
⊢ (a.factorization.prod fun x1 x2 ↦ x1 ^ x2) = a

Tactic:
<;>

Goal state after:
case pos
n : ℕ
hn : n ≠ 0
a : ℕ
h✝ : a = 0
⊢ 0 = a

case neg
n : ℕ
hn : n ≠ 0
a : ℕ
h✝ : ¬a = 0
⊢ (a.factorization.prod fun x1 x2 ↦ x1 ^ x2) = a
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: case mp
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
x₁ x₂ : ℕ
hx : (x₁, x₂) ∈ range (n % p + 1) ×ˢ range (n / p + 1)
⊢ k = (x₁, x₂).1 + p * (x₁, x₂).2 → k % p = x₁ ∧ k / p = x₂

pp: case mpr
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
x₁ x₂ : ℕ
hx : (x₁, x₂) ∈ range (n % p + 1) ×ˢ range (n / p + 1)
⊢ k % p = x₁ ∧ k / p = x₂ → k = (x₁, x₂).1 + p * (x₁, x₂).2

Tactic:
<;>

Goal state after:
case mp
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
x₁ x₂ : ℕ
hx : (x₁, x₂) ∈ range (n % p + 1) ×ˢ range (n / p + 1)
⊢ k = (x₁, x₂).1 + p * (x₁, x₂).2 → k % p = x₁ ∧ k / p = x₂

case mpr
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
x₁ x₂ : ℕ
hx : (x₁, x₂) ∈ range (n % p + 1) ×ˢ range (n / p + 1)
⊢ k % p = x₁ ∧ k / p = x₂ → k = (x₁, x₂).1 + p * (x₁, x₂).2
Module: Mathlib.Data.Nat.Factorization.Root

Goal state before:
pp: case pos.inl
a : ℕ
⊢ factorization 0 = a.factorization ⌊/⌋ 0

pp: case pos.inr
n : ℕ
⊢ factorization 0 = factorization 0 ⌊/⌋ n

Tactic:
<;>

Goal state after:
case pos.inl
a : ℕ
⊢ factorization 0 = a.factorization ⌊/⌋ 0

case pos.inr
n : ℕ
⊢ factorization 0 = factorization 0 ⌊/⌋ n
Module: Mathlib.Data.Nat.Factorization.Root

Goal state before:
pp: case pos
a n : ℕ
h : n = 0 ∨ a = 0
⊢ 0 = 0

pp: case neg
a n : ℕ
h : ¬(n = 0 ∨ a = 0)
⊢ (a.factorization.prod fun p k ↦ p ^ ((k + n - 1) / n)) = (a.factorization ⌈/⌉ n).prod fun x1 x2 ↦ x1 ^ x2

Tactic:
<;>

Goal state after:
case pos
a n : ℕ
h : n = 0 ∨ a = 0
⊢ 0 = 0

case neg
a n : ℕ
h : ¬(n = 0 ∨ a = 0)
⊢ (a.factorization.prod fun p k ↦ p ^ ((k + n - 1) / n)) = (a.factorization ⌈/⌉ n).prod fun x1 x2 ↦ x1 ^ x2
Module: Mathlib.Data.Nat.Factorization.Root

Goal state before:
pp: case pos.inl
a : ℕ
⊢ factorization 0 = a.factorization ⌈/⌉ 0

pp: case pos.inr
n : ℕ
⊢ factorization 0 = factorization 0 ⌈/⌉ n

Tactic:
<;>

Goal state after:
case pos.inl
a : ℕ
⊢ factorization 0 = a.factorization ⌈/⌉ 0

case pos.inr
n : ℕ
⊢ factorization 0 = factorization 0 ⌈/⌉ n
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: case neg.inl
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
h_iff : ∀ x ∈ range (n % p + 1) ×ˢ range (n / p + 1), k = x.1 + p * x.2 ↔ (k % p, k / p) = x
h✝ : n % p < (k % p, k / p).1
⊢ 0 = (Int.castRingHom (ZMod p)) ↑((n % p).choose (k % p) * (n / p).choose (k / p))

pp: case neg.inr
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
h_iff : ∀ x ∈ range (n % p + 1) ×ˢ range (n / p + 1), k = x.1 + p * x.2 ↔ (k % p, k / p) = x
h✝ : n / p + 1 ≤ (k % p, k / p).2
⊢ 0 = (Int.castRingHom (ZMod p)) ↑((n % p).choose (k % p) * (n / p).choose (k / p))

Tactic:
<;>

Goal state after:
case neg.inl
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
h_iff : ∀ x ∈ range (n % p + 1) ×ˢ range (n / p + 1), k = x.1 + p * x.2 ↔ (k % p, k / p) = x
h✝ : n % p < (k % p, k / p).1
⊢ 0 = (Int.castRingHom (ZMod p)) ↑((n % p).choose (k % p) * (n / p).choose (k / p))

case neg.inr
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
h_iff : ∀ x ∈ range (n % p + 1) ×ˢ range (n / p + 1), k = x.1 + p * x.2 ↔ (k % p, k / p) = x
h✝ : n / p + 1 ≤ (k % p, k / p).2
⊢ 0 = (Int.castRingHom (ZMod p)) ↑((n % p).choose (k % p) * (n / p).choose (k / p))
Module: Mathlib.Data.Nat.Fib.Zeckendorf

Goal state before:
pp: case case1
⊢ (map fib (zeckendorf 0)).sum = 0

pp: case case2
n✝ : ℕ
ih1✝ : (map fib (n✝ + 1 - fib (n✝ + 1).greatestFib).zeckendorf).sum = n✝ + 1 - fib (n✝ + 1).greatestFib
⊢ (map fib n✝.succ.zeckendorf).sum = n✝.succ

Tactic:
<;>

Goal state after:
case case1
⊢ (map fib (zeckendorf 0)).sum = 0

case case2
n✝ : ℕ
ih1✝ : (map fib (n✝ + 1 - fib (n✝ + 1).greatestFib).zeckendorf).sum = n✝ + 1 - fib (n✝ + 1).greatestFib
⊢ (map fib n✝.succ.zeckendorf).sum = n✝.succ
Module: Mathlib.Data.Ordering.Lemmas

Goal state before:
pp: case pos
c : Prop
inst✝ : Decidable c
a b : Ordering
h✝ : c
⊢ ((if c then a else b) = lt) = if c then a = lt else b = lt

pp: case neg
c : Prop
inst✝ : Decidable c
a b : Ordering
h✝ : ¬c
⊢ ((if c then a else b) = lt) = if c then a = lt else b = lt

Tactic:
<;>

Goal state after:
case pos
c : Prop
inst✝ : Decidable c
a b : Ordering
h✝ : c
⊢ ((if c then a else b) = lt) = if c then a = lt else b = lt

case neg
c : Prop
inst✝ : Decidable c
a b : Ordering
h✝ : ¬c
⊢ ((if c then a else b) = lt) = if c then a = lt else b = lt
Module: Mathlib.Data.Ordering.Lemmas

Goal state before:
pp: case pos
c : Prop
inst✝ : Decidable c
a b : Ordering
h✝ : c
⊢ ((if c then a else b) = eq) = if c then a = eq else b = eq

pp: case neg
c : Prop
inst✝ : Decidable c
a b : Ordering
h✝ : ¬c
⊢ ((if c then a else b) = eq) = if c then a = eq else b = eq

Tactic:
<;>

Goal state after:
case pos
c : Prop
inst✝ : Decidable c
a b : Ordering
h✝ : c
⊢ ((if c then a else b) = eq) = if c then a = eq else b = eq

case neg
c : Prop
inst✝ : Decidable c
a b : Ordering
h✝ : ¬c
⊢ ((if c then a else b) = eq) = if c then a = eq else b = eq
Module: Mathlib.Data.Ordering.Lemmas

Goal state before:
pp: case pos
c : Prop
inst✝ : Decidable c
a b : Ordering
h✝ : c
⊢ ((if c then a else b) = gt) = if c then a = gt else b = gt

pp: case neg
c : Prop
inst✝ : Decidable c
a b : Ordering
h✝ : ¬c
⊢ ((if c then a else b) = gt) = if c then a = gt else b = gt

Tactic:
<;>

Goal state after:
case pos
c : Prop
inst✝ : Decidable c
a b : Ordering
h✝ : c
⊢ ((if c then a else b) = gt) = if c then a = gt else b = gt

case neg
c : Prop
inst✝ : Decidable c
a b : Ordering
h✝ : ¬c
⊢ ((if c then a else b) = gt) = if c then a = gt else b = gt
Module: Mathlib.Data.Ordering.Lemmas

Goal state before:
pp: case lt
o₂ : Ordering
⊢ (lt.dthen fun x ↦ o₂) = lt.then o₂

pp: case eq
o₂ : Ordering
⊢ (eq.dthen fun x ↦ o₂) = eq.then o₂

pp: case gt
o₂ : Ordering
⊢ (gt.dthen fun x ↦ o₂) = gt.then o₂

Tactic:
<;>

Goal state after:
case lt
o₂ : Ordering
⊢ (lt.dthen fun x ↦ o₂) = lt.then o₂

case eq
o₂ : Ordering
⊢ (eq.dthen fun x ↦ o₂) = eq.then o₂

case gt
o₂ : Ordering
⊢ (gt.dthen fun x ↦ o₂) = gt.then o₂
Module: Mathlib.Data.Num.Prime

Goal state before:
pp: case zero
n k : PosNum
h : (↑n).sqrt < 0 + ↑k.bit1
⊢ ↑(n.minFacAux 0 k) = (↑n).minFacAux ↑k.bit1

pp: case succ
n : PosNum
n✝ : ℕ
a✝ : ∀ {k : PosNum}, (↑n).sqrt < n✝ + ↑k.bit1 → ↑(n.minFacAux n✝ k) = (↑n).minFacAux ↑k.bit1
k : PosNum
h : (↑n).sqrt < n✝ + 1 + ↑k.bit1
⊢ ↑(n.minFacAux (n✝ + 1) k) = (↑n).minFacAux ↑k.bit1

Tactic:
<;>

Goal state after:
case zero
n k : PosNum
h : (↑n).sqrt < 0 + ↑k.bit1
⊢ ↑(n.minFacAux 0 k) = (↑n).minFacAux ↑k.bit1

case succ
n : PosNum
n✝ : ℕ
a✝ : ∀ {k : PosNum}, (↑n).sqrt < n✝ + ↑k.bit1 → ↑(n.minFacAux n✝ k) = (↑n).minFacAux ↑k.bit1
k : PosNum
h : (↑n).sqrt < n✝ + 1 + ↑k.bit1
⊢ ↑(n.minFacAux (n✝ + 1) k) = (↑n).minFacAux ↑k.bit1
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: case x
p : ℕ → Prop
f : ℕ → ℕ
hmaps : Set.MapsTo f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset} (Set.ofPred p)
hmono : StrictMonoOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}
n : ℕ
ih : ∀ m < n, (∀ (hf : (Set.ofPred p).Finite), m < #hf.toFinset) → nth p m ≤ f m
hn : ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset
k : ℕ
hk : k < n
⊢ k ∈ {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}

pp: case x
p : ℕ → Prop
f : ℕ → ℕ
hmaps : Set.MapsTo f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset} (Set.ofPred p)
hmono : StrictMonoOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}
n : ℕ
ih : ∀ m < n, (∀ (hf : (Set.ofPred p).Finite), m < #hf.toFinset) → nth p m ≤ f m
hn : ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset
k : ℕ
hk : k < n
⊢ n ∈ {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}

pp: case a
p : ℕ → Prop
f : ℕ → ℕ
hmaps : Set.MapsTo f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset} (Set.ofPred p)
hmono : StrictMonoOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}
n : ℕ
ih : ∀ m < n, (∀ (hf : (Set.ofPred p).Finite), m < #hf.toFinset) → nth p m ≤ f m
hn : ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset
k : ℕ
hk : k < n
⊢ k < n

Tactic:
<;>

Goal state after:
case x
p : ℕ → Prop
f : ℕ → ℕ
hmaps : Set.MapsTo f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset} (Set.ofPred p)
hmono : StrictMonoOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}
n : ℕ
ih : ∀ m < n, (∀ (hf : (Set.ofPred p).Finite), m < #hf.toFinset) → nth p m ≤ f m
hn : ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset
k : ℕ
hk : k < n
⊢ k ∈ {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}

case x
p : ℕ → Prop
f : ℕ → ℕ
hmaps : Set.MapsTo f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset} (Set.ofPred p)
hmono : StrictMonoOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}
n : ℕ
ih : ∀ m < n, (∀ (hf : (Set.ofPred p).Finite), m < #hf.toFinset) → nth p m ≤ f m
hn : ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset
k : ℕ
hk : k < n
⊢ n ∈ {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}

case a
p : ℕ → Prop
f : ℕ → ℕ
hmaps : Set.MapsTo f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset} (Set.ofPred p)
hmono : StrictMonoOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}
n : ℕ
ih : ∀ m < n, (∀ (hf : (Set.ofPred p).Finite), m < #hf.toFinset) → nth p m ≤ f m
hn : ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset
k : ℕ
hk : k < n
⊢ k < n
Module: Mathlib.Data.Num.Prime

Goal state before:
pp: case pos
n : PosNum
fuel : ℕ
ih : ∀ {k : PosNum}, (↑n).sqrt < fuel + ↑k.bit1 → ↑(n.minFacAux fuel k) = (↑n).minFacAux ↑k.bit1
k : PosNum
h : (↑n).sqrt < fuel + 1 + ↑k.bit1
h✝ : n < k.bit1 * k.bit1
⊢ ↑n = ↑n

pp: case pos
n : PosNum
fuel : ℕ
ih : ∀ {k : PosNum}, (↑n).sqrt < fuel + ↑k.bit1 → ↑(n.minFacAux fuel k) = (↑n).minFacAux ↑k.bit1
k : PosNum
h : (↑n).sqrt < fuel + 1 + ↑k.bit1
h✝¹ : ¬n < k.bit1 * k.bit1
h✝ : k.bit1 ∣ n
⊢ ↑k.bit1 = ↑k.bit1

pp: case neg
n : PosNum
fuel : ℕ
ih : ∀ {k : PosNum}, (↑n).sqrt < fuel + ↑k.bit1 → ↑(n.minFacAux fuel k) = (↑n).minFacAux ↑k.bit1
k : PosNum
h : (↑n).sqrt < fuel + 1 + ↑k.bit1
h✝¹ : ¬n < k.bit1 * k.bit1
h✝ : ¬k.bit1 ∣ n
⊢ ↑(n.minFacAux fuel k.succ) = (↑n).minFacAux (↑k.bit1 + 2)

Tactic:
<;>

Goal state after:
case pos
n : PosNum
fuel : ℕ
ih : ∀ {k : PosNum}, (↑n).sqrt < fuel + ↑k.bit1 → ↑(n.minFacAux fuel k) = (↑n).minFacAux ↑k.bit1
k : PosNum
h : (↑n).sqrt < fuel + 1 + ↑k.bit1
h✝ : n < k.bit1 * k.bit1
⊢ ↑n = ↑n

case pos
n : PosNum
fuel : ℕ
ih : ∀ {k : PosNum}, (↑n).sqrt < fuel + ↑k.bit1 → ↑(n.minFacAux fuel k) = (↑n).minFacAux ↑k.bit1
k : PosNum
h : (↑n).sqrt < fuel + 1 + ↑k.bit1
h✝¹ : ¬n < k.bit1 * k.bit1
h✝ : k.bit1 ∣ n
⊢ ↑k.bit1 = ↑k.bit1

case neg
n : PosNum
fuel : ℕ
ih : ∀ {k : PosNum}, (↑n).sqrt < fuel + ↑k.bit1 → ↑(n.minFacAux fuel k) = (↑n).minFacAux ↑k.bit1
k : PosNum
h : (↑n).sqrt < fuel + 1 + ↑k.bit1
h✝¹ : ¬n < k.bit1 * k.bit1
h✝ : ¬k.bit1 ∣ n
⊢ ↑(n.minFacAux fuel k.succ) = (↑n).minFacAux (↑k.bit1 + 2)
Module: Mathlib.Data.Num.Prime

Goal state before:
pp: case neg.e_a
n : PosNum
fuel : ℕ
ih : ∀ {k : PosNum}, (↑n).sqrt < fuel + ↑k.bit1 → ↑(n.minFacAux fuel k) = (↑n).minFacAux ↑k.bit1
k : PosNum
h : (↑n).sqrt < fuel + 1 + ↑k.bit1
h✝¹ : ¬n < k.bit1 * k.bit1
h✝ : ¬k.bit1 ∣ n
⊢ ↑k.succ.bit1 = ↑k.bit1 + 2

pp: n : PosNum
fuel : ℕ
ih : ∀ {k : PosNum}, (↑n).sqrt < fuel + ↑k.bit1 → ↑(n.minFacAux fuel k) = (↑n).minFacAux ↑k.bit1
k : PosNum
h : (↑n).sqrt < fuel + 1 + ↑k.bit1
h✝¹ : ¬n < k.bit1 * k.bit1
h✝ : ¬k.bit1 ∣ n
⊢ fuel + ↑k.succ.bit1 = (fuel + 1 + ↑k.bit1).succ

Tactic:
<;>

Goal state after:
case neg.e_a
n : PosNum
fuel : ℕ
ih : ∀ {k : PosNum}, (↑n).sqrt < fuel + ↑k.bit1 → ↑(n.minFacAux fuel k) = (↑n).minFacAux ↑k.bit1
k : PosNum
h : (↑n).sqrt < fuel + 1 + ↑k.bit1
h✝¹ : ¬n < k.bit1 * k.bit1
h✝ : ¬k.bit1 ∣ n
⊢ ↑k.succ.bit1 = ↑k.bit1 + 2

n : PosNum
fuel : ℕ
ih : ∀ {k : PosNum}, (↑n).sqrt < fuel + ↑k.bit1 → ↑(n.minFacAux fuel k) = (↑n).minFacAux ↑k.bit1
k : PosNum
h : (↑n).sqrt < fuel + 1 + ↑k.bit1
h✝¹ : ¬n < k.bit1 * k.bit1
h✝ : ¬k.bit1 ∣ n
⊢ fuel + ↑k.succ.bit1 = (fuel + 1 + ↑k.bit1).succ
Module: Mathlib.Data.Num.Prime

Goal state before:
pp: n : PosNum
⊢ ↑n + ↑n + ↑n = ↑n * (1 + 1 + 1)

Tactic:
simp only [mul_add, mul_one]

Goal state after: