mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.List.Find

Goal state before:
pp: case nil
α : Type u_1
p : α → Bool
l₁ l₂ : List α
hp : {x | x ∈ [] ∧ p x = true}.Subsingleton
⊢ find? p [] = find? p []

Tactic:
rfl

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

Goal state before:
pp: case cons
α : Type u_1
p : α → Bool
l₁ l₂ : List α
x : α
l₁✝ l₂✝ : List α
a✝ : l₁✝ ~ l₂✝
ih : {x | x ∈ l₁✝ ∧ p x = true}.Subsingleton → find? p l₁✝ = find? p l₂✝
hp : {x_1 | x_1 ∈ x :: l₁✝ ∧ p x_1 = true}.Subsingleton
⊢ find? p (x :: l₁✝) = find? p (x :: l₂✝)

Tactic:
grind

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

Goal state before:
pp: case pos
α : Type u_1
p : α → Bool
l₁ l₂ : List α
x y : α
l : List α
hp : ∀ ⦃x_1 : α⦄, x_1 ∈ y :: x :: l ∧ p x_1 = true → ∀ ⦃y_1 : α⦄, y_1 ∈ y :: x :: l ∧ p y_1 = true → x_1 = y_1
h✝ : p x = true
⊢ find? p (y :: x :: l) = find? p (x :: y :: l)

Tactic:
by_cases p y

Goal state after:
case pos
α : Type u_1
p : α → Bool
l₁ l₂ : List α
x y : α
l : List α
hp : ∀ ⦃x_1 : α⦄, x_1 ∈ y :: x :: l ∧ p x_1 = true → ∀ ⦃y_1 : α⦄, y_1 ∈ y :: x :: l ∧ p y_1 = true → x_1 = y_1
h✝¹ : p x = true
h✝ : p y = true
⊢ find? p (y :: x :: l) = find? p (x :: y :: l)

case neg
α : Type u_1
p : α → Bool
l₁ l₂ : List α
x y : α
l : List α
hp : ∀ ⦃x_1 : α⦄, x_1 ∈ y :: x :: l ∧ p x_1 = true → ∀ ⦃y_1 : α⦄, y_1 ∈ y :: x :: l ∧ p y_1 = true → x_1 = y_1
h✝¹ : p x = true
h✝ : ¬p y = true
⊢ find? p (y :: x :: l) = find? p (x :: y :: l)
Module: Mathlib.Data.List.Find

Goal state before:
pp: case neg
α : Type u_1
p : α → Bool
l₁ l₂ : List α
x y : α
l : List α
hp : ∀ ⦃x_1 : α⦄, x_1 ∈ y :: x :: l ∧ p x_1 = true → ∀ ⦃y_1 : α⦄, y_1 ∈ y :: x :: l ∧ p y_1 = true → x_1 = y_1
h✝ : ¬p x = true
⊢ find? p (y :: x :: l) = find? p (x :: y :: l)

Tactic:
by_cases p y

Goal state after:
case pos
α : Type u_1
p : α → Bool
l₁ l₂ : List α
x y : α
l : List α
hp : ∀ ⦃x_1 : α⦄, x_1 ∈ y :: x :: l ∧ p x_1 = true → ∀ ⦃y_1 : α⦄, y_1 ∈ y :: x :: l ∧ p y_1 = true → x_1 = y_1
h✝¹ : ¬p x = true
h✝ : p y = true
⊢ find? p (y :: x :: l) = find? p (x :: y :: l)

case neg
α : Type u_1
p : α → Bool
l₁ l₂ : List α
x y : α
l : List α
hp : ∀ ⦃x_1 : α⦄, x_1 ∈ y :: x :: l ∧ p x_1 = true → ∀ ⦃y_1 : α⦄, y_1 ∈ y :: x :: l ∧ p y_1 = true → x_1 = y_1
h✝¹ : ¬p x = true
h✝ : ¬p y = true
⊢ find? p (y :: x :: l) = find? p (x :: y :: l)
Module: Mathlib.Data.List.Find

Goal state before:
pp: case pos
α : Type u_1
p : α → Bool
l₁ l₂ : List α
x y : α
l : List α
hp : ∀ ⦃x_1 : α⦄, x_1 ∈ y :: x :: l ∧ p x_1 = true → ∀ ⦃y_1 : α⦄, y_1 ∈ y :: x :: l ∧ p y_1 = true → x_1 = y_1
h✝¹ : p x = true
h✝ : p y = true
⊢ find? p (y :: x :: l) = find? p (x :: y :: l)

Tactic:
grind

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

Goal state before:
pp: case neg
α : Type u_1
p : α → Bool
l₁ l₂ : List α
x y : α
l : List α
hp : ∀ ⦃x_1 : α⦄, x_1 ∈ y :: x :: l ∧ p x_1 = true → ∀ ⦃y_1 : α⦄, y_1 ∈ y :: x :: l ∧ p y_1 = true → x_1 = y_1
h✝¹ : p x = true
h✝ : ¬p y = true
⊢ find? p (y :: x :: l) = find? p (x :: y :: l)

Tactic:
grind

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

Goal state before:
pp: case pos
α : Type u_1
p : α → Bool
l₁ l₂ : List α
x y : α
l : List α
hp : ∀ ⦃x_1 : α⦄, x_1 ∈ y :: x :: l ∧ p x_1 = true → ∀ ⦃y_1 : α⦄, y_1 ∈ y :: x :: l ∧ p y_1 = true → x_1 = y_1
h✝¹ : ¬p x = true
h✝ : p y = true
⊢ find? p (y :: x :: l) = find? p (x :: y :: l)

Tactic:
grind

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

Goal state before:
pp: case neg
α : Type u_1
p : α → Bool
l₁ l₂ : List α
x y : α
l : List α
hp : ∀ ⦃x_1 : α⦄, x_1 ∈ y :: x :: l ∧ p x_1 = true → ∀ ⦃y_1 : α⦄, y_1 ∈ y :: x :: l ∧ p y_1 = true → x_1 = y_1
h✝¹ : ¬p x = true
h✝ : ¬p y = true
⊢ find? p (y :: x :: l) = find? p (x :: y :: l)

Tactic:
grind

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

Goal state before:
pp: case trans.refine_1
α : Type u_1
p : α → Bool
l₁ l₂ l₁✝ l₂✝ l₃✝ : List α
a✝¹ : l₁✝ ~ l₂✝
a✝ : l₂✝ ~ l₃✝
ih1 : {x | x ∈ l₁✝ ∧ p x = true}.Subsingleton → find? p l₁✝ = find? p l₂✝
ih2 : {x | x ∈ l₂✝ ∧ p x = true}.Subsingleton → find? p l₂✝ = find? p l₃✝
hp : {x | x ∈ l₁✝ ∧ p x = true}.Subsingleton
⊢ {x | x ∈ l₁✝ ∧ p x = true}.Subsingleton

Tactic:
grind

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

Goal state before:
pp: case trans.refine_2
α : Type u_1
p : α → Bool
l₁ l₂ l₁✝ l₂✝ l₃✝ : List α
a✝¹ : l₁✝ ~ l₂✝
a✝ : l₂✝ ~ l₃✝
ih1 : {x | x ∈ l₁✝ ∧ p x = true}.Subsingleton → find? p l₁✝ = find? p l₂✝
ih2 : {x | x ∈ l₂✝ ∧ p x = true}.Subsingleton → find? p l₂✝ = find? p l₃✝
hp : {x | x ∈ l₁✝ ∧ p x = true}.Subsingleton
⊢ {x | x ∈ l₂✝ ∧ p x = true}.Subsingleton

Tactic:
grind

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

Goal state before:
pp: case nil
α : Type u_1
p₁ p₂ : α → Bool
h : ∀ (x : α), x ∈ [] → p₁ x = p₂ x
⊢ find? p₁ [] = find? p₂ []

Tactic:
grind

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

Goal state before:
pp: case cons
α : Type u_1
p₁ p₂ : α → Bool
head✝ : α
tail✝ : List α
tail_ih✝ : (∀ (x : α), x ∈ tail✝ → p₁ x = p₂ x) → find? p₁ tail✝ = find? p₂ tail✝
h : ∀ (x : α), x ∈ head✝ :: tail✝ → p₁ x = p₂ x
⊢ find? p₁ (head✝ :: tail✝) = find? p₂ (head✝ :: tail✝)

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
hp : {x | x ∈ a ::ₘ s ∧ p x}.Subsingleton
h : ¬p a
⊢ {x | x ∈ s ∧ p x}.Subsingleton

Tactic:
grind

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

Goal state before:
pp: case h
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a : α
a✝ : List α
hp : {x | x ∈ a ::ₘ ⟦a✝⟧ ∧ p x}.Subsingleton
⊢ find? p ↑(a :: a✝) ⋯ = if h : p a then some a else find? p ↑a✝ ⋯

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s t : Multiset α
hp : {x | x ∈ s + t ∧ p x}.Subsingleton
⊢ {x | x ∈ s ∧ p x} ⊆ {x | x ∈ s + t ∧ p x}

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s t : Multiset α
hp : {x | x ∈ s + t ∧ p x}.Subsingleton
⊢ {x | x ∈ t ∧ p x} ⊆ {x | x ∈ s + t ∧ p x}

Tactic:
grind

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

Goal state before:
pp: case cons.isTrue
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a x : α
s : Multiset α
ih : ∀ (hp : {x | x ∈ s ∧ p x}.Subsingleton), find? p s hp = some a ↔ a ∈ s ∧ p a
hp : ∀ ⦃y : α⦄, y ∈ x ::ₘ s ∧ p y → x = y
h✝ : p x
⊢ some x = some a ↔ a ∈ x ::ₘ s ∧ p a

Tactic:
grind

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

Goal state before:
pp: case cons.isFalse
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a x : α
s : Multiset α
ih : ∀ (hp : {x | x ∈ s ∧ p x}.Subsingleton), find? p s hp = some a ↔ a ∈ s ∧ p a
hp : {x_1 | x_1 ∈ x ::ₘ s ∧ p x_1}.Subsingleton
h✝ : ¬p x
⊢ a ∈ s ∧ p a ↔ a ∈ x ::ₘ s ∧ p a

Tactic:
grind

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

Goal state before:
pp: case cons
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
x : α
s : Multiset α
ih : ∀ (hp : {x | x ∈ s ∧ p x}.Subsingleton), find? p s hp = none ↔ ∀ (a : α), a ∈ s → ¬p a
hp : ∀ ⦃x_1 : α⦄, x_1 ∈ x ::ₘ s ∧ p x_1 → ∀ ⦃y : α⦄, y ∈ x ::ₘ s ∧ p y → x_1 = y
⊢ (if h : p x then some x else find? p s ⋯) = none ↔ ∀ (a : α), a ∈ x ::ₘ s → ¬p a

Tactic:
grind

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: M : Type u_4
M₂ : Type u_5
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M₂
R : Type u_8
R₂ : Type u_9
inst✝⁴ : Semiring R
inst✝³ : Ring R₂
τ₁₂ : R →+* R₂
inst✝² : RingHomSurjective τ₁₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
ι : Type u_10
s : Set ι
hs : s.Nonempty
p : ι → Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
hf : f.range = ⨆ i ∈ s, p i
this : ⨆ i ∈ s, comap f.range.subtype (p i) = ⊤
⊢ ⨆ i ∈ s, comap f (p i) = ⨆ i ∈ s, comap f.rangeRestrict (comap f.range.subtype (p i))

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝ : Zero M
s : Set α
f : α →₀ M
⊢ ↑f.support ⊆ s ↔ ∀ a ∉ s, f a = 0

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝ : Zero M
s : Finset α
f : α → M
hf : ∀ (a : α), f a ≠ 0 → a ∈ s
⊢ (onFinset s f hf).support ⊆ s

Tactic:
grind

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

Goal state before:
pp: ι : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : Zero M
inst✝ : Zero N
e : M → N
he0 : e 0 = 0
f : ι →₀ M
he : Injective e
⊢ (mapRange e he0 f).support = f.support

Tactic:
grind

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

Goal state before:
pp: case mp
α : Type u_1
M : Type u_4
N : Type u_5
inst✝¹ : Zero M
inst✝ : Zero N
e : M → N
he₀ : e 0 = 0
g : α →₀ N
⊢ (∃ y, mapRange e he₀ y = g) → ∀ (i : α), ∃ y, e y = g i

Tactic:
grind

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

Goal state before:
pp: case h
α : Type u_1
M : Type u_4
N : Type u_5
inst✝¹ : Zero M
inst✝ : Zero N
e : M → N
he₀ : e 0 = 0
g : α →₀ N
f : α → M
h : ∀ (i : α), e (f i) = g i
⊢ mapRange e he₀ (onFinset g.support (fun x ↦ if x ∈ g.support then f x else 0) ⋯) = g

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
v : α →₀ M
b : β
this : DecidableEq β
x : α
⊢ x ∈ {x | x ∈ v.support.val ∧ f x = b} → ∀ ⦃y : α⦄, y ∈ {x | x ∈ v.support.val ∧ f x = b} → x = y

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
v : α →₀ M
a₂ : β
⊢ a₂ ∈ map f v.support ↔
    (match Multiset.find? (fun a ↦ f a = a₂) v.support.val ⋯ with
      | some a => v a
      | none => 0) ≠
      0

Tactic:
grind

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
M : Type u_4
inst✝ : Zero M
f : α ↪ β
v : α →₀ M
b : β
h✝ : ∃ a, f a = b
⊢ (match Multiset.find? (fun a ↦ f a = b) v.support.val ⋯ with
    | some a => v a
    | none => 0) =
    v h✝.choose

Tactic:
grind

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
M : Type u_4
inst✝ : Zero M
f : α ↪ β
v : α →₀ M
b : β
h✝ : ¬∃ a, f a = b
⊢ (match Multiset.find? (fun a ↦ f a = b) v.support.val ⋯ with
    | some a => v a
    | none => 0) =
    0

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_4
inst✝ : Zero M
f : α ↪ β
v : α →₀ M
a : α
⊢ (match Multiset.find? (fun a_1 ↦ f a_1 = f a) v.support.val ⋯ with
    | some a => v a
    | none => 0) =
    v a

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_4
N : Type u_5
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
g : M → N
p : α →₀ M
hg : g 0 = 0
⊢ embDomain f (mapRange g hg p) = mapRange g hg (embDomain f p)

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H✝ : Type u_8
inst✝² : Zero M
inst✝¹ : Zero N
inst✝ : Zero O
f : M → N → O
hf : f 0 0 = 0
g₁ : α →₀ M
g₂ : α →₀ N
a : α
H : f (g₁ a) (g₂ a) ≠ 0
⊢ a ∈ g₁.support ∪ g₂.support

Tactic:
grind

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
σ₁₂ : R →+* R₂
s : Set M
f g : M →ₛₗ[σ₁₂] M₂
⊢ s ⊆ ↑(f.eqLocus g) ↔ Set.EqOn (⇑f) (⇑g) s

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝⁴ : Ring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.IsTorsionFree R M
x : M
h : x ≠ 0
t : R
⊢ (toSpanNonzeroSingleton R M x h) t = ⟨t • x, ⋯⟩

Tactic:
rfl

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
g : ι → α
this :
  (Function.support g ⊆ ↑s ∧ ∀ (i : ι) (hi : i ∈ s), f i hi = g i) ↔
    ∀ (i : ι), if hi : i ∈ s then f i hi = g i else g i = 0
⊢ (∀ (x : ι), g x = if hi : x ∈ s then f x hi else 0) ↔ ∀ (i : ι), if hi : i ∈ s then f i hi = g i else g i = 0

Tactic:
grind

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
g : ι → α
⊢ (∀ (i : ι), if hi : i ∈ s then f i hi = g i else g i = 0) ↔ (∀ (i : ι) (hi : i ∈ s), f i hi = g i) ∧ ∀ i ∉ s, g i = 0

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a✝ a'✝ : α
b✝ : M
a : α
b : M
a' : α
⊢ (a' ∈ if b = 0 then ∅ else {a}) ↔ Pi.single a b a' ≠ 0

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
a a' : α
b : M
⊢ single a ((single a' b) a) = (single a' (single a' b)) a

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
b : M
⊢ (single a b).support ⊆ {a}

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
b : M
x : α
⊢ (single a b) x ∈ {0, b}

Tactic:
grind

Goal state after:
Module: Mathlib.Algebra.Group.Finsupp

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
a : ι
b : M
f : ι →₀ M
ha : a ∉ f.support
hb : b ≠ 0
⊢ (single a b + f).support = cons a f.support ha

Tactic:
classical
  have H := support_single a hb
  rw [support_add_eq, H, cons_eq_insert, insert_eq]
  rwa [H, disjoint_singleton_left]

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
a : α
h : f.support ⊆ {a}
x : α
⊢ f x = (single a (f a)) x

Tactic:
by_cases hx : x = a

Goal state after:
case pos
α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
a : α
h : f.support ⊆ {a}
x : α
hx : x = a
⊢ f x = (single a (f a)) x

case neg
α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
a : α
h : f.support ⊆ {a}
x : α
hx : ¬x = a
⊢ f x = (single a (f a)) x
Module: Mathlib.Data.Finsupp.Single

Goal state before:
pp: case pos
α : Type u_1
M : Type u_5
inst✝ : Zero M
a₁ a₂ : α
b₁ b₂ : M
eq : single a₁ b₁ = single a₂ b₂
h : a₁ = a₂
⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0

Tactic:
refine Or.inl ⟨h, ?_⟩
      rwa [h, (single_injective a₂).eq_iff] at eq

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

Goal state before:
pp: case neg
α : Type u_1
M : Type u_5
inst✝ : Zero M
a₁ a₂ : α
b₁ b₂ : M
eq : ∀ (x : α), (single a₁ b₁) x = (single a₂ b₂) x
h : ¬a₁ = a₂
h₁ : (single a₁ b₁) a₁ = (single a₂ b₂) a₁
h₂ : (single a₁ b₁) a₂ = (single a₂ b₂) a₂
⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0

Tactic:
grind

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

Goal state before:
pp: case mpr
α : Type u_1
M : Type u_5
inst✝ : Zero M
a₁ a₂ : α
b₁ b₂ : M
⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0 → single a₁ b₁ = single a₂ b₂

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
N : Type u_7
P : Type u_8
inst✝¹ : Zero N
inst✝ : Zero P
e : N → P
he : e 0 = 0
a : α
n : N
b : α
⊢ e ((single a n) b) = (single a (e n)) b

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
f✝ : α →₀ M
a✝ : α
b✝ : M
i✝ : α
f : α →₀ M
a : α
b : M
i : α
⊢ (i ∈ if b = 0 then f.support.erase a else insert a f.support) ↔ Function.update (⇑f) a b i ≠ 0

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝¹ : Zero M
f : α →₀ M
a : α
b : M
i : α
inst✝ : DecidableEq α
⊢ { support := if b = 0 then f.support.erase a else insert a f.support,
        toFun := fun a_1 ↦ if h : a_1 = a then ⋯ ▸ b else f a_1, mem_support_toFun := ⋯ }
      i =
    if i = a then b else f i

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝¹ : Zero M
f : α →₀ M
a : α
b : M
inst✝ : DecidableEq α
⊢ ⇑(f.update a b) = Function.update (⇑f) a b

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
a : α
⊢ f.update a (f a) = f

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝² : Zero M
f : α →₀ M
a : α
b : M
inst✝¹ : DecidableEq α
inst✝ : DecidableEq M
⊢ (f.update a b).support = if b = 0 then f.support.erase a else insert a f.support

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝¹ : Zero M
f : α →₀ M
a : α
inst✝ : DecidableEq α
⊢ (f.update a 0).support = f.support.erase a

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝¹ : Zero M
f : α →₀ M
a : α
b : M
inst✝ : DecidableEq α
h : b ≠ 0
⊢ (f.update a b).support = insert a f.support

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝¹ : Zero M
f : α →₀ M
a : α
b : M
inst✝ : DecidableEq α
⊢ (f.update a b).support ⊆ insert a f.support

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
a₁ a₂ : α
h : a₁ ≠ a₂
m₁ m₂ : M
⊢ (f.update a₁ m₁).update a₂ m₂ = (f.update a₂ m₂).update a₁ m₁

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
a : α
b c : M
⊢ (f.update a b).update a c = f.update a c

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a : α
f : α →₀ M
a' : α
⊢ a' ∈ f.support.erase a ↔ (if a' = a then 0 else f a') ≠ 0

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝¹ : Zero M
inst✝ : DecidableEq α
a : α
f : α →₀ M
⊢ (erase a f).support = f.support.erase a

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
f : α →₀ M
⊢ (erase a f) a = 0

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
a a' : α
f : α →₀ M
h : a' ≠ a
⊢ (erase a f) a' = f a'

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
b : M
⊢ erase a (single a b) = 0

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
a a' : α
b : M
h : a ≠ a'
⊢ erase a (single a' b) = single a' b

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
a : α
haf : a ∉ f.support
⊢ erase a f = f

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
a : α
⊢ erase a f = f.update a 0

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
a a' : α
ha : a ≠ a'
b : M
⊢ erase a (f.update a' b) = (erase a f).update a' b

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
a : α
⊢ erase a (erase a f) = erase a f

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
a : α
b : M
⊢ (erase a f).update a b = f.update a b

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
a : α
b : M
⊢ erase a (f.update a b) = erase a f

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
M : Type u_5
N : Type u_7
inst✝¹ : Zero M
inst✝ : Zero N
f : M → N
hf : f 0 = 0
a : α
b : M
⊢ mapRange f hf (single a b) = single a (f b)

Tactic:
grind

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

Goal state before:
pp: case h.left
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
h_map_support : map f l.support = {a}
ha : a ∈ map f l.support
c : α
_hc₁ : c ∈ l.support
hc₂ : f c = a
d : α
⊢ (single a b) (f d) = (single c b) d

Tactic:
grind

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ↪ β
a : α
m : M
b : β
h : b ∈ Set.range ⇑f
⊢ (embDomain f (single a m)) b = (single (f a) m) b

Tactic:
grind

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ↪ β
a : α
m : M
b : β
h : b ∉ Set.range ⇑f
⊢ (embDomain f (single a m)) b = (single (f a) m) b

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
M : Type u_5
N : Type u_7
P : Type u_8
inst✝² : Zero M
inst✝¹ : Zero N
inst✝ : Zero P
f : M → N → P
hf : f 0 0 = 0
a : α
m : M
n : N
⊢ zipWith f hf (single a m) (single a n) = single a (f m n)

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
a : α
m : M
b : α
⊢ (single (Option.some a) m).some b = (single a m) b

Tactic:
simp [single_apply]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Indicator

Goal state before:
pp: case pos
ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
s : Set ι
f g : ι → M₀
x✝ : ι
h✝ : x✝ ∈ s
⊢ f x✝ * g x✝ = f x✝ * g x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Indicator

Goal state before:
pp: case pos
ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
i : ι
s : Set ι
f g : ι → M₀
h✝ : i ∈ s
⊢ f i * g i = f i * g i

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
ι : Type u_2
M : Type u_8
inst✝ : AddCommMonoid M
s : Finset ι
f : ι → M
a : α
⊢ (Multiset.map (single a ∘ fun b ↦ f b) s.val).sum = ∑ b ∈ s, single a (f b)

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: case empty
α : Type u_1
β : Type u_7
M : Type u_8
inst✝¹ : DecidableEq β
inst✝ : AddCommMonoid M
f : α → β →₀ M
⊢ (∅.sum f).support ⊆ ∅.sup fun x ↦ (f x).support

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.FiniteSupport.Basic

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝¹ : One M
β : Type u_3
f : β → M
g : α → β
inst✝ : One β
hfg : HasFiniteMulSupport (f ∘ g)
h : f 1 = 1
hf : Injective f
x✝ : α
ha : x✝ ∈ mulSupport g
H : (f ∘ g) x✝ = 1
⊢ g x✝ = 1

Tactic:
grind

Goal state after:
Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: R : Type u_5
inst✝² : Semiring R
S : Type u_6
inst✝¹ : Semiring S
inst✝ : PartialOrder S
v : AbsoluteValue R S
⊢ (∀ (x : R), x ≠ 0 → v x = 1) ↔ ∀ (x : R), x ≠ 0 → v x = 1

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset

Goal state before:
pp: case zero
α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : Preorder α
s t : Multiset α
inst✝ : MulLeftMono α
⊢ prod 0 ≤ prod 0

Tactic:
rfl

Goal state after: