mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: case nil
M : Type u_4
inst✝ : Monoid M
⊢ [][0]?.getD 1 * [].tail.prod = [].prod

pp: case cons
M : Type u_4
inst✝ : Monoid M
head✝ : M
tail✝ : List M
⊢ (head✝ :: tail✝)[0]?.getD 1 * (head✝ :: tail✝).tail.prod = (head✝ :: tail✝).prod

Tactic:
<;>

Goal state after:
case nil
M : Type u_4
inst✝ : Monoid M
⊢ [][0]?.getD 1 * [].tail.prod = [].prod

case cons
M : Type u_4
inst✝ : Monoid M
head✝ : M
tail✝ : List M
⊢ (head✝ :: tail✝)[0]?.getD 1 * (head✝ :: tail✝).tail.prod = (head✝ :: tail✝).prod
Module: Mathlib.Data.List.Basic

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

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

Tactic:
<;>

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

case cons
α : Type u
inst✝ : Inhabited α
head✝ : α
tail✝ : List α
⊢ (head✝ :: tail✝).head! = (head✝ :: tail✝).head?.getD default
Module: Mathlib.Data.List.Basic

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

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

Tactic:
<;>

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

case cons
α : Type u
k : ℕ
h : k ≠ 0
head✝ : α
tail✝ : List α
hk : k < (head✝ :: tail✝).length
⊢ (head✝ :: tail✝)[k] ∈ (head✝ :: tail✝).tail
Module: Mathlib.Data.List.Basic

Goal state before:
pp: case mp
α : Type u
l : List α
a : α
⊢ l <+ [a] → l = [] ∨ l = [a]

pp: case mpr
α : Type u
l : List α
a : α
⊢ l = [] ∨ l = [a] → l <+ [a]

Tactic:
<;>

Goal state after:
case mp
α : Type u
l : List α
a : α
⊢ l <+ [a] → l = [] ∨ l = [a]

case mpr
α : Type u
l : List α
a : α
⊢ l = [] ∨ l = [a] → l <+ [a]
Module: Mathlib.Data.List.Basic

Goal state before:
pp: case mp.cons
α : Type u
l : List α
a : α
a✝ : l <+ []
⊢ l = [] ∨ l = [a]

pp: case mp.cons_cons
α : Type u
a : α
l₁✝ : List α
a✝ : l₁✝ <+ []
⊢ a :: l₁✝ = [] ∨ a :: l₁✝ = [a]

pp: case mpr.inl
α : Type u
l : List α
a : α
h✝ : l = []
⊢ l <+ [a]

pp: case mpr.inr
α : Type u
l : List α
a : α
h✝ : l = [a]
⊢ l <+ [a]

Tactic:
<;>

Goal state after:
case mp.cons
α : Type u
l : List α
a : α
a✝ : l <+ []
⊢ l = [] ∨ l = [a]

case mp.cons_cons
α : Type u
a : α
l₁✝ : List α
a✝ : l₁✝ <+ []
⊢ a :: l₁✝ = [] ∨ a :: l₁✝ = [a]

case mpr.inl
α : Type u
l : List α
a : α
h✝ : l = []
⊢ l <+ [a]

case mpr.inr
α : Type u
l : List α
a : α
h✝ : l = [a]
⊢ l <+ [a]
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

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

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

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
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) []

pp: case cons
ι : 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
head✝ : ι
tail✝ : List ι
tail_ih✝ : ∀ (a : α) (b : β), f (foldl op₁ a tail✝) (foldl op₂ b tail✝) = foldl op₃ (f a b) tail✝
⊢ ∀ (a : α) (b : β),
    f (foldl op₁ a (head✝ :: tail✝)) (foldl op₂ b (head✝ :: tail✝)) = foldl op₃ (f a b) (head✝ :: tail✝)

Tactic:
<;>

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

case cons
ι : 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
head✝ : ι
tail✝ : List ι
tail_ih✝ : ∀ (a : α) (b : β), f (foldl op₁ a tail✝) (foldl op₂ b tail✝) = foldl op₃ (f a b) tail✝
⊢ ∀ (a : α) (b : β),
    f (foldl op₁ a (head✝ :: tail✝)) (foldl op₂ b (head✝ :: tail✝)) = foldl op₃ (f a b) (head✝ :: tail✝)
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 [])

pp: case cons
ι : 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)
head✝ : ι
tail✝ : List ι
tail_ih✝ : ∀ (a : α), foldr op₃ (f a b) tail✝ = f (foldr op₁ a tail✝) (foldr op₂ b tail✝)
⊢ ∀ (a : α), foldr op₃ (f a b) (head✝ :: tail✝) = f (foldr op₁ a (head✝ :: tail✝)) (foldr op₂ b (head✝ :: tail✝))

Tactic:
<;>

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

case cons
ι : 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)
head✝ : ι
tail✝ : List ι
tail_ih✝ : ∀ (a : α), foldr op₃ (f a b) tail✝ = f (foldr op₁ a tail✝) (foldr op₂ b tail✝)
⊢ ∀ (a : α), foldr op₃ (f a b) (head✝ :: tail✝) = f (foldr op₁ a (head✝ :: tail✝)) (foldr op₂ b (head✝ :: tail✝))
Module: Mathlib.Data.List.Basic

Goal state before:
pp: case mp.inl.inl
α : Type u
x₁ z₂ : List α
a₂ : α
notin_x : ¬a₂ ∈ x₁
notin_z : ¬a₂ ∈ z₂
⊢ x₁ = x₁ ++ [] ∧ a₂ = a₂ ∧ z₂ = z₂

pp: case mp.inl.inr
α : Type u
x₁ z₂ : List α
a₁ a₂ : α
notin_x : ¬a₂ ∈ x₁
d : List α
notin_z : ¬a₂ ∈ d ++ a₂ :: z₂
⊢ x₁ = x₁ ++ a₁ :: d ∧ a₁ = a₂ ∧ d ++ a₂ :: z₂ = z₂

pp: case mp.inr.inl
α : Type u
x₂ z₁ : List α
a₁ : α
notin_z : ¬a₁ ∈ z₁
notin_x : ¬a₁ ∈ x₂ ++ []
⊢ x₂ ++ [] = x₂ ∧ a₁ = a₁ ∧ z₁ = z₁

pp: case mp.inr.inr
α : Type u
x₂ z₁ : List α
a₁ a₂ : α
notin_z : ¬a₂ ∈ z₁
d : List α
notin_x : ¬a₂ ∈ x₂ ++ a₂ :: d
⊢ x₂ ++ a₂ :: d = x₂ ∧ a₁ = a₂ ∧ z₁ = d ++ a₁ :: z₁

Tactic:
<;>

Goal state after:
case mp.inl.inl
α : Type u
x₁ z₂ : List α
a₂ : α
notin_x : ¬a₂ ∈ x₁
notin_z : ¬a₂ ∈ z₂
⊢ x₁ = x₁ ++ [] ∧ a₂ = a₂ ∧ z₂ = z₂

case mp.inl.inr
α : Type u
x₁ z₂ : List α
a₁ a₂ : α
notin_x : ¬a₂ ∈ x₁
d : List α
notin_z : ¬a₂ ∈ d ++ a₂ :: z₂
⊢ x₁ = x₁ ++ a₁ :: d ∧ a₁ = a₂ ∧ d ++ a₂ :: z₂ = z₂

case mp.inr.inl
α : Type u
x₂ z₁ : List α
a₁ : α
notin_z : ¬a₁ ∈ z₁
notin_x : ¬a₁ ∈ x₂ ++ []
⊢ x₂ ++ [] = x₂ ∧ a₁ = a₁ ∧ z₁ = z₁

case mp.inr.inr
α : Type u
x₂ z₁ : List α
a₁ a₂ : α
notin_z : ¬a₂ ∈ z₁
d : List α
notin_x : ¬a₂ ∈ x₂ ++ a₂ :: d
⊢ x₂ ++ a₂ :: d = x₂ ∧ a₁ = a₂ ∧ z₁ = d ++ a₁ :: z₁
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: case nil
⊢ [].headI + [].tail.sum = [].sum

pp: case cons
head✝ : ℕ
tail✝ : List ℕ
⊢ (head✝ :: tail✝).headI + (head✝ :: tail✝).tail.sum = (head✝ :: tail✝).sum

Tactic:
<;>

Goal state after:
case nil
⊢ [].headI + [].tail.sum = [].sum

case cons
head✝ : ℕ
tail✝ : List ℕ
⊢ (head✝ :: tail✝).headI + (head✝ :: tail✝).tail.sum = (head✝ :: tail✝).sum
Module: Mathlib.Data.List.Basic

Goal state before:
pp: case nil
α : Type u
β : Type v
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m β
b : β
⊢ foldrM f b [] = foldr (fun a mb ↦ mb >>= f a) (pure b) []

pp: case cons
α : Type u
β : Type v
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m β
b : β
head✝ : α
tail✝ : List α
tail_ih✝ : foldrM f b tail✝ = foldr (fun a mb ↦ mb >>= f a) (pure b) tail✝
⊢ foldrM f b (head✝ :: tail✝) = foldr (fun a mb ↦ mb >>= f a) (pure b) (head✝ :: tail✝)

Tactic:
<;>

Goal state after:
case nil
α : Type u
β : Type v
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m β
b : β
⊢ foldrM f b [] = foldr (fun a mb ↦ mb >>= f a) (pure b) []

case cons
α : Type u
β : Type v
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m β
b : β
head✝ : α
tail✝ : List α
tail_ih✝ : foldrM f b tail✝ = foldr (fun a mb ↦ mb >>= f a) (pure b) tail✝
⊢ foldrM f b (head✝ :: tail✝) = foldr (fun a mb ↦ mb >>= f a) (pure b) (head✝ :: tail✝)
Module: Mathlib.Data.List.Basic

Goal state before:
pp: case nil
α : Type u
β : Type v
f : α → Option β
⊢ filterMap f [] = flatMap (fun a ↦ (f a).toList) []

pp: case cons
α : Type u
β : Type v
f : α → Option β
a : α
l : List α
ih : filterMap f l = flatMap (fun a ↦ (f a).toList) l
⊢ filterMap f (a :: l) = flatMap (fun a ↦ (f a).toList) (a :: l)

Tactic:
<;>

Goal state after:
case nil
α : Type u
β : Type v
f : α → Option β
⊢ filterMap f [] = flatMap (fun a ↦ (f a).toList) []

case cons
α : Type u
β : Type v
f : α → Option β
a : α
l : List α
ih : filterMap f l = flatMap (fun a ↦ (f a).toList) l
⊢ filterMap f (a :: l) = flatMap (fun a ↦ (f a).toList) (a :: l)
Module: Mathlib.Data.List.Basic

Goal state before:
pp: case cons.none
α : Type u
β : Type v
f : α → Option β
a : α
l : List α
ih : filterMap f l = flatMap (fun a ↦ (f a).toList) l
⊢ (match none with
    | none => filterMap f l
    | some b => b :: filterMap f l) =
    none.toList ++ flatMap (fun a ↦ (f a).toList) l

pp: case cons.some
α : Type u
β : Type v
f : α → Option β
a : α
l : List α
ih : filterMap f l = flatMap (fun a ↦ (f a).toList) l
val✝ : β
⊢ (match some val✝ with
    | none => filterMap f l
    | some b => b :: filterMap f l) =
    (some val✝).toList ++ flatMap (fun a ↦ (f a).toList) l

Tactic:
<;>

Goal state after:
case cons.none
α : Type u
β : Type v
f : α → Option β
a : α
l : List α
ih : filterMap f l = flatMap (fun a ↦ (f a).toList) l
⊢ (match none with
    | none => filterMap f l
    | some b => b :: filterMap f l) =
    none.toList ++ flatMap (fun a ↦ (f a).toList) l

case cons.some
α : Type u
β : Type v
f : α → Option β
a : α
l : List α
ih : filterMap f l = flatMap (fun a ↦ (f a).toList) l
val✝ : β
⊢ (match some val✝ with
    | none => filterMap f l
    | some b => b :: filterMap f l) =
    (some val✝).toList ++ flatMap (fun a ↦ (f a).toList) l
Module: Mathlib.Data.List.Basic

Goal state before:
pp: case nil
α : Type u
β : Type v
f g : α → Option β
h : ∀ (x : α), x ∈ [] → f x = g x
⊢ filterMap f [] = filterMap g []

pp: case cons
α : Type u
β : Type v
f g : α → Option β
head✝ : α
tail✝ : List α
tail_ih✝ : (∀ (x : α), x ∈ tail✝ → f x = g x) → filterMap f tail✝ = filterMap g tail✝
h : ∀ (x : α), x ∈ head✝ :: tail✝ → f x = g x
⊢ filterMap f (head✝ :: tail✝) = filterMap g (head✝ :: tail✝)

Tactic:
<;>

Goal state after:
case nil
α : Type u
β : Type v
f g : α → Option β
h : ∀ (x : α), x ∈ [] → f x = g x
⊢ filterMap f [] = filterMap g []

case cons
α : Type u
β : Type v
f g : α → Option β
head✝ : α
tail✝ : List α
tail_ih✝ : (∀ (x : α), x ∈ tail✝ → f x = g x) → filterMap f tail✝ = filterMap g tail✝
h : ∀ (x : α), x ∈ head✝ :: tail✝ → f x = g x
⊢ filterMap f (head✝ :: tail✝) = filterMap g (head✝ :: tail✝)
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: case nil
n : ℤ
⊢ [].sum % n = (map (fun x ↦ x % n) []).sum % n

pp: case cons
n head✝ : ℤ
tail✝ : List ℤ
tail_ih✝ : tail✝.sum % n = (map (fun x ↦ x % n) tail✝).sum % n
⊢ (head✝ :: tail✝).sum % n = (map (fun x ↦ x % n) (head✝ :: tail✝)).sum % n

Tactic:
<;>

Goal state after:
case nil
n : ℤ
⊢ [].sum % n = (map (fun x ↦ x % n) []).sum % n

case cons
n head✝ : ℤ
tail✝ : List ℤ
tail_ih✝ : tail✝.sum % n = (map (fun x ↦ x % n) tail✝).sum % n
⊢ (head✝ :: tail✝).sum % n = (map (fun x ↦ x % n) (head✝ :: tail✝)).sum % n
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: case nil
n : ℤ
⊢ [].prod % n = (map (fun x ↦ x % n) []).prod % n

pp: case cons
n head✝ : ℤ
tail✝ : List ℤ
tail_ih✝ : tail✝.prod % n = (map (fun x ↦ x % n) tail✝).prod % n
⊢ (head✝ :: tail✝).prod % n = (map (fun x ↦ x % n) (head✝ :: tail✝)).prod % n

Tactic:
<;>

Goal state after:
case nil
n : ℤ
⊢ [].prod % n = (map (fun x ↦ x % n) []).prod % n

case cons
n head✝ : ℤ
tail✝ : List ℤ
tail_ih✝ : tail✝.prod % n = (map (fun x ↦ x % n) tail✝).prod % n
⊢ (head✝ :: tail✝).prod % n = (map (fun x ↦ x % n) (head✝ :: tail✝)).prod % n
Module: Mathlib.Data.List.Basic

Goal state before:
pp: case nil
α : Type u
β : Type v
⊢ filterMap (fun x ↦ none) [] = []

pp: case cons
α : Type u
β : Type v
head✝ : α
tail✝ : List α
tail_ih✝ : filterMap (fun x ↦ none) tail✝ = []
⊢ filterMap (fun x ↦ none) (head✝ :: tail✝) = []

Tactic:
<;>

Goal state after:
case nil
α : Type u
β : Type v
⊢ filterMap (fun x ↦ none) [] = []

case cons
α : Type u
β : Type v
head✝ : α
tail✝ : List α
tail_ih✝ : filterMap (fun x ↦ none) tail✝ = []
⊢ filterMap (fun x ↦ none) (head✝ :: tail✝) = []
Module: Mathlib.Data.List.Basic

Goal state before:
pp: case nil
α : Type u
p : α → Bool
⊢ filter p [] = foldr (fun a out ↦ bif p a then a :: out else out) [] []

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✝
⊢ filter p (head✝ :: tail✝) = foldr (fun a out ↦ bif p a then a :: out else out) [] (head✝ :: tail✝)

Tactic:
<;>

Goal state after:
case nil
α : Type u
p : α → Bool
⊢ filter p [] = foldr (fun a out ↦ bif p a then a :: out else out) [] []

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✝
⊢ filter p (head✝ :: tail✝) = foldr (fun a out ↦ bif p a then a :: out else out) [] (head✝ :: tail✝)
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: case cons.zero
α : Type u_2
head✝ : List α
tail✝ : List (List α)
tail_ih✝ : ∀ (i : ℕ), take (take i (map length tail✝)).sum tail✝.flatten = (take i tail✝).flatten
⊢ take (take 0 (map length (head✝ :: tail✝))).sum (head✝ :: tail✝).flatten = (take 0 (head✝ :: tail✝)).flatten

pp: case cons.succ
α : Type u_2
head✝ : List α
tail✝ : List (List α)
tail_ih✝ : ∀ (i : ℕ), take (take i (map length tail✝)).sum tail✝.flatten = (take i tail✝).flatten
n✝ : ℕ
⊢ take (take (n✝ + 1) (map length (head✝ :: tail✝))).sum (head✝ :: tail✝).flatten =
    (take (n✝ + 1) (head✝ :: tail✝)).flatten

Tactic:
<;>

Goal state after:
case cons.zero
α : Type u_2
head✝ : List α
tail✝ : List (List α)
tail_ih✝ : ∀ (i : ℕ), take (take i (map length tail✝)).sum tail✝.flatten = (take i tail✝).flatten
⊢ take (take 0 (map length (head✝ :: tail✝))).sum (head✝ :: tail✝).flatten = (take 0 (head✝ :: tail✝)).flatten

case cons.succ
α : Type u_2
head✝ : List α
tail✝ : List (List α)
tail_ih✝ : ∀ (i : ℕ), take (take i (map length tail✝)).sum tail✝.flatten = (take i tail✝).flatten
n✝ : ℕ
⊢ take (take (n✝ + 1) (map length (head✝ :: tail✝))).sum (head✝ :: tail✝).flatten =
    (take (n✝ + 1) (head✝ :: tail✝)).flatten
Module: Mathlib.Data.Rat.Defs

Goal state before:
pp: ⊢ 1 ≠ 0

pp: ⊢ 1 ≠ 0

Tactic:
<;>

Goal state after:
⊢ 1 ≠ 0

⊢ 1 ≠ 0
Module: Mathlib.Data.List.Basic

Goal state before:
pp: case nil
α : Type u
⊢ filter (fun x ↦ true) [] = []

pp: case cons
α : Type u
head✝ : α
tail✝ : List α
tail_ih✝ : filter (fun x ↦ true) tail✝ = tail✝
⊢ filter (fun x ↦ true) (head✝ :: tail✝) = head✝ :: tail✝

Tactic:
<;>

Goal state after:
case nil
α : Type u
⊢ filter (fun x ↦ true) [] = []

case cons
α : Type u
head✝ : α
tail✝ : List α
tail_ih✝ : filter (fun x ↦ true) tail✝ = tail✝
⊢ filter (fun x ↦ true) (head✝ :: tail✝) = head✝ :: tail✝
Module: Mathlib.Data.List.Basic

Goal state before:
pp: case nil
α : Type u
⊢ filter (fun x ↦ false) [] = []

pp: case cons
α : Type u
head✝ : α
tail✝ : List α
tail_ih✝ : filter (fun x ↦ false) tail✝ = []
⊢ filter (fun x ↦ false) (head✝ :: tail✝) = []

Tactic:
<;>

Goal state after:
case nil
α : Type u
⊢ filter (fun x ↦ false) [] = []

case cons
α : Type u
head✝ : α
tail✝ : List α
tail_ih✝ : filter (fun x ↦ false) tail✝ = []
⊢ filter (fun x ↦ false) (head✝ :: tail✝) = []
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: case cons.zero
α : Type u_2
head✝ : List α
tail✝ : List (List α)
tail_ih✝ : ∀ (i : ℕ), drop (take i (map length tail✝)).sum tail✝.flatten = (drop i tail✝).flatten
⊢ drop (take 0 (map length (head✝ :: tail✝))).sum (head✝ :: tail✝).flatten = (drop 0 (head✝ :: tail✝)).flatten

pp: case cons.succ
α : Type u_2
head✝ : List α
tail✝ : List (List α)
tail_ih✝ : ∀ (i : ℕ), drop (take i (map length tail✝)).sum tail✝.flatten = (drop i tail✝).flatten
n✝ : ℕ
⊢ drop (take (n✝ + 1) (map length (head✝ :: tail✝))).sum (head✝ :: tail✝).flatten =
    (drop (n✝ + 1) (head✝ :: tail✝)).flatten

Tactic:
<;>

Goal state after:
case cons.zero
α : Type u_2
head✝ : List α
tail✝ : List (List α)
tail_ih✝ : ∀ (i : ℕ), drop (take i (map length tail✝)).sum tail✝.flatten = (drop i tail✝).flatten
⊢ drop (take 0 (map length (head✝ :: tail✝))).sum (head✝ :: tail✝).flatten = (drop 0 (head✝ :: tail✝)).flatten

case cons.succ
α : Type u_2
head✝ : List α
tail✝ : List (List α)
tail_ih✝ : ∀ (i : ℕ), drop (take i (map length tail✝)).sum tail✝.flatten = (drop i tail✝).flatten
n✝ : ℕ
⊢ drop (take (n✝ + 1) (map length (head✝ :: tail✝))).sum (head✝ :: tail✝).flatten =
    (drop (n✝ + 1) (head✝ :: tail✝)).flatten
Module: Mathlib.Data.Rat.Defs

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

Tactic:
conv_rhs => rw [← num_divInt_den q, hq]
  rw [intCast_eq_divInt]
  rfl

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

Goal state before:
pp: case nil
α : Type u
β : Type v
l : List α
p : β → Prop
f : α → β
⊢ Forall p (map f []) ↔ Forall (p ∘ f) []

pp: case cons
α : Type u
β : Type v
l : List α
p : β → Prop
f : α → β
head✝ : α
tail✝ : List α
tail_ih✝ : Forall p (map f tail✝) ↔ Forall (p ∘ f) tail✝
⊢ Forall p (map f (head✝ :: tail✝)) ↔ Forall (p ∘ f) (head✝ :: tail✝)

Tactic:
<;>

Goal state after:
case nil
α : Type u
β : Type v
l : List α
p : β → Prop
f : α → β
⊢ Forall p (map f []) ↔ Forall (p ∘ f) []

case cons
α : Type u
β : Type v
l : List α
p : β → Prop
f : α → β
head✝ : α
tail✝ : List α
tail_ih✝ : Forall p (map f tail✝) ↔ Forall (p ∘ f) tail✝
⊢ Forall p (map f (head✝ :: tail✝)) ↔ Forall (p ∘ f) (head✝ :: tail✝)
Module: Mathlib.Algebra.Order.Ring.Unbundled.Rat

Goal state before:
pp: a : ℤ
b : ℕ
hb : b ≠ 0
⊢ 0 < ↑b

Tactic:
simpa using Nat.pos_of_ne_zero hb

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

Goal state before:
pp: case refine_1
q : ℚ
⊢ |q|.num = { num := |q.num|, den := q.den, den_nz := ⋯, reduced := ⋯ }.num

pp: case refine_2
q : ℚ
⊢ |q|.den = { num := |q.num|, den := q.den, den_nz := ⋯, reduced := ⋯ }.den

Tactic:
<;>

Goal state after:
case refine_1
q : ℚ
⊢ |q|.num = { num := |q.num|, den := q.den, den_nz := ⋯, reduced := ⋯ }.num

case refine_2
q : ℚ
⊢ |q|.den = { num := |q.num|, den := q.den, den_nz := ⋯, reduced := ⋯ }.den
Module: Mathlib.Algebra.Field.Rat

Goal state before:
pp: q : ℚ≥0
⊢ q⁻¹ = divNat q.den q.num

Tactic:
by ext; simp [Rat.inv_def, num_coe, den_coe]

Goal state after:
Module: Mathlib.Algebra.Divisibility.Units

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
a b u : α
hu : IsUnit u
⊢ a ∣ u * b ↔ a ∣ b

Tactic:
by
  rcases hu with ⟨u, rfl⟩
  apply Units.dvd_mul_left

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Divisibility

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

pp: case inr
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : Subsingleton αˣ
c d : α
⊢ 0 = 0 * c

Tactic:
<;>

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.Rat.Lemmas

Goal state before:
pp: case a
q₁ q₂ : ℚ
⊢ ↑(q₁.den.gcd q₂.den) ∣ q₁.num * ↑q₂.den

pp: case a
q₁ q₂ : ℚ
⊢ ↑(q₁.den.gcd q₂.den) ∣ q₂.num * ↑q₁.den

Tactic:
<;>

Goal state after:
case a
q₁ q₂ : ℚ
⊢ ↑(q₁.den.gcd q₂.den) ∣ q₁.num * ↑q₂.den

case a
q₁ q₂ : ℚ
⊢ ↑(q₁.den.gcd q₂.den) ∣ q₂.num * ↑q₁.den
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: case a
q₁ q₂ : ℚ
⊢ ↑(q₁.den.gcd q₂.den) ∣ ↑q₂.den

pp: case a
q₁ q₂ : ℚ
⊢ ↑(q₁.den.gcd q₂.den) ∣ ↑q₁.den

Tactic:
<;>

Goal state after:
case a
q₁ q₂ : ℚ
⊢ ↑(q₁.den.gcd q₂.den) ∣ ↑q₂.den

case a
q₁ q₂ : ℚ
⊢ ↑(q₁.den.gcd q₂.den) ∣ ↑q₁.den
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: q : ℚ
⊢ (-q)⁻¹ = -q⁻¹

Tactic:
rw [← num_divInt_den q]
  simp only [Rat.neg_divInt, Rat.inv_divInt, Rat.divInt_neg]

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

Goal state before:
pp: case mp
m n : ℤ
hn : ↑n ≠ 0
⊢ (↑m / ↑n).den = 1 → n ∣ m

Tactic:
rw [Rat.den_eq_one_iff, eq_div_iff hn]

Goal state after:
case mp
m n : ℤ
hn : ↑n ≠ 0
⊢ ↑(↑m / ↑n).num * ↑n = ↑m → n ∣ m
Module: Mathlib.Data.Tree.Basic

Goal state before:
pp: case nil
α : Type u
⊢ nil.numLeaves = nil.numNodes + 1

pp: case node
α : Type u
value✝ : α
left✝ right✝ : BinaryTree α
left_ih✝ : left✝.numLeaves = left✝.numNodes + 1
right_ih✝ : right✝.numLeaves = right✝.numNodes + 1
⊢ (node value✝ left✝ right✝).numLeaves = (node value✝ left✝ right✝).numNodes + 1

Tactic:
<;>

Goal state after:
case nil
α : Type u
⊢ nil.numLeaves = nil.numNodes + 1

case node
α : Type u
value✝ : α
left✝ right✝ : BinaryTree α
left_ih✝ : left✝.numLeaves = left✝.numNodes + 1
right_ih✝ : right✝.numLeaves = right✝.numNodes + 1
⊢ (node value✝ left✝ right✝).numLeaves = (node value✝ left✝ right✝).numNodes + 1
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a : R
⊢ Nat.rawCast 1 * a = a

Tactic:
simp [Nat.rawCast]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a : R
⊢ a * Nat.rawCast 1 = a

Tactic:
simp [Nat.rawCast]

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

Goal state before:
pp: R : Type u
inst✝⁶ : CommSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : CanonicallyOrderedAdd R
inst✝³ : Sub R
inst✝² : OrderedSub R
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : AddLeftReflectLE R
a : R
⊢ a * a - 1 = (a + 1) * (a - 1)

Tactic:
by
  rw [← mul_self_tsub_mul_self, mul_one]

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

Goal state before:
pp: case zero
⊢ 0 ∈ {0} ∪ range succ ↔ 0 ∈ univ

pp: case succ
n✝ : ℕ
⊢ n✝ + 1 ∈ {0} ∪ range succ ↔ n✝ + 1 ∈ univ

Tactic:
<;>

Goal state after:
case zero
⊢ 0 ∈ {0} ∪ range succ ↔ 0 ∈ univ

case succ
n✝ : ℕ
⊢ n✝ + 1 ∈ {0} ∪ range succ ↔ n✝ + 1 ∈ univ
Module: Mathlib.Data.Nat.Set

Goal state before:
pp: case zero
⊢ 0 ∈ range succ ↔ 0 ∈ {i | 0 < i}

pp: case succ
i : ℕ
⊢ i + 1 ∈ range succ ↔ i + 1 ∈ {i | 0 < i}

Tactic:
<;>

Goal state after:
case zero
⊢ 0 ∈ range succ ↔ 0 ∈ {i | 0 < i}

case succ
i : ℕ
⊢ i + 1 ∈ range succ ↔ i + 1 ∈ {i | 0 < i}
Module: Mathlib.Data.Nat.Set

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

Tactic:
rename_i n

Goal state after:
case e'_4
α : Type u_2
x : α
f : ℕ → α → α
n : ℕ
⊢ rec (f 0 x) (f ∘ succ) n = f n (rec x f n)