internlm/Lean-Github huggingface dataset:
Theorem: MulAction.Setoid.nat_sum
Proof 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
Proof 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
Theorem: MulAction.Setoid.nat_sum
Proof 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
Proof 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
Theorem: MulAction.Setoid.nat_sum
Proof 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
Proof 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
Theorem: MulAction.Setoid.nat_sum
Proof 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
Proof 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
Theorem: MulAction.Setoid.nat_sum
Proof 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]
Proof 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
Theorem: MulAction.Setoid.nat_sum
Proof 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]
Proof 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
Theorem: MulAction.Setoid.nat_sum
Proof 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
Proof 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
Theorem: MulAction.Setoid.nat_sum
Proof 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) _ _
Proof 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
Theorem: MulAction.Setoid.nat_sum
Proof 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]
Proof 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
Theorem: MulAction.Setoid.nat_sum
Proof 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⟩
Proof 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
Theorem: MulAction.Setoid.nat_sum
Proof 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]
Proof 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
Theorem: MulAction.Setoid.nat_sum
Proof 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⟩
Proof 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
Theorem: MulAction.Setoid.nat_sum
Proof 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
Proof 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
Theorem: MulAction.Setoid.nat_sum
Proof 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
Proof 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
Theorem: MulAction.Setoid.nat_sum
Proof 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⟩⟩
Proof state after:
no goals
Theorem: MulAction.ncard_block_mul_ncard_orbit_eq
Proof state before:
G : Type u_2
inst✝³ : Group G
X : Type u_1
inst✝² : MulAction G X
inst✝¹ : Finite X
inst✝ : IsPretransitive G X
B : Set X
hB : IsBlock G B
hB_ne : Set.Nonempty B
⊢ Set.ncard B * Set.ncard (Set.range fun g => g • B) = Nat.card X
Tactic:
have := Fintype.ofFinite X
Proof state after:
G : Type u_2
inst✝³ : Group G
X : Type u_1
inst✝² : MulAction G X
inst✝¹ : Finite X
inst✝ : IsPretransitive G X
B : Set X
hB : IsBlock G B
hB_ne : Set.Nonempty B
this : Fintype X
⊢ Set.ncard B * Set.ncard (Set.range fun g => g • B) = Nat.card X
Theorem: MulAction.ncard_block_mul_ncard_orbit_eq
Proof state before:
G : Type u_2
inst✝³ : Group G
X : Type u_1
inst✝² : MulAction G X
inst✝¹ : Finite X
inst✝ : IsPretransitive G X
B : Set X
hB : IsBlock G B
hB_ne : Set.Nonempty B
this : Fintype X
⊢ Set.ncard B * Set.ncard (Set.range fun g => g • B) = Nat.card X
Tactic:
rw [← Setoid.nat_sum (IsBlockSystem.of_block hB hB_ne).1]
Proof state after:
G : Type u_2
inst✝³ : Group G
X : Type u_1
inst✝² : MulAction G X
inst✝¹ : Finite X
inst✝ : IsPretransitive G X
B : Set X
hB : IsBlock G B
hB_ne : Set.Nonempty B
this : Fintype X
⊢ Set.ncard B * Set.ncard (Set.range fun g => g • B) = ∑ᶠ (x : ↑(Set.range fun g => g • B)), Nat.card ↑↑x
Theorem: MulAction.ncard_block_mul_ncard_orbit_eq
Proof state before:
G : Type u_2
inst✝³ : Group G
X : Type u_1
inst✝² : MulAction G X
inst✝¹ : Finite X
inst✝ : IsPretransitive G X
B : Set X
hB : IsBlock G B
hB_ne : Set.Nonempty B
this : Fintype X
⊢ Set.ncard B * Set.ncard (Set.range fun g => g • B) = ∑ᶠ (x : ↑(Set.range fun g => g • B)), Nat.card ↑↑x
Tactic:
simp only [finsum_eq_sum_of_fintype]
Proof state after:
G : Type u_2
inst✝³ : Group G
X : Type u_1
inst✝² : MulAction G X
inst✝¹ : Finite X
inst✝ : IsPretransitive G X
B : Set X
hB : IsBlock G B
hB_ne : Set.Nonempty B
this : Fintype X
⊢ Set.ncard B * Set.ncard (Set.range fun g => g • B) = ∑ x : ↑(Set.range fun g => g • B), Nat.card ↑↑x
Theorem: MulAction.ncard_block_mul_ncard_orbit_eq
Proof state before:
G : Type u_2
inst✝³ : Group G
X : Type u_1
inst✝² : MulAction G X
inst✝¹ : Finite X
inst✝ : IsPretransitive G X
B : Set X
hB : IsBlock G B
hB_ne : Set.Nonempty B
this : Fintype X
⊢ Set.ncard B * Set.ncard (Set.range fun g => g • B) = ∑ x : ↑(Set.range fun g => g • B), Nat.card ↑↑x
Tactic:
simp_rw [Set.Nat.card_coe_set_eq]
Proof state after:
G : Type u_2
inst✝³ : Group G
X : Type u_1
inst✝² : MulAction G X
inst✝¹ : Finite X
inst✝ : IsPretransitive G X
B : Set X
hB : IsBlock G B
hB_ne : Set.Nonempty B
this : Fintype X
⊢ Set.ncard B * Set.ncard (Set.range fun g => g • B) = ∑ x : ↑(Set.range fun g => g • B), Set.ncard ↑x
Theorem: MulAction.ncard_block_mul_ncard_orbit_eq
Proof state before:
G : Type u_2
inst✝³ : Group G
X : Type u_1
inst✝² : MulAction G X
inst✝¹ : Finite X
inst✝ : IsPretransitive G X
B : Set X
hB : IsBlock G B
hB_ne : Set.Nonempty B
this : Fintype X
⊢ Set.ncard B * Set.ncard (Set.range fun g => g • B) = ∑ x : ↑(Set.range fun g => g • B), Set.ncard ↑x
Tactic:
rw [Finset.sum_congr rfl ?_]
Proof state after:
G : Type u_2
inst✝³ : Group G
X : Type u_1
inst✝² : MulAction G X
inst✝¹ : Finite X
inst✝ : IsPretransitive G X
B : Set X
hB : IsBlock G B
hB_ne : Set.Nonempty B
this : Fintype X
⊢ Set.ncard B * Set.ncard (Set.range fun g => g • B) = Finset.sum Finset.univ ?m.191744

G : Type u_2
inst✝³ : Group G
X : Type u_1
inst✝² : MulAction G X
inst✝¹ : Finite X
inst✝ : IsPretransitive G X
B : Set X
hB : IsBlock G B
hB_ne : Set.Nonempty B
this : Fintype X
⊢ ↑(Set.range fun g => g • B) → ℕ

G : Type u_2
inst✝³ : Group G
X : Type u_1
inst✝² : MulAction G X
inst✝¹ : Finite X
inst✝ : IsPretransitive G X
B : Set X
hB : IsBlock G B
hB_ne : Set.Nonempty B
this : Fintype X
⊢ ∀ x ∈ Finset.univ, Set.ncard ↑x = ?m.191744 x
Theorem: MulAction.ncard_block_mul_ncard_orbit_eq
Proof state before:
G : Type u_2
inst✝³ : Group G
X : Type u_1
inst✝² : MulAction G X
inst✝¹ : Finite X
inst✝ : IsPretransitive G X
B : Set X
hB : IsBlock G B
hB_ne : Set.Nonempty B
this : Fintype X
⊢ Set.ncard B * Set.ncard (Set.range fun g => g • B) = Finset.sum Finset.univ ?m.191744

G : Type u_2
inst✝³ : Group G
X : Type u_1
inst✝² : MulAction G X
inst✝¹ : Finite X
inst✝ : IsPretransitive G X
B : Set X
hB : IsBlock G B
hB_ne : Set.Nonempty B
this : Fintype X
⊢ ↑(Set.range fun g => g • B) → ℕ

G : Type u_2
inst✝³ : Group G
X : Type u_1
inst✝² : MulAction G X
inst✝¹ : Finite X
inst✝ : IsPretransitive G X
B : Set X
hB : IsBlock G B
hB_ne : Set.Nonempty B
this : Fintype X
⊢ ∀ x ∈ Finset.univ, Set.ncard ↑x = ?m.191744 x
Tactic:
rw [Finset.sum_const]
Proof state after:
G : Type u_2
inst✝³ : Group G
X : Type u_1
inst✝² : MulAction G X
inst✝¹ : Finite X
inst✝ : IsPretransitive G X
B : Set X
hB : IsBlock G B
hB_ne : Set.Nonempty B
this : Fintype X
⊢ Set.ncard B * Set.ncard (Set.range fun g => g • B) = Finset.univ.card • ?m.191918

G : Type u_2
inst✝³ : Group G
X : Type u_1
inst✝² : MulAction G X
inst✝¹ : Finite X
inst✝ : IsPretransitive G X
B : Set X
hB : IsBlock G B
hB_ne : Set.Nonempty B
this : Fintype X
⊢ ℕ

G : Type u_2
inst✝³ : Group G
X : Type u_1
inst✝² : MulAction G X
inst✝¹ : Finite X
inst✝ : IsPretransitive G X
B : Set X
hB : IsBlock G B
hB_ne : Set.Nonempty B
this : Fintype X
⊢ ∀ x ∈ Finset.univ, Set.ncard ↑x = ?m.191918