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

Goal state before:
pp: case cons.inl
M : Type u_4
inst✝¹ : Monoid M
l✝ : List M
a : M
inst✝ : DecidableEq M
l : List M
ih : a ∈ l → (∀ (x : M), x ∈ l → ∀ (y : M), y ∈ l → x * y = y * x) → a * (l.erase a).prod = l.prod
ha : a ∈ a :: l
comm : ∀ (x : M), x ∈ a :: l → ∀ (y : M), y ∈ a :: l → x * y = y * x
⊢ a * ((a :: l).erase a).prod = (a :: l).prod

pp: case cons.inr
M : Type u_4
inst✝¹ : Monoid M
l✝ : List M
a : M
inst✝ : DecidableEq M
b : M
l : List M
ih : a ∈ l → (∀ (x : M), x ∈ l → ∀ (y : M), y ∈ l → x * y = y * x) → a * (l.erase a).prod = l.prod
ha : a ∈ b :: l
comm : ∀ (x : M), x ∈ b :: l → ∀ (y : M), y ∈ b :: l → x * y = y * x
ne : a ≠ b
h : a ∈ l
⊢ a * ((b :: l).erase a).prod = (b :: l).prod

Tactic:
·

Goal state after:
case cons.inl
M : Type u_4
inst✝¹ : Monoid M
l✝ : List M
a : M
inst✝ : DecidableEq M
l : List M
ih : a ∈ l → (∀ (x : M), x ∈ l → ∀ (y : M), y ∈ l → x * y = y * x) → a * (l.erase a).prod = l.prod
ha : a ∈ a :: l
comm : ∀ (x : M), x ∈ a :: l → ∀ (y : M), y ∈ a :: l → x * y = y * x
⊢ a * ((a :: l).erase a).prod = (a :: l).prod
Module: Mathlib.Data.List.Basic

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

Tactic:
by
  constructor <;> rintro (_ | _) <;> aesop

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

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

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

Goal state after:
case nil
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
⊢ idxOf a [] = 0 ↔ [] = [] ∨ [].head? = some a
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:
·

Goal state after:
case cons
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a head✝ : α
tail✝ : List α
⊢ idxOf a (head✝ :: tail✝) = 0 ↔ head✝ :: tail✝ = [] ∨ (head✝ :: tail✝).head? = some a
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: case pos
α : Type u_2
M : Type u_4
inst✝¹ : Monoid M
inst✝ : DecidableEq α
f : α → M
a' : α
as : List α
a : α
h : (map f as).prod = f a ^ count a as
hf : ∀ (a'_1 : α), a'_1 ≠ a → a'_1 ∈ a' :: as → f a'_1 = 1
ha' : a' = a
⊢ f a' * f a ^ count a as = f a ^ (count a as + 1)

pp: case neg
α : Type u_2
M : Type u_4
inst✝¹ : Monoid M
inst✝ : DecidableEq α
f : α → M
a' : α
as : List α
a : α
h : (map f as).prod = f a ^ count a as
hf : ∀ (a'_1 : α), a'_1 ≠ a → a'_1 ∈ a' :: as → f a'_1 = 1
ha' : ¬a' = a
⊢ f a' * f a ^ count a as = f a ^ (count a as + 0)

Tactic:
·

Goal state after:
case pos
α : Type u_2
M : Type u_4
inst✝¹ : Monoid M
inst✝ : DecidableEq α
f : α → M
a' : α
as : List α
a : α
h : (map f as).prod = f a ^ count a as
hf : ∀ (a'_1 : α), a'_1 ≠ a → a'_1 ∈ a' :: as → f a'_1 = 1
ha' : a' = a
⊢ f a' * f a ^ count a as = f a ^ (count a as + 1)
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: case neg
α : Type u_2
M : Type u_4
inst✝¹ : Monoid M
inst✝ : DecidableEq α
f : α → M
a' : α
as : List α
a : α
h : (map f as).prod = f a ^ count a as
hf : ∀ (a'_1 : α), a'_1 ≠ a → a'_1 ∈ a' :: as → f a'_1 = 1
ha' : ¬a' = a
⊢ f a' * f a ^ count a as = f a ^ (count a as + 0)

Tactic:
·

Goal state after:
case neg
α : Type u_2
M : Type u_4
inst✝¹ : Monoid M
inst✝ : DecidableEq α
f : α → M
a' : α
as : List α
a : α
h : (map f as).prod = f a ^ count a as
hf : ∀ (a'_1 : α), a'_1 ≠ a → a'_1 ∈ a' :: as → f a'_1 = 1
ha' : ¬a' = a
⊢ f a' * f a ^ count a as = f a ^ (count a as + 0)
Module: Mathlib.Data.List.Basic

Goal state before:
pp: case refine_1
α : Type u
l₁ l₂ : List α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
hl : l₁ <+: l₂
a : α
h : a ∈ l₁
⊢ idxOf a l₂ < l₁.length

pp: case refine_2
α : Type u
l₁ l₂ : List α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
hl : l₁ <+: l₂
a : α
h : idxOf a l₂ < l₁.length
⊢ a ∈ l₁

Tactic:
·

Goal state after:
case refine_1
α : Type u
l₁ l₂ : List α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
hl : l₁ <+: l₂
a : α
h : a ∈ l₁
⊢ idxOf a l₂ < l₁.length
Module: Mathlib.Data.List.Basic

Goal state before:
pp: case refine_2
α : Type u
l₁ l₂ : List α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
hl : l₁ <+: l₂
a : α
h : idxOf a l₂ < l₁.length
⊢ a ∈ l₁

Tactic:
·

Goal state after:
case refine_2
α : Type u
l₁ l₂ : List α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
hl : l₁ <+: l₂
a : α
h : idxOf a l₂ < l₁.length
⊢ a ∈ l₁
Module: Mathlib.Data.List.Basic

Goal state before:
pp: case mp
α : Type u
l₁ l₂ : List α
⊢ l₁ = l₂ → l₁.length = l₂.length ∧ ∀ (n : ℕ) (h₁ : n < l₁.length) (h₂ : n < l₂.length), l₁.get ⟨n, h₁⟩ = l₂.get ⟨n, h₂⟩

pp: case mpr
α : Type u
l₁ l₂ : List α
⊢ (l₁.length = l₂.length ∧ ∀ (n : ℕ) (h₁ : n < l₁.length) (h₂ : n < l₂.length), l₁.get ⟨n, h₁⟩ = l₂.get ⟨n, h₂⟩) →
    l₁ = l₂

Tactic:
·

Goal state after:
case mp
α : Type u
l₁ l₂ : List α
⊢ l₁ = l₂ → l₁.length = l₂.length ∧ ∀ (n : ℕ) (h₁ : n < l₁.length) (h₂ : n < l₂.length), l₁.get ⟨n, h₁⟩ = l₂.get ⟨n, h₂⟩
Module: Mathlib.Data.List.Basic

Goal state before:
pp: case mpr
α : Type u
l₁ l₂ : List α
⊢ (l₁.length = l₂.length ∧ ∀ (n : ℕ) (h₁ : n < l₁.length) (h₂ : n < l₂.length), l₁.get ⟨n, h₁⟩ = l₂.get ⟨n, h₂⟩) →
    l₁ = l₂

Tactic:
·

Goal state after:
case mpr
α : Type u
l₁ l₂ : List α
⊢ (l₁.length = l₂.length ∧ ∀ (n : ℕ) (h₁ : n < l₁.length) (h₂ : n < l₂.length), l₁.get ⟨n, h₁⟩ = l₂.get ⟨n, h₂⟩) →
    l₁ = l₂
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: case inl
α : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq α
f : α → M
a : α
l : List α
h : a ∈ a :: l
⊢ f a * (map f ((a :: l).erase a)).prod = (map f (a :: l)).prod

pp: case inr
α : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq α
f : α → M
a b : α
l : List α
h✝ : a ∈ b :: l
ne : a ≠ b
h : a ∈ l
⊢ f a * (map f ((b :: l).erase a)).prod = (map f (b :: l)).prod

Tactic:
·

Goal state after:
case inl
α : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq α
f : α → M
a : α
l : List α
h : a ∈ a :: l
⊢ f a * (map f ((a :: l).erase a)).prod = (map f (a :: l)).prod
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: case inr
α : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq α
f : α → M
a b : α
l : List α
h✝ : a ∈ b :: l
ne : a ≠ b
h : a ∈ l
⊢ f a * (map f ((b :: l).erase a)).prod = (map f (b :: l)).prod

Tactic:
·

Goal state after:
case inr
α : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq α
f : α → M
a b : α
l : List α
h✝ : a ∈ b :: l
ne : a ≠ b
h : a ∈ l
⊢ f a * (map f ((b :: l).erase a)).prod = (map f (b :: l)).prod
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
x : M
xs : List M
y : M
ys : List M
| ys.prod * xs.prod

Tactic:
rw [mul_comm, prod_mul_prod_eq_prod_zipWith_mul_prod_drop xs ys]

Goal state after:
M : Type u_4
inst✝ : CommMonoid M
x : M
xs : List M
y : M
ys : List M
| (zipWith (fun x1 x2 ↦ x1 * x2) xs ys).prod * (drop ys.length xs).prod * (drop xs.length ys).prod
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: case pos
α : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
p : α → Prop
inst✝ : DecidablePred p
f g : α → M
x : α
xs : List α
hx : p x
⊢ (if p x then f x else g x) *
      ((map f (filter (fun b ↦ decide (p b)) xs)).prod * (map g (filter (fun a ↦ decide ¬p a) xs)).prod) =
    (map f
          (if decide (p x) = true then x :: filter (fun b ↦ decide (p b)) xs
          else filter (fun b ↦ decide (p b)) xs)).prod *
      (map g
          (if (decide ¬p x) = true then x :: filter (fun a ↦ decide ¬p a) xs else filter (fun a ↦ decide ¬p a) xs)).prod

pp: case neg
α : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
p : α → Prop
inst✝ : DecidablePred p
f g : α → M
x : α
xs : List α
hx : ¬p x
⊢ (if p x then f x else g x) *
      ((map f (filter (fun b ↦ decide (p b)) xs)).prod * (map g (filter (fun a ↦ decide ¬p a) xs)).prod) =
    (map f
          (if decide (p x) = true then x :: filter (fun b ↦ decide (p b)) xs
          else filter (fun b ↦ decide (p b)) xs)).prod *
      (map g
          (if (decide ¬p x) = true then x :: filter (fun a ↦ decide ¬p a) xs else filter (fun a ↦ decide ¬p a) xs)).prod

Tactic:
·

Goal state after:
case pos
α : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
p : α → Prop
inst✝ : DecidablePred p
f g : α → M
x : α
xs : List α
hx : p x
⊢ (if p x then f x else g x) *
      ((map f (filter (fun b ↦ decide (p b)) xs)).prod * (map g (filter (fun a ↦ decide ¬p a) xs)).prod) =
    (map f
          (if decide (p x) = true then x :: filter (fun b ↦ decide (p b)) xs
          else filter (fun b ↦ decide (p b)) xs)).prod *
      (map g
          (if (decide ¬p x) = true then x :: filter (fun a ↦ decide ¬p a) xs else filter (fun a ↦ decide ¬p a) xs)).prod
Module: Mathlib.Data.List.Basic

Goal state before:
pp: ι : Type u_1
α : Type u
β : Type v
γ : Type w
l✝ l₁ l₂ l : List α
h : l.length = 1
⊢ 0 < l.length

Tactic:
by lia

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

Goal state before:
pp: case neg
α : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
p : α → Prop
inst✝ : DecidablePred p
f g : α → M
x : α
xs : List α
hx : ¬p x
⊢ (if p x then f x else g x) *
      ((map f (filter (fun b ↦ decide (p b)) xs)).prod * (map g (filter (fun a ↦ decide ¬p a) xs)).prod) =
    (map f
          (if decide (p x) = true then x :: filter (fun b ↦ decide (p b)) xs
          else filter (fun b ↦ decide (p b)) xs)).prod *
      (map g
          (if (decide ¬p x) = true then x :: filter (fun a ↦ decide ¬p a) xs else filter (fun a ↦ decide ¬p a) xs)).prod

Tactic:
·

Goal state after:
case neg
α : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
p : α → Prop
inst✝ : DecidablePred p
f g : α → M
x : α
xs : List α
hx : ¬p x
⊢ (if p x then f x else g x) *
      ((map f (filter (fun b ↦ decide (p b)) xs)).prod * (map g (filter (fun a ↦ decide ¬p a) xs)).prod) =
    (map f
          (if decide (p x) = true then x :: filter (fun b ↦ decide (p b)) xs
          else filter (fun b ↦ decide (p b)) xs)).prod *
      (map g
          (if (decide ¬p x) = true then x :: filter (fun a ↦ decide ¬p a) xs else filter (fun a ↦ decide ¬p a) xs)).prod
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: case pos
G : Type u_7
inst✝ : CommGroup G
L : List G
n : ℕ
a : G
hn : n < L.length
⊢ (take n L).prod * a * (drop (n + 1) L).prod = L.prod * (L[n]⁻¹ * a)

pp: case neg
G : Type u_7
inst✝ : CommGroup G
L : List G
n : ℕ
a : G
hn : ¬n < L.length
⊢ (take n L).prod * 1 * (drop (n + 1) L).prod = L.prod * 1

Tactic:
·

Goal state after:
case pos
G : Type u_7
inst✝ : CommGroup G
L : List G
n : ℕ
a : G
hn : n < L.length
⊢ (take n L).prod * a * (drop (n + 1) L).prod = L.prod * (L[n]⁻¹ * a)
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: case neg
G : Type u_7
inst✝ : CommGroup G
L : List G
n : ℕ
a : G
hn : ¬n < L.length
⊢ (take n L).prod * 1 * (drop (n + 1) L).prod = L.prod * 1

Tactic:
·

Goal state after:
case neg
G : Type u_7
inst✝ : CommGroup G
L : List G
n : ℕ
a : G
hn : ¬n < L.length
⊢ (take n L).prod * 1 * (drop (n + 1) L).prod = L.prod * 1
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

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

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

Tactic:
·

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)
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

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

Tactic:
·

Goal state after:
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 mp
α : Type u
x₁ x₂ z₁ z₂ : List α
a₁ a₂ : α
notin_x : ¬a₂ ∈ x₁
notin_z : ¬a₂ ∈ z₁
⊢ x₁ ++ a₁ :: z₁ = x₂ ++ a₂ :: z₂ → x₁ = x₂ ∧ a₁ = a₂ ∧ z₁ = z₂

pp: case mpr
α : Type u
x₁ x₂ z₁ z₂ : List α
a₁ a₂ : α
notin_x : ¬a₂ ∈ x₁
notin_z : ¬a₂ ∈ z₁
⊢ x₁ = x₂ ∧ a₁ = a₂ ∧ z₁ = z₂ → x₁ ++ a₁ :: z₁ = x₂ ++ a₂ :: z₂

Tactic:
·

Goal state after:
case mp
α : Type u
x₁ x₂ z₁ z₂ : List α
a₁ a₂ : α
notin_x : ¬a₂ ∈ x₁
notin_z : ¬a₂ ∈ z₁
⊢ x₁ ++ a₁ :: z₁ = x₂ ++ a₂ :: z₂ → x₁ = x₂ ∧ a₁ = a₂ ∧ z₁ = z₂
Module: Mathlib.Data.List.Basic

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

Tactic:
·

Goal state after:
case mpr
α : Type u
x₁ x₂ z₁ z₂ : List α
a₁ a₂ : α
notin_x : ¬a₂ ∈ x₁
notin_z : ¬a₂ ∈ z₁
⊢ x₁ = x₂ ∧ a₁ = a₂ ∧ z₁ = z₂ → x₁ ++ a₁ :: z₁ = x₂ ++ a₂ :: z₂
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: L : List ℕ
⊢ L.headI + L.tail.sum = L.sum

Tactic:
by
  cases L <;> simp

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
⊢ filterMap f (a :: l) = map g (a :: l) → ∀ (x : α), x ∈ a :: l → f x = some (g x)

pp: case cons.some
α : 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)
b : β
ha : f a = some b
⊢ filterMap f (a :: l) = map g (a :: l) → ∀ (x : α), x ∈ a :: l → f x = some (g x)

Tactic:
·

Goal state after:
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
⊢ filterMap f (a :: l) = map g (a :: l) → ∀ (x : α), x ∈ a :: l → f x = some (g x)
Module: Mathlib.Data.List.Basic

Goal state before:
pp: case cons.some
α : 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)
b : β
ha : f a = some b
⊢ filterMap f (a :: l) = map g (a :: l) → ∀ (x : α), x ∈ a :: l → f x = some (g x)

Tactic:
·

Goal state after:
case cons.some
α : 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)
b : β
ha : f a = some b
⊢ filterMap f (a :: l) = map g (a :: l) → ∀ (x : α), x ∈ a :: l → f x = some (g x)
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: case nil
α : Type u_2
i : ℕ
⊢ take (take i (map length [])).sum [].flatten = (take i []).flatten

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

Tactic:
·

Goal state after:
case nil
α : Type u_2
i : ℕ
⊢ take (take i (map length [])).sum [].flatten = (take i []).flatten
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

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

Tactic:
·

Goal state after:
case cons
α : Type u_2
head✝ : List α
tail✝ : List (List α)
tail_ih✝ : ∀ (i : ℕ), take (take i (map length tail✝)).sum tail✝.flatten = (take i tail✝).flatten
i : ℕ
⊢ take (take i (map length (head✝ :: tail✝))).sum (head✝ :: tail✝).flatten = (take i (head✝ :: tail✝)).flatten
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: case nil
α : Type u_2
i : ℕ
⊢ drop (take i (map length [])).sum [].flatten = (drop i []).flatten

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

Tactic:
·

Goal state after:
case nil
α : Type u_2
i : ℕ
⊢ drop (take i (map length [])).sum [].flatten = (drop i []).flatten
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

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

Tactic:
·

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

Goal state before:
pp: case pos
x : ℤ
hx : x ≠ 0
n d : ℤ
hd : d = 0
⊢ n /. x * (x /. d) = n /. d

pp: case neg
x : ℤ
hx : x ≠ 0
n d : ℤ
hd : ¬d = 0
⊢ n /. x * (x /. d) = n /. d

Tactic:
·

Goal state after:
case pos
x : ℤ
hx : x ≠ 0
n d : ℤ
hd : d = 0
⊢ n /. x * (x /. d) = n /. d
Module: Mathlib.Algebra.Ring.Rat

Goal state before:
pp: q : ℚ
this : ↑q.den ≠ 0
⊢ q.num * ↑q.den /. (1 * ↑q.den) = q.num /. 1

Tactic:
divInt_mul_right this

Goal state after:
q : ℚ
this : ↑q.den ≠ 0
⊢ q.num /. 1 = q.num /. 1
Module: Mathlib.Algebra.Order.Ring.Unbundled.Rat

Goal state before:
pp: case false
m e : ℕ
⊢ 0 ≤ if false = true then normalize (↑m) (10 ^ e) ⋯ else ↑(m * 10 ^ e)

pp: case true
m e : ℕ
⊢ 0 ≤ if true = true then normalize (↑m) (10 ^ e) ⋯ else ↑(m * 10 ^ e)

Tactic:
·

Goal state after:
case false
m e : ℕ
⊢ 0 ≤ if false = true then normalize (↑m) (10 ^ e) ⋯ else ↑(m * 10 ^ e)
Module: Mathlib.Algebra.Order.Ring.Unbundled.Rat

Goal state before:
pp: case true
m e : ℕ
⊢ 0 ≤ if true = true then normalize (↑m) (10 ^ e) ⋯ else ↑(m * 10 ^ e)

Tactic:
·

Goal state after:
case true
m e : ℕ
⊢ 0 ≤ if true = true then normalize (↑m) (10 ^ e) ⋯ else ↑(m * 10 ^ e)
Module: Mathlib.Algebra.Order.Ring.Unbundled.Rat

Goal state before:
pp: case inl
a : ℤ
ha : a ≤ 0
⊢ mkRat a 0 ≤ 0

pp: case inr
a : ℤ
ha : a ≤ 0
b : ℕ
hb : b ≠ 0
⊢ mkRat a b ≤ 0

Tactic:
·

Goal state after:
case inl
a : ℤ
ha : a ≤ 0
⊢ mkRat a 0 ≤ 0
Module: Mathlib.Algebra.Order.Ring.Unbundled.Rat

Goal state before:
pp: case inr
a : ℤ
ha : a ≤ 0
b : ℕ
hb : b ≠ 0
⊢ mkRat a b ≤ 0

Tactic:
·

Goal state after:
case inr
a : ℤ
ha : a ≤ 0
b : ℕ
hb : b ≠ 0
⊢ mkRat a b ≤ 0
Module: Mathlib.Algebra.Order.Ring.Unbundled.Rat

Goal state before:
pp: case h₁
a b c d : ℤ
b_pos : 0 < b
d_pos : 0 < d
⊢ ↑a / ↑b ≤ ↑c / ↑d ↔ a * d ≤ c * b

pp: case h₂
a b c d : ℤ
b_pos : 0 < b
d_pos : 0 < d
⊢ ¬↑c / ↑d ≤ ↑a / ↑b ↔ ¬c * b ≤ a * d

Tactic:
·

Goal state after:
case h₁
a b c d : ℤ
b_pos : 0 < b
d_pos : 0 < d
⊢ ↑a / ↑b ≤ ↑c / ↑d ↔ a * d ≤ c * b
Module: Mathlib.Algebra.Order.Ring.Unbundled.Rat

Goal state before:
pp: case h₂
a b c d : ℤ
b_pos : 0 < b
d_pos : 0 < d
⊢ ¬↑c / ↑d ≤ ↑a / ↑b ↔ ¬c * b ≤ a * d

Tactic:
·

Goal state after:
case h₂
a b c d : ℤ
b_pos : 0 < b
d_pos : 0 < d
⊢ ¬↑c / ↑d ≤ ↑a / ↑b ↔ ¬c * b ≤ a * d
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

Tactic:
simp [Int.abs_eq_natAbs, abs_def,
      ← Rat.mk_eq_divInt (num := q.num.natAbs) (nz := q.den_ne_zero) (c := q.reduced)]

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

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

Tactic:
simp [Int.abs_eq_natAbs, abs_def,
      ← Rat.mk_eq_divInt (num := q.num.natAbs) (nz := q.den_ne_zero) (c := q.reduced)]

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

Goal state before:
pp: case pos
K : Type u_1
inst✝ : NNRatCast K
m : ℕ
b : Bool
d : ℕ
h✝ : b = true
⊢ ↑⟨OfScientific.ofScientific m b d, ⋯⟩ = ↑(NNRat.divNat m (10 ^ d))

pp: case neg
K : Type u_1
inst✝ : NNRatCast K
m : ℕ
b : Bool
d : ℕ
h✝ : ¬b = true
⊢ ↑⟨OfScientific.ofScientific m b d, ⋯⟩ = ↑↑(m * 10 ^ d)

Tactic:
·

Goal state after:
case pos
K : Type u_1
inst✝ : NNRatCast K
m : ℕ
b : Bool
d : ℕ
h✝ : b = true
⊢ ↑⟨OfScientific.ofScientific m b d, ⋯⟩ = ↑(NNRat.divNat m (10 ^ d))
Module: Mathlib.Algebra.Field.Rat

Goal state before:
pp: case neg
K : Type u_1
inst✝ : NNRatCast K
m : ℕ
b : Bool
d : ℕ
h✝ : ¬b = true
⊢ ↑⟨OfScientific.ofScientific m b d, ⋯⟩ = ↑↑(m * 10 ^ d)

Tactic:
·

Goal state after:
case neg
K : Type u_1
inst✝ : NNRatCast K
m : ℕ
b : Bool
d : ℕ
h✝ : ¬b = true
⊢ ↑⟨OfScientific.ofScientific m b d, ⋯⟩ = ↑↑(m * 10 ^ d)
Module: Mathlib.Data.NNRat.Defs

Goal state before:
pp: q : ℚ
⊢ q.toNNRat = 0 ↔ q ≤ 0

Tactic:
by
  simpa [-toNNRat_pos] using (@toNNRat_pos q).not

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

Goal state before:
pp: case inl
p q : ℚ
hp : 0 ≤ p
hq : 0 ≤ q
⊢ (p * q).toNNRat = p.toNNRat * q.toNNRat

pp: case inr
p q : ℚ
hp : 0 ≤ p
hq : q ≤ 0
⊢ (p * q).toNNRat = p.toNNRat * q.toNNRat

Tactic:
·

Goal state after:
case inl
p q : ℚ
hp : 0 ≤ p
hq : 0 ≤ q
⊢ (p * q).toNNRat = p.toNNRat * q.toNNRat
Module: Mathlib.Data.NNRat.Defs

Goal state before:
pp: case inr
p q : ℚ
hp : 0 ≤ p
hq : q ≤ 0
⊢ (p * q).toNNRat = p.toNNRat * q.toNNRat

Tactic:
·

Goal state after:
case inr
p q : ℚ
hp : 0 ≤ p
hq : q ≤ 0
⊢ (p * q).toNNRat = p.toNNRat * q.toNNRat
Module: Mathlib.Algebra.GroupWithZero.Divisibility

Goal state before:
pp: case left
α : Type u_1
inst✝ : CommMonoidWithZero α
a b : α
hd : a ∣ b
hnd : ¬b ∣ a
⊢ a ≠ 0

pp: case right
α : Type u_1
inst✝ : CommMonoidWithZero α
a b : α
hd : a ∣ b
hnd : ¬b ∣ a
⊢ ∃ x, ¬IsUnit x ∧ b = a * x

Tactic:
·

Goal state after:
case left
α : Type u_1
inst✝ : CommMonoidWithZero α
a b : α
hd : a ∣ b
hnd : ¬b ∣ a
⊢ a ≠ 0
Module: Mathlib.Algebra.GroupWithZero.Divisibility

Goal state before:
pp: case right
α : Type u_1
inst✝ : CommMonoidWithZero α
a b : α
hd : a ∣ b
hnd : ¬b ∣ a
⊢ ∃ x, ¬IsUnit x ∧ b = a * x

Tactic:
·

Goal state after:
case right
α : Type u_1
inst✝ : CommMonoidWithZero α
a b : α
hd : a ∣ b
hnd : ¬b ∣ a
⊢ ∃ x, ¬IsUnit x ∧ b = a * x
Module: Mathlib.Algebra.Divisibility.Units

Goal state before:
pp: case inl
α : Type u_1
inst✝ : CommMonoid α
x : α
⊢ x ∣ x ^ 0 ↔ 0 ≠ 0 ∨ IsUnit x

pp: case inr
α : Type u_1
inst✝ : CommMonoid α
x : α
n : ℕ
hn : n ≠ 0
⊢ x ∣ x ^ n ↔ n ≠ 0 ∨ IsUnit x

Tactic:
·

Goal state after:
case inl
α : Type u_1
inst✝ : CommMonoid α
x : α
⊢ x ∣ x ^ 0 ↔ 0 ≠ 0 ∨ IsUnit x
Module: Mathlib.Algebra.Divisibility.Units

Goal state before:
pp: case inr
α : Type u_1
inst✝ : CommMonoid α
x : α
n : ℕ
hn : n ≠ 0
⊢ x ∣ x ^ n ↔ n ≠ 0 ∨ IsUnit x

Tactic:
·

Goal state after:
case inr
α : Type u_1
inst✝ : CommMonoid α
x : α
n : ℕ
hn : n ≠ 0
⊢ x ∣ x ^ n ↔ n ≠ 0 ∨ IsUnit x