mathlib-initiative/mathlib-tactics huggingface dataset:
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✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : CommSemiring S
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
⊢ (let __spread.0 := LinearMap.mul' R S;
      { toAddHom := __spread.0.toAddHom, map_smul' := ⋯ })
      (1 ⊗ₜ[R] 1) =
    1

Tactic:
by simp

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✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
inst✝ : CompatibleSMul R S S S
x : S ⊗[R] S
⊢ (includeLeft.comp (lmul'' R)) 0 = (AlgHom.id S (S ⊗[R] S)) 0

Tactic:
by simp

Goal state after:
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✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : CommSemiring S
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
b : B
⊢ (productMap f g) (1 ⊗ₜ[R] b) = g b

Tactic:
by simp

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

Goal state before:
pp: A : Type u_1
inst✝³ : PartialOrder A
inst✝² : Monoid A
inst✝¹ : Zero A
inst✝ : Subsingleton A
a : A
⊢ 0 ≤ a

Tactic:
by simp

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

Goal state before:
pp: A : Type u_1
inst✝³ : Semiring A
inst✝² : StarRing A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
u a : A
hu : IsUnit u
⊢ 0 ≤ u * a * star u ∧ IsUnit (u * a * star u) ↔ 0 ≤ a ∧ IsUnit a

Tactic:
hu.star_right_conjugate_nonneg_iff

Goal state after:
A : Type u_1
inst✝³ : Semiring A
inst✝² : StarRing A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
u a : A
hu : IsUnit u
⊢ 0 ≤ a ∧ IsUnit (u * a * star u) ↔ 0 ≤ a ∧ IsUnit a
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:
mem_centralizer_iff

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.Algebra.Subalgebra.Centralizer

Goal state before:
pp: 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
ℬ : Module.Basis (Module.Free.ChooseBasisIndex R B) R B := Module.Free.chooseBasis R B
b : Module.Free.ChooseBasisIndex R B →₀ A
hw : ∀ g ∈ ⇑includeLeft '' S, (g * b.sum fun i m ↦ m ⊗ₜ[R] ℬ i) = (b.sum fun i m ↦ m ⊗ₜ[R] ℬ i) * g
j : Module.Free.ChooseBasisIndex R B
hj : j ∈ b.support
⊢ (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).toRingHom (⟨b j, ?m.153⟩ ⊗ₜ[R] ℬ j) =
    (fun i m ↦ m ⊗ₜ[R] ℬ i) j (b j)

Tactic:
by simp

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

Goal state before:
pp: 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
ℬ : Module.Basis (Module.Free.ChooseBasisIndex R B) R B := Module.Free.chooseBasis R B
b : Module.Free.ChooseBasisIndex R B →₀ A
hw : ∀ g ∈ ⇑includeLeft '' S, (g * b.sum fun i m ↦ m ⊗ₜ[R] ℬ i) = (b.sum fun i m ↦ m ⊗ₜ[R] ℬ i) * g
j : Module.Free.ChooseBasisIndex R B
hj : j ∈ b.support
x : A
hx : x ∈ S
⊢ 0 * x = 0

Tactic:
by simp

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

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
S : Subalgebra R A
ι : Type u_4
inst✝ : Nonempty ι
K : ι → Subalgebra R A
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : Subalgebra R A
hT : T ≤ iSup K
compat : ∀ (i j : ι) (x : A) (hxi : x ∈ ↑(K i)) (hxj : x ∈ ↑(K j)), (f i) ⟨x, hxi⟩ = (f j) ⟨x, hxj⟩ :=
  iSupLift._proof_2 K dir f hf
⊢ ∀ (i : ι), (f i) 1 = 1

Tactic:
by simp

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

Goal state before:
pp: 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
ℬ : Module.Basis (Module.Free.ChooseBasisIndex R B) R B := Module.Free.chooseBasis R B
b : Module.Free.ChooseBasisIndex R B →₀ A
j : Module.Free.ChooseBasisIndex R B
hj : j ∈ b.support
x : A
hx : x ∈ S
hw : ∑ i ∈ b.support, (x * b i) ⊗ₜ[R] ℬ i = ∑ i ∈ b.support, (b i * x) ⊗ₜ[R] ℬ i
⊢ ∀ i ∈ b.support, ((TensorProduct.mk R A B).flip (ℬ i)) 0 = 0

Tactic:
by simp

Goal state after:
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 : R
ha : a ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
c x y : R
x✝¹ : x ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
x✝ : y ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
hx : 0 ≤ star c * x * c
hy : 0 ≤ star c * y * c
⊢ star c * x * c + star c * y * c ≤ (star c * x + star c * y) * c

Tactic:
add_mul

Goal state after:
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 y : R
x✝¹ : x ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
x✝ : y ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
hx : 0 ≤ star c * x * c
hy : 0 ≤ star c * y * c
⊢ star c * x * c + star c * y * c ≤ star c * x * c + star c * y * c
Module: Mathlib.Algebra.Algebra.Subalgebra.Directed

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
S : Subalgebra R A
ι : Type u_4
inst✝ : Nonempty ι
K : ι → Subalgebra R A
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : Subalgebra R A
hT : T ≤ iSup K
compat : ∀ (i j : ι) (x : A) (hxi : x ∈ ↑(K i)) (hxj : x ∈ ↑(K j)), (f i) ⟨x, hxi⟩ = (f j) ⟨x, hxj⟩ :=
  iSupLift._proof_2 K dir f hf
⊢ ∀ (i : ι), (f i) 0 = 0

Tactic:
by simp

Goal state after:
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
x✝ y x d : R
hd : d ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
s : R
⊢ (fun s ↦ star s * s) s = starAddEquiv ((fun s ↦ star s * s) s)

Tactic:
by simp

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

Goal state before:
pp: case mpr.add
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
x : A
hx : x ∈ S
y z : ↥(centralizer R S) ⊗[R] B
hy :
  includeLeft x * (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).toRingHom y =
    (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).toRingHom y * includeLeft x
hz :
  includeLeft x * (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).toRingHom z =
    (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).toRingHom z * includeLeft x
⊢ (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).toRingHom y * includeLeft x +
      (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).toRingHom z * includeLeft x =
    ((Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).toRingHom y +
        (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).toRingHom z) *
      includeLeft x

Tactic:
add_mul

Goal state after:
case mpr.add
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
x : A
hx : x ∈ S
y z : ↥(centralizer R S) ⊗[R] B
hy :
  includeLeft x * (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).toRingHom y =
    (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).toRingHom y * includeLeft x
hz :
  includeLeft x * (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).toRingHom z =
    (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).toRingHom z * includeLeft x
⊢ (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).toRingHom y * includeLeft x +
      (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).toRingHom z * includeLeft x =
    (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).toRingHom y * includeLeft x +
      (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).toRingHom z * includeLeft x
Module: Mathlib.Algebra.Algebra.Subalgebra.Directed

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
S : Subalgebra R A
ι : Type u_4
inst✝ : Nonempty ι
K : ι → Subalgebra R A
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : Subalgebra R A
hT : T ≤ iSup K
compat : ∀ (i j : ι) (x : A) (hxi : x ∈ ↑(K i)) (hxj : x ∈ ↑(K j)), (f i) ⟨x, hxi⟩ = (f j) ⟨x, hxj⟩ :=
  iSupLift._proof_2 K dir f hf
r : R
⊢ ∀ (i : ι), (f i) ((algebraMap R ↥(K i)) r) = (algebraMap R B) r

Tactic:
by simp

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

Goal state before:
pp: R : Type u
M M₁ : Type v
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : Module R M
inst✝³ : Module R M₁
inst✝² : StrongRankCondition R
inst✝¹ : Free R M
inst✝ : Free R M₁
⊢ Module.rank R (M × M₁) = Module.rank R M + Module.rank R M₁

Tactic:
by simp

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : StrongRankCondition R
ι : Type u
⊢ Module.rank R (ι →₀ R) = #ι

Tactic:
by simp

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

Goal state before:
pp: R : Type u
inst✝³ : Semiring R
inst✝² : StrongRankCondition R
m n : Type u
inst✝¹ : Finite m
inst✝ : Finite n
⊢ Module.rank R (Matrix m n R) = #m * #n

Tactic:
by simp

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : StrongRankCondition R
n : ℕ
⊢ Module.rank R (Fin n → R) = ↑n

Tactic:
by simp

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : StrongRankCondition R
n : ℕ
⊢ finrank R (Fin n → R) = n

Tactic:
by simp

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

Goal state before:
pp: R : Type u
S : Type u'
M 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
⊢ Module.rank R (M ⊗[S] M₁) = Module.rank R M * Module.rank S M₁

Tactic:
by simp

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

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

Tactic:
by simp

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

Goal state before:
pp: R : Type u
S : Type u'
M' : Type v'
inst✝⁷ : Semiring R
inst✝⁶ : CommSemiring S
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : StrongRankCondition R
inst✝³ : StrongRankCondition S
inst✝² : Module S M'
inst✝¹ : Free S M'
inst✝ : Algebra S R
⊢ finrank R (R ⊗[S] M') = finrank S M'

Tactic:
by simp

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

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
s : Finset M
⊢ (↑s).toFinset.card = s.card

Tactic:
by simp

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
⊢ Module.rank F ↥⊥ = ↑1

Tactic:
by simp

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

Goal state before:
pp: R : Type u_2
V : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
W : Submodule R V
m : Type u_4
n : Type u_5
bW : Basis m R ↥W
bQ : Basis n R (V ⧸ W)
i : m
⊢ (bW.sumQuot bQ) (Sum.inl i) = ↑(bW i)

Tactic:
by
  simp [sumQuot]

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
⊢ #{ i // p i ≠ ⊥ } ≤ ↑(finrank R M)

Tactic:
suffices Cardinal.lift.{v} #{ i // p i ≠ ⊥ } ≤ Cardinal.lift.{v} (finrank R M : Cardinal.{w}) by
    rwa [Cardinal.lift_le] at this

Goal state after:
ι : 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
⊢ lift.{v, w} #{ i // p i ≠ ⊥ } ≤ lift.{v, w} ↑(finrank R M)
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
⊢ lift.{w, v} ↑(finrank R M) = lift.{v, w} ↑(finrank R M)

Tactic:
by simp

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

Goal state before:
pp: case refine_1
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Submodule K V
hbot : W ≠ ⊥
h : ∀ b < W, b = ⊥
⊢ ∃ v, v ≠ 0 ∧ W = K ∙ v

Tactic:
rcases (Submodule.ne_bot_iff W).1 hbot with ⟨v, ⟨hW, hv⟩⟩

Goal state after:
case refine_1
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Submodule K V
hbot : W ≠ ⊥
h : ∀ b < W, b = ⊥
v : V
hW : v ∈ W
hv : v ≠ 0
⊢ ∃ v, v ≠ 0 ∧ W = K ∙ v
Module: Mathlib.Algebra.Star.NonUnitalSubalgebra

Goal state before:
pp: F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝¹³ : CommSemiring R
inst✝¹² : NonUnitalNonAssocSemiring A
inst✝¹¹ : Module R A
inst✝¹⁰ : Star A
inst✝⁹ : NonUnitalNonAssocSemiring B
inst✝⁸ : Module R B
inst✝⁷ : Star B
inst✝⁶ : NonUnitalNonAssocSemiring C
inst✝⁵ : Module R C
inst✝⁴ : Star C
inst✝³ : FunLike F A B
inst✝² : NonUnitalAlgHomClass F R A B
inst✝¹ : StarHomClass F A B
S : NonUnitalStarSubalgebra R A
inst✝ : IsTorsionFree R A
⊢ ∀ (r : R) (m : ↥S), ↑(r • m) = r • ↑m

Tactic:
by simp

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

Goal state before:
pp: K : Type u_6
V : Type u_7
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : V →ₗ[K] K
v : V
hfv : f v ≠ 0
b₁ : Basis (↑(Basis.ofVectorSpaceIndex K ↥f.ker)) K ↥f.ker := Basis.ofVectorSpace K ↥f.ker
s : Set V := ⇑f.ker.subtype '' Set.range ⇑b₁
hs : span K s = f.ker
n : Set V := insert v s
⊢ ∃ n b i, v = b i ∧ f = f v • b.coord i

Tactic:
have H₁ : LinearIndepOn K _root_.id n := by
    apply LinearIndepOn.id_insert
    · apply LinearIndepOn.image
      · exact b₁.linearIndependent.linearIndepOn_id
      · simp
    · simp [hs, hfv]

Goal state after:
K : Type u_6
V : Type u_7
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : V →ₗ[K] K
v : V
hfv : f v ≠ 0
b₁ : Basis (↑(Basis.ofVectorSpaceIndex K ↥f.ker)) K ↥f.ker := Basis.ofVectorSpace K ↥f.ker
s : Set V := ⇑f.ker.subtype '' Set.range ⇑b₁
hs : span K s = f.ker
n : Set V := insert v s
H₁ : LinearIndepOn K _root_.id n
⊢ ∃ n b i, v = b i ∧ f = f v • b.coord i
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
t : Finset M
h : finrank R M + 1 < #t
x₀ : M
x₀_mem : x₀ ∈ t
shift : M ↪ M := { toFun := fun x ↦ x - x₀, inj' := ⋯ }
t' : Finset M := Finset.map shift (t.erase x₀)
h' : finrank R M < #t'
g : M → R
gsum : ∑ e ∈ t', g e • e = 0
x₁ : M
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : M → R := fun z ↦ if z = x₀ then -∑ z ∈ t.erase x₀, g (z - x₀) else g (z - x₀)
⊢ (∑ x ∈ t.erase x₀, if x = x₀ then -∑ z ∈ t.erase x₀, g (z - x₀) else g (x - x₀)) = ∑ z ∈ t.erase x₀, g (z - x₀)

Tactic:
exact sum_congr rfl fun x x_mem ↦ if_neg (mem_erase.mp x_mem).1

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 (NonUnitalStarSubalgebra R A)
⊢ ↑(sInf S).toNonUnitalSubalgebra = ↑(sInf (toNonUnitalSubalgebra '' S))

Tactic:
by simp

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
ι : Sort u_1
S : ι → NonUnitalStarSubalgebra R A
⊢ ↑(⨅ i, S i).toNonUnitalSubalgebra = ↑(⨅ i, (S i).toNonUnitalSubalgebra)

Tactic:
by simp

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

Goal state before:
pp: F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝¹⁷ : CommSemiring R
inst✝¹⁶ : NonUnitalSemiring A
inst✝¹⁵ : StarRing A
inst✝¹⁴ : Module R A
inst✝¹³ : NonUnitalSemiring B
inst✝¹² : StarRing B
inst✝¹¹ : Module R B
inst✝¹⁰ : FunLike F A B
inst✝⁹ : NonUnitalAlgHomClass F R A B
inst✝⁸ : StarHomClass F A B
S : NonUnitalStarSubalgebra R A
ι : Type u_1
inst✝⁷ : StarRing R
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : StarModule R A
inst✝³ : IsScalarTower R B B
inst✝² : SMulCommClass R B B
inst✝¹ : StarModule R B
inst✝ : Nonempty ι
K : ι → NonUnitalStarSubalgebra R A
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) K
f : (i : ι) → ↥(K i) →⋆ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
i j : ι
x : A
hxi : x ∈ ↑(K i)
hxj : x ∈ ↑(K j)
⊢ (f i) ⟨x, hxi⟩ = (f j) ⟨x, hxj⟩

Tactic:
let ⟨k, hik, hjk⟩ := dir i j

Goal state after:
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝¹⁷ : CommSemiring R
inst✝¹⁶ : NonUnitalSemiring A
inst✝¹⁵ : StarRing A
inst✝¹⁴ : Module R A
inst✝¹³ : NonUnitalSemiring B
inst✝¹² : StarRing B
inst✝¹¹ : Module R B
inst✝¹⁰ : FunLike F A B
inst✝⁹ : NonUnitalAlgHomClass F R A B
inst✝⁸ : StarHomClass F A B
S : NonUnitalStarSubalgebra R A
ι : Type u_1
inst✝⁷ : StarRing R
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : StarModule R A
inst✝³ : IsScalarTower R B B
inst✝² : SMulCommClass R B B
inst✝¹ : StarModule R B
inst✝ : Nonempty ι
K : ι → NonUnitalStarSubalgebra R A
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) K
f : (i : ι) → ↥(K i) →⋆ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
i j : ι
x : A
hxi : x ∈ ↑(K i)
hxj : x ∈ ↑(K j)
k : ι
hik : (fun x1 x2 ↦ x1 ≤ x2) (K i) (K k)
hjk : (fun x1 x2 ↦ x1 ≤ x2) (K j) (K k)
⊢ (f i) ⟨x, hxi⟩ = (f j) ⟨x, hxj⟩
Module: Mathlib.Algebra.Star.NonUnitalSubalgebra

Goal state before:
pp: F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝¹⁷ : CommSemiring R
inst✝¹⁶ : NonUnitalSemiring A
inst✝¹⁵ : StarRing A
inst✝¹⁴ : Module R A
inst✝¹³ : NonUnitalSemiring B
inst✝¹² : StarRing B
inst✝¹¹ : Module R B
inst✝¹⁰ : FunLike F A B
inst✝⁹ : NonUnitalAlgHomClass F R A B
inst✝⁸ : StarHomClass F A B
S : NonUnitalStarSubalgebra R A
ι : Type u_1
inst✝⁷ : StarRing R
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : StarModule R A
inst✝³ : IsScalarTower R B B
inst✝² : SMulCommClass R B B
inst✝¹ : StarModule R B
inst✝ : Nonempty ι
K : ι → NonUnitalStarSubalgebra R A
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) K
f : (i : ι) → ↥(K i) →⋆ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
⊢ ∀ (i : ι), (f i) 0 = 0

Tactic:
by simp

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

Goal state before:
pp: K : Type u_6
V : Type u_7
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : V →ₗ[K] K
hf : f ≠ 0
v : ↥f.ker
hv : ↑v ≠ 0
this : LinearIndepOn K _root_.id {v}
b₁ : Basis (↑(this.extend ⋯)) K ↥f.ker := Basis.extend this
w : V
hw : f w = 1
s : Set V := ⇑f.ker.subtype '' Set.range ⇑b₁
hs : span K s = f.ker
⊢ f.ker.subtype v = ↑v

Tactic:
by simp

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

Goal state before:
pp: F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
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
a : A
inst✝ : IsStarNormal a
⊢ ∀ x ∈ {a}, ∀ y ∈ {a}, x * y = y * x

Tactic:
by simp

Goal state after:
Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic

Goal state before:
pp: K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
S : Submodule K V
h : finrank K ↥S = finrank K V
bS : Basis (↑(Basis.ofVectorSpaceIndex K ↥S)) K ↥S := Basis.ofVectorSpace K ↥S
bS_eq : bS = Basis.ofVectorSpace K ↥S
⊢ Disjoint (span K (Set.range ⇑bS)) S.subtype.ker

Tactic:
by simp

Goal state after:
Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic

Goal state before:
pp: K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Unique ι
h : finrank K V = 1
v : V
hv : v ≠ 0
⊢ {(basisSingleton ι h v hv) default} = {v}

Tactic:
basisSingleton_apply

Goal state after:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Unique ι
h : finrank K V = 1
v : V
hv : v ≠ 0
⊢ {v} = {v}
Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic

Goal state before:
pp: K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
⊢ Module.rank K ↥⊥ = 0

Tactic:
by simp

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

Goal state before:
pp: K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
s : Submodule K V
inst✝ : Free K ↥s
x✝ : ∃ v₀, v₀ ≠ 0 ∧ ∀ (v : ↥s), ∃ r, r • v₀ = v
v₀ : V
hv₀ : v₀ ∈ s
H : ⟨v₀, hv₀⟩ ≠ 0
h : ∀ (v : ↥s), ∃ r, r • ⟨v₀, hv₀⟩ = v
v : V
hv : v ∈ s
r : K
hr : r • ⟨v₀, hv₀⟩ = ⟨v, hv⟩
⊢ r • v₀ = v

Tactic:
rwa [Subtype.ext_iff, coe_smul] at hr

Goal state after: