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

Goal state before:
pp: α : Type
ds₁ ds₂ ds₃ : List ℕ
inst✝ : Semigroup α
x : Holor α ds₁
y : Holor α ds₂
z : Holor α ds₃
t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)
⊢ x t.assocRight.take * (y t.assocRight.drop.take * z t.drop) =
    cast ⋯ (fun t ↦ x t.take * (y t.drop.take * z t.drop.drop)) t

Tactic:
← HolorIndex.drop_drop,

Goal state after:
α : Type
ds₁ ds₂ ds₃ : List ℕ
inst✝ : Semigroup α
x : Holor α ds₁
y : Holor α ds₂
z : Holor α ds₃
t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)
⊢ x t.assocRight.take * (y t.assocRight.drop.take * z t.assocRight.drop.drop) =
    cast ⋯ (fun t ↦ x t.take * (y t.drop.take * z t.drop.drop)) t
Module: Mathlib.Data.Int.Lemmas

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

Tactic:
rw [← sq_eq_sq₀ ha hb, ← natAbs_eq_iff_sq_eq]

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

Goal state before:
pp: a b r q : ℤ
h : b ≠ 0
⊢ a / b = q ∧ a % b = r ↔ r + b * q = a ∧ 0 ≤ r ∧ r < |b|

Tactic:
constructor

Goal state after:
case mp
a b r q : ℤ
h : b ≠ 0
⊢ a / b = q ∧ a % b = r → r + b * q = a ∧ 0 ≤ r ∧ r < |b|

case mpr
a b r q : ℤ
h : b ≠ 0
⊢ r + b * q = a ∧ 0 ≤ r ∧ r < |b| → a / b = q ∧ a % b = r
Module: Mathlib.Data.Int.Lemmas

Goal state before:
pp: case mpr
a b r q : ℤ
h : b ≠ 0
hz : 0 ≤ r
hb : r < |b|
⊢ (r + b * q) / b = q ∧ (r + b * q) % b = r

Tactic:
constructor

Goal state after:
case mpr.left
a b r q : ℤ
h : b ≠ 0
hz : 0 ≤ r
hb : r < |b|
⊢ (r + b * q) / b = q

case mpr.right
a b r q : ℤ
h : b ≠ 0
hz : 0 ≤ r
hb : r < |b|
⊢ (r + b * q) % b = r
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: a b r v : ℕ
x : ℤ
⊢ (∃ a_1, ((a ≤ a_1 ∧ a_1 < b) ∧ a_1 ≡ v [MOD r]) ∧ ↑a_1 = x) ↔ (↑a ≤ x ∧ x < ↑b) ∧ x ≡ ↑v [ZMOD ↑r]

Tactic:
constructor

Goal state after:
case mp
a b r v : ℕ
x : ℤ
⊢ (∃ a_1, ((a ≤ a_1 ∧ a_1 < b) ∧ a_1 ≡ v [MOD r]) ∧ ↑a_1 = x) → (↑a ≤ x ∧ x < ↑b) ∧ x ≡ ↑v [ZMOD ↑r]

case mpr
a b r v : ℕ
x : ℤ
⊢ (↑a ≤ x ∧ x < ↑b) ∧ x ≡ ↑v [ZMOD ↑r] → ∃ a_2, ((a ≤ a_2 ∧ a_2 < b) ∧ a_2 ≡ v [MOD r]) ∧ ↑a_2 = x
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: case mp
a b r v : ℕ
x : ℤ
⊢ (∃ a_1, ((a ≤ a_1 ∧ a_1 < b) ∧ a_1 ≡ v [MOD r]) ∧ ↑a_1 = x) → (↑a ≤ x ∧ x < ↑b) ∧ x ≡ ↑v [ZMOD ↑r]

Tactic:
simp_rw [forall_exists_index, ← natCast_modEq_iff]; intro y ⟨h, c⟩; subst c; exact_mod_cast h

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

Goal state before:
pp: a b r v : ℕ
x : ℤ
⊢ (∃ a_1, ((a < a_1 ∧ a_1 ≤ b) ∧ a_1 ≡ v [MOD r]) ∧ ↑a_1 = x) ↔ (↑a < x ∧ x ≤ ↑b) ∧ x ≡ ↑v [ZMOD ↑r]

Tactic:
constructor

Goal state after:
case mp
a b r v : ℕ
x : ℤ
⊢ (∃ a_1, ((a < a_1 ∧ a_1 ≤ b) ∧ a_1 ≡ v [MOD r]) ∧ ↑a_1 = x) → (↑a < x ∧ x ≤ ↑b) ∧ x ≡ ↑v [ZMOD ↑r]

case mpr
a b r v : ℕ
x : ℤ
⊢ (↑a < x ∧ x ≤ ↑b) ∧ x ≡ ↑v [ZMOD ↑r] → ∃ a_2, ((a < a_2 ∧ a_2 ≤ b) ∧ a_2 ≡ v [MOD r]) ∧ ↑a_2 = x
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: case mp
a b r v : ℕ
x : ℤ
⊢ (∃ a_1, ((a < a_1 ∧ a_1 ≤ b) ∧ a_1 ≡ v [MOD r]) ∧ ↑a_1 = x) → (↑a < x ∧ x ≤ ↑b) ∧ x ≡ ↑v [ZMOD ↑r]

Tactic:
simp_rw [forall_exists_index, ← natCast_modEq_iff]; intro y ⟨h, c⟩; subst c; exact_mod_cast h

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

Goal state before:
pp: b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
⊢ -↑(v % r) / ↑r ∈ Set.Ioc (-1) 0

Tactic:
Set.mem_Ioc,

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

Goal state before:
pp: case neg
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
h : ¬v % r < b % r
⊢ (↑(b % r) - ↑(v % r)) / ↑r ∈ Set.Ioc (-1) 0

Tactic:
Set.mem_Ioc,

Goal state after:
case neg
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
h : ¬v % r < b % r
⊢ -1 < (↑(b % r) - ↑(v % r)) / ↑r ∧ (↑(b % r) - ↑(v % r)) / ↑r ≤ 0
Module: Mathlib.Data.List.TakeWhile

Goal state before:
pp: case true
α : Type u_1
p : α → Bool
l : List α
head : α
tail : List α
hi : find? p tail = (dropWhile (fun x ↦ !p x) tail).head?
phh : true = p head
⊢ find? p (head :: tail) = (dropWhile (fun x ↦ !p x) (head :: tail)).head?

Tactic:
rw [find?_cons_of_pos phh.symm, dropWhile_cons_of_neg]
      · simp
      · simpa using phh

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

Goal state before:
pp: n m l : ℕ
hlm : l ≤ m
⊢ filter (fun x ↦ decide (x < l)) (Ico n m) = Ico n l

Tactic:
rcases le_total n l with hnl | hln

Goal state after:
case inl
n m l : ℕ
hlm : l ≤ m
hnl : n ≤ l
⊢ filter (fun x ↦ decide (x < l)) (Ico n m) = Ico n l

case inr
n m l : ℕ
hlm : l ≤ m
hln : l ≤ n
⊢ filter (fun x ↦ decide (x < l)) (Ico n m) = Ico n l
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: n m l : ℕ
⊢ filter (fun x ↦ decide (l ≤ x)) (Ico n m) = Ico (max n l) m

Tactic:
rcases le_total n l with hnl | hln

Goal state after:
case inl
n m l : ℕ
hnl : n ≤ l
⊢ filter (fun x ↦ decide (l ≤ x)) (Ico n m) = Ico (max n l) m

case inr
n m l : ℕ
hln : l ≤ n
⊢ filter (fun x ↦ decide (l ≤ x)) (Ico n m) = Ico (max n l) m
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: α : Type u_1
p : ℕ
w : List α
⊢ w.HasPeriod p ↔ ∀ i < w.length - p, w[i]? = w[i + p]?

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
p : ℕ
w : List α
⊢ w.HasPeriod p → ∀ i < w.length - p, w[i]? = w[i + p]?

case mpr
α : Type u_1
p : ℕ
w : List α
⊢ (∀ i < w.length - p, w[i]? = w[i + p]?) → w.HasPeriod p
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: case nil.inl
α : Type u_1
m : List α
r : α → α → Bool
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : IsChain (fun y x ↦ r x y = true) g
hm : m ∈ []
⊢ IsChain (fun x y ↦ r x y = true) m

pp: case nil.inr
α : Type u_1
r : α → α → Bool
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : IsChain (fun y x ↦ r x y = true) g
⊢ IsChain (fun x y ↦ r x y = true) (a :: g).reverse

Tactic:
· cases not_mem_nil hm

Goal state after:
case nil.inr
α : Type u_1
r : α → α → Bool
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : IsChain (fun y x ↦ r x y = true) g
⊢ IsChain (fun x y ↦ r x y = true) (a :: g).reverse
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: α : Type u_1
p : ℕ
w : List α
⊢ w.HasPeriod p ↔ ∀ i < w.length, w[i]? = w[i % p]?

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
p : ℕ
w : List α
⊢ w.HasPeriod p → ∀ i < w.length, w[i]? = w[i % p]?

case mpr
α : Type u_1
p : ℕ
w : List α
⊢ (∀ i < w.length, w[i]? = w[i % p]?) → w.HasPeriod p
Module: Mathlib.LinearAlgebra.Matrix.Bilinear

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
A : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : Semiring R
inst✝² : NonUnitalSemiring A
inst✝¹ : Module R A
inst✝ : SMulCommClass R A A
a : Matrix l m A
b : Matrix m n A
⊢ mulLeftLinearMap o R (a * b) = mulLeftLinearMap o R a ∘ₗ mulLeftLinearMap o R b

Tactic:
ext

Goal state after:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
A : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : Semiring R
inst✝² : NonUnitalSemiring A
inst✝¹ : Module R A
inst✝ : SMulCommClass R A A
a : Matrix l m A
b : Matrix m n A
x✝ : Matrix n o A
i✝ : l
j✝ : o
⊢ (mulLeftLinearMap o R (a * b)) x✝ i✝ j✝ = (mulLeftLinearMap o R a ∘ₗ mulLeftLinearMap o R b) x✝ i✝ j✝
Module: Mathlib.LinearAlgebra.Matrix.Bilinear

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
A : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : Semiring R
inst✝² : NonUnitalSemiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
a : Matrix m n A
b : Matrix n o A
⊢ mulRightLinearMap l R (a * b) = mulRightLinearMap l R b ∘ₗ mulRightLinearMap l R a

Tactic:
ext

Goal state after:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
A : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : Semiring R
inst✝² : NonUnitalSemiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
a : Matrix m n A
b : Matrix n o A
x✝ : Matrix l m A
i✝ : l
j✝ : o
⊢ (mulRightLinearMap l R (a * b)) x✝ i✝ j✝ = (mulRightLinearMap l R b ∘ₗ mulRightLinearMap l R a) x✝ i✝ j✝
Module: Mathlib.LinearAlgebra.Matrix.Bilinear

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : Semiring R
inst✝³ : Semiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : Nonempty n
a : Matrix l m A
⊢ mulLeftLinearMap n R a = 0 ↔ a = 0

Tactic:
constructor

Goal state after:
case mp
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : Semiring R
inst✝³ : Semiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : Nonempty n
a : Matrix l m A
⊢ mulLeftLinearMap n R a = 0 → a = 0

case mpr
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : Semiring R
inst✝³ : Semiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : Nonempty n
a : Matrix l m A
⊢ a = 0 → mulLeftLinearMap n R a = 0
Module: Mathlib.LinearAlgebra.Matrix.Bilinear

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : Semiring R
inst✝³ : Semiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
a : Matrix m n A
inst✝ : Nonempty l
⊢ mulRightLinearMap l R a = 0 ↔ a = 0

Tactic:
constructor

Goal state after:
case mp
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : Semiring R
inst✝³ : Semiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
a : Matrix m n A
inst✝ : Nonempty l
⊢ mulRightLinearMap l R a = 0 → a = 0

case mpr
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : Semiring R
inst✝³ : Semiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
a : Matrix m n A
inst✝ : Nonempty l
⊢ a = 0 → mulRightLinearMap l R a = 0
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: α : Type u_1
w : List α
p q : ℕ
per_p : w.HasPeriod p
per_q : w.HasPeriod q
len : p + q - p.gcd q ≤ w.length
p_pos : p > 0
q_pos : q > 0
hyp : compare p q = Ordering.gt
q_lt_p : q < p
gcd_lt_p : p.gcd q < p
per_diff : (drop q w).HasPeriod (p - q)
⊢ (drop q w).HasPeriod q

Tactic:
apply @HasPeriod.factor _ (take q w) (drop q w) [] q

Goal state after:
α : Type u_1
w : List α
p q : ℕ
per_p : w.HasPeriod p
per_q : w.HasPeriod q
len : p + q - p.gcd q ≤ w.length
p_pos : p > 0
q_pos : q > 0
hyp : compare p q = Ordering.gt
q_lt_p : q < p
gcd_lt_p : p.gcd q < p
per_diff : (drop q w).HasPeriod (p - q)
⊢ (take q w ++ drop q w ++ []).HasPeriod q
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: α : Type u_1
m : List α
r : α → α → Bool
l : List (List α)
⊢ splitBy r m = l ↔
    m = l.flatten ∧
      ¬[] ∈ l ∧
        (∀ (m : List α), m ∈ l → IsChain (fun x y ↦ r x y = true) m) ∧
          IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) l

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
m : List α
r : α → α → Bool
l : List (List α)
⊢ splitBy r m = l →
    m = l.flatten ∧
      ¬[] ∈ l ∧
        (∀ (m : List α), m ∈ l → IsChain (fun x y ↦ r x y = true) m) ∧
          IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) l

case mpr
α : Type u_1
m : List α
r : α → α → Bool
l : List (List α)
⊢ m = l.flatten ∧
      ¬[] ∈ l ∧
        (∀ (m : List α), m ∈ l → IsChain (fun x y ↦ r x y = true) m) ∧
          IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) l →
    splitBy r m = l
Module: Mathlib.LinearAlgebra.Matrix.DualNumber

Goal state before:
pp: R n : Type
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A B : Matrix n n (DualNumber R)
⊢ (of fun i j ↦ fst ((A * B) i j), of fun i j ↦ snd ((A * B) i j)) =
    (of fun i j ↦ fst (A i j), of fun i j ↦ snd (A i j)) * (of fun i j ↦ fst (B i j), of fun i j ↦ snd (B i j))

Tactic:
ext

Goal state after:
case h1
R n : Type
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A B : Matrix n n (DualNumber R)
i✝ j✝ : n
⊢ fst (of fun i j ↦ fst ((A * B) i j), of fun i j ↦ snd ((A * B) i j)) i✝ j✝ =
    fst ((of fun i j ↦ fst (A i j), of fun i j ↦ snd (A i j)) * (of fun i j ↦ fst (B i j), of fun i j ↦ snd (B i j))) i✝
      j✝

case h2
R n : Type
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A B : Matrix n n (DualNumber R)
i✝ j✝ : n
⊢ snd (of fun i j ↦ fst ((A * B) i j), of fun i j ↦ snd ((A * B) i j)) i✝ j✝ =
    snd ((of fun i j ↦ fst (A i j), of fun i j ↦ snd (A i j)) * (of fun i j ↦ fst (B i j), of fun i j ↦ snd (B i j))) i✝
      j✝
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst✝² : Semiring R
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
B₁ : Matrix m₁ n R
B₂ : Matrix m₂ n R
v₁ : m₁ → R
v₂ : m₂ → R
⊢ Sum.elim v₁ v₂ ᵥ* B₁.fromRows B₂ = v₁ ᵥ* B₁ + v₂ ᵥ* B₂

Tactic:
ext

Goal state after:
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst✝² : Semiring R
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
B₁ : Matrix m₁ n R
B₂ : Matrix m₂ n R
v₁ : m₁ → R
v₂ : m₂ → R
x✝ : n
⊢ (Sum.elim v₁ v₂ ᵥ* B₁.fromRows B₂) x✝ = (v₁ ᵥ* B₁ + v₂ ᵥ* B₂) x✝
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
inst✝² : Semiring R
inst✝¹ : Fintype n₁
inst✝ : Fintype n₂
A₁ : Matrix m n₁ R
A₂ : Matrix m n₂ R
v₁ : n₁ → R
v₂ : n₂ → R
⊢ A₁.fromCols A₂ *ᵥ Sum.elim v₁ v₂ = A₁ *ᵥ v₁ + A₂ *ᵥ v₂

Tactic:
ext

Goal state after:
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
inst✝² : Semiring R
inst✝¹ : Fintype n₁
inst✝ : Fintype n₂
A₁ : Matrix m n₁ R
A₂ : Matrix m n₂ R
v₁ : n₁ → R
v₂ : n₂ → R
x✝ : m
⊢ (A₁.fromCols A₂ *ᵥ Sum.elim v₁ v₂) x✝ = (A₁ *ᵥ v₁ + A₂ *ᵥ v₂) x✝
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: R : Type u_1
m : Type u_2
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝² : Semiring R
inst✝¹ : Fintype n₁
inst✝ : Fintype n₂
A₁ : Matrix m n₁ R
A₂ : Matrix m n₂ R
B₁ : Matrix n₁ n R
B₂ : Matrix n₂ n R
⊢ A₁.fromCols A₂ * B₁.fromRows B₂ = A₁ * B₁ + A₂ * B₂

Tactic:
ext

Goal state after:
R : Type u_1
m : Type u_2
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝² : Semiring R
inst✝¹ : Fintype n₁
inst✝ : Fintype n₂
A₁ : Matrix m n₁ R
A₂ : Matrix m n₂ R
B₁ : Matrix n₁ n R
B₂ : Matrix n₂ n R
i✝ : m
j✝ : n
⊢ (A₁.fromCols A₂ * B₁.fromRows B₂) i✝ j✝ = (A₁ * B₁ + A₂ * B₂) i✝ j✝
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: case empty
α : Type u_1
inst✝ : Preorder α
M : Multiset α
hM : ∀ (x : α), x ∈ 0 → Acc LT.lt x
⊢ Acc OneStep 0

Tactic:
constructor

Goal state after:
case empty
α : Type u_1
inst✝ : Preorder α
M : Multiset α
hM : ∀ (x : α), x ∈ 0 → Acc LT.lt x
⊢ ∀ (y : Multiset α), y.OneStep 0 → Acc OneStep y
Module: Mathlib.Data.NNRat.Floor

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
x : ℚ≥0
⊢ ↑↑⌈x⌉₊ < ↑x + 1 ∧ ↑x ≤ ↑↑⌈x⌉₊

Tactic:
constructor

Goal state after:
case left
K : Type u_1
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
x : ℚ≥0
⊢ ↑↑⌈x⌉₊ < ↑x + 1

case right
K : Type u_1
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
x : ℚ≥0
⊢ ↑x ≤ ↑↑⌈x⌉₊
Module: Mathlib.Data.NNRat.Floor

Goal state before:
pp: R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
r : R
n d : ℕ
h : IsNNRat r n d
res : ℕ
hres : ⌈↑n / ↑d⌉₊ = res
⊢ IsNat ⌈r⌉₊ res

Tactic:
constructor

Goal state after:
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
r : R
n d : ℕ
h : IsNNRat r n d
res : ℕ
hres : ⌈↑n / ↑d⌉₊ = res
⊢ ⌈r⌉₊ = ↑res
Module: Mathlib.Data.NNRat.Floor

Goal state before:
pp: R : Type u_1
inst✝³ : Field R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
r : R
n d : ℕ
h : IsRat r (Int.negOfNat n) d
⊢ IsNat ⌈r⌉₊ 0

Tactic:
constructor

Goal state after:
R : Type u_1
inst✝³ : Field R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
r : R
n d : ℕ
h : IsRat r (Int.negOfNat n) d
⊢ ⌈r⌉₊ = ↑0
Module: Mathlib.Data.Nat.Prime.Factorial

Goal state before:
pp: m n : ℕ
hm : m ≠ 1
⊢ m.minFac ≤ n ↔ ∃ p, Prime p ∧ p ∣ m ∧ p ∣ n !

Tactic:
constructor

Goal state after:
case mp
m n : ℕ
hm : m ≠ 1
⊢ m.minFac ≤ n → ∃ p, Prime p ∧ p ∣ m ∧ p ∣ n !

case mpr
m n : ℕ
hm : m ≠ 1
⊢ (∃ p, Prime p ∧ p ∣ m ∧ p ∣ n !) → m.minFac ≤ n
Module: Mathlib.Data.Nat.ChineseRemainder

Goal state before:
pp: case cons
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
⊢ (a ≡ b [MOD m] ∧ ∀ (i : Fin l.length), a ≡ b [MOD l.get i]) ↔ ∀ (i : Fin (l.length + 1)), a ≡ b [MOD (m :: l).get i]

Tactic:
constructor

Goal state after:
case cons.mp
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
⊢ (a ≡ b [MOD m] ∧ ∀ (i : Fin l.length), a ≡ b [MOD l.get i]) → ∀ (i : Fin (l.length + 1)), a ≡ b [MOD (m :: l).get i]

case cons.mpr
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
⊢ (∀ (i : Fin (l.length + 1)), a ≡ b [MOD (m :: l).get i]) → a ≡ b [MOD m] ∧ ∀ (i : Fin l.length), a ≡ b [MOD l.get i]
Module: Mathlib.Data.Nat.ChineseRemainder

Goal state before:
pp: ι : Type u_1
a s : ι → ℕ
m : Multiset ι
l l' : List ι
pp : l.Perm l'
nod' : l'.Nodup
nod : l.Nodup
hs' : ∀ i ∈ l', s i ≠ 0
hs : ∀ i ∈ l, s i ≠ 0
co' : {x | x ∈ l'}.Pairwise (Coprime on s)
co : {x | x ∈ l}.Pairwise (Coprime on s)
lco : List.Pairwise (Coprime on s) l
this :
  ∀ {m' : Multiset ι} {e : ↑l = m'} {nod'' : m'.Nodup} {hs'' : ∀ i ∈ m', s i ≠ 0}
    {co'' : {x | x ∈ m'}.Pairwise (Coprime on s)},
    ↑(Eq.ndrec (motive := fun m ↦
          m.Nodup → (∀ i ∈ m, s i ≠ 0) → {x | x ∈ m}.Pairwise (Coprime on s) → { k // ∀ i ∈ m, k ≡ a i [MOD s i] })
          (fun nod x co ↦ chineseRemainderOfList a s l ⋯) e nod'' hs'' co'') =
      ↑(chineseRemainderOfList a s l lco)
⊢ Eq.ndrec (motive := fun x ↦
      x.Nodup → (∀ i ∈ x, s i ≠ 0) → {x_1 | x_1 ∈ x}.Pairwise (Coprime on s) → { k // ∀ i ∈ x, k ≡ a i [MOD s i] })
      (fun nod x co ↦ chineseRemainderOfList a s l ⋯) ⋯ nod' hs' co' =
    chineseRemainderOfList a s l' ⋯

Tactic:
ext

Goal state after:
ι : Type u_1
a s : ι → ℕ
m : Multiset ι
l l' : List ι
pp : l.Perm l'
nod' : l'.Nodup
nod : l.Nodup
hs' : ∀ i ∈ l', s i ≠ 0
hs : ∀ i ∈ l, s i ≠ 0
co' : {x | x ∈ l'}.Pairwise (Coprime on s)
co : {x | x ∈ l}.Pairwise (Coprime on s)
lco : List.Pairwise (Coprime on s) l
this :
  ∀ {m' : Multiset ι} {e : ↑l = m'} {nod'' : m'.Nodup} {hs'' : ∀ i ∈ m', s i ≠ 0}
    {co'' : {x | x ∈ m'}.Pairwise (Coprime on s)},
    ↑(Eq.ndrec (motive := fun m ↦
          m.Nodup → (∀ i ∈ m, s i ≠ 0) → {x | x ∈ m}.Pairwise (Coprime on s) → { k // ∀ i ∈ m, k ≡ a i [MOD s i] })
          (fun nod x co ↦ chineseRemainderOfList a s l ⋯) e nod'' hs'' co'') =
      ↑(chineseRemainderOfList a s l lco)
⊢ ↑(Eq.ndrec (motive := fun x ↦
        x.Nodup → (∀ i ∈ x, s i ≠ 0) → {x_1 | x_1 ∈ x}.Pairwise (Coprime on s) → { k // ∀ i ∈ x, k ≡ a i [MOD s i] })
        (fun nod x co ↦ chineseRemainderOfList a s l ⋯) ⋯ nod' hs' co') =
    ↑(chineseRemainderOfList a s l' ⋯)
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: 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₂

Tactic:
constructor

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.Fib.Zeckendorf

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ (n - fib n.greatestFib).greatestFib ≤ n.greatestFib - 2

Tactic:
by
  rw [← Nat.lt_succ_iff, greatestFib_lt, tsub_lt_iff_right n.fib_greatestFib_le, Nat.sub_succ,
    succ_pred, ← fib_add_one]
  · exact n.lt_fib_greatestFib_add_one
  · simpa
  · simpa [← succ_le_iff, tsub_eq_zero_iff_le] using hn.bot_lt

Goal state after:
Module: Mathlib.Data.Nat.Fib.Zeckendorf

Goal state before:
pp: case inr
n a : ℕ
ha :
  a ∈
    ((n + 1 - fib (n + 1).greatestFib).greatestFib ::
        ((n + 1 - fib (n + 1).greatestFib - fib (n + 1 - fib (n + 1).greatestFib).greatestFib).zeckendorf ++ [0])).head?
h : n + 1 - fib (n + 1).greatestFib > 0
⊢ a + 2 ≤ (n + 1).greatestFib

Tactic:
head?_cons,

Goal state after:
case inr
n a : ℕ
ha : a ∈ some (n + 1 - fib (n + 1).greatestFib).greatestFib
h : n + 1 - fib (n + 1).greatestFib > 0
⊢ a + 2 ≤ (n + 1).greatestFib
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: n : ℕ
hn : 1 < n
hpn : (Icc 1 (n - 1)).gcd n.choose ≠ 1
q : ℕ
hq : Nat.Prime q
h : ∀ b ∈ Icc 1 (n - 1), n.choose b ≡ 0 [MOD q]
this✝ : Fact (Nat.Prime q)
this : n = q ^ multiplicity q n
⊢ q ∣ n

Tactic:
specialize h 1 (by grind)

Goal state after:
n : ℕ
hn : 1 < n
hpn : (Icc 1 (n - 1)).gcd n.choose ≠ 1
q : ℕ
hq : Nat.Prime q
h : n.choose 1 ≡ 0 [MOD q]
this✝ : Fact (Nat.Prime q)
this : n = q ^ multiplicity q n
⊢ q ∣ n
Module: Mathlib.Data.Ordmap.Ordnode

Goal state before:
pp: case nil.node.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
lls : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ Ordnode α

Tactic:
rcases id lr with _ | ⟨lrs, lrl, lrx, lrr⟩

Goal state after:
case nil.node.node.nil
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
lls : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ Ordnode α

case nil.node.node.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
lls : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
⊢ Ordnode α
Module: Mathlib.Data.Ordmap.Ordnode

Goal state before:
pp: case node.node.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
l✝¹ : Ordnode α
x✝¹ : α
r✝¹ : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
lls : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ Ordnode α

Tactic:
rcases id lr with _ | ⟨lrs, lrl, lrx, lrr⟩

Goal state after:
case node.node.node.nil
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
l✝¹ : Ordnode α
x✝¹ : α
r✝¹ : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
lls : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ Ordnode α

case node.node.node.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
l✝¹ : Ordnode α
x✝¹ : α
r✝¹ : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
lls : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
⊢ Ordnode α
Module: Mathlib.Data.Ordmap.Ordnode

Goal state before:
pp: case node.nil.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
lls : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ Ordnode α

Tactic:
rcases id lr with _ | ⟨lrs, lrl, lrx, lrr⟩

Goal state after:
case node.nil.node.nil
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
lls : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ Ordnode α

case node.nil.node.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
lls : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
⊢ Ordnode α