mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Category.Stonean.Basic

Goal state before:
pp: case mp
X : CompHaus
⊢ Projective X → ExtremallyDisconnected ↑X.toTop

pp: case mpr
X : CompHaus
⊢ ExtremallyDisconnected ↑X.toTop → Projective X

Tactic:
· intro h
    change ExtremallyDisconnected X.toStonean
    infer_instance

Goal state after:
case mpr
X : CompHaus
⊢ ExtremallyDisconnected ↑X.toTop → Projective X
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case case.succ
f g : Code
IHf :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepNormal f k v) b₂ ∧
        Reaches₁ (TM2.step tr)
          { l := some (trNormal f (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) } b₂
IHg :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepNormal g k v) b₂ ∧
        Reaches₁ (TM2.step tr)
          { l := some (trNormal g (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) } b₂
k : Cont
v : List ℕ
s s' : Option Γ'
n : ℕ
h :
  Reaches₁ (TM2.step tr)
    { l := some ((trNormal f (trCont k)).pred (trNormal g (trCont k))), var := s,
      stk := elim (trList v) [] [] (trContStack k) }
    (Nat.rec { l := some (trNormal f (trCont k)), var := s', stk := elim (trList v.tail) [] [] (trContStack k) }
      (fun n x ↦
        { l := some (trNormal g (trCont k)), var := s', stk := elim (trList (n :: v.tail)) [] [] (trContStack k) })
      (n + 1))
⊢ ∃ b₂,
    TrCfg (Nat.rec (stepNormal f k v.tail) (fun y x ↦ stepNormal g k (y :: v.tail)) (n + 1)) b₂ ∧
      Reaches₁ (TM2.step tr)
        { l := some (trNormal (f.case g) (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) } b₂

Tactic:
obtain ⟨c, h₁, h₂⟩ := IHg k _ s'
      exact ⟨_, h₁, h.trans h₂⟩

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

Goal state before:
pp: case mp
X Y : LightProfinite
f : X ⟶ Y
⊢ Epi f → Function.Surjective ⇑(ConcreteCategory.hom f)

Tactic:
dsimp [Function.Surjective]
    contrapose!
    rintro ⟨y, hy⟩ hf
    let C := Set.range f
    have hC : IsClosed C := (isCompact_range f.hom.hom.continuous).isClosed
    let U := Cᶜ
    have hyU : y ∈ U := by
      refine Set.mem_compl ?_
      rintro ⟨y', hy'⟩
      exact hy y' hy'
    have hUy : U ∈ 𝓝 y := hC.compl_mem_nhds hyU
    obtain ⟨V, hV, hyV, hVU⟩ := isTopologicalBasis_isClopen.mem_nhds_iff.mp hUy
    classical
      let Z := of (ULift.{u} <| Fin 2)
      let g : Y ⟶ Z := CompHausLike.ofHom _
        ⟨(LocallyConstant.ofIsClopen hV).map ULift.up, LocallyConstant.continuous _⟩
      let h : Y ⟶ Z := CompHausLike.ofHom _ ⟨fun _ => ⟨1⟩, continuous_const⟩
      have H : h = g := by
        rw [← cancel_epi f]
        ext x
        dsimp [g, LocallyConstant.ofIsClopen]
        rw [ContinuousMap.coe_mk, ContinuousMap.coe_mk, hom_ofHom, ContinuousMap.coe_mk,
          Function.comp_apply, if_neg]
        refine mt (fun α => hVU α) ?_
        simp [U, C]
      apply_fun fun e => (e y).down at H
      dsimp [g, LocallyConstant.ofIsClopen] at H
      rw [ContinuousMap.coe_mk, ContinuousMap.coe_mk, Function.comp_apply, if_pos hyV] at H
      exact top_ne_bot H

Goal state after:
Module: Mathlib.Topology.Category.Profinite.CofilteredLimit

Goal state before:
pp: case e'_3
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) α
S : DiscreteQuotient ↑C.pt.toTop := f.discreteQuotient
ff : Quotient S.toSetoid → α := ⇑f.lift
h✝ : IsEmpty (Quotient S.toSetoid)
this : ∃ j, IsEmpty ↑(F.obj j).toTop
j : J
hj : IsEmpty ↑(F.obj j).toTop
A : Set α
x : ↑(F.obj j).toTop
⊢ x ∈ (fun a ↦ hj.elim a) ⁻¹' A ↔ x ∈ ∅

Tactic:
exact hj.elim x

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

Goal state before:
pp: X Y : LightCondSet
f : X ⟶ Y
⊢ Continuous ⇑(ConcreteCategory.hom (f.hom.app (Opposite.op (of PUnit.{u + 1}))))

Tactic:
rw [continuous_coinduced_dom]

Goal state after:
X Y : LightCondSet
f : X ⟶ Y
⊢ Continuous (⇑(ConcreteCategory.hom (f.hom.app (Opposite.op (of PUnit.{u + 1})))) ∘ LightCondSet.coinducingCoprod✝ X)
Module: Mathlib.Condensed.Light.TopCatAdjunction

Goal state before:
pp: X✝ Y : LightCondSet
f : X✝ ⟶ Y
X : TopCat
⊢ Continuous fun x ↦ x.toFun PUnit.unit

Tactic:
rw [continuous_coinduced_dom]

Goal state after:
X✝ Y : LightCondSet
f : X✝ ⟶ Y
X : TopCat
⊢ Continuous ((fun x ↦ x.toFun PUnit.unit) ∘ LightCondSet.coinducingCoprod✝ X.toLightCondSet)
Module: Mathlib.Condensed.Light.InternallyProjective

Goal state before:
pp: case refine_2
R : Type u
inst✝ : CommRing R
P : LightCondSet
h :
  ∀ {A B : LightCondMod R} (e : A ⟶ B) [Epi e] (S : LightProfinite) (g : (free R).obj (S.toCondensed ⊗ P) ⟶ B),
    ∃ S' π,
      ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
        ∃ g', (free R).map (lightProfiniteToLightCondSet.map π ▷ P) ≫ g = g' ≫ e
A B : LightCondMod R
e : A ⟶ B
he : Epi e
S : LightProfinite
g : (free R).obj S.toCondensed ⊗ (free R).obj P ⟶ B
⊢ ∃ S' π,
    ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
      ∃ g', (lightProfiniteToLightCondSet ⋙ free R).map π ▷ (free R).obj P ≫ g = g' ≫ e

Tactic:
· specialize h e S ((μIso (free R) _ _).inv ≫ g)
    obtain ⟨S', π, hπ, g', hh⟩ := h
    refine ⟨S', π, hπ, (μIso (free R) _ _).hom ≫ g', ?_⟩
    rw [assoc, ← hh, ← assoc, ← assoc]
    -- Generated by `simp? [← μ_natural_left]`
    -- Leaving it unsqueezed is too slow.
    simp only [comp_obj, Functor.comp_map, μIso_hom, ← μ_natural_left, μIso_inv, assoc, μ_δ,
      comp_id]

Goal state after:
Module: Mathlib.Condensed.TopCatAdjunction

Goal state before:
pp: X Y : CondensedSet
f : X ⟶ Y
⊢ Continuous ⇑(ConcreteCategory.hom (f.hom.app (Opposite.op (of PUnit.{u + 1}))))

Tactic:
rw [continuous_coinduced_dom]

Goal state after:
X Y : CondensedSet
f : X ⟶ Y
⊢ Continuous (⇑(ConcreteCategory.hom (f.hom.app (Opposite.op (of PUnit.{u + 1})))) ∘ CondensedSet.coinducingCoprod✝ X)
Module: Mathlib.Condensed.TopCatAdjunction

Goal state before:
pp: X✝ : CondensedSet
X : TopCat
⊢ Continuous fun x ↦ x.toFun PUnit.unit

Tactic:
rw [continuous_coinduced_dom]

Goal state after:
X✝ : CondensedSet
X : TopCat
⊢ Continuous ((fun x ↦ x.toFun PUnit.unit) ∘ CondensedSet.coinducingCoprod✝ X.toCondensedSet)
Module: Mathlib.Condensed.TopCatAdjunction

Goal state before:
pp: X✝ X : CondensedSet
Y : Type (u + 1)
tY✝ : TopologicalSpace Y
f : ↑X.toTopCat → Y
h : ∀ (S : CompHaus) (g : C(↑S.toTop, ↑X.toTopCat)), Continuous (f ∘ ⇑g)
⊢ Continuous f

Tactic:
continuous_coinduced_dom,

Goal state after:
X✝ X : CondensedSet
Y : Type (u + 1)
tY✝ : TopologicalSpace Y
f : ↑X.toTopCat → Y
h : ∀ (S : CompHaus) (g : C(↑S.toTop, ↑X.toTopCat)), Continuous (f ∘ ⇑g)
⊢ Continuous (f ∘ X.coinducingCoprod)
Module: Mathlib.Control.Fix

Goal state before:
pp: α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i ↦ (Fix.approx f i x).Dom
k : ℕ
⊢ p (k + ↑Upto.zero) → Nat.find h' = k + ↑Upto.zero → ⋯.fix (fixAux f) Upto.zero x = Fix.approx f (k + 1) x

Tactic:
generalize Upto.zero = z

Goal state after:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i ↦ (Fix.approx f i x).Dom
k : ℕ
z : Upto p
⊢ p (k + ↑z) → Nat.find h' = k + ↑z → ⋯.fix (fixAux f) z x = Fix.approx f (k + 1) x
Module: Mathlib.Control.Fix

Goal state before:
pp: α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
⊢ Part.fix f x = Fix.approx f (Nat.find h').succ x

Tactic:
by
  let p := fun i : ℕ => (Fix.approx f i x).Dom
  have : p (Nat.find h') := Nat.find_spec h'
  generalize hk : Nat.find h' = k
  replace hk : Nat.find h' = k + (@Upto.zero p).val := hk
  rw [hk] at this
  revert hk
  dsimp [Part.fix]; rw [assert_pos h']; revert this
  generalize Upto.zero = z; intro _this hk
  suffices ∀ x' hwf,
    WellFounded.fix hwf (fixAux f) z x' = Fix.approx f (succ k) x'
    from this _ _
  induction k generalizing z with
  | zero =>
    intro x' _
    rw [Fix.approx, WellFounded.fix_eq, fixAux]
    congr
    ext x : 1
    rw [assert_neg]
    · rfl
    · rw [Nat.zero_add] at _this
      simpa only [not_not, Coe]
  | succ n n_ih =>
    intro x' _
    rw [Fix.approx, WellFounded.fix_eq, fixAux]
    congr
    ext : 1
    have hh : ¬(Fix.approx f z.val x).Dom := by
      apply Nat.find_min h'
      lia
    rw [succ_add_eq_add_succ] at _this hk
    rw [assert_pos hh, n_ih (Upto.succ z hh) _this hk]

Goal state after:
Module: Mathlib.Control.Functor.Multivariate

Goal state before:
pp: case h₀
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
P : β → Prop
x✝ : F (α ::: β)
i : Fin2 (n + 1)
x : (α ::: β) i
property✝ : α.PredLast P x
⊢ ↑((f P n α ⊚ g P n α) i ⟨x, property✝⟩) = ↑(TypeVec.id i ⟨x, property✝⟩)

Tactic:
cases i <;> rfl

Goal state after:
Module: Mathlib.Control.Functor.Multivariate

Goal state before:
pp: case h₁
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
P : β → Prop
x✝ : F (α ::: β)
u✝ : F fun i ↦ { p_1 // ofRepeat (α.PredLast' P i p_1) }
i : Fin2 (n + 1)
x : (α ::: β) i
property✝ : ofRepeat (α.PredLast' P i x)
⊢ ↑⟨x, property✝⟩ = ↑(f P n α i ⟨x, property✝⟩)

Tactic:
cases i <;> rfl

Goal state after:
Module: Mathlib.Control.Functor.Multivariate

Goal state before:
pp: case h₀
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
rr : β → β → Prop
x✝ y : F (α ::: β)
i : Fin2 (n + 1)
x : (α ::: β) i × (α ::: β) i
property✝ : α.RelLast rr x.1 x.2
⊢ (f' rr n α ⊚ g' rr n α) i ⟨x, property✝⟩ = TypeVec.id i ⟨x, property✝⟩

Tactic:
cases i <;> rfl

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
α : TypeVec.{u_1} (n + 1)
i : Fin2 (n + 1)
⊢ (α.drop ::: α.last) i = α i

Tactic:
cases i <;> rfl

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: β : Type u_1
γ : Type u_2
x : γ
n : ℕ
α : TypeVec.{u_1} n
i : Fin2 (n + 1)
⊢ TypeVec.const x (α ::: β) i = (TypeVec.const x α ::: fun x_1 ↦ x) i

Tactic:
cases i <;> rfl

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

Goal state before:
pp: m : Type u → Type v
m₁ : Type u₀ → Type v₀
m₂ : Type u₁ → Type v₁
α₁ r₁ : Type u₀
α₂ r₂ : Type u₁
F : m₁ r₁ ≃ m₂ r₂
G : α₁ ≃ α₂
f : ContT r₁ m₁ α₁
⊢ (fun f r ↦ F.symm (f fun x ↦ F (r (G.symm x)))) ((fun f r ↦ F (f fun x ↦ F.symm (r (G x)))) f) = f

Tactic:
by funext r; simp

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

Goal state before:
pp: m : Type u → Type v
m₁ : Type u₀ → Type v₀
m₂ : Type u₁ → Type v₁
α₁ r₁ : Type u₀
α₂ r₂ : Type u₁
F : m₁ r₁ ≃ m₂ r₂
G : α₁ ≃ α₂
f : ContT r₂ m₂ α₂
⊢ (fun f r ↦ F (f fun x ↦ F.symm (r (G x)))) ((fun f r ↦ F.symm (f fun x ↦ F (r (G.symm x)))) f) = f

Tactic:
by funext r; simp

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

Goal state before:
pp: case refine_2
S : Type u_1
T : Type u_2
X : Type u_3
inst✝⁵ : TopologicalSpace S
inst✝⁴ : TopologicalSpace T
inst✝³ : TopologicalSpace X
inst✝² : DiscreteTopology X
inst✝¹ : T2Space T
inst✝ : CompactSpace S
π : T → S × OnePoint X
hπ : Continuous π
σ : Option X → S → T
hσ : ∀ (x : Option X), Continuous (σ x)
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
i : X
⊢ IsOpen (Prod.snd ∘ π ⁻¹' {↑i})

Tactic:
· exact .preimage (continuous_snd.comp hπ) ⟨fun h ↦ by simp_all, by simp⟩

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

Goal state before:
pp: case neg
S : Type u_1
T : Type u_2
X : Type u_3
π : T → S × Option X
σ : Option X → S → T
hσ : ∀ (x : Option X) (s : S), (π (σ x s)).1 = s
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
t : T
ht : t ∈ fibres π σ
t' : T
ht' : t' ∈ fibres π σ
property✝ : π_r π σ (⟨t, ht⟩, ⟨t', ht'⟩).1 = π_r π σ (⟨t, ht⟩, ⟨t', ht'⟩).2
h : ¬(π t).2 = none
⊢ ∃ a, coverToFun (fibreIncl π σ) (π_r π σ) a = ⟨(⟨t, ht⟩, ⟨t', ht'⟩), property✝⟩

Tactic:
obtain ⟨n, hn⟩ := Option.ne_none_iff_exists'.mp h
    exact ⟨Sum.inl ⟨σ n (π t).1, by grind⟩, by grind⟩

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Embedding

Goal state before:
pp: case neg
α : Type u_1
x✝ : ↑{(a, b) | a ≠ b}
a b : α
h : (a, b) ∈ {(a, b) | a ≠ b}
i j : Fin 2
hij : (fun i ↦ if i = 0 then a else b) i = (fun i ↦ if i = 0 then a else b) j
hi : ¬i = 0
⊢ i = j

Tactic:
eq_one_of_ne_zero i hi

Goal state after:
case neg
α : Type u_1
x✝ : ↑{(a, b) | a ≠ b}
a b : α
h : (a, b) ∈ {(a, b) | a ≠ b}
i j : Fin 2
hij : (fun i ↦ if i = 0 then a else b) 1 = (fun i ↦ if i = 0 then a else b) j
hi : ¬i = 0
⊢ 1 = j
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
l₁ l₂ : List (Sigma β)
s : Sigma β
⊢ (l₁ ++ s :: l₂).NodupKeys ↔ (s :: (l₁ ++ l₂)).NodupKeys

Tactic:
simp_all [NodupKeys, keys, nodup_middle]

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s : Finmap β
h : lookup a s = some b
x : α
h' : ¬x = a
this : x ∉ singleton a b
⊢ lookup x (erase a s ∪ singleton a b) = lookup x s

Tactic:
lookup_union_left_of_not_in this,

Goal state after:
case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s : Finmap β
h : lookup a s = some b
x : α
h' : ¬x = a
this : x ∉ singleton a b
⊢ lookup x (erase a s) = lookup x s
Module: Mathlib.Data.List.Sigma

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

Tactic:
by cases hd; rfl

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

Goal state before:
pp: case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
h : ¬a = a'
x : Sigma β
xs : List (Sigma β)
tail_ih✝ : kerase a (kerase a' xs) = kerase a' (kerase a xs)
h✝ : ¬a' = x.fst
h' : a = x.fst
⊢ kerase a (kerase a' (x :: xs)) = kerase a' (kerase a (x :: xs))

Tactic:
subst a
      simp [kerase_cons_eq rfl, kerase_cons_ne (Ne.symm h)]

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

Goal state before:
pp: m n : ℕ
⊢ (m * n).divisors = m.divisors * n.divisors

Tactic:
ext k
  simp_rw [mem_mul, mem_divisors, Nat.dvd_mul, mul_ne_zero_iff, ← exists_and_left,
    ← exists_and_right]
  simp only [and_assoc, and_comm, and_left_comm]

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

Goal state before:
pp: case pos
κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst✝¹ : Zero M
inst✝ : DecidableEq κ
k : κ
i : ι k
f : ι ⟨k, i⟩.fst →₀ M
⊢ (embDomain { toFun := Sigma.mk k, inj' := ⋯ } f) ⟨k, i⟩ = f i

Tactic:
apply embDomain_apply_self

Goal state after:
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
ds₁ ds₂ ds₃ : List ℕ
inst✝ : Semigroup α
x : Holor α ds₁
y : Holor α ds₂
z : Holor α ds₃
t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)
⊢ x t.take.take * y t.take.drop * z t.drop = cast ⋯ (fun t ↦ x t.take * (y t.drop.take * z t.drop.drop)) t

Tactic:
rw [mul_assoc, ← HolorIndex.take_take, ← HolorIndex.drop_take, ← HolorIndex.drop_drop,
      cast_type]

Goal state after:
α : Type
ds₁ ds₂ ds₃ : List ℕ
inst✝ : Semigroup α
x : Holor α ds₁
y : Holor α ds₂
z : Holor α ds₃
t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)
⊢ x t.assocRight.take * (y t.assocRight.drop.take * z t.assocRight.drop.drop) =
    (fun t ↦ x (cast ⋯ t).take * (y (cast ⋯ t).drop.take * z (cast ⋯ t).drop.drop)) t

case eq
α : Type
ds₁ ds₂ ds₃ : List ℕ
inst✝ : Semigroup α
x : Holor α ds₁
y : Holor α ds₂
z : Holor α ds₃
t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)
⊢ ds₁ ++ (ds₂ ++ ds₃) = ds₁ ++ ds₂ ++ ds₃
Module: Mathlib.Data.Holor

Goal state before:
pp: case h₁
α : Type
d : ℕ
ds : List ℕ
inst✝ : Semiring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
⊢ ⟨i, ⋯⟩ ∉ (Finset.range d).attach → (if i = ↑⟨i, ⋯⟩ then x.slice ↑⟨i, ⋯⟩ ⋯ else 0) = 0

Tactic:
intro (hid' : Subtype.mk i _ ∉ Finset.attach (Finset.range d))
    exfalso
    exact absurd (Finset.mem_attach _ _) hid'

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

Goal state before:
pp: ⊢ bitwise xor = Int.xor

Tactic:
funext m n
  rcases m with m | m <;> rcases n with n | n <;> try {rfl}
    <;> simp only [bitwise, natBitwise, Bool.not_false, Bool.bne_eq_xor,
      cond_false, cond_true, negSucc.injEq, Bool.false_xor,
      Bool.true_xor, Bool.not_true,
      Int.xor, HXor.hXor, XorOp.xor, Nat.xor] <;> simp

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

Goal state before:
pp: f : Bool → Bool → Bool
m n : ℤ
k : ℕ
⊢ (bitwise f m n).testBit k = f (m.testBit k) (n.testBit k)

Tactic:
cases m <;> cases n

Goal state after:
case ofNat.ofNat
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
⊢ (bitwise f (ofNat a✝¹) (ofNat a✝)).testBit k = f ((ofNat a✝¹).testBit k) ((ofNat a✝).testBit k)

case ofNat.negSucc
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
⊢ (bitwise f (ofNat a✝¹) -[a✝+1]).testBit k = f ((ofNat a✝¹).testBit k) (-[a✝+1].testBit k)

case negSucc.ofNat
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
⊢ (bitwise f -[a✝¹+1] (ofNat a✝)).testBit k = f (-[a✝¹+1].testBit k) ((ofNat a✝).testBit k)

case negSucc.negSucc
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
⊢ (bitwise f -[a✝¹+1] -[a✝+1]).testBit k = f (-[a✝¹+1].testBit k) (-[a✝+1].testBit k)
Module: Mathlib.Data.Int.CardIntervalMod

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

Tactic:
neg_lt_neg_iff,

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

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

Tactic:
have phh' : ¬(p head = true) := by simp [phh.symm]

Goal state after:
case false
α : Type u_1
p : α → Bool
l : List α
head : α
tail : List α
hi : find? p tail = (dropWhile (fun x ↦ !p x) tail).head?
phh : false = p head
phh' : ¬p head = true
⊢ find? p (head :: tail) = (dropWhile (fun x ↦ !p x) (head :: tail)).head?
Module: Mathlib.Data.List.DropRight

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

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

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : Option α → β → γ
as : List α
bs : List β
⊢ map₂Right f as bs = (map₂Right' f as bs).fst

Tactic:
simp only [map₂Right, map₂Right', map₂Left_eq_map₂Left']

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

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

Tactic:
min_eq_right hlm,

Goal state after:
case inr
n m l : ℕ
hlm : l ≤ m
⊢ filter (fun x ↦ decide (x < l)) (Ico n m) = Ico n l
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: case h.a
α : Type u_1
r : α → α → Bool
l m : List α
ha : ∀ (x : α), x ∈ l.getLast? → ∀ (y : α), y ∈ m.head? → r x y = false
hl : l ≠ []
hm : m ≠ []
x : List α
hx : x ∈ (splitBy r l).getLast?
y : List α
hy : y ∈ (splitBy r m).head?
⊢ x.getLast ⋯ ∈ l.getLast?

Tactic:
← getLast_of_mem_getLast? hx,

Goal state after:
case h.a
α : Type u_1
r : α → α → Bool
l m : List α
ha : ∀ (x : α), x ∈ l.getLast? → ∀ (y : α), y ∈ m.head? → r x y = false
hl : l ≠ []
hm : m ≠ []
x : List α
hx : x ∈ (splitBy r l).getLast?
y : List α
hy : y ∈ (splitBy r m).head?
⊢ ((splitBy r l).getLast ⋯).getLast ⋯ ∈ l.getLast?
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
⊢ Function.Injective2 fromRows

Tactic:
intro x1 x2 y1 y2
  simp [← Matrix.ext_iff]

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
ha : Acc LT.lt a
⊢ ∀ {M : Multiset α}, Acc OneStep M → Acc OneStep (a ::ₘ M)

Tactic:
induction ha with | _ a _ ha
   =>  _ 

Goal state after:
case intro
α : Type u_1
inst✝ : Preorder α
a✝ a : α
h✝ : ∀ (y : α), y < a → Acc LT.lt y
ha : ∀ (y : α), y < a → ∀ {M : Multiset α}, Acc OneStep M → Acc OneStep (y ::ₘ M)
⊢ ∀ {M : Multiset α}, Acc OneStep M → Acc OneStep (a ::ₘ M)
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
x : ℕ
h : p x
⊢ ∃ n, (∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset) ∧ nth p n = x

Tactic:
by
  refine (Set.ofPred p).finite_or_infinite.elim (fun hf => ?_) fun hf => ?_
  · rcases exists_lt_card_finite_nth_eq hf h with ⟨n, hn, hx⟩
    exact ⟨n, fun _ => hn, hx⟩
  · rw [← @Set.mem_ofPred_eq _ _ p, ← range_nth_of_infinite hf] at h
    rcases h with ⟨n, hx⟩
    exact ⟨n, fun hf' => absurd hf' hf, hx⟩

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

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

Tactic:
rw [succ, Num.zneg_toZNumNeg]

Goal state after:
case neg
a✝ : PosNum
⊢ a✝.pred'.toZNum = (-neg a✝).pred
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: p : PosNum
⊢ (ZNum.pos p).pred.succ = ZNum.pos p

Tactic:
rw [ZNum.pred, ← toZNum_succ, Num.succ, PosNum.succ'_pred', toZNum]

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

Goal state before:
pp: case pos.succ.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✝¹ n✝ : ℕ
mm : n✝¹ + 1 + (n✝ + 1) ≤ 1
⊢ BalancedSz 1 (n✝¹ + 1) ∧ BalancedSz (n✝ + 1) 1 ∧ BalancedSz (1 + (n✝¹ + 1) + 1) (n✝ + 1 + 1 + 1)

Tactic:
· rw [Nat.succ_add] at mm; rcases mm with (_ | ⟨⟨⟩⟩)

Goal state after: