mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
inst✝¹ : Add α
a : α
inst✝ : LE α
ha : AddLECancellable a
⊢ AddLECancellable ↑a

Tactic:
by
  rintro (_ | b) (_ | c)
  · simp [none_eq_bot]
  · simp [none_eq_bot]
  · simp [some_eq_coe, ← coe_add, none_eq_bot]
  · simpa [none_eq_bot, some_eq_coe, ← coe_add] using fun a ↦ ha a

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedCancelMonoid α
a : α
x✝¹ : 0 < ↑a
c : α
x✝ : 0 < ↑c
⊢ ↑a * 0 < ↑a * ↑c

Tactic:
simp [← WithZero.coe_mul]

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

Goal state before:
pp: case inr
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
n : ℕ
hn : n ≠ 0
a : R
ha : 0 ≤ a
m : ℕ
⊢ ↑(m * n) ≤ a * ↑n ↔ m ≤ ⌊a⌋₊

Tactic:
le_floor_iff ha,

Goal state after:
case inr
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
n : ℕ
hn : n ≠ 0
a : R
ha : 0 ≤ a
m : ℕ
⊢ ↑(m * n) ≤ a * ↑n ↔ ↑m ≤ a
Module: Mathlib.Algebra.Group.Invertible.Defs

Goal state before:
pp: α : Type u
inst✝¹ : Monoid α
a b c : α
inst✝ : Invertible c
⊢ a * ⅟c * c = b * c ↔ a = b * c

Tactic:
invOf_mul_cancel_right

Goal state after:
α : Type u
inst✝¹ : Monoid α
a b c : α
inst✝ : Invertible c
⊢ a = b * c ↔ a = b * c
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : Preorder α
inst✝ : Std.Trichotomous fun x1 x2 ↦ x1 < x2
x y : WithBot α
⊢ x < y ∨ x = y ∨ y < x

Tactic:
by
    cases x <;> cases y <;> simp [trichotomous]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : Preorder α
inst✝ : Std.Trichotomous fun x1 x2 ↦ x1 < x2
x y : WithTop α
⊢ x < y ∨ x = y ∨ y < x

Tactic:
by
    cases x <;> cases y <;> simp [trichotomous]

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

Goal state before:
pp: case succ
α : Type u_1
inst✝² : CommRing α
inst✝¹ : LinearOrder α
a b : α
n✝ : ℕ
inst✝ : IsOrderedRing α
n : ℕ
ih : |geomSum a b n| ≤ (↑n + 1) * max |a| |b| ^ n
⊢ |a * geomSum a b n| + |b ^ (n + 1)| ≤ (↑(n + 1) + 1) * max |a| |b| ^ (n + 1)

Tactic:
abs_mul,

Goal state after:
case succ
α : Type u_1
inst✝² : CommRing α
inst✝¹ : LinearOrder α
a b : α
n✝ : ℕ
inst✝ : IsOrderedRing α
n : ℕ
ih : |geomSum a b n| ≤ (↑n + 1) * max |a| |b| ^ n
⊢ |a| * |geomSum a b n| + |b ^ (n + 1)| ≤ (↑(n + 1) + 1) * max |a| |b| ^ (n + 1)
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: case succ
α : Type u_1
inst✝² : CommRing α
inst✝¹ : LinearOrder α
a b : α
inst✝ : IsOrderedRing α
n : ℕ
⊢ |(a - b) * geomSum a b n| ≤ |a - b| * ↑(n + 1) * max |a| |b| ^ n

Tactic:
abs_mul,

Goal state after:
case succ
α : Type u_1
inst✝² : CommRing α
inst✝¹ : LinearOrder α
a b : α
inst✝ : IsOrderedRing α
n : ℕ
⊢ |a - b| * |geomSum a b n| ≤ |a - b| * ↑(n + 1) * max |a| |b| ^ n
Module: Mathlib.Logic.Equiv.Set

Goal state before:
pp: α✝¹ : Sort u
β✝¹ : Sort v
γ : Sort w
α✝ : Type u_1
β✝ : Type u_2
α : Type u_3
β : Type u_4
f : α → β
s : Set ↑(range f)
x : ↑(rangeSplitting f '' s)
⊢ ⟨f ↑x, ⋯⟩ ∈ s

Tactic:
by
      rcases x with ⟨x, ⟨y, ⟨m, rfl⟩⟩⟩
      simpa [apply_rangeSplitting f] using m

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

Goal state before:
pp: α : Type u_3
β : Type u_4
f : α → β
f_inv : Nonempty α → β → α
hf : ∀ (h : Nonempty α), LeftInverse (f_inv h) f
⊢ ofLeftInverse f f_inv hf = ofInjective f ⋯

Tactic:
by
  ext
  simp

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

Goal state before:
pp: α : Type u_3
β : Type u_4
f : α → β
f_inv : β → α
hf : LeftInverse f_inv f
⊢ ofLeftInverse' f f_inv hf = ofInjective f ⋯

Tactic:
by
  ext
  simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
h : Icc a b = Ioc a b
⊢ ¬a ≤ b

Tactic:
by simpa using Set.ext_iff.mp h a

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
h : Ioc a b = Ico a b
⊢ ¬a < b

Tactic:
by simpa using Set.ext_iff.mp h a

Goal state after:
Module: Mathlib.Tactic.Abel

Goal state before:
pp: α : Type u_1
inst✝ : AddCommMonoid α
x a : α
⊢ term 0 x a = a

Tactic:
by
  simp [term, zero_nsmul]

Goal state after:
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)
⊢ ↑na * ⅟↑da * (↑nb * ⅟↑db) = ↑nc * ⅟↑dc

Tactic:
simp only [Int.cast_mul, Int.cast_natCast] at 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
⊢ ↑na * ⅟↑da * (↑nb * ⅟↑db) = ↑nc * ⅟↑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
⊢ b / c ≤ a ↔ c * a ≤ b

Tactic:
rw [mul_comm, div_le_iff_of_neg hc]

Goal state after:
Module: Mathlib.Tactic.NormNum.Basic

Goal state before:
pp: x y : ℕ
⊢ x.ble y = false ↔ y < x

Tactic:
rw [← Nat.not_le, ← Bool.not_eq_true, Nat.ble_eq]

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

Goal state before:
pp: α : Type u
l : List α
h : l ≠ []
⊢ drop (l.length - 1) l = [l.getLast h]

Tactic:
induction l with
  | nil => aesop
  | cons a l ih =>
    by_cases hl : l = []
    · simp_all
    rw [length_cons, Nat.add_one_sub_one, List.drop_length_cons hl a]
    simp [getLast_cons, hl]

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 b : α
hb : b < 0
h : a < b
⊢ 1 / b < 1 / a

Tactic:
rwa [div_lt_iff_of_neg' hb, ← div_eq_mul_one_div, div_lt_one_of_neg (h.trans hb)]

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

Goal state before:
pp: case ha
α : 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| ≤ 1 ∧ |q - r| + |q - r| * ↑n * (B + 1) ^ (n - 1) ≤ ε
h : 0 < |q - r|
⊢ 0 ≤ max |q| |r|

Tactic:
exact (abs_nonneg _).trans le_sup_left

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
a b : α
m n : ℕ
h : a ≠ b
x✝ : α
⊢ x✝ ∈ l → x✝ = b ∨ x✝ = a ↔ x✝ ≠ b → x✝ ≠ a → ¬x✝ ∈ l

Tactic:
← and_imp,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
a b : α
m n : ℕ
h : a ≠ b
x✝ : α
⊢ x✝ ∈ l → x✝ = b ∨ x✝ = a ↔ x✝ ≠ b ∧ x✝ ≠ a → ¬x✝ ∈ l
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: case pos
α : Type u_1
inst✝ : GroupWithZero α
a : α
m n : ℤ
ha : ¬a = 0
hn : n = 0
⊢ zpow' a (m * n) = zpow' (zpow' a m) n

pp: case neg
α : Type u_1
inst✝ : GroupWithZero α
a : α
m n : ℤ
ha : ¬a = 0
hn : ¬n = 0
⊢ zpow' a (m * n) = zpow' (zpow' a m) n

Tactic:
· rw [hn]
    simp [zpow', ha, zpow_ne_zero ]

Goal state after:
case neg
α : Type u_1
inst✝ : GroupWithZero α
a : α
m n : ℤ
ha : ¬a = 0
hn : ¬n = 0
⊢ zpow' a (m * n) = zpow' (zpow' a m) n
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
inst✝ : Inhabited α
l : List α
h : l ≠ []
⊢ l.head! ∈ l

Tactic:
have h' : l.head! ∈ l.head! :: l.tail := mem_cons_self
  rwa [cons_head!_tail h] at h'

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

Goal state before:
pp: M : Type u_1
inst✝ : CommGroupWithZero M
n : ℤ
e : M
t t_n t_d : NF M
h : t.eval = t_n.eval / t_d.eval
⊢ ((-n, e) ::ᵣ t).eval = t_n.eval / ((n, e) ::ᵣ t_d).eval

Tactic:
simp only [eval_cons, h, zpow'_neg, div_eq_mul_inv, mul_inv]
  ac_rfl

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
g : β → α
h : LeftInverse f g
x : β
xs : List β
⊢ map f (map g (x :: xs)) = x :: xs

Tactic:
by simp_rw [map_cons, h x, h.list_map xs]

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

Goal state before:
pp: ι : Type u_1
α : Type u
β : Type v
γ : Type w
l : List ι
f : α → β → γ
op₁ : ι → α → α
op₂ : ι → β → β
op₃ : ι → γ → γ
a : α
b : β
h : ∀ (a : α) (b : β) (i : ι), f (op₁ i a) (op₂ i b) = op₃ i (f a b)
⊢ foldr op₃ (f a b) l = f (foldr op₁ a l) (foldr op₂ b l)

Tactic:
revert a

Goal state after:
ι : Type u_1
α : Type u
β : Type v
γ : Type w
l : List ι
f : α → β → γ
op₁ : ι → α → α
op₂ : ι → β → β
op₃ : ι → γ → γ
b : β
h : ∀ (a : α) (b : β) (i : ι), f (op₁ i a) (op₂ i b) = op₃ i (f a b)
⊢ ∀ (a : α), foldr op₃ (f a b) l = f (foldr op₁ a l) (foldr op₂ b l)
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: G : Type u_7
inst✝¹ : CommGroup G
A : Type u_8
inst✝ : DecidableEq A
l : List A
f g : A → G
a : A
⊢ (map (fun x ↦ if x = a then f x else g x) l).prod = (f a / g a) ^ count a l * (map g l).prod

Tactic:
induction l with
  | nil => simp
  | cons x xs ih =>
    simp only [map_cons, prod_cons, count_cons] at ih ⊢
    rw [ih]
    clear ih
    by_cases hx : x = a
    · simp only [hx, ite_true, pow_add, pow_one, div_eq_mul_inv, mul_assoc, mul_comm, mul_left_comm,
      mul_inv_cancel_left, beq_self_eq_true]
    · simp only [hx, ite_false, add_zero, mul_assoc, mul_comm (g x) _, beq_iff_eq]

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

Goal state before:
pp: α : Type u
β : Type v
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : β → α → m β
b : β
l : List α
⊢ foldlM f b l =
    foldl
      (fun mb a ↦ do
        let b ← mb
        f b a)
      (pure b) l

Tactic:
suffices h :
    ∀ mb : m β, (mb >>= fun b => List.foldlM f b l) = foldl (fun mb a => mb >>= fun b => f b a) mb l
    by simp [← h (pure b)]

Goal state after:
α : Type u
β : Type v
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : β → α → m β
b : β
l : List α
⊢ ∀ (mb : m β),
    (do
        let b ← mb
        foldlM f b l) =
      foldl
        (fun mb a ↦ do
          let b ← mb
          f b a)
        mb l
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: case cons
n a : ℕ
l : List ℕ
ih : l.sum % n = (map (fun x ↦ x % n) l).sum % n
⊢ (a :: l).sum % n = (map (fun x ↦ x % n) (a :: l)).sum % n

Tactic:
simpa only [map_cons, sum_cons, Nat.mod_add_mod, Nat.add_mod_mod] using congr((a + $ih) % n)

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

Goal state before:
pp: q : ℚ≥0
hq : q ≠ 0
⊢ q⁻¹.den = q.num

Tactic:
by
  rw [inv_def, divNat, den, coe_mk, Rat.divInt_ofNat, ← Rat.mk_eq_mkRat _ _ (num_ne_zero.mpr hq)]
  simpa using q.coprime_num_den.symm

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

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

Tactic:
apply mul_right_dvd

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

Goal state before:
pp: α : Type u_1
inst✝ : MonoidWithZero α
x y : α
nonzero : ¬(x = 0 ∧ y = 0)
H : ∀ (z : α), ¬IsUnit z → z ≠ 0 → z ∣ x → ¬z ∣ y
hx : 0 ∣ x
hy : 0 ∣ y
h : ¬IsUnit 0
⊢ False

Tactic:
exact nonzero ⟨zero_dvd_iff.1 hx, zero_dvd_iff.1 hy⟩

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

Goal state before:
pp: n : ℤ
q : ℚ
⊢ (q + ↑n).den = q.den

Tactic:
add_intCast_den

Goal state after:
n : ℤ
q : ℚ
⊢ q.den = q.den
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: q : ℚ
n : ℤ
⊢ (q + ↑(-n)).den = q.den

Tactic:
add_intCast_den

Goal state after:
q : ℚ
n : ℤ
⊢ q.den = q.den
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: case left
a b c d : ℤ
hb0 : 0 < b
hd0 : 0 < d
h1 : a.natAbs.Coprime b.natAbs
h2 : c.natAbs.Coprime d.natAbs
h : ↑a / ↑b = ↑c / ↑d
⊢ a = c

Tactic:
rw [← num_div_eq_of_coprime hb0 h1, h, num_div_eq_of_coprime hd0 h2]

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

Goal state before:
pp: F : Type u_1
α : Type u_3
inst✝² : DivisionRing α
inst✝¹ : FunLike F ℚ α
inst✝ : RingHomClass F ℚ α
f : F
q : ℚ
⊢ f q = ↑q

Tactic:
← map_ratCast f,

Goal state after:
F : Type u_1
α : Type u_3
inst✝² : DivisionRing α
inst✝¹ : FunLike F ℚ α
inst✝ : RingHomClass F ℚ α
f : F
q : ℚ
⊢ f q = f ↑q
Module: Mathlib.Tactic.Ring.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Mul α
a a' : α
h : a = a'
b : α
⊢ a • b = a' * b

Tactic:
subst h
  rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
f : α ≃o β
x✝ : ι → α
x : α
⊢ f (⨆ i, x✝ i) ≤ f x ↔ ⨆ i, f (x✝ i) ≤ f x

Tactic:
by simp only [f.le_iff_le, iSup_le_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
κ : ι → Sort u_6
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
f : α ≃o β
x✝ : (i : ι) → κ i → α
x : α
⊢ f (⨆ i, ⨆ j, x✝ i j) ≤ f x ↔ ⨆ i, ⨆ j, f (x✝ i j) ≤ f x

Tactic:
by simp only [f.le_iff_le, iSup_le_iff]

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
minAx : MinimalAxioms α
a : α
s : Set α
⊢ a ⊓ sSup s ≤ ⨆ b ∈ s, a ⊓ b

Tactic:
by
    calc
      _ = ⨅ i : ULift.{u} Bool, ⨆ j : match i with | .up true => PUnit.{u + 1} | .up false => s,
          match i with
          | .up true => a
          | .up false => j := by simp [sSup_eq_iSup', iSup_unique, iInf_bool_eq]
      _ ≤ _ := by
        simp only [minAx.iInf_iSup_eq, iInf_ulift, iInf_bool_eq, iSup_le_iff]
        exact fun x ↦ le_biSup _ (x (.up false)).2

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

Goal state before:
pp: α : Type u_1
ι : Type u_12
σ : Type u_13
s : ι → Set α
t : σ → Set α
⊢ ⋃ x, Sum.elim s t x = (⋃ x, s x) ∪ ⋃ x, t x

Tactic:
by
  ext
  simp

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

Goal state before:
pp: α : Type u_1
π : α → Type u_12
i : Set α
s : (a : α) → Set (π a)
⊢ i.pi s = ⋂ a ∈ i, eval a ⁻¹' s a

Tactic:
by
  ext
  simp

Goal state after:
Module: Mathlib.Order.LatticeIntervals

Goal state before:
pp: α : Type u_1
a : α
inst✝¹ : Lattice α
inst✝ : OrderBot α
x y : ↑(Iic a)
⊢ IsCompl x y ↔ Disjoint ↑x ↑y ∧ ↑x ⊔ ↑y = a

Tactic:
_root_.isCompl_iff,

Goal state after:
α : Type u_1
a : α
inst✝¹ : Lattice α
inst✝ : OrderBot α
x y : ↑(Iic a)
⊢ Disjoint x y ∧ Codisjoint x y ↔ Disjoint ↑x ↑y ∧ ↑x ⊔ ↑y = a
Module: Mathlib.Order.LatticeIntervals

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderTop α
a : α
x y : ↑(Ici a)
⊢ IsCompl x y ↔ ↑x ⊓ ↑y = a ∧ Codisjoint ↑x ↑y

Tactic:
_root_.isCompl_iff,

Goal state after:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderTop α
a : α
x y : ↑(Ici a)
⊢ Disjoint x y ∧ Codisjoint x y ↔ ↑x ⊓ ↑y = a ∧ Codisjoint ↑x ↑y
Module: Mathlib.Order.LatticeIntervals

Goal state before:
pp: α : Type u_1
a b : α
inst✝¹ : Lattice α
inst✝ : Fact (a ≤ b)
x y : ↑(Icc a b)
⊢ IsCompl x y ↔ ↑x ⊓ ↑y = a ∧ ↑x ⊔ ↑y = b

Tactic:
_root_.isCompl_iff,

Goal state after:
α : Type u_1
a b : α
inst✝¹ : Lattice α
inst✝ : Fact (a ≤ b)
x y : ↑(Icc a b)
⊢ Disjoint x y ∧ Codisjoint x y ↔ ↑x ⊓ ↑y = a ∧ ↑x ⊔ ↑y = b
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
inst✝ : Frame α
ι : Type u_1
f : ι → α
h : Pairwise (Disjoint on f)
s t : Set ι
⊢ ⨆ i ∈ s ∩ t, f i = (⨆ i ∈ s, f i) ⊓ ⨆ i ∈ t, f i

Tactic:
biSup_inf_biSup

Goal state after:
α : Type u
inst✝ : Frame α
ι : Type u_1
f : ι → α
h : Pairwise (Disjoint on f)
s t : Set ι
⊢ ⨆ i ∈ s ∩ t, f i = ⨆ p ∈ s ×ˢ t, f p.1 ⊓ f p.2
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
a b : α
hab : a ≤ b
h' : MonotoneOn f (Icc a b)
⊢ sInf (f '' Icc a b) = f a

Tactic:
refine IsGLB.csInf_eq ?_ ((nonempty_Icc.mpr hab).image f)

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
a b : α
hab : a ≤ b
h' : MonotoneOn f (Icc a b)
⊢ IsGLB (f '' Icc a b) (f a)
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
a b : α
hab : a ≤ b
h' : AntitoneOn f (Icc a b)
this : Icc a b = Icc (toDual b) (toDual a)
⊢ sInf (f '' Icc a b) = f b

Tactic:
rw [this] at h' ⊢

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
a b : α
hab : a ≤ b
h' : AntitoneOn f (Icc (toDual b) (toDual a))
this : Icc a b = Icc (toDual b) (toDual a)
⊢ sInf (f '' Icc (toDual b) (toDual a)) = f b
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ a ∉ Ι b c ↔ a ≤ b ∧ a ≤ c ∨ c < a ∧ b < a

Tactic:
simp only [uIoc_eq_union, mem_union, mem_Ioc, ← not_le]

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b) ↔ a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b
Module: Mathlib.Order.Interval.Set.OrdConnected

Goal state before:
pp: α : Type u_3
inst✝ : PartialOrder α
a : α
⊢ {a}.OrdConnected

Tactic:
rw [← Icc_self]

Goal state after:
α : Type u_3
inst✝ : PartialOrder α
a : α
⊢ (Icc a a).OrdConnected
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝² : One M
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq M
f : ι → M
x : ι
y : M
⊢ mulSupport (update f x y) = if y = 1 then mulSupport f \ {x} else insert x (mulSupport f)

Tactic:
by
  rcases eq_or_ne y 1 with rfl | hy <;> simp [mulSupport_update_one, mulSupport_update_of_ne_one, *]

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

Goal state before:
pp: n m : ℕ
hnm : n ≤ m
⊢ n ! * (n + 1) ^ (m - n) ≤ m !

Tactic:
simpa [hnm] using @Nat.factorial_mul_pow_le_factorial n (m - n)

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

Goal state before:
pp: case pos
k m n : ℕ
hkm : k ≤ m
hmn : ¬m ≤ n
hkn : k ≤ n
⊢ (n - k).descFactorial (m - k) * n.descFactorial k = 0

Tactic:
rw [descFactorial_eq_zero_iff_lt.mpr (show n - k < m - k by lia), Nat.zero_mul]

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

Goal state before:
pp: F : Type u_2
α : Type u_3
β : Type u_4
inst✝⁵ : FunLike F α β
inst✝⁴ : Group α
inst✝³ : AddCommGroup β
inst✝² : LinearOrder β
inst✝¹ : IsOrderedAddMonoid β
inst✝ : GroupSeminormClass F α β
f : F
x y : α
⊢ f x - f y ≤ f (x / y) ∧ f y - f x ≤ f (x / y)

Tactic:
sub_le_iff_le_add',

Goal state after:
F : Type u_2
α : Type u_3
β : Type u_4
inst✝⁵ : FunLike F α β
inst✝⁴ : Group α
inst✝³ : AddCommGroup β
inst✝² : LinearOrder β
inst✝¹ : IsOrderedAddMonoid β
inst✝ : GroupSeminormClass F α β
f : F
x y : α
⊢ f x ≤ f y + f (x / y) ∧ f y - f x ≤ f (x / y)
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: case inr
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
hx : x < ↑z
⊢ 1 - fract x ≤ |x - ↑z|

Tactic:
rw [abs_eq_neg_self.mpr (sub_neg.mpr hx).le]

Goal state after:
case inr
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
hx : x < ↑z
⊢ 1 - fract x ≤ -(x - ↑z)
Module: Mathlib.Data.PNat.Basic

Goal state before:
pp: case pos
k m : ℕ+
h : m.mod k = k
h' : ↑m % ↑k = 0
⊢ ↑m % ↑k = 0

pp: case neg
k m : ℕ+
h : m.mod k = k
h' : ¬↑m % ↑k = 0
⊢ ↑m % ↑k = 0

Tactic:
· exact h'

Goal state after:
case neg
k m : ℕ+
h : m.mod k = k
h' : ¬↑m % ↑k = 0
⊢ ↑m % ↑k = 0
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⌋ - 1 - a ≤ b - 1

Tactic:
sub_le_iff_le_add',

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
⊢ ↑⌊a + b⌋ - 1 ≤ a + (b - 1)
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
x k : R
hk : 1 < k
⊢ k * x = k * ↑⌊x⌋ + 1 ↔ ∃ n, k * x = k * ↑n + 1

Tactic:
refine ⟨fun hx ↦ ⟨⌊x⌋, hx⟩, ?_⟩

Goal state after:
R : Type u_4
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
x k : R
hk : 1 < k
⊢ (∃ n, k * x = k * ↑n + 1) → k * x = k * ↑⌊x⌋ + 1
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: n d : ℕ
n_coprime_d : n.Coprime d
⊢ (↑n - ↑d * ⌊↑n / ↑d⌋).natAbs.Coprime d

Tactic:
have : (n : ℤ) % d = n - d * ⌊(n : ℚ) / d⌋ := Int.mod_nat_eq_sub_mul_floor_rat_div

Goal state after:
n d : ℕ
n_coprime_d : n.Coprime d
this : ↑n % ↑d = ↑n - ↑d * ⌊↑n / ↑d⌋
⊢ (↑n - ↑d * ⌊↑n / ↑d⌋).natAbs.Coprime d
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✝⁶ : AddCommGroup G
inst✝⁵ : LinearOrder G
inst✝⁴ : IsOrderedAddMonoid G
inst✝³ : Archimedean G
inst✝² : AddGroup H
inst✝¹ : AddConstMapClass F G H a b
f : F
R : H → H → Prop
inst✝ : IsTrans H R
hR : CovariantClass H H (fun x y ↦ y + x) R
ha : 0 < a
l : G
hf : ∀ x ∈ Icc l (l + a), ∀ y ∈ Icc l (l + a), x < y → R (f x) (f y)
x y : G
hxy : (fun x1 x2 ↦ x1 < x2) x y
⊢ R (f x) (f y)

Tactic:
by
  replace hR := hR.elim
  have ha' : 0 ≤ a := ha.le
  -- Shift both points by `m • a` so that `l ≤ x < l + a`
  wlog hx : x ∈ Ico l (l + a) generalizing x y
  · rcases existsUnique_sub_zsmul_mem_Ico ha x l with ⟨m, hm, -⟩
    suffices R (f (x - m • a)) (f (y - m • a)) by simpa using hR (m • b) this
    exact this _ _ (by simpa) hm
  · -- Now find `n` such that `l + n • a < y ≤ l + (n + 1) • a`
    rcases existsUnique_sub_zsmul_mem_Ioc ha y l with ⟨n, hny, -⟩
    rcases lt_trichotomy n 0 with hn | rfl | hn
    · -- Since `l ≤ x ≤ y`, the case `n < 0` is impossible
      refine absurd ?_ hxy.not_ge
      calc
        y ≤ l + a + n • a := sub_le_iff_le_add.1 hny.2
        _ = l + (n + 1) • a := by rw [add_comm n, add_smul, one_smul, add_assoc]
        _ ≤ l + (0 : ℤ) • a := by gcongr; lia
        _ ≤ x := by simpa using hx.1
    · -- If `n = 0`, then `l < y ≤ l + a`, hence we can apply the assumption
      exact hf x (Ico_subset_Icc_self hx) y (by simpa using Ioc_subset_Icc_self hny) hxy
    · -- In the remaining case `0 < n` we use transitivity.
      -- If `R = (· < ·)`, then the proof looks like
      -- `f x < f (l + a) ≤ f (l + n • a) < f y`
      trans f (l + (1 : ℤ) • a)
      · grind
      have hy : R (f (l + n • a)) (f y) := by
        rw [← sub_add_cancel y (n • a), map_add_zsmul, map_add_zsmul]
        refine hR _ <| hf _ ?_ _ (Ioc_subset_Icc_self hny) hny.1; simpa
      rw [← Int.add_one_le_iff, zero_add] at hn
      rcases hn.eq_or_lt with rfl | hn; · assumption
      trans f (l + n • a)
      · refine Int.rel_of_forall_rel_succ_of_lt R (f := (f <| l + · • a)) (fun k ↦ ?_) hn
        simp_rw [add_comm k 1, add_zsmul, ← add_assoc, one_zsmul, map_add_zsmul]
        refine hR (k • b) (hf _ ?_ _ ?_ ?_) <;> simpa
      · assumption

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

Goal state before:
pp: α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : List α
hl : l₂ <+~ l₁
p : α → Bool
⊢ countP p l₁ = countP p (l₁.diff l₂ ++ l₂)

Tactic:
exact ((subperm_append_diff_self_of_count_le <| subperm_ext_iff.1 hl).symm.trans
    perm_append_comm).countP_eq _

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
h : ¬a ∈ s
⊢ (s.erase a).card = if a ∈ s then s.card.pred else s.card

Tactic:
· rwa [erase_of_notMem h, if_neg]

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

Goal state before:
pp: case zero
α : Type u_1
β : Type v
r : α → β → Prop
s : Multiset α
t : Multiset β
u : Multiset α
v : Multiset β
huv : Rel r u v
⊢ Rel r (0 + u) (0 + v)

Tactic:
simpa using huv

Goal state after: