mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs

Goal state before:
pp: α : Type u
inst✝³ : MulOneClass α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedMul α
a b : α
inst✝ : MulLeftStrictMono α
⊢ (∃ x, b = a * x ∧ a ≠ b) ↔ ∃ c, c > 1 ∧ b = a * c

Tactic:
apply exists_congr

Goal state after:
α : Type u
inst✝³ : MulOneClass α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedMul α
a b : α
inst✝ : MulLeftStrictMono α
⊢ ∀ (a_1 : α), b = a * a_1 ∧ a ≠ b ↔ a_1 > 1 ∧ b = a * a_1
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
β : Type v
inst✝² : LE α
inst✝¹ : Add α
inst✝ : ExistsAddOfLE α
a✝ b✝ : WithTop α
a b : α
h : ↑a ≤ ↑b
⊢ ∃ c, ↑b = ↑a + c

Tactic:
obtain ⟨c, rfl⟩ := exists_add_of_le (WithTop.coe_le_coe.1 h)

Goal state after:
α : Type u
β : Type v
inst✝² : LE α
inst✝¹ : Add α
inst✝ : ExistsAddOfLE α
a✝ b : WithTop α
a c : α
h : ↑a ≤ ↑(a + c)
⊢ ∃ c_1, ↑(a + c) = ↑a + c_1
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
inst✝ : Add α
a : α
ha : IsAddLeftRegular a
⊢ IsAddLeftRegular ↑a

Tactic:
by
  rintro (_ | b) (_ | c) <;> simp [none_eq_bot, some_eq_coe, ← coe_add]; simpa using @ha _ _

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
inst✝ : Add α
a : α
ha : IsAddRightRegular a
⊢ IsAddRightRegular ↑a

Tactic:
by
  rintro (_ | b) (_ | c) <;> simp [none_eq_bot, some_eq_coe, ← coe_add]; simpa using @ha _ _

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
S : Type u_3
inst✝⁶ : Semiring S
inst✝⁵ : LinearOrder S
inst✝⁴ : FloorSemiring S
F : Type u_4
inst✝³ : FunLike F R S
inst✝² : RingHomClass F R S
inst✝¹ : IsStrictOrderedRing R
inst✝ : IsStrictOrderedRing S
f : F
hf : StrictMono ⇑f
a : R
n : ℕ
⊢ ↑n ≤ f a ↔ ↑n ≤ a

Tactic:
← map_natCast f,

Goal state after:
R : Type u_1
inst✝⁹ : Semiring R
inst✝⁸ : LinearOrder R
inst✝⁷ : FloorSemiring R
S : Type u_3
inst✝⁶ : Semiring S
inst✝⁵ : LinearOrder S
inst✝⁴ : FloorSemiring S
F : Type u_4
inst✝³ : FunLike F R S
inst✝² : RingHomClass F R S
inst✝¹ : IsStrictOrderedRing R
inst✝ : IsStrictOrderedRing S
f : F
hf : StrictMono ⇑f
a : R
n : ℕ
⊢ f ↑n ≤ f a ↔ ↑n ≤ a
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: R : Type u_1
inst✝⁷ : Semiring R
inst✝⁶ : LinearOrder R
inst✝⁵ : FloorSemiring R
S : Type u_3
inst✝⁴ : Semiring S
inst✝³ : LinearOrder S
inst✝² : FloorSemiring S
F : Type u_4
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : StrictMono ⇑f
a : R
n : ℕ
⊢ f a ≤ ↑n ↔ a ≤ ↑n

Tactic:
← map_natCast f,

Goal state after:
R : Type u_1
inst✝⁷ : Semiring R
inst✝⁶ : LinearOrder R
inst✝⁵ : FloorSemiring R
S : Type u_3
inst✝⁴ : Semiring S
inst✝³ : LinearOrder S
inst✝² : FloorSemiring S
F : Type u_4
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : StrictMono ⇑f
a : R
n : ℕ
⊢ f a ≤ f ↑n ↔ a ≤ ↑n
Module: Mathlib.Algebra.Order.Ring.Basic

Goal state before:
pp: R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsOrderedRing R
inst✝ : ExistsAddOfLE R
n : ℕ
hn : Even n
a : R
⊢ 0 ≤ a ^ n

Tactic:
obtain ⟨k, rfl⟩ := hn; rw [pow_add]; exact mul_self_nonneg _

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

Goal state before:
pp: R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a b : R
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Even n
⊢ (a + b) ^ n ≤ 2 ^ (n - 1) * (a ^ n + b ^ n)

Tactic:
by
  obtain ⟨n, rfl⟩ := hn
  rw [← two_mul, pow_mul]
  calc
    _ ≤ (2 * (a ^ 2 + b ^ 2)) ^ n := pow_le_pow_left₀ (sq_nonneg _) add_sq_le _
    _ = 2 ^ n * (a ^ 2 + b ^ 2) ^ n := by -- TODO: Should be `Nat.cast_commute`
        rw [Commute.mul_pow]; simp [Commute, SemiconjBy, two_mul, mul_two]
    _ ≤ 2 ^ n * (2 ^ (n - 1) * ((a ^ 2) ^ n + (b ^ 2) ^ n)) := mul_le_mul_of_nonneg_left
          (add_pow_le (sq_nonneg _) (sq_nonneg _) _) <| pow_nonneg (zero_le_two (α := R)) _
    _ = _ := by
      simp only [← mul_assoc, ← pow_add, ← pow_mul]
      cases n
      · rfl
      · simp [Nat.two_mul]

Goal state after:
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 b : R
hab : a < b
ha : a ≤ 0
hb : b ≤ 0
c : R
hac : 0 = a + c
d : R
hbd : 0 = b + d
hd : 0 ≤ d
⊢ c ^ n = b ^ n + (c ^ n + d ^ n)

Tactic:
by rw [add_left_comm, hn.pow_add_pow_eq_zero hbd.symm, add_zero]

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

Goal state before:
pp: α : Type u_1
β : Type u_3
f : α → β → β
a : α
h : ∀ (b : β), f a b = b
t : Set β
⊢ id '' t = t

Tactic:
image_id

Goal state after:
α : Type u_1
β : Type u_3
f : α → β → β
a : α
h : ∀ (b : β), f a b = b
t : Set β
⊢ t = t
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 ∪ image2 f (s ∩ s') t' ⊆ image2 f s t ∪ image2 f s' t'

Tactic:
nth_grw 1 [inter_subset_left, inter_subset_right]

Goal state after:
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 (t ∩ t') ∪ image2 f s' (t ∩ t') ⊆ image2 f s t ∪ image2 f s' t'

Tactic:
nth_grw 1 [inter_subset_left, inter_subset_right]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
a b : α
inst✝ : DenselyOrdered α
⊢ Ioo a b = ∅ ↔ ¬a < b

Tactic:
by
  contrapose!; exact nonempty_Ioo

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

Goal state before:
pp: α : Type u_7
f : α → α
a : α
n : ℕ
⊢ iterate f a n = iterateTR f a n

Tactic:
exact Eq.symm <| iterateTR_loop_eq f a n []

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

Goal state before:
pp: α : Type u
l : List α
n : ℕ
⊢ (take n l).tail = take (n - 1) l.tail

Tactic:
by
  ext
  grind

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

Goal state before:
pp: α : Type u
l : List α
n : ℕ
⊢ (take n l).dropLast = take (n - 1) l.dropLast

Tactic:
by
  ext
  grind

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

Goal state before:
pp: α : Type u
l : List α
n : ℕ
⊢ (drop n l).tail = drop n l.tail

Tactic:
by
  ext
  grind

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

Goal state before:
pp: α : Type u
l : List α
n : ℕ
⊢ (drop n l).dropLast = drop n l.dropLast

Tactic:
by
  ext
  grind

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 : α
a2 : 2 ≤ a
⊢ 2⁻¹ ≤ 1 - 1 / a

Tactic:
le_sub_iff_add_le,

Goal state after:
α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a : α
a2 : 2 ≤ a
⊢ 2⁻¹ + 1 / a ≤ 1
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : α
ha : 0 ≤ a
hc : 0 ≤ c
h : c < a * b
hb : 0 < b
⊢ ∃ b' ∈ Set.Ico 0 b, c < a * b'

Tactic:
mul_comm a

Goal state after:
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : α
ha : 0 ≤ a
hc : 0 ≤ c
hb : 0 < b
h : c < b * a
⊢ ∃ b' ∈ Set.Ico 0 b, c < b' * a
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:
mul_comm a

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: case inr
α : Type u_1
l₁ l₂ : List α
n : ℕ
a : α
this : ∀ {l₁ l₂ : List α}, l₁.length ≤ l₂.length → (l₁.insertIdx n a ~ l₂.insertIdx n a ↔ l₁ ~ l₂)
hle : ¬l₁.length ≤ l₂.length
⊢ l₂ ~ l₁ ↔ l₁ ~ l₂

Tactic:
perm_comm

Goal state after:
case inr
α : Type u_1
l₁ l₂ : List α
n : ℕ
a : α
this : ∀ {l₁ l₂ : List α}, l₁.length ≤ l₂.length → (l₁.insertIdx n a ~ l₂.insertIdx n a ↔ l₁ ~ l₂)
hle : ¬l₁.length ≤ l₂.length
⊢ l₁ ~ l₂ ↔ l₁ ~ l₂
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: case trans
α : Type u_1
β : Type u_2
r : α → β → Prop
l u l₁✝ l₂✝ l₃✝ : List α
a✝¹ : l₁✝ ~ l₂✝
a✝ : l₂✝ ~ l₃✝
ih₁ : ∀ {v : List β}, Forall₂ r l₂✝ v → (Forall₂ r ∘r Perm) l₁✝ v
ih₂ : ∀ {v : List β}, Forall₂ r l₃✝ v → (Forall₂ r ∘r Perm) l₂✝ v
v : List β
huv : Forall₂ r l₃✝ v
⊢ (Forall₂ r ∘r Perm) l₁✝ v

Tactic:
rcases ih₂ huv with ⟨lb₂, hab₂, h₂₃⟩
    rcases ih₁ hab₂ with ⟨lb₁, hab₁, h₁₂⟩
    exact ⟨lb₁, hab₁, Perm.trans h₁₂ h₂₃⟩

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

Goal state before:
pp: M : Type u_1
inst✝ : CommGroupWithZero M
r₁ r₂ : ℤ
x : M
l₁ l₂ l : NF M
h : l₁.eval / l₂.eval = l.eval
⊢ ((r₁, x) ::ᵣ l₁).eval / ((r₂, x) ::ᵣ l₂).eval = ((r₁ - r₂, x) ::ᵣ l).eval

Tactic:
by
  simp only [← h, eval_cons, div_eq_mul_inv, mul_inv, ← zpow'_neg, sub_eq_add_neg, zpow'_add]
  ac_rfl

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s t : List α
hf : Injective f
h : s.Disjoint t
⊢ (pmap (fun a x ↦ f a) s ⋯).Disjoint (map f t)

Tactic:
← pmap_eq_map (fun _ _ ↦ trivial)

Goal state after:
α : Type u
β : Type v
f : α → β
s t : List α
hf : Injective f
h : s.Disjoint t
⊢ (pmap (fun a x ↦ f a) s ⋯).Disjoint (pmap (fun a x ↦ f a) t ⋯)
Module: Mathlib.Algebra.Order.Ring.Unbundled.Rat

Goal state before:
pp: m : ℕ
s : Bool
e : ℕ
⊢ 0 ≤ if s = true then normalize (↑m) (10 ^ e) ⋯ else ↑(m * 10 ^ e)

Tactic:
cases s

Goal state after:
case false
m e : ℕ
⊢ 0 ≤ if false = true then normalize (↑m) (10 ^ e) ⋯ else ↑(m * 10 ^ e)

case true
m e : ℕ
⊢ 0 ≤ if true = true then normalize (↑m) (10 ^ e) ⋯ else ↑(m * 10 ^ e)
Module: Mathlib.Algebra.Field.Rat

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

Tactic:
coe_div,

Goal state after:
q : ℚ≥0
⊢ ↑↑q.num / ↑↑q.den = ↑q
Module: Mathlib.Algebra.Divisibility.Units

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
x y z : α
hu : IsUnit x
⊢ IsRelPrime y (x * z) ↔ IsRelPrime y z

Tactic:
rw [isRelPrime_comm, isRelPrime_mul_unit_left_left hu, isRelPrime_comm]

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

Goal state before:
pp: q₁ q₂ : ℚ
⊢ (q₁ + q₂).den ∣ q₁.den.lcm q₂.den

Tactic:
rw [add_def, normalize_eq, Nat.div_dvd_iff_dvd_mul (Nat.gcd_dvd_right _ _)
    (Nat.gcd_pos_of_pos_right _ (by simp [Nat.pos_iff_ne_zero])), ← Nat.gcd_mul_lcm,
    mul_dvd_mul_iff_right (Nat.lcm_ne_zero (by simp) (by simp)), Nat.dvd_gcd_iff]
  refine ⟨?_, dvd_mul_right _ _⟩
  rw [← Int.natCast_dvd_natCast, Int.dvd_natAbs]
  apply Int.dvd_add
    <;> apply dvd_mul_of_dvd_right <;> rw [Int.natCast_dvd_natCast]
    <;> [exact Nat.gcd_dvd_right _ _; exact Nat.gcd_dvd_left _ _]

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionSemiring α
a : α
b : ℤ
nb ne : ℕ
pb : IsInt b (Int.negOfNat nb)
pe' : IsNat (a ^ nb)⁻¹ ne
⊢ IsNat (a ^ b) ne

Tactic:
rwa [pb.out, Int.cast_negOfNat, zpow_neg, zpow_natCast]

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionRing α
a : α
b : ℤ
nb ne : ℕ
pb : IsInt b (Int.negOfNat nb)
pe' : IsInt (a ^ nb)⁻¹ (Int.negOfNat ne)
⊢ IsInt (a ^ b) (Int.negOfNat ne)

Tactic:
rwa [pb.out, Int.cast_negOfNat, zpow_neg, zpow_natCast]

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionSemiring α
a : α
b : ℤ
nb num den : ℕ
pb : IsInt b (Int.negOfNat nb)
pe' : IsNNRat (a ^ nb)⁻¹ num den
⊢ IsNNRat (a ^ b) num den

Tactic:
rwa [pb.out, Int.cast_negOfNat, zpow_neg, zpow_natCast]

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionRing α
a : α
b : ℤ
nb : ℕ
num : ℤ
den : ℕ
pb : IsInt b (Int.negOfNat nb)
pe' : IsRat (a ^ nb)⁻¹ num den
⊢ IsRat (a ^ b) num den

Tactic:
rwa [pb.out, Int.cast_negOfNat, zpow_neg, zpow_natCast]

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

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

Tactic:
refine fun i hi => le_sSup ⟨i - n, ?_⟩

Goal state after:
case a
α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
n i : ℕ
hi : i ≥ n
⊢ (fun i ↦ u (i + n)) (i - n) = u i
Module: Mathlib.Order.GaloisConnection.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a₁ a₂ : α
b₁ b₂ : β
l : α → β
u : β → α
inst✝¹ : PartialOrder β
inst✝ : SemilatticeInf α
gi : GaloisInsertion l u
⊢ ∀ (a b c : β), a ≤ b → a ≤ c → a ≤ gi.choice (u b ⊓ u c) ⋯

Tactic:
by
      simp only [gi.choice_eq]
      exact fun a b c hac hbc =>
        (gi.le_l_u a).trans <|
          gi.gc.monotone_l <| le_inf (gi.gc.monotone_u hac) (gi.gc.monotone_u hbc)

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

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
s : Set α
h_sup : sSup s = ⊥
hne : s.Nonempty
⊢ s.Nonempty ∧ ∀ x ∈ s, x = ⊥

Tactic:
sSup_eq_bot

Goal state after:
α : Type u_1
inst✝ : CompleteLattice α
s : Set α
h_sup : ∀ a ∈ s, a = ⊥
hne : s.Nonempty
⊢ s.Nonempty ∧ ∀ x ∈ s, x = ⊥
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: ι : Type u_12
α : Type u_13
s : Set ι
hs : s.Nonempty
f : ι → Set α
t : Set α
this : Nonempty ↑s
⊢ ⋂ i ∈ s, f i ∩ t = (⋂ i ∈ s, f i) ∩ t

Tactic:
simp [biInter_eq_iInter, ← iInter_inter]

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

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

Tactic:
compl_compl_image

Goal state after:
α : Type u_1
S : Set (Set α)
⊢ (⋂₀ S)ᶜ = (⋂₀ S)ᶜ
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
minAx : MinimalAxioms α
a : α
s : Set α
⊢ ⨅ b ∈ s, a ⊔ b ≤
    ⨆ i,
      ⨅ j,
        match i, j with
        | { down := true }, j => a
        | { down := false }, j => ↑j

Tactic:
simp only [minAx.iSup_iInf_eq, iSup_ulift, iSup_bool_eq, le_iInf_iff]
        exact fun x ↦ biInf_le _ (x (.up false)).2

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 → α✝
⊢ ⨅ a, ⨆ b, g a b = ⨆ g_1, ⨅ a, g a (g_1 a)

Tactic:
let lhs := ⨅ a, ⨆ b, g a b

Goal state after:
α✝ : Type u
β✝ : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLinearOrder α✝
α : Type u
β : α → Type u
g : (a : α) → β a → α✝
lhs : α✝ := ⨅ a, ⨆ b, g a b
⊢ ⨅ a, ⨆ b, g a b = ⨆ g_1, ⨅ a, g a (g_1 a)
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : Frame α
s t : Set α
a✝ b✝ c✝ d a b c : α
⊢ a ⊓ (b ⊔ c) ≤ a ⊓ b ⊔ a ⊓ c

Tactic:
← sSup_pair,

Goal state after:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : Frame α
s t : Set α
a✝ b✝ c✝ d a b c : α
⊢ a ⊓ sSup {b, c} ≤ a ⊓ b ⊔ a ⊓ c
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : Frame α
s t : Set α
a✝ b✝ c✝ d a b c : α
⊢ a ⊓ sSup {b, c} ≤ a ⊓ b ⊔ a ⊓ c

Tactic:
← sSup_pair,

Goal state after:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : Frame α
s t : Set α
a✝ b✝ c✝ d a b c : α
⊢ a ⊓ sSup {b, c} ≤ sSup {a ⊓ b, a ⊓ c}
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι✝ : Sort u_4
ι : Type u_5
α : ι → Type u_6
inst✝ : (i : ι) → ConditionallyCompleteLattice (α i)
x✝¹ : Set ((i : ι) → α i)
hn : x✝¹.Nonempty
hb : BddAbove x✝¹
x✝ : ι
⊢ IsLUB (eval x✝ '' x✝¹) (sSup x✝¹ x✝)

Tactic:
by
    rw [sSup_apply_eq_sSup_image]
    exact isLUB_csSup (image_nonempty.mpr hn) ((monotone_eval _).map_bddAbove hb)

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
inst✝ : CompleteBooleanAlgebra α
s : Set α
hs : s.Nonempty
a : α
this : Nonempty ↑s
⊢ (⨆ a, ↑a) ∆ a ≤ ⨆ a_1, ↑a_1 ∆ a

Tactic:
exact iSup_symmDiff_le

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

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s t : Set α
⊢ sSup (s ∪ t) ≤ max (sSup s) (sSup t)

Tactic:
by
  rcases s.eq_empty_or_nonempty with (rfl | hs)
  · simp
  rcases t.eq_empty_or_nonempty with (rfl | ht)
  · simp
  by_cases BddAbove (s ∪ t) <;>
    grind [csSup_union, bddAbove_union, csSup_of_not_bddAbove]

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

Goal state before:
pp: case pos.none
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∈ s
ha : none ∈ upperBounds s
⊢ ⊤ ≤ none

Tactic:
exact le_rfl

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

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

Tactic:
exact le_rfl

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ Ici a ∩ (Ioi b)ᶜ = Icc a b

Tactic:
compl_Ioi,

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ Ici a ∩ Iic b = Icc a b
Module: Mathlib.Order.Interval.Set.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ Ioi a ∩ (Ioi b)ᶜ = Ioc a b

Tactic:
compl_Ioi,

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ Ioi a ∩ Iic b = Ioc a b
Module: Mathlib.Order.Interval.Set.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c d : α
hab : a < b ∨ c < d
h : Ioc a b = Ioc c d
⊢ a = c ∧ b = d

Tactic:
have : b ≤ d ∧ c ≤ a := (Ioc_subset_Ioc_iff (show a < b by grind [Set.nonempty_Ioc])).1 h.subset

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
hab : a < b ∨ c < d
h : Ioc a b = Ioc c d
this : b ≤ d ∧ c ≤ a
⊢ a = c ∧ b = d
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case pos.top
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
inst✝ : ConditionallyCompleteLattice α
S : Set (WithTop (WithBot α))
h₁ : S ⊆ {⊤}
haS : ⊤ ∈ S
⊢ ⊤ ≤ ⊤

Tactic:
exact le_rfl

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a✝ b c✝ a c : α
h : b ∈ [[a, c]]
hac : a ≤ c
⊢ Ι a b ∪ Ι b c = Ι a c

Tactic:
rw [uIcc_of_le hac] at h

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a✝ b c✝ a c : α
h : b ∈ Icc a c
hac : a ≤ c
⊢ Ι a b ∪ Ι b c = Ι a c
Module: Mathlib.Order.Antichain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
inst✝ : Std.Trichotomous r
h : IsAntichain r s
⊢ s.Subsingleton

Tactic:
rintro a ha b hb
  obtain hab | hab | hab := trichotomous_of r a b
  · exact h.eq ha hb hab
  · exact hab
  · exact h.eq' ha hb hab

Goal state after:
Module: Mathlib.Order.Preorder.Chain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
hs : IsChain r s
⊢ IsChain r (SuccChain r s)

Tactic:
by
  if h : ∃ t, IsChain r s ∧ SuperChain r s t then exact (succChain_spec h).1
  else
    rw [exists_and_left] at h
    simpa [SuccChain, dif_neg, h] using hs

Goal state after:
Module: Mathlib.Order.Preorder.Chain

Goal state before:
pp: α : Type u_1
β : Type u_2
F : Type u_3
inst✝ : LE α
s✝ t✝ : Flag α
a : α
s t : Flag α
h : s.carrier = t.carrier
⊢ s = t

Tactic:
cases s

Goal state after:
case mk
α : Type u_1
β : Type u_2
F : Type u_3
inst✝ : LE α
s t✝ : Flag α
a : α
t : Flag α
carrier✝ : Set α
Chain'✝ : IsChain (fun x1 x2 ↦ x1 ≤ x2) carrier✝
max_chain'✝ : ∀ ⦃s : Set α⦄, IsChain (fun x1 x2 ↦ x1 ≤ x2) s → carrier✝ ⊆ s → carrier✝ = s
h : { carrier := carrier✝, Chain' := Chain'✝, max_chain' := max_chain'✝ }.carrier = t.carrier
⊢ { carrier := carrier✝, Chain' := Chain'✝, max_chain' := max_chain'✝ } = t
Module: Mathlib.Tactic.NormNum.Ineq

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
num✝¹ num✝ : ℤ
da db : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h✝¹ : decide (num✝¹.mul (Int.ofNat db) ≤ num✝.mul (Int.ofNat da)) = true
h✝ : ↑(num✝¹.mul (Int.ofNat db)) ≤ ↑(num✝.mul (Int.ofNat da))
ha : 0 ≤ ⅟↑da
hb : 0 ≤ ⅟↑db
h : ⅟↑db * (↑(num✝¹.mul (Int.ofNat db)) * ⅟↑da) ≤ ⅟↑db * (↑(num✝.mul (Int.ofNat da)) * ⅟↑da)
⊢ ↑num✝¹ * ⅟↑da ≤ ↑num✝ * ⅟↑db

Tactic:
rw [← mul_assoc, Int.commute_cast] at h

Goal state after:
α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
num✝¹ num✝ : ℤ
da db : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h✝¹ : decide (num✝¹.mul (Int.ofNat db) ≤ num✝.mul (Int.ofNat da)) = true
h✝ : ↑(num✝¹.mul (Int.ofNat db)) ≤ ↑(num✝.mul (Int.ofNat da))
ha : 0 ≤ ⅟↑da
hb : 0 ≤ ⅟↑db
h : ↑(num✝¹.mul (Int.ofNat db)) * ⅟↑db * ⅟↑da ≤ ⅟↑db * (↑(num✝.mul (Int.ofNat da)) * ⅟↑da)
⊢ ↑num✝¹ * ⅟↑da ≤ ↑num✝ * ⅟↑db
Module: Mathlib.Tactic.NormNum.Ineq

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
num✝¹ num✝ : ℤ
da db : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h✝¹ : decide (num✝¹ * ↑db < num✝ * ↑da) = true
h✝ : (fun x ↦ ↑x) (num✝¹ * ↑db) < (fun x ↦ ↑x) (num✝ * ↑da)
ha : 0 < ⅟↑da
hb : 0 < ⅟↑db
h : ⅟↑db * ((fun x ↦ ↑x) (num✝¹ * ↑db) * ⅟↑da) < ⅟↑db * ((fun x ↦ ↑x) (num✝ * ↑da) * ⅟↑da)
⊢ ↑num✝¹ * ⅟↑da < ↑num✝ * ⅟↑db

Tactic:
rw [← mul_assoc, Int.commute_cast] at h

Goal state after:
α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
num✝¹ num✝ : ℤ
da db : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h✝¹ : decide (num✝¹ * ↑db < num✝ * ↑da) = true
h✝ : (fun x ↦ ↑x) (num✝¹ * ↑db) < (fun x ↦ ↑x) (num✝ * ↑da)
ha : 0 < ⅟↑da
hb : 0 < ⅟↑db
h : ↑(num✝¹ * ↑db) * ⅟↑db * ⅟↑da < ⅟↑db * ((fun x ↦ ↑x) (num✝ * ↑da) * ⅟↑da)
⊢ ↑num✝¹ * ⅟↑da < ↑num✝ * ⅟↑db
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n : ℕ
⊢ (2 * n)! ≤ (2 * n) ^ n * n !

Tactic:
Nat.two_mul,

Goal state after:
n : ℕ
⊢ (n + n)! ≤ (n + n) ^ n * n !
Module: Mathlib.Data.PNat.Basic

Goal state before:
pp: n : ℕ+
⊢ 1 + n.natPred = ↑n

Tactic:
natPred,

Goal state after:
n : ℕ+
⊢ 1 + (↑n - 1) = ↑n
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
a : α
⊢ round (a - 1) = round a - 1

Tactic:
by
  rw [← round_sub_intCast a 1, cast_one]

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

Goal state before:
pp: case mp
k m : ℕ+
h : k ∣ m
⊢ ↑k ∣ ↑m

Tactic:
rcases h with ⟨_, rfl⟩

Goal state after:
case mp
k w✝ : ℕ+
⊢ ↑k ∣ ↑(k * w✝)
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 ≤ -(fract x + ↑⌊x⌋ - ↑z)

Tactic:
add_sub_assoc,

Goal state after:
case inr
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
hx : x < ↑z
⊢ 1 - fract x ≤ -(fract x + (↑⌊x⌋ - ↑z))
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case left
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
x : R
hx : fract x ≠ 0
⊢ 0 ≤ 1 - fract x

Tactic:
le_sub_iff_add_le,

Goal state after:
case left
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
x : R
hx : fract x ≠ 0
⊢ 0 + fract x ≤ 1
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case inr.inl
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
n : ℕ
hn : 0 < ↑n
this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
m₀ : ℕ
⊢ fract (↑↑m₀ / ↑n) = ↑(↑m₀ % ↑n) / ↑n

Tactic:
exact this (natCast_nonneg m₀)

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 : R
⊢ ⌈a - 1⌉ = ⌈a⌉ - 1

Tactic:
by
  rw [eq_sub_iff_add_eq, ← ceil_add_one, sub_add_cancel]

Goal state after: