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

Goal state before:
pp: case cons
α : Type u
l₂ : List α
h : l₂ ≠ []
head✝ : α
tail✝ : List α
tail_ih✝ : (tail✝ ++ l₂).getLast ⋯ = l₂.getLast h
⊢ (head✝ :: tail✝ ++ l₂).getLast ⋯ = l₂.getLast h

Tactic:
grind

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

Goal state before:
pp: α : Type u
l₂ : List α
h₂ h₁ : l₂ ≠ []
⊢ l₂.getLast h₁ = l₂.getLast h₂

Tactic:
rfl

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

Goal state before:
pp: α : Type u
x : α
hx : x ∈ [].getLast?
⊢ ∃ h, x = [].getLast h

Tactic:
grind

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

Goal state before:
pp: α : Type u
a x : α
hx : x ∈ [a].getLast?
⊢ ∃ h, x = [a].getLast h

Tactic:
grind

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

Goal state before:
pp: α : Type u
a b : α
l : List α
x : α
hx : x ∈ (a :: b :: l).getLast?
⊢ ∃ h, x = (a :: b :: l).getLast h

Tactic:
grind

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

Goal state before:
pp: α : Type u
l₁ l₂ : List α
x : α
h : x ∈ l₂.getLast?
⊢ x ∈ (l₁ ++ l₂).getLast?

Tactic:
grind

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

Goal state before:
pp: α : Type u
l : List α
a d : α
ha : a ∈ l
ha' : a ≠ l.getLastD d
⊢ a ≠ l.getLast ⋯

Tactic:
grind

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

Goal state before:
pp: α : Type u
l : List α
a : α
ha : a ∈ l
ha' : some a ≠ l.getLast?
⊢ a ≠ l.getLast ⋯

Tactic:
grind

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

Goal state before:
pp: case nil
α : Type u
inst✝ : Inhabited α
⊢ [].head! = [].head?.getD default

Tactic:
rfl

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

Goal state before:
pp: case cons
α : Type u
inst✝ : Inhabited α
head✝ : α
tail✝ : List α
⊢ (head✝ :: tail✝).head! = (head✝ :: tail✝).head?.getD default

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: case nil
M : Type u_4
inst✝ : Monoid M
l : List M
hl : ∀ (x : M), x ∈ [] → x = 1
⊢ [].prod = 1

Tactic:
rfl

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

Goal state before:
pp: case cons
α : Type u
inst✝ : Inhabited α
t : List α
head✝ : α
tail✝ : List α
tail_ih✝ : tail✝ ≠ [] → (tail✝ ++ t).head! = tail✝.head!
h : head✝ :: tail✝ ≠ []
⊢ (head✝ :: tail✝ ++ t).head! = (head✝ :: tail✝).head!

Tactic:
rfl

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

Goal state before:
pp: α : Type u
a : α
l : List α
h : l ≠ []
⊢ (l ++ [a]).tail = l.tail ++ [a]

Tactic:
grind

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

Goal state before:
pp: case nil
α : Type u
k : ℕ
h : k ≠ 0
hk : k < [].length
⊢ [][k] ∈ [].tail

Tactic:
grind

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

Goal state before:
pp: case cons
α : Type u
k : ℕ
h : k ≠ 0
head✝ : α
tail✝ : List α
hk : k < (head✝ :: tail✝).length
⊢ (head✝ :: tail✝)[k] ∈ (head✝ :: tail✝).tail

Tactic:
grind

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

Goal state before:
pp: α : Type u
l₁ l₂ : List α
a b : α
⊢ a :: l₁ <+ b :: l₂ ↔ a :: l₁ <+ l₂ ∨ a = b ∧ l₁ <+ l₂

Tactic:
grind

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

Goal state before:
pp: α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
⊢ idxOf a l = l.length ↔ ¬a ∈ l

Tactic:
grind

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

Goal state before:
pp: case cons
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a head✝ : α
tail✝ : List α
⊢ idxOf a (head✝ :: tail✝) = 0 ↔ head✝ :: tail✝ = [] ∨ (head✝ :: tail✝).head? = some a

Tactic:
grind

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

Goal state before:
pp: α : Type u
l₁ l₂ : List α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
h : a ∈ l₁
⊢ idxOf a (l₁ ++ l₂) = idxOf a l₁

Tactic:
grind

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

Goal state before:
pp: α : Type u
l₁ l₂ : List α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
h : ¬a ∈ l₁
⊢ idxOf a (l₁ ++ l₂) = l₁.length + idxOf a l₂

Tactic:
grind

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

Goal state before:
pp: α : Type u
l₁ : List α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l₃ : List α
⊢ idxOf a l₁ ≤ idxOf a (l₁ ++ l₃)

Tactic:
grind

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

Goal state before:
pp: α : Type u
l₁ : List α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l₃ : List α
⊢ idxOf a (l₃ ++ l₁) ≤ (l₃ ++ l₁).length - l₁.length + idxOf a l₁

Tactic:
grind

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

Goal state before:
pp: α : Type u
l₁ : List α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l₃ : List α
⊢ idxOf a (l₃ ++ l₁) + l₁.length ≤ idxOf a l₁ + (l₃ ++ l₁).length

Tactic:
grind

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

Goal state before:
pp: α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
n : ℕ
l : List α
ha : a ∈ l
⊢ idxOf a l < (take n l).length ↔ idxOf a l < n

Tactic:
grind

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
a : M
l : List M
hlen : 0 ≤ l.length
hcomm : ∀ (a' : M), a' ∈ take 0 l → Commute a a'
⊢ (l.insertIdx 0 a).prod = a * l.prod

Tactic:
rfl

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

Goal state before:
pp: α : Type u
l₁ l₂ : List α
h' : ∀ (n : ℕ), n < max l₁.length l₂.length → l₁[n]? = l₂[n]?
⊢ ∀ (i : ℕ), l₁[i]? = l₂[i]?

Tactic:
grind

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
l : List M
i : ℕ
hlen : i < l.length
hcomm : ∀ (a' : M), a' ∈ take i l → Commute l[i] a'
⊢ i ≤ (l.eraseIdx i).length

Tactic:
grind

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: case nil
M : Type u_4
inst✝² : Monoid M
inst✝¹ : BEq M
inst✝ : LawfulBEq M
⊢ (filter (fun x ↦ x != 1) []).prod = [].prod

Tactic:
grind

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: case cons
M : Type u_4
inst✝² : Monoid M
inst✝¹ : BEq M
inst✝ : LawfulBEq M
head✝ : M
tail✝ : List M
tail_ih✝ : (filter (fun x ↦ x != 1) tail✝).prod = tail✝.prod
⊢ (filter (fun x ↦ x != 1) (head✝ :: tail✝)).prod = (head✝ :: tail✝).prod

Tactic:
grind

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

Goal state before:
pp: α : Type u
l₁ : List α
n✝ : ℕ
a✝ : n✝ < max l₁.length l₁.length
⊢ l₁[n✝]? = l₁[n✝]?

Tactic:
rfl

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

Goal state before:
pp: α : Type u
l : List α
h : l.length = 1
⊢ ∀ (n : ℕ) (h₁ : n < l.length) (h₂ : n < [l.get ⟨0, ⋯⟩].length), l.get ⟨n, h₁⟩ = [l.get ⟨0, ⋯⟩].get ⟨n, h₂⟩

Tactic:
grind

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
h : Injective (map f)
x y : α
hxy : f x = f y
⊢ map f [x] = map f [y]

Tactic:
simp [hxy]

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

Goal state before:
pp: case nil
α : Type u
β : Type v
f g : α → β → α
a : α
H : ∀ (a : α) (b : β), b ∈ [] → f a b = g a b
⊢ foldl f a [] = foldl g a []

Tactic:
rfl

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

Goal state before:
pp: case cons
α : Type u
β : Type v
f g : α → β → α
hd : β
tl : List β
ih : ∀ (a : α), (∀ (a : α) (b : β), b ∈ tl → f a b = g a b) → foldl f a tl = foldl g a tl
a : α
H : ∀ (a : α) (b : β), b ∈ hd :: tl → f a b = g a b
⊢ foldl f a (hd :: tl) = foldl g a (hd :: tl)

Tactic:
| cons hd tl ih =>

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

Goal state before:
pp: case nil
α : Type u
β : Type v
f g : α → β → β
b : β
H : ∀ (a : α), a ∈ [] → ∀ (b : β), f a b = g a b
⊢ foldr f b [] = foldr g b []

Tactic:
rfl

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

Goal state before:
pp: case cons
α : Type u
β : Type v
f g : α → β → β
b : β
hd : α
tl : List α
ih : (∀ (a : α), a ∈ tl → ∀ (b : β), f a b = g a b) → foldr f b tl = foldr g b tl
H : ∀ (a : α), a ∈ hd :: tl → ∀ (b : β), f a b = g a b
⊢ foldr f b (hd :: tl) = foldr g b (hd :: tl)

Tactic:
| cons hd tl ih =>

Goal state after:
case cons
α : Type u
β : Type v
f g : α → β → β
b : β
hd : α
tl : List α
ih : (∀ (a : α), a ∈ tl → ∀ (b : β), f a b = g a b) → foldr f b tl = foldr g b tl
H : ∀ (a : α), a ∈ hd :: tl → ∀ (b : β), f a b = g a b
⊢ foldr f b (hd :: tl) = foldr g b (hd :: tl)
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: case cons
G : Type u_7
inst✝¹ : CommGroup G
A : Type u_8
inst✝ : DecidableEq A
f g : A → G
a x : A
xs : List A
⊢ (if x = a then f x else g x) * ((f a / g a) ^ count a xs * (map g xs).prod) =
    (f a / g a) ^ (count a xs + if (x == a) = true then 1 else 0) * (g x * (map g xs).prod)

Tactic:
by_cases hx : x = a

Goal state after:
case pos
G : Type u_7
inst✝¹ : CommGroup G
A : Type u_8
inst✝ : DecidableEq A
f g : A → G
a x : A
xs : List A
hx : x = a
⊢ (if x = a then f x else g x) * ((f a / g a) ^ count a xs * (map g xs).prod) =
    (f a / g a) ^ (count a xs + if (x == a) = true then 1 else 0) * (g x * (map g xs).prod)

case neg
G : Type u_7
inst✝¹ : CommGroup G
A : Type u_8
inst✝ : DecidableEq A
f g : A → G
a x : A
xs : List A
hx : ¬x = a
⊢ (if x = a then f x else g x) * ((f a / g a) ^ count a xs * (map g xs).prod) =
    (f a / g a) ^ (count a xs + if (x == a) = true then 1 else 0) * (g x * (map g xs).prod)
Module: Mathlib.Data.List.Basic

Goal state before:
pp: case nil
ι : Type u_1
α : Type u
β : Type v
γ : Type w
f : α → β → γ
op₁ : α → ι → α
op₂ : β → ι → β
op₃ : γ → ι → γ
h : ∀ (a : α) (b : β) (i : ι), f (op₁ a i) (op₂ b i) = op₃ (f a b) i
a✝ : α
b✝ : β
⊢ f (foldl op₁ a✝ []) (foldl op₂ b✝ []) = foldl op₃ (f a✝ b✝) []

Tactic:
rfl

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

Goal state before:
pp: case nil
ι : Type u_1
α : Type u
β : Type v
γ : Type w
f : α → β → γ
op₁ : ι → α → α
op₂ : ι → β → β
op₃ : ι → γ → γ
b : β
h : ∀ (a : α) (b : β) (i : ι), f (op₁ i a) (op₂ i b) = op₃ i (f a b)
a✝ : α
⊢ foldr op₃ (f a✝ b) [] = f (foldr op₁ a✝ []) (foldr op₂ b [])

Tactic:
rfl

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

Goal state before:
pp: case mpr
α : Type u
x₁ z₁ : List α
a₁ : α
notin_x : ¬a₁ ∈ x₁
notin_z : ¬a₁ ∈ z₁
⊢ x₁ ++ a₁ :: z₁ = x₁ ++ a₁ :: z₁

Tactic:
rfl

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

Goal state before:
pp: α : Type u
β : Type v
f : α → Option β
g : α → β
a : α
l : List α
ih : filterMap f l = map g l → ∀ (x : α), x ∈ l → f x = some (g x)
ha : f a = none
h : filterMap f (a :: l) = map g (a :: l)
⊢ (filterMap f l).length = l.length + 1

Tactic:
grind

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

Goal state before:
pp: case cons.none
α : Type u
β : Type v
f : α → Option β
g : α → β
a : α
l : List α
ih : filterMap f l = map g l → ∀ (x : α), x ∈ l → f x = some (g x)
ha : f a = none
h : filterMap f (a :: l) = map g (a :: l)
this : (filterMap f l).length = l.length + 1
⊢ ∀ (x : α), x ∈ a :: l → f x = some (g x)

Tactic:
grind

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

Goal state before:
pp: case cons
α : Type u
p : α → Bool
head✝ : α
tail✝ : List α
tail_ih✝ : filter p tail✝ = foldr (fun a out ↦ bif p a then a :: out else out) [] tail✝
⊢ (match p head✝ with
    | true => head✝ :: foldr (fun a out ↦ bif p a then a :: out else out) [] tail✝
    | false => foldr (fun a out ↦ bif p a then a :: out else out) [] tail✝) =
    bif p head✝ then head✝ :: foldr (fun a out ↦ bif p a then a :: out else out) [] tail✝
    else foldr (fun a out ↦ bif p a then a :: out else out) [] tail✝

Tactic:
rfl

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

Goal state before:
pp: case nil
α : Type u
p q : α → Bool
h : ∀ (a : α), p a = true → q a = true
⊢ filter p [] <+ filter q []

Tactic:
grind

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

Goal state before:
pp: case cons
α : Type u
p q : α → Bool
h : ∀ (a : α), p a = true → q a = true
head✝ : α
tail✝ : List α
tail_ih✝ : filter p tail✝ <+ filter q tail✝
⊢ filter p (head✝ :: tail✝) <+ filter q (head✝ :: tail✝)

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Rat.Defs

Goal state before:
pp: q✝ a b c : ℚ
n : ℕ
q : ℚ
⊢ ↑↑n * q + q = n • q + q

Tactic:
rfl

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

Goal state before:
pp: α : Type u
p : α → Bool
l : List α
a : α
al : a ∈ l
pa : p a = true
⊢ (eraseP p l).length + 1 = l.length

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Rat.Defs

Goal state before:
pp: q a b c : ℚ
x✝¹ : ℕ
x✝ : ℚ
⊢ -(↑(↑x✝¹ + 1) * x✝) = -(↑↑x✝¹.succ * x✝)

Tactic:
rfl

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

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : BEq α
inst✝² : LawfulBEq α
inst✝¹ : BEq β
inst✝ : LawfulBEq β
f : α → β
finj : Injective f
a : α
l : List α
this : (fun x ↦ a == x) = fun x ↦ f a == f x
⊢ map f (eraseP (fun x ↦ f a == f x) l) = map f (eraseP ((fun x ↦ f a == x) ∘ f) l)

Tactic:
rfl

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

Goal state before:
pp: case nil
α : Type u
β : Type v
inst✝³ : BEq α
inst✝² : LawfulBEq α
inst✝¹ : BEq β
inst✝ : LawfulBEq β
f : α → β
finj : Injective f
l₁ : List α
⊢ map f (foldl List.erase l₁ []) = foldl (fun l a ↦ l.erase (f a)) (map f l₁) []

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Rat.Defs

Goal state before:
pp: q : ℚ
hq : q.den = 1
⊢ q.num /. 1 = q.num /. ↑1

Tactic:
rfl

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

Goal state before:
pp: case cons.zero
ι : Type u_1
inst✝¹ : BEq ι
inst✝ : LawfulBEq ι
a : ι
l : List ι
IH : ∀ {i : ℕ} (hi : i < l.length), l.erase l[i] ~ l.eraseIdx i
hi : 0 < (a :: l).length
⊢ (a :: l).erase (a :: l)[0] ~ (a :: l).eraseIdx 0

Tactic:
grind

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

Goal state before:
pp: case cons.succ
ι : Type u_1
inst✝¹ : BEq ι
inst✝ : LawfulBEq ι
a : ι
l : List ι
IH : ∀ {i : ℕ} (hi : i < l.length), l.erase l[i] ~ l.eraseIdx i
n✝ : ℕ
hi : n✝ + 1 < (a :: l).length
⊢ (a :: l).erase (a :: l)[n✝ + 1] ~ (a :: l).eraseIdx (n✝ + 1)

Tactic:
grind

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

Goal state before:
pp: ι : Type u_1
l : List ι
i : ℕ
h : i < l.length
⊢ (l.eraseIdx i).length + 1 = l.length

Tactic:
grind

Goal state after:
Module: Mathlib.Algebra.Ring.Rat

Goal state before:
pp: r : ℚ
⊢ ↑r.num / ↑r.den = r

Tactic:
← Int.cast_natCast,

Goal state after:
r : ℚ
⊢ ↑r.num / ↑↑r.den = r
Module: Mathlib.Algebra.Ring.Rat

Goal state before:
pp: n : ℕ
⊢ ↑n = ↑n /. 1

Tactic:
← Int.cast_natCast,

Goal state after:
n : ℕ
⊢ ↑↑n = ↑n /. 1
Module: Mathlib.Data.List.Basic

Goal state before:
pp: case nil
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
f : α → β
a : α
h : a ∈ []
⊢ lookup a (map (fun x ↦ (x, f x)) []) = some (f a)

Tactic:
grind

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

Goal state before:
pp: case cons
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
f : α → β
a head✝ : α
tail✝ : List α
tail_ih✝ : a ∈ tail✝ → lookup a (map (fun x ↦ (x, f x)) tail✝) = some (f a)
h : a ∈ head✝ :: tail✝
⊢ lookup a (map (fun x ↦ (x, f x)) (head✝ :: tail✝)) = some (f a)

Tactic:
grind

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

Goal state before:
pp: n : ℕ
⊢ ↑n = ↑↑n

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Group.Semiconj.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a x y : G
⊢ SemiconjBy a x⁻¹ y⁻¹ ↔ SemiconjBy a x y

Tactic:
by
  rw [← inv_symm_left_iff, inv_inv_symm_iff]

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

Goal state before:
pp: q : ℚ≥0
⊢ ↑q * ↑q.den = ↑q.num

Tactic:
← Int.cast_natCast,

Goal state after:
q : ℚ≥0
⊢ ↑q * ↑↑q.den = ↑q.num
Module: Mathlib.Algebra.GroupWithZero.Divisibility

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
a : α
inst✝ : Subsingleton αˣ
c d : α
hcd : c = 1 ∧ d = 1 ∨ a = 0
⊢ a = a * c

Tactic:
obtain ⟨rfl, -⟩ | rfl := hcd

Goal state after:
case inl
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
a : α
inst✝ : Subsingleton αˣ
d : α
⊢ a = a * 1

case inr
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : Subsingleton αˣ
c d : α
⊢ 0 = 0 * c
Module: Mathlib.Data.PNat.Defs

Goal state before:
pp: m : ℕ
⊢ ↑(m + 1).toPNat' = m + 1

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.PNat.Defs

Goal state before:
pp: case zero
m k : ℕ+
⊢ ↑(k.modDivAux 0 (↑m / ↑k)).fst = ↑k

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.PNat.Defs

Goal state before:
pp: case succ
m k : ℕ+
n : ℕ
⊢ ↑(k.modDivAux (n + 1) (↑m / ↑k)).fst = n + 1

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.PNat.Defs

Goal state before:
pp: case zero
m k : ℕ+
⊢ (k.modDivAux 0 (↑m / ↑k)).snd = ↑m / ↑k - 1

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.PNat.Defs

Goal state before:
pp: case succ
m k : ℕ+
n : ℕ
⊢ (k.modDivAux (n + 1) (↑m / ↑k)).snd = ↑m / ↑k

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Rat.Cast.CharZero

Goal state before:
pp: α : Type u_3
inst✝¹ : DivisionRing α
inst✝ : CharZero α
a b : ℤ
⊢ ↑(a /. b) = ↑a / ↑b

Tactic:
simp only [divInt_eq_div, cast_div, cast_intCast]

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

Goal state before:
pp: q : ℚ
⊢ q.num * q.num / 1 = q.num * q.num

pp: q : ℚ
⊢ (q.num.natAbs * q.num.natAbs).Coprime (q.den * q.den)

Tactic:
Int.ediv_one

Goal state after:
q : ℚ
⊢ q.num * q.num = q.num * q.num

q : ℚ
⊢ (q.num.natAbs * q.num.natAbs).Coprime (q.den * q.den)
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: q r : ℚ
hqd : ↑q.den ≠ 0
hrd : ↑r.den ≠ 0
⊢ (q.num * ↑r.den + r.num * ↑q.den) /. (↑q.den * ↑r.den) = (q.num * ↑r.den + ↑q.den * r.num) /. (↑q.den * ↑r.den)

Tactic:
mul_comm r.num q.den

Goal state after:
q r : ℚ
hqd : ↑q.den ≠ 0
hrd : ↑r.den ≠ 0
⊢ (q.num * ↑r.den + ↑q.den * r.num) /. (↑q.den * ↑r.den) = (q.num * ↑r.den + ↑q.den * r.num) /. (↑q.den * ↑r.den)
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ (↑q.num * ↑r.den + ↑q.den * ↑r.num) / (↑q.den * ↑r.den) = (↑q.num * ↑r.den + ↑q.den * ↑r.num) / (↑q.den * ↑r.den)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑q.num * ↑r.num / (↑q.den * ↑r.den) = ↑q.num * ↑r.num / (↑q.den * ↑r.den)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.num ≠ 0
⊢ ↑q.num * ↑r.den / (↑q.den * ↑r.num) = ↑q.num * ↑r.den / (↑q.den * ↑r.num)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: α : Type u_3
inst✝ : DivisionRing α
n : ℕ
⊢ ↑↑n = ↑n

Tactic:
← Int.cast_natCast,

Goal state after:
α : Type u_3
inst✝ : DivisionRing α
n : ℕ
⊢ ↑↑↑n = ↑n
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: α : Type u_3
inst✝¹ : DivisionRing α
n : ℕ
inst✝ : n.AtLeastTwo
⊢ ↑(OfNat.ofNat n) = OfNat.ofNat n

Tactic:
by
  simp [cast_def]

Goal state after:
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: α : Type u_3
inst✝ : DivisionRing α
q r : ℚ
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ (↑q.num * ↑r.den + ↑q.den * ↑r.num) / (↑q.den * ↑r.den) = (↑q.num * ↑r.den + ↑q.den * ↑r.num) / (↑q.den * ↑r.den)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: α : Type u_3
inst✝ : DivisionRing α
p q : ℚ
hp : ↑p.den ≠ 0
hq : ↑q.den ≠ 0
⊢ ↑p.num * ↑q.num / (↑p.den * ↑q.den) = ↑p.num * ↑q.num / (↑p.den * ↑q.den)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: α : Type u_3
inst✝ : DivisionRing α
p q : ℚ
hp : ↑p.den ≠ 0
hq : ↑q.num ≠ 0
⊢ ↑p.num * ↑q.den / (↑p.den * ↑q.num) = ↑p.num * ↑q.den / (↑p.den * ↑q.num)

Tactic:
rfl

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

Goal state before:
pp: a : ℤ
ha0 : 0 < a
⊢ ↑(if a = 0 then 1 else a.natAbs) = a

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: F : Type u_1
M₀ : Type u_5
inst✝² : MonoidWithZero M₀
inst✝¹ : FunLike F ℚ M₀
inst✝ : MonoidWithZeroHomClass F ℚ M₀
f g : F
h : ∀ (m : ℤ), f ↑m = g ↑m
r : ℚ
⊢ g ↑r.num * f (↑r.den)⁻¹ = g ↑r.num * g (↑r.den)⁻¹

Tactic:
← Int.cast_natCast,

Goal state after:
F : Type u_1
M₀ : Type u_5
inst✝² : MonoidWithZero M₀
inst✝¹ : FunLike F ℚ M₀
inst✝ : MonoidWithZeroHomClass F ℚ M₀
f g : F
h : ∀ (m : ℤ), f ↑m = g ↑m
r : ℚ
⊢ g ↑r.num * f (↑↑r.den)⁻¹ = g ↑r.num * g (↑↑r.den)⁻¹
Module: Mathlib.Tactic.Ring.Basic

Goal state before:
pp: n d : ℕ
R : Type u_2
inst✝ : DivisionSemiring R
a : R
inv✝ : Invertible ↑d
e : a = ↑n * ⅟↑d
⊢ a = NNRat.rawCast n d + 0

Tactic:
by simp [e, div_eq_mul_inv]

Goal state after:
Module: Mathlib.Tactic.Ring.Basic

Goal state before:
pp: n : ℤ
d : ℕ
R : Type u_2
inst✝ : DivisionRing R
a : R
inv✝ : Invertible ↑d
e : a = ↑n * ⅟↑d
⊢ a = Rat.rawCast n d + 0

Tactic:
by simp [e, div_eq_mul_inv]

Goal state after:
Module: Mathlib.Tactic.Ring.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Mul α
a b : α
⊢ a • b = a * b

Tactic:
rfl

Goal state after:
Module: Mathlib.Tactic.Ring.Basic

Goal state before:
pp: α : Sort u_2
c : α
⊢ c = c

Tactic:
rfl

Goal state after:
Module: Mathlib.Tactic.CancelDenoms.Core

Goal state before:
pp: α : Type u_1
inst✝ : Field α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : ad ≠ 0
hbd : bd ≠ 0
hgcd : gcd ≠ 0
⊢ (a = b) = (1 / gcd * (bd * a') = 1 / gcd * (ad * b'))

Tactic:
grind

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Canonical

Goal state before:
pp: R : Type u
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : CanonicallyOrderedAdd R
inst✝ : Nontrivial R
a : R
⊢ Odd a → 0 < a

Tactic:
by
  rintro ⟨k, rfl⟩; simp

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a' b' : R
⊢ a' + b' = a' + b'

Tactic:
rfl

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a' b' : R
⊢ a' * b' = a' * b'

Tactic:
rfl

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
b' : R
a' : ℕ
⊢ a' • b' = a' • b'

Tactic:
rfl

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
b' : R
a' : ℤ
⊢ a' • b' = a' • b'

Tactic:
rfl

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a' : R
b' : ℕ
⊢ a' ^ b' = a' ^ b'

Tactic:
rfl

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
a' : R
⊢ -a' = -a'

Tactic:
rfl

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
a' b' : R
⊢ a' - b' = a' - b'

Tactic:
rfl

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_2
inst✝ : Semifield R
a' : R
⊢ a'⁻¹ = a'⁻¹

Tactic:
rfl

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_2
inst✝ : Semifield R
a' b' : R
⊢ a' / b' = a' / b'

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Bool.Set

Goal state before:
pp: ⊢ univ = {false, true}

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Nat.Set

Goal state before:
pp: case e'_4.zero
α : Type u_2
x : α
f : ℕ → α → α
⊢ rec (f 0 x) (f ∘ succ) 0 = f 0 (rec x f 0)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Nat.Set

Goal state before:
pp: case e'_4.succ
α : Type u_2
x : α
f : ℕ → α → α
n : ℕ
ihn : rec (f 0 x) (f ∘ succ) n = f n (rec x f n)
⊢ f (n + 1) (rec (f 0 x) (f ∘ succ) n) = f (n + 1) (f n (rec x f n))

Tactic:
rw [ihn]

Goal state after:
Module: Mathlib.Order.CompleteLattice.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
a b : α
c d : Set α
hs : ∀ e ∈ c, e ≤ a
ht : ∀ e ∈ d, e ≤ b
hd : Disjoint a b
he : ⊥ ∉ c ∨ ⊥ ∉ d
⊢ Disjoint c d

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: γ : Type u_3
ι : Sort u_5
κ : ι → Sort u_8
x : γ
s : (i : ι) → κ i → Set γ
⊢ x ∈ ⋂ i, ⋂ j, s i j ↔ ∀ (i : ι) (j : κ i), x ∈ s i j

Tactic:
simp_rw [mem_iInter]

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
S : Set (Set α)
h : S ⊆ {∅, univ}
⊢ ⋃₀ S ∈ {∅, univ}

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
S : Set (Set α)
⊢ ⋃₀ S = (⋂₀ (compl '' S))ᶜ

Tactic:
rw [← compl_compl (⋃₀ S), compl_sUnion]

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: ι : Type u_12
σ : ι → Type u_13
s : Set (Sigma σ)
x : (i : ι) × σ i
⊢ (∃ i x_1, ⟨i, x_1⟩ ∈ s ∧ ⟨i, x_1⟩ = x) ↔ x ∈ s

Tactic:
grind

Goal state after: