[GOAL]
α : Sort u_1
inst✝ : Subsingleton α
p : α → Prop
x✝¹ x✝ : Subtype p
x : α
property✝¹ : p x
y : α
property✝ : p y
⊢ { val := x, property := property✝¹ } = { val := y, property := property✝ }
[PROOFSTEP]
cases Subsingleton.elim x y
[GOAL]
case refl
α : Sort u_1
inst✝ : Subsingleton α
p : α → Prop
x✝¹ x✝ : Subtype p
x : α
property✝¹ property✝ : p x
⊢ { val := x, property := property✝¹ } = { val := x, property := property✝ }
[PROOFSTEP]
rfl
[GOAL]
α β : Sort u_1
γ : Sort u_2
f : α → γ
g : β → γ
x : α
y : β
h₁ : HEq f g
h₂ : HEq x y
⊢ f x = g y
[PROOFSTEP]
cases h₂
[GOAL]
case refl
α : Sort u_1
γ : Sort u_2
f : α → γ
x : α
g : α → γ
h₁ : HEq f g
⊢ f x = g x
[PROOFSTEP]
cases h₁
[GOAL]
case refl.refl
α : Sort u_1
γ : Sort u_2
f : α → γ
x : α
⊢ f x = f x
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
a b : α
x✝ : { down := a }.down = { down := b }.down
⊢ { down := a } = { down := b }
[PROOFSTEP]
congr
[GOAL]
α : Type u_1
a b : ULift α
h : a = b
⊢ a.down = b.down
[PROOFSTEP]
rw [h]
[GOAL]
α : Sort u_1
a b : α
x✝ : { down := a }.down = { down := b }.down
⊢ { down := a } = { down := b }
[PROOFSTEP]
congr
[GOAL]
α : Sort u_1
a b : PLift α
h : a = b
⊢ a.down = b.down
[PROOFSTEP]
rw [h]
[GOAL]
α : Sort u_1
b c : α
h : ∀ {a : α}, a = b ↔ a = c
⊢ b = c
[PROOFSTEP]
rw [← h]
[GOAL]
α : Sort u_1
b c : α
h : b = c
a : α
⊢ a = b ↔ a = c
[PROOFSTEP]
rw [h]
[GOAL]
α : Sort u_1
a b : α
h : ∀ {c : α}, a = c ↔ b = c
⊢ a = b
[PROOFSTEP]
rw [h]
[GOAL]
α : Sort u_1
a✝ b : α
h : a✝ = b
a : α
⊢ a✝ = a ↔ b = a
[PROOFSTEP]
rw [h]
[GOAL]
⊢ Eq True = id
[PROOFSTEP]
funext _
[GOAL]
case h
x✝ : Prop
⊢ (True = x✝) = id x✝
[PROOFSTEP]
simp only [true_iff, id.def, eq_iff_iff]
[GOAL]
⊢ Xor' True = Not
[PROOFSTEP]
simp [Xor']
[GOAL]
⊢ Xor' False = id
[PROOFSTEP]
ext
[GOAL]
case h.a
x✝ : Prop
⊢ Xor' False x✝ ↔ id x✝
[PROOFSTEP]
simp [Xor']
[GOAL]
a b : Prop
⊢ Xor' a b = Xor' b a
[PROOFSTEP]
simp [Xor', and_comm, or_comm]
[GOAL]
a : Prop
⊢ Xor' a a = False
[PROOFSTEP]
simp [Xor']
[GOAL]
a b : Prop
⊢ Xor' (¬a) b ↔ (a ↔ b)
[PROOFSTEP]
by_cases a
[GOAL]
a b : Prop
⊢ Xor' (¬a) b ↔ (a ↔ b)
[PROOFSTEP]
by_cases a
[GOAL]
case pos
a b : Prop
h : a
⊢ Xor' (¬a) b ↔ (a ↔ b)
[PROOFSTEP]
simp [*]
[GOAL]
case neg
a b : Prop
h : ¬a
⊢ Xor' (¬a) b ↔ (a ↔ b)
[PROOFSTEP]
simp [*]
[GOAL]
a b : Prop
⊢ Xor' a ¬b ↔ (a ↔ b)
[PROOFSTEP]
by_cases a
[GOAL]
a b : Prop
⊢ Xor' a ¬b ↔ (a ↔ b)
[PROOFSTEP]
by_cases a
[GOAL]
case pos
a b : Prop
h : a
⊢ Xor' a ¬b ↔ (a ↔ b)
[PROOFSTEP]
simp [*]
[GOAL]
case neg
a b : Prop
h : ¬a
⊢ Xor' a ¬b ↔ (a ↔ b)
[PROOFSTEP]
simp [*]
[GOAL]
a b : Prop
⊢ Xor' (¬a) ¬b ↔ Xor' a b
[PROOFSTEP]
simp [Xor', or_comm, and_comm]
[GOAL]
α : Sort u_1
a b : α
p : Prop
⊢ p ∧ a = b ↔ p ∧ b = a
[PROOFSTEP]
simp [eq_comm]
[GOAL]
α : Sort u_1
a b : α
p : Prop
⊢ a = b ∧ p ↔ b = a ∧ p
[PROOFSTEP]
simp [eq_comm]
[GOAL]
P Q : Prop
⊢ ¬Xor' P Q ↔ (P ↔ Q)
[PROOFSTEP]
simp only [not_and, Xor', not_or, not_not, ← iff_iff_implies_and_implies]
[GOAL]
a b : Prop
⊢ Xor' a b ↔ (a ↔ ¬b)
[PROOFSTEP]
simp only [← @xor_not_right a, not_not]
[GOAL]
a b : Prop
⊢ Xor' a b ↔ (¬a ↔ b)
[PROOFSTEP]
simp only [← @xor_not_left _ b, not_not]
[GOAL]
a✝¹ a✝ : Sort u_1
e : a✝¹ = a✝
a : a✝¹
a' : a✝
h : HEq a a'
⊢ cast e a = a'
[PROOFSTEP]
cases h
[GOAL]
case refl
a✝ : Sort u_1
a : a✝
e : a✝ = a✝
⊢ cast e a = a
[PROOFSTEP]
rfl
[GOAL]
α : Sort u_1
a' : α
motive : (a : α) → a' = a → Sort u
p : motive a' (_ : a' = a')
a : α
t : a' = a
⊢ HEq (t ▸ p) p
[PROOFSTEP]
subst t
[GOAL]
α : Sort u_1
a' : α
motive : (a : α) → a' = a → Sort u
p : motive a' (_ : a' = a')
⊢ HEq ((_ : a' = a') ▸ p) p
[PROOFSTEP]
rfl
[GOAL]
α : Sort u_2
a : α
β : Sort u_1
b : α
C : α → Sort u_1
x : C a
y : β
e : a = b
h : HEq x y
⊢ HEq (e ▸ x) y
[PROOFSTEP]
subst e
[GOAL]
α : Sort u_2
a : α
β : Sort u_1
C : α → Sort u_1
x : C a
y : β
h : HEq x y
⊢ HEq ((_ : a = a) ▸ x) y
[PROOFSTEP]
exact h
[GOAL]
α : Sort u_2
a : α
β : Sort u_1
b : α
C : α → Sort u_1
x : C a
y : β
e : a = b
⊢ HEq (e ▸ x) y ↔ HEq x y
[PROOFSTEP]
subst e
[GOAL]
α : Sort u_2
a : α
β : Sort u_1
C : α → Sort u_1
x : C a
y : β
⊢ HEq ((_ : a = a) ▸ x) y ↔ HEq x y
[PROOFSTEP]
rfl
[GOAL]
α : Sort u_2
β : Sort u_1
a b : α
C : α → Sort u_1
x : β
y : C a
e : a = b
⊢ HEq x (e ▸ y) ↔ HEq x y
[PROOFSTEP]
subst e
[GOAL]
α : Sort u_2
β : Sort u_1
a : α
C : α → Sort u_1
x : β
y : C a
⊢ HEq x ((_ : a = a) ▸ y) ↔ HEq x y
[PROOFSTEP]
rfl
[GOAL]
α✝ : Sort u_1
x₁ y₁ x₂ y₂ : α✝
h₁ : x₁ = y₁
h₂ : x₂ = y₂
⊢ x₁ = x₂ ↔ y₁ = y₂
[PROOFSTEP]
subst h₁
[GOAL]
α✝ : Sort u_1
x₁ x₂ y₂ : α✝
h₂ : x₂ = y₂
⊢ x₁ = x₂ ↔ x₁ = y₂
[PROOFSTEP]
subst h₂
[GOAL]
α✝ : Sort u_1
x₁ x₂ : α✝
⊢ x₁ = x₂ ↔ x₁ = x₂
[PROOFSTEP]
rfl
[GOAL]
α : Sort u_1
x y z : α
h : x = y
⊢ x = z ↔ y = z
[PROOFSTEP]
rw [h]
[GOAL]
α : Sort u_1
x y z : α
h : x = y
⊢ z = x ↔ z = y
[PROOFSTEP]
rw [h]
[GOAL]
ι : Sort ?u.13179
α : Sort u_2
κ : ι → Sort u_1
p q : α → Prop
inst✝ : (x : α) → Decidable (p x)
⊢ (¬∃ x, ¬p x) ↔ ∀ (x : α), p x
[PROOFSTEP]
simp only [not_exists, Decidable.not_not]
[GOAL]
ι : Sort ?u.13446
α : Sort u_2
κ : ι → Sort u_1
p q : α → Prop
b : Prop
ha : Nonempty α
⊢ (∀ (x : α), p x) → b ↔ ∃ x, p x → b
[PROOFSTEP]
let ⟨a⟩ := ha
[GOAL]
ι : Sort ?u.13446
α : Sort u_2
κ : ι → Sort u_1
p q : α → Prop
b : Prop
ha : Nonempty α
a : α
⊢ (∀ (x : α), p x) → b ↔ ∃ x, p x → b
[PROOFSTEP]
refine ⟨fun h ↦ not_forall_not.1 fun h' ↦ ?_, fun ⟨x, hx⟩ h ↦ hx (h x)⟩
[GOAL]
ι : Sort ?u.13446
α : Sort u_2
κ : ι → Sort u_1
p q : α → Prop
b : Prop
ha : Nonempty α
a : α
h : (∀ (x : α), p x) → b
h' : ∀ (x : α), ¬(p x → b)
⊢ False
[PROOFSTEP]
exact if hb : b then h' a fun _ ↦ hb else hb <| h fun x ↦ (not_imp.1 (h' x)).1
[GOAL]
ι : Sort ?u.13873
α : Sort ?u.13878
κ : ι → Sort u_1
p q : α → Prop
β : α → Sort u_2
⊢ (∀ (a : α), β a → True) ↔ True
[PROOFSTEP]
simp
[GOAL]
ι : Sort ?u.14073
α : Sort ?u.14078
κ : ι → Sort u_1
p q : α → Prop
β : α → Sort u_2
γ : (a : α) → β a → Sort u_3
⊢ (∀ (a : α) (b : β a), γ a b → True) ↔ True
[PROOFSTEP]
simp
[GOAL]
ι : Sort ?u.14717
α✝ : Sort ?u.14722
κ : ι → Sort u_1
p q : α✝ → Prop
b : Prop
α : Sort u_2
i : Nonempty α
inst✝ : Subsingleton α
⊢ (∃! x, b) ↔ b
[PROOFSTEP]
simp
[GOAL]
ι : Sort ?u.14980
α : Sort u_2
κ : ι → Sort u_1
p✝ q : α → Prop
inst✝ : DecidableEq α
a : α
p : α → Prop
⊢ (p a ∧ ∀ (b : α), b ≠ a → p b) ↔ ∀ (b : α), p b
[PROOFSTEP]
simp only [← @forall_eq _ p a, ← forall_and, ← or_imp, Decidable.em, forall_const]
[GOAL]
ι : Sort ?u.15561
α : Sort u_2
κ : ι → Sort u_1
p q : α → Prop
a' : α
⊢ ∃! a, a = a'
[PROOFSTEP]
simp only [eq_comm, ExistsUnique, and_self, forall_eq', exists_eq']
[GOAL]
ι : Sort ?u.15937
α : Sort u_2
κ : ι → Sort u_1
p q : α → Prop
a' : α
⊢ ∃! a, a' = a
[PROOFSTEP]
simp only [ExistsUnique, and_self, forall_eq', exists_eq']
[GOAL]
ι : Sort ?u.17741
α : Sort ?u.17746
κ : ι → Sort u_1
p✝ q : α → Prop
β : Sort u_2
f : α → β
p : β → Prop
⊢ (∀ (a : α) (b : β), f a = b → p b) ↔ ∀ (a : α), p (f a)
[PROOFSTEP]
simp
[GOAL]
ι : Sort ?u.18041
α : Sort ?u.18046
κ : ι → Sort u_1
p✝ q : α → Prop
β : Sort u_2
f : α → β
p : β → Prop
⊢ (∀ (b : β) (a : α), f a = b → p b) ↔ ∀ (a : α), p (f a)
[PROOFSTEP]
simp [forall_swap]
[GOAL]
ι : Sort ?u.18571
α : Sort ?u.18576
κ : ι → Sort u_1
p✝ q : α → Prop
β : Sort u_2
f : α → β
p : β → Prop
⊢ (∀ (a : α) (b : β), b = f a → p b) ↔ ∀ (a : α), p (f a)
[PROOFSTEP]
simp
[GOAL]
ι : Sort ?u.18901
α : Sort ?u.18906
κ : ι → Sort u_1
p✝ q : α → Prop
β : Sort u_2
f : α → β
p : β → Prop
⊢ (∀ (b : β) (a : α), b = f a → p b) ↔ ∀ (a : α), p (f a)
[PROOFSTEP]
simp [forall_swap]
[GOAL]
ι : Sort ?u.19647
α : Sort u_2
κ : ι → Sort u_1
p q : α → Prop
a' : α
⊢ (∃ a, p a ∧ a' = a) ↔ p a'
[PROOFSTEP]
simp [@eq_comm _ a']
[GOAL]
ι : Sort ?u.19995
α : Sort ?u.20000
κ : ι → Sort u_1
p✝ q : α → Prop
ι₁ : Sort u_4
ι₂ : Sort u_5
κ₁ : ι₁ → Sort u_2
κ₂ : ι₂ → Sort u_3
p : (i₁ : ι₁) → κ₁ i₁ → (i₂ : ι₂) → κ₂ i₂ → Prop
⊢ (∃ i₁ j₁ i₂ j₂, p i₁ j₁ i₂ j₂) ↔ ∃ i₂ j₂ i₁ j₁, p i₁ j₁ i₂ j₂
[PROOFSTEP]
simp only [@exists_comm (κ₁ _), @exists_comm ι₁]
[GOAL]
ι : Sort ?u.21140
α : Sort ?u.21145
κ : ι → Sort u_1
p✝ q✝ : α → Prop
q : Prop
p : α → Prop
inst✝ : Decidable q
⊢ (∀ (x : α), p x ∨ q) ↔ (∀ (x : α), p x) ∨ q
[PROOFSTEP]
simp [or_comm, Decidable.forall_or_left]
[GOAL]
ι : Sort ?u.21525
α : Sort ?u.21530
κ : ι → Sort u_1
p✝ q✝ : α → Prop
p q : Prop
⊢ (∃! x, q) ↔ p ∧ q
[PROOFSTEP]
simp
[GOAL]
ι : Sort ?u.22333
α : Sort ?u.22338
κ : ι → Sort u_1
p✝ q : α → Prop
p : Prop → Prop
x✝ : ∃ h, p h
h₁ : Prop
h₂ : p h₁
H : h₁
⊢ p True
[PROOFSTEP]
simpa only [H] using h₂
[GOAL]
ι : Sort ?u.22333
α : Sort ?u.22338
κ : ι → Sort u_1
p✝ q : α → Prop
p : Prop → Prop
x✝ : ∃ h, p h
h₁ : Prop
h₂ : p h₁
H : ¬h₁
⊢ p False
[PROOFSTEP]
simpa only [H] using h₂
[GOAL]
ι : Sort ?u.22592
α : Sort ?u.22597
κ : ι → Sort u_1
p✝ q : α → Prop
p : Prop → Prop
x✝ : p False ∧ p True
h : Prop
h₁ : p False
h₂ : p True
⊢ p h
[PROOFSTEP]
by_cases H : h
[GOAL]
case pos
ι : Sort ?u.22592
α : Sort ?u.22597
κ : ι → Sort u_1
p✝ q : α → Prop
p : Prop → Prop
x✝ : p False ∧ p True
h : Prop
h₁ : p False
h₂ : p True
H : h
⊢ p h
[PROOFSTEP]
simpa only [H]
[GOAL]
case neg
ι : Sort ?u.22592
α : Sort ?u.22597
κ : ι → Sort u_1
p✝ q : α → Prop
p : Prop → Prop
x✝ : p False ∧ p True
h : Prop
h₁ : p False
h₂ : p True
H : ¬h
⊢ p h
[PROOFSTEP]
simpa only [H]
[GOAL]
ι : Sort ?u.23891
α✝ : Sort ?u.23896
κ : ι → Sort u_1
p✝ q✝ : α✝ → Prop
α : Sort u_2
p : α → Sort u_3
inst✝ : ∀ (x : α), Subsingleton (p x)
q : (x : α) → p x → Prop
b : Prop
h₂ : ∃! x h, q x h
h₁ : ∀ (x : α) (h : p x), q x h → (∀ (y : α) (hy : p y), q y hy → y = x) → b
⊢ b
[PROOFSTEP]
simp only [exists_unique_iff_exists] at h₂
[GOAL]
ι : Sort ?u.23891
α✝ : Sort ?u.23896
κ : ι → Sort u_1
p✝ q✝ : α✝ → Prop
α : Sort u_2
p : α → Sort u_3
inst✝ : ∀ (x : α), Subsingleton (p x)
q : (x : α) → p x → Prop
b : Prop
h₁ : ∀ (x : α) (h : p x), q x h → (∀ (y : α) (hy : p y), q y hy → y = x) → b
h₂ : ∃! x, ∃ h, q x h
⊢ b
[PROOFSTEP]
apply h₂.elim
[GOAL]
ι : Sort ?u.23891
α✝ : Sort ?u.23896
κ : ι → Sort u_1
p✝ q✝ : α✝ → Prop
α : Sort u_2
p : α → Sort u_3
inst✝ : ∀ (x : α), Subsingleton (p x)
q : (x : α) → p x → Prop
b : Prop
h₁ : ∀ (x : α) (h : p x), q x h → (∀ (y : α) (hy : p y), q y hy → y = x) → b
h₂ : ∃! x, ∃ h, q x h
⊢ ∀ (x : α), (∃ h, q x h) → (∀ (y : α), (∃ h, q y h) → y = x) → b
[PROOFSTEP]
exact fun x ⟨hxp, hxq⟩ H ↦ h₁ x hxp hxq fun y hyp hyq ↦ H y ⟨hyp, hyq⟩
[GOAL]
ι : Sort ?u.24313
α✝ : Sort ?u.24318
κ : ι → Sort u_1
p✝ q✝ : α✝ → Prop
α : Sort u_2
p : α → Sort u_3
inst✝ : ∀ (x : α), Subsingleton (p x)
q : (x : α) → p x → Prop
w : α
hp : p w
hq : q w hp
H : ∀ (y : α) (hy : p y), q y hy → y = w
⊢ ∃! x hx, q x hx
[PROOFSTEP]
simp only [exists_unique_iff_exists]
[GOAL]
ι : Sort ?u.24313
α✝ : Sort ?u.24318
κ : ι → Sort u_1
p✝ q✝ : α✝ → Prop
α : Sort u_2
p : α → Sort u_3
inst✝ : ∀ (x : α), Subsingleton (p x)
q : (x : α) → p x → Prop
w : α
hp : p w
hq : q w hp
H : ∀ (y : α) (hy : p y), q y hy → y = w
⊢ ∃! x, ∃ hx, q x hx
[PROOFSTEP]
exact ExistsUnique.intro w ⟨hp, hq⟩ fun y ⟨hyp, hyq⟩ ↦ H y hyp hyq
[GOAL]
ι : Sort ?u.24821
α✝ : Sort ?u.24826
κ : ι → Sort u_1
p✝ q✝ : α✝ → Prop
α : Sort u_2
p : α → Sort u_3
inst✝ : ∀ (x : α), Subsingleton (p x)
q : (x : α) → p x → Prop
h : ∃! x hx, q x hx
y₁ y₂ : α
hpy₁ : p y₁
hqy₁ : q y₁ hpy₁
hpy₂ : p y₂
hqy₂ : q y₂ hpy₂
⊢ y₁ = y₂
[PROOFSTEP]
simp only [exists_unique_iff_exists] at h
[GOAL]
ι : Sort ?u.24821
α✝ : Sort ?u.24826
κ : ι → Sort u_1
p✝ q✝ : α✝ → Prop
α : Sort u_2
p : α → Sort u_3
inst✝ : ∀ (x : α), Subsingleton (p x)
q : (x : α) → p x → Prop
y₁ y₂ : α
hpy₁ : p y₁
hqy₁ : q y₁ hpy₁
hpy₂ : p y₂
hqy₂ : q y₂ hpy₂
h : ∃! x, ∃ hx, q x hx
⊢ y₁ = y₂
[PROOFSTEP]
exact h.unique ⟨hpy₁, hqy₁⟩ ⟨hpy₂, hqy₂⟩
[GOAL]
α : Sort ?u.25125
p✝ : α → Prop
p : Prop
⊢ Decidable p
[PROOFSTEP]
infer_instance
[GOAL]
α : Sort ?u.25149
p✝ p : α → Prop
⊢ DecidablePred p
[PROOFSTEP]
infer_instance
[GOAL]
α : Sort ?u.25193
p✝ : α → Prop
p : α → α → Prop
⊢ DecidableRel p
[PROOFSTEP]
infer_instance
[GOAL]
α✝ : Sort ?u.25252
p : α✝ → Prop
α : Sort u
⊢ DecidableEq α
[PROOFSTEP]
infer_instance
[GOAL]
α : Sort u_1
r p q : α → Prop
P Q : (x : α) → p x → Prop
b : Prop
a : α
⊢ (∃ x x_1, p x) ↔ p a
[PROOFSTEP]
simp only [exists_prop, exists_eq_left]
[GOAL]
α : Sort u_1
r p q : α → Prop
P Q : (x : α) → p x → Prop
b : Prop
⊢ (∃ x h, P x h) → b ↔ ∀ (x : α) (h : p x), P x h → b
[PROOFSTEP]
simp
[GOAL]
α : Sort u_1
r p q : α → Prop
P Q : (x : α) → p x → Prop
b : Prop
⊢ (∃ x x_1, r x) ↔ (∃ x x_1, r x) ∨ ∃ x x_1, r x
[PROOFSTEP]
simp only [exists_prop]
[GOAL]
α : Sort u_1
r p q : α → Prop
P Q : (x : α) → p x → Prop
b : Prop
⊢ (∃ x, (p x ∨ q x) ∧ r x) ↔ (∃ x, p x ∧ r x) ∨ ∃ x, q x ∧ r x
[PROOFSTEP]
exact Iff.trans (exists_congr fun x ↦ or_and_right) exists_or
[GOAL]
α : Sort u_2
β : Sort ?u.31192
σ : α → Sort u_1
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B : ¬P → α
⊢ dite P A B = c ↔ (∃ h, A h = c) ∨ ∃ h, B h = c
[PROOFSTEP]
by_cases P
[GOAL]
α : Sort u_2
β : Sort ?u.31192
σ : α → Sort u_1
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B : ¬P → α
⊢ dite P A B = c ↔ (∃ h, A h = c) ∨ ∃ h, B h = c
[PROOFSTEP]
by_cases P
[GOAL]
case pos
α : Sort u_2
β : Sort ?u.31192
σ : α → Sort u_1
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B : ¬P → α
h : P
⊢ dite P A B = c ↔ (∃ h, A h = c) ∨ ∃ h, B h = c
[PROOFSTEP]
simp [*, exists_prop_of_true, exists_prop_of_false]
[GOAL]
case neg
α : Sort u_2
β : Sort ?u.31192
σ : α → Sort u_1
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B : ¬P → α
h : ¬P
⊢ dite P A B = c ↔ (∃ h, A h = c) ∨ ∃ h, B h = c
[PROOFSTEP]
simp [*, exists_prop_of_true, exists_prop_of_false]
[GOAL]
α : Sort u_2
β : Sort ?u.31675
σ : α → Sort u_1
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B : ¬P → α
⊢ ((∃ h, (fun x => a) h = c) ∨ ∃ h, (fun x => b) h = c) ↔ P ∧ a = c ∨ ¬P ∧ b = c
[PROOFSTEP]
simp only
[GOAL]
α : Sort u_2
β : Sort ?u.31675
σ : α → Sort u_1
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B : ¬P → α
⊢ ((∃ h, a = c) ∨ ∃ h, b = c) ↔ P ∧ a = c ∨ ¬P ∧ b = c
[PROOFSTEP]
rw [exists_prop, exists_prop]
[GOAL]
α : Sort u_2
β : Sort ?u.32661
σ : α → Sort u_1
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B : ¬P → α
⊢ dite P (fun x => a) B = a ↔ ∀ (h : ¬P), B h = a
[PROOFSTEP]
by_cases P
[GOAL]
α : Sort u_2
β : Sort ?u.32661
σ : α → Sort u_1
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B : ¬P → α
⊢ dite P (fun x => a) B = a ↔ ∀ (h : ¬P), B h = a
[PROOFSTEP]
by_cases P
[GOAL]
case pos
α : Sort u_2
β : Sort ?u.32661
σ : α → Sort u_1
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B : ¬P → α
h : P
⊢ dite P (fun x => a) B = a ↔ ∀ (h : ¬P), B h = a
[PROOFSTEP]
simp [*, forall_prop_of_true, forall_prop_of_false]
[GOAL]
case neg
α : Sort u_2
β : Sort ?u.32661
σ : α → Sort u_1
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B : ¬P → α
h : ¬P
⊢ dite P (fun x => a) B = a ↔ ∀ (h : ¬P), B h = a
[PROOFSTEP]
simp [*, forall_prop_of_true, forall_prop_of_false]
[GOAL]
α : Sort u_2
β : Sort ?u.33174
σ : α → Sort u_1
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B : ¬P → α
⊢ (dite P A fun x => b) = b ↔ ∀ (h : P), A h = b
[PROOFSTEP]
by_cases P
[GOAL]
α : Sort u_2
β : Sort ?u.33174
σ : α → Sort u_1
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B : ¬P → α
⊢ (dite P A fun x => b) = b ↔ ∀ (h : P), A h = b
[PROOFSTEP]
by_cases P
[GOAL]
case pos
α : Sort u_2
β : Sort ?u.33174
σ : α → Sort u_1
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B : ¬P → α
h : P
⊢ (dite P A fun x => b) = b ↔ ∀ (h : P), A h = b
[PROOFSTEP]
simp [*, forall_prop_of_true, forall_prop_of_false]
[GOAL]
case neg
α : Sort u_2
β : Sort ?u.33174
σ : α → Sort u_1
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B : ¬P → α
h : ¬P
⊢ (dite P A fun x => b) = b ↔ ∀ (h : P), A h = b
[PROOFSTEP]
simp [*, forall_prop_of_true, forall_prop_of_false]
[GOAL]
α : Sort u_2
β : Sort ?u.33996
σ : α → Sort u_1
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B : ¬P → α
⊢ dite P (fun x => a) B ≠ a ↔ ∃ h, a ≠ B h
[PROOFSTEP]
rw [Ne.def, dite_eq_left_iff, not_forall]
[GOAL]
α : Sort u_2
β : Sort ?u.33996
σ : α → Sort u_1
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B : ¬P → α
⊢ (∃ x, ¬B x = a) ↔ ∃ h, a ≠ B h
[PROOFSTEP]
exact exists_congr fun h ↦ by rw [ne_comm]
[GOAL]
α : Sort u_2
β : Sort ?u.33996
σ : α → Sort u_1
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B : ¬P → α
h : ¬P
⊢ ¬B h = a ↔ a ≠ B h
[PROOFSTEP]
rw [ne_comm]
[GOAL]
α : Sort u_2
β : Sort ?u.34290
σ : α → Sort u_1
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B : ¬P → α
⊢ (dite P A fun x => b) ≠ b ↔ ∃ h, A h ≠ b
[PROOFSTEP]
simp only [Ne.def, dite_eq_right_iff, not_forall]
[GOAL]
α : Sort u_2
β : Sort ?u.34782
σ : α → Sort u_1
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B : ¬P → α
⊢ (∃ h, a ≠ (fun x => b) h) ↔ ¬P ∧ a ≠ b
[PROOFSTEP]
simp only
[GOAL]
α : Sort u_2
β : Sort ?u.34782
σ : α → Sort u_1
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B : ¬P → α
⊢ (∃ h, a ≠ b) ↔ ¬P ∧ a ≠ b
[PROOFSTEP]
rw [exists_prop]
[GOAL]
α : Sort u_2
β : Sort ?u.35052
σ : α → Sort u_1
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B : ¬P → α
⊢ (∃ h, (fun x => a) h ≠ b) ↔ P ∧ a ≠ b
[PROOFSTEP]
simp only
[GOAL]
α : Sort u_2
β : Sort ?u.35052
σ : α → Sort u_1
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B : ¬P → α
⊢ (∃ h, a ≠ b) ↔ P ∧ a ≠ b
[PROOFSTEP]
rw [exists_prop]
[GOAL]
α : Sort u_3
β : Sort u_4
σ : α → Sort u_1
f✝ : α → β
P✝ Q : Prop
inst✝² : Decidable P✝
inst✝¹ : Decidable Q
a✝ b✝ c✝ : α
A : P✝ → α
B : ¬P✝ → α
γ : Sort u_2
f : α → β → γ
P : Prop
inst✝ : Decidable P
a : P → α
b : ¬P → α
c : P → β
d : ¬P → β
⊢ f (dite P a b) (dite P c d) = if h : P then f (a h) (c h) else f (b h) (d h)
[PROOFSTEP]
by_cases h : P
[GOAL]
case pos
α : Sort u_3
β : Sort u_4
σ : α → Sort u_1
f✝ : α → β
P✝ Q : Prop
inst✝² : Decidable P✝
inst✝¹ : Decidable Q
a✝ b✝ c✝ : α
A : P✝ → α
B : ¬P✝ → α
γ : Sort u_2
f : α → β → γ
P : Prop
inst✝ : Decidable P
a : P → α
b : ¬P → α
c : P → β
d : ¬P → β
h : P
⊢ f (dite P a b) (dite P c d) = if h : P then f (a h) (c h) else f (b h) (d h)
[PROOFSTEP]
simp [h]
[GOAL]
case neg
α : Sort u_3
β : Sort u_4
σ : α → Sort u_1
f✝ : α → β
P✝ Q : Prop
inst✝² : Decidable P✝
inst✝¹ : Decidable Q
a✝ b✝ c✝ : α
A : P✝ → α
B : ¬P✝ → α
γ : Sort u_2
f : α → β → γ
P : Prop
inst✝ : Decidable P
a : P → α
b : ¬P → α
c : P → β
d : ¬P → β
h : ¬P
⊢ f (dite P a b) (dite P c d) = if h : P then f (a h) (c h) else f (b h) (d h)
[PROOFSTEP]
simp [h]
[GOAL]
α : Sort u_2
β : Sort ?u.37772
σ : α → Sort u_1
f✝ : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a✝ b c : α
A : P → α
B : ¬P → α
f : P → (a : α) → σ a
g : ¬P → (a : α) → σ a
a : α
⊢ dite P f g a = if h : P then f h a else g h a
[PROOFSTEP]
by_cases h : P
[GOAL]
case pos
α : Sort u_2
β : Sort ?u.37772
σ : α → Sort u_1
f✝ : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a✝ b c : α
A : P → α
B : ¬P → α
f : P → (a : α) → σ a
g : ¬P → (a : α) → σ a
a : α
h : P
⊢ dite P f g a = if h : P then f h a else g h a
[PROOFSTEP]
simp [h]
[GOAL]
case neg
α : Sort u_2
β : Sort ?u.37772
σ : α → Sort u_1
f✝ : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a✝ b c : α
A : P → α
B : ¬P → α
f : P → (a : α) → σ a
g : ¬P → (a : α) → σ a
a : α
h : ¬P
⊢ dite P f g a = if h : P then f h a else g h a
[PROOFSTEP]
simp [h]
[GOAL]
α : Sort u_2
β : Sort ?u.38314
σ : α → Sort u_1
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B : ¬P → α
⊢ (if P ∧ Q then a else b) = if P then if Q then a else b else b
[PROOFSTEP]
by_cases hp : P
[GOAL]
case pos
α : Sort u_2
β : Sort ?u.38314
σ : α → Sort u_1
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B : ¬P → α
hp : P
⊢ (if P ∧ Q then a else b) = if P then if Q then a else b else b
[PROOFSTEP]
by_cases hq : Q
[GOAL]
case neg
α : Sort u_2
β : Sort ?u.38314
σ : α → Sort u_1
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B : ¬P → α
hp : ¬P
⊢ (if P ∧ Q then a else b) = if P then if Q then a else b else b
[PROOFSTEP]
by_cases hq : Q
[GOAL]
case pos
α : Sort u_2
β : Sort ?u.38314
σ : α → Sort u_1
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B : ¬P → α
hp : P
hq : Q
⊢ (if P ∧ Q then a else b) = if P then if Q then a else b else b
[PROOFSTEP]
simp [hp, hq]
[GOAL]
case neg
α : Sort u_2
β : Sort ?u.38314
σ : α → Sort u_1
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B : ¬P → α
hp : P
hq : ¬Q
⊢ (if P ∧ Q then a else b) = if P then if Q then a else b else b
[PROOFSTEP]
simp [hp, hq]
[GOAL]
case pos
α : Sort u_2
β : Sort ?u.38314
σ : α → Sort u_1
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B : ¬P → α
hp : ¬P
hq : Q
⊢ (if P ∧ Q then a else b) = if P then if Q then a else b else b
[PROOFSTEP]
simp [hp, hq]
[GOAL]
case neg
α : Sort u_2
β : Sort ?u.38314
σ : α → Sort u_1
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B : ¬P → α
hp : ¬P
hq : ¬Q
⊢ (if P ∧ Q then a else b) = if P then if Q then a else b else b
[PROOFSTEP]
simp [hp, hq]
[GOAL]
α : Sort u_2
β : Sort ?u.39011
σ : α → Sort u_1
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B✝ : ¬P → α
B : Q → α
C : ¬P → ¬Q → α
h : P → ¬Q
p : P
⊢ A p = if q : Q then B q else if p : P then A p else C p q
[PROOFSTEP]
rw [dif_neg (h p), dif_pos p]
[GOAL]
α : Sort u_2
β : Sort ?u.39011
σ : α → Sort u_1
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B✝ : ¬P → α
B : Q → α
C : ¬P → ¬Q → α
h : P → ¬Q
np : ¬P
⊢ (if q : Q then B q else C np q) = if q : Q then B q else if p : P then A p else C p q
[PROOFSTEP]
congr
[GOAL]
case e_e
α : Sort u_2
β : Sort ?u.39011
σ : α → Sort u_1
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B✝ : ¬P → α
B : Q → α
C : ¬P → ¬Q → α
h : P → ¬Q
np : ¬P
⊢ (fun q => C np q) = fun q => if p : P then A p else C p q
[PROOFSTEP]
funext _
[GOAL]
case e_e.h
α : Sort u_2
β : Sort ?u.39011
σ : α → Sort u_1
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B✝ : ¬P → α
B : Q → α
C : ¬P → ¬Q → α
h : P → ¬Q
np : ¬P
x✝ : ¬Q
⊢ C np x✝ = if p : P then A p else C p x✝
[PROOFSTEP]
rw [dif_neg np]


[GOAL]
R : Type u
inst✝¹⁸ : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
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
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
inst✝⁵ : LieRingModule L P
inst✝⁴ : LieModule R L P
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
inst✝¹ : LieRingModule L Q
inst✝ : LieModule R L Q
x y : L
t : M ⊗[R] N
⊢ ⁅x + y, t⁆ = ⁅x, t⁆ + ⁅y, t⁆
[PROOFSTEP]
simp only [hasBracketAux, LinearMap.lTensor_add, LinearMap.rTensor_add, LieHom.map_add, LinearMap.add_apply]
[GOAL]
R : Type u
inst✝¹⁸ : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
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
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
inst✝⁵ : LieRingModule L P
inst✝⁴ : LieModule R L P
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
inst✝¹ : LieRingModule L Q
inst✝ : LieModule R L Q
x y : L
t : M ⊗[R] N
⊢ ↑(LinearMap.rTensor N (↑(toEndomorphism R L M) x)) t + ↑(LinearMap.rTensor N (↑(toEndomorphism R L M) y)) t +
      (↑(LinearMap.lTensor M (↑(toEndomorphism R L N) x)) t + ↑(LinearMap.lTensor M (↑(toEndomorphism R L N) y)) t) =
    ↑(LinearMap.rTensor N (↑(toEndomorphism R L M) x)) t + ↑(LinearMap.lTensor M (↑(toEndomorphism R L N) x)) t +
      (↑(LinearMap.rTensor N (↑(toEndomorphism R L M) y)) t + ↑(LinearMap.lTensor M (↑(toEndomorphism R L N) y)) t)
[PROOFSTEP]
abel
[GOAL]
R : Type u
inst✝¹⁸ : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
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
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
inst✝⁵ : LieRingModule L P
inst✝⁴ : LieModule R L P
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
inst✝¹ : LieRingModule L Q
inst✝ : LieModule R L Q
x y : L
t : M ⊗[R] N
⊢ ↑(LinearMap.rTensor N (↑(toEndomorphism R L M) x)) t + ↑(LinearMap.rTensor N (↑(toEndomorphism R L M) y)) t +
      (↑(LinearMap.lTensor M (↑(toEndomorphism R L N) x)) t + ↑(LinearMap.lTensor M (↑(toEndomorphism R L N) y)) t) =
    ↑(LinearMap.rTensor N (↑(toEndomorphism R L M) x)) t + ↑(LinearMap.lTensor M (↑(toEndomorphism R L N) x)) t +
      (↑(LinearMap.rTensor N (↑(toEndomorphism R L M) y)) t + ↑(LinearMap.lTensor M (↑(toEndomorphism R L N) y)) t)
[PROOFSTEP]
abel
[GOAL]
R : Type u
inst✝¹⁸ : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
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
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
inst✝⁵ : LieRingModule L P
inst✝⁴ : LieModule R L P
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
inst✝¹ : LieRingModule L Q
inst✝ : LieModule R L Q
x y : L
t : M ⊗[R] N
⊢ ⁅x, ⁅y, t⁆⁆ = ⁅⁅x, y⁆, t⁆ + ⁅y, ⁅x, t⁆⁆
[PROOFSTEP]
suffices (hasBracketAux x).comp (hasBracketAux y) = hasBracketAux ⁅x, y⁆ + (hasBracketAux y).comp (hasBracketAux x) by
  simp only [← LinearMap.add_apply]; rw [← LinearMap.comp_apply, this]; rfl
[GOAL]
R : Type u
inst✝¹⁸ : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
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
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
inst✝⁵ : LieRingModule L P
inst✝⁴ : LieModule R L P
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
inst✝¹ : LieRingModule L Q
inst✝ : LieModule R L Q
x y : L
t : M ⊗[R] N
this :
  LinearMap.comp (hasBracketAux x) (hasBracketAux y) =
    hasBracketAux ⁅x, y⁆ + LinearMap.comp (hasBracketAux y) (hasBracketAux x)
⊢ ⁅x, ⁅y, t⁆⁆ = ⁅⁅x, y⁆, t⁆ + ⁅y, ⁅x, t⁆⁆
[PROOFSTEP]
simp only [← LinearMap.add_apply]
[GOAL]
R : Type u
inst✝¹⁸ : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
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
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
inst✝⁵ : LieRingModule L P
inst✝⁴ : LieModule R L P
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
inst✝¹ : LieRingModule L Q
inst✝ : LieModule R L Q
x y : L
t : M ⊗[R] N
this :
  LinearMap.comp (hasBracketAux x) (hasBracketAux y) =
    hasBracketAux ⁅x, y⁆ + LinearMap.comp (hasBracketAux y) (hasBracketAux x)
⊢ ↑(hasBracketAux x) (↑(hasBracketAux y) t) = ↑(hasBracketAux ⁅x, y⁆) t + ↑(hasBracketAux y) (↑(hasBracketAux x) t)
[PROOFSTEP]
rw [← LinearMap.comp_apply, this]
[GOAL]
R : Type u
inst✝¹⁸ : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
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
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
inst✝⁵ : LieRingModule L P
inst✝⁴ : LieModule R L P
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
inst✝¹ : LieRingModule L Q
inst✝ : LieModule R L Q
x y : L
t : M ⊗[R] N
this :
  LinearMap.comp (hasBracketAux x) (hasBracketAux y) =
    hasBracketAux ⁅x, y⁆ + LinearMap.comp (hasBracketAux y) (hasBracketAux x)
⊢ ↑(hasBracketAux ⁅x, y⁆ + LinearMap.comp (hasBracketAux y) (hasBracketAux x)) t =
    ↑(hasBracketAux ⁅x, y⁆) t + ↑(hasBracketAux y) (↑(hasBracketAux x) t)
R : Type u
inst✝¹⁸ : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
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
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
inst✝⁵ : LieRingModule L P
inst✝⁴ : LieModule R L P
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
inst✝¹ : LieRingModule L Q
inst✝ : LieModule R L Q
x y : L
t : M ⊗[R] N
⊢ LieAlgebra R L
R : Type u
inst✝¹⁸ : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
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
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
inst✝⁵ : LieRingModule L P
inst✝⁴ : LieModule R L P
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
inst✝¹ : LieRingModule L Q
inst✝ : LieModule R L Q
x y : L
t : M ⊗[R] N
⊢ LieRingModule L M
R : Type u
inst✝¹⁸ : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
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
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
inst✝⁵ : LieRingModule L P
inst✝⁴ : LieModule R L P
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
inst✝¹ : LieRingModule L Q
inst✝ : LieModule R L Q
x y : L
t : M ⊗[R] N
⊢ LieModule R L M
R : Type u
inst✝¹⁸ : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
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
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
inst✝⁵ : LieRingModule L P
inst✝⁴ : LieModule R L P
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
inst✝¹ : LieRingModule L Q
inst✝ : LieModule R L Q
x y : L
t : M ⊗[R] N
⊢ LieRingModule L N
R : Type u
inst✝¹⁸ : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
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
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
inst✝⁵ : LieRingModule L P
inst✝⁴ : LieModule R L P
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
inst✝¹ : LieRingModule L Q
inst✝ : LieModule R L Q
x y : L
t : M ⊗[R] N
⊢ LieModule R L N
R : Type u
inst✝¹⁸ : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
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
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
inst✝⁵ : LieRingModule L P
inst✝⁴ : LieModule R L P
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
inst✝¹ : LieRingModule L Q
inst✝ : LieModule R L Q
x y : L
t : M ⊗[R] N
⊢ LieAlgebra R L
R : Type u
inst✝¹⁸ : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
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
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
inst✝⁵ : LieRingModule L P
inst✝⁴ : LieModule R L P
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
inst✝¹ : LieRingModule L Q
inst✝ : LieModule R L Q
x y : L
t : M ⊗[R] N
⊢ LieRingModule L M
R : Type u
inst✝¹⁸ : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
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
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
inst✝⁵ : LieRingModule L P
inst✝⁴ : LieModule R L P
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
inst✝¹ : LieRingModule L Q
inst✝ : LieModule R L Q
x y : L
t : M ⊗[R] N
⊢ LieModule R L M
R : Type u
inst✝¹⁸ : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
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
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
inst✝⁵ : LieRingModule L P
inst✝⁴ : LieModule R L P
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
inst✝¹ : LieRingModule L Q
inst✝ : LieModule R L Q
x y : L
t : M ⊗[R] N
⊢ LieRingModule L N
R : Type u
inst✝¹⁸ : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
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
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
inst✝⁵ : LieRingModule L P
inst✝⁴ : LieModule R L P
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
inst✝¹ : LieRingModule L Q
inst✝ : LieModule R L Q
x y : L
t : M ⊗[R] N
⊢ LieModule R L N
R : Type u
inst✝¹⁸ : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
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
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
inst✝⁵ : LieRingModule L P
inst✝⁴ : LieModule R L P
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
inst✝¹ : LieRingModule L Q
inst✝ : LieModule R L Q
x y : L
t : M ⊗[R] N
⊢ LieAlgebra R L
R : Type u
inst✝¹⁸ : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
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
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
inst✝⁵ : LieRingModule L P
inst✝⁴ : LieModule R L P
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
inst✝¹ : LieRingModule L Q
inst✝ : LieModule R L Q
x y : L
t : M ⊗[R] N
⊢ LieRingModule L M
R : Type u
inst✝¹⁸ : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
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
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
inst✝⁵ : LieRingModule L P
inst✝⁴ : LieModule R L P
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
inst✝¹ : LieRingModule L Q
inst✝ : LieModule R L Q
x y : L
t : M ⊗[R] N
⊢ LieModule R L M
R : Type u
inst✝¹⁸ : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
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
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
inst✝⁵ : LieRingModule L P
inst✝⁴ : LieModule R L P
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
inst✝¹ : LieRingModule L Q
inst✝ : LieModule R L Q
x y : L
t : M ⊗[R] N
⊢ LieRingModule L N
R : Type u
inst✝¹⁸ : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
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
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
inst✝⁵ : LieRingModule L P
inst✝⁴ : LieModule R L P
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
inst✝¹ : LieRingModule L Q
inst✝ : LieModule R L Q
x y : L
t : M ⊗[R] N
⊢ LieModule R L N
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝¹⁸ : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
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
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
inst✝⁵ : LieRingModule L P
inst✝⁴ : LieModule R L P
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
inst✝¹ : LieRingModule L Q
inst✝ : LieModule R L Q
x y : L
t : M ⊗[R] N
⊢ LinearMap.comp (hasBracketAux x) (hasBracketAux y) =
    hasBracketAux ⁅x, y⁆ + LinearMap.comp (hasBracketAux y) (hasBracketAux x)
[PROOFSTEP]
ext m n
[GOAL]
case H.h.h
R : Type u
inst✝¹⁸ : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
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
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
inst✝⁵ : LieRingModule L P
inst✝⁴ : LieModule R L P
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
inst✝¹ : LieRingModule L Q
inst✝ : LieModule R L Q
x y : L
t : M ⊗[R] N
m : M
n : N
⊢ ↑(↑(LinearMap.compr₂ (mk R M N) (LinearMap.comp (hasBracketAux x) (hasBracketAux y))) m) n =
    ↑(↑(LinearMap.compr₂ (mk R M N) (hasBracketAux ⁅x, y⁆ + LinearMap.comp (hasBracketAux y) (hasBracketAux x))) m) n
[PROOFSTEP]
simp only [hasBracketAux, LieRing.of_associative_ring_bracket, LinearMap.mul_apply, mk_apply, LinearMap.lTensor_sub,
  LinearMap.compr₂_apply, Function.comp_apply, LinearMap.coe_comp, LinearMap.rTensor_tmul, LieHom.map_lie,
  toEndomorphism_apply_apply, LinearMap.add_apply, LinearMap.map_add, LinearMap.rTensor_sub, LinearMap.sub_apply,
  LinearMap.lTensor_tmul]
[GOAL]
case H.h.h
R : Type u
inst✝¹⁸ : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
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
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
inst✝⁵ : LieRingModule L P
inst✝⁴ : LieModule R L P
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
inst✝¹ : LieRingModule L Q
inst✝ : LieModule R L Q
x y : L
t : M ⊗[R] N
m : M
n : N
⊢ ⁅x, ⁅y, m⁆⁆ ⊗ₜ[R] n + ⁅y, m⁆ ⊗ₜ[R] ⁅x, n⁆ + (⁅x, m⁆ ⊗ₜ[R] ⁅y, n⁆ + m ⊗ₜ[R] ⁅x, ⁅y, n⁆⁆) =
    ⁅x, ⁅y, m⁆⁆ ⊗ₜ[R] n - ⁅y, ⁅x, m⁆⁆ ⊗ₜ[R] n + (m ⊗ₜ[R] ⁅x, ⁅y, n⁆⁆ - m ⊗ₜ[R] ⁅y, ⁅x, n⁆⁆) +
      (⁅y, ⁅x, m⁆⁆ ⊗ₜ[R] n + ⁅x, m⁆ ⊗ₜ[R] ⁅y, n⁆ + (⁅y, m⁆ ⊗ₜ[R] ⁅x, n⁆ + m ⊗ₜ[R] ⁅y, ⁅x, n⁆⁆))
[PROOFSTEP]
abel
[GOAL]
case H.h.h
R : Type u
inst✝¹⁸ : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
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
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
inst✝⁵ : LieRingModule L P
inst✝⁴ : LieModule R L P
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
inst✝¹ : LieRingModule L Q
inst✝ : LieModule R L Q
x y : L
t : M ⊗[R] N
m : M
n : N
⊢ ⁅x, ⁅y, m⁆⁆ ⊗ₜ[R] n + ⁅y, m⁆ ⊗ₜ[R] ⁅x, n⁆ + (⁅x, m⁆ ⊗ₜ[R] ⁅y, n⁆ + m ⊗ₜ[R] ⁅x, ⁅y, n⁆⁆) =
    ⁅x, ⁅y, m⁆⁆ ⊗ₜ[R] n - ⁅y, ⁅x, m⁆⁆ ⊗ₜ[R] n + (m ⊗ₜ[R] ⁅x, ⁅y, n⁆⁆ - m ⊗ₜ[R] ⁅y, ⁅x, n⁆⁆) +
      (⁅y, ⁅x, m⁆⁆ ⊗ₜ[R] n + ⁅x, m⁆ ⊗ₜ[R] ⁅y, n⁆ + (⁅y, m⁆ ⊗ₜ[R] ⁅x, n⁆ + m ⊗ₜ[R] ⁅y, ⁅x, n⁆⁆))
[PROOFSTEP]
abel
[GOAL]
R : Type u
inst✝¹⁸ : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
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
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
inst✝⁵ : LieRingModule L P
inst✝⁴ : LieModule R L P
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
inst✝¹ : LieRingModule L Q
inst✝ : LieModule R L Q
c : R
x : L
t : M ⊗[R] N
⊢ ⁅c • x, t⁆ = c • ⁅x, t⁆
[PROOFSTEP]
change hasBracketAux (c • x) _ = c • hasBracketAux _ _
[GOAL]
R : Type u
inst✝¹⁸ : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
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
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
inst✝⁵ : LieRingModule L P
inst✝⁴ : LieModule R L P
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
inst✝¹ : LieRingModule L Q
inst✝ : LieModule R L Q
c : R
x : L
t : M ⊗[R] N
⊢ ↑(hasBracketAux (c • x)) t = c • ↑(hasBracketAux x) t
[PROOFSTEP]
simp only [hasBracketAux, smul_add, LinearMap.rTensor_smul, LinearMap.smul_apply, LinearMap.lTensor_smul,
  LieHom.map_smul, LinearMap.add_apply]
[GOAL]
R : Type u
inst✝¹⁸ : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
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
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
inst✝⁵ : LieRingModule L P
inst✝⁴ : LieModule R L P
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
inst✝¹ : LieRingModule L Q
inst✝ : LieModule R L Q
x : L
m : M
n : N
⊢ ↑(hasBracketAux x) (m ⊗ₜ[R] n) = ⁅x, m⁆ ⊗ₜ[R] n + m ⊗ₜ[R] ⁅x, n⁆
[PROOFSTEP]
simp only [hasBracketAux, LinearMap.rTensor_tmul, toEndomorphism_apply_apply, LinearMap.add_apply,
  LinearMap.lTensor_tmul]
[GOAL]
R : Type u
inst✝¹⁸ : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
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
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
inst✝⁵ : LieRingModule L P
inst✝⁴ : LieModule R L P
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
inst✝¹ : LieRingModule L Q
inst✝ : LieModule R L Q
src✝ : (M →ₗ[R] N →ₗ[R] P) ≃ₗ[R] M ⊗[R] N →ₗ[R] P := lift.equiv R M N P
x : L
f : M →ₗ[R] N →ₗ[R] P
⊢ AddHom.toFun src✝.toAddHom ⁅x, f⁆ = ⁅x, AddHom.toFun src✝.toAddHom f⁆
[PROOFSTEP]
ext m n
[GOAL]
case H.h.h
R : Type u
inst✝¹⁸ : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
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
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
inst✝⁵ : LieRingModule L P
inst✝⁴ : LieModule R L P
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
inst✝¹ : LieRingModule L Q
inst✝ : LieModule R L Q
src✝ : (M →ₗ[R] N →ₗ[R] P) ≃ₗ[R] M ⊗[R] N →ₗ[R] P := lift.equiv R M N P
x : L
f : M →ₗ[R] N →ₗ[R] P
m : M
n : N
⊢ ↑(↑(LinearMap.compr₂ (mk R M N) (AddHom.toFun src✝.toAddHom ⁅x, f⁆)) m) n =
    ↑(↑(LinearMap.compr₂ (mk R M N) ⁅x, AddHom.toFun src✝.toAddHom f⁆) m) n
[PROOFSTEP]
simp only [mk_apply, LinearMap.compr₂_apply, lie_tmul_right, LinearMap.sub_apply, lift.equiv_apply,
  LinearEquiv.toFun_eq_coe, LieHom.lie_apply, LinearMap.map_add]
[GOAL]
case H.h.h
R : Type u
inst✝¹⁸ : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
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
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
inst✝⁵ : LieRingModule L P
inst✝⁴ : LieModule R L P
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
inst✝¹ : LieRingModule L Q
inst✝ : LieModule R L Q
src✝ : (M →ₗ[R] N →ₗ[R] P) ≃ₗ[R] M ⊗[R] N →ₗ[R] P := lift.equiv R M N P
x : L
f : M →ₗ[R] N →ₗ[R] P
m : M
n : N
⊢ ⁅x, ↑(↑f m) n⁆ - ↑(↑f m) ⁅x, n⁆ - ↑(↑f ⁅x, m⁆) n = ⁅x, ↑(↑f m) n⁆ - (↑(↑f ⁅x, m⁆) n + ↑(↑f m) ⁅x, n⁆)
[PROOFSTEP]
abel
[GOAL]
case H.h.h
R : Type u
inst✝¹⁸ : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
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
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
inst✝⁵ : LieRingModule L P
inst✝⁴ : LieModule R L P
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
inst✝¹ : LieRingModule L Q
inst✝ : LieModule R L Q
src✝ : (M →ₗ[R] N →ₗ[R] P) ≃ₗ[R] M ⊗[R] N →ₗ[R] P := lift.equiv R M N P
x : L
f : M →ₗ[R] N →ₗ[R] P
m : M
n : N
⊢ ⁅x, ↑(↑f m) n⁆ - ↑(↑f m) ⁅x, n⁆ - ↑(↑f ⁅x, m⁆) n = ⁅x, ↑(↑f m) n⁆ - (↑(↑f ⁅x, m⁆) n + ↑(↑f m) ⁅x, n⁆)
[PROOFSTEP]
abel
[GOAL]
R : Type u
inst✝¹⁸ : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
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
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
inst✝⁵ : LieRingModule L P
inst✝⁴ : LieModule R L P
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
inst✝¹ : LieRingModule L Q
inst✝ : LieModule R L Q
f : M →ₗ⁅R,L⁆ N →ₗ[R] P
⊢ ↑(↑(liftLie R L M N P) f) = ↑(↑(lift R L M N P) ↑f)
[PROOFSTEP]
suffices (liftLie R L M N P f : M ⊗[R] N →ₗ[R] P) = lift R L M N P f by rw [← this, LieModuleHom.coe_toLinearMap]
[GOAL]
R : Type u
inst✝¹⁸ : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
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
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
inst✝⁵ : LieRingModule L P
inst✝⁴ : LieModule R L P
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
inst✝¹ : LieRingModule L Q
inst✝ : LieModule R L Q
f : M →ₗ⁅R,L⁆ N →ₗ[R] P
this : ↑(↑(liftLie R L M N P) f) = ↑(lift R L M N P) ↑f
⊢ ↑(↑(liftLie R L M N P) f) = ↑(↑(lift R L M N P) ↑f)
[PROOFSTEP]
rw [← this, LieModuleHom.coe_toLinearMap]
[GOAL]
R : Type u
inst✝¹⁸ : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
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
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
inst✝⁵ : LieRingModule L P
inst✝⁴ : LieModule R L P
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
inst✝¹ : LieRingModule L Q
inst✝ : LieModule R L Q
f : M →ₗ⁅R,L⁆ N →ₗ[R] P
⊢ ↑(↑(liftLie R L M N P) f) = ↑(lift R L M N P) ↑f
[PROOFSTEP]
ext m n
[GOAL]
case H.h.h
R : Type u
inst✝¹⁸ : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
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
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
inst✝⁵ : LieRingModule L P
inst✝⁴ : LieModule R L P
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
inst✝¹ : LieRingModule L Q
inst✝ : LieModule R L Q
f : M →ₗ⁅R,L⁆ N →ₗ[R] P
m : M
n : N
⊢ ↑(↑(LinearMap.compr₂ (mk R M N) ↑(↑(liftLie R L M N P) f)) m) n =
    ↑(↑(LinearMap.compr₂ (mk R M N) (↑(lift R L M N P) ↑f)) m) n
[PROOFSTEP]
simp only [liftLie, LinearEquiv.trans_apply, LieModuleEquiv.coe_to_linearEquiv,
  coe_linearMap_maxTrivLinearMapEquivLieModuleHom, coe_maxTrivEquiv_apply,
  coe_linearMap_maxTrivLinearMapEquivLieModuleHom_symm]
[GOAL]
R : Type u
inst✝¹⁸ : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
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
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
inst✝⁵ : LieRingModule L P
inst✝⁴ : LieModule R L P
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
inst✝¹ : LieRingModule L Q
inst✝ : LieModule R L Q
f : M →ₗ⁅R,L⁆ N →ₗ[R] P
m : M
n : N
⊢ ↑(↑(liftLie R L M N P) f) (m ⊗ₜ[R] n) = ↑(↑f m) n
[PROOFSTEP]
simp only [coe_liftLie_eq_lift_coe, LieModuleHom.coe_toLinearMap, lift_apply]
[GOAL]
R : Type u
inst✝¹⁸ : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
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
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
inst✝⁵ : LieRingModule L P
inst✝⁴ : LieModule R L P
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
inst✝¹ : LieRingModule L Q
inst✝ : LieModule R L Q
f : M →ₗ⁅R,L⁆ P
g : N →ₗ⁅R,L⁆ Q
src✝ : M ⊗[R] N →ₗ[R] P ⊗[R] Q := TensorProduct.map ↑f ↑g
x : L
t : M ⊗[R] N
⊢ AddHom.toFun
      { toAddHom := src✝.toAddHom,
          map_smul' :=
            (_ :
              ∀ (r : R) (x : M ⊗[R] N),
                AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
      ⁅x, t⁆ =
    ⁅x,
      AddHom.toFun
        { toAddHom := src✝.toAddHom,
            map_smul' :=
              (_ :
                ∀ (r : R) (x : M ⊗[R] N),
                  AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
        t⁆
[PROOFSTEP]
simp only [LinearMap.toFun_eq_coe]
[GOAL]
R : Type u
inst✝¹⁸ : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
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
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
inst✝⁵ : LieRingModule L P
inst✝⁴ : LieModule R L P
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
inst✝¹ : LieRingModule L Q
inst✝ : LieModule R L Q
f : M →ₗ⁅R,L⁆ P
g : N →ₗ⁅R,L⁆ Q
src✝ : M ⊗[R] N →ₗ[R] P ⊗[R] Q := TensorProduct.map ↑f ↑g
x : L
t : M ⊗[R] N
⊢ ↑(TensorProduct.map ↑f ↑g) ⁅x, t⁆ = ⁅x, ↑(TensorProduct.map ↑f ↑g) t⁆
[PROOFSTEP]
refine' t.induction_on _ _ _
[GOAL]
case refine'_1
R : Type u
inst✝¹⁸ : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
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
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
inst✝⁵ : LieRingModule L P
inst✝⁴ : LieModule R L P
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
inst✝¹ : LieRingModule L Q
inst✝ : LieModule R L Q
f : M →ₗ⁅R,L⁆ P
g : N →ₗ⁅R,L⁆ Q
src✝ : M ⊗[R] N →ₗ[R] P ⊗[R] Q := TensorProduct.map ↑f ↑g
x : L
t : M ⊗[R] N
⊢ ↑(TensorProduct.map ↑f ↑g) ⁅x, 0⁆ = ⁅x, ↑(TensorProduct.map ↑f ↑g) 0⁆
[PROOFSTEP]
simp only [LinearMap.map_zero, lie_zero]
[GOAL]
case refine'_2
R : Type u
inst✝¹⁸ : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
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
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
inst✝⁵ : LieRingModule L P
inst✝⁴ : LieModule R L P
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
inst✝¹ : LieRingModule L Q
inst✝ : LieModule R L Q
f : M →ₗ⁅R,L⁆ P
g : N →ₗ⁅R,L⁆ Q
src✝ : M ⊗[R] N →ₗ[R] P ⊗[R] Q := TensorProduct.map ↑f ↑g
x : L
t : M ⊗[R] N
⊢ ∀ (x_1 : M) (y : N), ↑(TensorProduct.map ↑f ↑g) ⁅x, x_1 ⊗ₜ[R] y⁆ = ⁅x, ↑(TensorProduct.map ↑f ↑g) (x_1 ⊗ₜ[R] y)⁆
[PROOFSTEP]
intro m n
[GOAL]
case refine'_2
R : Type u
inst✝¹⁸ : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
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
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
inst✝⁵ : LieRingModule L P
inst✝⁴ : LieModule R L P
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
inst✝¹ : LieRingModule L Q
inst✝ : LieModule R L Q
f : M →ₗ⁅R,L⁆ P
g : N →ₗ⁅R,L⁆ Q
src✝ : M ⊗[R] N →ₗ[R] P ⊗[R] Q := TensorProduct.map ↑f ↑g
x : L
t : M ⊗[R] N
m : M
n : N
⊢ ↑(TensorProduct.map ↑f ↑g) ⁅x, m ⊗ₜ[R] n⁆ = ⁅x, ↑(TensorProduct.map ↑f ↑g) (m ⊗ₜ[R] n)⁆
[PROOFSTEP]
simp only [LieModuleHom.coe_toLinearMap, lie_tmul_right, LieModuleHom.map_lie, map_tmul, LinearMap.map_add]
[GOAL]
case refine'_3
R : Type u
inst✝¹⁸ : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
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
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
inst✝⁵ : LieRingModule L P
inst✝⁴ : LieModule R L P
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
inst✝¹ : LieRingModule L Q
inst✝ : LieModule R L Q
f : M →ₗ⁅R,L⁆ P
g : N →ₗ⁅R,L⁆ Q
src✝ : M ⊗[R] N →ₗ[R] P ⊗[R] Q := TensorProduct.map ↑f ↑g
x : L
t : M ⊗[R] N
⊢ ∀ (x_1 y : M ⊗[R] N),
    ↑(TensorProduct.map ↑f ↑g) ⁅x, x_1⁆ = ⁅x, ↑(TensorProduct.map ↑f ↑g) x_1⁆ →
      ↑(TensorProduct.map ↑f ↑g) ⁅x, y⁆ = ⁅x, ↑(TensorProduct.map ↑f ↑g) y⁆ →
        ↑(TensorProduct.map ↑f ↑g) ⁅x, x_1 + y⁆ = ⁅x, ↑(TensorProduct.map ↑f ↑g) (x_1 + y)⁆
[PROOFSTEP]
intro t₁ t₂ ht₁ ht₂
[GOAL]
case refine'_3
R : Type u
inst✝¹⁸ : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
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
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
inst✝⁵ : LieRingModule L P
inst✝⁴ : LieModule R L P
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
inst✝¹ : LieRingModule L Q
inst✝ : LieModule R L Q
f : M →ₗ⁅R,L⁆ P
g : N →ₗ⁅R,L⁆ Q
src✝ : M ⊗[R] N →ₗ[R] P ⊗[R] Q := TensorProduct.map ↑f ↑g
x : L
t t₁ t₂ : M ⊗[R] N
ht₁ : ↑(TensorProduct.map ↑f ↑g) ⁅x, t₁⁆ = ⁅x, ↑(TensorProduct.map ↑f ↑g) t₁⁆
ht₂ : ↑(TensorProduct.map ↑f ↑g) ⁅x, t₂⁆ = ⁅x, ↑(TensorProduct.map ↑f ↑g) t₂⁆
⊢ ↑(TensorProduct.map ↑f ↑g) ⁅x, t₁ + t₂⁆ = ⁅x, ↑(TensorProduct.map ↑f ↑g) (t₁ + t₂)⁆
[PROOFSTEP]
simp only [ht₁, ht₂, lie_add, LinearMap.map_add]
[GOAL]
R : Type u
inst✝⁶ : CommRing R
L : Type v
M : Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
src✝ : L →ₗ[R] Module.End R M := ↑(toEndomorphism R L M)
x m : L
⊢ AddHom.toFun
      { toAddHom := src✝.toAddHom,
          map_smul' :=
            (_ :
              ∀ (r : R) (x : L),
                AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
      ⁅x, m⁆ =
    ⁅x,
      AddHom.toFun
        { toAddHom := src✝.toAddHom,
            map_smul' :=
              (_ :
                ∀ (r : R) (x : L),
                  AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
        m⁆
[PROOFSTEP]
ext n
[GOAL]
case h
R : Type u
inst✝⁶ : CommRing R
L : Type v
M : Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
src✝ : L →ₗ[R] Module.End R M := ↑(toEndomorphism R L M)
x m : L
n : M
⊢ ↑(AddHom.toFun
          { toAddHom := src✝.toAddHom,
              map_smul' :=
                (_ :
                  ∀ (r : R) (x : L),
                    AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
          ⁅x, m⁆)
      n =
    ↑⁅x,
          AddHom.toFun
            { toAddHom := src✝.toAddHom,
                map_smul' :=
                  (_ :
                    ∀ (r : R) (x : L),
                      AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
            m⁆
      n
[PROOFSTEP]
simp [LieRing.of_associative_ring_bracket]
[GOAL]
R : Type u
inst✝⁶ : CommRing R
L : Type v
M : Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x : L
m : M
⊢ ↑(toModuleHom R L M) (x ⊗ₜ[R] m) = ⁅x, m⁆
[PROOFSTEP]
simp only [toModuleHom, TensorProduct.LieModule.liftLie_apply, LieModuleHom.coe_mk, LinearMap.coe_mk,
  LinearMap.coe_toAddHom, LieHom.coe_toLinearMap, toEndomorphism_apply_apply]
[GOAL]
R : Type u
inst✝⁶ : CommRing R
L : Type v
M : Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
N : LieSubmodule R L M
⊢ ⁅I, N⁆ = LieModuleHom.range (LieModuleHom.comp (toModuleHom R L M) (mapIncl I N))
[PROOFSTEP]
rw [← coe_toSubmodule_eq_iff, lieIdeal_oper_eq_linear_span, LieModuleHom.coeSubmodule_range,
  LieModuleHom.coe_linearMap_comp, LinearMap.range_comp, mapIncl_def, coe_linearMap_map,
  TensorProduct.map_range_eq_span_tmul, Submodule.map_span]
[GOAL]
R : Type u
inst✝⁶ : CommRing R
L : Type v
M : Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
N : LieSubmodule R L M
⊢ Submodule.span R {m | ∃ x n, ⁅↑x, ↑n⁆ = m} =
    Submodule.span R (↑↑(toModuleHom R L M) '' {t | ∃ m n, ↑↑(incl I) m ⊗ₜ[R] ↑↑(incl N) n = t})
[PROOFSTEP]
congr
[GOAL]
case e_s
R : Type u
inst✝⁶ : CommRing R
L : Type v
M : Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
N : LieSubmodule R L M
⊢ {m | ∃ x n, ⁅↑x, ↑n⁆ = m} = ↑↑(toModuleHom R L M) '' {t | ∃ m n, ↑↑(incl I) m ⊗ₜ[R] ↑↑(incl N) n = t}
[PROOFSTEP]
ext m
[GOAL]
case e_s.h
R : Type u
inst✝⁶ : CommRing R
L : Type v
M : Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
N : LieSubmodule R L M
m : M
⊢ m ∈ {m | ∃ x n, ⁅↑x, ↑n⁆ = m} ↔ m ∈ ↑↑(toModuleHom R L M) '' {t | ∃ m n, ↑↑(incl I) m ⊗ₜ[R] ↑↑(incl N) n = t}
[PROOFSTEP]
constructor
[GOAL]
case e_s.h.mp
R : Type u
inst✝⁶ : CommRing R
L : Type v
M : Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
N : LieSubmodule R L M
m : M
⊢ m ∈ {m | ∃ x n, ⁅↑x, ↑n⁆ = m} → m ∈ ↑↑(toModuleHom R L M) '' {t | ∃ m n, ↑↑(incl I) m ⊗ₜ[R] ↑↑(incl N) n = t}
[PROOFSTEP]
rintro ⟨⟨x, hx⟩, ⟨n, hn⟩, rfl⟩
[GOAL]
case e_s.h.mp.intro.mk.intro.mk
R : Type u
inst✝⁶ : CommRing R
L : Type v
M : Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
N : LieSubmodule R L M
x : L
hx : x ∈ I
n : M
hn : n ∈ N
⊢ ⁅↑{ val := x, property := hx }, ↑{ val := n, property := hn }⁆ ∈
    ↑↑(toModuleHom R L M) '' {t | ∃ m n, ↑↑(incl I) m ⊗ₜ[R] ↑↑(incl N) n = t}
[PROOFSTEP]
use x ⊗ₜ n
[GOAL]
case h
R : Type u
inst✝⁶ : CommRing R
L : Type v
M : Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
N : LieSubmodule R L M
x : L
hx : x ∈ I
n : M
hn : n ∈ N
⊢ x ⊗ₜ[R] n ∈ {t | ∃ m n, ↑↑(incl I) m ⊗ₜ[R] ↑↑(incl N) n = t} ∧
    ↑↑(toModuleHom R L M) (x ⊗ₜ[R] n) = ⁅↑{ val := x, property := hx }, ↑{ val := n, property := hn }⁆
[PROOFSTEP]
constructor
[GOAL]
case h.left
R : Type u
inst✝⁶ : CommRing R
L : Type v
M : Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
N : LieSubmodule R L M
x : L
hx : x ∈ I
n : M
hn : n ∈ N
⊢ x ⊗ₜ[R] n ∈ {t | ∃ m n, ↑↑(incl I) m ⊗ₜ[R] ↑↑(incl N) n = t}
[PROOFSTEP]
use⟨x, hx⟩, ⟨n, hn⟩
[GOAL]
case h
R : Type u
inst✝⁶ : CommRing R
L : Type v
M : Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
N : LieSubmodule R L M
x : L
hx : x ∈ I
n : M
hn : n ∈ N
⊢ ↑↑(incl I) { val := x, property := hx } ⊗ₜ[R] ↑↑(incl N) { val := n, property := hn } = x ⊗ₜ[R] n
[PROOFSTEP]
simp
[GOAL]
case h.right
R : Type u
inst✝⁶ : CommRing R
L : Type v
M : Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
N : LieSubmodule R L M
x : L
hx : x ∈ I
n : M
hn : n ∈ N
⊢ ↑↑(toModuleHom R L M) (x ⊗ₜ[R] n) = ⁅↑{ val := x, property := hx }, ↑{ val := n, property := hn }⁆
[PROOFSTEP]
simp
[GOAL]
case e_s.h.mpr
R : Type u
inst✝⁶ : CommRing R
L : Type v
M : Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
N : LieSubmodule R L M
m : M
⊢ m ∈ ↑↑(toModuleHom R L M) '' {t | ∃ m n, ↑↑(incl I) m ⊗ₜ[R] ↑↑(incl N) n = t} → m ∈ {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
[PROOFSTEP]
rintro ⟨t, ⟨⟨x, hx⟩, ⟨n, hn⟩, rfl⟩, h⟩
[GOAL]
case e_s.h.mpr.intro.intro.intro.mk.intro.mk
R : Type u
inst✝⁶ : CommRing R
L : Type v
M : Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
N : LieSubmodule R L M
m : M
x : L
hx : x ∈ ↑I
n : M
hn : n ∈ ↑N
h : ↑↑(toModuleHom R L M) (↑↑(incl I) { val := x, property := hx } ⊗ₜ[R] ↑↑(incl N) { val := n, property := hn }) = m
⊢ m ∈ {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
[PROOFSTEP]
rw [← h]
[GOAL]
case e_s.h.mpr.intro.intro.intro.mk.intro.mk
R : Type u
inst✝⁶ : CommRing R
L : Type v
M : Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
N : LieSubmodule R L M
m : M
x : L
hx : x ∈ ↑I
n : M
hn : n ∈ ↑N
h : ↑↑(toModuleHom R L M) (↑↑(incl I) { val := x, property := hx } ⊗ₜ[R] ↑↑(incl N) { val := n, property := hn }) = m
⊢ ↑↑(toModuleHom R L M) (↑↑(incl I) { val := x, property := hx } ⊗ₜ[R] ↑↑(incl N) { val := n, property := hn }) ∈
    {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
[PROOFSTEP]
use⟨x, hx⟩, ⟨n, hn⟩
[GOAL]
case h
R : Type u
inst✝⁶ : CommRing R
L : Type v
M : Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
N : LieSubmodule R L M
m : M
x : L
hx : x ∈ ↑I
n : M
hn : n ∈ ↑N
h : ↑↑(toModuleHom R L M) (↑↑(incl I) { val := x, property := hx } ⊗ₜ[R] ↑↑(incl N) { val := n, property := hn }) = m
⊢ ⁅↑{ val := x, property := hx }, ↑{ val := n, property := hn }⁆ =
    ↑↑(toModuleHom R L M) (↑↑(incl I) { val := x, property := hx } ⊗ₜ[R] ↑↑(incl N) { val := n, property := hn })
[PROOFSTEP]
simp


[GOAL]
α : Type u
β : Type v
f : α → α
n✝ n : ℕ
ihn : id^[n] = id
⊢ id^[Nat.succ n] = id
[PROOFSTEP]
rw [iterate_succ, ihn, comp.left_id]
[GOAL]
α : Type u
β : Type v
f : α → α
m n : ℕ
⊢ f^[m + Nat.succ n] = f^[m] ∘ f^[Nat.succ n]
[PROOFSTEP]
rw [Nat.add_succ, iterate_succ, iterate_succ, iterate_add m n]
[GOAL]
α : Type u
β : Type v
f : α → α
m n : ℕ
⊢ (f^[m] ∘ f^[n]) ∘ f = f^[m] ∘ f^[n] ∘ f
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
f : α → α
m n : ℕ
x : α
⊢ f^[m + n] x = f^[m] (f^[n] x)
[PROOFSTEP]
rw [iterate_add f m n]
[GOAL]
α : Type u
β : Type v
f : α → α
m n : ℕ
x : α
⊢ (f^[m] ∘ f^[n]) x = f^[m] (f^[n] x)
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
f : α → α
m : ℕ
⊢ f^[m * 0] = f^[m]^[0]
[PROOFSTEP]
simp only [Nat.mul_zero, iterate_zero]
[GOAL]
α : Type u
β : Type v
f : α → α
m n : ℕ
⊢ f^[m * (n + 1)] = f^[m]^[n + 1]
[PROOFSTEP]
simp only [Nat.mul_succ, Nat.mul_one, iterate_one, iterate_add, iterate_mul m n]
[GOAL]
α : Type u
β : Type v
f : α → α
x : α
h : f x = x
n✝ n : ℕ
ihn : f^[n] x = x
⊢ f^[Nat.succ n] x = x
[PROOFSTEP]
rw [iterate_succ_apply, h, ihn]
[GOAL]
α : Type u
β : Type v
f : α → α
g : ℕ → α → α
H : ∀ (n : ℕ), Semiconj f (g n) (g (n + 1))
n k : ℕ
⊢ Semiconj f^[n] (g k) (g (n + k))
[PROOFSTEP]
induction' n with n ihn generalizing k
[GOAL]
case zero
α : Type u
β : Type v
f : α → α
g : ℕ → α → α
H : ∀ (n : ℕ), Semiconj f (g n) (g (n + 1))
k✝ k : ℕ
⊢ Semiconj f^[Nat.zero] (g k) (g (Nat.zero + k))
[PROOFSTEP]
rw [Nat.zero_add]
[GOAL]
case zero
α : Type u
β : Type v
f : α → α
g : ℕ → α → α
H : ∀ (n : ℕ), Semiconj f (g n) (g (n + 1))
k✝ k : ℕ
⊢ Semiconj f^[Nat.zero] (g k) (g k)
[PROOFSTEP]
exact id_left
[GOAL]
case succ
α : Type u
β : Type v
f : α → α
g : ℕ → α → α
H : ∀ (n : ℕ), Semiconj f (g n) (g (n + 1))
k✝ n : ℕ
ihn : ∀ (k : ℕ), Semiconj f^[n] (g k) (g (n + k))
k : ℕ
⊢ Semiconj f^[Nat.succ n] (g k) (g (Nat.succ n + k))
[PROOFSTEP]
rw [Nat.succ_eq_add_one, Nat.add_right_comm, Nat.add_assoc]
[GOAL]
case succ
α : Type u
β : Type v
f : α → α
g : ℕ → α → α
H : ∀ (n : ℕ), Semiconj f (g n) (g (n + 1))
k✝ n : ℕ
ihn : ∀ (k : ℕ), Semiconj f^[n] (g k) (g (n + k))
k : ℕ
⊢ Semiconj f^[n + 1] (g k) (g (n + (k + 1)))
[PROOFSTEP]
exact (H k).comp_left (ihn (k + 1))
[GOAL]
α : Type u
β : Type v
f g : α → α
h : Commute f g
n✝ : ℕ
x : α
hx : f x = g x
n : ℕ
ihn : f^[n] x = g^[n] x
⊢ f^[Nat.succ n] x = g^[Nat.succ n] x
[PROOFSTEP]
simp only [iterate_succ_apply, hx, (h.iterate_left n).eq, ihn, ((refl g).iterate_right n).eq]
[GOAL]
α : Type u
β : Type v
f g : α → α
h : Commute f g
n : ℕ
⊢ (f ∘ g)^[n] = f^[n] ∘ g^[n]
[PROOFSTEP]
induction' n with n ihn
[GOAL]
case zero
α : Type u
β : Type v
f g : α → α
h : Commute f g
⊢ (f ∘ g)^[Nat.zero] = f^[Nat.zero] ∘ g^[Nat.zero]
[PROOFSTEP]
rfl
[GOAL]
case succ
α : Type u
β : Type v
f g : α → α
h : Commute f g
n : ℕ
ihn : (f ∘ g)^[n] = f^[n] ∘ g^[n]
⊢ (f ∘ g)^[Nat.succ n] = f^[Nat.succ n] ∘ g^[Nat.succ n]
[PROOFSTEP]
funext x
[GOAL]
case succ.h
α : Type u
β : Type v
f g : α → α
h : Commute f g
n : ℕ
ihn : (f ∘ g)^[n] = f^[n] ∘ g^[n]
x : α
⊢ (f ∘ g)^[Nat.succ n] x = (f^[Nat.succ n] ∘ g^[Nat.succ n]) x
[PROOFSTEP]
simp only [ihn, (h.iterate_right n).eq, iterate_succ, comp_apply]
[GOAL]
α : Type u
β : Type v
f : α → α
n : ℕ
⊢ f^[Nat.succ n] = f ∘ f^[n]
[PROOFSTEP]
rw [iterate_succ, (Commute.self_iterate f n).comp_eq]
[GOAL]
α : Type u
β : Type v
f : α → α
n : ℕ
x : α
⊢ f^[Nat.succ n] x = f (f^[n] x)
[PROOFSTEP]
rw [iterate_succ']
[GOAL]
α : Type u
β : Type v
f : α → α
n : ℕ
x : α
⊢ (f ∘ f^[n]) x = f (f^[n] x)
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
f : α → α
n : ℕ
hn : 0 < n
⊢ f^[Nat.pred n] ∘ f = f^[n]
[PROOFSTEP]
rw [← iterate_succ, Nat.succ_pred_eq_of_pos hn]
[GOAL]
α : Type u
β : Type v
f : α → α
n : ℕ
hn : 0 < n
⊢ f ∘ f^[Nat.pred n] = f^[n]
[PROOFSTEP]
rw [← iterate_succ', Nat.succ_pred_eq_of_pos hn]
[GOAL]
α : Type u
β : Type v
f : α → α
m n✝¹ : ℕ
a : α
g : α → α
hg : LeftInverse g f
n✝ n : ℕ
ihn : LeftInverse g^[n] f^[n]
⊢ LeftInverse g^[Nat.succ n] f^[Nat.succ n]
[PROOFSTEP]
rw [iterate_succ', iterate_succ]
[GOAL]
α : Type u
β : Type v
f : α → α
m n✝¹ : ℕ
a : α
g : α → α
hg : LeftInverse g f
n✝ n : ℕ
ihn : LeftInverse g^[n] f^[n]
⊢ LeftInverse (g ∘ g^[n]) (f^[n] ∘ f)
[PROOFSTEP]
exact ihn.comp hg
[GOAL]
α : Type u
β : Type v
f✝ : α → α
m✝ n✝ : ℕ
a : α
f : α → α
m n : ℕ
⊢ f^[n * m] = f^[m * n]
[PROOFSTEP]
rw [Nat.mul_comm]
[GOAL]
α : Type u
β : Type v
f : α → α
m n : ℕ
a : α
hf : Injective f
⊢ f^[m + n] a = f^[n] a ↔ f^[n] (f^[m] a) = f^[n] a
[PROOFSTEP]
rw [← iterate_add_apply, Nat.add_comm]
[GOAL]
α : Type u
β : Type v
f : α → α
m n : ℕ
a : α
hf : Injective f
ha : f^[m] a = f^[n] a
⊢ f^[m - n] a = a
[PROOFSTEP]
obtain h | h := le_total m n
[GOAL]
case inl
α : Type u
β : Type v
f : α → α
m n : ℕ
a : α
hf : Injective f
ha : f^[m] a = f^[n] a
h : m ≤ n
⊢ f^[m - n] a = a
case inr
α : Type u
β : Type v
f : α → α
m n : ℕ
a : α
hf : Injective f
ha : f^[m] a = f^[n] a
h : n ≤ m
⊢ f^[m - n] a = a
[PROOFSTEP]
{simp [Nat.sub_eq_zero_of_le h]
}
[GOAL]
case inl
α : Type u
β : Type v
f : α → α
m n : ℕ
a : α
hf : Injective f
ha : f^[m] a = f^[n] a
h : m ≤ n
⊢ f^[m - n] a = a
[PROOFSTEP]
simp [Nat.sub_eq_zero_of_le h]
[GOAL]
case inr
α : Type u
β : Type v
f : α → α
m n : ℕ
a : α
hf : Injective f
ha : f^[m] a = f^[n] a
h : n ≤ m
⊢ f^[m - n] a = a
[PROOFSTEP]
{exact iterate_cancel_of_add hf (by rwa [Nat.sub_add_cancel h])
}
[GOAL]
case inr
α : Type u
β : Type v
f : α → α
m n : ℕ
a : α
hf : Injective f
ha : f^[m] a = f^[n] a
h : n ≤ m
⊢ f^[m - n] a = a
[PROOFSTEP]
exact iterate_cancel_of_add hf (by rwa [Nat.sub_add_cancel h])
[GOAL]
α : Type u
β : Type v
f : α → α
m n : ℕ
a : α
hf : Injective f
ha : f^[m] a = f^[n] a
h : n ≤ m
⊢ f^[m - n + ?m.6123] a = f^[?m.6123] a
[PROOFSTEP]
rwa [Nat.sub_add_cancel h]
[GOAL]
α : Type u
β : Type v
f : α → α
a : α
l : List β
⊢ foldl (fun b x => f b) a l = f^[length l] a
[PROOFSTEP]
induction' l with b l H generalizing a
[GOAL]
case nil
α : Type u
β : Type v
f : α → α
a✝ a : α
⊢ foldl (fun b x => f b) a [] = f^[length []] a
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u
β : Type v
f : α → α
a✝ : α
b : β
l : List β
H : ∀ (a : α), foldl (fun b x => f b) a l = f^[length l] a
a : α
⊢ foldl (fun b x => f b) a (b :: l) = f^[length (b :: l)] a
[PROOFSTEP]
rw [length_cons, foldl, iterate_succ_apply, H]
[GOAL]
α : Type u
β : Type v
f : β → β
b : β
a : α
l : List α
⊢ foldr (fun x => f) b (a :: l) = f^[length (a :: l)] b
[PROOFSTEP]
rw [length_cons, foldr, foldr_const f b l, iterate_succ_apply']


[GOAL]
α : Type v
inst✝ : Small.{w, v} α
x y : Shrink α
w : ↑(equivShrink α).symm x = ↑(equivShrink α).symm y
⊢ x = y
[PROOFSTEP]
simpa using w
[GOAL]
α : Type v
inst✝ : Subsingleton α
⊢ Small.{w, v} α
[PROOFSTEP]
rcases isEmpty_or_nonempty α with ⟨⟩
[GOAL]
case inl
α : Type v
inst✝ : Subsingleton α
h✝ : IsEmpty α
⊢ Small.{w, v} α
[PROOFSTEP]
skip
[GOAL]
case inr
α : Type v
inst✝ : Subsingleton α
h✝ : Nonempty α
⊢ Small.{w, v} α
[PROOFSTEP]
skip
[GOAL]
case inl
α : Type v
inst✝ : Subsingleton α
h✝ : IsEmpty α
⊢ Small.{w, v} α
[PROOFSTEP]
apply small_map (Equiv.equivPEmpty α)
[GOAL]
case inr
α : Type v
inst✝ : Subsingleton α
h✝ : Nonempty α
⊢ Small.{w, v} α
[PROOFSTEP]
apply small_map Equiv.punitOfNonemptyOfSubsingleton
[GOAL]
α : Type ?u.2397
β : α → Type u_1
inst✝¹ : Small.{w, ?u.2397} α
inst✝ : ∀ (a : α), Small.{w, u_1} (β a)
a : α
⊢ β a ≃ Shrink (β (↑(equivShrink α).symm (↑(equivShrink α) a)))
[PROOFSTEP]
simpa using equivShrink (β a)
[GOAL]
α : Type ?u.2805
β : α → Type u_1
inst✝¹ : Small.{w, ?u.2805} α
inst✝ : ∀ (a : α), Small.{w, u_1} (β a)
a : α
⊢ β a ≃ Shrink (β (↑(equivShrink α).symm (↑(equivShrink α) a)))
[PROOFSTEP]
simpa using equivShrink (β a)
[GOAL]
S : Type u
e✝ : Type (max u v) ≃ S
a b : Set ((α : S) × ↑e✝.symm α)
e :
  (fun a =>
        { fst := Equiv.toFun e✝ (Set ((α : S) × ↑e✝.symm α)),
          snd :=
            cast (_ : Set ((α : S) × ↑e✝.symm α) = Equiv.invFun e✝ (Equiv.toFun e✝ (Set ((α : S) × ↑e✝.symm α)))) a })
      a =
    (fun a =>
        { fst := Equiv.toFun e✝ (Set ((α : S) × ↑e✝.symm α)),
          snd :=
            cast (_ : Set ((α : S) × ↑e✝.symm α) = Equiv.invFun e✝ (Equiv.toFun e✝ (Set ((α : S) × ↑e✝.symm α)))) a })
      b
⊢ a = b
[PROOFSTEP]
dsimp at e
[GOAL]
S : Type u
e✝ : Type (max u v) ≃ S
a b : Set ((α : S) × ↑e✝.symm α)
e :
  { fst := ↑e✝ (Set ((α : S) × ↑e✝.symm α)),
      snd := cast (_ : Set ((α : S) × ↑e✝.symm α) = ↑e✝.symm (↑e✝ (Set ((α : S) × ↑e✝.symm α)))) a } =
    { fst := ↑e✝ (Set ((α : S) × ↑e✝.symm α)),
      snd := cast (_ : Set ((α : S) × ↑e✝.symm α) = ↑e✝.symm (↑e✝ (Set ((α : S) × ↑e✝.symm α)))) b }
⊢ a = b
[PROOFSTEP]
injection e with h₁ h₂
[GOAL]
S : Type u
e : Type (max u v) ≃ S
a b : Set ((α : S) × ↑e.symm α)
h₁ : ↑e (Set ((α : S) × ↑e.symm α)) = ↑e (Set ((α : S) × ↑e.symm α))
h₂ :
  cast (_ : Set ((α : S) × ↑e.symm α) = ↑e.symm (↑e (Set ((α : S) × ↑e.symm α)))) a =
    cast (_ : Set ((α : S) × ↑e.symm α) = ↑e.symm (↑e (Set ((α : S) × ↑e.symm α)))) b
⊢ a = b
[PROOFSTEP]
simpa using h₂


[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Encodable β
inst✝ : CompleteLattice α
f : β → α
⊢ ⨆ (i : ℕ) (b : β) (_ : b ∈ decode₂ β i), f b = ⨆ (b : β), f b
[PROOFSTEP]
rw [iSup_comm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Encodable β
inst✝ : CompleteLattice α
f : β → α
⊢ ⨆ (j : β) (i : ℕ) (_ : j ∈ decode₂ β i), f j = ⨆ (b : β), f b
[PROOFSTEP]
simp only [mem_decode₂, iSup_iSup_eq_right]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Encodable β
f : β → Set α
C : Set α → Prop
H0 : C ∅
H1 : ∀ (b : β), C (f b)
n : ℕ
⊢ C (⋃ (b : β) (_ : b ∈ none), f b)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Encodable β
f : β → Set α
C : Set α → Prop
H0 : C ∅
H1 : ∀ (b : β), C (f b)
n : ℕ
⊢ C ∅
[PROOFSTEP]
apply H0
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Encodable β
f : β → Set α
C : Set α → Prop
H0 : C ∅
H1 : ∀ (b : β), C (f b)
n : ℕ
b : β
⊢ C (⋃ (b_1 : β) (_ : b_1 ∈ some b), f b_1)
[PROOFSTEP]
convert H1 b
[GOAL]
case h.e'_1
α : Type u_1
β : Type u_2
inst✝ : Encodable β
f : β → Set α
C : Set α → Prop
H0 : C ∅
H1 : ∀ (b : β), C (f b)
n : ℕ
b : β
⊢ ⋃ (b_1 : β) (_ : b_1 ∈ some b), f b_1 = f b
[PROOFSTEP]
simp [ext_iff]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Encodable β
f : β → Set α
hd : Pairwise (Disjoint on f)
⊢ Pairwise (Disjoint on fun i => ⋃ (b : β) (_ : b ∈ decode₂ β i), f b)
[PROOFSTEP]
rintro i j ij
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Encodable β
f : β → Set α
hd : Pairwise (Disjoint on f)
i j : ℕ
ij : i ≠ j
⊢ (Disjoint on fun i => ⋃ (b : β) (_ : b ∈ decode₂ β i), f b) i j
[PROOFSTEP]
refine' disjoint_left.mpr fun x => _
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Encodable β
f : β → Set α
hd : Pairwise (Disjoint on f)
i j : ℕ
ij : i ≠ j
x : α
⊢ x ∈ (fun i => ⋃ (b : β) (_ : b ∈ decode₂ β i), f b) i → ¬x ∈ (fun i => ⋃ (b : β) (_ : b ∈ decode₂ β i), f b) j
[PROOFSTEP]
suffices ∀ a, encode a = i → x ∈ f a → ∀ b, encode b = j → x ∉ f b by simpa [decode₂_eq_some]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Encodable β
f : β → Set α
hd : Pairwise (Disjoint on f)
i j : ℕ
ij : i ≠ j
x : α
this : ∀ (a : β), encode a = i → x ∈ f a → ∀ (b : β), encode b = j → ¬x ∈ f b
⊢ x ∈ (fun i => ⋃ (b : β) (_ : b ∈ decode₂ β i), f b) i → ¬x ∈ (fun i => ⋃ (b : β) (_ : b ∈ decode₂ β i), f b) j
[PROOFSTEP]
simpa [decode₂_eq_some]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Encodable β
f : β → Set α
hd : Pairwise (Disjoint on f)
i j : ℕ
ij : i ≠ j
x : α
⊢ ∀ (a : β), encode a = i → x ∈ f a → ∀ (b : β), encode b = j → ¬x ∈ f b
[PROOFSTEP]
rintro a rfl ha b rfl hb
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Encodable β
f : β → Set α
hd : Pairwise (Disjoint on f)
x : α
a : β
ha : x ∈ f a
b : β
ij : encode a ≠ encode b
hb : x ∈ f b
⊢ False
[PROOFSTEP]
exact (hd (mt (congr_arg encode) ij)).le_bot ⟨ha, hb⟩


[GOAL]
α : Type v
inst✝ : Small.{u, v} α
⊢ Small.{u, v} (List α)
[PROOFSTEP]
let e : (Σ n, Vector α n) ≃ List α := Equiv.sigmaFiberEquiv List.length
[GOAL]
α : Type v
inst✝ : Small.{u, v} α
e : (n : ℕ) × Vector α n ≃ List α := Equiv.sigmaFiberEquiv List.length
⊢ Small.{u, v} (List α)
[PROOFSTEP]
exact small_of_surjective e.surjective