internlm/Lean-Github huggingface dataset:
Theorem: SubMulAction.ofFixingSubgroupEmpty_equivariantMap_bijective
Proof state before:
case right
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
⊢ Function.Surjective ⇑(ofFixingSubgroupEmpty_equivariantMap M α)
Tactic:
intro x
Proof state after:
case right
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
x : α
⊢ ∃ a, (ofFixingSubgroupEmpty_equivariantMap M α) a = x
Theorem: SubMulAction.ofFixingSubgroupEmpty_equivariantMap_bijective
Proof state before:
case right
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
x : α
⊢ ∃ a, (ofFixingSubgroupEmpty_equivariantMap M α) a = x
Tactic:
use ⟨x, (SubMulAction.mem_ofFixingSubgroup_iff M).mp (Set.not_mem_empty x)⟩
Proof state after:
case h
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
x : α
⊢ (ofFixingSubgroupEmpty_equivariantMap M α) { val := x, property := ⋯ } = x
Theorem: SubMulAction.ofFixingSubgroupEmpty_equivariantMap_bijective
Proof state before:
case h
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
x : α
⊢ (ofFixingSubgroupEmpty_equivariantMap M α) { val := x, property := ⋯ } = x
Tactic:
rfl
Proof state after:
no goals
Theorem: SubMulAction.of_fixingSubgroupEmpty_mapScalars_surjective
Proof state before:
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
⊢ Function.Surjective ⇑(Subgroup.subtype (fixingSubgroup M ∅))
Tactic:
intro g
Proof state after:
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
g : M
⊢ ∃ a, (Subgroup.subtype (fixingSubgroup M ∅)) a = g
Theorem: SubMulAction.of_fixingSubgroupEmpty_mapScalars_surjective
Proof state before:
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
g : M
⊢ ∃ a, (Subgroup.subtype (fixingSubgroup M ∅)) a = g
Tactic:
suffices g ∈ fixingSubgroup M (∅ : Set α) by
  exact ⟨⟨g, this⟩, rfl⟩
Proof state after:
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
g : M
⊢ g ∈ fixingSubgroup M ∅
Theorem: SubMulAction.of_fixingSubgroupEmpty_mapScalars_surjective
Proof state before:
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
g : M
⊢ g ∈ fixingSubgroup M ∅
Tactic:
rw [mem_fixingSubgroup_iff]
Proof state after:
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
g : M
⊢ ∀ y ∈ ∅, g • y = y
Theorem: SubMulAction.of_fixingSubgroupEmpty_mapScalars_surjective
Proof state before:
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
g : M
⊢ ∀ y ∈ ∅, g • y = y
Tactic:
simp only [Set.mem_empty_iff_false, IsEmpty.forall_iff, implies_true]
Proof state after:
no goals
Theorem: SubMulAction.of_fixingSubgroupEmpty_mapScalars_surjective
Proof state before:
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
g : M
this : g ∈ fixingSubgroup M ∅
⊢ ∃ a, (Subgroup.subtype (fixingSubgroup M ∅)) a = g
Tactic:
exact ⟨⟨g, this⟩, rfl⟩
Proof state after:
no goals
Theorem: SubMulAction.equivariantMap_ofFixingSubgroup_to_ofStabilizer_coe
Proof state before:
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
x : α
hx : x ∈ ofFixingSubgroup M (insert a (Subtype.val '' s))
⊢ ↑↑((equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) { val := x, property := hx }) = x
Tactic:
rfl
Proof state after:
no goals
Theorem: SubMulAction.equivariantMap_ofFixingSubgroup_to_ofStabilizer_bijective
Proof state before:
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
⊢ Function.Bijective ⇑(equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s)
Tactic:
constructor
Proof state after:
case left
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
⊢ Function.Injective ⇑(equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s)

case right
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
⊢ Function.Surjective ⇑(equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s)
Theorem: SubMulAction.equivariantMap_ofFixingSubgroup_to_ofStabilizer_bijective
Proof state before:
case left
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
⊢ Function.Injective ⇑(equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s)
Tactic:
rintro ⟨x, hx⟩ ⟨y, hy⟩ h
Proof state after:
case left.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
x : α
hx : x ∈ ofFixingSubgroup M (insert a (Subtype.val '' s))
y : α
hy : y ∈ ofFixingSubgroup M (insert a (Subtype.val '' s))
h :
  (equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) { val := x, property := hx } =
    (equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) { val := y, property := hy }
⊢ { val := x, property := hx } = { val := y, property := hy }
Theorem: SubMulAction.equivariantMap_ofFixingSubgroup_to_ofStabilizer_bijective
Proof state before:
case left.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
x : α
hx : x ∈ ofFixingSubgroup M (insert a (Subtype.val '' s))
y : α
hy : y ∈ ofFixingSubgroup M (insert a (Subtype.val '' s))
h :
  (equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) { val := x, property := hx } =
    (equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) { 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 : α
s : Set ↥(ofStabilizer M a)
x : α
hx : x ∈ ofFixingSubgroup M (insert a (Subtype.val '' s))
y : α
hy : y ∈ ofFixingSubgroup M (insert a (Subtype.val '' s))
h :
  (equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) { val := x, property := hx } =
    (equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) { val := y, property := hy }
⊢ x = y
Theorem: SubMulAction.equivariantMap_ofFixingSubgroup_to_ofStabilizer_bijective
Proof state before:
case left.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
x : α
hx : x ∈ ofFixingSubgroup M (insert a (Subtype.val '' s))
y : α
hy : y ∈ ofFixingSubgroup M (insert a (Subtype.val '' s))
h :
  (equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) { val := x, property := hx } =
    (equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) { val := y, property := hy }
⊢ x = y
Tactic:
rw [← SubMulAction.equivariantMap_ofFixingSubgroup_to_ofStabilizer_coe M hx]
Proof state after:
case left.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
x : α
hx : x ∈ ofFixingSubgroup M (insert a (Subtype.val '' s))
y : α
hy : y ∈ ofFixingSubgroup M (insert a (Subtype.val '' s))
h :
  (equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) { val := x, property := hx } =
    (equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) { val := y, property := hy }
⊢ ↑↑((equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) { val := x, property := hx }) = y
Theorem: SubMulAction.equivariantMap_ofFixingSubgroup_to_ofStabilizer_bijective
Proof state before:
case left.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
x : α
hx : x ∈ ofFixingSubgroup M (insert a (Subtype.val '' s))
y : α
hy : y ∈ ofFixingSubgroup M (insert a (Subtype.val '' s))
h :
  (equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) { val := x, property := hx } =
    (equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) { val := y, property := hy }
⊢ ↑↑((equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) { val := x, property := hx }) = y
Tactic:
rw [← SubMulAction.equivariantMap_ofFixingSubgroup_to_ofStabilizer_coe M hy]
Proof state after:
case left.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
x : α
hx : x ∈ ofFixingSubgroup M (insert a (Subtype.val '' s))
y : α
hy : y ∈ ofFixingSubgroup M (insert a (Subtype.val '' s))
h :
  (equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) { val := x, property := hx } =
    (equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) { val := y, property := hy }
⊢ ↑↑((equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) { val := x, property := hx }) =
    ↑↑((equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) { val := y, property := hy })
Theorem: SubMulAction.equivariantMap_ofFixingSubgroup_to_ofStabilizer_bijective
Proof state before:
case left.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
x : α
hx : x ∈ ofFixingSubgroup M (insert a (Subtype.val '' s))
y : α
hy : y ∈ ofFixingSubgroup M (insert a (Subtype.val '' s))
h :
  (equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) { val := x, property := hx } =
    (equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) { val := y, property := hy }
⊢ ↑↑((equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) { val := x, property := hx }) =
    ↑↑((equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) { val := y, property := hy })
Tactic:
rw [h]
Proof state after:
no goals
Theorem: SubMulAction.equivariantMap_ofFixingSubgroup_to_ofStabilizer_bijective
Proof state before:
case right
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
⊢ Function.Surjective ⇑(equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s)
Tactic:
rintro ⟨⟨x, hx1⟩, hx2⟩
Proof state after:
case right.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
x : α
hx1 : x ∈ ofStabilizer M a
hx2 : { val := x, property := hx1 } ∈ ofFixingSubgroup (↥(stabilizer M a)) s
⊢ ∃ a_1,
    (equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) a_1 =
      { val := { val := x, property := hx1 }, property := hx2 }
Theorem: SubMulAction.equivariantMap_ofFixingSubgroup_to_ofStabilizer_bijective
Proof state before:
case right.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
x : α
hx1 : x ∈ ofStabilizer M a
hx2 : { val := x, property := hx1 } ∈ ofFixingSubgroup (↥(stabilizer M a)) s
⊢ ∃ a_1,
    (equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) a_1 =
      { val := { val := x, property := hx1 }, property := hx2 }
Tactic:
refine' ⟨⟨x, _⟩, rfl⟩
Proof state after:
case right.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
x : α
hx1 : x ∈ ofStabilizer M a
hx2 : { val := x, property := hx1 } ∈ ofFixingSubgroup (↥(stabilizer M a)) s
⊢ x ∈ ofFixingSubgroup M (insert a (Subtype.val '' s))
Theorem: SubMulAction.equivariantMap_ofFixingSubgroup_to_ofStabilizer_bijective
Proof state before:
case right.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
x : α
hx1 : x ∈ ofStabilizer M a
hx2 : { val := x, property := hx1 } ∈ ofFixingSubgroup (↥(stabilizer M a)) s
⊢ x ∈ ofFixingSubgroup M (insert a (Subtype.val '' s))
Tactic:
rw [SubMulAction.mem_ofFixingSubgroup_iff]
Proof state after:
case right.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
x : α
hx1 : x ∈ ofStabilizer M a
hx2 : { val := x, property := hx1 } ∈ ofFixingSubgroup (↥(stabilizer M a)) s
⊢ x ∉ insert a (Subtype.val '' s)
Theorem: SubMulAction.equivariantMap_ofFixingSubgroup_to_ofStabilizer_bijective
Proof state before:
case right.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
x : α
hx1 : x ∈ ofStabilizer M a
hx2 : { val := x, property := hx1 } ∈ ofFixingSubgroup (↥(stabilizer M a)) s
⊢ x ∉ insert a (Subtype.val '' s)
Tactic:
intro h
Proof state after:
case right.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
x : α
hx1 : x ∈ ofStabilizer M a
hx2 : { val := x, property := hx1 } ∈ ofFixingSubgroup (↥(stabilizer M a)) s
h : x ∈ insert a (Subtype.val '' s)
⊢ False
Theorem: SubMulAction.equivariantMap_ofFixingSubgroup_to_ofStabilizer_bijective
Proof state before:
case right.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
x : α
hx1 : x ∈ ofStabilizer M a
hx2 : { val := x, property := hx1 } ∈ ofFixingSubgroup (↥(stabilizer M a)) s
h : x ∈ insert a (Subtype.val '' s)
⊢ False
Tactic:
cases Set.mem_insert_iff.mp h with
| inl h' => rw [SubMulAction.mem_ofStabilizer_iff] at hx1 ; exact hx1 h'
| inr h' =>
rw [SubMulAction.mem_ofFixingSubgroup_iff] at hx2
apply hx2
obtain ⟨x1, hx1', rfl⟩ := h'
simp only [SetLike.eta]
exact hx1'
Proof state after:
no goals
Theorem: SubMulAction.equivariantMap_ofFixingSubgroup_to_ofStabilizer_bijective
Proof state before:
case right.mk.mk.inl
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
x : α
hx1 : x ∈ ofStabilizer M a
hx2 : { val := x, property := hx1 } ∈ ofFixingSubgroup (↥(stabilizer M a)) s
h : x ∈ insert a (Subtype.val '' s)
h' : x = a
⊢ False
Tactic:
rw [SubMulAction.mem_ofStabilizer_iff] at hx1
Proof state after:
case right.mk.mk.inl
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
x : α
hx1✝ : x ∈ ofStabilizer M a
hx1 : x ≠ a
hx2 : { val := x, property := hx1✝ } ∈ ofFixingSubgroup (↥(stabilizer M a)) s
h : x ∈ insert a (Subtype.val '' s)
h' : x = a
⊢ False
Theorem: SubMulAction.equivariantMap_ofFixingSubgroup_to_ofStabilizer_bijective
Proof state before:
case right.mk.mk.inl
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
x : α
hx1✝ : x ∈ ofStabilizer M a
hx1 : x ≠ a
hx2 : { val := x, property := hx1✝ } ∈ ofFixingSubgroup (↥(stabilizer M a)) s
h : x ∈ insert a (Subtype.val '' s)
h' : x = a
⊢ False
Tactic:
exact hx1 h'
Proof state after:
no goals
Theorem: SubMulAction.equivariantMap_ofFixingSubgroup_to_ofStabilizer_bijective
Proof state before:
case right.mk.mk.inr
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
x : α
hx1 : x ∈ ofStabilizer M a
hx2 : { val := x, property := hx1 } ∈ ofFixingSubgroup (↥(stabilizer M a)) s
h : x ∈ insert a (Subtype.val '' s)
h' : x ∈ Subtype.val '' s
⊢ False
Tactic:
rw [SubMulAction.mem_ofFixingSubgroup_iff] at hx2
Proof state after:
case right.mk.mk.inr
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
x : α
hx1 : x ∈ ofStabilizer M a
hx2 : { val := x, property := hx1 } ∉ s
h : x ∈ insert a (Subtype.val '' s)
h' : x ∈ Subtype.val '' s
⊢ False
Theorem: SubMulAction.equivariantMap_ofFixingSubgroup_to_ofStabilizer_bijective
Proof state before:
case right.mk.mk.inr
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
x : α
hx1 : x ∈ ofStabilizer M a
hx2 : { val := x, property := hx1 } ∉ s
h : x ∈ insert a (Subtype.val '' s)
h' : x ∈ Subtype.val '' s
⊢ False
Tactic:
apply hx2
Proof state after:
case right.mk.mk.inr
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
x : α
hx1 : x ∈ ofStabilizer M a
hx2 : { val := x, property := hx1 } ∉ s
h : x ∈ insert a (Subtype.val '' s)
h' : x ∈ Subtype.val '' s
⊢ { val := x, property := hx1 } ∈ s
Theorem: SubMulAction.equivariantMap_ofFixingSubgroup_to_ofStabilizer_bijective
Proof state before:
case right.mk.mk.inr
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
x : α
hx1 : x ∈ ofStabilizer M a
hx2 : { val := x, property := hx1 } ∉ s
h : x ∈ insert a (Subtype.val '' s)
h' : x ∈ Subtype.val '' s
⊢ { val := x, property := hx1 } ∈ s
Tactic:
obtain ⟨x1, hx1', rfl⟩ := h'
Proof state after:
case right.mk.mk.inr.intro.intro
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
x1 : ↥(ofStabilizer M a)
hx1' : x1 ∈ s
hx1 : ↑x1 ∈ ofStabilizer M a
hx2 : { val := ↑x1, property := hx1 } ∉ s
h : ↑x1 ∈ insert a (Subtype.val '' s)
⊢ { val := ↑x1, property := hx1 } ∈ s
Theorem: SubMulAction.equivariantMap_ofFixingSubgroup_to_ofStabilizer_bijective
Proof state before:
case right.mk.mk.inr.intro.intro
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
x1 : ↥(ofStabilizer M a)
hx1' : x1 ∈ s
hx1 : ↑x1 ∈ ofStabilizer M a
hx2 : { val := ↑x1, property := hx1 } ∉ s
h : ↑x1 ∈ insert a (Subtype.val '' s)
⊢ { val := ↑x1, property := hx1 } ∈ s
Tactic:
simp only [SetLike.eta]
Proof state after:
case right.mk.mk.inr.intro.intro
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
x1 : ↥(ofStabilizer M a)
hx1' : x1 ∈ s
hx1 : ↑x1 ∈ ofStabilizer M a
hx2 : { val := ↑x1, property := hx1 } ∉ s
h : ↑x1 ∈ insert a (Subtype.val '' s)
⊢ x1 ∈ s
Theorem: SubMulAction.equivariantMap_ofFixingSubgroup_to_ofStabilizer_bijective
Proof state before:
case right.mk.mk.inr.intro.intro
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
x1 : ↥(ofStabilizer M a)
hx1' : x1 ∈ s
hx1 : ↑x1 ∈ ofStabilizer M a
hx2 : { val := ↑x1, property := hx1 } ∉ s
h : ↑x1 ∈ insert a (Subtype.val '' s)
⊢ x1 ∈ s
Tactic:
exact hx1'
Proof state after:
no goals
Theorem: SubMulAction.scalarMap_ofFixingSubgroupOfStabilizer_bijective
Proof state before:
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
⊢ Function.Bijective (MulActionHom.toMap (equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s))
Tactic:
constructor
Proof state after:
case left
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
⊢ Function.Injective (MulActionHom.toMap (equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s))

case right
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
⊢ Function.Surjective (MulActionHom.toMap (equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s))
Theorem: SubMulAction.scalarMap_ofFixingSubgroupOfStabilizer_bijective
Proof state before:
case left
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
⊢ Function.Injective (MulActionHom.toMap (equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s))
Tactic:
rintro ⟨m, hm⟩ ⟨n, hn⟩ hmn
Proof state after:
case left.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
m : M
hm : m ∈ fixingSubgroup M (insert a (Subtype.val '' s))
n : M
hn : n ∈ fixingSubgroup M (insert a (Subtype.val '' s))
hmn :
  MulActionHom.toMap (equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) { val := m, property := hm } =
    MulActionHom.toMap (equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) { val := n, property := hn }
⊢ { val := m, property := hm } = { val := n, property := hn }
Theorem: SubMulAction.scalarMap_ofFixingSubgroupOfStabilizer_bijective
Proof state before:
case left.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
m : M
hm : m ∈ fixingSubgroup M (insert a (Subtype.val '' s))
n : M
hn : n ∈ fixingSubgroup M (insert a (Subtype.val '' s))
hmn :
  MulActionHom.toMap (equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) { val := m, property := hm } =
    MulActionHom.toMap (equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) { val := n, property := hn }
⊢ { val := m, property := hm } = { val := n, property := hn }
Tactic:
rw [← SetLike.coe_eq_coe, ← SetLike.coe_eq_coe] at hmn
Proof state after:
case left.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
m : M
hm : m ∈ fixingSubgroup M (insert a (Subtype.val '' s))
n : M
hn : n ∈ fixingSubgroup M (insert a (Subtype.val '' s))
hmn :
  ↑↑(MulActionHom.toMap (equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) { val := m, property := hm }) =
    ↑↑(MulActionHom.toMap (equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) { val := n, property := hn })
⊢ { val := m, property := hm } = { val := n, property := hn }
Theorem: SubMulAction.scalarMap_ofFixingSubgroupOfStabilizer_bijective
Proof state before:
case left.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
m : M
hm : m ∈ fixingSubgroup M (insert a (Subtype.val '' s))
n : M
hn : n ∈ fixingSubgroup M (insert a (Subtype.val '' s))
hmn :
  ↑↑(MulActionHom.toMap (equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) { val := m, property := hm }) =
    ↑↑(MulActionHom.toMap (equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) { val := n, property := hn })
⊢ { val := m, property := hm } = { val := n, property := hn }
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 : α
s : Set ↥(ofStabilizer M a)
m : M
hm : m ∈ fixingSubgroup M (insert a (Subtype.val '' s))
n : M
hn : n ∈ fixingSubgroup M (insert a (Subtype.val '' s))
hmn :
  ↑↑(MulActionHom.toMap (equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) { val := m, property := hm }) =
    ↑↑(MulActionHom.toMap (equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) { val := n, property := hn })
⊢ m = n
Theorem: SubMulAction.scalarMap_ofFixingSubgroupOfStabilizer_bijective
Proof state before:
case left.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
m : M
hm : m ∈ fixingSubgroup M (insert a (Subtype.val '' s))
n : M
hn : n ∈ fixingSubgroup M (insert a (Subtype.val '' s))
hmn :
  ↑↑(MulActionHom.toMap (equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) { val := m, property := hm }) =
    ↑↑(MulActionHom.toMap (equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) { val := n, property := hn })
⊢ m = n
Tactic:
exact hmn
Proof state after:
no goals
Theorem: SubMulAction.scalarMap_ofFixingSubgroupOfStabilizer_bijective
Proof state before:
case right
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
⊢ Function.Surjective (MulActionHom.toMap (equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s))
Tactic:
rintro ⟨⟨m, hm⟩, hm'⟩
Proof state after:
case right.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
m : M
hm : m ∈ stabilizer M a
hm' : { val := m, property := hm } ∈ fixingSubgroup (↥(stabilizer M a)) s
⊢ ∃ a_1,
    MulActionHom.toMap (equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) a_1 =
      { val := { val := m, property := hm }, property := hm' }
Theorem: SubMulAction.scalarMap_ofFixingSubgroupOfStabilizer_bijective
Proof state before:
case right.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
m : M
hm : m ∈ stabilizer M a
hm' : { val := m, property := hm } ∈ fixingSubgroup (↥(stabilizer M a)) s
⊢ ∃ a_1,
    MulActionHom.toMap (equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) a_1 =
      { val := { val := m, property := hm }, property := hm' }
Tactic:
suffices m ∈ fixingSubgroup M (insert a (Subtype.val '' s)) by
  use ⟨m, this⟩
  rfl
Proof state after:
case right.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
m : M
hm : m ∈ stabilizer M a
hm' : { val := m, property := hm } ∈ fixingSubgroup (↥(stabilizer M a)) s
⊢ m ∈ fixingSubgroup M (insert a (Subtype.val '' s))
Theorem: SubMulAction.scalarMap_ofFixingSubgroupOfStabilizer_bijective
Proof state before:
case right.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
m : M
hm : m ∈ stabilizer M a
hm' : { val := m, property := hm } ∈ fixingSubgroup (↥(stabilizer M a)) s
⊢ m ∈ fixingSubgroup M (insert a (Subtype.val '' s))
Tactic:
rw [mem_fixingSubgroup_iff]
Proof state after:
case right.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
m : M
hm : m ∈ stabilizer M a
hm' : { val := m, property := hm } ∈ fixingSubgroup (↥(stabilizer M a)) s
⊢ ∀ y ∈ insert a (Subtype.val '' s), m • y = y