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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a : G
⊢ a * a⁻¹ = 1

Tactic:
mul_inv_cancel a

Goal state after:
G : Type u_1
inst✝ : Group G
a : G
⊢ 1 = 1
Module: Mathlib.Algebra.Group.Defs

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

Tactic:
mul_inv_cancel_right a b

Goal state after:
G : Type u_1
inst✝ : Group G
a b : G
⊢ a = a
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u
β : α → Sort v
inst✝ : DecidableEq α
f : (a : α) → β a
a : α
b : β a
⊢ update f a b = f ↔ b = f a

Tactic:
by simp [update_eq_iff]

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

Goal state before:
pp: α : Sort u
β : Sort v
f : α ≃ β
g : β ≃ α
⊢ f.trans g = Equiv.refl α ↔ f.symm = g

Tactic:
rw [trans_eq_refl_iff_eq_symm]

Goal state after:
α : Sort u
β : Sort v
f : α ≃ β
g : β ≃ α
⊢ f = g.symm ↔ f.symm = g
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a : α
⊢ min a a = a

Tactic:
by rw [min_def, ite_id]

Goal state after:
Module: Mathlib.Lean.Meta.CongrTheorems

Goal state before:
pp: α β : Sort u
inst✝ : FastSubsingleton α
h₂ : α = β
a : α
b : β
⊢ a ≍ b

Tactic:
have : Subsingleton α := FastSubsingleton.inst
  exact Subsingleton.helim h₂ a b

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

Goal state before:
pp: case step
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Surjective next
m✝ : ℕ
hnm : n.le m✝
ih : Surjective (leRecOn hnm fun {k} ↦ next)
x : C n
⊢ leRecOn ⋯ (fun {k} ↦ next) x = next (leRecOn hnm (fun {k} ↦ next) x)

Tactic:
leRecOn_succ

Goal state after:
case step
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Surjective next
m✝ : ℕ
hnm : n.le m✝
ih : Surjective (leRecOn hnm fun {k} ↦ next)
x : C n
⊢ next (leRecOn ?step.h1 (fun {k} ↦ next) x) = next (leRecOn hnm (fun {k} ↦ next) x)

case step.h1
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Surjective next
m✝ : ℕ
hnm : n.le m✝
ih : Surjective (leRecOn hnm fun {k} ↦ next)
x : C n
⊢ n ≤ m✝
Module: Mathlib.Data.Nat.Init

Goal state before:
pp: m n : ℕ
motive : (m : ℕ) → n ≤ m → Sort u_1
refl : motive n ⋯
le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯
h1 : n ≤ m
h2 : n ≤ m + 1
| leRec refl le_succ_of_le h2 = le_succ_of_le h1 (leRec refl le_succ_of_le h1)

Tactic:
lhs
    rw [leRec, Or.by_cases, dif_pos h1]

Goal state after:
m n : ℕ
motive : (m : ℕ) → n ≤ m → Sort u_1
refl : motive n ⋯
le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯
h1 : n ≤ m
h2 : n ≤ m + 1
| le_succ_of_le h1 (leRec refl le_succ_of_le h1)
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
⊢ StrictMonoOn (⇑toDual ∘ f ∘ ⇑ofDual) s ↔ StrictMonoOn f s

Tactic:
strictMonoOn_toDual_comp_iff,

Goal state after:
α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
⊢ StrictAntiOn (f ∘ ⇑ofDual) s ↔ StrictMonoOn f s
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
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

Tactic:
· simpa [hx, hy] using hg h

Goal state after:
Module: Mathlib.Order.Disjoint

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

Tactic:
simp only [disjoint_iff, inf_sup_right, sup_eq_bot_iff]

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
inst✝ : SemilatticeSup α
a b c : α
⊢ a ⊔ (b ⊔ c) = a ⊔ (c ⊔ b)

Tactic:
sup_comm b

Goal state after:
α : Type u
inst✝ : SemilatticeSup α
a b c : α
⊢ a ⊔ (c ⊔ b) = a ⊔ (c ⊔ b)
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : SemilatticeSup α
inst✝ : Preorder β
f : α → β
h : ∀ (x y : α), f x ≤ f (x ⊔ y)
x y : α
hxy : x ≤ y
⊢ f x ≤ f y

Tactic:
rw [← sup_eq_right.2 hxy]

Goal state after:
α : Type u
β : Type v
inst✝¹ : SemilatticeSup α
inst✝ : Preorder β
f : α → β
h : ∀ (x y : α), f x ≤ f (x ⊔ y)
x y : α
hxy : x ≤ y
⊢ f x ≤ f (x ⊔ y)
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c : α
⊢ a \ (a \ b) ≤ c ⊔ b \ c

Tactic:
exact sdiff_sdiff_le.trans le_sup_sdiff

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c : α
⊢ a ∆ b ≤ c ↔ a ≤ b ⊔ c ∧ b ≤ a ⊔ c

Tactic:
simp_rw [symmDiff, sup_le_iff, sdiff_le_iff]

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

Goal state before:
pp: case mpr
α : Type u_9
inst✝ : DecidableEq α
s : Set α
i j : α
hi : i ∈ s
hj : ¬j ∈ s
a : α
⊢ a ∈ insert j s \ {i} → a ∈ Set.image (⇑(swap i j)) s

Tactic:
· rintro ⟨rfl | has, hai⟩
      · exact ⟨i, hi, swap_apply_left ..⟩
      · exact ⟨a, has, swap_apply_of_ne_of_ne hai (ne_of_mem_of_not_mem has hj)⟩

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

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.13
⊢ LeftInverse (Sum.elim (Prod.mk false) (Prod.mk true)) fun p ↦ if p.fst = true then inr p.snd else inl p.snd

Tactic:
by rintro ⟨_ | _, _⟩ <;> rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
g : β → α
b : β
s : Set α
h₁ : LeftInverse g f
h₂ : RightInverse g f
⊢ b ∈ f '' s ↔ g b ∈ s

Tactic:
rw [image_eq_preimage_of_inverse h₁ h₂, mem_preimage]

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : ¬(s = ∅ ∨ t = ∅)
⊢ s = s₁ ∧ t = t₁ ∨ False ∧ (s₁ = ∅ ∨ t₁ = ∅) ↔ s = s₁ ∧ t = t₁

Tactic:
false_and,

Goal state after:
case inr
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : ¬(s = ∅ ∨ t = ∅)
⊢ s = s₁ ∧ t = t₁ ∨ False ↔ s = s₁ ∧ t = t₁
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: ι : Type u_1
β : ι → Type u_3
inst✝ : DecidableEq ι
x : (i : ι) → β i
i : ι
s : Set (β i)
⊢ update x i '' s = univ.pi (update (fun j ↦ {x j}) i s)

Tactic:
by
  ext y
  simp only [mem_image, update_eq_iff, ne_eq, and_left_comm (a := _ ∈ s), exists_eq_left, mem_pi,
    mem_univ, true_implies]
  rw [forall_update_iff (p := fun x s => y x ∈ s)]
  simp [eq_comm]

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
F : Type u_9
inst✝¹ : Group G
inst✝ : MulOneClass M
f : M → G
map_mul : ∀ (a b : M), f (a * b) = f a * f b
⊢ f 1 = 1

Tactic:
by rw [← mul_right_cancel_iff, ← map_mul _ 1, one_mul, one_mul]

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

Goal state before:
pp: α : Type u
inst✝ : Monoid α
a✝ b u : αˣ
n : ℕ
a : αˣ
⊢ ↑a⁻¹ ^ n * ↑a ^ n = 1

Tactic:
← a.commute_inv_coe.mul_pow

Goal state after:
α : Type u
inst✝ : Monoid α
a✝ b u : αˣ
n : ℕ
a : αˣ
⊢ (↑a⁻¹ * ↑a) ^ n = 1
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
x : G₀
h : x ≠ 0
y y' : G₀
w : (fun y ↦ y * x) y = (fun y ↦ y * x) y'
⊢ y = y'

Tactic:
simpa only [mul_assoc, mul_inv_cancel₀ h, mul_one] using congr_arg (fun y => y * x⁻¹) w

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

Goal state before:
pp: case neg
M₀ : Type u_1
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a✝ b✝ x a b : G₀
ha : ¬a = 0
⊢ (a * b)⁻¹ = b⁻¹ * a⁻¹

Tactic:
by_cases hb : b = 0

Goal state after:
case pos
M₀ : Type u_1
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a✝ b✝ x a b : G₀
ha : ¬a = 0
hb : b = 0
⊢ (a * b)⁻¹ = b⁻¹ * a⁻¹

case neg
M₀ : Type u_1
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a✝ b✝ x a b : G₀
ha : ¬a = 0
hb : ¬b = 0
⊢ (a * b)⁻¹ = b⁻¹ * a⁻¹
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
n : ℕ
⊢ (a ^ (n + 1))⁻¹ = (a ^ (n + 1).succ)⁻¹ * a

Tactic:
pow_succ' _ (n + 1),

Goal state after:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
n : ℕ
⊢ (a ^ (n + 1))⁻¹ = (a * a ^ (n + 1))⁻¹ * a
Module: Mathlib.Algebra.Group.Nat.Even

Goal state before:
pp: m n : ℕ
⊢ Even (m * n) ↔ Even m ∨ Even n

Tactic:
by
  rcases mod_two_eq_zero_or_one m with h₁ | h₁ <;> rcases mod_two_eq_zero_or_one n with h₂ | h₂ <;>
    simp [even_iff, h₁, h₂, Nat.mul_mod]

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

Goal state before:
pp: case h
α : Type u_2
inst✝ : Ring α
a k : α
hk : a = 2 * k + 1
⊢ -a = -(2 * k) + (-1 + -1 + 1)

Tactic:
neg_add_cancel_right,

Goal state after:
case h
α : Type u_2
inst✝ : Ring α
a k : α
hk : a = 2 * k + 1
⊢ -a = -(2 * k) + -1
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
⊢ a ≤ max c d ∨ b ≤ max c d

Tactic:
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
⊢ a ≤ max c d ∨ b ≤ max c d

Tactic:
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.MinMax

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
inst✝² : Mul α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a₁ a₂ b₁ b₂ : α
⊢ a₂ ≤ a₁ ∧ b₂ ≤ b₁ → a₂ * b₂ ≤ a₁ * b₁

Tactic:
exact fun h => mul_le_mul' h.1 h.2

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

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

Tactic:
rcases lt_trichotomy a 0 with (ha | rfl | ha)

Goal state after:
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

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✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : IsOrderedAddMonoid R
inst✝¹ : ZeroLEOneClass R
inst✝ : Nontrivial R
mul_pos : ∀ (a b : R), 0 < a → 0 < b → 0 < a * b
a : R
ha : 0 < a
b c : R
hbc : b < c
⊢ a * b < a * c

Tactic:
simpa only [mul_sub, sub_pos] using mul_pos _ _ ha (sub_pos.2 hbc)

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

Goal state before:
pp: case inr.inl
R : Type u
inst✝³ : Semiring R
inst✝² : LinearOrder R
b : R
inst✝¹ : MulPosStrictMono R
inst✝ : PosMulStrictMono R
hab : 0 ≤ 0 * b
ab : 0 ≤ 0 → b < 0
nab : 0 ≤ 0 → 0 < b
⊢ 0 * b < 0

Tactic:
exact ((ab le_rfl).asymm (nab le_rfl)).elim

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

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

Tactic:
refine mul_nonneg_iff.trans ?_
  simp_rw [← not_le, ← or_iff_not_imp_left]
  have := le_total a 0
  have := le_total b 0
  tauto

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

Goal state before:
pp: case mpr
α : Type u_1
x✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
a : α
ac : Acc r a
⊢ Acc (Quotient.lift₂ r H) ⟦a⟧

Tactic:
induction ac with

Goal state after:
case mpr.intro
α : Type u_1
x✝¹ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
a x✝ : α
h✝ : ∀ (y : α), r y x✝ → Acc r y
IH : ∀ (y : α), r y x✝ → Acc (Quotient.lift₂ r H) ⟦y⟧
⊢ Acc (Quotient.lift₂ r H) ⟦x✝⟧
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✝ : AddLeftMono R
x : R
h : a ≤ b
⊢ (x - a) * (x - b) < 0 ↔ a < x ∧ x < b

Tactic:
rw [mul_neg_iff, sub_pos, sub_pos, sub_neg, sub_neg, or_iff_left_iff_imp, and_comm]

Goal state after:
R : Type u
inst✝⁴ : Ring R
inst✝³ : LinearOrder R
a b : R
inst✝² : MulPosStrictMono R
inst✝¹ : PosMulStrictMono R
inst✝ : AddLeftMono R
x : R
h : a ≤ b
⊢ b < x ∧ x < a → a < x ∧ x < b
Module: Mathlib.Algebra.Order.Group.Abs

Goal state before:
pp: G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
⊢ a ≤ b ∧ a⁻¹ ≤ b ↔ b⁻¹ ≤ a ∧ a ≤ b

Tactic:
and_comm,

Goal state after:
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
⊢ a⁻¹ ≤ b ∧ a ≤ b ↔ b⁻¹ ≤ a ∧ a ≤ b
Module: Mathlib.Algebra.Order.Group.Abs

Goal state before:
pp: G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b c : G
⊢ b ≤ a * c ∧ a ≤ b * c ↔ a ≤ b * c ∧ b / a ≤ c

Tactic:
and_comm,

Goal state after:
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b c : G
⊢ a ≤ b * c ∧ b ≤ a * c ↔ a ≤ b * c ∧ b / a ≤ c
Module: Mathlib.Algebra.Order.Group.Abs

Goal state before:
pp: G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b c : G
⊢ b < a * c ∧ a < b * c ↔ a < b * c ∧ b / a < c

Tactic:
and_comm,

Goal state after:
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b c : G
⊢ a < b * c ∧ b < a * c ↔ a < b * c ∧ b / a < c
Module: Mathlib.Algebra.Order.Group.Unbundled.Int

Goal state before:
pp: a : ℤ
⊢ a.sign * |a| = a

Tactic:
by
  rw [abs_eq_natAbs, sign_mul_natAbs a]

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 : α
⊢ b = a * c ∧ a ≠ b ↔ c > 1 ∧ b = a * c

Tactic:
and_comm,

Goal state after:
α : Type u
inst✝³ : MulOneClass α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedMul α
a b : α
inst✝ : MulLeftStrictMono α
c : α
⊢ a ≠ b ∧ b = a * c ↔ c > 1 ∧ b = a * c
Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs

Goal state before:
pp: case inr
α : Type u
inst✝² : Monoid α
inst✝¹ : LinearOrder α
inst✝ : CanonicallyOrderedMul α
a b c : α
hb : b ≤ a
⊢ min a (b * c) = min a (min a b * min a c)

Tactic:
rcases le_total a c with hc | hc
    · simp [hc, le_mul_left]
    · simp [hb, hc]

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

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

Tactic:
by_cases hb : b = 0

Goal state after:
case pos
α : Type u_1
inst✝ : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h✝¹ : ¬m = 0
h✝ : ¬n = 0
hb : b = 0
⊢ ∃ c, a = c ^ n ∧ b = c ^ m

case neg
α : Type u_1
inst✝ : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h✝¹ : ¬m = 0
h✝ : ¬n = 0
hb : ¬b = 0
⊢ ∃ c, a = c ^ n ∧ b = c ^ m
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 : α
ha : AddLECancellable a
h₁ : 0 < a
h₂ : 0 < b
⊢ a - b < a

Tactic:
by
  refine tsub_le_self.lt_of_ne fun h => ?_
  rw [← h, tsub_pos_iff_lt] at h₁
  exact h₂.not_ge (ha.add_le_iff_nonpos_left.1 <| add_le_of_le_tsub_left_of_le h₁.le h.ge)

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

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

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:
· rw [Nat.sub_eq_zero_of_le h, cast_zero, tsub_eq_zero_of_le]
    exact mono_cast h

Goal state after:
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
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
hn : n < 0
this : x + ↑n ≤ 1 + -1
⊢ x + ↑n ≤ 0

Tactic:
rwa [add_neg_cancel] at this

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

Goal state before:
pp: m✝ n✝ k : ℕ
p q : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
m : ℕ
IH : (y : ℕ) → y.lbp m → (∀ (n : ℕ), n < y → ¬p n) → { n // p n ∧ ∀ (m : ℕ), m < n → ¬p m }
al : ∀ (n : ℕ), n < m → ¬p n
pm : ¬p m
n : ℕ
h : n ≤ m
e : n = m
⊢ ¬p n

Tactic:
by rw [e]; exact pm

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

Goal state before:
pp: case refine_2
n : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
hₘ : ∃ m, p (m + n)
hₙ : ∃ n, p n
hn : n ≤ Nat.find hₙ
⊢ Nat.find hₙ ≤ Nat.find hₘ + n

Tactic:
· rw [← Nat.sub_le_iff_le_add]
    refine (le_find_iff _ _).2 fun m hm hpm => Nat.not_le.2 hm ?_
    rw [Nat.sub_le_iff_le_add]
    exact find_le hpm

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

Goal state before:
pp: case pos.mpr
P : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
hk : P (k + 1)
⊢ (m ≤ k + 1 ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k + 1 → ¬P n) → k + 1 = m

Tactic:
rintro ⟨hle, h0, hm⟩
        rcases Decidable.lt_or_eq_of_le hle with hlt | rfl
        exacts [(hm hlt (le_refl _) hk).elim, rfl]

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

Goal state before:
pp: case pos
m : ℕ
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
hmb : m ≤ n
hm : P m
h : findGreatest P n = 0
⊢ P (findGreatest P n)

Tactic:
cases m

Goal state after:
case pos.zero
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
h : findGreatest P n = 0
hmb : 0 ≤ n
hm : P 0
⊢ P (findGreatest P n)

case pos.succ
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
h : findGreatest P n = 0
n✝ : ℕ
hmb : n✝ + 1 ≤ n
hm : P (n✝ + 1)
⊢ P (findGreatest P n)
Module: Mathlib.Algebra.Order.Floor.Defs

Goal state before:
pp: α : Type u_2
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
z : ℤ
a : α
⊢ z ≤ ⌈a⌉ ↔ ↑z - 1 < a

Tactic:
by rw [← sub_one_lt_iff, lt_ceil]; norm_cast

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case mpr
α : Type u_1
inst✝¹ : LT α
inst✝ : NoMinOrder α
h : DenselyOrdered α
⊢ ∀ (a₁ a₂ : WithBot α), a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂

Tactic:
simpa [WithBot.exists, WithBot.forall, exists_lt] using DenselyOrdered.dense

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

Goal state before:
pp: case inr
G₀ : Type u_3
M₀' : Type u_4
F' : Type u_7
inst✝³ : GroupWithZero G₀
inst✝² : MonoidWithZero M₀'
inst✝¹ : FunLike F' G₀ M₀'
a : G₀
inst✝ : MonoidWithZeroHomClass F' G₀ M₀'
f g : F'
h : f a = g a
ha : a ≠ 0
⊢ f a⁻¹ = g a⁻¹

Tactic:
· exact (IsUnit.mk0 a ha).eq_on_inv f g h

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

Goal state before:
pp: case hbc
R : Type u_3
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
x y : R
hx : 0 ≤ x
hy : 0 ≤ y
k : ℕ
ih : k + 1 ≠ 0 → x ^ (k + 1) + y ^ (k + 1) ≤ (x + y) ^ (k + 1)
hn : k + 1 + 1 ≠ 0
n : ℕ := ⋯
h1 : 0 ≤ x * y ^ n + y * x ^ n
h2 : 0 ≤ x + y
⊢ x ^ n + y ^ n ≤ (x + y) ^ n

Tactic:
exact ih (Nat.succ_ne_zero k)

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

Goal state before:
pp: u v : ℤ
hu : IsUnit u
hv : IsUnit v
⊢ u ≠ v ↔ u = -v

Tactic:
obtain rfl | rfl := isUnit_eq_one_or hu

Goal state after:
case inl
v : ℤ
hv : IsUnit v
hu : IsUnit 1
⊢ 1 ≠ v ↔ 1 = -v

case inr
v : ℤ
hv : IsUnit v
hu : IsUnit (-1)
⊢ -1 ≠ v ↔ -1 = -v
Module: Mathlib.Order.Bounds.Image

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
Hf : Monotone f
s : Set α
⊢ f '' upperBounds s ⊆ upperBounds (f '' s)

Tactic:
rintro _ ⟨a, ha, rfl⟩
  exact Hf.mem_upperBounds_image ha

Goal state after:
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b c d : α
h : a ≤ b
⊢ Icc a b = Icc c d ↔ a = c ∧ b = d

Tactic:
by
  refine ⟨fun heq ↦ ?_, by rintro ⟨rfl, rfl⟩; rfl⟩
  have h' : c ≤ d := by
    by_contra contra; rw [Icc_eq_empty_iff.mpr contra, Icc_eq_empty_iff] at heq; contradiction
  simp only [Set.ext_iff, mem_Icc] at heq
  obtain ⟨-, h₁⟩ := (heq b).mp ⟨h, le_refl _⟩
  obtain ⟨h₂, -⟩ := (heq a).mp ⟨le_refl _, h⟩
  obtain ⟨h₃, -⟩ := (heq c).mpr ⟨le_refl _, h'⟩
  obtain ⟨-, h₄⟩ := (heq d).mpr ⟨h', le_refl _⟩
  exact ⟨le_antisymm h₃ h₂, le_antisymm h₁ h₄⟩

Goal state after:
Module: Mathlib.Tactic.NormNum.Basic

Goal state before:
pp: «$u» : Level
«$α» : Type u
«$a» «$b» : «$α»
«$inst» : Semiring «$α»
«$mα'» : AddMonoidWithOne «$α»
«$na» : ℕ
«$pa» : IsNat «$a» «$na»
«$mα» : AddMonoidWithOne «$α»
«$nb» : ℕ
«$pb» : IsNat «$b» «$nb»
⊢ AddMonoidWithOne «$α»

Tactic:
clear! mα mα'; apply AddCommMonoidWithOne.toAddMonoidWithOne

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

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b c : α
hc : c ≤ 0
h : b ≤ a
⊢ a / c ≤ b / c

Tactic:
rw [div_eq_mul_inv a c, div_eq_mul_inv b c]
  exact mul_le_mul_of_nonpos_right h (inv_nonpos'.2 hc)

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

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b c : α
hc : c < 0
h : b < a
⊢ a / c < b / c

Tactic:
rw [div_eq_mul_inv a c, div_eq_mul_inv b c]
  exact mul_lt_mul_of_neg_right h (inv_lt_zero'.2 hc)

Goal state after:
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
a✝ : α
b✝ : β
l₁✝ : List α
l₂✝ : List β
h₁ : R a✝ b✝
h₂ : Forall₂ R l₁✝ l₂✝
x : α
y : β
hx : (x, y) = (a✝, b✝) ∨ (x, y) ∈ zipWith Prod.mk l₁✝ l₂✝
⊢ R x y

Tactic:
match hx with
    | Or.inl rfl => exact h₁
    | Or.inr h₃ => exact forall₂_zip h₂ h₃

Goal state after:
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: α : Type u_1
l : List α
n : ℕ
h : n < l.length
⊢ l[n] :: l.eraseIdx n ~ l

Tactic:
simpa [h] using (set_perm_cons_eraseIdx h l[n]).symm

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

Goal state before:
pp: α : Type u
l : List α
a : α
⊢ (l ++ [a]).reverse = a :: l.reverse

Tactic:
rw [reverse_append]; rfl

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

Goal state before:
pp: α : Type u
b c : α
l₁ : List α
a : α
l₂ : List α
⊢ (b :: c :: (l₁ ++ a :: l₂)).getLast? = (a :: l₂).getLast?

Tactic:
getLast?_cons_cons,

Goal state after:
α : Type u
b c : α
l₁ : List α
a : α
l₂ : List α
⊢ (c :: (l₁ ++ a :: l₂)).getLast? = (a :: l₂).getLast?