[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A B : Matrix n n α
inst✝ : Invertible (det A)
⊢ ⅟(det A) • adjugate A * A = 1
[PROOFSTEP]
rw [smul_mul_assoc, adjugate_mul, smul_smul, invOf_mul_self, one_smul]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A B : Matrix n n α
inst✝ : Invertible (det A)
⊢ A * ⅟(det A) • adjugate A = 1
[PROOFSTEP]
rw [mul_smul_comm, mul_adjugate, smul_smul, invOf_mul_self, one_smul]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
A B : Matrix n n α
inst✝¹ : Invertible (det A)
inst✝ : Invertible A
⊢ ⅟A = ⅟(det A) • adjugate A
[PROOFSTEP]
letI := invertibleOfDetInvertible A
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
A B : Matrix n n α
inst✝¹ : Invertible (det A)
inst✝ : Invertible A
this : Invertible A := invertibleOfDetInvertible A
⊢ ⅟A = ⅟(det A) • adjugate A
[PROOFSTEP]
convert (rfl : ⅟A = _)
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h : B * A = 1
⊢ det B * det A = 1
[PROOFSTEP]
rw [← det_mul, h, det_one]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h : B * A = 1
⊢ det A * det B = 1
[PROOFSTEP]
rw [mul_comm, ← det_mul, h, det_one]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h : A * B = 1
⊢ det B * det A = 1
[PROOFSTEP]
rw [mul_comm, ← det_mul, h, det_one]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h : A * B = 1
⊢ det A * det B = 1
[PROOFSTEP]
rw [← det_mul, h, det_one]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
A B : Matrix n n α
inst✝¹ : Invertible A
inst✝ : Invertible (det A)
⊢ det ⅟A = ⅟(det A)
[PROOFSTEP]
letI := detInvertibleOfInvertible A
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
A B : Matrix n n α
inst✝¹ : Invertible A
inst✝ : Invertible (det A)
this : Invertible (det A) := detInvertibleOfInvertible A
⊢ det ⅟A = ⅟(det A)
[PROOFSTEP]
convert (rfl : _ = ⅟A.det)
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A✝ B✝ A B : Matrix n n α
h : A * B = 1
⊢ B * A = 1
[PROOFSTEP]
letI : Invertible B.det := detInvertibleOfLeftInverse _ _ h
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A✝ B✝ A B : Matrix n n α
h : A * B = 1
this : Invertible (det B) := detInvertibleOfLeftInverse B A h
⊢ B * A = 1
[PROOFSTEP]
letI : Invertible B := invertibleOfDetInvertible B
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A✝ B✝ A B : Matrix n n α
h : A * B = 1
this✝ : Invertible (det B) := detInvertibleOfLeftInverse B A h
this : Invertible B := invertibleOfDetInvertible B
⊢ B * A = 1
[PROOFSTEP]
calc
  B * A = B * A * (B * ⅟B) := by rw [mul_invOf_self, Matrix.mul_one]
  _ = B * (A * B * ⅟B) := by simp only [Matrix.mul_assoc]
  _ = B * ⅟B := by rw [h, Matrix.one_mul]
  _ = 1 := mul_invOf_self B
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A✝ B✝ A B : Matrix n n α
h : A * B = 1
this✝ : Invertible (det B) := detInvertibleOfLeftInverse B A h
this : Invertible B := invertibleOfDetInvertible B
⊢ B * A = B * A * (B * ⅟B)
[PROOFSTEP]
rw [mul_invOf_self, Matrix.mul_one]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A✝ B✝ A B : Matrix n n α
h : A * B = 1
this✝ : Invertible (det B) := detInvertibleOfLeftInverse B A h
this : Invertible B := invertibleOfDetInvertible B
⊢ B * A * (B * ⅟B) = B * (A * B * ⅟B)
[PROOFSTEP]
simp only [Matrix.mul_assoc]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A✝ B✝ A B : Matrix n n α
h : A * B = 1
this✝ : Invertible (det B) := detInvertibleOfLeftInverse B A h
this : Invertible B := invertibleOfDetInvertible B
⊢ B * (A * B * ⅟B) = B * ⅟B
[PROOFSTEP]
rw [h, Matrix.one_mul]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A B : Matrix n n α
inst✝ : Invertible A
⊢ Invertible (det Aᵀ)
[PROOFSTEP]
simpa using detInvertibleOfInvertible A
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A B : Matrix n n α
inst✝ : Invertible Aᵀ
⊢ Invertible A
[PROOFSTEP]
rw [← transpose_transpose A]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A B : Matrix n n α
inst✝ : Invertible Aᵀ
⊢ Invertible Aᵀᵀ
[PROOFSTEP]
infer_instance
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
A B : Matrix n n α
inst✝¹ : StarRing α
inst✝ : Invertible Aᴴ
⊢ Invertible A
[PROOFSTEP]
rw [← conjTranspose_conjTranspose A, ← star_eq_conjTranspose]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
A B : Matrix n n α
inst✝¹ : StarRing α
inst✝ : Invertible Aᴴ
⊢ Invertible (star Aᴴ)
[PROOFSTEP]
infer_instance
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
⊢ IsUnit A ↔ IsUnit (det A)
[PROOFSTEP]
simp only [← nonempty_invertible_iff_isUnit, (invertibleEquivDetInvertible A).nonempty_congr]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h : IsUnit (det A)
⊢ IsUnit (det Aᵀ)
[PROOFSTEP]
rw [det_transpose]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h : IsUnit (det A)
⊢ IsUnit (det A)
[PROOFSTEP]
exact h
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h : ¬IsUnit (det A)
⊢ A⁻¹ = 0
[PROOFSTEP]
rw [inv_def, Ring.inverse_non_unit _ h, zero_smul]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h : IsUnit (det A)
⊢ A⁻¹ = ↑(IsUnit.unit h)⁻¹ • adjugate A
[PROOFSTEP]
rw [inv_def, ← Ring.inverse_unit h.unit, IsUnit.unit_spec]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A B : Matrix n n α
inst✝ : Invertible A
⊢ ⅟A = A⁻¹
[PROOFSTEP]
letI := detInvertibleOfInvertible A
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A B : Matrix n n α
inst✝ : Invertible A
this : Invertible (det A) := detInvertibleOfInvertible A
⊢ ⅟A = A⁻¹
[PROOFSTEP]
rw [inv_def, Ring.inverse_invertible, invOf_eq]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A✝ B : Matrix n n α
A : (Matrix n n α)ˣ
⊢ ↑A⁻¹ = (↑A)⁻¹
[PROOFSTEP]
letI := A.invertible
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A✝ B : Matrix n n α
A : (Matrix n n α)ˣ
this : Invertible ↑A := Units.invertible A
⊢ ↑A⁻¹ = (↑A)⁻¹
[PROOFSTEP]
rw [← invOf_eq_nonsing_inv, invOf_units]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
⊢ A⁻¹ = Ring.inverse A
[PROOFSTEP]
by_cases h_det : IsUnit A.det
[GOAL]
case pos
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h_det : IsUnit (det A)
⊢ A⁻¹ = Ring.inverse A
[PROOFSTEP]
cases (A.isUnit_iff_isUnit_det.mpr h_det).nonempty_invertible
[GOAL]
case pos.intro
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h_det : IsUnit (det A)
val✝ : Invertible A
⊢ A⁻¹ = Ring.inverse A
[PROOFSTEP]
rw [← invOf_eq_nonsing_inv, Ring.inverse_invertible]
[GOAL]
case neg
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h_det : ¬IsUnit (det A)
⊢ A⁻¹ = Ring.inverse A
[PROOFSTEP]
have h := mt A.isUnit_iff_isUnit_det.mp h_det
[GOAL]
case neg
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h_det : ¬IsUnit (det A)
h : ¬IsUnit A
⊢ A⁻¹ = Ring.inverse A
[PROOFSTEP]
rw [Ring.inverse_non_unit _ h, nonsing_inv_apply_not_isUnit A h_det]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
⊢ A⁻¹ᵀ = Aᵀ⁻¹
[PROOFSTEP]
rw [inv_def, inv_def, transpose_smul, det_transpose, adjugate_transpose]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A B : Matrix n n α
inst✝ : StarRing α
⊢ A⁻¹ᴴ = Aᴴ⁻¹
[PROOFSTEP]
rw [inv_def, inv_def, conjTranspose_smul, det_conjTranspose, adjugate_conjTranspose, Ring.inverse_star]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h : IsUnit (det A)
⊢ A * A⁻¹ = 1
[PROOFSTEP]
cases (A.isUnit_iff_isUnit_det.mpr h).nonempty_invertible
[GOAL]
case intro
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h : IsUnit (det A)
val✝ : Invertible A
⊢ A * A⁻¹ = 1
[PROOFSTEP]
rw [← invOf_eq_nonsing_inv, mul_invOf_self]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h : IsUnit (det A)
⊢ A⁻¹ * A = 1
[PROOFSTEP]
cases (A.isUnit_iff_isUnit_det.mpr h).nonempty_invertible
[GOAL]
case intro
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h : IsUnit (det A)
val✝ : Invertible A
⊢ A⁻¹ * A = 1
[PROOFSTEP]
rw [← invOf_eq_nonsing_inv, invOf_mul_self]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A B : Matrix n n α
inst✝ : Invertible A
⊢ Invertible A⁻¹
[PROOFSTEP]
rw [← invOf_eq_nonsing_inv]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A B : Matrix n n α
inst✝ : Invertible A
⊢ Invertible ⅟A
[PROOFSTEP]
infer_instance
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A B : Matrix n n α
inst✝ : Invertible A
⊢ A⁻¹⁻¹ = A
[PROOFSTEP]
simp only [← invOf_eq_nonsing_inv, invOf_invOf]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B✝ : Matrix n n α
B : Matrix m n α
h : IsUnit (det A)
⊢ B * A * A⁻¹ = B
[PROOFSTEP]
simp [Matrix.mul_assoc, mul_nonsing_inv A h]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B✝ : Matrix n n α
B : Matrix n m α
h : IsUnit (det A)
⊢ A * (A⁻¹ * B) = B
[PROOFSTEP]
simp [← Matrix.mul_assoc, mul_nonsing_inv A h]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B✝ : Matrix n n α
B : Matrix m n α
h : IsUnit (det A)
⊢ B * A⁻¹ * A = B
[PROOFSTEP]
simp [Matrix.mul_assoc, nonsing_inv_mul A h]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B✝ : Matrix n n α
B : Matrix n m α
h : IsUnit (det A)
⊢ A⁻¹ * (A * B) = B
[PROOFSTEP]
simp [← Matrix.mul_assoc, nonsing_inv_mul A h]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A✝ B✝ A B C : Matrix n n α
inst✝ : Invertible A
h : A⁻¹ * B = C
⊢ B = A * C
[PROOFSTEP]
rw [← h, mul_inv_cancel_left_of_invertible]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A✝ B✝ A B C : Matrix n n α
inst✝ : Invertible A
h : B = A * C
⊢ A⁻¹ * B = C
[PROOFSTEP]
rw [h, inv_mul_cancel_left_of_invertible]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A✝ B✝ A B C : Matrix n n α
inst✝ : Invertible A
h : B * A⁻¹ = C
⊢ B = C * A
[PROOFSTEP]
rw [← h, inv_mul_cancel_right_of_invertible]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A✝ B✝ A B C : Matrix n n α
inst✝ : Invertible A
h : B = C * A
⊢ B * A⁻¹ = C
[PROOFSTEP]
rw [h, mul_inv_cancel_right_of_invertible]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A B : Matrix n n α
inst✝ : Invertible A
x✝¹ x✝ : Matrix n m α
h : (fun x => A * x) x✝¹ = (fun x => A * x) x✝
⊢ x✝¹ = x✝
[PROOFSTEP]
simpa only [inv_mul_cancel_left_of_invertible] using congr_arg (A⁻¹ * ·) h
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A B : Matrix n n α
inst✝ : Invertible A
a x : Matrix m n α
hax : (fun x => x * A) a = (fun x => x * A) x
⊢ a = x
[PROOFSTEP]
simpa only [mul_inv_cancel_right_of_invertible] using congr_arg (· * A⁻¹) hax
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
⊢ A⁻¹ * A = 1 ∧ A * A⁻¹ = 1 ∨ A⁻¹ = 0
[PROOFSTEP]
by_cases h : IsUnit A.det
[GOAL]
case pos
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h : IsUnit (det A)
⊢ A⁻¹ * A = 1 ∧ A * A⁻¹ = 1 ∨ A⁻¹ = 0
[PROOFSTEP]
exact Or.inl ⟨nonsing_inv_mul _ h, mul_nonsing_inv _ h⟩
[GOAL]
case neg
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h : ¬IsUnit (det A)
⊢ A⁻¹ * A = 1 ∧ A * A⁻¹ = 1 ∨ A⁻¹ = 0
[PROOFSTEP]
exact Or.inr (nonsing_inv_apply_not_isUnit _ h)
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h : IsUnit (det A)
⊢ det A⁻¹ * det A = 1
[PROOFSTEP]
rw [← det_mul, A.nonsing_inv_mul h, det_one]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
⊢ det A⁻¹ = Ring.inverse (det A)
[PROOFSTEP]
by_cases h : IsUnit A.det
[GOAL]
case pos
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h : IsUnit (det A)
⊢ det A⁻¹ = Ring.inverse (det A)
[PROOFSTEP]
cases h.nonempty_invertible
[GOAL]
case pos.intro
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h : IsUnit (det A)
val✝ : Invertible (det A)
⊢ det A⁻¹ = Ring.inverse (det A)
[PROOFSTEP]
letI := invertibleOfDetInvertible A
[GOAL]
case pos.intro
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h : IsUnit (det A)
val✝ : Invertible (det A)
this : Invertible A := invertibleOfDetInvertible A
⊢ det A⁻¹ = Ring.inverse (det A)
[PROOFSTEP]
rw [Ring.inverse_invertible, ← invOf_eq_nonsing_inv, det_invOf]
[GOAL]
case neg
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h : ¬IsUnit (det A)
⊢ det A⁻¹ = Ring.inverse (det A)
[PROOFSTEP]
cases isEmpty_or_nonempty n
[GOAL]
case neg.inl
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h : ¬IsUnit (det A)
h✝ : IsEmpty n
⊢ det A⁻¹ = Ring.inverse (det A)
[PROOFSTEP]
rw [det_isEmpty, det_isEmpty, Ring.inverse_one]
[GOAL]
case neg.inr
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h : ¬IsUnit (det A)
h✝ : Nonempty n
⊢ det A⁻¹ = Ring.inverse (det A)
[PROOFSTEP]
rw [Ring.inverse_non_unit _ h, nonsing_inv_apply_not_isUnit _ h, det_zero ‹_›]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h : IsUnit (det A)
⊢ A⁻¹⁻¹ = 1 * A⁻¹⁻¹
[PROOFSTEP]
rw [Matrix.one_mul]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h : IsUnit (det A)
⊢ 1 * A⁻¹⁻¹ = A * A⁻¹ * A⁻¹⁻¹
[PROOFSTEP]
rw [A.mul_nonsing_inv h]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h : IsUnit (det A)
⊢ A * A⁻¹ * A⁻¹⁻¹ = A
[PROOFSTEP]
rw [Matrix.mul_assoc, A⁻¹.mul_nonsing_inv (A.isUnit_nonsing_inv_det h), Matrix.mul_one]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A✝ B A : Matrix n n α
⊢ IsUnit (det A⁻¹) ↔ IsUnit (det A)
[PROOFSTEP]
rw [Matrix.det_nonsing_inv, isUnit_ring_inverse]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A B : Matrix n n α
inst✝ : Invertible (det A)
⊢ unitOfDetInvertible A = nonsingInvUnit A (_ : IsUnit (det A))
[PROOFSTEP]
ext
[GOAL]
case a.a.h
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A B : Matrix n n α
inst✝ : Invertible (det A)
i✝ x✝ : n
⊢ ↑(unitOfDetInvertible A) i✝ x✝ = ↑(nonsingInvUnit A (_ : IsUnit (det A))) i✝ x✝
[PROOFSTEP]
rfl
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B C : Matrix n n α
h : B * A = 1
g : C * A = 1
⊢ B = C
[PROOFSTEP]
rw [← inv_eq_left_inv h, ← inv_eq_left_inv g]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B C : Matrix n n α
h : A * B = 1
g : A * C = 1
⊢ B = C
[PROOFSTEP]
rw [← inv_eq_right_inv h, ← inv_eq_right_inv g]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B C : Matrix n n α
h : A * B = 1
g : C * A = 1
⊢ B = C
[PROOFSTEP]
rw [← inv_eq_right_inv h, ← inv_eq_left_inv g]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B C : Matrix n n α
h : A⁻¹ = B⁻¹
h' : IsUnit (det A)
⊢ A = B
[PROOFSTEP]
refine' left_inv_eq_left_inv (mul_nonsing_inv _ h') _
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B C : Matrix n n α
h : A⁻¹ = B⁻¹
h' : IsUnit (det A)
⊢ B * A⁻¹ = 1
[PROOFSTEP]
rw [h]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B C : Matrix n n α
h : A⁻¹ = B⁻¹
h' : IsUnit (det A)
⊢ B * B⁻¹ = 1
[PROOFSTEP]
refine' mul_nonsing_inv _ _
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B C : Matrix n n α
h : A⁻¹ = B⁻¹
h' : IsUnit (det A)
⊢ IsUnit (det B)
[PROOFSTEP]
rwa [← isUnit_nonsing_inv_det_iff, ← h, isUnit_nonsing_inv_det_iff]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
⊢ 0⁻¹ = 0
[PROOFSTEP]
cases' subsingleton_or_nontrivial α with ht ht
[GOAL]
case inl
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
ht : Subsingleton α
⊢ 0⁻¹ = 0
[PROOFSTEP]
simp
[GOAL]
case inr
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
ht : Nontrivial α
⊢ 0⁻¹ = 0
[PROOFSTEP]
cases' (Fintype.card n).zero_le.eq_or_lt with hc hc
[GOAL]
case inr.inl
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
ht : Nontrivial α
hc : 0 = Fintype.card n
⊢ 0⁻¹ = 0
[PROOFSTEP]
rw [eq_comm, Fintype.card_eq_zero_iff] at hc
[GOAL]
case inr.inl
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
ht : Nontrivial α
hc : IsEmpty n
⊢ 0⁻¹ = 0
[PROOFSTEP]
haveI := hc
[GOAL]
case inr.inl
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
ht : Nontrivial α
hc this : IsEmpty n
⊢ 0⁻¹ = 0
[PROOFSTEP]
ext i
[GOAL]
case inr.inl.a.h
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
ht : Nontrivial α
hc this : IsEmpty n
i x✝ : n
⊢ 0⁻¹ i x✝ = OfNat.ofNat 0 i x✝
[PROOFSTEP]
exact (IsEmpty.false i).elim
[GOAL]
case inr.inr
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
ht : Nontrivial α
hc : 0 < Fintype.card n
⊢ 0⁻¹ = 0
[PROOFSTEP]
have hn : Nonempty n := Fintype.card_pos_iff.mp hc
[GOAL]
case inr.inr
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
ht : Nontrivial α
hc : 0 < Fintype.card n
hn : Nonempty n
⊢ 0⁻¹ = 0
[PROOFSTEP]
refine' nonsing_inv_apply_not_isUnit _ _
[GOAL]
case inr.inr
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
ht : Nontrivial α
hc : 0 < Fintype.card n
hn : Nonempty n
⊢ ¬IsUnit (det 0)
[PROOFSTEP]
simp [hn]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
src✝¹ : One (Matrix n n α) := one
src✝ : Inv (Matrix n n α) := inv
⊢ 1 * 1 = 1
[PROOFSTEP]
simp
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A B : Matrix n n α
k : α
inst✝ : Invertible k
h : IsUnit (det A)
⊢ ⅟k • A⁻¹ * k • A = 1
[PROOFSTEP]
simp [h, smul_smul]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
k : αˣ
h : IsUnit (det A)
⊢ k⁻¹ • A⁻¹ * k • A = 1
[PROOFSTEP]
simp [h, smul_smul]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A✝ B A : Matrix n n α
h : IsUnit (det A)
⊢ (adjugate A)⁻¹ = (IsUnit.unit h)⁻¹ • A
[PROOFSTEP]
refine' inv_eq_left_inv _
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A✝ B A : Matrix n n α
h : IsUnit (det A)
⊢ (IsUnit.unit h)⁻¹ • A * adjugate A = 1
[PROOFSTEP]
rw [smul_mul, mul_adjugate, Units.smul_def, smul_smul, h.val_inv_mul, one_smul]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α✝ : Type v
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq n
inst✝³ : CommRing α✝
A B : Matrix n n α✝
α : Type u_2
inst✝² : Semiring α
v : n → α
inst✝¹ : Invertible v
inst✝ : Invertible (diagonal v)
⊢ ⅟(diagonal v) = diagonal ⅟v
[PROOFSTEP]
letI := diagonalInvertible v
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α✝ : Type v
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq n
inst✝³ : CommRing α✝
A B : Matrix n n α✝
α : Type u_2
inst✝² : Semiring α
v : n → α
inst✝¹ : Invertible v
inst✝ : Invertible (diagonal v)
this : Invertible (diagonal v) := diagonalInvertible v
⊢ ⅟(diagonal v) = diagonal ⅟v
[PROOFSTEP]
convert (rfl : ⅟(diagonal v) = _)
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A B : Matrix n n α
v : n → α
inst✝ : Invertible (diagonal v)
i : n
⊢ (diag ⅟(diagonal v) * v) i = OfNat.ofNat 1 i
[PROOFSTEP]
letI : Invertible (diagonal v).det := detInvertibleOfInvertible _
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A B : Matrix n n α
v : n → α
inst✝ : Invertible (diagonal v)
i : n
this : Invertible (det (diagonal v)) := detInvertibleOfInvertible (diagonal v)
⊢ (diag ⅟(diagonal v) * v) i = OfNat.ofNat 1 i
[PROOFSTEP]
rw [invOf_eq, diag_smul, adjugate_diagonal, diag_diagonal]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A B : Matrix n n α
v : n → α
inst✝ : Invertible (diagonal v)
i : n
this : Invertible (det (diagonal v)) := detInvertibleOfInvertible (diagonal v)
⊢ ((⅟(det (diagonal v)) • fun i => ∏ j in erase univ i, v j) * v) i = OfNat.ofNat 1 i
[PROOFSTEP]
dsimp
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A B : Matrix n n α
v : n → α
inst✝ : Invertible (diagonal v)
i : n
this : Invertible (det (diagonal v)) := detInvertibleOfInvertible (diagonal v)
⊢ (⅟(det (diagonal v)) * ∏ j in erase univ i, v j) * v i = 1
[PROOFSTEP]
rw [mul_assoc, prod_erase_mul _ _ (Finset.mem_univ _), ← det_diagonal]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A B : Matrix n n α
v : n → α
inst✝ : Invertible (diagonal v)
i : n
this : Invertible (det (diagonal v)) := detInvertibleOfInvertible (diagonal v)
⊢ ⅟(det (diagonal v)) * det (diagonal fun x => v x) = 1
[PROOFSTEP]
exact mul_invOf_self _
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A B : Matrix n n α
v : n → α
inst✝ : Invertible (diagonal v)
i : n
⊢ (v * diag ⅟(diagonal v)) i = OfNat.ofNat 1 i
[PROOFSTEP]
letI : Invertible (diagonal v).det := detInvertibleOfInvertible _
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A B : Matrix n n α
v : n → α
inst✝ : Invertible (diagonal v)
i : n
this : Invertible (det (diagonal v)) := detInvertibleOfInvertible (diagonal v)
⊢ (v * diag ⅟(diagonal v)) i = OfNat.ofNat 1 i
[PROOFSTEP]
rw [invOf_eq, diag_smul, adjugate_diagonal, diag_diagonal]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A B : Matrix n n α
v : n → α
inst✝ : Invertible (diagonal v)
i : n
this : Invertible (det (diagonal v)) := detInvertibleOfInvertible (diagonal v)
⊢ (v * ⅟(det (diagonal v)) • fun i => ∏ j in erase univ i, v j) i = OfNat.ofNat 1 i
[PROOFSTEP]
dsimp
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A B : Matrix n n α
v : n → α
inst✝ : Invertible (diagonal v)
i : n
this : Invertible (det (diagonal v)) := detInvertibleOfInvertible (diagonal v)
⊢ v i * (⅟(det (diagonal v)) * ∏ j in erase univ i, v j) = 1
[PROOFSTEP]
rw [mul_left_comm, mul_prod_erase _ _ (Finset.mem_univ _), ← det_diagonal]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A B : Matrix n n α
v : n → α
inst✝ : Invertible (diagonal v)
i : n
this : Invertible (det (diagonal v)) := detInvertibleOfInvertible (diagonal v)
⊢ ⅟(det (diagonal v)) * det (diagonal fun x => v x) = 1
[PROOFSTEP]
exact mul_invOf_self _
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
v : n → α
⊢ IsUnit (diagonal v) ↔ IsUnit v
[PROOFSTEP]
simp only [← nonempty_invertible_iff_isUnit, (diagonalInvertibleEquivInvertible v).nonempty_congr]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
v : n → α
⊢ (diagonal v)⁻¹ = diagonal (Ring.inverse v)
[PROOFSTEP]
rw [nonsing_inv_eq_ring_inverse]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
v : n → α
⊢ Ring.inverse (diagonal v) = diagonal (Ring.inverse v)
[PROOFSTEP]
by_cases h : IsUnit v
[GOAL]
case pos
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
v : n → α
h : IsUnit v
⊢ Ring.inverse (diagonal v) = diagonal (Ring.inverse v)
[PROOFSTEP]
have := isUnit_diagonal.mpr h
[GOAL]
case pos
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
v : n → α
h : IsUnit v
this : IsUnit (diagonal v)
⊢ Ring.inverse (diagonal v) = diagonal (Ring.inverse v)
[PROOFSTEP]
cases this.nonempty_invertible
[GOAL]
case pos.intro
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
v : n → α
h : IsUnit v
this : IsUnit (diagonal v)
val✝ : Invertible (diagonal v)
⊢ Ring.inverse (diagonal v) = diagonal (Ring.inverse v)
[PROOFSTEP]
cases h.nonempty_invertible
[GOAL]
case pos.intro.intro
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
v : n → α
h : IsUnit v
this : IsUnit (diagonal v)
val✝¹ : Invertible (diagonal v)
val✝ : Invertible v
⊢ Ring.inverse (diagonal v) = diagonal (Ring.inverse v)
[PROOFSTEP]
rw [Ring.inverse_invertible, Ring.inverse_invertible, invOf_diagonal_eq]
[GOAL]
case neg
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
v : n → α
h : ¬IsUnit v
⊢ Ring.inverse (diagonal v) = diagonal (Ring.inverse v)
[PROOFSTEP]
have := isUnit_diagonal.not.mpr h
[GOAL]
case neg
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
v : n → α
h : ¬IsUnit v
this : ¬IsUnit (diagonal v)
⊢ Ring.inverse (diagonal v) = diagonal (Ring.inverse v)
[PROOFSTEP]
rw [Ring.inverse_non_unit _ h, Pi.zero_def, diagonal_zero, Ring.inverse_non_unit _ this]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A✝ B A : Matrix n n α
⊢ A⁻¹⁻¹⁻¹ = A⁻¹
[PROOFSTEP]
by_cases h : IsUnit A.det
[GOAL]
case pos
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A✝ B A : Matrix n n α
h : IsUnit (det A)
⊢ A⁻¹⁻¹⁻¹ = A⁻¹
[PROOFSTEP]
rw [nonsing_inv_nonsing_inv _ h]
[GOAL]
case neg
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A✝ B A : Matrix n n α
h : ¬IsUnit (det A)
⊢ A⁻¹⁻¹⁻¹ = A⁻¹
[PROOFSTEP]
simp [nonsing_inv_apply_not_isUnit _ h]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A✝ B✝ A B : Matrix n n α
⊢ (A * B)⁻¹ = B⁻¹ * A⁻¹
[PROOFSTEP]
simp only [inv_def]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A✝ B✝ A B : Matrix n n α
⊢ Ring.inverse (det (A * B)) • adjugate (A * B) = Ring.inverse (det B) • adjugate B * Ring.inverse (det A) • adjugate A
[PROOFSTEP]
rw [Matrix.smul_mul, Matrix.mul_smul, smul_smul, det_mul, adjugate_mul_distrib, Ring.mul_inverse_rev]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
⊢ (List.prod [])⁻¹ = List.prod (List.map Inv.inv (List.reverse []))
[PROOFSTEP]
rw [List.reverse_nil, List.map_nil, List.prod_nil, inv_one]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A✝ B A : Matrix n n α
Xs : List (Matrix n n α)
⊢ (List.prod (A :: Xs))⁻¹ = List.prod (List.map Inv.inv (List.reverse (A :: Xs)))
[PROOFSTEP]
rw [List.reverse_cons', List.map_concat, List.prod_concat, List.prod_cons, mul_inv_rev, list_prod_inv_reverse Xs]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A✝ B A : Matrix n n α
b : n → α
h : IsUnit (det A)
⊢ det A • mulVec A⁻¹ b = ↑(cramer A) b
[PROOFSTEP]
rw [cramer_eq_adjugate_mulVec, A.nonsing_inv_apply h, ← smul_mulVec_assoc, smul_smul, h.mul_val_inv, one_smul]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A✝ B A : Matrix n n α
b : n → α
h : IsUnit (det A)
⊢ det A • vecMul b A⁻¹ = ↑(cramer Aᵀ) b
[PROOFSTEP]
rw [← A⁻¹.transpose_transpose, vecMul_transpose, transpose_nonsing_inv, ← det_transpose,
  Aᵀ.det_smul_inv_mulVec_eq_cramer _ (isUnit_det_transpose A h)]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq n
inst✝³ : CommRing α
A✝ B : Matrix n n α
inst✝² : Fintype m
inst✝¹ : DecidableEq m
A : Matrix m m α
e₁ e₂ : n ≃ m
inst✝ : Invertible A
⊢ submatrix A ↑e₁ ↑e₂ * submatrix ⅟A ↑e₂ ↑e₁ = 1
[PROOFSTEP]
rw [Matrix.submatrix_mul_equiv, mul_invOf_self, submatrix_one_equiv]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq n
inst✝³ : CommRing α
A✝ B : Matrix n n α
inst✝² : Fintype m
inst✝¹ : DecidableEq m
A : Matrix m m α
e₁ e₂ : n ≃ m
inst✝ : Invertible (submatrix A ↑e₁ ↑e₂)
⊢ A * submatrix ⅟(submatrix A ↑e₁ ↑e₂) ↑e₂.symm ↑e₁.symm = 1
[PROOFSTEP]
have : A = (A.submatrix e₁ e₂).submatrix e₁.symm e₂.symm := by
  simp
    -- Porting note: was
        -- conv in _ * _ =>
        --   congr
        --   rw [this]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq n
inst✝³ : CommRing α
A✝ B : Matrix n n α
inst✝² : Fintype m
inst✝¹ : DecidableEq m
A : Matrix m m α
e₁ e₂ : n ≃ m
inst✝ : Invertible (submatrix A ↑e₁ ↑e₂)
⊢ A = submatrix (submatrix A ↑e₁ ↑e₂) ↑e₁.symm ↑e₂.symm
[PROOFSTEP]
simp
  -- Porting note: was
      -- conv in _ * _ =>
      --   congr
      --   rw [this]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq n
inst✝³ : CommRing α
A✝ B : Matrix n n α
inst✝² : Fintype m
inst✝¹ : DecidableEq m
A : Matrix m m α
e₁ e₂ : n ≃ m
inst✝ : Invertible (submatrix A ↑e₁ ↑e₂)
this : A = submatrix (submatrix A ↑e₁ ↑e₂) ↑e₁.symm ↑e₂.symm
⊢ A * submatrix ⅟(submatrix A ↑e₁ ↑e₂) ↑e₂.symm ↑e₁.symm = 1
[PROOFSTEP]
rw [congr_arg₂ (· * ·) this rfl]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq n
inst✝³ : CommRing α
A✝ B : Matrix n n α
inst✝² : Fintype m
inst✝¹ : DecidableEq m
A : Matrix m m α
e₁ e₂ : n ≃ m
inst✝ : Invertible (submatrix A ↑e₁ ↑e₂)
this : A = submatrix (submatrix A ↑e₁ ↑e₂) ↑e₁.symm ↑e₂.symm
⊢ submatrix (submatrix A ↑e₁ ↑e₂) ↑e₁.symm ↑e₂.symm * submatrix ⅟(submatrix A ↑e₁ ↑e₂) ↑e₂.symm ↑e₁.symm = 1
[PROOFSTEP]
rw [Matrix.submatrix_mul_equiv, mul_invOf_self, submatrix_one_equiv]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing α
A✝ B : Matrix n n α
inst✝³ : Fintype m
inst✝² : DecidableEq m
A : Matrix m m α
e₁ e₂ : n ≃ m
inst✝¹ : Invertible A
inst✝ : Invertible (submatrix A ↑e₁ ↑e₂)
⊢ ⅟(submatrix A ↑e₁ ↑e₂) = submatrix ⅟A ↑e₂ ↑e₁
[PROOFSTEP]
letI := submatrixEquivInvertible A e₁ e₂
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing α
A✝ B : Matrix n n α
inst✝³ : Fintype m
inst✝² : DecidableEq m
A : Matrix m m α
e₁ e₂ : n ≃ m
inst✝¹ : Invertible A
inst✝ : Invertible (submatrix A ↑e₁ ↑e₂)
this : Invertible (submatrix A ↑e₁ ↑e₂) := submatrixEquivInvertible A e₁ e₂
⊢ ⅟(submatrix A ↑e₁ ↑e₂) = submatrix ⅟A ↑e₂ ↑e₁
[PROOFSTEP]
convert (rfl : ⅟(A.submatrix e₁ e₂) = _)
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
A✝ B : Matrix n n α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
e₁ e₂ : n ≃ m
⊢ IsUnit (submatrix A ↑e₁ ↑e₂) ↔ IsUnit A
[PROOFSTEP]
simp only [← nonempty_invertible_iff_isUnit, (submatrixEquivInvertibleEquivInvertible A _ _).nonempty_congr]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
A✝ B : Matrix n n α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
e₁ e₂ : n ≃ m
⊢ (submatrix A ↑e₁ ↑e₂)⁻¹ = submatrix A⁻¹ ↑e₂ ↑e₁
[PROOFSTEP]
by_cases h : IsUnit A
[GOAL]
case pos
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
A✝ B : Matrix n n α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
e₁ e₂ : n ≃ m
h : IsUnit A
⊢ (submatrix A ↑e₁ ↑e₂)⁻¹ = submatrix A⁻¹ ↑e₂ ↑e₁
[PROOFSTEP]
cases h.nonempty_invertible
[GOAL]
case pos.intro
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
A✝ B : Matrix n n α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
e₁ e₂ : n ≃ m
h : IsUnit A
val✝ : Invertible A
⊢ (submatrix A ↑e₁ ↑e₂)⁻¹ = submatrix A⁻¹ ↑e₂ ↑e₁
[PROOFSTEP]
letI := submatrixEquivInvertible A e₁ e₂
[GOAL]
case pos.intro
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
A✝ B : Matrix n n α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
e₁ e₂ : n ≃ m
h : IsUnit A
val✝ : Invertible A
this : Invertible (submatrix A ↑e₁ ↑e₂) := submatrixEquivInvertible A e₁ e₂
⊢ (submatrix A ↑e₁ ↑e₂)⁻¹ = submatrix A⁻¹ ↑e₂ ↑e₁
[PROOFSTEP]
rw [← invOf_eq_nonsing_inv, ← invOf_eq_nonsing_inv, invOf_submatrix_equiv_eq A]
[GOAL]
case neg
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
A✝ B : Matrix n n α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
e₁ e₂ : n ≃ m
h : ¬IsUnit A
⊢ (submatrix A ↑e₁ ↑e₂)⁻¹ = submatrix A⁻¹ ↑e₂ ↑e₁
[PROOFSTEP]
have := (isUnit_submatrix_equiv e₁ e₂).not.mpr h
[GOAL]
case neg
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
A✝ B : Matrix n n α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
e₁ e₂ : n ≃ m
h : ¬IsUnit A
this : ¬IsUnit (submatrix A ↑e₁ ↑e₂)
⊢ (submatrix A ↑e₁ ↑e₂)⁻¹ = submatrix A⁻¹ ↑e₂ ↑e₁
[PROOFSTEP]
simp_rw [nonsing_inv_eq_ring_inverse, Ring.inverse_non_unit _ h, Ring.inverse_non_unit _ this, submatrix_zero,
  Pi.zero_apply]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
A B : Matrix n n α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m m α
h : IsUnit M
N : Matrix m m α
⊢ det (M * N * M⁻¹) = det N
[PROOFSTEP]
rw [← h.unit_spec, ← coe_units_inv, det_units_conj]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
A B : Matrix n n α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m m α
h : IsUnit M
N : Matrix m m α
⊢ det (M⁻¹ * N * M) = det N
[PROOFSTEP]
rw [← h.unit_spec, ← coe_units_inv, det_units_conj']


[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
x y : α
S U Z : Set α
⊢ IsGenericPoint x S ↔ ∀ (y : α), x ⤳ y ↔ y ∈ S
[PROOFSTEP]
simp only [specializes_iff_mem_closure, IsGenericPoint, Set.ext_iff]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
x y : α
S U Z : Set α
h : IsGenericPoint x S
hU : IsOpen U
⊢ Disjoint S U ↔ ¬x ∈ U
[PROOFSTEP]
rw [h.mem_open_set_iff hU, ← not_disjoint_iff_nonempty_inter, Classical.not_not]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
x y : α
S U Z : Set α
h : IsGenericPoint x S
hZ : IsClosed Z
⊢ x ∈ Z ↔ S ⊆ Z
[PROOFSTEP]
rw [← h.def, hZ.closure_subset_iff, singleton_subset_iff]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
x y : α
S U Z : Set α
h : IsGenericPoint x S
f : α → β
hf : Continuous f
⊢ IsGenericPoint (f x) (closure (f '' S))
[PROOFSTEP]
rw [isGenericPoint_def, ← h.def, ← image_singleton, closure_image_closure hf]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
x y : α
S U Z : Set α
hS : IsClosed S
hxS : x ∈ S
⊢ IsGenericPoint x S ↔ ∀ (Z : Set α), IsClosed Z → x ∈ Z → S ⊆ Z
[PROOFSTEP]
have : closure { x } ⊆ S := closure_minimal (singleton_subset_iff.2 hxS) hS
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
x y : α
S U Z : Set α
hS : IsClosed S
hxS : x ∈ S
this : closure {x} ⊆ S
⊢ IsGenericPoint x S ↔ ∀ (Z : Set α), IsClosed Z → x ∈ Z → S ⊆ Z
[PROOFSTEP]
simp_rw [IsGenericPoint, subset_antisymm_iff, this, true_and_iff, closure, subset_sInter_iff, mem_setOf_eq, and_imp,
  singleton_subset_iff]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : QuasiSober α
inst✝ : IrreducibleSpace α
⊢ IsGenericPoint (genericPoint α) ⊤
[PROOFSTEP]
simpa using (IrreducibleSpace.isIrreducible_univ α).genericPoint_spec
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : QuasiSober α
inst✝ : IrreducibleSpace α
x : α
⊢ x ∈ closure univ
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : QuasiSober α
inst✝ : T0Space α
x : α
⊢ IsGenericPoint x (closure (closure {x}))
[PROOFSTEP]
rw [closure_closure]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : QuasiSober α
inst✝ : T0Space α
x : α
⊢ IsGenericPoint x (closure {x})
[PROOFSTEP]
exact isGenericPoint_closure
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : QuasiSober α
inst✝ : T0Space α
⊢ ∀ {a b : ↑{s | IsIrreducible s ∧ IsClosed s}},
    ↑{ toFun := fun s => IsIrreducible.genericPoint (_ : IsIrreducible ↑s),
              invFun := fun x =>
                { val := closure {x}, property := (_ : IsIrreducible (closure {x}) ∧ IsClosed (closure {x})) },
              left_inv :=
                (_ :
                  ∀ (s : ↑{s | IsIrreducible s ∧ IsClosed s}),
                    (fun x =>
                          { val := closure {x},
                            property := (_ : IsIrreducible (closure {x}) ∧ IsClosed (closure {x})) })
                        ((fun s => IsIrreducible.genericPoint (_ : IsIrreducible ↑s)) s) =
                      s),
              right_inv := (_ : ∀ (x : α), IsIrreducible.genericPoint (_ : IsIrreducible (closure {x})) = x) }
          a ≤
        ↑{ toFun := fun s => IsIrreducible.genericPoint (_ : IsIrreducible ↑s),
              invFun := fun x =>
                { val := closure {x}, property := (_ : IsIrreducible (closure {x}) ∧ IsClosed (closure {x})) },
              left_inv :=
                (_ :
                  ∀ (s : ↑{s | IsIrreducible s ∧ IsClosed s}),
                    (fun x =>
                          { val := closure {x},
                            property := (_ : IsIrreducible (closure {x}) ∧ IsClosed (closure {x})) })
                        ((fun s => IsIrreducible.genericPoint (_ : IsIrreducible ↑s)) s) =
                      s),
              right_inv := (_ : ∀ (x : α), IsIrreducible.genericPoint (_ : IsIrreducible (closure {x})) = x) }
          b ↔
      a ≤ b
[PROOFSTEP]
rintro ⟨s, hs⟩ ⟨t, ht⟩
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : QuasiSober α
inst✝ : T0Space α
s : Set α
hs : s ∈ {s | IsIrreducible s ∧ IsClosed s}
t : Set α
ht : t ∈ {s | IsIrreducible s ∧ IsClosed s}
⊢ ↑{ toFun := fun s => IsIrreducible.genericPoint (_ : IsIrreducible ↑s),
            invFun := fun x =>
              { val := closure {x}, property := (_ : IsIrreducible (closure {x}) ∧ IsClosed (closure {x})) },
            left_inv :=
              (_ :
                ∀ (s : ↑{s | IsIrreducible s ∧ IsClosed s}),
                  (fun x =>
                        { val := closure {x}, property := (_ : IsIrreducible (closure {x}) ∧ IsClosed (closure {x})) })
                      ((fun s => IsIrreducible.genericPoint (_ : IsIrreducible ↑s)) s) =
                    s),
            right_inv := (_ : ∀ (x : α), IsIrreducible.genericPoint (_ : IsIrreducible (closure {x})) = x) }
        { val := s, property := hs } ≤
      ↑{ toFun := fun s => IsIrreducible.genericPoint (_ : IsIrreducible ↑s),
            invFun := fun x =>
              { val := closure {x}, property := (_ : IsIrreducible (closure {x}) ∧ IsClosed (closure {x})) },
            left_inv :=
              (_ :
                ∀ (s : ↑{s | IsIrreducible s ∧ IsClosed s}),
                  (fun x =>
                        { val := closure {x}, property := (_ : IsIrreducible (closure {x}) ∧ IsClosed (closure {x})) })
                      ((fun s => IsIrreducible.genericPoint (_ : IsIrreducible ↑s)) s) =
                    s),
            right_inv := (_ : ∀ (x : α), IsIrreducible.genericPoint (_ : IsIrreducible (closure {x})) = x) }
        { val := t, property := ht } ↔
    { val := s, property := hs } ≤ { val := t, property := ht }
[PROOFSTEP]
refine specializes_iff_closure_subset.trans ?_
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : QuasiSober α
inst✝ : T0Space α
s : Set α
hs : s ∈ {s | IsIrreducible s ∧ IsClosed s}
t : Set α
ht : t ∈ {s | IsIrreducible s ∧ IsClosed s}
⊢ closure
        {↑{ toFun := fun s => IsIrreducible.genericPoint (_ : IsIrreducible ↑s),
                invFun := fun x =>
                  { val := closure {x}, property := (_ : IsIrreducible (closure {x}) ∧ IsClosed (closure {x})) },
                left_inv :=
                  (_ :
                    ∀ (s : ↑{s | IsIrreducible s ∧ IsClosed s}),
                      (fun x =>
                            { val := closure {x},
                              property := (_ : IsIrreducible (closure {x}) ∧ IsClosed (closure {x})) })
                          ((fun s => IsIrreducible.genericPoint (_ : IsIrreducible ↑s)) s) =
                        s),
                right_inv := (_ : ∀ (x : α), IsIrreducible.genericPoint (_ : IsIrreducible (closure {x})) = x) }
            { val := s, property := hs }} ⊆
      closure
        {↑{ toFun := fun s => IsIrreducible.genericPoint (_ : IsIrreducible ↑s),
                invFun := fun x =>
                  { val := closure {x}, property := (_ : IsIrreducible (closure {x}) ∧ IsClosed (closure {x})) },
                left_inv :=
                  (_ :
                    ∀ (s : ↑{s | IsIrreducible s ∧ IsClosed s}),
                      (fun x =>
                            { val := closure {x},
                              property := (_ : IsIrreducible (closure {x}) ∧ IsClosed (closure {x})) })
                          ((fun s => IsIrreducible.genericPoint (_ : IsIrreducible ↑s)) s) =
                        s),
                right_inv := (_ : ∀ (x : α), IsIrreducible.genericPoint (_ : IsIrreducible (closure {x})) = x) }
            { val := t, property := ht }} ↔
    { val := s, property := hs } ≤ { val := t, property := ht }
[PROOFSTEP]
simp [hs.2.closure_eq, ht.2.closure_eq]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
hf : ClosedEmbedding f
inst✝ : QuasiSober β
S✝ : Set α
hS : IsIrreducible S✝
hS' : IsClosed S✝
⊢ ∃ x, IsGenericPoint x S✝
[PROOFSTEP]
have hS'' := hS.image f hf.continuous.continuousOn
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
hf : ClosedEmbedding f
inst✝ : QuasiSober β
S✝ : Set α
hS : IsIrreducible S✝
hS' : IsClosed S✝
hS'' : IsIrreducible (f '' S✝)
⊢ ∃ x, IsGenericPoint x S✝
[PROOFSTEP]
obtain ⟨x, hx⟩ := QuasiSober.sober hS'' (hf.isClosedMap _ hS')
[GOAL]
case intro
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
hf : ClosedEmbedding f
inst✝ : QuasiSober β
S✝ : Set α
hS : IsIrreducible S✝
hS' : IsClosed S✝
hS'' : IsIrreducible (f '' S✝)
x : β
hx : IsGenericPoint x (f '' S✝)
⊢ ∃ x, IsGenericPoint x S✝
[PROOFSTEP]
obtain ⟨y, -, rfl⟩ := hx.mem
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
hf : ClosedEmbedding f
inst✝ : QuasiSober β
S✝ : Set α
hS : IsIrreducible S✝
hS' : IsClosed S✝
hS'' : IsIrreducible (f '' S✝)
y : α
hx : IsGenericPoint (f y) (f '' S✝)
⊢ ∃ x, IsGenericPoint x S✝
[PROOFSTEP]
use y
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
hf : ClosedEmbedding f
inst✝ : QuasiSober β
S✝ : Set α
hS : IsIrreducible S✝
hS' : IsClosed S✝
hS'' : IsIrreducible (f '' S✝)
y : α
hx : IsGenericPoint (f y) (f '' S✝)
⊢ IsGenericPoint y S✝
[PROOFSTEP]
apply image_injective.mpr hf.inj
[GOAL]
case h.a
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
hf : ClosedEmbedding f
inst✝ : QuasiSober β
S✝ : Set α
hS : IsIrreducible S✝
hS' : IsClosed S✝
hS'' : IsIrreducible (f '' S✝)
y : α
hx : IsGenericPoint (f y) (f '' S✝)
⊢ f '' closure {y} = f '' S✝
[PROOFSTEP]
rw [← hx.def, ← hf.closure_image_eq, image_singleton]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
hf : OpenEmbedding f
inst✝ : QuasiSober β
S✝ : Set α
hS : IsIrreducible S✝
hS' : IsClosed S✝
⊢ ∃ x, IsGenericPoint x S✝
[PROOFSTEP]
have hS'' := hS.image f hf.continuous.continuousOn
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
hf : OpenEmbedding f
inst✝ : QuasiSober β
S✝ : Set α
hS : IsIrreducible S✝
hS' : IsClosed S✝
hS'' : IsIrreducible (f '' S✝)
⊢ ∃ x, IsGenericPoint x S✝
[PROOFSTEP]
obtain ⟨x, hx⟩ := QuasiSober.sober hS''.closure isClosed_closure
[GOAL]
case intro
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
hf : OpenEmbedding f
inst✝ : QuasiSober β
S✝ : Set α
hS : IsIrreducible S✝
hS' : IsClosed S✝
hS'' : IsIrreducible (f '' S✝)
x : β
hx : IsGenericPoint x (closure (f '' S✝))
⊢ ∃ x, IsGenericPoint x S✝
[PROOFSTEP]
obtain ⟨T, hT, rfl⟩ := hf.toInducing.isClosed_iff.mp hS'
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
hf : OpenEmbedding f
inst✝ : QuasiSober β
x : β
T : Set β
hT : IsClosed T
hS : IsIrreducible (f ⁻¹' T)
hS' : IsClosed (f ⁻¹' T)
hS'' : IsIrreducible (f '' (f ⁻¹' T))
hx : IsGenericPoint x (closure (f '' (f ⁻¹' T)))
⊢ ∃ x, IsGenericPoint x (f ⁻¹' T)
[PROOFSTEP]
rw [image_preimage_eq_inter_range] at hx hS''
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
hf : OpenEmbedding f
inst✝ : QuasiSober β
x : β
T : Set β
hT : IsClosed T
hS : IsIrreducible (f ⁻¹' T)
hS' : IsClosed (f ⁻¹' T)
hS'' : IsIrreducible (T ∩ range f)
hx : IsGenericPoint x (closure (T ∩ range f))
⊢ ∃ x, IsGenericPoint x (f ⁻¹' T)
[PROOFSTEP]
have hxT : x ∈ T := by
  rw [← hT.closure_eq]
  exact closure_mono (inter_subset_left _ _) hx.mem
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
hf : OpenEmbedding f
inst✝ : QuasiSober β
x : β
T : Set β
hT : IsClosed T
hS : IsIrreducible (f ⁻¹' T)
hS' : IsClosed (f ⁻¹' T)
hS'' : IsIrreducible (T ∩ range f)
hx : IsGenericPoint x (closure (T ∩ range f))
⊢ x ∈ T
[PROOFSTEP]
rw [← hT.closure_eq]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
hf : OpenEmbedding f
inst✝ : QuasiSober β
x : β
T : Set β
hT : IsClosed T
hS : IsIrreducible (f ⁻¹' T)
hS' : IsClosed (f ⁻¹' T)
hS'' : IsIrreducible (T ∩ range f)
hx : IsGenericPoint x (closure (T ∩ range f))
⊢ x ∈ closure T
[PROOFSTEP]
exact closure_mono (inter_subset_left _ _) hx.mem
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
hf : OpenEmbedding f
inst✝ : QuasiSober β
x : β
T : Set β
hT : IsClosed T
hS : IsIrreducible (f ⁻¹' T)
hS' : IsClosed (f ⁻¹' T)
hS'' : IsIrreducible (T ∩ range f)
hx : IsGenericPoint x (closure (T ∩ range f))
hxT : x ∈ T
⊢ ∃ x, IsGenericPoint x (f ⁻¹' T)
[PROOFSTEP]
obtain ⟨y, rfl⟩ : x ∈ range f := by
  rw [hx.mem_open_set_iff hf.open_range]
  refine' Nonempty.mono _ hS''.1
  simpa using subset_closure
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
hf : OpenEmbedding f
inst✝ : QuasiSober β
x : β
T : Set β
hT : IsClosed T
hS : IsIrreducible (f ⁻¹' T)
hS' : IsClosed (f ⁻¹' T)
hS'' : IsIrreducible (T ∩ range f)
hx : IsGenericPoint x (closure (T ∩ range f))
hxT : x ∈ T
⊢ x ∈ range f
[PROOFSTEP]
rw [hx.mem_open_set_iff hf.open_range]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
hf : OpenEmbedding f
inst✝ : QuasiSober β
x : β
T : Set β
hT : IsClosed T
hS : IsIrreducible (f ⁻¹' T)
hS' : IsClosed (f ⁻¹' T)
hS'' : IsIrreducible (T ∩ range f)
hx : IsGenericPoint x (closure (T ∩ range f))
hxT : x ∈ T
⊢ Set.Nonempty (closure (T ∩ range f) ∩ range f)
[PROOFSTEP]
refine' Nonempty.mono _ hS''.1
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
hf : OpenEmbedding f
inst✝ : QuasiSober β
x : β
T : Set β
hT : IsClosed T
hS : IsIrreducible (f ⁻¹' T)
hS' : IsClosed (f ⁻¹' T)
hS'' : IsIrreducible (T ∩ range f)
hx : IsGenericPoint x (closure (T ∩ range f))
hxT : x ∈ T
⊢ T ∩ range f ⊆ closure (T ∩ range f) ∩ range f
[PROOFSTEP]
simpa using subset_closure
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
hf : OpenEmbedding f
inst✝ : QuasiSober β
T : Set β
hT : IsClosed T
hS : IsIrreducible (f ⁻¹' T)
hS' : IsClosed (f ⁻¹' T)
hS'' : IsIrreducible (T ∩ range f)
y : α
hx : IsGenericPoint (f y) (closure (T ∩ range f))
hxT : f y ∈ T
⊢ ∃ x, IsGenericPoint x (f ⁻¹' T)
[PROOFSTEP]
use y
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
hf : OpenEmbedding f
inst✝ : QuasiSober β
T : Set β
hT : IsClosed T
hS : IsIrreducible (f ⁻¹' T)
hS' : IsClosed (f ⁻¹' T)
hS'' : IsIrreducible (T ∩ range f)
y : α
hx : IsGenericPoint (f y) (closure (T ∩ range f))
hxT : f y ∈ T
⊢ IsGenericPoint y (f ⁻¹' T)
[PROOFSTEP]
change _ = _
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
hf : OpenEmbedding f
inst✝ : QuasiSober β
T : Set β
hT : IsClosed T
hS : IsIrreducible (f ⁻¹' T)
hS' : IsClosed (f ⁻¹' T)
hS'' : IsIrreducible (T ∩ range f)
y : α
hx : IsGenericPoint (f y) (closure (T ∩ range f))
hxT : f y ∈ T
⊢ closure {y} = f ⁻¹' T
[PROOFSTEP]
rw [hf.toEmbedding.closure_eq_preimage_closure_image, image_singleton, show _ = _ from hx]
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
hf : OpenEmbedding f
inst✝ : QuasiSober β
T : Set β
hT : IsClosed T
hS : IsIrreducible (f ⁻¹' T)
hS' : IsClosed (f ⁻¹' T)
hS'' : IsIrreducible (T ∩ range f)
y : α
hx : IsGenericPoint (f y) (closure (T ∩ range f))
hxT : f y ∈ T
⊢ f ⁻¹' closure (T ∩ range f) = f ⁻¹' T
[PROOFSTEP]
apply image_injective.mpr hf.inj
[GOAL]
case h.a
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
hf : OpenEmbedding f
inst✝ : QuasiSober β
T : Set β
hT : IsClosed T
hS : IsIrreducible (f ⁻¹' T)
hS' : IsClosed (f ⁻¹' T)
hS'' : IsIrreducible (T ∩ range f)
y : α
hx : IsGenericPoint (f y) (closure (T ∩ range f))
hxT : f y ∈ T
⊢ f '' (f ⁻¹' closure (T ∩ range f)) = f '' (f ⁻¹' T)
[PROOFSTEP]
ext z
[GOAL]
case h.a.h
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
hf : OpenEmbedding f
inst✝ : QuasiSober β
T : Set β
hT : IsClosed T
hS : IsIrreducible (f ⁻¹' T)
hS' : IsClosed (f ⁻¹' T)
hS'' : IsIrreducible (T ∩ range f)
y : α
hx : IsGenericPoint (f y) (closure (T ∩ range f))
hxT : f y ∈ T
z : β
⊢ z ∈ f '' (f ⁻¹' closure (T ∩ range f)) ↔ z ∈ f '' (f ⁻¹' T)
[PROOFSTEP]
simp only [image_preimage_eq_inter_range, mem_inter_iff, and_congr_left_iff]
[GOAL]
case h.a.h
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
hf : OpenEmbedding f
inst✝ : QuasiSober β
T : Set β
hT : IsClosed T
hS : IsIrreducible (f ⁻¹' T)
hS' : IsClosed (f ⁻¹' T)
hS'' : IsIrreducible (T ∩ range f)
y : α
hx : IsGenericPoint (f y) (closure (T ∩ range f))
hxT : f y ∈ T
z : β
⊢ z ∈ range f → (z ∈ closure (T ∩ range f) ↔ z ∈ T)
[PROOFSTEP]
exact fun hy => ⟨fun h => hT.closure_eq ▸ closure_mono (inter_subset_left _ _) h, fun h => subset_closure ⟨h, hy⟩⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
S : Set (Set α)
hS : ∀ (s : ↑S), IsOpen ↑s
hS' : ∀ (s : ↑S), QuasiSober ↑↑s
hS'' : ⋃₀ S = ⊤
⊢ QuasiSober α
[PROOFSTEP]
rw [quasiSober_iff]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
S : Set (Set α)
hS : ∀ (s : ↑S), IsOpen ↑s
hS' : ∀ (s : ↑S), QuasiSober ↑↑s
hS'' : ⋃₀ S = ⊤
⊢ ∀ {S : Set α}, IsIrreducible S → IsClosed S → ∃ x, IsGenericPoint x S
[PROOFSTEP]
intro t h h'
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
S : Set (Set α)
hS : ∀ (s : ↑S), IsOpen ↑s
hS' : ∀ (s : ↑S), QuasiSober ↑↑s
hS'' : ⋃₀ S = ⊤
t : Set α
h : IsIrreducible t
h' : IsClosed t
⊢ ∃ x, IsGenericPoint x t
[PROOFSTEP]
obtain ⟨x, hx⟩ := h.1
[GOAL]
case intro
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
S : Set (Set α)
hS : ∀ (s : ↑S), IsOpen ↑s
hS' : ∀ (s : ↑S), QuasiSober ↑↑s
hS'' : ⋃₀ S = ⊤
t : Set α
h : IsIrreducible t
h' : IsClosed t
x : α
hx : x ∈ t
⊢ ∃ x, IsGenericPoint x t
[PROOFSTEP]
obtain ⟨U, hU, hU'⟩ : x ∈ ⋃₀ S := by
  rw [hS'']
  trivial
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
S : Set (Set α)
hS : ∀ (s : ↑S), IsOpen ↑s
hS' : ∀ (s : ↑S), QuasiSober ↑↑s
hS'' : ⋃₀ S = ⊤
t : Set α
h : IsIrreducible t
h' : IsClosed t
x : α
hx : x ∈ t
⊢ x ∈ ⋃₀ S
[PROOFSTEP]
rw [hS'']
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
S : Set (Set α)
hS : ∀ (s : ↑S), IsOpen ↑s
hS' : ∀ (s : ↑S), QuasiSober ↑↑s
hS'' : ⋃₀ S = ⊤
t : Set α
h : IsIrreducible t
h' : IsClosed t
x : α
hx : x ∈ t
⊢ x ∈ ⊤
[PROOFSTEP]
trivial
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
S : Set (Set α)
hS : ∀ (s : ↑S), IsOpen ↑s
hS' : ∀ (s : ↑S), QuasiSober ↑↑s
hS'' : ⋃₀ S = ⊤
t : Set α
h : IsIrreducible t
h' : IsClosed t
x : α
hx : x ∈ t
U : Set α
hU : U ∈ S
hU' : x ∈ U
⊢ ∃ x, IsGenericPoint x t
[PROOFSTEP]
haveI : QuasiSober U := hS' ⟨U, hU⟩
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
S : Set (Set α)
hS : ∀ (s : ↑S), IsOpen ↑s
hS' : ∀ (s : ↑S), QuasiSober ↑↑s
hS'' : ⋃₀ S = ⊤
t : Set α
h : IsIrreducible t
h' : IsClosed t
x : α
hx : x ∈ t
U : Set α
hU : U ∈ S
hU' : x ∈ U
this : QuasiSober ↑U
⊢ ∃ x, IsGenericPoint x t
[PROOFSTEP]
have H : IsPreirreducible ((↑) ⁻¹' t : Set U) := h.2.preimage (hS ⟨U, hU⟩).openEmbedding_subtype_val
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
S : Set (Set α)
hS : ∀ (s : ↑S), IsOpen ↑s
hS' : ∀ (s : ↑S), QuasiSober ↑↑s
hS'' : ⋃₀ S = ⊤
t : Set α
h : IsIrreducible t
h' : IsClosed t
x : α
hx : x ∈ t
U : Set α
hU : U ∈ S
hU' : x ∈ U
this : QuasiSober ↑U
H : IsPreirreducible (Subtype.val ⁻¹' t)
⊢ ∃ x, IsGenericPoint x t
[PROOFSTEP]
replace H : IsIrreducible ((↑) ⁻¹' t : Set U) := ⟨⟨⟨x, hU'⟩, by simpa using hx⟩, H⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
S : Set (Set α)
hS : ∀ (s : ↑S), IsOpen ↑s
hS' : ∀ (s : ↑S), QuasiSober ↑↑s
hS'' : ⋃₀ S = ⊤
t : Set α
h : IsIrreducible t
h' : IsClosed t
x : α
hx : x ∈ t
U : Set α
hU : U ∈ S
hU' : x ∈ U
this : QuasiSober ↑U
H : IsPreirreducible (Subtype.val ⁻¹' t)
⊢ { val := x, property := hU' } ∈ Subtype.val ⁻¹' t
[PROOFSTEP]
simpa using hx
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
S : Set (Set α)
hS : ∀ (s : ↑S), IsOpen ↑s
hS' : ∀ (s : ↑S), QuasiSober ↑↑s
hS'' : ⋃₀ S = ⊤
t : Set α
h : IsIrreducible t
h' : IsClosed t
x : α
hx : x ∈ t
U : Set α
hU : U ∈ S
hU' : x ∈ U
this : QuasiSober ↑U
H : IsIrreducible (Subtype.val ⁻¹' t)
⊢ ∃ x, IsGenericPoint x t
[PROOFSTEP]
use H.genericPoint
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
S : Set (Set α)
hS : ∀ (s : ↑S), IsOpen ↑s
hS' : ∀ (s : ↑S), QuasiSober ↑↑s
hS'' : ⋃₀ S = ⊤
t : Set α
h : IsIrreducible t
h' : IsClosed t
x : α
hx : x ∈ t
U : Set α
hU : U ∈ S
hU' : x ∈ U
this : QuasiSober ↑U
H : IsIrreducible (Subtype.val ⁻¹' t)
⊢ IsGenericPoint (↑(IsIrreducible.genericPoint H)) t
[PROOFSTEP]
have := continuous_subtype_val.closure_preimage_subset _ H.genericPoint_spec.mem
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
S : Set (Set α)
hS : ∀ (s : ↑S), IsOpen ↑s
hS' : ∀ (s : ↑S), QuasiSober ↑↑s
hS'' : ⋃₀ S = ⊤
t : Set α
h : IsIrreducible t
h' : IsClosed t
x : α
hx : x ∈ t
U : Set α
hU : U ∈ S
hU' : x ∈ U
this✝ : QuasiSober ↑U
H : IsIrreducible (Subtype.val ⁻¹' t)
this : IsIrreducible.genericPoint H ∈ Subtype.val ⁻¹' closure t
⊢ IsGenericPoint (↑(IsIrreducible.genericPoint H)) t
[PROOFSTEP]
rw [h'.closure_eq] at this
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
S : Set (Set α)
hS : ∀ (s : ↑S), IsOpen ↑s
hS' : ∀ (s : ↑S), QuasiSober ↑↑s
hS'' : ⋃₀ S = ⊤
t : Set α
h : IsIrreducible t
h' : IsClosed t
x : α
hx : x ∈ t
U : Set α
hU : U ∈ S
hU' : x ∈ U
this✝ : QuasiSober ↑U
H : IsIrreducible (Subtype.val ⁻¹' t)
this : IsIrreducible.genericPoint H ∈ Subtype.val ⁻¹' t
⊢ IsGenericPoint (↑(IsIrreducible.genericPoint H)) t
[PROOFSTEP]
apply le_antisymm
[GOAL]
case h.a
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
S : Set (Set α)
hS : ∀ (s : ↑S), IsOpen ↑s
hS' : ∀ (s : ↑S), QuasiSober ↑↑s
hS'' : ⋃₀ S = ⊤
t : Set α
h : IsIrreducible t
h' : IsClosed t
x : α
hx : x ∈ t
U : Set α
hU : U ∈ S
hU' : x ∈ U
this✝ : QuasiSober ↑U
H : IsIrreducible (Subtype.val ⁻¹' t)
this : IsIrreducible.genericPoint H ∈ Subtype.val ⁻¹' t
⊢ closure {↑(IsIrreducible.genericPoint H)} ≤ t
[PROOFSTEP]
apply h'.closure_subset_iff.mpr
[GOAL]
case h.a
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
S : Set (Set α)
hS : ∀ (s : ↑S), IsOpen ↑s
hS' : ∀ (s : ↑S), QuasiSober ↑↑s
hS'' : ⋃₀ S = ⊤
t : Set α
h : IsIrreducible t
h' : IsClosed t
x : α
hx : x ∈ t
U : Set α
hU : U ∈ S
hU' : x ∈ U
this✝ : QuasiSober ↑U
H : IsIrreducible (Subtype.val ⁻¹' t)
this : IsIrreducible.genericPoint H ∈ Subtype.val ⁻¹' t
⊢ {↑(IsIrreducible.genericPoint H)} ⊆ t
[PROOFSTEP]
simpa using this
[GOAL]
case h.a
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
S : Set (Set α)
hS : ∀ (s : ↑S), IsOpen ↑s
hS' : ∀ (s : ↑S), QuasiSober ↑↑s
hS'' : ⋃₀ S = ⊤
t : Set α
h : IsIrreducible t
h' : IsClosed t
x : α
hx : x ∈ t
U : Set α
hU : U ∈ S
hU' : x ∈ U
this✝ : QuasiSober ↑U
H : IsIrreducible (Subtype.val ⁻¹' t)
this : IsIrreducible.genericPoint H ∈ Subtype.val ⁻¹' t
⊢ t ≤ closure {↑(IsIrreducible.genericPoint H)}
[PROOFSTEP]
rw [← image_singleton, ← closure_image_closure continuous_subtype_val, H.genericPoint_spec.def]
[GOAL]
case h.a
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
S : Set (Set α)
hS : ∀ (s : ↑S), IsOpen ↑s
hS' : ∀ (s : ↑S), QuasiSober ↑↑s
hS'' : ⋃₀ S = ⊤
t : Set α
h : IsIrreducible t
h' : IsClosed t
x : α
hx : x ∈ t
U : Set α
hU : U ∈ S
hU' : x ∈ U
this✝ : QuasiSober ↑U
H : IsIrreducible (Subtype.val ⁻¹' t)
this : IsIrreducible.genericPoint H ∈ Subtype.val ⁻¹' t
⊢ t ≤ closure (Subtype.val '' closure (Subtype.val ⁻¹' t))
[PROOFSTEP]
refine' (subset_closure_inter_of_isPreirreducible_of_isOpen h.2 (hS ⟨U, hU⟩) ⟨x, hx, hU'⟩).trans (closure_mono _)
[GOAL]
case h.a
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
S : Set (Set α)
hS : ∀ (s : ↑S), IsOpen ↑s
hS' : ∀ (s : ↑S), QuasiSober ↑↑s
hS'' : ⋃₀ S = ⊤
t : Set α
h : IsIrreducible t
h' : IsClosed t
x : α
hx : x ∈ t
U : Set α
hU : U ∈ S
hU' : x ∈ U
this✝ : QuasiSober ↑U
H : IsIrreducible (Subtype.val ⁻¹' t)
this : IsIrreducible.genericPoint H ∈ Subtype.val ⁻¹' t
⊢ t ∩ ↑{ val := U, property := hU } ⊆ Subtype.val '' closure (Subtype.val ⁻¹' t)
[PROOFSTEP]
rw [← Subtype.image_preimage_coe]
[GOAL]
case h.a
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
S : Set (Set α)
hS : ∀ (s : ↑S), IsOpen ↑s
hS' : ∀ (s : ↑S), QuasiSober ↑↑s
hS'' : ⋃₀ S = ⊤
t : Set α
h : IsIrreducible t
h' : IsClosed t
x : α
hx : x ∈ t
U : Set α
hU : U ∈ S
hU' : x ∈ U
this✝ : QuasiSober ↑U
H : IsIrreducible (Subtype.val ⁻¹' t)
this : IsIrreducible.genericPoint H ∈ Subtype.val ⁻¹' t
⊢ Subtype.val '' (Subtype.val ⁻¹' t) ⊆ Subtype.val '' closure (Subtype.val ⁻¹' t)
[PROOFSTEP]
exact Set.image_subset _ subset_closure
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T2Space α
S✝ : Set α
h : IsIrreducible S✝
x✝ : IsClosed S✝
⊢ ∃ x, IsGenericPoint x S✝
[PROOFSTEP]
obtain ⟨x, rfl⟩ := isIrreducible_iff_singleton.mp h
[GOAL]
case intro
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T2Space α
x : α
h : IsIrreducible {x}
x✝ : IsClosed {x}
⊢ ∃ x_1, IsGenericPoint x_1 {x}
[PROOFSTEP]
exact ⟨x, closure_singleton⟩


[GOAL]
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace X
s : Set X
a : X
⊢ a ∈ closure s ↔ ∃ x, (∀ (n : ℕ), x n ∈ s) ∧ Tendsto x atTop (𝓝 a)
[PROOFSTEP]
rw [← seqClosure_eq_closure]
[GOAL]
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace X
s : Set X
a : X
⊢ a ∈ seqClosure s ↔ ∃ x, (∀ (n : ℕ), x n ∈ s) ∧ Tendsto x atTop (𝓝 a)
[PROOFSTEP]
rfl
[GOAL]
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace X
f : X → Y
a : X
b : Y
⊢ Tendsto f (𝓝 a) (𝓝 b) ↔ ∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 b)
[PROOFSTEP]
refine' ⟨fun hf u hu => hf.comp hu, fun h => ((nhds_basis_closeds _).tendsto_iff (nhds_basis_closeds _)).2 _⟩
[GOAL]
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace X
f : X → Y
a : X
b : Y
h : ∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 b)
⊢ ∀ (ib : Set Y), ¬b ∈ ib ∧ IsClosed ib → ∃ ia, (¬a ∈ ia ∧ IsClosed ia) ∧ ∀ (x : X), x ∈ iaᶜ → f x ∈ ibᶜ
[PROOFSTEP]
rintro s ⟨hbs, hsc⟩
[GOAL]
case intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace X
f : X → Y
a : X
b : Y
h : ∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 b)
s : Set Y
hbs : ¬b ∈ s
hsc : IsClosed s
⊢ ∃ ia, (¬a ∈ ia ∧ IsClosed ia) ∧ ∀ (x : X), x ∈ iaᶜ → f x ∈ sᶜ
[PROOFSTEP]
refine' ⟨closure (f ⁻¹' s), ⟨mt _ hbs, isClosed_closure⟩, fun x => mt fun hx => subset_closure hx⟩
[GOAL]
case intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace X
f : X → Y
a : X
b : Y
h : ∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 b)
s : Set Y
hbs : ¬b ∈ s
hsc : IsClosed s
⊢ a ∈ closure (f ⁻¹' s) → b ∈ s
[PROOFSTEP]
rw [← seqClosure_eq_closure]
[GOAL]
case intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace X
f : X → Y
a : X
b : Y
h : ∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 b)
s : Set Y
hbs : ¬b ∈ s
hsc : IsClosed s
⊢ a ∈ seqClosure (f ⁻¹' s) → b ∈ s
[PROOFSTEP]
rintro ⟨u, hus, hu⟩
[GOAL]
case intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace X
f : X → Y
a : X
b : Y
h : ∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 b)
s : Set Y
hbs : ¬b ∈ s
hsc : IsClosed s
u : ℕ → X
hus : ∀ (n : ℕ), u n ∈ f ⁻¹' s
hu : Tendsto u atTop (𝓝 a)
⊢ b ∈ s
[PROOFSTEP]
exact hsc.mem_of_tendsto (h u hu) (eventually_of_forall hus)
[GOAL]
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h :
  ∀ (f : X → Prop) (a : X), (∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 (f a))) → ContinuousAt f a
⊢ FrechetUrysohnSpace X
[PROOFSTEP]
refine ⟨fun s x hcx => ?_⟩
[GOAL]
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h :
  ∀ (f : X → Prop) (a : X), (∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 (f a))) → ContinuousAt f a
s : Set X
x : X
hcx : x ∈ closure s
⊢ x ∈ seqClosure s
[PROOFSTEP]
by_cases hx : x ∈ s
[GOAL]
case pos
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h :
  ∀ (f : X → Prop) (a : X), (∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 (f a))) → ContinuousAt f a
s : Set X
x : X
hcx : x ∈ closure s
hx : x ∈ s
⊢ x ∈ seqClosure s
[PROOFSTEP]
exact subset_seqClosure hx
[GOAL]
case neg
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h :
  ∀ (f : X → Prop) (a : X), (∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 (f a))) → ContinuousAt f a
s : Set X
x : X
hcx : x ∈ closure s
hx : ¬x ∈ s
⊢ x ∈ seqClosure s
[PROOFSTEP]
obtain ⟨u, hux, hus⟩ : ∃ u : ℕ → X, Tendsto u atTop (𝓝 x) ∧ ∃ᶠ x in atTop, u x ∈ s
[GOAL]
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h :
  ∀ (f : X → Prop) (a : X), (∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 (f a))) → ContinuousAt f a
s : Set X
x : X
hcx : x ∈ closure s
hx : ¬x ∈ s
⊢ ∃ u, Tendsto u atTop (𝓝 x) ∧ ∃ᶠ (x : ℕ) in atTop, u x ∈ s
[PROOFSTEP]
simpa only [ContinuousAt, hx, tendsto_nhds_true, (· ∘ ·), ← not_frequently, exists_prop, ← mem_closure_iff_frequently,
  hcx, imp_false, not_forall, not_not] using h (· ∉ s) x
[GOAL]
case neg.intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h :
  ∀ (f : X → Prop) (a : X), (∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 (f a))) → ContinuousAt f a
s : Set X
x : X
hcx : x ∈ closure s
hx : ¬x ∈ s
u : ℕ → X
hux : Tendsto u atTop (𝓝 x)
hus : ∃ᶠ (x : ℕ) in atTop, u x ∈ s
⊢ x ∈ seqClosure s
[PROOFSTEP]
rcases extraction_of_frequently_atTop hus with ⟨φ, φ_mono, hφ⟩
[GOAL]
case neg.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h :
  ∀ (f : X → Prop) (a : X), (∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 (f a))) → ContinuousAt f a
s : Set X
x : X
hcx : x ∈ closure s
hx : ¬x ∈ s
u : ℕ → X
hux : Tendsto u atTop (𝓝 x)
hus : ∃ᶠ (x : ℕ) in atTop, u x ∈ s
φ : ℕ → ℕ
φ_mono : StrictMono φ
hφ : ∀ (n : ℕ), u (φ n) ∈ s
⊢ x ∈ seqClosure s
[PROOFSTEP]
exact ⟨u ∘ φ, hφ, hux.comp φ_mono.tendsto_atTop⟩
[GOAL]
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace X
s : Set X
hs : IsSeqClosed s
⊢ IsClosed s
[PROOFSTEP]
rw [← closure_eq_iff_isClosed, ← seqClosure_eq_closure, hs.seqClosure_eq]
[GOAL]
X : Type u_1
Y : Type u_2
inst✝ : UniformSpace X
s : Set X
h : IsSeqCompact s
⊢ TotallyBounded s
[PROOFSTEP]
intro V V_in
[GOAL]
X : Type u_1
Y : Type u_2
inst✝ : UniformSpace X
s : Set X
h : IsSeqCompact s
V : Set (X × X)
V_in : V ∈ 𝓤 X
⊢ ∃ t, Set.Finite t ∧ s ⊆ ⋃ (y : X) (_ : y ∈ t), {x | (x, y) ∈ V}
[PROOFSTEP]
unfold IsSeqCompact at h
[GOAL]
X : Type u_1
Y : Type u_2
inst✝ : UniformSpace X
s : Set X
h : ∀ ⦃x : ℕ → X⦄, (∀ (n : ℕ), x n ∈ s) → ∃ a, a ∈ s ∧ ∃ φ, StrictMono φ ∧ Tendsto (x ∘ φ) atTop (𝓝 a)
V : Set (X × X)
V_in : V ∈ 𝓤 X
⊢ ∃ t, Set.Finite t ∧ s ⊆ ⋃ (y : X) (_ : y ∈ t), {x | (x, y) ∈ V}
[PROOFSTEP]
contrapose! h
[GOAL]
X : Type u_1
Y : Type u_2
inst✝ : UniformSpace X
s : Set X
V : Set (X × X)
V_in : V ∈ 𝓤 X
h : ∀ (t : Set X), Set.Finite t → ¬s ⊆ ⋃ (y : X) (_ : y ∈ t), {x | (x, y) ∈ V}
⊢ Exists fun ⦃x⦄ => (∀ (n : ℕ), x n ∈ s) ∧ ∀ (a : X), a ∈ s → ∀ (φ : ℕ → ℕ), StrictMono φ → ¬Tendsto (x ∘ φ) atTop (𝓝 a)
[PROOFSTEP]
obtain ⟨u, u_in, hu⟩ : ∃ u : ℕ → X, (∀ n, u n ∈ s) ∧ ∀ n m, m < n → u m ∉ ball (u n) V :=
  by
  simp only [not_subset, mem_iUnion₂, not_exists, exists_prop] at h
  simpa only [forall_and, ball_image_iff, not_and] using seq_of_forall_finite_exists h
[GOAL]
X : Type u_1
Y : Type u_2
inst✝ : UniformSpace X
s : Set X
V : Set (X × X)
V_in : V ∈ 𝓤 X
h : ∀ (t : Set X), Set.Finite t → ¬s ⊆ ⋃ (y : X) (_ : y ∈ t), {x | (x, y) ∈ V}
⊢ ∃ u, (∀ (n : ℕ), u n ∈ s) ∧ ∀ (n m : ℕ), m < n → ¬u m ∈ ball (u n) V
[PROOFSTEP]
simp only [not_subset, mem_iUnion₂, not_exists, exists_prop] at h
[GOAL]
X : Type u_1
Y : Type u_2
inst✝ : UniformSpace X
s : Set X
V : Set (X × X)
V_in : V ∈ 𝓤 X
h : ∀ (t : Set X), Set.Finite t → ∃ a, a ∈ s ∧ ∀ (x : X), ¬(x ∈ t ∧ a ∈ {x_1 | (x_1, x) ∈ V})
⊢ ∃ u, (∀ (n : ℕ), u n ∈ s) ∧ ∀ (n m : ℕ), m < n → ¬u m ∈ ball (u n) V
[PROOFSTEP]
simpa only [forall_and, ball_image_iff, not_and] using seq_of_forall_finite_exists h
[GOAL]
case intro.intro
X : Type u_1
Y : Type u_2
inst✝ : UniformSpace X
s : Set X
V : Set (X × X)
V_in : V ∈ 𝓤 X
h : ∀ (t : Set X), Set.Finite t → ¬s ⊆ ⋃ (y : X) (_ : y ∈ t), {x | (x, y) ∈ V}
u : ℕ → X
u_in : ∀ (n : ℕ), u n ∈ s
hu : ∀ (n m : ℕ), m < n → ¬u m ∈ ball (u n) V
⊢ Exists fun ⦃x⦄ => (∀ (n : ℕ), x n ∈ s) ∧ ∀ (a : X), a ∈ s → ∀ (φ : ℕ → ℕ), StrictMono φ → ¬Tendsto (x ∘ φ) atTop (𝓝 a)
[PROOFSTEP]
refine' ⟨u, u_in, fun x _ φ hφ huφ => _⟩
[GOAL]
case intro.intro
X : Type u_1
Y : Type u_2
inst✝ : UniformSpace X
s : Set X
V : Set (X × X)
V_in : V ∈ 𝓤 X
h : ∀ (t : Set X), Set.Finite t → ¬s ⊆ ⋃ (y : X) (_ : y ∈ t), {x | (x, y) ∈ V}
u : ℕ → X
u_in : ∀ (n : ℕ), u n ∈ s
hu : ∀ (n m : ℕ), m < n → ¬u m ∈ ball (u n) V
x : X
x✝ : x ∈ s
φ : ℕ → ℕ
hφ : StrictMono φ
huφ : Tendsto (u ∘ φ) atTop (𝓝 x)
⊢ False
[PROOFSTEP]
obtain ⟨N, hN⟩ : ∃ N, ∀ p q, p ≥ N → q ≥ N → (u (φ p), u (φ q)) ∈ V
[GOAL]
X : Type u_1
Y : Type u_2
inst✝ : UniformSpace X
s : Set X
V : Set (X × X)
V_in : V ∈ 𝓤 X
h : ∀ (t : Set X), Set.Finite t → ¬s ⊆ ⋃ (y : X) (_ : y ∈ t), {x | (x, y) ∈ V}
u : ℕ → X
u_in : ∀ (n : ℕ), u n ∈ s
hu : ∀ (n m : ℕ), m < n → ¬u m ∈ ball (u n) V
x : X
x✝ : x ∈ s
φ : ℕ → ℕ
hφ : StrictMono φ
huφ : Tendsto (u ∘ φ) atTop (𝓝 x)
⊢ ∃ N, ∀ (p q : ℕ), p ≥ N → q ≥ N → (u (φ p), u (φ q)) ∈ V
case intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝ : UniformSpace X
s : Set X
V : Set (X × X)
V_in : V ∈ 𝓤 X
h : ∀ (t : Set X), Set.Finite t → ¬s ⊆ ⋃ (y : X) (_ : y ∈ t), {x | (x, y) ∈ V}
u : ℕ → X
u_in : ∀ (n : ℕ), u n ∈ s
hu : ∀ (n m : ℕ), m < n → ¬u m ∈ ball (u n) V
x : X
x✝ : x ∈ s
φ : ℕ → ℕ
hφ : StrictMono φ
huφ : Tendsto (u ∘ φ) atTop (𝓝 x)
N : ℕ
hN : ∀ (p q : ℕ), p ≥ N → q ≥ N → (u (φ p), u (φ q)) ∈ V
⊢ False
[PROOFSTEP]
exact huφ.cauchySeq.mem_entourage V_in
[GOAL]
case intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝ : UniformSpace X
s : Set X
V : Set (X × X)
V_in : V ∈ 𝓤 X
h : ∀ (t : Set X), Set.Finite t → ¬s ⊆ ⋃ (y : X) (_ : y ∈ t), {x | (x, y) ∈ V}
u : ℕ → X
u_in : ∀ (n : ℕ), u n ∈ s
hu : ∀ (n m : ℕ), m < n → ¬u m ∈ ball (u n) V
x : X
x✝ : x ∈ s
φ : ℕ → ℕ
hφ : StrictMono φ
huφ : Tendsto (u ∘ φ) atTop (𝓝 x)
N : ℕ
hN : ∀ (p q : ℕ), p ≥ N → q ≥ N → (u (φ p), u (φ q)) ∈ V
⊢ False
[PROOFSTEP]
exact hu (φ <| N + 1) (φ N) (hφ <| lt_add_one N) (hN (N + 1) N N.le_succ le_rfl)
[GOAL]
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
s : Set X
inst✝ : IsCountablyGenerated (𝓤 X)
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
⊢ ∃ x, x ∈ s ∧ l ≤ 𝓝 x
[PROOFSTEP]
have := hl.1
[GOAL]
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
s : Set X
inst✝ : IsCountablyGenerated (𝓤 X)
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
this : NeBot l
⊢ ∃ x, x ∈ s ∧ l ≤ 𝓝 x
[PROOFSTEP]
rcases exists_antitone_basis (𝓤 X) with ⟨V, hV⟩
[GOAL]
case intro
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
s : Set X
inst✝ : IsCountablyGenerated (𝓤 X)
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
this : NeBot l
V : ℕ → Set (X × X)
hV : HasAntitoneBasis (𝓤 X) V
⊢ ∃ x, x ∈ s ∧ l ≤ 𝓝 x
[PROOFSTEP]
choose W hW hWV using fun n => comp_mem_uniformity_sets (hV.mem n)
[GOAL]
case intro
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
s : Set X
inst✝ : IsCountablyGenerated (𝓤 X)
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
this : NeBot l
V : ℕ → Set (X × X)
hV : HasAntitoneBasis (𝓤 X) V
W : ℕ → Set (X × X)
hW : ∀ (n : ℕ), W n ∈ 𝓤 X
hWV : ∀ (n : ℕ), W n ○ W n ⊆ V n
⊢ ∃ x, x ∈ s ∧ l ≤ 𝓝 x
[PROOFSTEP]
have hWV' : ∀ n, W n ⊆ V n := fun n ⟨x, y⟩ hx => @hWV n (x, y) ⟨x, refl_mem_uniformity <| hW _, hx⟩
[GOAL]
case intro
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
s : Set X
inst✝ : IsCountablyGenerated (𝓤 X)
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
this : NeBot l
V : ℕ → Set (X × X)
hV : HasAntitoneBasis (𝓤 X) V
W : ℕ → Set (X × X)
hW : ∀ (n : ℕ), W n ∈ 𝓤 X
hWV : ∀ (n : ℕ), W n ○ W n ⊆ V n
hWV' : ∀ (n : ℕ), W n ⊆ V n
⊢ ∃ x, x ∈ s ∧ l ≤ 𝓝 x
[PROOFSTEP]
obtain ⟨t, ht_anti, htl, htW, hts⟩ :
  ∃ t : ℕ → Set X, Antitone t ∧ (∀ n, t n ∈ l) ∧ (∀ n, t n ×ˢ t n ⊆ W n) ∧ ∀ n, t n ⊆ s :=
  by
  have : ∀ n, ∃ t ∈ l, t ×ˢ t ⊆ W n ∧ t ⊆ s :=
    by
    rw [le_principal_iff] at hls
    have : ∀ n, W n ∩ s ×ˢ s ∈ l ×ˢ l := fun n => inter_mem (hl.2 (hW n)) (prod_mem_prod hls hls)
    simpa only [l.basis_sets.prod_self.mem_iff, true_imp_iff, subset_inter_iff, prod_self_subset_prod_self,
      and_assoc] using this
  choose t htl htW hts using this
  have : ∀ n : ℕ, ⋂ k ≤ n, t k ⊆ t n := fun n => by apply iInter₂_subset; rfl
  exact
    ⟨fun n => ⋂ k ≤ n, t k, fun m n h => biInter_subset_biInter_left fun k (hk : k ≤ m) => hk.trans h, fun n =>
      (biInter_mem (finite_le_nat n)).2 fun k _ => htl k, fun n => (prod_mono (this n) (this n)).trans (htW n), fun n =>
      (this n).trans (hts n)⟩
[GOAL]
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
s : Set X
inst✝ : IsCountablyGenerated (𝓤 X)
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
this : NeBot l
V : ℕ → Set (X × X)
hV : HasAntitoneBasis (𝓤 X) V
W : ℕ → Set (X × X)
hW : ∀ (n : ℕ), W n ∈ 𝓤 X
hWV : ∀ (n : ℕ), W n ○ W n ⊆ V n
hWV' : ∀ (n : ℕ), W n ⊆ V n
⊢ ∃ t, Antitone t ∧ (∀ (n : ℕ), t n ∈ l) ∧ (∀ (n : ℕ), t n ×ˢ t n ⊆ W n) ∧ ∀ (n : ℕ), t n ⊆ s
[PROOFSTEP]
have : ∀ n, ∃ t ∈ l, t ×ˢ t ⊆ W n ∧ t ⊆ s := by
  rw [le_principal_iff] at hls
  have : ∀ n, W n ∩ s ×ˢ s ∈ l ×ˢ l := fun n => inter_mem (hl.2 (hW n)) (prod_mem_prod hls hls)
  simpa only [l.basis_sets.prod_self.mem_iff, true_imp_iff, subset_inter_iff, prod_self_subset_prod_self,
    and_assoc] using this
[GOAL]
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
s : Set X
inst✝ : IsCountablyGenerated (𝓤 X)
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
this : NeBot l
V : ℕ → Set (X × X)
hV : HasAntitoneBasis (𝓤 X) V
W : ℕ → Set (X × X)
hW : ∀ (n : ℕ), W n ∈ 𝓤 X
hWV : ∀ (n : ℕ), W n ○ W n ⊆ V n
hWV' : ∀ (n : ℕ), W n ⊆ V n
⊢ ∀ (n : ℕ), ∃ t, t ∈ l ∧ t ×ˢ t ⊆ W n ∧ t ⊆ s
[PROOFSTEP]
rw [le_principal_iff] at hls
[GOAL]
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
s : Set X
inst✝ : IsCountablyGenerated (𝓤 X)
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : s ∈ l
this : NeBot l
V : ℕ → Set (X × X)
hV : HasAntitoneBasis (𝓤 X) V
W : ℕ → Set (X × X)
hW : ∀ (n : ℕ), W n ∈ 𝓤 X
hWV : ∀ (n : ℕ), W n ○ W n ⊆ V n
hWV' : ∀ (n : ℕ), W n ⊆ V n
⊢ ∀ (n : ℕ), ∃ t, t ∈ l ∧ t ×ˢ t ⊆ W n ∧ t ⊆ s
[PROOFSTEP]
have : ∀ n, W n ∩ s ×ˢ s ∈ l ×ˢ l := fun n => inter_mem (hl.2 (hW n)) (prod_mem_prod hls hls)
[GOAL]
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
s : Set X
inst✝ : IsCountablyGenerated (𝓤 X)
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : s ∈ l
this✝ : NeBot l
V : ℕ → Set (X × X)
hV : HasAntitoneBasis (𝓤 X) V
W : ℕ → Set (X × X)
hW : ∀ (n : ℕ), W n ∈ 𝓤 X
hWV : ∀ (n : ℕ), W n ○ W n ⊆ V n
hWV' : ∀ (n : ℕ), W n ⊆ V n
this : ∀ (n : ℕ), W n ∩ s ×ˢ s ∈ l ×ˢ l
⊢ ∀ (n : ℕ), ∃ t, t ∈ l ∧ t ×ˢ t ⊆ W n ∧ t ⊆ s
[PROOFSTEP]
simpa only [l.basis_sets.prod_self.mem_iff, true_imp_iff, subset_inter_iff, prod_self_subset_prod_self, and_assoc] using
  this
[GOAL]
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
s : Set X
inst✝ : IsCountablyGenerated (𝓤 X)
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
this✝ : NeBot l
V : ℕ → Set (X × X)
hV : HasAntitoneBasis (𝓤 X) V
W : ℕ → Set (X × X)
hW : ∀ (n : ℕ), W n ∈ 𝓤 X
hWV : ∀ (n : ℕ), W n ○ W n ⊆ V n
hWV' : ∀ (n : ℕ), W n ⊆ V n
this : ∀ (n : ℕ), ∃ t, t ∈ l ∧ t ×ˢ t ⊆ W n ∧ t ⊆ s
⊢ ∃ t, Antitone t ∧ (∀ (n : ℕ), t n ∈ l) ∧ (∀ (n : ℕ), t n ×ˢ t n ⊆ W n) ∧ ∀ (n : ℕ), t n ⊆ s
[PROOFSTEP]
choose t htl htW hts using this
[GOAL]
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
s : Set X
inst✝ : IsCountablyGenerated (𝓤 X)
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
this : NeBot l
V : ℕ → Set (X × X)
hV : HasAntitoneBasis (𝓤 X) V
W : ℕ → Set (X × X)
hW : ∀ (n : ℕ), W n ∈ 𝓤 X
hWV : ∀ (n : ℕ), W n ○ W n ⊆ V n
hWV' : ∀ (n : ℕ), W n ⊆ V n
t : ℕ → Set X
htl : ∀ (n : ℕ), t n ∈ l
htW : ∀ (n : ℕ), t n ×ˢ t n ⊆ W n
hts : ∀ (n : ℕ), t n ⊆ s
⊢ ∃ t, Antitone t ∧ (∀ (n : ℕ), t n ∈ l) ∧ (∀ (n : ℕ), t n ×ˢ t n ⊆ W n) ∧ ∀ (n : ℕ), t n ⊆ s
[PROOFSTEP]
have : ∀ n : ℕ, ⋂ k ≤ n, t k ⊆ t n := fun n => by apply iInter₂_subset; rfl
[GOAL]
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
s : Set X
inst✝ : IsCountablyGenerated (𝓤 X)
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
this : NeBot l
V : ℕ → Set (X × X)
hV : HasAntitoneBasis (𝓤 X) V
W : ℕ → Set (X × X)
hW : ∀ (n : ℕ), W n ∈ 𝓤 X
hWV : ∀ (n : ℕ), W n ○ W n ⊆ V n
hWV' : ∀ (n : ℕ), W n ⊆ V n
t : ℕ → Set X
htl : ∀ (n : ℕ), t n ∈ l
htW : ∀ (n : ℕ), t n ×ˢ t n ⊆ W n
hts : ∀ (n : ℕ), t n ⊆ s
n : ℕ
⊢ ⋂ (k : ℕ) (_ : k ≤ n), t k ⊆ t n
[PROOFSTEP]
apply iInter₂_subset
[GOAL]
case j
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
s : Set X
inst✝ : IsCountablyGenerated (𝓤 X)
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
this : NeBot l
V : ℕ → Set (X × X)
hV : HasAntitoneBasis (𝓤 X) V
W : ℕ → Set (X × X)
hW : ∀ (n : ℕ), W n ∈ 𝓤 X
hWV : ∀ (n : ℕ), W n ○ W n ⊆ V n
hWV' : ∀ (n : ℕ), W n ⊆ V n
t : ℕ → Set X
htl : ∀ (n : ℕ), t n ∈ l
htW : ∀ (n : ℕ), t n ×ˢ t n ⊆ W n
hts : ∀ (n : ℕ), t n ⊆ s
n : ℕ
⊢ n ≤ n
[PROOFSTEP]
rfl
[GOAL]
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
s : Set X
inst✝ : IsCountablyGenerated (𝓤 X)
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
this✝ : NeBot l
V : ℕ → Set (X × X)
hV : HasAntitoneBasis (𝓤 X) V
W : ℕ → Set (X × X)
hW : ∀ (n : ℕ), W n ∈ 𝓤 X
hWV : ∀ (n : ℕ), W n ○ W n ⊆ V n
hWV' : ∀ (n : ℕ), W n ⊆ V n
t : ℕ → Set X
htl : ∀ (n : ℕ), t n ∈ l
htW : ∀ (n : ℕ), t n ×ˢ t n ⊆ W n
hts : ∀ (n : ℕ), t n ⊆ s
this : ∀ (n : ℕ), ⋂ (k : ℕ) (_ : k ≤ n), t k ⊆ t n
⊢ ∃ t, Antitone t ∧ (∀ (n : ℕ), t n ∈ l) ∧ (∀ (n : ℕ), t n ×ˢ t n ⊆ W n) ∧ ∀ (n : ℕ), t n ⊆ s
[PROOFSTEP]
exact
  ⟨fun n => ⋂ k ≤ n, t k, fun m n h => biInter_subset_biInter_left fun k (hk : k ≤ m) => hk.trans h, fun n =>
    (biInter_mem (finite_le_nat n)).2 fun k _ => htl k, fun n => (prod_mono (this n) (this n)).trans (htW n), fun n =>
    (this n).trans (hts n)⟩
[GOAL]
case intro.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
s : Set X
inst✝ : IsCountablyGenerated (𝓤 X)
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
this : NeBot l
V : ℕ → Set (X × X)
hV : HasAntitoneBasis (𝓤 X) V
W : ℕ → Set (X × X)
hW : ∀ (n : ℕ), W n ∈ 𝓤 X
hWV : ∀ (n : ℕ), W n ○ W n ⊆ V n
hWV' : ∀ (n : ℕ), W n ⊆ V n
t : ℕ → Set X
ht_anti : Antitone t
htl : ∀ (n : ℕ), t n ∈ l
htW : ∀ (n : ℕ), t n ×ˢ t n ⊆ W n
hts : ∀ (n : ℕ), t n ⊆ s
⊢ ∃ x, x ∈ s ∧ l ≤ 𝓝 x
[PROOFSTEP]
choose u hu using fun n => Filter.nonempty_of_mem (htl n)
[GOAL]
case intro.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
s : Set X
inst✝ : IsCountablyGenerated (𝓤 X)
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
this : NeBot l
V : ℕ → Set (X × X)
hV : HasAntitoneBasis (𝓤 X) V
W : ℕ → Set (X × X)
hW : ∀ (n : ℕ), W n ∈ 𝓤 X
hWV : ∀ (n : ℕ), W n ○ W n ⊆ V n
hWV' : ∀ (n : ℕ), W n ⊆ V n
t : ℕ → Set X
ht_anti : Antitone t
htl : ∀ (n : ℕ), t n ∈ l
htW : ∀ (n : ℕ), t n ×ˢ t n ⊆ W n
hts : ∀ (n : ℕ), t n ⊆ s
u : ℕ → X
hu : ∀ (n : ℕ), u n ∈ t n
⊢ ∃ x, x ∈ s ∧ l ≤ 𝓝 x
[PROOFSTEP]
have huc : CauchySeq u :=
  hV.toHasBasis.cauchySeq_iff.2 fun N _ =>
    ⟨N, fun m hm n hn => hWV' _ <| @htW N (_, _) ⟨ht_anti hm (hu _), ht_anti hn (hu _)⟩⟩
[GOAL]
case intro.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
s : Set X
inst✝ : IsCountablyGenerated (𝓤 X)
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
this : NeBot l
V : ℕ → Set (X × X)
hV : HasAntitoneBasis (𝓤 X) V
W : ℕ → Set (X × X)
hW : ∀ (n : ℕ), W n ∈ 𝓤 X
hWV : ∀ (n : ℕ), W n ○ W n ⊆ V n
hWV' : ∀ (n : ℕ), W n ⊆ V n
t : ℕ → Set X
ht_anti : Antitone t
htl : ∀ (n : ℕ), t n ∈ l
htW : ∀ (n : ℕ), t n ×ˢ t n ⊆ W n
hts : ∀ (n : ℕ), t n ⊆ s
u : ℕ → X
hu : ∀ (n : ℕ), u n ∈ t n
huc : CauchySeq u
⊢ ∃ x, x ∈ s ∧ l ≤ 𝓝 x
[PROOFSTEP]
rcases hs.exists_tendsto (fun n => hts n (hu n)) huc with ⟨x, hxs, hx⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
s : Set X
inst✝ : IsCountablyGenerated (𝓤 X)
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
this : NeBot l
V : ℕ → Set (X × X)
hV : HasAntitoneBasis (𝓤 X) V
W : ℕ → Set (X × X)
hW : ∀ (n : ℕ), W n ∈ 𝓤 X
hWV : ∀ (n : ℕ), W n ○ W n ⊆ V n
hWV' : ∀ (n : ℕ), W n ⊆ V n
t : ℕ → Set X
ht_anti : Antitone t
htl : ∀ (n : ℕ), t n ∈ l
htW : ∀ (n : ℕ), t n ×ˢ t n ⊆ W n
hts : ∀ (n : ℕ), t n ⊆ s
u : ℕ → X
hu : ∀ (n : ℕ), u n ∈ t n
huc : CauchySeq u
x : X
hxs : x ∈ s
hx : Tendsto (fun n => u n) atTop (𝓝 x)
⊢ ∃ x, x ∈ s ∧ l ≤ 𝓝 x
[PROOFSTEP]
refine ⟨x, hxs, (nhds_basis_uniformity' hV.toHasBasis).ge_iff.2 fun N _ => ?_⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
s : Set X
inst✝ : IsCountablyGenerated (𝓤 X)
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
this : NeBot l
V : ℕ → Set (X × X)
hV : HasAntitoneBasis (𝓤 X) V
W : ℕ → Set (X × X)
hW : ∀ (n : ℕ), W n ∈ 𝓤 X
hWV : ∀ (n : ℕ), W n ○ W n ⊆ V n
hWV' : ∀ (n : ℕ), W n ⊆ V n
t : ℕ → Set X
ht_anti : Antitone t
htl : ∀ (n : ℕ), t n ∈ l
htW : ∀ (n : ℕ), t n ×ˢ t n ⊆ W n
hts : ∀ (n : ℕ), t n ⊆ s
u : ℕ → X
hu : ∀ (n : ℕ), u n ∈ t n
huc : CauchySeq u
x : X
hxs : x ∈ s
hx : Tendsto (fun n => u n) atTop (𝓝 x)
N : ℕ
x✝ : True
⊢ ball x (V N) ∈ l
[PROOFSTEP]
obtain ⟨n, hNn, hn⟩ : ∃ n, N ≤ n ∧ u n ∈ ball x (W N)
[GOAL]
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
s : Set X
inst✝ : IsCountablyGenerated (𝓤 X)
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
this : NeBot l
V : ℕ → Set (X × X)
hV : HasAntitoneBasis (𝓤 X) V
W : ℕ → Set (X × X)
hW : ∀ (n : ℕ), W n ∈ 𝓤 X
hWV : ∀ (n : ℕ), W n ○ W n ⊆ V n
hWV' : ∀ (n : ℕ), W n ⊆ V n
t : ℕ → Set X
ht_anti : Antitone t
htl : ∀ (n : ℕ), t n ∈ l
htW : ∀ (n : ℕ), t n ×ˢ t n ⊆ W n
hts : ∀ (n : ℕ), t n ⊆ s
u : ℕ → X
hu : ∀ (n : ℕ), u n ∈ t n
huc : CauchySeq u
x : X
hxs : x ∈ s
hx : Tendsto (fun n => u n) atTop (𝓝 x)
N : ℕ
x✝ : True
⊢ ∃ n, N ≤ n ∧ u n ∈ ball x (W N)
[PROOFSTEP]
exact ((eventually_ge_atTop N).and (hx <| ball_mem_nhds x (hW N))).exists
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
s : Set X
inst✝ : IsCountablyGenerated (𝓤 X)
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
this : NeBot l
V : ℕ → Set (X × X)
hV : HasAntitoneBasis (𝓤 X) V
W : ℕ → Set (X × X)
hW : ∀ (n : ℕ), W n ∈ 𝓤 X
hWV : ∀ (n : ℕ), W n ○ W n ⊆ V n
hWV' : ∀ (n : ℕ), W n ⊆ V n
t : ℕ → Set X
ht_anti : Antitone t
htl : ∀ (n : ℕ), t n ∈ l
htW : ∀ (n : ℕ), t n ×ˢ t n ⊆ W n
hts : ∀ (n : ℕ), t n ⊆ s
u : ℕ → X
hu : ∀ (n : ℕ), u n ∈ t n
huc : CauchySeq u
x : X
hxs : x ∈ s
hx : Tendsto (fun n => u n) atTop (𝓝 x)
N : ℕ
x✝ : True
n : ℕ
hNn : N ≤ n
hn : u n ∈ ball x (W N)
⊢ ball x (V N) ∈ l
[PROOFSTEP]
refine mem_of_superset (htl n) fun y hy => hWV N ⟨u n, hn, htW N ?_⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
s : Set X
inst✝ : IsCountablyGenerated (𝓤 X)
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
this : NeBot l
V : ℕ → Set (X × X)
hV : HasAntitoneBasis (𝓤 X) V
W : ℕ → Set (X × X)
hW : ∀ (n : ℕ), W n ∈ 𝓤 X
hWV : ∀ (n : ℕ), W n ○ W n ⊆ V n
hWV' : ∀ (n : ℕ), W n ⊆ V n
t : ℕ → Set X
ht_anti : Antitone t
htl : ∀ (n : ℕ), t n ∈ l
htW : ∀ (n : ℕ), t n ×ˢ t n ⊆ W n
hts : ∀ (n : ℕ), t n ⊆ s
u : ℕ → X
hu : ∀ (n : ℕ), u n ∈ t n
huc : CauchySeq u
x : X
hxs : x ∈ s
hx : Tendsto (fun n => u n) atTop (𝓝 x)
N : ℕ
x✝ : True
n : ℕ
hNn : N ≤ n
hn : u n ∈ ball x (W N)
y : X
hy : y ∈ t n
⊢ (u n, (x, y).snd) ∈ t N ×ˢ t N
[PROOFSTEP]
exact ⟨ht_anti hNn (hu n), ht_anti hNn hy⟩
[GOAL]
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
s : Set X
inst✝ : IsCountablyGenerated (𝓤 X)
⊢ CompactSpace X ↔ SeqCompactSpace X
[PROOFSTEP]
simp only [← isCompact_univ_iff, seqCompactSpace_iff, UniformSpace.isCompact_iff_isSeqCompact]