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

Goal state before:
pp: t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
G : Type u → Type u
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
g : α → G β
h : β → γ
⊢ traverse (map h ∘ g) = map (map h) ∘ traverse g

Tactic:
ext
  rw [comp_apply, map_traverse]

Goal state after:
Module: Mathlib.Condensed.Light.InternallyProjective

Goal state before:
pp: case refine_2
R : Type u
inst✝ : CommRing R
P : LightProfinite
h :
  ∀ {A B : LightCondMod R} (e : A ⟶ B) [Epi e] (S : LightProfinite) (g : (free R).obj (P ⊗ S).toCondensed ⟶ B),
    ∃ S' π,
      ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
        ∃ g', (free R).map (lightProfiniteToLightCondSet.map (P ◁ π)) ≫ g = g' ≫ e
A B : LightCondMod R
e : A ⟶ B
he : Epi e
S : LightProfinite
g : (free R).obj (P.toCondensed ⊗ S.toCondensed) ⟶ B
⊢ ∃ S' π,
    ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
      ∃ g', (free R).map (P.toCondensed ◁ lightProfiniteToLightCondSet.map π) ≫ g = g' ≫ e

Tactic:
specialize h e S ((free R).map (μIso lightProfiniteToLightCondSet _ _).inv ≫ g)

Goal state after:
case refine_2
R : Type u
inst✝ : CommRing R
P : LightProfinite
A B : LightCondMod R
e : A ⟶ B
he : Epi e
S : LightProfinite
g : (free R).obj (P.toCondensed ⊗ S.toCondensed) ⟶ B
h :
  ∃ S' π,
    ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
      ∃ g',
        (free R).map (lightProfiniteToLightCondSet.map (P ◁ π)) ≫
            (free R).map (μIso lightProfiniteToLightCondSet P S).inv ≫ g =
          g' ≫ e
⊢ ∃ S' π,
    ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
      ∃ g', (free R).map (P.toCondensed ◁ lightProfiniteToLightCondSet.map π) ≫ g = g' ≫ e
Module: Mathlib.Condensed.Light.InternallyProjective

Goal state before:
pp: case refine_2
R : Type u
inst✝ : CommRing R
P : LightProfinite
h :
  ∀ {A B : LightCondMod R} (e : A ⟶ B) [Epi e] (S : LightProfinite) (g : (free R).obj (S ⊗ P).toCondensed ⟶ B),
    ∃ S' π,
      ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
        ∃ g', (free R).map (lightProfiniteToLightCondSet.map (π ▷ P)) ≫ g = g' ≫ e
A B : LightCondMod R
e : A ⟶ B
he : Epi e
S : LightProfinite
g : (free R).obj (S.toCondensed ⊗ P.toCondensed) ⟶ B
⊢ ∃ S' π,
    ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
      ∃ g', (free R).map (lightProfiniteToLightCondSet.map π ▷ P.toCondensed) ≫ g = g' ≫ e

Tactic:
specialize h e S ((free R).map (μIso lightProfiniteToLightCondSet _ _).inv ≫ g)

Goal state after:
case refine_2
R : Type u
inst✝ : CommRing R
P : LightProfinite
A B : LightCondMod R
e : A ⟶ B
he : Epi e
S : LightProfinite
g : (free R).obj (S.toCondensed ⊗ P.toCondensed) ⟶ B
h :
  ∃ S' π,
    ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
      ∃ g',
        (free R).map (lightProfiniteToLightCondSet.map (π ▷ P)) ≫
            (free R).map (μIso lightProfiniteToLightCondSet S P).inv ≫ g =
          g' ≫ e
⊢ ∃ S' π,
    ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
      ∃ g', (free R).map (lightProfiniteToLightCondSet.map π ▷ P.toCondensed) ≫ g = g' ≫ e
Module: Mathlib.Control.Traversable.Instances

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

Tactic:
simp! [*, functor_norm, Option.traverse]

Goal state after:
Module: Mathlib.Control.Traversable.Instances

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

Tactic:
simp! [*, functor_norm, Option.traverse]

Goal state after:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: case succ
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
i j : ℕ
ih : i ≤ j → approx (⇑f) i ≤ approx (⇑f) j
hij : i ≤ j + 1
⊢ approx (⇑f) i ≤ approx (⇑f) (j + 1)

Tactic:
| succ j ih =>

Goal state after:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: case pos.mpr
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (⇑f) i a).Dom
y : β a
h₁ : y ∈ approx (⇑f) (Nat.find h₀).succ a
i : ℕ
hh : b ∈ approx (⇑f) i a
⊢ y = b

Tactic:
revert h₁

Goal state after:
case pos.mpr
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (⇑f) i a).Dom
y : β a
i : ℕ
hh : b ∈ approx (⇑f) i a
⊢ y ∈ approx (⇑f) (Nat.find h₀).succ a → y = b
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: case refine_1
S : Type u_1
T : Type u_2
X : Type u_3
π : T → S × Option X
σ : Option X → S → T
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
x : T
x✝ : ¬(π x).2 = none ∧ ∀ (x_1 : X) (x_2 : S), ¬σ (Option.some x_1) x_2 = x
h₁ : ¬(π x).2 = none
h₂ : ∀ (x_1 : X) (x_2 : S), ¬σ (Option.some x_1) x_2 = x
n : X
hn : (π x).2 = Option.some n
⊢ ∃ i, (∀ (x_1 : S), ¬σ (Option.some i) x_1 = x) ∧ (π x).2 = ↑i

Tactic:
exact ⟨n, h₂ n, hn⟩

Goal state after:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : (a : α) → Part (β a)
⊢ x ∈ approxChain f → x ≤ f x

Tactic:
simp only [Membership.mem, forall_exists_index]
  rintro i rfl
  apply approx_mono'

Goal state after:
Module: Mathlib.Control.Traversable.Equiv

Goal state before:
pp: t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝² : Traversable t
inst✝¹ : LawfulTraversable t
inst✝ : Traversable t'
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
h₂ :
  ∀ {F : Type u → Type u} [inst : Applicative F] [LawfulApplicative F] {α β : Type u} (f : α → F β),
    traverse f = Equiv.traverse eqv f
α✝ : Type u
x✝ : t' α✝
⊢ traverse pure x✝ = pure x✝

Tactic:
by rw [h₂, Equiv.id_traverse]

Goal state after:
Module: Mathlib.Data.Analysis.Filter

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f g : Filter α
F : f.Realizer
G : g.Realizer
x✝ : Set α
⊢ x✝ ∈
      {
            f := fun x ↦
              match x with
              | (s, t) => F.F.f s ∪ G.F.f t,
            pt := (F.F.pt, G.F.pt),
            inf := fun x x_1 ↦
              match x with
              | (a, a') =>
                match x_1 with
                | (b, b') => (F.F.inf a b, G.F.inf a' b'),
            inf_le_left := ⋯, inf_le_right := ⋯ }.toFilter.sets ↔
    x✝ ∈ (f ⊔ g).sets

Tactic:
by cases F; cases G; subst f g; simp [CFilter.toFilter]

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

Goal state before:
pp: n : ℕ
α : Fin n → Sort u_1
v : (i : Fin n) → α i
⊢ take 0 ⋯ v = fun i ↦ i.elim0

Tactic:
by
  ext i; exact elim0 i

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

Goal state before:
pp: case pos
n : ℕ
α : Fin n → Sort u_1
m : ℕ
h : m ≤ n
v : (i : Fin n) → α i
i : Fin m
x : α (castLE h i)
j : Fin m
h' : j = i
⊢ take m h (update v (castLE h i) x) i = update (take m h v) i x i

Tactic:
simp only [take, update_self]

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s : AList β
⊢ (insert a b s).keys = a :: s.keys.erase a

Tactic:
by
  simp [insert, keys, keys_kerase]

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

Goal state before:
pp: case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
h : a = a'
⊢ lookupAll a (⟨a', b⟩ :: l) = [] ↔ ∀ (b_1 : β a), ¬⟨a, b_1⟩ ∈ ⟨a', b⟩ :: l

pp: case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
h : ¬a = a'
⊢ lookupAll a (⟨a', b⟩ :: l) = [] ↔ ∀ (b_1 : β a), ¬⟨a, b_1⟩ ∈ ⟨a', b⟩ :: l

Tactic:
· subst a'
      simp only [lookupAll_cons_eq, mem_cons, Sigma.mk.inj_iff, heq_eq_eq, true_and, not_or,
        false_iff, not_forall, not_and, not_not, reduceCtorEq]
      use b
      simp

Goal state after:
case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
h : ¬a = a'
⊢ lookupAll a (⟨a', b⟩ :: l) = [] ↔ ∀ (b_1 : β a), ¬⟨a, b_1⟩ ∈ ⟨a', b⟩ :: l
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys
⊢ (lookupAll a l).length ≤ 1 → lookupAll a l = (lookupAll a l).head?.toList

Tactic:
rcases lookupAll a l with (_ | ⟨b, _ | ⟨c, l⟩⟩)

Goal state after:
case nil
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys
⊢ [].length ≤ 1 → [] = [].head?.toList

case cons.nil
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys
b : β a
⊢ [b].length ≤ 1 → [b] = [b].head?.toList

case cons.cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l✝ : List (Sigma β)
h : l✝.NodupKeys
b c : β a
l : List (β a)
⊢ (b :: c :: l).length ≤ 1 → b :: c :: l = (b :: c :: l).head?.toList
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys
⊢ (lookupAll a l).length ≤ 1 → lookupAll a l = (lookupAll a l).head?.toList

Tactic:
rcases lookupAll a l with (_ | ⟨b, _ | ⟨c, l⟩⟩) <;> intro h1 <;> try rfl

Goal state after:
case cons.cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l✝ : List (Sigma β)
h : l✝.NodupKeys
b c : β a
l : List (β a)
h1 : (b :: c :: l).length ≤ 1
⊢ b :: c :: l = (b :: c :: l).head?.toList
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s : AList β
⊢ insert a b ⟦s⟧ = ⟦AList.insert a b s⟧

Tactic:
simp [insert]

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : ¬a ∈ l.keys
⊢ kerase a l = l

Tactic:
by
  induction l with
  | nil => rfl
  | cons _ _ ih => simp [not_or] at h; simp [h.1, ih h.2]

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

Goal state before:
pp: case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
tail✝ : List (Sigma β)
l_ih : dlookup a tail✝.dedupKeys = dlookup a tail✝
a' : α
b : β a'
h : a = a'
⊢ dlookup a (⟨a', b⟩ :: tail✝).dedupKeys = dlookup a (⟨a', b⟩ :: tail✝)

Tactic:
subst a'
      rw [dedupKeys_cons, dlookup_kinsert, dlookup_cons_eq]

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

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x ↦ M
a : α
⊢ l.lookupFinsupp a = 0 ↔ a ∉ l ∨ 0 ∈ lookup a l

Tactic:
rw [lookupFinsupp_apply, ← lookup_eq_none]
  rcases lookup a l with - | m <;> simp

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

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
⊢ f.toAList.lookupFinsupp = f

Tactic:
ext a
  classical
    by_cases h : f a = 0
    · suffices f.toAList.lookup a = none by simp [h, this]
      simp [lookup_eq_none, h]
    · suffices f.toAList.lookup a = some (f a) by simp [this]
      apply mem_lookup_iff.2
      simpa using h

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

Goal state before:
pp: case e'_2
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Finset (ι →₀ M)
hs : (↑s).PairwiseDisjoint Finsupp.support
this : Multiset.Pairwise (Disjoint on Finsupp.support) s.val
⊢ s.sum id = s.val.sum

Tactic:
exact (Finset.sum_val _).symm

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

Goal state before:
pp: α : Type u_1
N : Type u_3
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : AddGroup N
f₁ f₂ g : α →₀ N
⊢ (f₁ - g).neLocus (f₂ - g) = f₁.neLocus f₂

Tactic:
simpa only [sub_eq_add_neg] using neLocus_add_right _ _ _

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

Goal state before:
pp: κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst✝¹ : Zero M
inst✝ : DecidableEq κ
k : κ
f : ι k →₀ M
i : (k : κ) × ι k
⊢ f.embSigma i = if h : i.fst = k then f (h ▸ i.snd) else 0

Tactic:
rcases i with ⟨k, i⟩
  split_ifs with h
  · subst h
    simp only [embSigma, Embedding.sigmaMk]
    apply embDomain_apply_self
  · simp only [embSigma, Embedding.sigmaMk]
    rw [embDomain_of_notMem_range]
    simp_all

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|
⊢ (r + b * q) / b = q

Tactic:
Int.add_mul_ediv_left r q h,

Goal state after:
case mpr.left
a b r q : ℤ
h : b ≠ 0
hz : 0 ≤ r
hb : r < |b|
⊢ r / b + q = q
Module: Mathlib.Data.LawfulXor.Basic

Goal state before:
pp: α : Type u_1
inst✝² : XorOp α
inst✝¹ : Zero α
inst✝ : LawfulXor α
a : α
⊢ 0 ^^^ a = a

Tactic:
rw [LawfulXor.xor_comm, xor_zero]

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

Goal state before:
pp: b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
| ⌈(↑b - ↑v) / ↑r⌉ - ⌈(↑0 - ↑v) / ↑r⌉

Tactic:
rw [← div_add_mod v r, cast_add, cast_mul, add_comm]

Goal state after:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
| ⌈(↑b - (↑(v % r) + ↑r * ↑(v / r))) / ↑r⌉ - ⌈(↑0 - (↑(v % r) + ↑r * ↑(v / r))) / ↑r⌉
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
⊢ ⌈(↑b - ↑(v % r) - ↑r * ↑(v / r)) / ↑r⌉ - ⌈(↑0 - ↑(v % r) - ↑r * ↑(v / r)) / ↑r⌉ = ?m.91

Tactic:
sub_div (_ - _),

Goal state after:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
⊢ ⌈(↑b - ↑(v % r)) / ↑r - ↑r * ↑(v / r) / ↑r⌉ - ⌈(↑0 - ↑(v % r)) / ↑r - ↑r * ↑(v / r) / ↑r⌉ = ?m.91
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: case append_singleton.succ
α : Type u_1
xs : List α
x : α
IH : ∀ (n : ℕ), take (xs.length - n) xs = (drop n xs.reverse).reverse
n✝ : ℕ
⊢ take ((xs ++ [x]).length - (n✝ + 1)) (xs ++ [x]) = (drop (n✝ + 1) (xs ++ [x]).reverse).reverse

Tactic:
· simp [take_append, IH]

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

Goal state before:
pp: n m k : ℕ
⊢ map (fun x ↦ k + x) (range' n (m - n)) = range' (n + k) (m + k - (n + k))

Tactic:
map_add_range',

Goal state after:
n m k : ℕ
⊢ range' (k + n) (m - n) = range' (n + k) (m + k - (n + k))
Module: Mathlib.Data.List.ModifyLast

Goal state before:
pp: α : Type u_1
f : α → α
l₁ : List α
hd hd' : α
tl' : List α
x✝ : hd :: hd' :: tl' ≠ []
⊢ hd' :: tl' ≠ []

pp: α : Type u_1
f : α → α
l₁ : List α
hd hd' : α
tl' : List α
x✝ : hd :: hd' :: tl' ≠ []
⊢ hd' :: tl' ≠ []

Tactic:
all_goals { exact cons_ne_nil _ _ }

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

Goal state before:
pp: α : Type u_1
l : List α
p : l.Palindrome
⊢ l.reverse = l

Tactic:
induction p <;> try (exact rfl)

Goal state after:
case cons_concat
α : Type u_1
l : List α
x✝ : α
l✝ : List α
a✝ : l✝.Palindrome
a_ih✝ : l✝.reverse = l✝
⊢ (x✝ :: (l✝ ++ [x✝])).reverse = x✝ :: (l✝ ++ [x✝])
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 β
H : foldr f a l ∈ Set.range (foldr g a)
⊢ foldr f a (b :: l) ∈ Set.range (foldr g a)

Tactic:
obtain ⟨c, hgf⟩ := hfg (Set.mem_range_self b)
    obtain ⟨m, hgf'⟩ := H
    rw [foldr_cons, ← hgf, ← hgf']
    exact ⟨c :: m, rfl⟩

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

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Bool
a : List α
l : List (List α)
IH :
  ¬[] ∈ l →
    (∀ (m : List α), m ∈ l → IsChain (fun x y ↦ r x y = true) m) →
      IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) l → splitBy r l.flatten = l
hn : ¬a = [] ∧ ¬[] ∈ l
hc : ∀ (m : List α), m ∈ a :: l → IsChain (fun x y ↦ r x y = true) m
hc' : IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) (a :: l)
y : α
hy : y ∈ l.flatten.head?
⊢ r (a.getLast ⋯) (l.flatten.head ⋯) = false

Tactic:
isChain_cons

Goal state after:
case cons
α : Type u_1
r : α → α → Bool
a : List α
l : List (List α)
IH :
  ¬[] ∈ l →
    (∀ (m : List α), m ∈ l → IsChain (fun x y ↦ r x y = true) m) →
      IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) l → splitBy r l.flatten = l
hn : ¬a = [] ∧ ¬[] ∈ l
hc : ∀ (m : List α), m ∈ a :: l → IsChain (fun x y ↦ r x y = true) m
hc' :
  (∀ (y : List α), y ∈ l.head? → ∃ ha hb, r (a.getLast ha) (y.head hb) = false) ∧
    IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) l
y : α
hy : y ∈ l.flatten.head?
⊢ r (a.getLast ⋯) (l.flatten.head ⋯) = false
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
⊢ w.HasPeriod (p.gcd q)

Tactic:
by
  rcases Nat.eq_zero_or_pos p with rfl | p_pos
  · simp_all [HasPeriod]
  rcases Nat.eq_zero_or_pos q with rfl | q_pos
  · simp_all
  cases hyp : compare p q with
  | lt => -- if `p` is less than `q`, switch the two periods
      have p_lt_q := Nat.compare_eq_lt.mp hyp
      exact (gcd_comm q p ▸ per_q.gcd) per_p (add_comm p q ▸ len)
  | eq => simpa [(Nat.compare_eq_eq).mp hyp]
  | gt =>
      have q_lt_p : q < p := Nat.compare_eq_gt.mp hyp
      have gcd_lt_p : p.gcd q < p := by
        have : p.gcd q ≠ p := by
          simp [gcd_eq_left_iff_dvd, not_dvd_of_pos_of_lt q_pos q_lt_p]
        exact this.lt_of_le (gcd_le_left q p_pos)
      have per_diff : HasPeriod (drop q w) (p - q) := by
        have : p = (p - q) + q := by lia
        exact per_q.drop_of_hasPeriod_add (this ▸ per_p)
      have per_q' : HasPeriod (drop q w) q := by
        apply @HasPeriod.factor _ (take q w) (drop q w) [] q
        all_goals simp_all
      have gcd_stable : (p - q).gcd q = p.gcd q := gcd_sub_self_left (le_of_lt q_lt_p)
      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
      have take_eq : take q (drop q w) = take q w := by
          let ⟨z, hz⟩ := per_q.drop_prefix
          convert_to take q (drop q w) = take q (drop q w ++ z)
          · rw [hz]
          exact (take_append_of_le_length drop_len).symm
      -- the induction step
      have IH : HasPeriod (drop q w) ((p - q).gcd q) :=
        per_diff.gcd per_q' (by simp; lia)
      convert_to HasPeriod (take q (drop q w) ++ drop q w) (p.gcd q)
      · rw [take_eq, take_append_drop q w]
      · exact (gcd_stable ▸ IH).take_append (p.gcd q) q (drop q w)
          (gcd_dvd_right p q) drop_len

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

Goal state before:
pp: R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
r : R
n d : ℕ
h : IsNNRat r n d
res : ℕ
hres : ⌈↑n / ↑d⌉₊ = res
⊢ ⌈r⌉₊ = ↑res

Tactic:
rw [← hres, h.to_eq rfl rfl, ← @NNRat.ceil_cast R]

Goal state after:
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
r : R
n d : ℕ
h : IsNNRat r n d
res : ℕ
hres : ⌈↑n / ↑d⌉₊ = res
⊢ ⌈↑n / ↑d⌉₊ = ↑⌈↑(↑n / ↑d)⌉₊
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: case inl.inr
p : ℕ → Prop
k : ℕ
hf : (Set.ofPred p).Finite
n : ℕ
hn : n < #hf.toFinset
h : nth p n < nth p (k + 1)
ha : p (nth p n)
hk : #hf.toFinset ≤ k + 1
⊢ nth p n ≤ nth p k

Tactic:
· rw [nth_of_card_le _ hk] at h
      exact absurd h (zero_le _).not_gt

Goal state after:
Module: Mathlib.Data.Num.Prime

Goal state before:
pp: case bit1
n : PosNum
⊢ ↑n.bit1.minFac = (↑n.bit1).minFac

Tactic:
minFac,

Goal state after:
case bit1
n : PosNum
⊢ ↑(n.bit1.minFacAux (↑n) 1) = (↑n.bit1).minFac
Module: Mathlib.Data.Num.Prime

Goal state before:
pp: case bit0
a✝ : PosNum
⊢ ↑a✝.bit0.minFac = (↑a✝.bit0).minFac

Tactic:
minFac,

Goal state after:
case bit0
a✝ : PosNum
⊢ ↑2 = (↑a✝.bit0).minFac
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
n : ℕ
hp : ∀ n' ≥ n, ¬p n'
⊢ Set.ofPred p ⊆ ↑(range n)

Tactic:
intro n'

Goal state after:
p : ℕ → Prop
n : ℕ
hp : ∀ n' ≥ n, ¬p n'
n' : ℕ
⊢ n' ∈ Set.ofPred p → n' ∈ ↑(range n)
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: p : PosNum
this : (↑p).bit1 = (ZNum.pos p).bit1
⊢ ↑p.bit1 = ZNum.pos p.bit1

Tactic:
← ZNum.bit1_of_bit1

Goal state after:
p : PosNum
this : ↑p + ↑p + 1 = (ZNum.pos p).bit1
⊢ ↑p.bit1 = ZNum.pos p.bit1
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ ↑(a.sub' b).bit0 = ↑a.bit0 - ↑b.bit0

Tactic:
ZNum.cast_bit0,

Goal state after:
α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ ↑(a.sub' b) + ↑(a.sub' b) = ↑a.bit0 - ↑b.bit0
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ ↑(a.sub' b).bit0 = ↑a.bit1 - ↑b.bit1

Tactic:
ZNum.cast_bit0,

Goal state after:
α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ ↑(a.sub' b) + ↑(a.sub' b) = ↑a.bit1 - ↑b.bit1
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: p : PosNum
⊢ ↑(↑p.pred' + 1) = ↑p

Tactic:
← succ'_to_nat

Goal state after:
p : PosNum
⊢ ↑↑p.pred'.succ' = ↑p
Module: Mathlib.Data.PFunctor.Multivariate.M

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type v
g₀ : β → P.A
g₁ : (b : β) → P.drop.B (g₀ b) ⟹ α
g₂ : (b : β) → P.last.B (g₀ b) → β
x✝ : P.last.M
b : β
x : P.last.M
i : Fin2 n
a : P.A
f : P.last.B a → P.last.M
h' : x.dest = ⟨a, f⟩
c : P.drop.B a i
h : x = corecShape P g₀ g₂ b
⊢ a = g₀ b

Tactic:
rw [h, M.corecShape, PFunctor.M.dest_corec] at h'

Goal state after:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type v
g₀ : β → P.A
g₁ : (b : β) → P.drop.B (g₀ b) ⟹ α
g₂ : (b : β) → P.last.B (g₀ b) → β
x✝ : P.last.M
b : β
x : P.last.M
i : Fin2 n
a : P.A
f : P.last.B a → P.last.M
h' : P.last.map (PFunctor.M.corec fun b ↦ ⟨g₀ b, g₂ b⟩) ⟨g₀ b, g₂ b⟩ = ⟨a, f⟩
c : P.drop.B a i
h : x = corecShape P g₀ g₂ b
⊢ a = g₀ b
Module: Mathlib.Data.PFunctor.Multivariate.M

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type v
g₀ : β → P.A
g₁ : (b : β) → P.drop.B (g₀ b) ⟹ α
g₂ : (b : β) → P.last.B (g₀ b) → β
x✝ : P.last.M
b : β
x : P.last.M
i : Fin2 n
a : P.A
f : P.last.B a → P.last.M
h' : x.dest = ⟨a, f⟩
j : P.last.B a
c : Path P (f j) i
h : x = corecShape P g₀ g₂ b
⊢ a = g₀ b

Tactic:
rw [h, M.corecShape, PFunctor.M.dest_corec] at h'

Goal state after:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type v
g₀ : β → P.A
g₁ : (b : β) → P.drop.B (g₀ b) ⟹ α
g₂ : (b : β) → P.last.B (g₀ b) → β
x✝ : P.last.M
b : β
x : P.last.M
i : Fin2 n
a : P.A
f : P.last.B a → P.last.M
h' : P.last.map (PFunctor.M.corec fun b ↦ ⟨g₀ b, g₂ b⟩) ⟨g₀ b, g₂ b⟩ = ⟨a, f⟩
j : P.last.B a
c : Path P (f j) i
h : x = corecShape P g₀ g₂ b
⊢ a = g₀ b
Module: Mathlib.Data.PFunctor.Multivariate.M

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type v
g₀ : β → P.A
g₁ : (b : β) → P.drop.B (g₀ b) ⟹ α
g₂ : (b : β) → P.last.B (g₀ b) → β
x✝ : P.last.M
b : β
x : P.last.M
i : Fin2 n
a : P.A
f : P.last.B a → P.last.M
h' : x.dest = ⟨a, f⟩
j : P.last.B a
c : Path P (f j) i
h : x = corecShape P g₀ g₂ b
h₀ : a = g₀ b
⊢ f j = corecShape P g₀ g₂ (g₂ b (P.castLastB h₀ j))

Tactic:
rw [h, M.corecShape, PFunctor.M.dest_corec] at h'

Goal state after:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type v
g₀ : β → P.A
g₁ : (b : β) → P.drop.B (g₀ b) ⟹ α
g₂ : (b : β) → P.last.B (g₀ b) → β
x✝ : P.last.M
b : β
x : P.last.M
i : Fin2 n
a : P.A
f : P.last.B a → P.last.M
h' : P.last.map (PFunctor.M.corec fun b ↦ ⟨g₀ b, g₂ b⟩) ⟨g₀ b, g₂ b⟩ = ⟨a, f⟩
j : P.last.B a
c : Path P (f j) i
h : x = corecShape P g₀ g₂ b
h₀ : a = g₀ b
⊢ f j = corecShape P g₀ g₂ (g₂ b (P.castLastB h₀ j))
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case nil
α : Type u_1
l : Ordnode α
x y : α
r : Ordnode α
hm : nil.Sized
⊢ (l.node4L x nil y r).size = l.size + nil.size + r.size + 2

Tactic:
simp [node4L, node3L, node']
    abel

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

Goal state before:
pp: v : Multiset ℕ+
h✝ : ∀ (p : ℕ+), p ∈ v → p.Prime
p : ℕ+
h : p.Prime
⊢ ↑⟨↑p, h⟩ = id p

Tactic:
apply Subtype.ext

Goal state after:
v : Multiset ℕ+
h✝ : ∀ (p : ℕ+), p ∈ v → p.Prime
p : ℕ+
h : p.Prime
⊢ ↑↑⟨↑p, h⟩ = ↑(id p)