-- Mathlib/Analysis/InnerProductSpace/Projection.lean
theorem LinearIsometryEquiv.reflections_generate [FiniteDimensional ℝ F] :
    Subgroup.closure (Set.range fun v : F => reflection (ℝ ∙ v)ᗮ) = ⊤

Proof state:
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : FiniteDimensional ℝ F
⊢ Subgroup.closure (Set.range fun v => reflection (Submodule.span ℝ {v})ᗮ) = ⊤

Tactic:
rw [Subgroup.eq_top_iff']

Result:
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : FiniteDimensional ℝ F
⊢ ∀ (x : F ≃ₗᵢ[ℝ] F), x ∈ Subgroup.closure (Set.range fun v => reflection (Submodule.span ℝ {v})ᗮ)

Proof state:
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : FiniteDimensional ℝ F
φ : F ≃ₗᵢ[ℝ] F
⊢ φ ∈ Subgroup.closure (Set.range fun v => reflection (Submodule.span ℝ {v})ᗮ)

Tactic:
rcases φ.reflections_generate_dim with ⟨l, _, rfl⟩

Result:
case intro.intro
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : FiniteDimensional ℝ F
l : List F
left✝ : l.length ≤ finrank ℝ F
⊢ (List.map (fun v => reflection (Submodule.span ℝ {v})ᗮ) l).prod ∈
    Subgroup.closure (Set.range fun v => reflection (Submodule.span ℝ {v})ᗮ)

Proof state:
case intro.intro
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : FiniteDimensional ℝ F
l : List F
left✝ : l.length ≤ finrank ℝ F
⊢ (List.map (fun v => reflection (Submodule.span ℝ {v})ᗮ) l).prod ∈
    Subgroup.closure (Set.range fun v => reflection (Submodule.span ℝ {v})ᗮ)

Tactic:
apply (Subgroup.closure _).list_prod_mem

Result:
case intro.intro
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : FiniteDimensional ℝ F
l : List F
left✝ : l.length ≤ finrank ℝ F
⊢ ∀ x ∈ List.map (fun v => reflection (Submodule.span ℝ {v})ᗮ) l,
    x ∈ Subgroup.closure (Set.range fun v => reflection (Submodule.span ℝ {v})ᗮ)

Proof state:
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : FiniteDimensional ℝ F
⊢ ∀ (x : F ≃ₗᵢ[ℝ] F), x ∈ Subgroup.closure (Set.range fun v => reflection (Submodule.span ℝ {v})ᗮ)

Tactic:
intro φ

Result:
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : FiniteDimensional ℝ F
φ : F ≃ₗᵢ[ℝ] F
⊢ φ ∈ Subgroup.closure (Set.range fun v => reflection (Submodule.span ℝ {v})ᗮ)

Proof state:
case intro.intro.intro.intro
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : FiniteDimensional ℝ F
l : List F
left✝¹ : l.length ≤ finrank ℝ F
x : F ≃ₗᵢ[ℝ] F
hx : x ∈ List.map (fun v => reflection (Submodule.span ℝ {v})ᗮ) l
a : F
left✝ : a ∈ l
hax : reflection (Submodule.span ℝ {a})ᗮ = x
⊢ x ∈ Subgroup.closure (Set.range fun v => reflection (Submodule.span ℝ {v})ᗮ)

Tactic:
exact Subgroup.subset_closure ⟨a, hax⟩

Result:
no goals

Proof state:
case intro.intro
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : FiniteDimensional ℝ F
l : List F
left✝ : l.length ≤ finrank ℝ F
⊢ ∀ x ∈ List.map (fun v => reflection (Submodule.span ℝ {v})ᗮ) l,
    x ∈ Subgroup.closure (Set.range fun v => reflection (Submodule.span ℝ {v})ᗮ)

Tactic:
intro x hx

Result:
case intro.intro
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : FiniteDimensional ℝ F
l : List F
left✝ : l.length ≤ finrank ℝ F
x : F ≃ₗᵢ[ℝ] F
hx : x ∈ List.map (fun v => reflection (Submodule.span ℝ {v})ᗮ) l
⊢ x ∈ Subgroup.closure (Set.range fun v => reflection (Submodule.span ℝ {v})ᗮ)

Proof state:
case intro.intro
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : FiniteDimensional ℝ F
l : List F
left✝ : l.length ≤ finrank ℝ F
x : F ≃ₗᵢ[ℝ] F
hx : x ∈ List.map (fun v => reflection (Submodule.span ℝ {v})ᗮ) l
⊢ x ∈ Subgroup.closure (Set.range fun v => reflection (Submodule.span ℝ {v})ᗮ)

Tactic:
rcases List.mem_map.mp hx with ⟨a, _, hax⟩

Result:
case intro.intro.intro.intro
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : FiniteDimensional ℝ F
l : List F
left✝¹ : l.length ≤ finrank ℝ F
x : F ≃ₗᵢ[ℝ] F
hx : x ∈ List.map (fun v => reflection (Submodule.span ℝ {v})ᗮ) l
a : F
left✝ : a ∈ l
hax : reflection (Submodule.span ℝ {a})ᗮ = x
⊢ x ∈ Subgroup.closure (Set.range fun v => reflection (Submodule.span ℝ {v})ᗮ)