mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: σ : Type u
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative G
inst✝ : LawfulApplicative F
η : ApplicativeTransformation F G
α : Type u_1
β : Type u
f : α → F β
x : σ ⊕ α
⊢ (fun {α} ↦ η.app α) (Sum.traverse f x) = Sum.traverse ((fun {α} ↦ η.app α) ∘ f) x

Tactic:
cases x

Goal state after:
case inl
σ : Type u
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative G
inst✝ : LawfulApplicative F
η : ApplicativeTransformation F G
α : Type u_1
β : Type u
f : α → F β
val✝ : σ
⊢ (fun {α} ↦ η.app α) (Sum.traverse f (inl val✝)) = Sum.traverse ((fun {α} ↦ η.app α) ∘ f) (inl val✝)

case inr
σ : Type u
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative G
inst✝ : LawfulApplicative F
η : ApplicativeTransformation F G
α : Type u_1
β : Type u
f : α → F β
val✝ : α
⊢ (fun {α} ↦ η.app α) (Sum.traverse f (inr val✝)) = Sum.traverse ((fun {α} ↦ η.app α) ∘ f) (inr val✝)
Module: Mathlib.Control.Fold

Goal state before:
pp: α : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
xs : t α
⊢ ((ConcreteCategory.hom (unop ((Foldl.ofFreeMonoid (flip cons)) (foldMap FreeMonoid.of xs)))) []).reverse = toList xs

Tactic:
rw [foldMap_hom_free (Foldl.ofFreeMonoid (flip <| @cons α))]

Goal state after:
α : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
xs : t α
⊢ ((ConcreteCategory.hom (unop (foldMap (⇑(Foldl.ofFreeMonoid (flip cons)) ∘ FreeMonoid.of) xs))) []).reverse =
    toList xs
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
α : TypeVec.{u} n
β : TypeVec.{v} n
f g : α ⟹ β
⊢ (∀ (i : Fin2 n), f i = g i) → f = g

Tactic:
intro h

Goal state after:
n : ℕ
α : TypeVec.{u} n
β : TypeVec.{v} n
f g : α ⟹ β
h : ∀ (i : Fin2 n), f i = g i
⊢ f = g
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
α : TypeVec.{u_1} (n + 1)
β : TypeVec.{u_2} (n + 1)
f g : α ⟹ β
h₀ : dropFun f = dropFun g
h₁ : lastFun f = lastFun g
x : Fin2 (n + 1)
⊢ f x = g x

Tactic:
cases x

Goal state after:
case fz
n : ℕ
α : TypeVec.{u_1} (n + 1)
β : TypeVec.{u_2} (n + 1)
f g : α ⟹ β
h₀ : dropFun f = dropFun g
h₁ : lastFun f = lastFun g
⊢ f Fin2.fz = g Fin2.fz

case fs
n : ℕ
α : TypeVec.{u_1} (n + 1)
β : TypeVec.{u_2} (n + 1)
f g : α ⟹ β
h₀ : dropFun f = dropFun g
h₁ : lastFun f = lastFun g
a✝ : Fin2 n
⊢ f a✝.fs = g a✝.fs
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: m : Type u → Type v
inst✝ : Monad m
α β ε : Type u
x : Label (Except ε α) m β
i : α
⊢ goto (mkLabel x) i = mk (Except.ok <$> goto x (Except.ok i))

Tactic:
cases x

Goal state after:
case mk
m : Type u → Type v
inst✝ : Monad m
α β ε : Type u
i : α
apply✝ : Except ε α → m β
⊢ goto (mkLabel { apply := apply✝ }) i = mk (Except.ok <$> goto { apply := apply✝ } (Except.ok i))
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: m : Type u → Type v
inst✝¹ : Monad m
α : Type u_1
β ω : Type u
inst✝ : EmptyCollection ω
x : Label (α × ω) m β
i : α
⊢ goto (mkLabel x) i = monadLift (goto x (i, ∅))

Tactic:
cases x

Goal state after:
case mk
m : Type u → Type v
inst✝¹ : Monad m
α : Type u_1
β ω : Type u
inst✝ : EmptyCollection ω
i : α
apply✝ : α × ω → m β
⊢ goto (mkLabel { apply := apply✝ }) i = monadLift (goto { apply := apply✝ } (i, ∅))
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: m : Type u → Type v
inst✝¹ : Monad m
α : Type u_1
β ω : Type u
inst✝ : Monoid ω
x : Label (α × ω) m β
i : α
⊢ goto (mkLabel' x) i = monadLift (goto x (i, 1))

Tactic:
cases x

Goal state after:
case mk
m : Type u → Type v
inst✝¹ : Monad m
α : Type u_1
β ω : Type u
inst✝ : Monoid ω
i : α
apply✝ : α × ω → m β
⊢ goto (mkLabel' { apply := apply✝ }) i = monadLift (goto { apply := apply✝ } (i, 1))
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: m : Type u → Type v
α β σ : Type u
x : Label (α × σ) m (β × σ)
i : α
⊢ goto (mkLabel x) i = mk fun s ↦ goto x (i, s)

Tactic:
cases x

Goal state after:
case mk
m : Type u → Type v
α β σ : Type u
i : α
apply✝ : α × σ → m (β × σ)
⊢ goto (mkLabel { apply := apply✝ }) i = mk fun s ↦ goto { apply := apply✝ } (i, s)
Module: Mathlib.Data.TypeVec

Goal state before:
pp: α : TypeVec.{u_1} 0
β : TypeVec.{u_2} 0
f : α ⟹ β
x : Fin2 0
x✝ : α x
⊢ f x x✝ = nilFun x x✝

Tactic:
cases x

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: α : TypeVec.{u_1} 0
x : Fin2 0
x✝ : α x
⊢ id x x✝ = nilFun x x✝

Tactic:
cases x

Goal state after:
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: m : Type u → Type v
α : Type u_1
ρ β : Type u
x : Label α m β
i : α
⊢ goto (mkLabel ρ x) i = monadLift (goto x i)

Tactic:
cases x

Goal state after:
case mk
m : Type u → Type v
α : Type u_1
ρ β : Type u
i : α
apply✝ : α → m β
⊢ goto (mkLabel ρ { apply := apply✝ }) i = monadLift (goto { apply := apply✝ } i)
Module: Mathlib.Data.Bool.Count

Goal state before:
pp: b x : Bool
l : List Bool
h : IsChain (fun x1 x2 ↦ x1 ≠ x2) (b :: x :: l)
⊢ count (!b) (x :: l) = count b (x :: l) + (x :: l).length % 2

Tactic:
by
    grind [h.of_cons.count_not_cons]

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Embedding

Goal state before:
pp: α : Type u_1
e : Fin 2 ↪ α
⊢ (fun x ↦
        match x with
        | ⟨(a, b), h⟩ => { toFun := fun i ↦ if i = 0 then a else b, inj' := ⋯ })
      ((fun e ↦ ⟨(e 0, e 1), ⋯⟩) e) =
    e

Tactic:
by
    ext i
    by_cases hi : i = 0
    · simp [hi]
    · simp [Fin.eq_one_of_ne_zero i hi]

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β✝ : α → Type v
β : Type ?u.23
inst✝¹ : FinEnum α
inst✝ : FinEnum β
x : α × β
⊢ x ∈ toList α ×ˢ toList β

Tactic:
cases x

Goal state after:
case mk
α : Type u
β✝ : α → Type v
β : Type ?u.23
inst✝¹ : FinEnum α
inst✝ : FinEnum β
fst✝ : α
snd✝ : β
⊢ (fst✝, snd✝) ∈ toList α ×ˢ toList β
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β✝ : α → Type v
β : Type ?u.12
inst✝¹ : FinEnum α
inst✝ : FinEnum β
x : α ⊕ β
⊢ x ∈ List.map Sum.inl (toList α) ++ List.map Sum.inr (toList β)

Tactic:
cases x

Goal state after:
case inl
α : Type u
β✝ : α → Type v
β : Type ?u.12
inst✝¹ : FinEnum α
inst✝ : FinEnum β
val✝ : α
⊢ Sum.inl val✝ ∈ List.map Sum.inl (toList α) ++ List.map Sum.inr (toList β)

case inr
α : Type u
β✝ : α → Type v
β : Type ?u.12
inst✝¹ : FinEnum α
inst✝ : FinEnum β
val✝ : β
⊢ Sum.inr val✝ ∈ List.map Sum.inl (toList α) ++ List.map Sum.inr (toList β)
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β✝ β : α → Type v
inst✝¹ : FinEnum α
inst✝ : (a : α) → FinEnum (β a)
x : Sigma β
⊢ x ∈ List.flatMap (fun a ↦ List.map (Sigma.mk a) (toList (β a))) (toList α)

Tactic:
cases x

Goal state after:
case mk
α : Type u
β✝ β : α → Type v
inst✝¹ : FinEnum α
inst✝ : (a : α) → FinEnum (β a)
fst✝ : α
snd✝ : β fst✝
⊢ ⟨fst✝, snd✝⟩ ∈ List.flatMap (fun a ↦ List.map (Sigma.mk a) (toList (β a))) (toList α)
Module: Mathlib.Data.List.AList

Goal state before:
pp: case mpr.inl
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint s₂
x✝ : α
y✝ : β x✝
h' : dlookup x✝ s₂.entries = some y✝
⊢ dlookup x✝ s₁.entries = some y✝ ∨ ¬x✝ ∈ s₁.entries.keys ∧ dlookup x✝ s₂.entries = some y✝

pp: case mpr.inr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint s₂
x✝ : α
y✝ : β x✝
h' : ¬x✝ ∈ s₂.entries.keys ∧ dlookup x✝ s₁.entries = some y✝
⊢ dlookup x✝ s₁.entries = some y✝ ∨ ¬x✝ ∈ s₁.entries.keys ∧ dlookup x✝ s₂.entries = some y✝

Tactic:
· right
          refine ⟨?_, h'⟩
          intro h''
          apply h _ h''
          rw [keys, ← List.dlookup_isSome, h']
          exact rfl

Goal state after:
case mpr.inr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint s₂
x✝ : α
y✝ : β x✝
h' : ¬x✝ ∈ s₂.entries.keys ∧ dlookup x✝ s₁.entries = some y✝
⊢ dlookup x✝ s₁.entries = some y✝ ∨ ¬x✝ ∈ s₁.entries.keys ∧ dlookup x✝ s₂.entries = some y✝
Module: Mathlib.Data.Finmap

Goal state before:
pp: case cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
x : Sigma β
xs : List (Sigma β)
tail_ih✝ : a ∈ xs.toFinmap ↔ ∃ b, ⟨a, b⟩ ∈ xs
⊢ a ∈ (x :: xs).toFinmap ↔ ∃ b, ⟨a, b⟩ ∈ x :: xs

Tactic:
obtain ⟨fst_i, snd_i⟩ := x

Goal state after:
case cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
xs : List (Sigma β)
tail_ih✝ : a ∈ xs.toFinmap ↔ ∃ b, ⟨a, b⟩ ∈ xs
fst_i : α
snd_i : β fst_i
⊢ a ∈ (⟨fst_i, snd_i⟩ :: xs).toFinmap ↔ ∃ b, ⟨a, b⟩ ∈ ⟨fst_i, snd_i⟩ :: xs
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁✝ s₂✝ : Finmap β
s₁ s₂ : AList β
⊢ ⟦s₁⟧.Disjoint ⟦s₂⟧ → ⟦s₁⟧ ∪ ⟦s₂⟧ = ⟦s₂⟧ ∪ ⟦s₁⟧

Tactic:
intro h

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁✝ s₂✝ : Finmap β
s₁ s₂ : AList β
h : ⟦s₁⟧.Disjoint ⟦s₂⟧
⊢ ⟦s₁⟧ ∪ ⟦s₂⟧ = ⟦s₂⟧ ∪ ⟦s₁⟧
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l' : List (Sigma β)
this : l'.NodupKeys
x : Sigma β
xs : List (Sigma β)
l_ih : (foldr (fun x ↦ kinsert x.fst x.snd) l' xs).NodupKeys
⊢ (foldr (fun x ↦ kinsert x.fst x.snd) l' (x :: xs)).NodupKeys

Tactic:
cases x

Goal state after:
case cons.mk
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l' : List (Sigma β)
this : l'.NodupKeys
xs : List (Sigma β)
l_ih : (foldr (fun x ↦ kinsert x.fst x.snd) l' xs).NodupKeys
fst✝ : α
snd✝ : β fst✝
⊢ (foldr (fun x ↦ kinsert x.fst x.snd) l' (⟨fst✝, snd✝⟩ :: xs)).NodupKeys
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case cons.mk.left
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l' : List (Sigma β)
this : l'.NodupKeys
xs : List (Sigma β)
l_ih : (foldr (fun x ↦ kinsert x.fst x.snd) l' xs).NodupKeys
fst✝ : α
snd✝ : β fst✝
⊢ ¬fst✝ ∈ (kerase fst✝ (foldr (fun x ↦ kinsert x.fst x.snd) l' xs)).keys

Tactic:
simp only [keys_kerase]

Goal state after:
case cons.mk.left
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l' : List (Sigma β)
this : l'.NodupKeys
xs : List (Sigma β)
l_ih : (foldr (fun x ↦ kinsert x.fst x.snd) l' xs).NodupKeys
fst✝ : α
snd✝ : β fst✝
⊢ ¬fst✝ ∈ (foldr (fun x ↦ kinsert x.fst x.snd) l' xs).keys.erase fst✝
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u_1
inst✝ : SizeOf α
l r : List α
a : α
h : sizeOf l ≤ sizeOf r
⊢ 1 + sizeOf a + sizeOf l ≤ sizeOf (a :: r)

Tactic:
cons.sizeOf_spec

Goal state after:
α : Type u_1
inst✝ : SizeOf α
l r : List α
a : α
h : sizeOf l ≤ sizeOf r
⊢ 1 + sizeOf a + sizeOf l ≤ 1 + sizeOf a + sizeOf r
Module: Mathlib.Data.Finset.PImage

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
f : α →. β
inst✝ : (x : α) → Decidable (f x).Dom
s : Finset α
b : β
⊢ b ∈ pimage f s ↔ ∃ a ∈ s, b ∈ f a

Tactic:
simp [pimage]

Goal state after:
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
⊢ Multiset.Pairwise (Disjoint on Finsupp.support) s.val

Tactic:
obtain ⟨l, hl, hn⟩ : ∃ l : List (ι →₀ M), l.toFinset = s ∧ l.Nodup := by
    refine ⟨s.toList, ?_, Finset.nodup_toList _⟩
    simp

Goal state after:
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Finset (ι →₀ M)
hs : (↑s).PairwiseDisjoint Finsupp.support
l : List (ι →₀ M)
hl : l.toFinset = s
hn : l.Nodup
⊢ Multiset.Pairwise (Disjoint on Finsupp.support) s.val
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)).natAbs

Tactic:
natAbs_natCast,

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 =
    (-1) ^ (i + 1)
Module: Mathlib.Data.Int.Bitwise

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

Tactic:
cases x

Goal state after:
case ofNat.negSucc.e_f.false
m n : ℕ
y : Bool
⊢ (!(y || !false)) = (false && !y)

case ofNat.negSucc.e_f.true
m n : ℕ
y : Bool
⊢ (!(y || !true)) = (true && !y)
Module: Mathlib.Data.Int.Bitwise

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

Tactic:
cases x

Goal state after:
case negSucc.ofNat.e_f.false
m n : ℕ
y : Bool
⊢ (!y && false) = (false && !y)

case negSucc.ofNat.e_f.true
m n : ℕ
y : Bool
⊢ (!y && true) = (true && !y)
Module: Mathlib.Data.Int.Bitwise

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

Tactic:
cases x

Goal state after:
case negSucc.negSucc.e_f.false
m n : ℕ
y : Bool
⊢ (!y && !!false) = (false && !y)

case negSucc.negSucc.e_f.true
m n : ℕ
y : Bool
⊢ (!y && !!true) = (true && !y)
Module: Mathlib.Data.LawfulXor.Basic

Goal state before:
pp: α : Type u_1
inst✝² : XorOp α
inst✝¹ : Zero α
inst✝ : LawfulXor α
a : α
⊢ (fun x ↦ x ^^^ a) = id ↔ a = 0

Tactic:
by
  rw [xor_right_eq, xor_left_eq_id_iff]

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

Goal state before:
pp: case mpr
a b r v : ℕ
x : ℤ
⊢ (↑a ≤ x ∧ x < ↑b) ∧ x ≡ ↑v [ZMOD ↑r] → ∃ a_2, ((a ≤ a_2 ∧ a_2 < b) ∧ a_2 ≡ v [MOD r]) ∧ ↑a_2 = x

Tactic:
intro h

Goal state after:
case mpr
a b r v : ℕ
x : ℤ
h : (↑a ≤ x ∧ x < ↑b) ∧ x ≡ ↑v [ZMOD ↑r]
⊢ ∃ a_1, ((a ≤ a_1 ∧ a_1 < b) ∧ a_1 ≡ v [MOD r]) ∧ ↑a_1 = x
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: case mpr
a b r v : ℕ
x : ℤ
⊢ (↑a < x ∧ x ≤ ↑b) ∧ x ≡ ↑v [ZMOD ↑r] → ∃ a_2, ((a < a_2 ∧ a_2 ≤ b) ∧ a_2 ≡ v [MOD r]) ∧ ↑a_2 = x

Tactic:
intro h

Goal state after:
case mpr
a b r v : ℕ
x : ℤ
h : (↑a < x ∧ x ≤ ↑b) ∧ x ≡ ↑v [ZMOD ↑r]
⊢ ∃ a_1, ((a < a_1 ∧ a_1 ≤ b) ∧ a_1 ≡ v [MOD r]) ∧ ↑a_1 = x
Module: Mathlib.Data.List.TakeWhile

Goal state before:
pp: case pos
α : Type u_1
p : α → Bool
hd : α
tl : List α
h_p_hd : p hd = true
⊢ ¬dropWhile p tl = hd :: tl

Tactic:
intro h

Goal state after:
case pos
α : Type u_1
p : α → Bool
hd : α
tl : List α
h_p_hd : p hd = true
h : dropWhile p tl = hd :: tl
⊢ False
Module: Mathlib.Data.List.TakeWhile

Goal state before:
pp: case nil
α : Type u_1
p : α → Bool
l : List α
⊢ ∀ (hl : 0 < [].length), p ([].get ⟨0, hl⟩) = false

Tactic:
intro h

Goal state after:
case nil
α : Type u_1
p : α → Bool
l : List α
h : 0 < [].length
⊢ p ([].get ⟨0, h⟩) = false
Module: Mathlib.Data.List.TakeWhile

Goal state before:
pp: case cons.false
α : Type u_1
p : α → Bool
l : List α
x hd : α
tl : List α
IH : x ∈ takeWhile p tl → p x = true
hx :
  x ∈
    match p hd with
    | true => hd :: takeWhile p tl
    | false => []
hp : p hd = false
⊢ p x = true

Tactic:
simp [hp] at hx

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

Goal state before:
pp: n m : ℕ
hnm : n < m
r : min m (n + 1) = n + 1
⊢ filter (fun x ↦ decide (x < n + 1)) (Ico n m) = [n]

Tactic:
simp [filter_lt n m (n + 1), r]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Bilinear

Goal state before:
pp: case mp
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : Semiring R
inst✝³ : Semiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : Nonempty n
a : Matrix l m A
⊢ mulLeftLinearMap n R a = 0 → a = 0

Tactic:
intro h

Goal state after:
case mp
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : Semiring R
inst✝³ : Semiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : Nonempty n
a : Matrix l m A
h : mulLeftLinearMap n R a = 0
⊢ a = 0
Module: Mathlib.LinearAlgebra.Matrix.Bilinear

Goal state before:
pp: case mpr
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : Semiring R
inst✝³ : Semiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : Nonempty n
a : Matrix l m A
⊢ a = 0 → mulLeftLinearMap n R a = 0

Tactic:
intro h

Goal state after:
case mpr
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : Semiring R
inst✝³ : Semiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : Nonempty n
a : Matrix l m A
h : a = 0
⊢ mulLeftLinearMap n R a = 0
Module: Mathlib.LinearAlgebra.Matrix.Bilinear

Goal state before:
pp: case mp
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : Semiring R
inst✝³ : Semiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
a : Matrix m n A
inst✝ : Nonempty l
⊢ mulRightLinearMap l R a = 0 → a = 0

Tactic:
intro h

Goal state after:
case mp
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : Semiring R
inst✝³ : Semiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
a : Matrix m n A
inst✝ : Nonempty l
h : mulRightLinearMap l R a = 0
⊢ a = 0
Module: Mathlib.LinearAlgebra.Matrix.Bilinear

Goal state before:
pp: case mpr
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : Semiring R
inst✝³ : Semiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
a : Matrix m n A
inst✝ : Nonempty l
⊢ a = 0 → mulRightLinearMap l R a = 0

Tactic:
intro h

Goal state after:
case mpr
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : Semiring R
inst✝³ : Semiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
a : Matrix m n A
inst✝ : Nonempty l
h : a = 0
⊢ mulRightLinearMap l R a = 0
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: case inr.inr.gt
α : 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
⊢ w.HasPeriod (p.gcd q)

Tactic:
have drop_len : q ≤ (drop q w).length := by
        rw [length_drop]
        have : p.gcd q ≤ p - q := by
          rw [← gcd_stable]; apply gcd_le_left q; lia
        lia

Goal state after:
case inr.inr.gt
α : 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
⊢ w.HasPeriod (p.gcd q)
Module: Mathlib.LinearAlgebra.Matrix.DualNumber

Goal state before:
pp: case h1
R n : Type
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A B : Matrix n n (DualNumber R)
i✝ j✝ : n
⊢ fst (of fun i j ↦ fst ((A * B) i j), of fun i j ↦ snd ((A * B) i j)) i✝ j✝ =
    fst ((of fun i j ↦ fst (A i j), of fun i j ↦ snd (A i j)) * (of fun i j ↦ fst (B i j), of fun i j ↦ snd (B i j))) i✝
      j✝

Tactic:
dsimp [mul_apply]
      simp_rw [fst_sum]
      rfl

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

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

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

Tactic:
· obtain ⟨z, hz, hyz⟩ := hYZ₁ y hy
    by_cases z_in : z ∈ Y₂
    · obtain ⟨w, hw, hzw⟩ := hYZ₂ z z_in
      exact ⟨w, .inl hw, hyz.trans hzw⟩
    · exact ⟨z, .inr <| by rwa [mem_sub, count_eq_zero_of_notMem z_in, count_pos], hyz⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
M N : Multiset α
a : α
h : N.OneStep (a ::ₘ M)
⊢ ∃ M', N = a ::ₘ M' ∧ M'.OneStep M ∨ N = M + M' ∧ ∀ (x : α), x ∈ M' → x < a

Tactic:
obtain ⟨X, Y, b, rfl, h0, h2⟩ := h

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

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

Tactic:
toNNRat_coe

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

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

Tactic:
intro h

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

Goal state before:
pp: case cons.mpr
a b m : ℕ
l : List ℕ
ih : List.Pairwise Coprime l → (a ≡ b [MOD l.prod] ↔ ∀ (i : Fin l.length), a ≡ b [MOD l.get i])
co : List.Pairwise Coprime (m :: l)
this : m.Coprime l.prod
⊢ (∀ (i : Fin (l.length + 1)), a ≡ b [MOD (m :: l).get i]) → a ≡ b [MOD m] ∧ ∀ (i : Fin l.length), a ≡ b [MOD l.get i]

Tactic:
intro h

Goal state after:
case cons.mpr
a b m : ℕ
l : List ℕ
ih : List.Pairwise Coprime l → (a ≡ b [MOD l.prod] ↔ ∀ (i : Fin l.length), a ≡ b [MOD l.get i])
co : List.Pairwise Coprime (m :: l)
this : m.Coprime l.prod
h : ∀ (i : Fin (l.length + 1)), a ≡ b [MOD (m :: l).get i]
⊢ a ≡ b [MOD m] ∧ ∀ (i : Fin l.length), a ≡ b [MOD l.get i]
Module: Mathlib.Data.Nat.Factorization.Root

Goal state before:
pp: a : ℕ
⊢ floorRoot 0 a = 0

Tactic:
by simp [floorRoot]

Goal state after:
Module: Mathlib.Data.Nat.Factorization.Root

Goal state before:
pp: n : ℕ
⊢ n.floorRoot 0 = 0

Tactic:
by simp [floorRoot]

Goal state after:
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: case mp
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
x₁ x₂ : ℕ
hx : (x₁, x₂) ∈ range (n % p + 1) ×ˢ range (n / p + 1)
⊢ k = (x₁, x₂).1 + p * (x₁, x₂).2 → k % p = x₁ ∧ k / p = x₂

Tactic:
intro h

Goal state after:
case mp
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
x₁ x₂ : ℕ
hx : (x₁, x₂) ∈ range (n % p + 1) ×ˢ range (n / p + 1)
h : k = (x₁, x₂).1 + p * (x₁, x₂).2
⊢ k % p = x₁ ∧ k / p = x₂
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: case mpr
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
x₁ x₂ : ℕ
hx : (x₁, x₂) ∈ range (n % p + 1) ×ˢ range (n / p + 1)
⊢ k % p = x₁ ∧ k / p = x₂ → k = (x₁, x₂).1 + p * (x₁, x₂).2

Tactic:
intro h

Goal state after:
case mpr
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
x₁ x₂ : ℕ
hx : (x₁, x₂) ∈ range (n % p + 1) ×ˢ range (n / p + 1)
h : k % p = x₁ ∧ k / p = x₂
⊢ k = (x₁, x₂).1 + p * (x₁, x₂).2
Module: Mathlib.Data.Nat.Fib.Zeckendorf

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ (n - fib n.greatestFib).greatestFib ≤ n.greatestFib - 2

Tactic:
← Nat.lt_succ_iff,

Goal state after:
n : ℕ
hn : n ≠ 0
⊢ (n - fib n.greatestFib).greatestFib < (n.greatestFib - 2).succ
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
hf : (Set.ofPred p).Infinite
this : Infinite ↑(Set.ofPred p)
⊢ Set.range (Subtype.val ∘ ⇑(Subtype.orderIsoOfNat (Set.ofPred p))) = Set.ofPred p

Tactic:
classical exact Nat.Subtype.coe_comp_ofNat_range

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

Goal state before:
pp: case neg
p : ℕ → Prop
a b : ℕ
hab : a ≤ b
h : p (nth p b)
h' : ∃ (h : (Set.ofPred p).Finite), #⋯.toFinset ≤ a
h'b : ∃ (hf : (Set.ofPred p).Finite), #hf.toFinset ≤ b
ha0 : nth p a = 0
⊢ p (nth p a)

Tactic:
have hb0 : nth p b = 0 := by simp [nth_eq_zero, h'b]

Goal state after:
case neg
p : ℕ → Prop
a b : ℕ
hab : a ≤ b
h : p (nth p b)
h' : ∃ (h : (Set.ofPred p).Finite), #⋯.toFinset ≤ a
h'b : ∃ (hf : (Set.ofPred p).Finite), #hf.toFinset ≤ b
ha0 : nth p a = 0
hb0 : nth p b = 0
⊢ p (nth p a)