[GOAL]
α : Type u_1
a : Lists α
l : Lists' α true
⊢ toList (cons a l) = a :: toList l
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
l : List (Lists α)
⊢ toList (ofList l) = l
[PROOFSTEP]
induction l
[GOAL]
case nil
α : Type u_1
⊢ toList (ofList []) = []
[PROOFSTEP]
simp [*]
[GOAL]
case cons
α : Type u_1
head✝ : Lists α
tail✝ : List (Lists α)
tail_ih✝ : toList (ofList tail✝) = tail✝
⊢ toList (ofList (head✝ :: tail✝)) = head✝ :: tail✝
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
b : Bool
h : true = b
l : Lists' α b
⊢ Lists' α true
[PROOFSTEP]
rw [h]
[GOAL]
α : Type u_1
b : Bool
h : true = b
l : Lists' α b
⊢ Lists' α b
[PROOFSTEP]
exact l
[GOAL]
α : Type u_1
b : Bool
h : true = b
l : Lists' α b
⊢ let l' := Eq.mpr (_ : Lists' α true = Lists' α b) l;
  ofList (toList l') = l'
[PROOFSTEP]
induction l with
| atom => cases h
| nil => simp
| cons' b a _ IH =>
  intro l'
  simpa [cons] using IH rfl
[GOAL]
α : Type u_1
b : Bool
h : true = b
l : Lists' α b
⊢ let l' := Eq.mpr (_ : Lists' α true = Lists' α b) l;
  ofList (toList l') = l'
[PROOFSTEP]
induction l with
| atom => cases h
| nil => simp
| cons' b a _ IH =>
  intro l'
  simpa [cons] using IH rfl
[GOAL]
case atom
α : Type u_1
b : Bool
a✝ : α
h : true = false
⊢ let l' := Eq.mpr (_ : Lists' α true = Lists' α false) (atom a✝);
  ofList (toList l') = l'
[PROOFSTEP]

| atom => cases h
[GOAL]
case atom
α : Type u_1
b : Bool
a✝ : α
h : true = false
⊢ let l' := Eq.mpr (_ : Lists' α true = Lists' α false) (atom a✝);
  ofList (toList l') = l'
[PROOFSTEP]
cases h
[GOAL]
case nil
α : Type u_1
b : Bool
h : true = true
⊢ let l' := Eq.mpr (_ : Lists' α true = Lists' α true) nil;
  ofList (toList l') = l'
[PROOFSTEP]

| nil => simp
[GOAL]
case nil
α : Type u_1
b : Bool
h : true = true
⊢ let l' := Eq.mpr (_ : Lists' α true = Lists' α true) nil;
  ofList (toList l') = l'
[PROOFSTEP]
simp
[GOAL]
case cons'
α : Type u_1
b✝¹ b✝ : Bool
b : Lists' α b✝
a : Lists' α true
a_ih✝ :
  ∀ (h : true = b✝),
    let l' := Eq.mpr (_ : Lists' α true = Lists' α b✝) b;
    ofList (toList l') = l'
IH :
  ∀ (h : true = true),
    let l' := Eq.mpr (_ : Lists' α true = Lists' α true) a;
    ofList (toList l') = l'
h : true = true
⊢ let l' := Eq.mpr (_ : Lists' α true = Lists' α true) (cons' b a);
  ofList (toList l') = l'
[PROOFSTEP]

| cons' b a _ IH =>
  intro l'
  simpa [cons] using IH rfl
[GOAL]
case cons'
α : Type u_1
b✝¹ b✝ : Bool
b : Lists' α b✝
a : Lists' α true
a_ih✝ :
  ∀ (h : true = b✝),
    let l' := Eq.mpr (_ : Lists' α true = Lists' α b✝) b;
    ofList (toList l') = l'
IH :
  ∀ (h : true = true),
    let l' := Eq.mpr (_ : Lists' α true = Lists' α true) a;
    ofList (toList l') = l'
h : true = true
⊢ let l' := Eq.mpr (_ : Lists' α true = Lists' α true) (cons' b a);
  ofList (toList l') = l'
[PROOFSTEP]
intro l'
[GOAL]
case cons'
α : Type u_1
b✝¹ b✝ : Bool
b : Lists' α b✝
a : Lists' α true
a_ih✝ :
  ∀ (h : true = b✝),
    let l' := Eq.mpr (_ : Lists' α true = Lists' α b✝) b;
    ofList (toList l') = l'
IH :
  ∀ (h : true = true),
    let l' := Eq.mpr (_ : Lists' α true = Lists' α true) a;
    ofList (toList l') = l'
h : true = true
l' : Lists' α true := Eq.mpr (_ : Lists' α true = Lists' α true) (cons' b a)
⊢ ofList (toList l') = l'
[PROOFSTEP]
simpa [cons] using IH rfl
[GOAL]
α : Type u_1
a y : Lists α
l : Lists' α true
⊢ a ∈ cons y l ↔ a ~ y ∨ a ∈ l
[PROOFSTEP]
simp [mem_def, or_and_right, exists_or]
[GOAL]
α : Type u_1
a : Lists α
l₁ l₂ : Lists' α true
⊢ cons a l₁ ⊆ l₂ ↔ a ∈ l₂ ∧ l₁ ⊆ l₂
[PROOFSTEP]
refine' ⟨fun h => _, fun ⟨⟨a', m, e⟩, s⟩ => Subset.cons e m s⟩
[GOAL]
α : Type u_1
a : Lists α
l₁ l₂ : Lists' α true
h : cons a l₁ ⊆ l₂
⊢ a ∈ l₂ ∧ l₁ ⊆ l₂
[PROOFSTEP]
generalize h' : Lists'.cons a l₁ = l₁' at h
[GOAL]
α : Type u_1
a : Lists α
l₁ l₂ l₁' : Lists' α true
h' : cons a l₁ = l₁'
h : l₁' ⊆ l₂
⊢ a ∈ l₂ ∧ l₁ ⊆ l₂
[PROOFSTEP]
cases' h with l a' a'' l l' e m s
[GOAL]
case nil
α : Type u_1
a : Lists α
l₁ l₂ : Lists' α true
h' : cons a l₁ = nil
⊢ a ∈ l₂ ∧ l₁ ⊆ l₂
[PROOFSTEP]
cases a
[GOAL]
case nil.mk
α : Type u_1
l₁ l₂ : Lists' α true
fst✝ : Bool
snd✝ : Lists' α fst✝
h' : cons { fst := fst✝, snd := snd✝ } l₁ = nil
⊢ { fst := fst✝, snd := snd✝ } ∈ l₂ ∧ l₁ ⊆ l₂
[PROOFSTEP]
cases h'
[GOAL]
case cons
α : Type u_1
a : Lists α
l₁ l₂ : Lists' α true
a' a'' : Lists α
l : Lists' α true
e : a' ~ a''
h' : cons a l₁ = cons a' l
m : a'' ∈ toList l₂
s : Subset l l₂
⊢ a ∈ l₂ ∧ l₁ ⊆ l₂
[PROOFSTEP]
cases a
[GOAL]
case cons.mk
α : Type u_1
l₁ l₂ : Lists' α true
a' a'' : Lists α
l : Lists' α true
e : a' ~ a''
m : a'' ∈ toList l₂
s : Subset l l₂
fst✝ : Bool
snd✝ : Lists' α fst✝
h' : cons { fst := fst✝, snd := snd✝ } l₁ = cons a' l
⊢ { fst := fst✝, snd := snd✝ } ∈ l₂ ∧ l₁ ⊆ l₂
[PROOFSTEP]
cases a'
[GOAL]
case cons.mk.mk
α : Type u_1
l₁ l₂ : Lists' α true
a'' : Lists α
l : Lists' α true
m : a'' ∈ toList l₂
s : Subset l l₂
fst✝¹ : Bool
snd✝¹ : Lists' α fst✝¹
fst✝ : Bool
snd✝ : Lists' α fst✝
e : { fst := fst✝, snd := snd✝ } ~ a''
h' : cons { fst := fst✝¹, snd := snd✝¹ } l₁ = cons { fst := fst✝, snd := snd✝ } l
⊢ { fst := fst✝¹, snd := snd✝¹ } ∈ l₂ ∧ l₁ ⊆ l₂
[PROOFSTEP]
cases h'
[GOAL]
case cons.mk.mk.refl
α : Type u_1
l₁ l₂ : Lists' α true
a'' : Lists α
m : a'' ∈ toList l₂
fst✝ : Bool
snd✝ : Lists' α fst✝
e : { fst := fst✝, snd := snd✝ } ~ a''
s : Subset l₁ l₂
⊢ { fst := fst✝, snd := snd✝ } ∈ l₂ ∧ l₁ ⊆ l₂
[PROOFSTEP]
exact ⟨⟨_, m, e⟩, s⟩
[GOAL]
α : Type u_1
l₁ l₂ : List (Lists α)
h : l₁ ⊆ l₂
⊢ ofList l₁ ⊆ ofList l₂
[PROOFSTEP]
induction' l₁ with _ _ l₁_ih
[GOAL]
case nil
α : Type u_1
l₁ l₂ : List (Lists α)
h✝ : l₁ ⊆ l₂
h : [] ⊆ l₂
⊢ ofList [] ⊆ ofList l₂
[PROOFSTEP]
exact Subset.nil
[GOAL]
case cons
α : Type u_1
l₁ l₂ : List (Lists α)
h✝ : l₁ ⊆ l₂
head✝ : Lists α
tail✝ : List (Lists α)
l₁_ih : tail✝ ⊆ l₂ → ofList tail✝ ⊆ ofList l₂
h : head✝ :: tail✝ ⊆ l₂
⊢ ofList (head✝ :: tail✝) ⊆ ofList l₂
[PROOFSTEP]
refine' Subset.cons (Lists.Equiv.refl _) _ (l₁_ih (List.subset_of_cons_subset h))
[GOAL]
case cons
α : Type u_1
l₁ l₂ : List (Lists α)
h✝ : l₁ ⊆ l₂
head✝ : Lists α
tail✝ : List (Lists α)
l₁_ih : tail✝ ⊆ l₂ → ofList tail✝ ⊆ ofList l₂
h : head✝ :: tail✝ ⊆ l₂
⊢ head✝ ∈ toList (ofList l₂)
[PROOFSTEP]
simp at h
[GOAL]
case cons
α : Type u_1
l₁ l₂ : List (Lists α)
h✝ : l₁ ⊆ l₂
head✝ : Lists α
tail✝ : List (Lists α)
l₁_ih : tail✝ ⊆ l₂ → ofList tail✝ ⊆ ofList l₂
h : head✝ ∈ l₂ ∧ tail✝ ⊆ l₂
⊢ head✝ ∈ toList (ofList l₂)
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
l : Lists' α true
⊢ l ⊆ l
[PROOFSTEP]
rw [← Lists'.of_toList l]
[GOAL]
α : Type u_1
l : Lists' α true
⊢ ofList (toList l) ⊆ ofList (toList l)
[PROOFSTEP]
exact ofList_subset (List.Subset.refl _)
[GOAL]
α : Type u_1
l : Lists' α true
⊢ l ⊆ nil → l = nil
[PROOFSTEP]
rw [← of_toList l]
[GOAL]
α : Type u_1
l : Lists' α true
⊢ ofList (toList l) ⊆ nil → ofList (toList l) = nil
[PROOFSTEP]
induction toList l
[GOAL]
case nil
α : Type u_1
l : Lists' α true
⊢ ofList [] ⊆ nil → ofList [] = nil
[PROOFSTEP]
intro h
[GOAL]
case cons
α : Type u_1
l : Lists' α true
head✝ : Lists α
tail✝ : List (Lists α)
tail_ih✝ : ofList tail✝ ⊆ nil → ofList tail✝ = nil
⊢ ofList (head✝ :: tail✝) ⊆ nil → ofList (head✝ :: tail✝) = nil
[PROOFSTEP]
intro h
[GOAL]
case nil
α : Type u_1
l : Lists' α true
h : ofList [] ⊆ nil
⊢ ofList [] = nil
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u_1
l : Lists' α true
head✝ : Lists α
tail✝ : List (Lists α)
tail_ih✝ : ofList tail✝ ⊆ nil → ofList tail✝ = nil
h : ofList (head✝ :: tail✝) ⊆ nil
⊢ ofList (head✝ :: tail✝) = nil
[PROOFSTEP]
rcases cons_subset.1 h with ⟨⟨_, ⟨⟩, _⟩, _⟩
[GOAL]
α : Type u_1
a : Lists α
x✝ : Lists' α true
h : a ∈ toList nil
⊢ a ∈ x✝
[PROOFSTEP]
cases h
[GOAL]
α : Type u_1
a : Lists α
b✝ : Bool
a0 : Lists' α b✝
l0 l₂ : Lists' α true
s : cons' a0 l0 ⊆ l₂
h : a ∈ toList (cons' a0 l0)
⊢ a ∈ l₂
[PROOFSTEP]
cases' s with _ _ _ _ _ e m s
[GOAL]
case cons
α : Type u_1
a : Lists α
l0 l₂ : Lists' α true
a✝ a'✝ : Lists α
e : a✝ ~ a'✝
h : a ∈ toList (cons' a✝.snd l0)
m : a'✝ ∈ toList l₂
s : Subset l0 l₂
⊢ a ∈ l₂
[PROOFSTEP]
simp only [toList, Sigma.eta, List.find?, List.mem_cons] at h
[GOAL]
case cons
α : Type u_1
a : Lists α
l0 l₂ : Lists' α true
a✝ a'✝ : Lists α
e : a✝ ~ a'✝
m : a'✝ ∈ toList l₂
s : Subset l0 l₂
h : a = a✝ ∨ a ∈ toList l0
⊢ a ∈ l₂
[PROOFSTEP]
rcases h with (rfl | h)
[GOAL]
case cons.inl
α : Type u_1
a : Lists α
l0 l₂ : Lists' α true
a'✝ : Lists α
m : a'✝ ∈ toList l₂
s : Subset l0 l₂
e : a ~ a'✝
⊢ a ∈ l₂
[PROOFSTEP]
exact ⟨_, m, e⟩
[GOAL]
case cons.inr
α : Type u_1
a : Lists α
l0 l₂ : Lists' α true
a✝ a'✝ : Lists α
e : a✝ ~ a'✝
m : a'✝ ∈ toList l₂
s : Subset l0 l₂
h : a ∈ toList l0
⊢ a ∈ l₂
[PROOFSTEP]
exact mem_of_subset' s h
[GOAL]
α : Type u_1
l₁ l₂ : Lists' α true
H : ∀ (a : Lists α), a ∈ toList l₁ → a ∈ l₂
⊢ l₁ ⊆ l₂
[PROOFSTEP]
rw [← of_toList l₁]
[GOAL]
α : Type u_1
l₁ l₂ : Lists' α true
H : ∀ (a : Lists α), a ∈ toList l₁ → a ∈ l₂
⊢ ofList (toList l₁) ⊆ l₂
[PROOFSTEP]
revert H
[GOAL]
α : Type u_1
l₁ l₂ : Lists' α true
⊢ (∀ (a : Lists α), a ∈ toList l₁ → a ∈ l₂) → ofList (toList l₁) ⊆ l₂
[PROOFSTEP]
induction' toList l₁ with h t t_ih
[GOAL]
case nil
α : Type u_1
l₁ l₂ : Lists' α true
⊢ (∀ (a : Lists α), a ∈ [] → a ∈ l₂) → ofList [] ⊆ l₂
[PROOFSTEP]
intro H
[GOAL]
case cons
α : Type u_1
l₁ l₂ : Lists' α true
h : Lists α
t : List (Lists α)
t_ih : (∀ (a : Lists α), a ∈ t → a ∈ l₂) → ofList t ⊆ l₂
⊢ (∀ (a : Lists α), a ∈ h :: t → a ∈ l₂) → ofList (h :: t) ⊆ l₂
[PROOFSTEP]
intro H
[GOAL]
case nil
α : Type u_1
l₁ l₂ : Lists' α true
H : ∀ (a : Lists α), a ∈ [] → a ∈ l₂
⊢ ofList [] ⊆ l₂
[PROOFSTEP]
exact Subset.nil
[GOAL]
case cons
α : Type u_1
l₁ l₂ : Lists' α true
h : Lists α
t : List (Lists α)
t_ih : (∀ (a : Lists α), a ∈ t → a ∈ l₂) → ofList t ⊆ l₂
H : ∀ (a : Lists α), a ∈ h :: t → a ∈ l₂
⊢ ofList (h :: t) ⊆ l₂
[PROOFSTEP]
simp only [ofList, List.find?, List.mem_cons, forall_eq_or_imp] at *
[GOAL]
case cons
α : Type u_1
l₁ l₂ : Lists' α true
h : Lists α
t : List (Lists α)
t_ih : (∀ (a : Lists α), a ∈ t → a ∈ l₂) → ofList t ⊆ l₂
H : h ∈ l₂ ∧ ∀ (a : Lists α), a ∈ t → a ∈ l₂
⊢ cons h (ofList t) ⊆ l₂
[PROOFSTEP]
exact cons_subset.2 ⟨H.1, t_ih H.2⟩
[GOAL]
α : Type u_1
l : List (Lists α)
⊢ toList (ofList l) = l
[PROOFSTEP]
simp [ofList, of']
[GOAL]
α : Type u_1
l : Lists' α true
x✝ : IsList { fst := true, snd := l }
⊢ ofList (toList { fst := true, snd := l }) = { fst := true, snd := l }
[PROOFSTEP]
simp_all [ofList, of']
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
⊢ DecidableEq (Lists α)
[PROOFSTEP]
unfold Lists
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
⊢ DecidableEq ((b : Bool) × Lists' α b)
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
inst✝ : SizeOf α
⊢ SizeOf (Lists α)
[PROOFSTEP]
unfold Lists
[GOAL]
α : Type u_1
inst✝ : SizeOf α
⊢ SizeOf ((b : Bool) × Lists' α b)
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
C : Lists α → Sort u_2
D : Lists' α true → Sort u_3
C0 : (a : α) → C (atom a)
C1 : (l : Lists' α true) → D l → C (of' l)
D0 : D Lists'.nil
D1 : (a : Lists α) → (l : Lists' α true) → C a → D l → D (Lists'.cons a l)
⊢ PProd ((l : Lists α) → C l) ((l : Lists' α true) → D l)
[PROOFSTEP]
suffices
  ∀ {b} (l : Lists' α b),
    PProd (C ⟨_, l⟩)
      (match b, l with
      | true, l => D l
      | false, _ => PUnit)
  by exact ⟨fun ⟨b, l⟩ => (this _).1, fun l => (this l).2⟩
[GOAL]
α : Type u_1
C : Lists α → Sort u_2
D : Lists' α true → Sort u_3
C0 : (a : α) → C (atom a)
C1 : (l : Lists' α true) → D l → C (of' l)
D0 : D Lists'.nil
D1 : (a : Lists α) → (l : Lists' α true) → C a → D l → D (Lists'.cons a l)
this :
  {b : Bool} →
    (l : Lists' α b) →
      PProd (C { fst := b, snd := l })
        (match b, l with
        | true, l => D l
        | false, x => PUnit)
⊢ PProd ((l : Lists α) → C l) ((l : Lists' α true) → D l)
[PROOFSTEP]
exact ⟨fun ⟨b, l⟩ => (this _).1, fun l => (this l).2⟩
[GOAL]
α : Type u_1
C : Lists α → Sort u_2
D : Lists' α true → Sort u_3
C0 : (a : α) → C (atom a)
C1 : (l : Lists' α true) → D l → C (of' l)
D0 : D Lists'.nil
D1 : (a : Lists α) → (l : Lists' α true) → C a → D l → D (Lists'.cons a l)
⊢ {b : Bool} →
    (l : Lists' α b) →
      PProd (C { fst := b, snd := l })
        (match b, l with
        | true, l => D l
        | false, x => PUnit)
[PROOFSTEP]
intros b l
[GOAL]
α : Type u_1
C : Lists α → Sort u_2
D : Lists' α true → Sort u_3
C0 : (a : α) → C (atom a)
C1 : (l : Lists' α true) → D l → C (of' l)
D0 : D Lists'.nil
D1 : (a : Lists α) → (l : Lists' α true) → C a → D l → D (Lists'.cons a l)
b : Bool
l : Lists' α b
⊢ PProd (C { fst := b, snd := l })
    (match b, l with
    | true, l => D l
    | false, x => PUnit)
[PROOFSTEP]
induction' l with a b a l IH₁ IH
[GOAL]
case atom
α : Type u_1
C : Lists α → Sort u_2
D : Lists' α true → Sort u_3
C0 : (a : α) → C (atom a)
C1 : (l : Lists' α true) → D l → C (of' l)
D0 : D Lists'.nil
D1 : (a : Lists α) → (l : Lists' α true) → C a → D l → D (Lists'.cons a l)
b : Bool
a : α
⊢ PProd (C { fst := false, snd := Lists'.atom a })
    (match false, Lists'.atom a with
    | true, l => D l
    | false, x => PUnit)
[PROOFSTEP]
exact ⟨C0 _, ⟨⟩⟩
[GOAL]
case nil
α : Type u_1
C : Lists α → Sort u_2
D : Lists' α true → Sort u_3
C0 : (a : α) → C (atom a)
C1 : (l : Lists' α true) → D l → C (of' l)
D0 : D Lists'.nil
D1 : (a : Lists α) → (l : Lists' α true) → C a → D l → D (Lists'.cons a l)
b : Bool
⊢ PProd (C { fst := true, snd := Lists'.nil })
    (match true, Lists'.nil with
    | true, l => D l
    | false, x => PUnit)
[PROOFSTEP]
exact ⟨C1 _ D0, D0⟩
[GOAL]
case cons'
α : Type u_1
C : Lists α → Sort u_2
D : Lists' α true → Sort u_3
C0 : (a : α) → C (atom a)
C1 : (l : Lists' α true) → D l → C (of' l)
D0 : D Lists'.nil
D1 : (a : Lists α) → (l : Lists' α true) → C a → D l → D (Lists'.cons a l)
b✝ b : Bool
a : Lists' α b
l : Lists' α true
IH₁ :
  PProd (C { fst := b, snd := a })
    (match b, a with
    | true, l => D l
    | false, x => PUnit)
IH :
  PProd (C { fst := true, snd := l })
    (match true, l with
    | true, l => D l
    | false, x => PUnit)
⊢ PProd (C { fst := true, snd := Lists'.cons' a l })
    (match true, Lists'.cons' a l with
    | true, l => D l
    | false, x => PUnit)
[PROOFSTEP]
have : D (Lists'.cons' a l) := D1 ⟨_, _⟩ _ IH₁.1 IH.2
[GOAL]
case cons'
α : Type u_1
C : Lists α → Sort u_2
D : Lists' α true → Sort u_3
C0 : (a : α) → C (atom a)
C1 : (l : Lists' α true) → D l → C (of' l)
D0 : D Lists'.nil
D1 : (a : Lists α) → (l : Lists' α true) → C a → D l → D (Lists'.cons a l)
b✝ b : Bool
a : Lists' α b
l : Lists' α true
IH₁ :
  PProd (C { fst := b, snd := a })
    (match b, a with
    | true, l => D l
    | false, x => PUnit)
IH :
  PProd (C { fst := true, snd := l })
    (match true, l with
    | true, l => D l
    | false, x => PUnit)
this : D (Lists'.cons' a l)
⊢ PProd (C { fst := true, snd := Lists'.cons' a l })
    (match true, Lists'.cons' a l with
    | true, l => D l
    | false, x => PUnit)
[PROOFSTEP]
exact ⟨C1 _ this, this⟩
[GOAL]
α : Type u_1
l₁ l₂ : Lists' α true
⊢ of' l₁ ~ of' l₂ ↔ l₁ ⊆ l₂ ∧ l₂ ⊆ l₁
[PROOFSTEP]
refine' ⟨fun h => _, fun ⟨h₁, h₂⟩ => Equiv.antisymm h₁ h₂⟩
[GOAL]
α : Type u_1
l₁ l₂ : Lists' α true
h : of' l₁ ~ of' l₂
⊢ l₁ ⊆ l₂ ∧ l₂ ⊆ l₁
[PROOFSTEP]
cases' h with _ _ _ h₁ h₂
[GOAL]
case refl
α : Type u_1
l₁ : Lists' α true
⊢ l₁ ⊆ l₁ ∧ l₁ ⊆ l₁
[PROOFSTEP]
simp [Lists'.Subset.refl]
[GOAL]
case antisymm
α : Type u_1
l₁ l₂ : Lists' α true
h₁ : Lists'.Subset l₁ l₂
h₂ : Lists'.Subset l₂ l₁
⊢ l₁ ⊆ l₂ ∧ l₂ ⊆ l₁
[PROOFSTEP]
exact ⟨h₁, h₂⟩
[GOAL]
α : Type u_1
a : α
l : Lists α
h : atom a ~ l
⊢ atom a = l
[PROOFSTEP]
cases h
[GOAL]
case refl
α : Type u_1
a : α
⊢ atom a = atom a
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
l₁ l₂ : Lists α
h : l₁ ~ l₂
⊢ l₂ ~ l₁
[PROOFSTEP]
cases' h with _ _ _ h₁ h₂ <;> [rfl; exact Equiv.antisymm h₂ h₁]
[GOAL]
α : Type u_1
l₁ l₂ : Lists α
h : l₁ ~ l₂
⊢ l₂ ~ l₁
[PROOFSTEP]
cases' h with _ _ _ h₁ h₂
[GOAL]
case refl
α : Type u_1
l₁ : Lists α
⊢ l₁ ~ l₁
[PROOFSTEP]
rfl
[GOAL]
case antisymm
α : Type u_1
l₁✝ l₂✝ : Lists' α true
h₁ : Lists'.Subset l₁✝ l₂✝
h₂ : Lists'.Subset l₂✝ l₁✝
⊢ { fst := true, snd := l₂✝ } ~ { fst := true, snd := l₁✝ }
[PROOFSTEP]
exact Equiv.antisymm h₂ h₁
[GOAL]
α : Type u_1
⊢ ∀ {l₁ l₂ l₃ : Lists α}, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
[PROOFSTEP]
let trans := fun l₁ : Lists α => ∀ ⦃l₂ l₃⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
[GOAL]
α : Type u_1
trans : Lists α → Prop := fun l₁ => ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
⊢ ∀ {l₁ l₂ l₃ : Lists α}, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
[PROOFSTEP]
suffices PProd (∀ l₁, trans l₁) (∀ (l : Lists' α true), ∀ l' ∈ l.toList, trans l') by exact this.1
[GOAL]
α : Type u_1
trans : Lists α → Prop := fun l₁ => ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
this : PProd (∀ (l₁ : Lists α), trans l₁) (∀ (l : Lists' α true) (l' : Lists α), l' ∈ Lists'.toList l → trans l')
⊢ ∀ {l₁ l₂ l₃ : Lists α}, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
[PROOFSTEP]
exact this.1
[GOAL]
α : Type u_1
trans : Lists α → Prop := fun l₁ => ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
⊢ PProd (∀ (l₁ : Lists α), trans l₁) (∀ (l : Lists' α true) (l' : Lists α), l' ∈ Lists'.toList l → trans l')
[PROOFSTEP]
apply inductionMut
[GOAL]
case C0
α : Type u_1
trans : Lists α → Prop := fun l₁ => ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
⊢ ∀ (a : α), trans (atom a)
[PROOFSTEP]
intro a l₂ l₃ h₁ h₂
[GOAL]
case C0
α : Type u_1
trans : Lists α → Prop := fun l₁ => ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
a : α
l₂ l₃ : Lists α
h₁ : atom a ~ l₂
h₂ : l₂ ~ l₃
⊢ atom a ~ l₃
[PROOFSTEP]
rwa [← equiv_atom.1 h₁] at h₂
[GOAL]
case C1
α : Type u_1
trans : Lists α → Prop := fun l₁ => ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
⊢ ∀ (l : Lists' α true), (∀ (l' : Lists α), l' ∈ Lists'.toList l → trans l') → trans (of' l)
[PROOFSTEP]
intro l₁ IH l₂ l₃ h₁ h₂
[GOAL]
case C1
α : Type u_1
trans : Lists α → Prop := fun l₁ => ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ Lists'.toList l₁ → trans l'
l₂ l₃ : Lists α
h₁ : of' l₁ ~ l₂
h₂ : l₂ ~ l₃
⊢ of' l₁ ~ l₃
[PROOFSTEP]
have h₁' := h₁
[GOAL]
case C1
α : Type u_1
trans : Lists α → Prop := fun l₁ => ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ Lists'.toList l₁ → trans l'
l₂ l₃ : Lists α
h₁ : of' l₁ ~ l₂
h₂ : l₂ ~ l₃
h₁' : of' l₁ ~ l₂
⊢ of' l₁ ~ l₃
[PROOFSTEP]
have h₂' := h₂
[GOAL]
case C1
α : Type u_1
trans : Lists α → Prop := fun l₁ => ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ Lists'.toList l₁ → trans l'
l₂ l₃ : Lists α
h₁ : of' l₁ ~ l₂
h₂ : l₂ ~ l₃
h₁' : of' l₁ ~ l₂
h₂' : l₂ ~ l₃
⊢ of' l₁ ~ l₃
[PROOFSTEP]
cases' h₁ with _ _ l₂
[GOAL]
case C1.refl
α : Type u_1
trans : Lists α → Prop := fun l₁ => ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ Lists'.toList l₁ → trans l'
l₃ : Lists α
h₂ : of' l₁ ~ l₃
h₁' : of' l₁ ~ of' l₁
h₂' : of' l₁ ~ l₃
⊢ of' l₁ ~ l₃
[PROOFSTEP]
exact h₂
[GOAL]
case C1.antisymm
α : Type u_1
trans : Lists α → Prop := fun l₁ => ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ Lists'.toList l₁ → trans l'
l₃ : Lists α
l₂ : Lists' α true
a✝¹ : Lists'.Subset l₁ l₂
a✝ : Lists'.Subset l₂ l₁
h₂ : { fst := true, snd := l₂ } ~ l₃
h₁' : of' l₁ ~ { fst := true, snd := l₂ }
h₂' : { fst := true, snd := l₂ } ~ l₃
⊢ of' l₁ ~ l₃
[PROOFSTEP]
cases' h₂ with _ _ l₃
[GOAL]
case C1.antisymm.refl
α : Type u_1
trans : Lists α → Prop := fun l₁ => ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ Lists'.toList l₁ → trans l'
l₂ : Lists' α true
a✝¹ : Lists'.Subset l₁ l₂
a✝ : Lists'.Subset l₂ l₁
h₁' : of' l₁ ~ { fst := true, snd := l₂ }
h₂' : { fst := true, snd := l₂ } ~ { fst := true, snd := l₂ }
⊢ of' l₁ ~ { fst := true, snd := l₂ }
[PROOFSTEP]
exact h₁'
[GOAL]
case C1.antisymm.antisymm
α : Type u_1
trans : Lists α → Prop := fun l₁ => ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ Lists'.toList l₁ → trans l'
l₂ : Lists' α true
a✝³ : Lists'.Subset l₁ l₂
a✝² : Lists'.Subset l₂ l₁
h₁' : of' l₁ ~ { fst := true, snd := l₂ }
l₃ : Lists' α true
a✝¹ : Lists'.Subset l₂ l₃
a✝ : Lists'.Subset l₃ l₂
h₂' : { fst := true, snd := l₂ } ~ { fst := true, snd := l₃ }
⊢ of' l₁ ~ { fst := true, snd := l₃ }
[PROOFSTEP]
cases' Equiv.antisymm_iff.1 h₁' with hl₁ hr₁
[GOAL]
case C1.antisymm.antisymm.intro
α : Type u_1
trans : Lists α → Prop := fun l₁ => ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ Lists'.toList l₁ → trans l'
l₂ : Lists' α true
a✝³ : Lists'.Subset l₁ l₂
a✝² : Lists'.Subset l₂ l₁
h₁' : of' l₁ ~ { fst := true, snd := l₂ }
l₃ : Lists' α true
a✝¹ : Lists'.Subset l₂ l₃
a✝ : Lists'.Subset l₃ l₂
h₂' : { fst := true, snd := l₂ } ~ { fst := true, snd := l₃ }
hl₁ : l₁ ⊆ l₂
hr₁ : l₂ ⊆ l₁
⊢ of' l₁ ~ { fst := true, snd := l₃ }
[PROOFSTEP]
cases' Equiv.antisymm_iff.1 h₂' with hl₂ hr₂
[GOAL]
case C1.antisymm.antisymm.intro.intro
α : Type u_1
trans : Lists α → Prop := fun l₁ => ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ Lists'.toList l₁ → trans l'
l₂ : Lists' α true
a✝³ : Lists'.Subset l₁ l₂
a✝² : Lists'.Subset l₂ l₁
h₁' : of' l₁ ~ { fst := true, snd := l₂ }
l₃ : Lists' α true
a✝¹ : Lists'.Subset l₂ l₃
a✝ : Lists'.Subset l₃ l₂
h₂' : { fst := true, snd := l₂ } ~ { fst := true, snd := l₃ }
hl₁ : l₁ ⊆ l₂
hr₁ : l₂ ⊆ l₁
hl₂ : l₂ ⊆ l₃
hr₂ : l₃ ⊆ l₂
⊢ of' l₁ ~ { fst := true, snd := l₃ }
[PROOFSTEP]
apply Equiv.antisymm_iff.2
[GOAL]
case C1.antisymm.antisymm.intro.intro
α : Type u_1
trans : Lists α → Prop := fun l₁ => ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ Lists'.toList l₁ → trans l'
l₂ : Lists' α true
a✝³ : Lists'.Subset l₁ l₂
a✝² : Lists'.Subset l₂ l₁
h₁' : of' l₁ ~ { fst := true, snd := l₂ }
l₃ : Lists' α true
a✝¹ : Lists'.Subset l₂ l₃
a✝ : Lists'.Subset l₃ l₂
h₂' : { fst := true, snd := l₂ } ~ { fst := true, snd := l₃ }
hl₁ : l₁ ⊆ l₂
hr₁ : l₂ ⊆ l₁
hl₂ : l₂ ⊆ l₃
hr₂ : l₃ ⊆ l₂
⊢ l₁ ⊆ l₃ ∧ l₃ ⊆ l₁
[PROOFSTEP]
constructor
[GOAL]
case C1.antisymm.antisymm.intro.intro.left
α : Type u_1
trans : Lists α → Prop := fun l₁ => ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ Lists'.toList l₁ → trans l'
l₂ : Lists' α true
a✝³ : Lists'.Subset l₁ l₂
a✝² : Lists'.Subset l₂ l₁
h₁' : of' l₁ ~ { fst := true, snd := l₂ }
l₃ : Lists' α true
a✝¹ : Lists'.Subset l₂ l₃
a✝ : Lists'.Subset l₃ l₂
h₂' : { fst := true, snd := l₂ } ~ { fst := true, snd := l₃ }
hl₁ : l₁ ⊆ l₂
hr₁ : l₂ ⊆ l₁
hl₂ : l₂ ⊆ l₃
hr₂ : l₃ ⊆ l₂
⊢ l₁ ⊆ l₃
[PROOFSTEP]
apply Lists'.subset_def.2
[GOAL]
case C1.antisymm.antisymm.intro.intro.right
α : Type u_1
trans : Lists α → Prop := fun l₁ => ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ Lists'.toList l₁ → trans l'
l₂ : Lists' α true
a✝³ : Lists'.Subset l₁ l₂
a✝² : Lists'.Subset l₂ l₁
h₁' : of' l₁ ~ { fst := true, snd := l₂ }
l₃ : Lists' α true
a✝¹ : Lists'.Subset l₂ l₃
a✝ : Lists'.Subset l₃ l₂
h₂' : { fst := true, snd := l₂ } ~ { fst := true, snd := l₃ }
hl₁ : l₁ ⊆ l₂
hr₁ : l₂ ⊆ l₁
hl₂ : l₂ ⊆ l₃
hr₂ : l₃ ⊆ l₂
⊢ l₃ ⊆ l₁
[PROOFSTEP]
apply Lists'.subset_def.2
[GOAL]
case C1.antisymm.antisymm.intro.intro.left
α : Type u_1
trans : Lists α → Prop := fun l₁ => ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ Lists'.toList l₁ → trans l'
l₂ : Lists' α true
a✝³ : Lists'.Subset l₁ l₂
a✝² : Lists'.Subset l₂ l₁
h₁' : of' l₁ ~ { fst := true, snd := l₂ }
l₃ : Lists' α true
a✝¹ : Lists'.Subset l₂ l₃
a✝ : Lists'.Subset l₃ l₂
h₂' : { fst := true, snd := l₂ } ~ { fst := true, snd := l₃ }
hl₁ : l₁ ⊆ l₂
hr₁ : l₂ ⊆ l₁
hl₂ : l₂ ⊆ l₃
hr₂ : l₃ ⊆ l₂
⊢ ∀ (a : Lists α), a ∈ Lists'.toList l₁ → a ∈ l₃
[PROOFSTEP]
intro a₁ m₁
[GOAL]
case C1.antisymm.antisymm.intro.intro.left
α : Type u_1
trans : Lists α → Prop := fun l₁ => ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ Lists'.toList l₁ → trans l'
l₂ : Lists' α true
a✝³ : Lists'.Subset l₁ l₂
a✝² : Lists'.Subset l₂ l₁
h₁' : of' l₁ ~ { fst := true, snd := l₂ }
l₃ : Lists' α true
a✝¹ : Lists'.Subset l₂ l₃
a✝ : Lists'.Subset l₃ l₂
h₂' : { fst := true, snd := l₂ } ~ { fst := true, snd := l₃ }
hl₁ : l₁ ⊆ l₂
hr₁ : l₂ ⊆ l₁
hl₂ : l₂ ⊆ l₃
hr₂ : l₃ ⊆ l₂
a₁ : Lists α
m₁ : a₁ ∈ Lists'.toList l₁
⊢ a₁ ∈ l₃
[PROOFSTEP]
rcases Lists'.mem_of_subset' hl₁ m₁ with ⟨a₂, m₂, e₁₂⟩
[GOAL]
case C1.antisymm.antisymm.intro.intro.left.intro.intro
α : Type u_1
trans : Lists α → Prop := fun l₁ => ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ Lists'.toList l₁ → trans l'
l₂ : Lists' α true
a✝³ : Lists'.Subset l₁ l₂
a✝² : Lists'.Subset l₂ l₁
h₁' : of' l₁ ~ { fst := true, snd := l₂ }
l₃ : Lists' α true
a✝¹ : Lists'.Subset l₂ l₃
a✝ : Lists'.Subset l₃ l₂
h₂' : { fst := true, snd := l₂ } ~ { fst := true, snd := l₃ }
hl₁ : l₁ ⊆ l₂
hr₁ : l₂ ⊆ l₁
hl₂ : l₂ ⊆ l₃
hr₂ : l₃ ⊆ l₂
a₁ : Lists α
m₁ : a₁ ∈ Lists'.toList l₁
a₂ : Lists α
m₂ : a₂ ∈ Lists'.toList l₂
e₁₂ : a₁ ~ a₂
⊢ a₁ ∈ l₃
[PROOFSTEP]
rcases Lists'.mem_of_subset' hl₂ m₂ with ⟨a₃, m₃, e₂₃⟩
[GOAL]
case C1.antisymm.antisymm.intro.intro.left.intro.intro.intro.intro
α : Type u_1
trans : Lists α → Prop := fun l₁ => ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ Lists'.toList l₁ → trans l'
l₂ : Lists' α true
a✝³ : Lists'.Subset l₁ l₂
a✝² : Lists'.Subset l₂ l₁
h₁' : of' l₁ ~ { fst := true, snd := l₂ }
l₃ : Lists' α true
a✝¹ : Lists'.Subset l₂ l₃
a✝ : Lists'.Subset l₃ l₂
h₂' : { fst := true, snd := l₂ } ~ { fst := true, snd := l₃ }
hl₁ : l₁ ⊆ l₂
hr₁ : l₂ ⊆ l₁
hl₂ : l₂ ⊆ l₃
hr₂ : l₃ ⊆ l₂
a₁ : Lists α
m₁ : a₁ ∈ Lists'.toList l₁
a₂ : Lists α
m₂ : a₂ ∈ Lists'.toList l₂
e₁₂ : a₁ ~ a₂
a₃ : Lists α
m₃ : a₃ ∈ Lists'.toList l₃
e₂₃ : a₂ ~ a₃
⊢ a₁ ∈ l₃
[PROOFSTEP]
exact ⟨a₃, m₃, IH _ m₁ e₁₂ e₂₃⟩
[GOAL]
case C1.antisymm.antisymm.intro.intro.right
α : Type u_1
trans : Lists α → Prop := fun l₁ => ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ Lists'.toList l₁ → trans l'
l₂ : Lists' α true
a✝³ : Lists'.Subset l₁ l₂
a✝² : Lists'.Subset l₂ l₁
h₁' : of' l₁ ~ { fst := true, snd := l₂ }
l₃ : Lists' α true
a✝¹ : Lists'.Subset l₂ l₃
a✝ : Lists'.Subset l₃ l₂
h₂' : { fst := true, snd := l₂ } ~ { fst := true, snd := l₃ }
hl₁ : l₁ ⊆ l₂
hr₁ : l₂ ⊆ l₁
hl₂ : l₂ ⊆ l₃
hr₂ : l₃ ⊆ l₂
⊢ ∀ (a : Lists α), a ∈ Lists'.toList l₃ → a ∈ l₁
[PROOFSTEP]
intro a₃ m₃
[GOAL]
case C1.antisymm.antisymm.intro.intro.right
α : Type u_1
trans : Lists α → Prop := fun l₁ => ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ Lists'.toList l₁ → trans l'
l₂ : Lists' α true
a✝³ : Lists'.Subset l₁ l₂
a✝² : Lists'.Subset l₂ l₁
h₁' : of' l₁ ~ { fst := true, snd := l₂ }
l₃ : Lists' α true
a✝¹ : Lists'.Subset l₂ l₃
a✝ : Lists'.Subset l₃ l₂
h₂' : { fst := true, snd := l₂ } ~ { fst := true, snd := l₃ }
hl₁ : l₁ ⊆ l₂
hr₁ : l₂ ⊆ l₁
hl₂ : l₂ ⊆ l₃
hr₂ : l₃ ⊆ l₂
a₃ : Lists α
m₃ : a₃ ∈ Lists'.toList l₃
⊢ a₃ ∈ l₁
[PROOFSTEP]
rcases Lists'.mem_of_subset' hr₂ m₃ with ⟨a₂, m₂, e₃₂⟩
[GOAL]
case C1.antisymm.antisymm.intro.intro.right.intro.intro
α : Type u_1
trans : Lists α → Prop := fun l₁ => ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ Lists'.toList l₁ → trans l'
l₂ : Lists' α true
a✝³ : Lists'.Subset l₁ l₂
a✝² : Lists'.Subset l₂ l₁
h₁' : of' l₁ ~ { fst := true, snd := l₂ }
l₃ : Lists' α true
a✝¹ : Lists'.Subset l₂ l₃
a✝ : Lists'.Subset l₃ l₂
h₂' : { fst := true, snd := l₂ } ~ { fst := true, snd := l₃ }
hl₁ : l₁ ⊆ l₂
hr₁ : l₂ ⊆ l₁
hl₂ : l₂ ⊆ l₃
hr₂ : l₃ ⊆ l₂
a₃ : Lists α
m₃ : a₃ ∈ Lists'.toList l₃
a₂ : Lists α
m₂ : a₂ ∈ Lists'.toList l₂
e₃₂ : a₃ ~ a₂
⊢ a₃ ∈ l₁
[PROOFSTEP]
rcases Lists'.mem_of_subset' hr₁ m₂ with ⟨a₁, m₁, e₂₁⟩
[GOAL]
case C1.antisymm.antisymm.intro.intro.right.intro.intro.intro.intro
α : Type u_1
trans : Lists α → Prop := fun l₁ => ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ Lists'.toList l₁ → trans l'
l₂ : Lists' α true
a✝³ : Lists'.Subset l₁ l₂
a✝² : Lists'.Subset l₂ l₁
h₁' : of' l₁ ~ { fst := true, snd := l₂ }
l₃ : Lists' α true
a✝¹ : Lists'.Subset l₂ l₃
a✝ : Lists'.Subset l₃ l₂
h₂' : { fst := true, snd := l₂ } ~ { fst := true, snd := l₃ }
hl₁ : l₁ ⊆ l₂
hr₁ : l₂ ⊆ l₁
hl₂ : l₂ ⊆ l₃
hr₂ : l₃ ⊆ l₂
a₃ : Lists α
m₃ : a₃ ∈ Lists'.toList l₃
a₂ : Lists α
m₂ : a₂ ∈ Lists'.toList l₂
e₃₂ : a₃ ~ a₂
a₁ : Lists α
m₁ : a₁ ∈ Lists'.toList l₁
e₂₁ : a₂ ~ a₁
⊢ a₃ ∈ l₁
[PROOFSTEP]
exact ⟨a₁, m₁, (IH _ m₁ e₂₁.symm e₃₂.symm).symm⟩
[GOAL]
case D0
α : Type u_1
trans : Lists α → Prop := fun l₁ => ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
⊢ ∀ (l' : Lists α), l' ∈ Lists'.toList Lists'.nil → trans l'
[PROOFSTEP]
rintro _ ⟨⟩
[GOAL]
case D1
α : Type u_1
trans : Lists α → Prop := fun l₁ => ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
⊢ ∀ (a : Lists α) (l : Lists' α true),
    trans a →
      (∀ (l' : Lists α), l' ∈ Lists'.toList l → trans l') →
        ∀ (l' : Lists α), l' ∈ Lists'.toList (Lists'.cons a l) → trans l'
[PROOFSTEP]
intro a l IH₁ IH
[GOAL]
case D1
α : Type u_1
trans : Lists α → Prop := fun l₁ => ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
a : Lists α
l : Lists' α true
IH₁ : trans a
IH : ∀ (l' : Lists α), l' ∈ Lists'.toList l → trans l'
⊢ ∀ (l' : Lists α), l' ∈ Lists'.toList (Lists'.cons a l) → trans l'
[PROOFSTEP]
simp only [Lists'.toList, Sigma.eta, List.find?, List.mem_cons, forall_eq_or_imp]
[GOAL]
case D1
α : Type u_1
trans : Lists α → Prop := fun l₁ => ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
a : Lists α
l : Lists' α true
IH₁ : trans a
IH : ∀ (l' : Lists α), l' ∈ Lists'.toList l → trans l'
⊢ (∀ ⦃l₂ l₃ : Lists α⦄, a ~ l₂ → l₂ ~ l₃ → a ~ l₃) ∧
    ∀ (a : Lists α), a ∈ Lists'.toList l → ∀ ⦃l₂ l₃ : Lists α⦄, a ~ l₂ → l₂ ~ l₃ → a ~ l₃
[PROOFSTEP]
constructor
[GOAL]
case D1.left
α : Type u_1
trans : Lists α → Prop := fun l₁ => ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
a : Lists α
l : Lists' α true
IH₁ : trans a
IH : ∀ (l' : Lists α), l' ∈ Lists'.toList l → trans l'
⊢ ∀ ⦃l₂ l₃ : Lists α⦄, a ~ l₂ → l₂ ~ l₃ → a ~ l₃
[PROOFSTEP]
intros l₂ l₃ h₁ h₂
[GOAL]
case D1.left
α : Type u_1
trans : Lists α → Prop := fun l₁ => ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
a : Lists α
l : Lists' α true
IH₁ : trans a
IH : ∀ (l' : Lists α), l' ∈ Lists'.toList l → trans l'
l₂ l₃ : Lists α
h₁ : a ~ l₂
h₂ : l₂ ~ l₃
⊢ a ~ l₃
[PROOFSTEP]
exact IH₁ h₁ h₂
[GOAL]
case D1.right
α : Type u_1
trans : Lists α → Prop := fun l₁ => ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
a : Lists α
l : Lists' α true
IH₁ : trans a
IH : ∀ (l' : Lists α), l' ∈ Lists'.toList l → trans l'
⊢ ∀ (a : Lists α), a ∈ Lists'.toList l → ∀ ⦃l₂ l₃ : Lists α⦄, a ~ l₂ → l₂ ~ l₃ → a ~ l₃
[PROOFSTEP]
intros a h₁ l₂ l₃ h₂ h₃
[GOAL]
case D1.right
α : Type u_1
trans : Lists α → Prop := fun l₁ => ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
a✝ : Lists α
l : Lists' α true
IH₁ : trans a✝
IH : ∀ (l' : Lists α), l' ∈ Lists'.toList l → trans l'
a : Lists α
h₁ : a ∈ Lists'.toList l
l₂ l₃ : Lists α
h₂ : a ~ l₂
h₃ : l₂ ~ l₃
⊢ a ~ l₃
[PROOFSTEP]
exact IH _ h₁ h₂ h₃
[GOAL]
α : Type u_1
b : Bool
l : Lists' α b
⊢ 0 < sizeOf l
[PROOFSTEP]
cases l
[GOAL]
case atom
α : Type u_1
a✝ : α
⊢ 0 < sizeOf (Lists'.atom a✝)
[PROOFSTEP]
simp only [Lists'.atom.sizeOf_spec, Lists'.nil.sizeOf_spec, Lists'.cons'.sizeOf_spec, true_or, add_pos_iff]
[GOAL]
case nil
α : Type u_1
⊢ 0 < sizeOf Lists'.nil
[PROOFSTEP]
simp only [Lists'.atom.sizeOf_spec, Lists'.nil.sizeOf_spec, Lists'.cons'.sizeOf_spec, true_or, add_pos_iff]
[GOAL]
case cons'
α : Type u_1
b✝ : Bool
a✝¹ : Lists' α b✝
a✝ : Lists' α true
⊢ 0 < sizeOf (Lists'.cons' a✝¹ a✝)
[PROOFSTEP]
simp only [Lists'.atom.sizeOf_spec, Lists'.nil.sizeOf_spec, Lists'.cons'.sizeOf_spec, true_or, add_pos_iff]
[GOAL]
α : Type u_1
b : Bool
a : Lists' α b
l : Lists' α true
⊢ sizeOf { fst := b, snd := a } < sizeOf (Lists'.cons' a l)
[PROOFSTEP]
simp only [Sigma.mk.sizeOf_spec, Lists'.cons'.sizeOf_spec, lt_add_iff_pos_right]
[GOAL]
α : Type u_1
b : Bool
a : Lists' α b
l : Lists' α true
⊢ 0 < sizeOf l
[PROOFSTEP]
apply sizeof_pos
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : Lists' α false
⊢ { fst := false, snd := l₁ } ~ { fst := false, snd := l₂ } ↔ l₁ = l₂
[PROOFSTEP]
cases l₁
[GOAL]
case atom
α : Type u_1
inst✝ : DecidableEq α
l₂ : Lists' α false
a✝ : α
⊢ { fst := false, snd := Lists'.atom a✝ } ~ { fst := false, snd := l₂ } ↔ Lists'.atom a✝ = l₂
[PROOFSTEP]
apply equiv_atom.trans
[GOAL]
case atom
α : Type u_1
inst✝ : DecidableEq α
l₂ : Lists' α false
a✝ : α
⊢ atom a✝ = { fst := false, snd := l₂ } ↔ Lists'.atom a✝ = l₂
[PROOFSTEP]
simp [atom]
[GOAL]
case atom
α : Type u_1
inst✝ : DecidableEq α
l₂ : Lists' α false
a✝ : α
⊢ { fst := false, snd := Lists'.atom a✝ } = { fst := false, snd := l₂ } ↔ Lists'.atom a✝ = l₂
[PROOFSTEP]
constructor
[GOAL]
case atom.mp
α : Type u_1
inst✝ : DecidableEq α
l₂ : Lists' α false
a✝ : α
⊢ { fst := false, snd := Lists'.atom a✝ } = { fst := false, snd := l₂ } → Lists'.atom a✝ = l₂
[PROOFSTEP]
rintro ⟨rfl⟩
[GOAL]
case atom.mp.refl
α : Type u_1
inst✝ : DecidableEq α
a✝ : α
⊢ Lists'.atom a✝ = Lists'.atom a✝
[PROOFSTEP]
rfl
[GOAL]
case atom.mpr
α : Type u_1
inst✝ : DecidableEq α
l₂ : Lists' α false
a✝ : α
⊢ Lists'.atom a✝ = l₂ → { fst := false, snd := Lists'.atom a✝ } = { fst := false, snd := l₂ }
[PROOFSTEP]
rintro ⟨rfl⟩
[GOAL]
case atom.mpr.refl
α : Type u_1
inst✝ : DecidableEq α
a✝ : α
⊢ { fst := false, snd := Lists'.atom a✝ } = { fst := false, snd := Lists'.atom a✝ }
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l₁ : Lists' α false
l₂ : Lists' α true
⊢ ¬{ fst := false, snd := l₁ } ~ { fst := true, snd := l₂ }
[PROOFSTEP]
rintro ⟨⟩
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l₁ : Lists' α true
l₂ : Lists' α false
⊢ ¬{ fst := true, snd := l₁ } ~ { fst := false, snd := l₂ }
[PROOFSTEP]
rintro ⟨⟩
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : Lists' α true
⊢ Decidable ({ fst := true, snd := l₁ } ~ { fst := true, snd := l₂ })
[PROOFSTEP]
haveI : Decidable (l₁ ⊆ l₂) :=
  have :
    SizeOf.sizeOf l₁ + SizeOf.sizeOf l₂ < SizeOf.sizeOf (⟨true, l₁⟩ : Lists α) + SizeOf.sizeOf (⟨true, l₂⟩ : Lists α) :=
    by decreasing_tactic
  Subset.decidable l₁ l₂
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : Lists' α true
⊢ sizeOf l₁ + sizeOf l₂ < sizeOf { fst := true, snd := l₁ } + sizeOf { fst := true, snd := l₂ }
[PROOFSTEP]
decreasing_tactic
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : Lists' α true
this : Decidable (l₁ ⊆ l₂)
⊢ Decidable ({ fst := true, snd := l₁ } ~ { fst := true, snd := l₂ })
[PROOFSTEP]
haveI : Decidable (l₂ ⊆ l₁) :=
  have :
    SizeOf.sizeOf l₂ + SizeOf.sizeOf l₁ < SizeOf.sizeOf (⟨true, l₁⟩ : Lists α) + SizeOf.sizeOf (⟨true, l₂⟩ : Lists α) :=
    by decreasing_tactic
  Subset.decidable l₂ l₁
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : Lists' α true
this : Decidable (l₁ ⊆ l₂)
⊢ sizeOf l₂ + sizeOf l₁ < sizeOf { fst := true, snd := l₁ } + sizeOf { fst := true, snd := l₂ }
[PROOFSTEP]
decreasing_tactic
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : Lists' α true
this✝ : Decidable (l₁ ⊆ l₂)
this : Decidable (l₂ ⊆ l₁)
⊢ Decidable ({ fst := true, snd := l₁ } ~ { fst := true, snd := l₂ })
[PROOFSTEP]
exact decidable_of_iff' _ Equiv.antisymm_iff
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
b : Bool
a : Lists' α b
l₁ l₂ : Lists' α true
⊢ Decidable (Lists'.cons' a l₁ ⊆ l₂)
[PROOFSTEP]
haveI :=
  have : sizeOf (⟨b, a⟩ : Lists α) < 1 + 1 + sizeOf a + sizeOf l₁ := by simp [sizeof_pos]
  mem.decidable ⟨b, a⟩ l₂
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
b : Bool
a : Lists' α b
l₁ l₂ : Lists' α true
⊢ sizeOf { fst := b, snd := a } < 1 + 1 + sizeOf a + sizeOf l₁
[PROOFSTEP]
simp [sizeof_pos]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
b : Bool
a : Lists' α b
l₁ l₂ : Lists' α true
this : Decidable ({ fst := b, snd := a } ∈ l₂)
⊢ Decidable (Lists'.cons' a l₁ ⊆ l₂)
[PROOFSTEP]
haveI :=
  have : SizeOf.sizeOf l₁ + SizeOf.sizeOf l₂ < SizeOf.sizeOf (Lists'.cons' a l₁) + SizeOf.sizeOf l₂ := by
    decreasing_tactic
  Subset.decidable l₁ l₂
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
b : Bool
a : Lists' α b
l₁ l₂ : Lists' α true
this : Decidable ({ fst := b, snd := a } ∈ l₂)
⊢ sizeOf l₁ + sizeOf l₂ < sizeOf (Lists'.cons' a l₁) + sizeOf l₂
[PROOFSTEP]
decreasing_tactic
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
b : Bool
a : Lists' α b
l₁ l₂ : Lists' α true
this✝ : Decidable ({ fst := b, snd := a } ∈ l₂)
this : Decidable (l₁ ⊆ l₂)
⊢ Decidable (Lists'.cons' a l₁ ⊆ l₂)
[PROOFSTEP]
exact decidable_of_iff' _ (@Lists'.cons_subset _ ⟨_, _⟩ _ _)
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
a : Lists α
⊢ ¬a ∈ Lists'.nil
[PROOFSTEP]
rintro ⟨_, ⟨⟩, _⟩
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
a : Lists α
b✝ : Bool
b : Lists' α b✝
l₂ : Lists' α true
⊢ Decidable (a ∈ Lists'.cons' b l₂)
[PROOFSTEP]
haveI :=
  have : sizeOf (⟨_, b⟩ : Lists α) < 1 + 1 + sizeOf b + sizeOf l₂ := by simp [sizeof_pos]
  Equiv.decidable a ⟨_, b⟩
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
a : Lists α
b✝ : Bool
b : Lists' α b✝
l₂ : Lists' α true
⊢ sizeOf { fst := b✝, snd := b } < 1 + 1 + sizeOf b + sizeOf l₂
[PROOFSTEP]
simp [sizeof_pos]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
a : Lists α
b✝ : Bool
b : Lists' α b✝
l₂ : Lists' α true
this : Decidable (a ~ { fst := b✝, snd := b })
⊢ Decidable (a ∈ Lists'.cons' b l₂)
[PROOFSTEP]
haveI :=
  have : SizeOf.sizeOf a + SizeOf.sizeOf l₂ < SizeOf.sizeOf a + SizeOf.sizeOf (Lists'.cons' b l₂) := by
    decreasing_tactic
  mem.decidable a l₂
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
a : Lists α
b✝ : Bool
b : Lists' α b✝
l₂ : Lists' α true
this : Decidable (a ~ { fst := b✝, snd := b })
⊢ sizeOf a + sizeOf l₂ < sizeOf a + sizeOf (Lists'.cons' b l₂)
[PROOFSTEP]
decreasing_tactic
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
a : Lists α
b✝ : Bool
b : Lists' α b✝
l₂ : Lists' α true
this✝ : Decidable (a ~ { fst := b✝, snd := b })
this : Decidable (a ∈ l₂)
⊢ Decidable (a ∈ Lists'.cons' b l₂)
[PROOFSTEP]
refine' decidable_of_iff' (a ~ ⟨_, b⟩ ∨ a ∈ l₂) _
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
a : Lists α
b✝ : Bool
b : Lists' α b✝
l₂ : Lists' α true
this✝ : Decidable (a ~ { fst := b✝, snd := b })
this : Decidable (a ∈ l₂)
⊢ a ∈ Lists'.cons' b l₂ ↔ a ~ { fst := b✝, snd := b } ∨ a ∈ l₂
[PROOFSTEP]
rw [← Lists'.mem_cons]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
a : Lists α
b✝ : Bool
b : Lists' α b✝
l₂ : Lists' α true
this✝ : Decidable (a ~ { fst := b✝, snd := b })
this : Decidable (a ∈ l₂)
⊢ a ∈ Lists'.cons' b l₂ ↔ a ∈ Lists'.cons { fst := b✝, snd := b } l₂
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
⊢ DecidableEq (Finsets α)
[PROOFSTEP]
unfold Finsets
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
⊢ DecidableEq (Quotient Lists.instSetoidLists)
[PROOFSTEP]
exact (Quotient.decidableEq (d := fun _ _ => Lists.Equiv.decidable _ _))


[GOAL]
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
h : LieModule.IsTrivial L { x // x ∈ ↑I }
x y : { x // x ∈ ↑I }
⊢ ⁅x, y⁆ = 0
[PROOFSTEP]
apply h.trivial
[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₁ : Surjective ↑f
h₂ : IsLieAbelian L₁
x y : L₂
⊢ ⁅x, y⁆ = 0
[PROOFSTEP]
obtain ⟨u, rfl⟩ := h₁ x
[GOAL]
case intro
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₁ : Surjective ↑f
h₂ : IsLieAbelian L₁
y : L₂
u : L₁
⊢ ⁅↑f u, y⁆ = 0
[PROOFSTEP]
obtain ⟨v, rfl⟩ := h₁ y
[GOAL]
case intro.intro
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₁ : Surjective ↑f
h₂ : IsLieAbelian L₁
u v : L₁
⊢ ⁅↑f u, ↑f v⁆ = 0
[PROOFSTEP]
rw [← LieHom.map_lie, trivial_lie_zero, LieHom.map_zero]
[GOAL]
A : Type v
inst✝ : Ring A
⊢ (IsCommutative A fun x x_1 => x * x_1) ↔ IsLieAbelian A
[PROOFSTEP]
have h₁ : IsCommutative A (· * ·) ↔ ∀ a b : A, a * b = b * a := ⟨fun h => h.1, fun h => ⟨h⟩⟩
[GOAL]
A : Type v
inst✝ : Ring A
h₁ : (IsCommutative A fun x x_1 => x * x_1) ↔ ∀ (a b : A), a * b = b * a
⊢ (IsCommutative A fun x x_1 => x * x_1) ↔ IsLieAbelian A
[PROOFSTEP]
have h₂ : IsLieAbelian A ↔ ∀ a b : A, ⁅a, b⁆ = 0 := ⟨fun h => h.1, fun h => ⟨h⟩⟩
[GOAL]
A : Type v
inst✝ : Ring A
h₁ : (IsCommutative A fun x x_1 => x * x_1) ↔ ∀ (a b : A), a * b = b * a
h₂ : IsLieAbelian A ↔ ∀ (a b : A), ⁅a, b⁆ = 0
⊢ (IsCommutative A fun x x_1 => x * x_1) ↔ IsLieAbelian A
[PROOFSTEP]
simp only [h₁, h₂, LieRing.of_associative_ring_bracket, sub_eq_zero]
[GOAL]
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x✝¹ x✝ : { x // x ∈ ↑⊥ }
x : L
hx : x ∈ ↑⊥
⊢ ⁅{ val := x, property := hx }, x✝⁆ = 0
[PROOFSTEP]
simp
[GOAL]
R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
x : L
⊢ x ∈ LieModule.ker R L M ↔ ∀ (m : M), ⁅x, m⁆ = 0
[PROOFSTEP]
simp only [LieModule.ker, LieHom.mem_ker, LinearMap.ext_iff, LinearMap.zero_apply, toEndomorphism_apply_apply]
[GOAL]
R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
x y : M
hx : x ∈ {m | ∀ (x : L), ⁅x, m⁆ = 0}
hy : y ∈ {m | ∀ (x : L), ⁅x, m⁆ = 0}
z : L
⊢ ⁅z, x + y⁆ = 0
[PROOFSTEP]
rw [lie_add, hx, hy, add_zero]
[GOAL]
R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
c : R
x : M
hx :
  x ∈
    {
          toAddSubsemigroup :=
            { carrier := {m | ∀ (x : L), ⁅x, m⁆ = 0},
              add_mem' :=
                (_ :
                  ∀ {x y : M},
                    x ∈ {m | ∀ (x : L), ⁅x, m⁆ = 0} → y ∈ {m | ∀ (x : L), ⁅x, m⁆ = 0} → ∀ (z : L), ⁅z, x + y⁆ = 0) },
          zero_mem' := (_ : ∀ (x : L), ⁅x, 0⁆ = 0) }.toAddSubsemigroup.carrier
y : L
⊢ ⁅y, c • x⁆ = 0
[PROOFSTEP]
rw [lie_smul, hx, smul_zero]
[GOAL]
R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
x : L
m : M
hm :
  m ∈
    {
            toAddSubmonoid :=
              {
                toAddSubsemigroup :=
                  { carrier := {m | ∀ (x : L), ⁅x, m⁆ = 0},
                    add_mem' :=
                      (_ :
                        ∀ {x y : M},
                          x ∈ {m | ∀ (x : L), ⁅x, m⁆ = 0} →
                            y ∈ {m | ∀ (x : L), ⁅x, m⁆ = 0} → ∀ (z : L), ⁅z, x + y⁆ = 0) },
                zero_mem' := (_ : ∀ (x : L), ⁅x, 0⁆ = 0) },
            smul_mem' :=
              (_ :
                ∀ (c : R) (x : M),
                  x ∈
                      {
                            toAddSubsemigroup :=
                              { carrier := {m | ∀ (x : L), ⁅x, m⁆ = 0},
                                add_mem' :=
                                  (_ :
                                    ∀ {x y : M},
                                      x ∈ {m | ∀ (x : L), ⁅x, m⁆ = 0} →
                                        y ∈ {m | ∀ (x : L), ⁅x, m⁆ = 0} → ∀ (z : L), ⁅z, x + y⁆ = 0) },
                            zero_mem' := (_ : ∀ (x : L), ⁅x, 0⁆ = 0) }.toAddSubsemigroup.carrier →
                    ∀ (y : L), ⁅y, c • x⁆ = 0) }.toAddSubmonoid.toAddSubsemigroup.carrier
y : L
⊢ ⁅y, ⁅x, m⁆⁆ = 0
[PROOFSTEP]
rw [hm, lie_zero]
[GOAL]
R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
I : LieIdeal R L
⊢ ⁅I, maxTrivSubmodule R L M⁆ = ⊥
[PROOFSTEP]
rw [← LieSubmodule.coe_toSubmodule_eq_iff, LieSubmodule.lieIdeal_oper_eq_linear_span, LieSubmodule.bot_coeSubmodule,
  Submodule.span_eq_bot]
[GOAL]
R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
I : LieIdeal R L
⊢ ∀ (x : M), x ∈ {m | ∃ x n, ⁅↑x, ↑n⁆ = m} → x = 0
[PROOFSTEP]
rintro m ⟨⟨x, hx⟩, ⟨⟨m, hm⟩, rfl⟩⟩
[GOAL]
case intro.mk.intro.mk
R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
I : LieIdeal R L
x : L
hx : x ∈ I
m : M
hm : m ∈ maxTrivSubmodule R L M
⊢ ⁅↑{ val := x, property := hx }, ↑{ val := m, property := hm }⁆ = 0
[PROOFSTEP]
exact hm x
[GOAL]
R : Type u
L : Type v
M : Type w
N✝ : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup N✝
inst✝² : Module R N✝
inst✝¹ : LieRingModule L N✝
inst✝ : LieModule R L N✝
N : LieSubmodule R L M
⊢ N ≤ maxTrivSubmodule R L M ↔ ⁅⊤, N⁆ = ⊥
[PROOFSTEP]
refine' ⟨fun h => _, fun h m hm => _⟩
[GOAL]
case refine'_1
R : Type u
L : Type v
M : Type w
N✝ : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup N✝
inst✝² : Module R N✝
inst✝¹ : LieRingModule L N✝
inst✝ : LieModule R L N✝
N : LieSubmodule R L M
h : N ≤ maxTrivSubmodule R L M
⊢ ⁅⊤, N⁆ = ⊥
[PROOFSTEP]
rw [← le_bot_iff, ← ideal_oper_maxTrivSubmodule_eq_bot R L M ⊤]
[GOAL]
case refine'_1
R : Type u
L : Type v
M : Type w
N✝ : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup N✝
inst✝² : Module R N✝
inst✝¹ : LieRingModule L N✝
inst✝ : LieModule R L N✝
N : LieSubmodule R L M
h : N ≤ maxTrivSubmodule R L M
⊢ ⁅⊤, N⁆ ≤ ⁅⊤, maxTrivSubmodule R L M⁆
[PROOFSTEP]
exact LieSubmodule.mono_lie_right _ _ ⊤ h
[GOAL]
case refine'_2
R : Type u
L : Type v
M : Type w
N✝ : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup N✝
inst✝² : Module R N✝
inst✝¹ : LieRingModule L N✝
inst✝ : LieModule R L N✝
N : LieSubmodule R L M
h : ⁅⊤, N⁆ = ⊥
m : M
hm : m ∈ N
⊢ m ∈ maxTrivSubmodule R L M
[PROOFSTEP]
rw [mem_maxTrivSubmodule]
[GOAL]
case refine'_2
R : Type u
L : Type v
M : Type w
N✝ : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup N✝
inst✝² : Module R N✝
inst✝¹ : LieRingModule L N✝
inst✝ : LieModule R L N✝
N : LieSubmodule R L M
h : ⁅⊤, N⁆ = ⊥
m : M
hm : m ∈ N
⊢ ∀ (x : L), ⁅x, m⁆ = 0
[PROOFSTEP]
rw [LieSubmodule.lie_eq_bot_iff] at h
[GOAL]
case refine'_2
R : Type u
L : Type v
M : Type w
N✝ : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup N✝
inst✝² : Module R N✝
inst✝¹ : LieRingModule L N✝
inst✝ : LieModule R L N✝
N : LieSubmodule R L M
h : ∀ (x : L), x ∈ ⊤ → ∀ (m : M), m ∈ N → ⁅x, m⁆ = 0
m : M
hm : m ∈ N
⊢ ∀ (x : L), ⁅x, m⁆ = 0
[PROOFSTEP]
exact fun x => h x (LieSubmodule.mem_top x) m hm
[GOAL]
R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
⊢ IsTrivial L M ↔ maxTrivSubmodule R L M = ⊤
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
⊢ IsTrivial L M → maxTrivSubmodule R L M = ⊤
[PROOFSTEP]
rintro ⟨h⟩
[GOAL]
case mp.mk
R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
h : ∀ (x : L) (m : M), ⁅x, m⁆ = 0
⊢ maxTrivSubmodule R L M = ⊤
[PROOFSTEP]
ext
[GOAL]
case mp.mk.h
R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
h : ∀ (x : L) (m : M), ⁅x, m⁆ = 0
m✝ : M
⊢ m✝ ∈ maxTrivSubmodule R L M ↔ m✝ ∈ ⊤
[PROOFSTEP]
simp only [mem_maxTrivSubmodule, h, forall_const, LieSubmodule.mem_top]
[GOAL]
case mpr
R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
⊢ maxTrivSubmodule R L M = ⊤ → IsTrivial L M
[PROOFSTEP]
intro h
[GOAL]
case mpr
R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
h : maxTrivSubmodule R L M = ⊤
⊢ IsTrivial L M
[PROOFSTEP]
constructor
[GOAL]
case mpr.trivial
R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
h : maxTrivSubmodule R L M = ⊤
⊢ ∀ (x : L) (m : M), ⁅x, m⁆ = 0
[PROOFSTEP]
intro x m
[GOAL]
case mpr.trivial
R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
h : maxTrivSubmodule R L M = ⊤
x : L
m : M
⊢ ⁅x, m⁆ = 0
[PROOFSTEP]
revert x
[GOAL]
case mpr.trivial
R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
h : maxTrivSubmodule R L M = ⊤
m : M
⊢ ∀ (x : L), ⁅x, m⁆ = 0
[PROOFSTEP]
rw [← mem_maxTrivSubmodule R L M, h]
[GOAL]
case mpr.trivial
R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
h : maxTrivSubmodule R L M = ⊤
m : M
⊢ m ∈ ⊤
[PROOFSTEP]
exact LieSubmodule.mem_top m
[GOAL]
R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
f : M →ₗ⁅R,L⁆ N
m n : { x // x ∈ ↑(maxTrivSubmodule R L M) }
⊢ (fun m => { val := ↑f ↑m, property := (_ : ∀ (x : L), ⁅x, ↑f ↑m⁆ = 0) }) (m + n) =
    (fun m => { val := ↑f ↑m, property := (_ : ∀ (x : L), ⁅x, ↑f ↑m⁆ = 0) }) m +
      (fun m => { val := ↑f ↑m, property := (_ : ∀ (x : L), ⁅x, ↑f ↑m⁆ = 0) }) n
[PROOFSTEP]
simp [Function.comp_apply]
[GOAL]
R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
f : M →ₗ⁅R,L⁆ N
m n : { x // x ∈ ↑(maxTrivSubmodule R L M) }
⊢ { val := ↑f ↑m + ↑f ↑n, property := (_ : (fun x => x ∈ ↑(maxTrivSubmodule R L N)) (↑f ↑m + ↑f ↑n)) } =
    { val := ↑f ↑m, property := (_ : ∀ (x : L), ⁅x, ↑f ↑m⁆ = 0) } +
      { val := ↑f ↑n, property := (_ : ∀ (x : L), ⁅x, ↑f ↑n⁆ = 0) }
[PROOFSTEP]
rfl
  -- Porting note:
[GOAL]
R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
f : M →ₗ⁅R,L⁆ N
t : R
m : { x // x ∈ ↑(maxTrivSubmodule R L M) }
⊢ AddHom.toFun
      { toFun := fun m => { val := ↑f ↑m, property := (_ : ∀ (x : L), ⁅x, ↑f ↑m⁆ = 0) },
        map_add' :=
          (_ :
            ∀ (m n : { x // x ∈ ↑(maxTrivSubmodule R L M) }),
              (fun m => { val := ↑f ↑m, property := (_ : ∀ (x : L), ⁅x, ↑f ↑m⁆ = 0) }) (m + n) =
                (fun m => { val := ↑f ↑m, property := (_ : ∀ (x : L), ⁅x, ↑f ↑m⁆ = 0) }) m +
                  (fun m => { val := ↑f ↑m, property := (_ : ∀ (x : L), ⁅x, ↑f ↑m⁆ = 0) }) n) }
      (t • m) =
    ↑(RingHom.id R) t •
      AddHom.toFun
        { toFun := fun m => { val := ↑f ↑m, property := (_ : ∀ (x : L), ⁅x, ↑f ↑m⁆ = 0) },
          map_add' :=
            (_ :
              ∀ (m n : { x // x ∈ ↑(maxTrivSubmodule R L M) }),
                (fun m => { val := ↑f ↑m, property := (_ : ∀ (x : L), ⁅x, ↑f ↑m⁆ = 0) }) (m + n) =
                  (fun m => { val := ↑f ↑m, property := (_ : ∀ (x : L), ⁅x, ↑f ↑m⁆ = 0) }) m +
                    (fun m => { val := ↑f ↑m, property := (_ : ∀ (x : L), ⁅x, ↑f ↑m⁆ = 0) }) n) }
        m
[PROOFSTEP]
simp [Function.comp_apply]
[GOAL]
R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
f : M →ₗ⁅R,L⁆ N
t : R
m : { x // x ∈ ↑(maxTrivSubmodule R L M) }
⊢ { val := t • ↑f ↑m, property := (_ : (fun x => x ∈ ↑(maxTrivSubmodule R L N)) (t • ↑f ↑m)) } =
    t • { val := ↑f ↑m, property := (_ : ∀ (x : L), ⁅x, ↑f ↑m⁆ = 0) }
[PROOFSTEP]
rfl
  -- these two were `by simpa`
[GOAL]
R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
f : M →ₗ⁅R,L⁆ N
x : L
m : { x // x ∈ ↑(maxTrivSubmodule R L M) }
⊢ AddHom.toFun
      {
          toAddHom :=
            { toFun := fun m => { val := ↑f ↑m, property := (_ : ∀ (x : L), ⁅x, ↑f ↑m⁆ = 0) },
              map_add' :=
                (_ :
                  ∀ (m n : { x // x ∈ ↑(maxTrivSubmodule R L M) }),
                    (fun m => { val := ↑f ↑m, property := (_ : ∀ (x : L), ⁅x, ↑f ↑m⁆ = 0) }) (m + n) =
                      (fun m => { val := ↑f ↑m, property := (_ : ∀ (x : L), ⁅x, ↑f ↑m⁆ = 0) }) m +
                        (fun m => { val := ↑f ↑m, property := (_ : ∀ (x : L), ⁅x, ↑f ↑m⁆ = 0) }) n) },
          map_smul' :=
            (_ :
              ∀ (t : R) (m : { x // x ∈ ↑(maxTrivSubmodule R L M) }),
                AddHom.toFun
                    { toFun := fun m => { val := ↑f ↑m, property := (_ : ∀ (x : L), ⁅x, ↑f ↑m⁆ = 0) },
                      map_add' :=
                        (_ :
                          ∀ (m n : { x // x ∈ ↑(maxTrivSubmodule R L M) }),
                            (fun m => { val := ↑f ↑m, property := (_ : ∀ (x : L), ⁅x, ↑f ↑m⁆ = 0) }) (m + n) =
                              (fun m => { val := ↑f ↑m, property := (_ : ∀ (x : L), ⁅x, ↑f ↑m⁆ = 0) }) m +
                                (fun m => { val := ↑f ↑m, property := (_ : ∀ (x : L), ⁅x, ↑f ↑m⁆ = 0) }) n) }
                    (t • m) =
                  ↑(RingHom.id R) t •
                    AddHom.toFun
                      { toFun := fun m => { val := ↑f ↑m, property := (_ : ∀ (x : L), ⁅x, ↑f ↑m⁆ = 0) },
                        map_add' :=
                          (_ :
                            ∀ (m n : { x // x ∈ ↑(maxTrivSubmodule R L M) }),
                              (fun m => { val := ↑f ↑m, property := (_ : ∀ (x : L), ⁅x, ↑f ↑m⁆ = 0) }) (m + n) =
                                (fun m => { val := ↑f ↑m, property := (_ : ∀ (x : L), ⁅x, ↑f ↑m⁆ = 0) }) m +
                                  (fun m => { val := ↑f ↑m, property := (_ : ∀ (x : L), ⁅x, ↑f ↑m⁆ = 0) }) n) }
                      m) }.toAddHom
      ⁅x, m⁆ =
    ⁅x,
      AddHom.toFun
        {
            toAddHom :=
              { toFun := fun m => { val := ↑f ↑m, property := (_ : ∀ (x : L), ⁅x, ↑f ↑m⁆ = 0) },
                map_add' :=
                  (_ :
                    ∀ (m n : { x // x ∈ ↑(maxTrivSubmodule R L M) }),
                      (fun m => { val := ↑f ↑m, property := (_ : ∀ (x : L), ⁅x, ↑f ↑m⁆ = 0) }) (m + n) =
                        (fun m => { val := ↑f ↑m, property := (_ : ∀ (x : L), ⁅x, ↑f ↑m⁆ = 0) }) m +
                          (fun m => { val := ↑f ↑m, property := (_ : ∀ (x : L), ⁅x, ↑f ↑m⁆ = 0) }) n) },
            map_smul' :=
              (_ :
                ∀ (t : R) (m : { x // x ∈ ↑(maxTrivSubmodule R L M) }),
                  AddHom.toFun
                      { toFun := fun m => { val := ↑f ↑m, property := (_ : ∀ (x : L), ⁅x, ↑f ↑m⁆ = 0) },
                        map_add' :=
                          (_ :
                            ∀ (m n : { x // x ∈ ↑(maxTrivSubmodule R L M) }),
                              (fun m => { val := ↑f ↑m, property := (_ : ∀ (x : L), ⁅x, ↑f ↑m⁆ = 0) }) (m + n) =
                                (fun m => { val := ↑f ↑m, property := (_ : ∀ (x : L), ⁅x, ↑f ↑m⁆ = 0) }) m +
                                  (fun m => { val := ↑f ↑m, property := (_ : ∀ (x : L), ⁅x, ↑f ↑m⁆ = 0) }) n) }
                      (t • m) =
                    ↑(RingHom.id R) t •
                      AddHom.toFun
                        { toFun := fun m => { val := ↑f ↑m, property := (_ : ∀ (x : L), ⁅x, ↑f ↑m⁆ = 0) },
                          map_add' :=
                            (_ :
                              ∀ (m n : { x // x ∈ ↑(maxTrivSubmodule R L M) }),
                                (fun m => { val := ↑f ↑m, property := (_ : ∀ (x : L), ⁅x, ↑f ↑m⁆ = 0) }) (m + n) =
                                  (fun m => { val := ↑f ↑m, property := (_ : ∀ (x : L), ⁅x, ↑f ↑m⁆ = 0) }) m +
                                    (fun m => { val := ↑f ↑m, property := (_ : ∀ (x : L), ⁅x, ↑f ↑m⁆ = 0) }) n) }
                        m) }.toAddHom
        m⁆
[PROOFSTEP]
simp
[GOAL]
R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
e : M ≃ₗ⁅R,L⁆ N
src✝ : { x // x ∈ ↑(maxTrivSubmodule R L M) } →ₗ⁅R,L⁆ { x // x ∈ ↑(maxTrivSubmodule R L N) } :=
  maxTrivHom e.toLieModuleHom
m : { x // x ∈ ↑(maxTrivSubmodule R L M) }
⊢ ↑(maxTrivHom (LieModuleEquiv.symm e).toLieModuleHom)
      (AddHom.toFun
        (↑{
              toLinearMap :=
                {
                  toAddHom :=
                    { toFun := ↑(maxTrivHom e.toLieModuleHom),
                      map_add' :=
                        (_ :
                          ∀ (x y : { x // x ∈ ↑(maxTrivSubmodule R L M) }),
                            AddHom.toFun src✝.toAddHom (x + y) =
                              AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) },
                  map_smul' :=
                    (_ :
                      ∀ (r : R) (x : { x // x ∈ ↑(maxTrivSubmodule R L M) }),
                        AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) },
              map_lie' :=
                (_ :
                  ∀ {x : L} {m : { x // x ∈ ↑(maxTrivSubmodule R L M) }},
                    AddHom.toFun src✝.toAddHom ⁅x, m⁆ = ⁅x, AddHom.toFun src✝.toAddHom m⁆) }).toAddHom
        m) =
    m
[PROOFSTEP]
ext
[GOAL]
case a
R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
e : M ≃ₗ⁅R,L⁆ N
src✝ : { x // x ∈ ↑(maxTrivSubmodule R L M) } →ₗ⁅R,L⁆ { x // x ∈ ↑(maxTrivSubmodule R L N) } :=
  maxTrivHom e.toLieModuleHom
m : { x // x ∈ ↑(maxTrivSubmodule R L M) }
⊢ ↑(↑(maxTrivHom (LieModuleEquiv.symm e).toLieModuleHom)
        (AddHom.toFun
          (↑{
                toLinearMap :=
                  {
                    toAddHom :=
                      { toFun := ↑(maxTrivHom e.toLieModuleHom),
                        map_add' :=
                          (_ :
                            ∀ (x y : { x // x ∈ ↑(maxTrivSubmodule R L M) }),
                              AddHom.toFun src✝.toAddHom (x + y) =
                                AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) },
                    map_smul' :=
                      (_ :
                        ∀ (r : R) (x : { x // x ∈ ↑(maxTrivSubmodule R L M) }),
                          AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) },
                map_lie' :=
                  (_ :
                    ∀ {x : L} {m : { x // x ∈ ↑(maxTrivSubmodule R L M) }},
                      AddHom.toFun src✝.toAddHom ⁅x, m⁆ = ⁅x, AddHom.toFun src✝.toAddHom m⁆) }).toAddHom
          m)) =
    ↑m
[PROOFSTEP]
simp [LieModuleEquiv.coe_to_lieModuleHom]
[GOAL]
R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
e : M ≃ₗ⁅R,L⁆ N
src✝ : { x // x ∈ ↑(maxTrivSubmodule R L M) } →ₗ⁅R,L⁆ { x // x ∈ ↑(maxTrivSubmodule R L N) } :=
  maxTrivHom e.toLieModuleHom
n : { x // x ∈ ↑(maxTrivSubmodule R L N) }
⊢ AddHom.toFun
      (↑{
            toLinearMap :=
              {
                toAddHom :=
                  { toFun := ↑(maxTrivHom e.toLieModuleHom),
                    map_add' :=
                      (_ :
                        ∀ (x y : { x // x ∈ ↑(maxTrivSubmodule R L M) }),
                          AddHom.toFun src✝.toAddHom (x + y) =
                            AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) },
                map_smul' :=
                  (_ :
                    ∀ (r : R) (x : { x // x ∈ ↑(maxTrivSubmodule R L M) }),
                      AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) },
            map_lie' :=
              (_ :
                ∀ {x : L} {m : { x // x ∈ ↑(maxTrivSubmodule R L M) }},
                  AddHom.toFun src✝.toAddHom ⁅x, m⁆ = ⁅x, AddHom.toFun src✝.toAddHom m⁆) }).toAddHom
      (↑(maxTrivHom (LieModuleEquiv.symm e).toLieModuleHom) n) =
    n
[PROOFSTEP]
ext
[GOAL]
case a
R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
e : M ≃ₗ⁅R,L⁆ N
src✝ : { x // x ∈ ↑(maxTrivSubmodule R L M) } →ₗ⁅R,L⁆ { x // x ∈ ↑(maxTrivSubmodule R L N) } :=
  maxTrivHom e.toLieModuleHom
n : { x // x ∈ ↑(maxTrivSubmodule R L N) }
⊢ ↑(AddHom.toFun
        (↑{
              toLinearMap :=
                {
                  toAddHom :=
                    { toFun := ↑(maxTrivHom e.toLieModuleHom),
                      map_add' :=
                        (_ :
                          ∀ (x y : { x // x ∈ ↑(maxTrivSubmodule R L M) }),
                            AddHom.toFun src✝.toAddHom (x + y) =
                              AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) },
                  map_smul' :=
                    (_ :
                      ∀ (r : R) (x : { x // x ∈ ↑(maxTrivSubmodule R L M) }),
                        AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) },
              map_lie' :=
                (_ :
                  ∀ {x : L} {m : { x // x ∈ ↑(maxTrivSubmodule R L M) }},
                    AddHom.toFun src✝.toAddHom ⁅x, m⁆ = ⁅x, AddHom.toFun src✝.toAddHom m⁆) }).toAddHom
        (↑(maxTrivHom (LieModuleEquiv.symm e).toLieModuleHom) n)) =
    ↑n
[PROOFSTEP]
simp [LieModuleEquiv.coe_to_lieModuleHom]
[GOAL]
R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
⊢ maxTrivEquiv LieModuleEquiv.refl = LieModuleEquiv.refl
[PROOFSTEP]
ext
[GOAL]
case h.a
R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
m✝ : { x // x ∈ ↑(maxTrivSubmodule R L M) }
⊢ ↑(↑(maxTrivEquiv LieModuleEquiv.refl) m✝) = ↑(↑LieModuleEquiv.refl m✝)
[PROOFSTEP]
simp only [coe_maxTrivEquiv_apply, LieModuleEquiv.refl_apply]
[GOAL]
R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
f : { x // x ∈ ↑(maxTrivSubmodule R L (M →ₗ[R] N)) }
x : L
m : M
⊢ AddHom.toFun (↑f).toAddHom ⁅x, m⁆ = ⁅x, AddHom.toFun (↑f).toAddHom m⁆
[PROOFSTEP]
have hf : ⁅x, f.val⁆ m = 0 := by rw [f.property x, LinearMap.zero_apply]
[GOAL]
R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
f : { x // x ∈ ↑(maxTrivSubmodule R L (M →ₗ[R] N)) }
x : L
m : M
⊢ ↑⁅x, ↑f⁆ m = 0
[PROOFSTEP]
rw [f.property x, LinearMap.zero_apply]
[GOAL]
R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
f : { x // x ∈ ↑(maxTrivSubmodule R L (M →ₗ[R] N)) }
x : L
m : M
hf : ↑⁅x, ↑f⁆ m = 0
⊢ AddHom.toFun (↑f).toAddHom ⁅x, m⁆ = ⁅x, AddHom.toFun (↑f).toAddHom m⁆
[PROOFSTEP]
rw [LieHom.lie_apply, sub_eq_zero, ← LinearMap.toFun_eq_coe] at hf
[GOAL]
R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
f : { x // x ∈ ↑(maxTrivSubmodule R L (M →ₗ[R] N)) }
x : L
m : M
hf : ⁅x, AddHom.toFun (↑f).toAddHom m⁆ = AddHom.toFun (↑f).toAddHom ⁅x, m⁆
⊢ AddHom.toFun (↑f).toAddHom ⁅x, m⁆ = ⁅x, AddHom.toFun (↑f).toAddHom m⁆
[PROOFSTEP]
exact hf.symm
[GOAL]
R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
f g : { x // x ∈ ↑(maxTrivSubmodule R L (M →ₗ[R] N)) }
⊢ (fun f =>
        { toLinearMap := ↑f,
          map_lie' := (_ : ∀ {x : L} {m : M}, AddHom.toFun (↑f).toAddHom ⁅x, m⁆ = ⁅x, AddHom.toFun (↑f).toAddHom m⁆) })
      (f + g) =
    (fun f =>
          { toLinearMap := ↑f,
            map_lie' :=
              (_ : ∀ {x : L} {m : M}, AddHom.toFun (↑f).toAddHom ⁅x, m⁆ = ⁅x, AddHom.toFun (↑f).toAddHom m⁆) })
        f +
      (fun f =>
          { toLinearMap := ↑f,
            map_lie' :=
              (_ : ∀ {x : L} {m : M}, AddHom.toFun (↑f).toAddHom ⁅x, m⁆ = ⁅x, AddHom.toFun (↑f).toAddHom m⁆) })
        g
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
f g : { x // x ∈ ↑(maxTrivSubmodule R L (M →ₗ[R] N)) }
m✝ : M
⊢ ↑((fun f =>
            { toLinearMap := ↑f,
              map_lie' :=
                (_ : ∀ {x : L} {m : M}, AddHom.toFun (↑f).toAddHom ⁅x, m⁆ = ⁅x, AddHom.toFun (↑f).toAddHom m⁆) })
          (f + g))
      m✝ =
    ↑((fun f =>
              { toLinearMap := ↑f,
                map_lie' :=
                  (_ : ∀ {x : L} {m : M}, AddHom.toFun (↑f).toAddHom ⁅x, m⁆ = ⁅x, AddHom.toFun (↑f).toAddHom m⁆) })
            f +
          (fun f =>
              { toLinearMap := ↑f,
                map_lie' :=
                  (_ : ∀ {x : L} {m : M}, AddHom.toFun (↑f).toAddHom ⁅x, m⁆ = ⁅x, AddHom.toFun (↑f).toAddHom m⁆) })
            g)
      m✝
[PROOFSTEP]
simp
[GOAL]
R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
F : R
G : { x // x ∈ ↑(maxTrivSubmodule R L (M →ₗ[R] N)) }
⊢ AddHom.toFun
      {
        toFun := fun f =>
          { toLinearMap := ↑f,
            map_lie' :=
              (_ : ∀ {x : L} {m : M}, AddHom.toFun (↑f).toAddHom ⁅x, m⁆ = ⁅x, AddHom.toFun (↑f).toAddHom m⁆) },
        map_add' :=
          (_ :
            ∀ (f g : { x // x ∈ ↑(maxTrivSubmodule R L (M →ₗ[R] N)) }),
              (fun f =>
                    { toLinearMap := ↑f,
                      map_lie' :=
                        (_ :
                          ∀ {x : L} {m : M}, AddHom.toFun (↑f).toAddHom ⁅x, m⁆ = ⁅x, AddHom.toFun (↑f).toAddHom m⁆) })
                  (f + g) =
                (fun f =>
                      { toLinearMap := ↑f,
                        map_lie' :=
                          (_ :
                            ∀ {x : L} {m : M}, AddHom.toFun (↑f).toAddHom ⁅x, m⁆ = ⁅x, AddHom.toFun (↑f).toAddHom m⁆) })
                    f +
                  (fun f =>
                      { toLinearMap := ↑f,
                        map_lie' :=
                          (_ :
                            ∀ {x : L} {m : M}, AddHom.toFun (↑f).toAddHom ⁅x, m⁆ = ⁅x, AddHom.toFun (↑f).toAddHom m⁆) })
                    g) }
      (F • G) =
    ↑(RingHom.id R) F •
      AddHom.toFun
        {
          toFun := fun f =>
            { toLinearMap := ↑f,
              map_lie' :=
                (_ : ∀ {x : L} {m : M}, AddHom.toFun (↑f).toAddHom ⁅x, m⁆ = ⁅x, AddHom.toFun (↑f).toAddHom m⁆) },
          map_add' :=
            (_ :
              ∀ (f g : { x // x ∈ ↑(maxTrivSubmodule R L (M →ₗ[R] N)) }),
                (fun f =>
                      { toLinearMap := ↑f,
                        map_lie' :=
                          (_ :
                            ∀ {x : L} {m : M}, AddHom.toFun (↑f).toAddHom ⁅x, m⁆ = ⁅x, AddHom.toFun (↑f).toAddHom m⁆) })
                    (f + g) =
                  (fun f =>
                        { toLinearMap := ↑f,
                          map_lie' :=
                            (_ :
                              ∀ {x : L} {m : M},
                                AddHom.toFun (↑f).toAddHom ⁅x, m⁆ = ⁅x, AddHom.toFun (↑f).toAddHom m⁆) })
                      f +
                    (fun f =>
                        { toLinearMap := ↑f,
                          map_lie' :=
                            (_ :
                              ∀ {x : L} {m : M},
                                AddHom.toFun (↑f).toAddHom ⁅x, m⁆ = ⁅x, AddHom.toFun (↑f).toAddHom m⁆) })
                      g) }
        G
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
F : R
G : { x // x ∈ ↑(maxTrivSubmodule R L (M →ₗ[R] N)) }
m✝ : M
⊢ ↑(AddHom.toFun
          {
            toFun := fun f =>
              { toLinearMap := ↑f,
                map_lie' :=
                  (_ : ∀ {x : L} {m : M}, AddHom.toFun (↑f).toAddHom ⁅x, m⁆ = ⁅x, AddHom.toFun (↑f).toAddHom m⁆) },
            map_add' :=
              (_ :
                ∀ (f g : { x // x ∈ ↑(maxTrivSubmodule R L (M →ₗ[R] N)) }),
                  (fun f =>
                        { toLinearMap := ↑f,
                          map_lie' :=
                            (_ :
                              ∀ {x : L} {m : M},
                                AddHom.toFun (↑f).toAddHom ⁅x, m⁆ = ⁅x, AddHom.toFun (↑f).toAddHom m⁆) })
                      (f + g) =
                    (fun f =>
                          { toLinearMap := ↑f,
                            map_lie' :=
                              (_ :
                                ∀ {x : L} {m : M},
                                  AddHom.toFun (↑f).toAddHom ⁅x, m⁆ = ⁅x, AddHom.toFun (↑f).toAddHom m⁆) })
                        f +
                      (fun f =>
                          { toLinearMap := ↑f,
                            map_lie' :=
                              (_ :
                                ∀ {x : L} {m : M},
                                  AddHom.toFun (↑f).toAddHom ⁅x, m⁆ = ⁅x, AddHom.toFun (↑f).toAddHom m⁆) })
                        g) }
          (F • G))
      m✝ =
    ↑(↑(RingHom.id R) F •
          AddHom.toFun
            {
              toFun := fun f =>
                { toLinearMap := ↑f,
                  map_lie' :=
                    (_ : ∀ {x : L} {m : M}, AddHom.toFun (↑f).toAddHom ⁅x, m⁆ = ⁅x, AddHom.toFun (↑f).toAddHom m⁆) },
              map_add' :=
                (_ :
                  ∀ (f g : { x // x ∈ ↑(maxTrivSubmodule R L (M →ₗ[R] N)) }),
                    (fun f =>
                          { toLinearMap := ↑f,
                            map_lie' :=
                              (_ :
                                ∀ {x : L} {m : M},
                                  AddHom.toFun (↑f).toAddHom ⁅x, m⁆ = ⁅x, AddHom.toFun (↑f).toAddHom m⁆) })
                        (f + g) =
                      (fun f =>
                            { toLinearMap := ↑f,
                              map_lie' :=
                                (_ :
                                  ∀ {x : L} {m : M},
                                    AddHom.toFun (↑f).toAddHom ⁅x, m⁆ = ⁅x, AddHom.toFun (↑f).toAddHom m⁆) })
                          f +
                        (fun f =>
                            { toLinearMap := ↑f,
                              map_lie' :=
                                (_ :
                                  ∀ {x : L} {m : M},
                                    AddHom.toFun (↑f).toAddHom ⁅x, m⁆ = ⁅x, AddHom.toFun (↑f).toAddHom m⁆) })
                          g) }
            G)
      m✝
[PROOFSTEP]
simp
[GOAL]
R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
F : M →ₗ⁅R,L⁆ N
x : L
⊢ ⁅x, ↑F⁆ = 0
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
F : M →ₗ⁅R,L⁆ N
x : L
x✝ : M
⊢ ↑⁅x, ↑F⁆ x✝ = ↑0 x✝
[PROOFSTEP]
simp
[GOAL]
R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
f : { x // x ∈ ↑(maxTrivSubmodule R L (M →ₗ[R] N)) }
⊢ (fun F => { val := ↑F, property := (_ : ∀ (x : L), ⁅x, ↑F⁆ = 0) })
      (AddHom.toFun
        {
            toAddHom :=
              {
                toFun := fun f =>
                  { toLinearMap := ↑f,
                    map_lie' :=
                      (_ : ∀ {x : L} {m : M}, AddHom.toFun (↑f).toAddHom ⁅x, m⁆ = ⁅x, AddHom.toFun (↑f).toAddHom m⁆) },
                map_add' :=
                  (_ :
                    ∀ (f g : { x // x ∈ ↑(maxTrivSubmodule R L (M →ₗ[R] N)) }),
                      (fun f =>
                            { toLinearMap := ↑f,
                              map_lie' :=
                                (_ :
                                  ∀ {x : L} {m : M},
                                    AddHom.toFun (↑f).toAddHom ⁅x, m⁆ = ⁅x, AddHom.toFun (↑f).toAddHom m⁆) })
                          (f + g) =
                        (fun f =>
                              { toLinearMap := ↑f,
                                map_lie' :=
                                  (_ :
                                    ∀ {x : L} {m : M},
                                      AddHom.toFun (↑f).toAddHom ⁅x, m⁆ = ⁅x, AddHom.toFun (↑f).toAddHom m⁆) })
                            f +
                          (fun f =>
                              { toLinearMap := ↑f,
                                map_lie' :=
                                  (_ :
                                    ∀ {x : L} {m : M},
                                      AddHom.toFun (↑f).toAddHom ⁅x, m⁆ = ⁅x, AddHom.toFun (↑f).toAddHom m⁆) })
                            g) },
            map_smul' :=
              (_ :
                ∀ (F : R) (G : { x // x ∈ ↑(maxTrivSubmodule R L (M →ₗ[R] N)) }),
                  AddHom.toFun
                      {
                        toFun := fun f =>
                          { toLinearMap := ↑f,
                            map_lie' :=
                              (_ :
                                ∀ {x : L} {m : M},
                                  AddHom.toFun (↑f).toAddHom ⁅x, m⁆ = ⁅x, AddHom.toFun (↑f).toAddHom m⁆) },
                        map_add' :=
                          (_ :
                            ∀ (f g : { x // x ∈ ↑(maxTrivSubmodule R L (M →ₗ[R] N)) }),
                              (fun f =>
                                    { toLinearMap := ↑f,
                                      map_lie' :=
                                        (_ :
                                          ∀ {x : L} {m : M},
                                            AddHom.toFun (↑f).toAddHom ⁅x, m⁆ = ⁅x, AddHom.toFun (↑f).toAddHom m⁆) })
                                  (f + g) =
                                (fun f =>
                                      { toLinearMap := ↑f,
                                        map_lie' :=
                                          (_ :
                                            ∀ {x : L} {m : M},
                                              AddHom.toFun (↑f).toAddHom ⁅x, m⁆ = ⁅x, AddHom.toFun (↑f).toAddHom m⁆) })
                                    f +
                                  (fun f =>
                                      { toLinearMap := ↑f,
                                        map_lie' :=
                                          (_ :
                                            ∀ {x : L} {m : M},
                                              AddHom.toFun (↑f).toAddHom ⁅x, m⁆ = ⁅x, AddHom.toFun (↑f).toAddHom m⁆) })
                                    g) }
                      (F • G) =
                    ↑(RingHom.id R) F •
                      AddHom.toFun
                        {
                          toFun := fun f =>
                            { toLinearMap := ↑f,
                              map_lie' :=
                                (_ :
                                  ∀ {x : L} {m : M},
                                    AddHom.toFun (↑f).toAddHom ⁅x, m⁆ = ⁅x, AddHom.toFun (↑f).toAddHom m⁆) },
                          map_add' :=
                            (_ :
                              ∀ (f g : { x // x ∈ ↑(maxTrivSubmodule R L (M →ₗ[R] N)) }),
                                (fun f =>
                                      { toLinearMap := ↑f,
                                        map_lie' :=
                                          (_ :
                                            ∀ {x : L} {m : M},
                                              AddHom.toFun (↑f).toAddHom ⁅x, m⁆ = ⁅x, AddHom.toFun (↑f).toAddHom m⁆) })
                                    (f + g) =
                                  (fun f =>
                                        { toLinearMap := ↑f,
                                          map_lie' :=
                                            (_ :
                                              ∀ {x : L} {m : M},
                                                AddHom.toFun (↑f).toAddHom ⁅x, m⁆ =
                                                  ⁅x, AddHom.toFun (↑f).toAddHom m⁆) })
                                      f +
                                    (fun f =>
                                        { toLinearMap := ↑f,
                                          map_lie' :=
                                            (_ :
                                              ∀ {x : L} {m : M},
                                                AddHom.toFun (↑f).toAddHom ⁅x, m⁆ =
                                                  ⁅x, AddHom.toFun (↑f).toAddHom m⁆) })
                                      g) }
                        G) }.toAddHom
        f) =
    f
[PROOFSTEP]
simp
[GOAL]
R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
F : M →ₗ⁅R,L⁆ N
⊢ AddHom.toFun
      {
          toAddHom :=
            {
              toFun := fun f =>
                { toLinearMap := ↑f,
                  map_lie' :=
                    (_ : ∀ {x : L} {m : M}, AddHom.toFun (↑f).toAddHom ⁅x, m⁆ = ⁅x, AddHom.toFun (↑f).toAddHom m⁆) },
              map_add' :=
                (_ :
                  ∀ (f g : { x // x ∈ ↑(maxTrivSubmodule R L (M →ₗ[R] N)) }),
                    (fun f =>
                          { toLinearMap := ↑f,
                            map_lie' :=
                              (_ :
                                ∀ {x : L} {m : M},
                                  AddHom.toFun (↑f).toAddHom ⁅x, m⁆ = ⁅x, AddHom.toFun (↑f).toAddHom m⁆) })
                        (f + g) =
                      (fun f =>
                            { toLinearMap := ↑f,
                              map_lie' :=
                                (_ :
                                  ∀ {x : L} {m : M},
                                    AddHom.toFun (↑f).toAddHom ⁅x, m⁆ = ⁅x, AddHom.toFun (↑f).toAddHom m⁆) })
                          f +
                        (fun f =>
                            { toLinearMap := ↑f,
                              map_lie' :=
                                (_ :
                                  ∀ {x : L} {m : M},
                                    AddHom.toFun (↑f).toAddHom ⁅x, m⁆ = ⁅x, AddHom.toFun (↑f).toAddHom m⁆) })
                          g) },
          map_smul' :=
            (_ :
              ∀ (F : R) (G : { x // x ∈ ↑(maxTrivSubmodule R L (M →ₗ[R] N)) }),
                AddHom.toFun
                    {
                      toFun := fun f =>
                        { toLinearMap := ↑f,
                          map_lie' :=
                            (_ :
                              ∀ {x : L} {m : M},
                                AddHom.toFun (↑f).toAddHom ⁅x, m⁆ = ⁅x, AddHom.toFun (↑f).toAddHom m⁆) },
                      map_add' :=
                        (_ :
                          ∀ (f g : { x // x ∈ ↑(maxTrivSubmodule R L (M →ₗ[R] N)) }),
                            (fun f =>
                                  { toLinearMap := ↑f,
                                    map_lie' :=
                                      (_ :
                                        ∀ {x : L} {m : M},
                                          AddHom.toFun (↑f).toAddHom ⁅x, m⁆ = ⁅x, AddHom.toFun (↑f).toAddHom m⁆) })
                                (f + g) =
                              (fun f =>
                                    { toLinearMap := ↑f,
                                      map_lie' :=
                                        (_ :
                                          ∀ {x : L} {m : M},
                                            AddHom.toFun (↑f).toAddHom ⁅x, m⁆ = ⁅x, AddHom.toFun (↑f).toAddHom m⁆) })
                                  f +
                                (fun f =>
                                    { toLinearMap := ↑f,
                                      map_lie' :=
                                        (_ :
                                          ∀ {x : L} {m : M},
                                            AddHom.toFun (↑f).toAddHom ⁅x, m⁆ = ⁅x, AddHom.toFun (↑f).toAddHom m⁆) })
                                  g) }
                    (F • G) =
                  ↑(RingHom.id R) F •
                    AddHom.toFun
                      {
                        toFun := fun f =>
                          { toLinearMap := ↑f,
                            map_lie' :=
                              (_ :
                                ∀ {x : L} {m : M},
                                  AddHom.toFun (↑f).toAddHom ⁅x, m⁆ = ⁅x, AddHom.toFun (↑f).toAddHom m⁆) },
                        map_add' :=
                          (_ :
                            ∀ (f g : { x // x ∈ ↑(maxTrivSubmodule R L (M →ₗ[R] N)) }),
                              (fun f =>
                                    { toLinearMap := ↑f,
                                      map_lie' :=
                                        (_ :
                                          ∀ {x : L} {m : M},
                                            AddHom.toFun (↑f).toAddHom ⁅x, m⁆ = ⁅x, AddHom.toFun (↑f).toAddHom m⁆) })
                                  (f + g) =
                                (fun f =>
                                      { toLinearMap := ↑f,
                                        map_lie' :=
                                          (_ :
                                            ∀ {x : L} {m : M},
                                              AddHom.toFun (↑f).toAddHom ⁅x, m⁆ = ⁅x, AddHom.toFun (↑f).toAddHom m⁆) })
                                    f +
                                  (fun f =>
                                      { toLinearMap := ↑f,
                                        map_lie' :=
                                          (_ :
                                            ∀ {x : L} {m : M},
                                              AddHom.toFun (↑f).toAddHom ⁅x, m⁆ = ⁅x, AddHom.toFun (↑f).toAddHom m⁆) })
                                    g) }
                      G) }.toAddHom
      ((fun F => { val := ↑F, property := (_ : ∀ (x : L), ⁅x, ↑F⁆ = 0) }) F) =
    F
[PROOFSTEP]
simp
[GOAL]
R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
f : { x // x ∈ maxTrivSubmodule R L (M →ₗ[R] N) }
⊢ ↑(↑maxTrivLinearMapEquivLieModuleHom f) = ↑↑f
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
f : { x // x ∈ maxTrivSubmodule R L (M →ₗ[R] N) }
x✝ : M
⊢ ↑(↑maxTrivLinearMapEquivLieModuleHom f) x✝ = ↑↑f x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
f : { x // x ∈ maxTrivSubmodule R L (M →ₗ[R] N) }
⊢ ↑(↑maxTrivLinearMapEquivLieModuleHom f) = ↑f
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
f : { x // x ∈ maxTrivSubmodule R L (M →ₗ[R] N) }
x✝ : M
⊢ ↑↑(↑maxTrivLinearMapEquivLieModuleHom f) x✝ = ↑↑f x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
⊢ LieModule.ker R L L = center R L
[PROOFSTEP]
ext y
[GOAL]
case h
R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
y : L
⊢ y ∈ LieModule.ker R L L ↔ y ∈ center R L
[PROOFSTEP]
simp only [LieModule.mem_maxTrivSubmodule, LieModule.mem_ker, ← lie_skew _ y, neg_eq_zero]
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
N N' : LieSubmodule R L M
I J : LieIdeal R L
inst✝ : LieModule.IsTrivial L M
⊢ ⁅I, N⁆ = ⊥
[PROOFSTEP]
suffices : ⁅I, N⁆ ≤ ⊥
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
N N' : LieSubmodule R L M
I J : LieIdeal R L
inst✝ : LieModule.IsTrivial L M
this : ⁅I, N⁆ ≤ ⊥
⊢ ⁅I, N⁆ = ⊥
case this
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
N N' : LieSubmodule R L M
I J : LieIdeal R L
inst✝ : LieModule.IsTrivial L M
⊢ ⁅I, N⁆ ≤ ⊥
[PROOFSTEP]
exact le_bot_iff.mp this
[GOAL]
case this
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
N N' : LieSubmodule R L M
I J : LieIdeal R L
inst✝ : LieModule.IsTrivial L M
⊢ ⁅I, N⁆ ≤ ⊥
[PROOFSTEP]
rw [lieIdeal_oper_eq_span, LieSubmodule.lieSpan_le]
[GOAL]
case this
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
N N' : LieSubmodule R L M
I J : LieIdeal R L
inst✝ : LieModule.IsTrivial L M
⊢ {m | ∃ x n, ⁅↑x, ↑n⁆ = m} ⊆ ↑⊥
[PROOFSTEP]
rintro m ⟨x, n, h⟩
[GOAL]
case this.intro.intro
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
N N' : LieSubmodule R L M
I J : LieIdeal R L
inst✝ : LieModule.IsTrivial L M
m : M
x : { x // x ∈ I }
n : { x // x ∈ N }
h : ⁅↑x, ↑n⁆ = m
⊢ m ∈ ↑⊥
[PROOFSTEP]
rw [trivial_lie_zero] at h
[GOAL]
case this.intro.intro
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
N N' : LieSubmodule R L M
I J : LieIdeal R L
inst✝ : LieModule.IsTrivial L M
m : M
x : { x // x ∈ I }
n : { x // x ∈ N }
h : 0 = m
⊢ m ∈ ↑⊥
[PROOFSTEP]
simp [← h]
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N N' : LieSubmodule R L M
I J : LieIdeal R L
⊢ IsLieAbelian { x // x ∈ ↑I } ↔ ⁅I, I⁆ = ⊥
[PROOFSTEP]
simp only [_root_.eq_bot_iff, lieIdeal_oper_eq_span, LieSubmodule.lieSpan_le, LieSubmodule.bot_coe,
  Set.subset_singleton_iff, Set.mem_setOf_eq, exists_imp]
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N N' : LieSubmodule R L M
I J : LieIdeal R L
⊢ IsLieAbelian { x // x ∈ ↑I } ↔ ∀ (y : L) (x : { x // x ∈ I }) (x_1 : { x // x ∈ I }), ⁅↑x, ↑x_1⁆ = y → y = 0
[PROOFSTEP]
refine'
  ⟨fun h z x y hz =>
    hz.symm.trans
      (((I : LieSubalgebra R L).coe_bracket x y).symm.trans ((coe_zero_iff_zero _ _).mpr (by apply h.trivial))),
    fun h => ⟨fun x y => ((I : LieSubalgebra R L).coe_zero_iff_zero _).mp (h _ x y rfl)⟩⟩
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N N' : LieSubmodule R L M
I J : LieIdeal R L
h : IsLieAbelian { x // x ∈ ↑I }
z : L
x : { x // x ∈ I }
y : { x // x ∈ I }
hz : ⁅↑x, ↑y⁆ = z
⊢ ⁅x, y⁆ = 0
[PROOFSTEP]
apply h.trivial