[Merged by Bors] - chore: remove nonterminal simp by BoltonBailey · Pull Request #7580 · leanprover-community/mathlib4

BoltonBailey · 2023-10-09T02:53:32Z

Removes nonterminal simps on lines looking like simp [...]

depends on: Incorrect simp tracing for local right-to-left simp theorems ([<- x]) leanprover/lean4#2131

…lib4 into BoltonBailey/nonterminal-simp-w-brackets-removal-squad

BoltonBailey · 2023-10-10T03:34:08Z

Lean 4 issue 2131 seems like it would make this easier, since I am currently trying to fix these by hand.

Mathlib/Tactic/NormNum/Basic.lean

…lib4 into BoltonBailey/nonterminal-simp-w-brackets-removal-squad

ghost · 2023-10-15T01:26:48Z

This PR/issue depends on:

~~Incorrect simp tracing for local right-to-left simp theorems ([<- x]) leanprover/lean4#2131~~
By Dependent Issues (🤖). Happy coding!

Mathlib/Algebra/ContinuedFractions/Computation/Translations.lean

Mathlib/AlgebraicTopology/SimplexCategory.lean

Mathlib/Analysis/Normed/Order/UpperLower.lean

Mathlib/Analysis/NormedSpace/Pointwise.lean

Mathlib/GroupTheory/Perm/Cycle/Concrete.lean

Mathlib/GroupTheory/Perm/Option.lean

Mathlib/MeasureTheory/Measure/FiniteMeasure.lean

Mathlib/Topology/Algebra/InfiniteSum/Basic.lean

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>

Mathlib/Algebra/ContinuedFractions/Computation/Translations.lean

Mathlib/AlgebraicTopology/SimplexCategory.lean

Mathlib/Analysis/Normed/Order/UpperLower.lean

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>

Mathlib/AlgebraicTopology/SimplexCategory.lean

Mathlib/Analysis/Normed/Order/UpperLower.lean

Mathlib/Analysis/NormedSpace/Pointwise.lean

Mathlib/Combinatorics/SimpleGraph/Connectivity.lean

github-actions · 2023-10-15T08:15:59Z

Mathlib/Algebra/ContinuedFractions/Computation/Translations.lean

  have : IntFractPair.stream v (n + 1) = some (IntFractPair.of ifp_n.fr⁻¹) := by
    cases ifp_n
-    simp [IntFractPair.stream, stream_nth_eq, nth_fr_ne_zero]
+    simp only [IntFractPair.stream, Nat.add_eq, add_zero, stream_nth_eq, Option.some_bind,             ite_eq_right_iff]


[lint-style] _{reported by reviewdog 🐶}

Suggested change

simp only [IntFractPair.stream, Nat.add_eq, add_zero, stream_nth_eq, Option.some_bind, ite_eq_right_iff]

simp only [IntFractPair.stream, Nat.add_eq, add_zero, stream_nth_eq, Option.some_bind, ite_eq_right_iff]

github-actions · 2023-10-15T08:19:24Z

Mathlib/Algebra/ContinuedFractions/Computation/Translations.lean

  have : IntFractPair.stream v (n + 1) = some (IntFractPair.of ifp_n.fr⁻¹) := by
    cases ifp_n
-    simp [IntFractPair.stream, stream_nth_eq, nth_fr_ne_zero]
+    simp only [IntFractPair.stream, Nat.add_eq, add_zero, stream_nth_eq, Option.some_bind,             ite_eq_right_iff]


[lint-style] _{reported by reviewdog 🐶}

Suggested change

simp only [IntFractPair.stream, Nat.add_eq, add_zero, stream_nth_eq, Option.some_bind, ite_eq_right_iff]

simp only [IntFractPair.stream, Nat.add_eq, add_zero, stream_nth_eq, Option.some_bind,

ite_eq_right_iff]

github-actions · 2023-10-15T08:19:24Z

Mathlib/AlgebraicTopology/SimplexCategory.lean

  simp at hj
  dsimp [σ, δ, Fin.predAbove, Fin.succAbove]
-  simp [Fin.lt_iff_val_lt_val, Fin.ite_val, Fin.dite_val]
+  simp only [Fin.lt_iff_val_lt_val, Fin.dite_val, Fin.ite_val, Fin.coe_pred, ge_iff_le,     Fin.coe_castLT, dite_eq_ite]


[lint-style] _{reported by reviewdog 🐶}

Suggested change

simp only [Fin.lt_iff_val_lt_val, Fin.dite_val, Fin.ite_val, Fin.coe_pred, ge_iff_le, Fin.coe_castLT, dite_eq_ite]

simp only [Fin.lt_iff_val_lt_val, Fin.dite_val, Fin.ite_val, Fin.coe_pred, ge_iff_le,

Fin.coe_castLT, dite_eq_ite]

github-actions · 2023-10-15T08:19:24Z

Mathlib/AlgebraicTopology/SimplexCategory.lean

  simp at H hk
  dsimp [σ, Fin.predAbove]
-  simp [Fin.lt_iff_val_lt_val, Fin.ite_val]
+  simp only [Fin.lt_iff_val_lt_val, Fin.ite_val, Fin.coe_pred, ge_iff_le, dite_eq_ite,     Fin.coe_castLT]


[lint-style] _{reported by reviewdog 🐶}

Suggested change

simp only [Fin.lt_iff_val_lt_val, Fin.ite_val, Fin.coe_pred, ge_iff_le, dite_eq_ite, Fin.coe_castLT]

simp only [Fin.lt_iff_val_lt_val, Fin.ite_val, Fin.coe_pred, ge_iff_le, dite_eq_ite,

Fin.coe_castLT]

github-actions · 2023-10-15T08:19:24Z

Mathlib/Analysis/Normed/Order/UpperLower.lean

  · rw [dist_self_sub_left]
    refine' (add_le_add_left (pi_norm_const_le <| 3 / 4 * δ) _).trans_eq _
-    simp [abs_of_pos, abs_of_pos hδ]
+    simp only [norm_mul, norm_div, Real.norm_eq_abs, gt_iff_lt, zero_lt_three, abs_of_pos,       zero_lt_four, abs_of_pos hδ]


[lint-style] _{reported by reviewdog 🐶}

Suggested change

simp only [norm_mul, norm_div, Real.norm_eq_abs, gt_iff_lt, zero_lt_three, abs_of_pos, zero_lt_four, abs_of_pos hδ]

simp only [norm_mul, norm_div, Real.norm_eq_abs, gt_iff_lt, zero_lt_three, abs_of_pos,

zero_lt_four, abs_of_pos hδ]

github-actions · 2023-10-15T08:19:24Z

Mathlib/Analysis/NormedSpace/Pointwise.lean

    ⟨r • ‖y - x‖⁻¹ • (y - x) + x, _⟩⟩
  have : ‖y - x‖ ≠ 0 := by simpa [sub_eq_zero]
-  simp [norm_smul, this, Real.norm_of_nonneg hr]
+  simp only [mem_sphere_iff_norm, add_sub_cancel, norm_smul, Real.norm_eq_abs, norm_inv, norm_norm,     ne_eq, norm_eq_zero]


[lint-style] _{reported by reviewdog 🐶}

Suggested change

simp only [mem_sphere_iff_norm, add_sub_cancel, norm_smul, Real.norm_eq_abs, norm_inv, norm_norm, ne_eq, norm_eq_zero]

simp only [mem_sphere_iff_norm, add_sub_cancel, norm_smul, Real.norm_eq_abs, norm_inv, norm_norm,

ne_eq, norm_eq_zero]

github-actions · 2023-10-15T08:19:26Z

Mathlib/GroupTheory/Perm/Cycle/Concrete.lean

  rw [toList, hc.cycleOf_eq (mem_support.mp _), hs, card_toFinset, dedup_eq_self.mpr hn]
  · refine' ext_get (by simp) fun k hk hk' => _
-    simp [formPerm_pow_apply_nthLe _ hn, Nat.mod_eq_of_lt hk']
+    simp only [Nat.zero_eq, get_map, get_range, formPerm_pow_apply_nthLe _ hn, zero_add,       Nat.mod_eq_of_lt hk']


[lint-style] _{reported by reviewdog 🐶}

Suggested change

simp only [Nat.zero_eq, get_map, get_range, formPerm_pow_apply_nthLe _ hn, zero_add, Nat.mod_eq_of_lt hk']

simp only [Nat.zero_eq, get_map, get_range, formPerm_pow_apply_nthLe _ hn, zero_add,

Nat.mod_eq_of_lt hk']

Mathlib/GroupTheory/Perm/Option.lean

github-actions · 2023-10-15T08:19:27Z

Mathlib/MeasureTheory/Measure/FiniteMeasure.lean

 theorem coeFn_add (μ ν : FiniteMeasure Ω) : (⇑(μ + ν) : Set Ω → ℝ≥0) = (⇑μ + ⇑ν : Set Ω → ℝ≥0) := by
  funext
-  simp [← ENNReal.coe_eq_coe]
+  simp only [Pi.add_apply, ← ENNReal.coe_eq_coe, ne_eq, ennreal_coeFn_eq_coeFn_toMeasure, ENNReal.coe_add]


[lint-style] _{reported by reviewdog 🐶}

Suggested change

simp only [Pi.add_apply, ← ENNReal.coe_eq_coe, ne_eq, ennreal_coeFn_eq_coeFn_toMeasure, ENNReal.coe_add]

simp only [Pi.add_apply, ← ENNReal.coe_eq_coe, ne_eq, ennreal_coeFn_eq_coeFn_toMeasure,

ENNReal.coe_add]

github-actions · 2023-10-15T08:19:27Z

Mathlib/MeasureTheory/Measure/FiniteMeasure.lean

    (⇑(c • μ) : Set Ω → ℝ≥0) = c • (⇑μ : Set Ω → ℝ≥0) := by
  funext
-  simp [← ENNReal.coe_eq_coe, ENNReal.coe_smul]
+  simp only [Pi.smul_apply, ← ENNReal.coe_eq_coe, ne_eq, ennreal_coeFn_eq_coeFn_toMeasure, ENNReal.coe_smul]


[lint-style] _{reported by reviewdog 🐶}

Suggested change

simp only [Pi.smul_apply, ← ENNReal.coe_eq_coe, ne_eq, ennreal_coeFn_eq_coeFn_toMeasure, ENNReal.coe_smul]

simp only [Pi.smul_apply, ← ENNReal.coe_eq_coe, ne_eq, ennreal_coeFn_eq_coeFn_toMeasure,

ENNReal.coe_smul]

Mathlib/Topology/Algebra/InfiniteSum/Basic.lean

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>

…lib4 into BoltonBailey/nonterminal-simp-w-brackets-removal-squad

Mathlib/Tactic/NormNum/Basic.lean

Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

adomani · 2023-10-18T12:29:27Z

LGTM! I am sorry to have caused so much pain, but I think that this is a strong improvement!

I agree with the comment that ideally the linter should be implemented in lean directly, but currently, this is what is available!

Thanks!

BoltonBailey · 2023-10-18T13:01:50Z

LGTM! I am sorry to have caused so much pain, but I think that this is a strong improvement!

I agree with the comment that ideally the linter should be implemented in lean directly, but currently, this is what is available!

Thanks!

What doesn't kill you makes you stronger!

joelriou · 2023-10-19T17:06:47Z

Thanks!

bors merge

Removes nonterminal simps on lines looking like `simp [...]`

bors · 2023-10-19T18:23:38Z

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

BoltonBailey added 6 commits October 8, 2023 21:52

add ?

d05e9cd

try this

f943995

fix more ?

fa037e4

Merge branch 'master' of https://github.com/leanprover-community/math…

74dfdb1

…lib4 into BoltonBailey/nonterminal-simp-w-brackets-removal-squad

fix

212ca94

eliminate more ?

d6b008b

BoltonBailey mentioned this pull request Oct 10, 2023

[Merged by Bors] - style: add nonterminal simp checker #7496

Closed

3 tasks

more ?

f1eeab4

github-actions bot reviewed Oct 10, 2023

View reviewed changes

Mathlib/Tactic/NormNum/Basic.lean Outdated Show resolved Hide resolved

Mathlib/Tactic/NormNum/Basic.lean Outdated Show resolved Hide resolved

more ?

71e880b

ghost added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Oct 10, 2023

BoltonBailey added 4 commits October 12, 2023 15:48

fix ?

d9221e6

Merge branch 'master' of https://github.com/leanprover-community/math…

415bee2

…lib4 into BoltonBailey/nonterminal-simp-w-brackets-removal-squad

add lemmas

a46ee90

remove ?

53cb804

ghost removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Oct 15, 2023

BoltonBailey added 3 commits October 15, 2023 00:46

remove ?

2242a51

add a line splitter

ecda23d

bugfix

bf767f8

github-actions bot reviewed Oct 15, 2023

View reviewed changes

BoltonBailey and others added 4 commits October 15, 2023 03:12

Update Mathlib/Algebra/ContinuedFractions/Computation/Translations.lean

540ec35

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>

Update Mathlib/AlgebraicTopology/SimplexCategory.lean

6d6d311

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>

Update Mathlib/AlgebraicTopology/SimplexCategory.lean

1b5a4cb

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>

Update Mathlib/Analysis/Normed/Order/UpperLower.lean

23b9582

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>

github-actions bot reviewed Oct 15, 2023

View reviewed changes

BoltonBailey and others added 2 commits October 15, 2023 03:13

Update Mathlib/Analysis/NormedSpace/Pointwise.lean

0d483e2

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>

Update Mathlib/Combinatorics/SimpleGraph/Connectivity.lean

f07d9c0

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>

github-actions bot reviewed Oct 15, 2023

View reviewed changes

add newlines

c559f27

github-actions bot reviewed Oct 15, 2023

View reviewed changes

BoltonBailey and others added 7 commits October 15, 2023 03:25

Update Mathlib/Topology/Algebra/InfiniteSum/Basic.lean

2d75452

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>

Update Mathlib/GroupTheory/Perm/Option.lean

73290e8

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>

fix lines

bb12278

reformat lemma lists

fc4b77d

reformat lemma lists

985eb28

reformat lemma lists

66a7dae

revert style

587f55f

BoltonBailey added the awaiting-review label Oct 16, 2023

BoltonBailey added 2 commits October 16, 2023 02:02

remove unneeded lemmas

a269a6e

rewrite statement

474b21c

ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 17, 2023

Merge branch 'master' of https://github.com/leanprover-community/math…

b820b5a

…lib4 into BoltonBailey/nonterminal-simp-w-brackets-removal-squad

ghost removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 18, 2023

BoltonBailey added 2 commits October 17, 2023 23:37

correct arrow

54e4e1c

len/card

70c7c6e

joelriou reviewed Oct 18, 2023

View reviewed changes

Mathlib/Tactic/NormNum/Basic.lean Outdated Show resolved Hide resolved

Update Mathlib/Tactic/NormNum/Basic.lean

659f147

Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Oct 19, 2023

bors bot pushed a commit that referenced this pull request Oct 19, 2023

chore: remove nonterminal simp (#7580)

6fc8e6e

Removes nonterminal simps on lines looking like `simp [...]`

bors bot changed the title ~~chore: remove nonterminal simp~~ [Merged by Bors] - chore: remove nonterminal simp Oct 19, 2023

bors bot closed this Oct 19, 2023

bors bot deleted the BoltonBailey/nonterminal-simp-w-brackets-removal-squad branch October 19, 2023 18:23

	simp only [IntFractPair.stream, Nat.add_eq, add_zero, stream_nth_eq, Option.some_bind, ite_eq_right_iff]
	simp only [IntFractPair.stream, Nat.add_eq, add_zero, stream_nth_eq, Option.some_bind, ite_eq_right_iff]

	simp only [IntFractPair.stream, Nat.add_eq, add_zero, stream_nth_eq, Option.some_bind, ite_eq_right_iff]
	simp only [IntFractPair.stream, Nat.add_eq, add_zero, stream_nth_eq, Option.some_bind,
	ite_eq_right_iff]

	simp only [Fin.lt_iff_val_lt_val, Fin.dite_val, Fin.ite_val, Fin.coe_pred, ge_iff_le, Fin.coe_castLT, dite_eq_ite]
	simp only [Fin.lt_iff_val_lt_val, Fin.dite_val, Fin.ite_val, Fin.coe_pred, ge_iff_le,
	Fin.coe_castLT, dite_eq_ite]

	simp only [Fin.lt_iff_val_lt_val, Fin.ite_val, Fin.coe_pred, ge_iff_le, dite_eq_ite, Fin.coe_castLT]
	simp only [Fin.lt_iff_val_lt_val, Fin.ite_val, Fin.coe_pred, ge_iff_le, dite_eq_ite,
	Fin.coe_castLT]

	simp only [norm_mul, norm_div, Real.norm_eq_abs, gt_iff_lt, zero_lt_three, abs_of_pos, zero_lt_four, abs_of_pos hδ]
	simp only [norm_mul, norm_div, Real.norm_eq_abs, gt_iff_lt, zero_lt_three, abs_of_pos,
	zero_lt_four, abs_of_pos hδ]

	simp only [mem_sphere_iff_norm, add_sub_cancel, norm_smul, Real.norm_eq_abs, norm_inv, norm_norm, ne_eq, norm_eq_zero]
	simp only [mem_sphere_iff_norm, add_sub_cancel, norm_smul, Real.norm_eq_abs, norm_inv, norm_norm,
	ne_eq, norm_eq_zero]

	simp only [Nat.zero_eq, get_map, get_range, formPerm_pow_apply_nthLe _ hn, zero_add, Nat.mod_eq_of_lt hk']
	simp only [Nat.zero_eq, get_map, get_range, formPerm_pow_apply_nthLe _ hn, zero_add,
	Nat.mod_eq_of_lt hk']

	simp only [Pi.add_apply, ← ENNReal.coe_eq_coe, ne_eq, ennreal_coeFn_eq_coeFn_toMeasure, ENNReal.coe_add]
	simp only [Pi.add_apply, ← ENNReal.coe_eq_coe, ne_eq, ennreal_coeFn_eq_coeFn_toMeasure,
	ENNReal.coe_add]

	simp only [Pi.smul_apply, ← ENNReal.coe_eq_coe, ne_eq, ennreal_coeFn_eq_coeFn_toMeasure, ENNReal.coe_smul]
	simp only [Pi.smul_apply, ← ENNReal.coe_eq_coe, ne_eq, ennreal_coeFn_eq_coeFn_toMeasure,
	ENNReal.coe_smul]

Conversation

BoltonBailey commented Oct 9, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

BoltonBailey commented Oct 10, 2023

Uh oh!

Uh oh!

Uh oh!

ghost commented Oct 15, 2023

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

github-actions bot Oct 15, 2023

Choose a reason for hiding this comment

Uh oh!

github-actions bot Oct 15, 2023

Choose a reason for hiding this comment

Uh oh!

github-actions bot Oct 15, 2023

Choose a reason for hiding this comment

Uh oh!

github-actions bot Oct 15, 2023

Choose a reason for hiding this comment

Uh oh!

github-actions bot Oct 15, 2023

Choose a reason for hiding this comment

Uh oh!

github-actions bot Oct 15, 2023

Choose a reason for hiding this comment

Uh oh!

github-actions bot Oct 15, 2023

Choose a reason for hiding this comment

Uh oh!

Uh oh!

github-actions bot Oct 15, 2023

Choose a reason for hiding this comment

Uh oh!

github-actions bot Oct 15, 2023

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

adomani commented Oct 18, 2023

Uh oh!

BoltonBailey commented Oct 18, 2023

Uh oh!

joelriou commented Oct 19, 2023

Uh oh!

bors bot commented Oct 19, 2023

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

BoltonBailey commented Oct 9, 2023 •

edited

Loading