internlm/Lean-Github huggingface dataset:
Theorem: MulAction.isMultiplyPreprimitive_of_bijective_map
Proof state before:
case w
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x =>
    match x with
    | { val := m, property := hm } => { val := φ m, property := ⋯ }
f' : ↥(SubMulAction.ofFixingSubgroup M s) →ₑ[φ'] ↥(SubMulAction.ofFixingSubgroup N t) :=
  {
    toFun := fun x =>
      match x with
      | { val := x, property := hx } => { val := f.toFun x, property := ⋯ },
    map_smul' := ⋯ }
y : β
hy : y ∈ SubMulAction.ofFixingSubgroup N t
x : α
hx : f x = y
⊢ x ∈ SubMulAction.ofFixingSubgroup M s
Tactic:
intro h
Proof state after:
case w
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h✝ : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x =>
    match x with
    | { val := m, property := hm } => { val := φ m, property := ⋯ }
f' : ↥(SubMulAction.ofFixingSubgroup M s) →ₑ[φ'] ↥(SubMulAction.ofFixingSubgroup N t) :=
  {
    toFun := fun x =>
      match x with
      | { val := x, property := hx } => { val := f.toFun x, property := ⋯ },
    map_smul' := ⋯ }
y : β
hy : y ∈ SubMulAction.ofFixingSubgroup N t
x : α
hx : f x = y
h : x ∈ s
⊢ False
Theorem: MulAction.isMultiplyPreprimitive_of_bijective_map
Proof state before:
case w
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h✝ : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x =>
    match x with
    | { val := m, property := hm } => { val := φ m, property := ⋯ }
f' : ↥(SubMulAction.ofFixingSubgroup M s) →ₑ[φ'] ↥(SubMulAction.ofFixingSubgroup N t) :=
  {
    toFun := fun x =>
      match x with
      | { val := x, property := hx } => { val := f.toFun x, property := ⋯ },
    map_smul' := ⋯ }
y : β
hy : y ∈ SubMulAction.ofFixingSubgroup N t
x : α
hx : f x = y
h : x ∈ s
⊢ False
Tactic:
apply hy
Proof state after:
case w
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h✝ : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x =>
    match x with
    | { val := m, property := hm } => { val := φ m, property := ⋯ }
f' : ↥(SubMulAction.ofFixingSubgroup M s) →ₑ[φ'] ↥(SubMulAction.ofFixingSubgroup N t) :=
  {
    toFun := fun x =>
      match x with
      | { val := x, property := hx } => { val := f.toFun x, property := ⋯ },
    map_smul' := ⋯ }
y : β
hy : y ∈ SubMulAction.ofFixingSubgroup N t
x : α
hx : f x = y
h : x ∈ s
⊢ y ∈ t
Theorem: MulAction.isMultiplyPreprimitive_of_bijective_map
Proof state before:
case w
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h✝ : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x =>
    match x with
    | { val := m, property := hm } => { val := φ m, property := ⋯ }
f' : ↥(SubMulAction.ofFixingSubgroup M s) →ₑ[φ'] ↥(SubMulAction.ofFixingSubgroup N t) :=
  {
    toFun := fun x =>
      match x with
      | { val := x, property := hx } => { val := f.toFun x, property := ⋯ },
    map_smul' := ⋯ }
y : β
hy : y ∈ SubMulAction.ofFixingSubgroup N t
x : α
hx : f x = y
h : x ∈ s
⊢ y ∈ t
Tactic:
rw [← hs']
Proof state after:
case w
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h✝ : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x =>
    match x with
    | { val := m, property := hm } => { val := φ m, property := ⋯ }
f' : ↥(SubMulAction.ofFixingSubgroup M s) →ₑ[φ'] ↥(SubMulAction.ofFixingSubgroup N t) :=
  {
    toFun := fun x =>
      match x with
      | { val := x, property := hx } => { val := f.toFun x, property := ⋯ },
    map_smul' := ⋯ }
y : β
hy : y ∈ SubMulAction.ofFixingSubgroup N t
x : α
hx : f x = y
h : x ∈ s
⊢ y ∈ ⇑f '' s
Theorem: MulAction.isMultiplyPreprimitive_of_bijective_map
Proof state before:
case w
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h✝ : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x =>
    match x with
    | { val := m, property := hm } => { val := φ m, property := ⋯ }
f' : ↥(SubMulAction.ofFixingSubgroup M s) →ₑ[φ'] ↥(SubMulAction.ofFixingSubgroup N t) :=
  {
    toFun := fun x =>
      match x with
      | { val := x, property := hx } => { val := f.toFun x, property := ⋯ },
    map_smul' := ⋯ }
y : β
hy : y ∈ SubMulAction.ofFixingSubgroup N t
x : α
hx : f x = y
h : x ∈ s
⊢ y ∈ ⇑f '' s
Tactic:
exact ⟨x, h, hx⟩
Proof state after:
no goals
Theorem: Setoid.isPartition_on
Proof state before:
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
⊢ IsPartition {u | ∃ t ∈ P, Subtype.val ⁻¹' t = u ∧ t ∩ s ≠ ∅}
Tactic:
constructor
Proof state after:
case left
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
⊢ ∅ ∉ {u | ∃ t ∈ P, Subtype.val ⁻¹' t = u ∧ t ∩ s ≠ ∅}

case right
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
⊢ ∀ (a : ↑s), ∃! b x, a ∈ b
Theorem: Setoid.isPartition_on
Proof state before:
case left
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
⊢ ∅ ∉ {u | ∃ t ∈ P, Subtype.val ⁻¹' t = u ∧ t ∩ s ≠ ∅}
Tactic:
intro h
Proof state after:
case left
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
h : ∅ ∈ {u | ∃ t ∈ P, Subtype.val ⁻¹' t = u ∧ t ∩ s ≠ ∅}
⊢ False
Theorem: Setoid.isPartition_on
Proof state before:
case left
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
h : ∅ ∈ {u | ∃ t ∈ P, Subtype.val ⁻¹' t = u ∧ t ∩ s ≠ ∅}
⊢ False
Tactic:
obtain ⟨t, _, ht, hts⟩ := Set.mem_setOf_eq.mp h
Proof state after:
case left.intro.intro.intro
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
h : ∅ ∈ {u | ∃ t ∈ P, Subtype.val ⁻¹' t = u ∧ t ∩ s ≠ ∅}
t : Set α
left✝ : t ∈ P
ht : Subtype.val ⁻¹' t = ∅
hts : t ∩ s ≠ ∅
⊢ False
Theorem: Setoid.isPartition_on
Proof state before:
case left.intro.intro.intro
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
h : ∅ ∈ {u | ∃ t ∈ P, Subtype.val ⁻¹' t = u ∧ t ∩ s ≠ ∅}
t : Set α
left✝ : t ∈ P
ht : Subtype.val ⁻¹' t = ∅
hts : t ∩ s ≠ ∅
⊢ False
Tactic:
apply hts
Proof state after:
case left.intro.intro.intro
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
h : ∅ ∈ {u | ∃ t ∈ P, Subtype.val ⁻¹' t = u ∧ t ∩ s ≠ ∅}
t : Set α
left✝ : t ∈ P
ht : Subtype.val ⁻¹' t = ∅
hts : t ∩ s ≠ ∅
⊢ t ∩ s = ∅
Theorem: Setoid.isPartition_on
Proof state before:
case left.intro.intro.intro
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
h : ∅ ∈ {u | ∃ t ∈ P, Subtype.val ⁻¹' t = u ∧ t ∩ s ≠ ∅}
t : Set α
left✝ : t ∈ P
ht : Subtype.val ⁻¹' t = ∅
hts : t ∩ s ≠ ∅
⊢ t ∩ s = ∅
Tactic:
rw [Set.inter_comm, ← Subtype.image_preimage_coe, ht, Set.image_empty]
Proof state after:
no goals
Theorem: Setoid.isPartition_on
Proof state before:
case right
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
⊢ ∀ (a : ↑s), ∃! b x, a ∈ b
Tactic:
intro a
Proof state after:
case right
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
a : ↑s
⊢ ∃! b x, a ∈ b
Theorem: Setoid.isPartition_on
Proof state before:
case right
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
a : ↑s
⊢ ∃! b x, a ∈ b
Tactic:
obtain ⟨t, ht⟩ := hP.right ↑a
Proof state after:
case right.intro
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
a : ↑s
t : Set α
ht : (fun b => ∃! x, ↑a ∈ b) t ∧ ∀ (y : Set α), (fun b => ∃! x, ↑a ∈ b) y → y = t
⊢ ∃! b x, a ∈ b
Theorem: Setoid.isPartition_on
Proof state before:
case right.intro
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
a : ↑s
t : Set α
ht : (fun b => ∃! x, ↑a ∈ b) t ∧ ∀ (y : Set α), (fun b => ∃! x, ↑a ∈ b) y → y = t
⊢ ∃! b x, a ∈ b
Tactic:
simp only [exists_unique_iff_exists, exists_prop, and_imp] at ht
Proof state after:
case right.intro
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
a : ↑s
t : Set α
ht : (t ∈ P ∧ ↑a ∈ t) ∧ ∀ y ∈ P, ↑a ∈ y → y = t
⊢ ∃! b x, a ∈ b
Theorem: Setoid.isPartition_on
Proof state before:
case right.intro
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
a : ↑s
t : Set α
ht : (t ∈ P ∧ ↑a ∈ t) ∧ ∀ y ∈ P, ↑a ∈ y → y = t
⊢ ∃! b x, a ∈ b
Tactic:
use Subtype.val ⁻¹' t
Proof state after:
case h
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
a : ↑s
t : Set α
ht : (t ∈ P ∧ ↑a ∈ t) ∧ ∀ y ∈ P, ↑a ∈ y → y = t
⊢ (fun b => ∃! x, a ∈ b) (Subtype.val ⁻¹' t) ∧ ∀ (y : Set ↑s), (fun b => ∃! x, a ∈ b) y → y = Subtype.val ⁻¹' t
Theorem: Setoid.isPartition_on
Proof state before:
case h
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
a : ↑s
t : Set α
ht : (t ∈ P ∧ ↑a ∈ t) ∧ ∀ y ∈ P, ↑a ∈ y → y = t
⊢ (fun b => ∃! x, a ∈ b) (Subtype.val ⁻¹' t) ∧ ∀ (y : Set ↑s), (fun b => ∃! x, a ∈ b) y → y = Subtype.val ⁻¹' t
Tactic:
constructor
Proof state after:
case h.left
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
a : ↑s
t : Set α
ht : (t ∈ P ∧ ↑a ∈ t) ∧ ∀ y ∈ P, ↑a ∈ y → y = t
⊢ (fun b => ∃! x, a ∈ b) (Subtype.val ⁻¹' t)

case h.right
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
a : ↑s
t : Set α
ht : (t ∈ P ∧ ↑a ∈ t) ∧ ∀ y ∈ P, ↑a ∈ y → y = t
⊢ ∀ (y : Set ↑s), (fun b => ∃! x, a ∈ b) y → y = Subtype.val ⁻¹' t
Theorem: Setoid.isPartition_on
Proof state before:
case h.left
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
a : ↑s
t : Set α
ht : (t ∈ P ∧ ↑a ∈ t) ∧ ∀ y ∈ P, ↑a ∈ y → y = t
⊢ (fun b => ∃! x, a ∈ b) (Subtype.val ⁻¹' t)
Tactic:
simp only [Ne.def, Set.mem_setOf_eq, Set.mem_preimage, exists_unique_iff_exists, exists_prop]
Proof state after:
case h.left
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
a : ↑s
t : Set α
ht : (t ∈ P ∧ ↑a ∈ t) ∧ ∀ y ∈ P, ↑a ∈ y → y = t
⊢ (∃ t_1 ∈ P, Subtype.val ⁻¹' t_1 = Subtype.val ⁻¹' t ∧ ¬t_1 ∩ s = ∅) ∧ ↑a ∈ t
Theorem: Setoid.isPartition_on
Proof state before:
case h.left
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
a : ↑s
t : Set α
ht : (t ∈ P ∧ ↑a ∈ t) ∧ ∀ y ∈ P, ↑a ∈ y → y = t
⊢ (∃ t_1 ∈ P, Subtype.val ⁻¹' t_1 = Subtype.val ⁻¹' t ∧ ¬t_1 ∩ s = ∅) ∧ ↑a ∈ t
Tactic:
refine ⟨⟨t, ht.1.1, rfl, ?_⟩, ht.1.2⟩
Proof state after:
case h.left
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
a : ↑s
t : Set α
ht : (t ∈ P ∧ ↑a ∈ t) ∧ ∀ y ∈ P, ↑a ∈ y → y = t
⊢ ¬t ∩ s = ∅
Theorem: Setoid.isPartition_on
Proof state before:
case h.left
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
a : ↑s
t : Set α
ht : (t ∈ P ∧ ↑a ∈ t) ∧ ∀ y ∈ P, ↑a ∈ y → y = t
⊢ ¬t ∩ s = ∅
Tactic:
intro h
Proof state after:
case h.left
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
a : ↑s
t : Set α
ht : (t ∈ P ∧ ↑a ∈ t) ∧ ∀ y ∈ P, ↑a ∈ y → y = t
h : t ∩ s = ∅
⊢ False
Theorem: Setoid.isPartition_on
Proof state before:
case h.left
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
a : ↑s
t : Set α
ht : (t ∈ P ∧ ↑a ∈ t) ∧ ∀ y ∈ P, ↑a ∈ y → y = t
h : t ∩ s = ∅
⊢ False
Tactic:
rw [← Set.mem_empty_iff_false (a : α), ← h]
Proof state after:
case h.left
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
a : ↑s
t : Set α
ht : (t ∈ P ∧ ↑a ∈ t) ∧ ∀ y ∈ P, ↑a ∈ y → y = t
h : t ∩ s = ∅
⊢ ↑a ∈ t ∩ s
Theorem: Setoid.isPartition_on
Proof state before:
case h.left
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
a : ↑s
t : Set α
ht : (t ∈ P ∧ ↑a ∈ t) ∧ ∀ y ∈ P, ↑a ∈ y → y = t
h : t ∩ s = ∅
⊢ ↑a ∈ t ∩ s
Tactic:
exact Set.mem_inter ht.left.right (Subtype.mem a)
Proof state after:
no goals
Theorem: Setoid.isPartition_on
Proof state before:
case h.right
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
a : ↑s
t : Set α
ht : (t ∈ P ∧ ↑a ∈ t) ∧ ∀ y ∈ P, ↑a ∈ y → y = t
⊢ ∀ (y : Set ↑s), (fun b => ∃! x, a ∈ b) y → y = Subtype.val ⁻¹' t
Tactic:
simp only [Ne.def, Set.mem_setOf_eq, exists_unique_iff_exists,
  exists_prop, and_imp, forall_exists_index]
Proof state after:
case h.right
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
a : ↑s
t : Set α
ht : (t ∈ P ∧ ↑a ∈ t) ∧ ∀ y ∈ P, ↑a ∈ y → y = t
⊢ ∀ (y : Set ↑s), ∀ x ∈ P, Subtype.val ⁻¹' x = y → ¬x ∩ s = ∅ → a ∈ y → y = Subtype.val ⁻¹' t
Theorem: Setoid.isPartition_on
Proof state before:
case h.right
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
a : ↑s
t : Set α
ht : (t ∈ P ∧ ↑a ∈ t) ∧ ∀ y ∈ P, ↑a ∈ y → y = t
⊢ ∀ (y : Set ↑s), ∀ x ∈ P, Subtype.val ⁻¹' x = y → ¬x ∩ s = ∅ → a ∈ y → y = Subtype.val ⁻¹' t
Tactic:
intro y x hxP hxy _ hay
Proof state after:
case h.right
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
a : ↑s
t : Set α
ht : (t ∈ P ∧ ↑a ∈ t) ∧ ∀ y ∈ P, ↑a ∈ y → y = t
y : Set ↑s
x : Set α
hxP : x ∈ P
hxy : Subtype.val ⁻¹' x = y
a✝ : ¬x ∩ s = ∅
hay : a ∈ y
⊢ y = Subtype.val ⁻¹' t
Theorem: Setoid.isPartition_on
Proof state before:
case h.right
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
a : ↑s
t : Set α
ht : (t ∈ P ∧ ↑a ∈ t) ∧ ∀ y ∈ P, ↑a ∈ y → y = t
y : Set ↑s
x : Set α
hxP : x ∈ P
hxy : Subtype.val ⁻¹' x = y
a✝ : ¬x ∩ s = ∅
hay : a ∈ y
⊢ y = Subtype.val ⁻¹' t
Tactic:
rw [← hxy, Subtype.preimage_coe_eq_preimage_coe_iff]
Proof state after:
case h.right
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
a : ↑s
t : Set α
ht : (t ∈ P ∧ ↑a ∈ t) ∧ ∀ y ∈ P, ↑a ∈ y → y = t
y : Set ↑s
x : Set α
hxP : x ∈ P
hxy : Subtype.val ⁻¹' x = y
a✝ : ¬x ∩ s = ∅
hay : a ∈ y
⊢ s ∩ x = s ∩ t
Theorem: Setoid.isPartition_on
Proof state before:
case h.right
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
a : ↑s
t : Set α
ht : (t ∈ P ∧ ↑a ∈ t) ∧ ∀ y ∈ P, ↑a ∈ y → y = t
y : Set ↑s
x : Set α
hxP : x ∈ P
hxy : Subtype.val ⁻¹' x = y
a✝ : ¬x ∩ s = ∅
hay : a ∈ y
⊢ s ∩ x = s ∩ t
Tactic:
congr
Proof state after:
case h.right.e_a
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
a : ↑s
t : Set α
ht : (t ∈ P ∧ ↑a ∈ t) ∧ ∀ y ∈ P, ↑a ∈ y → y = t
y : Set ↑s
x : Set α
hxP : x ∈ P
hxy : Subtype.val ⁻¹' x = y
a✝ : ¬x ∩ s = ∅
hay : a ∈ y
⊢ x = t
Theorem: Setoid.isPartition_on
Proof state before:
case h.right.e_a
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
a : ↑s
t : Set α
ht : (t ∈ P ∧ ↑a ∈ t) ∧ ∀ y ∈ P, ↑a ∈ y → y = t
y : Set ↑s
x : Set α
hxP : x ∈ P
hxy : Subtype.val ⁻¹' x = y
a✝ : ¬x ∩ s = ∅
hay : a ∈ y
⊢ x = t
Tactic:
apply ht.right x hxP
Proof state after:
case h.right.e_a
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
a : ↑s
t : Set α
ht : (t ∈ P ∧ ↑a ∈ t) ∧ ∀ y ∈ P, ↑a ∈ y → y = t
y : Set ↑s
x : Set α
hxP : x ∈ P
hxy : Subtype.val ⁻¹' x = y
a✝ : ¬x ∩ s = ∅
hay : a ∈ y
⊢ ↑a ∈ x
Theorem: Setoid.isPartition_on
Proof state before:
case h.right.e_a
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
a : ↑s
t : Set α
ht : (t ∈ P ∧ ↑a ∈ t) ∧ ∀ y ∈ P, ↑a ∈ y → y = t
y : Set ↑s
x : Set α
hxP : x ∈ P
hxy : Subtype.val ⁻¹' x = y
a✝ : ¬x ∩ s = ∅
hay : a ∈ y
⊢ ↑a ∈ x
Tactic:
rw [← Set.mem_preimage, hxy]
Proof state after:
case h.right.e_a
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
a : ↑s
t : Set α
ht : (t ∈ P ∧ ↑a ∈ t) ∧ ∀ y ∈ P, ↑a ∈ y → y = t
y : Set ↑s
x : Set α
hxP : x ∈ P
hxy : Subtype.val ⁻¹' x = y
a✝ : ¬x ∩ s = ∅
hay : a ∈ y
⊢ a ∈ y
Theorem: Setoid.isPartition_on
Proof state before:
case h.right.e_a
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
a : ↑s
t : Set α
ht : (t ∈ P ∧ ↑a ∈ t) ∧ ∀ y ∈ P, ↑a ∈ y → y = t
y : Set ↑s
x : Set α
hxP : x ∈ P
hxy : Subtype.val ⁻¹' x = y
a✝ : ¬x ∩ s = ∅
hay : a ∈ y
⊢ a ∈ y
Tactic:
exact hay
Proof state after:
no goals
Theorem: Partition.card_of_partition'
Proof state before:
α : Type u_1
inst✝ : Fintype α
c : Finset (Finset α)
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c}
⊢ ∑ s in c, s.card = Fintype.card α
Tactic:
rw [← mul_one (Fintype.card α), ← Finset.sum_card]
Proof state after:
α : Type u_1
inst✝ : Fintype α
c : Finset (Finset α)
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c}
⊢ ∀ (a : α), (Finset.filter (fun x => a ∈ x) c).card = 1
Theorem: Partition.card_of_partition'
Proof state before:
α : Type u_1
inst✝ : Fintype α
c : Finset (Finset α)
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c}
⊢ ∀ (a : α), (Finset.filter (fun x => a ∈ x) c).card = 1
Tactic:
intro a
Proof state after:
α : Type u_1
inst✝ : Fintype α
c : Finset (Finset α)
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c}
a : α
⊢ (Finset.filter (fun x => a ∈ x) c).card = 1
Theorem: Partition.card_of_partition'
Proof state before:
α : Type u_1
inst✝ : Fintype α
c : Finset (Finset α)
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c}
a : α
⊢ (Finset.filter (fun x => a ∈ x) c).card = 1
Tactic:
rw [Finset.card_eq_one]
Proof state after:
α : Type u_1
inst✝ : Fintype α
c : Finset (Finset α)
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c}
a : α
⊢ ∃ a_1, Finset.filter (fun x => a ∈ x) c = {a_1}
Theorem: Partition.card_of_partition'
Proof state before:
α : Type u_1
inst✝ : Fintype α
c : Finset (Finset α)
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c}
a : α
⊢ ∃ a_1, Finset.filter (fun x => a ∈ x) c = {a_1}
Tactic:
obtain ⟨s, hs, hs'⟩ := hc.right a
Proof state after:
case intro.intro
α : Type u_1
inst✝ : Fintype α
c : Finset (Finset α)
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c}
a : α
s : Set α
hs : ∃! x, a ∈ s
hs' : ∀ (y : Set α), (fun b => ∃! x, a ∈ b) y → y = s
⊢ ∃ a_1, Finset.filter (fun x => a ∈ x) c = {a_1}
Theorem: Partition.card_of_partition'
Proof state before:
case intro.intro
α : Type u_1
inst✝ : Fintype α
c : Finset (Finset α)
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c}
a : α
s : Set α
hs : ∃! x, a ∈ s
hs' : ∀ (y : Set α), (fun b => ∃! x, a ∈ b) y → y = s
⊢ ∃ a_1, Finset.filter (fun x => a ∈ x) c = {a_1}
Tactic:
simp only [Set.mem_setOf_eq, exists_unique_iff_exists, exists_eq_left', exists_prop, and_imp] at hs hs'
Proof state after:
case intro.intro
α : Type u_1
inst✝ : Fintype α
c : Finset (Finset α)
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c}
a : α
s : Set α
hs : Set.toFinset s ∈ c ∧ a ∈ s
hs' : ∀ (y : Set α), Set.toFinset y ∈ c → a ∈ y → y = s
⊢ ∃ a_1, Finset.filter (fun x => a ∈ x) c = {a_1}
Theorem: Partition.card_of_partition'
Proof state before:
case intro.intro
α : Type u_1
inst✝ : Fintype α
c : Finset (Finset α)
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c}
a : α
s : Set α
hs : Set.toFinset s ∈ c ∧ a ∈ s
hs' : ∀ (y : Set α), Set.toFinset y ∈ c → a ∈ y → y = s
⊢ ∃ a_1, Finset.filter (fun x => a ∈ x) c = {a_1}
Tactic:
have hs'2 : ∀ z : Finset α, z ∈ c → a ∈ z → z = s.toFinset := by
  intro z hz ha
  rw [← Finset.coe_inj, Set.coe_toFinset]
  refine hs' z ?_ (Finset.mem_coe.mpr ha)
  simp only [Finset.toFinset_coe, hz]
Proof state after:
case intro.intro
α : Type u_1
inst✝ : Fintype α
c : Finset (Finset α)
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c}
a : α
s : Set α
hs : Set.toFinset s ∈ c ∧ a ∈ s
hs' : ∀ (y : Set α), Set.toFinset y ∈ c → a ∈ y → y = s
hs'2 : ∀ z ∈ c, a ∈ z → z = Set.toFinset s
⊢ ∃ a_1, Finset.filter (fun x => a ∈ x) c = {a_1}
Theorem: Partition.card_of_partition'
Proof state before:
case intro.intro
α : Type u_1
inst✝ : Fintype α
c : Finset (Finset α)
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c}
a : α
s : Set α
hs : Set.toFinset s ∈ c ∧ a ∈ s
hs' : ∀ (y : Set α), Set.toFinset y ∈ c → a ∈ y → y = s
hs'2 : ∀ z ∈ c, a ∈ z → z = Set.toFinset s
⊢ ∃ a_1, Finset.filter (fun x => a ∈ x) c = {a_1}
Tactic:
use s.toFinset
Proof state after:
case h
α : Type u_1
inst✝ : Fintype α
c : Finset (Finset α)
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c}
a : α
s : Set α
hs : Set.toFinset s ∈ c ∧ a ∈ s
hs' : ∀ (y : Set α), Set.toFinset y ∈ c → a ∈ y → y = s
hs'2 : ∀ z ∈ c, a ∈ z → z = Set.toFinset s
⊢ Finset.filter (fun x => a ∈ x) c = {Set.toFinset s}
Theorem: Partition.card_of_partition'
Proof state before:
case h
α : Type u_1
inst✝ : Fintype α
c : Finset (Finset α)
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c}
a : α
s : Set α
hs : Set.toFinset s ∈ c ∧ a ∈ s
hs' : ∀ (y : Set α), Set.toFinset y ∈ c → a ∈ y → y = s
hs'2 : ∀ z ∈ c, a ∈ z → z = Set.toFinset s
⊢ Finset.filter (fun x => a ∈ x) c = {Set.toFinset s}
Tactic:
ext t
Proof state after:
case h.a
α : Type u_1
inst✝ : Fintype α
c : Finset (Finset α)
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c}
a : α
s : Set α
hs : Set.toFinset s ∈ c ∧ a ∈ s
hs' : ∀ (y : Set α), Set.toFinset y ∈ c → a ∈ y → y = s
hs'2 : ∀ z ∈ c, a ∈ z → z = Set.toFinset s
t : Finset α
⊢ t ∈ Finset.filter (fun x => a ∈ x) c ↔ t ∈ {Set.toFinset s}
Theorem: Partition.card_of_partition'
Proof state before:
case h.a
α : Type u_1
inst✝ : Fintype α
c : Finset (Finset α)
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c}
a : α
s : Set α
hs : Set.toFinset s ∈ c ∧ a ∈ s
hs' : ∀ (y : Set α), Set.toFinset y ∈ c → a ∈ y → y = s
hs'2 : ∀ z ∈ c, a ∈ z → z = Set.toFinset s
t : Finset α
⊢ t ∈ Finset.filter (fun x => a ∈ x) c ↔ t ∈ {Set.toFinset s}
Tactic:
simp only [Finset.mem_filter, Finset.mem_singleton]
Proof state after:
case h.a
α : Type u_1
inst✝ : Fintype α
c : Finset (Finset α)
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c}
a : α
s : Set α
hs : Set.toFinset s ∈ c ∧ a ∈ s
hs' : ∀ (y : Set α), Set.toFinset y ∈ c → a ∈ y → y = s
hs'2 : ∀ z ∈ c, a ∈ z → z = Set.toFinset s
t : Finset α
⊢ t ∈ c ∧ a ∈ t ↔ t = Set.toFinset s
Theorem: Partition.card_of_partition'
Proof state before:
case h.a
α : Type u_1
inst✝ : Fintype α
c : Finset (Finset α)
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c}
a : α
s : Set α
hs : Set.toFinset s ∈ c ∧ a ∈ s
hs' : ∀ (y : Set α), Set.toFinset y ∈ c → a ∈ y → y = s
hs'2 : ∀ z ∈ c, a ∈ z → z = Set.toFinset s
t : Finset α
⊢ t ∈ c ∧ a ∈ t ↔ t = Set.toFinset s
Tactic:
constructor
Proof state after:
case h.a.mp
α : Type u_1
inst✝ : Fintype α
c : Finset (Finset α)
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c}
a : α
s : Set α
hs : Set.toFinset s ∈ c ∧ a ∈ s
hs' : ∀ (y : Set α), Set.toFinset y ∈ c → a ∈ y → y = s
hs'2 : ∀ z ∈ c, a ∈ z → z = Set.toFinset s
t : Finset α
⊢ t ∈ c ∧ a ∈ t → t = Set.toFinset s

case h.a.mpr
α : Type u_1
inst✝ : Fintype α
c : Finset (Finset α)
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c}
a : α
s : Set α
hs : Set.toFinset s ∈ c ∧ a ∈ s
hs' : ∀ (y : Set α), Set.toFinset y ∈ c → a ∈ y → y = s
hs'2 : ∀ z ∈ c, a ∈ z → z = Set.toFinset s
t : Finset α
⊢ t = Set.toFinset s → t ∈ c ∧ a ∈ t