-- Mathlib/LinearAlgebra/Reflection.lean
/-- This rather technical-looking lemma exists because it is exactly what is needed to establish a
uniqueness result for root data. See the doc string of `Module.Dual.eq_of_preReflection_mapsTo` for
further remarks. -/
lemma Dual.eq_of_preReflection_mapsTo' [CharZero R] [NoZeroSMulDivisors R M]
    {x : M} {Φ : Set M} (hΦ₁ : Φ.Finite) (hx : x ∈ 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) Φ Φ) :
    (span R Φ).subtype.dualMap f = (span R Φ).subtype.dualMap 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 ↑Φ
hx : x ∈ 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)) Φ Φ
Φ' : Set ↥(span R Φ) := range (inclusion ⋯)
hΦ'₁ : Φ'.Finite
hΦ'₂ : span R Φ' = ⊤
x' : ↥(span R Φ) := ⟨x, hx⟩
⊢ (span R Φ).subtype.dualMap f = (span R Φ).subtype.dualMap g

Tactic:
have this : ∀ {F : Dual R M}, MapsTo (preReflection x F) Φ Φ →
    MapsTo (preReflection x' ((span R Φ).subtype.dualMap F)) Φ' Φ' := by
  intro F hF ⟨y, hy⟩ hy'
  simp only [Φ'] at hy' ⊢
  rw [range_inclusion] at hy'
  simp only [SetLike.coe_sort_coe, mem_setOf_eq] at hy' ⊢
  rw [range_inclusion]
  exact hF hy'

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 ↑Φ
hx : x ∈ 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)) Φ Φ
Φ' : Set ↥(span R Φ) := range (inclusion ⋯)
hΦ'₁ : Φ'.Finite
hΦ'₂ : span R Φ' = ⊤
x' : ↥(span R Φ) := ⟨x, hx⟩
this :
  ∀ {F : Dual R M},
    MapsTo (⇑(preReflection x F)) Φ Φ → MapsTo (⇑(preReflection x' ((span R Φ).subtype.dualMap F))) Φ' Φ'
⊢ (span R Φ).subtype.dualMap f = (span R Φ).subtype.dualMap 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
hx : x ∈ 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)) Φ Φ
Φ' : Set ↥(span R Φ) := range (inclusion ⋯)
⊢ (span R Φ).subtype.dualMap f = (span R Φ).subtype.dualMap g

Tactic:
rw [← finite_coe_iff] at hΦ₁

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 ↑Φ
hx : x ∈ 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)) Φ Φ
Φ' : Set ↥(span R Φ) := range (inclusion ⋯)
⊢ (span R Φ).subtype.dualMap f = (span R Φ).subtype.dualMap 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 ↑Φ
hx : x ∈ 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)) Φ Φ
Φ' : Set ↥(span R Φ) := range (inclusion ⋯)
hΦ'₁ : Φ'.Finite
hΦ'₂ : span R Φ' = ⊤
x' : ↥(span R Φ) := ⟨x, hx⟩
F : Dual R M
hF : MapsTo (⇑(preReflection x F)) Φ Φ
y : M
hy : y ∈ span R Φ
hy' : ⟨y, hy⟩ ∈ range (inclusion ⋯)
⊢ (preReflection x' ((span R Φ).subtype.dualMap F)) ⟨y, hy⟩ ∈ range (inclusion ⋯)

Tactic:
rw [range_inclusion] at hy'

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 ↑Φ
hx : x ∈ 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)) Φ Φ
Φ' : Set ↥(span R Φ) := range (inclusion ⋯)
hΦ'₁ : Φ'.Finite
hΦ'₂ : span R Φ' = ⊤
x' : ↥(span R Φ) := ⟨x, hx⟩
F : Dual R M
hF : MapsTo (⇑(preReflection x F)) Φ Φ
y : M
hy : y ∈ span R Φ
hy' : ⟨y, hy⟩ ∈ {x | ↑x ∈ Φ}
⊢ (preReflection x' ((span R Φ).subtype.dualMap F)) ⟨y, hy⟩ ∈ range (inclusion ⋯)

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
hx : x ∈ 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)) Φ Φ
⊢ (span R Φ).subtype.dualMap f = (span R Φ).subtype.dualMap g

Tactic:
set Φ' : Set (span R Φ) := range (inclusion <| Submodule.subset_span (R := R) (s := Φ))

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
hx : x ∈ 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)) Φ Φ
Φ' : Set ↥(span R Φ) := range (inclusion ⋯)
⊢ (span R Φ).subtype.dualMap f = (span R Φ).subtype.dualMap 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 ↑Φ
hx : x ∈ 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)) Φ Φ
Φ' : Set ↥(span R Φ) := range (inclusion ⋯)
hΦ'₁ : Φ'.Finite
hΦ'₂ : span R Φ' = ⊤
x' : ↥(span R Φ) := ⟨x, hx⟩
F : Dual R M
hF : MapsTo (⇑(preReflection x F)) Φ Φ
y : M
hy : y ∈ span R Φ
hy' : ⟨y, hy⟩ ∈ Φ'
⊢ (preReflection x' ((span R Φ).subtype.dualMap F)) ⟨y, hy⟩ ∈ Φ'

Tactic:
simp only [Φ'] at hy' ⊢

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 ↑Φ
hx : x ∈ 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)) Φ Φ
Φ' : Set ↥(span R Φ) := range (inclusion ⋯)
hΦ'₁ : Φ'.Finite
hΦ'₂ : span R Φ' = ⊤
x' : ↥(span R Φ) := ⟨x, hx⟩
F : Dual R M
hF : MapsTo (⇑(preReflection x F)) Φ Φ
y : M
hy : y ∈ span R Φ
hy' : ⟨y, hy⟩ ∈ range (inclusion ⋯)
⊢ (preReflection x' ((span R Φ).subtype.dualMap F)) ⟨y, hy⟩ ∈ range (inclusion ⋯)

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 ↑Φ
hx : x ∈ 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)) Φ Φ
Φ' : Set ↥(span R Φ) := range (inclusion ⋯)
hΦ'₁ : Φ'.Finite
hΦ'₂ : span R Φ' = ⊤
x' : ↥(span R Φ) := ⟨x, hx⟩
⊢ ∀ {F : Dual R M},
    MapsTo (⇑(preReflection x F)) Φ Φ → MapsTo (⇑(preReflection x' ((span R Φ).subtype.dualMap F))) Φ' Φ'

Tactic:
intro F hF ⟨y, hy⟩ hy'

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 ↑Φ
hx : x ∈ 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)) Φ Φ
Φ' : Set ↥(span R Φ) := range (inclusion ⋯)
hΦ'₁ : Φ'.Finite
hΦ'₂ : span R Φ' = ⊤
x' : ↥(span R Φ) := ⟨x, hx⟩
F : Dual R M
hF : MapsTo (⇑(preReflection x F)) Φ Φ
y : M
hy : y ∈ span R Φ
hy' : ⟨y, hy⟩ ∈ Φ'
⊢ (preReflection x' ((span R Φ).subtype.dualMap F)) ⟨y, hy⟩ ∈ Φ'