mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Logic.Equiv.Set

Goal state before:
pp: α : Type u_3
s t : Set α
h : s ⊆ t
inst✝ : DecidablePred fun x ↦ x ∈ s
x : ↑t
hx : ¬↑x ∈ s
⊢ (Set.sumDiffSubset h).symm x = Sum.inr ⟨↑x, ⋯⟩

Tactic:
by
  apply (Equiv.Set.sumDiffSubset h).injective
  simp only [apply_symm_apply, sumDiffSubset_apply_inr]

Goal state after:
Module: Mathlib.Logic.Equiv.Set

Goal state before:
pp: α✝¹ : Sort u
β✝¹ : Sort v
γ : Sort w
α✝ : Type u_1
β✝ : Type u_2
α : Type u
β : Type v
s : Set α
t : Set β
inst✝¹ : DecidablePred fun x ↦ x ∈ s
inst✝ : DecidablePred fun x ↦ x ∈ t
e₀ : ↑s ≃ ↑t
e₁ : ↑sᶜ ≃ ↑tᶜ
x : ↑s
⊢ (Trans.trans (Trans.trans (Set.sumCompl s).symm (e₀.sumCongr e₁)) (Set.sumCompl t)) ↑x = ↑(e₀ x)

Tactic:
simp only [Sum.map_inl, trans_apply, sumCongr_apply, Set.sumCompl_apply_inl,
        Set.sumCompl_symm_apply, Trans.trans]

Goal state after:
Module: Mathlib.Order.WellFounded

Goal state before:
pp: β : Type u_2
inst✝² : LinearOrder β
f : β → β
inst✝¹ : WellFoundedLT β
inst✝ : NoMaxOrder β
hf : StrictMono f
a : β
ha : a ∈ upperBounds (Set.range f)
⊢ False

Tactic:
obtain ⟨b, hb⟩ := exists_gt a

Goal state after:
β : Type u_2
inst✝² : LinearOrder β
f : β → β
inst✝¹ : WellFoundedLT β
inst✝ : NoMaxOrder β
hf : StrictMono f
a : β
ha : a ∈ upperBounds (Set.range f)
b : β
hb : a < b
⊢ False
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a : α
⊢ ∀ (x : α), x ∈ Icc a a ↔ x ∈ {a}

Tactic:
by simp [Icc, le_antisymm_iff, and_comm]

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

Goal state before:
pp: case inl
α : Type u_1
inst✝ : Preorder α
s t : Set α
h : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (s ∪ t)
x : α
hx : x ∈ s
y : α
hy : y ∈ t
hys : ∀ x ∈ s, ¬y ≤ x
z : α
hzs : z ∈ s
hxz : x ≤ z
hyz : y ≤ z
⊢ ∃ b ∈ t, x ≤ b

Tactic:
cases hys z hzs hyz

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
s t : Set α
⊢ BddAbove s → BddAbove t → BddAbove (s ∪ t)

Tactic:
by
  rintro ⟨a, ha⟩ ⟨b, hb⟩
  obtain ⟨c, hca, hcb⟩ := exists_ge_ge a b
  rw [BddAbove, upperBounds_union]
  exact ⟨c, upperBounds_mono_mem hca ha, upperBounds_mono_mem hcb hb⟩

Goal state after:
Module: Mathlib.Tactic.Abel

Goal state before:
pp: α : Type u_1
inst✝ : AddCommGroup α
l : ℕ
r : α
tl : ℕ
zl : ℤ
tr t : α
prl₁ : l = tl
prl₂ : ↑tl = zl
prr : r = tr
prt : smulg zl tr = t
⊢ smul l r = t

Tactic:
by
  simp [← prt, prl₁, ← prl₂, prr, smul, smulg, natCast_zsmul]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
a✝ : α
b✝ : β
l₁✝ : List α
l₂✝ : List β
h₁ : R a✝ b✝
h₂ : Forall₂ R l₁✝ l₂✝
x : α
y : β
hx : (x, y) ∈ (a✝ :: l₁✝).zip (b✝ :: l₂✝)
⊢ R x y

Tactic:
rw [zip, zipWith, mem_cons] at hx

Goal state after:
α : Type u_1
β : Type u_2
R : α → β → Prop
a✝ : α
b✝ : β
l₁✝ : List α
l₂✝ : List β
h₁ : R a✝ b✝
h₂ : Forall₂ R l₁✝ l₂✝
x : α
y : β
hx : (x, y) = (a✝, b✝) ∨ (x, y) ∈ zipWith Prod.mk l₁✝ l₂✝
⊢ R x y
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: case mpr.cons_cons
α : Type u_1
β : Type u_2
R : α → β → Prop
l₂ l l₁✝ l₂✝ : List β
a✝¹ : β
a✝ : l₁✝ <+ l₂✝
ih : ∀ {l₁ : List α}, Forall₂ R l₁ l₁✝ → SublistForall₂ R l₁ l₂✝
⊢ ∀ {l₁ : List α}, Forall₂ R l₁ (a✝¹ :: l₁✝) → SublistForall₂ R l₁ (a✝¹ :: l₂✝)

Tactic:
intro l₁ hl1
      obtain - | ⟨hr, hl⟩ := hl1
      exact SublistForall₂.cons hr (ih hl)

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 ∈ l₂

Tactic:
rcases mem_map.1 (h2 (mem_map_of_mem hx)) with ⟨x', hx', hxx'⟩

Goal state after:
α : 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₂
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : GroupWithZero M
l₁ l₂ l : NF M
x₁ x₂ : M
hx₁ : x₁ = l₁.eval
hx₂ : x₂ = l₂.eval
h : l₁.eval * l₂.eval = l.eval
⊢ x₁ * x₂ = l.eval

Tactic:
by
  rw [hx₁, hx₂, h]

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

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

Tactic:
induction i generalizing l

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

case succ
M : Type u_4
inst✝ : Monoid M
a : M
n✝ : ℕ
a✝ : ∀ {l : List M}, n✝ ≤ l.length → (∀ (a' : M), a' ∈ take n✝ l → Commute a a') → (l.insertIdx n✝ a).prod = a * l.prod
l : List M
hlen : n✝ + 1 ≤ l.length
hcomm : ∀ (a' : M), a' ∈ take (n✝ + 1) l → Commute a a'
⊢ (l.insertIdx (n✝ + 1) a).prod = a * l.prod
Module: Mathlib.Data.List.Basic

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

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

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

Goal state before:
pp: M : Type u_1
inst✝ : GroupWithZero M
l₁ l₂ l : NF M
x₁ x₂ : M
hx₁ : x₁ = l₁.eval
hx₂ : x₂ = l₂.eval
h : l₁.eval / l₂.eval = l.eval
⊢ x₁ / x₂ = l.eval

Tactic:
by
  rw [hx₁, hx₂, h]

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

Goal state before:
pp: case inl
α : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq α
f : α → M
a : α
l : List α
h : a ∈ a :: l
⊢ f a * (map f ((a :: l).erase a)).prod = (map f (a :: l)).prod

Tactic:
simp only [map, erase_cons_head, prod_cons]

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

Goal state before:
pp: α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
x y : α
hx : x ∈ l
⊢ idxOf x l = idxOf y l ↔ x = y

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ h ▸ rfl⟩
  rw [← getElem_idxOf (idxOf_lt_length_iff.mpr hx)]
  simp [h]

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

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

Tactic:
by
  simp [hr, zpow'_zero_of_ne_zero hx]

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, ⋯⟩ = ↑(NNRat.divNat m (10 ^ d))

pp: case neg
K : Type u_1
inst✝ : NNRatCast K
m : ℕ
b : Bool
d : ℕ
h✝ : ¬b = true
⊢ ↑⟨OfScientific.ofScientific m b d, ⋯⟩ = ↑↑(m * 10 ^ d)

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

Goal state after:
case neg
K : Type u_1
inst✝ : NNRatCast K
m : ℕ
b : Bool
d : ℕ
h✝ : ¬b = true
⊢ ↑⟨OfScientific.ofScientific m b d, ⋯⟩ = ↑↑(m * 10 ^ d)
Module: Mathlib.Algebra.Divisibility.Units

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
a b : α
u : αˣ
⊢ a ∣ b * ↑u ↔ a ∣ b

Tactic:
apply dvd_mul_right

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

Goal state before:
pp: a b : ℤ
⊢ ↑(a /. b).den ∣ b

Tactic:
by
  by_cases b0 : b = 0; · simp [b0]
  rcases e : a /. b with ⟨n, d, h, c⟩
  rw [mk_eq_divInt,
    divInt_eq_divInt_iff b0 (ne_of_gt (Int.natCast_pos.2 (Nat.pos_of_ne_zero h)))] at e
  refine Int.dvd_natAbs.1 <| Int.natCast_dvd_natCast.2 <| c.symm.dvd_of_dvd_mul_left ?_
  rw [← Int.natAbs_mul, ← Int.natCast_dvd_natCast, Int.dvd_natAbs, ← e]; simp

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

Goal state before:
pp: q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
⊢ ∃ c, n = c * q.num ∧ d = c * ↑q.den

Tactic:
by
  obtain rfl | hn := eq_or_ne n 0
  · simp [qdf]
  have : q.num * d = n * ↑q.den := by
    refine (divInt_eq_divInt_iff ?_ hd).mp ?_
    · exact Int.natCast_ne_zero.mpr (Rat.den_nz _)
    · rwa [num_divInt_den]
  have hqdn : q.num ∣ n := by
    rw [qdf]
    exact Rat.num_dvd _ hd
  refine ⟨n / q.num, ?_, ?_⟩
  · rw [Int.ediv_mul_cancel hqdn]
  · 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.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₂ }
⊢ { num := n₁, den := d₁, den_nz := d₁0, reduced := c₁ } = { num := n₂, den := d₂, den_nz := d₂0, reduced := c₂ }

Tactic:
have d₁a : (d₁ : α) ≠ 0 := Nat.cast_ne_zero.2 d₁0
    have d₂a : (d₂ : α) ≠ 0 := Nat.cast_ne_zero.2 d₂0
    rw [mk_eq_divInt, mk_eq_divInt] at h ⊢
    rw [cast_divInt_of_ne_zero _ (by simpa), cast_divInt_of_ne_zero _ (by simpa)] at h
    norm_cast at h
    rwa [eq_div_iff_mul_eq d₂a, division_def, mul_assoc, (d₁.cast_commute (d₂ : α)).inv_left₀.eq,
      ← mul_assoc, ← division_def, eq_comm, eq_div_iff_mul_eq d₁a, eq_comm, ← Int.cast_natCast d₁,
      ← Int.cast_mul, ← Int.cast_natCast d₂, ← Int.cast_mul, Int.cast_inj, ← mkRat_eq_iff d₁0 d₂0]
      at h

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
⊢ node (id v) l r = node v l r

Tactic:
id_eq

Goal state after:
case node
α : Type u
v : α
l r : BinaryTree α
hl : map id l = l
hr : map id r = r
⊢ node v l r = node v l r
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: β : Type u_2
ι : Sort u_5
x : β
t : ι → Set β
⊢ insert x (⋂ i, t i) = ⋂ i, insert x (t i)

Tactic:
simp_rw [← union_singleton, iInter_union]

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLattice α
minAx : MinimalAxioms α
x✝ b c : α
h : x✝ ≤ sSup {c_1 | c_1 ⊓ b ≤ c}
⊢ sSup {c_1 | c_1 ⊓ b ≤ c} ⊓ b ≤ c

Tactic:
by simp [minAx.sSup_inf_eq]

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

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

Tactic:
by
  rw [← compl_compl (⋃₀ S), compl_sUnion]

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

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

Tactic:
simp only [mem_iUnion, mem_image, mem_preimage]

Goal state after:
ι : Type u_12
σ : ι → Type u_13
s : Set (Sigma σ)
x : (i : ι) × σ i
⊢ (∃ i x_1, ⟨i, x_1⟩ ∈ s ∧ ⟨i, x_1⟩ = x) ↔ x ∈ s
Module: Mathlib.Order.CompleteBooleanAlgebra

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

Tactic:
refine iSup_le fun g => ?_

Goal state after:
α : Type u
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLattice α
minAx : MinimalAxioms α
f : (i : ι) → κ i → α
g : ((i : ι) → κ i) → ι
⊢ ⨅ i, f (g i) (i (g i)) ≤ ⨆ i, ⨅ j, f i j
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
e : α ≃ β
inst✝ : CompleteLattice β
top : Top α := e.top
⊢ CompleteLattice α

Tactic:
let bot := e.bot

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
e : α ≃ β
inst✝ : CompleteLattice β
top : Top α := e.top
bot : Bot α := e.bot
⊢ CompleteLattice α
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
e : α ≃ β
inst✝ : CompleteLattice β
top : Top α := e.top
bot : Bot α := e.bot
⊢ CompleteLattice α

Tactic:
let supSet := e.supSet

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
e : α ≃ β
inst✝ : CompleteLattice β
top : Top α := e.top
bot : Bot α := e.bot
supSet : SupSet α := e.supSet
⊢ CompleteLattice α
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)
h : ¬∃ x, rhs < x ∧ x < lhs
⊢ lhs ≤ rhs

Tactic:
refine le_of_not_gt fun hrl : rhs < lhs => not_le_of_gt hrl ?_

Goal state after:
α✝ : 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)
h : ¬∃ x, rhs < x ∧ x < lhs
hrl : rhs < lhs
⊢ lhs ≤ rhs
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case neg.inr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
h : ConditionallyCompleteLinearOrder α
a b : α
hab : ¬a = b
h₂ : b ≤ a
⊢ min a b = if a ≤ b then a else b

Tactic:
· simp [show ¬(a ≤ b) from fun h => hab (le_antisymm h h₂), h₂]

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

Goal state before:
pp: case neg.inr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
h : ConditionallyCompleteLinearOrder α
a b : α
hab : ¬a = b
h₂ : b ≤ a
⊢ max a b = if a ≤ b then b else a

Tactic:
· simp [show ¬(a ≤ b) from fun h => hab (le_antisymm h h₂), h₂]

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
ι : Sort w
inst✝ : CompleteBooleanAlgebra α
f g : ι → α
⊢ ⨆ i, f i ≤ ⨆ x, g x ⊔ f x ∆ g x ∧ ⨆ i, g i ≤ ⨆ x, f x ⊔ f x ∆ g x

Tactic:
exact ⟨iSup_mono fun i ↦ sup_comm (g i) _ ▸ le_symmDiff_sup_right ..,
    iSup_mono fun i ↦ sup_comm (f i) _ ▸ symmDiff_comm (f i) _ ▸ le_symmDiff_sup_right ..⟩

Goal state after:
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 ↦ ?_)
      rcases ht y hy with ⟨x, xs, hyx⟩
      exact hyx.trans (le_csSup Bs xs)

Goal state after:
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PartialOrder γ
inst✝ : OrderBot γ
e : α → β
f : α → γ
hf : Pairwise (Disjoint on f)
he : FactorsThrough f e
b₁ b₂ : β
hne : b₁ ≠ b₂
⊢ (Disjoint on extend e f ⊥) b₁ b₂

Tactic:
rcases em (∃ a₁, e a₁ = b₁) with ⟨a₁, rfl⟩ | hb₁

Goal state after:
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PartialOrder γ
inst✝ : OrderBot γ
e : α → β
f : α → γ
hf : Pairwise (Disjoint on f)
he : FactorsThrough f e
b₂ : β
a₁ : α
hne : e a₁ ≠ b₂
⊢ (Disjoint on extend e f ⊥) (e a₁) b₂

case inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PartialOrder γ
inst✝ : OrderBot γ
e : α → β
f : α → γ
hf : Pairwise (Disjoint on f)
he : FactorsThrough f e
b₁ b₂ : β
hne : b₁ ≠ b₂
hb₁ : ¬∃ a₁, e a₁ = b₁
⊢ (Disjoint on extend e f ⊥) b₁ b₂
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
⊢ Monotone f ∨ Antitone f ↔ ∀ (a b c : α), c ∈ [[a, b]] → f c ∈ [[f a, f b]]

Tactic:
by
  constructor
  · rintro (hf | hf) a b c <;> simp_rw [← Icc_min_max, ← hf.map_min, ← hf.map_max]
    exacts [fun hc => ⟨hf hc.1, hf hc.2⟩, fun hc => ⟨hf hc.2, hf hc.1⟩]
  contrapose!
  rw [not_monotone_not_antitone_iff_exists_le_le]
  rintro ⟨a, b, c, hab, hbc, ⟨hfab, hfcb⟩ | ⟨hfba, hfbc⟩⟩
  · exact ⟨a, c, b, Icc_subset_uIcc ⟨hab, hbc⟩, fun h => h.2.not_gt <| max_lt hfab hfcb⟩
  · exact ⟨a, c, b, Icc_subset_uIcc ⟨hab, hbc⟩, fun h => h.1.not_gt <| lt_min hfba hfbc⟩

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

Goal state before:
pp: case mp
k w✝ : ℕ+
⊢ ↑k ∣ ↑(k * w✝)

Tactic:
apply dvd_mul_right

Goal state after:
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
m : ℤ
⊢ m ≤ ⌊a * ↑n⌋ / n ↔ m ≤ ⌊a⌋

Tactic:
Int.le_ediv_iff_mul_le hn,

Goal state after:
R : Type u_4
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
n : ℤ
hn : 0 < n
a : R
m : ℤ
⊢ m * n ≤ ⌊a * ↑n⌋ ↔ m ≤ ⌊a⌋
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 : a < 1
⊢ False

pp: case inr.inl
α : Type u_1
inst✝⁴ : CommGroup α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : DenselyOrdered α
inst✝ : Nontrivial α
h : IsCyclic α
ha : Surjective fun x ↦ 1 ^ x
⊢ False

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
⊢ False

Tactic:
· rcases exists_between hlt with ⟨b, hab, hb⟩
    rcases ha b with ⟨k, rfl⟩
    suffices 0 < k ∧ k < 1 by lia
    rw [← one_lt_inv'] at hlt
    simp_rw [← zpow_lt_zpow_iff_right hlt]
    simp_all

Goal state after:
case inr.inl
α : Type u_1
inst✝⁴ : CommGroup α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : DenselyOrdered α
inst✝ : Nontrivial α
h : IsCyclic α
ha : Surjective fun x ↦ 1 ^ x
⊢ False

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
⊢ False
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
x : R
⊢ (∃ z, -x = ↑z) ↔ ∃ z, x = ↑z

Tactic:
constructor <;> rintro ⟨z, hz⟩ <;> use -z <;> simp [← hz]

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
inst✝ : IsOrderedRing R
a b : R
⊢ ⌈a⌉ + ⌈b⌉ ≤ ⌈a + b⌉ + 1

Tactic:
by
  rw [← le_sub_iff_add_le, ceil_le, Int.cast_sub, Int.cast_add, Int.cast_one, le_sub_comm]
  refine (ceil_lt_add_one _).le.trans ?_
  rw [le_sub_iff_add_le', ← add_assoc, add_le_add_iff_right]
  exact le_ceil _

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

Goal state before:
pp: F : Type u_1
G : Type u_2
H : Type u_3
inst✝³ : FunLike F G H
a : G
b : H
inst✝² : AddCommMonoid G
inst✝¹ : AddMonoid H
inst✝ : AddConstMapClass F G H a b
f : F
n : ℕ
x : G
⊢ f (n • a + x) = f x + n • b

Tactic:
rw [add_comm, map_add_nsmul]

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

Goal state before:
pp: G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
a : G
ha : 1 < a
g : G
s : Set ℤ := {n | a ^ n ≤ g}
k✝ : ℕ
hk✝ : g⁻¹ ≤ a ^ k✝
h_ne : s.Nonempty
k : ℕ
hk : g ≤ a ^ k
h_bdd : ∀ n ∈ s, n ≤ ↑k
m : ℤ
hm : m ∈ s
hm' : ∀ z ∈ s, z ≤ m
⊢ g < a ^ (m + 1)

Tactic:
contrapose! hm'

Goal state after:
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
a : G
ha : 1 < a
g : G
s : Set ℤ := {n | a ^ n ≤ g}
k✝ : ℕ
hk✝ : g⁻¹ ≤ a ^ k✝
h_ne : s.Nonempty
k : ℕ
hk : g ≤ a ^ k
h_bdd : ∀ n ∈ s, n ≤ ↑k
m : ℤ
hm : m ∈ s
hm' : a ^ (m + 1) ≤ g
⊢ ∃ z ∈ s, m < z
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: K : Type u_4
inst✝⁴ : Semifield K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : Archimedean K
x y : K
inst✝ : ExistsAddOfLE K
hx : 0 < x
hy : 1 < y
m : ℤ
hle : y ^ m ≤ x⁻¹
hlt : x⁻¹ < y ^ (m + 1)
hyp : 0 < y
⊢ x ≤ y ^ (-(m + 1) + 1)

Tactic:
by
    rwa [neg_add, neg_add_cancel_right, zpow_neg, le_inv_comm₀ hx (zpow_pos hyp _)]

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

Goal state before:
pp: K : Type u_4
inst✝⁴ : Semifield K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : Archimedean K
inst✝ : ExistsAddOfLE K
a b c : K
h : a < b * c
hb₀ : 0 < b
hb₁ : b ≤ 1
hc₀ : 0 < c
hc₁ : c < 1
⊢ ∃ n, a < c ^ n ∧ c ^ n < b

Tactic:
have := exists_pow_lt_of_lt_one hb₀ hc₁

Goal state after:
K : Type u_4
inst✝⁴ : Semifield K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : Archimedean K
inst✝ : ExistsAddOfLE K
a b c : K
h : a < b * c
hb₀ : 0 < b
hb₁ : b ≤ 1
hc₀ : 0 < c
hc₁ : c < 1
this : ∃ n, c ^ n < b
⊢ ∃ n, a < c ^ n ∧ c ^ n < b
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: 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
⊢ ↑⌈a⌉ < b * a

Tactic:
obtain hab | hba := le_total a (b - 1)⁻¹
  · calc
      ⌈a⌉ ≤ (⌈(b - 1)⁻¹⌉ : k) := by gcongr
      _ < b * a := by rwa [← div_lt_iff₀']; positivity
  · rw [← sub_pos] at hb
    calc
      ⌈a⌉ < a + 1 := ceil_lt_add_one _
      _ = a + (b - 1) * (b - 1)⁻¹ := by rw [mul_inv_cancel₀]; positivity
      _ ≤ a + (b - 1) * a := by gcongr
      _ = b * a := by rw [sub_one_mul, add_sub_cancel]

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
a : R
⊢ Int.cast ⁻¹' Iio a = Iio ⌈a⌉

Tactic:
by
  ext
  simp [lt_ceil]

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

Goal state before:
pp: G : Type u_1
M : Type u_2
R : Type u_3
K : Type u_4
n m : ℕ
m0 : 0 < m
⊢ n ≤ n • m

Tactic:
rw [← mul_one n, nsmul_eq_mul, Nat.cast_id, mul_one]

Goal state after:
G : Type u_1
M : Type u_2
R : Type u_3
K : Type u_4
n m : ℕ
m0 : 0 < m
⊢ n ≤ n * m
Module: Mathlib.Data.Multiset.Defs

Goal state before:
pp: case mk.mk
α : Type u_1
β : Type v
γ : Type u_2
a✝ : Multiset α
l₁ : List α
b✝ : Multiset α
l₂ : List α
h₁ : Multiset.Le (Quot.mk (⇑(isSetoid α)) l₁) (Quot.mk (⇑(isSetoid α)) l₂)
h₂ : Multiset.Le (Quot.mk (⇑(isSetoid α)) l₂) (Quot.mk (⇑(isSetoid α)) l₁)
⊢ Quot.mk (⇑(isSetoid α)) l₁ = Quot.mk (⇑(isSetoid α)) l₂

Tactic:
exact Quot.sound (Subperm.antisymm h₁ h₂)

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

Goal state before:
pp: α : Type u_1
l : List α
a : α
⊢ l ~ [a] ↔ l = [a]

Tactic:
List.perm_singleton

Goal state after:
α : Type u_1
l : List α
a : α
⊢ l = [a] ↔ l = [a]
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: α : Type u
p : α → Bool
l : List α
⊢ l.Nodup → (List.filter p l).Nodup

Tactic:
simpa using! Pairwise.filter p

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

Goal state before:
pp: α : Type u
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₂ ≠ []
hl : l₂.head hne ∈ l₁
hnd : l₂.Nodup
⊢ l₁ <+: l₂

Tactic:
by
  grind [List.IsInfix]

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

Goal state before:
pp: α : Type u
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₂ ≠ []
hl : l₂.getLast hne ∈ l₁
hnd : l₂.Nodup
⊢ l₁ <:+ l₂

Tactic:
by
  grind [List.IsInfix]

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

Goal state before:
pp: α : Type u
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₂ ≠ []
hlh : l₂.head hne ∈ l₁
hlg : l₂.getLast hne ∈ l₁
hnd : l₂.Nodup
⊢ l₁ = l₂

Tactic:
by
  grind [List.IsInfix]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n m : ℕ
h : xs ~ ys
h' : ys.Nodup
this : n ≤ n + m
h₂ : xs.Nodup
⊢ List.take n xs ++ List.drop (n + m) xs ~ ys ∩ (List.take n xs ++ List.drop (n + m) xs)

Tactic:
apply Perm.trans _ (Perm.inter_append _).symm

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n m : ℕ
h : xs ~ ys
h' : ys.Nodup
this : n ≤ n + m
h₂ : xs.Nodup
⊢ List.take n xs ++ List.drop (n + m) xs ~ ys ∩ List.take n xs ++ ys ∩ List.drop (n + m) xs

α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n m : ℕ
h : xs ~ ys
h' : ys.Nodup
this : n ≤ n + m
h₂ : xs.Nodup
⊢ (List.take n xs).Disjoint (List.drop (n + m) xs)
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
⊢ t ∩ u + s = (s + t) ∩ (s + u)

Tactic:
inter_add_distrib,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
⊢ (t + s) ∩ (u + s) = (s + t) ∩ (s + u)