mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Condensed.Discrete.LocallyConstant

Goal state before:
pp: P : TopCat → Prop
inst✝⁴ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
S : CompHausLike P
Y : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝³ : HasProp P PUnit.{u + 1}
f : LocallyConstant (↑S.toTop) (Y.obj (op (of P PUnit.{u + 1})))
T : CompHausLike P
g : T ⟶ S
X✝ : TopCat
inst✝² : HasExplicitFiniteCoproducts P
inst✝¹ : HasExplicitPullbacks P
hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Surjective ⇑(ConcreteCategory.hom f)
inst✝ : HasExplicitFiniteCoproducts P
X : Sheaf (coherentTopology (CompHausLike P)) (Type (max u w))
x : X.obj.obj (op (of P PUnit.{u + 1}))
this✝ : Preregular (CompHausLike P)
this : PreservesFiniteProducts ((sheafToPresheaf (coherentTopology (CompHausLike P)) (Type (max u w))).obj X) :=
  @CompHausLike.LocallyConstant.adjunction._proof_2 P inst✝² inst✝¹ hs X this✝
a : Fiber ⇑((ConcreteCategory.hom ((unit P hs).app (X.obj.obj (op (of P PUnit.{u + 1}))))) x)
⊢ PUnit.unit ∈ ↑a

Tactic:
by simp [mem_iff_eq_image, ← map_preimage_eq_image]

Goal state after:
Module: Mathlib.Condensed.Epi

Goal state before:
pp: A : Type u'
inst✝⁹ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type v'
inst✝⁸ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝⁷ : ConcreteCategory A FA
inst✝⁶ : HasFunctorialSurjectiveInjectiveFactorization A
X Y : Condensed A
f : X ⟶ Y
inst✝⁵ : PreservesFiniteProducts (CategoryTheory.forget A)
inst✝⁴ : ∀ (X : CompHausᵒᵖ), HasLimitsOfShape (StructuredArrow X Stonean.toCompHaus.op) A
inst✝³ : (extensiveTopology Stonean).WEqualsLocallyBijective A
inst✝² : HasSheafify (extensiveTopology Stonean) A
inst✝¹ : (extensiveTopology Stonean).HasSheafCompose (CategoryTheory.forget A)
inst✝ : Balanced (Sheaf (extensiveTopology Stonean) A)
⊢ Epi f ↔ ∀ (S : Stonean), Function.Surjective ⇑(hom (f.hom.app (op S.compHaus)))

Tactic:
by
  rw [← (StoneanCompHaus.equivalence A).inverse.epi_map_iff_epi,
    ← Presheaf.coherentExtensiveEquivalence.functor.epi_map_iff_epi,
    ← isLocallySurjective_iff_epi']
  exact extensiveTopology.isLocallySurjective_iff (D := A) _

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

Goal state before:
pp: F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
X : Type u
hc : IsLimit c
inst✝ : ∀ (i : ℕᵒᵖ), Epi (c.π.app i)
⊢ IsColimit ((locallyConstantPresheaf X).mapCocone c.op)

Tactic:
by
  refine Types.FilteredColimit.isColimitOf _ _ ?_ ?_
  · intro (f : LocallyConstant c.pt X)
    obtain ⟨j, h⟩ := Profinite.exists_locallyConstant.{_, 0} (lightToProfinite.mapCone c)
      (isLimitOfPreserves lightToProfinite hc) f
    exact ⟨⟨j⟩, h⟩
  · intro ⟨i⟩ ⟨j⟩ (fi : LocallyConstant _ _) (fj : LocallyConstant _ _)
      (h : fi.comap (c.π.app i).hom.hom = fj.comap (c.π.app j).hom.hom)
    obtain ⟨k, ki, kj, _⟩ := IsCofilteredOrEmpty.cone_objs i j
    refine ⟨⟨k⟩, ki.op, kj.op, ?_⟩
    dsimp
    ext x
    obtain ⟨x, hx⟩ := ((LightProfinite.epi_iff_surjective (c.π.app k)).mp inferInstance) x
    rw [← hx]
    change fi ((c.π.app k ≫ (F ⋙ toLightProfinite).map _) x) =
      fj ((c.π.app k ≫ (F ⋙ toLightProfinite).map _) x)
    have h := LocallyConstant.congr_fun h x
    dsimp [- CompHausLike.coe_comp] -- `coe_comp` prevents rewriting with `c.w`
    rwa [dsimp% c.w, dsimp% c.w]

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

Goal state before:
pp: case refine_1
R : Type u
inst✝ : CommRing R
P : LightCondMod R
x✝ : InternallyProjective P
A B : LightCondMod R
e : A ⟶ B
he : Epi e
S : LightProfinite
g : P ⊗ (free R).obj S.toCondensed ⟶ B
h : isInternallyProjective P
hh : Epi ((ihom P).map e)
⊢ ∃ S' π,
    ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
      ∃ g', P ◁ (lightProfiniteToLightCondSet ⋙ free R).map π ≫ g = g' ≫ e

Tactic:
rw [LightCondMod.epi_iff_locallySurjective_on_lightProfinite] at hh

Goal state after:
case refine_1
R : Type u
inst✝ : CommRing R
P : LightCondMod R
x✝ : InternallyProjective P
A B : LightCondMod R
e : A ⟶ B
he : Epi e
S : LightProfinite
g : P ⊗ (free R).obj S.toCondensed ⟶ B
h : isInternallyProjective P
hh :
  ∀ (S : LightProfinite) (y : ↑((P ⟹ B).obj.obj (Opposite.op S))),
    ∃ S' φ,
      ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom φ)),
        ∃ x,
          (ConcreteCategory.hom (((ihom P).map e).hom.app (Opposite.op S'))) x =
            (ConcreteCategory.hom ((P ⟹ B).obj.map (Opposite.op φ))) y
⊢ ∃ S' π,
    ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
      ∃ g', P ◁ (lightProfiniteToLightCondSet ⋙ free R).map π ≫ g = g' ≫ e
Module: Mathlib.Topology.Category.LightProfinite.Injective

Goal state before:
pp: X : Type u_1
Y : Type u_2
S : Type u_3
T : Type u_4
inst✝¹⁰ : TopologicalSpace X
inst✝⁹ : CompactSpace X
inst✝⁸ : TopologicalSpace Y
inst✝⁷ : CompactSpace Y
inst✝⁶ : T2Space Y
inst✝⁵ : TotallyDisconnectedSpace Y
inst✝⁴ : TopologicalSpace S
inst✝³ : T2Space S
inst✝² : Finite S
inst✝¹ : TopologicalSpace T
inst✝ : T2Space T
f : X → Y
hf : Continuous[inst✝¹⁰, inst✝⁸] f
f_inj : Function.Injective f
f' : S → T
f'_surj : Function.Surjective f'
g : X → S
hg : Continuous[inst✝¹⁰, inst✝⁴] g
g' : Y → T
hg' : Continuous[inst✝⁸, inst✝¹] g'
h_comm : g' ∘ f = f' ∘ g
this : Finite T
Z : S → Set Y := fun i ↦ f '' g ⁻¹' {i}
Z_closed : ∀ (i : S), IsClosed[inst✝⁸] (Z i)
Z_disj : univ.PairwiseDisjoint Z
D : S → Set Y := fun i ↦ g' ⁻¹' {f' i}
D_clopen : ∀ (i : S), IsClopen (D i)
Z_subset_D : ∀ (i : S), Z i ⊆ D i
C : S → Set Y
C_clopen : ∀ (i : S), IsClopen (C i)
Z_subset_C : ∀ (i : S), Z i ⊆ C i
C_subset_D : ∀ (i : S), C i ⊆ D i
C_cover_D : ⋃ i, D i ⊆ ⋃ i, C i
C_disj : univ.PairwiseDisjoint C
D_cover_univ : univ ⊆ ⋃ i, D i
C_cover_univ : ⋃ i, C i = univ
h_glue : ∀ (i j : S), ∀ x ∈ C i, x ∈ C j → i = j
y : Y
⊢ y ∈ ⋃ i, C i

Tactic:
simp [C_cover_univ]

Goal state after:
Module: Mathlib.Topology.Category.LightProfinite.Injective

Goal state before:
pp: S : LightProfinite
inst✝ : Nonempty ↑S.toTop
X Y : Profinite
g : X ⟶ lightToProfinite.obj S
f : X ⟶ Y
h : Mono f
this✝¹ : ∀ (n : ℕ), Finite ↑(lightToProfinite.obj (S.component n)).toTop
this✝ : Nonempty ↑(lightToProfinite.obj (S.component 0)).toTop
this : ∀ (n : ℕ), Epi (S.transitionMap n)
k0 : Y ⟶ lightToProfinite.obj (S.diagram.obj (Opposite.op 0))
h_down0 : f ≫ k0 = g ≫ lightToProfinite.map (S.proj 0)
h_comm :
  ∀ (n : ℕ) (k : Y ⟶ lightToProfinite.obj (S.component n)),
    f ≫ k = g ≫ lightToProfinite.map (S.proj n) →
      f ≫ k = g ≫ lightToProfinite.map (S.proj (n + 1)) ≫ lightToProfinite.map (S.transitionMap n)
h_step :
  ∀ (n : ℕ) (k : Y ⟶ lightToProfinite.obj (S.component n)),
    f ≫ k = g ≫ lightToProfinite.map (S.proj n) →
      ∃ k', k' ≫ lightToProfinite.map (S.transitionMap n) = k ∧ f ≫ k' = g ≫ lightToProfinite.map (S.proj (n + 1))
lifts : ℕ → Type (max 0 u) := fun n ↦ { k // f ≫ k = g ≫ lightToProfinite.map (S.proj n) }
next : (n : ℕ) → lifts n → lifts (n + 1) := fun n k ↦ ⟨⋯.choose, ⋯⟩
k_seq : (n : ℕ) → lifts n := fun n ↦ Nat.rec ⟨k0, h_down0⟩ next n
h_down : ∀ (n : ℕ), f ≫ ↑(k_seq n) = g ≫ lightToProfinite.map (S.proj n)
h_up : ∀ (n : ℕ), ↑(k_seq (n + 1)) ≫ lightToProfinite.map (S.transitionMap n) = ↑(k_seq n)
k_cone : Cone (S.diagram ⋙ lightToProfinite) := { pt := Y, π := NatTrans.ofOpSequence (fun n ↦ ↑(k_seq n)) ⋯ }
n : ℕᵒᵖ
⊢ g ≫ (lightToProfinite.mapCone S.asLimitCone).π.app n = (k_cone.extend f).π.app n

Tactic:
simp [show k_cone.π.app n = (k_seq n.unop).1 from rfl, h_down]

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

Goal state before:
pp: F : Type u → Type u
inst✝¹ : Applicative F
α' β' : Type u
f : α' → F β'
inst✝ : LawfulApplicative F
a : α'
as bs : List α'
⊢ traverse f (a :: as ++ bs) = (fun x1 x2 ↦ x1 ++ x2) <$> traverse f (a :: as) <*> traverse f bs

Tactic:
simp [traverse_append as bs, functor_norm]; congr

Goal state after:
Module: Mathlib.Control.Fold

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

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

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

Goal state before:
pp: n : ℕ
α β : TypeVec.{u} n
F : TypeVec.{u} n → Type v
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
P : F α → Prop
q : F β → Prop
f : α ⟹ β
g : β ⟹ α
h₀ : f ⊚ g = TypeVec.id
h₁ : ∀ (u : F α), P u ↔ q (f <$$> u)
⊢ (∃ u, P u) ↔ ∃ u, q u

Tactic:
constructor <;> rintro ⟨u, h₂⟩

Goal state after:
case mp
n : ℕ
α β : TypeVec.{u} n
F : TypeVec.{u} n → Type v
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
P : F α → Prop
q : F β → Prop
f : α ⟹ β
g : β ⟹ α
h₀ : f ⊚ g = TypeVec.id
h₁ : ∀ (u : F α), P u ↔ q (f <$$> u)
u : F α
h₂ : P u
⊢ ∃ u, q u

case mpr
n : ℕ
α β : TypeVec.{u} n
F : TypeVec.{u} n → Type v
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
P : F α → Prop
q : F β → Prop
f : α ⟹ β
g : β ⟹ α
h₀ : f ⊚ g = TypeVec.id
h₁ : ∀ (u : F α), P u ↔ q (f <$$> u)
u : F β
h₂ : q u
⊢ ∃ u, P u
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n✝ n : ℕ
β : (v : TypeVec.{?u.30} (n + 1)) → (v' : TypeVec.{?u.32} (n + 1)) → v ⟹ v' → Sort u_1
F :
  (t : Type ?u.30) →
    (t' : Type ?u.32) →
      (f : t → t') →
        (v : TypeVec.{?u.30} n) → (v' : TypeVec.{?u.32} n) → (fs : v ⟹ v') → β (v ::: t) (v' ::: t') (fs ::: f)
v : TypeVec.{?u.30} (n + 1)
v' : TypeVec.{?u.32} (n + 1)
⊢ (fs : v.drop ::: v.last ⟹ v'.drop ::: v'.last) → β (v.drop ::: v.last) (v'.drop ::: v'.last) fs

Tactic:
intro fs

Goal state after:
n✝ n : ℕ
β : (v : TypeVec.{?u.30} (n + 1)) → (v' : TypeVec.{?u.32} (n + 1)) → v ⟹ v' → Sort u_1
F :
  (t : Type ?u.30) →
    (t' : Type ?u.32) →
      (f : t → t') →
        (v : TypeVec.{?u.30} n) → (v' : TypeVec.{?u.32} n) → (fs : v ⟹ v') → β (v ::: t) (v' ::: t') (fs ::: f)
v : TypeVec.{?u.30} (n + 1)
v' : TypeVec.{?u.32} (n + 1)
fs : v.drop ::: v.last ⟹ v'.drop ::: v'.last
⊢ β (v.drop ::: v.last) (v'.drop ::: v'.last) fs
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n✝ n : ℕ
t : Type u_1
t' : Type u_2
v : TypeVec.{u_1} n
v' : TypeVec.{u_2} n
β : v ::: t ⟹ v' ::: t' → Sort u_3
F : (f : t → t') → (fs : v ⟹ v') → β (fs ::: f)
⊢ (fs : v ::: t ⟹ v' ::: t') → β fs

Tactic:
intro fs

Goal state after:
n✝ n : ℕ
t : Type u_1
t' : Type u_2
v : TypeVec.{u_1} n
v' : TypeVec.{u_2} n
β : v ::: t ⟹ v' ::: t' → Sort u_3
F : (f : t → t') → (fs : v ⟹ v') → β (fs ::: f)
fs : v ::: t ⟹ v' ::: t'
⊢ β fs
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: S : Type u_1
T : Type u_2
X : Type u_3
π : T → S × Option X
hπ : Function.Surjective π
σ : Option X → S → T
hσ : ∀ (x : Option X) (s : S), (π (σ x s)).1 = s
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
⊢ Function.Surjective fun x ↦ π ↑x

Tactic:
rintro ⟨s, (rfl | x)⟩
  · obtain ⟨y, hy⟩ := hπ (s, none)
    exact ⟨⟨y, by grind⟩, hy⟩
  · exact ⟨⟨σ x s, by simp⟩, Prod.ext (by grind) (by grind)⟩

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

Goal state before:
pp: R : Type
inst✝ : CommRing R
X Y : LightCondMod R
p : X ⟶ Y
hp : Epi p
S : LightProfinite
f : (free R).obj (S ⊗ ℕ∪{∞}).toCondensed ⟶ Y
T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
g : (free R).obj T.toCondensed ⟶ X
hπ : Epi π
comm : (lightProfiniteToLightCondSet ⋙ free R).map π ≫ f = g ≫ p
S' T' : LightProfinite
y' : S' ⟶ S
π' : T' ⟶ S' ⊗ ℕ∪{∞}
g' : T' ⟶ T
hπ' : Epi π'
hy' : Epi y'
comp : π' ≫ y' ▷ ℕ∪{∞} = g' ≫ π
epi : Epi (cover π')
split : SplitEpi (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π' ≫ fst S' ℕ∪{∞})
⊢ ∃ S' π,
    ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
      ∃ g', (free R).map (lightProfiniteToLightCondSet.map (π ▷ ℕ∪{∞})) ≫ f = g' ≫ p

Tactic:
refine ⟨S', y', (LightProfinite.epi_iff_surjective _).mp inferInstance, ?_⟩

Goal state after:
R : Type
inst✝ : CommRing R
X Y : LightCondMod R
p : X ⟶ Y
hp : Epi p
S : LightProfinite
f : (free R).obj (S ⊗ ℕ∪{∞}).toCondensed ⟶ Y
T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
g : (free R).obj T.toCondensed ⟶ X
hπ : Epi π
comm : (lightProfiniteToLightCondSet ⋙ free R).map π ≫ f = g ≫ p
S' T' : LightProfinite
y' : S' ⟶ S
π' : T' ⟶ S' ⊗ ℕ∪{∞}
g' : T' ⟶ T
hπ' : Epi π'
hy' : Epi y'
comp : π' ≫ y' ▷ ℕ∪{∞} = g' ≫ π
epi : Epi (cover π')
split : SplitEpi (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π' ≫ fst S' ℕ∪{∞})
⊢ ∃ g', (free R).map (lightProfiniteToLightCondSet.map (y' ▷ ℕ∪{∞})) ≫ f = g' ≫ p
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : IsEmpty α
e : FinEnum α
⊢ e = { card := 0, equiv := Equiv.equivOfIsEmpty α (Fin 0), decEq := fun a b ↦ decidableEq_of_subsingleton a b }

Tactic:
change FinEnum.mk e.1 e.2 = _
    congr 1
    · exact card_eq_zero
    · refine heq_of_cast_eq ?_ (Subsingleton.allEq _ _)
      exact congrArg (α ≃ Fin ·) <| card_eq_zero
    · funext x
      exact ‹IsEmpty α›.elim x

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

Goal state before:
pp: α : Type u_1
f : α → Option α
h : ∀ (a b : α), b ∈ f a → a = b
l : List α
⊢ lookmap f l = l

Tactic:
by
  rw [← map_id (l.lookmap f), lookmap_map_eq, map_id]; exact h

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

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

Tactic:
simp [← dlookup_isSome, Option.isNone_iff_eq_none]

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
γ : Sort ?u.13
s : Finmap β
f : AList β → γ
H : ∀ (a b : AList β), a.entries ~ b.entries → f a = f b
⊢ γ

Tactic:
refine
    (Quotient.liftOn s.entries
      (fun (l : List (Sigma β)) => (⟨_, fun nd => f ⟨l, nd⟩⟩ : Part γ))
      (fun l₁ l₂ p => Part.ext' (perm_nodupKeys p) ?_) : Part γ).get ?_

Goal state after:
case refine_1
α : Type u
β : α → Type v
γ : Type ?u.32
s : Finmap β
f : AList β → γ
H : ∀ (a b : AList β), a.entries ~ b.entries → f a = f b
l₁ l₂ : List (Sigma β)
p : l₁ ≈ l₂
⊢ ∀ (h₁ : { Dom := l₁.NodupKeys, get := fun nd ↦ f { entries := l₁, nodupKeys := nd } }.Dom)
    (h₂ : { Dom := l₂.NodupKeys, get := fun nd ↦ f { entries := l₂, nodupKeys := nd } }.Dom),
    { Dom := l₁.NodupKeys, get := fun nd ↦ f { entries := l₁, nodupKeys := nd } }.get h₁ =
      { Dom := l₂.NodupKeys, get := fun nd ↦ f { entries := l₂, nodupKeys := nd } }.get h₂

case refine_2
α : Type u
β : α → Type v
γ : Type ?u.32
s : Finmap β
f : AList β → γ
H : ∀ (a b : AList β), a.entries ~ b.entries → f a = f b
⊢ (Quotient.liftOn s.entries (fun l ↦ { Dom := l.NodupKeys, get := fun nd ↦ f { entries := l, nodupKeys := nd } })
      ⋯).Dom
Module: Mathlib.Data.Finmap

Goal state before:
pp: case mk
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
entries✝ : Multiset (Sigma β)
l : List (Sigma β)
hl : Multiset.NodupKeys (Quot.mk (⇑(isSetoid (Sigma β))) l)
⊢ b ∈ lookup a { entries := Quot.mk (⇑(isSetoid (Sigma β))) l, nodupKeys := hl } ↔
    ⟨a, b⟩ ∈ { entries := Quot.mk (⇑(isSetoid (Sigma β))) l, nodupKeys := hl }.entries

Tactic:
exact List.mem_dlookup_iff hl

Goal state after:
Module: Mathlib.Data.Finset.Functor

Goal state before:
pp: α β γ : Type u
G : Type u → Type u
inst✝¹ : Applicative G
inst✝ : CommApplicative G
g : α → G β
h : β → γ
s : Finset α
⊢ Functor.map h <$> traverse g s = traverse (Functor.map h ∘ g) s

Tactic:
by
  unfold traverse
  simp only [Functor.map_map, fmap_def, map_comp_coe_apply, Multiset.fmap_def, ←
    Multiset.map_traverse]

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

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
a : α
h : ¬f a = 0
this : lookup a f.toAList = some (f a)
⊢ f.toAList.lookupFinsupp a = f a

Tactic:
by simp [this]

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

Goal state before:
pp: a b n : ℕ
a_le_n : a ≤ n
b_le_n : b ≤ n
⊢ ↑(↑a - ↑b).natAbs ≤ ↑n

Tactic:
natCast_natAbs

Goal state after:
a b n : ℕ
a_le_n : a ≤ n
b_le_n : b ≤ n
⊢ |↑a - ↑b| ≤ ↑n
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:
natCast_natAbs

Goal state after:
a b n : ℕ
a_lt_n : a < n
b_lt_n : b < n
⊢ |↑a - ↑b| < ↑n
Module: Mathlib.Data.List.DropRight

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

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_length_add_append]

Goal state after:
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
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
l : List α
n : ℕ
⊢ l.rtake n = (take n l.reverse).reverse

Tactic:
rw [rtake]
  induction l using List.reverseRecOn generalizing n with
  | nil => simp
  | append_singleton xs x IH =>
    cases n
    · exact drop_length
    · simp [drop_append, IH]

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α → Option β → γ
a : α
as : List α
b : β
bs : List β
h : (a :: as).length ≤ (b :: bs).length
⊢ map₂Left f (a :: as) (b :: bs) = zipWith (fun a b ↦ f a (some b)) (a :: as) (b :: bs)

Tactic:
simp only [length_cons, succ_le_succ_iff] at h

Goal state after:
α : Type u
β : Type v
γ : Type w
f : α → Option β → γ
a : α
as : List α
b : β
bs : List β
h : as.length ≤ bs.length
⊢ map₂Left f (a :: as) (b :: bs) = zipWith (fun a b ↦ f a (some b)) (a :: as) (b :: bs)
Module: Mathlib.Data.List.Lemmas

Goal state before:
pp: α : Type u_1
l : List α
x : α
hx : ¬x ∈ l
n : ℕ
⊢ n ∈ {n | n ≤ l.length} →
    ∀ ⦃x₂ : ℕ⦄, x₂ ∈ {n | n ≤ l.length} → (fun k ↦ l.insertIdx k x) n = (fun k ↦ l.insertIdx k x) x₂ → n = x₂

Tactic:
hn

Goal state after:
α : Type u_1
l : List α
x : α
hx : ¬x ∈ l
n : ℕ
hn : n ∈ {n | n ≤ l.length}
⊢ ∀ ⦃x₂ : ℕ⦄, x₂ ∈ {n | n ≤ l.length} → (fun k ↦ l.insertIdx k x) n = (fun k ↦ l.insertIdx k x) x₂ → n = x₂
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
⊢ w.HasPeriod (p.gcd q)

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

Goal state after:
case inr.inr.gt
α : Type u_1
w : List α
p q : ℕ
per_p : w.HasPeriod p
per_q : w.HasPeriod q
len : p + q - p.gcd q ≤ w.length
p_pos : p > 0
q_pos : q > 0
hyp : compare p q = Ordering.gt
q_lt_p : q < p
gcd_lt_p : p.gcd q < p
per_diff : (drop q w).HasPeriod (p - q)
per_q' : (drop q w).HasPeriod q
gcd_stable : (p - q).gcd q = p.gcd q
drop_len : q ≤ (drop q w).length
take_eq : take q (drop q w) = take q w
⊢ w.HasPeriod (p.gcd q)
Module: Mathlib.Data.Multiset.DershowitzManna

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

Tactic:
· exact ⟨z, .inr <| by rwa [mem_sub, count_eq_zero_of_notMem z_in, count_pos], hyz⟩

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

Goal state before:
pp: p : ℕ → Prop
hf : (Set.ofPred p).Finite
n : ℕ
hn : #hf.toFinset ≤ n
⊢ nth p n = 0

Tactic:
rw [nth, dif_pos hf, List.getD_eq_default]; rwa [Finset.length_sort]

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

Goal state before:
pp: p : ℕ → Prop
hf : (Set.ofPred p).Finite
⊢ nth p '' Set.Iio #hf.toFinset = Set.range ⇑(hf.toFinset.orderEmbOfFin ⋯)

Tactic:
ext x
      simp only [Set.mem_image, Set.mem_range, Fin.exists_iff, ← nth_eq_orderEmbOfFin hf,
        Set.mem_Iio, exists_prop]

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

Goal state before:
pp: case inl
p : ℕ → Prop
k a : ℕ
h : a < nth p (k + 1)
ha : p a
hf : (Set.ofPred p).Finite
⊢ a ≤ nth p k

Tactic:
rcases exists_lt_card_finite_nth_eq hf ha with ⟨n, hn, rfl⟩
    rcases lt_or_ge (k + 1) #hf.toFinset with hk | hk
    · rwa [(nth_strictMonoOn hf).lt_iff_lt hn hk, Nat.lt_succ_iff,
        ← (nth_strictMonoOn hf).le_iff_le hn (k.lt_succ_self.trans hk)] at h
    · rw [nth_of_card_le _ hk] at h
      exact absurd h (zero_le _).not_gt

Goal state after:
Module: Mathlib.Data.Ordmap.Ordnode

Goal state before:
pp: case node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ Ordnode α

Tactic:
rcases id r with _ | ⟨rs, rl, rx, rr⟩
    · exact node (ls + 1) l x nil
    · refine if rs > delta * ls then ?_ else node (ls + rs + 1) l x r
      rcases id rr with _ | rrs
      · exact nil
      --should not happen
      rcases id rl with _ | ⟨rls, rll, rlx, rlr⟩
      · exact nil
      --should not happen
      exact
        if rls < ratio * rrs then node (ls + rs + 1) (node (ls + rls + 1) l x rl) rx rr
        else
          node (ls + rs + 1) (node (ls + size rll + 1) l x rll) rlx
            (node (size rlr + rrs + 1) rlr rx rr)

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

Goal state before:
pp: n : ZNum
⊢ -n.pred = (-n).succ

Tactic:
rw [← zneg_zneg (succ (-n)), zneg_succ, zneg_zneg]

Goal state after:
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
⊢ (l.node3L x m y r).dual = r.dual.node3R y m.dual x l.dual

Tactic:
by
  simp [node3L, node3R, add_comm]

Goal state after:
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
⊢ (l.node3R x m y r).dual = r.dual.node3L y m.dual x l.dual

Tactic:
by
  simp [node3L, node3R, add_comm]

Goal state after:
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: F : PFunctor.{uA, uB}
n m : ℕ
x : (n : ℕ) → CofixA F n
Hconsistent : AllAgree x
this : ∀ (n : ℕ), head' (x n.succ) = head' (x 1)
⊢ head' (x n.succ) = head' (x m.succ)

Tactic:
by simp [this]

Goal state after:
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
x✝ ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
x : α
r : Ordnode α
⊢ (match (ll.findMin' lx, (node ls ll lx lr).eraseMin) with
    | (xm, l') => (xm, l'.balanceR x r)) =
    (ll.findMin' lx, (node x✝ (node ls ll lx lr) x r).eraseMin)

Tactic:
eraseMin

Goal state after:
α : Type u_1
x✝ ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
x : α
r : Ordnode α
⊢ (match (ll.findMin' lx, (node ls ll lx lr).eraseMin) with
    | (xm, l') => (xm, l'.balanceR x r)) =
    (ll.findMin' lx, (node ls ll lx lr).eraseMin.balanceR x r)
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case neg
F : PFunctor.{uA, uB}
R : F.M → F.M → Prop
inst✝ : Nonempty F.M
bisim : IsBisimulation R
inhabited_h : Inhabited F.M
s₁ s₂ : F.M
Hr : R s₁ s₂
ps : Path F
h : ¬(IsPath ps s₁ ∨ IsPath ps s₂)
⊢ iselect ps s₁ = iselect ps s₂

Tactic:
not_or

Goal state after:
case neg
F : PFunctor.{uA, uB}
R : F.M → F.M → Prop
inst✝ : Nonempty F.M
bisim : IsBisimulation R
inhabited_h : Inhabited F.M
s₁ s₂ : F.M
Hr : R s₁ s₂
ps : Path F
h : ¬IsPath ps s₁ ∧ ¬IsPath ps s₂
⊢ iselect ps s₁ = iselect ps s₂
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
P : α → Prop
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
H : (∃ l', Raised l' l.size ∧ BalancedSz l' r.size) ∨ ∃ r', Raised r.size r' ∧ BalancedSz l.size r'
⊢ All P (l.balanceL x r) ↔ All P l ∧ P x ∧ All P r

Tactic:
by
  rw [balanceL_eq_balance' hl hr sl sr H, all_balance']

Goal state after: