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})))
X : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝¹ : PreservesFiniteProducts X
x y : X.obj (op S)
inst✝ : HasExplicitFiniteCoproducts P
h :
  ∀ (a : Fiber ⇑f),
    (ConcreteCategory.hom (X.map (sigmaIncl f a).op)) x = (ConcreteCategory.hom (X.map (sigmaIncl f a).op)) y
a : Fiber ⇑f
⊢ (ConcreteCategory.hom (sigmaComparison X fun a ↦ ↑(fiber f a).toTop))
      ((ConcreteCategory.hom (X.mapIso (sigmaIso f).op).hom) x) a =
    (ConcreteCategory.hom (sigmaComparison X fun a ↦ ↑(fiber f a).toTop))
      ((ConcreteCategory.hom (X.mapIso (sigmaIso f).op).hom) y) a

Tactic:
specialize h a

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})))
X : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝¹ : PreservesFiniteProducts X
x y : X.obj (op S)
inst✝ : HasExplicitFiniteCoproducts P
a : Fiber ⇑f
h : (ConcreteCategory.hom (X.map (sigmaIncl f a).op)) x = (ConcreteCategory.hom (X.map (sigmaIncl f a).op)) y
⊢ (ConcreteCategory.hom (sigmaComparison X fun a ↦ ↑(fiber f a).toTop))
      ((ConcreteCategory.hom (X.mapIso (sigmaIso f).op).hom) x) a =
    (ConcreteCategory.hom (sigmaComparison X fun a ↦ ↑(fiber f a).toTop))
      ((ConcreteCategory.hom (X.mapIso (sigmaIso f).op).hom) y) a
Module: Mathlib.Condensed.Discrete.Characterization

Goal state before:
pp: X : LightCondSet
h : (S : LightProfinite) → IsColimit (X.obj.mapCocone (coconeRightOpOfCone S.asLimitCone))
i : X.obj ≅ (LocallyConstant.functor.obj (X.obj.obj (toLightProfinite.op.obj (Opposite.op (of PUnit.{u + 1}))))).obj :=
  LightCondensed.isoLocallyConstantOfIsColimit X.obj h
⊢ LocallyConstant.functor.essImage X

Tactic:
exact ⟨_, ⟨((sheafToPresheaf _ _).preimageIso i.symm)⟩⟩

Goal state after:
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
⊢ ∃ k, Continuous[inst✝⁸, inst✝⁴] k ∧ f' ∘ k = g' ∧ k ∘ f = g

Tactic:
let D : S → Set Y := fun i ↦ g' ⁻¹' ({f' i})

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}
⊢ ∃ k, Continuous[inst✝⁸, inst✝⁴] k ∧ f' ∘ k = g' ∧ k ∘ f = g
Module: Mathlib.Condensed.TopCatAdjunction

Goal state before:
pp: X✝ : CondensedSet
X : TopCat
inst✝ : UCompactlyGeneratedSpace ↑X
⊢ Continuous (topCatAdjunctionCounitEquiv X).invFun

Tactic:
apply continuous_from_uCompactlyGeneratedSpace

Goal state after:
X✝ : CondensedSet
X : TopCat
inst✝ : UCompactlyGeneratedSpace ↑X
⊢ ∀ (S : CompHaus) (g : C(↑S.toTop, ↑X)), Continuous ((topCatAdjunctionCounitEquiv X).invFun ∘ ⇑g)
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α : Type u_1
β γ : Type u
f : β → F γ
g : α → G β
x : Option α
⊢ Option.traverse (Comp.mk ∘ (fun x ↦ f <$> x) ∘ g) x = Comp.mk (Option.traverse f <$> Option.traverse g x)

Tactic:
cases x <;> (simp [Option.traverse, Option.mapM, functor_norm] <;> rfl)

Goal state after:
Module: Mathlib.Control.Fold

Goal state before:
pp: m : Type u → Type u
inst✝¹ : Monad m
α β : Type u
inst✝ : LawfulMonad m
f : α → β → m β
⊢ ∀ (x y : FreeMonoid α),
    flip (List.foldrM f) (FreeMonoid.toList (x * y)) =
      flip (List.foldrM f) (FreeMonoid.toList x) * flip (List.foldrM f) (FreeMonoid.toList y)

Tactic:
intros; funext; apply List.foldrM_append

Goal state after:
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: m : Type u → Type v
inst✝ : Monad m
α β ε : Type u
x : Label (Except ε α) m β
i : α
⊢ goto (mkLabel x) i = mk (Except.ok <$> goto x (Except.ok i))

Tactic:
cases x; rfl

Goal state after:
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: m : Type u → Type v
inst✝¹ : Monad m
α : Type u_1
β ω : Type u
inst✝ : EmptyCollection ω
x : Label (α × ω) m β
i : α
⊢ goto (mkLabel x) i = monadLift (goto x (i, ∅))

Tactic:
cases x; rfl

Goal state after:
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: m : Type u → Type v
inst✝¹ : Monad m
α : Type u_1
β ω : Type u
inst✝ : Monoid ω
x : Label (α × ω) m β
i : α
⊢ goto (mkLabel' x) i = monadLift (goto x (i, 1))

Tactic:
cases x; rfl

Goal state after:
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: m : Type u → Type v
α β σ : Type u
x : Label (α × σ) m (β × σ)
i : α
⊢ goto (mkLabel x) i = mk fun s ↦ goto x (i, s)

Tactic:
cases x; rfl

Goal state after:
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: m : Type u → Type v
α : Type u_1
ρ β : Type u
x : Label α m β
i : α
⊢ goto (mkLabel ρ x) i = monadLift (goto x i)

Tactic:
cases x; rfl

Goal state after:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: case pos
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
i : ℕ
b : β x
hb : b ∈ approx (⇑f) i x
b' : β x
h' : b' ∈ Part.fix (⇑f) x
⊢ b' ∈ approx (⇑f) i x

Tactic:
have hb' := approx_le_fix f i _ _ hb

Goal state after:
case pos
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
i : ℕ
b : β x
hb : b ∈ approx (⇑f) i x
b' : β x
h' : b' ∈ Part.fix (⇑f) x
hb' : b ∈ Part.fix (⇑f) x
⊢ b' ∈ approx (⇑f) i x
Module: Mathlib.Data.Analysis.Filter

Goal state before:
pp: case mk.mk.mpr
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
σ✝¹ : Type ?u.88
F✝¹ : CFilter (Set α) σ✝¹
σ✝ : Type ?u.92
F✝ : CFilter (Set α) σ✝
s✝ : Set α
⊢ s✝ ∈
      { sets := {a | ∃ b, F✝¹.f b ⊆ a}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ } ⊓
        { sets := {a | ∃ b, F✝.f b ⊆ a}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ } →
    s✝ ∈ { sets := {a | ∃ a_1 b, F✝¹.f a_1 ∩ F✝.f b ⊆ a}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }

Tactic:
rintro ⟨_, ⟨a, ha⟩, _, ⟨b, hb⟩, rfl⟩

Goal state after:
case mk.mk.mpr
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
σ✝¹ : Type ?u.88
F✝¹ : CFilter (Set α) σ✝¹
σ✝ : Type ?u.92
F✝ : CFilter (Set α) σ✝
w✝¹ : Set α
a : σ✝¹
ha : F✝¹.f a ⊆ w✝¹
w✝ : Set α
b : σ✝
hb : F✝.f b ⊆ w✝
⊢ w✝¹ ∩ w✝ ∈ { sets := {a | ∃ a_1 b, F✝¹.f a_1 ∩ F✝.f b ⊆ a}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }
Module: Mathlib.Data.DFinsupp.Interval

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

Tactic:
intro x hx

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : (i : ι) → Zero (α i)
inst✝³ : (i : ι) → PartialOrder (α i)
inst✝² : (i : ι) → LocallyFiniteOrder (α i)
f g : Π₀ (i : ι), α i
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
x : ι
hx : x ∈ (f.rangeIcc g).support
⊢ x ∈ f.support ∪ g.support
Module: Mathlib.Data.Fin.Tuple.Take

Goal state before:
pp: case pos
n : ℕ
α : Fin n → Sort u_1
m : ℕ
h : m ≤ n
v : (i : Fin n) → α i
i : Fin m
x : α (castLE h i)
j : Fin m
h' : j = i
⊢ take m h (update v (castLE h i) x) j = update (take m h v) i x j

pp: case neg
n : ℕ
α : Fin n → Sort u_1
m : ℕ
h : m ≤ n
v : (i : Fin n) → α i
i : Fin m
x : α (castLE h i)
j : Fin m
h' : ¬j = i
⊢ take m h (update v (castLE h i) x) j = update (take m h v) i x j

Tactic:
· rw [h']
    simp only [take, update_self]

Goal state after:
case neg
n : ℕ
α : Fin n → Sort u_1
m : ℕ
h : m ≤ n
v : (i : Fin n) → α i
i : Fin m
x : α (castLE h i)
j : Fin m
h' : ¬j = i
⊢ take m h (update v (castLE h i) x) j = update (take m h v) i x j
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
inst✝ : FinEnum α
⊢ (List.map (⇑equiv.symm) (List.finRange (card α))).Nodup

Tactic:
apply List.Nodup.map

Goal state after:
case hf
α : Type u
inst✝ : FinEnum α
⊢ Injective ⇑equiv.symm

case a
α : Type u
inst✝ : FinEnum α
⊢ (List.finRange (card α)).Nodup
Module: Mathlib.Data.FinEnum

Goal state before:
pp: case e_4
α : Type u
β : α → Type v
inst✝ : IsEmpty α
e : FinEnum α
x : α
⊢ (fun b ↦ decEq x b) = fun b ↦ decidableEq_of_subsingleton x b

Tactic:
exact ‹IsEmpty α›.elim x

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Pi

Goal state before:
pp: case insert.refine_1.inl
α : Type u_1
ι : Type u_2
inst✝² : DistribLattice α
inst✝¹ : BoundedOrder α
inst✝ : DecidableEq ι
κ : ι → Type u_3
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → α
s : Finset ι
ih : (s.inf fun i ↦ (t i).sup (f i)) = (s.pi t).sup fun g ↦ s.attach.inf fun i ↦ f (↑i) (g ↑i ⋯)
c : α
g : (a : ι) → a ∈ s → κ a
hg : ∀ (a : ι) (h : a ∈ s), g a h ∈ t a
j : ι
hi : j ∉ s
h :
  ∀ (b : (a : ι) → a ∈ insert j s → κ a),
    (∀ (a : ι) (h : a ∈ insert j s), b a h ∈ t a) →
      f j (b j ⋯) ⊓ s.attach.inf ((fun i ↦ f (↑i) (b ↑i ⋯)) ∘ fun x ↦ ⟨↑x, ⋯⟩) ≤ c
a : κ j
ha : a ∈ t j
aux : ∀ (j_1 : ↥s), ↑j_1 ≠ j
hj : j ∈ insert j s
⊢ (if hji : j = j then cast ⋯ a else g j ⋯) ∈ t j

pp: case insert.refine_1.inr
α : Type u_1
ι : Type u_2
inst✝² : DistribLattice α
inst✝¹ : BoundedOrder α
inst✝ : DecidableEq ι
κ : ι → Type u_3
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → α
i : ι
s : Finset ι
hi : i ∉ s
ih : (s.inf fun i ↦ (t i).sup (f i)) = (s.pi t).sup fun g ↦ s.attach.inf fun i ↦ f (↑i) (g ↑i ⋯)
c : α
h :
  ∀ (b : (a : ι) → a ∈ insert i s → κ a),
    (∀ (a : ι) (h : a ∈ insert i s), b a h ∈ t a) →
      f i (b i ⋯) ⊓ s.attach.inf ((fun i_1 ↦ f (↑i_1) (b ↑i_1 ⋯)) ∘ fun x ↦ ⟨↑x, ⋯⟩) ≤ c
a : κ i
g : (a : ι) → a ∈ s → κ a
ha : a ∈ t i
hg : ∀ (a : ι) (h : a ∈ s), g a h ∈ t a
aux : ∀ (j : ↥s), ↑j ≠ i
j : ι
hj✝ : j ∈ insert i s
hj : j ∈ s
⊢ (if hji : j = i then cast ⋯ a else g j ⋯) ∈ t j

Tactic:
· simpa

Goal state after:
case insert.refine_1.inr
α : Type u_1
ι : Type u_2
inst✝² : DistribLattice α
inst✝¹ : BoundedOrder α
inst✝ : DecidableEq ι
κ : ι → Type u_3
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → α
i : ι
s : Finset ι
hi : i ∉ s
ih : (s.inf fun i ↦ (t i).sup (f i)) = (s.pi t).sup fun g ↦ s.attach.inf fun i ↦ f (↑i) (g ↑i ⋯)
c : α
h :
  ∀ (b : (a : ι) → a ∈ insert i s → κ a),
    (∀ (a : ι) (h : a ∈ insert i s), b a h ∈ t a) →
      f i (b i ⋯) ⊓ s.attach.inf ((fun i_1 ↦ f (↑i_1) (b ↑i_1 ⋯)) ∘ fun x ↦ ⟨↑x, ⋯⟩) ≤ c
a : κ i
g : (a : ι) → a ∈ s → κ a
ha : a ∈ t i
hg : ∀ (a : ι) (h : a ∈ s), g a h ∈ t a
aux : ∀ (j : ↥s), ↑j ≠ i
j : ι
hj✝ : j ∈ insert i s
hj : j ∈ s
⊢ (if hji : j = i then cast ⋯ a else g j ⋯) ∈ t j
Module: Mathlib.Data.List.Sigma

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

Tactic:
simp only [kextract]; split_ifs with h
    · subst a'
      simp [kerase]
    · simp [Ne.symm h, kextract_eq_dlookup_kerase a l, kerase]

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

Goal state before:
pp: m n k : ℕ
⊢ (∃ x x_1, (x ∣ m ∧ x_1 ∣ n ∧ x * x_1 = k) ∧ m ≠ 0 ∧ n ≠ 0) ↔ ∃ y x, (y ∣ m ∧ m ≠ 0) ∧ (x ∣ n ∧ n ≠ 0) ∧ y * x = k

Tactic:
simp only [and_assoc, and_comm, and_left_comm]

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

Goal state before:
pp: case h
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
a✝ : List (ι →₀ M)
⊢ (sum (Quot.mk (⇑(List.isSetoid (ι →₀ M))) a✝)).support ⊆
    (map Finsupp.support (Quot.mk (⇑(List.isSetoid (ι →₀ M))) a✝)).sup

Tactic:
simpa only [Multiset.quot_mk_to_coe'', Multiset.sum_coe, Multiset.map_coe, Multiset.sup_coe,
    List.foldr_map] using! List.support_sum_subset _

Goal state after:
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
ds : List ℕ
inst✝¹ : Mul α
inst✝ : AddMonoid α
n : ℕ
x y : Holor α ds
hx : CPRankMax 0 x
hy : CPRankMax n y
⊢ CPRankMax (0 + n) (0 + y)

Tactic:
simp only [zero_add, hy]

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

Goal state before:
pp: b : Bool
n : ℕ
⊢ (2 * ↑n + bif b then 1 else 0) = ↑(2 * n + b.toNat)

Tactic:
cases b <;> rfl

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

Goal state before:
pp: b : Bool
n : ℕ
⊢ (2 * -[n+1] + bif b then 1 else 0) = -[2 * n + (!b).toNat+1]

Tactic:
cases b <;> rfl

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 β
h_x_notin_s : x ∉ s
ih : (∀ x ∈ s, CPRankMax n (f x)) → CPRankMax (s.card * n) (∑ x ∈ s, f x)
h_cprank : ∀ x_1 ∈ insert x s, CPRankMax n (f x_1)
⊢ CPRankMax ((insert x s).card * n) (∑ x ∈ insert x s, f x)

Tactic:
simp only [Finset.sum_insert h_x_notin_s, Finset.card_insert_of_notMem h_x_notin_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
ih : (∀ x ∈ s, CPRankMax n (f x)) → CPRankMax (s.card * n) (∑ x ∈ s, f x)
h_cprank : ∀ x_1 ∈ insert x s, CPRankMax n (f x_1)
⊢ CPRankMax ((s.card + 1) * n) (f x + ∑ x ∈ s, f x)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case a
m n✝ k i n : ℕ
⊢ n ≤ n + i

Tactic:
apply Nat.le_add_right

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

Goal state before:
pp: case cons
α : Type u_1
p : α → Bool
head : α
tail : List α
ih : (dropWhile p tail).length ≤ tail.length
⊢ (dropWhile p (head :: tail)).length ≤ (head :: tail).length

Tactic:
simp only [dropWhile, length_cons]

Goal state after:
case cons
α : Type u_1
p : α → Bool
head : α
tail : List α
ih : (dropWhile p tail).length ≤ tail.length
⊢ (match p head with
      | true => dropWhile p tail
      | false => head :: tail).length ≤
    tail.length + 1
Module: Mathlib.Data.List.SplitLengths

Goal state before:
pp: α : Type u_1
l : List α
sz : List ℕ
i : ℕ
⊢ take i (sz.splitLengths l) = (take i sz).splitLengths l

Tactic:
by
  induction i generalizing sz l
  case zero => simp
  case succ i hi =>
    cases sz
    · simp
    · simp only [splitLengths_cons, take_succ_cons, hi]

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

Goal state before:
pp: α : Type u_1
r : α → α → Bool
l : List α
a : α
g : List α
gs : List (List α)
⊢ splitBy.loop r l a g gs = gs.reverse ++ splitBy.loop r l a g []

Tactic:
induction l generalizing a g gs with

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

Goal state before:
pp: case h_1
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α} {gs : List (List α)},
    ¬[] ∈ gs →
      IsChain (fun b a ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) gs →
        (∀ (m : List α), m ∈ gs.head? → ∃ ha hb, r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false) →
          IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) (splitBy.loop r l a g gs)
a : α
g : List α
gs : List (List α)
hgs' : ¬[] ∈ gs
hgs : IsChain (fun b a ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) gs
hga : ∀ (m : List α), m ∈ gs.head? → ∃ ha hb, r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false
x✝ : Bool
heq✝ : r a b = true
m : List α
hm : m ∈ gs.head?
ha : m ≠ []
w✝ : g.reverse ++ [a] ≠ []
H : r (m.getLast ha) ((g.reverse ++ [a]).head w✝) = false
⊢ ∃ ha hb, r (m.getLast ha) (((a :: g).reverse ++ [b]).head hb) = false

Tactic:
refine ⟨ha, append_ne_nil_of_right_ne_nil _ (cons_ne_nil _ _), ?_⟩

Goal state after:
case h_1
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α} {gs : List (List α)},
    ¬[] ∈ gs →
      IsChain (fun b a ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) gs →
        (∀ (m : List α), m ∈ gs.head? → ∃ ha hb, r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false) →
          IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) (splitBy.loop r l a g gs)
a : α
g : List α
gs : List (List α)
hgs' : ¬[] ∈ gs
hgs : IsChain (fun b a ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) gs
hga : ∀ (m : List α), m ∈ gs.head? → ∃ ha hb, r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false
x✝ : Bool
heq✝ : r a b = true
m : List α
hm : m ∈ gs.head?
ha : m ≠ []
w✝ : g.reverse ++ [a] ≠ []
H : r (m.getLast ha) ((g.reverse ++ [a]).head w✝) = false
⊢ r (m.getLast ha) (((a :: g).reverse ++ [b]).head ⋯) = false
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: case h_2.hga
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α} {gs : List (List α)},
    ¬[] ∈ gs →
      IsChain (fun b a ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) gs →
        (∀ (m : List α), m ∈ gs.head? → ∃ ha hb, r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false) →
          IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) (splitBy.loop r l a g gs)
a : α
g : List α
gs : List (List α)
hgs' : ¬[] ∈ gs
hgs : IsChain (fun b a ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) gs
hga : ∀ (m : List α), m ∈ gs.head? → ∃ ha hb, r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false
x✝ : Bool
heq✝ : r a b = false
⊢ ∀ (m : List α), m ∈ ((a :: g).reverse :: gs).head? → ∃ ha hb, r (m.getLast ha) (([].reverse ++ [b]).head hb) = false

Tactic:
· simpa

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

Goal state before:
pp: α : Type u_1
r : α → α → Bool
l : List α
a : α
g : List α
gs : List (List α)
hgs' : ¬[] ∈ gs
hgs : IsChain (fun b a ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) gs
hga : ∀ (m : List α), m ∈ gs.head? → ∃ ha hb, r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false
⊢ IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) (splitBy.loop r l a g gs)

Tactic:
induction l generalizing a g gs with

Goal state after:
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: case right
α : Type u_1
inst✝ : Preorder α
M N X Y : Multiset α
a : α
M_def : M = X + Y
N_def : N = X + {a}
ys_lt_a : ∀ (y : α), y ∈ Y → y < a
⊢ ∀ (y : α), y ∈ Y → ∃ z, z ∈ {a} ∧ y < z

Tactic:
· simpa

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

Goal state before:
pp: case cons.mpr
a b m : ℕ
l : List ℕ
ih : List.Pairwise Coprime l → (a ≡ b [MOD l.prod] ↔ ∀ (i : Fin l.length), a ≡ b [MOD l.get i])
co : List.Pairwise Coprime (m :: l)
this : m.Coprime l.prod
h : ∀ (i : Fin (l.length + 1)), a ≡ b [MOD (m :: l).get i]
⊢ a ≡ b [MOD m] ∧ ∀ (i : Fin l.length), a ≡ b [MOD l.get i]

Tactic:
exact ⟨h 0, fun i => h i.succ⟩

Goal state after:
Module: Mathlib.Data.Nat.Fib.Zeckendorf

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

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

Tactic:
· simpa

Goal state after:
n : ℕ
hn : n ≠ 0
⊢ n.greatestFib - 1 ≠ 0
Module: Mathlib.Data.Ordering.Lemmas

Goal state before:
pp: α : Type u
lt : α → α → Prop
inst✝¹ : DecidableRel lt
inst✝ : IsStrictOrder α lt
a b : α
⊢ cmpUsing lt a b = Ordering.gt ↔ lt b a

Tactic:
simp only [cmpUsing, Ordering.ite_eq_gt_distrib, if_false_right, and_true, if_false_left,
    and_iff_right_iff_imp, reduceCtorEq]
  exact fun hba hab ↦ (irrefl a) (_root_.trans hab hba)

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

Goal state before:
pp: case nil.node.nil.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
rx : α
rr : Ordnode α
size✝ : ℕ
l✝ : Ordnode α
rlx : α
r✝ : Ordnode α
⊢ Ordnode α

Tactic:
· exact node 3 (ι x) rlx ι rx

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

Goal state before:
pp: case nil.node.node.nil
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
⊢ Ordnode α

pp: case nil.node.node.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ Ordnode α

Tactic:
· exact node 3 (ι x) rlx ι rx

Goal state after:
case nil.node.node.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ Ordnode α
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
⊢ ↑↑(neg p) = ↑(neg p)

Tactic:
cast_neg,

Goal state after:
α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
⊢ ↑(-↑p) = ↑(neg p)
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
⊢ ↑(-↑p) = ↑(neg p)

Tactic:
cast_neg,

Goal state after:
α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
⊢ ↑(-↑p) = -↑p
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
⊢ ↑(neg p.bit0) = ↑(neg p) + ↑(neg p)

Tactic:
cast_neg,

Goal state after:
α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
⊢ -↑p.bit0 = ↑(neg p) + ↑(neg p)
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
⊢ -↑p.bit0 = ↑(neg p) + ↑(neg p)

Tactic:
cast_neg,

Goal state after:
α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
⊢ -↑p.bit0 = -↑p + -↑p
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
⊢ ↑(neg (Num.casesOn p.pred' 1 bit1)) = ↑(neg p) + ↑(neg p) + 1

Tactic:
cast_neg,

Goal state after:
α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
⊢ -↑(Num.casesOn p.pred' 1 bit1) = ↑(neg p) + ↑(neg p) + 1
Module: Mathlib.Data.PFunctor.Univariate.Basic

Goal state before:
pp: P : PFunctor.{uA, uB}
α : Type v₁
β : Type v₂
x : ↑P α
f : α → β
⊢ (P.map f x).fst = x.fst

Tactic:
cases x; rfl

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

Goal state before:
pp: n : PosNum
⊢ ↑n = ↑↑n.pred' + 1

Tactic:
rw [← n.to_nat_to_int, to_nat_eq_succ_pred]

Goal state after:
n : PosNum
⊢ ↑(↑n.pred' + 1) = ↑↑n.pred' + 1
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: ⊢ ofInt' ↑0 = 0

Tactic:
dsimp [ofInt', cast_zero]
    simp only [Num.ofNat'_zero, Num.toZNum]

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

Goal state before:
pp: a : PosNum
⊢ ofInt' ↑(neg a) = neg a

Tactic:
cast_neg,

Goal state after:
a : PosNum
⊢ ofInt' (-↑a) = neg a
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: 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

Tactic:
simp +contextual

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

Goal state before:
pp: F : PFunctor.{uA, uB}
n : ℕ
x : CofixA F (n + 1)
⊢ x = CofixA.intro (head' x) (children' x)

Tactic:
cases x; rfl

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

Goal state before:
pp: n : PosNum
d : ZNum
⊢ ↑↑d.abs - ↑(n.pred' % d.abs).succ = ↑(neg n) % ↑d

Tactic:
cast_neg,

Goal state after:
n : PosNum
d : ZNum
⊢ ↑↑d.abs - ↑(n.pred' % d.abs).succ = -↑n % ↑d