mathlib-initiative/mathlib-tactics huggingface dataset:
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₁
inst✝⁶ : DecidableEq ι₁
M₁ : ι₁ → Type w₁
M₂' : Type w₂'
inst✝⁵ : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)
inst✝⁴ : AddCommMonoid M₂'
inst✝³ : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝² : Module R M₂'
inst✝¹ : (i₁ : ι₁) → Module S (M₁ i₁)
inst✝ : ∀ (i₁ : ι₁), IsScalarTower R S (M₁ i₁)
i : ι₁
x : M₁ i ⊗[R] M₂'
⊢ (directSumLeft R S M₁ M₂').symm ((of (fun i ↦ M₁ i ⊗[R] M₂') i) x) = (rTensor M₂' (lof R ι₁ M₁ i)) x

Tactic:
by
  induction x using TensorProduct.induction_on with
  | zero => simp
  | tmul x y => rw [← lof_eq_of S, directSumLeft_symm_lof_tmul, rTensor_tmul, lof_eq_of, lof_eq_of]
  | add x y h₁ h₂ => simp [h₁, h₂]

Goal state after:
Module: Mathlib.Data.Matrix.Composition

Goal state before:
pp: I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
inst✝⁴ : DecidableEq I
inst✝³ : DecidableEq J
inst✝² : DecidableEq K
inst✝¹ : DecidableEq L
inst✝ : Zero R
i : I
j : J
k : K
l : L
r : R
i' : I
k' : K
j' : J
l' : L
⊢ (comp I J K L R) (single i j (single k l r)) (i', k') (j', l') = single (i, k) (j, l) r (i', k') (j', l')

Tactic:
dsimp [comp_apply]

Goal state after:
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
inst✝⁴ : DecidableEq I
inst✝³ : DecidableEq J
inst✝² : DecidableEq K
inst✝¹ : DecidableEq L
inst✝ : Zero R
i : I
j : J
k : K
l : L
r : R
i' : I
k' : K
j' : J
l' : L
⊢ single i j (single k l r) i' j' k' l' = single (i, k) (j, l) r (i', k') (j', l')
Module: Mathlib.Data.Matrix.Composition

Goal state before:
pp: I : Type u_1
J : Type u_2
R : Type u_5
inst✝² : DecidableEq I
inst✝¹ : DecidableEq J
inst✝ : Zero R
d : I → J → R
i₁ : I
j₁ : J
i₂ : I
j₂ : J
⊢ (comp I I J J R) (diagonal fun i ↦ diagonal fun j ↦ d i j) (i₁, j₁) (i₂, j₂) =
    diagonal (fun ij ↦ d ij.1 ij.2) (i₁, j₁) (i₂, j₂)

Tactic:
dsimp [comp_apply]

Goal state after:
I : Type u_1
J : Type u_2
R : Type u_5
inst✝² : DecidableEq I
inst✝¹ : DecidableEq J
inst✝ : Zero R
d : I → J → R
i₁ : I
j₁ : J
i₂ : I
j₂ : J
⊢ diagonal (fun i ↦ diagonal fun j ↦ d i j) i₁ i₂ j₁ j₂ = diagonal (fun ij ↦ d ij.1 ij.2) (i₁, j₁) (i₂, j₂)
Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : AddMonoid α
inst✝ : StarAddMonoid α
M : Matrix m n α
⊢ Mᴴ = 0 ↔ Mᴴ = 0ᴴ

Tactic:
conjTranspose_zero

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : AddMonoid α
inst✝ : StarAddMonoid α
M : Matrix m n α
⊢ Mᴴ = 0 ↔ Mᴴ = 0
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: case succ
R : Type u_1
inst✝² : CommSemiring R
n✝ : Type u_5
inst✝¹ : DecidableEq n✝
inst✝ : Fintype n✝
M : Matrix n✝ n✝ R
n : ℕ
ih : toLin' (M ^ n) = toLin' M ^ n
⊢ toLin' (M ^ (n + 1)) = toLin' M ^ (n + 1)

Tactic:
pow_succ,

Goal state after:
case succ
R : Type u_1
inst✝² : CommSemiring R
n✝ : Type u_5
inst✝¹ : DecidableEq n✝
inst✝ : Fintype n✝
M : Matrix n✝ n✝ R
n : ℕ
ih : toLin' (M ^ n) = toLin' M ^ n
⊢ toLin' (M ^ n * M) = toLin' M ^ (n + 1)
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: case succ
R : Type u_1
inst✝² : CommSemiring R
n✝ : Type u_5
inst✝¹ : DecidableEq n✝
inst✝ : Fintype n✝
M : Matrix n✝ n✝ R
n : ℕ
ih : toLin' (M ^ n) = toLin' M ^ n
⊢ toLin' (M ^ n * M) = toLin' M ^ (n + 1)

Tactic:
pow_succ,

Goal state after:
case succ
R : Type u_1
inst✝² : CommSemiring R
n✝ : Type u_5
inst✝¹ : DecidableEq n✝
inst✝ : Fintype n✝
M : Matrix n✝ n✝ R
n : ℕ
ih : toLin' (M ^ n) = toLin' M ^ n
⊢ toLin' (M ^ n * M) = toLin' M ^ n * toLin' M
Module: Mathlib.Algebra.Field.Subfield.Basic

Goal state before:
pp: K✝ : Type u
L : Type v
M : Type w
inst✝³ : DivisionRing K✝
inst✝² : DivisionRing L
inst✝¹ : DivisionRing M
s✝¹ : Set K✝
K : Type u
inst✝ : Field K
s✝ : Subfield K
s : Set K
x : K
⊢ x ∈ {z | ∃ x ∈ Subring.closure s, ∃ y ∈ Subring.closure s, x / y = z} →
    x⁻¹ ∈ {z | ∃ x ∈ Subring.closure s, ∃ y ∈ Subring.closure s, x / y = z}

Tactic:
by rintro ⟨y, hy, z, hz, x_eq⟩; exact ⟨z, hz, y, hy, x_eq ▸ (inv_div _ _).symm⟩

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

Goal state before:
pp: case succ
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₁
f : M₁ →ₗ[R] M₁
k : ℕ
ih : (toMatrix v₁ v₁) f ^ k = (toMatrix v₁ v₁) (f ^ k)
⊢ (toMatrix v₁ v₁) f ^ (k + 1) = (toMatrix v₁ v₁) (f ^ (k + 1))

Tactic:
pow_succ,

Goal state after:
case succ
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₁
f : M₁ →ₗ[R] M₁
k : ℕ
ih : (toMatrix v₁ v₁) f ^ k = (toMatrix v₁ v₁) (f ^ k)
⊢ (toMatrix v₁ v₁) f ^ k * (toMatrix v₁ v₁) f = (toMatrix v₁ v₁) (f ^ (k + 1))
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: case succ
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₁
f : M₁ →ₗ[R] M₁
k : ℕ
ih : (toMatrix v₁ v₁) f ^ k = (toMatrix v₁ v₁) (f ^ k)
⊢ (toMatrix v₁ v₁) f ^ k * (toMatrix v₁ v₁) f = (toMatrix v₁ v₁) (f ^ (k + 1))

Tactic:
pow_succ,

Goal state after:
case succ
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₁
f : M₁ →ₗ[R] M₁
k : ℕ
ih : (toMatrix v₁ v₁) f ^ k = (toMatrix v₁ v₁) (f ^ k)
⊢ (toMatrix v₁ v₁) f ^ k * (toMatrix v₁ v₁) f = (toMatrix v₁ v₁) (f ^ k * f)
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: case succ
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₁
A : Matrix n✝ n✝ R
n : ℕ
ih : (toLin v₁ v₁) (A ^ n) = (toLin v₁ v₁) A ^ n
⊢ (toLin v₁ v₁) (A ^ (n + 1)) = (toLin v₁ v₁) A ^ (n + 1)

Tactic:
pow_succ,

Goal state after:
case succ
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₁
A : Matrix n✝ n✝ R
n : ℕ
ih : (toLin v₁ v₁) (A ^ n) = (toLin v₁ v₁) A ^ n
⊢ (toLin v₁ v₁) (A ^ n * A) = (toLin v₁ v₁) A ^ (n + 1)
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: case succ
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₁
A : Matrix n✝ n✝ R
n : ℕ
ih : (toLin v₁ v₁) (A ^ n) = (toLin v₁ v₁) A ^ n
⊢ (toLin v₁ v₁) (A ^ n * A) = (toLin v₁ v₁) A ^ (n + 1)

Tactic:
pow_succ,

Goal state after:
case succ
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₁
A : Matrix n✝ n✝ R
n : ℕ
ih : (toLin v₁ v₁) (A ^ n) = (toLin v₁ v₁) A ^ n
⊢ (toLin v₁ v₁) (A ^ n * A) = (toLin v₁ v₁) A ^ n * (toLin v₁ v₁) A
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
i✝ j✝ : m
⊢ Matrix.diagonal (fun x ↦ r) i✝ j✝ = Matrix.diagonal ((algebraMap R (m → R)) r) i✝ j✝

Tactic:
Pi.algebraMap_def,

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
⊢ Matrix.diagonal (fun x ↦ r) i✝ j✝ = Matrix.diagonal (fun i ↦ (algebraMap R R) r) i✝ j✝
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✝³ : IsPrincipalIdealRing R
inst✝² : IsDomain R
S : Type u_4
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal S
hI₁ : Module.Finite R ↥I
hI₂ : IsTorsionFree R ↥I
this✝ : Module.Finite R ↥(restrictScalars R I)
this : IsTorsionFree R ↥(restrictScalars R I)
⊢ Free R ↥(restrictScalars R I)

Tactic:
exact Module.free_of_finite_type_torsion_free'

Goal state after:
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
T : Submonoid P
Q : Type u_4
inst✝⁶ : CommSemiring Q
inst✝⁵ : Algebra P Q
inst✝⁴ : IsLocalization T Q
hy : M ≤ Submonoid.comap g T
A : Type u_5
inst✝³ : CommSemiring A
U : Submonoid A
W : Type u_6
inst✝² : CommSemiring W
inst✝¹ : Algebra A W
inst✝ : IsLocalization U W
l : P →+* A
hl : T ≤ Submonoid.comap l U
x : S
⊢ (map W l hl) ((map Q g hy) x) = (map W (l.comp g) ⋯) x

Tactic:
rw [← map_comp_map (Q := Q) hy hl]; rfl

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

Goal state before:
pp: 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 := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
y : S
⊢ ∃ x, y * (algebraMap P S) ↑x.2 = (algebraMap P S) x.1

Tactic:
obtain ⟨⟨x, s⟩, e⟩ := IsLocalization.surj M y

Goal state after:
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 := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
y : S
x : R
s : ↥M
e : y * (algebraMap R S) ↑(x, s).2 = (algebraMap R S) (x, s).1
⊢ ∃ x, y * (algebraMap P S) ↑x.2 = (algebraMap P S) x.1
Module: Mathlib.RingTheory.Localization.Basic

Goal state before:
pp: 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
x y : S₁
r s : R
d : ↥M₁
hr : x * (algebraMap R S₁) ↑d = (algebraMap R S₁) r
hs : y * (algebraMap R S₁) ↑d = (algebraMap R S₁) s
hxy : (algebraMap S₂ T) ((algebraMap R S₂) r) = (algebraMap S₂ T) ((algebraMap R S₂) s)
c : R
hmc : c ∈ ↑M₁
hc : ↑⟨(algebraMap R S₂) c, ⋯⟩ * (algebraMap R S₂) r = ↑⟨(algebraMap R S₂) c, ⋯⟩ * (algebraMap R S₂) s
⊢ ∃ c, ↑c * x = ↑c * y

Tactic:
simp_rw [← map_mul] at hc

Goal state after:
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
x y : S₁
r s : R
d : ↥M₁
hr : x * (algebraMap R S₁) ↑d = (algebraMap R S₁) r
hs : y * (algebraMap R S₁) ↑d = (algebraMap R S₁) s
hxy : (algebraMap S₂ T) ((algebraMap R S₂) r) = (algebraMap S₂ T) ((algebraMap R S₂) s)
c : R
hmc : c ∈ ↑M₁
hc : (algebraMap R S₂) (c * r) = (algebraMap R S₂) (c * s)
⊢ ∃ c, ↑c * x = ↑c * y
Module: Mathlib.RingTheory.Localization.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Semiring A
inst✝⁹ : Semiring B
S : Type u_4
inst✝⁸ : CommSemiring S
inst✝⁷ : Algebra R S
M : Submonoid R
inst✝⁶ : IsLocalization M S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[R] B
⊢ ∀ (r : S), (↑↑f.toRingHom).toFun ((algebraMap S A) r) = (algebraMap S B) r

Tactic:
by
    let f := f.comp (IsScalarTower.toAlgHom R S A)
    let g := IsScalarTower.toAlgHom R S B
    have : f.toRingHom.comp (algebraMap R S) = g.toRingHom.comp (algebraMap R S) := by simp
    suffices f = g by rwa [DFunLike.ext_iff] at this
    apply IsLocalization.algHom_ext M
    rwa [DFunLike.ext_iff] at this ⊢

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

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalCommRing β
⊢ NonUnitalCommRing α

Tactic:
let zero := e.zero
  let add := e.add
  let mul := e.mul
  let neg := e.Neg
  let sub := e.sub
  let nsmul := e.smul ℕ
  let zsmul := e.smul ℤ
  apply e.injective.nonUnitalCommRing _ <;> intros <;> exact e.apply_symm_apply _

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

Goal state before:
pp: case refine_2
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 A
inst✝² : Algebra R A
inst✝¹ : CommSemiring B
inst✝ : Algebra R B
x y : A ⊗[R] B
⊢ ∀ (x : A) (y_1 : B), x ⊗ₜ[R] y_1 * y = y * x ⊗ₜ[R] y_1

Tactic:
intro a₁

Goal state after:
case refine_2
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 A
inst✝² : Algebra R A
inst✝¹ : CommSemiring B
inst✝ : Algebra R B
x y : A ⊗[R] B
a₁ : A
⊢ ∀ (y_1 : B), a₁ ⊗ₜ[R] y_1 * y = y * a₁ ⊗ₜ[R] y_1
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : Set B
hs : adjoin R s = ⊤
⊢ adjoin A ↑(Subalgebra.map includeRight ⊤) = ⊤

Tactic:
← Algebra.toSubmodule_eq_top,

Goal state after:
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : Set B
hs : adjoin R s = ⊤
⊢ Subalgebra.toSubmodule (adjoin A ↑(Subalgebra.map includeRight ⊤)) = ⊤
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: case refine_2.refine_2
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
x y : A ⊗[R] B
m : M
⊢ ∀ (x : A) (y : B) (x_1 : A) (y_1 : B), (x_1 ⊗ₜ[R] y_1 * x ⊗ₜ[R] y) • m = x_1 ⊗ₜ[R] y_1 • x ⊗ₜ[R] y • m

Tactic:
intro a₁

Goal state after:
case refine_2.refine_2
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
x y : A ⊗[R] B
m : M
a₁ : A
⊢ ∀ (y : B) (x : A) (y_1 : B), (x ⊗ₜ[R] y_1 * a₁ ⊗ₜ[R] y) • m = x ⊗ₜ[R] y_1 • a₁ ⊗ₜ[R] y • m
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: case refine_3.refine_3
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
x y : A ⊗[R] B
m : M
⊢ ∀ (x y : A ⊗[R] B),
    (∀ (x_1 y : A ⊗[R] B),
        (x_1 * x) • m = x_1 • x • m → (y * x) • m = y • x • m → ((x_1 + y) * x) • m = (x_1 + y) • x • m) →
      (∀ (x y_1 : A ⊗[R] B),
          (x * y) • m = x • y • m → (y_1 * y) • m = y_1 • y • m → ((x + y_1) * y) • m = (x + y_1) • y • m) →
        ∀ (x_1 y_1 : A ⊗[R] B),
          (x_1 * (x + y)) • m = x_1 • (x + y) • m →
            (y_1 * (x + y)) • m = y_1 • (x + y) • m → ((x_1 + y_1) * (x + y)) • m = (x_1 + y_1) • (x + y) • m

Tactic:
intro u v _ _ z w hz hw
      simp only [(· • ·)] at hz hw ⊢
      simp only [add_mul, map_add, LinearMap.add_apply, hz, hw, add_add_add_comm]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
x : A ⊗[R] B
m₁ m₂ : M
⊢ x • (m₁ + m₂) = x • m₁ + x • m₂

Tactic:
by simp only [(· • ·), map_add]

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
R✝ : Type u_3
S : Type u_4
T : Type u_5
A : Type u_6
B : Type u_7
inst✝²³ : CommSemiring R✝
inst✝²² : CommSemiring S
inst✝²¹ : CommSemiring T
inst✝²⁰ : Semiring A
inst✝¹⁹ : Semiring B
inst✝¹⁸ : Algebra R✝ A
inst✝¹⁷ : Algebra R✝ B
inst✝¹⁶ : Algebra S A
inst✝¹⁵ : Algebra S B
inst✝¹⁴ : Algebra T A
inst✝¹³ : SMulCommClass R✝ T A
inst✝¹² : SMulCommClass S T A
inst✝¹¹ : SMulCommClass R✝ S A
inst✝¹⁰ : CompatibleSMul R✝ S A B
inst✝⁹ : Algebra R✝ S
inst✝⁸ : CompatibleSMul R✝ S S A
inst✝⁷ : CompatibleSMul S R✝ S A
R : Type u_8
M : Type u_9
N : Type u_10
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module ℚ M
inst✝ : Module ℚ N
q : ℚ
m : M
n : N
this : IsAddTorsionFree (M ⊗[R] N)
⊢ q.den • (q • m) ⊗ₜ[R] n = q.den • m ⊗ₜ[R] (q • n)

Tactic:
rw [smul_tmul', ← tmul_smul, ← smul_assoc, ← smul_assoc, nsmul_eq_mul, Rat.den_mul_eq_num]

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✝⁴³ : 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
R✝ : Type u_3
S : Type u_4
T : Type u_5
A : Type u_6
B : Type u_7
inst✝²³ : CommSemiring R✝
inst✝²² : CommSemiring S
inst✝²¹ : CommSemiring T
inst✝²⁰ : Semiring A
inst✝¹⁹ : Semiring B
inst✝¹⁸ : Algebra R✝ A
inst✝¹⁷ : Algebra R✝ B
inst✝¹⁶ : Algebra S A
inst✝¹⁵ : Algebra S B
inst✝¹⁴ : Algebra T A
inst✝¹³ : SMulCommClass R✝ T A
inst✝¹² : SMulCommClass S T A
inst✝¹¹ : SMulCommClass R✝ S A
inst✝¹⁰ : CompatibleSMul R✝ S A B
inst✝⁹ : Algebra R✝ S
inst✝⁸ : CompatibleSMul R✝ S S A
inst✝⁷ : CompatibleSMul S R✝ S A
R : Type u_8
M : Type u_9
N : Type u_10
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module ℚ M
inst✝ : Module ℚ N
q : ℚ
m : M
n : N
this : IsAddTorsionFree (M ⊗[R] N)
⊢ (↑q.num • m) ⊗ₜ[R] n = m ⊗ₜ[R] (↑q.num • n)
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
hx : IsUnit x
i : ι
⊢ ↑hx.unit⁻¹ i = ↑⋯.unit⁻¹

Tactic:
rw [← Units.inv_eq_val_inv, ← MulEquiv.val_inv_piUnits_apply]; congr; ext; rfl

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

Goal state before:
pp: A : Type u_2
B : Type u_3
inst✝¹ : NonUnitalSemiring A
inst✝ : NonUnitalSemiring B
a : A
b : B
⊢ IsQuasiregular (a, b) ↔ IsQuasiregular a ∧ IsQuasiregular b

Tactic:
simp only [isQuasiregular_iff', ← isUnit_map_iff (PreQuasiregular.toProd A B), Prod.isUnit_iff]
  congr!

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

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
a b : A
f g : End R M
⊢ (tensorProduct R A M M) ((a * b) ⊗ₜ[R] (f * g)) =
    (tensorProduct R A M M) (a ⊗ₜ[R] f) * (tensorProduct R A M M) (b ⊗ₜ[R] g)

Tactic:
by
      apply LinearMap.ext
      intro x
      simp only [tensorProduct, mul_comm a b, Module.End.mul_eq_comp,
        TensorProduct.AlgebraTensorModule.lift_apply, TensorProduct.lift.tmul, coe_restrictScalars,
        coe_mk, AddHom.coe_mk, mul_smul, smul_apply, baseChangeHom_apply, baseChange_comp,
        comp_apply, Algebra.mul_smul_comm, Algebra.smul_mul_assoc]

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

Goal state before:
pp: case 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 A
inst✝ : Module.Free R B
w : A ⊗[R] B
hw : w ∈ centralizer R (⇑includeLeft '' S)
⊢ w ∈ (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).range

Tactic:
rw [mem_centralizer_iff] at hw

Goal state after:
case 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 A
inst✝ : Module.Free R B
w : A ⊗[R] B
hw : ∀ g ∈ ⇑includeLeft '' S, g * w = w * g
⊢ w ∈ (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).range
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
inst✝ : StarOrderedRing R
a : R
ha : a ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
c x : R
hx : x ∈ range fun s ↦ star s * s
⊢ 0 ≤ star c * x * c

Tactic:
obtain ⟨x, rfl⟩ := hx
    convert! star_mul_self_nonneg (x * c) using 1
    rw [star_mul, ← mul_assoc, mul_assoc _ _ c]

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

Goal state before:

Tactic:
0 ≤ star c * x * c + 0 := by rw [add_zero]; exact hx
      _ ≤ star c * x * c + star c * y * c := by gcongr
      _ ≤ _ := by rw [mul_add, add_mul]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝¹¹ : Semiring R
inst✝¹⁰ : PartialOrder R
inst✝⁹ : StarRing R
inst✝⁸ : StarOrderedRing R
inst✝⁷ : NonUnitalSemiring A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : Module R A
inst✝² : StarModule R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
r : R
hr : 0 ≤ r
a b : A
hab : a ≤ b
⊢ r • a ≤ r • b

Tactic:
by
    rw [StarOrderedRing.nonneg_iff] at hr
    rw [StarOrderedRing.le_iff] at hab ⊢
    obtain ⟨a, ha, rfl⟩ := hab
    exact ⟨r • a, smul_mem_closure_star_mul hr ha, smul_add ..⟩

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

Goal state before:
pp: ι : Type w
R : Type u
M : Type v
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : IsDomain R
inst✝³ : IsTorsionFree R M
inst✝² : Module.Finite R M
inst✝¹ : StrongRankCondition R
p : ι → Submodule R M
hp : iSupIndep p
inst✝ : Fintype { i // p i ≠ ⊥ }
⊢ Fintype.card { i // p i ≠ ⊥ } ≤ finrank R M

Tactic:
simpa using hp.subtype_ne_bot_le_finrank_aux

Goal state after: