mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Logic.Equiv.Set

Goal state before:
pp: α✝¹ : Sort u
β✝ : Sort v
γ : Sort w
α✝ : Type u_1
β : Type u_2
α : Type ?u.8
s t : Set α
p : α → Prop
inst✝ : DecidablePred p
hs : ∀ (x : α), x ∈ s → p x
ht : ∀ (x : α), x ∈ t → ¬p x
x✝ : ↑(s ∪ t)
x : α
h' : x ∈ s ∪ t
⊢ (fun o ↦
        match o with
        | Sum.inl x => ⟨↑x, ⋯⟩
        | Sum.inr x => ⟨↑x, ⋯⟩)
      ((fun x ↦ if hp : p ↑x then Sum.inl ⟨↑x, ⋯⟩ else Sum.inr ⟨↑x, ⋯⟩) ⟨x, h'⟩) =
    ⟨x, h'⟩

Tactic:
by_cases h : p x

Goal state after:
case pos
α✝¹ : Sort u
β✝ : Sort v
γ : Sort w
α✝ : Type u_1
β : Type u_2
α : Type ?u.8
s t : Set α
p : α → Prop
inst✝ : DecidablePred p
hs : ∀ (x : α), x ∈ s → p x
ht : ∀ (x : α), x ∈ t → ¬p x
x✝ : ↑(s ∪ t)
x : α
h' : x ∈ s ∪ t
h : p x
⊢ (fun o ↦
        match o with
        | Sum.inl x => ⟨↑x, ⋯⟩
        | Sum.inr x => ⟨↑x, ⋯⟩)
      ((fun x ↦ if hp : p ↑x then Sum.inl ⟨↑x, ⋯⟩ else Sum.inr ⟨↑x, ⋯⟩) ⟨x, h'⟩) =
    ⟨x, h'⟩

case neg
α✝¹ : Sort u
β✝ : Sort v
γ : Sort w
α✝ : Type u_1
β : Type u_2
α : Type ?u.8
s t : Set α
p : α → Prop
inst✝ : DecidablePred p
hs : ∀ (x : α), x ∈ s → p x
ht : ∀ (x : α), x ∈ t → ¬p x
x✝ : ↑(s ∪ t)
x : α
h' : x ∈ s ∪ t
h : ¬p x
⊢ (fun o ↦
        match o with
        | Sum.inl x => ⟨↑x, ⋯⟩
        | Sum.inr x => ⟨↑x, ⋯⟩)
      ((fun x ↦ if hp : p ↑x then Sum.inl ⟨↑x, ⋯⟩ else Sum.inr ⟨↑x, ⋯⟩) ⟨x, h'⟩) =
    ⟨x, h'⟩
Module: Mathlib.Logic.Equiv.Set

Goal state before:
pp: case neg
α✝¹ : Sort u
β✝¹ : Sort v
γ : Sort w
α✝ : Type u_1
β✝ : Type u_2
α : Type u
β : Type v
s : Set α
t : Set β
inst✝¹ : DecidablePred fun x ↦ x ∈ s
inst✝ : DecidablePred fun x ↦ x ∈ t
e₀ : ↑s ≃ ↑t
e : { e // ∀ (x : ↑s), e ↑x = ↑(e₀ x) }
x : α
hx : ¬x ∈ s
⊢ ↑((fun e₁ ↦ ⟨Trans.trans (Trans.trans (Set.sumCompl s).symm (e₀.sumCongr e₁)) (Set.sumCompl t), ⋯⟩)
          ((fun e ↦ (↑e).subtypeEquiv ⋯) e))
      x =
    ↑e x

Tactic:
· simp only [Set.sumCompl_symm_apply_of_notMem hx, Sum.map_inr, subtypeEquiv_apply,
        Set.sumCompl_apply_inr, trans_apply, sumCongr_apply, Trans.trans]

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

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a ≤ b
⊢ Ioo a b ∪ {a, b} = Icc a b

Tactic:
have : (Icc a b \ {a, b}) ∪ {a, b} = Icc a b := sdiff_union_of_subset fun
    | x, .inl rfl => left_mem_Icc.mpr h
    | x, .inr rfl => right_mem_Icc.mpr h
  rw [← this, Icc_sdiff_both]

Goal state after:
Module: Mathlib.Order.Hom.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
e : α ≃o β
x y : α
z : ↑(Icc x y)
⊢ e ↑z ∈ Icc (e x) (e y)

Tactic:
simp only [mem_Icc, map_le_map_iff]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
e : α ≃o β
x y : α
z : ↑(Icc x y)
⊢ x ≤ ↑z ∧ ↑z ≤ y
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 : smul tl tr = t
⊢ smul l r = t

Tactic:
by simp [prl, prr, prt]

Goal state after:
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 : smulg tl tr = t
⊢ smulg l r = t

Tactic:
by simp [prl, prr, prt]

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

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
num✝ : ℤ
denom✝ : ℕ
h : Invertible ↑denom✝
⊢ -(↑num✝ * ⅟↑denom✝) = ↑num✝.neg * ⅟↑denom✝

Tactic:
rw [← neg_mul, ← Int.cast_neg]

Goal state after:
α : Type u_1
inst✝ : Ring α
num✝ : ℤ
denom✝ : ℕ
h : Invertible ↑denom✝
⊢ ↑(-num✝) * ⅟↑denom✝ = ↑num✝.neg * ⅟↑denom✝
Module: Mathlib.Tactic.NormNum.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
f : α → α → α
a b : α
na nb nc : ℤ
da db dc k : ℕ
hf : f = HSub.hSub
ra : IsRat a na da
rb : IsRat b nb db
h₁ : (na.mul ↑db).sub (nb.mul ↑da) = (↑k).mul nc
h₂ : da.mul db = k.mul dc
⊢ IsRat (f a b) nc dc

Tactic:
rw [hf, sub_eq_add_neg]

Goal state after:
α : Type u_1
inst✝ : Ring α
f : α → α → α
a b : α
na nb nc : ℤ
da db dc k : ℕ
hf : f = HSub.hSub
ra : IsRat a na da
rb : IsRat b nb db
h₁ : (na.mul ↑db).sub (nb.mul ↑da) = (↑k).mul nc
h₂ : da.mul db = k.mul dc
⊢ IsRat (a + -b) nc dc
Module: Mathlib.Algebra.BigOperators.Group.List.Defs

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
l : List M
m : M
h : ∀ (x : M), x ∈ l → x = m
⊢ l.prod = (replicate l.length m).prod

Tactic:
← List.eq_replicate_iff.mpr ⟨rfl, h⟩

Goal state after:
M : Type u_2
inst✝ : Monoid M
l : List M
m : M
h : ∀ (x : M), x ∈ l → x = m
⊢ l.prod = l.prod
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b c : α
hc : c ≤ 0
h : b ≤ a
⊢ a / c ≤ b / c

Tactic:
by
  rw [div_eq_mul_inv a c, div_eq_mul_inv b c]
  exact mul_le_mul_of_nonpos_right h (inv_nonpos'.2 hc)

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

Goal state before:
pp: case neg
α : 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
⊢ Forall₂ R (filter p (a :: as)) (filter q (b :: bs))

Tactic:
have : ¬q b := by rwa [← hpq h₁]

Goal state after:
case neg
α : 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))
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ : List β
h : ∃ l, Forall₂ R l₁ l ∧ l <+ l₂
⊢ SublistForall₂ R l₁ l₂

Tactic:
obtain ⟨l, hl1, hl2⟩ := h
    revert l₁
    induction hl2 with
    | slnil =>
      intro l₁ hl1
      rw [forall₂_nil_right_iff.1 hl1]
      exact SublistForall₂.nil
    | cons _ _ ih => intro l₁ hl1; exact SublistForall₂.cons_right (ih hl1)
    | cons_cons _ _ ih =>
      intro l₁ hl1
      obtain - | ⟨hr, hl⟩ := hl1
      exact SublistForall₂.cons hr (ih hl)

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

Goal state before:
pp: case cons.nil
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
inst✝ : IsTrans α Rₐ
head✝ : α
tail✝ : List α
ih : ∀ (a b : List α), SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b tail✝ → SublistForall₂ Rₐ a tail✝
a : List α
h1 : SublistForall₂ Rₐ a []
⊢ SublistForall₂ Rₐ a (head✝ :: tail✝)

pp: case cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
inst✝ : IsTrans α Rₐ
head✝ : α
tail✝ : List α
ih : ∀ (a b : List α), SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b tail✝ → SublistForall₂ Rₐ a tail✝
a : List α
a₁✝ : α
l₁✝ : List α
h1 : SublistForall₂ Rₐ a (a₁✝ :: l₁✝)
hbc : Rₐ a₁✝ head✝
tbc : SublistForall₂ Rₐ l₁✝ tail✝
⊢ SublistForall₂ Rₐ a (head✝ :: tail✝)

pp: case cons.cons_right
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
inst✝ : IsTrans α Rₐ
head✝ : α
tail✝ : List α
ih : ∀ (a b : List α), SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b tail✝ → SublistForall₂ Rₐ a tail✝
a b : List α
h1 : SublistForall₂ Rₐ a b
btc : SublistForall₂ Rₐ b tail✝
⊢ SublistForall₂ Rₐ a (head✝ :: tail✝)

Tactic:
· cases h1
        exact SublistForall₂.nil

Goal state after:
case cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
inst✝ : IsTrans α Rₐ
head✝ : α
tail✝ : List α
ih : ∀ (a b : List α), SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b tail✝ → SublistForall₂ Rₐ a tail✝
a : List α
a₁✝ : α
l₁✝ : List α
h1 : SublistForall₂ Rₐ a (a₁✝ :: l₁✝)
hbc : Rₐ a₁✝ head✝
tbc : SublistForall₂ Rₐ l₁✝ tail✝
⊢ SublistForall₂ Rₐ a (head✝ :: tail✝)

case cons.cons_right
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
inst✝ : IsTrans α Rₐ
head✝ : α
tail✝ : List α
ih : ∀ (a b : List α), SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b tail✝ → SublistForall₂ Rₐ a tail✝
a b : List α
h1 : SublistForall₂ Rₐ a b
btc : SublistForall₂ Rₐ b tail✝
⊢ SublistForall₂ Rₐ a (head✝ :: tail✝)
Module: Mathlib.Data.List.Basic

Goal state before:
pp: case nil
α : Type u
n : ℕ
h : n.succ ≠ 0
⊢ (replicate n.succ []).flatten.head? = [].head?

Tactic:
simp [replicate]

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

Goal state before:
pp: case cons
α : Type u
n : ℕ
h : n.succ ≠ 0
head✝ : α
tail✝ : List α
tail_ih✝ : (replicate n.succ tail✝).flatten.head? = tail✝.head?
⊢ (replicate n.succ (head✝ :: tail✝)).flatten.head? = (head✝ :: tail✝).head?

Tactic:
simp [replicate]

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

Goal state before:
pp: α : Type u
a b : α
l : List α
c : α
hc : c ∈ (a :: b :: l).getLast?
⊢ (a :: b :: l).dropLast ++ [c] = a :: b :: l

Tactic:
rw [getLast?_cons_cons] at hc

Goal state after:
α : Type u
a b : α
l : List α
c : α
hc : c ∈ (b :: l).getLast?
⊢ (a :: b :: l).dropLast ++ [c] = a :: b :: l
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : Ring M
x₁ x₂ X₁ X₂ Y y a : M
h₁ : x₁ = a * X₁
h₂ : x₂ = a * X₂
H_atom : X₁ - X₂ = Y
hy : a * Y = y
⊢ x₁ - x₂ = y

Tactic:
subst h₁ h₂ H_atom hy
  simp [mul_sub]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
l : List M
i : ℕ
hlen : i < l.length
hcomm : ∀ (a' : M), a' ∈ take i l → Commute l[i] a'
⊢ l[i] * (l.eraseIdx i).prod = l.prod

Tactic:
by
  rw [← prod_insertIdx (by grind : i ≤ (l.eraseIdx i).length) (fun a' a'_mem =>
      hcomm a' (by rwa [take_eraseIdx_eq_take_of_le l i i (Nat.le_refl i)] at a'_mem)),
    insertIdx_eraseIdx_getElem hlen]

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

Goal state before:
pp: α : Type u
l₁ l₂ : List α
⊢ l₁ = l₂ → ∀ (n : ℕ), n < max l₁.length l₂.length → l₁[n]? = l₂[n]?

Tactic:
rintro rfl _ _; rfl

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

Goal state before:
pp: M : Type u_1
inst✝ : CommGroupWithZero M
l : NF M
⊢ l⁻¹.eval = l.eval⁻¹

Tactic:
simp +instances only [NF.eval, List.map_map, NF.instInv, List.prod_inv]
  congr! 2
  ext p
  simp [zpow'_neg]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: G : Type u_7
inst✝ : DivInvMonoid G
a b : G
l : List G
⊢ (a :: b :: l).alternatingProd = a / b * l.alternatingProd

Tactic:
rw [div_eq_mul_inv, alternatingProd_cons_cons']

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

Goal state before:
pp: α : Type u
β : Type v
f g : α → Option β
l : List α
h : ∀ (x : α), x ∈ l → f x = g x
⊢ filterMap f l = filterMap g l

Tactic:
induction l <;> simp_all [filterMap_cons]

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

Goal state before:
pp: q a b c : ℚ
x✝¹ : ℕ
x✝ : ℚ
⊢ ↑(Int.negSucc x✝¹) * x✝ = -(↑↑x✝¹.succ * x✝)

Tactic:
Int.negSucc_eq,

Goal state after:
q a b c : ℚ
x✝¹ : ℕ
x✝ : ℚ
⊢ ↑(-(↑x✝¹ + 1)) * x✝ = -(↑↑x✝¹.succ * x✝)
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
⊢ (j :: L).length ≤ (j :: L).sum

Tactic:
| cons j L IH =>

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

Goal state before:
pp: ι : Type u_1
inst✝¹ : BEq ι
inst✝ : LawfulBEq ι
l : List ι
i : ℕ
hi : i < l.length
⊢ l.erase l[i] ~ l.eraseIdx i

Tactic:
by
  induction l generalizing i with
  | nil => simp
  | cons a l IH => cases i with grind

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

Goal state before:
pp: a : ℚ
ha : 0 ≤ a
⊢ 0 ≤ a⁻¹

Tactic:
inv_def

Goal state after:
a : ℚ
ha : 0 ≤ a
⊢ 0 ≤ ↑a.den /. a.num
Module: Mathlib.Algebra.GroupWithZero.Divisibility

Goal state before:
pp: α : Type u_1
inst✝ : MonoidWithZero α
p q : α
h₁ : q ≠ 0
h₂ : p ∣ q
⊢ p ≠ 0

Tactic:
rcases h₂ with ⟨u, rfl⟩

Goal state after:
α : Type u_1
inst✝ : MonoidWithZero α
p u : α
h₁ : p * u ≠ 0
⊢ p ≠ 0
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: α : Type u_3
inst✝ : DivisionRing α
n : ℤ
⊢ ↑n / ↑1 = ↑n

Tactic:
Nat.cast_one,

Goal state after:
α : Type u_3
inst✝ : DivisionRing α
n : ℤ
⊢ ↑n / 1 = ↑n
Module: Mathlib.Tactic.NormNum.Pow

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
an : ℤ
ad b : ℕ
inv✝ : Invertible ↑ad
this : Invertible (↑ad ^ b)
⊢ IsRat ((↑an * ⅟↑ad) ^ b) (an ^ b) (ad ^ b)

Tactic:
rw [← Nat.cast_pow] at this

Goal state after:
α : Type u_1
inst✝ : Ring α
an : ℤ
ad b : ℕ
inv✝ : Invertible ↑ad
this : Invertible ↑(ad ^ b)
⊢ IsRat ((↑an * ⅟↑ad) ^ b) (an ^ b) (ad ^ b)
Module: Mathlib.Tactic.NormNum.Pow

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
an ad b : ℕ
inv✝ : Invertible ↑ad
this : Invertible (↑ad ^ b)
⊢ IsNNRat ((↑an * ⅟↑ad) ^ b) (an ^ b) (ad ^ b)

Tactic:
rw [← Nat.cast_pow] at this

Goal state after:
α : Type u_1
inst✝ : Semiring α
an ad b : ℕ
inv✝ : Invertible ↑ad
this : Invertible ↑(ad ^ b)
⊢ IsNNRat ((↑an * ⅟↑ad) ^ b) (an ^ b) (ad ^ b)
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a b₂ b₁ : R
⊢ a + (b₁ + b₂) = b₁ + (a + b₂)

Tactic:
simp [add_left_comm]

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

Goal state before:
pp: R : Type u
inst✝⁶ : NonUnitalNonAssocSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : CanonicallyOrderedAdd R
inst✝³ : Sub R
inst✝² : OrderedSub R
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : MulRightMono R
a b c : R
h : AddLECancellable (b * c)
⊢ (a - b) * c = a * c - b * c

Tactic:
by
  obtain (hab | hba) := total_of (· ≤ ·) a b
  · rw [tsub_eq_zero_iff_le.2 hab, zero_mul, tsub_eq_zero_iff_le.2 (mul_le_mul_left hab c)]
  · apply h.eq_tsub_of_add_eq
    rw [← add_mul, tsub_add_cancel_of_le hba]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
s : Set α
f : α → β
hf : Monotone f
⊢ ⨆ a ∈ s, f a ≤ f (sSup s)

Tactic:
rw [sSup_eq_iSup]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
s : Set α
f : α → β
hf : Monotone f
⊢ ⨆ a ∈ s, f a ≤ f (⨆ a ∈ s, a)
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
β : Type u_2
t : α → Set β
h : Pairwise (Disjoint on t)
a₁ : α
b₁ : β
h₁ : b₁ ∈ t a₁
a₂ : α
b₂ : β
h₂ : b₂ ∈ t a₂
eq : sigmaToiUnion t ⟨a₁, ⟨b₁, h₁⟩⟩ = sigmaToiUnion t ⟨a₂, ⟨b₂, h₂⟩⟩
b_eq : b₁ = b₂
a_eq : a₁ = a₂
⊢ ↑(Eq.recOn a_eq ⟨a₁, ⟨b₁, h₁⟩⟩.snd) = ↑⟨a₂, ⟨b₂, h₂⟩⟩.snd

Tactic:
subst b_eq

Goal state after:
α : Type u_1
β : Type u_2
t : α → Set β
h : Pairwise (Disjoint on t)
a₁ : α
b₁ : β
h₁ : b₁ ∈ t a₁
a₂ : α
a_eq : a₁ = a₂
h₂ : b₁ ∈ t a₂
eq : sigmaToiUnion t ⟨a₁, ⟨b₁, h₁⟩⟩ = sigmaToiUnion t ⟨a₂, ⟨b₁, h₂⟩⟩
⊢ ↑(Eq.recOn a_eq ⟨a₁, ⟨b₁, h₁⟩⟩.snd) = ↑⟨a₂, ⟨b₁, h₂⟩⟩.snd
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
S : Set (Set α)
p : α → Prop
⊢ (∀ x ∈ ⋃₀ S, p x) ↔ ∀ s ∈ S, ∀ x ∈ s, p x

Tactic:
← iInf_Prop_eq,

Goal state after:
α : Type u_1
S : Set (Set α)
p : α → Prop
⊢ ⨅ i ∈ ⋃₀ S, p i ↔ ⨅ i ∈ S, ⨅ i_2 ∈ i, p i_2
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
ι : Sort w
inst✝ : Frame α
a : α
f : ι → α
b : α
⊢ b ≤ (⨆ x, f x) ⇨ a ↔ b ≤ ⨅ x, f x ⇨ a

Tactic:
simp [inf_iSup_eq]

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
minAx : CompletelyDistribLattice.MinimalAxioms β
f : α → β
hf : Injective f
map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a
map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a
ι✝ : Type u
κ✝ : ι✝ → Type u
g : (a : ι✝) → κ✝ a → α
⊢ ⨅ i, ⨆ a ∈ range fun b ↦ g i b, f a = ⨆ a ∈ range fun g_1 ↦ sInf (range fun a ↦ g a (g_1 a)), f a

Tactic:
iSup_range,

Goal state after:
α : Type u
β : Type v
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
minAx : CompletelyDistribLattice.MinimalAxioms β
f : α → β
hf : Injective f
map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a
map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a
ι✝ : Type u
κ✝ : ι✝ → Type u
g : (a : ι✝) → κ✝ a → α
⊢ ⨅ i, ⨆ i_1, f (g i i_1) = ⨆ i, f (sInf (range fun a ↦ g a (i a)))
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝¹² : Max α
inst✝¹¹ : Min α
inst✝¹⁰ : LE α
inst✝⁹ : LT α
inst✝⁸ : SupSet α
inst✝⁷ : InfSet α
inst✝⁶ : Top α
inst✝⁵ : Bot α
inst✝⁴ : Compl α
inst✝³ : HImp α
inst✝² : HNot α
inst✝¹ : SDiff α
inst✝ : CompletelyDistribLattice β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a
map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
map_compl : ∀ (a : α), f aᶜ = (f a)ᶜ
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
map_hnot : ∀ (a : α), f (￢a) = ￢f a
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
ι✝ : Type u
κ✝ : ι✝ → Type u
g : (a : ι✝) → κ✝ a → α
⊢ ⨅ i, ⨆ a ∈ range fun b ↦ g i b, f a = ⨆ a ∈ range fun g_1 ↦ sInf (range fun a ↦ g a (g_1 a)), f a

Tactic:
iSup_range,

Goal state after:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝¹² : Max α
inst✝¹¹ : Min α
inst✝¹⁰ : LE α
inst✝⁹ : LT α
inst✝⁸ : SupSet α
inst✝⁷ : InfSet α
inst✝⁶ : Top α
inst✝⁵ : Bot α
inst✝⁴ : Compl α
inst✝³ : HImp α
inst✝² : HNot α
inst✝¹ : SDiff α
inst✝ : CompletelyDistribLattice β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a
map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
map_compl : ∀ (a : α), f aᶜ = (f a)ᶜ
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
map_hnot : ∀ (a : α), f (￢a) = ￢f a
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
ι✝ : Type u
κ✝ : ι✝ → Type u
g : (a : ι✝) → κ✝ a → α
⊢ ⨅ i, ⨆ i_1, f (g i i_1) = ⨆ i, f (sInf (range fun a ↦ g a (i a)))
Module: Mathlib.Order.Interval.Set.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ Ici a ∩ Iic b = Icc a b

Tactic:
Ici_inter_Iic

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

Goal state before:
pp: case mpr.inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a b c : α
hab : a ≤ b
hbc : b ≤ c
hfab : f a < f b
hfcb : f c < f b
⊢ ∃ a b, ∃ c ∈ [[a, b]], f c ∉ [[f a, f b]]

pp: case mpr.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a b c : α
hab : a ≤ b
hbc : b ≤ c
hfba : f b < f a
hfbc : f b < f c
⊢ ∃ a b, ∃ c ∈ [[a, b]], f c ∉ [[f a, f b]]

Tactic:
· exact ⟨a, c, b, Icc_subset_uIcc ⟨hab, hbc⟩, fun h => h.2.not_gt <| max_lt hfab hfcb⟩

Goal state after:
case mpr.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a b c : α
hab : a ≤ b
hbc : b ≤ c
hfba : f b < f a
hfbc : f b < f c
⊢ ∃ a b, ∃ c ∈ [[a, b]], f c ∉ [[f a, f b]]
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: case inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h : ∀ (x : α), x ∈ (fun b ↦ Ι b a) b ↔ x ∈ (fun b ↦ Ι b a) c
ha : a < b
⊢ b = c

Tactic:
refine
      eq_of_mem_uIoc_of_mem_uIoc ((h _).1 <| left_mem_uIoc.2 ha)
        ((h _).2 <| left_mem_uIoc.2 <| ha.trans_le ?_)

Goal state after:
case inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h : ∀ (x : α), x ∈ (fun b ↦ Ι b a) b ↔ x ∈ (fun b ↦ Ι b a) c
ha : a < b
⊢ b ≤ c
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ uIoo a b = uIoo b a

Tactic:
simp_rw [uIoo, inf_comm, sup_comm]

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

Goal state before:
pp: A : Type u_1
B : Type u_2
i : SetLike A B
inst✝ : Subsingleton B
S : A
h : Nonempty ↥S
b : B
⊢ b ∈ S

Tactic:
obtain ⟨s, hs⟩ := nonempty_subtype.mp h

Goal state after:
A : Type u_1
B : Type u_2
i : SetLike A B
inst✝ : Subsingleton B
S : A
h : Nonempty ↥S
b s : B
hs : s ∈ S
⊢ b ∈ S
Module: Mathlib.Algebra.Order.Nonneg.Ring

Goal state before:
pp: α : Type u_1
inst✝³ : Nontrivial α
inst✝² : AddGroup α
inst✝¹ : LinearOrder α
inst✝ : AddLeftMono α
⊢ Nontrivial { x // 0 ≤ x }

Tactic:
have ⟨a, ha⟩ := exists_ne (0 : α)

Goal state after:
α : Type u_1
inst✝³ : Nontrivial α
inst✝² : AddGroup α
inst✝¹ : LinearOrder α
inst✝ : AddLeftMono α
a : α
ha : a ≠ 0
⊢ Nontrivial { x // 0 ≤ x }
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : Group α
inst✝ : MulLeftMono α
a b : α
hpos : a⁺ᵐ = b⁺ᵐ
hneg : a⁻ᵐ = b⁻ᵐ
⊢ b⁺ᵐ / a⁻ᵐ = b⁺ᵐ / b⁻ᵐ

Tactic:
hneg

Goal state after:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : Group α
inst✝ : MulLeftMono α
a b : α
hpos : a⁺ᵐ = b⁺ᵐ
hneg : a⁻ᵐ = b⁻ᵐ
⊢ b⁺ᵐ / b⁻ᵐ = b⁺ᵐ / b⁻ᵐ
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : One M
i j : ι
a b : M
ha : a ≠ 1
hb : b ≠ 1
⊢ Disjoint {i} (mulSupport (mulSingle j b)) ↔ i ≠ j

Tactic:
mulSupport_mulSingle_of_ne hb,

Goal state after:
ι : Type u_1
M : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : One M
i j : ι
a b : M
ha : a ≠ 1
hb : b ≠ 1
⊢ Disjoint {i} {j} ↔ i ≠ j
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: k : ℕ
⊢ (1 + k) * ascFactorial 1 k = (k + 1)!

Tactic:
one_ascFactorial k,

Goal state after:
k : ℕ
⊢ (1 + k) * k ! = (k + 1)!
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:
← round_add_intCast a 1,

Goal state after:
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
a : α
⊢ round (a + 1) = round (a + ↑1)
Module: Mathlib.Data.PNat.Basic

Goal state before:
pp: n : ℕ+
a : ℕ
h : a ∣ ↑n
⊢ 0 < a

Tactic:
apply pos_iff_ne_zero.2
  intro hzero
  rw [hzero] at h
  exact PNat.ne_zero n (eq_zero_of_zero_dvd h)

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

Goal state before:
pp: R : Type u_4
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
x k : R
hk : 1 < k
n : ℤ
hn : k * x = k * ↑n + 1
hk0 : 0 < k
⊢ ↑n ≤ x ∧ x < ↑n + 1

Tactic:
← mul_le_mul_iff_right₀ hk0,

Goal state after:
R : Type u_4
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
x k : R
hk : 1 < k
n : ℤ
hn : k * x = k * ↑n + 1
hk0 : 0 < k
⊢ k * ↑n ≤ k * x ∧ x < ↑n + 1
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case succ
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
c : ℕ
z : ℤ
hz : fract a * ↑c - fract (a * ↑c) = ↑z
⊢ ∃ z, fract a * ↑c + fract a * ↑1 - fract (a * ↑c + a * ↑1) = ↑z

Tactic:
Nat.cast_one,

Goal state after:
case succ
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
c : ℕ
z : ℤ
hz : fract a * ↑c - fract (a * ↑c) = ↑z
⊢ ∃ z, fract a * ↑c + fract a * 1 - fract (a * ↑c + a * 1) = ↑z
Module: Mathlib.Algebra.Order.Floor.Ring

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

Tactic:
intro l

Goal state after:
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
m : ℤ
n : ℕ
hn : 0 < ↑n
l : ℤ
⊢ 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case inr.inr.calc_2.e_a
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₀ : ℕ
q : ℤ := ⌈↑m₀ / ↑n⌉
m₁ : ℤ := q * ↑n - ↑m₀
hm₁ : 0 ≤ m₁
⊢ (q * ↑n - ↑m₀) % ↑n = -↑m₀ % ↑n

Tactic:
rw [sub_eq_add_neg, add_comm (q * ↑n), add_mul_emod_self_right]

Goal state after: