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

Goal state before:
pp: case refine_1
k : Type u_1
G : Type u_2
inst✝² : Mul G
inst✝¹ : NonUnitalNonAssocSemiring k
inst✝ : DistribSMul G k
f g h : SkewMonoidAlgebra k G
x✝¹ : G
x✝ : k
⊢ ∀ a ∈ g.support ∪ h.support, single (x✝¹ * a) (x✝ * x✝¹ • 0) = 0

pp: case refine_2
k : Type u_1
G : Type u_2
inst✝² : Mul G
inst✝¹ : NonUnitalNonAssocSemiring k
inst✝ : DistribSMul G k
f g h : SkewMonoidAlgebra k G
x✝¹ : G
x✝ : k
⊢ ∀ a ∈ g.support ∪ h.support,
    ∀ (b₁ b₂ : k),
      single (x✝¹ * a) (x✝ * x✝¹ • (b₁ + b₂)) = single (x✝¹ * a) (x✝ * x✝¹ • b₁) + single (x✝¹ * a) (x✝ * x✝¹ • b₂)

pp: case refine_3
k : Type u_1
G : Type u_2
inst✝² : Mul G
inst✝¹ : NonUnitalNonAssocSemiring k
inst✝ : DistribSMul G k
f g h : SkewMonoidAlgebra k G
⊢ (f.sum fun x x_1 ↦
      (g.sum fun a₂ b₂ ↦ single (x * a₂) (x_1 * x • b₂)) + h.sum fun a₂ b₂ ↦ single (x * a₂) (x_1 * x • b₂)) =
    (f.sum fun a₁ b₁ ↦ g.sum fun a₂ b₂ ↦ single (a₁ * a₂) (b₁ * a₁ • b₂)) +
      f.sum fun a₁ b₁ ↦ h.sum fun a₂ b₂ ↦ single (a₁ * a₂) (b₁ * a₁ • b₂)

Tactic:
<;>

Goal state after:
case refine_1
k : Type u_1
G : Type u_2
inst✝² : Mul G
inst✝¹ : NonUnitalNonAssocSemiring k
inst✝ : DistribSMul G k
f g h : SkewMonoidAlgebra k G
x✝¹ : G
x✝ : k
⊢ ∀ a ∈ g.support ∪ h.support, single (x✝¹ * a) (x✝ * x✝¹ • 0) = 0

case refine_2
k : Type u_1
G : Type u_2
inst✝² : Mul G
inst✝¹ : NonUnitalNonAssocSemiring k
inst✝ : DistribSMul G k
f g h : SkewMonoidAlgebra k G
x✝¹ : G
x✝ : k
⊢ ∀ a ∈ g.support ∪ h.support,
    ∀ (b₁ b₂ : k),
      single (x✝¹ * a) (x✝ * x✝¹ • (b₁ + b₂)) = single (x✝¹ * a) (x✝ * x✝¹ • b₁) + single (x✝¹ * a) (x✝ * x✝¹ • b₂)

case refine_3
k : Type u_1
G : Type u_2
inst✝² : Mul G
inst✝¹ : NonUnitalNonAssocSemiring k
inst✝ : DistribSMul G k
f g h : SkewMonoidAlgebra k G
⊢ (f.sum fun x x_1 ↦
      (g.sum fun a₂ b₂ ↦ single (x * a₂) (x_1 * x • b₂)) + h.sum fun a₂ b₂ ↦ single (x * a₂) (x_1 * x • b₂)) =
    (f.sum fun a₁ b₁ ↦ g.sum fun a₂ b₂ ↦ single (a₁ * a₂) (b₁ * a₁ • b₂)) +
      f.sum fun a₁ b₁ ↦ h.sum fun a₂ b₂ ↦ single (a₁ * a₂) (b₁ * a₁ • b₂)
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: case refine_1
k : Type u_1
G : Type u_2
inst✝² : Mul G
inst✝¹ : NonUnitalNonAssocSemiring k
inst✝ : DistribSMul G k
f g h : SkewMonoidAlgebra k G
⊢ ∀ a ∈ f.support ∪ g.support, (h.sum fun a₂ b₂ ↦ single (a * a₂) (0 * a • b₂)) = 0

pp: case refine_2
k : Type u_1
G : Type u_2
inst✝² : Mul G
inst✝¹ : NonUnitalNonAssocSemiring k
inst✝ : DistribSMul G k
f g h : SkewMonoidAlgebra k G
⊢ ∀ a ∈ f.support ∪ g.support,
    ∀ (b₁ b₂ : k),
      (h.sum fun a₂ b₂_1 ↦ single (a * a₂) ((b₁ + b₂) * a • b₂_1)) =
        (h.sum fun a₂ b₂ ↦ single (a * a₂) (b₁ * a • b₂)) + h.sum fun a₂ b₂_1 ↦ single (a * a₂) (b₂ * a • b₂_1)

pp: case refine_3
k : Type u_1
G : Type u_2
inst✝² : Mul G
inst✝¹ : NonUnitalNonAssocSemiring k
inst✝ : DistribSMul G k
f g h : SkewMonoidAlgebra k G
⊢ ((f.sum fun a₁ b₁ ↦ h.sum fun a₂ b₂ ↦ single (a₁ * a₂) (b₁ * a₁ • b₂)) +
      g.sum fun a₁ b₁ ↦ h.sum fun a₂ b₂ ↦ single (a₁ * a₂) (b₁ * a₁ • b₂)) =
    (f.sum fun a₁ b₁ ↦ h.sum fun a₂ b₂ ↦ single (a₁ * a₂) (b₁ * a₁ • b₂)) +
      g.sum fun a₁ b₁ ↦ h.sum fun a₂ b₂ ↦ single (a₁ * a₂) (b₁ * a₁ • b₂)

Tactic:
<;>

Goal state after:
case refine_1
k : Type u_1
G : Type u_2
inst✝² : Mul G
inst✝¹ : NonUnitalNonAssocSemiring k
inst✝ : DistribSMul G k
f g h : SkewMonoidAlgebra k G
⊢ ∀ a ∈ f.support ∪ g.support, (h.sum fun a₂ b₂ ↦ single (a * a₂) (0 * a • b₂)) = 0

case refine_2
k : Type u_1
G : Type u_2
inst✝² : Mul G
inst✝¹ : NonUnitalNonAssocSemiring k
inst✝ : DistribSMul G k
f g h : SkewMonoidAlgebra k G
⊢ ∀ a ∈ f.support ∪ g.support,
    ∀ (b₁ b₂ : k),
      (h.sum fun a₂ b₂_1 ↦ single (a * a₂) ((b₁ + b₂) * a • b₂_1)) =
        (h.sum fun a₂ b₂ ↦ single (a * a₂) (b₁ * a • b₂)) + h.sum fun a₂ b₂_1 ↦ single (a * a₂) (b₂ * a • b₂_1)

case refine_3
k : Type u_1
G : Type u_2
inst✝² : Mul G
inst✝¹ : NonUnitalNonAssocSemiring k
inst✝ : DistribSMul G k
f g h : SkewMonoidAlgebra k G
⊢ ((f.sum fun a₁ b₁ ↦ h.sum fun a₂ b₂ ↦ single (a₁ * a₂) (b₁ * a₁ • b₂)) +
      g.sum fun a₁ b₁ ↦ h.sum fun a₂ b₂ ↦ single (a₁ * a₂) (b₁ * a₁ • b₂)) =
    (f.sum fun a₁ b₁ ↦ h.sum fun a₂ b₂ ↦ single (a₁ * a₂) (b₁ * a₁ • b₂)) +
      g.sum fun a₁ b₁ ↦ h.sum fun a₂ b₂ ↦ single (a₁ * a₂) (b₁ * a₁ • b₂)
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: case single
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Monoid G
inst✝ : MulSemiringAction G k
g : G
a : k
⊢ ((single g a).sum fun a₂ b₂ ↦ single (1 * a₂) (1 * 1 • b₂)) = single g a

pp: case single
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Monoid G
inst✝ : MulSemiringAction G k
g : G
a : k
⊢ ((single g a).sum fun a₂ b₂ ↦ single (1 * a₂) (0 * 1 • b₂)) = 0

Tactic:
<;>

Goal state after:
case single
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Monoid G
inst✝ : MulSemiringAction G k
g : G
a : k
⊢ ((single g a).sum fun a₂ b₂ ↦ single (1 * a₂) (1 * 1 • b₂)) = single g a

case single
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Monoid G
inst✝ : MulSemiringAction G k
g : G
a : k
⊢ ((single g a).sum fun a₂ b₂ ↦ single (1 * a₂) (0 * 1 • b₂)) = 0
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: case single
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Monoid G
inst✝ : MulSemiringAction G k
g : G
a : k
⊢ single (g * 1) (a * g • 1) = single g a

pp: case single
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Monoid G
inst✝ : MulSemiringAction G k
g : G
a : k
⊢ single (g * 1) (a * g • 0) = 0

pp: case single
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Monoid G
inst✝ : MulSemiringAction G k
g : G
a : k
⊢ ((single 1 1).sum fun a₂ b₂ ↦ single (g * a₂) (0 * g • b₂)) = 0

Tactic:
<;>

Goal state after:
case single
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Monoid G
inst✝ : MulSemiringAction G k
g : G
a : k
⊢ single (g * 1) (a * g • 1) = single g a

case single
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Monoid G
inst✝ : MulSemiringAction G k
g : G
a : k
⊢ single (g * 1) (a * g • 0) = 0

case single
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Monoid G
inst✝ : MulSemiringAction G k
g : G
a : k
⊢ ((single 1 1).sum fun a₂ b₂ ↦ single (g * a₂) (0 * g • b₂)) = 0
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: case pos
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : SMulZeroClass G k
f g : SkewMonoidAlgebra k G
x : G
s : Finset (G × G)
hs : ∀ {p : G × G}, p ∈ s ↔ p.1 * p.2 = x
F : G × G → k := fun p ↦ if p.1 * p.2 = x then f.coeff p.1 * p.1 • g.coeff p.2 else 0
p : G × G
hps : p ∈ s
hp : p ∈ s → f.coeff p.1 ≠ 0 → g.coeff p.2 = 0
h1 : f.coeff p.1 = 0
⊢ f.coeff p.1 * p.1 • g.coeff p.2 = 0

pp: case neg
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : SMulZeroClass G k
f g : SkewMonoidAlgebra k G
x : G
s : Finset (G × G)
hs : ∀ {p : G × G}, p ∈ s ↔ p.1 * p.2 = x
F : G × G → k := fun p ↦ if p.1 * p.2 = x then f.coeff p.1 * p.1 • g.coeff p.2 else 0
p : G × G
hps : p ∈ s
hp : p ∈ s → f.coeff p.1 ≠ 0 → g.coeff p.2 = 0
h1 : ¬f.coeff p.1 = 0
⊢ f.coeff p.1 * p.1 • g.coeff p.2 = 0

Tactic:
<;>

Goal state after:
case pos
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : SMulZeroClass G k
f g : SkewMonoidAlgebra k G
x : G
s : Finset (G × G)
hs : ∀ {p : G × G}, p ∈ s ↔ p.1 * p.2 = x
F : G × G → k := fun p ↦ if p.1 * p.2 = x then f.coeff p.1 * p.1 • g.coeff p.2 else 0
p : G × G
hps : p ∈ s
hp : p ∈ s → f.coeff p.1 ≠ 0 → g.coeff p.2 = 0
h1 : f.coeff p.1 = 0
⊢ f.coeff p.1 * p.1 • g.coeff p.2 = 0

case neg
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : SMulZeroClass G k
f g : SkewMonoidAlgebra k G
x : G
s : Finset (G × G)
hs : ∀ {p : G × G}, p ∈ s ↔ p.1 * p.2 = x
F : G × G → k := fun p ↦ if p.1 * p.2 = x then f.coeff p.1 * p.1 • g.coeff p.2 else 0
p : G × G
hps : p ∈ s
hp : p ∈ s → f.coeff p.1 ≠ 0 → g.coeff p.2 = 0
h1 : ¬f.coeff p.1 = 0
⊢ f.coeff p.1 * p.1 • g.coeff p.2 = 0
Module: Mathlib.Algebra.Tropical.Basic

Goal state before:
pp: case pos
R : Type u
inst✝ : LinearOrder R
a b : Tropical R
h✝ : a ≤ b
⊢ untrop a = untrop a

pp: case neg
R : Type u
inst✝ : LinearOrder R
a b : Tropical R
h✝ : ¬a ≤ b
⊢ untrop b = untrop b

Tactic:
<;>

Goal state after:
case pos
R : Type u
inst✝ : LinearOrder R
a b : Tropical R
h✝ : a ≤ b
⊢ untrop a = untrop a

case neg
R : Type u
inst✝ : LinearOrder R
a b : Tropical R
h✝ : ¬a ≤ b
⊢ untrop b = untrop b
Module: Mathlib.Algebra.Tropical.Basic

Goal state before:
pp: case pos
R : Type u
inst✝ : LinearOrder R
a b : Tropical R
h✝ : a ≤ b
⊢ untrop b = untrop b

pp: case neg
R : Type u
inst✝ : LinearOrder R
a b : Tropical R
h✝ : ¬a ≤ b
⊢ untrop a = untrop a

Tactic:
<;>

Goal state after:
case pos
R : Type u
inst✝ : LinearOrder R
a b : Tropical R
h✝ : a ≤ b
⊢ untrop b = untrop b

case neg
R : Type u
inst✝ : LinearOrder R
a b : Tropical R
h✝ : ¬a ≤ b
⊢ untrop a = untrop a
Module: Mathlib.Algebra.Tropical.Basic

Goal state before:
pp: case zero
R : Type u
inst✝² : LinearOrder R
inst✝¹ : OrderTop R
inst✝ : Zero R
⊢ untrop (if 0 + 1 = 0 then 0 else 1) = untrop ((if 0 = 0 then 0 else 1) + 1)

pp: case succ
R : Type u
inst✝² : LinearOrder R
inst✝¹ : OrderTop R
inst✝ : Zero R
n✝ : ℕ
⊢ untrop (if n✝ + 1 + 1 = 0 then 0 else 1) = untrop ((if n✝ + 1 = 0 then 0 else 1) + 1)

Tactic:
<;>

Goal state after:
case zero
R : Type u
inst✝² : LinearOrder R
inst✝¹ : OrderTop R
inst✝ : Zero R
⊢ untrop (if 0 + 1 = 0 then 0 else 1) = untrop ((if 0 = 0 then 0 else 1) + 1)

case succ
R : Type u
inst✝² : LinearOrder R
inst✝¹ : OrderTop R
inst✝ : Zero R
n✝ : ℕ
⊢ untrop (if n✝ + 1 + 1 = 0 then 0 else 1) = untrop ((if n✝ + 1 = 0 then 0 else 1) + 1)
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: case h₁
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : SMulZeroClass G k
f g : SkewMonoidAlgebra k G
x : G
this : ({p | p.1 * p.2 = x} ∩ Function.support fun p ↦ f.coeff p.1 * p.1 • g.coeff p.2).Finite
s : Finset (G × G) := ⋯
F : G × G → k := ⋯
⊢ ∀ a ∈ {p ∈ f.support ×ˢ g.support | p.1 * p.2 = x},
    a ∉ {p ∈ s | p.1 ∈ f.support ∧ p.2 ∈ g.support} → f.coeff a.1 * a.1 • g.coeff a.2 = 0

pp: case h₂
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : SMulZeroClass G k
f g : SkewMonoidAlgebra k G
x : G
this : ({p | p.1 * p.2 = x} ∩ Function.support fun p ↦ f.coeff p.1 * p.1 • g.coeff p.2).Finite
s : Finset (G × G) := ⋯
F : G × G → k := ⋯
⊢ ∀ a ∈ {p ∈ s | p.1 ∈ f.support ∧ p.2 ∈ g.support},
    a ∉ {p ∈ f.support ×ˢ g.support | p.1 * p.2 = x} → f.coeff a.1 * a.1 • g.coeff a.2 = 0

pp: case h
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : SMulZeroClass G k
f g : SkewMonoidAlgebra k G
x : G
this : ({p | p.1 * p.2 = x} ∩ Function.support fun p ↦ f.coeff p.1 * p.1 • g.coeff p.2).Finite
s : Finset (G × G) := ⋯
F : G × G → k := ⋯
⊢ ∀ a ∈ {p ∈ f.support ×ˢ g.support | p.1 * p.2 = x},
    a ∈ {p ∈ s | p.1 ∈ f.support ∧ p.2 ∈ g.support} → f.coeff a.1 * a.1 • g.coeff a.2 = f.coeff a.1 * a.1 • g.coeff a.2

Tactic:
<;>

Goal state after:
case h₁
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : SMulZeroClass G k
f g : SkewMonoidAlgebra k G
x : G
this : ({p | p.1 * p.2 = x} ∩ Function.support fun p ↦ f.coeff p.1 * p.1 • g.coeff p.2).Finite
s : Finset (G × G) := ⋯
F : G × G → k := ⋯
⊢ ∀ a ∈ {p ∈ f.support ×ˢ g.support | p.1 * p.2 = x},
    a ∉ {p ∈ s | p.1 ∈ f.support ∧ p.2 ∈ g.support} → f.coeff a.1 * a.1 • g.coeff a.2 = 0

case h₂
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : SMulZeroClass G k
f g : SkewMonoidAlgebra k G
x : G
this : ({p | p.1 * p.2 = x} ∩ Function.support fun p ↦ f.coeff p.1 * p.1 • g.coeff p.2).Finite
s : Finset (G × G) := ⋯
F : G × G → k := ⋯
⊢ ∀ a ∈ {p ∈ s | p.1 ∈ f.support ∧ p.2 ∈ g.support},
    a ∉ {p ∈ f.support ×ˢ g.support | p.1 * p.2 = x} → f.coeff a.1 * a.1 • g.coeff a.2 = 0

case h
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : SMulZeroClass G k
f g : SkewMonoidAlgebra k G
x : G
this : ({p | p.1 * p.2 = x} ∩ Function.support fun p ↦ f.coeff p.1 * p.1 • g.coeff p.2).Finite
s : Finset (G × G) := ⋯
F : G × G → k := ⋯
⊢ ∀ a ∈ {p ∈ f.support ×ˢ g.support | p.1 * p.2 = x},
    a ∈ {p ∈ s | p.1 ∈ f.support ∧ p.2 ∈ g.support} → f.coeff a.1 * a.1 • g.coeff a.2 = f.coeff a.1 * a.1 • g.coeff a.2
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: case pos
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : SMulZeroClass G k
f g : SkewMonoidAlgebra k G
x : G
this : ({p | p.1 * p.2 = x} ∩ Function.support fun p ↦ f.coeff p.1 * p.1 • g.coeff p.2).Finite
s : Finset (G × G) := this.toFinset
F : G × G → k := fun p ↦ if p.1 * p.2 = x then f.coeff p.1 * p.1 • g.coeff p.2 else 0
p : G × G
hps : p ∈ s
hp : p ∈ s → f.coeff p.1 ≠ 0 → g.coeff p.2 = 0
h1 : f.coeff p.1 = 0
⊢ f.coeff p.1 * p.1 • g.coeff p.2 = 0

pp: case neg
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : SMulZeroClass G k
f g : SkewMonoidAlgebra k G
x : G
this : ({p | p.1 * p.2 = x} ∩ Function.support fun p ↦ f.coeff p.1 * p.1 • g.coeff p.2).Finite
s : Finset (G × G) := this.toFinset
F : G × G → k := fun p ↦ if p.1 * p.2 = x then f.coeff p.1 * p.1 • g.coeff p.2 else 0
p : G × G
hps : p ∈ s
hp : p ∈ s → f.coeff p.1 ≠ 0 → g.coeff p.2 = 0
h1 : ¬f.coeff p.1 = 0
⊢ f.coeff p.1 * p.1 • g.coeff p.2 = 0

Tactic:
<;>

Goal state after:
case pos
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : SMulZeroClass G k
f g : SkewMonoidAlgebra k G
x : G
this : ({p | p.1 * p.2 = x} ∩ Function.support fun p ↦ f.coeff p.1 * p.1 • g.coeff p.2).Finite
s : Finset (G × G) := this.toFinset
F : G × G → k := fun p ↦ if p.1 * p.2 = x then f.coeff p.1 * p.1 • g.coeff p.2 else 0
p : G × G
hps : p ∈ s
hp : p ∈ s → f.coeff p.1 ≠ 0 → g.coeff p.2 = 0
h1 : f.coeff p.1 = 0
⊢ f.coeff p.1 * p.1 • g.coeff p.2 = 0

case neg
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : SMulZeroClass G k
f g : SkewMonoidAlgebra k G
x : G
this : ({p | p.1 * p.2 = x} ∩ Function.support fun p ↦ f.coeff p.1 * p.1 • g.coeff p.2).Finite
s : Finset (G × G) := this.toFinset
F : G × G → k := fun p ↦ if p.1 * p.2 = x then f.coeff p.1 * p.1 • g.coeff p.2 else 0
p : G × G
hps : p ∈ s
hp : p ∈ s → f.coeff p.1 ≠ 0 → g.coeff p.2 = 0
h1 : ¬f.coeff p.1 = 0
⊢ f.coeff p.1 * p.1 • g.coeff p.2 = 0
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: case pos
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : SMulZeroClass G k
f : SkewMonoidAlgebra k G
r : k
x y z : G
H : ∀ (a : G), a * x = z ↔ a = y
A :
  ∀ (a₁ : G) (b₁ : k),
    ((single x r).sum fun a₂ b₂ ↦ if a₁ * a₂ = z then b₁ * a₁ • b₂ else 0) = if a₁ * x = z then b₁ * a₁ • r else 0
h : y ∈ f.support
⊢ f.coeff y * y • r = f.coeff y * y • r

pp: case neg
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : SMulZeroClass G k
f : SkewMonoidAlgebra k G
r : k
x y z : G
H : ∀ (a : G), a * x = z ↔ a = y
A :
  ∀ (a₁ : G) (b₁ : k),
    ((single x r).sum fun a₂ b₂ ↦ if a₁ * a₂ = z then b₁ * a₁ • b₂ else 0) = if a₁ * x = z then b₁ * a₁ • r else 0
h : y ∉ f.support
⊢ 0 = f.coeff y * y • r

Tactic:
<;>

Goal state after:
case pos
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : SMulZeroClass G k
f : SkewMonoidAlgebra k G
r : k
x y z : G
H : ∀ (a : G), a * x = z ↔ a = y
A :
  ∀ (a₁ : G) (b₁ : k),
    ((single x r).sum fun a₂ b₂ ↦ if a₁ * a₂ = z then b₁ * a₁ • b₂ else 0) = if a₁ * x = z then b₁ * a₁ • r else 0
h : y ∈ f.support
⊢ f.coeff y * y • r = f.coeff y * y • r

case neg
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : SMulZeroClass G k
f : SkewMonoidAlgebra k G
r : k
x y z : G
H : ∀ (a : G), a * x = z ↔ a = y
A :
  ∀ (a₁ : G) (b₁ : k),
    ((single x r).sum fun a₂ b₂ ↦ if a₁ * a₂ = z then b₁ * a₁ • b₂ else 0) = if a₁ * x = z then b₁ * a₁ • r else 0
h : y ∉ f.support
⊢ 0 = f.coeff y * y • r
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: case pos
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : SMulZeroClass G k
f : SkewMonoidAlgebra k G
r : k
x y z : G
H : ∀ (a : G), a * x = z ↔ a = y
A :
  ∀ (a₁ : G) (b₁ : k),
    ((single x r).sum fun a₂ b₂ ↦ if a₁ * a₂ = z then b₁ * a₁ • b₂ else 0) = if a₁ * x = z then b₁ * a₁ • r else 0
h : ¬f.coeff y = 0
⊢ f.coeff y * y • r = f.coeff y * y • r

pp: case neg
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : SMulZeroClass G k
f : SkewMonoidAlgebra k G
r : k
x y z : G
H : ∀ (a : G), a * x = z ↔ a = y
A :
  ∀ (a₁ : G) (b₁ : k),
    ((single x r).sum fun a₂ b₂ ↦ if a₁ * a₂ = z then b₁ * a₁ • b₂ else 0) = if a₁ * x = z then b₁ * a₁ • r else 0
h : f.coeff y = 0
⊢ 0 = f.coeff y * y • r

Tactic:
<;>

Goal state after:
case pos
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : SMulZeroClass G k
f : SkewMonoidAlgebra k G
r : k
x y z : G
H : ∀ (a : G), a * x = z ↔ a = y
A :
  ∀ (a₁ : G) (b₁ : k),
    ((single x r).sum fun a₂ b₂ ↦ if a₁ * a₂ = z then b₁ * a₁ • b₂ else 0) = if a₁ * x = z then b₁ * a₁ • r else 0
h : ¬f.coeff y = 0
⊢ f.coeff y * y • r = f.coeff y * y • r

case neg
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : SMulZeroClass G k
f : SkewMonoidAlgebra k G
r : k
x y z : G
H : ∀ (a : G), a * x = z ↔ a = y
A :
  ∀ (a₁ : G) (b₁ : k),
    ((single x r).sum fun a₂ b₂ ↦ if a₁ * a₂ = z then b₁ * a₁ • b₂ else 0) = if a₁ * x = z then b₁ * a₁ • r else 0
h : f.coeff y = 0
⊢ 0 = f.coeff y * y • r
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: case pos
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : SMulZeroClass G k
f : SkewMonoidAlgebra k G
r : k
x y z : G
H : ∀ (a : G), x * a = y ↔ a = z
this : (f.sum fun a b ↦ if x * a = y then 0 * x • b else 0) = 0
h : z ∈ f.support
⊢ r * x • f.coeff z = r * x • f.coeff z

pp: case neg
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : SMulZeroClass G k
f : SkewMonoidAlgebra k G
r : k
x y z : G
H : ∀ (a : G), x * a = y ↔ a = z
this : (f.sum fun a b ↦ if x * a = y then 0 * x • b else 0) = 0
h : z ∉ f.support
⊢ 0 = r * x • f.coeff z

Tactic:
<;>

Goal state after:
case pos
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : SMulZeroClass G k
f : SkewMonoidAlgebra k G
r : k
x y z : G
H : ∀ (a : G), x * a = y ↔ a = z
this : (f.sum fun a b ↦ if x * a = y then 0 * x • b else 0) = 0
h : z ∈ f.support
⊢ r * x • f.coeff z = r * x • f.coeff z

case neg
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : SMulZeroClass G k
f : SkewMonoidAlgebra k G
r : k
x y z : G
H : ∀ (a : G), x * a = y ↔ a = z
this : (f.sum fun a b ↦ if x * a = y then 0 * x • b else 0) = 0
h : z ∉ f.support
⊢ 0 = r * x • f.coeff z
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: case pos
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : SMulZeroClass G k
f : SkewMonoidAlgebra k G
r : k
x y z : G
H : ∀ (a : G), x * a = y ↔ a = z
this : (f.sum fun a b ↦ if x * a = y then 0 * x • b else 0) = 0
h : ¬f.coeff z = 0
⊢ r * x • f.coeff z = r * x • f.coeff z

pp: case neg
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : SMulZeroClass G k
f : SkewMonoidAlgebra k G
r : k
x y z : G
H : ∀ (a : G), x * a = y ↔ a = z
this : (f.sum fun a b ↦ if x * a = y then 0 * x • b else 0) = 0
h : f.coeff z = 0
⊢ 0 = r * x • f.coeff z

Tactic:
<;>

Goal state after:
case pos
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : SMulZeroClass G k
f : SkewMonoidAlgebra k G
r : k
x y z : G
H : ∀ (a : G), x * a = y ↔ a = z
this : (f.sum fun a b ↦ if x * a = y then 0 * x • b else 0) = 0
h : ¬f.coeff z = 0
⊢ r * x • f.coeff z = r * x • f.coeff z

case neg
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : SMulZeroClass G k
f : SkewMonoidAlgebra k G
r : k
x y z : G
H : ∀ (a : G), x * a = y ↔ a = z
this : (f.sum fun a b ↦ if x * a = y then 0 * x • b else 0) = 0
h : f.coeff z = 0
⊢ 0 = r * x • f.coeff z
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: case refine_1
k : Type u_1
G : Type u_2
inst✝³ : Semiring k
inst✝² : Monoid G
inst✝¹ : MulSemiringAction G k
inst✝ : IsScalarTower k k k
t : k
a b : SkewMonoidAlgebra k G
⊢ ∀ (i : G), (b.sum fun a₂ b₂ ↦ single (i * a₂) (0 * i • b₂)) = 0

pp: case refine_2
k : Type u_1
G : Type u_2
inst✝³ : Semiring k
inst✝² : Monoid G
inst✝¹ : MulSemiringAction G k
inst✝ : IsScalarTower k k k
t : k
a b : SkewMonoidAlgebra k G
⊢ (a.sum fun x1 x2 ↦ b.sum fun a₂ b₂ ↦ single (x1 * a₂) (t • x2 * x1 • b₂)) = t • (a * b)

Tactic:
<;>

Goal state after:
case refine_1
k : Type u_1
G : Type u_2
inst✝³ : Semiring k
inst✝² : Monoid G
inst✝¹ : MulSemiringAction G k
inst✝ : IsScalarTower k k k
t : k
a b : SkewMonoidAlgebra k G
⊢ ∀ (i : G), (b.sum fun a₂ b₂ ↦ single (i * a₂) (0 * i • b₂)) = 0

case refine_2
k : Type u_1
G : Type u_2
inst✝³ : Semiring k
inst✝² : Monoid G
inst✝¹ : MulSemiringAction G k
inst✝ : IsScalarTower k k k
t : k
a b : SkewMonoidAlgebra k G
⊢ (a.sum fun x1 x2 ↦ b.sum fun a₂ b₂ ↦ single (x1 * a₂) (t • x2 * x1 • b₂)) = t • (a * b)
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace

Goal state before:
pp: case w
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : PresheafedSpace C
H : ↑X ≅ ↑Y
α : (Presheaf.pushforward C H.hom).obj X.presheaf ≅ Y.presheaf
x✝ : ↑↑X
⊢ (ConcreteCategory.hom
        ({ base := H.hom, c := α.inv } ≫ { base := H.inv, c := Presheaf.toPushforwardOfIso H α.hom }).base)
      x✝ =
    (ConcreteCategory.hom (𝟙 X).base) x✝

pp: case h
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : PresheafedSpace C
H : ↑X ≅ ↑Y
α : (Presheaf.pushforward C H.hom).obj X.presheaf ≅ Y.presheaf
U✝ : Opens ↑↑X
⊢ (({ base := H.hom, c := α.inv } ≫ { base := H.inv, c := Presheaf.toPushforwardOfIso H α.hom }).c ≫
          whiskerRight (eqToHom ⋯) X.presheaf).app
      (op U✝) =
    (𝟙 X).c.app (op U✝)

Tactic:
<;>

Goal state after:
case w
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : PresheafedSpace C
H : ↑X ≅ ↑Y
α : (Presheaf.pushforward C H.hom).obj X.presheaf ≅ Y.presheaf
x✝ : ↑↑X
⊢ (ConcreteCategory.hom
        ({ base := H.hom, c := α.inv } ≫ { base := H.inv, c := Presheaf.toPushforwardOfIso H α.hom }).base)
      x✝ =
    (ConcreteCategory.hom (𝟙 X).base) x✝

case h
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : PresheafedSpace C
H : ↑X ≅ ↑Y
α : (Presheaf.pushforward C H.hom).obj X.presheaf ≅ Y.presheaf
U✝ : Opens ↑↑X
⊢ (({ base := H.hom, c := α.inv } ≫ { base := H.inv, c := Presheaf.toPushforwardOfIso H α.hom }).c ≫
          whiskerRight (eqToHom ⋯) X.presheaf).app
      (op U✝) =
    (𝟙 X).c.app (op U✝)
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace

Goal state before:
pp: case refine_1
X✝ X : LocallyRingedSpace
U : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
⊢ 0 1 = 1

pp: case refine_2
X✝ X : LocallyRingedSpace
U : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
⊢ ∀ (x y : ↑(X.presheaf.1 U)),
    { toFun := 0, map_one' := ?refine_1 }.toFun (x * y) =
      { toFun := 0, map_one' := ?refine_1 }.toFun x * { toFun := 0, map_one' := ?refine_1 }.toFun y

pp: case refine_3
X✝ X : LocallyRingedSpace
U : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
⊢ (↑{ toFun := 0, map_one' := ?refine_1, map_mul' := ?refine_2 }).toFun 0 = 0

pp: case refine_4
X✝ X : LocallyRingedSpace
U : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
⊢ ∀ (x y : ↑(X.presheaf.1 U)),
    (↑{ toFun := 0, map_one' := ?refine_1, map_mul' := ?refine_2 }).toFun (x + y) =
      (↑{ toFun := 0, map_one' := ?refine_1, map_mul' := ?refine_2 }).toFun x +
        (↑{ toFun := 0, map_one' := ?refine_1, map_mul' := ?refine_2 }).toFun y

Tactic:
<;>

Goal state after:
case refine_1
X✝ X : LocallyRingedSpace
U : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
⊢ 0 1 = 1

case refine_2
X✝ X : LocallyRingedSpace
U : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
⊢ ∀ (x y : ↑(X.presheaf.1 U)),
    { toFun := 0, map_one' := ?refine_1 }.toFun (x * y) =
      { toFun := 0, map_one' := ?refine_1 }.toFun x * { toFun := 0, map_one' := ?refine_1 }.toFun y

case refine_3
X✝ X : LocallyRingedSpace
U : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
⊢ (↑{ toFun := 0, map_one' := ?refine_1, map_mul' := ?refine_2 }).toFun 0 = 0

case refine_4
X✝ X : LocallyRingedSpace
U : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
⊢ ∀ (x y : ↑(X.presheaf.1 U)),
    (↑{ toFun := 0, map_one' := ?refine_1, map_mul' := ?refine_2 }).toFun (x + y) =
      (↑{ toFun := 0, map_one' := ?refine_1, map_mul' := ?refine_2 }).toFun x +
        (↑{ toFun := 0, map_one' := ?refine_1, map_mul' := ?refine_2 }).toFun y