Commit 2025-01-24 20:24 a02db214

View on Github →

chore: simplify some proofs with rfl and tauto (#20985) Those simplifications were found by tryAtEachStep.

Estimated changes

Modified Mathlib/Algebra/Algebra/Quasispectrum.lean

Modified Mathlib/Analysis/NormedSpace/PiTensorProduct/ProjectiveSeminorm.lean

Modified Mathlib/CategoryTheory/Triangulated/Opposite/Basic.lean

Modified Mathlib/Combinatorics/SimpleGraph/Walk.lean

modified theorem SimpleGraph.Walk.getVert_copy

Modified Mathlib/LinearAlgebra/SesquilinearForm.lean

Modified Mathlib/NumberTheory/ModularForms/CongruenceSubgroups.lean

modified theorem CongruenceSubgroup.Gamma_zero_bot

Modified Mathlib/Topology/Gluing.lean