internlm/Lean-Github huggingface dataset:
Theorem: Matroid.isIso_loopyOn_iff
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 α
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
Proof 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)
Theorem: Matroid.isIso_loopyOn_iff
Proof 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]
Proof 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)
Theorem: Matroid.isIso_loopyOn_iff
Proof 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, ?_⟩
Proof 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)
Theorem: Matroid.isIso_loopyOn_iff
Proof 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]
Proof 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)
Theorem: Matroid.isIso_loopyOn_iff
Proof 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
Proof 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)
Theorem: Matroid.isIso_loopyOn_iff
Proof 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
Proof 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 (↑∅ ≃ ↑∅)
Theorem: Matroid.isIso_loopyOn_iff
Proof 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
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 β
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
Proof state after:
no goals
Theorem: Matroid.isIso_loopyOn_iff
Proof 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
Proof state after:
no goals
Theorem: Matroid.isIso_loopyOn_iff
Proof 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]
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 α
⊢ E = ∅
Theorem: Matroid.isIso_loopyOn_iff
Proof 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
Proof state after:
no goals
Theorem: Matroid.isIso_loopyOn_iff
Proof 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]
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 = emptyOn α
Theorem: Matroid.isIso_loopyOn_iff
Proof 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]
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 β
⊢ IsEmpty ↑M.E
Theorem: Matroid.isIso_loopyOn_iff
Proof 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
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 ≃ ↑∅
h✝¹ : Nonempty α
h✝ : IsEmpty β
⊢ IsEmpty ↑M.E
Theorem: Matroid.isIso_loopyOn_iff
Proof 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
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 β
hM : M = loopyOn M.E
e : ↑M.E ≃ ↑E
h✝¹ : Nonempty α
h✝ : Nonempty β
⊢ (PartialEquiv.ofSetEquiv e).source = M.E
Tactic:
simp
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 β
hM : M = loopyOn M.E
e : ↑M.E ≃ ↑E
h✝¹ : Nonempty α
h✝ : Nonempty β
⊢ (PartialEquiv.ofSetEquiv e).target = (loopyOn E).E
Tactic:
simp
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 β
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
Proof state after:
no goals
Theorem: Matroid.isIso_freeOn_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 ≂ freeOn E ↔ M = freeOn M.E ∧ Nonempty (↑M.E ≃ ↑E)
Tactic:
rw [← isIso_dual_iff, freeOn_dual_eq, isIso_loopyOn_iff, ← eq_dual_iff_dual_eq, dual_ground,
  loopyOn_dual_eq]
Proof state after:
no goals
Theorem: Partition.ext
Proof state before:
α : Type u_1
inst✝ : CompleteLattice α
s x y z : α
P✝ P Q : Partition s
hP : ∀ (x : α), x ∈ P ↔ x ∈ Q
⊢ P = Q
Tactic:
cases P
Proof state after:
case mk
α : Type u_1
inst✝ : CompleteLattice α
s x y z : α
P Q : Partition s
parts✝ : Set α
setIndependent✝ : CompleteLattice.SetIndependent parts✝
bot_not_mem✝ : ⊥ ∉ parts✝
sSup_eq'✝ : sSup parts✝ = s
hP :
  ∀ (x : α),
    x ∈ { parts := parts✝, setIndependent := setIndependent✝, bot_not_mem := bot_not_mem✝, sSup_eq' := sSup_eq'✝ } ↔
      x ∈ Q
⊢ { parts := parts✝, setIndependent := setIndependent✝, bot_not_mem := bot_not_mem✝, sSup_eq' := sSup_eq'✝ } = Q
Theorem: Partition.ext
Proof state before:
case mk
α : Type u_1
inst✝ : CompleteLattice α
s x y z : α
P Q : Partition s
parts✝ : Set α
setIndependent✝ : CompleteLattice.SetIndependent parts✝
bot_not_mem✝ : ⊥ ∉ parts✝
sSup_eq'✝ : sSup parts✝ = s
hP :
  ∀ (x : α),
    x ∈ { parts := parts✝, setIndependent := setIndependent✝, bot_not_mem := bot_not_mem✝, sSup_eq' := sSup_eq'✝ } ↔
      x ∈ Q
⊢ { parts := parts✝, setIndependent := setIndependent✝, bot_not_mem := bot_not_mem✝, sSup_eq' := sSup_eq'✝ } = Q
Tactic:
cases Q
Proof state after:
case mk.mk
α : Type u_1
inst✝ : CompleteLattice α
s x y z : α
P : Partition s
parts✝¹ : Set α
setIndependent✝¹ : CompleteLattice.SetIndependent parts✝¹
bot_not_mem✝¹ : ⊥ ∉ parts✝¹
sSup_eq'✝¹ : sSup parts✝¹ = s
parts✝ : Set α
setIndependent✝ : CompleteLattice.SetIndependent parts✝
bot_not_mem✝ : ⊥ ∉ parts✝
sSup_eq'✝ : sSup parts✝ = s
hP :
  ∀ (x : α),
    x ∈ { parts := parts✝¹, setIndependent := setIndependent✝¹, bot_not_mem := bot_not_mem✝¹, sSup_eq' := sSup_eq'✝¹ } ↔
      x ∈ { parts := parts✝, setIndependent := setIndependent✝, bot_not_mem := bot_not_mem✝, sSup_eq' := sSup_eq'✝ }
⊢ { parts := parts✝¹, setIndependent := setIndependent✝¹, bot_not_mem := bot_not_mem✝¹, sSup_eq' := sSup_eq'✝¹ } =
    { parts := parts✝, setIndependent := setIndependent✝, bot_not_mem := bot_not_mem✝, sSup_eq' := sSup_eq'✝ }
Theorem: Partition.ext
Proof state before:
case mk.mk
α : Type u_1
inst✝ : CompleteLattice α
s x y z : α
P : Partition s
parts✝¹ : Set α
setIndependent✝¹ : CompleteLattice.SetIndependent parts✝¹
bot_not_mem✝¹ : ⊥ ∉ parts✝¹
sSup_eq'✝¹ : sSup parts✝¹ = s
parts✝ : Set α
setIndependent✝ : CompleteLattice.SetIndependent parts✝
bot_not_mem✝ : ⊥ ∉ parts✝
sSup_eq'✝ : sSup parts✝ = s
hP :
  ∀ (x : α),
    x ∈ { parts := parts✝¹, setIndependent := setIndependent✝¹, bot_not_mem := bot_not_mem✝¹, sSup_eq' := sSup_eq'✝¹ } ↔
      x ∈ { parts := parts✝, setIndependent := setIndependent✝, bot_not_mem := bot_not_mem✝, sSup_eq' := sSup_eq'✝ }
⊢ { parts := parts✝¹, setIndependent := setIndependent✝¹, bot_not_mem := bot_not_mem✝¹, sSup_eq' := sSup_eq'✝¹ } =
    { parts := parts✝, setIndependent := setIndependent✝, bot_not_mem := bot_not_mem✝, sSup_eq' := sSup_eq'✝ }
Tactic:
simp only [mk.injEq]
Proof state after:
case mk.mk
α : Type u_1
inst✝ : CompleteLattice α
s x y z : α
P : Partition s
parts✝¹ : Set α
setIndependent✝¹ : CompleteLattice.SetIndependent parts✝¹
bot_not_mem✝¹ : ⊥ ∉ parts✝¹
sSup_eq'✝¹ : sSup parts✝¹ = s
parts✝ : Set α
setIndependent✝ : CompleteLattice.SetIndependent parts✝
bot_not_mem✝ : ⊥ ∉ parts✝
sSup_eq'✝ : sSup parts✝ = s
hP :
  ∀ (x : α),
    x ∈ { parts := parts✝¹, setIndependent := setIndependent✝¹, bot_not_mem := bot_not_mem✝¹, sSup_eq' := sSup_eq'✝¹ } ↔
      x ∈ { parts := parts✝, setIndependent := setIndependent✝, bot_not_mem := bot_not_mem✝, sSup_eq' := sSup_eq'✝ }
⊢ parts✝¹ = parts✝
Theorem: Partition.ext
Proof state before:
case mk.mk
α : Type u_1
inst✝ : CompleteLattice α
s x y z : α
P : Partition s
parts✝¹ : Set α
setIndependent✝¹ : CompleteLattice.SetIndependent parts✝¹
bot_not_mem✝¹ : ⊥ ∉ parts✝¹
sSup_eq'✝¹ : sSup parts✝¹ = s
parts✝ : Set α
setIndependent✝ : CompleteLattice.SetIndependent parts✝
bot_not_mem✝ : ⊥ ∉ parts✝
sSup_eq'✝ : sSup parts✝ = s
hP :
  ∀ (x : α),
    x ∈ { parts := parts✝¹, setIndependent := setIndependent✝¹, bot_not_mem := bot_not_mem✝¹, sSup_eq' := sSup_eq'✝¹ } ↔
      x ∈ { parts := parts✝, setIndependent := setIndependent✝, bot_not_mem := bot_not_mem✝, sSup_eq' := sSup_eq'✝ }
⊢ parts✝¹ = parts✝
Tactic:
ext x
Proof state after:
case mk.mk.h
α : Type u_1
inst✝ : CompleteLattice α
s x✝ y z : α
P : Partition s
parts✝¹ : Set α
setIndependent✝¹ : CompleteLattice.SetIndependent parts✝¹
bot_not_mem✝¹ : ⊥ ∉ parts✝¹
sSup_eq'✝¹ : sSup parts✝¹ = s
parts✝ : Set α
setIndependent✝ : CompleteLattice.SetIndependent parts✝
bot_not_mem✝ : ⊥ ∉ parts✝
sSup_eq'✝ : sSup parts✝ = s
hP :
  ∀ (x : α),
    x ∈ { parts := parts✝¹, setIndependent := setIndependent✝¹, bot_not_mem := bot_not_mem✝¹, sSup_eq' := sSup_eq'✝¹ } ↔
      x ∈ { parts := parts✝, setIndependent := setIndependent✝, bot_not_mem := bot_not_mem✝, sSup_eq' := sSup_eq'✝ }
x : α
⊢ x ∈ parts✝¹ ↔ x ∈ parts✝
Theorem: Partition.ext
Proof state before:
case mk.mk.h
α : Type u_1
inst✝ : CompleteLattice α
s x✝ y z : α
P : Partition s
parts✝¹ : Set α
setIndependent✝¹ : CompleteLattice.SetIndependent parts✝¹
bot_not_mem✝¹ : ⊥ ∉ parts✝¹
sSup_eq'✝¹ : sSup parts✝¹ = s
parts✝ : Set α
setIndependent✝ : CompleteLattice.SetIndependent parts✝
bot_not_mem✝ : ⊥ ∉ parts✝
sSup_eq'✝ : sSup parts✝ = s
hP :
  ∀ (x : α),
    x ∈ { parts := parts✝¹, setIndependent := setIndependent✝¹, bot_not_mem := bot_not_mem✝¹, sSup_eq' := sSup_eq'✝¹ } ↔
      x ∈ { parts := parts✝, setIndependent := setIndependent✝, bot_not_mem := bot_not_mem✝, sSup_eq' := sSup_eq'✝ }
x : α
⊢ x ∈ parts✝¹ ↔ x ∈ parts✝
Tactic:
simpa using hP x
Proof state after:
no goals
Theorem: Partition.iSup_eq
Proof state before:
α : Type u_1
inst✝ : CompleteLattice α
s x y z : α
P✝ P : Partition s
⊢ ⨆ x ∈ P, x = s
Tactic:
simp_rw [← P.sSup_eq', sSup_eq_iSup]
Proof state after:
α : Type u_1
inst✝ : CompleteLattice α
s x y z : α
P✝ P : Partition s
⊢ ⨆ x ∈ P, x = ⨆ a ∈ P.parts, a
Theorem: Partition.iSup_eq
Proof state before:
α : Type u_1
inst✝ : CompleteLattice α
s x y z : α
P✝ P : Partition s
⊢ ⨆ x ∈ P, x = ⨆ a ∈ P.parts, a
Tactic:
rfl
Proof state after:
no goals
Theorem: Partition.parts_nonempty
Proof state before:
α : Type u_1
inst✝ : CompleteLattice α
s x y z : α
P✝ P : Partition s
hs : s ≠ ⊥
hP : ↑P = ∅
⊢ False
Tactic:
simp [← P.sSup_eq, hP, sSup_empty] at hs
Proof state after:
no goals
Theorem: Partition.not_mem_empty
Proof state before:
α✝ : Type u_1
inst✝¹ : CompleteLattice α✝
s x y z : α✝
α : Type u_2
inst✝ : CompleteLattice α
a : α
⊢ a ∉ Partition.empty α
Tactic:
rw [← SetLike.mem_coe, empty_coe_eq]
Proof state after:
α✝ : Type u_1
inst✝¹ : CompleteLattice α✝
s x y z : α✝
α : Type u_2
inst✝ : CompleteLattice α
a : α
⊢ a ∉ ∅
Theorem: Partition.not_mem_empty
Proof state before:
α✝ : Type u_1
inst✝¹ : CompleteLattice α✝
s x y z : α✝
α : Type u_2
inst✝ : CompleteLattice α
a : α
⊢ a ∉ ∅
Tactic:
simp
Proof state after:
no goals
Theorem: Partition.eq_empty
Proof state before:
α : Type u_1
inst✝ : CompleteLattice α
s x y z : α
P : Partition ⊥
⊢ P = Partition.empty α
Tactic:
ext x
Proof state after:
case hP
α : Type u_1
inst✝ : CompleteLattice α
s x✝ y z : α
P : Partition ⊥
x : α
⊢ x ∈ P ↔ x ∈ Partition.empty α
Theorem: Partition.eq_empty
Proof state before:
case hP
α : Type u_1
inst✝ : CompleteLattice α
s x✝ y z : α
P : Partition ⊥
x : α
⊢ x ∈ P ↔ x ∈ Partition.empty α
Tactic:
have hsup := P.sSup_eq
Proof state after:
case hP
α : Type u_1
inst✝ : CompleteLattice α
s x✝ y z : α
P : Partition ⊥
x : α
hsup : sSup ↑P = ⊥
⊢ x ∈ P ↔ x ∈ Partition.empty α
Theorem: Partition.eq_empty
Proof state before:
case hP
α : Type u_1
inst✝ : CompleteLattice α
s x✝ y z : α
P : Partition ⊥
x : α
hsup : sSup ↑P = ⊥
⊢ x ∈ P ↔ x ∈ Partition.empty α
Tactic:
simp only [sSup_eq_bot, SetLike.mem_coe] at hsup
Proof state after:
case hP
α : Type u_1
inst✝ : CompleteLattice α
s x✝ y z : α
P : Partition ⊥
x : α
hsup : ∀ a ∈ P, a = ⊥
⊢ x ∈ P ↔ x ∈ Partition.empty α
Theorem: Partition.eq_empty
Proof state before:
case hP
α : Type u_1
inst✝ : CompleteLattice α
s x✝ y z : α
P : Partition ⊥
x : α
hsup : ∀ a ∈ P, a = ⊥
⊢ x ∈ P ↔ x ∈ Partition.empty α
Tactic:
simp only [not_mem_empty, iff_false]
Proof state after:
case hP
α : Type u_1
inst✝ : CompleteLattice α
s x✝ y z : α
P : Partition ⊥
x : α
hsup : ∀ a ∈ P, a = ⊥
⊢ x ∉ P
Theorem: Partition.eq_empty
Proof state before:
case hP
α : Type u_1
inst✝ : CompleteLattice α
s x✝ y z : α
P : Partition ⊥
x : α
hsup : ∀ a ∈ P, a = ⊥
⊢ x ∉ P
Tactic:
exact fun hx ↦ P.ne_bot_of_mem hx <| hsup x hx
Proof state after:
no goals
Theorem: Partition.mem_top_iff
Proof state before:
α✝ : Type u_1
inst✝¹ : CompleteLattice α✝
s✝ x y z : α✝
α : Type u_2
inst✝ : CompleteLattice α
a s : α
⊢ a ∈ ⊤ ↔ a = s ∧ a ≠ ⊥
Tactic:
change a ∈ Partition.congr _ _ ↔ _
Proof state after:
α✝ : Type u_1
inst✝¹ : CompleteLattice α✝
s✝ x y z : α✝
α : Type u_2
inst✝ : CompleteLattice α
a s : α
⊢ a ∈ (ofIndependent' ⋯).congr ⋯ ↔ a = s ∧ a ≠ ⊥
Theorem: Partition.mem_top_iff
Proof state before:
α✝ : Type u_1
inst✝¹ : CompleteLattice α✝
s✝ x y z : α✝
α : Type u_2
inst✝ : CompleteLattice α
a s : α
⊢ a ∈ (ofIndependent' ⋯).congr ⋯ ↔ a = s ∧ a ≠ ⊥
Tactic:
rw [mem_congr_iff, mem_ofIndependent'_iff, mem_singleton_iff]
Proof state after:
no goals
Theorem: Partition.top_eq_indiscrete
Proof state before:
α✝ : Type u_1
inst✝¹ : CompleteLattice α✝
s x y z : α✝
α : Type u_2
inst✝ : CompleteLattice α
hs : s ≠ ⊥
⊢ ⊤ = indiscrete s hs
Tactic:
ext a
Proof state after:
case hP
α✝ : Type u_1
inst✝¹ : CompleteLattice α✝
s x y z : α✝
α : Type u_2
inst✝ : CompleteLattice α
hs : s ≠ ⊥
a : α✝
⊢ a ∈ ⊤ ↔ a ∈ indiscrete s hs
Theorem: Partition.top_eq_indiscrete
Proof state before:
case hP
α✝ : Type u_1
inst✝¹ : CompleteLattice α✝
s x y z : α✝
α : Type u_2
inst✝ : CompleteLattice α
hs : s ≠ ⊥
a : α✝
⊢ a ∈ ⊤ ↔ a ∈ indiscrete s hs
Tactic:
rw [mem_top_iff, mem_indiscrete_iff, and_iff_left_iff_imp]
Proof state after:
case hP
α✝ : Type u_1
inst✝¹ : CompleteLattice α✝
s x y z : α✝
α : Type u_2
inst✝ : CompleteLattice α
hs : s ≠ ⊥
a : α✝
⊢ a = s → a ≠ ⊥
Theorem: Partition.top_eq_indiscrete
Proof state before:
case hP
α✝ : Type u_1
inst✝¹ : CompleteLattice α✝
s x y z : α✝
α : Type u_2
inst✝ : CompleteLattice α
hs : s ≠ ⊥
a : α✝
⊢ a = s → a ≠ ⊥
Tactic:
rintro rfl
Proof state after:
case hP
α✝ : Type u_1
inst✝¹ : CompleteLattice α✝
x y z : α✝
α : Type u_2
inst✝ : CompleteLattice α
a : α✝
hs : a ≠ ⊥
⊢ a ≠ ⊥
Theorem: Partition.top_eq_indiscrete
Proof state before:
case hP
α✝ : Type u_1
inst✝¹ : CompleteLattice α✝
x y z : α✝
α : Type u_2
inst✝ : CompleteLattice α
a : α✝
hs : a ≠ ⊥
⊢ a ≠ ⊥
Tactic:
assumption
Proof state after:
no goals
Theorem: Partition.parts_top_subset
Proof state before:
α✝ : Type u_1
inst✝¹ : CompleteLattice α✝
s✝ x y z : α✝
α : Type u_2
inst✝ : CompleteLattice α
s : α
⊢ ↑⊤ ⊆ {s}
Tactic:
simp
Proof state after:
no goals
Theorem: Partition.mem_bind_iff
Proof state before:
α✝ : Type u_1
inst✝¹ : CompleteLattice α✝
s✝ x y z : α✝
α : Type u_2
inst✝ : CompleteDistribLattice α
s : α
P : Partition s
Qs : (a : α) → a ∈ P → Partition a
a : α
⊢ a ∈ P.bind Qs ↔ ∃ b, ∃ (hb : b ∈ P), a ∈ Qs b hb
Tactic:
change _ ∈ ⋃ _, _ ↔ _
Proof state after:
α✝ : Type u_1
inst✝¹ : CompleteLattice α✝
s✝ x y z : α✝
α : Type u_2
inst✝ : CompleteDistribLattice α
s : α
P : Partition s
Qs : (a : α) → a ∈ P → Partition a
a : α
⊢ a ∈ ⋃ x, ↑(Qs ↑x ⋯) ↔ ∃ b, ∃ (hb : b ∈ P), a ∈ Qs b hb
Theorem: Partition.mem_bind_iff
Proof state before:
α✝ : Type u_1
inst✝¹ : CompleteLattice α✝
s✝ x y z : α✝
α : Type u_2
inst✝ : CompleteDistribLattice α
s : α
P : Partition s
Qs : (a : α) → a ∈ P → Partition a
a : α
⊢ a ∈ ⋃ x, ↑(Qs ↑x ⋯) ↔ ∃ b, ∃ (hb : b ∈ P), a ∈ Qs b hb
Tactic:
simp
Proof state after:
no goals
Theorem: Partition.bind_le
Proof state before:
α✝¹ : Type u_1
inst✝² : CompleteLattice α✝¹
s✝¹ x y z : α✝¹
α✝ : Type u_2
inst✝¹ : CompleteDistribLattice α✝
s✝ : α✝
α : Type u_3
inst✝ : CompleteDistribLattice α
s : α
P : Partition s
Qs : (a : α) → a ∈ P → Partition a
⊢ P.bind Qs ≤ P
Tactic:
intro t ht
Proof state after:
α✝¹ : Type u_1
inst✝² : CompleteLattice α✝¹
s✝¹ x y z : α✝¹
α✝ : Type u_2
inst✝¹ : CompleteDistribLattice α✝
s✝ : α✝
α : Type u_3
inst✝ : CompleteDistribLattice α
s : α
P : Partition s
Qs : (a : α) → a ∈ P → Partition a
t : α
ht : t ∈ P.bind Qs
⊢ ∃ y ∈ P, t ≤ y
Theorem: Partition.bind_le
Proof state before:
α✝¹ : Type u_1
inst✝² : CompleteLattice α✝¹
s✝¹ x y z : α✝¹
α✝ : Type u_2
inst✝¹ : CompleteDistribLattice α✝
s✝ : α✝
α : Type u_3
inst✝ : CompleteDistribLattice α
s : α
P : Partition s
Qs : (a : α) → a ∈ P → Partition a
t : α
ht : t ∈ P.bind Qs
⊢ ∃ y ∈ P, t ≤ y
Tactic:
obtain ⟨b, hbp, h⟩ := mem_bind_iff.1 ht
Proof state after:
case intro.intro
α✝¹ : Type u_1
inst✝² : CompleteLattice α✝¹
s✝¹ x y z : α✝¹
α✝ : Type u_2
inst✝¹ : CompleteDistribLattice α✝
s✝ : α✝
α : Type u_3
inst✝ : CompleteDistribLattice α
s : α
P : Partition s
Qs : (a : α) → a ∈ P → Partition a
t : α
ht : t ∈ P.bind Qs
b : α
hbp : b ∈ P
h : t ∈ Qs b hbp
⊢ ∃ y ∈ P, t ≤ y