Theorem: Partition.ext (Matroid/ForMathlib/SetPartition.lean)

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
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

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
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'✝ }

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]
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✝

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
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✝

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
State after:
no goals