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

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Finset (ι →₀ M)
hs : (↑s).PairwiseDisjoint Finsupp.support
⊢ s.toList.toFinset = s

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finsupp.Pointwise

Goal state before:
pp: α : Type u₁
β : Type u₂
γ : Type u₃
inst✝¹ : Zero γ
inst✝ : SMulZeroClass β γ
f : α → β
g : α →₀ γ
⊢ (Function.support fun x ↦ f x • g x) ⊆ Function.support ⇑g

Tactic:
simp

Goal state after:
α : Type u₁
β : Type u₂
γ : Type u₃
inst✝¹ : Zero γ
inst✝ : SMulZeroClass β γ
f : α → β
g : α →₀ γ
⊢ ∀ (x : α), ¬f x • g x = 0 → ¬g x = 0
Module: Mathlib.Data.Finsupp.Sigma

Goal state before:
pp: κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst✝ : Zero M
k : κ
f : ι k →₀ M
i : ι k
⊢ f.embSigma ⟨k, i⟩ = f i

Tactic:
rw [embSigma]
  exact embDomain_apply_self (Embedding.sigmaMk k) f i

Goal state after:
Module: Mathlib.Data.Finsupp.Sigma

Goal state before:
pp: case pos
κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst✝ : AddMonoid M
k' : κ
i : ι k'
f g : ι k' →₀ M
⊢ (f + g).embSigma ⟨k', i⟩ = (f.embSigma + g.embSigma) ⟨k', i⟩

Tactic:
simp

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

Goal state before:
pp: case inl
S : Type u_2
inst✝² : CommRing S
inst✝¹ : LinearOrder S
inst✝ : IsStrictOrderedRing S
abv : AbsoluteValue ℤ S
⊢ abv ↑1 = 1

Tactic:
simp

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

Goal state before:
pp: case inr
S : Type u_2
inst✝² : CommRing S
inst✝¹ : LinearOrder S
inst✝ : IsStrictOrderedRing S
abv : AbsoluteValue ℤ S
⊢ abv ↑(-1) = 1

Tactic:
simp

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

Goal state before:
pp: case inl
R : Type u_1
S : Type u_2
inst✝⁴ : Ring R
inst✝³ : CommRing S
inst✝² : LinearOrder S
inst✝¹ : IsStrictOrderedRing S
inst✝ : Nontrivial R
abv : AbsoluteValue R S
⊢ abv ↑↑1 = 1

Tactic:
simp

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

Goal state before:
pp: case inr
R : Type u_1
S : Type u_2
inst✝⁴ : Ring R
inst✝³ : CommRing S
inst✝² : LinearOrder S
inst✝¹ : IsStrictOrderedRing S
inst✝ : Nontrivial R
abv : AbsoluteValue R S
⊢ abv ↑↑(-1) = 1

Tactic:
simp

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

Goal state before:
pp: case inl
R : Type u_1
S : Type u_2
inst✝³ : Ring R
inst✝² : CommRing S
inst✝¹ : LinearOrder S
inst✝ : IsStrictOrderedRing S
abv : AbsoluteValue R S
y : R
⊢ abv (1 • y) = abv y

Tactic:
simp

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

Goal state before:
pp: case inr
R : Type u_1
S : Type u_2
inst✝³ : Ring R
inst✝² : CommRing S
inst✝¹ : LinearOrder S
inst✝ : IsStrictOrderedRing S
abv : AbsoluteValue R S
y : R
⊢ abv (-1 • y) = abv y

Tactic:
simp

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

Goal state before:
pp: case hp.false
m n i j : ℕ
⊢ false = (j.bodd ^^ false ^^ j.bodd)

Tactic:
simp

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

Goal state before:
pp: case hp.true
m n i j : ℕ
⊢ true = (j.bodd ^^ true ^^ j.bodd)

Tactic:
simp

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

Goal state before:
pp: case hn.false
m n i j : ℕ
⊢ (!false) = (j.bodd ^^ (j.bodd ^^ false ^^ Nat.bodd 1))

Tactic:
simp

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

Goal state before:
pp: case hn.true
m n i j : ℕ
⊢ (!true) = (j.bodd ^^ (j.bodd ^^ true ^^ Nat.bodd 1))

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
d : ℕ
ds : List ℕ
inst✝ : Semiring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
⊢ (if i = ↑⟨i, ⋯⟩ then x.slice ↑⟨i, ⋯⟩ ⋯ else 0) = x.slice i hid

Tactic:
simp

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

Goal state before:
pp: case zero
⊢ fib (↑0 + 1) * fib (↑0 - 1) - fib ↑0 ^ 2 = (-1) ^ 0

Tactic:
simp

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

Goal state before:
pp: i : ℕ
hn : ¬i + 1 = 0
⊢ -↑(i + 1) + 1 = -↑i

Tactic:
simp

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

Goal state before:
pp: i : ℕ
hn : ¬i + 1 = 0
⊢ ((if Even ↑i then -fib ↑i else fib ↑i) * if Even (↑(i + 1) + 1) then -fib (↑(i + 1) + 1) else fib (↑(i + 1) + 1)) +
      -(if Even ↑(i + 1) then -fib ↑(i + 1) else fib ↑(i + 1)) ^ 2 =
    (-1) ^ (i + 1)

Tactic:
← fib_natCast_succ_mul_fib_natCast_pred_sub_fib_natCast_sq

Goal state after:
i : ℕ
hn : ¬i + 1 = 0
⊢ ((if Even ↑i then -fib ↑i else fib ↑i) * if Even (↑(i + 1) + 1) then -fib (↑(i + 1) + 1) else fib (↑(i + 1) + 1)) +
      -(if Even ↑(i + 1) then -fib ↑(i + 1) else fib ↑(i + 1)) ^ 2 =
    fib (↑(i + 1) + 1) * fib (↑(i + 1) - 1) - fib ↑(i + 1) ^ 2
Module: Mathlib.Data.Int.Lemmas

Goal state before:
pp: n : ℕ
⊢ 0 ≤ ↑n

Tactic:
simp

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

Goal state before:
pp: case true
n : ℤ
⊢ ofNat 0 = 0

Tactic:
simp

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

Goal state before:
pp: case true
n : ℤ
⊢ 1 < 2

Tactic:
simp

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

Goal state before:
pp: case negSucc.ofNat
m n : ℕ
⊢ Nat.bitwise (fun x y ↦ !(!x || y)) m n = Nat.bitwise (fun a b ↦ a && !b) m n

Tactic:
simp

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

Goal state before:
pp: case negSucc.negSucc.e_f
m n : ℕ
⊢ (fun x y ↦ !(!x || !y)) = and

Tactic:
simp

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

Goal state before:
pp: case negSucc.negSucc.e_f
m n : ℕ
⊢ (fun x y ↦ !(!x && !y)) = or

Tactic:
simp

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

Goal state before:
pp: case mpr.left
a b r q : ℤ
h : b ≠ 0
hz : 0 ≤ r
hb : r < |b|
⊢ 0 + q = q

Tactic:
simp

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

Goal state before:
pp: case ofNat.negSucc.e_f
m n : ℕ
⊢ (fun x y ↦ x && !!y) = and

Tactic:
simp

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

Goal state before:
pp: case negSucc.ofNat.e_f
m n : ℕ
⊢ (fun x y ↦ !(!x && !y)) = or

Tactic:
simp

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

Goal state before:
pp: case ofNat.negSucc
m n : ℕ
⊢ Nat.bitwise (fun x y ↦ !(x ^^ !y)) m n = Nat.bitwise xor m n

Tactic:
simp

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

Goal state before:
pp: case negSucc.ofNat
m n : ℕ
⊢ Nat.bitwise (fun x y ↦ !(!x ^^ y)) m n = Nat.bitwise xor m n

Tactic:
simp

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

Goal state before:
pp: case negSucc.negSucc
m n : ℕ
⊢ ↑(Nat.bitwise (fun x y ↦ !x ^^ !y) m n) = ↑(Nat.bitwise xor m n)

Tactic:
simp

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

Goal state before:
pp: m n : ℕ
⊢ (match ↑m, ↑n with
    | ofNat m, ofNat n => ↑(Nat.shiftLeft' false m n)
    | ofNat m, -[n+1] => ↑(m.shiftRight n.succ)
    | -[m+1], ofNat n => -[Nat.shiftLeft' true m n+1]
    | -[m+1], -[n+1] => -[m.shiftRight n.succ+1]) =
    ↑(m.shiftLeft n)

Tactic:
simp

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

Goal state before:
pp: case ofNat
n a✝ : ℕ
⊢ ofNat a✝ >>> ↑n = ofNat a✝ >>> n

Tactic:
simp

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

Goal state before:
pp: case negSucc
n a✝ : ℕ
⊢ -[a✝+1] >>> ↑n = -[a✝+1] >>> n

Tactic:
simp

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

Goal state before:
pp: n : ℕ
⊢ Nat.shiftLeft' false 0 n = 0

Tactic:
simp

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

Goal state before:
pp: a✝ : ℕ
⊢ 0 >>> a✝.succ = 0

Tactic:
simp

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

Goal state before:
pp: b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
⊢ -↑(v % r) ≤ 0

Tactic:
simp

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

Goal state before:
pp: case nil
α : Type u_1
p : α → Bool
⊢ (dropWhile p []).length ≤ [].length

Tactic:
simp

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

Goal state before:
pp: case h_2
α : Type u_1
p : α → Bool
head : α
tail : List α
ih : (dropWhile p tail).length ≤ tail.length
x✝ : Bool
heq✝ : p head = false
⊢ (head :: tail).length ≤ tail.length + 1

Tactic:
simp

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

Goal state before:
pp: case nil
α : Type u_1
p : α → Bool
⊢ dropWhile p [] = [] ↔ ∀ (hl : 0 < [].length), ¬p [][0] = true

Tactic:
simp

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

Goal state before:
pp: case nil
α : Type u_1
p : α → Bool
l : List α
⊢ takeWhile p [] = [] ↔ ∀ (x : α), x ∈ [] → p x = true

Tactic:
simp

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

Goal state before:
pp: b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
h : v % r < b % r
⊢ r ≤ r + v % r

Tactic:
simp

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

Goal state before:
pp: case nil
α : Type u
β : Type v
f : ℕ → α → β
⊢ mapIdx f [] = ofFn fun i ↦ f (↑i) ([].get i)

Tactic:
simp

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

Goal state before:
pp: case nil
α : Type u_1
p q : α → Bool
⊢ takeWhile p (takeWhile q []) = takeWhile (fun a ↦ decide (p a = true ∧ q a = true)) []

Tactic:
simp

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

Goal state before:
pp: b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
h : ¬v % r < b % r
⊢ r ≤ r + b % r

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
⊢ find? p [] = (dropWhile (fun x ↦ !p x) []).head?

Tactic:
simp

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

Goal state before:
pp: case nil
α : Type u_1
n : ℕ
⊢ take ([].length - n) [] = (drop n [].reverse).reverse

Tactic:
simp

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

Goal state before:
pp: case nil
α : Type u_1
n : ℕ
⊢ drop ([].length - n) [] = (take n [].reverse).reverse

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
hl : rdropWhile p l ≠ []
⊢ ¬false = true

Tactic:
simp

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

Goal state before:
pp: case e'_3
α : Type u_1
p : α → Bool
l : List α
x✝ : α
⊢ p x✝ = !!p x✝

Tactic:
simp

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

Goal state before:
pp: case e'_3
α : Type u_1
p : α → Bool
l : List α
h : ∃ x, x ∈ l ∧ ¬p x = true
x✝ : α
⊢ p x✝ = !!p x✝

Tactic:
simp

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

Goal state before:
pp: n m : ℕ
⊢ Pairwise (fun x1 x2 ↦ x1 < x2) (Ico n m)

Tactic:
by
  dsimp [Ico]
  simp [pairwise_lt_range']

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

Goal state before:
pp: case nil
α : Type u_1
f : α → α
a : α
r : Array α
⊢ r.toListAppend [f a] = r.toListAppend (#[].toListAppend [f a])

Tactic:
simp

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α → Option β → γ
x✝ : List β
⊢ map₂Left f [] x✝ = (map₂Left' f [] x✝).fst

Tactic:
simp

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α → Option β → γ
a : α
as : List α
⊢ map₂Left f (a :: as) [] = (map₂Left' f (a :: as) []).fst

Tactic:
simp

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α → Option β → γ
x✝ : [].length ≤ [].length
⊢ map₂Left f [] [] = zipWith (fun a b ↦ f a (some b)) [] []

Tactic:
simp

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α → Option β → γ
head✝ : β
tail✝ : List β
x✝ : [].length ≤ (head✝ :: tail✝).length
⊢ map₂Left f [] (head✝ :: tail✝) = zipWith (fun a b ↦ f a (some b)) [] (head✝ :: tail✝)

Tactic:
simp

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

Goal state before:
pp: n m : ℕ
⊢ ¬m ∈ Ico n m

Tactic:
simp

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

Goal state before:
pp: case cons
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → α → α
g : γ → α → α
hfg : Set.range f ⊆ Set.range g
a : α
b : β
l : List β
c : γ
hgf : g c = f b
m : List γ
hgf' : foldr g a m = foldr f a l
⊢ g c (foldr f a l) ∈ Set.range (foldr g a)

Tactic:
← hgf'

Goal state after:
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → α → α
g : γ → α → α
hfg : Set.range f ⊆ Set.range g
a : α
b : β
l : List β
c : γ
hgf : g c = f b
m : List γ
hgf' : foldr g a m = foldr f a l
⊢ g c (foldr g a m) ∈ Set.range (foldr g a)
Module: Mathlib.Data.List.Shortlex

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s t : List α
len_eq : s.length = t.length
h_lex : Lex r s t
⊢ Shortlex r s t

Tactic:
by
  apply Prod.lex_def.mpr
  right
  exact ⟨len_eq, h_lex⟩

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

Goal state before:
pp: α : Type u_1
l : List α
sz : List ℕ
⊢ take 0 (sz.splitLengths l) = (take 0 sz).splitLengths l

Tactic:
simp

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

Goal state before:
pp: case nil
α : Type u_1
i : ℕ
hi : ∀ (l : List α) (sz : List ℕ), take i (sz.splitLengths l) = (take i sz).splitLengths l
l : List α
⊢ take (i + 1) ([].splitLengths l) = (take (i + 1) []).splitLengths l

Tactic:
simp

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

Goal state before:
pp: case zero
α : Type u_1
head : ℕ
tail : List ℕ
tail_ih : ∀ (l : List α) {i : ℕ} {hi : i < (tail.splitLengths l).length}, (tail.splitLengths l)[i].length ≤ tail[i]
l : List α
hi : 0 < ((head :: tail).splitLengths l).length
⊢ (take head l :: tail.splitLengths (drop head l))[0].length ≤ (head :: tail)[0]

Tactic:
simp

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

Goal state before:
pp: case nil
α : Type u_1
l : List α
h : [].sum ≤ l.length
⊢ map length ([].splitLengths l) = []

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a xa : α
h✝¹ : ∀ (y : α), r y xa → Acc r y
iha :
  ∀ (y : α),
    r y xa →
      ∀ {b : List α},
        Acc (Shortlex r) b →
          (∀ (s : List α), s.length < (y :: b).length → Acc (Shortlex r) s) → Acc (Shortlex r) (y :: b)
b xb : List α
h✝ : ∀ (y : List α), Shortlex r y xb → Acc (Shortlex r) y
ihb :
  ∀ (y : List α),
    Shortlex r y xb → (∀ (s : List α), s.length < (xa :: y).length → Acc (Shortlex r) s) → Acc (Shortlex r) (xa :: y)
ih : ∀ (s : List α), s.length < (xa :: xb).length → Acc (Shortlex r) s
x : α
xs : List α
lt : Shortlex r (x :: xs) (xa :: xb)
h : r x xa
h2len : xs.length = xb.length
⊢ xb.length < (xa :: xb).length

Tactic:
simp

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

Goal state before:
pp: case h_2
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α} (gs : List (List α)), splitBy.loop r l a g gs = gs.reverse ++ splitBy.loop r l a g []
a : α
g : List α
gs : List (List α)
x✝ : Bool
heq✝ : r a b = false
⊢ ((a :: g).reverse :: gs).reverse ++ splitBy.loop r l b [] [] =
    gs.reverse ++ ([(a :: g).reverse].reverse ++ splitBy.loop r l b [] [])

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
r : α → α → Bool
l : List α
hn : l ≠ []
⊢ ((splitBy r l).head ⋯).head ⋯ = l.head hn

Tactic:
by
  simp [head_head_eq_head_flatten]

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

Goal state before:
pp: α : Type u_1
p : ℕ
⊢ [].HasPeriod p

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
u v w : List α
p : ℕ
per : (u ++ v ++ w).HasPeriod p
⊢ ∀ j < v.length - p, v[j]? = v[j + p]?

Tactic:
intro j

Goal state after:
α : Type u_1
u v w : List α
p : ℕ
per : (u ++ v ++ w).HasPeriod p
j : ℕ
⊢ j < v.length - p → v[j]? = v[j + p]?
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: α : Type u_1
m : List α
r : α → α → Bool
l✝ : List α
h✝ : m ∈ splitBy r l✝
a : α
l : List α
h : m ∈ splitBy r (a :: l)
⊢ ∀ (b : α), b ∈ [].head? → r b a = true

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
m : List α
r : α → α → Bool
l✝ : List α
h✝ : m ∈ splitBy r l✝
a : α
l : List α
h : m ∈ splitBy r (a :: l)
⊢ IsChain (fun y x ↦ r x y = true) []

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
u v w : List α
p : ℕ
per : (u ++ v ++ w).HasPeriod p
j : ℕ
len : j < v.length - p
shift_position : (u ++ (v ++ w))[j + u.length]? = v[j]?
shift_position' : (u ++ (v ++ w))[j + u.length + p]? = v[j + p]?
this : ∀ i < u.length + (v.length + w.length) - p, (u ++ (v ++ w))[i]? = (u ++ (v ++ w))[i + p]?
⊢ v[j]? = v[j + p]?

Tactic:
← shift_position',

Goal state after:
α : Type u_1
u v w : List α
p : ℕ
per : (u ++ v ++ w).HasPeriod p
j : ℕ
len : j < v.length - p
shift_position : (u ++ (v ++ w))[j + u.length]? = v[j]?
shift_position' : (u ++ (v ++ w))[j + u.length + p]? = v[j + p]?
this : ∀ i < u.length + (v.length + w.length) - p, (u ++ (v ++ w))[i]? = (u ++ (v ++ w))[i + p]?
⊢ v[j]? = (u ++ (v ++ w))[j + u.length + p]?
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: case h_2.hgs
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α} {gs : List (List α)},
    ¬[] ∈ gs →
      IsChain (fun b a ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) gs →
        (∀ (m : List α), m ∈ gs.head? → ∃ ha hb, r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false) →
          IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) (splitBy.loop r l a g gs)
a : α
g : List α
gs : List (List α)
hgs' : ¬[] ∈ gs
hgs : IsChain (fun b a ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) gs
hga : ∀ (m : List α), m ∈ gs.head? → ∃ ha hb, r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false
x✝ : Bool
heq✝ : r a b = false
⊢ IsChain (fun b a ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) ((a :: g).reverse :: gs)

Tactic:
rw [reverse_cons]

Goal state after:
case h_2.hgs
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α} {gs : List (List α)},
    ¬[] ∈ gs →
      IsChain (fun b a ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) gs →
        (∀ (m : List α), m ∈ gs.head? → ∃ ha hb, r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false) →
          IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) (splitBy.loop r l a g gs)
a : α
g : List α
gs : List (List α)
hgs' : ¬[] ∈ gs
hgs : IsChain (fun b a ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) gs
hga : ∀ (m : List α), m ∈ gs.head? → ∃ ha hb, r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false
x✝ : Bool
heq✝ : r a b = false
⊢ IsChain (fun b a ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) ((g.reverse ++ [a]) :: gs)
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: α : Type u_1
p n : ℕ
w : List α
dvd : p ∣ n
len : n ≤ w.length
per : w.HasPeriod p
p_pos : p > 0
pos : n > 0
mod_w : ∀ i < w.length, w[i % p]? = w[i]?
i : ℕ
less_i : i < n + w.length
⊢ ∀ j < n + w.length, (take n w ++ w)[j]? = w[j % p]?

Tactic:
intro j

Goal state after:
α : Type u_1
p n : ℕ
w : List α
dvd : p ∣ n
len : n ≤ w.length
per : w.HasPeriod p
p_pos : p > 0
pos : n > 0
mod_w : ∀ i < w.length, w[i % p]? = w[i]?
i : ℕ
less_i : i < n + w.length
j : ℕ
⊢ j < n + w.length → (take n w ++ w)[j]? = w[j % p]?
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: case cons
α : Type u_1
m : List α
r : α → α → Bool
a : α
l : List α
hn : a :: l ≠ []
h : IsChain (fun x y ↦ r x y = true) (a :: l)
ha : ∀ (x : α), x ∈ m.head? → r ((a :: l).getLast hn) x = false
⊢ ([].reverse ++ a :: l) :: splitBy r m = (a :: l) :: splitBy r m

Tactic:
simp

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

Goal state before:
pp: case inl
α : Type u_1
r : α → α → Bool
m : List α
ha : ∀ (x : α), x ∈ [].getLast? → ∀ (y : α), y ∈ m.head? → r x y = false
⊢ splitBy r ([] ++ m) = splitBy r [] ++ splitBy r m

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: α : 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 ≠ []
⊢ l ++ m = (splitBy r l ++ splitBy r m).flatten

Tactic:
simp

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

Goal state before:
pp: α : 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 ≠ []
⊢ ¬[] ∈ splitBy r l ++ splitBy r m

Tactic:
simp

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

Tactic:
aesop (add apply unsafe isChain_of_mem_splitBy)

Goal state after:
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: case inl
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
A : Matrix m (n₁ ⊕ n₂) R
i : m
j : n₁
⊢ A.toCols₁.fromCols A.toCols₂ i (Sum.inl j) = A i (Sum.inl j)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: case inr
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
A : Matrix m (n₁ ⊕ n₂) R
i : m
j : n₂
⊢ A.toCols₁.fromCols A.toCols₂ i (Sum.inr j) = A i (Sum.inr j)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: case inl
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
A : Matrix (m₁ ⊕ m₂) n R
i : m₁
j : n
⊢ A.toRows₁.fromRows A.toRows₂ (Sum.inl i) j = A (Sum.inl i) j

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: case inr
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
A : Matrix (m₁ ⊕ m₂) n R
i : m₂
j : n
⊢ A.toRows₁.fromRows A.toRows₂ (Sum.inr i) j = A (Sum.inr i) j

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: case inl
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
A₁ : Matrix m n₁ R
A₂ : Matrix m n₂ R
i : n₁
j : m
⊢ (A₁.fromCols A₂)ᵀ (Sum.inl i) j = A₁ᵀ.fromRows A₂ᵀ (Sum.inl i) j

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: case inr
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
A₁ : Matrix m n₁ R
A₂ : Matrix m n₂ R
i : n₂
j : m
⊢ (A₁.fromCols A₂)ᵀ (Sum.inr i) j = A₁ᵀ.fromRows A₂ᵀ (Sum.inr i) j

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: case inl
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
i : n
j : m₁
⊢ (A₁.fromRows A₂)ᵀ i (Sum.inl j) = A₁ᵀ.fromCols A₂ᵀ i (Sum.inl j)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: case inr
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
i : n
j : m₂
⊢ (A₁.fromRows A₂)ᵀ i (Sum.inr j) = A₁ᵀ.fromCols A₂ᵀ i (Sum.inr j)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: case inl
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst✝ : Neg R
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
i : m₁
j : n
⊢ (-A₁.fromRows A₂) (Sum.inl i) j = (-A₁).fromRows (-A₂) (Sum.inl i) j

Tactic:
simp

Goal state after: