awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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
inst_5 : P.EmbeddedG2
inst_6 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
inst_9 : P.IsIrreducible
i : ι
hi : ((P.root : (a : ι) → M) i : M) ∉ allRoots P
this_1 : Fintype ι
B : P.InvariantForm
h₂ :
  Eq.{u_2 + 1} (α := R)
    ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) (long P) : M) :
      R)
    (0 : R)
h₁ :
  Eq.{u_2 + 1} (α := R)
    ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) (short P) : M) :
      R)
    (0 : R)
this : Module.IsReflexive R M
x : M
hx : Membership.mem (γ := Submodule R M) (Submodule.span R {longRoot P, shortRoot P}) x
h :
  Eq.{u_2 + 1} (α := R) ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) x : R)
    (0 : R)
⊢ Eq.{u_2 + 1} (α := R) ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) x : R)
    ((0 : (a : M) → R) x : R)

Tactic:
simp only [LinearMap.zero_apply]

Premises used: LinearMap.zero_apply
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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
inst_5 : P.EmbeddedG2
inst_6 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
inst_9 : P.IsIrreducible
i : ι
hi : ((P.root : (a : ι) → M) i : M) ∉ allRoots P
this_1 : Fintype ι
B : P.InvariantForm
h₂ :
  Eq.{u_2 + 1} (α := R)
    ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) (long P) : M) :
      R)
    (0 : R)
h₁ :
  Eq.{u_2 + 1} (α := R)
    ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) (short P) : M) :
      R)
    (0 : R)
this : Module.IsReflexive R M
x : M
⊢ Eq.{u_2 + 1} (α := R) ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) 0 : R)
    (0 : R)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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
inst_5 : P.EmbeddedG2
inst_6 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
inst_9 : P.IsIrreducible
i : ι
hi : ((P.root : (a : ι) → M) i : M) ∉ allRoots P
this_1 : Fintype ι
B : P.InvariantForm
h₂ :
  Eq.{u_2 + 1} (α := R)
    ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) (long P) : M) :
      R)
    (0 : R)
h₁ :
  Eq.{u_2 + 1} (α := R)
    ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) (short P) : M) :
      R)
    (0 : R)
this : Module.IsReflexive R M
x x_1 : M
h : Membership.mem (γ := Set M) {longRoot P, shortRoot P} x_1
⊢ Eq.{u_2 + 1} (α := R)
    ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) x_1 : R) (0 : R)

Tactic:
grind
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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
inst_5 : P.EmbeddedG2
inst_6 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
inst_9 : P.IsIrreducible
i : ι
hi : ((P.root : (a : ι) → M) i : M) ∉ allRoots P
this_1 : Fintype ι
B : P.InvariantForm
h₂ :
  Eq.{u_2 + 1} (α := R)
    ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) (long P) : M) :
      R)
    (0 : R)
h₁ :
  Eq.{u_2 + 1} (α := R)
    ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) (short P) : M) :
      R)
    (0 : R)
this : Module.IsReflexive R M
x x_1 y : M
hx : Membership.mem (γ := Submodule R M) (Submodule.span R {longRoot P, shortRoot P}) x_1
hy : Membership.mem (γ := Submodule R M) (Submodule.span R {longRoot P, shortRoot P}) y
h :
  Eq.{u_2 + 1} (α := R)
    ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) x_1 : R) (0 : R)
h_1 :
  Eq.{u_2 + 1} (α := R) ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) y : R)
    (0 : R)
⊢ Eq.{u_2 + 1} (α := R)
    ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) (x_1 + y) : R) (0 : R)

Tactic:
simp_all
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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
inst_5 : P.EmbeddedG2
inst_6 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
inst_9 : P.IsIrreducible
i : ι
hi : ((P.root : (a : ι) → M) i : M) ∉ allRoots P
this_1 : Fintype ι
B : P.InvariantForm
h₂ :
  Eq.{u_2 + 1} (α := R)
    ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) (long P) : M) :
      R)
    (0 : R)
h₁ :
  Eq.{u_2 + 1} (α := R)
    ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) (short P) : M) :
      R)
    (0 : R)
this : Module.IsReflexive R M
x : M
a : R
x_1 : M
hx : Membership.mem (γ := Submodule R M) (Submodule.span R {longRoot P, shortRoot P}) x_1
h :
  Eq.{u_2 + 1} (α := R)
    ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) x_1 : R) (0 : R)
⊢ Eq.{u_2 + 1} (α := R)
    ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) (a • x_1) : R) (0 : R)

Tactic:
simp_all
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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
inst_5 : P.EmbeddedG2
inst_6 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
inst_9 : P.IsIrreducible
i : ι
hi : ((P.root : (a : ι) → M) i : M) ∉ allRoots P
this_1 : Fintype ι
B : P.InvariantForm
h₂ :
  Eq.{u_2 + 1} (α := R)
    ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) (long P) : M) :
      R)
    (0 : R)
h₁ :
  Eq.{u_2 + 1} (α := R)
    ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) (short P) : M) :
      R)
    (0 : R)
this : Module.IsReflexive R M
x : M
hx : Membership.mem (γ := Submodule R M) (Submodule.span R {longRoot P, shortRoot P}) x
h :
  Eq.{u_2 + 1} (α := R) ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) 0 : R)
    (0 : R)
h₃ :
  ∀ (x : M),
    Membership.mem (γ := Set M) {longRoot P, shortRoot P} x →
      Eq.{u_2 + 1} (α := R)
        ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) x : R) (0 : R)
h₄ :
  ∀ (x y : M),
    Membership.mem (γ := Submodule R M) (Submodule.span R {longRoot P, shortRoot P}) x →
      Membership.mem (γ := Submodule R M) (Submodule.span R {longRoot P, shortRoot P}) y →
        Eq.{u_2 + 1} (α := R)
            ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) x : R) (0 : R) →
          Eq.{u_2 + 1} (α := R)
              ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R) →
            Eq.{u_2 + 1} (α := R)
              ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) (x + y) : R)
              (0 : R)
h₅ :
  ∀ (a : R) (x : M),
    Membership.mem (γ := Submodule R M) (Submodule.span R {longRoot P, shortRoot P}) x →
      Eq.{u_2 + 1} (α := R)
          ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) x : R) (0 : R) →
        Eq.{u_2 + 1} (α := R)
          ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) (a • x) : R) (0 : R)
⊢ Eq.{u_2 + 1} (α := R) ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) x : R)
    (0 : R)

Tactic:
induction hx using Submodule.span_induction with
    | zero => simp
    | mem => grind
    | add => simp_all
    | smul => simp_all

Premises used: Submodule.smul, Submodule.zero, Submodule.add
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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
inst_5 : P.EmbeddedG2
inst_6 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
inst_9 : P.IsIrreducible
i : ι
hi : ((P.root : (a : ι) → M) i : M) ∉ allRoots P
this_1 : Fintype ι
B : P.InvariantForm
h₂ :
  Eq.{u_2 + 1} (α := R)
    ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) (long P) : M) :
      R)
    (0 : R)
h₁ :
  Eq.{u_2 + 1} (α := R)
    ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) (short P) : M) :
      R)
    (0 : R)
this : Module.IsReflexive R M
⊢ Eq (α := M →ₗ[R] R) ((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) (0 : M →ₗ[R] R)

Tactic:
have key : B.form (P.root i) = 0 := by
    ext x
    have hx : x ∈ span R {longRoot P, shortRoot P} := by simp
    simp only [LinearMap.zero_apply]
    induction hx using Submodule.span_induction with
    | zero => simp
    | mem => grind
    | add => simp_all
    | smul => simp_all
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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
inst_5 : P.EmbeddedG2
inst_6 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
inst_9 : P.IsIrreducible
i : ι
hi : ((P.root : (a : ι) → M) i : M) ∉ allRoots P
this_1 : Fintype ι
B : P.InvariantForm
h₂ :
  Eq.{u_2 + 1} (α := R)
    ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) (long P) : M) :
      R)
    (0 : R)
h₁ :
  Eq.{u_2 + 1} (α := R)
    ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) (short P) : M) :
      R)
    (0 : R)
this : Module.IsReflexive R M
key : Eq (α := M →ₗ[R] R) ((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) (0 : M →ₗ[R] R)
⊢ False

Tactic:
simpa using LinearMap.congr_fun key (P.root i)

Premises used: RootPairing.root, LinearMap.congr_fun, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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
inst_5 : P.EmbeddedG2
inst_6 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
inst_9 : P.IsIrreducible
i : ι
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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
inst_5 : P.EmbeddedG2
inst_6 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
inst_9 : P.IsIrreducible
x : M
hx : x ∈ (allRoots P).toFinset
simp : (P.root : (a : ι) → M) (Exists.choose (p := fun (y : ι) ↦ (P.root : (a : ι) → M) y = x) ⋯) = x
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp only [Subtype.mk.injEq]

Premises used: Subtype.mk.injEq
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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
inst_5 : P.EmbeddedG2
inst_6 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
inst_9 : P.IsIrreducible
x : M
hx : x ∈ (allRoots P).toFinset
⊢ (P.root : (a : ι) → M) (Exists.choose (p := fun (y : ι) ↦ (P.root : (a : ι) → M) y = x) ⋯) = x

Tactic:
(allRoots_subset_range_root P hx).choose_spec

Premises used: Exists.choose_spec, RootPairing.EmbeddedG2.allRoots_subset_range_root
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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
inst_5 : P.EmbeddedG2
inst_6 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
inst_9 : P.IsIrreducible
x : M
hx : x ∈ (allRoots P).toFinset
⊢ (P.root : (a : ι) → M) (Exists.choose (p := fun (y : ι) ↦ (P.root : (a : ι) → M) y = x) ⋯) = x

Tactic:
exact (allRoots_subset_range_root P hx).choose_spec

Premises used: Exists.choose_spec, RootPairing.EmbeddedG2.allRoots_subset_range_root
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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
inst_5 : P.EmbeddedG2
inst_6 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
inst_9 : P.IsIrreducible
rw : (allRoots P).length = 12
⊢ Nat.card.{u_3} ↥(allRoots P).toFinset = 12

Tactic:
rw [Nat.card_eq_fintype_card, Fintype.card_coe, toFinset_card_of_nodup (allRoots_nodup P)]

Premises used: List.toFinset_card_of_nodup, RootPairing.EmbeddedG2.allRoots_nodup, Fintype.card_coe, Nat.card_eq_fintype_card
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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
inst_5 : P.EmbeddedG2
inst_6 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
inst_9 : P.IsIrreducible
⊢ (allRoots P).length = 12

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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
inst_5 : P.EmbeddedG2
inst_6 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
inst_9 : P.IsIrreducible
⊢ Nat.card.{u_3} ↥(allRoots P).toFinset = 12

Tactic:
have this : Nat.card (allRoots P).toFinset = 12 := by
    rw [Nat.card_eq_fintype_card, Fintype.card_coe, toFinset_card_of_nodup (allRoots_nodup P)]
    simp
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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
inst_5 : P.EmbeddedG2
inst_6 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
inst_9 : P.IsIrreducible
this : Nat.card.{u_3} ↥(allRoots P).toFinset = 12
rw : Nat.card ι = Nat.card.{u_3} ↥(allRoots P).toFinset
⊢ Nat.card ι = 12

Tactic:
rw [← this]
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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
inst_5 : P.EmbeddedG2
inst_6 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
inst_9 : P.IsIrreducible
this : Nat.card.{u_3} ↥(allRoots P).toFinset = 12
⊢ Nat.card ι = Nat.card.{u_3} ↥(allRoots P).toFinset

Tactic:
Nat.card_congr <| indexEquivAllRoots P

Premises used: Nat.card_congr, RootPairing.EmbeddedG2.indexEquivAllRoots
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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
inst_5 : P.EmbeddedG2
inst_6 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
inst_9 : P.IsIrreducible
this : Nat.card.{u_3} ↥(allRoots P).toFinset = 12
⊢ Nat.card ι = Nat.card.{u_3} ↥(allRoots P).toFinset

Tactic:
exact Nat.card_congr <| indexEquivAllRoots P

Premises used: Nat.card_congr, RootPairing.EmbeddedG2.indexEquivAllRoots
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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
inst_5 : P.EmbeddedG2
inst_6 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
inst_9 : P.IsIrreducible
have : Nat.card.{u_3} ↥(allRoots P).toFinset = 12
have₁ : ∀ (this : Nat.card.{u_3} ↥(allRoots P).toFinset = 12), Nat.card ι = 12
have₂ : Nat.card.{u_3} ↥(allRoots P).toFinset = 12
have₃ have₄ : ∀ (this : Nat.card.{u_3} ↥(allRoots P).toFinset = 12), Nat.card ι = 12
have₅ : ∀ (this : Nat.card.{u_3} ↥(allRoots P).toFinset = 12), Nat.card ι = Nat.card.{u_3} ↥(allRoots P).toFinset
⊢ Nat.card ι = 12

Tactic:
classical
  have this : Nat.card (allRoots P).toFinset = 12 := by
    rw [Nat.card_eq_fintype_card, Fintype.card_coe, toFinset_card_of_nodup (allRoots_nodup P)]
    simp
  rw [← this]
  exact Nat.card_congr <| indexEquivAllRoots P

Premises used: Nat.card_congr, RootPairing.EmbeddedG2.indexEquivAllRoots
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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
inst_5 : P.EmbeddedG2
inst_6 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
inst_9 : P.IsIrreducible
i : ι
⊢ Membership.mem (γ := Set ι)
    {long P, -long P, short P, -short P, shortAddLong P, -shortAddLong P, twoShortAddLong P, -twoShortAddLong P,
      threeShortAddLong P, -threeShortAddLong P, threeShortAddTwoLong P, -threeShortAddTwoLong P}
    i

Tactic:
simpa using mem_allRoots P i

Premises used: RootPairing.EmbeddedG2.mem_allRoots
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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
inst_5 : P.IsG2
b : P.Base
inst_6 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
have : ∀ (_i : P.EmbeddedG2), b.support.card = 2
⊢ b.support.card = 2

Tactic:
have _i : P.EmbeddedG2 := toEmbeddedG2 P
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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
inst_5 : P.IsG2
b : P.Base
inst_6 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
_i : P.EmbeddedG2
⊢ Nonempty ι

Tactic:
have _i : Nonempty ι := IsG2.nonempty P
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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
inst_5 : P.IsG2
b : P.Base
inst_6 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
_i_1 : P.EmbeddedG2
_i : Nonempty ι
rw : b.support.card = Fintype.card (Fin 2)
rw₁ : b.support.card = Module.finrank R M
rw₂ : b.support.card = Fintype.card.{u_1} ↥b.support
rw₃ rw₄ : b.support.card = b.support.card
⊢ b.support.card = 2

Tactic:
rw [← Fintype.card_fin 2, ← Module.finrank_eq_card_basis (EmbeddedG2.basis P),
    Module.finrank_eq_card_basis b.toWeightBasis, Fintype.card_coe]

Premises used: Fintype.card_fin, RootPairing.EmbeddedG2.basis, Module.finrank_eq_card_basis, RootPairing.Base.toWeightBasis, OfNat.ofNat, Fintype.card_coe
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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
inst_5 : P.IsG2
b : P.Base
inst_6 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
i j : ι
hi : i ∈ b.support
hj : j ∈ b.support
h_ne : i ≠ j
⊢ {i, j} ⊆ b.support

Tactic:
grind
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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
inst_5 : P.IsG2
b : P.Base
inst_6 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
i j : ι
hi : i ∈ b.support
hj : j ∈ b.support
h_ne : i ≠ j
⊢ {i, j} ⊆ b.support

Tactic:
have : {i, j} ⊆ b.support := by grind
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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
inst_5 : P.IsG2
b : P.Base
inst_6 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
i j : ι
hi : i ∈ b.support
hj : j ∈ b.support
h_ne : i ≠ j
this : {i, j} ⊆ b.support
⊢ b.support.card ≤ Finset.card (α := ι) {i, j}

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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
inst_5 : P.IsG2
b : P.Base
inst_6 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
i j : ι
hi : i ∈ b.support
hj : j ∈ b.support
h_ne : i ≠ j
this : {i, j} ⊆ b.support
rw : Eq (α := Submodule ℤ M) (Submodule.span ℤ (image (α := ι) (⇑P.root : (a : ι) → M) {i, j})) (P.rootSpan ℤ)
rw₁ : Eq (α := Submodule ℤ M) (Submodule.span ℤ ((⇑P.root : (a : ι) → M) '' (↑{i, j} : Set ι))) (P.rootSpan ℤ)
rw₂ : Eq (α := Submodule ℤ M) (Submodule.span ℤ ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) (P.rootSpan ℤ)
rw₃ rw₄ :
  Eq (α := Submodule ℤ M) (Submodule.span ℤ (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) (P.rootSpan ℤ)
⊢ Eq (α := Submodule ℤ M)
    (Submodule.span ℤ
      (insert (α := M) ((P.root : (a : ι) → M) i : M) (singleton (α := M) ((P.root : (a : ι) → M) j : M))))
    (P.rootSpan ℤ)

Tactic:
rw [← image_pair, ← Finset.coe_pair, Finset.eq_of_subset_of_card_le this (by aesop),
    b.span_int_root_support]

Premises used: Set.image_pair, Finset.coe_pair, RootPairing.Base.span_int_root_support, Finset.eq_of_subset_of_card_le
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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
inst_5 : P.IsG2
b : P.Base
inst_6 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
i j : ι
hi : i ∈ b.support
hj : j ∈ b.support
h_ne : i ≠ j
have : {i, j} ⊆ b.support
have₁ :
  ∀ (this : {i, j} ⊆ b.support),
    Eq (α := Submodule ℤ M)
      (Submodule.span ℤ
        (insert (α := M) ((P.root : (a : ι) → M) i : M) (singleton (α := M) ((P.root : (a : ι) → M) j : M))))
      (P.rootSpan ℤ)
have₂ : {i, j} ⊆ b.support
have₃ have₄ :
  ∀ (this : {i, j} ⊆ b.support),
    Eq (α := Submodule ℤ M)
      (Submodule.span ℤ
        (insert (α := M) ((P.root : (a : ι) → M) i : M) (singleton (α := M) ((P.root : (a : ι) → M) j : M))))
      (P.rootSpan ℤ)
⊢ Eq (α := Submodule ℤ M)
    (Submodule.span ℤ
      (insert (α := M) ((P.root : (a : ι) → M) i : M) (singleton (α := M) ((P.root : (a : ι) → M) j : M))))
    (P.rootSpan ℤ)

Tactic:
classical
  have : {i, j} ⊆ b.support := by grind
  rw [← image_pair, ← Finset.coe_pair, Finset.eq_of_subset_of_card_le this (by aesop),
    b.span_int_root_support]

Premises used: Set.image_pair, Finset.coe_pair, RootPairing.Base.span_int_root_support