[GOAL]
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype m₁
inst✝⁹ : Fintype m₂
inst✝⁸ : Fintype n
inst✝⁷ : Fintype n₁
inst✝⁶ : Fintype n₂
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq m₁
inst✝³ : DecidableEq m₂
inst✝² : DecidableEq n
inst✝¹ : DecidableEq n₁
inst✝ : DecidableEq n₂
A : Matrix m (n₁ ⊕ n₂) R
⊢ fromColumns (toColumns₁ A) (toColumns₂ A) = A
[PROOFSTEP]
ext i (j | j)
[GOAL]
case a.h.inl
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype m₁
inst✝⁹ : Fintype m₂
inst✝⁸ : Fintype n
inst✝⁷ : Fintype n₁
inst✝⁶ : Fintype n₂
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq m₁
inst✝³ : DecidableEq m₂
inst✝² : DecidableEq n
inst✝¹ : DecidableEq n₁
inst✝ : DecidableEq n₂
A : Matrix m (n₁ ⊕ n₂) R
i : m
j : n₁
⊢ fromColumns (toColumns₁ A) (toColumns₂ A) i (Sum.inl j) = A i (Sum.inl j)
[PROOFSTEP]
simp
[GOAL]
case a.h.inr
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype m₁
inst✝⁹ : Fintype m₂
inst✝⁸ : Fintype n
inst✝⁷ : Fintype n₁
inst✝⁶ : Fintype n₂
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq m₁
inst✝³ : DecidableEq m₂
inst✝² : DecidableEq n
inst✝¹ : DecidableEq n₁
inst✝ : DecidableEq n₂
A : Matrix m (n₁ ⊕ n₂) R
i : m
j : n₂
⊢ fromColumns (toColumns₁ A) (toColumns₂ A) i (Sum.inr j) = A i (Sum.inr j)
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype m₁
inst✝⁹ : Fintype m₂
inst✝⁸ : Fintype n
inst✝⁷ : Fintype n₁
inst✝⁶ : Fintype n₂
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq m₁
inst✝³ : DecidableEq m₂
inst✝² : DecidableEq n
inst✝¹ : DecidableEq n₁
inst✝ : DecidableEq n₂
A : Matrix (m₁ ⊕ m₂) n R
⊢ fromRows (toRows₁ A) (toRows₂ A) = A
[PROOFSTEP]
ext (i | i) j
[GOAL]
case a.inl.h
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype m₁
inst✝⁹ : Fintype m₂
inst✝⁸ : Fintype n
inst✝⁷ : Fintype n₁
inst✝⁶ : Fintype n₂
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq m₁
inst✝³ : DecidableEq m₂
inst✝² : DecidableEq n
inst✝¹ : DecidableEq n₁
inst✝ : DecidableEq n₂
A : Matrix (m₁ ⊕ m₂) n R
i : m₁
j : n
⊢ fromRows (toRows₁ A) (toRows₂ A) (Sum.inl i) j = A (Sum.inl i) j
[PROOFSTEP]
simp
[GOAL]
case a.inr.h
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype m₁
inst✝⁹ : Fintype m₂
inst✝⁸ : Fintype n
inst✝⁷ : Fintype n₁
inst✝⁶ : Fintype n₂
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq m₁
inst✝³ : DecidableEq m₂
inst✝² : DecidableEq n
inst✝¹ : DecidableEq n₁
inst✝ : DecidableEq n₂
A : Matrix (m₁ ⊕ m₂) n R
i : m₂
j : n
⊢ fromRows (toRows₁ A) (toRows₂ A) (Sum.inr i) j = A (Sum.inr i) j
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype m₁
inst✝⁹ : Fintype m₂
inst✝⁸ : Fintype n
inst✝⁷ : Fintype n₁
inst✝⁶ : Fintype n₂
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq m₁
inst✝³ : DecidableEq m₂
inst✝² : DecidableEq n
inst✝¹ : DecidableEq n₁
inst✝ : DecidableEq n₂
⊢ Function.Injective2 fromRows
[PROOFSTEP]
intros x1 x2 y1 y2
[GOAL]
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype m₁
inst✝⁹ : Fintype m₂
inst✝⁸ : Fintype n
inst✝⁷ : Fintype n₁
inst✝⁶ : Fintype n₂
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq m₁
inst✝³ : DecidableEq m₂
inst✝² : DecidableEq n
inst✝¹ : DecidableEq n₁
inst✝ : DecidableEq n₂
x1 x2 : Matrix m₁ n R
y1 y2 : Matrix m₂ n R
⊢ fromRows x1 y1 = fromRows x2 y2 → x1 = x2 ∧ y1 = y2
[PROOFSTEP]
simp only [Function.funext_iff, ← Matrix.ext_iff]
[GOAL]
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype m₁
inst✝⁹ : Fintype m₂
inst✝⁸ : Fintype n
inst✝⁷ : Fintype n₁
inst✝⁶ : Fintype n₂
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq m₁
inst✝³ : DecidableEq m₂
inst✝² : DecidableEq n
inst✝¹ : DecidableEq n₁
inst✝ : DecidableEq n₂
x1 x2 : Matrix m₁ n R
y1 y2 : Matrix m₂ n R
⊢ (∀ (i : m₁ ⊕ m₂) (j : n), fromRows x1 y1 i j = fromRows x2 y2 i j) →
    (∀ (i : m₁) (j : n), x1 i j = x2 i j) ∧ ∀ (i : m₂) (j : n), y1 i j = y2 i j
[PROOFSTEP]
aesop
[GOAL]
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype m₁
inst✝⁹ : Fintype m₂
inst✝⁸ : Fintype n
inst✝⁷ : Fintype n₁
inst✝⁶ : Fintype n₂
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq m₁
inst✝³ : DecidableEq m₂
inst✝² : DecidableEq n
inst✝¹ : DecidableEq n₁
inst✝ : DecidableEq n₂
⊢ Function.Injective2 fromColumns
[PROOFSTEP]
intros x1 x2 y1 y2
[GOAL]
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype m₁
inst✝⁹ : Fintype m₂
inst✝⁸ : Fintype n
inst✝⁷ : Fintype n₁
inst✝⁶ : Fintype n₂
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq m₁
inst✝³ : DecidableEq m₂
inst✝² : DecidableEq n
inst✝¹ : DecidableEq n₁
inst✝ : DecidableEq n₂
x1 x2 : Matrix m n₁ R
y1 y2 : Matrix m n₂ R
⊢ fromColumns x1 y1 = fromColumns x2 y2 → x1 = x2 ∧ y1 = y2
[PROOFSTEP]
simp only [Function.funext_iff, ← Matrix.ext_iff]
[GOAL]
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype m₁
inst✝⁹ : Fintype m₂
inst✝⁸ : Fintype n
inst✝⁷ : Fintype n₁
inst✝⁶ : Fintype n₂
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq m₁
inst✝³ : DecidableEq m₂
inst✝² : DecidableEq n
inst✝¹ : DecidableEq n₁
inst✝ : DecidableEq n₂
x1 x2 : Matrix m n₁ R
y1 y2 : Matrix m n₂ R
⊢ (∀ (i : m) (j : n₁ ⊕ n₂), fromColumns x1 y1 i j = fromColumns x2 y2 i j) →
    (∀ (i : m) (j : n₁), x1 i j = x2 i j) ∧ ∀ (i : m) (j : n₂), y1 i j = y2 i j
[PROOFSTEP]
aesop
[GOAL]
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype m₁
inst✝⁹ : Fintype m₂
inst✝⁸ : Fintype n
inst✝⁷ : Fintype n₁
inst✝⁶ : Fintype n₂
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq m₁
inst✝³ : DecidableEq m₂
inst✝² : DecidableEq n
inst✝¹ : DecidableEq n₁
inst✝ : DecidableEq n₂
A₁ : Matrix m n₁ R
A₂ : Matrix m n₂ R
⊢ (fromColumns A₁ A₂)ᵀ = fromRows A₁ᵀ A₂ᵀ
[PROOFSTEP]
ext (i | i) j
[GOAL]
case a.inl.h
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype m₁
inst✝⁹ : Fintype m₂
inst✝⁸ : Fintype n
inst✝⁷ : Fintype n₁
inst✝⁶ : Fintype n₂
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq m₁
inst✝³ : DecidableEq m₂
inst✝² : DecidableEq n
inst✝¹ : DecidableEq n₁
inst✝ : DecidableEq n₂
A₁ : Matrix m n₁ R
A₂ : Matrix m n₂ R
i : n₁
j : m
⊢ (fromColumns A₁ A₂)ᵀ (Sum.inl i) j = fromRows A₁ᵀ A₂ᵀ (Sum.inl i) j
[PROOFSTEP]
simp
  /- A row partioned matrix when transposed gives a column partioned matrix with rows of the initial
  matrix tranposed to become columns. -/
[GOAL]
case a.inr.h
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype m₁
inst✝⁹ : Fintype m₂
inst✝⁸ : Fintype n
inst✝⁷ : Fintype n₁
inst✝⁶ : Fintype n₂
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq m₁
inst✝³ : DecidableEq m₂
inst✝² : DecidableEq n
inst✝¹ : DecidableEq n₁
inst✝ : DecidableEq n₂
A₁ : Matrix m n₁ R
A₂ : Matrix m n₂ R
i : n₂
j : m
⊢ (fromColumns A₁ A₂)ᵀ (Sum.inr i) j = fromRows A₁ᵀ A₂ᵀ (Sum.inr i) j
[PROOFSTEP]
simp
  /- A row partioned matrix when transposed gives a column partioned matrix with rows of the initial
  matrix tranposed to become columns. -/
[GOAL]
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype m₁
inst✝⁹ : Fintype m₂
inst✝⁸ : Fintype n
inst✝⁷ : Fintype n₁
inst✝⁶ : Fintype n₂
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq m₁
inst✝³ : DecidableEq m₂
inst✝² : DecidableEq n
inst✝¹ : DecidableEq n₁
inst✝ : DecidableEq n₂
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
⊢ (fromRows A₁ A₂)ᵀ = fromColumns A₁ᵀ A₂ᵀ
[PROOFSTEP]
ext i (j | j)
[GOAL]
case a.h.inl
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype m₁
inst✝⁹ : Fintype m₂
inst✝⁸ : Fintype n
inst✝⁷ : Fintype n₁
inst✝⁶ : Fintype n₂
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq m₁
inst✝³ : DecidableEq m₂
inst✝² : DecidableEq n
inst✝¹ : DecidableEq n₁
inst✝ : DecidableEq n₂
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
i : n
j : m₁
⊢ (fromRows A₁ A₂)ᵀ i (Sum.inl j) = fromColumns A₁ᵀ A₂ᵀ i (Sum.inl j)
[PROOFSTEP]
simp
[GOAL]
case a.h.inr
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype m₁
inst✝⁹ : Fintype m₂
inst✝⁸ : Fintype n
inst✝⁷ : Fintype n₁
inst✝⁶ : Fintype n₂
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq m₁
inst✝³ : DecidableEq m₂
inst✝² : DecidableEq n
inst✝¹ : DecidableEq n₁
inst✝ : DecidableEq n₂
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
i : n
j : m₂
⊢ (fromRows A₁ A₂)ᵀ i (Sum.inr j) = fromColumns A₁ᵀ A₂ᵀ i (Sum.inr j)
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹² : Fintype m
inst✝¹¹ : Fintype m₁
inst✝¹⁰ : Fintype m₂
inst✝⁹ : Fintype n
inst✝⁸ : Fintype n₁
inst✝⁷ : Fintype n₂
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq m₁
inst✝⁴ : DecidableEq m₂
inst✝³ : DecidableEq n
inst✝² : DecidableEq n₁
inst✝¹ : DecidableEq n₂
inst✝ : Semiring R
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
B : Matrix n m R
⊢ fromRows A₁ A₂ * B = fromRows (A₁ * B) (A₂ * B)
[PROOFSTEP]
ext (_ | _) _
[GOAL]
case a.inl.h
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹² : Fintype m
inst✝¹¹ : Fintype m₁
inst✝¹⁰ : Fintype m₂
inst✝⁹ : Fintype n
inst✝⁸ : Fintype n₁
inst✝⁷ : Fintype n₂
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq m₁
inst✝⁴ : DecidableEq m₂
inst✝³ : DecidableEq n
inst✝² : DecidableEq n₁
inst✝¹ : DecidableEq n₂
inst✝ : Semiring R
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
B : Matrix n m R
val✝ : m₁
x✝ : m
⊢ (fromRows A₁ A₂ * B) (Sum.inl val✝) x✝ = fromRows (A₁ * B) (A₂ * B) (Sum.inl val✝) x✝
[PROOFSTEP]
simp [mul_apply]
[GOAL]
case a.inr.h
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹² : Fintype m
inst✝¹¹ : Fintype m₁
inst✝¹⁰ : Fintype m₂
inst✝⁹ : Fintype n
inst✝⁸ : Fintype n₁
inst✝⁷ : Fintype n₂
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq m₁
inst✝⁴ : DecidableEq m₂
inst✝³ : DecidableEq n
inst✝² : DecidableEq n₁
inst✝¹ : DecidableEq n₂
inst✝ : Semiring R
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
B : Matrix n m R
val✝ : m₂
x✝ : m
⊢ (fromRows A₁ A₂ * B) (Sum.inr val✝) x✝ = fromRows (A₁ * B) (A₂ * B) (Sum.inr val✝) x✝
[PROOFSTEP]
simp [mul_apply]
[GOAL]
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹² : Fintype m
inst✝¹¹ : Fintype m₁
inst✝¹⁰ : Fintype m₂
inst✝⁹ : Fintype n
inst✝⁸ : Fintype n₁
inst✝⁷ : Fintype n₂
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq m₁
inst✝⁴ : DecidableEq m₂
inst✝³ : DecidableEq n
inst✝² : DecidableEq n₁
inst✝¹ : DecidableEq n₂
inst✝ : Semiring R
A : Matrix m n R
B₁ : Matrix n n₁ R
B₂ : Matrix n n₂ R
⊢ A * fromColumns B₁ B₂ = fromColumns (A * B₁) (A * B₂)
[PROOFSTEP]
ext _ (_ | _)
[GOAL]
case a.h.inl
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹² : Fintype m
inst✝¹¹ : Fintype m₁
inst✝¹⁰ : Fintype m₂
inst✝⁹ : Fintype n
inst✝⁸ : Fintype n₁
inst✝⁷ : Fintype n₂
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq m₁
inst✝⁴ : DecidableEq m₂
inst✝³ : DecidableEq n
inst✝² : DecidableEq n₁
inst✝¹ : DecidableEq n₂
inst✝ : Semiring R
A : Matrix m n R
B₁ : Matrix n n₁ R
B₂ : Matrix n n₂ R
i✝ : m
val✝ : n₁
⊢ (A * fromColumns B₁ B₂) i✝ (Sum.inl val✝) = fromColumns (A * B₁) (A * B₂) i✝ (Sum.inl val✝)
[PROOFSTEP]
simp [mul_apply]
[GOAL]
case a.h.inr
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹² : Fintype m
inst✝¹¹ : Fintype m₁
inst✝¹⁰ : Fintype m₂
inst✝⁹ : Fintype n
inst✝⁸ : Fintype n₁
inst✝⁷ : Fintype n₂
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq m₁
inst✝⁴ : DecidableEq m₂
inst✝³ : DecidableEq n
inst✝² : DecidableEq n₁
inst✝¹ : DecidableEq n₂
inst✝ : Semiring R
A : Matrix m n R
B₁ : Matrix n n₁ R
B₂ : Matrix n n₂ R
i✝ : m
val✝ : n₂
⊢ (A * fromColumns B₁ B₂) i✝ (Sum.inr val✝) = fromColumns (A * B₁) (A * B₂) i✝ (Sum.inr val✝)
[PROOFSTEP]
simp [mul_apply]
[GOAL]
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹² : Fintype m
inst✝¹¹ : Fintype m₁
inst✝¹⁰ : Fintype m₂
inst✝⁹ : Fintype n
inst✝⁸ : Fintype n₁
inst✝⁷ : Fintype n₂
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq m₁
inst✝⁴ : DecidableEq m₂
inst✝³ : DecidableEq n
inst✝² : DecidableEq n₁
inst✝¹ : DecidableEq n₂
inst✝ : Semiring R
⊢ fromRows 0 0 = 0
[PROOFSTEP]
ext (_ | _) _
[GOAL]
case a.inl.h
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹² : Fintype m
inst✝¹¹ : Fintype m₁
inst✝¹⁰ : Fintype m₂
inst✝⁹ : Fintype n
inst✝⁸ : Fintype n₁
inst✝⁷ : Fintype n₂
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq m₁
inst✝⁴ : DecidableEq m₂
inst✝³ : DecidableEq n
inst✝² : DecidableEq n₁
inst✝¹ : DecidableEq n₂
inst✝ : Semiring R
val✝ : m₁
x✝ : n
⊢ fromRows 0 0 (Sum.inl val✝) x✝ = OfNat.ofNat 0 (Sum.inl val✝) x✝
[PROOFSTEP]
simp
[GOAL]
case a.inr.h
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹² : Fintype m
inst✝¹¹ : Fintype m₁
inst✝¹⁰ : Fintype m₂
inst✝⁹ : Fintype n
inst✝⁸ : Fintype n₁
inst✝⁷ : Fintype n₂
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq m₁
inst✝⁴ : DecidableEq m₂
inst✝³ : DecidableEq n
inst✝² : DecidableEq n₁
inst✝¹ : DecidableEq n₂
inst✝ : Semiring R
val✝ : m₂
x✝ : n
⊢ fromRows 0 0 (Sum.inr val✝) x✝ = OfNat.ofNat 0 (Sum.inr val✝) x✝
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹² : Fintype m
inst✝¹¹ : Fintype m₁
inst✝¹⁰ : Fintype m₂
inst✝⁹ : Fintype n
inst✝⁸ : Fintype n₁
inst✝⁷ : Fintype n₂
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq m₁
inst✝⁴ : DecidableEq m₂
inst✝³ : DecidableEq n
inst✝² : DecidableEq n₁
inst✝¹ : DecidableEq n₂
inst✝ : Semiring R
⊢ fromColumns 0 0 = 0
[PROOFSTEP]
ext _ (_ | _)
[GOAL]
case a.h.inl
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹² : Fintype m
inst✝¹¹ : Fintype m₁
inst✝¹⁰ : Fintype m₂
inst✝⁹ : Fintype n
inst✝⁸ : Fintype n₁
inst✝⁷ : Fintype n₂
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq m₁
inst✝⁴ : DecidableEq m₂
inst✝³ : DecidableEq n
inst✝² : DecidableEq n₁
inst✝¹ : DecidableEq n₂
inst✝ : Semiring R
i✝ : m
val✝ : n₁
⊢ fromColumns 0 0 i✝ (Sum.inl val✝) = OfNat.ofNat 0 i✝ (Sum.inl val✝)
[PROOFSTEP]
simp
[GOAL]
case a.h.inr
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹² : Fintype m
inst✝¹¹ : Fintype m₁
inst✝¹⁰ : Fintype m₂
inst✝⁹ : Fintype n
inst✝⁸ : Fintype n₁
inst✝⁷ : Fintype n₂
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq m₁
inst✝⁴ : DecidableEq m₂
inst✝³ : DecidableEq n
inst✝² : DecidableEq n₁
inst✝¹ : DecidableEq n₂
inst✝ : Semiring R
i✝ : m
val✝ : n₂
⊢ fromColumns 0 0 i✝ (Sum.inr val✝) = OfNat.ofNat 0 i✝ (Sum.inr val✝)
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹² : Fintype m
inst✝¹¹ : Fintype m₁
inst✝¹⁰ : Fintype m₂
inst✝⁹ : Fintype n
inst✝⁸ : Fintype n₁
inst✝⁷ : Fintype n₂
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq m₁
inst✝⁴ : DecidableEq m₂
inst✝³ : DecidableEq n
inst✝² : DecidableEq n₁
inst✝¹ : DecidableEq n₂
inst✝ : Semiring R
B₁₁ : Matrix m₁ n₁ R
B₁₂ : Matrix m₁ n₂ R
B₂₁ : Matrix m₂ n₁ R
B₂₂ : Matrix m₂ n₂ R
⊢ fromColumns (fromRows B₁₁ B₂₁) (fromRows B₁₂ B₂₂) = fromBlocks B₁₁ B₁₂ B₂₁ B₂₂
[PROOFSTEP]
ext (_ | _) (_ | _)
[GOAL]
case a.inl.h.inl
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹² : Fintype m
inst✝¹¹ : Fintype m₁
inst✝¹⁰ : Fintype m₂
inst✝⁹ : Fintype n
inst✝⁸ : Fintype n₁
inst✝⁷ : Fintype n₂
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq m₁
inst✝⁴ : DecidableEq m₂
inst✝³ : DecidableEq n
inst✝² : DecidableEq n₁
inst✝¹ : DecidableEq n₂
inst✝ : Semiring R
B₁₁ : Matrix m₁ n₁ R
B₁₂ : Matrix m₁ n₂ R
B₂₁ : Matrix m₂ n₁ R
B₂₂ : Matrix m₂ n₂ R
val✝¹ : m₁
val✝ : n₁
⊢ fromColumns (fromRows B₁₁ B₂₁) (fromRows B₁₂ B₂₂) (Sum.inl val✝¹) (Sum.inl val✝) =
    fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ (Sum.inl val✝¹) (Sum.inl val✝)
[PROOFSTEP]
simp
[GOAL]
case a.inl.h.inr
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹² : Fintype m
inst✝¹¹ : Fintype m₁
inst✝¹⁰ : Fintype m₂
inst✝⁹ : Fintype n
inst✝⁸ : Fintype n₁
inst✝⁷ : Fintype n₂
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq m₁
inst✝⁴ : DecidableEq m₂
inst✝³ : DecidableEq n
inst✝² : DecidableEq n₁
inst✝¹ : DecidableEq n₂
inst✝ : Semiring R
B₁₁ : Matrix m₁ n₁ R
B₁₂ : Matrix m₁ n₂ R
B₂₁ : Matrix m₂ n₁ R
B₂₂ : Matrix m₂ n₂ R
val✝¹ : m₁
val✝ : n₂
⊢ fromColumns (fromRows B₁₁ B₂₁) (fromRows B₁₂ B₂₂) (Sum.inl val✝¹) (Sum.inr val✝) =
    fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ (Sum.inl val✝¹) (Sum.inr val✝)
[PROOFSTEP]
simp
[GOAL]
case a.inr.h.inl
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹² : Fintype m
inst✝¹¹ : Fintype m₁
inst✝¹⁰ : Fintype m₂
inst✝⁹ : Fintype n
inst✝⁸ : Fintype n₁
inst✝⁷ : Fintype n₂
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq m₁
inst✝⁴ : DecidableEq m₂
inst✝³ : DecidableEq n
inst✝² : DecidableEq n₁
inst✝¹ : DecidableEq n₂
inst✝ : Semiring R
B₁₁ : Matrix m₁ n₁ R
B₁₂ : Matrix m₁ n₂ R
B₂₁ : Matrix m₂ n₁ R
B₂₂ : Matrix m₂ n₂ R
val✝¹ : m₂
val✝ : n₁
⊢ fromColumns (fromRows B₁₁ B₂₁) (fromRows B₁₂ B₂₂) (Sum.inr val✝¹) (Sum.inl val✝) =
    fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ (Sum.inr val✝¹) (Sum.inl val✝)
[PROOFSTEP]
simp
[GOAL]
case a.inr.h.inr
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹² : Fintype m
inst✝¹¹ : Fintype m₁
inst✝¹⁰ : Fintype m₂
inst✝⁹ : Fintype n
inst✝⁸ : Fintype n₁
inst✝⁷ : Fintype n₂
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq m₁
inst✝⁴ : DecidableEq m₂
inst✝³ : DecidableEq n
inst✝² : DecidableEq n₁
inst✝¹ : DecidableEq n₂
inst✝ : Semiring R
B₁₁ : Matrix m₁ n₁ R
B₁₂ : Matrix m₁ n₂ R
B₂₁ : Matrix m₂ n₁ R
B₂₂ : Matrix m₂ n₂ R
val✝¹ : m₂
val✝ : n₂
⊢ fromColumns (fromRows B₁₁ B₂₁) (fromRows B₁₂ B₂₂) (Sum.inr val✝¹) (Sum.inr val✝) =
    fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ (Sum.inr val✝¹) (Sum.inr val✝)
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹² : Fintype m
inst✝¹¹ : Fintype m₁
inst✝¹⁰ : Fintype m₂
inst✝⁹ : Fintype n
inst✝⁸ : Fintype n₁
inst✝⁷ : Fintype n₂
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq m₁
inst✝⁴ : DecidableEq m₂
inst✝³ : DecidableEq n
inst✝² : DecidableEq n₁
inst✝¹ : DecidableEq n₂
inst✝ : Semiring R
B₁₁ : Matrix m₁ n₁ R
B₁₂ : Matrix m₁ n₂ R
B₂₁ : Matrix m₂ n₁ R
B₂₂ : Matrix m₂ n₂ R
⊢ fromRows (fromColumns B₁₁ B₁₂) (fromColumns B₂₁ B₂₂) = fromBlocks B₁₁ B₁₂ B₂₁ B₂₂
[PROOFSTEP]
ext (_ | _) (_ | _)
[GOAL]
case a.inl.h.inl
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹² : Fintype m
inst✝¹¹ : Fintype m₁
inst✝¹⁰ : Fintype m₂
inst✝⁹ : Fintype n
inst✝⁸ : Fintype n₁
inst✝⁷ : Fintype n₂
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq m₁
inst✝⁴ : DecidableEq m₂
inst✝³ : DecidableEq n
inst✝² : DecidableEq n₁
inst✝¹ : DecidableEq n₂
inst✝ : Semiring R
B₁₁ : Matrix m₁ n₁ R
B₁₂ : Matrix m₁ n₂ R
B₂₁ : Matrix m₂ n₁ R
B₂₂ : Matrix m₂ n₂ R
val✝¹ : m₁
val✝ : n₁
⊢ fromRows (fromColumns B₁₁ B₁₂) (fromColumns B₂₁ B₂₂) (Sum.inl val✝¹) (Sum.inl val✝) =
    fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ (Sum.inl val✝¹) (Sum.inl val✝)
[PROOFSTEP]
simp
[GOAL]
case a.inl.h.inr
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹² : Fintype m
inst✝¹¹ : Fintype m₁
inst✝¹⁰ : Fintype m₂
inst✝⁹ : Fintype n
inst✝⁸ : Fintype n₁
inst✝⁷ : Fintype n₂
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq m₁
inst✝⁴ : DecidableEq m₂
inst✝³ : DecidableEq n
inst✝² : DecidableEq n₁
inst✝¹ : DecidableEq n₂
inst✝ : Semiring R
B₁₁ : Matrix m₁ n₁ R
B₁₂ : Matrix m₁ n₂ R
B₂₁ : Matrix m₂ n₁ R
B₂₂ : Matrix m₂ n₂ R
val✝¹ : m₁
val✝ : n₂
⊢ fromRows (fromColumns B₁₁ B₁₂) (fromColumns B₂₁ B₂₂) (Sum.inl val✝¹) (Sum.inr val✝) =
    fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ (Sum.inl val✝¹) (Sum.inr val✝)
[PROOFSTEP]
simp
[GOAL]
case a.inr.h.inl
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹² : Fintype m
inst✝¹¹ : Fintype m₁
inst✝¹⁰ : Fintype m₂
inst✝⁹ : Fintype n
inst✝⁸ : Fintype n₁
inst✝⁷ : Fintype n₂
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq m₁
inst✝⁴ : DecidableEq m₂
inst✝³ : DecidableEq n
inst✝² : DecidableEq n₁
inst✝¹ : DecidableEq n₂
inst✝ : Semiring R
B₁₁ : Matrix m₁ n₁ R
B₁₂ : Matrix m₁ n₂ R
B₂₁ : Matrix m₂ n₁ R
B₂₂ : Matrix m₂ n₂ R
val✝¹ : m₂
val✝ : n₁
⊢ fromRows (fromColumns B₁₁ B₁₂) (fromColumns B₂₁ B₂₂) (Sum.inr val✝¹) (Sum.inl val✝) =
    fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ (Sum.inr val✝¹) (Sum.inl val✝)
[PROOFSTEP]
simp
[GOAL]
case a.inr.h.inr
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹² : Fintype m
inst✝¹¹ : Fintype m₁
inst✝¹⁰ : Fintype m₂
inst✝⁹ : Fintype n
inst✝⁸ : Fintype n₁
inst✝⁷ : Fintype n₂
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq m₁
inst✝⁴ : DecidableEq m₂
inst✝³ : DecidableEq n
inst✝² : DecidableEq n₁
inst✝¹ : DecidableEq n₂
inst✝ : Semiring R
B₁₁ : Matrix m₁ n₁ R
B₁₂ : Matrix m₁ n₂ R
B₂₁ : Matrix m₂ n₁ R
B₂₂ : Matrix m₂ n₂ R
val✝¹ : m₂
val✝ : n₂
⊢ fromRows (fromColumns B₁₁ B₁₂) (fromColumns B₂₁ B₂₂) (Sum.inr val✝¹) (Sum.inr val✝) =
    fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ (Sum.inr val✝¹) (Sum.inr val✝)
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹² : Fintype m
inst✝¹¹ : Fintype m₁
inst✝¹⁰ : Fintype m₂
inst✝⁹ : Fintype n
inst✝⁸ : Fintype n₁
inst✝⁷ : Fintype n₂
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq m₁
inst✝⁴ : DecidableEq m₂
inst✝³ : DecidableEq n
inst✝² : DecidableEq n₁
inst✝¹ : DecidableEq n₂
inst✝ : Semiring R
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
B₁ : Matrix n n₁ R
B₂ : Matrix n n₂ R
⊢ fromRows A₁ A₂ * fromColumns B₁ B₂ = fromBlocks (A₁ * B₁) (A₁ * B₂) (A₂ * B₁) (A₂ * B₂)
[PROOFSTEP]
ext (_ | _) (_ | _)
[GOAL]
case a.inl.h.inl
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹² : Fintype m
inst✝¹¹ : Fintype m₁
inst✝¹⁰ : Fintype m₂
inst✝⁹ : Fintype n
inst✝⁸ : Fintype n₁
inst✝⁷ : Fintype n₂
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq m₁
inst✝⁴ : DecidableEq m₂
inst✝³ : DecidableEq n
inst✝² : DecidableEq n₁
inst✝¹ : DecidableEq n₂
inst✝ : Semiring R
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
B₁ : Matrix n n₁ R
B₂ : Matrix n n₂ R
val✝¹ : m₁
val✝ : n₁
⊢ (fromRows A₁ A₂ * fromColumns B₁ B₂) (Sum.inl val✝¹) (Sum.inl val✝) =
    fromBlocks (A₁ * B₁) (A₁ * B₂) (A₂ * B₁) (A₂ * B₂) (Sum.inl val✝¹) (Sum.inl val✝)
[PROOFSTEP]
simp
[GOAL]
case a.inl.h.inr
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹² : Fintype m
inst✝¹¹ : Fintype m₁
inst✝¹⁰ : Fintype m₂
inst✝⁹ : Fintype n
inst✝⁸ : Fintype n₁
inst✝⁷ : Fintype n₂
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq m₁
inst✝⁴ : DecidableEq m₂
inst✝³ : DecidableEq n
inst✝² : DecidableEq n₁
inst✝¹ : DecidableEq n₂
inst✝ : Semiring R
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
B₁ : Matrix n n₁ R
B₂ : Matrix n n₂ R
val✝¹ : m₁
val✝ : n₂
⊢ (fromRows A₁ A₂ * fromColumns B₁ B₂) (Sum.inl val✝¹) (Sum.inr val✝) =
    fromBlocks (A₁ * B₁) (A₁ * B₂) (A₂ * B₁) (A₂ * B₂) (Sum.inl val✝¹) (Sum.inr val✝)
[PROOFSTEP]
simp
[GOAL]
case a.inr.h.inl
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹² : Fintype m
inst✝¹¹ : Fintype m₁
inst✝¹⁰ : Fintype m₂
inst✝⁹ : Fintype n
inst✝⁸ : Fintype n₁
inst✝⁷ : Fintype n₂
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq m₁
inst✝⁴ : DecidableEq m₂
inst✝³ : DecidableEq n
inst✝² : DecidableEq n₁
inst✝¹ : DecidableEq n₂
inst✝ : Semiring R
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
B₁ : Matrix n n₁ R
B₂ : Matrix n n₂ R
val✝¹ : m₂
val✝ : n₁
⊢ (fromRows A₁ A₂ * fromColumns B₁ B₂) (Sum.inr val✝¹) (Sum.inl val✝) =
    fromBlocks (A₁ * B₁) (A₁ * B₂) (A₂ * B₁) (A₂ * B₂) (Sum.inr val✝¹) (Sum.inl val✝)
[PROOFSTEP]
simp
[GOAL]
case a.inr.h.inr
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹² : Fintype m
inst✝¹¹ : Fintype m₁
inst✝¹⁰ : Fintype m₂
inst✝⁹ : Fintype n
inst✝⁸ : Fintype n₁
inst✝⁷ : Fintype n₂
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq m₁
inst✝⁴ : DecidableEq m₂
inst✝³ : DecidableEq n
inst✝² : DecidableEq n₁
inst✝¹ : DecidableEq n₂
inst✝ : Semiring R
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
B₁ : Matrix n n₁ R
B₂ : Matrix n n₂ R
val✝¹ : m₂
val✝ : n₂
⊢ (fromRows A₁ A₂ * fromColumns B₁ B₂) (Sum.inr val✝¹) (Sum.inr val✝) =
    fromBlocks (A₁ * B₁) (A₁ * B₂) (A₂ * B₁) (A₂ * B₂) (Sum.inr val✝¹) (Sum.inr val✝)
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹² : Fintype m
inst✝¹¹ : Fintype m₁
inst✝¹⁰ : Fintype m₂
inst✝⁹ : Fintype n
inst✝⁸ : Fintype n₁
inst✝⁷ : Fintype n₂
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq m₁
inst✝⁴ : DecidableEq m₂
inst✝³ : DecidableEq n
inst✝² : DecidableEq n₁
inst✝¹ : DecidableEq n₂
inst✝ : Semiring R
A₁ : Matrix m n₁ R
A₂ : Matrix m n₂ R
B₁ : Matrix n₁ n R
B₂ : Matrix n₂ n R
⊢ fromColumns A₁ A₂ * fromRows B₁ B₂ = A₁ * B₁ + A₂ * B₂
[PROOFSTEP]
ext
[GOAL]
case a.h
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹² : Fintype m
inst✝¹¹ : Fintype m₁
inst✝¹⁰ : Fintype m₂
inst✝⁹ : Fintype n
inst✝⁸ : Fintype n₁
inst✝⁷ : Fintype n₂
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq m₁
inst✝⁴ : DecidableEq m₂
inst✝³ : DecidableEq n
inst✝² : DecidableEq n₁
inst✝¹ : DecidableEq n₂
inst✝ : Semiring R
A₁ : Matrix m n₁ R
A₂ : Matrix m n₂ R
B₁ : Matrix n₁ n R
B₂ : Matrix n₂ n R
i✝ : m
x✝ : n
⊢ (fromColumns A₁ A₂ * fromRows B₁ B₂) i✝ x✝ = (A₁ * B₁ + A₂ * B₂) i✝ x✝
[PROOFSTEP]
simp [mul_apply]
[GOAL]
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹² : Fintype m
inst✝¹¹ : Fintype m₁
inst✝¹⁰ : Fintype m₂
inst✝⁹ : Fintype n
inst✝⁸ : Fintype n₁
inst✝⁷ : Fintype n₂
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq m₁
inst✝⁴ : DecidableEq m₂
inst✝³ : DecidableEq n
inst✝² : DecidableEq n₁
inst✝¹ : DecidableEq n₂
inst✝ : Semiring R
A₁ : Matrix m m₁ R
A₂ : Matrix m m₂ R
B₁₁ : Matrix m₁ n₁ R
B₁₂ : Matrix m₁ n₂ R
B₂₁ : Matrix m₂ n₁ R
B₂₂ : Matrix m₂ n₂ R
⊢ fromColumns A₁ A₂ * fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ = fromColumns (A₁ * B₁₁ + A₂ * B₂₁) (A₁ * B₁₂ + A₂ * B₂₂)
[PROOFSTEP]
ext _ (_ | _)
[GOAL]
case a.h.inl
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹² : Fintype m
inst✝¹¹ : Fintype m₁
inst✝¹⁰ : Fintype m₂
inst✝⁹ : Fintype n
inst✝⁸ : Fintype n₁
inst✝⁷ : Fintype n₂
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq m₁
inst✝⁴ : DecidableEq m₂
inst✝³ : DecidableEq n
inst✝² : DecidableEq n₁
inst✝¹ : DecidableEq n₂
inst✝ : Semiring R
A₁ : Matrix m m₁ R
A₂ : Matrix m m₂ R
B₁₁ : Matrix m₁ n₁ R
B₁₂ : Matrix m₁ n₂ R
B₂₁ : Matrix m₂ n₁ R
B₂₂ : Matrix m₂ n₂ R
i✝ : m
val✝ : n₁
⊢ (fromColumns A₁ A₂ * fromBlocks B₁₁ B₁₂ B₂₁ B₂₂) i✝ (Sum.inl val✝) =
    fromColumns (A₁ * B₁₁ + A₂ * B₂₁) (A₁ * B₁₂ + A₂ * B₂₂) i✝ (Sum.inl val✝)
[PROOFSTEP]
simp [mul_apply]
[GOAL]
case a.h.inr
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹² : Fintype m
inst✝¹¹ : Fintype m₁
inst✝¹⁰ : Fintype m₂
inst✝⁹ : Fintype n
inst✝⁸ : Fintype n₁
inst✝⁷ : Fintype n₂
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq m₁
inst✝⁴ : DecidableEq m₂
inst✝³ : DecidableEq n
inst✝² : DecidableEq n₁
inst✝¹ : DecidableEq n₂
inst✝ : Semiring R
A₁ : Matrix m m₁ R
A₂ : Matrix m m₂ R
B₁₁ : Matrix m₁ n₁ R
B₁₂ : Matrix m₁ n₂ R
B₂₁ : Matrix m₂ n₁ R
B₂₂ : Matrix m₂ n₂ R
i✝ : m
val✝ : n₂
⊢ (fromColumns A₁ A₂ * fromBlocks B₁₁ B₁₂ B₂₁ B₂₂) i✝ (Sum.inr val✝) =
    fromColumns (A₁ * B₁₁ + A₂ * B₂₁) (A₁ * B₁₂ + A₂ * B₂₂) i✝ (Sum.inr val✝)
[PROOFSTEP]
simp [mul_apply]
[GOAL]
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹² : Fintype m
inst✝¹¹ : Fintype m₁
inst✝¹⁰ : Fintype m₂
inst✝⁹ : Fintype n
inst✝⁸ : Fintype n₁
inst✝⁷ : Fintype n₂
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq m₁
inst✝⁴ : DecidableEq m₂
inst✝³ : DecidableEq n
inst✝² : DecidableEq n₁
inst✝¹ : DecidableEq n₂
inst✝ : Semiring R
A₁ : Matrix n₁ n R
A₂ : Matrix n₂ n R
B₁₁ : Matrix m₁ n₁ R
B₁₂ : Matrix m₁ n₂ R
B₂₁ : Matrix m₂ n₁ R
B₂₂ : Matrix m₂ n₂ R
⊢ fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ * fromRows A₁ A₂ = fromRows (B₁₁ * A₁ + B₁₂ * A₂) (B₂₁ * A₁ + B₂₂ * A₂)
[PROOFSTEP]
ext (_ | _) _
[GOAL]
case a.inl.h
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹² : Fintype m
inst✝¹¹ : Fintype m₁
inst✝¹⁰ : Fintype m₂
inst✝⁹ : Fintype n
inst✝⁸ : Fintype n₁
inst✝⁷ : Fintype n₂
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq m₁
inst✝⁴ : DecidableEq m₂
inst✝³ : DecidableEq n
inst✝² : DecidableEq n₁
inst✝¹ : DecidableEq n₂
inst✝ : Semiring R
A₁ : Matrix n₁ n R
A₂ : Matrix n₂ n R
B₁₁ : Matrix m₁ n₁ R
B₁₂ : Matrix m₁ n₂ R
B₂₁ : Matrix m₂ n₁ R
B₂₂ : Matrix m₂ n₂ R
val✝ : m₁
x✝ : n
⊢ (fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ * fromRows A₁ A₂) (Sum.inl val✝) x✝ =
    fromRows (B₁₁ * A₁ + B₁₂ * A₂) (B₂₁ * A₁ + B₂₂ * A₂) (Sum.inl val✝) x✝
[PROOFSTEP]
simp [mul_apply]
[GOAL]
case a.inr.h
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹² : Fintype m
inst✝¹¹ : Fintype m₁
inst✝¹⁰ : Fintype m₂
inst✝⁹ : Fintype n
inst✝⁸ : Fintype n₁
inst✝⁷ : Fintype n₂
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq m₁
inst✝⁴ : DecidableEq m₂
inst✝³ : DecidableEq n
inst✝² : DecidableEq n₁
inst✝¹ : DecidableEq n₂
inst✝ : Semiring R
A₁ : Matrix n₁ n R
A₂ : Matrix n₂ n R
B₁₁ : Matrix m₁ n₁ R
B₁₂ : Matrix m₁ n₂ R
B₂₁ : Matrix m₂ n₁ R
B₂₂ : Matrix m₂ n₂ R
val✝ : m₂
x✝ : n
⊢ (fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ * fromRows A₁ A₂) (Sum.inr val✝) x✝ =
    fromRows (B₁₁ * A₁ + B₁₂ * A₂) (B₂₁ * A₁ + B₂₂ * A₂) (Sum.inr val✝) x✝
[PROOFSTEP]
simp [mul_apply]
[GOAL]
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹² : Fintype m
inst✝¹¹ : Fintype m₁
inst✝¹⁰ : Fintype m₂
inst✝⁹ : Fintype n
inst✝⁸ : Fintype n₁
inst✝⁷ : Fintype n₂
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq m₁
inst✝⁴ : DecidableEq m₂
inst✝³ : DecidableEq n
inst✝² : DecidableEq n₁
inst✝¹ : DecidableEq n₂
inst✝ : CommRing R
e : n ≃ n₁ ⊕ n₂
A₁ : Matrix n n₁ R
A₂ : Matrix n n₂ R
B₁ : Matrix n₁ n R
B₂ : Matrix n₂ n R
⊢ fromColumns A₁ A₂ * fromRows B₁ B₂ = 1 ↔ fromRows B₁ B₂ * fromColumns A₁ A₂ = 1
[PROOFSTEP]
calc
  fromColumns A₁ A₂ * fromRows B₁ B₂ = 1
  _ ↔ submatrix (fromColumns A₁ A₂) id e * submatrix (fromRows B₁ B₂) e id = 1 := by simp
  _ ↔ submatrix (fromRows B₁ B₂) e id * submatrix (fromColumns A₁ A₂) id e = 1 := mul_eq_one_comm
  _ ↔ reindex e.symm e.symm (fromRows B₁ B₂ * fromColumns A₁ A₂) = reindex e.symm e.symm 1 := by
    simp only [reindex_apply, Equiv.symm_symm, submatrix_one_equiv, submatrix_mul (he₂ := Function.bijective_id)]
  _ ↔ fromRows B₁ B₂ * fromColumns A₁ A₂ = 1 := (reindex _ _).injective.eq_iff
[GOAL]
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹² : Fintype m
inst✝¹¹ : Fintype m₁
inst✝¹⁰ : Fintype m₂
inst✝⁹ : Fintype n
inst✝⁸ : Fintype n₁
inst✝⁷ : Fintype n₂
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq m₁
inst✝⁴ : DecidableEq m₂
inst✝³ : DecidableEq n
inst✝² : DecidableEq n₁
inst✝¹ : DecidableEq n₂
inst✝ : CommRing R
e : n ≃ n₁ ⊕ n₂
A₁ : Matrix n n₁ R
A₂ : Matrix n n₂ R
B₁ : Matrix n₁ n R
B₂ : Matrix n₂ n R
⊢ fromColumns A₁ A₂ * fromRows B₁ B₂ = 1 ↔ submatrix (fromColumns A₁ A₂) id ↑e * submatrix (fromRows B₁ B₂) (↑e) id = 1
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹² : Fintype m
inst✝¹¹ : Fintype m₁
inst✝¹⁰ : Fintype m₂
inst✝⁹ : Fintype n
inst✝⁸ : Fintype n₁
inst✝⁷ : Fintype n₂
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq m₁
inst✝⁴ : DecidableEq m₂
inst✝³ : DecidableEq n
inst✝² : DecidableEq n₁
inst✝¹ : DecidableEq n₂
inst✝ : CommRing R
e : n ≃ n₁ ⊕ n₂
A₁ : Matrix n n₁ R
A₂ : Matrix n n₂ R
B₁ : Matrix n₁ n R
B₂ : Matrix n₂ n R
⊢ submatrix (fromRows B₁ B₂) (↑e) id * submatrix (fromColumns A₁ A₂) id ↑e = 1 ↔
    ↑(reindex e.symm e.symm) (fromRows B₁ B₂ * fromColumns A₁ A₂) = ↑(reindex e.symm e.symm) 1
[PROOFSTEP]
simp only [reindex_apply, Equiv.symm_symm, submatrix_one_equiv, submatrix_mul (he₂ := Function.bijective_id)]
[GOAL]
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹² : Fintype m
inst✝¹¹ : Fintype m₁
inst✝¹⁰ : Fintype m₂
inst✝⁹ : Fintype n
inst✝⁸ : Fintype n₁
inst✝⁷ : Fintype n₂
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq m₁
inst✝⁴ : DecidableEq m₂
inst✝³ : DecidableEq n
inst✝² : DecidableEq n₁
inst✝¹ : DecidableEq n₂
inst✝ : Star R
A₁ : Matrix m n₁ R
A₂ : Matrix m n₂ R
⊢ (fromColumns A₁ A₂)ᴴ = fromRows A₁ᴴ A₂ᴴ
[PROOFSTEP]
ext (_ | _) _
[GOAL]
case a.inl.h
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹² : Fintype m
inst✝¹¹ : Fintype m₁
inst✝¹⁰ : Fintype m₂
inst✝⁹ : Fintype n
inst✝⁸ : Fintype n₁
inst✝⁷ : Fintype n₂
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq m₁
inst✝⁴ : DecidableEq m₂
inst✝³ : DecidableEq n
inst✝² : DecidableEq n₁
inst✝¹ : DecidableEq n₂
inst✝ : Star R
A₁ : Matrix m n₁ R
A₂ : Matrix m n₂ R
val✝ : n₁
x✝ : m
⊢ (fromColumns A₁ A₂)ᴴ (Sum.inl val✝) x✝ = fromRows A₁ᴴ A₂ᴴ (Sum.inl val✝) x✝
[PROOFSTEP]
simp
  /- A row partioned matrix in a Star ring when conjugate transposed gives a column partitioned matrix
  with the rows of the initial matrix conjugate transposed to become columns. -/
[GOAL]
case a.inr.h
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹² : Fintype m
inst✝¹¹ : Fintype m₁
inst✝¹⁰ : Fintype m₂
inst✝⁹ : Fintype n
inst✝⁸ : Fintype n₁
inst✝⁷ : Fintype n₂
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq m₁
inst✝⁴ : DecidableEq m₂
inst✝³ : DecidableEq n
inst✝² : DecidableEq n₁
inst✝¹ : DecidableEq n₂
inst✝ : Star R
A₁ : Matrix m n₁ R
A₂ : Matrix m n₂ R
val✝ : n₂
x✝ : m
⊢ (fromColumns A₁ A₂)ᴴ (Sum.inr val✝) x✝ = fromRows A₁ᴴ A₂ᴴ (Sum.inr val✝) x✝
[PROOFSTEP]
simp
  /- A row partioned matrix in a Star ring when conjugate transposed gives a column partitioned matrix
  with the rows of the initial matrix conjugate transposed to become columns. -/
[GOAL]
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹² : Fintype m
inst✝¹¹ : Fintype m₁
inst✝¹⁰ : Fintype m₂
inst✝⁹ : Fintype n
inst✝⁸ : Fintype n₁
inst✝⁷ : Fintype n₂
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq m₁
inst✝⁴ : DecidableEq m₂
inst✝³ : DecidableEq n
inst✝² : DecidableEq n₁
inst✝¹ : DecidableEq n₂
inst✝ : Star R
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
⊢ (fromRows A₁ A₂)ᴴ = fromColumns A₁ᴴ A₂ᴴ
[PROOFSTEP]
ext _ (_ | _)
[GOAL]
case a.h.inl
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹² : Fintype m
inst✝¹¹ : Fintype m₁
inst✝¹⁰ : Fintype m₂
inst✝⁹ : Fintype n
inst✝⁸ : Fintype n₁
inst✝⁷ : Fintype n₂
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq m₁
inst✝⁴ : DecidableEq m₂
inst✝³ : DecidableEq n
inst✝² : DecidableEq n₁
inst✝¹ : DecidableEq n₂
inst✝ : Star R
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
i✝ : n
val✝ : m₁
⊢ (fromRows A₁ A₂)ᴴ i✝ (Sum.inl val✝) = fromColumns A₁ᴴ A₂ᴴ i✝ (Sum.inl val✝)
[PROOFSTEP]
simp
[GOAL]
case a.h.inr
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹² : Fintype m
inst✝¹¹ : Fintype m₁
inst✝¹⁰ : Fintype m₂
inst✝⁹ : Fintype n
inst✝⁸ : Fintype n₁
inst✝⁷ : Fintype n₂
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq m₁
inst✝⁴ : DecidableEq m₂
inst✝³ : DecidableEq n
inst✝² : DecidableEq n₁
inst✝¹ : DecidableEq n₂
inst✝ : Star R
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
i✝ : n
val✝ : m₂
⊢ (fromRows A₁ A₂)ᴴ i✝ (Sum.inr val✝) = fromColumns A₁ᴴ A₂ᴴ i✝ (Sum.inr val✝)
[PROOFSTEP]
simp


[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
inst✝ : PartialOrder α
F : CFilter α σ
E : σ ≃ τ
f : σ → α
p : σ
g : σ → σ → σ
h₁ : ∀ (a b : σ), f (g a b) ≤ f a
h₂ : ∀ (a b : σ), f (g a b) ≤ f b
a b : τ
⊢ (fun a => f (↑E.symm a)) ((fun a b => ↑E (g (↑E.symm a) (↑E.symm b))) a b) ≤ (fun a => f (↑E.symm a)) a
[PROOFSTEP]
simpa using h₁ (E.symm a) (E.symm b)
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
inst✝ : PartialOrder α
F : CFilter α σ
E : σ ≃ τ
f : σ → α
p : σ
g : σ → σ → σ
h₁ : ∀ (a b : σ), f (g a b) ≤ f a
h₂ : ∀ (a b : σ), f (g a b) ≤ f b
a b : τ
⊢ (fun a => f (↑E.symm a)) ((fun a b => ↑E (g (↑E.symm a) (↑E.symm b))) a b) ≤ (fun a => f (↑E.symm a)) b
[PROOFSTEP]
simpa using h₂ (E.symm a) (E.symm b)
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
inst✝ : PartialOrder α
F✝ : CFilter α σ
E : σ ≃ τ
F : CFilter α σ
a : τ
⊢ f (ofEquiv E F) a = f F (↑E.symm a)
[PROOFSTEP]
cases F
[GOAL]
case mk
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
inst✝ : PartialOrder α
F : CFilter α σ
E : σ ≃ τ
a : τ
f✝ : σ → α
pt✝ : σ
inf✝ : σ → σ → σ
inf_le_left✝ : ∀ (a b : σ), f✝ (inf✝ a b) ≤ f✝ a
inf_le_right✝ : ∀ (a b : σ), f✝ (inf✝ a b) ≤ f✝ b
⊢ f (ofEquiv E { f := f✝, pt := pt✝, inf := inf✝, inf_le_left := inf_le_left✝, inf_le_right := inf_le_right✝ }) a =
    f { f := f✝, pt := pt✝, inf := inf✝, inf_le_left := inf_le_left✝, inf_le_right := inf_le_right✝ } (↑E.symm a)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f : Filter α
F : Realizer f
a : Set α
⊢ a ∈ f ↔ ∃ b, CFilter.f F.F b ⊆ a
[PROOFSTEP]
cases F
[GOAL]
case mk
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f : Filter α
a : Set α
σ✝ : Type u_5
F✝ : CFilter (Set α) σ✝
eq✝ : CFilter.toFilter F✝ = f
⊢ a ∈ f ↔ ∃ b, CFilter.f { σ := σ✝, F := F✝, eq := eq✝ }.F b ⊆ a
[PROOFSTEP]
subst f
[GOAL]
case mk
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
a : Set α
σ✝ : Type u_5
F✝ : CFilter (Set α) σ✝
⊢ a ∈ CFilter.toFilter F✝ ↔
    ∃ b, CFilter.f { σ := σ✝, F := F✝, eq := (_ : CFilter.toFilter F✝ = CFilter.toFilter F✝) }.F b ⊆ a
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f : Filter α
x✝ : Set α
⊢ x✝ ∈
      (CFilter.toFilter
          { f := Subtype.val, pt := { val := univ, property := (_ : univ ∈ f) },
            inf := fun x x_1 =>
              match x with
              | { val := val, property := h₁ } =>
                match x_1 with
                | { val := val_1, property := h₂ } => { val := val ∩ val_1, property := (_ : val ∩ val_1 ∈ f) },
            inf_le_left :=
              (_ :
                ∀ (x x_1 : ↑f.sets),
                  ↑((fun x x_2 =>
                          match x with
                          | { val := val, property := h₁ } =>
                            match x_2 with
                            | { val := val_1, property := h₂ } =>
                              { val := val ∩ val_1, property := (_ : val ∩ val_1 ∈ f) })
                        x x_1) ≤
                    ↑x),
            inf_le_right :=
              (_ :
                ∀ (x x_1 : ↑f.sets),
                  ↑((fun x x_2 =>
                          match x with
                          | { val := val, property := h₁ } =>
                            match x_2 with
                            | { val := val_1, property := h₂ } =>
                              { val := val ∩ val_1, property := (_ : val ∩ val_1 ∈ f) })
                        x x_1) ≤
                    ↑x_1) }).sets ↔
    x✝ ∈ f.sets
[PROOFSTEP]
simp [exists_mem_subset_iff]
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f : Filter α
F : Realizer f
E : F.σ ≃ τ
⊢ CFilter.toFilter (CFilter.ofEquiv E F.F) = f
[PROOFSTEP]
refine' Eq.trans _ F.eq
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f : Filter α
F : Realizer f
E : F.σ ≃ τ
⊢ CFilter.toFilter (CFilter.ofEquiv E F.F) = CFilter.toFilter F.F
[PROOFSTEP]
exact filter_eq (Set.ext fun _ ↦ ⟨fun ⟨s, h⟩ ↦ ⟨E.symm s, by simpa using h⟩, fun ⟨t, h⟩ ↦ ⟨E t, by simp [h]⟩⟩)
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f : Filter α
F : Realizer f
E : F.σ ≃ τ
x✝¹ : Set α
x✝ : x✝¹ ∈ (CFilter.toFilter (CFilter.ofEquiv E F.F)).sets
s : τ
h : CFilter.f (CFilter.ofEquiv E F.F) s ⊆ x✝¹
⊢ CFilter.f F.F (↑E.symm s) ⊆ x✝¹
[PROOFSTEP]
simpa using h
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f : Filter α
F : Realizer f
E : F.σ ≃ τ
x✝¹ : Set α
x✝ : x✝¹ ∈ (CFilter.toFilter F.F).sets
t : F.σ
h : CFilter.f F.F t ⊆ x✝¹
⊢ CFilter.f (CFilter.ofEquiv E F.F) (↑E t) ⊆ x✝¹
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
m : α → β
f : Filter α
F : Realizer f
x✝ : Set β
⊢ x✝ ∈
      (CFilter.toFilter
          { f := fun s => m '' CFilter.f F.F s, pt := F.F.pt, inf := F.F.inf,
            inf_le_left := (_ : ∀ (x x_1 : F.σ), m '' CFilter.f F.F (CFilter.inf F.F x x_1) ⊆ m '' CFilter.f F.F x),
            inf_le_right :=
              (_ : ∀ (x x_1 : F.σ), m '' CFilter.f F.F (CFilter.inf F.F x x_1) ⊆ m '' CFilter.f F.F x_1) }).sets ↔
    x✝ ∈ (map m f).sets
[PROOFSTEP]
simp only [CFilter.toFilter, image_subset_iff, mem_setOf_eq, Filter.mem_sets, mem_map]
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
m : α → β
f : Filter α
F : Realizer f
x✝ : Set β
⊢ (∃ b, CFilter.f F.F b ⊆ m ⁻¹' x✝) ↔ m ⁻¹' x✝ ∈ f
[PROOFSTEP]
rw [F.mem_sets]
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
m : α → β
f : Filter β
F : Realizer f
x✝ : Set α
⊢ x✝ ∈
      (CFilter.toFilter
          { f := fun s => m ⁻¹' CFilter.f F.F s, pt := F.F.pt, inf := F.F.inf,
            inf_le_left := (_ : ∀ (x x_1 : F.σ), m ⁻¹' CFilter.f F.F (CFilter.inf F.F x x_1) ⊆ m ⁻¹' CFilter.f F.F x),
            inf_le_right :=
              (_ : ∀ (x x_1 : F.σ), m ⁻¹' CFilter.f F.F (CFilter.inf F.F x x_1) ⊆ m ⁻¹' CFilter.f F.F x_1) }).sets ↔
    x✝ ∈ (comap m f).sets
[PROOFSTEP]
cases F
[GOAL]
case mk
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
m : α → β
f : Filter β
x✝ : Set α
σ✝ : Type ?u.20076
F✝ : CFilter (Set β) σ✝
eq✝ : CFilter.toFilter F✝ = f
⊢ x✝ ∈
      (CFilter.toFilter
          { f := fun s => m ⁻¹' CFilter.f { σ := σ✝, F := F✝, eq := eq✝ }.F s,
            pt := { σ := σ✝, F := F✝, eq := eq✝ }.F.pt, inf := { σ := σ✝, F := F✝, eq := eq✝ }.F.inf,
            inf_le_left :=
              (_ :
                ∀ (x x_1 : { σ := σ✝, F := F✝, eq := eq✝ }.σ),
                  m ⁻¹'
                      CFilter.f { σ := σ✝, F := F✝, eq := eq✝ }.F
                        (CFilter.inf { σ := σ✝, F := F✝, eq := eq✝ }.F x x_1) ⊆
                    m ⁻¹' CFilter.f { σ := σ✝, F := F✝, eq := eq✝ }.F x),
            inf_le_right :=
              (_ :
                ∀ (x x_1 : { σ := σ✝, F := F✝, eq := eq✝ }.σ),
                  m ⁻¹'
                      CFilter.f { σ := σ✝, F := F✝, eq := eq✝ }.F
                        (CFilter.inf { σ := σ✝, F := F✝, eq := eq✝ }.F x x_1) ⊆
                    m ⁻¹' CFilter.f { σ := σ✝, F := F✝, eq := eq✝ }.F x_1) }).sets ↔
    x✝ ∈ (comap m f).sets
[PROOFSTEP]
subst f
[GOAL]
case mk
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
m : α → β
x✝ : Set α
σ✝ : Type ?u.20076
F✝ : CFilter (Set β) σ✝
⊢ x✝ ∈
      (CFilter.toFilter
          {
            f := fun s =>
              m ⁻¹' CFilter.f { σ := σ✝, F := F✝, eq := (_ : CFilter.toFilter F✝ = CFilter.toFilter F✝) }.F s,
            pt := { σ := σ✝, F := F✝, eq := (_ : CFilter.toFilter F✝ = CFilter.toFilter F✝) }.F.pt,
            inf := { σ := σ✝, F := F✝, eq := (_ : CFilter.toFilter F✝ = CFilter.toFilter F✝) }.F.inf,
            inf_le_left :=
              (_ :
                ∀ (x x_1 : { σ := σ✝, F := F✝, eq := (_ : CFilter.toFilter F✝ = CFilter.toFilter F✝) }.σ),
                  m ⁻¹'
                      CFilter.f { σ := σ✝, F := F✝, eq := (_ : CFilter.toFilter F✝ = CFilter.toFilter F✝) }.F
                        (CFilter.inf { σ := σ✝, F := F✝, eq := (_ : CFilter.toFilter F✝ = CFilter.toFilter F✝) }.F x
                          x_1) ⊆
                    m ⁻¹' CFilter.f { σ := σ✝, F := F✝, eq := (_ : CFilter.toFilter F✝ = CFilter.toFilter F✝) }.F x),
            inf_le_right :=
              (_ :
                ∀ (x x_1 : { σ := σ✝, F := F✝, eq := (_ : CFilter.toFilter F✝ = CFilter.toFilter F✝) }.σ),
                  m ⁻¹'
                      CFilter.f { σ := σ✝, F := F✝, eq := (_ : CFilter.toFilter F✝ = CFilter.toFilter F✝) }.F
                        (CFilter.inf { σ := σ✝, F := F✝, eq := (_ : CFilter.toFilter F✝ = CFilter.toFilter F✝) }.F x
                          x_1) ⊆
                    m ⁻¹'
                      CFilter.f { σ := σ✝, F := F✝, eq := (_ : CFilter.toFilter F✝ = CFilter.toFilter F✝) }.F
                        x_1) }).sets ↔
    x✝ ∈ (comap m (CFilter.toFilter F✝)).sets
[PROOFSTEP]
exact ⟨fun ⟨s, h⟩ ↦ ⟨_, ⟨s, Subset.refl _⟩, h⟩, fun ⟨_, ⟨s, h⟩, h₂⟩ ↦ ⟨s, Subset.trans (preimage_mono h) h₂⟩⟩
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f g : Filter α
F : Realizer f
G : Realizer g
x✝ : Set α
⊢ x✝ ∈
      (CFilter.toFilter
          {
            f := fun x =>
              match x with
              | (s, t) => CFilter.f F.F s ∪ CFilter.f G.F t,
            pt := (F.F.pt, G.F.pt),
            inf := fun x x_1 =>
              match x with
              | (a, a') =>
                match x_1 with
                | (b, b') => (CFilter.inf F.F a b, CFilter.inf G.F a' b'),
            inf_le_left :=
              (_ :
                ∀ (x x_1 : F.σ × G.σ),
                  CFilter.f F.F (CFilter.inf F.F x.fst x_1.fst) ∪ CFilter.f G.F (CFilter.inf G.F x.snd x_1.snd) ⊆
                    CFilter.f F.F x.fst ∪ CFilter.f G.F x.snd),
            inf_le_right :=
              (_ :
                ∀ (x x_1 : F.σ × G.σ),
                  CFilter.f F.F (CFilter.inf F.F x.fst x_1.fst) ∪ CFilter.f G.F (CFilter.inf G.F x.snd x_1.snd) ⊆
                    CFilter.f F.F x_1.fst ∪ CFilter.f G.F x_1.snd) }).sets ↔
    x✝ ∈ (f ⊔ g).sets
[PROOFSTEP]
cases F
[GOAL]
case mk
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f g : Filter α
G : Realizer g
x✝ : Set α
σ✝ : Type ?u.22357
F✝ : CFilter (Set α) σ✝
eq✝ : CFilter.toFilter F✝ = f
⊢ x✝ ∈
      (CFilter.toFilter
          {
            f := fun x =>
              match x with
              | (s, t) => CFilter.f { σ := σ✝, F := F✝, eq := eq✝ }.F s ∪ CFilter.f G.F t,
            pt := ({ σ := σ✝, F := F✝, eq := eq✝ }.F.pt, G.F.pt),
            inf := fun x x_1 =>
              match x with
              | (a, a') =>
                match x_1 with
                | (b, b') => (CFilter.inf { σ := σ✝, F := F✝, eq := eq✝ }.F a b, CFilter.inf G.F a' b'),
            inf_le_left :=
              (_ :
                ∀ (x x_1 : { σ := σ✝, F := F✝, eq := eq✝ }.σ × G.σ),
                  CFilter.f { σ := σ✝, F := F✝, eq := eq✝ }.F
                        (CFilter.inf { σ := σ✝, F := F✝, eq := eq✝ }.F x.fst x_1.fst) ∪
                      CFilter.f G.F (CFilter.inf G.F x.snd x_1.snd) ⊆
                    CFilter.f { σ := σ✝, F := F✝, eq := eq✝ }.F x.fst ∪ CFilter.f G.F x.snd),
            inf_le_right :=
              (_ :
                ∀ (x x_1 : { σ := σ✝, F := F✝, eq := eq✝ }.σ × G.σ),
                  CFilter.f { σ := σ✝, F := F✝, eq := eq✝ }.F
                        (CFilter.inf { σ := σ✝, F := F✝, eq := eq✝ }.F x.fst x_1.fst) ∪
                      CFilter.f G.F (CFilter.inf G.F x.snd x_1.snd) ⊆
                    CFilter.f { σ := σ✝, F := F✝, eq := eq✝ }.F x_1.fst ∪ CFilter.f G.F x_1.snd) }).sets ↔
    x✝ ∈ (f ⊔ g).sets
[PROOFSTEP]
cases G
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f g : Filter α
x✝ : Set α
σ✝¹ : Type ?u.22357
F✝¹ : CFilter (Set α) σ✝¹
eq✝¹ : CFilter.toFilter F✝¹ = f
σ✝ : Type ?u.22412
F✝ : CFilter (Set α) σ✝
eq✝ : CFilter.toFilter F✝ = g
⊢ x✝ ∈
      (CFilter.toFilter
          {
            f := fun x =>
              match x with
              | (s, t) =>
                CFilter.f { σ := σ✝¹, F := F✝¹, eq := eq✝¹ }.F s ∪ CFilter.f { σ := σ✝, F := F✝, eq := eq✝ }.F t,
            pt := ({ σ := σ✝¹, F := F✝¹, eq := eq✝¹ }.F.pt, { σ := σ✝, F := F✝, eq := eq✝ }.F.pt),
            inf := fun x x_1 =>
              match x with
              | (a, a') =>
                match x_1 with
                | (b, b') =>
                  (CFilter.inf { σ := σ✝¹, F := F✝¹, eq := eq✝¹ }.F a b,
                    CFilter.inf { σ := σ✝, F := F✝, eq := eq✝ }.F a' b'),
            inf_le_left :=
              (_ :
                ∀ (x x_1 : { σ := σ✝¹, F := F✝¹, eq := eq✝¹ }.σ × { σ := σ✝, F := F✝, eq := eq✝ }.σ),
                  CFilter.f { σ := σ✝¹, F := F✝¹, eq := eq✝¹ }.F
                        (CFilter.inf { σ := σ✝¹, F := F✝¹, eq := eq✝¹ }.F x.fst x_1.fst) ∪
                      CFilter.f { σ := σ✝, F := F✝, eq := eq✝ }.F
                        (CFilter.inf { σ := σ✝, F := F✝, eq := eq✝ }.F x.snd x_1.snd) ⊆
                    CFilter.f { σ := σ✝¹, F := F✝¹, eq := eq✝¹ }.F x.fst ∪
                      CFilter.f { σ := σ✝, F := F✝, eq := eq✝ }.F x.snd),
            inf_le_right :=
              (_ :
                ∀ (x x_1 : { σ := σ✝¹, F := F✝¹, eq := eq✝¹ }.σ × { σ := σ✝, F := F✝, eq := eq✝ }.σ),
                  CFilter.f { σ := σ✝¹, F := F✝¹, eq := eq✝¹ }.F
                        (CFilter.inf { σ := σ✝¹, F := F✝¹, eq := eq✝¹ }.F x.fst x_1.fst) ∪
                      CFilter.f { σ := σ✝, F := F✝, eq := eq✝ }.F
                        (CFilter.inf { σ := σ✝, F := F✝, eq := eq✝ }.F x.snd x_1.snd) ⊆
                    CFilter.f { σ := σ✝¹, F := F✝¹, eq := eq✝¹ }.F x_1.fst ∪
                      CFilter.f { σ := σ✝, F := F✝, eq := eq✝ }.F x_1.snd) }).sets ↔
    x✝ ∈ (f ⊔ g).sets
[PROOFSTEP]
substs f g
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
x✝ : Set α
σ✝¹ : Type ?u.22357
F✝¹ : CFilter (Set α) σ✝¹
σ✝ : Type ?u.22412
F✝ : CFilter (Set α) σ✝
⊢ x✝ ∈
      (CFilter.toFilter
          {
            f := fun x =>
              match x with
              | (s, t) =>
                CFilter.f { σ := σ✝¹, F := F✝¹, eq := (_ : CFilter.toFilter F✝¹ = CFilter.toFilter F✝¹) }.F s ∪
                  CFilter.f { σ := σ✝, F := F✝, eq := (_ : CFilter.toFilter F✝ = CFilter.toFilter F✝) }.F t,
            pt :=
              ({ σ := σ✝¹, F := F✝¹, eq := (_ : CFilter.toFilter F✝¹ = CFilter.toFilter F✝¹) }.F.pt,
                { σ := σ✝, F := F✝, eq := (_ : CFilter.toFilter F✝ = CFilter.toFilter F✝) }.F.pt),
            inf := fun x x_1 =>
              match x with
              | (a, a') =>
                match x_1 with
                | (b, b') =>
                  (CFilter.inf { σ := σ✝¹, F := F✝¹, eq := (_ : CFilter.toFilter F✝¹ = CFilter.toFilter F✝¹) }.F a b,
                    CFilter.inf { σ := σ✝, F := F✝, eq := (_ : CFilter.toFilter F✝ = CFilter.toFilter F✝) }.F a' b'),
            inf_le_left :=
              (_ :
                ∀
                  (x x_1 :
                    { σ := σ✝¹, F := F✝¹, eq := (_ : CFilter.toFilter F✝¹ = CFilter.toFilter F✝¹) }.σ ×
                      { σ := σ✝, F := F✝, eq := (_ : CFilter.toFilter F✝ = CFilter.toFilter F✝) }.σ),
                  CFilter.f { σ := σ✝¹, F := F✝¹, eq := (_ : CFilter.toFilter F✝¹ = CFilter.toFilter F✝¹) }.F
                        (CFilter.inf { σ := σ✝¹, F := F✝¹, eq := (_ : CFilter.toFilter F✝¹ = CFilter.toFilter F✝¹) }.F
                          x.fst x_1.fst) ∪
                      CFilter.f { σ := σ✝, F := F✝, eq := (_ : CFilter.toFilter F✝ = CFilter.toFilter F✝) }.F
                        (CFilter.inf { σ := σ✝, F := F✝, eq := (_ : CFilter.toFilter F✝ = CFilter.toFilter F✝) }.F x.snd
                          x_1.snd) ⊆
                    CFilter.f { σ := σ✝¹, F := F✝¹, eq := (_ : CFilter.toFilter F✝¹ = CFilter.toFilter F✝¹) }.F x.fst ∪
                      CFilter.f { σ := σ✝, F := F✝, eq := (_ : CFilter.toFilter F✝ = CFilter.toFilter F✝) }.F x.snd),
            inf_le_right :=
              (_ :
                ∀
                  (x x_1 :
                    { σ := σ✝¹, F := F✝¹, eq := (_ : CFilter.toFilter F✝¹ = CFilter.toFilter F✝¹) }.σ ×
                      { σ := σ✝, F := F✝, eq := (_ : CFilter.toFilter F✝ = CFilter.toFilter F✝) }.σ),
                  CFilter.f { σ := σ✝¹, F := F✝¹, eq := (_ : CFilter.toFilter F✝¹ = CFilter.toFilter F✝¹) }.F
                        (CFilter.inf { σ := σ✝¹, F := F✝¹, eq := (_ : CFilter.toFilter F✝¹ = CFilter.toFilter F✝¹) }.F
                          x.fst x_1.fst) ∪
                      CFilter.f { σ := σ✝, F := F✝, eq := (_ : CFilter.toFilter F✝ = CFilter.toFilter F✝) }.F
                        (CFilter.inf { σ := σ✝, F := F✝, eq := (_ : CFilter.toFilter F✝ = CFilter.toFilter F✝) }.F x.snd
                          x_1.snd) ⊆
                    CFilter.f { σ := σ✝¹, F := F✝¹, eq := (_ : CFilter.toFilter F✝¹ = CFilter.toFilter F✝¹) }.F
                        x_1.fst ∪
                      CFilter.f { σ := σ✝, F := F✝, eq := (_ : CFilter.toFilter F✝ = CFilter.toFilter F✝) }.F
                        x_1.snd) }).sets ↔
    x✝ ∈ (CFilter.toFilter F✝¹ ⊔ CFilter.toFilter F✝).sets
[PROOFSTEP]
simp [CFilter.toFilter]
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f g : Filter α
F : Realizer f
G : Realizer g
⊢ CFilter.toFilter
      {
        f := fun x =>
          match x with
          | (s, t) => CFilter.f F.F s ∩ CFilter.f G.F t,
        pt := (F.F.pt, G.F.pt),
        inf := fun x x_1 =>
          match x with
          | (a, a') =>
            match x_1 with
            | (b, b') => (CFilter.inf F.F a b, CFilter.inf G.F a' b'),
        inf_le_left :=
          (_ :
            ∀ (x x_1 : F.σ × G.σ),
              CFilter.f F.F (CFilter.inf F.F x.fst x_1.fst) ∩ CFilter.f G.F (CFilter.inf G.F x.snd x_1.snd) ⊆
                CFilter.f F.F x.fst ∩ CFilter.f G.F x.snd),
        inf_le_right :=
          (_ :
            ∀ (x x_1 : F.σ × G.σ),
              CFilter.f F.F (CFilter.inf F.F x.fst x_1.fst) ∩ CFilter.f G.F (CFilter.inf G.F x.snd x_1.snd) ⊆
                CFilter.f F.F x_1.fst ∩ CFilter.f G.F x_1.snd) } =
    f ⊓ g
[PROOFSTEP]
cases F
[GOAL]
case mk
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f g : Filter α
G : Realizer g
σ✝ : Type ?u.34651
F✝ : CFilter (Set α) σ✝
eq✝ : CFilter.toFilter F✝ = f
⊢ CFilter.toFilter
      {
        f := fun x =>
          match x with
          | (s, t) => CFilter.f { σ := σ✝, F := F✝, eq := eq✝ }.F s ∩ CFilter.f G.F t,
        pt := ({ σ := σ✝, F := F✝, eq := eq✝ }.F.pt, G.F.pt),
        inf := fun x x_1 =>
          match x with
          | (a, a') =>
            match x_1 with
            | (b, b') => (CFilter.inf { σ := σ✝, F := F✝, eq := eq✝ }.F a b, CFilter.inf G.F a' b'),
        inf_le_left :=
          (_ :
            ∀ (x x_1 : { σ := σ✝, F := F✝, eq := eq✝ }.σ × G.σ),
              CFilter.f { σ := σ✝, F := F✝, eq := eq✝ }.F
                    (CFilter.inf { σ := σ✝, F := F✝, eq := eq✝ }.F x.fst x_1.fst) ∩
                  CFilter.f G.F (CFilter.inf G.F x.snd x_1.snd) ⊆
                CFilter.f { σ := σ✝, F := F✝, eq := eq✝ }.F x.fst ∩ CFilter.f G.F x.snd),
        inf_le_right :=
          (_ :
            ∀ (x x_1 : { σ := σ✝, F := F✝, eq := eq✝ }.σ × G.σ),
              CFilter.f { σ := σ✝, F := F✝, eq := eq✝ }.F
                    (CFilter.inf { σ := σ✝, F := F✝, eq := eq✝ }.F x.fst x_1.fst) ∩
                  CFilter.f G.F (CFilter.inf G.F x.snd x_1.snd) ⊆
                CFilter.f { σ := σ✝, F := F✝, eq := eq✝ }.F x_1.fst ∩ CFilter.f G.F x_1.snd) } =
    f ⊓ g
[PROOFSTEP]
cases G
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f g : Filter α
σ✝¹ : Type ?u.34651
F✝¹ : CFilter (Set α) σ✝¹
eq✝¹ : CFilter.toFilter F✝¹ = f
σ✝ : Type ?u.34706
F✝ : CFilter (Set α) σ✝
eq✝ : CFilter.toFilter F✝ = g
⊢ CFilter.toFilter
      {
        f := fun x =>
          match x with
          | (s, t) => CFilter.f { σ := σ✝¹, F := F✝¹, eq := eq✝¹ }.F s ∩ CFilter.f { σ := σ✝, F := F✝, eq := eq✝ }.F t,
        pt := ({ σ := σ✝¹, F := F✝¹, eq := eq✝¹ }.F.pt, { σ := σ✝, F := F✝, eq := eq✝ }.F.pt),
        inf := fun x x_1 =>
          match x with
          | (a, a') =>
            match x_1 with
            | (b, b') =>
              (CFilter.inf { σ := σ✝¹, F := F✝¹, eq := eq✝¹ }.F a b,
                CFilter.inf { σ := σ✝, F := F✝, eq := eq✝ }.F a' b'),
        inf_le_left :=
          (_ :
            ∀ (x x_1 : { σ := σ✝¹, F := F✝¹, eq := eq✝¹ }.σ × { σ := σ✝, F := F✝, eq := eq✝ }.σ),
              CFilter.f { σ := σ✝¹, F := F✝¹, eq := eq✝¹ }.F
                    (CFilter.inf { σ := σ✝¹, F := F✝¹, eq := eq✝¹ }.F x.fst x_1.fst) ∩
                  CFilter.f { σ := σ✝, F := F✝, eq := eq✝ }.F
                    (CFilter.inf { σ := σ✝, F := F✝, eq := eq✝ }.F x.snd x_1.snd) ⊆
                CFilter.f { σ := σ✝¹, F := F✝¹, eq := eq✝¹ }.F x.fst ∩
                  CFilter.f { σ := σ✝, F := F✝, eq := eq✝ }.F x.snd),
        inf_le_right :=
          (_ :
            ∀ (x x_1 : { σ := σ✝¹, F := F✝¹, eq := eq✝¹ }.σ × { σ := σ✝, F := F✝, eq := eq✝ }.σ),
              CFilter.f { σ := σ✝¹, F := F✝¹, eq := eq✝¹ }.F
                    (CFilter.inf { σ := σ✝¹, F := F✝¹, eq := eq✝¹ }.F x.fst x_1.fst) ∩
                  CFilter.f { σ := σ✝, F := F✝, eq := eq✝ }.F
                    (CFilter.inf { σ := σ✝, F := F✝, eq := eq✝ }.F x.snd x_1.snd) ⊆
                CFilter.f { σ := σ✝¹, F := F✝¹, eq := eq✝¹ }.F x_1.fst ∩
                  CFilter.f { σ := σ✝, F := F✝, eq := eq✝ }.F x_1.snd) } =
    f ⊓ g
[PROOFSTEP]
substs f g
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
σ✝¹ : Type ?u.34651
F✝¹ : CFilter (Set α) σ✝¹
σ✝ : Type ?u.34706
F✝ : CFilter (Set α) σ✝
⊢ CFilter.toFilter
      {
        f := fun x =>
          match x with
          | (s, t) =>
            CFilter.f { σ := σ✝¹, F := F✝¹, eq := (_ : CFilter.toFilter F✝¹ = CFilter.toFilter F✝¹) }.F s ∩
              CFilter.f { σ := σ✝, F := F✝, eq := (_ : CFilter.toFilter F✝ = CFilter.toFilter F✝) }.F t,
        pt :=
          ({ σ := σ✝¹, F := F✝¹, eq := (_ : CFilter.toFilter F✝¹ = CFilter.toFilter F✝¹) }.F.pt,
            { σ := σ✝, F := F✝, eq := (_ : CFilter.toFilter F✝ = CFilter.toFilter F✝) }.F.pt),
        inf := fun x x_1 =>
          match x with
          | (a, a') =>
            match x_1 with
            | (b, b') =>
              (CFilter.inf { σ := σ✝¹, F := F✝¹, eq := (_ : CFilter.toFilter F✝¹ = CFilter.toFilter F✝¹) }.F a b,
                CFilter.inf { σ := σ✝, F := F✝, eq := (_ : CFilter.toFilter F✝ = CFilter.toFilter F✝) }.F a' b'),
        inf_le_left :=
          (_ :
            ∀
              (x x_1 :
                { σ := σ✝¹, F := F✝¹, eq := (_ : CFilter.toFilter F✝¹ = CFilter.toFilter F✝¹) }.σ ×
                  { σ := σ✝, F := F✝, eq := (_ : CFilter.toFilter F✝ = CFilter.toFilter F✝) }.σ),
              CFilter.f { σ := σ✝¹, F := F✝¹, eq := (_ : CFilter.toFilter F✝¹ = CFilter.toFilter F✝¹) }.F
                    (CFilter.inf { σ := σ✝¹, F := F✝¹, eq := (_ : CFilter.toFilter F✝¹ = CFilter.toFilter F✝¹) }.F x.fst
                      x_1.fst) ∩
                  CFilter.f { σ := σ✝, F := F✝, eq := (_ : CFilter.toFilter F✝ = CFilter.toFilter F✝) }.F
                    (CFilter.inf { σ := σ✝, F := F✝, eq := (_ : CFilter.toFilter F✝ = CFilter.toFilter F✝) }.F x.snd
                      x_1.snd) ⊆
                CFilter.f { σ := σ✝¹, F := F✝¹, eq := (_ : CFilter.toFilter F✝¹ = CFilter.toFilter F✝¹) }.F x.fst ∩
                  CFilter.f { σ := σ✝, F := F✝, eq := (_ : CFilter.toFilter F✝ = CFilter.toFilter F✝) }.F x.snd),
        inf_le_right :=
          (_ :
            ∀
              (x x_1 :
                { σ := σ✝¹, F := F✝¹, eq := (_ : CFilter.toFilter F✝¹ = CFilter.toFilter F✝¹) }.σ ×
                  { σ := σ✝, F := F✝, eq := (_ : CFilter.toFilter F✝ = CFilter.toFilter F✝) }.σ),
              CFilter.f { σ := σ✝¹, F := F✝¹, eq := (_ : CFilter.toFilter F✝¹ = CFilter.toFilter F✝¹) }.F
                    (CFilter.inf { σ := σ✝¹, F := F✝¹, eq := (_ : CFilter.toFilter F✝¹ = CFilter.toFilter F✝¹) }.F x.fst
                      x_1.fst) ∩
                  CFilter.f { σ := σ✝, F := F✝, eq := (_ : CFilter.toFilter F✝ = CFilter.toFilter F✝) }.F
                    (CFilter.inf { σ := σ✝, F := F✝, eq := (_ : CFilter.toFilter F✝ = CFilter.toFilter F✝) }.F x.snd
                      x_1.snd) ⊆
                CFilter.f { σ := σ✝¹, F := F✝¹, eq := (_ : CFilter.toFilter F✝¹ = CFilter.toFilter F✝¹) }.F x_1.fst ∩
                  CFilter.f { σ := σ✝, F := F✝, eq := (_ : CFilter.toFilter F✝ = CFilter.toFilter F✝) }.F x_1.snd) } =
    CFilter.toFilter F✝¹ ⊓ CFilter.toFilter F✝
[PROOFSTEP]
simp only [CFilter.toFilter, Prod.exists]
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
σ✝¹ : Type ?u.34651
F✝¹ : CFilter (Set α) σ✝¹
σ✝ : Type ?u.34706
F✝ : CFilter (Set α) σ✝
⊢ { sets := {a | ∃ a_1 b, CFilter.f F✝¹ a_1 ∩ CFilter.f F✝ b ⊆ a},
      univ_sets := (_ : univ ∈ {a | ∃ a_1 b, CFilter.f F✝¹ a_1 ∩ CFilter.f F✝ b ⊆ a}),
      sets_of_superset :=
        (_ :
          ∀ {x y : Set α},
            x ∈ {a | ∃ a_1 b, CFilter.f F✝¹ a_1 ∩ CFilter.f F✝ b ⊆ a} →
              x ⊆ y → y ∈ {a | ∃ a_1 b, CFilter.f F✝¹ a_1 ∩ CFilter.f F✝ b ⊆ a}),
      inter_sets :=
        (_ :
          ∀ {x y : Set α},
            x ∈ {a | ∃ a_1 b, CFilter.f F✝¹ a_1 ∩ CFilter.f F✝ b ⊆ a} →
              y ∈ {a | ∃ a_1 b, CFilter.f F✝¹ a_1 ∩ CFilter.f F✝ b ⊆ a} →
                x ∩ y ∈ {a | ∃ a_1 b, CFilter.f F✝¹ a_1 ∩ CFilter.f F✝ b ⊆ a}) } =
    { sets := {a | ∃ b, CFilter.f F✝¹ b ⊆ a}, univ_sets := (_ : ∃ b, CFilter.f F✝¹ b ⊆ univ),
        sets_of_superset :=
          (_ : ∀ {x y : Set α}, x ∈ {a | ∃ b, CFilter.f F✝¹ b ⊆ a} → x ⊆ y → y ∈ {a | ∃ b, CFilter.f F✝¹ b ⊆ a}),
        inter_sets :=
          (_ :
            ∀ {x y : Set α},
              x ∈ {a | ∃ b, CFilter.f F✝¹ b ⊆ a} →
                y ∈ {a | ∃ b, CFilter.f F✝¹ b ⊆ a} → x ∩ y ∈ {a | ∃ b, CFilter.f F✝¹ b ⊆ a}) } ⊓
      { sets := {a | ∃ b, CFilter.f F✝ b ⊆ a}, univ_sets := (_ : ∃ b, CFilter.f F✝ b ⊆ univ),
        sets_of_superset :=
          (_ : ∀ {x y : Set α}, x ∈ {a | ∃ b, CFilter.f F✝ b ⊆ a} → x ⊆ y → y ∈ {a | ∃ b, CFilter.f F✝ b ⊆ a}),
        inter_sets :=
          (_ :
            ∀ {x y : Set α},
              x ∈ {a | ∃ b, CFilter.f F✝ b ⊆ a} →
                y ∈ {a | ∃ b, CFilter.f F✝ b ⊆ a} → x ∩ y ∈ {a | ∃ b, CFilter.f F✝ b ⊆ a}) }
[PROOFSTEP]
ext
[GOAL]
case mk.mk.a
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
σ✝¹ : Type ?u.34651
F✝¹ : CFilter (Set α) σ✝¹
σ✝ : Type ?u.34706
F✝ : CFilter (Set α) σ✝
s✝ : Set α
⊢ s✝ ∈
      { sets := {a | ∃ a_1 b, CFilter.f F✝¹ a_1 ∩ CFilter.f F✝ b ⊆ a},
        univ_sets := (_ : univ ∈ {a | ∃ a_1 b, CFilter.f F✝¹ a_1 ∩ CFilter.f F✝ b ⊆ a}),
        sets_of_superset :=
          (_ :
            ∀ {x y : Set α},
              x ∈ {a | ∃ a_1 b, CFilter.f F✝¹ a_1 ∩ CFilter.f F✝ b ⊆ a} →
                x ⊆ y → y ∈ {a | ∃ a_1 b, CFilter.f F✝¹ a_1 ∩ CFilter.f F✝ b ⊆ a}),
        inter_sets :=
          (_ :
            ∀ {x y : Set α},
              x ∈ {a | ∃ a_1 b, CFilter.f F✝¹ a_1 ∩ CFilter.f F✝ b ⊆ a} →
                y ∈ {a | ∃ a_1 b, CFilter.f F✝¹ a_1 ∩ CFilter.f F✝ b ⊆ a} →
                  x ∩ y ∈ {a | ∃ a_1 b, CFilter.f F✝¹ a_1 ∩ CFilter.f F✝ b ⊆ a}) } ↔
    s✝ ∈
      { sets := {a | ∃ b, CFilter.f F✝¹ b ⊆ a}, univ_sets := (_ : ∃ b, CFilter.f F✝¹ b ⊆ univ),
          sets_of_superset :=
            (_ : ∀ {x y : Set α}, x ∈ {a | ∃ b, CFilter.f F✝¹ b ⊆ a} → x ⊆ y → y ∈ {a | ∃ b, CFilter.f F✝¹ b ⊆ a}),
          inter_sets :=
            (_ :
              ∀ {x y : Set α},
                x ∈ {a | ∃ b, CFilter.f F✝¹ b ⊆ a} →
                  y ∈ {a | ∃ b, CFilter.f F✝¹ b ⊆ a} → x ∩ y ∈ {a | ∃ b, CFilter.f F✝¹ b ⊆ a}) } ⊓
        { sets := {a | ∃ b, CFilter.f F✝ b ⊆ a}, univ_sets := (_ : ∃ b, CFilter.f F✝ b ⊆ univ),
          sets_of_superset :=
            (_ : ∀ {x y : Set α}, x ∈ {a | ∃ b, CFilter.f F✝ b ⊆ a} → x ⊆ y → y ∈ {a | ∃ b, CFilter.f F✝ b ⊆ a}),
          inter_sets :=
            (_ :
              ∀ {x y : Set α},
                x ∈ {a | ∃ b, CFilter.f F✝ b ⊆ a} →
                  y ∈ {a | ∃ b, CFilter.f F✝ b ⊆ a} → x ∩ y ∈ {a | ∃ b, CFilter.f F✝ b ⊆ a}) }
[PROOFSTEP]
constructor
[GOAL]
case mk.mk.a.mp
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
σ✝¹ : Type ?u.34651
F✝¹ : CFilter (Set α) σ✝¹
σ✝ : Type ?u.34706
F✝ : CFilter (Set α) σ✝
s✝ : Set α
⊢ s✝ ∈
      { sets := {a | ∃ a_1 b, CFilter.f F✝¹ a_1 ∩ CFilter.f F✝ b ⊆ a},
        univ_sets := (_ : univ ∈ {a | ∃ a_1 b, CFilter.f F✝¹ a_1 ∩ CFilter.f F✝ b ⊆ a}),
        sets_of_superset :=
          (_ :
            ∀ {x y : Set α},
              x ∈ {a | ∃ a_1 b, CFilter.f F✝¹ a_1 ∩ CFilter.f F✝ b ⊆ a} →
                x ⊆ y → y ∈ {a | ∃ a_1 b, CFilter.f F✝¹ a_1 ∩ CFilter.f F✝ b ⊆ a}),
        inter_sets :=
          (_ :
            ∀ {x y : Set α},
              x ∈ {a | ∃ a_1 b, CFilter.f F✝¹ a_1 ∩ CFilter.f F✝ b ⊆ a} →
                y ∈ {a | ∃ a_1 b, CFilter.f F✝¹ a_1 ∩ CFilter.f F✝ b ⊆ a} →
                  x ∩ y ∈ {a | ∃ a_1 b, CFilter.f F✝¹ a_1 ∩ CFilter.f F✝ b ⊆ a}) } →
    s✝ ∈
      { sets := {a | ∃ b, CFilter.f F✝¹ b ⊆ a}, univ_sets := (_ : ∃ b, CFilter.f F✝¹ b ⊆ univ),
          sets_of_superset :=
            (_ : ∀ {x y : Set α}, x ∈ {a | ∃ b, CFilter.f F✝¹ b ⊆ a} → x ⊆ y → y ∈ {a | ∃ b, CFilter.f F✝¹ b ⊆ a}),
          inter_sets :=
            (_ :
              ∀ {x y : Set α},
                x ∈ {a | ∃ b, CFilter.f F✝¹ b ⊆ a} →
                  y ∈ {a | ∃ b, CFilter.f F✝¹ b ⊆ a} → x ∩ y ∈ {a | ∃ b, CFilter.f F✝¹ b ⊆ a}) } ⊓
        { sets := {a | ∃ b, CFilter.f F✝ b ⊆ a}, univ_sets := (_ : ∃ b, CFilter.f F✝ b ⊆ univ),
          sets_of_superset :=
            (_ : ∀ {x y : Set α}, x ∈ {a | ∃ b, CFilter.f F✝ b ⊆ a} → x ⊆ y → y ∈ {a | ∃ b, CFilter.f F✝ b ⊆ a}),
          inter_sets :=
            (_ :
              ∀ {x y : Set α},
                x ∈ {a | ∃ b, CFilter.f F✝ b ⊆ a} →
                  y ∈ {a | ∃ b, CFilter.f F✝ b ⊆ a} → x ∩ y ∈ {a | ∃ b, CFilter.f F✝ b ⊆ a}) }
[PROOFSTEP]
rintro ⟨s, t, h⟩
[GOAL]
case mk.mk.a.mp.intro.intro
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
σ✝¹ : Type ?u.34651
F✝¹ : CFilter (Set α) σ✝¹
σ✝ : Type ?u.34706
F✝ : CFilter (Set α) σ✝
s✝ : Set α
s : σ✝¹
t : σ✝
h : CFilter.f F✝¹ s ∩ CFilter.f F✝ t ⊆ s✝
⊢ s✝ ∈
    { sets := {a | ∃ b, CFilter.f F✝¹ b ⊆ a}, univ_sets := (_ : ∃ b, CFilter.f F✝¹ b ⊆ univ),
        sets_of_superset :=
          (_ : ∀ {x y : Set α}, x ∈ {a | ∃ b, CFilter.f F✝¹ b ⊆ a} → x ⊆ y → y ∈ {a | ∃ b, CFilter.f F✝¹ b ⊆ a}),
        inter_sets :=
          (_ :
            ∀ {x y : Set α},
              x ∈ {a | ∃ b, CFilter.f F✝¹ b ⊆ a} →
                y ∈ {a | ∃ b, CFilter.f F✝¹ b ⊆ a} → x ∩ y ∈ {a | ∃ b, CFilter.f F✝¹ b ⊆ a}) } ⊓
      { sets := {a | ∃ b, CFilter.f F✝ b ⊆ a}, univ_sets := (_ : ∃ b, CFilter.f F✝ b ⊆ univ),
        sets_of_superset :=
          (_ : ∀ {x y : Set α}, x ∈ {a | ∃ b, CFilter.f F✝ b ⊆ a} → x ⊆ y → y ∈ {a | ∃ b, CFilter.f F✝ b ⊆ a}),
        inter_sets :=
          (_ :
            ∀ {x y : Set α},
              x ∈ {a | ∃ b, CFilter.f F✝ b ⊆ a} →
                y ∈ {a | ∃ b, CFilter.f F✝ b ⊆ a} → x ∩ y ∈ {a | ∃ b, CFilter.f F✝ b ⊆ a}) }
[PROOFSTEP]
apply mem_inf_of_inter _ _ h
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
σ✝¹ : Type ?u.34651
F✝¹ : CFilter (Set α) σ✝¹
σ✝ : Type ?u.34706
F✝ : CFilter (Set α) σ✝
s✝ : Set α
s : σ✝¹
t : σ✝
h : CFilter.f F✝¹ s ∩ CFilter.f F✝ t ⊆ s✝
⊢ CFilter.f F✝¹ s ∈
    { sets := {a | ∃ b, CFilter.f F✝¹ b ⊆ a}, univ_sets := (_ : ∃ b, CFilter.f F✝¹ b ⊆ univ),
      sets_of_superset :=
        (_ : ∀ {x y : Set α}, x ∈ {a | ∃ b, CFilter.f F✝¹ b ⊆ a} → x ⊆ y → y ∈ {a | ∃ b, CFilter.f F✝¹ b ⊆ a}),
      inter_sets :=
        (_ :
          ∀ {x y : Set α},
            x ∈ {a | ∃ b, CFilter.f F✝¹ b ⊆ a} →
              y ∈ {a | ∃ b, CFilter.f F✝¹ b ⊆ a} → x ∩ y ∈ {a | ∃ b, CFilter.f F✝¹ b ⊆ a}) }
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
σ✝¹ : Type ?u.34651
F✝¹ : CFilter (Set α) σ✝¹
σ✝ : Type ?u.34706
F✝ : CFilter (Set α) σ✝
s✝ : Set α
s : σ✝¹
t : σ✝
h : CFilter.f F✝¹ s ∩ CFilter.f F✝ t ⊆ s✝
⊢ CFilter.f F✝ t ∈
    { sets := {a | ∃ b, CFilter.f F✝ b ⊆ a}, univ_sets := (_ : ∃ b, CFilter.f F✝ b ⊆ univ),
      sets_of_superset :=
        (_ : ∀ {x y : Set α}, x ∈ {a | ∃ b, CFilter.f F✝ b ⊆ a} → x ⊆ y → y ∈ {a | ∃ b, CFilter.f F✝ b ⊆ a}),
      inter_sets :=
        (_ :
          ∀ {x y : Set α},
            x ∈ {a | ∃ b, CFilter.f F✝ b ⊆ a} →
              y ∈ {a | ∃ b, CFilter.f F✝ b ⊆ a} → x ∩ y ∈ {a | ∃ b, CFilter.f F✝ b ⊆ a}) }
[PROOFSTEP]
use s
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
σ✝¹ : Type ?u.34651
F✝¹ : CFilter (Set α) σ✝¹
σ✝ : Type ?u.34706
F✝ : CFilter (Set α) σ✝
s✝ : Set α
s : σ✝¹
t : σ✝
h : CFilter.f F✝¹ s ∩ CFilter.f F✝ t ⊆ s✝
⊢ CFilter.f F✝ t ∈
    { sets := {a | ∃ b, CFilter.f F✝ b ⊆ a}, univ_sets := (_ : ∃ b, CFilter.f F✝ b ⊆ univ),
      sets_of_superset :=
        (_ : ∀ {x y : Set α}, x ∈ {a | ∃ b, CFilter.f F✝ b ⊆ a} → x ⊆ y → y ∈ {a | ∃ b, CFilter.f F✝ b ⊆ a}),
      inter_sets :=
        (_ :
          ∀ {x y : Set α},
            x ∈ {a | ∃ b, CFilter.f F✝ b ⊆ a} →
              y ∈ {a | ∃ b, CFilter.f F✝ b ⊆ a} → x ∩ y ∈ {a | ∃ b, CFilter.f F✝ b ⊆ a}) }
[PROOFSTEP]
use t
[GOAL]
case mk.mk.a.mpr
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
σ✝¹ : Type ?u.34651
F✝¹ : CFilter (Set α) σ✝¹
σ✝ : Type ?u.34706
F✝ : CFilter (Set α) σ✝
s✝ : Set α
⊢ s✝ ∈
      { sets := {a | ∃ b, CFilter.f F✝¹ b ⊆ a}, univ_sets := (_ : ∃ b, CFilter.f F✝¹ b ⊆ univ),
          sets_of_superset :=
            (_ : ∀ {x y : Set α}, x ∈ {a | ∃ b, CFilter.f F✝¹ b ⊆ a} → x ⊆ y → y ∈ {a | ∃ b, CFilter.f F✝¹ b ⊆ a}),
          inter_sets :=
            (_ :
              ∀ {x y : Set α},
                x ∈ {a | ∃ b, CFilter.f F✝¹ b ⊆ a} →
                  y ∈ {a | ∃ b, CFilter.f F✝¹ b ⊆ a} → x ∩ y ∈ {a | ∃ b, CFilter.f F✝¹ b ⊆ a}) } ⊓
        { sets := {a | ∃ b, CFilter.f F✝ b ⊆ a}, univ_sets := (_ : ∃ b, CFilter.f F✝ b ⊆ univ),
          sets_of_superset :=
            (_ : ∀ {x y : Set α}, x ∈ {a | ∃ b, CFilter.f F✝ b ⊆ a} → x ⊆ y → y ∈ {a | ∃ b, CFilter.f F✝ b ⊆ a}),
          inter_sets :=
            (_ :
              ∀ {x y : Set α},
                x ∈ {a | ∃ b, CFilter.f F✝ b ⊆ a} →
                  y ∈ {a | ∃ b, CFilter.f F✝ b ⊆ a} → x ∩ y ∈ {a | ∃ b, CFilter.f F✝ b ⊆ a}) } →
    s✝ ∈
      { sets := {a | ∃ a_1 b, CFilter.f F✝¹ a_1 ∩ CFilter.f F✝ b ⊆ a},
        univ_sets := (_ : univ ∈ {a | ∃ a_1 b, CFilter.f F✝¹ a_1 ∩ CFilter.f F✝ b ⊆ a}),
        sets_of_superset :=
          (_ :
            ∀ {x y : Set α},
              x ∈ {a | ∃ a_1 b, CFilter.f F✝¹ a_1 ∩ CFilter.f F✝ b ⊆ a} →
                x ⊆ y → y ∈ {a | ∃ a_1 b, CFilter.f F✝¹ a_1 ∩ CFilter.f F✝ b ⊆ a}),
        inter_sets :=
          (_ :
            ∀ {x y : Set α},
              x ∈ {a | ∃ a_1 b, CFilter.f F✝¹ a_1 ∩ CFilter.f F✝ b ⊆ a} →
                y ∈ {a | ∃ a_1 b, CFilter.f F✝¹ a_1 ∩ CFilter.f F✝ b ⊆ a} →
                  x ∩ y ∈ {a | ∃ a_1 b, CFilter.f F✝¹ a_1 ∩ CFilter.f F✝ b ⊆ a}) }
[PROOFSTEP]
rintro ⟨_, ⟨a, ha⟩, _, ⟨b, hb⟩, rfl⟩
[GOAL]
case mk.mk.a.mpr.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
σ✝¹ : Type ?u.34651
F✝¹ : CFilter (Set α) σ✝¹
σ✝ : Type ?u.34706
F✝ : CFilter (Set α) σ✝
w✝¹ : Set α
a : σ✝¹
ha : CFilter.f F✝¹ a ⊆ w✝¹
w✝ : Set α
b : σ✝
hb : CFilter.f F✝ b ⊆ w✝
⊢ w✝¹ ∩ w✝ ∈
    { sets := {a | ∃ a_1 b, CFilter.f F✝¹ a_1 ∩ CFilter.f F✝ b ⊆ a},
      univ_sets := (_ : univ ∈ {a | ∃ a_1 b, CFilter.f F✝¹ a_1 ∩ CFilter.f F✝ b ⊆ a}),
      sets_of_superset :=
        (_ :
          ∀ {x y : Set α},
            x ∈ {a | ∃ a_1 b, CFilter.f F✝¹ a_1 ∩ CFilter.f F✝ b ⊆ a} →
              x ⊆ y → y ∈ {a | ∃ a_1 b, CFilter.f F✝¹ a_1 ∩ CFilter.f F✝ b ⊆ a}),
      inter_sets :=
        (_ :
          ∀ {x y : Set α},
            x ∈ {a | ∃ a_1 b, CFilter.f F✝¹ a_1 ∩ CFilter.f F✝ b ⊆ a} →
              y ∈ {a | ∃ a_1 b, CFilter.f F✝¹ a_1 ∩ CFilter.f F✝ b ⊆ a} →
                x ∩ y ∈ {a | ∃ a_1 b, CFilter.f F✝¹ a_1 ∩ CFilter.f F✝ b ⊆ a}) }
[PROOFSTEP]
exact ⟨a, b, inter_subset_inter ha hb⟩
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
inst✝ : DecidableEq α
x✝ : Set α
h : x✝ ∈ cofinite.sets
⊢ CFilter.f
      { f := fun s => {a | ¬a ∈ s}, pt := ∅, inf := fun x x_1 => x ∪ x_1,
        inf_le_left := (_ : ∀ (x x_1 : Finset α) (x_2 : α), ¬x_2 ∈ (fun x x_3 => x ∪ x_3) x x_1 → ¬x_2 ∈ x),
        inf_le_right := (_ : ∀ (x x_1 : Finset α) (x_2 : α), ¬x_2 ∈ (fun x x_3 => x ∪ x_3) x x_1 → ¬x_2 ∈ x_1) }
      (Finite.toFinset h) ⊆
    x✝
[PROOFSTEP]
simp [Subset.rfl]
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f✝ : Filter α
m : α → Filter β
F : Realizer f✝
G : (i : α) → Realizer (m i)
x✝ : (s : F.σ) × ((i : α) → i ∈ CFilter.f F.F s → (G i).σ)
s : F.σ
f : (i : α) → i ∈ CFilter.f F.F s → (G i).σ
i : α
h✝ : i ∈ CFilter.f F.F s
⊢ i ∈ CFilter.f F.F s
[PROOFSTEP]
assumption
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f : Filter α
m : α → Filter β
F : Realizer f
G : (i : α) → Realizer (m i)
x✝² x✝¹ : (s : F.σ) × ((i : α) → i ∈ CFilter.f F.F s → (G i).σ)
x✝ : β
⊢ x✝ ∈
      (fun x =>
          match x with
          | { fst := s, snd := f_1 } => ⋃ (i : α) (h : i ∈ CFilter.f F.F s), CFilter.f (G i).F (f_1 i h))
        ((fun x x_1 =>
            match x with
            | { fst := a, snd := f_1 } =>
              match x_1 with
              | { fst := b, snd := f' } =>
                { fst := CFilter.inf F.F a b,
                  snd := fun i h =>
                    CFilter.inf (G i).F (f_1 i (_ : i ∈ CFilter.f F.F a)) (f' i (_ : i ∈ CFilter.f F.F b)) })
          x✝² x✝¹) →
    x✝ ∈
      (fun x =>
          match x with
          | { fst := s, snd := f_1 } => ⋃ (i : α) (h : i ∈ CFilter.f F.F s), CFilter.f (G i).F (f_1 i h))
        x✝²
[PROOFSTEP]
simp only [mem_iUnion, forall_exists_index]
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f : Filter α
m : α → Filter β
F : Realizer f
G : (i : α) → Realizer (m i)
x✝² x✝¹ : (s : F.σ) × ((i : α) → i ∈ CFilter.f F.F s → (G i).σ)
x✝ : β
⊢ ∀ (x : α) (x_1 : x ∈ CFilter.f F.F (CFilter.inf F.F x✝².fst x✝¹.fst)),
    x✝ ∈
        CFilter.f (G x).F
          (CFilter.inf (G x).F (Sigma.snd x✝² x (_ : x ∈ CFilter.f F.F x✝².fst))
            (Sigma.snd x✝¹ x (_ : x ∈ CFilter.f F.F x✝¹.fst))) →
      ∃ i i_1, x✝ ∈ CFilter.f (G i).F (Sigma.snd x✝² i i_1)
[PROOFSTEP]
exact fun i h₁ h₂ ↦ ⟨i, F.F.inf_le_left _ _ h₁, (G i).F.inf_le_left _ _ h₂⟩
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f : Filter α
m : α → Filter β
F : Realizer f
G : (i : α) → Realizer (m i)
x✝² x✝¹ : (s : F.σ) × ((i : α) → i ∈ CFilter.f F.F s → (G i).σ)
x✝ : β
⊢ x✝ ∈
      (fun x =>
          match x with
          | { fst := s, snd := f_1 } => ⋃ (i : α) (h : i ∈ CFilter.f F.F s), CFilter.f (G i).F (f_1 i h))
        ((fun x x_1 =>
            match x with
            | { fst := a, snd := f_1 } =>
              match x_1 with
              | { fst := b, snd := f' } =>
                { fst := CFilter.inf F.F a b,
                  snd := fun i h =>
                    CFilter.inf (G i).F (f_1 i (_ : i ∈ CFilter.f F.F a)) (f' i (_ : i ∈ CFilter.f F.F b)) })
          x✝² x✝¹) →
    x✝ ∈
      (fun x =>
          match x with
          | { fst := s, snd := f_1 } => ⋃ (i : α) (h : i ∈ CFilter.f F.F s), CFilter.f (G i).F (f_1 i h))
        x✝¹
[PROOFSTEP]
simp only [mem_iUnion, forall_exists_index]
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f : Filter α
m : α → Filter β
F : Realizer f
G : (i : α) → Realizer (m i)
x✝² x✝¹ : (s : F.σ) × ((i : α) → i ∈ CFilter.f F.F s → (G i).σ)
x✝ : β
⊢ ∀ (x : α) (x_1 : x ∈ CFilter.f F.F (CFilter.inf F.F x✝².fst x✝¹.fst)),
    x✝ ∈
        CFilter.f (G x).F
          (CFilter.inf (G x).F (Sigma.snd x✝² x (_ : x ∈ CFilter.f F.F x✝².fst))
            (Sigma.snd x✝¹ x (_ : x ∈ CFilter.f F.F x✝¹.fst))) →
      ∃ i i_1, x✝ ∈ CFilter.f (G i).F (Sigma.snd x✝¹ i i_1)
[PROOFSTEP]
exact fun i h₁ h₂ ↦ ⟨i, F.F.inf_le_right _ _ h₁, (G i).F.inf_le_right _ _ h₂⟩
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f : Filter α
m : α → Filter β
F : Realizer f
G : (i : α) → Realizer (m i)
x✝ : Set β
⊢ x✝ ∈
      (CFilter.toFilter
          {
            f := fun x =>
              match x with
              | { fst := s, snd := f_1 } => ⋃ (i : α) (h : i ∈ CFilter.f F.F s), CFilter.f (G i).F (f_1 i h),
            pt := { fst := F.F.pt, snd := fun i x => (G i).F.pt },
            inf := fun x x_1 =>
              match x with
              | { fst := a, snd := f_1 } =>
                match x_1 with
                | { fst := b, snd := f' } =>
                  { fst := CFilter.inf F.F a b,
                    snd := fun i h =>
                      CFilter.inf (G i).F (f_1 i (_ : i ∈ CFilter.f F.F a)) (f' i (_ : i ∈ CFilter.f F.F b)) },
            inf_le_left :=
              (_ :
                ∀ (x x_1 : (s : F.σ) × ((i : α) → i ∈ CFilter.f F.F s → (G i).σ)) (x_2 : β),
                  x_2 ∈
                      (fun x =>
                          match x with
                          | { fst := s, snd := f_1 } =>
                            ⋃ (i : α) (h : i ∈ CFilter.f F.F s), CFilter.f (G i).F (f_1 i h))
                        ((fun x x_3 =>
                            match x with
                            | { fst := a, snd := f_1 } =>
                              match x_3 with
                              | { fst := b, snd := f' } =>
                                { fst := CFilter.inf F.F a b,
                                  snd := fun i h =>
                                    CFilter.inf (G i).F (f_1 i (_ : i ∈ CFilter.f F.F a))
                                      (f' i (_ : i ∈ CFilter.f F.F b)) })
                          x x_1) →
                    x_2 ∈
                      (fun x =>
                          match x with
                          | { fst := s, snd := f_1 } =>
                            ⋃ (i : α) (h : i ∈ CFilter.f F.F s), CFilter.f (G i).F (f_1 i h))
                        x),
            inf_le_right :=
              (_ :
                ∀ (x x_1 : (s : F.σ) × ((i : α) → i ∈ CFilter.f F.F s → (G i).σ)) (x_2 : β),
                  x_2 ∈
                      (fun x =>
                          match x with
                          | { fst := s, snd := f_1 } =>
                            ⋃ (i : α) (h : i ∈ CFilter.f F.F s), CFilter.f (G i).F (f_1 i h))
                        ((fun x x_3 =>
                            match x with
                            | { fst := a, snd := f_1 } =>
                              match x_3 with
                              | { fst := b, snd := f' } =>
                                { fst := CFilter.inf F.F a b,
                                  snd := fun i h =>
                                    CFilter.inf (G i).F (f_1 i (_ : i ∈ CFilter.f F.F a))
                                      (f' i (_ : i ∈ CFilter.f F.F b)) })
                          x x_1) →
                    x_2 ∈
                      (fun x =>
                          match x with
                          | { fst := s, snd := f_1 } =>
                            ⋃ (i : α) (h : i ∈ CFilter.f F.F s), CFilter.f (G i).F (f_1 i h))
                        x_1) }).sets ↔
    x✝ ∈ (bind f m).sets
[PROOFSTEP]
cases' F with _ F _
[GOAL]
case mk
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f : Filter α
m : α → Filter β
G : (i : α) → Realizer (m i)
x✝ : Set β
σ✝ : Type ?u.44096
F : CFilter (Set α) σ✝
eq✝ : CFilter.toFilter F = f
⊢ x✝ ∈
      (CFilter.toFilter
          {
            f := fun x =>
              match x with
              | { fst := s, snd := f_1 } =>
                ⋃ (i : α) (h : i ∈ CFilter.f { σ := σ✝, F := F, eq := eq✝ }.F s), CFilter.f (G i).F (f_1 i h),
            pt := { fst := { σ := σ✝, F := F, eq := eq✝ }.F.pt, snd := fun i x => (G i).F.pt },
            inf := fun x x_1 =>
              match x with
              | { fst := a, snd := f_1 } =>
                match x_1 with
                | { fst := b, snd := f' } =>
                  { fst := CFilter.inf { σ := σ✝, F := F, eq := eq✝ }.F a b,
                    snd := fun i h =>
                      CFilter.inf (G i).F (f_1 i (_ : i ∈ CFilter.f { σ := σ✝, F := F, eq := eq✝ }.F a))
                        (f' i (_ : i ∈ CFilter.f { σ := σ✝, F := F, eq := eq✝ }.F b)) },
            inf_le_left :=
              (_ :
                ∀
                  (x x_1 :
                    (s : { σ := σ✝, F := F, eq := eq✝ }.σ) ×
                      ((i : α) → i ∈ CFilter.f { σ := σ✝, F := F, eq := eq✝ }.F s → (G i).σ))
                  (x_2 : β),
                  x_2 ∈
                      (fun x =>
                          match x with
                          | { fst := s, snd := f_1 } =>
                            ⋃ (i : α) (h : i ∈ CFilter.f { σ := σ✝, F := F, eq := eq✝ }.F s),
                              CFilter.f (G i).F (f_1 i h))
                        ((fun x x_3 =>
                            match x with
                            | { fst := a, snd := f_1 } =>
                              match x_3 with
                              | { fst := b, snd := f' } =>
                                { fst := CFilter.inf { σ := σ✝, F := F, eq := eq✝ }.F a b,
                                  snd := fun i h =>
                                    CFilter.inf (G i).F (f_1 i (_ : i ∈ CFilter.f { σ := σ✝, F := F, eq := eq✝ }.F a))
                                      (f' i (_ : i ∈ CFilter.f { σ := σ✝, F := F, eq := eq✝ }.F b)) })
                          x x_1) →
                    x_2 ∈
                      (fun x =>
                          match x with
                          | { fst := s, snd := f_1 } =>
                            ⋃ (i : α) (h : i ∈ CFilter.f { σ := σ✝, F := F, eq := eq✝ }.F s),
                              CFilter.f (G i).F (f_1 i h))
                        x),
            inf_le_right :=
              (_ :
                ∀
                  (x x_1 :
                    (s : { σ := σ✝, F := F, eq := eq✝ }.σ) ×
                      ((i : α) → i ∈ CFilter.f { σ := σ✝, F := F, eq := eq✝ }.F s → (G i).σ))
                  (x_2 : β),
                  x_2 ∈
                      (fun x =>
                          match x with
                          | { fst := s, snd := f_1 } =>
                            ⋃ (i : α) (h : i ∈ CFilter.f { σ := σ✝, F := F, eq := eq✝ }.F s),
                              CFilter.f (G i).F (f_1 i h))
                        ((fun x x_3 =>
                            match x with
                            | { fst := a, snd := f_1 } =>
                              match x_3 with
                              | { fst := b, snd := f' } =>
                                { fst := CFilter.inf { σ := σ✝, F := F, eq := eq✝ }.F a b,
                                  snd := fun i h =>
                                    CFilter.inf (G i).F (f_1 i (_ : i ∈ CFilter.f { σ := σ✝, F := F, eq := eq✝ }.F a))
                                      (f' i (_ : i ∈ CFilter.f { σ := σ✝, F := F, eq := eq✝ }.F b)) })
                          x x_1) →
                    x_2 ∈
                      (fun x =>
                          match x with
                          | { fst := s, snd := f_1 } =>
                            ⋃ (i : α) (h : i ∈ CFilter.f { σ := σ✝, F := F, eq := eq✝ }.F s),
                              CFilter.f (G i).F (f_1 i h))
                        x_1) }).sets ↔
    x✝ ∈ (bind f m).sets
[PROOFSTEP]
subst f
[GOAL]
case mk
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
m : α → Filter β
G : (i : α) → Realizer (m i)
x✝ : Set β
σ✝ : Type ?u.44096
F : CFilter (Set α) σ✝
⊢ x✝ ∈
      (CFilter.toFilter
          {
            f := fun x =>
              match x with
              | { fst := s, snd := f } =>
                ⋃ (i : α) (h :
                  i ∈ CFilter.f { σ := σ✝, F := F, eq := (_ : CFilter.toFilter F = CFilter.toFilter F) }.F s),
                  CFilter.f (G i).F (f i h),
            pt :=
              { fst := { σ := σ✝, F := F, eq := (_ : CFilter.toFilter F = CFilter.toFilter F) }.F.pt,
                snd := fun i x => (G i).F.pt },
            inf := fun x x_1 =>
              match x with
              | { fst := a, snd := f } =>
                match x_1 with
                | { fst := b, snd := f' } =>
                  { fst := CFilter.inf { σ := σ✝, F := F, eq := (_ : CFilter.toFilter F = CFilter.toFilter F) }.F a b,
                    snd := fun i h =>
                      CFilter.inf (G i).F
                        (f i
                          (_ :
                            i ∈ CFilter.f { σ := σ✝, F := F, eq := (_ : CFilter.toFilter F = CFilter.toFilter F) }.F a))
                        (f' i
                          (_ :
                            i ∈
                              CFilter.f { σ := σ✝, F := F, eq := (_ : CFilter.toFilter F = CFilter.toFilter F) }.F
                                b)) },
            inf_le_left :=
              (_ :
                ∀
                  (x x_1 :
                    (s : { σ := σ✝, F := F, eq := (_ : CFilter.toFilter F = CFilter.toFilter F) }.σ) ×
                      ((i : α) →
                        i ∈ CFilter.f { σ := σ✝, F := F, eq := (_ : CFilter.toFilter F = CFilter.toFilter F) }.F s →
                          (G i).σ))
                  (x_2 : β),
                  x_2 ∈
                      (fun x =>
                          match x with
                          | { fst := s, snd := f } =>
                            ⋃ (i : α) (h :
                              i ∈
                                CFilter.f { σ := σ✝, F := F, eq := (_ : CFilter.toFilter F = CFilter.toFilter F) }.F s),
                              CFilter.f (G i).F (f i h))
                        ((fun x x_3 =>
                            match x with
                            | { fst := a, snd := f } =>
                              match x_3 with
                              | { fst := b, snd := f' } =>
                                {
                                  fst :=
                                    CFilter.inf
                                      { σ := σ✝, F := F, eq := (_ : CFilter.toFilter F = CFilter.toFilter F) }.F a b,
                                  snd := fun i h =>
                                    CFilter.inf (G i).F
                                      (f i
                                        (_ :
                                          i ∈
                                            CFilter.f
                                              { σ := σ✝, F := F, eq := (_ : CFilter.toFilter F = CFilter.toFilter F) }.F
                                              a))
                                      (f' i
                                        (_ :
                                          i ∈
                                            CFilter.f
                                              { σ := σ✝, F := F, eq := (_ : CFilter.toFilter F = CFilter.toFilter F) }.F
                                              b)) })
                          x x_1) →
                    x_2 ∈
                      (fun x =>
                          match x with
                          | { fst := s, snd := f } =>
                            ⋃ (i : α) (h :
                              i ∈
                                CFilter.f { σ := σ✝, F := F, eq := (_ : CFilter.toFilter F = CFilter.toFilter F) }.F s),
                              CFilter.f (G i).F (f i h))
                        x),
            inf_le_right :=
              (_ :
                ∀
                  (x x_1 :
                    (s : { σ := σ✝, F := F, eq := (_ : CFilter.toFilter F = CFilter.toFilter F) }.σ) ×
                      ((i : α) →
                        i ∈ CFilter.f { σ := σ✝, F := F, eq := (_ : CFilter.toFilter F = CFilter.toFilter F) }.F s →
                          (G i).σ))
                  (x_2 : β),
                  x_2 ∈
                      (fun x =>
                          match x with
                          | { fst := s, snd := f } =>
                            ⋃ (i : α) (h :
                              i ∈
                                CFilter.f { σ := σ✝, F := F, eq := (_ : CFilter.toFilter F = CFilter.toFilter F) }.F s),
                              CFilter.f (G i).F (f i h))
                        ((fun x x_3 =>
                            match x with
                            | { fst := a, snd := f } =>
                              match x_3 with
                              | { fst := b, snd := f' } =>
                                {
                                  fst :=
                                    CFilter.inf
                                      { σ := σ✝, F := F, eq := (_ : CFilter.toFilter F = CFilter.toFilter F) }.F a b,
                                  snd := fun i h =>
                                    CFilter.inf (G i).F
                                      (f i
                                        (_ :
                                          i ∈
                                            CFilter.f
                                              { σ := σ✝, F := F, eq := (_ : CFilter.toFilter F = CFilter.toFilter F) }.F
                                              a))
                                      (f' i
                                        (_ :
                                          i ∈
                                            CFilter.f
                                              { σ := σ✝, F := F, eq := (_ : CFilter.toFilter F = CFilter.toFilter F) }.F
                                              b)) })
                          x x_1) →
                    x_2 ∈
                      (fun x =>
                          match x with
                          | { fst := s, snd := f } =>
                            ⋃ (i : α) (h :
                              i ∈
                                CFilter.f { σ := σ✝, F := F, eq := (_ : CFilter.toFilter F = CFilter.toFilter F) }.F s),
                              CFilter.f (G i).F (f i h))
                        x_1) }).sets ↔
    x✝ ∈ (bind (CFilter.toFilter F) m).sets
[PROOFSTEP]
simp only [CFilter.toFilter, iUnion_subset_iff, Sigma.exists, Filter.mem_sets, mem_bind]
[GOAL]
case mk
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
m : α → Filter β
G : (i : α) → Realizer (m i)
x✝ : Set β
σ✝ : Type ?u.44096
F : CFilter (Set α) σ✝
⊢ x✝ ∈ {a | ∃ a_1 b, ∀ (i : α) (i_1 : i ∈ CFilter.f F { fst := a_1, snd := b }.fst), CFilter.f (G i).F (b i i_1) ⊆ a} ↔
    ∃ t,
      t ∈
          { sets := {a | ∃ b, CFilter.f F b ⊆ a}, univ_sets := (_ : ∃ b, CFilter.f F b ⊆ univ),
            sets_of_superset :=
              (_ : ∀ {x y : Set α}, x ∈ {a | ∃ b, CFilter.f F b ⊆ a} → x ⊆ y → y ∈ {a | ∃ b, CFilter.f F b ⊆ a}),
            inter_sets :=
              (_ :
                ∀ {x y : Set α},
                  x ∈ {a | ∃ b, CFilter.f F b ⊆ a} →
                    y ∈ {a | ∃ b, CFilter.f F b ⊆ a} → x ∩ y ∈ {a | ∃ b, CFilter.f F b ⊆ a}) } ∧
        ∀ (x : α), x ∈ t → x✝ ∈ m x
[PROOFSTEP]
exact
  ⟨fun ⟨s, f, h⟩ ↦ ⟨F s, ⟨s, Subset.refl _⟩, fun i H ↦ (G i).mem_sets.2 ⟨f i H, fun _ h' ↦ h i H h'⟩⟩,
    fun ⟨_, ⟨s, h⟩, f⟩ ↦
    let ⟨f', h'⟩ := Classical.axiom_of_choice fun i : F s ↦ (G i).mem_sets.1 (f i (h i.2))
    ⟨s, fun i h ↦ f' ⟨i, h⟩, fun _ H _ m ↦ h' ⟨_, H⟩ m⟩⟩
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f : α → Filter β
F : (i : α) → Realizer (f i)
⊢ ∀ (x : Set β), x ∈ (bind ⊤ fun i => f i).sets ↔ x ∈ (⨆ (i : α), f i).sets
[PROOFSTEP]
simp [Filter.bind, eq_univ_iff_forall, iSup_sets_eq]
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f : Filter α
F : Realizer f
⊢ f ≠ ⊥ ↔ ∀ (a : F.σ), Set.Nonempty (CFilter.f F.F a)
[PROOFSTEP]
rw [not_iff_comm, ← le_bot_iff, F.le_iff Realizer.bot, not_forall]
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f : Filter α
F : Realizer f
⊢ (∃ x, ¬Set.Nonempty (CFilter.f F.F x)) ↔ ∀ (b : Realizer.bot.σ), ∃ a, CFilter.f F.F a ≤ CFilter.f Realizer.bot.F b
[PROOFSTEP]
simp only [Set.not_nonempty_iff_eq_empty]
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f : Filter α
F : Realizer f
⊢ (∃ x, CFilter.f F.F x = ∅) ↔ ∀ (b : Realizer.bot.σ), ∃ a, CFilter.f F.F a ≤ CFilter.f Realizer.bot.F b
[PROOFSTEP]
exact
  ⟨fun ⟨x, e⟩ _ ↦ ⟨x, le_of_eq e⟩, fun h ↦
    let ⟨x, h⟩ := h ()
    ⟨x, le_bot_iff.1 h⟩⟩


[GOAL]
⊢ ↑LinearMap.det (AlgEquiv.toLinearMap conjAe) = -1
[PROOFSTEP]
rw [← LinearMap.det_toMatrix basisOneI, toMatrix_conjAe, Matrix.det_fin_two_of]
[GOAL]
⊢ 1 * -1 - 0 * 0 = -1
[PROOFSTEP]
simp
[GOAL]
⊢ ↑LinearEquiv.det (AlgEquiv.toLinearEquiv conjAe) = -1
[PROOFSTEP]
rw [← Units.eq_iff, LinearEquiv.coe_det, AlgEquiv.toLinearEquiv_toLinearMap, det_conjAe, Units.coe_neg_one]