mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Set.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
⊢ image2 f s t = ∅ ↔ s = ∅ ∨ t = ∅

Tactic:
rw [← not_nonempty_iff_eq_empty, image2_nonempty_iff, not_and_or]

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
⊢ ¬s.Nonempty ∨ ¬t.Nonempty ↔ s = ∅ ∨ t = ∅
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: α : Type u_1
inst✝² : CommRing α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedRing α
a : ℤˣ
⊢ |↑↑a| = 1

Tactic:
cases Int.units_eq_one_or a <;> simp_all

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

Goal state before:
pp: α✝¹ : Sort u
β✝ : Sort v
γ : Sort w
α✝ : Type u_1
β : Type u_2
α : Type ?u.8
S : Set α
x : ↑(𝒫 S)
⊢ (fun x ↦ ⟨Subtype.val '' x, ⋯⟩) ((fun x ↦ Subtype.val ⁻¹' ↑x) x) = x

Tactic:
ext y

Goal state after:
α✝¹ : Sort u
β✝ : Sort v
γ : Sort w
α✝ : Type u_1
β : Type u_2
α : Type ?u.8
S : Set α
x : ↑(𝒫 S)
y : α
⊢ y ∈ ↑((fun x ↦ ⟨Subtype.val '' x, ⋯⟩) ((fun x ↦ Subtype.val ⁻¹' ↑x) x)) ↔ y ∈ ↑x
Module: Mathlib.Order.Bounds.Basic

Goal state before:
pp: case refine_2.inl
α : Type u_1
inst✝ : Preorder α
s t : Set α
hs : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
hts : IsCofinalFor t s
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
⊢ ∃ z ∈ s ∪ t, (fun x1 x2 ↦ x1 ≤ x2) x z ∧ (fun x1 x2 ↦ x1 ≤ x2) y z

pp: case refine_2.inr
α : Type u_1
inst✝ : Preorder α
s t : Set α
ht : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) t
hst : IsCofinalFor s t
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
⊢ ∃ z ∈ s ∪ t, (fun x1 x2 ↦ x1 ≤ x2) x z ∧ (fun x1 x2 ↦ x1 ≤ x2) y z

Tactic:
· obtain ⟨x', hx', hxx'⟩ := hts.union_right hx
      obtain ⟨y', hy', hyy'⟩ := hts.union_right hy
      obtain ⟨z, hz, hx'z, hy'z⟩ := hs x' hx' y' hy'
      exact ⟨z, .inl hz, hxx'.trans hx'z, hyy'.trans hy'z⟩

Goal state after:
case refine_2.inr
α : Type u_1
inst✝ : Preorder α
s t : Set α
ht : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) t
hst : IsCofinalFor s t
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
⊢ ∃ z ∈ s ∪ t, (fun x1 x2 ↦ x1 ≤ x2) x z ∧ (fun x1 x2 ↦ x1 ≤ x2) y z
Module: Mathlib.Order.Bounds.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
s t : Set α
a : α
ha : a ∈ upperBounds s
b : α
hb : b ∈ upperBounds t
c : α
hca : a ≤ c
hcb : b ≤ c
⊢ BddAbove (s ∪ t)

Tactic:
BddAbove,

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
s t : Set α
a : α
ha : a ∈ upperBounds s
b : α
hb : b ∈ upperBounds t
c : α
hca : a ≤ c
hcb : b ≤ c
⊢ (upperBounds (s ∪ t)).Nonempty
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a : α
⊢ a⁻¹ < 0 ↔ a < 0

Tactic:
by
  rw [← neg_pos, ← inv_neg, inv_pos, neg_pos]

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

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

Tactic:
div_le_iff_of_neg hc,

Goal state after:
α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b c : α
hc : c < 0
⊢ b / c * c ≤ a ↔ b ≤ a
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
a✝ : α
b✝ : β
l₁✝ : List α
l₂✝ : List β
h₂ : Forall₂ R l₁✝ l₂✝
x : α
y : β
hx : (x, y) = (a✝, b✝) ∨ (x, y) ∈ zipWith Prod.mk l₁✝ l₂✝
x✝¹ : β
x✝ : α
h₃ : (x, y) ∈ zipWith Prod.mk l₁✝ l₂✝
h₁ : R x✝ x✝¹
⊢ R x y

Tactic:
exact forall₂_zip h₂ h₃

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
R : α → β → Prop
p : α → Bool
q : β → Bool
hpq : ∀ ⦃a : α⦄ ⦃b : β⦄, R a b → (p a = true ↔ q b = true)
a : α
as : List α
b : β
bs : List β
h₁ : R a b
h₂ : Forall₂ R as bs
h : ¬p a = true
⊢ Forall₂ R (filter p (a :: as)) (filter q (b :: bs))

Tactic:
· have : ¬q b := by rwa [← hpq h₁]
      simp only [filter_cons_of_neg h, filter_cons_of_neg this, rel_filter hpq h₂]

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

Goal state before:
pp: M : Type u_4
inst✝ : LeftCancelMonoid M
L L' : List M
h : L.length = L'.length
h' : ∀ (i : ℕ), i ≤ L.length → (take i L).prod = (take i L').prod
⊢ L = L'

Tactic:
refine ext_get h fun i h₁ h₂ => ?_

Goal state after:
M : Type u_4
inst✝ : LeftCancelMonoid M
L L' : List M
h : L.length = L'.length
h' : ∀ (i : ℕ), i ≤ L.length → (take i L).prod = (take i L').prod
i : ℕ
h₁ : i < L.length
h₂ : i < L'.length
⊢ L.get ⟨i, h₁⟩ = L'.get ⟨i, h₂⟩
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
β : Type v
b₁ b₂ : β
l : List α
h : b₁ ∈ map (const α b₂) l
⊢ b₁ = b₂

Tactic:
map_const

Goal state after:
α : Type u
β : Type v
b₁ b₂ : β
l : List α
h : b₁ ∈ replicate l.length b₂
⊢ b₁ = b₂
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
β : Type v
b₁ b₂ : β
l : List α
h : b₁ ∈ map (const α b₂) l
⊢ b₁ = b₂

Tactic:
rw [map_const] at h; exact eq_of_mem_replicate h

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

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

Tactic:
obtain ⟨a, ha⟩ := a
  simp [toNonneg, ha.not_gt]

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

Goal state before:
pp: x : ℤ
hx : x ≠ 0
n d : ℤ
⊢ n /. x * (x /. d) = n /. d

Tactic:
divInt_mul_divInt_cancel hx

Goal state after:
x : ℤ
hx : x ≠ 0
n d : ℤ
⊢ n /. d = n /. d
Module: Mathlib.Algebra.Ring.Rat

Goal state before:
pp: x : ℤ
hx : x ≠ 0
n d : ℤ
⊢ d /. x * (x /. n) = d /. n

Tactic:
divInt_mul_divInt_cancel hx

Goal state after:
x : ℤ
hx : x ≠ 0
n d : ℤ
⊢ d /. n = d /. n
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:
List.disjoint_left,

Goal state after:
α : Type u
l₁ l₂ l : List α
p : l₁ ~ l₂
⊢ (∀ ⦃a : α⦄, a ∈ l₁ → ¬a ∈ l) ↔ ∀ ⦃a : α⦄, a ∈ l₂ → ¬a ∈ l
Module: Mathlib.Data.NNRat.Defs

Goal state before:
pp: n₁ n₂ d₁ d₂ : ℕ
⊢ divNat n₁ d₁ * divNat n₂ d₂ = divNat (n₁ * n₂) (d₁ * d₂)

Tactic:
ext; push_cast; exact Rat.divInt_mul_divInt _ _

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

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

Tactic:
subst_vars

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
b₁ b₂ : R
a₁ a₂ : ℕ
x✝¹ : ↑a₁ = b₁
x✝ : ↑a₂ = b₂
⊢ ↑(a₁ + a₂) = b₁ + b₂

Tactic:
subst_vars

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
b₁ b₃ : R
a₁ a₃ : ℤ
a₂ : ℕ
x✝¹ : ↑a₁ = b₁
x✝ : ↑a₃ = b₃
⊢ ↑(a₁ ^ a₂ * a₃) = b₁ ^ a₂ * b₃

Tactic:
subst_vars

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
b₁ b₂ : R
a₁ a₂ : ℤ
x✝¹ : ↑a₁ = b₁
x✝ : ↑a₂ = b₂
⊢ ↑(a₁ + a₂) = b₁ + b₂

Tactic:
subst_vars

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: R : Type u_1
inst✝ : CommSemiring R
n n' : ℕ
r : R
hr : ↑n = r
hn : n' = n
a : R
⊢ n' • a = r * a

Tactic:
subst_vars

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
n' : ℕ
a : R
⊢ n' • a = ↑n' * a
Module: Mathlib.Tactic.Ring.Basic

Goal state before:
pp: R : Type u_2
n n' : ℤ
r : R
inst✝ : CommRing R
hr : ↑n = r
hn : n' = n
a : R
⊢ n' • a = r * a

Tactic:
subst_vars

Goal state after:
R : Type u_2
n' : ℤ
inst✝ : CommRing R
a : R
⊢ n' • a = ↑n' * a
Module: Mathlib.Tactic.Ring.Basic

Goal state before:
pp: α : Sort u_2
a b c : α
x✝¹ : a = c
x✝ : b = c
⊢ a = b

Tactic:
subst_vars

Goal state after:
α : Sort u_2
c : α
⊢ c = c
Module: Mathlib.Tactic.Ring.Common

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

Tactic:
subst_vars

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₂ c₁ c₂ : R
x✝¹ : a₁ + b₁ = c₁
x✝ : a₂ + b₂ = c₂
⊢ a₁ + a₂ + (b₁ + b₂) = c₁ + c₂

Tactic:
subst_vars

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₂ c : R
h : IsNat (a₁ + b₁) 0
h₄ : a₂ + b₂ = c
⊢ a₁ + a₂ + (b₁ + b₂) = c

Tactic:
subst_vars

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₂ c b₁ : R
x✝ : a + b₂ = c
⊢ a + (b₁ + b₂) = b₁ + c

Tactic:
subst_vars

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 c a₁ : R
a₂ : ℕ
x✝ : a₃ * b = c
⊢ a₁ ^ a₂ * a₃ * b = a₁ ^ a₂ * c

Tactic:
subst_vars

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₃ c b₁ : R
b₂ : ℕ
x✝ : a * b₃ = c
⊢ a * (b₁ ^ b₂ * b₃) = b₁ ^ b₂ * c

Tactic:
subst_vars

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₂ c : R
ea eb e : ℕ
x : R
x✝¹ : ea + eb = e
x✝ : a₂ * b₂ = c
⊢ x ^ ea * a₂ * (x ^ eb * b₂) = x ^ e * c

Tactic:
subst_vars

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.Tactic.Ring.Common

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

Tactic:
subst_vars

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 c₁ c₂ d : R
x✝² : a₁ * b = c₁
x✝¹ : a₂ * b = c₂
x✝ : c₁ + c₂ = d
⊢ (a₁ + a₂) * b = d

Tactic:
subst_vars

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 b : R
x✝ : -1 * a = b
⊢ -a = b

Tactic:
subst_vars

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₃ b : R
x✝ : -a₃ = b
⊢ -(a₁ ^ a₂ * a₃) = a₁ ^ a₂ * b

Tactic:
subst_vars

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₂ b₁ b₂ : R
x✝¹ : -a₁ = b₁
x✝ : -a₂ = b₂
⊢ -(a₁ + a₂) = b₁ + b₂

Tactic:
subst_vars

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 c d : R
x✝¹ : -b = c
x✝ : a + c = d
⊢ a - b = d

Tactic:
subst_vars

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 b c : R
k : ℕ
x✝¹ : a ^ k = b
x✝ : b * b = c
⊢ a ^ Nat.mul 2 k = c

Tactic:
subst_vars

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 b c : R
k : ℕ
d : R
x✝² : a ^ k = b
x✝¹ : b * b = c
x✝ : c * a = d
⊢ a ^ (Nat.mul 2 k).add 1 = d

Tactic:
subst_vars

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₂ c₂ : R
ea₁ b c₁ : ℕ
xa₁ : R
x✝¹ : ea₁ * b = c₁
x✝ : a₂ ^ b = c₂
⊢ (xa₁ ^ ea₁ * a₂) ^ b = xa₁ ^ c₁ * c₂

Tactic:
subst_vars

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₂ c₂ : R
ea₁ b c₁ : ℕ
xa₁ c₃ d : R
x✝³ : ea₁ * b = c₁
x✝² : a₂ ^ b = c₂
x✝¹ : xa₁ ^ c₁ * Nat.rawCast 1 = c₃
x✝ : c₃ * c₂ = d
⊢ (xa₁ ^ ea₁ * a₂) ^ b = d

Tactic:
subst_vars

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: a₃ c₂ k a₁ a₂ : ℕ
x✝ : a₃ = c₂ * k
⊢ a₁ ^ a₂ * a₃ = a₁ ^ a₂ * c₂ * k

Tactic:
subst_vars

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
b c k : ℕ
d e : R
x✝² : b = c * k
x✝¹ : a ^ c = d
x✝ : d ^ k = e
⊢ a ^ b = e

Tactic:
subst_vars

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 c₁ c₂ : R
b₁ b₂ : ℕ
d : R
x✝² : a ^ b₁ = c₁
x✝¹ : a ^ b₂ = c₂
x✝ : c₁ * c₂ = d
⊢ a ^ (b₁ + b₂) = d

Tactic:
subst_vars

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₃ b₁ b₃ c : R
x✝² : a₁⁻¹ = b₁
x✝¹ : a₃⁻¹ = b₃
x✝ : b₃ * (b₁ ^ a₂ * Nat.rawCast 1) = c
⊢ (a₁ ^ a₂ * a₃)⁻¹ = c

Tactic:
subst_vars

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
b₁ b₂ : R
a₁ a₂ : ℕ
x✝¹ : ↑a₁ = b₁
x✝ : ↑a₂ = b₂
⊢ ↑(a₁ + a₂) = b₁ + b₂

Tactic:
subst_vars

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 c d : R
x✝¹ : b⁻¹ = c
x✝ : a * c = d
⊢ a / b = d

Tactic:
subst_vars

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 a' b b' c : R
x✝² : a = a'
x✝¹ : b = b'
x✝ : a' + b' = c
⊢ a + b = c

Tactic:
subst_vars

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 a' b b' c : R
x✝² : a = a'
x✝¹ : b = b'
x✝ : a' * b' = c
⊢ a * b = c

Tactic:
subst_vars

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 b' c : R
a a' : ℕ
x✝² : a = a'
x✝¹ : b = b'
x✝ : a' • b' = c
⊢ a • b = c

Tactic:
subst_vars

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 b' c : R
a a' : ℤ
x✝² : a = a'
x✝¹ : b = b'
x✝ : a' • b' = c
⊢ a • b = c

Tactic:
subst_vars

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 a' c : R
b b' : ℕ
x✝² : a = a'
x✝¹ : b = b'
x✝ : a' ^ b' = c
⊢ a ^ b = c

Tactic:
subst_vars

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 a' b : R
x✝¹ : a = a'
x✝ : -a' = b
⊢ -a = b

Tactic:
subst_vars

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 a' b b' c : R
x✝² : a = a'
x✝¹ : b = b'
x✝ : a' - b' = c
⊢ a - b = c

Tactic:
subst_vars

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 a' b : R
x✝¹ : a = a'
x✝ : a'⁻¹ = b
⊢ a⁻¹ = b

Tactic:
subst_vars

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 a' b b' c : R
x✝² : a = a'
x✝¹ : b = b'
x✝ : a' / b' = c
⊢ a / b = c

Tactic:
subst_vars

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_2
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : SMul R α
r : R
a b t c : α
x✝² : a = b
x✝¹ : ∀ (x : α), r • x = t * x
x✝ : t * b = c
⊢ r • a = c

Tactic:
subst_vars

Goal state after:
R : Type u_2
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : SMul R α
r : R
b t : α
x✝ : ∀ (x : α), r • x = t * x
⊢ r • b = t * 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✝ : CompleteLattice α
gi : GaloisInsertion l u
x✝ : Set β
⊢ IsGLB x✝ (gi.choice (sInf (u '' x✝)) ⋯)

Tactic:
rw [gi.choice_eq]
      exact gi.isGLB_of_u_image (isGLB_sInf _)

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

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

Tactic:
calc
      _ = ⨅ i : ULift.{u} Bool, ⨆ j : match i with | .up true => PUnit.{u + 1} | .up false => s,
          match i with
          | .up true => a
          | .up false => j := by simp [sSup_eq_iSup', iSup_unique, iInf_bool_eq]
      _ ≤ _ := by
        simp only [minAx.iInf_iSup_eq, iInf_ulift, iInf_bool_eq, iSup_le_iff]
        exact fun x ↦ le_biSup _ (x (.up false)).2

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

Goal state before:
pp: α : Type u_1
π : α → Type u_12
α' : Type u_13
s : α' → Set α
t : (a : α) → Set (π a)
⊢ (⋃ i, s i).pi t = ⋂ i, (s i).pi t

Tactic:
ext f

Goal state after:
α : Type u_1
π : α → Type u_12
α' : Type u_13
s : α' → Set α
t : (a : α) → Set (π a)
f : (i : α) → π i
⊢ f ∈ (⋃ i, s i).pi t ↔ f ∈ ⋂ i, (s i).pi t
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:
by simpa only [mem_iUnion, exists_prop] using ⟨i, i_in_J, hix⟩

Goal state after:
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
inst✝⁸ : Max α
inst✝⁷ : Min α
inst✝⁶ : LE α
inst✝⁵ : LT α
inst✝⁴ : SupSet α
inst✝³ : InfSet α
inst✝² : Top α
inst✝¹ : Bot α
inst✝ : CompleteLattice β
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 ⊥ = ⊥
x✝ : Set α
⊢ IsGLB ((fun {x} ↦ f x) '' x✝) (f (sInf x✝))

Tactic:
rw [map_sInf]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
inst✝⁸ : Max α
inst✝⁷ : Min α
inst✝⁶ : LE α
inst✝⁵ : LT α
inst✝⁴ : SupSet α
inst✝³ : InfSet α
inst✝² : Top α
inst✝¹ : Bot α
inst✝ : CompleteLattice β
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 ⊥ = ⊥
x✝ : Set α
⊢ IsGLB ((fun {x} ↦ f x) '' x✝) (⨅ a ∈ x✝, f a)
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
ι : Sort u_5
inst✝ : Preorder α
f : ι → α
⊢ (⋂ i, Iic (f i)).Nonempty ↔ BddBelow (range f)

Tactic:
have : (⋂ (i : ι), Iic (f i)) = lowerBounds (range f) := by
    ext c; simp [lowerBounds]

Goal state after:
α : Type u_1
ι : Sort u_5
inst✝ : Preorder α
f : ι → α
this : ⋂ i, Iic (f i) = lowerBounds (range f)
⊢ (⋂ i, Iic (f i)).Nonempty ↔ BddBelow (range f)
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 = ⨆ i, ⨆ a ∈ s i, f a

Tactic:
rw [iSup_comm]
  simp_rw [mem_iUnion, iSup_exists]

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
x : α
h : IsTop x
⊢ Ici x = {x}

Tactic:
ext y

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
x : α
h : IsTop x
y : α
⊢ y ∈ Ici x ↔ y ∈ {x}
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: case mp.inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
hf : Monotone f
a b c : α
⊢ c ∈ [[a, b]] → f c ∈ [[f a, f b]]

Tactic:
simp_rw [← Icc_min_max, ← hf.map_min, ← hf.map_max]

Goal state after:
case mp.inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
hf : Monotone f
a b c : α
⊢ c ∈ Icc (min a b) (max a b) → f c ∈ Icc (f (min a b)) (f (max a b))
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: case mp.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
hf : Antitone f
a b c : α
⊢ c ∈ [[a, b]] → f c ∈ [[f a, f b]]

Tactic:
simp_rw [← Icc_min_max, ← hf.map_min, ← hf.map_max]

Goal state after:
case mp.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
hf : Antitone f
a b c : α
⊢ c ∈ Icc (min a b) (max a b) → f c ∈ Icc (f (max a b)) (f (min a b))
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (b : β), b ∈ t → Injective fun a ↦ f a b
ht : InjOn (fun p ↦ f p.1 p.2) (s ×ˢ t)
x : β
hx : x ∈ t
y : β
hy : y ∈ t
h : x ≠ y
⊢ (Disjoint on fun b ↦ (fun a ↦ f a b) '' s) x y

Tactic:
· refine disjoint_iff_inf_le.mpr ?_
    rintro _ ⟨⟨a, ha, hab⟩, b, hb, rfl⟩
    exact h (congr_arg Prod.snd <| ht (mk_mem_prod ha hx) (mk_mem_prod hb hy) hab)

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

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

Tactic:
by
  rw [uIoo, inf_eq_left.2 h, sup_eq_right.2 h]

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

Goal state before:
pp: α : Type u_1
inst✝³ : Semiring α
inst✝² : PartialOrder α
inst✝¹ : IsOrderedRing α
inst✝ : NoZeroDivisors α
⊢ ∀ {a b : { x // 0 ≤ x }}, a * b = 0 → a = 0 ∨ b = 0

Tactic:
by
      rintro ⟨a, ha⟩ ⟨b, hb⟩
      simp only [mk_mul_mk, mk_eq_zero, mul_eq_zero, imp_self]

Goal state after:
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
⊢ (a⁻¹ ⊔ 1)⁻¹ = (a ⊓ 1)⁻¹⁻¹

Tactic:
inv_sup,

Goal state after:
α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
⊢ a⁻¹⁻¹ ⊓ 1⁻¹ = (a ⊓ 1)⁻¹⁻¹
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: case succ
n : ℕ
⊢ (n + 1)! * 2 ^ (n + 1) ≤ (2 * (n + 1))!

Tactic:
Nat.two_mul

Goal state after:
case succ
n : ℕ
⊢ (n + 1)! * 2 ^ (n + 1) ≤ (n + 1 + (n + 1))!