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

Goal state before:
pp: case nil.cons
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
s : Option Γ'
S : K' → List Γ'
a : Γ'
Sk : List Γ'
⊢ (bif p a then ([], some a, Sk) else (a :: (splitAtPred p Sk).1, (splitAtPred p Sk).2.1, (splitAtPred p Sk).2.2)) =
      ([], o, L₂) →
    ReflTransGen
      (fun a b ↦
        (match a with
          | { l := none, var := var, stk := stk } => none
          | { l := some l, var := v, stk := S } => some (TM2.stepAux (tr l) v S)) =
          some b)
      (bif p a then { l := some q, var := some a, stk := update S k Sk }
      else { l := some (Λ'.clear p k q), var := some a, stk := update S k Sk })
      { l := some q, var := o, stk := update S k L₂ }

Tactic:
cases p a

Goal state after:
case nil.cons.false
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
s : Option Γ'
S : K' → List Γ'
a : Γ'
Sk : List Γ'
⊢ (bif false then ([], some a, Sk) else (a :: (splitAtPred p Sk).1, (splitAtPred p Sk).2.1, (splitAtPred p Sk).2.2)) =
      ([], o, L₂) →
    ReflTransGen
      (fun a b ↦
        (match a with
          | { l := none, var := var, stk := stk } => none
          | { l := some l, var := v, stk := S } => some (TM2.stepAux (tr l) v S)) =
          some b)
      (bif false then { l := some q, var := some a, stk := update S k Sk }
      else { l := some (Λ'.clear p k q), var := some a, stk := update S k Sk })
      { l := some q, var := o, stk := update S k L₂ }

case nil.cons.true
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
s : Option Γ'
S : K' → List Γ'
a : Γ'
Sk : List Γ'
⊢ (bif true then ([], some a, Sk) else (a :: (splitAtPred p Sk).1, (splitAtPred p Sk).2.1, (splitAtPred p Sk).2.2)) =
      ([], o, L₂) →
    ReflTransGen
      (fun a b ↦
        (match a with
          | { l := none, var := var, stk := stk } => none
          | { l := some l, var := v, stk := S } => some (TM2.stepAux (tr l) v S)) =
          some b)
      (bif true then { l := some q, var := some a, stk := update S k Sk }
      else { l := some (Λ'.clear p k q), var := some a, stk := update S k Sk })
      { l := some q, var := o, stk := update S k L₂ }
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
U : Set ↑C.pt.toTop
hC : IsLimit C
hU : IsClopen U
⊢ ∃ j V, IsClopen V ∧ U = ⇑(ConcreteCategory.hom (C.π.app j)) ⁻¹' V

Tactic:
have hB := TopCat.isTopologicalBasis_cofiltered_limit.{u, v} (F ⋙ Profinite.toTopCat)
      (Profinite.toTopCat.mapCone C) (isLimitOfPreserves _ hC) (fun j => {W | IsClopen W}) ?_
      (fun i => isClopen_univ) (fun i U1 U2 hU1 hU2 => hU1.inter hU2) ?_

Goal state after:
case refine_3
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
hB :
  TopologicalSpace.IsTopologicalBasis
    {U | ∃ j, ∃ V ∈ {W | IsClopen W}, U = ⇑(ConcreteCategory.hom ((toTopCat.mapCone C).π.app j)) ⁻¹' V}
⊢ ∃ j V, IsClopen V ∧ U = ⇑(ConcreteCategory.hom (C.π.app j)) ⁻¹' V

case refine_1
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
⊢ ∀ (j : J), TopologicalSpace.IsTopologicalBasis {W | IsClopen W}

case refine_2
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
⊢ ∀ (i j : J) (f : i ⟶ j),
    ∀ V ∈ {W | IsClopen W}, ⇑(ConcreteCategory.hom ((F ⋙ toTopCat).map f)) ⁻¹' V ∈ {W | IsClopen W}
Module: Mathlib.Topology.Category.Profinite.CofilteredLimit

Goal state before:
pp: case refine_3.refine_2.mp
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
hx : x ∈ U
s : ↑S
hs : s ∈ G
hh : x ∈ (fun h ↦ ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s) hs
⊢ x ∈
    ⇑(ConcreteCategory.hom (C.π.app j0)) ⁻¹'
      if h : s ∈ G then ⇑(ConcreteCategory.hom (F.map (f s ⋯))) ⁻¹' V s else Set.univ

Tactic:
rwa [dif_pos hs, ← Set.preimage_comp, ← CompHausLike.coe_comp, C.w]

Goal state after:
Module: Mathlib.Topology.FiberPartition

Goal state before:
pp: S : Type u_1
Y : Type u_2
f : S → Y
inst✝¹ : TopologicalSpace S
l : LocallyConstant S Y
inst✝ : CompactSpace S
x : Fiber ⇑l
⊢ CompactSpace ↑↑x

Tactic:
obtain ⟨y, hy⟩ := x.prop

Goal state after:
S : Type u_1
Y : Type u_2
f : S → Y
inst✝¹ : TopologicalSpace S
l : LocallyConstant S Y
inst✝ : CompactSpace S
x : Fiber ⇑l
y : ↑(Set.range ⇑l)
hy : (fun x ↦ ⇑l ⁻¹' {↑x}) y = ↑x
⊢ CompactSpace ↑↑x
Module: Mathlib.Condensed.Discrete.Characterization

Goal state before:
pp: R : Type (u + 1)
inst✝ : Ring R
M : CondensedMod R
tfae_1_iff_2 : Condensed.IsDiscrete M ↔ IsIso ((Condensed.discreteUnderlyingAdj (ModuleCat R)).counit.app M)
tfae_1_iff_3 : Condensed.IsDiscrete M ↔ (Condensed.discrete (ModuleCat R)).essImage M
tfae_1_iff_4 : Condensed.IsDiscrete M ↔ (functor R).essImage M
tfae_1_iff_5 : Condensed.IsDiscrete M ↔ IsIso ((LocallyConstant.adjunction R).counit.app M)
tfae_1_iff_6 :
  Condensed.IsDiscrete M ↔
    Sheaf.IsConstant (coherentTopology Profinite)
      ((Condensed.ProfiniteCompHaus.equivalence (ModuleCat R)).inverse.obj M)
h : ∀ (S : Profinite), Nonempty (IsColimit ((profiniteToCompHaus.op ⋙ M.obj).mapCocone S.asLimitCone.op))
S : Profinite
⊢ Nonempty (IsColimit ((profiniteToCompHaus.op ⋙ ((Condensed.forget R).obj M).obj).mapCocone S.asLimitCone.op))

Tactic:
let : PreservesFilteredColimitsOfSize.{u, u} (forget (ModuleCat R)) :=
      preservesFilteredColimitsOfSize_shrink.{u, u + 1, u, u + 1} _

Goal state after:
R : Type (u + 1)
inst✝ : Ring R
M : CondensedMod R
tfae_1_iff_2 : Condensed.IsDiscrete M ↔ IsIso ((Condensed.discreteUnderlyingAdj (ModuleCat R)).counit.app M)
tfae_1_iff_3 : Condensed.IsDiscrete M ↔ (Condensed.discrete (ModuleCat R)).essImage M
tfae_1_iff_4 : Condensed.IsDiscrete M ↔ (functor R).essImage M
tfae_1_iff_5 : Condensed.IsDiscrete M ↔ IsIso ((LocallyConstant.adjunction R).counit.app M)
tfae_1_iff_6 :
  Condensed.IsDiscrete M ↔
    Sheaf.IsConstant (coherentTopology Profinite)
      ((Condensed.ProfiniteCompHaus.equivalence (ModuleCat R)).inverse.obj M)
h : ∀ (S : Profinite), Nonempty (IsColimit ((profiniteToCompHaus.op ⋙ M.obj).mapCocone S.asLimitCone.op))
S : Profinite
this : PreservesFilteredColimitsOfSize.{u, u, u + 1, u + 1, u + 2, u + 2} (forget (ModuleCat R)) :=
  preservesFilteredColimitsOfSize_shrink (forget (ModuleCat R))
⊢ Nonempty (IsColimit ((profiniteToCompHaus.op ⋙ ((Condensed.forget R).obj M).obj).mapCocone S.asLimitCone.op))
Module: Mathlib.Condensed.EffectiveEpi

Goal state before:
pp: X✝ Y✝ : CompHaus
f : X✝ ⟶ Y✝
hf : Epi f
⊢ Epi (compHausToCondensed.map f)

Tactic:
rw [CondensedSet.epi_iff_locallySurjective_on_compHaus]
    intro S g
    refine ⟨pullback f g.down, pullback.snd _ _, fun y ↦ ?_, ⟨pullback.fst _ _⟩,
      ULift.ext _ _ <| pullback.condition _ _⟩
    rw [CompHaus.epi_iff_surjective] at hf
    obtain ⟨x, hx⟩ := hf (g.down.hom y)
    exact ⟨⟨⟨x, y⟩, hx⟩, rfl⟩

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
F : ℕᵒᵖ ⥤ LightCondMod R
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Epi (F.map (homOfLE ⋯).op)
⊢ Epi (((forget R).mapCone c).π.app (Opposite.op 0))

Tactic:
apply coherentTopology.epi_π_app_zero_of_epi

Goal state after:
case h
R : Type u_1
inst✝ : Ring R
F : ℕᵒᵖ ⥤ LightCondMod R
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Epi (F.map (homOfLE ⋯).op)
⊢ ∀ (G : ℕᵒᵖ ⥤ LightProfinite),
    (∀ (n : ℕ), EffectiveEpi (G.map (homOfLE ⋯).op)) → EffectiveEpi (limit.π G (Opposite.op 0))

case hc
R : Type u_1
inst✝ : Ring R
F : ℕᵒᵖ ⥤ LightCondMod R
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Epi (F.map (homOfLE ⋯).op)
⊢ IsLimit ((forget R).mapCone c)

case hF
R : Type u_1
inst✝ : Ring R
F : ℕᵒᵖ ⥤ LightCondMod R
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Epi (F.map (homOfLE ⋯).op)
⊢ ∀ (n : ℕ), Epi ((F ⋙ forget R).map (homOfLE ⋯).op)
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)
i : S
z : Y
hz : z ∈ Z i
⊢ z ∈ D i

Tactic:
rw [mem_preimage, mem_singleton_iff]

Goal state after:
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)
i : S
z : Y
hz : z ∈ Z i
⊢ g' z = f' i
Module: Mathlib.Data.TypeVec

Goal state before:
pp: case fs
n : ℕ
p : Prop
n✝ : ℕ
a✝ : Fin2 n✝
ih : ∀ {α : TypeVec.{u_1} n✝} {x : α a✝}, ofRepeat (TypeVec.const p α a✝ x) ↔ p
α : TypeVec.{u_1} (n✝ + 1)
x : α a✝.fs
⊢ ofRepeat
      ((match (motive := (x : ℕ) → (x_1 : TypeVec.{u_1} x) → (x_2 : Fin2 x) → x_1 x_2 → «repeat» x Prop x_2) n✝.succ, α,
          a✝.fs with
        | n.succ, α, a.fs => TypeVec.const p α.drop a
        | n.succ, x, Fin2.fz => fun x ↦ p)
        x) ↔
    p

Tactic:
exact ih

Goal state after:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: case a
α : Type u_1
β : α → Type u_2
g : ((a : α) → Part (β a)) → (a : α) → Part (β a)
hc : ωScottContinuous g
⊢ ωSup (approxChain { toFun := g, monotone' := ⋯ }) ≤
    ωSup ((approxChain { toFun := g, monotone' := ⋯ }).map { toFun := g, monotone' := ⋯ })

Tactic:
apply ωSup_le_ωSup_of_le _

Goal state after:
α : Type u_1
β : α → Type u_2
g : ((a : α) → Part (β a)) → (a : α) → Part (β a)
hc : ωScottContinuous g
⊢ approxChain { toFun := g, monotone' := ⋯ } ≤
    (approxChain { toFun := g, monotone' := ⋯ }).map { toFun := g, monotone' := ⋯ }
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: case a
α : Type u_1
β : α → Type u_2
g : ((a : α) → Part (β a)) → (a : α) → Part (β a)
hc : ωScottContinuous g
⊢ ωSup ((approxChain { toFun := g, monotone' := ⋯ }).map { toFun := g, monotone' := ⋯ }) ≤
    ωSup (approxChain { toFun := g, monotone' := ⋯ })

Tactic:
apply ωSup_le_ωSup_of_le _

Goal state after:
α : Type u_1
β : α → Type u_2
g : ((a : α) → Part (β a)) → (a : α) → Part (β a)
hc : ωScottContinuous g
⊢ (approxChain { toFun := g, monotone' := ⋯ }).map { toFun := g, monotone' := ⋯ } ≤
    approxChain { toFun := g, monotone' := ⋯ }
Module: Mathlib.Data.BitVec

Goal state before:
pp: z : ℤ
w : ℕ
⊢ (z % 2 ^ (w + 1)).bmod (2 ^ (w + 1)) = z.bmod (2 ^ (w + 1))

pp: z : ℤ
w : ℕ
⊢ 0 ≤ z % 2 ^ (w + 1)

Tactic:
· have h : (2 ^ (w + 1) : Int) = (2 ^ (w + 1) : Nat) := by simp
      rw [h, Int.emod_bmod]

Goal state after:
z : ℤ
w : ℕ
⊢ 0 ≤ z % 2 ^ (w + 1)
Module: Mathlib.Data.Fin.Tuple.Take

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_2
v : (i : Fin (n + 1)) → α i
⊢ take 1 ⋯ v = fun i ↦ v (castLE ⋯ i)

Tactic:
by
  ext i
  simp only [take]

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
s₁ s₂ : AList β
⊢ ⟦s₁⟧ = ⟦s₂⟧ ↔ s₁.entries ~ s₂.entries

Tactic:
by
  cases s₁
  cases s₂
  simp [AList.toFinmap]

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

Goal state before:
pp: α : Type u
α' : Type u'
β : α → Type v
β' : α' → Type v'
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
l : List (Sigma β)
f : α → α'
hf : Function.Injective f
g : (a : α) → β a → β' (f a)
a : α
⊢ dlookup (f a) (map (Sigma.map f g) l) = Option.map (g a) (dlookup a l)

Tactic:
induction l with
  | nil => grind
  | cons s _ _ =>
    have (h : a ≠ s.fst) : ¬ f a = (⟨f s.fst, g s.fst s.snd⟩ : Sigma β').fst := fun he => h <| hf he
    by_cases a = s.fst <;> grind [Sigma.map]

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

Goal state before:
pp: case cons.mk.left
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l' : List (Sigma β)
this : l'.NodupKeys
xs : List (Sigma β)
l_ih : (foldr (fun x ↦ kinsert x.fst x.snd) l' xs).NodupKeys
fst✝ : α
snd✝ : β fst✝
⊢ ¬fst✝ ∈ (kerase fst✝ (foldr (fun x ↦ kinsert x.fst x.snd) l' xs)).keys

Tactic:
simp only [keys_kerase]
      apply l_ih.not_mem_erase

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

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x ↦ M
a : α
⊢ l.lookupFinsupp a = (lookup a l).getD 0

Tactic:
simp only [lookupFinsupp, ne_eq, Finsupp.coe_mk]

Goal state after:
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x ↦ M
a : α
⊢ (lookup a l).getD 0 = (lookup a l).getD 0
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:
by simp; grind [smul_zero]

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

Goal state before:
pp: a b : ℤ
hn : 0 ≤ b
⊢ ↑|a|.toNat ≤ ↑b.toNat.sqrt ↔ ↑|a|.toNat * ↑|a|.toNat ≤ ↑b.toNat

Tactic:
← Int.natCast_mul,

Goal state after:
a b : ℤ
hn : 0 ≤ b
⊢ ↑|a|.toNat ≤ ↑b.toNat.sqrt ↔ ↑(|a|.toNat * |a|.toNat) ≤ ↑b.toNat
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: a b r : ℤ
hr : 0 < r
⊢ ↑(#({x ∈ Ioc a b | r ∣ x})) = max (⌊↑b / ↑r⌋ - ⌊↑a / ↑r⌋) 0

Tactic:
by
  rw [Ioc_filter_dvd_eq _ _ hr, card_map, card_Ioc, toNat_eq_max]

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

Goal state before:
pp: case cons
α : Type u_1
x hd : α
tl : List α
IH :
  ¬x ∈ tl →
    ∀ ⦃n : ℕ⦄,
      n ∈ {n | n ≤ tl.length} →
        ∀ ⦃m : ℕ⦄, m ∈ {n | n ≤ tl.length} → (fun k ↦ tl.insertIdx k x) n = (fun k ↦ tl.insertIdx k x) m → n = m
hx : ¬x ∈ hd :: tl
n : ℕ
hn : n ≤ tl.length + 1
m : ℕ
hm : m ≤ tl.length + 1
h : (fun k ↦ (hd :: tl).insertIdx k x) n = (fun k ↦ (hd :: tl).insertIdx k x) m
⊢ n = m

Tactic:
simp only [mem_cons, not_or] at hx

Goal state after:
case cons
α : Type u_1
x hd : α
tl : List α
IH :
  ¬x ∈ tl →
    ∀ ⦃n : ℕ⦄,
      n ∈ {n | n ≤ tl.length} →
        ∀ ⦃m : ℕ⦄, m ∈ {n | n ≤ tl.length} → (fun k ↦ tl.insertIdx k x) n = (fun k ↦ tl.insertIdx k x) m → n = m
n : ℕ
hn : n ≤ tl.length + 1
m : ℕ
hm : m ≤ tl.length + 1
h : (fun k ↦ (hd :: tl).insertIdx k x) n = (fun k ↦ (hd :: tl).insertIdx k x) m
hx : ¬x = hd ∧ ¬x ∈ tl
⊢ n = m
Module: Mathlib.Data.List.Map2

Goal state before:
pp: α : Type u
β : Type v
as : List α
bs : List β
⊢ as.zipRight bs = (as.zipRight' bs).fst

Tactic:
induction as generalizing bs

Goal state after:
case nil
α : Type u
β : Type v
bs : List β
⊢ [].zipRight bs = ([].zipRight' bs).fst

case cons
α : Type u
β : Type v
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (bs : List β), tail✝.zipRight bs = (tail✝.zipRight' bs).fst
bs : List β
⊢ (head✝ :: tail✝).zipRight bs = ((head✝ :: tail✝).zipRight' bs).fst
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]?
⊢ v[j]? = v[j + p]?

Tactic:
have shift_position' : (u ++ (v ++ w))[j + u.length + p]? = v[j + p]? := by
    have eq : j + u.length + p - u.length = j + p := by lia
    rw [getElem?_append_right]
    · rw [getElem?_append_left]
      · exact congrArg (getElem? v) eq
      · lia
    · lia

Goal state after:
α : 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]?
⊢ v[j]? = v[j + p]?
Module: Mathlib.Data.Ordmap.Ordnode

Goal state before:
pp: α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
⊢ Ordnode α

Tactic:
by
  rcases id l with _ | ls
  · rcases id r with _ | ⟨rs, rl, rx, rr⟩
    · exact ι x
    · rcases id rr with _ | rrs
      · rcases rl with _ | ⟨_, _, rlx⟩
        · exact node 2 nil x r
        · exact node 3 (ι x) rlx ι rx
      · rcases id rl with _ | ⟨rls, rll, rlx, rlr⟩
        · exact node 3 (ι x) rx rr
        · exact
            if rls < ratio * rrs then node (rs + 1) (node (rls + 1) nil x rl) rx rr
            else
              node (rs + 1) (node (size rll + 1) nil x rll) rlx
                (node (size rlr + rrs + 1) rlr rx rr)
  · 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.Ordmap.Ordset

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x✝ : α
r : Ordnode α
lo✝ : WithBot α
hi✝ : WithTop α
ol : l.Bounded lo✝ ↑x✝
Or : r.Bounded (↑x✝) hi✝
sl : l.Sized
sr : r.Sized
b : BalancedSz l.size r.size
bl : l.Balanced
br : r.Balanced
ol' : l.dual.Bounded (↑x✝) lo✝
sl' : l.dual.Sized
bl' : l.dual.Balanced
or' : r.dual.Bounded hi✝ ↑x✝
sr' : r.dual.Sized
br' : r.dual.Balanced
⊢ l.size + r.size + 1 = r.dual.size + l.dual.size + 1

Tactic:
by simp [size_dual, add_comm]

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

Goal state before:
pp: case zero
⊢ -zero.succ = (-zero).pred

Tactic:
try { rfl }

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

Goal state before:
pp: case pos
a✝ : PosNum
⊢ -(pos a✝).succ = (-pos a✝).pred

Tactic:
try { rfl }

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

Goal state before:
pp: case neg
a✝ : PosNum
⊢ -(neg a✝).succ = (-neg a✝).pred

Tactic:
try { rfl }

Goal state after:
case neg
a✝ : PosNum
⊢ -(neg a✝).succ = (-neg a✝).pred
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: l : ℕ
⊢ BalancedSz l 0 ↔ l ≤ 1

Tactic:
by
  simp +contextual [BalancedSz]

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

Goal state before:
pp: F : PFunctor.{uA, uB}
X : Type u_1
f : X → ↑F X
x : F.M
i : F.B x.head
H : ∀ (n : ℕ), head' (x.approx n.succ) = head' (x.approx (succ 0))
n : ℕ
P' : Agree (x.approx n.succ) (x.approx n.succ.succ)
⊢ cast ⋯ i ≍ i

pp: F : PFunctor.{uA, uB}
X : Type u_1
f : X → ↑F X
x : F.M
i : F.B x.head
H : ∀ (n : ℕ), head' (x.approx n.succ) = head' (x.approx (succ 0))
n : ℕ
P' : Agree (x.approx n.succ) (x.approx n.succ.succ)
⊢ i ≍ cast ⋯ i

Tactic:
· apply cast_heq

Goal state after:
F : PFunctor.{uA, uB}
X : Type u_1
f : X → ↑F X
x : F.M
i : F.B x.head
H : ∀ (n : ℕ), head' (x.approx n.succ) = head' (x.approx (succ 0))
n : ℕ
P' : Agree (x.approx n.succ) (x.approx n.succ.succ)
⊢ i ≍ cast ⋯ i
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case cons
F : PFunctor.{uA, uB}
xs : Path F
a a' : F.A
f : F.B a → F.M
i : F.B a'
f✝ : F.B a' → F.M
a✝ : IsPath xs (f✝ i)
h : M.mk ⟨a, f⟩ = M.mk ⟨a', f✝⟩
⊢ a = a'

Tactic:
cases mk_inj h

Goal state after:
case cons.refl
F : PFunctor.{uA, uB}
xs : Path F
a : F.A
f : F.B a → F.M
i : F.B a
a✝ : IsPath xs (f i)
h : M.mk ⟨a, f⟩ = M.mk ⟨a, f⟩
⊢ a = a
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case cons
F : PFunctor.{uA, uB}
xs : Path F
a : F.A
f : F.B a → F.M
i : F.B a
f✝ : F.B a → F.M
hp : IsPath xs (f✝ i)
h : M.mk ⟨a, f⟩ = M.mk ⟨a, f✝⟩
⊢ IsPath xs (f i)

Tactic:
cases mk_inj h

Goal state after:
case cons.refl
F : PFunctor.{uA, uB}
xs : Path F
a : F.A
f : F.B a → F.M
i : F.B a
hp : IsPath xs (f i)
h : M.mk ⟨a, f⟩ = M.mk ⟨a, f⟩
⊢ IsPath xs (f i)
Module: Mathlib.Data.PFunctor.Multivariate.M

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type u
g : β → ↑P (α ::: β)
x : β
⊢ ⟨(g x).fst,
      splitFun (dropFun (g x).snd)
        ((corec' P (fun b ↦ (g b).fst) (fun b ↦ dropFun (g b).snd) fun b ↦ lastFun (g b).snd) ∘ lastFun (g x).snd)⟩ =
    (TypeVec.id ::: corec P g) <$$> g x

Tactic:
obtain ⟨a, f⟩ := g x

Goal state after:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type u
g : β → ↑P (α ::: β)
x : β
a : P.A
f : P.B a ⟹ α ::: β
⊢ ⟨⟨a, f⟩.fst,
      splitFun (dropFun ⟨a, f⟩.snd)
        ((corec' P (fun b ↦ (g b).fst) (fun b ↦ dropFun (g b).snd) fun b ↦ lastFun (g b).snd) ∘ lastFun ⟨a, f⟩.snd)⟩ =
    (TypeVec.id ::: corec P g) <$$> ⟨a, f⟩
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
l : Ordnode α
x✝ : α
r : Ordnode α
sl : l.Sized
sr : r.Sized
⊢ l.size + r.size + 1 = r.dual.size + l.dual.size + 1

Tactic:
by simp [size_dual, add_comm]

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

Goal state before:
pp: v : Multiset ℕ+
h : ∀ (p : ℕ+), p ∈ v → p.Prime
⊢ (ofPNatMultiset v h).toPNatMultiset = v

Tactic:
dsimp [ofPNatMultiset, toPNatMultiset]
  have : (fun (p : ℕ+) (h : p.Prime) => ((↑) : Nat.Primes → ℕ+) ⟨p, h⟩) = fun p _ => id p := by
    funext p h
    apply Subtype.ext
    rfl
  rw [Multiset.map_pmap, this, Multiset.pmap_eq_map, Multiset.map_id]

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

Goal state before:
pp: v : Multiset ℕ+
h : ∀ (p : ℕ+), p ∈ v → p.Prime
⊢ (ofPNatMultiset v h).toPNatMultiset.prod = v.prod

Tactic:
rw [to_ofPNatMultiset]

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

Goal state before:
pp: α : Type u_1
x : α
hl : nil.Balanced
sl : nil.Sized
rs : ℕ
rx : α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
hr : ((node rls rll rlx rlr).node' rx nil).Balanced
sr : (node rs (node rls rll rlx rlr) rx nil).Sized
this : rls ≤ 1
⊢ rll.size = 0 ∧ rlr.size = 0

Tactic:
sr.2.1.1,

Goal state after:
α : Type u_1
x : α
hl : nil.Balanced
sl : nil.Sized
rs : ℕ
rx : α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
hr : ((node rls rll rlx rlr).node' rx nil).Balanced
sr : (node rs (node rls rll rlx rlr) rx nil).Sized
this : rll.size + rlr.size + 1 ≤ 1
⊢ rll.size = 0 ∧ rlr.size = 0
Module: Mathlib.Data.PNat.Find

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

Tactic:
simp [find_eq_iff]

Goal state after: