mathlib-initiative/mathlib-tactics huggingface dataset:
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

Tactic:
rw [← zero_mul b]

Goal state after:
R : Type u_1
inst✝ : MulZeroClass R
a b : R
hb : IsRightRegular b
| a * b = 0 * b
Module: Mathlib.Algebra.Order.Monoid.WithTop

Goal state before:
pp: case coe.coe
α : Type u
inst✝² : AddCommMagma α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedAdd α
a✝¹ : α
hx : ↑a✝¹ ≠ ⊥
a✝ : α
⊢ a✝ ≤ a✝¹ + a✝

Tactic:
exact le_add_self

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

Goal state before:
pp: case pos
α : Type u_1
inst✝³ : AddCommMonoid α
inst✝² : LinearOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : AddRightReflectLE α
a b c : α
h : b ≤ a
⊢ ⋯.choose ≤ c ↔ a ≤ c + b

Tactic:
have := (exists_add_of_le h).choose_spec
      rw [this] at h
      conv_rhs => rw [this, add_comm]
      rw [add_le_add_iff_right]

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

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
n : ℤ
hx : |x| ≤ 1
hn : 0 < n
this : -1 + 1 ≤ x + ↑n
⊢ 0 ≤ x + ↑n

Tactic:
neg_add_cancel

Goal state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
n : ℤ
hx : |x| ≤ 1
hn : 0 < n
this : 0 ≤ x + ↑n
⊢ 0 ≤ x + ↑n
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: case refine_3
α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
x✝ : Nontrivial αˣ ∧ DenselyOrdered αˣ
H₁ : Nontrivial αˣ
H₂ : DenselyOrdered αˣ
⊢ DenselyOrdered α

Tactic:
refine ⟨fun x y h ↦ ?_⟩
    lift y to αˣ using (ne_zero_of_lt h).isUnit
    obtain rfl | hx := eq_zero_or_pos x
    · obtain ⟨z, hz⟩ := exists_one_lt' (α := αˣ)
      exact ⟨(y * z⁻¹ : αˣ), by simp, Units.val_lt_val.mpr <| by simp [hz]⟩
    · lift x to αˣ using hx.ne'.isUnit
      obtain ⟨z, hz, hz'⟩ := H₂.dense x y (Units.val_lt_val.mpr h)
      exact ⟨z, by simp [hz, hz']⟩

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
x : WithZero α
inst✝ : NoMinOrder α
hx : x ≠ 0
z : α
hlt : z < unzero hx
⊢ ∃ y, y ≠ 0 ∧ y < x

Tactic:
← WithZero.coe_lt_coe,

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
x : WithZero α
inst✝ : NoMinOrder α
hx : x ≠ 0
z : α
hlt : ↑z < ↑(unzero hx)
⊢ ∃ y, y ≠ 0 ∧ y < x
Module: Mathlib.Data.Nat.Find

Goal state before:
pp: P Q : ℕ → Prop
inst✝¹ : DecidablePred P
inst✝ : DecidablePred Q
hPQ : ∀ (n : ℕ), P n → Q n
n : ℕ
⊢ findGreatest P n ≤ findGreatest Q n

Tactic:
by
  induction n with
  | zero => rfl
  | succ n hn =>
    by_cases h : P (n + 1)
    · rw [findGreatest_eq h, findGreatest_eq (hPQ _ h)]
    · rw [findGreatest_of_not h]
      exact le_trans hn (Nat.findGreatest_mono_right _ <| le_succ _)

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

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
y : WithZero α
a b : α
hy : ↑b ≤ y
hne : y ≠ 0
⊢ b ≤ unzeroD a y

Tactic:
rwa [le_unzeroD_iff hne]

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
a : R
n : ℕ
inst✝ : IsStrictOrderedRing R
hn : n ≠ 0
ha : 0 ≤ a
⊢ n ≤ ⌊a⌋₊ ↔ ↑n ≤ a

Tactic:
· exact le_floor_iff ha

Goal state after:
Module: Mathlib.Order.Directed

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_3
inst✝¹ : Preorder α
inst✝ : OrderBot α
e : ι → β
f : ι → α
hf : Directed (fun x1 x2 ↦ x1 ≤ x2) f
he : Injective e
a : β
⊢ ∀ (y : β),
    ∃ z,
      (fun x1 x2 ↦ x1 ≤ x2) (extend e f ⊥ a) (extend e f ⊥ z) ∧ (fun x1 x2 ↦ x1 ≤ x2) (extend e f ⊥ y) (extend e f ⊥ z)

Tactic:
b

Goal state after:
α : Type u_1
β : Type u_2
ι : Sort u_3
inst✝¹ : Preorder α
inst✝ : OrderBot α
e : ι → β
f : ι → α
hf : Directed (fun x1 x2 ↦ x1 ≤ x2) f
he : Injective e
a b : β
⊢ ∃ z, (fun x1 x2 ↦ x1 ≤ x2) (extend e f ⊥ a) (extend e f ⊥ z) ∧ (fun x1 x2 ↦ x1 ≤ x2) (extend e f ⊥ b) (extend e f ⊥ z)
Module: Mathlib.Order.WithBot

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : LT α
inst✝ : NoMinOrder α
h : DenselyOrdered (WithBot α)
a : α
⊢ ∀ (a₂ : α), a < a₂ → ∃ a_2, a < a_2 ∧ a_2 < a₂

Tactic:
b

Goal state after:
case mp
α : Type u_1
inst✝¹ : LT α
inst✝ : NoMinOrder α
h : DenselyOrdered (WithBot α)
a b : α
⊢ a < b → ∃ a_2, a < a_2 ∧ a_2 < b
Module: Mathlib.Order.WithBot

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : LT α
inst✝ : NoMaxOrder α
h : DenselyOrdered (WithTop α)
a : α
⊢ ∀ (a₂ : α), a < a₂ → ∃ a_2, a < a_2 ∧ a_2 < a₂

Tactic:
b

Goal state after:
case mp
α : Type u_1
inst✝¹ : LT α
inst✝ : NoMaxOrder α
h : DenselyOrdered (WithTop α)
a b : α
⊢ a < b → ∃ a_2, a < a_2 ∧ a_2 < b
Module: Mathlib.Order.Directed

Goal state before:
pp: ι : Type u_5
α : ι → Type u_6
r : (i : ι) → α i → α i → Prop
d : (i : ι) → Set (α i)
hd : ∀ (i : ι), DirectedOn (r i) (d i)
a : (i : ι) → α i
ha : a ∈ Set.univ.pi d
⊢ ∀ y ∈ Set.univ.pi d,
    ∃ z ∈ Set.univ.pi d, (fun x y ↦ ∀ (i : ι), r i (x i) (y i)) a z ∧ (fun x y ↦ ∀ (i : ι), r i (x i) (y i)) y z

Tactic:
b

Goal state after:
ι : Type u_5
α : ι → Type u_6
r : (i : ι) → α i → α i → Prop
d : (i : ι) → Set (α i)
hd : ∀ (i : ι), DirectedOn (r i) (d i)
a : (i : ι) → α i
ha : a ∈ Set.univ.pi d
b : (i : ι) → α i
⊢ b ∈ Set.univ.pi d →
    ∃ z ∈ Set.univ.pi d, (fun x y ↦ ∀ (i : ι), r i (x i) (y i)) a z ∧ (fun x y ↦ ∀ (i : ι), r i (x i) (y i)) b z
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 + 1) = ⅟b * a + ⅟a * b ↔ -1 + 0 = ⅟b * a + ⅟a * b

Tactic:
neg_add_cancel

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

Goal state before:
pp: R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a : R
⊢ ∀ ⦃b : R⦄, a < b → (fun a ↦ a ^ n) a < (fun a ↦ a ^ n) b

Tactic:
b

Goal state after:
R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a b : R
⊢ a < b → (fun a ↦ a ^ n) a < (fun a ↦ a ^ n) b
Module: Mathlib.Data.Set.Monotone

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f₁ f₂ : α → β
inst✝¹ : Preorder α
inst✝ : Preorder β
h₁ : MonotoneOn f₁ s
h : EqOn f₁ f₂ s
a : α
ha : a ∈ s
⊢ ∀ ⦃b : α⦄, b ∈ s → a ≤ b → f₂ a ≤ f₂ b

Tactic:
b

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
f₁ f₂ : α → β
inst✝¹ : Preorder α
inst✝ : Preorder β
h₁ : MonotoneOn f₁ s
h : EqOn f₁ f₂ s
a : α
ha : a ∈ s
b : α
⊢ b ∈ s → a ≤ b → f₂ a ≤ f₂ b
Module: Mathlib.Data.Set.Monotone

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f₁ f₂ : α → β
inst✝¹ : Preorder α
inst✝ : Preorder β
h₁ : StrictMonoOn f₁ s
h : EqOn f₁ f₂ s
a : α
ha : a ∈ s
⊢ ∀ ⦃b : α⦄, b ∈ s → a < b → f₂ a < f₂ b

Tactic:
b

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
f₁ f₂ : α → β
inst✝¹ : Preorder α
inst✝ : Preorder β
h₁ : StrictMonoOn f₁ s
h : EqOn f₁ f₂ s
a : α
ha : a ∈ s
b : α
⊢ b ∈ s → a < b → f₂ a < f₂ b
Module: Mathlib.Data.Set.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s s' : Set α
t t' : Set β
⊢ image2 f (s ∩ s') (t ∪ t') ⊆ image2 f s t ∪ image2 f s' t'

Tactic:
image2_union_right

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s s' : Set α
t t' : Set β
⊢ image2 f (s ∩ s') t ∪ image2 f (s ∩ s') t' ⊆ image2 f s t ∪ image2 f s' t'
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
a₁ a₂ : α
b₁ b₂ : β
x : α
y : β
⊢ (x, y) ∈ Icc a₁ a₂ ×ˢ Icc b₁ b₂ ↔ (x, y) ∈ Icc (a₁, b₁) (a₂, b₂)

Tactic:
simp [and_assoc, and_left_comm]

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : Set α
a b : α
h : DirectedOn (fun x y ↦ y ≤ x) s
hMin : Minimal (fun x ↦ x ∈ s) a
hb : b ∈ s
⊢ a ≤ b

Tactic:
obtain ⟨z, hz, hza, hzb⟩ := h a hMin.1 b hb
  exact (hMin.2 hz hza).trans hzb

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
⊢ b ∉ upperBounds s ↔ ∃ c ∈ s, ¬c ≤ b

Tactic:
mem_upperBounds,

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
s : Set α
a b : α
h : IsLUB s a
⊢ (¬∀ x ∈ s, x ≤ b) ↔ ∃ c ∈ s, ¬c ≤ b
Module: Mathlib.Tactic.NormNum.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
m : ℕ
⊢ IsNat (↑↑m) m

Tactic:
exact ⟨by simp⟩

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

Goal state before:
pp: case inl
α : Type u_4
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
hb : 0 ≤ 0
h : ∀ (ε : α), 1 < ε → a ≤ 0 * ε
⊢ a ≤ 0

pp: case inr
α : Type u_4
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
hb✝ : 0 ≤ b
h : ∀ (ε : α), 1 < ε → a ≤ b * ε
hb : 0 < b
⊢ a ≤ b

Tactic:
· simp_rw [zero_mul] at h
    exact h 2 one_lt_two

Goal state after:
case inr
α : Type u_4
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
hb✝ : 0 ≤ b
h : ∀ (ε : α), 1 < ε → a ≤ b * ε
hb : 0 < b
⊢ a ≤ b
Module: Mathlib.Tactic.NormNum.Basic

Goal state before:
pp: α : Type u
inst✝ : Semiring α
num✝ denom✝ : ℕ
inv✝¹ inv✝ : Invertible ↑denom✝
⊢ ↑num✝ * ⅟↑denom✝ = ↑num✝ * ⅟↑denom✝

Tactic:
by congr; apply Subsingleton.elim

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

Goal state before:
pp: α : Type u
inst✝ : Ring α
num✝ : ℤ
denom✝ : ℕ
inv✝¹ inv✝ : Invertible ↑denom✝
⊢ ↑num✝ * ⅟↑denom✝ = ↑num✝ * ⅟↑denom✝

Tactic:
by congr; apply Subsingleton.elim

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

Goal state before:
pp: α : Type u
x : List α
m n : ℕ
⊢ take n (drop m x) ++ drop (m + n) x = drop m x

Tactic:
drop_take_append_drop

Goal state after:
α : Type u
x : List α
m n : ℕ
⊢ drop m x = drop m x
Module: Mathlib.Data.List.TakeDrop

Goal state before:
pp: α : Type u
p : α → Bool
l : List α
⊢ span p l = (takeWhile p l, dropWhile p l)

Tactic:
simpa using! span.loop_eq_take_drop p l []

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

Goal state before:
pp: α : Type u_2
inst✝² : Field α
inst✝¹ : PartialOrder α
inst✝ : IsStrictOrderedRing α
a b c d : α
hc : c ≠ 0
hd : d ≠ 0
⊢ a / c - b / d < 0 ↔ a / c < b / d

Tactic:
sub_lt_zero

Goal state after:
α : Type u_2
inst✝² : Field α
inst✝¹ : PartialOrder α
inst✝ : IsStrictOrderedRing α
a b c d : α
hc : c ≠ 0
hd : d ≠ 0
⊢ a / c < b / d ↔ a / c < b / d
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
R : α → β → Prop
p : α → Bool
q : β → Bool
hpq : ∀ ⦃a : α⦄ ⦃b : β⦄, R a b → (p a = true ↔ q b = true)
a : α
as : List α
b : β
bs : List β
h₁ : R a b
h₂ : Forall₂ R as bs
h : p a = true
this : q b = true
⊢ Forall₂ R (filter p (a :: as)) (filter q (b :: bs))

Tactic:
simp only [filter_cons_of_pos h, filter_cons_of_pos this, forall₂_cons, h₁, true_and,
        rel_filter hpq h₂]

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

Goal state before:
pp: case refl
α : Type u
β : Type v
l₁ l₂ : List α
f : α → β
h : Injective f
h2 : map f l₁ ⊆ map f l₂
x : α
hx : x ∈ l₁
hx' : x ∈ l₂
hxx' : f x = f x
⊢ x ∈ l₂

Tactic:
exact hx'

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

Goal state before:
pp: M : Type u_1
inst✝ : CommGroupWithZero M
e : M
L l l' l₀ : NF M
h : L.eval * l.eval = l'.eval
h' : ((0, e) ::ᵣ l).eval = l₀.eval
⊢ L.eval * l₀.eval = ((0, e) ::ᵣ l').eval

Tactic:
by
  rw [← eval_mul_eval_cons 0 e h, h']

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

Goal state before:
pp: q : ℚ
n : ℕ
⊢ q.num ^ n /. ↑(q.den ^ n) = q.num ^ n /. ↑q.den ^ n

Tactic:
Int.natCast_pow

Goal state after:
q : ℚ
n : ℕ
⊢ q.num ^ n /. ↑q.den ^ n = q.num ^ n /. ↑q.den ^ n
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : BEq α
inst✝² : LawfulBEq α
inst✝¹ : BEq β
inst✝ : LawfulBEq β
f : α → β
finj : Injective f
l₁ l₂ : List α
⊢ map f (l₁.diff l₂) = (map f l₁).diff (map f l₂)

Tactic:
by
  simp only [diff_eq_foldl, foldl_map, map_foldl_erase finj]

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

Goal state before:
pp: num den n : ℕ
⊢ ↑num ^ n /. ↑den ^ n = ↑num ^ n /. ↑(den ^ n)

Tactic:
Int.natCast_pow

Goal state after:
num den n : ℕ
⊢ ↑num ^ n /. ↑den ^ n = ↑num ^ n /. ↑den ^ n
Module: Mathlib.Data.NNRat.Defs

Goal state before:
pp: q : ℚ
p : ℚ≥0
hq : 0 ≤ q
⊢ ↑q.toNNRat < ↑p ↔ q < ↑p

Tactic:
Rat.coe_toNNRat q hq

Goal state after:
q : ℚ
p : ℚ≥0
hq : 0 ≤ q
⊢ q < ↑p ↔ q < ↑p
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: case neg
a b : ℤ
b0 : ¬b = 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a * ↑d = n * b
⊢ d ∣ n.natAbs * b.natAbs

Tactic:
← Int.natAbs_mul,

Goal state after:
case neg
a b : ℤ
b0 : ¬b = 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a * ↑d = n * b
⊢ d ∣ (n * b).natAbs
Module: Mathlib.Order.GaloisConnection.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
s : Set α
t : Set β
l : α → β → γ
u₁ : β → γ → α
u₂ : α → γ → β
a₀ : α
b₀ : β
h₁ : ∀ (b : β), GaloisConnection (swap l b) (u₁ b)
h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)
ha₀ : ∀ (b : α), a₀ ≤ b ↔ ∀ x ∈ s, x ≤ b
hb₀ : ∀ (b : β), b₀ ≤ b ↔ ∀ x ∈ t, x ≤ b
⊢ ∀ (b : γ), l a₀ b₀ ≤ b ↔ b ∈ upperBounds (image2 l s t)

Tactic:
mem_upperBounds,

Goal state after:
α : Type u
β : Type v
γ : Type w
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
s : Set α
t : Set β
l : α → β → γ
u₁ : β → γ → α
u₂ : α → γ → β
a₀ : α
b₀ : β
h₁ : ∀ (b : β), GaloisConnection (swap l b) (u₁ b)
h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)
ha₀ : ∀ (b : α), a₀ ≤ b ↔ ∀ x ∈ s, x ≤ b
hb₀ : ∀ (b : β), b₀ ≤ b ↔ ∀ x ∈ t, x ≤ b
⊢ ∀ (b : γ), l a₀ b₀ ≤ b ↔ ∀ x ∈ image2 l s t, x ≤ b
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
ι₁ : Sort u_8
ι₂ : Sort u_9
κ₁ : ι₁ → Sort u_10
κ₂ : ι₂ → Sort u_11
f : (i₁ : ι₁) → κ₁ i₁ → (i₂ : ι₂) → κ₂ i₂ → α
⊢ ⨆ i₁, ⨆ j₁, ⨆ i₂, ⨆ j₂, f i₁ j₁ i₂ j₂ = ⨆ i₂, ⨆ j₂, ⨆ i₁, ⨆ j₁, f i₁ j₁ i₂ j₂

Tactic:
by
  simp only [@iSup_comm _ (κ₁ _), @iSup_comm _ ι₁]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝ : CompleteLattice α
e : ι → β
he : Injective e
f : ι → α
⊢ ⨆ j, extend e f ⊥ j = ⨆ i, f i

Tactic:
iSup_split _ fun j => ∃ i, e i = j

Goal state after:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝ : CompleteLattice α
e : ι → β
he : Injective e
f : ι → α
⊢ (⨆ i, ⨆ (_ : ∃ i_1, e i_1 = i), extend e f ⊥ i) ⊔ ⨆ i, ⨆ (_ : ¬∃ i_1, e i_1 = i), extend e f ⊥ i = ⨆ i, f i
Module: Mathlib.Order.CompleteBooleanAlgebra

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

Tactic:
iInf_subtype,

Goal state after:
α : Type u
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLattice α
minAx : MinimalAxioms α
f : (a : ι) → κ a → α
⊢ ⨅ i, ⨆ j, f i j = ⨅ i ∈ range fun x ↦ range (f x), ⨆ b, ↑b
Module: Mathlib.Data.Set.Lattice

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

Tactic:
show i = j by by_contra i_ne_j; exact Disjoint.ne_of_mem (Es_disj i_ne_j) hix hjx rfl

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

Goal state before:
pp: α : Type u_1
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : WellFoundedLT α
hs : s.Nonempty
n : α
⊢ sInf s = n ↔ n ∈ s ∧ ∀ a ∈ s, n ≤ a

Tactic:
have : OrderBot α := WellFoundedLT.toOrderBot α

Goal state after:
α : Type u_1
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : WellFoundedLT α
hs : s.Nonempty
n : α
this : OrderBot α
⊢ sInf s = n ↔ n ∈ s ∧ ∀ a ∈ s, n ≤ a
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case pos
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : s ⊆ {⊤}
⊢ ⊤ ∈ lowerBounds s

pp: case neg
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
⊢ ↑(sInf ((fun a ↦ ↑a) ⁻¹' s)) ∈ lowerBounds s

Tactic:
· intro a ha
      exact top_le_iff.2 (Set.mem_singleton_iff.1 (h ha))

Goal state after:
case neg
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
⊢ ↑(sInf ((fun a ↦ ↑a) ⁻¹' s)) ∈ lowerBounds s
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : MonotoneOn f [[a, b]]
⊢ MapsTo f (Icc (min a b) (max a b)) (Icc (f a ⊓ f b) (f (max a b)))

pp: case hx
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : MonotoneOn f [[a, b]]
⊢ a ∈ [[a, b]]

pp: case hy
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : MonotoneOn f [[a, b]]
⊢ b ∈ [[a, b]]

Tactic:
← hf.map_inf

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : MonotoneOn f [[a, b]]
⊢ MapsTo f (Icc (min a b) (max a b)) (Icc (f (min a b)) (f (max a b)))

case hx
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : MonotoneOn f [[a, b]]
⊢ a ∈ [[a, b]]

case hy
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : MonotoneOn f [[a, b]]
⊢ b ∈ [[a, b]]

case hx
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : MonotoneOn f [[a, b]]
⊢ a ∈ [[a, b]]

case hy
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : MonotoneOn f [[a, b]]
⊢ b ∈ [[a, b]]
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : AntitoneOn f [[a, b]]
⊢ MapsTo f (Icc (min a b) (max a b)) (Icc (f (max a b)) (f a ⊔ f b))

pp: case hx
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : AntitoneOn f [[a, b]]
⊢ a ∈ [[a, b]]

pp: case hy
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : AntitoneOn f [[a, b]]
⊢ b ∈ [[a, b]]

Tactic:
← hf.map_inf

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : AntitoneOn f [[a, b]]
⊢ MapsTo f (Icc (min a b) (max a b)) (Icc (f (max a b)) (f (min a b)))

case hx
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : AntitoneOn f [[a, b]]
⊢ a ∈ [[a, b]]

case hy
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : AntitoneOn f [[a, b]]
⊢ b ∈ [[a, b]]

case hx
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : AntitoneOn f [[a, b]]
⊢ a ∈ [[a, b]]

case hy
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : AntitoneOn f [[a, b]]
⊢ b ∈ [[a, b]]
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
a b : α
inst✝ : DenselyOrdered α
⊢ (uIoo a b).Nonempty ↔ a ≠ b

Tactic:
simp [uIoo, eq_comm]

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : One M
f : ι → M
s : Set ι
⊢ (∀ (x : ι), x ∈ s → f x = 1) ↔ EqOn f 1 s

Tactic:
EqOn,

Goal state after:
ι : Type u_1
M : Type u_3
inst✝ : One M
f : ι → M
s : Set ι
⊢ (∀ (x : ι), x ∈ s → f x = 1) ↔ ∀ ⦃x : ι⦄, x ∈ s → f x = 1 x
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: case inl.inr
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
hx : 2 * fract x ≠ 1
m : ℤ
hm : ↑(2 * m + 1) = 2 * x
⊢ round x = (2 * m + 1) / 2

Tactic:
refine absurd ?_ hx

Goal state after:
case inl.inr
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
hx : 2 * fract x ≠ 1
m : ℤ
hm : ↑(2 * m + 1) = 2 * x
⊢ 2 * fract x = 1
Module: Mathlib.Data.PNat.Basic

Goal state before:
pp: case neg
a b : ℕ+
hab : a < b
h : ¬1 < b
⊢ ↑a ≤ 1

Tactic:
exact hab.le.trans (le_of_not_gt h)

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

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

Tactic:
conv_rhs => rw [abs_eq_self.mpr (sub_nonneg.mpr hx), ← fract_add_floor x, add_sub_assoc]

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

Goal state before:
pp: m n : ℕ+
h : n.mod m = m
⊢ n.mod m ≤ n

Tactic:
apply (mod_le n m).left

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

Tactic:
gcongr <;> apply floor_le

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
h₀ : 0 ≤ b
h₁ : b < 1
z : ℤ
hz : a - b = ↑z
⊢ ↑⌊a⌋ = ↑z

Tactic:
refine congrArg Int.cast ?_

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
h₀ : 0 ≤ b
h₁ : b < 1
z : ℤ
hz : a - b = ↑z
⊢ ⌊a⌋ = z
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: R : Type u_3
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
m : ℕ
⊢ IsNat ⌊↑m⌋ m

Tactic:
exact ⟨by simp⟩

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

Goal state before:
pp: R : Type u_3
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
m : ℤ
⊢ IsInt ⌊↑m⌋ m

Tactic:
exact ⟨by simp⟩

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

Goal state before:
pp: R : Type u_3
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
m : ℕ
⊢ IsNat ⌈↑m⌉ m

Tactic:
exact ⟨by simp⟩

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

Goal state before:
pp: R : Type u_3
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
m : ℤ
⊢ IsInt ⌈↑m⌉ m

Tactic:
exact ⟨by simp⟩

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

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
m : ℕ
⊢ IsNat (fract ↑m) 0

Tactic:
exact ⟨by simp⟩

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

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
m : ℤ
⊢ IsNat (fract ↑m) 0

Tactic:
exact ⟨by simp⟩

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

Goal state before:
pp: R : Type u_3
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
m : ℕ
⊢ IsNat (round ↑m) m

Tactic:
exact ⟨by simp⟩

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

Goal state before:
pp: R : Type u_3
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
m : ℤ
⊢ IsInt (round ↑m) m

Tactic:
exact ⟨by simp⟩

Goal state after: