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
h : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
h₁ :
  ∀ (m : M),
    Eq (α := M)
      (((preReflection ((preReflection x f : (a : M) → M) y)
                (((preReflection (R := R) f ((Dual.eval R M : (a : M) → Dual R (Dual R M)) x) : End R (Dual R M)) :
                    (a : Dual R M) → Dual R M)
                  g) :
              End R M) :
            (a : M) → M)
          m :
        M)
      ((preReflection x f ∘ₗ preReflection y g ∘ₗ preReflection x f : (a : M) → M) m : M)
⊢ preReflection ((preReflection x f : (a : M) → M) y)
      (((preReflection (R := R) f ((Dual.eval R M : (a : M) → Dual R (Dual R M)) x) : End R (Dual R M)) :
          (a : Dual R M) → Dual R M)
        g) =
    preReflection x f ∘ₗ preReflection y g ∘ₗ preReflection x f

Tactic:
ext m
-- 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
h : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
m : M
h₁ :
  m -
      (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((g : (a : M) → R) m : R) y -
          HMul.hMul (α := R) (β := R) ((f : (a : M) → R) m : R) ((g : (a : M) → R) x : R) • y -
        (HMul.hMul (α := R) (β := R) ((g : (a : M) → R) m : R) ((f : (a : M) → R) y : R) • x -
          HMul.hMul (α := R) ((f : (a : M) → R) m : R)
              (HMul.hMul (α := R) (β := R) ((g : (a : M) → R) x : R) ((f : (a : M) → R) y : R)) •
            x)) =
    m - HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) m : R) x -
        (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((g : (a : M) → R) m : R) y -
          HMul.hMul (α := R) (β := R) ((g : (a : M) → R) m : R) ((f : (a : M) → R) y : R) • x) -
      (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) m : R) x -
          (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) m : R) x +
            HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) m : R) x) -
        (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) m : R) ((g : (a : M) → R) x : R) • y -
          HMul.hMul (α := R) ((f : (a : M) → R) m : R)
              (HMul.hMul (α := R) (β := R) ((g : (a : M) → R) x : R) ((f : (a : M) → R) y : R)) •
            x))
⊢ Eq (α := M)
    (((preReflection ((preReflection x f : (a : M) → M) y)
              (((preReflection (R := R) f ((Dual.eval R M : (a : M) → Dual R (Dual R M)) x) : End R (Dual R M)) :
                  (a : Dual R M) → Dual R M)
                g) :
            End R M) :
          (a : M) → M)
        m :
      M)
    ((preReflection x f ∘ₗ preReflection y g ∘ₗ preReflection x f : (a : M) → M) m : M)

Tactic:
simp only [h, preReflection_apply, mul_comm (g x) (f m), mul_two, mul_assoc, Dual.eval_apply,
    LinearMap.sub_apply, LinearMap.coe_comp, LinearMap.smul_apply, smul_eq_mul, smul_sub, sub_smul,
    smul_smul, sub_mul, comp_apply, map_sub, map_smul, add_smul]

Premises used: map_sub, LinearMap.smul_apply, mul_assoc, Module.Dual.eval_apply, sub_smul, smul_smul, sub_mul, Module.preReflection_apply, smul_sub, add_smul, LinearMap.coe_comp, mul_comm, LinearMap.sub_apply, Function.comp_apply, smul_eq_mul, DFunLike.coe, mul_two, map_smul
-- 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
h : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
m : M
⊢ m -
      (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((g : (a : M) → R) m : R) y -
          HMul.hMul (α := R) (β := R) ((f : (a : M) → R) m : R) ((g : (a : M) → R) x : R) • y -
        (HMul.hMul (α := R) (β := R) ((g : (a : M) → R) m : R) ((f : (a : M) → R) y : R) • x -
          HMul.hMul (α := R) ((f : (a : M) → R) m : R)
              (HMul.hMul (α := R) (β := R) ((g : (a : M) → R) x : R) ((f : (a : M) → R) y : R)) •
            x)) =
    m - HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) m : R) x -
        (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((g : (a : M) → R) m : R) y -
          HMul.hMul (α := R) (β := R) ((g : (a : M) → R) m : R) ((f : (a : M) → R) y : R) • x) -
      (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) m : R) x -
          (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) m : R) x +
            HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) m : R) x) -
        (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) m : R) ((g : (a : M) → R) x : R) • y -
          HMul.hMul (α := R) ((f : (a : M) → R) m : R)
              (HMul.hMul (α := R) (β := R) ((g : (a : M) → R) x : R) ((f : (a : M) → R) y : R)) •
            x))

Tactic:
abel
-- 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
h : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
⊢ (reflection h : (a : M) → M) y = y - HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x

Tactic:
preReflection_apply x f y

Premises used: Module.preReflection_apply
-- 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
h : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
⊢ (reflection h : (a : M) → M) x = -x

Tactic:
preReflection_apply_self h

Premises used: Module.preReflection_apply_self
-- 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
h : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
⊢ Involutive (α := M) (⇑(reflection h) : (a : M) → M)

Tactic:
involutive_preReflection h

Premises used: Module.involutive_preReflection
-- 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
h : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
⊢ (reflection h)⁻¹ = reflection h

Tactic:
rfl

Premises used: LinearEquiv.symm, Module.preReflection, Module.reflection, rfl
-- 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
h : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
⊢ (reflection h).symm = reflection h

Tactic:
rfl

Premises used: LinearEquiv.symm, Module.preReflection, Module.reflection, rfl
-- 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
Φ : Set M
h : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
⊢ InvOn (⇑(reflection h) : (a : M) → M) (⇑(reflection h) : (a : M) → M) Φ Φ

Tactic:
⟨fun x _ ↦ involutive_reflection h x, fun x _ ↦ involutive_reflection h x⟩

Premises used: Set.InvOn, Module.involutive_reflection, And.intro
-- 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
Φ : Set M
h : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
h' : MapsTo (⇑(reflection h) : (a : M) → M) Φ Φ
⊢ BijOn (⇑(reflection h) : (a : M) → M) Φ Φ

Tactic:
(invOn_reflection_of_mapsTo h).bijOn h' h'

Premises used: Module.invOn_reflection_of_mapsTo, Set.InvOn.bijOn
-- 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
h : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
p : Submodule R M
hx : x ∈ p
this : ∀ y ∈ p, Membership.mem (α := M) p ((reflection h : (a : M) → M) y : M)
y : M
hy : y ∈ p
⊢ y ∈ Submodule.comap (↑(reflection h) : M →ₗ[R] M) p

Tactic:
simpa using this y hy
-- 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
h : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
p : Submodule R M
hx : x ∈ p
suffices : ∀ y ∈ p, Membership.mem (α := M) p ((reflection h : (a : M) → M) y : M)
⊢ p ∈ End.invtSubmodule (↑(reflection h) : M →ₗ[R] M)

Tactic:
suffices ∀ y ∈ p, reflection h y ∈ p from
    (End.mem_invtSubmodule _).mpr fun y hy ↦ by simpa using this y hy
-- 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
h : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
p : Submodule R M
hx : x ∈ p
y : M
hy : y ∈ p
⊢ Membership.mem (α := M) p ((reflection h : (a : M) → M) y : M)

Tactic:
simpa only [reflection_apply, p.sub_mem_iff_right hy] using p.smul_mem (f y) hx

Premises used: Module.reflection_apply, DFunLike.coe, Submodule.sub_mem_iff_right, Submodule.smul_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
inst_3 : IsDomain R
inst_4 : NeZero.{u_1} (R := R) 2
inst_5 : IsTorsionFree R M
h : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
p : Submodule R M
hp : Disjoint p (R ∙ x)
⊢ p ∈ End.invtSubmodule (↑(reflection h) : M →ₗ[R] M) ↔ p ≤ LinearMap.ker f

Tactic:
⟨fun h' y hy ↦ ?_, fun h' y hy ↦ ?_⟩

Premises used: Iff.intro
-- 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
inst_3 : IsDomain R
inst_4 : NeZero.{u_1} (R := R) 2
inst_5 : IsTorsionFree R M
h : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
p : Submodule R M
hp : Disjoint p (R ∙ x)
refine_1 : ∀ (h' : p ∈ End.invtSubmodule (↑(reflection h) : M →ₗ[R] M)) (y : M) (hy : y ∈ p), y ∈ LinearMap.ker f
refine_2 : ∀ (h' : p ≤ LinearMap.ker f) (y : M) (hy : y ∈ p), y ∈ Submodule.comap (↑(reflection h) : M →ₗ[R] M) p
⊢ p ∈ End.invtSubmodule (↑(reflection h) : M →ₗ[R] M) ↔ p ≤ LinearMap.ker f

Tactic:
refine ⟨fun h' y hy ↦ ?_, fun h' y hy ↦ ?_⟩
-- 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
f : Dual R M
inst_3 : IsDomain R
inst_4 : NeZero.{u_1} (R := R) 2
inst_5 : IsTorsionFree R M
p : Submodule R M
y : M
hy : y ∈ p
h : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) 0 : R) (2 : R)
hp : Disjoint p (R ∙ 0)
h' : p ∈ End.invtSubmodule (↑(reflection h) : M →ₗ[R] M)
⊢ Eq.{u_1 + 1} (α := R) 2 0

Tactic:
simp [← 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
f : Dual R M
inst_3 : IsDomain R
inst_4 : NeZero.{u_1} (R := R) 2
inst_5 : IsTorsionFree R M
p : Submodule R M
y : M
hy : y ∈ p
h : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) 0 : R) (2 : R)
hp : Disjoint p (R ∙ 0)
h' : p ∈ End.invtSubmodule (↑(reflection h) : M →ₗ[R] M)
⊢ False

Tactic:
exact two_ne_zero (α := R) <| by simp [← h]

Premises used: two_ne_zero
-- 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
inst_3 : IsDomain R
inst_4 : NeZero.{u_1} (R := R) 2
inst_5 : IsTorsionFree R M
h : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
p : Submodule R M
hp : Disjoint p (R ∙ x)
h' : p ∈ End.invtSubmodule (↑(reflection h) : M →ₗ[R] M)
y : M
hy : y ∈ p
⊢ x ≠ 0

Tactic:
have hx : x ≠ 0 := by rintro rfl; exact two_ne_zero (α := R) <| by simp [← 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
inst_3 : IsDomain R
inst_4 : NeZero.{u_1} (R := R) 2
inst_5 : IsTorsionFree R M
h : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
p : Submodule R M
hp : Disjoint p (R ∙ x)
h' : p ∈ End.invtSubmodule (↑(reflection h) : M →ₗ[R] M)
y : M
hy : y ∈ p
hx : x ≠ 0
this : HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x ∈ p
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x ∈ p ⊓ R ∙ x

Tactic:
have aux : f y • x ∈ p ⊓ R ∙ x := ⟨this, Submodule.mem_span_singleton.mpr ⟨f y, rfl⟩⟩
-- 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
inst_3 : IsDomain R
inst_4 : NeZero.{u_1} (R := R) 2
inst_5 : IsTorsionFree R M
h : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
p : Submodule R M
hp : Disjoint p (R ∙ x)
h' : p ∈ End.invtSubmodule (↑(reflection h) : M →ₗ[R] M)
y : M
hy : y ∈ p
hx : x ≠ 0
this : HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x ∈ p
aux : HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x ∈ p ⊓ R ∙ x
⊢ Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) y : R) (0 : R) ∨ x = 0

Tactic:
rw [hp.eq_bot, Submodule.mem_bot, smul_eq_zero] at aux

Premises used: Submodule.mem_bot, Disjoint.eq_bot, smul_eq_zero
-- 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
inst_3 : IsDomain R
inst_4 : NeZero.{u_1} (R := R) 2
inst_5 : IsTorsionFree R M
h : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
p : Submodule R M
hp : Disjoint p (R ∙ x)
h' : p ∈ End.invtSubmodule (↑(reflection h) : M →ₗ[R] M)
y : M
hy : y ∈ p
hx : x ≠ 0
this : HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x ∈ p
aux : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) y : R) (0 : R) ∨ x = 0
⊢ y ∈ LinearMap.ker f

Tactic:
aux.resolve_right hx

Premises used: Set.Mem, setOf, Set.preimage, Set.singleton, Or.resolve_right
-- 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
inst_3 : IsDomain R
inst_4 : NeZero.{u_1} (R := R) 2
inst_5 : IsTorsionFree R M
h : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
p : Submodule R M
hp : Disjoint p (R ∙ x)
h' : p ∈ End.invtSubmodule (↑(reflection h) : M →ₗ[R] M)
y : M
hy : y ∈ p
hx : x ≠ 0
this : HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x ∈ p
aux : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) y : R) (0 : R) ∨ x = 0
⊢ y ∈ LinearMap.ker f

Tactic:
exact aux.resolve_right hx

Premises used: Or.resolve_right
-- 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
inst_3 : IsDomain R
inst_4 : NeZero.{u_1} (R := R) 2
inst_5 : IsTorsionFree R M
h : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
p : Submodule R M
hp : Disjoint p (R ∙ x)
h' : p ∈ End.invtSubmodule (↑(reflection h) : M →ₗ[R] M)
y : M
hy : y ∈ p
hx : x ≠ 0
refine_1 : HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x ∈ p
⊢ y ∈ LinearMap.ker f

Tactic:
suffices f y • x ∈ p by
      have aux : f y • x ∈ p ⊓ R ∙ x := ⟨this, Submodule.mem_span_singleton.mpr ⟨f y, rfl⟩⟩
      rw [hp.eq_bot, Submodule.mem_bot, smul_eq_zero] at aux
      exact aux.resolve_right hx
-- 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
inst_3 : IsDomain R
inst_4 : NeZero.{u_1} (R := R) 2
inst_5 : IsTorsionFree R M
h : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
p : Submodule R M
hp : Disjoint p (R ∙ x)
h' : p ∈ End.invtSubmodule (↑(reflection h) : M →ₗ[R] M)
y : M
hy : y ∈ p
hx : x ≠ 0
⊢ y ∈ Submodule.comap (↑(reflection h) : M →ₗ[R] M) p

Tactic:
specialize h' hy
-- 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
inst_3 : IsDomain R
inst_4 : NeZero.{u_1} (R := R) 2
inst_5 : IsTorsionFree R M
h : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
p : Submodule R M
hp : Disjoint p (R ∙ x)
y : M
hy : y ∈ p
hx : x ≠ 0
h' : y ∈ Submodule.comap (↑(reflection h) : M →ₗ[R] M) p
⊢ y - HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x ∈ p

Tactic:
simp only [Submodule.mem_comap, LinearEquiv.coe_coe, reflection_apply] at h'

Premises used: Submodule.mem_comap, Module.reflection_apply, LinearEquiv.coe_coe
-- 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
inst_3 : IsDomain R
inst_4 : NeZero.{u_1} (R := R) 2
inst_5 : IsTorsionFree R M
h : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
p : Submodule R M
hp : Disjoint p (R ∙ x)
y : M
hy : y ∈ p
hx : x ≠ 0
h' : y - HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x ∈ p
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x ∈ p

Tactic:
simpa using p.sub_mem h' hy

Premises used: Submodule.sub_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
inst_3 : IsDomain R
inst_4 : NeZero.{u_1} (R := R) 2
inst_5 : IsTorsionFree R M
h : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
p : Submodule R M
hp : Disjoint p (R ∙ x)
h' : p ≤ LinearMap.ker f
y : M
hy : y ∈ p
⊢ Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) y : R) (0 : R)

Tactic:
simpa using h' hy
-- 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
inst_3 : IsDomain R
inst_4 : NeZero.{u_1} (R := R) 2
inst_5 : IsTorsionFree R M
h : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
p : Submodule R M
hp : Disjoint p (R ∙ x)
h' : p ≤ LinearMap.ker f
y : M
hy : y ∈ p
⊢ Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) y : R) (0 : R)

Tactic:
have hy' : f y = 0 := by simpa using h' hy
-- 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
inst_3 : IsDomain R
inst_4 : NeZero.{u_1} (R := R) 2
inst_5 : IsTorsionFree R M
h : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
p : Submodule R M
hp : Disjoint p (R ∙ x)
h' : p ≤ LinearMap.ker f
y : M
hy : y ∈ p
hy' : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) y : R) (0 : R)
⊢ y ∈ Submodule.comap (↑(reflection h) : M →ₗ[R] M) p

Tactic:
simpa [reflection_apply, hy']

Premises used: Module.reflection_apply
-- 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 y : M
f g : Dual R M
hf : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
hg : Eq.{u_1 + 1} (α := R) ((g : (a : M) → R) y : R) (2 : R)
z : M
t : R
ht : t = HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2
⊢ (HPow.hPow (β := ℕ) (reflection hf * reflection hg) 0 : (a : M) → M) z =
    z +
        (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑0 : ℤ) 2 / 2)) *
            (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑0 : ℤ) 1 / 2)) +
              Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑0 : ℤ) 3 / 2)))) •
          (HSub.hSub (β := R) (HMul.hMul (α := R) (β := R) ((g : (a : M) → R) x : R) ((f : (a : M) → R) z : R))
                ((g : (a : M) → R) z : R) •
              y -
            HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) z : R) x) +
      (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑0 : ℤ) 1 / 2)) *
          (Polynomial.eval t (S R (HDiv.hDiv (α := ℤ) (↑0 : ℤ) 2)) +
            Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑0 : ℤ) 2 / 2)))) •
        (HSub.hSub (β := R) (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) z : R))
              ((f : (a : M) → R) z : R) •
            x -
          HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((g : (a : M) → R) z : R) y)

Tactic:
simp
-- 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 y : M
f g : Dual R M
hf : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
hg : Eq.{u_1 + 1} (α := R) ((g : (a : M) → R) y : R) (2 : R)
z : M
t : R
ht : t = HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2
m : ℕ
ih :
  ((reflection hf * reflection hg) ^ m : (a : M) → M) z =
    z +
        (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 2 / 2)) *
            (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 1 / 2)) +
              Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 3 / 2)))) •
          (HSub.hSub (β := R) (HMul.hMul (α := R) (β := R) ((g : (a : M) → R) x : R) ((f : (a : M) → R) z : R))
                ((g : (a : M) → R) z : R) •
              y -
            HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) z : R) x) +
      (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 1 / 2)) *
          (Polynomial.eval t (S R (HDiv.hDiv (α := ℤ) (↑m : ℤ) 2)) +
            Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 2 / 2)))) •
        (HSub.hSub (β := R) (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) z : R))
              ((f : (a : M) → R) z : R) •
            x -
          HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((g : (a : M) → R) z : R) y)
k : ℤ
⊢ Polynomial.eval t (S R (k - 2)) = t * Polynomial.eval t (S R (k - 1)) - Polynomial.eval t (S R k)

Tactic:
simp [S_sub_two]

Premises used: Polynomial.Chebyshev.S_sub_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
x y : M
f g : Dual R M
hf : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
hg : Eq.{u_1 + 1} (α := R) ((g : (a : M) → R) y : R) (2 : R)
z : M
t : R
ht : t = HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) - 2
m : ℕ
ih :
  ((reflection hf * reflection hg) ^ m : (a : M) → M) z =
    z +
        (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 2 / 2)) *
            (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 1 / 2)) +
              Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 3 / 2)))) •
          (HSub.hSub (β := R) (HMul.hMul (α := R) (β := R) ((g : (a : M) → R) x : R) ((f : (a : M) → R) z : R))
                ((g : (a : M) → R) z : R) •
              y -
            HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) z : R) x) +
      (Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 1 / 2)) *
          (Polynomial.eval t (S R (HDiv.hDiv (α := ℤ) (↑m : ℤ) 2)) +
            Polynomial.eval t (S R (HSub.hSub (α := ℤ) (↑m : ℤ) 2 / 2)))) •
        (HSub.hSub (β := R) (HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) z : R))
              ((f : (a : M) → R) z : R) •
            x -
          HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((g : (a : M) → R) z : R) y)
⊢ ∀ (k : ℤ), Polynomial.eval t (S R (k - 2)) = t * Polynomial.eval t (S R (k - 1)) - Polynomial.eval t (S R k)

Tactic:
have S_eval_t_sub_two (k : ℤ) :
        (S R (k - 2)).eval t = t * (S R (k - 1)).eval t - (S R k).eval t := by
      simp [S_sub_two]