internlm/Lean-Github huggingface dataset:
Theorem: Matrix.ncard_rowBasis_eq_ncard_colBasis
Proof state before:
case refine_2
l : Type u_1
m✝ : Type u_2
m' : Type u_3
n✝ : Type u_4
n' : Type u_5
n₁ : Type u_6
n₂ : Type u_7
o : Type u_8
α : Type u_9
R✝ : Type u_10
A✝¹ B✝ : Matrix m✝ n✝ R✝
s✝ : Set m✝
t✝ : Set n✝
m : Type u_11
n : Type u_12
R : Type u_13
s : Set m
t : Set n
A✝ B : Matrix m n R
K : Type u_14
inst✝ : Field K
A : Matrix m n K
hs : A.RowBasis s
ht : A.ColBasis t
ht' : (A.rowSubmatrix s).ColBasis t
hinf : s.Infinite
htfin : t.Finite
x✝ : Fintype ↑t
⊢ s.Finite
Tactic:
have hs' := ht.submatrix_rowBasis hs
Proof state after:
case refine_2
l : Type u_1
m✝ : Type u_2
m' : Type u_3
n✝ : Type u_4
n' : Type u_5
n₁ : Type u_6
n₂ : Type u_7
o : Type u_8
α : Type u_9
R✝ : Type u_10
A✝¹ B✝ : Matrix m✝ n✝ R✝
s✝ : Set m✝
t✝ : Set n✝
m : Type u_11
n : Type u_12
R : Type u_13
s : Set m
t : Set n
A✝ B : Matrix m n R
K : Type u_14
inst✝ : Field K
A : Matrix m n K
hs : A.RowBasis s
ht : A.ColBasis t
ht' : (A.rowSubmatrix s).ColBasis t
hinf : s.Infinite
htfin : t.Finite
x✝ : Fintype ↑t
hs' : (A.colSubmatrix t).RowBasis s
⊢ s.Finite
Theorem: Matrix.ncard_rowBasis_eq_ncard_colBasis
Proof state before:
case refine_2
l : Type u_1
m✝ : Type u_2
m' : Type u_3
n✝ : Type u_4
n' : Type u_5
n₁ : Type u_6
n₂ : Type u_7
o : Type u_8
α : Type u_9
R✝ : Type u_10
A✝¹ B✝ : Matrix m✝ n✝ R✝
s✝ : Set m✝
t✝ : Set n✝
m : Type u_11
n : Type u_12
R : Type u_13
s : Set m
t : Set n
A✝ B : Matrix m n R
K : Type u_14
inst✝ : Field K
A : Matrix m n K
hs : A.RowBasis s
ht : A.ColBasis t
ht' : (A.rowSubmatrix s).ColBasis t
hinf : s.Infinite
htfin : t.Finite
x✝ : Fintype ↑t
hs' : (A.colSubmatrix t).RowBasis s
⊢ s.Finite
Tactic:
have hb := hs'.basisFun ht.linearIndependent
Proof state after:
case refine_2
l : Type u_1
m✝ : Type u_2
m' : Type u_3
n✝ : Type u_4
n' : Type u_5
n₁ : Type u_6
n₂ : Type u_7
o : Type u_8
α : Type u_9
R✝ : Type u_10
A✝¹ B✝ : Matrix m✝ n✝ R✝
s✝ : Set m✝
t✝ : Set n✝
m : Type u_11
n : Type u_12
R : Type u_13
s : Set m
t : Set n
A✝ B : Matrix m n R
K : Type u_14
inst✝ : Field K
A : Matrix m n K
hs : A.RowBasis s
ht : A.ColBasis t
ht' : (A.rowSubmatrix s).ColBasis t
hinf : s.Infinite
htfin : t.Finite
x✝ : Fintype ↑t
hs' : (A.colSubmatrix t).RowBasis s
hb : Basis (↑s) K (↑t → K)
⊢ s.Finite
Theorem: Matrix.ncard_rowBasis_eq_ncard_colBasis
Proof state before:
case refine_2
l : Type u_1
m✝ : Type u_2
m' : Type u_3
n✝ : Type u_4
n' : Type u_5
n₁ : Type u_6
n₂ : Type u_7
o : Type u_8
α : Type u_9
R✝ : Type u_10
A✝¹ B✝ : Matrix m✝ n✝ R✝
s✝ : Set m✝
t✝ : Set n✝
m : Type u_11
n : Type u_12
R : Type u_13
s : Set m
t : Set n
A✝ B : Matrix m n R
K : Type u_14
inst✝ : Field K
A : Matrix m n K
hs : A.RowBasis s
ht : A.ColBasis t
ht' : (A.rowSubmatrix s).ColBasis t
hinf : s.Infinite
htfin : t.Finite
x✝ : Fintype ↑t
hs' : (A.colSubmatrix t).RowBasis s
hb : Basis (↑s) K (↑t → K)
⊢ s.Finite
Tactic:
have _ := hb.linearIndependent.fintype_index
Proof state after:
case refine_2
l : Type u_1
m✝ : Type u_2
m' : Type u_3
n✝ : Type u_4
n' : Type u_5
n₁ : Type u_6
n₂ : Type u_7
o : Type u_8
α : Type u_9
R✝ : Type u_10
A✝¹ B✝ : Matrix m✝ n✝ R✝
s✝ : Set m✝
t✝ : Set n✝
m : Type u_11
n : Type u_12
R : Type u_13
s : Set m
t : Set n
A✝ B : Matrix m n R
K : Type u_14
inst✝ : Field K
A : Matrix m n K
hs : A.RowBasis s
ht : A.ColBasis t
ht' : (A.rowSubmatrix s).ColBasis t
hinf : s.Infinite
htfin : t.Finite
x✝¹ : Fintype ↑t
hs' : (A.colSubmatrix t).RowBasis s
hb : Basis (↑s) K (↑t → K)
x✝ : Fintype ↑s
⊢ s.Finite
Theorem: Matrix.ncard_rowBasis_eq_ncard_colBasis
Proof state before:
case refine_2
l : Type u_1
m✝ : Type u_2
m' : Type u_3
n✝ : Type u_4
n' : Type u_5
n₁ : Type u_6
n₂ : Type u_7
o : Type u_8
α : Type u_9
R✝ : Type u_10
A✝¹ B✝ : Matrix m✝ n✝ R✝
s✝ : Set m✝
t✝ : Set n✝
m : Type u_11
n : Type u_12
R : Type u_13
s : Set m
t : Set n
A✝ B : Matrix m n R
K : Type u_14
inst✝ : Field K
A : Matrix m n K
hs : A.RowBasis s
ht : A.ColBasis t
ht' : (A.rowSubmatrix s).ColBasis t
hinf : s.Infinite
htfin : t.Finite
x✝¹ : Fintype ↑t
hs' : (A.colSubmatrix t).RowBasis s
hb : Basis (↑s) K (↑t → K)
x✝ : Fintype ↑s
⊢ s.Finite
Tactic:
exact s.toFinite
Proof state after:
no goals
Theorem: Matrix.ncard_rowBasis_eq_ncard_colBasis
Proof state before:
case refine_1
l : Type u_1
m✝ : Type u_2
m' : Type u_3
n✝ : Type u_4
n' : Type u_5
n₁ : Type u_6
n₂ : Type u_7
o : Type u_8
α : Type u_9
R✝ : Type u_10
A✝¹ B✝ : Matrix m✝ n✝ R✝
s✝ : Set m✝
t✝ : Set n✝
m : Type u_11
n : Type u_12
R : Type u_13
s : Set m
t : Set n
A✝ B : Matrix m n R
K : Type u_14
inst✝ : Field K
A : Matrix m n K
hs : A.RowBasis s
ht : A.ColBasis t
ht' : (A.rowSubmatrix s).ColBasis t
hfin : s.Finite
⊢ s.ncard = t.ncard
Tactic:
have _ := hfin.fintype
Proof state after:
case refine_1
l : Type u_1
m✝ : Type u_2
m' : Type u_3
n✝ : Type u_4
n' : Type u_5
n₁ : Type u_6
n₂ : Type u_7
o : Type u_8
α : Type u_9
R✝ : Type u_10
A✝¹ B✝ : Matrix m✝ n✝ R✝
s✝ : Set m✝
t✝ : Set n✝
m : Type u_11
n : Type u_12
R : Type u_13
s : Set m
t : Set n
A✝ B : Matrix m n R
K : Type u_14
inst✝ : Field K
A : Matrix m n K
hs : A.RowBasis s
ht : A.ColBasis t
ht' : (A.rowSubmatrix s).ColBasis t
hfin : s.Finite
x✝ : Fintype ↑s
⊢ s.ncard = t.ncard
Theorem: Matrix.ncard_rowBasis_eq_ncard_colBasis
Proof state before:
case refine_1
l : Type u_1
m✝ : Type u_2
m' : Type u_3
n✝ : Type u_4
n' : Type u_5
n₁ : Type u_6
n₂ : Type u_7
o : Type u_8
α : Type u_9
R✝ : Type u_10
A✝¹ B✝ : Matrix m✝ n✝ R✝
s✝ : Set m✝
t✝ : Set n✝
m : Type u_11
n : Type u_12
R : Type u_13
s : Set m
t : Set n
A✝ B : Matrix m n R
K : Type u_14
inst✝ : Field K
A : Matrix m n K
hs : A.RowBasis s
ht : A.ColBasis t
ht' : (A.rowSubmatrix s).ColBasis t
hfin : s.Finite
x✝ : Fintype ↑s
⊢ s.ncard = t.ncard
Tactic:
have hb := ht'.basisFun hs.linearIndependent
Proof state after:
case refine_1
l : Type u_1
m✝ : Type u_2
m' : Type u_3
n✝ : Type u_4
n' : Type u_5
n₁ : Type u_6
n₂ : Type u_7
o : Type u_8
α : Type u_9
R✝ : Type u_10
A✝¹ B✝ : Matrix m✝ n✝ R✝
s✝ : Set m✝
t✝ : Set n✝
m : Type u_11
n : Type u_12
R : Type u_13
s : Set m
t : Set n
A✝ B : Matrix m n R
K : Type u_14
inst✝ : Field K
A : Matrix m n K
hs : A.RowBasis s
ht : A.ColBasis t
ht' : (A.rowSubmatrix s).ColBasis t
hfin : s.Finite
x✝ : Fintype ↑s
hb : Basis (↑t) K (↑s → K)
⊢ s.ncard = t.ncard
Theorem: Matrix.ncard_rowBasis_eq_ncard_colBasis
Proof state before:
case refine_1
l : Type u_1
m✝ : Type u_2
m' : Type u_3
n✝ : Type u_4
n' : Type u_5
n₁ : Type u_6
n₂ : Type u_7
o : Type u_8
α : Type u_9
R✝ : Type u_10
A✝¹ B✝ : Matrix m✝ n✝ R✝
s✝ : Set m✝
t✝ : Set n✝
m : Type u_11
n : Type u_12
R : Type u_13
s : Set m
t : Set n
A✝ B : Matrix m n R
K : Type u_14
inst✝ : Field K
A : Matrix m n K
hs : A.RowBasis s
ht : A.ColBasis t
ht' : (A.rowSubmatrix s).ColBasis t
hfin : s.Finite
x✝ : Fintype ↑s
hb : Basis (↑t) K (↑s → K)
⊢ s.ncard = t.ncard
Tactic:
have _ := hb.linearIndependent.fintype_index
Proof state after:
case refine_1
l : Type u_1
m✝ : Type u_2
m' : Type u_3
n✝ : Type u_4
n' : Type u_5
n₁ : Type u_6
n₂ : Type u_7
o : Type u_8
α : Type u_9
R✝ : Type u_10
A✝¹ B✝ : Matrix m✝ n✝ R✝
s✝ : Set m✝
t✝ : Set n✝
m : Type u_11
n : Type u_12
R : Type u_13
s : Set m
t : Set n
A✝ B : Matrix m n R
K : Type u_14
inst✝ : Field K
A : Matrix m n K
hs : A.RowBasis s
ht : A.ColBasis t
ht' : (A.rowSubmatrix s).ColBasis t
hfin : s.Finite
x✝¹ : Fintype ↑s
hb : Basis (↑t) K (↑s → K)
x✝ : Fintype ↑t
⊢ s.ncard = t.ncard
Theorem: Matrix.ncard_rowBasis_eq_ncard_colBasis
Proof state before:
case refine_1
l : Type u_1
m✝ : Type u_2
m' : Type u_3
n✝ : Type u_4
n' : Type u_5
n₁ : Type u_6
n₂ : Type u_7
o : Type u_8
α : Type u_9
R✝ : Type u_10
A✝¹ B✝ : Matrix m✝ n✝ R✝
s✝ : Set m✝
t✝ : Set n✝
m : Type u_11
n : Type u_12
R : Type u_13
s : Set m
t : Set n
A✝ B : Matrix m n R
K : Type u_14
inst✝ : Field K
A : Matrix m n K
hs : A.RowBasis s
ht : A.ColBasis t
ht' : (A.rowSubmatrix s).ColBasis t
hfin : s.Finite
x✝¹ : Fintype ↑s
hb : Basis (↑t) K (↑s → K)
x✝ : Fintype ↑t
⊢ s.ncard = t.ncard
Tactic:
rw [← Nat.card_coe_set_eq, ← Nat.card_coe_set_eq, Nat.card_eq_fintype_card,
  Nat.card_eq_fintype_card, ← finrank_eq_card_basis hb, finrank_fintype_fun_eq_card]
Proof state after:
no goals
Theorem: Matrix.ncard_rowBasis
Proof state before:
l : Type u_1
m✝ : Type u_2
m' : Type u_3
n✝ : Type u_4
n' : Type u_5
n₁ : Type u_6
n₂ : Type u_7
o : Type u_8
α : Type u_9
R✝ : Type u_10
A✝¹ B✝ : Matrix m✝ n✝ R✝
s✝ : Set m✝
t✝ : Set n✝
m : Type u_11
n : Type u_12
R : Type u_13
s : Set m
t : Set n
A✝ B : Matrix m n R
K : Type u_14
inst✝ : Field K
A : Matrix m n K
hs : A.RowBasis s
⊢ s.ncard = A.rank'
Tactic:
obtain ⟨t, ht⟩ := A.exists_colBasis
Proof state after:
case intro
l : Type u_1
m✝ : Type u_2
m' : Type u_3
n✝ : Type u_4
n' : Type u_5
n₁ : Type u_6
n₂ : Type u_7
o : Type u_8
α : Type u_9
R✝ : Type u_10
A✝¹ B✝ : Matrix m✝ n✝ R✝
s✝ : Set m✝
t✝¹ : Set n✝
m : Type u_11
n : Type u_12
R : Type u_13
s : Set m
t✝ : Set n
A✝ B : Matrix m n R
K : Type u_14
inst✝ : Field K
A : Matrix m n K
hs : A.RowBasis s
t : Set n
ht : A.ColBasis t
⊢ s.ncard = A.rank'
Theorem: Matrix.ncard_rowBasis
Proof state before:
case intro
l : Type u_1
m✝ : Type u_2
m' : Type u_3
n✝ : Type u_4
n' : Type u_5
n₁ : Type u_6
n₂ : Type u_7
o : Type u_8
α : Type u_9
R✝ : Type u_10
A✝¹ B✝ : Matrix m✝ n✝ R✝
s✝ : Set m✝
t✝¹ : Set n✝
m : Type u_11
n : Type u_12
R : Type u_13
s : Set m
t✝ : Set n
A✝ B : Matrix m n R
K : Type u_14
inst✝ : Field K
A : Matrix m n K
hs : A.RowBasis s
t : Set n
ht : A.ColBasis t
⊢ s.ncard = A.rank'
Tactic:
rw [ncard_rowBasis_eq_ncard_colBasis hs ht, ncard_colBasis ht]
Proof state after:
no goals
Theorem: Matrix.rank'_transpose
Proof state before:
l : Type u_1
m✝ : Type u_2
m' : Type u_3
n✝ : Type u_4
n' : Type u_5
n₁ : Type u_6
n₂ : Type u_7
o : Type u_8
α : Type u_9
R✝ : Type u_10
A✝² B✝ : Matrix m✝ n✝ R✝
s✝ : Set m✝
t✝ : Set n✝
m : Type u_11
n : Type u_12
R : Type u_13
s : Set m
t : Set n
A✝¹ B : Matrix m n R
K : Type u_14
inst✝ : Field K
A✝ A : Matrix m n K
⊢ Aᵀ.rank' = A.rank'
Tactic:
obtain ⟨s, hs⟩ := A.exists_rowBasis
Proof state after:
case intro
l : Type u_1
m✝ : Type u_2
m' : Type u_3
n✝ : Type u_4
n' : Type u_5
n₁ : Type u_6
n₂ : Type u_7
o : Type u_8
α : Type u_9
R✝ : Type u_10
A✝² B✝ : Matrix m✝ n✝ R✝
s✝¹ : Set m✝
t✝ : Set n✝
m : Type u_11
n : Type u_12
R : Type u_13
s✝ : Set m
t : Set n
A✝¹ B : Matrix m n R
K : Type u_14
inst✝ : Field K
A✝ A : Matrix m n K
s : Set m
hs : A.RowBasis s
⊢ Aᵀ.rank' = A.rank'
Theorem: Matrix.rank'_transpose
Proof state before:
case intro
l : Type u_1
m✝ : Type u_2
m' : Type u_3
n✝ : Type u_4
n' : Type u_5
n₁ : Type u_6
n₂ : Type u_7
o : Type u_8
α : Type u_9
R✝ : Type u_10
A✝² B✝ : Matrix m✝ n✝ R✝
s✝¹ : Set m✝
t✝ : Set n✝
m : Type u_11
n : Type u_12
R : Type u_13
s✝ : Set m
t : Set n
A✝¹ B : Matrix m n R
K : Type u_14
inst✝ : Field K
A✝ A : Matrix m n K
s : Set m
hs : A.RowBasis s
⊢ Aᵀ.rank' = A.rank'
Tactic:
obtain ⟨t, ht⟩ := A.exists_colBasis
Proof state after:
case intro.intro
l : Type u_1
m✝ : Type u_2
m' : Type u_3
n✝ : Type u_4
n' : Type u_5
n₁ : Type u_6
n₂ : Type u_7
o : Type u_8
α : Type u_9
R✝ : Type u_10
A✝² B✝ : Matrix m✝ n✝ R✝
s✝¹ : Set m✝
t✝¹ : Set n✝
m : Type u_11
n : Type u_12
R : Type u_13
s✝ : Set m
t✝ : Set n
A✝¹ B : Matrix m n R
K : Type u_14
inst✝ : Field K
A✝ A : Matrix m n K
s : Set m
hs : A.RowBasis s
t : Set n
ht : A.ColBasis t
⊢ Aᵀ.rank' = A.rank'
Theorem: Matrix.rank'_transpose
Proof state before:
case intro.intro
l : Type u_1
m✝ : Type u_2
m' : Type u_3
n✝ : Type u_4
n' : Type u_5
n₁ : Type u_6
n₂ : Type u_7
o : Type u_8
α : Type u_9
R✝ : Type u_10
A✝² B✝ : Matrix m✝ n✝ R✝
s✝¹ : Set m✝
t✝¹ : Set n✝
m : Type u_11
n : Type u_12
R : Type u_13
s✝ : Set m
t✝ : Set n
A✝¹ B : Matrix m n R
K : Type u_14
inst✝ : Field K
A✝ A : Matrix m n K
s : Set m
hs : A.RowBasis s
t : Set n
ht : A.ColBasis t
⊢ Aᵀ.rank' = A.rank'
Tactic:
rw [← ncard_colBasis ht, ← ncard_rowBasis_eq_ncard_colBasis hs ht,
  ← ncard_colBasis hs.colBasis_transpose]
Proof state after:
no goals
Theorem: Basis.toRowMatrix_rowSpace
Proof state before:
R : Type u_1
m : Type u_2
n : Type u_3
inst✝ : CommRing R
U : Submodule R (n → R)
b : Basis m R ↥U
⊢ b.toRowMatrix.rowSpace = U
Tactic:
convert congr_arg (fun (W : Submodule R U) ↦ W.map (Submodule.subtype U)) b.span_eq
Proof state after:
case h.e'_2
R : Type u_1
m : Type u_2
n : Type u_3
inst✝ : CommRing R
U : Submodule R (n → R)
b : Basis m R ↥U
⊢ b.toRowMatrix.rowSpace = map U.subtype (span R (range ⇑b))

case h.e'_3
R : Type u_1
m : Type u_2
n : Type u_3
inst✝ : CommRing R
U : Submodule R (n → R)
b : Basis m R ↥U
⊢ U = map U.subtype ⊤
Theorem: Basis.toRowMatrix_rowSpace
Proof state before:
case h.e'_3
R : Type u_1
m : Type u_2
n : Type u_3
inst✝ : CommRing R
U : Submodule R (n → R)
b : Basis m R ↥U
⊢ U = map U.subtype ⊤
Tactic:
simp
Proof state after:
no goals
Theorem: Basis.toRowMatrix_rowSpace
Proof state before:
case h.e'_2
R : Type u_1
m : Type u_2
n : Type u_3
inst✝ : CommRing R
U : Submodule R (n → R)
b : Basis m R ↥U
⊢ b.toRowMatrix.rowSpace = map U.subtype (span R (range ⇑b))
Tactic:
rw [Matrix.rowSpace, map_span]
Proof state after:
case h.e'_2
R : Type u_1
m : Type u_2
n : Type u_3
inst✝ : CommRing R
U : Submodule R (n → R)
b : Basis m R ↥U
⊢ span R (range b.toRowMatrix.rowFun) = span R (⇑U.subtype '' range ⇑b)
Theorem: Basis.toRowMatrix_rowSpace
Proof state before:
case h.e'_2
R : Type u_1
m : Type u_2
n : Type u_3
inst✝ : CommRing R
U : Submodule R (n → R)
b : Basis m R ↥U
⊢ span R (range b.toRowMatrix.rowFun) = span R (⇑U.subtype '' range ⇑b)
Tactic:
convert rfl
Proof state after:
case h.e'_3.h.e'_6
R : Type u_1
m : Type u_2
n : Type u_3
inst✝ : CommRing R
U : Submodule R (n → R)
b : Basis m R ↥U
⊢ ⇑U.subtype '' range ⇑b = range b.toRowMatrix.rowFun
Theorem: Basis.toRowMatrix_rowSpace
Proof state before:
case h.e'_3.h.e'_6
R : Type u_1
m : Type u_2
n : Type u_3
inst✝ : CommRing R
U : Submodule R (n → R)
b : Basis m R ↥U
⊢ ⇑U.subtype '' range ⇑b = range b.toRowMatrix.rowFun
Tactic:
ext x
Proof state after:
case h.e'_3.h.e'_6.h
R : Type u_1
m : Type u_2
n : Type u_3
inst✝ : CommRing R
U : Submodule R (n → R)
b : Basis m R ↥U
x : n → R
⊢ x ∈ ⇑U.subtype '' range ⇑b ↔ x ∈ range b.toRowMatrix.rowFun
Theorem: Basis.toRowMatrix_rowSpace
Proof state before:
case h.e'_3.h.e'_6.h
R : Type u_1
m : Type u_2
n : Type u_3
inst✝ : CommRing R
U : Submodule R (n → R)
b : Basis m R ↥U
x : n → R
⊢ x ∈ ⇑U.subtype '' range ⇑b ↔ x ∈ range b.toRowMatrix.rowFun
Tactic:
simp only [coeSubtype, mem_image, mem_range, exists_exists_eq_and, toRowMatrix]
Proof state after:
case h.e'_3.h.e'_6.h
R : Type u_1
m : Type u_2
n : Type u_3
inst✝ : CommRing R
U : Submodule R (n → R)
b : Basis m R ↥U
x : n → R
⊢ (∃ a, ↑(b a) = x) ↔ ∃ y, (Matrix.of fun i j => ↑(b i) j).rowFun y = x
Theorem: Basis.toRowMatrix_rowSpace
Proof state before:
case h.e'_3.h.e'_6.h
R : Type u_1
m : Type u_2
n : Type u_3
inst✝ : CommRing R
U : Submodule R (n → R)
b : Basis m R ↥U
x : n → R
⊢ (∃ a, ↑(b a) = x) ↔ ∃ y, (Matrix.of fun i j => ↑(b i) j).rowFun y = x
Tactic:
rfl
Proof state after:
no goals
Theorem: Matroid.Iso.image_subset_target
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
α₃ : Type u_6
M : Matroid α
N : Matroid β
B I D X✝ Y : Set α
e : M.Iso N
X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
⊢ ↑e.toPartialEquiv '' X ⊆ e.toPartialEquiv.target
Tactic:
rw [← image_source_eq_target]
Proof state after:
α : Type u_1
β : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
α₃ : Type u_6
M : Matroid α
N : Matroid β
B I D X✝ Y : Set α
e : M.Iso N
X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
⊢ ↑e.toPartialEquiv '' X ⊆ ↑e.toPartialEquiv '' e.toPartialEquiv.source
Theorem: Matroid.Iso.image_subset_target
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
α₃ : Type u_6
M : Matroid α
N : Matroid β
B I D X✝ Y : Set α
e : M.Iso N
X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
⊢ ↑e.toPartialEquiv '' X ⊆ ↑e.toPartialEquiv '' e.toPartialEquiv.source
Tactic:
exact image_subset _ (e.subset_source X)
Proof state after:
no goals
Theorem: Matroid.Iso.image_ground
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
α₃ : Type u_6
M : Matroid α
N : Matroid β
B I D X Y : Set α
e : M.Iso N
⊢ ↑e.toPartialEquiv '' M.E = N.E
Tactic:
rw [← e.source_eq, ← e.target_eq, image_source_eq_target]
Proof state after:
no goals
Theorem: Matroid.Iso.ground_subset_preimage_ground
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
α₃ : Type u_6
M : Matroid α
N : Matroid β
B I D X Y : Set α
e : M.Iso N
⊢ M.E ⊆ ↑e.toPartialEquiv ⁻¹' N.E
Tactic:
rw [← e.source_eq, ← e.target_eq]
Proof state after:
α : Type u_1
β : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
α₃ : Type u_6
M : Matroid α
N : Matroid β
B I D X Y : Set α
e : M.Iso N
⊢ e.toPartialEquiv.source ⊆ ↑e.toPartialEquiv ⁻¹' e.toPartialEquiv.target
Theorem: Matroid.Iso.ground_subset_preimage_ground
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
α₃ : Type u_6
M : Matroid α
N : Matroid β
B I D X Y : Set α
e : M.Iso N
⊢ e.toPartialEquiv.source ⊆ ↑e.toPartialEquiv ⁻¹' e.toPartialEquiv.target
Tactic:
exact source_subset_preimage_target e.toPartialEquiv
Proof state after:
no goals
Theorem: Matroid.Iso.image_subset_ground
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
α₃ : Type u_6
M : Matroid α
N : Matroid β
B I D X✝ Y : Set α
e : M.Iso N
X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
⊢ ↑e.toPartialEquiv '' X ⊆ N.E
Tactic:
convert image_subset _ hX
Proof state after:
case h.e'_4
α : Type u_1
β : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
α₃ : Type u_6
M : Matroid α
N : Matroid β
B I D X✝ Y : Set α
e : M.Iso N
X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
⊢ N.E = ↑e.toPartialEquiv '' M.E
Theorem: Matroid.Iso.image_subset_ground
Proof state before:
case h.e'_4
α : Type u_1
β : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
α₃ : Type u_6
M : Matroid α
N : Matroid β
B I D X✝ Y : Set α
e : M.Iso N
X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
⊢ N.E = ↑e.toPartialEquiv '' M.E
Tactic:
rw [← e.source_eq, image_source_eq_target, e.target_eq]
Proof state after:
no goals
Theorem: Matroid.Iso.injOn_ground
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
α₃ : Type u_6
M : Matroid α
N : Matroid β
B I D X Y : Set α
e : M.Iso N
⊢ InjOn (↑e.toPartialEquiv) M.E
Tactic:
rw [← e.source_eq]
Proof state after:
α : Type u_1
β : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
α₃ : Type u_6
M : Matroid α
N : Matroid β
B I D X Y : Set α
e : M.Iso N
⊢ InjOn (↑e.toPartialEquiv) e.toPartialEquiv.source
Theorem: Matroid.Iso.injOn_ground
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
α₃ : Type u_6
M : Matroid α
N : Matroid β
B I D X Y : Set α
e : M.Iso N
⊢ InjOn (↑e.toPartialEquiv) e.toPartialEquiv.source
Tactic:
exact e.toPartialEquiv.injOn
Proof state after:
no goals
Theorem: Matroid.Iso.on_base_iff
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
α₃ : Type u_6
M : Matroid α
N : Matroid β
B I D X Y : Set α
e : M.Iso N
hB : autoParam (B ⊆ M.E) _auto✝
⊢ M.Base B ↔ N.Base (↑e.toPartialEquiv '' B)
Tactic:
change (_ ↔ _ ∈ setOf N.Base)
Proof state after:
α : Type u_1
β : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
α₃ : Type u_6
M : Matroid α
N : Matroid β
B I D X Y : Set α
e : M.Iso N
hB : autoParam (B ⊆ M.E) _auto✝
⊢ M.Base B ↔ ↑e.toPartialEquiv '' B ∈ setOf N.Base
Theorem: Matroid.Iso.on_base_iff
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
α₃ : Type u_6
M : Matroid α
N : Matroid β
B I D X Y : Set α
e : M.Iso N
hB : autoParam (B ⊆ M.E) _auto✝
⊢ M.Base B ↔ ↑e.toPartialEquiv '' B ∈ setOf N.Base
Tactic:
simp_rw [e.setOf_base_eq', mem_image, mem_setOf_eq]
Proof state after:
α : Type u_1
β : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
α₃ : Type u_6
M : Matroid α
N : Matroid β
B I D X Y : Set α
e : M.Iso N
hB : autoParam (B ⊆ M.E) _auto✝
⊢ M.Base B ↔ ∃ x, M.Base x ∧ ↑e.toPartialEquiv '' x = ↑e.toPartialEquiv '' B
Theorem: Matroid.Iso.on_base_iff
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
α₃ : Type u_6
M : Matroid α
N : Matroid β
B I D X Y : Set α
e : M.Iso N
hB : autoParam (B ⊆ M.E) _auto✝
⊢ M.Base B ↔ ∃ x, M.Base x ∧ ↑e.toPartialEquiv '' x = ↑e.toPartialEquiv '' B
Tactic:
refine' ⟨fun h ↦ ⟨B, h, rfl⟩, fun ⟨B', h, h'⟩ ↦ _⟩
Proof state after:
α : Type u_1
β : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
α₃ : Type u_6
M : Matroid α
N : Matroid β
B I D X Y : Set α
e : M.Iso N
hB : autoParam (B ⊆ M.E) _auto✝
x✝ : ∃ x, M.Base x ∧ ↑e.toPartialEquiv '' x = ↑e.toPartialEquiv '' B
B' : Set α
h : M.Base B'
h' : ↑e.toPartialEquiv '' B' = ↑e.toPartialEquiv '' B
⊢ M.Base B
Theorem: Matroid.Iso.symm_symm
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
α₃ : Type u_6
M : Matroid α
N : Matroid β
B I D X Y : Set α
e : M.Iso N
⊢ e.symm.symm = e
Tactic:
cases e
Proof state after:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
α₃ : Type u_6
M : Matroid α
N : Matroid β
B I D X Y : Set α
toPartialEquiv✝ : PartialEquiv α β
source_eq'✝ : toPartialEquiv✝.source = M.E
target_eq'✝ : toPartialEquiv✝.target = N.E
setOf_base_eq'✝ : setOf N.Base = image ↑toPartialEquiv✝ '' setOf M.Base
⊢ { toPartialEquiv := toPartialEquiv✝, source_eq' := source_eq'✝, target_eq' := target_eq'✝,
          setOf_base_eq' := setOf_base_eq'✝ }.symm.symm =
    { toPartialEquiv := toPartialEquiv✝, source_eq' := source_eq'✝, target_eq' := target_eq'✝,
      setOf_base_eq' := setOf_base_eq'✝ }
Theorem: Matroid.Iso.symm_symm
Proof state before:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
α₃ : Type u_6
M : Matroid α
N : Matroid β
B I D X Y : Set α
toPartialEquiv✝ : PartialEquiv α β
source_eq'✝ : toPartialEquiv✝.source = M.E
target_eq'✝ : toPartialEquiv✝.target = N.E
setOf_base_eq'✝ : setOf N.Base = image ↑toPartialEquiv✝ '' setOf M.Base
⊢ { toPartialEquiv := toPartialEquiv✝, source_eq' := source_eq'✝, target_eq' := target_eq'✝,
          setOf_base_eq' := setOf_base_eq'✝ }.symm.symm =
    { toPartialEquiv := toPartialEquiv✝, source_eq' := source_eq'✝, target_eq' := target_eq'✝,
      setOf_base_eq' := setOf_base_eq'✝ }
Tactic:
rfl
Proof state after:
no goals
Theorem: Matroid.Iso.apply_symm_apply_mem
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
α₃ : Type u_6
M : Matroid α
N : Matroid β
B I D X Y : Set α
e : M.Iso N
x : α
hx : x ∈ M.E
⊢ x ∈ e.toPartialEquiv.source
Tactic:
rwa [e.source_eq]
Proof state after:
no goals
Theorem: Matroid.Iso.setOf_prop_eq
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
α₃ : Type u_6
M : Matroid α
N : Matroid β
B I D X Y : Set α
PM : Set α → Prop
PN : Set β → Prop
e : M.Iso N
hN : ∀ {Y : Set β}, PN Y → Y ⊆ N.E
hMN : ∀ {X : Set α}, PM X → PN (↑e.toPartialEquiv '' X)
hNM : ∀ {Y : Set β}, PN Y → PM (↑e.symm.toPartialEquiv '' Y)
⊢ setOf PN = image ↑e.toPartialEquiv '' setOf PM
Tactic:
refine' Set.ext (fun Y ↦ ⟨fun h ↦ _, _⟩)
Proof state after:
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
α₃ : Type u_6
M : Matroid α
N : Matroid β
B I D X Y✝ : Set α
PM : Set α → Prop
PN : Set β → Prop
e : M.Iso N
hN : ∀ {Y : Set β}, PN Y → Y ⊆ N.E
hMN : ∀ {X : Set α}, PM X → PN (↑e.toPartialEquiv '' X)
hNM : ∀ {Y : Set β}, PN Y → PM (↑e.symm.toPartialEquiv '' Y)
Y : Set β
h : Y ∈ setOf PN
⊢ Y ∈ image ↑e.toPartialEquiv '' setOf PM

case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
α₃ : Type u_6
M : Matroid α
N : Matroid β
B I D X Y✝ : Set α
PM : Set α → Prop
PN : Set β → Prop
e : M.Iso N
hN : ∀ {Y : Set β}, PN Y → Y ⊆ N.E
hMN : ∀ {X : Set α}, PM X → PN (↑e.toPartialEquiv '' X)
hNM : ∀ {Y : Set β}, PN Y → PM (↑e.symm.toPartialEquiv '' Y)
Y : Set β
⊢ Y ∈ image ↑e.toPartialEquiv '' setOf PM → Y ∈ setOf PN