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

Goal state before:
pp: α : Type u_1
l : List (α → Prop)
H : ∀ (a : α), (map (fun p ↦ p a) l).TFAE
⊢ ∀ (j : α → Prop), j ∈ l → ∀ (j_1 : α → Prop), j_1 ∈ l → ((∃ a, j a) ↔ ∃ a, j_1 a)

Tactic:
intro p₁

Goal state after:
α : Type u_1
l : List (α → Prop)
H : ∀ (a : α), (map (fun p ↦ p a) l).TFAE
p₁ : α → Prop
⊢ p₁ ∈ l → ∀ (j : α → Prop), j ∈ l → ((∃ a, p₁ a) ↔ ∃ a, j a)
Module: Mathlib.Algebra.Ring.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : DivisionMonoid R
inst✝ : HasDistribNeg R
⊢ -1 * -1 = 1

Tactic:
neg_mul_neg,

Goal state after:
R : Type u_1
inst✝¹ : DivisionMonoid R
inst✝ : HasDistribNeg R
⊢ 1 * 1 = 1
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: M₀ : Type u_2
inst✝ : MonoidWithZero M₀
u : M₀ˣ
⊢ ↑u * (↑u)⁻¹ʳ = 1

Tactic:
rw [inverse_unit, Units.mul_inv]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: M₀ : Type u_2
inst✝ : MonoidWithZero M₀
x : M₀
⊢ IsUnit x ↔ x * x⁻¹ʳ = 1

Tactic:
nontriviality M₀
  refine ⟨mul_inverse_cancel _, ?_⟩
  contrapose
  simp +contextual [not_isUnit_iff_inverse_eq_zero]

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

Goal state before:
pp: M : Type u_1
inst✝ : DivisionMonoid M
a b c d : M
hbd : Commute b d
hb : IsUnit b
hd : IsUnit d
⊢ b⁻¹ * a = d⁻¹ * c ↔ d * a = b * c

Tactic:
← (hd.mul hb).mul_right_inj,

Goal state after:
M : Type u_1
inst✝ : DivisionMonoid M
a b c d : M
hbd : Commute b d
hb : IsUnit b
hd : IsUnit d
⊢ d * b * (b⁻¹ * a) = d * b * (d⁻¹ * c) ↔ d * a = b * c
Module: Mathlib.Algebra.Module.NatInt

Goal state before:
pp: R : Type u_5
inst✝ : NonAssocRing R
m : ℤ
⊢ m • 1 = ↑m

Tactic:
rw [zsmul_eq_mul, mul_one]

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b c d : α
hac : a ≤ c
hbd : b ≤ d
⊢ a * b = c * d ↔ a = c ∧ b = d

Tactic:
by
  have := mulLeftMono_of_mulLeftStrictMono α
  have := mulRightMono_of_mulRightStrictMono α
  rw [le_antisymm_iff, eq_true (mul_le_mul' hac hbd), true_and, mul_le_mul_iff_of_ge hac hbd]

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

Goal state before:
pp: M₀ : Type u_2
inst✝³ : MonoidWithZero M₀
inst✝² : LinearOrder M₀
inst✝¹ : PosMulStrictMono M₀
a : M₀
n : ℕ
inst✝ : ZeroLEOneClass M₀
ha : 0 ≤ a
hn : n ≠ 0
h : 1 < a
⊢ 1 < a ^ n

Tactic:
exact one_lt_pow₀ h hn

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

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a : G₀
⊢ ∀ (a : G₀), 0 < a → 0 < a⁻¹

Tactic:
intro a ha

Goal state after:
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a✝ a : G₀
ha : 0 < a
⊢ 0 < a⁻¹
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a : G₀
⊢ ∀ (a : G₀), 0 < a → 0 < a⁻¹

Tactic:
intro a ha

Goal state after:
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a✝ a : G₀
ha : 0 < a
⊢ 0 < a⁻¹
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b : G₀
ha : 0 < a
⊢ a⁻¹ < b ↔ 1 < b * a

Tactic:
← mul_inv_lt_iff₀ ha,

Goal state after:
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b : G₀
ha : 0 < a
⊢ a⁻¹ < b ↔ 1 * a⁻¹ < b
Module: Mathlib.Algebra.Order.Archimedean.Defs

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
x : R
n : ℤ
h : -x < ↑n
⊢ ↑(-n) < x

Tactic:
Int.cast_neg

Goal state after:
R : Type u_1
inst✝³ : Ring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
x : R
n : ℤ
h : -x < ↑n
⊢ -↑n < x
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow

Goal state before:
pp: M : Type u_3
inst✝³ : Monoid M
inst✝² : LinearOrder M
inst✝¹ : MulLeftStrictMono M
inst✝ : MulRightStrictMono M
a b c : M
h : a * b ≤ c ^ 2
⊢ min a b ≤ c

Tactic:
simpa using min_le_max_of_mul_le_mul (h.trans_eq <| pow_two _)

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

Goal state before:
pp: G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b c : G
⊢ |a / b|ₘ < c ↔ a / b < c ∧ b / a < c

Tactic:
rw [mabs_lt, inv_lt_div_iff_lt_mul', div_lt_iff_lt_mul', and_comm, div_lt_iff_lt_mul']

Goal state after:
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ a / b ⊔ b / a ⊔ 1 = |b / a|ₘ

Tactic:
rw [← inv_div, sup_comm (b := _ / _), ← mabs, sup_eq_left]

Goal state after:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ 1 ≤ |b / a|ₘ
Module: Mathlib.Algebra.Order.Group.Unbundled.Int

Goal state before:
pp: a : ℤ
n : ℕ
⊢ |a / ↑n| ≤ |a|

Tactic:
by
  rw [abs_eq_natAbs, abs_eq_natAbs];
  exact ofNat_le_ofNat_of_le
    (match a, n with
      | (m : ℕ), n => Nat.div_le_self _ _
      | -[m+1], 0 => Nat.zero_le _
      | -[m+1], n + 1 => Nat.succ_le_succ (Nat.div_le_self _ _))

Goal state after:
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: case H1
x y a b : ℕ
h : 0 < a
IH :
  ∀ {s t s' t' : ℤ},
    ↑b % ↑a = ↑x * s + ↑y * t →
      ↑a = ↑x * s' + ↑y * t' →
        ↑((b % a).xgcdAux s t a s' t').1 =
          ↑x * ((b % a).xgcdAux s t a s' t').2.1 + ↑y * ((b % a).xgcdAux s t a s' t').2.2
s t s' t' : ℤ
p : ↑a = ↑x * s + ↑y * t
p' : ↑b = ↑x * s' + ↑y * t'
k : ℤ
⊢ ↑b - ↑a * k = ↑x * (s' - k * s) + ↑y * (t' - k * t)

Tactic:
p,

Goal state after:
case H1
x y a b : ℕ
h : 0 < a
IH :
  ∀ {s t s' t' : ℤ},
    ↑b % ↑a = ↑x * s + ↑y * t →
      ↑a = ↑x * s' + ↑y * t' →
        ↑((b % a).xgcdAux s t a s' t').1 =
          ↑x * ((b % a).xgcdAux s t a s' t').2.1 + ↑y * ((b % a).xgcdAux s t a s' t').2.2
s t s' t' : ℤ
p : ↑a = ↑x * s + ↑y * t
p' : ↑b = ↑x * s' + ↑y * t'
k : ℤ
⊢ ↑b - (↑x * s + ↑y * t) * k = ↑x * (s' - k * s) + ↑y * (t' - k * t)
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: k n : ℕ
hk : n.gcd k < k
hk' : ↑k ≠ 0
⊢ ∃ m, m < k ∧ n * m % k = n.gcd k

Tactic:
have key := congr(($(gcd_eq_gcd_ab n k) % k).toNat)

Goal state after:
k n : ℕ
hk : n.gcd k < k
hk' : ↑k ≠ 0
key : (↑(n.gcd k) % ↑k).toNat = ((↑n * n.gcdA k + ↑k * n.gcdB k) % ↑k).toNat
⊢ ∃ m, m < k ∧ n * m % k = n.gcd k
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: k n : ℕ
hk : n.gcd k < k
hk' : ↑k ≠ 0
key : n.gcd k = (↑n * n.gcdA k % ↑k).toNat
⊢ ∃ m, m < k ∧ n * m % k = n.gcd k

Tactic:
refine ⟨(n.gcdA k % k).toNat, ?_, (Int.ofNat_inj.1 ?_).trans key.symm⟩

Goal state after:
case refine_1
k n : ℕ
hk : n.gcd k < k
hk' : ↑k ≠ 0
key : n.gcd k = (↑n * n.gcdA k % ↑k).toNat
⊢ (n.gcdA k % ↑k).toNat < k

case refine_2
k n : ℕ
hk : n.gcd k < k
hk' : ↑k ≠ 0
key : n.gcd k = (↑n * n.gcdA k % ↑k).toNat
⊢ ↑(n * (n.gcdA k % ↑k).toNat % k) = ↑(↑n * n.gcdA k % ↑k).toNat
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
inst✝ : Group α
γ : (WithZero α)ˣ
⊢ ↑(unitsWithZeroEquiv γ) = ↑γ

Tactic:
simp only [WithZero.unitsWithZeroEquiv, MulEquiv.coe_mk, Equiv.coe_fn_mk, WithZero.coe_unzero]

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
inst✝ : Add α
a b c : α
⊢ ↑a + ↑b = ↑c ↔ ∃ a' b', ↑a' = ↑a ∧ ↑b' = ↑b ∧ a' + b' = c

Tactic:
norm_cast; simp

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

Goal state before:
pp: case neg.mp
α : Type u_1
inst✝³ : AddCommMonoid α
inst✝² : LinearOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : AddRightReflectLE α
a b c : α
h : a < b
⊢ 0 ≤ c → a ≤ c + b

Tactic:
intro h'

Goal state after:
case neg.mp
α : Type u_1
inst✝³ : AddCommMonoid α
inst✝² : LinearOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : AddRightReflectLE α
a b c : α
h : a < b
h' : 0 ≤ c
⊢ a ≤ c + b
Module: Mathlib.Algebra.Order.Sub.Basic

Goal state before:
pp: case neg.mpr
α : Type u_1
inst✝³ : AddCommMonoid α
inst✝² : LinearOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : AddRightReflectLE α
a b c : α
h : a < b
⊢ a ≤ c + b → 0 ≤ c

Tactic:
intro h'

Goal state after:
case neg.mpr
α : Type u_1
inst✝³ : AddCommMonoid α
inst✝² : LinearOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : AddRightReflectLE α
a b c : α
h : a < b
h' : a ≤ c + b
⊢ 0 ≤ c
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
a : α
inst✝ : LE α
x : WithBot α
⊢ ↑a ≤ x ↔ ∃ b, x = ↑b ∧ a ≤ b

Tactic:
by simp [le_iff_forall]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
b : α
inst✝ : LE α
x : WithBot α
⊢ x ≤ ↑b ↔ ∀ (a : α), x = ↑a → a ≤ b

Tactic:
by simp [le_iff_forall]

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

Goal state before:
pp: F : Type u_1
α✝ : Type u_2
β : Type u_3
α : Type ?u.6
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedRing α
ceil : α → ℤ
gc_ceil_coe : GaloisConnection ceil Int.cast
a : ℤ
z : α
⊢ ↑a ≤ z ↔ a ≤ (fun a ↦ -ceil (-a)) z

Tactic:
rw [le_neg, gc_ceil_coe, Int.cast_neg, neg_le_neg_iff]

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: G : Type u_3
inst✝¹ : Preorder G
a : G
inst✝ : AddGroup G
x : WithZero (Multiplicative G)
hxa : x.log ≤ a
⊢ x ≤ exp a

Tactic:
by
  obtain rfl | hx := eq_or_ne x 0 <;> simp [← log_le_iff_le_exp, *]

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

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
n : ℕ
inst✝ : IsStrictOrderedRing R
hn : n ≠ 0
⊢ n ≤ ⌊a⌋₊ ↔ ↑n ≤ a

Tactic:
obtain ha | ha := le_total a 0
  · rw [floor_of_nonpos ha]
    exact
      iff_of_false (Nat.pos_of_ne_zero hn).not_ge
        (not_le_of_gt <| ha.trans_lt <| cast_pos.2 <| Nat.pos_of_ne_zero hn)
  · exact le_floor_iff ha

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe.coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
a✝² a✝¹ a✝ : α
⊢ (a✝² ⊔ a✝¹) ⊓ (a✝² ⊔ a✝) ≤ a✝² ⊔ a✝¹ ⊓ a✝

Tactic:
simpa [← coe_inf, ← coe_sup] using le_sup_inf

Goal state after:
Module: Mathlib.Order.Directed

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
x : α
x✝ : x ∈ s
⊢ (∀ y ∈ s, ∃ z ∈ s, r x z ∧ r y z) ↔ ∀ a ∈ s, ∃ a_1, r x a_1 ∧ a_1 ∈ s ∧ r a a_1

Tactic:
by simp [And.comm, and_assoc]

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
s : Set α
t : Set β
hs : s.Subsingleton
ht : t.Subsingleton
f : α → β → γ
⊢ (Set.image2 f s t).Subsingleton

Tactic:
by
  rw [← image_prod]
  apply (hs.prod ht).image

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
h : Iic a ⊂ Iic b
⊢ a < b

Tactic:
obtain ⟨ab, c, cb, ac⟩ := ssubset_iff_exists.mp h

Goal state after:
α : Type u_1
inst✝ : Preorder α
a b : α
h : Iic a ⊂ Iic b
ab : Iic a ⊆ Iic b
c : α
cb : c ∈ Iic b
ac : ¬c ∈ Iic a
⊢ a < b
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a ≤ b
⊢ Icc a b \ Ioo a b = {a, b}

Tactic:
rw [← Icc_sdiff_both, sdiff_sdiff_cancel_left]

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a ≤ b
⊢ {a, b} ⊆ Icc a b
Module: Mathlib.Order.Bounds.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s t : Set α
⊢ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (s ∪ t) ↔
    DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s ∧ IsCofinalFor t s ∨ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) t ∧ IsCofinalFor s t

Tactic:
by
  refine ⟨fun h ↦ ?_, ?_⟩
  · rcases isCofinalFor_or_isCofinalFor_of_directedOn_union h with hts | hst
    · exact .inl ⟨DirectedOn.of_isCofinalFor h subset_union_left hts.union_right, hts⟩
    · exact .inr ⟨DirectedOn.of_isCofinalFor h subset_union_right hst.union_left, hst⟩
  · rintro (⟨hs, hts⟩ | ⟨ht, hst⟩) x hx y hy
    · 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⟩
    · obtain ⟨x', hx', hxx'⟩ := hst.union_left hx
      obtain ⟨y', hy', hyy'⟩ := hst.union_left hy
      obtain ⟨z, hz, hx'z, hy'z⟩ := ht x' hx' y' hy'
      exact ⟨z, .inr hz, hxx'.trans hx'z, hyy'.trans hy'z⟩

Goal state after:
Module: Mathlib.Tactic.Abel

Goal state before:
pp: α : Type u_1
inst✝ : AddCommMonoid α
x : α
⊢ x = term 1 x 0

Tactic:
simp [term, one_nsmul]

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

Goal state before:
pp: case cons
M : Type u_2
inst✝ : MulOneClass M
l✝ : List M
p : M → Prop
hom : ∀ (a b : M), p a → p b → p (a * b)
a : M
l : List M
ih : l ≠ [] → (∀ (x : M), x ∈ l → p x) → p l.prod
hl : a :: l ≠ []
base : ∀ (x : M), x ∈ a :: l → p x
⊢ p (a :: l).prod

Tactic:
by_cases hl_empty : l = []
    · simp [*]
    rw [List.prod_cons]
    simp only [mem_cons, forall_eq_or_imp] at base
    exact hom _ _ (base.1) (ih hl_empty base.2)

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

Goal state before:
pp: α : Type u
l : List α
n : ℕ
h : n < l.length
⊢ take 1 (drop n l) = [l.get ⟨n, h⟩]

Tactic:
drop_eq_getElem_cons h,

Goal state after:
α : Type u
l : List α
n : ℕ
h : n < l.length
⊢ take 1 (l[n] :: drop (n + 1) l) = [l.get ⟨n, h⟩]
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
a✝ : α
b✝ : β
l₁✝ : List α
l₂✝ : List β
h₁ : R a✝ b✝
h₂ : Forall₂ R l₁✝ l₂✝
x : α
y : β
hx : (x, y) ∈ (a✝ :: l₁✝).zip (b✝ :: l₂✝)
⊢ R x y

Tactic:
zip,

Goal state after:
α : Type u_1
β : Type u_2
R : α → β → Prop
a✝ : α
b✝ : β
l₁✝ : List α
l₂✝ : List β
h₁ : R a✝ b✝
h₂ : Forall₂ R l₁✝ l₂✝
x : α
y : β
hx : (x, y) ∈ zipWith Prod.mk (a✝ :: l₁✝) (b✝ :: l₂✝)
⊢ R x y
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: case inl
α : Type u_1
l₁ l₂ : List α
m n : ℕ
h : l₁[m]? = l₂[n]?
hm : m < l₁.length
⊢ l₁.eraseIdx m ~ l₂.eraseIdx n ↔ l₁ ~ l₂

Tactic:
rw [getElem?_eq_getElem hm, eq_comm, getElem?_eq_some_iff] at h
    cases h with
    | intro hn hnm =>
      rw [← perm_cons l₁[m], rel_congr_left (getElem_cons_eraseIdx_perm ..), ← hnm,
        rel_congr_right (getElem_cons_eraseIdx_perm ..)]

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

Goal state before:
pp: case cons
α : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
p : α → Prop
inst✝ : DecidablePred p
f g : α → M
x : α
xs : List α
ih :
  (map (fun a ↦ if p a then f a else g a) xs).prod =
    (map f (filter (fun b ↦ decide (p b)) xs)).prod * (map g (filter (fun a ↦ decide ¬p a) xs)).prod
⊢ (map (fun a ↦ if p a then f a else g a) (x :: xs)).prod =
    (map f (filter (fun b ↦ decide (p b)) (x :: xs))).prod * (map g (filter (fun a ↦ decide ¬p a) (x :: xs))).prod

Tactic:
simp only [map_cons, filter_cons, prod_cons] at ih ⊢
    rw [ih]
    clear ih
    by_cases hx : p x
    · simp only [hx, ↓reduceIte, decide_not, decide_true, map_cons, prod_cons, not_true_eq_false,
        decide_false, Bool.false_eq_true, mul_assoc]
    · simp only [hx, ↓reduceIte, decide_not, decide_false, Bool.false_eq_true, not_false_eq_true,
      decide_true, map_cons, prod_cons, mul_left_comm]

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

Goal state before:
pp: x✝¹ : ℕ
x✝ : ℚ
⊢ x✝ ^ ↑x✝¹.succ = x✝ ^ ↑x✝¹ * x✝

Tactic:
by rw [Rat.zpow_natCast, Rat.zpow_natCast, Rat.pow_succ]

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

Goal state before:
pp: case refine_1
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
⊢ ↑q.den ≠ 0

pp: case refine_2
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
⊢ q.num /. ↑q.den = n /. d

Tactic:
· exact Int.natCast_ne_zero.mpr (Rat.den_nz _)

Goal state after:
case refine_2
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
⊢ q.num /. ↑q.den = n /. d
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: α : Type u_3
inst✝ : DivisionSemiring α
a b : ℕ
hb : ↑b ≠ 0
⊢ ↑(divNat a b) = ↑a / ↑b

Tactic:
by
  rcases e : divNat a b with ⟨⟨n, d, h, c⟩, hn⟩
  rw [← Rat.num_nonneg] at hn
  lift n to ℕ using hn
  have hd : (d : α) ≠ 0 := by
    refine fun hd ↦ hb ?_
    have : Rat.divInt a b = _ := congr_arg NNRat.cast e
    obtain ⟨k, rfl⟩ : d ∣ b := by simpa [Int.natCast_dvd_natCast, this] using Rat.den_dvd a b
    simp [*]
  have hb' : b ≠ 0 := by rintro rfl; exact hb Nat.cast_zero
  simp_rw [Rat.mk_eq_divInt, mk_divInt, divNat_inj hb' h] at e
  rw [cast_def]
  dsimp
  rw [Commute.div_eq_div_iff _ hd hb]
  · norm_cast
    rw [e]
  exact b.commute_cast _

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

Goal state before:
pp: F : Type u_1
α : Type u_3
inst✝² : DivisionSemiring α
inst✝¹ : FunLike F ℚ≥0 α
inst✝ : RingHomClass F ℚ≥0 α
f : F
q : ℚ≥0
⊢ f q = ↑q

Tactic:
by rw [← map_nnratCast f, NNRat.cast_id]

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

Goal state before:
pp: α : Type u_1
inst✝ : CompleteSemilatticeSup α
s : Set α
a : α
⊢ sSup s = a → IsLUB s a

Tactic:
rintro rfl; exact isLUB_sSup _

Goal state after:
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 : γ → α
hf : BijOn f s t
⊢ ⨆ x ∈ s, g (f x) = ⨆ y ∈ t, g y

Tactic:
by
  rw [← hf.image_eq, iSup_image]

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

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

Tactic:
iSup_psigma',

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

Goal state before:
pp: α : Type u_1
p q r : α → α → Prop
a b : α
c : { x // p a x ∧ q x b }
h : ∀ {x : α}, r (↑c) x → p a x
x✝ : α
⊢ x✝ ∈ {x | p a x ∧ q x b} ∩ {y | r (↑c) y} ↔ x✝ ∈ {y | r (↑c) y ∧ q y b}

Tactic:
simp +contextual [@and_comm (r _ _), h]

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
minAx : CompletelyDistribLattice.MinimalAxioms β
f : α → β
hf : Injective f
map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a
map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a
ι✝ : Type u
κ✝ : ι✝ → Type u
g : (a : ι✝) → κ✝ a → α
⊢ f (⨅ a, ⨆ b, g a b) = f (⨆ g_1, ⨅ a, g a (g_1 a))

Tactic:
iInf,

Goal state after:
α : Type u
β : Type v
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
minAx : CompletelyDistribLattice.MinimalAxioms β
f : α → β
hf : Injective f
map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a
map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a
ι✝ : Type u
κ✝ : ι✝ → Type u
g : (a : ι✝) → κ✝ a → α
⊢ f (sInf (range fun a ↦ ⨆ b, g a b)) = f (⨆ g_1, sInf (range fun a ↦ g a (g_1 a)))
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 → α
⊢ f (⨅ a, ⨆ b, g a b) = f (⨆ g_1, ⨅ a, g a (g_1 a))

Tactic:
iInf,

Goal state after:
α : 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 → α
⊢ f (sInf (range fun a ↦ ⨆ b, g a b)) = f (⨆ g_1, sInf (range fun a ↦ g a (g_1 a)))
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case pos.some.refine_2
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : BddAbove ((fun a ↦ ↑a) ⁻¹' s)
b : β
hb : Option.some b ∈ upperBounds s
⊢ ∀ b_1 ∈ (fun a ↦ ↑a) ⁻¹' s, b_1 ≤ b

Tactic:
intro a ha

Goal state after:
case pos.some.refine_2
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : BddAbove ((fun a ↦ ↑a) ⁻¹' s)
b : β
hb : Option.some b ∈ upperBounds s
a : β
ha : a ∈ (fun a ↦ ↑a) ⁻¹' s
⊢ a ≤ b
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case h
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : ¬BddAbove ((fun a ↦ ↑a) ⁻¹' s)
b : β
hb : Option.some b ∈ upperBounds s
⊢ b ∈ upperBounds ((fun a ↦ ↑a) ⁻¹' s)

Tactic:
intro a ha

Goal state after:
case h
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : ¬BddAbove ((fun a ↦ ↑a) ⁻¹' s)
b : β
hb : Option.some b ∈ upperBounds s
a : β
ha : a ∈ (fun a ↦ ↑a) ⁻¹' s
⊢ a ≤ b
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case pos
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : s ⊆ {⊤}
⊢ ⊤ ∈ lowerBounds s

Tactic:
intro a ha

Goal state after:
case pos
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : s ⊆ {⊤}
a : WithTop β
ha : a ∈ s
⊢ ⊤ ≤ a
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
s t : Set α
ht : BddBelow (f '' t)
hf : MonotoneOn f t
hst : s ⊆ t
h : ∀ y ∈ t, ∃ x ∈ s, x ≤ y
hs : s.Nonempty
⊢ ∀ a ∈ t, sInf (f '' s) ≤ f a

Tactic:
intro a ha

Goal state after:
case inr
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
s t : Set α
ht : BddBelow (f '' t)
hf : MonotoneOn f t
hst : s ⊆ t
h : ∀ y ∈ t, ∃ x ∈ s, x ≤ y
hs : s.Nonempty
a : α
ha : a ∈ t
⊢ sInf (f '' s) ≤ f a
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : MonotoneOn f [[a, b]]
⊢ MapsTo f (Icc (min a b) (max a b)) (Icc (f (min a b)) (f (max a b)))

Tactic:
apply_rules [left_mem_uIcc, right_mem_uIcc, hf.mapsTo_Icc]

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

Goal state before:
pp: case hx
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : MonotoneOn f [[a, b]]
⊢ a ∈ [[a, b]]

Tactic:
apply_rules [left_mem_uIcc, right_mem_uIcc, hf.mapsTo_Icc]

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

Goal state before:
pp: case hy
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : MonotoneOn f [[a, b]]
⊢ b ∈ [[a, b]]

Tactic:
apply_rules [left_mem_uIcc, right_mem_uIcc, hf.mapsTo_Icc]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : AntitoneOn f [[a, b]]
⊢ MapsTo f (Icc (min a b) (max a b)) (Icc (f (max a b)) (f (min a b)))

Tactic:
apply_rules [left_mem_uIcc, right_mem_uIcc, hf.mapsTo_Icc]

Goal state after: