mathlib-initiative/mathlib-tactics huggingface dataset:
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
this : Mono (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}))
x : ↑T'.toTop
hx : (⇑(ConcreteCategory.hom (snd S' ℕ∪{∞})) ∘ ⇑(ConcreteCategory.hom π')) x = ∞
⊢ x ∈ ⇑(ConcreteCategory.hom (π' ≫ snd S' ℕ∪{∞})) ⁻¹' {∞}

Tactic:
simpa using

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
this : Mono (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}))
x : ↑T'.toTop
hx : (⇑(ConcreteCategory.hom (snd S' ℕ∪{∞})) ∘ ⇑(ConcreteCategory.hom π')) x = ∞
⊢ (ConcreteCategory.hom (snd S' ℕ∪{∞})) ((ConcreteCategory.hom π') x) = ∞
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β✝ : α → Type v
β : Type ?u.19
f : β → α
inst✝¹ : DecidableEq α
inst✝ : FinEnum β
h : Surjective f
x✝ : α
⊢ x✝ ∈ List.map f (toList β)

Tactic:
simpa using

Goal state after:
α : Type u
β✝ : α → Type v
β : Type ?u.19
f : β → α
inst✝¹ : DecidableEq α
inst✝ : FinEnum β
h : Surjective f
x✝ : α
⊢ ∃ a, f a = x✝
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u_1
inst✝¹ : FinEnum α
β : α → Type u_2
inst✝ : (a : α) → FinEnum (β a)
f : (a : α) → β a
⊢ f ∈ enum β

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝¹ : FinEnum α
β : α → Type u_2
inst✝ : (a : α) → FinEnum (β a)
f : (a : α) → β a
⊢ ∃ a ∈ (FinEnum.toList α).pi fun x ↦ FinEnum.toList (β x), (fun x ↦ a x ⋯) = f
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α✝ : Type u_1
inst✝³ : FinEnum α✝
β : α✝ → Type u_2
inst✝² : (a : α✝) → FinEnum (β a)
p : Prop
inst✝¹ : Decidable p
α : p → Type
inst✝ : (hp : p) → FinEnum (α hp)
hp : p
x : (hp : p) → α hp
⊢ x ∈ map (fun x x_1 ↦ x) (FinEnum.toList (α hp))

Tactic:
simpa using

Goal state after:
α✝ : Type u_1
inst✝³ : FinEnum α✝
β : α✝ → Type u_2
inst✝² : (a : α✝) → FinEnum (β a)
p : Prop
inst✝¹ : Decidable p
α : p → Type
inst✝ : (hp : p) → FinEnum (α hp)
hp : p
x : (hp : p) → α hp
⊢ ∃ a, (fun x ↦ a) = x
Module: Mathlib.Data.Finite.Perm

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
hα : Nat.card α ≤ 2
⊢ Nat.card (Perm α) ∣ 2

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : Finite α
hα : Nat.card α ≤ 2
⊢ (Nat.card α)! ∣ 2
Module: Mathlib.Data.Finite.Perm

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
a b c : α
left✝² : a ∈ _root_.Set.univ
left✝¹ : b ∈ _root_.Set.univ
left✝ : c ∈ _root_.Set.univ
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
h : ∀ (a b : Perm α) (x : α), (a * b) x = (b * a) x
⊢ b = c

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : Finite α
a b c : α
left✝² : a ∈ _root_.Set.univ
left✝¹ : b ∈ _root_.Set.univ
left✝ : c ∈ _root_.Set.univ
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
h : ∀ (a b : Perm α) (x : α), (a * b) x = (b * a) x
⊢ b = c
Module: Mathlib.Data.List.Lookmap

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

Tactic:
simpa using

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

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

Tactic:
simpa using

Goal state after:
case cons.none
α : Type u_1
f : α → Option α
l₁ l₂ : List α
a : α
l₁✝ l₂✝ : List α
p : l₁✝ ~ l₂✝
IH : Pairwise (fun a b ↦ ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₁✝ → lookmap f l₁✝ ~ lookmap f l₂✝
H : Pairwise (fun a b ↦ ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) (a :: l₁✝)
h : f a = none
⊢ lookmap f l₁✝ ~ lookmap f l₂✝
Module: Mathlib.Data.List.Lookmap

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

Tactic:
simpa using

Goal state after:
case swap.none.none
α : Type u_1
f : α → Option α
l₁ l₂ : List α
a b : α
l : List α
H : Pairwise (fun a b ↦ ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) (b :: a :: l)
h₁ : f a = none
h₂ : f b = none
⊢ b :: a :: lookmap f l ~ a :: b :: lookmap f l
Module: Mathlib.Data.List.Lookmap

Goal state before:
pp: case swap.none.some
α : Type u_1
f : α → Option α
l₁ l₂ : List α
a b : α
l : List α
H : Pairwise (fun a b ↦ ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) (b :: a :: l)
h₁ : f a = none
d : α
h₂ : f b = some d
⊢ lookmap f (b :: a :: l) ~ lookmap f (a :: b :: l)

Tactic:
simpa using

Goal state after:
case swap.none.some
α : Type u_1
f : α → Option α
l₁ l₂ : List α
a b : α
l : List α
H : Pairwise (fun a b ↦ ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) (b :: a :: l)
h₁ : f a = none
d : α
h₂ : f b = some d
⊢ d :: a :: l ~ a :: d :: l
Module: Mathlib.Data.List.AList

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
c : Sigma β
l : List (Sigma β)
h : (c :: l).NodupKeys
⊢ { entries := c :: l, nodupKeys := h } = insert c.fst c.snd { entries := l, nodupKeys := ⋯ }

Tactic:
simpa using

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
c : Sigma β
l : List (Sigma β)
h : (c :: l).NodupKeys
⊢ l = kerase c.fst l
Module: Mathlib.Data.List.Lookmap

Goal state before:
pp: case swap.some.none
α : Type u_1
f : α → Option α
l₁ l₂ : List α
a b : α
l : List α
H : Pairwise (fun a b ↦ ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) (b :: a :: l)
c : α
h₁ : f a = some c
h₂ : f b = none
⊢ lookmap f (b :: a :: l) ~ lookmap f (a :: b :: l)

Tactic:
simpa using

Goal state after:
case swap.some.none
α : Type u_1
f : α → Option α
l₁ l₂ : List α
a b : α
l : List α
H : Pairwise (fun a b ↦ ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) (b :: a :: l)
c : α
h₁ : f a = some c
h₂ : f b = none
⊢ b :: c :: l ~ c :: b :: l
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
α' : Type u'
β : Type v
f : α → α'
hf : Function.Injective f
hd : (_ : α) × β
tl : List ((_ : α) × β)
ih : tl.NodupKeys → (map (Sigma.map f fun x ↦ id) tl).NodupKeys
nd : ¬hd.fst ∈ tl.keys ∧ tl.NodupKeys
h : (Sigma.map f (fun x ↦ id) hd).fst ∈ (map (Sigma.map f fun x ↦ id) tl).keys
⊢ hd.fst ∈ tl.keys

Tactic:
simp only [keys, map_map] at h ⊢
      obtain ⟨x, hm, he⟩ := mem_map.mp h
      exact mem_map.mpr ⟨x, hm, hf he⟩

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
⊢ IsEmpty ↑S'.toTop

Tactic:
simpa using

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
⊢ IsEmpty ↑S'.toTop
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
f : { f // ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1 }
i : α
x : β i
left✝¹ : ⟨i, x⟩.fst ∈ (↑f).1
hx : (↑f).2 ⟨i, x⟩.fst = some ⟨i, x⟩.snd
y : β i
left✝ : ⟨i, y⟩.fst ∈ (↑f).1
hy : (↑f).2 ⟨i, y⟩.fst = some ⟨i, y⟩.snd
⊢ ⟨i, x⟩ = ⟨i, y⟩

Tactic:
simpa using

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
f : { f // ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1 }
i : α
x : β i
left✝¹ : ⟨i, x⟩.fst ∈ (↑f).1
hx : (↑f).2 ⟨i, x⟩.fst = some ⟨i, x⟩.snd
y : β i
left✝ : ⟨i, y⟩.fst ∈ (↑f).1
hy : (↑f).2 ⟨i, y⟩.fst = some ⟨i, y⟩.snd
⊢ x = y
Module: Mathlib.Data.Finset.DenselyOrdered

Goal state before:
pp: case neg
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
s t : Finset α
inst✝² : NoMaxOrder α
inst✝¹ : NoMinOrder α
inst✝ : Nonempty α
H : ∀ x ∈ s, ∀ y ∈ t, x < y
hs : ¬s.Nonempty
ht : ¬t.Nonempty
⊢ ∃ b, (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y

Tactic:
exact Nonempty.elim ‹_› fun p ↦ ⟨p, by simp_all⟩

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a₁ a₂ : α
l : List (Sigma β)
h : a₁ ≠ a₂
p✝ : a₁ ∈ l.keys
w✝² : β a₂
w✝¹ w✝ : List (Sigma β)
left✝ : ¬a₂ ∈ w✝¹.keys
p : a₁ ∈ (w✝¹ ++ ⟨a₂, w✝²⟩ :: w✝).keys
q : a₂ ∈ (w✝¹ ++ ⟨a₂, w✝²⟩ :: w✝).keys
⊢ a₁ ∈ (w✝¹ ++ w✝).keys

Tactic:
simpa using

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a₁ a₂ : α
l : List (Sigma β)
h : a₁ ≠ a₂
p✝ : a₁ ∈ l.keys
w✝² : β a₂
w✝¹ w✝ : List (Sigma β)
left✝ : ¬a₂ ∈ w✝¹.keys
p : a₁ ∈ (w✝¹ ++ ⟨a₂, w✝²⟩ :: w✝).keys
q : a₂ ∈ (w✝¹ ++ ⟨a₂, w✝²⟩ :: w✝).keys
⊢ (∃ x, ⟨a₁, x⟩ ∈ w✝¹) ∨ ∃ x, ⟨a₁, x⟩ ∈ w✝
Module: Mathlib.Data.Finset.PiInduction

Goal state before:
pp: ι : 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)
ihs : ∀ t ⊂ univ.sigma f, ∀ (f : (i : ι) → Finset (α i)), univ.sigma f = t → p f
he : univ.sigma f = ∅
⊢ f = fun x ↦ ∅

Tactic:
simpa using

Goal state after:
ι : 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)
ihs : ∀ t ⊂ univ.sigma f, ∀ (f : (i : ι) → Finset (α i)), univ.sigma f = t → p f
he : univ.sigma f = ∅
⊢ ∀ (x : ι), f x = ∅
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s : Sigma β
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, b ∈ dlookup a (tail✝.kunion l₂) ↔ b ∈ dlookup a tail✝ ∨ ¬a ∈ tail✝.keys ∧ b ∈ dlookup a l₂
l₂ : List (Sigma β)
⊢ b ∈ dlookup a ((s :: tail✝).kunion l₂) ↔ b ∈ dlookup a (s :: tail✝) ∨ ¬a ∈ (s :: tail✝).keys ∧ b ∈ dlookup a l₂

Tactic:
obtain ⟨a'⟩ := s
    by_cases h₁ : a = a'
    · subst h₁
      simp
    · simp [h₁, @ih (kerase a' l₂)]

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

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝² : Zero M
inst✝¹ : DecidableEq α
inst✝ : DecidableEq M
l : AList fun _x ↦ M
⊢ l.lookupFinsupp.support = (filter (fun x ↦ decide (x.snd ≠ 0)) l.entries).keys.toFinset

Tactic:
dsimp only [lookupFinsupp]

Goal state after:
α : Type u_1
M : Type u_2
inst✝² : Zero M
inst✝¹ : DecidableEq α
inst✝ : DecidableEq M
l : AList fun _x ↦ M
⊢ (filter (fun x ↦ decide (x.snd ≠ 0)) l.entries).keys.toFinset =
    (filter (fun x ↦ decide (x.snd ≠ 0)) l.entries).keys.toFinset
Module: Mathlib.Data.Finsupp.AList

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x ↦ M
a : α
⊢ l.lookupFinsupp a = 0 ↔ a ∉ l ∨ 0 ∈ lookup a l

Tactic:
by
  rw [lookupFinsupp_apply, ← lookup_eq_none]
  rcases lookup a l with - | m <;> simp

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

Goal state before:
pp: case neg
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
a : α
h : ¬f a = 0
⊢ ⟨a, f a⟩ ∈ f.toAList.entries

Tactic:
simpa using

Goal state after:
case neg
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
a : α
h : ¬f a = 0
⊢ ¬f a = 0
Module: Mathlib.Data.Finsupp.NeLocus

Goal state before:
pp: α : Type u_1
N : Type u_3
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : Zero N
f g : α →₀ N
a : α
⊢ a ∈ f.neLocus g ↔ f a ≠ g a

Tactic:
simpa using

Goal state after:
α : Type u_1
N : Type u_3
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : Zero N
f g : α →₀ N
a : α
⊢ f a ≠ g a → f a ≠ 0 ∨ g a ≠ 0
Module: Mathlib.Data.Finsupp.NeLocus

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : DecidableEq α
inst✝³ : DecidableEq N
inst✝² : Zero N
inst✝¹ : DecidableEq M
inst✝ : Zero M
f g : α →₀ N
F : N → M
F0 : F 0 = 0
x : α
⊢ x ∈ (mapRange F F0 f).neLocus (mapRange F F0 g) → x ∈ f.neLocus g

Tactic:
simpa using

Goal state after:
α : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : DecidableEq α
inst✝³ : DecidableEq N
inst✝² : Zero N
inst✝¹ : DecidableEq M
inst✝ : Zero M
f g : α →₀ N
F : N → M
F0 : F 0 = 0
x : α
⊢ f x = g x → F (f x) = F (g x)
Module: Mathlib.Data.Finsupp.NeLocus

Goal state before:
pp: α : Type u_1
N : Type u_3
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : AddGroup N
f₁ f₂ g : α →₀ N
⊢ (f₁ - g).neLocus (f₂ - g) = f₁.neLocus f₂

Tactic:
simpa using

Goal state after:
α : Type u_1
N : Type u_3
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : AddGroup N
f₁ f₂ g : α →₀ N
⊢ (f₁ + -g).neLocus (f₂ + -g) = f₁.neLocus f₂
Module: Mathlib.Data.Finsupp.Sigma

Goal state before:
pp: κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst✝ : Zero M
k : κ
f g : ι k →₀ M
h : f.embSigma = g.embSigma
i : ι k
this : f.embSigma ⟨k, i⟩ = g.embSigma ⟨k, i⟩
⊢ f i = g i

Tactic:
simpa using

Goal state after:
κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst✝ : Zero M
k : κ
f g : ι k →₀ M
h : f.embSigma = g.embSigma
i : ι k
this : f.embSigma ⟨k, i⟩ = g.embSigma ⟨k, i⟩
⊢ f i = g i
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 ⊗ y ⊗ z) t = cast ⋯ (x ⊗ (y ⊗ z)) t

Tactic:
unfold mul

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.take.take * y t.take.drop * z t.drop = cast ⋯ (fun t ↦ x t.take * (y t.drop.take * z t.drop.drop)) t
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
d : ℕ
ds : List ℕ
inst✝ : Semiring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
b : ↥(Finset.range d)
a✝ : b ∈ (Finset.range d).attach
hbi : b ≠ ⟨i, ⋯⟩
⊢ i ≠ ↑b

Tactic:
simpa using

Goal state after:
α : Type
d : ℕ
ds : List ℕ
inst✝ : Semiring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
b : ↥(Finset.range d)
a✝ : b ∈ (Finset.range d).attach
hbi : b ≠ ⟨i, ⋯⟩
⊢ ¬i = ↑b
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
ds : List ℕ
inst✝¹ : Mul α
inst✝ : AddMonoid α
m n : ℕ
y x₁ x₂ : Holor α ds
hx₁ : x₁.CPRankMax1
hx₂ : CPRankMax m x₂
hy : CPRankMax n y
this : CPRankMax (m + n + 1) (x₁ + (x₂ + y))
⊢ CPRankMax (m + 1 + n) (x₁ + x₂ + y)

Tactic:
simpa using

Goal state after:
α : Type
ds : List ℕ
inst✝¹ : Mul α
inst✝ : AddMonoid α
m n : ℕ
y x₁ x₂ : Holor α ds
hx₁ : x₁.CPRankMax1
hx₂ : CPRankMax m x₂
hy : CPRankMax n y
this : CPRankMax (m + n + 1) (x₁ + (x₂ + y))
⊢ CPRankMax (m + (n + 1)) (x₁ + (x₂ + y))
Module: Mathlib.Data.Int.Lemmas

Goal state before:
pp: a b : ℤ
ha : a ≤ 0
hb : b ≤ 0
⊢ a.natAbs = b.natAbs ↔ a = b

Tactic:
simpa using

Goal state after:
a b : ℤ
ha : a ≤ 0
hb : b ≤ 0
⊢ a.natAbs = b.natAbs ↔ a = b
Module: Mathlib.Data.Int.Lemmas

Goal state before:
pp: a b : ℤ
ha : 0 ≤ a
hb : b ≤ 0
⊢ a.natAbs = b.natAbs ↔ a = -b

Tactic:
simpa using

Goal state after:
a b : ℤ
ha : 0 ≤ a
hb : b ≤ 0
⊢ a.natAbs = b.natAbs ↔ a = -b
Module: Mathlib.Data.Int.Lemmas

Goal state before:
pp: a b : ℤ
ha : a ≤ 0
hb : 0 ≤ b
⊢ a.natAbs = b.natAbs ↔ -a = b

Tactic:
simpa using

Goal state after:
a b : ℤ
ha : a ≤ 0
hb : 0 ≤ b
⊢ a.natAbs = b.natAbs ↔ -a = b
Module: Mathlib.Data.Int.Lemmas

Goal state before:
pp: a : ℤ
x✝ : a ∈ Iic 0
b : ℤ
hb : b ∈ Iic 0
hab : a < b
⊢ b.natAbs < a.natAbs

Tactic:
simpa using

Goal state after:
a : ℤ
x✝ : a ∈ Iic 0
b : ℤ
hb : b ∈ Iic 0
hab : a < b
⊢ b.natAbs < a.natAbs
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
inst✝ : Semiring α
d : ℕ
ds : List ℕ
x : Holor α (d :: ds)
h_summands : ∀ (i : ↥(Finset.range d)), CPRankMax ds.prod (unitVec d ↑i ⊗ x.slice ↑i ⋯)
h_dds_prod : (d :: ds).prod = (Finset.range d).card * ds.prod
this : CPRankMax ((Finset.range d).attach.card * ds.prod) (∑ i ∈ (Finset.range d).attach, unitVec d ↑i ⊗ x.slice ↑i ⋯)
h_cprankMax_sum :
  CPRankMax ((Finset.range d).card * ds.prod) (∑ i ∈ (Finset.range d).attach, unitVec d ↑i ⊗ x.slice ↑i ⋯)
⊢ CPRankMax (d :: ds).prod (∑ i ∈ (Finset.range d).attach, unitVec d ↑i ⊗ x.slice ↑i ⋯)

Tactic:
rw [h_dds_prod]

Goal state after:
α : Type
inst✝ : Semiring α
d : ℕ
ds : List ℕ
x : Holor α (d :: ds)
h_summands : ∀ (i : ↥(Finset.range d)), CPRankMax ds.prod (unitVec d ↑i ⊗ x.slice ↑i ⋯)
h_dds_prod : (d :: ds).prod = (Finset.range d).card * ds.prod
this : CPRankMax ((Finset.range d).attach.card * ds.prod) (∑ i ∈ (Finset.range d).attach, unitVec d ↑i ⊗ x.slice ↑i ⋯)
h_cprankMax_sum :
  CPRankMax ((Finset.range d).card * ds.prod) (∑ i ∈ (Finset.range d).attach, unitVec d ↑i ⊗ x.slice ↑i ⋯)
⊢ CPRankMax ((Finset.range d).card * ds.prod) (∑ i ∈ (Finset.range d).attach, unitVec d ↑i ⊗ x.slice ↑i ⋯)
Module: Mathlib.Data.Int.CardIntervalMod

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

Tactic:
simp only [mem_map, mem_filter, mem_Ioc, floor_lt, le_floor, div_lt_iff₀, le_div_iff₀,
    dvd_iff_exists_eq_mul_left, cast_pos.2 hr, ← cast_mul, cast_lt, cast_le]

Goal state after:
a b r : ℤ
hr : 0 < r
x : ℤ
⊢ ((a < x ∧ x ≤ b) ∧ ∃ c, x = c * r) ↔
    ∃ a_1, (a < a_1 * r ∧ a_1 * r ≤ b) ∧ { toFun := fun x ↦ x * r, inj' := ⋯ } a_1 = x
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
phh' : ¬p head = true
⊢ (!p head) = true

Tactic:
simpa using

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
⊢ p head = false
Module: Mathlib.Data.List.TakeWhile

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

Tactic:
simpa using

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

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
h : ∃ x, x ∈ l ∧ p x = true
⊢ dropWhile (fun x ↦ !p x) l ≠ []

Tactic:
simpa using

Goal state after:
α : Type u_1
p : α → Bool
l : List α
h : ∃ x, x ∈ l ∧ p x = true
⊢ ∃ x, x ∈ l ∧ p x = true
Module: Mathlib.Data.List.TakeWhile

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
h : ∃ x, x ∈ l ∧ ¬p x = true
⊢ dropWhile p l ≠ []

Tactic:
simpa using

Goal state after:
α : Type u_1
p : α → Bool
l : List α
h : ∃ x, x ∈ l ∧ ¬p x = true
⊢ ∃ x, x ∈ l ∧ p x = false
Module: Mathlib.Data.List.TakeWhile

Goal state before:
pp: case convert_2
α : Type u_1
p : α → Bool
l : List α
h : ∃ x, x ∈ l ∧ ¬p x = true
⊢ ∃ x, x ∈ l ∧ (!p x) = true

Tactic:
simpa using

Goal state after:
case convert_2
α : Type u_1
p : α → Bool
l : List α
h : ∃ x, x ∈ l ∧ ¬p x = true
⊢ ∃ x, x ∈ l ∧ p x = false
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: n m l : ℕ
this : n ≤ l ∧ l < n + (m - n) ↔ n ≤ l ∧ l < m
⊢ l ∈ Ico n m ↔ n ≤ l ∧ l < m

Tactic:
simp [Ico, this]

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

Goal state before:
pp: n m k : ℕ
⊢ range' (k + n) (m - n) = range' (n + k) (m - n)

Tactic:
Nat.add_comm n k

Goal state after:
n m k : ℕ
⊢ range' (k + n) (m - n) = range' (k + n) (m - n)
Module: Mathlib.Data.List.ModifyLast

Goal state before:
pp: case cons
α : Type u_1
f : α → α
a head✝ : α
tl : List α
⊢ (#[].push head✝).toListAppend (modifyLast.go f (tl ++ [a]) #[]) = head✝ :: (tl ++ [f a])

Tactic:
Array.toListAppend_eq,

Goal state after:
case cons
α : Type u_1
f : α → α
a head✝ : α
tl : List α
⊢ (#[].push head✝).toList ++ modifyLast.go f (tl ++ [a]) #[] = head✝ :: (tl ++ [f a])
Module: Mathlib.Data.List.Palindrome

Goal state before:
pp: α : Type u_1
l : List α
⊢ (l ++ l.reverse).Palindrome

Tactic:
by
  apply of_reverse_eq
  rw [reverse_append, reverse_reverse]

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

Goal state before:
pp: case cons.succ.succ.refine_1
α : Type u_1
x hd : α
tl : List α
IH :
  ¬x ∈ tl →
    ∀ ⦃n : ℕ⦄,
      n ∈ {n | n ≤ tl.length} →
        ∀ ⦃m : ℕ⦄, m ∈ {n | n ≤ tl.length} → (fun k ↦ tl.insertIdx k x) n = (fun k ↦ tl.insertIdx k x) m → n = m
hx : ¬x = hd ∧ ¬x ∈ tl
n✝¹ : ℕ
hn : n✝¹ + 1 ≤ tl.length + 1
n✝ : ℕ
hm : n✝ + 1 ≤ tl.length + 1
h : tl.insertIdx n✝¹ x = tl.insertIdx n✝ x
⊢ n✝¹ ∈ {n | n ≤ tl.length}

Tactic:
simpa using

Goal state after:
case cons.succ.succ.refine_1
α : Type u_1
x hd : α
tl : List α
IH :
  ¬x ∈ tl →
    ∀ ⦃n : ℕ⦄,
      n ∈ {n | n ≤ tl.length} →
        ∀ ⦃m : ℕ⦄, m ∈ {n | n ≤ tl.length} → (fun k ↦ tl.insertIdx k x) n = (fun k ↦ tl.insertIdx k x) m → n = m
hx : ¬x = hd ∧ ¬x ∈ tl
n✝¹ : ℕ
hn : n✝¹ + 1 ≤ tl.length + 1
n✝ : ℕ
hm : n✝ + 1 ≤ tl.length + 1
h : tl.insertIdx n✝¹ x = tl.insertIdx n✝ x
⊢ n✝¹ ≤ tl.length
Module: Mathlib.Data.List.Lemmas

Goal state before:
pp: case cons.succ.succ.refine_2
α : Type u_1
x hd : α
tl : List α
IH :
  ¬x ∈ tl →
    ∀ ⦃n : ℕ⦄,
      n ∈ {n | n ≤ tl.length} →
        ∀ ⦃m : ℕ⦄, m ∈ {n | n ≤ tl.length} → (fun k ↦ tl.insertIdx k x) n = (fun k ↦ tl.insertIdx k x) m → n = m
hx : ¬x = hd ∧ ¬x ∈ tl
n✝¹ : ℕ
hn : n✝¹ + 1 ≤ tl.length + 1
n✝ : ℕ
hm : n✝ + 1 ≤ tl.length + 1
h : tl.insertIdx n✝¹ x = tl.insertIdx n✝ x
⊢ n✝ ∈ {n | n ≤ tl.length}

Tactic:
simpa using

Goal state after:
case cons.succ.succ.refine_2
α : Type u_1
x hd : α
tl : List α
IH :
  ¬x ∈ tl →
    ∀ ⦃n : ℕ⦄,
      n ∈ {n | n ≤ tl.length} →
        ∀ ⦃m : ℕ⦄, m ∈ {n | n ≤ tl.length} → (fun k ↦ tl.insertIdx k x) n = (fun k ↦ tl.insertIdx k x) m → n = m
hx : ¬x = hd ∧ ¬x ∈ tl
n✝¹ : ℕ
hn : n✝¹ + 1 ≤ tl.length + 1
n✝ : ℕ
hm : n✝ + 1 ≤ tl.length + 1
h : tl.insertIdx n✝¹ x = tl.insertIdx n✝ x
⊢ n✝ ≤ tl.length
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: n m : ℕ
hnm : n < m
x✝¹ : ℕ
x✝ : x✝¹ ∈ Ico n m
⊢ decide (x✝¹ ≤ n) = decide (x✝¹ < n + 1)

Tactic:
simpa using

Goal state after:
n m : ℕ
hnm : n < m
x✝¹ : ℕ
x✝ : x✝¹ ∈ Ico n m
⊢ x✝¹ ≤ n ↔ x✝¹ < n + 1