chore(*): make more transitive relations available to calc (#12860)

ericrbg · ericrbg · commit 6f9cb03e8a39 · 2022-04-11T02:03:03.000Z
Fixed as many possible declarations to have the correct argument order, as per [Zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/calc.20with.20.60.E2.89.83*.60). Golfed some random ones while I was at it.
diff --git a/src/algebra/divisibility.lean b/src/algebra/divisibility.lean
@@ -55,11 +55,8 @@ exists.elim H₁ H₂
 
 local attribute [simp] mul_assoc mul_comm mul_left_comm
 
-@[trans] theorem dvd_trans (h₁ : a ∣ b) (h₂ : b ∣ c) : a ∣ c :=
-match h₁, h₂ with
-| ⟨d, (h₃ : b = a * d)⟩, ⟨e, (h₄ : c = b * e)⟩ :=
-  ⟨d * e, show c = a * (d * e), by simp [h₃, h₄]⟩
-end
+@[trans] theorem dvd_trans : a ∣ b → b ∣ c → a ∣ c
+| ⟨d, h₁⟩ ⟨e, h₂⟩ := ⟨d * e, h₁ ▸ h₂.trans $ mul_assoc a d e⟩
 
 alias dvd_trans ← has_dvd.dvd.trans
 
diff --git a/src/analysis/asymptotics/asymptotic_equivalent.lean b/src/analysis/asymptotics/asymptotic_equivalent.lean
@@ -9,7 +9,7 @@ import analysis.normed_space.ordered
 /-!
 # Asymptotic equivalence
 
-In this file, we define the relation `is_equivalent u v l`, which means that `u-v` is little o of
+In this file, we define the relation `is_equivalent l u v`, which means that `u-v` is little o of
 `v` along the filter `l`.
 
 Unlike `is_[oO]` relations, this one requires `u` and `v` to have the same codomain `β`. While the
@@ -18,7 +18,7 @@ definition only requires `β` to be a `normed_group`, most interesting propertie
 
 ## Notations
 
-We introduce the notation `u ~[l] v := is_equivalent u v l`, which you can use by opening the
+We introduce the notation `u ~[l] v := is_equivalent l u v`, which you can use by opening the
 `asymptotics` locale.
 
 ## Main results
@@ -47,6 +47,11 @@ If `β` is a `normed_linear_ordered_field` :
 - If `u ~[l] v`, we have `tendsto u l at_top ↔ tendsto v l at_top`
   (see `is_equivalent.tendsto_at_top_iff`)
 
+## Implementation Notes
+
+Note that `is_equivalent` takes the parameters `(l : filter α) (u v : α → β)` in that order.
+This is to enable `calc` support, as `calc` requires that the last two explicit arguments are `u v`.
+
 -/
 
 namespace asymptotics
@@ -60,9 +65,9 @@ variables {α β : Type*} [normed_group β]
 
 /-- Two functions `u` and `v` are said to be asymptotically equivalent along a filter `l` when
     `u x - v x = o(v x)` as x converges along `l`. -/
-def is_equivalent (u v : α → β) (l : filter α) := is_o (u - v) v l
+def is_equivalent (l : filter α) (u v : α → β) := is_o (u - v) v l
 
-localized "notation u ` ~[`:50 l:50 `] `:0 v:50 := asymptotics.is_equivalent u v l" in asymptotics
+localized "notation u ` ~[`:50 l:50 `] `:0 v:50 := asymptotics.is_equivalent l u v" in asymptotics
 
 variables {u v w : α → β} {l : filter α}
 
@@ -87,7 +92,8 @@ end
 @[symm] lemma is_equivalent.symm (h : u ~[l] v) : v ~[l] u :=
 (h.is_o.trans_is_O h.is_O_symm).symm
 
-@[trans] lemma is_equivalent.trans (huv : u ~[l] v) (hvw : v ~[l] w) : u ~[l] w :=
+@[trans] lemma is_equivalent.trans {l : filter α} {u v w : α → β}
+  (huv : u ~[l] v) (hvw : v ~[l] w) : u ~[l] w :=
 (huv.is_o.trans_is_O hvw.is_O).triangle hvw.is_o
 
 lemma is_equivalent.congr_left {u v w : α → β} {l : filter α} (huv : u ~[l] v)
diff --git a/src/analysis/convex/extreme.lean b/src/analysis/convex/extreme.lean
@@ -71,8 +71,7 @@ is_extreme.refl 𝕜 A
 @[trans] protected lemma is_extreme.trans (hAB : is_extreme 𝕜 A B) (hBC : is_extreme 𝕜 B C) :
   is_extreme 𝕜 A C :=
 begin
-  use subset.trans hBC.1 hAB.1,
-  rintro x₁ hx₁A x₂ hx₂A x hxC hx,
+  refine ⟨subset.trans hBC.1 hAB.1, λ x₁ hx₁A x₂ hx₂A x hxC hx, _⟩,
   obtain ⟨hx₁B, hx₂B⟩ := hAB.2 x₁ hx₁A x₂ hx₂A x (hBC.1 hxC) hx,
   exact hBC.2 x₁ hx₁B x₂ hx₂B x hxC hx,
 end
diff --git a/src/analysis/special_functions/polynomials.lean b/src/analysis/special_functions/polynomials.lean
@@ -43,7 +43,7 @@ lemma is_equivalent_at_top_lead :
 begin
   by_cases h : P = 0,
   { simp [h] },
-  { conv_lhs
+  { conv_rhs
     { funext,
       rw [polynomial.eval_eq_sum_range, sum_range_succ] },
     exact is_equivalent.refl.add_is_o (is_o.sum $ λ i hi, is_o.const_mul_left
diff --git a/src/combinatorics/colex.lean b/src/combinatorics/colex.lean
@@ -131,24 +131,20 @@ instance [has_lt α] : is_irrefl (finset.colex α) (<) :=
 ⟨λ A h, exists.elim h (λ _ ⟨_,a,b⟩, a b)⟩
 
 @[trans]
-lemma lt_trans [linear_order α] {a b c : finset.colex α} :
-  a < b → b < c → a < c :=
+lemma lt_trans [linear_order α] {a b c : finset.colex α} : a < b → b < c → a < c :=
 begin
   rintros ⟨k₁, k₁z, notinA, inB⟩ ⟨k₂, k₂z, notinB, inC⟩,
   cases lt_or_gt_of_ne (ne_of_mem_of_not_mem inB notinB),
-  { refine ⟨k₂, _, by rwa k₁z h, inC⟩,
-    intros x hx,
+  { refine ⟨k₂, λ x hx, _, by rwa k₁z h, inC⟩,
     rw ← k₂z hx,
     apply k₁z (trans h hx) },
-  { refine ⟨k₁, _, notinA, by rwa ← k₂z h⟩,
-    intros x hx,
+  { refine ⟨k₁, λ x hx, _, notinA, by rwa ← k₂z h⟩,
     rw k₁z hx,
     apply k₂z (trans h hx) }
 end
 
 @[trans]
-lemma le_trans [linear_order α] (a b c : finset.colex α) :
-  a ≤ b → b ≤ c → a ≤ c :=
+lemma le_trans [linear_order α] (a b c : finset.colex α) : a ≤ b → b ≤ c → a ≤ c :=
 λ AB BC, AB.elim (λ k, BC.elim (λ t, or.inl (lt_trans k t)) (λ t, t ▸ AB)) (λ k, k.symm ▸ BC)
 
 instance [linear_order α] : is_trans (finset.colex α) (<) := ⟨λ _ _ _, colex.lt_trans⟩
diff --git a/src/computability/tm_computable.lean b/src/computability/tm_computable.lean
@@ -92,6 +92,9 @@ structure evals_to {σ : Type*} (f : σ → option σ) (a : σ) (b : option σ)
 (steps : ℕ)
 (evals_in_steps : ((flip bind f)^[steps] a) = b)
 
+-- note: this cannot currently be used in `calc`, as the last two arguments must be `a` and `b`.
+-- If this is desired, this argument order can be changed, but this spelling is I think the most
+-- natural, so there is a trade-off that needs to be made here. A notation can get around this.
 /-- A "proof" of the fact that `f` eventually reaches `b` in at most `m` steps when repeatedly
 evaluated on `a`, remembering the number of steps it takes. -/
 structure evals_to_in_time {σ : Type*} (f : σ → option σ) (a : σ) (b : option σ) (m : ℕ)
@@ -113,8 +116,8 @@ structure evals_to_in_time {σ : Type*} (f : σ → option σ) (a : σ) (b : opt
 ⟨evals_to.refl f a, le_refl 0⟩
 
 /-- Transitivity of `evals_to_in_time` in the sum of the numbers of steps. -/
-@[trans] def evals_to_in_time.trans {σ : Type*} (f : σ → option σ) (a : σ) (b : σ) (c : option σ)
-  (m₁ : ℕ) (m₂ : ℕ) (h₁ : evals_to_in_time f a b m₁) (h₂ : evals_to_in_time f b c m₂) :
+@[trans] def evals_to_in_time.trans {σ : Type*} (f : σ → option σ) (m₁ : ℕ) (m₂ : ℕ)
+  (a : σ) (b : σ) (c : option σ) (h₁ : evals_to_in_time f a b m₁) (h₂ : evals_to_in_time f b c m₂) :
   evals_to_in_time f a c (m₂ + m₁) :=
 ⟨evals_to.trans f a b c h₁.to_evals_to h₂.to_evals_to, add_le_add h₂.steps_le_m h₁.steps_le_m⟩
 
diff --git a/src/computability/turing_machine.lean b/src/computability/turing_machine.lean
@@ -71,7 +71,7 @@ def blank_extends {Γ} [inhabited Γ] (l₁ l₂ : list Γ) : Prop :=
 
 @[trans] theorem blank_extends.trans {Γ} [inhabited Γ] {l₁ l₂ l₃ : list Γ} :
   blank_extends l₁ l₂ → blank_extends l₂ l₃ → blank_extends l₁ l₃ :=
-by rintro ⟨i, rfl⟩ ⟨j, rfl⟩; exact ⟨i+j, by simp [list.repeat_add]⟩
+by { rintro ⟨i, rfl⟩ ⟨j, rfl⟩, exact ⟨i+j, by simp [list.repeat_add]⟩ }
 
 theorem blank_extends.below_of_le {Γ} [inhabited Γ] {l l₁ l₂ : list Γ} :
   blank_extends l l₁ → blank_extends l l₂ →
diff --git a/src/data/list/rotate.lean b/src/data/list/rotate.lean
@@ -368,14 +368,8 @@ lemma is_rotated_comm : l ~r l' ↔ l' ~r l :=
 @[simp] protected lemma is_rotated.forall (l : list α) (n : ℕ) : l.rotate n ~r l :=
 is_rotated.symm ⟨n, rfl⟩
 
-@[trans] lemma is_rotated.trans {l'' : list α} (h : l ~r l') (h' : l' ~r l'') :
-  l ~r l'' :=
-begin
-  obtain ⟨n, rfl⟩ := h,
-  obtain ⟨m, rfl⟩ := h',
-  rw rotate_rotate,
-  use (n + m)
-end
+@[trans] lemma is_rotated.trans : ∀ {l l' l'' : list α}, l ~r l' → l' ~r l'' → l ~r l''
+| _ _ _ ⟨n, rfl⟩ ⟨m, rfl⟩ := ⟨n + m, by rw [rotate_rotate]⟩
 
 lemma is_rotated.eqv : equivalence (@is_rotated α) :=
 mk_equivalence _ is_rotated.refl (λ _ _, is_rotated.symm) (λ _ _ _, is_rotated.trans)
diff --git a/src/data/set/basic.lean b/src/data/set/basic.lean
@@ -177,8 +177,7 @@ funext (assume x, propext (h x))
 theorem ext_iff {s t : set α} : s = t ↔ ∀ x, x ∈ s ↔ x ∈ t :=
 ⟨λ h x, by rw h, ext⟩
 
-@[trans] theorem mem_of_mem_of_subset {x : α} {s t : set α}
-  (hx : x ∈ s) (h : s ⊆ t) : x ∈ t := h hx
+@[trans] theorem mem_of_mem_of_subset {x : α} {s t : set α} (hx : x ∈ s) (h : s ⊆ t) : x ∈ t := h hx
 
 lemma forall_in_swap {p : α → β → Prop} :
   (∀ (a ∈ s) b, p a b) ↔ ∀ b (a ∈ s), p a b :=
@@ -228,8 +227,7 @@ lemma ssubset_def : s ⊂ t = (s ⊆ t ∧ ¬ t ⊆ s) := rfl
 @[refl] theorem subset.refl (a : set α) : a ⊆ a := assume x, id
 theorem subset.rfl {s : set α} : s ⊆ s := subset.refl s
 
-@[trans] theorem subset.trans {a b c : set α} (ab : a ⊆ b) (bc : b ⊆ c) : a ⊆ c :=
-assume x h, bc (ab h)
+@[trans] theorem subset.trans {a b c : set α} (ab : a ⊆ b) (bc : b ⊆ c) : a ⊆ c := λ x h, bc $ ab h
 
 @[trans] theorem mem_of_eq_of_mem {x y : α} {s : set α} (hx : x = y) (h : y ∈ s) : x ∈ s :=
 hx.symm ▸ h
diff --git a/src/data/sym/sym2.lean b/src/data/sym/sym2.lean
@@ -60,8 +60,8 @@ attribute [refl] rel.refl
 @[symm] lemma rel.symm {x y : α × α} : rel α x y → rel α y x :=
 by rintro ⟨_, _⟩; constructor
 
-@[trans] lemma rel.trans {x y z : α × α} : rel α x y → rel α y z → rel α x z :=
-by { intros a b, cases_matching* rel _ _ _; apply rel.refl <|> apply rel.swap }
+@[trans] lemma rel.trans {x y z : α × α} (a : rel α x y) (b : rel α y z) : rel α x z :=
+by { cases_matching* rel _ _ _; apply rel.refl <|> apply rel.swap }
 
 lemma rel.is_equivalence : equivalence (rel α) := by tidy; apply rel.trans; assumption
 
diff --git a/src/logic/equiv/basic.lean b/src/logic/equiv/basic.lean
@@ -132,8 +132,7 @@ initialize_simps_projections equiv (to_fun → apply, inv_fun → symm_apply)
 
 /-- Composition of equivalences `e₁ : α ≃ β` and `e₂ : β ≃ γ`. -/
 @[trans] protected def trans (e₁ : α ≃ β) (e₂ : β ≃ γ) : α ≃ γ :=
-⟨e₂ ∘ e₁, e₁.symm ∘ e₂.symm,
-  e₂.left_inv.comp e₁.left_inv, e₂.right_inv.comp e₁.right_inv⟩
+⟨e₂ ∘ e₁, e₁.symm ∘ e₂.symm, e₂.left_inv.comp e₁.left_inv, e₂.right_inv.comp e₁.right_inv⟩
 
 @[simp]
 lemma to_fun_as_coe (e : α ≃ β) : e.to_fun = e := rfl
diff --git a/src/measure_theory/integral/interval_integral.lean b/src/measure_theory/integral/interval_integral.lean
@@ -233,8 +233,8 @@ h.symm
 @[refl] lemma refl : interval_integrable f μ a a :=
 by split; simp
 
-@[trans] lemma trans (hab : interval_integrable f μ a b) (hbc : interval_integrable f μ b c) :
-  interval_integrable f μ a c :=
+@[trans] lemma trans {a b c : ℝ} (hab : interval_integrable f μ a b)
+  (hbc : interval_integrable f μ b c) : interval_integrable f μ a c :=
 ⟨(hab.1.union hbc.1).mono_set Ioc_subset_Ioc_union_Ioc,
   (hbc.2.union hab.2).mono_set Ioc_subset_Ioc_union_Ioc⟩
 
diff --git a/src/measure_theory/measure/vector_measure.lean b/src/measure_theory/measure/vector_measure.lean
@@ -1030,7 +1030,8 @@ lemma eq {w : vector_measure α M} (h : v = w) : v ≪ᵥ w :=
 @[refl] lemma refl (v : vector_measure α M) : v ≪ᵥ v :=
 eq rfl
 
-@[trans] lemma trans {u : vector_measure α L} (huv : u ≪ᵥ v) (hvw : v ≪ᵥ w) : u ≪ᵥ w :=
+@[trans] lemma trans {u : vector_measure α L} {v : vector_measure α M} {w : vector_measure α N}
+  (huv : u ≪ᵥ v) (hvw : v ≪ᵥ w) : u ≪ᵥ w :=
 λ _ hs, huv $ hvw hs
 
 lemma zero (v : vector_measure α N) : (0 : vector_measure α M) ≪ᵥ v :=
diff --git a/src/order/filter/basic.lean b/src/order/filter/basic.lean
@@ -1246,9 +1246,8 @@ lemma eventually_eq.rfl {l : filter α} {f : α → β} : f =ᶠ[l] f := eventua
   g =ᶠ[l] f :=
 H.mono $ λ _, eq.symm
 
-@[trans] lemma eventually_eq.trans {f g h : α → β} {l : filter α}
-  (H₁ : f =ᶠ[l] g) (H₂ : g =ᶠ[l] h) :
-  f =ᶠ[l] h :=
+@[trans] lemma eventually_eq.trans {l : filter α} {f g h : α → β}
+  (H₁ : f =ᶠ[l] g) (H₂ : g =ᶠ[l] h) : f =ᶠ[l] h :=
 H₂.rw (λ x y, f x = y) H₁
 
 lemma eventually_eq.prod_mk {l} {f f' : α → β} (hf : f =ᶠ[l] f') {g g' : α → γ} (hg : g =ᶠ[l] g') :
diff --git a/src/order/ideal.lean b/src/order/ideal.lean
@@ -109,7 +109,7 @@ protected lemma is_ideal (I : ideal P) : is_ideal (I : set P) := ⟨I.2, I.3, I.
 /-- The partial ordering by subset inclusion, inherited from `set P`. -/
 instance : partial_order (ideal P) := partial_order.lift coe coe_injective
 
-@[trans] lemma mem_of_mem_of_le : x ∈ I → I ≤ J → x ∈ J :=
+@[trans] lemma mem_of_mem_of_le {x : P} {I J : ideal P} : x ∈ I → I ≤ J → x ∈ J :=
 @set.mem_of_mem_of_subset P x I J
 
 /-- A proper ideal is one that is not the whole set.
diff --git a/src/order/rel_classes.lean b/src/order/rel_classes.lean
@@ -320,7 +320,7 @@ lemma subset_of_eq [is_refl α (⊆)] : a = b → a ⊆ b := λ h, h ▸ subset_
 lemma superset_of_eq [is_refl α (⊆)] : a = b → b ⊆ a := λ h, h ▸ subset_rfl
 lemma ne_of_not_subset [is_refl α (⊆)] : ¬ a ⊆ b → a ≠ b := mt subset_of_eq
 lemma ne_of_not_superset [is_refl α (⊆)] : ¬ a ⊆ b → b ≠ a := mt superset_of_eq
-@[trans] lemma subset_trans [is_trans α (⊆)] (h : a ⊆ b) (h' : b ⊆ c) : a ⊆ c := trans h h'
+@[trans] lemma subset_trans [is_trans α (⊆)] {a b c : α} : a ⊆ b → b ⊆ c → a ⊆ c := trans
 
 lemma subset_antisymm [is_antisymm α (⊆)] (h : a ⊆ b) (h' : b ⊆ a) : a = b :=
 antisymm h h'
@@ -349,8 +349,7 @@ lemma ssubset_irrefl [is_irrefl α (⊂)] (a : α) : ¬ a ⊂ a := irrefl _
 lemma ssubset_irrfl [is_irrefl α (⊂)] {a : α} : ¬ a ⊂ a := irrefl _
 lemma ne_of_ssubset [is_irrefl α (⊂)] {a b : α} : a ⊂ b → a ≠ b := ne_of_irrefl
 lemma ne_of_ssuperset [is_irrefl α (⊂)] {a b : α} : a ⊂ b → b ≠ a := ne_of_irrefl'
-@[trans] lemma ssubset_trans [is_trans α (⊂)] {a b c : α} (h : a ⊂ b) (h' : b ⊂ c) : a ⊂ c :=
-trans h h'
+@[trans] lemma ssubset_trans [is_trans α (⊂)] {a b c : α} : a ⊂ b → b ⊂ c → a ⊂ c := trans
 lemma ssubset_asymm [is_asymm α (⊂)] {a b : α} (h : a ⊂ b) : ¬ b ⊂ a := asymm h
 
 alias ssubset_irrfl   ← has_ssubset.ssubset.false
diff --git a/test/calc.lean b/test/calc.lean
@@ -0,0 +1,41 @@
+import analysis.asymptotics.asymptotic_equivalent
+import measure_theory.integral.interval_integral
+import measure_theory.measure.vector_measure
+
+variables {α β γ δ : Type*}
+
+section is_equivalent
+
+open_locale asymptotics
+
+example {l : filter α} {u v w : α → β} [normed_group β]
+  (huv : u ~[l] v) (hvw : v ~[l] w) : u ~[l] w :=
+calc u ~[l] v : huv
+   ... ~[l] w : hvw
+
+end is_equivalent
+
+section interval_integral
+
+variables {f : ℝ → ℝ} {μ : measure_theory.measure ℝ}
+local notation u ` ~[`:50 a:50`-`:40 b `] `:0 v:50 := interval_integrable a b u v
+
+example {a b c : ℝ} (hab : a ~[f-μ] b)
+  (hbc : b ~[f-μ] c) : interval_integrable f μ a c :=
+calc a ~[f-μ] b : hab
+   ... ~[f-μ] c : hbc
+
+end interval_integral
+
+section vector_measure
+
+open measure_theory measure_theory.vector_measure
+
+open_locale measure_theory
+
+example {u : vector_measure ℝ ℝ} {v : vector_measure ℝ ℝ} {w : vector_measure ℝ ℝ}
+  (huv : u ≪ᵥ v) (hvw : v ≪ᵥ w) : u ≪ᵥ w :=
+calc u ≪ᵥ v : huv
+   ... ≪ᵥ w : hvw
+
+end vector_measure
