mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: case H0
x y n✝ : ℕ
⊢ ∀ {s t s' t' : ℤ}, x.P y (0, s, t) → x.P y (n✝, s', t') → x.P y (xgcdAux 0 s t n✝ s' t')

Tactic:
| H0 =>

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

Goal state before:
pp: m n k : ℕ
⊢ m - n ≤ k ↔ m ≤ k + n

Tactic:
induction n generalizing k with
  | zero => simp
  | succ n ih => simp only [sub_succ, pred_le_iff, ih, succ_add, add_succ]

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

Goal state before:
pp: k n : ℕ
hkn : n.Coprime k
hk : 1 < k
⊢ ∃ m, m < k ∧ n * m % k = 1

Tactic:
simpa [hkn, hk] using exists_mul_mod_eq_gcd (k := k) (n := n)

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
m n : ℕ
hm : a ^ m = 1
hn : a ^ n = 1
⊢ a ^ m.gcd n = 1

Tactic:
obtain _ | m := m

Goal state after:
case zero
M : Type u_1
inst✝ : Monoid M
a : M
n : ℕ
hn : a ^ n = 1
hm : a ^ 0 = 1
⊢ a ^ Nat.gcd 0 n = 1

case succ
M : Type u_1
inst✝ : Monoid M
a : M
n : ℕ
hn : a ^ n = 1
m : ℕ
hm : a ^ (m + 1) = 1
⊢ a ^ (m + 1).gcd n = 1
Module: Mathlib.Algebra.GroupWithZero.Regular

Goal state before:
pp: R : Type u_1
inst✝ : MulZeroClass R
a b : R
hb : IsRightRegular b
⊢ a * b = 0 ↔ a = 0

Tactic:
conv_lhs => rw [← zero_mul b]

Goal state after:
R : Type u_1
inst✝ : MulZeroClass R
a b : R
hb : IsRightRegular b
⊢ a * b = 0 * b ↔ a = 0
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a : α
⊢ 0 < -a ↔ a < 0 ∨ a = ⊤

Tactic:
by
  simpa using sub_pos (a := 0) (b := a)

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
⊢ ¬a ≤ b ↔ b < a

Tactic:
not_le

Goal state after:
α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
⊢ b < a ↔ b < a
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
β : Type v
inst✝ : AddMonoid α
n : ℕ
a : WithTop α
⊢ (match a, n + 1 with
    | Option.some a, n => ↑(n • a)
    | none, 0 => 0
    | none, _n.succ => ⊤) =
    (match a, n with
      | Option.some a, n => ↑(n • a)
      | none, 0 => 0
      | none, _n.succ => ⊤) +
      a

Tactic:
cases a <;> cases n

Goal state after:
case top.zero
α : Type u
β : Type v
inst✝ : AddMonoid α
⊢ (match ⊤, 0 + 1 with
    | Option.some a, n => ↑(n • a)
    | none, 0 => 0
    | none, _n.succ => ⊤) =
    (match ⊤, 0 with
      | Option.some a, n => ↑(n • a)
      | none, 0 => 0
      | none, _n.succ => ⊤) +
      ⊤

case top.succ
α : Type u
β : Type v
inst✝ : AddMonoid α
n✝ : ℕ
⊢ (match ⊤, n✝ + 1 + 1 with
    | Option.some a, n => ↑(n • a)
    | none, 0 => 0
    | none, _n.succ => ⊤) =
    (match ⊤, n✝ + 1 with
      | Option.some a, n => ↑(n • a)
      | none, 0 => 0
      | none, _n.succ => ⊤) +
      ⊤

case coe.zero
α : Type u
β : Type v
inst✝ : AddMonoid α
a✝ : α
⊢ (match ↑a✝, 0 + 1 with
    | Option.some a, n => ↑(n • a)
    | none, 0 => 0
    | none, _n.succ => ⊤) =
    (match ↑a✝, 0 with
      | Option.some a, n => ↑(n • a)
      | none, 0 => 0
      | none, _n.succ => ⊤) +
      ↑a✝

case coe.succ
α : Type u
β : Type v
inst✝ : AddMonoid α
a✝ : α
n✝ : ℕ
⊢ (match ↑a✝, n✝ + 1 + 1 with
    | Option.some a, n => ↑(n • a)
    | none, 0 => 0
    | none, _n.succ => ⊤) =
    (match ↑a✝, n✝ + 1 with
      | Option.some a, n => ↑(n • a)
      | none, 0 => 0
      | none, _n.succ => ⊤) +
      ↑a✝
Module: Mathlib.Algebra.Order.Sub.Basic

Goal state before:
pp: case neg
α : Type u_1
inst✝³ : AddCommMonoid α
inst✝² : LinearOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : AddRightReflectLE α
a b c : α
h : ¬b ≤ a
⊢ 0 ≤ c ↔ a ≤ c + b

Tactic:
not_le

Goal state after:
case neg
α : Type u_1
inst✝³ : AddCommMonoid α
inst✝² : LinearOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : AddRightReflectLE α
a b c : α
h : a < b
⊢ 0 ≤ c ↔ a ≤ c + b
Module: Mathlib.Algebra.Order.Ring.Cast

Goal state before:
pp: R : Type u_1
inst✝⁴ : AddCommGroupWithOne R
inst✝³ : PartialOrder R
inst✝² : AddLeftMono R
inst✝¹ : ZeroLEOneClass R
inst✝ : NeZero 1
n : ℤ
⊢ ↑n ≤ 0 ↔ n ≤ 0

Tactic:
by rw [← cast_zero, cast_le]

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

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

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
⊢ ⌊a * ↑n⌋₊ / n = ⌊a⌋₊

Tactic:
· rw [floor_of_nonpos, floor_of_nonpos ha]
    · simp
    apply mul_nonpos_of_nonpos_of_nonneg ha n.cast_nonneg

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
⊢ ⌊a * ↑n⌋₊ / n = ⌊a⌋₊
Module: Mathlib.Algebra.Group.Invertible.Defs

Goal state before:
pp: α : Type u
inst✝² : Monoid α
a b : α
inst✝¹ : Invertible a
inst✝ : Invertible b
h : a = b
⊢ a * ⅟b = 1

Tactic:
rw [h, mul_invOf_self]

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

Goal state before:
pp: case inr
G₀ : Type u_1
inst✝² : GroupWithZero G₀
inst✝¹ : SemilatticeInf G₀
inst✝ : MulPosReflectLT G₀
c : G₀
hc✝ : 0 ≤ c
a b : G₀
hc : 0 < c
⊢ (a ⊓ b) * c = a * c ⊓ b * c

Tactic:
exact (OrderIso.mulRight₀ c hc).map_inf a b

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

Goal state before:
pp: K : Type u_1
inst✝ : DivisionSemiring K
a b c : K
⊢ (a + b) / c = a / c + b / c

Tactic:
simp_rw [div_eq_mul_inv, add_mul]

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

Goal state before:
pp: case inr
K : Type u_1
inst✝ : DivisionRing K
a : K
ha : a ≠ 0
⊢ a⁻¹ = a ↔ a = -1 ∨ a = 0 ∨ a = 1

Tactic:
← mul_eq_one_iff_inv_eq₀ ha,

Goal state after:
case inr
K : Type u_1
inst✝ : DivisionRing K
a : K
ha : a ≠ 0
⊢ a * a = 1 ↔ a = -1 ∨ a = 0 ∨ a = 1
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedRing α
x : α
⊢ |x ^ 2| = x ^ 2

Tactic:
simpa only [sq] using abs_mul_self x

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

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
⊢ 1 < a ^ 2 ↔ 1 < |a|

Tactic:
simpa only [one_pow, abs_one] using sq_lt_sq (a := 1) (b := a)

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

Goal state before:
pp: α : Type u_3
β : α → Type u_4
p : α → Prop
inst✝ : DecidablePred p
s : (i : α) → Set (β i)
f : (i : { x // p x }) → β ↑i
g : (i : { x // ¬p x }) → β ↑i
i : α
⊢ (piEquivPiSubtypeProd p β).symm (f, g) i ∈ s i ↔ (∀ (b : p i), f ⟨i, b⟩ ∈ s i) ∧ ∀ (b : ¬p i), g ⟨i, b⟩ ∈ s i

Tactic:
by_cases hi : p i

Goal state after:
case pos
α : Type u_3
β : α → Type u_4
p : α → Prop
inst✝ : DecidablePred p
s : (i : α) → Set (β i)
f : (i : { x // p x }) → β ↑i
g : (i : { x // ¬p x }) → β ↑i
i : α
hi : p i
⊢ (piEquivPiSubtypeProd p β).symm (f, g) i ∈ s i ↔ (∀ (b : p i), f ⟨i, b⟩ ∈ s i) ∧ ∀ (b : ¬p i), g ⟨i, b⟩ ∈ s i

case neg
α : Type u_3
β : α → Type u_4
p : α → Prop
inst✝ : DecidablePred p
s : (i : α) → Set (β i)
f : (i : { x // p x }) → β ↑i
g : (i : { x // ¬p x }) → β ↑i
i : α
hi : ¬p i
⊢ (piEquivPiSubtypeProd p β).symm (f, g) i ∈ s i ↔ (∀ (b : p i), f ⟨i, b⟩ ∈ s i) ∧ ∀ (b : ¬p i), g ⟨i, b⟩ ∈ s i
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a ≤ b
⊢ Icc a b \ (Icc a b \ {b}) = {b}

Tactic:
sdiff_sdiff_cancel_left (singleton_subset_iff.2 <| right_mem_Icc.2 h)

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a ≤ b
⊢ {b} = {b}
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : DenselyOrdered α
x y : α
x✝ : ↑(Ioi x)
a : α
ha : a ∈ Ioi x
b : α
hb₁ : x < b
hb₂ : b < a
⊢ ∃ b, b < ⟨a, ha⟩

Tactic:
exact ⟨⟨b, hb₁⟩, hb₂⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Set α
a b : α
h : IsLUB s a
⊢ (∃ x, ∃ (_ : x ∈ s), b < x) ↔ ∃ c ∈ s, b < c

Tactic:
exists_prop

Goal state after:
Module: Mathlib.Tactic.Abel

Goal state before:
pp: α : Type u_1
inst✝ : AddCommGroup α
x : α
⊢ x = termg 1 x 0

Tactic:
simp [termg]

Goal state after:
Module: Mathlib.Tactic.Abel

Goal state before:
pp: α : Type u_1
inst✝ : AddCommMonoid α
l r tl tr t : α
prl : l = tl
prr : r = tr
prt : tl + tr = t
⊢ tl + r = t

Tactic:
prr,

Goal state after:
α : Type u_1
inst✝ : AddCommMonoid α
l r tl tr t : α
prl : l = tl
prr : r = tr
prt : tl + tr = t
⊢ tl + tr = t
Module: Mathlib.Tactic.Abel

Goal state before:
pp: α : Type u_1
inst✝ : AddCommGroup α
l r tl tr t : α
prl : l = tl
prr : r = tr
prt : tl + tr = t
⊢ tl + r = t

Tactic:
prr,

Goal state after:
α : Type u_1
inst✝ : AddCommGroup α
l r tl tr t : α
prl : l = tl
prr : r = tr
prt : tl + tr = t
⊢ tl + tr = t
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: case hc
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a b c d e : α
m n : ℤ
inst✝ : IsStrictOrderedRing α
a₁ a₂ : α
h : a₁ < a₂
⊢ 0 < 2

Tactic:
exact zero_lt_two

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

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
f : α → α → α
a b : α
na nb nc da db dc k : ℕ
⊢ f = HMul.hMul →
    IsNNRat a na da → IsNNRat b nb db → na.mul nb = k.mul nc → da.mul db = k.mul dc → IsNNRat (f a b) nc dc

Tactic:
rintro rfl ⟨_, rfl⟩ ⟨_, rfl⟩ (h₁ : na * nb = k * nc) (h₂ : da * db = k * dc)
  have : Invertible (↑(da * db) : α) := by simpa using invertibleMul (da:α) db
  have := invertibleOfMul' (α := α) h₂
  refine ⟨this, ?_⟩
  have H := (Nat.cast_commute (α := α) da db).invOf_left.invOf_right.right_comm
  have h₁ := congr_arg (Nat.cast (R := α)) h₁
  simp only [Nat.cast_mul] at h₁
  simp only [← mul_assoc, (Nat.cast_commute (α := α) da nb).invOf_left.right_comm, h₁]
  have h₂ := congr_arg (↑nc * ↑· * (⅟↑da * ⅟↑db * ⅟↑dc : α)) h₂
  simp only [Nat.cast_mul, ← mul_assoc] at h₂; rw [H] at h₂
  simp only [mul_invOf_cancel_right'] at h₂; rw [h₂, Nat.cast_commute]
  simp only [mul_invOf_cancel_right',
    (Nat.cast_commute (α := α) da dc).invOf_left.invOf_right.right_comm,
    (Nat.cast_commute (α := α) db dc).invOf_left.invOf_right.right_comm]

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

Goal state before:
pp: α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : α
hc : a * b < c
⊢ ∃ b' > b, a * b' < c

Tactic:
simp_rw [mul_comm a] at hc ⊢

Goal state after:
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : α
hc : b * a < c
⊢ ∃ b' > b, b' * a < c
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
a b : α
m n : ℕ
h : a ≠ b
⊢ l ~ replicate m a ++ replicate n b ↔ count a l = m ∧ count b l = n ∧ l ⊆ [a, b]

Tactic:
perm_iff_count,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
a b : α
m n : ℕ
h : a ≠ b
⊢ (∀ (a_1 : α), count a_1 l = count a_1 (replicate m a ++ replicate n b)) ↔ count a l = m ∧ count b l = n ∧ l ⊆ [a, b]
Module: Mathlib.Data.Rat.Defs

Goal state before:
pp: q r : ℚ
⊢ normalize (q.num * r.num) (q.den * r.den) ⋯ = mkRat (q.num * r.num) (q.den * r.den)

Tactic:
normalize_eq_mkRat

Goal state after:
q r : ℚ
⊢ mkRat (q.num * r.num) (q.den * r.den) = mkRat (q.num * r.num) (q.den * r.den)
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: case cons
j : ℕ
L : List ℕ
IH : (∀ (i : ℕ), i ∈ L → 1 ≤ i) → L.length ≤ L.sum
h : ∀ (i : ℕ), i ∈ j :: L → 1 ≤ i
⊢ 1 + L.length ≤ j + L.sum

Tactic:
exact Nat.add_le_add (h _ mem_cons_self) (IH fun i hi => h i (mem_cons.2 (Or.inr hi)))

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a x y : G
⊢ SemiconjBy a x⁻¹ y⁻¹ ↔ SemiconjBy a x y

Tactic:
rw [← inv_symm_left_iff, inv_inv_symm_iff]

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

Goal state before:
pp: p q : ℚ≥0
hn : p.num = q.num
hd : p.den = q.den
⊢ (↑p).num = (↑q).num

Tactic:
simpa [num_coe]

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

Goal state before:
pp: case pos
n : ℤ
hn : n = 0
⊢ ↑(n / n) = ↑n / ↑n

Tactic:
subst hn
    simp

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

Goal state before:
pp: F : Type u_1
α : Type u_3
β : Type u_4
inst✝³ : FunLike F α β
inst✝² : DivisionSemiring α
inst✝¹ : DivisionSemiring β
inst✝ : RingHomClass F α β
f : F
q : ℚ≥0
⊢ f ↑q.num / f ↑q.den = ↑q.num / ↑q.den

Tactic:
map_natCast

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

Goal state before:
pp: F : Type u_1
α : Type u_3
β : Type u_4
inst✝³ : FunLike F α β
inst✝² : DivisionSemiring α
inst✝¹ : DivisionSemiring β
inst✝ : RingHomClass F α β
f : F
q : ℚ≥0
⊢ f ↑q = ↑q

Tactic:
simp_rw [NNRat.cast_def, map_div₀, map_natCast]

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

Goal state before:
pp: case nil
α : Type u
⊢ map id nil = nil

Tactic:
map

Goal state after:
case nil
α : Type u
⊢ nil = nil
Module: Mathlib.Data.Tree.Basic

Goal state before:
pp: case nil
α : Type u
β : Type u_1
γ : Type u_2
f : α → β
g : β → γ
⊢ nil = map g nil

Tactic:
map

Goal state after:
case nil
α : Type u
β : Type u_1
γ : Type u_2
f : α → β
g : β → γ
⊢ nil = nil
Module: Mathlib.Data.Nat.Set

Goal state before:
pp: case e'_4.succ
α : Type u_2
x : α
f : ℕ → α → α
n : ℕ
ihn : rec (f 0 x) (f ∘ succ) n = f n (rec x f n)
⊢ rec (f 0 x) (f ∘ succ) (n + 1) = f (n + 1) (rec x f (n + 1))

Tactic:
dsimp at ihn ⊢

Goal state after:
case e'_4.succ
α : Type u_2
x : α
f : ℕ → α → α
n : ℕ
ihn : rec (f 0 x) (f ∘ succ) n = f n (rec x f n)
⊢ f (n + 1) (rec (f 0 x) (f ∘ succ) n) = f (n + 1) (f n (rec x f n))
Module: Mathlib.Order.CompleteLattice.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
f : Bool → α
⊢ sSup {f false, f true} = f true ⊔ f false

Tactic:
sSup_pair,

Goal state after:
α : Type u_1
inst✝ : CompleteLattice α
f : Bool → α
⊢ f false ⊔ f true = f true ⊔ f false
Module: Mathlib.Order.CompleteLattice.Lemmas

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

Tactic:
apply le_antisymm

Goal state after:
case a
α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
n : ℕ
⊢ ⨆ i, ⨆ (_ : i ≥ n), u i ≤ ⨆ i, u (i + n)

case a
α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
n : ℕ
⊢ ⨆ i, u (i + n) ≤ ⨆ i, ⨆ (_ : i ≥ n), u i
Module: Mathlib.Order.CompleteLattice.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
f : ℕ → α
⊢ ⨅ i, ⨅ (_ : i > 0), f i = ⨅ i, f (i + 1)

Tactic:
by
  rw [← iInf_range, Nat.range_succ]
  simp

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

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

Tactic:
apply le_antisymm

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

case a
α : Type u_1
inst✝² : CompleteLattice α
ι : Type u_8
inst✝¹ : LT ι
inst✝ : NoMaxOrder ι
f : ι → α
⊢ ⨆ i, f i ≤ ⨆ i, ⨆ j, ⨆ (_ : j < i), f j
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CompleteLattice α
ι : Type u_8
inst✝ : Preorder ι
f : ι → α
⊢ ⨆ i, ⨆ j, ⨆ (_ : j ≤ i), f j = ⨆ i, f i

Tactic:
apply le_antisymm

Goal state after:
case a
α : Type u_1
inst✝¹ : CompleteLattice α
ι : Type u_8
inst✝ : Preorder ι
f : ι → α
⊢ ⨆ i, ⨆ j, ⨆ (_ : j ≤ i), f j ≤ ⨆ i, f i

case a
α : Type u_1
inst✝¹ : CompleteLattice α
ι : Type u_8
inst✝ : Preorder ι
f : ι → α
⊢ ⨆ i, f i ≤ ⨆ i, ⨆ j, ⨆ (_ : j ≤ i), f j
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
inst✝² : CompleteLattice α
ι : Type u_8
inst✝¹ : LT ι
inst✝ : NoMinOrder ι
f : ι → α
⊢ ⨆ i, ⨆ j, ⨆ (_ : j > i), f j = ⨆ i, f i

Tactic:
apply le_antisymm

Goal state after:
case a
α : Type u_1
inst✝² : CompleteLattice α
ι : Type u_8
inst✝¹ : LT ι
inst✝ : NoMinOrder ι
f : ι → α
⊢ ⨆ i, ⨆ j, ⨆ (_ : j > i), f j ≤ ⨆ i, f i

case a
α : Type u_1
inst✝² : CompleteLattice α
ι : Type u_8
inst✝¹ : LT ι
inst✝ : NoMinOrder ι
f : ι → α
⊢ ⨆ i, f i ≤ ⨆ i, ⨆ j, ⨆ (_ : j > i), f j
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CompleteLattice α
ι : Type u_8
inst✝ : Preorder ι
f : ι → α
⊢ ⨆ i, ⨆ j, ⨆ (_ : j ≥ i), f j = ⨆ i, f i

Tactic:
apply le_antisymm

Goal state after:
case a
α : Type u_1
inst✝¹ : CompleteLattice α
ι : Type u_8
inst✝ : Preorder ι
f : ι → α
⊢ ⨆ i, ⨆ j, ⨆ (_ : j ≥ i), f j ≤ ⨆ i, f i

case a
α : Type u_1
inst✝¹ : CompleteLattice α
ι : Type u_8
inst✝ : Preorder ι
f : ι → α
⊢ ⨆ i, f i ≤ ⨆ i, ⨆ j, ⨆ (_ : j ≥ i), f j
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: β : Type u_2
ι : Sort u_5
s : Set β
t : ι → Set β
⊢ (⋃ i, t i) \ s = ⋃ i, t i \ s

Tactic:
simp only [sdiff_eq, iUnion_inter]

Goal state after:
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
hrl : rhs < lhs
⊢ ∀ (x : α✝), x ≤ rhs ∨ lhs ≤ x

Tactic:
simpa only [not_exists, not_and_or, not_or, not_lt] using h

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
inst✝ : Frame α
ι : Type u_1
f : ι → α
h : Pairwise (Disjoint on f)
s t : Set ι
x✝¹ : ι × ι
i j : ι
x✝ : (i, j) ∈ s ×ˢ t
his : (i, j).1 ∈ s
hjs : (i, j).2 ∈ t
⊢ f (i, j).1 ⊓ f (i, j).2 ≤ ⨆ i ∈ s ∩ t, f i

Tactic:
by_cases hij : i = j

Goal state after:
case pos
α : Type u
inst✝ : Frame α
ι : Type u_1
f : ι → α
h : Pairwise (Disjoint on f)
s t : Set ι
x✝¹ : ι × ι
i j : ι
x✝ : (i, j) ∈ s ×ˢ t
his : (i, j).1 ∈ s
hjs : (i, j).2 ∈ t
hij : i = j
⊢ f (i, j).1 ⊓ f (i, j).2 ≤ ⨆ i ∈ s ∩ t, f i

case neg
α : Type u
inst✝ : Frame α
ι : Type u_1
f : ι → α
h : Pairwise (Disjoint on f)
s t : Set ι
x✝¹ : ι × ι
i j : ι
x✝ : (i, j) ∈ s ×ˢ t
his : (i, j).1 ∈ s
hjs : (i, j).2 ∈ t
hij : ¬i = j
⊢ f (i, j).1 ⊓ f (i, j).2 ≤ ⨆ i ∈ s ∩ t, f i
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
ι : Sort w
κ : ι → Sort w'
inst✝ : Frame α
a : α
f : (i : ι) → κ i → α
⊢ Disjoint (⨆ i, ⨆ j, f i j) a ↔ ∀ (i : ι) (j : κ i), Disjoint (f i j) a

Tactic:
iSup_disjoint_iff

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

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : ¬BddAbove s
⊢ sSup s = sSup univ

Tactic:
rw [csSup_of_not_bddAbove hs, csSup_of_not_bddAbove (s := univ)]
  contrapose hs
  exact hs.mono (subset_univ _)

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

Goal state before:
pp: case pos
α : 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 s = sSup t

Tactic:
apply le_antisymm

Goal state after:
case pos.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 s ≤ sSup t

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
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case mpr
α : Type u_1
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : WellFoundedLT α
hs : s.Nonempty
n : α
this : OrderBot α
hn : n ∈ s
hle : ∀ a ∈ s, n ≤ a
⊢ sInf s = n

Tactic:
exact le_antisymm (csInf_le (OrderBot.bddBelow s) hn) (le_csInf hs hle)

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

Goal state before:
pp: case pos
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : BddAbove ((fun a ↦ ↑a) ⁻¹' s)
⊢ ↑(sSup ((fun a ↦ ↑a) ⁻¹' s)) ∈ upperBounds s

Tactic:
rintro (⟨⟩ | a) ha
      · contradiction
      apply coe_le_coe.2
      exact le_csSup h₂ ha

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

Goal state before:
pp: case inl.inl
α : Type u_1
inst✝ : LinearOrder α
a b c : α
left✝¹ : b < a
right✝¹ : a ≤ c
left✝ : a < b
right✝ : b ≤ c
⊢ a = b

Tactic:
apply le_antisymm

Goal state after:
case inl.inl.a
α : Type u_1
inst✝ : LinearOrder α
a b c : α
left✝¹ : b < a
right✝¹ : a ≤ c
left✝ : a < b
right✝ : b ≤ c
⊢ a ≤ b

case a
α : Type u_1
inst✝ : LinearOrder α
a b c : α
left✝¹ : b < a
right✝¹ : a ≤ c
left✝ : a < b
right✝ : b ≤ c
⊢ b ≤ a
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: case inl.inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
left✝¹ : b < a
right✝¹ : a ≤ c
left✝ : c < b
right✝ : b ≤ a
⊢ a = b

Tactic:
apply le_antisymm

Goal state after:
case inl.inr.a
α : Type u_1
inst✝ : LinearOrder α
a b c : α
left✝¹ : b < a
right✝¹ : a ≤ c
left✝ : c < b
right✝ : b ≤ a
⊢ a ≤ b

case a
α : Type u_1
inst✝ : LinearOrder α
a b c : α
left✝¹ : b < a
right✝¹ : a ≤ c
left✝ : c < b
right✝ : b ≤ a
⊢ b ≤ a
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝ : LinearOrder α
a b c : α
left✝¹ : c < a
right✝¹ : a ≤ b
left✝ : a < b
right✝ : b ≤ c
⊢ a = b

Tactic:
apply le_antisymm

Goal state after:
case inr.inl.a
α : Type u_1
inst✝ : LinearOrder α
a b c : α
left✝¹ : c < a
right✝¹ : a ≤ b
left✝ : a < b
right✝ : b ≤ c
⊢ a ≤ b

case a
α : Type u_1
inst✝ : LinearOrder α
a b c : α
left✝¹ : c < a
right✝¹ : a ≤ b
left✝ : a < b
right✝ : b ≤ c
⊢ b ≤ a
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
left✝¹ : c < a
right✝¹ : a ≤ b
left✝ : c < b
right✝ : b ≤ a
⊢ a = b

Tactic:
apply le_antisymm

Goal state after:
case inr.inr.a
α : Type u_1
inst✝ : LinearOrder α
a b c : α
left✝¹ : c < a
right✝¹ : a ≤ b
left✝ : c < b
right✝ : b ≤ a
⊢ a ≤ b

case a
α : Type u_1
inst✝ : LinearOrder α
a b c : α
left✝¹ : c < a
right✝¹ : a ≤ b
left✝ : c < b
right✝ : b ≤ a
⊢ b ≤ a
Module: Mathlib.Order.Interval.Set.OrdConnected

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

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

Goal state after:
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: ι : Sort u_1
α : Type u_2
s : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : Inhabited ↑s
h_Sup : ∀ {t : Set ↑s}, t.Nonempty → BddAbove t → sSup (Subtype.val '' t) ∈ s
h_Inf : ∀ {t : Set ↑s}, t.Nonempty → BddBelow t → sInf (Subtype.val '' t) ∈ s
t : Set ↑s
ht : t.Nonempty
h_bdd : BddBelow t
⊢ IsGLB ((fun {x} ↦ ↑x) '' t) ↑(sInf t)

Tactic:
rw [← subset_sInf_of_within s ht h_bdd (h_Inf ht h_bdd)]
      exact isGLB_csInf (ht.image _) ((Subtype.mono_coe _).map_bddBelow h_bdd)

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Group α
a : α
ha : ¬a ≤ 1
⊢ a⁺ᵐ = a

Tactic:
not_le

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Group α
a : α
ha : 1 < a
⊢ a⁺ᵐ = a
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n k : ℕ
⊢ (n - k) * (n - k + 1).ascFactorial k = (n - k).ascFactorial (k + 1)

Tactic:
succ_ascFactorial,

Goal state after:
n k : ℕ
⊢ (n - k + k) * (n - k).ascFactorial k = (n - k).ascFactorial (k + 1)