mathlib-initiative/mathlib-tactics huggingface dataset:
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)

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:
<;>

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
⊢ 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
⊢ 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)

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)

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)

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:
<;>

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)

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 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

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:
<;>

Goal state after:
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

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
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case mp
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
⊢ ComplementedLattice α → IsAtomistic α

pp: case mpr
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
⊢ IsAtomistic α → ComplementedLattice α

Tactic:
<;>

Goal state after:
case mp
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
⊢ ComplementedLattice α → IsAtomistic α

case mpr
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
⊢ IsAtomistic α → ComplementedLattice α
Module: Mathlib.Data.Finsupp.Defs

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝ : Zero M
f g : α →₀ M
x✝ : f.support = g.support ∧ ∀ x ∈ f.support, f x = g x
h₁ : f.support = g.support
h₂ : ∀ x ∈ f.support, f x = g x
a : α
h : a ∉ f.support
hf : f a = 0
⊢ g a = 0

Tactic:
rwa [h₁, notMem_support_iff] at h

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

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:
<;>

Goal state after:
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

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
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: case inr
R : Type u_4
inst✝ : CommRing R
n k : ℕ
hnk : n ∈ range k
⊢ ↑(n - n) = 0

pp: case inr
R : Type u_4
inst✝ : CommRing R
n k : ℕ
hnk : n ∈ range k
⊢ ↑n - ↑n = 0

Tactic:
<;>

Goal state after:
case inr
R : Type u_4
inst✝ : CommRing R
n k : ℕ
hnk : n ∈ range k
⊢ ↑(n - n) = 0

case inr
R : Type u_4
inst✝ : CommRing R
n k : ℕ
hnk : n ∈ range k
⊢ ↑n - ↑n = 0
Module: Mathlib.Data.Finsupp.Indicator

Goal state before:
pp: case pos
ι : Type u_1
α : Type u_2
inst✝ : Zero α
a : ι
f : (j : ι) → j ∈ {a} → α
j : ι
h : j = a
⊢ f j ⋯ = f a ⋯

pp: case neg
ι : Type u_1
α : Type u_2
inst✝ : Zero α
a : ι
f : (j : ι) → j ∈ {a} → α
j : ι
h : ¬j = a
⊢ 0 = 0

Tactic:
<;>

Goal state after:
case pos
ι : Type u_1
α : Type u_2
inst✝ : Zero α
a : ι
f : (j : ι) → j ∈ {a} → α
j : ι
h : j = a
⊢ f j ⋯ = f a ⋯

case neg
ι : Type u_1
α : Type u_2
inst✝ : Zero α
a : ι
f : (j : ι) → j ∈ {a} → α
j : ι
h : ¬j = a
⊢ 0 = 0
Module: Mathlib.Algebra.Group.Finsupp

Goal state before:
pp: case inl
ι : Type u_1
M : Type u_3
inst✝¹ : AddZeroClass M
g₁ g₂ : ι →₀ M
inst✝ : DecidableEq ι
h : Disjoint g₁.support g₂.support
a : ι
ha : a ∈ g₁.support ∪ g₂.support
h✝ : a ∈ g₁.support ∧ a ∉ g₂.support
⊢ a ∈ (g₁ + g₂).support

pp: case inr
ι : Type u_1
M : Type u_3
inst✝¹ : AddZeroClass M
g₁ g₂ : ι →₀ M
inst✝ : DecidableEq ι
h : Disjoint g₁.support g₂.support
a : ι
ha : a ∈ g₁.support ∪ g₂.support
h✝ : a ∈ g₂.support ∧ a ∉ g₁.support
⊢ a ∈ (g₁ + g₂).support

Tactic:
<;>

Goal state after:
case inl
ι : Type u_1
M : Type u_3
inst✝¹ : AddZeroClass M
g₁ g₂ : ι →₀ M
inst✝ : DecidableEq ι
h : Disjoint g₁.support g₂.support
a : ι
ha : a ∈ g₁.support ∪ g₂.support
h✝ : a ∈ g₁.support ∧ a ∉ g₂.support
⊢ a ∈ (g₁ + g₂).support

case inr
ι : Type u_1
M : Type u_3
inst✝¹ : AddZeroClass M
g₁ g₂ : ι →₀ M
inst✝ : DecidableEq ι
h : Disjoint g₁.support g₂.support
a : ι
ha : a ∈ g₁.support ∪ g₂.support
h✝ : a ∈ g₂.support ∧ a ∉ g₁.support
⊢ a ∈ (g₁ + g₂).support
Module: Mathlib.Data.Finsupp.Single

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

pp: 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

Tactic:
<;>

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.Algebra.Group.Finsupp

Goal state before:
pp: case refine_1
ι : Type u_1
M : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : DecidableEq ι
f₁ f₂ : ι
g₁ g₂ : M
⊢ (single f₁ g₁).support ⊆ {f₁, f₂}

pp: case refine_2
ι : Type u_1
M : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : DecidableEq ι
f₁ f₂ : ι
g₁ g₂ : M
⊢ (single f₂ g₂).support ⊆ {f₁, f₂}

Tactic:
<;>

Goal state after:
case refine_1
ι : Type u_1
M : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : DecidableEq ι
f₁ f₂ : ι
g₁ g₂ : M
⊢ (single f₁ g₁).support ⊆ {f₁, f₂}

case refine_2
ι : Type u_1
M : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : DecidableEq ι
f₁ f₂ : ι
g₁ g₂ : M
⊢ (single f₂ g₂).support ⊆ {f₁, f₂}
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

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:
<;>

Goal state after:
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

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
Module: Mathlib.Algebra.Group.Finsupp

Goal state before:
pp: ι : Type u_1
G : Type u_6
inst✝¹ : AddGroup G
inst✝ : DecidableEq ι
f g : ι →₀ G
⊢ (f - g).support ⊆ f.support ∪ g.support

Tactic:
rw [sub_eq_add_neg, ← support_neg g]

Goal state after:
ι : Type u_1
G : Type u_6
inst✝¹ : AddGroup G
inst✝ : DecidableEq ι
f g : ι →₀ G
⊢ (f + -g).support ⊆ f.support ∪ (-g).support
Module: Mathlib.Data.Finsupp.Option

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
a✝ : α
⊢ (embDomain Embedding.some f) (Option.some a✝) = f a✝

Tactic:
exact embDomain_apply_self _ _ _

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

Goal state before:
pp: case none
α : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
inst✝ : Zero M
P : Option α →₀ M
⊢ ((fun P ↦ (embDomain Embedding.some P.2).update none P.1) ((fun P ↦ (P none, P.some)) P)) none = P none

pp: case some
α : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
inst✝ : Zero M
P : Option α →₀ M
a : α
⊢ ((fun P ↦ (embDomain Embedding.some P.2).update none P.1) ((fun P ↦ (P none, P.some)) P)) (Option.some a) =
    P (Option.some a)

Tactic:
<;>

Goal state after:
case none
α : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
inst✝ : Zero M
P : Option α →₀ M
⊢ ((fun P ↦ (embDomain Embedding.some P.2).update none P.1) ((fun P ↦ (P none, P.some)) P)) none = P none

case some
α : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
inst✝ : Zero M
P : Option α →₀ M
a : α
⊢ ((fun P ↦ (embDomain Embedding.some P.2).update none P.1) ((fun P ↦ (P none, P.some)) P)) (Option.some a) =
    P (Option.some a)
Module: Mathlib.Data.Finsupp.Option

Goal state before:
pp: case fst
α : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
inst✝ : Zero M
P : M × (α →₀ M)
⊢ ((fun P ↦ (P none, P.some)) ((fun P ↦ (embDomain Embedding.some P.2).update none P.1) P)).1 = P.1

pp: case snd
α : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
inst✝ : Zero M
P : M × (α →₀ M)
a✝ : α
⊢ ((fun P ↦ (P none, P.some)) ((fun P ↦ (embDomain Embedding.some P.2).update none P.1) P)).2 a✝ = P.2 a✝

Tactic:
<;>

Goal state after:
case fst
α : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
inst✝ : Zero M
P : M × (α →₀ M)
⊢ ((fun P ↦ (P none, P.some)) ((fun P ↦ (embDomain Embedding.some P.2).update none P.1) P)).1 = P.1

case snd
α : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
inst✝ : Zero M
P : M × (α →₀ M)
a✝ : α
⊢ ((fun P ↦ (P none, P.some)) ((fun P ↦ (embDomain Embedding.some P.2).update none P.1) P)).2 a✝ = P.2 a✝
Module: Mathlib.Data.Finsupp.Option

Goal state before:
pp: case mpr.inr
α : Type u_1
M : Type u_2
inst✝ : Zero M
y : M
f : α →₀ M
h : y ≠ 0
⊢ optionElim y f ≠ 0

Tactic:
exact optionElim_ne_zero_of_left y f h

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 t : Set ι
f g : ι → M₀
i : ι
h✝¹ : i ∈ s
h✝ : i ∈ t
⊢ f i * g i = f i * g i

pp: case neg
ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
s t : Set ι
f g : ι → M₀
i : ι
h✝¹ : i ∈ s
h✝ : ¬i ∈ t
⊢ 0 = f i * 0

pp: case pos
ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
s t : Set ι
f g : ι → M₀
i : ι
h✝¹ : ¬i ∈ s
h✝ : i ∈ t
⊢ 0 = 0 * g i

pp: case neg
ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
s t : Set ι
f g : ι → M₀
i : ι
h✝¹ : ¬i ∈ s
h✝ : ¬i ∈ t
⊢ 0 = 0 * 0

Tactic:
<;>

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

case neg
ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
s t : Set ι
f g : ι → M₀
i : ι
h✝¹ : i ∈ s
h✝ : ¬i ∈ t
⊢ 0 = f i * 0

case pos
ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
s t : Set ι
f g : ι → M₀
i : ι
h✝¹ : ¬i ∈ s
h✝ : i ∈ t
⊢ 0 = 0 * g i

case neg
ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
s t : Set ι
f g : ι → M₀
i : ι
h✝¹ : ¬i ∈ s
h✝ : ¬i ∈ t
⊢ 0 = 0 * 0
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: case cons
α : Type u_1
β : Type u_7
M : Type u_8
inst✝¹ : DecidableEq β
inst✝ : AddCommMonoid M
f : α → β →₀ M
a✝ : α
s✝ : Finset α
h✝ : a✝ ∉ s✝
ih : (s✝.sum f).support ⊆ s✝.sup fun x ↦ (f x).support
⊢ (f a✝ + ∑ x ∈ s✝, f x).support ⊆ (cons a✝ s✝ h✝).sup fun x ↦ (f x).support

Tactic:
Finset.sup_cons

Goal state after:
case cons
α : Type u_1
β : Type u_7
M : Type u_8
inst✝¹ : DecidableEq β
inst✝ : AddCommMonoid M
f : α → β →₀ M
a✝ : α
s✝ : Finset α
h✝ : a✝ ∉ s✝
ih : (s✝.sum f).support ⊆ s✝.sup fun x ↦ (f x).support
⊢ (f a✝ + ∑ x ∈ s✝, f x).support ⊆ (f a✝).support ⊔ s✝.sup fun x ↦ (f x).support
Module: Mathlib.Algebra.GroupWithZero.Indicator

Goal state before:
pp: case pos
ι : Type u_1
κ : Type u_2
M₀ : Type u_4
inst✝ : MulZeroOneClass M₀
s : Set ι
i : ι
t : Set κ
j : κ
h₀ : i ∈ s ∧ j ∈ t
h✝¹ : i ∈ s
h✝ : j ∈ t
⊢ 1 (i, j) = 1 i * 1 j

pp: case neg
ι : Type u_1
κ : Type u_2
M₀ : Type u_4
inst✝ : MulZeroOneClass M₀
s : Set ι
i : ι
t : Set κ
j : κ
h₀ : i ∈ s ∧ j ∈ t
h✝¹ : i ∈ s
h✝ : ¬j ∈ t
⊢ 1 (i, j) = 1 i * 0

pp: case pos
ι : Type u_1
κ : Type u_2
M₀ : Type u_4
inst✝ : MulZeroOneClass M₀
s : Set ι
i : ι
t : Set κ
j : κ
h₀ : i ∈ s ∧ j ∈ t
h✝¹ : ¬i ∈ s
h✝ : j ∈ t
⊢ 1 (i, j) = 0 * 1 j

pp: case neg
ι : Type u_1
κ : Type u_2
M₀ : Type u_4
inst✝ : MulZeroOneClass M₀
s : Set ι
i : ι
t : Set κ
j : κ
h₀ : i ∈ s ∧ j ∈ t
h✝¹ : ¬i ∈ s
h✝ : ¬j ∈ t
⊢ 1 (i, j) = 0 * 0

pp: case pos
ι : Type u_1
κ : Type u_2
M₀ : Type u_4
inst✝ : MulZeroOneClass M₀
s : Set ι
i : ι
t : Set κ
j : κ
h₀ : ¬(i ∈ s ∧ j ∈ t)
h✝¹ : i ∈ s
h✝ : j ∈ t
⊢ 0 = 1 i * 1 j

pp: case neg
ι : Type u_1
κ : Type u_2
M₀ : Type u_4
inst✝ : MulZeroOneClass M₀
s : Set ι
i : ι
t : Set κ
j : κ
h₀ : ¬(i ∈ s ∧ j ∈ t)
h✝¹ : i ∈ s
h✝ : ¬j ∈ t
⊢ 0 = 1 i * 0

pp: case pos
ι : Type u_1
κ : Type u_2
M₀ : Type u_4
inst✝ : MulZeroOneClass M₀
s : Set ι
i : ι
t : Set κ
j : κ
h₀ : ¬(i ∈ s ∧ j ∈ t)
h✝¹ : ¬i ∈ s
h✝ : j ∈ t
⊢ 0 = 0 * 1 j

pp: case neg
ι : Type u_1
κ : Type u_2
M₀ : Type u_4
inst✝ : MulZeroOneClass M₀
s : Set ι
i : ι
t : Set κ
j : κ
h₀ : ¬(i ∈ s ∧ j ∈ t)
h✝¹ : ¬i ∈ s
h✝ : ¬j ∈ t
⊢ 0 = 0 * 0

Tactic:
<;>

Goal state after:
case pos
ι : Type u_1
κ : Type u_2
M₀ : Type u_4
inst✝ : MulZeroOneClass M₀
s : Set ι
i : ι
t : Set κ
j : κ
h₀ : i ∈ s ∧ j ∈ t
h✝¹ : i ∈ s
h✝ : j ∈ t
⊢ 1 (i, j) = 1 i * 1 j

case neg
ι : Type u_1
κ : Type u_2
M₀ : Type u_4
inst✝ : MulZeroOneClass M₀
s : Set ι
i : ι
t : Set κ
j : κ
h₀ : i ∈ s ∧ j ∈ t
h✝¹ : i ∈ s
h✝ : ¬j ∈ t
⊢ 1 (i, j) = 1 i * 0

case pos
ι : Type u_1
κ : Type u_2
M₀ : Type u_4
inst✝ : MulZeroOneClass M₀
s : Set ι
i : ι
t : Set κ
j : κ
h₀ : i ∈ s ∧ j ∈ t
h✝¹ : ¬i ∈ s
h✝ : j ∈ t
⊢ 1 (i, j) = 0 * 1 j

case neg
ι : Type u_1
κ : Type u_2
M₀ : Type u_4
inst✝ : MulZeroOneClass M₀
s : Set ι
i : ι
t : Set κ
j : κ
h₀ : i ∈ s ∧ j ∈ t
h✝¹ : ¬i ∈ s
h✝ : ¬j ∈ t
⊢ 1 (i, j) = 0 * 0

case pos
ι : Type u_1
κ : Type u_2
M₀ : Type u_4
inst✝ : MulZeroOneClass M₀
s : Set ι
i : ι
t : Set κ
j : κ
h₀ : ¬(i ∈ s ∧ j ∈ t)
h✝¹ : i ∈ s
h✝ : j ∈ t
⊢ 0 = 1 i * 1 j

case neg
ι : Type u_1
κ : Type u_2
M₀ : Type u_4
inst✝ : MulZeroOneClass M₀
s : Set ι
i : ι
t : Set κ
j : κ
h₀ : ¬(i ∈ s ∧ j ∈ t)
h✝¹ : i ∈ s
h✝ : ¬j ∈ t
⊢ 0 = 1 i * 0

case pos
ι : Type u_1
κ : Type u_2
M₀ : Type u_4
inst✝ : MulZeroOneClass M₀
s : Set ι
i : ι
t : Set κ
j : κ
h₀ : ¬(i ∈ s ∧ j ∈ t)
h✝¹ : ¬i ∈ s
h✝ : j ∈ t
⊢ 0 = 0 * 1 j

case neg
ι : Type u_1
κ : Type u_2
M₀ : Type u_4
inst✝ : MulZeroOneClass M₀
s : Set ι
i : ι
t : Set κ
j : κ
h₀ : ¬(i ∈ s ∧ j ∈ t)
h✝¹ : ¬i ∈ s
h✝ : ¬j ∈ t
⊢ 0 = 0 * 0
Module: Mathlib.Algebra.GroupWithZero.Indicator

Goal state before:
pp: case neg
ι : Type u_1
κ : Type u_2
M₀ : Type u_4
inst✝ : MulZeroOneClass M₀
s : Set ι
i : ι
t : Set κ
j : κ
h₀ : i ∈ s ∧ j ∈ t
h✝¹ : i ∈ s
h✝ : ¬j ∈ t
⊢ 1 = 0

pp: case pos
ι : Type u_1
κ : Type u_2
M₀ : Type u_4
inst✝ : MulZeroOneClass M₀
s : Set ι
i : ι
t : Set κ
j : κ
h₀ : i ∈ s ∧ j ∈ t
h✝¹ : ¬i ∈ s
h✝ : j ∈ t
⊢ 1 = 0

pp: case neg
ι : Type u_1
κ : Type u_2
M₀ : Type u_4
inst✝ : MulZeroOneClass M₀
s : Set ι
i : ι
t : Set κ
j : κ
h₀ : i ∈ s ∧ j ∈ t
h✝¹ : ¬i ∈ s
h✝ : ¬j ∈ t
⊢ 1 = 0

pp: case pos
ι : Type u_1
κ : Type u_2
M₀ : Type u_4
inst✝ : MulZeroOneClass M₀
s : Set ι
i : ι
t : Set κ
j : κ
h₀ : ¬(i ∈ s ∧ j ∈ t)
h✝¹ : i ∈ s
h✝ : j ∈ t
⊢ 0 = 1

Tactic:
<;>

Goal state after:
case neg
ι : Type u_1
κ : Type u_2
M₀ : Type u_4
inst✝ : MulZeroOneClass M₀
s : Set ι
i : ι
t : Set κ
j : κ
h₀ : i ∈ s ∧ j ∈ t
h✝¹ : i ∈ s
h✝ : ¬j ∈ t
⊢ 1 = 0

case pos
ι : Type u_1
κ : Type u_2
M₀ : Type u_4
inst✝ : MulZeroOneClass M₀
s : Set ι
i : ι
t : Set κ
j : κ
h₀ : i ∈ s ∧ j ∈ t
h✝¹ : ¬i ∈ s
h✝ : j ∈ t
⊢ 1 = 0

case neg
ι : Type u_1
κ : Type u_2
M₀ : Type u_4
inst✝ : MulZeroOneClass M₀
s : Set ι
i : ι
t : Set κ
j : κ
h₀ : i ∈ s ∧ j ∈ t
h✝¹ : ¬i ∈ s
h✝ : ¬j ∈ t
⊢ 1 = 0

case pos
ι : Type u_1
κ : Type u_2
M₀ : Type u_4
inst✝ : MulZeroOneClass M₀
s : Set ι
i : ι
t : Set κ
j : κ
h₀ : ¬(i ∈ s ∧ j ∈ t)
h✝¹ : i ∈ s
h✝ : j ∈ t
⊢ 0 = 1
Module: Mathlib.Algebra.GroupWithZero.Indicator

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M₀ : Type u_4
inst✝ : MulZeroOneClass M₀
s : Set ι
i : ι
t : Set κ
j : κ
⊢ (s ×ˢ t).indicator 1 (i, j) = s.indicator 1 i * t.indicator 1 j

Tactic:
simp_rw [indicator, mem_prod_eq]
  split_ifs with h₀ <;> simp only [Pi.one_apply, mul_one, mul_zero] <;> tauto

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

Goal state before:
pp: case pos
M : Type u_3
M₂ : Type u_4
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
F : Type u_5
inst✝⁵ : FunLike F M M₂
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
n : ℕ
x : M
hR : ↑n = 0
⊢ f ((↑n)⁻¹ • x) = (↑n)⁻¹ • f x

pp: case neg
M : Type u_3
M₂ : Type u_4
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
F : Type u_5
inst✝⁵ : FunLike F M M₂
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
n : ℕ
x : M
hR : ¬↑n = 0
⊢ f ((↑n)⁻¹ • x) = (↑n)⁻¹ • f x

Tactic:
<;>

Goal state after:
case pos
M : Type u_3
M₂ : Type u_4
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
F : Type u_5
inst✝⁵ : FunLike F M M₂
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
n : ℕ
x : M
hR : ↑n = 0
⊢ f ((↑n)⁻¹ • x) = (↑n)⁻¹ • f x

case neg
M : Type u_3
M₂ : Type u_4
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
F : Type u_5
inst✝⁵ : FunLike F M M₂
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
n : ℕ
x : M
hR : ¬↑n = 0
⊢ f ((↑n)⁻¹ • x) = (↑n)⁻¹ • f x
Module: Mathlib.Data.Finsupp.Option

Goal state before:
pp: case single.none
α : Type u_1
M : Type u_2
N : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : CommMonoid N
b : Option α → M → N
h_zero : ∀ (o : Option α), b o 0 = 1
h_add : ∀ (o : Option α) (m₁ m₂ : M), b o (m₁ + m₂) = b o m₁ * b o m₂
m : M
⊢ (single none m).prod b = b none ((single none m) none) * (single none m).some.prod fun a ↦ b (Option.some a)

pp: case single.some
α : Type u_1
M : Type u_2
N : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : CommMonoid N
b : Option α → M → N
h_zero : ∀ (o : Option α), b o 0 = 1
h_add : ∀ (o : Option α) (m₁ m₂ : M), b o (m₁ + m₂) = b o m₁ * b o m₂
m : M
val✝ : α
⊢ (single (Option.some val✝) m).prod b =
    b none ((single (Option.some val✝) m) none) * (single (Option.some val✝) m).some.prod fun a ↦ b (Option.some a)

Tactic:
<;>

Goal state after:
case single.none
α : Type u_1
M : Type u_2
N : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : CommMonoid N
b : Option α → M → N
h_zero : ∀ (o : Option α), b o 0 = 1
h_add : ∀ (o : Option α) (m₁ m₂ : M), b o (m₁ + m₂) = b o m₁ * b o m₂
m : M
⊢ (single none m).prod b = b none ((single none m) none) * (single none m).some.prod fun a ↦ b (Option.some a)

case single.some
α : Type u_1
M : Type u_2
N : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : CommMonoid N
b : Option α → M → N
h_zero : ∀ (o : Option α), b o 0 = 1
h_add : ∀ (o : Option α) (m₁ m₂ : M), b o (m₁ + m₂) = b o m₁ * b o m₂
m : M
val✝ : α
⊢ (single (Option.some val✝) m).prod b =
    b none ((single (Option.some val✝) m) none) * (single (Option.some val✝) m).some.prod fun a ↦ b (Option.some a)
Module: Mathlib.Data.Finsupp.Option

Goal state before:
pp: case none
α : Type u_1
M : Type u_2
inst✝ : AddZeroClass M
a b : α →₀ M
i j : M
⊢ (optionElim (i + j) (a + b)) none = (optionElim i a + optionElim j b) none

pp: case some
α : Type u_1
M : Type u_2
inst✝ : AddZeroClass M
a b : α →₀ M
i j : M
val✝ : α
⊢ (optionElim (i + j) (a + b)) (Option.some val✝) = (optionElim i a + optionElim j b) (Option.some val✝)

Tactic:
<;>

Goal state after:
case none
α : Type u_1
M : Type u_2
inst✝ : AddZeroClass M
a b : α →₀ M
i j : M
⊢ (optionElim (i + j) (a + b)) none = (optionElim i a + optionElim j b) none

case some
α : Type u_1
M : Type u_2
inst✝ : AddZeroClass M
a b : α →₀ M
i j : M
val✝ : α
⊢ (optionElim (i + j) (a + b)) (Option.some val✝) = (optionElim i a + optionElim j b) (Option.some val✝)
Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: R : Type u_5
S : Type u_6
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : PartialOrder S
abv : AbsoluteValue R S
inst✝ : AddLeftMono S
l : List R
⊢ abv l.sum ≤ (List.map (⇑abv) l).sum

Tactic:
by
  induction l with
  | nil => simp
  | cons head tail ih => exact (abv.add_le ..).trans <| add_le_add_right ih (abv head)

Goal state after: