mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Tactic.NormNum.Inv

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

Tactic:
;

Goal state after:
n✝¹ num✝ n✝ denom✝ : ℕ
inv✝ : Invertible ↑denom✝
h : ↑n✝¹ / ↑n✝ = ↑num✝ * ⅟↑denom✝
⊢ IsNNRat (↑↑n✝¹ / ↑↑n✝) num✝ denom✝
Module: Mathlib.Tactic.NormNum.Inv

Goal state before:
pp: R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
num✝ denom✝ : ℕ
qi : ℚ
invOf_mul_self✝ : qi * ↑denom✝ = 1
mul_invOf_self✝ : ↑denom✝ * qi = 1
⊢ ↑(↑num✝ * qi) = ↑num✝ * ↑qi

Tactic:
;

Goal state after:
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
num✝ denom✝ : ℕ
qi : ℚ
invOf_mul_self✝ : qi * ↑denom✝ = 1
mul_invOf_self✝ : ↑denom✝ * qi = 1
⊢ ↑(↑num✝ * qi) = ↑num✝ * ↑qi
Module: Mathlib.Tactic.NormNum.Inv

Goal state before:
pp: R : Type u_1
inst✝¹ : DivisionSemiring R
inst✝ : CharZero R
num✝ denom✝ : ℕ
qi : ℚ≥0
invOf_mul_self✝ : qi * ↑denom✝ = 1
mul_invOf_self✝ : ↑denom✝ * qi = 1
⊢ ↑(↑num✝ * qi) = ↑num✝ * ↑qi

Tactic:
;

Goal state after:
R : Type u_1
inst✝¹ : DivisionSemiring R
inst✝ : CharZero R
num✝ denom✝ : ℕ
qi : ℚ≥0
invOf_mul_self✝ : qi * ↑denom✝ = 1
mul_invOf_self✝ : ↑denom✝ * qi = 1
⊢ ↑(↑num✝ * qi) = ↑num✝ * ↑qi
Module: Mathlib.Tactic.NormNum.Inv

Goal state before:
pp: R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
num✝ : ℤ
denom✝ : ℕ
qi : ℚ
invOf_mul_self✝ : qi * ↑denom✝ = 1
mul_invOf_self✝ : ↑denom✝ * qi = 1
⊢ ↑(↑num✝ * qi) = ↑num✝ * ↑qi

Tactic:
;

Goal state after:
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
num✝ : ℤ
denom✝ : ℕ
qi : ℚ
invOf_mul_self✝ : qi * ↑denom✝ = 1
mul_invOf_self✝ : ↑denom✝ * qi = 1
⊢ ↑(↑num✝ * qi) = ↑num✝ * ↑qi
Module: Mathlib.Tactic.NormNum.Inv

Goal state before:
pp: case eq
α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n✝ d : ℕ
inv✝ : Invertible ↑d
n : ℕ
this : Invertible ↑n
⊢ (↑(-Int.ofNat n) * ⅟↑d)⁻¹ = ↑(-Int.ofNat d) * ⅟↑n

Tactic:
;

Goal state after:
case eq
α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n✝ d : ℕ
inv✝ : Invertible ↑d
n : ℕ
this : Invertible ↑n
⊢ (↑(-Int.ofNat n) * ⅟↑d)⁻¹ = ↑(-Int.ofNat d) * ⅟↑n
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: α : Type u_3
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a /. b = n /. ↑d
d0 : ↑d ≠ 0
⊢ ↑{ num := n, den := d, den_nz := h, reduced := c } = ↑a / ↑b

Tactic:
have := congr_arg ((↑) : ℤ → α)
    ((divInt_eq_divInt_iff b0' <| ne_of_gt <| Int.natCast_pos.2 h.bot_lt).1 e)

Goal state after:
α : Type u_3
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a /. b = n /. ↑d
d0 : ↑d ≠ 0
this : ↑(a * ↑d) = ↑(n * b)
⊢ ↑{ num := n, den := d, den_nz := h, reduced := c } = ↑a / ↑b
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: case b0
α : Type u_3
inst✝ : DivisionRing α
a : ℤ
b : ℕ
hb : ↑b ≠ 0
⊢ ↑↑b ≠ 0

Tactic:
;

Goal state after:
case b0
α : Type u_3
inst✝ : DivisionRing α
a : ℤ
b : ℕ
hb : ↑b ≠ 0
⊢ ↑↑b ≠ 0
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: case pos
n : ℤ
hn : n = 0
⊢ ↑(n / n) = ↑n / ↑n

pp: case neg
n : ℤ
hn : ¬n = 0
⊢ ↑(n / n) = ↑n / ↑n

Tactic:
· subst hn
    simp

Goal state after:
case neg
n : ℤ
hn : ¬n = 0
⊢ ↑(n / n) = ↑n / ↑n
Module: Mathlib.Tactic.NormNum.Pow

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

Tactic:
;

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

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

Tactic:
;

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a₁ a₃ a₂ : ℕ
⊢ ↑(a₁ ^ a₂ * a₃) = ↑a₁ ^ a₂ * ↑a₃

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a₁ a₃ a₂ : ℕ
⊢ ↑(a₁ ^ a₂ * a₃) = ↑a₁ ^ a₂ * ↑a₃
Module: Mathlib.Tactic.Ring.Basic

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

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a₁ a₂ : ℕ
⊢ ↑(a₁ + a₂) = ↑a₁ + ↑a₂
Module: Mathlib.Tactic.Ring.Basic

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
a₁ a₃ : ℤ
a₂ : ℕ
⊢ ↑(a₁ ^ a₂ * a₃) = ↑a₁ ^ a₂ * ↑a₃

Tactic:
;

Goal state after:
R : Type u_2
inst✝ : CommRing R
a₁ a₃ : ℤ
a₂ : ℕ
⊢ ↑(a₁ ^ a₂ * a₃) = ↑a₁ ^ a₂ * ↑a₃
Module: Mathlib.Tactic.Ring.Basic

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
a₁ a₂ : ℤ
⊢ ↑(a₁ + a₂) = ↑a₁ + ↑a₂

Tactic:
;

Goal state after:
R : Type u_2
inst✝ : CommRing R
a₁ a₂ : ℤ
⊢ ↑(a₁ + a₂) = ↑a₁ + ↑a₂
Module: Mathlib.Tactic.Ring.Basic

Goal state before:
pp: α : Sort u_2
c : α
⊢ c = c

Tactic:
;

Goal state after:
α : Sort u_2
c : α
⊢ c = c
Module: Mathlib.Data.Tree.Basic

Goal state before:
pp: α : Type u
β : Type u_1
γ : Type u_2
f : α → β
g : β → γ
t : BinaryTree α
⊢ map (g ∘ f) t = map g (map f t)

Tactic:
induction t with
  | nil => rw [map, map, map]
  | node v l r hl hr => rw [map, map, map, hl, hr, Function.comp_apply]

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a b x : R
e : ℕ
⊢ x ^ e * a + x ^ e * b = x ^ e * (a + b)

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a b x : R
e : ℕ
⊢ x ^ e * a + x ^ e * b = x ^ e * (a + b)
Module: Mathlib.Tactic.Ring.Common

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

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a₁ a₂ b₁ b₂ : R
⊢ a₁ + a₂ + (b₁ + b₂) = a₁ + b₁ + (a₂ + b₂)
Module: Mathlib.Tactic.Ring.Common

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

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a₁ a₂ b₁ b₂ : R
h : IsNat (a₁ + b₁) 0
⊢ a₁ + a₂ + (b₁ + b₂) = a₂ + 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:
;

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a b₂ b₁ : R
⊢ a + (b₁ + b₂) = b₁ + (a + b₂)
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a₃ b a₁ : R
a₂ : ℕ
⊢ a₁ ^ a₂ * a₃ * b = a₁ ^ a₂ * (a₃ * b)

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a₃ b a₁ : R
a₂ : ℕ
⊢ a₁ ^ a₂ * a₃ * b = a₁ ^ a₂ * (a₃ * b)
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a b₃ b₁ : R
b₂ : ℕ
⊢ a * (b₁ ^ b₂ * b₃) = b₁ ^ b₂ * (a * b₃)

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a b₃ b₁ : R
b₂ : ℕ
⊢ a * (b₁ ^ b₂ * b₃) = b₁ ^ b₂ * (a * b₃)
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a₂ b₂ : R
ea eb : ℕ
x : R
⊢ x ^ ea * a₂ * (x ^ eb * b₂) = x ^ (ea + eb) * (a₂ * b₂)

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a₂ b₂ : R
ea eb : ℕ
x : R
⊢ x ^ ea * a₂ * (x ^ eb * b₂) = x ^ (ea + eb) * (a₂ * b₂)
Module: Mathlib.Algebra.Order.Ring.Canonical

Goal state before:
pp: R : Type u
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : CanonicallyOrderedAdd R
inst✝ : Nontrivial R
k : R
⊢ 0 < 2 * k + 1

Tactic:
;

Goal state after:
R : Type u
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : CanonicallyOrderedAdd R
inst✝ : Nontrivial R
k : R
⊢ 0 < 2 * k + 1
Module: Mathlib.Tactic.Ring.Common

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

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a b₁ b₂ : R
⊢ a * (b₁ + b₂) = a * b₁ + 0 + a * b₂
Module: Mathlib.Tactic.Ring.Common

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

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a₁ a₂ b : R
⊢ (a₁ + a₂) * b = a₁ * b + a₂ * b
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
a : R
⊢ -a = -1 * a

Tactic:
;

Goal state after:
R : Type u_2
inst✝ : CommRing R
a : R
⊢ -a = -1 * a
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
a₁ : R
a₂ : ℕ
a₃ : R
⊢ -(a₁ ^ a₂ * a₃) = a₁ ^ a₂ * -a₃

Tactic:
;

Goal state after:
R : Type u_2
inst✝ : CommRing R
a₁ : R
a₂ : ℕ
a₃ : R
⊢ -(a₁ ^ a₂ * a₃) = a₁ ^ a₂ * -a₃
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
a₁ a₂ : R
⊢ -(a₁ + a₂) = -a₁ + -a₂

Tactic:
;

Goal state after:
R : Type u_2
inst✝ : CommRing R
a₁ a₂ : R
⊢ -(a₁ + a₂) = -a₁ + -a₂
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
a b : R
⊢ a - b = a + -b

Tactic:
;

Goal state after:
R : Type u_2
inst✝ : CommRing R
a b : R
⊢ a - b = a + -b
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a : R
k : ℕ
⊢ a ^ Nat.mul 2 k = a ^ k * a ^ k

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a : R
k : ℕ
⊢ a ^ Nat.mul 2 k = a ^ k * a ^ k
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a : R
k : ℕ
⊢ a ^ (Nat.mul 2 k).add 1 = a ^ k * a ^ k * a

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a : R
k : ℕ
⊢ a ^ (Nat.mul 2 k).add 1 = a ^ k * a ^ k * a
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a₂ : R
ea₁ b : ℕ
xa₁ : R
⊢ (xa₁ ^ ea₁ * a₂) ^ b = xa₁ ^ (ea₁ * b) * a₂ ^ b

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a₂ : R
ea₁ b : ℕ
xa₁ : R
⊢ (xa₁ ^ ea₁ * a₂) ^ b = xa₁ ^ (ea₁ * b) * a₂ ^ b
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a₂ : R
ea₁ b : ℕ
xa₁ : R
⊢ (xa₁ ^ ea₁ * a₂) ^ b = xa₁ ^ (ea₁ * b) * Nat.rawCast 1 * a₂ ^ b

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a₂ : R
ea₁ b : ℕ
xa₁ : R
⊢ (xa₁ ^ ea₁ * a₂) ^ b = xa₁ ^ (ea₁ * b) * Nat.rawCast 1 * a₂ ^ b
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: c₂ k a₁ a₂ : ℕ
⊢ a₁ ^ a₂ * (c₂ * k) = a₁ ^ a₂ * c₂ * k

Tactic:
;

Goal state after:
c₂ k a₁ a₂ : ℕ
⊢ a₁ ^ a₂ * (c₂ * k) = a₁ ^ a₂ * c₂ * k
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a : R
c k : ℕ
⊢ a ^ (c * k) = (a ^ c) ^ k

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a : R
c k : ℕ
⊢ a ^ (c * k) = (a ^ c) ^ k
Module: Mathlib.Tactic.Ring.Common

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

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a : R
b₁ b₂ : ℕ
⊢ a ^ (b₁ + b₂) = a ^ b₁ * a ^ b₂
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_2
inst✝ : Semifield R
a₁ : R
a₂ : ℕ
a₃ : R
⊢ (a₁ ^ a₂ * a₃)⁻¹ = a₃⁻¹ * (a₁⁻¹ ^ a₂ * Nat.rawCast 1)

Tactic:
;

Goal state after:
R : Type u_2
inst✝ : Semifield R
a₁ : R
a₂ : ℕ
a₃ : R
⊢ (a₁ ^ a₂ * a₃)⁻¹ = a₃⁻¹ * (a₁⁻¹ ^ a₂ * Nat.rawCast 1)
Module: Mathlib.Tactic.Ring.Common

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

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a₁ a₂ : ℕ
⊢ ↑(a₁ + a₂) = ↑a₁ + ↑a₂
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_2
inst✝ : Semifield R
a b : R
⊢ a / b = a * b⁻¹

Tactic:
;

Goal state after:
R : Type u_2
inst✝ : Semifield R
a b : R
⊢ a / b = a * b⁻¹
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a' b' : R
⊢ a' + b' = a' + b'

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a' b' : R
⊢ a' + b' = a' + b'
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a' b' : R
⊢ a' * b' = a' * b'

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a' b' : R
⊢ a' * b' = a' * b'
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
b' : R
a' : ℕ
⊢ a' • b' = a' • b'

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
b' : R
a' : ℕ
⊢ a' • b' = a' • b'
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
b' : R
a' : ℤ
⊢ a' • b' = a' • b'

Tactic:
;

Goal state after:
R : Type u_2
inst✝ : CommRing R
b' : R
a' : ℤ
⊢ a' • b' = a' • b'
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a' : R
b' : ℕ
⊢ a' ^ b' = a' ^ b'

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a' : R
b' : ℕ
⊢ a' ^ b' = a' ^ b'
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
a' : R
⊢ -a' = -a'

Tactic:
;

Goal state after:
R : Type u_2
inst✝ : CommRing R
a' : R
⊢ -a' = -a'
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
a' b' : R
⊢ a' - b' = a' - b'

Tactic:
;

Goal state after:
R : Type u_2
inst✝ : CommRing R
a' b' : R
⊢ a' - b' = a' - b'
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_2
inst✝ : Semifield R
a' : R
⊢ a'⁻¹ = a'⁻¹

Tactic:
;

Goal state after:
R : Type u_2
inst✝ : Semifield R
a' : R
⊢ a'⁻¹ = a'⁻¹
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_2
inst✝ : Semifield R
a' b' : R
⊢ a' / b' = a' / b'

Tactic:
;

Goal state after:
R : Type u_2
inst✝ : Semifield R
a' b' : R
⊢ a' / b' = a' / b'
Module: Mathlib.Data.Nat.Set

Goal state before:
pp: case e'_4.succ
α : Type u_2
x : α
f : ℕ → α → α
n : ℕ
ihn : rec (f 0 x) (f ∘ succ) n = f n (rec x f n)
⊢ f (n + 1) (rec (f 0 x) (f ∘ succ) n) = f (n + 1) (f n (rec x f n))

Tactic:
;

Goal state after:
case e'_4.succ
α : Type u_2
x : α
f : ℕ → α → α
n : ℕ
ihn : rec (f 0 x) (f ∘ succ) n = f n (rec x f n)
⊢ f (n + 1) (rec (f 0 x) (f ∘ succ) n) = f (n + 1) (f n (rec x f n))
Module: Mathlib.Order.CompleteLattice.Defs

Goal state before:
pp: α : Type u_1
inst✝ : CompleteSemilatticeSup α
s : Set α
⊢ IsLUB s (sSup s)

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : CompleteSemilatticeSup α
s : Set α
⊢ IsLUB s (sSup s)
Module: Mathlib.Order.CompleteLattice.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
f : ℕ → α
⊢ ⨅ i, ⨅ (_ : i > 0), f i = ⨅ i, f (i + 1)

Tactic:
← iInf_range,

Goal state after:
α : Type u_1
inst✝ : CompleteLattice α
f : ℕ → α
⊢ ⨅ i, ⨅ (_ : i > 0), f i = ⨅ b ∈ range fun i ↦ i + 1, f b
Module: Mathlib.Order.CompleteLattice.Lemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
a✝ b✝ c✝ : PUnit
⊢ a✝ ≤ b✝ ⇨ c✝ ↔ min a✝ b✝ ≤ c✝

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
a✝ b✝ c✝ : PUnit
⊢ a✝ ≤ b✝ ⇨ c✝ ↔ min a✝ b✝ ≤ c✝
Module: Mathlib.Order.CompleteLattice.Lemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
a✝ : PUnit
⊢ a✝ ⇨ ⊥ = a✝ᶜ

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
a✝ : PUnit
⊢ a✝ ⇨ ⊥ = a✝ᶜ
Module: Mathlib.Order.CompleteLattice.Lemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
a✝ b✝ c✝ : PUnit
⊢ a✝ \ b✝ ≤ c✝ ↔ a✝ ≤ max b✝ c✝

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
a✝ b✝ c✝ : PUnit
⊢ a✝ \ b✝ ≤ c✝ ↔ a✝ ≤ max b✝ c✝
Module: Mathlib.Order.CompleteLattice.Lemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
a✝ : PUnit
⊢ ⊤ \ a✝ = ￢a✝

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
a✝ : PUnit
⊢ ⊤ \ a✝ = ￢a✝
Module: Mathlib.Data.Set.BooleanAlgebra

Goal state before:
pp: α ι✝ : Type u_1
κ✝ : ι✝ → Type u_1
f✝ : (a : ι✝) → κ✝ a → Set α
⊢ ⨅ a, ⨆ b, f✝ a b = ⨆ g, ⨅ a, f✝ a (g a)

Tactic:
;

Goal state after:
α ι✝ : Type u_1
κ✝ : ι✝ → Type u_1
f✝ : (a : ι✝) → κ✝ a → Set α
⊢ ⨅ a, ⨆ b, f✝ a b = ⨆ g, ⨅ a, f✝ a (g a)
Module: Mathlib.Data.Set.BooleanAlgebra

Goal state before:
pp: α ι✝ : Type u_1
κ✝ : ι✝ → Type u_1
f✝ : (a : ι✝) → κ✝ a → Set α
x✝ : α
⊢ x✝ ∈ ⨅ a, ⨆ b, f✝ a b ↔ x✝ ∈ ⨆ g, ⨅ a, f✝ a (g a)

Tactic:
;

Goal state after:
α ι✝ : Type u_1
κ✝ : ι✝ → Type u_1
f✝ : (a : ι✝) → κ✝ a → Set α
x✝ : α
⊢ x✝ ∈ ⨅ a, ⨆ b, f✝ a b ↔ x✝ ∈ ⨆ g, ⨅ a, f✝ a (g a)
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 (l '' range f) (l (sSup (range f)))

Tactic:
;

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.GaloisConnection.Basic

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

Tactic:
;

Goal state after:
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a₁ a₂ : α
b₁ b₂ : β
l : α → β
u : β → α
inst✝¹ : PartialOrder β
inst✝ : SemilatticeInf α
gi : GaloisInsertion l u
⊢ ∀ (a b : β), l (u a ⊓ u b) ≤ a
Module: Mathlib.Order.GaloisConnection.Basic

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

Tactic:
simp only [gi.choice_eq]; exact fun a b => gi.gc.l_le inf_le_left

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

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

Tactic:
;

Goal state after:
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a₁ a₂ : α
b₁ b₂ : β
l : α → β
u : β → α
inst✝¹ : PartialOrder β
inst✝ : SemilatticeInf α
gi : GaloisInsertion l u
⊢ ∀ (a b : β), l (u a ⊓ u b) ≤ b
Module: Mathlib.Order.GaloisConnection.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a₁ a₂ : α
b₁ b₂ : β
l : α → β
u : β → α
inst✝² : PartialOrder β
inst✝¹ : Preorder α
inst✝ : OrderTop α
gi : GaloisInsertion l u
⊢ ∀ (a : β), a ≤ l ⊤

Tactic:
;

Goal state after:
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a₁ a₂ : α
b₁ b₂ : β
l : α → β
u : β → α
inst✝² : PartialOrder β
inst✝¹ : Preorder α
inst✝ : OrderTop α
gi : GaloisInsertion l u
⊢ ∀ (a : β), a ≤ l ⊤
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
ι : Type u_8
inst✝ : SupSet α
f : ULift ι → α
⊢ sSup (range fun i ↦ f i) = sSup (range fun i ↦ f { down := i })

Tactic:
;

Goal state after:
α : Type u_1
ι : Type u_8
inst✝ : SupSet α
f : ULift ι → α
⊢ sSup (range fun i ↦ f i) = sSup (range fun i ↦ f { down := i })
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
ι : Type u_8
inst✝ : SupSet α
f : ULift ι → α
x : α
⊢ (x ∈ range fun i ↦ f i) ↔ x ∈ range fun i ↦ f { down := i }

Tactic:
;

Goal state after:
α : Type u_1
ι : Type u_8
inst✝ : SupSet α
f : ULift ι → α
x : α
⊢ (x ∈ range fun i ↦ f i) ↔ x ∈ range fun i ↦ f { down := i }
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
ι' : Sort u_5
inst✝ : SupSet α
f : ι → ι'
hf : Surjective f
g : ι' → α
⊢ ⨆ x, g (f x) = ⨆ y, g y

Tactic:
by
  simp only [iSup.eq_1]
  congr
  exact hf.range_comp g

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 (⨆ a ∈ s, a)

Tactic:
;

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.Order.CompleteLattice.Basic

Goal state before:
pp: case a
α : Type u_1
inst✝² : CompleteLattice α
ι : Type u_8
inst✝¹ : LT ι
inst✝ : NoMaxOrder ι
f : ι → α
j i : ι
jlt : j < i
⊢ f j ≤ ⨆ i, ⨆ j, ⨆ (_ : j < i), f j

Tactic:
exact le_iSup_of_le i (le_iSup₂_of_le j jlt le_rfl)

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

Goal state before:
pp: case a
α : Type u_1
inst✝² : CompleteLattice α
ι : Type u_8
inst✝¹ : LT ι
inst✝ : NoMinOrder ι
f : ι → α
j i : ι
jlt : i < j
⊢ f j ≤ ⨆ i, ⨆ j, ⨆ (_ : j > i), f j

Tactic:
exact le_iSup_of_le i (le_iSup₂_of_le j jlt le_rfl)

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

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

Tactic:
rw [iSup, minAx.sSup_inf_eq, iSup_range]

Goal state after:
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:
iSup_prod,

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

Goal state before:
pp: α : Type u_1
s t : Set α
S : Set (Set α)
hs : t ∈ S
h : s ∩ ⋃₀ S = ∅
⊢ s ∩ t ⊆ s ∩ ⋃₀ S

Tactic:
;

Goal state after:
α : Type u_1
s t : Set α
S : Set (Set α)
hs : t ∈ S
h : s ∩ ⋃₀ S = ∅
⊢ s ∩ t ⊆ s ∩ ⋃₀ S
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_12
β : Type u_13
C : Set (Set α)
f : (s : ↑C) → β → ↑↑s
hf : ∀ (s : ↑C), Surjective (f s)
x : α
⊢ (x ∈ ⋃ y, range fun s ↦ ↑(f s y)) ↔ x ∈ ⋃₀ C

Tactic:
;

Goal state after:
α : Type u_12
β : Type u_13
C : Set (Set α)
f : (s : ↑C) → β → ↑↑s
hf : ∀ (s : ↑C), Surjective (f s)
x : α
⊢ (x ∈ ⋃ y, range fun s ↦ ↑(f s y)) ↔ x ∈ ⋃₀ C
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
α : Type u_8
β : α → Type u_9
inst✝ : (i : α) → CompleteLattice (β i)
x✝¹ : Set ((i : α) → β i)
x✝ : α
⊢ IsLUB (eval x✝ '' x✝¹) (sSup (eval x✝ '' x✝¹))

Tactic:
;

Goal state after:
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
α : Type u_8
β : α → Type u_9
inst✝ : (i : α) → CompleteLattice (β i)
x✝¹ : Set ((i : α) → β i)
x✝ : α
⊢ IsLUB (eval x✝ '' x✝¹) (sSup (eval x✝ '' x✝¹))
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
C : ι → Set α
f : (x : ι) → β → ↑(C x)
hf : ∀ (x : ι), Surjective (f x)
x : α
⊢ (x ∈ ⋃ y, range fun x ↦ ↑(f x y)) ↔ x ∈ ⋃ x, C x

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
ι : Sort u_5
C : ι → Set α
f : (x : ι) → β → ↑(C x)
hf : ∀ (x : ι), Surjective (f x)
x : α
⊢ (x ∈ ⋃ y, range fun x ↦ ↑(f x y)) ↔ x ∈ ⋃ x, C x
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
α : Type u_8
β : α → Type u_9
inst✝ : (i : α) → CompleteLattice (β i)
x✝¹ : Set ((i : α) → β i)
x✝ : α
⊢ IsGLB (eval x✝ '' x✝¹) (sInf (eval x✝ '' x✝¹))

Tactic:
;

Goal state after:
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
α : Type u_8
β : α → Type u_9
inst✝ : (i : α) → CompleteLattice (β i)
x✝¹ : Set ((i : α) → β i)
x✝ : α
⊢ IsGLB (eval x✝ '' x✝¹) (sInf (eval x✝ '' x✝¹))