mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Nat.Even

Goal state before:
pp: m n : ℕ
⊢ Even (m * n) ↔ Even m ∨ Even n

Tactic:
rcases mod_two_eq_zero_or_one m with h₁ | h₁ <;> rcases mod_two_eq_zero_or_one n with h₂ | h₂

Goal state after:
case inl.inl
m n : ℕ
h₁ : m % 2 = 0
h₂ : n % 2 = 0
⊢ Even (m * n) ↔ Even m ∨ Even n

case inl.inr
m n : ℕ
h₁ : m % 2 = 0
h₂ : n % 2 = 1
⊢ Even (m * n) ↔ Even m ∨ Even n

case inr.inl
m n : ℕ
h₁ : m % 2 = 1
h₂ : n % 2 = 0
⊢ Even (m * n) ↔ Even m ∨ Even n

case inr.inr
m n : ℕ
h₁ : m % 2 = 1
h₂ : n % 2 = 1
⊢ Even (m * n) ↔ Even m ∨ Even n
Module: Mathlib.Algebra.Ring.Hom.Defs

Goal state before:
pp: α : Type u_2
β : Type u_3
x✝¹ : NonAssocSemiring α
x✝ : NonAssocSemiring β
f : α →+* β
⊢ 0 = 1 ↔ f 1 = 0

Tactic:
by rw [map_one, eq_comm]

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

Goal state before:
pp: case neg.inl
M₀ : Type u_1
inst✝ : MonoidWithZero M₀
a b : M₀
h : Commute a b
hab : ¬IsUnit (a * b)
ha : ¬IsUnit a
⊢ (a * b)⁻¹ʳ = b⁻¹ʳ * a⁻¹ʳ

Tactic:
rw [inverse_non_unit _ hab, inverse_non_unit _ ha, mul_zero]

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

Goal state before:
pp: A : Type u_2
inst✝ : DivisionRing A
m : ℚ
⊢ m • 1 = ↑m

Tactic:
rw [Rat.smul_def, mul_one]

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

Goal state before:
pp: α : Type u_1
inst✝³ : Mul α
inst✝² : LinearOrder α
a b c d : α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
h : a * b < c * d
⊢ min a b < max c d

Tactic:
min_lt_iff,

Goal state after:
α : Type u_1
inst✝³ : Mul α
inst✝² : LinearOrder α
a b c d : α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
h : a * b < c * d
⊢ a < max c d ∨ b < max c d
Module: Mathlib.Algebra.Order.Ring.Defs

Goal state before:
pp: R : Type u
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b c : R
h : a + c + b * c ≤ b
⊢ 1 + a ≤ 1 + b - (1 + b) * c

Tactic:
one_add_mul,

Goal state after:
R : Type u
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b c : R
h : a + c + b * c ≤ b
⊢ 1 + a ≤ 1 + b - (c + b * c)
Module: Mathlib.Algebra.Order.Ring.Defs

Goal state before:
pp: R : Type u
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b c : R
h : c + b * c ≤ a + b
⊢ 1 - a ≤ 1 + b - (1 + b) * c

Tactic:
one_add_mul,

Goal state after:
R : Type u
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b c : R
h : c + b * c ≤ a + b
⊢ 1 - a ≤ 1 + b - (c + b * c)
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : PartialOrder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : MulPosStrictMono R
inst✝¹ : AddRightStrictMono R
inst✝ : AddRightReflectLT R
h : b < a
hc : c < 0
⊢ a * c < b * c

Tactic:
obtain ⟨d, hcd⟩ := exists_add_of_le hc.le
  refine (add_lt_add_iff_right (b * d + a * d)).1 ?_
  calc
    _ = b * d := by rw [add_left_comm, ← mul_add, ← hcd, mul_zero, add_zero]
    _ < a * d := mul_lt_mul_of_pos_right h <| hcd.trans_lt <| add_lt_of_neg_left _ hc
    _ = _ := by rw [← add_assoc, ← mul_add, ← hcd, mul_zero, zero_add]

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

Goal state before:
pp: case inl
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b : G₀
hb : 0 ≤ b
hc : 0 ≤ 0
h : a ≤ 0⁻¹ * b
⊢ 0 * a ≤ b

pp: case inr
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b c : G₀
hb : 0 ≤ b
hc✝ : 0 ≤ c
h : a ≤ c⁻¹ * b
hc : 0 < c
⊢ c * a ≤ b

Tactic:
· simpa using hb

Goal state after:
case inr
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b c : G₀
hb : 0 ≤ b
hc✝ : 0 ≤ c
h : a ≤ c⁻¹ * b
hc : 0 < c
⊢ c * a ≤ b
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: case inl
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b : G₀
hb : 0 ≤ b
hc : 0 ≤ 0
h : a ≤ b * 0⁻¹
⊢ a * 0 ≤ b

pp: case inr
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
hb : 0 ≤ b
hc✝ : 0 ≤ c
h : a ≤ b * c⁻¹
hc : 0 < c
⊢ a * c ≤ b

Tactic:
· simpa using hb

Goal state after:
case inr
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
hb : 0 ≤ b
hc✝ : 0 ≤ c
h : a ≤ b * c⁻¹
hc : 0 < c
⊢ a * c ≤ b
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b c d : G₀
hb : 0 < b
hd : 0 < d
⊢ a / b ≤ c / d ↔ a * d ≤ c * b

Tactic:
by
  rw [div_le_iff₀ hb, ← mul_div_right_comm, le_div_iff₀ hd]

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

Goal state before:
pp: R : Type u
inst✝⁴ : Ring R
inst✝³ : LinearOrder R
a b : R
inst✝² : MulPosStrictMono R
inst✝¹ : PosMulStrictMono R
inst✝ : AddLeftMono R
x : R
h : a ≤ b
⊢ 0 ≤ (x - a) * (x - b) ↔ x ≤ a ∨ b ≤ x

Tactic:
rw [mul_nonneg_iff, sub_nonneg, sub_nonneg, sub_nonpos, sub_nonpos,
    and_iff_right_of_imp h.trans, and_iff_left_of_imp h.trans', or_comm]

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

Goal state before:
pp: M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulLeftMono M
a : M
n : ℕ
ha : 1 ≤ a
hn : n ≠ 0
⊢ a ≤ a ^ n

Tactic:
by
  simpa using pow_le_pow_right' ha (Nat.one_le_iff_ne_zero.2 hn)

Goal state after:
Module: Mathlib.Algebra.Ring.Int.Parity

Goal state before:
pp: n : ℕ
⊢ IsSquare ↑n ↔ IsSquare n

Tactic:
constructor <;> rintro ⟨x, h⟩
  · exact ⟨x.natAbs, (natAbs_mul_natAbs_eq h.symm).symm⟩
  · exact ⟨x, mod_cast h⟩

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs

Goal state before:
pp: α : Type u
inst✝² : Monoid α
inst✝¹ : LinearOrder α
inst✝ : CanonicallyOrderedMul α
a b c : α
⊢ min (a * b) c = min (min a c * min b c) c

Tactic:
simpa [min_comm _ c] using min_mul_distrib c a b

Goal state after:
Module: Mathlib.Algebra.Regular.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Monoid R
a b : R
ha : IsLeftRegular a
h : b = 1
⊢ a * b = a

Tactic:
rw [h, mul_one]

Goal state after:
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a b : α
⊢ ¬a + b = ⊤ ↔ ¬(a = ⊤ ∨ b = ⊤)

Tactic:
not_or

Goal state after:
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a b : α
⊢ ¬a + b = ⊤ ↔ ¬a = ⊤ ∧ ¬b = ⊤
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : AddMonoidWithOne α
n : ℕ
⊢ (if n + 1 = 0 then 0 else ↑↑(n + 1)) = (if n = 0 then 0 else ↑↑n) + 1

Tactic:
cases n <;> simp

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

Goal state before:
pp: G₀ : Type u_1
M₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : MulZeroOneClass M₀
inst✝ : Nontrivial M₀
f : G₀ →*₀ M₀
x : G₀
⊢ x ≠ 0 → f x ≠ 0

Tactic:
intro hx H

Goal state after:
G₀ : Type u_1
M₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : MulZeroOneClass M₀
inst✝ : Nontrivial M₀
f : G₀ →*₀ M₀
x : G₀
hx : x ≠ 0
H : f x = 0
⊢ False
Module: Mathlib.Data.Nat.Find

Goal state before:
pp: case mpr
m : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
⊢ (p m ∧ ∀ (n : ℕ), n < m → ¬p n) → Nat.find h = m

Tactic:
· rintro ⟨hm, hlt⟩
    have := Nat.find_min' h hm
    grind

Goal state after:
Module: Mathlib.Data.Nat.Find

Goal state before:
pp: P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
h : ¬P (n + 1)
⊢ findGreatest P (n + 1) = findGreatest P n

Tactic:
by
  simp [Nat.findGreatest, h]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : Nonempty α
inst✝ : NoTopOrder α
x : WithBot (WithTop α)
⊢ x = ⊤ ↔ ∀ (a : α), ↑↑a ≤ x

Tactic:
refine ⟨by simp_all, fun H ↦ ?_⟩

Goal state after:
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : Nonempty α
inst✝ : NoTopOrder α
x : WithBot (WithTop α)
H : ∀ (a : α), ↑↑a ≤ x
⊢ x = ⊤
Module: Mathlib.Data.Int.LeastGreatest

Goal state before:
pp: P : ℤ → Prop
Hbdd : ∃ b, ∀ (z : ℤ), P z → z ≤ b
Hinh : ∃ z, P z
⊢ ∃ ub, P ub ∧ ∀ (z : ℤ), P z → z ≤ ub

Tactic:
classical
  let ⟨b, Hb⟩ := Hbdd
  let ⟨lb, H⟩ := greatestOfBdd b Hb Hinh
  exact ⟨lb, H⟩

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 < x

Tactic:
← log_lt_log exp_ne_zero hx,

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 ↔ (exp a).log < x.log
Module: Mathlib.Order.Directed

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : IsDirectedOrder α
inst✝ : Preorder β
f g : α → β
hf : Monotone f
hg : Antitone g
h : f ≤ g
m n : α
⊢ f m ≤ g n

Tactic:
obtain ⟨k, hkm, hkn⟩ := exists_ge_ge m n

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : IsDirectedOrder α
inst✝ : Preorder β
f g : α → β
hf : Monotone f
hg : Antitone g
h : f ≤ g
m n k : α
hkm : m ≤ k
hkn : n ≤ k
⊢ f m ≤ g n
Module: Mathlib.Algebra.GroupWithZero.Units.Lemmas

Goal state before:
pp: G₀ : Type u_3
M₀' : Type u_4
F : Type u_6
inst✝⁴ : GroupWithZero G₀
inst✝³ : MulZeroOneClass M₀'
inst✝² : Nontrivial M₀'
inst✝¹ : FunLike F G₀ M₀'
inst✝ : MonoidWithZeroHomClass F G₀ M₀'
f : F
a : G₀
⊢ a ≠ 0 → f a ≠ 0

Tactic:
intro hx H

Goal state after:
G₀ : Type u_3
M₀' : Type u_4
F : Type u_6
inst✝⁴ : GroupWithZero G₀
inst✝³ : MulZeroOneClass M₀'
inst✝² : Nontrivial M₀'
inst✝¹ : FunLike F G₀ M₀'
inst✝ : MonoidWithZeroHomClass F G₀ M₀'
f : F
a : G₀
hx : a ≠ 0
H : f a = 0
⊢ False
Module: Mathlib.Algebra.Order.Ring.Basic

Goal state before:
pp: case ha
R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a b : R
inst✝ : ExistsAddOfLE R
ha : 0 ≤ a
hb : 0 ≤ b
n : ℕ
⊢ 0 ≤ 2 ^ n

Tactic:
exact pow_nonneg zero_le_two _

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

Goal state before:
pp: case inr.inr
R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a b : R
hab : a < b
ha : a ≤ 0
hb : b ≤ 0
⊢ (fun a ↦ a ^ n) a < (fun a ↦ a ^ n) b

Tactic:
obtain ⟨c, hac⟩ := exists_add_of_le ha

Goal state after:
case inr.inr
R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a b : R
hab : a < b
ha : a ≤ 0
hb : b ≤ 0
c : R
hac : 0 = a + c
⊢ (fun a ↦ a ^ n) a < (fun a ↦ a ^ n) b
Module: Mathlib.Data.Set.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t t' : Set β
⊢ image2 f s (t ∪ t') = image2 f s t ∪ image2 f s t'

Tactic:
← image2_swap,

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t t' : Set β
⊢ image2 (fun b a ↦ f a b) (t ∪ t') s = image2 f s t ∪ image2 f s t'
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedRing α
a b : α
⊢ |a * b| = |a| * |b|

Tactic:
by
  rw [abs_eq (mul_nonneg (abs_nonneg a) (abs_nonneg b))]
  rcases le_total a 0 with ha | ha <;> rcases le_total b 0 with hb | hb <;>
    simp only [abs_of_nonpos, abs_of_nonneg, true_or, or_true, neg_mul, mul_neg, neg_neg, *]

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

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedRing α
n : ℕ
⊢ |1| ^ n = 1

Tactic:
abs_one,

Goal state after:
α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedRing α
n : ℕ
⊢ 1 ^ n = 1
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:
← not_nonempty_iff_eq_empty,

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
⊢ ¬(image2 f s t).Nonempty ↔ s = ∅ ∨ t = ∅
Module: Mathlib.Order.BoundedOrder.Monotone

Goal state before:
pp: α : Type u
β : Type v
inst✝² : LinearOrder α
inst✝¹ : Preorder β
inst✝ : OrderBot β
f : α → β
H : StrictMono f
a : α
h_bot : f a = ⊥
x : α
p : β
⊢ f a ≤ p

Tactic:
by
      rw [h_bot]
      exact bot_le

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_3
β : Type u_4
f : α → β
s : Set ↑(range f)
x : ↑(rangeSplitting f '' s)
⊢ ⟨f ↑x, ⋯⟩ ∈ s

Tactic:
rcases x with ⟨x, ⟨y, ⟨m, rfl⟩⟩⟩

Goal state after:
α✝¹ : Sort u
β✝¹ : Sort v
γ : Sort w
α✝ : Type u_1
β✝ : Type u_2
α : Type u_3
β : Type u_4
f : α → β
s : Set ↑(range f)
y : ↑(range f)
m : y ∈ s
⊢ ⟨f ↑⟨rangeSplitting f y, ⋯⟩, ⋯⟩ ∈ s
Module: Mathlib.Logic.Equiv.Set

Goal state before:
pp: α✝¹ : Sort u
β✝¹ : Sort v
γ : Sort w
α✝ : Type u_1
β✝ : Type u_2
α : Type u_3
β : Type u_4
f : α → β
s : Set ↑(range f)
x : ↑(rangeSplitting f '' s)
⊢ (fun x ↦ ⟨rangeSplitting f ↑x, ⋯⟩) ((fun x ↦ ⟨⟨f ↑x, ⋯⟩, ⋯⟩) x) = x

Tactic:
rcases x with ⟨x, ⟨y, ⟨m, rfl⟩⟩⟩

Goal state after:
α✝¹ : Sort u
β✝¹ : Sort v
γ : Sort w
α✝ : Type u_1
β✝ : Type u_2
α : Type u_3
β : Type u_4
f : α → β
s : Set ↑(range f)
y : ↑(range f)
m : y ∈ s
⊢ (fun x ↦ ⟨rangeSplitting f ↑x, ⋯⟩) ((fun x ↦ ⟨⟨f ↑x, ⋯⟩, ⋯⟩) ⟨rangeSplitting f y, ⋯⟩) = ⟨rangeSplitting f y, ⋯⟩
Module: Mathlib.Order.Bounds.OrderIso

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
s : Set α
x : α
⊢ IsLUB (⇑f '' s) (f x) ↔ IsLUB s x

Tactic:
rw [isLUB_image, f.symm_apply_apply]

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

Goal state before:
pp: case inr.inr
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
hb : 0 < b
⊢ 1 < a / b ↔ 0 < b ∧ b < a ∨ b < 0 ∧ a < b

Tactic:
· simp [hb, hb.not_gt, one_lt_div]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
l : List β
H : Forall₂ R [] l
⊢ l = []

Tactic:
by cases H; rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
l : List α
H : Forall₂ R l []
⊢ l = []

Tactic:
by cases H; rfl

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

Goal state before:
pp: α : Type u
n : ℕ
a : α
l : List α
⊢ l.insertIdx n a ⊆ a :: l

Tactic:
by
  intro b hb
  simpa using eq_or_mem_of_mem_insertIdx hb

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

Goal state before:
pp: α : Type u
β : Type v
a : α
l : List α
x : α
n : ℕ
hn : n ≤ l.length
⊢ n < (l.insertIdx n x).length

Tactic:
length_insertIdx_of_le_length hn,

Goal state after:
α : Type u
β : Type v
a : α
l : List α
x : α
n : ℕ
hn : n ≤ l.length
⊢ n < l.length + 1
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: case cons.nil
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
inst✝ : IsTrans α Rₐ
head✝ : α
tail✝ : List α
ih : ∀ (a b : List α), SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b tail✝ → SublistForall₂ Rₐ a tail✝
a : List α
h1 : SublistForall₂ Rₐ a []
⊢ SublistForall₂ Rₐ a (head✝ :: tail✝)

Tactic:
cases h1

Goal state after:
case cons.nil.nil
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
inst✝ : IsTrans α Rₐ
head✝ : α
tail✝ : List α
ih : ∀ (a b : List α), SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b tail✝ → SublistForall₂ Rₐ a tail✝
⊢ SublistForall₂ Rₐ [] (head✝ :: tail✝)
Module: Mathlib.Data.List.Perm.Basic

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

Tactic:
| intro hn hnm =>

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : GroupWithZero α
a : α
m n : ℤ
ha : ¬a = 0
hn : n = 0
⊢ zpow' a (m * n) = zpow' (zpow' a m) n

Tactic:
hn

Goal state after:
case pos
α : Type u_1
inst✝ : GroupWithZero α
a : α
m n : ℤ
ha : ¬a = 0
hn : n = 0
⊢ zpow' a (m * 0) = zpow' (zpow' a m) 0
Module: Mathlib.Data.List.Basic

Goal state before:
pp: case refine_2
α : Type u
l₁ l₂ : List α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
hl : l₁ <+: l₂
a : α
h : idxOf a l₂ < l₁.length
⊢ a ∈ l₁

Tactic:
have := hl.idxOf_le a
    grind [List.idxOf_lt_length_iff]

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

Goal state before:
pp: G : Type u_7
inst✝ : CommGroup G
n : ℕ
f : ℕ → G
h : ((fun x ↦ x⁻¹) ∘ fun k ↦ f (k + 1) / f k) = fun k ↦ f k / f (k + 1)
⊢ (map (fun k ↦ f (k + 1) / f k) (range n)).prod = f n / f 0

Tactic:
← inv_inj,

Goal state after:
G : Type u_7
inst✝ : CommGroup G
n : ℕ
f : ℕ → G
h : ((fun x ↦ x⁻¹) ∘ fun k ↦ f (k + 1) / f k) = fun k ↦ f k / f (k + 1)
⊢ (map (fun k ↦ f (k + 1) / f k) (range n)).prod⁻¹ = (f n / f 0)⁻¹
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
p : α → Bool
l : List α
⊢ filter p l = foldr (fun a out ↦ bif p a then a :: out else out) [] l

Tactic:
induction l <;> simp [*, filter]; rfl

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

Goal state before:
pp: a b c d : ℤ
b0 : 0 < b
d0 : 0 < d
⊢ 0 ≤ c /. d - a /. b ↔ a * d ≤ c * b

Tactic:
← Int.sub_nonneg

Goal state after:
a b c d : ℤ
b0 : 0 < b
d0 : 0 < d
⊢ 0 ≤ c /. d - a /. b ↔ 0 ≤ c * b - a * d
Module: Mathlib.Algebra.Field.Rat

Goal state before:
pp: a : ℚ≥0
⊢ a ^ 0 = 1

Tactic:
by ext; apply Field.zpow_zero'

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoid α
x y z : α
inst✝ : DecompositionMonoid α
H1 : IsRelPrime x y
H2 : IsRelPrime x z
⊢ IsRelPrime x (y * z)

Tactic:
rw [isRelPrime_comm] at H1 H2 ⊢

Goal state after:
α : Type u_1
inst✝¹ : CommMonoid α
x y z : α
inst✝ : DecompositionMonoid α
H1 : IsRelPrime y x
H2 : IsRelPrime z x
⊢ IsRelPrime (y * z) x
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:
rintro ⟨c, rfl⟩ ⟨d, hcd⟩

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
a : α
inst✝ : Subsingleton αˣ
c d : α
hcd : a = a * c * d
⊢ a = a * c
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: case mpr
q : ℚ
⊢ IsSquare q.num ∧ IsSquare q.den → IsSquare q

Tactic:
rintro ⟨⟨nr, hnr⟩, ⟨dr, hdr⟩⟩
    refine ⟨nr / dr, ?_⟩
    rw [div_mul_div_comm, ← Int.cast_mul, ← Nat.cast_mul, ← hnr, ← hdr, num_div_den]

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

Goal state before:
pp: q r : ℚ
s : ℚ := (q.num * ↑r.den + r.num * ↑q.den) /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * ↑r.den + r.num * ↑q.den = c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den
⊢ c * ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den * (q + r).num =
    c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num * ↑(q + r).den

Tactic:
rw [Int.mul_assoc]

Goal state after:
q r : ℚ
s : ℚ := (q.num * ↑r.den + r.num * ↑q.den) /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * ↑r.den + r.num * ↑q.den = c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den
⊢ c * (↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den * (q + r).num) =
    c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num * ↑(q + r).den
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: q r : ℚ
s : ℚ := (q.num * ↑r.den + r.num * ↑q.den) /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * ↑r.den + r.num * ↑q.den = c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den
⊢ c * (↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den * (q + r).num) =
    c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num * ↑(q + r).den

Tactic:
rw [Int.mul_assoc]

Goal state after:
q r : ℚ
s : ℚ := (q.num * ↑r.den + r.num * ↑q.den) /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * ↑r.den + r.num * ↑q.den = c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den
⊢ c * (↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den * (q + r).num) =
    c * ((↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num * ↑(q + r).den)
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: q r : ℚ
s : ℚ := (q.num * ↑r.den + r.num * ↑q.den) /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * ↑r.den + r.num * ↑q.den = c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den
⊢ c * (↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den * (q + r).num) =
    c * ((↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num * ↑(q + r).den)

Tactic:
rw [Int.mul_assoc]

Goal state after:
q r : ℚ
s : ℚ := (q.num * ↑r.den + r.num * ↑q.den) /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * ↑r.den + r.num * ↑q.den = c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den
⊢ c * (↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den * (q + r).num) =
    c * ((↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num * ↑(q + r).den)
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑(q.num * r.den + r.num * q.den) / ↑(q.den * r.den) = ↑q.num / ↑q.den + ↑r.num / ↑r.den

pp: case hb
α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑(q.den * r.den) ≠ 0

Tactic:
mul_comm _ q.den,

Goal state after:
α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑(q.num * r.den + q.den * r.num) / ↑(q.den * r.den) = ↑q.num / ↑q.den + ↑r.num / ↑r.den

case hb
α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑(q.den * r.den) ≠ 0
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: q r : ℚ
s : ℚ := (q.num * ↑r.den + r.num * ↑q.den) /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * ↑r.den + r.num * ↑q.den = c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den
⊢ c * ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den * (q + r).num =
    c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num * ↑(q + r).den

Tactic:
repeat rw [Int.mul_assoc]

Goal state after:
q r : ℚ
s : ℚ := (q.num * ↑r.den + r.num * ↑q.den) /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * ↑r.den + r.num * ↑q.den = c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den
⊢ c * (↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den * (q + r).num) =
    c * ((↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num * ↑(q + r).den)
Module: Mathlib.Tactic.CancelDenoms.Core

Goal state before:
pp: α : Type u_1
inst✝ : CommRing α
n e1 t1 k l : α
e2 : ℕ
h1 : n * e1 = t1
h2 : l * n ^ e2 = k
⊢ k * e1 ^ e2 = l * t1 ^ e2

Tactic:
rw [← h2, ← h1, mul_pow, mul_assoc]

Goal state after:
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; simp [Nat.succ_mul, pow_add]

Goal state after:
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; simp [Nat.succ_mul, pow_add]

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

Goal state before:
pp: n : ℕ
⊢ n ∈ {0} ∪ range succ ↔ n ∈ univ

Tactic:
cases n <;> simp

Goal state after: