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

Goal state before:
pp: α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : α
ha : 0 ≤ a
hc : 0 ≤ c
h : ∀ a' ≥ 0, a' < a → ∀ b' ≥ 0, b' < b → a' * b' ≤ c
d : α
d_ab : d < a * b
⊢ d ≤ c

Tactic:
rcases lt_or_ge d 0 with hd | hd

Goal state after:
case inl
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : α
ha : 0 ≤ a
hc : 0 ≤ c
h : ∀ a' ≥ 0, a' < a → ∀ b' ≥ 0, b' < b → a' * b' ≤ c
d : α
d_ab : d < a * b
hd : d < 0
⊢ d ≤ c

case inr
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : α
ha : 0 ≤ a
hc : 0 ≤ c
h : ∀ a' ≥ 0, a' < a → ∀ b' ≥ 0, b' < b → a' * b' ≤ c
d : α
d_ab : d < a * b
hd : 0 ≤ d
⊢ d ≤ c
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
pos : 0 < 1 + ↑n * (B + 1) ^ (n - 1)
⊢ ∃ δ > 0, ∀ (q r : α), |r| ≤ B → |q - r| ≤ δ → |q ^ n - r ^ n| < ε

Tactic:
refine ⟨min 1 (ε / (1 + n * (B + 1) ^ (n - 1))), lt_min zero_lt_one (div_pos hε pos),
    fun q r hr hqr ↦ (abs_pow_sub_pow_le ..).trans_lt ?_⟩

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)
q r : α
hr : |r| ≤ B
hqr : |q - r| ≤ min 1 (ε / (1 + ↑n * (B + 1) ^ (n - 1)))
⊢ |q - r| * ↑n * max |q| |r| ^ (n - 1) < ε
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: case nil
M : Type u_4
inst✝ : Monoid M
h : [].prod ≠ 1
⊢ 0 < [].length

Tactic:
simp at h

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

Goal state before:
pp: α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
hl : l ≠ []
hl' : ¬l.getLast hl ∈ l.dropLast
⊢ l.length - 1 ≤ idxOf (l.getLast hl) l

Tactic:
contrapose hl'
    rwa [mem_dropLast_iff_idxOf_lt <| getLast_mem hl, ← Nat.not_le]

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

Goal state before:
pp: α : Type u
β : Type v
b₁ b₂ : β
l : List α
h : b₁ ∈ map (const α b₂) l
⊢ b₁ = b₂

Tactic:
by rw [map_const] at h; exact eq_of_mem_replicate h

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

Goal state before:
pp: case mp
α : Type u
x₁ x₂ z₁ z₂ : List α
a₁ a₂ : α
notin_x : ¬a₂ ∈ x₁
notin_z : ¬a₂ ∈ z₁
⊢ ((∃ as, x₂ = x₁ ++ as ∧ (as = [] ∧ a₂ = a₁ ∧ z₂ = z₁ ∨ ∃ as', as = a₁ :: as' ∧ z₁ = as' ++ a₂ :: z₂)) ∨
      ∃ bs, x₁ = x₂ ++ bs ∧ (bs = [] ∧ a₁ = a₂ ∧ z₁ = z₂ ∨ ∃ as', bs = a₂ :: as' ∧ z₂ = as' ++ a₁ :: z₁)) →
    x₁ = x₂ ∧ a₁ = a₂ ∧ z₁ = z₂

Tactic:
rintro (⟨c, rfl, ⟨rfl, rfl, rfl⟩ | ⟨d, rfl, rfl⟩⟩ |
      ⟨c, rfl, ⟨rfl, rfl, rfl⟩ | ⟨d, rfl, rfl⟩⟩)

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

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₂

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

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₁
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : BEq α
inst✝² : LawfulBEq α
inst✝¹ : BEq β
inst✝ : LawfulBEq β
f : α → β
finj : Injective f
a : α
l : List α
b : α
⊢ (a == b) = (f a == f b)

Tactic:
simp [finj.eq_iff]

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

Goal state before:
pp: a : ℚ≥0
⊢ a ^ 0 = 1

Tactic:
ext; apply Field.zpow_zero'

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

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
x : α
n : ℕ
⊢ x ∣ x ^ n ↔ n ≠ 0 ∨ IsUnit x

Tactic:
rcases eq_or_ne n 0 with rfl | hn

Goal state after:
case inl
α : Type u_1
inst✝ : CommMonoid α
x : α
⊢ x ∣ x ^ 0 ↔ 0 ≠ 0 ∨ IsUnit x

case inr
α : Type u_1
inst✝ : CommMonoid α
x : α
n : ℕ
hn : n ≠ 0
⊢ x ∣ x ^ n ↔ n ≠ 0 ∨ IsUnit x
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: q₁ q₂ : ℚ
⊢ q₁.num * q₂.num = (q₁ * q₂).num * ↑((q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den))

Tactic:
rw [mul_num]
  refine (Int.ediv_mul_cancel ?_).symm
  rw [← Int.dvd_natAbs]
  exact Int.ofNat_dvd.mpr (Nat.gcd_dvd_left _ _)

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

Goal state before:
pp: n : ℕ
⊢ IsSquare ↑n ∧ True ↔ IsSquare n

Tactic:
and_true,

Goal state after:
n : ℕ
⊢ IsSquare ↑n ↔ IsSquare n
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: n₁ n₂ : ℤ
d : ℕ
h : d ≠ 0
⊢ mkRat n₁ d + mkRat n₂ d = mkRat (n₁ + n₂) d

Tactic:
rw [mkRat_add_mkRat _ _ h h, ← add_mul, mkRat_mul_right h]

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

Goal state before:
pp: case mp
m n : ℤ
hn : ↑n ≠ 0
⊢ ↑(↑m / ↑n).num * ↑n = ↑m → n ∣ m

Tactic:
exact mod_cast (Dvd.intro_left _)

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

Goal state before:
pp: case node
α : Type u
v : α
l r : BinaryTree α
hl : map id l = l
hr : map id r = r
⊢ map id (node v l r) = node v l r

Tactic:
| node v l r hl hr =>

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

Goal state before:
pp: case node
α : Type u
β : Type u_1
γ : Type u_2
f : α → β
g : β → γ
v : α
l r : BinaryTree α
hl : map (g ∘ f) l = map g (map f l)
hr : map (g ∘ f) r = map g (map f r)
⊢ map (g ∘ f) (node v l r) = map g (map f (node v l r))

Tactic:
| node v l r hl hr =>

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

Goal state before:
pp: case node
α : Type u
m : Type u → Type u_1
inst✝¹ : Applicative m
inst✝ : LawfulApplicative m
v : α
l r : BinaryTree α
hl : traverse pure l = pure l
hr : traverse pure r = pure r
⊢ traverse pure (node v l r) = pure (node v l r)

Tactic:
| node v l r hl hr =>

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

Goal state before:
pp: α : Type u_1
inst✝ : CommRing α
n1 n2 k e1 e2 t1 t2 : α
h1 : n1 * e1 = t1
h2 : n2 * e2 = t2
h3 : n1 * n2 = k
⊢ n2 * (t1 * e2) = t1 * t2

Tactic:
← mul_assoc n2,

Goal state after:
α : Type u_1
inst✝ : CommRing α
n1 n2 k e1 e2 t1 t2 : α
h1 : n1 * e1 = t1
h2 : n2 * e2 = t2
h3 : n1 * n2 = k
⊢ n2 * t1 * e2 = t1 * t2
Module: Mathlib.Order.GaloisConnection.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
l : α → β
u : β → α
gc : GaloisConnection l u
a : β
b : α
⊢ (compl ∘ u ∘ compl) a ≤ b ↔ a ≤ (compl ∘ l ∘ compl) b

Tactic:
by
  dsimp
  rw [le_compl_iff_le_compl, gc, compl_le_iff_compl_le]

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

Goal state before:
pp: case a
α : Type u_1
inst✝² : CompleteLattice α
ι : Type u_8
inst✝¹ : LT ι
inst✝ : NoMaxOrder ι
f : ι → α
⊢ ⨆ i, f i ≤ ⨆ i, ⨆ j, ⨆ (_ : j < i), f j

Tactic:
· refine iSup_le fun j ↦ ?_
    obtain ⟨i, jlt⟩ := exists_gt j
    exact le_iSup_of_le i (le_iSup₂_of_le j jlt le_rfl)

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

Goal state before:
pp: ι : Type u_12
σ : ι → Type u_13
s : Set (Sigma σ)
⊢ ⋃ i, Sigma.mk i '' Sigma.mk i ⁻¹' s = s

Tactic:
ext x

Goal state after:
ι : Type u_12
σ : ι → Type u_13
s : Set (Sigma σ)
x : (i : ι) × σ i
⊢ x ∈ ⋃ i, Sigma.mk i '' Sigma.mk i ⁻¹' s ↔ x ∈ s
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
⊢ ⋃ x, {f x} = range f

Tactic:
ext x

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
x : β
⊢ x ∈ ⋃ x, {f x} ↔ x ∈ range f
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_12
β : Type u_13
C : Set (Set α)
f : (s : ↑C) → β → ↑↑s
hf : ∀ (s : ↑C), Surjective (f s)
⊢ (⋃ y, range fun s ↦ ↑(f s y)) = ⋃₀ C

Tactic:
ext x

Goal state after:
α : Type u_12
β : Type u_13
C : Set (Set α)
f : (s : ↑C) → β → ↑↑s
hf : ∀ (s : ↑C), Surjective (f s)
x : α
⊢ (x ∈ ⋃ y, range fun s ↦ ↑(f s y)) ↔ x ∈ ⋃₀ C
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
C : ι → Set α
f : (x : ι) → β → ↑(C x)
hf : ∀ (x : ι), Surjective (f x)
⊢ (⋃ y, range fun x ↦ ↑(f x y)) = ⋃ x, C x

Tactic:
ext x

Goal state after:
α : Type u_1
β : Type u_2
ι : Sort u_5
C : ι → Set α
f : (x : ι) → β → ↑(C x)
hf : ∀ (x : ι), Surjective (f x)
x : α
⊢ (x ∈ ⋃ y, range fun x ↦ ↑(f x y)) ↔ x ∈ ⋃ x, C x
Module: Mathlib.Order.CompleteLattice.Basic

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
β : α → Type u_9
inst✝ : (i : α) → CompleteLattice (β i)
x✝¹ : Set ((i : α) → β i)
x✝ : α
⊢ IsGLB (eval x✝ '' x✝¹) (sInf x✝¹ x✝)

Tactic:
rw [sInf_apply_eq_sInf_image]; exact isGLB_sInf _

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

Goal state before:
pp: α : Type u_1
ι : Type u_12
Es : ι → Set α
Es_union : ⋃ i, Es i = univ
Es_disj : Pairwise fun i j ↦ Disjoint (Es i) (Es j)
I : Set ι
⊢ (⋃ i ∈ I, Es i)ᶜ = ⋃ i ∈ Iᶜ, Es i

Tactic:
ext x

Goal state after:
α : Type u_1
ι : Type u_12
Es : ι → Set α
Es_union : ⋃ i, Es i = univ
Es_disj : Pairwise fun i j ↦ Disjoint (Es i) (Es j)
I : Set ι
x : α
⊢ x ∈ (⋃ i ∈ I, Es i)ᶜ ↔ x ∈ ⋃ i ∈ Iᶜ, Es i
Module: Mathlib.Order.CompleteLattice.Basic

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
inst✝⁸ : Max α
inst✝⁷ : Min α
inst✝⁶ : LE α
inst✝⁵ : LT α
inst✝⁴ : SupSet α
inst✝³ : InfSet α
inst✝² : Top α
inst✝¹ : Bot α
inst✝ : CompleteLattice β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a
map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
x✝ : Set α
⊢ IsGLB ((fun {x} ↦ f x) '' x✝) (f (sInf x✝))

Tactic:
rw [map_sInf]; exact isGLB_biInf

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

Goal state before:
pp: α : Type u_1
ι : Sort u_5
inst✝ : Preorder α
f : ι → α
c : α
⊢ c ∈ ⋂ i, Iic (f i) ↔ c ∈ lowerBounds (range f)

Tactic:
simp [lowerBounds]

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
ι : Sort w
inst✝ : Frame α
f : ι → α
a : α
⊢ sSup (range fun i ↦ f i) ⊓ a = ⨆ i, f i ⊓ a

Tactic:
sSup_inf_eq,

Goal state after:
α : Type u
ι : Sort w
inst✝ : Frame α
f : ι → α
a : α
⊢ ⨆ a_1 ∈ range fun i ↦ f i, a_1 ⊓ a = ⨆ i, f i ⊓ a
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
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 t_ne (fun y hy ↦ ?_)

Goal state after:
α : 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
y : α
hy : y ∈ t
⊢ y ≤ sSup s
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case neg.some.none
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ s
hb : none ∈ lowerBounds s
⊢ s ⊆ {⊤}

Tactic:
intro c hc

Goal state after:
case neg.some.none
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ s
hb : none ∈ lowerBounds s
c : WithTop β
hc : c ∈ s
⊢ c ∈ {⊤}
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case h
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ s
b : β
hb : Option.some b ∈ lowerBounds s
⊢ b ∈ lowerBounds ((fun a ↦ ↑a) ⁻¹' s)

Tactic:
intro c hc

Goal state after:
case h
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ s
b : β
hb : Option.some b ∈ lowerBounds s
c : β
hc : c ∈ (fun a ↦ ↑a) ⁻¹' s
⊢ b ≤ c
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝ : Lattice α
a : α
⊢ [[a, a]] = {a}

Tactic:
simp [uIcc]

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

Goal state before:
pp: case mp.inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
hf : Monotone f
a b c : α
⊢ c ∈ Icc (min a b) (max a b) → f c ∈ Icc (min (f a) (f b)) (max (f a) (f b))

Tactic:
← hf.map_min,

Goal state after:
case mp.inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
hf : Monotone f
a b c : α
⊢ c ∈ Icc (min a b) (max a b) → f c ∈ Icc (f (min a b)) (max (f a) (f b))
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: case mp.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
hf : Antitone f
a b c : α
⊢ c ∈ Icc (min a b) (max a b) → f c ∈ Icc (min (f a) (f b)) (max (f a) (f b))

Tactic:
← hf.map_min,

Goal state after:
case mp.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
hf : Antitone f
a b c : α
⊢ c ∈ Icc (min a b) (max a b) → f c ∈ Icc (min (f a) (f b)) (f (min a b))
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: case inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h : b ∈ [[a, c]]
this : ∀ {a c : α}, b ∈ [[a, c]] → a ≤ c → Ι a b ∪ Ι b c = Ι a c
hac : ¬a ≤ c
⊢ Ι a b ∪ Ι b c = Ι a c

Tactic:
uIoc_comm,

Goal state after:
case inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h : b ∈ [[a, c]]
this : ∀ {a c : α}, b ∈ [[a, c]] → a ≤ c → Ι a b ∪ Ι b c = Ι a c
hac : ¬a ≤ c
⊢ Ι b a ∪ Ι b c = Ι a c
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: case inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h : b ∈ [[a, c]]
this : ∀ {a c : α}, b ∈ [[a, c]] → a ≤ c → Ι a b ∪ Ι b c = Ι a c
hac : ¬a ≤ c
⊢ Ι b c ∪ Ι b a = Ι a c

Tactic:
uIoc_comm,

Goal state after:
case inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h : b ∈ [[a, c]]
this : ∀ {a c : α}, b ∈ [[a, c]] → a ≤ c → Ι a b ∪ Ι b c = Ι a c
hac : ¬a ≤ c
⊢ Ι c b ∪ Ι b a = Ι a c
Module: Mathlib.Order.Interval.Set.OrdConnected

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : β → α
t : Set β
s : Set α
hs : s.OrdConnected
hf : MonotoneOn f t
u : Set β := {x | (∃ y ∈ t, y ≤ x ∧ f y ∈ s) ∧ ∃ z ∈ t, x ≤ z ∧ f z ∈ s}
⊢ ∀ ⦃x : β⦄, x ∈ u → ∀ ⦃y : β⦄, y ∈ u → Icc x y ⊆ u

Tactic:
rintro x ⟨⟨y, yt, yx, ys⟩, -⟩ x' ⟨-, ⟨z, zt, x'z, zs⟩⟩ a ha

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : β → α
t : Set β
s : Set α
hs : s.OrdConnected
hf : MonotoneOn f t
u : Set β := {x | (∃ y ∈ t, y ≤ x ∧ f y ∈ s) ∧ ∃ z ∈ t, x ≤ z ∧ f z ∈ s}
x y : β
yt : y ∈ t
yx : y ≤ x
ys : f y ∈ s
x' z : β
zt : z ∈ t
x'z : x' ≤ z
zs : f z ∈ s
a : β
ha : a ∈ Icc x x'
⊢ a ∈ u
Module: Mathlib.Algebra.Order.Monoid.Basic

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

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

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

Goal state before:
pp: α : Type u_1
inst✝³ : Semiring α
inst✝² : PartialOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : ExistsAddOfLE α
a b : { x // 0 ≤ x }
h : a ≤ b
⊢ ∃ c, b = a + c

Tactic:
rw [← Subtype.coe_le_coe] at h
    obtain ⟨c, hc⟩ := exists_add_of_le h
    refine ⟨⟨c, ?_⟩, by simp [Subtype.ext_iff, hc]⟩
    rw [← add_zero a.val, hc] at h
    exact le_of_add_le_add_left h

Goal state after:
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : One M
c : M
hc : c ≠ 1
⊢ (mulSupport fun x ↦ c) = univ

Tactic:
ext x

Goal state after:
ι : Type u_1
M : Type u_3
inst✝ : One M
c : M
hc : c ≠ 1
x : ι
⊢ (x ∈ mulSupport fun x ↦ c) ↔ x ∈ univ
Module: Mathlib.Data.Rat.Cast.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : DivisionRing α
n : ℤ
⊢ ↑(↑n)⁻¹ = (↑n)⁻¹

Tactic:
by
  rcases n with n | n
  · simp [cast_inv_nat]
  · simp only [Int.cast_negSucc, cast_neg, inv_neg, cast_inv_nat]

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

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
⊢ |x - ↑(round x)| ≤ 1 / 2

Tactic:
rw [round_eq, abs_sub_le_iff]
  have := floor_le (x + 1 / 2)
  have := lt_floor_add_one (x + 1 / 2)
  constructor <;> linarith

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

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b : R
Hcomm : Commute a b
ha : 0 ≤ a
Hsq : 0 ≤ b ^ 2
Hsq' : 0 ≤ (a + b) ^ 2
H : 0 ≤ 2 * a + b
n : ℕ
⊢ (a + b) ^ 2 * (a + b) ^ (n + 1) = (a + b) ^ (n + 3)

Tactic:
by simp [pow_succ', mul_assoc]

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

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : R
H : -1 ≤ a
n : ℕ
⊢ -1 + -1 ≤ a - 1

Tactic:
← sub_eq_add_neg,

Goal state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : R
H : -1 ≤ a
n : ℕ
⊢ -1 - 1 ≤ a - 1
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
s : Set R
⊢ fract ⁻¹' s = ⋃ m, (fun x ↦ x - ↑m) ⁻¹' (s ∩ Ico 0 1)

Tactic:
ext x

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
s : Set R
x : R
⊢ x ∈ fract ⁻¹' s ↔ x ∈ ⋃ m, (fun x ↦ x - ↑m) ⁻¹' (s ∩ Ico 0 1)
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
s : Set R
⊢ fract '' s = ⋃ m, (fun x ↦ x - ↑m) '' s ∩ Ico 0 1

Tactic:
ext x

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
s : Set R
x : R
⊢ x ∈ fract '' s ↔ x ∈ ⋃ m, (fun x ↦ x - ↑m) '' s ∩ Ico 0 1
Module: Mathlib.Algebra.Group.Action.Basic

Goal state before:
pp: G✝ : Type u_1
M : Type u_2
A✝ : Type u_3
B✝ : Type u_4
α : Type u_5
β : Type u_6
G : Type u_7
A : Type u_8
B : Type u_9
inst✝¹ : DivisionMonoid G
inst✝ : MulAction G A
x y : G
f : A → B
⊢ (x * y) • f = x • y • f

Tactic:
change (fun a => f ((x * y)⁻¹ • a)) = (fun a => f (y⁻¹ • x⁻¹ • a))
    simp only [mul_smul, mul_inv_rev]

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

Goal state before:
pp: R : Type u_1
G : Type u_2
inst✝⁴ : Ring R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : FloorRing R
inst✝ : AddGroup G
a : G
x✝ : ↑(Ico 0 1) → G
⊢ (fun f x ↦ f ↑x) ((fun f ↦ { toFun := fun x ↦ f ⟨Int.fract x, ⋯⟩ + ⌊x⌋ • a, map_add_const' := ⋯ }) x✝) = x✝

Tactic:
ext x

Goal state after:
R : Type u_1
G : Type u_2
inst✝⁴ : Ring R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : FloorRing R
inst✝ : AddGroup G
a : G
x✝ : ↑(Ico 0 1) → G
x : ↑(Ico 0 1)
⊢ (fun f x ↦ f ↑x) ((fun f ↦ { toFun := fun x ↦ f ⟨Int.fract x, ⋯⟩ + ⌊x⌋ • a, map_add_const' := ⋯ }) x✝) x = x✝ x
Module: Mathlib.Algebra.AddConstMap.Basic

Goal state before:
pp: R : Type u_1
G : Type u_2
inst✝⁴ : Ring R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : FloorRing R
inst✝ : AddGroup G
a : G
f : R →+c[1, a] G
⊢ (fun f ↦ { toFun := fun x ↦ f ⟨Int.fract x, ⋯⟩ + ⌊x⌋ • a, map_add_const' := ⋯ }) ((fun f x ↦ f ↑x) f) = f

Tactic:
ext x

Goal state after:
R : Type u_1
G : Type u_2
inst✝⁴ : Ring R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : FloorRing R
inst✝ : AddGroup G
a : G
f : R →+c[1, a] G
x : R
⊢ ((fun f ↦ { toFun := fun x ↦ f ⟨Int.fract x, ⋯⟩ + ⌊x⌋ • a, map_add_const' := ⋯ }) ((fun f x ↦ f ↑x) f)) x = f x
Module: Mathlib.Algebra.Torsor.Basic

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝¹ : CommGroup G
inst✝ : Torsor G P
v : G
p₁ p₂ : P
⊢ v • p₁ /ₛ v • p₂ = p₁ /ₛ p₂

Tactic:
by
  rw [sdiv_smul_eq_sdiv_div, smul_sdiv_assoc, mul_div_cancel_left]

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

Goal state before:
pp: α : Type u_1
l : List α
⊢ range l.get = {x | x ∈ l}

Tactic:
ext x

Goal state after:
α : Type u_1
l : List α
x : α
⊢ x ∈ range l.get ↔ x ∈ {x | x ∈ l}
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
s t u : Multiset α
r1 : Rel r s t
r2 : Rel r t u
⊢ Rel r s u

Tactic:
induction t using Multiset.induction_on generalizing s u with
  | empty => rw [rel_zero_right.mp r1, rel_zero_left.mp r2, rel_zero_left]
  | cons x t ih =>
    obtain ⟨a, as, ha1, ha2, rfl⟩ := rel_cons_right.mp r1
    obtain ⟨b, bs, hb1, hb2, rfl⟩ := rel_cons_left.mp r2
    exact Multiset.Rel.cons (_root_.trans ha1 hb1) (ih ha2 hb2)

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

Goal state before:
pp: α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
hl : l.Nodup
i : ℕ
h : i < l.length
⊢ l.erase l[i] = l.eraseIdx i

Tactic:
by
  induction l generalizing i with
  | nil => simp
  | cons a l IH =>
    cases i with
    | zero => simp
    | succ i => grind

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

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
r : α → β → Prop
s : Multiset α
t : Multiset γ
f : γ → β
⊢ Rel r s (map f t) ↔ Rel (fun a b ↦ r a (f b)) s t

Tactic:
rw [← rel_flip, rel_map_left, ← rel_flip]; rfl

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
⊢ (a :: l).dedup = if a ∈ l.dedup then l.dedup else a :: l.dedup

Tactic:
split <;> simp [dedup_cons_of_mem', dedup_cons_of_notMem', *]

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

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
p : α → Prop
inst✝ : DecidablePred p
l : Multiset α
a b : List α
p✝ : a ≈ b
x : α
px : x ∈ b ∧ p x
y : α
py : y ∈ b ∧ p y
z : α
z_unique : ∀ (y : α), (fun a ↦ a ∈ ⟦b⟧ ∧ p a) y → y = z
_z_mem_l : z ∈ ⟦b⟧
_pz : p z
⊢ x = y

Tactic:
calc
        x = z := z_unique x px
        _ = y := (z_unique y py).symm

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ {s u : Multiset α}, s ≤ t → s ≤ u → s ≤ t ∩ u
s u : Multiset α
h₁ : s ≤ a ::ₘ t
h₂ : s ≤ u
h : ¬a ∈ u
⊢ s ≤ (a ::ₘ t) ∩ u

Tactic:
cons_inter_of_neg _ h

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ {s u : Multiset α}, s ≤ t → s ≤ u → s ≤ t ∩ u
s u : Multiset α
h₁ : s ≤ a ::ₘ t
h₂ : s ≤ u
h : ¬a ∈ u
⊢ s ≤ t ∩ u
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
⊢ N ∩ Q + (P - M) = N

Tactic:
ext x

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
⊢ count x (N ∩ Q + (P - M)) = count x N
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
h : p a
⊢ filter p (s.erase a) - filter p t = filter p s - filter p (a ::ₘ t)

Tactic:
rw [filter_cons_of_pos _ h, sub_cons]

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
h : p a
⊢ filter p (s.erase a) - filter p t = (filter p s).erase a - filter p t
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
l₁ l₂ : List (List α)
h : l₁ <:+: l₂
⊢ l₁.flatten <:+: l₂.flatten

Tactic:
by
  rcases h with ⟨l, l', rfl⟩
  simp

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

Goal state before:
pp: case mp.nil
α : Type u_1
xs : List α
x head✝¹ head✝ : α
tail✝ w✝ : List α
h : [] ++ head✝¹ :: head✝ :: tail✝ ++ w✝ = [x]
⊢ head✝¹ :: head✝ :: tail✝ = [] ∨ head✝¹ :: head✝ :: tail✝ = [x]

Tactic:
simp at h

Goal state after: