internlm/Lean-Github huggingface dataset:
Theorem: MulAction.IsMultiplyPretransitive.isPreprimitive_of_two
Proof state before:
case neg.intro.intro
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : ∀ {g : M} {b : α}, b ∈ B → b ∈ g • B → g • B ≤ B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
c : α
a✝ : c ∈ ⊤
h' : ¬a = c
g : M
hga : g • a = a
hgb : g • b = c
⊢ c ∈ B
Tactic:
apply hB ha
Proof state after:
case neg.intro.intro.x
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : ∀ {g : M} {b : α}, b ∈ B → b ∈ g • B → g • B ≤ B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
c : α
a✝ : c ∈ ⊤
h' : ¬a = c
g : M
hga : g • a = a
hgb : g • b = c
⊢ a ∈ ?m.235992 • B

case neg.intro.intro.a
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : ∀ {g : M} {b : α}, b ∈ B → b ∈ g • B → g • B ≤ B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
c : α
a✝ : c ∈ ⊤
h' : ¬a = c
g : M
hga : g • a = a
hgb : g • b = c
⊢ c ∈ ?m.235992 • B

M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : ∀ {g : M} {b : α}, b ∈ B → b ∈ g • B → g • B ≤ B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
c : α
a✝ : c ∈ ⊤
h' : ¬a = c
g : M
hga : g • a = a
hgb : g • b = c
⊢ M
Theorem: MulAction.IsMultiplyPretransitive.isPreprimitive_of_two
Proof state before:
case neg.intro.intro.x
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : ∀ {g : M} {b : α}, b ∈ B → b ∈ g • B → g • B ≤ B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
c : α
a✝ : c ∈ ⊤
h' : ¬a = c
g : M
hga : g • a = a
hgb : g • b = c
⊢ a ∈ ?m.235992 • B
Tactic:
rw [← hga]
Proof state after:
case neg.intro.intro.x
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : ∀ {g : M} {b : α}, b ∈ B → b ∈ g • B → g • B ≤ B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
c : α
a✝ : c ∈ ⊤
h' : ¬a = c
g : M
hga : g • a = a
hgb : g • b = c
⊢ g • a ∈ ?m.235992 • B

M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : ∀ {g : M} {b : α}, b ∈ B → b ∈ g • B → g • B ≤ B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
c : α
a✝ : c ∈ ⊤
h' : ¬a = c
g : M
hga : g • a = a
hgb : g • b = c
⊢ M
Theorem: MulAction.IsMultiplyPretransitive.isPreprimitive_of_two
Proof state before:
case neg.intro.intro.x
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : ∀ {g : M} {b : α}, b ∈ B → b ∈ g • B → g • B ≤ B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
c : α
a✝ : c ∈ ⊤
h' : ¬a = c
g : M
hga : g • a = a
hgb : g • b = c
⊢ g • a ∈ ?m.235992 • B

M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : ∀ {g : M} {b : α}, b ∈ B → b ∈ g • B → g • B ≤ B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
c : α
a✝ : c ∈ ⊤
h' : ¬a = c
g : M
hga : g • a = a
hgb : g • b = c
⊢ M
Tactic:
exact Set.smul_mem_smul_set ha
Proof state after:
no goals
Theorem: MulAction.IsMultiplyPretransitive.isPreprimitive_of_two
Proof state before:
case neg.intro.intro.a
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : ∀ {g : M} {b : α}, b ∈ B → b ∈ g • B → g • B ≤ B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
c : α
a✝ : c ∈ ⊤
h' : ¬a = c
g : M
hga : g • a = a
hgb : g • b = c
⊢ c ∈ g • B
Tactic:
rw [← hgb]
Proof state after:
case neg.intro.intro.a
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : ∀ {g : M} {b : α}, b ∈ B → b ∈ g • B → g • B ≤ B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
c : α
a✝ : c ∈ ⊤
h' : ¬a = c
g : M
hga : g • a = a
hgb : g • b = c
⊢ g • b ∈ g • B
Theorem: MulAction.IsMultiplyPretransitive.isPreprimitive_of_two
Proof state before:
case neg.intro.intro.a
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : ∀ {g : M} {b : α}, b ∈ B → b ∈ g • B → g • B ≤ B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
c : α
a✝ : c ∈ ⊤
h' : ¬a = c
g : M
hga : g • a = a
hgb : g • b = c
⊢ g • b ∈ g • B
Tactic:
exact Set.smul_mem_smul_set hb
Proof state after:
no goals
Theorem: Equiv.Perm.isPretransitive
Proof state before:
M : Type ?u.237454
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : DecidableEq α
⊢ IsPretransitive (Equiv.Perm α) α
Tactic:
apply IsPretransitive.mk
Proof state after:
case exists_smul_eq
M : Type ?u.237454
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : DecidableEq α
⊢ ∀ (x y : α), ∃ g, g • x = y
Theorem: Equiv.Perm.isPretransitive
Proof state before:
case exists_smul_eq
M : Type ?u.237454
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : DecidableEq α
⊢ ∀ (x y : α), ∃ g, g • x = y
Tactic:
intro x y
Proof state after:
case exists_smul_eq
M : Type ?u.237454
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : DecidableEq α
x y : α
⊢ ∃ g, g • x = y
Theorem: Equiv.Perm.isPretransitive
Proof state before:
case exists_smul_eq
M : Type ?u.237454
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : DecidableEq α
x y : α
⊢ ∃ g, g • x = y
Tactic:
use Equiv.swap x y
Proof state after:
case h
M : Type ?u.237454
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : DecidableEq α
x y : α
⊢ Equiv.swap x y • x = y
Theorem: Equiv.Perm.isPretransitive
Proof state before:
case h
M : Type ?u.237454
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : DecidableEq α
x y : α
⊢ Equiv.swap x y • x = y
Tactic:
simp only [Equiv.Perm.smul_def]
Proof state after:
case h
M : Type ?u.237454
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : DecidableEq α
x y : α
⊢ (Equiv.swap x y) x = y
Theorem: Equiv.Perm.isPretransitive
Proof state before:
case h
M : Type ?u.237454
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : DecidableEq α
x y : α
⊢ (Equiv.swap x y) x = y
Tactic:
rw [Equiv.swap_apply_left x y]
Proof state after:
no goals
Theorem: Equiv.Perm.isMultiplyPretransitive
Proof state before:
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
⊢ IsMultiplyPretransitive (Equiv.Perm α) α n
Tactic:
cases' le_or_gt n (Fintype.card α) with hn hn
Proof state after:
case inl
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
⊢ IsMultiplyPretransitive (Equiv.Perm α) α n

case inr
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n > Fintype.card α
⊢ IsMultiplyPretransitive (Equiv.Perm α) α n
Theorem: Equiv.Perm.isMultiplyPretransitive
Proof state before:
case inr
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n > Fintype.card α
⊢ IsMultiplyPretransitive (Equiv.Perm α) α n
Tactic:
suffices IsEmpty (Fin n ↪ α) by
  apply IsPretransitive.mk
  intro x
  exfalso
  exact this.false  x
Proof state after:
case inr
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n > Fintype.card α
⊢ IsEmpty (Fin n ↪ α)
Theorem: Equiv.Perm.isMultiplyPretransitive
Proof state before:
case inr
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n > Fintype.card α
⊢ IsEmpty (Fin n ↪ α)
Tactic:
apply Function.Embedding.isEmpty_of_card_lt
Proof state after:
case inr.h
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n > Fintype.card α
⊢ Fintype.card α < Fintype.card (Fin n)
Theorem: Equiv.Perm.isMultiplyPretransitive
Proof state before:
case inr.h
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n > Fintype.card α
⊢ Fintype.card α < Fintype.card (Fin n)
Tactic:
simp only [Fintype.card_fin]
Proof state after:
case inr.h
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n > Fintype.card α
⊢ Fintype.card α < n
Theorem: Equiv.Perm.isMultiplyPretransitive
Proof state before:
case inr.h
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n > Fintype.card α
⊢ Fintype.card α < n
Tactic:
exact hn
Proof state after:
no goals
Theorem: Equiv.Perm.isMultiplyPretransitive
Proof state before:
case inl
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
⊢ IsMultiplyPretransitive (Equiv.Perm α) α n
Tactic:
apply isMultiplyPretransitive_of_higher (Equiv.Perm α) α _ hn
Proof state after:
case inl
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
⊢ ↑(Fintype.card α) ≤ PartENat.card α

M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
⊢ IsMultiplyPretransitive (Equiv.Perm α) α (Fintype.card α)
Theorem: Equiv.Perm.isMultiplyPretransitive
Proof state before:
case inl
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
⊢ ↑(Fintype.card α) ≤ PartENat.card α

M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
⊢ IsMultiplyPretransitive (Equiv.Perm α) α (Fintype.card α)
Tactic:
apply le_of_eq
Proof state after:
case inl.a
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
⊢ ↑(Fintype.card α) = PartENat.card α

M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
⊢ IsMultiplyPretransitive (Equiv.Perm α) α (Fintype.card α)
Theorem: Equiv.Perm.isMultiplyPretransitive
Proof state before:
case inl.a
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
⊢ ↑(Fintype.card α) = PartENat.card α

M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
⊢ IsMultiplyPretransitive (Equiv.Perm α) α (Fintype.card α)
Tactic:
rw [PartENat.card_eq_coe_fintype_card]
Proof state after:
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
⊢ IsMultiplyPretransitive (Equiv.Perm α) α (Fintype.card α)
Theorem: Equiv.Perm.isMultiplyPretransitive
Proof state before:
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
⊢ IsMultiplyPretransitive (Equiv.Perm α) α (Fintype.card α)
Tactic:
apply IsPretransitive.mk
Proof state after:
case exists_smul_eq
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
⊢ ∀ (x y : Fin (Fintype.card α) ↪ α), ∃ g, g • x = y
Theorem: Equiv.Perm.isMultiplyPretransitive
Proof state before:
case exists_smul_eq
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
⊢ ∀ (x y : Fin (Fintype.card α) ↪ α), ∃ g, g • x = y
Tactic:
intro x y
Proof state after:
case exists_smul_eq
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
x y : Fin (Fintype.card α) ↪ α
⊢ ∃ g, g • x = y
Theorem: Equiv.Perm.isMultiplyPretransitive
Proof state before:
case exists_smul_eq
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
x y : Fin (Fintype.card α) ↪ α
⊢ ∃ g, g • x = y
Tactic:
suffices h : Function.Bijective x ∧ Function.Bijective y by
  let x' := Equiv.ofBijective x h.1
  let y' := Equiv.ofBijective y h.2
  use x'.symm.trans y'
  ext i
  simp only [smul_apply, Equiv.Perm.smul_def, Equiv.trans_apply, x', y']
  simp only [Equiv.ofBijective_symm_apply_apply, Equiv.ofBijective_apply]
Proof state after:
case exists_smul_eq
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
x y : Fin (Fintype.card α) ↪ α
⊢ Function.Bijective ⇑x ∧ Function.Bijective ⇑y
Theorem: Equiv.Perm.isMultiplyPretransitive
Proof state before:
case exists_smul_eq
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
x y : Fin (Fintype.card α) ↪ α
⊢ Function.Bijective ⇑x ∧ Function.Bijective ⇑y
Tactic:
constructor
Proof state after:
case exists_smul_eq.left
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
x y : Fin (Fintype.card α) ↪ α
⊢ Function.Bijective ⇑x

case exists_smul_eq.right
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
x y : Fin (Fintype.card α) ↪ α
⊢ Function.Bijective ⇑y
Theorem: Equiv.Perm.isMultiplyPretransitive
Proof state before:
case exists_smul_eq.left
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
x y : Fin (Fintype.card α) ↪ α
⊢ Function.Bijective ⇑x

case exists_smul_eq.right
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
x y : Fin (Fintype.card α) ↪ α
⊢ Function.Bijective ⇑y
Tactic:
all_goals
  rw [Fintype.bijective_iff_injective_and_card]
  constructor
  apply EmbeddingLike.injective
  exact Fintype.card_fin (Fintype.card α)
Proof state after:
no goals
Theorem: Equiv.Perm.isMultiplyPretransitive
Proof state before:
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
x y : Fin (Fintype.card α) ↪ α
h : Function.Bijective ⇑x ∧ Function.Bijective ⇑y
⊢ ∃ g, g • x = y
Tactic:
let x' := Equiv.ofBijective x h.1
Proof state after:
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
x y : Fin (Fintype.card α) ↪ α
h : Function.Bijective ⇑x ∧ Function.Bijective ⇑y
x' : Fin (Fintype.card α) ≃ α := Equiv.ofBijective ⇑x ⋯
⊢ ∃ g, g • x = y
Theorem: Equiv.Perm.isMultiplyPretransitive
Proof state before:
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
x y : Fin (Fintype.card α) ↪ α
h : Function.Bijective ⇑x ∧ Function.Bijective ⇑y
x' : Fin (Fintype.card α) ≃ α := Equiv.ofBijective ⇑x ⋯
⊢ ∃ g, g • x = y
Tactic:
let y' := Equiv.ofBijective y h.2
Proof state after:
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
x y : Fin (Fintype.card α) ↪ α
h : Function.Bijective ⇑x ∧ Function.Bijective ⇑y
x' : Fin (Fintype.card α) ≃ α := Equiv.ofBijective ⇑x ⋯
y' : Fin (Fintype.card α) ≃ α := Equiv.ofBijective ⇑y ⋯
⊢ ∃ g, g • x = y
Theorem: Equiv.Perm.isMultiplyPretransitive
Proof state before:
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
x y : Fin (Fintype.card α) ↪ α
h : Function.Bijective ⇑x ∧ Function.Bijective ⇑y
x' : Fin (Fintype.card α) ≃ α := Equiv.ofBijective ⇑x ⋯
y' : Fin (Fintype.card α) ≃ α := Equiv.ofBijective ⇑y ⋯
⊢ ∃ g, g • x = y
Tactic:
use x'.symm.trans y'
Proof state after:
case h
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
x y : Fin (Fintype.card α) ↪ α
h : Function.Bijective ⇑x ∧ Function.Bijective ⇑y
x' : Fin (Fintype.card α) ≃ α := Equiv.ofBijective ⇑x ⋯
y' : Fin (Fintype.card α) ≃ α := Equiv.ofBijective ⇑y ⋯
⊢ x'.symm.trans y' • x = y
Theorem: Equiv.Perm.isMultiplyPretransitive
Proof state before:
case h
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
x y : Fin (Fintype.card α) ↪ α
h : Function.Bijective ⇑x ∧ Function.Bijective ⇑y
x' : Fin (Fintype.card α) ≃ α := Equiv.ofBijective ⇑x ⋯
y' : Fin (Fintype.card α) ≃ α := Equiv.ofBijective ⇑y ⋯
⊢ x'.symm.trans y' • x = y
Tactic:
ext i
Proof state after:
case h.h
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
x y : Fin (Fintype.card α) ↪ α
h : Function.Bijective ⇑x ∧ Function.Bijective ⇑y
x' : Fin (Fintype.card α) ≃ α := Equiv.ofBijective ⇑x ⋯
y' : Fin (Fintype.card α) ≃ α := Equiv.ofBijective ⇑y ⋯
i : Fin (Fintype.card α)
⊢ (x'.symm.trans y' • x) i = y i
Theorem: Equiv.Perm.isMultiplyPretransitive
Proof state before:
case h.h
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
x y : Fin (Fintype.card α) ↪ α
h : Function.Bijective ⇑x ∧ Function.Bijective ⇑y
x' : Fin (Fintype.card α) ≃ α := Equiv.ofBijective ⇑x ⋯
y' : Fin (Fintype.card α) ≃ α := Equiv.ofBijective ⇑y ⋯
i : Fin (Fintype.card α)
⊢ (x'.symm.trans y' • x) i = y i
Tactic:
simp only [smul_apply, Equiv.Perm.smul_def, Equiv.trans_apply, x', y']
Proof state after:
case h.h
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
x y : Fin (Fintype.card α) ↪ α
h : Function.Bijective ⇑x ∧ Function.Bijective ⇑y
x' : Fin (Fintype.card α) ≃ α := Equiv.ofBijective ⇑x ⋯
y' : Fin (Fintype.card α) ≃ α := Equiv.ofBijective ⇑y ⋯
i : Fin (Fintype.card α)
⊢ (Equiv.ofBijective ⇑y ⋯) ((Equiv.ofBijective ⇑x ⋯).symm (x i)) = y i
Theorem: Equiv.Perm.isMultiplyPretransitive
Proof state before:
case h.h
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
x y : Fin (Fintype.card α) ↪ α
h : Function.Bijective ⇑x ∧ Function.Bijective ⇑y
x' : Fin (Fintype.card α) ≃ α := Equiv.ofBijective ⇑x ⋯
y' : Fin (Fintype.card α) ≃ α := Equiv.ofBijective ⇑y ⋯
i : Fin (Fintype.card α)
⊢ (Equiv.ofBijective ⇑y ⋯) ((Equiv.ofBijective ⇑x ⋯).symm (x i)) = y i
Tactic:
simp only [Equiv.ofBijective_symm_apply_apply, Equiv.ofBijective_apply]
Proof state after:
no goals
Theorem: Equiv.Perm.isMultiplyPretransitive
Proof state before:
case exists_smul_eq.right
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
x y : Fin (Fintype.card α) ↪ α
⊢ Function.Bijective ⇑y
Tactic:
rw [Fintype.bijective_iff_injective_and_card]
Proof state after:
case exists_smul_eq.right
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
x y : Fin (Fintype.card α) ↪ α
⊢ Function.Injective ⇑y ∧ Fintype.card (Fin (Fintype.card α)) = Fintype.card α
Theorem: Equiv.Perm.isMultiplyPretransitive
Proof state before:
case exists_smul_eq.right
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
x y : Fin (Fintype.card α) ↪ α
⊢ Function.Injective ⇑y ∧ Fintype.card (Fin (Fintype.card α)) = Fintype.card α
Tactic:
constructor
Proof state after:
case exists_smul_eq.right.left
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
x y : Fin (Fintype.card α) ↪ α
⊢ Function.Injective ⇑y

case exists_smul_eq.right.right
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
x y : Fin (Fintype.card α) ↪ α
⊢ Fintype.card (Fin (Fintype.card α)) = Fintype.card α
Theorem: Equiv.Perm.isMultiplyPretransitive
Proof state before:
case exists_smul_eq.right.left
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
x y : Fin (Fintype.card α) ↪ α
⊢ Function.Injective ⇑y

case exists_smul_eq.right.right
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
x y : Fin (Fintype.card α) ↪ α
⊢ Fintype.card (Fin (Fintype.card α)) = Fintype.card α
Tactic:
apply EmbeddingLike.injective
Proof state after:
case exists_smul_eq.right.right
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
x y : Fin (Fintype.card α) ↪ α
⊢ Fintype.card (Fin (Fintype.card α)) = Fintype.card α
Theorem: Equiv.Perm.isMultiplyPretransitive
Proof state before:
case exists_smul_eq.right.right
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
x y : Fin (Fintype.card α) ↪ α
⊢ Fintype.card (Fin (Fintype.card α)) = Fintype.card α
Tactic:
exact Fintype.card_fin (Fintype.card α)
Proof state after:
no goals
Theorem: Equiv.Perm.isMultiplyPretransitive
Proof state before:
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n > Fintype.card α
this : IsEmpty (Fin n ↪ α)
⊢ IsMultiplyPretransitive (Equiv.Perm α) α n
Tactic:
apply IsPretransitive.mk
Proof state after:
case exists_smul_eq
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n > Fintype.card α
this : IsEmpty (Fin n ↪ α)
⊢ ∀ (x y : Fin n ↪ α), ∃ g, g • x = y
Theorem: Equiv.Perm.isMultiplyPretransitive
Proof state before:
case exists_smul_eq
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n > Fintype.card α
this : IsEmpty (Fin n ↪ α)
⊢ ∀ (x y : Fin n ↪ α), ∃ g, g • x = y
Tactic:
intro x
Proof state after:
case exists_smul_eq
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n > Fintype.card α
this : IsEmpty (Fin n ↪ α)
x : Fin n ↪ α
⊢ ∀ (y : Fin n ↪ α), ∃ g, g • x = y
Theorem: Equiv.Perm.isMultiplyPretransitive
Proof state before:
case exists_smul_eq
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n > Fintype.card α
this : IsEmpty (Fin n ↪ α)
x : Fin n ↪ α
⊢ ∀ (y : Fin n ↪ α), ∃ g, g • x = y
Tactic:
exfalso
Proof state after:
case exists_smul_eq
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n > Fintype.card α
this : IsEmpty (Fin n ↪ α)
x : Fin n ↪ α
⊢ False
Theorem: Equiv.Perm.isMultiplyPretransitive
Proof state before:
case exists_smul_eq
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n > Fintype.card α
this : IsEmpty (Fin n ↪ α)
x : Fin n ↪ α
⊢ False
Tactic:
exact this.false  x
Proof state after:
no goals
Theorem: Equiv.Perm.isPreprimitive
Proof state before:
M : Type ?u.243758
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
⊢ IsPreprimitive (Equiv.Perm α) α
Tactic:
cases subsingleton_or_nontrivial α
Proof state after:
case inl
M : Type ?u.243758
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
h✝ : Subsingleton α
⊢ IsPreprimitive (Equiv.Perm α) α

case inr
M : Type ?u.243758
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
h✝ : Nontrivial α
⊢ IsPreprimitive (Equiv.Perm α) α