internlm/Lean-Github huggingface dataset:
Theorem: SubMulAction.conjMap_ofFixingSubgroup_bijective
Proof state before:
case h
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
g : M
hst : g • s = t
x : α
hx : x ∈ ofFixingSubgroup M t
hst' : g⁻¹ • t = s
⊢ (conjMap_ofFixingSubgroup M hst) ((conjMap_ofFixingSubgroup M hst') { val := x, property := hx }) =
    { val := x, property := hx }
Tactic:
rw [← SetLike.coe_eq_coe]
Proof state after:
case h
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
g : M
hst : g • s = t
x : α
hx : x ∈ ofFixingSubgroup M t
hst' : g⁻¹ • t = s
⊢ ↑((conjMap_ofFixingSubgroup M hst) ((conjMap_ofFixingSubgroup M hst') { val := x, property := hx })) =
    ↑{ val := x, property := hx }
Theorem: SubMulAction.conjMap_ofFixingSubgroup_bijective
Proof state before:
case h
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
g : M
hst : g • s = t
x : α
hx : x ∈ ofFixingSubgroup M t
hst' : g⁻¹ • t = s
⊢ ↑((conjMap_ofFixingSubgroup M hst) ((conjMap_ofFixingSubgroup M hst') { val := x, property := hx })) =
    ↑{ val := x, property := hx }
Tactic:
change g • g⁻¹ • x = x
Proof state after:
case h
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
g : M
hst : g • s = t
x : α
hx : x ∈ ofFixingSubgroup M t
hst' : g⁻¹ • t = s
⊢ g • g⁻¹ • x = x
Theorem: SubMulAction.conjMap_ofFixingSubgroup_bijective
Proof state before:
case h
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
g : M
hst : g • s = t
x : α
hx : x ∈ ofFixingSubgroup M t
hst' : g⁻¹ • t = s
⊢ g • g⁻¹ • x = x
Tactic:
rw [← mul_smul, mul_inv_self, one_smul]
Proof state after:
no goals
Theorem: SubMulAction.conjMap_ofFixingSubgroup_bijective
Proof state before:
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
g : M
hst : g • s = t
x : α
hx : x ∈ ofFixingSubgroup M t
⊢ g⁻¹ • t = s
Tactic:
apply symm
Proof state after:
case a
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
g : M
hst : g • s = t
x : α
hx : x ∈ ofFixingSubgroup M t
⊢ s = g⁻¹ • t
Theorem: SubMulAction.conjMap_ofFixingSubgroup_bijective
Proof state before:
case a
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
g : M
hst : g • s = t
x : α
hx : x ∈ ofFixingSubgroup M t
⊢ s = g⁻¹ • t
Tactic:
rw [← inv_smul_eq_iff]
Proof state after:
case a
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
g : M
hst : g • s = t
x : α
hx : x ∈ ofFixingSubgroup M t
⊢ g⁻¹⁻¹ • s = t
Theorem: SubMulAction.conjMap_ofFixingSubgroup_bijective
Proof state before:
case a
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
g : M
hst : g • s = t
x : α
hx : x ∈ ofFixingSubgroup M t
⊢ g⁻¹⁻¹ • s = t
Tactic:
rw [inv_inv]
Proof state after:
case a
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
g : M
hst : g • s = t
x : α
hx : x ∈ ofFixingSubgroup M t
⊢ g • s = t
Theorem: SubMulAction.conjMap_ofFixingSubgroup_bijective
Proof state before:
case a
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
g : M
hst : g • s = t
x : α
hx : x ∈ ofFixingSubgroup M t
⊢ g • s = t
Tactic:
exact hst
Proof state after:
no goals
Theorem: SubMulAction.ofStabilizer.conjMap_bijective
Proof state before:
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a b : α
g : M
hab : g • a = b
⊢ Function.Bijective ⇑(conjMap M hab)
Tactic:
constructor
Proof state after:
case left
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a b : α
g : M
hab : g • a = b
⊢ Function.Injective ⇑(conjMap M hab)

case right
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a b : α
g : M
hab : g • a = b
⊢ Function.Surjective ⇑(conjMap M hab)
Theorem: SubMulAction.ofStabilizer.conjMap_bijective
Proof state before:
case left
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a b : α
g : M
hab : g • a = b
⊢ Function.Injective ⇑(conjMap M hab)
Tactic:
rintro ⟨x, hx⟩ ⟨y, hy⟩ hxy
Proof state after:
case left.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a b : α
g : M
hab : g • a = b
x : α
hx : x ∈ ofStabilizer M a
y : α
hy : y ∈ ofStabilizer M a
hxy : (conjMap M hab) { val := x, property := hx } = (conjMap M hab) { val := y, property := hy }
⊢ { val := x, property := hx } = { val := y, property := hy }
Theorem: SubMulAction.ofStabilizer.conjMap_bijective
Proof state before:
case left.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a b : α
g : M
hab : g • a = b
x : α
hx : x ∈ ofStabilizer M a
y : α
hy : y ∈ ofStabilizer M a
hxy : (conjMap M hab) { val := x, property := hx } = (conjMap M hab) { val := y, property := hy }
⊢ { val := x, property := hx } = { val := y, property := hy }
Tactic:
simp only [Subtype.mk_eq_mk]
Proof state after:
case left.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a b : α
g : M
hab : g • a = b
x : α
hx : x ∈ ofStabilizer M a
y : α
hy : y ∈ ofStabilizer M a
hxy : (conjMap M hab) { val := x, property := hx } = (conjMap M hab) { val := y, property := hy }
⊢ x = y
Theorem: SubMulAction.ofStabilizer.conjMap_bijective
Proof state before:
case left.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a b : α
g : M
hab : g • a = b
x : α
hx : x ∈ ofStabilizer M a
y : α
hy : y ∈ ofStabilizer M a
hxy : (conjMap M hab) { val := x, property := hx } = (conjMap M hab) { val := y, property := hy }
⊢ x = y
Tactic:
rw [← SetLike.coe_eq_coe] at hxy
Proof state after:
case left.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a b : α
g : M
hab : g • a = b
x : α
hx : x ∈ ofStabilizer M a
y : α
hy : y ∈ ofStabilizer M a
hxy : ↑((conjMap M hab) { val := x, property := hx }) = ↑((conjMap M hab) { val := y, property := hy })
⊢ x = y
Theorem: SubMulAction.ofStabilizer.conjMap_bijective
Proof state before:
case left.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a b : α
g : M
hab : g • a = b
x : α
hx : x ∈ ofStabilizer M a
y : α
hy : y ∈ ofStabilizer M a
hxy : ↑((conjMap M hab) { val := x, property := hx }) = ↑((conjMap M hab) { val := y, property := hy })
⊢ x = y
Tactic:
change g • x = g • y at hxy
Proof state after:
case left.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a b : α
g : M
hab : g • a = b
x : α
hx : x ∈ ofStabilizer M a
y : α
hy : y ∈ ofStabilizer M a
hxy : g • x = g • y
⊢ x = y
Theorem: SubMulAction.ofStabilizer.conjMap_bijective
Proof state before:
case left.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a b : α
g : M
hab : g • a = b
x : α
hx : x ∈ ofStabilizer M a
y : α
hy : y ∈ ofStabilizer M a
hxy : g • x = g • y
⊢ x = y
Tactic:
apply (MulAction.injective g) hxy
Proof state after:
no goals
Theorem: SubMulAction.ofStabilizer.conjMap_bijective
Proof state before:
case right
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a b : α
g : M
hab : g • a = b
⊢ Function.Surjective ⇑(conjMap M hab)
Tactic:
rintro ⟨x, hx⟩
Proof state after:
case right.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a b : α
g : M
hab : g • a = b
x : α
hx : x ∈ ofStabilizer M b
⊢ ∃ a_1, (conjMap M hab) a_1 = { val := x, property := hx }
Theorem: SubMulAction.ofStabilizer.conjMap_bijective
Proof state before:
case right.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a b : α
g : M
hab : g • a = b
x : α
hx : x ∈ ofStabilizer M b
⊢ ∃ a_1, (conjMap M hab) a_1 = { val := x, property := hx }
Tactic:
use (SubMulAction.ofStabilizer.conjMap M (inv_smul_eq_iff.mpr hab.symm)) ⟨x, hx⟩
Proof state after:
case h
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a b : α
g : M
hab : g • a = b
x : α
hx : x ∈ ofStabilizer M b
⊢ (conjMap M hab) ((conjMap M ⋯) { val := x, property := hx }) = { val := x, property := hx }
Theorem: SubMulAction.ofStabilizer.conjMap_bijective
Proof state before:
case h
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a b : α
g : M
hab : g • a = b
x : α
hx : x ∈ ofStabilizer M b
⊢ (conjMap M hab) ((conjMap M ⋯) { val := x, property := hx }) = { val := x, property := hx }
Tactic:
rw [← SetLike.coe_eq_coe]
Proof state after:
case h
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a b : α
g : M
hab : g • a = b
x : α
hx : x ∈ ofStabilizer M b
⊢ ↑((conjMap M hab) ((conjMap M ⋯) { val := x, property := hx })) = ↑{ val := x, property := hx }
Theorem: SubMulAction.ofStabilizer.conjMap_bijective
Proof state before:
case h
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a b : α
g : M
hab : g • a = b
x : α
hx : x ∈ ofStabilizer M b
⊢ ↑((conjMap M hab) ((conjMap M ⋯) { val := x, property := hx })) = ↑{ val := x, property := hx }
Tactic:
change g • g⁻¹ • x = x
Proof state after:
case h
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a b : α
g : M
hab : g • a = b
x : α
hx : x ∈ ofStabilizer M b
⊢ g • g⁻¹ • x = x
Theorem: SubMulAction.ofStabilizer.conjMap_bijective
Proof state before:
case h
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a b : α
g : M
hab : g • a = b
x : α
hx : x ∈ ofStabilizer M b
⊢ g • g⁻¹ • x = x
Tactic:
simp only [smul_inv_smul]
Proof state after:
no goals
Theorem: SubMulAction.OfFixingSubgroupUnion.map_bijective
Proof state before:
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
⊢ Function.Bijective ⇑(map_ofFixingSubgroupUnion M s t)
Tactic:
constructor
Proof state after:
case left
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
⊢ Function.Injective ⇑(map_ofFixingSubgroupUnion M s t)

case right
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
⊢ Function.Surjective ⇑(map_ofFixingSubgroupUnion M s t)
Theorem: SubMulAction.OfFixingSubgroupUnion.map_bijective
Proof state before:
case left
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
⊢ Function.Injective ⇑(map_ofFixingSubgroupUnion M s t)
Tactic:
intro a b h
Proof state after:
case left
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
a b : ↥(ofFixingSubgroup M (s ∪ t))
h : (map_ofFixingSubgroupUnion M s t) a = (map_ofFixingSubgroupUnion M s t) b
⊢ a = b
Theorem: SubMulAction.OfFixingSubgroupUnion.map_bijective
Proof state before:
case left
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
a b : ↥(ofFixingSubgroup M (s ∪ t))
h : (map_ofFixingSubgroupUnion M s t) a = (map_ofFixingSubgroupUnion M s t) b
⊢ a = b
Tactic:
simp only [← SetLike.coe_eq_coe] at h ⊢
Proof state after:
case left
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
a b : ↥(ofFixingSubgroup M (s ∪ t))
h : ↑↑((map_ofFixingSubgroupUnion M s t) a) = ↑↑((map_ofFixingSubgroupUnion M s t) b)
⊢ ↑a = ↑b
Theorem: SubMulAction.OfFixingSubgroupUnion.map_bijective
Proof state before:
case left
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
a b : ↥(ofFixingSubgroup M (s ∪ t))
h : ↑↑((map_ofFixingSubgroupUnion M s t) a) = ↑↑((map_ofFixingSubgroupUnion M s t) b)
⊢ ↑a = ↑b
Tactic:
exact h
Proof state after:
no goals
Theorem: SubMulAction.OfFixingSubgroupUnion.map_bijective
Proof state before:
case right
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
⊢ Function.Surjective ⇑(map_ofFixingSubgroupUnion M s t)
Tactic:
rintro ⟨⟨a, ha⟩, ha'⟩
Proof state after:
case right.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
a : α
ha : a ∈ ofFixingSubgroup M s
ha' : { val := a, property := ha } ∈ ofFixingSubgroup (↥(fixingSubgroup M s)) (Subtype.val ⁻¹' t)
⊢ ∃ a_1, (map_ofFixingSubgroupUnion M s t) a_1 = { val := { val := a, property := ha }, property := ha' }
Theorem: SubMulAction.OfFixingSubgroupUnion.map_bijective
Proof state before:
case right.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
a : α
ha : a ∈ ofFixingSubgroup M s
ha' : { val := a, property := ha } ∈ ofFixingSubgroup (↥(fixingSubgroup M s)) (Subtype.val ⁻¹' t)
⊢ ∃ a_1, (map_ofFixingSubgroupUnion M s t) a_1 = { val := { val := a, property := ha }, property := ha' }
Tactic:
suffices a ∈ ofFixingSubgroup M (s ∪ t) by
  exact ⟨⟨a, this⟩,  rfl⟩
Proof state after:
case right.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
a : α
ha : a ∈ ofFixingSubgroup M s
ha' : { val := a, property := ha } ∈ ofFixingSubgroup (↥(fixingSubgroup M s)) (Subtype.val ⁻¹' t)
⊢ a ∈ ofFixingSubgroup M (s ∪ t)
Theorem: SubMulAction.OfFixingSubgroupUnion.map_bijective
Proof state before:
case right.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
a : α
ha : a ∈ ofFixingSubgroup M s
ha' : { val := a, property := ha } ∈ ofFixingSubgroup (↥(fixingSubgroup M s)) (Subtype.val ⁻¹' t)
⊢ a ∈ ofFixingSubgroup M (s ∪ t)
Tactic:
intro hy
Proof state after:
case right.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
a : α
ha : a ∈ ofFixingSubgroup M s
ha' : { val := a, property := ha } ∈ ofFixingSubgroup (↥(fixingSubgroup M s)) (Subtype.val ⁻¹' t)
hy : a ∈ s ∪ t
⊢ False
Theorem: SubMulAction.OfFixingSubgroupUnion.map_bijective
Proof state before:
case right.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
a : α
ha : a ∈ ofFixingSubgroup M s
ha' : { val := a, property := ha } ∈ ofFixingSubgroup (↥(fixingSubgroup M s)) (Subtype.val ⁻¹' t)
hy : a ∈ s ∪ t
⊢ False
Tactic:
cases' (Set.mem_union a s t).mp hy with h h
Proof state after:
case right.mk.mk.inl
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
a : α
ha : a ∈ ofFixingSubgroup M s
ha' : { val := a, property := ha } ∈ ofFixingSubgroup (↥(fixingSubgroup M s)) (Subtype.val ⁻¹' t)
hy : a ∈ s ∪ t
h : a ∈ s
⊢ False

case right.mk.mk.inr
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
a : α
ha : a ∈ ofFixingSubgroup M s
ha' : { val := a, property := ha } ∈ ofFixingSubgroup (↥(fixingSubgroup M s)) (Subtype.val ⁻¹' t)
hy : a ∈ s ∪ t
h : a ∈ t
⊢ False
Theorem: SubMulAction.OfFixingSubgroupUnion.map_bijective
Proof state before:
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
a : α
ha : a ∈ ofFixingSubgroup M s
ha' : { val := a, property := ha } ∈ ofFixingSubgroup (↥(fixingSubgroup M s)) (Subtype.val ⁻¹' t)
this : a ∈ ofFixingSubgroup M (s ∪ t)
⊢ ∃ a_1, (map_ofFixingSubgroupUnion M s t) a_1 = { val := { val := a, property := ha }, property := ha' }
Tactic:
exact ⟨⟨a, this⟩,  rfl⟩
Proof state after:
no goals
Theorem: SubMulAction.OfFixingSubgroupUnion.map_bijective
Proof state before:
case right.mk.mk.inl
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
a : α
ha : a ∈ ofFixingSubgroup M s
ha' : { val := a, property := ha } ∈ ofFixingSubgroup (↥(fixingSubgroup M s)) (Subtype.val ⁻¹' t)
hy : a ∈ s ∪ t
h : a ∈ s
⊢ False
Tactic:
exact ha h
Proof state after:
no goals
Theorem: SubMulAction.OfFixingSubgroupUnion.map_bijective
Proof state before:
case right.mk.mk.inr
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
a : α
ha : a ∈ ofFixingSubgroup M s
ha' : { val := a, property := ha } ∈ ofFixingSubgroup (↥(fixingSubgroup M s)) (Subtype.val ⁻¹' t)
hy : a ∈ s ∪ t
h : a ∈ t
⊢ False
Tactic:
apply ha'
Proof state after:
case right.mk.mk.inr
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
a : α
ha : a ∈ ofFixingSubgroup M s
ha' : { val := a, property := ha } ∈ ofFixingSubgroup (↥(fixingSubgroup M s)) (Subtype.val ⁻¹' t)
hy : a ∈ s ∪ t
h : a ∈ t
⊢ { val := a, property := ha } ∈ Subtype.val ⁻¹' t
Theorem: SubMulAction.OfFixingSubgroupUnion.map_bijective
Proof state before:
case right.mk.mk.inr
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
a : α
ha : a ∈ ofFixingSubgroup M s
ha' : { val := a, property := ha } ∈ ofFixingSubgroup (↥(fixingSubgroup M s)) (Subtype.val ⁻¹' t)
hy : a ∈ s ∪ t
h : a ∈ t
⊢ { val := a, property := ha } ∈ Subtype.val ⁻¹' t
Tactic:
simp only [Set.mem_preimage]
Proof state after:
case right.mk.mk.inr
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
a : α
ha : a ∈ ofFixingSubgroup M s
ha' : { val := a, property := ha } ∈ ofFixingSubgroup (↥(fixingSubgroup M s)) (Subtype.val ⁻¹' t)
hy : a ∈ s ∪ t
h : a ∈ t
⊢ a ∈ t
Theorem: SubMulAction.OfFixingSubgroupUnion.map_bijective
Proof state before:
case right.mk.mk.inr
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
a : α
ha : a ∈ ofFixingSubgroup M s
ha' : { val := a, property := ha } ∈ ofFixingSubgroup (↥(fixingSubgroup M s)) (Subtype.val ⁻¹' t)
hy : a ∈ s ∪ t
h : a ∈ t
⊢ a ∈ t
Tactic:
exact h
Proof state after:
no goals
Theorem: SubMulAction.ofFixingSubgroup.mapOfInclusion_injective
Proof state before:
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : t ⊆ s
⊢ Function.Injective ⇑(mapOfInclusion M hst)
Tactic:
rintro ⟨x, hx⟩ ⟨y, hy⟩ hxy
Proof state after:
case mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : t ⊆ s
x : α
hx : x ∈ ofFixingSubgroup M s
y : α
hy : y ∈ ofFixingSubgroup M s
hxy : (mapOfInclusion M hst) { val := x, property := hx } = (mapOfInclusion M hst) { val := y, property := hy }
⊢ { val := x, property := hx } = { val := y, property := hy }
Theorem: SubMulAction.ofFixingSubgroup.mapOfInclusion_injective
Proof state before:
case mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : t ⊆ s
x : α
hx : x ∈ ofFixingSubgroup M s
y : α
hy : y ∈ ofFixingSubgroup M s
hxy : (mapOfInclusion M hst) { val := x, property := hx } = (mapOfInclusion M hst) { val := y, property := hy }
⊢ { val := x, property := hx } = { val := y, property := hy }
Tactic:
rw [← SetLike.coe_eq_coe] at hxy ⊢
Proof state after:
case mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : t ⊆ s
x : α
hx : x ∈ ofFixingSubgroup M s
y : α
hy : y ∈ ofFixingSubgroup M s
hxy : ↑((mapOfInclusion M hst) { val := x, property := hx }) = ↑((mapOfInclusion M hst) { val := y, property := hy })
⊢ ↑{ val := x, property := hx } = ↑{ val := y, property := hy }
Theorem: SubMulAction.ofFixingSubgroup.mapOfInclusion_injective
Proof state before:
case mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : t ⊆ s
x : α
hx : x ∈ ofFixingSubgroup M s
y : α
hy : y ∈ ofFixingSubgroup M s
hxy : ↑((mapOfInclusion M hst) { val := x, property := hx }) = ↑((mapOfInclusion M hst) { val := y, property := hy })
⊢ ↑{ val := x, property := hx } = ↑{ val := y, property := hy }
Tactic:
exact hxy
Proof state after:
no goals
Theorem: SubMulAction.OfFixingSubgroupOfSingleton.map_bijective
Proof state before:
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
⊢ Function.Bijective ⇑(map M a)
Tactic:
constructor
Proof state after:
case left
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
⊢ Function.Injective ⇑(map M a)

case right
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
⊢ Function.Surjective ⇑(map M a)
Theorem: SubMulAction.OfFixingSubgroupOfSingleton.map_bijective
Proof state before:
case left
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
⊢ Function.Injective ⇑(map M a)
Tactic:
intro _ _ hxy
Proof state after:
case left
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
a₁✝ a₂✝ : ↥(ofFixingSubgroup M {a})
hxy : (map M a) a₁✝ = (map M a) a₂✝
⊢ a₁✝ = a₂✝
Theorem: SubMulAction.OfFixingSubgroupOfSingleton.map_bijective
Proof state before:
case left
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
a₁✝ a₂✝ : ↥(ofFixingSubgroup M {a})
hxy : (map M a) a₁✝ = (map M a) a₂✝
⊢ a₁✝ = a₂✝
Tactic:
exact hxy
Proof state after:
no goals
Theorem: SubMulAction.OfFixingSubgroupOfSingleton.map_bijective
Proof state before:
case right
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
⊢ Function.Surjective ⇑(map M a)
Tactic:
intro x
Proof state after:
case right
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
x : ↥(ofStabilizer M a)
⊢ ∃ a_1, (map M a) a_1 = x
Theorem: SubMulAction.OfFixingSubgroupOfSingleton.map_bijective
Proof state before:
case right
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
x : ↥(ofStabilizer M a)
⊢ ∃ a_1, (map M a) a_1 = x
Tactic:
use x
Proof state after:
case h
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
x : ↥(ofStabilizer M a)
⊢ (map M a) x = x
Theorem: SubMulAction.OfFixingSubgroupOfSingleton.map_bijective
Proof state before:
case h
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
x : ↥(ofStabilizer M a)
⊢ (map M a) x = x
Tactic:
rfl
Proof state after:
no goals
Theorem: SubMulAction.OfFixingSubgroupOfEq.map_bijective
Proof state before:
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : s = t
⊢ Function.Bijective ⇑(map M hst)
Tactic:
constructor
Proof state after:
case left
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : s = t
⊢ Function.Injective ⇑(map M hst)

case right
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : s = t
⊢ Function.Surjective ⇑(map M hst)
Theorem: SubMulAction.OfFixingSubgroupOfEq.map_bijective
Proof state before:
case left
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : s = t
⊢ Function.Injective ⇑(map M hst)
Tactic:
rintro ⟨x, hx⟩ ⟨y, hy⟩ hxy
Proof state after:
case left.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : s = t
x : α
hx : x ∈ ofFixingSubgroup M s
y : α
hy : y ∈ ofFixingSubgroup M s
hxy : (map M hst) { val := x, property := hx } = (map M hst) { val := y, property := hy }
⊢ { val := x, property := hx } = { val := y, property := hy }
Theorem: SubMulAction.OfFixingSubgroupOfEq.map_bijective
Proof state before:
case left.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : s = t
x : α
hx : x ∈ ofFixingSubgroup M s
y : α
hy : y ∈ ofFixingSubgroup M s
hxy : (map M hst) { val := x, property := hx } = (map M hst) { val := y, property := hy }
⊢ { val := x, property := hx } = { val := y, property := hy }
Tactic:
rw [← SetLike.coe_eq_coe] at hxy ⊢
Proof state after:
case left.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : s = t
x : α
hx : x ∈ ofFixingSubgroup M s
y : α
hy : y ∈ ofFixingSubgroup M s
hxy : ↑((map M hst) { val := x, property := hx }) = ↑((map M hst) { val := y, property := hy })
⊢ ↑{ val := x, property := hx } = ↑{ val := y, property := hy }
Theorem: SubMulAction.OfFixingSubgroupOfEq.map_bijective
Proof state before:
case left.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : s = t
x : α
hx : x ∈ ofFixingSubgroup M s
y : α
hy : y ∈ ofFixingSubgroup M s
hxy : ↑((map M hst) { val := x, property := hx }) = ↑((map M hst) { val := y, property := hy })
⊢ ↑{ val := x, property := hx } = ↑{ val := y, property := hy }
Tactic:
simp only [SubMulAction.OfFixingSubgroupOfEq.map_def M hst] at hxy
Proof state after:
case left.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : s = t
x : α
hx : x ∈ ofFixingSubgroup M s
y : α
hy : y ∈ ofFixingSubgroup M s
hxy : x = y
⊢ ↑{ val := x, property := hx } = ↑{ val := y, property := hy }
Theorem: SubMulAction.OfFixingSubgroupOfEq.map_bijective
Proof state before:
case left.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : s = t
x : α
hx : x ∈ ofFixingSubgroup M s
y : α
hy : y ∈ ofFixingSubgroup M s
hxy : x = y
⊢ ↑{ val := x, property := hx } = ↑{ val := y, property := hy }
Tactic:
simp only
Proof state after:
case left.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : s = t
x : α
hx : x ∈ ofFixingSubgroup M s
y : α
hy : y ∈ ofFixingSubgroup M s
hxy : x = y
⊢ x = y
Theorem: SubMulAction.OfFixingSubgroupOfEq.map_bijective
Proof state before:
case left.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : s = t
x : α
hx : x ∈ ofFixingSubgroup M s
y : α
hy : y ∈ ofFixingSubgroup M s
hxy : x = y
⊢ x = y
Tactic:
rw [hxy]
Proof state after:
no goals