mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Category.Stonean.Basic

Goal state before:
pp: X : CompHaus
inst✝⁶ : Projective X
A B : Type u
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSpace B
inst✝³ : CompactSpace A
inst✝² : T2Space A
inst✝¹ : CompactSpace B
inst✝ : T2Space B
f : ↑X.toTop → B
g : A → B
hf : Continuous[_, inst✝⁴] f
hg : Continuous[inst✝⁵, inst✝⁴] g
hsurj : Function.Surjective g
A' : CompHaus := of A
B' : CompHaus := of B
⊢ ∃ h, Continuous[_, inst✝⁵] h ∧ g ∘ h = f

Tactic:
let f' : X ⟶ B' := CompHausLike.ofHom _ ⟨f, hf⟩

Goal state after:
X : CompHaus
inst✝⁶ : Projective X
A B : Type u
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSpace B
inst✝³ : CompactSpace A
inst✝² : T2Space A
inst✝¹ : CompactSpace B
inst✝ : T2Space B
f : ↑X.toTop → B
g : A → B
hf : Continuous[_, inst✝⁴] f
hg : Continuous[inst✝⁵, inst✝⁴] g
hsurj : Function.Surjective g
A' : CompHaus := of A
B' : CompHaus := of B
f' : X ⟶ B' := CompHausLike.ofHom (fun x ↦ True) { toFun := f, continuous_toFun := hf }
⊢ ∃ h, Continuous[_, inst✝⁵] h ∧ g ∘ h = f
Module: Mathlib.Topology.Category.Stonean.EffectiveEpi

Goal state before:
pp: B X : Stonean
π : X ⟶ B
⊢ [EffectiveEpi π, Epi π, Function.Surjective ⇑(ConcreteCategory.hom π)].TFAE

Tactic:
by
  tfae_have 1 → 2 := fun _ ↦ inferInstance
  tfae_have 2 ↔ 3 := epi_iff_surjective π
  tfae_have 3 → 1 := fun hπ ↦ ⟨⟨effectiveEpiStruct π hπ⟩⟩
  tfae_finish

Goal state after:
Module: Mathlib.Topology.Category.Profinite.CofilteredLimit

Goal state before:
pp: J : Type v
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) α
⊢ ∃ j g,
    LocallyConstant.map (fun a b ↦ if a = b then 0 else 1) f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g

Tactic:
cases nonempty_fintype α

Goal state after:
case intro
J : Type v
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) α
val✝ : Fintype α
⊢ ∃ j g,
    LocallyConstant.map (fun a b ↦ if a = b then 0 else 1) f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: K₁ K₂ S : Finset Λ'
⊢ Supports (K₁ ∪ K₂) S ↔ Supports K₁ S ∧ Supports K₂ S

Tactic:
by
  simp [Supports, or_imp, forall_and]

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

Goal state before:
pp: X : Profiniteᵒᵖ ⥤ Type (u + 1)
inst✝ : PreservesFiniteProducts X
hX : (S : Profinite) → IsColimit (X.mapCocone S.asLimitCone.op)
S : Profiniteᵒᵖ
Y : FintypeCatᵒᵖ
right✝ : Discrete PUnit.{1}
g : toProfinite.op.obj Y ⟶ (fromPUnit S).obj right✝
this :
  ?m.112 ≫ (isoFinYonedaComponents X (toProfinite.obj (Opposite.unop Y))).inv ≫ X.map g =
    (locallyConstantPresheaf
            (X.obj (Opposite.op (CompHausLike.of (fun X ↦ TotallyDisconnectedSpace ↑X) PUnit.{u + 1})))).map
        g ≫
      counitAppApp (Opposite.unop S) X
⊢ colimit.ι
        (CostructuredArrow.proj toProfinite.op S ⋙
          toProfinite.op ⋙ locallyConstantPresheaf (X.obj (Opposite.op (Profinite.of PUnit.{u + 1}))))
        { left := Y, right := right✝, hom := g } ≫
      ((lanPresheafExt (isoFinYoneda X ≪≫ (locallyConstantIsoFinYoneda X).symm)).inv ≫ (lanPresheafNatIso hX).hom).app
        S =
    colimit.ι
        (CostructuredArrow.proj toProfinite.op S ⋙
          toProfinite.op ⋙ locallyConstantPresheaf (X.obj (Opposite.op (Profinite.of PUnit.{u + 1}))))
        { left := Y, right := right✝, hom := g } ≫
      ((lanPresheafNatIso fun x ↦
                isColimitLocallyConstantPresheafDiagram (X.obj (Opposite.op (Profinite.of PUnit.{u + 1}))) x).hom ≫
            counitApp X).app
        S

Tactic:
simpa [locallyConstantIsoFinYoneda, isoFinYoneda, counitApp]

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

Goal state before:
pp: X : LightProfiniteᵒᵖ ⥤ Type u
inst✝ : PreservesFiniteProducts X
hX : (S : LightProfinite) → IsColimit (X.mapCocone (coconeRightOpOfCone S.asLimitCone))
S : LightProfiniteᵒᵖ
Y : FintypeCatᵒᵖ
right✝ : Discrete PUnit.{1}
g : toLightProfinite.op.obj Y ⟶ (fromPUnit S).obj right✝
this :
  ?m.112 ≫ (isoFinYonedaComponents X (toLightProfinite.obj (Opposite.unop Y))).inv ≫ X.map g =
    (locallyConstantPresheaf
            (X.obj
              (Opposite.op
                (CompHausLike.of (fun X ↦ TotallyDisconnectedSpace ↑X ∧ SecondCountableTopology ↑X)
                  PUnit.{u + 1})))).map
        g ≫
      counitAppApp (Opposite.unop S) X
⊢ colimit.ι
        (CostructuredArrow.proj toLightProfinite.op S ⋙
          toLightProfinite.op ⋙ locallyConstantPresheaf (X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))))
        { left := Y, right := right✝, hom := g } ≫
      ((lanPresheafExt (isoFinYoneda X ≪≫ (locallyConstantIsoFinYoneda X).symm)).inv ≫ (lanPresheafNatIso hX).hom).app
        S =
    colimit.ι
        (CostructuredArrow.proj toLightProfinite.op S ⋙
          toLightProfinite.op ⋙ locallyConstantPresheaf (X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))))
        { left := Y, right := right✝, hom := g } ≫
      ((lanPresheafNatIso fun x ↦
                isColimitLocallyConstantPresheafDiagram (X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))) x).hom ≫
            counitApp X).app
        S

Tactic:
simpa [locallyConstantIsoFinYoneda, isoFinYoneda, counitApp]

Goal state after:
Module: Mathlib.Condensed.TopCatAdjunction

Goal state before:
pp: X✝ X : CondensedSet
Y : Type (u + 1)
tY✝ : TopologicalSpace Y
f : ↑X.toTopCat → Y
h : ∀ (S : CompHaus) (g : C(↑S.toTop, ↑X.toTopCat)), Continuous (f ∘ ⇑g)
⊢ ∀ (i : (S : CompHaus) × X.obj.obj (Opposite.op S)), Continuous fun a ↦ (f ∘ X.coinducingCoprod) ⟨i, a⟩

Tactic:
exact fun ⟨S, s⟩ ↦ h S ⟨_, continuous_coinducingCoprod X _⟩

Goal state after:
Module: Mathlib.Control.Fix

Goal state before:
pp: α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := ⋯
n : ℕ
n_ih :
  ∀ (z : Upto p),
    p (n + ↑z) →
      Nat.find h' = n + ↑z →
        ∀ (x' : α) (hwf : WellFounded fun y x ↦ x < y), hwf.fix (fixAux f) z x' = Fix.approx f n.succ x'
z : Upto p
_this : p (n + 1 + ↑z)
hk : Nat.find h' = n + 1 + ↑z
x' : α
hwf✝ : WellFounded fun y x ↦ x < y
x✝ : α
⊢ ↑z < Nat.find h'

Tactic:
lia

Goal state after:
Module: Mathlib.Control.Functor.Multivariate

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
P : β → Prop
x : F (α ::: β)
⊢ LiftP' (α.PredLast' P) x ↔ LiftP (α.PredLast P) x

Tactic:
dsimp only [LiftP, LiftP']

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
P : β → Prop
x : F (α ::: β)
⊢ (∃ u, (fun i ↦ Subtype.val) <$$> u = x) ↔ ∃ u, (fun i ↦ Subtype.val) <$$> u = x
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
α : TypeVec.{u} n
⊢ subtypeVal α.repeatEq ⊚ diagSub = prod.diag

Tactic:
by
  ext i x
  induction i with
  | fz => simp only [comp, subtypeVal, diagSub, prod.diag]
  | fs _ i_ih => apply @i_ih (drop α)

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: case fz
n : ℕ
α α' β β' : TypeVec.{u} n
φ φ' ψ ψ' : Type u
f₀ : α ⟹ α'
g₀ : β ⟹ β'
f₁ : φ → φ'
g₁ : ψ → ψ'
a : ((α ⊗ β) ::: (φ × ψ)) Fin2.fz
⊢ (f₀ ⊗' g₀ ::: Prod.map f₁ g₁) Fin2.fz a = ((f₀ ::: f₁) ⊗' (g₀ ::: g₁)) Fin2.fz a

pp: case fs
n : ℕ
α α' β β' : TypeVec.{u} n
φ φ' ψ ψ' : Type u
f₀ : α ⟹ α'
g₀ : β ⟹ β'
f₁ : φ → φ'
g₁ : ψ → ψ'
a✝ : Fin2 n
a : ((α ⊗ β) ::: (φ × ψ)) a✝.fs
⊢ (f₀ ⊗' g₀ ::: Prod.map f₁ g₁) a✝.fs a = ((f₀ ::: f₁) ⊗' (g₀ ::: g₁)) a✝.fs a

Tactic:
· cases a
    rfl

Goal state after:
case fs
n : ℕ
α α' β β' : TypeVec.{u} n
φ φ' ψ ψ' : Type u
f₀ : α ⟹ α'
g₀ : β ⟹ β'
f₁ : φ → φ'
g₁ : ψ → ψ'
a✝ : Fin2 n
a : ((α ⊗ β) ::: (φ × ψ)) a✝.fs
⊢ (f₀ ⊗' g₀ ::: Prod.map f₁ g₁) a✝.fs a = ((f₀ ::: f₁) ⊗' (g₀ ::: g₁)) a✝.fs a
Module: Mathlib.Data.DFinsupp.Interval

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝⁴ : (i : ι) → Zero (α i)
inst✝³ : (i : ι) → PartialOrder (α i)
inst✝² : (i : ι) → LocallyFiniteOrder (α i)
f g : Π₀ (i : ι), α i
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
⊢ (f.rangeIcc g).support ⊆ f.support ∪ g.support

Tactic:
by
  intro x hx
  by_contra h
  refine notMem_support_iff.2 ?_ hx
  rw [rangeIcc_apply, notMem_support_iff.1 (notMem_mono subset_union_left h),
    notMem_support_iff.1 (notMem_mono subset_union_right h)]
  exact Icc_self _

Goal state after:
Module: Mathlib.Data.Semiquot

Goal state before:
pp: α : Type u_1
β : Type u_2
q : Semiquot α
f : α → β
a : α
aq : a ∈ q
⊢ ∀ (h : ∀ a ∈ q, ∀ b ∈ q, f a = f b), q.liftOn f h = f a

Tactic:
eq_mk_of_mem aq

Goal state after:
α : Type u_1
β : Type u_2
q : Semiquot α
f : α → β
a : α
aq : a ∈ q
⊢ ∀ (h : ∀ a_1 ∈ mk aq, ∀ b ∈ mk aq, f a_1 = f b), (mk aq).liftOn f h = f a
Module: Mathlib.Data.FP.Basic

Goal state before:
pp: C : FloatCfg
this : 0 ≤ ↑(2 * FloatCfg.emax) - ↑prec
⊢ 0 ≤ ↑FloatCfg.emax - (1 - ↑FloatCfg.emax + ↑prec - 1)

Tactic:
lia

Goal state after:
Module: Mathlib.Data.Semiquot

Goal state before:
pp: α : Type u_1
β : Type u_2
q : Semiquot α
f : α → Semiquot β
b : β
⊢ b ∈ q.bind f ↔ ∃ a ∈ q, b ∈ f a

Tactic:
simp_rw [← exists_prop]

Goal state after:
α : Type u_1
β : Type u_2
q : Semiquot α
f : α → Semiquot β
b : β
⊢ b ∈ q.bind f ↔ ∃ a, ∃ (_ : a ∈ q), b ∈ f a
Module: Mathlib.Data.Fin.Tuple.Embedding

Goal state before:
pp: α : Type u_1
n : ℕ
x : Fin n ↪ α
a : α
ha : ¬a ∈ range ⇑x
i : Fin n
⊢ (snoc x ha) i.castSucc = x i

Tactic:
rw [coe_snoc, Fin.snoc_castSucc]

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s₁ s₂ : AList β
p : s₁.entries ~ s₂.entries
⊢ (insert a b s₁).entries ~ (insert a b s₂).entries

Tactic:
simp only [entries_insert]

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s₁ s₂ : AList β
p : s₁.entries ~ s₂.entries
⊢ ⟨a, b⟩ :: kerase a s₁.entries ~ ⟨a, b⟩ :: kerase a s₂.entries
Module: Mathlib.Data.List.AList

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a
b' : β a'
s : AList β
h : a ≠ a'
⊢ (insert a' b' (insert a b s)).entries ~ (insert a b (insert a' b' s)).entries

Tactic:
simp only [entries_insert]

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a
b' : β a'
s : AList β
h : a ≠ a'
⊢ ⟨a', b'⟩ :: kerase a' (⟨a, b⟩ :: kerase a s.entries) ~ ⟨a, b⟩ :: kerase a (⟨a', b'⟩ :: kerase a' s.entries)
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
s✝ : Finmap β
s : AList β
⊢ (erase a (erase a' ⟦s⟧)).entries = (erase a' (erase a ⟦s⟧)).entries

Tactic:
simp only [AList.erase_erase, erase_toFinmap]

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s : Finmap β
h : lookup a s = some b
x : α
h' : x = a
⊢ lookup x (erase a s ∪ singleton a b) = lookup x s

pp: case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s : Finmap β
h : lookup a s = some b
x : α
h' : ¬x = a
⊢ lookup x (erase a s ∪ singleton a b) = lookup x s

Tactic:
· subst a
      rw [lookup_union_right notMem_erase_self, lookup_singleton_eq, h]

Goal state after:
case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s : Finmap β
h : lookup a s = some b
x : α
h' : ¬x = a
⊢ lookup x (erase a s ∪ singleton a b) = lookup x s
Module: Mathlib.Data.Finset.PImage

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
f : α →. β
inst✝ : (x : α) → Decidable (f x).Dom
⊢ pimage f ∅ = ∅

Tactic:
ext
  simp

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

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
l : AList fun _x ↦ M
this : DecidableEq α
⊢ Finset α

Tactic:
haveI := Classical.decEq M

Goal state after:
α : Type u_1
M : Type u_2
inst✝ : Zero M
l : AList fun _x ↦ M
this✝ : DecidableEq α
this : DecidableEq M
⊢ Finset α
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: b : Bool
n : ℕ
⊢ -[Nat.bit (!b) n+1].testBit 0 = b

Tactic:
dsimp [testBit]

Goal state after:
b : Bool
n : ℕ
⊢ (!(Nat.bit (!b) n).testBit 0) = b
Module: Mathlib.Data.Int.Lemmas

Goal state before:
pp: m n : ℕ
⊢ ↑m - ↑n ≤ ↑(m - n)

Tactic:
lia

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

Goal state before:
pp: a b n : ℕ
a_lt_n : a < n
b_lt_n : b < n
⊢ (↑a - ↑b).natAbs < n

Tactic:
← Nat.cast_lt (α := ℤ),

Goal state after:
a b n : ℕ
a_lt_n : a < n
b_lt_n : b < n
⊢ ↑(↑a - ↑b).natAbs < ↑n
Module: Mathlib.Data.Int.Bitwise

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

Tactic:
congr
    simp

Goal state after:
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
inst✝ : Semiring α
d : ℕ
ds : List ℕ
x : Holor α (d :: ds)
h_summands : ∀ (i : ↥(Finset.range d)), CPRankMax ds.prod (unitVec d ↑i ⊗ x.slice ↑i ⋯)
h_dds_prod : (d :: ds).prod = (Finset.range d).card * ds.prod
this : CPRankMax ((Finset.range d).attach.card * ds.prod) (∑ i ∈ (Finset.range d).attach, unitVec d ↑i ⊗ x.slice ↑i ⋯)
⊢ CPRankMax ((Finset.range d).card * ds.prod) (∑ i ∈ (Finset.range d).attach, unitVec d ↑i ⊗ x.slice ↑i ⋯)

Tactic:
Finset.card_attach

Goal state after:
α : Type
inst✝ : Semiring α
d : ℕ
ds : List ℕ
x : Holor α (d :: ds)
h_summands : ∀ (i : ↥(Finset.range d)), CPRankMax ds.prod (unitVec d ↑i ⊗ x.slice ↑i ⋯)
h_dds_prod : (d :: ds).prod = (Finset.range d).card * ds.prod
this : CPRankMax ((Finset.range d).card * ds.prod) (∑ i ∈ (Finset.range d).attach, unitVec d ↑i ⊗ x.slice ↑i ⋯)
⊢ CPRankMax ((Finset.range d).card * ds.prod) (∑ i ∈ (Finset.range d).attach, unitVec d ↑i ⊗ x.slice ↑i ⋯)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case negSucc.negSucc
m n : ℕ
⊢ -[Nat.bitwise (fun x y ↦ !(!x && !y)) m n+1] = -[m+1].land -[n+1]

Tactic:
congr
    simp

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

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

Tactic:
rw [Int.add_mul_ediv_left r q h, ediv_eq_zero_of_lt_abs hz hb]
      simp

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

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

Tactic:
congr
    simp

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

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

Tactic:
congr
    simp

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

Goal state before:
pp: a b r v x : ℤ
⊢ x ∈ {x ∈ Ioc a b | x ≡ v [ZMOD r]} ↔ x ∈ map { toFun := fun x ↦ x + v, inj' := ⋯ } ({x ∈ Ioc (a - v) (b - v) | r ∣ x})

Tactic:
simp_rw [mem_map, mem_filter, mem_Ioc, Function.Embedding.coeFn_mk, ← eq_sub_iff_add_eq,
    exists_eq_right, modEq_comm, modEq_iff_dvd, sub_lt_sub_iff_right, sub_le_sub_iff_right]

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:
lia

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

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

Tactic:
zero_mul,

Goal state after:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
⊢ -↑r < -↑(v % r) ∧ -↑(v % r) ≤ 0
Module: Mathlib.Data.List.TakeWhile

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

Tactic:
lia

Goal state after:
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
h : (dropWhile p tl).length = tl.length + 1
this : (dropWhile p tl).length ≤ tl.length
⊢ False

Tactic:
lia

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
⊢ 0 * ↑r < ↑(b % r - v % r) ∧ ↑(b % r - v % r) ≤ 1 * ↑r

Tactic:
zero_mul,

Goal state after:
case pos
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
h : v % r < b % r
⊢ 0 < ↑(b % r - v % r) ∧ ↑(b % r - v % r) ≤ 1 * ↑r
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: case neg
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
h : ¬v % r < b % r
⊢ -1 * ↑r < ↑(b % r) - ↑(v % r) ∧ ↑(b % r) - ↑(v % r) ≤ 0 * ↑r

Tactic:
zero_mul,

Goal state after:
case neg
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
h : ¬v % r < b % r
⊢ -1 * ↑r < ↑(b % r) - ↑(v % r) ∧ ↑(b % r) - ↑(v % r) ≤ 0
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: n m l : ℕ
⊢ n ≤ l ∧ l < n + (m - n) ↔ n ≤ l ∧ l < m

Tactic:
lia

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

Goal state before:
pp: case e'_3
n m l : ℕ
hnm : n ≤ m
hml : m ≤ l
⊢ l - n = m - n + (l - m)

Tactic:
lia

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

Goal state before:
pp: case inl
α : Type u_1
r : α → α → Prop
s₁ s₂ t : List α
h : Shortlex r s₁ s₂
h1 : s₁.length < s₂.length
⊢ s₁.length < s₂.length + t.length

Tactic:
lia

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

Goal state before:
pp: case inr.cons
α : Type u_1
r : α → α → Prop
s₁ s₂ : List α
h : Shortlex r s₁ s₂
h2 : s₁.length = s₂.length ∧ Lex r s₁ s₂
head : α
tail : List α
⊢ s₁.length < s₂.length + (tail.length + 1)

Tactic:
lia

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

Goal state before:
pp: case inl
α : Type u_1
r : α → α → Prop
t₁ t₂ : List α
h : Shortlex r t₁ t₂
s : List α
h1 : t₁.length < t₂.length
⊢ s.length + t₁.length < s.length + t₂.length

Tactic:
lia

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

Goal state before:
pp: case inr.cons
α : Type u_1
r : α → α → Prop
t₁ t₂ : List α
h : Shortlex r t₁ t₂
h2 : t₁.length = t₂.length ∧ Lex r t₁ t₂
head : α
tail : List α
⊢ Shortlex r (head :: tail ++ t₁) (head :: tail ++ t₂)

Tactic:
apply of_lex
    · simp only [List.cons_append, List.length_cons, List.length_append,
      add_left_inj, add_right_inj]
      exact h2.1
    exact List.Lex.append_left r h2.2 (head :: tail)

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

Goal state before:
pp: α : Type u_1
l : List α
sz : List ℕ
h : sz.sum ≤ l.length
⊢ map length (sz.splitLengths l) = sz

Tactic:
induction sz generalizing l
  · simp
  case cons head tail ih =>
    simp only [sum_cons] at h
    simp only [splitLengths_cons, map_cons, length_take, cons.injEq, min_eq_left_iff]
    rw [ih]
    · simp [Nat.le_of_add_right_le h]
    · simp [Nat.le_sub_of_add_le' h]

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]
this : sz[i] ≤ b
⊢ (sz.splitLengths l)[i].length ≤ b

Tactic:
lia

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

Goal state before:
pp: α : Type u_1
p : ℕ
w : List α
pref : w <+: take p w ++ w
j : ℕ
len : j < w.length - p
⊢ j < w.length

Tactic:
lia

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

Goal state before:
pp: α : Type u_1
p : ℕ
w : List α
pref : w <+: take p w ++ w
j : ℕ
len : j < w.length - p
i1 : j < w.length
⊢ j + p < w.length

Tactic:
lia

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

Goal state before:
pp: α : Type u_1
p : ℕ
w : List α
pref : w <+: take p w ++ w
j : ℕ
len : j < w.length - p
i1 : j < w.length
i2 : j + p < w.length
⊢ p < w.length

Tactic:
lia

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

Goal state before:
pp: case nil
α : Type u_1
m : List α
r : α → α → Bool
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : IsChain (fun y x ↦ r x y = true) g
h : m ∈ splitBy.loop r [] a g []
⊢ IsChain (fun x y ↦ r x y = true) m

Tactic:
rw [splitBy.loop, reverse_cons, mem_append, mem_reverse, mem_singleton] at h
    obtain hm | rfl := h
    · cases not_mem_nil hm
    · apply List.isChain_reverse.1
      rw [reverse_reverse]
      exact isChain_cons.2 ⟨hga, hg⟩

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

Goal state before:
pp: α : Type u_1
p : ℕ
w : List α
lhs : ∀ i < w.length - p, w[i]? = w[i + p]?
i : ℕ
leni : i < w.length - p
⊢ i + p < w.length

Tactic:
lia

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

Goal state before:
pp: α : Type u_1
p i : ℕ
w : List α
per : w.HasPeriod p
less : i < w.length
p_zero : ¬p = 0
large : p ≤ i
⊢ i - p < w.length

Tactic:
lia

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

Goal state before:
pp: α : Type u_1
p i : ℕ
w : List α
per : ∀ i < w.length - p, w[i]? = w[i + p]?
less : i < w.length
p_zero : ¬p = 0
large : p ≤ i
len' : i - p < w.length
IH : w[(i - p) % p]? = w[i - p]?
⊢ i - p < w.length - p

Tactic:
lia

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

Goal state before:
pp: α : Type u_1
p : ℕ
w : List α
mod : ∀ i < w.length, w[i]? = w[i % p]?
i : ℕ
less : i < w.length - p
⊢ i + p < w.length

Tactic:
lia

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

Goal state before:
pp: α : Type u_1
p : ℕ
w : List α
mod : ∀ i < w.length, w[i]? = w[i % p]?
i : ℕ
less : i < w.length - p
⊢ i < w.length

Tactic:
lia

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

Goal state before:
pp: α : Type u_1
u v w : List α
p : ℕ
per : (u ++ v ++ w).HasPeriod p
j : ℕ
len : j < v.length - p
⊢ j < v.length

Tactic:
lia

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

Goal state before:
pp: α : Type u_1
u v w : List α
p : ℕ
per : (u ++ v ++ w).HasPeriod p
j : ℕ
len : j < v.length - p
⊢ u.length ≤ j + u.length

Tactic:
lia

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

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

Tactic:
lia

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

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

Tactic:
lia

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

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

Tactic:
lia

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

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

Tactic:
lia

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_lt_n : j < n
⊢ j < w.length

Tactic:
lia

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_lt_n : ¬j < n
⊢ j - n < w.length

Tactic:
lia

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
⊢ j - n < w.length

Tactic:
lia

Goal state after: