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

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

Tactic:
rcases emod_two_eq_zero_or_one m with h₁ | h₁ <;>
  rcases emod_two_eq_zero_or_one n with h₂ | h₂

Goal state after:
case inl.inl
m n : ℤ
h₁ : m % 2 = 0
h₂ : n % 2 = 0
⊢ Even (m * n) ↔ Even m ∨ Even n

case inl.inr
m n : ℤ
h₁ : m % 2 = 0
h₂ : n % 2 = 1
⊢ Even (m * n) ↔ Even m ∨ Even n

case inr.inl
m n : ℤ
h₁ : m % 2 = 1
h₂ : n % 2 = 0
⊢ Even (m * n) ↔ Even m ∨ Even n

case inr.inr
m n : ℤ
h₁ : m % 2 = 1
h₂ : n % 2 = 1
⊢ Even (m * n) ↔ Even m ∨ Even n
Module: Mathlib.Algebra.Group.Nat.Hom

Goal state before:
pp: M : Type u_1
inst✝ : AddMonoid M
f : ℕ →+ M
n : ℕ
⊢ f n = n • (multiplesHom M).symm f

Tactic:
← multiplesHom_apply,

Goal state after:
M : Type u_1
inst✝ : AddMonoid M
f : ℕ →+ M
n : ℕ
⊢ f n = ((multiplesHom M) ((multiplesHom M).symm f)) n
Module: Mathlib.Algebra.Group.Nat.Hom

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
f g : Multiplicative ℕ →* M
h : f (ofAdd 1) = g (ofAdd 1)
n : Multiplicative ℕ
⊢ f n = g n

Tactic:
f.apply_mnat,

Goal state after:
M : Type u_1
inst✝ : Monoid M
f g : Multiplicative ℕ →* M
h : f (ofAdd 1) = g (ofAdd 1)
n : Multiplicative ℕ
⊢ f (ofAdd 1) ^ toAdd n = g n
Module: Mathlib.Data.List.TFAE

Goal state before:
pp: p : Prop
⊢ [p].TFAE

Tactic:
simp [TFAE, -eq_iff_iff]

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

Goal state before:
pp: case tail.tail
a b : Prop
l : List Prop
h : b ∈ l
ab : a ↔ b
H : l.TFAE
p : Prop
hp : Mem p l
q : Prop
hq : Mem q l
⊢ p ↔ q

Tactic:
· exact H _ hp _ hq

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

Goal state before:
pp: R : Type u_1
inst✝¹ : DivisionMonoid R
inst✝ : HasDistribNeg R
a : R
⊢ 1 / a * (1 / -1) = 1 / a * -1

Tactic:
rw [one_div_neg_one_eq_neg_one]

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
u : Mˣ
a : M
⊢ Commute (↑u) a ↔ ↑u * a * ↑u⁻¹ = a

Tactic:
by
  rw [Units.mul_inv_eq_iff_eq_mul, Commute, SemiconjBy]

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
a : R
inst✝ : NoZeroDivisors R
⊢ a ^ 2 = 1 ↔ a = 1 ∨ a = -1

Tactic:
← (Commute.one_right a).sq_eq_sq_iff_eq_or_eq_neg,

Goal state after:
R : Type u
inst✝¹ : Ring R
a : R
inst✝ : NoZeroDivisors R
⊢ a ^ 2 = 1 ↔ a ^ 2 = 1 ^ 2
Module: Mathlib.Algebra.Ring.InjSurj

Goal state before:
pp: R : Type u_1
S : Type u_2
f : R → S
hf : Surjective f
inst✝¹² : Add S
inst✝¹¹ : Mul S
inst✝¹⁰ : Zero S
inst✝⁹ : One S
inst✝⁸ : Neg S
inst✝⁷ : Sub S
inst✝⁶ : SMul ℕ S
inst✝⁵ : SMul ℤ S
inst✝⁴ : Pow S ℕ
inst✝³ : NatCast S
inst✝² : IntCast S
inst✝¹ : Mul R
inst✝ : HasDistribNeg R
neg : ∀ (a : R), f (-a) = -f a
mul : ∀ (a b : R), f (a * b) = f a * f b
x y : R
⊢ f (-x) * f y = -(f x * f y)

Tactic:
← mul,

Goal state after:
R : Type u_1
S : Type u_2
f : R → S
hf : Surjective f
inst✝¹² : Add S
inst✝¹¹ : Mul S
inst✝¹⁰ : Zero S
inst✝⁹ : One S
inst✝⁸ : Neg S
inst✝⁷ : Sub S
inst✝⁶ : SMul ℕ S
inst✝⁵ : SMul ℤ S
inst✝⁴ : Pow S ℕ
inst✝³ : NatCast S
inst✝² : IntCast S
inst✝¹ : Mul R
inst✝ : HasDistribNeg R
neg : ∀ (a : R), f (-a) = -f a
mul : ∀ (a b : R), f (a * b) = f a * f b
x y : R
⊢ f (-x * y) = -(f x * f y)
Module: Mathlib.Algebra.Ring.InjSurj

Goal state before:
pp: R : Type u_1
S : Type u_2
f : R → S
hf : Surjective f
inst✝¹² : Add S
inst✝¹¹ : Mul S
inst✝¹⁰ : Zero S
inst✝⁹ : One S
inst✝⁸ : Neg S
inst✝⁷ : Sub S
inst✝⁶ : SMul ℕ S
inst✝⁵ : SMul ℤ S
inst✝⁴ : Pow S ℕ
inst✝³ : NatCast S
inst✝² : IntCast S
inst✝¹ : Mul R
inst✝ : HasDistribNeg R
neg : ∀ (a : R), f (-a) = -f a
mul : ∀ (a b : R), f (a * b) = f a * f b
x y : R
⊢ f x * f (-y) = -(f x * f y)

Tactic:
← mul,

Goal state after:
R : Type u_1
S : Type u_2
f : R → S
hf : Surjective f
inst✝¹² : Add S
inst✝¹¹ : Mul S
inst✝¹⁰ : Zero S
inst✝⁹ : One S
inst✝⁸ : Neg S
inst✝⁷ : Sub S
inst✝⁶ : SMul ℕ S
inst✝⁵ : SMul ℤ S
inst✝⁴ : Pow S ℕ
inst✝³ : NatCast S
inst✝² : IntCast S
inst✝¹ : Mul R
inst✝ : HasDistribNeg R
neg : ∀ (a : R), f (-a) = -f a
mul : ∀ (a b : R), f (a * b) = f a * f b
x y : R
⊢ f (x * -y) = -(f x * f y)
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝ : Semiring α
a : α
ha : Even a
n : ℕ
x✝ : n + 1 ≠ 0
⊢ Even (a ^ (n + 1))

Tactic:
by rw [pow_succ]; exact ha.mul_left _

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

Goal state before:
pp: α : Type u_2
inst✝ : Semiring α
a b : α
⊢ Even (2 * a + 1 + (2 * b + 1))

Tactic:
refine ⟨a + b + 1, ?_⟩

Goal state after:
α : Type u_2
inst✝ : Semiring α
a b : α
⊢ 2 * a + 1 + (2 * b + 1) = a + b + 1 + (a + b + 1)
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a₁ a₂ b₁ b₂ : α
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
⊢ a₂ * b₂ ≤ a₁ * b₁ ↔ a₁ = a₂ ∧ b₁ = b₂

Tactic:
by
  have := mulLeftMono_of_mulLeftStrictMono α
  have := mulRightMono_of_mulRightStrictMono α
  refine ⟨fun h ↦ ?_, by rintro ⟨rfl, rfl⟩; rfl⟩
  simp only [eq_iff_le_not_lt, ha, hb, true_and]
  refine ⟨fun ha ↦ h.not_gt ?_, fun hb ↦ h.not_gt ?_⟩
  exacts [mul_lt_mul_of_lt_of_le ha hb, mul_lt_mul_of_le_of_lt ha hb]

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

Goal state before:
pp: case h
α : Type u_1
inst✝² : MulOneClass α
inst✝¹ : LinearOrder α
inst✝ : MulLeftStrictMono α
a : α
h : a < 1
this : a * a < a * 1
⊢ a * a ≤ a

Tactic:
rw [mul_one] at this

Goal state after:
case h
α : Type u_1
inst✝² : MulOneClass α
inst✝¹ : LinearOrder α
inst✝ : MulLeftStrictMono α
a : α
h : a < 1
this : a * a < a
⊢ a * a ≤ a
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : Preorder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : MulPosMono R
inst✝¹ : AddRightMono R
inst✝ : AddRightReflectLE R
h : b ≤ a
hc : c ≤ 0
d : R
hcd : 0 = c + d
⊢ a * d = b * c + (b * d + a * d)

Tactic:
by rw [← add_assoc, ← mul_add, ← hcd, mul_zero, zero_add]

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

Goal state before:
pp: R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : PartialOrder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : MulPosStrictMono R
inst✝¹ : AddRightStrictMono R
inst✝ : AddRightReflectLT R
h : b < a
hc : c < 0
d : R
hcd : 0 = c + d
⊢ a * d = b * c + (b * d + a * d)

Tactic:
by rw [← add_assoc, ← mul_add, ← hcd, mul_zero, zero_add]

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

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b : G₀
ha : 0 < a
⊢ a⁻¹ * b < 1 ↔ b < a

Tactic:
by rw [inv_mul_lt_iff₀ ha, mul_one]

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

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : ZeroLEOneClass G₀
ha : 1 ≤ a
n : ℤ
⊢ a ^ n ≤ a ^ (n + 1)

Tactic:
rw [zpow_add_one₀ (zero_lt_one.trans_le ha).ne']

Goal state after:
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : ZeroLEOneClass G₀
ha : 1 ≤ a
n : ℤ
⊢ a ^ n ≤ a ^ n * a
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Irrefl s
f : α → β
hf : ∀ {x y : α}, r x y → s (f x) (f y)
x y : α
hxy : f x = f y
h : r x y
this : s (f y) (f y)
⊢ x = y

Tactic:
exfalso

Goal state after:
case inl
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Irrefl s
f : α → β
hf : ∀ {x y : α}, r x y → s (f x) (f y)
x y : α
hxy : f x = f y
h : r x y
this : s (f y) (f y)
⊢ False
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: case inr.inr
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Irrefl s
f : α → β
hf : ∀ {x y : α}, r x y → s (f x) (f y)
x y : α
hxy : f x = f y
h : r y x
this : s (f y) (f y)
⊢ x = y

Tactic:
exfalso

Goal state after:
case inr.inr
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Irrefl s
f : α → β
hf : ∀ {x y : α}, r x y → s (f x) (f y)
x y : α
hxy : f x = f y
h : r y x
this : s (f y) (f y)
⊢ False
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: α : Type u_6
β : Type u_7
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
x : α
| IsMax x

Tactic:
← f.symm_apply_apply x

Goal state after:
α : Type u_6
β : Type u_7
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
x : α
| IsMax (f.symm (f x))
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: case succ
M : Type u_1
inst✝ : Monoid M
n m : ℕ
y : Mˣ
hn : y ^ ↑n = 1
hm : y ^ ↑(m + 1) = 1
⊢ y ^ (↑(m + 1) * (m + 1).gcdA n + ↑n * (m + 1).gcdB n) = 1

Tactic:
zpow_add,

Goal state after:
case succ
M : Type u_1
inst✝ : Monoid M
n m : ℕ
y : Mˣ
hn : y ^ ↑n = 1
hm : y ^ ↑(m + 1) = 1
⊢ y ^ (↑(m + 1) * (m + 1).gcdA n) * y ^ (↑n * (m + 1).gcdB n) = 1
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: case neg.refine_1
α : 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
ha : ¬a = 0
⊢ a ^ (↑m * m.gcdA n) * a ^ (↑n * m.gcdB n) = a ^ (↑n * m.gcdB n) * b ^ (↑n * m.gcdA n)

Tactic:
simp only [zpow_mul, zpow_natCast, h]

Goal state after:
case neg.refine_1
α : 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
ha : ¬a = 0
⊢ (b ^ n) ^ m.gcdA n * (a ^ n) ^ m.gcdB n = (a ^ n) ^ m.gcdB n * (b ^ n) ^ m.gcdA n
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: case neg.refine_2
α : 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
ha : ¬a = 0
⊢ b ^ (↑m * m.gcdA n) * b ^ (↑n * m.gcdB n) = a ^ (↑m * m.gcdB n) * b ^ (↑m * m.gcdA n)

Tactic:
simp only [zpow_mul, zpow_natCast, h]

Goal state after:
case neg.refine_2
α : 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
ha : ¬a = 0
⊢ (b ^ m) ^ m.gcdA n * (b ^ n) ^ m.gcdB n = (b ^ n) ^ m.gcdB n * (b ^ m) ^ m.gcdA n
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DivInvMonoid α
n : ℕ
⊢ none ^ ↑n.succ = none ^ ↑n * none

Tactic:
change 0 ^ _ = 0 ^ _ * 0; simp only [mul_zero]; rfl

Goal state after:
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 c : α
h : a ≤ a + c
⊢ a + (a + c - a) ≤ a + c

Tactic:
add_tsub_le_left

Goal state after:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a c : α
h : a ≤ a + c
⊢ a + c ≤ a + c
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case none.none
α : Type u
inst✝ : Add α
a : α
ha : IsAddLeftRegular a
⊢ (fun x ↦ ↑a + x) none = (fun x ↦ ↑a + x) none → none = none

Tactic:
simp [none_eq_bot, some_eq_coe, ← coe_add]

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

Goal state before:
pp: case none.some
α : Type u
inst✝ : Add α
a : α
ha : IsAddLeftRegular a
c : α
⊢ (fun x ↦ ↑a + x) none = (fun x ↦ ↑a + x) (Option.some c) → none = Option.some c

Tactic:
simp [none_eq_bot, some_eq_coe, ← coe_add]

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

Goal state before:
pp: case some.none
α : Type u
inst✝ : Add α
a : α
ha : IsAddLeftRegular a
b : α
⊢ (fun x ↦ ↑a + x) (Option.some b) = (fun x ↦ ↑a + x) none → Option.some b = none

Tactic:
simp [none_eq_bot, some_eq_coe, ← coe_add]

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

Goal state before:
pp: case some.some
α : Type u
inst✝ : Add α
a : α
ha : IsAddLeftRegular a
b c : α
⊢ (fun x ↦ ↑a + x) (Option.some b) = (fun x ↦ ↑a + x) (Option.some c) → Option.some b = Option.some c

Tactic:
simp [none_eq_bot, some_eq_coe, ← coe_add]

Goal state after:
case some.some
α : Type u
inst✝ : Add α
a : α
ha : IsAddLeftRegular a
b c : α
⊢ a + b = a + c → b = c
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case none.none
α : Type u
inst✝ : Add α
a : α
ha : IsAddRightRegular a
⊢ (fun x ↦ x + ↑a) none = (fun x ↦ x + ↑a) none → none = none

Tactic:
simp [none_eq_bot, some_eq_coe, ← coe_add]

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

Goal state before:
pp: case none.some
α : Type u
inst✝ : Add α
a : α
ha : IsAddRightRegular a
c : α
⊢ (fun x ↦ x + ↑a) none = (fun x ↦ x + ↑a) (Option.some c) → none = Option.some c

Tactic:
simp [none_eq_bot, some_eq_coe, ← coe_add]

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

Goal state before:
pp: case some.none
α : Type u
inst✝ : Add α
a : α
ha : IsAddRightRegular a
b : α
⊢ (fun x ↦ x + ↑a) (Option.some b) = (fun x ↦ x + ↑a) none → Option.some b = none

Tactic:
simp [none_eq_bot, some_eq_coe, ← coe_add]

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

Goal state before:
pp: case some.some
α : Type u
inst✝ : Add α
a : α
ha : IsAddRightRegular a
b c : α
⊢ (fun x ↦ x + ↑a) (Option.some b) = (fun x ↦ x + ↑a) (Option.some c) → Option.some b = Option.some c

Tactic:
simp [none_eq_bot, some_eq_coe, ← coe_add]

Goal state after:
case some.some
α : Type u
inst✝ : Add α
a : α
ha : IsAddRightRegular a
b c : α
⊢ b + a = c + a → b = c
Module: Mathlib.Data.Nat.Find

Goal state before:
pp: case mpr
m : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
⊢ (p m ∧ ∀ (n : ℕ), n < m → ¬p n) → Nat.find h = m

Tactic:
rintro ⟨hm, hlt⟩

Goal state after:
case mpr
m : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
hm : p m
hlt : ∀ (n : ℕ), n < m → ¬p n
⊢ Nat.find h = m
Module: Mathlib.Data.Int.LeastGreatest

Goal state before:
pp: P : ℤ → Prop
inst✝ : DecidablePred P
b : ℤ
Hb : ∀ (z : ℤ), P z → z ≤ b
Hinh : ∃ z, P z
Hbdd' : ∀ (z : ℤ), P (-z) → -b ≤ z
elt : ℤ
Helt : P elt
⊢ P elt

Tactic:
exact Helt

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
x y : WithZero α
inst✝ : NoMinOrder α
hx : x ≠ 0
hy : y ≠ 0
⊢ ∃ z, z ≠ 0 ∧ z < x ∧ z < y

Tactic:
by
  obtain ⟨z', hnz', hzx, hzy⟩ := exists_ne_zero_and_le_and_le hx hy
  obtain ⟨z, hnz, hlt⟩ := exists_ne_zero_and_lt hnz'
  use z, hnz
  constructor <;> exact lt_of_lt_of_le hlt ‹z' ≤ _›

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

Goal state before:
pp: x : WithZero (Multiplicative ℤ)
hx : x ≠ 0
y : WithZero (Multiplicative ℤ)
hnz : y ≠ 0
hyx : y < x
⊢ exp (-↑(-y.log).toNat) ≤ y

Tactic:
← WithZero.le_log_iff_exp_le hnz,

Goal state after:
x : WithZero (Multiplicative ℤ)
hx : x ≠ 0
y : WithZero (Multiplicative ℤ)
hnz : y ≠ 0
hyx : y < x
⊢ -↑(-y.log).toNat ≤ y.log
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
n a : ℕ
⊢ ⌈↑n⌉₊ ≤ a ↔ n ≤ a

Tactic:
rw [ceil_le, cast_le]

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

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
a b : R
inst✝¹ : Invertible a
inst✝ : Invertible b
⊢ ⅟a + ⅟b = ⅟a * (a + b) * ⅟b

Tactic:
by
  rw [mul_add, invOf_mul_self, add_mul, one_mul, mul_assoc, mul_invOf_self, mul_one, add_comm]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
s : Set β
x : β
⊢ IsLUB (⇑f ⁻¹' s) (f.symm x) ↔ IsLUB s x

Tactic:
rw [isLUB_preimage, f.apply_symm_apply]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
β : Type u_4
inst✝ : Preorder β
s : Set (α × β)
hs : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
⊢ IsCofinalFor ((Prod.fst '' s) ×ˢ (Prod.snd '' s)) s

Tactic:
by
  rintro ⟨_, _⟩ ⟨⟨x, hx, rfl⟩, y, hy, rfl⟩
  obtain ⟨z, hz, hxz, hyz⟩ := hs _ hx _ hy
  exact ⟨z, hz, hxz.1, hyz.2⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a : α
s : Set α
ho : Iio a ⊆ s
hc : s ⊆ Iic a
h : a ∈ s
⊢ Iic a ⊆ s

Tactic:
← Iio_union_right,

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
a : α
s : Set α
ho : Iio a ⊆ s
hc : s ⊆ Iic a
h : a ∈ s
⊢ Iio a ∪ {a} ⊆ s
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
ε : α
hε : 0 < ε
n : ℕ
B : α
B_pos : 0 < B
⊢ ∃ δ > 0, ∀ (q r : α), |r| ≤ B → |q - r| ≤ δ → |q ^ n - r ^ n| < ε

Tactic:
have pos : 0 < 1 + ↑n * (B + 1) ^ (n - 1) := zero_lt_one.trans_le <| le_add_of_nonneg_right <|
    mul_nonneg n.cast_nonneg <| (pow_pos (B_pos.trans <| lt_add_of_pos_right _ zero_lt_one) _).le

Goal state after:
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
ε : α
hε : 0 < ε
n : ℕ
B : α
B_pos : 0 < B
pos : 0 < 1 + ↑n * (B + 1) ^ (n - 1)
⊢ ∃ δ > 0, ∀ (q r : α), |r| ≤ B → |q - r| ≤ δ → |q ^ n - r ^ n| < ε
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: case mp.cons
α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ : List β
a : α
b : β
l1 : List α
l2 : List β
rab : R a b
a✝ : SublistForall₂ R l1 l2
ih : ∃ l, Forall₂ R l1 l ∧ l <+ l2
⊢ ∃ l, Forall₂ R (a :: l1) l ∧ l <+ b :: l2

Tactic:
| @cons a b l1 l2 rab _ ih =>

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

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

Tactic:
| inl hn₂ =>

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

Goal state before:
pp: α : Type u
β : Type v
l₁ l₂ : List α
f : α → β
h : Injective f
h2 : map f l₁ ⊆ map f l₂
x : α
hx : x ∈ l₁
x' : α
hx' : x' ∈ l₂
hxx' : f x' = f x
⊢ x ∈ l₂

Tactic:
cases h hxx'

Goal state after:
case refl
α : Type u
β : Type v
l₁ l₂ : List α
f : α → β
h : Injective f
h2 : map f l₁ ⊆ map f l₂
x : α
hx : x ∈ l₁
hx' : x ∈ l₂
hxx' : f x = f x
⊢ x ∈ l₂
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
l : List α
⊢ (Surjective fun n ↦ l[n]?) ↔ ∀ (x : α), x ∈ l

Tactic:
refine ⟨fun h x ↦ mem_iff_getElem?.mpr <| h x, fun h x ↦ ?_⟩

Goal state after:
α : Type u
l : List α
h : ∀ (x : α), x ∈ l
x : Option α
⊢ ∃ a, (fun n ↦ l[n]?) a = x
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: case e'_4
M : Type u_1
inst✝ : CommGroupWithZero M
l : NF M
⊢ ((fun x ↦ zpow' x.2 x.1) ∘ fun x ↦ (-x.1, x.2)) = (fun x ↦ x⁻¹) ∘ fun x ↦ zpow' x.2 x.1

Tactic:
ext p

Goal state after:
case e'_4
M : Type u_1
inst✝ : CommGroupWithZero M
l : NF M
p : ℤ × M
⊢ ((fun x ↦ zpow' x.2 x.1) ∘ fun x ↦ (-x.1, x.2)) p = ((fun x ↦ x⁻¹) ∘ fun x ↦ zpow' x.2 x.1) p
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : CommGroupWithZero M
l : NF M
r : ℤ
⊢ ((fun x ↦ zpow' x.2 x.1) ∘ fun x ↦ (r * x.1, x.2)) = (fun x ↦ zpow' x r) ∘ fun x ↦ zpow' x.2 x.1

Tactic:
ext p

Goal state after:
M : Type u_1
inst✝ : CommGroupWithZero M
l : NF M
r : ℤ
p : ℤ × M
⊢ ((fun x ↦ zpow' x.2 x.1) ∘ fun x ↦ (r * x.1, x.2)) p = ((fun x ↦ zpow' x r) ∘ fun x ↦ zpow' x.2 x.1) p
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
β : Type v
f : α → β
⊢ Bijective (map f) ↔ Bijective f

Tactic:
simp_rw [Function.Bijective, map_injective_iff, map_surjective_iff]

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

Goal state before:
pp: a b : ℕ
hab : ↑a = ↑b
⊢ a = b

Tactic:
simpa using congr_arg num hab

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

Goal state before:
pp: q : ℚ
⊢ q * ↑q.den = ↑q.num

Tactic:
by
  suffices (q.num /. ↑q.den) * (↑q.den /. 1) = q.num /. 1 by simp_all
  have : (q.den : ℤ) ≠ 0 := mod_cast q.den_ne_zero
  rw [divInt_mul_divInt, mul_comm (q.den : ℤ) 1, divInt_mul_right this]

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

Goal state before:
pp: case pos
K : Type u_1
inst✝ : NNRatCast K
m : ℕ
b : Bool
d : ℕ
h✝ : b = true
⊢ OfScientific.ofScientific m b d = Rat.divInt ↑m ↑(10 ^ d)

Tactic:
rw [← Rat.ofScientific_eq_ofScientific, Rat.ofScientific_def, if_pos ‹_›]

Goal state after:
case pos
K : Type u_1
inst✝ : NNRatCast K
m : ℕ
b : Bool
d : ℕ
h✝ : b = true
⊢ mkRat (↑(OfNat.ofNat m)) (10 ^ OfNat.ofNat d) = Rat.divInt ↑m ↑(10 ^ d)
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: case inr.refine_2
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
this : q.num * d = n * ↑q.den
hqdn : q.num ∣ n
⊢ d = n / q.num * ↑q.den

Tactic:
refine Int.eq_mul_div_of_mul_eq_mul_of_dvd_left ?_ hqdn this
    rw [qdf]
    exact Rat.num_ne_zero.2 ((divInt_ne_zero hd).mpr hn)

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

Goal state before:
pp: α : Type u_3
inst✝ : DivisionRing α
p q : ℚ
hp : ↑p.den ≠ 0
hq : ↑q.num ≠ 0
⊢ ↑(p / q) = ↑p / ↑q

Tactic:
by
  rw [div_def', cast_divInt_of_ne_zero, cast_def, cast_def, div_eq_mul_inv (_ / _), inv_div,
    (Int.commute_cast _ _).div_mul_div_comm (Nat.commute_cast _ _)]
  · push_cast
    rfl
  · push_cast
    exact mul_ne_zero hp hq

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

Goal state before:
pp: F : Type u_1
α : Type u_3
β : Type u_4
inst✝³ : FunLike F α β
inst✝² : DivisionSemiring α
inst✝¹ : DivisionSemiring β
inst✝ : RingHomClass F α β
f : F
q : ℚ≥0
⊢ f (↑q.num / ↑q.den) = ↑q.num / ↑q.den

Tactic:
map_div₀,

Goal state after:
F : Type u_1
α : Type u_3
β : Type u_4
inst✝³ : FunLike F α β
inst✝² : DivisionSemiring α
inst✝¹ : DivisionSemiring β
inst✝ : RingHomClass F α β
f : F
q : ℚ≥0
⊢ f ↑q.num / f ↑q.den = ↑q.num / ↑q.den
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: F : Type u_1
α : Type u_3
β : Type u_4
inst✝³ : FunLike F α β
inst✝² : DivisionRing α
inst✝¹ : DivisionRing β
inst✝ : RingHomClass F α β
f : F
q : ℚ
⊢ f (↑q.num / ↑q.den) = ↑q

Tactic:
map_div₀,

Goal state after:
F : Type u_1
α : Type u_3
β : Type u_4
inst✝³ : FunLike F α β
inst✝² : DivisionRing α
inst✝¹ : DivisionRing β
inst✝ : RingHomClass F α β
f : F
q : ℚ
⊢ f ↑q.num / f ↑q.den = ↑q
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
S : Set (Set α)
⊢ ⋃₀ S = (⋂₀ (compl '' S))ᶜ

Tactic:
← compl_compl (⋃₀ S),

Goal state after:
α : Type u_1
S : Set (Set α)
⊢ (⋃₀ S)ᶜᶜ = (⋂₀ (compl '' S))ᶜ
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
s t : Set α
S : Set (Set α)
hs : t ∈ S
h : s ∩ ⋃₀ S = ∅
⊢ s ∩ t ⊆ s ∩ ⋃₀ S

Tactic:
exact inter_subset_inter_right _ (subset_sUnion_of_mem hs)

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α✝ : Type u
β✝ : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLinearOrder α✝
α : Type u
β : α → Type u
g : (a : α) → β a → α✝
lhs : α✝ := ⨅ a, ⨆ b, g a b
rhs : α✝ := ⨆ h, ⨅ a, g a (h a)
hrl : rhs < lhs
h : ∀ (x : α✝), x ≤ rhs ∨ lhs ≤ x
f : (a : α) → β a
hf : ∀ (a : α), rhs < g a (f a)
this : ∀ (a : α), lhs ≤ g a (f a)
⊢ lhs ≤ ⨅ a, g a (f a)

Tactic:
exact le_iInf fun a => this _

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

Goal state before:
pp: α : Type u_1
S : Set (Set α)
p : α → Prop
⊢ (∀ x ∈ ⋃₀ S, p x) ↔ ∀ s ∈ S, ∀ x ∈ s, p x

Tactic:
simp_rw [← iInf_Prop_eq, iInf_sUnion]

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

Goal state before:
pp: α : Type u
β : Type v
s : Set α
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
⊢ ¬MonotoneOn f s ∧ ¬AntitoneOn f s ↔
    ∃ a, a ∈ s ∧ ∃ b, b ∈ s ∧ ∃ c, c ∈ s ∧ a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)

Tactic:
simp [monotoneOn_iff_monotone, antitoneOn_iff_antitone, and_assoc, exists_and_left,
    not_monotone_not_antitone_iff_exists_le_le, @and_left_comm (_ ∈ s)]

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

Goal state before:
pp: case inr
α : 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 : α
hb : b ∈ upperBounds t
⊢ BddAbove s

Tactic:
refine ⟨b, fun x hx ↦ ?_⟩
        rcases hs x hx with ⟨y, hy, hxy⟩
        exact hxy.trans (hb hy)

Goal state after: