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

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : LinearOrder G₀
a : G₀
inst✝¹ : PosMulStrictMono G₀
inst✝ : ZeroLEOneClass G₀
⊢ a⁻¹ < 1 ↔ a ≤ 0 ∨ 1 < a

Tactic:
by
  simp_rw [← not_le, one_le_inv_iff₀, not_and_or, not_lt]

Goal state after:
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b c : α
⊢ |(a ⊔ c) / (b ⊔ c)|ₘ * |(a ⊓ c) / (b ⊓ c)|ₘ = |a / b|ₘ

Tactic:
let : DistribLattice α := CommGroup.toDistribLattice α

Goal state after:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b c : α
this : DistribLattice α := CommGroup.toDistribLattice α
⊢ |(a ⊔ c) / (b ⊔ c)|ₘ * |(a ⊓ c) / (b ⊓ c)|ₘ = |a / b|ₘ
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : Group α
inst✝ : LinearOrder α
b : α
h : |(|b|ₘ)|ₘ = |b|ₘ
⊢ |b|ₘ = b ∨ |b|ₘ = b⁻¹

Tactic:
simpa only [inv_eq_iff_eq_inv (a := |b|ₘ), inv_inv, inv_inj, or_comm] using mabs_choice b

Goal state after:
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : Group α
inst✝ : LinearOrder α
b : α
h : ||b|ₘ⁻¹|ₘ = |b|ₘ
⊢ |b|ₘ⁻¹ = b ∨ |b|ₘ⁻¹ = b⁻¹

Tactic:
simpa only [inv_eq_iff_eq_inv (a := |b|ₘ), inv_inv, inv_inj, or_comm] using mabs_choice b

Goal state after:
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: case H1
x y a b : ℕ
h : 0 < a
IH :
  ∀ {s t s' t' : ℤ},
    ↑b % ↑a = ↑x * s + ↑y * t →
      ↑a = ↑x * s' + ↑y * t' →
        ↑((b % a).xgcdAux s t a s' t').1 =
          ↑x * ((b % a).xgcdAux s t a s' t').2.1 + ↑y * ((b % a).xgcdAux s t a s' t').2.2
s t s' t' : ℤ
p : ↑a = ↑x * s + ↑y * t
p' : ↑b = ↑x * s' + ↑y * t'
k : ℤ
⊢ ↑b - (↑x * s + ↑y * t) * k = ↑x * (s' - k * s) + ↑y * (t' - k * t)

Tactic:
p',

Goal state after:
case H1
x y a b : ℕ
h : 0 < a
IH :
  ∀ {s t s' t' : ℤ},
    ↑b % ↑a = ↑x * s + ↑y * t →
      ↑a = ↑x * s' + ↑y * t' →
        ↑((b % a).xgcdAux s t a s' t').1 =
          ↑x * ((b % a).xgcdAux s t a s' t').2.1 + ↑y * ((b % a).xgcdAux s t a s' t').2.2
s t s' t' : ℤ
p : ↑a = ↑x * s + ↑y * t
p' : ↑b = ↑x * s' + ↑y * t'
k : ℤ
⊢ ↑x * s' + ↑y * t' - (↑x * s + ↑y * t) * k = ↑x * (s' - k * s) + ↑y * (t' - k * t)
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : Preorder α
x y : WithBot α
⊢ x < y ↔ x ≤ y ∧ ¬y ≤ x

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

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

Goal state before:
pp: case refine_3.inl
α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
x✝ : Nontrivial αˣ ∧ DenselyOrdered αˣ
H₁ : Nontrivial αˣ
H₂ : DenselyOrdered αˣ
y : αˣ
h : 0 < ↑y
⊢ ∃ a, 0 < a ∧ a < ↑y

Tactic:
obtain ⟨z, hz⟩ := exists_one_lt' (α := αˣ)

Goal state after:
case refine_3.inl
α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
x✝ : Nontrivial αˣ ∧ DenselyOrdered αˣ
H₁ : Nontrivial αˣ
H₂ : DenselyOrdered αˣ
y : αˣ
h : 0 < ↑y
z : αˣ
hz : 1 < z
⊢ ∃ a, 0 < a ∧ a < ↑y
Module: Mathlib.Data.Nat.Find

Goal state before:
pp: n : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
hₘ : ∃ m, p (m + n)
hₙ : ∃ n, p n
hn : n ≤ Nat.find hₙ
⊢ Nat.find hₘ + n = Nat.find hₙ

Tactic:
by
  refine le_antisymm ((le_find_iff _ _).2 fun m hm hpm => Nat.not_le.2 hm ?_) ?_
  · have hnm : n ≤ m := le_trans hn (find_le hpm)
    refine Nat.add_le_of_le_sub hnm (find_le ?_)
    rwa [Nat.sub_add_cancel hnm]
  · rw [← Nat.sub_le_iff_le_add]
    refine (le_find_iff _ _).2 fun m hm hpm => Nat.not_le.2 hm ?_
    rw [Nat.sub_le_iff_le_add]
    exact find_le hpm

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
x y : WithZero α
hx : x ≠ 0
hy : y ≠ 0
⊢ min x y ≠ 0

Tactic:
by simp [min_eq_iff, hx, hy]

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

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

Tactic:
rw [← Nat.lt_ceil, Nat.add_one_le_iff]

Goal state after:
Module: Mathlib.Algebra.Group.Invertible.Defs

Goal state before:
pp: α : Type u
inst✝ : Monoid α
a b : α
x✝ : Invertible a
⊢ a * (⅟a * b) = b

Tactic:
by
  rw [← mul_assoc, mul_invOf_self, one_mul]

Goal state after:
Module: Mathlib.Order.Directed

Goal state before:
pp: β : Type u_2
inst✝² : PartialOrder β
inst✝¹ : Nontrivial β
inst✝ : IsDirectedOrder β
b : β
hb : IsMax b
hb' : IsMin b
⊢ False

Tactic:
obtain ⟨a, c, hac⟩ := exists_lt_of_directed_le β

Goal state after:
β : Type u_2
inst✝² : PartialOrder β
inst✝¹ : Nontrivial β
inst✝ : IsDirectedOrder β
b : β
hb : IsMax b
hb' : IsMin b
a c : β
hac : c < a
⊢ False
Module: Mathlib.Algebra.Ring.Invertible

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

Tactic:
add_comm _ 1,

Goal state after:
R : Type u_1
inst✝³ : Ring R
a b : R
inst✝² : Invertible a
inst✝¹ : Invertible b
inst✝ : Invertible (a + b)
⊢ 1 = 1 + (1 + ⅟b * a) + ⅟a * b ↔ 1 = 1 + 1 + ⅟b * a + ⅟a * b
Module: Mathlib.Algebra.Group.Int.Units

Goal state before:
pp: u v : ℤ
h : u * v = 1
⊢ u = 1 ∧ v = 1 ∨ u = -1 ∧ v = -1

Tactic:
have h' : v * u = 1 := mul_comm u v ▸ h
  obtain rfl | rfl := eq_one_or_neg_one_of_mul_eq_one h <;>
      obtain rfl | rfl := eq_one_or_neg_one_of_mul_eq_one h' <;> tauto

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

Goal state before:
pp: case inl.inl
α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedRing α
a b : α
ha : a ≤ 0
hb : b ≤ 0
⊢ a * b = |a| * |b| ∨ a * b = -(|a| * |b|)

Tactic:
simp only [abs_of_nonpos, abs_of_nonneg, true_or, or_true, neg_mul, mul_neg, neg_neg, *]

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

Goal state before:
pp: case inl.inr
α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedRing α
a b : α
ha : a ≤ 0
hb : 0 ≤ b
⊢ a * b = |a| * |b| ∨ a * b = -(|a| * |b|)

Tactic:
simp only [abs_of_nonpos, abs_of_nonneg, true_or, or_true, neg_mul, mul_neg, neg_neg, *]

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

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedRing α
a b : α
ha : 0 ≤ a
hb : b ≤ 0
⊢ a * b = |a| * |b| ∨ a * b = -(|a| * |b|)

Tactic:
simp only [abs_of_nonpos, abs_of_nonneg, true_or, or_true, neg_mul, mul_neg, neg_neg, *]

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

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedRing α
a b : α
ha : 0 ≤ a
hb : 0 ≤ b
⊢ a * b = |a| * |b| ∨ a * b = -(|a| * |b|)

Tactic:
simp only [abs_of_nonpos, abs_of_nonneg, true_or, or_true, neg_mul, mul_neg, neg_neg, *]

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : Preorder α
s t : Set α
h : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (s ∪ t)
⊢ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s ∧ IsCofinalFor t s ∨ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) t ∧ IsCofinalFor s t

pp: case refine_2
α : Type u_1
inst✝ : Preorder α
s t : Set α
⊢ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s ∧ IsCofinalFor t s ∨ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) t ∧ IsCofinalFor s t →
    DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (s ∪ t)

Tactic:
· rcases isCofinalFor_or_isCofinalFor_of_directedOn_union h with hts | hst
    · exact .inl ⟨DirectedOn.of_isCofinalFor h subset_union_left hts.union_right, hts⟩
    · exact .inr ⟨DirectedOn.of_isCofinalFor h subset_union_right hst.union_left, hst⟩

Goal state after:
case refine_2
α : Type u_1
inst✝ : Preorder α
s t : Set α
⊢ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s ∧ IsCofinalFor t s ∨ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) t ∧ IsCofinalFor s t →
    DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (s ∪ t)
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: case neg.refine_1
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : a ∈ s
hb : ¬b ∈ s
⊢ s ⊆ Ico a b

Tactic:
rw [← Icc_sdiff_right]
      exact subset_sdiff_singleton hc hb

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : Set α
⊢ BddBelow s ∧ BddAbove s ↔ ∃ a b, s ⊆ Icc a b

Tactic:
simp [Ici_inter_Iic.symm, subset_inter_iff, bddBelow_iff_subset_Ici,
    bddAbove_iff_subset_Iic, exists_and_left, exists_and_right]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
s : Set α
a : α
inst✝ : NoBotOrder α
hs : IsLUB s a
h : s = ∅
x✝ : α
⊢ x✝ ∈ upperBounds ∅

Tactic:
upperBounds_empty

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
s : Set α
a : α
inst✝ : NoBotOrder α
hs : IsLUB s a
h : s = ∅
x✝ : α
⊢ x✝ ∈ univ
Module: Mathlib.Order.Bounds.Basic

Goal state before:
pp: γ : Type u_3
inst✝ : LinearOrder γ
a b : γ
s : Set γ
hs : IsGreatest s b
⊢ IsGreatest ({a} ∪ s) (max a b)

Tactic:
exact isGreatest_singleton.union hs

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

Goal state before:
pp: α : Type u_2
inst✝² : Semifield α
inst✝¹ : PartialOrder α
inst✝ : PosMulReflectLT α
a b : α
ha : 0 < a
hb : 0 < b
⊢ a < 1 / b ↔ b < 1 / a

Tactic:
simpa using lt_inv_comm₀ ha hb

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

Goal state before:
pp: case mp
α : Type u
h : Injective length
x y : α
⊢ x = y

Tactic:
suffices [x] = [y] by simpa using this

Goal state after:
case mp
α : Type u
h : Injective length
x y : α
⊢ [x] = [y]
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
n : ℕ
h : n ≠ 0
l : List α
⊢ (replicate n l.reverse).flatten.head? = l.reverse.head?

Tactic:
head?_flatten_replicate h

Goal state after:
α : Type u
n : ℕ
h : n ≠ 0
l : List α
⊢ l.reverse.head? = l.reverse.head?
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
β : Type v
f : α → β
h : Injective (map f)
x y : α
hxy : f x = f y
⊢ x = y

Tactic:
suffices [x] = [y] by simpa using this

Goal state after:
α : Type u
β : Type v
f : α → β
h : Injective (map f)
x y : α
hxy : f x = f y
⊢ [x] = [y]
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
β : Type v
f g : α → β → β
b : β
l : List α
H : ∀ (a : α), a ∈ l → ∀ (b : β), f a b = g a b
⊢ foldr f b l = foldr g b l

Tactic:
by
  induction l with | nil => rfl | cons hd tl ih => ?_
  simp only [mem_cons, or_imp, forall_and, forall_eq] at H
  simp only [foldr, ih H.2, H.1]

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

Goal state before:
pp: case inr
p q : ℚ
hp : 0 ≤ p
hq : q ≤ 0
hpq : p * q ≤ 0
⊢ (p * q).toNNRat = p.toNNRat * q.toNNRat

Tactic:
toNNRat_eq_zero.2 hq,

Goal state after:
case inr
p q : ℚ
hp : 0 ≤ p
hq : q ≤ 0
hpq : p * q ≤ 0
⊢ (p * q).toNNRat = p.toNNRat * 0
Module: Mathlib.Data.Rat.Lemmas

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

Tactic:
apply Nat.dvd_antisymm
  · simpa using add_den_dvd q n
  · simpa using add_den_dvd (q + n) (-n)

Goal state after:
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]

Goal state after:
q₁ q₂ : ℚ
⊢ q₁.num * q₂.num =
    q₁.num * q₂.num / ↑((q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den)) *
      ↑((q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den))
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: case mpr
q : ℚ
nr : ℤ
hnr : q.num = nr * nr
dr : ℕ
hdr : q.den = dr * dr
⊢ q = ↑nr / ↑dr * (↑nr / ↑dr)

Tactic:
div_mul_div_comm,

Goal state after:
case mpr
q : ℚ
nr : ℤ
hnr : q.num = nr * nr
dr : ℕ
hdr : q.den = dr * dr
⊢ q = ↑nr * ↑nr / (↑dr * ↑dr)
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: α : Type u_3
inst✝ : DivisionRing α
n : ℕ
⊢ ↑↑n = ↑n

Tactic:
rw [← Int.cast_natCast, cast_intCast, Int.cast_natCast]

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

Goal state before:
pp: α : Type u_3
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
⊢ ↑(a /. b) = ↑a / ↑b

Tactic:
by
  have b0' : b ≠ 0 := by
    refine mt ?_ b0
    simp +contextual
  rcases e : a /. b with ⟨n, d, h, c⟩
  have d0 : (d : α) ≠ 0 := by
    intro d0
    have dd := den_dvd a b
    rcases show (d : ℤ) ∣ b by rwa [e] at dd with ⟨k, ke⟩
    have : (b : α) = (d : α) * (k : α) := by rw [ke, Int.cast_mul, Int.cast_natCast]
    rw [d0, zero_mul] at this
    contradiction
  rw [mk_eq_divInt] at e
  have := congr_arg ((↑) : ℤ → α)
    ((divInt_eq_divInt_iff b0' <| ne_of_gt <| Int.natCast_pos.2 h.bot_lt).1 e)
  rw [Int.cast_mul, Int.cast_mul, Int.cast_natCast] at this
  rw [eq_comm, cast_def, div_eq_mul_inv, eq_div_iff_mul_eq d0, mul_assoc, (d.commute_cast _).eq,
    ← mul_assoc, this, mul_assoc, mul_inv_cancel₀ b0, mul_one]

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

Goal state before:
pp: n d : ℕ
R : Type u_2
inst✝ : DivisionSemiring R
a : R
inv✝ : Invertible ↑d
e : a = ↑n * ⅟↑d
⊢ a = NNRat.rawCast n d + 0

Tactic:
simp [e, div_eq_mul_inv]

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

Goal state before:
pp: n : ℤ
d : ℕ
R : Type u_2
inst✝ : DivisionRing R
a : R
inv✝ : Invertible ↑d
e : a = ↑n * ⅟↑d
⊢ a = Rat.rawCast n d + 0

Tactic:
simp [e, div_eq_mul_inv]

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

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
f : ℕ → α
k : ℕ
⊢ ⨆ n, ⨅ i, ⨅ (_ : i ≥ n), f (i + k) = ⨆ n, ⨅ i, ⨅ (_ : i ≥ n), f i

Tactic:
by
  have hf : Monotone fun n => ⨅ i ≥ n, f i := fun n m h => biInf_mono fun i => h.trans
  rw [← Monotone.iSup_nat_add hf k]
  · simp_rw [iInf_ge_eq_iInf_nat_add, ← Nat.add_assoc]

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

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✝ : CompleteLattice α
s : Set (ULift α)
⊢ (sSup s).down = ⨆ a ∈ s, a.down

Tactic:
sSup_eq_iSup',

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
inst✝ : CompleteLattice α
s : Set (ULift α)
⊢ (⨆ a, ↑a).down = ⨆ a ∈ s, a.down
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : β → α
s t : Set β
⊢ ⨆ x, ⨆ (_ : x ∈ s ∨ x ∈ t), f x = (⨆ x ∈ s, f x) ⊔ ⨆ x ∈ t, f x

Tactic:
iSup_or,

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : β → α
s t : Set β
⊢ ⨆ x, (⨆ (_ : x ∈ s), f x) ⊔ ⨆ (_ : x ∈ t), f x = (⨆ x ∈ s, f x) ⊔ ⨆ x ∈ t, f x
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
ι : Sort u_5
P : ι → α → Prop
x✝ : α
⊢ x✝ ∈ ⋃ i, {x | P i x} ↔ x✝ ∈ {x | ∃ i, P i x}

Tactic:
exact mem_iUnion

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

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

Tactic:
ext x
  simp [@eq_comm _ x]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice β
S : Set (Set α)
f : α → β
⊢ ⨅ x ∈ ⋃₀ S, f x = ⨅ s ∈ S, ⨅ x ∈ s, f x

Tactic:
rw [sUnion_eq_iUnion, iInf_iUnion, ← iInf_subtype'']

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
minAx : Frame.MinimalAxioms β
f : α → β
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a
a : α
s : Set α
⊢ f (a ⊓ sSup s) ≤ f (sSup (min a '' s))

Tactic:
map_inf,

Goal state after:
α : Type u
β : Type v
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
minAx : Frame.MinimalAxioms β
f : α → β
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a
a : α
s : Set α
⊢ f a ⊓ f (sSup s) ≤ f (sSup (min a '' s))
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case inr
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s t : Set α
hs : BddAbove s
ht : BddAbove t
hne : s.Nonempty
⊢ sSup (s ∪ t) = max (sSup s) (sSup t)

Tactic:
exact (isLUB_csSup' hs |>.union <| isLUB_csSup' ht).csSup_eq hne.inl

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : One M
f : ι → M
⊢ mulSupport f = ∅ ↔ f = 1

Tactic:
rw [← subset_empty_iff, mulSupport_subset_iff', funext_iff]

Goal state after:
ι : Type u_1
M : Type u_3
inst✝ : One M
f : ι → M
⊢ (∀ (x : ι), ¬x ∈ ∅ → f x = 1) ↔ ∀ (x : ι), f x = 1 x
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: i n : ℕ
hi : 2 ≤ i
⊢ i + (n + 1)! < (i + n + 1)!

Tactic:
factorial_succ (i + _),

Goal state after:
i n : ℕ
hi : 2 ≤ i
⊢ i + (n + 1)! < (i + n + 1) * (i + n)!
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n k : ℕ
⊢ n.descFactorial k.succ = 0 ↔ n < k.succ

Tactic:
by
    rw [descFactorial_succ, mul_eq_zero, descFactorial_eq_zero_iff_lt, Nat.lt_succ_iff,
      Nat.sub_eq_zero_iff_le, Nat.lt_iff_le_and_ne, or_iff_left_iff_imp, and_imp]
    exact fun h _ => h

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

Goal state before:
pp: case neg.e_a
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
H : ⌊2 * fract x⌋ = 1
h : fract x ≤ 0
⊢ 2 * fract x < 1

Tactic:
grw [h]

Goal state after:
case neg.e_a
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
H : ⌊2 * fract x⌋ = 1
h : fract x ≤ 0
⊢ 2 * 0 < 1
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 b : R
h : ⌊a⌋ = ⌊b⌋
this : ∀ {a b : R}, ⌊a⌋ = ⌊b⌋ → b ≤ a → |a - b| < 1
h0 : ¬b ≤ a
⊢ |b - a| < 1

Tactic:
exact this h.symm (le_of_not_ge h0)

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

Goal state before:
pp: case inr.inr.inr.refine_1
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
hc₀ : 0 < c
hc₁ : c < 1
ha : 0 < a
hb₁ : 1 < b
ha₁ : 1 ≤ a
this : b⁻¹ < a⁻¹ * c
n : ℕ
hn₁ : b⁻¹ < c ^ n
hn₂ : c ^ n < a⁻¹
⊢ a < c ^ (-↑n)

pp: case inr.inr.inr.refine_2
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
hc₀ : 0 < c
hc₁ : c < 1
ha : 0 < a
hb₁ : 1 < b
ha₁ : 1 ≤ a
this : b⁻¹ < a⁻¹ * c
n : ℕ
hn₁ : b⁻¹ < c ^ n
hn₂ : c ^ n < a⁻¹
⊢ c ^ (-↑n) < b

Tactic:
· rwa [lt_inv_comm₀ (pow_pos hc₀ n) ha, ← zpow_natCast, ← zpow_neg] at hn₂

Goal state after:
case inr.inr.inr.refine_2
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
hc₀ : 0 < c
hc₁ : c < 1
ha : 0 < a
hb₁ : 1 < b
ha₁ : 1 ≤ a
this : b⁻¹ < a⁻¹ * c
n : ℕ
hn₁ : b⁻¹ < c ^ n
hn₂ : c ^ n < a⁻¹
⊢ c ^ (-↑n) < b
Module: Mathlib.Algebra.Group.Action.Units

Goal state before:
pp: G : Type u_1
H : Type u_2
M✝ : Type u_3
N : Type u_4
α : Type u_5
M : Type u_6
inst✝ : CommMonoid M
⊢ mulAction'.toSMul = instSMulOfMul

Tactic:
fail_if_success rfl -- there is an instance diamond here
  ext
  rfl

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

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
⊢ ∀ (a_1 : List α), p a → countP p (a ::ₘ Quot.mk (⇑(isSetoid α)) a_1) = countP p (Quot.mk (⇑(isSetoid α)) a_1) + 1

Tactic:
by simpa using fun _ => List.countP_cons_of_pos (p := (p ·))

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

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
p₁ p₂ p : P
h : p₁ /ₛ p = p₂ /ₛ p
⊢ p₁ = p₂

Tactic:
by
  rwa [← div_eq_one, sdiv_div_sdiv_cancel_right, sdiv_eq_one_iff_eq] at h

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

Goal state before:
pp: α : Type u_1
s s' : Multiset α
p p' : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred p'
l l' : List α
hp : ∀ (x : α), x ∈ Quot.mk (⇑(isSetoid α)) l → p x = p' x
hs : l ~ l'
⊢ countP p (Quot.mk (⇑(isSetoid α)) l) = countP p' (Quot.mk (⇑(isSetoid α)) l')

Tactic:
apply hs.countP_congr

Goal state after:
α : Type u_1
s s' : Multiset α
p p' : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred p'
l l' : List α
hp : ∀ (x : α), x ∈ Quot.mk (⇑(isSetoid α)) l → p x = p' x
hs : l ~ l'
⊢ ∀ (x : α), x ∈ l → decide (p x) = decide (p' x)
Module: Mathlib.Algebra.Torsor.Basic

Goal state before:
pp: G : Type u_3
P : Type u_4
inst✝ : AddGroup G
T : AddTorsor G P
x y : P
⊢ -(y -ᵥ (pointReflection x) y) = -(2 • (y -ᵥ x))

Tactic:
simp [← neg_nsmul]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ 0 < count a s ↔ a ∈ s

Tactic:
simp [count, countP_pos]

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

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Prop
inst✝² : IsTrans α r
inst✝¹ : Std.Symm r
x : α
inst✝ : DecidablePred (r x)
y : α
s : Multiset α
ih : ∀ {t : Multiset α}, Rel r s t → countP (r x) s = countP (r x) t
t : Multiset α
h : Rel r (y ::ₘ s) t
⊢ countP (r x) (y ::ₘ s) = countP (r x) t

Tactic:
obtain ⟨b, bs, hb1, hb2, rfl⟩ := rel_cons_left.mp h

Goal state after:
case cons
α : Type u_1
r : α → α → Prop
inst✝² : IsTrans α r
inst✝¹ : Std.Symm r
x : α
inst✝ : DecidablePred (r x)
y : α
s : Multiset α
ih : ∀ {t : Multiset α}, Rel r s t → countP (r x) s = countP (r x) t
b : α
bs : Multiset α
hb1 : r y b
hb2 : Rel r s bs
h : Rel r (y ::ₘ s) (b ::ₘ bs)
⊢ countP (r x) (y ::ₘ s) = countP (r x) (b ::ₘ bs)
Module: Mathlib.Data.Set.List

Goal state before:
pp: α : Type u_1
l : List α
d : α
⊢ ((fun o ↦ o.getD d) '' range fun x ↦ l[x]?) = insert d {x | x ∈ l}

Tactic:
simp only [Option.getD, range_list_getElem?, image_insert_eq, image_image, image_id']

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

Goal state before:
pp: α : Type u
l : List α
h : l.Nodup
x : α
⊢ l ≠ [x] ↔ l = [] ∨ ∃ y, y ∈ l ∧ y ≠ x

Tactic:
induction l with
  | nil => simp
  | cons hd tl hl =>
    specialize hl h.of_cons
    by_cases hx : tl = [x]
    · simpa [hx, and_comm, and_or_left] using h
    · rw [← Ne, hl] at hx
      rcases hx with (rfl | ⟨y, hy, hx⟩)
      · simp
      · suffices ∃ y ∈ hd :: tl, y ≠ x by simpa [ne_nil_of_mem hy]
        exact ⟨y, mem_cons_of_mem _ hy, hx⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ s - {a} = s.erase a

Tactic:
by
  ext
  simp only [count_sub, count_singleton]
  split <;> simp_all

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

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
x : α
t : Multiset α
ih : ∀ {s u : Multiset α}, Rel r s t → Rel r t u → Rel r s u
u : Multiset α
r2 : Rel r (x ::ₘ t) u
a : α
as : Multiset α
ha1 : r a x
ha2 : Rel r as t
r1 : Rel r (a ::ₘ as) (x ::ₘ t)
⊢ Rel r (a ::ₘ as) u

Tactic:
obtain ⟨b, bs, hb1, hb2, rfl⟩ := rel_cons_left.mp r2

Goal state after:
case cons
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
x : α
t : Multiset α
ih : ∀ {s u : Multiset α}, Rel r s t → Rel r t u → Rel r s u
a : α
as : Multiset α
ha1 : r a x
ha2 : Rel r as t
r1 : Rel r (a ::ₘ as) (x ::ₘ t)
b : α
bs : Multiset α
hb1 : r x b
hb2 : Rel r t bs
r2 : Rel r (x ::ₘ t) (b ::ₘ bs)
⊢ Rel r (a ::ₘ as) (b ::ₘ bs)
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: α : Type u
l : List α
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
h : l.Nodup
h' : ¬a ∈ l
⊢ (List.insert a l).Nodup

Tactic:
rw [insert_of_not_mem h', nodup_cons]; constructor <;> assumption

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
l' : List α
⊢ l.dedup = a :: l' ↔ a ∈ l ∧ ¬a ∈ l' ∧ l.dedup.tail = l'

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩

Goal state after:
case refine_1
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
l' : List α
h : l.dedup = a :: l'
⊢ a ∈ l ∧ ¬a ∈ l' ∧ l.dedup.tail = l'

case refine_2
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
l' : List α
h : a ∈ l ∧ ¬a ∈ l' ∧ l.dedup.tail = l'
⊢ l.dedup = a :: l'