mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: α : Type u
A : Matrix (Fin 2) (Fin 2) α
⊢ A = !![A 0 0, A 0 1; A 1 0, A 1 1]

Tactic:
ext i j

Goal state after:
α : Type u
A : Matrix (Fin 2) (Fin 2) α
i j : Fin 2
⊢ A i j = !![A 0 0, A 0 1; A 1 0, A 1 1] i j
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: α : Type u
A : Matrix (Fin 3) (Fin 3) α
⊢ A = !![A 0 0, A 0 1, A 0 2; A 1 0, A 1 1, A 1 2; A 2 0, A 2 1, A 2 2]

Tactic:
ext i j

Goal state after:
α : Type u
A : Matrix (Fin 3) (Fin 3) α
i j : Fin 3
⊢ A i j = !![A 0 0, A 0 1, A 0 2; A 1 0, A 1 1, A 1 2; A 2 0, A 2 1, A 2 2] i j
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: α : Type u
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
a₁₁ a₁₂ a₂₁ a₂₂ b₁₁ b₁₂ b₂₁ b₂₂ : α
⊢ !![a₁₁, a₁₂; a₂₁, a₂₂] * !![b₁₁, b₁₂; b₂₁, b₂₂] =
    !![a₁₁ * b₁₁ + a₁₂ * b₂₁, a₁₁ * b₁₂ + a₁₂ * b₂₂; a₂₁ * b₁₁ + a₂₂ * b₂₁, a₂₁ * b₁₂ + a₂₂ * b₂₂]

Tactic:
ext i j

Goal state after:
α : Type u
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
a₁₁ a₁₂ a₂₁ a₂₂ b₁₁ b₁₂ b₂₁ b₂₂ : α
i j : Fin 2
⊢ (!![a₁₁, a₁₂; a₂₁, a₂₂] * !![b₁₁, b₁₂; b₂₁, b₂₂]) i j =
    !![a₁₁ * b₁₁ + a₁₂ * b₂₁, a₁₁ * b₁₂ + a₁₂ * b₂₂; a₂₁ * b₁₁ + a₂₂ * b₂₁, a₂₁ * b₁₂ + a₂₂ * b₂₂] i j
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: α : Type u
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
a₁₁ a₁₂ a₁₃ a₂₁ a₂₂ a₂₃ a₃₁ a₃₂ a₃₃ b₁₁ b₁₂ b₁₃ b₂₁ b₂₂ b₂₃ b₃₁ b₃₂ b₃₃ : α
⊢ !![a₁₁, a₁₂, a₁₃; a₂₁, a₂₂, a₂₃; a₃₁, a₃₂, a₃₃] * !![b₁₁, b₁₂, b₁₃; b₂₁, b₂₂, b₂₃; b₃₁, b₃₂, b₃₃] =
    !![a₁₁ * b₁₁ + a₁₂ * b₂₁ + a₁₃ * b₃₁, a₁₁ * b₁₂ + a₁₂ * b₂₂ + a₁₃ * b₃₂, a₁₁ * b₁₃ + a₁₂ * b₂₃ + a₁₃ * b₃₃;
      a₂₁ * b₁₁ + a₂₂ * b₂₁ + a₂₃ * b₃₁, a₂₁ * b₁₂ + a₂₂ * b₂₂ + a₂₃ * b₃₂, a₂₁ * b₁₃ + a₂₂ * b₂₃ + a₂₃ * b₃₃;
      a₃₁ * b₁₁ + a₃₂ * b₂₁ + a₃₃ * b₃₁, a₃₁ * b₁₂ + a₃₂ * b₂₂ + a₃₃ * b₃₂, a₃₁ * b₁₃ + a₃₂ * b₂₃ + a₃₃ * b₃₃]

Tactic:
ext i j

Goal state after:
α : Type u
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
a₁₁ a₁₂ a₁₃ a₂₁ a₂₂ a₂₃ a₃₁ a₃₂ a₃₃ b₁₁ b₁₂ b₁₃ b₂₁ b₂₂ b₂₃ b₃₁ b₃₂ b₃₃ : α
i j : Fin 3
⊢ (!![a₁₁, a₁₂, a₁₃; a₂₁, a₂₂, a₂₃; a₃₁, a₃₂, a₃₃] * !![b₁₁, b₁₂, b₁₃; b₂₁, b₂₂, b₂₃; b₃₁, b₃₂, b₃₃]) i j =
    !![a₁₁ * b₁₁ + a₁₂ * b₂₁ + a₁₃ * b₃₁, a₁₁ * b₁₂ + a₁₂ * b₂₂ + a₁₃ * b₃₂, a₁₁ * b₁₃ + a₁₂ * b₂₃ + a₁₃ * b₃₃;
        a₂₁ * b₁₁ + a₂₂ * b₂₁ + a₂₃ * b₃₁, a₂₁ * b₁₂ + a₂₂ * b₂₂ + a₂₃ * b₃₂, a₂₁ * b₁₃ + a₂₂ * b₂₃ + a₂₃ * b₃₃;
        a₃₁ * b₁₁ + a₃₂ * b₂₁ + a₃₃ * b₃₁, a₃₁ * b₁₂ + a₃₂ * b₂₂ + a₃₃ * b₃₂, a₃₁ * b₁₃ + a₃₂ * b₂₃ + a₃₃ * b₃₃]
      i j
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝¹ : Fintype m
inst✝ : DecidableEq m
f g : (m → R) →ₗ[R] n → R
⊢ (fun i j ↦ (f + g) ((single R (fun x ↦ R) i) 1) j) =
    (fun i j ↦ f ((single R (fun x ↦ R) i) 1) j) + fun i j ↦ g ((single R (fun x ↦ R) i) 1) j

Tactic:
ext i j

Goal state after:
R : Type u_1
inst✝² : Semiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝¹ : Fintype m
inst✝ : DecidableEq m
f g : (m → R) →ₗ[R] n → R
i : m
j : n
⊢ (f + g) ((single R (fun x ↦ R) i) 1) j =
    ((fun i j ↦ f ((single R (fun x ↦ R) i) 1) j) + fun i j ↦ g ((single R (fun x ↦ R) i) 1) j) i j
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝¹ : Fintype m
inst✝ : DecidableEq m
c : Rᵐᵒᵖ
f : (m → R) →ₗ[R] n → R
⊢ (fun i j ↦ (c • f) ((single R (fun x ↦ R) i) 1) j) = (RingHom.id Rᵐᵒᵖ) c • fun i j ↦ f ((single R (fun x ↦ R) i) 1) j

Tactic:
ext i j

Goal state after:
R : Type u_1
inst✝² : Semiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝¹ : Fintype m
inst✝ : DecidableEq m
c : Rᵐᵒᵖ
f : (m → R) →ₗ[R] n → R
i : m
j : n
⊢ (c • f) ((single R (fun x ↦ R) i) 1) j = ((RingHom.id Rᵐᵒᵖ) c • fun i j ↦ f ((single R (fun x ↦ R) i) 1) j) i j
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m n R
⊢ (fun f i j ↦ f ((single R (fun x ↦ R) i) 1) j) M.vecMulLinear = M

Tactic:
ext i j

Goal state after:
R : Type u_1
inst✝² : Semiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m n R
i : m
j : n
⊢ (fun f i j ↦ f ((single R (fun x ↦ R) i) 1) j) M.vecMulLinear i j = M i j
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
k : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
inst✝¹ : DecidableEq n
inst✝ : Fintype n
f g : (n → R) →ₗ[R] m → R
⊢ (of fun i j ↦ (f + g) (Pi.single j 1) i) = (of fun i j ↦ f (Pi.single j 1) i) + of fun i j ↦ g (Pi.single j 1) i

Tactic:
ext i j

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
k : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
inst✝¹ : DecidableEq n
inst✝ : Fintype n
f g : (n → R) →ₗ[R] m → R
i : m
j : n
⊢ of (fun i j ↦ (f + g) (Pi.single j 1) i) i j =
    ((of fun i j ↦ f (Pi.single j 1) i) + of fun i j ↦ g (Pi.single j 1) i) i j
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
k : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
inst✝¹ : DecidableEq n
inst✝ : Fintype n
c : R
f : (n → R) →ₗ[R] m → R
⊢ (of fun i j ↦ (c • f) (Pi.single j 1) i) = (RingHom.id R) c • of fun i j ↦ f (Pi.single j 1) i

Tactic:
ext i j

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
k : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
inst✝¹ : DecidableEq n
inst✝ : Fintype n
c : R
f : (n → R) →ₗ[R] m → R
i : m
j : n
⊢ of (fun i j ↦ (c • f) (Pi.single j 1) i) i j = ((RingHom.id R) c • of fun i j ↦ f (Pi.single j 1) i) i j
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
k : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
inst✝¹ : DecidableEq n
inst✝ : Fintype n
f : (n → R) →ₗ[R] m → R
⊢ ((fun f ↦ of fun i j ↦ f (Pi.single j 1) i) f).mulVecLin = f

Tactic:
by
    apply (Pi.basisFun R n).ext
    intro j; ext i
    simp only [Pi.basisFun_apply, Matrix.mulVec_single_one, col_apply,
      Matrix.mulVecLin_apply, of_apply]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
k : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix m n R
⊢ (fun f ↦ of fun i j ↦ f (Pi.single j 1) i) M.mulVecLin = M

Tactic:
ext i j

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
k : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix m n R
i : m
j : n
⊢ (fun f ↦ of fun i j ↦ f (Pi.single j 1) i) M.mulVecLin i j = M i j
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
m : Type u_4
n : Type u_5
inst✝¹ : DecidableEq n
inst✝ : Fintype n
f : (n → R) →ₗ[R] m → R
v : n → R
⊢ toMatrix' f *ᵥ v = f v

Tactic:
by
  rw [← toLin'_apply, toLin'_toMatrix']

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
l : Type u_3
m : Type u_4
n : Type u_5
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : Fintype l
inst✝ : DecidableEq l
f : (n → R) →ₗ[R] m → R
g : (l → R) →ₗ[R] n → R
⊢ f ∘ₗ g = toLin' (toMatrix' f * toMatrix' g)

Tactic:
rw [Matrix.toLin'_mul, Matrix.toLin'_toMatrix', Matrix.toLin'_toMatrix']

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
n : Type u_4
inst✝³ : Fintype n
inst✝² : DecidableEq n
M₁ : Type u_5
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
v₁ : Basis n R M₁
⊢ (toMatrix v₁ v₁) id = 1

Tactic:
ext i j

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
n : Type u_4
inst✝³ : Fintype n
inst✝² : DecidableEq n
M₁ : Type u_5
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
v₁ : Basis n R M₁
i j : n
⊢ (toMatrix v₁ v₁) id i j = 1 i j
Module: Mathlib.RingTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
s : ↥S
⊢ 0 /ₒ s = 0

Tactic:
rw [OreLocalization.zero_def, oreDiv_eq_iff]
  exact ⟨s, 1, by simp⟩

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
n : Type u_4
inst✝³ : Fintype n
inst✝² : DecidableEq n
M₁ : Type u_5
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
v₁ : Basis n R M₁
r : R
⊢ (toMatrix v₁ v₁) ((toLin v₁ v₁) ((scalar n) r)) = (toMatrix v₁ v₁) (r • LinearMap.id)

Tactic:
simp [toMatrix_id, smul_one_eq_diagonal]

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_5
M₂ : Type u_6
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₁
inst✝² : Module R M₂
inst✝¹ : Fintype l
inst✝ : DecidableEq l
b : Basis l R M₁
b' : Basis l R M₂
⊢ (toMatrix b' b) ↑(b'.equiv b (Equiv.refl l)) = 1

Tactic:
ext i j

Goal state after:
R : Type u_1
inst✝⁶ : CommSemiring R
l : Type u_2
M₁ : Type u_5
M₂ : Type u_6
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₁
inst✝² : Module R M₂
inst✝¹ : Fintype l
inst✝ : DecidableEq l
b : Basis l R M₁
b' : Basis l R M₂
i j : l
⊢ (toMatrix b' b) (↑(b'.equiv b (Equiv.refl l))) i j = 1 i j
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✝ : Finite m
f : M₁ →ₗ[R] R
x : M₂
⊢ (toMatrix v₁ v₂) (f.smulRight x) = vecMulVec (⇑(v₂.repr x)) (⇑f ∘ ⇑v₁)

Tactic:
ext i j

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✝ : Finite m
f : M₁ →ₗ[R] R
x : M₂
i : m
j : n
⊢ (toMatrix v₁ v₂) (f.smulRight x) i j = vecMulVec (⇑(v₂.repr x)) (⇑f ∘ ⇑v₁) i j
Module: Mathlib.RingTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : DistribMulAction R X
x y : OreLocalization S X
⊢ x + y = y + x

Tactic:
induction x with | _ r s
  induction y with | _ r' s'
  rcases oreDivAddChar' r r' s s' with ⟨ra, sa, ha, ha'⟩
  rw [ha', oreDiv_add_char' s' s _ _ ha.symm (ha ▸ (sa * s).2), add_comm]
  congr; ext; exact ha

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
n : Type u_4
inst✝³ : Fintype n
inst✝² : DecidableEq n
M₁ : Type u_5
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
v₁ : Basis n R M₁
M : Matrix n n R
v : M₁
⊢ v₁.equivFun.symm (M *ᵥ ⇑(v₁.repr v)) = ∑ j, (M *ᵥ ⇑(v₁.repr v)) j • v₁ j

Tactic:
v₁.equivFun_symm_apply

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
n : Type u_4
inst✝³ : Fintype n
inst✝² : DecidableEq n
M₁ : Type u_5
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
v₁ : Basis n R M₁
M : Matrix n n R
v : M₁
⊢ ∑ i, (M *ᵥ ⇑(v₁.repr v)) i • v₁ i = ∑ j, (M *ᵥ ⇑(v₁.repr v)) j • v₁ j
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
⊢ (algebraMap R S)
      (((toLocalizationMap M S).sec y).1 * ↑((toLocalizationMap M S).sec x).2 *
          ↑((toLocalizationMap M S).sec (x + y)).2 +
        ↑((toLocalizationMap M S).sec y).2 * ((toLocalizationMap M S).sec x).1 *
          ↑((toLocalizationMap M S).sec (x + y)).2) =
    (algebraMap R S)
      (↑((toLocalizationMap M S).sec y).2 * ↑((toLocalizationMap M S).sec x).2 *
        ((toLocalizationMap M S).sec (x + y)).1)

Tactic:
simp only [sec_spec', toLocalizationMap_sec, map_add, map_mul]

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
⊢ (algebraMap R S) ↑(sec M y).2 * y * (algebraMap R S) ↑(sec M x).2 * (algebraMap R S) ↑(sec M (x + y)).2 +
      (algebraMap R S) ↑(sec M y).2 * ((algebraMap R S) ↑(sec M x).2 * x) * (algebraMap R S) ↑(sec M (x + y)).2 =
    (algebraMap R S) ↑(sec M y).2 * (algebraMap R S) ↑(sec M x).2 * ((algebraMap R S) ↑(sec M (x + y)).2 * (x + y))
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
K : Type u_5
inst✝² : CommRing K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K
hx : x ∈ K⁰
r : R × ↥R⁰
eq : x * (algebraMap R K) ↑r.2 = (algebraMap R K) r.1
⊢ x ∈ IsUnit.submonoid K

Tactic:
let r' : R⁰ := ⟨r.1, mem_nonZeroDivisors_of_injective (IsFractionRing.injective R K)
    (eq ▸ mul_mem hx (map_units ..).mem_nonZeroDivisors)⟩

Goal state after:
R : Type u_1
inst✝³ : CommRing R
K : Type u_5
inst✝² : CommRing K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K
hx : x ∈ K⁰
r : R × ↥R⁰
eq : x * (algebraMap R K) ↑r.2 = (algebraMap R K) r.1
r' : ↥R⁰ := ⟨r.1, ⋯⟩
⊢ x ∈ IsUnit.submonoid K
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: A : Type u_4
inst✝⁴ : CommRing A
K : Type u_5
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
L : Type u_8
inst✝ : Field L
g : A →+* L
f : K →+* L
h : f.comp (algebraMap A K) = g
⊢ Subfield.map f (Subfield.closure (Set.range ⇑(algebraMap A K))) = Subfield.closure ↑g.range

Tactic:
f.map_field_closure,

Goal state after:
A : Type u_4
inst✝⁴ : CommRing A
K : Type u_5
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
L : Type u_8
inst✝ : Field L
g : A →+* L
f : K →+* L
h : f.comp (algebraMap A K) = g
⊢ Subfield.closure (⇑f '' Set.range ⇑(algebraMap A K)) = Subfield.closure ↑g.range
Module: Mathlib.RingTheory.Localization.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
M : Submonoid R
a : R
b : ↥M
c : R
⊢ (r M) (↑b * c + ↑b * a, b * b) (a + c, b)

Tactic:
r_eq_r'

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
M : Submonoid R
a : R
b : ↥M
c : R
⊢ (r' M) (↑b * c + ↑b * a, b * b) (a + c, b)
Module: Mathlib.RingTheory.Localization.Basic

Goal state before:
pp: R : Type u_4
Rₘ : Type u_5
inst✝³ : CommRing R
inst✝² : CommRing Rₘ
M : Submonoid R
hM : 0 ∉ M
hR : IsField R
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
⊢ Bijective ⇑(algebraMap R Rₘ)

Tactic:
let := hR.toField
  replace hM := le_nonZeroDivisors_of_noZeroDivisors hM
  refine ⟨IsLocalization.injective _ hM, fun x => ?_⟩
  obtain ⟨r, ⟨m, hm⟩, rfl⟩ := exists_mk'_eq M x
  obtain ⟨n, hn⟩ := hR.mul_inv_cancel (nonZeroDivisors.ne_zero <| hM hm)
  exact ⟨r * n, by rw [eq_mk'_iff_mul_eq, ← map_mul, mul_assoc, _root_.mul_comm n, hn, mul_one]⟩

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

Goal state before:
pp: α : Type u_1
s : Set α
a : α
inst✝ : InvolutiveStar α
⊢ a⋆ ∈ s⋆ ↔ a ∈ s

Tactic:
simp only [mem_star, star_star]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonAssocRing β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
mul : Mul α := e.mul
⊢ NonAssocRing α

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

Goal state after:
case zero
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonAssocRing β
add_group_with_one : AddGroupWithOne α := ⋯
mul : Mul α := ⋯
⊢ e 0 = 0

case one
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonAssocRing β
add_group_with_one : AddGroupWithOne α := ⋯
mul : Mul α := ⋯
⊢ e 1 = 1

case add
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonAssocRing β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
mul : Mul α := e.mul
x✝ y✝ : α
⊢ e (x✝ + y✝) = e x✝ + e y✝

case mul
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonAssocRing β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
mul : Mul α := e.mul
x✝ y✝ : α
⊢ e (x✝ * y✝) = e x✝ * e y✝

case neg
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonAssocRing β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
mul : Mul α := e.mul
x✝ : α
⊢ e (-x✝) = -e x✝

case sub
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonAssocRing β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
mul : Mul α := e.mul
x✝ y✝ : α
⊢ e (x✝ - y✝) = e x✝ - e y✝

case nsmul
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonAssocRing β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
mul : Mul α := e.mul
n✝ : ℕ
x✝ : α
⊢ e (n✝ • x✝) = n✝ • e x✝

case zsmul
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonAssocRing β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
mul : Mul α := e.mul
n✝ : ℤ
x✝ : α
⊢ e (n✝ • x✝) = n✝ • e x✝

case natCast
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonAssocRing β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
mul : Mul α := e.mul
n✝ : ℕ
⊢ e ↑n✝ = ↑n✝

case intCast
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonAssocRing β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
mul : Mul α := e.mul
n✝ : ℤ
⊢ e ↑n✝ = ↑n✝
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
⊢ ↑(IsUnit.unit ha) * ((↑(IsUnit.unit ha)⁻¹ - ↑(IsUnit.unit hb)⁻¹) * ↑(IsUnit.unit hb)) = a - b

Tactic:
sub_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 ha) * (↑(IsUnit.unit ha)⁻¹ * ↑(IsUnit.unit hb) - ↑(IsUnit.unit hb)⁻¹ * ↑(IsUnit.unit hb)) = a - b
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
r : Rˣ
a : Aˣ
h : IsUnit (r • 1 - ↑a)
h₁ : ↑a * (r • ↑a⁻¹ - 1) = r • 1 - ↑a
⊢ (r • ↑a⁻¹ - 1) * ↑a = r • 1 - ↑a

Tactic:
sub_mul,

Goal state after:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
a : Aˣ
h : IsUnit (r • 1 - ↑a)
h₁ : ↑a * (r • ↑a⁻¹ - 1) = r • 1 - ↑a
⊢ r • ↑a⁻¹ * ↑a - 1 * ↑a = r • 1 - ↑a
Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum

Goal state before:
pp: R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁵ : Semifield R
inst✝⁴ : Semifield S
inst✝³ : Ring A
inst✝² : Algebra R S
inst✝¹ : Algebra R A
inst✝ : Algebra S A
a : A
f : S → R
h₁ : Function.LeftInverse f ⇑(algebraMap R S)
h₂ : Set.RightInvOn f (⇑(algebraMap R S)) (spectrum S a)
x : S
hx : x ∈ quasispectrum S a
⊢ (algebraMap R S) (f x) = x

Tactic:
obtain (rfl | hx) := mem_quasispectrum_iff.mp hx

Goal state after:
case inl
R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁵ : Semifield R
inst✝⁴ : Semifield S
inst✝³ : Ring A
inst✝² : Algebra R S
inst✝¹ : Algebra R A
inst✝ : Algebra S A
a : A
f : S → R
h₁ : Function.LeftInverse f ⇑(algebraMap R S)
h₂ : Set.RightInvOn f (⇑(algebraMap R S)) (spectrum S a)
hx : 0 ∈ quasispectrum S a
⊢ (algebraMap R S) (f 0) = 0

case inr
R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁵ : Semifield R
inst✝⁴ : Semifield S
inst✝³ : Ring A
inst✝² : Algebra R S
inst✝¹ : Algebra R A
inst✝ : Algebra S A
a : A
f : S → R
h₁ : Function.LeftInverse f ⇑(algebraMap R S)
h₂ : Set.RightInvOn f (⇑(algebraMap R S)) (spectrum S a)
x : S
hx✝ : x ∈ quasispectrum S a
hx : x ∈ spectrum S a
⊢ (algebraMap R S) (f x) = x
Module: Mathlib.Algebra.Group.Pi.Units

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
x : (i : ι) → M i
⊢ (∃ b, (∀ (x_1 : ι), (x * b) x_1 = 1 x_1) ∧ ∀ (x_1 : ι), (b * x) x_1 = 1 x_1) ↔
    ∀ (i : ι), ∃ b, x i * b = 1 ∧ b * x i = 1

Tactic:
← forall_and

Goal state after:
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
x : (i : ι) → M i
⊢ (∃ b, ∀ (x_1 : ι), (x * b) x_1 = 1 x_1 ∧ (b * x) x_1 = 1 x_1) ↔ ∀ (i : ι), ∃ b, x i * b = 1 ∧ b * x i = 1
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
⊢ s • (inl r✝ + ↑a✝) = inl ((algebraMap S R) s) * inl r✝ + inl ((algebraMap S R) s) * ↑a✝

Tactic:
smul_add,

Goal state after:
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
⊢ s • inl r✝ + s • ↑a✝ = inl ((algebraMap S R) s) * inl r✝ + inl ((algebraMap S R) s) * ↑a✝
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
h_le_iff : ∀ (x y : R), x ≤ y ↔ ∃ s, y = x + star s * s
x y : R
h : x ≤ y
p : R
hp : y = x + star p * p
⊢ ∃ p ∈ AddSubmonoid.closure (range fun s ↦ star s * s), y = x + p

Tactic:
exact ⟨star p * p, AddSubmonoid.subset_closure ⟨p, rfl⟩, hp⟩

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

Goal state before:
pp: case refine_2.refine_2
R : Type u_1
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
h_le_iff : ∀ (x y : R), x ≤ y ↔ ∃ s, y = x + star s * s
p : R
hp : p ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
⊢ ∀ (x y : R),
    x ∈ AddSubmonoid.closure (range fun s ↦ star s * s) →
      y ∈ AddSubmonoid.closure (range fun s ↦ star s * s) →
        (∀ (x_1 y : R), y = x_1 + x → x_1 ≤ y) →
          (∀ (x y_1 : R), y_1 = x + y → x ≤ y_1) → ∀ (x_1 y_1 : R), y_1 = x_1 + (x + y) → x_1 ≤ y_1

Tactic:
· rintro _ _ _ _ ha hb x y rfl
        rw [← add_assoc]
        exact (ha _ _ rfl).trans (hb _ _ rfl)

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

Goal state before:
pp: R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
S T : NonUnitalStarSubalgebra R A
⊢ ∀ {x : A}, x ∈ T → x ∈ S ⊔ T

Tactic:
rw [← SetLike.le_def]
  exact le_sup_right

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : StrongRankCondition R
inst✝² : Module.Finite R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
⊢ 0 < finrank R M ↔ Nontrivial M

Tactic:
rw [← rank_pos_iff_nontrivial (R := R), ← finrank_eq_rank]
  norm_cast

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
⊢ finrank R M = 0 ↔ ∀ (x : M), ∃ a, a ≠ 0 ∧ a • x = 0

Tactic:
← rank_eq_zero_iff (R := R),

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
⊢ finrank R M = 0 ↔ Module.rank R M = 0