mathlib-initiative/mathlib-tactics huggingface dataset:
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:
le_div_iff₀ hb,

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

Goal state before:
pp: case inr
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
hb✝ : 0 ≤ b
hc : 0 ≤ c
h : a ≤ c * b
hb : 0 < b
⊢ a * b⁻¹ ≤ c

Tactic:
· rwa [mul_inv_le_iff₀ hb]

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

Goal state before:
pp: R : Type u
inst✝⁵ : CommSemiring R
inst✝⁴ : LinearOrder R
inst✝³ : ExistsAddOfLE R
inst✝² : MulPosStrictMono R
inst✝¹ : AddLeftReflectLE R
inst✝ : AddLeftMono R
a b : R
⊢ 4 * a * b = 2 * a * b + 2 * a * b

Tactic:
by rw [mul_assoc, two_add_two_eq_four.symm, add_mul, mul_assoc]

Goal state after:
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
ha₁ : 1 < a
⊢ Injective fun n ↦ a ^ n

Tactic:
exact (zpow_right_strictMono₀ ha₁).injective

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
⊢ a ≤ b * c⁻¹ ↔ c * a ≤ b

Tactic:
rw [le_mul_inv_iff₀ hc, mul_comm]

Goal state after:
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
hab : a ≤ b
ha : a < 1
hb : 1 ≤ b
⊢ (|a * b|ₘ = a⁻¹ * b ↔ b ≤ 1) ↔ (|a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1)

Tactic:
simp [ha.le, ha.not_ge, hb, mabs_of_le_one, mabs_of_one_le]

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

Goal state before:
pp: β : Type u_1
M : Type u_3
inst✝⁴ : Monoid M
inst✝³ : Preorder M
inst✝² : Preorder β
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
f : β → M
hf : Monotone f
⊢ Monotone fun a ↦ f a ^ 0

Tactic:
simpa using monotone_const

Goal state after:
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|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1

Tactic:
obtain ab | ab := le_total a b
  · exact mabs_mul_eq_mul_mabs_le ab
  · simpa only [mul_comm, and_comm] using mabs_mul_eq_mul_mabs_le ab

Goal state after:
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
⊢ |b|ₘ / |a|ₘ ≤ |a / b|ₘ

Tactic:
rw [mabs_div_comm]

Goal state after:
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
⊢ |b|ₘ / |a|ₘ ≤ |b / a|ₘ
Module: Mathlib.Algebra.GroupWithZero.Regular

Goal state before:
pp: R : Type u_1
inst✝¹ : MulZeroClass R
a : R
inst✝ : Nontrivial R
la : IsLeftRegular a
⊢ a ≠ 0

Tactic:
rintro rfl
  rcases exists_pair_ne R with ⟨x, y, xy⟩
  refine xy (la ?_)
  simp

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

Goal state before:
pp: R : Type u_1
inst✝ : Monoid R
a : R
n : ℕ
rra : IsRightRegular a
⊢ IsRightRegular (a ^ n)

Tactic:
rw [IsRightRegular, ← mul_right_iterate]

Goal state after:
R : Type u_1
inst✝ : Monoid R
a : R
n : ℕ
rra : IsRightRegular a
⊢ Function.Injective (fun x ↦ x * a)^[n]
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot
α : Type u_1
β : Type u_2
f : α → β
y : β
⊢ ↑y = map f ⊥ ↔ ∃ x, ⊥ = ↑x ∧ f x = y

Tactic:
simp [eq_comm]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe
α : Type u_1
β : Type u_2
f : α → β
y : β
a✝ : α
⊢ ↑y = map f ↑a✝ ↔ ∃ x, ↑a✝ = ↑x ∧ f x = y

Tactic:
simp [eq_comm]

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

Goal state before:
pp: case pos
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)
⊢ findGreatest P (k + 1) = m ↔ m ≤ k + 1 ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k + 1 → ¬P n

Tactic:
findGreatest_eq hk

Goal state after:
case pos
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)
⊢ k + 1 = m ↔ m ≤ k + 1 ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k + 1 → ¬P n
Module: Mathlib.Data.Nat.Find

Goal state before:
pp: case pos
P : ℕ → Prop
inst✝ : DecidablePred P
m n m✝ : ℕ
hmk : m.le m✝
ih : findGreatest P m ≤ findGreatest P m✝
h✝ : P (m✝ + 1)
⊢ findGreatest P m ≤ m✝ + 1

Tactic:
exact le_trans ih <| le_trans (findGreatest_le _) (le_succ _)

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
a b : R
h : IsUnit a ↔ IsUnit b
ha : IsUnit a
hb : IsUnit b
⊢ a⁻¹ʳ + b⁻¹ʳ = a⁻¹ʳ * (a + b) * b⁻¹ʳ

Tactic:
obtain ⟨ia⟩ := ha.nonempty_invertible

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
a b : R
h : IsUnit a ↔ IsUnit b
ha : IsUnit a
hb : IsUnit b
ia : Invertible a
⊢ a⁻¹ʳ + b⁻¹ʳ = a⁻¹ʳ * (a + b) * b⁻¹ʳ
Module: Mathlib.Algebra.Ring.Invertible

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Ring R
a b : R
h : IsUnit a ↔ IsUnit b
ha : IsUnit a
hb : IsUnit b
⊢ a⁻¹ʳ - b⁻¹ʳ = a⁻¹ʳ * (b - a) * b⁻¹ʳ

Tactic:
obtain ⟨ia⟩ := ha.nonempty_invertible

Goal state after:
case pos
R : Type u_1
inst✝ : Ring R
a b : R
h : IsUnit a ↔ IsUnit b
ha : IsUnit a
hb : IsUnit b
ia : Invertible a
⊢ a⁻¹ʳ - b⁻¹ʳ = a⁻¹ʳ * (b - a) * b⁻¹ʳ
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
h : a ^ 2 < b ^ 2
hb : 0 ≤ b
⊢ |a| < b

Tactic:
← abs_of_nonneg hb,

Goal state after:
α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
h : a ^ 2 < b ^ 2
hb : 0 ≤ b
⊢ |a| < |b|
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
h : a ^ 2 ≤ b ^ 2
hb : 0 ≤ b
⊢ |a| ≤ b

Tactic:
← abs_of_nonneg hb,

Goal state after:
α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
h : a ^ 2 ≤ b ^ 2
hb : 0 ≤ b
⊢ |a| ≤ |b|
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: n : ℕ
hn : Odd n
hm : 2 ∣ n
⊢ False

Tactic:
exact absurd (hn.of_dvd_nat hm) (by decide)

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

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

Tactic:
exact Hf.mem_upperBounds_image ha

Goal state after:
Module: Mathlib.Order.WellFounded

Goal state before:
pp: α : Type u_1
r : α → α → Prop
⊢ IsWellOrder α r ↔ ∀ (s : Set α), s.Nonempty → ∃ m, m ∈ s ∧ ∀ (x : α), x ∈ s → ¬r x m ∧ (m = x ∨ r m x)

Tactic:
refine ⟨fun h s hs ↦ ?_, fun h ↦ { wf := ?_, trichotomous a b := ?_ }⟩

Goal state after:
case refine_1
α : Type u_1
r : α → α → Prop
h : IsWellOrder α r
s : Set α
hs : s.Nonempty
⊢ ∃ m, m ∈ s ∧ ∀ (x : α), x ∈ s → ¬r x m ∧ (m = x ∨ r m x)

case refine_2
α : Type u_1
r : α → α → Prop
h : ∀ (s : Set α), s.Nonempty → ∃ m, m ∈ s ∧ ∀ (x : α), x ∈ s → ¬r x m ∧ (m = x ∨ r m x)
⊢ WellFounded r

case refine_3
α : Type u_1
r : α → α → Prop
h : ∀ (s : Set α), s.Nonempty → ∃ m, m ∈ s ∧ ∀ (x : α), x ∈ s → ¬r x m ∧ (m = x ∨ r m x)
a b : α
⊢ ¬r a b → ¬r b a → a = b
Module: Mathlib.Order.WellFounded

Goal state before:
pp: case inl
β : 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 : b < a
⊢ f a = g a

pp: case inr.inl
β : 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 b : β
IH : ∀ (y : β), y < b → f y = g y
hb : g b = f b
⊢ f b = g b

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
⊢ f a = g a

Tactic:
· rw [← IH b h] at hb
    cases (hf.injective hb).not_lt h

Goal state after:
case inr.inl
β : 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 b : β
IH : ∀ (y : β), y < b → f y = g y
hb : g b = f b
⊢ f b = g b

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
⊢ f a = g a
Module: Mathlib.Order.Bounds.Basic

Goal state before:
pp: case neg
γ : Type u_3
inst✝ : LinearOrder γ
i : γ
h_exists_lt : ∀ j ∈ upperBounds (Iio i), i ≤ j
⊢ ∃ j, IsLUB (Iio i) j

Tactic:
· refine ⟨i, fun j hj => le_of_lt hj, ?_⟩
    rw [mem_lowerBounds]
    exact h_exists_lt

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

Goal state before:
pp: case eq
α : Type u_1
inst✝ : Semiring α
na nb nc da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁✝ : na * db + nb * da = k * nc
h₂ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da
h₁ : ↑na * ↑db * ⅟↑da * ⅟↑db + ↑nb * ⅟↑db = ↑k * ↑nc * ⅟↑da * ⅟↑db
⊢ ↑na * ⅟↑da + ↑nb * ⅟↑db = ↑nc * ⅟↑dc

Tactic:
have h₂ := congr_arg (↑nc * ↑· * (⅟↑da * ⅟↑db * ⅟↑dc : α)) h₂

Goal state after:
case eq
α : Type u_1
inst✝ : Semiring α
na nb nc da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁✝ : na * db + nb * da = k * nc
h₂✝ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da
h₁ : ↑na * ↑db * ⅟↑da * ⅟↑db + ↑nb * ⅟↑db = ↑k * ↑nc * ⅟↑da * ⅟↑db
h₂ : ↑nc * ↑(da * db) * (⅟↑da * ⅟↑db * ⅟↑dc) = ↑nc * ↑(k * dc) * (⅟↑da * ⅟↑db * ⅟↑dc)
⊢ ↑na * ⅟↑da + ↑nb * ⅟↑db = ↑nc * ⅟↑dc
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:
le_div_iff₀ hb,

Goal state after:
α : Type u_2
inst✝² : Semifield α
inst✝¹ : PartialOrder α
inst✝ : PosMulReflectLT α
a b : α
hb : 0 < b
⊢ 1 * b ≤ a ↔ b ≤ a
Module: Mathlib.Tactic.NormNum.Basic

Goal state before:
pp: case eq
α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁✝ : na * ↑db + nb * ↑da = ↑k * nc
h₂ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da
h₁ : ↑na * ↑db * ⅟↑da * ⅟↑db + ↑nb * ⅟↑db = ↑k * ↑nc * ⅟↑da * ⅟↑db
⊢ ↑na * ⅟↑da + ↑nb * ⅟↑db = ↑nc * ⅟↑dc

Tactic:
have h₂ := congr_arg (↑nc * ↑· * (⅟↑da * ⅟↑db * ⅟↑dc : α)) h₂

Goal state after:
case eq
α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁✝ : na * ↑db + nb * ↑da = ↑k * nc
h₂✝ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da
h₁ : ↑na * ↑db * ⅟↑da * ⅟↑db + ↑nb * ⅟↑db = ↑k * ↑nc * ⅟↑da * ⅟↑db
h₂ : ↑nc * ↑(da * db) * (⅟↑da * ⅟↑db * ⅟↑dc) = ↑nc * ↑(k * dc) * (⅟↑da * ⅟↑db * ⅟↑dc)
⊢ ↑na * ⅟↑da + ↑nb * ⅟↑db = ↑nc * ⅟↑dc
Module: Mathlib.Algebra.Order.Field.Basic

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

Tactic:
by
  simpa using inv_le_comm₀ ha hb

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

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
na nb nc da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁✝ : na * nb = k * nc
h₂ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da
h₁ : ↑na * ↑nb = ↑k * ↑nc
⊢ ↑k * ↑nc * ⅟↑da * ⅟↑db = ↑nc * ⅟↑dc

Tactic:
have h₂ := congr_arg (↑nc * ↑· * (⅟↑da * ⅟↑db * ⅟↑dc : α)) h₂

Goal state after:
α : Type u_1
inst✝ : Semiring α
na nb nc da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁✝ : na * nb = k * nc
h₂✝ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da
h₁ : ↑na * ↑nb = ↑k * ↑nc
h₂ : ↑nc * ↑(da * db) * (⅟↑da * ⅟↑db * ⅟↑dc) = ↑nc * ↑(k * dc) * (⅟↑da * ⅟↑db * ⅟↑dc)
⊢ ↑k * ↑nc * ⅟↑da * ⅟↑db = ↑nc * ⅟↑dc
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: case inr.inr
α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
b : α
inst✝ : IsStrictOrderedRing α
s : Set α
hs : IsLUB s b
ha : 0 ≤ 0
ne : s.Nonempty
⊢ IsLUB ((fun a ↦ 0) '' s) 0

Tactic:
rw [ne.image_const]

Goal state after:
case inr.inr
α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
b : α
inst✝ : IsStrictOrderedRing α
s : Set α
hs : IsLUB s b
ha : 0 ≤ 0
ne : s.Nonempty
⊢ IsLUB {0} 0
Module: Mathlib.Tactic.NormNum.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁✝ : na * nb = ↑k * nc
h₂ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da
h₁ : ↑na * ↑nb = ↑k * ↑nc
⊢ ↑k * ↑nc * ⅟↑da * ⅟↑db = ↑nc * ⅟↑dc

Tactic:
have h₂ := congr_arg (↑nc * ↑· * (⅟↑da * ⅟↑db * ⅟↑dc : α)) h₂

Goal state after:
α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁✝ : na * nb = ↑k * nc
h₂✝ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da
h₁ : ↑na * ↑nb = ↑k * ↑nc
h₂ : ↑nc * ↑(da * db) * (⅟↑da * ⅟↑db * ⅟↑dc) = ↑nc * ↑(k * dc) * (⅟↑da * ⅟↑db * ⅟↑dc)
⊢ ↑k * ↑nc * ⅟↑da * ⅟↑db = ↑nc * ⅟↑dc
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
⊢ |1 / a| = 1 / |a|

Tactic:
by rw [abs_div, abs_one]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → β → Prop
hr : RightUnique r
a : List α
b : List β
h₁ : Forall₂ r a b
c : List α
d : List β
h₂ : Forall₂ r c d
h : a ~ c
this : (flip (Forall₂ r) ∘r Forall₂ r ∘r Perm) b d
⊢ ((flip (Forall₂ r) ∘r Forall₂ r) ∘r Perm) b d

Tactic:
← Relation.comp_assoc

Goal state after:
α : Type u_1
β : Type u_2
r : α → β → Prop
hr : RightUnique r
a : List α
b : List β
h₁ : Forall₂ r a b
c : List α
d : List β
h₂ : Forall₂ r c d
h : a ~ c
this : ((flip (Forall₂ r) ∘r Forall₂ r) ∘r Perm) b d
⊢ ((flip (Forall₂ r) ∘r Forall₂ r) ∘r Perm) b d
Module: Mathlib.Data.List.Basic

Goal state before:
pp: case mpr
α : Type u
hα : Subsingleton α
l1 l2 : List α
hl : l1.length = l2.length
⊢ l1 = l2

Tactic:
induction l1 generalizing l2 <;> cases l2

Goal state after:
case mpr.nil.nil
α : Type u
hα : Subsingleton α
hl : [].length = [].length
⊢ [] = []

case mpr.nil.cons
α : Type u
hα : Subsingleton α
head✝ : α
tail✝ : List α
hl : [].length = (head✝ :: tail✝).length
⊢ [] = head✝ :: tail✝

case mpr.cons.nil
α : Type u
hα : Subsingleton α
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ ⦃l2 : List α⦄, tail✝.length = l2.length → tail✝ = l2
hl : (head✝ :: tail✝).length = [].length
⊢ head✝ :: tail✝ = []

case mpr.cons.cons
α : Type u
hα : Subsingleton α
head✝¹ : α
tail✝¹ : List α
tail_ih✝ : ∀ ⦃l2 : List α⦄, tail✝¹.length = l2.length → tail✝¹ = l2
head✝ : α
tail✝ : List α
hl : (head✝¹ :: tail✝¹).length = (head✝ :: tail✝).length
⊢ head✝¹ :: tail✝¹ = head✝ :: tail✝
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
a b : α
m n : ℕ
h : a ≠ b
⊢ (count a l = count a (replicate m a ++ replicate n b) ∧
      ∀ (b_1 : α), b_1 ≠ a → count b_1 l = count b_1 (replicate m a ++ replicate n b)) ↔
    count a l = m ∧ count b l = n ∧ l ⊆ [a, b]

Tactic:
← Decidable.and_forall_ne b

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
a b : α
m n : ℕ
h : a ≠ b
⊢ (count a l = count a (replicate m a ++ replicate n b) ∧
      (b ≠ a → count b l = count b (replicate m a ++ replicate n b)) ∧
        ∀ (b_1 : α), b_1 ≠ b → b_1 ≠ a → count b_1 l = count b_1 (replicate m a ++ replicate n b)) ↔
    count a l = m ∧ count b l = n ∧ l ⊆ [a, b]
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
a b : α
l : List α
h : a :: b :: l ≠ []
⊢ (a :: b :: l).dropLast ++ [(a :: b :: l).getLast h] = a :: b :: l

Tactic:
rw [dropLast_cons_cons, cons_append, getLast_cons (cons_ne_nil _ _)]
    congr
    exact dropLast_append_getLast (cons_ne_nil b l)

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
a : M
l : List M
hlen : 0 ≤ l.length
hcomm : ∀ (a' : M), a' ∈ take 0 l → Commute a a'
⊢ (l.insertIdx 0 a).prod = a * l.prod

Tactic:
case =>

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
a : M
i : ℕ
ih : ∀ {l : List M}, i ≤ l.length → (∀ (a' : M), a' ∈ take i l → Commute a a') → (l.insertIdx i a).prod = a * l.prod
l : List M
hlen : i + 1 ≤ l.length
hcomm : ∀ (a' : M), a' ∈ take (i + 1) l → Commute a a'
⊢ (l.insertIdx (i + 1) a).prod = a * l.prod

Tactic:
case =>

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : CommGroupWithZero M
e : M
L l l' l₀ : NF M
h : L.eval * l.eval = l'.eval
h' : ((0, e) ::ᵣ l).eval = l₀.eval
⊢ L.eval * l₀.eval = L.eval * ((0, e) ::ᵣ l).eval

Tactic:
h'

Goal state after:
M : Type u_1
inst✝ : CommGroupWithZero M
e : M
L l l' l₀ : NF M
h : L.eval * l.eval = l'.eval
h' : ((0, e) ::ᵣ l).eval = l₀.eval
⊢ L.eval * l₀.eval = L.eval * l₀.eval
Module: Mathlib.Data.Rat.Defs

Goal state before:
pp: q : ℚ
x✝ : q = 0
⊢ q.num = 0

Tactic:
by simp [*]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a x y : G
h : SemiconjBy a x y
⊢ y * a * a⁻¹ = 1 ↔ y = 1

Tactic:
mul_inv_cancel_right

Goal state after:
G : Type u_1
inst✝ : Group G
a x y : G
h : SemiconjBy a x y
⊢ y = 1 ↔ y = 1
Module: Mathlib.Data.NNRat.Defs

Goal state before:
pp: q : ℚ≥0
⊢ ↑q * ↑↑(↑q).den = ↑(↑q).num

Tactic:
exact Rat.mul_den_eq_num _

Goal state after:
Module: Mathlib.Tactic.CancelDenoms.Core

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
n e t : α
h1 : n * e = t
⊢ n * -e = -t

Tactic:
by simp [*]

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

Goal state before:
pp: R : Type u_2
inst✝ : Semifield R
a b : R
x✝ : a⁻¹ = b
⊢ (a + 0)⁻¹ = b + 0

Tactic:
by simp [*]

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

Goal state before:
pp: ⊢ range succ = {i | 0 < i}

Tactic:
ext (_ | i) <;> simp

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
α : Type u_8
H1 : PartialOrder α
H2 : InfSet α
isGLB_sInf : ∀ (s : Set α), IsGLB s (sInf s)
a b c : α
hac : a ≤ c
hbc : b ≤ c
⊢ c ∈ {x | a ≤ x ∧ b ≤ x}

Tactic:
by simp [*]

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
α : Type u_8
H1 : PartialOrder α
H2 : SupSet α
isLUB_sSup : ∀ (s : Set α), IsLUB s (sSup s)
a b c : α
hac : a ≤ c
hbc : b ≤ c
⊢ c ∈ upperBounds {a, b}

Tactic:
by simp [*]

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
α : Type u_8
H1 : PartialOrder α
H2 : SupSet α
isLUB_sSup : ∀ (s : Set α), IsLUB s (sSup s)
a b c : α
hab : a ≤ b
hac : a ≤ c
⊢ a ∈ {x | x ≤ b ∧ x ≤ c}

Tactic:
by simp [*]

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
s : Set α
t : Set β
l : α → β → γ
u₁ : β → γ → α
u₂ : α → γ → β
a₀ : α
b₀ : β
h₁ : ∀ (b : β), GaloisConnection (swap l b) (u₁ b)
h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)
ha₀ : ∀ (b : α), a₀ ≤ b ↔ ∀ x ∈ s, x ≤ b
hb₀ : ∀ (b : β), b₀ ≤ b ↔ ∀ x ∈ t, x ≤ b
⊢ ∀ (b : γ), l a₀ b₀ ≤ b ↔ ∀ x ∈ s, l x b₀ ≤ b

Tactic:
(h₁ _).le_iff_le,

Goal state after:
α : Type u
β : Type v
γ : Type w
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
s : Set α
t : Set β
l : α → β → γ
u₁ : β → γ → α
u₂ : α → γ → β
a₀ : α
b₀ : β
h₁ : ∀ (b : β), GaloisConnection (swap l b) (u₁ b)
h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)
ha₀ : ∀ (b : α), a₀ ≤ b ↔ ∀ x ∈ s, x ≤ b
hb₀ : ∀ (b : β), b₀ ≤ b ↔ ∀ x ∈ t, x ≤ b
⊢ ∀ (b : γ), a₀ ≤ u₁ b₀ b ↔ ∀ x ∈ s, x ≤ u₁ b₀ b
Module: Mathlib.Order.GaloisConnection.Basic

Goal state before:
pp: α : Type u
β : Type v
l : α → β
u : β → α
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
gi : GaloisInsertion l u
s : Set β
⊢ l (sInf (u '' s)) = sInf s

Tactic:
sInf_image,

Goal state after:
α : Type u
β : Type v
l : α → β
u : β → α
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
gi : GaloisInsertion l u
s : Set β
⊢ l (⨅ a ∈ s, u a) = sInf s
Module: Mathlib.Order.GaloisConnection.Basic

Goal state before:
pp: α : Type u
β : Type v
l : α → β
u : β → α
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
gi : GaloisInsertion l u
s : Set β
⊢ ⨅ i ∈ s, i = sInf s

Tactic:
sInf_eq_iInf

Goal state after:
α : Type u
β : Type v
l : α → β
u : β → α
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
gi : GaloisInsertion l u
s : Set β
⊢ ⨅ i ∈ s, i = ⨅ a ∈ s, a
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
γ : Type u_8
f : β → γ
g : γ → α
t : Set β
⊢ ⨆ c ∈ f '' t, g c = ⨆ b ∈ t, g (f b)

Tactic:
by
  rw [← sSup_image, ← sSup_image, ← image_comp, comp_def]

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
κ : ι → Sort u_6
inst✝ : CompleteLinearOrder α
f : (i : ι) → κ i → α
⊢ ⨆ i, ⨆ j, f i j = ⊤ ↔ ∀ b < ⊤, ∃ i j, b < f i j

Tactic:
by
  simp_rw [iSup_psigma', iSup_eq_top, PSigma.exists]

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
ι : Sort w
κ : ι → Sort w'
inst✝ : Frame α
a : α
f : (i : ι) → κ i → α
⊢ Disjoint (⨆ i, ⨆ j, f i j) a ↔ ∀ (i : ι) (j : κ i), Disjoint (f i j) a

Tactic:
by
  simp_rw [iSup_disjoint_iff]

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

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
t : Set α
hs : ∀ x ∈ ∅, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ ∅, y ≤ x
y : α
yt : y ∈ t
⊢ False

Tactic:
simpa using ht y yt

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : BddBelow s
⊢ IsGLB s (sInf s)

Tactic:
exact isGLB_sInf' hs

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

Goal state before:
pp: a b q q' : ℤ
h : IsInt (a / -b) q
hq : -q = q'
⊢ a / b = ↑q'

Tactic:
rw [Int.cast_id, ← hq, ← @Int.cast_id q, ← h.out, ← Int.ediv_neg, Int.neg_neg]

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

Goal state before:
pp: n : ℕ
⊢ 2 ≤ 0 → (n + 1) ^ 0 < (n + 1).ascFactorial 0

Tactic:
rintro ⟨⟩

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

Goal state before:
pp: n : ℕ
⊢ 2 ≤ 0 → (n + 1).ascFactorial 0 < (n + 0) ^ 0

Tactic:
rintro ⟨⟩

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

Goal state before:
pp: k : ℕ
h : k.succ ≤ 0
⊢ (0 - k.succ)! * descFactorial 0 k.succ = 0!

Tactic:
by
    exfalso
    exact not_succ_le_zero k h

Goal state after: