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
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
a✝ : G × G
⊢ a✝ ∈ {p ∈ f.support ×ˢ g.support | p.1 * p.2 = x} ↔ a✝ ∈ {p ∈ s | p.1 ∈ f.support ∧ p.2 ∈ g.support}

Tactic:
;

Goal state after:
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
a✝ : G × G
⊢ a✝ ∈ {p ∈ f.support ×ˢ g.support | p.1 * p.2 = x} ↔ a✝ ∈ {p ∈ s | p.1 ∈ f.support ∧ p.2 ∈ g.support}
Module: Mathlib.Algebra.TrivSqZeroExt.Ideal

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
r : R
m : M
hr : r = 0
⊢ (0, m) = inr (snd (0, m))

Tactic:
;

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
r : R
m : M
hr : r = 0
⊢ (0, m) = inr (snd (0, m))
Module: Mathlib.Algebra.Tropical.Basic

Goal state before:
pp: R : Type u
inst✝ : LinearOrder R
a b : Tropical R
⊢ (if a ≤ b then untrop a else untrop b) = untrop (if a ≤ b then a else b)

Tactic:
;

Goal state after:
R : Type u
inst✝ : LinearOrder R
a b : Tropical R
⊢ (if a ≤ b then untrop a else untrop b) = untrop (if a ≤ b then a else b)
Module: Mathlib.Algebra.Tropical.Basic

Goal state before:
pp: R : Type u
inst✝ : LinearOrder R
a b : Tropical R
⊢ (if a ≤ b then untrop b else untrop a) = untrop (if a ≤ b then b else a)

Tactic:
;

Goal state after:
R : Type u
inst✝ : LinearOrder R
a b : Tropical R
⊢ (if a ≤ b then untrop b else untrop a) = untrop (if a ≤ b then b else a)
Module: Mathlib.Algebra.Tropical.BigOperators

Goal state before:
pp: case inl
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
f : S → WithTop R
⊢ trop (sInf (f '' ↑∅)) = ∑ i ∈ ∅, trop (f i)

Tactic:
simp only [Set.image_empty, coe_empty, sum_empty, WithTop.sInf_empty, trop_top]

Goal state after:
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
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
⊢ (if z ∈ f.support then r * x • f.coeff z else 0) = r * x • f.coeff z

Tactic:
by split_ifs with h <;> simp [support] at h <;> simp [h]

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

Goal state before:
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
⊢ (t • a.sum fun a b_1 ↦ b.sum fun a_1 b ↦ single (a * a_1) (b_1 * a • b)) = t • (a * b)

Tactic:
;

Goal state after:
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
⊢ (t • a.sum fun a b_1 ↦ b.sum fun a_1 b ↦ single (a * a_1) (b_1 * a • b)) = t • (a * b)
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝⁵ : Monoid G
inst✝⁴ : CommSemiring k
A : Type u_3
inst✝³ : Semiring A
inst✝² : Algebra k A
inst✝¹ : MulSemiringAction G A
inst✝ : SMulCommClass G k A
r : k
a : SkewMonoidAlgebra A G
a✝ : G
⊢ (r • a).coeff a✝ = ((singleOneRingHom.comp (algebraMap k A)) r * a).coeff a✝

Tactic:
;

Goal state after:
k : Type u_1
G : Type u_2
inst✝⁵ : Monoid G
inst✝⁴ : CommSemiring k
A : Type u_3
inst✝³ : Semiring A
inst✝² : Algebra k A
inst✝¹ : MulSemiringAction G A
inst✝ : SMulCommClass G k A
r : k
a : SkewMonoidAlgebra A G
a✝ : G
⊢ (r • a).coeff a✝ = ((singleOneRingHom.comp (algebraMap k A)) r * a).coeff a✝
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:
;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Goal state after:
Γ : 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✝
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✝
Γ : Type u_5
Γ' : Type u_6
inst✝⁸ : PartialOrder Γ
inst✝⁷ : PartialOrder Γ'
R : Type u_7
inst✝⁶ : CommRing R
U : Type u_8
V : Type u_9
W : Type u_10
inst✝⁵ : AddCommGroup U
inst✝⁴ : Module R U
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
A : HVertexOperator Γ R V W
B : HVertexOperator Γ' R U V
⊢ ∀ (m : R) (x : U),
    (of R) (A.compHahnSeries B (m • x)).ofIterate = (RingHom.id R) m • (of R) (A.compHahnSeries B x).ofIterate

Tactic:
intro r

Goal state after:
Γ✝ : 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✝
Γ : Type u_5
Γ' : Type u_6
inst✝⁸ : PartialOrder Γ
inst✝⁷ : PartialOrder Γ'
R : Type u_7
inst✝⁶ : CommRing R
U : Type u_8
V : Type u_9
W : Type u_10
inst✝⁵ : AddCommGroup U
inst✝⁴ : Module R U
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
A : HVertexOperator Γ R V W
B : HVertexOperator Γ' R U V
r : R
⊢ ∀ (x : U), (of R) (A.compHahnSeries B (r • x)).ofIterate = (RingHom.id R) r • (of R) (A.compHahnSeries B x).ofIterate
Module: Mathlib.Geometry.RingedSpace.SheafedSpace

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : SheafedSpace C
α : X ⟶ Y
U : (Opens ↑↑Y.toPresheafedSpace)ᵒᵖ
⊢ (Opens.map α.hom.base).op.obj U = (Opens.map α.hom.base).op.obj U

Tactic:
;

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : SheafedSpace C
α : X ⟶ Y
U : (Opens ↑↑Y.toPresheafedSpace)ᵒᵖ
⊢ (Opens.map α.hom.base).op.obj U = (Opens.map α.hom.base).op.obj U
Module: Mathlib.Geometry.RingedSpace.Stalks

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
x : ↑U
⊢ IsIso (X.restrictStalkIso h x).inv

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
x : ↑U
⊢ IsIso (X.restrictStalkIso h x).inv