mathlib-initiative/mathlib-tactics huggingface dataset:
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
φ₁ φ₂ : ↥(adjoin R s) →ₐ[R] B
h : ∀ (x : A) (hx : x ∈ s), φ₁ ⟨x, ⋯⟩ = φ₂ ⟨x, ⋯⟩
⊢ φ₁ = φ₂

Tactic:
exact adjoin_ext h

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

Goal state before:
pp: case tmul
R : Type u_1
S : Type u_2
inst✝⁹ : CommSemiring R
inst✝⁸ : Semiring S
inst✝⁷ : Algebra R S
M : Type u_3
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : Module S M
inst✝³ : IsScalarTower R S M
N : Type u_4
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_5
inst✝ : DecidableEq ι
i : ι
m : M
f : ι →₀ N
⊢ ((finsuppRight R S M N ι) (m ⊗ₜ[R] f)) i = (lTensor M (Finsupp.lapply i)) (m ⊗ₜ[R] f)

Tactic:
| tmul m f =>

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.{w, u} R
inst✝ : Small.{w, v} P
e : (Shrink.{w, v} P →₀ Shrink.{w, u} R) ≃ₗ[R] P →₀ R :=
  mapDomain.linearEquiv (Shrink.{w, u} R) R (equivShrink P).symm ≪≫ₗ mapRange.linearEquiv (Shrink.linearEquiv R R)
x✝ : Projective R P
i : P →ₗ[R] P →₀ R
hi : Function.LeftInverse ⇑(linearCombination R id) ⇑i
⊢ (linearCombination R id ∘ₗ ↑e) ∘ₗ ↑e.symm ∘ₗ i = LinearMap.id

Tactic:
apply LinearMap.ext

Goal state after:
R : Type u
inst✝⁴ : Semiring R
P : Type v
inst✝³ : AddCommMonoid P
inst✝² : Module R P
inst✝¹ : Small.{w, u} R
inst✝ : Small.{w, v} P
e : (Shrink.{w, v} P →₀ Shrink.{w, u} R) ≃ₗ[R] P →₀ R := ⋯
x✝ : Projective R P
i : P →ₗ[R] P →₀ R
hi : Function.LeftInverse ⇑(linearCombination R id) ⇑i
⊢ ∀ (x : P), ((linearCombination R id ∘ₗ ↑e) ∘ₗ ↑e.symm ∘ₗ i) x = LinearMap.id x
Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose

Goal state before:
pp: n : Type u_3
α : Type v
inst✝² : DecidableEq n
inst✝¹ : AddMonoid α
inst✝ : StarAddMonoid α
v : n → α
⊢ (diagonal v)ᴴ = diagonal (star v)

Tactic:
rw [conjTranspose, diagonal_transpose, diagonal_map (star_zero _)]
  rfl

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
x : A
⊢ ⅟2 • (x - star x) ∈ skewAdjoint A

Tactic:
simp only [skewAdjoint.mem_iff, star_smul, star_sub, star_star, star_trivial, ← smul_neg,
        neg_sub]

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

Goal state before:
pp: l : Type u_1
m : Type u_2
α : Type u_12
inst✝² : DecidableEq l
inst✝¹ : DecidableEq m
inst✝ : Zero α
d₁ : l → α
d₂ : m → α
i j : l ⊕ m
⊢ fromBlocks (diagonal d₁) 0 0 (diagonal d₂) i j = diagonal (Sum.elim d₁ d₂) i j

Tactic:
rcases i with ⟨⟩ <;> rcases j with ⟨⟩ <;> simp [diagonal]

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

Goal state before:
pp: R : Type u_2
inst✝⁴ : CommRing R
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsPrincipalIdealRing R
N O : Submodule R M
hNO : N ≤ O
ϕ : ↥O →ₗ[R] R
hϕ : ∀ (ψ : ↥O →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
inst✝ : (ϕ.submoduleImage N).IsPrincipal
y : M
yN : y ∈ N
ϕy_eq : ϕ ⟨y, ⋯⟩ = generator (ϕ.submoduleImage N)
ψ : ↥O →ₗ[R] R
a : R := generator (ϕ.submoduleImage N)
d : R := generator (span R {a, ψ ⟨y, ⋯⟩})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ψ ⟨y, ⋯⟩
⊢ ∃ r₁ r₂, d = r₁ * a + r₂ * ψ ⟨y, ⋯⟩

Tactic:
obtain ⟨r₁, r₂', hr₂', hr₁⟩ :=
        mem_span_insert.mp (IsPrincipal.generator_mem (Submodule.span R {a, ψ ⟨y, hNO yN⟩}))
      obtain ⟨r₂, rfl⟩ := mem_span_singleton.mp hr₂'
      exact ⟨r₁, r₂, hr₁⟩

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
m : Type u_3
n : Type u_4
inst✝ : Fintype m
M : Matrix m n R
⊢ (Function.Injective fun v ↦ v ᵥ* M) ↔ LinearIndependent R M.row

Tactic:
← coe_vecMulLinear,

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
m : Type u_3
n : Type u_4
inst✝ : Fintype m
M : Matrix m n R
⊢ Function.Injective ⇑M.vecMulLinear ↔ LinearIndependent R M.row
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: case neg.intro.refine_2.refine_1
ι : 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 : O
yN : y ∈ N
ϕy_eq : ϕ ⟨y, ⋯⟩ = a
c : ι → R
hc : ∀ (i : ι), (b'M.coord i) ⟨y, ⋯⟩ = a * c i
val✝ : Fintype ι
y' : O := ∑ i, c i • ↑(b'M i)
y'M : y' ∈ M
mk_y' : ⟨y', y'M⟩ = ∑ i, c i • b'M i
a_smul_y' : a • y' = y
ϕy'_eq : ϕ ⟨y', y'M⟩ = 1
ϕy'_ne_zero : ϕ ⟨y', y'M⟩ ≠ 0
M' : Submodule R O := map M.subtype ϕ.ker
N' : Submodule R O := map N.subtype (ϕ ∘ₗ inclusion N_le_M).ker
M'_le_M : M' ≤ M
N'_le_M' : N' ≤ M'
N'_le_N : N' ≤ N
y'_ortho_M' : ∀ (c : R), ∀ z ∈ M', c • y' + z = 0 → c = 0
ay'_ortho_N' : ∀ (c : R), ∀ z ∈ N', c • a • y' + z = 0 → c = 0
n' : ℕ
bN' : Basis (Fin n') R ↥N'
m' : ℕ
hn'm' : n' ≤ m'
bM' : Basis (Fin m') R ↥M'
⊢ Basis (Fin (m' + 1)) R ↥M

Tactic:
refine Basis.mkFinConsOfLE y' y'M bM' M'_le_M y'_ortho_M' ?_
    intro z zM
    refine ⟨-ϕ ⟨z, zM⟩, ⟨⟨z, zM⟩ - ϕ ⟨z, zM⟩ • ⟨y', y'M⟩, LinearMap.mem_ker.mpr ?_, ?_⟩⟩
    · rw [map_sub, map_smul, ϕy'_eq, smul_eq_mul, mul_one, sub_self]
    · rw [map_sub, map_smul, sub_eq_add_neg, neg_smul]
      rfl

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
S : Type u_4
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Finite ι
b : Basis ι R S
I : Ideal S
hI : I ≠ ⊥
⊢ finrank R ↥(restrictScalars R I) = finrank R S

Tactic:
by
  obtain ⟨_, bS, bI, _, _, _⟩ := (I.restrictScalars R).smithNormalForm b
  cases nonempty_fintype ι
  rw [Module.finrank_eq_card_basis bS, Module.finrank_eq_card_basis bI]
  exact Ideal.rank_eq bS hI (bI.map ((restrictScalarsEquiv R S S I).restrictScalars R))

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

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

Tactic:
change _ ∈ B'.toSubmonoid

Goal state after:
R : Type uR
A : Type uA
B : Type uB
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : CommSemiring B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
r : A
s : Set B
B' : Subalgebra R B
hs : r • s ⊆ ↑B'
hr : (algebraMap A B) r ∈ B'
l : ↑↑(Submonoid.closure s) →₀ R
n₁ : ↥(Submonoid.closure s) → ℕ
n₂ : ∀ (x : ↥(Submonoid.closure s)), r ^ n₁ x • ↑x ∈ Submonoid.closure (r • s)
n : ℕ
hn : n ≥ l.support.sup n₁
a : ↑↑(Submonoid.closure s)
ha : a ∈ l.support
this : n ≥ n₁ a
⊢ r ^ n₁ a • ↑a ∈ B'.toSubmonoid
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
inst✝² : IsDomain A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
⊢ FaithfulSMul R (FractionRing A)

Tactic:
rw [faithfulSMul_iff_algebraMap_injective, IsScalarTower.algebraMap_eq R A]

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
inst✝² : IsDomain A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
⊢ Function.Injective ⇑((algebraMap A (FractionRing A)).comp (algebraMap R A))
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
x : R
y : ↥M
⊢ (algEquiv M S).symm (mk' S x y) = mk' (Localization M) x y

Tactic:
algEquiv_symm_mk'

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
x : R
y : ↥M
⊢ mk' (Localization M) x y = mk' (Localization M) x y
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
hR : IsField R
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
this : Field R := hR.toField
hM : M ≤ nonZeroDivisors R
r m : R
hm : m ∈ M
n : R
hn : m * n = 1
⊢ (algebraMap R Rₘ) (r * n) = mk' Rₘ r ⟨m, hm⟩

Tactic:
rw [eq_mk'_iff_mul_eq, ← map_mul, mul_assoc, _root_.mul_comm n, hn, mul_one]

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

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

Tactic:
by
  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.nonUnitalNonAssocRing _ <;> intros <;> exact e.apply_symm_apply _

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

Goal state before:
pp: R : Type u_1
inst✝² : NonUnitalRing R
inst✝¹ : StarRing R
inst✝ : IsAddTorsionFree R
p q : R
hp : IsStarProjection p
hq : IsStarProjection q
⊢ p * q = p ∧ q * p = p ↔ p * q = p

Tactic:
← hp.isSelfAdjoint

Goal state after:
R : Type u_1
inst✝² : NonUnitalRing R
inst✝¹ : StarRing R
inst✝ : IsAddTorsionFree R
p q : R
hp : IsStarProjection p
hq : IsStarProjection q
⊢ p * q = p ∧ q * star p = p ↔ p * q = p
Module: Mathlib.RingTheory.TensorProduct.Basic

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

Tactic:
induction x with
      | zero => simp [smul_zero]
      | tmul a' b' =>
        dsimp
        rw [TensorProduct.smul_tmul', TensorProduct.smul_tmul', tmul_mul_tmul, smul_mul_assoc]
      | add x y hx hy => simp [smul_add, add_mul _, *]

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
k : 𝕜
⊢ σ (↑ₐ k + 0) = {k}

Tactic:
← singleton_add_eq,

Goal state after:
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial A
k : 𝕜
⊢ {k} + σ 0 = {k}
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
u v : A ⊗[R] B
a✝¹ : ∀ (x y : A ⊗[R] B), (x * u) • m = x • u • m → (y * u) • m = y • u • m → ((x + y) * u) • m = (x + y) • u • m
a✝ : ∀ (x y : A ⊗[R] B), (x * v) • m = x • v • m → (y * v) • m = y • v • m → ((x + y) * v) • m = (x + y) • v • m
z w : A ⊗[R] B
hz : (moduleAux (z * (u + v))) m = (moduleAux z) ((moduleAux (u + v)) m)
hw : (moduleAux (w * (u + v))) m = (moduleAux w) ((moduleAux (u + v)) m)
⊢ (moduleAux ((z + w) * (u + v))) m = (moduleAux (z + w)) ((moduleAux (u + v)) m)

Tactic:
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
Q : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
I : Submodule R R
⊢ (↑(TensorProduct.lid R Q) ∘ₗ rTensor Q I.subtype).range = I • ⊤

Tactic:
refine le_antisymm ?_ fun q h ↦ Submodule.smul_induction_on h
    (fun r hr q _ ↦ ⟨⟨r, hr⟩ ⊗ₜ q, by simp⟩) (by simp +contextual [add_mem])

Goal state after:
R : Type u_1
Q : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
I : Submodule R R
⊢ (↑(TensorProduct.lid R Q) ∘ₗ rTensor Q I.subtype).range ≤ I • ⊤
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: R : Type uR
S : Type uS
A : Type uA
B : Type uB
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
h : Function.Bijective ⇑(algebraMap R B)
this : includeLeft.comp ↑(TensorProduct.rid R S A) = map (AlgHom.id S A) (ofId R B)
⊢ ⇑includeLeft ∘ ⇑(TensorProduct.rid R S A) = ⇑(map (AlgHom.id R A) (ofId R B))

pp: R : Type uR
S : Type uS
A : Type uA
B : Type uB
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
h : Function.Bijective ⇑(algebraMap R B)
this : includeLeft.comp ↑(TensorProduct.rid R S A) = map (AlgHom.id S A) (ofId R B)
⊢ Function.Bijective ⇑(map (AlgHom.id R A) (ofId R B))

Tactic:
· exact DFunLike.coe_fn_eq.mpr this

Goal state after:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
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
h : Function.Bijective ⇑(algebraMap R B)
this : includeLeft.comp ↑(TensorProduct.rid R S A) = map (AlgHom.id S A) (ofId R B)
⊢ Function.Bijective ⇑(map (AlgHom.id R A) (ofId R B))
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:
apply LinearMap.ext

Goal state after:
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
⊢ ∀ (x : A ⊗[R] M),
    ((tensorProduct R A M M) ((a * b) ⊗ₜ[R] (f * g))) x =
      ((tensorProduct R A M M) (a ⊗ₜ[R] f) * (tensorProduct R A M M) (b ⊗ₜ[R] g)) x
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
⊢ (tensorProduct R A M M) (1 ⊗ₜ[R] 1) = 1

Tactic:
apply LinearMap.ext

Goal state after:
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
⊢ ∀ (x : A ⊗[R] M), ((tensorProduct R A M M) (1 ⊗ₜ[R] 1)) x = 1 x
Module: Mathlib.Algebra.Algebra.Subalgebra.Directed

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
ι : Type u_4
inst✝ : Nonempty ι
K : ι → Subalgebra R A
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) K
s : Subalgebra R A :=
  let __spread.0 := (⨆ i, (K i).toSubsemiring).copy (⋃ i, ↑(K i).toSubsemiring) ⋯;
  { toSubsemiring := __spread.0, algebraMap_mem' := ⋯ }
⊢ ↑(iSup K) = ⋃ i, ↑(K i)

Tactic:
have : iSup K = s := le_antisymm
    (iSup_le fun i ↦ le_iSup (fun i ↦ (K i : Set A)) i) (Set.iUnion_subset fun _ ↦ le_iSup K _)

Goal state after:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
ι : Type u_4
inst✝ : Nonempty ι
K : ι → Subalgebra R A
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) K
s : Subalgebra R A :=
  let __spread.0 := (⨆ i, (K i).toSubsemiring).copy (⋃ i, ↑(K i).toSubsemiring) ⋯;
  { toSubsemiring := __spread.0, algebraMap_mem' := ⋯ }
this : iSup K = s
⊢ ↑(iSup K) = ⋃ i, ↑(K i)
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a c p : R
hp : p ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
⊢ ∃ p_1 ∈ AddSubmonoid.closure (range fun s ↦ star s * s), star c * (a + p) * c = star c * a * c + p_1

Tactic:
← StarOrderedRing.nonneg_iff

Goal state after:
R : Type u_1
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a c p : R
hp : 0 ≤ p
⊢ ∃ p_1, 0 ≤ p_1 ∧ star c * (a + p) * c = star c * a * c + p_1
Module: Mathlib.LinearAlgebra.Dimension.Constructions

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

Tactic:
rank_self,

Goal state after:
R : Type u
inst✝³ : Semiring R
inst✝² : StrongRankCondition R
m : Type v
n : Type w
inst✝¹ : Finite m
inst✝ : Finite n
⊢ lift.{max u w, v} #m * lift.{max u v, w} #n * lift.{max v w, u} 1 = lift.{max v w u, v} #m * lift.{max v w u, w} #n
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
H : ∀ (s : Finset M), (LinearIndependent R fun i ↦ ↑i) → s.card ≤ n
⊢ ∀ (s : Set M), LinearIndependent R Subtype.val → #↑s ≤ ↑n

Tactic:
intro s li

Goal state after:
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
H : ∀ (s : Finset M), (LinearIndependent R fun i ↦ ↑i) → s.card ≤ n
s : Set M
li : LinearIndependent R Subtype.val
⊢ #↑s ≤ ↑n
Module: Mathlib.LinearAlgebra.Dimension.Constructions

Goal state before:
pp: R : Type u
η : Type u₁'
inst✝² : Semiring R
inst✝¹ : StrongRankCondition R
inst✝ : Fintype η
⊢ ↑(Fintype.card η) * lift.{u₁', u} (Module.rank R R) = ↑(Fintype.card η)

Tactic:
rank_self,

Goal state after:
R : Type u
η : Type u₁'
inst✝² : Semiring R
inst✝¹ : StrongRankCondition R
inst✝ : Fintype η
⊢ ↑(Fintype.card η) * lift.{u₁', u} 1 = ↑(Fintype.card η)
Module: Mathlib.LinearAlgebra.Dimension.Constructions

Goal state before:
pp: R : Type u
S : Type u'
M : Type v
M' : Type v'
inst✝¹² : Semiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M'
inst✝⁸ : Module R M
inst✝⁷ : StrongRankCondition R
inst✝⁶ : StrongRankCondition S
inst✝⁵ : Module S M
inst✝⁴ : Module S M'
inst✝³ : Free S M'
inst✝² : Algebra S R
inst✝¹ : IsScalarTower S R M
inst✝ : Free R M
fst✝¹ : Type v
bM : Basis fst✝¹ R M
fst✝ : Type v'
bN : Basis fst✝ S M'
⊢ Module.rank R (M ⊗[S] M') = Cardinal.lift.{v', v} (Module.rank R M) * Cardinal.lift.{v, v'} (Module.rank S M')

Tactic:
rw [← bM.mk_eq_rank'', ← bN.mk_eq_rank'', ← (bM.tensorProduct bN).mk_eq_rank'', Cardinal.mk_prod]

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

Goal state before:
pp: F : Type u_2
E : Type u_3
inst✝⁶ : CommRing F
inst✝⁵ : IsDomain F
inst✝⁴ : Ring E
inst✝³ : Algebra F E
inst✝² : StrongRankCondition F
inst✝¹ : IsTorsionFree F E
inst✝ : Nontrivial E
⊢ LinearIndepOn F id {1}

Tactic:
have := Module.nontrivial F E

Goal state after:
F : Type u_2
E : Type u_3
inst✝⁶ : CommRing F
inst✝⁵ : IsDomain F
inst✝⁴ : Ring E
inst✝³ : Algebra F E
inst✝² : StrongRankCondition F
inst✝¹ : IsTorsionFree F E
inst✝ : Nontrivial E
this : Nontrivial F
⊢ LinearIndepOn F id {1}
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: case inr
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
hn : ↑n ≤ Module.rank R M
h : ↑n < Module.rank R M
⊢ ∃ s, s.card = n ∧ LinearIndepOn R id ↑s

Tactic:
· obtain ⟨s, hs, hs'⟩ := exists_set_linearIndependent_of_lt_rank h
    have : Finite s := lt_aleph0_iff_finite.mp (hs ▸ natCast_lt_aleph0)
    cases nonempty_fintype s
    exact ⟨s.toFinset, by simpa using hs, by simpa⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.VectorSpace

Goal state before:
pp: K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x : ↑(ofVectorSpaceIndex K V)
⊢ (ofVectorSpace K V) x = ↑x

Tactic:
unfold ofVectorSpace
  exact Basis.mk_apply _ _ _

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

Goal state before:
pp: R✝ : Type u
M✝ : Type v
ι : Type w
inst✝⁹ : Semiring R✝
inst✝⁸ : AddCommMonoid M✝
inst✝⁷ : Module R✝ M✝
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
⊢ ↑(finrank R M) < ℵ₀

Tactic:
simp [Cardinal.natCast_lt_aleph0]

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 : Set A
hcomm✝ : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x
hcomm_star : ∀ a ∈ s, ∀ b ∈ s, a * star b = star b * a
this : adjoin R s ≤ centralizer R ↑(centralizer R s)
x✝¹ x✝ : A
h₂ : x✝ ∈ adjoin R s
hcomm : ∀ a ∈ s ∪ star s, ∀ b ∈ s ∪ star s, a * b = b * a
h₁ : x✝¹ ∈ centralizer R ↑(centralizer R s)
⊢ x✝¹ * x✝ = x✝ * x✝¹

Tactic:
apply this at h₂

Goal state after:
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 : Set A
hcomm✝ : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x
hcomm_star : ∀ a ∈ s, ∀ b ∈ s, a * star b = star b * a
this : adjoin R s ≤ centralizer R ↑(centralizer R s)
x✝¹ x✝ : A
hcomm : ∀ a ∈ s ∪ star s, ∀ b ∈ s ∪ star s, a * b = b * a
h₁ : x✝¹ ∈ centralizer R ↑(centralizer R s)
h₂ : x✝ ∈ centralizer R ↑(centralizer R s)
⊢ x✝¹ * x✝ = x✝ * x✝¹
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Ring S
σ : R →+* S
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module S F
f_dom : Submodule R E
f g : ↥f_dom →ₛₗ[σ] F
h' :
  ∀ ⦃x : E⦄ ⦃hf : x ∈ { domain := f_dom, toFun := f }.domain⦄ ⦃hg : x ∈ { domain := f_dom, toFun := g }.domain⦄,
    ↑{ domain := f_dom, toFun := f } ⟨x, hf⟩ = ↑{ domain := f_dom, toFun := g } ⟨x, hg⟩
⊢ f = g

Tactic:
apply LinearMap.ext

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Ring S
σ : R →+* S
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module S F
f_dom : Submodule R E
f g : ↥f_dom →ₛₗ[σ] F
h' :
  ∀ ⦃x : E⦄ ⦃hf : x ∈ { domain := f_dom, toFun := f }.domain⦄ ⦃hg : x ∈ { domain := f_dom, toFun := g }.domain⦄,
    ↑{ domain := f_dom, toFun := f } ⟨x, hf⟩ = ↑{ domain := f_dom, toFun := g } ⟨x, hg⟩
⊢ ∀ (x : ↥f_dom), f x = g x