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

Goal state before:
pp: case inr.inr.refine_1
α : Type u_1
r : α → α → Bool
l m : List α
ha : ∀ (x : α), x ∈ l.getLast? → ∀ (y : α), y ∈ m.head? → r x y = false
hl : l ≠ []
hm : m ≠ []
⊢ ∀ (m_1 : List α), m_1 ∈ splitBy r l ++ splitBy r m → IsChain (fun x y ↦ r x y = true) m_1

pp: case inr.inr.refine_2
α : Type u_1
r : α → α → Bool
l m : List α
ha : ∀ (x : α), x ∈ l.getLast? → ∀ (y : α), y ∈ m.head? → r x y = false
hl : l ≠ []
hm : m ≠ []
⊢ IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) (splitBy r l ++ splitBy r m)

Tactic:
·

Goal state after:
case inr.inr.refine_1
α : Type u_1
r : α → α → Bool
l m : List α
ha : ∀ (x : α), x ∈ l.getLast? → ∀ (y : α), y ∈ m.head? → r x y = false
hl : l ≠ []
hm : m ≠ []
⊢ ∀ (m_1 : List α), m_1 ∈ splitBy r l ++ splitBy r m → IsChain (fun x y ↦ r x y = true) m_1
Module: Mathlib.LinearAlgebra.Matrix.DualNumber

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

pp: 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✝

Tactic:
·

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✝
Module: Mathlib.LinearAlgebra.Matrix.DualNumber

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

Tactic:
·

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

Goal state before:
pp: case h.a
α : Type u_1
r : α → α → Bool
l m : List α
ha : ∀ (x : α), x ∈ l.getLast? → ∀ (y : α), y ∈ m.head? → r x y = false
hl : l ≠ []
hm : m ≠ []
x : List α
hx : x ∈ (splitBy r l).getLast?
y : List α
hy : y ∈ (splitBy r m).head?
⊢ x.getLast ⋯ ∈ l.getLast?

pp: case h.a
α : Type u_1
r : α → α → Bool
l m : List α
ha : ∀ (x : α), x ∈ l.getLast? → ∀ (y : α), y ∈ m.head? → r x y = false
hl : l ≠ []
hm : m ≠ []
x : List α
hx : x ∈ (splitBy r l).getLast?
y : List α
hy : y ∈ (splitBy r m).head?
⊢ y.head ⋯ ∈ m.head?

Tactic:
·

Goal state after:
case h.a
α : Type u_1
r : α → α → Bool
l m : List α
ha : ∀ (x : α), x ∈ l.getLast? → ∀ (y : α), y ∈ m.head? → r x y = false
hl : l ≠ []
hm : m ≠ []
x : List α
hx : x ∈ (splitBy r l).getLast?
y : List α
hy : y ∈ (splitBy r m).head?
⊢ x.getLast ⋯ ∈ l.getLast?
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: case h.a
α : Type u_1
r : α → α → Bool
l m : List α
ha : ∀ (x : α), x ∈ l.getLast? → ∀ (y : α), y ∈ m.head? → r x y = false
hl : l ≠ []
hm : m ≠ []
x : List α
hx : x ∈ (splitBy r l).getLast?
y : List α
hy : y ∈ (splitBy r m).head?
⊢ y.head ⋯ ∈ m.head?

Tactic:
·

Goal state after:
case h.a
α : Type u_1
r : α → α → Bool
l m : List α
ha : ∀ (x : α), x ∈ l.getLast? → ∀ (y : α), y ∈ m.head? → r x y = false
hl : l ≠ []
hm : m ≠ []
x : List α
hx : x ∈ (splitBy r l).getLast?
y : List α
hy : y ∈ (splitBy r m).head?
⊢ y.head ⋯ ∈ m.head?
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : Preorder α
X₁ Y₁ Z₁ : Multiset α
hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ z, z ∈ Z₁ ∧ y < z
X₂ Y₂ Z₂ : Multiset α
hZ₂ : Z₂ ≠ ∅
hXZXY : Z₁ + X₁ = Y₂ + X₂
hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ z, z ∈ Z₂ ∧ y < z
⊢ Z₂ + (Z₁ - Y₂) ≠ ∅

pp: case refine_2
α : Type u_1
inst✝ : Preorder α
X₁ Y₁ Z₁ : Multiset α
hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ z, z ∈ Z₁ ∧ y < z
X₂ Y₂ Z₂ : Multiset α
hZ₂ : Z₂ ≠ ∅
hXZXY : Z₁ + X₁ = Y₂ + X₂
hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ z, z ∈ Z₂ ∧ y < z
⊢ X₁ + Y₁ = X₁ ∩ X₂ + (Y₁ + (Y₂ - Z₁))

pp: case refine_3
α : Type u_1
inst✝ : Preorder α
X₁ Y₁ Z₁ : Multiset α
hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ z, z ∈ Z₁ ∧ y < z
X₂ Y₂ Z₂ : Multiset α
hZ₂ : Z₂ ≠ ∅
hXZXY : Z₁ + X₁ = Y₂ + X₂
hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ z, z ∈ Z₂ ∧ y < z
⊢ X₂ + Z₂ = X₁ ∩ X₂ + (Z₂ + (Z₁ - Y₂))

pp: case refine_4
α : Type u_1
inst✝ : Preorder α
X₁ Y₁ Z₁ : Multiset α
hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ z, z ∈ Z₁ ∧ y < z
X₂ Y₂ Z₂ : Multiset α
hZ₂ : Z₂ ≠ ∅
hXZXY : Z₁ + X₁ = Y₂ + X₂
hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ z, z ∈ Z₂ ∧ y < z
⊢ ∀ (y : α), y ∈ Y₁ + (Y₂ - Z₁) → ∃ z, z ∈ Z₂ + (Z₁ - Y₂) ∧ y < z

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
inst✝ : Preorder α
X₁ Y₁ Z₁ : Multiset α
hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ z, z ∈ Z₁ ∧ y < z
X₂ Y₂ Z₂ : Multiset α
hZ₂ : Z₂ ≠ ∅
hXZXY : Z₁ + X₁ = Y₂ + X₂
hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ z, z ∈ Z₂ ∧ y < z
⊢ Z₂ + (Z₁ - Y₂) ≠ ∅
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : Preorder α
X₁ Y₁ Z₁ : Multiset α
hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ z, z ∈ Z₁ ∧ y < z
X₂ Y₂ Z₂ : Multiset α
hZ₂ : Z₂ ≠ ∅
hXZXY : Z₁ + X₁ = Y₂ + X₂
hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ z, z ∈ Z₂ ∧ y < z
⊢ X₁ + Y₁ = X₁ ∩ X₂ + (Y₁ + (Y₂ - Z₁))

pp: case refine_3
α : Type u_1
inst✝ : Preorder α
X₁ Y₁ Z₁ : Multiset α
hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ z, z ∈ Z₁ ∧ y < z
X₂ Y₂ Z₂ : Multiset α
hZ₂ : Z₂ ≠ ∅
hXZXY : Z₁ + X₁ = Y₂ + X₂
hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ z, z ∈ Z₂ ∧ y < z
⊢ X₂ + Z₂ = X₁ ∩ X₂ + (Z₂ + (Z₁ - Y₂))

pp: case refine_4
α : Type u_1
inst✝ : Preorder α
X₁ Y₁ Z₁ : Multiset α
hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ z, z ∈ Z₁ ∧ y < z
X₂ Y₂ Z₂ : Multiset α
hZ₂ : Z₂ ≠ ∅
hXZXY : Z₁ + X₁ = Y₂ + X₂
hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ z, z ∈ Z₂ ∧ y < z
⊢ ∀ (y : α), y ∈ Y₁ + (Y₂ - Z₁) → ∃ z, z ∈ Z₂ + (Z₁ - Y₂) ∧ y < z

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
inst✝ : Preorder α
X₁ Y₁ Z₁ : Multiset α
hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ z, z ∈ Z₁ ∧ y < z
X₂ Y₂ Z₂ : Multiset α
hZ₂ : Z₂ ≠ ∅
hXZXY : Z₁ + X₁ = Y₂ + X₂
hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ z, z ∈ Z₂ ∧ y < z
⊢ X₁ + Y₁ = X₁ ∩ X₂ + (Y₁ + (Y₂ - Z₁))
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: case refine_3
α : Type u_1
inst✝ : Preorder α
X₁ Y₁ Z₁ : Multiset α
hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ z, z ∈ Z₁ ∧ y < z
X₂ Y₂ Z₂ : Multiset α
hZ₂ : Z₂ ≠ ∅
hXZXY : Z₁ + X₁ = Y₂ + X₂
hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ z, z ∈ Z₂ ∧ y < z
⊢ X₂ + Z₂ = X₁ ∩ X₂ + (Z₂ + (Z₁ - Y₂))

pp: case refine_4
α : Type u_1
inst✝ : Preorder α
X₁ Y₁ Z₁ : Multiset α
hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ z, z ∈ Z₁ ∧ y < z
X₂ Y₂ Z₂ : Multiset α
hZ₂ : Z₂ ≠ ∅
hXZXY : Z₁ + X₁ = Y₂ + X₂
hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ z, z ∈ Z₂ ∧ y < z
⊢ ∀ (y : α), y ∈ Y₁ + (Y₂ - Z₁) → ∃ z, z ∈ Z₂ + (Z₁ - Y₂) ∧ y < z

Tactic:
·

Goal state after:
case refine_3
α : Type u_1
inst✝ : Preorder α
X₁ Y₁ Z₁ : Multiset α
hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ z, z ∈ Z₁ ∧ y < z
X₂ Y₂ Z₂ : Multiset α
hZ₂ : Z₂ ≠ ∅
hXZXY : Z₁ + X₁ = Y₂ + X₂
hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ z, z ∈ Z₂ ∧ y < z
⊢ X₂ + Z₂ = X₁ ∩ X₂ + (Z₂ + (Z₁ - Y₂))
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: case refine_4.refine_1
α : Type u_1
inst✝ : Preorder α
X₁ Y₁ Z₁ : Multiset α
hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ z, z ∈ Z₁ ∧ y < z
X₂ Y₂ Z₂ : Multiset α
hZ₂ : Z₂ ≠ ∅
hXZXY : Z₁ + X₁ = Y₂ + X₂
hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ z, z ∈ Z₂ ∧ y < z
y : α
hy : y ∈ Y₁
⊢ ∃ z, (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ y < z

pp: case refine_4.refine_2
α : Type u_1
inst✝ : Preorder α
X₁ Y₁ Z₁ : Multiset α
hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ z, z ∈ Z₁ ∧ y < z
X₂ Y₂ Z₂ : Multiset α
hZ₂ : Z₂ ≠ ∅
hXZXY : Z₁ + X₁ = Y₂ + X₂
hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ z, z ∈ Z₂ ∧ y < z
y : α
hy : y ∈ Y₂ - Z₁
⊢ ∃ z, (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ y < z

Tactic:
·

Goal state after:
case refine_4.refine_1
α : Type u_1
inst✝ : Preorder α
X₁ Y₁ Z₁ : Multiset α
hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ z, z ∈ Z₁ ∧ y < z
X₂ Y₂ Z₂ : Multiset α
hZ₂ : Z₂ ≠ ∅
hXZXY : Z₁ + X₁ = Y₂ + X₂
hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ z, z ∈ Z₂ ∧ y < z
y : α
hy : y ∈ Y₁
⊢ ∃ z, (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ y < z
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: case pos
α : Type u_1
inst✝ : Preorder α
X₁ Y₁ Z₁ : Multiset α
hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ z, z ∈ Z₁ ∧ y < z
X₂ Y₂ Z₂ : Multiset α
hZ₂ : Z₂ ≠ ∅
hXZXY : Z₁ + X₁ = Y₂ + X₂
hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ z, z ∈ Z₂ ∧ y < z
y : α
hy : y ∈ Y₁
z : α
hz : z ∈ Z₁
hyz : y < z
z_in : z ∈ Y₂
⊢ ∃ z, (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ y < z

pp: case neg
α : Type u_1
inst✝ : Preorder α
X₁ Y₁ Z₁ : Multiset α
hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ z, z ∈ Z₁ ∧ y < z
X₂ Y₂ Z₂ : Multiset α
hZ₂ : Z₂ ≠ ∅
hXZXY : Z₁ + X₁ = Y₂ + X₂
hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ z, z ∈ Z₂ ∧ y < z
y : α
hy : y ∈ Y₁
z : α
hz : z ∈ Z₁
hyz : y < z
z_in : ¬z ∈ Y₂
⊢ ∃ z, (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ y < z

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝ : Preorder α
X₁ Y₁ Z₁ : Multiset α
hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ z, z ∈ Z₁ ∧ y < z
X₂ Y₂ Z₂ : Multiset α
hZ₂ : Z₂ ≠ ∅
hXZXY : Z₁ + X₁ = Y₂ + X₂
hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ z, z ∈ Z₂ ∧ y < z
y : α
hy : y ∈ Y₁
z : α
hz : z ∈ Z₁
hyz : y < z
z_in : z ∈ Y₂
⊢ ∃ z, (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ y < z
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: case neg
α : Type u_1
inst✝ : Preorder α
X₁ Y₁ Z₁ : Multiset α
hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ z, z ∈ Z₁ ∧ y < z
X₂ Y₂ Z₂ : Multiset α
hZ₂ : Z₂ ≠ ∅
hXZXY : Z₁ + X₁ = Y₂ + X₂
hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ z, z ∈ Z₂ ∧ y < z
y : α
hy : y ∈ Y₁
z : α
hz : z ∈ Z₁
hyz : y < z
z_in : ¬z ∈ Y₂
⊢ ∃ z, (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ y < z

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝ : Preorder α
X₁ Y₁ Z₁ : Multiset α
hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ z, z ∈ Z₁ ∧ y < z
X₂ Y₂ Z₂ : Multiset α
hZ₂ : Z₂ ≠ ∅
hXZXY : Z₁ + X₁ = Y₂ + X₂
hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ z, z ∈ Z₂ ∧ y < z
y : α
hy : y ∈ Y₁
z : α
hz : z ∈ Z₁
hyz : y < z
z_in : ¬z ∈ Y₂
⊢ ∃ z, (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ y < z
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: case refine_4.refine_2
α : Type u_1
inst✝ : Preorder α
X₁ Y₁ Z₁ : Multiset α
hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ z, z ∈ Z₁ ∧ y < z
X₂ Y₂ Z₂ : Multiset α
hZ₂ : Z₂ ≠ ∅
hXZXY : Z₁ + X₁ = Y₂ + X₂
hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ z, z ∈ Z₂ ∧ y < z
y : α
hy : y ∈ Y₂ - Z₁
⊢ ∃ z, (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ y < z

Tactic:
·

Goal state after:
case refine_4.refine_2
α : Type u_1
inst✝ : Preorder α
X₁ Y₁ Z₁ : Multiset α
hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ z, z ∈ Z₁ ∧ y < z
X₂ Y₂ Z₂ : Multiset α
hZ₂ : Z₂ ≠ ∅
hXZXY : Z₁ + X₁ = Y₂ + X₂
hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ z, z ∈ Z₂ ∧ y < z
y : α
hy : y ∈ Y₂ - Z₁
⊢ ∃ z, (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ y < z
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: case right
α : Type u_1
inst✝ : Preorder α
M N X Y : Multiset α
a : α
M_def : M = X + Y
N_def : N = X + {a}
ys_lt_a : ∀ (y : α), y ∈ Y → y < a
⊢ ∀ (y : α), y ∈ Y → ∃ z, z ∈ {a} ∧ y < z

Tactic:
·

Goal state after:
case right
α : Type u_1
inst✝ : Preorder α
M N X Y : Multiset α
a : α
M_def : M = X + Y
N_def : N = X + {a}
ys_lt_a : ∀ (y : α), y ∈ Y → y < a
⊢ ∀ (y : α), y ∈ Y → ∃ z, z ∈ {a} ∧ y < z
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: case inl
α : Type u_1
inst✝ : Preorder α
M : Multiset α
a : α
X Y : Multiset α
h0 : a ::ₘ M = X + {a}
h2 : ∀ (y : α), y ∈ Y → y < a
⊢ ∃ M', X + Y = a ::ₘ M' ∧ M'.OneStep M ∨ X + Y = M + M' ∧ ∀ (x : α), x ∈ M' → x < a

pp: case inr
α : Type u_1
inst✝ : Preorder α
M : Multiset α
a : α
X Y : Multiset α
b : α
h0 : a ::ₘ M = X + {b}
h2 : ∀ (y : α), y ∈ Y → y < b
hab : a ≠ b
⊢ ∃ M', X + Y = a ::ₘ M' ∧ M'.OneStep M ∨ X + Y = M + M' ∧ ∀ (x : α), x ∈ M' → x < a

Tactic:
·

Goal state after:
case inl
α : Type u_1
inst✝ : Preorder α
M : Multiset α
a : α
X Y : Multiset α
h0 : a ::ₘ M = X + {a}
h2 : ∀ (y : α), y ∈ Y → y < a
⊢ ∃ M', X + Y = a ::ₘ M' ∧ M'.OneStep M ∨ X + Y = M + M' ∧ ∀ (x : α), x ∈ M' → x < a
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: case inr.refine_1
α : Type u_1
inst✝ : Preorder α
M : Multiset α
a : α
X Y : Multiset α
b : α
h0 : a ::ₘ M = X + {b}
h2 : ∀ (y : α), y ∈ Y → y < b
hab : a ≠ b
⊢ X + Y = a ::ₘ (Y + (M - {b}))

pp: case inr.refine_2
α : Type u_1
inst✝ : Preorder α
M : Multiset α
a : α
X Y : Multiset α
b : α
h0 : a ::ₘ M = X + {b}
h2 : ∀ (y : α), y ∈ Y → y < b
hab : a ≠ b
⊢ M = M - {b} + {b}

Tactic:
·

Goal state after:
case inr.refine_1
α : Type u_1
inst✝ : Preorder α
M : Multiset α
a : α
X Y : Multiset α
b : α
h0 : a ::ₘ M = X + {b}
h2 : ∀ (y : α), y ∈ Y → y < b
hab : a ≠ b
⊢ X + Y = a ::ₘ (Y + (M - {b}))
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: case inr.refine_2
α : Type u_1
inst✝ : Preorder α
M : Multiset α
a : α
X Y : Multiset α
b : α
h0 : a ::ₘ M = X + {b}
h2 : ∀ (y : α), y ∈ Y → y < b
hab : a ≠ b
⊢ M = M - {b} + {b}

Tactic:
·

Goal state after:
case inr.refine_2
α : Type u_1
inst✝ : Preorder α
M : Multiset α
a : α
X Y : Multiset α
b : α
h0 : a ::ₘ M = X + {b}
h2 : ∀ (y : α), y ∈ Y → y < b
hab : a ≠ b
⊢ M = M - {b} + {b}
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: case intro.intro.inl
α : Type u_1
inst✝ : Preorder α
a✝ a : α
h✝ : ∀ (y : α), y < a → Acc LT.lt y
ha : ∀ (y : α), y < a → ∀ {M : Multiset α}, Acc OneStep M → Acc OneStep (y ::ₘ M)
M✝ M : Multiset α
hM : ∀ (y : Multiset α), y.OneStep M → Acc OneStep y
ihM : ∀ (y : Multiset α), y.OneStep M → Acc OneStep (a ::ₘ y)
N : Multiset α
hNM' : N.OneStep M
hNM : (a ::ₘ N).OneStep (a ::ₘ M)
⊢ Acc OneStep (a ::ₘ N)

pp: case intro.intro.inr
α : Type u_1
inst✝ : Preorder α
a✝ a : α
h✝ : ∀ (y : α), y < a → Acc LT.lt y
ha : ∀ (y : α), y < a → ∀ {M : Multiset α}, Acc OneStep M → Acc OneStep (y ::ₘ M)
M✝ M : Multiset α
hM : ∀ (y : Multiset α), y.OneStep M → Acc OneStep y
ihM : ∀ (y : Multiset α), y.OneStep M → Acc OneStep (a ::ₘ y)
N : Multiset α
hN : ∀ (x : α), x ∈ N → x < a
hNM : (M + N).OneStep (a ::ₘ M)
⊢ Acc OneStep (M + N)

Tactic:
·

Goal state after:
case intro.intro.inl
α : Type u_1
inst✝ : Preorder α
a✝ a : α
h✝ : ∀ (y : α), y < a → Acc LT.lt y
ha : ∀ (y : α), y < a → ∀ {M : Multiset α}, Acc OneStep M → Acc OneStep (y ::ₘ M)
M✝ M : Multiset α
hM : ∀ (y : Multiset α), y.OneStep M → Acc OneStep y
ihM : ∀ (y : Multiset α), y.OneStep M → Acc OneStep (a ::ₘ y)
N : Multiset α
hNM' : N.OneStep M
hNM : (a ::ₘ N).OneStep (a ::ₘ M)
⊢ Acc OneStep (a ::ₘ N)
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: case cons.inl
α : Type u_1
inst✝ : Preorder α
z : α
M N X Y : Multiset α
hM : M = X + Y
ih :
  ∀ {M N : Multiset α} (X Y : Multiset α),
    0 ≠ ∅ → M = X + Y → N = X + 0 → (∀ (y : α), y ∈ Y → ∃ z, z ∈ 0 ∧ y < z) → TransGen OneStep M N
hZ : z ::ₘ 0 ≠ ∅
hN : N = X + z ::ₘ 0
hYZ : ∀ (y : α), y ∈ Y → ∃ z_1, z_1 ∈ z ::ₘ 0 ∧ y < z_1
⊢ TransGen OneStep M N

pp: case cons.inr
α : Type u_1
inst✝ : Preorder α
z : α
Z : Multiset α
ih :
  ∀ {M N : Multiset α} (X Y : Multiset α),
    Z ≠ ∅ → M = X + Y → N = X + Z → (∀ (y : α), y ∈ Y → ∃ z, z ∈ Z ∧ y < z) → TransGen OneStep M N
M N X Y : Multiset α
hZ✝ : z ::ₘ Z ≠ ∅
hM : M = X + Y
hN : N = X + z ::ₘ Z
hYZ : ∀ (y : α), y ∈ Y → ∃ z_1, z_1 ∈ z ::ₘ Z ∧ y < z_1
hZ : Z ≠ 0
⊢ TransGen OneStep M N

Tactic:
·

Goal state after:
case cons.inl
α : Type u_1
inst✝ : Preorder α
z : α
M N X Y : Multiset α
hM : M = X + Y
ih :
  ∀ {M N : Multiset α} (X Y : Multiset α),
    0 ≠ ∅ → M = X + Y → N = X + 0 → (∀ (y : α), y ∈ Y → ∃ z, z ∈ 0 ∧ y < z) → TransGen OneStep M N
hZ : z ::ₘ 0 ≠ ∅
hN : N = X + z ::ₘ 0
hYZ : ∀ (y : α), y ∈ Y → ∃ z_1, z_1 ∈ z ::ₘ 0 ∧ y < z_1
⊢ TransGen OneStep M N
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
z : α
Z : Multiset α
ih :
  ∀ {M N : Multiset α} (X Y : Multiset α),
    Z ≠ ∅ → M = X + Y → N = X + Z → (∀ (y : α), y ∈ Y → ∃ z, z ∈ Z ∧ y < z) → TransGen OneStep M N
M N X Y : Multiset α
hZ✝ : z ::ₘ Z ≠ ∅
hM : M = X + Y
hN : N = X + z ::ₘ Z
hYZ : ∀ (y : α), y ∈ Y → ∃ z_1, z_1 ∈ z ::ₘ Z ∧ y < z_1
hZ : Z ≠ 0
Y' : Multiset α := filter (fun x ↦ x < z) Y
⊢ ∀ (y : α), y ∈ Y' → y < z

Tactic:
simp [Y']

Goal state after:
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: case cons.inr.refine_1
α : Type u_1
inst✝ : Preorder α
z : α
Z : Multiset α
ih :
  ∀ {M N : Multiset α} (X Y : Multiset α),
    Z ≠ ∅ → M = X + Y → N = X + Z → (∀ (y : α), y ∈ Y → ∃ z, z ∈ Z ∧ y < z) → TransGen OneStep M N
M N X Y : Multiset α
hZ✝ : z ::ₘ Z ≠ ∅
hM : M = X + Y
hN : N = X + z ::ₘ Z
hYZ : ∀ (y : α), y ∈ Y → ∃ z_1, z_1 ∈ z ::ₘ Z ∧ y < z_1
hZ : Z ≠ 0
Y' : Multiset α := filter (fun x ↦ x < z) Y
⊢ M = X + Y' + (Y - Y')

pp: case cons.inr.refine_2
α : Type u_1
inst✝ : Preorder α
z : α
Z : Multiset α
ih :
  ∀ {M N : Multiset α} (X Y : Multiset α),
    Z ≠ ∅ → M = X + Y → N = X + Z → (∀ (y : α), y ∈ Y → ∃ z, z ∈ Z ∧ y < z) → TransGen OneStep M N
M N X Y : Multiset α
hZ✝ : z ::ₘ Z ≠ ∅
hM : M = X + Y
hN : N = X + z ::ₘ Z
hYZ : ∀ (y : α), y ∈ Y → ∃ z_1, z_1 ∈ z ::ₘ Z ∧ y < z_1
hZ : Z ≠ 0
Y' : Multiset α := filter (fun x ↦ x < z) Y
y : α
hy : y ∈ Y - Y'
⊢ ∃ z, z ∈ Z ∧ y < z

Tactic:
·

Goal state after:
case cons.inr.refine_1
α : Type u_1
inst✝ : Preorder α
z : α
Z : Multiset α
ih :
  ∀ {M N : Multiset α} (X Y : Multiset α),
    Z ≠ ∅ → M = X + Y → N = X + Z → (∀ (y : α), y ∈ Y → ∃ z, z ∈ Z ∧ y < z) → TransGen OneStep M N
M N X Y : Multiset α
hZ✝ : z ::ₘ Z ≠ ∅
hM : M = X + Y
hN : N = X + z ::ₘ Z
hYZ : ∀ (y : α), y ∈ Y → ∃ z_1, z_1 ∈ z ::ₘ Z ∧ y < z_1
hZ : Z ≠ 0
Y' : Multiset α := filter (fun x ↦ x < z) Y
⊢ M = X + Y' + (Y - Y')
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: case cons.inr.refine_2
α : Type u_1
inst✝ : Preorder α
z : α
Z : Multiset α
ih :
  ∀ {M N : Multiset α} (X Y : Multiset α),
    Z ≠ ∅ → M = X + Y → N = X + Z → (∀ (y : α), y ∈ Y → ∃ z, z ∈ Z ∧ y < z) → TransGen OneStep M N
M N X Y : Multiset α
hZ✝ : z ::ₘ Z ≠ ∅
hM : M = X + Y
hN : N = X + z ::ₘ Z
hYZ : ∀ (y : α), y ∈ Y → ∃ z_1, z_1 ∈ z ::ₘ Z ∧ y < z_1
hZ : Z ≠ 0
Y' : Multiset α := filter (fun x ↦ x < z) Y
y : α
hy : y ∈ Y - Y'
⊢ ∃ z, z ∈ Z ∧ y < z

Tactic:
·

Goal state after:
case cons.inr.refine_2
α : Type u_1
inst✝ : Preorder α
z : α
Z : Multiset α
ih :
  ∀ {M N : Multiset α} (X Y : Multiset α),
    Z ≠ ∅ → M = X + Y → N = X + Z → (∀ (y : α), y ∈ Y → ∃ z, z ∈ Z ∧ y < z) → TransGen OneStep M N
M N X Y : Multiset α
hZ✝ : z ::ₘ Z ≠ ∅
hM : M = X + Y
hN : N = X + z ::ₘ Z
hYZ : ∀ (y : α), y ∈ Y → ∃ z_1, z_1 ∈ z ::ₘ Z ∧ y < z_1
hZ : Z ≠ 0
Y' : Multiset α := filter (fun x ↦ x < z) Y
y : α
hy : y ∈ Y - Y'
⊢ ∃ z, z ∈ Z ∧ y < z
Module: Mathlib.Data.NNRat.Lemmas

Goal state before:
pp: case inl
q : ℚ
hq : q ≤ 0
⊢ q⁻¹.toNNRat = q.toNNRat⁻¹

pp: case inr
q : ℚ
hq : 0 ≤ q
⊢ q⁻¹.toNNRat = q.toNNRat⁻¹

Tactic:
·

Goal state after:
case inl
q : ℚ
hq : q ≤ 0
⊢ q⁻¹.toNNRat = q.toNNRat⁻¹
Module: Mathlib.Data.NNRat.Lemmas

Goal state before:
pp: case inr
q : ℚ
hq : 0 ≤ q
⊢ q⁻¹.toNNRat = q.toNNRat⁻¹

Tactic:
·

Goal state after:
case inr
q : ℚ
hq : 0 ≤ q
⊢ q⁻¹.toNNRat = q.toNNRat⁻¹
Module: Mathlib.Data.NNRat.Floor

Goal state before:
pp: case inl
K : Type u_1
inst✝³ : Semifield K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorSemiring K
⊢ ⌈↑0⌉₊ = ⌈0⌉₊

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:
·

Goal state after:
case inl
K : Type u_1
inst✝³ : Semifield K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorSemiring K
⊢ ⌈↑0⌉₊ = ⌈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:
·

Goal state after:
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⌉₊
Module: Mathlib.Data.NNRat.Floor

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

pp: case right
K : Type u_1
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
x : ℚ≥0
⊢ ↑x ≤ ↑↑⌈x⌉₊

Tactic:
·

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
Module: Mathlib.Data.NNRat.Floor

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

Tactic:
·

Goal state after:
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.Nat.Prime.Factorial

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

pp: case mpr
m n : ℕ
hm : m ≠ 1
⊢ (∃ p, Prime p ∧ p ∣ m ∧ p ∣ n !) → m.minFac ≤ n

Tactic:
·

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

Goal state before:
pp: case mpr
m n : ℕ
hm : m ≠ 1
⊢ (∃ p, Prime p ∧ p ∣ m ∧ p ∣ n !) → m.minFac ≤ n

Tactic:
·

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

pp: 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]

Tactic:
·

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]
Module: Mathlib.Data.Nat.ChineseRemainder

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

Tactic:
·

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

Goal state before:
pp: A : Type u_1
inst✝ : CommRing A
n p : ℕ
hp : IsNilpotent ↑p
h : p.Coprime n
⊢ IsUnit ↑n

Tactic:
obtain ⟨m, hm⟩ := hp
  suffices ∃ a b : A, p ^ m * a + n * b = 1 by
    obtain ⟨a, b, h⟩ := this
    refine .of_mul_eq_one b ?_
    simpa [hm] using h
  refine ⟨(p ^ m).gcdA n, (p ^ m).gcdB n, ?_⟩
  norm_cast
  rw [← Nat.cast_one, ← Int.cast_natCast 1, ← (h.pow_left m).gcd_eq_one, Nat.gcd_eq_gcd_ab]

Goal state after:
Module: Mathlib.Data.Nat.Factorial.NatCast

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
n✝ p : ℕ
hp : IsNilpotent ↑p
inst✝ : Fact (Nat.Prime p)
n : ℕ
ih : n < p → IsUnit ↑n !
h : n + 1 < p
⊢ n < p

Tactic:
by lia

Goal state after: