Theorem: MulAction.Setoid.nat_sum (Jordan/Blocks.lean)

State before:
G : Type ?u.182986
inst✝² : Group G
X : Type ?u.182992
inst✝¹ : MulAction G X
α : Type u_1
inst✝ : Finite α
c : Set (Set α)
hc : Setoid.IsPartition c
⊢ ∑ᶠ (x : ↑c), Nat.card ↑↑x = Nat.card α
Tactic:
classical
have := Fintype.ofFinite α
simp only [finsum_eq_sum_of_fintype, Nat.card_eq_fintype_card]
rw [← Fintype.card_sigma]
refine' Fintype.card_congr (Equiv.ofBijective (fun x => x.snd : (Σ a : ↥c, a) → α) _)
constructor
rintro ⟨⟨x, hx⟩, ⟨a, ha : a ∈ x⟩⟩ ⟨⟨y, hy⟩, ⟨b, hb : b ∈ y⟩⟩ hab
dsimp at hab
rw [hab] at ha
rw [Sigma.subtype_ext_iff]
simp only [Subtype.mk_eq_mk, Subtype.coe_mk]
apply And.intro _ hab
refine' ExistsUnique.unique (hc.2 b) _ _
simp only [exists_unique_iff_exists, exists_prop]
exact ⟨hx, ha⟩
simp only [exists_unique_iff_exists, exists_prop]
exact ⟨hy, hb⟩
intro a
obtain ⟨x, ⟨hx, ha : a ∈ x, _⟩, _⟩ := hc.2 a
use ⟨⟨x, hx⟩, ⟨a, ha⟩⟩
State after:
no goals

State before:
G : Type ?u.182986
inst✝² : Group G
X : Type ?u.182992
inst✝¹ : MulAction G X
α : Type u_1
inst✝ : Finite α
c : Set (Set α)
hc : Setoid.IsPartition c
⊢ ∑ᶠ (x : ↑c), Nat.card ↑↑x = Nat.card α
Tactic:
have := Fintype.ofFinite α
State after:
G : Type ?u.182986
inst✝² : Group G
X : Type ?u.182992
inst✝¹ : MulAction G X
α : Type u_1
inst✝ : Finite α
c : Set (Set α)
hc : Setoid.IsPartition c
this : Fintype α
⊢ ∑ᶠ (x : ↑c), Nat.card ↑↑x = Nat.card α

State before:
G : Type ?u.182986
inst✝² : Group G
X : Type ?u.182992
inst✝¹ : MulAction G X
α : Type u_1
inst✝ : Finite α
c : Set (Set α)
hc : Setoid.IsPartition c
this : Fintype α
⊢ ∑ᶠ (x : ↑c), Nat.card ↑↑x = Nat.card α
Tactic:
simp only [finsum_eq_sum_of_fintype, Nat.card_eq_fintype_card]
State after:
G : Type ?u.182986
inst✝² : Group G
X : Type ?u.182992
inst✝¹ : MulAction G X
α : Type u_1
inst✝ : Finite α
c : Set (Set α)
hc : Setoid.IsPartition c
this : Fintype α
⊢ ∑ x : ↑c, Fintype.card ↑↑x = Fintype.card α

State before:
G : Type ?u.182986
inst✝² : Group G
X : Type ?u.182992
inst✝¹ : MulAction G X
α : Type u_1
inst✝ : Finite α
c : Set (Set α)
hc : Setoid.IsPartition c
this : Fintype α
⊢ ∑ x : ↑c, Fintype.card ↑↑x = Fintype.card α
Tactic:
rw [← Fintype.card_sigma]
State after:
G : Type ?u.182986
inst✝² : Group G
X : Type ?u.182992
inst✝¹ : MulAction G X
α : Type u_1
inst✝ : Finite α
c : Set (Set α)
hc : Setoid.IsPartition c
this : Fintype α
⊢ Fintype.card ((x : ↑c) × ↑↑x) = Fintype.card α

State before:
G : Type ?u.182986
inst✝² : Group G
X : Type ?u.182992
inst✝¹ : MulAction G X
α : Type u_1
inst✝ : Finite α
c : Set (Set α)
hc : Setoid.IsPartition c
this : Fintype α
⊢ Fintype.card ((x : ↑c) × ↑↑x) = Fintype.card α
Tactic:
refine' Fintype.card_congr (Equiv.ofBijective (fun x => x.snd : (Σ a : ↥c, a) → α) _)
State after:
G : Type ?u.182986
inst✝² : Group G
X : Type ?u.182992
inst✝¹ : MulAction G X
α : Type u_1
inst✝ : Finite α
c : Set (Set α)
hc : Setoid.IsPartition c
this : Fintype α
⊢ Function.Bijective fun x => ↑x.snd

State before:
G : Type ?u.182986
inst✝² : Group G
X : Type ?u.182992
inst✝¹ : MulAction G X
α : Type u_1
inst✝ : Finite α
c : Set (Set α)
hc : Setoid.IsPartition c
this : Fintype α
⊢ Function.Bijective fun x => ↑x.snd
Tactic:
constructor
State after:
case left
G : Type ?u.182986
inst✝² : Group G
X : Type ?u.182992
inst✝¹ : MulAction G X
α : Type u_1
inst✝ : Finite α
c : Set (Set α)
hc : Setoid.IsPartition c
this : Fintype α
⊢ Function.Injective fun x => ↑x.snd

case right
G : Type ?u.182986
inst✝² : Group G
X : Type ?u.182992
inst✝¹ : MulAction G X
α : Type u_1
inst✝ : Finite α
c : Set (Set α)
hc : Setoid.IsPartition c
this : Fintype α
⊢ Function.Surjective fun x => ↑x.snd

State before:
case left
G : Type ?u.182986
inst✝² : Group G
X : Type ?u.182992
inst✝¹ : MulAction G X
α : Type u_1
inst✝ : Finite α
c : Set (Set α)
hc : Setoid.IsPartition c
this : Fintype α
⊢ Function.Injective fun x => ↑x.snd

case right
G : Type ?u.182986
inst✝² : Group G
X : Type ?u.182992
inst✝¹ : MulAction G X
α : Type u_1
inst✝ : Finite α
c : Set (Set α)
hc : Setoid.IsPartition c
this : Fintype α
⊢ Function.Surjective fun x => ↑x.snd
Tactic:
rintro ⟨⟨x, hx⟩, ⟨a, ha : a ∈ x⟩⟩ ⟨⟨y, hy⟩, ⟨b, hb : b ∈ y⟩⟩ hab
State after:
case left.mk.mk.mk.mk.mk.mk
G : Type ?u.182986
inst✝² : Group G
X : Type ?u.182992
inst✝¹ : MulAction G X
α : Type u_1
inst✝ : Finite α
c : Set (Set α)
hc : Setoid.IsPartition c
this : Fintype α
x : Set α
hx : x ∈ c
a : α
ha : a ∈ x
y : Set α
hy : y ∈ c
b : α
hb : b ∈ y
hab :
  (fun x => ↑x.snd) { fst := { val := x, property := hx }, snd := { val := a, property := ha } } =
    (fun x => ↑x.snd) { fst := { val := y, property := hy }, snd := { val := b, property := hb } }
⊢ { fst := { val := x, property := hx }, snd := { val := a, property := ha } } =
    { fst := { val := y, property := hy }, snd := { val := b, property := hb } }

case right
G : Type ?u.182986
inst✝² : Group G
X : Type ?u.182992
inst✝¹ : MulAction G X
α : Type u_1
inst✝ : Finite α
c : Set (Set α)
hc : Setoid.IsPartition c
this : Fintype α
⊢ Function.Surjective fun x => ↑x.snd

State before:
case left.mk.mk.mk.mk.mk.mk
G : Type ?u.182986
inst✝² : Group G
X : Type ?u.182992
inst✝¹ : MulAction G X
α : Type u_1
inst✝ : Finite α
c : Set (Set α)
hc : Setoid.IsPartition c
this : Fintype α
x : Set α
hx : x ∈ c
a : α
ha : a ∈ x
y : Set α
hy : y ∈ c
b : α
hb : b ∈ y
hab :
  (fun x => ↑x.snd) { fst := { val := x, property := hx }, snd := { val := a, property := ha } } =
    (fun x => ↑x.snd) { fst := { val := y, property := hy }, snd := { val := b, property := hb } }
⊢ { fst := { val := x, property := hx }, snd := { val := a, property := ha } } =
    { fst := { val := y, property := hy }, snd := { val := b, property := hb } }

case right
G : Type ?u.182986
inst✝² : Group G
X : Type ?u.182992
inst✝¹ : MulAction G X
α : Type u_1
inst✝ : Finite α
c : Set (Set α)
hc : Setoid.IsPartition c
this : Fintype α
⊢ Function.Surjective fun x => ↑x.snd
Tactic:
dsimp at hab
State after:
case left.mk.mk.mk.mk.mk.mk
G : Type ?u.182986
inst✝² : Group G
X : Type ?u.182992
inst✝¹ : MulAction G X
α : Type u_1
inst✝ : Finite α
c : Set (Set α)
hc : Setoid.IsPartition c
this : Fintype α
x : Set α
hx : x ∈ c
a : α
ha : a ∈ x
y : Set α
hy : y ∈ c
b : α
hb : b ∈ y
hab : a = b
⊢ { fst := { val := x, property := hx }, snd := { val := a, property := ha } } =
    { fst := { val := y, property := hy }, snd := { val := b, property := hb } }

case right
G : Type ?u.182986
inst✝² : Group G
X : Type ?u.182992
inst✝¹ : MulAction G X
α : Type u_1
inst✝ : Finite α
c : Set (Set α)
hc : Setoid.IsPartition c
this : Fintype α
⊢ Function.Surjective fun x => ↑x.snd

State before:
case left.mk.mk.mk.mk.mk.mk
G : Type ?u.182986
inst✝² : Group G
X : Type ?u.182992
inst✝¹ : MulAction G X
α : Type u_1
inst✝ : Finite α
c : Set (Set α)
hc : Setoid.IsPartition c
this : Fintype α
x : Set α
hx : x ∈ c
a : α
ha : a ∈ x
y : Set α
hy : y ∈ c
b : α
hb : b ∈ y
hab : a = b
⊢ { fst := { val := x, property := hx }, snd := { val := a, property := ha } } =
    { fst := { val := y, property := hy }, snd := { val := b, property := hb } }

case right
G : Type ?u.182986
inst✝² : Group G
X : Type ?u.182992
inst✝¹ : MulAction G X
α : Type u_1
inst✝ : Finite α
c : Set (Set α)
hc : Setoid.IsPartition c
this : Fintype α
⊢ Function.Surjective fun x => ↑x.snd
Tactic:
rw [hab] at ha
State after:
case left.mk.mk.mk.mk.mk.mk
G : Type ?u.182986
inst✝² : Group G
X : Type ?u.182992
inst✝¹ : MulAction G X
α : Type u_1
inst✝ : Finite α
c : Set (Set α)
hc : Setoid.IsPartition c
this : Fintype α
x : Set α
hx : x ∈ c
a : α
ha✝ : a ∈ x
y : Set α
hy : y ∈ c
b : α
ha : b ∈ x
hb : b ∈ y
hab : a = b
⊢ { fst := { val := x, property := hx }, snd := { val := a, property := ha✝ } } =
    { fst := { val := y, property := hy }, snd := { val := b, property := hb } }

case right
G : Type ?u.182986
inst✝² : Group G
X : Type ?u.182992
inst✝¹ : MulAction G X
α : Type u_1
inst✝ : Finite α
c : Set (Set α)
hc : Setoid.IsPartition c
this : Fintype α
⊢ Function.Surjective fun x => ↑x.snd

State before:
case left.mk.mk.mk.mk.mk.mk
G : Type ?u.182986
inst✝² : Group G
X : Type ?u.182992
inst✝¹ : MulAction G X
α : Type u_1
inst✝ : Finite α
c : Set (Set α)
hc : Setoid.IsPartition c
this : Fintype α
x : Set α
hx : x ∈ c
a : α
ha✝ : a ∈ x
y : Set α
hy : y ∈ c
b : α
ha : b ∈ x
hb : b ∈ y
hab : a = b
⊢ { fst := { val := x, property := hx }, snd := { val := a, property := ha✝ } } =
    { fst := { val := y, property := hy }, snd := { val := b, property := hb } }

case right
G : Type ?u.182986
inst✝² : Group G
X : Type ?u.182992
inst✝¹ : MulAction G X
α : Type u_1
inst✝ : Finite α
c : Set (Set α)
hc : Setoid.IsPartition c
this : Fintype α
⊢ Function.Surjective fun x => ↑x.snd
Tactic:
rw [Sigma.subtype_ext_iff]
State after:
case left.mk.mk.mk.mk.mk.mk
G : Type ?u.182986
inst✝² : Group G
X : Type ?u.182992
inst✝¹ : MulAction G X
α : Type u_1
inst✝ : Finite α
c : Set (Set α)
hc : Setoid.IsPartition c
this : Fintype α
x : Set α
hx : x ∈ c
a : α
ha✝ : a ∈ x
y : Set α
hy : y ∈ c
b : α
ha : b ∈ x
hb : b ∈ y
hab : a = b
⊢ { fst := { val := x, property := hx }, snd := { val := a, property := ha✝ } }.fst =
      { fst := { val := y, property := hy }, snd := { val := b, property := hb } }.fst ∧
    ↑{ fst := { val := x, property := hx }, snd := { val := a, property := ha✝ } }.snd =
      ↑{ fst := { val := y, property := hy }, snd := { val := b, property := hb } }.snd

case right
G : Type ?u.182986
inst✝² : Group G
X : Type ?u.182992
inst✝¹ : MulAction G X
α : Type u_1
inst✝ : Finite α
c : Set (Set α)
hc : Setoid.IsPartition c
this : Fintype α
⊢ Function.Surjective fun x => ↑x.snd

State before:
case left.mk.mk.mk.mk.mk.mk
G : Type ?u.182986
inst✝² : Group G
X : Type ?u.182992
inst✝¹ : MulAction G X
α : Type u_1
inst✝ : Finite α
c : Set (Set α)
hc : Setoid.IsPartition c
this : Fintype α
x : Set α
hx : x ∈ c
a : α
ha✝ : a ∈ x
y : Set α
hy : y ∈ c
b : α
ha : b ∈ x
hb : b ∈ y
hab : a = b
⊢ { fst := { val := x, property := hx }, snd := { val := a, property := ha✝ } }.fst =
      { fst := { val := y, property := hy }, snd := { val := b, property := hb } }.fst ∧
    ↑{ fst := { val := x, property := hx }, snd := { val := a, property := ha✝ } }.snd =
      ↑{ fst := { val := y, property := hy }, snd := { val := b, property := hb } }.snd

case right
G : Type ?u.182986
inst✝² : Group G
X : Type ?u.182992
inst✝¹ : MulAction G X
α : Type u_1
inst✝ : Finite α
c : Set (Set α)
hc : Setoid.IsPartition c
this : Fintype α
⊢ Function.Surjective fun x => ↑x.snd
Tactic:
simp only [Subtype.mk_eq_mk, Subtype.coe_mk]
State after:
case left.mk.mk.mk.mk.mk.mk
G : Type ?u.182986
inst✝² : Group G
X : Type ?u.182992
inst✝¹ : MulAction G X
α : Type u_1
inst✝ : Finite α
c : Set (Set α)
hc : Setoid.IsPartition c
this : Fintype α
x : Set α
hx : x ∈ c
a : α
ha✝ : a ∈ x
y : Set α
hy : y ∈ c
b : α
ha : b ∈ x
hb : b ∈ y
hab : a = b
⊢ x = y ∧ a = b

case right
G : Type ?u.182986
inst✝² : Group G
X : Type ?u.182992
inst✝¹ : MulAction G X
α : Type u_1
inst✝ : Finite α
c : Set (Set α)
hc : Setoid.IsPartition c
this : Fintype α
⊢ Function.Surjective fun x => ↑x.snd

State before:
case left.mk.mk.mk.mk.mk.mk
G : Type ?u.182986
inst✝² : Group G
X : Type ?u.182992
inst✝¹ : MulAction G X
α : Type u_1
inst✝ : Finite α
c : Set (Set α)
hc : Setoid.IsPartition c
this : Fintype α
x : Set α
hx : x ∈ c
a : α
ha✝ : a ∈ x
y : Set α
hy : y ∈ c
b : α
ha : b ∈ x
hb : b ∈ y
hab : a = b
⊢ x = y ∧ a = b

case right
G : Type ?u.182986
inst✝² : Group G
X : Type ?u.182992
inst✝¹ : MulAction G X
α : Type u_1
inst✝ : Finite α
c : Set (Set α)
hc : Setoid.IsPartition c
this : Fintype α
⊢ Function.Surjective fun x => ↑x.snd
Tactic:
apply And.intro _ hab
State after:
G : Type ?u.182986
inst✝² : Group G
X : Type ?u.182992
inst✝¹ : MulAction G X
α : Type u_1
inst✝ : Finite α
c : Set (Set α)
hc : Setoid.IsPartition c
this : Fintype α
x : Set α
hx : x ∈ c
a : α
ha✝ : a ∈ x
y : Set α
hy : y ∈ c
b : α
ha : b ∈ x
hb : b ∈ y
hab : a = b
⊢ x = y

case right
G : Type ?u.182986
inst✝² : Group G
X : Type ?u.182992
inst✝¹ : MulAction G X
α : Type u_1
inst✝ : Finite α
c : Set (Set α)
hc : Setoid.IsPartition c
this : Fintype α
⊢ Function.Surjective fun x => ↑x.snd

State before:
G : Type ?u.182986
inst✝² : Group G
X : Type ?u.182992
inst✝¹ : MulAction G X
α : Type u_1
inst✝ : Finite α
c : Set (Set α)
hc : Setoid.IsPartition c
this : Fintype α
x : Set α
hx : x ∈ c
a : α
ha✝ : a ∈ x
y : Set α
hy : y ∈ c
b : α
ha : b ∈ x
hb : b ∈ y
hab : a = b
⊢ x = y

case right
G : Type ?u.182986
inst✝² : Group G
X : Type ?u.182992
inst✝¹ : MulAction G X
α : Type u_1
inst✝ : Finite α
c : Set (Set α)
hc : Setoid.IsPartition c
this : Fintype α
⊢ Function.Surjective fun x => ↑x.snd
Tactic:
refine' ExistsUnique.unique (hc.2 b) _ _
State after:
case refine'_1
G : Type ?u.182986
inst✝² : Group G
X : Type ?u.182992
inst✝¹ : MulAction G X
α : Type u_1
inst✝ : Finite α
c : Set (Set α)
hc : Setoid.IsPartition c
this : Fintype α
x : Set α
hx : x ∈ c
a : α
ha✝ : a ∈ x
y : Set α
hy : y ∈ c
b : α
ha : b ∈ x
hb : b ∈ y
hab : a = b
⊢ ∃! x_1, b ∈ x

case refine'_2
G : Type ?u.182986
inst✝² : Group G
X : Type ?u.182992
inst✝¹ : MulAction G X
α : Type u_1
inst✝ : Finite α
c : Set (Set α)
hc : Setoid.IsPartition c
this : Fintype α
x : Set α
hx : x ∈ c
a : α
ha✝ : a ∈ x
y : Set α
hy : y ∈ c
b : α
ha : b ∈ x
hb : b ∈ y
hab : a = b
⊢ ∃! x, b ∈ y

case right
G : Type ?u.182986
inst✝² : Group G
X : Type ?u.182992
inst✝¹ : MulAction G X
α : Type u_1
inst✝ : Finite α
c : Set (Set α)
hc : Setoid.IsPartition c
this : Fintype α
⊢ Function.Surjective fun x => ↑x.snd

State before:
case refine'_1
G : Type ?u.182986
inst✝² : Group G
X : Type ?u.182992
inst✝¹ : MulAction G X
α : Type u_1
inst✝ : Finite α
c : Set (Set α)
hc : Setoid.IsPartition c
this : Fintype α
x : Set α
hx : x ∈ c
a : α
ha✝ : a ∈ x
y : Set α
hy : y ∈ c
b : α
ha : b ∈ x
hb : b ∈ y
hab : a = b
⊢ ∃! x_1, b ∈ x

case refine'_2
G : Type ?u.182986
inst✝² : Group G
X : Type ?u.182992
inst✝¹ : MulAction G X
α : Type u_1
inst✝ : Finite α
c : Set (Set α)
hc : Setoid.IsPartition c
this : Fintype α
x : Set α
hx : x ∈ c
a : α
ha✝ : a ∈ x
y : Set α
hy : y ∈ c
b : α
ha : b ∈ x
hb : b ∈ y
hab : a = b
⊢ ∃! x, b ∈ y

case right
G : Type ?u.182986
inst✝² : Group G
X : Type ?u.182992
inst✝¹ : MulAction G X
α : Type u_1
inst✝ : Finite α
c : Set (Set α)
hc : Setoid.IsPartition c
this : Fintype α
⊢ Function.Surjective fun x => ↑x.snd
Tactic:
simp only [exists_unique_iff_exists, exists_prop]
State after:
case refine'_1
G : Type ?u.182986
inst✝² : Group G
X : Type ?u.182992
inst✝¹ : MulAction G X
α : Type u_1
inst✝ : Finite α
c : Set (Set α)
hc : Setoid.IsPartition c
this : Fintype α
x : Set α
hx : x ∈ c
a : α
ha✝ : a ∈ x
y : Set α
hy : y ∈ c
b : α
ha : b ∈ x
hb : b ∈ y
hab : a = b
⊢ x ∈ c ∧ b ∈ x

case refine'_2
G : Type ?u.182986
inst✝² : Group G
X : Type ?u.182992
inst✝¹ : MulAction G X
α : Type u_1
inst✝ : Finite α
c : Set (Set α)
hc : Setoid.IsPartition c
this : Fintype α
x : Set α
hx : x ∈ c
a : α
ha✝ : a ∈ x
y : Set α
hy : y ∈ c
b : α
ha : b ∈ x
hb : b ∈ y
hab : a = b
⊢ ∃! x, b ∈ y

case right
G : Type ?u.182986
inst✝² : Group G
X : Type ?u.182992
inst✝¹ : MulAction G X
α : Type u_1
inst✝ : Finite α
c : Set (Set α)
hc : Setoid.IsPartition c
this : Fintype α
⊢ Function.Surjective fun x => ↑x.snd

State before:
case refine'_1
G : Type ?u.182986
inst✝² : Group G
X : Type ?u.182992
inst✝¹ : MulAction G X
α : Type u_1
inst✝ : Finite α
c : Set (Set α)
hc : Setoid.IsPartition c
this : Fintype α
x : Set α
hx : x ∈ c
a : α
ha✝ : a ∈ x
y : Set α
hy : y ∈ c
b : α
ha : b ∈ x
hb : b ∈ y
hab : a = b
⊢ x ∈ c ∧ b ∈ x

case refine'_2
G : Type ?u.182986
inst✝² : Group G
X : Type ?u.182992
inst✝¹ : MulAction G X
α : Type u_1
inst✝ : Finite α
c : Set (Set α)
hc : Setoid.IsPartition c
this : Fintype α
x : Set α
hx : x ∈ c
a : α
ha✝ : a ∈ x
y : Set α
hy : y ∈ c
b : α
ha : b ∈ x
hb : b ∈ y
hab : a = b
⊢ ∃! x, b ∈ y

case right
G : Type ?u.182986
inst✝² : Group G
X : Type ?u.182992
inst✝¹ : MulAction G X
α : Type u_1
inst✝ : Finite α
c : Set (Set α)
hc : Setoid.IsPartition c
this : Fintype α
⊢ Function.Surjective fun x => ↑x.snd
Tactic:
exact ⟨hx, ha⟩
State after:
case refine'_2
G : Type ?u.182986
inst✝² : Group G
X : Type ?u.182992
inst✝¹ : MulAction G X
α : Type u_1
inst✝ : Finite α
c : Set (Set α)
hc : Setoid.IsPartition c
this : Fintype α
x : Set α
hx : x ∈ c
a : α
ha✝ : a ∈ x
y : Set α
hy : y ∈ c
b : α
ha : b ∈ x
hb : b ∈ y
hab : a = b
⊢ ∃! x, b ∈ y

case right
G : Type ?u.182986
inst✝² : Group G
X : Type ?u.182992
inst✝¹ : MulAction G X
α : Type u_1
inst✝ : Finite α
c : Set (Set α)
hc : Setoid.IsPartition c
this : Fintype α
⊢ Function.Surjective fun x => ↑x.snd

State before:
case refine'_2
G : Type ?u.182986
inst✝² : Group G
X : Type ?u.182992
inst✝¹ : MulAction G X
α : Type u_1
inst✝ : Finite α
c : Set (Set α)
hc : Setoid.IsPartition c
this : Fintype α
x : Set α
hx : x ∈ c
a : α
ha✝ : a ∈ x
y : Set α
hy : y ∈ c
b : α
ha : b ∈ x
hb : b ∈ y
hab : a = b
⊢ ∃! x, b ∈ y

case right
G : Type ?u.182986
inst✝² : Group G
X : Type ?u.182992
inst✝¹ : MulAction G X
α : Type u_1
inst✝ : Finite α
c : Set (Set α)
hc : Setoid.IsPartition c
this : Fintype α
⊢ Function.Surjective fun x => ↑x.snd
Tactic:
simp only [exists_unique_iff_exists, exists_prop]
State after:
case refine'_2
G : Type ?u.182986
inst✝² : Group G
X : Type ?u.182992
inst✝¹ : MulAction G X
α : Type u_1
inst✝ : Finite α
c : Set (Set α)
hc : Setoid.IsPartition c
this : Fintype α
x : Set α
hx : x ∈ c
a : α
ha✝ : a ∈ x
y : Set α
hy : y ∈ c
b : α
ha : b ∈ x
hb : b ∈ y
hab : a = b
⊢ y ∈ c ∧ b ∈ y

case right
G : Type ?u.182986
inst✝² : Group G
X : Type ?u.182992
inst✝¹ : MulAction G X
α : Type u_1
inst✝ : Finite α
c : Set (Set α)
hc : Setoid.IsPartition c
this : Fintype α
⊢ Function.Surjective fun x => ↑x.snd

State before:
case refine'_2
G : Type ?u.182986
inst✝² : Group G
X : Type ?u.182992
inst✝¹ : MulAction G X
α : Type u_1
inst✝ : Finite α
c : Set (Set α)
hc : Setoid.IsPartition c
this : Fintype α
x : Set α
hx : x ∈ c
a : α
ha✝ : a ∈ x
y : Set α
hy : y ∈ c
b : α
ha : b ∈ x
hb : b ∈ y
hab : a = b
⊢ y ∈ c ∧ b ∈ y

case right
G : Type ?u.182986
inst✝² : Group G
X : Type ?u.182992
inst✝¹ : MulAction G X
α : Type u_1
inst✝ : Finite α
c : Set (Set α)
hc : Setoid.IsPartition c
this : Fintype α
⊢ Function.Surjective fun x => ↑x.snd
Tactic:
exact ⟨hy, hb⟩
State after:
case right
G : Type ?u.182986
inst✝² : Group G
X : Type ?u.182992
inst✝¹ : MulAction G X
α : Type u_1
inst✝ : Finite α
c : Set (Set α)
hc : Setoid.IsPartition c
this : Fintype α
⊢ Function.Surjective fun x => ↑x.snd

State before:
case right
G : Type ?u.182986
inst✝² : Group G
X : Type ?u.182992
inst✝¹ : MulAction G X
α : Type u_1
inst✝ : Finite α
c : Set (Set α)
hc : Setoid.IsPartition c
this : Fintype α
⊢ Function.Surjective fun x => ↑x.snd
Tactic:
intro a
State after:
case right
G : Type ?u.182986
inst✝² : Group G
X : Type ?u.182992
inst✝¹ : MulAction G X
α : Type u_1
inst✝ : Finite α
c : Set (Set α)
hc : Setoid.IsPartition c
this : Fintype α
a : α
⊢ ∃ a_1, (fun x => ↑x.snd) a_1 = a

State before:
case right
G : Type ?u.182986
inst✝² : Group G
X : Type ?u.182992
inst✝¹ : MulAction G X
α : Type u_1
inst✝ : Finite α
c : Set (Set α)
hc : Setoid.IsPartition c
this : Fintype α
a : α
⊢ ∃ a_1, (fun x => ↑x.snd) a_1 = a
Tactic:
obtain ⟨x, ⟨hx, ha : a ∈ x, _⟩, _⟩ := hc.2 a
State after:
case right.intro.intro.intro.intro
G : Type ?u.182986
inst✝² : Group G
X : Type ?u.182992
inst✝¹ : MulAction G X
α : Type u_1
inst✝ : Finite α
c : Set (Set α)
hc : Setoid.IsPartition c
this : Fintype α
a : α
x : Set α
right✝¹ : ∀ (y : Set α), (fun b => ∃! x, a ∈ b) y → y = x
hx : x ∈ c
ha : a ∈ x
right✝ : ∀ (y : x ∈ c), (fun x_1 => a ∈ x) y → y = hx
⊢ ∃ a_1, (fun x => ↑x.snd) a_1 = a

State before:
case right.intro.intro.intro.intro
G : Type ?u.182986
inst✝² : Group G
X : Type ?u.182992
inst✝¹ : MulAction G X
α : Type u_1
inst✝ : Finite α
c : Set (Set α)
hc : Setoid.IsPartition c
this : Fintype α
a : α
x : Set α
right✝¹ : ∀ (y : Set α), (fun b => ∃! x, a ∈ b) y → y = x
hx : x ∈ c
ha : a ∈ x
right✝ : ∀ (y : x ∈ c), (fun x_1 => a ∈ x) y → y = hx
⊢ ∃ a_1, (fun x => ↑x.snd) a_1 = a
Tactic:
use ⟨⟨x, hx⟩, ⟨a, ha⟩⟩
State after:
no goals