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

Goal state before:
pp: case branch
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₁✝ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁✝
f : σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ : q₁✝ ∈ stmts₁ q₁ → q₀ ∈ stmts₁ q₁
IH₂ : q₁✝ ∈ stmts₁ q₂ → q₀ ∈ stmts₁ q₂
h₁₂ : q₁✝ = branch f q₁ q₂ ∨ q₁✝ ∈ stmts₁ q₁ ∨ q₁✝ ∈ stmts₁ q₂
⊢ q₀ ∈ insert (branch f q₁ q₂) (stmts₁ q₁ ∪ stmts₁ q₂)

Tactic:
rcases h₁₂ with (rfl | h₁₂ | h₁₂)

Goal state after:
case branch.inl
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₀ : Stmt Γ Λ σ
f : σ → Bool
q₁ q₂ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ (branch f q₁ q₂)
IH₁ : branch f q₁ q₂ ∈ stmts₁ q₁ → q₀ ∈ stmts₁ q₁
IH₂ : branch f q₁ q₂ ∈ stmts₁ q₂ → q₀ ∈ stmts₁ q₂
⊢ q₀ ∈ insert (branch f q₁ q₂) (stmts₁ q₁ ∪ stmts₁ q₂)

case branch.inr.inl
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₁✝ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁✝
f : σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ : q₁✝ ∈ stmts₁ q₁ → q₀ ∈ stmts₁ q₁
IH₂ : q₁✝ ∈ stmts₁ q₂ → q₀ ∈ stmts₁ q₂
h₁₂ : q₁✝ ∈ stmts₁ q₁
⊢ q₀ ∈ insert (branch f q₁ q₂) (stmts₁ q₁ ∪ stmts₁ q₂)

case branch.inr.inr
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₁✝ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁✝
f : σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ : q₁✝ ∈ stmts₁ q₁ → q₀ ∈ stmts₁ q₁
IH₂ : q₁✝ ∈ stmts₁ q₂ → q₀ ∈ stmts₁ q₂
h₁₂ : q₁✝ ∈ stmts₁ q₂
⊢ q₀ ∈ insert (branch f q₁ q₂) (stmts₁ q₁ ∪ stmts₁ q₂)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case zero
n : ℕ
⊢ ↑0 = ↑zero >>> n

pp: case pos
n : ℕ
m : PosNum
⊢ ↑(m >>> n) = ↑(pos m) >>> n

Tactic:
· symm
    apply Nat.zero_shiftRight

Goal state after:
case pos
n : ℕ
m : PosNum
⊢ ↑(m >>> n) = ↑(pos m) >>> n
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pos
n : ℕ
m : PosNum
⊢ m.testBit n = (↑(pos m)).testBit n

Tactic:
cast_pos

Goal state after:
case pos
n : ℕ
m : PosNum
⊢ m.testBit n = (↑m).testBit n
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case rfind.mpr
n✝¹ : ℕ
f✝ : List.Vector ℕ n✝¹ →. ℕ
n✝ : ℕ
f : List.Vector ℕ (n✝ + 1) → ℕ
a✝ : Nat.Partrec' ↑f
cf : Code
v : List.Vector ℕ n✝
hf : ∀ (a : ℕ), cf.eval (a :: ↑v) = Part.some [f (a ::ᵥ v)]
n : ℕ
hn : f (n ::ᵥ v) = 0
hm : ∀ {m : ℕ}, m < n → ¬f (m ::ᵥ v) = 0
⊢ ∃
    a ∈
      PFun.fix
        (fun v ↦
          (cf.eval v).bind fun y ↦
            Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
        (0 :: ↑v),
    pure n = [a.headI.pred]

Tactic:
refine ⟨n.succ::v.1, ?_, rfl⟩

Goal state after:
case rfind.mpr
n✝¹ : ℕ
f✝ : List.Vector ℕ n✝¹ →. ℕ
n✝ : ℕ
f : List.Vector ℕ (n✝ + 1) → ℕ
a✝ : Nat.Partrec' ↑f
cf : Code
v : List.Vector ℕ n✝
hf : ∀ (a : ℕ), cf.eval (a :: ↑v) = Part.some [f (a ::ᵥ v)]
n : ℕ
hn : f (n ::ᵥ v) = 0
hm : ∀ {m : ℕ}, m < n → ¬f (m ::ᵥ v) = 0
⊢ n.succ :: ↑v ∈
    PFun.fix
      (fun v ↦
        (cf.eval v).bind fun y ↦
          Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
      (0 :: ↑v)
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: n✝¹ : ℕ
f✝ : List.Vector ℕ n✝¹ →. ℕ
n✝ : ℕ
f : List.Vector ℕ (n✝ + 1) → ℕ
a✝ : Nat.Partrec' ↑f
cf : Code
v : List.Vector ℕ n✝
hf : ∀ (a : ℕ), cf.eval (a :: ↑v) = Part.some [f (a ::ᵥ v)]
n : ℕ
hn : f (n ::ᵥ v) = 0
hm : ∀ {m : ℕ}, m < n → ¬f (m ::ᵥ v) = 0
⊢ Sum.inl (n.succ :: ↑v) ∈
    (cf.eval (n :: ↑v)).bind fun y ↦
      Part.some
        (if y.headI = 0 then Sum.inl ((n :: ↑v).headI.succ :: (n :: ↑v).tail)
        else Sum.inr ((n :: ↑v).headI.succ :: (n :: ↑v).tail))

Tactic:
simp [hf, hn]

Goal state after:
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case pos
k' : Cont
a✝¹ : Code
a✝ : Cont
k_ih : ∀ {v : List ℕ}, stepRet (a✝.then k') v = (stepRet a✝ v).then k'
v : List ℕ
h✝ : v.headI = 0
⊢ (stepRet a✝ v.tail).then k' = (stepRet a✝ v.tail).then k'

Tactic:
← k_ih

Goal state after:
case pos
k' : Cont
a✝¹ : Code
a✝ : Cont
k_ih : ∀ {v : List ℕ}, stepRet (a✝.then k') v = (stepRet a✝ v).then k'
v : List ℕ
h✝ : v.headI = 0
⊢ stepRet (a✝.then k') v.tail = stepRet (a✝.then k') v.tail
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case some
α : Type u_1
p : α → Bool
a : α
L l₁ l₂ : List α
h₁ : ∀ x ∈ l₁, p x = false
IH :
  ∀ (l₁ : List α) (o : Option α) (l₂ : List α),
    (∀ x ∈ l₁, p x = false) →
      Option.elim' (L = l₁ ∧ l₂ = []) (fun a ↦ p a = true ∧ L = l₁ ++ a :: l₂) o → splitAtPred p L = (l₁, o, l₂)
o : α
h₂ : Option.elim' (a :: L = l₁ ∧ l₂ = []) (fun a_1 ↦ p a_1 = true ∧ a :: L = l₁ ++ a_1 :: l₂) (some o)
⊢ (bif p a then ([], some a, L)
    else
      match splitAtPred p L with
      | (l₁, o, l₂) => (a :: l₁, o, l₂)) =
    (l₁, some o, l₂)

Tactic:
rcases l₁ with - | ⟨a', l₁⟩ <;> rcases h₂ with ⟨h₂, ⟨⟩⟩

Goal state after:
case some.nil
α : Type u_1
p : α → Bool
a : α
L : List α
IH :
  ∀ (l₁ : List α) (o : Option α) (l₂ : List α),
    (∀ x ∈ l₁, p x = false) →
      Option.elim' (L = l₁ ∧ l₂ = []) (fun a ↦ p a = true ∧ L = l₁ ++ a :: l₂) o → splitAtPred p L = (l₁, o, l₂)
h₁ : ∀ x ∈ [], p x = false
h₂ : p a = true
⊢ (bif p a then ([], some a, L)
    else
      match splitAtPred p L with
      | (l₁, o, l₂) => (a :: l₁, o, l₂)) =
    ([], some a, L)

case some.cons
α : Type u_1
p : α → Bool
a : α
l₂ : List α
o : α
l₁ : List α
h₂ : p o = true
h₁ : ∀ x ∈ a :: l₁, p x = false
IH :
  ∀ (l₁_1 : List α) (o_1 : Option α) (l₂_1 : List α),
    (∀ x ∈ l₁_1, p x = false) →
      Option.elim' (l₁.append (o :: l₂) = l₁_1 ∧ l₂_1 = [])
          (fun a ↦ p a = true ∧ l₁.append (o :: l₂) = l₁_1 ++ a :: l₂_1) o_1 →
        splitAtPred p (l₁.append (o :: l₂)) = (l₁_1, o_1, l₂_1)
⊢ (bif p a then ([], some a, l₁.append (o :: l₂))
    else
      match splitAtPred p (l₁.append (o :: l₂)) with
      | (l₁, o, l₂) => (a :: l₁, o, l₂)) =
    (a :: l₁, some o, l₂)
Module: Mathlib.Topology.ClopenBox

Goal state before:
pp: case h
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : CompactSpace Y
inst✝ : CompactSpace X
W : Clopens (X × Y)
U : X × Y → Clopens X
hxU : ∀ x ∈ W, x.1 ∈ U x
V : X × Y → Clopens Y
hxV : ∀ x ∈ W, x.2 ∈ V x
hUV : ∀ x ∈ W, U x ×ˢ V x ≤ W
I : Finset (X × Y)
hIW : ∀ x ∈ I, x ∈ W.carrier
hWI : W.carrier ⊆ ⋃ x ∈ I, ↑(U x) ×ˢ ↑(V x)
⊢ W = (Finset.image (fun x ↦ (U x, V x)) I).sup fun i ↦ i.1 ×ˢ i.2

Tactic:
rw [Finset.sup_image]

Goal state after:
case h
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : CompactSpace Y
inst✝ : CompactSpace X
W : Clopens (X × Y)
U : X × Y → Clopens X
hxU : ∀ x ∈ W, x.1 ∈ U x
V : X × Y → Clopens Y
hxV : ∀ x ∈ W, x.2 ∈ V x
hUV : ∀ x ∈ W, U x ×ˢ V x ≤ W
I : Finset (X × Y)
hIW : ∀ x ∈ I, x ∈ W.carrier
hWI : W.carrier ⊆ ⋃ x ∈ I, ↑(U x) ×ˢ ↑(V x)
⊢ W = I.sup ((fun i ↦ i.1 ×ˢ i.2) ∘ fun x ↦ (U x, V x))
Module: Mathlib.Topology.ClopenBox

Goal state before:
pp: case refine_3
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : TotallyDisconnectedSpace X
h : SecondCountableTopology X
⊢ Countable (Clopens X)

Tactic:
have : ∀ (s : Clopens X), ∃ (t : Finset (countableBasis X)), s.1 = (SetLike.coe t).sUnion :=
      fun s ↦ eq_sUnion_finset_of_isTopologicalBasis_of_isCompact_open _
        (isBasis_countableBasis X) s.1 s.2.1.isCompact s.2.2
    let f : Clopens X → Finset (countableBasis X) := fun s ↦ (this s).choose
    have hf : f.Injective := by
      intro s t (h : Exists.choose _ = Exists.choose _)
      ext1; change s.carrier = t.carrier
      rw [(this s).choose_spec, (this t).choose_spec, h]
    exact hf.countable

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case fix
S : Finset Λ'
f : Code
IHf : ∀ {k : Cont'}, codeSupp f k ⊆ S → Supports (codeSupp' f k) S
k : Cont'
H H' : codeSupp f.fix k ⊆ S
⊢ Supports (codeSupp' f.fix k) S

Tactic:
simp only [codeSupp_fix, Finset.union_subset_iff] at H'

Goal state after:
case fix
S : Finset Λ'
f : Code
IHf : ∀ {k : Cont'}, codeSupp f k ⊆ S → Supports (codeSupp' f k) S
k : Cont'
H : codeSupp f.fix k ⊆ S
H' : trStmts₁ (trNormal f.fix k) ⊆ S ∧ codeSupp f (Cont'.fix f k) ⊆ S
⊢ Supports (codeSupp' f.fix k) S
Module: Mathlib.Condensed.Explicit

Goal state before:
pp: A : Type u_1
inst✝⁵ : Category.{v_1, u_1} A
inst✝⁴ : ∀ (X : CompHausᵒᵖ), HasLimitsOfShape (StructuredArrow X Stonean.toCompHaus.op) A
FA : A → A → Type u_2
CA : A → Type u_3
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
inst✝¹ : ReflectsFiniteProducts (CategoryTheory.forget A)
F : Stoneanᵒᵖ ⥤ A
inst✝ : PreservesFiniteProducts (F ⋙ CategoryTheory.forget A)
⊢ IsSheaf (coherentTopology Stonean) F

Tactic:
apply isSheaf_coherent_of_projective_of_comp F (CategoryTheory.forget A)

Goal state after:
A : Type u_1
inst✝⁵ : Category.{v_1, u_1} A
inst✝⁴ : ∀ (X : CompHausᵒᵖ), HasLimitsOfShape (StructuredArrow X Stonean.toCompHaus.op) A
FA : A → A → Type u_2
CA : A → Type u_3
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
inst✝¹ : ReflectsFiniteProducts (CategoryTheory.forget A)
F : Stoneanᵒᵖ ⥤ A
inst✝ : PreservesFiniteProducts (F ⋙ CategoryTheory.forget A)
⊢ IsSheaf (coherentTopology Stonean) (F ⋙ CategoryTheory.forget A)
Module: Mathlib.Condensed.Discrete.Module

Goal state before:
pp: P : TopCat → Prop
R : Type u
inst✝ : Ring R
X✝ Y✝ : ModuleCat R
f : X✝ ⟶ Y✝
⊢ ((functorIsoDiscreteAux₂ R X✝).hom ≫ (discreteUnderlyingAdj (ModuleCat R)).counit.app ((functor R).obj X✝)) ≫
      (functor R).map f =
    (presheafToSheaf (coherentTopology LightProfinite) (ModuleCat R)).map ((Functor.const LightProfiniteᵒᵖ).map f) ≫
      (functorIsoDiscreteAux₂ R Y✝).hom ≫ (discreteUnderlyingAdj (ModuleCat R)).counit.app ((functor R).obj Y✝)

Tactic:
Category.assoc,

Goal state after:
P : TopCat → Prop
R : Type u
inst✝ : Ring R
X✝ Y✝ : ModuleCat R
f : X✝ ⟶ Y✝
⊢ (functorIsoDiscreteAux₂ R X✝).hom ≫
      (discreteUnderlyingAdj (ModuleCat R)).counit.app ((functor R).obj X✝) ≫ (functor R).map f =
    (presheafToSheaf (coherentTopology LightProfinite) (ModuleCat R)).map ((Functor.const LightProfiniteᵒᵖ).map f) ≫
      (functorIsoDiscreteAux₂ R Y✝).hom ≫ (discreteUnderlyingAdj (ModuleCat R)).counit.app ((functor R).obj Y✝)
Module: Mathlib.Condensed.Light.Epi

Goal state before:
pp: R : Type u
inst✝ : Ring R
X Y : LightCondMod R
f✝ : X ⟶ Y
X✝ Y✝ : LightCondMod R
f : X✝ ⟶ Y✝
hf : Epi f
⊢ Epi ((LightCondensed.forget R).map f)

Tactic:
rw [← Sheaf.isLocallySurjective_iff_epi'] at hf ⊢
    exact (Presheaf.isLocallySurjective_iff_whisker_forget _ f.hom).mp hf

Goal state after:
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: X : Type u
S : LightProfinite
s : Cocone (S.diagram.rightOp ⋙ locallyConstantPresheaf X)
n : ℕ
f : LocallyConstant (↑(S.diagram.obj (Opposite.op n)).toTop) X
⊢ (ConcreteCategory.hom ((isColimitLocallyConstantPresheafDiagram X S).desc s))
      (LocallyConstant.comap (TopCat.Hom.hom (S.asLimitCone.π.app (Opposite.op n)).hom) f) =
    (ConcreteCategory.hom (s.ι.app n)) f

Tactic:
by
  change ((((locallyConstantPresheaf X).mapCocone (coconeRightOpOfCone S.asLimitCone)).ι.app n) ≫
    (isColimitLocallyConstantPresheafDiagram X S).desc s) _ = _
  rw [(isColimitLocallyConstantPresheafDiagram X S).fac]

Goal state after:
Module: Mathlib.Control.Bitraversable.Lemmas

Goal state before:
pp: t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
inst✝ : LawfulBitraversable t
α α' β : Type u
f : α → α'
x : t α β
⊢ tfst (pure ∘ f) x = pure (fst f x)

Tactic:
apply bitraverse_eq_bimap_id

Goal state after:
Module: Mathlib.Control.Bitraversable.Lemmas

Goal state before:
pp: t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
inst✝ : LawfulBitraversable t
α β β' : Type u
f : β → β'
x : t α β
⊢ tsnd (pure ∘ f) x = pure (snd f x)

Tactic:
apply bitraverse_eq_bimap_id

Goal state after:
Module: Mathlib.Control.Fold

Goal state before:
pp: α β : Type u
m : Type u → Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : β → α → m α
⊢ ⇑(foldrM.ofFreeMonoid f) ∘ FreeMonoid.of = foldrM.mk ∘ f

Tactic:
by
  ext
  simp [(· ∘ ·), foldrM.ofFreeMonoid, foldrM.mk, Function.flip_def]

Goal state after:
Module: Mathlib.Data.DFinsupp.Interval

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → DecidableEq (α i)
inst✝² : (i : ι) → PartialOrder (α i)
inst✝¹ : (i : ι) → Zero (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
f g : Π₀ (i : ι), α i
⊢ #(Ico f g) = ∏ i ∈ f.support ∪ g.support, #(Icc (f i) (g i)) - 1

Tactic:
by
  rw [card_Ico_eq_card_Icc_sub_one, card_Icc]

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

Goal state before:
pp: α : Type u_1
s : Finset α
f : α → ℕ∞
hf : ∀ a ∈ s, f a ≠ ⊤
⊢ ∑ a ∈ s, f a = ∑ x ∈ s, ↑(f x).toNat

Tactic:
exact sum_congr rfl fun x hx => (natCast_toNat (hf x hx)).symm

Goal state after:
Module: Mathlib.Data.Semiquot

Goal state before:
pp: α : Type u_1
q : Semiquot α
p : q.IsPure
a : α
⊢ a ∈ q ↔ a ∈ pure (q.get p)

Tactic:
simpa using ⟨fun h => p _ h _ (get_mem _), fun e => e.symm ▸ get_mem _⟩

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

Goal state before:
pp: n : ℕ
α : Fin n → Sort u_1
m : ℕ
h : m ≤ n
v : (i : Fin n) → α i
i : Fin n
hi : ↑i ≥ m
x : α i
j : Fin m
⊢ ↑j ≠ ↑i

Tactic:
exact Nat.ne_of_lt (lt_of_lt_of_le j.isLt hi)

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: case e_4
α : Type u
β : α → Type v
inst✝ : Unique α
e : FinEnum α
⊢ (fun a b ↦ decEq a b) = fun a b ↦ decidableEq_of_subsingleton a b

Tactic:
· subsingleton

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

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

Tactic:
ext : 1; simp only [AList.entries_insert, List.kerase_cons_eq]

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

Goal state before:
pp: α : Type u
β : α → Type v
a : α
l : List (Sigma β)
h : a ∈ l.keys
⊢ ∃ b, ⟨a, b⟩ ∈ l

Tactic:
by
  have := exists_of_mem_map h
  grind

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

Goal state before:
pp: α : Type u
β : α → Type v
a : α
b b' : β a
l : List (Sigma β)
nd : l.NodupKeys
h : ⟨a, b⟩ ∈ l
h' : ⟨a, b'⟩ ∈ l
⊢ b = b'

Tactic:
by
  grind [NodupKeys.eq_of_fst_eq]

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
⊢ ∀ (a_1 b_1 : Sigma β), (b_1 ∈ if a = a_1.fst then some ⟨a, b⟩ else none) → a_1.fst = b_1.fst

Tactic:
rintro ⟨a₁, b₂⟩ ⟨a₂, b₂⟩

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
a₁ : α
b₂✝ : β a₁
a₂ : α
b₂ : β a₂
⊢ (⟨a₂, b₂⟩ ∈ if a = ⟨a₁, b₂✝⟩.fst then some ⟨a, b⟩ else none) → ⟨a₁, b₂✝⟩.fst = ⟨a₂, b₂⟩.fst
Module: Mathlib.Data.Finset.NatDivisors

Goal state before:
pp: m n : ℕ
hmn : m.Coprime n
dm₁ dn₁ : ℕ
h₁ : (dm₁, dn₁) ∈ ↑(m.divisors ×ˢ n.divisors)
dm₂ dn₂ : ℕ
h₂ : (dm₂, dn₂) ∈ ↑(m.divisors ×ˢ n.divisors)
hd : (fun p ↦ p.1 * p.2) (dm₁, dn₁) = (fun p ↦ p.1 * p.2) (dm₂, dn₂)
⊢ (dm₁, dn₁) = (dm₂, dn₂)

Tactic:
simp only [Finset.mem_coe, Finset.mem_product, mem_divisors] at *

Goal state after:
m n : ℕ
hmn : m.Coprime n
dm₁ dn₁ dm₂ dn₂ : ℕ
hd : dm₁ * dn₁ = dm₂ * dn₂
h₁ : (dm₁ ∣ m ∧ m ≠ 0) ∧ dn₁ ∣ n ∧ n ≠ 0
h₂ : (dm₂ ∣ m ∧ m ≠ 0) ∧ dn₂ ∣ n ∧ n ≠ 0
⊢ (dm₁, dn₁) = (dm₂, dn₂)
Module: Mathlib.Data.Finset.PiInduction

Goal state before:
pp: case intro.a.inr
ι : Type u_1
α : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)
p : ((i : ι) → Finset (α i)) → Prop
h0 : p fun x ↦ ∅
step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), r i x (g i) → p g → p (update g i (insert x (g i)))
val✝ : Fintype ι
f : (i : ι) → Finset (α i)
ihs : ∀ t ⊂ univ.sigma f, ∀ (f : (i : ι) → Finset (α i)), univ.sigma f = t → p f
hne : (univ.sigma f).Nonempty
i : ι
hi : (f i).Nonempty
x : α i
x_mem : x ∈ f i
hr : r i x ((f i).erase x)
⊢ p f

Tactic:
set g := update f i ((f i).erase x) with hg

Goal state after:
case intro.a.inr
ι : Type u_1
α : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)
p : ((i : ι) → Finset (α i)) → Prop
h0 : p fun x ↦ ∅
step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), r i x (g i) → p g → p (update g i (insert x (g i)))
val✝ : Fintype ι
f : (i : ι) → Finset (α i)
ihs : ∀ t ⊂ univ.sigma f, ∀ (f : (i : ι) → Finset (α i)), univ.sigma f = t → p f
hne : (univ.sigma f).Nonempty
i : ι
hi : (f i).Nonempty
x : α i
x_mem : x ∈ f i
hr : r i x ((f i).erase x)
g : (a : ι) → Finset (α a) := update f i ((f i).erase x)
hg : g = update f i ((f i).erase x)
⊢ p f
Module: Mathlib.Data.Finsupp.NeLocus

Goal state before:
pp: α : Type u_1
N : Type u_3
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : Zero N
f : α →₀ N
a✝ : α
⊢ f a✝ ≠ 0 a✝ ↔ a✝ ∈ f.support

Tactic:
mem_support_iff,

Goal state after:
α : Type u_1
N : Type u_3
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : Zero N
f : α →₀ N
a✝ : α
⊢ f a✝ ≠ 0 a✝ ↔ f a✝ ≠ 0
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 g : α →₀ N
⊢ f.neLocus (f - g) = g.support

Tactic:
by
  rw [sub_eq_add_neg, neLocus_self_add_right, support_neg]

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

Goal state before:
pp: b : Bool
n : ℕ
⊢ (bit b ↑n).testBit 0 = b

Tactic:
rw [bit_coe_nat]; apply Nat.testBit_bit_zero

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

Goal state before:
pp: a b : ℤ
⊢ a.natAbs ≤ b.natAbs ↔ ↑a.natAbs ≤ ↑b.natAbs

Tactic:
exact Int.ofNat_le.symm

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

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

Tactic:
exact ⟨h, ((mod_lt _ hr).trans_le (by simp)).le⟩

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

Goal state before:
pp: α : Type u_1
l✝ : List α
x : α
l : List α
y : α
hp : l.reverse = l → l.Palindrome
hr : [y].reverse ++ l.reverse ++ [x] = x :: (l ++ [y])
this : l.Palindrome
⊢ (x :: (l ++ [x])).Palindrome

Tactic:
exact Palindrome.cons_concat x this

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

Goal state before:
pp: α : Type u_1
l : List α
sz : List ℕ
i : ℕ
hi : i < (sz.splitLengths l).length
⊢ i < sz.length

Tactic:
simpa using hi

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

Goal state before:
pp: α✝ : Type u_1
l✝ : List α✝
sz✝ : List ℕ
α : Type u_2
l : List α
sz : List ℕ
h : sz.sum ≤ l.length
i : ℕ
hi : i < (sz.splitLengths l).length
⊢ i < sz.length

Tactic:
simpa using hi

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

Goal state before:
pp: α : Type u_2
l : List α
sz : List ℕ
h : sz.sum ≤ l.length
i : ℕ
hi : i < (sz.splitLengths l).length
this : map length (sz.splitLengths l) = sz
⊢ i < (map length (sz.splitLengths l)).length

Tactic:
simpa using hi

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

Goal state before:
pp: α : Type u_2
l : List α
sz : List ℕ
b : ℕ
h : ∀ (n : ℕ), n ∈ sz → n ≤ b
i : ℕ
hi : i < (sz.splitLengths l).length
this : (sz.splitLengths l)[i].length ≤ sz[i]
⊢ i < sz.length

Tactic:
simpa using hi

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

Goal state before:
pp: case inr.inr
α : 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
⊢ (take n w ++ w)[i]? = (take n w ++ w)[i % p]?

Tactic:
have mod_p : ∀ j < n + length w, (take n w ++ w)[j]? = w[j % p]? := by
    intro j less_j
    by_cases j_lt_n : j < n
    · -- indices within `take n w` can be reduced due to the period of `w`
      calc
        (take n w ++ w)[j]? = (take n w)[j]? := getElem?_append_left (by simp_all)
        _ = w[j]? := getElem?_take_of_lt j_lt_n
        _ = w[j % p]? := Eq.symm (mod_w j (by lia))
    · -- larger indices are indices of `w` decreased by `n`
      have j_minus : j - n < w.length := by lia
      have n_le_j : n ≤ j := le_of_not_gt j_lt_n; clear j_lt_n;
      have j_mod : (j - n) % p = j % p := by
        calc
          (j - n) % p = (j - p * (n / p)) % p := by rw [Nat.mul_div_cancel' dvd]
          _ = j % p := sub_mul_mod ((Nat.mul_div_cancel' dvd).symm ▸ n_le_j)
      calc
        (take n w ++ w)[j]? = w[j - (take n w).length]? := getElem?_append_right (by simp_all)
        _ = w[j - n]? := by simp_all
        _ = w[(j - n) % p]? := Eq.symm (mod_w (j - n) (by lia))
        _ = w[j % p]? := by rw [j_mod]

Goal state after:
case inr.inr
α : 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
mod_p : ∀ j < n + w.length, (take n w ++ w)[j]? = w[j % p]?
⊢ (take n w ++ w)[i]? = (take n w ++ w)[i % p]?
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
⊢ q ≤ w.length - q

Tactic:
have : p.gcd q ≤ p - q := by
          rw [← gcd_stable]; apply gcd_le_left q; lia

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
this : p.gcd q ≤ p - q
⊢ q ≤ w.length - q
Module: Mathlib.Data.NNRat.Lemmas

Goal state before:
pp: q₁ q₂ : ℚ≥0
⊢ ↑q₁.num * ↑q₂.num = ↑(q₁ * q₂).num * ↑((q₁.num * q₂.num).gcd (q₁.den * q₂.den))

Tactic:
convert! Rat.num_mul_num_eq_num_mul_gcd q₁ q₂ <;> norm_cast

Goal state after:
Module: Mathlib.Data.Nat.Prime.Factorial

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

Tactic:
rintro ⟨p, hp, hdvd, hdvd'⟩
    exact le_trans (minFac_le_of_dvd hp.two_le hdvd) (hp.dvd_factorial.mp hdvd')

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

Goal state before:
pp: n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
| fun i ↦ ∑ j ∈ range (n / p + 1), X ^ i * ↑((n % p).choose i) * (X ^ (p * j) * ↑((n / p).choose j))

Tactic:
k,

Goal state after:
n k✝ p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
k : ℕ
| ∑ j ∈ range (n / p + 1), X ^ k * ↑((n % p).choose k) * (X ^ (p * j) * ↑((n / p).choose j))
Module: Mathlib.Data.Nat.Factorization.Divisors

Goal state before:
pp: n : ℕ
⊢ n.properDivisors =
    Finset.map { toFun := fun x ↦ (↑x).prod fun x1 x2 ↦ x1 ^ x2, inj' := ⋯ } (Finset.Iio n.factorization).attach

Tactic:
by
  rw [Finset.map_eq_image]
  change _ = (Finset.Iio n.factorization).attach.image ((·.prod (· ^ ·)) ∘ Subtype.val)
  rw [← Finset.image_image, Finset.attach_image_val]
  exact properDivisors_eq_image_Iio_factorization_prod_pow

Goal state after: