[GOAL]
α : Type u_1
β : α → Type u
δ : α → Sort v
inst✝ : DecidableEq α
a : α
b : δ a
s : Finset α
hs : ¬a ∈ s
e₁ e₂ : (a : α) → a ∈ s → δ a
eq : cons s a b e₁ = cons s a b e₂
e : α
h : e ∈ a ::ₘ s.val
⊢ e ∈ insert a s
[PROOFSTEP]
simpa only [Multiset.mem_cons, mem_insert] using h
[GOAL]
α : Type u_1
β : α → Type u
δ : α → Sort v
inst✝ : DecidableEq α
a : α
b : δ a
s : Finset α
hs : ¬a ∈ s
e₁ e₂ : (a : α) → a ∈ s → δ a
eq : cons s a b e₁ = cons s a b e₂
e : α
h : e ∈ a ::ₘ s.val
⊢ e ∈ insert a s
[PROOFSTEP]
simpa only [Multiset.mem_cons, mem_insert] using h
[GOAL]
α : Type u_1
β : α → Type u
δ : α → Sort v
inst✝ : DecidableEq α
a : α
b : δ a
s : Finset α
hs : ¬a ∈ s
e₁ e₂ : (a : α) → a ∈ s → δ a
eq : cons s a b e₁ = cons s a b e₂
e : α
h : e ∈ a ::ₘ s.val
⊢ cons s a b e₁ e (_ : e ∈ insert a s) = cons s a b e₂ e (_ : e ∈ insert a s)
[PROOFSTEP]
rw [eq]
[GOAL]
α : Type u_1
β : α → Type u
δ : α → Sort v
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
s : Finset α
t : (a : α) → Finset (β a)
a : α
ha : ¬a ∈ s
⊢ pi (insert a s) t = Finset.biUnion (t a) fun b => image (Pi.cons s a b) (pi s t)
[PROOFSTEP]
apply eq_of_veq
[GOAL]
case a
α : Type u_1
β : α → Type u
δ : α → Sort v
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
s : Finset α
t : (a : α) → Finset (β a)
a : α
ha : ¬a ∈ s
⊢ (pi (insert a s) t).val = (Finset.biUnion (t a) fun b => image (Pi.cons s a b) (pi s t)).val
[PROOFSTEP]
rw [← (pi (insert a s) t).2.dedup]
[GOAL]
case a
α : Type u_1
β : α → Type u
δ : α → Sort v
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
s : Finset α
t : (a : α) → Finset (β a)
a : α
ha : ¬a ∈ s
⊢ dedup (pi (insert a s) t).val = (Finset.biUnion (t a) fun b => image (Pi.cons s a b) (pi s t)).val
[PROOFSTEP]
refine'
  (fun s' (h : s' = a ::ₘ s.1) =>
      (_ :
        dedup (Multiset.pi s' fun a => (t a).1) =
          dedup
            ((t a).1.bind fun b =>
              dedup <|
                (Multiset.pi s.1 fun a : α => (t a).val).map fun f a' h' => Multiset.Pi.cons s.1 a b f a' (h ▸ h'))))
    _ (insert_val_of_not_mem ha)
[GOAL]
case a
α : Type u_1
β : α → Type u
δ : α → Sort v
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
s : Finset α
t : (a : α) → Finset (β a)
a : α
ha : ¬a ∈ s
s' : Multiset α
h : s' = a ::ₘ s.val
⊢ dedup (Multiset.pi s' fun a => (t a).val) =
    dedup
      (Multiset.bind (t a).val fun b =>
        dedup
          (Multiset.map (fun f a' h' => Multiset.Pi.cons s.val a b f a' (_ : a' ∈ a ::ₘ s.val))
            (Multiset.pi s.val fun a => (t a).val)))
[PROOFSTEP]
subst s'
[GOAL]
case a
α : Type u_1
β : α → Type u
δ : α → Sort v
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
s : Finset α
t : (a : α) → Finset (β a)
a : α
ha : ¬a ∈ s
⊢ dedup (Multiset.pi (a ::ₘ s.val) fun a => (t a).val) =
    dedup
      (Multiset.bind (t a).val fun b =>
        dedup
          (Multiset.map (fun f a' h' => Multiset.Pi.cons s.val a b f a' (_ : a' ∈ a ::ₘ s.val))
            (Multiset.pi s.val fun a => (t a).val)))
[PROOFSTEP]
rw [pi_cons]
[GOAL]
case a
α : Type u_1
β : α → Type u
δ : α → Sort v
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
s : Finset α
t : (a : α) → Finset (β a)
a : α
ha : ¬a ∈ s
⊢ dedup
      (Multiset.bind (t a).val fun b =>
        Multiset.map (Multiset.Pi.cons s.val a b) (Multiset.pi s.val fun a => (t a).val)) =
    dedup
      (Multiset.bind (t a).val fun b =>
        dedup
          (Multiset.map (fun f a' h' => Multiset.Pi.cons s.val a b f a' (_ : a' ∈ a ::ₘ s.val))
            (Multiset.pi s.val fun a => (t a).val)))
[PROOFSTEP]
congr
[GOAL]
case a.e_s.e_f
α : Type u_1
β : α → Type u
δ : α → Sort v
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
s : Finset α
t : (a : α) → Finset (β a)
a : α
ha : ¬a ∈ s
⊢ (fun b => Multiset.map (Multiset.Pi.cons s.val a b) (Multiset.pi s.val fun a => (t a).val)) = fun b =>
    dedup
      (Multiset.map (fun f a' h' => Multiset.Pi.cons s.val a b f a' (_ : a' ∈ a ::ₘ s.val))
        (Multiset.pi s.val fun a => (t a).val))
[PROOFSTEP]
funext b
[GOAL]
case a.e_s.e_f.h
α : Type u_1
β : α → Type u
δ : α → Sort v
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
s : Finset α
t : (a : α) → Finset (β a)
a : α
ha : ¬a ∈ s
b : β a
⊢ Multiset.map (Multiset.Pi.cons s.val a b) (Multiset.pi s.val fun a => (t a).val) =
    dedup
      (Multiset.map (fun f a' h' => Multiset.Pi.cons s.val a b f a' (_ : a' ∈ a ::ₘ s.val))
        (Multiset.pi s.val fun a => (t a).val))
[PROOFSTEP]
exact ((pi s t).nodup.map <| Multiset.Pi.cons_injective ha).dedup.symm
[GOAL]
α : Type u_1
β✝ : α → Type u
δ : α → Sort v
inst✝ : DecidableEq α
β : Type u_2
s : Finset α
f : α → β
⊢ (pi s fun a => {f a}) = {fun a x => f a}
[PROOFSTEP]
rw [eq_singleton_iff_unique_mem]
[GOAL]
α : Type u_1
β✝ : α → Type u
δ : α → Sort v
inst✝ : DecidableEq α
β : Type u_2
s : Finset α
f : α → β
⊢ ((fun a x => f a) ∈ pi s fun a => {f a}) ∧ ∀ (x : (a : α) → a ∈ s → β), (x ∈ pi s fun a => {f a}) → x = fun a x => f a
[PROOFSTEP]
constructor
[GOAL]
case left
α : Type u_1
β✝ : α → Type u
δ : α → Sort v
inst✝ : DecidableEq α
β : Type u_2
s : Finset α
f : α → β
⊢ (fun a x => f a) ∈ pi s fun a => {f a}
[PROOFSTEP]
simp
[GOAL]
case right
α : Type u_1
β✝ : α → Type u
δ : α → Sort v
inst✝ : DecidableEq α
β : Type u_2
s : Finset α
f : α → β
⊢ ∀ (x : (a : α) → a ∈ s → β), (x ∈ pi s fun a => {f a}) → x = fun a x => f a
[PROOFSTEP]
intro a ha
[GOAL]
case right
α : Type u_1
β✝ : α → Type u
δ : α → Sort v
inst✝ : DecidableEq α
β : Type u_2
s : Finset α
f : α → β
a : (a : α) → a ∈ s → β
ha : a ∈ pi s fun a => {f a}
⊢ a = fun a x => f a
[PROOFSTEP]
ext i hi
[GOAL]
case right.h.h
α : Type u_1
β✝ : α → Type u
δ : α → Sort v
inst✝ : DecidableEq α
β : Type u_2
s : Finset α
f : α → β
a : (a : α) → a ∈ s → β
ha : a ∈ pi s fun a => {f a}
i : α
hi : i ∈ s
⊢ a i hi = f i
[PROOFSTEP]
rw [mem_pi] at ha
[GOAL]
case right.h.h
α : Type u_1
β✝ : α → Type u
δ : α → Sort v
inst✝ : DecidableEq α
β : Type u_2
s : Finset α
f : α → β
a : (a : α) → a ∈ s → β
ha : ∀ (a_1 : α) (h : a_1 ∈ s), a a_1 h ∈ {f a_1}
i : α
hi : i ∈ s
⊢ a i hi = f i
[PROOFSTEP]
simpa using ha i hi


[GOAL]
α✝ β✝ : Type u
inst✝ : (P : Prop) → Decidable P
α β : Type ?u.384
⊢ Functor.mapConst = Functor.map ∘ const β
[PROOFSTEP]
simp only [Functor.mapConst, Functor.map]
[GOAL]
α✝ β✝ : Type u
inst✝ : (P : Prop) → Decidable P
α β γ : Type u_1
f : α → β → γ
s : Finset α
t : Finset β
⊢ image₂ f s t = Seq.seq (f <$> s) fun x => t
[PROOFSTEP]
ext
[GOAL]
case a
α✝ β✝ : Type u
inst✝ : (P : Prop) → Decidable P
α β γ : Type u_1
f : α → β → γ
s : Finset α
t : Finset β
a✝ : γ
⊢ a✝ ∈ image₂ f s t ↔ a✝ ∈ Seq.seq (f <$> s) fun x => t
[PROOFSTEP]
simp [mem_sup]
[GOAL]
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulFunctor Finset := lawfulFunctor
α✝ β✝ : Type ?u.13031
s : Finset α✝
t : Finset β✝
⊢ (SeqLeft.seqLeft s fun x => t) = Seq.seq (const β✝ <$> s) fun x => t
[PROOFSTEP]
rw [seq_def, fmap_def, seqLeft_def]
[GOAL]
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulFunctor Finset := lawfulFunctor
α✝ β✝ : Type ?u.13031
s : Finset α✝
t : Finset β✝
⊢ (if t = ∅ then ∅ else s) = sup (image (const β✝) s) fun f => image f t
[PROOFSTEP]
obtain rfl | ht := t.eq_empty_or_nonempty
[GOAL]
case inl
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulFunctor Finset := lawfulFunctor
α✝ β✝ : Type ?u.13031
s : Finset α✝
⊢ (if ∅ = ∅ then ∅ else s) = sup (image (const β✝) s) fun f => image f ∅
[PROOFSTEP]
simp_rw [image_empty, if_true]
[GOAL]
case inl
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulFunctor Finset := lawfulFunctor
α✝ β✝ : Type ?u.13031
s : Finset α✝
⊢ ∅ = sup (image (const β✝) s) fun f => ∅
[PROOFSTEP]
exact (sup_bot _).symm
[GOAL]
case inr
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulFunctor Finset := lawfulFunctor
α✝ β✝ : Type ?u.13031
s : Finset α✝
t : Finset β✝
ht : Finset.Nonempty t
⊢ (if t = ∅ then ∅ else s) = sup (image (const β✝) s) fun f => image f t
[PROOFSTEP]
ext a
[GOAL]
case inr.a
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulFunctor Finset := lawfulFunctor
α✝ β✝ : Type ?u.13031
s : Finset α✝
t : Finset β✝
ht : Finset.Nonempty t
a : α✝
⊢ (a ∈ if t = ∅ then ∅ else s) ↔ a ∈ sup (image (const β✝) s) fun f => image f t
[PROOFSTEP]
rw [if_neg ht.ne_empty, mem_sup]
[GOAL]
case inr.a
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulFunctor Finset := lawfulFunctor
α✝ β✝ : Type ?u.13031
s : Finset α✝
t : Finset β✝
ht : Finset.Nonempty t
a : α✝
⊢ a ∈ s ↔ ∃ v, v ∈ image (const β✝) s ∧ a ∈ image v t
[PROOFSTEP]
refine' ⟨fun ha => ⟨const _ a, mem_image_of_mem _ ha, mem_image_const_self.2 ht⟩, _⟩
[GOAL]
case inr.a
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulFunctor Finset := lawfulFunctor
α✝ β✝ : Type ?u.13031
s : Finset α✝
t : Finset β✝
ht : Finset.Nonempty t
a : α✝
⊢ (∃ v, v ∈ image (const β✝) s ∧ a ∈ image v t) → a ∈ s
[PROOFSTEP]
rintro ⟨f, hf, ha⟩
[GOAL]
case inr.a.intro.intro
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulFunctor Finset := lawfulFunctor
α✝ β✝ : Type ?u.13031
s : Finset α✝
t : Finset β✝
ht : Finset.Nonempty t
a : α✝
f : β✝ → α✝
hf : f ∈ image (const β✝) s
ha : a ∈ image f t
⊢ a ∈ s
[PROOFSTEP]
rw [mem_image] at hf ha
[GOAL]
case inr.a.intro.intro
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulFunctor Finset := lawfulFunctor
α✝ β✝ : Type ?u.13031
s : Finset α✝
t : Finset β✝
ht : Finset.Nonempty t
a : α✝
f : β✝ → α✝
hf : ∃ a, a ∈ s ∧ const β✝ a = f
ha : ∃ a_1, a_1 ∈ t ∧ f a_1 = a
⊢ a ∈ s
[PROOFSTEP]
obtain ⟨b, hb, rfl⟩ := hf
[GOAL]
case inr.a.intro.intro.intro.intro
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulFunctor Finset := lawfulFunctor
α✝ β✝ : Type ?u.13031
s : Finset α✝
t : Finset β✝
ht : Finset.Nonempty t
a b : α✝
hb : b ∈ s
ha : ∃ a_1, a_1 ∈ t ∧ const β✝ b a_1 = a
⊢ a ∈ s
[PROOFSTEP]
obtain ⟨_, _, rfl⟩ := ha
[GOAL]
case inr.a.intro.intro.intro.intro.intro.intro
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulFunctor Finset := lawfulFunctor
α✝ β✝ : Type ?u.13031
s : Finset α✝
t : Finset β✝
ht : Finset.Nonempty t
b : α✝
hb : b ∈ s
w✝ : β✝
left✝ : w✝ ∈ t
⊢ const β✝ b w✝ ∈ s
[PROOFSTEP]
exact hb
[GOAL]
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulFunctor Finset := lawfulFunctor
α✝ β✝ : Type ?u.13031
s : Finset α✝
t : Finset β✝
⊢ (SeqRight.seqRight s fun x => t) = Seq.seq (const α✝ id <$> s) fun x => t
[PROOFSTEP]
rw [seq_def, fmap_def, seqRight_def]
[GOAL]
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulFunctor Finset := lawfulFunctor
α✝ β✝ : Type ?u.13031
s : Finset α✝
t : Finset β✝
⊢ (if s = ∅ then ∅ else t) = sup (image (const α✝ id) s) fun f => image f t
[PROOFSTEP]
obtain rfl | hs := s.eq_empty_or_nonempty
[GOAL]
case inl
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulFunctor Finset := lawfulFunctor
α✝ β✝ : Type ?u.13031
t : Finset β✝
⊢ (if ∅ = ∅ then ∅ else t) = sup (image (const α✝ id) ∅) fun f => image f t
[PROOFSTEP]
rw [if_pos rfl, image_empty, sup_empty, bot_eq_empty]
[GOAL]
case inr
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulFunctor Finset := lawfulFunctor
α✝ β✝ : Type ?u.13031
s : Finset α✝
t : Finset β✝
hs : Finset.Nonempty s
⊢ (if s = ∅ then ∅ else t) = sup (image (const α✝ id) s) fun f => image f t
[PROOFSTEP]
ext a
[GOAL]
case inr.a
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulFunctor Finset := lawfulFunctor
α✝ β✝ : Type ?u.13031
s : Finset α✝
t : Finset β✝
hs : Finset.Nonempty s
a : β✝
⊢ (a ∈ if s = ∅ then ∅ else t) ↔ a ∈ sup (image (const α✝ id) s) fun f => image f t
[PROOFSTEP]
rw [if_neg hs.ne_empty, mem_sup]
[GOAL]
case inr.a
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulFunctor Finset := lawfulFunctor
α✝ β✝ : Type ?u.13031
s : Finset α✝
t : Finset β✝
hs : Finset.Nonempty s
a : β✝
⊢ a ∈ t ↔ ∃ v, v ∈ image (const α✝ id) s ∧ a ∈ image v t
[PROOFSTEP]
refine' ⟨fun ha => ⟨id, mem_image_const_self.2 hs, by rwa [image_id]⟩, _⟩
[GOAL]
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulFunctor Finset := lawfulFunctor
α✝ β✝ : Type ?u.13031
s : Finset α✝
t : Finset β✝
hs : Finset.Nonempty s
a : β✝
ha : a ∈ t
⊢ a ∈ image id t
[PROOFSTEP]
rwa [image_id]
[GOAL]
case inr.a
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulFunctor Finset := lawfulFunctor
α✝ β✝ : Type ?u.13031
s : Finset α✝
t : Finset β✝
hs : Finset.Nonempty s
a : β✝
⊢ (∃ v, v ∈ image (const α✝ id) s ∧ a ∈ image v t) → a ∈ t
[PROOFSTEP]
rintro ⟨f, hf, ha⟩
[GOAL]
case inr.a.intro.intro
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulFunctor Finset := lawfulFunctor
α✝ β✝ : Type ?u.13031
s : Finset α✝
t : Finset β✝
hs : Finset.Nonempty s
a : β✝
f : β✝ → β✝
hf : f ∈ image (const α✝ id) s
ha : a ∈ image f t
⊢ a ∈ t
[PROOFSTEP]
rw [mem_image] at hf ha
[GOAL]
case inr.a.intro.intro
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulFunctor Finset := lawfulFunctor
α✝ β✝ : Type ?u.13031
s : Finset α✝
t : Finset β✝
hs : Finset.Nonempty s
a : β✝
f : β✝ → β✝
hf : ∃ a, a ∈ s ∧ const α✝ id a = f
ha : ∃ a_1, a_1 ∈ t ∧ f a_1 = a
⊢ a ∈ t
[PROOFSTEP]
obtain ⟨b, hb, rfl⟩ := ha
[GOAL]
case inr.a.intro.intro.intro.intro
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulFunctor Finset := lawfulFunctor
α✝ β✝ : Type ?u.13031
s : Finset α✝
t : Finset β✝
hs : Finset.Nonempty s
f : β✝ → β✝
hf : ∃ a, a ∈ s ∧ const α✝ id a = f
b : β✝
hb : b ∈ t
⊢ f b ∈ t
[PROOFSTEP]
obtain ⟨_, _, rfl⟩ := hf
[GOAL]
case inr.a.intro.intro.intro.intro.intro.intro
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulFunctor Finset := lawfulFunctor
α✝ β✝ : Type ?u.13031
s : Finset α✝
t : Finset β✝
hs : Finset.Nonempty s
b : β✝
hb : b ∈ t
w✝ : α✝
left✝ : w✝ ∈ s
⊢ const α✝ id w✝ b ∈ t
[PROOFSTEP]
exact hb
[GOAL]
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulFunctor Finset := lawfulFunctor
α✝ β✝ : Type ?u.13031
f : α✝ → β✝
s : Finset α✝
⊢ (Seq.seq (pure f) fun x => s) = f <$> s
[PROOFSTEP]
simp only [pure_def, seq_def, sup_singleton, fmap_def]
[GOAL]
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulFunctor Finset := lawfulFunctor
α✝ β✝ γ✝ : Type ?u.13031
s : Finset α✝
t : Finset (α✝ → β✝)
u : Finset (β✝ → γ✝)
⊢ (Seq.seq u fun x => Seq.seq t fun x => s) = Seq.seq (Seq.seq (comp <$> u) fun x => t) fun x => s
[PROOFSTEP]
ext a
[GOAL]
case a
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulFunctor Finset := lawfulFunctor
α✝ β✝ γ✝ : Type ?u.13031
s : Finset α✝
t : Finset (α✝ → β✝)
u : Finset (β✝ → γ✝)
a : γ✝
⊢ (a ∈ Seq.seq u fun x => Seq.seq t fun x => s) ↔ a ∈ Seq.seq (Seq.seq (comp <$> u) fun x => t) fun x => s
[PROOFSTEP]
simp_rw [seq_def, fmap_def]
[GOAL]
case a
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulFunctor Finset := lawfulFunctor
α✝ β✝ γ✝ : Type ?u.13031
s : Finset α✝
t : Finset (α✝ → β✝)
u : Finset (β✝ → γ✝)
a : γ✝
⊢ (a ∈ sup u fun f => image f (sup t fun f => image f s)) ↔
    a ∈ sup (sup (image comp u) fun f => image f t) fun f => image f s
[PROOFSTEP]
simp only [exists_prop, mem_sup, mem_image]
[GOAL]
case a
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulFunctor Finset := lawfulFunctor
α✝ β✝ γ✝ : Type ?u.13031
s : Finset α✝
t : Finset (α✝ → β✝)
u : Finset (β✝ → γ✝)
a : γ✝
⊢ (∃ v, v ∈ u ∧ ∃ a_1, (∃ v, v ∈ t ∧ ∃ a, a ∈ s ∧ v a = a_1) ∧ v a_1 = a) ↔
    ∃ v, (∃ v_1, (∃ a, a ∈ u ∧ comp a = v_1) ∧ ∃ a, a ∈ t ∧ v_1 a = v) ∧ ∃ a_1, a_1 ∈ s ∧ v a_1 = a
[PROOFSTEP]
constructor
[GOAL]
case a.mp
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulFunctor Finset := lawfulFunctor
α✝ β✝ γ✝ : Type ?u.13031
s : Finset α✝
t : Finset (α✝ → β✝)
u : Finset (β✝ → γ✝)
a : γ✝
⊢ (∃ v, v ∈ u ∧ ∃ a_1, (∃ v, v ∈ t ∧ ∃ a, a ∈ s ∧ v a = a_1) ∧ v a_1 = a) →
    ∃ v, (∃ v_1, (∃ a, a ∈ u ∧ comp a = v_1) ∧ ∃ a, a ∈ t ∧ v_1 a = v) ∧ ∃ a_2, a_2 ∈ s ∧ v a_2 = a
[PROOFSTEP]
rintro ⟨g, hg, b, ⟨f, hf, a, ha, rfl⟩, rfl⟩
[GOAL]
case a.mp.intro.intro.intro.intro.intro.intro.intro.intro
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulFunctor Finset := lawfulFunctor
α✝ β✝ γ✝ : Type ?u.13031
s : Finset α✝
t : Finset (α✝ → β✝)
u : Finset (β✝ → γ✝)
g : β✝ → γ✝
hg : g ∈ u
f : α✝ → β✝
hf : f ∈ t
a : α✝
ha : a ∈ s
⊢ ∃ v, (∃ v_1, (∃ a, a ∈ u ∧ comp a = v_1) ∧ ∃ a, a ∈ t ∧ v_1 a = v) ∧ ∃ a_1, a_1 ∈ s ∧ v a_1 = g (f a)
[PROOFSTEP]
exact ⟨g ∘ f, ⟨comp g, ⟨g, hg, rfl⟩, f, hf, rfl⟩, a, ha, rfl⟩
[GOAL]
case a.mpr
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulFunctor Finset := lawfulFunctor
α✝ β✝ γ✝ : Type ?u.13031
s : Finset α✝
t : Finset (α✝ → β✝)
u : Finset (β✝ → γ✝)
a : γ✝
⊢ (∃ v, (∃ v_1, (∃ a, a ∈ u ∧ comp a = v_1) ∧ ∃ a, a ∈ t ∧ v_1 a = v) ∧ ∃ a_1, a_1 ∈ s ∧ v a_1 = a) →
    ∃ v, v ∈ u ∧ ∃ a_2, (∃ v, v ∈ t ∧ ∃ a, a ∈ s ∧ v a = a_2) ∧ v a_2 = a
[PROOFSTEP]
rintro ⟨c, ⟨_, ⟨g, hg, rfl⟩, f, hf, rfl⟩, a, ha, rfl⟩
[GOAL]
case a.mpr.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulFunctor Finset := lawfulFunctor
α✝ β✝ γ✝ : Type ?u.13031
s : Finset α✝
t : Finset (α✝ → β✝)
u : Finset (β✝ → γ✝)
g : β✝ → γ✝
hg : g ∈ u
f : α✝ → β✝
hf : f ∈ t
a : α✝
ha : a ∈ s
⊢ ∃ v, v ∈ u ∧ ∃ a_1, (∃ v, v ∈ t ∧ ∃ a, a ∈ s ∧ v a = a_1) ∧ v a_1 = (g ∘ f) a
[PROOFSTEP]
exact ⟨g, hg, f a, ⟨f, hf, a, ha, rfl⟩, rfl⟩
[GOAL]
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulApplicative Finset := lawfulApplicative
α✝ β✝ : Type ?u.21428
s : Finset α✝
t : Finset β✝
⊢ (Seq.seq (Prod.mk <$> s) fun x => t) = Seq.seq ((fun b a => (a, b)) <$> t) fun x => s
[PROOFSTEP]
simp_rw [seq_def, fmap_def, sup_image, sup_eq_biUnion]
[GOAL]
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulApplicative Finset := lawfulApplicative
α✝ β✝ : Type ?u.21428
s : Finset α✝
t : Finset β✝
⊢ Finset.biUnion s ((fun f => image f t) ∘ Prod.mk) = Finset.biUnion t ((fun f => image f s) ∘ fun b a => (a, b))
[PROOFSTEP]
change (s.biUnion fun a => t.image fun b => (a, b)) = t.biUnion fun b => s.image fun a => (a, b)
[GOAL]
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulApplicative Finset := lawfulApplicative
α✝ β✝ : Type ?u.21428
s : Finset α✝
t : Finset β✝
⊢ (Finset.biUnion s fun a => image (fun b => (a, b)) t) = Finset.biUnion t fun b => image (fun a => (a, b)) s
[PROOFSTEP]
trans s ×ˢ t <;> [rw [product_eq_biUnion]; rw [product_eq_biUnion_right]]
[GOAL]
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulApplicative Finset := lawfulApplicative
α✝ β✝ : Type ?u.21428
s : Finset α✝
t : Finset β✝
⊢ (Finset.biUnion s fun a => image (fun b => (a, b)) t) = Finset.biUnion t fun b => image (fun a => (a, b)) s
[PROOFSTEP]
trans s ×ˢ t
[GOAL]
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulApplicative Finset := lawfulApplicative
α✝ β✝ : Type ?u.23242
s : Finset α✝
t : Finset β✝
⊢ (Finset.biUnion s fun a => image (fun b => (a, b)) t) = s ×ˢ t
[PROOFSTEP]
rw [product_eq_biUnion]
[GOAL]
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulApplicative Finset := lawfulApplicative
α✝ β✝ : Type ?u.23242
s : Finset α✝
t : Finset β✝
⊢ s ×ˢ t = Finset.biUnion t fun b => image (fun a => (a, b)) s
[PROOFSTEP]
rw [product_eq_biUnion_right]
[GOAL]
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulApplicative Finset := lawfulApplicative
α✝ β✝ γ✝ : Type ?u.24298
s : Finset α✝
f : α✝ → Finset β✝
g : β✝ → Finset γ✝
⊢ s >>= f >>= g = s >>= fun x => f x >>= g
[PROOFSTEP]
simp only [bind, ← sup_biUnion, sup_eq_biUnion, biUnion_biUnion]
[GOAL]
α β γ : Type u
F G : Type u → Type u
inst✝⁴ : Applicative F
inst✝³ : Applicative G
inst✝² : CommApplicative F
inst✝¹ : CommApplicative G
inst✝ : DecidableEq α
s : Finset α
⊢ traverse pure s = s
[PROOFSTEP]
rw [traverse, Multiset.id_traverse]
[GOAL]
α β γ : Type u
F G : Type u → Type u
inst✝⁴ : Applicative F
inst✝³ : Applicative G
inst✝² : CommApplicative F
inst✝¹ : CommApplicative G
inst✝ : DecidableEq α
s : Finset α
⊢ Multiset.toFinset <$> s.val = s
[PROOFSTEP]
exact s.val_toFinset
[GOAL]
α β γ : Type u
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : CommApplicative F
inst✝ : CommApplicative G
g : α → G β
h : β → γ
s : Finset α
⊢ Functor.map h <$> traverse g s = traverse (Functor.map h ∘ g) s
[PROOFSTEP]
unfold traverse
[GOAL]
α β γ : Type u
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : CommApplicative F
inst✝ : CommApplicative G
g : α → G β
h : β → γ
s : Finset α
⊢ Functor.map h <$> Multiset.toFinset <$> Multiset.traverse g s.val =
    Multiset.toFinset <$> Multiset.traverse (Functor.map h ∘ g) s.val
[PROOFSTEP]
simp only [map_comp_coe, functor_norm]
[GOAL]
α β γ : Type u
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : CommApplicative F
inst✝ : CommApplicative G
g : α → G β
h : β → γ
s : Finset α
⊢ (Multiset.toFinset ∘ Functor.map h) <$> Multiset.traverse g s.val =
    Multiset.toFinset <$> Multiset.traverse (Functor.map h ∘ g) s.val
[PROOFSTEP]
rw [LawfulFunctor.comp_map, Multiset.map_traverse]


[GOAL]
f : Type u → Type v
inst✝¹ : Functor f
inst✝ : LawfulFunctor f
α β : Type u
h : α ≃ β
x : f α
⊢ ↑h.symm <$> ↑h <$> x = x
[PROOFSTEP]
simp [map_map]
[GOAL]
f : Type u → Type v
inst✝¹ : Functor f
inst✝ : LawfulFunctor f
α β : Type u
h : α ≃ β
x : f β
⊢ ↑h <$> ↑h.symm <$> x = x
[PROOFSTEP]
simp [map_map]


[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝⁴ : Fintype n
inst✝³ : Fintype o
inst✝² : CommRing R
inst✝¹ : StrongRankCondition R
inst✝ : DecidableEq n
⊢ rank 1 = Fintype.card n
[PROOFSTEP]
rw [rank, mulVecLin_one, LinearMap.range_id, finrank_top, finrank_pi]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : CommRing R
inst✝ : Nontrivial R
⊢ rank 0 = 0
[PROOFSTEP]
rw [rank, mulVecLin_zero, LinearMap.range_zero, finrank_bot]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : CommRing R
inst✝ : StrongRankCondition R
A : Matrix m n R
⊢ rank A ≤ Fintype.card n
[PROOFSTEP]
haveI : Module.Finite R (n → R) := Module.Finite.pi
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : CommRing R
inst✝ : StrongRankCondition R
A : Matrix m n R
this : Module.Finite R (n → R)
⊢ rank A ≤ Fintype.card n
[PROOFSTEP]
haveI : Module.Free R (n → R) := Module.Free.pi _ _
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : CommRing R
inst✝ : StrongRankCondition R
A : Matrix m n R
this✝ : Module.Finite R (n → R)
this : Module.Free R (n → R)
⊢ rank A ≤ Fintype.card n
[PROOFSTEP]
exact A.mulVecLin.finrank_range_le.trans_eq (finrank_pi _)
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : CommRing R
inst✝ : StrongRankCondition R
A : Matrix m n R
B : Matrix n o R
⊢ rank (A * B) ≤ rank A
[PROOFSTEP]
rw [rank, rank, mulVecLin_mul]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : CommRing R
inst✝ : StrongRankCondition R
A : Matrix m n R
B : Matrix n o R
⊢ finrank R { x // x ∈ LinearMap.range (LinearMap.comp (mulVecLin A) (mulVecLin B)) } ≤
    finrank R { x // x ∈ LinearMap.range (mulVecLin A) }
[PROOFSTEP]
exact Cardinal.toNat_le_of_le_of_lt_aleph0 (rank_lt_aleph0 _ _) (LinearMap.rank_comp_le_left _ _)
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : CommRing R
inst✝ : StrongRankCondition R
A : Matrix l m R
B : Matrix m n R
⊢ rank (A * B) ≤ rank B
[PROOFSTEP]
rw [rank, rank, mulVecLin_mul]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : CommRing R
inst✝ : StrongRankCondition R
A : Matrix l m R
B : Matrix m n R
⊢ finrank R { x // x ∈ LinearMap.range (LinearMap.comp (mulVecLin A) (mulVecLin B)) } ≤
    finrank R { x // x ∈ LinearMap.range (mulVecLin B) }
[PROOFSTEP]
exact finrank_le_finrank_of_rank_le_rank (LinearMap.lift_rank_comp_le_right _ _) (rank_lt_aleph0 _ _)
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝⁴ : Fintype n
inst✝³ : Fintype o
inst✝² : CommRing R
inst✝¹ : StrongRankCondition R
inst✝ : DecidableEq n
A : (Matrix n n R)ˣ
⊢ rank ↑A = Fintype.card n
[PROOFSTEP]
refine' le_antisymm (rank_le_card_width A) _
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝⁴ : Fintype n
inst✝³ : Fintype o
inst✝² : CommRing R
inst✝¹ : StrongRankCondition R
inst✝ : DecidableEq n
A : (Matrix n n R)ˣ
⊢ Fintype.card n ≤ rank ↑A
[PROOFSTEP]
have := rank_mul_le_left (A : Matrix n n R) (↑A⁻¹ : Matrix n n R)
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝⁴ : Fintype n
inst✝³ : Fintype o
inst✝² : CommRing R
inst✝¹ : StrongRankCondition R
inst✝ : DecidableEq n
A : (Matrix n n R)ˣ
this : rank (↑A * ↑A⁻¹) ≤ rank ↑A
⊢ Fintype.card n ≤ rank ↑A
[PROOFSTEP]
rwa [← Units.val_mul, mul_inv_self, Units.val_one, rank_one] at this
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝⁴ : Fintype n
inst✝³ : Fintype o
inst✝² : CommRing R
inst✝¹ : StrongRankCondition R
inst✝ : DecidableEq n
A : Matrix n n R
h : IsUnit A
⊢ rank A = Fintype.card n
[PROOFSTEP]
obtain ⟨A, rfl⟩ := h
[GOAL]
case intro
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝⁴ : Fintype n
inst✝³ : Fintype o
inst✝² : CommRing R
inst✝¹ : StrongRankCondition R
inst✝ : DecidableEq n
A : (Matrix n n R)ˣ
⊢ rank ↑A = Fintype.card n
[PROOFSTEP]
exact rank_unit A
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : CommRing R
inst✝ : DecidableEq n
A : Matrix n n R
B : Matrix m n R
hA : IsUnit (det A)
⊢ rank (B * A) = rank B
[PROOFSTEP]
suffices : Function.Surjective A.mulVecLin
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : CommRing R
inst✝ : DecidableEq n
A : Matrix n n R
B : Matrix m n R
hA : IsUnit (det A)
this : Function.Surjective ↑(mulVecLin A)
⊢ rank (B * A) = rank B
[PROOFSTEP]
rw [rank, mulVecLin_mul, LinearMap.range_comp_of_range_eq_top _ (LinearMap.range_eq_top.mpr this), ← rank]
[GOAL]
case this
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : CommRing R
inst✝ : DecidableEq n
A : Matrix n n R
B : Matrix m n R
hA : IsUnit (det A)
⊢ Function.Surjective ↑(mulVecLin A)
[PROOFSTEP]
intro v
[GOAL]
case this
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : CommRing R
inst✝ : DecidableEq n
A : Matrix n n R
B : Matrix m n R
hA : IsUnit (det A)
v : n → R
⊢ ∃ a, ↑(mulVecLin A) a = v
[PROOFSTEP]
exact ⟨(A⁻¹).mulVecLin v, by simp [mul_nonsing_inv _ hA]⟩
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : CommRing R
inst✝ : DecidableEq n
A : Matrix n n R
B : Matrix m n R
hA : IsUnit (det A)
v : n → R
⊢ ↑(mulVecLin A) (↑(mulVecLin A⁻¹) v) = v
[PROOFSTEP]
simp [mul_nonsing_inv _ hA]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : CommRing R
inst✝ : DecidableEq m
A : Matrix m m R
B : Matrix m n R
hA : IsUnit (det A)
⊢ rank (A * B) = rank B
[PROOFSTEP]
let b : Basis m R (m → R) := Pi.basisFun R m
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : CommRing R
inst✝ : DecidableEq m
A : Matrix m m R
B : Matrix m n R
hA : IsUnit (det A)
b : Basis m R (m → R) := Pi.basisFun R m
⊢ rank (A * B) = rank B
[PROOFSTEP]
replace hA : IsUnit (LinearMap.toMatrix b b A.mulVecLin).det := by convert hA; rw [← LinearEquiv.eq_symm_apply]; rfl
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : CommRing R
inst✝ : DecidableEq m
A : Matrix m m R
B : Matrix m n R
hA : IsUnit (det A)
b : Basis m R (m → R) := Pi.basisFun R m
⊢ IsUnit (det (↑(LinearMap.toMatrix b b) (mulVecLin A)))
[PROOFSTEP]
convert hA
[GOAL]
case h.e'_3.h.e'_6
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : CommRing R
inst✝ : DecidableEq m
A : Matrix m m R
B : Matrix m n R
hA : IsUnit (det A)
b : Basis m R (m → R) := Pi.basisFun R m
⊢ ↑(LinearMap.toMatrix b b) (mulVecLin A) = A
[PROOFSTEP]
rw [← LinearEquiv.eq_symm_apply]
[GOAL]
case h.e'_3.h.e'_6
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : CommRing R
inst✝ : DecidableEq m
A : Matrix m m R
B : Matrix m n R
hA : IsUnit (det A)
b : Basis m R (m → R) := Pi.basisFun R m
⊢ mulVecLin A = ↑(LinearEquiv.symm (LinearMap.toMatrix b b)) A
[PROOFSTEP]
rfl
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : CommRing R
inst✝ : DecidableEq m
A : Matrix m m R
B : Matrix m n R
b : Basis m R (m → R) := Pi.basisFun R m
hA : IsUnit (det (↑(LinearMap.toMatrix b b) (mulVecLin A)))
⊢ rank (A * B) = rank B
[PROOFSTEP]
have hAB : mulVecLin (A * B) = (LinearEquiv.ofIsUnitDet hA).comp (mulVecLin B) := by ext; simp
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : CommRing R
inst✝ : DecidableEq m
A : Matrix m m R
B : Matrix m n R
b : Basis m R (m → R) := Pi.basisFun R m
hA : IsUnit (det (↑(LinearMap.toMatrix b b) (mulVecLin A)))
⊢ mulVecLin (A * B) = LinearMap.comp (↑(LinearEquiv.ofIsUnitDet hA)) (mulVecLin B)
[PROOFSTEP]
ext
[GOAL]
case h.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : CommRing R
inst✝ : DecidableEq m
A : Matrix m m R
B : Matrix m n R
b : Basis m R (m → R) := Pi.basisFun R m
hA : IsUnit (det (↑(LinearMap.toMatrix b b) (mulVecLin A)))
x✝¹ : n → R
x✝ : m
⊢ ↑(mulVecLin (A * B)) x✝¹ x✝ = ↑(LinearMap.comp (↑(LinearEquiv.ofIsUnitDet hA)) (mulVecLin B)) x✝¹ x✝
[PROOFSTEP]
simp
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : CommRing R
inst✝ : DecidableEq m
A : Matrix m m R
B : Matrix m n R
b : Basis m R (m → R) := Pi.basisFun R m
hA : IsUnit (det (↑(LinearMap.toMatrix b b) (mulVecLin A)))
hAB : mulVecLin (A * B) = LinearMap.comp (↑(LinearEquiv.ofIsUnitDet hA)) (mulVecLin B)
⊢ rank (A * B) = rank B
[PROOFSTEP]
rw [rank, rank, hAB, LinearMap.range_comp, LinearEquiv.finrank_map_eq]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝⁴ : Fintype n
inst✝³ : Fintype o
inst✝² : CommRing R
inst✝¹ : StrongRankCondition R
inst✝ : Fintype m
f : n → m
e : n ≃ m
A : Matrix m m R
⊢ rank (submatrix A f ↑e) ≤ rank A
[PROOFSTEP]
rw [rank, rank, mulVecLin_submatrix, LinearMap.range_comp, LinearMap.range_comp,
  show LinearMap.funLeft R R e.symm = LinearEquiv.funCongrLeft R R e.symm from rfl, LinearEquiv.range,
  Submodule.map_top]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝⁴ : Fintype n
inst✝³ : Fintype o
inst✝² : CommRing R
inst✝¹ : StrongRankCondition R
inst✝ : Fintype m
f : n → m
e : n ≃ m
A : Matrix m m R
⊢ finrank R { x // x ∈ Submodule.map (LinearMap.funLeft R R f) (LinearMap.range (mulVecLin A)) } ≤
    finrank R { x // x ∈ LinearMap.range (mulVecLin A) }
[PROOFSTEP]
exact Submodule.finrank_map_le _ _
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : CommRing R
inst✝ : Fintype m
e₁ e₂ : m ≃ n
A : Matrix m m R
⊢ rank (↑(reindex e₁ e₂) A) = rank A
[PROOFSTEP]
rw [rank, rank, mulVecLin_reindex, LinearMap.range_comp, LinearMap.range_comp, LinearEquiv.range, Submodule.map_top,
  LinearEquiv.finrank_map_eq]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : CommRing R
inst✝ : Fintype m
A : Matrix m m R
e₁ e₂ : n ≃ m
⊢ rank (submatrix A ↑e₁ ↑e₂) = rank A
[PROOFSTEP]
simpa only [reindex_apply] using rank_reindex e₁.symm e₂.symm A
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝⁷ : Fintype n
inst✝⁶ : Fintype o
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq n
M₁ : Type u_6
M₂ : Type u_7
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
A : Matrix m n R
v₁ : Basis m R M₁
v₂ : Basis n R M₂
⊢ rank A = finrank R { x // x ∈ LinearMap.range (↑(toLin v₂ v₁) A) }
[PROOFSTEP]
let e₁ := (Pi.basisFun R m).equiv v₁ (Equiv.refl _)
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝⁷ : Fintype n
inst✝⁶ : Fintype o
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq n
M₁ : Type u_6
M₂ : Type u_7
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
A : Matrix m n R
v₁ : Basis m R M₁
v₂ : Basis n R M₂
e₁ : (m → R) ≃ₗ[R] M₁ := Basis.equiv (Pi.basisFun R m) v₁ (Equiv.refl m)
⊢ rank A = finrank R { x // x ∈ LinearMap.range (↑(toLin v₂ v₁) A) }
[PROOFSTEP]
let e₂ := (Pi.basisFun R n).equiv v₂ (Equiv.refl _)
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝⁷ : Fintype n
inst✝⁶ : Fintype o
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq n
M₁ : Type u_6
M₂ : Type u_7
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
A : Matrix m n R
v₁ : Basis m R M₁
v₂ : Basis n R M₂
e₁ : (m → R) ≃ₗ[R] M₁ := Basis.equiv (Pi.basisFun R m) v₁ (Equiv.refl m)
e₂ : (n → R) ≃ₗ[R] M₂ := Basis.equiv (Pi.basisFun R n) v₂ (Equiv.refl n)
⊢ rank A = finrank R { x // x ∈ LinearMap.range (↑(toLin v₂ v₁) A) }
[PROOFSTEP]
have range_e₂ : LinearMap.range e₂ = ⊤ := by
  rw [LinearMap.range_eq_top]
  exact e₂.surjective
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝⁷ : Fintype n
inst✝⁶ : Fintype o
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq n
M₁ : Type u_6
M₂ : Type u_7
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
A : Matrix m n R
v₁ : Basis m R M₁
v₂ : Basis n R M₂
e₁ : (m → R) ≃ₗ[R] M₁ := Basis.equiv (Pi.basisFun R m) v₁ (Equiv.refl m)
e₂ : (n → R) ≃ₗ[R] M₂ := Basis.equiv (Pi.basisFun R n) v₂ (Equiv.refl n)
⊢ LinearMap.range e₂ = ⊤
[PROOFSTEP]
rw [LinearMap.range_eq_top]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝⁷ : Fintype n
inst✝⁶ : Fintype o
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq n
M₁ : Type u_6
M₂ : Type u_7
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
A : Matrix m n R
v₁ : Basis m R M₁
v₂ : Basis n R M₂
e₁ : (m → R) ≃ₗ[R] M₁ := Basis.equiv (Pi.basisFun R m) v₁ (Equiv.refl m)
e₂ : (n → R) ≃ₗ[R] M₂ := Basis.equiv (Pi.basisFun R n) v₂ (Equiv.refl n)
⊢ Function.Surjective ↑e₂
[PROOFSTEP]
exact e₂.surjective
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝⁷ : Fintype n
inst✝⁶ : Fintype o
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq n
M₁ : Type u_6
M₂ : Type u_7
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
A : Matrix m n R
v₁ : Basis m R M₁
v₂ : Basis n R M₂
e₁ : (m → R) ≃ₗ[R] M₁ := Basis.equiv (Pi.basisFun R m) v₁ (Equiv.refl m)
e₂ : (n → R) ≃ₗ[R] M₂ := Basis.equiv (Pi.basisFun R n) v₂ (Equiv.refl n)
range_e₂ : LinearMap.range e₂ = ⊤
⊢ rank A = finrank R { x // x ∈ LinearMap.range (↑(toLin v₂ v₁) A) }
[PROOFSTEP]
refine' LinearEquiv.finrank_eq (e₁.ofSubmodules _ _ _)
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝⁷ : Fintype n
inst✝⁶ : Fintype o
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq n
M₁ : Type u_6
M₂ : Type u_7
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
A : Matrix m n R
v₁ : Basis m R M₁
v₂ : Basis n R M₂
e₁ : (m → R) ≃ₗ[R] M₁ := Basis.equiv (Pi.basisFun R m) v₁ (Equiv.refl m)
e₂ : (n → R) ≃ₗ[R] M₂ := Basis.equiv (Pi.basisFun R n) v₂ (Equiv.refl n)
range_e₂ : LinearMap.range e₂ = ⊤
⊢ Submodule.map (↑e₁) (LinearMap.range (mulVecLin A)) = LinearMap.range (↑(toLin v₂ v₁) A)
[PROOFSTEP]
rw [← LinearMap.range_comp, ← LinearMap.range_comp_of_range_eq_top (toLin v₂ v₁ A) range_e₂]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝⁷ : Fintype n
inst✝⁶ : Fintype o
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq n
M₁ : Type u_6
M₂ : Type u_7
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
A : Matrix m n R
v₁ : Basis m R M₁
v₂ : Basis n R M₂
e₁ : (m → R) ≃ₗ[R] M₁ := Basis.equiv (Pi.basisFun R m) v₁ (Equiv.refl m)
e₂ : (n → R) ≃ₗ[R] M₂ := Basis.equiv (Pi.basisFun R n) v₂ (Equiv.refl n)
range_e₂ : LinearMap.range e₂ = ⊤
⊢ LinearMap.range (LinearMap.comp (↑e₁) (mulVecLin A)) = LinearMap.range (LinearMap.comp (↑(toLin v₂ v₁) A) ↑e₂)
[PROOFSTEP]
congr 1
[GOAL]
case e_f
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝⁷ : Fintype n
inst✝⁶ : Fintype o
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq n
M₁ : Type u_6
M₂ : Type u_7
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
A : Matrix m n R
v₁ : Basis m R M₁
v₂ : Basis n R M₂
e₁ : (m → R) ≃ₗ[R] M₁ := Basis.equiv (Pi.basisFun R m) v₁ (Equiv.refl m)
e₂ : (n → R) ≃ₗ[R] M₂ := Basis.equiv (Pi.basisFun R n) v₂ (Equiv.refl n)
range_e₂ : LinearMap.range e₂ = ⊤
⊢ LinearMap.comp (↑e₁) (mulVecLin A) = LinearMap.comp (↑(toLin v₂ v₁) A) ↑e₂
[PROOFSTEP]
apply LinearMap.pi_ext'
[GOAL]
case e_f.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝⁷ : Fintype n
inst✝⁶ : Fintype o
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq n
M₁ : Type u_6
M₂ : Type u_7
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
A : Matrix m n R
v₁ : Basis m R M₁
v₂ : Basis n R M₂
e₁ : (m → R) ≃ₗ[R] M₁ := Basis.equiv (Pi.basisFun R m) v₁ (Equiv.refl m)
e₂ : (n → R) ≃ₗ[R] M₂ := Basis.equiv (Pi.basisFun R n) v₂ (Equiv.refl n)
range_e₂ : LinearMap.range e₂ = ⊤
⊢ ∀ (i : n),
    LinearMap.comp (LinearMap.comp (↑e₁) (mulVecLin A)) (LinearMap.single i) =
      LinearMap.comp (LinearMap.comp (↑(toLin v₂ v₁) A) ↑e₂) (LinearMap.single i)
[PROOFSTEP]
rintro i
[GOAL]
case e_f.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝⁷ : Fintype n
inst✝⁶ : Fintype o
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq n
M₁ : Type u_6
M₂ : Type u_7
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
A : Matrix m n R
v₁ : Basis m R M₁
v₂ : Basis n R M₂
e₁ : (m → R) ≃ₗ[R] M₁ := Basis.equiv (Pi.basisFun R m) v₁ (Equiv.refl m)
e₂ : (n → R) ≃ₗ[R] M₂ := Basis.equiv (Pi.basisFun R n) v₂ (Equiv.refl n)
range_e₂ : LinearMap.range e₂ = ⊤
i : n
⊢ LinearMap.comp (LinearMap.comp (↑e₁) (mulVecLin A)) (LinearMap.single i) =
    LinearMap.comp (LinearMap.comp (↑(toLin v₂ v₁) A) ↑e₂) (LinearMap.single i)
[PROOFSTEP]
apply LinearMap.ext_ring
[GOAL]
case e_f.h.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝⁷ : Fintype n
inst✝⁶ : Fintype o
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq n
M₁ : Type u_6
M₂ : Type u_7
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
A : Matrix m n R
v₁ : Basis m R M₁
v₂ : Basis n R M₂
e₁ : (m → R) ≃ₗ[R] M₁ := Basis.equiv (Pi.basisFun R m) v₁ (Equiv.refl m)
e₂ : (n → R) ≃ₗ[R] M₂ := Basis.equiv (Pi.basisFun R n) v₂ (Equiv.refl n)
range_e₂ : LinearMap.range e₂ = ⊤
i : n
⊢ ↑(LinearMap.comp (LinearMap.comp (↑e₁) (mulVecLin A)) (LinearMap.single i)) 1 =
    ↑(LinearMap.comp (LinearMap.comp (↑(toLin v₂ v₁) A) ↑e₂) (LinearMap.single i)) 1
[PROOFSTEP]
have aux₁ := toLin_self (Pi.basisFun R n) (Pi.basisFun R m) A i
[GOAL]
case e_f.h.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝⁷ : Fintype n
inst✝⁶ : Fintype o
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq n
M₁ : Type u_6
M₂ : Type u_7
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
A : Matrix m n R
v₁ : Basis m R M₁
v₂ : Basis n R M₂
e₁ : (m → R) ≃ₗ[R] M₁ := Basis.equiv (Pi.basisFun R m) v₁ (Equiv.refl m)
e₂ : (n → R) ≃ₗ[R] M₂ := Basis.equiv (Pi.basisFun R n) v₂ (Equiv.refl n)
range_e₂ : LinearMap.range e₂ = ⊤
i : n
aux₁ :
  ↑(↑(toLin (Pi.basisFun R n) (Pi.basisFun R m)) A) (↑(Pi.basisFun R n) i) =
    Finset.sum Finset.univ fun j => A j i • ↑(Pi.basisFun R m) j
⊢ ↑(LinearMap.comp (LinearMap.comp (↑e₁) (mulVecLin A)) (LinearMap.single i)) 1 =
    ↑(LinearMap.comp (LinearMap.comp (↑(toLin v₂ v₁) A) ↑e₂) (LinearMap.single i)) 1
[PROOFSTEP]
have aux₂ := Basis.equiv_apply (Pi.basisFun R n) i v₂
[GOAL]
case e_f.h.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝⁷ : Fintype n
inst✝⁶ : Fintype o
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq n
M₁ : Type u_6
M₂ : Type u_7
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
A : Matrix m n R
v₁ : Basis m R M₁
v₂ : Basis n R M₂
e₁ : (m → R) ≃ₗ[R] M₁ := Basis.equiv (Pi.basisFun R m) v₁ (Equiv.refl m)
e₂ : (n → R) ≃ₗ[R] M₂ := Basis.equiv (Pi.basisFun R n) v₂ (Equiv.refl n)
range_e₂ : LinearMap.range e₂ = ⊤
i : n
aux₁ :
  ↑(↑(toLin (Pi.basisFun R n) (Pi.basisFun R m)) A) (↑(Pi.basisFun R n) i) =
    Finset.sum Finset.univ fun j => A j i • ↑(Pi.basisFun R m) j
aux₂ : ∀ (e : n ≃ n), ↑(Basis.equiv (Pi.basisFun R n) v₂ e) (↑(Pi.basisFun R n) i) = ↑v₂ (↑e i)
⊢ ↑(LinearMap.comp (LinearMap.comp (↑e₁) (mulVecLin A)) (LinearMap.single i)) 1 =
    ↑(LinearMap.comp (LinearMap.comp (↑(toLin v₂ v₁) A) ↑e₂) (LinearMap.single i)) 1
[PROOFSTEP]
rw [toLin_eq_toLin', toLin'_apply'] at aux₁
[GOAL]
case e_f.h.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝⁷ : Fintype n
inst✝⁶ : Fintype o
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq n
M₁ : Type u_6
M₂ : Type u_7
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
A : Matrix m n R
v₁ : Basis m R M₁
v₂ : Basis n R M₂
e₁ : (m → R) ≃ₗ[R] M₁ := Basis.equiv (Pi.basisFun R m) v₁ (Equiv.refl m)
e₂ : (n → R) ≃ₗ[R] M₂ := Basis.equiv (Pi.basisFun R n) v₂ (Equiv.refl n)
range_e₂ : LinearMap.range e₂ = ⊤
i : n
aux₁ : ↑(mulVecLin A) (↑(Pi.basisFun R n) i) = Finset.sum Finset.univ fun j => A j i • ↑(Pi.basisFun R m) j
aux₂ : ∀ (e : n ≃ n), ↑(Basis.equiv (Pi.basisFun R n) v₂ e) (↑(Pi.basisFun R n) i) = ↑v₂ (↑e i)
⊢ ↑(LinearMap.comp (LinearMap.comp (↑e₁) (mulVecLin A)) (LinearMap.single i)) 1 =
    ↑(LinearMap.comp (LinearMap.comp (↑(toLin v₂ v₁) A) ↑e₂) (LinearMap.single i)) 1
[PROOFSTEP]
rw [Pi.basisFun_apply, LinearMap.coe_stdBasis] at aux₁ aux₂
[GOAL]
case e_f.h.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝⁷ : Fintype n
inst✝⁶ : Fintype o
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq n
M₁ : Type u_6
M₂ : Type u_7
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
A : Matrix m n R
v₁ : Basis m R M₁
v₂ : Basis n R M₂
e₁ : (m → R) ≃ₗ[R] M₁ := Basis.equiv (Pi.basisFun R m) v₁ (Equiv.refl m)
e₂ : (n → R) ≃ₗ[R] M₂ := Basis.equiv (Pi.basisFun R n) v₂ (Equiv.refl n)
range_e₂ : LinearMap.range e₂ = ⊤
i : n
aux₁ : ↑(mulVecLin A) (Pi.single i 1) = Finset.sum Finset.univ fun j => A j i • ↑(Pi.basisFun R m) j
aux₂ : ∀ (e : n ≃ n), ↑(Basis.equiv (Pi.basisFun R n) v₂ e) (Pi.single i 1) = ↑v₂ (↑e i)
⊢ ↑(LinearMap.comp (LinearMap.comp (↑e₁) (mulVecLin A)) (LinearMap.single i)) 1 =
    ↑(LinearMap.comp (LinearMap.comp (↑(toLin v₂ v₁) A) ↑e₂) (LinearMap.single i)) 1
[PROOFSTEP]
simp only [LinearMap.comp_apply, LinearEquiv.coe_coe, Equiv.refl_apply, aux₁, aux₂, LinearMap.coe_single, toLin_self,
  LinearEquiv.map_sum, LinearEquiv.map_smul, Basis.equiv_apply]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : CommRing R
inst✝ : StrongRankCondition R
A : Matrix m n R
⊢ rank A ≤ Fintype.card m
[PROOFSTEP]
haveI : Module.Finite R (m → R) := Module.Finite.pi
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : CommRing R
inst✝ : StrongRankCondition R
A : Matrix m n R
this : Module.Finite R (m → R)
⊢ rank A ≤ Fintype.card m
[PROOFSTEP]
haveI : Module.Free R (m → R) := Module.Free.pi _ _
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : CommRing R
inst✝ : StrongRankCondition R
A : Matrix m n R
this✝ : Module.Finite R (m → R)
this : Module.Free R (m → R)
⊢ rank A ≤ Fintype.card m
[PROOFSTEP]
exact (Submodule.finrank_le _).trans (finrank_pi R).le
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝² : Fintype n
inst✝¹ : Fintype o
inst✝ : CommRing R
A : Matrix m n R
⊢ rank A = finrank R { x // x ∈ Submodule.span R (Set.range Aᵀ) }
[PROOFSTEP]
rw [rank, Matrix.range_mulVecLin]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝⁴ : Fintype n
inst✝³ : Fintype o
inst✝² : Field R
inst✝¹ : DecidableEq m
inst✝ : DecidableEq R
w : m → R
⊢ rank (diagonal w) = Fintype.card { i // w i ≠ 0 }
[PROOFSTEP]
rw [Matrix.rank, ← Matrix.toLin'_apply', FiniteDimensional.finrank, ← LinearMap.rank, LinearMap.rank_diagonal,
  Cardinal.toNat_cast]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : Fintype o
inst✝³ : Fintype m
inst✝² : Field R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
A : Matrix m n R
⊢ LinearMap.ker (mulVecLin (Aᴴ * A)) = LinearMap.ker (mulVecLin A)
[PROOFSTEP]
ext x
[GOAL]
case h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : Fintype o
inst✝³ : Fintype m
inst✝² : Field R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
A : Matrix m n R
x : n → R
⊢ x ∈ LinearMap.ker (mulVecLin (Aᴴ * A)) ↔ x ∈ LinearMap.ker (mulVecLin A)
[PROOFSTEP]
simp only [LinearMap.mem_ker, mulVecLin_apply, conjTranspose_mul_self_mulVec_eq_zero]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : Fintype o
inst✝³ : Fintype m
inst✝² : Field R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
A : Matrix m n R
⊢ rank (Aᴴ * A) = rank A
[PROOFSTEP]
dsimp only [rank]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : Fintype o
inst✝³ : Fintype m
inst✝² : Field R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
A : Matrix m n R
⊢ finrank R { x // x ∈ LinearMap.range (mulVecLin (Aᴴ * A)) } = finrank R { x // x ∈ LinearMap.range (mulVecLin A) }
[PROOFSTEP]
refine' add_left_injective (finrank R (LinearMap.ker (mulVecLin A))) _
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : Fintype o
inst✝³ : Fintype m
inst✝² : Field R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
A : Matrix m n R
⊢ (fun x => x + finrank R { x // x ∈ LinearMap.ker (mulVecLin A) })
      (finrank R { x // x ∈ LinearMap.range (mulVecLin (Aᴴ * A)) }) =
    (fun x => x + finrank R { x // x ∈ LinearMap.ker (mulVecLin A) })
      (finrank R { x // x ∈ LinearMap.range (mulVecLin A) })
[PROOFSTEP]
dsimp only
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : Fintype o
inst✝³ : Fintype m
inst✝² : Field R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
A : Matrix m n R
⊢ finrank R { x // x ∈ LinearMap.range (mulVecLin (Aᴴ * A)) } + finrank R { x // x ∈ LinearMap.ker (mulVecLin A) } =
    finrank R { x // x ∈ LinearMap.range (mulVecLin A) } + finrank R { x // x ∈ LinearMap.ker (mulVecLin A) }
[PROOFSTEP]
trans
  finrank R { x // x ∈ LinearMap.range (mulVecLin (Aᴴ * A)) } +
    finrank R { x // x ∈ LinearMap.ker (mulVecLin (Aᴴ * A)) }
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : Fintype o
inst✝³ : Fintype m
inst✝² : Field R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
A : Matrix m n R
⊢ finrank R { x // x ∈ LinearMap.range (mulVecLin (Aᴴ * A)) } + finrank R { x // x ∈ LinearMap.ker (mulVecLin A) } =
    finrank R { x // x ∈ LinearMap.range (mulVecLin (Aᴴ * A)) } +
      finrank R { x // x ∈ LinearMap.ker (mulVecLin (Aᴴ * A)) }
[PROOFSTEP]
rw [ker_mulVecLin_conjTranspose_mul_self]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : Fintype o
inst✝³ : Fintype m
inst✝² : Field R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
A : Matrix m n R
⊢ finrank R { x // x ∈ LinearMap.range (mulVecLin (Aᴴ * A)) } +
      finrank R { x // x ∈ LinearMap.ker (mulVecLin (Aᴴ * A)) } =
    finrank R { x // x ∈ LinearMap.range (mulVecLin A) } + finrank R { x // x ∈ LinearMap.ker (mulVecLin A) }
[PROOFSTEP]
simp only [LinearMap.finrank_range_add_finrank_ker]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : Fintype o
inst✝³ : Fintype m
inst✝² : Field R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
A : Matrix m n R
⊢ rank (A * Aᴴ) = rank A
[PROOFSTEP]
simpa only [rank_conjTranspose, conjTranspose_conjTranspose] using rank_conjTranspose_mul_self Aᴴ
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : Fintype m
inst✝ : LinearOrderedField R
A : Matrix m n R
⊢ LinearMap.ker (mulVecLin (Aᵀ * A)) = LinearMap.ker (mulVecLin A)
[PROOFSTEP]
ext x
[GOAL]
case h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : Fintype m
inst✝ : LinearOrderedField R
A : Matrix m n R
x : n → R
⊢ x ∈ LinearMap.ker (mulVecLin (Aᵀ * A)) ↔ x ∈ LinearMap.ker (mulVecLin A)
[PROOFSTEP]
simp only [LinearMap.mem_ker, mulVecLin_apply, ← mulVec_mulVec]
[GOAL]
case h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : Fintype m
inst✝ : LinearOrderedField R
A : Matrix m n R
x : n → R
⊢ mulVec Aᵀ (mulVec A x) = 0 ↔ mulVec A x = 0
[PROOFSTEP]
constructor
[GOAL]
case h.mp
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : Fintype m
inst✝ : LinearOrderedField R
A : Matrix m n R
x : n → R
⊢ mulVec Aᵀ (mulVec A x) = 0 → mulVec A x = 0
[PROOFSTEP]
intro h
[GOAL]
case h.mp
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : Fintype m
inst✝ : LinearOrderedField R
A : Matrix m n R
x : n → R
h : mulVec Aᵀ (mulVec A x) = 0
⊢ mulVec A x = 0
[PROOFSTEP]
replace h := congr_arg (dotProduct x) h
[GOAL]
case h.mp
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : Fintype m
inst✝ : LinearOrderedField R
A : Matrix m n R
x : n → R
h : x ⬝ᵥ mulVec Aᵀ (mulVec A x) = x ⬝ᵥ 0
⊢ mulVec A x = 0
[PROOFSTEP]
rwa [dotProduct_mulVec, dotProduct_zero, vecMul_transpose, dotProduct_self_eq_zero] at h
[GOAL]
case h.mpr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : Fintype m
inst✝ : LinearOrderedField R
A : Matrix m n R
x : n → R
⊢ mulVec A x = 0 → mulVec Aᵀ (mulVec A x) = 0
[PROOFSTEP]
intro h
[GOAL]
case h.mpr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : Fintype m
inst✝ : LinearOrderedField R
A : Matrix m n R
x : n → R
h : mulVec A x = 0
⊢ mulVec Aᵀ (mulVec A x) = 0
[PROOFSTEP]
rw [h, mulVec_zero]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : Fintype m
inst✝ : LinearOrderedField R
A : Matrix m n R
⊢ rank (Aᵀ * A) = rank A
[PROOFSTEP]
dsimp only [rank]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : Fintype m
inst✝ : LinearOrderedField R
A : Matrix m n R
⊢ finrank R { x // x ∈ LinearMap.range (mulVecLin (Aᵀ * A)) } = finrank R { x // x ∈ LinearMap.range (mulVecLin A) }
[PROOFSTEP]
refine' add_left_injective (finrank R <| LinearMap.ker A.mulVecLin) _
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : Fintype m
inst✝ : LinearOrderedField R
A : Matrix m n R
⊢ (fun x => x + finrank R { x // x ∈ LinearMap.ker (mulVecLin A) })
      (finrank R { x // x ∈ LinearMap.range (mulVecLin (Aᵀ * A)) }) =
    (fun x => x + finrank R { x // x ∈ LinearMap.ker (mulVecLin A) })
      (finrank R { x // x ∈ LinearMap.range (mulVecLin A) })
[PROOFSTEP]
dsimp only
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : Fintype m
inst✝ : LinearOrderedField R
A : Matrix m n R
⊢ finrank R { x // x ∈ LinearMap.range (mulVecLin (Aᵀ * A)) } + finrank R { x // x ∈ LinearMap.ker (mulVecLin A) } =
    finrank R { x // x ∈ LinearMap.range (mulVecLin A) } + finrank R { x // x ∈ LinearMap.ker (mulVecLin A) }
[PROOFSTEP]
trans
  finrank R { x // x ∈ LinearMap.range (mulVecLin (Aᵀ * A)) } +
    finrank R { x // x ∈ LinearMap.ker (mulVecLin (Aᵀ * A)) }
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : Fintype m
inst✝ : LinearOrderedField R
A : Matrix m n R
⊢ finrank R { x // x ∈ LinearMap.range (mulVecLin (Aᵀ * A)) } + finrank R { x // x ∈ LinearMap.ker (mulVecLin A) } =
    finrank R { x // x ∈ LinearMap.range (mulVecLin (Aᵀ * A)) } +
      finrank R { x // x ∈ LinearMap.ker (mulVecLin (Aᵀ * A)) }
[PROOFSTEP]
rw [ker_mulVecLin_transpose_mul_self]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : Fintype m
inst✝ : LinearOrderedField R
A : Matrix m n R
⊢ finrank R { x // x ∈ LinearMap.range (mulVecLin (Aᵀ * A)) } +
      finrank R { x // x ∈ LinearMap.ker (mulVecLin (Aᵀ * A)) } =
    finrank R { x // x ∈ LinearMap.range (mulVecLin A) } + finrank R { x // x ∈ LinearMap.ker (mulVecLin A) }
[PROOFSTEP]
simp only [LinearMap.finrank_range_add_finrank_ker]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : Fintype m
inst✝ : LinearOrderedField R
A : Matrix m n R
⊢ rank (A * Aᵀ) = rank A
[PROOFSTEP]
simpa only [rank_transpose, transpose_transpose] using rank_transpose_mul_self Aᵀ
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : LinearOrderedField R
inst✝ : Finite m
A : Matrix m n R
⊢ rank A = finrank R { x // x ∈ Submodule.span R (Set.range A) }
[PROOFSTEP]
cases nonempty_fintype m
[GOAL]
case intro
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
m_fin : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : LinearOrderedField R
inst✝ : Finite m
A : Matrix m n R
val✝ : Fintype m
⊢ rank A = finrank R { x // x ∈ Submodule.span R (Set.range A) }
[PROOFSTEP]
rw [← rank_transpose, rank_eq_finrank_span_cols, transpose_transpose]