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

Goal state before:
pp: case cons
q : Λ'
s : Option Γ'
L₁ : List ℕ
L₃ : List Γ'
a : ℕ
L₂ : List ℕ
⊢ TransGen (fun a b ↦ b ∈ TM2.step tr a)
    (TM2.stepAux
      (tr
        ((fun x ↦
            Λ'.read fun s ↦
              (if s = some Γ'.consₗ then id else Λ'.clear (fun x ↦ decide (x = Γ'.consₗ)) stack) (unrev q))
          (some Γ'.cons)))
      (some Γ'.cons)
      (update
        (update
          (update (elim (trList L₁) [] [] (trList (a :: L₂) ++ Γ'.consₗ :: L₃)) stack (trList L₂ ++ Γ'.consₗ :: L₃)) rev
          ((trNat a).reverseAux (elim (trList L₁) [] [] (trList (a :: L₂) ++ Γ'.consₗ :: L₃) rev)))
        rev
        ((fun s ↦ ((fun x ↦ some Γ'.cons) s).getD default) (some Γ'.cons) ::
          update
            (update (elim (trList L₁) [] [] (trList (a :: L₂) ++ Γ'.consₗ :: L₃)) stack (trList L₂ ++ Γ'.consₗ :: L₃))
            rev ((trNat a).reverseAux (elim (trList L₁) [] [] (trList (a :: L₂) ++ Γ'.consₗ :: L₃) rev)) rev)))
    { l := some q, var := none, stk := elim (trList ((a :: L₂).headI :: L₁)) [] [] L₃ }

Tactic:
simp only [TM2.step, Option.mem_def, trList, List.append_assoc,
      List.cons_append, elim_update_stack, elim_rev, elim_update_rev, Function.update_self,
      List.headI_cons]

Goal state after:
case cons
q : Λ'
s : Option Γ'
L₁ : List ℕ
L₃ : List Γ'
a : ℕ
L₂ : List ℕ
⊢ TransGen
    (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)
    (TM2.stepAux
      (tr
        (Λ'.read fun s ↦ (if s = some Γ'.consₗ then id else Λ'.clear (fun x ↦ decide (x = Γ'.consₗ)) stack) (unrev q)))
      (some Γ'.cons)
      (elim (trList L₁) ((some Γ'.cons).getD default :: (trNat a).reverseAux []) [] (trList L₂ ++ Γ'.consₗ :: L₃)))
    { l := some q, var := none, stk := elim (trNat a ++ Γ'.cons :: trList L₁) [] [] L₃ }
Module: Mathlib.Topology.Category.LightProfinite.Basic

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ LightProfinite
⊢ TotallyDisconnectedSpace ↑(CompHaus.limitCone (F ⋙ lightProfiniteToCompHaus)).pt.toTop

Tactic:
by
  change TotallyDisconnectedSpace ({ u : ∀ j : J, F.obj j | _ } : Type _)
  exact Subtype.totallyDisconnectedSpace

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Yoneda

Goal state before:
pp: Y : Type w'
inst✝ : TopologicalSpace Y
α : Type
X : α → TopCat
⊢ (piComparison (yonedaPresheaf' Y) fun x ↦ op (X x)) =
    (yonedaPresheaf' Y).map ((opCoproductIsoProduct X).inv ≫ (TopCat.sigmaIsoSigma X).inv.op) ≫
      (equivEquivIso (sigmaEquiv Y fun x ↦ ↑(X x))).inv ≫ (Types.productIso fun i ↦ C(↑(X i), Y)).inv

Tactic:
← Category.assoc,

Goal state after:
Y : Type w'
inst✝ : TopologicalSpace Y
α : Type
X : α → TopCat
⊢ (piComparison (yonedaPresheaf' Y) fun x ↦ op (X x)) =
    ((yonedaPresheaf' Y).map ((opCoproductIsoProduct X).inv ≫ (TopCat.sigmaIsoSigma X).inv.op) ≫
        (equivEquivIso (sigmaEquiv Y fun x ↦ ↑(X x))).inv) ≫
      (Types.productIso fun i ↦ C(↑(X i), Y)).inv
Module: Mathlib.Topology.Category.Profinite.Extend

Goal state before:
pp: I : Type u
inst✝¹ : SmallCategory I
inst✝ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
hc : IsLimit c
X : FintypeCat
f : c.pt ⟶ toProfinite.obj X
this : DiscreteTopology ↑(toProfinite.obj X).toTop
f' : LocallyConstant ↑c.pt.toTop ↑(toProfinite.obj X).toTop :=
  { toFun := ⇑(ConcreteCategory.hom f), isLocallyConstant := ⋯ }
i : I
g : LocallyConstant ↑((F ⋙ toProfinite).obj i).toTop ↑(toProfinite.obj X).toTop
h : f' = LocallyConstant.comap (TopCat.Hom.hom (c.π.app i).hom) g
x : ↑c.pt.toTop
⊢ (ConcreteCategory.hom f) x = (ConcreteCategory.hom (c.π.app i ≫ toProfinite.map { hom := ↾⇑g })) x

Tactic:
exact LocallyConstant.congr_fun h x

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

Goal state before:
pp: case cons₁
S : Finset Λ'
f : Code
k : Cont'
IH : contSupp k ⊆ S → Supports (contSupp k) S
H : contSupp (Cont'.cons₁ f k) ⊆ S
⊢ Supports (contSupp (Cont'.cons₁ f k)) S

Tactic:
have H₁ := H; rw [contSupp_cons₁] at H₁; have H₂ := Finset.union_subset_right H₁
    refine trStmts₁_supports' (trNormal_supports H₂) H₁ fun h => ?_
    refine supports_union.2 ⟨codeSupp'_supports H₂, ?_⟩
    simp only [codeSupp, contSupp_cons₂, Finset.union_subset_iff] at H₂
    exact trStmts₁_supports' (head_supports H₂.2.2) (Finset.union_subset_right h) IH

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)
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})))
inst✝¹ : PreservesFiniteProducts Y
inst✝ : HasExplicitFiniteCoproducts P
a : Fiber ⇑f
⊢ (ConcreteCategory.hom ((sigmaComparison Y fun a ↦ ↑(fiber f a).toTop) ≫ ↾fun g ↦ g a))
      ((ConcreteCategory.hom (Y.map (sigmaIso f).hom.op)) ((ConcreteCategory.hom (counitAppApp S Y)) f)) =
    counitAppAppImage f a

Tactic:
simp only [counitAppApp, Functor.mapIso_inv, ← Iso.op_hom, CategoryTheory.comp_apply,
    ConcreteCategory.hom_ofHom, TypeCat.Fun.coe_mk, ← Functor.map_comp_apply, Iso.inv_hom_id,
    Functor.map_id_apply]

Goal state after:
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})))
inst✝¹ : PreservesFiniteProducts Y
inst✝ : HasExplicitFiniteCoproducts P
a : Fiber ⇑f
⊢ (ConcreteCategory.hom (sigmaComparison Y fun a ↦ ↑↑a))
      ((ConcreteCategory.hom (inv (sigmaComparison Y fun a ↦ ↑↑a))) (counitAppAppImage f)) a =
    counitAppAppImage f a
Module: Mathlib.Condensed.Discrete.Module

Goal state before:
pp: P : TopCat → Prop
R : Type (u + 1)
inst✝ : Ring R
X✝ Y✝ : ModuleCat R
f : X✝ ⟶ Y✝
⊢ (functorIsoDiscreteComponents R X✝).hom ≫ (functor R).map f ≫ (functorIsoDiscreteComponents R Y✝).inv =
    (presheafToSheaf (coherentTopology CompHaus) (ModuleCat R)).map ((Functor.const CompHausᵒᵖ).map f)

Tactic:
← Category.assoc,

Goal state after:
P : TopCat → Prop
R : Type (u + 1)
inst✝ : Ring R
X✝ Y✝ : ModuleCat R
f : X✝ ⟶ Y✝
⊢ ((functorIsoDiscreteComponents R X✝).hom ≫ (functor R).map f) ≫ (functorIsoDiscreteComponents R Y✝).inv =
    (presheafToSheaf (coherentTopology CompHaus) (ModuleCat R)).map ((Functor.const CompHausᵒᵖ).map f)
Module: Mathlib.Condensed.Discrete.Module

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

Tactic:
← Category.assoc,

Goal state after:
P : TopCat → Prop
R : Type u
inst✝ : Ring R
X✝ Y✝ : ModuleCat R
f : X✝ ⟶ Y✝
⊢ ((functorIsoDiscreteComponents R X✝).hom ≫ (functor R).map f) ≫ (functorIsoDiscreteComponents R Y✝).inv =
    (presheafToSheaf (coherentTopology LightProfinite) (ModuleCat R)).map ((Functor.const LightProfiniteᵒᵖ).map f)
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
⊢ ∃ S' π,
    ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
      ∃ g', P ◁ (lightProfiniteToLightCondSet ⋙ free R).map π ≫ g = g' ≫ e

Tactic:
have hh := h.1 e
    rw [LightCondMod.epi_iff_locallySurjective_on_lightProfinite] at hh
    specialize hh S ((ihomPoints R P B S).symm g)
    obtain ⟨S', π, hπ, g', hh⟩ := hh
    refine ⟨S', π, hπ, (ihomPoints _ _ _ _) g', ?_⟩
    rw [ihom_map_val_app] at hh
    apply (ihomPoints R P B S').symm.injective
    rw [hh]
    exact ihomPoints_symm_comp R B P S' S π g

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
C : TypeVec.{?u.15} (n + 1) → Sort u
H : (α : TypeVec.{?u.15} n) → (β : Type ?u.15) → C (α ::: β)
γ : TypeVec.{?u.15} (n + 1)
⊢ C (γ.drop ::: γ.last)

Tactic:
apply H

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

Goal state before:
pp: S : Type u_1
T : Type u_2
X : Type u_3
π : T → S × OnePoint X
hπ : Function.Surjective π
⊢ Function.Surjective (y π)

Tactic:
intro s
  let p (s : S) (n : OnePoint X) : T := (hπ (s, n)).choose
  have hp (s : S) (n : OnePoint X) : π (p s n) = (s, n) := (hπ (s, n)).choose_spec
  exact ⟨⟨fun n ↦ ⟨p s n, by grind⟩, by grind⟩, by grind⟩

Goal state after:
Module: Mathlib.Data.Analysis.Topology

Goal state before:
pp: α : Type u_1
τ : Type u_4
inst✝ : TopologicalSpace α
F : Realizer α
E : F.σ ≃ τ
s : τ
⊢ (F.ofEquiv E).F.f s = F.F.f (E.symm s)

Tactic:
by
  delta ofEquiv; simp

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

Goal state before:
pp: case refine_1
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
t : (i : ι) → Finset (α i)
inst✝ : (i : ι) → DecidableEq (α i)
f : (a : ι) → a ∈ s → α a
hf : f ∈ s.pi t
⊢ (DFinsupp.mk s fun i ↦ f ↑i ⋯).support ⊆ s ∧ ∀ i ∈ s, (DFinsupp.mk s fun i ↦ f ↑i ⋯) i ∈ t i

Tactic:
refine ⟨support_mk_subset, fun i hi => ?_⟩

Goal state after:
case refine_1
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
t : (i : ι) → Finset (α i)
inst✝ : (i : ι) → DecidableEq (α i)
f : (a : ι) → a ∈ s → α a
hf : f ∈ s.pi t
i : ι
hi : i ∈ s
⊢ (DFinsupp.mk s fun i ↦ f ↑i ⋯) i ∈ t i
Module: Mathlib.Data.Bool.Count

Goal state before:
pp: l : List Bool
b : Bool
⊢ count (!b) l + count b l = l.length

Tactic:
have := length_eq_countP_add_countP (l := l) (· == !b)
  aesop (add simp this)

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:
← 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.List.Lookmap

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

Tactic:
rcases h' : f a with - | b

Goal state after:
case none
α : Type u_1
β : Type u_2
f : α → Option α
g : α → β
h : ∀ (a b : α), b ∈ f a → g a = g b
a : α
l : List α
h' : f a = none
⊢ map g (lookmap f (a :: l)) = map g (a :: l)

case some
α : Type u_1
β : Type u_2
f : α → Option α
g : α → β
h : ∀ (a b : α), b ∈ f a → g a = g b
a : α
l : List α
b : α
h' : f a = some b
⊢ map g (lookmap f (a :: l)) = map g (a :: l)
Module: Mathlib.Data.List.Lookmap

Goal state before:
pp: case cons
α : Type u_1
f : α → Option α
l₁ l₂ : List α
a : α
l₁✝ l₂✝ : List α
p : l₁✝ ~ l₂✝
IH : Pairwise (fun a b ↦ ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₁✝ → lookmap f l₁✝ ~ lookmap f l₂✝
H : Pairwise (fun a b ↦ ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) (a :: l₁✝)
⊢ lookmap f (a :: l₁✝) ~ lookmap f (a :: l₂✝)

Tactic:
| cons a p IH =>

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

Goal state before:
pp: case mp
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint s₂
x✝ : α
y✝ : β x✝
h' : dlookup x✝ s₁.entries = some y✝ ∨ ¬x✝ ∈ s₁.entries.keys ∧ dlookup x✝ s₂.entries = some y✝
⊢ dlookup x✝ s₂.entries = some y✝ ∨ ¬x✝ ∈ s₂.entries.keys ∧ dlookup x✝ s₁.entries = some y✝

pp: case mpr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint s₂
x✝ : α
y✝ : β x✝
h' : dlookup x✝ s₂.entries = some y✝ ∨ ¬x✝ ∈ s₂.entries.keys ∧ dlookup x✝ s₁.entries = some y✝
⊢ dlookup x✝ s₁.entries = some y✝ ∨ ¬x✝ ∈ s₁.entries.keys ∧ dlookup x✝ s₂.entries = some y✝

Tactic:
· rcases h' with h' | h'
        · right
          refine ⟨?_, h'⟩
          apply h
          rw [keys, ← List.dlookup_isSome, h']
          exact rfl
        · left
          rw [h'.2]

Goal state after:
case mpr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint s₂
x✝ : α
y✝ : β x✝
h' : dlookup x✝ s₂.entries = some y✝ ∨ ¬x✝ ∈ s₂.entries.keys ∧ dlookup x✝ s₁.entries = some y✝
⊢ dlookup x✝ s₁.entries = some y✝ ∨ ¬x✝ ∈ s₁.entries.keys ∧ dlookup x✝ s₂.entries = some y✝
Module: Mathlib.Data.Finset.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : DenselyOrdered α
s t : Set α
hsf : s.Finite
hs : s.Nonempty
htf : t.Finite
ht : t.Nonempty
H : ∀ x ∈ s, ∀ y ∈ t, x < y
⊢ ∃ b, (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y

Tactic:
convert!
    Finset.exists_between (s := hsf.toFinset) (t := htf.toFinset) (by simpa) (by simpa)
      (by simpa) using
    1

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : DenselyOrdered α
s t : Set α
hsf : s.Finite
hs : s.Nonempty
htf : t.Finite
ht : t.Nonempty
H : ∀ x ∈ s, ∀ y ∈ t, x < y
⊢ (fun b ↦ (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y) = fun b ↦ (∀ x ∈ hsf.toFinset, x < b) ∧ ∀ y ∈ htf.toFinset, b < y
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s✝ : Finmap β
s : AList β
⊢ lookup a (insert a b ⟦s⟧) = some b

Tactic:
simp only [insert_toFinmap, lookup_toFinmap, AList.lookup_insert]

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁✝ : Finmap β
s₁ : AList β
⊢ ⟦∅⟧ ∪ ⟦s₁⟧ = ⟦s₁⟧

Tactic:
simp [-empty_toFinmap, union_toFinmap]

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁✝ : Finmap β
s₁ : AList β
⊢ ⟦s₁⟧ ∪ ⟦∅⟧ = ⟦s₁⟧

Tactic:
simp [-empty_toFinmap, union_toFinmap]

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih : a ∈ tl.keys → ∃ b l₁ l₂, ¬a ∈ l₁.keys ∧ tl = l₁ ++ ⟨a, b⟩ :: l₂ ∧ kerase a tl = l₁ ++ l₂
e : ¬a = hd.fst
h : a ∈ tl.keys
b : β a
tl₁ tl₂ : List (Sigma β)
h₁ : ¬a ∈ tl₁.keys
h₂ : tl = tl₁ ++ ⟨a, b⟩ :: tl₂
h₃ : kerase a tl = tl₁ ++ tl₂
⊢ hd :: tl = hd :: tl₁ ++ ⟨a, b⟩ :: tl₂

Tactic:
(rw [h₂]; rfl)

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

Goal state before:
pp: case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
l : List (Sigma β)
h : ¬a = a'
⊢ kerase a (kerase a' l) = kerase a' (kerase a l)

Tactic:
induction l with
  | nil => rfl
  | cons x xs =>
    by_cases a' = x.1
    · subst a'
      simp [kerase_cons_ne h, kerase_cons_eq rfl]
    by_cases h' : a = x.1
    · subst a
      simp [kerase_cons_eq rfl, kerase_cons_ne (Ne.symm h)]
    · simp [kerase_cons_ne, *]

Goal state after:
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
ds : List ℕ
inst✝ : NonUnitalNonAssocSemiring α
β : Type u_1
n : ℕ
s✝ : Finset β
f : β → Holor α ds
this : DecidableEq β := Classical.decEq β
x : β
s : Finset β
⊢ x ∉ s →
    ((∀ x ∈ s, CPRankMax n (f x)) → CPRankMax (s.card * n) (∑ x ∈ s, f x)) →
      (∀ x_1 ∈ insert x s, CPRankMax n (f x_1)) → CPRankMax ((insert x s).card * n) (∑ x ∈ insert x s, f x)

Tactic:
(h_x_notin_s : x ∉ s)

Goal state after:
α : Type
ds : List ℕ
inst✝ : NonUnitalNonAssocSemiring α
β : Type u_1
n : ℕ
s✝ : Finset β
f : β → Holor α ds
this : DecidableEq β := Classical.decEq β
x : β
s : Finset β
h_x_notin_s : x ∉ s
⊢ ((∀ x ∈ s, CPRankMax n (f x)) → CPRankMax (s.card * n) (∑ x ∈ s, f x)) →
    (∀ x_1 ∈ insert x s, CPRankMax n (f x_1)) → CPRankMax ((insert x s).card * n) (∑ x ∈ insert x s, f x)
Module: Mathlib.Data.Int.Order.Lemmas

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

Tactic:
exact Int.ofNat_lt.symm

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

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
⊢ takeWhile (fun a ↦ decide (p a = true)) l = takeWhile p l

Tactic:
Bool.decide_coe

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

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
⊢ takeWhile p (takeWhile p l) = takeWhile p l

Tactic:
simp_rw [takeWhile_takeWhile, and_self_iff, Bool.decide_coe]

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

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
⊢ rdropWhile p l <+: l

Tactic:
rw [← reverse_suffix, rdropWhile, reverse_reverse]
  exact dropWhile_suffix _

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

Goal state before:
pp: case inr
n m l : ℕ
hlm : l ≤ m
hln : l ≤ n
⊢ filter (fun x ↦ decide (x < l)) (Ico n m) = []

Tactic:
filter_lt_of_le_bot hln

Goal state after:
case inr
n m l : ℕ
hlm : l ≤ m
hln : l ≤ n
⊢ [] = []
Module: Mathlib.Data.List.Palindrome

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

Tactic:
have : Palindrome l := hp (append_inj_left' (tail_eq_of_cons_eq hr) rfl)

Goal state after:
α : Type u_1
l✝ : List α
x : α
l : List α
y : α
hp : l.reverse = l → l.Palindrome
hr : [y].reverse ++ l.reverse ++ [x] = x :: (l ++ [y])
this : l.Palindrome
⊢ (x :: (l ++ [x])).Palindrome
Module: Mathlib.Data.List.Lemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → α
g : α → γ → α
hfg : (Set.range fun a c ↦ f c a) ⊆ Set.range fun b c ↦ g c b
a : α
⊢ Set.range (foldl f a) ⊆ Set.range (foldl g a)

Tactic:
change (Set.range fun l => _) ⊆ Set.range fun l => _
  -- Porting note: have to write `(foldr_reverse)` instead of `foldr_reverse`.
  simp_rw [← (foldr_reverse), Set.range_comp' _ reverse,
    reverse_involutive.bijective.surjective.range_eq, Set.image_univ]
  exact foldr_range_subset_of_range_subset hfg a

Goal state after:
Module: Mathlib.Data.Nat.Factorization.Divisors

Goal state before:
pp: n : ℕ
hn : ¬n = 0
k : ℕ
x✝ : k ∈ {x | ∃ f < n.factorization, (f.prod fun x1 x2 ↦ x1 ^ x2) = x}
f : ℕ →₀ ℕ
hlt : f < n.factorization
h : (f.prod fun x1 x2 ↦ x1 ^ x2) = k
⊢ (f.prod fun x1 x2 ↦ x1 ^ x2) ∣ n.factorization.prod fun x1 x2 ↦ x1 ^ x2

Tactic:
apply prod_dvd_prod_of_subset_of_dvd <| support_mono hlt.le

Goal state after:
n : ℕ
hn : ¬n = 0
k : ℕ
x✝ : k ∈ {x | ∃ f < n.factorization, (f.prod fun x1 x2 ↦ x1 ^ x2) = x}
f : ℕ →₀ ℕ
hlt : f < n.factorization
h : (f.prod fun x1 x2 ↦ x1 ^ x2) = k
⊢ ∀ a ∈ f.support, a ^ f a ∣ a ^ n.factorization a
Module: Mathlib.Data.Nat.Fib.Zeckendorf

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ n.greatestFib - 1 ≠ 0

Tactic:
simpa [← succ_le_iff, tsub_eq_zero_iff_le] using hn.bot_lt

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

Goal state before:
pp: p : ℕ → Prop
hf : (Set.ofPred p).Infinite
⊢ StrictMono (nth p)

Tactic:
rw [nth_eq_orderIsoOfNat hf]

Goal state after:
p : ℕ → Prop
hf : (Set.ofPred p).Infinite
⊢ StrictMono (Subtype.val ∘ ⇑(Subtype.orderIsoOfNat (Set.ofPred p)))
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
hf : (Set.ofPred p).Infinite
⊢ Set.range (nth p) = Set.ofPred p

Tactic:
rw [nth_eq_orderIsoOfNat hf]

Goal state after:
p : ℕ → Prop
hf : (Set.ofPred p).Infinite
⊢ Set.range (Subtype.val ∘ ⇑(Subtype.orderIsoOfNat (Set.ofPred p))) = Set.ofPred p
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: case pos
p : ℕ → Prop
f : ℕ → ℕ
hmaps : Set.MapsTo f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset} (Set.ofPred p)
hmono : StrictMonoOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}
n : ℕ
hn : ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset
⊢ nth p n ≤ f n

Tactic:
induction n using Nat.strong_induction_on with

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

Goal state before:
pp: case succ
p : ℕ → Prop
inst✝ : DecidablePred p
k : ℕ
ihk : (∀ (hf : (Set.ofPred p).Finite), k < #hf.toFinset) → count p (nth p k) = k
hn : ∀ (hf : (Set.ofPred p).Finite), k + 1 < #hf.toFinset
⊢ #(insert (nth p k) ({n ∈ range (nth p k) | p n})) = k + 1

Tactic:
card_insert_of_notMem,

Goal state after:
case succ
p : ℕ → Prop
inst✝ : DecidablePred p
k : ℕ
ihk : (∀ (hf : (Set.ofPred p).Finite), k < #hf.toFinset) → count p (nth p k) = k
hn : ∀ (hf : (Set.ofPred p).Finite), k + 1 < #hf.toFinset
⊢ #({n ∈ range (nth p k) | p n}) + 1 = k + 1

case succ
p : ℕ → Prop
inst✝ : DecidablePred p
k : ℕ
ihk : (∀ (hf : (Set.ofPred p).Finite), k < #hf.toFinset) → count p (nth p k) = k
hn : ∀ (hf : (Set.ofPred p).Finite), k + 1 < #hf.toFinset
⊢ nth p k ∉ {n ∈ range (nth p k) | p n}
Module: Mathlib.Data.PFunctor.Multivariate.Basic

Goal state before:
pp: case mp
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : P.B a ⟹ α
⊢ (∃ a_1 f_1, ⟨a, f⟩ = ⟨a_1, f_1⟩ ∧ ∀ (i : Fin2 n) (j : P.B a_1 i), p (f_1 i j)) →
    ∀ (i : Fin2 n) (x : P.B a i), p (f i x)

pp: case mpr
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : P.B a ⟹ α
⊢ (∀ (i : Fin2 n) (x : P.B a i), p (f i x)) →
    ∃ a_2 f_1, ⟨a, f⟩ = ⟨a_2, f_1⟩ ∧ ∀ (i : Fin2 n) (j : P.B a_2 i), p (f_1 i j)

Tactic:
· rintro ⟨_, _, ⟨⟩, _⟩
    assumption

Goal state after:
case mpr
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : P.B a ⟹ α
⊢ (∀ (i : Fin2 n) (x : P.B a i), p (f i x)) →
    ∃ a_2 f_1, ⟨a, f⟩ = ⟨a_2, f_1⟩ ∧ ∀ (i : Fin2 n) (j : P.B a_2 i), p (f_1 i j)
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case pos.zero.succ
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : 0 < l.size
mr₁ : 2 * r.size ≤ ml.size + mr.size + 1
lr₁ : 3 * l.size ≤ ml.size + mr.size + (1 + 1)
lr₂ : 3 * (ml.size + mr.size + 1 + r.size) ≤ 16 * l.size + 9
mr₂ : ml.size + mr.size + 1 ≤ delta * r.size
r0 : r.size > 0
r1 : r.size = 1
l1 : l.size = 1
n✝ : ℕ
mm : n✝ + 1 ≤ 1
⊢ BalancedSz 1 0 ∧ BalancedSz (n✝ + 1) 1 ∧ BalancedSz (1 + 0 + 1) (n✝ + 1 + 1 + 1)

Tactic:
rcases mm with (_ | ⟨⟨⟩⟩)

Goal state after:
case pos.zero.succ.refl
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : 0 < l.size
mr₁ : 2 * r.size ≤ ml.size + mr.size + 1
lr₁ : 3 * l.size ≤ ml.size + mr.size + (1 + 1)
lr₂ : 3 * (ml.size + mr.size + 1 + r.size) ≤ 16 * l.size + 9
mr₂ : ml.size + mr.size + 1 ≤ delta * r.size
r0 : r.size > 0
r1 : r.size = 1
l1 : l.size = 1
⊢ BalancedSz 1 0 ∧ BalancedSz (0 + 1) 1 ∧ BalancedSz (1 + 0 + 1) (0 + 1 + 1 + 1)
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
t : Ordnode α
ht : t.Sized
⊢ t.size = 0 ↔ t = nil

Tactic:
cases t <;> [simp; simp [ht.1]]

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

Goal state before:
pp: case pos.succ.zero
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : 0 < l.size
mr₁ : 2 * r.size ≤ ml.size + mr.size + 1
lr₁ : 3 * l.size ≤ ml.size + mr.size + (1 + 1)
lr₂ : 3 * (ml.size + mr.size + 1 + r.size) ≤ 16 * l.size + 9
mr₂ : ml.size + mr.size + 1 ≤ delta * r.size
r0 : r.size > 0
r1 : r.size = 1
l1 : l.size = 1
n✝ : ℕ
mm : n✝ + 1 + 0 ≤ 1
⊢ BalancedSz 1 (n✝ + 1) ∧ BalancedSz 0 1 ∧ BalancedSz (1 + (n✝ + 1) + 1) (0 + 1 + 1)

Tactic:
rcases mm with (_ | ⟨⟨⟩⟩)

Goal state after:
case pos.succ.zero.refl
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : 0 < l.size
mr₁ : 2 * r.size ≤ ml.size + mr.size + 1
lr₁ : 3 * l.size ≤ ml.size + mr.size + (1 + 1)
lr₂ : 3 * (ml.size + mr.size + 1 + r.size) ≤ 16 * l.size + 9
mr₂ : ml.size + mr.size + 1 ≤ delta * r.size
r0 : r.size > 0
r1 : r.size = 1
l1 : l.size = 1
⊢ BalancedSz 1 (0 + 1) ∧ BalancedSz 0 1 ∧ BalancedSz (1 + (0 + 1) + 1) (0 + 1 + 1)