mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Category.Profinite.CofilteredLimit

Goal state before:
pp: case refine_3.refine_2.mpr
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toTop
hC : IsLimit C
hU : IsClopen U
S : Set (Set ↑(toTopCat.mapCone C).pt)
hS : S ⊆ {U | ∃ j, ∃ V ∈ {W | IsClopen W}, U = ⇑(ConcreteCategory.hom ((toTopCat.mapCone C).π.app j)) ⁻¹' V}
h : U = ⋃₀ S
j : ↑S → J := fun s ↦ Exists.choose ⋯
V : (s : ↑S) → Set ↑(F.obj (j s)).toTop := fun s ↦ ⋯.choose
hV : ∀ (s : ↑S), IsClopen (V s) ∧ ↑s = ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s
hUo : ∀ (i : ↑S), IsOpen ((fun s ↦ ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s) i)
hsU : U ⊆ ⋃ i, (fun s ↦ ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s) i
G : Finset ↑S
hG : U ⊆ ⋃ i ∈ G, ⇑(ConcreteCategory.hom (C.π.app (j i))) ⁻¹' V i
j0 : J
hj0 : ∀ {X : J}, X ∈ Finset.image j G → Nonempty (j0 ⟶ X)
f : (s : ↑S) → s ∈ G → (j0 ⟶ j s) := fun s hs ↦ ⋯.some
W : ↑S → Set ↑(F.obj j0).toTop :=
  fun s ↦ if hs : s ∈ G then ⇑(ConcreteCategory.hom (F.map (f s hs))) ⁻¹' V s else Set.univ
x : ↑C.pt.toTop
s : ↑S
hs : s ∈ G
hx :
  x ∈
    ⇑(ConcreteCategory.hom (C.π.app j0)) ⁻¹'
      if h : s ∈ G then ⇑(ConcreteCategory.hom (F.map (f s ⋯))) ⁻¹' V s else Set.univ
⊢ x ∈ ↑s

Tactic:
rw [(hV s).2]

Goal state after:
case refine_3.refine_2.mpr
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toTop
hC : IsLimit C
hU : IsClopen U
S : Set (Set ↑(toTopCat.mapCone C).pt)
hS : S ⊆ {U | ∃ j, ∃ V ∈ {W | IsClopen W}, U = ⇑(ConcreteCategory.hom ((toTopCat.mapCone C).π.app j)) ⁻¹' V}
h : U = ⋃₀ S
j : ↑S → J := fun s ↦ Exists.choose ⋯
V : (s : ↑S) → Set ↑(F.obj (j s)).toTop := fun s ↦ ⋯.choose
hV : ∀ (s : ↑S), IsClopen (V s) ∧ ↑s = ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s
hUo : ∀ (i : ↑S), IsOpen ((fun s ↦ ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s) i)
hsU : U ⊆ ⋃ i, (fun s ↦ ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s) i
G : Finset ↑S
hG : U ⊆ ⋃ i ∈ G, ⇑(ConcreteCategory.hom (C.π.app (j i))) ⁻¹' V i
j0 : J
hj0 : ∀ {X : J}, X ∈ Finset.image j G → Nonempty (j0 ⟶ X)
f : (s : ↑S) → s ∈ G → (j0 ⟶ j s) := fun s hs ↦ ⋯.some
W : ↑S → Set ↑(F.obj j0).toTop :=
  fun s ↦ if hs : s ∈ G then ⇑(ConcreteCategory.hom (F.map (f s hs))) ⁻¹' V s else Set.univ
x : ↑C.pt.toTop
s : ↑S
hs : s ∈ G
hx :
  x ∈
    ⇑(ConcreteCategory.hom (C.π.app j0)) ⁻¹'
      if h : s ∈ G then ⇑(ConcreteCategory.hom (F.map (f s ⋯))) ⁻¹' V s else Set.univ
⊢ x ∈ ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: f g : Code
k : Cont'
⊢ trStmts₁ (trNormal g (Cont'.comp f k)) ∪
      (codeSupp' g (Cont'.comp f k) ∪ (trStmts₁ (trNormal f k) ∪ (codeSupp' f k ∪ contSupp k))) =
    trStmts₁ (trNormal g (Cont'.comp f k)) ∪ (codeSupp' g (Cont'.comp f k) ∪ (codeSupp' f k ∪ contSupp k))

Tactic:
← Finset.union_assoc _ _ (contSupp k),

Goal state after:
f g : Code
k : Cont'
⊢ trStmts₁ (trNormal g (Cont'.comp f k)) ∪
      (codeSupp' g (Cont'.comp f k) ∪ (trStmts₁ (trNormal f k) ∪ codeSupp' f k ∪ contSupp k)) =
    trStmts₁ (trNormal g (Cont'.comp f k)) ∪ (codeSupp' g (Cont'.comp f k) ∪ (codeSupp' f k ∪ contSupp k))
Module: Mathlib.Topology.FiberPartition

Goal state before:
pp: S : Type u_1
Y : Type u_2
f : S → Y
inst✝ : TopologicalSpace S
⊢ Injective ⇑(sigmaIsoHom f)

Tactic:
by
  rintro ⟨⟨_, _, rfl⟩, ⟨_, hx⟩⟩ ⟨⟨_, _, rfl⟩, ⟨_, hy⟩⟩ h
  refine Sigma.subtype_ext ?_ h
  simp only [sigmaIsoHom_apply] at h
  rw [Set.mem_preimage, Set.mem_singleton_iff] at hx hy
  simp [← hx, ← hy, h]

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

Goal state before:
pp: case zero'
S : Finset Λ'
k : Cont'
Hk : codeSupp Code.zero' k ⊆ S
⊢ contSupp k ⊆ S

Tactic:
| zero' =>

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

Goal state before:
pp: case halt
S : Finset Λ'
H : contSupp Cont'.halt ⊆ S
⊢ Supports (contSupp Cont'.halt) S

Tactic:
simp [contSupp_halt, Supports]

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

Goal state before:
pp: P : TopCat → Prop
inst✝⁴ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
inst✝³ : HasProp P PUnit.{u + 1}
inst✝² : HasExplicitFiniteCoproducts P
inst✝¹ : HasExplicitPullbacks P
hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Surjective ⇑(ConcreteCategory.hom f)
inst✝ : HasExplicitFiniteCoproducts P
X : Type (max u w)
⊢ functorToPresheaves.map ((unit P hs).app X) ≫ ((counit P hs).app ((functor P hs).obj X)).hom =
    𝟙 (functorToPresheaves.obj X)

Tactic:
by
  ext ⟨S⟩ (f : LocallyConstant _ X)
  simp only [Functor.id_obj, functor_obj_obj_obj, functorToPresheaves_obj_obj, Functor.comp_obj,
    Functor.flip_obj_obj, ObjectProperty.ι_obj, unit_app, NatTrans.comp_app,
    functorToPresheaves_map_app, ConcreteCategory.hom_ofHom, TypeCat.Fun.toFun_apply,
    CategoryTheory.comp_apply, TypeCat.Fun.coe_mk, NatTrans.id_app, id_apply]
  simp only [counit]
  have := CompHausLike.preregular hs
  apply presheaf_ext
    (X := ((functor P hs).obj X).obj) (Y := ((functor.{u, w} P hs).obj X).obj)
      (f.map ((unit P hs).app X))
  intro a
  erw [incl_of_counitAppApp]
  simp only [functor_obj_obj_obj, Functor.id_obj, Functor.comp_obj, Functor.flip_obj_obj,
    ObjectProperty.ι_obj, unit_app, counitAppAppImage, functor_obj_obj_map,
    Quiver.Hom.unop_op, ConcreteCategory.hom_ofHom]
  ext x
  erw [← map_eq_image _ a x]
  rfl

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

Goal state before:
pp: case refine_2
F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
X : Type u
hc : IsLimit c
inst✝ : ∀ (i : ℕᵒᵖ), Epi (c.π.app i)
i j : ℕᵒᵖ
fi : LocallyConstant (↑((F ⋙ toLightProfinite).obj (Opposite.unop (Opposite.op i))).toTop) X
fj : LocallyConstant (↑((F ⋙ toLightProfinite).obj (Opposite.unop (Opposite.op j))).toTop) X
h :
  LocallyConstant.comap (TopCat.Hom.hom (c.π.app i).hom) fi = LocallyConstant.comap (TopCat.Hom.hom (c.π.app j).hom) fj
k : ℕᵒᵖ
ki : k ⟶ i
kj : k ⟶ j
h✝ : True
x : ↑(toLightProfinite.obj (F.obj k)).toTop
⊢ ({ toFun := fun g ↦ LocallyConstant.comap (TopCat.Hom.hom (toLightProfinite.map (F.map ki)).hom) g } fi) x =
    ({ toFun := fun g ↦ LocallyConstant.comap (TopCat.Hom.hom (toLightProfinite.map (F.map kj)).hom) g } fj) x

Tactic:
obtain ⟨x, hx⟩ := ((LightProfinite.epi_iff_surjective (c.π.app k)).mp inferInstance) x

Goal state after:
case refine_2
F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
X : Type u
hc : IsLimit c
inst✝ : ∀ (i : ℕᵒᵖ), Epi (c.π.app i)
i j : ℕᵒᵖ
fi : LocallyConstant (↑((F ⋙ toLightProfinite).obj (Opposite.unop (Opposite.op i))).toTop) X
fj : LocallyConstant (↑((F ⋙ toLightProfinite).obj (Opposite.unop (Opposite.op j))).toTop) X
h :
  LocallyConstant.comap (TopCat.Hom.hom (c.π.app i).hom) fi = LocallyConstant.comap (TopCat.Hom.hom (c.π.app j).hom) fj
k : ℕᵒᵖ
ki : k ⟶ i
kj : k ⟶ j
h✝ : True
x✝ : ↑(toLightProfinite.obj (F.obj k)).toTop
x : ↑(((const ℕᵒᵖ).obj c.pt).obj k).toTop
hx : (ConcreteCategory.hom (c.π.app k)) x = x✝
⊢ ({ toFun := fun g ↦ LocallyConstant.comap (TopCat.Hom.hom (toLightProfinite.map (F.map ki)).hom) g } fi) x✝ =
    ({ toFun := fun g ↦ LocallyConstant.comap (TopCat.Hom.hom (toLightProfinite.map (F.map kj)).hom) g } fj) x✝
Module: Mathlib.Topology.Category.LightProfinite.Injective

Goal state before:
pp: S : LightProfinite
inst✝ : Nonempty ↑S.toTop
X Y : LightProfinite
g : X ⟶ S
f : X ⟶ Y
x✝ : Mono f
⊢ ∃ h, f ≫ h = g

Tactic:
by
    obtain ⟨h, _⟩ := Injective.factors (lightToProfinite.map g) (lightToProfinite.map f)
    refine ⟨lightToProfiniteFullyFaithful.preimage h, ?_⟩
    apply lightToProfiniteFullyFaithful.map_injective
    cat_disch

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: case fs
n : ℕ
α : TypeVec.{u_1} (n + 1)
β : TypeVec.{u_2} (n + 1)
f g : α ⟹ β
h₀ : dropFun f = dropFun g
h₁ : lastFun f = lastFun g
a✝ : Fin2 n
⊢ f a✝.fs = g a✝.fs

Tactic:
apply congr_fun h₀

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
β : (v : TypeVec.{?u.4} 0) → (v' : TypeVec.{?u.7} 0) → v ⟹ v' → Sort u_1
f : β Fin2.elim0 Fin2.elim0 nilFun
v : TypeVec.{?u.4} 0
v' : TypeVec.{?u.7} 0
fs : v ⟹ v'
eq₁ : v = Fin2.elim0
eq₂ : v' = Fin2.elim0
eq₃ : fs = nilFun
⊢ β Fin2.elim0 Fin2.elim0 nilFun = β v v' fs

Tactic:
cases eq₁

Goal state after:
case refl
n : ℕ
β : (v : TypeVec.{?u.4} 0) → (v' : TypeVec.{?u.7} 0) → v ⟹ v' → Sort u_1
f : β Fin2.elim0 Fin2.elim0 nilFun
v' : TypeVec.{?u.7} 0
eq₂ : v' = Fin2.elim0
fs : Fin2.elim0 ⟹ v'
eq₃ : fs = nilFun
⊢ β Fin2.elim0 Fin2.elim0 nilFun = β Fin2.elim0 v' fs
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: m : Type u → Type v
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
⊢ ∀ {α ω γ : Type u} (cmd : OptionT m α) (next : Label ω (OptionT m) γ → α → OptionT m ω),
    (callCC fun f ↦ cmd >>= next f) = do
      let x ← cmd
      callCC fun f ↦ next f x

Tactic:
refine fun _ _ => OptionT.ext ?_

Goal state after:
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ ω✝ γ✝ : Type u
x✝¹ : OptionT m α✝
x✝ : Label ω✝ (OptionT m) γ✝ → α✝ → OptionT m ω✝
⊢ (callCC fun f ↦ x✝¹ >>= x✝ f).run =
    (do
        let x ← x✝¹
        callCC fun f ↦ x✝ f x).run
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
α : TypeVec.{u_1} n
r : α ⊗ α ⟹ «repeat» n Prop
⊢ subtypeVal r ⊚ toSubtype' r = fun i x ↦ prod.mk i (↑x).1 (↑x).2

Tactic:
ext i x
  induction i <;> simp only [toSubtype', comp, subtypeVal, prod.mk] at *
  simp [*]

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:
| cons x xs ih =>

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
⊢ b ∈ dlookup a l → ⟨a, b⟩ ∈ l

Tactic:
induction l with
  | nil => grind
  | cons s _ _ => by_cases a = s.fst <;> grind

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
s : Finmap β
x : (i : α) × β i
this : x ∈ s.entries → x.fst ∈ s.keys
⊢ (x ∈ s.keys.sigma fun i ↦ (lookup i s).toFinset) ↔ x ∈ { val := s.entries, nodup := ⋯ }

Tactic:
simpa [lookup_eq_some_iff]

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys
this : (map (Sigma.fst ∘ Sigma.mk a) (lookupAll a l)).Nodup
⊢ (replicate (lookupAll a l).length ?m.42).Nodup

pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys
this : (map (Sigma.fst ∘ Sigma.mk a) (lookupAll a l)).Nodup
⊢ Type ?u.49

pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys
this : (map (Sigma.fst ∘ Sigma.mk a) (lookupAll a l)).Nodup
⊢ ?m.40

Tactic:
← map_const

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys
this : (map (Sigma.fst ∘ Sigma.mk a) (lookupAll a l)).Nodup
⊢ (map (Function.const (β a) ?m.47) (lookupAll a l)).Nodup

α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys
this : (map (Sigma.fst ∘ Sigma.mk a) (lookupAll a l)).Nodup
⊢ Type ?u.50

α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys
this : (map (Sigma.fst ∘ Sigma.mk a) (lookupAll a l)).Nodup
⊢ ?m.45
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case refine_1
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : l.NodupKeys
h : ⟨a, b⟩ ∈ l
⊢ ∀ (a_1 : Sigma β),
    a_1 ∈ l → (if a = a_1.fst then some ⟨a, b⟩ else none) = Option.guard (fun s ↦ decide (a = s.fst)) a_1

pp: case refine_2
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : l.NodupKeys
h : ⟨a, b⟩ ∈ l
⊢ ∀ (a_1 b : Sigma β), b ∈ Option.guard (fun s ↦ decide (a = s.fst)) a_1 → a_1 = b

Tactic:
· rintro ⟨a', b'⟩ h'
    dsimp [Option.guard]
    split_ifs
    · subst a'
      simp [nd.eq_of_mk_mem h h']
    · simp_all
    · simp_all
    · rfl

Goal state after:
case refine_2
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : l.NodupKeys
h : ⟨a, b⟩ ∈ l
⊢ ∀ (a_1 b : Sigma β), b ∈ Option.guard (fun s ↦ decide (a = s.fst)) a_1 → a_1 = b
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l_hd : Sigma β
tail✝ : List (Sigma β)
l_ih : dlookup a tail✝.dedupKeys = dlookup a tail✝
⊢ dlookup a (l_hd :: tail✝).dedupKeys = dlookup a (l_hd :: tail✝)

Tactic:
obtain ⟨a', b⟩ := l_hd
    by_cases h : a = a'
    · subst a'
      rw [dedupKeys_cons, dlookup_kinsert, dlookup_cons_eq]
    · rw [dedupKeys_cons, dlookup_kinsert_ne h, l_ih, dlookup_cons_ne]
      exact h

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

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

Tactic:
by
  simp only [sub_eq_add_neg, neLocus_add_left, neLocus_neg_neg]

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

Goal state before:
pp: α : Type u₁
β : Type u₂
γ : Type u₃
inst✝¹ : Zero γ
inst✝ : SMulZeroClass β γ
f : α → β
g : α →₀ γ
⊢ (Function.support fun x ↦ f x • g x) ⊆ Function.support ⇑g

Tactic:
simp; grind [smul_zero]

Goal state after:
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: b : Bool
n : ℤ
⊢ (bit b n).bodd = b

Tactic:
bit_val

Goal state after:
b : Bool
n : ℤ
⊢ (2 * n + bif b then 1 else 0).bodd = b
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 ⋯)
h_cprankMax_sum :
  CPRankMax ((Finset.range d).card * ds.prod) (∑ i ∈ (Finset.range d).attach, unitVec d ↑i ⊗ x.slice ↑i ⋯)
⊢ CPRankMax (d :: ds).prod (∑ i ∈ (Finset.range d).attach, unitVec d ↑i ⊗ x.slice ↑i ⋯)

Tactic:
h_dds_prod

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).attach.card * ds.prod) (∑ i ∈ (Finset.range d).attach, unitVec d ↑i ⊗ x.slice ↑i ⋯)
h_cprankMax_sum :
  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.CardIntervalMod

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

Tactic:
neg_lt_sub_iff_lt_add,

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

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
head : α
tail : List α
hi : find? p tail = (dropWhile (fun x ↦ !p x) tail).head?
⊢ find? p (head :: tail) = (dropWhile (fun x ↦ !p x) (head :: tail)).head?

Tactic:
set ph := p head with phh
    rcases ph with rfl | rfl
    · have phh' : ¬(p head = true) := by simp [phh.symm]
      rw [find?_cons_of_neg phh', dropWhile_cons_of_pos]
      · exact hi
      · simpa using phh
    · rw [find?_cons_of_pos phh.symm, dropWhile_cons_of_neg]
      · simp
      · simpa using phh

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

Goal state before:
pp: case inr.inr.lt
α : 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.lt
⊢ w.HasPeriod (p.gcd q)

Tactic:
| lt =>

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

Goal state before:
pp: n k : ℕ
⊢ hyperoperation (n + 3) 1 k = 1

Tactic:
by
  induction n generalizing k with grind [cases Nat]

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

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
n : ZNum
⊢ ↑n + ↑1 = ↑n + 1

Tactic:
cast_one

Goal state after:
α : Type u_1
inst✝ : AddGroupWithOne α
n : ZNum
⊢ ↑n + 1 = ↑n + 1
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: a b : PosNum
⊢ Ordering.rec (↑b < ↑a) (b = a) (↑a < ↑b) (b.cmp a) → Ordering.rec (-↑a < -↑b) (neg a = neg b) (-↑b < -↑a) (b.cmp a)

Tactic:
cases PosNum.cmp b a

Goal state after:
case lt
a b : PosNum
⊢ Ordering.rec (↑b < ↑a) (b = a) (↑a < ↑b) Ordering.lt →
    Ordering.rec (-↑a < -↑b) (neg a = neg b) (-↑b < -↑a) Ordering.lt

case eq
a b : PosNum
⊢ Ordering.rec (↑b < ↑a) (b = a) (↑a < ↑b) Ordering.eq →
    Ordering.rec (-↑a < -↑b) (neg a = neg b) (-↑b < -↑a) Ordering.eq

case gt
a b : PosNum
⊢ Ordering.rec (↑b < ↑a) (b = a) (↑a < ↑b) Ordering.gt →
    Ordering.rec (-↑a < -↑b) (neg a = neg b) (-↑b < -↑a) Ordering.gt
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : PartialOrder α
inst✝ : IsStrictOrderedRing α
m n : ZNum
⊢ ↑↑m < ↑n ↔ m < n

Tactic:
← cast_to_int n,

Goal state after:
α : Type u_1
inst✝² : Ring α
inst✝¹ : PartialOrder α
inst✝ : IsStrictOrderedRing α
m n : ZNum
⊢ ↑↑m < ↑↑n ↔ m < n
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : PartialOrder α
inst✝ : IsStrictOrderedRing α
m n : ZNum
⊢ ↑↑m = ↑n ↔ m = n

Tactic:
← cast_to_int n,

Goal state after:
α : Type u_1
inst✝² : Ring α
inst✝¹ : PartialOrder α
inst✝ : IsStrictOrderedRing α
m n : ZNum
⊢ ↑↑m = ↑↑n ↔ m = n
Module: Mathlib.Data.PFunctor.Multivariate.Basic

Goal state before:
pp: case mpr
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : ↑P α
a : P.A
f₀ f₁ : P.B a ⟹ α
xeq : x = ⟨a, f₀⟩
yeq : y = ⟨a, f₁⟩
h : ∀ (i : Fin2 n) (j : P.B a i), r (f₀ i j) (f₁ i j)
⊢ LiftR r x y

Tactic:
exact ⟨⟨a, fun i j => ⟨(f₀ i j, f₁ i j), h i j⟩⟩, xeq.symm, yeq.symm⟩

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

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h₀ : Equivalence R
x y : P.M α
ax : P.A
fx fy : P.B ax ⟹ α ::: P.M α
h₁ : (TypeVec.id ::: Quot.mk R) ⊚ fx = (TypeVec.id ::: Quot.mk R) ⊚ fy
Hdrop : dropFun fx = dropFun fy
⊢ ⟨ax, fx⟩ = ⟨ax, fx⟩ ∧
    ⟨ax, fy⟩ = ⟨ax, splitFun (dropFun fy) (lastFun fy)⟩ ∧ ∀ (i : (P.B ax).last), R (lastFun fx i) (lastFun fy i)

Tactic:
split_dropFun_lastFun

Goal state after:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h₀ : Equivalence R
x y : P.M α
ax : P.A
fx fy : P.B ax ⟹ α ::: P.M α
h₁ : (TypeVec.id ::: Quot.mk R) ⊚ fx = (TypeVec.id ::: Quot.mk R) ⊚ fy
Hdrop : dropFun fx = dropFun fy
⊢ ⟨ax, fx⟩ = ⟨ax, fx⟩ ∧ ⟨ax, fy⟩ = ⟨ax, fy⟩ ∧ ∀ (i : (P.B ax).last), R (lastFun fx i) (lastFun fy i)
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: F : PFunctor.{uA, uB}
R : F.M → F.M → Prop
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
bisim : IsBisimulation R
ps : List F.Idx
ps_ih :
  ∀ (a : F.A) (f f' : F.B a → F.M),
    R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩) →
      IsPath ps (M.mk ⟨a, f⟩) ∨ IsPath ps (M.mk ⟨a, f'⟩) →
        iselect ps (M.mk ⟨a, f⟩) = iselect ps (M.mk ⟨a, f'⟩) ∧
          ∃ a_1 f_1 f'_1,
            isubtree ps (M.mk ⟨a, f⟩) = M.mk ⟨a_1, f_1⟩ ∧
              isubtree ps (M.mk ⟨a, f'⟩) = M.mk ⟨a_1, f'_1⟩ ∧ ∀ (i : F.B a_1), R (f_1 i) (f'_1 i)
a : F.A
f f' : F.B a → F.M
h₀ : R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩)
a' : F.A
i : F.B a'
hh : IsPath (⟨a', i⟩ :: ps) (M.mk ⟨a, f⟩) ∨ IsPath (⟨a', i⟩ :: ps) (M.mk ⟨a, f'⟩)
⊢ a = a'

Tactic:
by rcases hh with hh | hh <;> cases isPath_cons hh <;> rfl

Goal state after:
Module: Mathlib.Data.PFunctor.Multivariate.W

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
a : P.A
f : P.B a ⟹ α ::: P.W α
⊢ ⟨a, splitFun (dropFun f) (lastFun f)⟩ = ⟨a, f⟩

Tactic:
split_dropFun_lastFun

Goal state after:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
a : P.A
f : P.B a ⟹ α ::: P.W α
⊢ ⟨a, f⟩ = ⟨a, f⟩
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: n m : ℕ+
u : PrimeMultiset := n.factorMultiset
v : PrimeMultiset := m.factorMultiset
this✝ : n = u.prod
this : m = v.prod
⊢ (u + v).prod.factorMultiset = u.prod.factorMultiset + v.prod.factorMultiset

Tactic:
repeat' rw [PrimeMultiset.factorMultiset_prod]

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

Goal state before:
pp: n : ℕ+
m : ℕ
u : PrimeMultiset := n.factorMultiset
this : n = u.prod
⊢ (m • u).prod.factorMultiset = m • u.prod.factorMultiset

Tactic:
repeat' rw [PrimeMultiset.factorMultiset_prod]

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

Goal state before:
pp: case fst
u : XgcdType
⊢ u.v.1 = (succ₂ u.vp).1

Tactic:
dsimp [v, vp, w, z, a, b, succ₂]

Goal state after:
case fst
u : XgcdType
⊢ (u.wp + 1) * (u.ap + 1) + u.x * (u.bp + 1) = u.wp + u.x + u.ap + u.wp * u.ap + u.x * u.bp + 1
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: case snd
u : XgcdType
⊢ u.v.2 = (succ₂ u.vp).2

Tactic:
dsimp [v, vp, w, z, a, b, succ₂]

Goal state after:
case snd
u : XgcdType
⊢ u.y * (u.ap + 1) + (u.zp + 1) * (u.bp + 1) = u.y + u.zp + u.bp + u.y * u.ap + u.zp * u.bp + 1
Module: Mathlib.Data.PSigma.Order

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : LinearOrder ι
inst✝ : (i : ι) → LinearOrder (α i)
⊢ ∀ (a b : Σₗ' (i : ι), α i), a ≤ b ∨ b ≤ a

Tactic:
rintro ⟨i, a⟩ ⟨j, b⟩

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : LinearOrder ι
inst✝ : (i : ι) → LinearOrder (α i)
i : ι
a : α i
j : ι
b : α j
⊢ ⟨i, a⟩ ≤ ⟨j, b⟩ ∨ ⟨j, b⟩ ≤ ⟨i, a⟩
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: u : XgcdType
h : u.r ≠ 0
⊢ u.reduce = u.step.reduce.flip

Tactic:
rw [reduce]
  exact if_neg h

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

Goal state before:
pp: a b : ℕ+
⊢ let d := a.gcdD b;
  let w := a.gcdW b;
  let x := a.gcdX b;
  let y := a.gcdY b;
  let z := a.gcdZ b;
  let a' := a.gcdA' b;
  let b' := a.gcdB' b;
  w * z = (x * y).succPNat ∧
    a = a' * d ∧
      b = b' * d ∧
        z * a' = (x * ↑b').succPNat ∧ w * b' = (y * ↑a').succPNat ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d

Tactic:
by
  intro d w x y z a' b'
  let u := XgcdType.start a b
  let ur := u.reduce
  have hb : d = ur.b := u.reduce_isReduced'
  have ha' : (a' : ℕ) = w + x := gcdA'_coe a b
  have hb' : (b' : ℕ) = y + z := gcdB'_coe a b
  have hdet : w * z = succPNat (x * y) := u.reduce_isSpecial' rfl
  constructor
  · exact hdet
  have hdet' : (w * z : ℕ) = x * y + 1 := by rw [← mul_coe, hdet, succPNat_coe]
  let hv : Prod.mk (w * d + x * ur.b : ℕ) (y * d + z * ur.b : ℕ) = ⟨a, b⟩ :=
    u.reduce_v.trans (XgcdType.start_v a b)
  rw [← hb, ← add_mul, ← add_mul, ← ha', ← hb'] at hv
  have ha'' : (a : ℕ) = a' * d := (congr_arg Prod.fst hv).symm
  have hb'' : (b : ℕ) = b' * d := (congr_arg Prod.snd hv).symm
  constructor
  · exact eq ha''
  constructor
  · exact eq hb''
  have hza' : (z * a' : ℕ) = x * b' + 1 := by
    rw [ha', hb', mul_add, mul_add, mul_comm (z : ℕ), hdet']
    ring
  have hwb' : (w * b' : ℕ) = y * a' + 1 := by
    rw [ha', hb', mul_add, mul_add, hdet']
    ring
  constructor
  · apply eq
    rw [succPNat_coe, Nat.succ_eq_add_one, mul_coe, hza']
  constructor
  · apply eq
    rw [succPNat_coe, Nat.succ_eq_add_one, mul_coe, hwb']
  grind

Goal state after: