[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
⊢ IsIntegrallyClosed R ↔ ∀ {x : K}, IsIntegral R x → ∃ y, ↑(algebraMap R K) y = x
[PROOFSTEP]
let e : K ≃ₐ[R] FractionRing R := IsLocalization.algEquiv R⁰ _ _
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
e : K ≃ₐ[R] FractionRing R := IsLocalization.algEquiv R⁰ K (FractionRing R)
⊢ IsIntegrallyClosed R ↔ ∀ {x : K}, IsIntegral R x → ∃ y, ↑(algebraMap R K) y = x
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
e : K ≃ₐ[R] FractionRing R := IsLocalization.algEquiv R⁰ K (FractionRing R)
⊢ IsIntegrallyClosed R → ∀ {x : K}, IsIntegral R x → ∃ y, ↑(algebraMap R K) y = x
[PROOFSTEP]
rintro ⟨cl⟩
[GOAL]
case mp.mk
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
e : K ≃ₐ[R] FractionRing R := IsLocalization.algEquiv R⁰ K (FractionRing R)
cl : ∀ {x : FractionRing R}, IsIntegral R x → ∃ y, ↑(algebraMap R (FractionRing R)) y = x
⊢ ∀ {x : K}, IsIntegral R x → ∃ y, ↑(algebraMap R K) y = x
[PROOFSTEP]
refine' fun hx => _
[GOAL]
case mp.mk
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
e : K ≃ₐ[R] FractionRing R := IsLocalization.algEquiv R⁰ K (FractionRing R)
cl : ∀ {x : FractionRing R}, IsIntegral R x → ∃ y, ↑(algebraMap R (FractionRing R)) y = x
x✝ : K
hx : IsIntegral R x✝
⊢ ∃ y, ↑(algebraMap R K) y = x✝
[PROOFSTEP]
obtain ⟨y, hy⟩ := cl ((isIntegral_algEquiv e).mpr hx)
[GOAL]
case mp.mk.intro
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
e : K ≃ₐ[R] FractionRing R := IsLocalization.algEquiv R⁰ K (FractionRing R)
cl : ∀ {x : FractionRing R}, IsIntegral R x → ∃ y, ↑(algebraMap R (FractionRing R)) y = x
x✝ : K
hx : IsIntegral R x✝
y : R
hy : ↑(algebraMap R (FractionRing R)) y = ↑e x✝
⊢ ∃ y, ↑(algebraMap R K) y = x✝
[PROOFSTEP]
exact ⟨y, e.algebraMap_eq_apply.mp hy⟩
[GOAL]
case mpr
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
e : K ≃ₐ[R] FractionRing R := IsLocalization.algEquiv R⁰ K (FractionRing R)
⊢ (∀ {x : K}, IsIntegral R x → ∃ y, ↑(algebraMap R K) y = x) → IsIntegrallyClosed R
[PROOFSTEP]
rintro cl
[GOAL]
case mpr
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
e : K ≃ₐ[R] FractionRing R := IsLocalization.algEquiv R⁰ K (FractionRing R)
cl : ∀ {x : K}, IsIntegral R x → ∃ y, ↑(algebraMap R K) y = x
⊢ IsIntegrallyClosed R
[PROOFSTEP]
refine' ⟨fun hx => _⟩
[GOAL]
case mpr
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
e : K ≃ₐ[R] FractionRing R := IsLocalization.algEquiv R⁰ K (FractionRing R)
cl : ∀ {x : K}, IsIntegral R x → ∃ y, ↑(algebraMap R K) y = x
x✝ : FractionRing R
hx : IsIntegral R x✝
⊢ ∃ y, ↑(algebraMap R (FractionRing R)) y = x✝
[PROOFSTEP]
obtain ⟨y, hy⟩ := cl ((isIntegral_algEquiv e.symm).mpr hx)
[GOAL]
case mpr.intro
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
e : K ≃ₐ[R] FractionRing R := IsLocalization.algEquiv R⁰ K (FractionRing R)
cl : ∀ {x : K}, IsIntegral R x → ∃ y, ↑(algebraMap R K) y = x
x✝ : FractionRing R
hx : IsIntegral R x✝
y : R
hy : ↑(algebraMap R K) y = ↑(AlgEquiv.symm e) x✝
⊢ ∃ y, ↑(algebraMap R (FractionRing R)) y = x✝
[PROOFSTEP]
exact ⟨y, e.symm.algebraMap_eq_apply.mp hy⟩
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
⊢ (∀ {x : K}, IsIntegral R x → ∃ y, ↑(algebraMap R K) y = x) ↔ IsIntegralClosure R R K
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
⊢ (∀ {x : K}, IsIntegral R x → ∃ y, ↑(algebraMap R K) y = x) → IsIntegralClosure R R K
[PROOFSTEP]
intro cl
[GOAL]
case mp
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
cl : ∀ {x : K}, IsIntegral R x → ∃ y, ↑(algebraMap R K) y = x
⊢ IsIntegralClosure R R K
[PROOFSTEP]
refine' ⟨IsFractionRing.injective R K, ⟨cl, _⟩⟩
[GOAL]
case mp
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
cl : ∀ {x : K}, IsIntegral R x → ∃ y, ↑(algebraMap R K) y = x
x✝ : K
⊢ (∃ y, ↑(algebraMap R K) y = x✝) → IsIntegral R x✝
[PROOFSTEP]
rintro ⟨y, y_eq⟩
[GOAL]
case mp.intro
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
cl : ∀ {x : K}, IsIntegral R x → ∃ y, ↑(algebraMap R K) y = x
x✝ : K
y : R
y_eq : ↑(algebraMap R K) y = x✝
⊢ IsIntegral R x✝
[PROOFSTEP]
rw [← y_eq]
[GOAL]
case mp.intro
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
cl : ∀ {x : K}, IsIntegral R x → ∃ y, ↑(algebraMap R K) y = x
x✝ : K
y : R
y_eq : ↑(algebraMap R K) y = x✝
⊢ IsIntegral R (↑(algebraMap R K) y)
[PROOFSTEP]
exact isIntegral_algebraMap
[GOAL]
case mpr
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
⊢ IsIntegralClosure R R K → ∀ {x : K}, IsIntegral R x → ∃ y, ↑(algebraMap R K) y = x
[PROOFSTEP]
rintro ⟨-, cl⟩ x hx
[GOAL]
case mpr.mk
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
cl : ∀ {x : K}, IsIntegral R x ↔ ∃ y, ↑(algebraMap R K) y = x
x : K
hx : IsIntegral R x
⊢ ∃ y, ↑(algebraMap R K) y = x
[PROOFSTEP]
exact cl.mp hx
[GOAL]
R : Type u_1
inst✝² : CommRing R
id : IsDomain R
iic : IsIntegrallyClosed R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
ifr : IsFractionRing R K
⊢ integralClosure R K = ⊥ ↔ IsIntegrallyClosed R
[PROOFSTEP]
refine' eq_bot_iff.trans _
[GOAL]
R : Type u_1
inst✝² : CommRing R
id : IsDomain R
iic : IsIntegrallyClosed R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
ifr : IsFractionRing R K
⊢ integralClosure R K ≤ ⊥ ↔ IsIntegrallyClosed R
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
inst✝² : CommRing R
id : IsDomain R
iic : IsIntegrallyClosed R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
ifr : IsFractionRing R K
⊢ integralClosure R K ≤ ⊥ → IsIntegrallyClosed R
[PROOFSTEP]
rw [isIntegrallyClosed_iff K]
[GOAL]
case mp
R : Type u_1
inst✝² : CommRing R
id : IsDomain R
iic : IsIntegrallyClosed R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
ifr : IsFractionRing R K
⊢ integralClosure R K ≤ ⊥ → ∀ {x : K}, IsIntegral R x → ∃ y, ↑(algebraMap R K) y = x
[PROOFSTEP]
intro h x hx
[GOAL]
case mp
R : Type u_1
inst✝² : CommRing R
id : IsDomain R
iic : IsIntegrallyClosed R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
ifr : IsFractionRing R K
h : integralClosure R K ≤ ⊥
x : K
hx : IsIntegral R x
⊢ ∃ y, ↑(algebraMap R K) y = x
[PROOFSTEP]
exact Set.mem_range.mp (Algebra.mem_bot.mp (h hx))
[GOAL]
case mpr
R : Type u_1
inst✝² : CommRing R
id : IsDomain R
iic : IsIntegrallyClosed R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
ifr : IsFractionRing R K
⊢ IsIntegrallyClosed R → integralClosure R K ≤ ⊥
[PROOFSTEP]
intro h x hx
[GOAL]
case mpr
R : Type u_1
inst✝² : CommRing R
id : IsDomain R
iic : IsIntegrallyClosed R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
ifr : IsFractionRing R K
h : IsIntegrallyClosed R
x : K
hx : x ∈ integralClosure R K
⊢ x ∈ ⊥
[PROOFSTEP]
rw [Algebra.mem_bot, Set.mem_range]
[GOAL]
case mpr
R : Type u_1
inst✝² : CommRing R
id : IsDomain R
iic : IsIntegrallyClosed R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
ifr : IsFractionRing R K
h : IsIntegrallyClosed R
x : K
hx : x ∈ integralClosure R K
⊢ ∃ y, ↑(algebraMap R K) y = x
[PROOFSTEP]
exact isIntegral_iff.mp hx


[GOAL]
R : Type u_1
inst✝¹ inst✝ : Semiring R
e f : RingInvo R
h₁ : (fun f => f.toFun) e = (fun f => f.toFun) f
h₂ : (fun f => f.invFun) e = (fun f => f.invFun) f
⊢ e = f
[PROOFSTEP]
rcases e with ⟨⟨tE, _⟩, _⟩
[GOAL]
case mk.mk
R : Type u_1
inst✝¹ inst✝ : Semiring R
f : RingInvo R
tE : R ≃ Rᵐᵒᵖ
map_mul'✝ : ∀ (x y : R), Equiv.toFun tE (x * y) = Equiv.toFun tE x * Equiv.toFun tE y
map_add'✝ : ∀ (x y : R), Equiv.toFun tE (x + y) = Equiv.toFun tE x + Equiv.toFun tE y
involution'✝ :
  ∀ (x : R),
    MulOpposite.unop
        (Equiv.toFun { toEquiv := tE, map_mul' := map_mul'✝, map_add' := map_add'✝ }.toEquiv
          (MulOpposite.unop (Equiv.toFun { toEquiv := tE, map_mul' := map_mul'✝, map_add' := map_add'✝ }.toEquiv x))) =
      x
h₁ :
  (fun f => f.toFun)
      { toRingEquiv := { toEquiv := tE, map_mul' := map_mul'✝, map_add' := map_add'✝ }, involution' := involution'✝ } =
    (fun f => f.toFun) f
h₂ :
  (fun f => f.invFun)
      { toRingEquiv := { toEquiv := tE, map_mul' := map_mul'✝, map_add' := map_add'✝ }, involution' := involution'✝ } =
    (fun f => f.invFun) f
⊢ { toRingEquiv := { toEquiv := tE, map_mul' := map_mul'✝, map_add' := map_add'✝ }, involution' := involution'✝ } = f
[PROOFSTEP]
rcases f with ⟨⟨tF, _⟩, _⟩
[GOAL]
case mk.mk.mk.mk
R : Type u_1
inst✝¹ inst✝ : Semiring R
tE : R ≃ Rᵐᵒᵖ
map_mul'✝¹ : ∀ (x y : R), Equiv.toFun tE (x * y) = Equiv.toFun tE x * Equiv.toFun tE y
map_add'✝¹ : ∀ (x y : R), Equiv.toFun tE (x + y) = Equiv.toFun tE x + Equiv.toFun tE y
involution'✝¹ :
  ∀ (x : R),
    MulOpposite.unop
        (Equiv.toFun { toEquiv := tE, map_mul' := map_mul'✝¹, map_add' := map_add'✝¹ }.toEquiv
          (MulOpposite.unop
            (Equiv.toFun { toEquiv := tE, map_mul' := map_mul'✝¹, map_add' := map_add'✝¹ }.toEquiv x))) =
      x
tF : R ≃ Rᵐᵒᵖ
map_mul'✝ : ∀ (x y : R), Equiv.toFun tF (x * y) = Equiv.toFun tF x * Equiv.toFun tF y
map_add'✝ : ∀ (x y : R), Equiv.toFun tF (x + y) = Equiv.toFun tF x + Equiv.toFun tF y
involution'✝ :
  ∀ (x : R),
    MulOpposite.unop
        (Equiv.toFun { toEquiv := tF, map_mul' := map_mul'✝, map_add' := map_add'✝ }.toEquiv
          (MulOpposite.unop (Equiv.toFun { toEquiv := tF, map_mul' := map_mul'✝, map_add' := map_add'✝ }.toEquiv x))) =
      x
h₁ :
  (fun f => f.toFun)
      { toRingEquiv := { toEquiv := tE, map_mul' := map_mul'✝¹, map_add' := map_add'✝¹ },
        involution' := involution'✝¹ } =
    (fun f => f.toFun)
      { toRingEquiv := { toEquiv := tF, map_mul' := map_mul'✝, map_add' := map_add'✝ }, involution' := involution'✝ }
h₂ :
  (fun f => f.invFun)
      { toRingEquiv := { toEquiv := tE, map_mul' := map_mul'✝¹, map_add' := map_add'✝¹ },
        involution' := involution'✝¹ } =
    (fun f => f.invFun)
      { toRingEquiv := { toEquiv := tF, map_mul' := map_mul'✝, map_add' := map_add'✝ }, involution' := involution'✝ }
⊢ { toRingEquiv := { toEquiv := tE, map_mul' := map_mul'✝¹, map_add' := map_add'✝¹ }, involution' := involution'✝¹ } =
    { toRingEquiv := { toEquiv := tF, map_mul' := map_mul'✝, map_add' := map_add'✝ }, involution' := involution'✝ }
[PROOFSTEP]
cases tE
[GOAL]
case mk.mk.mk.mk.mk
R : Type u_1
inst✝¹ inst✝ : Semiring R
tF : R ≃ Rᵐᵒᵖ
map_mul'✝¹ : ∀ (x y : R), Equiv.toFun tF (x * y) = Equiv.toFun tF x * Equiv.toFun tF y
map_add'✝¹ : ∀ (x y : R), Equiv.toFun tF (x + y) = Equiv.toFun tF x + Equiv.toFun tF y
involution'✝¹ :
  ∀ (x : R),
    MulOpposite.unop
        (Equiv.toFun { toEquiv := tF, map_mul' := map_mul'✝¹, map_add' := map_add'✝¹ }.toEquiv
          (MulOpposite.unop
            (Equiv.toFun { toEquiv := tF, map_mul' := map_mul'✝¹, map_add' := map_add'✝¹ }.toEquiv x))) =
      x
toFun✝ : R → Rᵐᵒᵖ
invFun✝ : Rᵐᵒᵖ → R
left_inv✝ : Function.LeftInverse invFun✝ toFun✝
right_inv✝ : Function.RightInverse invFun✝ toFun✝
map_mul'✝ :
  ∀ (x y : R),
    Equiv.toFun { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } (x * y) =
      Equiv.toFun { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } x *
        Equiv.toFun { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } y
map_add'✝ :
  ∀ (x y : R),
    Equiv.toFun { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } (x + y) =
      Equiv.toFun { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } x +
        Equiv.toFun { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } y
involution'✝ :
  ∀ (x : R),
    MulOpposite.unop
        (Equiv.toFun
          { toEquiv := { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
              map_mul' := map_mul'✝, map_add' := map_add'✝ }.toEquiv
          (MulOpposite.unop
            (Equiv.toFun
              { toEquiv := { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
                  map_mul' := map_mul'✝, map_add' := map_add'✝ }.toEquiv
              x))) =
      x
h₁ :
  (fun f => f.toFun)
      {
        toRingEquiv :=
          { toEquiv := { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
            map_mul' := map_mul'✝, map_add' := map_add'✝ },
        involution' := involution'✝ } =
    (fun f => f.toFun)
      { toRingEquiv := { toEquiv := tF, map_mul' := map_mul'✝¹, map_add' := map_add'✝¹ }, involution' := involution'✝¹ }
h₂ :
  (fun f => f.invFun)
      {
        toRingEquiv :=
          { toEquiv := { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
            map_mul' := map_mul'✝, map_add' := map_add'✝ },
        involution' := involution'✝ } =
    (fun f => f.invFun)
      { toRingEquiv := { toEquiv := tF, map_mul' := map_mul'✝¹, map_add' := map_add'✝¹ }, involution' := involution'✝¹ }
⊢ {
      toRingEquiv :=
        { toEquiv := { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
          map_mul' := map_mul'✝, map_add' := map_add'✝ },
      involution' := involution'✝ } =
    { toRingEquiv := { toEquiv := tF, map_mul' := map_mul'✝¹, map_add' := map_add'✝¹ }, involution' := involution'✝¹ }
[PROOFSTEP]
cases tF
[GOAL]
case mk.mk.mk.mk.mk.mk
R : Type u_1
inst✝¹ inst✝ : Semiring R
toFun✝¹ : R → Rᵐᵒᵖ
invFun✝¹ : Rᵐᵒᵖ → R
left_inv✝¹ : Function.LeftInverse invFun✝¹ toFun✝¹
right_inv✝¹ : Function.RightInverse invFun✝¹ toFun✝¹
map_mul'✝¹ :
  ∀ (x y : R),
    Equiv.toFun { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } (x * y) =
      Equiv.toFun { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } x *
        Equiv.toFun { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } y
map_add'✝¹ :
  ∀ (x y : R),
    Equiv.toFun { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } (x + y) =
      Equiv.toFun { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } x +
        Equiv.toFun { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } y
involution'✝¹ :
  ∀ (x : R),
    MulOpposite.unop
        (Equiv.toFun
          { toEquiv := { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ },
              map_mul' := map_mul'✝¹, map_add' := map_add'✝¹ }.toEquiv
          (MulOpposite.unop
            (Equiv.toFun
              { toEquiv := { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ },
                  map_mul' := map_mul'✝¹, map_add' := map_add'✝¹ }.toEquiv
              x))) =
      x
toFun✝ : R → Rᵐᵒᵖ
invFun✝ : Rᵐᵒᵖ → R
left_inv✝ : Function.LeftInverse invFun✝ toFun✝
right_inv✝ : Function.RightInverse invFun✝ toFun✝
map_mul'✝ :
  ∀ (x y : R),
    Equiv.toFun { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } (x * y) =
      Equiv.toFun { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } x *
        Equiv.toFun { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } y
map_add'✝ :
  ∀ (x y : R),
    Equiv.toFun { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } (x + y) =
      Equiv.toFun { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } x +
        Equiv.toFun { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } y
involution'✝ :
  ∀ (x : R),
    MulOpposite.unop
        (Equiv.toFun
          { toEquiv := { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
              map_mul' := map_mul'✝, map_add' := map_add'✝ }.toEquiv
          (MulOpposite.unop
            (Equiv.toFun
              { toEquiv := { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
                  map_mul' := map_mul'✝, map_add' := map_add'✝ }.toEquiv
              x))) =
      x
h₁ :
  (fun f => f.toFun)
      {
        toRingEquiv :=
          { toEquiv := { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ },
            map_mul' := map_mul'✝¹, map_add' := map_add'✝¹ },
        involution' := involution'✝¹ } =
    (fun f => f.toFun)
      {
        toRingEquiv :=
          { toEquiv := { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
            map_mul' := map_mul'✝, map_add' := map_add'✝ },
        involution' := involution'✝ }
h₂ :
  (fun f => f.invFun)
      {
        toRingEquiv :=
          { toEquiv := { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ },
            map_mul' := map_mul'✝¹, map_add' := map_add'✝¹ },
        involution' := involution'✝¹ } =
    (fun f => f.invFun)
      {
        toRingEquiv :=
          { toEquiv := { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
            map_mul' := map_mul'✝, map_add' := map_add'✝ },
        involution' := involution'✝ }
⊢ {
      toRingEquiv :=
        { toEquiv := { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ },
          map_mul' := map_mul'✝¹, map_add' := map_add'✝¹ },
      involution' := involution'✝¹ } =
    {
      toRingEquiv :=
        { toEquiv := { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
          map_mul' := map_mul'✝, map_add' := map_add'✝ },
      involution' := involution'✝ }
[PROOFSTEP]
congr


[GOAL]
𝕜 : Type u_1
inst✝²¹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝²⁰ : NormedAddCommGroup E
inst✝¹⁹ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹⁸ : NormedAddCommGroup E'
inst✝¹⁷ : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝¹⁵ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝¹⁴ : TopologicalSpace N
inst✝¹³ : ChartedSpace H N
E'' : Type u_7
inst✝¹² : NormedAddCommGroup E''
inst✝¹¹ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝¹⁰ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝⁹ : TopologicalSpace N'
inst✝⁸ : ChartedSpace H'' N'
G' : Type u_10
inst✝⁷ : Monoid G'
inst✝⁶ : TopologicalSpace G'
inst✝⁵ : ChartedSpace H' G'
inst✝⁴ : SmoothMul I' G'
G'' : Type u_11
inst✝³ : Monoid G''
inst✝² : TopologicalSpace G''
inst✝¹ : ChartedSpace H'' G''
inst✝ : SmoothMul I'' G''
φ : G' →* G''
hφ : Smooth I' I'' ↑φ
⊢ (fun f => { val := ↑φ ∘ ↑f, property := (_ : ∀ (x : N), ContMDiffAt I I'' ⊤ (↑φ ∘ ↑f) x) }) 1 = 1
[PROOFSTEP]
ext
[GOAL]
case h
𝕜 : Type u_1
inst✝²¹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝²⁰ : NormedAddCommGroup E
inst✝¹⁹ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹⁸ : NormedAddCommGroup E'
inst✝¹⁷ : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝¹⁵ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝¹⁴ : TopologicalSpace N
inst✝¹³ : ChartedSpace H N
E'' : Type u_7
inst✝¹² : NormedAddCommGroup E''
inst✝¹¹ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝¹⁰ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝⁹ : TopologicalSpace N'
inst✝⁸ : ChartedSpace H'' N'
G' : Type u_10
inst✝⁷ : Monoid G'
inst✝⁶ : TopologicalSpace G'
inst✝⁵ : ChartedSpace H' G'
inst✝⁴ : SmoothMul I' G'
G'' : Type u_11
inst✝³ : Monoid G''
inst✝² : TopologicalSpace G''
inst✝¹ : ChartedSpace H'' G''
inst✝ : SmoothMul I'' G''
φ : G' →* G''
hφ : Smooth I' I'' ↑φ
x✝ : N
⊢ ↑((fun f => { val := ↑φ ∘ ↑f, property := (_ : ∀ (x : N), ContMDiffAt I I'' ⊤ (↑φ ∘ ↑f) x) }) 1) x✝ = ↑1 x✝
[PROOFSTEP]
show φ 1 = 1
[GOAL]
case h
𝕜 : Type u_1
inst✝²¹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝²⁰ : NormedAddCommGroup E
inst✝¹⁹ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹⁸ : NormedAddCommGroup E'
inst✝¹⁷ : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝¹⁵ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝¹⁴ : TopologicalSpace N
inst✝¹³ : ChartedSpace H N
E'' : Type u_7
inst✝¹² : NormedAddCommGroup E''
inst✝¹¹ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝¹⁰ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝⁹ : TopologicalSpace N'
inst✝⁸ : ChartedSpace H'' N'
G' : Type u_10
inst✝⁷ : Monoid G'
inst✝⁶ : TopologicalSpace G'
inst✝⁵ : ChartedSpace H' G'
inst✝⁴ : SmoothMul I' G'
G'' : Type u_11
inst✝³ : Monoid G''
inst✝² : TopologicalSpace G''
inst✝¹ : ChartedSpace H'' G''
inst✝ : SmoothMul I'' G''
φ : G' →* G''
hφ : Smooth I' I'' ↑φ
x✝ : N
⊢ ↑φ 1 = 1
[PROOFSTEP]
simp
[GOAL]
𝕜 : Type u_1
inst✝²¹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝²⁰ : NormedAddCommGroup E
inst✝¹⁹ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹⁸ : NormedAddCommGroup E'
inst✝¹⁷ : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝¹⁵ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝¹⁴ : TopologicalSpace N
inst✝¹³ : ChartedSpace H N
E'' : Type u_7
inst✝¹² : NormedAddCommGroup E''
inst✝¹¹ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝¹⁰ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝⁹ : TopologicalSpace N'
inst✝⁸ : ChartedSpace H'' N'
G' : Type u_10
inst✝⁷ : Monoid G'
inst✝⁶ : TopologicalSpace G'
inst✝⁵ : ChartedSpace H' G'
inst✝⁴ : SmoothMul I' G'
G'' : Type u_11
inst✝³ : Monoid G''
inst✝² : TopologicalSpace G''
inst✝¹ : ChartedSpace H'' G''
inst✝ : SmoothMul I'' G''
φ : G' →* G''
hφ : Smooth I' I'' ↑φ
f g : C^⊤⟮I, N; I', G'⟯
⊢ OneHom.toFun
      { toFun := fun f => { val := ↑φ ∘ ↑f, property := (_ : ∀ (x : N), ContMDiffAt I I'' ⊤ (↑φ ∘ ↑f) x) },
        map_one' :=
          (_ : (fun f => { val := ↑φ ∘ ↑f, property := (_ : ∀ (x : N), ContMDiffAt I I'' ⊤ (↑φ ∘ ↑f) x) }) 1 = 1) }
      (f * g) =
    OneHom.toFun
        { toFun := fun f => { val := ↑φ ∘ ↑f, property := (_ : ∀ (x : N), ContMDiffAt I I'' ⊤ (↑φ ∘ ↑f) x) },
          map_one' :=
            (_ : (fun f => { val := ↑φ ∘ ↑f, property := (_ : ∀ (x : N), ContMDiffAt I I'' ⊤ (↑φ ∘ ↑f) x) }) 1 = 1) }
        f *
      OneHom.toFun
        { toFun := fun f => { val := ↑φ ∘ ↑f, property := (_ : ∀ (x : N), ContMDiffAt I I'' ⊤ (↑φ ∘ ↑f) x) },
          map_one' :=
            (_ : (fun f => { val := ↑φ ∘ ↑f, property := (_ : ∀ (x : N), ContMDiffAt I I'' ⊤ (↑φ ∘ ↑f) x) }) 1 = 1) }
        g
[PROOFSTEP]
ext x
[GOAL]
case h
𝕜 : Type u_1
inst✝²¹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝²⁰ : NormedAddCommGroup E
inst✝¹⁹ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹⁸ : NormedAddCommGroup E'
inst✝¹⁷ : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝¹⁵ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝¹⁴ : TopologicalSpace N
inst✝¹³ : ChartedSpace H N
E'' : Type u_7
inst✝¹² : NormedAddCommGroup E''
inst✝¹¹ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝¹⁰ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝⁹ : TopologicalSpace N'
inst✝⁸ : ChartedSpace H'' N'
G' : Type u_10
inst✝⁷ : Monoid G'
inst✝⁶ : TopologicalSpace G'
inst✝⁵ : ChartedSpace H' G'
inst✝⁴ : SmoothMul I' G'
G'' : Type u_11
inst✝³ : Monoid G''
inst✝² : TopologicalSpace G''
inst✝¹ : ChartedSpace H'' G''
inst✝ : SmoothMul I'' G''
φ : G' →* G''
hφ : Smooth I' I'' ↑φ
f g : C^⊤⟮I, N; I', G'⟯
x : N
⊢ ↑(OneHom.toFun
          { toFun := fun f => { val := ↑φ ∘ ↑f, property := (_ : ∀ (x : N), ContMDiffAt I I'' ⊤ (↑φ ∘ ↑f) x) },
            map_one' :=
              (_ : (fun f => { val := ↑φ ∘ ↑f, property := (_ : ∀ (x : N), ContMDiffAt I I'' ⊤ (↑φ ∘ ↑f) x) }) 1 = 1) }
          (f * g))
      x =
    ↑(OneHom.toFun
            { toFun := fun f => { val := ↑φ ∘ ↑f, property := (_ : ∀ (x : N), ContMDiffAt I I'' ⊤ (↑φ ∘ ↑f) x) },
              map_one' :=
                (_ :
                  (fun f => { val := ↑φ ∘ ↑f, property := (_ : ∀ (x : N), ContMDiffAt I I'' ⊤ (↑φ ∘ ↑f) x) }) 1 = 1) }
            f *
          OneHom.toFun
            { toFun := fun f => { val := ↑φ ∘ ↑f, property := (_ : ∀ (x : N), ContMDiffAt I I'' ⊤ (↑φ ∘ ↑f) x) },
              map_one' :=
                (_ :
                  (fun f => { val := ↑φ ∘ ↑f, property := (_ : ∀ (x : N), ContMDiffAt I I'' ⊤ (↑φ ∘ ↑f) x) }) 1 = 1) }
            g)
      x
[PROOFSTEP]
show φ (f x * g x) = φ (f x) * φ (g x)
[GOAL]
case h
𝕜 : Type u_1
inst✝²¹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝²⁰ : NormedAddCommGroup E
inst✝¹⁹ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹⁸ : NormedAddCommGroup E'
inst✝¹⁷ : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝¹⁵ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝¹⁴ : TopologicalSpace N
inst✝¹³ : ChartedSpace H N
E'' : Type u_7
inst✝¹² : NormedAddCommGroup E''
inst✝¹¹ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝¹⁰ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝⁹ : TopologicalSpace N'
inst✝⁸ : ChartedSpace H'' N'
G' : Type u_10
inst✝⁷ : Monoid G'
inst✝⁶ : TopologicalSpace G'
inst✝⁵ : ChartedSpace H' G'
inst✝⁴ : SmoothMul I' G'
G'' : Type u_11
inst✝³ : Monoid G''
inst✝² : TopologicalSpace G''
inst✝¹ : ChartedSpace H'' G''
inst✝ : SmoothMul I'' G''
φ : G' →* G''
hφ : Smooth I' I'' ↑φ
f g : C^⊤⟮I, N; I', G'⟯
x : N
⊢ ↑φ (↑f x * ↑g x) = ↑φ (↑f x) * ↑φ (↑g x)
[PROOFSTEP]
simp
[GOAL]
𝕜 : Type u_1
inst✝¹⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁶ : NormedAddCommGroup E
inst✝¹⁵ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹⁴ : NormedAddCommGroup E'
inst✝¹³ : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝¹¹ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝¹⁰ : TopologicalSpace N
inst✝⁹ : ChartedSpace H N
E'' : Type u_7
inst✝⁸ : NormedAddCommGroup E''
inst✝⁷ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝⁶ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝⁵ : TopologicalSpace N'
inst✝⁴ : ChartedSpace H'' N'
G : Type u_10
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : ChartedSpace H' G
inst✝ : LieGroup I' G
src✝ : Monoid C^⊤⟮I, N; I', G⟯ := monoid
f g : C^⊤⟮I, N; I', G⟯
⊢ f / g = f * g⁻¹
[PROOFSTEP]
ext
[GOAL]
case h
𝕜 : Type u_1
inst✝¹⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁶ : NormedAddCommGroup E
inst✝¹⁵ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹⁴ : NormedAddCommGroup E'
inst✝¹³ : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝¹¹ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝¹⁰ : TopologicalSpace N
inst✝⁹ : ChartedSpace H N
E'' : Type u_7
inst✝⁸ : NormedAddCommGroup E''
inst✝⁷ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝⁶ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝⁵ : TopologicalSpace N'
inst✝⁴ : ChartedSpace H'' N'
G : Type u_10
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : ChartedSpace H' G
inst✝ : LieGroup I' G
src✝ : Monoid C^⊤⟮I, N; I', G⟯ := monoid
f g : C^⊤⟮I, N; I', G⟯
x✝ : N
⊢ ↑(f / g) x✝ = ↑(f * g⁻¹) x✝
[PROOFSTEP]
exact div_eq_mul_inv _ _
[GOAL]
𝕜 : Type u_1
inst✝¹⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁶ : NormedAddCommGroup E
inst✝¹⁵ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹⁴ : NormedAddCommGroup E'
inst✝¹³ : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝¹¹ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝¹⁰ : TopologicalSpace N
inst✝⁹ : ChartedSpace H N
E'' : Type u_7
inst✝⁸ : NormedAddCommGroup E''
inst✝⁷ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝⁶ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝⁵ : TopologicalSpace N'
inst✝⁴ : ChartedSpace H'' N'
G : Type u_10
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : ChartedSpace H' G
inst✝ : LieGroup I' G
src✝ : Monoid C^⊤⟮I, N; I', G⟯ := monoid
a : C^⊤⟮I, N; I', G⟯
⊢ a⁻¹ * a = 1
[PROOFSTEP]
ext
[GOAL]
case h
𝕜 : Type u_1
inst✝¹⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁶ : NormedAddCommGroup E
inst✝¹⁵ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹⁴ : NormedAddCommGroup E'
inst✝¹³ : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝¹¹ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝¹⁰ : TopologicalSpace N
inst✝⁹ : ChartedSpace H N
E'' : Type u_7
inst✝⁸ : NormedAddCommGroup E''
inst✝⁷ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝⁶ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝⁵ : TopologicalSpace N'
inst✝⁴ : ChartedSpace H'' N'
G : Type u_10
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : ChartedSpace H' G
inst✝ : LieGroup I' G
src✝ : Monoid C^⊤⟮I, N; I', G⟯ := monoid
a : C^⊤⟮I, N; I', G⟯
x✝ : N
⊢ ↑(a⁻¹ * a) x✝ = ↑1 x✝
[PROOFSTEP]
exact mul_left_inv _
[GOAL]
𝕜 : Type u_1
inst✝¹⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁶ : NormedAddCommGroup E
inst✝¹⁵ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹⁴ : NormedAddCommGroup E'
inst✝¹³ : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝¹¹ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝¹⁰ : TopologicalSpace N
inst✝⁹ : ChartedSpace H N
E'' : Type u_7
inst✝⁸ : NormedAddCommGroup E''
inst✝⁷ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝⁶ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝⁵ : TopologicalSpace N'
inst✝⁴ : ChartedSpace H'' N'
R : Type u_10
inst✝³ : Semiring R
inst✝² : TopologicalSpace R
inst✝¹ : ChartedSpace H' R
inst✝ : SmoothRing I' R
src✝¹ : AddCommMonoid C^⊤⟮I, N; I', R⟯ := addCommMonoid
src✝ : Monoid C^⊤⟮I, N; I', R⟯ := monoid
a b c : C^⊤⟮I, N; I', R⟯
⊢ a * (b + c) = a * b + a * c
[PROOFSTEP]
ext
[GOAL]
case h
𝕜 : Type u_1
inst✝¹⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁶ : NormedAddCommGroup E
inst✝¹⁵ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹⁴ : NormedAddCommGroup E'
inst✝¹³ : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝¹¹ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝¹⁰ : TopologicalSpace N
inst✝⁹ : ChartedSpace H N
E'' : Type u_7
inst✝⁸ : NormedAddCommGroup E''
inst✝⁷ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝⁶ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝⁵ : TopologicalSpace N'
inst✝⁴ : ChartedSpace H'' N'
R : Type u_10
inst✝³ : Semiring R
inst✝² : TopologicalSpace R
inst✝¹ : ChartedSpace H' R
inst✝ : SmoothRing I' R
src✝¹ : AddCommMonoid C^⊤⟮I, N; I', R⟯ := addCommMonoid
src✝ : Monoid C^⊤⟮I, N; I', R⟯ := monoid
a b c : C^⊤⟮I, N; I', R⟯
x✝ : N
⊢ ↑(a * (b + c)) x✝ = ↑(a * b + a * c) x✝
[PROOFSTEP]
exact left_distrib _ _ _
[GOAL]
𝕜 : Type u_1
inst✝¹⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁶ : NormedAddCommGroup E
inst✝¹⁵ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹⁴ : NormedAddCommGroup E'
inst✝¹³ : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝¹¹ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝¹⁰ : TopologicalSpace N
inst✝⁹ : ChartedSpace H N
E'' : Type u_7
inst✝⁸ : NormedAddCommGroup E''
inst✝⁷ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝⁶ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝⁵ : TopologicalSpace N'
inst✝⁴ : ChartedSpace H'' N'
R : Type u_10
inst✝³ : Semiring R
inst✝² : TopologicalSpace R
inst✝¹ : ChartedSpace H' R
inst✝ : SmoothRing I' R
src✝¹ : AddCommMonoid C^⊤⟮I, N; I', R⟯ := addCommMonoid
src✝ : Monoid C^⊤⟮I, N; I', R⟯ := monoid
a b c : C^⊤⟮I, N; I', R⟯
⊢ (a + b) * c = a * c + b * c
[PROOFSTEP]
ext
[GOAL]
case h
𝕜 : Type u_1
inst✝¹⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁶ : NormedAddCommGroup E
inst✝¹⁵ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹⁴ : NormedAddCommGroup E'
inst✝¹³ : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝¹¹ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝¹⁰ : TopologicalSpace N
inst✝⁹ : ChartedSpace H N
E'' : Type u_7
inst✝⁸ : NormedAddCommGroup E''
inst✝⁷ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝⁶ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝⁵ : TopologicalSpace N'
inst✝⁴ : ChartedSpace H'' N'
R : Type u_10
inst✝³ : Semiring R
inst✝² : TopologicalSpace R
inst✝¹ : ChartedSpace H' R
inst✝ : SmoothRing I' R
src✝¹ : AddCommMonoid C^⊤⟮I, N; I', R⟯ := addCommMonoid
src✝ : Monoid C^⊤⟮I, N; I', R⟯ := monoid
a b c : C^⊤⟮I, N; I', R⟯
x✝ : N
⊢ ↑((a + b) * c) x✝ = ↑(a * c + b * c) x✝
[PROOFSTEP]
exact right_distrib _ _ _
[GOAL]
𝕜 : Type u_1
inst✝¹⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁶ : NormedAddCommGroup E
inst✝¹⁵ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹⁴ : NormedAddCommGroup E'
inst✝¹³ : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝¹¹ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝¹⁰ : TopologicalSpace N
inst✝⁹ : ChartedSpace H N
E'' : Type u_7
inst✝⁸ : NormedAddCommGroup E''
inst✝⁷ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝⁶ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝⁵ : TopologicalSpace N'
inst✝⁴ : ChartedSpace H'' N'
R : Type u_10
inst✝³ : Semiring R
inst✝² : TopologicalSpace R
inst✝¹ : ChartedSpace H' R
inst✝ : SmoothRing I' R
src✝¹ : AddCommMonoid C^⊤⟮I, N; I', R⟯ := addCommMonoid
src✝ : Monoid C^⊤⟮I, N; I', R⟯ := monoid
a : C^⊤⟮I, N; I', R⟯
⊢ 0 * a = 0
[PROOFSTEP]
ext
[GOAL]
case h
𝕜 : Type u_1
inst✝¹⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁶ : NormedAddCommGroup E
inst✝¹⁵ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹⁴ : NormedAddCommGroup E'
inst✝¹³ : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝¹¹ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝¹⁰ : TopologicalSpace N
inst✝⁹ : ChartedSpace H N
E'' : Type u_7
inst✝⁸ : NormedAddCommGroup E''
inst✝⁷ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝⁶ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝⁵ : TopologicalSpace N'
inst✝⁴ : ChartedSpace H'' N'
R : Type u_10
inst✝³ : Semiring R
inst✝² : TopologicalSpace R
inst✝¹ : ChartedSpace H' R
inst✝ : SmoothRing I' R
src✝¹ : AddCommMonoid C^⊤⟮I, N; I', R⟯ := addCommMonoid
src✝ : Monoid C^⊤⟮I, N; I', R⟯ := monoid
a : C^⊤⟮I, N; I', R⟯
x✝ : N
⊢ ↑(0 * a) x✝ = ↑0 x✝
[PROOFSTEP]
exact zero_mul _
[GOAL]
𝕜 : Type u_1
inst✝¹⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁶ : NormedAddCommGroup E
inst✝¹⁵ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹⁴ : NormedAddCommGroup E'
inst✝¹³ : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝¹¹ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝¹⁰ : TopologicalSpace N
inst✝⁹ : ChartedSpace H N
E'' : Type u_7
inst✝⁸ : NormedAddCommGroup E''
inst✝⁷ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝⁶ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝⁵ : TopologicalSpace N'
inst✝⁴ : ChartedSpace H'' N'
R : Type u_10
inst✝³ : Semiring R
inst✝² : TopologicalSpace R
inst✝¹ : ChartedSpace H' R
inst✝ : SmoothRing I' R
src✝¹ : AddCommMonoid C^⊤⟮I, N; I', R⟯ := addCommMonoid
src✝ : Monoid C^⊤⟮I, N; I', R⟯ := monoid
a : C^⊤⟮I, N; I', R⟯
⊢ a * 0 = 0
[PROOFSTEP]
ext
[GOAL]
case h
𝕜 : Type u_1
inst✝¹⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁶ : NormedAddCommGroup E
inst✝¹⁵ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹⁴ : NormedAddCommGroup E'
inst✝¹³ : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝¹¹ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝¹⁰ : TopologicalSpace N
inst✝⁹ : ChartedSpace H N
E'' : Type u_7
inst✝⁸ : NormedAddCommGroup E''
inst✝⁷ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝⁶ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝⁵ : TopologicalSpace N'
inst✝⁴ : ChartedSpace H'' N'
R : Type u_10
inst✝³ : Semiring R
inst✝² : TopologicalSpace R
inst✝¹ : ChartedSpace H' R
inst✝ : SmoothRing I' R
src✝¹ : AddCommMonoid C^⊤⟮I, N; I', R⟯ := addCommMonoid
src✝ : Monoid C^⊤⟮I, N; I', R⟯ := monoid
a : C^⊤⟮I, N; I', R⟯
x✝ : N
⊢ ↑(a * 0) x✝ = ↑0 x✝
[PROOFSTEP]
exact mul_zero _
[GOAL]
𝕜 : Type u_1
inst✝¹⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁵ : NormedAddCommGroup E
inst✝¹⁴ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹³ : NormedAddCommGroup E'
inst✝¹² : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝¹⁰ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝⁹ : TopologicalSpace N
inst✝⁸ : ChartedSpace H N
E'' : Type u_7
inst✝⁷ : NormedAddCommGroup E''
inst✝⁶ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝⁵ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝⁴ : TopologicalSpace N'
inst✝³ : ChartedSpace H'' N'
A : Type u_10
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : SmoothRing 𝓘(𝕜, A) A
⊢ (fun c => { val := fun x => ↑(algebraMap 𝕜 A) c, property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
      1 =
    1
[PROOFSTEP]
ext
[GOAL]
case h
𝕜 : Type u_1
inst✝¹⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁵ : NormedAddCommGroup E
inst✝¹⁴ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹³ : NormedAddCommGroup E'
inst✝¹² : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝¹⁰ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝⁹ : TopologicalSpace N
inst✝⁸ : ChartedSpace H N
E'' : Type u_7
inst✝⁷ : NormedAddCommGroup E''
inst✝⁶ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝⁵ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝⁴ : TopologicalSpace N'
inst✝³ : ChartedSpace H'' N'
A : Type u_10
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : SmoothRing 𝓘(𝕜, A) A
x✝ : N
⊢ ↑((fun c => { val := fun x => ↑(algebraMap 𝕜 A) c, property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
          1)
      x✝ =
    ↑1 x✝
[PROOFSTEP]
exact (algebraMap 𝕜 A).map_one
[GOAL]
𝕜 : Type u_1
inst✝¹⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁵ : NormedAddCommGroup E
inst✝¹⁴ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹³ : NormedAddCommGroup E'
inst✝¹² : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝¹⁰ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝⁹ : TopologicalSpace N
inst✝⁸ : ChartedSpace H N
E'' : Type u_7
inst✝⁷ : NormedAddCommGroup E''
inst✝⁶ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝⁵ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝⁴ : TopologicalSpace N'
inst✝³ : ChartedSpace H'' N'
A : Type u_10
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : SmoothRing 𝓘(𝕜, A) A
c₁ c₂ : 𝕜
⊢ OneHom.toFun
      {
        toFun := fun c =>
          { val := fun x => ↑(algebraMap 𝕜 A) c, property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) },
        map_one' :=
          (_ :
            (fun c =>
                  { val := fun x => ↑(algebraMap 𝕜 A) c,
                    property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
                1 =
              1) }
      (c₁ * c₂) =
    OneHom.toFun
        {
          toFun := fun c =>
            { val := fun x => ↑(algebraMap 𝕜 A) c, property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) },
          map_one' :=
            (_ :
              (fun c =>
                    { val := fun x => ↑(algebraMap 𝕜 A) c,
                      property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
                  1 =
                1) }
        c₁ *
      OneHom.toFun
        {
          toFun := fun c =>
            { val := fun x => ↑(algebraMap 𝕜 A) c, property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) },
          map_one' :=
            (_ :
              (fun c =>
                    { val := fun x => ↑(algebraMap 𝕜 A) c,
                      property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
                  1 =
                1) }
        c₂
[PROOFSTEP]
ext
[GOAL]
case h
𝕜 : Type u_1
inst✝¹⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁵ : NormedAddCommGroup E
inst✝¹⁴ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹³ : NormedAddCommGroup E'
inst✝¹² : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝¹⁰ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝⁹ : TopologicalSpace N
inst✝⁸ : ChartedSpace H N
E'' : Type u_7
inst✝⁷ : NormedAddCommGroup E''
inst✝⁶ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝⁵ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝⁴ : TopologicalSpace N'
inst✝³ : ChartedSpace H'' N'
A : Type u_10
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : SmoothRing 𝓘(𝕜, A) A
c₁ c₂ : 𝕜
x✝ : N
⊢ ↑(OneHom.toFun
          {
            toFun := fun c =>
              { val := fun x => ↑(algebraMap 𝕜 A) c, property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) },
            map_one' :=
              (_ :
                (fun c =>
                      { val := fun x => ↑(algebraMap 𝕜 A) c,
                        property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
                    1 =
                  1) }
          (c₁ * c₂))
      x✝ =
    ↑(OneHom.toFun
            {
              toFun := fun c =>
                { val := fun x => ↑(algebraMap 𝕜 A) c,
                  property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) },
              map_one' :=
                (_ :
                  (fun c =>
                        { val := fun x => ↑(algebraMap 𝕜 A) c,
                          property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
                      1 =
                    1) }
            c₁ *
          OneHom.toFun
            {
              toFun := fun c =>
                { val := fun x => ↑(algebraMap 𝕜 A) c,
                  property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) },
              map_one' :=
                (_ :
                  (fun c =>
                        { val := fun x => ↑(algebraMap 𝕜 A) c,
                          property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
                      1 =
                    1) }
            c₂)
      x✝
[PROOFSTEP]
exact (algebraMap 𝕜 A).map_mul _ _
[GOAL]
𝕜 : Type u_1
inst✝¹⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁵ : NormedAddCommGroup E
inst✝¹⁴ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹³ : NormedAddCommGroup E'
inst✝¹² : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝¹⁰ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝⁹ : TopologicalSpace N
inst✝⁸ : ChartedSpace H N
E'' : Type u_7
inst✝⁷ : NormedAddCommGroup E''
inst✝⁶ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝⁵ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝⁴ : TopologicalSpace N'
inst✝³ : ChartedSpace H'' N'
A : Type u_10
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : SmoothRing 𝓘(𝕜, A) A
⊢ OneHom.toFun
      (↑{
          toOneHom :=
            {
              toFun := fun c =>
                { val := fun x => ↑(algebraMap 𝕜 A) c,
                  property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) },
              map_one' :=
                (_ :
                  (fun c =>
                        { val := fun x => ↑(algebraMap 𝕜 A) c,
                          property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
                      1 =
                    1) },
          map_mul' :=
            (_ :
              ∀ (c₁ c₂ : 𝕜),
                OneHom.toFun
                    {
                      toFun := fun c =>
                        { val := fun x => ↑(algebraMap 𝕜 A) c,
                          property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) },
                      map_one' :=
                        (_ :
                          (fun c =>
                                { val := fun x => ↑(algebraMap 𝕜 A) c,
                                  property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
                              1 =
                            1) }
                    (c₁ * c₂) =
                  OneHom.toFun
                      {
                        toFun := fun c =>
                          { val := fun x => ↑(algebraMap 𝕜 A) c,
                            property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) },
                        map_one' :=
                          (_ :
                            (fun c =>
                                  { val := fun x => ↑(algebraMap 𝕜 A) c,
                                    property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
                                1 =
                              1) }
                      c₁ *
                    OneHom.toFun
                      {
                        toFun := fun c =>
                          { val := fun x => ↑(algebraMap 𝕜 A) c,
                            property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) },
                        map_one' :=
                          (_ :
                            (fun c =>
                                  { val := fun x => ↑(algebraMap 𝕜 A) c,
                                    property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
                                1 =
                              1) }
                      c₂) })
      0 =
    0
[PROOFSTEP]
ext
[GOAL]
case h
𝕜 : Type u_1
inst✝¹⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁵ : NormedAddCommGroup E
inst✝¹⁴ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹³ : NormedAddCommGroup E'
inst✝¹² : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝¹⁰ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝⁹ : TopologicalSpace N
inst✝⁸ : ChartedSpace H N
E'' : Type u_7
inst✝⁷ : NormedAddCommGroup E''
inst✝⁶ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝⁵ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝⁴ : TopologicalSpace N'
inst✝³ : ChartedSpace H'' N'
A : Type u_10
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : SmoothRing 𝓘(𝕜, A) A
x✝ : N
⊢ ↑(OneHom.toFun
          (↑{
              toOneHom :=
                {
                  toFun := fun c =>
                    { val := fun x => ↑(algebraMap 𝕜 A) c,
                      property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) },
                  map_one' :=
                    (_ :
                      (fun c =>
                            { val := fun x => ↑(algebraMap 𝕜 A) c,
                              property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
                          1 =
                        1) },
              map_mul' :=
                (_ :
                  ∀ (c₁ c₂ : 𝕜),
                    OneHom.toFun
                        {
                          toFun := fun c =>
                            { val := fun x => ↑(algebraMap 𝕜 A) c,
                              property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) },
                          map_one' :=
                            (_ :
                              (fun c =>
                                    { val := fun x => ↑(algebraMap 𝕜 A) c,
                                      property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
                                  1 =
                                1) }
                        (c₁ * c₂) =
                      OneHom.toFun
                          {
                            toFun := fun c =>
                              { val := fun x => ↑(algebraMap 𝕜 A) c,
                                property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) },
                            map_one' :=
                              (_ :
                                (fun c =>
                                      { val := fun x => ↑(algebraMap 𝕜 A) c,
                                        property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
                                    1 =
                                  1) }
                          c₁ *
                        OneHom.toFun
                          {
                            toFun := fun c =>
                              { val := fun x => ↑(algebraMap 𝕜 A) c,
                                property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) },
                            map_one' :=
                              (_ :
                                (fun c =>
                                      { val := fun x => ↑(algebraMap 𝕜 A) c,
                                        property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
                                    1 =
                                  1) }
                          c₂) })
          0)
      x✝ =
    ↑0 x✝
[PROOFSTEP]
exact (algebraMap 𝕜 A).map_zero
[GOAL]
𝕜 : Type u_1
inst✝¹⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁵ : NormedAddCommGroup E
inst✝¹⁴ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹³ : NormedAddCommGroup E'
inst✝¹² : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝¹⁰ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝⁹ : TopologicalSpace N
inst✝⁸ : ChartedSpace H N
E'' : Type u_7
inst✝⁷ : NormedAddCommGroup E''
inst✝⁶ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝⁵ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝⁴ : TopologicalSpace N'
inst✝³ : ChartedSpace H'' N'
A : Type u_10
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : SmoothRing 𝓘(𝕜, A) A
c₁ c₂ : 𝕜
⊢ OneHom.toFun
      (↑{
          toOneHom :=
            {
              toFun := fun c =>
                { val := fun x => ↑(algebraMap 𝕜 A) c,
                  property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) },
              map_one' :=
                (_ :
                  (fun c =>
                        { val := fun x => ↑(algebraMap 𝕜 A) c,
                          property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
                      1 =
                    1) },
          map_mul' :=
            (_ :
              ∀ (c₁ c₂ : 𝕜),
                OneHom.toFun
                    {
                      toFun := fun c =>
                        { val := fun x => ↑(algebraMap 𝕜 A) c,
                          property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) },
                      map_one' :=
                        (_ :
                          (fun c =>
                                { val := fun x => ↑(algebraMap 𝕜 A) c,
                                  property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
                              1 =
                            1) }
                    (c₁ * c₂) =
                  OneHom.toFun
                      {
                        toFun := fun c =>
                          { val := fun x => ↑(algebraMap 𝕜 A) c,
                            property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) },
                        map_one' :=
                          (_ :
                            (fun c =>
                                  { val := fun x => ↑(algebraMap 𝕜 A) c,
                                    property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
                                1 =
                              1) }
                      c₁ *
                    OneHom.toFun
                      {
                        toFun := fun c =>
                          { val := fun x => ↑(algebraMap 𝕜 A) c,
                            property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) },
                        map_one' :=
                          (_ :
                            (fun c =>
                                  { val := fun x => ↑(algebraMap 𝕜 A) c,
                                    property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
                                1 =
                              1) }
                      c₂) })
      (c₁ + c₂) =
    OneHom.toFun
        (↑{
            toOneHom :=
              {
                toFun := fun c =>
                  { val := fun x => ↑(algebraMap 𝕜 A) c,
                    property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) },
                map_one' :=
                  (_ :
                    (fun c =>
                          { val := fun x => ↑(algebraMap 𝕜 A) c,
                            property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
                        1 =
                      1) },
            map_mul' :=
              (_ :
                ∀ (c₁ c₂ : 𝕜),
                  OneHom.toFun
                      {
                        toFun := fun c =>
                          { val := fun x => ↑(algebraMap 𝕜 A) c,
                            property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) },
                        map_one' :=
                          (_ :
                            (fun c =>
                                  { val := fun x => ↑(algebraMap 𝕜 A) c,
                                    property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
                                1 =
                              1) }
                      (c₁ * c₂) =
                    OneHom.toFun
                        {
                          toFun := fun c =>
                            { val := fun x => ↑(algebraMap 𝕜 A) c,
                              property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) },
                          map_one' :=
                            (_ :
                              (fun c =>
                                    { val := fun x => ↑(algebraMap 𝕜 A) c,
                                      property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
                                  1 =
                                1) }
                        c₁ *
                      OneHom.toFun
                        {
                          toFun := fun c =>
                            { val := fun x => ↑(algebraMap 𝕜 A) c,
                              property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) },
                          map_one' :=
                            (_ :
                              (fun c =>
                                    { val := fun x => ↑(algebraMap 𝕜 A) c,
                                      property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
                                  1 =
                                1) }
                        c₂) })
        c₁ +
      OneHom.toFun
        (↑{
            toOneHom :=
              {
                toFun := fun c =>
                  { val := fun x => ↑(algebraMap 𝕜 A) c,
                    property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) },
                map_one' :=
                  (_ :
                    (fun c =>
                          { val := fun x => ↑(algebraMap 𝕜 A) c,
                            property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
                        1 =
                      1) },
            map_mul' :=
              (_ :
                ∀ (c₁ c₂ : 𝕜),
                  OneHom.toFun
                      {
                        toFun := fun c =>
                          { val := fun x => ↑(algebraMap 𝕜 A) c,
                            property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) },
                        map_one' :=
                          (_ :
                            (fun c =>
                                  { val := fun x => ↑(algebraMap 𝕜 A) c,
                                    property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
                                1 =
                              1) }
                      (c₁ * c₂) =
                    OneHom.toFun
                        {
                          toFun := fun c =>
                            { val := fun x => ↑(algebraMap 𝕜 A) c,
                              property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) },
                          map_one' :=
                            (_ :
                              (fun c =>
                                    { val := fun x => ↑(algebraMap 𝕜 A) c,
                                      property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
                                  1 =
                                1) }
                        c₁ *
                      OneHom.toFun
                        {
                          toFun := fun c =>
                            { val := fun x => ↑(algebraMap 𝕜 A) c,
                              property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) },
                          map_one' :=
                            (_ :
                              (fun c =>
                                    { val := fun x => ↑(algebraMap 𝕜 A) c,
                                      property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
                                  1 =
                                1) }
                        c₂) })
        c₂
[PROOFSTEP]
ext
[GOAL]
case h
𝕜 : Type u_1
inst✝¹⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁵ : NormedAddCommGroup E
inst✝¹⁴ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹³ : NormedAddCommGroup E'
inst✝¹² : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝¹⁰ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝⁹ : TopologicalSpace N
inst✝⁸ : ChartedSpace H N
E'' : Type u_7
inst✝⁷ : NormedAddCommGroup E''
inst✝⁶ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝⁵ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝⁴ : TopologicalSpace N'
inst✝³ : ChartedSpace H'' N'
A : Type u_10
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : SmoothRing 𝓘(𝕜, A) A
c₁ c₂ : 𝕜
x✝ : N
⊢ ↑(OneHom.toFun
          (↑{
              toOneHom :=
                {
                  toFun := fun c =>
                    { val := fun x => ↑(algebraMap 𝕜 A) c,
                      property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) },
                  map_one' :=
                    (_ :
                      (fun c =>
                            { val := fun x => ↑(algebraMap 𝕜 A) c,
                              property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
                          1 =
                        1) },
              map_mul' :=
                (_ :
                  ∀ (c₁ c₂ : 𝕜),
                    OneHom.toFun
                        {
                          toFun := fun c =>
                            { val := fun x => ↑(algebraMap 𝕜 A) c,
                              property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) },
                          map_one' :=
                            (_ :
                              (fun c =>
                                    { val := fun x => ↑(algebraMap 𝕜 A) c,
                                      property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
                                  1 =
                                1) }
                        (c₁ * c₂) =
                      OneHom.toFun
                          {
                            toFun := fun c =>
                              { val := fun x => ↑(algebraMap 𝕜 A) c,
                                property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) },
                            map_one' :=
                              (_ :
                                (fun c =>
                                      { val := fun x => ↑(algebraMap 𝕜 A) c,
                                        property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
                                    1 =
                                  1) }
                          c₁ *
                        OneHom.toFun
                          {
                            toFun := fun c =>
                              { val := fun x => ↑(algebraMap 𝕜 A) c,
                                property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) },
                            map_one' :=
                              (_ :
                                (fun c =>
                                      { val := fun x => ↑(algebraMap 𝕜 A) c,
                                        property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
                                    1 =
                                  1) }
                          c₂) })
          (c₁ + c₂))
      x✝ =
    ↑(OneHom.toFun
            (↑{
                toOneHom :=
                  {
                    toFun := fun c =>
                      { val := fun x => ↑(algebraMap 𝕜 A) c,
                        property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) },
                    map_one' :=
                      (_ :
                        (fun c =>
                              { val := fun x => ↑(algebraMap 𝕜 A) c,
                                property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
                            1 =
                          1) },
                map_mul' :=
                  (_ :
                    ∀ (c₁ c₂ : 𝕜),
                      OneHom.toFun
                          {
                            toFun := fun c =>
                              { val := fun x => ↑(algebraMap 𝕜 A) c,
                                property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) },
                            map_one' :=
                              (_ :
                                (fun c =>
                                      { val := fun x => ↑(algebraMap 𝕜 A) c,
                                        property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
                                    1 =
                                  1) }
                          (c₁ * c₂) =
                        OneHom.toFun
                            {
                              toFun := fun c =>
                                { val := fun x => ↑(algebraMap 𝕜 A) c,
                                  property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) },
                              map_one' :=
                                (_ :
                                  (fun c =>
                                        { val := fun x => ↑(algebraMap 𝕜 A) c,
                                          property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
                                      1 =
                                    1) }
                            c₁ *
                          OneHom.toFun
                            {
                              toFun := fun c =>
                                { val := fun x => ↑(algebraMap 𝕜 A) c,
                                  property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) },
                              map_one' :=
                                (_ :
                                  (fun c =>
                                        { val := fun x => ↑(algebraMap 𝕜 A) c,
                                          property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
                                      1 =
                                    1) }
                            c₂) })
            c₁ +
          OneHom.toFun
            (↑{
                toOneHom :=
                  {
                    toFun := fun c =>
                      { val := fun x => ↑(algebraMap 𝕜 A) c,
                        property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) },
                    map_one' :=
                      (_ :
                        (fun c =>
                              { val := fun x => ↑(algebraMap 𝕜 A) c,
                                property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
                            1 =
                          1) },
                map_mul' :=
                  (_ :
                    ∀ (c₁ c₂ : 𝕜),
                      OneHom.toFun
                          {
                            toFun := fun c =>
                              { val := fun x => ↑(algebraMap 𝕜 A) c,
                                property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) },
                            map_one' :=
                              (_ :
                                (fun c =>
                                      { val := fun x => ↑(algebraMap 𝕜 A) c,
                                        property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
                                    1 =
                                  1) }
                          (c₁ * c₂) =
                        OneHom.toFun
                            {
                              toFun := fun c =>
                                { val := fun x => ↑(algebraMap 𝕜 A) c,
                                  property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) },
                              map_one' :=
                                (_ :
                                  (fun c =>
                                        { val := fun x => ↑(algebraMap 𝕜 A) c,
                                          property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
                                      1 =
                                    1) }
                            c₁ *
                          OneHom.toFun
                            {
                              toFun := fun c =>
                                { val := fun x => ↑(algebraMap 𝕜 A) c,
                                  property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) },
                              map_one' :=
                                (_ :
                                  (fun c =>
                                        { val := fun x => ↑(algebraMap 𝕜 A) c,
                                          property := (_ : Smooth I 𝓘(𝕜, A) fun x => ↑(algebraMap 𝕜 A) c) })
                                      1 =
                                    1) }
                            c₂) })
            c₂)
      x✝
[PROOFSTEP]
exact (algebraMap 𝕜 A).map_add _ _
[GOAL]
𝕜 : Type u_1
inst✝¹⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁵ : NormedAddCommGroup E
inst✝¹⁴ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹³ : NormedAddCommGroup E'
inst✝¹² : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝¹⁰ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝⁹ : TopologicalSpace N
inst✝⁸ : ChartedSpace H N
E'' : Type u_7
inst✝⁷ : NormedAddCommGroup E''
inst✝⁶ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝⁵ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝⁴ : TopologicalSpace N'
inst✝³ : ChartedSpace H'' N'
A : Type u_10
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : SmoothRing 𝓘(𝕜, A) A
c : 𝕜
f : (fun x => C^⊤⟮I, N; 𝓘(𝕜, A), A⟯) c
⊢ ↑C c * f = f * ↑C c
[PROOFSTEP]
ext x
[GOAL]
case h
𝕜 : Type u_1
inst✝¹⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁵ : NormedAddCommGroup E
inst✝¹⁴ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹³ : NormedAddCommGroup E'
inst✝¹² : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝¹⁰ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝⁹ : TopologicalSpace N
inst✝⁸ : ChartedSpace H N
E'' : Type u_7
inst✝⁷ : NormedAddCommGroup E''
inst✝⁶ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝⁵ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝⁴ : TopologicalSpace N'
inst✝³ : ChartedSpace H'' N'
A : Type u_10
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : SmoothRing 𝓘(𝕜, A) A
c : 𝕜
f : (fun x => C^⊤⟮I, N; 𝓘(𝕜, A), A⟯) c
x : N
⊢ ↑(↑C c * f) x = ↑(f * ↑C c) x
[PROOFSTEP]
exact Algebra.commutes' _ _
[GOAL]
𝕜 : Type u_1
inst✝¹⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁵ : NormedAddCommGroup E
inst✝¹⁴ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹³ : NormedAddCommGroup E'
inst✝¹² : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝¹⁰ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝⁹ : TopologicalSpace N
inst✝⁸ : ChartedSpace H N
E'' : Type u_7
inst✝⁷ : NormedAddCommGroup E''
inst✝⁶ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝⁵ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝⁴ : TopologicalSpace N'
inst✝³ : ChartedSpace H'' N'
A : Type u_10
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : SmoothRing 𝓘(𝕜, A) A
c : 𝕜
f : (fun x => C^⊤⟮I, N; 𝓘(𝕜, A), A⟯) c
⊢ c • f = ↑C c * f
[PROOFSTEP]
ext x
[GOAL]
case h
𝕜 : Type u_1
inst✝¹⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁵ : NormedAddCommGroup E
inst✝¹⁴ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹³ : NormedAddCommGroup E'
inst✝¹² : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝¹⁰ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝⁹ : TopologicalSpace N
inst✝⁸ : ChartedSpace H N
E'' : Type u_7
inst✝⁷ : NormedAddCommGroup E''
inst✝⁶ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝⁵ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝⁴ : TopologicalSpace N'
inst✝³ : ChartedSpace H'' N'
A : Type u_10
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : SmoothRing 𝓘(𝕜, A) A
c : 𝕜
f : (fun x => C^⊤⟮I, N; 𝓘(𝕜, A), A⟯) c
x : N
⊢ ↑(c • f) x = ↑(↑C c * f) x
[PROOFSTEP]
exact Algebra.smul_def' _ _
[GOAL]
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹⁰ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝⁹ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝⁸ : TopologicalSpace N
inst✝⁷ : ChartedSpace H N
E'' : Type u_7
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝⁴ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝³ : TopologicalSpace N'
inst✝² : ChartedSpace H'' N'
V : Type u_10
inst✝¹ : NormedAddCommGroup V
inst✝ : NormedSpace 𝕜 V
f : C^⊤⟮I, N; 𝓘(𝕜, V), V⟯
⊢ 1 • f = f
[PROOFSTEP]
ext x
[GOAL]
case h
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹⁰ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝⁹ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝⁸ : TopologicalSpace N
inst✝⁷ : ChartedSpace H N
E'' : Type u_7
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝⁴ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝³ : TopologicalSpace N'
inst✝² : ChartedSpace H'' N'
V : Type u_10
inst✝¹ : NormedAddCommGroup V
inst✝ : NormedSpace 𝕜 V
f : C^⊤⟮I, N; 𝓘(𝕜, V), V⟯
x : N
⊢ ↑(1 • f) x = ↑f x
[PROOFSTEP]
exact one_smul 𝕜 (f x)
[GOAL]
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹⁰ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝⁹ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝⁸ : TopologicalSpace N
inst✝⁷ : ChartedSpace H N
E'' : Type u_7
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝⁴ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝³ : TopologicalSpace N'
inst✝² : ChartedSpace H'' N'
V : Type u_10
inst✝¹ : NormedAddCommGroup V
inst✝ : NormedSpace 𝕜 V
c₁ c₂ : C^⊤⟮I, N; 𝓘(𝕜, 𝕜), 𝕜⟯
f : C^⊤⟮I, N; 𝓘(𝕜, V), V⟯
⊢ (c₁ * c₂) • f = c₁ • c₂ • f
[PROOFSTEP]
ext x
[GOAL]
case h
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹⁰ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝⁹ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝⁸ : TopologicalSpace N
inst✝⁷ : ChartedSpace H N
E'' : Type u_7
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝⁴ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝³ : TopologicalSpace N'
inst✝² : ChartedSpace H'' N'
V : Type u_10
inst✝¹ : NormedAddCommGroup V
inst✝ : NormedSpace 𝕜 V
c₁ c₂ : C^⊤⟮I, N; 𝓘(𝕜, 𝕜), 𝕜⟯
f : C^⊤⟮I, N; 𝓘(𝕜, V), V⟯
x : N
⊢ ↑((c₁ * c₂) • f) x = ↑(c₁ • c₂ • f) x
[PROOFSTEP]
exact mul_smul (c₁ x) (c₂ x) (f x)
[GOAL]
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹⁰ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝⁹ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝⁸ : TopologicalSpace N
inst✝⁷ : ChartedSpace H N
E'' : Type u_7
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝⁴ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝³ : TopologicalSpace N'
inst✝² : ChartedSpace H'' N'
V : Type u_10
inst✝¹ : NormedAddCommGroup V
inst✝ : NormedSpace 𝕜 V
r : C^⊤⟮I, N; 𝓘(𝕜, 𝕜), 𝕜⟯
⊢ r • 0 = 0
[PROOFSTEP]
ext x
[GOAL]
case h
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹⁰ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝⁹ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝⁸ : TopologicalSpace N
inst✝⁷ : ChartedSpace H N
E'' : Type u_7
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝⁴ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝³ : TopologicalSpace N'
inst✝² : ChartedSpace H'' N'
V : Type u_10
inst✝¹ : NormedAddCommGroup V
inst✝ : NormedSpace 𝕜 V
r : C^⊤⟮I, N; 𝓘(𝕜, 𝕜), 𝕜⟯
x : N
⊢ ↑(r • 0) x = ↑0 x
[PROOFSTEP]
exact smul_zero _
[GOAL]
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹⁰ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝⁹ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝⁸ : TopologicalSpace N
inst✝⁷ : ChartedSpace H N
E'' : Type u_7
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝⁴ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝³ : TopologicalSpace N'
inst✝² : ChartedSpace H'' N'
V : Type u_10
inst✝¹ : NormedAddCommGroup V
inst✝ : NormedSpace 𝕜 V
c : C^⊤⟮I, N; 𝓘(𝕜, 𝕜), 𝕜⟯
f g : C^⊤⟮I, N; 𝓘(𝕜, V), V⟯
⊢ c • (f + g) = c • f + c • g
[PROOFSTEP]
ext x
[GOAL]
case h
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹⁰ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝⁹ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝⁸ : TopologicalSpace N
inst✝⁷ : ChartedSpace H N
E'' : Type u_7
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝⁴ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝³ : TopologicalSpace N'
inst✝² : ChartedSpace H'' N'
V : Type u_10
inst✝¹ : NormedAddCommGroup V
inst✝ : NormedSpace 𝕜 V
c : C^⊤⟮I, N; 𝓘(𝕜, 𝕜), 𝕜⟯
f g : C^⊤⟮I, N; 𝓘(𝕜, V), V⟯
x : N
⊢ ↑(c • (f + g)) x = ↑(c • f + c • g) x
[PROOFSTEP]
exact smul_add (c x) (f x) (g x)
[GOAL]
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹⁰ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝⁹ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝⁸ : TopologicalSpace N
inst✝⁷ : ChartedSpace H N
E'' : Type u_7
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝⁴ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝³ : TopologicalSpace N'
inst✝² : ChartedSpace H'' N'
V : Type u_10
inst✝¹ : NormedAddCommGroup V
inst✝ : NormedSpace 𝕜 V
c₁ c₂ : C^⊤⟮I, N; 𝓘(𝕜, 𝕜), 𝕜⟯
f : C^⊤⟮I, N; 𝓘(𝕜, V), V⟯
⊢ (c₁ + c₂) • f = c₁ • f + c₂ • f
[PROOFSTEP]
ext x
[GOAL]
case h
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹⁰ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝⁹ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝⁸ : TopologicalSpace N
inst✝⁷ : ChartedSpace H N
E'' : Type u_7
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝⁴ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝³ : TopologicalSpace N'
inst✝² : ChartedSpace H'' N'
V : Type u_10
inst✝¹ : NormedAddCommGroup V
inst✝ : NormedSpace 𝕜 V
c₁ c₂ : C^⊤⟮I, N; 𝓘(𝕜, 𝕜), 𝕜⟯
f : C^⊤⟮I, N; 𝓘(𝕜, V), V⟯
x : N
⊢ ↑((c₁ + c₂) • f) x = ↑(c₁ • f + c₂ • f) x
[PROOFSTEP]
exact add_smul (c₁ x) (c₂ x) (f x)
[GOAL]
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹⁰ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝⁹ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝⁸ : TopologicalSpace N
inst✝⁷ : ChartedSpace H N
E'' : Type u_7
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝⁴ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝³ : TopologicalSpace N'
inst✝² : ChartedSpace H'' N'
V : Type u_10
inst✝¹ : NormedAddCommGroup V
inst✝ : NormedSpace 𝕜 V
f : C^⊤⟮I, N; 𝓘(𝕜, V), V⟯
⊢ 0 • f = 0
[PROOFSTEP]
ext x
[GOAL]
case h
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹⁰ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝⁹ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝⁸ : TopologicalSpace N
inst✝⁷ : ChartedSpace H N
E'' : Type u_7
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝⁴ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝³ : TopologicalSpace N'
inst✝² : ChartedSpace H'' N'
V : Type u_10
inst✝¹ : NormedAddCommGroup V
inst✝ : NormedSpace 𝕜 V
f : C^⊤⟮I, N; 𝓘(𝕜, V), V⟯
x : N
⊢ ↑(0 • f) x = ↑0 x
[PROOFSTEP]
exact zero_smul _ _