awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.WithTop.Untop0 (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : PartialOrder α
b : WithTop α
hb : b ≠ ⊤
a : α
⊢ (↑a : WithTop α).untop₀ ≤ b.untop₀ ↔ (↑a : WithTop α) ≤ b
have lift : ∀ (b : α), (↑a : WithTop α).untop₀ ≤ (↑b : WithTop α).untop₀ ↔ (↑a : WithTop α) ≤ (↑b : WithTop α)
Tactic: lift b to α using hb
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.Algebra.Order.WithTop.Untop0 (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
a b : WithTop α
ha : a ≠ ⊤
hb : b ≠ ⊤
⊢ (max a b).untop₀ = max a.untop₀ b.untop₀
have lift : ∀ (a : α), (max (↑a : WithTop α) b).untop₀ = max (↑a : WithTop α).untop₀ b.untop₀
Tactic: lift a to α using ha
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Algebra.Order.WithTop.Untop0 (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
b : WithTop α
hb : b ≠ ⊤
a : α
⊢ (max (↑a : WithTop α) b).untop₀ = max (↑a : WithTop α).untop₀ b.untop₀
have lift : ∀ (b : α), (max (↑a : WithTop α) (↑b : WithTop α)).untop₀ = max (↑a : WithTop α).untop₀ (↑b : WithTop α).untop₀
Tactic: lift b to α using hb
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.Algebra.Order.WithTop.Untop0 (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
a b : α
⊢ (max (↑a : WithTop α) (↑b : WithTop α)).untop₀ = max (↑a : WithTop α).untop₀ (↑b : WithTop α).untop₀
have simp : (max (↑a : WithTop α) (↑b : WithTop α)).untop₀ = max a b
Tactic: simp only [untop₀_coe]
-- Lean 4 proof step from Mathlib.Algebra.Order.WithTop.Untop0 (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
a b : α
⊢ (max (↑a : WithTop α) (↑b : WithTop α)).untop₀ = max a b
have pos : ∀ (h : a ≤ b), (max (↑a : WithTop α) (↑b : WithTop α)).untop₀ = max a b
Tactic: by_cases h : a ≤ b
-- Lean 4 proof step from Mathlib.Algebra.Order.WithTop.Untop0 (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
a b : α
pos : ∀ (h : a ≤ b), (max (↑a : WithTop α) (↑b : WithTop α)).untop₀ = max a b
⊢ (max (↑a : WithTop α) (↑b : WithTop α)).untop₀ = max a b
have neg : ∀ (h : ¬a ≤ b), (max (↑a : WithTop α) (↑b : WithTop α)).untop₀ = max a b
Tactic: by_cases h : a ≤ b
-- Lean 4 proof step from Mathlib.Algebra.Order.WithTop.Untop0 (hypothesis)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
a b : α
h : ¬a ≤ b
⊢ (max (↑a : WithTop α) (↑b : WithTop α)).untop₀ = max a b
have h₁ : b < a
Tactic: rw [not_le] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.WithTop.Untop0 (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
a b : WithTop α
ha : a ≠ ⊤
hb : b ≠ ⊤
⊢ (min a b).untop₀ = min a.untop₀ b.untop₀
have lift : ∀ (a : α), (min (↑a : WithTop α) b).untop₀ = min (↑a : WithTop α).untop₀ b.untop₀
Tactic: lift a to α using ha
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Algebra.Order.WithTop.Untop0 (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
b : WithTop α
hb : b ≠ ⊤
a : α
⊢ (min (↑a : WithTop α) b).untop₀ = min (↑a : WithTop α).untop₀ b.untop₀
have lift : ∀ (b : α), (min (↑a : WithTop α) (↑b : WithTop α)).untop₀ = min (↑a : WithTop α).untop₀ (↑b : WithTop α).untop₀
Tactic: lift b to α using hb
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.Algebra.Order.WithTop.Untop0 (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
a b : α
⊢ (min (↑a : WithTop α) (↑b : WithTop α)).untop₀ = min (↑a : WithTop α).untop₀ (↑b : WithTop α).untop₀
have norm_cast : (↑(min a b) : WithTop α).untop₀ = min (↑a : WithTop α).untop₀ (↑b : WithTop α).untop₀
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Algebra.Pointwise.Stabilizer (goal)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
⊢ Eq (α := Subgroup G) (stabilizer.{u_1, u_3} G (α := Set α) univ) ⊤
have h : ∀ (x : G),
  Membership.mem (γ := Subgroup G) (stabilizer.{u_1, u_3} G (α := Set α) univ) x ↔ Membership.mem (γ := Subgroup G) ⊤ x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Pointwise.Stabilizer (goal)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
b : α
⊢ Eq (α := Subgroup G) (stabilizer G (α := Set α) {b}) (stabilizer G b)
have h : ∀ (x : G),
  Membership.mem (γ := Subgroup G) (stabilizer G (α := Set α) {b}) x ↔
    Membership.mem (γ := Subgroup G) (stabilizer G b) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Pointwise.Stabilizer (goal)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
a : G
s : Set α
⊢ Membership.mem (γ := Subgroup G) (stabilizer G s) a ↔ ∀ (b : α), a • b ∈ s ↔ b ∈ s
have refine_1 : ∀ (h : a • s = s) (b : α), a • b ∈ s ↔ b ∈ s
Tactic: refine mem_stabilizer_iff.trans ⟨fun h b ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Pointwise.Stabilizer (goal)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
a : G
s : Set α
refine_1 : ∀ (h : a • s = s) (b : α), a • b ∈ s ↔ b ∈ s
⊢ Membership.mem (γ := Subgroup G) (stabilizer G s) a ↔ ∀ (b : α), a • b ∈ s ↔ b ∈ s
have refine_2 : ∀ (h : ∀ (b : α), a • b ∈ s ↔ b ∈ s), a • s = s
Tactic: refine mem_stabilizer_iff.trans ⟨fun h b ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Pointwise.Stabilizer (goal)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
a : G
s : Set α
h : a • s = s
b : α
⊢ a • b ∈ s ↔ b ∈ s
have refine_1 : a • b ∈ s ↔ a • b ∈ a • s
Tactic: rw [← (smul_mem_smul_set_iff : a • b ∈ _ ↔ _), h]
-- Lean 4 proof step from Mathlib.Algebra.Pointwise.Stabilizer (goal)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
a : G
s : Set α
h : a • s = s
b : α
refine_1 : a • b ∈ s ↔ a • b ∈ a • s
⊢ a • b ∈ s ↔ b ∈ s
have refine_1₁ : a • b ∈ s ↔ a • b ∈ s
Tactic: rw [← (smul_mem_smul_set_iff : a • b ∈ _ ↔ _), h]
-- Lean 4 proof step from Mathlib.Algebra.Pointwise.Stabilizer (goal)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
a : G
s : Set α
h : ∀ (b : α), a • b ∈ s ↔ b ∈ s
⊢ a • s = s
have refine_2 : ∀ (x : α), a⁻¹ • x ∈ s ↔ x ∈ s
Tactic: simp_rw [Set.ext_iff, mem_smul_set_iff_inv_smul_mem]
-- Lean 4 proof step from Mathlib.Algebra.Pointwise.Stabilizer (goal)
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
f : G →* H
s : Set G
a : H
⊢ a ∈ Subgroup.map f (stabilizer G s) →
    Membership.mem (γ := Subgroup H) (stabilizer H (α := Set H) ((⇑f : (a : G) → H) '' s)) a
have simp : ∀ (x : G),
  x • s = s → (f : (a : G) → H) x = a → HSMul.hSMul (β := Set H) a ((⇑f : (a : G) → H) '' s) = (⇑f : (a : G) → H) '' s
Tactic: simp only [Subgroup.mem_map, mem_stabilizer_iff, forall_exists_index, and_imp]
-- Lean 4 proof step from Mathlib.Algebra.Pointwise.Stabilizer (goal)
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
f : G →* H
s : Set G
a : G
ha : a • s = s
⊢ HSMul.hSMul (α := H) (β := Set H) ((f : (a : G) → H) a : H) ((⇑f : (a : G) → H) '' s) = (⇑f : (a : G) → H) '' s
have rw : Eq.{u_2 + 1} (α := Set H) ((⇑f : (a : G) → H) '' (a • s)) ((⇑f : (a : G) → H) '' s)
Tactic: rw [← image_smul_distrib, ha]
-- Lean 4 proof step from Mathlib.Algebra.Pointwise.Stabilizer (goal)
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
f : G →* H
s : Set G
a : G
ha : a • s = s
rw : Eq.{u_2 + 1} (α := Set H) ((⇑f : (a : G) → H) '' (a • s)) ((⇑f : (a : G) → H) '' s)
⊢ HSMul.hSMul (α := H) (β := Set H) ((f : (a : G) → H) a : H) ((⇑f : (a : G) → H) '' s) = (⇑f : (a : G) → H) '' s
have rw₁ : Eq.{u_2 + 1} (α := Set H) ((⇑f : (a : G) → H) '' s) ((⇑f : (a : G) → H) '' s)
Tactic: rw [← image_smul_distrib, ha]
-- Lean 4 proof step from Mathlib.Algebra.Pointwise.Stabilizer (goal)
Goal:
G : Type u_1
inst : Group G
s : Set G
⊢ (↑(stabilizer G s) : Set G) * s = s
have h : ∀ (x : G), x ∈ (↑(stabilizer G s) : Set G) * s ↔ x ∈ s
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Pointwise.Stabilizer (goal)
Goal:
G : Type u_1
inst : Group G
s : Set G
x : G
⊢ x ∈ (↑(stabilizer G s) : Set G) * s ↔ x ∈ s
have h : x ∈ (↑(stabilizer G s) : Set G) * s → x ∈ s
Tactic: refine ⟨?_, fun h ↦ ⟨_, (stabilizer G s).one_mem, _, h, one_mul _⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Pointwise.Stabilizer (goal)
Goal:
G : Type u_1
inst : Group G
s : Set G
a : G
ha : a ∈ (↑(stabilizer G s) : Set G)
b : G
hb : b ∈ s
⊢ (fun (x1 x2 : G) ↦ x1 * x2) a b ∈ s
have h : (fun (x1 x2 : G) ↦ x1 * x2) a b ∈ a • s
Tactic: rw [← mem_stabilizer_iff.1 ha]
-- Lean 4 proof step from Mathlib.Algebra.Pointwise.Stabilizer (goal)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
s t : Set α
hdisj : Disjoint s t
hstab : LE.le (α := Subgroup G) (stabilizer G s) (stabilizer G t)
hstab_union : LE.le (α := Subgroup G) (stabilizer G (s ∪ t)) (stabilizer G t)
⊢ Eq (α := Subgroup G) (stabilizer G (s ∪ t)) (stabilizer G s)
have refine_1 : LE.le (α := Subgroup G) (stabilizer G (s ∪ t)) (stabilizer G s)
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Pointwise.Stabilizer (goal)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
s t : Set α
hdisj : Disjoint s t
hstab : LE.le (α := Subgroup G) (stabilizer G s) (stabilizer G t)
hstab_union : LE.le (α := Subgroup G) (stabilizer G (s ∪ t)) (stabilizer G t)
refine_1 : LE.le (α := Subgroup G) (stabilizer G (s ∪ t)) (stabilizer G s)
⊢ Eq (α := Subgroup G) (stabilizer G (s ∪ t)) (stabilizer G s)
have refine_2 : LE.le (α := Subgroup G) (stabilizer G s) (stabilizer G (s ∪ t))
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Pointwise.Stabilizer (goal)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
s t : Set α
hdisj : Disjoint s t
hstab : LE.le (α := Subgroup G) (stabilizer G s) (stabilizer G t)
hstab_union : LE.le (α := Subgroup G) (stabilizer G (s ∪ t)) (stabilizer G t)
⊢ Eq (α := Subgroup G) (stabilizer G ((s ∪ t) \ t)) (stabilizer G s)
have rw : s ∩ t ⊆ ∅
Tactic: rw [union_diff_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Pointwise.Stabilizer (goal)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
s t : Set α
hdisj : Disjoint s t
hstab : LE.le (α := Subgroup G) (stabilizer G s) (stabilizer G t)
hstab_union : LE.le (α := Subgroup G) (stabilizer G (s ∪ t)) (stabilizer G t)
⊢ LE.le (α := Subgroup G) (stabilizer G (s ∪ t)) (stabilizer G s)
have stabilizer : LE.le (α := Subgroup G) (stabilizer G (s ∪ t)) (stabilizer G (s ∪ t) ⊓ stabilizer G t)
Tactic: calc
      stabilizer G (s ∪ t)
        ≤ stabilizer G (s ∪ t) ⊓ stabilizer G t := by simpa
      _ ≤ stabilizer G ((s ∪ t) \ t) := stabilizer_inf_stabilizer_le_stabilizer_sdiff
      _ = stabilizer G s := by rw [union_diff_cancel_right]; simpa [← disjoint_iff_inter_eq_empty]
-- Lean 4 proof step from Mathlib.Algebra.Pointwise.Stabilizer (goal)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
s t : Set α
hdisj : Disjoint s t
hstab : LE.le (α := Subgroup G) (MulAction.stabilizer G s) (MulAction.stabilizer G t)
hstab_union : LE.le (α := Subgroup G) (MulAction.stabilizer G (s ∪ t)) (MulAction.stabilizer G t)
stabilizer :
  LE.le (α := Subgroup G) (MulAction.stabilizer G (s ∪ t)) (MulAction.stabilizer G (s ∪ t) ⊓ MulAction.stabilizer G t)
⊢ LE.le (α := Subgroup G) (MulAction.stabilizer G (s ∪ t)) (MulAction.stabilizer G s)
have stabilizer₁ : Eq (α := Subgroup G) (MulAction.stabilizer G ((s ∪ t) \ t)) (MulAction.stabilizer G s)
Tactic: calc
      stabilizer G (s ∪ t)
        ≤ stabilizer G (s ∪ t) ⊓ stabilizer G t := by simpa
      _ ≤ stabilizer G ((s ∪ t) \ t) := stabilizer_inf_stabilizer_le_stabilizer_sdiff
      _ = stabilizer G s := by rw [union_diff_cancel_right]; simpa [← disjoint_iff_inter_eq_empty]
-- Lean 4 proof step from Mathlib.Algebra.Pointwise.Stabilizer (goal)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
s t : Set α
hdisj : Disjoint s t
hstab : LE.le (α := Subgroup G) (stabilizer G s) (stabilizer G t)
hstab_union : LE.le (α := Subgroup G) (stabilizer G (s ∪ t)) (stabilizer G t)
⊢ LE.le (α := Subgroup G) (stabilizer G s) (stabilizer G (s ∪ t))
have stabilizer : LE.le (α := Subgroup G) (stabilizer G s) (stabilizer G s ⊓ stabilizer G t)
Tactic: calc
      stabilizer G s
        ≤ stabilizer G s ⊓ stabilizer G t := by simpa
      _ ≤ stabilizer G (s ∪ t) := stabilizer_inf_stabilizer_le_stabilizer_union
-- Lean 4 proof step from Mathlib.Algebra.Pointwise.Stabilizer (goal)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
s t : Set α
hdisj : Disjoint s t
hstab : LE.le (α := Subgroup G) (stabilizer G t) (stabilizer G s)
hstab_union : LE.le (α := Subgroup G) (stabilizer G (s ∪ t)) (stabilizer G s)
⊢ Eq (α := Subgroup G) (stabilizer G (s ∪ t)) (stabilizer G t)
have rw : Eq (α := Subgroup G) (stabilizer G (t ∪ s)) (stabilizer G t)
Tactic: rw [union_comm, stabilizer_union_eq_left hdisj.symm hstab (union_comm .. ▸ hstab_union)]
-- Lean 4 proof step from Mathlib.Algebra.Pointwise.Stabilizer (goal)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
s t : Set α
hdisj : Disjoint s t
hstab : LE.le (α := Subgroup G) (stabilizer G t) (stabilizer G s)
hstab_union : LE.le (α := Subgroup G) (stabilizer G (s ∪ t)) (stabilizer G s)
rw : Eq (α := Subgroup G) (stabilizer G (t ∪ s)) (stabilizer G t)
⊢ Eq (α := Subgroup G) (stabilizer G (s ∪ t)) (stabilizer G t)
have rw₁ : Eq (α := Subgroup G) (stabilizer G t) (stabilizer G t)
Tactic: rw [union_comm, stabilizer_union_eq_left hdisj.symm hstab (union_comm .. ▸ hstab_union)]
-- Lean 4 proof step from Mathlib.Algebra.Pointwise.Stabilizer (goal)
Goal:
G : Type u_1
inst : Group G
a : G
s : Set G
ha : a ∈ s
b : G
hb : b ∈ (↑(stabilizer G s) : Set G)
⊢ b <• a ∈ s
have rw : b <• a ∈ b •> s
Tactic: rw [← hb]
-- Lean 4 proof step from Mathlib.Algebra.Pointwise.Stabilizer (goal)
Goal:
G : Type u_1
inst : Group G
a : G
s : Set G
ha : a ∈ s
b : G
hb : b ∈ (↑(stabilizer G s) : Set G)
⊢ b * a ∈ s
have rwa : b • a ∈ s
Tactic: rwa [← smul_eq_mul, mem_stabilizer_set.1 hb]
-- Lean 4 proof step from Mathlib.Algebra.Pointwise.Stabilizer (goal)
Goal:
G : Type u_1
inst : Group G
s : Set G
hs₀ : s.Nonempty
hs : s.Finite
⊢ (↑(stabilizer G s) : Set G).Finite
have obtain : ∀ (a : G) (ha : a ∈ s), (↑(stabilizer G s) : Set G).Finite
Tactic: obtain ⟨a, ha⟩ := hs₀
Cleared hypotheses: hs₀
-- Lean 4 proof step from Mathlib.Algebra.Pointwise.Stabilizer (goal)
Goal:
G : Type u_1
inst : Group G
s : Subgroup G
⊢ stabilizer G (↑s : Set G) = s
have simp_rw : ∀ (x : G), (∀ (b : G), x • b ∈ (↑s : Set G) ↔ b ∈ (↑s : Set G)) ↔ x ∈ s
Tactic: simp_rw [SetLike.ext_iff, mem_stabilizer_set]
-- Lean 4 proof step from Mathlib.Algebra.Pointwise.Stabilizer (goal)
Goal:
G : Type u_1
inst : Group G
s : Subgroup G
⊢ ∀ (x : G), (∀ (b : G), x • b ∈ (↑s : Set G) ↔ b ∈ (↑s : Set G)) ↔ x ∈ s
have refine : ∀ (a : G) (h : ∀ (b : G), a • b ∈ (↑s : Set G) ↔ b ∈ (↑s : Set G)), a ∈ s
Tactic: refine fun a ↦ ⟨fun h ↦ ?_, fun ha b ↦ s.mul_mem_cancel_left ha⟩
-- Lean 4 proof step from Mathlib.Algebra.Pointwise.Stabilizer (goal)
Goal:
G : Type u_1
inst : Group G
s : Subgroup G
⊢ stabilizer Gᵐᵒᵖ (↑s : Set G) = s.op
have simp_rw : ∀ (x : Gᵐᵒᵖ), (∀ (b : G), x • b ∈ (↑s : Set G) ↔ b ∈ (↑s : Set G)) ↔ x ∈ s.op
Tactic: simp_rw [SetLike.ext_iff, mem_stabilizer_set]
-- Lean 4 proof step from Mathlib.Algebra.Pointwise.Stabilizer (goal)
Goal:
G : Type u_1
inst : Group G
s : Subgroup G
⊢ ∀ (x : Gᵐᵒᵖ), (∀ (b : G), x • b ∈ (↑s : Set G) ↔ b ∈ (↑s : Set G)) ↔ x ∈ s.op
have simp : ∀ (a : G), (∀ (b : G), b * a ∈ s ↔ b ∈ s) ↔ a ∈ s
Tactic: simp only [smul_eq_mul_unop, SetLike.mem_coe, Subgroup.mem_op, «forall», unop_op]
-- Lean 4 proof step from Mathlib.Algebra.Pointwise.Stabilizer (goal)
Goal:
G : Type u_1
inst : Group G
s : Subgroup G
⊢ ∀ (a : G), (∀ (b : G), b * a ∈ s ↔ b ∈ s) ↔ a ∈ s
have refine : ∀ (a : G) (h : ∀ (b : G), b * a ∈ s ↔ b ∈ s), a ∈ s
Tactic: refine fun a ↦ ⟨fun h ↦ ?_, fun ha b ↦ s.mul_mem_cancel_right ha⟩
-- Lean 4 proof step from Mathlib.Algebra.Pointwise.Stabilizer (goal)
Goal:
G : Type u_1
inst : Group G
s : Subgroup Gᵐᵒᵖ
⊢ stabilizer G (↑s : Set Gᵐᵒᵖ) = s.unop
have simp_rw : ∀ (x : G), (∀ (b : Gᵐᵒᵖ), x • b ∈ (↑s : Set Gᵐᵒᵖ) ↔ b ∈ (↑s : Set Gᵐᵒᵖ)) ↔ x ∈ s.unop
Tactic: simp_rw [SetLike.ext_iff, mem_stabilizer_set]
-- Lean 4 proof step from Mathlib.Algebra.Pointwise.Stabilizer (goal)
Goal:
G : Type u_1
inst : Group G
s : Subgroup Gᵐᵒᵖ
⊢ ∀ (x : G), (∀ (b : Gᵐᵒᵖ), x • b ∈ (↑s : Set Gᵐᵒᵖ) ↔ b ∈ (↑s : Set Gᵐᵒᵖ)) ↔ x ∈ s.unop
have refine : ∀ (a : G) (h : ∀ (b : Gᵐᵒᵖ), a • b ∈ (↑s : Set Gᵐᵒᵖ) ↔ b ∈ (↑s : Set Gᵐᵒᵖ)), a ∈ s.unop
Tactic: refine fun a ↦ ⟨fun h ↦ ?_, fun ha b ↦ s.mul_mem_cancel_right ha⟩
-- Lean 4 proof step from Mathlib.Algebra.Pointwise.Stabilizer (hypothesis)
Goal:
G : Type u_1
inst : Group G
s : Subgroup Gᵐᵒᵖ
a : G
h : ∀ (b : Gᵐᵒᵖ), a • b ∈ (↑s : Set Gᵐᵒᵖ) ↔ b ∈ (↑s : Set Gᵐᵒᵖ)
⊢ a ∈ s.unop
have this : 1 * op a ∈ s
Tactic: have : 1 * MulOpposite.op a ∈ s := (h 1).2 s.one_mem
-- Lean 4 proof step from Mathlib.Algebra.Pointwise.Stabilizer (goal)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : DecidableEq α
s : Finset α
⊢ Eq (α := Subgroup G) (stabilizer G (↑s : Set α)) (stabilizer G s)
have h : ∀ (x : G),
  Membership.mem (γ := Subgroup G) (stabilizer G (↑s : Set α)) x ↔ Membership.mem (γ := Subgroup G) (stabilizer G s) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Pointwise.Stabilizer (goal)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : DecidableEq α
inst_3 : Fintype α
⊢ Eq (α := Subgroup G) (stabilizer.{u_1, u_3} G (α := Finset α) Finset.univ) ⊤
have h : ∀ (x : G),
  Membership.mem (γ := Subgroup G) (stabilizer.{u_1, u_3} G (α := Finset α) Finset.univ) x ↔
    Membership.mem (γ := Subgroup G) ⊤ x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Pointwise.Stabilizer (goal)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : DecidableEq α
b : α
⊢ Eq (α := Subgroup G) (stabilizer G (α := Finset α) {b}) (stabilizer G b)
have h : ∀ (x : G),
  Membership.mem (γ := Subgroup G) (stabilizer G (α := Finset α) {b}) x ↔
    Membership.mem (γ := Subgroup G) (stabilizer G b) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Pointwise.Stabilizer (goal)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
a : G
inst_2 : DecidableEq α
s : Finset α
⊢ Membership.mem (γ := Subgroup G) (stabilizer G s) a ↔ ∀ (b : α), a • b ∈ s ↔ b ∈ s
have simp_rw : Membership.mem (γ := Subgroup G) (stabilizer G (↑s : Set α)) a ↔ ∀ (b : α), a • b ∈ s ↔ b ∈ s
Tactic: simp_rw [← stabilizer_coe_finset, mem_stabilizer_set, Finset.mem_coe]
-- Lean 4 proof step from Mathlib.Algebra.Pointwise.Stabilizer (goal)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
a : G
inst_2 : DecidableEq α
s : Finset α
simp_rw : Membership.mem (γ := Subgroup G) (stabilizer G (↑s : Set α)) a ↔ ∀ (b : α), a • b ∈ s ↔ b ∈ s
⊢ Membership.mem (γ := Subgroup G) (stabilizer G s) a ↔ ∀ (b : α), a • b ∈ s ↔ b ∈ s
have simp_rw₁ : (∀ (b : α), a • b ∈ (↑s : Set α) ↔ b ∈ (↑s : Set α)) ↔ ∀ (b : α), a • b ∈ s ↔ b ∈ s
Tactic: simp_rw [← stabilizer_coe_finset, mem_stabilizer_set, Finset.mem_coe]
-- Lean 4 proof step from Mathlib.Algebra.Pointwise.Stabilizer (goal)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
a : G
inst_2 : DecidableEq α
s : Finset α
⊢ Membership.mem (γ := Subgroup G) (stabilizer G s) a ↔ s ⊆ a • s
have rw : a • s = s ↔ s ⊆ a • s
Tactic: rw [mem_stabilizer_iff, Finset.subset_iff_eq_of_card_le (Finset.card_smul_finset _ _).le, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.Pointwise.Stabilizer (goal)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
a : G
inst_2 : DecidableEq α
s : Finset α
rw : a • s = s ↔ s ⊆ a • s
⊢ Membership.mem (γ := Subgroup G) (stabilizer G s) a ↔ s ⊆ a • s
have rw₁ : a • s = s ↔ s = a • s
Tactic: rw [mem_stabilizer_iff, Finset.subset_iff_eq_of_card_le (Finset.card_smul_finset _ _).le, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.Pointwise.Stabilizer (goal)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
a : G
inst_2 : DecidableEq α
s : Finset α
rw : a • s = s ↔ s ⊆ a • s
rw₁ : a • s = s ↔ s = a • s
⊢ Membership.mem (γ := Subgroup G) (stabilizer G s) a ↔ s ⊆ a • s
have rw₂ : s = a • s ↔ s = a • s
Tactic: rw [mem_stabilizer_iff, Finset.subset_iff_eq_of_card_le (Finset.card_smul_finset _ _).le, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.Pointwise.Stabilizer (goal)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
a : G
inst_2 : DecidableEq α
s : Finset α
⊢ Membership.mem (γ := Subgroup G) (stabilizer G s) a ↔ a • s ⊆ s
have rw : a • s = s ↔ a • s ⊆ s
Tactic: rw [mem_stabilizer_iff, Finset.subset_iff_eq_of_card_le (Finset.card_smul_finset _ _).ge]
-- Lean 4 proof step from Mathlib.Algebra.Pointwise.Stabilizer (goal)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
a : G
inst_2 : DecidableEq α
s : Finset α
rw : a • s = s ↔ a • s ⊆ s
⊢ Membership.mem (γ := Subgroup G) (stabilizer G s) a ↔ a • s ⊆ s
have rw₁ : a • s = s ↔ a • s = s
Tactic: rw [mem_stabilizer_iff, Finset.subset_iff_eq_of_card_le (Finset.card_smul_finset _ _).ge]
-- Lean 4 proof step from Mathlib.Algebra.Pointwise.Stabilizer (goal)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
a : G
inst_2 : DecidableEq α
s : Finset α
⊢ Membership.mem (γ := Subgroup G) (stabilizer G s) a ↔ ∀ ⦃b : α⦄, b ∈ s → a • b ∈ s
have rw : s ⊆ a⁻¹ • s ↔ ∀ ⦃b : α⦄, b ∈ s → a • b ∈ s
Tactic: rw [← Subgroup.inv_mem_iff, mem_stabilizer_finset_iff_subset_smul_finset]
-- Lean 4 proof step from Mathlib.Algebra.Pointwise.Stabilizer (goal)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
a : G
inst_2 : DecidableEq α
s : Finset α
⊢ s ⊆ a⁻¹ • s ↔ ∀ ⦃b : α⦄, b ∈ s → a • b ∈ s
have simp_rw : s ⊆ a⁻¹ • s ↔ ∀ ⦃b : α⦄, b ∈ s → b ∈ a⁻¹ • s
Tactic: simp_rw [← Finset.mem_inv_smul_finset_iff, Finset.subset_iff]
-- Lean 4 proof step from Mathlib.Algebra.Pointwise.Stabilizer (goal)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
a : G
s : Set α
hs : s.Finite
⊢ Membership.mem (γ := Subgroup G) (stabilizer G s) a ↔ s ⊆ a • s
have lift : ∀ (s : Finset α), Membership.mem (γ := Subgroup G) (stabilizer G (↑s : Set α)) a ↔ (↑s : Set α) ⊆ a • (↑s : Set α)
Tactic: lift s to Finset α using hs
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Algebra.Pointwise.Stabilizer (goal)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
a : G
s : Finset α
⊢ Membership.mem (γ := Subgroup G) (stabilizer G (↑s : Set α)) a ↔ (↑s : Set α) ⊆ a • (↑s : Set α)
have rw : Membership.mem (γ := Subgroup G) (stabilizer G s) a ↔ (↑s : Set α) ⊆ a • (↑s : Set α)
Tactic: rw [stabilizer_coe_finset, mem_stabilizer_finset_iff_subset_smul_finset, ← Finset.coe_smul_finset,
    Finset.coe_subset]
-- Lean 4 proof step from Mathlib.Algebra.Pointwise.Stabilizer (goal)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
a : G
s : Finset α
rw : Membership.mem (γ := Subgroup G) (stabilizer G s) a ↔ (↑s : Set α) ⊆ a • (↑s : Set α)
⊢ Membership.mem (γ := Subgroup G) (stabilizer G (↑s : Set α)) a ↔ (↑s : Set α) ⊆ a • (↑s : Set α)
have rw₁ : s ⊆ a • s ↔ (↑s : Set α) ⊆ a • (↑s : Set α)
Tactic: rw [stabilizer_coe_finset, mem_stabilizer_finset_iff_subset_smul_finset, ← Finset.coe_smul_finset,
    Finset.coe_subset]
-- Lean 4 proof step from Mathlib.Algebra.Pointwise.Stabilizer (goal)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
a : G
s : Finset α
rw : Membership.mem (γ := Subgroup G) (stabilizer G s) a ↔ (↑s : Set α) ⊆ a • (↑s : Set α)
rw₁ : s ⊆ a • s ↔ (↑s : Set α) ⊆ a • (↑s : Set α)
⊢ Membership.mem (γ := Subgroup G) (stabilizer G (↑s : Set α)) a ↔ (↑s : Set α) ⊆ a • (↑s : Set α)
have rw₂ : s ⊆ a • s ↔ (↑s : Set α) ⊆ (↑(a • s) : Set α)
Tactic: rw [stabilizer_coe_finset, mem_stabilizer_finset_iff_subset_smul_finset, ← Finset.coe_smul_finset,
    Finset.coe_subset]