awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
G : Type u_1
inst : Group G
a b : G
⊢ a * (a⁻¹ * b) = b
have rw : a * a⁻¹ * b = b
Tactic: rw [← mul_assoc, mul_inv_cancel, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
G : Type u_1
inst : Group G
a b : G
rw : a * a⁻¹ * b = b
⊢ a * (a⁻¹ * b) = b
have rw₁ : 1 * b = b
Tactic: rw [← mul_assoc, mul_inv_cancel, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
G : Type u_1
inst : Group G
a b : G
rw : a * a⁻¹ * b = b
rw₁ : 1 * b = b
⊢ a * (a⁻¹ * b) = b
have rw₂ : b = b
Tactic: rw [← mul_assoc, mul_inv_cancel, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
G : Type u_1
inst : Group G
a b : G
⊢ a * b * b⁻¹ = a
have rw : a * (b * b⁻¹) = a
Tactic: rw [mul_assoc, mul_inv_cancel, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
G : Type u_1
inst : Group G
a b : G
rw : a * (b * b⁻¹) = a
⊢ a * b * b⁻¹ = a
have rw₁ : a * 1 = a
Tactic: rw [mul_assoc, mul_inv_cancel, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
G : Type u_1
inst : Group G
a b : G
rw : a * (b * b⁻¹) = a
rw₁ : a * 1 = a
⊢ a * b * b⁻¹ = a
have rw₂ : a = a
Tactic: rw [mul_assoc, mul_inv_cancel, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
G : Type u_1
inst : Group G
a b : G
⊢ a * b / b = a
have rw : a * b * b⁻¹ = a
Tactic: rw [div_eq_mul_inv, mul_inv_cancel_right a b]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
G : Type u_1
inst : Group G
a b : G
rw : a * b * b⁻¹ = a
⊢ a * b / b = a
have rw₁ : a = a
Tactic: rw [div_eq_mul_inv, mul_inv_cancel_right a b]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
G : Type u_1
inst : Group G
a b : G
⊢ a * b⁻¹ * b = a
have rw : a * (b⁻¹ * b) = a
Tactic: rw [mul_assoc, inv_mul_cancel, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
G : Type u_1
inst : Group G
a b : G
rw : a * (b⁻¹ * b) = a
⊢ a * b⁻¹ * b = a
have rw₁ : a * 1 = a
Tactic: rw [mul_assoc, inv_mul_cancel, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
G : Type u_1
inst : Group G
a b : G
rw : a * (b⁻¹ * b) = a
rw₁ : a * 1 = a
⊢ a * b⁻¹ * b = a
have rw₂ : a = a
Tactic: rw [mul_assoc, inv_mul_cancel, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
G : Type u_1
inst : Group G
a b : G
⊢ a / b * b = a
have rw : a * b⁻¹ * b = a
Tactic: rw [div_eq_mul_inv, inv_mul_cancel_right a b]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
G : Type u_1
inst : Group G
a b : G
rw : a * b⁻¹ * b = a
⊢ a / b * b = a
have rw₁ : a = a
Tactic: rw [div_eq_mul_inv, inv_mul_cancel_right a b]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
G : Type u_1
inst : Group G
a_1 b_1 a b : G
⊢ (a * b)⁻¹ = b⁻¹ * a⁻¹
have h : a * b * (b⁻¹ * a⁻¹) = 1
Tactic: apply inv_eq_of_mul
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
G : Type u_1
inst : Group G
a_1 b_1 a b : G
⊢ a * b * (b⁻¹ * a⁻¹) = 1
have h : a * (b * (b⁻¹ * a⁻¹)) = 1
Tactic: rw [mul_assoc, mul_inv_cancel_left, mul_inv_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
G : Type u_1
inst : Group G
a_1 b_1 a b : G
h : a * (b * (b⁻¹ * a⁻¹)) = 1
⊢ a * b * (b⁻¹ * a⁻¹) = 1
have h₁ : a * a⁻¹ = 1
Tactic: rw [mul_assoc, mul_inv_cancel_left, mul_inv_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
G : Type u_1
inst : Group G
a_1 b_1 a b : G
h : a * (b * (b⁻¹ * a⁻¹)) = 1
h₁ : a * a⁻¹ = 1
⊢ a * b * (b⁻¹ * a⁻¹) = 1
have h₂ : Eq.{u_1 + 1} (α := G) 1 1
Tactic: rw [mul_assoc, mul_inv_cancel_left, mul_inv_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
G : Type u_1
inst : Group G
a_1 b_1 a b c : G
h : Eq.{u_1 + 1} (α := G) ((fun (x : G) ↦ a * x) b) ((fun (x : G) ↦ a * x) c)
⊢ b = c
have rw : a⁻¹ * (a * b) = c
Tactic: rw [← inv_mul_cancel_left a b, show a * b = a * c from h, inv_mul_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
G : Type u_1
inst : Group G
a_1 b_1 a b c : G
h : Eq.{u_1 + 1} (α := G) ((fun (x : G) ↦ a * x) b) ((fun (x : G) ↦ a * x) c)
rw : a⁻¹ * (a * b) = c
⊢ b = c
have rw₁ : a⁻¹ * (a * c) = c
Tactic: rw [← inv_mul_cancel_left a b, show a * b = a * c from h, inv_mul_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
G : Type u_1
inst : Group G
a_1 b_1 a b c : G
h : Eq.{u_1 + 1} (α := G) ((fun (x : G) ↦ a * x) b) ((fun (x : G) ↦ a * x) c)
rw : a⁻¹ * (a * b) = c
rw₁ : a⁻¹ * (a * c) = c
⊢ b = c
have rw₂ : c = c
Tactic: rw [← inv_mul_cancel_left a b, show a * b = a * c from h, inv_mul_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
G : Type u_1
inst : Group G
a_1 b_1 a b c : G
h : Eq.{u_1 + 1} (α := G) ((fun (x : G) ↦ x * a) b) ((fun (x : G) ↦ x * a) c)
⊢ b = c
have rw : b * a * a⁻¹ = c
Tactic: rw [← mul_inv_cancel_right b a, show b * a = c * a from h, mul_inv_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
G : Type u_1
inst : Group G
a_1 b_1 a b c : G
h : Eq.{u_1 + 1} (α := G) ((fun (x : G) ↦ x * a) b) ((fun (x : G) ↦ x * a) c)
rw : b * a * a⁻¹ = c
⊢ b = c
have rw₁ : c * a * a⁻¹ = c
Tactic: rw [← mul_inv_cancel_right b a, show b * a = c * a from h, mul_inv_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
G : Type u_1
inst : Group G
a_1 b_1 a b c : G
h : Eq.{u_1 + 1} (α := G) ((fun (x : G) ↦ x * a) b) ((fun (x : G) ↦ x * a) c)
rw : b * a * a⁻¹ = c
rw₁ : c * a * a⁻¹ = c
⊢ b = c
have rw₂ : c = c
Tactic: rw [← mul_inv_cancel_right b a, show b * a = c * a from h, mul_inv_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
G : Type u_1
inst : CommGroup G
a b : G
⊢ a⁻¹ * b * a = b
have rw : a * (a⁻¹ * b) = b
Tactic: rw [mul_comm, mul_inv_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
G : Type u_1
inst : CommGroup G
a b : G
rw : a * (a⁻¹ * b) = b
⊢ a⁻¹ * b * a = b
have rw₁ : b = b
Tactic: rw [mul_comm, mul_inv_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
G : Type u_1
inst : CommGroup G
a b : G
⊢ a * b * a⁻¹ = b
have rw : a⁻¹ * (a * b) = b
Tactic: rw [mul_comm, inv_mul_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
G : Type u_1
inst : CommGroup G
a b : G
rw : a⁻¹ * (a * b) = b
⊢ a * b * a⁻¹ = b
have rw₁ : b = b
Tactic: rw [mul_comm, inv_mul_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
G : Type u_1
inst : CommGroup G
a b : G
⊢ a⁻¹ * (b * a) = b
have rw : b * a * a⁻¹ = b
Tactic: rw [mul_comm, mul_inv_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
G : Type u_1
inst : CommGroup G
a b : G
rw : b * a * a⁻¹ = b
⊢ a⁻¹ * (b * a) = b
have rw₁ : b = b
Tactic: rw [mul_comm, mul_inv_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
G : Type u_1
inst : CommGroup G
a b : G
⊢ a * (b * a⁻¹) = b
have rw : b * a⁻¹ * a = b
Tactic: rw [mul_comm, inv_mul_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
G : Type u_1
inst : CommGroup G
a b : G
rw : b * a⁻¹ * a = b
⊢ a * (b * a⁻¹) = b
have rw₁ : b = b
Tactic: rw [mul_comm, inv_mul_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Embedding (goal)
Goal:
G : Type u_1
inst : CommMagma G
inst_1 : IsCancelMul G
g : G
⊢ mulLeftEmbedding g = mulRightEmbedding g
have h : ∀ (x : G), Eq (α := G) ((mulLeftEmbedding g : (a : G) → G) x : G) ((mulRightEmbedding g : (a : G) → G) x : G)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.End (goal)
Goal:
α : Type u_7
σ : Perm α
m n : ℤ
x : α
⊢ Eq (α := α) ((σ ^ m : (a : α) → α) ((σ ^ n : (a : α) → α) x : α) : α)
    ((σ ^ n : (a : α) → α) ((σ ^ m : (a : α) → α) x : α) : α)
have rw : Eq (α := α) ((σ ^ m * σ ^ n : (a : α) → α) x : α) ((σ ^ n : (a : α) → α) ((σ ^ m : (a : α) → α) x : α) : α)
Tactic: rw [← Equiv.Perm.mul_apply, ← Equiv.Perm.mul_apply, zpow_mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.End (goal)
Goal:
α : Type u_7
σ : Perm α
m n : ℤ
x : α
rw : Eq (α := α) ((σ ^ m * σ ^ n : (a : α) → α) x : α) ((σ ^ n : (a : α) → α) ((σ ^ m : (a : α) → α) x : α) : α)
⊢ Eq (α := α) ((σ ^ m : (a : α) → α) ((σ ^ n : (a : α) → α) x : α) : α)
    ((σ ^ n : (a : α) → α) ((σ ^ m : (a : α) → α) x : α) : α)
have rw₁ : Eq (α := α) ((σ ^ m * σ ^ n : (a : α) → α) x : α) ((σ ^ n * σ ^ m : (a : α) → α) x : α)
Tactic: rw [← Equiv.Perm.mul_apply, ← Equiv.Perm.mul_apply, zpow_mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.End (goal)
Goal:
α : Type u_7
σ : Perm α
m n : ℤ
x : α
rw : Eq (α := α) ((σ ^ m * σ ^ n : (a : α) → α) x : α) ((σ ^ n : (a : α) → α) ((σ ^ m : (a : α) → α) x : α) : α)
rw₁ : Eq (α := α) ((σ ^ m * σ ^ n : (a : α) → α) x : α) ((σ ^ n * σ ^ m : (a : α) → α) x : α)
⊢ Eq (α := α) ((σ ^ m : (a : α) → α) ((σ ^ n : (a : α) → α) x : α) : α)
    ((σ ^ n : (a : α) → α) ((σ ^ m : (a : α) → α) x : α) : α)
have rw₂ : Eq (α := α) ((σ ^ n * σ ^ m : (a : α) → α) x : α) ((σ ^ n * σ ^ m : (a : α) → α) x : α)
Tactic: rw [← Equiv.Perm.mul_apply, ← Equiv.Perm.mul_apply, zpow_mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.End (goal)
Goal:
α : Type u_7
β : Type u_8
fst : Perm α
snd : Perm β
fst_1 : Perm α
snd_1 : Perm β
h :
  Eq (α := Perm (α ⊕ β)) ((sumCongrHom α β : (a : Perm α × Perm β) → Perm (α ⊕ β)) (fst, snd) : Perm (α ⊕ β))
    ((sumCongrHom α β : (a : Perm α × Perm β) → Perm (α ⊕ β)) (fst_1, snd_1) : Perm (α ⊕ β))
⊢ (fst, snd) = (fst_1, snd_1)
have rw : fst = fst_1 ∧ snd = snd_1
Tactic: rw [Prod.mk_inj]
-- Lean 4 proof step from Mathlib.Algebra.Group.End (goal)
Goal:
α : Type u_7
β : Type u_8
fst : Perm α
snd : Perm β
fst_1 : Perm α
snd_1 : Perm β
h :
  Eq (α := Perm (α ⊕ β)) ((sumCongrHom α β : (a : Perm α × Perm β) → Perm (α ⊕ β)) (fst, snd) : Perm (α ⊕ β))
    ((sumCongrHom α β : (a : Perm α × Perm β) → Perm (α ⊕ β)) (fst_1, snd_1) : Perm (α ⊕ β))
⊢ fst = fst_1 ∧ snd = snd_1
have left : fst = fst_1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Group.End (goal)
Goal:
α : Type u_7
β : Type u_8
fst : Perm α
snd : Perm β
fst_1 : Perm α
snd_1 : Perm β
h :
  Eq (α := Perm (α ⊕ β)) ((sumCongrHom α β : (a : Perm α × Perm β) → Perm (α ⊕ β)) (fst, snd) : Perm (α ⊕ β))
    ((sumCongrHom α β : (a : Perm α × Perm β) → Perm (α ⊕ β)) (fst_1, snd_1) : Perm (α ⊕ β))
left : fst = fst_1
⊢ fst = fst_1 ∧ snd = snd_1
have right : snd = snd_1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Group.End (goal)
Goal:
α : Type u_7
β : Type u_8
fst : Perm α
snd : Perm β
fst_1 : Perm α
snd_1 : Perm β
h :
  Eq (α := Perm (α ⊕ β)) ((sumCongrHom α β : (a : Perm α × Perm β) → Perm (α ⊕ β)) (fst, snd) : Perm (α ⊕ β))
    ((sumCongrHom α β : (a : Perm α × Perm β) → Perm (α ⊕ β)) (fst_1, snd_1) : Perm (α ⊕ β))
⊢ fst = fst_1
have left : ∀ (i : α), Eq (α := α) ((fst : (a : α) → α) i : α) ((fst_1 : (a : α) → α) i : α)
Tactic: ext i
-- Lean 4 proof step from Mathlib.Algebra.Group.End (goal)
Goal:
α : Type u_7
β : Type u_8
fst : Perm α
snd : Perm β
fst_1 : Perm α
snd_1 : Perm β
h :
  Eq (α := Perm (α ⊕ β)) ((sumCongrHom α β : (a : Perm α × Perm β) → Perm (α ⊕ β)) (fst, snd) : Perm (α ⊕ β))
    ((sumCongrHom α β : (a : Perm α × Perm β) → Perm (α ⊕ β)) (fst_1, snd_1) : Perm (α ⊕ β))
⊢ snd = snd_1
have right : ∀ (i : β), Eq (α := β) ((snd : (a : β) → β) i : β) ((snd_1 : (a : β) → β) i : β)
Tactic: ext i
-- Lean 4 proof step from Mathlib.Algebra.Group.End (goal)
Goal:
α : Type u_7
β : α → Type u_8
x y : (a : α) → Perm (β a)
h :
  Eq (α := Perm ((a : α) × β a))
    ((sigmaCongrRightHom β : (a : (a : α) → Perm (β a)) → Perm ((a : α) × β a)) x : Perm ((a : α) × β a))
    ((sigmaCongrRightHom β : (a : (a : α) → Perm (β a)) → Perm ((a : α) × β a)) y : Perm ((a : α) × β a))
⊢ x = y
have h₁ : ∀ (a : α) (b : β a), Eq (α := β a) ((x a : (a_1 : β a) → β a) b : β a) ((y a : (a_1 : β a) → β a) b : β a)
Tactic: ext a b
-- Lean 4 proof step from Mathlib.Algebra.Group.End (goal)
Goal:
α : Type u_4
p : α → Prop
inst : DecidablePred p
fst : Perm { a : α // p a }
snd : Perm { a : α // ¬p a }
fst_1 : Perm { a : α // p a }
snd_1 : Perm { a : α // ¬p a }
h :
  Eq (α := Perm α)
    ((subtypeCongrHom p : (a : Perm { a : α // p a } × Perm { a : α // ¬p a }) → Perm α) (fst, snd) : Perm α)
    ((subtypeCongrHom p : (a : Perm { a : α // p a } × Perm { a : α // ¬p a }) → Perm α) (fst_1, snd_1) : Perm α)
⊢ (fst, snd) = (fst_1, snd_1)
have rw : fst = fst_1 ∧ snd = snd_1
Tactic: rw [Prod.mk_inj]
-- Lean 4 proof step from Mathlib.Algebra.Group.End (goal)
Goal:
α : Type u_4
p : α → Prop
inst : DecidablePred p
fst : Perm { a : α // p a }
snd : Perm { a : α // ¬p a }
fst_1 : Perm { a : α // p a }
snd_1 : Perm { a : α // ¬p a }
h :
  Eq (α := Perm α)
    ((subtypeCongrHom p : (a : Perm { a : α // p a } × Perm { a : α // ¬p a }) → Perm α) (fst, snd) : Perm α)
    ((subtypeCongrHom p : (a : Perm { a : α // p a } × Perm { a : α // ¬p a }) → Perm α) (fst_1, snd_1) : Perm α)
⊢ fst = fst_1 ∧ snd = snd_1
have left : fst = fst_1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Group.End (goal)
Goal:
α : Type u_4
p : α → Prop
inst : DecidablePred p
fst : Perm { a : α // p a }
snd : Perm { a : α // ¬p a }
fst_1 : Perm { a : α // p a }
snd_1 : Perm { a : α // ¬p a }
h :
  Eq (α := Perm α)
    ((subtypeCongrHom p : (a : Perm { a : α // p a } × Perm { a : α // ¬p a }) → Perm α) (fst, snd) : Perm α)
    ((subtypeCongrHom p : (a : Perm { a : α // p a } × Perm { a : α // ¬p a }) → Perm α) (fst_1, snd_1) : Perm α)
left : fst = fst_1
⊢ fst = fst_1 ∧ snd = snd_1
have right : snd = snd_1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Group.End (goal)
Goal:
α : Type u_4
p : α → Prop
inst : DecidablePred p
fst : Perm { a : α // p a }
snd : Perm { a : α // ¬p a }
fst_1 : Perm { a : α // p a }
snd_1 : Perm { a : α // ¬p a }
h :
  Eq (α := Perm α)
    ((subtypeCongrHom p : (a : Perm { a : α // p a } × Perm { a : α // ¬p a }) → Perm α) (fst, snd) : Perm α)
    ((subtypeCongrHom p : (a : Perm { a : α // p a } × Perm { a : α // ¬p a }) → Perm α) (fst_1, snd_1) : Perm α)
⊢ fst = fst_1
have left : ∀ (i : { a : α // p a }),
  Eq.{u_4 + 1} (α := α) (↑((fst : (a : { a : α // p a }) → { a : α // p a }) i) : α)
    (↑((fst_1 : (a : { a : α // p a }) → { a : α // p a }) i) : α)
Tactic: ext i
-- Lean 4 proof step from Mathlib.Algebra.Group.End (goal)
Goal:
α : Type u_4
p : α → Prop
inst : DecidablePred p
fst : Perm { a : α // p a }
snd : Perm { a : α // ¬p a }
fst_1 : Perm { a : α // p a }
snd_1 : Perm { a : α // ¬p a }
h :
  Eq (α := Perm α)
    ((subtypeCongrHom p : (a : Perm { a : α // p a } × Perm { a : α // ¬p a }) → Perm α) (fst, snd) : Perm α)
    ((subtypeCongrHom p : (a : Perm { a : α // p a } × Perm { a : α // ¬p a }) → Perm α) (fst_1, snd_1) : Perm α)
⊢ snd = snd_1
have right : ∀ (i : { a : α // ¬p a }),
  Eq.{u_4 + 1} (α := α) (↑((snd : (a : { a : α // ¬p a }) → { a : α // ¬p a }) i) : α)
    (↑((snd_1 : (a : { a : α // ¬p a }) → { a : α // ¬p a }) i) : α)
Tactic: ext i
-- Lean 4 proof step from Mathlib.Algebra.Group.End (goal)
Goal:
α : Type u_4
p : α → Prop
f : Perm α
hf : ∀ (x : α), p ((f : (a : α) → α) x) ↔ p x
n : ℕ
ih : f.subtypePerm (p := p) hf ^ n = (f ^ n).subtypePerm (p := p) ⋯
⊢ f.subtypePerm (p := p) hf ^ (n + 1) = (f ^ (n + 1)).subtypePerm (p := p) ⋯
have succ : f.subtypePerm (p := p) hf * f.subtypePerm (p := p) hf ^ n = (f * f ^ n).subtypePerm (p := p) sorry
Tactic: simp_rw [pow_succ', ih, subtypePerm_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.End (goal)
Goal:
α : Type u_4
p : α → Prop
f : Perm α
hf : ∀ (x : α), p ((f : (a : α) → α) x) ↔ p x
n : ℕ
ih : f.subtypePerm (p := p) hf ^ n = (f ^ n).subtypePerm (p := p) ⋯
succ : f.subtypePerm (p := p) hf * f.subtypePerm (p := p) hf ^ n = (f * f ^ n).subtypePerm (p := p) ⋯
⊢ f.subtypePerm (p := p) hf ^ (n + 1) = (f ^ (n + 1)).subtypePerm (p := p) ⋯
have succ₁ : f.subtypePerm (p := p) hf * (f ^ n).subtypePerm (p := p) sorry = (f * f ^ n).subtypePerm (p := p) sorry
Tactic: simp_rw [pow_succ', ih, subtypePerm_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.End (goal)
Goal:
α : Type u_4
p : α → Prop
f : Perm α
n : ℕ
hf : ∀ (x : α), p ((f : (a : α) → α) x) ↔ p x
⊢ f.subtypePerm (p := p) hf ^ n = (f ^ n).subtypePerm (p := p) ⋯
have zero : HPow.hPow (β := ℕ) (f.subtypePerm (p := p) hf) 0 = (HPow.hPow (β := ℕ) f 0).subtypePerm (p := p) sorry
Tactic: induction n with
  | zero => simp
  | succ n ih => simp_rw [pow_succ', ih, subtypePerm_mul]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Group.End (goal)
Goal:
α : Type u_4
p : α → Prop
f : Perm α
n : ℕ
hf : ∀ (x : α), p ((f : (a : α) → α) x) ↔ p x
zero : HPow.hPow (β := ℕ) (f.subtypePerm (p := p) hf) 0 = (HPow.hPow (β := ℕ) f 0).subtypePerm (p := p) ⋯
⊢ f.subtypePerm (p := p) hf ^ n = (f ^ n).subtypePerm (p := p) ⋯
have succ : ∀ (n : ℕ) (ih : f.subtypePerm (p := p) hf ^ n = (f ^ n).subtypePerm (p := p) sorry),
  f.subtypePerm (p := p) hf ^ (n + 1) = (f ^ (n + 1)).subtypePerm (p := p) sorry
Tactic: induction n with
  | zero => simp
  | succ n ih => simp_rw [pow_succ', ih, subtypePerm_mul]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Group.End (goal)
Goal:
α : Type u_4
p : α → Prop
f : Perm α
hf : ∀ (x : α), p ((f : (a : α) → α) x) ↔ p x
n : ℕ
⊢ ∀ (x : α), p ((f ^ Int.negSucc n : (a : α) → α) x) ↔ p x
have rw : ∀ (x : α), p (((f ^ (n + 1))⁻¹ : (a : α) → α) x) ↔ p x
Tactic: rw [zpow_negSucc]
-- Lean 4 proof step from Mathlib.Algebra.Group.End (goal)
Goal:
α : Type u_4
p : α → Prop
f : Perm α
n : ℤ
hf : ∀ (x : α), p ((f : (a : α) → α) x) ↔ p x
⊢ f.subtypePerm (p := p) hf ^ n = (f ^ n).subtypePerm (p := p) ⋯
have ofNat : ∀ (n : ℕ), f.subtypePerm (p := p) hf ^ Int.ofNat n = (f ^ Int.ofNat n).subtypePerm (p := p) sorry
Tactic: cases n with
  | ofNat n => exact subtypePerm_pow _ _ _
  | negSucc n => simp only [zpow_negSucc, subtypePerm_pow, subtypePerm_inv]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Group.End (goal)
Goal:
α : Type u_4
p : α → Prop
f : Perm α
n : ℤ
hf : ∀ (x : α), p ((f : (a : α) → α) x) ↔ p x
ofNat : ∀ (n : ℕ), f.subtypePerm (p := p) hf ^ Int.ofNat n = (f ^ Int.ofNat n).subtypePerm (p := p) ⋯
⊢ f.subtypePerm (p := p) hf ^ n = (f ^ n).subtypePerm (p := p) ⋯
have negSucc : ∀ (n : ℕ), f.subtypePerm (p := p) hf ^ Int.negSucc n = (f ^ Int.negSucc n).subtypePerm (p := p) sorry
Tactic: cases n with
  | ofNat n => exact subtypePerm_pow _ _ _
  | negSucc n => simp only [zpow_negSucc, subtypePerm_pow, subtypePerm_inv]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Group.End (goal)
Goal:
α : Type u_4
p : α → Prop
inst : DecidablePred p
f : Perm α
h₁ : ∀ (x : α), p ((f : (a : α) → α) x) ↔ p x
h₂ : ∀ (x : α), (f : (a : α) → α) x ≠ x → p x
x : α
⊢ Eq (α := α)
    ((((ofSubtype (p := fun (x : α) ↦ p x) : (a : Perm { x : α // p x }) → Perm α) (f.subtypePerm (p := p) h₁) :
            Perm α) :
          (a : α) → α)
        x :
      α)
    ((f : (a : α) → α) x : α)
have pos : ∀ (hx : p x),
  Eq (α := α)
    ((((ofSubtype (p := fun (x : α) ↦ p x) : (a : Perm { x : α // p x }) → Perm α) (f.subtypePerm (p := p) h₁) :
            Perm α) :
          (a : α) → α)
        x :
      α)
    ((f : (a : α) → α) x : α)
Tactic: by_cases hx : p x
-- Lean 4 proof step from Mathlib.Algebra.Group.End (goal)
Goal:
α : Type u_4
p : α → Prop
inst : DecidablePred p
f : Perm α
h₁ : ∀ (x : α), p ((f : (a : α) → α) x) ↔ p x
h₂ : ∀ (x : α), (f : (a : α) → α) x ≠ x → p x
x : α
pos :
  ∀ (hx : p x),
    Eq (α := α)
      ((((ofSubtype (p := fun (x : α) ↦ p x) : (a : Perm { x : α // p x }) → Perm α) (f.subtypePerm (p := p) h₁) :
              Perm α) :
            (a : α) → α)
          x :
        α)
      ((f : (a : α) → α) x : α)
⊢ Eq (α := α)
    ((((ofSubtype (p := fun (x : α) ↦ p x) : (a : Perm { x : α // p x }) → Perm α) (f.subtypePerm (p := p) h₁) :
            Perm α) :
          (a : α) → α)
        x :
      α)
    ((f : (a : α) → α) x : α)
have neg : ∀ (hx : ¬p x),
  Eq (α := α)
    ((((ofSubtype (p := fun (x : α) ↦ p x) : (a : Perm { x : α // p x }) → Perm α) (f.subtypePerm (p := p) h₁) :
            Perm α) :
          (a : α) → α)
        x :
      α)
    ((f : (a : α) → α) x : α)
Tactic: by_cases hx : p x
-- Lean 4 proof step from Mathlib.Algebra.Group.End (goal)
Goal:
α : Type u_4
p : α → Prop
inst : DecidablePred p
f : Perm α
h₁ : ∀ (x : α), p ((f : (a : α) → α) x) ↔ p x
h₂ : ∀ (x : α), (f : (a : α) → α) x ≠ x → p x
x : α
hx : ¬p x
⊢ Eq (α := α)
    ((((ofSubtype (p := fun (x : α) ↦ p x) : (a : Perm { x : α // p x }) → Perm α) (f.subtypePerm (p := p) h₁) :
            Perm α) :
          (a : α) → α)
        x :
      α)
    ((f : (a : α) → α) x : α)
have neg : x = (f : (a : α) → α) x
Tactic: rw [ofSubtype, MonoidHom.coe_mk, OneHom.coe_mk,
        Equiv.Perm.extendDomain_apply_not_subtype _ _ hx]
-- Lean 4 proof step from Mathlib.Algebra.Group.End (goal)
Goal:
α : Type u_4
p : α → Prop
inst : DecidablePred p
x y : Perm (Subtype p)
h :
  Eq (α := Perm α) ((ofSubtype (p := p) : (a : Perm (Subtype p)) → Perm α) x : Perm α)
    ((ofSubtype (p := p) : (a : Perm (Subtype p)) → Perm α) y : Perm α)
⊢ x = y
have rw : ∀
  (h :
    ∀ (x_1 : α),
      Eq (α := α) ((((ofSubtype (p := p) : (a : Perm (Subtype p)) → Perm α) x : Perm α) : (a : α) → α) x_1 : α)
        ((((ofSubtype (p := p) : (a : Perm (Subtype p)) → Perm α) y : Perm α) : (a : α) → α) x_1 : α))
  (x_1 : Subtype p),
  Eq (α := Subtype p) ((x : (a : Subtype p) → Subtype p) x_1 : Subtype p)
    ((y : (a : Subtype p) → Subtype p) x_1 : Subtype p)
Tactic: rw [Perm.ext_iff] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Group.End (hypothesis)
Goal:
α : Type u_4
p : α → Prop
inst : DecidablePred p
x y : Perm (Subtype p)
h :
  ∀ (x_1 : α),
    Eq (α := α) ((((ofSubtype (p := p) : (a : Perm (Subtype p)) → Perm α) x : Perm α) : (a : α) → α) x_1 : α)
      ((((ofSubtype (p := p) : (a : Perm (Subtype p)) → Perm α) y : Perm α) : (a : α) → α) x_1 : α)
a : Subtype p
⊢ Eq (α := Subtype p) ((x : (a : Subtype p) → Subtype p) a : Subtype p)
    ((y : (a : Subtype p) → Subtype p) a : Subtype p)
have h₁ : Eq (α := α) ((((ofSubtype (p := p) : (a : Perm (Subtype p)) → Perm α) x : Perm α) : (a : α) → α) (↑a : α) : α)
  ((((ofSubtype (p := p) : (a : Perm (Subtype p)) → Perm α) y : Perm α) : (a : α) → α) (↑a : α) : α)
Tactic: specialize h a
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Group.End (goal)
Goal:
α : Type u_4
p : α → Prop
inst : DecidablePred p
x y : Perm (Subtype p)
a : Subtype p
h :
  Eq (α := α) ((((ofSubtype (p := p) : (a : Perm (Subtype p)) → Perm α) x : Perm α) : (a : α) → α) (↑a : α) : α)
    ((((ofSubtype (p := p) : (a : Perm (Subtype p)) → Perm α) y : Perm α) : (a : α) → α) (↑a : α) : α)
⊢ Eq (α := Subtype p) ((x : (a : Subtype p) → Subtype p) a : Subtype p)
    ((y : (a : Subtype p) → Subtype p) a : Subtype p)
have rwa : ∀
  (h :
    Eq (α := α) ((↑((x : (a : Subtype p) → Subtype p) a) : α) : α)
      ((((ofSubtype (p := p) : (a : Perm (Subtype p)) → Perm α) y : Perm α) : (a : α) → α) (↑a : α) : α)),
  Eq (α := Subtype p) ((x : (a : Subtype p) → Subtype p) a : Subtype p)
    ((y : (a : Subtype p) → Subtype p) a : Subtype p)
Tactic: rwa [ofSubtype_apply_coe, ofSubtype_apply_coe, SetCoe.ext_iff] at h
Cleared hypotheses: h