[GOAL]
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x y : L
hx : x ∈ 0.carrier
_hy : y ∈ 0.carrier
⊢ ⁅x, y⁆ ∈ 0.carrier
[PROOFSTEP]
rw [(Submodule.mem_bot R).1 hx, zero_lie]
[GOAL]
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x y : L
hx : x ∈ 0.carrier
_hy : y ∈ 0.carrier
⊢ 0 ∈ 0.carrier
[PROOFSTEP]
exact Submodule.zero_mem 0
[GOAL]
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
L' L'' : LieSubalgebra R L
h : (fun L' => L'.carrier) L' = (fun L' => L'.carrier) L''
⊢ L' = L''
[PROOFSTEP]
rcases L' with ⟨⟨⟩⟩
[GOAL]
case mk.mk
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
L'' : LieSubalgebra R L
toAddSubmonoid✝ : AddSubmonoid L
smul_mem'✝ : ∀ (c : R) {x : L}, x ∈ toAddSubmonoid✝.carrier → c • x ∈ toAddSubmonoid✝.carrier
lie_mem'✝ :
  ∀ {x y : L},
    x ∈ { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }.toAddSubmonoid.toAddSubsemigroup.carrier →
      y ∈ { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }.toAddSubmonoid.toAddSubsemigroup.carrier →
        ⁅x, y⁆ ∈ { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }.toAddSubmonoid.toAddSubsemigroup.carrier
h :
  (fun L' => L'.carrier)
      { toSubmodule := { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }, lie_mem' := lie_mem'✝ } =
    (fun L' => L'.carrier) L''
⊢ { toSubmodule := { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }, lie_mem' := lie_mem'✝ } = L''
[PROOFSTEP]
rcases L'' with ⟨⟨⟩⟩
[GOAL]
case mk.mk.mk.mk
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
toAddSubmonoid✝¹ : AddSubmonoid L
smul_mem'✝¹ : ∀ (c : R) {x : L}, x ∈ toAddSubmonoid✝¹.carrier → c • x ∈ toAddSubmonoid✝¹.carrier
lie_mem'✝¹ :
  ∀ {x y : L},
    x ∈ { toAddSubmonoid := toAddSubmonoid✝¹, smul_mem' := smul_mem'✝¹ }.toAddSubmonoid.toAddSubsemigroup.carrier →
      y ∈ { toAddSubmonoid := toAddSubmonoid✝¹, smul_mem' := smul_mem'✝¹ }.toAddSubmonoid.toAddSubsemigroup.carrier →
        ⁅x, y⁆ ∈
          { toAddSubmonoid := toAddSubmonoid✝¹, smul_mem' := smul_mem'✝¹ }.toAddSubmonoid.toAddSubsemigroup.carrier
toAddSubmonoid✝ : AddSubmonoid L
smul_mem'✝ : ∀ (c : R) {x : L}, x ∈ toAddSubmonoid✝.carrier → c • x ∈ toAddSubmonoid✝.carrier
lie_mem'✝ :
  ∀ {x y : L},
    x ∈ { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }.toAddSubmonoid.toAddSubsemigroup.carrier →
      y ∈ { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }.toAddSubmonoid.toAddSubsemigroup.carrier →
        ⁅x, y⁆ ∈ { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }.toAddSubmonoid.toAddSubsemigroup.carrier
h :
  (fun L' => L'.carrier)
      { toSubmodule := { toAddSubmonoid := toAddSubmonoid✝¹, smul_mem' := smul_mem'✝¹ }, lie_mem' := lie_mem'✝¹ } =
    (fun L' => L'.carrier)
      { toSubmodule := { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }, lie_mem' := lie_mem'✝ }
⊢ { toSubmodule := { toAddSubmonoid := toAddSubmonoid✝¹, smul_mem' := smul_mem'✝¹ }, lie_mem' := lie_mem'✝¹ } =
    { toSubmodule := { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }, lie_mem' := lie_mem'✝ }
[PROOFSTEP]
congr
[GOAL]
case mk.mk.mk.mk.e_toSubmodule.e_toAddSubmonoid
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
toAddSubmonoid✝¹ : AddSubmonoid L
smul_mem'✝¹ : ∀ (c : R) {x : L}, x ∈ toAddSubmonoid✝¹.carrier → c • x ∈ toAddSubmonoid✝¹.carrier
lie_mem'✝¹ :
  ∀ {x y : L},
    x ∈ { toAddSubmonoid := toAddSubmonoid✝¹, smul_mem' := smul_mem'✝¹ }.toAddSubmonoid.toAddSubsemigroup.carrier →
      y ∈ { toAddSubmonoid := toAddSubmonoid✝¹, smul_mem' := smul_mem'✝¹ }.toAddSubmonoid.toAddSubsemigroup.carrier →
        ⁅x, y⁆ ∈
          { toAddSubmonoid := toAddSubmonoid✝¹, smul_mem' := smul_mem'✝¹ }.toAddSubmonoid.toAddSubsemigroup.carrier
toAddSubmonoid✝ : AddSubmonoid L
smul_mem'✝ : ∀ (c : R) {x : L}, x ∈ toAddSubmonoid✝.carrier → c • x ∈ toAddSubmonoid✝.carrier
lie_mem'✝ :
  ∀ {x y : L},
    x ∈ { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }.toAddSubmonoid.toAddSubsemigroup.carrier →
      y ∈ { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }.toAddSubmonoid.toAddSubsemigroup.carrier →
        ⁅x, y⁆ ∈ { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }.toAddSubmonoid.toAddSubsemigroup.carrier
h :
  (fun L' => L'.carrier)
      { toSubmodule := { toAddSubmonoid := toAddSubmonoid✝¹, smul_mem' := smul_mem'✝¹ }, lie_mem' := lie_mem'✝¹ } =
    (fun L' => L'.carrier)
      { toSubmodule := { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }, lie_mem' := lie_mem'✝ }
⊢ toAddSubmonoid✝¹ = toAddSubmonoid✝
[PROOFSTEP]
exact SetLike.coe_injective' h
[GOAL]
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
L' : LieSubalgebra R L
⊢ ∀ (x y z : { x // x ∈ L' }), ⁅x + y, z⁆ = ⁅x, z⁆ + ⁅y, z⁆
[PROOFSTEP]
intros
[GOAL]
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
L' : LieSubalgebra R L
x✝ y✝ z✝ : { x // x ∈ L' }
⊢ ⁅x✝ + y✝, z✝⁆ = ⁅x✝, z✝⁆ + ⁅y✝, z✝⁆
[PROOFSTEP]
apply SetCoe.ext
[GOAL]
case a
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
L' : LieSubalgebra R L
x✝ y✝ z✝ : { x // x ∈ L' }
⊢ ↑⁅x✝ + y✝, z✝⁆ = ↑(⁅x✝, z✝⁆ + ⁅y✝, z✝⁆)
[PROOFSTEP]
apply add_lie
[GOAL]
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
L' : LieSubalgebra R L
⊢ ∀ (x y z : { x // x ∈ L' }), ⁅x, y + z⁆ = ⁅x, y⁆ + ⁅x, z⁆
[PROOFSTEP]
intros
[GOAL]
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
L' : LieSubalgebra R L
x✝ y✝ z✝ : { x // x ∈ L' }
⊢ ⁅x✝, y✝ + z✝⁆ = ⁅x✝, y✝⁆ + ⁅x✝, z✝⁆
[PROOFSTEP]
apply SetCoe.ext
[GOAL]
case a
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
L' : LieSubalgebra R L
x✝ y✝ z✝ : { x // x ∈ L' }
⊢ ↑⁅x✝, y✝ + z✝⁆ = ↑(⁅x✝, y✝⁆ + ⁅x✝, z✝⁆)
[PROOFSTEP]
apply lie_add
[GOAL]
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
L' : LieSubalgebra R L
⊢ ∀ (x : { x // x ∈ L' }), ⁅x, x⁆ = 0
[PROOFSTEP]
intros
[GOAL]
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
L' : LieSubalgebra R L
x✝ : { x // x ∈ L' }
⊢ ⁅x✝, x✝⁆ = 0
[PROOFSTEP]
apply SetCoe.ext
[GOAL]
case a
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
L' : LieSubalgebra R L
x✝ : { x // x ∈ L' }
⊢ ↑⁅x✝, x✝⁆ = ↑0
[PROOFSTEP]
apply lie_self
[GOAL]
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
L' : LieSubalgebra R L
⊢ ∀ (x y z : { x // x ∈ L' }), ⁅x, ⁅y, z⁆⁆ = ⁅⁅x, y⁆, z⁆ + ⁅y, ⁅x, z⁆⁆
[PROOFSTEP]
intros
[GOAL]
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
L' : LieSubalgebra R L
x✝ y✝ z✝ : { x // x ∈ L' }
⊢ ⁅x✝, ⁅y✝, z✝⁆⁆ = ⁅⁅x✝, y✝⁆, z✝⁆ + ⁅y✝, ⁅x✝, z✝⁆⁆
[PROOFSTEP]
apply SetCoe.ext
[GOAL]
case a
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
L' : LieSubalgebra R L
x✝ y✝ z✝ : { x // x ∈ L' }
⊢ ↑⁅x✝, ⁅y✝, z✝⁆⁆ = ↑(⁅⁅x✝, y✝⁆, z✝⁆ + ⁅y✝, ⁅x✝, z✝⁆⁆)
[PROOFSTEP]
apply leibniz_lie
[GOAL]
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
L' : LieSubalgebra R L
⊢ ∀ (t : R) (x y : { x // x ∈ L' }), ⁅x, t • y⁆ = t • ⁅x, y⁆
[PROOFSTEP]
{ intros
  apply SetCoe.ext
  apply lie_smul
}
[GOAL]
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
L' : LieSubalgebra R L
⊢ ∀ (t : R) (x y : { x // x ∈ L' }), ⁅x, t • y⁆ = t • ⁅x, y⁆
[PROOFSTEP]
intros
[GOAL]
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
L' : LieSubalgebra R L
t✝ : R
x✝ y✝ : { x // x ∈ L' }
⊢ ⁅x✝, t✝ • y✝⁆ = t✝ • ⁅x✝, y✝⁆
[PROOFSTEP]
apply SetCoe.ext
[GOAL]
case a
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
L' : LieSubalgebra R L
t✝ : R
x✝ y✝ : { x // x ∈ L' }
⊢ ↑⁅x✝, t✝ • y✝⁆ = ↑(t✝ • ⁅x✝, y✝⁆)
[PROOFSTEP]
apply lie_smul
[GOAL]
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
L' : LieSubalgebra R L
p : Submodule R L
h :
  ∀ {x y : L},
    x ∈
        { toAddSubmonoid := p.toAddSubmonoid,
                smul_mem' :=
                  (_ :
                    ∀ (c : R) {x : L}, x ∈ p.carrier → c • x ∈ p.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier →
      y ∈
          { toAddSubmonoid := p.toAddSubmonoid,
                  smul_mem' :=
                    (_ :
                      ∀ (c : R) {x : L}, x ∈ p.carrier → c • x ∈ p.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier →
        ⁅x, y⁆ ∈
          { toAddSubmonoid := p.toAddSubmonoid,
                  smul_mem' :=
                    (_ :
                      ∀ (c : R) {x : L}, x ∈ p.carrier → c • x ∈ p.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
⊢ {
        toSubmodule :=
          { toAddSubmonoid := p.toAddSubmonoid,
            smul_mem' := (_ : ∀ (c : R) {x : L}, x ∈ p.carrier → c • x ∈ p.carrier) },
        lie_mem' := h }.toSubmodule =
    p
[PROOFSTEP]
cases p
[GOAL]
case mk
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
L' : LieSubalgebra R L
toAddSubmonoid✝ : AddSubmonoid L
smul_mem'✝ : ∀ (c : R) {x : L}, x ∈ toAddSubmonoid✝.carrier → c • x ∈ toAddSubmonoid✝.carrier
h :
  ∀ {x y : L},
    x ∈
        { toAddSubmonoid := { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }.toAddSubmonoid,
                smul_mem' :=
                  (_ :
                    ∀ (c : R) {x : L},
                      x ∈
                          { toAddSubmonoid := toAddSubmonoid✝,
                                  smul_mem' := smul_mem'✝ }.toAddSubmonoid.toAddSubsemigroup.carrier →
                        c • x ∈
                          { toAddSubmonoid := toAddSubmonoid✝,
                                  smul_mem' :=
                                    smul_mem'✝ }.toAddSubmonoid.toAddSubsemigroup.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier →
      y ∈
          { toAddSubmonoid := { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }.toAddSubmonoid,
                  smul_mem' :=
                    (_ :
                      ∀ (c : R) {x : L},
                        x ∈
                            { toAddSubmonoid := toAddSubmonoid✝,
                                    smul_mem' := smul_mem'✝ }.toAddSubmonoid.toAddSubsemigroup.carrier →
                          c • x ∈
                            { toAddSubmonoid := toAddSubmonoid✝,
                                    smul_mem' :=
                                      smul_mem'✝ }.toAddSubmonoid.toAddSubsemigroup.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier →
        ⁅x, y⁆ ∈
          { toAddSubmonoid := { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }.toAddSubmonoid,
                  smul_mem' :=
                    (_ :
                      ∀ (c : R) {x : L},
                        x ∈
                            { toAddSubmonoid := toAddSubmonoid✝,
                                    smul_mem' := smul_mem'✝ }.toAddSubmonoid.toAddSubsemigroup.carrier →
                          c • x ∈
                            { toAddSubmonoid := toAddSubmonoid✝,
                                    smul_mem' :=
                                      smul_mem'✝ }.toAddSubmonoid.toAddSubsemigroup.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
⊢ {
        toSubmodule :=
          { toAddSubmonoid := { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }.toAddSubmonoid,
            smul_mem' :=
              (_ :
                ∀ (c : R) {x : L},
                  x ∈
                      { toAddSubmonoid := toAddSubmonoid✝,
                              smul_mem' := smul_mem'✝ }.toAddSubmonoid.toAddSubsemigroup.carrier →
                    c • x ∈
                      { toAddSubmonoid := toAddSubmonoid✝,
                              smul_mem' := smul_mem'✝ }.toAddSubmonoid.toAddSubsemigroup.carrier) },
        lie_mem' := h }.toSubmodule =
    { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }
[PROOFSTEP]
rfl
[GOAL]
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
L' L₁' L₂' : LieSubalgebra R L
h : L₁'.toSubmodule = L₂'.toSubmodule
⊢ L₁' = L₂'
[PROOFSTEP]
rw [SetLike.ext'_iff] at h
[GOAL]
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
L' L₁' L₂' : LieSubalgebra R L
h✝ : L₁'.toSubmodule = L₂'.toSubmodule
h : ↑L₁'.toSubmodule = ↑L₂'.toSubmodule
⊢ L₁' = L₂'
[PROOFSTEP]
rw [← coe_set_eq]
[GOAL]
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
L' L₁' L₂' : LieSubalgebra R L
h✝ : L₁'.toSubmodule = L₂'.toSubmodule
h : ↑L₁'.toSubmodule = ↑L₂'.toSubmodule
⊢ ↑L₁' = ↑L₂'
[PROOFSTEP]
exact h
[GOAL]
R : Type u
L : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
L' : LieSubalgebra R L
M : Type w
inst✝⁷ : AddCommGroup M
inst✝⁶ : LieRingModule L M
N : Type w₁
inst✝⁵ : AddCommGroup N
inst✝⁴ : LieRingModule L N
inst✝³ : Module R N
inst✝² : LieModule R L N
inst✝¹ : Module R M
inst✝ : LieModule R L M
t : R
x : { x // x ∈ L' }
m : M
⊢ ⁅t • x, m⁆ = t • ⁅x, m⁆
[PROOFSTEP]
simp only [coe_bracket_of_module, smul_lie, Submodule.coe_smul_of_tower]
[GOAL]
R : Type u
L : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
L' : LieSubalgebra R L
M : Type w
inst✝⁷ : AddCommGroup M
inst✝⁶ : LieRingModule L M
N : Type w₁
inst✝⁵ : AddCommGroup N
inst✝⁴ : LieRingModule L N
inst✝³ : Module R N
inst✝² : LieModule R L N
inst✝¹ : Module R M
inst✝ : LieModule R L M
t : R
x : { x // x ∈ L' }
m : M
⊢ ⁅x, t • m⁆ = t • ⁅x, m⁆
[PROOFSTEP]
simp only [coe_bracket_of_module, lie_smul]
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
src✝ : Submodule R L₂ := LinearMap.range ↑f
⊢ ∀ {x y : L₂},
    x ∈
        { toAddSubmonoid := src✝.toAddSubmonoid,
                smul_mem' :=
                  (_ :
                    ∀ (c : R) {x : L₂},
                      x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier →
      y ∈
          { toAddSubmonoid := src✝.toAddSubmonoid,
                  smul_mem' :=
                    (_ :
                      ∀ (c : R) {x : L₂},
                        x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier →
        ⁅x, y⁆ ∈
          { toAddSubmonoid := src✝.toAddSubmonoid,
                  smul_mem' :=
                    (_ :
                      ∀ (c : R) {x : L₂},
                        x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
[PROOFSTEP]
rintro - - ⟨x, rfl⟩ ⟨y, rfl⟩
[GOAL]
case intro.intro
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
src✝ : Submodule R L₂ := LinearMap.range ↑f
x y : L
⊢ ⁅↑↑f x, ↑↑f y⁆ ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            smul_mem' :=
              (_ :
                ∀ (c : R) {x : L₂}, x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
[PROOFSTEP]
exact ⟨⁅x, y⁆, f.map_lie x y⟩
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
src✝ : L →ₗ[R] { x // x ∈ LinearMap.range ↑f } := LinearMap.rangeRestrict ↑f
x y : L
⊢ AddHom.toFun
      { toAddHom := src✝.toAddHom,
          map_smul' :=
            (_ :
              ∀ (r : R) (x : L),
                AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
      ⁅x, y⁆ =
    ⁅AddHom.toFun
        { toAddHom := src✝.toAddHom,
            map_smul' :=
              (_ :
                ∀ (r : R) (x : L),
                  AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
        x,
      AddHom.toFun
        { toAddHom := src✝.toAddHom,
            map_smul' :=
              (_ :
                ∀ (r : R) (x : L),
                  AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
        y⁆
[PROOFSTEP]
apply Subtype.ext
[GOAL]
case a
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
src✝ : L →ₗ[R] { x // x ∈ LinearMap.range ↑f } := LinearMap.rangeRestrict ↑f
x y : L
⊢ ↑(AddHom.toFun
        { toAddHom := src✝.toAddHom,
            map_smul' :=
              (_ :
                ∀ (r : R) (x : L),
                  AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
        ⁅x, y⁆) =
    ↑⁅AddHom.toFun
          { toAddHom := src✝.toAddHom,
              map_smul' :=
                (_ :
                  ∀ (r : R) (x : L),
                    AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
          x,
        AddHom.toFun
          { toAddHom := src✝.toAddHom,
              map_smul' :=
                (_ :
                  ∀ (r : R) (x : L),
                    AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
          y⁆
[PROOFSTEP]
exact f.map_lie x y
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
⊢ Function.Surjective ↑(rangeRestrict f)
[PROOFSTEP]
rintro ⟨y, hy⟩
[GOAL]
case mk
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
y : L₂
hy : y ∈ range f
⊢ ∃ a, ↑(rangeRestrict f) a = { val := y, property := hy }
[PROOFSTEP]
erw [mem_range] at hy
[GOAL]
case mk
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
y : L₂
hy✝ : y ∈ range f
hy : ∃ y_1, ↑f y_1 = y
⊢ ∃ a, ↑(rangeRestrict f) a = { val := y, property := hy✝ }
[PROOFSTEP]
obtain ⟨x, rfl⟩ := hy
[GOAL]
case mk.intro
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
x : L
hy : ↑f x ∈ range f
⊢ ∃ a, ↑(rangeRestrict f) a = { val := ↑f x, property := hy }
[PROOFSTEP]
use x
[GOAL]
case h
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
x : L
hy : ↑f x ∈ range f
⊢ ↑(rangeRestrict f) x = { val := ↑f x, property := hy }
[PROOFSTEP]
simp only [Subtype.mk_eq_mk, rangeRestrict_apply]
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
h : Function.Injective ↑f
x y : L
hxy : ↑(rangeRestrict f) x = ↑(rangeRestrict f) y
⊢ x = y
[PROOFSTEP]
simp only [Subtype.mk_eq_mk, rangeRestrict_apply] at hxy
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
h : Function.Injective ↑f
x y : L
hxy : ↑f x = ↑f y
⊢ x = y
[PROOFSTEP]
exact h hxy
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
p : Submodule R L
⊢ (∃ K, K.toSubmodule = p) ↔ ∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
p : Submodule R L
⊢ (∃ K, K.toSubmodule = p) → ∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p
[PROOFSTEP]
rintro ⟨K, rfl⟩ _ _
[GOAL]
case mp.intro
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K : LieSubalgebra R L
x✝ y✝ : L
⊢ x✝ ∈ K.toSubmodule → y✝ ∈ K.toSubmodule → ⁅x✝, y✝⁆ ∈ K.toSubmodule
[PROOFSTEP]
exact K.lie_mem'
[GOAL]
case mpr
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
p : Submodule R L
⊢ (∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p) → ∃ K, K.toSubmodule = p
[PROOFSTEP]
intro h
[GOAL]
case mpr
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
p : Submodule R L
h : ∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p
⊢ ∃ K, K.toSubmodule = p
[PROOFSTEP]
use{ p with lie_mem' := h _ _ }
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
⊢ LieHom.range (incl K) = K
[PROOFSTEP]
rw [← coe_to_submodule_eq_iff]
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
⊢ (LieHom.range (incl K)).toSubmodule = K.toSubmodule
[PROOFSTEP]
exact (K : Submodule R L).range_subtype
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
src✝ : Submodule R L₂ := Submodule.map (↑f) K.toSubmodule
x y : L₂
hx :
  x ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            smul_mem' :=
              (_ :
                ∀ (c : R) {x : L₂}, x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
hy :
  y ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            smul_mem' :=
              (_ :
                ∀ (c : R) {x : L₂}, x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
⊢ ⁅x, y⁆ ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            smul_mem' :=
              (_ :
                ∀ (c : R) {x : L₂}, x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
[PROOFSTEP]
erw [Submodule.mem_map] at hx
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
src✝ : Submodule R L₂ := Submodule.map (↑f) K.toSubmodule
x y : L₂
hx : ∃ y, y ∈ K.toSubmodule ∧ ↑↑f y = x
hy :
  y ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            smul_mem' :=
              (_ :
                ∀ (c : R) {x : L₂}, x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
⊢ ⁅x, y⁆ ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            smul_mem' :=
              (_ :
                ∀ (c : R) {x : L₂}, x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
[PROOFSTEP]
rcases hx with ⟨x', hx', hx⟩
[GOAL]
case intro.intro
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
src✝ : Submodule R L₂ := Submodule.map (↑f) K.toSubmodule
x y : L₂
hy :
  y ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            smul_mem' :=
              (_ :
                ∀ (c : R) {x : L₂}, x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
x' : L
hx' : x' ∈ K.toSubmodule
hx : ↑↑f x' = x
⊢ ⁅x, y⁆ ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            smul_mem' :=
              (_ :
                ∀ (c : R) {x : L₂}, x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
[PROOFSTEP]
rw [← hx]
[GOAL]
case intro.intro
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
src✝ : Submodule R L₂ := Submodule.map (↑f) K.toSubmodule
x y : L₂
hy :
  y ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            smul_mem' :=
              (_ :
                ∀ (c : R) {x : L₂}, x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
x' : L
hx' : x' ∈ K.toSubmodule
hx : ↑↑f x' = x
⊢ ⁅↑↑f x', y⁆ ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            smul_mem' :=
              (_ :
                ∀ (c : R) {x : L₂}, x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
[PROOFSTEP]
erw [Submodule.mem_map] at hy
[GOAL]
case intro.intro
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
src✝ : Submodule R L₂ := Submodule.map (↑f) K.toSubmodule
x y : L₂
hy : ∃ y_1, y_1 ∈ K.toSubmodule ∧ ↑↑f y_1 = y
x' : L
hx' : x' ∈ K.toSubmodule
hx : ↑↑f x' = x
⊢ ⁅↑↑f x', y⁆ ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            smul_mem' :=
              (_ :
                ∀ (c : R) {x : L₂}, x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
[PROOFSTEP]
rcases hy with ⟨y', hy', hy⟩
[GOAL]
case intro.intro.intro.intro
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
src✝ : Submodule R L₂ := Submodule.map (↑f) K.toSubmodule
x y : L₂
x' : L
hx' : x' ∈ K.toSubmodule
hx : ↑↑f x' = x
y' : L
hy' : y' ∈ K.toSubmodule
hy : ↑↑f y' = y
⊢ ⁅↑↑f x', y⁆ ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            smul_mem' :=
              (_ :
                ∀ (c : R) {x : L₂}, x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
[PROOFSTEP]
rw [← hy]
[GOAL]
case intro.intro.intro.intro
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
src✝ : Submodule R L₂ := Submodule.map (↑f) K.toSubmodule
x y : L₂
x' : L
hx' : x' ∈ K.toSubmodule
hx : ↑↑f x' = x
y' : L
hy' : y' ∈ K.toSubmodule
hy : ↑↑f y' = y
⊢ ⁅↑↑f x', ↑↑f y'⁆ ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            smul_mem' :=
              (_ :
                ∀ (c : R) {x : L₂}, x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
[PROOFSTEP]
erw [Submodule.mem_map]
[GOAL]
case intro.intro.intro.intro
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
src✝ : Submodule R L₂ := Submodule.map (↑f) K.toSubmodule
x y : L₂
x' : L
hx' : x' ∈ K.toSubmodule
hx : ↑↑f x' = x
y' : L
hy' : y' ∈ K.toSubmodule
hy : ↑↑f y' = y
⊢ ∃ y, y ∈ K.toSubmodule ∧ ↑↑f y = ⁅↑↑f x', ↑↑f y'⁆
[PROOFSTEP]
exact ⟨⁅x', y'⁆, K.lie_mem hx' hy', f.map_lie x' y'⟩
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
src✝ : Submodule R L := Submodule.comap (↑f) K₂.toSubmodule
x y : L
hx :
  x ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            smul_mem' :=
              (_ :
                ∀ (c : R) {x : L}, x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
hy :
  y ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            smul_mem' :=
              (_ :
                ∀ (c : R) {x : L}, x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
⊢ ⁅x, y⁆ ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            smul_mem' :=
              (_ :
                ∀ (c : R) {x : L}, x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
[PROOFSTEP]
suffices ⁅f x, f y⁆ ∈ K₂ by simp [this]
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
src✝ : Submodule R L := Submodule.comap (↑f) K₂.toSubmodule
x y : L
hx :
  x ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            smul_mem' :=
              (_ :
                ∀ (c : R) {x : L}, x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
hy :
  y ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            smul_mem' :=
              (_ :
                ∀ (c : R) {x : L}, x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
this : ⁅↑f x, ↑f y⁆ ∈ K₂
⊢ ⁅x, y⁆ ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            smul_mem' :=
              (_ :
                ∀ (c : R) {x : L}, x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
[PROOFSTEP]
simp [this]
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
src✝ : Submodule R L := Submodule.comap (↑f) K₂.toSubmodule
x y : L
hx :
  x ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            smul_mem' :=
              (_ :
                ∀ (c : R) {x : L}, x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
hy :
  y ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            smul_mem' :=
              (_ :
                ∀ (c : R) {x : L}, x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
⊢ ⁅↑f x, ↑f y⁆ ∈ K₂
[PROOFSTEP]
exact K₂.lie_mem hx hy
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
⊢ LieHom.range f = map f ⊤
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
x✝ : L₂
⊢ x✝ ∈ LieHom.range f ↔ x✝ ∈ map f ⊤
[PROOFSTEP]
simp
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
S : Set (LieSubalgebra R L)
src✝ : Submodule R L := sInf {x | ∃ s, s ∈ S ∧ s.toSubmodule = x}
x y : L
hx :
  x ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            smul_mem' :=
              (_ :
                ∀ (c : R) {x : L}, x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
hy :
  y ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            smul_mem' :=
              (_ :
                ∀ (c : R) {x : L}, x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
⊢ ⁅x, y⁆ ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            smul_mem' :=
              (_ :
                ∀ (c : R) {x : L}, x ∈ src✝.carrier → c • x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
[PROOFSTEP]
simp only [Submodule.mem_carrier, mem_iInter, Submodule.sInf_coe, mem_setOf_eq, forall_apply_eq_imp_iff₂, exists_imp,
  and_imp] at hx hy ⊢
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
S : Set (LieSubalgebra R L)
src✝ : Submodule R L := sInf {x | ∃ s, s ∈ S ∧ s.toSubmodule = x}
x y : L
hx : ∀ (a : LieSubalgebra R L), a ∈ S → x ∈ ↑a.toSubmodule
hy : ∀ (a : LieSubalgebra R L), a ∈ S → y ∈ ↑a.toSubmodule
⊢ ∀ (a : LieSubalgebra R L), a ∈ S → ⁅x, y⁆ ∈ ↑a.toSubmodule
[PROOFSTEP]
intro K hK
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K✝ K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
S : Set (LieSubalgebra R L)
src✝ : Submodule R L := sInf {x | ∃ s, s ∈ S ∧ s.toSubmodule = x}
x y : L
hx : ∀ (a : LieSubalgebra R L), a ∈ S → x ∈ ↑a.toSubmodule
hy : ∀ (a : LieSubalgebra R L), a ∈ S → y ∈ ↑a.toSubmodule
K : LieSubalgebra R L
hK : K ∈ S
⊢ ⁅x, y⁆ ∈ ↑K.toSubmodule
[PROOFSTEP]
exact K.lie_mem (hx K hK) (hy K hK)
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
S : Set (LieSubalgebra R L)
⊢ ↑(sInf S) = ⋂ (s : LieSubalgebra R L) (_ : s ∈ S), ↑s
[PROOFSTEP]
rw [← coe_to_submodule, sInf_coe_to_submodule, Submodule.sInf_coe]
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
S : Set (LieSubalgebra R L)
⊢ ⋂ (p : Submodule R L) (_ : p ∈ {x | ∃ s, s ∈ S ∧ s.toSubmodule = x}), ↑p = ⋂ (s : LieSubalgebra R L) (_ : s ∈ S), ↑s
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
S : Set (LieSubalgebra R L)
x : L
⊢ x ∈ ⋂ (p : Submodule R L) (_ : p ∈ {x | ∃ s, s ∈ S ∧ s.toSubmodule = x}), ↑p ↔
    x ∈ ⋂ (s : LieSubalgebra R L) (_ : s ∈ S), ↑s
[PROOFSTEP]
simp
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
S : Set (LieSubalgebra R L)
⊢ IsGLB S (sInf S)
[PROOFSTEP]
have h : ∀ K K' : LieSubalgebra R L, (K : Set L) ≤ K' ↔ K ≤ K' :=
  by
  intros
  exact Iff.rfl
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
S : Set (LieSubalgebra R L)
⊢ ∀ (K K' : LieSubalgebra R L), ↑K ≤ ↑K' ↔ K ≤ K'
[PROOFSTEP]
intros
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
S : Set (LieSubalgebra R L)
K✝ K'✝ : LieSubalgebra R L
⊢ ↑K✝ ≤ ↑K'✝ ↔ K✝ ≤ K'✝
[PROOFSTEP]
exact Iff.rfl
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
S : Set (LieSubalgebra R L)
h : ∀ (K K' : LieSubalgebra R L), ↑K ≤ ↑K' ↔ K ≤ K'
⊢ IsGLB S (sInf S)
[PROOFSTEP]
apply IsGLB.of_image @h
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
S : Set (LieSubalgebra R L)
h : ∀ (K K' : LieSubalgebra R L), ↑K ≤ ↑K' ↔ K ≤ K'
⊢ IsGLB ((fun x => ↑x) '' S) ↑(sInf S)
[PROOFSTEP]
simp only [sInf_coe]
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
S : Set (LieSubalgebra R L)
h : ∀ (K K' : LieSubalgebra R L), ↑K ≤ ↑K' ↔ K ≤ K'
⊢ IsGLB ((fun x => ↑x) '' S) (⋂ (s : LieSubalgebra R L) (_ : s ∈ S), ↑s)
[PROOFSTEP]
exact isGLB_biInf
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
src✝ : CompleteLattice (LieSubalgebra R L) :=
  completeLatticeOfInf (LieSubalgebra R L) (_ : ∀ (S : Set (LieSubalgebra R L)), IsGLB S (sInf S))
N : LieSubalgebra R L
x✝ : L
h : x✝ ∈ ⊥
⊢ x✝ ∈ N
[PROOFSTEP]
rw [mem_bot] at h
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
src✝ : CompleteLattice (LieSubalgebra R L) :=
  completeLatticeOfInf (LieSubalgebra R L) (_ : ∀ (S : Set (LieSubalgebra R L)), IsGLB S (sInf S))
N : LieSubalgebra R L
x✝ : L
h : x✝ = 0
⊢ x✝ ∈ N
[PROOFSTEP]
rw [h]
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
src✝ : CompleteLattice (LieSubalgebra R L) :=
  completeLatticeOfInf (LieSubalgebra R L) (_ : ∀ (S : Set (LieSubalgebra R L)), IsGLB S (sInf S))
N : LieSubalgebra R L
x✝ : L
h : x✝ = 0
⊢ 0 ∈ N
[PROOFSTEP]
exact N.zero_mem'
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
x : L
⊢ x ∈ K ⊓ K' ↔ x ∈ K ∧ x ∈ K'
[PROOFSTEP]
rw [← mem_coe_submodule, ← mem_coe_submodule, ← mem_coe_submodule, inf_coe_to_submodule, Submodule.mem_inf]
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
⊢ K = ⊥ ↔ ∀ (x : L), x ∈ K → x = 0
[PROOFSTEP]
rw [_root_.eq_bot_iff]
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
⊢ K ≤ ⊥ ↔ ∀ (x : L), x ∈ K → x = 0
[PROOFSTEP]
exact Iff.rfl
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
⊢ Subsingleton (LieSubalgebra R { x // x ∈ ⊥ })
[PROOFSTEP]
apply subsingleton_of_bot_eq_top
[GOAL]
case hα
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
⊢ ⊥ = ⊤
[PROOFSTEP]
ext ⟨x, hx⟩
[GOAL]
case hα.h.mk
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
x : L
hx : x ∈ ⊥
⊢ { val := x, property := hx } ∈ ⊥ ↔ { val := x, property := hx } ∈ ⊤
[PROOFSTEP]
change x ∈ ⊥ at hx
[GOAL]
case hα.h.mk
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
x : L
hx : x ∈ ⊥
⊢ { val := x, property := hx } ∈ ⊥ ↔ { val := x, property := hx } ∈ ⊤
[PROOFSTEP]
rw [LieSubalgebra.mem_bot] at hx
[GOAL]
case hα.h.mk
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
x : L
hx✝ : x ∈ ⊥
hx : x = 0
⊢ { val := x, property := hx✝ } ∈ ⊥ ↔ { val := x, property := hx✝ } ∈ ⊤
[PROOFSTEP]
subst hx
[GOAL]
case hα.h.mk
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
hx : 0 ∈ ⊥
⊢ { val := 0, property := hx } ∈ ⊥ ↔ { val := 0, property := hx } ∈ ⊤
[PROOFSTEP]
simp only [true_iff_iff, eq_self_iff_true, Submodule.mk_eq_zero, mem_bot, mem_top]
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
⊢ Subsingleton ↑↑⊥
[PROOFSTEP]
simp
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
h : K ≤ K'
x y : { x // x ∈ K }
⊢ ↑(homOfLe h) x = ↑(homOfLe h) y → x = y
[PROOFSTEP]
simp only [homOfLe_apply, imp_self, Subtype.mk_eq_mk, SetLike.coe_eq_coe]
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
h : K ≤ K'
x : { x // x ∈ K' }
⊢ x ∈ ofLe h ↔ ↑x ∈ K
[PROOFSTEP]
simp only [ofLe, homOfLe_apply, LieHom.mem_range]
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
h : K ≤ K'
x : { x // x ∈ K' }
⊢ (∃ y, { val := ↑y, property := (_ : ↑y ∈ K') } = x) ↔ ↑x ∈ K
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
h : K ≤ K'
x : { x // x ∈ K' }
⊢ (∃ y, { val := ↑y, property := (_ : ↑y ∈ K') } = x) → ↑x ∈ K
[PROOFSTEP]
rintro ⟨y, rfl⟩
[GOAL]
case mp.intro
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
h : K ≤ K'
y : { x // x ∈ K }
⊢ ↑{ val := ↑y, property := (_ : ↑y ∈ K') } ∈ K
[PROOFSTEP]
exact y.property
[GOAL]
case mpr
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
h : K ≤ K'
x : { x // x ∈ K' }
⊢ ↑x ∈ K → ∃ y, { val := ↑y, property := (_ : ↑y ∈ K') } = x
[PROOFSTEP]
intro h
[GOAL]
case mpr
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
h✝ : K ≤ K'
x : { x // x ∈ K' }
h : ↑x ∈ K
⊢ ∃ y, { val := ↑y, property := (_ : ↑y ∈ K') } = x
[PROOFSTEP]
use⟨(x : L), h⟩
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
h : K ≤ K'
⊢ ofLe h = comap (incl K') K
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
h : K ≤ K'
x✝ : { x // x ∈ K' }
⊢ x✝ ∈ ofLe h ↔ x✝ ∈ comap (incl K') K
[PROOFSTEP]
rw [mem_ofLe]
[GOAL]
case h
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
h : K ≤ K'
x✝ : { x // x ∈ K' }
⊢ ↑x✝ ∈ K ↔ x✝ ∈ comap (incl K') K
[PROOFSTEP]
rfl
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
s : Set L
x : L
⊢ x ∈ lieSpan R L s ↔ ∀ (K : LieSubalgebra R L), s ⊆ ↑K → x ∈ K
[PROOFSTEP]
change x ∈ (lieSpan R L s : Set L) ↔ _
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
s : Set L
x : L
⊢ x ∈ ↑(lieSpan R L s) ↔ ∀ (K : LieSubalgebra R L), s ⊆ ↑K → x ∈ K
[PROOFSTEP]
erw [sInf_coe]
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
s : Set L
x : L
⊢ x ∈ ⋂ (s_1 : LieSubalgebra R L) (_ : s_1 ∈ {N | s ⊆ ↑N}), ↑s_1 ↔ ∀ (K : LieSubalgebra R L), s ⊆ ↑K → x ∈ K
[PROOFSTEP]
exact Set.mem_iInter₂
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
s : Set L
⊢ s ⊆ ↑(lieSpan R L s)
[PROOFSTEP]
intro m hm
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
s : Set L
m : L
hm : m ∈ s
⊢ m ∈ ↑(lieSpan R L s)
[PROOFSTEP]
erw [mem_lieSpan]
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
s : Set L
m : L
hm : m ∈ s
⊢ ∀ (K : LieSubalgebra R L), s ⊆ ↑K → m ∈ K
[PROOFSTEP]
intro K hK
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K✝ K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
s : Set L
m : L
hm : m ∈ s
K : LieSubalgebra R L
hK : s ⊆ ↑K
⊢ m ∈ K
[PROOFSTEP]
exact hK hm
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
s : Set L
⊢ Submodule.span R s ≤ (lieSpan R L s).toSubmodule
[PROOFSTEP]
rw [Submodule.span_le]
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
s : Set L
⊢ s ⊆ ↑(lieSpan R L s).toSubmodule
[PROOFSTEP]
apply subset_lieSpan
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K✝ K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
s : Set L
K : LieSubalgebra R L
⊢ lieSpan R L s ≤ K ↔ s ⊆ ↑K
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K✝ K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
s : Set L
K : LieSubalgebra R L
⊢ lieSpan R L s ≤ K → s ⊆ ↑K
[PROOFSTEP]
exact Set.Subset.trans subset_lieSpan
[GOAL]
case mpr
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K✝ K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
s : Set L
K : LieSubalgebra R L
⊢ s ⊆ ↑K → lieSpan R L s ≤ K
[PROOFSTEP]
intro hs m hm
[GOAL]
case mpr
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K✝ K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
s : Set L
K : LieSubalgebra R L
hs : s ⊆ ↑K
m : L
hm : m ∈ lieSpan R L s
⊢ m ∈ K
[PROOFSTEP]
rw [mem_lieSpan] at hm
[GOAL]
case mpr
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K✝ K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
s : Set L
K : LieSubalgebra R L
hs : s ⊆ ↑K
m : L
hm : ∀ (K : LieSubalgebra R L), s ⊆ ↑K → m ∈ K
⊢ m ∈ K
[PROOFSTEP]
exact hm _ hs
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
s t : Set L
h : s ⊆ t
⊢ lieSpan R L s ≤ lieSpan R L t
[PROOFSTEP]
rw [lieSpan_le]
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
s t : Set L
h : s ⊆ t
⊢ s ⊆ ↑(lieSpan R L t)
[PROOFSTEP]
exact Set.Subset.trans h subset_lieSpan
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
s : Set L
p : Submodule R L
⊢ (lieSpan R L ↑p).toSubmodule = p ↔ ∃ K, K.toSubmodule = p
[PROOFSTEP]
rw [p.exists_lieSubalgebra_coe_eq_iff]
[GOAL]
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
s : Set L
p : Submodule R L
⊢ (lieSpan R L ↑p).toSubmodule = p ↔ ∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
s : Set L
p : Submodule R L
⊢ (lieSpan R L ↑p).toSubmodule = p → ∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p
[PROOFSTEP]
intro h
[GOAL]
case mpr
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
s : Set L
p : Submodule R L
⊢ (∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p) → (lieSpan R L ↑p).toSubmodule = p
[PROOFSTEP]
intro h
[GOAL]
case mp
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
s : Set L
p : Submodule R L
h : (lieSpan R L ↑p).toSubmodule = p
⊢ ∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p
[PROOFSTEP]
intro x m hm
[GOAL]
case mp
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
s : Set L
p : Submodule R L
h : (lieSpan R L ↑p).toSubmodule = p
x m : L
hm : x ∈ p
⊢ m ∈ p → ⁅x, m⁆ ∈ p
[PROOFSTEP]
rw [← h, mem_coe_submodule]
[GOAL]
case mp
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
s : Set L
p : Submodule R L
h : (lieSpan R L ↑p).toSubmodule = p
x m : L
hm : x ∈ p
⊢ m ∈ lieSpan R L ↑p → ⁅x, m⁆ ∈ (lieSpan R L ↑p).toSubmodule
[PROOFSTEP]
exact lie_mem _ (subset_lieSpan hm)
[GOAL]
case mpr
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
s : Set L
p : Submodule R L
h : ∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p
⊢ (lieSpan R L ↑p).toSubmodule = p
[PROOFSTEP]
rw [← coe_to_submodule_mk p @h, coe_to_submodule, coe_to_submodule_eq_iff, lieSpan_eq]
[GOAL]
R : Type u
L₁ : Type v
L₂ : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L₁
inst✝² : LieRing L₂
inst✝¹ : LieAlgebra R L₁
inst✝ : LieAlgebra R L₂
f : L₁ →ₗ⁅R⁆ L₂
h : Function.Injective ↑f
⊢ Function.Injective ↑↑f
[PROOFSTEP]
rwa [LieHom.coe_toLinearMap]
[GOAL]
R : Type u
L₁ : Type v
L₂ : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L₁
inst✝² : LieRing L₂
inst✝¹ : LieAlgebra R L₁
inst✝ : LieAlgebra R L₂
L₁' L₁'' : LieSubalgebra R L₁
L₂' : LieSubalgebra R L₂
h : ↑L₁' = ↑L₁''
⊢ L₁'.toSubmodule = L₁''.toSubmodule
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u
L₁ : Type v
L₂ : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L₁
inst✝² : LieRing L₂
inst✝¹ : LieAlgebra R L₁
inst✝ : LieAlgebra R L₂
L₁' L₁'' : LieSubalgebra R L₁
L₂' : LieSubalgebra R L₂
h : ↑L₁' = ↑L₁''
x : L₁
⊢ x ∈ L₁'.toSubmodule ↔ x ∈ L₁''.toSubmodule
[PROOFSTEP]
change x ∈ (L₁' : Set L₁) ↔ x ∈ (L₁'' : Set L₁)
[GOAL]
case h
R : Type u
L₁ : Type v
L₂ : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L₁
inst✝² : LieRing L₂
inst✝¹ : LieAlgebra R L₁
inst✝ : LieAlgebra R L₂
L₁' L₁'' : LieSubalgebra R L₁
L₂' : LieSubalgebra R L₂
h : ↑L₁' = ↑L₁''
x : L₁
⊢ x ∈ ↑L₁' ↔ x ∈ ↑L₁''
[PROOFSTEP]
rw [h]
[GOAL]
R : Type u
L₁ : Type v
L₂ : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L₁
inst✝² : LieRing L₂
inst✝¹ : LieAlgebra R L₁
inst✝ : LieAlgebra R L₂
L₁' L₁'' : LieSubalgebra R L₁
L₂' : LieSubalgebra R L₂
e : L₁ ≃ₗ⁅R⁆ L₂
src✝ : { x // x ∈ L₁''.toSubmodule } ≃ₗ[R] { x // x ∈ Submodule.map (↑(toLinearEquiv e)) L₁''.toSubmodule } :=
  LinearEquiv.submoduleMap (toLinearEquiv e) L₁''.toSubmodule
x y : { x // x ∈ L₁'' }
⊢ AddHom.toFun src✝.toAddHom ⁅x, y⁆ = ⁅AddHom.toFun src✝.toAddHom x, AddHom.toFun src✝.toAddHom y⁆
[PROOFSTEP]
apply SetCoe.ext
[GOAL]
case a
R : Type u
L₁ : Type v
L₂ : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L₁
inst✝² : LieRing L₂
inst✝¹ : LieAlgebra R L₁
inst✝ : LieAlgebra R L₂
L₁' L₁'' : LieSubalgebra R L₁
L₂' : LieSubalgebra R L₂
e : L₁ ≃ₗ⁅R⁆ L₂
src✝ : { x // x ∈ L₁''.toSubmodule } ≃ₗ[R] { x // x ∈ Submodule.map (↑(toLinearEquiv e)) L₁''.toSubmodule } :=
  LinearEquiv.submoduleMap (toLinearEquiv e) L₁''.toSubmodule
x y : { x // x ∈ L₁'' }
⊢ ↑(AddHom.toFun src✝.toAddHom ⁅x, y⁆) = ↑⁅AddHom.toFun src✝.toAddHom x, AddHom.toFun src✝.toAddHom y⁆
[PROOFSTEP]
exact LieHom.map_lie (↑e : L₁ →ₗ⁅R⁆ L₂) ↑x ↑y
[GOAL]
R : Type u
L₁ : Type v
L₂ : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L₁
inst✝² : LieRing L₂
inst✝¹ : LieAlgebra R L₁
inst✝ : LieAlgebra R L₂
L₁' L₁'' : LieSubalgebra R L₁
L₂' : LieSubalgebra R L₂
e : L₁ ≃ₗ⁅R⁆ L₂
h : LieSubalgebra.map e.toLieHom L₁' = L₂'
⊢ Submodule.map (↑(toLinearEquiv e)) L₁'.toSubmodule = L₂'.toSubmodule
[PROOFSTEP]
rw [← h]
[GOAL]
R : Type u
L₁ : Type v
L₂ : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L₁
inst✝² : LieRing L₂
inst✝¹ : LieAlgebra R L₁
inst✝ : LieAlgebra R L₂
L₁' L₁'' : LieSubalgebra R L₁
L₂' : LieSubalgebra R L₂
e : L₁ ≃ₗ⁅R⁆ L₂
h : LieSubalgebra.map e.toLieHom L₁' = L₂'
⊢ Submodule.map (↑(toLinearEquiv e)) L₁'.toSubmodule = (LieSubalgebra.map e.toLieHom L₁').toSubmodule
[PROOFSTEP]
rfl
[GOAL]
R : Type u
L₁ : Type v
L₂ : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L₁
inst✝² : LieRing L₂
inst✝¹ : LieAlgebra R L₁
inst✝ : LieAlgebra R L₂
L₁' L₁'' : LieSubalgebra R L₁
L₂' : LieSubalgebra R L₂
e : L₁ ≃ₗ⁅R⁆ L₂
h : LieSubalgebra.map e.toLieHom L₁' = L₂'
src✝ : { x // x ∈ L₁'.toSubmodule } ≃ₗ[R] { x // x ∈ L₂'.toSubmodule } :=
  LinearEquiv.ofSubmodules (toLinearEquiv e) L₁'.toSubmodule L₂'.toSubmodule
    (_ : Submodule.map (↑(toLinearEquiv e)) L₁'.toSubmodule = L₂'.toSubmodule)
x y : { x // x ∈ L₁' }
⊢ AddHom.toFun src✝.toAddHom ⁅x, y⁆ = ⁅AddHom.toFun src✝.toAddHom x, AddHom.toFun src✝.toAddHom y⁆
[PROOFSTEP]
apply SetCoe.ext
[GOAL]
case a
R : Type u
L₁ : Type v
L₂ : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L₁
inst✝² : LieRing L₂
inst✝¹ : LieAlgebra R L₁
inst✝ : LieAlgebra R L₂
L₁' L₁'' : LieSubalgebra R L₁
L₂' : LieSubalgebra R L₂
e : L₁ ≃ₗ⁅R⁆ L₂
h : LieSubalgebra.map e.toLieHom L₁' = L₂'
src✝ : { x // x ∈ L₁'.toSubmodule } ≃ₗ[R] { x // x ∈ L₂'.toSubmodule } :=
  LinearEquiv.ofSubmodules (toLinearEquiv e) L₁'.toSubmodule L₂'.toSubmodule
    (_ : Submodule.map (↑(toLinearEquiv e)) L₁'.toSubmodule = L₂'.toSubmodule)
x y : { x // x ∈ L₁' }
⊢ ↑(AddHom.toFun src✝.toAddHom ⁅x, y⁆) = ↑⁅AddHom.toFun src✝.toAddHom x, AddHom.toFun src✝.toAddHom y⁆
[PROOFSTEP]
exact LieHom.map_lie (↑e : L₁ →ₗ⁅R⁆ L₂) ↑x ↑y


[GOAL]
a b : Cardinal.{u}
n m : ℕ
⊢ IsUnit a ↔ a = 1
[PROOFSTEP]
refine'
  ⟨fun h => _, by
    rintro rfl
    exact isUnit_one⟩
[GOAL]
a b : Cardinal.{u}
n m : ℕ
⊢ a = 1 → IsUnit a
[PROOFSTEP]
rintro rfl
[GOAL]
b : Cardinal.{u}
n m : ℕ
⊢ IsUnit 1
[PROOFSTEP]
exact isUnit_one
[GOAL]
a b : Cardinal.{u}
n m : ℕ
h : IsUnit a
⊢ a = 1
[PROOFSTEP]
rcases eq_or_ne a 0 with (rfl | ha)
[GOAL]
case inl
b : Cardinal.{u}
n m : ℕ
h : IsUnit 0
⊢ 0 = 1
[PROOFSTEP]
exact (not_isUnit_zero h).elim
[GOAL]
case inr
a b : Cardinal.{u}
n m : ℕ
h : IsUnit a
ha : a ≠ 0
⊢ a = 1
[PROOFSTEP]
rw [isUnit_iff_forall_dvd] at h
[GOAL]
case inr
a b : Cardinal.{u}
n m : ℕ
h : ∀ (y : Cardinal.{u}), a ∣ y
ha : a ≠ 0
⊢ a = 1
[PROOFSTEP]
cases' h 1 with t ht
[GOAL]
case inr.intro
a b : Cardinal.{u}
n m : ℕ
h : ∀ (y : Cardinal.{u}), a ∣ y
ha : a ≠ 0
t : Cardinal.{u}
ht : 1 = a * t
⊢ a = 1
[PROOFSTEP]
rw [eq_comm, mul_eq_one_iff'] at ht
[GOAL]
case inr.intro
a b : Cardinal.{u}
n m : ℕ
h : ∀ (y : Cardinal.{u}), a ∣ y
ha : a ≠ 0
t : Cardinal.{u}
ht : a = 1 ∧ t = 1
⊢ a = 1
[PROOFSTEP]
exact ht.1
[GOAL]
case inr.intro.ha
a b : Cardinal.{u}
n m : ℕ
h : ∀ (y : Cardinal.{u}), a ∣ y
ha : a ≠ 0
t : Cardinal.{u}
ht : a * t = 1
⊢ 1 ≤ a
[PROOFSTEP]
exact one_le_iff_ne_zero.mpr ha
[GOAL]
case inr.intro.hb
a b : Cardinal.{u}
n m : ℕ
h : ∀ (y : Cardinal.{u}), a ∣ y
ha : a ≠ 0
t : Cardinal.{u}
ht : a * t = 1
⊢ 1 ≤ t
[PROOFSTEP]
apply one_le_iff_ne_zero.mpr
[GOAL]
case inr.intro.hb
a b : Cardinal.{u}
n m : ℕ
h : ∀ (y : Cardinal.{u}), a ∣ y
ha : a ≠ 0
t : Cardinal.{u}
ht : a * t = 1
⊢ t ≠ 0
[PROOFSTEP]
intro h
[GOAL]
case inr.intro.hb
a b : Cardinal.{u}
n m : ℕ
h✝ : ∀ (y : Cardinal.{u}), a ∣ y
ha : a ≠ 0
t : Cardinal.{u}
ht : a * t = 1
h : t = 0
⊢ False
[PROOFSTEP]
rw [h, mul_zero] at ht
[GOAL]
case inr.intro.hb
a b : Cardinal.{u}
n m : ℕ
h✝ : ∀ (y : Cardinal.{u}), a ∣ y
ha : a ≠ 0
t : Cardinal.{u}
ht : 0 = 1
h : t = 0
⊢ False
[PROOFSTEP]
exact zero_ne_one ht
[GOAL]
a✝ b✝ : Cardinal.{u}
n m : ℕ
a x : Cardinal.{u_1}
b0 : x ≠ 0
b : Cardinal.{u_1}
hab : x = a * b
⊢ a ≤ x
[PROOFSTEP]
simpa only [hab, mul_one] using
  mul_le_mul_left' (one_le_iff_ne_zero.2 fun h : b = 0 => b0 (by rwa [h, mul_zero] at hab )) a
[GOAL]
a✝ b✝ : Cardinal.{u}
n m : ℕ
a x : Cardinal.{u_1}
b0 : x ≠ 0
b : Cardinal.{u_1}
hab : x = a * b
h : b = 0
⊢ x = 0
[PROOFSTEP]
rwa [h, mul_zero] at hab
[GOAL]
a b : Cardinal.{u}
n m : ℕ
ha : ℵ₀ ≤ a
⊢ Prime a
[PROOFSTEP]
refine' ⟨(aleph0_pos.trans_le ha).ne', _, fun b c hbc => _⟩
[GOAL]
case refine'_1
a b : Cardinal.{u}
n m : ℕ
ha : ℵ₀ ≤ a
⊢ ¬IsUnit a
[PROOFSTEP]
rw [isUnit_iff]
[GOAL]
case refine'_1
a b : Cardinal.{u}
n m : ℕ
ha : ℵ₀ ≤ a
⊢ ¬a = 1
[PROOFSTEP]
exact (one_lt_aleph0.trans_le ha).ne'
[GOAL]
case refine'_2
a b✝ : Cardinal.{u}
n m : ℕ
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
⊢ a ∣ b ∨ a ∣ c
[PROOFSTEP]
cases' eq_or_ne (b * c) 0 with hz hz
[GOAL]
case refine'_2.inl
a b✝ : Cardinal.{u}
n m : ℕ
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c = 0
⊢ a ∣ b ∨ a ∣ c
[PROOFSTEP]
rcases mul_eq_zero.mp hz with (rfl | rfl)
[GOAL]
case refine'_2.inl.inl
a b : Cardinal.{u}
n m : ℕ
ha : ℵ₀ ≤ a
c : Cardinal.{u}
hbc : a ∣ 0 * c
hz : 0 * c = 0
⊢ a ∣ 0 ∨ a ∣ c
[PROOFSTEP]
simp
[GOAL]
case refine'_2.inl.inr
a b✝ : Cardinal.{u}
n m : ℕ
ha : ℵ₀ ≤ a
b : Cardinal.{u}
hbc : a ∣ b * 0
hz : b * 0 = 0
⊢ a ∣ b ∨ a ∣ 0
[PROOFSTEP]
simp
[GOAL]
case refine'_2.inr
a b✝ : Cardinal.{u}
n m : ℕ
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
⊢ a ∣ b ∨ a ∣ c
[PROOFSTEP]
wlog h : c ≤ b
[GOAL]
case refine'_2.inr.inr
a b✝ : Cardinal.{u}
n m : ℕ
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this :
  ∀ {a : Cardinal.{u}} {b : Cardinal.{u}} {n m : ℕ},
    ℵ₀ ≤ a → ∀ (b c : Cardinal.{u}), a ∣ b * c → b * c ≠ 0 → c ≤ b → a ∣ b ∨ a ∣ c
h : ¬c ≤ b
⊢ a ∣ b ∨ a ∣ c
[PROOFSTEP]
cases le_total c b <;> [skip; rw [or_comm]]
[GOAL]
case refine'_2.inr.inr
a b✝ : Cardinal.{u}
n m : ℕ
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this :
  ∀ {a : Cardinal.{u}} {b : Cardinal.{u}} {n m : ℕ},
    ℵ₀ ≤ a → ∀ (b c : Cardinal.{u}), a ∣ b * c → b * c ≠ 0 → c ≤ b → a ∣ b ∨ a ∣ c
h : ¬c ≤ b
⊢ a ∣ b ∨ a ∣ c
[PROOFSTEP]
cases le_total c b
[GOAL]
case refine'_2.inr.inr.inl
a b✝ : Cardinal.{u}
n m : ℕ
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this :
  ∀ {a : Cardinal.{u}} {b : Cardinal.{u}} {n m : ℕ},
    ℵ₀ ≤ a → ∀ (b c : Cardinal.{u}), a ∣ b * c → b * c ≠ 0 → c ≤ b → a ∣ b ∨ a ∣ c
h : ¬c ≤ b
h✝ : c ≤ b
⊢ a ∣ b ∨ a ∣ c
[PROOFSTEP]
skip
[GOAL]
case refine'_2.inr.inr.inr
a b✝ : Cardinal.{u}
n m : ℕ
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this :
  ∀ {a : Cardinal.{u}} {b : Cardinal.{u}} {n m : ℕ},
    ℵ₀ ≤ a → ∀ (b c : Cardinal.{u}), a ∣ b * c → b * c ≠ 0 → c ≤ b → a ∣ b ∨ a ∣ c
h : ¬c ≤ b
h✝ : b ≤ c
⊢ a ∣ b ∨ a ∣ c
[PROOFSTEP]
rw [or_comm]
[GOAL]
case refine'_2.inr.inr.inl
a b✝ : Cardinal.{u}
n m : ℕ
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this :
  ∀ {a : Cardinal.{u}} {b : Cardinal.{u}} {n m : ℕ},
    ℵ₀ ≤ a → ∀ (b c : Cardinal.{u}), a ∣ b * c → b * c ≠ 0 → c ≤ b → a ∣ b ∨ a ∣ c
h : ¬c ≤ b
h✝ : c ≤ b
⊢ a ∣ b ∨ a ∣ c
[PROOFSTEP]
apply_assumption
[GOAL]
case refine'_2.inr.inr.inr
a b✝ : Cardinal.{u}
n m : ℕ
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this :
  ∀ {a : Cardinal.{u}} {b : Cardinal.{u}} {n m : ℕ},
    ℵ₀ ≤ a → ∀ (b c : Cardinal.{u}), a ∣ b * c → b * c ≠ 0 → c ≤ b → a ∣ b ∨ a ∣ c
h : ¬c ≤ b
h✝ : b ≤ c
⊢ a ∣ c ∨ a ∣ b
[PROOFSTEP]
apply_assumption
[GOAL]
case refine'_2.inr.inr.inl.b
a b✝ : Cardinal.{u}
n m : ℕ
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this :
  ∀ {a : Cardinal.{u}} {b : Cardinal.{u}} {n m : ℕ},
    ℵ₀ ≤ a → ∀ (b c : Cardinal.{u}), a ∣ b * c → b * c ≠ 0 → c ≤ b → a ∣ b ∨ a ∣ c
h : ¬c ≤ b
h✝ : c ≤ b
hz_symm : 0 ≠ b * c
⊢ Cardinal.{u}
case refine'_2.inr.inr.inl.n
a b✝ : Cardinal.{u}
n m : ℕ
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this :
  ∀ {a : Cardinal.{u}} {b : Cardinal.{u}} {n m : ℕ},
    ℵ₀ ≤ a → ∀ (b c : Cardinal.{u}), a ∣ b * c → b * c ≠ 0 → c ≤ b → a ∣ b ∨ a ∣ c
h : ¬c ≤ b
h✝ : c ≤ b
hz_symm : 0 ≠ b * c
⊢ ℕ
case refine'_2.inr.inr.inl.m
a b✝ : Cardinal.{u}
n m : ℕ
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this :
  ∀ {a : Cardinal.{u}} {b : Cardinal.{u}} {n m : ℕ},
    ℵ₀ ≤ a → ∀ (b c : Cardinal.{u}), a ∣ b * c → b * c ≠ 0 → c ≤ b → a ∣ b ∨ a ∣ c
h : ¬c ≤ b
h✝ : c ≤ b
hz_symm : 0 ≠ b * c
⊢ ℕ
case refine'_2.inr.inr.inl.ha
a b✝ : Cardinal.{u}
n m : ℕ
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this :
  ∀ {a : Cardinal.{u}} {b : Cardinal.{u}} {n m : ℕ},
    ℵ₀ ≤ a → ∀ (b c : Cardinal.{u}), a ∣ b * c → b * c ≠ 0 → c ≤ b → a ∣ b ∨ a ∣ c
h : ¬c ≤ b
h✝ : c ≤ b
hz_symm : 0 ≠ b * c
⊢ ℵ₀ ≤ a
case refine'_2.inr.inr.inl.hbc
a b✝ : Cardinal.{u}
n m : ℕ
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this :
  ∀ {a : Cardinal.{u}} {b : Cardinal.{u}} {n m : ℕ},
    ℵ₀ ≤ a → ∀ (b c : Cardinal.{u}), a ∣ b * c → b * c ≠ 0 → c ≤ b → a ∣ b ∨ a ∣ c
h : ¬c ≤ b
h✝ : c ≤ b
hz_symm : 0 ≠ b * c
⊢ a ∣ b * c
case refine'_2.inr.inr.inl.hz
a b✝ : Cardinal.{u}
n m : ℕ
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this :
  ∀ {a : Cardinal.{u}} {b : Cardinal.{u}} {n m : ℕ},
    ℵ₀ ≤ a → ∀ (b c : Cardinal.{u}), a ∣ b * c → b * c ≠ 0 → c ≤ b → a ∣ b ∨ a ∣ c
h : ¬c ≤ b
h✝ : c ≤ b
hz_symm : 0 ≠ b * c
⊢ b * c ≠ 0
case refine'_2.inr.inr.inl.h
a b✝ : Cardinal.{u}
n m : ℕ
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this :
  ∀ {a : Cardinal.{u}} {b : Cardinal.{u}} {n m : ℕ},
    ℵ₀ ≤ a → ∀ (b c : Cardinal.{u}), a ∣ b * c → b * c ≠ 0 → c ≤ b → a ∣ b ∨ a ∣ c
h : ¬c ≤ b
h✝ : c ≤ b
hz_symm : 0 ≠ b * c
⊢ c ≤ b
case refine'_2.inr.inr.inr.b
a b✝ : Cardinal.{u}
n m : ℕ
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this :
  ∀ {a : Cardinal.{u}} {b : Cardinal.{u}} {n m : ℕ},
    ℵ₀ ≤ a → ∀ (b c : Cardinal.{u}), a ∣ b * c → b * c ≠ 0 → c ≤ b → a ∣ b ∨ a ∣ c
h : ¬c ≤ b
h✝ : b ≤ c
hz_symm : 0 ≠ b * c
⊢ Cardinal.{u}
case refine'_2.inr.inr.inr.n
a b✝ : Cardinal.{u}
n m : ℕ
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this :
  ∀ {a : Cardinal.{u}} {b : Cardinal.{u}} {n m : ℕ},
    ℵ₀ ≤ a → ∀ (b c : Cardinal.{u}), a ∣ b * c → b * c ≠ 0 → c ≤ b → a ∣ b ∨ a ∣ c
h : ¬c ≤ b
h✝ : b ≤ c
hz_symm : 0 ≠ b * c
⊢ ℕ
case refine'_2.inr.inr.inr.m
a b✝ : Cardinal.{u}
n m : ℕ
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this :
  ∀ {a : Cardinal.{u}} {b : Cardinal.{u}} {n m : ℕ},
    ℵ₀ ≤ a → ∀ (b c : Cardinal.{u}), a ∣ b * c → b * c ≠ 0 → c ≤ b → a ∣ b ∨ a ∣ c
h : ¬c ≤ b
h✝ : b ≤ c
hz_symm : 0 ≠ b * c
⊢ ℕ
case refine'_2.inr.inr.inr.ha
a b✝ : Cardinal.{u}
n m : ℕ
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this :
  ∀ {a : Cardinal.{u}} {b : Cardinal.{u}} {n m : ℕ},
    ℵ₀ ≤ a → ∀ (b c : Cardinal.{u}), a ∣ b * c → b * c ≠ 0 → c ≤ b → a ∣ b ∨ a ∣ c
h : ¬c ≤ b
h✝ : b ≤ c
hz_symm : 0 ≠ b * c
⊢ ℵ₀ ≤ a
case refine'_2.inr.inr.inr.hbc
a b✝ : Cardinal.{u}
n m : ℕ
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this :
  ∀ {a : Cardinal.{u}} {b : Cardinal.{u}} {n m : ℕ},
    ℵ₀ ≤ a → ∀ (b c : Cardinal.{u}), a ∣ b * c → b * c ≠ 0 → c ≤ b → a ∣ b ∨ a ∣ c
h : ¬c ≤ b
h✝ : b ≤ c
hz_symm : 0 ≠ b * c
⊢ a ∣ c * b
case refine'_2.inr.inr.inr.hz
a b✝ : Cardinal.{u}
n m : ℕ
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this :
  ∀ {a : Cardinal.{u}} {b : Cardinal.{u}} {n m : ℕ},
    ℵ₀ ≤ a → ∀ (b c : Cardinal.{u}), a ∣ b * c → b * c ≠ 0 → c ≤ b → a ∣ b ∨ a ∣ c
h : ¬c ≤ b
h✝ : b ≤ c
hz_symm : 0 ≠ b * c
⊢ c * b ≠ 0
case refine'_2.inr.inr.inr.h
a b✝ : Cardinal.{u}
n m : ℕ
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this :
  ∀ {a : Cardinal.{u}} {b : Cardinal.{u}} {n m : ℕ},
    ℵ₀ ≤ a → ∀ (b c : Cardinal.{u}), a ∣ b * c → b * c ≠ 0 → c ≤ b → a ∣ b ∨ a ∣ c
h : ¬c ≤ b
h✝ : b ≤ c
hz_symm : 0 ≠ b * c
⊢ b ≤ c
[PROOFSTEP]
assumption'
[GOAL]
case refine'_2.inr.inr.inr.hbc
a b✝ : Cardinal.{u}
n m : ℕ
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this :
  ∀ {a : Cardinal.{u}} {b : Cardinal.{u}} {n m : ℕ},
    ℵ₀ ≤ a → ∀ (b c : Cardinal.{u}), a ∣ b * c → b * c ≠ 0 → c ≤ b → a ∣ b ∨ a ∣ c
h : ¬c ≤ b
h✝ : b ≤ c
hz_symm : 0 ≠ b * c
⊢ a ∣ c * b
case refine'_2.inr.inr.inr.hz
a b✝ : Cardinal.{u}
n m : ℕ
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this :
  ∀ {a : Cardinal.{u}} {b : Cardinal.{u}} {n m : ℕ},
    ℵ₀ ≤ a → ∀ (b c : Cardinal.{u}), a ∣ b * c → b * c ≠ 0 → c ≤ b → a ∣ b ∨ a ∣ c
h : ¬c ≤ b
h✝ : b ≤ c
hz_symm : 0 ≠ b * c
⊢ c * b ≠ 0
[PROOFSTEP]
all_goals rwa [mul_comm]
[GOAL]
case refine'_2.inr.inr.inr.hbc
a b✝ : Cardinal.{u}
n m : ℕ
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this :
  ∀ {a : Cardinal.{u}} {b : Cardinal.{u}} {n m : ℕ},
    ℵ₀ ≤ a → ∀ (b c : Cardinal.{u}), a ∣ b * c → b * c ≠ 0 → c ≤ b → a ∣ b ∨ a ∣ c
h : ¬c ≤ b
h✝ : b ≤ c
hz_symm : 0 ≠ b * c
⊢ a ∣ c * b
[PROOFSTEP]
rwa [mul_comm]
[GOAL]
case refine'_2.inr.inr.inr.hz
a b✝ : Cardinal.{u}
n m : ℕ
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this :
  ∀ {a : Cardinal.{u}} {b : Cardinal.{u}} {n m : ℕ},
    ℵ₀ ≤ a → ∀ (b c : Cardinal.{u}), a ∣ b * c → b * c ≠ 0 → c ≤ b → a ∣ b ∨ a ∣ c
h : ¬c ≤ b
h✝ : b ≤ c
hz_symm : 0 ≠ b * c
⊢ c * b ≠ 0
[PROOFSTEP]
rwa [mul_comm]
[GOAL]
a✝ a b✝ : Cardinal.{u}
n m : ℕ
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
h : c ≤ b
⊢ a ∣ b ∨ a ∣ c
[PROOFSTEP]
left
[GOAL]
case h
a✝ a b✝ : Cardinal.{u}
n m : ℕ
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
h : c ≤ b
⊢ a ∣ b
[PROOFSTEP]
have habc := le_of_dvd hz hbc
[GOAL]
case h
a✝ a b✝ : Cardinal.{u}
n m : ℕ
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
h : c ≤ b
habc : a ≤ b * c
⊢ a ∣ b
[PROOFSTEP]
rwa [mul_eq_max' <| ha.trans <| habc, max_def', if_pos h] at hbc
[GOAL]
a b : Cardinal.{u}
n m : ℕ
ha : ℵ₀ ≤ a
⊢ ¬Irreducible a
[PROOFSTEP]
rw [irreducible_iff, not_and_or]
[GOAL]
a b : Cardinal.{u}
n m : ℕ
ha : ℵ₀ ≤ a
⊢ ¬¬IsUnit a ∨ ¬∀ (a_1 b : Cardinal.{u}), a = a_1 * b → IsUnit a_1 ∨ IsUnit b
[PROOFSTEP]
refine' Or.inr fun h => _
[GOAL]
a b : Cardinal.{u}
n m : ℕ
ha : ℵ₀ ≤ a
h : ∀ (a_1 b : Cardinal.{u}), a = a_1 * b → IsUnit a_1 ∨ IsUnit b
⊢ False
[PROOFSTEP]
simpa [mul_aleph0_eq ha, isUnit_iff, (one_lt_aleph0.trans_le ha).ne', one_lt_aleph0.ne'] using h a ℵ₀
[GOAL]
a b : Cardinal.{u}
n m : ℕ
⊢ ↑n ∣ ↑m ↔ n ∣ m
[PROOFSTEP]
refine' ⟨_, fun ⟨h, ht⟩ => ⟨h, by exact_mod_cast ht⟩⟩
[GOAL]
a b : Cardinal.{u}
n m : ℕ
x✝ : n ∣ m
h : ℕ
ht : m = n * h
⊢ ↑m = ↑n * ↑h
[PROOFSTEP]
exact_mod_cast ht
[GOAL]
a b : Cardinal.{u}
n m : ℕ
⊢ ↑n ∣ ↑m → n ∣ m
[PROOFSTEP]
rintro ⟨k, hk⟩
[GOAL]
case intro
a b : Cardinal.{u}
n m : ℕ
k : Cardinal.{u_1}
hk : ↑m = ↑n * k
⊢ n ∣ m
[PROOFSTEP]
have : ↑m < ℵ₀ := nat_lt_aleph0 m
[GOAL]
case intro
a b : Cardinal.{u}
n m : ℕ
k : Cardinal.{u_1}
hk : ↑m = ↑n * k
this : ↑m < ℵ₀
⊢ n ∣ m
[PROOFSTEP]
rw [hk, mul_lt_aleph0_iff] at this
[GOAL]
case intro
a b : Cardinal.{u}
n m : ℕ
k : Cardinal.{u_1}
hk : ↑m = ↑n * k
this : ↑n = 0 ∨ k = 0 ∨ ↑n < ℵ₀ ∧ k < ℵ₀
⊢ n ∣ m
[PROOFSTEP]
rcases this with (h | h | ⟨-, hk'⟩)
[GOAL]
case intro.inl
a b : Cardinal.{u}
n m : ℕ
k : Cardinal.{u_1}
hk : ↑m = ↑n * k
h : ↑n = 0
⊢ n ∣ m
case intro.inr.inl
a b : Cardinal.{u}
n m : ℕ
k : Cardinal.{u_1}
hk : ↑m = ↑n * k
h : k = 0
⊢ n ∣ m
case intro.inr.inr.intro a b : Cardinal.{u} n m : ℕ k : Cardinal.{u_1} hk : ↑m = ↑n * k hk' : k < ℵ₀ ⊢ n ∣ m
[PROOFSTEP]
iterate 2 simp only [h, mul_zero, zero_mul, Nat.cast_eq_zero] at hk ; simp [hk]
[GOAL]
case intro.inl
a b : Cardinal.{u}
n m : ℕ
k : Cardinal.{u_1}
hk : ↑m = ↑n * k
h : ↑n = 0
⊢ n ∣ m
case intro.inr.inl
a b : Cardinal.{u}
n m : ℕ
k : Cardinal.{u_1}
hk : ↑m = ↑n * k
h : k = 0
⊢ n ∣ m
case intro.inr.inr.intro a b : Cardinal.{u} n m : ℕ k : Cardinal.{u_1} hk : ↑m = ↑n * k hk' : k < ℵ₀ ⊢ n ∣ m
[PROOFSTEP]
simp only [h, mul_zero, zero_mul, Nat.cast_eq_zero] at hk
[GOAL]
case intro.inl
a b : Cardinal.{u}
n m : ℕ
k : Cardinal.{u_1}
h : ↑n = 0
hk : m = 0
⊢ n ∣ m
case intro.inr.inl
a b : Cardinal.{u}
n m : ℕ
k : Cardinal.{u_1}
hk : ↑m = ↑n * k
h : k = 0
⊢ n ∣ m
case intro.inr.inr.intro a b : Cardinal.{u} n m : ℕ k : Cardinal.{u_1} hk : ↑m = ↑n * k hk' : k < ℵ₀ ⊢ n ∣ m
[PROOFSTEP]
simp [hk]
[GOAL]
case intro.inr.inl
a b : Cardinal.{u}
n m : ℕ
k : Cardinal.{u_1}
hk : ↑m = ↑n * k
h : k = 0
⊢ n ∣ m
case intro.inr.inr.intro a b : Cardinal.{u} n m : ℕ k : Cardinal.{u_1} hk : ↑m = ↑n * k hk' : k < ℵ₀ ⊢ n ∣ m
[PROOFSTEP]
simp only [h, mul_zero, zero_mul, Nat.cast_eq_zero] at hk
[GOAL]
case intro.inr.inl
a b : Cardinal.{u}
n m : ℕ
k : Cardinal.{u_1}
h : k = 0
hk : m = 0
⊢ n ∣ m
case intro.inr.inr.intro a b : Cardinal.{u} n m : ℕ k : Cardinal.{u_1} hk : ↑m = ↑n * k hk' : k < ℵ₀ ⊢ n ∣ m
[PROOFSTEP]
simp [hk]
[GOAL]
case intro.inr.inr.intro
a b : Cardinal.{u}
n m : ℕ
k : Cardinal.{u_1}
hk : ↑m = ↑n * k
hk' : k < ℵ₀
⊢ n ∣ m
[PROOFSTEP]
lift k to ℕ using hk'
[GOAL]
case intro.inr.inr.intro.intro
a b : Cardinal.{u}
n m k : ℕ
hk : ↑m = ↑n * ↑k
⊢ n ∣ m
[PROOFSTEP]
exact ⟨k, by exact_mod_cast hk⟩
[GOAL]
a b : Cardinal.{u}
n m k : ℕ
hk : ↑m = ↑n * ↑k
⊢ m = n * k
[PROOFSTEP]
exact_mod_cast hk
[GOAL]
a b : Cardinal.{u}
n m : ℕ
⊢ Prime ↑n ↔ Nat.Prime n
[PROOFSTEP]
simp only [Prime, Nat.prime_iff]
[GOAL]
a b : Cardinal.{u}
n m : ℕ
⊢ (↑n ≠ 0 ∧ ¬IsUnit ↑n ∧ ∀ (a b : Cardinal.{u_1}), ↑n ∣ a * b → ↑n ∣ a ∨ ↑n ∣ b) ↔
    n ≠ 0 ∧ ¬IsUnit n ∧ ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
[PROOFSTEP]
refine' and_congr (by simp) (and_congr _ ⟨fun h b c hbc => _, fun h b c hbc => _⟩)
[GOAL]
a b : Cardinal.{u}
n m : ℕ
⊢ ↑n ≠ 0 ↔ n ≠ 0
[PROOFSTEP]
simp
[GOAL]
case refine'_1
a b : Cardinal.{u}
n m : ℕ
⊢ ¬IsUnit ↑n ↔ ¬IsUnit n
[PROOFSTEP]
simp only [isUnit_iff, Nat.isUnit_iff]
[GOAL]
case refine'_1
a b : Cardinal.{u}
n m : ℕ
⊢ ¬↑n = 1 ↔ ¬n = 1
[PROOFSTEP]
exact_mod_cast Iff.rfl
[GOAL]
case refine'_2
a b✝ : Cardinal.{u}
n m : ℕ
h : ∀ (a b : Cardinal.{u_1}), ↑n ∣ a * b → ↑n ∣ a ∨ ↑n ∣ b
b c : ℕ
hbc : n ∣ b * c
⊢ n ∣ b ∨ n ∣ c
[PROOFSTEP]
exact_mod_cast h b c (by exact_mod_cast hbc)
[GOAL]
a b✝ : Cardinal.{u}
n m : ℕ
h : ∀ (a b : Cardinal.{u_1}), ↑n ∣ a * b → ↑n ∣ a ∨ ↑n ∣ b
b c : ℕ
hbc : n ∣ b * c
⊢ ↑n ∣ ↑b * ↑c
[PROOFSTEP]
exact_mod_cast hbc
[GOAL]
case refine'_3
a b✝ : Cardinal.{u}
n m : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
⊢ ↑n ∣ b ∨ ↑n ∣ c
[PROOFSTEP]
cases' lt_or_le (b * c) ℵ₀ with h' h'
[GOAL]
case refine'_3.inl
a b✝ : Cardinal.{u}
n m : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
h' : b * c < ℵ₀
⊢ ↑n ∣ b ∨ ↑n ∣ c
[PROOFSTEP]
rcases mul_lt_aleph0_iff.mp h' with (rfl | rfl | ⟨hb, hc⟩)
[GOAL]
case refine'_3.inl.inl
a b : Cardinal.{u}
n m : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
c : Cardinal.{u_1}
hbc : ↑n ∣ 0 * c
h' : 0 * c < ℵ₀
⊢ ↑n ∣ 0 ∨ ↑n ∣ c
[PROOFSTEP]
simp
[GOAL]
case refine'_3.inl.inr.inl
a b✝ : Cardinal.{u}
n m : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b : Cardinal.{u_1}
hbc : ↑n ∣ b * 0
h' : b * 0 < ℵ₀
⊢ ↑n ∣ b ∨ ↑n ∣ 0
[PROOFSTEP]
simp
[GOAL]
case refine'_3.inl.inr.inr.intro
a b✝ : Cardinal.{u}
n m : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
h' : b * c < ℵ₀
hb : b < ℵ₀
hc : c < ℵ₀
⊢ ↑n ∣ b ∨ ↑n ∣ c
[PROOFSTEP]
lift b to ℕ using hb
[GOAL]
case refine'_3.inl.inr.inr.intro.intro
a b✝ : Cardinal.{u}
n m : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
c : Cardinal.{u_1}
hc : c < ℵ₀
b : ℕ
hbc : ↑n ∣ ↑b * c
h' : ↑b * c < ℵ₀
⊢ ↑n ∣ ↑b ∨ ↑n ∣ c
[PROOFSTEP]
lift c to ℕ using hc
[GOAL]
case refine'_3.inl.inr.inr.intro.intro.intro
a b✝ : Cardinal.{u}
n m : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : ℕ
hbc : ↑n ∣ ↑b * ↑c
h' : ↑b * ↑c < ℵ₀
⊢ ↑n ∣ ↑b ∨ ↑n ∣ ↑c
[PROOFSTEP]
exact_mod_cast h b c (by exact_mod_cast hbc)
[GOAL]
a b✝ : Cardinal.{u}
n m : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : ℕ
hbc : ↑n ∣ ↑b * ↑c
h' : ↑b * ↑c < ℵ₀
⊢ n ∣ b * c
[PROOFSTEP]
exact_mod_cast hbc
[GOAL]
case refine'_3.inr
a b✝ : Cardinal.{u}
n m : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
h' : ℵ₀ ≤ b * c
⊢ ↑n ∣ b ∨ ↑n ∣ c
[PROOFSTEP]
rcases aleph0_le_mul_iff.mp h' with ⟨hb, hc, hℵ₀⟩
[GOAL]
case refine'_3.inr.intro.intro
a b✝ : Cardinal.{u}
n m : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
⊢ ↑n ∣ b ∨ ↑n ∣ c
[PROOFSTEP]
have hn : (n : Cardinal) ≠ 0 := by
  intro h
  rw [h, zero_dvd_iff, mul_eq_zero] at hbc
  cases hbc <;> contradiction
[GOAL]
a b✝ : Cardinal.{u}
n m : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
⊢ ↑n ≠ 0
[PROOFSTEP]
intro h
[GOAL]
a b✝ : Cardinal.{u}
n m : ℕ
h✝ : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
h : ↑n = 0
⊢ False
[PROOFSTEP]
rw [h, zero_dvd_iff, mul_eq_zero] at hbc
[GOAL]
a b✝ : Cardinal.{u}
n m : ℕ
h✝ : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : b = 0 ∨ c = 0
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
h : ↑n = 0
⊢ False
[PROOFSTEP]
cases hbc
[GOAL]
case inl
a b✝ : Cardinal.{u}
n m : ℕ
h✝¹ : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
h : ↑n = 0
h✝ : b = 0
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
case inr
a b✝ : Cardinal.{u}
n m : ℕ
h✝¹ : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
h : ↑n = 0
h✝ : c = 0
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
case refine'_3.inr.intro.intro
a b✝ : Cardinal.{u}
n m : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
hn : ↑n ≠ 0
⊢ ↑n ∣ b ∨ ↑n ∣ c
[PROOFSTEP]
wlog hℵ₀b : ℵ₀ ≤ b
[GOAL]
case refine'_3.inr.intro.intro.inr
a b✝ : Cardinal.{u}
n m : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
hn : ↑n ≠ 0
this :
  ∀ {a b : Cardinal.{u}} {n : ℕ} {m : ℕ},
    (∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b) →
      ∀ (b c : Cardinal.{u_1}),
        ↑n ∣ b * c → ℵ₀ ≤ b * c → b ≠ 0 → c ≠ 0 → ℵ₀ ≤ b ∨ ℵ₀ ≤ c → ↑n ≠ 0 → ℵ₀ ≤ b → ↑n ∣ b ∨ ↑n ∣ c
hℵ₀b : ¬ℵ₀ ≤ b
⊢ ↑n ∣ b ∨ ↑n ∣ c
[PROOFSTEP]
refine' (this h c b _ _ hc hb hℵ₀.symm hn (hℵ₀.resolve_left hℵ₀b)).symm
[GOAL]
case refine'_3.inr.intro.intro.inr.refine'_1
a b✝ : Cardinal.{u}
n m : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
hn : ↑n ≠ 0
this :
  ∀ {a b : Cardinal.{u}} {n : ℕ} {m : ℕ},
    (∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b) →
      ∀ (b c : Cardinal.{u_1}),
        ↑n ∣ b * c → ℵ₀ ≤ b * c → b ≠ 0 → c ≠ 0 → ℵ₀ ≤ b ∨ ℵ₀ ≤ c → ↑n ≠ 0 → ℵ₀ ≤ b → ↑n ∣ b ∨ ↑n ∣ c
hℵ₀b : ¬ℵ₀ ≤ b
⊢ Cardinal.{u}
[PROOFSTEP]
try assumption
[GOAL]
case refine'_3.inr.intro.intro.inr.refine'_1
a b✝ : Cardinal.{u}
n m : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
hn : ↑n ≠ 0
this :
  ∀ {a b : Cardinal.{u}} {n : ℕ} {m : ℕ},
    (∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b) →
      ∀ (b c : Cardinal.{u_1}),
        ↑n ∣ b * c → ℵ₀ ≤ b * c → b ≠ 0 → c ≠ 0 → ℵ₀ ≤ b ∨ ℵ₀ ≤ c → ↑n ≠ 0 → ℵ₀ ≤ b → ↑n ∣ b ∨ ↑n ∣ c
hℵ₀b : ¬ℵ₀ ≤ b
⊢ Cardinal.{u}
[PROOFSTEP]
assumption
[GOAL]
case refine'_3.inr.intro.intro.inr.refine'_2
a b✝ : Cardinal.{u}
n m : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
hn : ↑n ≠ 0
this :
  ∀ {a b : Cardinal.{u}} {n : ℕ} {m : ℕ},
    (∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b) →
      ∀ (b c : Cardinal.{u_1}),
        ↑n ∣ b * c → ℵ₀ ≤ b * c → b ≠ 0 → c ≠ 0 → ℵ₀ ≤ b ∨ ℵ₀ ≤ c → ↑n ≠ 0 → ℵ₀ ≤ b → ↑n ∣ b ∨ ↑n ∣ c
hℵ₀b : ¬ℵ₀ ≤ b
⊢ Cardinal.{u}
[PROOFSTEP]
try assumption
[GOAL]
case refine'_3.inr.intro.intro.inr.refine'_2
a b✝ : Cardinal.{u}
n m : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
hn : ↑n ≠ 0
this :
  ∀ {a b : Cardinal.{u}} {n : ℕ} {m : ℕ},
    (∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b) →
      ∀ (b c : Cardinal.{u_1}),
        ↑n ∣ b * c → ℵ₀ ≤ b * c → b ≠ 0 → c ≠ 0 → ℵ₀ ≤ b ∨ ℵ₀ ≤ c → ↑n ≠ 0 → ℵ₀ ≤ b → ↑n ∣ b ∨ ↑n ∣ c
hℵ₀b : ¬ℵ₀ ≤ b
⊢ Cardinal.{u}
[PROOFSTEP]
assumption
[GOAL]
case refine'_3.inr.intro.intro.inr.refine'_3
a b✝ : Cardinal.{u}
n m : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
hn : ↑n ≠ 0
this :
  ∀ {a b : Cardinal.{u}} {n : ℕ} {m : ℕ},
    (∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b) →
      ∀ (b c : Cardinal.{u_1}),
        ↑n ∣ b * c → ℵ₀ ≤ b * c → b ≠ 0 → c ≠ 0 → ℵ₀ ≤ b ∨ ℵ₀ ≤ c → ↑n ≠ 0 → ℵ₀ ≤ b → ↑n ∣ b ∨ ↑n ∣ c
hℵ₀b : ¬ℵ₀ ≤ b
⊢ ℕ
[PROOFSTEP]
try assumption
[GOAL]
case refine'_3.inr.intro.intro.inr.refine'_3
a b✝ : Cardinal.{u}
n m : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
hn : ↑n ≠ 0
this :
  ∀ {a b : Cardinal.{u}} {n : ℕ} {m : ℕ},
    (∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b) →
      ∀ (b c : Cardinal.{u_1}),
        ↑n ∣ b * c → ℵ₀ ≤ b * c → b ≠ 0 → c ≠ 0 → ℵ₀ ≤ b ∨ ℵ₀ ≤ c → ↑n ≠ 0 → ℵ₀ ≤ b → ↑n ∣ b ∨ ↑n ∣ c
hℵ₀b : ¬ℵ₀ ≤ b
⊢ ℕ
[PROOFSTEP]
assumption
[GOAL]
case refine'_3.inr.intro.intro.inr.refine'_4
a b✝ : Cardinal.{u}
n m : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
hn : ↑n ≠ 0
this :
  ∀ {a b : Cardinal.{u}} {n : ℕ} {m : ℕ},
    (∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b) →
      ∀ (b c : Cardinal.{u_1}),
        ↑n ∣ b * c → ℵ₀ ≤ b * c → b ≠ 0 → c ≠ 0 → ℵ₀ ≤ b ∨ ℵ₀ ≤ c → ↑n ≠ 0 → ℵ₀ ≤ b → ↑n ∣ b ∨ ↑n ∣ c
hℵ₀b : ¬ℵ₀ ≤ b
⊢ ↑n ∣ c * b
[PROOFSTEP]
try assumption
[GOAL]
case refine'_3.inr.intro.intro.inr.refine'_4
a b✝ : Cardinal.{u}
n m : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
hn : ↑n ≠ 0
this :
  ∀ {a b : Cardinal.{u}} {n : ℕ} {m : ℕ},
    (∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b) →
      ∀ (b c : Cardinal.{u_1}),
        ↑n ∣ b * c → ℵ₀ ≤ b * c → b ≠ 0 → c ≠ 0 → ℵ₀ ≤ b ∨ ℵ₀ ≤ c → ↑n ≠ 0 → ℵ₀ ≤ b → ↑n ∣ b ∨ ↑n ∣ c
hℵ₀b : ¬ℵ₀ ≤ b
⊢ ↑n ∣ c * b
[PROOFSTEP]
assumption
[GOAL]
case refine'_3.inr.intro.intro.inr.refine'_5
a b✝ : Cardinal.{u}
n m : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
hn : ↑n ≠ 0
this :
  ∀ {a b : Cardinal.{u}} {n : ℕ} {m : ℕ},
    (∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b) →
      ∀ (b c : Cardinal.{u_1}),
        ↑n ∣ b * c → ℵ₀ ≤ b * c → b ≠ 0 → c ≠ 0 → ℵ₀ ≤ b ∨ ℵ₀ ≤ c → ↑n ≠ 0 → ℵ₀ ≤ b → ↑n ∣ b ∨ ↑n ∣ c
hℵ₀b : ¬ℵ₀ ≤ b
⊢ ℵ₀ ≤ c * b
[PROOFSTEP]
try assumption
[GOAL]
case refine'_3.inr.intro.intro.inr.refine'_5
a b✝ : Cardinal.{u}
n m : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
hn : ↑n ≠ 0
this :
  ∀ {a b : Cardinal.{u}} {n : ℕ} {m : ℕ},
    (∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b) →
      ∀ (b c : Cardinal.{u_1}),
        ↑n ∣ b * c → ℵ₀ ≤ b * c → b ≠ 0 → c ≠ 0 → ℵ₀ ≤ b ∨ ℵ₀ ≤ c → ↑n ≠ 0 → ℵ₀ ≤ b → ↑n ∣ b ∨ ↑n ∣ c
hℵ₀b : ¬ℵ₀ ≤ b
⊢ ℵ₀ ≤ c * b
[PROOFSTEP]
assumption
[GOAL]
case refine'_3.inr.intro.intro.inr.refine'_4
a b✝ : Cardinal.{u}
n m : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
hn : ↑n ≠ 0
this :
  ∀ {a b : Cardinal.{u}} {n : ℕ} {m : ℕ},
    (∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b) →
      ∀ (b c : Cardinal.{u_1}),
        ↑n ∣ b * c → ℵ₀ ≤ b * c → b ≠ 0 → c ≠ 0 → ℵ₀ ≤ b ∨ ℵ₀ ≤ c → ↑n ≠ 0 → ℵ₀ ≤ b → ↑n ∣ b ∨ ↑n ∣ c
hℵ₀b : ¬ℵ₀ ≤ b
⊢ ↑n ∣ c * b
case refine'_3.inr.intro.intro.inr.refine'_5
a b✝ : Cardinal.{u}
n m : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
hn : ↑n ≠ 0
this :
  ∀ {a b : Cardinal.{u}} {n : ℕ} {m : ℕ},
    (∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b) →
      ∀ (b c : Cardinal.{u_1}),
        ↑n ∣ b * c → ℵ₀ ≤ b * c → b ≠ 0 → c ≠ 0 → ℵ₀ ≤ b ∨ ℵ₀ ≤ c → ↑n ≠ 0 → ℵ₀ ≤ b → ↑n ∣ b ∨ ↑n ∣ c
hℵ₀b : ¬ℵ₀ ≤ b
⊢ ℵ₀ ≤ c * b
n✝ : ℕ
a b✝ : Cardinal.{u}
n m : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
hn : ↑n ≠ 0
hℵ₀b : ℵ₀ ≤ b
⊢ ↑n ∣ b ∨ ↑n ∣ c
[PROOFSTEP]
rwa [mul_comm] at hbc
[GOAL]
case refine'_3.inr.intro.intro.inr.refine'_5
a b✝ : Cardinal.{u}
n m : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
hn : ↑n ≠ 0
this :
  ∀ {a b : Cardinal.{u}} {n : ℕ} {m : ℕ},
    (∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b) →
      ∀ (b c : Cardinal.{u_1}),
        ↑n ∣ b * c → ℵ₀ ≤ b * c → b ≠ 0 → c ≠ 0 → ℵ₀ ≤ b ∨ ℵ₀ ≤ c → ↑n ≠ 0 → ℵ₀ ≤ b → ↑n ∣ b ∨ ↑n ∣ c
hℵ₀b : ¬ℵ₀ ≤ b
⊢ ℵ₀ ≤ c * b
n✝ : ℕ
a b✝ : Cardinal.{u}
n m : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
hn : ↑n ≠ 0
hℵ₀b : ℵ₀ ≤ b
⊢ ↑n ∣ b ∨ ↑n ∣ c
[PROOFSTEP]
rwa [mul_comm] at h'
[GOAL]
n✝ : ℕ
a b✝ : Cardinal.{u}
n m : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
hn : ↑n ≠ 0
hℵ₀b : ℵ₀ ≤ b
⊢ ↑n ∣ b ∨ ↑n ∣ c
[PROOFSTEP]
exact Or.inl (dvd_of_le_of_aleph0_le hn ((nat_lt_aleph0 n).le.trans hℵ₀b) hℵ₀b)
[GOAL]
a✝ b : Cardinal.{u}
n m : ℕ
a : Cardinal.{u_1}
⊢ Prime a ↔ ℵ₀ ≤ a ∨ ∃ p, a = ↑p ∧ Nat.Prime p
[PROOFSTEP]
cases' le_or_lt ℵ₀ a with h h
[GOAL]
case inl
a✝ b : Cardinal.{u}
n m : ℕ
a : Cardinal.{u_1}
h : ℵ₀ ≤ a
⊢ Prime a ↔ ℵ₀ ≤ a ∨ ∃ p, a = ↑p ∧ Nat.Prime p
[PROOFSTEP]
simp [h]
[GOAL]
case inr
a✝ b : Cardinal.{u}
n m : ℕ
a : Cardinal.{u_1}
h : a < ℵ₀
⊢ Prime a ↔ ℵ₀ ≤ a ∨ ∃ p, a = ↑p ∧ Nat.Prime p
[PROOFSTEP]
lift a to ℕ using id h
[GOAL]
case inr.intro
a✝ b : Cardinal.{u}
n m a : ℕ
h : ↑a < ℵ₀
⊢ Prime ↑a ↔ ℵ₀ ≤ ↑a ∨ ∃ p, ↑a = ↑p ∧ Nat.Prime p
[PROOFSTEP]
simp [not_le.mpr h]
[GOAL]
a✝ b : Cardinal.{u}
n m : ℕ
a : Cardinal.{u_1}
⊢ IsPrimePow a ↔ ℵ₀ ≤ a ∨ ∃ n, a = ↑n ∧ IsPrimePow n
[PROOFSTEP]
by_cases h : ℵ₀ ≤ a
[GOAL]
case pos
a✝ b : Cardinal.{u}
n m : ℕ
a : Cardinal.{u_1}
h : ℵ₀ ≤ a
⊢ IsPrimePow a ↔ ℵ₀ ≤ a ∨ ∃ n, a = ↑n ∧ IsPrimePow n
[PROOFSTEP]
simp [h, (prime_of_aleph0_le h).isPrimePow]
[GOAL]
case neg
a✝ b : Cardinal.{u}
n m : ℕ
a : Cardinal.{u_1}
h : ¬ℵ₀ ≤ a
⊢ IsPrimePow a ↔ ℵ₀ ≤ a ∨ ∃ n, a = ↑n ∧ IsPrimePow n
[PROOFSTEP]
simp only [h, Nat.cast_inj, exists_eq_left', false_or_iff, isPrimePow_nat_iff]
[GOAL]
case neg
a✝ b : Cardinal.{u}
n m : ℕ
a : Cardinal.{u_1}
h : ¬ℵ₀ ≤ a
⊢ IsPrimePow a ↔ ∃ n, a = ↑n ∧ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
[PROOFSTEP]
lift a to ℕ using not_le.mp h
[GOAL]
case neg.intro
a✝ b : Cardinal.{u}
n m a : ℕ
h : ¬ℵ₀ ≤ ↑a
⊢ IsPrimePow ↑a ↔ ∃ n, ↑a = ↑n ∧ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
[PROOFSTEP]
rw [isPrimePow_def]
[GOAL]
case neg.intro
a✝ b : Cardinal.{u}
n m a : ℕ
h : ¬ℵ₀ ≤ ↑a
⊢ (∃ p k, Prime p ∧ 0 < k ∧ p ^ k = ↑a) ↔ ∃ n, ↑a = ↑n ∧ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
[PROOFSTEP]
refine' ⟨_, fun ⟨n, han, p, k, hp, hk, h⟩ => ⟨p, k, nat_is_prime_iff.2 hp, hk, by rw [han]; exact_mod_cast h⟩⟩
[GOAL]
a✝ b : Cardinal.{u}
n✝ m a : ℕ
h✝ : ¬ℵ₀ ≤ ↑a
x✝ : ∃ n, ↑a = ↑n ∧ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
n : ℕ
han : ↑a = ↑n
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
h : p ^ k = n
⊢ ↑p ^ k = ↑a
[PROOFSTEP]
rw [han]
[GOAL]
a✝ b : Cardinal.{u}
n✝ m a : ℕ
h✝ : ¬ℵ₀ ≤ ↑a
x✝ : ∃ n, ↑a = ↑n ∧ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
n : ℕ
han : ↑a = ↑n
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
h : p ^ k = n
⊢ ↑p ^ k = ↑n
[PROOFSTEP]
exact_mod_cast h
[GOAL]
case neg.intro
a✝ b : Cardinal.{u}
n m a : ℕ
h : ¬ℵ₀ ≤ ↑a
⊢ (∃ p k, Prime p ∧ 0 < k ∧ p ^ k = ↑a) → ∃ n, ↑a = ↑n ∧ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
[PROOFSTEP]
rintro ⟨p, k, hp, hk, hpk⟩
[GOAL]
case neg.intro.intro.intro.intro.intro
a✝ b : Cardinal.{u}
n m a : ℕ
h : ¬ℵ₀ ≤ ↑a
p : Cardinal.{u_1}
k : ℕ
hp : Prime p
hk : 0 < k
hpk : p ^ k = ↑a
⊢ ∃ n, ↑a = ↑n ∧ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
[PROOFSTEP]
have key : p ^ 1 ≤ ↑a := by rw [← hpk]; apply power_le_power_left hp.ne_zero; exact_mod_cast hk
[GOAL]
a✝ b : Cardinal.{u}
n m a : ℕ
h : ¬ℵ₀ ≤ ↑a
p : Cardinal.{u_1}
k : ℕ
hp : Prime p
hk : 0 < k
hpk : p ^ k = ↑a
⊢ p ^ 1 ≤ ↑a
[PROOFSTEP]
rw [← hpk]
[GOAL]
a✝ b : Cardinal.{u}
n m a : ℕ
h : ¬ℵ₀ ≤ ↑a
p : Cardinal.{u_1}
k : ℕ
hp : Prime p
hk : 0 < k
hpk : p ^ k = ↑a
⊢ p ^ 1 ≤ p ^ k
[PROOFSTEP]
apply power_le_power_left hp.ne_zero
[GOAL]
a✝ b : Cardinal.{u}
n m a : ℕ
h : ¬ℵ₀ ≤ ↑a
p : Cardinal.{u_1}
k : ℕ
hp : Prime p
hk : 0 < k
hpk : p ^ k = ↑a
⊢ 1 ≤ ↑k
[PROOFSTEP]
exact_mod_cast hk
[GOAL]
case neg.intro.intro.intro.intro.intro
a✝ b : Cardinal.{u}
n m a : ℕ
h : ¬ℵ₀ ≤ ↑a
p : Cardinal.{u_1}
k : ℕ
hp : Prime p
hk : 0 < k
hpk : p ^ k = ↑a
key : p ^ 1 ≤ ↑a
⊢ ∃ n, ↑a = ↑n ∧ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
[PROOFSTEP]
rw [power_one] at key
[GOAL]
case neg.intro.intro.intro.intro.intro
a✝ b : Cardinal.{u}
n m a : ℕ
h : ¬ℵ₀ ≤ ↑a
p : Cardinal.{u_1}
k : ℕ
hp : Prime p
hk : 0 < k
hpk : p ^ k = ↑a
key : p ≤ ↑a
⊢ ∃ n, ↑a = ↑n ∧ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
[PROOFSTEP]
lift p to ℕ using key.trans_lt (nat_lt_aleph0 a)
[GOAL]
case neg.intro.intro.intro.intro.intro.intro
a✝ b : Cardinal.{u}
n m a : ℕ
h : ¬ℵ₀ ≤ ↑a
k : ℕ
hk : 0 < k
p : ℕ
hp : Prime ↑p
hpk : ↑p ^ k = ↑a
key : ↑p ≤ ↑a
⊢ ∃ n, ↑a = ↑n ∧ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
[PROOFSTEP]
exact ⟨a, rfl, p, k, nat_is_prime_iff.mp hp, hk, by exact_mod_cast hpk⟩
[GOAL]
a✝ b : Cardinal.{u}
n m a : ℕ
h : ¬ℵ₀ ≤ ↑a
k : ℕ
hk : 0 < k
p : ℕ
hp : Prime ↑p
hpk : ↑p ^ k = ↑a
key : ↑p ≤ ↑a
⊢ p ^ k = a
[PROOFSTEP]
exact_mod_cast hpk