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

Goal state before:
pp: S₁ : Type u_1
S₂ : Type u_2
S₃ : Type u_3
inst✝³ : Shelf S₁
inst✝² : Shelf S₂
inst✝¹ : Shelf S₃
S : Type u_4
inst✝ : Shelf S
⊢ ∀ {x y : S}, x ◃ y = x ◃ y

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: S₁ : Type u_1
S₂ : Type u_2
S₃ : Type u_3
inst✝² : Shelf S₁
inst✝¹ : Shelf S₂
inst✝ : Shelf S₃
g : S₂ →◃ S₃
f : S₁ →◃ S₂
⊢ ∀ {x y : S₁}, (g.toFun ∘ f.toFun) (x ◃ y) = (g.toFun ∘ f.toFun) x ◃ (g.toFun ∘ f.toFun) y

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: Q : Type u_1
inst✝¹ : Quandle Q
G : Type u_2
inst✝ : Group G
⊢ ∀ {x : Conj G}, (MulAut.conj x) x = x

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: Q : Type u_1
inst✝² : Quandle Q
G : Type u_2
H : Type u_3
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
⊢ ∀ {x y : Conj G}, f (x ◃ y) = f x ◃ f y

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
B : Basis A c₁ c₂ c₃
y : ℍ[R,c₁,c₂,c₃]
⊢ B.i ∈ {B.i, B.j, B.k}

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
B : Basis A c₁ c₂ c₃
y : ℍ[R,c₁,c₂,c₃]
⊢ B.j ∈ {B.i, B.j, B.k}

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
B : Basis A c₁ c₂ c₃
y : ℍ[R,c₁,c₂,c₃]
⊢ B.k ∈ {B.i, B.j, B.k}

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
inst₁ inst₂ : AddGroupWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
⊢ inst₁ = inst₂

Tactic:
have : inst₁.toAddMonoidWithOne = inst₂.toAddMonoidWithOne :=
    AddMonoidWithOne.ext h_add h_one
  have : inst₁.toNatCast = inst₂.toNatCast := congrArg (·.toNatCast) this
  have h_group : inst₁.toAddGroup = inst₂.toAddGroup := by ext : 1; exact h_add
  -- Extract equality of necessary substructures from h_group
  injection h_group with h_group; injection h_group
  have : inst₁.toIntCast.intCast = inst₂.toIntCast.intCast := by
    funext n; cases n with
    | ofNat n => rewrite [Int.ofNat_eq_natCast, inst₁.intCast_ofNat, inst₂.intCast_ofNat]; congr
    | negSucc n => rewrite [inst₁.intCast_negSucc, inst₂.intCast_negSucc]; congr
  rcases inst₁ with @⟨⟨⟩⟩; rcases inst₂ with @⟨⟨⟩⟩
  congr

Goal state after:
Module: Mathlib.Algebra.Ring.IsFormallyReal

Goal state before:
pp: R : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : IsFormallyReal R
s₁ s₂ : R
hs₁ : IsSumSq s₁
hs₂ : IsSumSq s₂
h : s₁ + s₂ = 0
h₁ : s₁ ≠ 0
h₂ : s₂ ≠ 0
⊢ False

Tactic:
← isSumNonzeroSq_iff_isSumSq h₁

Goal state after:
R : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : IsFormallyReal R
s₁ s₂ : R
hs₁ : IsSumNonzeroSq s₁
hs₂ : IsSumSq s₂
h : s₁ + s₂ = 0
h₁ : s₁ ≠ 0
h₂ : s₂ ≠ 0
⊢ False
Module: Mathlib.Algebra.Ring.IsFormallyReal

Goal state before:
pp: R : Type u_1
inst✝¹ : NonUnitalNonAssocRing R
inst✝ : IsFormallyReal R
s : R
h₁ : IsSumSq s
h₂ : IsSumSq (-s)
⊢ s + -s = 0

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Ring.Semireal.Defs

Goal state before:
pp: R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : IsSemireal R
n : ℕ
hn : 1 + ↑n = 0
⊢ IsSumSq ↑n

Tactic:
by simp

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

Goal state before:
pp: k : Type u_1
G : Type u_2
H : Type u_3
M : Type u_4
α : Type u_5
inst✝ : AddCommMonoid M
a a' : α
b : M
f : SkewMonoidAlgebra M α
⊢ { coeff := Finsupp.erase a (coeff 0) } = 0

Tactic:
by simp

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

Goal state before:
pp: k : Type u_1
G : Type u_2
H : Type u_3
M : Type u_4
α : Type u_5
inst✝ : AddCommMonoid M
a a' : α
b : M
f : SkewMonoidAlgebra M α
⊢ ∀ (x y : SkewMonoidAlgebra M α),
    { coeff := Finsupp.erase a (x + y).coeff } =
      { coeff := Finsupp.erase a x.coeff } + { coeff := Finsupp.erase a y.coeff }

Tactic:
by simp

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

Goal state before:
pp: R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : StarRing R
inst✝² : StarOrderedRing R
inst✝¹ : Algebra ℝ R
inst✝ : IsOrderedModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
P : R := 2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁
idem : P * P = 4 * P
idem' : P = (1 / 4) • (P * P)
sa : star P = P
⊢ 0 ≤ 1 / 4

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : SkewPolynomial R
⊢ p.support.card = 0 ↔ p = 0

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
n : ℕ
inst✝ : Semiring R
p : SkewPolynomial R
⊢ n ∉ p.support ↔ p.coeff n = 0

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: R : Type uR
inst✝⁶ : Semiring R
S : Type uS
inst✝⁵ : CommSemiring S
T : Type uT
A : Type uA
inst✝⁴ : Semiring A
inst✝³ : Algebra S A
r : R → R → Prop
inst✝² : Semiring T
B : Type u₄
inst✝¹ : Semiring B
inst✝ : Algebra S B
f : A ≃ₐ[S] B
rel : A → A → Prop
⊢ ((liftAlgHom S) ⟨(mkAlgHom S rel).comp ↑f.symm, ⋯⟩).comp ((liftAlgHom S) ⟨(mkAlgHom S (rel on ⇑f.symm)).comp ↑f, ⋯⟩) =
    AlgHom.id S (RingQuot rel)

Tactic:
ext a; simp

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: R : Type uR
inst✝⁶ : Semiring R
S : Type uS
inst✝⁵ : CommSemiring S
T : Type uT
A : Type uA
inst✝⁴ : Semiring A
inst✝³ : Algebra S A
r : R → R → Prop
inst✝² : Semiring T
B : Type u₄
inst✝¹ : Semiring B
inst✝ : Algebra S B
f : A ≃+* B
rel : A → A → Prop
n : ℕ
⊢ f ((algebraMap ℕ A) n) = (algebraMap ℕ B) n

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
p : SkewPolynomial R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
⊢ (p.sum fun a₂ b₂ ↦ (monomial (1 + a₂)) (0 * (⇑φ)^[1] b₂)) = 0

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
p : SkewPolynomial R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
⊢ ∀ (a : ℕ), (((monomial 1) 1).sum fun a₂ b₂ ↦ (monomial (a + a₂)) (0 * (⇑φ)^[a] b₂)) = 0

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
p : SkewPolynomial R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
⊢ ∀ (a : ℕ) (b₁ b₂ : R),
    (((monomial 1) 1).sum fun a₂ b₂_1 ↦ (monomial (a + a₂)) ((b₁ + b₂) * (⇑φ)^[a] b₂_1)) =
      (((monomial 1) 1).sum fun a₂ b₂ ↦ (monomial (a + a₂)) (b₁ * (⇑φ)^[a] b₂)) +
        ((monomial 1) 1).sum fun a₂ b₂_1 ↦ (monomial (a + a₂)) (b₂ * (⇑φ)^[a] b₂_1)

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : StarRing α
f : ↥(Subsemiring.center (CentroidHom α))
g : CentroidHom α
a : α
⊢ star ((star g * ↑f) (star a)) = star ((↑f * star g) (star a))

Tactic:
by rw [f.property.comm]

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

Goal state before:
pp: case refine_4
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
x : FreeAlgebra R X
y : FreeAlgebra R X →ₐ[R] (FreeAlgebra R X)ᵐᵒᵖ := (lift R) (MulOpposite.op ∘ ι R)
⊢ ∀ (a b : FreeAlgebra R X),
    MulOpposite.unop (y (MulOpposite.unop (y a))) = a →
      MulOpposite.unop (y (MulOpposite.unop (y b))) = b → MulOpposite.unop (y (MulOpposite.unop (y (a + b)))) = a + b

Tactic:
intros
      simp only [*, map_add, MulOpposite.unop_add]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
n : ℕ
ih : ∀ {p : SkewPolynomial R}, X ^ n * p = (p.sum fun a b ↦ (monomial a) ((⇑φ)^[n] b)) * X ^ n
p : SkewPolynomial R
⊢ ∀ (a : ℕ), (monomial a) ((⇑φ)^[n] 0) = 0

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
n : ℕ
ih : ∀ {p : SkewPolynomial R}, X ^ n * p = (p.sum fun a b ↦ (monomial a) ((⇑φ)^[n] b)) * X ^ n
p : SkewPolynomial R
⊢ ∀ (a : ℕ) (b₁ b₂ : R), (monomial a) ((⇑φ)^[n] (b₁ + b₂)) = (monomial a) ((⇑φ)^[n] b₁) + (monomial a) ((⇑φ)^[n] b₂)

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ ¬X.coeff 1 = coeff 0 1

Tactic:
by simp

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝¹ : One G
inst✝ : AddMonoidWithOne k
⊢ (coeff 1) 1 = 1

Tactic:
by simp

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

Goal state before:
pp: S : Type u_1
R : Type u_2
inst✝⁴ : Semiring R
inst✝³ : StarMul R
inst✝² : SMul S R
inst✝¹ : IsScalarTower S R R
inst✝ : SMulCommClass S R R
u : ↥(unitary R)
x : R
⊢ ((conjStarAlgAut S R) (star u)) x = star ↑u * x * ↑u

Tactic:
by simp

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

Goal state before:
pp: S : Type u_1
R : Type u_2
inst✝⁴ : Semiring R
inst✝³ : StarMul R
inst✝² : SMul S R
inst✝¹ : IsScalarTower S R R
inst✝ : SMulCommClass S R R
u₁ u₂ : ↥(unitary R)
x : R
⊢ ((conjStarAlgAut S R) (u₁ * u₂)) x = ((conjStarAlgAut S R) u₁) (((conjStarAlgAut S R) u₂) x)

Tactic:
by simp

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

Goal state before:
pp: k : Type u_1
G : Type u_2
S : Type u_3
S₁ : Type u_4
S₂ : Type u_5
inst✝² : Semiring S
inst✝¹ : AddCommMonoid k
inst✝ : Module S k
⊢ ∀ (c : S) (x : SkewMonoidAlgebra k G), coeffAddEquiv (c • x) = c • coeffAddEquiv x

Tactic:
by simp

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

Goal state before:
pp: R : Type u
inst✝ : LinearOrder R
x y : Tropical R
⊢ x + y = x ↔ x ≤ y

Tactic:
rw [trop_add_def, trop_eq_iff_eq_untrop, ← untrop_le_iff, min_eq_left_iff]

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 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
⊢ (f * g).coeff x = ∑ p ∈ s, f.coeff p.1 * p.1 • g.coeff p.2

Tactic:
calc
    (f * g).coeff x = ∑ a₁ ∈ f.support, ∑ a₂ ∈ g.support, F (a₁, a₂) := coeff_mul f g x
    _ = ∑ p ∈ f.support ×ˢ g.support, F p := by rw [Finset.sum_product]
    _ = ∑ p ∈ (f.support ×ˢ g.support).filter fun p : G × G ↦ p.1 * p.2 = x,
      f.coeff p.1 * p.1 • g.coeff p.2 := (Finset.sum_filter _ _).symm
    _ = ∑ p ∈ s.filter fun p : G × G ↦ p.1 ∈ f.support ∧ p.2 ∈ g.support,
      f.coeff p.1 * p.1 • g.coeff p.2 :=
      (Finset.sum_congr (by ext; simp [Finset.mem_filter, Finset.mem_product, hs, and_comm])
        fun _ _ ↦ rfl)
    _ = ∑ p ∈ s, f.coeff p.1 * p.1 • g.coeff p.2 :=
      Finset.sum_subset (Finset.filter_subset _ _) fun p hps hp ↦ by
        simp only [Finset.mem_filter, mem_support_iff, not_and, Classical.not_not] at hp ⊢
        by_cases h1 : f.coeff p.1 = 0 <;> simp_all

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

Goal state before:
pp: R : Type u
inst✝ : LinearOrder R
x y z : Tropical R
⊢ x + y = z ↔ x = z ∧ x ≤ y ∨ y = z ∧ y ≤ x

Tactic:
by
  rw [trop_add_def, trop_eq_iff_eq_untrop]
  simp [min_eq_iff]

Goal state after:
Module: Mathlib.Algebra.Symmetrized

Goal state before:
pp: α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
a b c : αˢʸᵐ
⊢ sym (⅟2 * (unsym a * (unsym b + unsym c) + (unsym b + unsym c) * unsym a)) =
    sym (⅟2 * (unsym a * unsym b + unsym b * unsym a + (unsym a * unsym c + unsym c * unsym a)))

Tactic:
add_mul

Goal state after:
α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
a b c : αˢʸᵐ
⊢ sym (⅟2 * (unsym a * (unsym b + unsym c) + (unsym b * unsym a + unsym c * unsym a))) =
    sym (⅟2 * (unsym a * unsym b + unsym b * unsym a + (unsym a * unsym c + unsym c * unsym a)))
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
this : ({p | p.1 * p.2 = x} ∩ Function.support fun p ↦ f.coeff p.1 * p.1 • g.coeff p.2).Finite
⊢ (f * g).coeff x =
    ∑ᶠ (i : G × G) (_ : i ∈ {p | p.1 * p.2 = x} ∩ Function.support fun p ↦ f.coeff p.1 * p.1 • g.coeff p.2),
      f.coeff i.1 * i.1 • g.coeff i.2

Tactic:
finsum_mem_eq_finite_toFinset_sum _ this

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
this : ({p | p.1 * p.2 = x} ∩ Function.support fun p ↦ f.coeff p.1 * p.1 • g.coeff p.2).Finite
⊢ (f * g).coeff x = ∑ i ∈ this.toFinset, f.coeff i.1 * i.1 • g.coeff i.2
Module: Mathlib.Algebra.Tropical.Basic

Goal state before:
pp: R : Type u
inst✝ : AddMonoid R
x✝ : Tropical R
⊢ untrop (x✝ ^ 0) = untrop 1

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Symmetrized

Goal state before:
pp: α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
a b c : αˢʸᵐ
⊢ sym (⅟2 * ((unsym a + unsym b) * unsym c + unsym c * (unsym a + unsym b))) =
    sym (⅟2 * (unsym a * unsym c + unsym c * unsym a + (unsym b * unsym c + unsym c * unsym b)))

Tactic:
add_mul

Goal state after:
α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
a b c : αˢʸᵐ
⊢ sym (⅟2 * (unsym a * unsym c + unsym b * unsym c + unsym c * (unsym a + unsym b))) =
    sym (⅟2 * (unsym a * unsym c + unsym c * unsym a + (unsym b * unsym c + unsym c * unsym b)))
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), a * x = z ↔ a = y
a₁ : G
b₁ : k
⊢ (if a₁ * x = z then b₁ * a₁ • 0 else 0) = 0

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrder R
inst✝ : Fintype S
f : S → WithTop R
⊢ trop (sInf (Set.range fun i ↦ f i)) = ∑ i, trop (f i)

Tactic:
← Set.image_univ,

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrder R
inst✝ : Fintype S
f : S → WithTop R
⊢ trop (sInf ((fun i ↦ f i) '' Set.univ)) = ∑ i, trop (f i)
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), a * x = z ↔ a = y
⊢ (f * single x r).coeff z = f.coeff y * y • r

Tactic:
have A : ∀ a₁ b₁, ((single x r).sum fun a₂ b₂ ↦ ite (a₁ * a₂ = z) (b₁ * a₁ • b₂) 0) =
      ite (a₁ * x = z) (b₁ * a₁ • r) 0 :=
    fun a₁ b₁ ↦ sum_single_index <| by simp
  calc
    (f * (single x r)).coeff z =
        sum f fun a b ↦ if a = y then b * y • r else 0 := by simp [coeff_mul, A, H, sum_ite_eq']
    _ = if y ∈ f.support then f.coeff y * y • r else 0 := (f.support.sum_ite_eq' _ _)
    _ = f.coeff y * y • r := by
      split_ifs with h <;> simp [support] at h <;> simp [h]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrder R
inst✝ : Fintype S
f : S → Tropical (WithTop R)
⊢ untrop (∑ i, f i) = sInf (Set.range fun i ↦ untrop (f i))

Tactic:
← Set.image_univ,

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrder R
inst✝ : Fintype S
f : S → Tropical (WithTop R)
⊢ untrop (∑ i, f i) = sInf ((fun i ↦ untrop (f i)) '' Set.univ)
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:
by 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:
by 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:
by 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:
by 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✝¹ : Monoid G
inst✝ : MulSemiringAction G k
a b : G
⊢ single (a * b) 1 = single a 1 * single b 1

Tactic:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by simp

Goal state after: