internlm/Lean-Github huggingface dataset:
Theorem: may_extend_with'
Proof state before:
case h
α : Type u_1
m n k : ℕ
s : Set α
z : Fin k ↪ ↑s
h : n = m + k
x : Fin m ↪ ↑sᶜ
h' : n = k + m := h.trans (add_comm m k)
p : Fin n → Prop := fun i => ↑i < m
f : ↑{i | p i} → α := fun i => ↑(x.toFun (Fin.castLT ↑i ⋯))
g : ↑{i | ¬p i} → α := fun i => ↑(z.toFun (Fin.subNat m ((Fin.castIso h') ↑i) ⋯))
i : ℕ
hi : i < m
⊢ f { val := (Fin.castLEEmb ⋯) { val := i, isLt := hi }, property := hi } = (subtype sᶜ) (x { val := i, isLt := hi })
Tactic:
rfl
Proof state after:
no goals
Theorem: may_extend_with'
Proof state before:
case h.right
α : Type u_1
m n k : ℕ
s : Set α
z : Fin k ↪ ↑s
h : n = m + k
x : Fin m ↪ ↑sᶜ
h' : n = k + m := h.trans (add_comm m k)
p : Fin n → Prop := fun i => ↑i < m
f : ↑{i | p i} → α := fun i => ↑(x.toFun (Fin.castLT ↑i ⋯))
g : ↑{i | ¬p i} → α := fun i => ↑(z.toFun (Fin.subNat m ((Fin.castIso h') ↑i) ⋯))
⊢ Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv)
        { toFun := fun i => if hi : p i then f { val := i, property := hi } else g { val := i, property := hi },
          inj' := ⋯ }) =
    Function.Embedding.trans z (subtype s)
Tactic:
ext ⟨j, hj⟩
Proof state after:
case h.right.h.mk
α : Type u_1
m n k : ℕ
s : Set α
z : Fin k ↪ ↑s
h : n = m + k
x : Fin m ↪ ↑sᶜ
h' : n = k + m := h.trans (add_comm m k)
p : Fin n → Prop := fun i => ↑i < m
f : ↑{i | p i} → α := fun i => ↑(x.toFun (Fin.castLT ↑i ⋯))
g : ↑{i | ¬p i} → α := fun i => ↑(z.toFun (Fin.subNat m ((Fin.castIso h') ↑i) ⋯))
j : ℕ
hj : j < k
⊢ (Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
        (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv)
          { toFun := fun i => if hi : p i then f { val := i, property := hi } else g { val := i, property := hi },
            inj' := ⋯ }))
      { val := j, isLt := hj } =
    (Function.Embedding.trans z (subtype s)) { val := j, isLt := hj }
Theorem: may_extend_with'
Proof state before:
case h.right.h.mk
α : Type u_1
m n k : ℕ
s : Set α
z : Fin k ↪ ↑s
h : n = m + k
x : Fin m ↪ ↑sᶜ
h' : n = k + m := h.trans (add_comm m k)
p : Fin n → Prop := fun i => ↑i < m
f : ↑{i | p i} → α := fun i => ↑(x.toFun (Fin.castLT ↑i ⋯))
g : ↑{i | ¬p i} → α := fun i => ↑(z.toFun (Fin.subNat m ((Fin.castIso h') ↑i) ⋯))
j : ℕ
hj : j < k
⊢ (Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
        (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv)
          { toFun := fun i => if hi : p i then f { val := i, property := hi } else g { val := i, property := hi },
            inj' := ⋯ }))
      { val := j, isLt := hj } =
    (Function.Embedding.trans z (subtype s)) { val := j, isLt := hj }
Tactic:
simp only [Fin.natAddEmb_toEmbedding, gt_iff_lt, Set.coe_setOf, Set.mem_setOf_eq, toFun_eq_coe,
  Fin.castIso_apply, trans_apply, coeFn_mk, Fin.natAdd_mk, Equiv.coe_toEmbedding,
  RelIso.coe_fn_toEquiv, Fin.cast_mk, add_lt_iff_neg_left, not_lt_zero', ↓reduceDite,
  Fin.subNat_mk, add_tsub_cancel_left, p, f, g]
Proof state after:
case h.right.h.mk
α : Type u_1
m n k : ℕ
s : Set α
z : Fin k ↪ ↑s
h : n = m + k
x : Fin m ↪ ↑sᶜ
h' : n = k + m := h.trans (add_comm m k)
p : Fin n → Prop := fun i => ↑i < m
f : ↑{i | p i} → α := fun i => ↑(x.toFun (Fin.castLT ↑i ⋯))
g : ↑{i | ¬p i} → α := fun i => ↑(z.toFun (Fin.subNat m ((Fin.castIso h') ↑i) ⋯))
j : ℕ
hj : j < k
⊢ ↑(z { val := j, isLt := ⋯ }) = (subtype s) (z { val := j, isLt := hj })
Theorem: may_extend_with'
Proof state before:
case h.right.h.mk
α : Type u_1
m n k : ℕ
s : Set α
z : Fin k ↪ ↑s
h : n = m + k
x : Fin m ↪ ↑sᶜ
h' : n = k + m := h.trans (add_comm m k)
p : Fin n → Prop := fun i => ↑i < m
f : ↑{i | p i} → α := fun i => ↑(x.toFun (Fin.castLT ↑i ⋯))
g : ↑{i | ¬p i} → α := fun i => ↑(z.toFun (Fin.subNat m ((Fin.castIso h') ↑i) ⋯))
j : ℕ
hj : j < k
⊢ ↑(z { val := j, isLt := ⋯ }) = (subtype s) (z { val := j, isLt := hj })
Tactic:
rfl
Proof state after:
no goals
Theorem: MulAction.isPretransitive_of_submonoid
Proof state before:
M : Type u_1
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Monoid M
inst✝ : MulAction M α
K : Submonoid M
h : IsPretransitive (↥K) α
⊢ IsPretransitive M α
Tactic:
let h_eq := h.exists_smul_eq
Proof state after:
M : Type u_1
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Monoid M
inst✝ : MulAction M α
K : Submonoid M
h : IsPretransitive (↥K) α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
⊢ IsPretransitive M α
Theorem: MulAction.isPretransitive_of_submonoid
Proof state before:
M : Type u_1
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Monoid M
inst✝ : MulAction M α
K : Submonoid M
h : IsPretransitive (↥K) α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
⊢ IsPretransitive M α
Tactic:
apply IsPretransitive.mk
Proof state after:
case exists_smul_eq
M : Type u_1
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Monoid M
inst✝ : MulAction M α
K : Submonoid M
h : IsPretransitive (↥K) α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
⊢ ∀ (x y : α), ∃ g, g • x = y
Theorem: MulAction.isPretransitive_of_submonoid
Proof state before:
case exists_smul_eq
M : Type u_1
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Monoid M
inst✝ : MulAction M α
K : Submonoid M
h : IsPretransitive (↥K) α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
⊢ ∀ (x y : α), ∃ g, g • x = y
Tactic:
intro x y
Proof state after:
case exists_smul_eq
M : Type u_1
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Monoid M
inst✝ : MulAction M α
K : Submonoid M
h : IsPretransitive (↥K) α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : α
⊢ ∃ g, g • x = y
Theorem: MulAction.isPretransitive_of_submonoid
Proof state before:
case exists_smul_eq
M : Type u_1
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Monoid M
inst✝ : MulAction M α
K : Submonoid M
h : IsPretransitive (↥K) α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : α
⊢ ∃ g, g • x = y
Tactic:
obtain ⟨⟨k, hk⟩, hk'⟩ := h_eq x y
Proof state after:
case exists_smul_eq.intro.mk
M : Type u_1
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Monoid M
inst✝ : MulAction M α
K : Submonoid M
h : IsPretransitive (↥K) α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : α
k : M
hk : k ∈ K
hk' : { val := k, property := hk } • x = y
⊢ ∃ g, g • x = y
Theorem: MulAction.isPretransitive_of_submonoid
Proof state before:
case exists_smul_eq.intro.mk
M : Type u_1
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Monoid M
inst✝ : MulAction M α
K : Submonoid M
h : IsPretransitive (↥K) α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : α
k : M
hk : k ∈ K
hk' : { val := k, property := hk } • x = y
⊢ ∃ g, g • x = y
Tactic:
exact ⟨k, hk'⟩
Proof state after:
no goals
Theorem: MulAction.isPretransitive_of_submonoid_le
Proof state before:
M : Type u_1
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Monoid M
inst✝ : MulAction M α
G K : Submonoid M
hKG : K ≤ G
h : IsPretransitive (↥K) α
⊢ IsPretransitive (↥G) α
Tactic:
let h_eq := h.exists_smul_eq
Proof state after:
M : Type u_1
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Monoid M
inst✝ : MulAction M α
G K : Submonoid M
hKG : K ≤ G
h : IsPretransitive (↥K) α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
⊢ IsPretransitive (↥G) α
Theorem: MulAction.isPretransitive_of_submonoid_le
Proof state before:
M : Type u_1
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Monoid M
inst✝ : MulAction M α
G K : Submonoid M
hKG : K ≤ G
h : IsPretransitive (↥K) α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
⊢ IsPretransitive (↥G) α
Tactic:
apply IsPretransitive.mk
Proof state after:
case exists_smul_eq
M : Type u_1
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Monoid M
inst✝ : MulAction M α
G K : Submonoid M
hKG : K ≤ G
h : IsPretransitive (↥K) α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
⊢ ∀ (x y : α), ∃ g, g • x = y
Theorem: MulAction.isPretransitive_of_submonoid_le
Proof state before:
case exists_smul_eq
M : Type u_1
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Monoid M
inst✝ : MulAction M α
G K : Submonoid M
hKG : K ≤ G
h : IsPretransitive (↥K) α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
⊢ ∀ (x y : α), ∃ g, g • x = y
Tactic:
intro x y
Proof state after:
case exists_smul_eq
M : Type u_1
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Monoid M
inst✝ : MulAction M α
G K : Submonoid M
hKG : K ≤ G
h : IsPretransitive (↥K) α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : α
⊢ ∃ g, g • x = y
Theorem: MulAction.isPretransitive_of_submonoid_le
Proof state before:
case exists_smul_eq
M : Type u_1
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Monoid M
inst✝ : MulAction M α
G K : Submonoid M
hKG : K ≤ G
h : IsPretransitive (↥K) α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : α
⊢ ∃ g, g • x = y
Tactic:
obtain ⟨⟨k, hk⟩, hk'⟩ := h_eq x y
Proof state after:
case exists_smul_eq.intro.mk
M : Type u_1
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Monoid M
inst✝ : MulAction M α
G K : Submonoid M
hKG : K ≤ G
h : IsPretransitive (↥K) α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : α
k : M
hk : k ∈ K
hk' : { val := k, property := hk } • x = y
⊢ ∃ g, g • x = y
Theorem: MulAction.isPretransitive_of_submonoid_le
Proof state before:
case exists_smul_eq.intro.mk
M : Type u_1
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Monoid M
inst✝ : MulAction M α
G K : Submonoid M
hKG : K ≤ G
h : IsPretransitive (↥K) α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : α
k : M
hk : k ∈ K
hk' : { val := k, property := hk } • x = y
⊢ ∃ g, g • x = y
Tactic:
use ⟨k, hKG hk⟩
Proof state after:
case h
M : Type u_1
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Monoid M
inst✝ : MulAction M α
G K : Submonoid M
hKG : K ≤ G
h : IsPretransitive (↥K) α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : α
k : M
hk : k ∈ K
hk' : { val := k, property := hk } • x = y
⊢ { val := k, property := ⋯ } • x = y
Theorem: MulAction.isPretransitive_of_submonoid_le
Proof state before:
case h
M : Type u_1
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Monoid M
inst✝ : MulAction M α
G K : Submonoid M
hKG : K ≤ G
h : IsPretransitive (↥K) α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : α
k : M
hk : k ∈ K
hk' : { val := k, property := hk } • x = y
⊢ { val := k, property := ⋯ } • x = y
Tactic:
exact hk'
Proof state after:
no goals
Theorem: MulAction.card_orbit_eq_stabilizer_index
Proof state before:
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
a : α
⊢ Set.ncard (orbit M a) = Subgroup.index (stabilizer M a)
Tactic:
rw [← Set.Nat.card_coe_set_eq]
Proof state after:
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
a : α
⊢ Nat.card ↑(orbit M a) = Subgroup.index (stabilizer M a)
Theorem: MulAction.card_orbit_eq_stabilizer_index
Proof state before:
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
a : α
⊢ Nat.card ↑(orbit M a) = Subgroup.index (stabilizer M a)
Tactic:
apply Nat.card_congr
Proof state after:
case f
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
a : α
⊢ ↑(orbit M a) ≃ M ⧸ stabilizer M a
Theorem: MulAction.card_orbit_eq_stabilizer_index
Proof state before:
case f
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
a : α
⊢ ↑(orbit M a) ≃ M ⧸ stabilizer M a
Tactic:
exact orbitEquivQuotientStabilizer M a
Proof state after:
no goals
Theorem: MulAction.stabilizer_index_of_pretransitive
Proof state before:
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
h : IsPretransitive M α
a : α
⊢ Subgroup.index (stabilizer M a) = Nat.card α
Tactic:
rw [← card_orbit_eq_stabilizer_index]
Proof state after:
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
h : IsPretransitive M α
a : α
⊢ Set.ncard (orbit M a) = Nat.card α
Theorem: MulAction.stabilizer_index_of_pretransitive
Proof state before:
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
h : IsPretransitive M α
a : α
⊢ Set.ncard (orbit M a) = Nat.card α
Tactic:
convert Set.ncard_univ α
Proof state after:
case h.e'_2.h.e'_2
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
h : IsPretransitive M α
a : α
⊢ orbit M a = Set.univ
Theorem: MulAction.stabilizer_index_of_pretransitive
Proof state before:
case h.e'_2.h.e'_2
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
h : IsPretransitive M α
a : α
⊢ orbit M a = Set.univ
Tactic:
exact orbit_eq_univ M a
Proof state after:
no goals
Theorem: MulAction.isPretransitive_of_subgroup
Proof state before:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
K : Subgroup M
h : IsPretransitive (↥K) α
⊢ IsPretransitive M α
Tactic:
apply isPretransitive_of_submonoid
Proof state after:
case h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
K : Subgroup M
h : IsPretransitive (↥K) α
⊢ IsPretransitive (↥?K) α

case K
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
K : Subgroup M
h : IsPretransitive (↥K) α
⊢ Submonoid M
Theorem: MulAction.isPretransitive_of_subgroup
Proof state before:
case h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
K : Subgroup M
h : IsPretransitive (↥K) α
⊢ IsPretransitive (↥?K) α

case K
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
K : Subgroup M
h : IsPretransitive (↥K) α
⊢ Submonoid M
Tactic:
swap
Proof state after:
case K
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
K : Subgroup M
h : IsPretransitive (↥K) α
⊢ Submonoid M

case h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
K : Subgroup M
h : IsPretransitive (↥K) α
⊢ IsPretransitive (↥?K) α
Theorem: MulAction.isPretransitive_of_subgroup
Proof state before:
case K
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
K : Subgroup M
h : IsPretransitive (↥K) α
⊢ Submonoid M

case h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
K : Subgroup M
h : IsPretransitive (↥K) α
⊢ IsPretransitive (↥?K) α
Tactic:
exact K.toSubmonoid
Proof state after:
case h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
K : Subgroup M
h : IsPretransitive (↥K) α
⊢ IsPretransitive (↥K.toSubmonoid) α
Theorem: MulAction.isPretransitive_of_subgroup
Proof state before:
case h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
K : Subgroup M
h : IsPretransitive (↥K) α
⊢ IsPretransitive (↥K.toSubmonoid) α
Tactic:
exact h
Proof state after:
no goals
Theorem: MulAction.isPretransitive_of_subgroup_le
Proof state before:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
G K : Subgroup M
hKG : K ≤ G
h : IsPretransitive (↥K) α
⊢ IsPretransitive (↥G) α
Tactic:
let h_eq := h.exists_smul_eq
Proof state after:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
G K : Subgroup M
hKG : K ≤ G
h : IsPretransitive (↥K) α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
⊢ IsPretransitive (↥G) α
Theorem: MulAction.isPretransitive_of_subgroup_le
Proof state before:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
G K : Subgroup M
hKG : K ≤ G
h : IsPretransitive (↥K) α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
⊢ IsPretransitive (↥G) α
Tactic:
apply IsPretransitive.mk
Proof state after:
case exists_smul_eq
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
G K : Subgroup M
hKG : K ≤ G
h : IsPretransitive (↥K) α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
⊢ ∀ (x y : α), ∃ g, g • x = y
Theorem: MulAction.isPretransitive_of_subgroup_le
Proof state before:
case exists_smul_eq
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
G K : Subgroup M
hKG : K ≤ G
h : IsPretransitive (↥K) α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
⊢ ∀ (x y : α), ∃ g, g • x = y
Tactic:
intro x y
Proof state after:
case exists_smul_eq
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
G K : Subgroup M
hKG : K ≤ G
h : IsPretransitive (↥K) α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : α
⊢ ∃ g, g • x = y
Theorem: MulAction.isPretransitive_of_subgroup_le
Proof state before:
case exists_smul_eq
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
G K : Subgroup M
hKG : K ≤ G
h : IsPretransitive (↥K) α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : α
⊢ ∃ g, g • x = y
Tactic:
obtain ⟨⟨k, hk⟩, hk'⟩ := h_eq x y
Proof state after:
case exists_smul_eq.intro.mk
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
G K : Subgroup M
hKG : K ≤ G
h : IsPretransitive (↥K) α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : α
k : M
hk : k ∈ K
hk' : { val := k, property := hk } • x = y
⊢ ∃ g, g • x = y
Theorem: MulAction.isPretransitive_of_subgroup_le
Proof state before:
case exists_smul_eq.intro.mk
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
G K : Subgroup M
hKG : K ≤ G
h : IsPretransitive (↥K) α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : α
k : M
hk : k ∈ K
hk' : { val := k, property := hk } • x = y
⊢ ∃ g, g • x = y
Tactic:
use ⟨k, hKG hk⟩
Proof state after:
case h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
G K : Subgroup M
hKG : K ≤ G
h : IsPretransitive (↥K) α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : α
k : M
hk : k ∈ K
hk' : { val := k, property := hk } • x = y
⊢ { val := k, property := ⋯ } • x = y
Theorem: MulAction.isPretransitive_of_subgroup_le
Proof state before:
case h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
G K : Subgroup M
hKG : K ≤ G
h : IsPretransitive (↥K) α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : α
k : M
hk : k ∈ K
hk' : { val := k, property := hk } • x = y
⊢ { val := k, property := ⋯ } • x = y
Tactic:
exact hk'
Proof state after:
no goals
Theorem: MulAction.finOneToMap_bijective
Proof state before:
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
⊢ Function.Bijective ⇑(finOneToMap M α)
Tactic:
constructor
Proof state after:
case left
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
⊢ Function.Injective ⇑(finOneToMap M α)

case right
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
⊢ Function.Surjective ⇑(finOneToMap M α)
Theorem: MulAction.finOneToMap_bijective
Proof state before:
case left
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
⊢ Function.Injective ⇑(finOneToMap M α)
Tactic:
intro x y hxy
Proof state after:
case left
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
x y : Fin 1 ↪ α
hxy : (finOneToMap M α) x = (finOneToMap M α) y
⊢ x = y
Theorem: MulAction.finOneToMap_bijective
Proof state before:
case left
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
x y : Fin 1 ↪ α
hxy : (finOneToMap M α) x = (finOneToMap M α) y
⊢ x = y
Tactic:
ext i
Proof state after:
case left.h
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
x y : Fin 1 ↪ α
hxy : (finOneToMap M α) x = (finOneToMap M α) y
i : Fin 1
⊢ x i = y i
Theorem: MulAction.finOneToMap_bijective
Proof state before:
case left.h
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
x y : Fin 1 ↪ α
hxy : (finOneToMap M α) x = (finOneToMap M α) y
i : Fin 1
⊢ x i = y i
Tactic:
rw [Fin.eq_zero i]
Proof state after:
case left.h
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
x y : Fin 1 ↪ α
hxy : (finOneToMap M α) x = (finOneToMap M α) y
i : Fin 1
⊢ x 0 = y 0
Theorem: MulAction.finOneToMap_bijective
Proof state before:
case left.h
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
x y : Fin 1 ↪ α
hxy : (finOneToMap M α) x = (finOneToMap M α) y
i : Fin 1
⊢ x 0 = y 0
Tactic:
exact hxy
Proof state after:
no goals
Theorem: MulAction.finOneToMap_bijective
Proof state before:
case right
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
⊢ Function.Surjective ⇑(finOneToMap M α)
Tactic:
intro a
Proof state after:
case right
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
a : α
⊢ ∃ a_1, (finOneToMap M α) a_1 = a
Theorem: MulAction.finOneToMap_bijective
Proof state before:
case right
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
a : α
⊢ ∃ a_1, (finOneToMap M α) a_1 = a
Tactic:
use {
  toFun := fun _ => a
  inj' := fun i j _ => by
    rw [Fin.eq_zero i, Fin.eq_zero j] }
Proof state after:
case h
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
a : α
⊢ (finOneToMap M α) { toFun := fun x => a, inj' := ⋯ } = a
Theorem: MulAction.finOneToMap_bijective
Proof state before:
case h
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
a : α
⊢ (finOneToMap M α) { toFun := fun x => a, inj' := ⋯ } = a
Tactic:
rfl
Proof state after:
no goals
Theorem: MulAction.finOneToMap_bijective
Proof state before:
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
a : α
i j : Fin 1
x✝ : (fun x => a) i = (fun x => a) j
⊢ i = j
Tactic:
rw [Fin.eq_zero i, Fin.eq_zero j]
Proof state after:
no goals
Theorem: MulAction.isMultiplyPretransitive_of_subgroup
Proof state before:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
K : Subgroup M
h : IsMultiplyPretransitive (↥K) α n
⊢ IsMultiplyPretransitive M α n
Tactic:
unfold IsMultiplyPretransitive at *
Proof state after:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
K : Subgroup M
h : IsPretransitive (↥K) (Fin n ↪ α)
⊢ IsPretransitive M (Fin n ↪ α)
Theorem: MulAction.isMultiplyPretransitive_of_subgroup
Proof state before:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
K : Subgroup M
h : IsPretransitive (↥K) (Fin n ↪ α)
⊢ IsPretransitive M (Fin n ↪ α)
Tactic:
exact isPretransitive_of_subgroup h
Proof state after:
no goals
Theorem: MulAction.isMultiplyPretransitive_of_le
Proof state before:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
H K : Subgroup M
hHK : K ≤ H
h : IsMultiplyPretransitive (↥K) α n
⊢ IsMultiplyPretransitive (↥H) α n
Tactic:
unfold IsMultiplyPretransitive at *
Proof state after:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
H K : Subgroup M
hHK : K ≤ H
h : IsPretransitive (↥K) (Fin n ↪ α)
⊢ IsPretransitive (↥H) (Fin n ↪ α)
Theorem: MulAction.isMultiplyPretransitive_of_le
Proof state before:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
H K : Subgroup M
hHK : K ≤ H
h : IsPretransitive (↥K) (Fin n ↪ α)
⊢ IsPretransitive (↥H) (Fin n ↪ α)
Tactic:
refine' isPretransitive_of_subgroup_le hHK h
Proof state after:
no goals
Theorem: MulAction.EquivariantMap.embeddingOfEquivariantMap_is_injective
Proof state before:
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.Injective ⇑f
ι : Type u_5
⊢ Function.Injective ⇑(embeddingOfEquivariantMap hf ι)
Tactic:
intro x y hxy
Proof state after:
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.Injective ⇑f
ι : Type u_5
x y : ι ↪ α
hxy : (embeddingOfEquivariantMap hf ι) x = (embeddingOfEquivariantMap hf ι) y
⊢ x = y
Theorem: MulAction.EquivariantMap.embeddingOfEquivariantMap_is_injective
Proof state before:
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.Injective ⇑f
ι : Type u_5
x y : ι ↪ α
hxy : (embeddingOfEquivariantMap hf ι) x = (embeddingOfEquivariantMap hf ι) y
⊢ x = y
Tactic:
ext i
Proof state after:
case h
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.Injective ⇑f
ι : Type u_5
x y : ι ↪ α
hxy : (embeddingOfEquivariantMap hf ι) x = (embeddingOfEquivariantMap hf ι) y
i : ι
⊢ x i = y i