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

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

Tactic:
simp only [neg_pos, neg_nonneg]

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

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

Tactic:
simp only [neg_pos, neg_nonneg]

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

Goal state before:
pp: α : Type u_1
x✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
⊢ WellFounded (Quotient.lift₂ r H) ↔ WellFounded r

Tactic:
by
  constructor
  · exact RelHomClass.wellFounded (Quotient.mkRelHom H)
  · refine fun wf => ⟨fun q => ?_⟩
    obtain ⟨a, rfl⟩ := q.exists_rep
    exact acc_lift₂_iff.2 (wf.apply a)

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
x : α
y : β
⊢ x < e.symm y ↔ e x < y

Tactic:
rw [← e.lt_iff_lt, e.apply_symm_apply]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : SemilatticeInf α
inst✝² : OrderBot α
inst✝¹ : SemilatticeInf β
inst✝ : OrderBot β
a b : α
f : α ≃o β
ha : Disjoint a b
⊢ f (a ⊓ b) ≤ ⊥

Tactic:
← f.map_bot

Goal state after:
α : Type u_2
β : Type u_3
inst✝³ : SemilatticeInf α
inst✝² : OrderBot α
inst✝¹ : SemilatticeInf β
inst✝ : OrderBot β
a b : α
f : α ≃o β
ha : Disjoint a b
⊢ f (a ⊓ b) ≤ f ⊥
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow

Goal state before:
pp: M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulLeftMono M
a : M
h : a < 1
k : ℕ
hn : k.succ ≠ 0
⊢ a ^ k.succ < 1

Tactic:
pow_succ'

Goal state after:
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulLeftMono M
a : M
h : a < 1
k : ℕ
hn : k.succ ≠ 0
⊢ a * a ^ k < 1
Module: Mathlib.Algebra.Order.Group.Abs

Goal state before:
pp: G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a : G
⊢ |a|ₘ = a ∧ 1 ≤ a ∨ |a|ₘ = a⁻¹ ∧ a < 1

Tactic:
by
  cases le_or_gt 1 a <;> simp [*, le_of_lt]

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

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b c : α
this : DistribLattice α := CommGroup.toDistribLattice α
⊢ (b ⊔ c ⊔ (a ⊔ c)) / ((b ⊔ c) ⊓ (a ⊔ c)) * |(a ⊓ c) / (b ⊓ c)|ₘ =
    (b ⊔ c ⊔ (a ⊔ c)) / ((b ⊔ c) ⊓ (a ⊔ c)) * ((b ⊓ c ⊔ a ⊓ c) / (b ⊓ c ⊓ (a ⊓ c)))

Tactic:
rw [sup_div_inf_eq_mabs_div (b ⊓ c) (a ⊓ c)]

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

Goal state before:
pp: α : Type u_1
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
a : α
⊢ |a|ₘ⁻¹ ≤ a

Tactic:
obtain h | h := le_total 1 a

Goal state after:
case inl
α : Type u_1
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
a : α
h : 1 ≤ a
⊢ |a|ₘ⁻¹ ≤ a

case inr
α : Type u_1
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
a : α
h : a ≤ 1
⊢ |a|ₘ⁻¹ ≤ a
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: a b : ℤ
ha : a ≠ 0
⊢ IsLeast {n | 0 < n ∧ ∃ x y, ↑n = a * x + b * y} (a.gcd b)

Tactic:
simp_rw [← gcd_dvd_iff]

Goal state after:
a b : ℤ
ha : a ≠ 0
⊢ IsLeast {n | 0 < n ∧ a.gcd b ∣ n} (a.gcd b)
Module: Mathlib.Algebra.Regular.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Monoid R
a : R
n : ℕ
n0 : 0 < n
⊢ IsRightRegular (a ^ n.pred.succ) → IsRightRegular a

Tactic:
pow_succ'

Goal state after:
R : Type u_1
inst✝ : Monoid R
a : R
n : ℕ
n0 : 0 < n
⊢ IsRightRegular (a * a ^ n.pred) → IsRightRegular 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 ↔ a = c + b

Tactic:
eq_comm,

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
⊢ c = a - b ↔ a = c + b
Module: Mathlib.Algebra.Order.Ring.Cast

Goal state before:
pp: R : Type u_1
inst✝³ : AddCommGroupWithOne R
inst✝² : PartialOrder R
inst✝¹ : AddLeftMono R
inst✝ : ZeroLEOneClass R
m n : ℤ
k : ℕ
hk : ↑k = n - m
⊢ 0 ≤ ↑n - ↑m

Tactic:
← cast_sub,

Goal state after:
R : Type u_1
inst✝³ : AddCommGroupWithOne R
inst✝² : PartialOrder R
inst✝¹ : AddLeftMono R
inst✝ : ZeroLEOneClass R
m n : ℤ
k : ℕ
hk : ↑k = n - m
⊢ 0 ≤ ↑(n - m)
Module: Mathlib.Algebra.Order.Ring.Cast

Goal state before:
pp: R : Type u_1
inst✝⁴ : AddCommGroupWithOne R
inst✝³ : PartialOrder R
inst✝² : AddLeftMono R
inst✝¹ : ZeroLEOneClass R
inst✝ : NeZero 1
m n : ℤ
⊢ 0 ≤ ↑n - ↑m ↔ m ≤ n

Tactic:
← cast_sub,

Goal state after:
R : Type u_1
inst✝⁴ : AddCommGroupWithOne R
inst✝³ : PartialOrder R
inst✝² : AddLeftMono R
inst✝¹ : ZeroLEOneClass R
inst✝ : NeZero 1
m n : ℤ
⊢ 0 ≤ ↑(n - m) ↔ m ≤ n
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:
eq_comm,

Goal state after:
case zero
P : ℕ → Prop
inst✝ : DecidablePred P
m : ℕ
⊢ m = findGreatest P 0 ↔ m ≤ 0 ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ 0 → ¬P n
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : WithZero (Multiplicative α)
b : α
ha : a ≠ 0
h : a < ↑(ofAdd b)
⊢ toAdd (unzero ha) < b

Tactic:
← coe_unzero ha,

Goal state after:
α : Type u_1
inst✝ : Preorder α
a : WithZero (Multiplicative α)
b : α
ha : a ≠ 0
h : ↑(unzero ha) < ↑(ofAdd b)
⊢ toAdd (unzero ha) < b
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : WithZero (Multiplicative α)
b : α
ha : a ≠ 0
h : toAdd (unzero ha) < b
⊢ a < ↑(ofAdd b)

Tactic:
← coe_unzero ha,

Goal state after:
α : Type u_1
inst✝ : Preorder α
a : WithZero (Multiplicative α)
b : α
ha : a ≠ 0
h : toAdd (unzero ha) < b
⊢ ↑(unzero ha) < ↑(ofAdd b)
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : WithZero (Multiplicative α)
b : α
ha : a ≠ 0
h : a ≤ ↑(ofAdd b)
⊢ toAdd (unzero ha) ≤ b

Tactic:
← coe_unzero ha,

Goal state after:
α : Type u_1
inst✝ : Preorder α
a : WithZero (Multiplicative α)
b : α
ha : a ≠ 0
h : ↑(unzero ha) ≤ ↑(ofAdd b)
⊢ toAdd (unzero ha) ≤ b
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : WithZero (Multiplicative α)
b : α
ha : a ≠ 0
h : toAdd (unzero ha) ≤ b
⊢ a ≤ ↑(ofAdd b)

Tactic:
← coe_unzero ha,

Goal state after:
α : Type u_1
inst✝ : Preorder α
a : WithZero (Multiplicative α)
b : α
ha : a ≠ 0
h : toAdd (unzero ha) ≤ b
⊢ ↑(unzero ha) ≤ ↑(ofAdd b)
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:
← sub_one_lt_iff,

Goal state after:
α : Type u_2
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
z : ℤ
a : α
⊢ z - 1 < ⌈a⌉ ↔ ↑z - 1 < a
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
y : WithZero α
a b : α
hy : ↑b ≤ y
hne : y ≠ 0
⊢ b ≤ unzeroD a y

Tactic:
le_unzeroD_iff hne

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
y : WithZero α
a b : α
hy : ↑b ≤ y
hne : y ≠ 0
⊢ ↑b ≤ y
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: case inr.inl
R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : FloorSemiring R
inst✝³ : IsStrictOrderedRing R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : ExistsAddOfLE R
a : R
n : ℕ
ha : 0 ≤ a
h : a ≤ ↑n
⊢ 0 = ⌊a⌋₊ - n

Tactic:
eq_comm,

Goal state after:
case inr.inl
R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : FloorSemiring R
inst✝³ : IsStrictOrderedRing R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : ExistsAddOfLE R
a : R
n : ℕ
ha : 0 ≤ a
h : a ≤ ↑n
⊢ ⌊a⌋₊ - n = 0
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: case inl
R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : FloorSemiring R
inst✝³ : IsStrictOrderedRing R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : ExistsAddOfLE R
a : R
n : ℕ
han : a ≤ ↑n
⊢ 0 = ⌈a⌉₊ - n

Tactic:
eq_comm,

Goal state after:
case inl
R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : FloorSemiring R
inst✝³ : IsStrictOrderedRing R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : ExistsAddOfLE R
a : R
n : ℕ
han : a ≤ ↑n
⊢ ⌈a⌉₊ - n = 0
Module: Mathlib.Algebra.Ring.Invertible

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

Tactic:
rw [← neg_eq_val_neg, ← val_neg_mulRight]
  apply AddUnits.neg_eq_of_add_eq_zero_left
  simp [← mul_add]

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

Goal state before:
pp: case inr
G₀ : Type u_1
inst✝² : GroupWithZero G₀
inst✝¹ : SemilatticeInf G₀
inst✝ : PosMulReflectLT G₀
c : G₀
hc✝ : 0 ≤ c
a b : G₀
hc : 0 < c
⊢ c * (a ⊓ b) = c * a ⊓ c * b

Tactic:
exact (OrderIso.mulLeft₀ c hc).map_inf a b

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

Goal state before:
pp: 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 : ℕ := k.succ
h1 : 0 ≤ x * y ^ n + y * x ^ n
h2 : 0 ≤ x + y
⊢ (x + y) * (x ^ n + y ^ n) ≤ (x + y) ^ (n + 1)

Tactic:
rw [pow_succ' _ n]

Goal state after:
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 : ℕ := k.succ
h1 : 0 ≤ x * y ^ n + y * x ^ n
h2 : 0 ≤ x + y
⊢ (x + y) * (x ^ n + y ^ n) ≤ (x + y) * (x + y) ^ n
Module: Mathlib.Algebra.Order.Ring.Basic

Goal state before:
pp: R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a b : R
inst✝ : ExistsAddOfLE R
ha : 0 ≤ a
hb : 0 ≤ b
n : ℕ
⊢ 2 ^ n * (a ^ (n + 2) + b ^ (n + 2) + (a ^ (n + 1) * a + b ^ (n + 1) * b)) =
    2 ^ (n + 2 - 1) * (a ^ (n + 2) + b ^ (n + 2))

Tactic:
by simp only [← pow_succ, ← two_mul, ← mul_assoc]; rfl

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

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

Tactic:
rw [add_comm]; exact dvd_add_left h

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

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

Tactic:
by
  rw [sub_eq_add_neg, dvd_add_right h, dvd_neg]

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

Goal state before:
pp: K : Type u_1
inst✝ : DivisionRing K
a : K
⊢ a = a⁻¹ ↔ a = -1 ∨ a = 0 ∨ a = 1

Tactic:
eq_comm,

Goal state after:
K : Type u_1
inst✝ : DivisionRing K
a : K
⊢ a⁻¹ = a ↔ a = -1 ∨ a = 0 ∨ a = 1
Module: Mathlib.Data.Set.Monotone

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → x ≤ a
⊢ StrictMonoOn f (insert a s) ↔ (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ StrictMonoOn f s

Tactic:
strictMonoOn_insert_iff

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → x ≤ a
⊢ (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s ↔
    (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ StrictMonoOn f s
Module: Mathlib.Data.Set.Monotone

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → a ≤ x
⊢ StrictMonoOn f (insert a s) ↔ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s

Tactic:
strictMonoOn_insert_iff

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → a ≤ x
⊢ (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s ↔
    (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
⊢ |a| ≤ |b| ↔ a * a ≤ b * b

Tactic:
by
  rw [← abs_mul_abs_self, ← abs_mul_abs_self b]
  exact mul_self_le_mul_self_iff (abs_nonneg a) (abs_nonneg b)

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

Goal state before:
pp: α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
f : α → β → γ
s : Set α
t : Set β
g : γ → δ
f' : β' → α' → δ
g₁ : β → β'
g₂ : α → α'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ b) (g₂ a)
⊢ g '' image2 f s t = image2 f' (g₁ '' t) (g₂ '' s)

Tactic:
by
  rw [image2_swap f]
  exact image_image2_distrib fun _ _ => h_antidistrib _ _

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

Goal state before:
pp: α : Type u_1
inst✝ : SemilatticeInf α
a b c : α
⊢ Ioc a b ∩ Iic c = Ioc a (b ⊓ c)

Tactic:
← Ioi_inter_Iic,

Goal state after:
α : Type u_1
inst✝ : SemilatticeInf α
a b c : α
⊢ Ioi a ∩ Iic b ∩ Iic c = Ioc a (b ⊓ c)
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : SemilatticeInf α
a b c : α
⊢ Ioi a ∩ Iic b ∩ Iic c = Ioc a (b ⊓ c)

Tactic:
← Ioi_inter_Iic,

Goal state after:
α : Type u_1
inst✝ : SemilatticeInf α
a b c : α
⊢ Ioi a ∩ Iic b ∩ Iic c = Ioi a ∩ Iic (b ⊓ c)
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : SemilatticeInf α
a b c : α
⊢ Ioi a ∩ Iic b ∩ Iic c = Ioi a ∩ Iic (b ⊓ c)

Tactic:
inter_assoc,

Goal state after:
α : Type u_1
inst✝ : SemilatticeInf α
a b c : α
⊢ Ioi a ∩ (Iic b ∩ Iic c) = Ioi a ∩ Iic (b ⊓ c)
Module: Mathlib.Algebra.BigOperators.Group.List.Defs

Goal state before:
pp: case succ
M : Type u_2
inst✝ : Monoid M
a : M
n : ℕ
ih : (replicate n a).prod = a ^ n
⊢ a * a ^ n = a ^ (n + 1)

Tactic:
pow_succ'

Goal state after:
case succ
M : Type u_2
inst✝ : Monoid M
a : M
n : ℕ
ih : (replicate n a).prod = a ^ n
⊢ a * a ^ n = a * a ^ n
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 / c ≤ b / c ↔ b ≤ a

Tactic:
by
  rw [div_le_iff_of_neg hc, div_mul_cancel₀ _ hc.ne]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ : List β
h : Forall₂ R l₁.reverse l₂.reverse
⊢ Forall₂ R l₁.reverse.reverse l₂

Tactic:
← reverse_reverse l₂

Goal state after:
α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ : List β
h : Forall₂ R l₁.reverse l₂.reverse
⊢ Forall₂ R l₁.reverse.reverse l₂.reverse.reverse
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: case inl
α : Type u_1
n : ℕ
a : α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
hn₁ : l₁.length < n
⊢ l₁.insertIdx n a ~ l₂.insertIdx n a ↔ l₁ ~ l₂

Tactic:
| inl hn₁ =>

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 : some l₁[m] = l₂[n]?
⊢ l₁.eraseIdx m ~ l₂.eraseIdx n ↔ l₁ ~ l₂

Tactic:
eq_comm,

Goal state after:
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₂
Module: Mathlib.Data.List.Perm.Basic

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

Tactic:
eq_comm,

Goal state after:
case inr
α : Type u_1
l₁ l₂ : List α
m n : ℕ
h : l₂[n]? = none
hm : m ≥ l₁.length
⊢ l₁.eraseIdx m ~ l₂.eraseIdx n ↔ l₁ ~ l₂
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
l : List α
f g : α → List β
h : ∀ (a : α), a ∈ l → f a ~ g a
⊢ Forall₂ (fun x1 x2 ↦ x1 ~ x2) (List.map f l) (List.map g l)

Tactic:
rwa [List.forall₂_map_right_iff, List.forall₂_map_left_iff, List.forall₂_same]

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

Goal state before:
pp: α : Type u
m : ℕ
a : α
⊢ (replicate (m + 1) a).getLast ⋯ = a

Tactic:
by
  simp only [replicate_succ']
  exact getLast_append_singleton _

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

Goal state before:
pp: M : Type u_1
inst✝ : GroupWithZero M
r : ℤ
x : M
hx : x ≠ 0
l : NF M
hl : l.eval ≠ 0
⊢ (map
        (fun x ↦
          match x with
          | (r, x) => zpow' x r)
        ((r, x) :: l)).prod ≠
    0

Tactic:
apply mul_ne_zero ?_ hl

Goal state after:
M : Type u_1
inst✝ : GroupWithZero M
r : ℤ
x : M
hx : x ≠ 0
l : NF M
hl : l.eval ≠ 0
⊢ (fun x ↦
        match x with
        | (r, x) => zpow' x r)
      (r, x) ≠
    0
Module: Mathlib.Data.Rat.Defs

Goal state before:
pp: q : ℚ
n : ℕ
⊢ { num := q.num ^ n, den := q.den ^ n, den_nz := ⋯, reduced := ⋯ } = q.num ^ n /. ↑q.den ^ n

Tactic:
mk_eq_divInt,

Goal state after:
q : ℚ
n : ℕ
⊢ q.num ^ n /. ↑(q.den ^ n) = q.num ^ n /. ↑q.den ^ n
Module: Mathlib.Algebra.GroupWithZero.Divisibility

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
a : α
inst✝ : Subsingleton αˣ
c d : α
hcd : a = a * (c * d)
⊢ a = a * c

Tactic:
eq_comm,

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
a : α
inst✝ : Subsingleton αˣ
c d : α
hcd : a * (c * d) = a
⊢ a = a * c
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: case neg
a b : ℤ
b0 : ¬b = 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a /. b = { num := n, den := d, den_nz := h, reduced := c }
⊢ ↑{ num := n, den := d, den_nz := h, reduced := c }.den ∣ b

Tactic:
mk_eq_divInt,

Goal state after:
case neg
a b : ℤ
b0 : ¬b = 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a /. b = n /. ↑d
⊢ ↑{ num := n, den := d, den_nz := h, reduced := c }.den ∣ b
Module: Mathlib.Data.Rat.Cast.CharZero

Goal state before:
pp: α : Type u_3
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n₁ : ℤ
d₁ : ℕ
d₁0 : d₁ ≠ 0
c₁ : n₁.natAbs.Coprime d₁
n₂ : ℤ
d₂ : ℕ
d₂0 : d₂ ≠ 0
c₂ : n₂.natAbs.Coprime d₂
h : ↑{ num := n₁, den := d₁, den_nz := d₁0, reduced := c₁ } = ↑{ num := n₂, den := d₂, den_nz := d₂0, reduced := c₂ }
d₁a : ↑d₁ ≠ 0
d₂a : ↑d₂ ≠ 0
⊢ { num := n₁, den := d₁, den_nz := d₁0, reduced := c₁ } = { num := n₂, den := d₂, den_nz := d₂0, reduced := c₂ }

Tactic:
mk_eq_divInt,

Goal state after:
α : Type u_3
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n₁ : ℤ
d₁ : ℕ
d₁0 : d₁ ≠ 0
c₁ : n₁.natAbs.Coprime d₁
n₂ : ℤ
d₂ : ℕ
d₂0 : d₂ ≠ 0
c₂ : n₂.natAbs.Coprime d₂
h : ↑(n₁ /. ↑d₁) = ↑{ num := n₂, den := d₂, den_nz := d₂0, reduced := c₂ }
d₁a : ↑d₁ ≠ 0
d₂a : ↑d₂ ≠ 0
⊢ n₁ /. ↑d₁ = { num := n₂, den := d₂, den_nz := d₂0, reduced := c₂ }
Module: Mathlib.Data.Rat.Cast.CharZero

Goal state before:
pp: α : Type u_3
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n₁ : ℤ
d₁ : ℕ
d₁0 : d₁ ≠ 0
c₁ : n₁.natAbs.Coprime d₁
n₂ : ℤ
d₂ : ℕ
d₂0 : d₂ ≠ 0
c₂ : n₂.natAbs.Coprime d₂
d₁a : ↑d₁ ≠ 0
d₂a : ↑d₂ ≠ 0
h : ↑n₁ * ↑d₂ / ↑d₁ = ↑n₂
⊢ n₁ /. ↑d₁ = n₂ /. ↑d₂

Tactic:
eq_comm,

Goal state after:
α : Type u_3
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n₁ : ℤ
d₁ : ℕ
d₁0 : d₁ ≠ 0
c₁ : n₁.natAbs.Coprime d₁
n₂ : ℤ
d₂ : ℕ
d₂0 : d₂ ≠ 0
c₂ : n₂.natAbs.Coprime d₂
d₁a : ↑d₁ ≠ 0
d₂a : ↑d₂ ≠ 0
h : ↑n₂ = ↑n₁ * ↑d₂ / ↑d₁
⊢ n₁ /. ↑d₁ = n₂ /. ↑d₂
Module: Mathlib.Data.Rat.Cast.CharZero

Goal state before:
pp: α : Type u_3
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n₁ : ℤ
d₁ : ℕ
d₁0 : d₁ ≠ 0
c₁ : n₁.natAbs.Coprime d₁
n₂ : ℤ
d₂ : ℕ
d₂0 : d₂ ≠ 0
c₂ : n₂.natAbs.Coprime d₂
d₁a : ↑d₁ ≠ 0
d₂a : ↑d₂ ≠ 0
h : ↑n₂ * ↑d₁ = ↑n₁ * ↑d₂
⊢ n₁ /. ↑d₁ = n₂ /. ↑d₂

Tactic:
eq_comm,

Goal state after:
α : Type u_3
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n₁ : ℤ
d₁ : ℕ
d₁0 : d₁ ≠ 0
c₁ : n₁.natAbs.Coprime d₁
n₂ : ℤ
d₂ : ℕ
d₂0 : d₂ ≠ 0
c₂ : n₂.natAbs.Coprime d₂
d₁a : ↑d₁ ≠ 0
d₂a : ↑d₂ ≠ 0
h : ↑n₁ * ↑d₂ = ↑n₂ * ↑d₁
⊢ n₁ /. ↑d₁ = n₂ /. ↑d₂
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: q : ℚ
⊢ (q * q).den = q.den * q.den

Tactic:
rw [Rat.mul_den, Int.natAbs_mul, Nat.Coprime.gcd_eq_one, Nat.div_one]
  exact (q.reduced.mul_right q.reduced).mul_left (q.reduced.mul_right q.reduced)

Goal state after:
Module: Mathlib.Data.Rat.Cast.CharZero

Goal state before:
pp: α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
a b : ℕ
⊢ ↑(divNat a b) = ↑(↑a / ↑b)

Tactic:
apply Rat.mkRat_eq_div

Goal state after:
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: α : Type u_3
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a /. b = n /. ↑d
d0 : ↑d ≠ 0
this : ↑a * ↑d = ↑n * ↑b
⊢ ↑{ num := n, den := d, den_nz := h, reduced := c } = ↑a / ↑b

Tactic:
eq_comm,

Goal state after:
α : Type u_3
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a /. b = n /. ↑d
d0 : ↑d ≠ 0
this : ↑a * ↑d = ↑n * ↑b
⊢ ↑a / ↑b = ↑{ num := n, den := d, den_nz := h, reduced := c }
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
s : Set β
f : β → α
⊢ sSup (f '' s) = ⨆ a ∈ s, f a

Tactic:
by
  rw [← iSup_subtype'', sSup_image']

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

Goal state before:
pp: case pos.a
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
B : BddAbove s ∨ BddAbove t
Bs : BddAbove s
Bt : BddAbove t
⊢ sSup s ≤ sSup t

pp: case a
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
B : BddAbove s ∨ BddAbove t
Bs : BddAbove s
Bt : BddAbove t
⊢ sSup t ≤ sSup s

Tactic:
· apply csSup_le s_ne (fun x hx ↦ ?_)
      rcases hs x hx with ⟨y, yt, hxy⟩
      exact hxy.trans (le_csSup Bt yt)

Goal state after:
case a
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
B : BddAbove s ∨ BddAbove t
Bs : BddAbove s
Bt : BddAbove t
⊢ sSup t ≤ sSup s
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:
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.Interval.Set.UnorderedInterval

Goal state before:
pp: case inl
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a < b
⊢ uIoo a b = Ioo a b ∪ Ioo b a

Tactic:
simp [uIoo_of_lt, h, Ioo_eq_empty_of_le h.le]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝ : Std.Refl r
f : β → α
c : Set β
h : IsChain (f ⁻¹'o r) c
x✝¹ x✝ : { a // a ∈ c }
a : β
ha : a ∈ c
b : β
hb : b ∈ c
hab : a = b
⊢ ∃ z, r ((fun x ↦ f ↑x) ⟨a, ha⟩) ((fun x ↦ f ↑x) z) ∧ r ((fun x ↦ f ↑x) ⟨b, hb⟩) ((fun x ↦ f ↑x) z)

Tactic:
simp only [hab, exists_prop, and_self_iff, Subtype.exists]

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝ : Std.Refl r
f : β → α
c : Set β
h : IsChain (f ⁻¹'o r) c
x✝¹ x✝ : { a // a ∈ c }
a : β
ha : a ∈ c
b : β
hb : b ∈ c
hab : a = b
⊢ ∃ a ∈ c, r (f b) (f a)