mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Localization.Defs

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit (g ↑y)
x y : S
⊢ ↑g.toMonoidWithZeroHom ((toLocalizationMap M S).sec (x + y)).1 =
    ↑g.toMonoidWithZeroHom ↑((toLocalizationMap M S).sec (x + y)).2 * ((toLocalizationMap M S).lift hg) x +
      ↑g.toMonoidWithZeroHom ↑((toLocalizationMap M S).sec (x + y)).2 * ((toLocalizationMap M S).lift hg) y

Tactic:
mul_comm,

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit (g ↑y)
x y : S
⊢ ↑g.toMonoidWithZeroHom ((toLocalizationMap M S).sec (x + y)).1 =
    ((toLocalizationMap M S).lift hg) x * ↑g.toMonoidWithZeroHom ↑((toLocalizationMap M S).sec (x + y)).2 +
      ↑g.toMonoidWithZeroHom ↑((toLocalizationMap M S).sec (x + y)).2 * ((toLocalizationMap M S).lift hg) y
Module: Mathlib.RingTheory.Localization.Defs

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit (g ↑y)
x y : S
⊢ g ↑((toLocalizationMap M S).sec x).2 *
        (↑g.toMonoidWithZeroHom ↑((toLocalizationMap M S).sec (x + y)).2 * ((toLocalizationMap M S).lift hg) y) +
      g ((toLocalizationMap M S).sec x).1 * ↑g.toMonoidWithZeroHom ↑((toLocalizationMap M S).sec (x + y)).2 =
    g ↑((toLocalizationMap M S).sec x).2 * ↑g.toMonoidWithZeroHom ((toLocalizationMap M S).sec (x + y)).1

Tactic:
mul_comm,

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit (g ↑y)
x y : S
⊢ ↑g.toMonoidWithZeroHom ↑((toLocalizationMap M S).sec (x + y)).2 * ((toLocalizationMap M S).lift hg) y *
        g ↑((toLocalizationMap M S).sec x).2 +
      g ((toLocalizationMap M S).sec x).1 * ↑g.toMonoidWithZeroHom ↑((toLocalizationMap M S).sec (x + y)).2 =
    g ↑((toLocalizationMap M S).sec x).2 * ↑g.toMonoidWithZeroHom ((toLocalizationMap M S).sec (x + y)).1
Module: Mathlib.RingTheory.Localization.Defs

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit (g ↑y)
x y : S
⊢ ↑g.toMonoidWithZeroHom ↑((toLocalizationMap M S).sec (x + y)).2 *
        (((toLocalizationMap M S).lift hg) y * g ↑((toLocalizationMap M S).sec x).2) +
      g ((toLocalizationMap M S).sec x).1 * ↑g.toMonoidWithZeroHom ↑((toLocalizationMap M S).sec (x + y)).2 =
    g ↑((toLocalizationMap M S).sec x).2 * ↑g.toMonoidWithZeroHom ((toLocalizationMap M S).sec (x + y)).1

Tactic:
mul_comm,

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit (g ↑y)
x y : S
⊢ ((toLocalizationMap M S).lift hg) y * g ↑((toLocalizationMap M S).sec x).2 *
        ↑g.toMonoidWithZeroHom ↑((toLocalizationMap M S).sec (x + y)).2 +
      g ((toLocalizationMap M S).sec x).1 * ↑g.toMonoidWithZeroHom ↑((toLocalizationMap M S).sec (x + y)).2 =
    g ↑((toLocalizationMap M S).sec x).2 * ↑g.toMonoidWithZeroHom ((toLocalizationMap M S).sec (x + y)).1
Module: Mathlib.RingTheory.Localization.Defs

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
T : Type u_4
inst✝ : CommSemiring T
f : S →+* T
⊢ Injective ⇑f ↔ ∀ (x y : R), (algebraMap R S) x = (algebraMap R S) y ↔ f ((algebraMap R S) x) = f ((algebraMap R S) y)

Tactic:
rw [← IsLocalization.lift_of_comp (M := M) f, IsLocalization.lift_injective_iff]

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
T : Type u_4
inst✝ : CommSemiring T
f : S →+* T
⊢ (∀ (x y : R), (algebraMap R S) x = (algebraMap R S) y ↔ (f.comp (algebraMap R S)) x = (f.comp (algebraMap R S)) y) ↔
    ∀ (x y : R), (algebraMap R S) x = (algebraMap R S) y ↔ (lift ⋯) ((algebraMap R S) x) = (lift ⋯) ((algebraMap R S) y)
Module: Mathlib.RingTheory.Localization.Basic

Goal state before:
pp: case refine_2
R : Type u_1
inst✝⁴ : CommSemiring R
M N : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit (g ↑y)
H : M ≤ IsUnit.submonoid R
⊢ Surjective ⇑(Algebra.ofId R S)

Tactic:
intro y
    obtain ⟨⟨x, s⟩, eq⟩ := IsLocalization.surj M y
    obtain ⟨u, hu⟩ := H s.prop
    use x * u.inv
    dsimp [Algebra.ofId, RingHom.toFun_eq_coe, AlgHom.coe_mks]
    rw [map_mul, ← eq, ← hu, mul_assoc, ← map_mul]
    simp

Goal state after:
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: A : Type u_4
inst✝⁴ : CommRing A
K : Type u_5
inst✝³ : CommRing K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDomain A
x : K
hx : x ≠ 0
⊢ x * mk' K ↑(sec A⁰ x).2 ⟨(sec A⁰ x).1, ⋯⟩ * (algebraMap A K) ↑⟨(sec A⁰ x).1, ⋯⟩ =
    1 * (algebraMap A K) ↑⟨(sec A⁰ x).1, ⋯⟩

Tactic:
one_mul,

Goal state after:
A : Type u_4
inst✝⁴ : CommRing A
K : Type u_5
inst✝³ : CommRing K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDomain A
x : K
hx : x ≠ 0
⊢ x * mk' K ↑(sec A⁰ x).2 ⟨(sec A⁰ x).1, ⋯⟩ * (algebraMap A K) ↑⟨(sec A⁰ x).1, ⋯⟩ = (algebraMap A K) ↑⟨(sec A⁰ x).1, ⋯⟩
Module: Mathlib.RingTheory.Adjoin.Basic

Goal state before:
pp: case h
R : Type uR
A : Type uA
B : Type uB
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : CommSemiring B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
r : A
s : Set B
B' : Subalgebra R B
hs : r • s ⊆ ↑B'
hr : (algebraMap A B) r ∈ B'
l : ↑↑(Submonoid.closure s) →₀ R
n₁ : ↥(Submonoid.closure s) → ℕ
n₂ : ∀ (x : ↥(Submonoid.closure s)), r ^ n₁ x • ↑x ∈ Submonoid.closure (r • s)
n : ℕ
hn : n ≥ l.support.sup n₁
a : ↑↑(Submonoid.closure s)
ha : a ∈ l.support
this : n ≥ n₁ a
⊢ r ^ (n - n₁ a) • (r ^ n₁ a * (algebraMap R A) (l a)) • ↑a ∈ Subalgebra.toSubmodule B'

Tactic:
mul_comm,

Goal state after:
case h
R : Type uR
A : Type uA
B : Type uB
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : CommSemiring B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
r : A
s : Set B
B' : Subalgebra R B
hs : r • s ⊆ ↑B'
hr : (algebraMap A B) r ∈ B'
l : ↑↑(Submonoid.closure s) →₀ R
n₁ : ↥(Submonoid.closure s) → ℕ
n₂ : ∀ (x : ↥(Submonoid.closure s)), r ^ n₁ x • ↑x ∈ Submonoid.closure (r • s)
n : ℕ
hn : n ≥ l.support.sup n₁
a : ↑↑(Submonoid.closure s)
ha : a ∈ l.support
this : n ≥ n₁ a
⊢ r ^ (n - n₁ a) • ((algebraMap R A) (l a) * r ^ n₁ a) • ↑a ∈ Subalgebra.toSubmodule B'
Module: Mathlib.RingTheory.Localization.Basic

Goal state before:
pp: case e'_3
R : Type u_1
inst✝¹³ : CommSemiring R
S₁ : Type u_4
S₂ : Type u_5
T : Type u_6
inst✝¹² : CommSemiring S₁
inst✝¹¹ : CommSemiring S₂
inst✝¹⁰ : CommSemiring T
inst✝⁹ : Algebra R S₁
inst✝⁸ : Algebra R S₂
inst✝⁷ : Algebra R T
inst✝⁶ : Algebra S₁ T
inst✝⁵ : Algebra S₂ T
inst✝⁴ : IsScalarTower R S₁ T
inst✝³ : IsScalarTower R S₂ T
M₁ M₂ : Submonoid R
inst✝² : IsLocalization M₁ S₁
inst✝¹ : IsLocalization M₂ S₂
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S₂ M₁) T
a : T
y : S₂
m : R
hm : m ∈ ↑M₁
hy : a * (algebraMap S₁ T) ((algebraMap R S₁) m) = (algebraMap S₂ T) (y, ⟨(algebraMap R S₂) m, ⋯⟩).1
z n : R
hn : n ∈ M₂
hz : y * (algebraMap R S₂) ↑(z, ⟨n, hn⟩).2 = (algebraMap R S₂) (z, ⟨n, hn⟩).1
hunit : IsUnit ((algebraMap R S₁) m)
⊢ a * (algebraMap S₁ T) ((algebraMap R S₁) m) * (algebraMap S₂ T) ((algebraMap R S₂) ↑(z, ⟨n, hn⟩).2) *
      (algebraMap S₁ T) ↑hunit.unit⁻¹ =
    a * (algebraMap S₂ T) ((algebraMap R S₂) n) * (algebraMap S₁ T) ((algebraMap R S₁) m * ↑hunit.unit⁻¹)

pp: case h.convert_2
R : Type u_1
inst✝¹³ : CommSemiring R
S₁ : Type u_4
S₂ : Type u_5
T : Type u_6
inst✝¹² : CommSemiring S₁
inst✝¹¹ : CommSemiring S₂
inst✝¹⁰ : CommSemiring T
inst✝⁹ : Algebra R S₁
inst✝⁸ : Algebra R S₂
inst✝⁷ : Algebra R T
inst✝⁶ : Algebra S₁ T
inst✝⁵ : Algebra S₂ T
inst✝⁴ : IsScalarTower R S₁ T
inst✝³ : IsScalarTower R S₂ T
M₁ M₂ : Submonoid R
inst✝² : IsLocalization M₁ S₁
inst✝¹ : IsLocalization M₂ S₂
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S₂ M₁) T
a : T
y : S₂
m : R
hm : m ∈ ↑M₁
hy : a * (algebraMap S₁ T) ((algebraMap R S₁) m) = (algebraMap S₂ T) (y, ⟨(algebraMap R S₂) m, ⋯⟩).1
z n : R
hn : n ∈ M₂
hz : y * (algebraMap R S₂) ↑(z, ⟨n, hn⟩).2 = (algebraMap R S₂) (z, ⟨n, hn⟩).1
hunit : IsUnit ((algebraMap R S₁) m)
⊢ a * (algebraMap S₂ T) ((algebraMap R S₂) n) =
    a * (algebraMap S₂ T) ((algebraMap R S₂) n) * (algebraMap S₁ T) ((algebraMap R S₁) m * ↑hunit.unit⁻¹)

Tactic:
· rw [map_mul]
      ring

Goal state after:
case h.convert_2
R : Type u_1
inst✝¹³ : CommSemiring R
S₁ : Type u_4
S₂ : Type u_5
T : Type u_6
inst✝¹² : CommSemiring S₁
inst✝¹¹ : CommSemiring S₂
inst✝¹⁰ : CommSemiring T
inst✝⁹ : Algebra R S₁
inst✝⁸ : Algebra R S₂
inst✝⁷ : Algebra R T
inst✝⁶ : Algebra S₁ T
inst✝⁵ : Algebra S₂ T
inst✝⁴ : IsScalarTower R S₁ T
inst✝³ : IsScalarTower R S₂ T
M₁ M₂ : Submonoid R
inst✝² : IsLocalization M₁ S₁
inst✝¹ : IsLocalization M₂ S₂
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S₂ M₁) T
a : T
y : S₂
m : R
hm : m ∈ ↑M₁
hy : a * (algebraMap S₁ T) ((algebraMap R S₁) m) = (algebraMap S₂ T) (y, ⟨(algebraMap R S₂) m, ⋯⟩).1
z n : R
hn : n ∈ M₂
hz : y * (algebraMap R S₂) ↑(z, ⟨n, hn⟩).2 = (algebraMap R S₂) (z, ⟨n, hn⟩).1
hunit : IsUnit ((algebraMap R S₁) m)
⊢ a * (algebraMap S₂ T) ((algebraMap R S₂) n) =
    a * (algebraMap S₂ T) ((algebraMap R S₂) n) * (algebraMap S₁ T) ((algebraMap R S₁) m * ↑hunit.unit⁻¹)
Module: Mathlib.RingTheory.Localization.Basic

Goal state before:
pp: R : Type u_1
inst✝¹¹ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Algebra R S
Rₘ : Type u_4
Sₘ : Type u_5
inst✝⁸ : CommSemiring Rₘ
inst✝⁷ : CommSemiring Sₘ
inst✝⁶ : Algebra R Rₘ
inst✝⁵ : IsLocalization M Rₘ
inst✝⁴ : Algebra S Sₘ
i : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝³ : Algebra Rₘ Sₘ
inst✝² : Algebra R Sₘ
inst✝¹ : IsScalarTower R Rₘ Sₘ
inst✝ : IsScalarTower R S Sₘ
x : R
y : ↥M
⊢ (algebraMap Rₘ Sₘ) (mk' Rₘ x y * (algebraMap R Rₘ) ↑y) = (algebraMap Rₘ Sₘ) ((algebraMap R Rₘ) x)

Tactic:
mul_comm,

Goal state after:
R : Type u_1
inst✝¹¹ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Algebra R S
Rₘ : Type u_4
Sₘ : Type u_5
inst✝⁸ : CommSemiring Rₘ
inst✝⁷ : CommSemiring Sₘ
inst✝⁶ : Algebra R Rₘ
inst✝⁵ : IsLocalization M Rₘ
inst✝⁴ : Algebra S Sₘ
i : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝³ : Algebra Rₘ Sₘ
inst✝² : Algebra R Sₘ
inst✝¹ : IsScalarTower R Rₘ Sₘ
inst✝ : IsScalarTower R S Sₘ
x : R
y : ↥M
⊢ (algebraMap Rₘ Sₘ) ((algebraMap R Rₘ) ↑y * mk' Rₘ x y) = (algebraMap Rₘ Sₘ) ((algebraMap R Rₘ) x)
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalNonAssocSemiring β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
nsmul : SMul ℕ α := Equiv.smul ℕ e
⊢ NonUnitalNonAssocSemiring α

Tactic:
apply e.injective.nonUnitalNonAssocSemiring _ <;> intros

Goal state after:
case zero
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalNonAssocSemiring β
zero : Zero α := ⋯
add : Add α := ⋯
mul : Mul α := ⋯
nsmul : SMul ℕ α := ⋯
⊢ e 0 = 0

case add
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalNonAssocSemiring β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
nsmul : SMul ℕ α := Equiv.smul ℕ e
x✝ y✝ : α
⊢ e (x✝ + y✝) = e x✝ + e y✝

case mul
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalNonAssocSemiring β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
nsmul : SMul ℕ α := Equiv.smul ℕ e
x✝ y✝ : α
⊢ e (x✝ * y✝) = e x✝ * e y✝

case nsmul
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalNonAssocSemiring β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
nsmul : SMul ℕ α := Equiv.smul ℕ e
n✝ : ℕ
x✝ : α
⊢ e (n✝ • x✝) = n✝ • e x✝
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: case add
R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst✝¹² : CommSemiring R
inst✝¹¹ : NonUnitalNonAssocSemiring A
inst✝¹⁰ : Module R A
inst✝⁹ : SMulCommClass R A A
inst✝⁸ : IsScalarTower R A A
inst✝⁷ : NonUnitalNonAssocSemiring B
inst✝⁶ : Module R B
inst✝⁵ : SMulCommClass R B B
inst✝⁴ : IsScalarTower R B B
inst✝³ : Monoid S
inst✝² : DistribMulAction S A
inst✝¹ : IsScalarTower S A A
inst✝ : SMulCommClass R S A
r : S
x✝ x y : A ⊗[R] B
hx : r • x✝ * x = r • (x✝ * x)
hy : r • x✝ * y = r • (x✝ * y)
⊢ r • x✝ * (x + y) = r • (x✝ * (x + y))

Tactic:
simp [smul_add, mul_add _, *]

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: case add
R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst✝¹² : CommSemiring R
inst✝¹¹ : NonUnitalNonAssocSemiring A
inst✝¹⁰ : Module R A
inst✝⁹ : SMulCommClass R A A
inst✝⁸ : IsScalarTower R A A
inst✝⁷ : NonUnitalNonAssocSemiring B
inst✝⁶ : Module R B
inst✝⁵ : SMulCommClass R B B
inst✝⁴ : IsScalarTower R B B
inst✝³ : Monoid S
inst✝² : DistribMulAction S A
inst✝¹ : SMulCommClass S A A
inst✝ : SMulCommClass R S A
r : S
x✝ x y : A ⊗[R] B
hx : r • (x✝ * x) = x✝ * r • x
hy : r • (x✝ * y) = x✝ * r • y
⊢ r • (x✝ * (x + y)) = x✝ * r • (x + y)

Tactic:
simp [smul_add, mul_add _, *]

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

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
⊢ ¬IsUnit (0 - a) ↔ ¬IsUnit a

Tactic:
zero_sub,

Goal state after:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
⊢ ¬IsUnit (-a) ↔ ¬IsUnit a
Module: Mathlib.Algebra.Algebra.Spectrum.Basic

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a b : A
r : R
ha : r ∈ resolventSet R a
hb : r ∈ resolventSet R b
⊢ 1 * ↑(IsUnit.unit hb) - ↑(IsUnit.unit ha) * 1 = a - b

Tactic:
one_mul,

Goal state after:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a b : A
r : R
ha : r ∈ resolventSet R a
hb : r ∈ resolventSet R b
⊢ ↑(IsUnit.unit hb) - ↑(IsUnit.unit ha) * 1 = a - b
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: R : Type uR
S : Type uS
A : Type uA
B : Type uB
C : Type uC
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A
inst✝¹⁰ : Algebra R A
inst✝⁹ : Semiring B
inst✝⁸ : Algebra R B
inst✝⁷ : Semiring C
inst✝⁶ : Algebra R C
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S A
inst✝³ : Algebra R S
inst✝² : Algebra S C
inst✝¹ : IsScalarTower R S A
inst✝ : IsScalarTower R S C
f g : A ⊗[R] B →ₐ[S] C
ha : f.comp includeLeft = g.comp includeLeft
hb : (AlgHom.restrictScalars R f).comp includeRight = (AlgHom.restrictScalars R g).comp includeRight
a : A
b : B
this : f ((a * 1) ⊗ₜ[R] (1 * b)) = g ((a * 1) ⊗ₜ[R] (1 * b))
⊢ ((AlgebraTensorModule.curry f.toLinearMap) a) b = ((AlgebraTensorModule.curry g.toLinearMap) a) b

Tactic:
one_mul,

Goal state after:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
C : Type uC
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A
inst✝¹⁰ : Algebra R A
inst✝⁹ : Semiring B
inst✝⁸ : Algebra R B
inst✝⁷ : Semiring C
inst✝⁶ : Algebra R C
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S A
inst✝³ : Algebra R S
inst✝² : Algebra S C
inst✝¹ : IsScalarTower R S A
inst✝ : IsScalarTower R S C
f g : A ⊗[R] B →ₐ[S] C
ha : f.comp includeLeft = g.comp includeLeft
hb : (AlgHom.restrictScalars R f).comp includeRight = (AlgHom.restrictScalars R g).comp includeRight
a : A
b : B
this : f ((a * 1) ⊗ₜ[R] b) = g ((a * 1) ⊗ₜ[R] b)
⊢ ((AlgebraTensorModule.curry f.toLinearMap) a) b = ((AlgebraTensorModule.curry g.toLinearMap) a) b
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
inst✝ : CompatibleSMul R S S S
x✝ : S ⊗[R] S
x y : S
⊢ (x * y) ⊗ₜ[R] 1 = x ⊗ₜ[R] y

Tactic:
mul_comm,

Goal state after:
R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
inst✝ : CompatibleSMul R S S S
x✝ : S ⊗[R] S
x y : S
⊢ (y * x) ⊗ₜ[R] 1 = x ⊗ₜ[R] y
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
x : R
⊢ star x ≤ 0 ↔ x ≤ 0

Tactic:
by
  simpa using star_le_star_iff (x := x) (y := 0)

Goal state after:
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a b : R
hab : a < b
c : R
hc : IsRegular c
⊢ star c * a * c < star c * b * c

Tactic:
(star_left_conjugate_le_conjugate hab.le _).lt_iff_ne,

Goal state after:
R : Type u_1
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a b : R
hab : a < b
c : R
hc : IsRegular c
⊢ star c * a * c ≠ star c * b * c
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
u x : R
hu : IsUnit u
h : 0 ≤ u * x * star u
v : R
hv : v * u = 1
this : 0 ≤ 1 * x * star u * star v
⊢ 0 ≤ x

Tactic:
one_mul,

Goal state after:
R : Type u_1
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
u x : R
hu : IsUnit u
h : 0 ≤ u * x * star u
v : R
hv : v * u = 1
this : 0 ≤ x * star u * star v
⊢ 0 ≤ x
Module: Mathlib.Algebra.Algebra.Subalgebra.Centralizer

Goal state before:
pp: case e'_3.mp
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Set B
inst✝ : Module.Free R A
eq1 :
  comap (↑(Algebra.TensorProduct.comm R A B)) (centralizer R (⇑includeLeft '' S)) =
    comap (↑(Algebra.TensorProduct.comm R A B)) (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R A)).range
x : A ⊗[R] ↥(centralizer R S)
⊢ ∃ x_1,
    (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R A)) x_1 =
      (Algebra.TensorProduct.comm R A B) ((Algebra.TensorProduct.map (AlgHom.id R A) (centralizer R S).val) x)

Tactic:
exact ⟨(Algebra.TensorProduct.comm R _ _) x,
        by rw [Algebra.TensorProduct.comm_comp_map_apply]⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Constructions

Goal state before:
pp: R : Type u
M : Type v
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : StrongRankCondition R
inst✝² : Free R M
m n : Type w
inst✝¹ : Finite m
inst✝ : Finite n
⊢ lift.{max v w, w} #m * lift.{max v w, w} #n * lift.{w, v} (Module.rank R M) =
    lift.{v, w} #m * lift.{v, w} #n * lift.{w, v} (Module.rank R M)

Tactic:
lift_umax.{w, v}

Goal state after:
R : Type u
M : Type v
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : StrongRankCondition R
inst✝² : Free R M
m n : Type w
inst✝¹ : Finite m
inst✝ : Finite n
⊢ lift.{v, w} #m * lift.{v, w} #n * lift.{w, v} (Module.rank R M) =
    lift.{v, w} #m * lift.{v, w} #n * lift.{w, v} (Module.rank R M)
Module: Mathlib.LinearAlgebra.Basis.VectorSpace

Goal state before:
pp: K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
f : V →ₗ[K] V'
hf_inj : f.ker = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndepOn K _root_.id (Set.range ⇑hB)
this : LinearIndepOn K _root_.id (⇑f '' B)
⊢ ∃ g, g ∘ₗ f = id

Tactic:
let C := this.extend (subset_univ _)

Goal state after:
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
f : V →ₗ[K] V'
hf_inj : f.ker = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndepOn K _root_.id (Set.range ⇑hB)
this : LinearIndepOn K _root_.id (⇑f '' B)
C : Set V' := this.extend ⋯
⊢ ∃ g, g ∘ₗ f = id
Module: Mathlib.Algebra.Star.NonUnitalSubalgebra

Goal state before:
pp: F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝¹³ : CommSemiring R
inst✝¹² : StarRing R
inst✝¹¹ : NonUnitalSemiring A
inst✝¹⁰ : StarRing A
inst✝⁹ : Module R A
inst✝⁸ : NonUnitalSemiring B
inst✝⁷ : StarRing B
inst✝⁶ : Module R B
inst✝⁵ : FunLike F A B
inst✝⁴ : NonUnitalAlgHomClass F R A B
inst✝³ : StarHomClass F A B
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
s : Set A
a✝ : A
x✝ : a✝ ∈ (NonUnitalAlgebra.adjoin R (s ∪ star s)).carrier
⊢ star a✝ ∈ (NonUnitalAlgebra.adjoin R (s ∪ star s)).carrier

Tactic:
NonUnitalSubalgebra.mem_carrier,

Goal state after:
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝¹³ : CommSemiring R
inst✝¹² : StarRing R
inst✝¹¹ : NonUnitalSemiring A
inst✝¹⁰ : StarRing A
inst✝⁹ : Module R A
inst✝⁸ : NonUnitalSemiring B
inst✝⁷ : StarRing B
inst✝⁶ : Module R B
inst✝⁵ : FunLike F A B
inst✝⁴ : NonUnitalAlgHomClass F R A B
inst✝³ : StarHomClass F A B
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
s : Set A
a✝ : A
x✝ : a✝ ∈ (NonUnitalAlgebra.adjoin R (s ∪ star s)).carrier
⊢ star a✝ ∈ NonUnitalAlgebra.adjoin R (s ∪ star s)
Module: Mathlib.Algebra.Star.NonUnitalSubalgebra

Goal state before:
pp: F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝¹³ : CommSemiring R
inst✝¹² : StarRing R
inst✝¹¹ : NonUnitalSemiring A
inst✝¹⁰ : StarRing A
inst✝⁹ : Module R A
inst✝⁸ : NonUnitalSemiring B
inst✝⁷ : StarRing B
inst✝⁶ : Module R B
inst✝⁵ : FunLike F A B
inst✝⁴ : NonUnitalAlgHomClass F R A B
inst✝³ : StarHomClass F A B
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
s : Set A
a✝ : A
x✝ : a✝ ∈ (NonUnitalAlgebra.adjoin R (s ∪ star s)).carrier
⊢ star a✝ ∈ NonUnitalAlgebra.adjoin R (s ∪ star s)

Tactic:
← NonUnitalSubalgebra.mem_star_iff,

Goal state after:
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝¹³ : CommSemiring R
inst✝¹² : StarRing R
inst✝¹¹ : NonUnitalSemiring A
inst✝¹⁰ : StarRing A
inst✝⁹ : Module R A
inst✝⁸ : NonUnitalSemiring B
inst✝⁷ : StarRing B
inst✝⁶ : Module R B
inst✝⁵ : FunLike F A B
inst✝⁴ : NonUnitalAlgHomClass F R A B
inst✝³ : StarHomClass F A B
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
s : Set A
a✝ : A
x✝ : a✝ ∈ (NonUnitalAlgebra.adjoin R (s ∪ star s)).carrier
⊢ a✝ ∈ star (NonUnitalAlgebra.adjoin R (s ∪ star s))
Module: Mathlib.LinearAlgebra.Basis.VectorSpace

Goal state before:
pp: K : Type u_6
V : Type u_7
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : V →ₗ[K] K
hf : f ≠ 0
v : ↥f.ker
hv : ↑v ≠ 0
this : LinearIndepOn K _root_.id {v}
b₁ : Basis (↑(this.extend ⋯)) K ↥f.ker := Basis.extend this
w : V
hw : f w = 1
s : Set V := ⇑f.ker.subtype '' Set.range ⇑b₁
hs : span K s = f.ker
⊢ v ∈ Set.range ⇑b₁

Tactic:
simp [b₁, this.subset_extend _ _]

Goal state after: