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

Goal state before:
pp: R : Type u
inst✝³ : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
A : ι → Submodule R M
inst✝ : DecidableEq M
x : ⨁ (i : ι), ↥(A i)
⊢ (DFinsupp.sum x fun x ↦ ⇑(A x).subtype.toAddMonoidHom) = DFinsupp.sum x fun i x ↦ ↑x

Tactic:
simp only [LinearMap.toAddMonoidHom_coe, Submodule.coe_subtype]

Goal state after:
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
x✝³ x✝² y✝ : A
hx✝ : x✝² ∈ adjoin R s
hy✝ : y✝ ∈ adjoin R s
hpx : x✝² ∈ span R ↑(Subsemigroup.closure s)
hpy : y✝ ∈ span R ↑(Subsemigroup.closure s)
r : R
x y : A
x✝¹ : x ∈ span R ↑(Subsemigroup.closure s)
x✝ : y ∈ span R ↑(Subsemigroup.closure s)
hxy : x * y ∈ span R ↑(Subsemigroup.closure s)
⊢ r • x * y ∈ span R ↑(Subsemigroup.closure s)

Tactic:
simpa [smul_mul_assoc] using smul_mem _ _ hxy

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : Set A
x : A
f : A →ₗ[R] B
hf : ∀ (a₁ a₂ : A), f (a₁ * a₂) = f a₁ * f a₂
h : x ∈ adjoin R s
⊢ f x ∈ adjoin R (⇑f '' (s ∪ {1}))

Tactic:
induction h using adjoin_induction with
  | mem a ha => exact subset_adjoin ⟨a, ⟨Set.subset_union_left ha, rfl⟩⟩
  | algebraMap r =>
    have : f 1 ∈ adjoin R (f '' (s ∪ {1})) :=
      subset_adjoin ⟨1, ⟨Set.subset_union_right <| Set.mem_singleton 1, rfl⟩⟩
    convert! Subalgebra.smul_mem (adjoin R (f '' (s ∪ { 1 }))) this r
    rw [algebraMap_eq_smul_one]
    exact f.map_smul _ _
  | add y z _ _ hy hz => simpa [hy, hz] using Subalgebra.add_mem _ hy hz
  | mul y z _ _ hy hz => simpa [hf, hy, hz] using Subalgebra.mul_mem _ hy hz

Goal state after:
Module: Mathlib.LinearAlgebra.DirectSum.TensorProduct

Goal state before:
pp: R : Type u
inst✝¹⁰ : CommSemiring R
S : Type u_1
inst✝⁹ : Semiring S
inst✝⁸ : Algebra R S
ι₁ : Type v₁
ι₂ : Type v₂
inst✝⁷ : DecidableEq ι₁
inst✝⁶ : DecidableEq ι₂
M₁ : ι₁ → Type w₁
M₂ : ι₂ → Type w₂
inst✝⁵ : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)
inst✝⁴ : (i₂ : ι₂) → AddCommMonoid (M₂ i₂)
inst✝³ : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝² : (i₂ : ι₂) → Module R (M₂ i₂)
inst✝¹ : (i₁ : ι₁) → Module S (M₁ i₁)
inst✝ : ∀ (i₁ : ι₁), IsScalarTower R S (M₁ i₁)
i₁ : ι₁
m₁ : M₁ i₁
i₂ : ι₂
m₂ : M₂ i₂
⊢ (TensorProduct.directSum R S M₁ M₂) ((lof S ι₁ M₁ i₁) m₁ ⊗ₜ[R] (lof R ι₂ M₂ i₂) m₂) =
    (lof S (ι₁ × ι₂) (fun i ↦ M₁ i.1 ⊗[R] M₂ i.2) (i₁, i₂)) (m₁ ⊗ₜ[R] m₂)

Tactic:
simp [TensorProduct.directSum]

Goal state after:
Module: Mathlib.Algebra.Module.Projective

Goal state before:
pp: R : Type u
inst✝³ : Semiring R
P : Type v
inst✝² : AddCommMonoid P
inst✝¹ : Module R P
inst✝ : Small.{v, u} R
h :
  ∀ {M N : Type v} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N] [inst_2 : Module R M] [inst_3 : Module R N]
    (f : M →ₗ[R] N) (g : P →ₗ[R] N), Function.Surjective ⇑f → ∃ h, f ∘ₗ h = g
p : (P →₀ R) →ₗ[R] P
hp : Function.Surjective ⇑p
⊢ ∃ h, p ∘ₗ h = LinearMap.id

Tactic:
let e := Finsupp.mapRange.linearEquiv (α := P) (Shrink.linearEquiv R R)

Goal state after:
R : Type u
inst✝³ : Semiring R
P : Type v
inst✝² : AddCommMonoid P
inst✝¹ : Module R P
inst✝ : Small.{v, u} R
h :
  ∀ {M N : Type v} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N] [inst_2 : Module R M] [inst_3 : Module R N]
    (f : M →ₗ[R] N) (g : P →ₗ[R] N), Function.Surjective ⇑f → ∃ h, f ∘ₗ h = g
p : (P →₀ R) →ₗ[R] P
hp : Function.Surjective ⇑p
e : (P →₀ Shrink.{v, u} R) ≃ₗ[R] P →₀ R := mapRange.linearEquiv (Shrink.linearEquiv R R)
⊢ ∃ h, p ∘ₗ h = LinearMap.id
Module: Mathlib.Algebra.Module.Projective

Goal state before:
pp: R : Type u
inst✝³ : Ring R
P : Type v
inst✝² : AddCommGroup P
inst✝¹ : Module R P
inst✝ : Small.{v, u} R
h :
  ∀ {M N : Type v} [inst : AddCommGroup M] [inst_1 : AddCommGroup N] [inst_2 : Module R M] [inst_3 : Module R N]
    (f : M →ₗ[R] N) (g : P →ₗ[R] N), Function.Surjective ⇑f → ∃ h, f ∘ₗ h = g
p : (P →₀ R) →ₗ[R] P
hp : Function.Surjective ⇑p
⊢ ∃ h, p ∘ₗ h = LinearMap.id

Tactic:
let e := Finsupp.mapRange.linearEquiv (α := P) (Shrink.linearEquiv R R)

Goal state after:
R : Type u
inst✝³ : Ring R
P : Type v
inst✝² : AddCommGroup P
inst✝¹ : Module R P
inst✝ : Small.{v, u} R
h :
  ∀ {M N : Type v} [inst : AddCommGroup M] [inst_1 : AddCommGroup N] [inst_2 : Module R M] [inst_3 : Module R N]
    (f : M →ₗ[R] N) (g : P →ₗ[R] N), Function.Surjective ⇑f → ∃ h, f ∘ₗ h = g
p : (P →₀ R) →ₗ[R] P
hp : Function.Surjective ⇑p
e : (P →₀ Shrink.{v, u} R) ≃ₗ[R] P →₀ R := mapRange.linearEquiv (Shrink.linearEquiv R R)
⊢ ∃ h, p ∘ₗ h = LinearMap.id
Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose

Goal state before:
pp: m : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : NonUnitalSemiring α
inst✝ : StarRing α
v w : m → α
⊢ star v ⬝ᵥ star w = star (w ⬝ᵥ v)

Tactic:
by simp [dotProduct]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose

Goal state before:
pp: m : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : NonUnitalSemiring α
inst✝ : StarRing α
v w : m → α
⊢ star v ⬝ᵥ w = star (star w ⬝ᵥ v)

Tactic:
by simp [dotProduct]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose

Goal state before:
pp: m : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : NonUnitalSemiring α
inst✝ : StarRing α
v w : m → α
⊢ v ⬝ᵥ star w = star (w ⬝ᵥ star v)

Tactic:
by simp [dotProduct]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarMul R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
r : R
x : A
⊢ ↑⟨⅟2 • (r • x + star (r • x)), ⋯⟩ = ↑((RingHom.id R) r • ⟨⅟2 • (x + star x), ⋯⟩)

Tactic:
simp [← mul_smul, show ⅟2 * r = r * ⅟2 from Commute.invOf_left <| (2 : ℕ).cast_commute r]

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: case pos
ι : Type u_1
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : IsDomain R
inst✝² : Finite ι
O : Type u_4
inst✝¹ : AddCommGroup O
inst✝ : Module R O
M N : Submodule R O
b'M : Basis ι R ↥M
N_bot : N ≠ ⊥
N_le_M : N ≤ M
this : ∃ ϕ, ∀ (ψ : ↥M →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
ϕ : ↥M →ₗ[R] R := this.choose
ϕ_max : ∀ (ψ : ↥M →ₗ[R] R), ¬this.choose.submoduleImage N < ψ.submoduleImage N
a : R := generator (ϕ.submoduleImage N)
a_mem : a ∈ ϕ.submoduleImage N
a_zero : a = 0
⊢ ∃ y ∈ M,
    ∃ a,
      a • y ∈ N ∧
        ∃ M' ≤ M,
          ∃ N' ≤ N,
            N' ≤ M' ∧
              (∀ (c : R), ∀ z ∈ M', c • y + z = 0 → c = 0) ∧
                (∀ (c : R), ∀ z ∈ N', c • a • y + z = 0 → c = 0) ∧
                  ∀ (n' : ℕ) (bN' : Basis (Fin n') R ↥N'),
                    ∃ bN,
                      ∀ (m' : ℕ) (hn'm' : n' ≤ m') (bM' : Basis (Fin m') R ↥M'),
                        ∃ (hnm : n' + 1 ≤ m' + 1),
                          ∃ bM,
                            ∀ (as : Fin n' → R),
                              (∀ (i : Fin n'), ↑(bN' i) = as i • ↑(bM' (Fin.castLE hn'm' i))) →
                                ∃ as', ∀ (i : Fin (n' + 1)), ↑(bN i) = as' i • ↑(bM (Fin.castLE hnm i))

Tactic:
have := eq_bot_of_generator_maximal_submoduleImage_eq_zero b'M N_le_M ϕ_max a_zero

Goal state after:
case pos
ι : Type u_1
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : IsDomain R
inst✝² : Finite ι
O : Type u_4
inst✝¹ : AddCommGroup O
inst✝ : Module R O
M N : Submodule R O
b'M : Basis ι R ↥M
N_bot : N ≠ ⊥
N_le_M : N ≤ M
this✝ : ∃ ϕ, ∀ (ψ : ↥M →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
ϕ : ↥M →ₗ[R] R := this✝.choose
ϕ_max : ∀ (ψ : ↥M →ₗ[R] R), ¬this✝.choose.submoduleImage N < ψ.submoduleImage N
a : R := generator (ϕ.submoduleImage N)
a_mem : a ∈ ϕ.submoduleImage N
a_zero : a = 0
this : N = ⊥
⊢ ∃ y ∈ M,
    ∃ a,
      a • y ∈ N ∧
        ∃ M' ≤ M,
          ∃ N' ≤ N,
            N' ≤ M' ∧
              (∀ (c : R), ∀ z ∈ M', c • y + z = 0 → c = 0) ∧
                (∀ (c : R), ∀ z ∈ N', c • a • y + z = 0 → c = 0) ∧
                  ∀ (n' : ℕ) (bN' : Basis (Fin n') R ↥N'),
                    ∃ bN,
                      ∀ (m' : ℕ) (hn'm' : n' ≤ m') (bM' : Basis (Fin m') R ↥M'),
                        ∃ (hnm : n' + 1 ≤ m' + 1),
                          ∃ bM,
                            ∀ (as : Fin n' → R),
                              (∀ (i : Fin n'), ↑(bN' i) = as i • ↑(bM' (Fin.castLE hn'm' i))) →
                                ∃ as', ∀ (i : Fin (n' + 1)), ↑(bN i) = as' i • ↑(bM (Fin.castLE hnm i))
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommSemiring R
m : Type u_3
n : Type u_4
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₁
inst✝¹ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst✝ : Fintype m
M : Matrix m n R
i : n
⊢ ((toLin v₁ v₂) M) (v₁ i) = ∑ j, M j i • v₂ j

Tactic:
rw [Matrix.toLin_apply, Finset.sum_congr rfl fun j _hj ↦ ?_]

Goal state after:
R : Type u_1
inst✝⁷ : CommSemiring R
m : Type u_3
n : Type u_4
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₁
inst✝¹ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst✝ : Fintype m
M : Matrix m n R
i : n
j : m
_hj : j ∈ Finset.univ
⊢ (M *ᵥ ⇑(v₁.repr (v₁ i))) j • v₂ j = M j i • v₂ j
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: case h₁
R : Type u_1
inst✝⁷ : CommSemiring R
m : Type u_3
n : Type u_4
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₁
inst✝¹ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst✝ : Fintype m
M : Matrix m n R
i : n
j : m
_hj : j ∈ Finset.univ
⊢ i ∉ Finset.univ → M j i * (Finsupp.single i 1) i = 0

Tactic:
intros
    have := Finset.mem_univ i
    contradiction

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝⁹ : Fintype n
inst✝⁸ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M₁
inst✝⁴ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst✝³ : Fintype m
M₃ : Type u_7
inst✝² : AddCommMonoid M₃
inst✝¹ : Module R M₃
v₃ : Basis l R M₃
inst✝ : DecidableEq m
M : Matrix m n R
M' : Matrix n m R
hMM' : M * M' = 1
hM'M : M' * M = 1
x : M₂
⊢ ((toLin v₁ v₂) M) (((toLin v₂ v₁) M') x) = x

Tactic:
rw [← Matrix.toLin_mul_apply, hMM', Matrix.toLin_one, id_apply]

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
b✝ : ι → M
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : Finite ι
b : Basis ι R M
N : Submodule R M
m n : ℕ
bM : Basis (Fin m) R ↥⊤
bN : Basis (Fin n) R ↥(comap ⊤.subtype N)
f : Fin n ↪ Fin m
a : Fin n → R
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
bM' : Basis (Fin m) R M := bM.map (LinearEquiv.ofTop ⊤ ⋯)
e : Fin m ≃ ι := bM'.indexEquiv b
i : Fin n
⊢ ↑((bN.map (comapSubtypeEquivOfLe ⋯)) i) = a i • (bM'.reindex e) ((f.trans e.toEmbedding) i)

Tactic:
by
    simp only [bM', snf, Basis.map_apply, LinearEquiv.ofTop_apply, Submodule.coe_smul_of_tower,
      Submodule.comapSubtypeEquivOfLe_apply_coe, Basis.reindex_apply,
      Equiv.toEmbedding_apply, Function.Embedding.trans_apply, Equiv.symm_apply_apply]

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommRing P
A : Type u_4
inst✝ : CommRing A
K : Type u_5
x y : ℕ
h : (algebraMap ℕ ℚ≥0) x = (algebraMap ℕ ℚ≥0) y
⊢ ↑1 * x = ↑1 * y

Tactic:
by simpa using h

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

Goal state before:
pp: case h
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₁) m) * (algebraMap S₂ T) ((algebraMap R S₂) ↑(z, ⟨n, hn⟩).2) *
      (algebraMap S₁ T) ↑hunit.unit⁻¹

Tactic:
convert_to _ = a * (algebraMap S₂ T) ((algebraMap R S₂) n) *
        (algebraMap S₁ T) (((algebraMap R S₁) m) * hunit.unit⁻¹.val)

Goal state after:
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⁻¹)

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.FractionRing

Goal state before:
pp: R : Type u_1
inst✝⁴¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴⁰ : CommRing S
inst✝³⁹ : Algebra R S
P : Type u_3
inst✝³⁸ : CommRing P
A✝ : Type u_4
inst✝³⁷ : CommRing A✝
K : Type u_5
B✝ : Type u_6
inst✝³⁶ : CommRing B✝
inst✝³⁵ : IsDomain B✝
inst✝³⁴ : Field K
L : Type u_7
inst✝³³ : Field L
inst✝³² : Algebra A✝ K
inst✝³¹ : IsFractionRing A✝ K
g : A✝ →+* L
A : Type u_8
B : Type u_9
C : Type u_10
D : Type u_11
inst✝³⁰ : CommRing A
inst✝²⁹ : CommRing B
inst✝²⁸ : CommRing C
inst✝²⁷ : CommRing D
inst✝²⁶ : Algebra A B
inst✝²⁵ : Algebra A C
inst✝²⁴ : Algebra A D
FA : Type u_12
FB : Type u_13
FC : Type u_14
FD : Type u_15
inst✝²³ : Field FA
inst✝²² : Field FB
inst✝²¹ : Field FC
inst✝²⁰ : Field FD
inst✝¹⁹ : Algebra A FA
inst✝¹⁸ : Algebra B FB
inst✝¹⁷ : Algebra C FC
inst✝¹⁶ : Algebra D FD
inst✝¹⁵ : IsFractionRing A FA
inst✝¹⁴ : IsFractionRing B FB
inst✝¹³ : IsFractionRing C FC
inst✝¹² : IsFractionRing D FD
inst✝¹¹ : Algebra A FB
inst✝¹⁰ : IsScalarTower A B FB
inst✝⁹ : Algebra A FC
inst✝⁸ : IsScalarTower A C FC
inst✝⁷ : Algebra A FD
inst✝⁶ : IsScalarTower A D FD
inst✝⁵ : Algebra FA FB
inst✝⁴ : IsScalarTower A FA FB
inst✝³ : Algebra FA FC
inst✝² : IsScalarTower A FA FC
inst✝¹ : Algebra FA FD
inst✝ : IsScalarTower A FA FD
f : B ≃ₐ[A] C
x y : A
⊢ (ringEquivOfRingEquiv f.toRingEquiv).toFun ((algebraMap A FB) x / (algebraMap A FB) y) =
    (algebraMap A FC) x / (algebraMap A FC) y

Tactic:
IsScalarTower.algebraMap_apply A B FB

Goal state after:
R : Type u_1
inst✝⁴¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴⁰ : CommRing S
inst✝³⁹ : Algebra R S
P : Type u_3
inst✝³⁸ : CommRing P
A✝ : Type u_4
inst✝³⁷ : CommRing A✝
K : Type u_5
B✝ : Type u_6
inst✝³⁶ : CommRing B✝
inst✝³⁵ : IsDomain B✝
inst✝³⁴ : Field K
L : Type u_7
inst✝³³ : Field L
inst✝³² : Algebra A✝ K
inst✝³¹ : IsFractionRing A✝ K
g : A✝ →+* L
A : Type u_8
B : Type u_9
C : Type u_10
D : Type u_11
inst✝³⁰ : CommRing A
inst✝²⁹ : CommRing B
inst✝²⁸ : CommRing C
inst✝²⁷ : CommRing D
inst✝²⁶ : Algebra A B
inst✝²⁵ : Algebra A C
inst✝²⁴ : Algebra A D
FA : Type u_12
FB : Type u_13
FC : Type u_14
FD : Type u_15
inst✝²³ : Field FA
inst✝²² : Field FB
inst✝²¹ : Field FC
inst✝²⁰ : Field FD
inst✝¹⁹ : Algebra A FA
inst✝¹⁸ : Algebra B FB
inst✝¹⁷ : Algebra C FC
inst✝¹⁶ : Algebra D FD
inst✝¹⁵ : IsFractionRing A FA
inst✝¹⁴ : IsFractionRing B FB
inst✝¹³ : IsFractionRing C FC
inst✝¹² : IsFractionRing D FD
inst✝¹¹ : Algebra A FB
inst✝¹⁰ : IsScalarTower A B FB
inst✝⁹ : Algebra A FC
inst✝⁸ : IsScalarTower A C FC
inst✝⁷ : Algebra A FD
inst✝⁶ : IsScalarTower A D FD
inst✝⁵ : Algebra FA FB
inst✝⁴ : IsScalarTower A FA FB
inst✝³ : Algebra FA FC
inst✝² : IsScalarTower A FA FC
inst✝¹ : Algebra FA FD
inst✝ : IsScalarTower A FA FD
f : B ≃ₐ[A] C
x y : A
⊢ (ringEquivOfRingEquiv f.toRingEquiv).toFun
      ((algebraMap B FB) ((algebraMap A B) x) / (algebraMap B FB) ((algebraMap A B) y)) =
    (algebraMap A FC) x / (algebraMap A FC) y
Module: Mathlib.RingTheory.Localization.Defs

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

Tactic:
rw [← sub_eq_zero, ← map_sub, ← map_sub] at hz

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
T : Type u_4
inst✝ : CommRing T
f : S →+* T
h : ∀ (x : R), f ((algebraMap R S) x) = 0 → (algebraMap R S) x = 0
x y : R
hz : f ((algebraMap R S) (x - y)) = 0
⊢ (algebraMap R S) x = (algebraMap R S) y
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 (-a) ↔ ¬IsUnit a

Tactic:
IsUnit.neg_iff

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ˣ
x y : A
h : IsUnit (1 - x * y)
⊢ (1 - y * x) * (1 + y * h.unit.inv * x) = 1 - y * x + y * ((1 - x * y) * h.unit.inv) * x

Tactic:
noncomm_ring

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 b : A
r : Rˣ
x y : A
h : IsUnit (1 - x * y)
⊢ (1 + y * h.unit.inv * x) * (1 - y * x) = 1 - y * x + y * (h.unit.inv * (1 - x * y)) * x

Tactic:
noncomm_ring

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

Goal state before:
pp: 𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial A
⊢ {0} ⊆ σ 0

Tactic:
simp [Algebra.algebraMap_eq_smul_one, mem_iff]

Goal state after:
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✝¹³ : CommSemiring S
inst✝¹² : Algebra R S
inst✝¹¹ : Semiring A
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra S A
inst✝⁸ : IsScalarTower R S A
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R B
inst✝⁵ : Semiring C
inst✝⁴ : Algebra S C
inst✝³ : Semiring D
inst✝² : Algebra R D
inst✝¹ : Algebra R C
inst✝ : IsScalarTower R S C
f : A →ₐ[S] C
g : B →ₐ[R] C
hfg : ∀ (x : A) (y : B), Commute (f x) (g y)
a₁ a₂ : A
b₁ b₂ : B
⊢ f (a₁ * a₂) * g (b₁ * b₂) = f a₁ * g b₁ * (f a₂ * g b₂)

Tactic:
rw [map_mul, map_mul, (hfg a₂ b₁).mul_mul_mul_comm]

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

Goal state before:
pp: case e'_2
R : Type u_1
inst✝ : Semiring R
x : R
hx : IsQuasiregular x
y : R
hy₁ : y + x + x * y = 0
hy₂ : x + y + y * x = 0
⊢ (1 + x) * (1 + y) = 1 + (y + x + x * y)

Tactic:
noncomm_ring

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

Goal state before:
pp: case e'_2
R : Type u_1
inst✝ : Semiring R
x : R
hx : IsQuasiregular x
y : R
hy₁ : y + x + x * y = 0
hy₂ : x + y + y * x = 0
⊢ (1 + y) * (1 + x) = 1 + (x + y + y * x)

Tactic:
noncomm_ring

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
x : R
hx : IsUnit (1 + x)
this : (↑hx.unit⁻¹ - 1 + 1) * (1 + x) - 1 = 0
⊢ x + (↑hx.unit⁻¹ - 1) + (↑hx.unit⁻¹ - 1) * x = (↑hx.unit⁻¹ - 1 + 1) * (1 + x) - 1

Tactic:
noncomm_ring

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
x : R
hx : IsUnit (1 + x)
this : (1 + x) * (↑hx.unit⁻¹ - 1 + 1) - 1 = 0
⊢ ↑hx.unit⁻¹ - 1 + x + x * (↑hx.unit⁻¹ - 1) = (1 + x) * (↑hx.unit⁻¹ - 1 + 1) - 1

Tactic:
noncomm_ring

Goal state after:
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✝¹⁹ : CommSemiring S
inst✝¹⁸ : Algebra R S
inst✝¹⁷ : Semiring A
inst✝¹⁶ : Algebra R A
inst✝¹⁵ : Algebra S A
inst✝¹⁴ : IsScalarTower R S A
inst✝¹³ : Semiring B
inst✝¹² : Algebra R B
inst✝¹¹ : Semiring C
inst✝¹⁰ : Algebra R C
inst✝⁹ : Algebra S C
inst✝⁸ : IsScalarTower R S C
inst✝⁷ : Semiring D
inst✝⁶ : Algebra R D
inst✝⁵ : Semiring E
inst✝⁴ : Algebra R E
inst✝³ : Algebra S E
inst✝² : IsScalarTower R S E
inst✝¹ : Semiring F
inst✝ : Algebra R F
f : A →ₐ[S] C
g : B →ₐ[R] D
⊢ (AlgebraTensorModule.map f.toLinearMap g.toLinearMap) (1 ⊗ₜ[R] 1) = 1

Tactic:
by simp [one_def]

Goal state after:
Module: Mathlib.Algebra.Algebra.Unitization

Goal state before:
pp: case inl_add_inr
S : Type u_1
R : Type u_2
A : Type u_3
inst✝⁸ : CommSemiring S
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalSemiring A
inst✝⁵ : Module R A
inst✝⁴ : IsScalarTower R A A
inst✝³ : SMulCommClass R A A
inst✝² : Algebra S R
inst✝¹ : DistribMulAction S A
inst✝ : IsScalarTower S R A
s : S
r✝ : R
a✝ : A
⊢ ((inlRingHom R A).comp (algebraMap S R)) s * (inl r✝ + ↑a✝) =
    (inl r✝ + ↑a✝) * ((inlRingHom R A).comp (algebraMap S R)) s

Tactic:
change inl (algebraMap S R s) * _ = _ * inl (algebraMap S R s)
      rw [mul_add, add_mul, inl_mul_inl, inl_mul_inl, inl_mul_inr, inr_mul_inl, mul_comm]

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

Goal state before:
pp: R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
h : Function.Bijective ⇑(algebraMap R A)
⊢ Function.Bijective ⇑includeRight

Tactic:
by
  rw [← Function.Bijective.of_comp_iff' (TensorProduct.comm R A B).bijective]
  exact Algebra.TensorProduct.includeLeft_bijective (S := R) h

Goal state after: