mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.ENat.BigOperators

Goal state before:
pp: ι : Type u_2
α : Type u_3
f : ι → α → ℕ∞
s : Finset α
inst✝ : Nonempty ι
h : ∀ (t : Finset α) (i j : ι), ∃ k, ∀ a ∈ t, f k a ≤ f i a ∧ f k a ≤ f j a
⊢ ⨅ i, ∑ a ∈ s, f i a = ∑ a ∈ s, ⨅ i, f i a

Tactic:
by
  induction s using Finset.cons_induction_on with
  | empty => simp only [Finset.sum_empty, ciInf_const]
  | cons a s ha ih =>
    simp only [Finset.sum_cons, ← ih]
    refine (iInf_add_iInf fun i j => ?_).symm
    refine (h (Finset.cons a s ha) i j).imp fun k hk => ?_
    rw [Finset.forall_mem_cons] at hk
    exact add_le_add hk.1.1 (Finset.sum_le_sum fun a ha => (hk.2 a ha).2)

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

Goal state before:
pp: n : ℕ
p : Fin n → Type u
τ : Type u
f : ((i : Fin n) → p i) → τ
⊢ (curry f).uncurry = f

Tactic:
ext args
  induction n with
  | zero => exact congrArg f (Subsingleton.allEq _ _)
  | succ n ih => exact Eq.trans (ih _ _) (congrArg f (Fin.cons_self_tail args))

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
s : Finmap β
⊢ (s.keys.sigma fun i ↦ (lookup i s).toFinset) = { val := s.entries, nodup := ⋯ }

Tactic:
ext x

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s : Finmap β
x : (i : α) × β i
⊢ (x ∈ s.keys.sigma fun i ↦ (lookup i s).toFinset) ↔ x ∈ { val := s.entries, nodup := ⋯ }
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: 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
h : IsEmpty (↑S'.toTop ⊗ ↑ℕ∪{∞}.toTop)
⊢ π' ≫ ConcreteCategory.ofHom { toFun := fun x ↦ h.elim x, continuous_toFun := ⋯ } = 𝟙 T'

Tactic:
ext x

Goal state after:
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
h : IsEmpty (↑S'.toTop ⊗ ↑ℕ∪{∞}.toTop)
x : ↑T'.toTop
⊢ (ConcreteCategory.hom (π' ≫ ConcreteCategory.ofHom { toFun := fun x ↦ h.elim x, continuous_toFun := ⋯ })) x =
    (ConcreteCategory.hom (𝟙 T')) x
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b' : β a'
l : List (Sigma β)
⊢ map (Sigma.mk a) (lookupAll a (⟨a', b'⟩ :: l)) <+ ⟨a', b'⟩ :: l

Tactic:
by_cases h : a = a'
    · subst h
      simp only [lookupAll_cons_eq, List.map]
      exact (lookupAll_sublist a l).cons_cons _
    · simp only [ne_eq, h, not_false_iff, lookupAll_cons_ne]
      exact (lookupAll_sublist a l).cons _

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

Goal state before:
pp: 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
h : IsEmpty (↑S'.toTop ⊗ ↑ℕ∪{∞}.toTop)
⊢ ConcreteCategory.ofHom { toFun := fun x ↦ h.elim x, continuous_toFun := ⋯ } ≫ π' = 𝟙 (S' ⊗ ℕ∪{∞})

Tactic:
ext x

Goal state after:
case h_fst
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
h : IsEmpty (↑S'.toTop ⊗ ↑ℕ∪{∞}.toTop)
x : ↑(S' ⊗ ℕ∪{∞}).toTop
⊢ (ConcreteCategory.hom
        ((ConcreteCategory.ofHom { toFun := fun x ↦ h.elim x, continuous_toFun := ⋯ } ≫ π') ≫ fst S' ℕ∪{∞}))
      x =
    (ConcreteCategory.hom (𝟙 (S' ⊗ ℕ∪{∞}) ≫ fst S' ℕ∪{∞})) x

case h_snd
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
h : IsEmpty (↑S'.toTop ⊗ ↑ℕ∪{∞}.toTop)
x : ↑(S' ⊗ ℕ∪{∞}).toTop
⊢ (ConcreteCategory.hom
        ((ConcreteCategory.ofHom { toFun := fun x ↦ h.elim x, continuous_toFun := ⋯ } ≫ π') ≫ snd S' ℕ∪{∞}))
      x =
    (ConcreteCategory.hom (𝟙 (S' ⊗ ℕ∪{∞}) ≫ snd S' ℕ∪{∞})) x
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ s₃ : Finmap β
h : s₁.Disjoint s₃
h' : s₂.Disjoint s₃
h'' : s₁ ∪ s₃ = s₂ ∪ s₃
x : α
this : lookup x (s₁ ∪ s₃) = lookup x (s₂ ∪ s₃)
⊢ lookup x s₁ = lookup x s₂

Tactic:
by_cases hs₁ : x ∈ s₁

Goal state after:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ s₃ : Finmap β
h : s₁.Disjoint s₃
h' : s₂.Disjoint s₃
h'' : s₁ ∪ s₃ = s₂ ∪ s₃
x : α
this : lookup x (s₁ ∪ s₃) = lookup x (s₂ ∪ s₃)
hs₁ : x ∈ s₁
⊢ lookup x s₁ = lookup x s₂

case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ s₃ : Finmap β
h : s₁.Disjoint s₃
h' : s₂.Disjoint s₃
h'' : s₁ ∪ s₃ = s₂ ∪ s₃
x : α
this : lookup x (s₁ ∪ s₃) = lookup x (s₂ ∪ s₃)
hs₁ : x ∉ s₁
⊢ lookup x s₁ = lookup x s₂
Module: Mathlib.Data.Finmap

Goal state before:
pp: case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ s₃ : Finmap β
h : s₁.Disjoint s₃
h' : s₂.Disjoint s₃
h'' : s₁ ∪ s₃ = s₂ ∪ s₃
x : α
this : lookup x (s₁ ∪ s₃) = lookup x (s₂ ∪ s₃)
hs₁ : x ∉ s₁
hs₂ : x ∉ s₂
⊢ none = lookup x s₂

Tactic:
lookup_eq_none.mpr hs₂

Goal state after:
case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ s₃ : Finmap β
h : s₁.Disjoint s₃
h' : s₂.Disjoint s₃
h'' : s₁ ∪ s₃ = s₂ ∪ s₃
x : α
this : lookup x (s₁ ∪ s₃) = lookup x (s₂ ∪ s₃)
hs₁ : x ∉ s₁
hs₂ : x ∉ s₂
⊢ none = none
Module: Mathlib.Data.Finset.Functor

Goal state before:
pp: α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
s : Finset α✝
t : Finset β✝
hs : s.Nonempty
a : β✝
ha : a ∈ t
⊢ a ∈ image id t

Tactic:
rwa [image_id]

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

Goal state before:
pp: case nil
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l₂ : List (Sigma β)
h : a ∈ [].keys
⊢ dlookup a ([].kunion l₂) = dlookup a []

Tactic:
simp at h

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

Goal state before:
pp: κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst✝ : AddMonoid M
k : κ
f g : ι k →₀ M
⊢ (f + g).embSigma = f.embSigma + g.embSigma

Tactic:
by
  ext ⟨k', i⟩
  by_cases hk : k' = k
  · subst hk
    simp
  · simp [embSigma_apply_of_ne _ hk]

Goal state after:
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
d : ℕ
ds : List ℕ
x y : Holor α (d :: ds)
h : x.slice = y.slice
t : HolorIndex (d :: ds)
i : ℕ
is : List ℕ
hiis : ↑t = i :: is
hiisdds : Forall₂ (fun x1 x2 ↦ x1 < x2) (i :: is) (d :: ds)
hid : i < d
hisds : Forall₂ (fun x1 x2 ↦ x1 < x2) is ds
⊢ x.slice i hid ⟨is, hisds⟩ = y.slice i hid ⟨is, hisds⟩

Tactic:
by rw [h]

Goal state after:
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
inst✝¹ : Mul α
inst✝ : AddMonoid α
x : Holor α []
⊢ CPRankMax 1 x

Tactic:
have h := CPRankMax.succ 0 x 0 (CPRankMax1.nil x) CPRankMax.zero

Goal state after:
α : Type
inst✝¹ : Mul α
inst✝ : AddMonoid α
x : Holor α []
h : CPRankMax (0 + 1) (x + 0)
⊢ CPRankMax 1 x
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 ∈ ∅, CPRankMax n (f x)) → CPRankMax (∅.card * n) (∑ x ∈ ∅, f x)

Tactic:
simp [CPRankMax.zero]

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

Goal state before:
pp: p : ℕ
p_prime : Nat.Prime p
m n : ℤ
k l : ℕ
hpm : ↑(p ^ k) ∣ m
hpn : ↑(p ^ l) ∣ n
hpmn : ↑(p ^ (k + l + 1)) ∣ m * n
hpm' : p ^ k ∣ m.natAbs
hpn' : p ^ l ∣ n.natAbs
hpmn' : p ^ (k + l + 1) ∣ m.natAbs * n.natAbs
hsd : p ^ (k + 1) ∣ m.natAbs ∨ p ^ (l + 1) ∣ n.natAbs := ⋯
hsd1 : p ^ (k + 1) ∣ m.natAbs
⊢ ↑(p ^ (k + 1)) ∣ ↑m.natAbs

Tactic:
apply Int.natCast_dvd_natCast.2 hsd1

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

Goal state before:
pp: a b r v : ℤ
⊢ {x ∈ Ico a b | x ≡ v [ZMOD r]} = map { toFun := fun x ↦ x + v, inj' := ⋯ } ({x ∈ Ico (a - v) (b - v) | r ∣ x})

Tactic:
ext x

Goal state after:
a b r v x : ℤ
⊢ x ∈ {x ∈ Ico a b | x ≡ v [ZMOD r]} ↔ x ∈ map { toFun := fun x ↦ x + v, inj' := ⋯ } ({x ∈ Ico (a - v) (b - v) | r ∣ x})
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: a b r v : ℤ
⊢ {x ∈ Ioc a b | x ≡ v [ZMOD r]} = map { toFun := fun x ↦ x + v, inj' := ⋯ } ({x ∈ Ioc (a - v) (b - v) | r ∣ x})

Tactic:
ext x

Goal state after:
a b r v x : ℤ
⊢ x ∈ {x ∈ Ioc a b | x ≡ v [ZMOD r]} ↔ x ∈ map { toFun := fun x ↦ x + v, inj' := ⋯ } ({x ∈ Ioc (a - v) (b - v) | r ∣ x})
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: a b r : ℤ
hr : 0 < r
⊢ {x ∈ Ico a b | r ∣ x} = map { toFun := fun x ↦ x * r, inj' := ⋯ } (Ico ⌈↑a / ↑r⌉ ⌈↑b / ↑r⌉)

Tactic:
ext x

Goal state after:
a b r : ℤ
hr : 0 < r
x : ℤ
⊢ x ∈ {x ∈ Ico a b | r ∣ x} ↔ x ∈ map { toFun := fun x ↦ x * r, inj' := ⋯ } (Ico ⌈↑a / ↑r⌉ ⌈↑b / ↑r⌉)
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: a b r : ℤ
hr : 0 < r
⊢ {x ∈ Ioc a b | r ∣ x} = map { toFun := fun x ↦ x * r, inj' := ⋯ } (Ioc ⌊↑a / ↑r⌋ ⌊↑b / ↑r⌋)

Tactic:
ext x

Goal state after:
a b r : ℤ
hr : 0 < r
x : ℤ
⊢ x ∈ {x ∈ Ioc a b | r ∣ x} ↔ x ∈ map { toFun := fun x ↦ x * r, inj' := ⋯ } (Ioc ⌊↑a / ↑r⌋ ⌊↑b / ↑r⌋)
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: a b r v : ℕ
⊢ map castEmbedding ({x ∈ Ico a b | x ≡ v [MOD r]}) = {x ∈ Ico ↑a ↑b | x ≡ ↑v [ZMOD ↑r]}

Tactic:
ext x

Goal state after:
a b r v : ℕ
x : ℤ
⊢ x ∈ map castEmbedding ({x ∈ Ico a b | x ≡ v [MOD r]}) ↔ x ∈ {x ∈ Ico ↑a ↑b | x ≡ ↑v [ZMOD ↑r]}
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: m n k : ℕ
⊢ ↑m >>> (↑n + ↑k) = ↑m >>> ↑n >>> ↑k

Tactic:
rw [shiftRight_natCast, shiftRight_natCast, ← Int.natCast_add, shiftRight_natCast,
      Nat.shiftRight_add]

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

Goal state before:
pp: a b r v : ℕ
⊢ map castEmbedding ({x ∈ Ioc a b | x ≡ v [MOD r]}) = {x ∈ Ioc ↑a ↑b | x ≡ ↑v [ZMOD ↑r]}

Tactic:
ext x

Goal state after:
a b r v : ℕ
x : ℤ
⊢ x ∈ map castEmbedding ({x ∈ Ioc a b | x ≡ v [MOD r]}) ↔ x ∈ {x ∈ Ioc ↑a ↑b | x ≡ ↑v [ZMOD ↑r]}
Module: Mathlib.Data.List.TakeWhile

Goal state before:
pp: case neg
α : Type u_1
p : α → Bool
hd : α
tl : List α
IH : ∀ (hl : 0 < (dropWhile p tl).length), ¬p ((dropWhile p tl).get ⟨0, hl⟩) = true
hl : 0 < (dropWhile p (hd :: tl)).length
hp : ¬p hd = true
⊢ ¬p
        ((match p hd with
            | true => dropWhile p tl
            | false => hd :: tl).get
          ⟨0, hl⟩) =
      true

Tactic:
simp [hp]

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

Goal state before:
pp: case pos
α : Type u_1
p : α → Bool
hd : α
tl : List α
h_p_hd : p hd = true
h : (dropWhile p tl).length = (hd :: tl).length
this : (dropWhile p tl).length ≤ tl.length
⊢ False

Tactic:
simp at h

Goal state after:
case pos
α : Type u_1
p : α → Bool
hd : α
tl : List α
h_p_hd : p hd = true
h : (dropWhile p tl).length = tl.length + 1
this : (dropWhile p tl).length ≤ tl.length
⊢ False
Module: Mathlib.Data.List.TakeWhile

Goal state before:
pp: case nil
α : Type u_1
p : α → Bool
l : List α
h : 0 < [].length
⊢ p ([].get ⟨0, h⟩) = false

Tactic:
simp at h

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

Goal state before:
pp: case pos
α : Type u_1
p : α → Bool
l : List α
x : α
xs : List α
IH : takeWhile p xs = [] ↔ ∀ (hl : 0 < xs.length), ¬p (xs.get ⟨0, hl⟩) = true
hp : p x = true
⊢ takeWhile p (x :: xs) = [] ↔ ∀ (hl : 0 < (x :: xs).length), ¬p ((x :: xs).get ⟨0, hl⟩) = true

Tactic:
simp [hp]

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

Goal state before:
pp: case neg
α : Type u_1
p : α → Bool
l : List α
x : α
xs : List α
IH : takeWhile p xs = [] ↔ ∀ (hl : 0 < xs.length), ¬p (xs.get ⟨0, hl⟩) = true
hp : ¬p x = true
⊢ takeWhile p (x :: xs) = [] ↔ ∀ (hl : 0 < (x :: xs).length), ¬p ((x :: xs).get ⟨0, hl⟩) = true

Tactic:
simp [hp]

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α → Option β → γ
a : α
as : List α
h : (a :: as).length ≤ [].length
⊢ map₂Left f (a :: as) [] = zipWith (fun a b ↦ f a (some b)) (a :: as) []

Tactic:
simp at h

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

Goal state before:
pp: case refine_1.nil
α : Type u_1
f : List α
h : f ∈ [].sections
⊢ Forall₂ (fun x1 x2 ↦ x1 ∈ x2) f []

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✝
f : List α
h : f ∈ (head✝ :: tail✝).sections
⊢ Forall₂ (fun x1 x2 ↦ x1 ∈ x2) f (head✝ :: tail✝)

Tactic:
· cases mem_singleton.1 h
      exact Forall₂.nil

Goal state after:
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✝
f : List α
h : f ∈ (head✝ :: tail✝).sections
⊢ Forall₂ (fun x1 x2 ↦ x1 ∈ x2) f (head✝ :: tail✝)
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: case mp
α : Type u_1
m : List α
r : α → α → Bool
⊢ m = (splitBy r m).flatten ∧
    ¬[] ∈ splitBy r m ∧
      (∀ (m_1 : List α), m_1 ∈ splitBy r m → IsChain (fun x y ↦ r x y = true) m_1) ∧
        IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) (splitBy r m)

Tactic:
exact ⟨(flatten_splitBy r m).symm, nil_notMem_splitBy r m, fun _ ↦ isChain_of_mem_splitBy,
      isChain_getLast_head_splitBy r m⟩

Goal state after:
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: R : Type u_1
m : Type u_2
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝² : Semiring R
inst✝¹ : Fintype n₁
inst✝ : Fintype n₂
A₁ : Matrix m n₁ R
A₂ : Matrix m n₂ R
B₁ : Matrix n₁ n R
B₂ : Matrix n₂ n R
⊢ A₁.fromCols A₂ * B₁.fromRows B₂ = A₁ * B₁ + A₂ * B₂

Tactic:
ext
  simp [mul_apply]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ Finset.map equivDFinsupp.symm.toEmbedding (Finset.Icc (toDFinsupp (s ⊓ t)) (toDFinsupp (s ⊔ t))) =
    Finset.map equivDFinsupp.symm.toEmbedding (uIcc (toDFinsupp s) (toDFinsupp t))

Tactic:
simp [uIcc]

Goal state after:
Module: Mathlib.Data.Nat.Prime.Factorial

Goal state before:
pp: n p : ℕ
hp : Prime p
h✝ : p ≤ n + 1
h : p = n + 1
⊢ p ∣ n + 1

Tactic:
by rw [h]

Goal state after:
Module: Mathlib.Data.Nat.Digits.Div

Goal state before:
pp: n : ℕ
p : (digits 10 n).Palindrome
dig : List ℤ := List.map (fun n ↦ ↑n) (digits 10 n)
h : Even dig.length
this : dig.reverse.alternatingSum = (-1) ^ (dig.length + 1) • dig.alternatingSum
⊢ dig.alternatingSum = 0

Tactic:
rw [(p.map _).reverse_eq, _root_.pow_succ', h.neg_one_pow, mul_one, neg_one_zsmul] at this

Goal state after:
n : ℕ
p : (digits 10 n).Palindrome
dig : List ℤ := List.map (fun n ↦ ↑n) (digits 10 n)
h : Even dig.length
this : (List.map (fun n ↦ ↑n) (digits 10 n)).alternatingSum = -dig.alternatingSum
⊢ dig.alternatingSum = 0
Module: Mathlib.Data.Nat.ChineseRemainder

Goal state before:
pp: ι : Type u_1
a s : ι → ℕ
t : Finset ι
hs : ∀ i ∈ t, s i ≠ 0
pp : (↑t).Pairwise (Coprime on s)
⊢ ∀ i ∈ t.val, s i ≠ 0

Tactic:
simpa using hs

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

Goal state before:
pp: a n : ℕ
⊢ n.ceilRoot a = if n = 0 ∨ a = 0 then 0 else (a.factorization ⌈/⌉ n).prod fun x1 x2 ↦ x1 ^ x2

Tactic:
unfold ceilRoot

Goal state after:
a n : ℕ
⊢ (if n = 0 ∨ a = 0 then 0 else a.factorization.prod fun p k ↦ p ^ ((k + n - 1) / n)) =
    if n = 0 ∨ a = 0 then 0 else (a.factorization ⌈/⌉ n).prod fun x1 x2 ↦ x1 ^ x2
Module: Mathlib.Data.Nat.Factorization.Root

Goal state before:
pp: a b n : ℕ
hn : n ≠ 0
⊢ a ∣ b ^ n ↔ n.ceilRoot a ∣ b

Tactic:
obtain rfl | ha := eq_or_ne a 0
  · aesop
  obtain rfl | hb := eq_or_ne b 0
  · simp [hn]
  rw [← factorization_le_iff_dvd ha (pow_ne_zero _ hb),
    ← factorization_le_iff_dvd (ceilRoot_ne_zero.2 ⟨hn, ha⟩) hb, factorization_pow,
    factorization_ceilRoot, ceilDiv_le_iff_le_smul (β := ℕ →₀ ℕ) (pos_iff_ne_zero.2 hn)]

Goal state after:
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: n : ℕ
h : IsPrimePow n
k : ℕ
left✝¹ : k ≤ log 2 n
left✝ : 0 < k
hn₁ : n = n.minFac ^ k
i : ℕ
hi : i ∈ Icc 1 (n - 1)
⊢ n.minFac ∣ n.choose i

Tactic:
nth_rw 2 [hn₁]
    exact Prime.dvd_choose_pow (minFac_prime_iff.mpr h.ne_one) (by grind) (by grind)

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

Goal state before:
pp: p : ℕ → Prop
hf : (Set.ofPred p).Finite
⊢ nth p '' Set.Iio #hf.toFinset = Set.range ⇑(hf.toFinset.orderEmbOfFin ⋯)

Tactic:
ext x

Goal state after:
p : ℕ → Prop
hf : (Set.ofPred p).Finite
x : ℕ
⊢ x ∈ nth p '' Set.Iio #hf.toFinset ↔ x ∈ Set.range ⇑(hf.toFinset.orderEmbOfFin ⋯)
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: case zero.mp
p : PosNum
h : pos p = zero
⊢ ZNum.pos p = zero.toZNum

Tactic:
try cases h <;> rfl

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

Goal state before:
pp: case zero.mpr
p : PosNum
h : ZNum.pos p = zero.toZNum
⊢ pos p = zero

Tactic:
try cases h <;> rfl

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

Goal state before:
pp: case pos.mp
p a✝ : PosNum
h : pos p = pos a✝
⊢ ZNum.pos p = (pos a✝).toZNum

Tactic:
try cases h <;> rfl

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

Goal state before:
pp: case pos.mpr
p a✝ : PosNum
h : ZNum.pos p = (pos a✝).toZNum
⊢ pos p = pos a✝

Tactic:
try cases h <;> rfl

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

Goal state before:
pp: P : PFunctor.{uA, uB}
α : Type u
a : P.A
f : P.B a → α
⊢ supp ⟨a, f⟩ = f '' univ

Tactic:
ext x

Goal state after:
P : PFunctor.{uA, uB}
α : Type u
a : P.A
f : P.B a → α
x : α
⊢ x ∈ supp ⟨a, f⟩ ↔ x ∈ f '' univ
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case node
α : Type u_1
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
ht : (node size✝ l✝ x✝ r✝).Sized
⊢ (node size✝ l✝ x✝ r✝).size = 0 ↔ node size✝ l✝ x✝ r✝ = nil

Tactic:
simp [ht.1]

Goal state after:
Module: Mathlib.Data.PFunctor.Multivariate.Basic

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
a : P.A
f : P.B a ⟹ α
i : Fin2 n
⊢ supp ⟨a, f⟩ i = f i '' univ

Tactic:
ext x

Goal state after:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
a : P.A
f : P.B a ⟹ α
i : Fin2 n
x : α i
⊢ x ∈ supp ⟨a, f⟩ i ↔ x ∈ f i '' univ
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case succ
F : PFunctor.{uA, uB}
n : ℕ
n_ih : ∀ (x : CofixA F n) (y : CofixA F n.succ), Agree x y → truncate y = x
x : CofixA F (n + 1)
y : CofixA F (n + 1).succ
h : Agree x y
⊢ truncate y = x

Tactic:
cases h with | intro f y h₁ =>
    simp only [truncate, Function.comp_def]
    congr with y
    exact n_ih _ _ (h₁ y)

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

Goal state before:
pp: F : PFunctor.{uA, uB}
X : Type u_1
f✝ : X → ↑F X
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited F.M
a : F.A
i : F.B a
ps : List F.Idx
x : F.M
a' : F.A
f : F.B a' → F.M
h : a = a'
⊢ F.B a = F.B a'

Tactic:
by rw [h]

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

Goal state before:
pp: case pos.inl.inl
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' (↑x) (Ordnode.node rs rl rx rr) o₂
H1 : ¬l.size + (Ordnode.node rs rl rx rr).size ≤ 1
H2 : delta * l.size ≤ rl.size + rr.size
H3_0 : l.size = 0 → rl.size + rr.size ≤ 2
H3p : l.size > 0 → 2 * (rl.size + rr.size) ≤ 9 * l.size + 3
ablem : ∀ {a b : ℕ}, 1 ≤ a → a + b ≤ 2 → b ≤ 1
hlp : l.size > 0 → ¬rl.size + rr.size ≤ 1
h : rl.size < ratio * rr.size
rr0 : rr.size > 0
l0 : l.size = 0
H3 : rl.size + rr.size ≤ 2
this : BalancedSz rl.size rr.size
rl0 : rl.size = 0
⊢ BalancedSz 0 rl.size ∧ BalancedSz (0 + rl.size + 1) rr.size

Tactic:
rl0

Goal state after:
case pos.inl.inl
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' (↑x) (Ordnode.node rs rl rx rr) o₂
H1 : ¬l.size + (Ordnode.node rs rl rx rr).size ≤ 1
H2 : delta * l.size ≤ rl.size + rr.size
H3_0 : l.size = 0 → rl.size + rr.size ≤ 2
H3p : l.size > 0 → 2 * (rl.size + rr.size) ≤ 9 * l.size + 3
ablem : ∀ {a b : ℕ}, 1 ≤ a → a + b ≤ 2 → b ≤ 1
hlp : l.size > 0 → ¬rl.size + rr.size ≤ 1
h : rl.size < ratio * rr.size
rr0 : rr.size > 0
l0 : l.size = 0
H3 : rl.size + rr.size ≤ 2
this : BalancedSz 0 rr.size
rl0 : rl.size = 0
⊢ BalancedSz 0 0 ∧ BalancedSz (0 + 0 + 1) rr.size
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case pos.inl.inr
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' (↑x) (Ordnode.node rs rl rx rr) o₂
H1 : ¬l.size + (Ordnode.node rs rl rx rr).size ≤ 1
H2 : delta * l.size ≤ rl.size + rr.size
H3_0 : l.size = 0 → rl.size + rr.size ≤ 2
H3p : l.size > 0 → 2 * (rl.size + rr.size) ≤ 9 * l.size + 3
ablem : ∀ {a b : ℕ}, 1 ≤ a → a + b ≤ 2 → b ≤ 1
hlp : l.size > 0 → ¬rl.size + rr.size ≤ 1
h : rl.size < ratio * rr.size
rr0 : rr.size > 0
l0 : l.size = 0
H3 : rl.size + rr.size ≤ 2
this : BalancedSz rl.size rr.size
rl0 : rl.size > 0
⊢ BalancedSz 0 rl.size ∧ BalancedSz (0 + rl.size + 1) rr.size

Tactic:
have rr1 : size rr = 1 := le_antisymm (ablem rl0 H3) rr0

Goal state after:
case pos.inl.inr
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' (↑x) (Ordnode.node rs rl rx rr) o₂
H1 : ¬l.size + (Ordnode.node rs rl rx rr).size ≤ 1
H2 : delta * l.size ≤ rl.size + rr.size
H3_0 : l.size = 0 → rl.size + rr.size ≤ 2
H3p : l.size > 0 → 2 * (rl.size + rr.size) ≤ 9 * l.size + 3
ablem : ∀ {a b : ℕ}, 1 ≤ a → a + b ≤ 2 → b ≤ 1
hlp : l.size > 0 → ¬rl.size + rr.size ≤ 1
h : rl.size < ratio * rr.size
rr0 : rr.size > 0
l0 : l.size = 0
H3 : rl.size + rr.size ≤ 2
this : BalancedSz rl.size rr.size
rl0 : rl.size > 0
rr1 : rr.size = 1
⊢ BalancedSz 0 rl.size ∧ BalancedSz (0 + rl.size + 1) rr.size
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: P : PFunctor.{uA, uB}
α : Type u_2
g : α → ↑P α
f : α → P.M
hyp : ∀ (x : α), (f x).dest = P.map f (g x)
⊢ f = M.corec g

Tactic:
ext x

Goal state after:
P : PFunctor.{uA, uB}
α : Type u_2
g : α → ↑P α
f : α → P.M
hyp : ∀ (x : α), (f x).dest = P.map f (g x)
x : α
⊢ f x = M.corec g x