awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
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
S : Type u_6
inst_5 : CommRing S
inst_6 : Algebra S R
inst_7 : P.IsValuedIn S
i j : ι
⊢ (algebraMap S R : (a : S) → R) (P.pairingIn S i j) = P.pairing i j

Tactic:
(P.exists_value i j).choose_spec

Premises used: Exists.choose_spec, RootPairing.pairingIn, RootPairing.exists_value
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
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
S : Type u_6
inst_5 : CommRing S
inst_6 : Algebra S R
inst_7 : FaithfulSMul S R
inst_8 : P.IsValuedIn S
i : ι
⊢ Eq.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) (P.pairingIn S i i) : R) ((algebraMap S R : (a : S) → R) 2 : R)

Tactic:
simp [map_ofNat]

Premises used: map_ofNat
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
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
S : Type u_6
inst_5 : CommRing S
inst_6 : Algebra S R
inst_7 : FaithfulSMul S R
inst_8 : P.IsValuedIn S
i j k l : ι
h : (P.root : (a : ι) → M) k = HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) l : M)
a :
  Eq.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) (P.pairingIn S k j) : R)
    ((algebraMap S R : (a : S) → R) (P.pairingIn S i j + P.pairingIn S l j) : R)
⊢ P.pairingIn S k j = P.pairingIn S i j + P.pairingIn S l j

Tactic:
apply FaithfulSMul.algebraMap_injective S R

Premises used: FaithfulSMul.algebraMap_injective
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
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
S : Type u_6
inst_5 : CommRing S
inst_6 : Algebra S R
inst_7 : FaithfulSMul S R
inst_8 : P.IsValuedIn S
i j k l : ι
h : (P.root : (a : ι) → M) k = HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) l : M)
⊢ Eq.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) (P.pairingIn S k j) : R)
    ((algebraMap S R : (a : S) → R) (P.pairingIn S i j + P.pairingIn S l j) : R)

Tactic:
simpa [← P.algebraMap_pairingIn S, -algebraMap_pairingIn] using pairing_eq_add_of_root_eq_add h

Premises used: RootPairing.pairing_eq_add_of_root_eq_add, RootPairing.algebraMap_pairingIn
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
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
S : Type u_6
inst_5 : CommRing S
inst_6 : Algebra S R
inst_7 : FaithfulSMul S R
inst_8 : P.IsValuedIn S
inst_9 : Module S M
inst_10 : IsScalarTower S R M
i j k l : ι
x y : S
h :
  (P.root : (a : ι) → M) k =
    HSMul.hSMul (β := M) x ((P.root : (a : ι) → M) i : M) + HSMul.hSMul (β := M) y ((P.root : (a : ι) → M) l : M)
a :
  Eq.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) (P.pairingIn S k j) : R)
    ((algebraMap S R : (a : S) → R) (x • P.pairingIn S i j + y • P.pairingIn S l j) : R)
⊢ P.pairingIn S k j = x • P.pairingIn S i j + y • P.pairingIn S l j

Tactic:
apply FaithfulSMul.algebraMap_injective S R

Premises used: FaithfulSMul.algebraMap_injective
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
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
S : Type u_6
inst_5 : CommRing S
inst_6 : Algebra S R
inst_7 : FaithfulSMul S R
inst_8 : P.IsValuedIn S
inst_9 : Module S M
inst_10 : IsScalarTower S R M
i j k l : ι
x y : S
h :
  (P.root : (a : ι) → M) k =
    HSMul.hSMul (β := M) x ((P.root : (a : ι) → M) i : M) + HSMul.hSMul (β := M) y ((P.root : (a : ι) → M) l : M)
⊢ (P.root : (a : ι) → M) k =
    HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := M) ((algebraMap S R : (a : S) → R) x : R)
        ((P.root : (a : ι) → M) i : M) +
      HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := M) ((algebraMap S R : (a : S) → R) y : R)
        ((P.root : (a : ι) → M) l : M)

Tactic:
simpa
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
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
S : Type u_6
inst_5 : CommRing S
inst_6 : Algebra S R
inst_7 : FaithfulSMul S R
inst_8 : P.IsValuedIn S
inst_9 : Module S M
inst_10 : IsScalarTower S R M
i j k l : ι
x y : S
h :
  (P.root : (a : ι) → M) k =
    HSMul.hSMul (β := M) x ((P.root : (a : ι) → M) i : M) + HSMul.hSMul (β := M) y ((P.root : (a : ι) → M) l : M)
⊢ (P.root : (a : ι) → M) k =
    HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := M) ((algebraMap S R : (a : S) → R) x : R)
        ((P.root : (a : ι) → M) i : M) +
      HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := M) ((algebraMap S R : (a : S) → R) y : R)
        ((P.root : (a : ι) → M) l : M)

Tactic:
replace h : P.root k = (algebraMap S R x) • P.root i + (algebraMap S R y) • P.root l := by simpa
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
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
S : Type u_6
inst_5 : CommRing S
inst_6 : Algebra S R
inst_7 : FaithfulSMul S R
inst_8 : P.IsValuedIn S
inst_9 : Module S M
inst_10 : IsScalarTower S R M
i j k l : ι
x y : S
h :
  (P.root : (a : ι) → M) k =
    HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := M) ((algebraMap S R : (a : S) → R) x : R)
        ((P.root : (a : ι) → M) i : M) +
      HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := M) ((algebraMap S R : (a : S) → R) y : R)
        ((P.root : (a : ι) → M) l : M)
⊢ Eq.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) (P.pairingIn S k j) : R)
    ((algebraMap S R : (a : S) → R) (x • P.pairingIn S i j + y • P.pairingIn S l j) : R)

Tactic:
simpa [← P.algebraMap_pairingIn S, -algebraMap_pairingIn] using
    pairing_eq_add_of_root_eq_smul_add_smul h

Premises used: RootPairing.algebraMap_pairingIn, RootPairing.pairing_eq_add_of_root_eq_smul_add_smul
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
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
S : Type u_6
inst_5 : CommRing S
inst_6 : Algebra S R
inst_7 : FaithfulSMul S R
inst_8 : P.IsValuedIn S
i j k : ι
simp : P.pairing j ((P.reflectionPerm i : (a : ι) → ι) k) = P.pairing ((P.reflectionPerm i : (a : ι) → ι) j) k
⊢ P.pairingIn S j ((P.reflectionPerm i : (a : ι) → ι) k) = P.pairingIn S ((P.reflectionPerm i : (a : ι) → ι) j) k

Tactic:
simp only [← (FaithfulSMul.algebraMap_injective S R).eq_iff, algebraMap_pairingIn]

Premises used: Function.Injective.eq_iff, RootPairing.algebraMap_pairingIn, FaithfulSMul.algebraMap_injective
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
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
S : Type u_6
inst_5 : CommRing S
inst_6 : Algebra S R
inst_7 : FaithfulSMul S R
inst_8 : P.IsValuedIn S
i j k : ι
⊢ P.pairing j ((P.reflectionPerm i : (a : ι) → ι) k) = P.pairing ((P.reflectionPerm i : (a : ι) → ι) j) k

Tactic:
pairing_reflectionPerm P i j k

Premises used: RootPairing.pairing_reflectionPerm
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
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
S : Type u_6
inst_5 : CommRing S
inst_6 : Algebra S R
inst_7 : FaithfulSMul S R
inst_8 : P.IsValuedIn S
i j k : ι
⊢ P.pairing j ((P.reflectionPerm i : (a : ι) → ι) k) = P.pairing ((P.reflectionPerm i : (a : ι) → ι) j) k

Tactic:
exact pairing_reflectionPerm P i j k

Premises used: RootPairing.pairing_reflectionPerm
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
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
S : Type u_6
inst_5 : CommRing S
inst_6 : Algebra S R
inst_7 : FaithfulSMul S R
inst_8 : P.IsValuedIn S
i j : ι
⊢ P.pairingIn S ((P.reflectionPerm i : (a : ι) → ι) i) j = -P.pairingIn S i j

Tactic:
simp [← (FaithfulSMul.algebraMap_injective S R).eq_iff]

Premises used: Function.Injective.eq_iff, FaithfulSMul.algebraMap_injective
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
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
S : Type u_6
inst_5 : CommRing S
inst_6 : Algebra S R
inst_7 : FaithfulSMul S R
inst_8 : P.IsValuedIn S
i j : ι
⊢ P.pairingIn S i ((P.reflectionPerm j : (a : ι) → ι) j) = -P.pairingIn S i j

Tactic:
simp [← (FaithfulSMul.algebraMap_injective S R).eq_iff]

Premises used: Function.Injective.eq_iff, FaithfulSMul.algebraMap_injective
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
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
S : Type u_6
inst_5 : CommRing S
inst_6 : Algebra S R
T : Type u_7
inst_7 : CommRing T
inst_8 : Algebra T S
inst_9 : Algebra T R
inst_10 : IsScalarTower T S R
inst_11 : P.IsValuedIn T
i j : ι
h : (algebraMap S R : (a : S) → R) ((algebraMap T S : (a : T) → S) (P.pairingIn T i j) : S) = P.pairing i j
⊢ ∃ (s : S), (algebraMap S R : (a : S) → R) s = P.pairing i j

Tactic:
use algebraMap T S (P.pairingIn T i j)

Premises used: Algebra.algebraMap, RootPairing.pairingIn, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
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
S : Type u_6
inst_5 : CommRing S
inst_6 : Algebra S R
T : Type u_7
inst_7 : CommRing T
inst_8 : Algebra T S
inst_9 : Algebra T R
inst_10 : IsScalarTower T S R
inst_11 : P.IsValuedIn T
i j : ι
⊢ (algebraMap S R : (a : S) → R) ((algebraMap T S : (a : T) → S) (P.pairingIn T i j) : S) = P.pairing i j

Tactic:
simp [← RingHom.comp_apply, ← IsScalarTower.algebraMap_eq T S R]

Premises used: IsScalarTower.algebraMap_eq, RingHom.comp_apply
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
Goal:
ι : Type u_1
R : Type u_2
S_1 : Type u_3
M : Type u_4
N : Type u_5
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 : ι
S : Type u_6
inst_5 : CommRing S
inst_6 : Algebra S R
inst_7 : P.IsCrystallographic
inst_8 : Algebra ℚ R
⊢ P.IsValuedIn ℚ

Tactic:
IsValuedIn.trans P (T := ℤ) (S := ℚ)

Premises used: Rat, Int, RootPairing.IsValuedIn.trans
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
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
S : Type u_6
inst_5 : CommRing S
inst_6 : Algebra S R
T : Type u_7
inst_7 : CommRing T
inst_8 : Algebra T S
inst_9 : Algebra T R
inst_10 : IsScalarTower T S R
inst_11 : P.IsValuedIn T
inst_12 : P.IsValuedIn S
inst_13 : FaithfulSMul S R
i j : ι
a :
  Eq.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) ((algebraMap T S : (a : T) → S) (P.pairingIn T i j) : S) : R)
    ((algebraMap S R : (a : S) → R) (P.pairingIn S i j) : R)
⊢ (algebraMap T S : (a : T) → S) (P.pairingIn T i j) = P.pairingIn S i j

Tactic:
apply FaithfulSMul.algebraMap_injective S R

Premises used: FaithfulSMul.algebraMap_injective
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
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
S : Type u_6
inst_5 : CommRing S
inst_6 : Algebra S R
T : Type u_7
inst_7 : CommRing T
inst_8 : Algebra T S
inst_9 : Algebra T R
inst_10 : IsScalarTower T S R
inst_11 : P.IsValuedIn T
inst_12 : P.IsValuedIn S
inst_13 : FaithfulSMul S R
i j : ι
a :
  Eq.{u_2 + 1} (α := R) ((algebraMap T R : (a : T) → R) (P.pairingIn T i j) : R)
    ((algebraMap S R : (a : S) → R) (P.pairingIn S i j) : R)
⊢ Eq.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) ((algebraMap T S : (a : T) → S) (P.pairingIn T i j) : S) : R)
    ((algebraMap S R : (a : S) → R) (P.pairingIn S i j) : R)

Tactic:
rw [← RingHom.comp_apply, ← IsScalarTower.algebraMap_eq]

Premises used: IsScalarTower.algebraMap_eq, RingHom.comp_apply
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
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
S : Type u_6
inst_5 : CommRing S
inst_6 : Algebra S R
T : Type u_7
inst_7 : CommRing T
inst_8 : Algebra T S
inst_9 : Algebra T R
inst_10 : IsScalarTower T S R
inst_11 : P.IsValuedIn T
inst_12 : P.IsValuedIn S
inst_13 : FaithfulSMul S R
i j : ι
⊢ Eq.{u_2 + 1} (α := R) ((algebraMap T R : (a : T) → R) (P.pairingIn T i j) : R)
    ((algebraMap S R : (a : S) → R) (P.pairingIn S i j) : R)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
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 : Nontrivial R
inst_6 : P.IsCrystallographic
inst_7 : Algebra ℚ R
i j : ι
⊢ P.pairingIn ℚ i j = (↑(P.pairingIn ℤ i j) : ℚ)

Tactic:
simp [← P.algebraMap_pairingIn' ℚ ℤ]

Premises used: Rat, Int, RootPairing.algebraMap_pairingIn'
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
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
S : Type u_6
inst_5 : CommRing S
inst_6 : Algebra S R
inst_7 : Module S M
inst_8 : IsScalarTower S R M
inst_9 : P.IsValuedIn S
x : M
hx : Membership.mem (γ := Submodule S M) (span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x
i : ι
h :
  ∀ (x : R),
    Membership.mem (γ := Set R) (range.{u_2, u_6 + 1} (ι := S) (⇑(algebraMap S R) : (a : S) → R)) x ↔
      x ∈ (↑(LinearMap.range (Algebra.linearMap S R)) : Set R)
⊢ range.{u_2, u_6 + 1} (ι := S) (⇑(algebraMap S R) : (a : S) → R) = (↑(LinearMap.range (Algebra.linearMap S R)) : Set R)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
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
S : Type u_6
inst_5 : CommRing S
inst_6 : Algebra S R
inst_7 : Module S M
inst_8 : IsScalarTower S R M
inst_9 : P.IsValuedIn S
x : M
hx : Membership.mem (γ := Submodule S M) (span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x
i : ι
x_1 : R
⊢ Membership.mem (γ := Set R) (range.{u_2, u_6 + 1} (ι := S) (⇑(algebraMap S R) : (a : S) → R)) x_1 ↔
    x_1 ∈ (↑(LinearMap.range (Algebra.linearMap S R)) : Set R)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
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
S : Type u_6
inst_5 : CommRing S
inst_6 : Algebra S R
inst_7 : Module S M
inst_8 : IsScalarTower S R M
inst_9 : P.IsValuedIn S
x : M
hx : Membership.mem (γ := Submodule S M) (span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x
i : ι
rw : Membership.mem (α := R) (↑(LinearMap.range (Algebra.linearMap S R)) : Set R) ((P.coroot' i : (a : M) → R) x : R)
⊢ Membership.mem.{u_2, u_2} (α := R) (γ := Set R) (range.{u_2, u_6 + 1} (ι := S) (⇑(algebraMap S R) : (a : S) → R))
    ((P.coroot' i : (a : M) → R) x : R)

Tactic:
rw [show range (algebraMap S R) = LinearMap.range (Algebra.linearMap S R) by ext; simp]
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
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
S : Type u_6
inst_5 : CommRing S
inst_6 : Algebra S R
inst_7 : Module S M
inst_8 : IsScalarTower S R M
inst_9 : P.IsValuedIn S
x_1 : M
i : ι
x : M
hx : Membership.mem (γ := Set M) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) x
mem :
  ∀ (k : ι),
    Membership.mem (α := R) (↑(LinearMap.range (Algebra.linearMap S R)) : Set R)
      ((P.coroot' i : (a : M) → R) ((P.root : (a : ι) → M) k : M) : R)
⊢ Membership.mem (α := R) (↑(LinearMap.range (Algebra.linearMap S R)) : Set R) ((P.coroot' i : (a : M) → R) x : R)

Tactic:
obtain ⟨k, rfl⟩ := hx

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
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
S : Type u_6
inst_5 : CommRing S
inst_6 : Algebra S R
inst_7 : Module S M
inst_8 : IsScalarTower S R M
inst_9 : P.IsValuedIn S
x : M
i k : ι
⊢ Membership.mem (α := R) (↑(LinearMap.range (Algebra.linearMap S R)) : Set R)
    ((P.coroot' i : (a : M) → R) ((P.root : (a : ι) → M) k : M) : R)

Tactic:
simpa using RootPairing.exists_value k i

Premises used: RootPairing.exists_value
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
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
S : Type u_6
inst_5 : CommRing S
inst_6 : Algebra S R
inst_7 : Module S M
inst_8 : IsScalarTower S R M
inst_9 : P.IsValuedIn S
x : M
i : ι
⊢ Membership.mem (α := R) (↑(LinearMap.range (Algebra.linearMap S R)) : Set R) ((P.coroot' i : (a : M) → R) 0 : R)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
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
S : Type u_6
inst_5 : CommRing S
inst_6 : Algebra S R
inst_7 : Module S M
inst_8 : IsScalarTower S R M
inst_9 : P.IsValuedIn S
x_1 : M
i : ι
x y : M
hx_1 : Membership.mem (γ := Submodule S M) (span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x
hy_1 : Membership.mem (γ := Submodule S M) (span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) y
hx : Membership.mem (α := R) (↑(LinearMap.range (Algebra.linearMap S R)) : Set R) ((P.coroot' i : (a : M) → R) x : R)
hy : Membership.mem (α := R) (↑(LinearMap.range (Algebra.linearMap S R)) : Set R) ((P.coroot' i : (a : M) → R) y : R)
⊢ Membership.mem (α := R) (↑(LinearMap.range (Algebra.linearMap S R)) : Set R) ((P.coroot' i : (a : M) → R) (x + y) : R)

Tactic:
simpa only [map_add] using add_mem hx hy

Premises used: map_add, AddMemClass.add_mem
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
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
S : Type u_6
inst_5 : CommRing S
inst_6 : Algebra S R
inst_7 : Module S M
inst_8 : IsScalarTower S R M
inst_9 : P.IsValuedIn S
x_1 : M
i : ι
t : S
x : M
hx_1 : Membership.mem (γ := Submodule S M) (span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x
hx : Membership.mem (α := R) (↑(LinearMap.range (Algebra.linearMap S R)) : Set R) ((P.coroot' i : (a : M) → R) x : R)
⊢ Membership.mem (α := R) (↑(LinearMap.range (Algebra.linearMap S R)) : Set R) ((P.coroot' i : (a : M) → R) (t • x) : R)

Tactic:
simpa only [LinearMap.map_smul_of_tower] using Submodule.smul_mem _ t hx

Premises used: LinearMap.map_smul_of_tower, Submodule.smul_mem
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
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
S : Type u_6
inst_5 : CommRing S
inst_6 : Algebra S R
inst_7 : Module S M
inst_8 : IsScalarTower S R M
inst_9 : P.IsValuedIn S
x : M
hx : Membership.mem (γ := Submodule S M) (span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x
i : ι
mem :
  ∀ (x : M) (hx : Membership.mem (γ := Set M) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) x),
    Membership.mem (α := R) (↑(LinearMap.range (Algebra.linearMap S R)) : Set R) ((P.coroot' i : (a : M) → R) x : R)
zero : Membership.mem (α := R) (↑(LinearMap.range (Algebra.linearMap S R)) : Set R) ((P.coroot' i : (a : M) → R) 0 : R)
add :
  ∀ (x y : M),
    Membership.mem (γ := Submodule S M) (span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x →
      Membership.mem (γ := Submodule S M) (span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) y →
        ∀
          (hx :
            Membership.mem (α := R) (↑(LinearMap.range (Algebra.linearMap S R)) : Set R)
              ((P.coroot' i : (a : M) → R) x : R))
          (hy :
            Membership.mem (α := R) (↑(LinearMap.range (Algebra.linearMap S R)) : Set R)
              ((P.coroot' i : (a : M) → R) y : R)),
          Membership.mem (α := R) (↑(LinearMap.range (Algebra.linearMap S R)) : Set R)
            ((P.coroot' i : (a : M) → R) (x + y) : R)
smul :
  ∀ (t : S) (x : M),
    Membership.mem (γ := Submodule S M) (span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x →
      ∀
        (hx :
          Membership.mem (α := R) (↑(LinearMap.range (Algebra.linearMap S R)) : Set R)
            ((P.coroot' i : (a : M) → R) x : R)),
        Membership.mem (α := R) (↑(LinearMap.range (Algebra.linearMap S R)) : Set R)
          ((P.coroot' i : (a : M) → R) (t • x) : R)
⊢ Membership.mem (α := R) (↑(LinearMap.range (Algebra.linearMap S R)) : Set R) ((P.coroot' i : (a : M) → R) x : R)

Tactic:
induction hx using Submodule.span_induction with
  | mem x hx =>
    obtain ⟨k, rfl⟩ := hx
    simpa using RootPairing.exists_value k i
  | zero => simp
  | add x y _ _ hx hy => simpa only [map_add] using add_mem hx hy
  | smul t x _ hx => simpa only [LinearMap.map_smul_of_tower] using Submodule.smul_mem _ t hx

Premises used: map_add, LinearMap.map_smul_of_tower, rfl
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
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
S : Type u_6
inst_5 : CommRing S
inst_6 : Algebra S R
inst_7 : Module S N
inst_8 : IsScalarTower S R N
inst_9 : P.IsValuedIn S
x : N
hx : Membership.mem (γ := Submodule S N) (span S (range.{u_5, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))) x
i : ι
⊢ Membership.mem (α := R) (γ := Submodule S R) (LinearMap.range (Algebra.linearMap S R))
    ((P.root' i : (a : N) → R) x : R)

Tactic:
P.flip.coroot'_apply_apply_mem_of_mem_span S hx i

Premises used: Set.Mem, RootPairing.flip, setOf, RootPairing.coroot'_apply_apply_mem_of_mem_span, Set.range
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
Goal:
ι : Type u_1
R : Type u_2
S_1 : Type u_3
M : Type u_4
N : Type u_5
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 : ι
S : Type u_6
inst_5 : CommRing S
inst_6 : Algebra S R
inst_7 : Module S M
inst_8 : Finite ι
⊢ Module.Finite.{u_6, u_4} S ↥(P.rootSpan S)

Tactic:
Finite.span_of_finite S <| finite_range _

Premises used: Set.Mem, Set.finite_range, Module.Finite.span_of_finite