[GOAL]
H : Type u_1
inst✝⁵ : TopologicalSpace H
H' : Type u_2
inst✝⁴ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
M : Type u
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
M' : Type u
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
hG : LocalInvariantProp G G' P
⊢ ∀ {U V : Opens ↑(TopCat.of M)} (i : U ⟶ V) (f : { x // x ∈ V } → M'),
    (fun {U} f => ChartedSpace.LiftProp P f) f →
      (fun {U} f => ChartedSpace.LiftProp P f) fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑V) }) x)
[PROOFSTEP]
intro U V i f h x
[GOAL]
H : Type u_1
inst✝⁵ : TopologicalSpace H
H' : Type u_2
inst✝⁴ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
M : Type u
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
M' : Type u
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
hG : LocalInvariantProp G G' P
U V : Opens ↑(TopCat.of M)
i : U ⟶ V
f : { x // x ∈ V } → M'
h : ChartedSpace.LiftProp P f
x : { x // x ∈ U }
⊢ ChartedSpace.LiftPropAt P (fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑V) }) x)) x
[PROOFSTEP]
have hUV : U ≤ V := CategoryTheory.leOfHom i
[GOAL]
H : Type u_1
inst✝⁵ : TopologicalSpace H
H' : Type u_2
inst✝⁴ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
M : Type u
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
M' : Type u
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
hG : LocalInvariantProp G G' P
U V : Opens ↑(TopCat.of M)
i : U ⟶ V
f : { x // x ∈ V } → M'
h : ChartedSpace.LiftProp P f
x : { x // x ∈ U }
hUV : U ≤ V
⊢ ChartedSpace.LiftPropAt P (fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑V) }) x)) x
[PROOFSTEP]
show ChartedSpace.LiftPropAt P (f ∘ Set.inclusion hUV) x
[GOAL]
H : Type u_1
inst✝⁵ : TopologicalSpace H
H' : Type u_2
inst✝⁴ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
M : Type u
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
M' : Type u
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
hG : LocalInvariantProp G G' P
U V : Opens ↑(TopCat.of M)
i : U ⟶ V
f : { x // x ∈ V } → M'
h : ChartedSpace.LiftProp P f
x : { x // x ∈ U }
hUV : U ≤ V
⊢ ChartedSpace.LiftPropAt P (f ∘ inclusion hUV) x
[PROOFSTEP]
rw [← hG.liftPropAt_iff_comp_inclusion hUV]
[GOAL]
H : Type u_1
inst✝⁵ : TopologicalSpace H
H' : Type u_2
inst✝⁴ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
M : Type u
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
M' : Type u
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
hG : LocalInvariantProp G G' P
U V : Opens ↑(TopCat.of M)
i : U ⟶ V
f : { x // x ∈ V } → M'
h : ChartedSpace.LiftProp P f
x : { x // x ∈ U }
hUV : U ≤ V
⊢ ChartedSpace.LiftPropAt P f (inclusion hUV x)
[PROOFSTEP]
apply h
[GOAL]
H : Type u_1
inst✝⁵ : TopologicalSpace H
H' : Type u_2
inst✝⁴ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
M : Type u
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
M' : Type u
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
hG : LocalInvariantProp G G' P
⊢ ∀ {U : Opens ↑(TopCat.of M)} (f : { x // x ∈ U } → M'),
    (∀ (x : { x // x ∈ U }),
        ∃ V x i,
          TopCat.PrelocalPredicate.pred
            { pred := fun {U} f => ChartedSpace.LiftProp P f,
              res :=
                (_ :
                  ∀ {U V : Opens ↑(TopCat.of M)} (i : U ⟶ V) (f : { x // x ∈ V } → M'),
                    ChartedSpace.LiftProp P f →
                      ∀ (x : { x // x ∈ U }), ChartedSpace.LiftPropAt P (f ∘ inclusion (_ : U ≤ V)) x) }
            fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U) }) x)) →
      TopCat.PrelocalPredicate.pred
        { pred := fun {U} f => ChartedSpace.LiftProp P f,
          res :=
            (_ :
              ∀ {U V : Opens ↑(TopCat.of M)} (i : U ⟶ V) (f : { x // x ∈ V } → M'),
                ChartedSpace.LiftProp P f →
                  ∀ (x : { x // x ∈ U }), ChartedSpace.LiftPropAt P (f ∘ inclusion (_ : U ≤ V)) x) }
        f
[PROOFSTEP]
intro V f h x
[GOAL]
H : Type u_1
inst✝⁵ : TopologicalSpace H
H' : Type u_2
inst✝⁴ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
M : Type u
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
M' : Type u
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
hG : LocalInvariantProp G G' P
V : Opens ↑(TopCat.of M)
f : { x // x ∈ V } → M'
h :
  ∀ (x : { x // x ∈ V }),
    ∃ V_1 x i,
      TopCat.PrelocalPredicate.pred
        { pred := fun {U} f => ChartedSpace.LiftProp P f,
          res :=
            (_ :
              ∀ {U V : Opens ↑(TopCat.of M)} (i : U ⟶ V) (f : { x // x ∈ V } → M'),
                ChartedSpace.LiftProp P f →
                  ∀ (x : { x // x ∈ U }), ChartedSpace.LiftPropAt P (f ∘ inclusion (_ : U ≤ V)) x) }
        fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑V) }) x)
x : { x // x ∈ V }
⊢ ChartedSpace.LiftPropAt P f x
[PROOFSTEP]
obtain ⟨U, hxU, i, hU : ChartedSpace.LiftProp P (f ∘ i)⟩ := h x
[GOAL]
case intro.intro.intro
H : Type u_1
inst✝⁵ : TopologicalSpace H
H' : Type u_2
inst✝⁴ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
M : Type u
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
M' : Type u
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
hG : LocalInvariantProp G G' P
V : Opens ↑(TopCat.of M)
f : { x // x ∈ V } → M'
h :
  ∀ (x : { x // x ∈ V }),
    ∃ V_1 x i,
      TopCat.PrelocalPredicate.pred
        { pred := fun {U} f => ChartedSpace.LiftProp P f,
          res :=
            (_ :
              ∀ {U V : Opens ↑(TopCat.of M)} (i : U ⟶ V) (f : { x // x ∈ V } → M'),
                ChartedSpace.LiftProp P f →
                  ∀ (x : { x // x ∈ U }), ChartedSpace.LiftPropAt P (f ∘ inclusion (_ : U ≤ V)) x) }
        fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑V) }) x)
x : { x // x ∈ V }
U : Opens ↑(TopCat.of M)
hxU : ↑x ∈ U
i : U ⟶ V
hU : ChartedSpace.LiftProp P (f ∘ fun x => { val := ↑x, property := (_ : ↑x ∈ ↑V) })
⊢ ChartedSpace.LiftPropAt P f x
[PROOFSTEP]
let x' : U := ⟨x, hxU⟩
[GOAL]
case intro.intro.intro
H : Type u_1
inst✝⁵ : TopologicalSpace H
H' : Type u_2
inst✝⁴ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
M : Type u
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
M' : Type u
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
hG : LocalInvariantProp G G' P
V : Opens ↑(TopCat.of M)
f : { x // x ∈ V } → M'
h :
  ∀ (x : { x // x ∈ V }),
    ∃ V_1 x i,
      TopCat.PrelocalPredicate.pred
        { pred := fun {U} f => ChartedSpace.LiftProp P f,
          res :=
            (_ :
              ∀ {U V : Opens ↑(TopCat.of M)} (i : U ⟶ V) (f : { x // x ∈ V } → M'),
                ChartedSpace.LiftProp P f →
                  ∀ (x : { x // x ∈ U }), ChartedSpace.LiftPropAt P (f ∘ inclusion (_ : U ≤ V)) x) }
        fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑V) }) x)
x : { x // x ∈ V }
U : Opens ↑(TopCat.of M)
hxU : ↑x ∈ U
i : U ⟶ V
hU : ChartedSpace.LiftProp P (f ∘ fun x => { val := ↑x, property := (_ : ↑x ∈ ↑V) })
x' : { x // x ∈ U } := { val := ↑x, property := hxU }
⊢ ChartedSpace.LiftPropAt P f x
[PROOFSTEP]
have hUV : U ≤ V := CategoryTheory.leOfHom i
[GOAL]
case intro.intro.intro
H : Type u_1
inst✝⁵ : TopologicalSpace H
H' : Type u_2
inst✝⁴ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
M : Type u
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
M' : Type u
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
hG : LocalInvariantProp G G' P
V : Opens ↑(TopCat.of M)
f : { x // x ∈ V } → M'
h :
  ∀ (x : { x // x ∈ V }),
    ∃ V_1 x i,
      TopCat.PrelocalPredicate.pred
        { pred := fun {U} f => ChartedSpace.LiftProp P f,
          res :=
            (_ :
              ∀ {U V : Opens ↑(TopCat.of M)} (i : U ⟶ V) (f : { x // x ∈ V } → M'),
                ChartedSpace.LiftProp P f →
                  ∀ (x : { x // x ∈ U }), ChartedSpace.LiftPropAt P (f ∘ inclusion (_ : U ≤ V)) x) }
        fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑V) }) x)
x : { x // x ∈ V }
U : Opens ↑(TopCat.of M)
hxU : ↑x ∈ U
i : U ⟶ V
hU : ChartedSpace.LiftProp P (f ∘ fun x => { val := ↑x, property := (_ : ↑x ∈ ↑V) })
x' : { x // x ∈ U } := { val := ↑x, property := hxU }
hUV : U ≤ V
⊢ ChartedSpace.LiftPropAt P f x
[PROOFSTEP]
have : ChartedSpace.LiftPropAt P f (inclusion hUV x') :=
  by
  rw [hG.liftPropAt_iff_comp_inclusion hUV]
  exact hU x'
[GOAL]
H : Type u_1
inst✝⁵ : TopologicalSpace H
H' : Type u_2
inst✝⁴ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
M : Type u
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
M' : Type u
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
hG : LocalInvariantProp G G' P
V : Opens ↑(TopCat.of M)
f : { x // x ∈ V } → M'
h :
  ∀ (x : { x // x ∈ V }),
    ∃ V_1 x i,
      TopCat.PrelocalPredicate.pred
        { pred := fun {U} f => ChartedSpace.LiftProp P f,
          res :=
            (_ :
              ∀ {U V : Opens ↑(TopCat.of M)} (i : U ⟶ V) (f : { x // x ∈ V } → M'),
                ChartedSpace.LiftProp P f →
                  ∀ (x : { x // x ∈ U }), ChartedSpace.LiftPropAt P (f ∘ inclusion (_ : U ≤ V)) x) }
        fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑V) }) x)
x : { x // x ∈ V }
U : Opens ↑(TopCat.of M)
hxU : ↑x ∈ U
i : U ⟶ V
hU : ChartedSpace.LiftProp P (f ∘ fun x => { val := ↑x, property := (_ : ↑x ∈ ↑V) })
x' : { x // x ∈ U } := { val := ↑x, property := hxU }
hUV : U ≤ V
⊢ ChartedSpace.LiftPropAt P f (inclusion hUV x')
[PROOFSTEP]
rw [hG.liftPropAt_iff_comp_inclusion hUV]
[GOAL]
H : Type u_1
inst✝⁵ : TopologicalSpace H
H' : Type u_2
inst✝⁴ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
M : Type u
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
M' : Type u
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
hG : LocalInvariantProp G G' P
V : Opens ↑(TopCat.of M)
f : { x // x ∈ V } → M'
h :
  ∀ (x : { x // x ∈ V }),
    ∃ V_1 x i,
      TopCat.PrelocalPredicate.pred
        { pred := fun {U} f => ChartedSpace.LiftProp P f,
          res :=
            (_ :
              ∀ {U V : Opens ↑(TopCat.of M)} (i : U ⟶ V) (f : { x // x ∈ V } → M'),
                ChartedSpace.LiftProp P f →
                  ∀ (x : { x // x ∈ U }), ChartedSpace.LiftPropAt P (f ∘ inclusion (_ : U ≤ V)) x) }
        fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑V) }) x)
x : { x // x ∈ V }
U : Opens ↑(TopCat.of M)
hxU : ↑x ∈ U
i : U ⟶ V
hU : ChartedSpace.LiftProp P (f ∘ fun x => { val := ↑x, property := (_ : ↑x ∈ ↑V) })
x' : { x // x ∈ U } := { val := ↑x, property := hxU }
hUV : U ≤ V
⊢ ChartedSpace.LiftPropAt P (f ∘ inclusion hUV) x'
[PROOFSTEP]
exact hU x'
[GOAL]
case intro.intro.intro
H : Type u_1
inst✝⁵ : TopologicalSpace H
H' : Type u_2
inst✝⁴ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
M : Type u
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
M' : Type u
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
hG : LocalInvariantProp G G' P
V : Opens ↑(TopCat.of M)
f : { x // x ∈ V } → M'
h :
  ∀ (x : { x // x ∈ V }),
    ∃ V_1 x i,
      TopCat.PrelocalPredicate.pred
        { pred := fun {U} f => ChartedSpace.LiftProp P f,
          res :=
            (_ :
              ∀ {U V : Opens ↑(TopCat.of M)} (i : U ⟶ V) (f : { x // x ∈ V } → M'),
                ChartedSpace.LiftProp P f →
                  ∀ (x : { x // x ∈ U }), ChartedSpace.LiftPropAt P (f ∘ inclusion (_ : U ≤ V)) x) }
        fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑V) }) x)
x : { x // x ∈ V }
U : Opens ↑(TopCat.of M)
hxU : ↑x ∈ U
i : U ⟶ V
hU : ChartedSpace.LiftProp P (f ∘ fun x => { val := ↑x, property := (_ : ↑x ∈ ↑V) })
x' : { x // x ∈ U } := { val := ↑x, property := hxU }
hUV : U ≤ V
this : ChartedSpace.LiftPropAt P f (inclusion hUV x')
⊢ ChartedSpace.LiftPropAt P f x
[PROOFSTEP]
convert this


[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ IsRadical I ↔ IsReduced (R ⧸ I)
[PROOFSTEP]
conv_lhs => rw [← @Ideal.mk_ker R _ I]
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
| IsRadical I
[PROOFSTEP]
rw [← @Ideal.mk_ker R _ I]
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
| IsRadical I
[PROOFSTEP]
rw [← @Ideal.mk_ker R _ I]
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
| IsRadical I
[PROOFSTEP]
rw [← @Ideal.mk_ker R _ I]
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ IsRadical (RingHom.ker (Quotient.mk I)) ↔ IsReduced (R ⧸ I)
[PROOFSTEP]
exact RingHom.ker_isRadical_iff_reduced_of_surjective (@Ideal.Quotient.mk_surjective R _ I)
[GOAL]
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal S
hI : IsNilpotent I
P : ⦃S : Type u_2⦄ → [inst : CommRing S] → Ideal S → Prop
h₁ : ∀ ⦃S : Type u_2⦄ [inst : CommRing S] (I : Ideal S), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_2⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
⊢ P I
[PROOFSTEP]
obtain ⟨n, hI : I ^ n = ⊥⟩ := hI
[GOAL]
case intro
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal S
P : ⦃S : Type u_2⦄ → [inst : CommRing S] → Ideal S → Prop
h₁ : ∀ ⦃S : Type u_2⦄ [inst : CommRing S] (I : Ideal S), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_2⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
n : ℕ
hI : I ^ n = ⊥
⊢ P I
[PROOFSTEP]
induction' n using Nat.strong_induction_on with n H generalizing S
[GOAL]
case intro.h
R : Type u_1
S✝ : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : CommRing S✝
inst✝² : Algebra R S✝
I✝ : Ideal S✝
P : ⦃S : Type u_2⦄ → [inst : CommRing S] → Ideal S → Prop
h₁ : ∀ ⦃S : Type u_2⦄ [inst : CommRing S] (I : Ideal S), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_2⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
n✝ : ℕ
hI✝ : I✝ ^ n✝ = ⊥
n : ℕ
H : ∀ (m : ℕ), m < n → ∀ {S : Type u_2} [inst : CommRing S] [inst_1 : Algebra R S] (I : Ideal S), I ^ m = ⊥ → P I
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal S
hI : I ^ n = ⊥
⊢ P I
[PROOFSTEP]
by_cases hI' : I = ⊥
[GOAL]
case pos
R : Type u_1
S✝ : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : CommRing S✝
inst✝² : Algebra R S✝
I✝ : Ideal S✝
P : ⦃S : Type u_2⦄ → [inst : CommRing S] → Ideal S → Prop
h₁ : ∀ ⦃S : Type u_2⦄ [inst : CommRing S] (I : Ideal S), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_2⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
n✝ : ℕ
hI✝ : I✝ ^ n✝ = ⊥
n : ℕ
H : ∀ (m : ℕ), m < n → ∀ {S : Type u_2} [inst : CommRing S] [inst_1 : Algebra R S] (I : Ideal S), I ^ m = ⊥ → P I
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal S
hI : I ^ n = ⊥
hI' : I = ⊥
⊢ P I
[PROOFSTEP]
subst hI'
[GOAL]
case pos
R : Type u_1
S✝ : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : CommRing S✝
inst✝² : Algebra R S✝
I : Ideal S✝
P : ⦃S : Type u_2⦄ → [inst : CommRing S] → Ideal S → Prop
h₁ : ∀ ⦃S : Type u_2⦄ [inst : CommRing S] (I : Ideal S), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_2⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
n✝ : ℕ
hI✝ : I ^ n✝ = ⊥
n : ℕ
H : ∀ (m : ℕ), m < n → ∀ {S : Type u_2} [inst : CommRing S] [inst_1 : Algebra R S] (I : Ideal S), I ^ m = ⊥ → P I
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
hI : ⊥ ^ n = ⊥
⊢ P ⊥
[PROOFSTEP]
apply h₁
[GOAL]
case pos.a
R : Type u_1
S✝ : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : CommRing S✝
inst✝² : Algebra R S✝
I : Ideal S✝
P : ⦃S : Type u_2⦄ → [inst : CommRing S] → Ideal S → Prop
h₁ : ∀ ⦃S : Type u_2⦄ [inst : CommRing S] (I : Ideal S), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_2⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
n✝ : ℕ
hI✝ : I ^ n✝ = ⊥
n : ℕ
H : ∀ (m : ℕ), m < n → ∀ {S : Type u_2} [inst : CommRing S] [inst_1 : Algebra R S] (I : Ideal S), I ^ m = ⊥ → P I
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
hI : ⊥ ^ n = ⊥
⊢ ⊥ ^ 2 = ⊥
[PROOFSTEP]
rw [← Ideal.zero_eq_bot, zero_pow]
[GOAL]
case pos.a
R : Type u_1
S✝ : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : CommRing S✝
inst✝² : Algebra R S✝
I : Ideal S✝
P : ⦃S : Type u_2⦄ → [inst : CommRing S] → Ideal S → Prop
h₁ : ∀ ⦃S : Type u_2⦄ [inst : CommRing S] (I : Ideal S), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_2⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
n✝ : ℕ
hI✝ : I ^ n✝ = ⊥
n : ℕ
H : ∀ (m : ℕ), m < n → ∀ {S : Type u_2} [inst : CommRing S] [inst_1 : Algebra R S] (I : Ideal S), I ^ m = ⊥ → P I
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
hI : ⊥ ^ n = ⊥
⊢ 0 < 2
[PROOFSTEP]
exact zero_lt_two
[GOAL]
case neg
R : Type u_1
S✝ : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : CommRing S✝
inst✝² : Algebra R S✝
I✝ : Ideal S✝
P : ⦃S : Type u_2⦄ → [inst : CommRing S] → Ideal S → Prop
h₁ : ∀ ⦃S : Type u_2⦄ [inst : CommRing S] (I : Ideal S), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_2⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
n✝ : ℕ
hI✝ : I✝ ^ n✝ = ⊥
n : ℕ
H : ∀ (m : ℕ), m < n → ∀ {S : Type u_2} [inst : CommRing S] [inst_1 : Algebra R S] (I : Ideal S), I ^ m = ⊥ → P I
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal S
hI : I ^ n = ⊥
hI' : ¬I = ⊥
⊢ P I
[PROOFSTEP]
cases' n with n
[GOAL]
case neg.zero
R : Type u_1
S✝ : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : CommRing S✝
inst✝² : Algebra R S✝
I✝ : Ideal S✝
P : ⦃S : Type u_2⦄ → [inst : CommRing S] → Ideal S → Prop
h₁ : ∀ ⦃S : Type u_2⦄ [inst : CommRing S] (I : Ideal S), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_2⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
n : ℕ
hI✝ : I✝ ^ n = ⊥
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal S
hI' : ¬I = ⊥
H : ∀ (m : ℕ), m < Nat.zero → ∀ {S : Type u_2} [inst : CommRing S] [inst_1 : Algebra R S] (I : Ideal S), I ^ m = ⊥ → P I
hI : I ^ Nat.zero = ⊥
⊢ P I
[PROOFSTEP]
rw [pow_zero, Ideal.one_eq_top] at hI
[GOAL]
case neg.zero
R : Type u_1
S✝ : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : CommRing S✝
inst✝² : Algebra R S✝
I✝ : Ideal S✝
P : ⦃S : Type u_2⦄ → [inst : CommRing S] → Ideal S → Prop
h₁ : ∀ ⦃S : Type u_2⦄ [inst : CommRing S] (I : Ideal S), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_2⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
n : ℕ
hI✝ : I✝ ^ n = ⊥
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal S
hI' : ¬I = ⊥
H : ∀ (m : ℕ), m < Nat.zero → ∀ {S : Type u_2} [inst : CommRing S] [inst_1 : Algebra R S] (I : Ideal S), I ^ m = ⊥ → P I
hI : ⊤ = ⊥
⊢ P I
[PROOFSTEP]
haveI := subsingleton_of_bot_eq_top hI.symm
[GOAL]
case neg.zero
R : Type u_1
S✝ : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : CommRing S✝
inst✝² : Algebra R S✝
I✝ : Ideal S✝
P : ⦃S : Type u_2⦄ → [inst : CommRing S] → Ideal S → Prop
h₁ : ∀ ⦃S : Type u_2⦄ [inst : CommRing S] (I : Ideal S), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_2⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
n : ℕ
hI✝ : I✝ ^ n = ⊥
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal S
hI' : ¬I = ⊥
H : ∀ (m : ℕ), m < Nat.zero → ∀ {S : Type u_2} [inst : CommRing S] [inst_1 : Algebra R S] (I : Ideal S), I ^ m = ⊥ → P I
hI : ⊤ = ⊥
this : Subsingleton (Ideal S)
⊢ P I
[PROOFSTEP]
exact (hI' (Subsingleton.elim _ _)).elim
[GOAL]
case neg.succ
R : Type u_1
S✝ : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : CommRing S✝
inst✝² : Algebra R S✝
I✝ : Ideal S✝
P : ⦃S : Type u_2⦄ → [inst : CommRing S] → Ideal S → Prop
h₁ : ∀ ⦃S : Type u_2⦄ [inst : CommRing S] (I : Ideal S), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_2⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
n✝ : ℕ
hI✝ : I✝ ^ n✝ = ⊥
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal S
hI' : ¬I = ⊥
n : ℕ
H :
  ∀ (m : ℕ), m < Nat.succ n → ∀ {S : Type u_2} [inst : CommRing S] [inst_1 : Algebra R S] (I : Ideal S), I ^ m = ⊥ → P I
hI : I ^ Nat.succ n = ⊥
⊢ P I
[PROOFSTEP]
cases' n with n
[GOAL]
case neg.succ.zero
R : Type u_1
S✝ : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : CommRing S✝
inst✝² : Algebra R S✝
I✝ : Ideal S✝
P : ⦃S : Type u_2⦄ → [inst : CommRing S] → Ideal S → Prop
h₁ : ∀ ⦃S : Type u_2⦄ [inst : CommRing S] (I : Ideal S), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_2⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
n : ℕ
hI✝ : I✝ ^ n = ⊥
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal S
hI' : ¬I = ⊥
H :
  ∀ (m : ℕ),
    m < Nat.succ Nat.zero → ∀ {S : Type u_2} [inst : CommRing S] [inst_1 : Algebra R S] (I : Ideal S), I ^ m = ⊥ → P I
hI : I ^ Nat.succ Nat.zero = ⊥
⊢ P I
[PROOFSTEP]
rw [pow_one] at hI
[GOAL]
case neg.succ.zero
R : Type u_1
S✝ : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : CommRing S✝
inst✝² : Algebra R S✝
I✝ : Ideal S✝
P : ⦃S : Type u_2⦄ → [inst : CommRing S] → Ideal S → Prop
h₁ : ∀ ⦃S : Type u_2⦄ [inst : CommRing S] (I : Ideal S), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_2⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
n : ℕ
hI✝ : I✝ ^ n = ⊥
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal S
hI' : ¬I = ⊥
H :
  ∀ (m : ℕ),
    m < Nat.succ Nat.zero → ∀ {S : Type u_2} [inst : CommRing S] [inst_1 : Algebra R S] (I : Ideal S), I ^ m = ⊥ → P I
hI : I = ⊥
⊢ P I
[PROOFSTEP]
exact (hI' hI).elim
[GOAL]
case neg.succ.succ
R : Type u_1
S✝ : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : CommRing S✝
inst✝² : Algebra R S✝
I✝ : Ideal S✝
P : ⦃S : Type u_2⦄ → [inst : CommRing S] → Ideal S → Prop
h₁ : ∀ ⦃S : Type u_2⦄ [inst : CommRing S] (I : Ideal S), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_2⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
n✝ : ℕ
hI✝ : I✝ ^ n✝ = ⊥
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal S
hI' : ¬I = ⊥
n : ℕ
H :
  ∀ (m : ℕ),
    m < Nat.succ (Nat.succ n) →
      ∀ {S : Type u_2} [inst : CommRing S] [inst_1 : Algebra R S] (I : Ideal S), I ^ m = ⊥ → P I
hI : I ^ Nat.succ (Nat.succ n) = ⊥
⊢ P I
[PROOFSTEP]
apply h₂ (I ^ 2) _ (Ideal.pow_le_self two_ne_zero)
[GOAL]
case neg.succ.succ.a
R : Type u_1
S✝ : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : CommRing S✝
inst✝² : Algebra R S✝
I✝ : Ideal S✝
P : ⦃S : Type u_2⦄ → [inst : CommRing S] → Ideal S → Prop
h₁ : ∀ ⦃S : Type u_2⦄ [inst : CommRing S] (I : Ideal S), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_2⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
n✝ : ℕ
hI✝ : I✝ ^ n✝ = ⊥
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal S
hI' : ¬I = ⊥
n : ℕ
H :
  ∀ (m : ℕ),
    m < Nat.succ (Nat.succ n) →
      ∀ {S : Type u_2} [inst : CommRing S] [inst_1 : Algebra R S] (I : Ideal S), I ^ m = ⊥ → P I
hI : I ^ Nat.succ (Nat.succ n) = ⊥
⊢ P (I ^ 2)
[PROOFSTEP]
apply H n.succ _ (I ^ 2)
[GOAL]
case neg.succ.succ.a
R : Type u_1
S✝ : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : CommRing S✝
inst✝² : Algebra R S✝
I✝ : Ideal S✝
P : ⦃S : Type u_2⦄ → [inst : CommRing S] → Ideal S → Prop
h₁ : ∀ ⦃S : Type u_2⦄ [inst : CommRing S] (I : Ideal S), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_2⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
n✝ : ℕ
hI✝ : I✝ ^ n✝ = ⊥
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal S
hI' : ¬I = ⊥
n : ℕ
H :
  ∀ (m : ℕ),
    m < Nat.succ (Nat.succ n) →
      ∀ {S : Type u_2} [inst : CommRing S] [inst_1 : Algebra R S] (I : Ideal S), I ^ m = ⊥ → P I
hI : I ^ Nat.succ (Nat.succ n) = ⊥
⊢ (I ^ 2) ^ Nat.succ n = ⊥
[PROOFSTEP]
rw [← pow_mul, eq_bot_iff, ← hI, Nat.succ_eq_add_one, Nat.succ_eq_add_one]
[GOAL]
case neg.succ.succ.a
R : Type u_1
S✝ : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : CommRing S✝
inst✝² : Algebra R S✝
I✝ : Ideal S✝
P : ⦃S : Type u_2⦄ → [inst : CommRing S] → Ideal S → Prop
h₁ : ∀ ⦃S : Type u_2⦄ [inst : CommRing S] (I : Ideal S), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_2⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
n✝ : ℕ
hI✝ : I✝ ^ n✝ = ⊥
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal S
hI' : ¬I = ⊥
n : ℕ
H :
  ∀ (m : ℕ),
    m < Nat.succ (Nat.succ n) →
      ∀ {S : Type u_2} [inst : CommRing S] [inst_1 : Algebra R S] (I : Ideal S), I ^ m = ⊥ → P I
hI : I ^ Nat.succ (Nat.succ n) = ⊥
⊢ I ^ (2 * (n + 1)) ≤ I ^ (n + 1 + 1)
[PROOFSTEP]
apply Ideal.pow_le_pow (by linarith)
[GOAL]
R : Type u_1
S✝ : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : CommRing S✝
inst✝² : Algebra R S✝
I✝ : Ideal S✝
P : ⦃S : Type u_2⦄ → [inst : CommRing S] → Ideal S → Prop
h₁ : ∀ ⦃S : Type u_2⦄ [inst : CommRing S] (I : Ideal S), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_2⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
n✝ : ℕ
hI✝ : I✝ ^ n✝ = ⊥
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal S
hI' : ¬I = ⊥
n : ℕ
H :
  ∀ (m : ℕ),
    m < Nat.succ (Nat.succ n) →
      ∀ {S : Type u_2} [inst : CommRing S] [inst_1 : Algebra R S] (I : Ideal S), I ^ m = ⊥ → P I
hI : I ^ Nat.succ (Nat.succ n) = ⊥
⊢ n + 1 + 1 ≤ 2 * (n + 1)
[PROOFSTEP]
linarith
[GOAL]
R : Type u_1
S✝ : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : CommRing S✝
inst✝² : Algebra R S✝
I✝ : Ideal S✝
P : ⦃S : Type u_2⦄ → [inst : CommRing S] → Ideal S → Prop
h₁ : ∀ ⦃S : Type u_2⦄ [inst : CommRing S] (I : Ideal S), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_2⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
n✝ : ℕ
hI✝ : I✝ ^ n✝ = ⊥
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal S
hI' : ¬I = ⊥
n : ℕ
H :
  ∀ (m : ℕ),
    m < Nat.succ (Nat.succ n) →
      ∀ {S : Type u_2} [inst : CommRing S] [inst_1 : Algebra R S] (I : Ideal S), I ^ m = ⊥ → P I
hI : I ^ Nat.succ (Nat.succ n) = ⊥
⊢ Nat.succ n < Nat.succ (Nat.succ n)
[PROOFSTEP]
exact n.succ.lt_succ_self
[GOAL]
case neg.succ.succ.a
R : Type u_1
S✝ : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : CommRing S✝
inst✝² : Algebra R S✝
I✝ : Ideal S✝
P : ⦃S : Type u_2⦄ → [inst : CommRing S] → Ideal S → Prop
h₁ : ∀ ⦃S : Type u_2⦄ [inst : CommRing S] (I : Ideal S), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_2⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
n✝ : ℕ
hI✝ : I✝ ^ n✝ = ⊥
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal S
hI' : ¬I = ⊥
n : ℕ
H :
  ∀ (m : ℕ),
    m < Nat.succ (Nat.succ n) →
      ∀ {S : Type u_2} [inst : CommRing S] [inst_1 : Algebra R S] (I : Ideal S), I ^ m = ⊥ → P I
hI : I ^ Nat.succ (Nat.succ n) = ⊥
⊢ P (map (Quotient.mk (I ^ 2)) I)
[PROOFSTEP]
apply h₁
[GOAL]
case neg.succ.succ.a.a
R : Type u_1
S✝ : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : CommRing S✝
inst✝² : Algebra R S✝
I✝ : Ideal S✝
P : ⦃S : Type u_2⦄ → [inst : CommRing S] → Ideal S → Prop
h₁ : ∀ ⦃S : Type u_2⦄ [inst : CommRing S] (I : Ideal S), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_2⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
n✝ : ℕ
hI✝ : I✝ ^ n✝ = ⊥
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal S
hI' : ¬I = ⊥
n : ℕ
H :
  ∀ (m : ℕ),
    m < Nat.succ (Nat.succ n) →
      ∀ {S : Type u_2} [inst : CommRing S] [inst_1 : Algebra R S] (I : Ideal S), I ^ m = ⊥ → P I
hI : I ^ Nat.succ (Nat.succ n) = ⊥
⊢ map (Quotient.mk (I ^ 2)) I ^ 2 = ⊥
[PROOFSTEP]
rw [← Ideal.map_pow, Ideal.map_quotient_self]
[GOAL]
R✝ : Type u_1
S : Type u_2
inst✝³ : CommSemiring R✝
inst✝² : CommRing S
inst✝¹ : Algebra R✝ S
I✝ : Ideal S
R : Type u_3
inst✝ : CommRing R
I : Ideal R
hI : IsNilpotent I
x : R
⊢ IsUnit (↑(Ideal.Quotient.mk I) x) ↔ IsUnit x
[PROOFSTEP]
refine' ⟨_, fun h => h.map <| Ideal.Quotient.mk I⟩
[GOAL]
R✝ : Type u_1
S : Type u_2
inst✝³ : CommSemiring R✝
inst✝² : CommRing S
inst✝¹ : Algebra R✝ S
I✝ : Ideal S
R : Type u_3
inst✝ : CommRing R
I : Ideal R
hI : IsNilpotent I
x : R
⊢ IsUnit (↑(Ideal.Quotient.mk I) x) → IsUnit x
[PROOFSTEP]
revert x
[GOAL]
R✝ : Type u_1
S : Type u_2
inst✝³ : CommSemiring R✝
inst✝² : CommRing S
inst✝¹ : Algebra R✝ S
I✝ : Ideal S
R : Type u_3
inst✝ : CommRing R
I : Ideal R
hI : IsNilpotent I
⊢ ∀ {x : R}, IsUnit (↑(Ideal.Quotient.mk I) x) → IsUnit x
[PROOFSTEP]
apply Ideal.IsNilpotent.induction_on (R := R) (S := R) I hI
[GOAL]
case h₁
R✝ : Type u_1
S : Type u_2
inst✝³ : CommSemiring R✝
inst✝² : CommRing S
inst✝¹ : Algebra R✝ S
I✝ : Ideal S
R : Type u_3
inst✝ : CommRing R
I : Ideal R
hI : IsNilpotent I
⊢ ∀ ⦃S : Type u_3⦄ [inst : CommRing S] (I : Ideal S),
    I ^ 2 = ⊥ → ∀ {x : S}, IsUnit (↑(Ideal.Quotient.mk I) x) → IsUnit x
[PROOFSTEP]
clear hI I
[GOAL]
case h₂
R✝ : Type u_1
S : Type u_2
inst✝³ : CommSemiring R✝
inst✝² : CommRing S
inst✝¹ : Algebra R✝ S
I✝ : Ideal S
R : Type u_3
inst✝ : CommRing R
I : Ideal R
hI : IsNilpotent I
⊢ ∀ ⦃S : Type u_3⦄ [inst : CommRing S] (I J : Ideal S),
    I ≤ J →
      (∀ {x : S}, IsUnit (↑(Ideal.Quotient.mk I) x) → IsUnit x) →
        (∀ {x : S ⧸ I}, IsUnit (↑(Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk I) J)) x) → IsUnit x) →
          ∀ {x : S}, IsUnit (↑(Ideal.Quotient.mk J) x) → IsUnit x
[PROOFSTEP]
clear hI I
[GOAL]
case h₁
R✝ : Type u_1
S : Type u_2
inst✝³ : CommSemiring R✝
inst✝² : CommRing S
inst✝¹ : Algebra R✝ S
I : Ideal S
R : Type u_3
inst✝ : CommRing R
⊢ ∀ ⦃S : Type u_3⦄ [inst : CommRing S] (I : Ideal S),
    I ^ 2 = ⊥ → ∀ {x : S}, IsUnit (↑(Ideal.Quotient.mk I) x) → IsUnit x
case h₂
R✝ : Type u_1
S : Type u_2
inst✝³ : CommSemiring R✝
inst✝² : CommRing S
inst✝¹ : Algebra R✝ S
I : Ideal S
R : Type u_3
inst✝ : CommRing R
⊢ ∀ ⦃S : Type u_3⦄ [inst : CommRing S] (I J : Ideal S),
    I ≤ J →
      (∀ {x : S}, IsUnit (↑(Ideal.Quotient.mk I) x) → IsUnit x) →
        (∀ {x : S ⧸ I}, IsUnit (↑(Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk I) J)) x) → IsUnit x) →
          ∀ {x : S}, IsUnit (↑(Ideal.Quotient.mk J) x) → IsUnit x
[PROOFSTEP]
swap
[GOAL]
case h₂
R✝ : Type u_1
S : Type u_2
inst✝³ : CommSemiring R✝
inst✝² : CommRing S
inst✝¹ : Algebra R✝ S
I : Ideal S
R : Type u_3
inst✝ : CommRing R
⊢ ∀ ⦃S : Type u_3⦄ [inst : CommRing S] (I J : Ideal S),
    I ≤ J →
      (∀ {x : S}, IsUnit (↑(Ideal.Quotient.mk I) x) → IsUnit x) →
        (∀ {x : S ⧸ I}, IsUnit (↑(Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk I) J)) x) → IsUnit x) →
          ∀ {x : S}, IsUnit (↑(Ideal.Quotient.mk J) x) → IsUnit x
[PROOFSTEP]
introv e h₁ h₂ h₃
[GOAL]
case h₂
R✝ : Type u_1
S✝ : Type u_2
inst✝⁴ : CommSemiring R✝
inst✝³ : CommRing S✝
inst✝² : Algebra R✝ S✝
I✝ : Ideal S✝
R : Type u_3
inst✝¹ : CommRing R
S : Type u_3
inst✝ : CommRing S
I J : Ideal S
e : I ≤ J
h₁ : ∀ {x : S}, IsUnit (↑(Ideal.Quotient.mk I) x) → IsUnit x
h₂ : ∀ {x : S ⧸ I}, IsUnit (↑(Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk I) J)) x) → IsUnit x
x : S
h₃ : IsUnit (↑(Ideal.Quotient.mk J) x)
⊢ IsUnit x
[PROOFSTEP]
apply h₁
[GOAL]
case h₂.a
R✝ : Type u_1
S✝ : Type u_2
inst✝⁴ : CommSemiring R✝
inst✝³ : CommRing S✝
inst✝² : Algebra R✝ S✝
I✝ : Ideal S✝
R : Type u_3
inst✝¹ : CommRing R
S : Type u_3
inst✝ : CommRing S
I J : Ideal S
e : I ≤ J
h₁ : ∀ {x : S}, IsUnit (↑(Ideal.Quotient.mk I) x) → IsUnit x
h₂ : ∀ {x : S ⧸ I}, IsUnit (↑(Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk I) J)) x) → IsUnit x
x : S
h₃ : IsUnit (↑(Ideal.Quotient.mk J) x)
⊢ IsUnit (↑(Ideal.Quotient.mk I) x)
[PROOFSTEP]
apply h₂
[GOAL]
case h₂.a.a
R✝ : Type u_1
S✝ : Type u_2
inst✝⁴ : CommSemiring R✝
inst✝³ : CommRing S✝
inst✝² : Algebra R✝ S✝
I✝ : Ideal S✝
R : Type u_3
inst✝¹ : CommRing R
S : Type u_3
inst✝ : CommRing S
I J : Ideal S
e : I ≤ J
h₁ : ∀ {x : S}, IsUnit (↑(Ideal.Quotient.mk I) x) → IsUnit x
h₂ : ∀ {x : S ⧸ I}, IsUnit (↑(Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk I) J)) x) → IsUnit x
x : S
h₃ : IsUnit (↑(Ideal.Quotient.mk J) x)
⊢ IsUnit (↑(Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk I) J)) (↑(Ideal.Quotient.mk I) x))
[PROOFSTEP]
exact h₃.map ((DoubleQuot.quotQuotEquivQuotSup I J).trans (Ideal.quotEquivOfEq (sup_eq_right.mpr e))).symm.toRingHom
[GOAL]
case h₁
R✝ : Type u_1
S : Type u_2
inst✝³ : CommSemiring R✝
inst✝² : CommRing S
inst✝¹ : Algebra R✝ S
I : Ideal S
R : Type u_3
inst✝ : CommRing R
⊢ ∀ ⦃S : Type u_3⦄ [inst : CommRing S] (I : Ideal S),
    I ^ 2 = ⊥ → ∀ {x : S}, IsUnit (↑(Ideal.Quotient.mk I) x) → IsUnit x
[PROOFSTEP]
introv e H
[GOAL]
case h₁
R✝ : Type u_1
S✝ : Type u_2
inst✝⁴ : CommSemiring R✝
inst✝³ : CommRing S✝
inst✝² : Algebra R✝ S✝
I✝ : Ideal S✝
R : Type u_3
inst✝¹ : CommRing R
S : Type u_3
inst✝ : CommRing S
I : Ideal S
e : I ^ 2 = ⊥
x : S
H : IsUnit (↑(Ideal.Quotient.mk I) x)
⊢ IsUnit x
[PROOFSTEP]
skip
[GOAL]
case h₁
R✝ : Type u_1
S✝ : Type u_2
inst✝⁴ : CommSemiring R✝
inst✝³ : CommRing S✝
inst✝² : Algebra R✝ S✝
I✝ : Ideal S✝
R : Type u_3
inst✝¹ : CommRing R
S : Type u_3
inst✝ : CommRing S
I : Ideal S
e : I ^ 2 = ⊥
x : S
H : IsUnit (↑(Ideal.Quotient.mk I) x)
⊢ IsUnit x
[PROOFSTEP]
obtain ⟨y, hy⟩ := Ideal.Quotient.mk_surjective (↑H.unit⁻¹ : S ⧸ I)
[GOAL]
case h₁.intro
R✝ : Type u_1
S✝ : Type u_2
inst✝⁴ : CommSemiring R✝
inst✝³ : CommRing S✝
inst✝² : Algebra R✝ S✝
I✝ : Ideal S✝
R : Type u_3
inst✝¹ : CommRing R
S : Type u_3
inst✝ : CommRing S
I : Ideal S
e : I ^ 2 = ⊥
x : S
H : IsUnit (↑(Ideal.Quotient.mk I) x)
y : S
hy : ↑(Ideal.Quotient.mk I) y = ↑(IsUnit.unit H)⁻¹
⊢ IsUnit x
[PROOFSTEP]
have : Ideal.Quotient.mk I (x * y) = Ideal.Quotient.mk I 1 := by rw [map_one, _root_.map_mul, hy, IsUnit.mul_val_inv]
[GOAL]
R✝ : Type u_1
S✝ : Type u_2
inst✝⁴ : CommSemiring R✝
inst✝³ : CommRing S✝
inst✝² : Algebra R✝ S✝
I✝ : Ideal S✝
R : Type u_3
inst✝¹ : CommRing R
S : Type u_3
inst✝ : CommRing S
I : Ideal S
e : I ^ 2 = ⊥
x : S
H : IsUnit (↑(Ideal.Quotient.mk I) x)
y : S
hy : ↑(Ideal.Quotient.mk I) y = ↑(IsUnit.unit H)⁻¹
⊢ ↑(Ideal.Quotient.mk I) (x * y) = ↑(Ideal.Quotient.mk I) 1
[PROOFSTEP]
rw [map_one, _root_.map_mul, hy, IsUnit.mul_val_inv]
[GOAL]
case h₁.intro
R✝ : Type u_1
S✝ : Type u_2
inst✝⁴ : CommSemiring R✝
inst✝³ : CommRing S✝
inst✝² : Algebra R✝ S✝
I✝ : Ideal S✝
R : Type u_3
inst✝¹ : CommRing R
S : Type u_3
inst✝ : CommRing S
I : Ideal S
e : I ^ 2 = ⊥
x : S
H : IsUnit (↑(Ideal.Quotient.mk I) x)
y : S
hy : ↑(Ideal.Quotient.mk I) y = ↑(IsUnit.unit H)⁻¹
this : ↑(Ideal.Quotient.mk I) (x * y) = ↑(Ideal.Quotient.mk I) 1
⊢ IsUnit x
[PROOFSTEP]
rw [Ideal.Quotient.eq] at this
[GOAL]
case h₁.intro
R✝ : Type u_1
S✝ : Type u_2
inst✝⁴ : CommSemiring R✝
inst✝³ : CommRing S✝
inst✝² : Algebra R✝ S✝
I✝ : Ideal S✝
R : Type u_3
inst✝¹ : CommRing R
S : Type u_3
inst✝ : CommRing S
I : Ideal S
e : I ^ 2 = ⊥
x : S
H : IsUnit (↑(Ideal.Quotient.mk I) x)
y : S
hy : ↑(Ideal.Quotient.mk I) y = ↑(IsUnit.unit H)⁻¹
this : x * y - 1 ∈ I
⊢ IsUnit x
[PROOFSTEP]
have : (x * y - 1) ^ 2 = 0 := by
  rw [← Ideal.mem_bot, ← e]
  exact Ideal.pow_mem_pow this _
[GOAL]
R✝ : Type u_1
S✝ : Type u_2
inst✝⁴ : CommSemiring R✝
inst✝³ : CommRing S✝
inst✝² : Algebra R✝ S✝
I✝ : Ideal S✝
R : Type u_3
inst✝¹ : CommRing R
S : Type u_3
inst✝ : CommRing S
I : Ideal S
e : I ^ 2 = ⊥
x : S
H : IsUnit (↑(Ideal.Quotient.mk I) x)
y : S
hy : ↑(Ideal.Quotient.mk I) y = ↑(IsUnit.unit H)⁻¹
this : x * y - 1 ∈ I
⊢ (x * y - 1) ^ 2 = 0
[PROOFSTEP]
rw [← Ideal.mem_bot, ← e]
[GOAL]
R✝ : Type u_1
S✝ : Type u_2
inst✝⁴ : CommSemiring R✝
inst✝³ : CommRing S✝
inst✝² : Algebra R✝ S✝
I✝ : Ideal S✝
R : Type u_3
inst✝¹ : CommRing R
S : Type u_3
inst✝ : CommRing S
I : Ideal S
e : I ^ 2 = ⊥
x : S
H : IsUnit (↑(Ideal.Quotient.mk I) x)
y : S
hy : ↑(Ideal.Quotient.mk I) y = ↑(IsUnit.unit H)⁻¹
this : x * y - 1 ∈ I
⊢ (x * y - 1) ^ 2 ∈ I ^ 2
[PROOFSTEP]
exact Ideal.pow_mem_pow this _
[GOAL]
case h₁.intro
R✝ : Type u_1
S✝ : Type u_2
inst✝⁴ : CommSemiring R✝
inst✝³ : CommRing S✝
inst✝² : Algebra R✝ S✝
I✝ : Ideal S✝
R : Type u_3
inst✝¹ : CommRing R
S : Type u_3
inst✝ : CommRing S
I : Ideal S
e : I ^ 2 = ⊥
x : S
H : IsUnit (↑(Ideal.Quotient.mk I) x)
y : S
hy : ↑(Ideal.Quotient.mk I) y = ↑(IsUnit.unit H)⁻¹
this✝ : x * y - 1 ∈ I
this : (x * y - 1) ^ 2 = 0
⊢ IsUnit x
[PROOFSTEP]
have : x * (y * (2 - x * y)) = 1 := by
  rw [eq_comm, ← sub_eq_zero, ← this]
  ring
[GOAL]
R✝ : Type u_1
S✝ : Type u_2
inst✝⁴ : CommSemiring R✝
inst✝³ : CommRing S✝
inst✝² : Algebra R✝ S✝
I✝ : Ideal S✝
R : Type u_3
inst✝¹ : CommRing R
S : Type u_3
inst✝ : CommRing S
I : Ideal S
e : I ^ 2 = ⊥
x : S
H : IsUnit (↑(Ideal.Quotient.mk I) x)
y : S
hy : ↑(Ideal.Quotient.mk I) y = ↑(IsUnit.unit H)⁻¹
this✝ : x * y - 1 ∈ I
this : (x * y - 1) ^ 2 = 0
⊢ x * (y * (2 - x * y)) = 1
[PROOFSTEP]
rw [eq_comm, ← sub_eq_zero, ← this]
[GOAL]
R✝ : Type u_1
S✝ : Type u_2
inst✝⁴ : CommSemiring R✝
inst✝³ : CommRing S✝
inst✝² : Algebra R✝ S✝
I✝ : Ideal S✝
R : Type u_3
inst✝¹ : CommRing R
S : Type u_3
inst✝ : CommRing S
I : Ideal S
e : I ^ 2 = ⊥
x : S
H : IsUnit (↑(Ideal.Quotient.mk I) x)
y : S
hy : ↑(Ideal.Quotient.mk I) y = ↑(IsUnit.unit H)⁻¹
this✝ : x * y - 1 ∈ I
this : (x * y - 1) ^ 2 = 0
⊢ 1 - x * (y * (2 - x * y)) = (x * y - 1) ^ 2
[PROOFSTEP]
ring
[GOAL]
case h₁.intro
R✝ : Type u_1
S✝ : Type u_2
inst✝⁴ : CommSemiring R✝
inst✝³ : CommRing S✝
inst✝² : Algebra R✝ S✝
I✝ : Ideal S✝
R : Type u_3
inst✝¹ : CommRing R
S : Type u_3
inst✝ : CommRing S
I : Ideal S
e : I ^ 2 = ⊥
x : S
H : IsUnit (↑(Ideal.Quotient.mk I) x)
y : S
hy : ↑(Ideal.Quotient.mk I) y = ↑(IsUnit.unit H)⁻¹
this✝¹ : x * y - 1 ∈ I
this✝ : (x * y - 1) ^ 2 = 0
this : x * (y * (2 - x * y)) = 1
⊢ IsUnit x
[PROOFSTEP]
exact isUnit_of_mul_eq_one _ _ this


[GOAL]
𝕜 : Type u_1
inst✝¹⁶ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝¹⁵ : TopologicalSpace H
E : Type u_3
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G✝ : Type u_4
inst✝¹² : Mul G✝
inst✝¹¹ : TopologicalSpace G✝
inst✝¹⁰ : ChartedSpace H G✝
inst✝⁹ : SmoothMul I G✝
E' : Type u_5
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁶ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_7
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H' M
g✝ h✝ : G✝
G : Type u_8
inst✝³ : Semigroup G
inst✝² : TopologicalSpace G
inst✝¹ : ChartedSpace H G
inst✝ : SmoothMul I G
g h : G
⊢ 𝑳 I (g * h) = ContMDiffMap.comp (𝑳 I g) (𝑳 I h)
[PROOFSTEP]
ext
[GOAL]
case h
𝕜 : Type u_1
inst✝¹⁶ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝¹⁵ : TopologicalSpace H
E : Type u_3
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G✝ : Type u_4
inst✝¹² : Mul G✝
inst✝¹¹ : TopologicalSpace G✝
inst✝¹⁰ : ChartedSpace H G✝
inst✝⁹ : SmoothMul I G✝
E' : Type u_5
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁶ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_7
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H' M
g✝ h✝ : G✝
G : Type u_8
inst✝³ : Semigroup G
inst✝² : TopologicalSpace G
inst✝¹ : ChartedSpace H G
inst✝ : SmoothMul I G
g h x✝ : G
⊢ ↑(𝑳 I (g * h)) x✝ = ↑(ContMDiffMap.comp (𝑳 I g) (𝑳 I h)) x✝
[PROOFSTEP]
simp only [ContMDiffMap.comp_apply, L_apply, mul_assoc]
[GOAL]
𝕜 : Type u_1
inst✝¹⁶ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝¹⁵ : TopologicalSpace H
E : Type u_3
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G✝ : Type u_4
inst✝¹² : Mul G✝
inst✝¹¹ : TopologicalSpace G✝
inst✝¹⁰ : ChartedSpace H G✝
inst✝⁹ : SmoothMul I G✝
E' : Type u_5
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁶ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_7
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H' M
g✝ h✝ : G✝
G : Type u_8
inst✝³ : Semigroup G
inst✝² : TopologicalSpace G
inst✝¹ : ChartedSpace H G
inst✝ : SmoothMul I G
g h : G
⊢ 𝑹 I (g * h) = ContMDiffMap.comp (𝑹 I h) (𝑹 I g)
[PROOFSTEP]
ext
[GOAL]
case h
𝕜 : Type u_1
inst✝¹⁶ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝¹⁵ : TopologicalSpace H
E : Type u_3
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G✝ : Type u_4
inst✝¹² : Mul G✝
inst✝¹¹ : TopologicalSpace G✝
inst✝¹⁰ : ChartedSpace H G✝
inst✝⁹ : SmoothMul I G✝
E' : Type u_5
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁶ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_7
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H' M
g✝ h✝ : G✝
G : Type u_8
inst✝³ : Semigroup G
inst✝² : TopologicalSpace G
inst✝¹ : ChartedSpace H G
inst✝ : SmoothMul I G
g h x✝ : G
⊢ ↑(𝑹 I (g * h)) x✝ = ↑(ContMDiffMap.comp (𝑹 I h) (𝑹 I g)) x✝
[PROOFSTEP]
simp only [ContMDiffMap.comp_apply, R_apply, mul_assoc]
[GOAL]
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝¹³ : TopologicalSpace H
E : Type u_3
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝¹⁰ : Monoid G
inst✝⁹ : TopologicalSpace G
inst✝⁸ : ChartedSpace H G
inst✝⁷ : SmoothMul I G
H' : Type u_5
inst✝⁶ : TopologicalSpace H'
E' : Type u_6
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
G' : Type u_7
inst✝³ : Monoid G'
inst✝² : TopologicalSpace G'
inst✝¹ : ChartedSpace H' G'
inst✝ : SmoothMul I' G'
⊢ Smooth I I fun a => a ^ 0
[PROOFSTEP]
simp only [pow_zero]
[GOAL]
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝¹³ : TopologicalSpace H
E : Type u_3
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝¹⁰ : Monoid G
inst✝⁹ : TopologicalSpace G
inst✝⁸ : ChartedSpace H G
inst✝⁷ : SmoothMul I G
H' : Type u_5
inst✝⁶ : TopologicalSpace H'
E' : Type u_6
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
G' : Type u_7
inst✝³ : Monoid G'
inst✝² : TopologicalSpace G'
inst✝¹ : ChartedSpace H' G'
inst✝ : SmoothMul I' G'
⊢ Smooth I I fun a => 1
[PROOFSTEP]
exact smooth_const
[GOAL]
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝¹³ : TopologicalSpace H
E : Type u_3
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝¹⁰ : Monoid G
inst✝⁹ : TopologicalSpace G
inst✝⁸ : ChartedSpace H G
inst✝⁷ : SmoothMul I G
H' : Type u_5
inst✝⁶ : TopologicalSpace H'
E' : Type u_6
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
G' : Type u_7
inst✝³ : Monoid G'
inst✝² : TopologicalSpace G'
inst✝¹ : ChartedSpace H' G'
inst✝ : SmoothMul I' G'
k : ℕ
⊢ Smooth I I fun a => a ^ (k + 1)
[PROOFSTEP]
simpa [pow_succ] using smooth_id.mul (smooth_pow _)
[GOAL]
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝¹³ : TopologicalSpace H
E : Type u_3
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝¹⁰ : Monoid G
inst✝⁹ : TopologicalSpace G
inst✝⁸ : ChartedSpace H G
inst✝⁷ : SmoothMul I G
H' : Type u_5
inst✝⁶ : TopologicalSpace H'
E' : Type u_6
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
G' : Type u_7
inst✝³ : Monoid G'
inst✝² : TopologicalSpace G'
inst✝¹ : ChartedSpace H' G'
inst✝ : SmoothMul I' G'
f g : SmoothMonoidMorphism I I' G G'
h : (fun a => a.toFun) f = (fun a => a.toFun) g
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝¹³ : TopologicalSpace H
E : Type u_3
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝¹⁰ : Monoid G
inst✝⁹ : TopologicalSpace G
inst✝⁸ : ChartedSpace H G
inst✝⁷ : SmoothMul I G
H' : Type u_5
inst✝⁶ : TopologicalSpace H'
E' : Type u_6
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
G' : Type u_7
inst✝³ : Monoid G'
inst✝² : TopologicalSpace G'
inst✝¹ : ChartedSpace H' G'
inst✝ : SmoothMul I' G'
g : SmoothMonoidMorphism I I' G G'
toMonoidHom✝ : G →* G'
smooth_toFun✝ : Smooth I I' toMonoidHom✝.toFun
h : (fun a => a.toFun) { toMonoidHom := toMonoidHom✝, smooth_toFun := smooth_toFun✝ } = (fun a => a.toFun) g
⊢ { toMonoidHom := toMonoidHom✝, smooth_toFun := smooth_toFun✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝¹³ : TopologicalSpace H
E : Type u_3
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝¹⁰ : Monoid G
inst✝⁹ : TopologicalSpace G
inst✝⁸ : ChartedSpace H G
inst✝⁷ : SmoothMul I G
H' : Type u_5
inst✝⁶ : TopologicalSpace H'
E' : Type u_6
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
G' : Type u_7
inst✝³ : Monoid G'
inst✝² : TopologicalSpace G'
inst✝¹ : ChartedSpace H' G'
inst✝ : SmoothMul I' G'
toMonoidHom✝¹ : G →* G'
smooth_toFun✝¹ : Smooth I I' toMonoidHom✝¹.toFun
toMonoidHom✝ : G →* G'
smooth_toFun✝ : Smooth I I' toMonoidHom✝.toFun
h :
  (fun a => a.toFun) { toMonoidHom := toMonoidHom✝¹, smooth_toFun := smooth_toFun✝¹ } =
    (fun a => a.toFun) { toMonoidHom := toMonoidHom✝, smooth_toFun := smooth_toFun✝ }
⊢ { toMonoidHom := toMonoidHom✝¹, smooth_toFun := smooth_toFun✝¹ } =
    { toMonoidHom := toMonoidHom✝, smooth_toFun := smooth_toFun✝ }
[PROOFSTEP]
congr
[GOAL]
case mk.mk.e_toMonoidHom
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝¹³ : TopologicalSpace H
E : Type u_3
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝¹⁰ : Monoid G
inst✝⁹ : TopologicalSpace G
inst✝⁸ : ChartedSpace H G
inst✝⁷ : SmoothMul I G
H' : Type u_5
inst✝⁶ : TopologicalSpace H'
E' : Type u_6
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
G' : Type u_7
inst✝³ : Monoid G'
inst✝² : TopologicalSpace G'
inst✝¹ : ChartedSpace H' G'
inst✝ : SmoothMul I' G'
toMonoidHom✝¹ : G →* G'
smooth_toFun✝¹ : Smooth I I' toMonoidHom✝¹.toFun
toMonoidHom✝ : G →* G'
smooth_toFun✝ : Smooth I I' toMonoidHom✝.toFun
h :
  (fun a => a.toFun) { toMonoidHom := toMonoidHom✝¹, smooth_toFun := smooth_toFun✝¹ } =
    (fun a => a.toFun) { toMonoidHom := toMonoidHom✝, smooth_toFun := smooth_toFun✝ }
⊢ toMonoidHom✝¹ = toMonoidHom✝
[PROOFSTEP]
exact FunLike.ext' h
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝¹² : NontriviallyNormedField 𝕜
H : Type u_3
inst✝¹¹ : TopologicalSpace H
E : Type u_4
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_5
inst✝⁸ : CommMonoid G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : ChartedSpace H G
inst✝⁵ : SmoothMul I G
E' : Type u_6
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_7
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_8
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H' M
s : Set M
x : M
t : Finset ι
f : ι → M → G
n : ℕ∞
p : ι → Prop
h : ∀ (i : ι), i ∈ t → ContMDiffWithinAt I' I n (f i) s x
⊢ ContMDiffWithinAt I' I n (fun x => ∏ i in t, f i x) s x
[PROOFSTEP]
simp only [← Finset.prod_apply]
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝¹² : NontriviallyNormedField 𝕜
H : Type u_3
inst✝¹¹ : TopologicalSpace H
E : Type u_4
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_5
inst✝⁸ : CommMonoid G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : ChartedSpace H G
inst✝⁵ : SmoothMul I G
E' : Type u_6
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_7
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_8
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H' M
s : Set M
x : M
t : Finset ι
f : ι → M → G
n : ℕ∞
p : ι → Prop
h : ∀ (i : ι), i ∈ t → ContMDiffWithinAt I' I n (f i) s x
⊢ ContMDiffWithinAt I' I n (fun x => Finset.prod t (fun c => f c) x) s x
[PROOFSTEP]
exact contMDiffWithinAt_finset_prod' h
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝¹² : NontriviallyNormedField 𝕜
H : Type u_3
inst✝¹¹ : TopologicalSpace H
E : Type u_4
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_5
inst✝⁸ : CommMonoid G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : ChartedSpace H G
inst✝⁵ : SmoothMul I G
E' : Type u_6
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_7
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_8
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H' M
s : Set M
x : M
t : Finset ι
f : ι → M → G
n : ℕ∞
p : ι → Prop
h : ∀ (i : ι), ContMDiff I' I n (f i)
hfin : LocallyFinite fun i => mulSupport (f i)
⊢ ContMDiff I' I n fun x => ∏ᶠ (i : ι), f i x
[PROOFSTEP]
intro x
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝¹² : NontriviallyNormedField 𝕜
H : Type u_3
inst✝¹¹ : TopologicalSpace H
E : Type u_4
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_5
inst✝⁸ : CommMonoid G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : ChartedSpace H G
inst✝⁵ : SmoothMul I G
E' : Type u_6
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_7
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_8
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H' M
s : Set M
x✝ : M
t : Finset ι
f : ι → M → G
n : ℕ∞
p : ι → Prop
h : ∀ (i : ι), ContMDiff I' I n (f i)
hfin : LocallyFinite fun i => mulSupport (f i)
x : M
⊢ ContMDiffAt I' I n (fun x => ∏ᶠ (i : ι), f i x) x
[PROOFSTEP]
rcases finprod_eventually_eq_prod hfin x with ⟨s, hs⟩
[GOAL]
case intro
ι : Type u_1
𝕜 : Type u_2
inst✝¹² : NontriviallyNormedField 𝕜
H : Type u_3
inst✝¹¹ : TopologicalSpace H
E : Type u_4
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_5
inst✝⁸ : CommMonoid G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : ChartedSpace H G
inst✝⁵ : SmoothMul I G
E' : Type u_6
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_7
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_8
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H' M
s✝ : Set M
x✝ : M
t : Finset ι
f : ι → M → G
n : ℕ∞
p : ι → Prop
h : ∀ (i : ι), ContMDiff I' I n (f i)
hfin : LocallyFinite fun i => mulSupport (f i)
x : M
s : Finset ι
hs : ∀ᶠ (y : M) in nhds x, ∏ᶠ (i : ι), f i y = ∏ i in s, f i y
⊢ ContMDiffAt I' I n (fun x => ∏ᶠ (i : ι), f i x) x
[PROOFSTEP]
exact (contMDiff_finset_prod (fun i _ => h i) x).congr_of_eventuallyEq hs
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝¹² : NontriviallyNormedField 𝕜
H : Type u_3
inst✝¹¹ : TopologicalSpace H
E : Type u_4
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_5
inst✝⁸ : CommMonoid G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : ChartedSpace H G
inst✝⁵ : SmoothMul I G
E' : Type u_6
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_7
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_8
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H' M
s : Set M
x : M
t : Finset ι
f : ι → M → G
n : ℕ∞
p : ι → Prop
hc : ∀ (i : ι), p i → ContMDiff I' I n (f i)
hf : LocallyFinite fun i => mulSupport (f i)
⊢ ContMDiff I' I n fun x => ∏ᶠ (i : ι) (_ : p i), f i x
[PROOFSTEP]
simp only [← finprod_subtype_eq_finprod_cond]
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝¹² : NontriviallyNormedField 𝕜
H : Type u_3
inst✝¹¹ : TopologicalSpace H
E : Type u_4
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_5
inst✝⁸ : CommMonoid G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : ChartedSpace H G
inst✝⁵ : SmoothMul I G
E' : Type u_6
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_7
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_8
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H' M
s : Set M
x : M
t : Finset ι
f : ι → M → G
n : ℕ∞
p : ι → Prop
hc : ∀ (i : ι), p i → ContMDiff I' I n (f i)
hf : LocallyFinite fun i => mulSupport (f i)
⊢ ContMDiff I' I n fun x => ∏ᶠ (j : { i // p i }), f (↑j) x
[PROOFSTEP]
exact contMDiff_finprod (fun i => hc i i.2) (hf.comp_injective Subtype.coe_injective)
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
⊢ Smooth (ModelWithCorners.prod 𝓘(𝕜, E) 𝓘(𝕜, E)) 𝓘(𝕜, E) fun p => p.fst + p.snd
[PROOFSTEP]
rw [← modelWithCornersSelf_prod]
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
⊢ Smooth 𝓘(𝕜, E × E) 𝓘(𝕜, E) fun p => p.fst + p.snd
[PROOFSTEP]
exact contDiff_add.contMDiff
[GOAL]
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
H : Type u_2
inst✝¹¹ : TopologicalSpace H
E : Type u_3
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁸ : DivInvMonoid G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : ChartedSpace H G
inst✝⁵ : SmoothMul I G
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_7
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H' M
f : M → G
s : Set M
x : M
n : ℕ∞
c : G
hf : ContMDiffWithinAt I' I n f s x
⊢ ContMDiffWithinAt I' I n (fun x => f x / c) s x
[PROOFSTEP]
simpa only [div_eq_mul_inv] using hf.mul contMDiffWithinAt_const