File tree Expand file tree Collapse file tree
Expand file tree Collapse file tree Original file line number Diff line number Diff line change @@ -24,6 +24,7 @@ We add some local simp lemmas so we can unfold the definitions of the normalizat
2424attribute [local simp] normalized hasNestedIf hasConstantIf hasRedundantIf disjoint vars
2525 List.disjoint
2626
27+ set_option warning.simp.varHead false in
2728attribute [local simp] apply_ite ite_eq_iff'
2829
2930variable {b : Bool} {f : ℕ → Bool} {i : ℕ} {t e : IfExpr}
Original file line number Diff line number Diff line change @@ -55,6 +55,7 @@ lemma Aquaesulian.injective : Function.Injective f := by
5555 · exact (h.eq_of_apply_eq_inl he.symm hc).symm
5656 · exact h.eq_of_apply_eq_inl he hc
5757
58+ set_option warning.simp.varHead false in
5859@[simp]
5960lemma Aquaesulian.apply_zero : f 0 = 0 := by
6061 refine h.injective ?_
@@ -68,6 +69,7 @@ lemma Aquaesulian.apply_neg_apply_add (x : G) : f (-(f x)) + x = 0 := by
6869 · rw [add_neg_cancel, h.apply_zero] at hc
6970 exact hc.symm
7071
72+ set_option warning.simp.varHead false in
7173@[simp]
7274lemma Aquaesulian.apply_neg_apply (x : G) : f (-(f x)) = -x := by
7375 rw [← add_eq_zero_iff_eq_neg]
You can’t perform that action at this time.
0 commit comments