mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

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

Tactic:
alternatingProd_cons' b l,

Goal state after:
G : Type u_7
inst✝ : CommGroup G
a b : G
l : List G
⊢ a * b⁻¹ * l.alternatingProd = a * (b * l.alternatingProd⁻¹)⁻¹
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: case cons
n a : ℕ
l : List ℕ
ih : l.sum % n = (map (fun x ↦ x % n) l).sum % n
⊢ (a :: l).sum % n = (map (fun x ↦ x % n) (a :: l)).sum % n

Tactic:
simpa using

Goal state after:
case cons
n a : ℕ
l : List ℕ
ih : l.sum % n = (map (fun x ↦ x % n) l).sum % n
⊢ (a + l.sum) % n = (a + (map (fun x ↦ x % n) l).sum) % n
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: case cons
n a : ℕ
l : List ℕ
ih : l.prod % n = (map (fun x ↦ x % n) l).prod % n
⊢ (a :: l).prod % n = (map (fun x ↦ x % n) (a :: l)).prod % n

Tactic:
simpa using

Goal state after:
case cons
n a : ℕ
l : List ℕ
ih : l.prod % n = (map (fun x ↦ x % n) l).prod % n
⊢ a * l.prod % n = a * (map (fun x ↦ x % n) l).prod % n
Module: Mathlib.Data.Rat.Defs

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

Tactic:
by
  rw [pow_def, mk_eq_divInt, Int.natCast_pow]

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

Goal state before:
pp: q : ℚ
hq : q.num = 0
⊢ q = 0

Tactic:
simpa using

Goal state after:
q : ℚ
hq : q.num = 0
⊢ q = 0
Module: Mathlib.Data.Rat.Defs

Goal state before:
pp: q : ℚ
n d : ℤ
hq : q ≠ 0
hqnd : q = n /. d
this : n = 0
⊢ q = 0

Tactic:
simpa using

Goal state after:
q : ℚ
n d : ℤ
hq : q ≠ 0
hqnd : q = n /. d
this : n = 0
⊢ q = 0
Module: Mathlib.Data.Rat.Defs

Goal state before:
pp: q : ℚ
n d : ℤ
hq : q ≠ 0
hqnd : q = n /. d
this : d = 0
⊢ q = 0

Tactic:
simpa using

Goal state after:
q : ℚ
n d : ℤ
hq : q ≠ 0
hqnd : q = n /. d
this : d = 0
⊢ q = 0
Module: Mathlib.Data.List.Basic

Goal state before:
pp: case cons
α : Type u
β : Type v
inst✝³ : BEq α
inst✝² : LawfulBEq α
inst✝¹ : BEq β
inst✝ : LawfulBEq β
f : α → β
finj : Injective f
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {l₁ : List α}, map f (foldl List.erase l₁ tail✝) = foldl (fun l a ↦ l.erase (f a)) (map f l₁) tail✝
l₁ : List α
⊢ map f (foldl List.erase l₁ (head✝ :: tail✝)) = foldl (fun l a ↦ l.erase (f a)) (map f l₁) (head✝ :: tail✝)

Tactic:
simp only [foldl_cons, map_erase finj, *]

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

Goal state before:
pp: a b : ℕ
hab : ↑a = ↑b
⊢ a = b

Tactic:
simpa using

Goal state after:
a b : ℕ
hab : ↑a = ↑b
⊢ a = b
Module: Mathlib.Algebra.Order.Ring.Unbundled.Rat

Goal state before:
pp: a : ℤ
ha : 0 ≤ a
b : ℕ
⊢ 0 ≤ mkRat a b

Tactic:
simpa using

Goal state after:
a : ℤ
ha : 0 ≤ a
b : ℕ
⊢ 0 ≤ mkRat a b
Module: Mathlib.Algebra.Order.Ring.Unbundled.Rat

Goal state before:
pp: a : ℤ
b : ℕ
hb : b ≠ 0
⊢ 0 < ↑b

Tactic:
simpa using

Goal state after:
a : ℤ
b : ℕ
hb : b ≠ 0
⊢ 0 < b
Module: Mathlib.Algebra.Field.Rat

Goal state before:
pp: q : ℚ≥0
hq : q ≠ 0
⊢ (↑q.den).natAbs.Coprime q.num

Tactic:
simpa using

Goal state after:
q : ℚ≥0
hq : q ≠ 0
⊢ q.den.Coprime q.num
Module: Mathlib.Data.NNRat.Defs

Goal state before:
pp: r : ℚ
hr : 0 ≤ r
p q : ℚ
hpq : p ≤ q
⊢ r * p ≤ r * q

Tactic:
simpa using

Goal state after:
r : ℚ
hr : 0 ≤ r
p q : ℚ
hpq : p ≤ q
⊢ r * p ≤ r * q
Module: Mathlib.Data.NNRat.Defs

Goal state before:
pp: q : ℚ
⊢ q.toNNRat = 0 ↔ q ≤ 0

Tactic:
simpa using

Goal state after:
q : ℚ
⊢ q.toNNRat = 0 ↔ q ≤ 0
Module: Mathlib.Data.NNRat.Defs

Goal state before:
pp: q : ℚ≥0
⊢ 0 < q.num ↔ 0 < q

Tactic:
simpa using

Goal state after:
q : ℚ≥0
⊢ 0 ≤ q
Module: Mathlib.Data.NNRat.Defs

Goal state before:
pp: q : ℚ≥0
⊢ q.num.Coprime q.den

Tactic:
simpa using

Goal state after:
q : ℚ≥0
⊢ (↑q).num.natAbs.Coprime (↑q).den
Module: Mathlib.Algebra.Divisibility.Units

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

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

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

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

Tactic:
simpa using

Goal state after:
q₁ q₂ : ℚ
⊢ (q₁ + -q₂).den ∣ q₁.den.lcm q₂.den
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: case a
q : ℚ
n : ℤ
⊢ (q + ↑n).den ∣ q.den

Tactic:
simpa using

Goal state after:
case a
q : ℚ
n : ℤ
⊢ (q + ↑n).den ∣ q.den
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: case a
q : ℚ
n : ℤ
⊢ q.den ∣ (q + ↑n).den

Tactic:
simpa using

Goal state after:
case a
q : ℚ
n : ℤ
⊢ q.den ∣ (q + ↑n).den
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: n : ℤ
q : ℚ
⊢ (↑n - q).den = q.den

Tactic:
rw [sub_eq_add_neg, intCast_add_den, neg_den]

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

Goal state before:
pp: q r : ℚ
⊢ q + r = (q.num * ↑r.den + ↑q.den * r.num) /. (↑q.den * ↑r.den)

Tactic:
by
  have hqd : (q.den : ℤ) ≠ 0 := Int.natCast_ne_zero_iff_pos.2 q.den_pos
  have hrd : (r.den : ℤ) ≠ 0 := Int.natCast_ne_zero_iff_pos.2 r.den_pos
  conv_lhs => rw [← num_divInt_den q, ← num_divInt_den r, divInt_add_divInt _ _ hqd hrd]
  rw [mul_comm r.num q.den]

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

Goal state before:
pp: α : Type u_3
inst✝ : DivisionSemiring α
q : ℚ≥0
a : α
⊢ Commute (↑q) a

Tactic:
simpa using

Goal state after:
α : Type u_3
inst✝ : DivisionSemiring α
q : ℚ≥0
a : α
⊢ Commute (↑q.num / ↑q.den) a
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
this : Rat.divInt ↑a ↑b = ↑⟨{ num := ↑n, den := d, den_nz := h, reduced := c }, hn⟩
⊢ d ∣ b

Tactic:
simpa using

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
this : Rat.divInt ↑a ↑b = ↑⟨{ num := ↑n, den := d, den_nz := h, reduced := c }, hn⟩
⊢ d ∣ b
Module: Mathlib.Tactic.NormNum.Inv

Goal state before:
pp: n✝¹ num✝ : ℤ
n✝ denom✝ : ℕ
inv✝ : Invertible ↑denom✝
h : ↑n✝¹ / ↑n✝ = ↑num✝ * ⅟↑denom✝
⊢ IsRat (mkRat ↑n✝¹ ↑n✝) num✝ denom✝

Tactic:
rw [Rat.mkRat_eq_div]; exact ⟨_, h⟩

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

Goal state before:
pp: α : Type u_3
inst✝ : DivisionRing α
r : ℚ
a : α
⊢ Commute (↑r) a

Tactic:
simpa using

Goal state after:
α : Type u_3
inst✝ : DivisionRing α
r : ℚ
a : α
⊢ Commute (↑r.num / ↑r.den) a
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: p : ℚ → Prop
h : ∀ (a b : ℤ), b ≠ 0 → p (↑a / ↑b)
q : ℚ
⊢ p q

Tactic:
simpa using

Goal state after:
p : ℚ → Prop
h : ∀ (a b : ℤ), b ≠ 0 → p (↑a / ↑b)
q : ℚ
⊢ p q
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: p : ℚ → Prop
⊢ (∃ r, p r) ↔ ∃ a b, b ≠ 0 ∧ p (↑a / ↑b)

Tactic:
simpa using

Goal state after:
p : ℚ → Prop
⊢ (∃ r, p r) ↔ ∃ a b, ¬b = 0 ∧ p (↑a / ↑b)
Module: Mathlib.Tactic.Ring.Common

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

Tactic:
subst_vars; simp [add_left_comm]

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : CompleteLattice α
p : ι → Prop
f : (i : ι) → p i → α
a : α
h : ∃ i, p i
⊢ a ⊔ ⨆ i, ⨆ (h : p i), f i h = ⨆ i, ⨆ (h : p i), a ⊔ f i h

Tactic:
simpa using

Goal state after:
α : Type u_1
ι : Sort u_4
inst✝ : CompleteLattice α
p : ι → Prop
f : (i : ι) → p i → α
a : α
h : ∃ i, p i
⊢ a ⊔ ⨆ i, ⨆ (h : p i), f i h = ⨆ i, ⨆ (h : p i), a ⊔ f i h
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: β : Type u_2
ι : Type u_12
t : Set ι
s : ι → Set β
w : ⋃ i ∈ t, s i = ⊤
x : β
p : ∃ i, x ∈ ⋃ (_ : i ∈ t), s i
⊢ ∃ i ∈ t, x ∈ s i

Tactic:
simpa using

Goal state after:
β : Type u_2
ι : Type u_12
t : Set ι
s : ι → Set β
w : ⋃ i ∈ t, s i = ⊤
x : β
p : ∃ i, x ∈ ⋃ (_ : i ∈ t), s i
⊢ ∃ i ∈ t, x ∈ s i
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
ι : Sort u_5
s : ι → Set α
inst✝ : Nonempty α
h_Union : ⋃ i, s i = univ
⊢ (⋃ i, s i).Nonempty

Tactic:
simpa using

Goal state after:
α : Type u_1
ι : Sort u_5
s : ι → Set α
inst✝ : Nonempty α
h_Union : ⋃ i, s i = univ
⊢ univ.Nonempty
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : β → α
p : β → Prop
⊢ ⨆ i, f i = (⨆ i, ⨆ (_ : p i), f i) ⊔ ⨆ i, ⨆ (_ : ¬p i), f i

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : β → α
p : β → Prop
⊢ ⨆ i, f i = (⨆ i, ⨆ (_ : p i), f i) ⊔ ⨆ i, ⨆ (_ : ¬p i), f i
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : CompleteLattice α
s : Set β
t : Set γ
f : β → α
g : γ → α
h : β → γ
h1 : BijOn h s t
h2 : ∀ (x : β), g (h x) = f x
⊢ ⨆ x ∈ s, f x = ⨆ y ∈ t, g y

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : CompleteLattice α
s : Set β
t : Set γ
f : β → α
g : γ → α
h : β → γ
h1 : BijOn h s t
h2 : ∀ (x : β), g (h x) = f x
⊢ ⨆ x ∈ s, f x = ⨆ y ∈ t, g y
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
s : Set α
b : α
inst✝ : CompleteLattice α
minAx : MinimalAxioms α
⊢ sSup s ⊓ b = ⨆ a ∈ s, a ⊓ b

Tactic:
simpa using

Goal state after:
α : Type u
s : Set α
b : α
inst✝ : CompleteLattice α
minAx : MinimalAxioms α
⊢ b ⊓ sSup s = ⨆ a ∈ s, b ⊓ a
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
ι : Sort w
inst✝ : CompleteLattice α
minAx : MinimalAxioms α
a : α
f : ι → α
⊢ a ⊓ ⨆ i, f i = ⨆ i, a ⊓ f i

Tactic:
simpa using

Goal state after:
α : Type u
ι : Sort w
inst✝ : CompleteLattice α
minAx : MinimalAxioms α
a : α
f : ι → α
⊢ a ⊓ ⨆ i, f i = ⨆ i, a ⊓ f i
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:
simp only [inter_iUnion]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
x : β
⊢ x ∈ ⋃ x, {f x} ↔ x ∈ range f

Tactic:
simp [@eq_comm _ x]

Goal state after:
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 ι
i_in_J : i ∈ J
⊢ x ∈ ⋃ j ∈ J, Es j

Tactic:
simpa using

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 ι
i_in_J : i ∈ J
⊢ ∃ i ∈ J, x ∈ Es i
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
obs : ∀ (J : Set ι), x ∈ ⋃ j ∈ J, Es j ↔ i ∈ J
J : Set ι
⊢ x ∈ (⋃ j ∈ J, Es j)ᶜ ↔ i ∉ J

Tactic:
simpa using

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
obs : ∀ (J : Set ι), x ∈ ⋃ j ∈ J, Es j ↔ i ∈ J
J : Set ι
⊢ x ∈ ⋃ j ∈ J, Es j ↔ i ∈ J
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α✝ : Type u
β✝ : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLinearOrder α✝
α : Type u
β : α → Type u
g : (a : α) → β a → α✝
lhs : α✝ := ⨅ a, ⨆ b, g a b
rhs : α✝ := ⨆ h, ⨅ a, g a (h a)
h : ¬∃ x, rhs < x ∧ x < lhs
hrl : rhs < lhs
⊢ ∀ (x : α✝), x ≤ rhs ∨ lhs ≤ x

Tactic:
simpa using

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
rhs : α✝ := ⨆ h, ⨅ a, g a (h a)
h : ¬∃ x, rhs < x ∧ x < lhs
hrl : rhs < lhs
⊢ ∀ (x : α✝), x ≤ rhs ∨ lhs ≤ x
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
β : Type u_2
t : α → Set β
b : β
hb : b ∈ ⋃ i, t i
⊢ ∃ a, b ∈ t a

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
t : α → Set β
b : β
hb : b ∈ ⋃ i, t i
⊢ ∃ a, b ∈ t a
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α✝ : Type u
β✝ : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLinearOrder α✝
α : Type u
β : α → Type u
g : (a : α) → β a → α✝
lhs : α✝ := ⨅ a, ⨆ b, g a b
rhs : α✝ := ⨆ h, ⨅ a, g a (h a)
hrl : rhs < lhs
h : ∀ (x : α✝), x ≤ rhs ∨ lhs ≤ x
f : (a : α) → β a
hf : ∀ (a : α), rhs < g a (f a)
a : α
⊢ ¬g a (f a) ≤ rhs

Tactic:
simpa using

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
rhs : α✝ := ⨆ h, ⨅ a, g a (h a)
hrl : rhs < lhs
h : ∀ (x : α✝), x ≤ rhs ∨ lhs ≤ x
f : (a : α) → β a
hf : ∀ (a : α), rhs < g a (f a)
a : α
⊢ rhs < g a (f a)
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
inst✝ : Frame α
s : Set α
b : α
⊢ sSup s ⊓ b = ⨆ a ∈ s, a ⊓ b

Tactic:
simpa using

Goal state after:
α : Type u
inst✝ : Frame α
s : Set α
b : α
⊢ b ⊓ sSup s = ⨆ a ∈ s, b ⊓ a
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
ι : Sort w
inst✝ : Frame α
a : α
f : ι → α
⊢ a ⊓ ⨆ i, f i = ⨆ i, a ⊓ f i

Tactic:
simpa using

Goal state after:
α : Type u
ι : Sort w
inst✝ : Frame α
a : α
f : ι → α
⊢ a ⊓ ⨆ i, f i = ⨆ i, a ⊓ f i
Module: Mathlib.Order.CompleteBooleanAlgebra

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

Tactic:
simpa using

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

Goal state before:
pp: α : Type u
inst✝ : Frame α
a : α
s : Set α
⊢ Disjoint a (sSup s) ↔ ∀ b ∈ s, Disjoint a b

Tactic:
simpa using

Goal state after:
α : Type u
inst✝ : Frame α
a : α
s : Set α
⊢ Disjoint a (sSup s) ↔ ∀ b ∈ s, Disjoint a b
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: α : Type u_1
inst✝² : ConditionallyCompleteLattice α
a : α
inst✝¹ : NoMinOrder α
inst✝ : DenselyOrdered α
w : α
hw : w < a
⊢ ∃ a_1 ∈ Iio a, w < a_1

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝² : ConditionallyCompleteLattice α
a : α
inst✝¹ : NoMinOrder α
inst✝ : DenselyOrdered α
w : α
hw : w < a
⊢ ∃ a_1, w < a_1 ∧ a_1 < a
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
t : Set α
hs : ∀ x ∈ ∅, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ ∅, y ≤ x
y : α
yt : y ∈ t
⊢ False

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
t : Set α
hs : ∀ x ∈ ∅, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ ∅, y ≤ x
y : α
yt : y ∈ t
⊢ False
Module: Mathlib.Order.CompleteBooleanAlgebra

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

Tactic:
simpa using

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

Goal state before:
pp: α : Type u
ι : Sort w
inst✝¹ : CompleteBooleanAlgebra α
f : ι → α
inst✝ : Nonempty ι
a : α
⊢ a ∆ ⨆ i, f i ≤ ⨆ i, a ∆ f i

Tactic:
simpa using

Goal state after:
α : Type u
ι : Sort w
inst✝¹ : CompleteBooleanAlgebra α
f : ι → α
inst✝ : Nonempty ι
a : α
⊢ a ∆ ⨆ i, f i ≤ ⨆ i, a ∆ f i
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
inst✝ : CompleteBooleanAlgebra α
s : Set α
hs : s.Nonempty
a : α
⊢ a ∆ sSup s ≤ sSup ((fun x ↦ a ∆ x) '' s)

Tactic:
simpa using

Goal state after:
α : Type u
inst✝ : CompleteBooleanAlgebra α
s : Set α
hs : s.Nonempty
a : α
⊢ a ∆ sSup s ≤ sSup ((fun x ↦ a ∆ x) '' s)
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
s_ne : s.Nonempty
hs : ∀ x ∈ s, ∃ y ∈ ∅, x ≤ y
ht : ∀ y ∈ ∅, ∃ x ∈ s, y ≤ x
x : α
xs : x ∈ s
⊢ False

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
s_ne : s.Nonempty
hs : ∀ x ∈ s, ∃ y ∈ ∅, x ≤ y
ht : ∀ y ∈ ∅, ∃ x ∈ s, y ≤ x
x : α
xs : x ∈ s
⊢ False
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
inst✝ : CompleteBooleanAlgebra α
s t : Set α
hs : s.Nonempty
ht : t.Nonempty
⊢ sSup s ∆ sSup t ≤ ⨆ a ∈ s, a ∆ sSup t

Tactic:
simpa using

Goal state after:
α : Type u
inst✝ : CompleteBooleanAlgebra α
s t : Set α
hs : s.Nonempty
ht : t.Nonempty
⊢ sSup s ∆ sSup t ≤ ⨆ a ∈ s, a ∆ sSup t
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
inst✝ : CompleteBooleanAlgebra α
s t : Set α
hs : s.Nonempty
ht : t.Nonempty
a : α
x✝ : a ∈ s
⊢ a ∆ sSup t ≤ ⨆ b ∈ t, a ∆ b

Tactic:
simpa using

Goal state after:
α : Type u
inst✝ : CompleteBooleanAlgebra α
s t : Set α
hs : s.Nonempty
ht : t.Nonempty
a : α
x✝ : a ∈ s
⊢ a ∆ sSup t ≤ ⨆ b ∈ t, a ∆ b
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
β : Type v
ι✝¹ : Sort w
κ : ι✝¹ → Sort w'
ι : Type u_1
π : ι → Type u_2
inst✝ : (i : ι) → CompleteAtomicBooleanAlgebra (π i)
ι✝ : Type (max u_1 u_2)
κ✝ : ι✝ → Type (max u_1 u_2)
f : (a : ι✝) → κ✝ a → (i : ι) → π i
x✝ : ι
⊢ (⨅ a, ⨆ b, f a b) x✝ = (⨆ g, ⨅ a, f a (g a)) x✝

Tactic:
iInf_iSup_eq

Goal state after:
α : Type u
β : Type v
ι✝¹ : Sort w
κ : ι✝¹ → Sort w'
ι : Type u_1
π : ι → Type u_2
inst✝ : (i : ι) → CompleteAtomicBooleanAlgebra (π i)
ι✝ : Type (max u_1 u_2)
κ✝ : ι✝ → Type (max u_1 u_2)
f : (a : ι✝) → κ✝ a → (i : ι) → π i
x✝ : ι
⊢ (⨆ g, ⨅ a, f a (g a)) x✝ = (⨆ g, ⨅ a, f a (g a)) x✝
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, ⨆ i_1, f (g i i_1) = ⨆ i, ⨅ i_1, f (g i_1 (i i_1))

Tactic:
iInf_iSup_eq

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

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set α
a : α
hb : BddAbove s
⊢ a < sSup s ↔ ∃ b ∈ s, a < b

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set α
a : α
hb : BddAbove s
⊢ a < sSup s ↔ ∃ b ∈ s, a < b
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
t : Set α
ht : BddBelow (f '' t)
hf : MonotoneOn f t
hst : ∅ ⊆ t
h : ∀ y ∈ t, ∃ x ∈ ∅, x ≤ y
⊢ t = ∅

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
t : Set α
ht : BddBelow (f '' t)
hf : MonotoneOn f t
hst : ∅ ⊆ t
h : ∀ y ∈ t, ∃ x ∈ ∅, x ≤ y
⊢ ∀ (x : α), x ∉ t
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := e.completeDistribLattice
⊢ CompletelyDistribLattice α

Tactic:
apply e.injective.completelyDistribLattice

Goal state after:
case le
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := ⋯
⊢ ∀ {x y : α}, e x ≤ e y ↔ x ≤ y

case lt
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := ⋯
⊢ ∀ {x y : α}, e x < e y ↔ x < y

case map_sup
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := ⋯
⊢ ∀ (a b : α), e (a ⊔ b) = e a ⊔ e b

case map_inf
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := ⋯
⊢ ∀ (a b : α), e (a ⊓ b) = e a ⊓ e b

case map_sSup
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := ⋯
⊢ ∀ (s : Set α), e (sSup s) = ⨆ a ∈ s, e a

case map_sInf
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := ⋯
⊢ ∀ (s : Set α), e (sInf s) = ⨅ a ∈ s, e a

case map_top
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := ⋯
⊢ e ⊤ = ⊤

case map_bot
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := ⋯
⊢ e ⊥ = ⊥

case map_compl
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := ⋯
⊢ ∀ (a : α), e aᶜ = (e a)ᶜ

case map_himp
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := ⋯
⊢ ∀ (a b : α), e (a ⇨ b) = e a ⇨ e b

case map_hnot
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := ⋯
⊢ ∀ (a : α), e (￢a) = ￢e a

case map_sdiff
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := ⋯
⊢ ∀ (a b : α), e (a \ b) = e a \ e b
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : Std.Symm r
a b : α
⊢ Pairwise (r on fun c ↦ bif c then a else b) ↔ r a b

Tactic:
simpa using

Goal state after:
α : Type u_1
r : α → α → Prop
inst✝ : Std.Symm r
a b : α
⊢ r a b → r b a
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝ : DistribLattice α
a b c : α
⊢ b ∈ [[a, c]] → c ∈ [[a, b]] → b = c

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : DistribLattice α
a b c : α
⊢ b ∈ [[c, a]] → c ∈ [[b, a]] → b = c
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝ : DistribLattice α
a : α
⊢ Injective (uIcc a)

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : DistribLattice α
a : α
⊢ Injective (uIcc a)
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: α : Type u_1
r : α → α → Prop
⊢ univ.Pairwise r ↔ Pairwise r

Tactic:
simp only [Set.Pairwise, Pairwise, mem_univ, forall_const]

Goal state after:
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (a : α), a ∈ s → Injective (f a)
hs : s.PairwiseDisjoint fun a ↦ f a '' t
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.1 x.2 = (fun p ↦ f p.1 p.2) y
this : x.1 = y.1
⊢ x = y

Tactic:
by exact Prod.ext this (hf _ hx.1 <| h.trans <| by rw [this])

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ b ∈ Ι a c → c ∈ Ι a b → b = c

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ b ∈ Ι c a → c ∈ Ι b a → b = c