awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Reflection
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
x : M
f : Dual R M
y : M
g : Dual R M
inst_3 : IsAddTorsionFree M
Φ : Set M
hΦ : Φ.Finite
hfx : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
hgy : Eq.{u_1 + 1} (α := R) ((g : (a : M) → R) y : R) (2 : R)
hgx : Eq.{u_1 + 1} (α := R) ((g : (a : M) → R) x : R) (2 : R)
hfy : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) y : R) (2 : R)
hxfΦ : MapsTo (⇑(preReflection x f) : (a : M) → M) Φ Φ
hygΦ : MapsTo (⇑(preReflection y g) : (a : M) → M) Φ Φ
hyΦ : y ∈ Φ
contrapose! :
  ∀ (hΦ : HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x ≠ HSMul.hSMul.{u_1, u_2, u_2} (α := R) 2 y),
    Φ.Infinite
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x = HSMul.hSMul.{u_1, u_2, u_2} (α := R) 2 y

Tactic:
contrapose! hΦ
-- Module: Mathlib.LinearAlgebra.Reflection
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
x : M
f : Dual R M
y : M
g : Dual R M
inst_3 : IsAddTorsionFree M
Φ : Set M
hfx : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
hgy : Eq.{u_1 + 1} (α := R) ((g : (a : M) → R) y : R) (2 : R)
hgx : Eq.{u_1 + 1} (α := R) ((g : (a : M) → R) x : R) (2 : R)
hfy : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) y : R) (2 : R)
hxfΦ : MapsTo (⇑(preReflection x f) : (a : M) → M) Φ Φ
hygΦ : MapsTo (⇑(preReflection y g) : (a : M) → M) Φ Φ
hyΦ : y ∈ Φ
hΦ : HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x ≠ HSMul.hSMul.{u_1, u_2, u_2} (α := R) 2 y
rw : HMul.hMul (α := R) 2 2 = 4
⊢ HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) = 4

Tactic:
rw [hfy, hgx]
-- Module: Mathlib.LinearAlgebra.Reflection
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
x : M
f : Dual R M
y : M
g : Dual R M
inst_3 : IsAddTorsionFree M
Φ : Set M
hfx : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
hgy : Eq.{u_1 + 1} (α := R) ((g : (a : M) → R) y : R) (2 : R)
hgx : Eq.{u_1 + 1} (α := R) ((g : (a : M) → R) x : R) (2 : R)
hfy : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) y : R) (2 : R)
hxfΦ : MapsTo (⇑(preReflection x f) : (a : M) → M) Φ Φ
hygΦ : MapsTo (⇑(preReflection y g) : (a : M) → M) Φ Φ
hyΦ : y ∈ Φ
hΦ : HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x ≠ HSMul.hSMul.{u_1, u_2, u_2} (α := R) 2 y
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : Eq.{u_1 + 1} (α := R) (↑(HMul.hMul (α := ℕ) 2 2) : R) 4
⊢ HMul.hMul (α := R) 2 2 = 4

Tactic:
norm_cast
-- Module: Mathlib.LinearAlgebra.Reflection
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
x : M
f : Dual R M
y : M
g : Dual R M
inst_3 : IsAddTorsionFree M
Φ : Set M
hfx : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
hgy : Eq.{u_1 + 1} (α := R) ((g : (a : M) → R) y : R) (2 : R)
hgx : Eq.{u_1 + 1} (α := R) ((g : (a : M) → R) x : R) (2 : R)
hfy : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) y : R) (2 : R)
hxfΦ : MapsTo (⇑(preReflection x f) : (a : M) → M) Φ Φ
hygΦ : MapsTo (⇑(preReflection y g) : (a : M) → M) Φ Φ
hyΦ : y ∈ Φ
hΦ : HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x ≠ HSMul.hSMul.{u_1, u_2, u_2} (α := R) 2 y
apply : (range fun (n : ℕ) ↦ (⇑(reflection hgy ≪≫ₗ reflection hfx) : (a : M) → M)^[n] y) ⊆ Φ
⊢ Φ.Infinite

Tactic:
apply ((infinite_range_reflection_reflection_iterate_iff hfx hgy
    (by rw [hfy, hgx]; norm_cast)).mpr hΦ).mono

Premises used: Iff.mpr, Set.Infinite.mono, Module.infinite_range_reflection_reflection_iterate_iff
-- Module: Mathlib.LinearAlgebra.Reflection
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
x : M
f : Dual R M
y : M
g : Dual R M
inst_3 : IsAddTorsionFree M
Φ : Set M
hfx : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
hgy : Eq.{u_1 + 1} (α := R) ((g : (a : M) → R) y : R) (2 : R)
hgx : Eq.{u_1 + 1} (α := R) ((g : (a : M) → R) x : R) (2 : R)
hfy : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) y : R) (2 : R)
hxfΦ : MapsTo (⇑(preReflection x f) : (a : M) → M) Φ Φ
hygΦ : MapsTo (⇑(preReflection y g) : (a : M) → M) Φ Φ
hyΦ : y ∈ Φ
hΦ : HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x ≠ HSMul.hSMul.{u_1, u_2, u_2} (α := R) 2 y
rw : ∀ (y_1 : ℕ), (⇑(reflection hgy ≪≫ₗ reflection hfx) : (a : M) → M)^[y_1] y ∈ Φ
⊢ (range fun (n : ℕ) ↦ (⇑(reflection hgy ≪≫ₗ reflection hfx) : (a : M) → M)^[n] y) ⊆ Φ

Tactic:
rw [range_subset_iff]

Premises used: Set.range_subset_iff
-- Module: Mathlib.LinearAlgebra.Reflection
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
x : M
f : Dual R M
y : M
g : Dual R M
inst_3 : IsAddTorsionFree M
Φ : Set M
hfx : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
hgy : Eq.{u_1 + 1} (α := R) ((g : (a : M) → R) y : R) (2 : R)
hgx : Eq.{u_1 + 1} (α := R) ((g : (a : M) → R) x : R) (2 : R)
hfy : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) y : R) (2 : R)
hxfΦ : MapsTo (⇑(preReflection x f) : (a : M) → M) Φ Φ
hygΦ : MapsTo (⇑(preReflection y g) : (a : M) → M) Φ Φ
hyΦ : y ∈ Φ
hΦ : HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x ≠ HSMul.hSMul.{u_1, u_2, u_2} (α := R) 2 y
n : ℕ
rw :
  (⇑(reflection hgy ≪≫ₗ reflection hfx) : (a : M) → M)^[n] y ∈
    (comp (β := M) (⇑(reflection hfx) : (a : M) → M) (⇑(reflection hgy) : (a : M) → M))^[n] '' Φ
⊢ (⇑(reflection hgy ≪≫ₗ reflection hfx) : (a : M) → M)^[n] y ∈ Φ

Tactic:
rw [← IsFixedPt.image_iterate ((bijOn_reflection_of_mapsTo hfx hxfΦ).comp
    (bijOn_reflection_of_mapsTo hgy hygΦ)).image_eq n]

Premises used: Module.bijOn_reflection_of_mapsTo, Set.BijOn.comp, Set.BijOn.image_eq, Function.IsFixedPt.image_iterate
-- Module: Mathlib.LinearAlgebra.Reflection
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
x : M
f : Dual R M
y : M
g : Dual R M
inst_3 : IsAddTorsionFree M
Φ : Set M
hfx : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
hgy : Eq.{u_1 + 1} (α := R) ((g : (a : M) → R) y : R) (2 : R)
hgx : Eq.{u_1 + 1} (α := R) ((g : (a : M) → R) x : R) (2 : R)
hfy : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) y : R) (2 : R)
hxfΦ : MapsTo (⇑(preReflection x f) : (a : M) → M) Φ Φ
hygΦ : MapsTo (⇑(preReflection y g) : (a : M) → M) Φ Φ
hyΦ : y ∈ Φ
hΦ : HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x ≠ HSMul.hSMul.{u_1, u_2, u_2} (α := R) 2 y
n : ℕ
⊢ (⇑(reflection hgy ≪≫ₗ reflection hfx) : (a : M) → M)^[n] y ∈
    (comp (β := M) (⇑(reflection hfx) : (a : M) → M) (⇑(reflection hgy) : (a : M) → M))^[n] '' Φ

Tactic:
mem_image_of_mem _ hyΦ

Premises used: Set.Mem, Set.mem_image_of_mem
-- Module: Mathlib.LinearAlgebra.Reflection
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
x : M
f : Dual R M
y : M
g : Dual R M
inst_3 : IsAddTorsionFree M
Φ : Set M
hfx : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
hgy : Eq.{u_1 + 1} (α := R) ((g : (a : M) → R) y : R) (2 : R)
hgx : Eq.{u_1 + 1} (α := R) ((g : (a : M) → R) x : R) (2 : R)
hfy : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) y : R) (2 : R)
hxfΦ : MapsTo (⇑(preReflection x f) : (a : M) → M) Φ Φ
hygΦ : MapsTo (⇑(preReflection y g) : (a : M) → M) Φ Φ
hyΦ : y ∈ Φ
hΦ : HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x ≠ HSMul.hSMul.{u_1, u_2, u_2} (α := R) 2 y
n : ℕ
⊢ (⇑(reflection hgy ≪≫ₗ reflection hfx) : (a : M) → M)^[n] y ∈
    (comp (β := M) (⇑(reflection hfx) : (a : M) → M) (⇑(reflection hgy) : (a : M) → M))^[n] '' Φ

Tactic:
exact mem_image_of_mem _ hyΦ

Premises used: Set.mem_image_of_mem
-- Module: Mathlib.LinearAlgebra.Reflection
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : IsAddTorsionFree M
r : ι ↪ M
c : ι → Dual R M
hfin : Set.Finite.{u_2} (α := M) (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M))
h_two : ∀ (i : ι), Eq.{u_1 + 1} (α := R) ((c i : (a : M) → R) ((r : (a : ι) → M) i : M) : R) (2 : R)
h_mapsTo :
  ∀ (i : ι),
    MapsTo.{u_2, u_2} (α := M) (β := M) (⇑(preReflection ((r : (a : ι) → M) i) (c i) : End R M) : (a : M) → M)
      (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M)) (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M))
i j : ι
hij :
  Eq (α := Dual.{u_1, u_2} R ↥(span R (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M))))
    ((LinearMap.dualMap (Submodule.subtype (span R (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M)))) :
          (a : Dual R M) → Dual R ↥(span R (range (⇑r : (a : ι) → M))))
        (c i) :
      Dual.{u_1, u_2} R ↥(span R (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M))))
    ((LinearMap.dualMap (Submodule.subtype (span R (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M)))) :
          (a : Dual R M) → Dual R ↥(span R (range (⇑r : (a : ι) → M))))
        (c j) :
      Dual.{u_1, u_2} R ↥(span R (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M))))
e_a : i = j
⊢ c i = c j

Tactic:
congr
-- Module: Mathlib.LinearAlgebra.Reflection
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : IsAddTorsionFree M
r : ι ↪ M
c : ι → Dual R M
hfin : Set.Finite.{u_2} (α := M) (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M))
h_two : ∀ (i : ι), Eq.{u_1 + 1} (α := R) ((c i : (a : M) → R) ((r : (a : ι) → M) i : M) : R) (2 : R)
h_mapsTo :
  ∀ (i : ι),
    MapsTo.{u_2, u_2} (α := M) (β := M) (⇑(preReflection ((r : (a : ι) → M) i) (c i) : End R M) : (a : M) → M)
      (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M)) (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M))
i j : ι
hij :
  Eq (α := Dual.{u_1, u_2} R ↥(span R (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M))))
    ((LinearMap.dualMap (Submodule.subtype (span R (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M)))) :
          (a : Dual R M) → Dual R ↥(span R (range (⇑r : (a : ι) → M))))
        (c i) :
      Dual.{u_1, u_2} R ↥(span R (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M))))
    ((LinearMap.dualMap (Submodule.subtype (span R (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M)))) :
          (a : Dual R M) → Dual R ↥(span R (range (⇑r : (a : ι) → M))))
        (c j) :
      Dual.{u_1, u_2} R ↥(span R (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M))))
this :
  ∀ (k : ι),
    Eq.{u_1 + 1} (α := R) ((c i : (a : M) → R) ((r : (a : ι) → M) k : M) : R)
      ((c j : (a : M) → R) ((r : (a : ι) → M) k : M) : R)
rw : Eq.{u_2 + 1} (α := M) ((r : (a : ι) → M) i : M) ((r : (a : ι) → M) j : M)
⊢ i = j

Tactic:
rw [← EmbeddingLike.apply_eq_iff_eq r]

Premises used: EmbeddingLike.apply_eq_iff_eq
-- Module: Mathlib.LinearAlgebra.Reflection
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : IsAddTorsionFree M
r : ι ↪ M
c : ι → Dual R M
hfin : Set.Finite.{u_2} (α := M) (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M))
h_two : ∀ (i : ι), Eq.{u_1 + 1} (α := R) ((c i : (a : M) → R) ((r : (a : ι) → M) i : M) : R) (2 : R)
h_mapsTo :
  ∀ (i : ι),
    MapsTo.{u_2, u_2} (α := M) (β := M) (⇑(preReflection ((r : (a : ι) → M) i) (c i) : End R M) : (a : M) → M)
      (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M)) (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M))
i j : ι
hij :
  Eq (α := Dual.{u_1, u_2} R ↥(span R (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M))))
    ((LinearMap.dualMap (Submodule.subtype (span R (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M)))) :
          (a : Dual R M) → Dual R ↥(span R (range (⇑r : (a : ι) → M))))
        (c i) :
      Dual.{u_1, u_2} R ↥(span R (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M))))
    ((LinearMap.dualMap (Submodule.subtype (span R (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M)))) :
          (a : Dual R M) → Dual R ↥(span R (range (⇑r : (a : ι) → M))))
        (c j) :
      Dual.{u_1, u_2} R ↥(span R (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M))))
this :
  ∀ (k : ι),
    Eq.{u_1 + 1} (α := R) ((c i : (a : M) → R) ((r : (a : ι) → M) k : M) : R)
      ((c j : (a : M) → R) ((r : (a : ι) → M) k : M) : R)
rw : Eq.{u_1 + 1} (α := R) ((c i : (a : M) → R) ((r : (a : ι) → M) i : M) : R) (2 : R)
rw₁ rw₂ : Eq.{u_1 + 1} (α := R) 2 2
⊢ Eq.{u_1 + 1} (α := R) ((c j : (a : M) → R) ((r : (a : ι) → M) i : M) : R) (2 : R)

Tactic:
rw [← this, h_two]
-- Module: Mathlib.LinearAlgebra.Reflection
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : IsAddTorsionFree M
r : ι ↪ M
c : ι → Dual R M
hfin : Set.Finite.{u_2} (α := M) (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M))
h_two : ∀ (i : ι), Eq.{u_1 + 1} (α := R) ((c i : (a : M) → R) ((r : (a : ι) → M) i : M) : R) (2 : R)
h_mapsTo :
  ∀ (i : ι),
    MapsTo.{u_2, u_2} (α := M) (β := M) (⇑(preReflection ((r : (a : ι) → M) i) (c i) : End R M) : (a : M) → M)
      (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M)) (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M))
i j : ι
hij :
  Eq (α := Dual.{u_1, u_2} R ↥(span R (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M))))
    ((LinearMap.dualMap (Submodule.subtype (span R (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M)))) :
          (a : Dual R M) → Dual R ↥(span R (range (⇑r : (a : ι) → M))))
        (c i) :
      Dual.{u_1, u_2} R ↥(span R (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M))))
    ((LinearMap.dualMap (Submodule.subtype (span R (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M)))) :
          (a : Dual R M) → Dual R ↥(span R (range (⇑r : (a : ι) → M))))
        (c j) :
      Dual.{u_1, u_2} R ↥(span R (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M))))
this :
  ∀ (k : ι),
    Eq.{u_1 + 1} (α := R) ((c i : (a : M) → R) ((r : (a : ι) → M) k : M) : R)
      ((c j : (a : M) → R) ((r : (a : ι) → M) k : M) : R)
rw : Eq.{u_1 + 1} (α := R) ((c j : (a : M) → R) ((r : (a : ι) → M) j : M) : R) (2 : R)
rw₁ rw₂ : Eq.{u_1 + 1} (α := R) 2 2
⊢ Eq.{u_1 + 1} (α := R) ((c i : (a : M) → R) ((r : (a : ι) → M) j : M) : R) (2 : R)

Tactic:
rw [this, h_two]
-- Module: Mathlib.LinearAlgebra.Reflection
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : IsAddTorsionFree M
r : ι ↪ M
c : ι → Dual R M
hfin : Set.Finite.{u_2} (α := M) (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M))
h_two : ∀ (i : ι), Eq.{u_1 + 1} (α := R) ((c i : (a : M) → R) ((r : (a : ι) → M) i : M) : R) (2 : R)
h_mapsTo :
  ∀ (i : ι),
    MapsTo.{u_2, u_2} (α := M) (β := M) (⇑(preReflection ((r : (a : ι) → M) i) (c i) : End R M) : (a : M) → M)
      (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M)) (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M))
i j : ι
hij :
  Eq (α := Dual.{u_1, u_2} R ↥(span R (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M))))
    ((LinearMap.dualMap (Submodule.subtype (span R (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M)))) :
          (a : Dual R M) → Dual R ↥(span R (range (⇑r : (a : ι) → M))))
        (c i) :
      Dual.{u_1, u_2} R ↥(span R (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M))))
    ((LinearMap.dualMap (Submodule.subtype (span R (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M)))) :
          (a : Dual R M) → Dual R ↥(span R (range (⇑r : (a : ι) → M))))
        (c j) :
      Dual.{u_1, u_2} R ↥(span R (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M))))
this :
  ∀ (k : ι),
    Eq.{u_1 + 1} (α := R) ((c i : (a : M) → R) ((r : (a : ι) → M) k : M) : R)
      ((c j : (a : M) → R) ((r : (a : ι) → M) k : M) : R)
⊢ Eq.{u_2 + 1} (α := M) ((r : (a : ι) → M) i : M) ((r : (a : ι) → M) j : M)

Tactic:
exact eq_of_mapsTo_reflection_of_mem (f := c i) (g := c j) hfin (h_two i) (h_two j)
      (by rw [← this, h_two]) (by rw [this, h_two]) (h_mapsTo i) (h_mapsTo j) (mem_range_self j)

Premises used: Set.mem_range_self, Module.eq_of_mapsTo_reflection_of_mem
-- Module: Mathlib.LinearAlgebra.Reflection
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : IsAddTorsionFree M
r : ι ↪ M
c : ι → Dual R M
hfin : Set.Finite.{u_2} (α := M) (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M))
h_two : ∀ (i : ι), Eq.{u_1 + 1} (α := R) ((c i : (a : M) → R) ((r : (a : ι) → M) i : M) : R) (2 : R)
h_mapsTo :
  ∀ (i : ι),
    MapsTo.{u_2, u_2} (α := M) (β := M) (⇑(preReflection ((r : (a : ι) → M) i) (c i) : End R M) : (a : M) → M)
      (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M)) (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M))
i j : ι
hij :
  Eq (α := Dual.{u_1, u_2} R ↥(span R (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M))))
    ((LinearMap.dualMap (Submodule.subtype (span R (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M)))) :
          (a : Dual R M) → Dual R ↥(span R (range (⇑r : (a : ι) → M))))
        (c i) :
      Dual.{u_1, u_2} R ↥(span R (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M))))
    ((LinearMap.dualMap (Submodule.subtype (span R (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M)))) :
          (a : Dual R M) → Dual R ↥(span R (range (⇑r : (a : ι) → M))))
        (c j) :
      Dual.{u_1, u_2} R ↥(span R (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M))))
e_a :
  ∀ (k : ι),
    Eq.{u_1 + 1} (α := R) ((c i : (a : M) → R) ((r : (a : ι) → M) k : M) : R)
      ((c j : (a : M) → R) ((r : (a : ι) → M) k : M) : R)
⊢ i = j

Tactic:
suffices ∀ k, c i (r k) = c j (r k) by
    rw [← EmbeddingLike.apply_eq_iff_eq r]
    exact eq_of_mapsTo_reflection_of_mem (f := c i) (g := c j) hfin (h_two i) (h_two j)
      (by rw [← this, h_two]) (by rw [this, h_two]) (h_mapsTo i) (h_mapsTo j) (mem_range_self j)
-- Module: Mathlib.LinearAlgebra.Reflection
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : IsAddTorsionFree M
r : ι ↪ M
c : ι → Dual R M
hfin : Set.Finite.{u_2} (α := M) (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M))
h_two : ∀ (i : ι), Eq.{u_1 + 1} (α := R) ((c i : (a : M) → R) ((r : (a : ι) → M) i : M) : R) (2 : R)
h_mapsTo :
  ∀ (i : ι),
    MapsTo.{u_2, u_2} (α := M) (β := M) (⇑(preReflection ((r : (a : ι) → M) i) (c i) : End R M) : (a : M) → M)
      (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M)) (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M))
i j : ι
hij :
  Eq (α := Dual.{u_1, u_2} R ↥(span R (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M))))
    ((LinearMap.dualMap (Submodule.subtype (span R (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M)))) :
          (a : Dual R M) → Dual R ↥(span R (range (⇑r : (a : ι) → M))))
        (c i) :
      Dual.{u_1, u_2} R ↥(span R (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M))))
    ((LinearMap.dualMap (Submodule.subtype (span R (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M)))) :
          (a : Dual R M) → Dual R ↥(span R (range (⇑r : (a : ι) → M))))
        (c j) :
      Dual.{u_1, u_2} R ↥(span R (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M))))
k : ι
⊢ Eq.{u_1 + 1} (α := R) ((c i : (a : M) → R) ((r : (a : ι) → M) k : M) : R)
    ((c j : (a : M) → R) ((r : (a : ι) → M) k : M) : R)

Tactic:
simpa using LinearMap.congr_fun hij ⟨r k, Submodule.subset_span (mem_range_self k)⟩

Premises used: Set.mem_range_self, Subtype.mk, LinearMap.congr_fun, Submodule.subset_span, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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
b : P.Base
inst_5 : Nonempty ι
inst_6 : NeZero.{u_2} (R := R) 2
by_contra! : ∀ (contra : b.support = ∅), False
⊢ b.support.Nonempty

Tactic:
by_contra! contra
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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
b : P.Base
inst_5 : Nonempty ι
inst_6 : NeZero.{u_2} (R := R) 2
contra : b.support = ∅
inhabit : ∀ (inhabited_h : Inhabited ι), False
⊢ False

Tactic:
inhabit ι
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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
b : P.Base
inst_5 : Nonempty ι
inst_6 : NeZero.{u_2} (R := R) 2
contra : b.support = ∅
inhabited_h : Inhabited ι
⊢ False

Tactic:
simpa [P.ne_zero default, contra] using b.root_mem_or_neg_mem default

Premises used: Inhabited.default, RootPairing.ne_zero, RootPairing.Base.root_mem_or_neg_mem
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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
b : P.Base
inst_5 : Nontrivial R
i j : ι
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
contra : Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
⊢ (↑{i, j} : Set ι) ⊆ (↑b.support : Set ι)

Tactic:
simp [Set.insert_subset_iff, hi, hj]

Premises used: Set.insert_subset_iff
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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
b : P.Base
inst_5 : Nontrivial R
i j : ι
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
contra : Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
⊢ Eq.{u_3 + 1} (α := M)
    (∑ i ∈ {i, j}, HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) (1 i) ((P.root : (a : ι) → M) i : M)) 0

Tactic:
simp [Finset.sum_pair hij, contra]

Premises used: Finset.sum_pair
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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
b : P.Base
inst_5 : Nontrivial R
i j : ι
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
contra : Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
⊢ ∀ (i_1 : ι), Membership.mem (γ := Finset ι) {i, j} i_1 → Eq.{u_2 + 1} (α := R) (1 i_1) 0

Tactic:
have := linearIndepOn_iff'.mp b.linearIndepOn_root ({i, j} : Finset ι) 1
    (by simp [Set.insert_subset_iff, hi, hj]) (by simp [Finset.sum_pair hij, contra])
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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
b : P.Base
inst_5 : Nontrivial R
i j : ι
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
contra : Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
this : ∀ (i_1 : ι), Membership.mem (γ := Finset ι) {i, j} i_1 → Eq.{u_2 + 1} (α := R) (1 i_1) 0
⊢ False

Tactic:
simp_all
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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
b : P.Base
inst_5 : Nontrivial R
i j : ι
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
intro : ∀ (contra : Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)), False
intro₁ :
  ∀ (contra : Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M))
    (this : ∀ (i_1 : ι), Membership.mem (γ := Finset ι) {i, j} i_1 → Eq.{u_2 + 1} (α := R) (1 i_1) 0), False
⊢ Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)

Tactic:
classical
  intro contra
  have := linearIndepOn_iff'.mp b.linearIndepOn_root ({i, j} : Finset ι) 1
    (by simp [Set.insert_subset_iff, hi, hj]) (by simp [Finset.sum_pair hij, contra])
  simp_all
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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
b : P.Base
i j : ↥b.support
hij : i ≠ j
⊢ {(↑j : ι), (↑i : ι)} ⊆ (↑b.support : Set ι)

Tactic:
simp [pair_subset_iff]

Premises used: Set.pair_subset_iff