mathlib-initiative/mathlib-tactics huggingface dataset:
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_6
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₂
inst✝ : Finite m
v₁ : Basis n R R
v₂ : Basis m R M₂
x : M₂
⊢ (toMatrix v₁ v₂) (toSpanSingleton R M₂ x) = vecMulVec ⇑(v₂.repr x) ⇑v₁

Tactic:
ext

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_6
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₂
inst✝ : Finite m
v₁ : Basis n R R
v₂ : Basis m R M₂
x : M₂
i✝ : m
j✝ : n
⊢ (toMatrix v₁ v₂) (toSpanSingleton R M₂ x) i✝ j✝ = vecMulVec (⇑(v₂.repr x)) (⇑v₁) i✝ j✝
Module: Mathlib.RingTheory.OreLocalization.Basic

Goal state before:
pp: case e_s
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : DistribMulAction R X
r : X
s : ↥S
r' : X
s' : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s = ra * ↑s'
ha' : r /ₒ s + r' /ₒ s' = (sa • r + ra • r') /ₒ (sa * s)
⊢ sa * s = ⟨ra * ↑s', ⋯⟩

Tactic:
ext

Goal state after:
case e_s
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : DistribMulAction R X
r : X
s : ↥S
r' : X
s' : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s = ra * ↑s'
ha' : r /ₒ s + r' /ₒ s' = (sa • r + ra • r') /ₒ (sa * s)
⊢ ↑(sa * s) = ↑⟨ra * ↑s', ⋯⟩
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₁
x : R
⊢ (toMatrix v₁ v₁) (DistribSMul.toLinearMap R M₁ x) = Matrix.diagonal fun x_1 ↦ x

Tactic:
ext

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₁
x : R
i✝ j✝ : n
⊢ (toMatrix v₁ v₁) (DistribSMul.toLinearMap R M₁ x) i✝ j✝ = Matrix.diagonal (fun x_1 ↦ x) i✝ j✝
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
m : Type u_3
inst✝¹ : Fintype m
inst✝ : DecidableEq m
b : Basis m R S
r : R
⊢ (toMatrix b b) ((lmul R S) ((algebraMap R S) r)) = (algebraMap R (Matrix m m R)) r

Tactic:
ext

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
m : Type u_3
inst✝¹ : Fintype m
inst✝ : DecidableEq m
b : Basis m R S
r : R
i✝ j✝ : m
⊢ (toMatrix b b) ((lmul R S) ((algebraMap R S) r)) i✝ j✝ = (algebraMap R (Matrix m m R)) r i✝ j✝
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring S
inst✝⁶ : Algebra R S
m : Type u_3
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq m
b : Basis m R S
G : Type u_4
inst✝³ : Group G
inst✝² : DistribMulAction G S
inst✝¹ : SMulCommClass G R S
inst✝ : SMulCommClass G S S
g : G
x : S
⊢ (leftMulMatrix (g • b)) x = (leftMulMatrix b) x

Tactic:
ext

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring S
inst✝⁶ : Algebra R S
m : Type u_3
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq m
b : Basis m R S
G : Type u_4
inst✝³ : Group G
inst✝² : DistribMulAction G S
inst✝¹ : SMulCommClass G R S
inst✝ : SMulCommClass G S S
g : G
x : S
i✝ j✝ : m
⊢ (leftMulMatrix (g • b)) x i✝ j✝ = (leftMulMatrix b) x i✝ j✝
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommSemiring R
m : Type u_3
inst✝⁹ : Fintype m
inst✝⁸ : DecidableEq m
A : Type u_4
M : Type u_5
n : Type u_6
inst✝⁷ : Fintype n
inst✝⁶ : DecidableEq n
inst✝⁵ : CommSemiring A
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module A M
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A M
bA : Basis m R A
bM : Basis n A M
f : M →ₗ[A] M
⊢ (toMatrix (bA.smulTower' bM) (bA.smulTower' bM)) (↑R f) =
    (Matrix.comp n n m m R) (((toMatrix bM bM) f).map ⇑(leftMulMatrix bA))

Tactic:
ext

Goal state after:
R : Type u_1
inst✝¹⁰ : CommSemiring R
m : Type u_3
inst✝⁹ : Fintype m
inst✝⁸ : DecidableEq m
A : Type u_4
M : Type u_5
n : Type u_6
inst✝⁷ : Fintype n
inst✝⁶ : DecidableEq n
inst✝⁵ : CommSemiring A
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module A M
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A M
bA : Basis m R A
bM : Basis n A M
f : M →ₗ[A] M
i✝ j✝ : n × m
⊢ (toMatrix (bA.smulTower' bM) (bA.smulTower' bM)) (↑R f) i✝ j✝ =
    (Matrix.comp n n m m R) (((toMatrix bM bM) f).map ⇑(leftMulMatrix bA)) i✝ j✝
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: ι : Type u_1
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
R : Type u_2
inst✝⁶ : CommSemiring R
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
m : Matrix ι ι (End A M)
x✝ y✝ : ι → M
⊢ (fun i ↦ ∑ j, (m i j) ((x✝ + y✝) j)) = (fun i ↦ ∑ j, (m i j) (x✝ j)) + fun i ↦ ∑ j, (m i j) (y✝ j)

Tactic:
ext

Goal state after:
ι : Type u_1
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
R : Type u_2
inst✝⁶ : CommSemiring R
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
m : Matrix ι ι (End A M)
x✝¹ y✝ : ι → M
x✝ : ι
⊢ ∑ j, (m x✝ j) ((x✝¹ + y✝) j) = ((fun i ↦ ∑ j, (m i j) (x✝¹ j)) + fun i ↦ ∑ j, (m i j) (y✝ j)) x✝
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: ι : Type u_1
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
R : Type u_2
inst✝⁶ : CommSemiring R
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
m : Matrix ι ι (End A M)
m✝ : A
x✝ : ι → M
⊢ (fun i ↦ ∑ j, (m i j) ((m✝ • x✝) j)) = (RingHom.id A) m✝ • fun i ↦ ∑ j, (m i j) (x✝ j)

Tactic:
ext

Goal state after:
ι : Type u_1
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
R : Type u_2
inst✝⁶ : CommSemiring R
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
m : Matrix ι ι (End A M)
m✝ : A
x✝¹ : ι → M
x✝ : ι
⊢ ∑ j, (m x✝ j) ((m✝ • x✝¹) j) = ((RingHom.id A) m✝ • fun i ↦ ∑ j, (m i j) (x✝¹ j)) x✝
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: ι : Type u_1
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
R : Type u_2
inst✝⁶ : CommSemiring R
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
m : Matrix ι ι (End A M)
⊢ (fun f i j ↦ { toFun := fun x ↦ f (Pi.single j x) i, map_add' := ⋯, map_smul' := ⋯ })
      ((fun m ↦ { toFun := fun x i ↦ ∑ j, (m i j) (x j), map_add' := ⋯, map_smul' := ⋯ }) m) =
    m

Tactic:
ext

Goal state after:
ι : Type u_1
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
R : Type u_2
inst✝⁶ : CommSemiring R
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
m : Matrix ι ι (End A M)
i✝ j✝ : ι
x✝ : M
⊢ ((fun f i j ↦ { toFun := fun x ↦ f (Pi.single j x) i, map_add' := ⋯, map_smul' := ⋯ })
        ((fun m ↦ { toFun := fun x i ↦ ∑ j, (m i j) (x j), map_add' := ⋯, map_smul' := ⋯ }) m) i✝ j✝)
      x✝ =
    (m i✝ j✝) x✝
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: ι : Type u_1
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
R : Type u_2
inst✝⁶ : CommSemiring R
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
f g : End A (ι → M)
⊢ (fun i j ↦ { toFun := fun x ↦ (f * g) (Pi.single j x) i, map_add' := ⋯, map_smul' := ⋯ }) =
    (fun i j ↦ { toFun := fun x ↦ f (Pi.single j x) i, map_add' := ⋯, map_smul' := ⋯ }) * fun i j ↦
      { toFun := fun x ↦ g (Pi.single j x) i, map_add' := ⋯, map_smul' := ⋯ }

Tactic:
ext

Goal state after:
ι : Type u_1
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
R : Type u_2
inst✝⁶ : CommSemiring R
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
f g : End A (ι → M)
i✝ j✝ : ι
x✝ : M
⊢ { toFun := fun x ↦ (f * g) (Pi.single j✝ x) i✝, map_add' := ⋯, map_smul' := ⋯ } x✝ =
    (((fun i j ↦ { toFun := fun x ↦ f (Pi.single j x) i, map_add' := ⋯, map_smul' := ⋯ }) * fun i j ↦
          { toFun := fun x ↦ g (Pi.single j x) i, map_add' := ⋯, map_smul' := ⋯ })
        i✝ j✝)
      x✝
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
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
i : Fin n
c : Fin n →₀ R
hm : (c.sum fun i x ↦ x • ↑(snf.bN i)) ∈ N
⊢ ⟨c.sum fun i t ↦ t • ↑(snf.bN i), hm⟩ = c.sum fun i t ↦ t • ⟨↑(snf.bN i), ⋯⟩

Tactic:
ext

Goal state after:
ι : Type u_1
R : Type u_2
inst✝² : CommRing R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
i : Fin n
c : Fin n →₀ R
hm : (c.sum fun i x ↦ x • ↑(snf.bN i)) ∈ N
⊢ ↑⟨c.sum fun i t ↦ t • ↑(snf.bN i), hm⟩ = ↑(c.sum fun i t ↦ t • ⟨↑(snf.bN i), ⋯⟩)
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: ι : Type u_1
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
R : Type u_2
inst✝⁶ : CommSemiring R
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
f g : End A (ι → M)
⊢ (fun i j ↦ { toFun := fun x ↦ (f + g) (Pi.single j x) i, map_add' := ⋯, map_smul' := ⋯ }) =
    (fun i j ↦ { toFun := fun x ↦ f (Pi.single j x) i, map_add' := ⋯, map_smul' := ⋯ }) + fun i j ↦
      { toFun := fun x ↦ g (Pi.single j x) i, map_add' := ⋯, map_smul' := ⋯ }

Tactic:
ext

Goal state after:
ι : Type u_1
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
R : Type u_2
inst✝⁶ : CommSemiring R
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
f g : End A (ι → M)
i✝ j✝ : ι
x✝ : M
⊢ { toFun := fun x ↦ (f + g) (Pi.single j✝ x) i✝, map_add' := ⋯, map_smul' := ⋯ } x✝ =
    (((fun i j ↦ { toFun := fun x ↦ f (Pi.single j x) i, map_add' := ⋯, map_smul' := ⋯ }) + fun i j ↦
          { toFun := fun x ↦ g (Pi.single j x) i, map_add' := ⋯, map_smul' := ⋯ })
        i✝ j✝)
      x✝
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: ι : Type u_1
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
R : Type u_2
inst✝⁶ : CommSemiring R
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
r : R
⊢ (endVecRingEquivMatrixEnd ι A M).toFun ((algebraMap R (End A (ι → M))) r) = (algebraMap R (Matrix ι ι (End A M))) r

Tactic:
ext

Goal state after:
ι : Type u_1
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
R : Type u_2
inst✝⁶ : CommSemiring R
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
r : R
i✝ j✝ : ι
x✝ : M
⊢ ((endVecRingEquivMatrixEnd ι A M).toFun ((algebraMap R (End A (ι → M))) r) i✝ j✝) x✝ =
    ((algebraMap R (Matrix ι ι (End A M))) r i✝ j✝) x✝
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: case refine_2
A : Type u_3
inst✝ : Semiring A
h : ∀ (n : ℕ) (f : End A (Fin n → A)), Surjective ⇑f → Injective ⇑f
n : ℕ
f g : End A (Fin n → A)
eq : f * g = 1
surj : Surjective ⇑f
this : ↑(LinearEquiv.ofBijective f ⋯).symm ∘ₗ ↑(LinearEquiv.ofBijective f ⋯) = LinearMap.id
⊢ g * f = 1

Tactic:
rwa [← left_inv_eq_right_inv this eq]

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

Goal state before:
pp: A : Type u_3
inst✝ : Semiring A
⊢ IsStablyFiniteRing A ↔ ∀ (n : ℕ) (f : End A (Fin n → A)), Surjective ⇑f → Injective ⇑f

Tactic:
by
  simp_rw [isStablyFiniteRing_iff_isDedekindFiniteMonoid_moduleEnd, isDedekindFiniteMonoid_iff]
  refine ⟨fun h n f surj ↦ ?_, fun h n f g eq ↦ ?_⟩
  · have ⟨g, eq⟩ := Module.projective_lifting_property _ .id surj
    exact injective_of_comp_eq_id _ _ (h _ eq)
  · have surj := surjective_of_comp_eq_id _ _ eq
    have := (LinearEquiv.ofBijective f ⟨h _ _ surj, surj⟩).symm_comp
    rwa [← left_inv_eq_right_inv this eq]

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

Goal state before:
pp: case e_6
ι : Type u_1
R : Type u_2
inst✝⁴ : CommRing R
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : M →ₗ[R] M
hf : ∀ (x : M), f x ∈ N
hf' : ∀ x ∈ N, f x ∈ N
i : Fin n
⊢ (f.restrict hf') (snf.bN i) = snf.a i • ⟨f (snf.bM (snf.f i)), ⋯⟩

Tactic:
ext

Goal state after:
case e_6
ι : Type u_1
R : Type u_2
inst✝⁴ : CommRing R
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : M →ₗ[R] M
hf : ∀ (x : M), f x ∈ N
hf' : ∀ x ∈ N, f x ∈ N
i : Fin n
⊢ ↑((f.restrict hf') (snf.bN i)) = ↑(snf.a i • ⟨f (snf.bM (snf.f i)), ⋯⟩)
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 O : Submodule R M
N_le_O : N ≤ O
n o : ℕ
hno : n ≤ o
bO : Basis (Fin o) R ↥O
bN : Basis (Fin n) R ↥N
a : Fin n → R
snf : ∀ (i : Fin n), ↑(bN i) = a i • ↑(bO (Fin.castLE hno i))
i : Fin n
⊢ ↑((bN.map (comapSubtypeEquivOfLe N_le_O).symm) i) = a i • bO ((Fin.castLEEmb hno) i)

Tactic:
ext

Goal state after:
ι : 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 O : Submodule R M
N_le_O : N ≤ O
n o : ℕ
hno : n ≤ o
bO : Basis (Fin o) R ↥O
bN : Basis (Fin n) R ↥N
a : Fin n → R
snf : ∀ (i : Fin n), ↑(bN i) = a i • ↑(bO (Fin.castLE hno i))
i : Fin n
⊢ ↑↑((bN.map (comapSubtypeEquivOfLe N_le_O).symm) i) = ↑(a i • bO ((Fin.castLEEmb hno) i))
Module: Mathlib.Algebra.Star.TensorProduct

Goal state before:
pp: case e'_2.e'_21
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : AddCommMonoid A
inst✝⁶ : StarAddMonoid A
inst✝⁵ : Module R A
inst✝⁴ : StarModule R A
inst✝³ : AddCommMonoid B
inst✝² : StarAddMonoid B
inst✝¹ : Module R B
inst✝ : StarModule R B
x : A ⊗[R] B
⊢ (starLinearEquiv R).trans (starLinearEquiv R) = LinearEquiv.refl R A

Tactic:
ext

Goal state after:
case e'_2.e'_21
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : AddCommMonoid A
inst✝⁶ : StarAddMonoid A
inst✝⁵ : Module R A
inst✝⁴ : StarModule R A
inst✝³ : AddCommMonoid B
inst✝² : StarAddMonoid B
inst✝¹ : Module R B
inst✝ : StarModule R B
x : A ⊗[R] B
x✝ : A
⊢ ((starLinearEquiv R).trans (starLinearEquiv R)) x✝ = (LinearEquiv.refl R A) x✝
Module: Mathlib.Algebra.Star.TensorProduct

Goal state before:
pp: case e'_2.e'_22
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : AddCommMonoid A
inst✝⁶ : StarAddMonoid A
inst✝⁵ : Module R A
inst✝⁴ : StarModule R A
inst✝³ : AddCommMonoid B
inst✝² : StarAddMonoid B
inst✝¹ : Module R B
inst✝ : StarModule R B
x : A ⊗[R] B
⊢ (starLinearEquiv R).trans (starLinearEquiv R) = LinearEquiv.refl R B

Tactic:
ext

Goal state after:
case e'_2.e'_22
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : AddCommMonoid A
inst✝⁶ : StarAddMonoid A
inst✝⁵ : Module R A
inst✝⁴ : StarModule R A
inst✝³ : AddCommMonoid B
inst✝² : StarAddMonoid B
inst✝¹ : Module R B
inst✝ : StarModule R B
x : A ⊗[R] B
x✝ : B
⊢ ((starLinearEquiv R).trans (starLinearEquiv R)) x✝ = (LinearEquiv.refl R B) x✝
Module: Mathlib.Algebra.Algebra.Subalgebra.Prod

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
⊢ ⊤.prod ⊤ = ⊤

Tactic:
ext

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
x✝ : A × B
⊢ x✝ ∈ ⊤.prod ⊤ ↔ x✝ ∈ ⊤
Module: Mathlib.RingTheory.Localization.Basic

Goal state before:
pp: case refine_1.inr
ι : Type u_1
R : ι → Type u_2
inst✝ : (i : ι) → CommSemiring (R i)
i : ι
S : Submonoid (R i)
T : Submonoid ((i : ι) → R i) := Submonoid.comap (Pi.evalRingHom R i) S
r₁ : (i : ι) → R i
s₁ : ↥T
r₂ : (i : ι) → R i
s₂ : ↥T
s : ↥S
hs :
  ↑s * (↑⟨(Pi.evalRingHom R i) ↑s₂, ⋯⟩ * (Pi.evalRingHom R i) r₁) =
    ↑s * (↑⟨(Pi.evalRingHom R i) ↑s₁, ⋯⟩ * (Pi.evalRingHom R i) r₂)
j : ι
ne : j ≠ i
⊢ (↑⟨update 0 i ↑s, ⋯⟩ * (↑s₂ * r₁)) j = (↑⟨update 0 i ↑s, ⋯⟩ * (↑s₁ * r₂)) j

Tactic:
· simp [update_of_ne ne]

Goal state after:
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
inst✝³ : IsLocalization M S
Q : Type u_4
inst✝² : CommSemiring Q
inst✝¹ : Algebra R Q
inst✝ : IsLocalization M Q
f : S →+* Q
hf : f.comp (algebraMap R S) = algebraMap R Q
⊢ algebraMap R Q = (↑(algEquiv M S Q)).comp (algebraMap R S)

Tactic:
ext

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
Q : Type u_4
inst✝² : CommSemiring Q
inst✝¹ : Algebra R Q
inst✝ : IsLocalization M Q
f : S →+* Q
hf : f.comp (algebraMap R S) = algebraMap R Q
x✝ : R
⊢ (algebraMap R Q) x✝ = ((↑(algEquiv M S Q)).comp (algebraMap R S)) x✝
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
P : Type u_3
inst✝² : CommSemiring P
inst✝¹ : Algebra R P
inst✝ : IsLocalization M S
h : S ≃ₐ[R] P
⊢ IsLocalization M P

Tactic:
constructor

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✝¹ : Algebra R P
inst✝ : IsLocalization M S
h : S ≃ₐ[R] P
⊢ M.IsLocalizationMap ⇑(algebraMap R P)
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
P : Type u_3
inst✝² : CommSemiring P
inst✝¹ : Algebra R P
inst✝ : IsLocalization M S
h : S ≃ₐ[R] P
⊢ M.IsLocalizationMap ⇑(algebraMap R P)

Tactic:
constructor

Goal state after:
case map_units
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✝¹ : Algebra R P
inst✝ : IsLocalization M S
h : S ≃ₐ[R] P
⊢ ∀ (y : ↥M), IsUnit ((algebraMap R P) ↑y)

case surj
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✝¹ : Algebra R P
inst✝ : IsLocalization M S
h : S ≃ₐ[R] P
⊢ ∀ (z : P), ∃ x, z * (algebraMap R P) ↑x.2 = (algebraMap R P) x.1

case exists_of_eq
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✝¹ : Algebra R P
inst✝ : IsLocalization M S
h : S ≃ₐ[R] P
⊢ ∀ {x y : R}, (algebraMap R P) x = (algebraMap R P) y → ∃ c, ↑c * x = ↑c * y
Module: Mathlib.RingTheory.Localization.Defs

Goal state before:
pp: case e_f
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)
T : Submonoid P
Q : Type u_4
inst✝² : CommSemiring Q
inst✝¹ : Algebra P Q
inst✝ : IsLocalization T Q
h : R ≃+* P
H : Submonoid.map h.toMonoidHom M = T
⊢ h.symm.toMonoidHom.comp h.toMonoidHom = MonoidHom.id R

Tactic:
ext

Goal state after:
case e_f
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)
T : Submonoid P
Q : Type u_4
inst✝² : CommSemiring Q
inst✝¹ : Algebra P Q
inst✝ : IsLocalization T Q
h : R ≃+* P
H : Submonoid.map h.toMonoidHom M = T
x✝ : R
⊢ (h.symm.toMonoidHom.comp h.toMonoidHom) x✝ = (MonoidHom.id R) x✝
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
h : R ≃+* P
this : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
⊢ IsLocalization (Submonoid.map h M) S

Tactic:
constructor

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
h : R ≃+* P
this : Algebra P S := ⋯
⊢ (Submonoid.map h M).IsLocalizationMap ⇑(algebraMap P S)
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
h : R ≃+* P
this : Algebra P S := ⋯
⊢ (Submonoid.map h M).IsLocalizationMap ⇑(algebraMap P S)

Tactic:
constructor

Goal state after:
case map_units
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
h : R ≃+* P
this : Algebra P S := ⋯
⊢ ∀ (y : ↥(Submonoid.map h M)), IsUnit ((algebraMap P S) ↑y)

case surj
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
h : R ≃+* P
this : Algebra P S := ⋯
⊢ ∀ (z : S), ∃ x, z * (algebraMap P S) ↑x.2 = (algebraMap P S) x.1

case exists_of_eq
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
h : R ≃+* P
this : Algebra P S := ⋯
⊢ ∀ {x y : P}, (algebraMap P S) x = (algebraMap P S) y → ∃ c, ↑c * x = ↑c * y
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
s : Set L
hs : g.range = Subring.closure s
⊢ Subfield.closure ↑(Subring.closure s) = Subfield.closure s

Tactic:
ext

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
s : Set L
hs : g.range = Subring.closure s
x✝ : L
⊢ x✝ ∈ Subfield.closure ↑(Subring.closure s) ↔ x✝ ∈ Subfield.closure s
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: A : Type u_4
inst✝⁴ : CommRing A
K : Type u_5
inst✝³ : Field K
L : Type u_7
inst✝² : Field L
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
g : A →+* L
hg : Injective ⇑g
⊢ (lift hg).comp (algebraMap A K) = g

Tactic:
ext

Goal state after:
A : Type u_4
inst✝⁴ : CommRing A
K : Type u_5
inst✝³ : Field K
L : Type u_7
inst✝² : Field L
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
g : A →+* L
hg : Injective ⇑g
x✝ : A
⊢ ((lift hg).comp (algebraMap A K)) x✝ = g x✝