awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : α) : α)
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)
⊢ 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.{u_4 + 1} (α := α) (↑((x : (a : Subtype p) → Subtype p) a) : α) (↑((y : (a : Subtype p) → Subtype p) 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
-- 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 : α) : α)
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)
rwa₁ :
  ∀
    (h :
      Eq.{u_4 + 1} (α := α) (↑((x : (a : Subtype p) → Subtype p) a) : α) (↑((y : (a : Subtype p) → Subtype p) a) : α)),
    Eq (α := Subtype p) ((x : (a : Subtype p) → Subtype p) a : Subtype p)
      ((y : (a : Subtype p) → Subtype p) 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 rwa₂ : ∀
  (h :
    Eq (α := (↑p : Type u_4)) ((x : (a : Subtype p) → Subtype p) a : Subtype p)
      ((y : (a : Subtype p) → Subtype p) a : Subtype p)),
  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
-- Lean 4 proof step from Mathlib.Algebra.Group.End (goal)
Goal:
α : Type u_4
inst : DecidableEq α
f : Perm α
x y z : α
⊢ Eq (α := α) ((swap x y * f : (a : α) → α) z : α)
    ((HMul.hMul (β := Perm α) f (swap ((f⁻¹ : (a : α) → α) x) ((f⁻¹ : (a : α) → α) y) : Perm α) : (a : α) → α) z : α)
have simp : (if (f : (a : α) → α) z = x then y else if (f : (a : α) → α) z = y then x else (f : (a : α) → α) z) =
  (f : (a : α) → α)
    (if z = (f⁻¹ : (a : α) → α) x then (f⁻¹ : (a : α) → α) y
      else if z = (f⁻¹ : (a : α) → α) y then (f⁻¹ : (a : α) → α) x else z :
      α)
Tactic: simp only [Perm.mul_apply, swap_apply_def]
-- Lean 4 proof step from Mathlib.Algebra.Group.End (goal)
Goal:
α : Type u_4
inst : DecidableEq α
f : Perm α
x y z : α
⊢ (if (f : (a : α) → α) z = x then y else if (f : (a : α) → α) z = y then x else (f : (a : α) → α) z) =
    (f : (a : α) → α)
      (if z = (f⁻¹ : (a : α) → α) x then (f⁻¹ : (a : α) → α) y
        else if z = (f⁻¹ : (a : α) → α) y then (f⁻¹ : (a : α) → α) x else z :
        α)
have pos : (f : (a : α) → α) z = x → z = (f⁻¹ : (a : α) → α) x → y = (f : (a : α) → α) ((f⁻¹ : (a : α) → α) y : α)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Group.End (goal)
Goal:
α : Type u_4
inst : DecidableEq α
f : Perm α
x y z : α
pos : (f : (a : α) → α) z = x → z = (f⁻¹ : (a : α) → α) x → y = (f : (a : α) → α) ((f⁻¹ : (a : α) → α) y : α)
⊢ (if (f : (a : α) → α) z = x then y else if (f : (a : α) → α) z = y then x else (f : (a : α) → α) z) =
    (f : (a : α) → α)
      (if z = (f⁻¹ : (a : α) → α) x then (f⁻¹ : (a : α) → α) y
        else if z = (f⁻¹ : (a : α) → α) y then (f⁻¹ : (a : α) → α) x else z :
        α)
have pos₁ : (f : (a : α) → α) z = x →
  ¬z = (f⁻¹ : (a : α) → α) x → z = (f⁻¹ : (a : α) → α) y → y = (f : (a : α) → α) ((f⁻¹ : (a : α) → α) x : α)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Group.End (goal)
Goal:
α : Type u_4
inst : DecidableEq α
f : Perm α
x y z : α
pos : (f : (a : α) → α) z = x → z = (f⁻¹ : (a : α) → α) x → y = (f : (a : α) → α) ((f⁻¹ : (a : α) → α) y : α)
pos₁ :
  (f : (a : α) → α) z = x →
    ¬z = (f⁻¹ : (a : α) → α) x → z = (f⁻¹ : (a : α) → α) y → y = (f : (a : α) → α) ((f⁻¹ : (a : α) → α) x : α)
⊢ (if (f : (a : α) → α) z = x then y else if (f : (a : α) → α) z = y then x else (f : (a : α) → α) z) =
    (f : (a : α) → α)
      (if z = (f⁻¹ : (a : α) → α) x then (f⁻¹ : (a : α) → α) y
        else if z = (f⁻¹ : (a : α) → α) y then (f⁻¹ : (a : α) → α) x else z :
        α)
have neg : (f : (a : α) → α) z = x → ¬z = (f⁻¹ : (a : α) → α) x → ¬z = (f⁻¹ : (a : α) → α) y → y = (f : (a : α) → α) z
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Group.End (goal)
Goal:
α : Type u_4
inst : DecidableEq α
f : Perm α
x y z : α
pos : (f : (a : α) → α) z = x → z = (f⁻¹ : (a : α) → α) x → y = (f : (a : α) → α) ((f⁻¹ : (a : α) → α) y : α)
pos₁ :
  (f : (a : α) → α) z = x →
    ¬z = (f⁻¹ : (a : α) → α) x → z = (f⁻¹ : (a : α) → α) y → y = (f : (a : α) → α) ((f⁻¹ : (a : α) → α) x : α)
neg : (f : (a : α) → α) z = x → ¬z = (f⁻¹ : (a : α) → α) x → ¬z = (f⁻¹ : (a : α) → α) y → y = (f : (a : α) → α) z
⊢ (if (f : (a : α) → α) z = x then y else if (f : (a : α) → α) z = y then x else (f : (a : α) → α) z) =
    (f : (a : α) → α)
      (if z = (f⁻¹ : (a : α) → α) x then (f⁻¹ : (a : α) → α) y
        else if z = (f⁻¹ : (a : α) → α) y then (f⁻¹ : (a : α) → α) x else z :
        α)
have pos₂ : ¬(f : (a : α) → α) z = x →
  (f : (a : α) → α) z = y → z = (f⁻¹ : (a : α) → α) x → x = (f : (a : α) → α) ((f⁻¹ : (a : α) → α) y : α)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Group.End (goal)
Goal:
α : Type u_4
inst : DecidableEq α
f : Perm α
x y z : α
pos : (f : (a : α) → α) z = x → z = (f⁻¹ : (a : α) → α) x → y = (f : (a : α) → α) ((f⁻¹ : (a : α) → α) y : α)
pos₁ :
  (f : (a : α) → α) z = x →
    ¬z = (f⁻¹ : (a : α) → α) x → z = (f⁻¹ : (a : α) → α) y → y = (f : (a : α) → α) ((f⁻¹ : (a : α) → α) x : α)
neg : (f : (a : α) → α) z = x → ¬z = (f⁻¹ : (a : α) → α) x → ¬z = (f⁻¹ : (a : α) → α) y → y = (f : (a : α) → α) z
pos₂ :
  ¬(f : (a : α) → α) z = x →
    (f : (a : α) → α) z = y → z = (f⁻¹ : (a : α) → α) x → x = (f : (a : α) → α) ((f⁻¹ : (a : α) → α) y : α)
⊢ (if (f : (a : α) → α) z = x then y else if (f : (a : α) → α) z = y then x else (f : (a : α) → α) z) =
    (f : (a : α) → α)
      (if z = (f⁻¹ : (a : α) → α) x then (f⁻¹ : (a : α) → α) y
        else if z = (f⁻¹ : (a : α) → α) y then (f⁻¹ : (a : α) → α) x else z :
        α)
have pos₃ : ¬(f : (a : α) → α) z = x →
  (f : (a : α) → α) z = y →
    ¬z = (f⁻¹ : (a : α) → α) x → z = (f⁻¹ : (a : α) → α) y → x = (f : (a : α) → α) ((f⁻¹ : (a : α) → α) x : α)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Group.End (goal)
Goal:
α : Type u_4
inst : DecidableEq α
f : Perm α
x y z : α
pos : (f : (a : α) → α) z = x → z = (f⁻¹ : (a : α) → α) x → y = (f : (a : α) → α) ((f⁻¹ : (a : α) → α) y : α)
pos₁ :
  (f : (a : α) → α) z = x →
    ¬z = (f⁻¹ : (a : α) → α) x → z = (f⁻¹ : (a : α) → α) y → y = (f : (a : α) → α) ((f⁻¹ : (a : α) → α) x : α)
neg : (f : (a : α) → α) z = x → ¬z = (f⁻¹ : (a : α) → α) x → ¬z = (f⁻¹ : (a : α) → α) y → y = (f : (a : α) → α) z
pos₂ :
  ¬(f : (a : α) → α) z = x →
    (f : (a : α) → α) z = y → z = (f⁻¹ : (a : α) → α) x → x = (f : (a : α) → α) ((f⁻¹ : (a : α) → α) y : α)
pos₃ :
  ¬(f : (a : α) → α) z = x →
    (f : (a : α) → α) z = y →
      ¬z = (f⁻¹ : (a : α) → α) x → z = (f⁻¹ : (a : α) → α) y → x = (f : (a : α) → α) ((f⁻¹ : (a : α) → α) x : α)
⊢ (if (f : (a : α) → α) z = x then y else if (f : (a : α) → α) z = y then x else (f : (a : α) → α) z) =
    (f : (a : α) → α)
      (if z = (f⁻¹ : (a : α) → α) x then (f⁻¹ : (a : α) → α) y
        else if z = (f⁻¹ : (a : α) → α) y then (f⁻¹ : (a : α) → α) x else z :
        α)
have neg₁ : ¬(f : (a : α) → α) z = x →
  (f : (a : α) → α) z = y → ¬z = (f⁻¹ : (a : α) → α) x → ¬z = (f⁻¹ : (a : α) → α) y → x = (f : (a : α) → α) z
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Group.End (goal)
Goal:
α : Type u_4
inst : DecidableEq α
f : Perm α
x y z : α
pos : (f : (a : α) → α) z = x → z = (f⁻¹ : (a : α) → α) x → y = (f : (a : α) → α) ((f⁻¹ : (a : α) → α) y : α)
pos₁ :
  (f : (a : α) → α) z = x →
    ¬z = (f⁻¹ : (a : α) → α) x → z = (f⁻¹ : (a : α) → α) y → y = (f : (a : α) → α) ((f⁻¹ : (a : α) → α) x : α)
neg : (f : (a : α) → α) z = x → ¬z = (f⁻¹ : (a : α) → α) x → ¬z = (f⁻¹ : (a : α) → α) y → y = (f : (a : α) → α) z
pos₂ :
  ¬(f : (a : α) → α) z = x →
    (f : (a : α) → α) z = y → z = (f⁻¹ : (a : α) → α) x → x = (f : (a : α) → α) ((f⁻¹ : (a : α) → α) y : α)
pos₃ :
  ¬(f : (a : α) → α) z = x →
    (f : (a : α) → α) z = y →
      ¬z = (f⁻¹ : (a : α) → α) x → z = (f⁻¹ : (a : α) → α) y → x = (f : (a : α) → α) ((f⁻¹ : (a : α) → α) x : α)
neg₁ :
  ¬(f : (a : α) → α) z = x →
    (f : (a : α) → α) z = y → ¬z = (f⁻¹ : (a : α) → α) x → ¬z = (f⁻¹ : (a : α) → α) y → x = (f : (a : α) → α) z
⊢ (if (f : (a : α) → α) z = x then y else if (f : (a : α) → α) z = y then x else (f : (a : α) → α) z) =
    (f : (a : α) → α)
      (if z = (f⁻¹ : (a : α) → α) x then (f⁻¹ : (a : α) → α) y
        else if z = (f⁻¹ : (a : α) → α) y then (f⁻¹ : (a : α) → α) x else z :
        α)
have pos₄ : ¬(f : (a : α) → α) z = x →
  ¬(f : (a : α) → α) z = y →
    z = (f⁻¹ : (a : α) → α) x →
      Eq (α := α) ((f : (a : α) → α) z : α) ((f : (a : α) → α) ((f⁻¹ : (a : α) → α) y : α) : α)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Group.End (goal)
Goal:
α : Type u_4
inst : DecidableEq α
f : Perm α
x y z : α
pos : (f : (a : α) → α) z = x → z = (f⁻¹ : (a : α) → α) x → y = (f : (a : α) → α) ((f⁻¹ : (a : α) → α) y : α)
pos₁ :
  (f : (a : α) → α) z = x →
    ¬z = (f⁻¹ : (a : α) → α) x → z = (f⁻¹ : (a : α) → α) y → y = (f : (a : α) → α) ((f⁻¹ : (a : α) → α) x : α)
neg : (f : (a : α) → α) z = x → ¬z = (f⁻¹ : (a : α) → α) x → ¬z = (f⁻¹ : (a : α) → α) y → y = (f : (a : α) → α) z
pos₂ :
  ¬(f : (a : α) → α) z = x →
    (f : (a : α) → α) z = y → z = (f⁻¹ : (a : α) → α) x → x = (f : (a : α) → α) ((f⁻¹ : (a : α) → α) y : α)
pos₃ :
  ¬(f : (a : α) → α) z = x →
    (f : (a : α) → α) z = y →
      ¬z = (f⁻¹ : (a : α) → α) x → z = (f⁻¹ : (a : α) → α) y → x = (f : (a : α) → α) ((f⁻¹ : (a : α) → α) x : α)
neg₁ :
  ¬(f : (a : α) → α) z = x →
    (f : (a : α) → α) z = y → ¬z = (f⁻¹ : (a : α) → α) x → ¬z = (f⁻¹ : (a : α) → α) y → x = (f : (a : α) → α) z
pos₄ :
  ¬(f : (a : α) → α) z = x →
    ¬(f : (a : α) → α) z = y →
      z = (f⁻¹ : (a : α) → α) x →
        Eq (α := α) ((f : (a : α) → α) z : α) ((f : (a : α) → α) ((f⁻¹ : (a : α) → α) y : α) : α)
⊢ (if (f : (a : α) → α) z = x then y else if (f : (a : α) → α) z = y then x else (f : (a : α) → α) z) =
    (f : (a : α) → α)
      (if z = (f⁻¹ : (a : α) → α) x then (f⁻¹ : (a : α) → α) y
        else if z = (f⁻¹ : (a : α) → α) y then (f⁻¹ : (a : α) → α) x else z :
        α)
have pos₅ : ¬(f : (a : α) → α) z = x →
  ¬(f : (a : α) → α) z = y →
    ¬z = (f⁻¹ : (a : α) → α) x →
      z = (f⁻¹ : (a : α) → α) y →
        Eq (α := α) ((f : (a : α) → α) z : α) ((f : (a : α) → α) ((f⁻¹ : (a : α) → α) x : α) : α)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Group.End (goal)
Goal:
α : Type u_4
inst : DecidableEq α
f : Perm α
x y z : α
pos : (f : (a : α) → α) z = x → z = (f⁻¹ : (a : α) → α) x → y = (f : (a : α) → α) ((f⁻¹ : (a : α) → α) y : α)
pos₁ :
  (f : (a : α) → α) z = x →
    ¬z = (f⁻¹ : (a : α) → α) x → z = (f⁻¹ : (a : α) → α) y → y = (f : (a : α) → α) ((f⁻¹ : (a : α) → α) x : α)
neg : (f : (a : α) → α) z = x → ¬z = (f⁻¹ : (a : α) → α) x → ¬z = (f⁻¹ : (a : α) → α) y → y = (f : (a : α) → α) z
pos₂ :
  ¬(f : (a : α) → α) z = x →
    (f : (a : α) → α) z = y → z = (f⁻¹ : (a : α) → α) x → x = (f : (a : α) → α) ((f⁻¹ : (a : α) → α) y : α)
pos₃ :
  ¬(f : (a : α) → α) z = x →
    (f : (a : α) → α) z = y →
      ¬z = (f⁻¹ : (a : α) → α) x → z = (f⁻¹ : (a : α) → α) y → x = (f : (a : α) → α) ((f⁻¹ : (a : α) → α) x : α)
neg₁ :
  ¬(f : (a : α) → α) z = x →
    (f : (a : α) → α) z = y → ¬z = (f⁻¹ : (a : α) → α) x → ¬z = (f⁻¹ : (a : α) → α) y → x = (f : (a : α) → α) z
pos₄ :
  ¬(f : (a : α) → α) z = x →
    ¬(f : (a : α) → α) z = y →
      z = (f⁻¹ : (a : α) → α) x →
        Eq (α := α) ((f : (a : α) → α) z : α) ((f : (a : α) → α) ((f⁻¹ : (a : α) → α) y : α) : α)
pos₅ :
  ¬(f : (a : α) → α) z = x →
    ¬(f : (a : α) → α) z = y →
      ¬z = (f⁻¹ : (a : α) → α) x →
        z = (f⁻¹ : (a : α) → α) y →
          Eq (α := α) ((f : (a : α) → α) z : α) ((f : (a : α) → α) ((f⁻¹ : (a : α) → α) x : α) : α)
⊢ (if (f : (a : α) → α) z = x then y else if (f : (a : α) → α) z = y then x else (f : (a : α) → α) z) =
    (f : (a : α) → α)
      (if z = (f⁻¹ : (a : α) → α) x then (f⁻¹ : (a : α) → α) y
        else if z = (f⁻¹ : (a : α) → α) y then (f⁻¹ : (a : α) → α) x else z :
        α)
have neg₂ : ¬(f : (a : α) → α) z = x →
  ¬(f : (a : α) → α) z = y →
    ¬z = (f⁻¹ : (a : α) → α) x →
      ¬z = (f⁻¹ : (a : α) → α) y → Eq (α := α) ((f : (a : α) → α) z : α) ((f : (a : α) → α) z : α)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Group.End (goal)
Goal:
α : Type u_4
inst : DecidableEq α
f : Perm α
x y : α
⊢ swap ((f : (a : α) → α) x) ((f : (a : α) → α) y) = f * swap x y * f⁻¹
have rw : swap ((f : (a : α) → α) x) ((f : (a : α) → α) y) =
  HMul.hMul (α := Perm α) (swap ((f : (a : α) → α) x) ((f : (a : α) → α) y) : Perm α) f * f⁻¹
Tactic: rw [mul_swap_eq_swap_mul, mul_inv_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.End (goal)
Goal:
α : Type u_4
inst : DecidableEq α
f : Perm α
x y : α
rw :
  swap ((f : (a : α) → α) x) ((f : (a : α) → α) y) =
    HMul.hMul (α := Perm α) (swap ((f : (a : α) → α) x) ((f : (a : α) → α) y) : Perm α) f * f⁻¹
⊢ swap ((f : (a : α) → α) x) ((f : (a : α) → α) y) = f * swap x y * f⁻¹
have rw₁ : Eq (α := Perm α) (swap ((f : (a : α) → α) x) ((f : (a : α) → α) y) : Perm α)
  (swap ((f : (a : α) → α) x) ((f : (a : α) → α) y) : Perm α)
Tactic: rw [mul_swap_eq_swap_mul, mul_inv_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.End (goal)
Goal:
α : Type u_4
inst : DecidableEq α
i j : α
σ : Perm α
⊢ σ * swap i j * swap i j = σ
have rw : σ * (swap i j * swap i j) = σ
Tactic: rw [mul_assoc, swap_mul_self, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.End (goal)
Goal:
α : Type u_4
inst : DecidableEq α
i j : α
σ : Perm α
rw : σ * (swap i j * swap i j) = σ
⊢ σ * swap i j * swap i j = σ
have rw₁ : σ * 1 = σ
Tactic: rw [mul_assoc, swap_mul_self, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.End (goal)
Goal:
α : Type u_4
inst : DecidableEq α
i j : α
σ : Perm α
rw : σ * (swap i j * swap i j) = σ
rw₁ : σ * 1 = σ
⊢ σ * swap i j * swap i j = σ
have rw₂ : σ = σ
Tactic: rw [mul_assoc, swap_mul_self, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.End (goal)
Goal:
α : Type u_4
inst : DecidableEq α
i j : α
σ : Perm α
⊢ swap i j * σ = σ ↔ i = j
have rw : swap i j = 1 ↔ i = j
Tactic: rw [mul_eq_right, swap_eq_one_iff]
-- Lean 4 proof step from Mathlib.Algebra.Group.End (goal)
Goal:
α : Type u_4
inst : DecidableEq α
i j : α
σ : Perm α
rw : swap i j = 1 ↔ i = j
⊢ swap i j * σ = σ ↔ i = j
have rw₁ : i = j ↔ i = j
Tactic: rw [mul_eq_right, swap_eq_one_iff]
-- Lean 4 proof step from Mathlib.Algebra.Group.End (goal)
Goal:
α : Type u_4
inst : DecidableEq α
i j : α
σ : Perm α
⊢ σ * swap i j = σ ↔ i = j
have rw : swap i j = 1 ↔ i = j
Tactic: rw [mul_eq_left, swap_eq_one_iff]
-- Lean 4 proof step from Mathlib.Algebra.Group.End (goal)
Goal:
α : Type u_4
inst : DecidableEq α
i j : α
σ : Perm α
rw : swap i j = 1 ↔ i = j
⊢ σ * swap i j = σ ↔ i = j
have rw₁ : i = j ↔ i = j
Tactic: rw [mul_eq_left, swap_eq_one_iff]
-- Lean 4 proof step from Mathlib.Algebra.Group.End (goal)
Goal:
α : Type u_4
inst : DecidableEq α
x y z : α
hxy : x ≠ y
hxz : x ≠ z
⊢ swap y z * swap x y * swap y z = swap z x
have nth_rewrite : swap y z * swap x y * (swap y z)⁻¹ = swap z x
Tactic: nth_rewrite 3 [← swap_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.End (goal)
Goal:
α : Type u_4
inst : DecidableEq α
x y z : α
hxy : x ≠ y
hxz : x ≠ z
⊢ swap y z * swap x y * (swap y z)⁻¹ = swap z x
have rw : swap ((swap y z : (a : α) → α) x) ((swap y z : (a : α) → α) y) = swap z x
Tactic: rw [← swap_apply_apply, swap_apply_left, swap_apply_of_ne_of_ne hxy hxz, swap_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.End (goal)
Goal:
α : Type u_4
inst : DecidableEq α
x y z : α
hxy : x ≠ y
hxz : x ≠ z
rw : swap ((swap y z : (a : α) → α) x) ((swap y z : (a : α) → α) y) = swap z x
⊢ swap y z * swap x y * (swap y z)⁻¹ = swap z x
have rw₁ : swap ((swap y z : (a : α) → α) x) z = swap z x
Tactic: rw [← swap_apply_apply, swap_apply_left, swap_apply_of_ne_of_ne hxy hxz, swap_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.End (goal)
Goal:
α : Type u_4
inst : DecidableEq α
x y z : α
hxy : x ≠ y
hxz : x ≠ z
rw : swap ((swap y z : (a : α) → α) x) ((swap y z : (a : α) → α) y) = swap z x
rw₁ : swap ((swap y z : (a : α) → α) x) z = swap z x
⊢ swap y z * swap x y * (swap y z)⁻¹ = swap z x
have rw₂ : swap x z = swap z x
Tactic: rw [← swap_apply_apply, swap_apply_left, swap_apply_of_ne_of_ne hxy hxz, swap_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.End (goal)
Goal:
α : Type u_4
inst : DecidableEq α
x y z : α
hxy : x ≠ y
hxz : x ≠ z
rw : swap ((swap y z : (a : α) → α) x) ((swap y z : (a : α) → α) y) = swap z x
rw₁ : swap ((swap y z : (a : α) → α) x) z = swap z x
rw₂ : swap x z = swap z x
⊢ swap y z * swap x y * (swap y z)⁻¹ = swap z x
have rw₃ : swap z x = swap z x
Tactic: rw [← swap_apply_apply, swap_apply_left, swap_apply_of_ne_of_ne hxy hxz, swap_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.End (goal)
Goal:
α : Type u_4
inst : Group α
a : α
n : ℕ
⊢ Equiv.mulLeft a ^ n = Equiv.mulLeft (a ^ n)
have H : ∀ (x : α), Eq (α := α) ((Equiv.mulLeft a ^ n : (a : α) → α) x : α) ((Equiv.mulLeft (a ^ n) : (a : α) → α) x : α)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.End (goal)
Goal:
α : Type u_4
inst : Group α
a : α
n : ℕ
⊢ Equiv.mulRight a ^ n = Equiv.mulRight (a ^ n)
have H : ∀ (x : α), Eq (α := α) ((Equiv.mulRight a ^ n : (a : α) → α) x : α) ((Equiv.mulRight (a ^ n) : (a : α) → α) x : α)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.End (goal)
Goal:
M : Type u_2
inst : Mul M
e : MulAut M
m : M
⊢ Eq (α := M) ((e⁻¹ : (a : M) → M) m : M) ((MulEquiv.symm e : (a : M) → M) m : M)
have rw : Eq (α := M) ((MulEquiv.symm e : (a : M) → M) m : M) ((MulEquiv.symm e : (a : M) → M) m : M)
Tactic: rw [inv_def]
-- Lean 4 proof step from Mathlib.Algebra.Group.End (goal)
Goal:
A : Type u_1
M : Type u_2
G : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
inst : Mul M
inst_1 : Group G
⊢ Eq.{u_3 + 1} (α := MulAut G)
    { toFun := fun (h : G) ↦ 1 * h * 1⁻¹, invFun := fun (h : G) ↦ 1⁻¹ * h * 1, left_inv := ⋯, right_inv := ⋯,
      map_mul' := ⋯ }
    1
have h : ∀ (x : G),
  Eq (α := G)
    (({ toFun := fun (h : G) ↦ 1 * h * 1⁻¹, invFun := fun (h : G) ↦ 1⁻¹ * h * 1, left_inv := sorry, right_inv := sorry,
            map_mul' := sorry } :
          (a : G) → G)
        x :
      G)
    ((1 : (a : G) → G) x : G)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.End (goal)
Goal:
A : Type u_1
M : Type u_2
G : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
inst : Mul M
inst_1 : Group G
x x_1 : G
⊢ { toFun := fun (h : G) ↦ x * x_1 * h * (x * x_1)⁻¹, invFun := fun (h : G) ↦ (x * x_1)⁻¹ * h * (x * x_1),
      left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ } =
    HMul.hMul (α := MulAut G)
      { toFun := fun (h : G) ↦ x * h * x⁻¹, invFun := fun (h : G) ↦ x⁻¹ * h * x, left_inv := ⋯, right_inv := ⋯,
        map_mul' := ⋯ : G ≃* G }
      { toFun := fun (h : G) ↦ x_1 * h * x_1⁻¹, invFun := fun (h : G) ↦ x_1⁻¹ * h * x_1, left_inv := ⋯, right_inv := ⋯,
        map_mul' := ⋯ : G ≃* G }
have h : ∀ (x_2 : G),
  Eq (α := G)
    (({ toFun := fun (h : G) ↦ x * x_1 * h * (x * x_1)⁻¹, invFun := fun (h : G) ↦ (x * x_1)⁻¹ * h * (x * x_1),
            left_inv := sorry, right_inv := sorry, map_mul' := sorry } :
          (a : G) → G)
        x_2 :
      G)
    ((HMul.hMul (α := MulAut G)
            { toFun := fun (h : G) ↦ x * h * x⁻¹, invFun := fun (h : G) ↦ x⁻¹ * h * x, left_inv := sorry, right_inv := sorry,
              map_mul' := sorry : G ≃* G }
            { toFun := fun (h : G) ↦ x_1 * h * x_1⁻¹, invFun := fun (h : G) ↦ x_1⁻¹ * h * x_1, left_inv := sorry,
              right_inv := sorry, map_mul' := sorry : G ≃* G } :
          (a : G) → G)
        x_2 :
      G)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.End (goal)
Goal:
A : Type u_1
M : Type u_2
G : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
inst : Add A
inst_1 : AddGroup G
⊢ Eq.{u_3 + 1} (α := AddAut G)
    ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G)
        ((Additive.ofMul : (a : AddAut G) → Additive (AddAut G))
          { toFun := fun (h : G) ↦ 0 + h + -0, invFun := fun (h : G) ↦ -0 + h + 0, left_inv := ⋯, right_inv := ⋯,
            map_add' := ⋯ }) :
      AddAut G)
    ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) 0 : AddAut G)
have a : ∀ (x : G),
  Eq (α := G)
    ((((Additive.toMul : (a : Additive (AddAut G)) → AddAut G)
              ((Additive.ofMul : (a : AddAut G) → Additive (AddAut G))
                { toFun := fun (h : G) ↦ 0 + h + -0, invFun := fun (h : G) ↦ -0 + h + 0, left_inv := sorry, right_inv := sorry,
                  map_add' := sorry }) :
            AddAut G) :
          (a : G) → G)
        x :
      G)
    (((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) 0 : (a : G) → G) x : G)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.End (goal)
Goal:
A : Type u_1
M : Type u_2
G : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
inst : Add A
inst_1 : AddGroup G
x : G
⊢ Eq (α := G)
    ((((Additive.toMul : (a : Additive (AddAut G)) → AddAut G)
              ((Additive.ofMul : (a : AddAut G) → Additive (AddAut G))
                { toFun := fun (h : G) ↦ 0 + h + -0, invFun := fun (h : G) ↦ -0 + h + 0, left_inv := ⋯, right_inv := ⋯,
                  map_add' := ⋯ }) :
            AddAut G) :
          (a : G) → G)
        x :
      G)
    (((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) 0 : (a : G) → G) x : G)
have a : ({ toFun := fun (h : G) ↦ h, invFun := fun (h : G) ↦ h, left_inv := sorry, right_inv := sorry, map_add' := sorry } : (a : G) → G)
    x =
  x
Tactic: simp only [zero_add, neg_zero, add_zero, toMul_ofMul, toMul_zero, one_apply]