[GOAL]
R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarSemigroup 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) ∈ selfAdjoint A
[PROOFSTEP]
simp only [selfAdjoint.mem_iff, star_smul, add_comm, StarAddMonoid.star_add, star_inv', star_bit0, star_one, star_star,
  star_invOf (2 : R), star_trivial]
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarSemigroup R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
x y : A
⊢ (fun x => { val := ⅟2 • (x + star x), property := (_ : ⅟2 • (x + star x) ∈ selfAdjoint A) }) (x + y) =
    (fun x => { val := ⅟2 • (x + star x), property := (_ : ⅟2 • (x + star x) ∈ selfAdjoint A) }) x +
      (fun x => { val := ⅟2 • (x + star x), property := (_ : ⅟2 • (x + star x) ∈ selfAdjoint A) }) y
[PROOFSTEP]
ext
[GOAL]
case a
R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarSemigroup R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
x y : A
⊢ ↑((fun x => { val := ⅟2 • (x + star x), property := (_ : ⅟2 • (x + star x) ∈ selfAdjoint A) }) (x + y)) =
    ↑((fun x => { val := ⅟2 • (x + star x), property := (_ : ⅟2 • (x + star x) ∈ selfAdjoint A) }) x +
        (fun x => { val := ⅟2 • (x + star x), property := (_ : ⅟2 • (x + star x) ∈ selfAdjoint A) }) y)
[PROOFSTEP]
simp [add_add_add_comm]
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarSemigroup R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
r : R
x : A
⊢ AddHom.toFun
      { toFun := fun x => { val := ⅟2 • (x + star x), property := (_ : ⅟2 • (x + star x) ∈ selfAdjoint A) },
        map_add' :=
          (_ :
            ∀ (x y : A),
              (fun x => { val := ⅟2 • (x + star x), property := (_ : ⅟2 • (x + star x) ∈ selfAdjoint A) }) (x + y) =
                (fun x => { val := ⅟2 • (x + star x), property := (_ : ⅟2 • (x + star x) ∈ selfAdjoint A) }) x +
                  (fun x => { val := ⅟2 • (x + star x), property := (_ : ⅟2 • (x + star x) ∈ selfAdjoint A) }) y) }
      (r • x) =
    ↑(RingHom.id R) r •
      AddHom.toFun
        { toFun := fun x => { val := ⅟2 • (x + star x), property := (_ : ⅟2 • (x + star x) ∈ selfAdjoint A) },
          map_add' :=
            (_ :
              ∀ (x y : A),
                (fun x => { val := ⅟2 • (x + star x), property := (_ : ⅟2 • (x + star x) ∈ selfAdjoint A) }) (x + y) =
                  (fun x => { val := ⅟2 • (x + star x), property := (_ : ⅟2 • (x + star x) ∈ selfAdjoint A) }) x +
                    (fun x => { val := ⅟2 • (x + star x), property := (_ : ⅟2 • (x + star x) ∈ selfAdjoint A) }) y) }
        x
[PROOFSTEP]
ext
[GOAL]
case a
R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarSemigroup R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
r : R
x : A
⊢ ↑(AddHom.toFun
        { toFun := fun x => { val := ⅟2 • (x + star x), property := (_ : ⅟2 • (x + star x) ∈ selfAdjoint A) },
          map_add' :=
            (_ :
              ∀ (x y : A),
                (fun x => { val := ⅟2 • (x + star x), property := (_ : ⅟2 • (x + star x) ∈ selfAdjoint A) }) (x + y) =
                  (fun x => { val := ⅟2 • (x + star x), property := (_ : ⅟2 • (x + star x) ∈ selfAdjoint A) }) x +
                    (fun x => { val := ⅟2 • (x + star x), property := (_ : ⅟2 • (x + star x) ∈ selfAdjoint A) }) y) }
        (r • x)) =
    ↑(↑(RingHom.id R) r •
        AddHom.toFun
          { toFun := fun x => { val := ⅟2 • (x + star x), property := (_ : ⅟2 • (x + star x) ∈ selfAdjoint A) },
            map_add' :=
              (_ :
                ∀ (x y : A),
                  (fun x => { val := ⅟2 • (x + star x), property := (_ : ⅟2 • (x + star x) ∈ selfAdjoint A) }) (x + y) =
                    (fun x => { val := ⅟2 • (x + star x), property := (_ : ⅟2 • (x + star x) ∈ selfAdjoint A) }) x +
                      (fun x => { val := ⅟2 • (x + star x), property := (_ : ⅟2 • (x + star x) ∈ selfAdjoint A) }) y) }
          x)
[PROOFSTEP]
simp [← mul_smul, show ⅟2 * r = r * ⅟2 from Commute.invOf_left <| (2 : ℕ).cast_commute r]
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarSemigroup 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
[PROOFSTEP]
simp only [skewAdjoint.mem_iff, star_smul, star_sub, star_star, star_trivial, ← smul_neg, neg_sub]
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarSemigroup R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
x y : A
⊢ (fun x => { val := ⅟2 • (x - star x), property := (_ : ⅟2 • (x - star x) ∈ skewAdjoint A) }) (x + y) =
    (fun x => { val := ⅟2 • (x - star x), property := (_ : ⅟2 • (x - star x) ∈ skewAdjoint A) }) x +
      (fun x => { val := ⅟2 • (x - star x), property := (_ : ⅟2 • (x - star x) ∈ skewAdjoint A) }) y
[PROOFSTEP]
ext
[GOAL]
case a
R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarSemigroup R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
x y : A
⊢ ↑((fun x => { val := ⅟2 • (x - star x), property := (_ : ⅟2 • (x - star x) ∈ skewAdjoint A) }) (x + y)) =
    ↑((fun x => { val := ⅟2 • (x - star x), property := (_ : ⅟2 • (x - star x) ∈ skewAdjoint A) }) x +
        (fun x => { val := ⅟2 • (x - star x), property := (_ : ⅟2 • (x - star x) ∈ skewAdjoint A) }) y)
[PROOFSTEP]
simp only [sub_add, ← smul_add, sub_sub_eq_add_sub, star_add, AddSubgroup.coe_mk, AddSubgroup.coe_add]
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarSemigroup R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
r : R
x : A
⊢ AddHom.toFun
      { toFun := fun x => { val := ⅟2 • (x - star x), property := (_ : ⅟2 • (x - star x) ∈ skewAdjoint A) },
        map_add' :=
          (_ :
            ∀ (x y : A),
              (fun x => { val := ⅟2 • (x - star x), property := (_ : ⅟2 • (x - star x) ∈ skewAdjoint A) }) (x + y) =
                (fun x => { val := ⅟2 • (x - star x), property := (_ : ⅟2 • (x - star x) ∈ skewAdjoint A) }) x +
                  (fun x => { val := ⅟2 • (x - star x), property := (_ : ⅟2 • (x - star x) ∈ skewAdjoint A) }) y) }
      (r • x) =
    ↑(RingHom.id R) r •
      AddHom.toFun
        { toFun := fun x => { val := ⅟2 • (x - star x), property := (_ : ⅟2 • (x - star x) ∈ skewAdjoint A) },
          map_add' :=
            (_ :
              ∀ (x y : A),
                (fun x => { val := ⅟2 • (x - star x), property := (_ : ⅟2 • (x - star x) ∈ skewAdjoint A) }) (x + y) =
                  (fun x => { val := ⅟2 • (x - star x), property := (_ : ⅟2 • (x - star x) ∈ skewAdjoint A) }) x +
                    (fun x => { val := ⅟2 • (x - star x), property := (_ : ⅟2 • (x - star x) ∈ skewAdjoint A) }) y) }
        x
[PROOFSTEP]
ext
[GOAL]
case a
R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarSemigroup R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
r : R
x : A
⊢ ↑(AddHom.toFun
        { toFun := fun x => { val := ⅟2 • (x - star x), property := (_ : ⅟2 • (x - star x) ∈ skewAdjoint A) },
          map_add' :=
            (_ :
              ∀ (x y : A),
                (fun x => { val := ⅟2 • (x - star x), property := (_ : ⅟2 • (x - star x) ∈ skewAdjoint A) }) (x + y) =
                  (fun x => { val := ⅟2 • (x - star x), property := (_ : ⅟2 • (x - star x) ∈ skewAdjoint A) }) x +
                    (fun x => { val := ⅟2 • (x - star x), property := (_ : ⅟2 • (x - star x) ∈ skewAdjoint A) }) y) }
        (r • x)) =
    ↑(↑(RingHom.id R) r •
        AddHom.toFun
          { toFun := fun x => { val := ⅟2 • (x - star x), property := (_ : ⅟2 • (x - star x) ∈ skewAdjoint A) },
            map_add' :=
              (_ :
                ∀ (x y : A),
                  (fun x => { val := ⅟2 • (x - star x), property := (_ : ⅟2 • (x - star x) ∈ skewAdjoint A) }) (x + y) =
                    (fun x => { val := ⅟2 • (x - star x), property := (_ : ⅟2 • (x - star x) ∈ skewAdjoint A) }) x +
                      (fun x => { val := ⅟2 • (x - star x), property := (_ : ⅟2 • (x - star x) ∈ skewAdjoint A) }) y) }
          x)
[PROOFSTEP]
simp [← mul_smul, ← smul_sub, show r * ⅟2 = ⅟2 * r from Commute.invOf_right <| (2 : ℕ).commute_cast r]
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarSemigroup R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
x : A
⊢ ↑(↑(selfAdjointPart R) x) + ↑(↑(skewAdjointPart R) x) = x
[PROOFSTEP]
simp only [smul_sub, selfAdjointPart_apply_coe, smul_add, skewAdjointPart_apply_coe, add_add_sub_cancel,
  invOf_two_smul_add_invOf_two_smul]
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarSemigroup R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
x : A
hx : IsSelfAdjoint x
⊢ ↑(↑(selfAdjointPart R) x) = x
[PROOFSTEP]
rw [selfAdjointPart_apply_coe, hx.star_eq, smul_add, invOf_two_smul_add_invOf_two_smul]
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarSemigroup R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
x : A
hx : IsSelfAdjoint x
⊢ ↑(↑(skewAdjointPart R) x) = ↑0
[PROOFSTEP]
rw [skewAdjointPart_apply_coe, hx.star_eq, sub_self, smul_zero, ZeroMemClass.coe_zero]
  -- porting note: todo: make it a `simp`
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarSemigroup R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
x✝ : { x // x ∈ skewAdjoint.submodule R A }
x : A
hx : star x = -x
⊢ ↑(↑(LinearMap.comp (selfAdjointPart R) (Submodule.subtype (skewAdjoint.submodule R A)))
        { val := x, property := hx }) =
    ↑(↑0 { val := x, property := hx })
[PROOFSTEP]
simp [hx]
  -- porting note: todo: make it a `simp`
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarSemigroup R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
x✝ : { x // x ∈ skewAdjoint.submodule R A }
x : A
hx : star x = -x
⊢ ↑(↑(LinearMap.comp (skewAdjointPart R) (Submodule.subtype (skewAdjoint.submodule R A)))
        { val := x, property := hx }) =
    ↑(↑LinearMap.id { val := x, property := hx })
[PROOFSTEP]
simp only [LinearMap.comp_apply, Submodule.subtype_apply, skewAdjointPart_apply_coe, hx, sub_neg_eq_add, smul_add,
  invOf_two_smul_add_invOf_two_smul]
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarSemigroup R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
x✝ : { x // x ∈ skewAdjoint.submodule R A }
x : A
hx : star x = -x
⊢ x = ↑(↑LinearMap.id { val := x, property := hx })
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarSemigroup R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
⊢ A ≃ₗ[R] { x // x ∈ selfAdjoint A } × { x // x ∈ skewAdjoint A }
[PROOFSTEP]
refine
  LinearEquiv.ofLinear ((selfAdjointPart R).prod (skewAdjointPart R))
    (LinearMap.coprod ((selfAdjoint.submodule R A).subtype) (skewAdjoint.submodule R A).subtype) ?_
    (LinearMap.ext <| StarModule.selfAdjointPart_add_skewAdjointPart R)
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarSemigroup R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
⊢ LinearMap.comp (LinearMap.prod (selfAdjointPart R) (skewAdjointPart R))
      (LinearMap.coprod (Submodule.subtype (selfAdjoint.submodule R A))
        (Submodule.subtype (skewAdjoint.submodule R A))) =
    LinearMap.id
[PROOFSTEP]
ext
[GOAL]
case hl.h.h₁.a
R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarSemigroup R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
x✝ : { x // x ∈ selfAdjoint A }
⊢ ↑(↑(LinearMap.comp
              (LinearMap.comp (LinearMap.prod (selfAdjointPart R) (skewAdjointPart R))
                (LinearMap.coprod (Submodule.subtype (selfAdjoint.submodule R A))
                  (Submodule.subtype (skewAdjoint.submodule R A))))
              (LinearMap.inl R { x // x ∈ selfAdjoint A } { x // x ∈ skewAdjoint A }))
          x✝).fst =
    ↑(↑(LinearMap.comp LinearMap.id (LinearMap.inl R { x // x ∈ selfAdjoint A } { x // x ∈ skewAdjoint A })) x✝).fst
[PROOFSTEP]
simp
[GOAL]
case hl.h.h₂.a
R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarSemigroup R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
x✝ : { x // x ∈ selfAdjoint A }
⊢ ↑(↑(LinearMap.comp
              (LinearMap.comp (LinearMap.prod (selfAdjointPart R) (skewAdjointPart R))
                (LinearMap.coprod (Submodule.subtype (selfAdjoint.submodule R A))
                  (Submodule.subtype (skewAdjoint.submodule R A))))
              (LinearMap.inl R { x // x ∈ selfAdjoint A } { x // x ∈ skewAdjoint A }))
          x✝).snd =
    ↑(↑(LinearMap.comp LinearMap.id (LinearMap.inl R { x // x ∈ selfAdjoint A } { x // x ∈ skewAdjoint A })) x✝).snd
[PROOFSTEP]
simp
[GOAL]
case hr.h.h₁.a
R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarSemigroup R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
x✝ : { x // x ∈ skewAdjoint A }
⊢ ↑(↑(LinearMap.comp
              (LinearMap.comp (LinearMap.prod (selfAdjointPart R) (skewAdjointPart R))
                (LinearMap.coprod (Submodule.subtype (selfAdjoint.submodule R A))
                  (Submodule.subtype (skewAdjoint.submodule R A))))
              (LinearMap.inr R { x // x ∈ selfAdjoint A } { x // x ∈ skewAdjoint A }))
          x✝).fst =
    ↑(↑(LinearMap.comp LinearMap.id (LinearMap.inr R { x // x ∈ selfAdjoint A } { x // x ∈ skewAdjoint A })) x✝).fst
[PROOFSTEP]
simp
[GOAL]
case hr.h.h₂.a
R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarSemigroup R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
x✝ : { x // x ∈ skewAdjoint A }
⊢ ↑(↑(LinearMap.comp
              (LinearMap.comp (LinearMap.prod (selfAdjointPart R) (skewAdjointPart R))
                (LinearMap.coprod (Submodule.subtype (selfAdjoint.submodule R A))
                  (Submodule.subtype (skewAdjoint.submodule R A))))
              (LinearMap.inr R { x // x ∈ selfAdjoint A } { x // x ∈ skewAdjoint A }))
          x✝).snd =
    ↑(↑(LinearMap.comp LinearMap.id (LinearMap.inr R { x // x ∈ selfAdjoint A } { x // x ∈ skewAdjoint A })) x✝).snd
[PROOFSTEP]
simp
[GOAL]
R✝ : Type u_1
A✝ : Type u_2
inst✝¹³ : Semiring R✝
inst✝¹² : StarSemigroup R✝
inst✝¹¹ : TrivialStar R✝
inst✝¹⁰ : AddCommGroup A✝
inst✝⁹ : Module R✝ A✝
inst✝⁸ : StarAddMonoid A✝
inst✝⁷ : StarModule R✝ A✝
inst✝⁶ : Invertible 2
R : Type u_3
A : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : StarSemigroup A
inst✝¹ : Algebra R A
inst✝ : StarModule R A
r : R
⊢ ↑(algebraMap R A) (star r) = star (↑(algebraMap R A) r)
[PROOFSTEP]
simp only [Algebra.algebraMap_eq_smul_one, star_smul, star_one]


[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : Semiring α
h : ∀ (a : α), a + a = a
src✝ : Semiring α := inst✝
a b c : α
hab : a ≤ b
hbc : b ≤ c
⊢ a ≤ c
[PROOFSTEP]
simp only
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : Semiring α
h : ∀ (a : α), a + a = a
src✝ : Semiring α := inst✝
a b c : α
hab : a ≤ b
hbc : b ≤ c
⊢ a + c = c
[PROOFSTEP]
rw [← hbc, ← add_assoc, hab]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : Semiring α
h : ∀ (a : α), a + a = a
src✝ : Semiring α := inst✝
a b : α
hab : a ≤ b
hba : b ≤ a
⊢ a = b
[PROOFSTEP]
rwa [← hba, add_comm]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : Semiring α
h : ∀ (a : α), a + a = a
src✝ : Semiring α := inst✝
a b : α
⊢ a ≤ a ⊔ b
[PROOFSTEP]
simp only
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : Semiring α
h : ∀ (a : α), a + a = a
src✝ : Semiring α := inst✝
a b : α
⊢ a + (a + b) = a + b
[PROOFSTEP]
rw [← add_assoc, h]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : Semiring α
h : ∀ (a : α), a + a = a
src✝ : Semiring α := inst✝
a b : α
⊢ b ≤ a ⊔ b
[PROOFSTEP]
simp only
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : Semiring α
h : ∀ (a : α), a + a = a
src✝ : Semiring α := inst✝
a b : α
⊢ b + (a + b) = a + b
[PROOFSTEP]
rw [add_comm, add_assoc, h]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : Semiring α
h : ∀ (a : α), a + a = a
src✝ : Semiring α := inst✝
a b c : α
hab : a ≤ c
hbc : b ≤ c
⊢ a ⊔ b ≤ c
[PROOFSTEP]
simp only
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : Semiring α
h : ∀ (a : α), a + a = a
src✝ : Semiring α := inst✝
a b c : α
hab : a ≤ c
hbc : b ≤ c
⊢ a + b + c = c
[PROOFSTEP]
rwa [add_assoc, hbc]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : IdemSemiring α
a✝ b c a : α
⊢ a + a = a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : IdemSemiring α
a✝ b c : α
n : ℕ
x✝ : n + 2 ≠ 0
a : α
⊢ (n + 2) • a = a
[PROOFSTEP]
rw [succ_nsmul, nsmul_eq_self n.succ_ne_zero, add_idem]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : IdemSemiring α
a b c : α
⊢ a + b = a ↔ b ≤ a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : IdemSemiring α
a b c : α
⊢ a + b = b ↔ a ≤ b
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : IdemSemiring α
a b c : α
⊢ a + b ≤ c ↔ a ≤ c ∧ b ≤ c
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : IdemSemiring α
a✝ b✝ c✝ : α
src✝ : IdemSemiring α := inst✝
a b : α
hbc : a ≤ b
c : α
⊢ c + a ≤ c + b
[PROOFSTEP]
simp_rw [add_eq_sup]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : IdemSemiring α
a✝ b✝ c✝ : α
src✝ : IdemSemiring α := inst✝
a b : α
hbc : a ≤ b
c : α
⊢ c ⊔ a ≤ c ⊔ b
[PROOFSTEP]
exact sup_le_sup_left hbc _
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : IdemSemiring α
a✝ b✝ c : α
src✝ : IdemSemiring α := inst✝
a b : α
⊢ a + (a + b) = a + b
[PROOFSTEP]
rw [← add_assoc, add_idem]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : IdemSemiring α
a✝ b✝ c✝ a b c : α
hbc : b ≤ c
⊢ a * c + a * b = a * c
[PROOFSTEP]
rw [← mul_add, hbc.add_eq_left]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : IdemSemiring α
a✝ b✝ c✝ a b c : α
hbc : b ≤ c
⊢ swap (fun x x_1 => x * x_1) a c + swap (fun x x_1 => x * x_1) a b = swap (fun x x_1 => x * x_1) a c
[PROOFSTEP]
rw [← add_mul, hbc.add_eq_left]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : KleeneAlgebra α
a b c : α
hb : 1 ≤ b
⊢ b * a ≤ b → a∗ ≤ b
[PROOFSTEP]
simpa using mul_kstar_le hb
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : KleeneAlgebra α
a b c : α
hb : 1 ≤ b
⊢ a * b ≤ b → a∗ ≤ b
[PROOFSTEP]
simpa using kstar_mul_le hb
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : KleeneAlgebra α
a b c : α
h : a ≤ 1
⊢ 1 * a ≤ 1
[PROOFSTEP]
rwa [one_mul]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : KleeneAlgebra α
a b c : α
h : a∗ = a
⊢ a * a = a
[PROOFSTEP]
rw [← h, kstar_mul_kstar]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : KleeneAlgebra α
a b c : α
n : ℕ
⊢ a ^ (n + 1) ≤ a∗
[PROOFSTEP]
rw [pow_succ]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : KleeneAlgebra α
a b c : α
n : ℕ
⊢ a * a ^ n ≤ a∗
[PROOFSTEP]
exact (mul_le_mul_left' pow_le_kstar _).trans mul_kstar_le_kstar
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝⁹ : IdemSemiring α
inst✝⁸ : Zero β
inst✝⁷ : One β
inst✝⁶ : Add β
inst✝⁵ : Mul β
inst✝⁴ : Pow β ℕ
inst✝³ : SMul ℕ β
inst✝² : NatCast β
inst✝¹ : Sup β
inst✝ : Bot β
f : β → α
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
nsmul : ∀ (x : β) (n : ℕ), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
sup : ∀ (a b : β), f (a ⊔ b) = f a ⊔ f b
bot : f ⊥ = ⊥
src✝² : Semiring β := Injective.semiring f hf zero one add mul nsmul npow nat_cast
src✝¹ : SemilatticeSup β := Injective.semilatticeSup f hf sup
src✝ : Bot β := inst✝
a b : β
⊢ f (a + b) = f (a ⊔ b)
[PROOFSTEP]
erw [sup, add, add_eq_sup]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝¹⁰ : KleeneAlgebra α
inst✝⁹ : Zero β
inst✝⁸ : One β
inst✝⁷ : Add β
inst✝⁶ : Mul β
inst✝⁵ : Pow β ℕ
inst✝⁴ : SMul ℕ β
inst✝³ : NatCast β
inst✝² : Sup β
inst✝¹ : Bot β
inst✝ : KStar β
f : β → α
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
nsmul : ∀ (x : β) (n : ℕ), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
sup : ∀ (a b : β), f (a ⊔ b) = f a ⊔ f b
bot : f ⊥ = ⊥
kstar : ∀ (a : β), f a∗ = (f a)∗
src✝¹ : IdemSemiring β := Injective.idemSemiring f hf zero one add mul nsmul npow nat_cast sup bot
src✝ : KStar β := inst✝
a : β
⊢ 1 ≤ f a∗
[PROOFSTEP]
erw [kstar]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝¹⁰ : KleeneAlgebra α
inst✝⁹ : Zero β
inst✝⁸ : One β
inst✝⁷ : Add β
inst✝⁶ : Mul β
inst✝⁵ : Pow β ℕ
inst✝⁴ : SMul ℕ β
inst✝³ : NatCast β
inst✝² : Sup β
inst✝¹ : Bot β
inst✝ : KStar β
f : β → α
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
nsmul : ∀ (x : β) (n : ℕ), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
sup : ∀ (a b : β), f (a ⊔ b) = f a ⊔ f b
bot : f ⊥ = ⊥
kstar : ∀ (a : β), f a∗ = (f a)∗
src✝¹ : IdemSemiring β := Injective.idemSemiring f hf zero one add mul nsmul npow nat_cast sup bot
src✝ : KStar β := inst✝
a : β
⊢ 1 ≤ (f a)∗
[PROOFSTEP]
exact one_le_kstar
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝¹⁰ : KleeneAlgebra α
inst✝⁹ : Zero β
inst✝⁸ : One β
inst✝⁷ : Add β
inst✝⁶ : Mul β
inst✝⁵ : Pow β ℕ
inst✝⁴ : SMul ℕ β
inst✝³ : NatCast β
inst✝² : Sup β
inst✝¹ : Bot β
inst✝ : KStar β
f : β → α
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
nsmul : ∀ (x : β) (n : ℕ), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
sup : ∀ (a b : β), f (a ⊔ b) = f a ⊔ f b
bot : f ⊥ = ⊥
kstar : ∀ (a : β), f a∗ = (f a)∗
src✝¹ : IdemSemiring β := Injective.idemSemiring f hf zero one add mul nsmul npow nat_cast sup bot
src✝ : KStar β := inst✝
a : β
⊢ a * a∗ ≤ a∗
[PROOFSTEP]
change f _ ≤ _
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝¹⁰ : KleeneAlgebra α
inst✝⁹ : Zero β
inst✝⁸ : One β
inst✝⁷ : Add β
inst✝⁶ : Mul β
inst✝⁵ : Pow β ℕ
inst✝⁴ : SMul ℕ β
inst✝³ : NatCast β
inst✝² : Sup β
inst✝¹ : Bot β
inst✝ : KStar β
f : β → α
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
nsmul : ∀ (x : β) (n : ℕ), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
sup : ∀ (a b : β), f (a ⊔ b) = f a ⊔ f b
bot : f ⊥ = ⊥
kstar : ∀ (a : β), f a∗ = (f a)∗
src✝¹ : IdemSemiring β := Injective.idemSemiring f hf zero one add mul nsmul npow nat_cast sup bot
src✝ : KStar β := inst✝
a : β
⊢ f (a * a∗) ≤ f a∗
[PROOFSTEP]
erw [mul, kstar]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝¹⁰ : KleeneAlgebra α
inst✝⁹ : Zero β
inst✝⁸ : One β
inst✝⁷ : Add β
inst✝⁶ : Mul β
inst✝⁵ : Pow β ℕ
inst✝⁴ : SMul ℕ β
inst✝³ : NatCast β
inst✝² : Sup β
inst✝¹ : Bot β
inst✝ : KStar β
f : β → α
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
nsmul : ∀ (x : β) (n : ℕ), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
sup : ∀ (a b : β), f (a ⊔ b) = f a ⊔ f b
bot : f ⊥ = ⊥
kstar : ∀ (a : β), f a∗ = (f a)∗
src✝¹ : IdemSemiring β := Injective.idemSemiring f hf zero one add mul nsmul npow nat_cast sup bot
src✝ : KStar β := inst✝
a : β
⊢ f a * (f a)∗ ≤ (f a)∗
[PROOFSTEP]
exact mul_kstar_le_kstar
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝¹⁰ : KleeneAlgebra α
inst✝⁹ : Zero β
inst✝⁸ : One β
inst✝⁷ : Add β
inst✝⁶ : Mul β
inst✝⁵ : Pow β ℕ
inst✝⁴ : SMul ℕ β
inst✝³ : NatCast β
inst✝² : Sup β
inst✝¹ : Bot β
inst✝ : KStar β
f : β → α
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
nsmul : ∀ (x : β) (n : ℕ), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
sup : ∀ (a b : β), f (a ⊔ b) = f a ⊔ f b
bot : f ⊥ = ⊥
kstar : ∀ (a : β), f a∗ = (f a)∗
src✝¹ : IdemSemiring β := Injective.idemSemiring f hf zero one add mul nsmul npow nat_cast sup bot
src✝ : KStar β := inst✝
a : β
⊢ a∗ * a ≤ a∗
[PROOFSTEP]
change f _ ≤ _
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝¹⁰ : KleeneAlgebra α
inst✝⁹ : Zero β
inst✝⁸ : One β
inst✝⁷ : Add β
inst✝⁶ : Mul β
inst✝⁵ : Pow β ℕ
inst✝⁴ : SMul ℕ β
inst✝³ : NatCast β
inst✝² : Sup β
inst✝¹ : Bot β
inst✝ : KStar β
f : β → α
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
nsmul : ∀ (x : β) (n : ℕ), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
sup : ∀ (a b : β), f (a ⊔ b) = f a ⊔ f b
bot : f ⊥ = ⊥
kstar : ∀ (a : β), f a∗ = (f a)∗
src✝¹ : IdemSemiring β := Injective.idemSemiring f hf zero one add mul nsmul npow nat_cast sup bot
src✝ : KStar β := inst✝
a : β
⊢ f (a∗ * a) ≤ f a∗
[PROOFSTEP]
erw [mul, kstar]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝¹⁰ : KleeneAlgebra α
inst✝⁹ : Zero β
inst✝⁸ : One β
inst✝⁷ : Add β
inst✝⁶ : Mul β
inst✝⁵ : Pow β ℕ
inst✝⁴ : SMul ℕ β
inst✝³ : NatCast β
inst✝² : Sup β
inst✝¹ : Bot β
inst✝ : KStar β
f : β → α
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
nsmul : ∀ (x : β) (n : ℕ), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
sup : ∀ (a b : β), f (a ⊔ b) = f a ⊔ f b
bot : f ⊥ = ⊥
kstar : ∀ (a : β), f a∗ = (f a)∗
src✝¹ : IdemSemiring β := Injective.idemSemiring f hf zero one add mul nsmul npow nat_cast sup bot
src✝ : KStar β := inst✝
a : β
⊢ (f a)∗ * f a ≤ (f a)∗
[PROOFSTEP]
exact kstar_mul_le_kstar
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝¹⁰ : KleeneAlgebra α
inst✝⁹ : Zero β
inst✝⁸ : One β
inst✝⁷ : Add β
inst✝⁶ : Mul β
inst✝⁵ : Pow β ℕ
inst✝⁴ : SMul ℕ β
inst✝³ : NatCast β
inst✝² : Sup β
inst✝¹ : Bot β
inst✝ : KStar β
f : β → α
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
nsmul : ∀ (x : β) (n : ℕ), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
sup : ∀ (a b : β), f (a ⊔ b) = f a ⊔ f b
bot : f ⊥ = ⊥
kstar : ∀ (a : β), f a∗ = (f a)∗
src✝¹ : IdemSemiring β := Injective.idemSemiring f hf zero one add mul nsmul npow nat_cast sup bot
src✝ : KStar β := inst✝
a b : β
h : f (b * a) ≤ f b
⊢ b * a∗ ≤ b
[PROOFSTEP]
change f _ ≤ _
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝¹⁰ : KleeneAlgebra α
inst✝⁹ : Zero β
inst✝⁸ : One β
inst✝⁷ : Add β
inst✝⁶ : Mul β
inst✝⁵ : Pow β ℕ
inst✝⁴ : SMul ℕ β
inst✝³ : NatCast β
inst✝² : Sup β
inst✝¹ : Bot β
inst✝ : KStar β
f : β → α
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
nsmul : ∀ (x : β) (n : ℕ), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
sup : ∀ (a b : β), f (a ⊔ b) = f a ⊔ f b
bot : f ⊥ = ⊥
kstar : ∀ (a : β), f a∗ = (f a)∗
src✝¹ : IdemSemiring β := Injective.idemSemiring f hf zero one add mul nsmul npow nat_cast sup bot
src✝ : KStar β := inst✝
a b : β
h : f (b * a) ≤ f b
⊢ f (b * a∗) ≤ f b
[PROOFSTEP]
erw [mul, kstar]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝¹⁰ : KleeneAlgebra α
inst✝⁹ : Zero β
inst✝⁸ : One β
inst✝⁷ : Add β
inst✝⁶ : Mul β
inst✝⁵ : Pow β ℕ
inst✝⁴ : SMul ℕ β
inst✝³ : NatCast β
inst✝² : Sup β
inst✝¹ : Bot β
inst✝ : KStar β
f : β → α
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
nsmul : ∀ (x : β) (n : ℕ), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
sup : ∀ (a b : β), f (a ⊔ b) = f a ⊔ f b
bot : f ⊥ = ⊥
kstar : ∀ (a : β), f a∗ = (f a)∗
src✝¹ : IdemSemiring β := Injective.idemSemiring f hf zero one add mul nsmul npow nat_cast sup bot
src✝ : KStar β := inst✝
a b : β
h : f (b * a) ≤ f b
⊢ f b * (f a)∗ ≤ f b
[PROOFSTEP]
erw [mul] at h
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝¹⁰ : KleeneAlgebra α
inst✝⁹ : Zero β
inst✝⁸ : One β
inst✝⁷ : Add β
inst✝⁶ : Mul β
inst✝⁵ : Pow β ℕ
inst✝⁴ : SMul ℕ β
inst✝³ : NatCast β
inst✝² : Sup β
inst✝¹ : Bot β
inst✝ : KStar β
f : β → α
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
nsmul : ∀ (x : β) (n : ℕ), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
sup : ∀ (a b : β), f (a ⊔ b) = f a ⊔ f b
bot : f ⊥ = ⊥
kstar : ∀ (a : β), f a∗ = (f a)∗
src✝¹ : IdemSemiring β := Injective.idemSemiring f hf zero one add mul nsmul npow nat_cast sup bot
src✝ : KStar β := inst✝
a b : β
h : f b * f a ≤ f b
⊢ f b * (f a)∗ ≤ f b
[PROOFSTEP]
exact mul_kstar_le_self h
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝¹⁰ : KleeneAlgebra α
inst✝⁹ : Zero β
inst✝⁸ : One β
inst✝⁷ : Add β
inst✝⁶ : Mul β
inst✝⁵ : Pow β ℕ
inst✝⁴ : SMul ℕ β
inst✝³ : NatCast β
inst✝² : Sup β
inst✝¹ : Bot β
inst✝ : KStar β
f : β → α
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
nsmul : ∀ (x : β) (n : ℕ), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
sup : ∀ (a b : β), f (a ⊔ b) = f a ⊔ f b
bot : f ⊥ = ⊥
kstar : ∀ (a : β), f a∗ = (f a)∗
src✝¹ : IdemSemiring β := Injective.idemSemiring f hf zero one add mul nsmul npow nat_cast sup bot
src✝ : KStar β := inst✝
a b : β
h : f (a * b) ≤ f b
⊢ a∗ * b ≤ b
[PROOFSTEP]
change f _ ≤ _
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝¹⁰ : KleeneAlgebra α
inst✝⁹ : Zero β
inst✝⁸ : One β
inst✝⁷ : Add β
inst✝⁶ : Mul β
inst✝⁵ : Pow β ℕ
inst✝⁴ : SMul ℕ β
inst✝³ : NatCast β
inst✝² : Sup β
inst✝¹ : Bot β
inst✝ : KStar β
f : β → α
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
nsmul : ∀ (x : β) (n : ℕ), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
sup : ∀ (a b : β), f (a ⊔ b) = f a ⊔ f b
bot : f ⊥ = ⊥
kstar : ∀ (a : β), f a∗ = (f a)∗
src✝¹ : IdemSemiring β := Injective.idemSemiring f hf zero one add mul nsmul npow nat_cast sup bot
src✝ : KStar β := inst✝
a b : β
h : f (a * b) ≤ f b
⊢ f (a∗ * b) ≤ f b
[PROOFSTEP]
erw [mul, kstar]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝¹⁰ : KleeneAlgebra α
inst✝⁹ : Zero β
inst✝⁸ : One β
inst✝⁷ : Add β
inst✝⁶ : Mul β
inst✝⁵ : Pow β ℕ
inst✝⁴ : SMul ℕ β
inst✝³ : NatCast β
inst✝² : Sup β
inst✝¹ : Bot β
inst✝ : KStar β
f : β → α
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
nsmul : ∀ (x : β) (n : ℕ), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
sup : ∀ (a b : β), f (a ⊔ b) = f a ⊔ f b
bot : f ⊥ = ⊥
kstar : ∀ (a : β), f a∗ = (f a)∗
src✝¹ : IdemSemiring β := Injective.idemSemiring f hf zero one add mul nsmul npow nat_cast sup bot
src✝ : KStar β := inst✝
a b : β
h : f (a * b) ≤ f b
⊢ (f a)∗ * f b ≤ f b
[PROOFSTEP]
erw [mul] at h
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝¹⁰ : KleeneAlgebra α
inst✝⁹ : Zero β
inst✝⁸ : One β
inst✝⁷ : Add β
inst✝⁶ : Mul β
inst✝⁵ : Pow β ℕ
inst✝⁴ : SMul ℕ β
inst✝³ : NatCast β
inst✝² : Sup β
inst✝¹ : Bot β
inst✝ : KStar β
f : β → α
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
nsmul : ∀ (x : β) (n : ℕ), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
sup : ∀ (a b : β), f (a ⊔ b) = f a ⊔ f b
bot : f ⊥ = ⊥
kstar : ∀ (a : β), f a∗ = (f a)∗
src✝¹ : IdemSemiring β := Injective.idemSemiring f hf zero one add mul nsmul npow nat_cast sup bot
src✝ : KStar β := inst✝
a b : β
h : f a * f b ≤ f b
⊢ (f a)∗ * f b ≤ f b
[PROOFSTEP]
exact kstar_mul_le_self h


[GOAL]
x y : ℤ
⊢ |x| < |y| ↔ natAbs x < natAbs y
[PROOFSTEP]
rw [abs_eq_natAbs, abs_eq_natAbs, ofNat_lt]


[GOAL]
R : Type u
inst✝ : CommRing R
A₀ A₁ B₀ B₁ : R
A₀_inv : A₀ ^ 2 = 1
A₁_inv : A₁ ^ 2 = 1
B₀_inv : B₀ ^ 2 = 1
B₁_inv : B₁ ^ 2 = 1
⊢ (2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁) * (2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁) =
    4 * (2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁)
[PROOFSTEP]
rw [← sub_eq_zero]
[GOAL]
R : Type u
inst✝ : CommRing R
A₀ A₁ B₀ B₁ : R
A₀_inv : A₀ ^ 2 = 1
A₁_inv : A₁ ^ 2 = 1
B₀_inv : B₀ ^ 2 = 1
B₁_inv : B₁ ^ 2 = 1
⊢ (2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁) * (2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁) -
      4 * (2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁) =
    0
[PROOFSTEP]
repeat'
  ring_nf
  simp only [A₁_inv, B₁_inv, sub_eq_add_neg, add_mul, mul_add, sub_mul, mul_sub, add_assoc, neg_add, neg_sub, sub_add,
    sub_sub, neg_mul, ← sq, A₀_inv, B₀_inv, ← sq, ← mul_assoc, one_mul, mul_one, add_right_neg, add_zero,
    sub_eq_add_neg, A₀_inv, mul_one, add_right_neg, zero_mul]
[GOAL]
R : Type u
inst✝ : CommRing R
A₀ A₁ B₀ B₁ : R
A₀_inv : A₀ ^ 2 = 1
A₁_inv : A₁ ^ 2 = 1
B₀_inv : B₀ ^ 2 = 1
B₁_inv : B₁ ^ 2 = 1
⊢ (2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁) * (2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁) -
      4 * (2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁) =
    0
[PROOFSTEP]
ring_nf
[GOAL]
R : Type u
inst✝ : CommRing R
A₀ A₁ B₀ B₁ : R
A₀_inv : A₀ ^ 2 = 1
A₁_inv : A₁ ^ 2 = 1
B₀_inv : B₀ ^ 2 = 1
B₁_inv : B₁ ^ 2 = 1
⊢ -4 + (A₀ * B₀ ^ 2 * A₁ * 2 - A₀ * B₁ ^ 2 * A₁ * 2) + A₀ ^ 2 * B₀ * B₁ * 2 + A₀ ^ 2 * B₀ ^ 2 +
          (A₀ ^ 2 * B₁ ^ 2 - B₀ * B₁ * A₁ ^ 2 * 2) +
        B₀ ^ 2 * A₁ ^ 2 +
      B₁ ^ 2 * A₁ ^ 2 =
    0
[PROOFSTEP]
simp only [A₁_inv, B₁_inv, sub_eq_add_neg, add_mul, mul_add, sub_mul, mul_sub, add_assoc, neg_add, neg_sub, sub_add,
  sub_sub, neg_mul, ← sq, A₀_inv, B₀_inv, ← sq, ← mul_assoc, one_mul, mul_one, add_right_neg, add_zero, sub_eq_add_neg,
  A₀_inv, mul_one, add_right_neg, zero_mul]
[GOAL]
R : Type u
inst✝ : CommRing R
A₀ A₁ B₀ B₁ : R
A₀_inv : A₀ ^ 2 = 1
A₁_inv : A₁ ^ 2 = 1
B₀_inv : B₀ ^ 2 = 1
B₁_inv : B₁ ^ 2 = 1
⊢ -4 + (B₀ * B₁ * 2 + (1 ^ 2 + (1 ^ 2 + (-(B₀ * B₁ * 2) + (1 ^ 2 + 1 ^ 2))))) = 0
[PROOFSTEP]
ring_nf
[GOAL]

[PROOFSTEP]
simp only [A₁_inv, B₁_inv, sub_eq_add_neg, add_mul, mul_add, sub_mul, mul_sub, add_assoc, neg_add, neg_sub, sub_add,
  sub_sub, neg_mul, ← sq, A₀_inv, B₀_inv, ← sq, ← mul_assoc, one_mul, mul_one, add_right_neg, add_zero, sub_eq_add_neg,
  A₀_inv, mul_one, add_right_neg, zero_mul]
[GOAL]
R : Type u
inst✝³ : OrderedCommRing R
inst✝² : StarOrderedRing R
inst✝¹ : Algebra ℝ R
inst✝ : OrderedSMul ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
⊢ A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁ ≤ 2
[PROOFSTEP]
let P := 2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁
[GOAL]
R : Type u
inst✝³ : OrderedCommRing R
inst✝² : StarOrderedRing R
inst✝¹ : Algebra ℝ R
inst✝ : OrderedSMul ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
P : R := 2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁
⊢ A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁ ≤ 2
[PROOFSTEP]
have i₁ : 0 ≤ P := by
  have idem : P * P = 4 * P := CHSH_id T.A₀_inv T.A₁_inv T.B₀_inv T.B₁_inv
  have idem' : P = (1 / 4 : ℝ) • (P * P) :=
    by
    have h : 4 * P = (4 : ℝ) • P := by simp [Algebra.smul_def]
    rw [idem, h, ← mul_smul]
    norm_num
  have sa : star P = P := by
    dsimp
    simp only [star_add, star_sub, star_mul, star_ofNat, star_one, T.A₀_sa, T.A₁_sa, T.B₀_sa, T.B₁_sa, mul_comm B₀,
      mul_comm B₁]
  rw [idem']
  conv_rhs =>
    arg 2
    arg 1
    rw [← sa]
  convert smul_le_smul_of_nonneg (R := ℝ) (star_mul_self_nonneg P) _
  · simp
  · norm_num
[GOAL]
R : Type u
inst✝³ : OrderedCommRing R
inst✝² : StarOrderedRing R
inst✝¹ : Algebra ℝ R
inst✝ : OrderedSMul ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
P : R := 2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁
⊢ 0 ≤ P
[PROOFSTEP]
have idem : P * P = 4 * P := CHSH_id T.A₀_inv T.A₁_inv T.B₀_inv T.B₁_inv
[GOAL]
R : Type u
inst✝³ : OrderedCommRing R
inst✝² : StarOrderedRing R
inst✝¹ : Algebra ℝ R
inst✝ : OrderedSMul ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
P : R := 2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁
idem : P * P = 4 * P
⊢ 0 ≤ P
[PROOFSTEP]
have idem' : P = (1 / 4 : ℝ) • (P * P) :=
  by
  have h : 4 * P = (4 : ℝ) • P := by simp [Algebra.smul_def]
  rw [idem, h, ← mul_smul]
  norm_num
[GOAL]
R : Type u
inst✝³ : OrderedCommRing R
inst✝² : StarOrderedRing R
inst✝¹ : Algebra ℝ R
inst✝ : OrderedSMul ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
P : R := 2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁
idem : P * P = 4 * P
⊢ P = (1 / 4) • (P * P)
[PROOFSTEP]
have h : 4 * P = (4 : ℝ) • P := by simp [Algebra.smul_def]
[GOAL]
R : Type u
inst✝³ : OrderedCommRing R
inst✝² : StarOrderedRing R
inst✝¹ : Algebra ℝ R
inst✝ : OrderedSMul ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
P : R := 2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁
idem : P * P = 4 * P
⊢ 4 * P = 4 • P
[PROOFSTEP]
simp [Algebra.smul_def]
[GOAL]
R : Type u
inst✝³ : OrderedCommRing R
inst✝² : StarOrderedRing R
inst✝¹ : Algebra ℝ R
inst✝ : OrderedSMul ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
P : R := 2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁
idem : P * P = 4 * P
h : 4 * P = 4 • P
⊢ P = (1 / 4) • (P * P)
[PROOFSTEP]
rw [idem, h, ← mul_smul]
[GOAL]
R : Type u
inst✝³ : OrderedCommRing R
inst✝² : StarOrderedRing R
inst✝¹ : Algebra ℝ R
inst✝ : OrderedSMul ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
P : R := 2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁
idem : P * P = 4 * P
h : 4 * P = 4 • P
⊢ P = (1 / 4 * 4) • P
[PROOFSTEP]
norm_num
[GOAL]
R : Type u
inst✝³ : OrderedCommRing R
inst✝² : StarOrderedRing R
inst✝¹ : Algebra ℝ R
inst✝ : OrderedSMul ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
P : R := 2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁
idem : P * P = 4 * P
idem' : P = (1 / 4) • (P * P)
⊢ 0 ≤ P
[PROOFSTEP]
have sa : star P = P := by
  dsimp
  simp only [star_add, star_sub, star_mul, star_ofNat, star_one, T.A₀_sa, T.A₁_sa, T.B₀_sa, T.B₁_sa, mul_comm B₀,
    mul_comm B₁]
[GOAL]
R : Type u
inst✝³ : OrderedCommRing R
inst✝² : StarOrderedRing R
inst✝¹ : Algebra ℝ R
inst✝ : OrderedSMul ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
P : R := 2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁
idem : P * P = 4 * P
idem' : P = (1 / 4) • (P * P)
⊢ star P = P
[PROOFSTEP]
dsimp
[GOAL]
R : Type u
inst✝³ : OrderedCommRing R
inst✝² : StarOrderedRing R
inst✝¹ : Algebra ℝ R
inst✝ : OrderedSMul ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
P : R := 2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁
idem : P * P = 4 * P
idem' : P = (1 / 4) • (P * P)
⊢ star (2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁) = 2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁
[PROOFSTEP]
simp only [star_add, star_sub, star_mul, star_ofNat, star_one, T.A₀_sa, T.A₁_sa, T.B₀_sa, T.B₁_sa, mul_comm B₀,
  mul_comm B₁]
[GOAL]
R : Type u
inst✝³ : OrderedCommRing R
inst✝² : StarOrderedRing R
inst✝¹ : Algebra ℝ R
inst✝ : OrderedSMul ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
P : R := 2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁
idem : P * P = 4 * P
idem' : P = (1 / 4) • (P * P)
sa : star P = P
⊢ 0 ≤ P
[PROOFSTEP]
rw [idem']
[GOAL]
R : Type u
inst✝³ : OrderedCommRing R
inst✝² : StarOrderedRing R
inst✝¹ : Algebra ℝ R
inst✝ : OrderedSMul ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
P : R := 2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁
idem : P * P = 4 * P
idem' : P = (1 / 4) • (P * P)
sa : star P = P
⊢ 0 ≤ (1 / 4) • (P * P)
[PROOFSTEP]
conv_rhs =>
  arg 2
  arg 1
  rw [← sa]
[GOAL]
R : Type u
inst✝³ : OrderedCommRing R
inst✝² : StarOrderedRing R
inst✝¹ : Algebra ℝ R
inst✝ : OrderedSMul ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
P : R := 2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁
idem : P * P = 4 * P
idem' : P = (1 / 4) • (P * P)
sa : star P = P
| (1 / 4) • (P * P)
[PROOFSTEP]
  arg 2
  arg 1
  rw [← sa]
[GOAL]
R : Type u
inst✝³ : OrderedCommRing R
inst✝² : StarOrderedRing R
inst✝¹ : Algebra ℝ R
inst✝ : OrderedSMul ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
P : R := 2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁
idem : P * P = 4 * P
idem' : P = (1 / 4) • (P * P)
sa : star P = P
| (1 / 4) • (P * P)
[PROOFSTEP]
  arg 2
  arg 1
  rw [← sa]
[GOAL]
R : Type u
inst✝³ : OrderedCommRing R
inst✝² : StarOrderedRing R
inst✝¹ : Algebra ℝ R
inst✝ : OrderedSMul ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
P : R := 2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁
idem : P * P = 4 * P
idem' : P = (1 / 4) • (P * P)
sa : star P = P
| (1 / 4) • (P * P)
[PROOFSTEP]
arg 2
[GOAL]
R : Type u
inst✝³ : OrderedCommRing R
inst✝² : StarOrderedRing R
inst✝¹ : Algebra ℝ R
inst✝ : OrderedSMul ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
P : R := 2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁
idem : P * P = 4 * P
idem' : P = (1 / 4) • (P * P)
sa : star P = P
| P * P
[PROOFSTEP]
arg 1
[GOAL]
R : Type u
inst✝³ : OrderedCommRing R
inst✝² : StarOrderedRing R
inst✝¹ : Algebra ℝ R
inst✝ : OrderedSMul ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
P : R := 2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁
idem : P * P = 4 * P
idem' : P = (1 / 4) • (P * P)
sa : star P = P
| P
[PROOFSTEP]
rw [← sa]
[GOAL]
R : Type u
inst✝³ : OrderedCommRing R
inst✝² : StarOrderedRing R
inst✝¹ : Algebra ℝ R
inst✝ : OrderedSMul ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
P : R := 2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁
idem : P * P = 4 * P
idem' : P = (1 / 4) • (P * P)
sa : star P = P
⊢ 0 ≤ (1 / 4) • (star P * P)
[PROOFSTEP]
convert smul_le_smul_of_nonneg (R := ℝ) (star_mul_self_nonneg P) _
[GOAL]
case h.e'_3
R : Type u
inst✝³ : OrderedCommRing R
inst✝² : StarOrderedRing R
inst✝¹ : Algebra ℝ R
inst✝ : OrderedSMul ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
P : R := 2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁
idem : P * P = 4 * P
idem' : P = (1 / 4) • (P * P)
sa : star P = P
⊢ 0 = (1 / 4) • 0
[PROOFSTEP]
simp
[GOAL]
case convert_2
R : Type u
inst✝³ : OrderedCommRing R
inst✝² : StarOrderedRing R
inst✝¹ : Algebra ℝ R
inst✝ : OrderedSMul ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
P : R := 2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁
idem : P * P = 4 * P
idem' : P = (1 / 4) • (P * P)
sa : star P = P
⊢ 0 ≤ 1 / 4
[PROOFSTEP]
norm_num
[GOAL]
R : Type u
inst✝³ : OrderedCommRing R
inst✝² : StarOrderedRing R
inst✝¹ : Algebra ℝ R
inst✝ : OrderedSMul ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
P : R := 2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁
i₁ : 0 ≤ P
⊢ A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁ ≤ 2
[PROOFSTEP]
apply le_of_sub_nonneg
[GOAL]
case a
R : Type u
inst✝³ : OrderedCommRing R
inst✝² : StarOrderedRing R
inst✝¹ : Algebra ℝ R
inst✝ : OrderedSMul ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
P : R := 2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁
i₁ : 0 ≤ P
⊢ 0 ≤ 2 - (A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁)
[PROOFSTEP]
simpa only [sub_add_eq_sub_sub, ← sub_add] using i₁
[GOAL]
R : Type u
⊢ Real.sqrt 2 * Real.sqrt 2 ^ 3 = Real.sqrt 2 * (2 * (Real.sqrt 2)⁻¹ + 4 * ((Real.sqrt 2)⁻¹ * 2⁻¹))
[PROOFSTEP]
ring_nf
[GOAL]
R : Type u
⊢ Real.sqrt 2 ^ 4 = Real.sqrt 2 * (Real.sqrt 2)⁻¹ * 4
[PROOFSTEP]
rw [mul_inv_cancel (ne_of_gt (Real.sqrt_pos.2 (show (2 : ℝ) > 0 by norm_num)))]
[GOAL]
R : Type u
⊢ 2 > 0
[PROOFSTEP]
norm_num
[GOAL]
R : Type u
⊢ Real.sqrt 2 ^ 4 = 1 * 4
[PROOFSTEP]
convert congr_arg (· ^ 2) (@Real.sq_sqrt 2 (by norm_num)) using 1
[GOAL]
R : Type u
⊢ 0 ≤ 2
[PROOFSTEP]
norm_num
[GOAL]
case h.e'_2
R : Type u
⊢ Real.sqrt 2 ^ 4 = (Real.sqrt 2 ^ 2) ^ 2
[PROOFSTEP]
try simp only [← pow_mul]
[GOAL]
case h.e'_2
R : Type u
⊢ Real.sqrt 2 ^ 4 = (Real.sqrt 2 ^ 2) ^ 2
[PROOFSTEP]
simp only [← pow_mul]
[GOAL]
case h.e'_3
R : Type u
⊢ 1 * 4 = 2 ^ 2
[PROOFSTEP]
try simp only [← pow_mul]
[GOAL]
case h.e'_3
R : Type u
⊢ 1 * 4 = 2 ^ 2
[PROOFSTEP]
simp only [← pow_mul]
[GOAL]
case h.e'_2
R : Type u
⊢ Real.sqrt 2 ^ 4 = Real.sqrt 2 ^ (2 * 2)
[PROOFSTEP]
norm_num
[GOAL]
case h.e'_3
R : Type u
⊢ 1 * 4 = 2 ^ 2
[PROOFSTEP]
norm_num
[GOAL]
R : Type u
⊢ (Real.sqrt 2)⁻¹ * (Real.sqrt 2)⁻¹ = 2⁻¹
[PROOFSTEP]
rw [← mul_inv]
[GOAL]
R : Type u
⊢ (Real.sqrt 2 * Real.sqrt 2)⁻¹ = 2⁻¹
[PROOFSTEP]
norm_num
[GOAL]
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
⊢ A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁ ≤ Real.sqrt 2 ^ 3 • 1
[PROOFSTEP]
have M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = ((m : ℝ) * a) • x := fun m a x => by
  rw [zsmul_eq_smul_cast ℝ, ← mul_smul]
[GOAL]
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
m : ℤ
a : ℝ
x : R
⊢ m • a • x = (↑m * a) • x
[PROOFSTEP]
rw [zsmul_eq_smul_cast ℝ, ← mul_smul]
[GOAL]
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
⊢ A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁ ≤ Real.sqrt 2 ^ 3 • 1
[PROOFSTEP]
let P := √2⁻¹ • (A₁ + A₀) - B₀
[GOAL]
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
⊢ A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁ ≤ Real.sqrt 2 ^ 3 • 1
[PROOFSTEP]
let Q := √2⁻¹ • (A₁ - A₀) + B₁
[GOAL]
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
⊢ A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁ ≤ Real.sqrt 2 ^ 3 • 1
[PROOFSTEP]
have w : √2 ^ 3 • (1 : R) - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = √2⁻¹ • (P ^ 2 + Q ^ 2) :=
  by
  dsimp
    -- distribute out all the powers and products appearing on the RHS
  simp only [sq, sub_mul, mul_sub, add_mul, mul_add, smul_add, smul_sub]
    -- pull all coefficients out to the front, and combine `√2`s where possible
  simp only [Algebra.mul_smul_comm, Algebra.smul_mul_assoc, ← mul_smul, sqrt_two_inv_mul_self]
    -- replace Aᵢ * Aᵢ = 1 and Bᵢ * Bᵢ = 1
  simp only [← sq, T.A₀_inv, T.A₁_inv, T.B₀_inv, T.B₁_inv]
    -- move Aᵢ to the left of Bᵢ
  simp only [← T.A₀B₀_commutes, ← T.A₀B₁_commutes, ← T.A₁B₀_commutes, ← T.A₁B₁_commutes]
    -- collect terms, simplify coefficients, and collect terms again:
  abel_nf
    -- all terms coincide, but the last one. Simplify all other terms
  simp only [M]
  simp only [neg_mul, one_mul, mul_inv_cancel_of_invertible, Int.cast_one, add_assoc, add_comm, add_left_comm, one_smul,
    Int.cast_neg, neg_smul, Int.int_cast_ofNat]
  simp only [← add_assoc, ← add_smul]
    -- just look at the coefficients now:
  congr
  exact mul_left_cancel₀ (by norm_num) tsirelson_inequality_aux
[GOAL]
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
⊢ Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
[PROOFSTEP]
dsimp
  -- distribute out all the powers and products appearing on the RHS
[GOAL]
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
⊢ Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ =
    (Real.sqrt 2)⁻¹ • (((Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀) ^ 2 + ((Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁) ^ 2)
[PROOFSTEP]
simp only [sq, sub_mul, mul_sub, add_mul, mul_add, smul_add, smul_sub]
  -- pull all coefficients out to the front, and combine `√2`s where possible
[GOAL]
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
⊢ Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ =
    (Real.sqrt 2)⁻¹ • ((Real.sqrt 2)⁻¹ • A₁ * (Real.sqrt 2)⁻¹ • A₁) +
              (Real.sqrt 2)⁻¹ • ((Real.sqrt 2)⁻¹ • A₀ * (Real.sqrt 2)⁻¹ • A₁) -
            (Real.sqrt 2)⁻¹ • (B₀ * (Real.sqrt 2)⁻¹ • A₁) +
          ((Real.sqrt 2)⁻¹ • ((Real.sqrt 2)⁻¹ • A₁ * (Real.sqrt 2)⁻¹ • A₀) +
              (Real.sqrt 2)⁻¹ • ((Real.sqrt 2)⁻¹ • A₀ * (Real.sqrt 2)⁻¹ • A₀) -
            (Real.sqrt 2)⁻¹ • (B₀ * (Real.sqrt 2)⁻¹ • A₀)) -
        ((Real.sqrt 2)⁻¹ • ((Real.sqrt 2)⁻¹ • A₁ * B₀) + (Real.sqrt 2)⁻¹ • ((Real.sqrt 2)⁻¹ • A₀ * B₀) -
          (Real.sqrt 2)⁻¹ • (B₀ * B₀)) +
      ((Real.sqrt 2)⁻¹ • ((Real.sqrt 2)⁻¹ • A₁ * (Real.sqrt 2)⁻¹ • A₁) -
              (Real.sqrt 2)⁻¹ • ((Real.sqrt 2)⁻¹ • A₀ * (Real.sqrt 2)⁻¹ • A₁) +
            (Real.sqrt 2)⁻¹ • (B₁ * (Real.sqrt 2)⁻¹ • A₁) -
          ((Real.sqrt 2)⁻¹ • ((Real.sqrt 2)⁻¹ • A₁ * (Real.sqrt 2)⁻¹ • A₀) -
              (Real.sqrt 2)⁻¹ • ((Real.sqrt 2)⁻¹ • A₀ * (Real.sqrt 2)⁻¹ • A₀) +
            (Real.sqrt 2)⁻¹ • (B₁ * (Real.sqrt 2)⁻¹ • A₀)) +
        ((Real.sqrt 2)⁻¹ • ((Real.sqrt 2)⁻¹ • A₁ * B₁) - (Real.sqrt 2)⁻¹ • ((Real.sqrt 2)⁻¹ • A₀ * B₁) +
          (Real.sqrt 2)⁻¹ • (B₁ * B₁)))
[PROOFSTEP]
simp only [Algebra.mul_smul_comm, Algebra.smul_mul_assoc, ← mul_smul, sqrt_two_inv_mul_self]
  -- replace Aᵢ * Aᵢ = 1 and Bᵢ * Bᵢ = 1
[GOAL]
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
⊢ Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ =
    ((Real.sqrt 2)⁻¹ * 2⁻¹) • (A₁ * A₁) + ((Real.sqrt 2)⁻¹ * 2⁻¹) • (A₀ * A₁) - 2⁻¹ • (B₀ * A₁) +
          (((Real.sqrt 2)⁻¹ * 2⁻¹) • (A₁ * A₀) + ((Real.sqrt 2)⁻¹ * 2⁻¹) • (A₀ * A₀) - 2⁻¹ • (B₀ * A₀)) -
        (2⁻¹ • (A₁ * B₀) + 2⁻¹ • (A₀ * B₀) - (Real.sqrt 2)⁻¹ • (B₀ * B₀)) +
      (((Real.sqrt 2)⁻¹ * 2⁻¹) • (A₁ * A₁) - ((Real.sqrt 2)⁻¹ * 2⁻¹) • (A₀ * A₁) + 2⁻¹ • (B₁ * A₁) -
          (((Real.sqrt 2)⁻¹ * 2⁻¹) • (A₁ * A₀) - ((Real.sqrt 2)⁻¹ * 2⁻¹) • (A₀ * A₀) + 2⁻¹ • (B₁ * A₀)) +
        (2⁻¹ • (A₁ * B₁) - 2⁻¹ • (A₀ * B₁) + (Real.sqrt 2)⁻¹ • (B₁ * B₁)))
[PROOFSTEP]
simp only [← sq, T.A₀_inv, T.A₁_inv, T.B₀_inv, T.B₁_inv]
  -- move Aᵢ to the left of Bᵢ
[GOAL]
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
⊢ Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ =
    ((Real.sqrt 2)⁻¹ * 2⁻¹) • 1 + ((Real.sqrt 2)⁻¹ * 2⁻¹) • (A₀ * A₁) - 2⁻¹ • (B₀ * A₁) +
          (((Real.sqrt 2)⁻¹ * 2⁻¹) • (A₁ * A₀) + ((Real.sqrt 2)⁻¹ * 2⁻¹) • 1 - 2⁻¹ • (B₀ * A₀)) -
        (2⁻¹ • (A₁ * B₀) + 2⁻¹ • (A₀ * B₀) - (Real.sqrt 2)⁻¹ • 1) +
      (((Real.sqrt 2)⁻¹ * 2⁻¹) • 1 - ((Real.sqrt 2)⁻¹ * 2⁻¹) • (A₀ * A₁) + 2⁻¹ • (B₁ * A₁) -
          (((Real.sqrt 2)⁻¹ * 2⁻¹) • (A₁ * A₀) - ((Real.sqrt 2)⁻¹ * 2⁻¹) • 1 + 2⁻¹ • (B₁ * A₀)) +
        (2⁻¹ • (A₁ * B₁) - 2⁻¹ • (A₀ * B₁) + (Real.sqrt 2)⁻¹ • 1))
[PROOFSTEP]
simp only [← T.A₀B₀_commutes, ← T.A₀B₁_commutes, ← T.A₁B₀_commutes, ← T.A₁B₁_commutes]
  -- collect terms, simplify coefficients, and collect terms again:
[GOAL]
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
⊢ Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ =
    ((Real.sqrt 2)⁻¹ * 2⁻¹) • 1 + ((Real.sqrt 2)⁻¹ * 2⁻¹) • (A₀ * A₁) - 2⁻¹ • (A₁ * B₀) +
          (((Real.sqrt 2)⁻¹ * 2⁻¹) • (A₁ * A₀) + ((Real.sqrt 2)⁻¹ * 2⁻¹) • 1 - 2⁻¹ • (A₀ * B₀)) -
        (2⁻¹ • (A₁ * B₀) + 2⁻¹ • (A₀ * B₀) - (Real.sqrt 2)⁻¹ • 1) +
      (((Real.sqrt 2)⁻¹ * 2⁻¹) • 1 - ((Real.sqrt 2)⁻¹ * 2⁻¹) • (A₀ * A₁) + 2⁻¹ • (A₁ * B₁) -
          (((Real.sqrt 2)⁻¹ * 2⁻¹) • (A₁ * A₀) - ((Real.sqrt 2)⁻¹ * 2⁻¹) • 1 + 2⁻¹ • (A₀ * B₁)) +
        (2⁻¹ • (A₁ * B₁) - 2⁻¹ • (A₀ * B₁) + (Real.sqrt 2)⁻¹ • 1))
[PROOFSTEP]
abel_nf
  -- all terms coincide, but the last one. Simplify all other terms
[GOAL]
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
⊢ Real.sqrt 2 ^ 3 • 1 + (-1 • (A₀ * B₀) + (-1 • (A₀ * B₁) + (-1 • (A₁ * B₀) + A₁ * B₁))) =
    4 • ((Real.sqrt 2)⁻¹ * 2⁻¹) • 1 +
      (-2 • 2⁻¹ • (A₁ * B₀) +
        (-2 • 2⁻¹ • (A₀ * B₀) + (2 • (Real.sqrt 2)⁻¹ • 1 + (2 • 2⁻¹ • (A₁ * B₁) + -2 • 2⁻¹ • (A₀ * B₁)))))
[PROOFSTEP]
simp only [M]
[GOAL]
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
⊢ Real.sqrt 2 ^ 3 • 1 + (-1 • (A₀ * B₀) + (-1 • (A₀ * B₁) + (-1 • (A₁ * B₀) + A₁ * B₁))) =
    (↑4 * ((Real.sqrt 2)⁻¹ * 2⁻¹)) • 1 +
      ((↑(-2) * 2⁻¹) • (A₁ * B₀) +
        ((↑(-2) * 2⁻¹) • (A₀ * B₀) +
          ((↑2 * (Real.sqrt 2)⁻¹) • 1 + ((↑2 * 2⁻¹) • (A₁ * B₁) + (↑(-2) * 2⁻¹) • (A₀ * B₁)))))
[PROOFSTEP]
simp only [neg_mul, one_mul, mul_inv_cancel_of_invertible, Int.cast_one, add_assoc, add_comm, add_left_comm, one_smul,
  Int.cast_neg, neg_smul, Int.int_cast_ofNat]
[GOAL]
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
⊢ A₁ * B₁ + (-(A₀ * B₀) + (-(A₀ * B₁) + (-(A₁ * B₀) + Real.sqrt 2 ^ 3 • 1))) =
    A₁ * B₁ +
      (-(A₀ * B₀) + (-(A₀ * B₁) + (-(A₁ * B₀) + ((2 * (Real.sqrt 2)⁻¹) • 1 + (4 * ((Real.sqrt 2)⁻¹ * 2⁻¹)) • 1))))
[PROOFSTEP]
simp only [← add_assoc, ← add_smul]
  -- just look at the coefficients now:
[GOAL]
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
⊢ A₁ * B₁ + -(A₀ * B₀) + -(A₀ * B₁) + -(A₁ * B₀) + Real.sqrt 2 ^ 3 • 1 =
    A₁ * B₁ + -(A₀ * B₀) + -(A₀ * B₁) + -(A₁ * B₀) + (2 * (Real.sqrt 2)⁻¹ + 4 * ((Real.sqrt 2)⁻¹ * 2⁻¹)) • 1
[PROOFSTEP]
congr
[GOAL]
case e_a.e_a
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
⊢ Real.sqrt 2 ^ 3 = 2 * (Real.sqrt 2)⁻¹ + 4 * ((Real.sqrt 2)⁻¹ * 2⁻¹)
[PROOFSTEP]
exact mul_left_cancel₀ (by norm_num) tsirelson_inequality_aux
[GOAL]
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
⊢ Real.sqrt 2 ≠ 0
[PROOFSTEP]
norm_num
[GOAL]
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
w : Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
⊢ A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁ ≤ Real.sqrt 2 ^ 3 • 1
[PROOFSTEP]
have pos : 0 ≤ √2⁻¹ • (P ^ 2 + Q ^ 2) :=
  by
  have P_sa : star P = P := by
    simp only [star_smul, star_add, star_sub, star_id_of_comm, T.A₀_sa, T.A₁_sa, T.B₀_sa, T.B₁_sa]
  have Q_sa : star Q = Q := by
    simp only [star_smul, star_add, star_sub, star_id_of_comm, T.A₀_sa, T.A₁_sa, T.B₀_sa, T.B₁_sa]
  have P2_nonneg : 0 ≤ P ^ 2 := by
    rw [sq]
    conv =>
      congr
      skip
      congr
      rw [← P_sa]
    convert (star_mul_self_nonneg P)
  have Q2_nonneg : 0 ≤ Q ^ 2 := by
    rw [sq]
    conv =>
      congr
      skip
      congr
      rw [← Q_sa]
    convert (star_mul_self_nonneg Q)
  convert
    smul_le_smul_of_nonneg (add_nonneg P2_nonneg Q2_nonneg)
      (le_of_lt (show 0 < √2⁻¹ by norm_num))
        -- `norm_num` can't directly show `0 ≤ √2⁻¹`
  simp
[GOAL]
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
w : Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
⊢ ↑0 ≤ (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
[PROOFSTEP]
have P_sa : star P = P := by
  simp only [star_smul, star_add, star_sub, star_id_of_comm, T.A₀_sa, T.A₁_sa, T.B₀_sa, T.B₁_sa]
[GOAL]
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
w : Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
⊢ star P = P
[PROOFSTEP]
simp only [star_smul, star_add, star_sub, star_id_of_comm, T.A₀_sa, T.A₁_sa, T.B₀_sa, T.B₁_sa]
[GOAL]
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
w : Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
P_sa : star P = P
⊢ ↑0 ≤ (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
[PROOFSTEP]
have Q_sa : star Q = Q := by
  simp only [star_smul, star_add, star_sub, star_id_of_comm, T.A₀_sa, T.A₁_sa, T.B₀_sa, T.B₁_sa]
[GOAL]
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
w : Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
P_sa : star P = P
⊢ star Q = Q
[PROOFSTEP]
simp only [star_smul, star_add, star_sub, star_id_of_comm, T.A₀_sa, T.A₁_sa, T.B₀_sa, T.B₁_sa]
[GOAL]
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
w : Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
P_sa : star P = P
Q_sa : star Q = Q
⊢ ↑0 ≤ (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
[PROOFSTEP]
have P2_nonneg : 0 ≤ P ^ 2 := by
  rw [sq]
  conv =>
    congr
    skip
    congr
    rw [← P_sa]
  convert (star_mul_self_nonneg P)
[GOAL]
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
w : Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
P_sa : star P = P
Q_sa : star Q = Q
⊢ 0 ≤ P ^ 2
[PROOFSTEP]
rw [sq]
[GOAL]
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
w : Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
P_sa : star P = P
Q_sa : star Q = Q
⊢ 0 ≤ P * P
[PROOFSTEP]
conv =>
  congr
  skip
  congr
  rw [← P_sa]
[GOAL]
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
w : Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
P_sa : star P = P
Q_sa : star Q = Q
| 0 ≤ P * P
[PROOFSTEP]
  congr
  skip
  congr
  rw [← P_sa]
[GOAL]
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
w : Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
P_sa : star P = P
Q_sa : star Q = Q
| 0 ≤ P * P
[PROOFSTEP]
  congr
  skip
  congr
  rw [← P_sa]
[GOAL]
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
w : Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
P_sa : star P = P
Q_sa : star Q = Q
| 0 ≤ P * P
[PROOFSTEP]
congr
[GOAL]
case a
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
w : Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
P_sa : star P = P
Q_sa : star Q = Q
| 0
case a
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
w : Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
P_sa : star P = P
Q_sa : star Q = Q
| P * P
[PROOFSTEP]
skip
[GOAL]
case a
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
w : Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
P_sa : star P = P
Q_sa : star Q = Q
| 0
case a
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
w : Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
P_sa : star P = P
Q_sa : star Q = Q
| P * P
[PROOFSTEP]
congr
[GOAL]
case a
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
w : Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
P_sa : star P = P
Q_sa : star Q = Q
| P * P
[PROOFSTEP]
rw [← P_sa]
[GOAL]
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
w : Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
P_sa : star P = P
Q_sa : star Q = Q
⊢ 0 ≤ star P * star P
[PROOFSTEP]
convert (star_mul_self_nonneg P)
[GOAL]
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
w : Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
P_sa : star P = P
Q_sa : star Q = Q
P2_nonneg : 0 ≤ P ^ 2
⊢ ↑0 ≤ (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
[PROOFSTEP]
have Q2_nonneg : 0 ≤ Q ^ 2 := by
  rw [sq]
  conv =>
    congr
    skip
    congr
    rw [← Q_sa]
  convert (star_mul_self_nonneg Q)
[GOAL]
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
w : Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
P_sa : star P = P
Q_sa : star Q = Q
P2_nonneg : 0 ≤ P ^ 2
⊢ 0 ≤ Q ^ 2
[PROOFSTEP]
rw [sq]
[GOAL]
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
w : Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
P_sa : star P = P
Q_sa : star Q = Q
P2_nonneg : 0 ≤ P ^ 2
⊢ 0 ≤ Q * Q
[PROOFSTEP]
conv =>
  congr
  skip
  congr
  rw [← Q_sa]
[GOAL]
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
w : Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
P_sa : star P = P
Q_sa : star Q = Q
P2_nonneg : 0 ≤ P ^ 2
| 0 ≤ Q * Q
[PROOFSTEP]
  congr
  skip
  congr
  rw [← Q_sa]
[GOAL]
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
w : Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
P_sa : star P = P
Q_sa : star Q = Q
P2_nonneg : 0 ≤ P ^ 2
| 0 ≤ Q * Q
[PROOFSTEP]
  congr
  skip
  congr
  rw [← Q_sa]
[GOAL]
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
w : Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
P_sa : star P = P
Q_sa : star Q = Q
P2_nonneg : 0 ≤ P ^ 2
| 0 ≤ Q * Q
[PROOFSTEP]
congr
[GOAL]
case a
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
w : Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
P_sa : star P = P
Q_sa : star Q = Q
P2_nonneg : 0 ≤ P ^ 2
| 0
case a
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
w : Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
P_sa : star P = P
Q_sa : star Q = Q
P2_nonneg : 0 ≤ P ^ 2
| Q * Q
[PROOFSTEP]
skip
[GOAL]
case a
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
w : Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
P_sa : star P = P
Q_sa : star Q = Q
P2_nonneg : 0 ≤ P ^ 2
| 0
case a
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
w : Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
P_sa : star P = P
Q_sa : star Q = Q
P2_nonneg : 0 ≤ P ^ 2
| Q * Q
[PROOFSTEP]
congr
[GOAL]
case a
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
w : Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
P_sa : star P = P
Q_sa : star Q = Q
P2_nonneg : 0 ≤ P ^ 2
| Q * Q
[PROOFSTEP]
rw [← Q_sa]
[GOAL]
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
w : Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
P_sa : star P = P
Q_sa : star Q = Q
P2_nonneg : 0 ≤ P ^ 2
⊢ 0 ≤ star Q * star Q
[PROOFSTEP]
convert (star_mul_self_nonneg Q)
[GOAL]
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
w : Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
P_sa : star P = P
Q_sa : star Q = Q
P2_nonneg : 0 ≤ P ^ 2
Q2_nonneg : 0 ≤ Q ^ 2
⊢ ↑0 ≤ (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
[PROOFSTEP]
convert
  smul_le_smul_of_nonneg (add_nonneg P2_nonneg Q2_nonneg)
    (le_of_lt (show 0 < √2⁻¹ by norm_num))
      -- `norm_num` can't directly show `0 ≤ √2⁻¹`
[GOAL]
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
w : Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
P_sa : star P = P
Q_sa : star Q = Q
P2_nonneg : 0 ≤ P ^ 2
Q2_nonneg : 0 ≤ Q ^ 2
⊢ 0 < (Real.sqrt 2)⁻¹
[PROOFSTEP]
norm_num
[GOAL]
case h.e'_3
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
w : Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
P_sa : star P = P
Q_sa : star Q = Q
P2_nonneg : 0 ≤ P ^ 2
Q2_nonneg : 0 ≤ Q ^ 2
⊢ ↑0 = (Real.sqrt 2)⁻¹ • 0
[PROOFSTEP]
simp
[GOAL]
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
w : Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
pos : ↑0 ≤ (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
⊢ A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁ ≤ Real.sqrt 2 ^ 3 • 1
[PROOFSTEP]
apply le_of_sub_nonneg
[GOAL]
case a
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
w : Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
pos : ↑0 ≤ (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
⊢ 0 ≤ Real.sqrt 2 ^ 3 • 1 - (A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁)
[PROOFSTEP]
simpa only [sub_add_eq_sub_sub, ← sub_add, w, Nat.cast_zero] using pos


[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
a : α
hs : IsUpperSet s
⊢ IsUpperSet (a • s)
[PROOFSTEP]
rintro _ y hxy ⟨x, hx, rfl⟩
[GOAL]
case intro.intro
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
a : α
hs : IsUpperSet s
y x : α
hx : x ∈ s
hxy : (fun x => a • x) x ≤ y
⊢ y ∈ a • s
[PROOFSTEP]
exact mem_smul_set_iff_inv_smul_mem.2 (hs (le_inv_mul_iff_mul_le.2 hxy) hx)
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
a : α
hs : OrdConnected s
⊢ OrdConnected (a • s)
[PROOFSTEP]
rw [← hs.upperClosure_inter_lowerClosure, smul_set_inter]
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
a : α
hs : OrdConnected s
⊢ OrdConnected (a • ↑(upperClosure s) ∩ a • ↑(lowerClosure s))
[PROOFSTEP]
exact (upperClosure _).upper.smul.ordConnected.inter (lowerClosure _).lower.smul.ordConnected
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
a : α
ht : IsUpperSet t
⊢ IsUpperSet (s * t)
[PROOFSTEP]
rw [← smul_eq_mul, ← Set.iUnion_smul_set]
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
a : α
ht : IsUpperSet t
⊢ IsUpperSet (⋃ (a : α) (_ : a ∈ s), a • t)
[PROOFSTEP]
exact isUpperSet_iUnion₂ fun x _ ↦ ht.smul
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
a : α
hs : IsUpperSet s
⊢ IsUpperSet (s * t)
[PROOFSTEP]
rw [mul_comm]
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
a : α
hs : IsUpperSet s
⊢ IsUpperSet (t * s)
[PROOFSTEP]
exact hs.mul_left
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
a : α
ht : IsUpperSet t
⊢ IsLowerSet (s / t)
[PROOFSTEP]
rw [div_eq_mul_inv]
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
a : α
ht : IsUpperSet t
⊢ IsLowerSet (s * t⁻¹)
[PROOFSTEP]
exact ht.inv.mul_left
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
a : α
hs : IsUpperSet s
⊢ IsUpperSet (s / t)
[PROOFSTEP]
rw [div_eq_mul_inv]
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
a : α
hs : IsUpperSet s
⊢ IsUpperSet (s * t⁻¹)
[PROOFSTEP]
exact hs.mul_right
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
s✝ t : Set α
a : α
s : UpperSet α
⊢ Set.Ici 1 * ↑s ⊆ ↑s
[PROOFSTEP]
rw [← smul_eq_mul, ← Set.iUnion_smul_set]
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
s✝ t : Set α
a : α
s : UpperSet α
⊢ ⋃ (a : α) (_ : a ∈ Set.Ici 1), a • ↑s ⊆ ↑s
[PROOFSTEP]
exact Set.iUnion₂_subset fun _ ↦ s.upper.smul_subset
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
s✝ t : Set α
a : α
src✝ : CommSemigroup (UpperSet α) := commSemigroup
s : UpperSet α
⊢ s * 1 = s
[PROOFSTEP]
rw [mul_comm]
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
s✝ t : Set α
a : α
src✝ : CommSemigroup (UpperSet α) := commSemigroup
s : UpperSet α
⊢ 1 * s = s
[PROOFSTEP]
exact one_mul _
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
s✝ t : Set α
a : α
s : LowerSet α
⊢ Set.Iic 1 * ↑s ⊆ ↑s
[PROOFSTEP]
rw [← smul_eq_mul, ← Set.iUnion_smul_set]
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
s✝ t : Set α
a : α
s : LowerSet α
⊢ ⋃ (a : α) (_ : a ∈ Set.Iic 1), a • ↑s ⊆ ↑s
[PROOFSTEP]
exact Set.iUnion₂_subset fun _ ↦ s.lower.smul_subset
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
s✝ t : Set α
a : α
src✝ : CommSemigroup (LowerSet α) := commSemigroup
s : LowerSet α
⊢ s * 1 = s
[PROOFSTEP]
rw [mul_comm]
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
s✝ t : Set α
a : α
src✝ : CommSemigroup (LowerSet α) := commSemigroup
s : LowerSet α
⊢ 1 * s = s
[PROOFSTEP]
exact one_mul _
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
a : α
⊢ s * ↑(upperClosure t) = ↑(upperClosure (s * t))
[PROOFSTEP]
simp_rw [← smul_eq_mul, ← Set.iUnion_smul_set, upperClosure_iUnion, upperClosure_smul, UpperSet.coe_iInf₂]
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
a : α
⊢ ⋃ (a : α) (_ : a ∈ s), a • ↑(upperClosure t) = ⋃ (i : α) (_ : i ∈ s), ↑(i • upperClosure t)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
a : α
⊢ s * ↑(lowerClosure t) = ↑(lowerClosure (s * t))
[PROOFSTEP]
simp_rw [← smul_eq_mul, ← Set.iUnion_smul_set, lowerClosure_iUnion, lowerClosure_smul, LowerSet.coe_iSup₂]
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
a : α
⊢ ⋃ (a : α) (_ : a ∈ s), a • ↑(lowerClosure t) = ⋃ (i : α) (_ : i ∈ s), ↑(i • lowerClosure t)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
a : α
⊢ ↑(upperClosure s) * t = ↑(upperClosure (s * t))
[PROOFSTEP]
simp_rw [mul_comm _ t]
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
a : α
⊢ t * ↑(upperClosure s) = ↑(upperClosure (t * s))
[PROOFSTEP]
exact mul_upperClosure _ _
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
a : α
⊢ ↑(lowerClosure s) * t = ↑(lowerClosure (s * t))
[PROOFSTEP]
simp_rw [mul_comm _ t]
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
a : α
⊢ t * ↑(lowerClosure s) = ↑(lowerClosure (t * s))
[PROOFSTEP]
exact mul_lowerClosure _ _
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
a : α
⊢ ↑(upperClosure (s * t)) = ↑(upperClosure s * upperClosure t)
[PROOFSTEP]
rw [UpperSet.coe_mul, mul_upperClosure, upperClosure_mul, UpperSet.upperClosure]
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
a : α
⊢ ↑(lowerClosure (s * t)) = ↑(lowerClosure s * lowerClosure t)
[PROOFSTEP]
rw [LowerSet.coe_mul, mul_lowerClosure, lowerClosure_mul, LowerSet.lowerClosure]