mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Directed

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : Std.Refl r
a b : α
hab : r a b
⊢ DirectedOn r {b, a}

Tactic:
by
  rw [Set.pair_comm]
  apply directedOn_pair hab

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

Goal state before:
pp: case inl
R : Type u_1
inst✝⁷ : Semiring R
inst✝⁶ : LinearOrder R
inst✝⁵ : FloorSemiring R
a : R
S : Type u_3
inst✝⁴ : Semiring S
inst✝³ : LinearOrder S
inst✝² : FloorSemiring S
b : S
inst✝¹ : IsStrictOrderedRing R
inst✝ : IsStrictOrderedRing S
h : ∀ (n : ℕ), ↑n ≤ a ↔ ↑n ≤ b
h₀ : 0 ≤ a ↔ 0 ≤ b
ha : a < 0
⊢ 0 = ⌊b⌋₊

Tactic:
floor_of_nonpos (le_of_not_ge <| h₀.not.mp ha.not_ge)

Goal state after:
case inl
R : Type u_1
inst✝⁷ : Semiring R
inst✝⁶ : LinearOrder R
inst✝⁵ : FloorSemiring R
a : R
S : Type u_3
inst✝⁴ : Semiring S
inst✝³ : LinearOrder S
inst✝² : FloorSemiring S
b : S
inst✝¹ : IsStrictOrderedRing R
inst✝ : IsStrictOrderedRing S
h : ∀ (n : ℕ), ↑n ≤ a ↔ ↑n ≤ b
h₀ : 0 ≤ a ↔ 0 ≤ b
ha : a < 0
⊢ 0 = 0
Module: Mathlib.Algebra.Order.Ring.Basic

Goal state before:
pp: R : Type u_3
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
x y : R
hx : 0 ≤ x
hy : 0 ≤ y
k : ℕ
hn : k + 1 ≠ 0
⊢ x ^ (k + 1) + y ^ (k + 1) ≤ (x + y) ^ (k + 1)

Tactic:
induction k with
  | zero => simp only [zero_add, pow_one, le_refl]
  | succ k ih =>
    let n := k.succ
    have h1 := add_nonneg (mul_nonneg hx (pow_nonneg hy n)) (mul_nonneg hy (pow_nonneg hx n))
    have h2 := add_nonneg hx hy
    calc
      x ^ (n + 1) + y ^ (n + 1) ≤ x * x ^ n + y * y ^ n + (x * y ^ n + y * x ^ n) := by
        rw [pow_succ' _ n, pow_succ' _ n]
        exact le_add_of_nonneg_right h1
      _ = (x + y) * (x ^ n + y ^ n) := by
        rw [add_mul, mul_add, mul_add, add_comm (y * x ^ n), ← add_assoc, ← add_assoc,
          add_assoc (x * x ^ n) (x * y ^ n), add_comm (x * y ^ n) (y * y ^ n), ← add_assoc]
      _ ≤ (x + y) ^ (n + 1) := by
        rw [pow_succ' _ n]
        gcongr; exact ih (Nat.succ_ne_zero k)

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

Goal state before:
pp: α : Type u_1
β : Type u_3
f : α → α → β
s t : Set α
hf : ∀ (a b : α), f a b = f b a
⊢ image2 f (s ∪ t) (s ∩ t) ⊆ image2 f s t

Tactic:
image2_comm hf

Goal state after:
α : Type u_1
β : Type u_3
f : α → α → β
s t : Set α
hf : ∀ (a b : α), f a b = f b a
⊢ image2 f (s ∩ t) (s ∪ t) ⊆ image2 f s t
Module: Mathlib.Order.Antisymmetrization

Goal state before:
pp: α : Type u_1
a b c : α
inst✝ : Preorder α
h₁ : SymmGen (fun x1 x2 ↦ x1 ≤ x2) a b
h₂ : AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) b c
⊢ SymmGen (fun x1 x2 ↦ x1 ≤ x2) a c

Tactic:
obtain (h | h) := h₁
  · exact (h.trans h₂.le).symmGen
  · exact (h₂.ge.trans h).symmGen_symm

Goal state after:
Module: Mathlib.Logic.Equiv.Set

Goal state before:
pp: α : Type u_3
s t : Set α
h : s ⊆ t
inst✝ : DecidablePred fun x ↦ x ∈ s
x : ↑t
hx : ↑x ∈ s
⊢ (Set.sumDiffSubset h).symm x = Sum.inl ⟨↑x, hx⟩

Tactic:
apply (Equiv.Set.sumDiffSubset h).injective

Goal state after:
α : Type u_3
s t : Set α
h : s ⊆ t
inst✝ : DecidablePred fun x ↦ x ∈ s
x : ↑t
hx : ↑x ∈ s
⊢ (Set.sumDiffSubset h) ((Set.sumDiffSubset h).symm x) = (Set.sumDiffSubset h) (Sum.inl ⟨↑x, hx⟩)
Module: Mathlib.Logic.Equiv.Set

Goal state before:
pp: α : Type u_3
s t : Set α
h : s ⊆ t
inst✝ : DecidablePred fun x ↦ x ∈ s
x : ↑t
hx : ¬↑x ∈ s
⊢ (Set.sumDiffSubset h).symm x = Sum.inr ⟨↑x, ⋯⟩

Tactic:
apply (Equiv.Set.sumDiffSubset h).injective

Goal state after:
α : Type u_3
s t : Set α
h : s ⊆ t
inst✝ : DecidablePred fun x ↦ x ∈ s
x : ↑t
hx : ¬↑x ∈ s
⊢ (Set.sumDiffSubset h) ((Set.sumDiffSubset h).symm x) = (Set.sumDiffSubset h) (Sum.inr ⟨↑x, ⋯⟩)
Module: Mathlib.Logic.Equiv.Set

Goal state before:
pp: α✝¹ : Sort u
β✝ : Sort v
γ : Sort w
α✝ : Type u_1
β : Type u_2
α : Type u
s t : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ ↑(t \ s) ⊕ ↑(s ∩ t) ≃ ↑(t \ s ∪ s ∩ t)

Tactic:
refine (Set.union' (· ∉ s) ?_ ?_).symm
          exacts [fun x hx => hx.2, fun x hx => not_not_intro hx.1]

Goal state after:
Module: Mathlib.Order.WellFounded

Goal state before:
pp: case inr.inr
β : Type u_2
γ : Type u_3
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : WellFoundedLT β
f : β → γ
hf : f ∈ {f | StrictMono f}
g : β → γ
hg : g ∈ {f | StrictMono f}
hfg : range f = range g
a✝ a : β
IH : ∀ (y : β), y < a → f y = g y
b : β
hb : g b = f a
h : a < b
⊢ f a = g a

Tactic:
obtain ⟨c, hc⟩ := hfg.symm ▸ mem_range_self a
    have := hg h
    rw [hb, ← hc, hf.lt_iff_lt] at this
    rw [IH c this] at hc
    cases (hg.injective hc).not_lt this

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
h : ¬a < b
⊢ Ioc a b = Ico a b

Tactic:
Ioc_eq_empty h,

Goal state after:
α : Type u_1
inst✝ : Preorder α
a b : α
h : ¬a < b
⊢ ∅ = Ico a b
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
h : ¬a < b
⊢ Ioc a b = Ico a b

Tactic:
by rw [Ioc_eq_empty h, Ico_eq_empty h]

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

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b x : α
⊢ x ∈ Ico a b \ {a} ↔ x ∈ Ioo a b

Tactic:
simp [and_right_comm, ← lt_iff_le_and_ne, eq_comm]

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

Goal state before:
pp: case inr
γ : Type u_3
inst✝ : PartialOrder γ
j i : γ
hj : IsLUB (Iio i) j
hj_lt_i : j < i
⊢ j = i ∨ Iio i = Iic j

Tactic:
right
    exact Set.ext fun k => ⟨fun hk_lt => hj.1 hk_lt, fun hk_le_j => lt_of_le_of_lt hk_le_j hj_lt_i⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
t : Set β
hs : s.Nonempty
ht : t.Nonempty
x✝ : α × β
⊢ x✝ ∈ upperBounds (s ×ˢ t) ↔ x✝ ∈ upperBounds s ×ˢ upperBounds t

Tactic:
← nonempty_coe_sort

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
t : Set β
hs : Nonempty ↑s
ht : Nonempty ↑t
x✝ : α × β
⊢ x✝ ∈ upperBounds (s ×ˢ t) ↔ x✝ ∈ upperBounds s ×ˢ upperBounds t
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝⁴ : Semifield α
inst✝³ : PartialOrder α
inst✝² : PosMulReflectLT α
inst✝¹ : IsStrictOrderedRing α
β : Type u_4
inst✝ : Preorder β
f : β → α
hf : StrictMono f
c : α
hc : 0 < c
⊢ StrictMono fun x ↦ f x / c

Tactic:
simpa only [div_eq_mul_inv] using hf.mul_const (inv_pos.2 hc)

Goal state after:
Module: Mathlib.Control.Functor

Goal state before:
pp: F : Type u_1 → Type u_2
m : {α β : Type u_1} → (α → β) → F α → F β
mc : {α β : Type u_1} → α → F β → F α
m' : {α β : Type u_1} → (α → β) → F α → F β
mc' : {α β : Type u_1} → α → F β → F α
H1 : LawfulFunctor F
H2 : LawfulFunctor F
H : ∀ (α β : Type u_1) (f : α → β) (x : F α), f <$> x = f <$> x
⊢ { map := m, mapConst := mc } = { map := m', mapConst := mc' }

Tactic:
by
    cases show @m = @m' by funext α β f x; apply H
    congr
    funext α β
    have E1 := @map_const _ ⟨@m, @mc⟩ H1
    have E2 := @map_const _ ⟨@m, @mc'⟩ H2
    exact E1.trans E2.symm

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

Goal state before:
pp: α : Type u
l : List α
n : ℕ
⊢ tail^[n] l = drop n l

Tactic:
by
  induction n generalizing l with
  | zero => rfl
  | succ n ih => cases l <;> simp [*]

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

Goal state before:
pp: case inr
α : Type u
l : List α
n : ℕ
a b : α
h : a ∈ l.insertIdx n b
hn : l.length ≥ n
⊢ a = b ∨ a ∈ l

Tactic:
rwa [mem_insertIdx hn] at h

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

Goal state before:
pp: case mpr
α : Type u_1
a c : List α
⊢ a ~ c → (Perm ∘r Perm) a c

Tactic:
· exact fun h => ⟨a, Perm.refl a, h⟩

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

Goal state before:
pp: case mpr
α : Type u
hα : Subsingleton α
l1 : List α
⊢ ∀ ⦃a₂ : List α⦄, l1.length = a₂.length → l1 = a₂

Tactic:
l2

Goal state after:
case mpr
α : Type u
hα : Subsingleton α
l1 l2 : List α
⊢ l1.length = l2.length → l1 = l2
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : CommGroupWithZero α
n : ℤ
a b : α
⊢ zpow' (a * b) n = zpow' a n * zpow' b n

Tactic:
by
  by_cases ha : a = 0
  · simp [ha]
  by_cases hb : b = 0
  · simp [hb]
  simpa [zpow', ha, hb] using mul_zpow a b n

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

Goal state before:
pp: M : Type u_1
inst✝⁴ : GroupWithZero M
inst✝³ : PartialOrder M
inst✝² : PosMulStrictMono M
inst✝¹ : PosMulReflectLT M
inst✝ : ZeroLEOneClass M
r : ℤ
x : M
hx : 0 < x
l : NF M
hl : 0 < l.eval
⊢ 0 < x ^ r

Tactic:
apply zpow_pos hx

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

Goal state before:
pp: ι : Type u_1
α : Type u
β : Type v
γ : Type w
l✝ l₁ l₂ l : List α
h : l.length - 1 < l.length
⊢ l ≠ []

Tactic:
by rintro rfl; exact Nat.lt_irrefl 0 h

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
g : β → α
h : LeftInverse (map f) (map g)
x : β
⊢ f (g x) = x

Tactic:
by injection h [x]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Zero α
inst✝ : SemilatticeSup α
a : α
b : { x // 0 ≤ x }
⊢ toNonneg a ≤ b ↔ a ≤ ↑b

Tactic:
by
  obtain ⟨b, hb⟩ := b
  simp [toNonneg, hb]

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

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

Tactic:
alternatingProd_cons'

Goal state after:
G : Type u_7
inst✝ : CommGroup G
a : G
l : List G
⊢ a * l.alternatingProd⁻¹ = a * l.alternatingProd⁻¹
Module: Mathlib.Data.List.Basic

Goal state before:
pp: case cons
α : Type u
β : Type v
f : α → Option β
a : α
l : List α
ih : filterMap f l = flatMap (fun a ↦ (f a).toList) l
⊢ (match f a with
    | none => filterMap f l
    | some b => b :: filterMap f l) =
    (f a).toList ++ flatMap (fun a ↦ (f a).toList) l

Tactic:
rcases f a

Goal state after:
case cons.none
α : Type u
β : Type v
f : α → Option β
a : α
l : List α
ih : filterMap f l = flatMap (fun a ↦ (f a).toList) l
⊢ (match none with
    | none => filterMap f l
    | some b => b :: filterMap f l) =
    none.toList ++ flatMap (fun a ↦ (f a).toList) l

case cons.some
α : Type u
β : Type v
f : α → Option β
a : α
l : List α
ih : filterMap f l = flatMap (fun a ↦ (f a).toList) l
val✝ : β
⊢ (match some val✝ with
    | none => filterMap f l
    | some b => b :: filterMap f l) =
    (some val✝).toList ++ flatMap (fun a ↦ (f a).toList) l
Module: Mathlib.Algebra.Field.Rat

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

Tactic:
ext; simp [Rat.div_def', num_coe, den_coe]

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

Goal state before:
pp: case pos
K : Type u_1
inst✝ : NNRatCast K
m : ℕ
b : Bool
d : ℕ
h✝ : b = true
⊢ (if b = true then mkRat (↑(OfNat.ofNat m)) (10 ^ OfNat.ofNat d) else ↑(OfNat.ofNat m * 10 ^ OfNat.ofNat d)) =
    Rat.divInt ↑m ↑(10 ^ d)

Tactic:
if_pos ‹_›

Goal state after:
case pos
K : Type u_1
inst✝ : NNRatCast K
m : ℕ
b : Bool
d : ℕ
h✝ : b = true
⊢ mkRat (↑(OfNat.ofNat m)) (10 ^ OfNat.ofNat d) = Rat.divInt ↑m ↑(10 ^ d)
Module: Mathlib.Algebra.GroupWithZero.Divisibility

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
a : α
m n : ℕ
ha₀ : a ≠ 0
ha : ¬IsUnit a
h : a ^ n ∣ a ^ m
hmn : m < n
⊢ a ^ (m + 1) ∣ a ^ m

Tactic:
exact (pow_dvd_pow _ (Nat.succ_le_of_lt hmn)).trans h

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

Goal state before:
pp: case inr
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
this : q.num * d = n * ↑q.den
⊢ ∃ c, n = c * q.num ∧ d = c * ↑q.den

Tactic:
have hqdn : q.num ∣ n := by
    rw [qdf]
    exact Rat.num_dvd _ hd

Goal state after:
case inr
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
this : q.num * d = n * ↑q.den
hqdn : q.num ∣ n
⊢ ∃ c, n = c * q.num ∧ d = c * ↑q.den
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: a : ℤ
b : ℕ
hb0 : 0 < ↑b
h : a.natAbs.Coprime (↑b).natAbs
⊢ (↑a / ↑↑b).num = a

Tactic:
simp only [Int.natAbs_natCast, Int.natCast_pos] at h hb0

Goal state after:
a : ℤ
b : ℕ
h : a.natAbs.Coprime b
hb0 : 0 < b
⊢ (↑a / ↑↑b).num = a
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: case hb
α : Type u_3
inst✝ : DivisionRing α
p q : ℚ
hp : ↑p.den ≠ 0
hq : ↑q.den ≠ 0
⊢ ↑p.den * ↑q.den ≠ 0

Tactic:
exact mul_ne_zero hp hq

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

Goal state before:
pp: a : ℤ
b : ℕ
hb0 : 0 < ↑b
h : a.natAbs.Coprime (↑b).natAbs
⊢ ↑(↑a / ↑↑b).den = ↑b

Tactic:
simp only [Int.natAbs_natCast, Int.natCast_pos] at h hb0

Goal state after:
a : ℤ
b : ℕ
h : a.natAbs.Coprime b
hb0 : 0 < b
⊢ ↑(↑a / ↑↑b).den = ↑b
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: case b0
α : Type u_3
inst✝ : DivisionRing α
p q : ℚ
hp : ↑p.den ≠ 0
hq : ↑q.num ≠ 0
⊢ ↑p.den * ↑q.num ≠ 0

Tactic:
exact mul_ne_zero hp hq

Goal state after:
Module: Mathlib.Tactic.CancelDenoms.Core

Goal state before:
pp: α : Type u_1
inst✝ : CommRing α
n1 n2 k e1 e2 t1 t2 : α
h1 : n1 * e1 = t1
h2 : n2 * e2 = t2
h3 : n1 * n2 = k
⊢ n2 * (n1 * (e1 * e2)) = t1 * t2

Tactic:
← mul_assoc n1,

Goal state after:
α : Type u_1
inst✝ : CommRing α
n1 n2 k e1 e2 t1 t2 : α
h1 : n1 * e1 = t1
h2 : n2 * e2 = t2
h3 : n1 * n2 = k
⊢ n2 * (n1 * e1 * e2) = t1 * t2
Module: Mathlib.Order.GaloisConnection.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set α
a : α
h : IsLUB s a
b : β
hb : b ∈ upperBounds (l '' s)
⊢ u b ∈ upperBounds s

Tactic:
rwa [gc.upperBounds_l_image] at hb

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

Goal state before:
pp: α : Type u
β : Type v
ι : Sort x
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
l : α → β
u : β → α
gc : GaloisConnection l u
f : ι → α
⊢ IsLUB (range (l ∘ f)) (l (iSup f))

Tactic:
rw [range_comp, ← sSup_range]

Goal state after:
α : Type u
β : Type v
ι : Sort x
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
l : α → β
u : β → α
gc : GaloisConnection l u
f : ι → α
⊢ IsLUB (l '' range f) (l (sSup (range f)))
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
s : Set α
⊢ sSup s = ⊥ ↔ s = ∅ ∨ s = {⊥}

Tactic:
sSup_eq_bot,

Goal state after:
α : Type u_1
inst✝ : CompleteLattice α
s : Set α
⊢ (∀ a ∈ s, a = ⊥) ↔ s = ∅ ∨ s = {⊥}
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: case le
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
e : α ≃ β
inst✝ : CompleteLattice β
top : Top α := e.top
bot : Bot α := e.bot
supSet : SupSet α := e.supSet
infSet : InfSet α := e.infSet
lattice : Lattice α := e.lattice
x✝ y✝ : α
⊢ e x✝ ≤ e y✝ ↔ x✝ ≤ y✝

Tactic:
first | rfl | exact e.apply_symm_apply _

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

Goal state before:
pp: case lt
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
e : α ≃ β
inst✝ : CompleteLattice β
top : Top α := e.top
bot : Bot α := e.bot
supSet : SupSet α := e.supSet
infSet : InfSet α := e.infSet
lattice : Lattice α := e.lattice
x✝ y✝ : α
⊢ e x✝ < e y✝ ↔ x✝ < y✝

Tactic:
first | rfl | exact e.apply_symm_apply _

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

Goal state before:
pp: case map_sup
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
e : α ≃ β
inst✝ : CompleteLattice β
top : Top α := e.top
bot : Bot α := e.bot
supSet : SupSet α := e.supSet
infSet : InfSet α := e.infSet
lattice : Lattice α := e.lattice
a✝ b✝ : α
⊢ e (a✝ ⊔ b✝) = e a✝ ⊔ e b✝

Tactic:
first | rfl | exact e.apply_symm_apply _

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

Goal state before:
pp: case map_inf
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
e : α ≃ β
inst✝ : CompleteLattice β
top : Top α := e.top
bot : Bot α := e.bot
supSet : SupSet α := e.supSet
infSet : InfSet α := e.infSet
lattice : Lattice α := e.lattice
a✝ b✝ : α
⊢ e (a✝ ⊓ b✝) = e a✝ ⊓ e b✝

Tactic:
first | rfl | exact e.apply_symm_apply _

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

Goal state before:
pp: case map_sSup
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
e : α ≃ β
inst✝ : CompleteLattice β
top : Top α := e.top
bot : Bot α := e.bot
supSet : SupSet α := e.supSet
infSet : InfSet α := e.infSet
lattice : Lattice α := e.lattice
s✝ : Set α
⊢ e (sSup s✝) = ⨆ a ∈ s✝, e a

Tactic:
first | rfl | exact e.apply_symm_apply _

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

Goal state before:
pp: case map_sInf
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
e : α ≃ β
inst✝ : CompleteLattice β
top : Top α := e.top
bot : Bot α := e.bot
supSet : SupSet α := e.supSet
infSet : InfSet α := e.infSet
lattice : Lattice α := e.lattice
s✝ : Set α
⊢ e (sInf s✝) = ⨅ a ∈ s✝, e a

Tactic:
first | rfl | exact e.apply_symm_apply _

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

Goal state before:
pp: case map_top
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
e : α ≃ β
inst✝ : CompleteLattice β
top : Top α := ⋯
bot : Bot α := ⋯
supSet : SupSet α := ⋯
infSet : InfSet α := ⋯
lattice : Lattice α := ⋯
⊢ e ⊤ = ⊤

Tactic:
first | rfl | exact e.apply_symm_apply _

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

Goal state before:
pp: case map_bot
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
e : α ≃ β
inst✝ : CompleteLattice β
top : Top α := ⋯
bot : Bot α := ⋯
supSet : SupSet α := ⋯
infSet : InfSet α := ⋯
lattice : Lattice α := ⋯
⊢ e ⊥ = ⊥

Tactic:
first | rfl | exact e.apply_symm_apply _

Goal state after:
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) ⊓ ⨆ i, g i ≤ ⨆ i, f i ⊓ g i

Tactic:
rw [iSup_inf_iSup]

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

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set α
a : α
h : ∀ b ∈ s, b ≤ a
⊢ sSup s ≤ a

Tactic:
exact csSup_le' h

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case le
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Frame β
completeLattice : CompleteLattice α := e.completeLattice
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
x✝ y✝ : α
⊢ e x✝ ≤ e y✝ ↔ x✝ ≤ y✝

Tactic:
first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case lt
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Frame β
completeLattice : CompleteLattice α := e.completeLattice
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
x✝ y✝ : α
⊢ e x✝ < e y✝ ↔ x✝ < y✝

Tactic:
first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_sup
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Frame β
completeLattice : CompleteLattice α := e.completeLattice
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
a✝ b✝ : α
⊢ e (a✝ ⊔ b✝) = e a✝ ⊔ e b✝

Tactic:
first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_inf
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Frame β
completeLattice : CompleteLattice α := e.completeLattice
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
a✝ b✝ : α
⊢ e (a✝ ⊓ b✝) = e a✝ ⊓ e b✝

Tactic:
first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_sSup
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Frame β
completeLattice : CompleteLattice α := e.completeLattice
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
s✝ : Set α
⊢ e (sSup s✝) = ⨆ a ∈ s✝, e a

Tactic:
first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_sInf
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Frame β
completeLattice : CompleteLattice α := e.completeLattice
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
s✝ : Set α
⊢ e (sInf s✝) = ⨅ a ∈ s✝, e a

Tactic:
first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_top
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Frame β
completeLattice : CompleteLattice α := ⋯
heytingAlgebra : HeytingAlgebra α := ⋯
⊢ e ⊤ = ⊤

Tactic:
first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_bot
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Frame β
completeLattice : CompleteLattice α := ⋯
heytingAlgebra : HeytingAlgebra α := ⋯
⊢ e ⊥ = ⊥

Tactic:
first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_compl
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Frame β
completeLattice : CompleteLattice α := e.completeLattice
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
a✝ : α
⊢ e a✝ᶜ = (e a✝)ᶜ

Tactic:
first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_himp
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Frame β
completeLattice : CompleteLattice α := e.completeLattice
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
a✝ b✝ : α
⊢ e (a✝ ⇨ b✝) = e a✝ ⇨ e b✝

Tactic:
first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case le
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Coframe β
completeLattice : CompleteLattice α := e.completeLattice
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
x✝ y✝ : α
⊢ e x✝ ≤ e y✝ ↔ x✝ ≤ y✝

Tactic:
first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case lt
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Coframe β
completeLattice : CompleteLattice α := e.completeLattice
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
x✝ y✝ : α
⊢ e x✝ < e y✝ ↔ x✝ < y✝

Tactic:
first | rfl | exact e.apply_symm_apply _

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

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set α
hs : s.Nonempty
h's : BddBelow s
⊢ ↑(sInf s) = ⨅ a ∈ s, ↑a

Tactic:
by
  rw [coe_sInf' hs h's, sInf_image]

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_sup
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Coframe β
completeLattice : CompleteLattice α := e.completeLattice
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
a✝ b✝ : α
⊢ e (a✝ ⊔ b✝) = e a✝ ⊔ e b✝

Tactic:
first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_inf
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Coframe β
completeLattice : CompleteLattice α := e.completeLattice
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
a✝ b✝ : α
⊢ e (a✝ ⊓ b✝) = e a✝ ⊓ e b✝

Tactic:
first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_sSup
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Coframe β
completeLattice : CompleteLattice α := e.completeLattice
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
s✝ : Set α
⊢ e (sSup s✝) = ⨆ a ∈ s✝, e a

Tactic:
first | rfl | exact e.apply_symm_apply _

Goal state after: