mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case pos.bit1
q : Λ'
n : ℕ
c d : List Γ'
m : PosNum
IH :
  ∀ {s : Option Γ'} (l₁ : List Γ'),
    ∃ l₁' l₂' s',
      l₁.reverseAux (trPosNum m.succ) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step tr) { l := some q.succ, var := s, stk := elim (trPosNum m ++ [Γ'.cons]) l₁ c d }
          { l := some (unrev q), var := s', stk := elim (l₂' ++ [Γ'.cons]) l₁' c d }
s : Option Γ'
l₁ l₁' l₂' : List Γ'
s' : Option Γ'
e : (Γ'.bit0 :: l₁).reverseAux (trPosNum m.succ) = l₁'.reverseAux l₂'
h :
  Reaches₁ (TM2.step tr) { l := some q.succ, var := ?m.498, stk := elim (trPosNum m ++ [Γ'.cons]) (Γ'.bit0 :: l₁) c d }
    { l := some (unrev q), var := s', stk := elim (l₂' ++ [Γ'.cons]) l₁' c d }
⊢ ∃ l₁' l₂' s',
    l₁.reverseAux (trPosNum m.bit1.succ) = l₁'.reverseAux l₂' ∧
      Reaches₁ (TM2.step tr) { l := some q.succ, var := s, stk := elim (trPosNum m.bit1 ++ [Γ'.cons]) l₁ c d }
        { l := some (unrev q), var := s', stk := elim (l₂' ++ [Γ'.cons]) l₁' c d }

Tactic:
refine ⟨l₁', l₂', s', e, TransGen.head ?_ h⟩

Goal state after:
case pos.bit1
q : Λ'
n : ℕ
c d : List Γ'
m : PosNum
IH :
  ∀ {s : Option Γ'} (l₁ : List Γ'),
    ∃ l₁' l₂' s',
      l₁.reverseAux (trPosNum m.succ) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step tr) { l := some q.succ, var := s, stk := elim (trPosNum m ++ [Γ'.cons]) l₁ c d }
          { l := some (unrev q), var := s', stk := elim (l₂' ++ [Γ'.cons]) l₁' c d }
s : Option Γ'
l₁ l₁' l₂' : List Γ'
s' : Option Γ'
e : (Γ'.bit0 :: l₁).reverseAux (trPosNum m.succ) = l₁'.reverseAux l₂'
h :
  Reaches₁ (TM2.step tr) { l := some q.succ, var := ?m.498, stk := elim (trPosNum m ++ [Γ'.cons]) (Γ'.bit0 :: l₁) c d }
    { l := some (unrev q), var := s', stk := elim (l₂' ++ [Γ'.cons]) l₁' c d }
⊢ { l := some q.succ, var := ?m.498, stk := elim (trPosNum m ++ [Γ'.cons]) (Γ'.bit0 :: l₁) c d } ∈
    TM2.step tr { l := some q.succ, var := s, stk := elim (trPosNum m.bit1 ++ [Γ'.cons]) l₁ c d }
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case cons.succ.pos.bit1
q₁ q₂ : Λ'
c d : List Γ'
v : List ℕ
n : ℕ
m : PosNum
IH :
  ∀ (s : Option Γ') (l₁ : List Γ'),
    ∃ l₁' l₂' s',
      l₁.reverseAux (trPosNum m) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step tr)
          { l := some (q₁.pred q₂), var := s, stk := elim (trPosNum m.succ ++ Γ'.cons :: trList v) l₁ c d }
          { l := some (unrev q₂), var := s', stk := elim (l₂' ++ Γ'.cons :: trList v) l₁' c d }
s : Option Γ'
l₁ l₁' l₂' : List Γ'
s' : Option Γ'
e : (Γ'.bit1 :: l₁).reverseAux (trPosNum m) = l₁'.reverseAux l₂'
h :
  Reaches₁ (TM2.step tr)
    { l := some (q₁.pred q₂), var := some Γ'.bit0,
      stk := elim (trPosNum m.succ ++ Γ'.cons :: trList v) (Γ'.bit1 :: l₁) c d }
    { l := some (unrev q₂), var := s', stk := elim (l₂' ++ Γ'.cons :: trList v) l₁' c d }
⊢ ∃ l₁' l₂' s',
    l₁.reverseAux (trPosNum m.bit1) = l₁'.reverseAux l₂' ∧
      Reaches₁ (TM2.step tr)
        { l := some (q₁.pred q₂), var := s, stk := elim (trPosNum m.bit1.succ ++ Γ'.cons :: trList v) l₁ c d }
        { l := some (unrev q₂), var := s', stk := elim (l₂' ++ Γ'.cons :: trList v) l₁' c d }

Tactic:
refine ⟨l₁', l₂', s', e, TransGen.head ?_ h⟩

Goal state after:
case cons.succ.pos.bit1
q₁ q₂ : Λ'
c d : List Γ'
v : List ℕ
n : ℕ
m : PosNum
IH :
  ∀ (s : Option Γ') (l₁ : List Γ'),
    ∃ l₁' l₂' s',
      l₁.reverseAux (trPosNum m) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step tr)
          { l := some (q₁.pred q₂), var := s, stk := elim (trPosNum m.succ ++ Γ'.cons :: trList v) l₁ c d }
          { l := some (unrev q₂), var := s', stk := elim (l₂' ++ Γ'.cons :: trList v) l₁' c d }
s : Option Γ'
l₁ l₁' l₂' : List Γ'
s' : Option Γ'
e : (Γ'.bit1 :: l₁).reverseAux (trPosNum m) = l₁'.reverseAux l₂'
h :
  Reaches₁ (TM2.step tr)
    { l := some (q₁.pred q₂), var := some Γ'.bit0,
      stk := elim (trPosNum m.succ ++ Γ'.cons :: trList v) (Γ'.bit1 :: l₁) c d }
    { l := some (unrev q₂), var := s', stk := elim (l₂' ++ Γ'.cons :: trList v) l₁' c d }
⊢ { l := some (q₁.pred q₂), var := some Γ'.bit0,
      stk := elim (trPosNum m.succ ++ Γ'.cons :: trList v) (Γ'.bit1 :: l₁) c d } ∈
    TM2.step tr { l := some (q₁.pred q₂), var := s, stk := elim (trPosNum m.bit1.succ ++ Γ'.cons :: trList v) l₁ c d }
Module: Mathlib.Condensed.Discrete.Characterization

Goal state before:
pp: X : LightCondSet
h : (S : LightProfinite) → IsColimit (X.obj.mapCocone (coconeRightOpOfCone S.asLimitCone))
⊢ LocallyConstant.functor.essImage X

Tactic:
by
  let i : X.obj ≅ (LightCondSet.LocallyConstant.functor.obj _).obj :=
    LightCondensed.isoLocallyConstantOfIsColimit _ h
  exact ⟨_, ⟨((sheafToPresheaf _ _).preimageIso i.symm)⟩⟩

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
X Y : LightCondMod R
f : X ⟶ Y
inst✝ : Epi f
S : LightProfinite
p : (LightCondensed.free R).obj S.toCondensed ⟶ Y
this : Epi ((LightCondensed.forget R).map f)
⊢ ∃ T π g, Epi π ∧ (lightProfiniteToLightCondSet ⋙ LightCondensed.free R).map π ≫ p = g ≫ f

Tactic:
rw [LightCondSet.epi_iff_locallySurjective_on_lightProfinite] at this

Goal state after:
R : Type u
inst✝¹ : Ring R
X Y : LightCondMod R
f : X ⟶ Y
inst✝ : Epi f
S : LightProfinite
p : (LightCondensed.free R).obj S.toCondensed ⟶ Y
this :
  ∀ (S : LightProfinite) (y : ((LightCondensed.forget R).obj Y).obj.obj (Opposite.op S)),
    ∃ S' φ,
      ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom φ)),
        ∃ x,
          (ConcreteCategory.hom (((LightCondensed.forget R).map f).hom.app (Opposite.op S'))) x =
            (ConcreteCategory.hom (((LightCondensed.forget R).obj Y).obj.map (Opposite.op φ))) y
⊢ ∃ T π g, Epi π ∧ (lightProfiniteToLightCondSet ⋙ LightCondensed.free R).map π ≫ p = g ≫ f
Module: Mathlib.Control.Fold

Goal state before:
pp: α β γ : Type u
inst✝¹ : Monoid α
inst✝ : Monoid β
f : α →* β
⊢ ∀ {α_1 : Type ?u.17} (x : α_1), f (pure x) = pure x

Tactic:
by intros; simp only [map_one, pure]

Goal state after:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: case zero.refl
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
⊢ approx (⇑f) 0 ≤ approx (⇑f) 0

Tactic:
exact le_rfl

Goal state after:
Module: Mathlib.Control.LawfulFix

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

Tactic:
exact le_rfl

Goal state after:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: case succ.step
α : 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
a✝ : i.le j
⊢ approx (⇑f) i ≤ approx (⇑f) (j + 1)

Tactic:
exact le_trans (ih ‹_›) (approx_mono' f)

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 : α
i : ℕ
hx : Part.fix (⇑f) x ≤ approx (⇑f) i x
⊢ approx (⇑f) i x ≤ approx (⇑f) i.succ x

Tactic:
· apply approx_mono' f

Goal state after:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: case a
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
⊢ Part.fix ⇑f ≤ ωSup (approxChain f)

pp: case a
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
⊢ ωSup (approxChain f) ≤ Part.fix ⇑f

Tactic:
· intro x
    obtain ⟨i, hx⟩ := exists_fix_le_approx f x
    trans approx f i.succ x
    · trans
      · apply hx
      · apply approx_mono' f
    apply le_ωSup_of_le i.succ
    dsimp [approx]
    rfl

Goal state after:
case a
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
⊢ ωSup (approxChain f) ≤ Part.fix ⇑f
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: S : Type u_1
T : Type u_2
X : Type u_3
inst✝⁵ : TopologicalSpace S
inst✝⁴ : T2Space S
inst✝³ : TopologicalSpace T
inst✝² : CompactSpace T
inst✝¹ : TopologicalSpace X
inst✝ : T1Space (OnePoint X)
π : T → S × OnePoint X
hπ : Continuous π
this : ∀ (x : OnePoint X), CompactSpace ↑(Prod.snd ∘ π ⁻¹' {x})
⊢ IsCompact (⋂ n, ⋂ m, {x | (π ↑(x n)).1 = (π ↑(x m)).1})

Tactic:
refine (isClosed_iInter fun n ↦ isClosed_iInter fun m ↦ isClosed_eq ?_ ?_).isCompact

Goal state after:
case refine_1
S : Type u_1
T : Type u_2
X : Type u_3
inst✝⁵ : TopologicalSpace S
inst✝⁴ : T2Space S
inst✝³ : TopologicalSpace T
inst✝² : CompactSpace T
inst✝¹ : TopologicalSpace X
inst✝ : T1Space (OnePoint X)
π : T → S × OnePoint X
hπ : Continuous π
this : ∀ (x : OnePoint X), CompactSpace ↑(Prod.snd ∘ π ⁻¹' {x})
n m : OnePoint X
⊢ Continuous fun x ↦ (π ↑(x n)).1

case refine_2
S : Type u_1
T : Type u_2
X : Type u_3
inst✝⁵ : TopologicalSpace S
inst✝⁴ : T2Space S
inst✝³ : TopologicalSpace T
inst✝² : CompactSpace T
inst✝¹ : TopologicalSpace X
inst✝ : T1Space (OnePoint X)
π : T → S × OnePoint X
hπ : Continuous π
this : ∀ (x : OnePoint X), CompactSpace ↑(Prod.snd ∘ π ⁻¹' {x})
n m : OnePoint X
⊢ Continuous fun x ↦ (π ↑(x m)).1
Module: Mathlib.Data.Analysis.Topology

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
F : Ctop α σ
E : σ ≃ τ
f : σ → Set α
T : α → σ
h₁ : ∀ (x : α), x ∈ f (T x)
I : (a b : σ) → (x : α) → x ∈ f a ∩ f b → σ
h₂ : ∀ (a b : σ) (x : α) (h : x ∈ f a ∩ f b), x ∈ f (I a b x h)
h₃ : ∀ (a b : σ) (x : α) (h : x ∈ f a ∩ f b), f (I a b x h) ⊆ f a ∩ f b
a b : τ
x : α
h : x ∈ f (E.symm a) ∩ f (E.symm b)
⊢ f (E.symm (E (I (E.symm a) (E.symm b) x h))) ⊆ f (E.symm a) ∩ f (E.symm b)

Tactic:
simpa using h₃ (E.symm a) (E.symm b) x h

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: case cons
α : Type u
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (s : Finset α), s ∈ enum xs ↔ ∀ x ∈ s, x ∈ xs
s : Finset α
⊢ s ∈ enum (x :: xs) ↔ ∀ x_1 ∈ s, x_1 ∈ x :: xs

Tactic:
simp only [enum, List.bind_eq_flatMap, List.mem_flatMap, List.mem_cons,
        List.not_mem_nil, or_false, ih]
      refine ⟨by aesop, fun hs => ⟨s.erase x, ?_⟩⟩
      simp only [or_iff_not_imp_left] at hs
      simp +contextual [eq_comm (a := s), or_iff_not_imp_left, hs]

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
γ : Type u_1
s : AList β
f : AList β → γ
H : ∀ (a b : AList β), a.entries ~ b.entries → f a = f b
⊢ ⟦s⟧.liftOn f H = f s

Tactic:
cases s

Goal state after:
case mk
α : Type u
β : α → Type v
γ : Type u_1
f : AList β → γ
H : ∀ (a b : AList β), a.entries ~ b.entries → f a = f b
entries✝ : List (Sigma β)
nodupKeys✝ : entries✝.NodupKeys
⊢ ⟦{ entries := entries✝, nodupKeys := nodupKeys✝ }⟧.liftOn f H = f { entries := entries✝, nodupKeys := nodupKeys✝ }
Module: Mathlib.Data.Finset.Functor

Goal state before:
pp: α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
s : Finset α✝
t : Finset β✝
hs : s.Nonempty
a : β✝
ha : a ∈ t
⊢ a ∈ image id t

Tactic:
image_id

Goal state after:
α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
s : Finset α✝
t : Finset β✝
hs : s.Nonempty
a : β✝
ha : a ∈ t
⊢ a ∈ t
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
h : ¬a = a'
x : Sigma β
xs : List (Sigma β)
tail_ih✝ : kerase a (kerase a' xs) = kerase a' (kerase a xs)
h✝ : a' = x.fst
⊢ kerase a (kerase a' (x :: xs)) = kerase a' (kerase a (x :: xs))

Tactic:
subst a'
      simp [kerase_cons_ne h, kerase_cons_eq rfl]

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⟩

Goal state after:
κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst✝¹ : Zero M
inst✝ : DecidableEq κ
k✝ : κ
f : ι k✝ →₀ M
k : κ
i : ι k
⊢ f.embSigma ⟨k, i⟩ = if h : ⟨k, i⟩.fst = k✝ then f (h ▸ ⟨k, i⟩.snd) else 0
Module: Mathlib.Data.Finsupp.Sigma

Goal state before:
pp: case neg
κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst✝¹ : Zero M
inst✝ : DecidableEq κ
k✝ : κ
f : ι k✝ →₀ M
k : κ
i : ι k
h : ¬⟨k, i⟩.fst = k✝
⊢ f.embSigma ⟨k, i⟩ = 0

Tactic:
· simp only [embSigma, Embedding.sigmaMk]
    rw [embDomain_of_notMem_range]
    simp_all

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

Goal state before:
pp: m : ℕ
b : Bool
n : ℕ
⊢ (!(Nat.bit (!b) n).testBit m.succ) = !n.testBit m

Tactic:
cases b <;> simp only [Bool.not_false, Bool.not_true, Nat.testBit_bit_succ]

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

Goal state before:
pp: case mpr
a b r q : ℤ
h : b ≠ 0
⊢ r + b * q = a ∧ 0 ≤ r ∧ r < |b| → a / b = q ∧ a % b = r

Tactic:
· intro ⟨rfl, hz, hb⟩
    constructor
    · rw [Int.add_mul_ediv_left r q h, ediv_eq_zero_of_lt_abs hz hb]
      simp
    · rw [add_mul_emod_self_left, ← emod_abs, emod_eq_of_lt hz hb]

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

Goal state before:
pp: a b r v : ℕ
x : ℤ
h : (↑a ≤ x ∧ x < ↑b) ∧ x ≡ ↑v [ZMOD ↑r]
⊢ 0 ≤ x

Tactic:
by omega

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

Goal state before:
pp: b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
⊢ ↑(#({x ∈ range b | x ≡ v [MOD r]})) = ⌈(↑b - ↑(v % r)) / ↑r⌉

Tactic:
← Ico_zero_eq_range,

Goal state after:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
⊢ ↑(#({x ∈ Ico 0 b | x ≡ v [MOD r]})) = ⌈(↑b - ↑(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⌉

Tactic:
rw [← div_add_mod b r, cast_add, cast_mul, ← add_sub, _root_.add_div,
    mul_div_cancel_left₀ _ hr'.ne', add_comm, Int.ceil_add_natCast, add_comm]

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

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

Tactic:
induction l with
  | nil =>
    simp only [takeWhile_nil, Bool.not_eq_true, true_iff]
    intro h
    simp at h
  | cons x xs IH => by_cases hp : p x <;> simp [hp]

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

Goal state before:
pp: n m l : ℕ
⊢ filter (fun x ↦ decide (l ≤ x)) (Ico n m) = Ico (max n l) m

Tactic:
by
  rcases le_total n l with hnl | hln
  · rw [max_eq_right hnl, filter_le_of_le hnl]
  · rw [max_eq_left hln, filter_le_of_le_bot hln]

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

Goal state before:
pp: case refine_2
α : Type u_1
L : List (List α)
f : List α
h : Forall₂ (fun x1 x2 ↦ x1 ∈ x2) f L
⊢ f ∈ L.sections

Tactic:
· induction h with
    | nil => simp only [sections, mem_singleton]
    | @cons a l f L al fL fs =>
      simp only [sections, mem_flatMap, mem_map]
      exact ⟨f, fs, a, al, rfl⟩

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
h : WellFounded r
a : List α
x✝ : ℕ
len_a : a.length = x✝
⊢ Acc (Shortlex r) a

Tactic:
induction len_a : a.length using Nat.caseStrongRecOn generalizing a with

Goal state after:
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 : ℕ
less_j : j < n + w.length
j_minus : j - n < w.length
n_le_j : n ≤ j
j_mod : (j - n) % p = j % p
⊢ w[(j - n) % p]? = w[j % p]?

Tactic:
by rw [j_mod]

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
h : mulLeftLinearMap n R a = 0
inhabited_h : Inhabited n
i : l
j : m
⊢ a i j = 0 i j

Tactic:
classical
    replace h := DFunLike.congr_fun h (Matrix.single j (default : n) 1)
    simpa using Matrix.ext_iff.2 h i default

Goal state after:
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
drop_len : q ≤ (drop q w).length
take_eq : take q (drop q w) = take q w
IH : (drop q w).HasPeriod ((p - q).gcd q)
⊢ (take q (drop q w) ++ drop q w).HasPeriod (p.gcd q)

Tactic:
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.List.SplitBy

Goal state before:
pp: case h.a
α : 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 ≠ []
x : List α
hx : x ∈ (splitBy r l).getLast?
y : List α
hy : y ∈ (splitBy r m).head?
⊢ x.getLast ⋯ ∈ l.getLast?

pp: case h.a
α : 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 ≠ []
x : List α
hx : x ∈ (splitBy r l).getLast?
y : List α
hy : y ∈ (splitBy r m).head?
⊢ y.head ⋯ ∈ m.head?

Tactic:
· simp_rw [← getLast_of_mem_getLast? hx, getLast_getLast_splitBy _ hl]
    exact getLast_mem_getLast? _

Goal state after:
case h.a
α : 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 ≠ []
x : List α
hx : x ∈ (splitBy r l).getLast?
y : List α
hy : y ∈ (splitBy r m).head?
⊢ y.head ⋯ ∈ m.head?
Module: Mathlib.Data.Multiset.Interval

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ #(Finset.Ioo s t) = ∏ i ∈ s.toFinset ∪ t.toFinset, (count i t + 1 - count i s) - 2

Tactic:
rw [Finset.card_Ioo_eq_card_Icc_sub_two, card_Icc]

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

Goal state before:
pp: α : Type u_1
s : Finset α
f : α → ℚ
hf : ∀ a ∈ s, 0 ≤ f a
⊢ ↑(∏ a ∈ s, f a).toNNRat = ∏ a ∈ s, ↑(f a).toNNRat

Tactic:
Rat.coe_toNNRat _ (Finset.prod_nonneg hf)

Goal state after:
α : Type u_1
s : Finset α
f : α → ℚ
hf : ∀ a ∈ s, 0 ≤ f a
⊢ ∏ i ∈ s, f i = ∏ a ∈ s, ↑(f a).toNNRat
Module: Mathlib.Data.Nat.ChineseRemainder

Goal state before:
pp: a b : ℕ
l : List ℕ
co : List.Pairwise Coprime l
⊢ a ≡ b [MOD l.prod] ↔ ∀ (i : Fin l.length), a ≡ b [MOD l.get i]

Tactic:
by
  induction l with
  | nil => simp [modEq_one]
  | cons m l ih =>
    have : Coprime m l.prod := coprime_list_prod_right_iff.mpr (List.pairwise_cons.mp co).1
    simp only [List.prod_cons, ← modEq_and_modEq_iff_modEq_mul this, ih (List.Pairwise.of_cons co),
      List.length_cons]
    constructor
    · rintro ⟨h0, hs⟩ i
      cases i using Fin.cases <;> simp_all
    · intro h; exact ⟨h 0, fun i => h i.succ⟩

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

Goal state before:
pp: case refine_1
n : ℕ
h : IsPrimePow n
k : ℕ
left✝ : k ≤ log 2 n
k_pos : 0 < k
hn₁ : n = n.minFac ^ k
isPrime : Nat.Prime n.minFac
this : n.minFac ^ (k - 1) ≤ n.minFac ^ k
⊢ n.minFac ^ (k - 1) ≤ n - 1

pp: case refine_2
n : ℕ
h : IsPrimePow n
k : ℕ
left✝ : k ≤ log 2 n
k_pos : 0 < k
hn₁ : n = n.minFac ^ k
isPrime : Nat.Prime n.minFac
this : n.minFac ^ (k - 1) ≤ n.minFac ^ k
⊢ ¬n.minFac ^ 2 ∣ n.choose (n.minFac ^ (k - 1))

Tactic:
· refine le_sub_one_of_lt ?_
    nth_rw 2 [hn₁]
    exact Nat.pow_lt_pow_of_lt (Prime.one_lt isPrime) (sub_one_lt_of_lt k_pos)

Goal state after:
case refine_2
n : ℕ
h : IsPrimePow n
k : ℕ
left✝ : k ≤ log 2 n
k_pos : 0 < k
hn₁ : n = n.minFac ^ k
isPrime : Nat.Prime n.minFac
this : n.minFac ^ (k - 1) ≤ n.minFac ^ k
⊢ ¬n.minFac ^ 2 ∣ n.choose (n.minFac ^ (k - 1))
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
hf : (Set.ofPred p).Finite
n : ℕ
hn : n < #hf.toFinset
⊢ (hf.toFinset.sort fun a b ↦ a ≤ b)[n] = (hf.toFinset.sort fun a b ↦ a ≤ b)[⟨n, hn⟩]

pp: case hn
p : ℕ → Prop
hf : (Set.ofPred p).Finite
n : ℕ
hn : n < #hf.toFinset
⊢ n < (hf.toFinset.sort fun a b ↦ a ≤ b).length

Tactic:
Fin.getElem_fin

Goal state after:
p : ℕ → Prop
hf : (Set.ofPred p).Finite
n : ℕ
hn : n < #hf.toFinset
⊢ (hf.toFinset.sort fun a b ↦ a ≤ b)[n] = (hf.toFinset.sort fun a b ↦ a ≤ b)[↑⟨n, hn⟩]

case hn
p : ℕ → Prop
hf : (Set.ofPred p).Finite
n : ℕ
hn : n < #hf.toFinset
⊢ n < (hf.toFinset.sort fun a b ↦ a ≤ b).length
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: case inl.inl
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 : k + 1 < #hf.toFinset
⊢ nth p n ≤ nth p k

Tactic:
(nth_strictMonoOn hf).lt_iff_lt hn hk,

Goal state after:
case inl.inl
p : ℕ → Prop
k : ℕ
hf : (Set.ofPred p).Finite
n : ℕ
hn : n < #hf.toFinset
h : n < k + 1
ha : p (nth p n)
hk : k + 1 < #hf.toFinset
⊢ nth p n ≤ nth p k
Module: Mathlib.Data.Num.Prime

Goal state before:
pp: n : PosNum
⊢ n.bit0.Prime ↔ n = 1

Tactic:
by
        refine Nat.prime_def_minFac.trans ((and_iff_right ?_).trans <| eq_comm.trans ?_)
        · exact add_le_add (Nat.succ_le_of_lt (to_nat_pos _)) (Nat.succ_le_of_lt (to_nat_pos _))
        rw [← minFac_to_nat, to_nat_inj]
        exact ⟨bit0.inj, congr_arg _⟩

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

Goal state before:
pp: α : Type u_1
a b : ZNum
⊢ ↑a < ↑b ↔ ↑a ≤ ↑b ∧ ¬↑b ≤ ↑a

Tactic:
apply lt_iff_le_not_ge

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

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
n : ℤ
⊢ ↑↑n = ↑n

Tactic:
rw [← cast_to_int, to_of_int]

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

Goal state before:
pp: case a
n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h : ↑(pos a) * ↑b < 2 ^ n.succ
⊢ ↑(pos a) * (↑b % ↑(pos a)) < 2 ^ n

Tactic:
rw [pow_succ, ← Nat.mod_add_div b (pos a)] at h

Goal state after:
case a
n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h : ↑(pos a) * (↑b % ↑(pos a) + ↑(pos a) * (↑b / ↑(pos a))) < 2 ^ n * 2
⊢ ↑(pos a) * (↑b % ↑(pos a)) < 2 ^ n
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case pos.inl.inr
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' (↑x) (Ordnode.node rs rl rx rr) o₂
H1 : ¬l.size + (Ordnode.node rs rl rx rr).size ≤ 1
H2 : delta * l.size ≤ rl.size + rr.size
H3_0 : l.size = 0 → rl.size + rr.size ≤ 2
H3p : l.size > 0 → 2 * (rl.size + rr.size) ≤ 9 * l.size + 3
ablem : ∀ {a b : ℕ}, 1 ≤ a → a + b ≤ 2 → b ≤ 1
hlp : l.size > 0 → ¬rl.size + rr.size ≤ 1
h : rl.size < ratio * rr.size
rr0 : rr.size > 0
l0 : l.size = 0
H3 : rr.size + rl.size ≤ 2
this : BalancedSz rl.size rr.size
rl0 : rl.size > 0
rr1 : rr.size = 1
⊢ BalancedSz 0 rl.size ∧ BalancedSz (0 + rl.size + 1) rr.size

Tactic:
rr1,

Goal state after:
case pos.inl.inr
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' (↑x) (Ordnode.node rs rl rx rr) o₂
H1 : ¬l.size + (Ordnode.node rs rl rx rr).size ≤ 1
H2 : delta * l.size ≤ rl.size + rr.size
H3_0 : l.size = 0 → rl.size + rr.size ≤ 2
H3p : l.size > 0 → 2 * (rl.size + rr.size) ≤ 9 * l.size + 3
ablem : ∀ {a b : ℕ}, 1 ≤ a → a + b ≤ 2 → b ≤ 1
hlp : l.size > 0 → ¬rl.size + rr.size ≤ 1
h : rl.size < ratio * rr.size
rr0 : rr.size > 0
l0 : l.size = 0
H3 : rr.size + rl.size ≤ 2
this : BalancedSz rl.size rr.size
rl0 : rl.size > 0
rr1 : rr.size = 1
⊢ BalancedSz 0 rl.size ∧ BalancedSz (0 + rl.size + 1) 1
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: v : PrimeMultiset
p : ℕ
h : p ∈ v.toNatMultiset
⊢ Nat.Prime p

Tactic:
rcases Multiset.mem_map.mp h with ⟨⟨_, hp'⟩, ⟨_, h_eq⟩⟩
  exact h_eq ▸ hp'

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

Goal state before:
pp: v : PrimeMultiset
p : ℕ+
h : p ∈ v.toPNatMultiset
⊢ p.Prime

Tactic:
rcases Multiset.mem_map.mp h with ⟨⟨_, hp'⟩, ⟨_, h_eq⟩⟩
  exact h_eq ▸ hp'

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

Goal state before:
pp: d : ℕ
u : PrimeMultiset
⊢ (d • u).prod = u.prod ^ d

Tactic:
induction d with
  | zero => simp only [zero_nsmul, pow_zero, prod_zero]
  | succ n ih => rw [succ_nsmul, prod_add, ih, pow_succ]

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

Goal state before:
pp: p : ℕ+ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
n : ℕ+
⊢ PNat.find h ≤ n ↔ ∃ m, m ≤ n ∧ p m

Tactic:
by
  simp only [← lt_add_one_iff, find_lt_iff]

Goal state after: