mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Algebra.Unitization

Goal state before:
pp: case fst
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : StarRing R
inst✝¹⁶ : NonUnitalSemiring A
inst✝¹⁵ : StarRing A
inst✝¹⁴ : Module R A
inst✝¹³ : SMulCommClass R A A
inst✝¹² : IsScalarTower R A A
inst✝¹¹ : NonUnitalSemiring B
inst✝¹⁰ : StarRing B
inst✝⁹ : Module R B
inst✝⁸ : SMulCommClass R B B
inst✝⁷ : IsScalarTower R B B
inst✝⁶ : NonUnitalSemiring C
inst✝⁵ : StarRing C
inst✝⁴ : Module R C
inst✝³ : SMulCommClass R C C
inst✝² : IsScalarTower R C C
inst✝¹ : StarModule R B
inst✝ : StarModule R C
φ : A →⋆ₙₐ[R] B
ψ : B →⋆ₙₐ[R] C
x✝ : A
⊢ (((↑(starMap (ψ.comp φ))).comp (inrNonUnitalStarAlgHom R A)) x✝).toProd.1 =
    (((↑((starMap ψ).comp (starMap φ))).comp (inrNonUnitalStarAlgHom R A)) x✝).toProd.1

Tactic:
simp

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

Goal state before:
pp: case snd
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : StarRing R
inst✝¹⁶ : NonUnitalSemiring A
inst✝¹⁵ : StarRing A
inst✝¹⁴ : Module R A
inst✝¹³ : SMulCommClass R A A
inst✝¹² : IsScalarTower R A A
inst✝¹¹ : NonUnitalSemiring B
inst✝¹⁰ : StarRing B
inst✝⁹ : Module R B
inst✝⁸ : SMulCommClass R B B
inst✝⁷ : IsScalarTower R B B
inst✝⁶ : NonUnitalSemiring C
inst✝⁵ : StarRing C
inst✝⁴ : Module R C
inst✝³ : SMulCommClass R C C
inst✝² : IsScalarTower R C C
inst✝¹ : StarModule R B
inst✝ : StarModule R C
φ : A →⋆ₙₐ[R] B
ψ : B →⋆ₙₐ[R] C
x✝ : A
⊢ (((↑(starMap (ψ.comp φ))).comp (inrNonUnitalStarAlgHom R A)) x✝).toProd.2 =
    (((↑((starMap ψ).comp (starMap φ))).comp (inrNonUnitalStarAlgHom R A)) x✝).toProd.2

Tactic:
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:
simp

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

Goal state before:
pp: case fst
R : Type u_1
B : Type u_3
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring B
inst✝⁴ : StarRing B
inst✝³ : Module R B
inst✝² : SMulCommClass R B B
inst✝¹ : IsScalarTower R B B
inst✝ : StarModule R B
x✝ : B
⊢ (((↑(starMap (NonUnitalStarAlgHom.id R B))).comp (inrNonUnitalStarAlgHom R B)) x✝).toProd.1 =
    (((↑(StarAlgHom.id R (Unitization R B))).comp (inrNonUnitalStarAlgHom R B)) x✝).toProd.1

Tactic:
simp

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

Goal state before:
pp: case snd
R : Type u_1
B : Type u_3
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring B
inst✝⁴ : StarRing B
inst✝³ : Module R B
inst✝² : SMulCommClass R B B
inst✝¹ : IsScalarTower R B B
inst✝ : StarModule R B
x✝ : B
⊢ (((↑(starMap (NonUnitalStarAlgHom.id R B))).comp (inrNonUnitalStarAlgHom R B)) x✝).toProd.2 =
    (((↑(StarAlgHom.id R (Unitization R B))).comp (inrNonUnitalStarAlgHom R B)) x✝).toProd.2

Tactic:
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
a : A
⊢ (productMap f g) (a ⊗ₜ[R] 1) = f a

Tactic:
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:
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:
simp

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

Goal state before:
pp: case zero
R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : StarModule R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
r : R
a : A
ha : a ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
⊢ 0 • a ∈ AddSubmonoid.closure (range fun s ↦ star s * s)

Tactic:
simp

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

Goal state before:
pp: case mem.zero
R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : StarModule R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
r✝ : R
a : A
r : R
hr : r ∈ range fun s ↦ star s * s
⊢ r • 0 ∈ AddSubmonoid.closure (range fun s ↦ star s * s)

Tactic:
simp

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
⊢ (tensorProduct R A M M) (1 ⊗ₜ[R] 1) = 1

Tactic:
apply LinearMap.ext
      intro x
      simp only [tensorProduct, TensorProduct.AlgebraTensorModule.lift_apply,
        TensorProduct.lift.tmul, coe_restrictScalars, coe_mk, AddHom.coe_mk, one_smul,
        baseChangeHom_apply, baseChange_eq_ltensor, Module.End.one_eq_id,
        lTensor_id, LinearMap.id_apply]

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

Goal state before:
pp: case ha
R : Type u_4
S : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
x✝ : ULift.{u₂, u_5} S
⊢ (((lmul' (ULift.{u₁, u_4} R)).comp includeLeft) x✝).down =
    ((((AlgHom.ulift.{u_8, u₁, u₂, u_4, u_5, u_5} (lmul' R)).comp ↑(uliftEquiv R (ULift.{u₁, u_4} R) S S).symm).comp
          includeLeft)
        x✝).down

Tactic:
simp

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

Goal state before:
pp: case hb
R : Type u_4
S : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
x✝ : ULift.{u₂, u_5} S
⊢ (((AlgHom.restrictScalars (ULift.{u₁, u_4} R) (lmul' (ULift.{u₁, u_4} R))).comp includeRight) x✝).down =
    (((AlgHom.restrictScalars (ULift.{u₁, u_4} R)
              ((AlgHom.ulift.{u_8, u₁, u₂, u_4, u_5, u_5} (lmul' R)).comp
                ↑(uliftEquiv R (ULift.{u₁, u_4} R) S S).symm)).comp
          includeRight)
        x✝).down

Tactic:
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
⊢ (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:
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:
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:
simp

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

Goal state before:
pp: case e_a
R : Type u_1
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
x : R
hx : IsSelfAdjoint x
d : R
hd : d ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
s : R
⊢ ↑starAddEquiv ((fun s ↦ star s * s) s) = (AddMonoidHom.id R) ((fun s ↦ star s * s) s)

Tactic:
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:
simp

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

Goal state before:
pp: case hopi
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⟩ := ⋯
⊢ ∀ (i : ι) (x y : ↑↑(K i)), Set.inclusion ⋯ (x * y) = Set.inclusion ⋯ x * Set.inclusion ⋯ y

Tactic:
simp

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

Goal state before:
pp: case h
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⟩ := ⋯
⊢ ∀ (i : ι) (x y : ↑↑(K i)), (f i) (x * y) = (f i) x * (f i) y

Tactic:
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) 0 = 0

Tactic:
simp

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

Goal state before:
pp: case mpr.zero
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
⊢ includeLeft x * (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).toRingHom 0 =
    (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).toRingHom 0 * includeLeft x

Tactic:
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:
simp

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

Goal state before:
pp: case hopi
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⟩ := ⋯
⊢ ∀ (i : ι) (x y : ↑↑(K i)), Set.inclusion ⋯ (x + y) = Set.inclusion ⋯ x + Set.inclusion ⋯ y

Tactic:
simp

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

Goal state before:
pp: case h
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⟩ := ⋯
⊢ ∀ (i : ι) (x y : ↑↑(K i)), (f i) (x + y) = (f i) x + (f i) y

Tactic:
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
r : R
⊢ ∀ (i : ι), (f i) ((algebraMap R ↥(K i)) r) = (algebraMap R B) r

Tactic:
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
ι : 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
i : ι
x : ↥(K i)
h : K i ≤ T
⊢ Set.iUnionLift (fun i ↦ ↑(K i)) (fun i x ↦ (f i) x) ⋯ ↑(iSup K) ⋯ ⟨↑x, ⋯⟩ = (f i) x

Tactic:
rw [Set.iUnionLift_inclusion]

Goal state after:
case h
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
ι : 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
i : ι
x : ↥(K i)
h : K i ≤ T
⊢ ↑(K i) ⊆ ↑(iSup K)
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
ι : 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
i : ι
h : K i ≤ T
x✝ : ↥(K i)
⊢ ((iSupLift K dir f hf T hT).comp (inclusion h)) x✝ = (f i) x✝

Tactic:
simp

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

Goal state before:
pp: case e'_4
R : Type u
M : Type v
ι : Type w
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t : Set ι
f : ι → M
hs : LinearIndepOn R f s
ht : LinearIndepOn R (⇑(span R (f '' s)).mkQ ∘ f) t
⊢ span R (f '' s) = (span R (f '' s)).mkQ.ker

Tactic:
simp

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

Goal state before:
pp: R : Type u
M : Type v
M' : Type v'
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Nontrivial R
⊢ lift.{v', v} (Module.rank R M) + lift.{v, v'} (Module.rank R M') ≤ Module.rank R (M × M')

Tactic:
rw [← rank_ulift, ← rank_ulift]
  exact (rank_add_rank_le_rank_prod R _).trans_eq
    (ULift.moduleEquiv.prodCongr ULift.moduleEquiv).rank_eq

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:
simp

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

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

Tactic:
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:
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:
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:
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:
simp

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

Goal state before:
pp: R : Type u
S : Type u'
M : Type v
M' : Type v'
M₁ : Type v
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type u_1
inst✝¹¹ : Semiring R
inst✝¹⁰ : CommSemiring S
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M'
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M
inst✝⁵ : StrongRankCondition R
inst✝⁴ : Free R M
inst✝³ : (i : η) → AddCommMonoid (φ i)
inst✝² : (i : η) → Module R (φ i)
inst✝¹ : ∀ (i : η), Free R (φ i)
inst✝ : Fintype η
n : ℕ
hn : Module.rank R M = ↑n
this : Nontrivial R
⊢ lift.{u, v} ↑n = lift.{v, u} ↑n

Tactic:
simp

Goal state after:
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
⊢ Module.rank R M ≤ ↑n

Tactic:
Module.rank_def

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
⊢ ⨆ ι, #↑↑ι ≤ ↑n
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:
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:
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:
simp

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

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a✝ : Nontrivial R
h : ∀ (x : M), ∃ a, a ≠ 0 ∧ a • x = 0
⊢ Module.rank R M ≤ 0

Tactic:
Module.rank_def

Goal state after:
case mpr
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a✝ : Nontrivial R
h : ∀ (x : M), ∃ a, a ≠ 0 ∧ a • x = 0
⊢ ⨆ ι, #↑↑ι ≤ 0
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:
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
hs : LinearIndepOn R id ↑s
a✝ : M
⊢ a✝ ∈ s ↔ a✝ ∈ (↑s).toFinset

Tactic:
simp

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

Goal state before:
pp: F : Type u_2
E : Type u_3
inst✝² : CommSemiring F
inst✝¹ : Semiring E
inst✝ : Algebra F E
⊢ Module.rank F ↥⊤ = Module.rank F E

Tactic:
exact _root_.rank_top F E

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:
simp

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
⊢ lift.{w, v} ↑(finrank R M) = lift.{v, w} ↑(finrank R M)

Tactic:
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✝¹² : 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:
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✝ : StarModule R A
S : NonUnitalSubalgebra R A
x : A
⊢ star x ∈ star S ↔ x ∈ S

Tactic:
simp

Goal state after: