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

Goal state before:
pp: case bit
M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
k : ℕ
b : Bool
k' : ℕ
k'0 : k' ≠ 0
ih :
  ∀ (m n : M),
    k' ≠ 0 →
      Nat.binaryRec (motive := fun x ↦ M → M → M) (fun y x ↦ y)
          (fun bn _n fn y x ↦ fn (bif bn then y * x else y) (x * x)) k' m n =
        m * npowRec' k' n
m n : M
hk : Nat.bit b k' ≠ 0
⊢ Nat.binaryRec (motive := fun x ↦ M → M → M) (fun y x ↦ y) (fun bn _n fn y x ↦ fn (bif bn then y * x else y) (x * x))
      (Nat.bit b k') m n =
    m * npowRec' (Nat.bit b k') n

Tactic:
rw [Nat.binaryRec_eq _ _ (Or.inl rfl), ih _ _ k'0]
    cases b <;> simp only [Nat.bit, cond_false, cond_true, npowRec'_two_mul]
    rw [npowRec'_succ (by lia), npowRec'_two_mul, ← npowRec'_two_mul,
      ← npowRec'_mul_comm (by lia), mul_assoc]

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

Goal state before:
pp: case neg
γ : Sort u_3
α₁ : Sort u_4
α₂ : Sort u_5
α₃ : Sort u_6
f₁₂ : α₁ → α₂
h₁₂ : Injective f₁₂
f₂₃ : α₂ → α₃
h₂₃ : Injective f₂₃
g : α₁ → γ
e' : α₃ → γ
b : α₂
h₂ : ¬∃ c, f₁₂ c = b
⊢ extend (f₂₃ ∘ f₁₂) g e' (f₂₃ b) = extend f₁₂ g (e' ∘ f₂₃) b

Tactic:
extend_apply' _ _ _ h₂,

Goal state after:
case neg
γ : Sort u_3
α₁ : Sort u_4
α₂ : Sort u_5
α₃ : Sort u_6
f₁₂ : α₁ → α₂
h₁₂ : Injective f₁₂
f₂₃ : α₂ → α₃
h₂₃ : Injective f₂₃
g : α₁ → γ
e' : α₃ → γ
b : α₂
h₂ : ¬∃ c, f₁₂ c = b
⊢ extend (f₂₃ ∘ f₁₂) g e' (f₂₃ b) = (e' ∘ f₂₃) b
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
motive : {a b : α} → TransGen r a b → Prop
a b : α
h : TransGen r a b
single : ∀ {a b : α} (h : r a b), motive ⋯
trans : ∀ {a b c : α} (h₁ : TransGen r a b) (h₂ : TransGen r b c), motive h₁ → motive h₂ → motive ⋯
⊢ motive h

Tactic:
induction h with
  | single h => exact single h
  | tail hab hbc h_ih => exact trans hab (.single hbc) h_ih (single hbc)

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
p : β → β → Prop
f : α → β
h : r ≤ (p on f)
⊢ TransGen r ≤ (TransGen p on f)

Tactic:
by
  intro a _ hab
  induction hab with
  | single hac => exact TransGen.single (h a _ hac)
  | tail _ hcd hac => exact TransGen.tail hac (h _ _ hcd)

Goal state after:
Module: Mathlib.Tactic.CongrExclamation

Goal state before:
pp: x y : Prop
p : x = y → Prop
h : ∀ (he : x ↔ y), p ⋯
he : x = y
⊢ p he

Tactic:
cases he
  exact h Iff.rfl

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

Goal state before:
pp: case isFalse
n m : Nat
h : n ≤ m
hn : ¬n = 0
⊢ (!decide (n = 0)) ≤ !decide (m = 0)

Tactic:
cases Nat.decEq m 0 with grind [Bool.le_true]

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

Goal state before:
pp: case le_succ_of_le
a b c d e m✝ n✝ k✝ : ℕ
p : ℕ → Prop
n m k : ℕ
h✝ : m ≤ k
ih :
  {motive : (m : ℕ) → m ≤ k → Sort u_1} →
    ((k_1 : ℕ) → (h : k_1 < k) → motive (k_1 + 1) h → motive k_1 ⋯) → motive k ⋯ → motive m h✝
motive : (m : ℕ) → m ≤ k + 1 → Sort u_1
of_succ : (k_1 : ℕ) → (h : k_1 < k + 1) → motive (k_1 + 1) h → motive k_1 ⋯
self : motive (k + 1) ⋯
⊢ motive m ⋯

Tactic:
apply ih (fun i hi => of_succ i (le_succ_of_le hi)) (of_succ k (lt_succ_self _) self)

Goal state after:
Module: Mathlib.Order.PropInstances

Goal state before:
pp: ι : Type u_1
α' : ι → Type u_3
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → OrderBot (α' i)
f g : (i : ι) → α' i
⊢ Disjoint f g ↔ ∀ (i : ι), Disjoint (f i) (g i)

Tactic:
classical
  constructor
  · intro h i x hf hg
    exact (update_le_iff.mp <| h (update_le_iff.mpr ⟨hf, fun _ _ => bot_le⟩)
      (update_le_iff.mpr ⟨hg, fun _ _ => bot_le⟩)).1
  · intro h x hf hg i
    apply h i (hf i) (hg i)

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

Goal state before:
pp: case neg
α : Type u
β : Type v
inst✝² : Preorder α
inst✝¹ : Preorder β
f g : α → β
hf : StrictMono f
hg : StrictMono g
p : α → Prop
inst✝ : DecidablePred p
hp : ∀ ⦃x y : α⦄, x < y → p y → p x
hfg : ∀ ⦃x y : α⦄, p x → ¬p y → x < y → f x < g y
x y : α
h : x < y
hy : ¬p y
⊢ (fun x ↦ if p x then f x else g x) x < (fun x ↦ if p x then f x else g x) y

Tactic:
by_cases hx : p x

Goal state after:
case pos
α : Type u
β : Type v
inst✝² : Preorder α
inst✝¹ : Preorder β
f g : α → β
hf : StrictMono f
hg : StrictMono g
p : α → Prop
inst✝ : DecidablePred p
hp : ∀ ⦃x y : α⦄, x < y → p y → p x
hfg : ∀ ⦃x y : α⦄, p x → ¬p y → x < y → f x < g y
x y : α
h : x < y
hy : ¬p y
hx : p x
⊢ (fun x ↦ if p x then f x else g x) x < (fun x ↦ if p x then f x else g x) y

case neg
α : Type u
β : Type v
inst✝² : Preorder α
inst✝¹ : Preorder β
f g : α → β
hf : StrictMono f
hg : StrictMono g
p : α → Prop
inst✝ : DecidablePred p
hp : ∀ ⦃x y : α⦄, x < y → p y → p x
hfg : ∀ ⦃x y : α⦄, p x → ¬p y → x < y → f x < g y
x y : α
h : x < y
hy : ¬p y
hx : ¬p x
⊢ (fun x ↦ if p x then f x else g x) x < (fun x ↦ if p x then f x else g x) y
Module: Mathlib.Data.Set.Basic

Goal state before:
pp: α : Type u
s : Set α
⊢ (s ⊆ univ ∧ ∃ a, ¬a ∈ s) ↔ sᶜ.Nonempty

Tactic:
Set.nonempty_def

Goal state after:
α : Type u
s : Set α
⊢ (s ⊆ univ ∧ ∃ a, ¬a ∈ s) ↔ ∃ x, x ∈ sᶜ
Module: Mathlib.Data.Set.Basic

Goal state before:
pp: α : Type u
s : Set α
⊢ (sᶜ ⊆ univ ∧ ∃ a, ¬a ∈ sᶜ) ↔ s.Nonempty

Tactic:
Set.nonempty_def

Goal state after:
α : Type u
s : Set α
⊢ (sᶜ ⊆ univ ∧ ∃ a, ¬a ∈ sᶜ) ↔ ∃ x, x ∈ s
Module: Mathlib.Logic.Equiv.Option

Goal state before:
pp: case none.some
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x : α
h1 : e.symm (e (some x)) = none
val✝ : β
h2 : e (some x) = some val✝
⊢ some (e.symm.removeNoneAux (e.removeNoneAux x)) = some x

Tactic:
simp at h1

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

Goal state before:
pp: case some.none
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x val✝ : α
h1 : e.symm (e none) = some val✝
h2 : e (some x) = none
⊢ some (e.symm.removeNoneAux (e.removeNoneAux x)) = some x

Tactic:
simp at h1

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

Goal state before:
pp: α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ x \ y ⊓ y \ x = x \ y ⊓ y \ x

Tactic:
rw [inf_of_le_right sdiff_le']

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

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
h : x ≤ y ∧ Disjoint x z
⊢ x ≤ y \ z

Tactic:
← h.2.sdiff_eq_left

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
h : x ≤ y ∧ Disjoint x z
⊢ x \ z ≤ y \ z
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hi : Disjoint x z
hs : x ⊔ z = y
h : y ⊓ x = x
⊢ y ⊓ x ⊔ z = y

Tactic:
by rw [h, hs]

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

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
h : y \ x = y \ z
⊢ y ⊓ x ⊔ y \ x = y ⊓ z ⊔ y \ x

Tactic:
by rw [sup_inf_sdiff, h, sup_inf_sdiff]

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

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
α : Type ?u.19
β : Type ?u.18
γ : Type ?u.21
δ : Type ?u.20
x : (α ⊕ β) ⊕ γ ⊕ δ
⊢ (⇑(sumAssoc (α ⊕ β) γ δ) ∘
        Sum.map (⇑(sumAssoc α β γ).symm) id ∘
          Sum.map (Sum.map id ⇑(sumComm β γ).symm) id ∘ Sum.map (⇑(sumAssoc α γ β)) id ∘ ⇑(sumAssoc (α ⊕ γ) β δ).symm)
      ((⇑(sumAssoc (α ⊕ γ) β δ) ∘
          Sum.map (⇑(sumAssoc α γ β).symm) id ∘
            Sum.map (Sum.map id ⇑(sumComm β γ)) id ∘ Sum.map (⇑(sumAssoc α β γ)) id ∘ ⇑(sumAssoc (α ⊕ β) γ δ).symm)
        x) =
    x

Tactic:
by rcases x with ((a | b) | (c | d)) <;> simp

Goal state after:
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
n : ℕ
⊢ Sum.elim succ (fun x ↦ 0) ((fun n ↦ Nat.casesOn n (inr PUnit.unit) inl) n) = n

Tactic:
cases n <;> rfl

Goal state after:
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
β : α → Sort v
p : (a : α) → β a → Prop
⊢ LeftInverse (fun f ↦ ⟨fun a ↦ ↑(f a), ⋯⟩) fun f a ↦ ⟨↑f a, ⋯⟩

Tactic:
rintro ⟨f, h⟩

Goal state after:
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
β : α → Sort v
p : (a : α) → β a → Prop
f : (a : α) → β a
h : ∀ (a : α), p a (f a)
⊢ (fun f ↦ ⟨fun a ↦ ↑(f a), ⋯⟩) ((fun f a ↦ ⟨↑f a, ⋯⟩) ⟨f, h⟩) = ⟨f, h⟩
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b : α
⊢ a \ a ∆ b = a ⊓ b

Tactic:
simp [sdiff_symmDiff]

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
simp_rw [symmDiff, compl_sup_distrib, compl_sdiff, bihimp, inf_comm]

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

Goal state before:
pp: α : Type u_1
s : Set α
f : α → α
h : MapsTo f s s
x : ↑s
k : ℕ
⊢ ↑((restrict f s s h)^[k] x) = f^[k] ↑x

Tactic:
induction k with
  | zero => simp
  | succ k ih => simp only [iterate_succ', comp_apply, val_restrict_apply, ih]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f f' g : α → β
t : Set α
⊢ EqOn (s.piecewise f f') g t ↔ EqOn f g (t ∩ s) ∧ EqOn f' g (t ∩ sᶜ)

Tactic:
simp only [EqOn, ← forall_and]

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f f' g : α → β
t : Set α
⊢ (∀ ⦃x : α⦄, x ∈ t → s.piecewise f f' x = g x) ↔ ∀ (x : α), (x ∈ t ∩ s → f x = g x) ∧ (x ∈ t ∩ sᶜ → f' x = g x)
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
⊢ ⊤ ⊆ range Sum.inl ⊔ range Sum.inr

Tactic:
by rintro (x | y) - <;> [left; right] <;> exact mem_range_self _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
p : α → Prop
q : β → Prop
f : α → β
h : ∀ (x : α), p x → q (f x)
⊢ range (Subtype.map f h) = Subtype.val ⁻¹' f '' {x | p x}

Tactic:
ext ⟨x, hx⟩

Goal state after:
α : Type u_1
β : Type u_2
p : α → Prop
q : β → Prop
f : α → β
h : ∀ (x : α), p x → q (f x)
x : β
hx : q x
⊢ ⟨x, hx⟩ ∈ range (Subtype.map f h) ↔ ⟨x, hx⟩ ∈ Subtype.val ⁻¹' f '' {x | p x}
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
s t : Set α
h : s ⊆ t
⊢ range (inclusion h) = {x | ↑x ∈ s}

Tactic:
ext ⟨x, hx⟩

Goal state after:
α : Type u_1
s t : Set α
h : s ⊆ t
x : α
hx : x ∈ t
⊢ ⟨x, hx⟩ ∈ range (inclusion h) ↔ ⟨x, hx⟩ ∈ {x | ↑x ∈ s}
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
inst✝ : DecidableEq ι
a : (i : ι) → α i
i : ι
b : α i
ha : a ∈ s.pi t
⊢ update a i b ∈ s.pi t ↔ i ∈ s → b ∈ t i

Tactic:
by
  rw [update_mem_pi_iff, and_iff_right]
  exact fun j hj => ha j hj.1

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Nonempty α
f : α → β
s : Set α
⊢ InjOn (invFunOn f s) (f '' s)

Tactic:
by
  rintro _ ⟨x, hx, rfl⟩ _ ⟨x', hx', rfl⟩ he
  rw [← invFunOn_apply_eq (f := f) hx, he, invFunOn_apply_eq (f := f) hx']

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

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
G : Type u_5
H : Type u_6
F : Type u_7
inst✝¹ : MulOneClass M
inst✝ : CommMonoid N
f g : M →* N
x y : M
⊢ f (x * y) * g (x * y) = f x * g x * (f y * g y)

Tactic:
by
        rw [f.map_mul, g.map_mul, ← mul_assoc, ← mul_assoc, mul_right_comm (f x)]

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a b : G
h : a = b
⊢ b / b = 1

Tactic:
div_self'

Goal state after:
G : Type u_3
inst✝ : Group G
a b : G
h : a = b
⊢ 1 = 1
Module: Mathlib.Algebra.Group.Units.Defs

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
n : ℕ
⊢ IsUnit a → IsUnit (a ^ n)

Tactic:
rintro ⟨u, rfl⟩

Goal state after:
M : Type u_1
inst✝ : Monoid M
n : ℕ
u : Mˣ
⊢ IsUnit (↑u ^ n)
Module: Mathlib.Algebra.Group.Units.Defs

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
a : M
inst✝ : Subsingleton Mˣ
⊢ IsUnit a → a = 1

Tactic:
rintro ⟨u, rfl⟩

Goal state after:
M : Type u_1
inst✝¹ : Monoid M
inst✝ : Subsingleton Mˣ
u : Mˣ
⊢ ↑u = 1
Module: Mathlib.Algebra.Group.Units.Defs

Goal state before:
pp: α : Type u
inst✝ : DivisionMonoid α
a : α
⊢ IsUnit a → a⁻¹ * a = 1

Tactic:
rintro ⟨u, rfl⟩

Goal state after:
α : Type u
inst✝ : DivisionMonoid α
u : αˣ
⊢ (↑u)⁻¹ * ↑u = 1
Module: Mathlib.Algebra.Group.Units.Defs

Goal state before:
pp: α : Type u
inst✝ : DivisionMonoid α
a : α
⊢ IsUnit a → a * a⁻¹ = 1

Tactic:
rintro ⟨u, rfl⟩

Goal state after:
α : Type u
inst✝ : DivisionMonoid α
u : αˣ
⊢ ↑u * (↑u)⁻¹ = 1
Module: Mathlib.Algebra.Group.End

Goal state before:
pp: α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
f : Perm α
h₁ : ∀ (x : α), p (f x) ↔ p x
h₂ : ∀ (x : α), f x ≠ x → p x
x : α
⊢ (ofSubtype (f.subtypePerm h₁)) x = f x

Tactic:
by_cases hx : p x

Goal state after:
case pos
α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
f : Perm α
h₁ : ∀ (x : α), p (f x) ↔ p x
h₂ : ∀ (x : α), f x ≠ x → p x
x : α
hx : p x
⊢ (ofSubtype (f.subtypePerm h₁)) x = f x

case neg
α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
f : Perm α
h₁ : ∀ (x : α), p (f x) ↔ p x
h₂ : ∀ (x : α), f x ≠ x → p x
x : α
hx : ¬p x
⊢ (ofSubtype (f.subtypePerm h₁)) x = f x
Module: Mathlib.Algebra.Group.End

Goal state before:
pp: M : Type u_2
inst✝ : Mul M
e : MulAut M
m : M
⊢ e⁻¹ m = (MulEquiv.symm e) m

Tactic:
rw [inv_def]

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

Goal state before:
pp: x : ℕ
x✝ : ∃ n, n * n = x
n : ℕ
hn : n * n = x
⊢ x.sqrt * x.sqrt = x

Tactic:
rw [← hn, sqrt_eq]

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

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

Tactic:
rw [sign_eq_neg_one_of_neg (by lia), ← neg_add', Int.neg_nonneg]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
z : ℕ
a : M
⊢ ↑z.succ • a = ↑z • a + a

Tactic:
by simp_rw [HSMul.hSMul, SMul.smul]; simp [add_comm, add_smul]

Goal state after:
Module: Mathlib.Logic.OpClass

Goal state before:
pp: α : Sort u
β : Sort v
f : α → α → α
hc : Std.Commutative f
ha : Std.Associative f
a b c : α
⊢ f (f a b) c = f (f a c) b

Tactic:
ha.assoc,

Goal state after:
α : Sort u
β : Sort v
f : α → α → α
hc : Std.Commutative f
ha : Std.Associative f
a b c : α
⊢ f a (f b c) = f (f a c) b
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_4
f : α → α
hf : Involutive f
n : ℕ
⊢ f^[2 * n] = id

Tactic:
iterate_mul,

Goal state after:
α : Type u_4
f : α → α
hf : Involutive f
n : ℕ
⊢ f^[2]^[n] = id
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic

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

Tactic:
simp_rw [min_le_iff, le_max_iff]

Goal state after:
α : Type u_1
inst✝³ : Mul α
inst✝² : LinearOrder α
a b c d : α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightMono α
h : a * b ≤ c * d
⊢ (a ≤ c ∨ a ≤ d) ∨ b ≤ c ∨ b ≤ d
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✝ : MulRightStrictMono α
h : a * b ≤ c * d
⊢ min a b ≤ max c d

Tactic:
simp_rw [min_le_iff, le_max_iff]

Goal state after:
α : Type u_1
inst✝³ : Mul α
inst✝² : LinearOrder α
a b c d : α
inst✝¹ : MulLeftMono α
inst✝ : MulRightStrictMono α
h : a * b ≤ c * d
⊢ (a ≤ c ∨ a ≤ d) ∨ b ≤ c ∨ b ≤ d
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : LE α
inst✝² : MulOneClass α
inst✝¹ : IsMulCommutative α
inst✝ : MulLeftMono α
a b : α
ha : MulLECancellable a
⊢ a ≤ a * b ↔ 1 ≤ b

Tactic:
ha.le_mul_iff_one_le_right

Goal state after:
α : Type u_1
inst✝³ : LE α
inst✝² : MulOneClass α
inst✝¹ : IsMulCommutative α
inst✝ : MulLeftMono α
a b : α
ha : MulLECancellable a
⊢ 1 ≤ b ↔ 1 ≤ b
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : MulOneClass α
inst✝² : Zero α
a b : α
inst✝¹ : Preorder α
inst✝ : MulPosStrictMono α
hb : 0 < b
h : a < 1
⊢ a * b < b

Tactic:
by
  simpa only [one_mul] using mul_lt_mul_of_pos_right h hb

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

Goal state before:
pp: α : Type u_1
inst✝³ : MulOneClass α
inst✝² : Zero α
a b : α
inst✝¹ : Preorder α
inst✝ : MulPosStrictMono α
hb : 0 < b
h : 1 < a
⊢ b < a * b

Tactic:
by
  simpa only [one_mul] using mul_lt_mul_of_pos_right h hb

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

Goal state before:
pp: α : Sort u
β : Sort v
γ : Sort w
inst✝ : Inhabited γ
e : α ↪ β
f₁ f₂ : α → γ
h : (fun f ↦ extend (⇑e) f default) f₁ = (fun f ↦ extend (⇑e) f default) f₂
x : α
⊢ f₁ x = f₂ x

Tactic:
by simpa only [e.injective.extend_apply] using congr_fun h (e x)

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

Goal state before:
pp: α : Sort u_1
β : Sort u_2
γ : Sort u_3
δ : Sort u_4
h : α ≃ β
h' : γ ≃ δ
x : α ↪ γ
⊢ (fun f ↦ Embedding.congr h.symm h'.symm f) ((fun f ↦ Embedding.congr h h' f) x) = x

Tactic:
by
    ext
    simp

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

Goal state before:
pp: α : Sort u_1
β : Sort u_2
γ : Sort u_3
δ : Sort u_4
h : α ≃ β
h' : γ ≃ δ
x : β ↪ δ
⊢ (fun f ↦ Embedding.congr h h' f) ((fun f ↦ Embedding.congr h.symm h'.symm f) x) = x

Tactic:
by
    ext
    simp

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

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : ZeroLEOneClass G₀
ha : 1 < a
⊢ StrictMono fun n ↦ a ^ n

Tactic:
refine strictMono_int_of_lt_succ fun n ↦ ?_

Goal state after:
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : ZeroLEOneClass G₀
ha : 1 < a
n : ℤ
⊢ a ^ n < a ^ (n + 1)
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: case inr
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : LinearOrder G₀
a : G₀
inst✝¹ : PosMulStrictMono G₀
inst✝ : ZeroLEOneClass G₀
ha₀✝ : 0 ≤ a
ha₁ : a ≠ 1
n : ℤ
ha₀ : 0 < a
⊢ a ^ n = 1 ↔ n = 0

Tactic:
simpa using zpow_right_inj₀ ha₀ ha₁ (n := 0)

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : LE α
inst✝ : PartialOrder β
f : α ≃o β
x : α
y : β
hx : ∀ (x' : α), x ≤ x'
hy : ∀ (y' : β), y ≤ y'
⊢ f x ≤ y

Tactic:
rw [← f.apply_symm_apply y, f.le_iff_le]

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : LE α
inst✝ : PartialOrder β
f : α ≃o β
x : α
y : β
hx : ∀ (x' : α), x ≤ x'
hy : ∀ (y' : β), y ≤ y'
⊢ x ≤ f.symm y
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:
rw [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.Regular.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Monoid R
a b : R
ha : IsLeftRegular a
h : a * b = a
⊢ b = 1

Tactic:
← ha.eq_iff,

Goal state after:
R : Type u_1
inst✝ : Monoid R
a b : R
ha : IsLeftRegular a
h : a * b = a
⊢ a * b = a * 1
Module: Mathlib.Algebra.Regular.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Monoid R
a b : R
ha : IsRightRegular a
h : b * a = a
⊢ b = 1

Tactic:
← ha.eq_iff,

Goal state after:
R : Type u_1
inst✝ : Monoid R
a b : R
ha : IsRightRegular a
h : b * a = a
⊢ b * a = 1 * a
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 : α
hb : AddLECancellable b
h : b ≤ a
⊢ a - b + c = c + a - b

Tactic:
hb.add_tsub_assoc_of_le h,

Goal state after:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hb : AddLECancellable b
h : b ≤ a
⊢ a - b + c = c + (a - b)
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 : α
hc : AddLECancellable c
hcb : c ≤ b
⊢ a + c + (b - c) = a + b

Tactic:
by
  rw [← hc.add_tsub_assoc_of_le hcb, add_right_comm, hc.add_tsub_cancel_right]

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

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

Tactic:
tsub_eq_zero_of_le h,

Goal state after:
case inl
α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
h : a ≤ b
⊢ 0 + b = b
Module: Mathlib.Algebra.Order.Sub.Basic

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
⊢ a + (b - a) = max a b

Tactic:
rw [add_comm, max_comm, tsub_add_eq_max]

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

Goal state before:
pp: case inl
α : Type u_1
inst✝⁵ : AddCommMonoid α
inst✝⁴ : LinearOrder α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : AddLeftReflectLE α
a b : α
h : a ≤ b
⊢ a + a - (b + b) = a - b + (a - b)

Tactic:
tsub_eq_zero_of_le h,

Goal state after:
case inl
α : Type u_1
inst✝⁵ : AddCommMonoid α
inst✝⁴ : LinearOrder α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : AddLeftReflectLE α
a b : α
h : a ≤ b
⊢ a + a - (b + b) = 0 + 0
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
⊢ 0 ≤ ↑n * x + ↑n * ↑n

Tactic:
have hnx : 0 < n → 0 ≤ x + n := fun hn => by
    have := _root_.add_le_add (neg_le_of_abs_le hx) (cast_one_le_of_pos hn)
    rwa [neg_add_cancel] at this
  have hnx' : n < 0 → x + n ≤ 0 := fun hn => by
    have := _root_.add_le_add (le_of_abs_le hx) (cast_le_neg_one_of_neg hn)
    rwa [add_neg_cancel] at this
  rw [← mul_add, mul_nonneg_iff]
  rcases lt_trichotomy n 0 with (h | rfl | h)
  · exact Or.inr ⟨mod_cast h.le, hnx' h⟩
  · simp [le_total 0 x]
  · exact Or.inl ⟨mod_cast h.le, hnx h⟩

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

Goal state before:
pp: case refine_3.inl
α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
x✝ : Nontrivial αˣ ∧ DenselyOrdered αˣ
H₁ : Nontrivial αˣ
H₂ : DenselyOrdered αˣ
y : αˣ
h : 0 < ↑y
z : αˣ
hz : 1 < z
⊢ ∃ a, 0 < a ∧ a < ↑y

Tactic:
exact ⟨(y * z⁻¹ : αˣ), by simp, Units.val_lt_val.mpr <| by simp [hz]⟩

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

Goal state before:
pp: case zero
P : ℕ → Prop
inst✝ : DecidablePred P
m : ℕ
⊢ findGreatest P 0 = m ↔ m ≤ 0 ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ 0 → ¬P n

Tactic:
rw [eq_comm, Iff.comm]
    simp only [Nat.le_zero, ne_eq, findGreatest_zero, and_iff_left_iff_imp]
    rintro rfl
    exact ⟨fun h ↦ (h rfl).elim, fun n hlt heq ↦ by lia⟩

Goal state after:
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
⊢ ⌈1⌉₊ = 1

Tactic:
rw [← Nat.cast_one, ceil_natCast]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : LT α
inst✝ : NoMinOrder α
h : DenselyOrdered (WithBot α)
a b : α
hab : a < b
⊢ ∃ a_1, a < a_1 ∧ a_1 < b

Tactic:
obtain ⟨c, hc⟩ := exists_between (WithBot.coe_lt_coe.mpr hab)

Goal state after:
case mp
α : Type u_1
inst✝¹ : LT α
inst✝ : NoMinOrder α
h : DenselyOrdered (WithBot α)
a b : α
hab : a < b
c : WithBot α
hc : ↑a < c ∧ c < ↑b
⊢ ∃ a_1, a < a_1 ∧ a_1 < b