Commit 2025-06-11 22:43 57471d1b

View on Github →

feat: a grw tactic for rewriting using inequalities (#8167)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Finset/Empty.lean

modified theorem Finset.Nonempty.mono

Modified Mathlib/Data/Fintype/Sets.lean

Modified Mathlib/Data/Set/Basic.lean

modified theorem Set.Nonempty.mono

modified theorem Set.mem_of_subset_of_mem

Modified Mathlib/MeasureTheory/Integral/Layercake.lean

Modified Mathlib/MeasureTheory/Integral/Lebesgue/Markov.lean

Modified Mathlib/Order/Bounds/Basic.lean

modified theorem BddAbove.mono

modified theorem BddBelow.mono

Modified Mathlib/Order/Disjoint.lean

modified theorem Codisjoint.mono

modified theorem Codisjoint.mono_left

modified theorem Codisjoint.mono_right

modified theorem Disjoint.mono

modified theorem Disjoint.mono_left

modified theorem Disjoint.mono_right

Modified Mathlib/Tactic.lean

Modified Mathlib/Tactic/GCongr.lean

added theorem Mathlib.Tactic.GCongr.gt_imp_gt

added theorem Mathlib.Tactic.GCongr.gt_imp_gt_left

added theorem Mathlib.Tactic.GCongr.gt_imp_gt_right

modified theorem Mathlib.Tactic.GCongr.le_imp_le

modified theorem Mathlib.Tactic.GCongr.lt_imp_lt

added theorem Mathlib.Tactic.GCongr.ssubset_imp_ssubset

added theorem Mathlib.Tactic.GCongr.ssubset_imp_ssubset_right

added theorem Mathlib.Tactic.GCongr.ssuperset_imp_ssuperset

added theorem Mathlib.Tactic.GCongr.ssuperset_imp_ssuperset_left

added theorem Mathlib.Tactic.GCongr.ssuperset_imp_ssuperset_right

Modified Mathlib/Tactic/GCongr/Core.lean

Created Mathlib/Tactic/GRewrite.lean

Created Mathlib/Tactic/GRewrite/Core.lean

added def Lean.MVarId.grewrite

added structure Mathlib.Tactic.GRewrite.Config

added def Mathlib.Tactic.GRewrite.dischargeMain

added structure Mathlib.Tactic.GRewriteResult

Created Mathlib/Tactic/GRewrite/Elab.lean

added def Mathlib.Tactic.evalGRewriteSeq

added def Mathlib.Tactic.grewriteLocalDecl

added def Mathlib.Tactic.grewriteTarget

Modified Mathlib/Tactic/NthRewrite.lean

deleted def Mathlib.Tactic.evalNthRewriteSeq

Created MathlibTest/GRewrite.lean