mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a b : G
⊢ a * b / b = a

Tactic:
by
  rw [div_eq_mul_inv, mul_inv_cancel_right a b]

Goal state after:
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_2
f : α → β
g₁ g₂ : β → α
h₁ : LeftInverse g₁ f
h₂ : RightInverse g₂ f
⊢ g₁ = g₁ ∘ f ∘ g₂

Tactic:
by rw [h₂.comp_eq_id, comp_id]

Goal state after:
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_2
f✝ : α → β
γ : Type u_4
inst✝ : Nontrivial γ
surj : Surjective fun g ↦ g ∘ f✝
c c' : γ
not_inj : ∃ x x_1 x_2, ¬x = x_1
a₁ a₂ : α
eq : f✝ a₁ = f✝ a₂
ne : ¬a₁ = a₂
f : β → γ
hf : (fun g ↦ g ∘ f✝) f = fun x ↦ if x = a₂ then c else c'
h₁ : f (f✝ a₁) = c'
h₂ : f (f✝ a₂) = c
⊢ c = c'

Tactic:
rw [← h₁, eq, h₂]

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case tail.inl
α : Type u_1
r : α → α → Prop
a b c : α
U : Relator.RightUnique r
ac : ReflTransGen r a c
b✝ c✝ : α
a✝ : ReflTransGen r a b✝
bd : r b✝ c✝
IH : ReflTransGen r b✝ c
⊢ ReflTransGen r c✝ c ∨ ReflTransGen r c c✝

pp: case tail.inr
α : Type u_1
r : α → α → Prop
a b c : α
U : Relator.RightUnique r
ac : ReflTransGen r a c
b✝ c✝ : α
a✝ : ReflTransGen r a b✝
bd : r b✝ c✝
IH : ReflTransGen r c b✝
⊢ ReflTransGen r c✝ c ∨ ReflTransGen r c c✝

Tactic:
· rcases cases_head IH with (rfl | ⟨e, be, ec⟩)
      · exact Or.inr (single bd)
      · cases U bd be
        exact Or.inl ec

Goal state after:
case tail.inr
α : Type u_1
r : α → α → Prop
a b c : α
U : Relator.RightUnique r
ac : ReflTransGen r a c
b✝ c✝ : α
a✝ : ReflTransGen r a b✝
bd : r b✝ c✝
IH : ReflTransGen r c b✝
⊢ ReflTransGen r c✝ c ∨ ReflTransGen r c c✝
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r r' : α → α → Prop
inst✝¹ : Std.Refl r
inst✝ : IsTrans α r
h : r' ≤ r
⊢ ReflTransGen r' ≤ r

Tactic:
simpa [reflTransGen_eq_self] using ReflTransGen.mono h

Goal state after:
Module: Mathlib.Logic.Function.Conjugate

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
ga : α → α → α
gb : β → β → β
inst✝ : Std.Associative ga
h : Semiconj₂ f ga gb
h_surj : Surjective f
x₁ x₂ x₃ : α
⊢ gb (gb (f x₁) (f x₂)) (f x₃) = gb (f x₁) (gb (f x₂) (f x₃))

Tactic:
by simp only [← h.eq, Std.Associative.assoc (op := ga)]

Goal state after:
Module: Mathlib.Logic.Function.Iterate

Goal state before:
pp: α : Type u
f : α → α
m n : ℕ
⊢ f^[m + n.succ] = f^[m] ∘ f^[n.succ]

Tactic:
Nat.add_succ,

Goal state after:
α : Type u
f : α → α
m n : ℕ
⊢ f^[(m + n).succ] = f^[m] ∘ f^[n.succ]
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: M : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
inst✝⁷ : SMul M α
inst✝⁶ : SMul Mᵐᵒᵖ α
inst✝⁵ : IsCentralScalar M α
inst✝⁴ : SMul M N
inst✝³ : SMul Mᵐᵒᵖ N
inst✝² : IsCentralScalar M N
inst✝¹ : SMul N α
inst✝ : IsScalarTower M N α
m : Mᵐᵒᵖ
n : N
a : α
⊢ (m • n) • a = m • n • a

Tactic:
by rw [← unop_smul_eq_smul m (n • a), ← unop_smul_eq_smul m n, smul_assoc]

Goal state after:
Module: Mathlib.Order.Compare

Goal state before:
pp: o o' : Ordering
⊢ o.swap = o' ↔ o = o'.swap

Tactic:
rw [← swap_inj, swap_swap]

Goal state after:
Module: Mathlib.Order.RelClasses

Goal state before:
pp: α : Type u
β : Type v
r✝ : α → α → Prop
s : β → β → Prop
r : α → α → Prop
inst✝ : IsStrictOrder α r
x y : α
h : r x y
e : y = x
⊢ False

Tactic:
rw [e] at h; exact irrefl _ h

Goal state after:
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
⊢ Antitone (f ∘ ⇑ofDual) ↔ Monotone f

Tactic:
antitone_comp_ofDual_iff

Goal state after:
α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
⊢ Monotone f ↔ Monotone f
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
a b c : α
⊢ Disjoint a (b ⊔ c) ↔ Disjoint a b ∧ Disjoint a c

Tactic:
simp only [disjoint_iff, inf_sup_left, sup_eq_bot_iff]

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
x y : α × β
⊢ Disjoint x.fst y.fst ∧ Disjoint x.snd y.snd → Disjoint x y

Tactic:
· rintro ⟨ha, hb⟩ z hza hzb
    exact ⟨ha hza.1 hzb.1, hb hza.2 hzb.2⟩

Goal state after:
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: case neg
n : ℕ
ih :
  ∀ (m : ℕ),
    m < n →
      ∀ {f : ℕ → ℕ},
        Antitone f →
          (∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)) → f 0 = m → ∃ n, n ≤ m ∧ ∀ (m : ℕ), n ≤ m → f m = f n
f : ℕ → ℕ
hfmono : Antitone f
hfstab : ∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)
h : f 0 = n
heq : ¬f 0 = f 1
⊢ ∃ n_1, n_1 ≤ n ∧ ∀ (m : ℕ), n_1 ≤ m → f m = f n_1

Tactic:
have hlt : f 1 < f 0 := (hfmono (Nat.le_succ 0)).lt_of_ne' heq
      let g (i : ℕ) := f (i + 1)
      have hg_anti : Antitone g := by grind [Antitone]
      obtain ⟨p, hp, hp'⟩ := ih (f 1) (by grind) hg_anti (by grind) rfl
      refine ⟨p + 1, by omega, fun m hm => ?_⟩
      specialize hp' (m - 1) (by lia)
      grind

Goal state after:
Module: Mathlib.Data.Set.Subsingleton

Goal state before:
pp: α : Type u
s : Set α
⊢ s.Subsingleton ∨ s.Nontrivial

Tactic:
simp [or_iff_not_imp_right]

Goal state after:
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : HeytingAlgebra α
a : α
inst✝ : Nontrivial α
⊢ a < aᶜ ↔ a = ⊥

Tactic:
rw [lt_iff_le_and_ne]; simp

Goal state after:
Module: Mathlib.Order.BooleanAlgebra.Set

Goal state before:
pp: α : Type u_1
s t : Set α
⊢ s \ t ∪ s ∩ t = s

Tactic:
union_comm

Goal state after:
α : Type u_1
s t : Set α
⊢ s ∩ t ∪ s \ t = s
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
f : ℕ → Type u
⊢ RightInverse (Sum.elim (Sigma.mk 0) (Sigma.map Nat.succ fun x ↦ id)) fun x ↦
    Sigma.casesOn x fun n ↦
      Nat.casesOn (motive := fun i ↦ f i → f 0 ⊕ (n : ℕ) × f (n + 1)) n (fun x ↦ inl x) fun n x ↦ inr ⟨n, x⟩

Tactic:
rintro (x | ⟨n, x⟩)

Goal state after:
case inl
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
f : ℕ → Type u
x : f 0
⊢ (fun x ↦
        Sigma.casesOn x fun n ↦
          Nat.casesOn (motive := fun i ↦ f i → f 0 ⊕ (n : ℕ) × f (n + 1)) n (fun x ↦ inl x) fun n x ↦ inr ⟨n, x⟩)
      (Sum.elim (Sigma.mk 0) (Sigma.map Nat.succ fun x ↦ id) (inl x)) =
    inl x

case inr
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
f : ℕ → Type u
n : ℕ
x : f (n + 1)
⊢ (fun x ↦
        Sigma.casesOn x fun n ↦
          Nat.casesOn (motive := fun i ↦ f i → f 0 ⊕ (n : ℕ) × f (n + 1)) n (fun x ↦ inl x) fun n x ↦ inr ⟨n, x⟩)
      (Sum.elim (Sigma.mk 0) (Sigma.map Nat.succ fun x ↦ id) (inr ⟨n, x⟩)) =
    inr ⟨n, x⟩
Module: Mathlib.Logic.Equiv.Prod

Goal state before:
pp: α₁ : Type u_9
β₁ : Type u_11
β₂ : Type u_12
e : α₁ → β₁ ≃ β₂
⊢ (prodCongrLeft e).trans (prodComm β₂ α₁) = (prodComm β₁ α₁).trans (prodCongrRight e)

Tactic:
by
  ext ⟨a, b⟩ : 1
  simp

Goal state after:
Module: Mathlib.Logic.Equiv.Prod

Goal state before:
pp: α₁ : Type u_9
β₁ : Type u_11
β₂ : Type u_12
e : α₁ → β₁ ≃ β₂
⊢ (prodCongrRight e).trans (prodComm α₁ β₂) = (prodComm α₁ β₁).trans (prodCongrLeft e)

Tactic:
by
  ext ⟨a, b⟩ : 1
  simp

Goal state after:
Module: Mathlib.Logic.Equiv.Prod

Goal state before:
pp: α₁ : Type u_9
β₁ : Type u_11
β₂ : Type u_12
e : α₁ → β₁ ≃ β₂
⊢ (sigmaCongrRight e).trans (sigmaEquivProd α₁ β₂) = (sigmaEquivProd α₁ β₁).trans (prodCongrRight e)

Tactic:
by
  ext ⟨a, b⟩ : 1
  simp

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
a b c : α
⊢ a ⇔ (b ⇔ c) = b ⇔ (a ⇔ c)

Tactic:
← bihimp_assoc,

Goal state after:
α : Type u_2
inst✝ : BooleanAlgebra α
a b c : α
⊢ a ⇔ b ⇔ c = b ⇔ a ⇔ c
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
s : Set α
⊢ ¬s.offDiag.Nonempty ↔ s.Subsingleton

Tactic:
← not_nontrivial_iff,

Goal state after:
α : Type u_1
s : Set α
⊢ ¬s.offDiag.Nonempty ↔ ¬s.Nontrivial
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s t : Set β
hf : Surjective f
⊢ s ⊆ range f

Tactic:
hf.range_eq

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s t : Set β
hf : Surjective f
⊢ s ⊆ univ
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t₁ t₂ : Set β
f : α → β
h₁ : SurjOn f s₁ t₁
h₂ : SurjOn f s₂ t₂
h : InjOn f (s₁ ∪ s₂)
⊢ SurjOn f (s₁ ∩ s₂) (t₁ ∩ t₂)

Tactic:
intro y hy

Goal state after:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t₁ t₂ : Set β
f : α → β
h₁ : SurjOn f s₁ t₁
h₂ : SurjOn f s₂ t₂
h : InjOn f (s₁ ∪ s₂)
y : β
hy : y ∈ t₁ ∩ t₂
⊢ y ∈ f '' (s₁ ∩ s₂)
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
r : Set β
hf : BijOn f s t
hrt : r ⊆ t
y : α
hy : y ∈ s
hx : f y ∈ r
⊢ f y ∈ f '' (s ∩ f ⁻¹' r)

Tactic:
exact ⟨y, ⟨hy, hx⟩, rfl⟩

Goal state after:
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
f' : β → α
h : LeftInvOn f' f s
hf : SurjOn f s t
y : β
hy : y ∈ t
x : α
hs : x ∈ s
hx : f x = y
⊢ f' y ∈ s

Tactic:
← hx,

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
f' : β → α
h : LeftInvOn f' f s
hf : SurjOn f s t
y : β
hy : y ∈ t
x : α
hs : x ∈ s
hx : f x = y
⊢ f' (f x) ∈ s
Module: Mathlib.Data.Set.Function

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
f : α → β
g : β → α
s : Set α
hgf : LeftInvOn g f s
ginj : InjOn g (g ⁻¹' s)
x : β
hx : x ∈ g ⁻¹' s
⊢ MapsTo f s (g ⁻¹' s)

Tactic:
intro y hy

Goal state after:
case mpr
α : Type u_1
β : Type u_2
f : α → β
g : β → α
s : Set α
hgf : LeftInvOn g f s
ginj : InjOn g (g ⁻¹' s)
x : β
hx : x ∈ g ⁻¹' s
y : α
hy : y ∈ s
⊢ f y ∈ g ⁻¹' s
Module: Mathlib.Data.Set.Function

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
⊢ SurjOn f s t → ∃ s', s' ⊆ s ∧ BijOn f s' t

Tactic:
rcases eq_empty_or_nonempty t with (rfl | ht)
    · exact fun _ => ⟨∅, empty_subset _, bijOn_empty f⟩
    · intro h
      have : Nonempty α := ⟨Classical.choose (h.comap_nonempty ht)⟩
      exact ⟨_, h.mapsTo_invFunOn.image_subset, h.bijOn_subset⟩

Goal state after:
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
h : Semiconj f fa fb
ha : Bijective fa
hf : Injective f
⊢ BijOn fb (range f) (range f)

Tactic:
rw [← image_univ]
  exact h.bijOn_image ha.bijOn_univ hf.injOn

Goal state after:
Module: Mathlib.Algebra.Group.Units.Defs

Goal state before:
pp: α : Type u
inst✝ : Monoid α
v i₁ : α
vi₁ : v * i₁ = 1
iv₁ : i₁ * v = 1
v' i₂ : α
vi₂ : v' * i₂ = 1
iv₂ : i₂ * v' = 1
e : ↑{ val := v, inv := i₁, val_inv := vi₁, inv_val := iv₁ } = ↑{ val := v', inv := i₂, val_inv := vi₂, inv_val := iv₂ }
⊢ { val := v, inv := i₁, val_inv := vi₁, inv_val := iv₁ } = { val := v', inv := i₂, val_inv := vi₂, inv_val := iv₂ }

Tactic:
by
    simp only at e; subst v'; congr
    simpa only [iv₂, vi₁, one_mul, mul_one] using mul_assoc i₂ v i₁

Goal state after:
Module: Mathlib.Algebra.Group.Units.Defs

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
u : Mˣ
x✝ : IsUnit (a * ↑u)
v : Mˣ
hv : ↑v = a * ↑u
⊢ IsUnit (a * ↑u * ↑u⁻¹)

Tactic:
exists v * u⁻¹

Goal state after:
M : Type u_1
inst✝ : Monoid M
a : M
u : Mˣ
x✝ : IsUnit (a * ↑u)
v : Mˣ
hv : ↑v = a * ↑u
⊢ ↑(v * u⁻¹) = a * ↑u * ↑u⁻¹
Module: Mathlib.Algebra.Group.Units.Basic

Goal state before:
pp: α : Type u
inst✝¹ : CommMonoid α
inst✝ : Subsingleton αˣ
a b : α
h : a * b = 1
⊢ b * a = 1

Tactic:
by rwa [mul_comm]

Goal state after:
Module: Mathlib.Algebra.Group.Prod

Goal state before:
pp: G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : DivInvMonoid G
inst✝ : DivInvMonoid H
x✝¹ x✝ : G × H
⊢ x✝¹ / x✝ = x✝¹ * x✝⁻¹

Tactic:
by ext <;> exact div_eq_mul_inv ..

Goal state after:
Module: Mathlib.Algebra.Group.End

Goal state before:
pp: α : Type u_4
inst✝ : DecidableEq α
i j : α
σ : Perm α
⊢ σ * swap i j = σ ↔ i = j

Tactic:
rw [mul_eq_left, swap_eq_one_iff]

Goal state after:
Module: Mathlib.Algebra.Group.Equiv.Opposite

Goal state before:
pp: M✝ : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
inst✝¹ : Mul M
inst✝ : Mul N
f : M →ₙ* N
hf : ∀ (x y : M), Commute (f x) (f y)
x y : M
⊢ (op ∘ ⇑f) (x * y) = (op ∘ ⇑f) x * (op ∘ ⇑f) y

Tactic:
simp [(hf x y).eq]

Goal state after:
Module: Mathlib.Algebra.Group.Equiv.Opposite

Goal state before:
pp: M✝ : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
f : M →* N
hf : ∀ (x y : M), Commute (f x) (f y)
x y : M
⊢ (op ∘ ⇑f) (x * y) = (op ∘ ⇑f) x * (op ∘ ⇑f) y

Tactic:
simp [(hf x y).eq]

Goal state after:
Module: Mathlib.Algebra.Ring.Defs

Goal state before:
pp: α : Type u
inst✝ : NonAssocRing α
a b c : α
⊢ a * (1 - b) * c = a * c - a * b * c

Tactic:
by
  rw [mul_one_sub, sub_mul]

Goal state after:
Module: Mathlib.Algebra.Group.Int.Even

Goal state before:
pp: case pred
i✝ : ℕ
a✝ : IsSquare (-↑i✝).sign ↔ 0 ≤ -↑i✝
⊢ IsSquare (-1) ↔ i✝ + 1 ≤ 0

Tactic:
simp only [reduceNeg, le_zero_eq, Nat.add_eq_zero_iff, succ_ne_self, and_false, iff_false]

Goal state after:
case pred
i✝ : ℕ
a✝ : IsSquare (-↑i✝).sign ↔ 0 ≤ -↑i✝
⊢ ¬IsSquare (-1)
Module: Mathlib.Algebra.Ring.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : DivisionMonoid R
inst✝ : HasDistribNeg R
a : R
⊢ 1 / (-1 * a) = 1 / a * (1 / -1)

Tactic:
by rw [one_div_mul_one_div_rev]

Goal state after:
Module: Mathlib.Algebra.Group.Commute.Units

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
u : Mˣ
a : M
⊢ Commute (↑u) a ↔ ↑u * a * ↑u⁻¹ = a

Tactic:
rw [Units.mul_inv_eq_iff_eq_mul, Commute, SemiconjBy]

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Defs

Goal state before:
pp: α : Type u_1
inst✝⁶ : Mul α
inst✝⁵ : Zero α
inst✝⁴ : Preorder α
inst✝³ : MulPosMono α
β : Type u_2
inst✝² : Zero β
inst✝¹ : Mul β
inst✝ : Preorder β
f : β → α
zero : f 0 = 0
mul : ∀ (x y : β), f (x * y) = f x * f y
le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y
a : β
ha : 0 ≤ a
b c : β
hbc : b ≤ c
⊢ b * a ≤ c * a

Tactic:
by
    rw [← le, mul, mul]; exact mul_le_mul_of_nonneg_right (le.2 hbc) (by rwa [← zero, le])

Goal state after:
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

Goal state before:
pp: α : Type u
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : MulLeftMono α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
⊢ a / d ≤ b / c

Tactic:
rw [div_eq_mul_inv, div_eq_mul_inv, mul_comm b, mul_inv_le_inv_mul_iff, mul_comm]

Goal state after:
α : Type u
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : MulLeftMono α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
⊢ a * c ≤ b * d
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : MulZeroClass α
a b : α
inst✝² : Preorder α
inst✝¹ : PosMulStrictMono α
inst✝ : PosMulReflectLT α
h : 0 < a
⊢ 0 < a * b ↔ 0 < b

Tactic:
simpa using mul_lt_mul_iff_right₀ (b := 0) h

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : MulZeroClass α
a b c d : α
inst✝² : PartialOrder α
inst✝¹ : PosMulStrictMono α
inst✝ : MulPosStrictMono α
hab : a ≤ b
hcd : c ≤ d
a0 : 0 < a
d0 : 0 < d
h : a * c = b * d
⊢ a = b ∧ c = d

Tactic:
simp only [eq_iff_le_not_lt, hab, hcd, true_and]

Goal state after:
α : Type u_1
inst✝³ : MulZeroClass α
a b c d : α
inst✝² : PartialOrder α
inst✝¹ : PosMulStrictMono α
inst✝ : MulPosStrictMono α
hab : a ≤ b
hcd : c ≤ d
a0 : 0 < a
d0 : 0 < d
h : a * c = b * d
⊢ ¬a < b ∧ ¬c < d
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : MulZeroClass α
a b c d : α
inst✝² : PartialOrder α
inst✝¹ : PosMulStrictMono α
inst✝ : MulPosStrictMono α
hab : a ≤ b
hcd : c ≤ d
b0 : 0 < b
c0 : 0 < c
h : a * c = b * d
⊢ a = b ∧ c = d

Tactic:
simp only [eq_iff_le_not_lt, hab, hcd, true_and]

Goal state after:
α : Type u_1
inst✝³ : MulZeroClass α
a b c d : α
inst✝² : PartialOrder α
inst✝¹ : PosMulStrictMono α
inst✝ : MulPosStrictMono α
hab : a ≤ b
hcd : c ≤ d
b0 : 0 < b
c0 : 0 < c
h : a * c = b * d
⊢ ¬a < b ∧ ¬c < d
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: case inl
α : Type u_1
inst✝³ : MulZeroClass α
a b : α
inst✝² : LinearOrder α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
hab : 0 < a * b
ha : a < 0
⊢ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0

pp: case inr.inl
α : Type u_1
inst✝³ : MulZeroClass α
b : α
inst✝² : LinearOrder α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
hab : 0 < 0 * b
⊢ 0 < 0 ∧ 0 < b ∨ 0 < 0 ∧ b < 0

pp: case inr.inr
α : Type u_1
inst✝³ : MulZeroClass α
a b : α
inst✝² : LinearOrder α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
hab : 0 < a * b
ha : 0 < a
⊢ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0

Tactic:
· refine Or.inr ⟨ha, lt_imp_lt_of_le_imp_le (fun hb => ?_) hab⟩
    exact mul_nonpos_of_nonpos_of_nonneg ha.le hb

Goal state after:
case inr.inl
α : Type u_1
inst✝³ : MulZeroClass α
b : α
inst✝² : LinearOrder α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
hab : 0 < 0 * b
⊢ 0 < 0 ∧ 0 < b ∨ 0 < 0 ∧ b < 0

case inr.inr
α : Type u_1
inst✝³ : MulZeroClass α
a b : α
inst✝² : LinearOrder α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
hab : 0 < a * b
ha : 0 < a
⊢ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0
Module: Mathlib.Algebra.Order.Ring.Defs

Goal state before:
pp: R : Type u
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
a b : R
hab : a * b = 0
⊢ a = 0 ∨ b = 0

Tactic:
contrapose! hab
    obtain ha | ha := hab.1.lt_or_gt <;> obtain hb | hb := hab.2.lt_or_gt
    exacts [(mul_pos_of_neg_of_neg ha hb).ne', (mul_neg_of_neg_of_pos ha hb).ne,
      (mul_neg_of_pos_of_neg ha hb).ne, (mul_pos ha hb).ne']

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : ExistsAddOfLE R
inst✝³ : MulPosStrictMono R
inst✝² : PosMulStrictMono R
inst✝¹ : AddLeftMono R
inst✝ : AddLeftReflectLE R
a b c : R
⊢ 0 ≤ a * b ∨ 0 ≤ b * c ∨ 0 ≤ c * a

Tactic:
mul_nonneg_iff

Goal state after:
R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : ExistsAddOfLE R
inst✝³ : MulPosStrictMono R
inst✝² : PosMulStrictMono R
inst✝¹ : AddLeftMono R
inst✝ : AddLeftReflectLE R
a b c : R
⊢ (0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0) ∨ 0 ≤ b * c ∨ 0 ≤ c * a
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : ExistsAddOfLE R
inst✝³ : MulPosStrictMono R
inst✝² : PosMulStrictMono R
inst✝¹ : AddLeftMono R
inst✝ : AddLeftReflectLE R
a b c : R
⊢ (0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0) ∨ 0 ≤ b * c ∨ 0 ≤ c * a

Tactic:
mul_nonneg_iff

Goal state after:
R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : ExistsAddOfLE R
inst✝³ : MulPosStrictMono R
inst✝² : PosMulStrictMono R
inst✝¹ : AddLeftMono R
inst✝ : AddLeftReflectLE R
a b c : R
⊢ (0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0) ∨ (0 ≤ b ∧ 0 ≤ c ∨ b ≤ 0 ∧ c ≤ 0) ∨ 0 ≤ c * a
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : ExistsAddOfLE R
inst✝³ : MulPosStrictMono R
inst✝² : PosMulStrictMono R
inst✝¹ : AddLeftMono R
inst✝ : AddLeftReflectLE R
a b c : R
⊢ (0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0) ∨ (0 ≤ b ∧ 0 ≤ c ∨ b ≤ 0 ∧ c ≤ 0) ∨ 0 ≤ c * a

Tactic:
mul_nonneg_iff

Goal state after:
R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : ExistsAddOfLE R
inst✝³ : MulPosStrictMono R
inst✝² : PosMulStrictMono R
inst✝¹ : AddLeftMono R
inst✝ : AddLeftReflectLE R
a b c : R
⊢ (0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0) ∨ (0 ≤ b ∧ 0 ≤ c ∨ b ≤ 0 ∧ c ≤ 0) ∨ 0 ≤ c ∧ 0 ≤ a ∨ c ≤ 0 ∧ a ≤ 0
Module: Mathlib.Algebra.Order.Group.Lattice

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
ha : 1 ≤ a ^ 2
⊢ 1 ≤ a

Tactic:
suffices this : (a ⊓ 1) * (a ⊓ 1) = a ⊓ 1 by
    rwa [← inf_eq_right, ← mul_eq_left]

Goal state after:
α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
ha : 1 ≤ a ^ 2
⊢ (a ⊓ 1) * (a ⊓ 1) = a ⊓ 1
Module: Mathlib.Algebra.Order.Group.Lattice

Goal state before:
pp: case right
α✝ : Type u_1
inst✝⁴ : Lattice α✝
inst✝³ : CommGroup α✝
α : Type u_2
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
x y z : α
⊢ x⁻¹ * ((x ⊓ (y ⊓ z)) * ((x ⊔ y) ⊓ (x ⊔ z))) ≤ z

Tactic:
rw [inv_mul_le_iff_le_mul, ← inf_mul_sup x z]
      exact mul_le_mul' (inf_le_inf_left _ inf_le_right) inf_le_right

Goal state after:
Module: Mathlib.Data.Nat.Cast.Order.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : AddMonoidWithOne α
inst✝² : PartialOrder α
inst✝¹ : AddLeftMono α
inst✝ : ZeroLEOneClass α
n : ℕ
⊢ ↑n ≤ ↑n + 1

Tactic:
exact le_add_of_nonneg_right zero_le_one

Goal state after:
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: case refine_1
k n : ℕ
hk : n.gcd k < k
hk' : ↑k ≠ 0
key : n.gcd k = (↑n * n.gcdA k % ↑k).toNat
⊢ (n.gcdA k % ↑k).toNat < k

Tactic:
Int.toNat_lt (Int.emod_nonneg _ hk')

Goal state after:
case refine_1
k n : ℕ
hk : n.gcd k < k
hk' : ↑k ≠ 0
key : n.gcd k = (↑n * n.gcdA k % ↑k).toNat
⊢ n.gcdA k % ↑k < ↑k
Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs

Goal state before:
pp: α : Type u
inst✝² : Mul α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedMul α
a c : α
⊢ a ≤ a * c

Tactic:
exact le_self_mul

Goal state after:
Module: Mathlib.Algebra.Regular.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemigroup R
a b : R
ab : IsRegular (a * b)
⊢ IsRegular (b * a)

Tactic:
by rwa [mul_comm]

Goal state after:
Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic

Goal state before:
pp: α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hab : AddLECancellable (a - b)
h₁ : b ≤ a
h₂ : c ≤ a
h₃ : a - b = a - c
⊢ b = c

Tactic:
by
  rw [← hab.inj]
  rw [tsub_add_cancel_of_le h₁, h₃, tsub_add_cancel_of_le h₂]

Goal state after:
Module: Mathlib.Algebra.Order.Sub.Basic

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
⊢ b - a + a = b ↔ a ≤ b

Tactic:
rw [add_comm]
  exact add_tsub_cancel_iff_le

Goal state after:
Module: Mathlib.Algebra.Order.Sub.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : AddCommMonoid α
inst✝² : LinearOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : AddRightReflectLE α
a b c : α
⊢ a - b ≤ c ↔ a ≤ c + b

Tactic:
change dite _ _ _ ≤ c ↔ _
    split_ifs with h
    · have := (exists_add_of_le h).choose_spec
      rw [this] at h
      conv_rhs => rw [this, add_comm]
      rw [add_le_add_iff_right]
    · rw [not_le] at h
      constructor <;> intro h'
      · simpa using add_le_add h' h.le
      · exact zero_le

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Cast

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
n : ℤ
hx : |x| ≤ 1
hnx : 0 < n → 0 ≤ x + ↑n
hnx' : n < 0 → x + ↑n ≤ 0
⊢ 0 ≤ ↑n * (x + ↑n)

Tactic:
mul_nonneg_iff

Goal state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
n : ℤ
hx : |x| ≤ 1
hnx : 0 < n → 0 ≤ x + ↑n
hnx' : n < 0 → x + ↑n ≤ 0
⊢ 0 ≤ ↑n ∧ 0 ≤ x + ↑n ∨ ↑n ≤ 0 ∧ x + ↑n ≤ 0
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
inst✝³ : Add α
x : WithBot α
inst✝² : Nonempty α
inst✝¹ : Preorder α
inst✝ : AddLeftReflectLE α
⊢ AddLECancellable x → x ≠ ⊥

Tactic:
by rintro h rfl; exact (bot_lt_coe <| Classical.arbitrary _).not_ge <| h <| by simp

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: case coe.coe.zero
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : Mul α
inst✝ : MulLeftReflectLT α
a✝¹ a✝ : α
this : ↑a✝¹ * ↑a✝ ≠ 0
h : ↑a✝¹ * 0 < ↑a✝¹ * ↑a✝
⊢ 0 < ↑a✝

pp: case coe.coe.coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : Mul α
inst✝ : MulLeftReflectLT α
a✝² a✝¹ : α
this : ↑a✝² * ↑a✝¹ ≠ 0
a✝ : α
h : ↑a✝² * ↑a✝ < ↑a✝² * ↑a✝¹
⊢ ↑a✝ < ↑a✝¹

Tactic:
exacts [zero_lt_coe _, coe_lt_coe.mpr (lt_of_mul_lt_mul_left' <| coe_lt_coe.mp h)]

Goal state after: