awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
R : Type u_1
inst : CommRing R
σ : Perm (Fin n)
f : Fin n → Fin n → R
hf : ∀ (i j : Fin n), f i j = -f j i
D : Finset ((_ : Fin n) × Fin n) := Finset.sigma (α := fun (i : Fin n) ↦ Fin n) Finset.univ Finset.Iio
hD : D = Finset.sigma (α := fun (i : Fin n) ↦ Fin n) Finset.univ Finset.Iio
x1 x2 : Fin n
⊢ (∃ (a : Fin n),
      ∃ b < a,
        max ((σ : (a : Fin n) → Fin n) a) ((σ : (a : Fin n) → Fin n) b) = x1 ∧
          min ((σ : (a : Fin n) → Fin n) a) ((σ : (a : Fin n) → Fin n) b) = x2) ↔
    x2 < x1
have h : (∃ (a : Fin n),
    ∃ b < a,
      max ((σ : (a : Fin n) → Fin n) a) ((σ : (a : Fin n) → Fin n) b) = x1 ∧
        min ((σ : (a : Fin n) → Fin n) a) ((σ : (a : Fin n) → Fin n) b) = x2) →
  x2 < x1
Tactic: refine ⟨?_, fun hlt ↦ ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
R : Type u_1
inst : CommRing R
σ : Perm (Fin n)
f : Fin n → Fin n → R
hf : ∀ (i j : Fin n), f i j = -f j i
D : Finset ((_ : Fin n) × Fin n) := Finset.sigma (α := fun (i : Fin n) ↦ Fin n) Finset.univ Finset.Iio
hD : D = Finset.sigma (α := fun (i : Fin n) ↦ Fin n) Finset.univ Finset.Iio
x1 x2 : Fin n
h :
  (∃ (a : Fin n),
      ∃ b < a,
        max ((σ : (a : Fin n) → Fin n) a) ((σ : (a : Fin n) → Fin n) b) = x1 ∧
          min ((σ : (a : Fin n) → Fin n) a) ((σ : (a : Fin n) → Fin n) b) = x2) →
    x2 < x1
⊢ (∃ (a : Fin n),
      ∃ b < a,
        max ((σ : (a : Fin n) → Fin n) a) ((σ : (a : Fin n) → Fin n) b) = x1 ∧
          min ((σ : (a : Fin n) → Fin n) a) ((σ : (a : Fin n) → Fin n) b) = x2) ↔
    x2 < x1
have h₁ : ∀ (hlt : x2 < x1),
  ∃ (a : Fin n),
    ∃ b < a,
      max ((σ : (a : Fin n) → Fin n) a) ((σ : (a : Fin n) → Fin n) b) = x1 ∧
        min ((σ : (a : Fin n) → Fin n) a) ((σ : (a : Fin n) → Fin n) b) = x2
Tactic: refine ⟨?_, fun hlt ↦ ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
R : Type u_1
inst : CommRing R
σ : Perm (Fin n)
f : Fin n → Fin n → R
hf : ∀ (i j : Fin n), f i j = -f j i
D : Finset ((_ : Fin n) × Fin n) := Finset.sigma (α := fun (i : Fin n) ↦ Fin n) Finset.univ Finset.Iio
hD : D = Finset.sigma (α := fun (i : Fin n) ↦ Fin n) Finset.univ Finset.Iio
x1 x2 : Fin n
hlt : x2 < x1
⊢ ∃ (a : Fin n),
    ∃ b < a,
      max ((σ : (a : Fin n) → Fin n) a) ((σ : (a : Fin n) → Fin n) b) = x1 ∧
        min ((σ : (a : Fin n) → Fin n) a) ((σ : (a : Fin n) → Fin n) b) = x2
have h : ∀
  (hlt' :
    LT.lt (α := Fin n) ((Equiv.symm σ : (a : Fin n) → Fin n) x1 : Fin n)
      ((Equiv.symm σ : (a : Fin n) → Fin n) x2 : Fin n)),
  ∃ (a : Fin n),
    ∃ b < a,
      max ((σ : (a : Fin n) → Fin n) a) ((σ : (a : Fin n) → Fin n) b) = x1 ∧
        min ((σ : (a : Fin n) → Fin n) a) ((σ : (a : Fin n) → Fin n) b) = x2
Tactic: obtain hlt' | hle := lt_or_ge (σ.symm x1) (σ.symm x2)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
R : Type u_1
inst : CommRing R
σ : Perm (Fin n)
f : Fin n → Fin n → R
hf : ∀ (i j : Fin n), f i j = -f j i
D : Finset ((_ : Fin n) × Fin n) := Finset.sigma (α := fun (i : Fin n) ↦ Fin n) Finset.univ Finset.Iio
hD : D = Finset.sigma (α := fun (i : Fin n) ↦ Fin n) Finset.univ Finset.Iio
x1 x2 : Fin n
hlt : x2 < x1
h :
  ∀
    (hlt' :
      LT.lt (α := Fin n) ((Equiv.symm σ : (a : Fin n) → Fin n) x1 : Fin n)
        ((Equiv.symm σ : (a : Fin n) → Fin n) x2 : Fin n)),
    ∃ (a : Fin n),
      ∃ b < a,
        max ((σ : (a : Fin n) → Fin n) a) ((σ : (a : Fin n) → Fin n) b) = x1 ∧
          min ((σ : (a : Fin n) → Fin n) a) ((σ : (a : Fin n) → Fin n) b) = x2
⊢ ∃ (a : Fin n),
    ∃ b < a,
      max ((σ : (a : Fin n) → Fin n) a) ((σ : (a : Fin n) → Fin n) b) = x1 ∧
        min ((σ : (a : Fin n) → Fin n) a) ((σ : (a : Fin n) → Fin n) b) = x2
have h₁ : ∀
  (hle :
    LE.le (α := Fin n) ((Equiv.symm σ : (a : Fin n) → Fin n) x2 : Fin n)
      ((Equiv.symm σ : (a : Fin n) → Fin n) x1 : Fin n)),
  ∃ (a : Fin n),
    ∃ b < a,
      max ((σ : (a : Fin n) → Fin n) a) ((σ : (a : Fin n) → Fin n) b) = x1 ∧
        min ((σ : (a : Fin n) → Fin n) a) ((σ : (a : Fin n) → Fin n) b) = x2
Tactic: obtain hlt' | hle := lt_or_ge (σ.symm x1) (σ.symm x2)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (hypothesis)
Goal:
n : ℕ
R : Type u_1
inst : CommRing R
σ : Perm (Fin n)
f : Fin n → Fin n → R
hf : ∀ (i j : Fin n), f i j = -f j i
D : Finset ((_ : Fin n) × Fin n) := Finset.sigma (α := fun (i : Fin n) ↦ Fin n) Finset.univ Finset.Iio
hD : D = Finset.sigma (α := fun (i : Fin n) ↦ Fin n) Finset.univ Finset.Iio
⊢ Eq.{u_1 + 1} (α := R)
    (∏ x ∈ D,
      f ((σ : (a : Fin n) → Fin n) (x.snd (β := fun (i : Fin n) ↦ Fin n)))
        ((σ : (a : Fin n) → Fin n) (x.fst (β := fun (i : Fin n) ↦ Fin n))))
    (∏ x ∈ D,
      (↑(↑(if
                    LT.lt (α := Fin n) ((σ⁻¹ : (a : Fin n) → Fin n) (x.snd (β := fun (i : Fin n) ↦ Fin n)) : Fin n)
                      ((σ⁻¹ : (a : Fin n) → Fin n) (x.fst (β := fun (i : Fin n) ↦ Fin n)) : Fin n) then
                  1
                else -1) :
              ℤ) :
          R) *
        f (x.snd (β := fun (i : Fin n) ↦ Fin n)) (x.fst (β := fun (i : Fin n) ↦ Fin n)))
have hφD : Finset.image
    (fun (x : (_ : Fin n) × Fin n) ↦
      Sigma.mk (β := fun (i : Fin n) ↦ Fin n)
        (max ((σ : (a : Fin n) → Fin n) (x.fst (β := fun (i : Fin n) ↦ Fin n)))
          ((σ : (a : Fin n) → Fin n) (x.snd (β := fun (i : Fin n) ↦ Fin n))))
        (min ((σ : (a : Fin n) → Fin n) (x.fst (β := fun (i : Fin n) ↦ Fin n)))
          ((σ : (a : Fin n) → Fin n) (x.snd (β := fun (i : Fin n) ↦ Fin n)))))
    D =
  D
Tactic: have hφD : D.image (fun x ↦ ⟨σ x.1 ⊔ σ x.2, σ x.1 ⊓ σ x.2⟩) = D := by
    ext ⟨x1, x2⟩
    suffices (∃ a, ∃ b < a, σ a ⊔ σ b = x1 ∧ σ a ⊓ σ b = x2) ↔ x2 < x1 by simpa [hD]
    refine ⟨?_, fun hlt ↦ ?_⟩
    · rintro ⟨i, j, hij, rfl, rfl⟩
      exact inf_le_sup.lt_of_ne <| by simp [hij.ne.symm]
    obtain hlt' | hle := lt_or_ge (σ.symm x1) (σ.symm x2)
    · exact ⟨_, _, hlt', by simp [hlt.le]⟩
    exact ⟨_, _, hle.lt_of_ne (by simp [hlt.ne]), by simp [hlt.le]⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
R : Type u_1
inst : CommRing R
σ : Perm (Fin n)
f : Fin n → Fin n → R
hf : ∀ (i j : Fin n), f i j = -f j i
D : Finset ((_ : Fin n) × Fin n) := Finset.sigma (α := fun (i : Fin n) ↦ Fin n) Finset.univ Finset.Iio
hD : D = Finset.sigma (α := fun (i : Fin n) ↦ Fin n) Finset.univ Finset.Iio
hφD :
  Finset.image
      (fun (x : (_ : Fin n) × Fin n) ↦
        Sigma.mk (β := fun (i : Fin n) ↦ Fin n)
          (max ((σ : (a : Fin n) → Fin n) (x.fst (β := fun (i : Fin n) ↦ Fin n)))
            ((σ : (a : Fin n) → Fin n) (x.snd (β := fun (i : Fin n) ↦ Fin n))))
          (min ((σ : (a : Fin n) → Fin n) (x.fst (β := fun (i : Fin n) ↦ Fin n)))
            ((σ : (a : Fin n) → Fin n) (x.snd (β := fun (i : Fin n) ↦ Fin n)))))
      D =
    D
⊢ Eq.{u_1 + 1} (α := R)
    (∏ x ∈ D,
      f ((σ : (a : Fin n) → Fin n) (x.snd (β := fun (i : Fin n) ↦ Fin n)))
        ((σ : (a : Fin n) → Fin n) (x.fst (β := fun (i : Fin n) ↦ Fin n))))
    (∏ x ∈ D,
      (↑(↑(if
                    LT.lt (α := Fin n) ((σ⁻¹ : (a : Fin n) → Fin n) (x.snd (β := fun (i : Fin n) ↦ Fin n)) : Fin n)
                      ((σ⁻¹ : (a : Fin n) → Fin n) (x.fst (β := fun (i : Fin n) ↦ Fin n)) : Fin n) then
                  1
                else -1) :
              ℤ) :
          R) *
        f (x.snd (β := fun (i : Fin n) ↦ Fin n)) (x.fst (β := fun (i : Fin n) ↦ Fin n)))
have nth_rw : Eq.{u_1 + 1} (α := R)
  (∏ x ∈ D,
    f ((σ : (a : Fin n) → Fin n) (x.snd (β := fun (i : Fin n) ↦ Fin n)))
      ((σ : (a : Fin n) → Fin n) (x.fst (β := fun (i : Fin n) ↦ Fin n))))
  (∏
    x ∈
      Finset.image
        (fun (x : (_ : Fin n) × Fin n) ↦
          Sigma.mk (β := fun (i : Fin n) ↦ Fin n)
            (max ((σ : (a : Fin n) → Fin n) (x.fst (β := fun (i : Fin n) ↦ Fin n)))
              ((σ : (a : Fin n) → Fin n) (x.snd (β := fun (i : Fin n) ↦ Fin n))))
            (min ((σ : (a : Fin n) → Fin n) (x.fst (β := fun (i : Fin n) ↦ Fin n)))
              ((σ : (a : Fin n) → Fin n) (x.snd (β := fun (i : Fin n) ↦ Fin n)))))
        D,
    (↑(↑(if
                  LT.lt (α := Fin n) ((σ⁻¹ : (a : Fin n) → Fin n) (x.snd (β := fun (i : Fin n) ↦ Fin n)) : Fin n)
                    ((σ⁻¹ : (a : Fin n) → Fin n) (x.fst (β := fun (i : Fin n) ↦ Fin n)) : Fin n) then
                1
              else -1) :
            ℤ) :
        R) *
      f (x.snd (β := fun (i : Fin n) ↦ Fin n)) (x.fst (β := fun (i : Fin n) ↦ Fin n)))
Tactic: nth_rw 2 [← hφD]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
R : Type u_1
inst : CommRing R
σ : Perm (Fin n)
f : Fin n → Fin n → R
hf : ∀ (i j : Fin n), f i j = -f j i
D : Finset ((_ : Fin n) × Fin n) := Finset.sigma (α := fun (i : Fin n) ↦ Fin n) Finset.univ Finset.Iio
hD : D = Finset.sigma (α := fun (i : Fin n) ↦ Fin n) Finset.univ Finset.Iio
hφD :
  Finset.image
      (fun (x : (_ : Fin n) × Fin n) ↦
        Sigma.mk (β := fun (i : Fin n) ↦ Fin n)
          (max ((σ : (a : Fin n) → Fin n) (x.fst (β := fun (i : Fin n) ↦ Fin n)))
            ((σ : (a : Fin n) → Fin n) (x.snd (β := fun (i : Fin n) ↦ Fin n))))
          (min ((σ : (a : Fin n) → Fin n) (x.fst (β := fun (i : Fin n) ↦ Fin n)))
            ((σ : (a : Fin n) → Fin n) (x.snd (β := fun (i : Fin n) ↦ Fin n)))))
      D =
    D
x : (_ : Fin n) × Fin n
hx : x ∈ (↑D : Set ((_ : Fin n) × Fin n))
y : (_ : Fin n) × Fin n
hy : y ∈ (↑D : Set ((_ : Fin n) × Fin n))
⊢ Finset.card (α := (_ : Fin n) × Fin n)
      (Finset.image
        (fun (x : (_ : Fin n) × Fin n) ↦
          Sigma.mk (β := fun (i : Fin n) ↦ Fin n)
            (max ((σ : (a : Fin n) → Fin n) (x.fst (β := fun (i : Fin n) ↦ Fin n)))
              ((σ : (a : Fin n) → Fin n) (x.snd (β := fun (i : Fin n) ↦ Fin n))))
            (min ((σ : (a : Fin n) → Fin n) (x.fst (β := fun (i : Fin n) ↦ Fin n)))
              ((σ : (a : Fin n) → Fin n) (x.snd (β := fun (i : Fin n) ↦ Fin n)))))
        D) =
    D.card
have rw : D.card = D.card
Tactic: rw [hφD]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
R : Type u_1
inst : CommRing R
σ : Perm (Fin n)
f : Fin n → Fin n → R
hf : ∀ (i j : Fin n), f i j = -f j i
⊢ ∏ i : Fin n, ∏ j ∈ Finset.Ioi i, f ((σ : (a : Fin n) → Fin n) i) ((σ : (a : Fin n) → Fin n) j) =
    HMul.hMul (α := R) (↑(↑((sign : (a : Perm (Fin n)) → ℤˣ) σ) : ℤ) : R) (∏ i : Fin n, ∏ j ∈ Finset.Ioi i, f i j)
have h : Eq.{u_1 + 1} (α := R) (∏ i : Fin n, ∏ j ∈ Finset.Ioi i, f ((σ : (a : Fin n) → Fin n) i) ((σ : (a : Fin n) → Fin n) j))
  (∏ j : Fin n, ∏ i ∈ Finset.Iio j, f ((σ : (a : Fin n) → Fin n) i) ((σ : (a : Fin n) → Fin n) j))
Tactic: convert! σ.prod_Iio_comp_eq_sign_mul_prod hf using 1
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
R : Type u_1
inst : CommRing R
σ : Perm (Fin n)
f : Fin n → Fin n → R
hf : ∀ (i j : Fin n), f i j = -f j i
h :
  Eq.{u_1 + 1} (α := R) (∏ i : Fin n, ∏ j ∈ Finset.Ioi i, f ((σ : (a : Fin n) → Fin n) i) ((σ : (a : Fin n) → Fin n) j))
    (∏ j : Fin n, ∏ i ∈ Finset.Iio j, f ((σ : (a : Fin n) → Fin n) i) ((σ : (a : Fin n) → Fin n) j))
⊢ ∏ i : Fin n, ∏ j ∈ Finset.Ioi i, f ((σ : (a : Fin n) → Fin n) i) ((σ : (a : Fin n) → Fin n) j) =
    HMul.hMul (α := R) (↑(↑((sign : (a : Perm (Fin n)) → ℤˣ) σ) : ℤ) : R) (∏ i : Fin n, ∏ j ∈ Finset.Ioi i, f i j)
have h₁ : HMul.hMul (α := R) (↑(↑((sign : (a : Perm (Fin n)) → ℤˣ) σ) : ℤ) : R) (∏ i : Fin n, ∏ j ∈ Finset.Ioi i, f i j) =
  HMul.hMul (α := R) (↑(↑((sign : (a : Perm (Fin n)) → ℤˣ) σ) : ℤ) : R) (∏ j : Fin n, ∏ i ∈ Finset.Iio j, f i j)
Tactic: convert! σ.prod_Iio_comp_eq_sign_mul_prod hf using 1
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
R : Type u_1
inst : CommRing R
σ : Perm (Fin n)
f : Fin n → Fin n → R
hf : ∀ (i j : Fin n), f i j = -f j i
⊢ HMul.hMul (α := R) (↑(↑((sign : (a : Perm (Fin n)) → ℤˣ) σ) : ℤ) : R) (∏ i : Fin n, ∏ j ∈ Finset.Ioi i, f i j) =
    HMul.hMul (α := R) (↑(↑((sign : (a : Perm (Fin n)) → ℤˣ) σ) : ℤ) : R) (∏ j : Fin n, ∏ i ∈ Finset.Iio j, f i j)
have h : Eq.{u_1 + 1} (α := R) (∏ j : Fin n, ∏ i ∈ Finset.Iio j, f i j) (∏ i : Fin n, ∏ j ∈ Finset.Ioi i, f i j)
Tactic: convert! rfl using 2
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
σ τ : Perm α
f : { x : α // x ∈ (↑σ.support : Set α) } ≃ { x : α // x ∈ (↑τ.support : Set α) }
hf :
  ∀ (x : α) (hx : x ∈ (↑σ.support : Set α)),
    Eq (α := α)
      ((↑((f : (a : { x : α // x ∈ (↑σ.support : Set α) }) → { x : α // x ∈ (↑τ.support : Set α) })
              (Subtype.mk (p := fun (x : α) ↦ x ∈ (↑σ.support : Set α)) ((σ : (a : α) → α) x) ⋯)) :
          α) :
        α)
      ((τ : (a : α) → α)
          (↑((f : (a : { x : α // x ∈ (↑σ.support : Set α) }) → { x : α // x ∈ (↑τ.support : Set α) })
                (Subtype.mk (p := fun (x : α) ↦ x ∈ (↑σ.support : Set α)) x hx)) :
            α) :
        α)
⊢ IsConj σ τ
have refine : f.extendSubtype (p := Membership.mem (↑σ.support : Set α)) (q := Membership.mem (↑τ.support : Set α)) * σ *
    (f.extendSubtype (p := Membership.mem (↑σ.support : Set α)) (q := Membership.mem (↑τ.support : Set α)))⁻¹ =
  τ
Tactic: refine isConj_iff.2 ⟨Equiv.extendSubtype f, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
σ τ : Perm α
f : { x : α // x ∈ (↑σ.support : Set α) } ≃ { x : α // x ∈ (↑τ.support : Set α) }
hf :
  ∀ (x : α) (hx : x ∈ (↑σ.support : Set α)),
    Eq (α := α)
      ((↑((f : (a : { x : α // x ∈ (↑σ.support : Set α) }) → { x : α // x ∈ (↑τ.support : Set α) })
              (Subtype.mk (p := fun (x : α) ↦ x ∈ (↑σ.support : Set α)) ((σ : (a : α) → α) x) ⋯)) :
          α) :
        α)
      ((τ : (a : α) → α)
          (↑((f : (a : { x : α // x ∈ (↑σ.support : Set α) }) → { x : α // x ∈ (↑τ.support : Set α) })
                (Subtype.mk (p := fun (x : α) ↦ x ∈ (↑σ.support : Set α)) x hx)) :
            α) :
        α)
⊢ f.extendSubtype (p := Membership.mem (↑σ.support : Set α)) (q := Membership.mem (↑τ.support : Set α)) * σ *
      (f.extendSubtype (p := Membership.mem (↑σ.support : Set α)) (q := Membership.mem (↑τ.support : Set α)))⁻¹ =
    τ
have rw : f.extendSubtype (p := Membership.mem (↑σ.support : Set α)) (q := Membership.mem (↑τ.support : Set α)) * σ =
  τ * f.extendSubtype (p := Membership.mem (↑σ.support : Set α)) (q := Membership.mem (↑τ.support : Set α))
Tactic: rw [mul_inv_eq_iff_eq_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
σ τ : Perm α
f : { x : α // x ∈ (↑σ.support : Set α) } ≃ { x : α // x ∈ (↑τ.support : Set α) }
hf :
  ∀ (x : α) (hx : x ∈ (↑σ.support : Set α)),
    Eq (α := α)
      ((↑((f : (a : { x : α // x ∈ (↑σ.support : Set α) }) → { x : α // x ∈ (↑τ.support : Set α) })
              (Subtype.mk (p := fun (x : α) ↦ x ∈ (↑σ.support : Set α)) ((σ : (a : α) → α) x) ⋯)) :
          α) :
        α)
      ((τ : (a : α) → α)
          (↑((f : (a : { x : α // x ∈ (↑σ.support : Set α) }) → { x : α // x ∈ (↑τ.support : Set α) })
                (Subtype.mk (p := fun (x : α) ↦ x ∈ (↑σ.support : Set α)) x hx)) :
            α) :
        α)
⊢ f.extendSubtype (p := Membership.mem (↑σ.support : Set α)) (q := Membership.mem (↑τ.support : Set α)) * σ =
    τ * f.extendSubtype (p := Membership.mem (↑σ.support : Set α)) (q := Membership.mem (↑τ.support : Set α))
have H : ∀ (x : α),
  Eq (α := α)
    ((f.extendSubtype (p := Membership.mem (↑σ.support : Set α)) (q := Membership.mem (↑τ.support : Set α)) * σ :
          (a : α) → α)
        x :
      α)
    ((τ * f.extendSubtype (p := Membership.mem (↑σ.support : Set α)) (q := Membership.mem (↑τ.support : Set α)) :
          (a : α) → α)
        x :
      α)
Tactic: ext x
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
σ τ : Perm α
f : { x : α // x ∈ (↑σ.support : Set α) } ≃ { x : α // x ∈ (↑τ.support : Set α) }
hf :
  ∀ (x : α) (hx : x ∈ (↑σ.support : Set α)),
    Eq (α := α)
      ((↑((f : (a : { x : α // x ∈ (↑σ.support : Set α) }) → { x : α // x ∈ (↑τ.support : Set α) })
              (Subtype.mk (p := fun (x : α) ↦ x ∈ (↑σ.support : Set α)) ((σ : (a : α) → α) x) ⋯)) :
          α) :
        α)
      ((τ : (a : α) → α)
          (↑((f : (a : { x : α // x ∈ (↑σ.support : Set α) }) → { x : α // x ∈ (↑τ.support : Set α) })
                (Subtype.mk (p := fun (x : α) ↦ x ∈ (↑σ.support : Set α)) x hx)) :
            α) :
        α)
x : α
⊢ Eq (α := α)
    ((f.extendSubtype (p := Membership.mem (↑σ.support : Set α)) (q := Membership.mem (↑τ.support : Set α)) * σ :
          (a : α) → α)
        x :
      α)
    ((τ * f.extendSubtype (p := Membership.mem (↑σ.support : Set α)) (q := Membership.mem (↑τ.support : Set α)) :
          (a : α) → α)
        x :
      α)
have H : Eq (α := α)
  ((f.extendSubtype (p := Membership.mem (↑σ.support : Set α)) (q := Membership.mem (↑τ.support : Set α)) : (a : α) → α)
      ((σ : (a : α) → α) x : α) :
    α)
  ((τ : (a : α) → α)
      ((f.extendSubtype (p := Membership.mem (↑σ.support : Set α)) (q := Membership.mem (↑τ.support : Set α)) :
            (a : α) → α)
          x :
        α) :
    α)
Tactic: simp only [Perm.mul_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
σ τ : Perm α
f : { x : α // x ∈ (↑σ.support : Set α) } ≃ { x : α // x ∈ (↑τ.support : Set α) }
hf :
  ∀ (x : α) (hx : x ∈ (↑σ.support : Set α)),
    Eq (α := α)
      ((↑((f : (a : { x : α // x ∈ (↑σ.support : Set α) }) → { x : α // x ∈ (↑τ.support : Set α) })
              (Subtype.mk (p := fun (x : α) ↦ x ∈ (↑σ.support : Set α)) ((σ : (a : α) → α) x) ⋯)) :
          α) :
        α)
      ((τ : (a : α) → α)
          (↑((f : (a : { x : α // x ∈ (↑σ.support : Set α) }) → { x : α // x ∈ (↑τ.support : Set α) })
                (Subtype.mk (p := fun (x : α) ↦ x ∈ (↑σ.support : Set α)) x hx)) :
            α) :
        α)
x : α
⊢ Eq (α := α)
    ((f.extendSubtype (p := Membership.mem (↑σ.support : Set α)) (q := Membership.mem (↑τ.support : Set α)) :
          (a : α) → α)
        ((σ : (a : α) → α) x : α) :
      α)
    ((τ : (a : α) → α)
        ((f.extendSubtype (p := Membership.mem (↑σ.support : Set α)) (q := Membership.mem (↑τ.support : Set α)) :
              (a : α) → α)
            x :
          α) :
      α)
have pos : ∀ (hx : x ∈ σ.support),
  Eq (α := α)
    ((f.extendSubtype (p := Membership.mem (↑σ.support : Set α)) (q := Membership.mem (↑τ.support : Set α)) :
          (a : α) → α)
        ((σ : (a : α) → α) x : α) :
      α)
    ((τ : (a : α) → α)
        ((f.extendSubtype (p := Membership.mem (↑σ.support : Set α)) (q := Membership.mem (↑τ.support : Set α)) :
              (a : α) → α)
            x :
          α) :
      α)
Tactic: by_cases hx : x ∈ σ.support
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
σ τ : Perm α
f : { x : α // x ∈ (↑σ.support : Set α) } ≃ { x : α // x ∈ (↑τ.support : Set α) }
hf :
  ∀ (x : α) (hx : x ∈ (↑σ.support : Set α)),
    Eq (α := α)
      ((↑((f : (a : { x : α // x ∈ (↑σ.support : Set α) }) → { x : α // x ∈ (↑τ.support : Set α) })
              (Subtype.mk (p := fun (x : α) ↦ x ∈ (↑σ.support : Set α)) ((σ : (a : α) → α) x) ⋯)) :
          α) :
        α)
      ((τ : (a : α) → α)
          (↑((f : (a : { x : α // x ∈ (↑σ.support : Set α) }) → { x : α // x ∈ (↑τ.support : Set α) })
                (Subtype.mk (p := fun (x : α) ↦ x ∈ (↑σ.support : Set α)) x hx)) :
            α) :
        α)
x : α
pos :
  ∀ (hx : x ∈ σ.support),
    Eq (α := α)
      ((f.extendSubtype (p := Membership.mem (↑σ.support : Set α)) (q := Membership.mem (↑τ.support : Set α)) :
            (a : α) → α)
          ((σ : (a : α) → α) x : α) :
        α)
      ((τ : (a : α) → α)
          ((f.extendSubtype (p := Membership.mem (↑σ.support : Set α)) (q := Membership.mem (↑τ.support : Set α)) :
                (a : α) → α)
              x :
            α) :
        α)
⊢ Eq (α := α)
    ((f.extendSubtype (p := Membership.mem (↑σ.support : Set α)) (q := Membership.mem (↑τ.support : Set α)) :
          (a : α) → α)
        ((σ : (a : α) → α) x : α) :
      α)
    ((τ : (a : α) → α)
        ((f.extendSubtype (p := Membership.mem (↑σ.support : Set α)) (q := Membership.mem (↑τ.support : Set α)) :
              (a : α) → α)
            x :
          α) :
      α)
have neg : ∀ (hx : x ∉ σ.support),
  Eq (α := α)
    ((f.extendSubtype (p := Membership.mem (↑σ.support : Set α)) (q := Membership.mem (↑τ.support : Set α)) :
          (a : α) → α)
        ((σ : (a : α) → α) x : α) :
      α)
    ((τ : (a : α) → α)
        ((f.extendSubtype (p := Membership.mem (↑σ.support : Set α)) (q := Membership.mem (↑τ.support : Set α)) :
              (a : α) → α)
            x :
          α) :
      α)
Tactic: by_cases hx : x ∈ σ.support
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
σ τ : Perm α
f : { x : α // x ∈ (↑σ.support : Set α) } ≃ { x : α // x ∈ (↑τ.support : Set α) }
hf :
  ∀ (x : α) (hx : x ∈ (↑σ.support : Set α)),
    Eq (α := α)
      ((↑((f : (a : { x : α // x ∈ (↑σ.support : Set α) }) → { x : α // x ∈ (↑τ.support : Set α) })
              (Subtype.mk (p := fun (x : α) ↦ x ∈ (↑σ.support : Set α)) ((σ : (a : α) → α) x) ⋯)) :
          α) :
        α)
      ((τ : (a : α) → α)
          (↑((f : (a : { x : α // x ∈ (↑σ.support : Set α) }) → { x : α // x ∈ (↑τ.support : Set α) })
                (Subtype.mk (p := fun (x : α) ↦ x ∈ (↑σ.support : Set α)) x hx)) :
            α) :
        α)
x : α
hx : x ∈ σ.support
⊢ Eq (α := α)
    ((f.extendSubtype (p := Membership.mem (↑σ.support : Set α)) (q := Membership.mem (↑τ.support : Set α)) :
          (a : α) → α)
        ((σ : (a : α) → α) x : α) :
      α)
    ((τ : (a : α) → α)
        ((f.extendSubtype (p := Membership.mem (↑σ.support : Set α)) (q := Membership.mem (↑τ.support : Set α)) :
              (a : α) → α)
            x :
          α) :
      α)
have pos : Eq (α := α)
  ((↑((f : (a : { x : α // x ∈ (↑σ.support : Set α) }) → { x : α // x ∈ (↑τ.support : Set α) })
          (Subtype.mk (p := fun (x : α) ↦ x ∈ (↑σ.support : Set α)) ((σ : (a : α) → α) x) sorry)) :
      α) :
    α)
  ((τ : (a : α) → α)
      (↑((f : (a : { x : α // x ∈ (↑σ.support : Set α) }) → { x : α // x ∈ (↑τ.support : Set α) })
            (Subtype.mk (p := fun (x : α) ↦ x ∈ (↑σ.support : Set α)) x sorry)) :
        α) :
    α)
Tactic: rw [Equiv.extendSubtype_apply_of_mem, Equiv.extendSubtype_apply_of_mem]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
σ τ : Perm α
f : { x : α // x ∈ (↑σ.support : Set α) } ≃ { x : α // x ∈ (↑τ.support : Set α) }
hf :
  ∀ (x : α) (hx : x ∈ (↑σ.support : Set α)),
    Eq (α := α)
      ((↑((f : (a : { x : α // x ∈ (↑σ.support : Set α) }) → { x : α // x ∈ (↑τ.support : Set α) })
              (Subtype.mk (p := fun (x : α) ↦ x ∈ (↑σ.support : Set α)) ((σ : (a : α) → α) x) ⋯)) :
          α) :
        α)
      ((τ : (a : α) → α)
          (↑((f : (a : { x : α // x ∈ (↑σ.support : Set α) }) → { x : α // x ∈ (↑τ.support : Set α) })
                (Subtype.mk (p := fun (x : α) ↦ x ∈ (↑σ.support : Set α)) x hx)) :
            α) :
        α)
x : α
hx : x ∈ σ.support
pos :
  Eq (α := α)
    ((↑((f : (a : { x : α // x ∈ (↑σ.support : Set α) }) → { x : α // x ∈ (↑τ.support : Set α) })
            (Subtype.mk (p := fun (x : α) ↦ x ∈ (↑σ.support : Set α)) ((σ : (a : α) → α) x) ⋯)) :
        α) :
      α)
    ((τ : (a : α) → α)
        (↑((f : (a : { x : α // x ∈ (↑σ.support : Set α) }) → { x : α // x ∈ (↑τ.support : Set α) })
              (Subtype.mk (p := fun (x : α) ↦ x ∈ (↑σ.support : Set α)) x ⋯)) :
          α) :
      α)
⊢ Eq (α := α)
    ((f.extendSubtype (p := Membership.mem (↑σ.support : Set α)) (q := Membership.mem (↑τ.support : Set α)) :
          (a : α) → α)
        ((σ : (a : α) → α) x : α) :
      α)
    ((τ : (a : α) → α)
        ((f.extendSubtype (p := Membership.mem (↑σ.support : Set α)) (q := Membership.mem (↑τ.support : Set α)) :
              (a : α) → α)
            x :
          α) :
      α)
have pos₁ : x ∈ (↑σ.support : Set α)
Tactic: rw [Equiv.extendSubtype_apply_of_mem, Equiv.extendSubtype_apply_of_mem]