mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.BinaryRec

Goal state before:
pp: n : Nat
hn : n >>> 1 ≠ 0
⊢ n ≠ 0

Tactic:
rintro rfl; exact hn rfl

Goal state after:
Module: Mathlib.Data.Nat.BinaryRec

Goal state before:
pp: motive : Nat → Sort u
zero : motive 0
bit : (b : Bool) → (n : Nat) → (n = 0 → b = true) → motive n → motive (Nat.bit b n)
b : Bool
n : Nat
h : n = 0 → b = true
⊢ binaryRec zero
      (fun b n ih ↦
        if h : n = 0 → b = true then bit b n h ih
        else
          have this := ⋯;
          ⋯ ▸ zero)
      (Nat.bit b n) =
    bit b n h (binaryRec' zero bit n)

Tactic:
binaryRec_eq _ _ (by simp),

Goal state after:
motive : Nat → Sort u
zero : motive 0
bit : (b : Bool) → (n : Nat) → (n = 0 → b = true) → motive n → motive (Nat.bit b n)
b : Bool
n : Nat
h : n = 0 → b = true
⊢ (if h : n = 0 → b = true then
      bit b n h
        (binaryRec zero
          (fun b n ih ↦
            if h : n = 0 → b = true then bit b n h ih
            else
              have this := ⋯;
              ⋯ ▸ zero)
          n)
    else
      have this := ⋯;
      ⋯ ▸ zero) =
    bit b n h (binaryRec' zero bit n)
Module: Mathlib.Order.Defs.Unbundled

Goal state before:
pp: α : Sort u_1
r : α → α → Prop
a✝ b✝ c : α
inst✝¹ : DecidableRel r
inst✝ : Antisymm r
a b : α
h₁ : Decidable.decide (r a b) = true
h₂ : Decidable.decide (r b a) = true
⊢ r a b

Tactic:
by simpa using h₁

Goal state after:
Module: Mathlib.Logic.Nontrivial.Defs

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : Nontrivial α
inst✝ : DecidableEq α
x y y' : α
h : y ≠ y'
hx : x = y
⊢ ∃ y, y ≠ x

pp: case neg
α : Type u_1
inst✝¹ : Nontrivial α
inst✝ : DecidableEq α
x y y' : α
h : y ≠ y'
hx : ¬x = y
⊢ ∃ y, y ≠ x

Tactic:
· rw [← hx] at h
    exact ⟨y', h.symm⟩

Goal state after:
case neg
α : Type u_1
inst✝¹ : Nontrivial α
inst✝ : DecidableEq α
x y y' : α
h : y ≠ y'
hx : ¬x = y
⊢ ∃ y, y ≠ x
Module: Mathlib.Logic.Basic

Goal state before:
pp: case refl
α : Sort u_2
γ : Sort u_3
f : α → γ
x : α
g : α → γ
h₁ : f ≍ g
⊢ f x = g x

Tactic:
cases h₁

Goal state after:
case refl.refl
α : Sort u_2
γ : Sort u_3
f : α → γ
x : α
⊢ f x = f x
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_3
β : Sort u_4
γ : Sort u_5
f : α → β → γ
P : Prop
inst✝ : Decidable P
a : P → α
b : ¬P → α
c : P → β
d : ¬P → β
⊢ f (dite P a b) (dite P c d) = if h : P then f (a h) (c h) else f (b h) (d h)

Tactic:
by
  by_cases h : P <;> simp [h]

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case tail.head
α : Type u_1
r : α → α → Prop
b✝ a b c : α
a✝ : ReflTransGen r a b
hbc : r b c
ih :
  ∀ {motive : (a : α) → ReflTransGen r a b → Prop},
    motive b ⋯ → (∀ {a c : α} (h' : r a c) (h : ReflTransGen r c b), motive c h → motive a ⋯) → motive a a✝
motive : (a : α) → ReflTransGen r a c → Prop
refl : motive c ⋯
head : ∀ {a c_1 : α} (h' : r a c_1) (h : ReflTransGen r c_1 c), motive c_1 h → motive a ⋯
⊢ ∀ {a c_1 : α} (h' : r a c_1) (h : ReflTransGen r c_1 b), motive c_1 ⋯ → motive a ⋯

Tactic:
· exact fun h1 h2 ↦ head h1 (h2.tail hbc)

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✝

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:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a b : α
h : ∀ (b : α), ¬r a b
⊢ ReflTransGen r a b ↔ b = a

Tactic:
rw [cases_head_iff]; simp [h, eq_comm]

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: ι : Type u_1
π : ι → Type u_4
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → Preorder (π i)
x y : (i : ι) → π i
i : ι
a b : π i
⊢ update x i a ≤ update y i b ↔ a ≤ b ∧ ∀ (j : ι), j ≠ i → x j ≤ y j

Tactic:
simp +contextual [update_le_iff]

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

Goal state before:
pp: x a : ℕ
hx : x ≠ 0
ha : a ≠ 0
⊢ x ^ (a - 1) = x ^ a / x

Tactic:
← Nat.pow_div (one_le_iff_ne_zero.mpr ha) (Nat.pos_iff_ne_zero.mpr hx),

Goal state after:
x a : ℕ
hx : x ≠ 0
ha : a ≠ 0
⊢ x ^ a / x ^ 1 = x ^ a / x
Module: Mathlib.Data.Nat.Init

Goal state before:
pp: case a
P : ℕ → ℕ → Prop
ha : ∀ (a : ℕ), P (a + 1) (a + 1)
hb : ∀ (b : ℕ), P 0 (b + 1)
hd : ∀ (a b : ℕ), a < b → P (a + 1) b → P a (b + 1) → P (a + 1) (b + 1)
a b : ℕ
h : a + 1 < b + 1
⊢ P (a + 1) b

Tactic:
have : a + 1 = b ∨ a + 1 < b := by lia

Goal state after:
case a
P : ℕ → ℕ → Prop
ha : ∀ (a : ℕ), P (a + 1) (a + 1)
hb : ∀ (b : ℕ), P 0 (b + 1)
hd : ∀ (a b : ℕ), a < b → P (a + 1) b → P a (b + 1) → P (a + 1) (b + 1)
a b : ℕ
h : a + 1 < b + 1
this : a + 1 = b ∨ a + 1 < b
⊢ P (a + 1) b
Module: Mathlib.Data.Nat.Init

Goal state before:
pp: a b c d e m n k : ℕ
p : ℕ → Prop
lo hi : ℕ
P : ℕ → Prop
inst✝ : DecidablePred P
⊢ (∀ (x : ℕ), x < hi - lo → P (lo + x)) ↔ ∀ (x : ℕ), lo ≤ x → x < hi → P x

Tactic:
refine ⟨fun al x hl hh ↦ ?_,
      fun al x h ↦ al _ (Nat.le_add_right _ _) (Nat.lt_sub_iff_add_lt'.1 h)⟩

Goal state after:
a b c d e m n k : ℕ
p : ℕ → Prop
lo hi : ℕ
P : ℕ → Prop
inst✝ : DecidablePred P
al : ∀ (x : ℕ), x < hi - lo → P (lo + x)
x : ℕ
hl : lo ≤ x
hh : x < hi
⊢ P x
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
a₁ a₂ : α
h_anti : Antitone f
h_fa : f a₁ = f a₂
i : α
h₁ : a₁ ≤ i
h₂ : i ≤ a₂
⊢ f i = f a₁

Tactic:
by
  apply le_antisymm
  · exact h_anti h₁
  · rw [h_fa]; exact h_anti h₂

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a b : Complementeds α
⊢ ↑a ⊓ ↑b = ⊥ ↔ a ⊓ b = ⊥

Tactic:
← coe_inf,

Goal state after:
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a b : Complementeds α
⊢ ↑(a ⊓ b) = ⊥ ↔ a ⊓ b = ⊥
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : Max α
inst✝² : LE α
inst✝¹ : LT α
inst✝ : SemilatticeSup β
f : α → β
hf_inj : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
a b c : α
ha : a ≤ c
hb : b ≤ c
⊢ a ⊔ b ≤ c

Tactic:
← le

Goal state after:
α : Type u
β : Type v
inst✝³ : Max α
inst✝² : LE α
inst✝¹ : LT α
inst✝ : SemilatticeSup β
f : α → β
hf_inj : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
a b c : α
ha : f a ≤ f c
hb : f b ≤ f c
⊢ f (a ⊔ b) ≤ f c
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
β : Type v
e : α ≃ β
inst✝ : DistribLattice β
lattice : Lattice α := e.lattice
⊢ DistribLattice α

Tactic:
apply e.injective.distribLattice

Goal state after:
case le
α : Type u
β : Type v
e : α ≃ β
inst✝ : DistribLattice β
lattice : Lattice α := ⋯
⊢ ∀ {x y : α}, e x ≤ e y ↔ x ≤ y

case lt
α : Type u
β : Type v
e : α ≃ β
inst✝ : DistribLattice β
lattice : Lattice α := ⋯
⊢ ∀ {x y : α}, e x < e y ↔ x < y

case map_sup
α : Type u
β : Type v
e : α ≃ β
inst✝ : DistribLattice β
lattice : Lattice α := ⋯
⊢ ∀ (a b : α), e (a ⊔ b) = e a ⊔ e b

case map_inf
α : Type u
β : Type v
e : α ≃ β
inst✝ : DistribLattice β
lattice : Lattice α := ⋯
⊢ ∀ (a b : α), e (a ⊓ b) = e a ⊓ e b
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: α : Type u_2
inst✝ : HeytingAlgebra α
a : α
⊢ a ≤ ⊤ᶜ ↔ a ≤ ⊥

Tactic:
rw [le_compl_iff_disjoint_right, disjoint_top, le_bot_iff]

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

Goal state before:
pp: α : Type u
x y : α
inst✝ : BooleanAlgebra α
h : x = yᶜ
⊢ IsCompl x y

Tactic:
rw [h]
    exact isCompl_compl.symm

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ a ∆ b = ⊥ ↔ a = b

Tactic:
by
  simp_rw [symmDiff, sup_eq_bot_iff, sdiff_eq_bot_iff, le_antisymm_iff]

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
simp_rw [bihimp_assoc, bihimp_left_comm]

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

Goal state before:
pp: case inr.refine_3
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
st : s.Nonempty ∧ t.Nonempty
H : s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅
⊢ s ×ˢ t ⊆ s₁ ×ˢ t₁

Tactic:
simp only [st.1.ne_empty, st.2.ne_empty, or_false] at H

Goal state after:
case inr.refine_3
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
st : s.Nonempty ∧ t.Nonempty
H : s ⊆ s₁ ∧ t ⊆ t₁
⊢ s ×ˢ t ⊆ s₁ ×ˢ t₁
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s : Set α
t : Set β
f f' : α → γ
g g' : β → δ
h : EqOn (Prod.map f g) (Prod.map f' g') (s ×ˢ t)
hs : s.Nonempty
⊢ EqOn g g' t

Tactic:
obtain ⟨x, hxs⟩ := hs
  intro x hxt
  have h' := h <| mk_mem_prod hxs hxt
  grind

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

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

Tactic:
by
  simp [offDiag, Set.Nonempty, Set.Nontrivial]

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

Goal state before:
pp: m n : ℕ
h : n.succ ≤ m
⊢ ↑m + -↑(n + 1) = ↑(m - n.succ)

Tactic:
← Int.sub_eq_add_neg,

Goal state after:
m n : ℕ
h : n.succ ≤ m
⊢ ↑m - ↑(n + 1) = ↑(m - n.succ)
Module: Mathlib.Data.Int.Init

Goal state before:
pp: m n : ℕ
h : n.succ ≤ m
⊢ ↑m - ↑(n + 1) = ↑(m - n.succ)

Tactic:
← Int.natCast_sub h

Goal state after:
m n : ℕ
h : n.succ ≤ m
⊢ ↑(m - n.succ) = ↑(m - n.succ)
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: M : Type u_4
inst✝¹ : MulOneClass M
P : Prop
inst✝ : Decidable P
a b : M
⊢ (if P then a * b else 1) = (if P then a else 1) * if P then b else 1

Tactic:
by
  by_cases h : P <;> simp [h]

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

Goal state before:
pp: M : Type u_4
inst✝¹ : MulOneClass M
P : Prop
inst✝ : Decidable P
a b : M
⊢ (if P then 1 else a * b) = (if P then 1 else a) * if P then 1 else b

Tactic:
by
  by_cases h : P <;> simp [h]

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

Goal state before:
pp: G : Type u_3
inst✝ : CommSemigroup G
a b c : G
⊢ a * b * c = a * c * b

Tactic:
by
  rw [mul_assoc, mul_comm b, mul_assoc]

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

Goal state before:
pp: case pred
G : Type u_3
inst✝ : Group G
g : G
P : G → Prop
h_one : P 1
h_mul : ∀ (a : G), P a → P (g * a)
h_inv : ∀ (a : G), P a → P (g⁻¹ * a)
n : ℕ
ih : P (g ^ (-↑n))
⊢ P (g ^ (-1) * g ^ (-↑n))

Tactic:
zpow_neg_one

Goal state after:
case pred
G : Type u_3
inst✝ : Group G
g : G
P : G → Prop
h_one : P 1
h_mul : ∀ (a : G), P a → P (g * a)
h_inv : ∀ (a : G), P a → P (g⁻¹ * a)
n : ℕ
ih : P (g ^ (-↑n))
⊢ P (g⁻¹ * g ^ (-↑n))
Module: Mathlib.Algebra.Group.Units.Defs

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
h : IsUnit a
⊢ a * ↑h.unit⁻¹ = 1

Tactic:
rw [← h.unit.mul_inv]

Goal state after:
M : Type u_1
inst✝ : Monoid M
a : M
h : IsUnit a
⊢ a * ↑h.unit⁻¹ = ↑h.unit * ↑h.unit⁻¹
Module: Mathlib.Algebra.Group.Units.Hom

Goal state before:
pp: M : Type u
N : Type v
inst✝¹ : Monoid M
inst✝ : Monoid N
f : M →* N
g : M → Nˣ
h : ∀ (x : M), ↑(g x) = f x
x : M
⊢ f x = ↑((liftRight f g h) x)

Tactic:
coe_liftRight

Goal state after:
M : Type u
N : Type v
inst✝¹ : Monoid M
inst✝ : Monoid N
f : M →* N
g : M → Nˣ
h : ∀ (x : M), ↑(g x) = f x
x : M
⊢ f x = f x
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:
rwa [mul_comm]

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

Goal state before:
pp: case inr.inr
G₀ : Type u_4
G₀' : Type u_5
inst✝⁴ : GroupWithZero G₀
inst✝³ : GroupWithZero G₀'
inst✝² : MulActionWithZero G₀ G₀'
inst✝¹ : SMulCommClass G₀ G₀' G₀'
inst✝ : IsScalarTower G₀ G₀' G₀'
c : G₀
x : G₀'
hc : c ≠ 0
hx : x ≠ 0
⊢ (c • x)⁻¹ = c⁻¹ • x⁻¹

Tactic:
refine inv_eq_of_mul_eq_one_left ?_

Goal state after:
case inr.inr
G₀ : Type u_4
G₀' : Type u_5
inst✝⁴ : GroupWithZero G₀
inst✝³ : GroupWithZero G₀'
inst✝² : MulActionWithZero G₀ G₀'
inst✝¹ : SMulCommClass G₀ G₀' G₀'
inst✝ : IsScalarTower G₀ G₀' G₀'
c : G₀
x : G₀'
hc : c ≠ 0
hx : x ≠ 0
⊢ c⁻¹ • x⁻¹ * c • x = 1
Module: Mathlib.Algebra.Group.Int.Defs

Goal state before:
pp: n : ℕ
x : ℤ
⊢ ↑n * x + 1 * x = ↑n * x + x

Tactic:
Int.one_mul

Goal state after:
n : ℕ
x : ℤ
⊢ ↑n * x + x = ↑n * x + x
Module: Mathlib.Data.Nat.Sqrt

Goal state before:
pp: m n : ℕ
⊢ m ≤ n.sqrt ↔ m ^ 2 ≤ n

Tactic:
by simpa only [Nat.pow_two] using le_sqrt

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
x✝² : NonAssocSemiring α
x✝¹ : NonAssocSemiring β
x✝ : NonAssocSemiring γ
n : ℕ
f : α →+* α
⊢ (⇑f)^[n] = ⇑(npowRec n f)

Tactic:
by induction n <;> simp [npowRec, *]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Semiconj

Goal state before:
pp: G₀ : Type u_1
inst✝ : MulZeroClass G₀
a : G₀
⊢ SemiconjBy a 0 0

Tactic:
by
  simp only [SemiconjBy, mul_zero, zero_mul]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Semiconj

Goal state before:
pp: G₀ : Type u_1
inst✝ : MulZeroClass G₀
x y : G₀
⊢ SemiconjBy 0 x y

Tactic:
by
  simp only [SemiconjBy, mul_zero, zero_mul]

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

Goal state before:
pp: M₀ : Type u_2
inst✝ : MonoidWithZero M₀
u : M₀ˣ
a : M₀
h : a * ↑u = 0
⊢ a = 0

Tactic:
simpa using mul_eq_zero_of_left h ↑u⁻¹

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

Goal state before:
pp: case inr.inr
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
a b : M₀
h : IsUnit a ∨ IsUnit b
ha : IsUnit a
hb : IsUnit b
⊢ (a * b)⁻¹ʳ = b⁻¹ʳ * a⁻¹ʳ

Tactic:
simp [Ring.inverse_of_isUnit, ha, hb, ha.mul hb, ← Units.val_mul, ← mul_inv_rev]
    simp

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

Goal state before:
pp: n : ℕ
⊢ ∃ k, n = 2 * k ∨ n = 2 * k + 1

Tactic:
simpa only [← two_mul, exists_or, Odd, Even] using even_or_odd n

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

Goal state before:
pp: α : Type u
inst✝³ : Group α
inst✝² : LT α
inst✝¹ : MulLeftStrictMono α
a b : α
inst✝ : MulRightStrictMono α
⊢ a⁻¹ < b⁻¹ ↔ b < a

Tactic:
by
  rw [← mul_lt_mul_iff_left a, ← mul_lt_mul_iff_right b]
  simp

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

Goal state before:
pp: α : Type u_1
inst✝³ : Mul α
inst✝² : LinearOrder α
a b c d : α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
h : a * b < c * d
⊢ min a b < max c d

Tactic:
simp_rw [min_lt_iff, lt_max_iff]; contrapose! h; exact mul_le_mul' h.1.1 h.2.2

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

Goal state before:
pp: α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : LinearOrder α
hmul : ∀ (a b c : α), b < c → a * b < a * c
a b : α
h : a ≤ b
c : α
⊢ a * c ≤ b * c

Tactic:
by
    obtain rfl | h := eq_or_lt_of_le h
    · simp
    · simpa [mul_comm] using (hmul _ _ _ h).le

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

Goal state before:

Tactic:
0 ≤ b ^ 2 := pow_succ_nonneg hb.le _
    _ = b ^ 2 + a * (a + b) := by rw [← hab, mul_zero, add_zero]
    _ = a ^ 2 + (a + b) * b := by rw [add_mul, mul_add, sq, sq, add_comm, add_assoc]
    _ = a ^ 2 := by rw [← hab, zero_mul, add_zero]

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

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ a ≤ b / c * c ↔ a ≤ b

Tactic:
div_mul_cancel₀ _ hc.ne'

Goal state after:
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ a ≤ b ↔ a ≤ b
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ a < b / c * c ↔ a < b

Tactic:
div_mul_cancel₀ _ hc.ne'

Goal state after:
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ a < b ↔ a < b
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b : G₀
hb : 0 < b
⊢ 1 < a / b ↔ b < a

Tactic:
rw [lt_div_iff₀ hb, one_mul]

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

Goal state before:
pp: R : Type u
inst✝⁵ : Ring R
inst✝⁴ : LinearOrder R
a b : R
inst✝³ : MulPosStrictMono R
inst✝² : PosMulStrictMono R
inst✝¹ : AddLeftReflectLE R
inst✝ : AddLeftMono R
⊢ 0 ≤ a ∧ 0 ≤ -b ∨ a ≤ 0 ∧ -b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b

Tactic:
neg_nonneg,

Goal state after:
R : Type u
inst✝⁵ : Ring R
inst✝⁴ : LinearOrder R
a b : R
inst✝³ : MulPosStrictMono R
inst✝² : PosMulStrictMono R
inst✝¹ : AddLeftReflectLE R
inst✝ : AddLeftMono R
⊢ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ -b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
Module: Mathlib.Data.Nat.Cast.Order.Basic

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

Tactic:
by
  apply zero_lt_one.trans_le
  convert! (@mono_cast α _).imp (?_ : 1 ≤ n + 1)
  <;> simp

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs

Goal state before:
pp: α : Type u
inst✝³ : MulOneClass α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedMul α
a b : α
inst✝ : MulLeftStrictMono α
c : α
⊢ a ≠ b ∧ b = a * c ↔ c > 1 ∧ b = a * c

Tactic:
and_congr_left_iff,

Goal state after:
α : Type u
inst✝³ : MulOneClass α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedMul α
a b : α
inst✝ : MulLeftStrictMono α
c : α
⊢ b = a * c → (a ≠ b ↔ c > 1)
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
⊢ a ^ m = b ^ n ↔ ∃ c, a = c ^ n ∧ b = c ^ m

Tactic:
refine ⟨fun h ↦ ?_, by rintro ⟨c, rfl, rfl⟩; rw [← pow_mul, ← pow_mul']⟩

Goal state after:
α : Type u_1
inst✝ : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
⊢ ∃ c, a = c ^ n ∧ b = c ^ m
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:
rwa [mul_comm]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: G₀ : Type u_1
M₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : MulZeroOneClass M₀
inst✝ : Nontrivial M₀
f : G₀ →*₀ M₀
x : G₀ˣ
hx : ↑x ≠ 0
H : f ↑x = 0
⊢ f 1 = 0

Tactic:
← Units.mul_inv x,

Goal state after:
G₀ : Type u_1
M₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : MulZeroOneClass M₀
inst✝ : Nontrivial M₀
f : G₀ →*₀ M₀
x : G₀ˣ
hx : ↑x ≠ 0
H : f ↑x = 0
⊢ f (↑x * ↑x⁻¹) = 0
Module: Mathlib.Data.Nat.Cast.Order.Ring

Goal state before:
pp: case inr
α : Type u_2
inst✝⁶ : CommSemiring α
inst✝⁵ : PartialOrder α
inst✝⁴ : IsOrderedRing α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : AddLeftReflectLE α
m n : ℕ
h : n ≤ m
⊢ ↑(m - n) = ↑m - ↑n

Tactic:
rcases le_iff_exists_add'.mp h with ⟨m, rfl⟩

Goal state after:
case inr
α : Type u_2
inst✝⁶ : CommSemiring α
inst✝⁵ : PartialOrder α
inst✝⁴ : IsOrderedRing α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : AddLeftReflectLE α
n m : ℕ
h : n ≤ m + n
⊢ ↑(m + n - n) = ↑(m + n) - ↑n
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
a b : R
⊢ a + b ≤ ↑⌈a⌉₊ + ↑⌈b⌉₊

Tactic:
gcongr <;> apply le_ceil

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
x y : AddUnits R
⊢ ↑(-x) * ↑y = ↑x * ↑(-y)

Tactic:
rw [← neg_eq_val_neg, ← val_neg_mulRight]

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
x y : AddUnits R
⊢ ↑(-x.mulRight ↑y) = ↑x * ↑(-y)
Module: Mathlib.Algebra.GroupWithZero.Units.Lemmas

Goal state before:
pp: case neg
G₀ : Type u_3
G₀' : Type u_5
F : Type u_6
inst✝³ : GroupWithZero G₀
inst✝² : GroupWithZero G₀'
inst✝¹ : FunLike F G₀ G₀'
inst✝ : MonoidWithZeroHomClass F G₀ G₀'
f : F
a : G₀
h : ¬a = 0
⊢ f a⁻¹ * f a = 1

Tactic:
rw [← map_mul, inv_mul_cancel₀ h, map_one]

Goal state after:
Module: Mathlib.Algebra.Ring.Divisibility.Basic

Goal state before:
pp: α : Type u_1
inst✝ : NonUnitalRing α
a b c : α
h : a ∣ b
⊢ a ∣ c + b ↔ a ∣ c

Tactic:
exact dvd_add_left h

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

Goal state before:
pp: case pos
K : Type u_1
L : Type u_2
inst✝ : Field K
a : K
n : ℕ
h : a = 0
⊢ a ^ (↑n + 1) = a ^ ↑n * a

Tactic:
rw [← Int.natCast_add_one, zpow_natCast, zpow_natCast, pow_succ]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f₁ f₂ : α → β
inst✝¹ : Preorder α
inst✝ : Preorder β
h₁ : MonotoneOn f₁ s
h : EqOn f₁ f₂ s
⊢ MonotoneOn f₂ s

Tactic:
intro a ha b hb hab

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
f₁ f₂ : α → β
inst✝¹ : Preorder α
inst✝ : Preorder β
h₁ : MonotoneOn f₁ s
h : EqOn f₁ f₂ s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a ≤ b
⊢ f₂ a ≤ f₂ b
Module: Mathlib.Data.Set.Monotone

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f₁ f₂ : α → β
inst✝¹ : Preorder α
inst✝ : Preorder β
h₁ : StrictMonoOn f₁ s
h : EqOn f₁ f₂ s
⊢ StrictMonoOn f₂ s

Tactic:
intro a ha b hb hab

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
f₁ f₂ : α → β
inst✝¹ : Preorder α
inst✝ : Preorder β
h₁ : StrictMonoOn f₁ s
h : EqOn f₁ f₂ s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a < b
⊢ f₂ a < f₂ b
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: case inl
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
n : ℤ
a : α
n0 : 0 ≤ n
⊢ |a ^ n|ₘ = |a|ₘ ^ |n|

Tactic:
obtain ⟨n, rfl⟩ := Int.eq_ofNat_of_zero_le n0

Goal state after:
case inl
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
a : α
n : ℕ
n0 : 0 ≤ ↑n
⊢ |a ^ ↑n|ₘ = |a|ₘ ^ |↑n|
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝² : Semifield α
inst✝¹ : PartialOrder α
inst✝ : PosMulReflectLT α
a b : α
hb : 0 < b
⊢ 1 < a / b ↔ b < a

Tactic:
rw [lt_div_iff₀ hb, one_mul]

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

Goal state before:
pp: α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
⊢ 1 ≤ a / b ↔ 0 < b ∧ b ≤ a ∨ b < 0 ∧ a ≤ b

Tactic:
rcases lt_trichotomy b 0 with (hb | rfl | hb)
  · simp [hb, hb.not_gt, one_le_div_of_neg]
  · simp [zero_lt_one.not_ge]
  · simp [hb, hb.not_gt, one_le_div]

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

Goal state before:
pp: case inr
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
B ε : α
hε : 0 < ε
n : ℕ
this : ∀ (B : α), 0 < B → ∃ δ > 0, ∀ (q r : α), |r| ≤ B → |q - r| ≤ δ → |q ^ n - r ^ n| < ε
B_pos : B ≤ 0
⊢ ∃ δ > 0, ∀ (q r : α), |r| ≤ B → |q - r| ≤ δ → |q ^ n - r ^ n| < ε

Tactic:
have ⟨δ, δ_pos, cont⟩ := this 1 zero_lt_one

Goal state after:
case inr
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
B ε : α
hε : 0 < ε
n : ℕ
this : ∀ (B : α), 0 < B → ∃ δ > 0, ∀ (q r : α), |r| ≤ B → |q - r| ≤ δ → |q ^ n - r ^ n| < ε
B_pos : B ≤ 0
δ : α
δ_pos : δ > 0
cont : ∀ (q r : α), |r| ≤ 1 → |q - r| ≤ δ → |q ^ n - r ^ n| < ε
⊢ ∃ δ > 0, ∀ (q r : α), |r| ≤ B → |q - r| ≤ δ → |q ^ n - r ^ n| < ε
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
β : Type v
l₁ l₂ : List α
f : α → β
h : Injective f
⊢ map f l₁ ⊆ map f l₂ → l₁ ⊆ l₂

Tactic:
intro h2

Goal state after:
α : Type u
β : Type v
l₁ l₂ : List α
f : α → β
h : Injective f
h2 : map f l₁ ⊆ map f l₂
⊢ l₁ ⊆ l₂
Module: Mathlib.Data.List.Basic

Goal state before:
pp: ι : Type u_1
α : Type u
β : Type v
γ : Type w
l✝ l₁ l₂ l : List α
i j : ℕ
h : i ≠ j
a : α
hj : j < (l.set i a).length
⊢ j < l.length

Tactic:
by simpa using hj

Goal state after: