internlm/Lean-Github huggingface dataset:
Theorem: Matroid.Iso.setOf_prop_eq
Proof state before:
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
Tactic:
intro h
Proof state after:
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 β
h : Y ∈ image ↑e.toPartialEquiv '' setOf PM
⊢ Y ∈ setOf PN
Theorem: Matroid.Iso.setOf_prop_eq
Proof state before:
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 β
h : Y ∈ image ↑e.toPartialEquiv '' setOf PM
⊢ Y ∈ setOf PN
Tactic:
obtain ⟨X, hX, rfl⟩ := h
Proof state after:
case refine'_2.intro.intro
α : 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)
X : Set α
hX : X ∈ setOf PM
⊢ ↑e.toPartialEquiv '' X ∈ setOf PN
Theorem: Matroid.Iso.setOf_prop_eq
Proof state before:
case refine'_2.intro.intro
α : 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)
X : Set α
hX : X ∈ setOf PM
⊢ ↑e.toPartialEquiv '' X ∈ setOf PN
Tactic:
exact hMN hX
Proof state after:
no goals
Theorem: Matroid.Iso.setOf_prop_eq
Proof state before:
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
Tactic:
refine' ⟨e.symm '' Y, hNM 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
⊢ ↑e.toPartialEquiv '' (↑e.symm.toPartialEquiv '' Y) = Y
Theorem: Matroid.Iso.setOf_prop_eq
Proof state before:
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
⊢ ↑e.toPartialEquiv '' (↑e.symm.toPartialEquiv '' Y) = Y
Tactic:
rw [symm_apply, image_symm_image_of_subset_target _ ((hN h).trans_eq e.target_eq.symm)]
Proof state after:
no goals
Theorem: Matroid.Iso.on_prop_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 α
PM : Set α → Prop
PN : Set β → Prop
e : M.Iso N
on_prop : ∀ {Y : Set β}, PN Y → PM (↑e.symm.toPartialEquiv '' Y)
h : PN (↑e.toPartialEquiv '' X)
hX : autoParam (X ⊆ M.E) _auto✝
⊢ PM X
Tactic:
convert on_prop h
Proof state after:
case h.e'_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
on_prop : ∀ {Y : Set β}, PN Y → PM (↑e.symm.toPartialEquiv '' Y)
h : PN (↑e.toPartialEquiv '' X)
hX : autoParam (X ⊆ M.E) _auto✝
⊢ X = ↑e.symm.toPartialEquiv '' (↑e.toPartialEquiv '' X)
Theorem: Matroid.Iso.on_prop_symm
Proof state before:
case h.e'_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
on_prop : ∀ {Y : Set β}, PN Y → PM (↑e.symm.toPartialEquiv '' Y)
h : PN (↑e.toPartialEquiv '' X)
hX : autoParam (X ⊆ M.E) _auto✝
⊢ X = ↑e.symm.toPartialEquiv '' (↑e.toPartialEquiv '' X)
Tactic:
rw [symm_apply, symm_image_image_of_subset_source _ (e.subset_source X)]
Proof state after:
no goals
Theorem: Matroid.Iso.on_base
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 : M.Base B
⊢ N.Base (↑e.toPartialEquiv '' B)
Tactic:
rwa [← e.on_base_iff]
Proof state after:
no goals
Theorem: Matroid.Iso.on_indep
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
hI : M.Indep I
⊢ N.Indep (↑e.toPartialEquiv '' I)
Tactic:
change (_ ∈ (setOf N.Indep))
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
hI : M.Indep I
⊢ ↑e.toPartialEquiv '' I ∈ setOf N.Indep
Theorem: Matroid.Iso.on_indep
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
hI : M.Indep I
⊢ ↑e.toPartialEquiv '' I ∈ setOf N.Indep
Tactic:
rw [setOf_indep_eq, e.setOf_base_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
hI : M.Indep I
⊢ ↑e.toPartialEquiv '' I ∈ ↑(lowerClosure (image ↑e.toPartialEquiv '' setOf M.Base))
Theorem: Matroid.Iso.on_indep
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
hI : M.Indep I
⊢ ↑e.toPartialEquiv '' I ∈ ↑(lowerClosure (image ↑e.toPartialEquiv '' setOf M.Base))
Tactic:
simp only [SetLike.mem_coe, mem_lowerClosure, mem_image, mem_setOf_eq, le_eq_subset,
  image_subset_iff, exists_exists_and_eq_and]
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
hI : M.Indep I
⊢ ∃ a, M.Base a ∧ I ⊆ ↑e.toPartialEquiv ⁻¹' (↑e.toPartialEquiv '' a)
Theorem: Matroid.Iso.on_indep
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
hI : M.Indep I
⊢ ∃ a, M.Base a ∧ I ⊆ ↑e.toPartialEquiv ⁻¹' (↑e.toPartialEquiv '' a)
Tactic:
obtain ⟨B, hB, hIB⟩ := hI.exists_base_superset
Proof state after:
case intro.intro
α : 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
hI : M.Indep I
B : Set α
hB : M.Base B
hIB : I ⊆ B
⊢ ∃ a, M.Base a ∧ I ⊆ ↑e.toPartialEquiv ⁻¹' (↑e.toPartialEquiv '' a)
Theorem: Matroid.Iso.on_indep
Proof state before:
case intro.intro
α : 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
hI : M.Indep I
B : Set α
hB : M.Base B
hIB : I ⊆ B
⊢ ∃ a, M.Base a ∧ I ⊆ ↑e.toPartialEquiv ⁻¹' (↑e.toPartialEquiv '' a)
Tactic:
exact ⟨B, hB, hIB.trans (subset_preimage_image _ _)⟩
Proof state after:
no goals
Theorem: Matroid.Iso.on_indep_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
hI : autoParam (I ⊆ M.E) _auto✝
⊢ M.Indep I ↔ N.Indep (↑e.toPartialEquiv '' I)
Tactic:
refine ⟨e.on_indep, fun h ↦ e.on_indep_symm h hI⟩
Proof state after:
no goals
Theorem: Matroid.Iso.on_dep
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
h : M.Dep D
⊢ N.Dep (↑e.toPartialEquiv '' D)
Tactic:
rw [Dep, and_iff_left (e.image_subset_ground D)]
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
h : M.Dep D
⊢ ¬N.Indep (↑e.toPartialEquiv '' D)
Theorem: Matroid.Iso.on_dep
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
h : M.Dep D
⊢ ¬N.Indep (↑e.toPartialEquiv '' D)
Tactic:
exact fun hI ↦ h.not_indep (e.on_indep_symm hI)
Proof state after:
no goals
Theorem: Matroid.Iso.encard_ground_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 α
e : M.Iso N
⊢ M.E.encard = N.E.encard
Tactic:
rw [← e.image_ground, e.injOn_ground.encard_image]
Proof state after:
no goals
Theorem: Matroid.Iso.restrict_apply
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
R : Set α
hR : autoParam (R ⊆ M.E) _auto✝
⊢ (e.restrict R hR).toPartialEquiv = e.toPartialEquiv.restr R
Tactic:
simp [restrict]
Proof state after:
no goals
Theorem: Matroid.Iso.on_basis
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
hI : M.Basis I X
⊢ N.Basis (↑e.toPartialEquiv '' I) (↑e.toPartialEquiv '' X)
Tactic:
rw [← base_restrict_iff _, (e.restrict X).symm.on_base_iff _, base_restrict_iff]
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
hI : M.Basis I X
⊢ M.Basis (↑(e.restrict X ⋯).symm.toPartialEquiv '' (↑e.toPartialEquiv '' I)) X

α : 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
hI : M.Basis I X
⊢ ↑e.toPartialEquiv '' I ⊆ (N ↾ ↑e.toPartialEquiv '' X).E

α : 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
hI : M.Basis I X
⊢ ↑e.toPartialEquiv '' X ⊆ N.E
Theorem: Matroid.Iso.on_basis
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
hI : M.Basis I X
⊢ ↑e.toPartialEquiv '' X ⊆ N.E
Tactic:
exact e.image_subset_ground X hI.subset_ground
Proof state after:
no goals
Theorem: Matroid.Iso.on_basis
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
hI : M.Basis I X
⊢ M.Basis (↑(e.restrict X ⋯).symm.toPartialEquiv '' (↑e.toPartialEquiv '' I)) X
Tactic:
convert hI
Proof state after:
case h.e'_3
α : 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
hI : M.Basis I X
⊢ ↑(e.restrict X ⋯).symm.toPartialEquiv '' (↑e.toPartialEquiv '' I) = I
Theorem: Matroid.Iso.on_basis
Proof state before:
case h.e'_3
α : 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
hI : M.Basis I X
⊢ ↑(e.restrict X ⋯).symm.toPartialEquiv '' (↑e.toPartialEquiv '' I) = I
Tactic:
simp only [symm_apply, restrict_apply, restr_coe_symm]
Proof state after:
case h.e'_3
α : 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
hI : M.Basis I X
⊢ (fun a => ↑e.toPartialEquiv.symm a) '' (↑e.toPartialEquiv '' I) = I
Theorem: Matroid.Iso.on_basis
Proof state before:
case h.e'_3
α : 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
hI : M.Basis I X
⊢ (fun a => ↑e.toPartialEquiv.symm a) '' (↑e.toPartialEquiv '' I) = I
Tactic:
apply e.toPartialEquiv.symm_image_image_of_subset_source
Proof state after:
case h.e'_3
α : 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
hI : M.Basis I X
⊢ I ⊆ e.toPartialEquiv.source
Theorem: Matroid.Iso.on_basis
Proof state before:
case h.e'_3
α : 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
hI : M.Basis I X
⊢ I ⊆ e.toPartialEquiv.source
Tactic:
rw [e.source_eq]
Proof state after:
case h.e'_3
α : 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
hI : M.Basis I X
⊢ I ⊆ M.E
Theorem: Matroid.Iso.on_basis
Proof state before:
case h.e'_3
α : 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
hI : M.Basis I X
⊢ I ⊆ M.E
Tactic:
exact hI.indep.subset_ground
Proof state after:
no goals
Theorem: Matroid.Iso.on_basis
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
hI : M.Basis I X
⊢ ↑e.toPartialEquiv '' I ⊆ (N ↾ ↑e.toPartialEquiv '' X).E
Tactic:
simp only [restrict_ground_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
hI : M.Basis I X
⊢ ↑e.toPartialEquiv '' I ⊆ ↑e.toPartialEquiv '' X
Theorem: Matroid.Iso.on_basis
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
hI : M.Basis I X
⊢ ↑e.toPartialEquiv '' I ⊆ ↑e.toPartialEquiv '' X
Tactic:
exact image_subset _ hI.subset
Proof state after:
no goals
Theorem: Matroid.isIso_emptyOn_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 α
M✝ : Matroid α
N : Matroid β✝
M : Matroid α
β : Type u_7
⊢ M ≂ emptyOn β ↔ M = emptyOn α
Tactic:
constructor
Proof state after:
case mp
α : 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 α
M✝ : Matroid α
N : Matroid β✝
M : Matroid α
β : Type u_7
⊢ M ≂ emptyOn β → M = emptyOn α

case mpr
α : 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 α
M✝ : Matroid α
N : Matroid β✝
M : Matroid α
β : Type u_7
⊢ M = emptyOn α → M ≂ emptyOn β
Theorem: Matroid.isIso_emptyOn_iff
Proof state before:
case mpr
α : 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 α
M✝ : Matroid α
N : Matroid β✝
M : Matroid α
β : Type u_7
⊢ M = emptyOn α → M ≂ emptyOn β
Tactic:
rintro rfl
Proof state after:
case mpr
α : 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 α
M : Matroid α
N : Matroid β✝
β : Type u_7
⊢ emptyOn α ≂ emptyOn β
Theorem: Matroid.isIso_emptyOn_iff
Proof state before:
case mpr
α : 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 α
M : Matroid α
N : Matroid β✝
β : Type u_7
⊢ emptyOn α ≂ emptyOn β
Tactic:
exact Or.inl ⟨rfl, rfl⟩
Proof state after:
no goals
Theorem: Matroid.isIso_emptyOn_iff
Proof state before:
case mp
α : 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 α
M✝ : Matroid α
N : Matroid β✝
M : Matroid α
β : Type u_7
⊢ M ≂ emptyOn β → M = emptyOn α
Tactic:
rintro (⟨rfl,-⟩ | ⟨⟨i⟩⟩ )
Proof state after:
case mp.inl.intro
α : 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 α
M : Matroid α
N : Matroid β✝
β : Type u_7
⊢ emptyOn α = emptyOn α

case mp.inr.intro
α : 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 α
M✝ : Matroid α
N : Matroid β✝
M : Matroid α
β : Type u_7
i : M.Iso (emptyOn β)
⊢ M = emptyOn α
Theorem: Matroid.isIso_emptyOn_iff
Proof state before:
case mp.inl.intro
α : 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 α
M : Matroid α
N : Matroid β✝
β : Type u_7
⊢ emptyOn α = emptyOn α

case mp.inr.intro
α : 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 α
M✝ : Matroid α
N : Matroid β✝
M : Matroid α
β : Type u_7
i : M.Iso (emptyOn β)
⊢ M = emptyOn α
Tactic:
rfl
Proof state after:
case mp.inr.intro
α : 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 α
M✝ : Matroid α
N : Matroid β✝
M : Matroid α
β : Type u_7
i : M.Iso (emptyOn β)
⊢ M = emptyOn α
Theorem: Matroid.isIso_emptyOn_iff
Proof state before:
case mp.inr.intro
α : 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 α
M✝ : Matroid α
N : Matroid β✝
M : Matroid α
β : Type u_7
i : M.Iso (emptyOn β)
⊢ M = emptyOn α
Tactic:
rw [← ground_eq_empty_iff, ← i.symm.image_ground]
Proof state after:
case mp.inr.intro
α : 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 α
M✝ : Matroid α
N : Matroid β✝
M : Matroid α
β : Type u_7
i : M.Iso (emptyOn β)
⊢ ↑i.symm.toPartialEquiv '' (emptyOn β).E = ∅
Theorem: Matroid.isIso_emptyOn_iff
Proof state before:
case mp.inr.intro
α : 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 α
M✝ : Matroid α
N : Matroid β✝
M : Matroid α
β : Type u_7
i : M.Iso (emptyOn β)
⊢ ↑i.symm.toPartialEquiv '' (emptyOn β).E = ∅
Tactic:
simp
Proof state after:
no goals
Theorem: Matroid.IsIso.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 α
M✝ : Matroid α
N✝ : Matroid β
M : Matroid α
N : Matroid β
h : M ≂ N
⊢ N ≂ M
Tactic:
obtain (⟨hM,hN⟩ | ⟨⟨e⟩⟩)  := h
Proof state after:
case inl.intro
α : 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 α
M✝ : Matroid α
N✝ : Matroid β
M : Matroid α
N : Matroid β
hM : M = emptyOn α
hN : N = emptyOn β
⊢ N ≂ M

case inr.intro
α : 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 α
M✝ : Matroid α
N✝ : Matroid β
M : Matroid α
N : Matroid β
e : M.Iso N
⊢ N ≂ M
Theorem: Matroid.IsIso.symm
Proof state before:
case inr.intro
α : 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 α
M✝ : Matroid α
N✝ : Matroid β
M : Matroid α
N : Matroid β
e : M.Iso N
⊢ N ≂ M
Tactic:
exact Or.inr ⟨e.symm⟩
Proof state after:
no goals
Theorem: Matroid.IsIso.symm
Proof state before:
case inl.intro
α : 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 α
M✝ : Matroid α
N✝ : Matroid β
M : Matroid α
N : Matroid β
hM : M = emptyOn α
hN : N = emptyOn β
⊢ N ≂ M
Tactic:
exact Or.inl ⟨hN, hM⟩
Proof state after:
no goals
Theorem: Matroid.IsIso.trans
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 α
M : Matroid α
N : Matroid β
O : Matroid γ
h1 : M ≂ N
h2 : N ≂ O
⊢ M ≂ O
Tactic:
obtain (⟨rfl,rfl⟩ | ⟨⟨i1⟩⟩) := h1
Proof state after:
case inl.intro
α : 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 α
O : Matroid γ
h2 : emptyOn β ≂ O
⊢ emptyOn α ≂ O

case inr.intro
α : 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 α
M : Matroid α
N : Matroid β
O : Matroid γ
h2 : N ≂ O
i1 : M.Iso N
⊢ M ≂ O
Theorem: Matroid.IsIso.trans
Proof state before:
case inr.intro
α : 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 α
M : Matroid α
N : Matroid β
O : Matroid γ
h2 : N ≂ O
i1 : M.Iso N
⊢ M ≂ O
Tactic:
obtain (⟨rfl,rfl⟩ | ⟨⟨i2⟩⟩) := h2
Proof state after:
case inr.intro.inl.intro
α : 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 α
M : Matroid α
i1 : M.Iso (emptyOn β)
⊢ M ≂ emptyOn γ

case inr.intro.inr.intro
α : 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 α
M : Matroid α
N : Matroid β
O : Matroid γ
i1 : M.Iso N
i2 : N.Iso O
⊢ M ≂ O
Theorem: Matroid.IsIso.trans
Proof state before:
case inr.intro.inr.intro
α : 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 α
M : Matroid α
N : Matroid β
O : Matroid γ
i1 : M.Iso N
i2 : N.Iso O
⊢ M ≂ O
Tactic:
exact Or.inr ⟨i1.trans i2⟩
Proof state after:
no goals
Theorem: Matroid.IsIso.trans
Proof state before:
case inl.intro
α : 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 α
O : Matroid γ
h2 : emptyOn β ≂ O
⊢ emptyOn α ≂ O
Tactic:
rwa [IsIso.comm, isIso_emptyOn_iff] at h2 ⊢
Proof state after:
no goals
Theorem: Matroid.IsIso.trans
Proof state before:
case inr.intro.inl.intro
α : 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 α
M : Matroid α
i1 : M.Iso (emptyOn β)
⊢ M ≂ emptyOn γ
Tactic:
rw [isIso_emptyOn_iff]
Proof state after:
case inr.intro.inl.intro
α : 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 α
M : Matroid α
i1 : M.Iso (emptyOn β)
⊢ M = emptyOn α
Theorem: Matroid.IsIso.trans
Proof state before:
case inr.intro.inl.intro
α : 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 α
M : Matroid α
i1 : M.Iso (emptyOn β)
⊢ M = emptyOn α
Tactic:
exact isIso_emptyOn_iff.1 i1.isIso
Proof state after:
no goals
Theorem: Matroid.IsIso.empty_or_nonempty_iso
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 α
M : Matroid α
N : Matroid β
h : M ≂ N
⊢ M = emptyOn α ∧ N = emptyOn β ∨ Nonempty α ∧ Nonempty β ∧ Nonempty (M.Iso N)
Tactic:
obtain (⟨rfl,rfl⟩ | ⟨⟨e⟩⟩) := h
Proof state after:
case inl.intro
α : 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 α
⊢ emptyOn α = emptyOn α ∧ emptyOn β = emptyOn β ∨ Nonempty α ∧ Nonempty β ∧ Nonempty ((emptyOn α).Iso (emptyOn β))

case inr.intro
α : 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 α
M : Matroid α
N : Matroid β
e : M.Iso N
⊢ M = emptyOn α ∧ N = emptyOn β ∨ Nonempty α ∧ Nonempty β ∧ Nonempty (M.Iso N)