awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
⊢ comp (β := N) (⇑P.flip.toPerfPair : (a : N) → Dual R M) (⇑P.coroot : (a : ι) → N) = P.coroot'

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
i j : ι
⊢ P.flip.coxeterWeight i j = P.coxeterWeight i j

Tactic:
simp [coxeterWeight, mul_comm (P.pairing j i)]

Premises used: RootPairing.coxeterWeight, RootPairing.pairing, mul_comm
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
i j : ι
⊢ P.coxeterWeight i j = P.coxeterWeight j i

Tactic:
simp only [coxeterWeight, mul_comm]

Premises used: RootPairing.coxeterWeight, mul_comm
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
i j : ι
⊢ P.IsOrthogonal i j ↔ P.IsOrthogonal j i

Tactic:
simp only [IsOrthogonal, and_comm]

Premises used: and_comm, RootPairing.IsOrthogonal
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
i j : ι
h : P.IsOrthogonal i j
h₁ :
  ∀ (x : M),
    Eq (α := M) ((P.reflection i * P.reflection j : (a : M) → M) x : M)
      ((P.reflection j * P.reflection i : (a : M) → M) x : M)
⊢ P.reflection i * P.reflection j = P.reflection j * P.reflection i

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
i j : ι
h : P.IsOrthogonal i j
x : M
⊢ P.pairing i j = 0 ∧ P.pairing j i = 0

Tactic:
simpa [IsOrthogonal] using h

Premises used: RootPairing.IsOrthogonal
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
i j : ι
h : P.IsOrthogonal i j
x : M
⊢ P.pairing i j = 0 ∧ P.pairing j i = 0

Tactic:
replace h : P.pairing i j = 0 ∧ P.pairing j i = 0 := by simpa [IsOrthogonal] using h
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
i j : ι
x : M
h : P.pairing i j = 0 ∧ P.pairing j i = 0
h₁ :
  x -
        HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
          ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
          ((P.root : (a : ι) → M) i : M) -
      HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
        ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) j : N) : R)
        ((P.root : (a : ι) → M) j : M) =
    x -
        HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
          ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) j : N) : R)
          ((P.root : (a : ι) → M) j : M) -
      HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
        ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
        ((P.root : (a : ι) → M) i : M)
⊢ Eq (α := M) ((P.reflection i * P.reflection j : (a : M) → M) x : M)
    ((P.reflection j * P.reflection i : (a : M) → M) x : M)

Tactic:
simp only [LinearEquiv.mul_apply, reflection_apply, LinearMap.flip_apply, map_sub,
    map_smul, root_coroot_eq_pairing, h, zero_smul, sub_zero]

Premises used: map_sub, RootPairing.root_coroot_eq_pairing, sub_zero, LinearEquiv.mul_apply, LinearMap.flip_apply, zero_smul, RootPairing.reflection_apply, map_smul
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
i j : ι
x : M
h : P.pairing i j = 0 ∧ P.pairing j i = 0
⊢ x -
        HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
          ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
          ((P.root : (a : ι) → M) i : M) -
      HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
        ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) j : N) : R)
        ((P.root : (a : ι) → M) j : M) =
    x -
        HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
          ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) j : N) : R)
          ((P.root : (a : ι) → M) j : M) -
      HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
        ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
        ((P.root : (a : ι) → M) i : M)

Tactic:
abel
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
i j : ι
h : P.IsOrthogonal i j
⊢ P.flip.IsOrthogonal i j

Tactic:
⟨h.2, h.1⟩

Premises used: And.right, And.left, And.intro, RootPairing.IsOrthogonal
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
i j : ι
h : P.IsOrthogonal i j
⊢ P.IsOrthogonal j i

Tactic:
⟨h.2, h.1⟩

Premises used: And.right, And.left, And.intro, RootPairing.IsOrthogonal
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
i j : ι
h : P.IsOrthogonal i j
⊢ Eq (α := M) ((P.reflection j : (a : M) → M) ((P.root : (a : ι) → M) i : M) : M) ((P.root : (a : ι) → M) i : M)

Tactic:
simp [reflection_apply, h.1]

Premises used: And.left, RootPairing.reflection_apply
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
i j : ι
h : P.IsOrthogonal j i
⊢ Eq (α := M) ((P.reflection j : (a : M) → M) ((P.root : (a : ι) → M) i : M) : M) ((P.root : (a : ι) → M) i : M)

Tactic:
h.symm.reflection_apply_left

Premises used: RootPairing.IsOrthogonal.reflection_apply_left, RootPairing.IsOrthogonal.symm
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
i j : ι
h : P.IsOrthogonal i j
⊢ Eq (α := N) ((P.coreflection j : (a : N) → N) ((P.coroot : (a : ι) → N) i : N) : N) ((P.coroot : (a : ι) → N) i : N)

Tactic:
h.flip.reflection_apply_left

Premises used: RootPairing.IsOrthogonal.flip, RootPairing.IsOrthogonal.reflection_apply_left
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
i j : ι
h : P.IsOrthogonal j i
⊢ Eq (α := N) ((P.coreflection j : (a : N) → N) ((P.coroot : (a : ι) → N) i : N) : N) ((P.coroot : (a : ι) → N) i : N)

Tactic:
h.flip.reflection_apply_right

Premises used: RootPairing.IsOrthogonal.flip, RootPairing.IsOrthogonal.reflection_apply_right
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
j : ι
s : Set ι
hj : ∀ i ∈ s, P.IsOrthogonal j i
x : M
zero zero₁ : Eq.{u_3 + 1} (α := M) 0 0
⊢ Eq (α := M) ((P.reflection j : (a : M) → M) 0 : M) (0 : M)

Tactic:
rw [map_zero]

Premises used: map_zero
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
j : ι
s : Set ι
hj : ∀ i ∈ s, P.IsOrthogonal j i
x u v : M
hu : Membership.mem (γ := Submodule R M) (span R ((⇑P.root : (a : ι) → M) '' s)) u
hv : Membership.mem (γ := Submodule R M) (span R ((⇑P.root : (a : ι) → M) '' s)) v
hu' : (P.reflection j : (a : M) → M) u = u
hv' : (P.reflection j : (a : M) → M) v = v
add : HAdd.hAdd (α := M) (β := M) ((P.reflection j : (a : M) → M) u : M) ((P.reflection j : (a : M) → M) v : M) = u + v
add₁ : HAdd.hAdd (β := M) u ((P.reflection j : (a : M) → M) v : M) = u + v
add₂ add₃ : u + v = u + v
⊢ (P.reflection j : (a : M) → M) (u + v) = u + v

Tactic:
rw [map_add, hu', hv']

Premises used: map_add
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
j : ι
s : Set ι
hj : ∀ i ∈ s, P.IsOrthogonal j i
x : M
t : R
u : M
hu : Membership.mem (γ := Submodule R M) (span R ((⇑P.root : (a : ι) → M) '' s)) u
hu' : (P.reflection j : (a : M) → M) u = u
smul : HSMul.hSMul (β := M) t ((P.reflection j : (a : M) → M) u : M) = t • u
smul₁ smul₂ : t • u = t • u
⊢ (P.reflection j : (a : M) → M) (t • u) = t • u

Tactic:
rw [map_smul, hu']

Premises used: map_smul
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
j : ι
s : Set ι
hj : ∀ i ∈ s, P.IsOrthogonal j i
x u : M
hu : Membership.mem (γ := Set M) ((⇑P.root : (a : ι) → M) '' s) u
mem :
  ∀ (i : ι) (his : i ∈ s),
    Eq (α := M) ((P.reflection j : (a : M) → M) ((P.root : (a : ι) → M) i : M) : M) ((P.root : (a : ι) → M) i : M)
⊢ (P.reflection j : (a : M) → M) u = u

Tactic:
obtain ⟨i, his, rfl⟩ := hu

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
j : ι
s : Set ι
hj : ∀ i ∈ s, P.IsOrthogonal j i
x : M
i : ι
his : i ∈ s
⊢ Eq (α := M) ((P.reflection j : (a : M) → M) ((P.root : (a : ι) → M) i : M) : M) ((P.root : (a : ι) → M) i : M)

Tactic:
IsOrthogonal.reflection_apply_right <| hj i his

Premises used: RootPairing.IsOrthogonal.reflection_apply_right
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
j : ι
s : Set ι
hj : ∀ i ∈ s, P.IsOrthogonal j i
x : M
i : ι
his : i ∈ s
⊢ Eq (α := M) ((P.reflection j : (a : M) → M) ((P.root : (a : ι) → M) i : M) : M) ((P.root : (a : ι) → M) i : M)

Tactic:
exact IsOrthogonal.reflection_apply_right <| hj i his

Premises used: RootPairing.IsOrthogonal.reflection_apply_right
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
j : ι
s : Set ι
hj : ∀ i ∈ s, P.IsOrthogonal j i
x : M
hx : Membership.mem (γ := Submodule R M) (span R ((⇑P.root : (a : ι) → M) '' s)) x
zero : Eq (α := M) ((P.reflection j : (a : M) → M) 0 : M) (0 : M)
add :
  ∀ (u v : M) (hu : Membership.mem (γ := Submodule R M) (span R ((⇑P.root : (a : ι) → M) '' s)) u)
    (hv : Membership.mem (γ := Submodule R M) (span R ((⇑P.root : (a : ι) → M) '' s)) v)
    (hu' : (P.reflection j : (a : M) → M) u = u) (hv' : (P.reflection j : (a : M) → M) v = v),
    (P.reflection j : (a : M) → M) (u + v) = u + v
smul :
  ∀ (t : R) (u : M) (hu : Membership.mem (γ := Submodule R M) (span R ((⇑P.root : (a : ι) → M) '' s)) u)
    (hu' : (P.reflection j : (a : M) → M) u = u), (P.reflection j : (a : M) → M) (t • u) = t • u
mem :
  ∀ (u : M) (hu : Membership.mem (γ := Set M) ((⇑P.root : (a : ι) → M) '' s) u), (P.reflection j : (a : M) → M) u = u
⊢ (P.reflection j : (a : M) → M) x = x

Tactic:
induction hx using Submodule.span_induction with
  | zero => rw [map_zero]
  | add u v hu hv hu' hv' => rw [map_add, hu', hv']
  | smul t u hu hu' => rw [map_smul, hu']
  | mem u hu =>
      obtain ⟨i, his, rfl⟩ := hu
      exact IsOrthogonal.reflection_apply_right <| hj i his

Premises used: map_zero, map_add, RootPairing.IsOrthogonal.reflection_apply_right, rfl, map_smul
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
i j : ι
h : P.pairing j i = 0
⊢ Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) ((P.reflectionPerm i : (a : ι) → ι) j : ι) : M)
    ((P.root : (a : ι) → M) j : M)

Tactic:
simp [reflection_apply, h]

Premises used: RootPairing.reflection_apply
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
i j : ι
h : P.pairing i j = 0
⊢ (P.reflectionPerm i : (a : ι) → ι) j = j

Tactic:
P.flip.reflectionPerm_eq_of_pairing_eq_zero h

Premises used: RootPairing.reflectionPerm_eq_of_pairing_eq_zero
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
i j : ι
h : (P.reflectionPerm i : (a : ι) → ι) j = j
⊢ HSMul.hSMul (β := M) (P.pairing j i) ((P.root : (a : ι) → M) i : M) = 0

Tactic:
simpa [h] using P.reflectionPerm_root i j

Premises used: RootPairing.reflectionPerm_root
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
i j : ι
h : HSMul.hSMul (β := M) (P.pairing j i) ((P.root : (a : ι) → M) i : M) = 0
⊢ Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) ((P.reflectionPerm i : (a : ι) → ι) j : ι) : M)
    ((P.root : (a : ι) → M) j : M)

Tactic:
simp [reflection_apply, h]

Premises used: RootPairing.reflection_apply
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
i j : ι
⊢ (P.reflectionPerm i : (a : ι) → ι) j = j ↔ HSMul.hSMul (β := N) (P.pairing i j) ((P.coroot : (a : ι) → N) i : N) = 0

Tactic:
P.flip.reflectionPerm_eq_iff_smul_root

Premises used: RootPairing.reflectionPerm_eq_iff_smul_root, RootPairing.pairing, RootPairing.flip
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
i j : ι
inst_5 : NeZero.{u_2} (R := R) 2
inst_6 : IsDomain R
inst_7 : IsTorsionFree R M
suffices : ∀ {i j : ι}, P.pairing i j = 0 → P.pairing j i = 0
⊢ P.pairing i j = 0 ↔ P.pairing j i = 0

Tactic:
suffices ∀ {i j : ι}, P.pairing i j = 0 → P.pairing j i = 0 from ⟨this, this⟩
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
i_1 j_1 : ι
inst_5 : NeZero.{u_2} (R := R) 2
inst_6 : IsDomain R
inst_7 : IsTorsionFree R M
i j : ι
h : P.pairing i j = 0
⊢ P.pairing j i = 0

Tactic:
simpa [P.ne_zero i, reflectionPerm_eq_iff_smul_root] using
    P.reflectionPerm_eq_of_pairing_eq_zero' h

Premises used: RootPairing.reflectionPerm_eq_iff_smul_root, RootPairing.ne_zero, RootPairing.reflectionPerm_eq_of_pairing_eq_zero'
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
i j : ι
inst_5 : NeZero.{u_2} (R := R) 2
inst_6 : IsDomain R
⊢ IsReflexive R M

Tactic:
have : IsReflexive R M := .of_isPerfPair P.toLinearMap
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
i j : ι
inst_5 : NeZero.{u_2} (R := R) 2
inst_6 : IsDomain R
this : IsReflexive R M
⊢ P.pairing i j = 0 ↔ P.pairing j i = 0

Tactic:
pairing_eq_zero_iff

Premises used: RootPairing.pairing_eq_zero_iff
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
i j : ι
inst_5 : NeZero.{u_2} (R := R) 2
inst_6 : IsDomain R
this : IsReflexive R M
⊢ P.pairing i j = 0 ↔ P.pairing j i = 0

Tactic:
exact pairing_eq_zero_iff

Premises used: RootPairing.pairing_eq_zero_iff
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
i j : ι
inst_5 : NeZero.{u_2} (R := R) 2
inst_6 : IsDomain R
this : IsReflexive R M
⊢ P.coxeterWeight i j = 0 ↔ P.IsOrthogonal i j

Tactic:
simp [coxeterWeight, IsOrthogonal, P.pairing_eq_zero_iff (i := i) (j := j)]

Premises used: RootPairing.coxeterWeight, RootPairing.pairing_eq_zero_iff, RootPairing.IsOrthogonal
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
i j : ι
inst_5 : NeZero.{u_2} (R := R) 2
inst_6 : IsDomain R
inst_7 : IsTorsionFree R M
⊢ P.IsOrthogonal i j ↔ P.pairing i j = 0

Tactic:
⟨fun h ↦ h.1, fun h ↦ ⟨h, pairing_eq_zero_iff.mp h⟩⟩

Premises used: RootPairing.pairing_eq_zero_iff, And.left, And.intro, Iff.intro, Iff.mp
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
i j : ι
inst_5 : NeZero.{u_2} (R := R) 2
inst_6 : IsDomain R
inst_7 : IsTorsionFree R M
⊢ IsFixedPt (⇑(P.reflectionPerm i) : (a : ι) → ι) j ↔ P.pairing i j = 0

Tactic:
simp [P.ne_zero i, pairing_eq_zero_iff, IsFixedPt, reflectionPerm_eq_iff_smul_root]

Premises used: RootPairing.reflectionPerm_eq_iff_smul_root, RootPairing.ne_zero, RootPairing.pairing_eq_zero_iff, Function.IsFixedPt
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
i j : ι
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : AddCommGroup N₂
inst_8 : Module R N₂
e : ι ≃ ι₂
f : M ≃ₗ[R] M₂
g : N ≃ₗ[R] N₂
⊢ IsReflexive R N

Tactic:
have : IsReflexive R N := .of_isPerfPair P.flip.toLinearMap
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
i j : ι
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : AddCommGroup N₂
inst_8 : Module R N₂
e : ι ≃ ι₂
f : M ≃ₗ[R] M₂
g : N ≃ₗ[R] N₂
this : IsReflexive R N
⊢ IsReflexive R N₂

Tactic:
have : IsReflexive R N₂ := equiv g
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
i j : ι
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : AddCommGroup N₂
inst_8 : Module R N₂
e : ι ≃ ι₂
f : M ≃ₗ[R] M₂
g : N ≃ₗ[R] N₂
this_1 : IsReflexive R N
this : IsReflexive R N₂
⊢ (↑(f.symm ≪≫ₗ P.toPerfPair ≪≫ₗ g.symm.dualMap) : M₂ →ₗ[R] Dual R N₂).IsPerfPair

Tactic:
infer_instance
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
i_1 j : ι
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : AddCommGroup N₂
inst_8 : Module R N₂
e : ι ≃ ι₂
f : M ≃ₗ[R] M₂
g : N ≃ₗ[R] N₂
i : ι₂
⊢ Eq.{u_2 + 1} (α := R)
    (((((↑(f.symm ≪≫ₗ P.toPerfPair ≪≫ₗ g.symm.dualMap) : M₂ →ₗ[R] Dual R N₂) : (a : M₂) → N₂ →ₗ[R] R)
              (((e.symm.toEmbedding.trans P.root).trans f.toAddEquiv.toEmbedding : (a : ι₂) → M₂) i) :
            N₂ →ₗ[R] R) :
          (a : N₂) → R)
        (((e.symm.toEmbedding.trans P.coroot).trans g.toAddEquiv.toEmbedding : (a : ι₂) → N₂) i : N₂) :
      R)
    (2 : R)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
i_1 j_1 : ι
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : AddCommGroup N₂
inst_8 : Module R N₂
e : ι ≃ ι₂
f : M ≃ₗ[R] M₂
g : N ≃ₗ[R] N₂
i j : ι₂
⊢ HSub.hSub (α := N₂) (((e.symm.toEmbedding.trans P.coroot).trans g.toAddEquiv.toEmbedding : (a : ι₂) → N₂) j : N₂)
      (HSMul.hSMul.{u_2, u_7, u_7} (α := R) (β := N₂)
        (((((↑(f.symm ≪≫ₗ P.toPerfPair ≪≫ₗ g.symm.dualMap) : M₂ →ₗ[R] Dual R N₂) : (a : M₂) → N₂ →ₗ[R] R)
                  (((e.symm.toEmbedding.trans P.root).trans f.toAddEquiv.toEmbedding : (a : ι₂) → M₂) i) :
                N₂ →ₗ[R] R) :
              (a : N₂) → R)
            (((e.symm.toEmbedding.trans P.coroot).trans g.toAddEquiv.toEmbedding : (a : ι₂) → N₂) j : N₂) :
          R)
        (((e.symm.toEmbedding.trans P.coroot).trans g.toAddEquiv.toEmbedding : (a : ι₂) → N₂) i : N₂)) =
    ((e.symm.toEmbedding.trans P.coroot).trans g.toAddEquiv.toEmbedding : (a : ι₂) → N₂)
      ((e.symm.trans ((P.reflectionPerm ((e.symm : (a : ι₂) → ι) i)).trans e) : (a : ι₂) → ι₂) j : ι₂)

Tactic:
simp [coreflection_apply]

Premises used: RootPairing.coreflection_apply