mathlib-initiative/mathlib-tactics huggingface dataset:
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:
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.Traversable.Instances

Goal state before:
pp: σ : Type u
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative G
inst✝ : LawfulApplicative F
η : ApplicativeTransformation F G
α : Type u_1
β : Type u
f : α → F β
x : σ ⊕ α
⊢ (fun {α} ↦ η.app α) (Sum.traverse f x) = Sum.traverse ((fun {α} ↦ η.app α) ∘ f) x

Tactic:
cases x <;> simp! [Sum.traverse, functor_norm]

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
⊢ Part.fix (⇑f) x ≤ approx (⇑f) i x

Tactic:
intro b'

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
⊢ b' ∈ Part.fix (⇑f) x → b' ∈ approx (⇑f) i x
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: case neg
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
hh : ∀ (i : ℕ) (b : β x), b ∉ approx (⇑f) i x
⊢ Part.fix (⇑f) x ≤ approx (⇑f) 0 x

Tactic:
intro b'

Goal state after:
case neg
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
hh : ∀ (i : ℕ) (b : β x), b ∉ approx (⇑f) i x
b' : β x
⊢ b' ∈ Part.fix (⇑f) x → b' ∈ approx (⇑f) 0 x
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: case refine_2
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)).2 = x
x : T
x✝ : ∃ i, (∀ (x_1 : S), ¬σ (Option.some i) x_1 = x) ∧ (π x).2 = ↑i
n : X
hn : ∀ (x_1 : S), ¬σ (Option.some n) x_1 = x
hn' : (π x).2 = ↑n
⊢ ¬(π x).2 = none ∧ ∀ (x_1 : X) (x_2 : S), ¬σ (Option.some x_1) x_2 = x

Tactic:
refine ⟨by simpa [hn'] using Option.isSome_iff_ne_none.mp rfl, fun i s h ↦ hn s ?_⟩
    rw [← h, hσ'] at hn'
    rw [← h, Option.some_injective _ hn'.symm]

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: case fz
n n✝ : ℕ
α : TypeVec.{u} (n✝ + 1)
x : α Fin2.fz
⊢ (subtypeVal α.repeatEq ⊚ diagSub) Fin2.fz x = prod.diag Fin2.fz x

Tactic:
simp only [comp, subtypeVal, diagSub, prod.diag]

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: case fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ : ∀ {α : TypeVec.{u_1} n✝} (p : α ⟹ «repeat» n✝ Prop) (x : Subtype_ p a✝), toSubtype p a✝ (ofSubtype p a✝ x) = x
α : TypeVec.{u_1} (n✝ + 1)
p : α ⟹ «repeat» (n✝ + 1) Prop
x : Subtype_ p a✝.fs
⊢ toSubtype (dropFun p) a✝ (ofSubtype (dropFun p) a✝ x) = x

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: case fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ :
  ∀ {α : TypeVec.{u_1} n✝} (p : α ⟹ «repeat» n✝ Prop) (x : { x // ofRepeat (p a✝ x) }),
    subtypeVal p a✝ (toSubtype p a✝ x) = ↑x
α : TypeVec.{u_1} (n✝ + 1)
p : α ⟹ «repeat» (n✝ + 1) Prop
x : { x // ofRepeat (p a✝.fs x) }
⊢ subtypeVal (dropFun p) a✝ (toSubtype (dropFun p) a✝ x) = ↑x

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Control.Traversable.Equiv

Goal state before:
pp: t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
α : Type u
x : t' α
⊢ Equiv.traverse eqv pure x = pure x

Tactic:
rw [Equiv.traverse, id_traverse, map_pure, apply_symm_apply]

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: case fz
n n✝ : ℕ
α : TypeVec.{u_1} (n✝ + 1)
r : α ⊗ α ⟹ «repeat» (n✝ + 1) Prop
x : Subtype_ r Fin2.fz
⊢ ⟨↑x, ⋯⟩ = x

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: case fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ :
  ∀ {α : TypeVec.{u_1} n✝} (r : α ⊗ α ⟹ «repeat» n✝ Prop) (x : Subtype_ r a✝), toSubtype' r a✝ (ofSubtype' r a✝ x) = x
α : TypeVec.{u_1} (n✝ + 1)
r : α ⊗ α ⟹ «repeat» (n✝ + 1) Prop
x : Subtype_ r a✝.fs
⊢ toSubtype' (dropFun r) a✝ (ofSubtype' (dropFun r) a✝ x) = x

Tactic:
simp [*]

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 π
s : S
p : S → OnePoint X → T := fun s n ↦ ⋯.choose
hp : ∀ (s : S) (n : OnePoint X), π (p s n) = (s, n)
⊢ ∃ a, y π a = s

Tactic:
exact ⟨⟨fun n ↦ ⟨p s n, by grind⟩, by grind⟩, by grind⟩

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: case fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ :
  ∀ {α : TypeVec.{u_1} n✝} (r : α ⊗ α ⟹ «repeat» n✝ Prop) (x : { x // ofRepeat (r a✝ (prod.mk a✝ x.1 x.2)) }),
    subtypeVal r a✝ (toSubtype' r a✝ x) = prod.mk a✝ (↑x).1 (↑x).2
α : TypeVec.{u_1} (n✝ + 1)
r : α ⊗ α ⟹ «repeat» (n✝ + 1) Prop
x : { x // ofRepeat (r a✝.fs (prod.mk a✝.fs x.1 x.2)) }
⊢ subtypeVal (dropFun r) a✝ (toSubtype' (dropFun r) a✝ x) = prod.mk a✝ (↑x).1 (↑x).2

Tactic:
simp [*]

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

Goal state before:
pp: α : Type u_1
T : TopologicalSpace α
F : Realizer α
⊢ TopologicalSpace.IsTopologicalBasis (range F.F.f)

Tactic:
have := toTopsp_isTopologicalBasis F.F; rwa [F.eq] at this

Goal state after:
Module: Mathlib.Data.FP.Basic

Goal state before:
pp: C : FloatCfg
n d : ℕ+
e₁ : ℤ := ↑(↑n).size - ↑(↑d).size - ↑prec
d₁ n₁ : ℕ
e₂ : ℤ := if n₁ < d₁ then e₁ - 1 else e₁
e₃ : ℤ := max e₂ emin
⊢ Float × Bool

Tactic:
obtain ⟨d₂, n₂⟩ := Int.shift2 d.1 n.1 (e₃ + prec)

Goal state after:
C : FloatCfg
n d : ℕ+
e₁ : ℤ := ↑(↑n).size - ↑(↑d).size - ↑prec
d₁ n₁ : ℕ
e₂ : ℤ := if n₁ < d₁ then e₁ - 1 else e₁
e₃ : ℤ := max e₂ emin
d₂ n₂ : ℕ
⊢ Float × Bool
Module: Mathlib.Data.Semiquot

Goal state before:
pp: α : Type u_1
s t : Semiquot α
h : t.IsPure
st : s ≤ t
⊢ pure (t.get h) ≤ pure (s.get ⋯)

Tactic:
simpa using h _ (get_mem _) _ (st <| get_mem _)

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
xs : List α
h : ∀ (x : α), x ∈ xs
⊢ ∀ (x : α), x ∈ xs.dedup

Tactic:
simp [*]

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

Goal state before:
pp: case pos
R : Type
inst✝ : CommRing R
X Y : LightCondMod R
p : X ⟶ Y
hp : Epi p
S : LightProfinite
f : (free R).obj (S ⊗ ℕ∪{∞}).toCondensed ⟶ Y
T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
g : (free R).obj T.toCondensed ⟶ X
hπ : Epi π
comm : (lightProfiniteToLightCondSet ⋙ free R).map π ≫ f = g ≫ p
S' T' : LightProfinite
y' : S' ⟶ S
π' : T' ⟶ S' ⊗ ℕ∪{∞}
g' : T' ⟶ T
hπ'✝ : Epi π'
hy' : Epi y'
comp : π' ≫ y' ▷ ℕ∪{∞} = g' ≫ π
epi : Epi (cover π')
split : SplitEpi (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π' ≫ fst S' ℕ∪{∞})
hS' : Nonempty ↑S'.toTop
this✝¹ : Mono (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}))
this✝ : Nonempty ↑(LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞})).toTop
r_inf : T' ⟶ LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞})
hr : LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ r_inf = 𝟙 (LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞}))
hπ'' : RegularEpi (lightProfiniteToLightCondSet.map π') := regularEpiOfEpi (lightProfiniteToLightCondSet.map π')
this : EffectiveEpi π'
hπ' : RegularEpi (lightProfiniteToLightCondSet.map π') :=
  regularEpiOfPreserves π' lightProfiniteToLightCondSet (pullback.cone π' π') (pullback.isLimit π' π')
hc : Limits.IsColimit ((free R).mapCocone (Limits.Cofork.ofπ (lightProfiniteToLightCondSet.map π') ⋯))
⊢ ∃ g', (free R).map (lightProfiniteToLightCondSet.map (y' ▷ ℕ∪{∞})) ≫ f = g' ≫ p

Tactic:
refine ⟨hc.desc (cocone R π' ((lightProfiniteToLightCondSet ⋙ free R).map g' ≫ g)
      r_inf split.section_ hr), ?_⟩

Goal state after:
case pos
R : Type
inst✝ : CommRing R
X Y : LightCondMod R
p : X ⟶ Y
hp : Epi p
S : LightProfinite
f : (free R).obj (S ⊗ ℕ∪{∞}).toCondensed ⟶ Y
T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
g : (free R).obj T.toCondensed ⟶ X
hπ : Epi π
comm : (lightProfiniteToLightCondSet ⋙ free R).map π ≫ f = g ≫ p
S' T' : LightProfinite
y' : S' ⟶ S
π' : T' ⟶ S' ⊗ ℕ∪{∞}
g' : T' ⟶ T
hπ'✝ : Epi π'
hy' : Epi y'
comp : π' ≫ y' ▷ ℕ∪{∞} = g' ≫ π
epi : Epi (cover π')
split : SplitEpi (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π' ≫ fst S' ℕ∪{∞})
hS' : Nonempty ↑S'.toTop
this✝¹ : Mono (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}))
this✝ : Nonempty ↑(LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞})).toTop
r_inf : T' ⟶ LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞})
hr : LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ r_inf = 𝟙 (LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞}))
hπ'' : RegularEpi (lightProfiniteToLightCondSet.map π') := regularEpiOfEpi (lightProfiniteToLightCondSet.map π')
this : EffectiveEpi π'
hπ' : RegularEpi (lightProfiniteToLightCondSet.map π') :=
  regularEpiOfPreserves π' lightProfiniteToLightCondSet (pullback.cone π' π') (pullback.isLimit π' π')
hc : Limits.IsColimit ((free R).mapCocone (Limits.Cofork.ofπ (lightProfiniteToLightCondSet.map π') ⋯))
⊢ (free R).map (lightProfiniteToLightCondSet.map (y' ▷ ℕ∪{∞})) ≫ f =
    hc.desc (cocone R π' ((lightProfiniteToLightCondSet ⋙ free R).map g' ≫ g) r_inf split.section_ hr) ≫ p
Module: Mathlib.Data.List.AList

Goal state before:
pp: α : Type u
β : α → Type v
s₁ s₂ : AList β
h : s₁.entries ⊆ s₂.entries
k : α
hk : k ∈ s₁.keys
this✝ : DecidableEq α := Classical.decEq α
this : lookup k s₂ = some ((lookup k s₁).get ⋯)
⊢ k ∈ s₂.keys

Tactic:
← mem_keys,

Goal state after:
α : Type u
β : α → Type v
s₁ s₂ : AList β
h : s₁.entries ⊆ s₂.entries
k : α
hk : k ∈ s₁.keys
this✝ : DecidableEq α := Classical.decEq α
this : lookup k s₂ = some ((lookup k s₁).get ⋯)
⊢ k ∈ s₂
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
⊢ lookup a (singleton a b) = some b

Tactic:
by
  rw [singleton, lookup_toFinmap, AList.singleton, AList.lookup, dlookup_cons_eq]

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

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

Tactic:
map_map

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys
this : (map (Sigma.fst ∘ Sigma.mk a) (lookupAll a l)).Nodup
⊢ (lookupAll a l).length ≤ 1
Module: Mathlib.Data.Multiset.Functor

Goal state before:
pp: case trans
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a b l₁✝ l₂✝ l₃✝ : List α'
a✝¹ : l₁✝ ~ l₂✝
a✝ : l₂✝ ~ l₃✝
a_ih✝¹ : ofList <$> Traversable.traverse f l₁✝ = ofList <$> Traversable.traverse f l₂✝
a_ih✝ : ofList <$> Traversable.traverse f l₂✝ = ofList <$> Traversable.traverse f l₃✝
⊢ ofList <$> Traversable.traverse f l₁✝ = ofList <$> Traversable.traverse f l₃✝

Tactic:
simp [*]

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

Goal state before:
pp: inst✝ : (P : Prop) → Decidable P
α β γ : Type u
f : α → β → γ
s : Finset α
t : Finset β
a✝ : γ
⊢ a✝ ∈ image₂ f s t ↔ a✝ ∈ f <$> s <*> t

Tactic:
simp [mem_sup]

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
x✝ : List (Sigma β)
h : a ∈ [].keys
⊢ kerase a ([] ++ x✝) = kerase a [] ++ x✝

Tactic:
by cases h

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

Goal state before:
pp: case pos
α : Type u
β : α → Type v
inst✝¹ : DecidableEq α
inst✝ : SizeOf (Sigma β)
x : α
y : Sigma β
ys : List (Sigma β)
tail_ih✝ : sizeOf (kerase x ys) ≤ sizeOf ys
h✝ : x = y.fst
⊢ sizeOf (kerase x (y :: ys)) ≤ sizeOf (y :: ys)

Tactic:
simp [*]

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

Goal state before:
pp: case neg
α : Type u
β : α → Type v
inst✝¹ : DecidableEq α
inst✝ : SizeOf (Sigma β)
x : α
y : Sigma β
ys : List (Sigma β)
tail_ih✝ : sizeOf (kerase x ys) ≤ sizeOf ys
h✝ : ¬x = y.fst
⊢ sizeOf (kerase x (y :: ys)) ≤ sizeOf (y :: ys)

Tactic:
simp [*]

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

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

Tactic:
← exists_and_left,

Goal state after:
m n k : ℕ
⊢ (∃ k₁ k₂, k₁ ∣ m ∧ k₂ ∣ n ∧ k₁ * k₂ = k) ∧ m ≠ 0 ∧ n ≠ 0 ↔ ∃ y x, (y ∣ m ∧ m ≠ 0) ∧ (x ∣ n ∧ n ≠ 0) ∧ y * x = k
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
head✝ : Sigma β
l : List (Sigma β)
⊢ head✝ :: l.kunion (kerase head✝.fst []) = head✝ :: l

Tactic:
kerase_nil,

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
head✝ : Sigma β
l : List (Sigma β)
⊢ head✝ :: l.kunion [] = head✝ :: l
Module: Mathlib.Data.Finset.PiInduction

Goal state before:
pp: case intro.a.inr
ι : Type u_1
α : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)
p : ((i : ι) → Finset (α i)) → Prop
h0 : p fun x ↦ ∅
step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), r i x (g i) → p g → p (update g i (insert x (g i)))
val✝ : Fintype ι
f : (i : ι) → Finset (α i)
hne : (univ.sigma f).Nonempty
i : ι
hi : (f i).Nonempty
x : α i
x_mem : x ∈ f i
g : (a : ι) → Finset (α a)
ihs : ∀ t ⊂ univ.sigma (update g i (insert x (g i))), ∀ (f : (i : ι) → Finset (α i)), univ.sigma f = t → p f
hr : r i x ((insert x (g i)).erase x)
hx' : x ∉ g i
⊢ p (update g i (insert x (g i)))

Tactic:
erase_insert hx'

Goal state after:
case intro.a.inr
ι : Type u_1
α : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)
p : ((i : ι) → Finset (α i)) → Prop
h0 : p fun x ↦ ∅
step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), r i x (g i) → p g → p (update g i (insert x (g i)))
val✝ : Fintype ι
f : (i : ι) → Finset (α i)
hne : (univ.sigma f).Nonempty
i : ι
hi : (f i).Nonempty
x : α i
x_mem : x ∈ f i
g : (a : ι) → Finset (α a)
ihs : ∀ t ⊂ univ.sigma (update g i (insert x (g i))), ∀ (f : (i : ι) → Finset (α i)), univ.sigma f = t → p f
hr : r i x (g i)
hx' : x ∉ g i
⊢ p (update g i (insert x (g i)))
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: m n : ℕ
⊢ (subNatNat m n).bodd = (m.bodd ^^ n.bodd)

Tactic:
by
  apply subNatNat_elim m n fun m n i => bodd i = xor m.bodd n.bodd <;>
  intro i j <;>
  simp only [Int.bodd, Nat.bodd_add] <;>
  cases Nat.bodd i <;> simp

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

Goal state before:
pp: α : Type u
β : Type v
l : List α
f : ℕ → α → β
⊢ mapIdx f l = ofFn fun i ↦ f (↑i) (l.get i)

Tactic:
induction l generalizing f with
  | nil => simp
  | cons _ _ IH => simp [IH]

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

Goal state before:
pp: case cons.cons
α : Type u_1
f : α → α
l₁ : List α
hd hd' : α
tl' : List α
x✝ : hd :: hd' :: tl' ≠ []
⊢ modifyLast f (l₁ ++ [hd] ++ hd' :: tl') = l₁ ++ modifyLast f ([hd] ++ hd' :: tl')

Tactic:
modifyLast_append_of_right_ne_nil _ (l₁ ++ [hd]) (hd' :: tl') _,

Goal state after:
case cons.cons
α : Type u_1
f : α → α
l₁ : List α
hd hd' : α
tl' : List α
x✝ : hd :: hd' :: tl' ≠ []
⊢ l₁ ++ [hd] ++ modifyLast f (hd' :: tl') = l₁ ++ modifyLast f ([hd] ++ hd' :: tl')

α : Type u_1
f : α → α
l₁ : List α
hd hd' : α
tl' : List α
x✝ : hd :: hd' :: tl' ≠ []
⊢ hd' :: tl' ≠ []
Module: Mathlib.Data.List.Map2

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

Tactic:
simp [*]

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

Goal state before:
pp: case nil.cons
α : Type u
β : Type v
head✝ : β
tail✝ : List β
⊢ [].zipRight (head✝ :: tail✝) = ([].zipRight' (head✝ :: tail✝)).fst

Tactic:
simp [*]

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

Goal state before:
pp: case cons.nil
α : Type u
β : Type v
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (bs : List β), tail✝.zipRight bs = (tail✝.zipRight' bs).fst
⊢ (head✝ :: tail✝).zipRight [] = ((head✝ :: tail✝).zipRight' []).fst

Tactic:
simp [*]

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

Goal state before:
pp: case cons.cons
α : Type u
β : Type v
head✝¹ : α
tail✝¹ : List α
tail_ih✝ : ∀ (bs : List β), tail✝¹.zipRight bs = (tail✝¹.zipRight' bs).fst
head✝ : β
tail✝ : List β
⊢ (head✝¹ :: tail✝¹).zipRight (head✝ :: tail✝) = ((head✝¹ :: tail✝¹).zipRight' (head✝ :: tail✝)).fst

Tactic:
simp [*]

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

Goal state before:
pp: n m l : ℕ
hnl : n ≤ l
⊢ filter (fun x ↦ decide (l ≤ x)) (Ico n m) = Ico l m

Tactic:
rcases le_total l m with hlm | hml
  · rw [← append_consecutive hnl hlm, filter_append, filter_le_of_top_le (le_refl l),
      filter_le_of_le_bot (le_refl l), nil_append]
  · rw [eq_nil_of_le hml, filter_le_of_top_le hml]

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

Goal state before:
pp: case refine_1.cons
α : Type u_1
head✝ : List α
tail✝ : List (List α)
tail_ih✝ : ∀ {f : List α}, f ∈ tail✝.sections → Forall₂ (fun x1 x2 ↦ x1 ∈ x2) f tail✝
w✝¹ : List α
left✝¹ : w✝¹ ∈ tail✝.sections
w✝ : α
left✝ : w✝ ∈ head✝
⊢ Forall₂ (fun x1 x2 ↦ x1 ∈ x2) (w✝ :: w✝¹) (head✝ :: tail✝)

Tactic:
simp only [*, forall₂_cons, true_and]

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

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α} (gs : List (List α)), splitBy.loop r l a g gs = gs.reverse ++ splitBy.loop r l a g []
a : α
g : List α
gs : List (List α)
⊢ splitBy.loop r (b :: l) a g gs = gs.reverse ++ splitBy.loop r (b :: l) a g []

Tactic:
splitBy.loop

Goal state after:
case cons
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α} (gs : List (List α)), splitBy.loop r l a g gs = gs.reverse ++ splitBy.loop r l a g []
a : α
g : List α
gs : List (List α)
⊢ (match r a b with
    | true => splitBy.loop r l b (a :: g) gs
    | false => splitBy.loop r l b [] ((a :: g).reverse :: gs)) =
    gs.reverse ++
      match r a b with
      | true => splitBy.loop r l b (a :: g) []
      | false => splitBy.loop r l b [] [(a :: g).reverse]
Module: Mathlib.Data.List.SplitBy

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

Tactic:
induction l generalizing a g with

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

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α}, ¬[] ∈ splitBy.loop r l a g []
a : α
g : List α
⊢ ¬[] ∈ splitBy.loop r (b :: l) a g []

Tactic:
splitBy.loop

Goal state after:
case cons
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α}, ¬[] ∈ splitBy.loop r l a g []
a : α
g : List α
⊢ ¬[] ∈
      match r a b with
      | true => splitBy.loop r l b (a :: g) []
      | false => splitBy.loop r l b [] [(a :: g).reverse]
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: α : Type u_1
r : α → α → Bool
l : List α
a : α
g : List α
⊢ ¬[] ∈ splitBy.loop r l a g []

Tactic:
induction l generalizing a g with

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

Goal state before:
pp: case nil
α : Type u_1
m : List α
r : α → α → Bool
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : IsChain (fun y x ↦ r x y = true) g
h : m ∈ [].reverse ∨ m ∈ [(a :: g).reverse]
⊢ IsChain (fun x y ↦ r x y = true) m

Tactic:
mem_reverse,

Goal state after:
case nil
α : Type u_1
m : List α
r : α → α → Bool
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : IsChain (fun y x ↦ r x y = true) g
h : m ∈ [] ∨ m ∈ [(a :: g).reverse]
⊢ IsChain (fun x y ↦ r x y = true) m
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: case mpr
α : Type u_1
p : ℕ
w : List α
⊢ (∀ i < w.length - p, w[i]? = w[i + p]?) → w.HasPeriod p

Tactic:
· intro lhs
    rw [HasPeriod]
    have drop : drop p w <+: w := by
      simp only [prefix_iff_getElem?, length_drop, getElem_drop]
      intro i leni
      have len : i + p < w.length := by lia
      simp_all only [getElem?_pos, add_comm p i]
    rw [← prefix_append_right_inj (w.take p)] at drop
    simp_all

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

Goal state before:
pp: α : Type u_1
m : List α
r : α → α → Bool
l : List α
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : IsChain (fun y x ↦ r x y = true) g
h : m ∈ splitBy.loop r l a g []
⊢ IsChain (fun x y ↦ r x y = true) m

Tactic:
induction l generalizing a g with

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

Goal state before:
pp: case cons
α : 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
⊢ IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) (splitBy.loop r (b :: l) a g gs)

Tactic:
splitBy.loop

Goal state after:
case cons
α : 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
⊢ IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false)
    (match r a b with
    | true => splitBy.loop r l b (a :: g) gs
    | false => splitBy.loop r l b [] ((a :: g).reverse :: gs))
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: α : Type u_1
m : List α
r : α → α → Bool
l g : List α
a : α
h : IsChain (fun x y ↦ r x y = true) (g.reverse ++ a :: l)
ha : ∀ (x : α), x ∈ m.head? → r ((a :: l).getLast ⋯) x = false
⊢ splitBy.loop r (l ++ m) a g [] = (g.reverse ++ a :: l) :: splitBy r m

Tactic:
induction l generalizing a g with

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

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Bool
a : α
l : List α
hn : a :: l ≠ []
h : IsChain (fun x y ↦ r x y = true) (a :: l)
⊢ splitBy r (a :: l) = [a :: l]

Tactic:
splitBy,

Goal state after:
case cons
α : Type u_1
r : α → α → Bool
a : α
l : List α
hn : a :: l ≠ []
h : IsChain (fun x y ↦ r x y = true) (a :: l)
⊢ splitBy.loop r l a [] [] = [a :: l]