text:
/-
Copyright (c) 2021 Floris van Doorn. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Floris van Doorn

! This file was ported from Lean 3 source module data.int.conditionally_complete_order
! leanprover-community/mathlib commit c3291da49cfa65f0d43b094750541c0731edc932
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathbin.Order.ConditionallyCompleteLattice.Basic
import Mathbin.Data.Int.LeastGreatest

/-!
## `ℤ` forms a conditionally complete linear order

> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
> Any changes to this file require a corresponding PR to mathlib4.

The integers form a conditionally complete linear order.
-/

open Int

open Classical

noncomputable section

instance : ConditionallyCompleteLinearOrder ℤ :=
  { Int.linearOrder,
    LinearOrder.toLattice with
    supₛ := fun s =>
      if h : s.Nonempty ∧ BddAbove s then
        greatestOfBdd (Classical.choose h.2) (Classical.choose_spec h.2) h.1
      else 0
    infₛ := fun s =>
      if h : s.Nonempty ∧ BddBelow s then
        leastOfBdd (Classical.choose h.2) (Classical.choose_spec h.2) h.1
      else 0
    le_cSup := by
      intro s n hs hns
      have : s.nonempty ∧ BddAbove s := ⟨⟨n, hns⟩, hs⟩
      rw [dif_pos this]
      exact (greatest_of_bdd _ _ _).2.2 n hns
    cSup_le := by
      intro s n hs hns
      have : s.nonempty ∧ BddAbove s := ⟨hs, ⟨n, hns⟩⟩
      rw [dif_pos this]
      exact hns (greatest_of_bdd _ (Classical.choose_spec this.2) _).2.1
    cInf_le := by
      intro s n hs hns
      have : s.nonempty ∧ BddBelow s := ⟨⟨n, hns⟩, hs⟩
      rw [dif_pos this]
      exact (least_of_bdd _ _ _).2.2 n hns
    le_cInf := by
      intro s n hs hns
      have : s.nonempty ∧ BddBelow s := ⟨hs, ⟨n, hns⟩⟩
      rw [dif_pos this]
      exact hns (least_of_bdd _ (Classical.choose_spec this.2) _).2.1 }

namespace Int

/- warning: int.cSup_eq_greatest_of_bdd -> Int.csupₛ_eq_greatest_of_bdd is a dubious translation:
lean 3 declaration is
  forall {s : Set.{0} Int} [_inst_1 : DecidablePred.{1} Int (fun (_x : Int) => Membership.Mem.{0, 0} Int (Set.{0} Int) (Set.hasMem.{0} Int) _x s)] (b : Int) (Hb : forall (z : Int), (Membership.Mem.{0, 0} Int (Set.{0} Int) (Set.hasMem.{0} Int) z s) -> (LE.le.{0} Int Int.hasLe z b)) (Hinh : Exists.{1} Int (fun (z : Int) => Membership.Mem.{0, 0} Int (Set.{0} Int) (Set.hasMem.{0} Int) z s)), Eq.{1} Int (SupSet.supₛ.{0} Int (ConditionallyCompleteLattice.toHasSup.{0} Int (ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice.{0} Int Int.conditionallyCompleteLinearOrder)) s) ((fun (a : Type) (b : Type) [self : HasLiftT.{1, 1} a b] => self.0) (Subtype.{1} Int (fun (ub : Int) => And (Membership.Mem.{0, 0} Int (Set.{0} Int) (Set.hasMem.{0} Int) ub s) (forall (z : Int), (Membership.Mem.{0, 0} Int (Set.{0} Int) (Set.hasMem.{0} Int) z s) -> (LE.le.{0} Int Int.hasLe z ub)))) Int (HasLiftT.mk.{1, 1} (Subtype.{1} Int (fun (ub : Int) => And (Membership.Mem.{0, 0} Int (Set.{0} Int) (Set.hasMem.{0} Int) ub s) (forall (z : Int), (Membership.Mem.{0, 0} Int (Set.{0} Int) (Set.hasMem.{0} Int) z s) -> (LE.le.{0} Int Int.hasLe z ub)))) Int (CoeTCₓ.coe.{1, 1} (Subtype.{1} Int (fun (ub : Int) => And (Membership.Mem.{0, 0} Int (Set.{0} Int) (Set.hasMem.{0} Int) ub s) (forall (z : Int), (Membership.Mem.{0, 0} Int (Set.{0} Int) (Set.hasMem.{0} Int) z s) -> (LE.le.{0} Int Int.hasLe z ub)))) Int (coeBase.{1, 1} (Subtype.{1} Int (fun (ub : Int) => And (Membership.Mem.{0, 0} Int (Set.{0} Int) (Set.hasMem.{0} Int) ub s) (forall (z : Int), (Membership.Mem.{0, 0} Int (Set.{0} Int) (Set.hasMem.{0} Int) z s) -> (LE.le.{0} Int Int.hasLe z ub)))) Int (coeSubtype.{1} Int (fun (ub : Int) => And (Membership.Mem.{0, 0} Int (Set.{0} Int) (Set.hasMem.{0} Int) ub s) (forall (z : Int), (Membership.Mem.{0, 0} Int (Set.{0} Int) (Set.hasMem.{0} Int) z s) -> (LE.le.{0} Int Int.hasLe z ub))))))) (Int.greatestOfBdd (fun (z : Int) => Membership.Mem.{0, 0} Int (Set.{0} Int) (Set.hasMem.{0} Int) z s) (fun (a : Int) => _inst_1 a) b Hb Hinh))
but is expected to have type
  forall {s : Set.{0} Int} [_inst_1 : DecidablePred.{1} Int (fun (_x : Int) => Membership.mem.{0, 0} Int (Set.{0} Int) (Set.instMembershipSet.{0} Int) _x s)] (b : Int) (Hb : forall (z : Int), (Membership.mem.{0, 0} Int (Set.{0} Int) (Set.instMembershipSet.{0} Int) z s) -> (LE.le.{0} Int Int.instLEInt z b)) (Hinh : Exists.{1} Int (fun (z : Int) => Membership.mem.{0, 0} Int (Set.{0} Int) (Set.instMembershipSet.{0} Int) z s)), Eq.{1} Int (SupSet.supₛ.{0} Int (ConditionallyCompleteLattice.toSupSet.{0} Int (ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice.{0} Int instConditionallyCompleteLinearOrderInt)) s) (Subtype.val.{1} Int (fun (ub : Int) => And (Membership.mem.{0, 0} Int (Set.{0} Int) (Set.instMembershipSet.{0} Int) ub s) (forall (z : Int), (Membership.mem.{0, 0} Int (Set.{0} Int) (Set.instMembershipSet.{0} Int) z s) -> (LE.le.{0} Int Int.instLEInt z ub))) (Int.greatestOfBdd (fun (z : Int) => Membership.mem.{0, 0} Int (Set.{0} Int) (Set.instMembershipSet.{0} Int) z s) (fun (a : Int) => _inst_1 a) b Hb Hinh))
Case conversion may be inaccurate. Consider using '#align int.cSup_eq_greatest_of_bdd Int.csupₛ_eq_greatest_of_bddₓ'. -/
theorem csupₛ_eq_greatest_of_bdd {s : Set ℤ} [DecidablePred (· ∈ s)] (b : ℤ) (Hb : ∀ z ∈ s, z ≤ b)
    (Hinh : ∃ z : ℤ, z ∈ s) : supₛ s = greatestOfBdd b Hb Hinh :=
  by
  convert dif_pos _ using 1
  · convert coe_greatest_of_bdd_eq _ (Classical.choose_spec (⟨b, Hb⟩ : BddAbove s)) _
  · exact ⟨Hinh, b, Hb⟩
#align int.cSup_eq_greatest_of_bdd Int.csupₛ_eq_greatest_of_bdd

/- warning: int.cSup_empty -> Int.csupₛ_empty is a dubious translation:
lean 3 declaration is
  Eq.{1} Int (SupSet.supₛ.{0} Int (ConditionallyCompleteLattice.toHasSup.{0} Int (ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice.{0} Int Int.conditionallyCompleteLinearOrder)) (EmptyCollection.emptyCollection.{0} (Set.{0} Int) (Set.hasEmptyc.{0} Int))) (OfNat.ofNat.{0} Int 0 (OfNat.mk.{0} Int 0 (Zero.zero.{0} Int Int.hasZero)))
but is expected to have type
  Eq.{1} Int (SupSet.supₛ.{0} Int (ConditionallyCompleteLattice.toSupSet.{0} Int (ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice.{0} Int instConditionallyCompleteLinearOrderInt)) (EmptyCollection.emptyCollection.{0} (Set.{0} Int) (Set.instEmptyCollectionSet.{0} Int))) (OfNat.ofNat.{0} Int 0 (instOfNatInt 0))
Case conversion may be inaccurate. Consider using '#align int.cSup_empty Int.csupₛ_emptyₓ'. -/
@[simp]
theorem csupₛ_empty : supₛ (∅ : Set ℤ) = 0 :=
  dif_neg (by simp)
#align int.cSup_empty Int.csupₛ_empty

/- warning: int.cSup_of_not_bdd_above -> Int.csupₛ_of_not_bdd_above is a dubious translation:
lean 3 declaration is
  forall {s : Set.{0} Int}, (Not (BddAbove.{0} Int (PartialOrder.toPreorder.{0} Int (OrderedAddCommGroup.toPartialOrder.{0} Int (StrictOrderedRing.toOrderedAddCommGroup.{0} Int (LinearOrderedRing.toStrictOrderedRing.{0} Int (LinearOrderedCommRing.toLinearOrderedRing.{0} Int Int.linearOrderedCommRing))))) s)) -> (Eq.{1} Int (SupSet.supₛ.{0} Int (ConditionallyCompleteLattice.toHasSup.{0} Int (ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice.{0} Int Int.conditionallyCompleteLinearOrder)) s) (OfNat.ofNat.{0} Int 0 (OfNat.mk.{0} Int 0 (Zero.zero.{0} Int Int.hasZero))))
but is expected to have type
  forall {s : Set.{0} Int}, (Not (BddAbove.{0} Int (PartialOrder.toPreorder.{0} Int (StrictOrderedRing.toPartialOrder.{0} Int (LinearOrderedRing.toStrictOrderedRing.{0} Int (LinearOrderedCommRing.toLinearOrderedRing.{0} Int Int.linearOrderedCommRing)))) s)) -> (Eq.{1} Int (SupSet.supₛ.{0} Int (ConditionallyCompleteLattice.toSupSet.{0} Int (ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice.{0} Int instConditionallyCompleteLinearOrderInt)) s) (OfNat.ofNat.{0} Int 0 (instOfNatInt 0)))
Case conversion may be inaccurate. Consider using '#align int.cSup_of_not_bdd_above Int.csupₛ_of_not_bdd_aboveₓ'. -/
theorem csupₛ_of_not_bdd_above {s : Set ℤ} (h : ¬BddAbove s) : supₛ s = 0 :=
  dif_neg (by simp [h])
#align int.cSup_of_not_bdd_above Int.csupₛ_of_not_bdd_above

/- warning: int.cInf_eq_least_of_bdd -> Int.cinfₛ_eq_least_of_bdd is a dubious translation:
lean 3 declaration is
  forall {s : Set.{0} Int} [_inst_1 : DecidablePred.{1} Int (fun (_x : Int) => Membership.Mem.{0, 0} Int (Set.{0} Int) (Set.hasMem.{0} Int) _x s)] (b : Int) (Hb : forall (z : Int), (Membership.Mem.{0, 0} Int (Set.{0} Int) (Set.hasMem.{0} Int) z s) -> (LE.le.{0} Int Int.hasLe b z)) (Hinh : Exists.{1} Int (fun (z : Int) => Membership.Mem.{0, 0} Int (Set.{0} Int) (Set.hasMem.{0} Int) z s)), Eq.{1} Int (InfSet.infₛ.{0} Int (ConditionallyCompleteLattice.toHasInf.{0} Int (ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice.{0} Int Int.conditionallyCompleteLinearOrder)) s) ((fun (a : Type) (b : Type) [self : HasLiftT.{1, 1} a b] => self.0) (Subtype.{1} Int (fun (lb : Int) => And (Membership.Mem.{0, 0} Int (Set.{0} Int) (Set.hasMem.{0} Int) lb s) (forall (z : Int), (Membership.Mem.{0, 0} Int (Set.{0} Int) (Set.hasMem.{0} Int) z s) -> (LE.le.{0} Int Int.hasLe lb z)))) Int (HasLiftT.mk.{1, 1} (Subtype.{1} Int (fun (lb : Int) => And (Membership.Mem.{0, 0} Int (Set.{0} Int) (Set.hasMem.{0} Int) lb s) (forall (z : Int), (Membership.Mem.{0, 0} Int (Set.{0} Int) (Set.hasMem.{0} Int) z s) -> (LE.le.{0} Int Int.hasLe lb z)))) Int (CoeTCₓ.coe.{1, 1} (Subtype.{1} Int (fun (lb : Int) => And (Membership.Mem.{0, 0} Int (Set.{0} Int) (Set.hasMem.{0} Int) lb s) (forall (z : Int), (Membership.Mem.{0, 0} Int (Set.{0} Int) (Set.hasMem.{0} Int) z s) -> (LE.le.{0} Int Int.hasLe lb z)))) Int (coeBase.{1, 1} (Subtype.{1} Int (fun (lb : Int) => And (Membership.Mem.{0, 0} Int (Set.{0} Int) (Set.hasMem.{0} Int) lb s) (forall (z : Int), (Membership.Mem.{0, 0} Int (Set.{0} Int) (Set.hasMem.{0} Int) z s) -> (LE.le.{0} Int Int.hasLe lb z)))) Int (coeSubtype.{1} Int (fun (lb : Int) => And (Membership.Mem.{0, 0} Int (Set.{0} Int) (Set.hasMem.{0} Int) lb s) (forall (z : Int), (Membership.Mem.{0, 0} Int (Set.{0} Int) (Set.hasMem.{0} Int) z s) -> (LE.le.{0} Int Int.hasLe lb z))))))) (Int.leastOfBdd (fun (z : Int) => Membership.Mem.{0, 0} Int (Set.{0} Int) (Set.hasMem.{0} Int) z s) (fun (a : Int) => _inst_1 a) b Hb Hinh))
but is expected to have type
  forall {s : Set.{0} Int} [_inst_1 : DecidablePred.{1} Int (fun (_x : Int) => Membership.mem.{0, 0} Int (Set.{0} Int) (Set.instMembershipSet.{0} Int) _x s)] (b : Int) (Hb : forall (z : Int), (Membership.mem.{0, 0} Int (Set.{0} Int) (Set.instMembershipSet.{0} Int) z s) -> (LE.le.{0} Int Int.instLEInt b z)) (Hinh : Exists.{1} Int (fun (z : Int) => Membership.mem.{0, 0} Int (Set.{0} Int) (Set.instMembershipSet.{0} Int) z s)), Eq.{1} Int (InfSet.infₛ.{0} Int (ConditionallyCompleteLattice.toInfSet.{0} Int (ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice.{0} Int instConditionallyCompleteLinearOrderInt)) s) (Subtype.val.{1} Int (fun (lb : Int) => And (Membership.mem.{0, 0} Int (Set.{0} Int) (Set.instMembershipSet.{0} Int) lb s) (forall (z : Int), (Membership.mem.{0, 0} Int (Set.{0} Int) (Set.instMembershipSet.{0} Int) z s) -> (LE.le.{0} Int Int.instLEInt lb z))) (Int.leastOfBdd (fun (z : Int) => Membership.mem.{0, 0} Int (Set.{0} Int) (Set.instMembershipSet.{0} Int) z s) (fun (a : Int) => _inst_1 a) b Hb Hinh))
Case conversion may be inaccurate. Consider using '#align int.cInf_eq_least_of_bdd Int.cinfₛ_eq_least_of_bddₓ'. -/
theorem cinfₛ_eq_least_of_bdd {s : Set ℤ} [DecidablePred (· ∈ s)] (b : ℤ) (Hb : ∀ z ∈ s, b ≤ z)
    (Hinh : ∃ z : ℤ, z ∈ s) : infₛ s = leastOfBdd b Hb Hinh :=
  by
  convert dif_pos _ using 1
  · convert coe_least_of_bdd_eq _ (Classical.choose_spec (⟨b, Hb⟩ : BddBelow s)) _
  · exact ⟨Hinh, b, Hb⟩
#align int.cInf_eq_least_of_bdd Int.cinfₛ_eq_least_of_bdd

/- warning: int.cInf_empty -> Int.cinfₛ_empty is a dubious translation:
lean 3 declaration is
  Eq.{1} Int (InfSet.infₛ.{0} Int (ConditionallyCompleteLattice.toHasInf.{0} Int (ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice.{0} Int Int.conditionallyCompleteLinearOrder)) (EmptyCollection.emptyCollection.{0} (Set.{0} Int) (Set.hasEmptyc.{0} Int))) (OfNat.ofNat.{0} Int 0 (OfNat.mk.{0} Int 0 (Zero.zero.{0} Int Int.hasZero)))
but is expected to have type
  Eq.{1} Int (InfSet.infₛ.{0} Int (ConditionallyCompleteLattice.toInfSet.{0} Int (ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice.{0} Int instConditionallyCompleteLinearOrderInt)) (EmptyCollection.emptyCollection.{0} (Set.{0} Int) (Set.instEmptyCollectionSet.{0} Int))) (OfNat.ofNat.{0} Int 0 (instOfNatInt 0))
Case conversion may be inaccurate. Consider using '#align int.cInf_empty Int.cinfₛ_emptyₓ'. -/
@[simp]
theorem cinfₛ_empty : infₛ (∅ : Set ℤ) = 0 :=
  dif_neg (by simp)
#align int.cInf_empty Int.cinfₛ_empty

/- warning: int.cInf_of_not_bdd_below -> Int.cinfₛ_of_not_bdd_below is a dubious translation:
lean 3 declaration is
  forall {s : Set.{0} Int}, (Not (BddBelow.{0} Int (PartialOrder.toPreorder.{0} Int (OrderedAddCommGroup.toPartialOrder.{0} Int (StrictOrderedRing.toOrderedAddCommGroup.{0} Int (LinearOrderedRing.toStrictOrderedRing.{0} Int (LinearOrderedCommRing.toLinearOrderedRing.{0} Int Int.linearOrderedCommRing))))) s)) -> (Eq.{1} Int (InfSet.infₛ.{0} Int (ConditionallyCompleteLattice.toHasInf.{0} Int (ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice.{0} Int Int.conditionallyCompleteLinearOrder)) s) (OfNat.ofNat.{0} Int 0 (OfNat.mk.{0} Int 0 (Zero.zero.{0} Int Int.hasZero))))
but is expected to have type
  forall {s : Set.{0} Int}, (Not (BddBelow.{0} Int (PartialOrder.toPreorder.{0} Int (StrictOrderedRing.toPartialOrder.{0} Int (LinearOrderedRing.toStrictOrderedRing.{0} Int (LinearOrderedCommRing.toLinearOrderedRing.{0} Int Int.linearOrderedCommRing)))) s)) -> (Eq.{1} Int (InfSet.infₛ.{0} Int (ConditionallyCompleteLattice.toInfSet.{0} Int (ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice.{0} Int instConditionallyCompleteLinearOrderInt)) s) (OfNat.ofNat.{0} Int 0 (instOfNatInt 0)))
Case conversion may be inaccurate. Consider using '#align int.cInf_of_not_bdd_below Int.cinfₛ_of_not_bdd_belowₓ'. -/
theorem cinfₛ_of_not_bdd_below {s : Set ℤ} (h : ¬BddBelow s) : infₛ s = 0 :=
  dif_neg (by simp [h])
#align int.cInf_of_not_bdd_below Int.cinfₛ_of_not_bdd_below

/- warning: int.cSup_mem -> Int.csupₛ_mem is a dubious translation:
lean 3 declaration is
  forall {s : Set.{0} Int}, (Set.Nonempty.{0} Int s) -> (BddAbove.{0} Int (PartialOrder.toPreorder.{0} Int (OrderedAddCommGroup.toPartialOrder.{0} Int (StrictOrderedRing.toOrderedAddCommGroup.{0} Int (LinearOrderedRing.toStrictOrderedRing.{0} Int (LinearOrderedCommRing.toLinearOrderedRing.{0} Int Int.linearOrderedCommRing))))) s) -> (Membership.Mem.{0, 0} Int (Set.{0} Int) (Set.hasMem.{0} Int) (SupSet.supₛ.{0} Int (ConditionallyCompleteLattice.toHasSup.{0} Int (ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice.{0} Int Int.conditionallyCompleteLinearOrder)) s) s)
but is expected to have type
  forall {s : Set.{0} Int}, (Set.Nonempty.{0} Int s) -> (BddAbove.{0} Int (PartialOrder.toPreorder.{0} Int (StrictOrderedRing.toPartialOrder.{0} Int (LinearOrderedRing.toStrictOrderedRing.{0} Int (LinearOrderedCommRing.toLinearOrderedRing.{0} Int Int.linearOrderedCommRing)))) s) -> (Membership.mem.{0, 0} Int (Set.{0} Int) (Set.instMembershipSet.{0} Int) (SupSet.supₛ.{0} Int (ConditionallyCompleteLattice.toSupSet.{0} Int (ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice.{0} Int instConditionallyCompleteLinearOrderInt)) s) s)
Case conversion may be inaccurate. Consider using '#align int.cSup_mem Int.csupₛ_memₓ'. -/
theorem csupₛ_mem {s : Set ℤ} (h1 : s.Nonempty) (h2 : BddAbove s) : supₛ s ∈ s :=
  by
  convert(greatest_of_bdd _ (Classical.choose_spec h2) h1).2.1
  exact dif_pos ⟨h1, h2⟩
#align int.cSup_mem Int.csupₛ_mem

/- warning: int.cInf_mem -> Int.cinfₛ_mem is a dubious translation:
lean 3 declaration is
  forall {s : Set.{0} Int}, (Set.Nonempty.{0} Int s) -> (BddBelow.{0} Int (PartialOrder.toPreorder.{0} Int (OrderedAddCommGroup.toPartialOrder.{0} Int (StrictOrderedRing.toOrderedAddCommGroup.{0} Int (LinearOrderedRing.toStrictOrderedRing.{0} Int (LinearOrderedCommRing.toLinearOrderedRing.{0} Int Int.linearOrderedCommRing))))) s) -> (Membership.Mem.{0, 0} Int (Set.{0} Int) (Set.hasMem.{0} Int) (InfSet.infₛ.{0} Int (ConditionallyCompleteLattice.toHasInf.{0} Int (ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice.{0} Int Int.conditionallyCompleteLinearOrder)) s) s)
but is expected to have type
  forall {s : Set.{0} Int}, (Set.Nonempty.{0} Int s) -> (BddBelow.{0} Int (PartialOrder.toPreorder.{0} Int (StrictOrderedRing.toPartialOrder.{0} Int (LinearOrderedRing.toStrictOrderedRing.{0} Int (LinearOrderedCommRing.toLinearOrderedRing.{0} Int Int.linearOrderedCommRing)))) s) -> (Membership.mem.{0, 0} Int (Set.{0} Int) (Set.instMembershipSet.{0} Int) (InfSet.infₛ.{0} Int (ConditionallyCompleteLattice.toInfSet.{0} Int (ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice.{0} Int instConditionallyCompleteLinearOrderInt)) s) s)
Case conversion may be inaccurate. Consider using '#align int.cInf_mem Int.cinfₛ_memₓ'. -/
theorem cinfₛ_mem {s : Set ℤ} (h1 : s.Nonempty) (h2 : BddBelow s) : infₛ s ∈ s :=
  by
  convert(least_of_bdd _ (Classical.choose_spec h2) h1).2.1
  exact dif_pos ⟨h1, h2⟩
#align int.cInf_mem Int.cinfₛ_mem

end Int


text:
/-
Copyright (c) 2020 Yury Kudryashov. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yury Kudryashov
-/
import Mathlib.PrePort
import Mathlib.Lean3Lib.init.default
import Mathlib.tactic.ring_exp
import Mathlib.algebra.algebra.basic
import Mathlib.algebra.opposites
import Mathlib.data.equiv.ring
import Mathlib.PostPort

universes u_1 l

namespace Mathlib

/-!
# Quaternions

In this file we define quaternions `ℍ[R]` over a commutative ring `R`, and define some
algebraic structures on `ℍ[R]`.

## Main definitions

* `quaternion_algebra R a b`, `ℍ[R, a, b]` :
  [quaternion algebra](https://en.wikipedia.org/wiki/Quaternion_algebra) with coefficients `a`, `b`
* `quaternion R`, `ℍ[R]` : the space of quaternions, a.k.a. `quaternion_algebra R (-1) (-1)`;
* `quaternion.norm_sq` : square of the norm of a quaternion;
* `quaternion.conj` : conjugate of a quaternion;

We also define the following algebraic structures on `ℍ[R]`:

* `ring ℍ[R, a, b]` and `algebra R ℍ[R, a, b]` : for any commutative ring `R`;
* `ring ℍ[R]` and `algebra R ℍ[R]` : for any commutative ring `R`;
* `domain ℍ[R]` : for a linear ordered commutative ring `R`;
* `division_algebra ℍ[R]` : for a linear ordered field `R`.

## Notation

The following notation is available with `open_locale quaternion`.

* `ℍ[R, c₁, c₂]` : `quaternion_algebra R  c₁ c₂`
* `ℍ[R]` : quaternions over `R`.

## Implementation notes

We define quaternions over any ring `R`, not just `ℝ` to be able to deal with, e.g., integer
or rational quaternions without using real numbers. In particular, all definitions in this file
are computable.

## Tags

quaternion
-/

/-- Quaternion algebra over a type with fixed coefficients $a=i^2$ and $b=j^2$.
Implemented as a structure with four fields: `re`, `im_i`, `im_j`, and `im_k`. -/
structure quaternion_algebra (R : Type u_1) (a : R) (b : R)
where
  re : R
  im_i : R
  im_j : R
  im_k : R

namespace quaternion_algebra

@[simp] theorem mk.eta {R : Type u_1} {c₁ : R} {c₂ : R} (a : quaternion_algebra R c₁ c₂) : mk (re a) (im_i a) (im_j a) (im_k a) = a := sorry

protected instance has_coe_t {R : Type u_1} [comm_ring R] {c₁ : R} {c₂ : R} : has_coe_t R (quaternion_algebra R c₁ c₂) :=
  has_coe_t.mk fun (x : R) => mk x 0 0 0

@[simp] theorem coe_re {R : Type u_1} [comm_ring R] {c₁ : R} {c₂ : R} (x : R) : re ↑x = x :=
  rfl

@[simp] theorem coe_im_i {R : Type u_1} [comm_ring R] {c₁ : R} {c₂ : R} (x : R) : im_i ↑x = 0 :=
  rfl

@[simp] theorem coe_im_j {R : Type u_1} [comm_ring R] {c₁ : R} {c₂ : R} (x : R) : im_j ↑x = 0 :=
  rfl

@[simp] theorem coe_im_k {R : Type u_1} [comm_ring R] {c₁ : R} {c₂ : R} (x : R) : im_k ↑x = 0 :=
  rfl

theorem coe_injective {R : Type u_1} [comm_ring R] {c₁ : R} {c₂ : R} : function.injective coe :=
  fun (x y : R) (h : ↑x = ↑y) => congr_arg re h

@[simp] theorem coe_inj {R : Type u_1} [comm_ring R] {c₁ : R} {c₂ : R} {x : R} {y : R} : ↑x = ↑y ↔ x = y :=
  function.injective.eq_iff coe_injective

@[simp] theorem has_zero_zero_im_j {R : Type u_1} [comm_ring R] {c₁ : R} {c₂ : R} : im_j 0 = 0 :=
  Eq.refl (im_j 0)

@[simp] theorem coe_zero {R : Type u_1} [comm_ring R] {c₁ : R} {c₂ : R} : ↑0 = 0 :=
  rfl

protected instance inhabited {R : Type u_1} [comm_ring R] {c₁ : R} {c₂ : R} : Inhabited (quaternion_algebra R c₁ c₂) :=
  { default := 0 }

@[simp] theorem has_one_one_re {R : Type u_1} [comm_ring R] {c₁ : R} {c₂ : R} : re 1 = 1 :=
  Eq.refl (re 1)

@[simp] theorem coe_one {R : Type u_1} [comm_ring R] {c₁ : R} {c₂ : R} : ↑1 = 1 :=
  rfl

@[simp] theorem has_add_add_im_i {R : Type u_1} [comm_ring R] {c₁ : R} {c₂ : R} (a : quaternion_algebra R c₁ c₂) (b : quaternion_algebra R c₁ c₂) : im_i (a + b) = im_i a + im_i b :=
  Eq.refl (im_i (a + b))

@[simp] theorem mk_add_mk {R : Type u_1} [comm_ring R] {c₁ : R} {c₂ : R} (a₁ : R) (a₂ : R) (a₃ : R) (a₄ : R) (b₁ : R) (b₂ : R) (b₃ : R) (b₄ : R) : mk a₁ a₂ a₃ a₄ + mk b₁ b₂ b₃ b₄ = mk (a₁ + b₁) (a₂ + b₂) (a₃ + b₃) (a₄ + b₄) :=
  rfl

protected instance has_neg {R : Type u_1} [comm_ring R] {c₁ : R} {c₂ : R} : Neg (quaternion_algebra R c₁ c₂) :=
  { neg := fun (a : quaternion_algebra R c₁ c₂) => mk (-re a) (-im_i a) (-im_j a) (-im_k a) }

@[simp] theorem neg_mk {R : Type u_1} [comm_ring R] {c₁ : R} {c₂ : R} (a₁ : R) (a₂ : R) (a₃ : R) (a₄ : R) : -mk a₁ a₂ a₃ a₄ = mk (-a₁) (-a₂) (-a₃) (-a₄) :=
  rfl

@[simp] theorem has_sub_sub_im_k {R : Type u_1} [comm_ring R] {c₁ : R} {c₂ : R} (a : quaternion_algebra R c₁ c₂) (b : quaternion_algebra R c₁ c₂) : im_k (a - b) = im_k a - im_k b :=
  Eq.refl (im_k (a - b))

@[simp] theorem mk_sub_mk {R : Type u_1} [comm_ring R] {c₁ : R} {c₂ : R} (a₁ : R) (a₂ : R) (a₃ : R) (a₄ : R) (b₁ : R) (b₂ : R) (b₃ : R) (b₄ : R) : mk a₁ a₂ a₃ a₄ - mk b₁ b₂ b₃ b₄ = mk (a₁ - b₁) (a₂ - b₂) (a₃ - b₃) (a₄ - b₄) :=
  rfl

/-- Multiplication is given by

* `1 * x = x * 1 = x`;
* `i * i = c₁`;
* `j * j = c₂`;
* `i * j = k`, `j * i = -k`;
* `k * k = -c₁ * c₂`;
* `i * k = c₁ * j`, `k * i = `-c₁ * j`;
* `j * k = -c₂ * i`, `k * j = c₂ * i`.  -/
@[simp] theorem has_mul_mul_im_i {R : Type u_1} [comm_ring R] {c₁ : R} {c₂ : R} (a : quaternion_algebra R c₁ c₂) (b : quaternion_algebra R c₁ c₂) : im_i (a * b) = re a * im_i b + im_i a * re b - c₂ * im_j a * im_k b + c₂ * im_k a * im_j b :=
  Eq.refl (im_i (a * b))

@[simp] theorem mk_mul_mk {R : Type u_1} [comm_ring R] {c₁ : R} {c₂ : R} (a₁ : R) (a₂ : R) (a₃ : R) (a₄ : R) (b₁ : R) (b₂ : R) (b₃ : R) (b₄ : R) : mk a₁ a₂ a₃ a₄ * mk b₁ b₂ b₃ b₄ =
  mk (a₁ * b₁ + c₁ * a₂ * b₂ + c₂ * a₃ * b₃ - c₁ * c₂ * a₄ * b₄) (a₁ * b₂ + a₂ * b₁ - c₂ * a₃ * b₄ + c₂ * a₄ * b₃)
    (a₁ * b₃ + c₁ * a₂ * b₄ + a₃ * b₁ - c₁ * a₄ * b₂) (a₁ * b₄ + a₂ * b₃ - a₃ * b₂ + a₄ * b₁) :=
  rfl

protected instance ring {R : Type u_1} [comm_ring R] {c₁ : R} {c₂ : R} : ring (quaternion_algebra R c₁ c₂) :=
  ring.mk Add.add sorry 0 sorry sorry Neg.neg Sub.sub sorry sorry Mul.mul sorry 1 sorry sorry sorry sorry

protected instance algebra {R : Type u_1} [comm_ring R] {c₁ : R} {c₂ : R} : algebra R (quaternion_algebra R c₁ c₂) :=
  algebra.mk (ring_hom.mk coe sorry sorry sorry sorry) sorry sorry

@[simp] theorem smul_re {R : Type u_1} [comm_ring R] {c₁ : R} {c₂ : R} (r : R) (a : quaternion_algebra R c₁ c₂) : re (r • a) = r • re a :=
  rfl

@[simp] theorem smul_im_i {R : Type u_1} [comm_ring R] {c₁ : R} {c₂ : R} (r : R) (a : quaternion_algebra R c₁ c₂) : im_i (r • a) = r • im_i a :=
  rfl

@[simp] theorem smul_im_j {R : Type u_1} [comm_ring R] {c₁ : R} {c₂ : R} (r : R) (a : quaternion_algebra R c₁ c₂) : im_j (r • a) = r • im_j a :=
  rfl

@[simp] theorem smul_im_k {R : Type u_1} [comm_ring R] {c₁ : R} {c₂ : R} (r : R) (a : quaternion_algebra R c₁ c₂) : im_k (r • a) = r • im_k a :=
  rfl

@[simp] theorem coe_add {R : Type u_1} [comm_ring R] {c₁ : R} {c₂ : R} (x : R) (y : R) : ↑(x + y) = ↑x + ↑y :=
  ring_hom.map_add (algebra_map R (quaternion_algebra R c₁ c₂)) x y

@[simp] theorem coe_sub {R : Type u_1} [comm_ring R] {c₁ : R} {c₂ : R} (x : R) (y : R) : ↑(x - y) = ↑x - ↑y :=
  ring_hom.map_sub (algebra_map R (quaternion_algebra R c₁ c₂)) x y

@[simp] theorem coe_neg {R : Type u_1} [comm_ring R] {c₁ : R} {c₂ : R} (x : R) : ↑(-x) = -↑x :=
  ring_hom.map_neg (algebra_map R (quaternion_algebra R c₁ c₂)) x

@[simp] theorem coe_mul {R : Type u_1} [comm_ring R] {c₁ : R} {c₂ : R} (x : R) (y : R) : ↑(x * y) = ↑x * ↑y :=
  ring_hom.map_mul (algebra_map R (quaternion_algebra R c₁ c₂)) x y

theorem coe_commutes {R : Type u_1} [comm_ring R] {c₁ : R} {c₂ : R} (r : R) (a : quaternion_algebra R c₁ c₂) : ↑r * a = a * ↑r :=
  algebra.commutes r a

theorem coe_commute {R : Type u_1} [comm_ring R] {c₁ : R} {c₂ : R} (r : R) (a : quaternion_algebra R c₁ c₂) : commute (↑r) a :=
  coe_commutes r a

theorem coe_mul_eq_smul {R : Type u_1} [comm_ring R] {c₁ : R} {c₂ : R} (r : R) (a : quaternion_algebra R c₁ c₂) : ↑r * a = r • a :=
  Eq.symm (algebra.smul_def r a)

theorem mul_coe_eq_smul {R : Type u_1} [comm_ring R] {c₁ : R} {c₂ : R} (r : R) (a : quaternion_algebra R c₁ c₂) : a * ↑r = r • a :=
  eq.mpr (id (Eq._oldrec (Eq.refl (a * ↑r = r • a)) (Eq.symm (coe_commutes r a))))
    (eq.mpr (id (Eq._oldrec (Eq.refl (↑r * a = r • a)) (coe_mul_eq_smul r a))) (Eq.refl (r • a)))

@[simp] theorem coe_algebra_map {R : Type u_1} [comm_ring R] {c₁ : R} {c₂ : R} : ⇑(algebra_map R (quaternion_algebra R c₁ c₂)) = coe :=
  rfl

theorem smul_coe {R : Type u_1} [comm_ring R] {c₁ : R} {c₂ : R} (x : R) (y : R) : x • ↑y = ↑(x * y) :=
  eq.mpr (id (Eq._oldrec (Eq.refl (x • ↑y = ↑(x * y))) (coe_mul x y)))
    (eq.mpr (id (Eq._oldrec (Eq.refl (x • ↑y = ↑x * ↑y)) (coe_mul_eq_smul x ↑y))) (Eq.refl (x • ↑y)))

/-- Quaternion conjugate. -/
def conj {R : Type u_1} [comm_ring R] {c₁ : R} {c₂ : R} : linear_equiv R (quaternion_algebra R c₁ c₂) (quaternion_algebra R c₁ c₂) :=
  linear_equiv.of_involutive
    (linear_map.mk (fun (a : quaternion_algebra R c₁ c₂) => mk (re a) (-im_i a) (-im_j a) (-im_k a)) sorry sorry) sorry

@[simp] theorem re_conj {R : Type u_1} [comm_ring R] {c₁ : R} {c₂ : R} (a : quaternion_algebra R c₁ c₂) : re (coe_fn conj a) = re a :=
  rfl

@[simp] theorem im_i_conj {R : Type u_1} [comm_ring R] {c₁ : R} {c₂ : R} (a : quaternion_algebra R c₁ c₂) : im_i (coe_fn conj a) = -im_i a :=
  rfl

@[simp] theorem im_j_conj {R : Type u_1} [comm_ring R] {c₁ : R} {c₂ : R} (a : quaternion_algebra R c₁ c₂) : im_j (coe_fn conj a) = -im_j a :=
  rfl

@[simp] theorem im_k_conj {R : Type u_1} [comm_ring R] {c₁ : R} {c₂ : R} (a : quaternion_algebra R c₁ c₂) : im_k (coe_fn conj a) = -im_k a :=
  rfl

@[simp] theorem conj_conj {R : Type u_1} [comm_ring R] {c₁ : R} {c₂ : R} (a : quaternion_algebra R c₁ c₂) : coe_fn conj (coe_fn conj a) = a :=
  ext (coe_fn conj (coe_fn conj a)) a rfl (neg_neg (im_i a)) (neg_neg (im_j a)) (neg_neg (im_k a))

theorem conj_add {R : Type u_1} [comm_ring R] {c₁ : R} {c₂ : R} (a : quaternion_algebra R c₁ c₂) (b : quaternion_algebra R c₁ c₂) : coe_fn conj (a + b) = coe_fn conj a + coe_fn conj b :=
  linear_equiv.map_add conj a b

@[simp] theorem conj_mul {R : Type u_1} [comm_ring R] {c₁ : R} {c₂ : R} (a : quaternion_algebra R c₁ c₂) (b : quaternion_algebra R c₁ c₂) : coe_fn conj (a * b) = coe_fn conj b * coe_fn conj a := sorry

theorem conj_conj_mul {R : Type u_1} [comm_ring R] {c₁ : R} {c₂ : R} (a : quaternion_algebra R c₁ c₂) (b : quaternion_algebra R c₁ c₂) : coe_fn conj (coe_fn conj a * b) = coe_fn conj b * a :=
  eq.mpr (id (Eq._oldrec (Eq.refl (coe_fn conj (coe_fn conj a * b) = coe_fn conj b * a)) (conj_mul (coe_fn conj a) b)))
    (eq.mpr (id (Eq._oldrec (Eq.refl (coe_fn conj b * coe_fn conj (coe_fn conj a) = coe_fn conj b * a)) (conj_conj a)))
      (Eq.refl (coe_fn conj b * a)))

theorem conj_mul_conj {R : Type u_1} [comm_ring R] {c₁ : R} {c₂ : R} (a : quaternion_algebra R c₁ c₂) (b : quaternion_algebra R c₁ c₂) : coe_fn conj (a * coe_fn conj b) = b * coe_fn conj a :=
  eq.mpr (id (Eq._oldrec (Eq.refl (coe_fn conj (a * coe_fn conj b) = b * coe_fn conj a)) (conj_mul a (coe_fn conj b))))
    (eq.mpr (id (Eq._oldrec (Eq.refl (coe_fn conj (coe_fn conj b) * coe_fn conj a = b * coe_fn conj a)) (conj_conj b)))
      (Eq.refl (b * coe_fn conj a)))

theorem self_add_conj' {R : Type u_1} [comm_ring R] {c₁ : R} {c₂ : R} (a : quaternion_algebra R c₁ c₂) : a + coe_fn conj a = ↑(bit0 1 * re a) := sorry

theorem self_add_conj {R : Type u_1} [comm_ring R] {c₁ : R} {c₂ : R} (a : quaternion_algebra R c₁ c₂) : a + coe_fn conj a = bit0 1 * ↑(re a) := sorry

theorem conj_add_self' {R : Type u_1} [comm_ring R] {c₁ : R} {c₂ : R} (a : quaternion_algebra R c₁ c₂) : coe_fn conj a + a = ↑(bit0 1 * re a) :=
  eq.mpr (id (Eq._oldrec (Eq.refl (coe_fn conj a + a = ↑(bit0 1 * re a))) (add_comm (coe_fn conj a) a)))
    (eq.mpr (id (Eq._oldrec (Eq.refl (a + coe_fn conj a = ↑(bit0 1 * re a))) (self_add_conj' a)))
      (Eq.refl ↑(bit0 1 * re a)))

theorem conj_add_self {R : Type u_1} [comm_ring R] {c₁ : R} {c₂ : R} (a : quaternion_algebra R c₁ c₂) : coe_fn conj a + a = bit0 1 * ↑(re a) :=
  eq.mpr (id (Eq._oldrec (Eq.refl (coe_fn conj a + a = bit0 1 * ↑(re a))) (add_comm (coe_fn conj a) a)))
    (eq.mpr (id (Eq._oldrec (Eq.refl (a + coe_fn conj a = bit0 1 * ↑(re a))) (self_add_conj a)))
      (Eq.refl (bit0 1 * ↑(re a))))

theorem conj_eq_two_re_sub {R : Type u_1} [comm_ring R] {c₁ : R} {c₂ : R} (a : quaternion_algebra R c₁ c₂) : coe_fn conj a = ↑(bit0 1 * re a) - a :=
  iff.mpr eq_sub_iff_add_eq (conj_add_self' a)

theorem commute_conj_self {R : Type u_1} [comm_ring R] {c₁ : R} {c₂ : R} (a : quaternion_algebra R c₁ c₂) : commute (coe_fn conj a) a :=
  eq.mpr (id (Eq._oldrec (Eq.refl (commute (coe_fn conj a) a)) (conj_eq_two_re_sub a)))
    (commute.sub_left (coe_commute (bit0 1 * re a) a) (commute.refl a))

theorem commute_self_conj {R : Type u_1} [comm_ring R] {c₁ : R} {c₂ : R} (a : quaternion_algebra R c₁ c₂) : commute a (coe_fn conj a) :=
  commute.symm (commute_conj_self a)

theorem commute_conj_conj {R : Type u_1} [comm_ring R] {c₁ : R} {c₂ : R} {a : quaternion_algebra R c₁ c₂} {b : quaternion_algebra R c₁ c₂} (h : commute a b) : commute (coe_fn conj a) (coe_fn conj b) := sorry

@[simp] theorem conj_coe {R : Type u_1} [comm_ring R] {c₁ : R} {c₂ : R} (x : R) : coe_fn conj ↑x = ↑x := sorry

theorem conj_smul {R : Type u_1} [comm_ring R] {c₁ : R} {c₂ : R} (r : R) (a : quaternion_algebra R c₁ c₂) : coe_fn conj (r • a) = r • coe_fn conj a :=
  linear_equiv.map_smul conj r a

@[simp] theorem conj_one {R : Type u_1} [comm_ring R] {c₁ : R} {c₂ : R} : coe_fn conj 1 = 1 :=
  conj_coe 1

theorem eq_re_of_eq_coe {R : Type u_1} [comm_ring R] {c₁ : R} {c₂ : R} {a : quaternion_algebra R c₁ c₂} {x : R} (h : a = ↑x) : a = ↑(re a) :=
  eq.mpr (id (Eq._oldrec (Eq.refl (a = ↑(re a))) h))
    (eq.mpr (id (Eq._oldrec (Eq.refl (↑x = ↑(re ↑x))) (coe_re x))) (Eq.refl ↑x))

theorem eq_re_iff_mem_range_coe {R : Type u_1} [comm_ring R] {c₁ : R} {c₂ : R} {a : quaternion_algebra R c₁ c₂} : a = ↑(re a) ↔ a ∈ set.range coe := sorry

@[simp] theorem conj_fixed {R : Type u_1} [comm_ring R] [no_zero_divisors R] [char_zero R] {c₁ : R} {c₂ : R} {a : quaternion_algebra R c₁ c₂} : coe_fn conj a = a ↔ a = ↑(re a) := sorry

-- Can't use `rw ← conj_fixed` in the proof without additional assumptions

theorem conj_mul_eq_coe {R : Type u_1} [comm_ring R] {c₁ : R} {c₂ : R} (a : quaternion_algebra R c₁ c₂) : coe_fn conj a * a = ↑(re (coe_fn conj a * a)) := sorry

theorem mul_conj_eq_coe {R : Type u_1} [comm_ring R] {c₁ : R} {c₂ : R} (a : quaternion_algebra R c₁ c₂) : a * coe_fn conj a = ↑(re (a * coe_fn conj a)) :=
  eq.mpr (id (Eq._oldrec (Eq.refl (a * coe_fn conj a = ↑(re (a * coe_fn conj a)))) (commute.eq (commute_self_conj a))))
    (conj_mul_eq_coe a)

theorem conj_zero {R : Type u_1} [comm_ring R] {c₁ : R} {c₂ : R} : coe_fn conj 0 = 0 :=
  linear_equiv.map_zero conj

theorem conj_neg {R : Type u_1} [comm_ring R] {c₁ : R} {c₂ : R} (a : quaternion_algebra R c₁ c₂) : coe_fn conj (-a) = -coe_fn conj a :=
  linear_equiv.map_neg conj a

theorem conj_sub {R : Type u_1} [comm_ring R] {c₁ : R} {c₂ : R} (a : quaternion_algebra R c₁ c₂) (b : quaternion_algebra R c₁ c₂) : coe_fn conj (a - b) = coe_fn conj a - coe_fn conj b :=
  linear_equiv.map_sub conj a b

protected instance star_ring {R : Type u_1} [comm_ring R] {c₁ : R} {c₂ : R} : star_ring (quaternion_algebra R c₁ c₂) :=
  star_ring.mk conj_add

@[simp] theorem star_def {R : Type u_1} [comm_ring R] {c₁ : R} {c₂ : R} (a : quaternion_algebra R c₁ c₂) : star a = coe_fn conj a :=
  rfl

/-- Quaternion conjugate as an `alg_equiv` to the opposite ring. -/
def conj_alg_equiv {R : Type u_1} [comm_ring R] {c₁ : R} {c₂ : R} : alg_equiv R (quaternion_algebra R c₁ c₂) (quaternion_algebra R c₁ c₂ᵒᵖ) :=
  alg_equiv.mk (opposite.op ∘ ⇑conj) (⇑conj ∘ opposite.unop) sorry sorry sorry sorry sorry

@[simp] theorem coe_conj_alg_equiv {R : Type u_1} [comm_ring R] {c₁ : R} {c₂ : R} : ⇑conj_alg_equiv = opposite.op ∘ ⇑conj :=
  rfl

end quaternion_algebra

/-- Space of quaternions over a type. Implemented as a structure with four fields:
`re`, `im_i`, `im_j`, and `im_k`. -/
def quaternion (R : Type u_1) [HasOne R] [Neg R] :=
  quaternion_algebra R (-1) (-1)

namespace quaternion

protected instance has_coe_t {R : Type u_1} [comm_ring R] : has_coe_t R (quaternion R) :=
  quaternion_algebra.has_coe_t

protected instance ring {R : Type u_1} [comm_ring R] : ring (quaternion R) :=
  quaternion_algebra.ring

protected instance inhabited {R : Type u_1} [comm_ring R] : Inhabited (quaternion R) :=
  quaternion_algebra.inhabited

protected instance algebra {R : Type u_1} [comm_ring R] : algebra R (quaternion R) :=
  quaternion_algebra.algebra

protected instance star_ring {R : Type u_1} [comm_ring R] : star_ring (quaternion R) :=
  quaternion_algebra.star_ring

theorem ext {R : Type u_1} [comm_ring R] (a : quaternion R) (b : quaternion R) : re a = re b → im_i a = im_i b → im_j a = im_j b → im_k a = im_k b → a = b :=
  quaternion_algebra.ext a b

theorem ext_iff {R : Type u_1} [comm_ring R] {a : quaternion R} {b : quaternion R} : a = b ↔ re a = re b ∧ im_i a = im_i b ∧ im_j a = im_j b ∧ im_k a = im_k b :=
  quaternion_algebra.ext_iff a b

@[simp] theorem coe_re {R : Type u_1} [comm_ring R] (x : R) : re ↑x = x :=
  rfl

@[simp] theorem coe_im_i {R : Type u_1} [comm_ring R] (x : R) : im_i ↑x = 0 :=
  rfl

@[simp] theorem coe_im_j {R : Type u_1} [comm_ring R] (x : R) : im_j ↑x = 0 :=
  rfl

@[simp] theorem coe_im_k {R : Type u_1} [comm_ring R] (x : R) : im_k ↑x = 0 :=
  rfl

@[simp] theorem zero_re {R : Type u_1} [comm_ring R] : re 0 = 0 :=
  rfl

@[simp] theorem zero_im_i {R : Type u_1} [comm_ring R] : im_i 0 = 0 :=
  rfl

@[simp] theorem zero_im_j {R : Type u_1} [comm_ring R] : im_j 0 = 0 :=
  rfl

@[simp] theorem zero_im_k {R : Type u_1} [comm_ring R] : im_k 0 = 0 :=
  rfl

@[simp] theorem coe_zero {R : Type u_1} [comm_ring R] : ↑0 = 0 :=
  rfl

@[simp] theorem one_re {R : Type u_1} [comm_ring R] : re 1 = 1 :=
  rfl

@[simp] theorem one_im_i {R : Type u_1} [comm_ring R] : im_i 1 = 0 :=
  rfl

@[simp] theorem one_im_j {R : Type u_1} [comm_ring R] : im_j 1 = 0 :=
  rfl

@[simp] theorem one_im_k {R : Type u_1} [comm_ring R] : im_k 1 = 0 :=
  rfl

@[simp] theorem coe_one {R : Type u_1} [comm_ring R] : ↑1 = 1 :=
  rfl

@[simp] theorem add_re {R : Type u_1} [comm_ring R] (a : quaternion R) (b : quaternion R) : re (a + b) = re a + re b :=
  rfl

@[simp] theorem add_im_i {R : Type u_1} [comm_ring R] (a : quaternion R) (b : quaternion R) : im_i (a + b) = im_i a + im_i b :=
  rfl

@[simp] theorem add_im_j {R : Type u_1} [comm_ring R] (a : quaternion R) (b : quaternion R) : im_j (a + b) = im_j a + im_j b :=
  rfl

@[simp] theorem add_im_k {R : Type u_1} [comm_ring R] (a : quaternion R) (b : quaternion R) : im_k (a + b) = im_k a + im_k b :=
  rfl

@[simp] theorem coe_add {R : Type u_1} [comm_ring R] (x : R) (y : R) : ↑(x + y) = ↑x + ↑y :=
  quaternion_algebra.coe_add x y

@[simp] theorem neg_re {R : Type u_1} [comm_ring R] (a : quaternion R) : re (-a) = -re a :=
  rfl

@[simp] theorem neg_im_i {R : Type u_1} [comm_ring R] (a : quaternion R) : im_i (-a) = -im_i a :=
  rfl

@[simp] theorem neg_im_j {R : Type u_1} [comm_ring R] (a : quaternion R) : im_j (-a) = -im_j a :=
  rfl

@[simp] theorem neg_im_k {R : Type u_1} [comm_ring R] (a : quaternion R) : im_k (-a) = -im_k a :=
  rfl

@[simp] theorem coe_neg {R : Type u_1} [comm_ring R] (x : R) : ↑(-x) = -↑x :=
  quaternion_algebra.coe_neg x

@[simp] theorem sub_re {R : Type u_1} [comm_ring R] (a : quaternion R) (b : quaternion R) : re (a - b) = re a - re b :=
  rfl

@[simp] theorem sub_im_i {R : Type u_1} [comm_ring R] (a : quaternion R) (b : quaternion R) : im_i (a - b) = im_i a - im_i b :=
  rfl

@[simp] theorem sub_im_j {R : Type u_1} [comm_ring R] (a : quaternion R) (b : quaternion R) : im_j (a - b) = im_j a - im_j b :=
  rfl

@[simp] theorem sub_im_k {R : Type u_1} [comm_ring R] (a : quaternion R) (b : quaternion R) : im_k (a - b) = im_k a - im_k b :=
  rfl

@[simp] theorem coe_sub {R : Type u_1} [comm_ring R] (x : R) (y : R) : ↑(x - y) = ↑x - ↑y :=
  quaternion_algebra.coe_sub x y

@[simp] theorem mul_re {R : Type u_1} [comm_ring R] (a : quaternion R) (b : quaternion R) : re (a * b) = re a * re b - im_i a * im_i b - im_j a * im_j b - im_k a * im_k b := sorry

@[simp] theorem mul_im_i {R : Type u_1} [comm_ring R] (a : quaternion R) (b : quaternion R) : im_i (a * b) = re a * im_i b + im_i a * re b + im_j a * im_k b - im_k a * im_j b := sorry

@[simp] theorem mul_im_j {R : Type u_1} [comm_ring R] (a : quaternion R) (b : quaternion R) : im_j (a * b) = re a * im_j b - im_i a * im_k b + im_j a * re b + im_k a * im_i b := sorry

@[simp] theorem mul_im_k {R : Type u_1} [comm_ring R] (a : quaternion R) (b : quaternion R) : im_k (a * b) = re a * im_k b + im_i a * im_j b - im_j a * im_i b + im_k a * re b := sorry

@[simp] theorem coe_mul {R : Type u_1} [comm_ring R] (x : R) (y : R) : ↑(x * y) = ↑x * ↑y :=
  quaternion_algebra.coe_mul x y

theorem coe_injective {R : Type u_1} [comm_ring R] : function.injective coe :=
  quaternion_algebra.coe_injective

@[simp] theorem coe_inj {R : Type u_1} [comm_ring R] {x : R} {y : R} : ↑x = ↑y ↔ x = y :=
  function.injective.eq_iff coe_injective

@[simp] theorem smul_re {R : Type u_1} [comm_ring R] (r : R) (a : quaternion R) : re (r • a) = r • re a :=
  rfl

@[simp] theorem smul_im_i {R : Type u_1} [comm_ring R] (r : R) (a : quaternion R) : im_i (r • a) = r • im_i a :=
  rfl

@[simp] theorem smul_im_j {R : Type u_1} [comm_ring R] (r : R) (a : quaternion R) : im_j (r • a) = r • im_j a :=
  rfl

@[simp] theorem smul_im_k {R : Type u_1} [comm_ring R] (r : R) (a : quaternion R) : im_k (r • a) = r • im_k a :=
  rfl

theorem coe_commutes {R : Type u_1} [comm_ring R] (r : R) (a : quaternion R) : ↑r * a = a * ↑r :=
  quaternion_algebra.coe_commutes r a

theorem coe_commute {R : Type u_1} [comm_ring R] (r : R) (a : quaternion R) : commute (↑r) a :=
  quaternion_algebra.coe_commute r a

theorem coe_mul_eq_smul {R : Type u_1} [comm_ring R] (r : R) (a : quaternion R) : ↑r * a = r • a :=
  quaternion_algebra.coe_mul_eq_smul r a

theorem mul_coe_eq_smul {R : Type u_1} [comm_ring R] (r : R) (a : quaternion R) : a * ↑r = r • a :=
  quaternion_algebra.mul_coe_eq_smul r a

@[simp] theorem algebra_map_def {R : Type u_1} [comm_ring R] : ⇑(algebra_map R (quaternion R)) = coe :=
  rfl

theorem smul_coe {R : Type u_1} [comm_ring R] (x : R) (y : R) : x • ↑y = ↑(x * y) :=
  quaternion_algebra.smul_coe x y

/-- Quaternion conjugate. -/
def conj {R : Type u_1} [comm_ring R] : linear_equiv R (quaternion R) (quaternion R) :=
  quaternion_algebra.conj

@[simp] theorem conj_re {R : Type u_1} [comm_ring R] (a : quaternion R) : re (coe_fn conj a) = re a :=
  rfl

@[simp] theorem conj_im_i {R : Type u_1} [comm_ring R] (a : quaternion R) : im_i (coe_fn conj a) = -im_i a :=
  rfl

@[simp] theorem conj_im_j {R : Type u_1} [comm_ring R] (a : quaternion R) : im_j (coe_fn conj a) = -im_j a :=
  rfl

@[simp] theorem conj_im_k {R : Type u_1} [comm_ring R] (a : quaternion R) : im_k (coe_fn conj a) = -im_k a :=
  rfl

@[simp] theorem conj_conj {R : Type u_1} [comm_ring R] (a : quaternion R) : coe_fn conj (coe_fn conj a) = a :=
  quaternion_algebra.conj_conj a

@[simp] theorem conj_add {R : Type u_1} [comm_ring R] (a : quaternion R) (b : quaternion R) : coe_fn conj (a + b) = coe_fn conj a + coe_fn conj b :=
  quaternion_algebra.conj_add a b

@[simp] theorem conj_mul {R : Type u_1} [comm_ring R] (a : quaternion R) (b : quaternion R) : coe_fn conj (a * b) = coe_fn conj b * coe_fn conj a :=
  quaternion_algebra.conj_mul a b

theorem conj_conj_mul {R : Type u_1} [comm_ring R] (a : quaternion R) (b : quaternion R) : coe_fn conj (coe_fn conj a * b) = coe_fn conj b * a :=
  quaternion_algebra.conj_conj_mul a b

theorem conj_mul_conj {R : Type u_1} [comm_ring R] (a : quaternion R) (b : quaternion R) : coe_fn conj (a * coe_fn conj b) = b * coe_fn conj a :=
  quaternion_algebra.conj_mul_conj a b

theorem self_add_conj' {R : Type u_1} [comm_ring R] (a : quaternion R) : a + coe_fn conj a = ↑(bit0 1 * re a) :=
  quaternion_algebra.self_add_conj' a

theorem self_add_conj {R : Type u_1} [comm_ring R] (a : quaternion R) : a + coe_fn conj a = bit0 1 * ↑(re a) :=
  quaternion_algebra.self_add_conj a

theorem conj_add_self' {R : Type u_1} [comm_ring R] (a : quaternion R) : coe_fn conj a + a = ↑(bit0 1 * re a) :=
  quaternion_algebra.conj_add_self' a

theorem conj_add_self {R : Type u_1} [comm_ring R] (a : quaternion R) : coe_fn conj a + a = bit0 1 * ↑(re a) :=
  quaternion_algebra.conj_add_self a

theorem conj_eq_two_re_sub {R : Type u_1} [comm_ring R] (a : quaternion R) : coe_fn conj a = ↑(bit0 1 * re a) - a :=
  quaternion_algebra.conj_eq_two_re_sub a

theorem commute_conj_self {R : Type u_1} [comm_ring R] (a : quaternion R) : commute (coe_fn conj a) a :=
  quaternion_algebra.commute_conj_self a

theorem commute_self_conj {R : Type u_1} [comm_ring R] (a : quaternion R) : commute a (coe_fn conj a) :=
  quaternion_algebra.commute_self_conj a

theorem commute_conj_conj {R : Type u_1} [comm_ring R] {a : quaternion R} {b : quaternion R} (h : commute a b) : commute (coe_fn conj a) (coe_fn conj b) :=
  quaternion_algebra.commute_conj_conj h

theorem Mathlib.commute.quaternion_conj {R : Type u_1} [comm_ring R] {a : quaternion R} {b : quaternion R} (h : commute a b) : commute (coe_fn conj a) (coe_fn conj b) :=
  commute_conj_conj

@[simp] theorem conj_coe {R : Type u_1} [comm_ring R] (x : R) : coe_fn conj ↑x = ↑x :=
  quaternion_algebra.conj_coe x

@[simp] theorem conj_smul {R : Type u_1} [comm_ring R] (r : R) (a : quaternion R) : coe_fn conj (r • a) = r • coe_fn conj a :=
  quaternion_algebra.conj_smul r a

@[simp] theorem conj_one {R : Type u_1} [comm_ring R] : coe_fn conj 1 = 1 :=
  conj_coe 1

theorem eq_re_of_eq_coe {R : Type u_1} [comm_ring R] {a : quaternion R} {x : R} (h : a = ↑x) : a = ↑(re a) :=
  quaternion_algebra.eq_re_of_eq_coe h

theorem eq_re_iff_mem_range_coe {R : Type u_1} [comm_ring R] {a : quaternion R} : a = ↑(re a) ↔ a ∈ set.range coe :=
  quaternion_algebra.eq_re_iff_mem_range_coe

@[simp] theorem conj_fixed {R : Type u_1} [comm_ring R] [no_zero_divisors R] [char_zero R] {a : quaternion R} : coe_fn conj a = a ↔ a = ↑(re a) :=
  quaternion_algebra.conj_fixed

theorem conj_mul_eq_coe {R : Type u_1} [comm_ring R] (a : quaternion R) : coe_fn conj a * a = ↑(re (coe_fn conj a * a)) :=
  quaternion_algebra.conj_mul_eq_coe a

theorem mul_conj_eq_coe {R : Type u_1} [comm_ring R] (a : quaternion R) : a * coe_fn conj a = ↑(re (a * coe_fn conj a)) :=
  quaternion_algebra.mul_conj_eq_coe a

@[simp] theorem conj_zero {R : Type u_1} [comm_ring R] : coe_fn conj 0 = 0 :=
  quaternion_algebra.conj_zero

@[simp] theorem conj_neg {R : Type u_1} [comm_ring R] (a : quaternion R) : coe_fn conj (-a) = -coe_fn conj a :=
  quaternion_algebra.conj_neg a

@[simp] theorem conj_sub {R : Type u_1} [comm_ring R] (a : quaternion R) (b : quaternion R) : coe_fn conj (a - b) = coe_fn conj a - coe_fn conj b :=
  quaternion_algebra.conj_sub a b

/-- Quaternion conjugate as an `alg_equiv` to the opposite ring. -/
def conj_alg_equiv {R : Type u_1} [comm_ring R] : alg_equiv R (quaternion R) (quaternion Rᵒᵖ) :=
  quaternion_algebra.conj_alg_equiv

@[simp] theorem coe_conj_alg_equiv {R : Type u_1} [comm_ring R] : ⇑conj_alg_equiv = opposite.op ∘ ⇑conj :=
  rfl

/-- Square of the norm. -/
def norm_sq {R : Type u_1} [comm_ring R] : monoid_with_zero_hom (quaternion R) R :=
  monoid_with_zero_hom.mk (fun (a : quaternion R) => re (a * coe_fn conj a)) sorry sorry sorry

theorem norm_sq_def {R : Type u_1} [comm_ring R] (a : quaternion R) : coe_fn norm_sq a = re (a * coe_fn conj a) :=
  rfl

theorem norm_sq_def' {R : Type u_1} [comm_ring R] (a : quaternion R) : coe_fn norm_sq a = re a ^ bit0 1 + im_i a ^ bit0 1 + im_j a ^ bit0 1 + im_k a ^ bit0 1 := sorry

theorem norm_sq_coe {R : Type u_1} [comm_ring R] (x : R) : coe_fn norm_sq ↑x = x ^ bit0 1 := sorry

@[simp] theorem norm_sq_neg {R : Type u_1} [comm_ring R] (a : quaternion R) : coe_fn norm_sq (-a) = coe_fn norm_sq a := sorry

theorem self_mul_conj {R : Type u_1} [comm_ring R] (a : quaternion R) : a * coe_fn conj a = ↑(coe_fn norm_sq a) :=
  eq.mpr (id (Eq._oldrec (Eq.refl (a * coe_fn conj a = ↑(coe_fn norm_sq a))) (mul_conj_eq_coe a)))
    (eq.mpr (id (Eq._oldrec (Eq.refl (↑(re (a * coe_fn conj a)) = ↑(coe_fn norm_sq a))) (norm_sq_def a)))
      (Eq.refl ↑(re (a * coe_fn conj a))))

theorem conj_mul_self {R : Type u_1} [comm_ring R] (a : quaternion R) : coe_fn conj a * a = ↑(coe_fn norm_sq a) := sorry

theorem coe_norm_sq_add {R : Type u_1} [comm_ring R] (a : quaternion R) (b : quaternion R) : ↑(coe_fn norm_sq (a + b)) = ↑(coe_fn norm_sq a) + a * coe_fn conj b + b * coe_fn conj a + ↑(coe_fn norm_sq b) := sorry

end quaternion

namespace quaternion

@[simp] theorem norm_sq_eq_zero {R : Type u_1} [linear_ordered_comm_ring R] {a : quaternion R} : coe_fn norm_sq a = 0 ↔ a = 0 := sorry

theorem norm_sq_ne_zero {R : Type u_1} [linear_ordered_comm_ring R] {a : quaternion R} : coe_fn norm_sq a ≠ 0 ↔ a ≠ 0 :=
  not_congr norm_sq_eq_zero

@[simp] theorem norm_sq_nonneg {R : Type u_1} [linear_ordered_comm_ring R] {a : quaternion R} : 0 ≤ coe_fn norm_sq a :=
  eq.mpr (id (Eq._oldrec (Eq.refl (0 ≤ coe_fn norm_sq a)) (norm_sq_def' a)))
    (add_nonneg (add_nonneg (add_nonneg (pow_two_nonneg (re a)) (pow_two_nonneg (im_i a))) (pow_two_nonneg (im_j a)))
      (pow_two_nonneg (im_k a)))

@[simp] theorem norm_sq_le_zero {R : Type u_1} [linear_ordered_comm_ring R] {a : quaternion R} : coe_fn norm_sq a ≤ 0 ↔ a = 0 := sorry

protected instance domain {R : Type u_1} [linear_ordered_comm_ring R] : domain (quaternion R) :=
  domain.mk ring.add sorry ring.zero sorry sorry ring.neg ring.sub sorry sorry ring.mul sorry ring.one sorry sorry sorry
    sorry sorry sorry

theorem has_inv_inv {R : Type u_1} [linear_ordered_field R] (a : quaternion R) : a⁻¹ = coe_fn norm_sq a⁻¹ • coe_fn conj a :=
  Eq.refl (a⁻¹)

protected instance division_ring {R : Type u_1} [linear_ordered_field R] : division_ring (quaternion R) :=
  division_ring.mk domain.add sorry domain.zero sorry sorry domain.neg domain.sub sorry sorry domain.mul sorry domain.one
    sorry sorry sorry sorry has_inv.inv (div_inv_monoid.div._default domain.mul sorry domain.one sorry sorry has_inv.inv)
    sorry sorry sorry

@[simp] theorem norm_sq_inv {R : Type u_1} [linear_ordered_field R] (a : quaternion R) : coe_fn norm_sq (a⁻¹) = (coe_fn norm_sq a⁻¹) :=
  monoid_with_zero_hom.map_inv' norm_sq a

@[simp] theorem norm_sq_div {R : Type u_1} [linear_ordered_field R] (a : quaternion R) (b : quaternion R) : coe_fn norm_sq (a / b) = coe_fn norm_sq a / coe_fn norm_sq b :=
  monoid_with_zero_hom.map_div norm_sq a b

author: AurelienSaue


text:
/-
Copyright (c) 2019 Oliver Nash. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Oliver Nash

! This file was ported from Lean 3 source module algebra.lie.basic
! leanprover-community/mathlib commit dc6c365e751e34d100e80fe6e314c3c3e0fd2988
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.Module.Equiv
import Mathlib.Data.Bracket
import Mathlib.LinearAlgebra.Basic

/-!
# Lie algebras

This file defines Lie rings and Lie algebras over a commutative ring together with their
modules, morphisms and equivalences, as well as various lemmas to make these definitions usable.

## Main definitions

  * `LieRing`
  * `LieAlgebra`
  * `LieRingModule`
  * `LieModule`
  * `LieHom`
  * `LieEquiv`
  * `LieModuleHom`
  * `LieModuleEquiv`

## Notation

Working over a fixed commutative ring `R`, we introduce the notations:
 * `L →ₗ⁅R⁆ L'` for a morphism of Lie algebras,
 * `L ≃ₗ⁅R⁆ L'` for an equivalence of Lie algebras,
 * `M →ₗ⁅R,L⁆ N` for a morphism of Lie algebra modules `M`, `N` over a Lie algebra `L`,
 * `M ≃ₗ⁅R,L⁆ N` for an equivalence of Lie algebra modules `M`, `N` over a Lie algebra `L`.

## Implementation notes

Lie algebras are defined as modules with a compatible Lie ring structure and thus, like modules,
are partially unbundled.

## References
* [N. Bourbaki, *Lie Groups and Lie Algebras, Chapters 1--3*](bourbaki1975)

## Tagsc

lie bracket, jacobi identity, lie ring, lie algebra, lie module
-/

universe u v w w₁ w₂

open Function

/-- A Lie ring is an additive group with compatible product, known as the bracket, satisfying the
Jacobi identity. -/
/- @[protect_proj] -- Porting note: not (yet) implemented. -/
class LieRing (L : Type v) extends AddCommGroup L, Bracket L L where
  /-- A Lie ring bracket is additive in its first component. -/
  add_lie : ∀ x y z : L, ⁅x + y, z⁆ = ⁅x, z⁆ + ⁅y, z⁆
  /-- A Lie ring bracket is additive in its second component. -/
  lie_add : ∀ x y z : L, ⁅x, y + z⁆ = ⁅x, y⁆ + ⁅x, z⁆
  /-- A Lie ring bracket vanishes on the diagonal in L × L. -/
  lie_self : ∀ x : L, ⁅x, x⁆ = 0
  /-- A Lie ring bracket satisfies a Leibniz / Jacobi identity. -/
  leibniz_lie : ∀ x y z : L, ⁅x, ⁅y, z⁆⁆ = ⁅⁅x, y⁆, z⁆ + ⁅y, ⁅x, z⁆⁆
#align lie_ring LieRing

/-- A Lie algebra is a module with compatible product, known as the bracket, satisfying the Jacobi
identity. Forgetting the scalar multiplication, every Lie algebra is a Lie ring. -/
/- @[protect_proj] -- Porting note: not (yet) implemented. -/
class LieAlgebra (R : Type u) (L : Type v) [CommRing R] [LieRing L] extends Module R L where
  /-- A Lie algebra bracket is compatible with scalar multiplication in its second argument.

  The compatibility in the first argument is not a class property, but follows since every
  Lie algebra has a natural Lie module action on itself, see `LieModule`. -/
  lie_smul : ∀ (t : R) (x y : L), ⁅x, t • y⁆ = t • ⁅x, y⁆
#align lie_algebra LieAlgebra

/-- A Lie ring module is an additive group, together with an additive action of a
Lie ring on this group, such that the Lie bracket acts as the commutator of endomorphisms.
(For representations of Lie *algebras* see `lie_module`.) -/
/- @[protect_proj] -- Porting note: not (yet) implemented. -/
class LieRingModule (L : Type v) (M : Type w) [LieRing L] [AddCommGroup M] extends Bracket L M where
  /-- A Lie ring module bracket is additive in its first component. -/
  add_lie : ∀ (x y : L) (m : M), ⁅x + y, m⁆ = ⁅x, m⁆ + ⁅y, m⁆
  /-- A Lie ring module bracket is additive in its second component. -/
  lie_add : ∀ (x : L) (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆
  /-- A Lie ring module bracket satisfies a Leibniz / Jacobi identity. -/
  leibniz_lie : ∀ (x y : L) (m : M), ⁅x, ⁅y, m⁆⁆ = ⁅⁅x, y⁆, m⁆ + ⁅y, ⁅x, m⁆⁆
#align lie_ring_module LieRingModule

/-- A Lie module is a module over a commutative ring, together with a linear action of a Lie
algebra on this module, such that the Lie bracket acts as the commutator of endomorphisms. -/
/- @[protect_proj] -- Porting note: not (yet) implemented. -/
class LieModule (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L]
  [AddCommGroup M] [Module R M] [LieRingModule L M] where
  /-- A Lie module bracket is compatible with scalar multiplication in its first argument. -/
  smul_lie : ∀ (t : R) (x : L) (m : M), ⁅t • x, m⁆ = t • ⁅x, m⁆
  /-- A Lie module bracket is compatible with scalar multiplication in its second argument. -/
  lie_smul : ∀ (t : R) (x : L) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆
#align lie_module LieModule

section BasicProperties

variable {R : Type u} {L : Type v} {M : Type w} {N : Type w₁}

variable [CommRing R] [LieRing L] [LieAlgebra R L]

variable [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M]

variable [AddCommGroup N] [Module R N] [LieRingModule L N] [LieModule R L N]

variable (t : R) (x y z : L) (m n : M)

@[simp]
theorem add_lie : ⁅x + y, m⁆ = ⁅x, m⁆ + ⁅y, m⁆ :=
  LieRingModule.add_lie x y m
#align add_lie add_lie

@[simp]
theorem lie_add : ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆ :=
  LieRingModule.lie_add x m n
#align lie_add lie_add

@[simp]
theorem smul_lie : ⁅t • x, m⁆ = t • ⁅x, m⁆ :=
  LieModule.smul_lie t x m
#align smul_lie smul_lie

@[simp]
theorem lie_smul : ⁅x, t • m⁆ = t • ⁅x, m⁆ :=
  LieModule.lie_smul t x m
#align lie_smul lie_smul

theorem leibniz_lie : ⁅x, ⁅y, m⁆⁆ = ⁅⁅x, y⁆, m⁆ + ⁅y, ⁅x, m⁆⁆ :=
  LieRingModule.leibniz_lie x y m
#align leibniz_lie leibniz_lie

@[simp]
theorem lie_zero : ⁅x, 0⁆ = (0 : M) :=
  (AddMonoidHom.mk' _ (lie_add x)).map_zero
#align lie_zero lie_zero

@[simp]
theorem zero_lie : ⁅(0 : L), m⁆ = 0 :=
  (AddMonoidHom.mk' (fun x : L => ⁅x, m⁆) fun x y => add_lie x y m).map_zero
#align zero_lie zero_lie

@[simp]
theorem lie_self : ⁅x, x⁆ = 0 :=
  LieRing.lie_self x
#align lie_self lie_self

instance lieRingSelfModule : LieRingModule L L :=
  { (inferInstance : LieRing L) with }
#align lie_ring_self_module lieRingSelfModule

@[simp]
theorem lie_skew : -⁅y, x⁆ = ⁅x, y⁆ := by
  have h : ⁅x + y, x⁆ + ⁅x + y, y⁆ = 0 := by rw [← lie_add]; apply lie_self
  simpa [neg_eq_iff_add_eq_zero] using h
#align lie_skew lie_skew

/-- Every Lie algebra is a module over itself. -/
instance lieAlgebraSelfModule : LieModule R L L
    where
  smul_lie t x m := by rw [← lie_skew, ← lie_skew x m, LieAlgebra.lie_smul, smul_neg]
  lie_smul := by apply LieAlgebra.lie_smul
#align lie_algebra_self_module lieAlgebraSelfModule

@[simp]
theorem neg_lie : ⁅-x, m⁆ = -⁅x, m⁆ := by
  rw [← sub_eq_zero, sub_neg_eq_add, ← add_lie]
  simp
#align neg_lie neg_lie

@[simp]
theorem lie_neg : ⁅x, -m⁆ = -⁅x, m⁆ := by
  rw [← sub_eq_zero, sub_neg_eq_add, ← lie_add]
  simp
#align lie_neg lie_neg

@[simp]
theorem sub_lie : ⁅x - y, m⁆ = ⁅x, m⁆ - ⁅y, m⁆ := by simp [sub_eq_add_neg]
#align sub_lie sub_lie

@[simp]
theorem lie_sub : ⁅x, m - n⁆ = ⁅x, m⁆ - ⁅x, n⁆ := by simp [sub_eq_add_neg]
#align lie_sub lie_sub

@[simp]
theorem nsmul_lie (n : ℕ) : ⁅n • x, m⁆ = n • ⁅x, m⁆ :=
  AddMonoidHom.map_nsmul ⟨⟨fun x : L => ⁅x, m⁆, zero_lie m⟩, fun _ _ => add_lie _ _ _⟩ _ _
#align nsmul_lie nsmul_lie

@[simp]
theorem lie_nsmul (n : ℕ) : ⁅x, n • m⁆ = n • ⁅x, m⁆ :=
  AddMonoidHom.map_nsmul ⟨⟨fun m : M => ⁅x, m⁆, lie_zero x⟩, fun _ _ => lie_add _ _ _⟩ _ _
#align lie_nsmul lie_nsmul

@[simp]
theorem zsmul_lie (a : ℤ) : ⁅a • x, m⁆ = a • ⁅x, m⁆ :=
  AddMonoidHom.map_zsmul ⟨⟨fun x : L => ⁅x, m⁆, zero_lie m⟩, fun _ _ => add_lie _ _ _⟩ _ _
#align zsmul_lie zsmul_lie

@[simp]
theorem lie_zsmul (a : ℤ) : ⁅x, a • m⁆ = a • ⁅x, m⁆ :=
  AddMonoidHom.map_zsmul ⟨⟨fun m : M => ⁅x, m⁆, lie_zero x⟩, fun _ _ => lie_add _ _ _⟩ _ _
#align lie_zsmul lie_zsmul

@[simp]
theorem lie_lie : ⁅⁅x, y⁆, m⁆ = ⁅x, ⁅y, m⁆⁆ - ⁅y, ⁅x, m⁆⁆ := by rw [leibniz_lie, add_sub_cancel]
#align lie_lie lie_lie

theorem lie_jacobi : ⁅x, ⁅y, z⁆⁆ + ⁅y, ⁅z, x⁆⁆ + ⁅z, ⁅x, y⁆⁆ = 0 := by
  rw [← neg_neg ⁅x, y⁆, lie_neg z, lie_skew y x, ← lie_skew, lie_lie]
  abel
#align lie_jacobi lie_jacobi

instance LieRing.intLieAlgebra : LieAlgebra ℤ L where lie_smul n x y := lie_zsmul x y n
#align lie_ring.int_lie_algebra LieRing.intLieAlgebra

-- Porting note: TODO Erase this line. Needed because we don't have η for classes. (lean4#2074)
attribute [-instance] Ring.toNonAssocRing

instance : LieRingModule L (M →ₗ[R] N) where
  bracket x f :=
    { toFun := fun m => ⁅x, f m⁆ - f ⁅x, m⁆
      map_add' := fun m n => by
        simp only [lie_add, LinearMap.map_add]
        abel
      map_smul' := fun t m => by
        simp only [smul_sub, LinearMap.map_smul, lie_smul, RingHom.id_apply] }
  add_lie x y f := by
    ext n
    simp only [add_lie, LinearMap.coe_mk, AddHom.coe_mk, LinearMap.add_apply, LinearMap.map_add]
    abel
  lie_add x f g := by
    ext n
    simp only [LinearMap.coe_mk, AddHom.coe_mk, lie_add, LinearMap.add_apply]
    abel
  leibniz_lie x y f := by
    ext n
    simp only [lie_lie, LinearMap.coe_mk, AddHom.coe_mk, LinearMap.map_sub, LinearMap.add_apply,
      lie_sub]
    abel

@[simp]
theorem LieHom.lie_apply (f : M →ₗ[R] N) (x : L) (m : M) : ⁅x, f⁆ m = ⁅x, f m⁆ - f ⁅x, m⁆ :=
  rfl
#align lie_hom.lie_apply LieHom.lie_apply

instance : LieModule R L (M →ₗ[R] N)
    where
  smul_lie t x f := by
    ext n
    simp only [smul_sub, smul_lie, LinearMap.smul_apply, LieHom.lie_apply, LinearMap.map_smul]
  lie_smul t x f := by
    ext n
    simp only [smul_sub, LinearMap.smul_apply, LieHom.lie_apply, lie_smul]

end BasicProperties

-- Porting note: TODO Erase this line. Needed because we don't have η for classes. (lean4#2074)
attribute [-instance] Ring.toNonAssocRing

/-- A morphism of Lie algebras is a linear map respecting the bracket operations. -/
structure LieHom (R L L': Type _) [CommRing R] [LieRing L] [LieAlgebra R L]
  [LieRing L'] [LieAlgebra R L'] extends L →ₗ[R] L' where
  /-- A morphism of Lie algebras is compatible with brackets. -/
  map_lie' : ∀ {x y : L}, toFun ⁅x, y⁆ = ⁅toFun x, toFun y⁆
#align lie_hom LieHom

@[inherit_doc]
notation:25 L " →ₗ⁅" R:25 "⁆ " L':0 => LieHom R L L'

namespace LieHom

variable {R : Type u} {L₁ : Type v} {L₂ : Type w} {L₃ : Type w₁}

variable [CommRing R]

variable [LieRing L₁] [LieAlgebra R L₁]

variable [LieRing L₂] [LieAlgebra R L₂]

variable [LieRing L₃] [LieAlgebra R L₃]

attribute [coe] LieHom.toLinearMap

instance : Coe (L₁ →ₗ⁅R⁆ L₂) (L₁ →ₗ[R] L₂) :=
  ⟨LieHom.toLinearMap⟩

instance : FunLike (L₁ →ₗ⁅R⁆ L₂) L₁ (fun _ => L₂) :=
  { coe := fun f => f.toFun,
    coe_injective' := fun x y h =>
      by cases x; cases y; simp at h; simp [h]  }

initialize_simps_projections LieHom (toFun → apply)

@[simp, norm_cast]
theorem coe_toLinearMap (f : L₁ →ₗ⁅R⁆ L₂) : ⇑(f : L₁ →ₗ[R] L₂) = f :=
  rfl
#align lie_hom.coe_to_linear_map LieHom.coe_toLinearMap

@[simp]
theorem toFun_eq_coe (f : L₁ →ₗ⁅R⁆ L₂) : f.toFun = ⇑f :=
  rfl
#align lie_hom.to_fun_eq_coe LieHom.toFun_eq_coe

@[simp]
theorem map_smul (f : L₁ →ₗ⁅R⁆ L₂) (c : R) (x : L₁) : f (c • x) = c • f x :=
  LinearMap.map_smul (f : L₁ →ₗ[R] L₂) c x
#align lie_hom.map_smul LieHom.map_smul

@[simp]
theorem map_add (f : L₁ →ₗ⁅R⁆ L₂) (x y : L₁) : f (x + y) = f x + f y :=
  LinearMap.map_add (f : L₁ →ₗ[R] L₂) x y
#align lie_hom.map_add LieHom.map_add

@[simp]
theorem map_sub (f : L₁ →ₗ⁅R⁆ L₂) (x y : L₁) : f (x - y) = f x - f y :=
  LinearMap.map_sub (f : L₁ →ₗ[R] L₂) x y
#align lie_hom.map_sub LieHom.map_sub

@[simp]
theorem map_neg (f : L₁ →ₗ⁅R⁆ L₂) (x : L₁) : f (-x) = -f x :=
  LinearMap.map_neg (f : L₁ →ₗ[R] L₂) x
#align lie_hom.map_neg LieHom.map_neg

@[simp]
theorem map_lie (f : L₁ →ₗ⁅R⁆ L₂) (x y : L₁) : f ⁅x, y⁆ = ⁅f x, f y⁆ :=
  LieHom.map_lie' f
#align lie_hom.map_lie LieHom.map_lie

@[simp]
theorem map_zero (f : L₁ →ₗ⁅R⁆ L₂) : f 0 = 0 :=
  (f : L₁ →ₗ[R] L₂).map_zero
#align lie_hom.map_zero LieHom.map_zero

/-- The identity map is a morphism of Lie algebras. -/
def id : L₁ →ₗ⁅R⁆ L₁ :=
  { (LinearMap.id : L₁ →ₗ[R] L₁) with map_lie' := rfl }
#align lie_hom.id LieHom.id

@[simp]
theorem coe_id : ⇑(id : L₁ →ₗ⁅R⁆ L₁) = _root_.id :=
  rfl
#align lie_hom.coe_id LieHom.coe_id

theorem id_apply (x : L₁) : (id : L₁ →ₗ⁅R⁆ L₁) x = x :=
  rfl
#align lie_hom.id_apply LieHom.id_apply

/-- The constant 0 map is a Lie algebra morphism. -/
instance : Zero (L₁ →ₗ⁅R⁆ L₂) :=
  ⟨{ (0 : L₁ →ₗ[R] L₂) with map_lie' := by simp }⟩

@[norm_cast, simp]
theorem coe_zero : ((0 : L₁ →ₗ⁅R⁆ L₂) : L₁ → L₂) = 0 :=
  rfl
#align lie_hom.coe_zero LieHom.coe_zero

theorem zero_apply (x : L₁) : (0 : L₁ →ₗ⁅R⁆ L₂) x = 0 :=
  rfl
#align lie_hom.zero_apply LieHom.zero_apply

/-- The identity map is a Lie algebra morphism. -/
instance : One (L₁ →ₗ⁅R⁆ L₁) :=
  ⟨id⟩

@[simp]
theorem coe_one : ((1 : L₁ →ₗ⁅R⁆ L₁) : L₁ → L₁) = _root_.id :=
  rfl
#align lie_hom.coe_one LieHom.coe_one

theorem one_apply (x : L₁) : (1 : L₁ →ₗ⁅R⁆ L₁) x = x :=
  rfl
#align lie_hom.one_apply LieHom.one_apply

instance : Inhabited (L₁ →ₗ⁅R⁆ L₂) :=
  ⟨0⟩

theorem coe_injective : @Function.Injective (L₁ →ₗ⁅R⁆ L₂) (L₁ → L₂) (↑) := by
  rintro ⟨⟨⟨f, _⟩, _⟩, _⟩ ⟨⟨⟨g, _⟩, _⟩, _⟩ h
  congr
#align lie_hom.coe_injective LieHom.coe_injective

@[ext]
theorem ext {f g : L₁ →ₗ⁅R⁆ L₂} (h : ∀ x, f x = g x) : f = g :=
  coe_injective <| funext h
#align lie_hom.ext LieHom.ext

theorem ext_iff {f g : L₁ →ₗ⁅R⁆ L₂} : f = g ↔ ∀ x, f x = g x :=
  ⟨by
    rintro rfl x
    rfl, ext⟩
#align lie_hom.ext_iff LieHom.ext_iff

theorem congr_fun {f g : L₁ →ₗ⁅R⁆ L₂} (h : f = g) (x : L₁) : f x = g x :=
  h ▸ rfl
#align lie_hom.congr_fun LieHom.congr_fun

@[simp]
theorem mk_coe (f : L₁ →ₗ⁅R⁆ L₂) (h₁ h₂ h₃) : (⟨⟨⟨f, h₁⟩, h₂⟩, h₃⟩ : L₁ →ₗ⁅R⁆ L₂) = f := by
  ext
  rfl
#align lie_hom.mk_coe LieHom.mk_coe

@[simp]
theorem coe_mk (f : L₁ → L₂) (h₁ h₂ h₃) : ((⟨⟨⟨f, h₁⟩, h₂⟩, h₃⟩ : L₁ →ₗ⁅R⁆ L₂) : L₁ → L₂) = f :=
  rfl
#align lie_hom.coe_mk LieHom.coe_mk

/-- The composition of morphisms is a morphism. -/
def comp (f : L₂ →ₗ⁅R⁆ L₃) (g : L₁ →ₗ⁅R⁆ L₂) : L₁ →ₗ⁅R⁆ L₃ :=
  { LinearMap.comp f.toLinearMap g.toLinearMap with
    map_lie' := by
      intros x y
      change f (g ⁅x, y⁆) = ⁅f (g x), f (g y)⁆
      rw [map_lie, map_lie] }
#align lie_hom.comp LieHom.comp

theorem comp_apply (f : L₂ →ₗ⁅R⁆ L₃) (g : L₁ →ₗ⁅R⁆ L₂) (x : L₁) : f.comp g x = f (g x) :=
  rfl
#align lie_hom.comp_apply LieHom.comp_apply

@[norm_cast, simp]
theorem coe_comp (f : L₂ →ₗ⁅R⁆ L₃) (g : L₁ →ₗ⁅R⁆ L₂) : (f.comp g : L₁ → L₃) = f ∘ g :=
  rfl
#align lie_hom.coe_comp LieHom.coe_comp

@[norm_cast, simp]
theorem coe_linearMap_comp (f : L₂ →ₗ⁅R⁆ L₃) (g : L₁ →ₗ⁅R⁆ L₂) :
    (f.comp g : L₁ →ₗ[R] L₃) = (f : L₂ →ₗ[R] L₃).comp (g : L₁ →ₗ[R] L₂) :=
  rfl
#align lie_hom.coe_linear_map_comp LieHom.coe_linearMap_comp

@[simp]
theorem comp_id (f : L₁ →ₗ⁅R⁆ L₂) : f.comp (id : L₁ →ₗ⁅R⁆ L₁) = f := by
  ext
  rfl
#align lie_hom.comp_id LieHom.comp_id

@[simp]
theorem id_comp (f : L₁ →ₗ⁅R⁆ L₂) : (id : L₂ →ₗ⁅R⁆ L₂).comp f = f := by
  ext
  rfl
#align lie_hom.id_comp LieHom.id_comp

/-- The inverse of a bijective morphism is a morphism. -/
def inverse (f : L₁ →ₗ⁅R⁆ L₂) (g : L₂ → L₁) (h₁ : Function.LeftInverse g f)
    (h₂ : Function.RightInverse g f) : L₂ →ₗ⁅R⁆ L₁ :=
  { LinearMap.inverse f.toLinearMap g h₁ h₂ with
    map_lie' := by
      intros x y
      calc
        g ⁅x, y⁆ = g ⁅f (g x), f (g y)⁆ := by conv_lhs => rw [← h₂ x, ← h₂ y]
        _ = g (f ⁅g x, g y⁆) := by rw [map_lie]
        _ = ⁅g x, g y⁆ := h₁ _
         }
#align lie_hom.inverse LieHom.inverse

end LieHom

section ModulePullBack

variable {R : Type u} {L₁ : Type v} {L₂ : Type w} (M : Type w₁)

variable [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂]

variable [AddCommGroup M] [LieRingModule L₂ M]

variable (f : L₁ →ₗ⁅R⁆ L₂)

/-- A Lie ring module may be pulled back along a morphism of Lie algebras.

See note [reducible non-instances]. -/
@[reducible]
def LieRingModule.compLieHom : LieRingModule L₁ M
    where
  bracket x m := ⁅f x, m⁆
  lie_add x := lie_add (f x)
  add_lie x y m := by simp only [LieHom.map_add, add_lie]
  leibniz_lie x y m := by simp only [lie_lie, sub_add_cancel, LieHom.map_lie]
#align lie_ring_module.comp_lie_hom LieRingModule.compLieHom

theorem LieRingModule.compLieHom_apply (x : L₁) (m : M) :
    haveI := LieRingModule.compLieHom M f
    ⁅x, m⁆ = ⁅f x, m⁆ :=
  rfl
#align lie_ring_module.comp_lie_hom_apply LieRingModule.compLieHom_apply

/-- A Lie module may be pulled back along a morphism of Lie algebras.

See note [reducible non-instances]. -/
@[reducible]
def LieModule.compLieHom [Module R M] [LieModule R L₂ M] :
    @LieModule R L₁ M _ _ _ _ _ (LieRingModule.compLieHom M f) :=
  { LieRingModule.compLieHom M f with
    smul_lie := fun t x m => by
      simp only [LieRingModule.compLieHom_apply, smul_lie, LieHom.map_smul]
    lie_smul := fun t x m => by
      simp only [LieRingModule.compLieHom_apply, lie_smul] }
#align lie_module.comp_lie_hom LieModule.compLieHom

end ModulePullBack

/-- An equivalence of Lie algebras is a morphism which is also a linear equivalence. We could
instead define an equivalence to be a morphism which is also a (plain) equivalence. However it is
more convenient to define via linear equivalence to get `.toLinearEquiv` for free. -/
structure LieEquiv (R : Type u) (L : Type v) (L' : Type w) [CommRing R] [LieRing L] [LieAlgebra R L]
  [LieRing L'] [LieAlgebra R L'] extends L →ₗ⁅R⁆ L' where
  /-- The inverse function of an equivalence of Lie algebras -/
  invFun : L' → L
  /-- The inverse function of an equivalence of Lie algebras is a left inverse of the underlying
  function. -/
  left_inv : Function.LeftInverse invFun toLieHom.toFun
  /-- The inverse function of an equivalence of Lie algebras is a right inverse of the underlying
  function. -/
  right_inv : Function.RightInverse invFun toLieHom.toFun
#align lie_equiv LieEquiv

@[inherit_doc]
notation:50 L " ≃ₗ⁅" R "⁆ " L' => LieEquiv R L L'

namespace LieEquiv

variable {R : Type u} {L₁ : Type v} {L₂ : Type w} {L₃ : Type w₁}

variable [CommRing R] [LieRing L₁] [LieRing L₂] [LieRing L₃]

variable [LieAlgebra R L₁] [LieAlgebra R L₂] [LieAlgebra R L₃]

/-- Consider an equivalence of Lie algebras as a linear equivalence. -/
def toLinearEquiv (f : L₁ ≃ₗ⁅R⁆ L₂) : L₁ ≃ₗ[R] L₂ :=
  { f.toLieHom, f with }
#align lie_equiv.to_linear_equiv LieEquiv.toLinearEquiv

instance hasCoeToLieHom : Coe (L₁ ≃ₗ⁅R⁆ L₂) (L₁ →ₗ⁅R⁆ L₂) :=
  ⟨toLieHom⟩
#align lie_equiv.has_coe_to_lie_hom LieEquiv.hasCoeToLieHom

instance hasCoeToLinearEquiv : Coe (L₁ ≃ₗ⁅R⁆ L₂) (L₁ ≃ₗ[R] L₂) :=
  ⟨toLinearEquiv⟩
#align lie_equiv.has_coe_to_linear_equiv LieEquiv.hasCoeToLinearEquiv

instance : EquivLike (L₁ ≃ₗ⁅R⁆ L₂) L₁ L₂ :=
  { coe := fun f => f.toFun,
    inv := fun f => f.invFun,
    left_inv := fun f => f.left_inv,
    right_inv := fun f => f.right_inv,
    coe_injective' := fun f g h₁ h₂ =>
      by cases f; cases g; simp at h₁ h₂; simp [*] }

theorem coe_to_lieHom (e : L₁ ≃ₗ⁅R⁆ L₂) : ⇑(e : L₁ →ₗ⁅R⁆ L₂) = e :=
  rfl
#align lie_equiv.coe_to_lie_hom LieEquiv.coe_to_lieHom

@[simp]
theorem coe_to_linearEquiv (e : L₁ ≃ₗ⁅R⁆ L₂) : ⇑(e : L₁ ≃ₗ[R] L₂) = e :=
  rfl
#align lie_equiv.coe_to_linear_equiv LieEquiv.coe_to_linearEquiv

@[simp]
theorem to_linearEquiv_mk (f : L₁ →ₗ⁅R⁆ L₂) (g h₁ h₂) :
    (mk f g h₁ h₂ : L₁ ≃ₗ[R] L₂) =
      { f with
        invFun := g
        left_inv := h₁
        right_inv := h₂ } :=
  rfl
#align lie_equiv.to_linear_equiv_mk LieEquiv.to_linearEquiv_mk

theorem coe_linearEquiv_injective : Injective ((↑) : (L₁ ≃ₗ⁅R⁆ L₂) → L₁ ≃ₗ[R] L₂) := by
  rintro ⟨⟨⟨⟨f, -⟩, -⟩, -⟩, f_inv⟩ ⟨⟨⟨⟨g, -⟩, -⟩, -⟩, g_inv⟩
  intro h
  simp only [to_linearEquiv_mk, LinearEquiv.mk.injEq, LinearMap.mk.injEq, AddHom.mk.injEq] at h
  congr
  exacts [h.1, h.2]
#align lie_equiv.coe_linear_equiv_injective LieEquiv.coe_linearEquiv_injective

theorem coe_injective : @Injective (L₁ ≃ₗ⁅R⁆ L₂) (L₁ → L₂) (↑) :=
  LinearEquiv.coe_injective.comp coe_linearEquiv_injective
#align lie_equiv.coe_injective LieEquiv.coe_injective

@[ext]
theorem ext {f g : L₁ ≃ₗ⁅R⁆ L₂} (h : ∀ x, f x = g x) : f = g :=
  coe_injective <| funext h
#align lie_equiv.ext LieEquiv.ext

instance : One (L₁ ≃ₗ⁅R⁆ L₁) :=
  ⟨{ (1 : L₁ ≃ₗ[R] L₁) with map_lie' := rfl }⟩

@[simp]
theorem one_apply (x : L₁) : (1 : L₁ ≃ₗ⁅R⁆ L₁) x = x :=
  rfl
#align lie_equiv.one_apply LieEquiv.one_apply

instance : Inhabited (L₁ ≃ₗ⁅R⁆ L₁) :=
  ⟨1⟩

/-- Lie algebra equivalences are reflexive. -/
def refl : L₁ ≃ₗ⁅R⁆ L₁ :=
  1
#align lie_equiv.refl LieEquiv.refl

@[simp]
theorem refl_apply (x : L₁) : (refl : L₁ ≃ₗ⁅R⁆ L₁) x = x :=
  rfl
#align lie_equiv.refl_apply LieEquiv.refl_apply

/-- Lie algebra equivalences are symmetric. -/
@[symm]
def symm (e : L₁ ≃ₗ⁅R⁆ L₂) : L₂ ≃ₗ⁅R⁆ L₁ :=
  { LieHom.inverse e.toLieHom e.invFun e.left_inv e.right_inv, e.toLinearEquiv.symm with }
#align lie_equiv.symm LieEquiv.symm

@[simp]
theorem symm_symm (e : L₁ ≃ₗ⁅R⁆ L₂) : e.symm.symm = e := by
  ext
  rfl
#align lie_equiv.symm_symm LieEquiv.symm_symm

@[simp]
theorem apply_symm_apply (e : L₁ ≃ₗ⁅R⁆ L₂) : ∀ x, e (e.symm x) = x :=
  e.toLinearEquiv.apply_symm_apply
#align lie_equiv.apply_symm_apply LieEquiv.apply_symm_apply

@[simp]
theorem symm_apply_apply (e : L₁ ≃ₗ⁅R⁆ L₂) : ∀ x, e.symm (e x) = x :=
  e.toLinearEquiv.symm_apply_apply
#align lie_equiv.symm_apply_apply LieEquiv.symm_apply_apply

@[simp]
theorem refl_symm : (refl : L₁ ≃ₗ⁅R⁆ L₁).symm = refl :=
  rfl
#align lie_equiv.refl_symm LieEquiv.refl_symm

/-- Lie algebra equivalences are transitive. -/
@[trans]
def trans (e₁ : L₁ ≃ₗ⁅R⁆ L₂) (e₂ : L₂ ≃ₗ⁅R⁆ L₃) : L₁ ≃ₗ⁅R⁆ L₃ :=
  { LieHom.comp e₂.toLieHom e₁.toLieHom, LinearEquiv.trans e₁.toLinearEquiv e₂.toLinearEquiv with }
#align lie_equiv.trans LieEquiv.trans

@[simp]
theorem self_trans_symm (e : L₁ ≃ₗ⁅R⁆ L₂) : e.trans e.symm = refl :=
  ext e.symm_apply_apply
#align lie_equiv.self_trans_symm LieEquiv.self_trans_symm

@[simp]
theorem symm_trans_self (e : L₁ ≃ₗ⁅R⁆ L₂) : e.symm.trans e = refl :=
  e.symm.self_trans_symm
#align lie_equiv.symm_trans_self LieEquiv.symm_trans_self

@[simp]
theorem trans_apply (e₁ : L₁ ≃ₗ⁅R⁆ L₂) (e₂ : L₂ ≃ₗ⁅R⁆ L₃) (x : L₁) : (e₁.trans e₂) x = e₂ (e₁ x) :=
  rfl
#align lie_equiv.trans_apply LieEquiv.trans_apply

@[simp]
theorem symm_trans (e₁ : L₁ ≃ₗ⁅R⁆ L₂) (e₂ : L₂ ≃ₗ⁅R⁆ L₃) :
    (e₁.trans e₂).symm = e₂.symm.trans e₁.symm :=
  rfl
#align lie_equiv.symm_trans LieEquiv.symm_trans

protected theorem bijective (e : L₁ ≃ₗ⁅R⁆ L₂) : Function.Bijective ((e : L₁ →ₗ⁅R⁆ L₂) : L₁ → L₂) :=
  e.toLinearEquiv.bijective
#align lie_equiv.bijective LieEquiv.bijective

protected theorem injective (e : L₁ ≃ₗ⁅R⁆ L₂) : Function.Injective ((e : L₁ →ₗ⁅R⁆ L₂) : L₁ → L₂) :=
  e.toLinearEquiv.injective
#align lie_equiv.injective LieEquiv.injective

protected theorem surjective (e : L₁ ≃ₗ⁅R⁆ L₂) :
    Function.Surjective ((e : L₁ →ₗ⁅R⁆ L₂) : L₁ → L₂) :=
  e.toLinearEquiv.surjective
#align lie_equiv.surjective LieEquiv.surjective

/-- A bijective morphism of Lie algebras yields an equivalence of Lie algebras. -/
@[simps!]
noncomputable def ofBijective (f : L₁ →ₗ⁅R⁆ L₂) (h : Function.Bijective f) : L₁ ≃ₗ⁅R⁆ L₂ :=
  { LinearEquiv.ofBijective (f : L₁ →ₗ[R] L₂)
      h with
    toFun := f
    map_lie' := by intros x y; exact f.map_lie x y }
#align lie_equiv.of_bijective LieEquiv.ofBijective

end LieEquiv

section LieModuleMorphisms

variable (R : Type u) (L : Type v) (M : Type w) (N : Type w₁) (P : Type w₂)

variable [CommRing R] [LieRing L] [LieAlgebra R L]

variable [AddCommGroup M] [AddCommGroup N] [AddCommGroup P]

variable [Module R M] [Module R N] [Module R P]

variable [LieRingModule L M] [LieRingModule L N] [LieRingModule L P]

variable [LieModule R L M] [LieModule R L N] [LieModule R L P]

/-- A morphism of Lie algebra modules is a linear map which commutes with the action of the Lie
algebra. -/
structure LieModuleHom extends M →ₗ[R] N where
  /-- A module of Lie algebra modules is compatible with the action of the Lie algebra on the
  modules. -/
  map_lie' : ∀ {x : L} {m : M}, toFun ⁅x, m⁆ = ⁅x, toFun m⁆
#align lie_module_hom LieModuleHom

@[inherit_doc]
notation:25 M " →ₗ⁅" R "," L:25 "⁆ " N:0 => LieModuleHom R L M N

namespace LieModuleHom

variable {R L M N P}

attribute [coe] LieModuleHom.toLinearMap

instance : CoeOut (M →ₗ⁅R,L⁆ N) (M →ₗ[R] N) :=
  ⟨LieModuleHom.toLinearMap⟩

instance : FunLike (M →ₗ⁅R, L⁆ N) M (fun _ => N) :=
  { coe := fun f => f.toFun,
    coe_injective' := fun x y h =>
      by cases x; cases y; simp at h; simp [h]  }

@[simp, norm_cast]
theorem coe_to_linearMap (f : M →ₗ⁅R,L⁆ N) : ((f : M →ₗ[R] N) : M → N) = f :=
  rfl
#align lie_module_hom.coe_to_linear_map LieModuleHom.coe_to_linearMap

@[simp]
theorem map_smul (f : M →ₗ⁅R,L⁆ N) (c : R) (x : M) : f (c • x) = c • f x :=
  LinearMap.map_smul (f : M →ₗ[R] N) c x
#align lie_module_hom.map_smul LieModuleHom.map_smul

@[simp]
theorem map_add (f : M →ₗ⁅R,L⁆ N) (x y : M) : f (x + y) = f x + f y :=
  LinearMap.map_add (f : M →ₗ[R] N) x y
#align lie_module_hom.map_add LieModuleHom.map_add

@[simp]
theorem map_sub (f : M →ₗ⁅R,L⁆ N) (x y : M) : f (x - y) = f x - f y :=
  LinearMap.map_sub (f : M →ₗ[R] N) x y
#align lie_module_hom.map_sub LieModuleHom.map_sub

@[simp]
theorem map_neg (f : M →ₗ⁅R,L⁆ N) (x : M) : f (-x) = -f x :=
  LinearMap.map_neg (f : M →ₗ[R] N) x
#align lie_module_hom.map_neg LieModuleHom.map_neg

@[simp]
theorem map_lie (f : M →ₗ⁅R,L⁆ N) (x : L) (m : M) : f ⁅x, m⁆ = ⁅x, f m⁆ :=
  LieModuleHom.map_lie' f
#align lie_module_hom.map_lie LieModuleHom.map_lie

theorem map_lie₂ (f : M →ₗ⁅R,L⁆ N →ₗ[R] P) (x : L) (m : M) (n : N) :
    ⁅x, f m n⁆ = f ⁅x, m⁆ n + f m ⁅x, n⁆ := by simp only [sub_add_cancel, map_lie, LieHom.lie_apply]
#align lie_module_hom.map_lie₂ LieModuleHom.map_lie₂

@[simp]
theorem map_zero (f : M →ₗ⁅R,L⁆ N) : f 0 = 0 :=
  LinearMap.map_zero (f : M →ₗ[R] N)
#align lie_module_hom.map_zero LieModuleHom.map_zero

/-- The identity map is a morphism of Lie modules. -/
def id : M →ₗ⁅R,L⁆ M :=
  { (LinearMap.id : M →ₗ[R] M) with map_lie' := rfl }
#align lie_module_hom.id LieModuleHom.id

@[simp]
theorem coe_id : ((id : M →ₗ⁅R,L⁆ M) : M → M) = _root_.id :=
  rfl
#align lie_module_hom.coe_id LieModuleHom.coe_id

theorem id_apply (x : M) : (id : M →ₗ⁅R,L⁆ M) x = x :=
  rfl
#align lie_module_hom.id_apply LieModuleHom.id_apply

/-- The constant 0 map is a Lie module morphism. -/
instance : Zero (M →ₗ⁅R,L⁆ N) :=
  ⟨{ (0 : M →ₗ[R] N) with map_lie' := by simp }⟩

@[norm_cast, simp]
theorem coe_zero : ⇑(0 : M →ₗ⁅R,L⁆ N) = 0 :=
  rfl
#align lie_module_hom.coe_zero LieModuleHom.coe_zero

theorem zero_apply (m : M) : (0 : M →ₗ⁅R,L⁆ N) m = 0 :=
  rfl
#align lie_module_hom.zero_apply LieModuleHom.zero_apply

/-- The identity map is a Lie module morphism. -/
instance : One (M →ₗ⁅R,L⁆ M) :=
  ⟨id⟩

instance : Inhabited (M →ₗ⁅R,L⁆ N) :=
  ⟨0⟩

theorem coe_injective : @Function.Injective (M →ₗ⁅R,L⁆ N) (M → N) (↑) := by
  rintro ⟨⟨⟨f, _⟩⟩⟩ ⟨⟨⟨g, _⟩⟩⟩ h
  congr
#align lie_module_hom.coe_injective LieModuleHom.coe_injective

@[ext]
theorem ext {f g : M →ₗ⁅R,L⁆ N} (h : ∀ m, f m = g m) : f = g :=
  coe_injective <| funext h
#align lie_module_hom.ext LieModuleHom.ext

theorem ext_iff {f g : M →ₗ⁅R,L⁆ N} : f = g ↔ ∀ m, f m = g m :=
  ⟨by
    rintro rfl m
    rfl, ext⟩
#align lie_module_hom.ext_iff LieModuleHom.ext_iff

theorem congr_fun {f g : M →ₗ⁅R,L⁆ N} (h : f = g) (x : M) : f x = g x :=
  h ▸ rfl
#align lie_module_hom.congr_fun LieModuleHom.congr_fun

@[simp]
theorem mk_coe (f : M →ₗ⁅R,L⁆ N) (h) : (⟨f, h⟩ : M →ₗ⁅R,L⁆ N) = f := by
  rfl
#align lie_module_hom.mk_coe LieModuleHom.mk_coe

@[simp]
theorem coe_mk (f : M →ₗ[R] N) (h) : ((⟨f, h⟩ : M →ₗ⁅R,L⁆ N) : M → N) = f := by
  rfl
#align lie_module_hom.coe_mk LieModuleHom.coe_mk

@[norm_cast]
theorem coe_linear_mk (f : M →ₗ[R] N) (h) : ((⟨f, h⟩ : M →ₗ⁅R,L⁆ N) : M →ₗ[R] N) = f := by
  rfl
#align lie_module_hom.coe_linear_mk LieModuleHom.coe_linear_mk

/-- The composition of Lie module morphisms is a morphism. -/
def comp (f : N →ₗ⁅R,L⁆ P) (g : M →ₗ⁅R,L⁆ N) : M →ₗ⁅R,L⁆ P :=
  { LinearMap.comp f.toLinearMap g.toLinearMap with
    map_lie' := by
      intros x m
      change f (g ⁅x, m⁆) = ⁅x, f (g m)⁆
      rw [map_lie, map_lie] }
#align lie_module_hom.comp LieModuleHom.comp

theorem comp_apply (f : N →ₗ⁅R,L⁆ P) (g : M →ₗ⁅R,L⁆ N) (m : M) : f.comp g m = f (g m) :=
  rfl
#align lie_module_hom.comp_apply LieModuleHom.comp_apply

@[norm_cast, simp]
theorem coe_comp (f : N →ₗ⁅R,L⁆ P) (g : M →ₗ⁅R,L⁆ N) : ⇑(f.comp g)  = f ∘ g :=
  rfl
#align lie_module_hom.coe_comp LieModuleHom.coe_comp

@[norm_cast, simp]
theorem coe_linearMap_comp (f : N →ₗ⁅R,L⁆ P) (g : M →ₗ⁅R,L⁆ N) :
    (f.comp g : M →ₗ[R] P) = (f : N →ₗ[R] P).comp (g : M →ₗ[R] N) :=
  rfl
#align lie_module_hom.coe_linear_map_comp LieModuleHom.coe_linearMap_comp

/-- The inverse of a bijective morphism of Lie modules is a morphism of Lie modules. -/
def inverse (f : M →ₗ⁅R,L⁆ N) (g : N → M) (h₁ : Function.LeftInverse g f)
    (h₂ : Function.RightInverse g f) : N →ₗ⁅R,L⁆ M :=
  { LinearMap.inverse f.toLinearMap g h₁ h₂ with
    map_lie' := by
      intros x n
      calc
        g ⁅x, n⁆ = g ⁅x, f (g n)⁆ := by rw [h₂]
        _ = g (f ⁅x, g n⁆) := by rw [map_lie]
        _ = ⁅x, g n⁆ := h₁ _
         }
#align lie_module_hom.inverse LieModuleHom.inverse

instance : Add (M →ₗ⁅R,L⁆ N)
    where add f g := { (f : M →ₗ[R] N) + (g : M →ₗ[R] N) with map_lie' := by simp }

instance : Sub (M →ₗ⁅R,L⁆ N)
    where sub f g := { (f : M →ₗ[R] N) - (g : M →ₗ[R] N) with map_lie' := by simp }

instance : Neg (M →ₗ⁅R,L⁆ N) where neg f := { -(f : M →ₗ[R] N) with map_lie' := by simp }

@[norm_cast, simp]
theorem coe_add (f g : M →ₗ⁅R,L⁆ N) : ⇑(f + g) = f + g :=
  rfl
#align lie_module_hom.coe_add LieModuleHom.coe_add

theorem add_apply (f g : M →ₗ⁅R,L⁆ N) (m : M) : (f + g) m = f m + g m :=
  rfl
#align lie_module_hom.add_apply LieModuleHom.add_apply

@[norm_cast, simp]
theorem coe_sub (f g : M →ₗ⁅R,L⁆ N) : ⇑(f - g) = f - g :=
  rfl
#align lie_module_hom.coe_sub LieModuleHom.coe_sub

theorem sub_apply (f g : M →ₗ⁅R,L⁆ N) (m : M) : (f - g) m = f m - g m :=
  rfl
#align lie_module_hom.sub_apply LieModuleHom.sub_apply

@[norm_cast, simp]
theorem coe_neg (f : M →ₗ⁅R,L⁆ N) : ⇑(-f) = -f :=
  rfl
#align lie_module_hom.coe_neg LieModuleHom.coe_neg

theorem neg_apply (f : M →ₗ⁅R,L⁆ N) (m : M) : (-f) m = -f m :=
  rfl
#align lie_module_hom.neg_apply LieModuleHom.neg_apply

instance hasNsmul : SMul ℕ (M →ₗ⁅R,L⁆ N)
    where smul n f := { n • (f : M →ₗ[R] N) with map_lie' := by simp }
#align lie_module_hom.has_nsmul LieModuleHom.hasNsmul

@[norm_cast, simp]
theorem coe_nsmul (n : ℕ) (f : M →ₗ⁅R,L⁆ N) : ⇑(n • f) = n • (⇑f) :=
  rfl
#align lie_module_hom.coe_nsmul LieModuleHom.coe_nsmul

theorem nsmul_apply (n : ℕ) (f : M →ₗ⁅R,L⁆ N) (m : M) : (n • f) m = n • f m :=
  rfl
#align lie_module_hom.nsmul_apply LieModuleHom.nsmul_apply

instance hasZsmul : SMul ℤ (M →ₗ⁅R,L⁆ N)
    where smul z f := { z • (f : M →ₗ[R] N) with map_lie' := by simp }
#align lie_module_hom.has_zsmul LieModuleHom.hasZsmul

@[norm_cast, simp]
theorem coe_zsmul (z : ℤ) (f : M →ₗ⁅R,L⁆ N) : ⇑(z • f) = z • (⇑f) :=
  rfl
#align lie_module_hom.coe_zsmul LieModuleHom.coe_zsmul

theorem zsmul_apply (z : ℤ) (f : M →ₗ⁅R,L⁆ N) (m : M) : (z • f) m = z • f m :=
  rfl
#align lie_module_hom.zsmul_apply LieModuleHom.zsmul_apply

instance : AddCommGroup (M →ₗ⁅R,L⁆ N) :=
  coe_injective.addCommGroup _ coe_zero coe_add coe_neg coe_sub (fun _ _ => coe_nsmul _ _)
    (fun _ _ => coe_zsmul _ _)

instance : SMul R (M →ₗ⁅R,L⁆ N) where smul t f := { t • (f : M →ₗ[R] N) with map_lie' := by simp }

@[norm_cast, simp]
theorem coe_smul (t : R) (f : M →ₗ⁅R,L⁆ N) : ⇑(t • f) = t • (⇑f) :=
  rfl
#align lie_module_hom.coe_smul LieModuleHom.coe_smul

theorem smul_apply (t : R) (f : M →ₗ⁅R,L⁆ N) (m : M) : (t • f) m = t • f m :=
  rfl
#align lie_module_hom.smul_apply LieModuleHom.smul_apply

instance : Module R (M →ₗ⁅R,L⁆ N) :=
  Function.Injective.module R ⟨⟨fun f => f.toLinearMap.toFun, rfl⟩, coe_add⟩ coe_injective coe_smul

end LieModuleHom

/-- An equivalence of Lie algebra modules is a linear equivalence which is also a morphism of
Lie algebra modules. -/
structure LieModuleEquiv extends M →ₗ⁅R,L⁆ N where
/-- The inverse function of an equivalence of Lie modules -/
  invFun : N → M
  /-- The inverse function of an equivalence of Lie modules is a left inverse of the underlying
  function. -/
  left_inv : Function.LeftInverse invFun toFun
  /-- The inverse function of an equivalence of Lie modules is a right inverse of the underlying
  function. -/
  right_inv : Function.RightInverse invFun toFun
#align lie_module_equiv LieModuleEquiv

attribute [nolint docBlame] LieModuleEquiv.toLieModuleHom

@[inherit_doc]
notation:25 M " ≃ₗ⁅" R "," L:25 "⁆ " N:0 => LieModuleEquiv R L M N

namespace LieModuleEquiv

variable {R L M N P}

/-- View an equivalence of Lie modules as a linear equivalence. -/
def toLinearEquiv (e : M ≃ₗ⁅R,L⁆ N) : M ≃ₗ[R] N :=
  { e with }
#align lie_module_equiv.to_linear_equiv LieModuleEquiv.toLinearEquiv

/-- View an equivalence of Lie modules as a type level equivalence. -/
def toEquiv (e : M ≃ₗ⁅R,L⁆ N) : M ≃ N :=
  { e with }
#align lie_module_equiv.to_equiv LieModuleEquiv.toEquiv

instance hasCoeToEquiv : CoeOut (M ≃ₗ⁅R,L⁆ N) (M ≃ N) :=
  ⟨toEquiv⟩
#align lie_module_equiv.has_coe_to_equiv LieModuleEquiv.hasCoeToEquiv

instance hasCoeToLieModuleHom : Coe (M ≃ₗ⁅R,L⁆ N) (M →ₗ⁅R,L⁆ N) :=
  ⟨toLieModuleHom⟩
#align lie_module_equiv.has_coe_to_lie_module_hom LieModuleEquiv.hasCoeToLieModuleHom

instance hasCoeToLinearEquiv : CoeOut (M ≃ₗ⁅R,L⁆ N) (M ≃ₗ[R] N) :=
  ⟨toLinearEquiv⟩
#align lie_module_equiv.has_coe_to_linear_equiv LieModuleEquiv.hasCoeToLinearEquiv

instance : EquivLike (M ≃ₗ⁅R,L⁆ N) M N :=
  { coe := fun f => f.toFun,
    inv := fun f => f.invFun,
    left_inv := fun f => f.left_inv,
    right_inv := fun f => f.right_inv,
    coe_injective' := fun f g h₁ h₂ =>
      by cases f; cases g; simp at h₁ h₂; simp [*] }

theorem injective (e : M ≃ₗ⁅R,L⁆ N) : Function.Injective e :=
  e.toEquiv.injective
#align lie_module_equiv.injective LieModuleEquiv.injective

@[simp]
theorem toEquiv_mk (f : M →ₗ⁅R,L⁆ N) (g : N → M) (h₁ h₂) :
  toEquiv (mk f g h₁ h₂ : M ≃ₗ⁅R,L⁆ N) = Equiv.mk f g h₁ h₂ :=
  rfl

@[simp]
theorem coe_mk (f : M →ₗ⁅R,L⁆ N) (invFun h₁ h₂) :
    ((⟨f, invFun, h₁, h₂⟩ : M ≃ₗ⁅R,L⁆ N) : M → N) = f :=
  rfl
#align lie_module_equiv.coe_mk LieModuleEquiv.coe_mk

theorem coe_to_lieModuleHom (e : M ≃ₗ⁅R,L⁆ N) : ⇑(e : M →ₗ⁅R,L⁆ N) = e :=
  rfl
#align lie_module_equiv.coe_to_lie_module_hom LieModuleEquiv.coe_to_lieModuleHom

@[simp]
theorem coe_to_linearEquiv (e : M ≃ₗ⁅R,L⁆ N) : ((e : M ≃ₗ[R] N) : M → N) = e :=
  rfl
#align lie_module_equiv.coe_to_linear_equiv LieModuleEquiv.coe_to_linearEquiv

theorem toEquiv_injective : Function.Injective (toEquiv : (M ≃ₗ⁅R,L⁆ N) → M ≃ N) :=
  by
  rintro ⟨⟨⟨⟨f, -⟩, -⟩, -⟩, f_inv⟩ ⟨⟨⟨⟨g, -⟩, -⟩, -⟩, g_inv⟩
  intro h
  simp only [toEquiv_mk, LieModuleHom.coe_mk, LinearMap.coe_mk, AddHom.coe_mk, Equiv.mk.injEq] at h
  congr
  exacts [h.1, h.2]
#align lie_module_equiv.to_equiv_injective LieModuleEquiv.toEquiv_injective

@[ext]
theorem ext (e₁ e₂ : M ≃ₗ⁅R,L⁆ N) (h : ∀ m, e₁ m = e₂ m) : e₁ = e₂ :=
  toEquiv_injective (Equiv.ext h)
#align lie_module_equiv.ext LieModuleEquiv.ext

instance : One (M ≃ₗ⁅R,L⁆ M) :=
  ⟨{ (1 : M ≃ₗ[R] M) with map_lie' := rfl }⟩

@[simp]
theorem one_apply (m : M) : (1 : M ≃ₗ⁅R,L⁆ M) m = m :=
  rfl
#align lie_module_equiv.one_apply LieModuleEquiv.one_apply

instance : Inhabited (M ≃ₗ⁅R,L⁆ M) :=
  ⟨1⟩

/-- Lie module equivalences are reflexive. -/
@[refl]
def refl : M ≃ₗ⁅R,L⁆ M :=
  1
#align lie_module_equiv.refl LieModuleEquiv.refl

@[simp]
theorem refl_apply (m : M) : (refl : M ≃ₗ⁅R,L⁆ M) m = m :=
  rfl
#align lie_module_equiv.refl_apply LieModuleEquiv.refl_apply

/-- Lie module equivalences are syemmtric. -/
@[symm]
def symm (e : M ≃ₗ⁅R,L⁆ N) : N ≃ₗ⁅R,L⁆ M :=
  { LieModuleHom.inverse e.toLieModuleHom e.invFun e.left_inv e.right_inv,
    (e : M ≃ₗ[R] N).symm with }
#align lie_module_equiv.symm LieModuleEquiv.symm

@[simp]
theorem apply_symm_apply (e : M ≃ₗ⁅R,L⁆ N) : ∀ x, e (e.symm x) = x :=
  e.toLinearEquiv.apply_symm_apply
#align lie_module_equiv.apply_symm_apply LieModuleEquiv.apply_symm_apply

@[simp]
theorem symm_apply_apply (e : M ≃ₗ⁅R,L⁆ N) : ∀ x, e.symm (e x) = x :=
  e.toLinearEquiv.symm_apply_apply
#align lie_module_equiv.symm_apply_apply LieModuleEquiv.symm_apply_apply

@[simp]
theorem symm_symm (e : M ≃ₗ⁅R,L⁆ N) : e.symm.symm = e := by
  rfl
#align lie_module_equiv.symm_symm LieModuleEquiv.symm_symm

/-- Lie module equivalences are transitive. -/
@[trans]
def trans (e₁ : M ≃ₗ⁅R,L⁆ N) (e₂ : N ≃ₗ⁅R,L⁆ P) : M ≃ₗ⁅R,L⁆ P :=
  { LieModuleHom.comp e₂.toLieModuleHom e₁.toLieModuleHom,
    LinearEquiv.trans e₁.toLinearEquiv e₂.toLinearEquiv with }
#align lie_module_equiv.trans LieModuleEquiv.trans

@[simp]
theorem trans_apply (e₁ : M ≃ₗ⁅R,L⁆ N) (e₂ : N ≃ₗ⁅R,L⁆ P) (m : M) : (e₁.trans e₂) m = e₂ (e₁ m) :=
  rfl
#align lie_module_equiv.trans_apply LieModuleEquiv.trans_apply

@[simp]
theorem symm_trans (e₁ : M ≃ₗ⁅R,L⁆ N) (e₂ : N ≃ₗ⁅R,L⁆ P) :
    (e₁.trans e₂).symm = e₂.symm.trans e₁.symm :=
  rfl
#align lie_module_equiv.symm_trans LieModuleEquiv.symm_trans

@[simp]
theorem self_trans_symm (e : M ≃ₗ⁅R,L⁆ N) : e.trans e.symm = refl :=
  ext _ _ e.symm_apply_apply
#align lie_module_equiv.self_trans_symm LieModuleEquiv.self_trans_symm

@[simp]
theorem symm_trans_self (e : M ≃ₗ⁅R,L⁆ N) : e.symm.trans e = refl :=
  ext _ _ e.apply_symm_apply
#align lie_module_equiv.symm_trans_self LieModuleEquiv.symm_trans_self

end LieModuleEquiv

end LieModuleMorphisms

author: leanprover-community