mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: case inl
R : Type u_3
S : Type u_4
inst✝⁴ : CommRing S
inst✝³ : PartialOrder S
inst✝² : IsOrderedRing S
inst✝¹ : Ring R
abv : AbsoluteValue R S
inst✝ : NoZeroDivisors S
w✝ : ℕ
⊢ abv ↑(↑w✝).natAbs = abv ↑↑w✝

pp: case inr
R : Type u_3
S : Type u_4
inst✝⁴ : CommRing S
inst✝³ : PartialOrder S
inst✝² : IsOrderedRing S
inst✝¹ : Ring R
abv : AbsoluteValue R S
inst✝ : NoZeroDivisors S
w✝ : ℕ
⊢ abv ↑(-↑w✝).natAbs = abv ↑(-↑w✝)

Tactic:
<;>

Goal state after:
case inl
R : Type u_3
S : Type u_4
inst✝⁴ : CommRing S
inst✝³ : PartialOrder S
inst✝² : IsOrderedRing S
inst✝¹ : Ring R
abv : AbsoluteValue R S
inst✝ : NoZeroDivisors S
w✝ : ℕ
⊢ abv ↑(↑w✝).natAbs = abv ↑↑w✝

case inr
R : Type u_3
S : Type u_4
inst✝⁴ : CommRing S
inst✝³ : PartialOrder S
inst✝² : IsOrderedRing S
inst✝¹ : Ring R
abv : AbsoluteValue R S
inst✝ : NoZeroDivisors S
w✝ : ℕ
⊢ abv ↑(-↑w✝).natAbs = abv ↑(-↑w✝)
Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: case inl
R : Type u_3
S : Type u_4
inst✝⁴ : CommRing S
inst✝³ : PartialOrder S
inst✝² : IsOrderedRing S
inst✝¹ : Ring R
inst✝ : NoZeroDivisors S
f g : AbsoluteValue R S
h : ∀ (n : ℕ), f ↑n = g ↑n
n : ℕ
⊢ f ↑↑n = g ↑↑n

pp: case inr
R : Type u_3
S : Type u_4
inst✝⁴ : CommRing S
inst✝³ : PartialOrder S
inst✝² : IsOrderedRing S
inst✝¹ : Ring R
inst✝ : NoZeroDivisors S
f g : AbsoluteValue R S
h : ∀ (n : ℕ), f ↑n = g ↑n
n : ℕ
⊢ f ↑(-↑n) = g ↑(-↑n)

Tactic:
<;>

Goal state after:
case inl
R : Type u_3
S : Type u_4
inst✝⁴ : CommRing S
inst✝³ : PartialOrder S
inst✝² : IsOrderedRing S
inst✝¹ : Ring R
inst✝ : NoZeroDivisors S
f g : AbsoluteValue R S
h : ∀ (n : ℕ), f ↑n = g ↑n
n : ℕ
⊢ f ↑↑n = g ↑↑n

case inr
R : Type u_3
S : Type u_4
inst✝⁴ : CommRing S
inst✝³ : PartialOrder S
inst✝² : IsOrderedRing S
inst✝¹ : Ring R
inst✝ : NoZeroDivisors S
f g : AbsoluteValue R S
h : ∀ (n : ℕ), f ↑n = g ↑n
n : ℕ
⊢ f ↑(-↑n) = g ↑(-↑n)
Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: case inl
ι : Type u_1
α : Type u_2
R✝ : Type u_3
S✝ : Type u_4
R : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : DecidablePred fun x ↦ x = 0
inst✝⁴ : NoZeroDivisors R
S : Type u_6
inst✝³ : Semiring S
inst✝² : PartialOrder S
inst✝¹ : IsOrderedRing S
inst✝ : Nontrivial S
x : R
hx : x = 0
⊢ 0 ≤ if x = 0 then 0 else 1

pp: case inr
ι : Type u_1
α : Type u_2
R✝ : Type u_3
S✝ : Type u_4
R : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : DecidablePred fun x ↦ x = 0
inst✝⁴ : NoZeroDivisors R
S : Type u_6
inst✝³ : Semiring S
inst✝² : PartialOrder S
inst✝¹ : IsOrderedRing S
inst✝ : Nontrivial S
x : R
hx : x ≠ 0
⊢ 0 ≤ if x = 0 then 0 else 1

Tactic:
<;>

Goal state after:
case inl
ι : Type u_1
α : Type u_2
R✝ : Type u_3
S✝ : Type u_4
R : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : DecidablePred fun x ↦ x = 0
inst✝⁴ : NoZeroDivisors R
S : Type u_6
inst✝³ : Semiring S
inst✝² : PartialOrder S
inst✝¹ : IsOrderedRing S
inst✝ : Nontrivial S
x : R
hx : x = 0
⊢ 0 ≤ if x = 0 then 0 else 1

case inr
ι : Type u_1
α : Type u_2
R✝ : Type u_3
S✝ : Type u_4
R : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : DecidablePred fun x ↦ x = 0
inst✝⁴ : NoZeroDivisors R
S : Type u_6
inst✝³ : Semiring S
inst✝² : PartialOrder S
inst✝¹ : IsOrderedRing S
inst✝ : Nontrivial S
x : R
hx : x ≠ 0
⊢ 0 ≤ if x = 0 then 0 else 1
Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: case inl
ι : Type u_1
α : Type u_2
R✝ : Type u_3
S✝ : Type u_4
R : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : DecidablePred fun x ↦ x = 0
inst✝⁴ : NoZeroDivisors R
S : Type u_6
inst✝³ : Semiring S
inst✝² : PartialOrder S
inst✝¹ : IsOrderedRing S
inst✝ : Nontrivial S
x : R
hx : x = 0
⊢ (if x = 0 then 0 else 1) = 0 ↔ x = 0

pp: case inr
ι : Type u_1
α : Type u_2
R✝ : Type u_3
S✝ : Type u_4
R : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : DecidablePred fun x ↦ x = 0
inst✝⁴ : NoZeroDivisors R
S : Type u_6
inst✝³ : Semiring S
inst✝² : PartialOrder S
inst✝¹ : IsOrderedRing S
inst✝ : Nontrivial S
x : R
hx : x ≠ 0
⊢ (if x = 0 then 0 else 1) = 0 ↔ x = 0

Tactic:
<;>

Goal state after:
case inl
ι : Type u_1
α : Type u_2
R✝ : Type u_3
S✝ : Type u_4
R : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : DecidablePred fun x ↦ x = 0
inst✝⁴ : NoZeroDivisors R
S : Type u_6
inst✝³ : Semiring S
inst✝² : PartialOrder S
inst✝¹ : IsOrderedRing S
inst✝ : Nontrivial S
x : R
hx : x = 0
⊢ (if x = 0 then 0 else 1) = 0 ↔ x = 0

case inr
ι : Type u_1
α : Type u_2
R✝ : Type u_3
S✝ : Type u_4
R : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : DecidablePred fun x ↦ x = 0
inst✝⁴ : NoZeroDivisors R
S : Type u_6
inst✝³ : Semiring S
inst✝² : PartialOrder S
inst✝¹ : IsOrderedRing S
inst✝ : Nontrivial S
x : R
hx : x ≠ 0
⊢ (if x = 0 then 0 else 1) = 0 ↔ x = 0
Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: case inr.inr.inl
ι : Type u_1
α : Type u_2
R✝ : Type u_3
S✝ : Type u_4
R : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : DecidablePred fun x ↦ x = 0
inst✝⁴ : NoZeroDivisors R
S : Type u_6
inst✝³ : Semiring S
inst✝² : PartialOrder S
inst✝¹ : IsOrderedRing S
inst✝ : Nontrivial S
x y : R
hx : x ≠ 0
hy : y ≠ 0
hxy : x + y = 0
⊢ (if x + y = 0 then 0 else 1) ≤ 2

pp: case inr.inr.inr
ι : Type u_1
α : Type u_2
R✝ : Type u_3
S✝ : Type u_4
R : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : DecidablePred fun x ↦ x = 0
inst✝⁴ : NoZeroDivisors R
S : Type u_6
inst✝³ : Semiring S
inst✝² : PartialOrder S
inst✝¹ : IsOrderedRing S
inst✝ : Nontrivial S
x y : R
hx : x ≠ 0
hy : y ≠ 0
hxy : x + y ≠ 0
⊢ (if x + y = 0 then 0 else 1) ≤ 2

Tactic:
<;>

Goal state after:
case inr.inr.inl
ι : Type u_1
α : Type u_2
R✝ : Type u_3
S✝ : Type u_4
R : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : DecidablePred fun x ↦ x = 0
inst✝⁴ : NoZeroDivisors R
S : Type u_6
inst✝³ : Semiring S
inst✝² : PartialOrder S
inst✝¹ : IsOrderedRing S
inst✝ : Nontrivial S
x y : R
hx : x ≠ 0
hy : y ≠ 0
hxy : x + y = 0
⊢ (if x + y = 0 then 0 else 1) ≤ 2

case inr.inr.inr
ι : Type u_1
α : Type u_2
R✝ : Type u_3
S✝ : Type u_4
R : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : DecidablePred fun x ↦ x = 0
inst✝⁴ : NoZeroDivisors R
S : Type u_6
inst✝³ : Semiring S
inst✝² : PartialOrder S
inst✝¹ : IsOrderedRing S
inst✝ : Nontrivial S
x y : R
hx : x ≠ 0
hy : y ≠ 0
hxy : x + y ≠ 0
⊢ (if x + y = 0 then 0 else 1) ≤ 2
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_8
inst✝ : AddCommMonoid M
s : Finset α
f : (a : α) → a ∈ s → M
⊢ ∀ x ∈ s, x ∉ (indicator s f).support → single x ((indicator s f) x) = 0

Tactic:
intro i _ hi
    rw [notMem_support_iff.mp hi, single_zero]

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.List

Goal state before:
pp: R : Type u_1
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
ι : Type u_2
f g : ι → R
a : ι
s : List ι
hind : (∀ (i : ι), i ∈ s → 0 ≤ f i) → (∀ (i : ι), i ∈ s → f i ≤ g i) → (map f s).prod ≤ (map g s).prod
h0 : ∀ (i : ι), i ∈ a :: s → 0 ≤ f i
h : ∀ (i : ι), i ∈ a :: s → f i ≤ g i
this : MulPosMono R
⊢ a ∈ a :: s

pp: R : Type u_1
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
ι : Type u_2
f g : ι → R
a : ι
s : List ι
hind : (∀ (i : ι), i ∈ s → 0 ≤ f i) → (∀ (i : ι), i ∈ s → f i ≤ g i) → (map f s).prod ≤ (map g s).prod
h0 : ∀ (i : ι), i ∈ a :: s → 0 ≤ f i
h : ∀ (i : ι), i ∈ a :: s → f i ≤ g i
this : MulPosMono R
⊢ a ∈ a :: s

Tactic:
<;>

Goal state after:
R : Type u_1
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
ι : Type u_2
f g : ι → R
a : ι
s : List ι
hind : (∀ (i : ι), i ∈ s → 0 ≤ f i) → (∀ (i : ι), i ∈ s → f i ≤ g i) → (map f s).prod ≤ (map g s).prod
h0 : ∀ (i : ι), i ∈ a :: s → 0 ≤ f i
h : ∀ (i : ι), i ∈ a :: s → f i ≤ g i
this : MulPosMono R
⊢ a ∈ a :: s

R : Type u_1
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
ι : Type u_2
f g : ι → R
a : ι
s : List ι
hind : (∀ (i : ι), i ∈ s → 0 ≤ f i) → (∀ (i : ι), i ∈ s → f i ≤ g i) → (map f s).prod ≤ (map g s).prod
h0 : ∀ (i : ι), i ∈ a :: s → 0 ≤ f i
h : ∀ (i : ι), i ∈ a :: s → f i ≤ g i
this : MulPosMono R
⊢ a ∈ a :: s
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
inst✝ : Zero M
f✝ : α ≃ β
f : α →₀ M
⊢ equivMapDomain f✝.symm (equivMapDomain f✝ f) = f

pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
inst✝ : Zero M
f✝ : α ≃ β
f : β →₀ M
⊢ equivMapDomain f✝ (equivMapDomain f✝.symm f) = f

Tactic:
<;>

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
inst✝ : Zero M
f✝ : α ≃ β
f : α →₀ M
⊢ equivMapDomain f✝.symm (equivMapDomain f✝ f) = f

case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
inst✝ : Zero M
f✝ : α ≃ β
f : β →₀ M
⊢ equivMapDomain f✝ (equivMapDomain f✝.symm f) = f
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
inst✝ : Zero M
f✝ : α ≃ β
f : α →₀ M
x : α
⊢ (equivMapDomain f✝.symm (equivMapDomain f✝ f)) x = f x

pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
inst✝ : Zero M
f✝ : α ≃ β
f : β →₀ M
x : β
⊢ (equivMapDomain f✝ (equivMapDomain f✝.symm f)) x = f x

Tactic:
<;>

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
inst✝ : Zero M
f✝ : α ≃ β
f : α →₀ M
x : α
⊢ (equivMapDomain f✝.symm (equivMapDomain f✝ f)) x = f x

case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
inst✝ : Zero M
f✝ : α ≃ β
f : β →₀ M
x : β
⊢ (equivMapDomain f✝ (equivMapDomain f✝.symm f)) x = f x
Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.List

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommMonoidWithZero R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : PosMulStrictMono R
inst✝ : NeZero 1
ι : Type u_2
s✝ : List ι
f g : ι → R
a : ι
s : List ι
hs : a :: s ≠ []
h0 : ∀ (i : ι), i ∈ a :: s → 0 < f i
h : ∀ (i : ι), i ∈ a :: s → f i < g i
this : MulPosStrictMono R
⊢ a ∈ a :: s

pp: R : Type u_1
inst✝⁴ : CommMonoidWithZero R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : PosMulStrictMono R
inst✝ : NeZero 1
ι : Type u_2
s✝ : List ι
f g : ι → R
a : ι
s : List ι
hs : a :: s ≠ []
h0 : ∀ (i : ι), i ∈ a :: s → 0 < f i
h : ∀ (i : ι), i ∈ a :: s → f i < g i
this : MulPosStrictMono R
⊢ a ∈ a :: s

Tactic:
<;>

Goal state after:
R : Type u_1
inst✝⁴ : CommMonoidWithZero R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : PosMulStrictMono R
inst✝ : NeZero 1
ι : Type u_2
s✝ : List ι
f g : ι → R
a : ι
s : List ι
hs : a :: s ≠ []
h0 : ∀ (i : ι), i ∈ a :: s → 0 < f i
h : ∀ (i : ι), i ∈ a :: s → f i < g i
this : MulPosStrictMono R
⊢ a ∈ a :: s

R : Type u_1
inst✝⁴ : CommMonoidWithZero R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : PosMulStrictMono R
inst✝ : NeZero 1
ι : Type u_2
s✝ : List ι
f g : ι → R
a : ι
s : List ι
hs : a :: s ≠ []
h0 : ∀ (i : ι), i ∈ a :: s → 0 < f i
h : ∀ (i : ι), i ∈ a :: s → f i < g i
this : MulPosStrictMono R
⊢ a ∈ a :: s
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α ↪ β
x : α →₀ M
⊢ (mapDomain (⇑f) x).support = map f x.support

Tactic:
by
  ext b
  simp only [mem_support_iff, ne_eq, mem_map]
  refine ⟨fun h ↦ ?_, ?_⟩
  · obtain ⟨a, rfl⟩ := mem_range_of_mapDomain_ne_zero h
    exact ⟨a, by simpa [f.injective] using h⟩
  · rintro ⟨a, ha, rfl⟩
    simpa [f.injective]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq β
f : α → β
s : α →₀ M
hf : Set.InjOn f ↑s.support
hx_w : α
hx_h_left : ¬s hx_w = 0
⊢ s hx_w ≠ 0

Tactic:
Ne

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq β
f : α → β
s : α →₀ M
hf : Set.InjOn f ↑s.support
hx_w : α
hx_h_left : ¬s hx_w = 0
⊢ ¬s hx_w = 0
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: case neg.h
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α ↪ β
v : α →₀ M
a : β
h : a ∉ Set.range ⇑f
⊢ a ∉ Set.range ⇑f

pp: case neg.h
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α ↪ β
v : α →₀ M
a : β
h : a ∉ Set.range ⇑f
⊢ a ∉ Set.range ⇑f

Tactic:
<;>

Goal state after:
case neg.h
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α ↪ β
v : α →₀ M
a : β
h : a ∉ Set.range ⇑f
⊢ a ∉ Set.range ⇑f

case neg.h
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α ↪ β
v : α →₀ M
a : β
h : a ∉ Set.range ⇑f
⊢ a ∉ Set.range ⇑f
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : v₁ ∈ {w | ↑w.support ⊆ S}
v₂ : α →₀ M
hv₂ : v₂ ∈ {w | ↑w.support ⊆ S}
eq : mapDomain f v₁ = mapDomain f v₂
a : α
h : a ∈ v₁.support ∪ v₂.support
⊢ a ∈ S

pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : v₁ ∈ {w | ↑w.support ⊆ S}
v₂ : α →₀ M
hv₂ : v₂ ∈ {w | ↑w.support ⊆ S}
eq : mapDomain f v₁ = mapDomain f v₂
a : α
h : a ∈ v₁.support ∪ v₂.support
⊢ a ∈ S

Tactic:
<;>

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : v₁ ∈ {w | ↑w.support ⊆ S}
v₂ : α →₀ M
hv₂ : v₂ ∈ {w | ↑w.support ⊆ S}
eq : mapDomain f v₁ = mapDomain f v₂
a : α
h : a ∈ v₁.support ∪ v₂.support
⊢ a ∈ S

α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : v₁ ∈ {w | ↑w.support ⊆ S}
v₂ : α →₀ M
hv₂ : v₂ ∈ {w | ↑w.support ⊆ S}
eq : mapDomain f v₁ = mapDomain f v₂
a : α
h : a ∈ v₁.support ∪ v₂.support
⊢ a ∈ S
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
inst✝² : Zero M
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
f✝ : α →₀ M
p : α → Prop
inst✝ : DecidablePred p
f : α →₀ M
a : α
h : p a
⊢ a ∈ Finset.filter p f.support ↔ f a ≠ 0

pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
inst✝² : Zero M
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
f✝ : α →₀ M
p : α → Prop
inst✝ : DecidablePred p
f : α →₀ M
a : α
h : ¬p a
⊢ a ∈ Finset.filter p f.support ↔ 0 ≠ 0

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
inst✝² : Zero M
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
f✝ : α →₀ M
p : α → Prop
inst✝ : DecidablePred p
f : α →₀ M
a : α
h : p a
⊢ a ∈ Finset.filter p f.support ↔ f a ≠ 0

case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
inst✝² : Zero M
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
f✝ : α →₀ M
p : α → Prop
inst✝ : DecidablePred p
f : α →₀ M
a : α
h : ¬p a
⊢ a ∈ Finset.filter p f.support ↔ 0 ≠ 0
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: case isTrue
α : Type u_1
M : Type u_5
inst✝¹ : AddCommMonoid M
f : α →₀ M
p : α → Prop
inst✝ : DecidablePred p
a✝ : α
h✝ : p a✝
⊢ f a✝ + 0 = f a✝

pp: case isFalse
α : Type u_1
M : Type u_5
inst✝¹ : AddCommMonoid M
f : α →₀ M
p : α → Prop
inst✝ : DecidablePred p
a✝ : α
h✝ : ¬p a✝
⊢ 0 + f a✝ = f a✝

Tactic:
<;>

Goal state after:
case isTrue
α : Type u_1
M : Type u_5
inst✝¹ : AddCommMonoid M
f : α →₀ M
p : α → Prop
inst✝ : DecidablePred p
a✝ : α
h✝ : p a✝
⊢ f a✝ + 0 = f a✝

case isFalse
α : Type u_1
M : Type u_5
inst✝¹ : AddCommMonoid M
f : α →₀ M
p : α → Prop
inst✝ : DecidablePred p
a✝ : α
h✝ : ¬p a✝
⊢ 0 + f a✝ = f a✝
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
p : α → Prop
D : DecidablePred p
f : α →₀ M
⊢ (subtypeDomain p f).support = Finset.subtype p f.support

pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
p : α → Prop
D : DecidablePred p
f : α →₀ M
⊢ DecidablePred p

Tactic:
<;>

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : Zero M
p : α → Prop
D : DecidablePred p
f : α →₀ M
⊢ (subtypeDomain p f).support = Finset.subtype p f.support

α : Type u_1
M : Type u_5
inst✝ : Zero M
p : α → Prop
D : DecidablePred p
f : α →₀ M
⊢ DecidablePred p
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: case refine_1
α : Type u_1
M : Type u_5
N : Type u_6
inst✝¹ : Zero M
p : α → Prop
inst✝ : CommMonoid N
v : α →₀ M
h : α → M → N
hp : ∀ x ∈ v.support, p x
⊢ ∀ a ∈ (subtypeDomain p v).support, ↑a ∈ v.support

pp: case refine_2
α : Type u_1
M : Type u_5
N : Type u_6
inst✝¹ : Zero M
p : α → Prop
inst✝ : CommMonoid N
v : α →₀ M
h : α → M → N
hp : ∀ x ∈ v.support, p x
⊢ ∀ a₁ ∈ (subtypeDomain p v).support, ∀ a₂ ∈ (subtypeDomain p v).support, ↑a₁ = ↑a₂ → a₁ = a₂

pp: case refine_3
α : Type u_1
M : Type u_5
N : Type u_6
inst✝¹ : Zero M
p : α → Prop
inst✝ : CommMonoid N
v : α →₀ M
h : α → M → N
hp : ∀ x ∈ v.support, p x
⊢ ∀ b ∈ v.support, ∃ a, ∃ (_ : a ∈ (subtypeDomain p v).support), ↑a = b

pp: case refine_4
α : Type u_1
M : Type u_5
N : Type u_6
inst✝¹ : Zero M
p : α → Prop
inst✝ : CommMonoid N
v : α →₀ M
h : α → M → N
hp : ∀ x ∈ v.support, p x
⊢ ∀ a ∈ (subtypeDomain p v).support, (fun a b ↦ h (↑a) b) a ((subtypeDomain p v) a) = h (↑a) (v ↑a)

Tactic:
<;>

Goal state after:
case refine_1
α : Type u_1
M : Type u_5
N : Type u_6
inst✝¹ : Zero M
p : α → Prop
inst✝ : CommMonoid N
v : α →₀ M
h : α → M → N
hp : ∀ x ∈ v.support, p x
⊢ ∀ a ∈ (subtypeDomain p v).support, ↑a ∈ v.support

case refine_2
α : Type u_1
M : Type u_5
N : Type u_6
inst✝¹ : Zero M
p : α → Prop
inst✝ : CommMonoid N
v : α →₀ M
h : α → M → N
hp : ∀ x ∈ v.support, p x
⊢ ∀ a₁ ∈ (subtypeDomain p v).support, ∀ a₂ ∈ (subtypeDomain p v).support, ↑a₁ = ↑a₂ → a₁ = a₂

case refine_3
α : Type u_1
M : Type u_5
N : Type u_6
inst✝¹ : Zero M
p : α → Prop
inst✝ : CommMonoid N
v : α →₀ M
h : α → M → N
hp : ∀ x ∈ v.support, p x
⊢ ∀ b ∈ v.support, ∃ a, ∃ (_ : a ∈ (subtypeDomain p v).support), ↑a = b

case refine_4
α : Type u_1
M : Type u_5
N : Type u_6
inst✝¹ : Zero M
p : α → Prop
inst✝ : CommMonoid N
v : α →₀ M
h : α → M → N
hp : ∀ x ∈ v.support, p x
⊢ ∀ a ∈ (subtypeDomain p v).support, (fun a b ↦ h (↑a) b) a ((subtypeDomain p v) a) = h (↑a) (v ↑a)
Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset

Goal state before:
pp: case h1
ι : Type u_1
R : Type u_2
inst✝² : CommSemiring R
inst✝¹ : PartialOrder R
inst✝ : CanonicallyOrderedAdd R
f g h : ι → R
s : Finset ι
i : ι
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ j ∈ s, j ≠ i → g j ≤ f j
hhf : ∀ j ∈ s, j ≠ i → h j ≤ f j
j : ι
hj : j ∈ s \ {i}
⊢ g j ≤ f j

pp: case h1
ι : Type u_1
R : Type u_2
inst✝² : CommSemiring R
inst✝¹ : PartialOrder R
inst✝ : CanonicallyOrderedAdd R
f g h : ι → R
s : Finset ι
i : ι
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ j ∈ s, j ≠ i → g j ≤ f j
hhf : ∀ j ∈ s, j ≠ i → h j ≤ f j
j : ι
hj : j ∈ s \ {i}
⊢ h j ≤ f j

Tactic:
<;>

Goal state after:
case h1
ι : Type u_1
R : Type u_2
inst✝² : CommSemiring R
inst✝¹ : PartialOrder R
inst✝ : CanonicallyOrderedAdd R
f g h : ι → R
s : Finset ι
i : ι
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ j ∈ s, j ≠ i → g j ≤ f j
hhf : ∀ j ∈ s, j ≠ i → h j ≤ f j
j : ι
hj : j ∈ s \ {i}
⊢ g j ≤ f j

case h1
ι : Type u_1
R : Type u_2
inst✝² : CommSemiring R
inst✝¹ : PartialOrder R
inst✝ : CanonicallyOrderedAdd R
f g h : ι → R
s : Finset ι
i : ι
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ j ∈ s, j ≠ i → g j ≤ f j
hhf : ∀ j ∈ s, j ≠ i → h j ≤ f j
j : ι
hj : j ∈ s \ {i}
⊢ h j ≤ f j
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: case empty
ι : Type u_1
α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : LE α
inst✝ : MulLeftMono α
s : Finset ι
f : ι → α
⊢ MulLECancellable (∏ i ∈ ∅, f i) ↔ ∀ ⦃i : ι⦄, i ∈ ∅ → MulLECancellable (f i)

pp: case cons
ι : Type u_1
α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : LE α
inst✝ : MulLeftMono α
s : Finset ι
f : ι → α
a✝¹ : ι
s✝ : Finset ι
h✝ : a✝¹ ∉ s✝
a✝ : MulLECancellable (∏ i ∈ s✝, f i) ↔ ∀ ⦃i : ι⦄, i ∈ s✝ → MulLECancellable (f i)
⊢ MulLECancellable (∏ i ∈ cons a✝¹ s✝ h✝, f i) ↔ ∀ ⦃i : ι⦄, i ∈ cons a✝¹ s✝ h✝ → MulLECancellable (f i)

Tactic:
<;>

Goal state after:
case empty
ι : Type u_1
α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : LE α
inst✝ : MulLeftMono α
s : Finset ι
f : ι → α
⊢ MulLECancellable (∏ i ∈ ∅, f i) ↔ ∀ ⦃i : ι⦄, i ∈ ∅ → MulLECancellable (f i)

case cons
ι : Type u_1
α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : LE α
inst✝ : MulLeftMono α
s : Finset ι
f : ι → α
a✝¹ : ι
s✝ : Finset ι
h✝ : a✝¹ ∉ s✝
a✝ : MulLECancellable (∏ i ∈ s✝, f i) ↔ ∀ ⦃i : ι⦄, i ∈ s✝ → MulLECancellable (f i)
⊢ MulLECancellable (∏ i ∈ cons a✝¹ s✝ h✝, f i) ↔ ∀ ⦃i : ι⦄, i ∈ cons a✝¹ s✝ h✝ → MulLECancellable (f i)
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
a : α
b : β
m : M
y : β
⊢ (single a (single b m)).uncurry (a, y) = (single (a, b) m) (a, y)

pp: case inr
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
a : α
b : β
m : M
x : α
y : β
hne : a ≠ x
⊢ (single a (single b m)).uncurry (x, y) = (single (a, b) m) (x, y)

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
a : α
b : β
m : M
y : β
⊢ (single a (single b m)).uncurry (a, y) = (single (a, b) m) (a, y)

case inr
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
a : α
b : β
m : M
x : α
y : β
hne : a ≠ x
⊢ (single a (single b m)).uncurry (x, y) = (single (a, b) m) (x, y)
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Zero γ
val✝ : α
⊢ (sumElim 0 0) (Sum.inl val✝) = 0 (Sum.inl val✝)

pp: case inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Zero γ
val✝ : β
⊢ (sumElim 0 0) (Sum.inr val✝) = 0 (Sum.inr val✝)

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Zero γ
val✝ : α
⊢ (sumElim 0 0) (Sum.inl val✝) = 0 (Sum.inl val✝)

case inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Zero γ
val✝ : β
⊢ (sumElim 0 0) (Sum.inr val✝) = 0 (Sum.inr val✝)
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Zero γ
a : α
c : γ
val✝ : α
⊢ ((single a c).sumElim 0) (Sum.inl val✝) = (single (Sum.inl a) c) (Sum.inl val✝)

pp: case inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Zero γ
a : α
c : γ
val✝ : β
⊢ ((single a c).sumElim 0) (Sum.inr val✝) = (single (Sum.inl a) c) (Sum.inr val✝)

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Zero γ
a : α
c : γ
val✝ : α
⊢ ((single a c).sumElim 0) (Sum.inl val✝) = (single (Sum.inl a) c) (Sum.inl val✝)

case inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Zero γ
a : α
c : γ
val✝ : β
⊢ ((single a c).sumElim 0) (Sum.inr val✝) = (single (Sum.inl a) c) (Sum.inr val✝)
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Zero γ
b : β
c : γ
val✝ : α
⊢ (sumElim 0 (single b c)) (Sum.inl val✝) = (single (Sum.inr b) c) (Sum.inl val✝)

pp: case inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Zero γ
b : β
c : γ
val✝ : β
⊢ (sumElim 0 (single b c)) (Sum.inr val✝) = (single (Sum.inr b) c) (Sum.inr val✝)

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Zero γ
b : β
c : γ
val✝ : α
⊢ (sumElim 0 (single b c)) (Sum.inl val✝) = (single (Sum.inr b) c) (Sum.inl val✝)

case inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Zero γ
b : β
c : γ
val✝ : β
⊢ (sumElim 0 (single b c)) (Sum.inr val✝) = (single (Sum.inr b) c) (Sum.inr val✝)