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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : SMulZeroClass G k
r : k
g g' : G
x : SkewMonoidAlgebra k G
h : ¬∃ d, g' = g * d
⊢ (x.sum fun a₂ b₂ ↦ if g * a₂ = g' then 0 * g • b₂ else 0) = 0

Tactic:
simp

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Group G
inst✝ : MulSemiringAction G k
f g : SkewMonoidAlgebra k G
x : G
⊢ (f.sum fun a b ↦ (single a b * g).coeff x) = f.sum fun a b ↦ b * a • g.coeff (a⁻¹ * x)

Tactic:
simp

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Group G
inst✝ : MulSemiringAction G k
f g : SkewMonoidAlgebra k G
x : G
⊢ (g.sum fun a b ↦ (f * single a b).coeff x) = g.sum fun a b ↦ f.coeff (x * a⁻¹) * (x * a⁻¹) • b

Tactic:
simp

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

Goal state before:
pp: α : Type u_3
α₂ : Type u_4
β : Type u_5
F : Type u_6
inst✝⁶ : Semiring β
inst✝⁵ : Monoid α
inst✝⁴ : Monoid α₂
inst✝³ : FunLike F α α₂
inst✝² : MulSemiringAction α β
inst✝¹ : MulSemiringAction α₂ β
inst✝ : MulHomClass F α α₂
f : F
x y : SkewMonoidAlgebra β α
hf : ∀ (a : α) (x : β), a • x = f a • x
⊢ ∀ (b : α₂), (((mapDomain ⇑f) y).sum fun a₂ b₂ ↦ single (b * a₂) (0 * b • b₂)) = 0

Tactic:
simp

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

Goal state before:
pp: α : Type u_3
α₂ : Type u_4
β : Type u_5
F : Type u_6
inst✝⁶ : Semiring β
inst✝⁵ : Monoid α
inst✝⁴ : Monoid α₂
inst✝³ : FunLike F α α₂
inst✝² : MulSemiringAction α β
inst✝¹ : MulSemiringAction α₂ β
inst✝ : MulHomClass F α α₂
f : F
x y : SkewMonoidAlgebra β α
hf : ∀ (a : α) (x : β), a • x = f a • x
a : α
b : β
c : α₂
⊢ ∀ (b_1 : α₂), single (f a * b_1) (b * f a • 0) = 0

Tactic:
simp

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

Goal state before:
pp: case e_g
α : Type u_3
α₂ : Type u_4
β : Type u_5
F : Type u_6
inst✝⁶ : Semiring β
inst✝⁵ : Monoid α
inst✝⁴ : Monoid α₂
inst✝³ : FunLike F α α₂
inst✝² : MulSemiringAction α β
inst✝¹ : MulSemiringAction α₂ β
inst✝ : MulHomClass F α α₂
f : F
x y : SkewMonoidAlgebra β α
hf : ∀ (a : α) (x : β), a • x = f a • x
a : α
b : β
c : α₂
⊢ (y.sum fun a₂ b₂ ↦ single (f a * f a₂) (b * a • b₂)).coeff c =
    (y.sum fun a_1 m ↦ single (f a * f a_1) (b * f a • m)).coeff c

Tactic:
hf

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

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

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : Semiring R
inst✝⁸ : InvolutiveStar R
inst✝⁷ : AddCommMonoid E
inst✝⁶ : Module R E
inst✝⁵ : StarAddMonoid E
inst✝⁴ : StarModule R E
inst✝³ : AddCommMonoid F
inst✝² : Module R F
inst✝¹ : StarAddMonoid F
inst✝ : StarModule R F
f : WithConv (E →ₗ[R] F)
⊢ ∀ (x y : E), star (f.ofConv (star (x + y))) = star (f.ofConv (star x)) + star (f.ofConv (star y))

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : Semiring R
inst✝⁸ : InvolutiveStar R
inst✝⁷ : AddCommMonoid E
inst✝⁶ : Module R E
inst✝⁵ : StarAddMonoid E
inst✝⁴ : StarModule R E
inst✝³ : AddCommMonoid F
inst✝² : Module R F
inst✝¹ : StarAddMonoid F
inst✝ : StarModule R F
f : WithConv (E →ₗ[R] F)
⊢ ∀ (m : R) (x : E), star (f.ofConv (star (m • x))) = (RingHom.id R) m • star (f.ofConv (star x))

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : Semiring R
inst✝⁸ : InvolutiveStar R
inst✝⁷ : AddCommMonoid E
inst✝⁶ : Module R E
inst✝⁵ : StarAddMonoid E
inst✝⁴ : StarModule R E
inst✝³ : AddCommMonoid F
inst✝² : Module R F
inst✝¹ : StarAddMonoid F
inst✝ : StarModule R F
x : WithConv (E →ₗ[R] F)
x✝ : E
⊢ (star (star x)).ofConv x✝ = x.ofConv x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : Semiring R
inst✝⁸ : InvolutiveStar R
inst✝⁷ : AddCommMonoid E
inst✝⁶ : Module R E
inst✝⁵ : StarAddMonoid E
inst✝⁴ : StarModule R E
inst✝³ : AddCommMonoid F
inst✝² : Module R F
inst✝¹ : StarAddMonoid F
inst✝ : StarModule R F
x y : WithConv (E →ₗ[R] F)
x✝ : E
⊢ (star (x + y)).ofConv x✝ = (star x + star y).ofConv x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹³ : Semiring R
inst✝¹² : InvolutiveStar R
inst✝¹¹ : AddCommMonoid E
inst✝¹⁰ : Module R E
inst✝⁹ : StarAddMonoid E
inst✝⁸ : StarModule R E
inst✝⁷ : AddCommMonoid F
inst✝⁶ : Module R F
inst✝⁵ : StarAddMonoid F
inst✝⁴ : StarModule R F
G : Type u_4
inst✝³ : AddCommMonoid G
inst✝² : Module R G
inst✝¹ : StarAddMonoid G
inst✝ : StarModule R G
f : WithConv (E →ₗ[R] F)
g : WithConv (G →ₗ[R] E)
x✝ : G
⊢ (star (toConv (f.ofConv ∘ₗ g.ofConv))).ofConv x✝ = (toConv ((star f).ofConv ∘ₗ (star g).ofConv)).ofConv x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_1
E : Type u_2
inst✝⁵ : Semiring R
inst✝⁴ : InvolutiveStar R
inst✝³ : AddCommMonoid E
inst✝² : Module R E
inst✝¹ : StarAddMonoid E
inst✝ : StarModule R E
x✝ : E
⊢ (star (toConv id)).ofConv x✝ = (toConv id).ofConv x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : Semiring R
inst✝⁸ : InvolutiveStar R
inst✝⁷ : AddCommMonoid E
inst✝⁶ : Module R E
inst✝⁵ : StarAddMonoid E
inst✝⁴ : StarModule R E
inst✝³ : AddCommMonoid F
inst✝² : Module R F
inst✝¹ : StarAddMonoid F
inst✝ : StarModule R F
⊢ star 0 = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_1
inst✝⁷ : Semiring R
inst✝⁶ : InvolutiveStar R
E : Type u_6
inst✝⁵ : NonUnitalNonAssocSemiring E
inst✝⁴ : StarRing E
inst✝³ : Module R E
inst✝² : StarModule R E
inst✝¹ : SMulCommClass R E E
inst✝ : IsScalarTower R E E
x x✝ : E
⊢ (star (toConv (mulLeft R x))).ofConv x✝ = (toConv (mulRight R (star x))).ofConv x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Star.LinearMap

Goal state before:
pp: R' : Type u_5
E : Type u_6
inst✝⁷ : CommSemiring R'
inst✝⁶ : StarRing R'
inst✝⁵ : NonUnitalNonAssocSemiring E
inst✝⁴ : StarRing E
inst✝³ : Module R' E
inst✝² : StarModule R' E
inst✝¹ : SMulCommClass R' E E
inst✝ : IsScalarTower R' E E
x✝¹ x✝ : E
⊢ (star (toConv (mul' R' E))).ofConv (x✝¹ ⊗ₜ[R'] x✝) =
    (toConv (mul' R' E ∘ₗ ↑(TensorProduct.comm R' E E))).ofConv (x✝¹ ⊗ₜ[R'] x✝)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁴ : Semiring R
inst✝¹³ : InvolutiveStar R
inst✝¹² : AddCommMonoid E
inst✝¹¹ : Module R E
inst✝¹⁰ : StarAddMonoid E
inst✝⁹ : StarModule R E
inst✝⁸ : AddCommMonoid F
inst✝⁷ : Module R F
inst✝⁶ : StarAddMonoid F
inst✝⁵ : StarModule R F
G : Type u_4
inst✝⁴ : AddCommMonoid G
inst✝³ : Module R G
inst✝² : StarAddMonoid G
inst✝¹ : StarModule R G
inst✝ : SMulCommClass R R F
x✝² : R
x✝¹ : WithConv (E →ₗ[R] F)
x✝ : E
⊢ (star (x✝² • x✝¹)).ofConv x✝ = (star x✝² • star x✝¹).ofConv x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_5
E : Type u_6
F : Type u_7
G : Type u_8
H : Type u_9
inst✝¹⁷ : CommSemiring R
inst✝¹⁶ : StarRing R
inst✝¹⁵ : AddCommMonoid E
inst✝¹⁴ : StarAddMonoid E
inst✝¹³ : Module R E
inst✝¹² : StarModule R E
inst✝¹¹ : AddCommMonoid F
inst✝¹⁰ : StarAddMonoid F
inst✝⁹ : Module R F
inst✝⁸ : StarModule R F
inst✝⁷ : AddCommMonoid G
inst✝⁶ : StarAddMonoid G
inst✝⁵ : Module R G
inst✝⁴ : StarModule R G
inst✝³ : AddCommMonoid H
inst✝² : StarAddMonoid H
inst✝¹ : Module R H
inst✝ : StarModule R H
f : WithConv (E →ₗ[R] F)
g : WithConv (G →ₗ[R] H)
x✝¹ : E
x✝ : G
⊢ (star (toConv (TensorProduct.map f.ofConv g.ofConv))).ofConv (x✝¹ ⊗ₜ[R] x✝) =
    (toConv (TensorProduct.map (star f).ofConv (star g).ofConv)).ofConv (x✝¹ ⊗ₜ[R] x✝)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_5
E : Type u_6
F : Type u_7
G : Type u_8
inst✝¹³ : CommSemiring R
inst✝¹² : StarRing R
inst✝¹¹ : AddCommMonoid E
inst✝¹⁰ : StarAddMonoid E
inst✝⁹ : Module R E
inst✝⁸ : StarModule R E
inst✝⁷ : AddCommMonoid F
inst✝⁶ : StarAddMonoid F
inst✝⁵ : Module R F
inst✝⁴ : StarModule R F
inst✝³ : AddCommMonoid G
inst✝² : StarAddMonoid G
inst✝¹ : Module R G
inst✝ : StarModule R G
f : WithConv (F →ₗ[R] G)
x✝¹ : E
x✝ : F
⊢ ((TensorProduct.AlgebraTensorModule.curry (star (toConv (lTensor E f.ofConv))).ofConv) x✝¹) x✝ =
    ((TensorProduct.AlgebraTensorModule.curry (toConv (lTensor E (star f).ofConv)).ofConv) x✝¹) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_5
E : Type u_6
F : Type u_7
G : Type u_8
inst✝¹³ : CommSemiring R
inst✝¹² : StarRing R
inst✝¹¹ : AddCommMonoid E
inst✝¹⁰ : StarAddMonoid E
inst✝⁹ : Module R E
inst✝⁸ : StarModule R E
inst✝⁷ : AddCommMonoid F
inst✝⁶ : StarAddMonoid F
inst✝⁵ : Module R F
inst✝⁴ : StarModule R F
inst✝³ : AddCommMonoid G
inst✝² : StarAddMonoid G
inst✝¹ : Module R G
inst✝ : StarModule R G
f : WithConv (E →ₗ[R] F)
x✝¹ : E
x✝ : G
⊢ ((TensorProduct.AlgebraTensorModule.curry (star (toConv (rTensor G f.ofConv))).ofConv) x✝¹) x✝ =
    ((TensorProduct.AlgebraTensorModule.curry (toConv (rTensor G (star f).ofConv)).ofConv) x✝¹) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Star.LinearMap

Goal state before:
pp: E : Type u_2
inst✝⁶ : AddCommMonoid E
inst✝⁵ : StarAddMonoid E
S : Type u_5
inst✝⁴ : Semiring S
inst✝³ : StarAddMonoid S
inst✝² : StarModule S S
inst✝¹ : Module S E
inst✝ : StarModule S E
a : E
⊢ (star (toConv (toSpanSingleton S E a))).ofConv 1 = (toConv (toSpanSingleton S E (star a))).ofConv 1

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Star.LinearMap

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝¹⁰ : AddCommMonoid E
inst✝⁹ : StarAddMonoid E
inst✝⁸ : AddCommMonoid F
inst✝⁷ : StarAddMonoid F
S : Type u_5
inst✝⁶ : Semiring S
inst✝⁵ : StarAddMonoid S
inst✝⁴ : StarModule S S
inst✝³ : Module S E
inst✝² : StarModule S E
inst✝¹ : Module S F
inst✝ : StarModule S F
f : WithConv (E →ₗ[S] S)
x : F
x✝ : E
⊢ (star (toConv (f.ofConv.smulRight x))).ofConv x✝ = (toConv ((star f).ofConv.smulRight (star x))).ofConv x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_5
A : Type u_6
C : Type u_7
inst✝¹² : CommSemiring R
inst✝¹¹ : StarRing R
inst✝¹⁰ : NonUnitalNonAssocSemiring A
inst✝⁹ : Module R A
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : IsScalarTower R A A
inst✝⁶ : StarRing A
inst✝⁵ : StarModule R A
inst✝⁴ : AddCommMonoid C
inst✝³ : Module R C
inst✝² : StarAddMonoid C
inst✝¹ : StarModule R C
inst✝ : CoalgebraStruct R C
h : star (toConv comul) = toConv (↑(TensorProduct.comm R C C) ∘ₗ comul)
f g : WithConv (C →ₗ[R] A)
x✝ : C
⊢ (toConv
          ((mul' R A ∘ₗ ↑(TensorProduct.comm R A A)) ∘ₗ
            (↑(TensorProduct.comm R A A) ∘ₗ TensorProduct.map (star g).ofConv (star f).ofConv) ∘ₗ comul)).ofConv
      x✝ =
    (toConv (mul' R A ∘ₗ TensorProduct.map (star g).ofConv (star f).ofConv ∘ₗ comul)).ofConv x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Vertex.VertexOperator

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
x✝³ x✝² : VertexOperator R V
x✝¹ : ℤ
x✝ : V
⊢ (coeff (x✝³ + x✝²) (-x✝¹ - 1)) x✝ = (((fun n ↦ coeff x✝³ (-n - 1)) + fun n ↦ coeff x✝² (-n - 1)) x✝¹) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Vertex.VertexOperator

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
x✝³ : R
x✝² : VertexOperator R V
x✝¹ : ℤ
x✝ : V
⊢ (coeff (x✝³ • x✝²) (-x✝¹ - 1)) x✝ = (((RingHom.id R) x✝³ • fun n ↦ coeff x✝² (-n - 1)) x✝¹) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_5
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
n : Type u_8
inst✝⁶ : DecidableEq n
B : n → Type u_9
inst✝⁵ : (i : n) → AddCommMonoid (B i)
inst✝⁴ : (i : n) → Module R (B i)
inst✝³ : (i : n) → StarAddMonoid (B i)
inst✝² : ∀ (i : n), StarModule R (B i)
inst✝¹ : Fintype n
inst✝ : (i : n) → CoalgebraStruct R (B i)
h : ∀ (i : n), star (toConv comul) = toConv (↑(TensorProduct.comm R (B i) (B i)) ∘ₗ comul)
i : n
x : B i
this : star (comul (star x)) = (TensorProduct.comm R (B i) (B i)) (comul x)
⊢ (TensorProduct.comm R ((i : n) → B i) ((i : n) → B i))
      ((TensorProduct.map (star (toConv (single R B i))).ofConv (star (toConv (single R B i))).ofConv) (comul x)) =
    (TensorProduct.comm R ((i : n) → B i) ((i : n) → B i)) ((TensorProduct.map (single R B i) (single R B i)) (comul x))

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_5
inst✝³ : CommSemiring R
inst✝² : StarRing R
n : Type u_8
inst✝¹ : DecidableEq n
inst✝ : Fintype n
x✝ : n
⊢ (star (toConv comul)).ofConv 1 = (toConv (↑(TensorProduct.comm R R R) ∘ₗ comul)).ofConv 1

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Star.LinearMap

Goal state before:
pp: R✝ : Type u_1
E : Type u_2
F : Type u_3
inst✝³¹ : Semiring R✝
inst✝³⁰ : InvolutiveStar R✝
inst✝²⁹ : AddCommMonoid E
inst✝²⁸ : Module R✝ E
inst✝²⁷ : StarAddMonoid E
inst✝²⁶ : StarModule R✝ E
inst✝²⁵ : AddCommMonoid F
inst✝²⁴ : Module R✝ F
inst✝²³ : StarAddMonoid F
inst✝²² : StarModule R✝ F
G : Type u_4
inst✝²¹ : AddCommMonoid G
inst✝²⁰ : Module R✝ G
inst✝¹⁹ : StarAddMonoid G
inst✝¹⁸ : StarModule R✝ G
R : Type u_5
A : Type u_6
C : Type u_7
inst✝¹⁷ : CommSemiring R
inst✝¹⁶ : StarRing R
inst✝¹⁵ : NonUnitalNonAssocSemiring A
inst✝¹⁴ : Module R A
inst✝¹³ : SMulCommClass R A A
inst✝¹² : IsScalarTower R A A
inst✝¹¹ : StarRing A
inst✝¹⁰ : StarModule R A
inst✝⁹ : AddCommMonoid C
inst✝⁸ : Module R C
inst✝⁷ : StarAddMonoid C
inst✝⁶ : StarModule R C
n : Type u_8
inst✝⁵ : DecidableEq n
B : n → Type u_9
inst✝⁴ : (i : n) → AddCommMonoid (B i)
inst✝³ : (i : n) → Module R (B i)
inst✝² : (i : n) → StarAddMonoid (B i)
inst✝¹ : ∀ (i : n), StarModule R (B i)
inst✝ : Fintype n
m : Type u_10
⊢ star (toConv comul) = toConv (↑(TensorProduct.comm R (n → R) (n → R)) ∘ₗ comul)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_4
m : Type u_5
n : Type u_6
inst✝³ : CommSemiring R
inst✝² : StarRing R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
f : WithConv ((m → R) →ₗ[R] n → R)
i✝ : n
j✝ : m
⊢ toMatrix' (star f).ofConv i✝ j✝ = (toMatrix' f.ofConv).map star i✝ j✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Vertex.HVertexOperator

Goal state before:
pp: Γ : Type u_1
inst✝⁵ : PartialOrder Γ
R : Type u_2
V : Type u_3
W : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
A : HVertexOperator Γ R V W
n : Γ
u v : V
⊢ ((of R).symm (A (u + v))).coeff n = ((of R).symm (A u)).coeff n + ((of R).symm (A v)).coeff n

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Vertex.HVertexOperator

Goal state before:
pp: Γ : Type u_1
inst✝⁵ : PartialOrder Γ
R : Type u_2
V : Type u_3
W : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
A : HVertexOperator Γ R V W
n : Γ
r : R
v : V
⊢ ((of R).symm (A (r • v))).coeff n = (RingHom.id R) r • ((of R).symm (A v)).coeff n

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Vertex.HVertexOperator

Goal state before:
pp: Γ : Type u_1
inst✝⁵ : PartialOrder Γ
R : Type u_2
V : Type u_3
W : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
x✝³ x✝² : HVertexOperator Γ R V W
x✝¹ : Γ
x✝ : V
⊢ { toFun := fun v ↦ ((of R).symm ((x✝³ + x✝²) v)).coeff x✝¹, map_add' := ⋯, map_smul' := ⋯ } x✝ =
    (((fun n ↦ { toFun := fun v ↦ ((of R).symm (x✝³ v)).coeff n, map_add' := ⋯, map_smul' := ⋯ }) + fun n ↦
          { toFun := fun v ↦ ((of R).symm (x✝² v)).coeff n, map_add' := ⋯, map_smul' := ⋯ })
        x✝¹)
      x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Vertex.HVertexOperator

Goal state before:
pp: Γ : Type u_1
inst✝⁵ : PartialOrder Γ
R : Type u_2
V : Type u_3
W : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
x✝³ : R
x✝² : HVertexOperator Γ R V W
x✝¹ : Γ
x✝ : V
⊢ { toFun := fun v ↦ ((of R).symm ((x✝³ • x✝²) v)).coeff x✝¹, map_add' := ⋯, map_smul' := ⋯ } x✝ =
    (((RingHom.id R) x✝³ • fun n ↦ { toFun := fun v ↦ ((of R).symm (x✝² v)).coeff n, map_add' := ⋯, map_smul' := ⋯ })
        x✝¹)
      x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Vertex.HVertexOperator

Goal state before:
pp: Γ : Type u_1
inst✝⁵ : PartialOrder Γ
R : Type u_2
V : Type u_3
W : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
f : Γ → V →ₗ[R] W
hf : ∀ (x : V), (Function.support fun x_1 ↦ (f x_1) x).IsPWO
x✝² x✝¹ : V
x✝ : Γ
⊢ ((of R).symm ((of R) { coeff := fun g ↦ (f g) (x✝² + x✝¹), isPWO_support' := ⋯ })).coeff x✝ =
    ((of R).symm
          ((of R) { coeff := fun g ↦ (f g) x✝², isPWO_support' := ⋯ } +
            (of R) { coeff := fun g ↦ (f g) x✝¹, isPWO_support' := ⋯ })).coeff
      x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Vertex.HVertexOperator

Goal state before:
pp: Γ : Type u_1
inst✝⁵ : PartialOrder Γ
R : Type u_2
V : Type u_3
W : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
f : Γ → V →ₗ[R] W
hf : ∀ (x : V), (Function.support fun x_1 ↦ (f x_1) x).IsPWO
x✝² : R
x✝¹ : V
x✝ : Γ
⊢ ((of R).symm ((of R) { coeff := fun g ↦ (f g) (x✝² • x✝¹), isPWO_support' := ⋯ })).coeff x✝ =
    ((of R).symm ((RingHom.id R) x✝² • (of R) { coeff := fun g ↦ (f g) x✝¹, isPWO_support' := ⋯ })).coeff x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Geometry.RingedSpace.Stalks

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X : PresheafedSpace C
x : ↑↑X
U✝ : Opens ↑↑X
hxU✝ : x ∈ U✝
⊢ X.presheaf.germ U✝ x hxU✝ ≫ (stalkFunctor C x).map (𝟙 X).c ≫ stalkPushforward C (𝟙 ↑X) X.presheaf x =
    X.presheaf.germ U✝ x hxU✝ ≫ 𝟙 (X.presheaf.stalk x)

Tactic:
simp

Goal state after:
Module: Mathlib.Geometry.RingedSpace.Stalks

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y Z : PresheafedSpace C
α : X ⟶ Y
β : Y ⟶ Z
x : ↑↑X
U : Opens ↑↑Z
hU : (TopCat.Hom.hom β.base) ((TopCat.Hom.hom α.base) x) ∈ U
⊢ colimit.ι
        (((whiskeringLeft (OpenNhds ((TopCat.Hom.hom β.base) ((TopCat.Hom.hom α.base) x)))ᵒᵖ (Opens ↑↑Z)ᵒᵖ C).obj
              (OpenNhds.inclusion ((TopCat.Hom.hom β.base) ((TopCat.Hom.hom α.base) x))).op).obj
          Z.presheaf)
        (op ⟨U, hU⟩) ≫
      colimMap ((OpenNhds.inclusion ((TopCat.Hom.hom β.base) ((TopCat.Hom.hom α.base) x))).op.whiskerLeft (α ≫ β).c) ≫
        colimMap (whiskerRight (𝟙 (OpenNhds.map (α.base ≫ β.base) x ⋙ OpenNhds.inclusion x).op) X.presheaf) ≫
          colimit.pre ((OpenNhds.inclusion x).op ⋙ X.presheaf) (OpenNhds.map (α.base ≫ β.base) x).op =
    colimit.ι
        (((whiskeringLeft (OpenNhds ((TopCat.Hom.hom β.base) ((TopCat.Hom.hom α.base) x)))ᵒᵖ (Opens ↑↑Z)ᵒᵖ C).obj
              (OpenNhds.inclusion ((TopCat.Hom.hom β.base) ((TopCat.Hom.hom α.base) x))).op).obj
          Z.presheaf)
        (op ⟨U, hU⟩) ≫
      (colimMap
            ((OpenNhds.inclusion ((ConcreteCategory.hom β.base) ((ConcreteCategory.hom α.base) x))).op.whiskerLeft
              β.c) ≫
          colimMap
              (whiskerRight
                (𝟙
                  (OpenNhds.map β.base ((ConcreteCategory.hom α.base) x) ⋙
                      OpenNhds.inclusion ((ConcreteCategory.hom α.base) x)).op)
                Y.presheaf) ≫
            colimit.pre ((OpenNhds.inclusion ((ConcreteCategory.hom α.base) x)).op ⋙ Y.presheaf)
              (OpenNhds.map β.base ((ConcreteCategory.hom α.base) x)).op) ≫
        colimMap ((OpenNhds.inclusion ((ConcreteCategory.hom α.base) x)).op.whiskerLeft α.c) ≫
          colimMap (whiskerRight (𝟙 (OpenNhds.map α.base x ⋙ OpenNhds.inclusion x).op) X.presheaf) ≫
            colimit.pre ((OpenNhds.inclusion x).op ⋙ X.presheaf) (OpenNhds.map α.base x).op

Tactic:
simp

Goal state after:
Module: Mathlib.Geometry.RingedSpace.Stalks

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
x : ↑↑X
U✝ : Opens ↑↑Y
hxU✝ : (ConcreteCategory.hom α.base) x ∈ U✝
⊢ Y.presheaf.germ U✝ ((ConcreteCategory.hom α.base) x) hxU✝ ≫ Hom.stalkMap α x ≫ eqToHom ⋯ =
    Y.presheaf.germ U✝ ((ConcreteCategory.hom α.base) x) hxU✝ ≫ eqToHom ⋯ ≫ Hom.stalkMap α x

Tactic:
simp

Goal state after:
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits

Goal state before:
pp: J : Type u'
inst✝¹ : Category.{v', u'} J
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ PresheafedSpace C
j : J
U : (Opens ↑↑(F.obj j))ᵒᵖ
⊢ 𝟙 ↑(F.obj j) = (F.map (𝟙 j)).base

Tactic:
simp

Goal state after:
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits

Goal state before:
pp: J : Type u'
inst✝² : Category.{v', u'} J
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ PresheafedSpace C
inst✝ : HasColimit F
U : Opens ↑↑(colimit F)
i j k : Jᵒᵖ
f : i ⟶ j
g : j ⟶ k
⊢ (F.map (f ≫ g).unop).c.app (op ((Opens.map (colimit.ι F (unop i)).base).obj U)) ≫
      (F.obj (unop k)).presheaf.map (eqToHom ⋯) =
    (F.map f.unop).c.app (op ((Opens.map (colimit.ι F (unop i)).base).obj U)) ≫
      (F.map g.unop).c.app
          ((Opens.map (F.map f.unop).base).op.obj (op ((Opens.map (colimit.ι F (unop i)).base).obj U))) ≫
        ((pushforward C (F.map g.unop).base).obj (F.obj (unop k)).presheaf).map (eqToHom ⋯) ≫
          (F.obj (unop k)).presheaf.map (eqToHom ⋯)

Tactic:
simp

Goal state after:
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits

Goal state before:
pp: J : Type u'
inst✝² : Category.{v', u'} J
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimitsOfShape J TopCat
F : J ⥤ PresheafedSpace C
j₁ j₂ j₃ : J
f : j₁ ⟶ j₂
g : j₂ ⟶ j₃
U : (Opens ↑(colimit (F ⋙ forget C)))ᵒᵖ
this :
  op ((Opens.map (F.map g).base).obj ((Opens.map (colimit.ι (F ⋙ forget C) j₃)).obj (unop U))) =
    op ((Opens.map (colimit.ι (F ⋙ forget C) j₂)).obj (unop U))
⊢ (F.map g).c.app (op ((Opens.map (colimit.ι (F ⋙ forget C) j₃)).obj (unop U))) ≫
      (F.map f).c.app (op ((Opens.map (F.map g).base).obj ((Opens.map (colimit.ι (F ⋙ forget C) j₃)).obj (unop U)))) ≫
        (F.obj j₁).presheaf.map (eqToHom ⋯) =
    (F.map g).c.app (op ((Opens.map (colimit.ι (F ⋙ forget C) j₃)).obj (unop U))) ≫
      (F.map f).c.app (op ((Opens.map (F.map g).base).obj ((Opens.map (colimit.ι (F ⋙ forget C) j₃)).obj (unop U)))) ≫
        (F.obj j₁).presheaf.map ((Opens.map (F.map f).base).map (eqToHom ⋯)).op ≫ (F.obj j₁).presheaf.map (eqToHom ⋯)

Tactic:
simp [NatTrans.congr (α := (F.map f).c) this]

Goal state after:
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : PresheafedSpace C
α : X ⟶ Y
U : (Opens ↑↑Y)ᵒᵖ
⊢ α.c.app U = α.c.app U ≫ X.presheaf.map (eqToHom ⋯)

Tactic:
simp

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

Tactic:
simp

Goal state after: