mathlib-initiative/mathlib-tactics huggingface dataset:
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 * ⅟↑da + ↑nb * ⅟↑db = ↑k * ↑nc * ⅟↑db * ⅟↑da
h₂ : ↑nc * ⅟↑dc = ↑nc * ↑k * ↑dc * ⅟↑db * ⅟↑da * ⅟↑dc
⊢ ↑k * ↑nc * ⅟↑db * ⅟↑da = ↑nc * ⅟↑dc

Tactic:
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 * ⅟↑da + ↑nb * ⅟↑db = ↑k * ↑nc * ⅟↑db * ⅟↑da
h₂ : ↑nc * ⅟↑dc = ↑nc * ↑k * ↑dc * ⅟↑db * ⅟↑da * ⅟↑dc
⊢ ↑k * ↑nc * ⅟↑db * ⅟↑da = ↑nc * ↑k * ↑dc * ⅟↑db * ⅟↑da * ⅟↑dc
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
h₂ : ↑nc * ⅟↑dc = ↑nc * ↑k * ↑dc * ⅟↑da * ⅟↑db * ⅟↑dc
⊢ ↑k * ↑nc * ⅟↑da * ⅟↑db = ↑nc * ⅟↑dc

Tactic:
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 * ⅟↑dc = ↑nc * ↑k * ↑dc * ⅟↑da * ⅟↑db * ⅟↑dc
⊢ ↑k * ↑nc * ⅟↑da * ⅟↑db = ↑nc * ↑k * ↑dc * ⅟↑da * ⅟↑db * ⅟↑dc
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: case inl
α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a b : α
inst✝ : IsStrictOrderedRing α
s : Set α
ha✝ : 0 ≤ a
hs : IsGLB s b
ha : 0 < a
⊢ IsGLB ((fun b ↦ a * b) '' s) (a * b)

pp: case inr
α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
b : α
inst✝ : IsStrictOrderedRing α
s : Set α
hs : IsGLB s b
ha : 0 ≤ 0
⊢ IsGLB ((fun b ↦ 0 * b) '' s) (0 * b)

Tactic:
· exact (OrderIso.mulLeft₀ _ ha).isGLB_image'.2 hs

Goal state after:
case inr
α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
b : α
inst✝ : IsStrictOrderedRing α
s : Set α
hs : IsGLB s b
ha : 0 ≤ 0
⊢ IsGLB ((fun b ↦ 0 * b) '' s) (0 * b)
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:
← neg_neg c,

Goal state after:
α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b c : α
hc : c < 0
⊢ a ≤ b / - -c ↔ b ≤ a * - -c
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
h₂ : ↑nc * ⅟↑dc = ↑nc * ↑k * ↑dc * ⅟↑da * ⅟↑db * ⅟↑dc
⊢ ↑k * ↑nc * ⅟↑da * ⅟↑db = ↑nc * ⅟↑dc

Tactic:
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 * ⅟↑dc = ↑nc * ↑k * ↑dc * ⅟↑da * ⅟↑db * ⅟↑dc
⊢ ↑k * ↑nc * ⅟↑da * ⅟↑db = ↑nc * ↑k * ↑dc * ⅟↑da * ⅟↑db * ⅟↑dc
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:
← neg_neg c,

Goal state after:
α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b c : α
hc : c < 0
⊢ a < b / - -c ↔ b < a * - -c
Module: Mathlib.Data.List.TakeDrop

Goal state before:
pp: case pos
α : Type u
a : α
l : List α
ih : ∀ (h : l ≠ []), drop (l.length - 1) l = [l.getLast h]
h : a :: l ≠ []
hl : l = []
⊢ drop ((a :: l).length - 1) (a :: l) = [(a :: l).getLast h]

Tactic:
simp_all

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

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a : α
a2 : 2 ≤ a
⊢ 1 = 2 * 2⁻¹

Tactic:
mul_inv_cancel₀ two_ne_zero

Goal state after:
α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a : α
a2 : 2 ≤ a
⊢ 1 = 1
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: case inl
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
hb : b < 0
⊢ 1 < a / b ↔ 0 < b ∧ b < a ∨ b < 0 ∧ a < b

Tactic:
simp [hb, hb.not_gt, one_lt_div_of_neg]

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

Goal state before:
pp: case zero.nil
α : Type u
a : α
hn : 0 ≠ [].length
⊢ ([].eraseIdx 0).insertIdx 0 a = [].set 0 a

Tactic:
simp_all

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

Goal state before:
pp: case zero.cons
α : Type u
a head✝ : α
tail✝ : List α
hn : 0 ≠ (head✝ :: tail✝).length
⊢ ((head✝ :: tail✝).eraseIdx 0).insertIdx 0 a = (head✝ :: tail✝).set 0 a

Tactic:
simp_all

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

Goal state before:
pp: case succ.nil
α : Type u
a : α
n✝ : ℕ
a✝ : ∀ {l : List α}, n✝ ≠ l.length → (l.eraseIdx n✝).insertIdx n✝ a = l.set n✝ a
hn : n✝ + 1 ≠ [].length
⊢ ([].eraseIdx (n✝ + 1)).insertIdx (n✝ + 1) a = [].set (n✝ + 1) a

Tactic:
simp_all

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

Goal state before:
pp: case succ.cons
α : Type u
a : α
n✝ : ℕ
a✝ : ∀ {l : List α}, n✝ ≠ l.length → (l.eraseIdx n✝).insertIdx n✝ a = l.set n✝ a
head✝ : α
tail✝ : List α
hn : n✝ + 1 ≠ (head✝ :: tail✝).length
⊢ ((head✝ :: tail✝).eraseIdx (n✝ + 1)).insertIdx (n✝ + 1) a = (head✝ :: tail✝).set (n✝ + 1) a

Tactic:
simp_all

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

Goal state before:
pp: case succ.nil
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
a : α
ha : p a
n : ℕ
ihn : ∀ {l : List α} (hl : ∀ (x : α), x ∈ l → p x), (pmap f l hl).insertIdx n (f a ha) = pmap f (l.insertIdx n a) ⋯
hl : ∀ (x : α), x ∈ [] → p x
⊢ (pmap f [] hl).insertIdx (n + 1) (f a ha) = pmap f ([].insertIdx (n + 1) a) ⋯

Tactic:
simp_all

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

Goal state before:
pp: case succ.cons
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
a : α
ha : p a
n : ℕ
ihn : ∀ {l : List α} (hl : ∀ (x : α), x ∈ l → p x), (pmap f l hl).insertIdx n (f a ha) = pmap f (l.insertIdx n a) ⋯
head✝ : α
tail✝ : List α
hl : ∀ (x : α), x ∈ head✝ :: tail✝ → p x
⊢ (pmap f (head✝ :: tail✝) hl).insertIdx (n + 1) (f a ha) = pmap f ((head✝ :: tail✝).insertIdx (n + 1) a) ⋯

Tactic:
simp_all

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
⊢ ((fun x1 x2 ↦ x1 = map f x2) ∘r fun x1 x2 ↦ x1 ~ x2) = fun x1 x2 ↦ x1 ~ map f x2

Tactic:
conv_rhs => rw [← Relation.comp_eq_fun (map f)]
  simp only [← forall₂_eq_eq_eq, forall₂_map_right_iff, forall₂_comp_perm_eq_perm_comp_forall₂]

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

Goal state before:
pp: 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

Tactic:
simp_all

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

Goal state before:
pp: 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

Tactic:
simp_all

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

Goal state before:
pp: 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

Tactic:
simp_all

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

Goal state before:
pp: 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

Tactic:
simp_all

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

Goal state before:
pp: α : Type u
inst✝ : Inhabited α
head✝¹ head✝ c : α
l : List α
⊢ (head✝¹ :: head✝ :: c :: l).getLastI = (head✝¹ :: head✝ :: c :: l).getLast?.getD default

Tactic:
simp [getLastI, getLastI_eq_getLast?_getD (c :: l)]

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

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
a b c D e f : M
h₁ : a = b
h₂ : b = c
h₃ : c = D * e
h₄ : e = f
⊢ b = D * f

Tactic:
h₂,

Goal state after:
M : Type u_1
inst✝ : Mul M
a b c D e f : M
h₁ : a = b
h₂ : b = c
h₃ : c = D * e
h₄ : e = f
⊢ c = D * f
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : CommGroupWithZero M
l : NF M
r : ℕ
hr : r ≠ 0
x : M
hx : x = l.eval
⊢ x ^ r = (l ^ r).eval

Tactic:
eval_pow,

Goal state after:
M : Type u_1
inst✝ : CommGroupWithZero M
l : NF M
r : ℕ
hr : r ≠ 0
x : M
hx : x = l.eval
⊢ x ^ r = zpow' l.eval ↑r
Module: Mathlib.Data.List.Basic

Goal state before:
pp: case mp.inl.inl
α : Type u
x₁ z₂ : List α
a₂ : α
notin_x : ¬a₂ ∈ x₁
notin_z : ¬a₂ ∈ z₂
⊢ x₁ = x₁ ++ [] ∧ a₂ = a₂ ∧ z₂ = z₂

Tactic:
simp_all

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

Goal state before:
pp: case mp.inl.inr
α : Type u
x₁ z₂ : List α
a₁ a₂ : α
notin_x : ¬a₂ ∈ x₁
d : List α
notin_z : ¬a₂ ∈ d ++ a₂ :: z₂
⊢ x₁ = x₁ ++ a₁ :: d ∧ a₁ = a₂ ∧ d ++ a₂ :: z₂ = z₂

Tactic:
simp_all

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

Goal state before:
pp: case mp.inr.inl
α : Type u
x₂ z₁ : List α
a₁ : α
notin_z : ¬a₁ ∈ z₁
notin_x : ¬a₁ ∈ x₂ ++ []
⊢ x₂ ++ [] = x₂ ∧ a₁ = a₁ ∧ z₁ = z₁

Tactic:
simp_all

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

Goal state before:
pp: case mp.inr.inr
α : Type u
x₂ z₁ : List α
a₁ a₂ : α
notin_z : ¬a₂ ∈ z₁
d : List α
notin_x : ¬a₂ ∈ x₂ ++ a₂ :: d
⊢ x₂ ++ a₂ :: d = x₂ ∧ a₁ = a₂ ∧ z₁ = d ++ a₁ :: z₁

Tactic:
simp_all

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

Goal state before:
pp: case e_den
d : ℕ
h : d ≠ 0
w : (Int.natAbs 0).Coprime d
⊢ d = 1

Tactic:
simp_all

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

Goal state before:
pp: q a b c : ℚ
x✝¹ : ℕ
x✝ : ℚ
⊢ ↑x✝¹.succ • x✝ = ↑x✝¹ • x✝ + x✝

Tactic:
HSMul.hSMul,

Goal state after:
q a b c : ℚ
x✝¹ : ℕ
x✝ : ℚ
⊢ SMul.smul (↑x✝¹.succ) x✝ = SMul.smul (↑x✝¹) x✝ + x✝
Module: Mathlib.Data.Rat.Defs

Goal state before:
pp: q a b c : ℚ
x✝¹ : ℕ
x✝ : ℚ
⊢ Int.negSucc x✝¹ • x✝ = -(↑x✝¹.succ • x✝)

Tactic:
HSMul.hSMul,

Goal state after:
q a b c : ℚ
x✝¹ : ℕ
x✝ : ℚ
⊢ SMul.smul (Int.negSucc x✝¹) x✝ = -SMul.smul (↑x✝¹.succ) x✝
Module: Mathlib.Algebra.Ring.Rat

Goal state before:
pp: q : ℚ
this : q.num /. ↑q.den * (↑q.den /. 1) = q.num /. 1
⊢ q * ↑q.den = ↑q.num

Tactic:
simp_all

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

Goal state before:
pp: n : ℕ
a : ℚ≥0
⊢ a ^ ↑n.succ = a ^ ↑n * a

Tactic:
by ext; apply Field.zpow_succ'

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : Nontrivial α
h : IsRelPrime 0 0
⊢ False

Tactic:
exact not_isRelPrime_zero_zero h

Goal state after:
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: case mp
qr : ℚ
⊢ IsSquare (qr * qr).num ∧ IsSquare (qr * qr).den

Tactic:
Rat.mul_self_num,

Goal state after:
case mp
qr : ℚ
⊢ IsSquare (qr.num * qr.num) ∧ IsSquare (qr * qr).den
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a b₁ b₂ c₁ c₂ d : R
x✝² : a * b₁ = c₁
x✝¹ : a * b₂ = c₂
x✝ : c₁ + 0 + c₂ = d
⊢ a * (b₁ + b₂) = d

Tactic:
by
  subst_vars; simp [_root_.mul_add]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
s : Set β
⊢ BddAbove (⇑e ⁻¹' s) ↔ BddAbove s

Tactic:
by
  rw [← e.bddAbove_image, e.image_preimage]

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:
simp_all

Goal state after:
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:
rw [← iSup_subtype'', sSup_image']

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
p : β → Type u_8
f : Sigma p → α
c : α
⊢ ⨆ x, f x ≤ c ↔ ⨆ i, ⨆ j, f ⟨i, j⟩ ≤ c

Tactic:
by simp only [iSup_le_iff, Sigma.forall]

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

Goal state before:
pp: ι : Type u_12
α : Type u_13
s : Set ι
hs : s.Nonempty
f : ι → Set α
t : Set α
⊢ ⋂ i ∈ s, t ∩ f i = t ∩ ⋂ i ∈ s, f i

Tactic:
rw [inter_comm, ← biInter_inter hs]

Goal state after:
ι : Type u_12
α : Type u_13
s : Set ι
hs : s.Nonempty
f : ι → Set α
t : Set α
⊢ ⋂ i ∈ s, t ∩ f i = ⋂ i ∈ s, f i ∩ t
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLattice α
minAx : MinimalAxioms α
f : (a : ι) → κ a → α
g : (a : ↑(range fun x ↦ range (f x))) → ↑↑a
⊢ ⨅ a, ↑(g a) ≤ ⨆ g, ⨅ i, f i (g i)

Tactic:
refine le_trans ?_ <| le_iSup _ fun a => Classical.choose (g ⟨_, a, rfl⟩).2
      refine le_iInf fun a => le_trans (iInf_le _ ⟨range (f a), a, rfl⟩) ?_
      rw [← Classical.choose_spec (g ⟨_, a, rfl⟩).2]

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
inst✝ : Frame α
ι : Type u_1
ι' : Type u_2
f : ι → α
g : ι' → α
s : Set ι
t : Set ι'
⊢ (⨆ i ∈ s, f i) ⊓ ⨆ j ∈ t, g j = ⨆ p ∈ s ×ˢ t, f p.1 ⊓ g p.2

Tactic:
by
  simp only [iSup_subtype', iSup_inf_iSup]
  exact (Equiv.surjective _).iSup_congr (Equiv.Set.prod s t).symm fun x => rfl

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
inst✝ : CompleteBooleanAlgebra α
s : Set α
hs : s.Nonempty
a : α
⊢ sSup s ∆ a ≤ sSup ((fun x ↦ x ∆ a) '' s)

Tactic:
sSup_image',

Goal state after:
α : Type u
inst✝ : CompleteBooleanAlgebra α
s : Set α
hs : s.Nonempty
a : α
⊢ sSup s ∆ a ≤ ⨆ a_1, ↑a_1 ∆ a
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompletelyDistribLattice β
⊢ CompletelyDistribLattice α

Tactic:
by
  let completeDistribLattice := e.completeDistribLattice
  apply e.injective.completelyDistribLattice <;> intros <;> first | rfl | exact e.apply_symm_apply _

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ Ι a b = Ioc a b ∪ Ioc b a

Tactic:
by
  cases le_total a b <;> simp [uIoc, *]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
he : (range ⇑e).OrdConnected
x y : α
⊢ ⇑e '' Ioo x y = Ioo (e x) (e y)

Tactic:
rw [← e.preimage_Ioo, image_preimage_eq_inter_range,
    inter_eq_left.2 <| Ioo_subset_Icc_self.trans <| he.out ⟨_, rfl⟩ ⟨_, rfl⟩]

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

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
⊢ ∀ (a b c : { x // 0 ≤ x }), a - b ≤ c ↔ a ≤ c + b

Tactic:
rintro ⟨a, ha⟩ ⟨b, hb⟩ ⟨c, hc⟩
    simp only [sub_le_iff_le_add, Subtype.mk_le_mk, mk_sub_mk, mk_add_mk, toNonneg_le]

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

Goal state before:
pp: case inl
m n : ℕ
hn : 1 < n
h : n ! = m !
hnm : n < m
⊢ n = m

Tactic:
← factorial_lt <| lt_of_succ_lt hn,

Goal state after:
case inl
m n : ℕ
hn : 1 < n
h : n ! = m !
hnm : n ! < m !
⊢ n = m
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: case inr.inr
m n : ℕ
hn : 1 < m
h : n ! = m !
hnm : m < n
⊢ n = m

Tactic:
← factorial_lt <| lt_of_succ_lt hn,

Goal state after:
case inr.inr
m n : ℕ
hn : 1 < m
h : n ! = m !
hnm : m ! < n !
⊢ n = m
Module: Mathlib.Data.Rat.Cast.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : DivisionRing α
p : ℚ
n : ℕ
⊢ ↑(p ^ n).num / ↑(p ^ n).den = (↑p.num / ↑p.den) ^ n

Tactic:
den_pow,

Goal state after:
α : Type u_1
inst✝ : DivisionRing α
p : ℚ
n : ℕ
⊢ ↑(p ^ n).num / ↑(p.den ^ n) = (↑p.num / ↑p.den) ^ n
Module: Mathlib.Data.Rat.Cast.Lemmas

Goal state before:
pp: K : Type u_1
inst✝ : DivisionSemiring K
q : ℚ≥0
n : ℕ
⊢ ↑(q ^ n).num / ↑(q ^ n).den = (↑q.num / ↑q.den) ^ n

Tactic:
den_pow,

Goal state after:
K : Type u_1
inst✝ : DivisionSemiring K
q : ℚ≥0
n : ℕ
⊢ ↑(q ^ n).num / ↑(q.den ^ n) = (↑q.num / ↑q.den) ^ n
Module: Mathlib.Data.PNat.Basic

Goal state before:
pp: a b : ℕ+
⊢ ↑(a - b) = if b < a then ↑a - ↑b else 1

Tactic:
change (toPNat' _ : ℕ) = ite _ _ _
  split_ifs with h
  · exact toPNat'_coe (tsub_pos_of_lt h)
  · rw [tsub_eq_zero_iff_le.mpr (le_of_not_gt h : (a : ℕ) ≤ b)]
    rfl

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

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : FloorRing R
z : ℤ
a : R
⊢ ⌊a⌋ = z ↔ ↑z ≤ a ∧ a < ↑z + 1

Tactic:
le_antisymm_iff,

Goal state after:
R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : FloorRing R
z : ℤ
a : R
⊢ ⌊a⌋ ≤ z ∧ z ≤ ⌊a⌋ ↔ ↑z ≤ a ∧ a < ↑z + 1
Module: Mathlib.Algebra.Order.Group.Basic

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

Tactic:
refine strictAnti_int_of_succ_lt fun n ↦ ?_

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a : α
ha : a < 1
n : ℤ
⊢ a ^ (n + 1) < a ^ n
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_4
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
n : ℤ
hn : 0 < n
a : R
⊢ ⌊↑n * a⌋ / n = ⌊a⌋

Tactic:
by
  rw [Commute.intCast_left, mul_cast_floor_div_cancel_of_pos hn]

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

Goal state before:
pp: case inl
α : Type u_1
inst✝⁴ : CommGroup α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : DenselyOrdered α
inst✝ : Nontrivial α
h : IsCyclic α
a : α
ha : Surjective fun x ↦ a ^ x
hlt : 1 < a⁻¹
k : ℤ
hab : a < (fun x ↦ a ^ x) k
hb : (fun x ↦ a ^ x) k < 1
⊢ a⁻¹ ^ 0 < a⁻¹ ^ k ∧ a⁻¹ ^ k < a⁻¹ ^ 1

Tactic:
simp_all

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

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝⁴ : CommGroup α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : DenselyOrdered α
inst✝ : Nontrivial α
h : IsCyclic α
a : α
ha : Surjective fun x ↦ a ^ x
hlt : 1 < a
k : ℤ
hb : 1 < (fun x ↦ a ^ x) k
hba : (fun x ↦ a ^ x) k < a
⊢ a ^ 0 < a ^ k ∧ a ^ k < a ^ 1

Tactic:
simp_all

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

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : FloorRing R
z : ℤ
a : R
⊢ ⌈a⌉ = z ↔ z ≤ ⌈a⌉ ∧ ⌈a⌉ ≤ z

Tactic:
le_antisymm_iff,

Goal state after:
R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : FloorRing R
z : ℤ
a : R
⊢ ⌈a⌉ ≤ z ∧ z ≤ ⌈a⌉ ↔ z ≤ ⌈a⌉ ∧ ⌈a⌉ ≤ z
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : ℚ
⊢ round ↑x = round x

Tactic:
by
  have : ((x + 1 / 2 : ℚ) : α) = x + 1 / 2 := by simp
  rw [round_eq, round_eq, ← this, floor_cast]

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

Goal state before:
pp: case inr
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
ha : fract a ≠ 0
⊢ fract a = a + 1 - ↑⌈a⌉

Tactic:
suffices (⌈a⌉ : R) = ⌊a⌋ + 1 by
    rw [this, ← self_sub_fract]
    abel

Goal state after:
case inr
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
ha : fract a ≠ 0
⊢ ↑⌈a⌉ = ↑⌊a⌋ + 1
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case inr
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
a b : k
hb : 1 < b
hba✝ : ↑⌈(b - 1)⁻¹⌉ / b ≤ a
hba : ↑⌈(b - 1)⁻¹⌉ / b < a
⊢ ↑⌈a⌉ ≤ b * a

Tactic:
exact (ceil_lt_mul hb hba).le

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

Goal state before:
pp: α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
⊢ count a l < l.length ↔ ∃ b, b ∈ l ∧ b ≠ a

Tactic:
simp [count]

Goal state after:
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: case pos
α : Type u_1
a : α
as bs : Multiset α
this : DecidableEq α
eq : a ::ₘ as = a ::ₘ bs
⊢ a = a ∧ as = bs ∨ a ≠ a ∧ ∃ cs, as = a ::ₘ cs ∧ bs = a ::ₘ cs

Tactic:
simp_all

Goal state after:
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: α : Type u_1
s t : Multiset α
⊢ s ≤ t + s

Tactic:
simpa using Multiset.add_le_add_right (zero_le t)

Goal state after:
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: case isTrue
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
a✝ : α
h✝ : a✝ = a
⊢ count a✝ s - 1 = count a✝ (s.erase a)

Tactic:
simp_all

Goal state after:
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: case isFalse
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
a✝ : α
h✝ : ¬a✝ = a
⊢ count a✝ s - 0 = count a✝ (s.erase a)

Tactic:
simp_all

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

Goal state before:
pp: case pos
α : Type u
a : α
l : List α
ih : l[0]? = l.getLast? → (l.reverse.tail.Nodup ↔ l.tail.Nodup)
h : (a :: l)[0]? = (a :: l).getLast?
hl : l = []
⊢ (a :: l).reverse.tail.Nodup ↔ (a :: l).tail.Nodup

Tactic:
simp_all

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Function.Injective f
x : α
xs : List α
ih : (map f xs).dedup = map f xs.dedup
h : x ∈ xs
⊢ (f x :: map f xs).dedup = map f (x :: xs).dedup

Tactic:
dedup_cons_of_mem h,

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Function.Injective f
x : α
xs : List α
ih : (map f xs).dedup = map f xs.dedup
h : x ∈ xs
⊢ (f x :: map f xs).dedup = map f xs.dedup
Module: Mathlib.Data.List.Lattice

Goal state before:
pp: case pos
α : Type u_1
l₂ : List α
a : α
inst✝ : DecidableEq α
l₁ : List α
h✝ : a ∈ l₂
⊢ (a :: l₁) ∩ l₂ = a :: l₁ ∩ l₂

Tactic:
simp_all

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

Goal state before:
pp: case neg
α : Type u_1
l₂ : List α
a : α
inst✝ : DecidableEq α
l₁ : List α
h✝ : ¬a ∈ l₂
⊢ (a :: l₁) ∩ l₂ = l₁ ∩ l₂

Tactic:
simp_all

Goal state after: