mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁴ : Semiring R
inst✝³ : LinearOrder R
inst✝² : ExistsAddOfLE R
inst✝¹ : PosMulMono R
inst✝ : AddLeftMono R
a : R
ha : a < 0
b : R
hab : 0 = a + b
hb : 0 < b
⊢ b * b + (a * a + a * b) = a ^ 2 + (a * b + b * b)

Tactic:
sq,

Goal state after:
R : Type u
inst✝⁴ : Semiring R
inst✝³ : LinearOrder R
inst✝² : ExistsAddOfLE R
inst✝¹ : PosMulMono R
inst✝ : AddLeftMono R
a : R
ha : a < 0
b : R
hab : 0 = a + b
hb : 0 < b
⊢ b * b + (a * a + a * b) = a * a + (a * b + b * b)
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : LinearOrder G₀
a : G₀
inst✝¹ : PosMulStrictMono G₀
inst✝ : ZeroLEOneClass G₀
ha₀ : 0 < a
ha₁ : a ≠ 1
⊢ Injective fun n ↦ a ^ n

Tactic:
by
  obtain ha₁ | ha₁ := ha₁.lt_or_gt
  · exact (zpow_right_strictAnti₀ ha₀ ha₁).injective
  · exact (zpow_right_strictMono₀ ha₁).injective

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
x✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
a✝ b✝ : α
⊢ (Embedding.quotientOut α) ⟦a✝⟧ ≈ a✝

Tactic:
apply Quotient.mk_out

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
x✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
a✝ b✝ : α
⊢ (Embedding.quotientOut α) ⟦b✝⟧ ≈ b✝

Tactic:
apply Quotient.mk_out

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

Goal state before:
pp: G₀ : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ b * c⁻¹ < a ↔ b < c * a

Tactic:
rw [mul_inv_lt_iff₀ hc, mul_comm]

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

Goal state before:
pp: α : Type u_1
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
a : α
⊢ 1 < |a|ₘ ↔ a ≠ 1

Tactic:
by
  obtain ha | rfl | ha := lt_trichotomy a 1
  · simp [mabs_of_lt_one ha, ha.ne, ha]
  · simp
  · simp [mabs_of_one_lt ha, ha, ha.ne']

Goal state after:
Module: Mathlib.Algebra.Order.Group.Nat

Goal state before:
pp: ⊢ OrderedSub ℕ

Tactic:
refine ⟨fun m n k ↦ ?_⟩
  induction n generalizing k with
  | zero => simp
  | succ n ih => simp only [sub_succ, pred_le_iff, ih, succ_add, add_succ]

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

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

Tactic:
exact (findGreatest_eq_iff.1 rfl).2.1 h

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

Goal state before:
pp: α : Type u_2
inst✝² : Semiring α
inst✝¹ : PartialOrder α
inst✝ : FloorSemiring α
⊢ StrictMono Nat.cast

Tactic:
refine strictMono_nat_of_lt_succ fun n => (natCast_mono (Nat.le_succ n)).lt_of_ne fun hn => ?_
  replace hn (k : ℕ) : ((n + k : ℕ) : α) = n := by
    induction k with | zero => rfl | succ k k_ih => grind
  have h : n + (floor (n : α) + 1) ≤ floor (n : α) := (gc_floor (natCast_nonneg n)).mpr (hn _).le
  grind

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
a : R
ha : 0 ≤ a
x✝ : ℕ
⊢ x✝ ∈ Nat.cast ⁻¹' Iic a ↔ x✝ ∈ Iic ⌊a⌋₊

Tactic:
simp [le_floor_iff, ha]

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

Goal state before:
pp: case inl
M : Type u_1
G₀ : Type u_3
F : Type u_6
inst✝³ : Monoid M
inst✝² : GroupWithZero G₀
inst✝¹ : FunLike F G₀ M
inst✝ : MonoidHomClass F G₀ M
f : F
hf : ∃ x, f x ≠ 1
h : IsUnit (f 0)
⊢ IsUnit 0

Tactic:
obtain ⟨t, ht⟩ := hf

Goal state after:
case inl
M : Type u_1
G₀ : Type u_3
F : Type u_6
inst✝³ : Monoid M
inst✝² : GroupWithZero G₀
inst✝¹ : FunLike F G₀ M
inst✝ : MonoidHomClass F G₀ M
f : F
h : IsUnit (f 0)
t : G₀
ht : f t ≠ 1
⊢ IsUnit 0
Module: Mathlib.Algebra.Field.Basic

Goal state before:
pp: K : Type u_1
inst✝ : DivisionRing K
a b : K
h : b ≠ 0
⊢ (a - b) / b = a / b - 1

Tactic:
by
  simpa only [← @div_self _ _ b h] using (div_sub_div_same a b b).symm

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

Goal state before:
pp: R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Odd n
⊢ StrictMono fun a ↦ a ^ n

Tactic:
have hn₀ : n ≠ 0 := by rintro rfl; simp [Odd] at hn

Goal state after:
R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
⊢ StrictMono fun a ↦ a ^ n
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: α : Type u_1
inst✝¹ : CommRing α
inst✝ : LinearOrder α
a b : α
⊢ |a - b| * |a - b| = a * a + b * b - (1 + 1) * a * b

Tactic:
rw [abs_mul_abs_self]

Goal state after:
α : Type u_1
inst✝¹ : CommRing α
inst✝ : LinearOrder α
a b : α
⊢ (a - b) * (a - b) = a * a + b * b - (1 + 1) * a * b
Module: Mathlib.Order.WellFounded

Goal state before:
pp: α : Type u_1
r : α → α → Prop
h : ∀ (s : Set α), s.Nonempty → ∃ m, m ∈ s ∧ ∀ (x : α), x ∈ s → ¬r x m
x : α
hx : ¬Acc r x
m : α
hm : m ∈ {x | ¬Acc r x}
hm' : ∀ (x : α), x ∈ {x | ¬Acc r x} → ¬r x m
y : α
hy : r y m
hy' : ¬Acc r y
⊢ False

Tactic:
exact hm' y hy' hy

Goal state after:
Module: Mathlib.Order.WellFounded

Goal state before:
pp: case inr.inr
β : Type u_2
γ : Type u_3
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : WellFoundedLT β
f : β → γ
hf : f ∈ {f | StrictMono f}
g : β → γ
hg : g ∈ {f | StrictMono f}
hfg : range f = range g
a✝ a : β
IH : ∀ (y : β), y < a → f y = g y
b : β
hb : g b = f a
h : a < b
c : β
hc : f c = g a
this : g a < g b
⊢ f a = g a

Tactic:
rw [hb, ← hc, hf.lt_iff_lt] at this

Goal state after:
case inr.inr
β : Type u_2
γ : Type u_3
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : WellFoundedLT β
f : β → γ
hf : f ∈ {f | StrictMono f}
g : β → γ
hg : g ∈ {f | StrictMono f}
hfg : range f = range g
a✝ a : β
IH : ∀ (y : β), y < a → f y = g y
b : β
hb : g b = f a
h : a < b
c : β
hc : f c = g a
this : c < a
⊢ f a = g a
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a < b
⊢ insert a (Ioo a b) = Ico a b

Tactic:
by
  rw [insert_eq, union_comm, Ioo_union_left h]

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

Goal state before:
pp: γ : Type u_3
inst✝¹ : SemilatticeSup γ
inst✝ : DenselyOrdered γ
a b : γ
h : a < b
x : γ
hx : x ∈ lowerBounds (Ioo a b)
h₂ : a < x ⊔ a
y : γ
lty : a < y
ylt : y < x ⊔ a
u : γ
au : a < u
ub : u < b
⊢ x ≤ b

Tactic:
apply (hx ⟨au, ub⟩).trans ub.le

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Defs

Goal state before:
pp: case pos
M : Type u_2
inst✝ : MulOneClass M
l✝ : List M
p : M → Prop
hom : ∀ (a b : M), p a → p b → p (a * b)
a : M
l : List M
ih : l ≠ [] → (∀ (x : M), x ∈ l → p x) → p l.prod
hl : a :: l ≠ []
base : ∀ (x : M), x ∈ a :: l → p x
hl_empty : l = []
⊢ p (a :: l).prod

pp: case neg
M : Type u_2
inst✝ : MulOneClass M
l✝ : List M
p : M → Prop
hom : ∀ (a b : M), p a → p b → p (a * b)
a : M
l : List M
ih : l ≠ [] → (∀ (x : M), x ∈ l → p x) → p l.prod
hl : a :: l ≠ []
base : ∀ (x : M), x ∈ a :: l → p x
hl_empty : ¬l = []
⊢ p (a :: l).prod

Tactic:
· simp [*]

Goal state after:
case neg
M : Type u_2
inst✝ : MulOneClass M
l✝ : List M
p : M → Prop
hom : ∀ (a b : M), p a → p b → p (a * b)
a : M
l : List M
ih : l ≠ [] → (∀ (x : M), x ∈ l → p x) → p l.prod
hl : a :: l ≠ []
base : ∀ (x : M), x ∈ a :: l → p x
hl_empty : ¬l = []
⊢ p (a :: l).prod
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
⊢ a < b / c ↔ b < a * c

Tactic:
lt_div_iff_of_neg hc

Goal state after:
α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b c : α
hc : c < 0
⊢ b < a * c ↔ b < a * c
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: case inr
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : α
hc : a * b < c
hb : 0 < b
⊢ ∃ a' > a, a' * b < c

Tactic:
obtain ⟨a', ha', hc'⟩ := exists_between ((lt_div_iff₀ hb).2 hc)
    exact ⟨a', ha', (lt_div_iff₀ hb).1 hc'⟩

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

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

Tactic:
by
  rw [← insertIdx_eraseIdx_self (Nat.ne_of_lt h)]
  apply perm_insertIdx
  rw [length_eraseIdx_of_lt h]
  exact Nat.le_sub_one_of_lt h

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

Goal state before:
pp: case inl
α : Type u_1
l₁ l₂ : List α
m n : ℕ
hm : m < l₁.length
h : l₂[n]? = some l₁[m]
⊢ l₁.eraseIdx m ~ l₂.eraseIdx n ↔ l₁ ~ l₂

Tactic:
getElem?_eq_some_iff

Goal state after:
case inl
α : Type u_1
l₁ l₂ : List α
m n : ℕ
hm : m < l₁.length
h : ∃ h, l₂[n] = l₁[m]
⊢ l₁.eraseIdx m ~ l₂.eraseIdx n ↔ l₁ ~ l₂
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
f : α → α
hf : Involutive f
x : α
l : List α
⊢ (∃ y, y ∈ l ∧ f y = x) → f x ∈ l

Tactic:
rintro ⟨y, h, rfl⟩

Goal state after:
α : Type u
f : α → α
hf : Involutive f
l : List α
y : α
h : y ∈ l
⊢ f (f y) ∈ l
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: M : Type u_4
N : Type u_5
inst✝³ : Monoid M
inst✝² : Monoid N
l : List M
F : Type u_8
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
f : F
hl✝ : l ≠ []
x : M
xs : List M
hl : x :: xs ≠ []
⊢ (map (⇑f) (x :: xs)).prod = f (x :: xs).prod

Tactic:
induction xs generalizing x

Goal state after:
case nil
M : Type u_4
N : Type u_5
inst✝³ : Monoid M
inst✝² : Monoid N
l : List M
F : Type u_8
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
f : F
hl✝ : l ≠ []
x : M
hl : [x] ≠ []
⊢ (map ⇑f [x]).prod = f [x].prod

case cons
M : Type u_4
N : Type u_5
inst✝³ : Monoid M
inst✝² : Monoid N
l : List M
F : Type u_8
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
f : F
hl✝ : l ≠ []
head✝ : M
tail✝ : List M
tail_ih✝ : ∀ (x : M), x :: tail✝ ≠ [] → (map (⇑f) (x :: tail✝)).prod = f (x :: tail✝).prod
x : M
hl : x :: head✝ :: tail✝ ≠ []
⊢ (map (⇑f) (x :: head✝ :: tail✝)).prod = f (x :: head✝ :: tail✝).prod
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: ι : Type u_1
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l : List ι
f : M → N → P
hf : ∀ (a b : M) (c d : N), f (a * b) (c * d) = f a c * f b d
f₁ : ι → M
f₂ : ι → N
hl✝ : l ≠ []
x : ι
xs : List ι
hl : x :: xs ≠ []
⊢ (map (fun i ↦ f (f₁ i) (f₂ i)) (x :: xs)).prod = f (map f₁ (x :: xs)).prod (map f₂ (x :: xs)).prod

Tactic:
induction xs generalizing x

Goal state after:
case nil
ι : Type u_1
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l : List ι
f : M → N → P
hf : ∀ (a b : M) (c d : N), f (a * b) (c * d) = f a c * f b d
f₁ : ι → M
f₂ : ι → N
hl✝ : l ≠ []
x : ι
hl : [x] ≠ []
⊢ (map (fun i ↦ f (f₁ i) (f₂ i)) [x]).prod = f (map f₁ [x]).prod (map f₂ [x]).prod

case cons
ι : Type u_1
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l : List ι
f : M → N → P
hf : ∀ (a b : M) (c d : N), f (a * b) (c * d) = f a c * f b d
f₁ : ι → M
f₂ : ι → N
hl✝ : l ≠ []
head✝ : ι
tail✝ : List ι
tail_ih✝ :
  ∀ (x : ι),
    x :: tail✝ ≠ [] →
      (map (fun i ↦ f (f₁ i) (f₂ i)) (x :: tail✝)).prod = f (map f₁ (x :: tail✝)).prod (map f₂ (x :: tail✝)).prod
x : ι
hl : x :: head✝ :: tail✝ ≠ []
⊢ (map (fun i ↦ f (f₁ i) (f₂ i)) (x :: head✝ :: tail✝)).prod =
    f (map f₁ (x :: head✝ :: tail✝)).prod (map f₂ (x :: head✝ :: tail✝)).prod
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
x : M
xs : List M
y : M
ys : List M
| x * xs.prod * (y * ys.prod)

Tactic:
rw [mul_assoc]

Goal state after:
M : Type u_4
inst✝ : CommMonoid M
x : M
xs : List M
y : M
ys : List M
| x * (xs.prod * (y * ys.prod))
Module: Mathlib.Data.List.Basic

Goal state before:
pp: case cons
α : Type u
β : Type v
f : α → Option β
g : α → β
a : α
l : List α
ih : filterMap f l = map g l → ∀ (x : α), x ∈ l → f x = some (g x)
⊢ filterMap f (a :: l) = map g (a :: l) → ∀ (x : α), x ∈ a :: l → f x = some (g x)

Tactic:
rcases ha : f a with - | b

Goal state after:
case cons.none
α : Type u
β : Type v
f : α → Option β
g : α → β
a : α
l : List α
ih : filterMap f l = map g l → ∀ (x : α), x ∈ l → f x = some (g x)
ha : f a = none
⊢ filterMap f (a :: l) = map g (a :: l) → ∀ (x : α), x ∈ a :: l → f x = some (g x)

case cons.some
α : Type u
β : Type v
f : α → Option β
g : α → β
a : α
l : List α
ih : filterMap f l = map g l → ∀ (x : α), x ∈ l → f x = some (g x)
b : β
ha : f a = some b
⊢ filterMap f (a :: l) = map g (a :: l) → ∀ (x : α), x ∈ a :: l → f x = some (g x)
Module: Mathlib.Data.Rat.Defs

Goal state before:
pp: a b c : ℤ
h : ¬c = 0
⊢ (a + b) /. c = (a * c + b * c) /. (c * c)

Tactic:
divInt_eq_divInt_iff h (Int.mul_ne_zero h h)

Goal state after:
a b c : ℤ
h : ¬c = 0
⊢ (a + b) * (c * c) = (a * c + b * c) * c
Module: Mathlib.Algebra.Order.Ring.Unbundled.Rat

Goal state before:
pp: a b c d : ℤ
b_pos : 0 < b
d_pos : 0 < d
⊢ ↑a / ↑b < ↑c / ↑d ↔ a * d < c * b

Tactic:
simp only [lt_iff_le_not_ge]
  apply and_congr
  · simp [div_def', Rat.divInt_le_divInt b_pos d_pos]
  · simp [div_def', Rat.divInt_le_divInt d_pos b_pos]

Goal state after:
Module: Mathlib.Algebra.Divisibility.Units

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b u : α
hu : IsUnit u
⊢ a * u ∣ b ↔ a ∣ b

Tactic:
by
  rcases hu with ⟨u, rfl⟩
  apply Units.mul_right_dvd

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
a : α
m n : ℕ
ha₀ : a ≠ 0
ha : ¬IsUnit a
⊢ a ^ n ∣ a ^ m ↔ n ≤ m

Tactic:
constructor
  · intro h
    rw [← not_lt]
    intro hmn
    apply ha
    have : a ^ m * a ∣ a ^ m * 1 := by
      rw [← pow_succ, mul_one]
      exact (pow_dvd_pow _ (Nat.succ_le_of_lt hmn)).trans h
    rwa [mul_dvd_mul_iff_left, ← isUnit_iff_dvd_one] at this
    apply pow_ne_zero m ha₀
  · apply pow_dvd_pow

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a₃ b a₁ : R
a₂ : ℕ
⊢ a₁ ^ a₂ * a₃ * b = a₁ ^ a₂ * (a₃ * b)

Tactic:
rw [mul_assoc]

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: c₂ k a₁ a₂ : ℕ
⊢ a₁ ^ a₂ * (c₂ * k) = a₁ ^ a₂ * c₂ * k

Tactic:
rw [mul_assoc]

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

Goal state before:
pp: R : Type u
inst✝⁶ : CommSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : CanonicallyOrderedAdd R
inst✝³ : Sub R
inst✝² : OrderedSub R
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : AddLeftReflectLE R
a b : R
⊢ a ^ 2 - b ^ 2 = (a + b) * (a - b)

Tactic:
sq,

Goal state after:
R : Type u
inst✝⁶ : CommSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : CanonicallyOrderedAdd R
inst✝³ : Sub R
inst✝² : OrderedSub R
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : AddLeftReflectLE R
a b : R
⊢ a * a - b ^ 2 = (a + b) * (a - b)
Module: Mathlib.Algebra.Order.Ring.Canonical

Goal state before:
pp: R : Type u
inst✝⁶ : CommSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : CanonicallyOrderedAdd R
inst✝³ : Sub R
inst✝² : OrderedSub R
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : AddLeftReflectLE R
a b : R
⊢ a * a - b ^ 2 = (a + b) * (a - b)

Tactic:
sq,

Goal state after:
R : Type u
inst✝⁶ : CommSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : CanonicallyOrderedAdd R
inst✝³ : Sub R
inst✝² : OrderedSub R
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : AddLeftReflectLE R
a b : R
⊢ a * a - b * b = (a + b) * (a - b)
Module: Mathlib.Order.CompleteLattice.Defs

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
i : CompleteLinearOrder α
a b : α
h : ¬a ≤ b
⊢ min a b = b

Tactic:
simp [(CompleteLinearOrder.le_total a b).resolve_left h]

Goal state after:
Module: Mathlib.Order.CompleteLattice.Defs

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
i : CompleteLinearOrder α
a b : α
h : ¬a ≤ b
⊢ max a b = a

Tactic:
simp [(CompleteLinearOrder.le_total a b).resolve_left h]

Goal state after:
Module: Mathlib.Order.CompleteLattice.Defs

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : CompleteLinearOrder α
f : ι → α
⊢ iSup f = ⊤ ↔ ∀ b < ⊤, ∃ i, b < f i

Tactic:
by
  rw [eq_top_iff, le_iSup_iff_forall_lt]

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : SupSet α
p : ι → Prop
f g : (i : ι) → p i → α
h : ∀ (i : ι) (hi : p i), f i hi = g i hi
⊢ ⨆ i, ⨆ (hi : p i), f i hi = ⨆ i, ⨆ (hi : p i), g i hi

Tactic:
#adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
  (replacing grind's canonicalizer with a type-directed normalizer), `grind` closed this goal.
  It is not yet clear whether this is due to defeq abuse in Mathlib or a problem in the new
  canonicalizer; a minimization would help. The original proof was: `grind` -/
  simp_all

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

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
ι : Sort u_5
C : ι → Set α
f : (x : ι) → β → ↑(C x)
hf : ∀ (x : ι), Surjective (f x)
y : β
i : ι
⊢ ∃ i_1, (fun x ↦ ↑(f x y)) i ∈ C i_1

Tactic:
exact ⟨i, (f i y).2⟩

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

Goal state before:
pp: α : Type u_1
ι : Sort u_5
r : α → α → Prop
f : ι → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) f
h : ∀ (x : ι), DirectedOn r (f x)
⊢ DirectedOn r (⋃ x, f x)

Tactic:
simp only [DirectedOn, mem_iUnion, exists_imp]

Goal state after:
α : Type u_1
ι : Sort u_5
r : α → α → Prop
f : ι → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) f
h : ∀ (x : ι), DirectedOn r (f x)
⊢ ∀ (x : α) (x_1 : ι), x ∈ f x_1 → ∀ (y : α) (x_2 : ι), y ∈ f x_2 → ∃ z, (∃ i, z ∈ f i) ∧ r x z ∧ r y z
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: case inr
α : Type u_1
ι : Type u_4
inst✝¹ : Nonempty ι
s : Set α
f : α → ι
r : ι → ι → Prop
inst✝ : IsEquiv ι r
hne : s.Nonempty
⊢ s.Pairwise (r on f) ↔ ∃ z, ∀ (x : α), x ∈ s → r (f x) z

Tactic:
exact hne.pairwise_iff_exists_forall

Goal state after:
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: α : Type u_1
ι : Type u_4
inst✝ : LinearOrder ι
f : ι → Set α
h : ¬Pairwise (Disjoint on f)
⊢ ∃ i j, i < j ∧ ∃ x, x ∈ f i ∩ f j

Tactic:
by
  rw [← pairwise_univ] at h
  obtain ⟨i, _hi, j, _hj, h⟩ := exists_lt_mem_inter_of_not_pairwiseDisjoint h
  exact ⟨i, j, h⟩

Goal state after:
Module: Mathlib.Order.Preorder.Chain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
h : IsChain r univ
a b : α
⊢ ¬r a b → ¬r b a → a = b

Tactic:
have : a ≠ b → (r a b ∨ r b a) := h trivial trivial

Goal state after:
α : Type u_1
r : α → α → Prop
h : IsChain r univ
a b : α
this : a ≠ b → r a b ∨ r b a
⊢ ¬r a b → ¬r b a → a = b
Module: Mathlib.Order.Antichain

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
hs : IsAntichain r s
φ : r ↪r r'
b : β
hb : b ∈ ⇑φ '' s
b' : β
hb' : b' ∈ ⇑φ '' s
h₁ : b ≠ b'
h₂ : r' b b'
⊢ False

Tactic:
rw [Set.mem_image] at hb hb'

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
hs : IsAntichain r s
φ : r ↪r r'
b : β
hb : ∃ x ∈ s, φ x = b
b' : β
hb' : ∃ x ∈ s, φ x = b'
h₁ : b ≠ b'
h₂ : r' b b'
⊢ False
Module: Mathlib.Algebra.Order.Monoid.Basic

Goal state before:
pp: α : Type u
β : Type u_1
inst✝⁴ : CommMonoid α
inst✝³ : Preorder α
inst✝² : IsOrderedCancelMonoid α
inst✝¹ : CommMonoid β
inst✝ : LinearOrder β
f : β → α
hf : StrictMono f
mul : ∀ (x y : β), f (x * y) = f x * f y
a b c : β
h : a * b ≤ a * c
⊢ b ≤ c

Tactic:
simpa [← hf.le_iff_le, mul] using h

Goal state after:
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: ι : Sort u_1
α : Type u_2
s : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : Inhabited ↑s
h_Sup : ∀ {t : Set ↑s}, t.Nonempty → BddAbove t → sSup (Subtype.val '' t) ∈ s
h_Inf : ∀ {t : Set ↑s}, t.Nonempty → BddBelow t → sInf (Subtype.val '' t) ∈ s
t : Set ↑s
ht : t.Nonempty
h_bdd : BddAbove t
⊢ IsLUB ((fun {y} ↦ ↑y) '' t) ↑(sSup t)

Tactic:
rw [← subset_sSup_of_within s ht h_bdd (h_Sup ht h_bdd)]

Goal state after:
ι : Sort u_1
α : Type u_2
s : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : Inhabited ↑s
h_Sup : ∀ {t : Set ↑s}, t.Nonempty → BddAbove t → sSup (Subtype.val '' t) ∈ s
h_Inf : ∀ {t : Set ↑s}, t.Nonempty → BddBelow t → sInf (Subtype.val '' t) ∈ s
t : Set ↑s
ht : t.Nonempty
h_bdd : BddAbove t
⊢ IsLUB ((fun {y} ↦ ↑y) '' t) (sSup (Subtype.val '' t))
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : Group α
inst✝ : MulLeftMono α
⊢ ∀ ⦃a₁ a₂ : α⦄, a₁⁺ᵐ = a₂⁺ᵐ → a₁⁻ᵐ = a₂⁻ᵐ → a₁ = a₂

Tactic:
rintro a b hpos hneg

Goal state after:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : Group α
inst✝ : MulLeftMono α
a b : α
hpos : a⁺ᵐ = b⁺ᵐ
hneg : a⁻ᵐ = b⁻ᵐ
⊢ a = b
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ a ≤ b ↔ a⁺ᵐ ≤ b⁺ᵐ ∧ b⁻ᵐ ≤ a⁻ᵐ

Tactic:
refine ⟨fun h ↦ ⟨oneLePart_mono h, leOnePart_anti h⟩, fun h ↦ ?_⟩
  rw [← oneLePart_div_leOnePart a, ← oneLePart_div_leOnePart b]
  exact div_le_div'' h.1 h.2

Goal state after:
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a : α
⊢ |a|ₘ * a = a⁺ᵐ ^ 2

Tactic:
sq,

Goal state after:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a : α
⊢ |a|ₘ * a = a⁺ᵐ * a⁺ᵐ
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a : α
⊢ |a|ₘ / a = a⁻ᵐ ^ 2

Tactic:
sq,

Goal state after:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a : α
⊢ |a|ₘ / a = a⁻ᵐ * a⁻ᵐ
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: i n : ℕ
n1 : 1 ≤ n
⊢ i + n ! ≤ (i + n)!

Tactic:
rcases n1 with - | @h
  · exact self_le_factorial _
  exact add_factorial_succ_le_factorial_add_succ i h

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

Goal state before:
pp: case zero
l k : ℕ
⊢ ascFactorial 0 l * (0 + l).ascFactorial k = ascFactorial 0 (l + k)

Tactic:
cases l
    · simp only [ascFactorial_zero, Nat.add_zero, Nat.one_mul, Nat.zero_add]
    · simp only [Nat.add_right_comm, zero_ascFactorial, Nat.zero_add, Nat.zero_mul]

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

Goal state before:
pp: case zero
p : ℕ+ → Sort u_1
one : p 1
succ : (n : ℕ+) → p n → p (n + 1)
h : 0 < 0
⊢ p ⟨0, h⟩

Tactic:
exact absurd h (by decide)

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

Goal state before:
pp: case zero
p : ℕ+ → Sort u_1
one : p 1
succ : (n : ℕ+) → p n → p (n + 1)
h : 0 < 0
⊢ (⟨0, h⟩ + 1).recOn one succ = succ ⟨0, h⟩ (recOn ⟨0, h⟩ one succ)

Tactic:
exact absurd h (by decide)

Goal state after:
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: case inr
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
hx : x < ↑z
⊢ 1 - fract x ≤ ↑z - ↑⌊x⌋ + -fract x

Tactic:
le_add_neg_iff_add_le,

Goal state after:
case inr
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
hx : x < ↑z
⊢ 1 - fract x + fract x ≤ ↑z - ↑⌊x⌋
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : FloorRing R
a : R
⊢ ⌊a⌋ = 0 ↔ a ∈ Ico 0 1

Tactic:
by simp [floor_eq_iff]

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

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a : α
ha : a < 1
n : ℤ
⊢ a ^ n * a < a ^ n

Tactic:
exact mul_lt_of_lt_one_right' (a ^ n) ha

Goal state after: