internlm/Lean-Github huggingface dataset:
Theorem: Matroid.IsIso.empty_or_nonempty_iso
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 β
e : M.Iso N
⊢ M = emptyOn α ∧ N = emptyOn β ∨ Nonempty α ∧ Nonempty β ∧ Nonempty (M.Iso N)
Tactic:
cases isEmpty_or_nonempty α
Proof state after:
case inr.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 β
e : M.Iso N
h✝ : IsEmpty α
⊢ M = emptyOn α ∧ N = emptyOn β ∨ Nonempty α ∧ Nonempty β ∧ Nonempty (M.Iso N)

case inr.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 β
e : M.Iso N
h✝ : Nonempty α
⊢ M = emptyOn α ∧ N = emptyOn β ∨ Nonempty α ∧ Nonempty β ∧ Nonempty (M.Iso N)
Theorem: Matroid.IsIso.empty_or_nonempty_iso
Proof state before:
case inr.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 β
e : M.Iso N
h✝ : Nonempty α
⊢ M = emptyOn α ∧ N = emptyOn β ∨ Nonempty α ∧ Nonempty β ∧ Nonempty (M.Iso N)
Tactic:
cases isEmpty_or_nonempty β
Proof state after:
case inr.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 β
e : M.Iso N
h✝¹ : Nonempty α
h✝ : IsEmpty β
⊢ M = emptyOn α ∧ N = emptyOn β ∨ Nonempty α ∧ Nonempty β ∧ Nonempty (M.Iso N)

case inr.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 β
e : M.Iso N
h✝¹ : Nonempty α
h✝ : Nonempty β
⊢ M = emptyOn α ∧ N = emptyOn β ∨ Nonempty α ∧ Nonempty β ∧ Nonempty (M.Iso N)
Theorem: Matroid.IsIso.empty_or_nonempty_iso
Proof state before:
case inr.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 β
e : M.Iso N
h✝¹ : Nonempty α
h✝ : Nonempty β
⊢ M = emptyOn α ∧ N = emptyOn β ∨ Nonempty α ∧ Nonempty β ∧ Nonempty (M.Iso N)
Tactic:
right
Proof state after:
case inr.intro.inr.inr.h
α : 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
h✝¹ : Nonempty α
h✝ : Nonempty β
⊢ Nonempty α ∧ Nonempty β ∧ Nonempty (M.Iso N)
Theorem: Matroid.IsIso.empty_or_nonempty_iso
Proof state before:
case inr.intro.inr.inr.h
α : 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
h✝¹ : Nonempty α
h✝ : Nonempty β
⊢ Nonempty α ∧ Nonempty β ∧ Nonempty (M.Iso N)
Tactic:
exact ⟨by assumption, by assumption, ⟨e⟩⟩
Proof state after:
no goals
Theorem: Matroid.IsIso.empty_or_nonempty_iso
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 α
⊢ emptyOn α = emptyOn α ∧ emptyOn β = emptyOn β ∨ Nonempty α ∧ Nonempty β ∧ Nonempty ((emptyOn α).Iso (emptyOn β))
Tactic:
exact Or.inl ⟨rfl,rfl⟩
Proof state after:
no goals
Theorem: Matroid.IsIso.empty_or_nonempty_iso
Proof state before:
case inr.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 β
e : M.Iso N
h✝ : IsEmpty α
⊢ M = emptyOn α ∧ N = emptyOn β ∨ Nonempty α ∧ Nonempty β ∧ Nonempty (M.Iso N)
Tactic:
left
Proof state after:
case inr.intro.inl.h
α : 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
h✝ : IsEmpty α
⊢ M = emptyOn α ∧ N = emptyOn β
Theorem: Matroid.IsIso.empty_or_nonempty_iso
Proof state before:
case inr.intro.inl.h
α : 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
h✝ : IsEmpty α
⊢ M = emptyOn α ∧ N = emptyOn β
Tactic:
obtain rfl := eq_emptyOn M
Proof state after:
case inr.intro.inl.h
α : 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 α
N : Matroid β
h✝ : IsEmpty α
e : (emptyOn α).Iso N
⊢ emptyOn α = emptyOn α ∧ N = emptyOn β
Theorem: Matroid.IsIso.empty_or_nonempty_iso
Proof state before:
case inr.intro.inl.h
α : 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 α
N : Matroid β
h✝ : IsEmpty α
e : (emptyOn α).Iso N
⊢ emptyOn α = emptyOn α ∧ N = emptyOn β
Tactic:
simp [isIso_emptyOn_iff.1 e.symm.isIso]
Proof state after:
no goals
Theorem: Matroid.IsIso.empty_or_nonempty_iso
Proof state before:
case inr.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 β
e : M.Iso N
h✝¹ : Nonempty α
h✝ : IsEmpty β
⊢ M = emptyOn α ∧ N = emptyOn β ∨ Nonempty α ∧ Nonempty β ∧ Nonempty (M.Iso N)
Tactic:
left
Proof state after:
case inr.intro.inr.inl.h
α : 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
h✝¹ : Nonempty α
h✝ : IsEmpty β
⊢ M = emptyOn α ∧ N = emptyOn β
Theorem: Matroid.IsIso.empty_or_nonempty_iso
Proof state before:
case inr.intro.inr.inl.h
α : 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
h✝¹ : Nonempty α
h✝ : IsEmpty β
⊢ M = emptyOn α ∧ N = emptyOn β
Tactic:
obtain rfl := eq_emptyOn N
Proof state after:
case inr.intro.inr.inl.h
α : 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 α
h✝¹ : Nonempty α
h✝ : IsEmpty β
e : M.Iso (emptyOn β)
⊢ M = emptyOn α ∧ emptyOn β = emptyOn β
Theorem: Matroid.IsIso.empty_or_nonempty_iso
Proof state before:
case inr.intro.inr.inl.h
α : 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 α
h✝¹ : Nonempty α
h✝ : IsEmpty β
e : M.Iso (emptyOn β)
⊢ M = emptyOn α ∧ emptyOn β = emptyOn β
Tactic:
simp [isIso_emptyOn_iff.1 e.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 β
e : M.Iso N
h✝¹ : Nonempty α
h✝ : Nonempty β
⊢ Nonempty α
Tactic:
assumption
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 β
e : M.Iso N
h✝¹ : Nonempty α
h✝ : Nonempty β
⊢ Nonempty β
Tactic:
assumption
Proof state after:
no goals
Theorem: Matroid.IsIso.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 β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
h : M ≂ N
⊢ 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 α
inst✝¹ : Nonempty α
inst✝ : 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 β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
e : M.Iso N
⊢ Nonempty (M.Iso N)
Theorem: Matroid.IsIso.nonempty_iso
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 β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
e : M.Iso N
⊢ Nonempty (M.Iso N)
Tactic:
exact ⟨e⟩
Proof state after:
no goals
Theorem: Matroid.IsIso.nonempty_iso
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 α
inst✝¹ : Nonempty α
inst✝ : Nonempty β
⊢ Nonempty ((emptyOn α).Iso (emptyOn β))
Tactic:
exact ⟨Iso.of_emptyOn⟩
Proof state after:
no goals
Theorem: Matroid.IsIso.finite_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 β
h : M ≂ N
⊢ M.Finite ↔ N.Finite
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 α).Finite ↔ (emptyOn β).Finite

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.Finite ↔ N.Finite
Theorem: Matroid.IsIso.finite_iff
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 β
e : M.Iso N
⊢ M.Finite ↔ N.Finite
Tactic:
refine ⟨fun ⟨h⟩ ↦ ⟨?_⟩, fun ⟨h⟩ ↦ ⟨?_⟩⟩
Proof state after:
case inr.intro.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 β
e : M.Iso N
x✝ : M.Finite
h : M.E.Finite
⊢ N.E.Finite

case inr.intro.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 β
e : M.Iso N
x✝ : N.Finite
h : N.E.Finite
⊢ M.E.Finite
Theorem: Matroid.IsIso.finite_iff
Proof state before:
case inr.intro.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 β
e : M.Iso N
x✝ : N.Finite
h : N.E.Finite
⊢ M.E.Finite
Tactic:
rw [← encard_ne_top_iff] at h ⊢
Proof state after:
case inr.intro.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 β
e : M.Iso N
x✝ : N.Finite
h : N.E.encard ≠ ⊤
⊢ M.E.encard ≠ ⊤
Theorem: Matroid.IsIso.finite_iff
Proof state before:
case inr.intro.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 β
e : M.Iso N
x✝ : N.Finite
h : N.E.encard ≠ ⊤
⊢ M.E.encard ≠ ⊤
Tactic:
rwa [e.encard_ground_eq]
Proof state after:
no goals
Theorem: Matroid.IsIso.finite_iff
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 α
⊢ (emptyOn α).Finite ↔ (emptyOn β).Finite
Tactic:
exact iff_of_true (finite_emptyOn α) (finite_emptyOn β)
Proof state after:
no goals
Theorem: Matroid.IsIso.finite_iff
Proof state before:
case inr.intro.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 β
e : M.Iso N
x✝ : M.Finite
h : M.E.Finite
⊢ N.E.Finite
Tactic:
rw [← encard_ne_top_iff] at h ⊢
Proof state after:
case inr.intro.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 β
e : M.Iso N
x✝ : M.Finite
h : M.E.encard ≠ ⊤
⊢ N.E.encard ≠ ⊤
Theorem: Matroid.IsIso.finite_iff
Proof state before:
case inr.intro.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 β
e : M.Iso N
x✝ : M.Finite
h : M.E.encard ≠ ⊤
⊢ N.E.encard ≠ ⊤
Tactic:
rwa [e.encard_ground_eq] at h
Proof state after:
no goals
Theorem: Matroid.IsIso.finiteRk_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 β
h : M ≂ N
⊢ M.FiniteRk ↔ N.FiniteRk
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 α).FiniteRk ↔ (emptyOn β).FiniteRk

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.FiniteRk ↔ N.FiniteRk
Theorem: Matroid.IsIso.finiteRk_iff
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 β
e : M.Iso N
⊢ M.FiniteRk ↔ N.FiniteRk
Tactic:
exact ⟨fun ⟨B, hB, hBfin⟩ ↦ ⟨e '' B, e.on_base hB, hBfin.image _⟩,
  fun ⟨B, hB, hBfin⟩ ↦ ⟨e.symm '' B, e.symm.on_base hB, hBfin.image _⟩⟩
Proof state after:
no goals
Theorem: Matroid.IsIso.finiteRk_iff
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 α
⊢ (emptyOn α).FiniteRk ↔ (emptyOn β).FiniteRk
Tactic:
apply iff_of_true <;> infer_instance
Proof state after:
no goals
Theorem: Matroid.IsIso.dual
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✶ ≂ 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 β)✶

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✶ ≂ N✶
Theorem: Matroid.IsIso.dual
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 β
e : M.Iso N
⊢ M✶ ≂ N✶
Tactic:
exact Or.inr ⟨e.dual⟩
Proof state after:
no goals
Theorem: Matroid.IsIso.dual
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 α
⊢ (emptyOn α)✶ ≂ (emptyOn β)✶
Tactic:
exact Or.inl ⟨by simp, by simp⟩
Proof state after:
no goals
Theorem: Matroid.IsIso.dual
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 α
⊢ (emptyOn α)✶ = emptyOn α
Tactic:
simp
Proof state after:
no goals
Theorem: Matroid.IsIso.dual
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 α
⊢ (emptyOn β)✶ = emptyOn β
Tactic:
simp
Proof state after:
no goals
Theorem: Matroid.isIso_dual_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✶ ≂ N✶ ↔ M ≂ N
Tactic:
refine ⟨fun h ↦ ?_, IsIso.dual⟩
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 α
M : Matroid α
N : Matroid β
h : M✶ ≂ N✶
⊢ M ≂ N
Theorem: Matroid.isIso_dual_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 β
h : M✶ ≂ N✶
⊢ M ≂ N
Tactic:
rw [← dual_dual M, ← dual_dual N]
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 α
M : Matroid α
N : Matroid β
h : M✶ ≂ N✶
⊢ M✶✶ ≂ N✶✶
Theorem: Matroid.isIso_dual_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 β
h : M✶ ≂ N✶
⊢ M✶✶ ≂ N✶✶
Tactic:
exact h.dual
Proof state after:
no goals
Theorem: Matroid.isIso_emptyOn_emptyOn
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 β✝
α : Type u_7
β : Type u_8
⊢ emptyOn α ≂ emptyOn β
Tactic:
rw [isIso_emptyOn_iff]
Proof state after:
no goals
Theorem: Matroid.emptyOn_isIso_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
⊢ emptyOn β ≂ M ↔ M = emptyOn α
Tactic:
rw [IsIso.comm, isIso_emptyOn_iff]
Proof state after:
no goals
Theorem: Matroid.isIso_loopyOn_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
E : Set β
⊢ M ≂ loopyOn E ↔ M = loopyOn M.E ∧ Nonempty (↑M.E ≃ ↑E)
Tactic:
refine ⟨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 α
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
Theorem: Matroid.isIso_loopyOn_iff
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 α
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⟩⟩
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 α
M✝ : Matroid α
N : Matroid β✝
M : Matroid α
β : Type u_7
E : Set β
hM : M = loopyOn M.E
e : ↑M.E ≃ ↑E
⊢ M ≂ loopyOn E
Theorem: Matroid.isIso_loopyOn_iff
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 α
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 α
Proof 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
Theorem: Matroid.isIso_loopyOn_iff
Proof 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 β
Proof 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
Theorem: Matroid.isIso_loopyOn_iff
Proof 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
Proof 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)
Theorem: Matroid.isIso_loopyOn_iff
Proof 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
Proof 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)
Theorem: Matroid.isIso_loopyOn_iff
Proof 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
Proof 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)
Theorem: Matroid.isIso_loopyOn_iff
Proof 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
Proof state after:
no goals