-- Mathlib/LinearAlgebra/Reflection.lean
/-- See also `Module.Dual.eq_of_preReflection_mapsTo'` for a variant of this lemma which
applies when `Φ` does not span.

This rather technical-looking lemma exists because it is exactly what is needed to establish various
uniqueness results for root data / systems. One might regard this lemma as lying at the boundary of
linear algebra and combinatorics since the finiteness assumption is the key. -/
lemma Dual.eq_of_preReflection_mapsTo [CharZero R] [NoZeroSMulDivisors R M]
    {x : M} {Φ : Set M} (hΦ₁ : Φ.Finite) (hΦ₂ : span R Φ = ⊤) {f g : Dual R M}
    (hf₁ : f x = 2) (hf₂ : MapsTo (preReflection x f) Φ Φ)
    (hg₁ : g x = 2) (hg₂ : MapsTo (preReflection x g) Φ Φ) :
    f = g

Proof state:
case succ
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CharZero R
inst✝ : NoZeroSMulDivisors R M
x : M
Φ : Set M
hΦ₁ : Φ.Finite
hΦ₂ : span R Φ = ⊤
f g : Dual R M
hf₁ : f x = 2
hf₂ : MapsTo (⇑(preReflection x f)) Φ Φ
hg₁ : g x = 2
hg₂ : MapsTo (⇑(preReflection x g)) Φ Φ
hx : x ≠ 0
u : M ≃ₗ[R] M := reflection hg₁ * reflection hf₁
hu : ↑u = LinearMap.id + LinearMap.smulRight (f - g) x
n : ℕ
ih : ↑(u ^ n) = LinearMap.id + ↑n • LinearMap.smulRight (f - g) x
this : LinearMap.smulRight (f - g) x ∘ₗ (↑n • LinearMap.smulRight (f - g) x) = 0
⊢ LinearMap.id * LinearMap.id + LinearMap.id * ↑n • LinearMap.smulRight (f - g) x +
      (LinearMap.smulRight (f - g) x * LinearMap.id +
        LinearMap.smulRight (f - g) x * ↑n • LinearMap.smulRight (f - g) x) =
    LinearMap.id + ↑(n + 1) • LinearMap.smulRight (f - g) x

Tactic:
simp_rw [LinearMap.mul_eq_comp, LinearMap.comp_id, LinearMap.id_comp, this, add_zero,
  add_assoc, Nat.cast_succ, add_smul, one_smul]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CharZero R
inst✝ : NoZeroSMulDivisors R M
x : M
Φ : Set M
hΦ₁ : Φ.Finite
hΦ₂ : span R Φ = ⊤
f g : Dual R M
hf₁ : f x = 2
hf₂ : MapsTo (⇑(preReflection x f)) Φ Φ
hg₁ : g x = 2
hg₂ : MapsTo (⇑(preReflection x g)) Φ Φ
hx : x ≠ 0
u : M ≃ₗ[R] M := reflection hg₁ * reflection hf₁
hu : ↑u = LinearMap.id + LinearMap.smulRight (f - g) x
⊢ f = g

Tactic:
replace hu : ∀ (n : ℕ),
    ↑(u ^ n) = LinearMap.id (R := R) (M := M) + (n : R) • (f - g).smulRight x := by
  intros n
  induction n with
  | zero => simp
  | succ n ih =>
    have : ((f - g).smulRight x).comp ((n : R) • (f - g).smulRight x) = 0 := by
      ext; simp [hf₁, hg₁]
    rw [pow_succ', LinearEquiv.coe_toLinearMap_mul, ih, hu, add_mul, mul_add, mul_add]
    simp_rw [LinearMap.mul_eq_comp, LinearMap.comp_id, LinearMap.id_comp, this, add_zero,
      add_assoc, Nat.cast_succ, add_smul, one_smul]

Result:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CharZero R
inst✝ : NoZeroSMulDivisors R M
x : M
Φ : Set M
hΦ₁ : Φ.Finite
hΦ₂ : span R Φ = ⊤
f g : Dual R M
hf₁ : f x = 2
hf₂ : MapsTo (⇑(preReflection x f)) Φ Φ
hg₁ : g x = 2
hg₂ : MapsTo (⇑(preReflection x g)) Φ Φ
hx : x ≠ 0
u : M ≃ₗ[R] M := reflection hg₁ * reflection hf₁
hu : ∀ (n : ℕ), ↑(u ^ n) = LinearMap.id + ↑n • LinearMap.smulRight (f - g) x
⊢ f = g

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CharZero R
inst✝ : NoZeroSMulDivisors R M
x : M
Φ : Set M
hΦ₁ : Φ.Finite
hΦ₂ : span R Φ = ⊤
f g : Dual R M
hf₁ : f x = 2
hf₂ : MapsTo (⇑(preReflection x f)) Φ Φ
hg₁ : g x = 2
hg₂ : MapsTo (⇑(preReflection x g)) Φ Φ
hx : x ≠ 0
u : M ≃ₗ[R] M := reflection hg₁ * reflection hf₁
hu : ↑u = LinearMap.id + LinearMap.smulRight (f - g) x
⊢ ∀ (n : ℕ), ↑(u ^ n) = LinearMap.id + ↑n • LinearMap.smulRight (f - g) x

Tactic:
intros n

Result:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CharZero R
inst✝ : NoZeroSMulDivisors R M
x : M
Φ : Set M
hΦ₁ : Φ.Finite
hΦ₂ : span R Φ = ⊤
f g : Dual R M
hf₁ : f x = 2
hf₂ : MapsTo (⇑(preReflection x f)) Φ Φ
hg₁ : g x = 2
hg₂ : MapsTo (⇑(preReflection x g)) Φ Φ
hx : x ≠ 0
u : M ≃ₗ[R] M := reflection hg₁ * reflection hf₁
hu : ↑u = LinearMap.id + LinearMap.smulRight (f - g) x
n : ℕ
⊢ ↑(u ^ n) = LinearMap.id + ↑n • LinearMap.smulRight (f - g) x

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CharZero R
inst✝ : NoZeroSMulDivisors R M
x : M
Φ : Set M
hΦ₁ : Φ.Finite
hΦ₂ : span R Φ = ⊤
f g : Dual R M
hf₁ : f x = 2
hf₂ : MapsTo (⇑(preReflection x f)) Φ Φ
hg₁ : g x = 2
hg₂ : MapsTo (⇑(preReflection x g)) Φ Φ
hx : x ≠ 0
u : M ≃ₗ[R] M := reflection hg₁ * reflection hf₁
hu : ↑u = LinearMap.id + LinearMap.smulRight (f - g) x
n : ℕ
⊢ ↑(u ^ n) = LinearMap.id + ↑n • LinearMap.smulRight (f - g) x

Tactic:
induction n with
| zero => simp
| succ n ih =>
  have : ((f - g).smulRight x).comp ((n : R) • (f - g).smulRight x) = 0 := by
    ext; simp [hf₁, hg₁]
  rw [pow_succ', LinearEquiv.coe_toLinearMap_mul, ih, hu, add_mul, mul_add, mul_add]
  simp_rw [LinearMap.mul_eq_comp, LinearMap.comp_id, LinearMap.id_comp, this, add_zero,
    add_assoc, Nat.cast_succ, add_smul, one_smul]

Result:
no goals

Proof state:
case h
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CharZero R
inst✝ : NoZeroSMulDivisors R M
x : M
Φ : Set M
hΦ₁ : Φ.Finite
hΦ₂ : span R Φ = ⊤
f g : Dual R M
hf₁ : f x = 2
hf₂ : MapsTo (⇑(preReflection x f)) Φ Φ
hg₁ : g x = 2
hg₂ : MapsTo (⇑(preReflection x g)) Φ Φ
hx : x ≠ 0
u : M ≃ₗ[R] M := reflection hg₁ * reflection hf₁
hu : ↑u = LinearMap.id + LinearMap.smulRight (f - g) x
n : ℕ
ih : ↑(u ^ n) = LinearMap.id + ↑n • LinearMap.smulRight (f - g) x
x✝ : M
⊢ (LinearMap.smulRight (f - g) x ∘ₗ (↑n • LinearMap.smulRight (f - g) x)) x✝ = 0 x✝

Tactic:
simp [hf₁, hg₁]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CharZero R
inst✝ : NoZeroSMulDivisors R M
x : M
Φ : Set M
hΦ₁ : Φ.Finite
hΦ₂ : span R Φ = ⊤
f g : Dual R M
hf₁ : f x = 2
hf₂ : MapsTo (⇑(preReflection x f)) Φ Φ
hg₁ : g x = 2
hg₂ : MapsTo (⇑(preReflection x g)) Φ Φ
hx : x ≠ 0
⊢ f = g

Tactic:
let u := reflection hg₁ * reflection hf₁

Result:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CharZero R
inst✝ : NoZeroSMulDivisors R M
x : M
Φ : Set M
hΦ₁ : Φ.Finite
hΦ₂ : span R Φ = ⊤
f g : Dual R M
hf₁ : f x = 2
hf₂ : MapsTo (⇑(preReflection x f)) Φ Φ
hg₁ : g x = 2
hg₂ : MapsTo (⇑(preReflection x g)) Φ Φ
hx : x ≠ 0
u : M ≃ₗ[R] M := reflection hg₁ * reflection hf₁
⊢ f = g

Proof state:
case succ
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CharZero R
inst✝ : NoZeroSMulDivisors R M
x : M
Φ : Set M
hΦ₁ : Φ.Finite
hΦ₂ : span R Φ = ⊤
f g : Dual R M
hf₁ : f x = 2
hf₂ : MapsTo (⇑(preReflection x f)) Φ Φ
hg₁ : g x = 2
hg₂ : MapsTo (⇑(preReflection x g)) Φ Φ
hx : x ≠ 0
u : M ≃ₗ[R] M := reflection hg₁ * reflection hf₁
hu : ↑u = LinearMap.id + LinearMap.smulRight (f - g) x
n : ℕ
ih : ↑(u ^ n) = LinearMap.id + ↑n • LinearMap.smulRight (f - g) x
⊢ ↑(u ^ (n + 1)) = LinearMap.id + ↑(n + 1) • LinearMap.smulRight (f - g) x

Tactic:
have : ((f - g).smulRight x).comp ((n : R) • (f - g).smulRight x) = 0 := by
  ext; simp [hf₁, hg₁]

Result:
case succ
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CharZero R
inst✝ : NoZeroSMulDivisors R M
x : M
Φ : Set M
hΦ₁ : Φ.Finite
hΦ₂ : span R Φ = ⊤
f g : Dual R M
hf₁ : f x = 2
hf₂ : MapsTo (⇑(preReflection x f)) Φ Φ
hg₁ : g x = 2
hg₂ : MapsTo (⇑(preReflection x g)) Φ Φ
hx : x ≠ 0
u : M ≃ₗ[R] M := reflection hg₁ * reflection hf₁
hu : ↑u = LinearMap.id + LinearMap.smulRight (f - g) x
n : ℕ
ih : ↑(u ^ n) = LinearMap.id + ↑n • LinearMap.smulRight (f - g) x
this : LinearMap.smulRight (f - g) x ∘ₗ (↑n • LinearMap.smulRight (f - g) x) = 0
⊢ ↑(u ^ (n + 1)) = LinearMap.id + ↑(n + 1) • LinearMap.smulRight (f - g) x