Module: Mathlib.LinearAlgebra.RootSystem.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
p₁ : M →ₗ[R] N →ₗ[R] R
isPerfPair_toLinearMap✝¹ : p₁.IsPerfPair
root✝¹ : ι ↪ M
coroot✝¹ : ι ↪ N
root_coroot_two✝¹ : ∀ (i : ι), (p₁ (root✝¹ i)) (coroot✝¹ i) = 2
reflectionPerm✝¹ : ι → ι ≃ ι
reflectionPerm_root✝¹ :
  ∀ (i j : ι), root✝¹ j - (p₁ (root✝¹ j)) (coroot✝¹ i) • root✝¹ i = root✝¹ ((reflectionPerm✝¹ i) j)
reflectionPerm_coroot✝¹ :
  ∀ (i j : ι), coroot✝¹ j - (p₁ (root✝¹ i)) (coroot✝¹ j) • coroot✝¹ i = coroot✝¹ ((reflectionPerm✝¹ i) j)
p₂ : M →ₗ[R] N →ₗ[R] R
isPerfPair_toLinearMap✝ : p₂.IsPerfPair
root✝ : ι ↪ M
coroot✝ : ι ↪ N
root_coroot_two✝ : ∀ (i : ι), (p₂ (root✝ i)) (coroot✝ i) = 2
reflectionPerm✝ : ι → ι ≃ ι
reflectionPerm_root✝ : ∀ (i j : ι), root✝ j - (p₂ (root✝ j)) (coroot✝ i) • root✝ i = root✝ ((reflectionPerm✝ i) j)
reflectionPerm_coroot✝ :
  ∀ (i j : ι), coroot✝ j - (p₂ (root✝ i)) (coroot✝ j) • coroot✝ i = coroot✝ ((reflectionPerm✝ i) j)
he :
  { toLinearMap := p₁, isPerfPair_toLinearMap := isPerfPair_toLinearMap✝¹, root := root✝¹, coroot := coroot✝¹,
        root_coroot_two := root_coroot_two✝¹, reflectionPerm := reflectionPerm✝¹,
        reflectionPerm_root := reflectionPerm_root✝¹, reflectionPerm_coroot := reflectionPerm_coroot✝¹ }.toLinearMap =
    { toLinearMap := p₂, isPerfPair_toLinearMap := isPerfPair_toLinearMap✝, root := root✝, coroot := coroot✝,
        root_coroot_two := root_coroot_two✝, reflectionPerm := reflectionPerm✝,
        reflectionPerm_root := reflectionPerm_root✝, reflectionPerm_coroot := reflectionPerm_coroot✝ }.toLinearMap
hr :
  { toLinearMap := p₁, isPerfPair_toLinearMap := isPerfPair_toLinearMap✝¹, root := root✝¹, coroot := coroot✝¹,
        root_coroot_two := root_coroot_two✝¹, reflectionPerm := reflectionPerm✝¹,
        reflectionPerm_root := reflectionPerm_root✝¹, reflectionPerm_coroot := reflectionPerm_coroot✝¹ }.root =
    { toLinearMap := p₂, isPerfPair_toLinearMap := isPerfPair_toLinearMap✝, root := root✝, coroot := coroot✝,
        root_coroot_two := root_coroot_two✝, reflectionPerm := reflectionPerm✝,
        reflectionPerm_root := reflectionPerm_root✝, reflectionPerm_coroot := reflectionPerm_coroot✝ }.root
hc :
  range
      ⇑{ toLinearMap := p₁, isPerfPair_toLinearMap := isPerfPair_toLinearMap✝¹, root := root✝¹, coroot := coroot✝¹,
            root_coroot_two := root_coroot_two✝¹, reflectionPerm := reflectionPerm✝¹,
            reflectionPerm_root := reflectionPerm_root✝¹, reflectionPerm_coroot := reflectionPerm_coroot✝¹ }.coroot =
    range
      ⇑{ toLinearMap := p₂, isPerfPair_toLinearMap := isPerfPair_toLinearMap✝, root := root✝, coroot := coroot✝,
            root_coroot_two := root_coroot_two✝, reflectionPerm := reflectionPerm✝,
            reflectionPerm_root := reflectionPerm_root✝, reflectionPerm_coroot := reflectionPerm_coroot✝ }.coroot
hp :
  { toLinearMap := p₁, isPerfPair_toLinearMap := isPerfPair_toLinearMap✝¹, root := root✝¹, coroot := coroot✝¹,
          root_coroot_two := root_coroot_two✝¹, reflectionPerm := reflectionPerm✝¹,
          reflectionPerm_root := reflectionPerm_root✝¹, reflectionPerm_coroot := reflectionPerm_coroot✝¹ }.coroot =
      { toLinearMap := p₂, isPerfPair_toLinearMap := isPerfPair_toLinearMap✝, root := root✝, coroot := coroot✝,
          root_coroot_two := root_coroot_two✝, reflectionPerm := reflectionPerm✝,
          reflectionPerm_root := reflectionPerm_root✝, reflectionPerm_coroot := reflectionPerm_coroot✝ }.coroot →
    { toLinearMap := p₁, isPerfPair_toLinearMap := isPerfPair_toLinearMap✝¹, root := root✝¹, coroot := coroot✝¹,
          root_coroot_two := root_coroot_two✝¹, reflectionPerm := reflectionPerm✝¹,
          reflectionPerm_root := reflectionPerm_root✝¹,
          reflectionPerm_coroot := reflectionPerm_coroot✝¹ }.reflectionPerm =
      { toLinearMap := p₂, isPerfPair_toLinearMap := isPerfPair_toLinearMap✝, root := root✝, coroot := coroot✝,
          root_coroot_two := root_coroot_two✝, reflectionPerm := reflectionPerm✝,
          reflectionPerm_root := reflectionPerm_root✝, reflectionPerm_coroot := reflectionPerm_coroot✝ }.reflectionPerm
this :
  { toLinearMap := p₁, isPerfPair_toLinearMap := isPerfPair_toLinearMap✝¹, root := root✝¹, coroot := coroot✝¹,
        root_coroot_two := root_coroot_two✝¹, reflectionPerm := reflectionPerm✝¹,
        reflectionPerm_root := reflectionPerm_root✝¹, reflectionPerm_coroot := reflectionPerm_coroot✝¹ }.coroot =
    { toLinearMap := p₂, isPerfPair_toLinearMap := isPerfPair_toLinearMap✝, root := root✝, coroot := coroot✝,
        root_coroot_two := root_coroot_two✝, reflectionPerm := reflectionPerm✝,
        reflectionPerm_root := reflectionPerm_root✝, reflectionPerm_coroot := reflectionPerm_coroot✝ }.coroot
⊢ { toLinearMap := p₁, isPerfPair_toLinearMap := isPerfPair_toLinearMap✝¹, root := root✝¹, coroot := coroot✝¹,
      root_coroot_two := root_coroot_two✝¹, reflectionPerm := reflectionPerm✝¹,
      reflectionPerm_root := reflectionPerm_root✝¹, reflectionPerm_coroot := reflectionPerm_coroot✝¹ } =
    { toLinearMap := p₂, isPerfPair_toLinearMap := isPerfPair_toLinearMap✝, root := root✝, coroot := coroot✝,
      root_coroot_two := root_coroot_two✝, reflectionPerm := reflectionPerm✝,
      reflectionPerm_root := reflectionPerm_root✝, reflectionPerm_coroot := reflectionPerm_coroot✝ }

Tactic:
#adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
    (replacing grind's canonicalizer with a type-directed normalizer), `grind` closed this goal.
    It is not yet clear whether this is due to defeq abuse in Mathlib or a problem in the new
    canonicalizer; a minimization would help. The original proof was: `grind` -/

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
p₁ : M →ₗ[R] N →ₗ[R] R
isPerfPair_toLinearMap✝¹ : p₁.IsPerfPair
root✝¹ : ι ↪ M
coroot✝¹ : ι ↪ N
root_coroot_two✝¹ : ∀ (i : ι), (p₁ (root✝¹ i)) (coroot✝¹ i) = 2
reflectionPerm✝¹ : ι → ι ≃ ι
reflectionPerm_root✝¹ :
  ∀ (i j : ι), root✝¹ j - (p₁ (root✝¹ j)) (coroot✝¹ i) • root✝¹ i = root✝¹ ((reflectionPerm✝¹ i) j)
reflectionPerm_coroot✝¹ :
  ∀ (i j : ι), coroot✝¹ j - (p₁ (root✝¹ i)) (coroot✝¹ j) • coroot✝¹ i = coroot✝¹ ((reflectionPerm✝¹ i) j)
p₂ : M →ₗ[R] N →ₗ[R] R
isPerfPair_toLinearMap✝ : p₂.IsPerfPair
root✝ : ι ↪ M
coroot✝ : ι ↪ N
root_coroot_two✝ : ∀ (i : ι), (p₂ (root✝ i)) (coroot✝ i) = 2
reflectionPerm✝ : ι → ι ≃ ι
reflectionPerm_root✝ : ∀ (i j : ι), root✝ j - (p₂ (root✝ j)) (coroot✝ i) • root✝ i = root✝ ((reflectionPerm✝ i) j)
reflectionPerm_coroot✝ :
  ∀ (i j : ι), coroot✝ j - (p₂ (root✝ i)) (coroot✝ j) • coroot✝ i = coroot✝ ((reflectionPerm✝ i) j)
he :
  { toLinearMap := p₁, isPerfPair_toLinearMap := isPerfPair_toLinearMap✝¹, root := root✝¹, coroot := coroot✝¹,
        root_coroot_two := root_coroot_two✝¹, reflectionPerm := reflectionPerm✝¹,
        reflectionPerm_root := reflectionPerm_root✝¹, reflectionPerm_coroot := reflectionPerm_coroot✝¹ }.toLinearMap =
    { toLinearMap := p₂, isPerfPair_toLinearMap := isPerfPair_toLinearMap✝, root := root✝, coroot := coroot✝,
        root_coroot_two := root_coroot_two✝, reflectionPerm := reflectionPerm✝,
        reflectionPerm_root := reflectionPerm_root✝, reflectionPerm_coroot := reflectionPerm_coroot✝ }.toLinearMap
hr :
  { toLinearMap := p₁, isPerfPair_toLinearMap := isPerfPair_toLinearMap✝¹, root := root✝¹, coroot := coroot✝¹,
        root_coroot_two := root_coroot_two✝¹, reflectionPerm := reflectionPerm✝¹,
        reflectionPerm_root := reflectionPerm_root✝¹, reflectionPerm_coroot := reflectionPerm_coroot✝¹ }.root =
    { toLinearMap := p₂, isPerfPair_toLinearMap := isPerfPair_toLinearMap✝, root := root✝, coroot := coroot✝,
        root_coroot_two := root_coroot_two✝, reflectionPerm := reflectionPerm✝,
        reflectionPerm_root := reflectionPerm_root✝, reflectionPerm_coroot := reflectionPerm_coroot✝ }.root
hc :
  range
      ⇑{ toLinearMap := p₁, isPerfPair_toLinearMap := isPerfPair_toLinearMap✝¹, root := root✝¹, coroot := coroot✝¹,
            root_coroot_two := root_coroot_two✝¹, reflectionPerm := reflectionPerm✝¹,
            reflectionPerm_root := reflectionPerm_root✝¹, reflectionPerm_coroot := reflectionPerm_coroot✝¹ }.coroot =
    range
      ⇑{ toLinearMap := p₂, isPerfPair_toLinearMap := isPerfPair_toLinearMap✝, root := root✝, coroot := coroot✝,
            root_coroot_two := root_coroot_two✝, reflectionPerm := reflectionPerm✝,
            reflectionPerm_root := reflectionPerm_root✝, reflectionPerm_coroot := reflectionPerm_coroot✝ }.coroot
hp :
  { toLinearMap := p₁, isPerfPair_toLinearMap := isPerfPair_toLinearMap✝¹, root := root✝¹, coroot := coroot✝¹,
          root_coroot_two := root_coroot_two✝¹, reflectionPerm := reflectionPerm✝¹,
          reflectionPerm_root := reflectionPerm_root✝¹, reflectionPerm_coroot := reflectionPerm_coroot✝¹ }.coroot =
      { toLinearMap := p₂, isPerfPair_toLinearMap := isPerfPair_toLinearMap✝, root := root✝, coroot := coroot✝,
          root_coroot_two := root_coroot_two✝, reflectionPerm := reflectionPerm✝,
          reflectionPerm_root := reflectionPerm_root✝, reflectionPerm_coroot := reflectionPerm_coroot✝ }.coroot →
    { toLinearMap := p₁, isPerfPair_toLinearMap := isPerfPair_toLinearMap✝¹, root := root✝¹, coroot := coroot✝¹,
          root_coroot_two := root_coroot_two✝¹, reflectionPerm := reflectionPerm✝¹,
          reflectionPerm_root := reflectionPerm_root✝¹,
          reflectionPerm_coroot := reflectionPerm_coroot✝¹ }.reflectionPerm =
      { toLinearMap := p₂, isPerfPair_toLinearMap := isPerfPair_toLinearMap✝, root := root✝, coroot := coroot✝,
          root_coroot_two := root_coroot_two✝, reflectionPerm := reflectionPerm✝,
          reflectionPerm_root := reflectionPerm_root✝, reflectionPerm_coroot := reflectionPerm_coroot✝ }.reflectionPerm
this :
  { toLinearMap := p₁, isPerfPair_toLinearMap := isPerfPair_toLinearMap✝¹, root := root✝¹, coroot := coroot✝¹,
        root_coroot_two := root_coroot_two✝¹, reflectionPerm := reflectionPerm✝¹,
        reflectionPerm_root := reflectionPerm_root✝¹, reflectionPerm_coroot := reflectionPerm_coroot✝¹ }.coroot =
    { toLinearMap := p₂, isPerfPair_toLinearMap := isPerfPair_toLinearMap✝, root := root✝, coroot := coroot✝,
        root_coroot_two := root_coroot_two✝, reflectionPerm := reflectionPerm✝,
        reflectionPerm_root := reflectionPerm_root✝, reflectionPerm_coroot := reflectionPerm_coroot✝ }.coroot
⊢ { toLinearMap := p₁, isPerfPair_toLinearMap := isPerfPair_toLinearMap✝¹, root := root✝¹, coroot := coroot✝¹,
      root_coroot_two := root_coroot_two✝¹, reflectionPerm := reflectionPerm✝¹,
      reflectionPerm_root := reflectionPerm_root✝¹, reflectionPerm_coroot := reflectionPerm_coroot✝¹ } =
    { toLinearMap := p₂, isPerfPair_toLinearMap := isPerfPair_toLinearMap✝, root := root✝, coroot := coroot✝,
      root_coroot_two := root_coroot_two✝, reflectionPerm := reflectionPerm✝,
      reflectionPerm_root := reflectionPerm_root✝, reflectionPerm_coroot := reflectionPerm_coroot✝ }