mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Group.Lattice

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
ha : 1 ≤ a ^ 2
this : (a ⊓ 1) * (a ⊓ 1) = a ⊓ 1
⊢ 1 ≤ a

Tactic:
← inf_eq_right,

Goal state after:
α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
ha : 1 ≤ a ^ 2
this : (a ⊓ 1) * (a ⊓ 1) = a ⊓ 1
⊢ a ⊓ 1 = 1
Module: Mathlib.Algebra.Order.Group.Lattice

Goal state before:
pp: case right
α✝ : Type u_1
inst✝⁴ : Lattice α✝
inst✝³ : CommGroup α✝
α : Type u_2
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
x y z : α
⊢ x⁻¹ * ((x ⊓ (y ⊓ z)) * ((x ⊔ y) ⊓ (x ⊔ z))) ≤ z

Tactic:
rw [inv_mul_le_iff_le_mul, ← inf_mul_sup x z]

Goal state after:
case right
α✝ : Type u_1
inst✝⁴ : Lattice α✝
inst✝³ : CommGroup α✝
α : Type u_2
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
x y z : α
⊢ (x ⊓ (y ⊓ z)) * ((x ⊔ y) ⊓ (x ⊔ z)) ≤ (x ⊓ z) * (x ⊔ z)
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 ^ 2 ≤ b * c
⊢ a ≤ max b c

Tactic:
simpa using min_le_max_of_mul_le_mul ((pow_two _).symm.trans_le h)

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

Goal state before:
pp: case inr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b c : G
hac : a ≤ b
hcd : b ≤ c
d : G
h : b ≤ d
⊢ |b / d|ₘ ≤ max (c / d) (d / a)

Tactic:
rw [mabs_of_le_one <| div_le_one'.mpr h, inv_div]
    exact le_max_of_le_right <| div_le_div_left' hac _

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

Goal state before:
pp: a : ℤ
⊢ a.sign * |a| = a

Tactic:
rw [abs_eq_natAbs, sign_mul_natAbs a]

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 : ℤ
⊢ ↑x * s' + ↑y * t' - (↑x * s + ↑y * t) * k = ↑x * s' + (↑y * t' - ↑y * (k * t)) - ↑x * (k * s)

Tactic:
Int.add_mul,

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 : ℤ
⊢ ↑x * s' + ↑y * t' - (↑x * s * k + ↑y * t * k) = ↑x * s' + (↑y * t' - ↑y * (k * t)) - ↑x * (k * s)
Module: Mathlib.Algebra.Order.Group.Nat

Goal state before:
pp: case succ
m n : ℕ
ih : ∀ (k : ℕ), m - n ≤ k ↔ m ≤ k + n
k : ℕ
⊢ m - (n + 1) ≤ k ↔ m ≤ k + (n + 1)

Tactic:
| succ n ih =>

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

Goal state before:
pp: x y : ℕ
this : x.P y (x.xgcdAux 1 0 y 0 1)
⊢ ↑(x.gcd y) = ↑x * x.gcdA y + ↑y * x.gcdB y

Tactic:
rwa [xgcdAux_val, xgcd_val] at this

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

Goal state before:
pp: case mp
a b : ℤ
n : ℕ
h : a.gcd b ∣ n
⊢ ∃ x y, (a * a.gcdA b + b * a.gcdB b) * ↑(n / a.gcd b) = a * x + b * y

Tactic:
Int.add_mul,

Goal state after:
case mp
a b : ℤ
n : ℕ
h : a.gcd b ∣ n
⊢ ∃ x y, a * a.gcdA b * ↑(n / a.gcd b) + b * a.gcdB b * ↑(n / a.gcd b) = a * x + b * y
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: a b c : ℤ
habc : a ∣ b * c
hab : a.gcd b = 1
⊢ a ∣ c

Tactic:
rw [mul_comm] at habc

Goal state after:
a b c : ℤ
habc : a ∣ c * b
hab : a.gcd b = 1
⊢ a ∣ c
Module: Mathlib.Algebra.Regular.Basic

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : Semigroup R
a b : R
⊢ IsRegular (a * b) ∧ IsRegular (b * a) → IsRegular a ∧ IsRegular b

Tactic:
rintro ⟨ab, ba⟩
    exact
      ⟨⟨IsLeftRegular.of_mul ba.left, IsRightRegular.of_mul ab.right⟩,
        ⟨IsLeftRegular.of_mul ab.left, IsRightRegular.of_mul ba.right⟩⟩

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
ha : AddLECancellable a
h₁ : 0 < a
h₂ : 0 < b
⊢ a - b < a

Tactic:
refine tsub_le_self.lt_of_ne fun h => ?_

Goal state after:
α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
ha : AddLECancellable a
h₁ : 0 < a
h₂ : 0 < b
h : a - b = a
⊢ False
Module: Mathlib.Data.Nat.Find

Goal state before:
pp: case neg
P : ℕ → Prop
inst✝ : DecidablePred P
m n m✝ : ℕ
hmk : m.le m✝
ih : findGreatest P m ≤ findGreatest P m✝
h✝ : ¬P (m✝ + 1)
⊢ findGreatest P m ≤ findGreatest P m✝

Tactic:
· exact ih

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

Goal state before:
pp: P : ℤ → Prop
inst✝ : DecidablePred P
b : ℤ
Hb : ∀ (z : ℤ), P z → z ≤ b
Hinh : ∃ z, P z
Hbdd' : ∀ (z : ℤ), P (-z) → -b ≤ z
elt : ℤ
Helt : P elt
⊢ P (- -elt)

Tactic:
by rw [neg_neg]; exact Helt

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)
hx : x ≠ 0
⊢ a ≤ x.log ↔ (exp a).log ≤ x.log

Tactic:
log_exp

Goal state after:
G : Type u_3
inst✝¹ : Preorder G
a : G
inst✝ : AddGroup G
x : WithZero (Multiplicative G)
hx : x ≠ 0
⊢ a ≤ x.log ↔ a ≤ x.log
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)
hx : x ≠ 0
⊢ a < x.log ↔ (exp a).log < x.log

Tactic:
log_exp

Goal state after:
G : Type u_3
inst✝¹ : Preorder G
a : G
inst✝ : AddGroup G
x : WithZero (Multiplicative G)
hx : x ≠ 0
⊢ a < x.log ↔ a < x.log
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
⊢ ⌈a⌉₊ = 0 ↔ a ≤ 0

Tactic:
← Nat.le_zero,

Goal state after:
R : Type u_1
inst✝² : Semiring R
inst✝¹ : LinearOrder R
inst✝ : FloorSemiring R
a : R
⊢ ⌈a⌉₊ ≤ 0 ↔ a ≤ 0
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
inst✝ : IsStrictOrderedRing R
ha : 0 ≤ a
n d : ℕ
hb : n ≤ n + d
⊢ ↑n + ↑d ≤ a + ↑n ↔ n + d ≤ ⌊a⌋₊ + n

Tactic:
add_comm n,

Goal state after:
case inl
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
inst✝ : IsStrictOrderedRing R
ha : 0 ≤ a
n d : ℕ
hb : n ≤ n + d
⊢ ↑n + ↑d ≤ a + ↑n ↔ d + n ≤ ⌊a⌋₊ + n
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
inst✝ : IsStrictOrderedRing R
ha : 0 ≤ a
n d : ℕ
hb : n ≤ n + d
⊢ ↑n + ↑d < a + ↑n ↔ n + d < ⌈a⌉₊ + n

Tactic:
add_comm n,

Goal state after:
case inl
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
inst✝ : IsStrictOrderedRing R
ha : 0 ≤ a
n d : ℕ
hb : n ≤ n + d
⊢ ↑n + ↑d < a + ↑n ↔ d + n < ⌈a⌉₊ + n
Module: Mathlib.Order.Directed

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
inst✝ : Preorder α
f : α → β
s : Set α
hf : MonotoneOn f s
hf' : AntitoneOn f s
hs : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
⊢ ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → f a = f b

Tactic:
by
  rintro a ha b hb
  obtain ⟨c, hc, hac, hbc⟩ := hs _ ha _ hb
  exact le_antisymm ((hf ha hc hac).trans <| hf' hb hc hbc) ((hf hb hc hbc).trans <| hf' ha hc hac)

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
S : Type u_3
inst✝⁶ : Semiring S
inst✝⁵ : LinearOrder S
inst✝⁴ : FloorSemiring S
F : Type u_4
inst✝³ : FunLike F R S
inst✝² : RingHomClass F R S
inst✝¹ : IsStrictOrderedRing R
inst✝ : IsStrictOrderedRing S
f : F
hf : StrictMono ⇑f
a : R
n : ℕ
⊢ f ↑n ≤ f a ↔ ↑n ≤ a

Tactic:
hf.le_iff_le

Goal state after:
R : Type u_1
inst✝⁹ : Semiring R
inst✝⁸ : LinearOrder R
inst✝⁷ : FloorSemiring R
S : Type u_3
inst✝⁶ : Semiring S
inst✝⁵ : LinearOrder S
inst✝⁴ : FloorSemiring S
F : Type u_4
inst✝³ : FunLike F R S
inst✝² : RingHomClass F R S
inst✝¹ : IsStrictOrderedRing R
inst✝ : IsStrictOrderedRing S
f : F
hf : StrictMono ⇑f
a : R
n : ℕ
⊢ ↑n ≤ a ↔ ↑n ≤ a
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: R : Type u_1
inst✝⁷ : Semiring R
inst✝⁶ : LinearOrder R
inst✝⁵ : FloorSemiring R
S : Type u_3
inst✝⁴ : Semiring S
inst✝³ : LinearOrder S
inst✝² : FloorSemiring S
F : Type u_4
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : StrictMono ⇑f
a : R
n : ℕ
⊢ f a ≤ f ↑n ↔ a ≤ ↑n

Tactic:
hf.le_iff_le

Goal state after:
R : Type u_1
inst✝⁷ : Semiring R
inst✝⁶ : LinearOrder R
inst✝⁵ : FloorSemiring R
S : Type u_3
inst✝⁴ : Semiring S
inst✝³ : LinearOrder S
inst✝² : FloorSemiring S
F : Type u_4
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : StrictMono ⇑f
a : R
n : ℕ
⊢ a ≤ ↑n ↔ a ≤ ↑n
Module: Mathlib.Algebra.GroupWithZero.Units.Lemmas

Goal state before:
pp: case inl
M : Type u_1
G₀ : Type u_3
F : Type u_6
inst✝³ : Monoid M
inst✝² : GroupWithZero G₀
inst✝¹ : FunLike F G₀ M
inst✝ : MonoidHomClass F G₀ M
f : F
h : IsUnit (f 0)
t : G₀
ht : f t ≠ 1
this : f (t * 0) = f t * f 0
⊢ f t = 1

Tactic:
← one_mul (f (t * 0)),

Goal state after:
case inl
M : Type u_1
G₀ : Type u_3
F : Type u_6
inst✝³ : Monoid M
inst✝² : GroupWithZero G₀
inst✝¹ : FunLike F G₀ M
inst✝ : MonoidHomClass F G₀ M
f : F
h : IsUnit (f 0)
t : G₀
ht : f t ≠ 1
this : 1 * f (t * 0) = f t * f 0
⊢ f t = 1
Module: Mathlib.Algebra.Order.Ring.Basic

Goal state before:
pp: case succ
R : Type u_3
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
x y : R
hx : 0 ≤ x
hy : 0 ≤ y
k : ℕ
ih : k + 1 ≠ 0 → x ^ (k + 1) + y ^ (k + 1) ≤ (x + y) ^ (k + 1)
hn : k + 1 + 1 ≠ 0
n : ℕ := k.succ
h1 : 0 ≤ x * y ^ n + y * x ^ n
⊢ x ^ (k + 1 + 1) + y ^ (k + 1 + 1) ≤ (x + y) ^ (k + 1 + 1)

Tactic:
have h2 := add_nonneg hx hy

Goal state after:
case succ
R : Type u_3
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
x y : R
hx : 0 ≤ x
hy : 0 ≤ y
k : ℕ
ih : k + 1 ≠ 0 → x ^ (k + 1) + y ^ (k + 1) ≤ (x + y) ^ (k + 1)
hn : k + 1 + 1 ≠ 0
n : ℕ := k.succ
h1 : 0 ≤ x * y ^ n + y * x ^ n
h2 : 0 ≤ x + y
⊢ x ^ (k + 1 + 1) + y ^ (k + 1 + 1) ≤ (x + y) ^ (k + 1 + 1)
Module: Mathlib.Algebra.Order.Ring.Basic

Goal state before:
pp: case hab
R : Type u_3
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b : R
n : ℕ
ha : 0 ≤ a
hb : 0 ≤ b
⊢ a ≤ a + b

pp: case hab
R : Type u_3
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b : R
n : ℕ
ha : 0 ≤ a
hb : 0 ≤ b
⊢ b ≤ a + b

Tactic:
exacts [le_add_of_nonneg_right hb, le_add_of_nonneg_left ha]

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

Goal state before:
pp: case succ
α : Type u_1
inst✝² : CommRing α
inst✝¹ : LinearOrder α
a b : α
n✝ : ℕ
inst✝ : IsOrderedRing α
n : ℕ
ih : |geomSum a b n| ≤ (↑n + 1) * max |a| |b| ^ n
⊢ |geomSum a b (n + 1)| ≤ (↑(n + 1) + 1) * max |a| |b| ^ (n + 1)

Tactic:
| succ n ih =>

Goal state after:
case succ
α : Type u_1
inst✝² : CommRing α
inst✝¹ : LinearOrder α
a b : α
n✝ : ℕ
inst✝ : IsOrderedRing α
n : ℕ
ih : |geomSum a b n| ≤ (↑n + 1) * max |a| |b| ^ n
⊢ |geomSum a b (n + 1)| ≤ (↑(n + 1) + 1) * max |a| |b| ^ (n + 1)
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: case succ
α : Type u_1
inst✝ : CommRing α
a b : α
n✝ n : ℕ
ih : a ^ (n + 1) - b ^ (n + 1) = (a - b) * geomSum a b n
⊢ a ^ (n + 1 + 1) - b ^ (n + 1 + 1) = (a - b) * geomSum a b (n + 1)

Tactic:
| succ n ih =>

Goal state after:
case succ
α : Type u_1
inst✝ : CommRing α
a b : α
n✝ n : ℕ
ih : a ^ (n + 1) - b ^ (n + 1) = (a - b) * geomSum a b n
⊢ a ^ (n + 1 + 1) - b ^ (n + 1 + 1) = (a - b) * geomSum a b (n + 1)
Module: Mathlib.Order.Bounds.Basic

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

Tactic:
intro hts x hx

Goal state after:
α : Type u_1
inst✝ : Preorder α
s t : Set α
h : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (s ∪ t)
hts : ¬IsCofinalFor t s
x : α
hx : x ∈ s
⊢ ∃ b ∈ t, x ≤ b
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a b : α
inst✝ : IsStrictOrderedRing α
ha : 0 < a
hb : 1 < b
⊢ a / b < a

Tactic:
simpa only [div_one] using div_lt_div_of_pos_left ha zero_lt_one hb

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

Goal state before:
pp: case succ
M : Type u_2
inst✝ : Monoid M
a : M
n : ℕ
ih : (replicate n a).prod = a ^ n
⊢ (replicate (n + 1) a).prod = a ^ (n + 1)

Tactic:
| succ n ih =>

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

Goal state before:
pp: α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a b : α
inst✝ : IsStrictOrderedRing α
s : Set α
ha : 0 ≤ a
hs : IsGLB s b
⊢ IsGLB ((fun b ↦ b * a) '' s) (b * a)

Tactic:
simpa [mul_comm] using hs.mul_left ha

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

Goal state before:
pp: α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a b : α
inst✝ : IsStrictOrderedRing α
s : Set α
ha : 0 ≤ a
hs : IsLUB s b
⊢ IsLUB ((fun b ↦ b * a) '' s) (b * a)

Tactic:
simpa [mul_comm] using hs.mul_left ha

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

Goal state before:
pp: case succ
α : Type u
n : ℕ
ih : ∀ (l : List α), tail^[n] l = drop n l
l : List α
⊢ tail^[n + 1] l = drop (n + 1) l

Tactic:
| succ n ih =>

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

Goal state before:
pp: α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : α
ha : 0 ≤ a
hc : 0 ≤ c
h : c < a * b
⊢ ∃ b' ∈ Set.Ico 0 b, c < a * b'

Tactic:
by
  have hb : 0 < b := pos_of_mul_pos_right (hc.trans_lt h) ha
  simp_rw [mul_comm a] at h ⊢
  exact exists_lt_mul_left_of_nonneg hb.le hc h

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

Goal state before:
pp: α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b ε : α
hε : 0 < ε
h : 2 * (ε * a) * b ≤ (ε * a) ^ 2 + b ^ 2
⊢ 2 * a * b * (ε * ε⁻¹) = 2 * (ε * a) * b * ε⁻¹

Tactic:
simp_rw [mul_assoc, mul_comm ε, mul_assoc]

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

Goal state before:
pp: α : Type u
h : Injective length
x y : α
this : [x] = [y]
⊢ x = y

Tactic:
by simpa using this

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

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
r : α → β → Prop
l₁ : List α
l₃ l₂ : List β
h₁₂ : Forall₂ r l₁ l₂
h₂₃ : l₂ ~ l₃
⊢ (Perm ∘r Forall₂ r) l₁ l₃

Tactic:
have : Forall₂ (flip r) l₂ l₁ := h₁₂.flip

Goal state after:
case mp
α : Type u_1
β : Type u_2
r : α → β → Prop
l₁ : List α
l₃ l₂ : List β
h₁₂ : Forall₂ r l₁ l₂
h₂₃ : l₂ ~ l₃
this : Forall₂ (flip r) l₂ l₁
⊢ (Perm ∘r Forall₂ r) l₁ l₃
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
m n : ℕ
a : α
⊢ replicate (m + n) a = replicate m a ++ replicate n a

Tactic:
replicate_append_replicate

Goal state after:
α : Type u
m n : ℕ
a : α
⊢ replicate (m + n) a = replicate (m + n) a
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
a : α
n : ℤ
hn : n ≠ 0
⊢ zpow' a n = a ^ n

Tactic:
by
  simp [zpow', hn]

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

Goal state before:
pp: case cons.inl
M : Type u_4
inst✝¹ : Monoid M
l✝ : List M
a : M
inst✝ : DecidableEq M
l : List M
ih : a ∈ l → (∀ (x : M), x ∈ l → ∀ (y : M), y ∈ l → x * y = y * x) → a * (l.erase a).prod = l.prod
ha : a ∈ a :: l
comm : ∀ (x : M), x ∈ a :: l → ∀ (y : M), y ∈ a :: l → x * y = y * x
⊢ a * ((a :: l).erase a).prod = (a :: l).prod

Tactic:
simp only [erase_cons_head, prod_cons]

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
i : ℕ
h₁ : i < L.length
h₂ : i < L'.length
this : (take (i + 1) L).prod = (take (i + 1) L').prod
⊢ L.get ⟨i, h₁⟩ = L'.get ⟨i, h₂⟩

Tactic:
prod_take_succ L i 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
this : (take i L).prod * L[i] = (take (i + 1) L').prod
⊢ L.get ⟨i, h₁⟩ = L'.get ⟨i, h₂⟩
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
β : Type v
f : α → β
h : Injective (map f)
x y : α
hxy : f x = f y
this : [x] = [y]
⊢ x = y

Tactic:
by simpa using this

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

Goal state before:
pp: case cons
α : Type u
β : Type v
f g : α → β → β
b : β
hd : α
tl : List α
ih : (∀ (a : α), a ∈ tl → ∀ (b : β), f a b = g a b) → foldr f b tl = foldr g b tl
H : (∀ (b : β), f hd b = g hd b) ∧ ∀ (x : α), x ∈ tl → ∀ (b : β), f x b = g x b
⊢ foldr f b (hd :: tl) = foldr g b (hd :: tl)

Tactic:
simp only [foldr, ih H.2, H.1]

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

Goal state before:
pp: l : List ℤ
n : ℤ
⊢ l.sum % n = (map (fun x ↦ x % n) l).sum % n

Tactic:
induction l <;> simp [Int.add_emod, *]

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

Goal state before:
pp: q : ℚ≥0
h : q ≠ 0
⊢ q * q⁻¹ = 1

Tactic:
ext; simp [h]

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
⊢ OfScientific.ofScientific m b d = Rat.divInt ↑m ↑(10 ^ d)

Tactic:
← Rat.ofScientific_eq_ofScientific,

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

Goal state before:
pp: case neg
K : Type u_1
inst✝ : NNRatCast K
m : ℕ
b : Bool
d : ℕ
h✝ : ¬b = true
⊢ OfScientific.ofScientific m b d = ↑(m * 10 ^ d)

Tactic:
← Rat.ofScientific_eq_ofScientific,

Goal state after:
case neg
K : Type u_1
inst✝ : NNRatCast K
m : ℕ
b : Bool
d : ℕ
h✝ : ¬b = true
⊢ Rat.ofScientific (OfNat.ofNat m) b (OfNat.ofNat d) = ↑(m * 10 ^ d)
Module: Mathlib.Data.NNRat.Defs

Goal state before:
pp: case inr
p q : ℚ
hp : 0 ≤ p
hq : q ≤ 0
hpq : p * q ≤ 0
⊢ (p * q).toNNRat = p.toNNRat * q.toNNRat

Tactic:
rw [toNNRat_eq_zero.2 hq, toNNRat_eq_zero.2 hpq, mul_zero]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Divisibility

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
a b : α
inst✝ : Subsingleton αˣ
⊢ a ∣ b → b ∣ a → a = b

Tactic:
by
  rintro ⟨c, rfl⟩ ⟨d, hcd⟩
  rw [mul_assoc, eq_comm, mul_right_eq_self₀, mul_eq_one] at hcd
  obtain ⟨rfl, -⟩ | rfl := hcd <;> simp

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

Goal state before:
pp: α : Type u_3
inst✝ : DivisionRing α
p q : ℚ
hp : ↑p.den ≠ 0
hq : ↑q.num ≠ 0
⊢ ↑(p / q) = ↑p / ↑q

Tactic:
rw [div_def', cast_divInt_of_ne_zero, cast_def, cast_def, div_eq_mul_inv (_ / _), inv_div,
    (Int.commute_cast _ _).div_mul_div_comm (Nat.commute_cast _ _)]
  · push_cast
    rfl
  · push_cast
    exact mul_ne_zero hp hq

Goal state after:
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; rfl

Goal state after:
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; rfl

Goal state after:
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; rfl

Goal state after:
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; rfl

Goal state after:
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; rfl

Goal state after:
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; rfl

Goal state after:
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; rfl

Goal state after:
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; rfl

Goal state after:
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; rfl

Goal state after:
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; rfl

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

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
i : CompleteLinearOrder α
a b : α
⊢ min a b = if a ≤ b then a else b

Tactic:
split_ifs with h
    · simp [h]
    · simp [(CompleteLinearOrder.le_total a b).resolve_left h]

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

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
i : CompleteLinearOrder α
a b : α
⊢ max a b = if a ≤ b then b else a

Tactic:
split_ifs with h
    · simp [h]
    · simp [(CompleteLinearOrder.le_total a b).resolve_left h]

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

Goal state before:
pp: α : Type u_1
ι : Type u_12
t : Set ι
s : ι → Set α
H : Nonempty α
w : ⋃ i ∈ t, s i = ⊤
⊢ t.Nonempty

Tactic:
obtain ⟨x, m, -⟩ := exists_set_mem_of_union_eq_top t s w H.some
  exact ⟨x, m⟩

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLattice α
minAx : MinimalAxioms α
f : (i : ι) → κ i → α
⊢ ⨅ g, ⨆ i, f i (g i) ≤ ⨆ i, ⨅ j, f i j

Tactic:
rw [minAx.iInf_iSup_eq']

Goal state after:
α : Type u
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLattice α
minAx : MinimalAxioms α
f : (i : ι) → κ i → α
⊢ ⨆ g, ⨅ i, f (g i) (i (g i)) ≤ ⨆ i, ⨅ j, f i j
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:

Tactic:
_ ≤ ⨆ 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 only [minAx.iSup_iInf_eq, iSup_ulift, iSup_bool_eq, le_iInf_iff]
        exact fun x ↦ biInf_le _ (x (.up false)).2
      _ = _ := by simp [sInf_eq_iInf', iInf_unique, iSup_bool_eq]

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

Goal state before:
pp: α : Type u_1
ι : Sort u_5
inst✝ : CompleteLattice α
f : ι → α
x✝ : α
⊢ x✝ ∈ Iic (⨅ i, f i) ↔ x✝ ∈ ⋂ i, Iic (f i)

Tactic:
simp only [mem_Iic, le_iInf_iff, mem_iInter]

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case fst
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝¹ : CompletelyDistribLattice α
inst✝ : CompletelyDistribLattice β
ι✝ : Type (max u v)
κ✝ : ι✝ → Type (max u v)
f : (a : ι✝) → κ✝ a → α × β
⊢ (⨅ a, ⨆ b, f a b).1 = (⨆ g, ⨅ a, f a (g a)).1

Tactic:
simp [fst_iSup, fst_iInf, snd_iSup, snd_iInf, iInf_iSup_eq]

Goal state after: