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

Goal state before:
pp: S : Type u_1
R : Type u_2
A : Type u_3
inst✝¹² : CommSemiring S
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : Module R A
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : IsScalarTower R A A
B : Type u_4
inst✝⁶ : Semiring B
inst✝⁵ : Algebra S B
inst✝⁴ : Algebra S R
inst✝³ : DistribMulAction S A
inst✝² : IsScalarTower S R A
C : Type u_5
inst✝¹ : Semiring C
inst✝ : Algebra R C
φ : A →ₙₐ[R] C
x✝ : A
⊢ ((fun φ ↦ (↑φ).comp (inrNonUnitalAlgHom R A)) φ.toAlgHom) x✝ = φ x✝

Tactic:
;

Goal state after:
S : Type u_1
R : Type u_2
A : Type u_3
inst✝¹² : CommSemiring S
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : Module R A
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : IsScalarTower R A A
B : Type u_4
inst✝⁶ : Semiring B
inst✝⁵ : Algebra S B
inst✝⁴ : Algebra S R
inst✝³ : DistribMulAction S A
inst✝² : IsScalarTower S R A
C : Type u_5
inst✝¹ : Semiring C
inst✝ : Algebra R C
φ : A →ₙₐ[R] C
x✝ : A
⊢ ((fun φ ↦ (↑φ).comp (inrNonUnitalAlgHom R A)) φ.toAlgHom) x✝ = φ x✝
Module: Mathlib.Algebra.Algebra.Unitization

Goal state before:
pp: S : Type u_1
R : Type u_2
A : Type u_3
inst✝¹² : CommSemiring S
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : Module R A
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : IsScalarTower R A A
B : Type u_4
inst✝⁶ : Semiring B
inst✝⁵ : Algebra S B
inst✝⁴ : Algebra S R
inst✝³ : DistribMulAction S A
inst✝² : IsScalarTower S R A
C : Type u_5
inst✝¹ : Semiring C
inst✝ : Algebra R C
φ : Unitization R A →ₐ[R] C
x✝ : A
⊢ ((↑((fun φ ↦ (↑φ).comp (inrNonUnitalAlgHom R A)) φ).toAlgHom).comp (inrNonUnitalAlgHom R A)) x✝ =
    ((↑φ).comp (inrNonUnitalAlgHom R A)) x✝

Tactic:
;

Goal state after:
S : Type u_1
R : Type u_2
A : Type u_3
inst✝¹² : CommSemiring S
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : Module R A
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : IsScalarTower R A A
B : Type u_4
inst✝⁶ : Semiring B
inst✝⁵ : Algebra S B
inst✝⁴ : Algebra S R
inst✝³ : DistribMulAction S A
inst✝² : IsScalarTower S R A
C : Type u_5
inst✝¹ : Semiring C
inst✝ : Algebra R C
φ : Unitization R A →ₐ[R] C
x✝ : A
⊢ ((↑((fun φ ↦ (↑φ).comp (inrNonUnitalAlgHom R A)) φ).toAlgHom).comp (inrNonUnitalAlgHom R A)) x✝ =
    ((↑φ).comp (inrNonUnitalAlgHom R A)) x✝
Module: Mathlib.Algebra.Algebra.Unitization

Goal state before:
pp: R : Type u_1
A : Type u_2
C : Type u_3
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✝³ : Semiring C
inst✝² : Algebra R C
inst✝¹ : StarRing C
inst✝ : StarModule R C
x✝¹ : A →⋆ₙₐ[R] C
x✝ : A
⊢ ((fun φ ↦ φ.toNonUnitalStarAlgHom.comp (inrNonUnitalStarAlgHom R A))
        ((fun φ ↦
            let __AlgHom := lift φ.toNonUnitalAlgHom;
            { toAlgHom := __AlgHom, map_star' := ⋯ })
          x✝¹))
      x✝ =
    x✝¹ x✝

Tactic:
;

Goal state after:
R : Type u_1
A : Type u_2
C : Type u_3
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✝³ : Semiring C
inst✝² : Algebra R C
inst✝¹ : StarRing C
inst✝ : StarModule R C
x✝¹ : A →⋆ₙₐ[R] C
x✝ : A
⊢ ((fun φ ↦ φ.toNonUnitalStarAlgHom.comp (inrNonUnitalStarAlgHom R A))
        ((fun φ ↦
            let __AlgHom := lift φ.toNonUnitalAlgHom;
            { toAlgHom := __AlgHom, map_star' := ⋯ })
          x✝¹))
      x✝ =
    x✝¹ x✝
Module: Mathlib.Algebra.Algebra.Unitization

Goal state before:
pp: R : Type u_1
A : Type u_2
C : Type u_3
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✝³ : Semiring C
inst✝² : Algebra R C
inst✝¹ : StarRing C
inst✝ : StarModule R C
x✝¹ : Unitization R A →⋆ₐ[R] C
x✝ : A
⊢ ((↑((fun φ ↦
                let __AlgHom := lift φ.toNonUnitalAlgHom;
                { toAlgHom := __AlgHom, map_star' := ⋯ })
              ((fun φ ↦ φ.toNonUnitalStarAlgHom.comp (inrNonUnitalStarAlgHom R A)) x✝¹))).comp
        (inrNonUnitalStarAlgHom R A))
      x✝ =
    ((↑x✝¹).comp (inrNonUnitalStarAlgHom R A)) x✝

Tactic:
;

Goal state after:
R : Type u_1
A : Type u_2
C : Type u_3
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✝³ : Semiring C
inst✝² : Algebra R C
inst✝¹ : StarRing C
inst✝ : StarModule R C
x✝¹ : Unitization R A →⋆ₐ[R] C
x✝ : A
⊢ ((↑((fun φ ↦
                let __AlgHom := lift φ.toNonUnitalAlgHom;
                { toAlgHom := __AlgHom, map_star' := ⋯ })
              ((fun φ ↦ φ.toNonUnitalStarAlgHom.comp (inrNonUnitalStarAlgHom R A)) x✝¹))).comp
        (inrNonUnitalStarAlgHom R A))
      x✝ =
    ((↑x✝¹).comp (inrNonUnitalStarAlgHom R A)) x✝
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: case ha
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)
x✝ : A
⊢ ((includeLeft.comp ↑(TensorProduct.rid R S A)).comp includeLeft) x✝ =
    ((map (AlgHom.id S A) (ofId R B)).comp includeLeft) x✝

Tactic:
;

Goal state after:
case ha
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)
x✝ : A
⊢ ((includeLeft.comp ↑(TensorProduct.rid R S A)).comp includeLeft) x✝ =
    ((map (AlgHom.id S A) (ofId R B)).comp includeLeft) x✝
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
x✝ : S
⊢ ((AlgHom.restrictScalars R (lmul'' R)).comp includeRight) x✝ =
    ((AlgHom.restrictScalars R ((↑(TensorProduct.lid S S)).comp (mapOfCompatibleSMul S R S S S))).comp includeRight) x✝

Tactic:
;

Goal state after:
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
x✝ : S
⊢ ((AlgHom.restrictScalars R (lmul'' R)).comp includeRight) x✝ =
    ((AlgHom.restrictScalars R ((↑(TensorProduct.lid S S)).comp (mapOfCompatibleSMul S R S S S))).comp includeRight) x✝
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

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

Goal state after:
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

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

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

Goal state after:
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

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
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: R : Type uR
S : Type uS
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : CompatibleSMul R S S S
x✝ : S
⊢ ((AlgHom.restrictScalars R ↑(lmulEquiv R S)).comp includeRight) x✝ =
    ((AlgHom.restrictScalars R ↑(lidOfCompatibleSMul R S S)).comp includeRight) x✝

Tactic:
;

Goal state after:
R : Type uR
S : Type uS
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : CompatibleSMul R S S S
x✝ : S
⊢ ((AlgHom.restrictScalars R ↑(lmulEquiv R S)).comp includeRight) x✝ =
    ((AlgHom.restrictScalars R ↑(lidOfCompatibleSMul R S S)).comp includeRight) x✝
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
⊢ 0 ≤ star c * x * c

Tactic:
;

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
⊢ 0 ≤ star c * x * c
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 + y) * c

Tactic:
rw [mul_add, add_mul]

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 : 0 ≤ a
c : R
hc : IsSelfAdjoint c
⊢ 0 ≤ c * a * star c

Tactic:
;

Goal state after:
R : Type u_1
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a : R
ha : 0 ≤ a
c : R
hc : IsSelfAdjoint c
⊢ 0 ≤ c * a * star 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
⊢ ∀ (x y : ↥(iSup K)),
    Set.iUnionLift (fun i ↦ ↑(K i)) (fun i x ↦ (f i) x) compat ↑(iSup K) ⋯ (x + y) =
      Set.iUnionLift (fun i ↦ ↑(K i)) (fun i x ↦ (f i) x) compat ↑(iSup K) ⋯ x +
        Set.iUnionLift (fun i ↦ ↑(K i)) (fun i x ↦ (f i) x) compat ↑(iSup K) ⋯ y

Tactic:
dsimp
        apply Set.iUnionLift_binary (coe_iSup_of_directed (K := K) dir) dir _ (fun _ => (· + ·))
        all_goals 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 : ι
h : K i ≤ T
x✝ : ↥(K i)
⊢ ((iSupLift K dir f hf T hT).comp (inclusion h)) x✝ = (f i) x✝

Tactic:
;

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
ι : 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✝
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
⊢ M ≃ₗ[R] Fin n → R

Tactic:
haveI := nontrivial_of_invariantBasisNumber R

Goal state after:
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
⊢ M ≃ₗ[R] Fin n → R
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
⊢ Module.rank R M ≤ 0 ↔ ∀ (x : M), x = 0

Tactic:
;

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
⊢ Module.rank R M ≤ 0 ↔ ∀ (x : M), x = 0
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
⊢ Module.rank R M = 0 ↔ ∀ (x : M), x = 0

Tactic:
;

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
⊢ Module.rank R M = 0 ↔ ∀ (x : M), x = 0
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Nontrivial R
s : Submodule R M
h : 0 < 0
eq : s = ⊥
⊢ False

Tactic:
;

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Nontrivial R
s : Submodule R M
h : 0 < 0
eq : s = ⊥
⊢ False
Module: Mathlib.LinearAlgebra.Dimension.Constructions

Goal state before:
pp: case e'_3
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type u_2
inst✝ : Fintype ι
v : ι → M
hv : span R (range v) = ⊤
⊢ (range v).toFinset.card = Fintype.card ↑(range v)

Tactic:
;

Goal state after:
case e'_3
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type u_2
inst✝ : Fintype ι
v : ι → M
hv : span R (range v) = ⊤
⊢ (range v).toFinset.card = Fintype.card ↑(range v)
Module: Mathlib.LinearAlgebra.Dimension.Constructions

Goal state before:
pp: case hsp
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
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)
b : m ⊕ n → V := Sum.elim (fun i ↦ ↑(bW i)) (surjInv ⋯ ∘ ⇑bQ)
br : ⇑W.mkQ ∘ b ∘ Sum.inr = ⇑bQ
⊢ ⊤ ≤ span R (⇑W.subtype '' range fun i ↦ bW i) ⊔ span R (range (surjInv ⋯ ∘ ⇑bQ))

Tactic:
← Submodule.map_span,

Goal state after:
case hsp
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
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)
b : m ⊕ n → V := Sum.elim (fun i ↦ ↑(bW i)) (surjInv ⋯ ∘ ⇑bQ)
br : ⇑W.mkQ ∘ b ∘ Sum.inr = ⇑bQ
⊢ ⊤ ≤ Submodule.map W.subtype (span R (range fun i ↦ bW i)) ⊔ span R (range (surjInv ⋯ ∘ ⇑bQ))
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: 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 < #t
g : ↥t → R
sum : ∑ i, g i • ↑i = 0
z : ↥t
nonzero : g z ≠ 0
⊢ ∑ i, extend Subtype.val g 0 ↑i • ↑i = 0

Tactic:
;

Goal state after:
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 < #t
g : ↥t → R
sum : ∑ i, g i • ↑i = 0
z : ↥t
nonzero : g z ≠ 0
⊢ ∑ i, extend Subtype.val g 0 ↑i • ↑i = 0
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: case a
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 < #t
g : ↥t → R
sum : ∑ i, g i • ↑i = 0
z : ↥t
nonzero : g z ≠ 0
x✝ : ↑↑t
a✝ : x✝ ∈ Finset.univ
⊢ extend Subtype.val g 0 ↑x✝ = g x✝

Tactic:
;

Goal state after:
case a
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 < #t
g : ↥t → R
sum : ∑ i, g i • ↑i = 0
z : ↥t
nonzero : g z ≠ 0
x✝ : ↑↑t
a✝ : x✝ ∈ Finset.univ
⊢ extend Subtype.val g 0 ↑x✝ = g x✝
Module: Mathlib.Algebra.Star.NonUnitalSubalgebra

Goal state before:
pp: case mk
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
q : NonUnitalStarSubalgebra R A
toNonUnitalSubalgebra✝ : NonUnitalSubalgebra R A
star_mem'✝ : ∀ {a : A}, a ∈ toNonUnitalSubalgebra✝.carrier → star a ∈ toNonUnitalSubalgebra✝.carrier
h : (fun {s} ↦ s.carrier) = fun {s} ↦ s.carrier
⊢ { toNonUnitalSubalgebra := toNonUnitalSubalgebra✝, star_mem' := star_mem'✝ } = q

Tactic:
;

Goal state after:
case mk
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
q : NonUnitalStarSubalgebra R A
toNonUnitalSubalgebra✝ : NonUnitalSubalgebra R A
star_mem'✝ : ∀ {a : A}, a ∈ toNonUnitalSubalgebra✝.carrier → star a ∈ toNonUnitalSubalgebra✝.carrier
h : (fun {s} ↦ s.carrier) = fun {s} ↦ s.carrier
⊢ { toNonUnitalSubalgebra := toNonUnitalSubalgebra✝, star_mem' := star_mem'✝ } = q
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: 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 < #t
⊢ ∃ f, ∑ e ∈ t, f e • e = 0 ∧ ∃ x ∈ t, f x ≠ 0

Tactic:
by
  obtain ⟨g, sum, z, nonzero⟩ := Fintype.not_linearIndependent_iff.mp
    (mt LinearIndependent.finset_card_le_finrank h.not_ge)
  refine ⟨Subtype.val.extend g 0, ?_, z, z.2, by rwa [Subtype.val_injective.extend_apply]⟩
  rw [← Finset.sum_finset_coe]; convert! sum; apply Subtype.val_injective.extend_apply

Goal state after: