Theorem: Matroid.isIso_loopyOn_iff (Matroid/Old/_Equiv.lean)

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
E : Set β
⊢ M ≂ loopyOn E ↔ M = loopyOn M.E ∧ Nonempty (↑M.E ≃ ↑E)
Tactic:
refine ⟨fun h ↦ ?_, ?_⟩
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 α
M✝ : Matroid α
N : Matroid β✝
M : Matroid α
β : Type u_7
E : Set β
h : M ≂ loopyOn E
⊢ M = loopyOn M.E ∧ Nonempty (↑M.E ≃ ↑E)

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 α
M✝ : Matroid α
N : Matroid β✝
M : Matroid α
β : Type u_7
E : Set β
⊢ M = loopyOn M.E ∧ Nonempty (↑M.E ≃ ↑E) → M ≂ loopyOn E

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 α
M✝ : Matroid α
N : Matroid β✝
M : Matroid α
β : Type u_7
E : Set β
⊢ M = loopyOn M.E ∧ Nonempty (↑M.E ≃ ↑E) → M ≂ loopyOn E
Tactic:
rintro ⟨hM, ⟨e⟩⟩
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 α
M✝ : Matroid α
N : Matroid β✝
M : Matroid α
β : Type u_7
E : Set β
hM : M = loopyOn M.E
e : ↑M.E ≃ ↑E
⊢ M ≂ loopyOn E

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 α
M✝ : Matroid α
N : Matroid β✝
M : Matroid α
β : Type u_7
E : Set β
hM : M = loopyOn M.E
e : ↑M.E ≃ ↑E
⊢ M ≂ loopyOn E
Tactic:
cases isEmpty_or_nonempty α
State after:
case refine_2.intro.intro.inl
α : 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
E : Set β
hM : M = loopyOn M.E
e : ↑M.E ≃ ↑E
h✝ : IsEmpty α
⊢ M ≂ loopyOn E

case refine_2.intro.intro.inr
α : 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
E : Set β
hM : M = loopyOn M.E
e : ↑M.E ≃ ↑E
h✝ : Nonempty α
⊢ M ≂ loopyOn E

State before:
case refine_2.intro.intro.inr
α : 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
E : Set β
hM : M = loopyOn M.E
e : ↑M.E ≃ ↑E
h✝ : Nonempty α
⊢ M ≂ loopyOn E
Tactic:
cases isEmpty_or_nonempty β
State after:
case refine_2.intro.intro.inr.inl
α : 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
E : Set β
hM : M = loopyOn M.E
e : ↑M.E ≃ ↑E
h✝¹ : Nonempty α
h✝ : IsEmpty β
⊢ M ≂ loopyOn E

case refine_2.intro.intro.inr.inr
α : 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
E : Set β
hM : M = loopyOn M.E
e : ↑M.E ≃ ↑E
h✝¹ : Nonempty α
h✝ : Nonempty β
⊢ M ≂ loopyOn E

State before:
case refine_2.intro.intro.inr.inr
α : 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
E : Set β
hM : M = loopyOn M.E
e : ↑M.E ≃ ↑E
h✝¹ : Nonempty α
h✝ : Nonempty β
⊢ M ≂ loopyOn E
Tactic:
refine (iso_of_forall_indep (PartialEquiv.ofSetEquiv e) (by simp) (by simp) ?_ (by simp)).isIso
State after:
case refine_2.intro.intro.inr.inr
α : 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
E : Set β
hM : M = loopyOn M.E
e : ↑M.E ≃ ↑E
h✝¹ : Nonempty α
h✝ : Nonempty β
⊢ ∀ (I : Set α), M.Indep I → (loopyOn E).Indep (↑(PartialEquiv.ofSetEquiv e) '' I)

State before:
case refine_2.intro.intro.inr.inr
α : 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
E : Set β
hM : M = loopyOn M.E
e : ↑M.E ≃ ↑E
h✝¹ : Nonempty α
h✝ : Nonempty β
⊢ ∀ (I : Set α), M.Indep I → (loopyOn E).Indep (↑(PartialEquiv.ofSetEquiv e) '' I)
Tactic:
intro I hI
State after:
case refine_2.intro.intro.inr.inr
α : 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
E : Set β
hM : M = loopyOn M.E
e : ↑M.E ≃ ↑E
h✝¹ : Nonempty α
h✝ : Nonempty β
I : Set α
hI : M.Indep I
⊢ (loopyOn E).Indep (↑(PartialEquiv.ofSetEquiv e) '' I)

State before:
case refine_2.intro.intro.inr.inr
α : 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
E : Set β
hM : M = loopyOn M.E
e : ↑M.E ≃ ↑E
h✝¹ : Nonempty α
h✝ : Nonempty β
I : Set α
hI : M.Indep I
⊢ (loopyOn E).Indep (↑(PartialEquiv.ofSetEquiv e) '' I)
Tactic:
simp only [eq_iff_indep_iff_indep_forall, loopyOn_ground, loopyOn_indep_iff, true_and] at hM
State after:
case refine_2.intro.intro.inr.inr
α : 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
E : Set β
e : ↑M.E ≃ ↑E
h✝¹ : Nonempty α
h✝ : Nonempty β
I : Set α
hI : M.Indep I
hM : ∀ I ⊆ M.E, M.Indep I ↔ I = ∅
⊢ (loopyOn E).Indep (↑(PartialEquiv.ofSetEquiv e) '' I)

State before:
case refine_2.intro.intro.inr.inr
α : 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
E : Set β
e : ↑M.E ≃ ↑E
h✝¹ : Nonempty α
h✝ : Nonempty β
I : Set α
hI : M.Indep I
hM : ∀ I ⊆ M.E, M.Indep I ↔ I = ∅
⊢ (loopyOn E).Indep (↑(PartialEquiv.ofSetEquiv e) '' I)
Tactic:
simpa using (hM I hI.subset_ground).1 hI
State after:
no goals

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 α
M✝ : Matroid α
N : Matroid β✝
M : Matroid α
β : Type u_7
E : Set β
h : M ≂ loopyOn E
⊢ M = loopyOn M.E ∧ Nonempty (↑M.E ≃ ↑E)
Tactic:
obtain (⟨rfl,hLoopy⟩ | ⟨-, -, ⟨e⟩⟩) := h.empty_or_nonempty_iso
State after:
case refine_1.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
E : Set β
hLoopy : loopyOn E = emptyOn β
h : emptyOn α ≂ loopyOn E
⊢ emptyOn α = loopyOn (emptyOn α).E ∧ Nonempty (↑(emptyOn α).E ≃ ↑E)

case refine_1.inr.intro.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 α
M✝ : Matroid α
N : Matroid β✝
M : Matroid α
β : Type u_7
E : Set β
h : M ≂ loopyOn E
e : M.Iso (loopyOn E)
⊢ M = loopyOn M.E ∧ Nonempty (↑M.E ≃ ↑E)

State before:
case refine_1.inr.intro.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 α
M✝ : Matroid α
N : Matroid β✝
M : Matroid α
β : Type u_7
E : Set β
h : M ≂ loopyOn E
e : M.Iso (loopyOn E)
⊢ M = loopyOn M.E ∧ Nonempty (↑M.E ≃ ↑E)
Tactic:
rw [eq_loopyOn_iff, and_iff_right rfl]
State after:
case refine_1.inr.intro.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 α
M✝ : Matroid α
N : Matroid β✝
M : Matroid α
β : Type u_7
E : Set β
h : M ≂ loopyOn E
e : M.Iso (loopyOn E)
⊢ (∀ X ⊆ M.E, M.Indep X → X = ∅) ∧ Nonempty (↑M.E ≃ ↑E)

State before:
case refine_1.inr.intro.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 α
M✝ : Matroid α
N : Matroid β✝
M : Matroid α
β : Type u_7
E : Set β
h : M ≂ loopyOn E
e : M.Iso (loopyOn E)
⊢ (∀ X ⊆ M.E, M.Indep X → X = ∅) ∧ Nonempty (↑M.E ≃ ↑E)
Tactic:
refine ⟨fun I _ hI ↦ by simpa using e.on_indep hI, ?_⟩
State after:
case refine_1.inr.intro.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 α
M✝ : Matroid α
N : Matroid β✝
M : Matroid α
β : Type u_7
E : Set β
h : M ≂ loopyOn E
e : M.Iso (loopyOn E)
⊢ Nonempty (↑M.E ≃ ↑E)

State before:
case refine_1.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
E : Set β
hLoopy : loopyOn E = emptyOn β
h : emptyOn α ≂ loopyOn E
⊢ emptyOn α = loopyOn (emptyOn α).E ∧ Nonempty (↑(emptyOn α).E ≃ ↑E)
Tactic:
simp only [emptyOn_ground, loopyOn_empty, true_and]
State after:
case refine_1.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
E : Set β
hLoopy : loopyOn E = emptyOn β
h : emptyOn α ≂ loopyOn E
⊢ Nonempty (↑∅ ≃ ↑E)

State before:
case refine_1.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
E : Set β
hLoopy : loopyOn E = emptyOn β
h : emptyOn α ≂ loopyOn E
⊢ Nonempty (↑∅ ≃ ↑E)
Tactic:
rw [← ground_eq_empty_iff, loopyOn_ground] at hLoopy
State after:
case refine_1.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
E : Set β
hLoopy : E = ∅
h : emptyOn α ≂ loopyOn E
⊢ Nonempty (↑∅ ≃ ↑E)

State before:
case refine_1.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
E : Set β
hLoopy : E = ∅
h : emptyOn α ≂ loopyOn E
⊢ Nonempty (↑∅ ≃ ↑E)
Tactic:
subst hLoopy
State after:
case refine_1.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
h : emptyOn α ≂ loopyOn ∅
⊢ Nonempty (↑∅ ≃ ↑∅)

State before:
case refine_1.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
h : emptyOn α ≂ loopyOn ∅
⊢ Nonempty (↑∅ ≃ ↑∅)
Tactic:
exact Fintype.card_eq.mp rfl
State after:
no goals

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
E : Set β
h : M ≂ loopyOn E
e : M.Iso (loopyOn E)
I : Set α
x✝ : I ⊆ M.E
hI : M.Indep I
⊢ I = ∅
Tactic:
simpa using e.on_indep hI
State after:
no goals

State before:
case refine_1.inr.intro.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 α
M✝ : Matroid α
N : Matroid β✝
M : Matroid α
β : Type u_7
E : Set β
h : M ≂ loopyOn E
e : M.Iso (loopyOn E)
⊢ Nonempty (↑M.E ≃ ↑E)
Tactic:
convert Nonempty.intro e.toPartialEquiv.toEquiv <;> simp
State after:
no goals

State before:
case refine_2.intro.intro.inl
α : 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
E : Set β
hM : M = loopyOn M.E
e : ↑M.E ≃ ↑E
h✝ : IsEmpty α
⊢ M ≂ loopyOn E
Tactic:
simp only [eq_emptyOn, emptyOn_isIso_iff, ← ground_eq_empty_iff, loopyOn_ground]
State after:
case refine_2.intro.intro.inl
α : 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
E : Set β
hM : M = loopyOn M.E
e : ↑M.E ≃ ↑E
h✝ : IsEmpty α
⊢ E = ∅

State before:
case refine_2.intro.intro.inl
α : 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
E : Set β
hM : M = loopyOn M.E
e : ↑M.E ≃ ↑E
h✝ : IsEmpty α
⊢ E = ∅
Tactic:
exact isEmpty_coe_sort.1 e.symm.isEmpty
State after:
no goals

State before:
case refine_2.intro.intro.inr.inl
α : 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
E : Set β
hM : M = loopyOn M.E
e : ↑M.E ≃ ↑E
h✝¹ : Nonempty α
h✝ : IsEmpty β
⊢ M ≂ loopyOn E
Tactic:
simp only [eq_emptyOn, isIso_emptyOn_iff]
State after:
case refine_2.intro.intro.inr.inl
α : 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
E : Set β
hM : M = loopyOn M.E
e : ↑M.E ≃ ↑E
h✝¹ : Nonempty α
h✝ : IsEmpty β
⊢ M = emptyOn α

State before:
case refine_2.intro.intro.inr.inl
α : 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
E : Set β
hM : M = loopyOn M.E
e : ↑M.E ≃ ↑E
h✝¹ : Nonempty α
h✝ : IsEmpty β
⊢ M = emptyOn α
Tactic:
rw [← ground_eq_empty_iff, ← isEmpty_coe_sort]
State after:
case refine_2.intro.intro.inr.inl
α : 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
E : Set β
hM : M = loopyOn M.E
e : ↑M.E ≃ ↑E
h✝¹ : Nonempty α
h✝ : IsEmpty β
⊢ IsEmpty ↑M.E

State before:
case refine_2.intro.intro.inr.inl
α : 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
E : Set β
hM : M = loopyOn M.E
e : ↑M.E ≃ ↑E
h✝¹ : Nonempty α
h✝ : IsEmpty β
⊢ IsEmpty ↑M.E
Tactic:
rw [E.eq_empty_of_isEmpty] at e
State after:
case refine_2.intro.intro.inr.inl
α : 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
E : Set β
hM : M = loopyOn M.E
e : ↑M.E ≃ ↑∅
h✝¹ : Nonempty α
h✝ : IsEmpty β
⊢ IsEmpty ↑M.E

State before:
case refine_2.intro.intro.inr.inl
α : 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
E : Set β
hM : M = loopyOn M.E
e : ↑M.E ≃ ↑∅
h✝¹ : Nonempty α
h✝ : IsEmpty β
⊢ IsEmpty ↑M.E
Tactic:
exact e.isEmpty
State after:
no goals

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
E : Set β
hM : M = loopyOn M.E
e : ↑M.E ≃ ↑E
h✝¹ : Nonempty α
h✝ : Nonempty β
⊢ (PartialEquiv.ofSetEquiv e).source = M.E
Tactic:
simp
State after:
no goals

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
E : Set β
hM : M = loopyOn M.E
e : ↑M.E ≃ ↑E
h✝¹ : Nonempty α
h✝ : Nonempty β
⊢ (PartialEquiv.ofSetEquiv e).target = (loopyOn E).E
Tactic:
simp
State after:
no goals

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
E : Set β
hM : M = loopyOn M.E
e : ↑M.E ≃ ↑E
h✝¹ : Nonempty α
h✝ : Nonempty β
⊢ ∀ (I : Set β), (loopyOn E).Indep I → M.Indep (↑(PartialEquiv.ofSetEquiv e).symm '' I)
Tactic:
simp
State after:
no goals