mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddMonoid M
a : α
b : β
m₁ m₂ : M
val✝ : α
⊢ ((single a m₁).sumElim (single b m₂)) (Sum.inl val✝) = (single (Sum.inl a) m₁ + single (Sum.inr b) m₂) (Sum.inl val✝)

pp: case inr
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddMonoid M
a : α
b : β
m₁ m₂ : M
val✝ : β
⊢ ((single a m₁).sumElim (single b m₂)) (Sum.inr val✝) = (single (Sum.inl a) m₁ + single (Sum.inr b) m₂) (Sum.inr val✝)

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddMonoid M
a : α
b : β
m₁ m₂ : M
val✝ : α
⊢ ((single a m₁).sumElim (single b m₂)) (Sum.inl val✝) = (single (Sum.inl a) m₁ + single (Sum.inr b) m₂) (Sum.inl val✝)

case inr
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddMonoid M
a : α
b : β
m₁ m₂ : M
val✝ : β
⊢ ((single a m₁).sumElim (single b m₂)) (Sum.inr val✝) = (single (Sum.inl a) m₁ + single (Sum.inr b) m₂) (Sum.inr val✝)
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α →₀ M
g : β →₀ M
val✝ : α
⊢ (f.sumElim g) (Sum.inl val✝) = (mapDomain Sum.inl f + mapDomain Sum.inr g) (Sum.inl val✝)

pp: case inr
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α →₀ M
g : β →₀ M
val✝ : β
⊢ (f.sumElim g) (Sum.inr val✝) = (mapDomain Sum.inl f + mapDomain Sum.inr g) (Sum.inr val✝)

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α →₀ M
g : β →₀ M
val✝ : α
⊢ (f.sumElim g) (Sum.inl val✝) = (mapDomain Sum.inl f + mapDomain Sum.inr g) (Sum.inl val✝)

case inr
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α →₀ M
g : β →₀ M
val✝ : β
⊢ (f.sumElim g) (Sum.inr val✝) = (mapDomain Sum.inl f + mapDomain Sum.inr g) (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 : α →₀ γ
val✝ : α
⊢ (embDomain Embedding.inl a) (Sum.inl val✝) = (a.sumElim 0) (Sum.inl val✝)

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

Tactic:
<;>

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

case inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Zero γ
a : α →₀ γ
val✝ : β
⊢ (embDomain Embedding.inl a) (Sum.inr val✝) = (a.sumElim 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 γ
b : β →₀ γ
val✝ : α
⊢ (embDomain Embedding.inr b) (Sum.inl val✝) = (sumElim 0 b) (Sum.inl val✝)

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

Tactic:
<;>

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

case inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Zero γ
b : β →₀ γ
val✝ : β
⊢ (embDomain Embedding.inr b) (Sum.inr val✝) = (sumElim 0 b) (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 γ
c : α ⊕ β →₀ γ
val✝ : α
⊢ ((comapDomain Sum.inl c ⋯).sumElim (comapDomain Sum.inr c ⋯)) (Sum.inl val✝) = c (Sum.inl val✝)

pp: case inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Zero γ
c : α ⊕ β →₀ γ
val✝ : β
⊢ ((comapDomain Sum.inl c ⋯).sumElim (comapDomain Sum.inr c ⋯)) (Sum.inr val✝) = c (Sum.inr val✝)

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Zero γ
c : α ⊕ β →₀ γ
val✝ : α
⊢ ((comapDomain Sum.inl c ⋯).sumElim (comapDomain Sum.inr c ⋯)) (Sum.inl val✝) = c (Sum.inl val✝)

case inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Zero γ
c : α ⊕ β →₀ γ
val✝ : β
⊢ ((comapDomain Sum.inl c ⋯).sumElim (comapDomain Sum.inr c ⋯)) (Sum.inr val✝) = c (Sum.inr val✝)
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddZeroClass M
a b : α →₀ M
c d : β →₀ M
val✝ : α
⊢ ((a + b).sumElim (c + d)) (Sum.inl val✝) = (a.sumElim c + b.sumElim d) (Sum.inl val✝)

pp: case inr
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddZeroClass M
a b : α →₀ M
c d : β →₀ M
val✝ : β
⊢ ((a + b).sumElim (c + d)) (Sum.inr val✝) = (a.sumElim c + b.sumElim d) (Sum.inr val✝)

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddZeroClass M
a b : α →₀ M
c d : β →₀ M
val✝ : α
⊢ ((a + b).sumElim (c + d)) (Sum.inl val✝) = (a.sumElim c + b.sumElim d) (Sum.inl val✝)

case inr
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddZeroClass M
a b : α →₀ M
c d : β →₀ M
val✝ : β
⊢ ((a + b).sumElim (c + d)) (Sum.inr val✝) = (a.sumElim c + b.sumElim d) (Sum.inr val✝)
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: case inl
α✝ : 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 γ✝
α : Type u_12
β : Type u_13
γ : Type u_14
inst✝ : Zero γ
f : α ⊕ β →₀ γ
a : α
⊢ ((fun fg ↦ fg.1.sumElim fg.2) ((fun f ↦ (comapDomain Sum.inl f ⋯, comapDomain Sum.inr f ⋯)) f)) (Sum.inl a) =
    f (Sum.inl a)

pp: case inr
α✝ : 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 γ✝
α : Type u_12
β : Type u_13
γ : Type u_14
inst✝ : Zero γ
f : α ⊕ β →₀ γ
b : β
⊢ ((fun fg ↦ fg.1.sumElim fg.2) ((fun f ↦ (comapDomain Sum.inl f ⋯, comapDomain Sum.inr f ⋯)) f)) (Sum.inr b) =
    f (Sum.inr b)

Tactic:
<;>

Goal state after:
case inl
α✝ : 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 γ✝
α : Type u_12
β : Type u_13
γ : Type u_14
inst✝ : Zero γ
f : α ⊕ β →₀ γ
a : α
⊢ ((fun fg ↦ fg.1.sumElim fg.2) ((fun f ↦ (comapDomain Sum.inl f ⋯, comapDomain Sum.inr f ⋯)) f)) (Sum.inl a) =
    f (Sum.inl a)

case inr
α✝ : 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 γ✝
α : Type u_12
β : Type u_13
γ : Type u_14
inst✝ : Zero γ
f : α ⊕ β →₀ γ
b : β
⊢ ((fun fg ↦ fg.1.sumElim fg.2) ((fun f ↦ (comapDomain Sum.inl f ⋯, comapDomain Sum.inr f ⋯)) f)) (Sum.inr b) =
    f (Sum.inr b)
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: case fst
α✝ : 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 γ✝
α : Type u_12
β : Type u_13
γ : Type u_14
inst✝ : Zero γ
fg : (α →₀ γ) × (β →₀ γ)
a✝ : α
⊢ ((fun f ↦ (comapDomain Sum.inl f ⋯, comapDomain Sum.inr f ⋯)) ((fun fg ↦ fg.1.sumElim fg.2) fg)).1 a✝ = fg.1 a✝

pp: case snd
α✝ : 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 γ✝
α : Type u_12
β : Type u_13
γ : Type u_14
inst✝ : Zero γ
fg : (α →₀ γ) × (β →₀ γ)
a✝ : β
⊢ ((fun f ↦ (comapDomain Sum.inl f ⋯, comapDomain Sum.inr f ⋯)) ((fun fg ↦ fg.1.sumElim fg.2) fg)).2 a✝ = fg.2 a✝

Tactic:
<;>

Goal state after:
case fst
α✝ : 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 γ✝
α : Type u_12
β : Type u_13
γ : Type u_14
inst✝ : Zero γ
fg : (α →₀ γ) × (β →₀ γ)
a✝ : α
⊢ ((fun f ↦ (comapDomain Sum.inl f ⋯, comapDomain Sum.inr f ⋯)) ((fun fg ↦ fg.1.sumElim fg.2) fg)).1 a✝ = fg.1 a✝

case snd
α✝ : 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 γ✝
α : Type u_12
β : Type u_13
γ : Type u_14
inst✝ : Zero γ
fg : (α →₀ γ) × (β →₀ γ)
a✝ : β
⊢ ((fun f ↦ (comapDomain Sum.inl f ⋯, comapDomain Sum.inr f ⋯)) ((fun fg ↦ fg.1.sumElim fg.2) fg)).2 a✝ = fg.2 a✝
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: case fst
α✝ : 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 γ
inst✝ : AddMonoid M
α : Type u_12
β : Type u_13
x✝ y✝ : α ⊕ β →₀ M
a✝ : α
⊢ (sumFinsuppEquivProdFinsupp.toFun (x✝ + y✝)).1 a✝ =
    (sumFinsuppEquivProdFinsupp.toFun x✝ + sumFinsuppEquivProdFinsupp.toFun y✝).1 a✝

pp: case snd
α✝ : 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 γ
inst✝ : AddMonoid M
α : Type u_12
β : Type u_13
x✝ y✝ : α ⊕ β →₀ M
a✝ : β
⊢ (sumFinsuppEquivProdFinsupp.toFun (x✝ + y✝)).2 a✝ =
    (sumFinsuppEquivProdFinsupp.toFun x✝ + sumFinsuppEquivProdFinsupp.toFun y✝).2 a✝

Tactic:
<;>

Goal state after:
case fst
α✝ : 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 γ
inst✝ : AddMonoid M
α : Type u_12
β : Type u_13
x✝ y✝ : α ⊕ β →₀ M
a✝ : α
⊢ (sumFinsuppEquivProdFinsupp.toFun (x✝ + y✝)).1 a✝ =
    (sumFinsuppEquivProdFinsupp.toFun x✝ + sumFinsuppEquivProdFinsupp.toFun y✝).1 a✝

case snd
α✝ : 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 γ
inst✝ : AddMonoid M
α : Type u_12
β : Type u_13
x✝ y✝ : α ⊕ β →₀ M
a✝ : β
⊢ (sumFinsuppEquivProdFinsupp.toFun (x✝ + y✝)).2 a✝ =
    (sumFinsuppEquivProdFinsupp.toFun x✝ + sumFinsuppEquivProdFinsupp.toFun y✝).2 a✝
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
M : Type u_12
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
f : Subtype P →₀ M
g : { a // ¬P a } →₀ M
a : α
ha : P a
⊢ a ∈ (map (Embedding.subtype P) f.support).disjUnion (map (Embedding.subtype fun a ↦ ¬P a) g.support) ⋯ ↔
    (if h : P a then f ⟨a, h⟩ else g ⟨a, h⟩) ≠ 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
M : Type u_12
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
f : Subtype P →₀ M
g : { a // ¬P a } →₀ M
a : α
ha : ¬P a
⊢ a ∈ (map (Embedding.subtype P) f.support).disjUnion (map (Embedding.subtype fun a ↦ ¬P a) g.support) ⋯ ↔
    (if h : P a then f ⟨a, h⟩ else g ⟨a, h⟩) ≠ 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
M : Type u_12
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
f : Subtype P →₀ M
g : { a // ¬P a } →₀ M
a : α
ha : P a
⊢ a ∈ (map (Embedding.subtype P) f.support).disjUnion (map (Embedding.subtype fun a ↦ ¬P a) g.support) ⋯ ↔
    (if h : P a then f ⟨a, h⟩ else g ⟨a, h⟩) ≠ 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
M : Type u_12
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
f : Subtype P →₀ M
g : { a // ¬P a } →₀ M
a : α
ha : ¬P a
⊢ a ∈ (map (Embedding.subtype P) f.support).disjUnion (map (Embedding.subtype fun a ↦ ¬P a) g.support) ⋯ ↔
    (if h : P a then f ⟨a, h⟩ else g ⟨a, h⟩) ≠ 0
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: case neg
α : Type u_1
M : Type u_12
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
f : Subtype P →₀ M
a : α
h : ¬P a
⊢ f.extendDomain a = 0

pp: case neg.h
α : Type u_1
M : Type u_12
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
f : Subtype P →₀ M
a : α
h : ¬P a
⊢ a ∉ Set.range ⇑(Embedding.subtype P)

Tactic:
<;>

Goal state after:
case neg
α : Type u_1
M : Type u_12
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
f : Subtype P →₀ M
a : α
h : ¬P a
⊢ f.extendDomain a = 0

case neg.h
α : Type u_1
M : Type u_12
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
f : Subtype P →₀ M
a : α
h : ¬P a
⊢ a ∉ Set.range ⇑(Embedding.subtype P)
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: case inl
α : Type u_1
M : Type u_12
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
a : Subtype P
m : M
⊢ (single a m).extendDomain ↑a = (single (↑a) m) ↑a

pp: case inr
α : Type u_1
M : Type u_12
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
a : Subtype P
m : M
a' : α
ha : a' ≠ ↑a
⊢ (single a m).extendDomain a' = (single (↑a) m) a'

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
M : Type u_12
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
a : Subtype P
m : M
⊢ (single a m).extendDomain ↑a = (single (↑a) m) ↑a

case inr
α : Type u_1
M : Type u_12
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
a : Subtype P
m : M
a' : α
ha : a' ≠ ↑a
⊢ (single a m).extendDomain a' = (single (↑a) m) a'
Module: Mathlib.Data.Finsupp.SMul

Goal state before:
pp: case pos
α : Type u_1
M : Type u_3
R : Type u_6
inst✝² : Zero M
inst✝¹ : MonoidWithZero R
inst✝ : MulActionWithZero R M
a b : α
f : α → M
r : R
h : a = b
⊢ (single a r) b • f a = (single a (r • f b)) b

pp: case neg
α : Type u_1
M : Type u_3
R : Type u_6
inst✝² : Zero M
inst✝¹ : MonoidWithZero R
inst✝ : MulActionWithZero R M
a b : α
f : α → M
r : R
h : ¬a = b
⊢ (single a r) b • f a = (single a (r • f b)) b

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
M : Type u_3
R : Type u_6
inst✝² : Zero M
inst✝¹ : MonoidWithZero R
inst✝ : MulActionWithZero R M
a b : α
f : α → M
r : R
h : a = b
⊢ (single a r) b • f a = (single a (r • f b)) b

case neg
α : Type u_1
M : Type u_3
R : Type u_6
inst✝² : Zero M
inst✝¹ : MonoidWithZero R
inst✝ : MulActionWithZero R M
a b : α
f : α → M
r : R
h : ¬a = b
⊢ (single a r) b • f a = (single a (r • f b)) b
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: case inl
ι : Type u_1
M : Type u_4
inst✝³ : Fintype ι
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedCancelMonoid M
hf : 1 ≤ 1
⊢ 1 < ∏ i, 1 i ↔ 1 < 1

pp: case inr
ι : Type u_1
M : Type u_4
inst✝³ : Fintype ι
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedCancelMonoid M
f : ι → M
hf✝ : 1 ≤ f
hf : 1 < f
⊢ 1 < ∏ i, f i ↔ 1 < f

Tactic:
<;>

Goal state after:
case inl
ι : Type u_1
M : Type u_4
inst✝³ : Fintype ι
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedCancelMonoid M
hf : 1 ≤ 1
⊢ 1 < ∏ i, 1 i ↔ 1 < 1

case inr
ι : Type u_1
M : Type u_4
inst✝³ : Fintype ι
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedCancelMonoid M
f : ι → M
hf✝ : 1 ≤ f
hf : 1 < f
⊢ 1 < ∏ i, f i ↔ 1 < f
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: case inl
ι : Type u_1
M : Type u_4
inst✝³ : Fintype ι
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedCancelMonoid M
hf : 1 ≤ 1
⊢ ∏ i, 1 i < 1 ↔ 1 < 1

pp: case inr
ι : Type u_1
M : Type u_4
inst✝³ : Fintype ι
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedCancelMonoid M
f : ι → M
hf✝ : f ≤ 1
hf : f < 1
⊢ ∏ i, f i < 1 ↔ f < 1

Tactic:
<;>

Goal state after:
case inl
ι : Type u_1
M : Type u_4
inst✝³ : Fintype ι
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedCancelMonoid M
hf : 1 ≤ 1
⊢ ∏ i, 1 i < 1 ↔ 1 < 1

case inr
ι : Type u_1
M : Type u_4
inst✝³ : Fintype ι
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedCancelMonoid M
f : ι → M
hf✝ : f ≤ 1
hf : f < 1
⊢ ∏ i, f i < 1 ↔ f < 1
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case inr
ι : Sort u_6
R : Type u_7
M : Type u_8
inst✝⁴ : Semiring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.IsTorsionFree R M
c : R
f : ι → M
hc : c ≠ 0
⊢ c • ∑ᶠ (i : ι), f i = ∑ᶠ (i : ι), c • f i

Tactic:
· exact (smulAddHom R M c).map_finsum_of_injective (smul_right_injective M hc) _

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Finset α
h : mulSupport f ⊆ ↑s
A : mulSupport (f ∘ PLift.down) = ⇑Equiv.plift.symm '' mulSupport f
this : mulSupport (f ∘ PLift.down) ⊆ ↑(Finset.map Equiv.plift.symm.toEmbedding s)
⊢ ∏ᶠ (i : α), f i = ∏ i ∈ s, f i

Tactic:
finprod_eq_prod_plift_of_mulSupport_subset this

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Finset α
h : mulSupport f ⊆ ↑s
A : mulSupport (f ∘ PLift.down) = ⇑Equiv.plift.symm '' mulSupport f
this : mulSupport (f ∘ PLift.down) ⊆ ↑(Finset.map Equiv.plift.symm.toEmbedding s)
⊢ ∏ i ∈ Finset.map Equiv.plift.symm.toEmbedding s, f i.down = ∏ i ∈ s, f i
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: ι : Type u_3
M : Type u_7
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedCancelMonoid M
f : ι → M
p : ι → Prop
h : ∀ (i : ι), p i → 1 ≤ f i
h' : ∃ i, p i ∧ 1 < f i
hf : (mulSupport f ∩ {i | p i}).Finite
⊢ 1 < ∏ᶠ (i : ι) (_ : p i), f i

Tactic:
by
  rw [finprod_cond_eq_prod_of_cond_iff (t := hf.toFinset)]
  · apply Finset.one_lt_prod'
    · simp +contextual [h]
    · aesop
  · simp +contextual

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case h
ι : Type u_3
M : Type u_7
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedCancelMonoid M
f : ι → M
h : ∀ (i : ι), 1 ≤ f i
h' : ∃ i, 1 < f i
hf : HasFiniteMulSupport f
⊢ ∀ i ∈ univ, 1 ≤ f i

pp: case h'
ι : Type u_3
M : Type u_7
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedCancelMonoid M
f : ι → M
h : ∀ (i : ι), 1 ≤ f i
h' : ∃ i, 1 < f i
hf : HasFiniteMulSupport f
⊢ ∃ i ∈ univ, 1 < f i

pp: case hf
ι : Type u_3
M : Type u_7
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedCancelMonoid M
f : ι → M
h : ∀ (i : ι), 1 ≤ f i
h' : ∃ i, 1 < f i
hf : HasFiniteMulSupport f
⊢ (mulSupport f ∩ {i | i ∈ univ}).Finite

Tactic:
<;>

Goal state after:
case h
ι : Type u_3
M : Type u_7
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedCancelMonoid M
f : ι → M
h : ∀ (i : ι), 1 ≤ f i
h' : ∃ i, 1 < f i
hf : HasFiniteMulSupport f
⊢ ∀ i ∈ univ, 1 ≤ f i

case h'
ι : Type u_3
M : Type u_7
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedCancelMonoid M
f : ι → M
h : ∀ (i : ι), 1 ≤ f i
h' : ∃ i, 1 < f i
hf : HasFiniteMulSupport f
⊢ ∃ i ∈ univ, 1 < f i

case hf
ι : Type u_3
M : Type u_7
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedCancelMonoid M
f : ι → M
h : ∀ (i : ι), 1 ≤ f i
h' : ∃ i, 1 < f i
hf : HasFiniteMulSupport f
⊢ (mulSupport f ∩ {i | i ∈ univ}).Finite
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_3
inst✝³ : Fintype α
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
⊢ map (Finsupp.linearCombination R v) (↑(Finsupp.linearEquivFunOnFinite R R α).symm).range = span R (Set.range v)

Tactic:
LinearEquiv.range,

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_3
inst✝³ : Fintype α
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
⊢ map (Finsupp.linearCombination R v) ⊤ = span R (Set.range v)
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: M' : Type u_7
inst✝⁷ : AddCommMonoid M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
b : Basis ι R M
inst✝³ : Module R M'
S : Type u_13
inst✝² : Semiring S
inst✝¹ : Module S M'
inst✝ : SMulCommClass R S M'
f : ι → M'
x : M
⊢ ((↑b.repr x).sum fun a m ↦ m • id (f a)) = (b.repr x).sum fun b a ↦ a • f b

pp: case h_zero
M' : Type u_7
inst✝⁷ : AddCommMonoid M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
b : Basis ι R M
inst✝³ : Module R M'
S : Type u_13
inst✝² : Semiring S
inst✝¹ : Module S M'
inst✝ : SMulCommClass R S M'
f : ι → M'
x : M
⊢ ∀ (b : M'), 0 • id b = 0

pp: case h_add
M' : Type u_7
inst✝⁷ : AddCommMonoid M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
b : Basis ι R M
inst✝³ : Module R M'
S : Type u_13
inst✝² : Semiring S
inst✝¹ : Module S M'
inst✝ : SMulCommClass R S M'
f : ι → M'
x : M
⊢ ∀ (b : M') (m₁ m₂ : R), (m₁ + m₂) • id b = m₁ • id b + m₂ • id b

Tactic:
<;>

Goal state after:
M' : Type u_7
inst✝⁷ : AddCommMonoid M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
b : Basis ι R M
inst✝³ : Module R M'
S : Type u_13
inst✝² : Semiring S
inst✝¹ : Module S M'
inst✝ : SMulCommClass R S M'
f : ι → M'
x : M
⊢ ((↑b.repr x).sum fun a m ↦ m • id (f a)) = (b.repr x).sum fun b a ↦ a • f b

case h_zero
M' : Type u_7
inst✝⁷ : AddCommMonoid M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
b : Basis ι R M
inst✝³ : Module R M'
S : Type u_13
inst✝² : Semiring S
inst✝¹ : Module S M'
inst✝ : SMulCommClass R S M'
f : ι → M'
x : M
⊢ ∀ (b : M'), 0 • id b = 0

case h_add
M' : Type u_7
inst✝⁷ : AddCommMonoid M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
b : Basis ι R M
inst✝³ : Module R M'
S : Type u_13
inst✝² : Semiring S
inst✝¹ : Module S M'
inst✝ : SMulCommClass R S M'
f : ι → M'
x : M
⊢ ∀ (b : M') (m₁ m₂ : R), (m₁ + m₂) • id b = m₁ • id b + m₂ • id b
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: M' : Type u_7
inst✝⁷ : AddCommMonoid M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
b : Basis ι R M
inst✝³ : Module R M'
S : Type u_13
inst✝² : Semiring S
inst✝¹ : Module S M'
inst✝ : SMulCommClass R S M'
f : ι → M'
⊢ map (linearCombination R id) (map (lmapDomain R R f) (↑b.repr).range) = span R (range f)

Tactic:
LinearEquiv.range,

Goal state after:
M' : Type u_7
inst✝⁷ : AddCommMonoid M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
b : Basis ι R M
inst✝³ : Module R M'
S : Type u_13
inst✝² : Semiring S
inst✝¹ : Module S M'
inst✝ : SMulCommClass R S M'
f : ι → M'
⊢ map (linearCombination R id) (map (lmapDomain R R f) ⊤) = span R (range f)
Module: Mathlib.Data.Fintype.Fin

Goal state before:
pp: case pos
n : ℕ
p : Fin (n + 1) → Prop
inst✝ : DecidablePred p
h✝ : p 0
⊢ #{x | p x.succ} + 1 = 1 + #{x | p x.succ}

pp: case neg
n : ℕ
p : Fin (n + 1) → Prop
inst✝ : DecidablePred p
h✝ : ¬p 0
⊢ #{x | p x.succ} = 0 + #{x | p x.succ}

Tactic:
<;>

Goal state after:
case pos
n : ℕ
p : Fin (n + 1) → Prop
inst✝ : DecidablePred p
h✝ : p 0
⊢ #{x | p x.succ} + 1 = 1 + #{x | p x.succ}

case neg
n : ℕ
p : Fin (n + 1) → Prop
inst✝ : DecidablePred p
h✝ : ¬p 0
⊢ #{x | p x.succ} = 0 + #{x | p x.succ}