mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
l : List α
f : α → Bool
⊢ l.length = (filter f l).length + (filter (fun x ↦ !f x) l).length

Tactic:
[

Goal state after:
α : Type u
l : List α
f : α → Bool
⊢ l.length = (filter f l).length + (filter (fun x ↦ !f x) l).length
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
l : List α
p : α → Bool
⊢ map (fun a ↦ ↑a) (filter (fun x ↦ p ↑x) l.attach) = map (fun a ↦ ↑a) (map (Subtype.map id ⋯) (filter p l).attach)

Tactic:
[

Goal state after:
α : Type u
l : List α
p : α → Bool
⊢ map (fun a ↦ ↑a) (filter (fun x ↦ p ↑x) l.attach) = map (fun a ↦ ↑a) (map (Subtype.map id ⋯) (filter p l).attach)
Module: Mathlib.Data.Rat.Defs

Goal state before:
pp: q a b c : ℚ
x✝¹ : ℕ
x✝ : ℚ
⊢ ↑x✝¹.succ • x✝ = ↑x✝¹ • x✝ + x✝

Tactic:
[

Goal state after:
q a b c : ℚ
x✝¹ : ℕ
x✝ : ℚ
⊢ ↑x✝¹.succ • x✝ = ↑x✝¹ • x✝ + x✝
Module: Mathlib.Data.Rat.Defs

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

Tactic:
[

Goal state after:
q a b c : ℚ
x✝¹ : ℕ
x✝ : ℚ
⊢ Int.negSucc x✝¹ • x✝ = -(↑x✝¹.succ • x✝)
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
a : α
l : List α
this : (fun x ↦ a == x) = fun x ↦ f a == f x
⊢ map f (eraseP (fun x ↦ a == x) l) = map f (eraseP ((fun x ↦ f a == x) ∘ f) l)

Tactic:
this

Goal state after:
α : Type u
β : Type v
inst✝³ : BEq α
inst✝² : LawfulBEq α
inst✝¹ : BEq β
inst✝ : LawfulBEq β
f : α → β
finj : Injective f
a : α
l : List α
this : (fun x ↦ a == x) = fun x ↦ f a == f x
⊢ map f (eraseP (fun x ↦ f a == f x) l) = map f (eraseP ((fun x ↦ f a == x) ∘ f) l)
Module: Mathlib.Data.Rat.Defs

Goal state before:
pp: q : ℚ
h : (q.den == 1) = true
⊢ q = ↑q.num

Tactic:
Nat.beq_eq_true_eq

Goal state after:
q : ℚ
h : q.den = 1
⊢ q = ↑q.num
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
p : α → Prop
ys✝ : List α
head✝ : α
tail✝ : List α
⊢ Forall p (head✝ :: tail✝ ++ ys✝) ↔ Forall p (head✝ :: tail✝) ∧ Forall p ys✝

Tactic:
by simp [forall_append, and_assoc]

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

Goal state before:
pp: α : Type u
l₁ l₂ l : List α
p : l₁ ~ l₂
⊢ l₁.Disjoint l ↔ l₂.Disjoint l

Tactic:
[

Goal state after:
α : Type u
l₁ l₂ l : List α
p : l₁ ~ l₂
⊢ l₁.Disjoint l ↔ l₂.Disjoint l
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
l₁ l₂ l : List α
p : l₁ ~ l₂
⊢ l.Disjoint l₁ ↔ l.Disjoint l₂

Tactic:
[

Goal state after:
α : Type u
l₁ l₂ l : List α
p : l₁ ~ l₂
⊢ l.Disjoint l₁ ↔ l.Disjoint l₂
Module: Mathlib.Algebra.Order.Ring.Unbundled.Rat

Goal state before:
pp: q : ℚ
⊢ |q| = { num := |q.num|, den := q.den, den_nz := ⋯, reduced := ⋯ }

Tactic:
by
  refine ext ?_ ?_ <;>
    simp [Int.abs_eq_natAbs, abs_def,
      ← Rat.mk_eq_divInt (num := q.num.natAbs) (nz := q.den_ne_zero) (c := q.reduced)]

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

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

Tactic:
[

Goal state after:
G : Type u_1
inst✝ : DivisionMonoid G
a x y : G
⊢ SemiconjBy a⁻¹ x⁻¹ y⁻¹ ↔ SemiconjBy a y x
Module: Mathlib.Algebra.Group.Semiconj.Basic

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

Tactic:
[

Goal state after:
G : Type u_1
inst✝ : Group G
a x y : G
⊢ SemiconjBy a⁻¹ y x ↔ SemiconjBy a x y
Module: Mathlib.Data.NNRat.Defs

Goal state before:
pp: a : ℕ
ha : a ≠ 0
n d : ℕ
⊢ divNat (a * n) (a * d) = divNat n d

Tactic:
by
  ext; push_cast; exact Rat.divInt_mul_left (mod_cast ha)

Goal state after:
Module: Mathlib.Algebra.Divisibility.Units

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a u : α
hu : IsUnit u
⊢ u ∣ a

Tactic:
by
  rcases hu with ⟨u, rfl⟩
  apply Units.coe_dvd

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

Goal state before:
pp: G : Type u_1
inst✝ : DivisionMonoid G
a b c d : G
hbd : Commute b d
hbc : Commute b⁻¹ c
⊢ a / b * (c / d) = a * c / (b * d)

Tactic:
[

Goal state after:
G : Type u_1
inst✝ : DivisionMonoid G
a b c d : G
hbd : Commute b d
hbc : Commute b⁻¹ c
⊢ a / b * (c / d) = a * c / (b * d)
Module: Mathlib.Algebra.Group.Commute.Basic

Goal state before:
pp: G : Type u_1
inst✝ : DivisionMonoid G
a b c d : G
hbc : Commute b c
hbd : Commute b⁻¹ d
hcd : Commute c⁻¹ d
⊢ a / b / (c / d) = a / c / (b / d)

Tactic:
[

Goal state after:
G : Type u_1
inst✝ : DivisionMonoid G
a b c d : G
hbc : Commute b c
hbd : Commute b⁻¹ d
hcd : Commute c⁻¹ d
⊢ a / b / (c / d) = a / c / (b / d)
Module: Mathlib.Data.PNat.Defs

Goal state before:
pp: case zero
m k : ℕ+
⊢ ↑(k.modDivAux 0 (↑m / ↑k)).fst = if 0 = 0 then ↑k else 0

Tactic:
rw [if_pos rfl]
    rfl

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

Goal state before:
pp: case zero
m k : ℕ+
⊢ (k.modDivAux 0 (↑m / ↑k)).snd = if 0 = 0 then ↑m / ↑k - 1 else ↑m / ↑k

Tactic:
rw [if_pos rfl]
    rfl

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

Goal state before:
pp: α : Type u_3
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n₁ : ℤ
d₁ : ℕ
d₁0 : d₁ ≠ 0
c₁ : n₁.natAbs.Coprime d₁
n₂ : ℤ
d₂ : ℕ
d₂0 : d₂ ≠ 0
c₂ : n₂.natAbs.Coprime d₂
d₁a : ↑d₁ ≠ 0
d₂a : ↑d₂ ≠ 0
h : ↑n₁ / ↑d₁ * ↑d₂ = ↑n₂
⊢ n₁ /. ↑d₁ = n₂ /. ↑d₂

Tactic:
division_def,

Goal state after:
α : Type u_3
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n₁ : ℤ
d₁ : ℕ
d₁0 : d₁ ≠ 0
c₁ : n₁.natAbs.Coprime d₁
n₂ : ℤ
d₂ : ℕ
d₂0 : d₂ ≠ 0
c₂ : n₂.natAbs.Coprime d₂
d₁a : ↑d₁ ≠ 0
d₂a : ↑d₂ ≠ 0
h : ↑n₁ * (↑d₁)⁻¹ * ↑d₂ = ↑n₂
⊢ n₁ /. ↑d₁ = n₂ /. ↑d₂
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: n : ℕ
⊢ IsSquare ↑n ↔ IsSquare n

Tactic:
[

Goal state after:
n : ℕ
⊢ IsSquare ↑n ↔ IsSquare n
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: z : ℤ
⊢ IsSquare ↑z ↔ IsSquare z

Tactic:
[

Goal state after:
z : ℤ
⊢ IsSquare ↑z ↔ IsSquare z
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: α : Type u_3
inst✝ : DivisionSemiring α
a b : ℕ
hb : ↑b ≠ 0
d : ℕ
h : d ≠ 0
n : ℕ
c : (↑n).natAbs.Coprime d
hn : 0 ≤ { num := ↑n, den := d, den_nz := h, reduced := c }
e : divNat a b = ⟨{ num := ↑n, den := d, den_nz := h, reduced := c }, hn⟩
hd : ↑d ≠ 0
hb' : b ≠ 0
⊢ ↑⟨{ num := ↑n, den := d, den_nz := h, reduced := c }, hn⟩ = ↑a / ↑b

Tactic:
[

Goal state after:
α : Type u_3
inst✝ : DivisionSemiring α
a b : ℕ
hb : ↑b ≠ 0
d : ℕ
h : d ≠ 0
n : ℕ
c : (↑n).natAbs.Coprime d
hn : 0 ≤ { num := ↑n, den := d, den_nz := h, reduced := c }
e : divNat a b = ⟨{ num := ↑n, den := d, den_nz := h, reduced := c }, hn⟩
hd : ↑d ≠ 0
hb' : b ≠ 0
⊢ ↑⟨{ num := ↑n, den := d, den_nz := h, reduced := c }, hn⟩ = ↑a / ↑b
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: α : Type u_3
inst✝ : DivisionRing α
p q : ℚ
hp : ↑p.den ≠ 0
hq : ↑q.den ≠ 0
⊢ ↑(p - q) = ↑p - ↑q

Tactic:
simp [sub_eq_add_neg, cast_add_of_ne_zero, hp, hq]

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

Goal state before:
pp: case right
a b c d : ℤ
hb0 : 0 < b
hd0 : 0 < d
h1 : a.natAbs.Coprime b.natAbs
h2 : c.natAbs.Coprime d.natAbs
h : ↑a / ↑b = ↑c / ↑d
⊢ b = d

Tactic:
· rw [← den_div_eq_of_coprime hb0 h1, h, den_div_eq_of_coprime hd0 h2]

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:
[

Goal state after:
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
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: a : ℕ
ha0 : 0 < a
⊢ ↑(↑a)⁻¹.den = ↑a

Tactic:
← Int.cast_natCast a,

Goal state after:
a : ℕ
ha0 : 0 < a
⊢ ↑(↑↑a)⁻¹.den = ↑a
Module: Mathlib.Tactic.NormNum.Pow

Goal state before:
pp: a b c b' c' : ℕ
h1 : a.pow b' = c'
hb : 2 * b' = b
hc : c' * c' = c
⊢ (-Int.ofNat a).pow (2 * b') = Int.ofNat c

Tactic:
Int.pow_eq,

Goal state after:
a b c b' c' : ℕ
h1 : a.pow b' = c'
hb : 2 * b' = b
hc : c' * c' = c
⊢ (-Int.ofNat a) ^ (2 * b') = Int.ofNat c
Module: Mathlib.Tactic.NormNum.Pow

Goal state before:
pp: a b c b' c' : ℕ
h1 : a.pow b' = c'
hb : 2 * b' + 1 = b
hc : c' * (c' * a) = c
⊢ (-Int.ofNat a).pow (2 * b' + 1) = -Int.ofNat c

Tactic:
Int.pow_eq,

Goal state after:
a b c b' c' : ℕ
h1 : a.pow b' = c'
hb : 2 * b' + 1 = b
hc : c' * (c' * a) = c
⊢ (-Int.ofNat a) ^ (2 * b' + 1) = -Int.ofNat c
Module: Mathlib.Algebra.Order.Field.Canonical

Goal state before:
pp: α : Type u_1
inst✝⁵ : Semifield α
inst✝⁴ : LinearOrder α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
⊢ (a - b) / c = a / c - b / c

Tactic:
[

Goal state after:
α : Type u_1
inst✝⁵ : Semifield α
inst✝⁴ : LinearOrder α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
⊢ (a - b) / c = a / c - b / c
Module: Mathlib.Data.Nat.Set

Goal state before:
pp: α : Type u_1
f : ℕ → α
⊢ {f 0} ∪ range (f ∘ succ) = range f

Tactic:
← image_singleton,

Goal state after:
α : Type u_1
f : ℕ → α
⊢ f '' {0} ∪ range (f ∘ succ) = range f
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, ?_⟩
    dsimp only
    rw [Nat.sub_add_cancel hi]

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

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

Tactic:
[

Goal state after:
α : Type u_1
inst✝ : CompleteLattice α
f : ℕ → α
k : ℕ
hf : Monotone fun n ↦ ⨅ i, ⨅ (_ : i ≥ n), f i
⊢ ⨆ n, ⨅ i, ⨅ (_ : i ≥ n), f (i + k) = ⨆ n, ⨅ i, ⨅ (_ : i ≥ n + k), f i
Module: Mathlib.Order.GaloisConnection.Basic

Goal state before:
pp: α : Type u
β : Type v
ι : Sort x
κ : ι → Sort u_1
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
l : α → β
u : β → α
gc : GaloisConnection l u
f : (i : ι) → κ i → α
⊢ l (⨆ i, ⨆ j, f i j) = ⨆ i, ⨆ j, l (f i j)

Tactic:
[

Goal state after:
α : Type u
β : Type v
ι : Sort x
κ : ι → Sort u_1
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
l : α → β
u : β → α
gc : GaloisConnection l u
f : (i : ι) → κ i → α
⊢ l (⨆ i, ⨆ j, f i j) = ⨆ i, ⨆ j, l (f i j)
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₀ : IsLUB s a₀
hb₀ : IsLUB t b₀
⊢ IsLUB (image2 l s t) (l a₀ b₀)

Tactic:
[

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₀ : IsLUB s a₀
hb₀ : IsLUB t b₀
⊢ IsLUB (image2 l s t) (l a₀ b₀)
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
⊢ IsLUB (image2 l s t) (l a₀ b₀)

Tactic:
[

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
⊢ IsLUB (image2 l s t) (l a₀ b₀)
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝ : SupSet α
g : β → α
f : ι → β
⊢ ⨆ b, g ↑b = ⨆ i, g (f i)

Tactic:
by
  rw [iSup, iSup, ← image_eq_range, ← range_comp']

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
κ : ι → Sort u_6
inst✝ : CompleteLattice α
a : α
f : (i : ι) → κ i → α
⊢ ⨆ i, ⨆ j, f i j ≤ a ↔ ∀ (i : ι) (j : κ i), f i j ≤ a

Tactic:
[

Goal state after:
α : Type u_1
ι : Sort u_4
κ : ι → Sort u_6
inst✝ : CompleteLattice α
a : α
f : (i : ι) → κ i → α
⊢ ⨆ i, ⨆ j, f i j ≤ a ↔ ∀ (i : ι) (j : κ i), f i j ≤ a
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: γ : Type u_3
ι : Sort u_5
κ : ι → Sort u_8
x : γ
s : (i : ι) → κ i → Set γ
⊢ x ∈ ⋃ i, ⋃ j, s i j ↔ ∃ i j, x ∈ s i j

Tactic:
[

Goal state after:
γ : Type u_3
ι : Sort u_5
κ : ι → Sort u_8
x : γ
s : (i : ι) → κ i → Set γ
⊢ x ∈ ⋃ i, ⋃ j, s i j ↔ ∃ i j, x ∈ s i j
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: γ : Type u_3
ι : Sort u_5
κ : ι → Sort u_8
x : γ
s : (i : ι) → κ i → Set γ
⊢ x ∈ ⋂ i, ⋂ j, s i j ↔ ∀ (i : ι) (j : κ i), x ∈ s i j

Tactic:
[

Goal state after:
γ : Type u_3
ι : Sort u_5
κ : ι → Sort u_8
x : γ
s : (i : ι) → κ i → Set γ
⊢ x ∈ ⋂ i, ⋂ j, s i j ↔ ∀ (i : ι) (j : κ i), x ∈ s i j
Module: Mathlib.Order.CompleteLattice.Basic

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

Tactic:
[

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

Goal state before:
pp: α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
s : (i : ι) → κ i → Set α
t : Set α
⊢ ⋃ i, ⋃ j, s i j ⊆ t ↔ ∀ (i : ι) (j : κ i), s i j ⊆ t

Tactic:
[

Goal state after:
α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
s : (i : ι) → κ i → Set α
t : Set α
⊢ ⋃ i, ⋃ j, s i j ⊆ t ↔ ∀ (i : ι) (j : κ i), s i j ⊆ t
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
s : Set α
t : (i : ι) → κ i → Set α
⊢ s ⊆ ⋂ i, ⋂ j, t i j ↔ ∀ (i : ι) (j : κ i), s ⊆ t i j

Tactic:
[

Goal state after:
α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
s : Set α
t : (i : ι) → κ i → Set α
⊢ s ⊆ ⋂ i, ⋂ j, t i j ↔ ∀ (i : ι) (j : κ i), s ⊆ t i j
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
s : (i : ι) → κ i → Set α
⊢ (⋃ i, ⋃ j, s i j)ᶜ = ⋂ i, ⋂ j, (s i j)ᶜ

Tactic:
[

Goal state after:
α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
s : (i : ι) → κ i → Set α
⊢ (⋃ i, ⋃ j, s i j)ᶜ = ⋂ i, ⋂ j, (s i j)ᶜ
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
s : (i : ι) → κ i → Set α
⊢ (⋂ i, ⋂ j, s i j)ᶜ = ⋃ i, ⋃ j, (s i j)ᶜ

Tactic:
[

Goal state after:
α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
s : (i : ι) → κ i → Set α
⊢ (⋂ i, ⋂ j, s i j)ᶜ = ⋃ i, ⋃ j, (s i j)ᶜ
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: β : Type u_2
ι : Sort u_5
inst✝ : Nonempty ι
x : β
t : ι → Set β
⊢ insert x (⋃ i, t i) = ⋃ i, insert x (t i)

Tactic:
[

Goal state after:
β : Type u_2
ι : Sort u_5
inst✝ : Nonempty ι
x : β
t : ι → Set β
⊢ insert x (⋃ i, t i) = ⋃ i, insert x (t i)
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: β : Type u_2
ι : Sort u_5
x : β
t : ι → Set β
⊢ insert x (⋂ i, t i) = ⋂ i, insert x (t i)

Tactic:
[

Goal state after:
β : Type u_2
ι : Sort u_5
x : β
t : ι → Set β
⊢ insert x (⋂ i, t i) = ⋂ i, insert x (t i)
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : CompleteLattice α
f : β × γ → α
s : Set β
t : Set γ
⊢ ⨆ x ∈ s ×ˢ t, f x = ⨆ a ∈ s, ⨆ b ∈ t, f (a, b)

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : CompleteLattice α
f : β × γ → α
s : Set β
t : Set γ
⊢ ⨆ x ∈ s ×ˢ t, f x = ⨆ a ∈ s, ⨆ b ∈ t, f (a, b)
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
s : (i : ι) → κ i → Set α
t : Set α
⊢ (⋃ i, ⋃ j, s i j) ∩ t = ⋃ i, ⋃ j, s i j ∩ t

Tactic:
[

Goal state after:
α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
s : (i : ι) → κ i → Set α
t : Set α
⊢ (⋃ i, ⋃ j, s i j) ∩ t = ⋃ i, ⋃ j, s i j ∩ t
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
s : Set α
t : (i : ι) → κ i → Set α
⊢ s ∪ ⋂ i, ⋂ j, t i j = ⋂ i, ⋂ j, s ∪ t i j

Tactic:
[

Goal state after:
α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
s : Set α
t : (i : ι) → κ i → Set α
⊢ s ∪ ⋂ i, ⋂ j, t i j = ⋂ i, ⋂ j, s ∪ t i j
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
s : (i : ι) → κ i → Set α
t : Set α
⊢ (⋂ i, ⋂ j, s i j) ∪ t = ⋂ i, ⋂ j, s i j ∪ t

Tactic:
[

Goal state after:
α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
s : (i : ι) → κ i → Set α
t : Set α
⊢ (⋂ i, ⋂ j, s i j) ∪ t = ⋂ i, ⋂ j, s i j ∪ t
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:
[

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

Goal state before:
pp: β : Type u_2
ι : Type u_12
x : ι → β
t : ι → Set β
⊢ ⋃ i, insert (x i) (t i) = range x ∪ ⋃ i, t i

Tactic:
[

Goal state after:
β : Type u_2
ι : Type u_12
x : ι → β
t : ι → Set β
⊢ ⋃ i, insert (x i) (t i) = range x ∪ ⋃ i, t i
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
κ : ι → Sort u_6
inst✝ : CompleteLinearOrder α
f : (i : ι) → κ i → α
⊢ ⨆ i, ⨆ j, f i j = ⊤ ↔ ∀ b < ⊤, ∃ i j, b < f i j

Tactic:
[

Goal state after:
α : Type u_1
ι : Sort u_4
κ : ι → Sort u_6
inst✝ : CompleteLinearOrder α
f : (i : ι) → κ i → α
⊢ ⨆ i, ⨆ j, f i j = ⊤ ↔ ∀ b < ⊤, ∃ i j, b < f i j
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝¹ : SupSet α
inst✝ : SupSet β
f : ι → α × β
⊢ (iSup f).swap = ⨆ i, (f i).swap

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝¹ : SupSet α
inst✝ : SupSet β
f : ι → α × β
⊢ (iSup f).swap = ⨆ i, (f i).swap
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
inst✝ : CompletelyDistribLattice α
ι : Type u_1
κ : Type u_2
f : ι → α
h : Pairwise (Disjoint on f)
s : κ → Set ι
j : κ
⊢ ⨆ i ∈ ⋂ j, s j, f i = ⨅ j, ⨆ i ∈ s j, f i

Tactic:
[

Goal state after:
α : Type u
inst✝ : CompletelyDistribLattice α
ι : Type u_1
κ : Type u_2
f : ι → α
h : Pairwise (Disjoint on f)
s : κ → Set ι
j : κ
⊢ ⨆ i ∈ ⋂ j, s j, f i = ⨅ j, ⨆ i ∈ s j, f i
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
ι : Sort u_5
inst✝ : CompleteLattice α
f : ι → α
x✝ : α
⊢ x✝ ∈ Iic (⨅ i, f i) ↔ x✝ ∈ ⋂ i, Iic (f i)

Tactic:
by simp only [mem_Iic, le_iInf_iff, mem_iInter]

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

Goal state before:
pp: α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
inst✝ : CompleteLattice α
f : (i : ι) → κ i → α
⊢ Ici (⨆ i, ⨆ j, f i j) = ⋂ i, ⋂ j, Ici (f i j)

Tactic:
[

Goal state after:
α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
inst✝ : CompleteLattice α
f : (i : ι) → κ i → α
⊢ Ici (⨆ i, ⨆ j, f i j) = ⋂ i, ⋂ j, Ici (f i j)
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
inst✝ : CompleteLattice α
f : (i : ι) → κ i → α
⊢ Iic (⨅ i, ⨅ j, f i j) = ⋂ i, ⋂ j, Iic (f i j)

Tactic:
[

Goal state after:
α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
inst✝ : CompleteLattice α
f : (i : ι) → κ i → α
⊢ Iic (⨅ i, ⨅ j, f i j) = ⋂ i, ⋂ j, Iic (f i j)
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
inst✝ : CompleteLattice β
s : ι → Set α
f : α → β
⊢ ⨆ a ∈ ⋃ i, s i, f a = ⨆ j, ⨆ i, ⨆ (_ : j ∈ s i), f j

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
ι : Sort u_5
inst✝ : CompleteLattice β
s : ι → Set α
f : α → β
⊢ ⨆ a ∈ ⋃ i, s i, f a = ⨆ j, ⨆ i, ⨆ (_ : j ∈ s i), f j
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: β : Type u_2
ι : Sort u_5
inst✝ : CompleteLattice β
t : ι → Set β
⊢ sSup (⋃ i, t i) = ⨆ i, sSup (t i)

Tactic:
[

Goal state after:
β : Type u_2
ι : Sort u_5
inst✝ : CompleteLattice β
t : ι → Set β
⊢ sSup (⋃ i, t i) = ⨆ i, sSup (t i)
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:
[

Goal state after:
α : Type u_1
S : Set (Set α)
p : α → Prop
⊢ (∀ x ∈ ⋃₀ S, p x) ↔ ∀ s ∈ S, ∀ x ∈ s, p x
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:
[

Goal state after:
α : Type u_1
S : Set (Set α)
p : α → Prop
⊢ (∃ x ∈ ⋃₀ S, p x) ↔ ∃ s ∈ S, ∃ x ∈ s, p x
Module: Mathlib.Order.LatticeIntervals

Goal state before:
pp: α : Type u_1
a : α
inst✝¹ : Lattice α
inst✝ : OrderBot α
⊢ ComplementedLattice ↑(Iic a) ↔ ∀ b ≤ a, ∃ c ≤ a, b ⊓ c = ⊥ ∧ b ⊔ c = a

Tactic:
[

Goal state after:
α : Type u_1
a : α
inst✝¹ : Lattice α
inst✝ : OrderBot α
⊢ ComplementedLattice ↑(Iic a) ↔ ∀ b ≤ a, ∃ c ≤ a, b ⊓ c = ⊥ ∧ b ⊔ c = a
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
inst✝ : Frame α
ι : Type u_1
ι' : Type u_2
f : ι → α
g : ι' → α
⊢ (⨆ i, f i) ⊓ ⨆ j, g j = ⨆ i, f i.1 ⊓ g i.2

Tactic:
[

Goal state after:
α : Type u
inst✝ : Frame α
ι : Type u_1
ι' : Type u_2
f : ι → α
g : ι' → α
⊢ (⨆ i, f i) ⊓ ⨆ j, g j = ⨆ i, f i.1 ⊓ g i.2
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:
[

Goal state after:
α : 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
Module: Mathlib.Order.CompleteBooleanAlgebra

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

Tactic:
[

Goal state after:
α : Type u
ι : Sort w
κ : ι → Sort w'
inst✝ : Frame α
a : α
f : (i : ι) → κ i → α
⊢ Disjoint a (⨆ i, ⨆ j, f i j) ↔ ∀ (i : ι) (j : κ i), Disjoint a (f i j)
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
inst✝² : Frame α
ι : Type u_1
inst✝¹ : Preorder ι
inst✝ : IsDirectedOrder ι
f g : ι → α
hf : Monotone f
hg : Monotone g
⊢ ⨆ i, f i.1 ⊓ g i.2 ≤ ⨆ i, f i ⊓ g i

Tactic:
refine iSup_mono' fun i => ?_

Goal state after:
α : Type u
inst✝² : Frame α
ι : Type u_1
inst✝¹ : Preorder ι
inst✝ : IsDirectedOrder ι
f g : ι → α
hf : Monotone f
hg : Monotone g
i : ι × ι
⊢ ∃ i', f i.1 ⊓ g i.2 ≤ f i' ⊓ g i'
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
ι : Sort w
inst✝ : CompleteBooleanAlgebra α
f g : ι → α
⊢ (⨆ i, f i) ∆ ⨆ i, g i ≤ ⨆ i, f i ∆ g i

Tactic:
[

Goal state after:
α : Type u
ι : Sort w
inst✝ : CompleteBooleanAlgebra α
f g : ι → α
⊢ (⨆ i, f i) ∆ ⨆ i, g i ≤ ⨆ i, f i ∆ g i
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case inl
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
t : Set α
hs : ∀ x ∈ ∅, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ ∅, y ≤ x
this : t = ∅
⊢ sSup ∅ = sSup t

Tactic:
this

Goal state after:
case inl
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
t : Set α
hs : ∀ x ∈ ∅, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ ∅, y ≤ x
this : t = ∅
⊢ sSup ∅ = sSup ∅
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
s_ne : s.Nonempty
hs : ∀ x ∈ s, ∃ y ∈ ∅, x ≤ y
ht : ∀ y ∈ ∅, ∃ x ∈ s, y ≤ x
this : s = ∅
⊢ sSup s = sSup ∅

Tactic:
this

Goal state after:
case inr.inl
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
s_ne : s.Nonempty
hs : ∀ x ∈ s, ∃ y ∈ ∅, x ≤ y
ht : ∀ y ∈ ∅, ∃ x ∈ s, y ≤ x
this : s = ∅
⊢ sSup ∅ = sSup ∅