internlm/Lean-Github huggingface dataset:
Theorem: Rudio
Proof state before:
case inl
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : Set.Subsingleton (⋂ k, ⋂ (_ : a ∈ k • A), k • A)
g : M
⊢ a ∈ ⋂ (_ : a ∈ g • A), g • A
Tactic:
simp only [Set.mem_iInter, imp_self]
Proof state after:
no goals
Theorem: Rudio
Proof state before:
case inr
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : ⋂ k, ⋂ (_ : a ∈ k • A), k • A = ⊤
⊢ B = {a}
Tactic:
change B = ⊤ at hyp
Proof state after:
case inr
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : B = ⊤
⊢ B = {a}
Theorem: Rudio
Proof state before:
case inr
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : B = ⊤
⊢ B = {a}
Tactic:
exfalso
Proof state after:
case inr
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : B = ⊤
⊢ False
Theorem: Rudio
Proof state before:
case inr
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : B = ⊤
⊢ False
Tactic:
apply hA'
Proof state after:
case inr
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : B = ⊤
⊢ A = ⊤
Theorem: Rudio
Proof state before:
case inr
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : B = ⊤
⊢ A = ⊤
Tactic:
suffices ∃ g : M, a ∈ g • A by
  obtain ⟨g, hg⟩ := this
  have : B ≤ g • A := Set.biInter_subset_of_mem hg
  rw [hyp, top_le_iff, ← eq_inv_smul_iff] at this
  rw [this, Set.top_eq_univ, Set.smul_set_univ]
Proof state after:
case inr
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : B = ⊤
⊢ ∃ g, a ∈ g • A
Theorem: Rudio
Proof state before:
case inr
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : B = ⊤
⊢ ∃ g, a ∈ g • A
Tactic:
obtain ⟨x, hx⟩ := hA
Proof state after:
case inr.intro
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : B = ⊤
x : α
hx : x ∈ A
⊢ ∃ g, a ∈ g • A
Theorem: Rudio
Proof state before:
case inr.intro
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : B = ⊤
x : α
hx : x ∈ A
⊢ ∃ g, a ∈ g • A
Tactic:
obtain ⟨g, hg⟩ := MulAction.exists_smul_eq M x a
Proof state after:
case inr.intro.intro
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : B = ⊤
x : α
hx : x ∈ A
g : M
hg : g • x = a
⊢ ∃ g, a ∈ g • A
Theorem: Rudio
Proof state before:
case inr.intro.intro
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : B = ⊤
x : α
hx : x ∈ A
g : M
hg : g • x = a
⊢ ∃ g, a ∈ g • A
Tactic:
use g
Proof state after:
case h
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : B = ⊤
x : α
hx : x ∈ A
g : M
hg : g • x = a
⊢ a ∈ g • A
Theorem: Rudio
Proof state before:
case h
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : B = ⊤
x : α
hx : x ∈ A
g : M
hg : g • x = a
⊢ a ∈ g • A
Tactic:
use x
Proof state after:
no goals
Theorem: Rudio
Proof state before:
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : B = ⊤
this : ∃ g, a ∈ g • A
⊢ A = ⊤
Tactic:
obtain ⟨g, hg⟩ := this
Proof state after:
case intro
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : B = ⊤
g : M
hg : a ∈ g • A
⊢ A = ⊤
Theorem: Rudio
Proof state before:
case intro
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : B = ⊤
g : M
hg : a ∈ g • A
⊢ A = ⊤
Tactic:
have : B ≤ g • A := Set.biInter_subset_of_mem hg
Proof state after:
case intro
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : B = ⊤
g : M
hg : a ∈ g • A
this : B ≤ g • A
⊢ A = ⊤
Theorem: Rudio
Proof state before:
case intro
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : B = ⊤
g : M
hg : a ∈ g • A
this : B ≤ g • A
⊢ A = ⊤
Tactic:
rw [hyp, top_le_iff, ← eq_inv_smul_iff] at this
Proof state after:
case intro
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : B = ⊤
g : M
hg : a ∈ g • A
this : A = g⁻¹ • ⊤
⊢ A = ⊤
Theorem: Rudio
Proof state before:
case intro
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : B = ⊤
g : M
hg : a ∈ g • A
this : A = g⁻¹ • ⊤
⊢ A = ⊤
Tactic:
rw [this, Set.top_eq_univ, Set.smul_set_univ]
Proof state after:
no goals
Theorem: Nat.add_lt_of_le_lt
Proof state before:
a b c d : ℕ
hab : a ≤ c
hbd : b < d
⊢ a + b < c + d
Tactic:
apply Nat.lt_of_lt_of_le
Proof state after:
case a
a b c d : ℕ
hab : a ≤ c
hbd : b < d
⊢ a + b < ?m

case a
a b c d : ℕ
hab : a ≤ c
hbd : b < d
⊢ ?m ≤ c + d

case m
a b c d : ℕ
hab : a ≤ c
hbd : b < d
⊢ ℕ
Theorem: Nat.add_lt_of_le_lt
Proof state before:
case a
a b c d : ℕ
hab : a ≤ c
hbd : b < d
⊢ a + b < ?m

case a
a b c d : ℕ
hab : a ≤ c
hbd : b < d
⊢ ?m ≤ c + d

case m
a b c d : ℕ
hab : a ≤ c
hbd : b < d
⊢ ℕ
Tactic:
apply Nat.add_lt_add_left _ a
Proof state after:
a b c d : ℕ
hab : a ≤ c
hbd : b < d
⊢ ℕ

a b c d : ℕ
hab : a ≤ c
hbd : b < d
⊢ b < ?m.126

case a
a b c d : ℕ
hab : a ≤ c
hbd : b < d
⊢ a + ?m.126 ≤ c + d
Theorem: Nat.add_lt_of_le_lt
Proof state before:
a b c d : ℕ
hab : a ≤ c
hbd : b < d
⊢ ℕ

a b c d : ℕ
hab : a ≤ c
hbd : b < d
⊢ b < ?m.126

case a
a b c d : ℕ
hab : a ≤ c
hbd : b < d
⊢ a + ?m.126 ≤ c + d
Tactic:
use d
Proof state after:
a b c d : ℕ
hab : a ≤ c
hbd : b < d
⊢ b < d

case a
a b c d : ℕ
hab : a ≤ c
hbd : b < d
⊢ a + d ≤ c + d
Theorem: Nat.add_lt_of_le_lt
Proof state before:
a b c d : ℕ
hab : a ≤ c
hbd : b < d
⊢ b < d

case a
a b c d : ℕ
hab : a ≤ c
hbd : b < d
⊢ a + d ≤ c + d
Tactic:
exact hbd
Proof state after:
case a
a b c d : ℕ
hab : a ≤ c
hbd : b < d
⊢ a + d ≤ c + d
Theorem: Nat.add_lt_of_le_lt
Proof state before:
case a
a b c d : ℕ
hab : a ≤ c
hbd : b < d
⊢ a + d ≤ c + d
Tactic:
apply Nat.add_le_add_right hab d
Proof state after:
no goals
Theorem: subgroup_of_group_of_order_two
Proof state before:
case inl
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
hG : Fintype.card G = 2
H : Subgroup G
h : Fintype.card ↥H ≤ 1
⊢ H = ⊥ ∨ H = ⊤
Tactic:
apply Or.intro_left
Proof state after:
case inl.h
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
hG : Fintype.card G = 2
H : Subgroup G
h : Fintype.card ↥H ≤ 1
⊢ H = ⊥
Theorem: subgroup_of_group_of_order_two
Proof state before:
case inl.h
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
hG : Fintype.card G = 2
H : Subgroup G
h : Fintype.card ↥H ≤ 1
⊢ H = ⊥
Tactic:
apply Subgroup.eq_bot_of_card_le
Proof state after:
case inl.h.h
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
hG : Fintype.card G = 2
H : Subgroup G
h : Fintype.card ↥H ≤ 1
⊢ Fintype.card ↥H ≤ 1
Theorem: subgroup_of_group_of_order_two
Proof state before:
case inl.h.h
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
hG : Fintype.card G = 2
H : Subgroup G
h : Fintype.card ↥H ≤ 1
⊢ Fintype.card ↥H ≤ 1
Tactic:
exact h
Proof state after:
no goals
Theorem: subgroup_of_group_of_order_two
Proof state before:
case inr
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
hG : Fintype.card G = 2
H : Subgroup G
h : 1 < Fintype.card ↥H
⊢ H = ⊥ ∨ H = ⊤
Tactic:
apply Or.intro_right
Proof state after:
case inr.h
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
hG : Fintype.card G = 2
H : Subgroup G
h : 1 < Fintype.card ↥H
⊢ H = ⊤
Theorem: subgroup_of_group_of_order_two
Proof state before:
case inr.h
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
hG : Fintype.card G = 2
H : Subgroup G
h : 1 < Fintype.card ↥H
⊢ H = ⊤
Tactic:
apply Subgroup.eq_top_of_card_eq
Proof state after:
case inr.h.h
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
hG : Fintype.card G = 2
H : Subgroup G
h : 1 < Fintype.card ↥H
⊢ Fintype.card ↥H = Fintype.card G
Theorem: subgroup_of_group_of_order_two
Proof state before:
case inr.h.h
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
hG : Fintype.card G = 2
H : Subgroup G
h : 1 < Fintype.card ↥H
⊢ Fintype.card ↥H = Fintype.card G
Tactic:
apply le_antisymm
Proof state after:
case inr.h.h.a
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
hG : Fintype.card G = 2
H : Subgroup G
h : 1 < Fintype.card ↥H
⊢ Fintype.card ↥H ≤ Fintype.card G

case inr.h.h.a
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
hG : Fintype.card G = 2
H : Subgroup G
h : 1 < Fintype.card ↥H
⊢ Fintype.card G ≤ Fintype.card ↥H
Theorem: subgroup_of_group_of_order_two
Proof state before:
case inr.h.h.a
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
hG : Fintype.card G = 2
H : Subgroup G
h : 1 < Fintype.card ↥H
⊢ Fintype.card ↥H ≤ Fintype.card G
Tactic:
apply Nat.le_of_dvd
Proof state after:
case inr.h.h.a.h
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
hG : Fintype.card G = 2
H : Subgroup G
h : 1 < Fintype.card ↥H
⊢ 0 < Fintype.card G

case inr.h.h.a.a
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
hG : Fintype.card G = 2
H : Subgroup G
h : 1 < Fintype.card ↥H
⊢ Fintype.card ↥H ∣ Fintype.card G
Theorem: subgroup_of_group_of_order_two
Proof state before:
case inr.h.h.a.h
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
hG : Fintype.card G = 2
H : Subgroup G
h : 1 < Fintype.card ↥H
⊢ 0 < Fintype.card G

case inr.h.h.a.a
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
hG : Fintype.card G = 2
H : Subgroup G
h : 1 < Fintype.card ↥H
⊢ Fintype.card ↥H ∣ Fintype.card G
Tactic:
refine' Fintype.card_pos
Proof state after:
case inr.h.h.a.a
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
hG : Fintype.card G = 2
H : Subgroup G
h : 1 < Fintype.card ↥H
⊢ Fintype.card ↥H ∣ Fintype.card G
Theorem: subgroup_of_group_of_order_two
Proof state before:
case inr.h.h.a.a
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
hG : Fintype.card G = 2
H : Subgroup G
h : 1 < Fintype.card ↥H
⊢ Fintype.card ↥H ∣ Fintype.card G
Tactic:
refine' Subgroup.card_subgroup_dvd_card H
Proof state after:
no goals
Theorem: subgroup_of_group_of_order_two
Proof state before:
case inr.h.h.a
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
hG : Fintype.card G = 2
H : Subgroup G
h : 1 < Fintype.card ↥H
⊢ Fintype.card G ≤ Fintype.card ↥H
Tactic:
rw [hG]
Proof state after:
case inr.h.h.a
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
hG : Fintype.card G = 2
H : Subgroup G
h : 1 < Fintype.card ↥H
⊢ 2 ≤ Fintype.card ↥H
Theorem: subgroup_of_group_of_order_two
Proof state before:
case inr.h.h.a
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
hG : Fintype.card G = 2
H : Subgroup G
h : 1 < Fintype.card ↥H
⊢ 2 ≤ Fintype.card ↥H
Tactic:
exact h
Proof state after:
no goals
Theorem: Equiv.Perm.IsPretransitive.of_partition
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
⊢ (∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b) → (∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b) → stabilizer G s ≠ ⊤ → IsPretransitive G α
Tactic:
intro hs hs' hG
Proof state after:
α : Type u_1
inst✝² : DecidableEq α
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hG : stabilizer G s ≠ ⊤
⊢ IsPretransitive G α
Theorem: Equiv.Perm.IsPretransitive.of_partition
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hG : stabilizer G s ≠ ⊤
⊢ ∃ a b g, a ∈ s ∧ b ∈ sᶜ ∧ g • a = b
Tactic:
by_contra hyp
Proof state after:
α : Type u_1
inst✝² : DecidableEq α
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hG : stabilizer G s ≠ ⊤
hyp : ¬∃ a b g, a ∈ s ∧ b ∈ sᶜ ∧ g • a = b
⊢ False
Theorem: Equiv.Perm.IsPretransitive.of_partition
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hG : stabilizer G s ≠ ⊤
hyp : ¬∃ a b g, a ∈ s ∧ b ∈ sᶜ ∧ g • a = b
⊢ False
Tactic:
push_neg at hyp
Proof state after:
α : Type u_1
inst✝² : DecidableEq α
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hG : stabilizer G s ≠ ⊤
hyp : ∀ (a b : α) (g : G), a ∈ s → b ∈ sᶜ → g • a ≠ b
⊢ False
Theorem: Equiv.Perm.IsPretransitive.of_partition
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hG : stabilizer G s ≠ ⊤
hyp : ∀ (a b : α) (g : G), a ∈ s → b ∈ sᶜ → g • a ≠ b
⊢ False
Tactic:
apply hG
Proof state after:
α : Type u_1
inst✝² : DecidableEq α
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hG : stabilizer G s ≠ ⊤
hyp : ∀ (a b : α) (g : G), a ∈ s → b ∈ sᶜ → g • a ≠ b
⊢ stabilizer G s = ⊤
Theorem: Equiv.Perm.IsPretransitive.of_partition
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hG : stabilizer G s ≠ ⊤
hyp : ∀ (a b : α) (g : G), a ∈ s → b ∈ sᶜ → g • a ≠ b
⊢ stabilizer G s = ⊤
Tactic:
rw [eq_top_iff, MulAction.le_stabilizer_iff_smul_le]
Proof state after:
α : Type u_1
inst✝² : DecidableEq α
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hG : stabilizer G s ≠ ⊤
hyp : ∀ (a b : α) (g : G), a ∈ s → b ∈ sᶜ → g • a ≠ b
⊢ ∀ g ∈ ⊤, g • s ⊆ s
Theorem: Equiv.Perm.IsPretransitive.of_partition
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hG : stabilizer G s ≠ ⊤
hyp : ∀ (a b : α) (g : G), a ∈ s → b ∈ sᶜ → g • a ≠ b
⊢ ∀ g ∈ ⊤, g • s ⊆ s
Tactic:
intro g _
Proof state after:
α : Type u_1
inst✝² : DecidableEq α
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hG : stabilizer G s ≠ ⊤
hyp : ∀ (a b : α) (g : G), a ∈ s → b ∈ sᶜ → g • a ≠ b
g : G
a✝ : g ∈ ⊤
⊢ g • s ⊆ s
Theorem: Equiv.Perm.IsPretransitive.of_partition
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hG : stabilizer G s ≠ ⊤
hyp : ∀ (a b : α) (g : G), a ∈ s → b ∈ sᶜ → g • a ≠ b
g : G
a✝ : g ∈ ⊤
⊢ g • s ⊆ s
Tactic:
rintro b ⟨a, ha, hgab⟩
Proof state after:
case intro.intro
α : Type u_1
inst✝² : DecidableEq α
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hG : stabilizer G s ≠ ⊤
hyp : ∀ (a b : α) (g : G), a ∈ s → b ∈ sᶜ → g • a ≠ b
g : G
a✝ : g ∈ ⊤
b a : α
ha : a ∈ s
hgab : (fun x => g • x) a = b
⊢ b ∈ s
Theorem: Equiv.Perm.IsPretransitive.of_partition
Proof state before:
case intro.intro
α : Type u_1
inst✝² : DecidableEq α
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hG : stabilizer G s ≠ ⊤
hyp : ∀ (a b : α) (g : G), a ∈ s → b ∈ sᶜ → g • a ≠ b
g : G
a✝ : g ∈ ⊤
b a : α
ha : a ∈ s
hgab : (fun x => g • x) a = b
⊢ b ∈ s
Tactic:
by_contra hb
Proof state after:
case intro.intro
α : Type u_1
inst✝² : DecidableEq α
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hG : stabilizer G s ≠ ⊤
hyp : ∀ (a b : α) (g : G), a ∈ s → b ∈ sᶜ → g • a ≠ b
g : G
a✝ : g ∈ ⊤
b a : α
ha : a ∈ s
hgab : (fun x => g • x) a = b
hb : b ∉ s
⊢ False
Theorem: Equiv.Perm.IsPretransitive.of_partition
Proof state before:
case intro.intro
α : Type u_1
inst✝² : DecidableEq α
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hG : stabilizer G s ≠ ⊤
hyp : ∀ (a b : α) (g : G), a ∈ s → b ∈ sᶜ → g • a ≠ b
g : G
a✝ : g ∈ ⊤
b a : α
ha : a ∈ s
hgab : (fun x => g • x) a = b
hb : b ∉ s
⊢ False
Tactic:
exact hyp a b g ha (Set.mem_compl hb) hgab
Proof state after:
no goals
Theorem: Equiv.Perm.IsPretransitive.of_partition
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hG : stabilizer G s ≠ ⊤
hss' : ∃ a b g, a ∈ s ∧ b ∈ sᶜ ∧ g • a = b
⊢ IsPretransitive G α
Tactic:
obtain ⟨a, b, g, ha, hb, hgab⟩ := hss'
Proof state after:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hG : stabilizer G s ≠ ⊤
a b : α
g : G
ha : a ∈ s
hb : b ∈ sᶜ
hgab : g • a = b
⊢ IsPretransitive G α
Theorem: Equiv.Perm.IsPretransitive.of_partition
Proof state before:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hG : stabilizer G s ≠ ⊤
a b : α
g : G
ha : a ∈ s
hb : b ∈ sᶜ
hgab : g • a = b
⊢ IsPretransitive G α
Tactic:
apply IsPretransitive.mk_base a
Proof state after:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hG : stabilizer G s ≠ ⊤
a b : α
g : G
ha : a ∈ s
hb : b ∈ sᶜ
hgab : g • a = b
⊢ ∀ (x : α), ∃ g, g • a = x
Theorem: Equiv.Perm.IsPretransitive.of_partition
Proof state before:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hG : stabilizer G s ≠ ⊤
a b : α
g : G
ha : a ∈ s
hb : b ∈ sᶜ
hgab : g • a = b
⊢ ∀ (x : α), ∃ g, g • a = x
Tactic:
intro x
Proof state after:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hG : stabilizer G s ≠ ⊤
a b : α
g : G
ha : a ∈ s
hb : b ∈ sᶜ
hgab : g • a = b
x : α
⊢ ∃ g, g • a = x
Theorem: Equiv.Perm.IsPretransitive.of_partition
Proof state before:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hG : stabilizer G s ≠ ⊤
a b : α
g : G
ha : a ∈ s
hb : b ∈ sᶜ
hgab : g • a = b
x : α
⊢ ∃ g, g • a = x
Tactic:
by_cases hx : x ∈ s
Proof state after:
case pos
α : Type u_1
inst✝² : DecidableEq α
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hG : stabilizer G s ≠ ⊤
a b : α
g : G
ha : a ∈ s
hb : b ∈ sᶜ
hgab : g • a = b
x : α
hx : x ∈ s
⊢ ∃ g, g • a = x

case neg
α : Type u_1
inst✝² : DecidableEq α
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hG : stabilizer G s ≠ ⊤
a b : α
g : G
ha : a ∈ s
hb : b ∈ sᶜ
hgab : g • a = b
x : α
hx : x ∉ s
⊢ ∃ g, g • a = x