mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.BinaryRec

Goal state before:
pp: case false
x n : Nat
⊢ 2 * x < 2 ^ (n + 1) ↔ x < 2 ^ n

Tactic:
lia

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

Goal state before:
pp: case true
x n : Nat
⊢ 2 * x + 1 < 2 ^ (n + 1) ↔ x < 2 ^ n

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Group.Semiconj.Defs

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a x y b : G
⊢ b * (a * (x * b⁻¹)) = b * (y * (a * b⁻¹)) ↔ a * x = y * a

Tactic:
rw [mul_left_cancel_iff, ← mul_assoc, ← mul_assoc, mul_right_cancel_iff]

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

Goal state before:
pp: M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
k : ℕ
m n : M
k' : ℕ
hk : k + 1 = k'
⊢ k' ≠ 0

Tactic:
lia

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

Goal state before:
pp: M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
k k' : ℕ
k'0 : k' ≠ 0
ih :
  ∀ (m n : M),
    k' ≠ 0 →
      Nat.binaryRec (motive := fun x ↦ M → M → M) (fun y x ↦ y)
          (fun bn _n fn y x ↦ fn (bif bn then y * x else y) (x * x)) k' m n =
        m * npowRec' k' n
m n : M
hk : Nat.bit true k' ≠ 0
⊢ 2 * k' ≠ 0

Tactic:
lia

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

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
a : M
m n : ℕ
⊢ (a ^ m) ^ n = (a ^ n) ^ m

Tactic:
rw [← pow_mul, Nat.mul_comm, pow_mul]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Type u_1
inst1 inst2 : BEq α
inst✝¹ : LawfulBEq α
inst✝ : LawfulBEq α
⊢ inst1 = inst2

Tactic:
ext
  simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Subsingleton α
e : Perm α
⊢ ⇑(Equiv.refl α) = id

Tactic:
coe_refl

Goal state after:
α : Type u_1
inst✝ : Subsingleton α
e : Perm α
⊢ id = id
Module: Mathlib.Algebra.Group.Pi.Basic

Goal state before:
pp: I : Type u
α : Type u_4
inst✝² : DecidableEq I
inst✝¹ : Subsingleton I
inst✝ : One α
i : I
x : α
j : I
⊢ Pi.mulSingle i x j = x

Tactic:
by rw [Subsingleton.elim j i, Pi.mulSingle_eq_same]

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
⊢ (a < b ↔ b < a) ↔ (a ≤ b ↔ b ≤ a)

Tactic:
by
  grind [= lt_iff_le_not_ge]

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
⊢ (a < b ↔ a ≤ b) ↔ (b < a ↔ b ≤ a)

Tactic:
by
  grind [= lt_iff_le_not_ge]

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
⊢ (a < b ↔ b ≤ a) ↔ (b < a ↔ a ≤ b)

Tactic:
by
  grind [= lt_iff_le_not_ge]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Nonempty α
inst✝ : Nonempty β
f : α → γ
g : β → δ
h : Injective (map f g)
b₁ b₂ : β
hb : g b₁ = g b₂
inhabited_h : Inhabited α
⊢ b₁ = b₂

Tactic:
injection @h (default, b₁) (default, b₂) (congr_arg (Prod.mk (f default)) hb :)

Goal state after:
Module: Mathlib.Tactic.GCongr.Core

Goal state before:
pp: declName : Name
stx : Syntax
kind : AttributeKind
prio : Nat
strict forGrw : Bool
cinfo : ConstantInfo
xs : Array Expr
type : Expr
c : Name
us✝ : List Level
i✝ i : Nat
h : i + 1 ≤ xs.size
⊢ i < xs.size

Tactic:
lia

Goal state after:
Module: Mathlib.Tactic.GCongr.Core

Goal state before:
pp: declName : Name
stx : Syntax
kind : AttributeKind
prio : Nat
strict forGrw : Bool
cinfo : ConstantInfo
xs : Array Expr
type : Expr
c : Name
us✝ : List Level
i✝ i : Nat
h : i + 1 ≤ xs.size
⊢ i ≤ xs.size

Tactic:
lia

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
le✝ A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), le✝ a a
le_trans✝¹ : ∀ (a b c : α), le✝ a b → le✝ b c → le✝ a c
A_iff : ∀ (a b : α), A_lt a b ↔ le✝ a b ∧ ¬le✝ b a
B_lt : α → α → Prop
le_refl✝ : ∀ (a : α), le✝ a a
le_trans✝ : ∀ (a b c : α), le✝ a b → le✝ b c → le✝ a c
B_iff : ∀ (a b : α), B_lt a b ↔ le✝ a b ∧ ¬le✝ b a
a b : α
⊢ (le✝ a b ∧ ¬le✝ b a) = B_lt a b

Tactic:
B_iff

Goal state after:
α : Type u_2
le✝ A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), le✝ a a
le_trans✝¹ : ∀ (a b c : α), le✝ a b → le✝ b c → le✝ a c
A_iff : ∀ (a b : α), A_lt a b ↔ le✝ a b ∧ ¬le✝ b a
B_lt : α → α → Prop
le_refl✝ : ∀ (a : α), le✝ a a
le_trans✝ : ∀ (a b c : α), le✝ a b → le✝ b c → le✝ a c
B_iff : ∀ (a b : α), B_lt a b ↔ le✝ a b ∧ ¬le✝ b a
a b : α
⊢ (le✝ a b ∧ ¬le✝ b a) = (le✝ a b ∧ ¬le✝ b a)
Module: Mathlib.Data.Int.Order.Basic

Goal state before:
pp: a b : ℤ
⊢ (0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0) ∧ a ≠ 0 ∧ b ≠ 0 ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0

Tactic:
lia

Goal state after:
Module: Mathlib.Data.Int.Order.Basic

Goal state before:
pp: a b : ℤ
⊢ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0 ↔ ¬(0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b)

Tactic:
lia

Goal state after:
Module: Mathlib.Data.Int.Order.Basic

Goal state before:
pp: a b : ℤ
⊢ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 ↔ ¬(0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b)

Tactic:
lia

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

Goal state before:
pp: n : ℕ
hn : n % 2 = 1
⊢ 2 * (n / 2) = n - 1

Tactic:
lia

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

Goal state before:
pp: a✝ b c d e m n k✝ : ℕ
p : ℕ → Prop
motive : ℕ → Sort u_1
k : ℕ
base : (i : ℕ) → i < k → motive i
step : (n : ℕ) → ((i : ℕ) → i < k → motive (n + i)) → motive (n + k)
a : ℕ
h : ¬a < k
⊢ a - k + k = a

Tactic:
lia

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

Goal state before:
pp: P : ℕ → ℕ → Prop
ha : ∀ (a : ℕ), P (a + 1) (a + 1)
hb : ∀ (b : ℕ), P 0 (b + 1)
hd : ∀ (a b : ℕ), a < b → P (a + 1) b → P a (b + 1) → P (a + 1) (b + 1)
a b : ℕ
h : a + 1 < b + 1
⊢ a + 1 = b ∨ a + 1 < b

Tactic:
lia

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

Goal state before:
pp: n : ℕ
⊢ ¬2 ∣ 2 * n + 1

Tactic:
lia

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

Goal state before:
pp: n : ℕ
inst✝ : n.AtLeastTwo
this : 2 ≤ n
⊢ n - 1 ≠ 0

Tactic:
lia

Goal state after:
Module: Mathlib.Order.Compare

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, o.Compares a b → o.Compares a' b'
o : Ordering
⊢ o.Compares a b ↔ o.Compares a' b'

Tactic:
refine ⟨h, fun ho => ?_⟩
  rcases lt_trichotomy a b with hab | hab | hab
  · have hab : Compares Ordering.lt a b := hab
    rwa [ho.inj (h hab)]
  · have hab : Compares Ordering.eq a b := hab
    rwa [ho.inj (h hab)]
  · have hab : Compares Ordering.gt a b := hab
    rwa [ho.inj (h hab)]

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

Goal state before:
pp: β : Type v
r : β → β → Prop
inst✝ : IsTrans β r
f : ℤ → β
h : ∀ (n : ℤ), r (f n) (f (n + 1))
a b : ℤ
hab : a < b
⊢ r (f a) (f b)

Tactic:
by
  rcases lt.dest hab with ⟨n, rfl⟩
  clear hab
  induction n with
  | zero => rw [Int.ofNat_one]; apply h
  | succ n ihn => rw [Int.natCast_succ, ← Int.add_assoc]; exact _root_.trans ihn (h _)

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

Goal state before:
pp: α : Type u
s t : Set α
⊢ s ∪ t = ∅ ↔ s = ∅ ∧ t = ∅

Tactic:
simp only [← subset_empty_iff]

Goal state after:
α : Type u
s t : Set α
⊢ s ∪ t ⊆ ∅ ↔ s ⊆ ∅ ∧ t ⊆ ∅
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: n : ℕ
ih :
  ∀ (m : ℕ),
    m < n →
      ∀ {f : ℕ → ℕ},
        Antitone f →
          (∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)) → f 0 = m → ∃ n, n ≤ m ∧ ∀ (m : ℕ), n ≤ m → f m = f n
f : ℕ → ℕ
hfmono : Antitone f
hfstab : ∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)
h : f 0 = n
heq : ¬f 0 = f 1
hlt : f 1 < f 0
g : ℕ → ℕ := fun i ↦ f (i + 1)
hg_anti : Antitone g
p : ℕ
hp : p ≤ f 1
hp' : ∀ (m : ℕ), p ≤ m → g m = g p
m : ℕ
hm : p + 1 ≤ m
⊢ p ≤ m - 1

Tactic:
lia

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

Goal state before:
pp: α : Type u_1
a : α
n : ℕ
hn : n > 0
H : n ≤ 1
⊢ n = 1

Tactic:
lia

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

Goal state before:
pp: f : ℕ → ℕ
mono_f : Monotone f
c : ℕ
ih : (∀ (n : ℕ), f n ≤ c) → ∃ b N, ∀ (n : ℕ), n ≥ N → f n = b
N : ℕ
hc : f N ≤ c + 1
hN : c < f N
⊢ f N = c + 1

Tactic:
lia

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

Goal state before:
pp: case h
f : ℕ → ℕ
c : ℕ
ih : (∀ (n : ℕ), f n ≤ c) → ∃ b N, ∀ (n : ℕ), n ≥ N → f n = b
N : ℕ
hN : f N = c + 1
n : ℕ
hc : f n ≤ c + 1
mono_f : f N ≤ f n
hn : n ≥ N
⊢ f n = c + 1

Tactic:
lia

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

Goal state before:
pp: case refine_1
α : Type u
a : α
⊢ {a}.Nonempty ∧ {a}.Subsingleton

Tactic:
exact ⟨singleton_nonempty a, subsingleton_singleton⟩

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

Goal state before:
pp: α : Type u
a : α
s : Set α
ha : a ∈ s
⊢ s = {a} ∨ s.Nontrivial

Tactic:
rw [← subsingleton_iff_singleton ha]; exact s.subsingleton_or_nontrivial

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
β : Type v
e : α ≃ β
inst✝¹ : LinearOrder β
inst✝ : DecidableEq α
max : Max α := e.max
min : Min α := e.min
preorder : Preorder α := e.preorder
compare : Ord α := e.ord
⊢ LinearOrder α

Tactic:
apply e.injective.linearOrder

Goal state after:
case le
α : Type u
β : Type v
e : α ≃ β
inst✝¹ : LinearOrder β
inst✝ : DecidableEq α
max : Max α := ⋯
min : Min α := ⋯
preorder : Preorder α := ⋯
compare : Ord α := ⋯
⊢ ∀ {x y : α}, e x ≤ e y ↔ x ≤ y

case lt
α : Type u
β : Type v
e : α ≃ β
inst✝¹ : LinearOrder β
inst✝ : DecidableEq α
max : Max α := ⋯
min : Min α := ⋯
preorder : Preorder α := ⋯
compare : Ord α := ⋯
⊢ ∀ {x y : α}, e x < e y ↔ x < y

case min
α : Type u
β : Type v
e : α ≃ β
inst✝¹ : LinearOrder β
inst✝ : DecidableEq α
max : Max α := ⋯
min : Min α := ⋯
preorder : Preorder α := ⋯
compare : Ord α := ⋯
⊢ ∀ (x y : α), e (x ⊓ y) = Min.min (e x) (e y)

case max
α : Type u
β : Type v
e : α ≃ β
inst✝¹ : LinearOrder β
inst✝ : DecidableEq α
max : Max α := ⋯
min : Min α := ⋯
preorder : Preorder α := ⋯
compare : Ord α := ⋯
⊢ ∀ (x y : α), e (x ⊔ y) = Max.max (e x) (e y)

case compare
α : Type u
β : Type v
e : α ≃ β
inst✝¹ : LinearOrder β
inst✝ : DecidableEq α
max : Max α := ⋯
min : Min α := ⋯
preorder : Preorder α := ⋯
compare : Ord α := ⋯
⊢ ∀ (x y : α), Ord.compare (e x) (e y) = Ord.compare x y
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b c : α
⊢ a ≤ b ⇨ c ↔ b ⊓ a ≤ c

Tactic:
rw [le_himp_iff, inf_comm]

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

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b c : α
⊢ (b ⇨ c) ⊓ (a ⇨ b) ⊓ a ≤ c

Tactic:
simpa using @himp_le_himp_himp_himp

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

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b : α
⊢ b ⇨ a = a ⇨ b ↔ a = b

Tactic:
simp [le_antisymm_iff]

Goal state after:
Module: Mathlib.Order.BooleanAlgebra.Set

Goal state before:
pp: α : Type u_1
s : Set α
a : α
ha : a ∈ s
x✝ : α
⊢ x✝ ∈ insert a (s \ {a}) ↔ x✝ ∈ s

Tactic:
simp +contextual [or_and_left, em, ha]

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

Goal state before:
pp: ε : Type u_9
p : ε → Prop
inst✝ : DecidablePred p
ep : Perm { a // p a }
en : Perm { a // ¬p a }
a : ε
h : p a
⊢ (ep.subtypeCongr en) a = ↑(ep ⟨a, h⟩)

Tactic:
by
  simp [Perm.subtypeCongr.apply, h]

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

Goal state before:
pp: ε : Type u_9
p : ε → Prop
inst✝ : DecidablePred p
ep : Perm { a // p a }
en : Perm { a // ¬p a }
a : ε
h : ¬p a
⊢ (ep.subtypeCongr en) a = ↑(en ⟨a, h⟩)

Tactic:
by
  simp [Perm.subtypeCongr.apply, h]

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

Goal state before:
pp: α : Type u_1
s : Set α
⊢ (fun x ↦ x) '' s = s

Tactic:
ext
  simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
t : Set β
f : α → β
u : Set ↑t
⊢ Subtype.val '' t.restrictPreimage f ⁻¹' u = f ⁻¹' Subtype.val '' u

Tactic:
ext
  simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set β
⊢ Sum.inl ⁻¹' Sum.inr '' s = ∅

Tactic:
ext
  simp

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

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
y : β
⊢ y ∈ range (s.piecewise f g) → y ∈ f '' s ∪ g '' sᶜ

Tactic:
rintro ⟨x, rfl⟩
    by_cases h : x ∈ s <;> [left; right] <;> use x <;> simp [h]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
⊢ Sum.inr ⁻¹' Sum.inl '' s = ∅

Tactic:
ext
  simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Option α → β
⊢ (Injective (f ∘ some) ∧ ∀ (x : α), ¬f (some x) = f none) → Injective f

Tactic:
rintro ⟨h_some, h_none⟩ (_ | a) (_ | b) hab

Goal state after:
case none.none
α : Type u_1
β : Type u_2
f : Option α → β
h_some : Injective (f ∘ some)
h_none : ∀ (x : α), ¬f (some x) = f none
hab : f none = f none
⊢ none = none

case none.some
α : Type u_1
β : Type u_2
f : Option α → β
h_some : Injective (f ∘ some)
h_none : ∀ (x : α), ¬f (some x) = f none
b : α
hab : f none = f (some b)
⊢ none = some b

case some.none
α : Type u_1
β : Type u_2
f : Option α → β
h_some : Injective (f ∘ some)
h_none : ∀ (x : α), ¬f (some x) = f none
a : α
hab : f (some a) = f none
⊢ some a = none

case some.some
α : Type u_1
β : Type u_2
f : Option α → β
h_some : Injective (f ∘ some)
h_none : ∀ (x : α), ¬f (some x) = f none
a b : α
hab : f (some a) = f (some b)
⊢ some a = some b
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
i : ι
inst✝ : DecidableEq ι
s : Set (α i)
⊢ eval i ⁻¹' s = {i}.pi (update (fun x ↦ univ) i s)

Tactic:
ext
  simp

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
π : ι ⊕ ι' → Type u_4
t : (i : ι ⊕ ι') → Set (π i)
⊢ ⇑(sumPiEquivProdPi π).symm ⁻¹' univ.pi t = (univ.pi fun i ↦ t (Sum.inl i)) ×ˢ univ.pi fun i ↦ t (Sum.inr i)

Tactic:
ext
  simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
t : Set β
f : α → β
h : BijOn f ∅ t
⊢ t = ∅

Tactic:
simpa using h.surjOn

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
p : Set γ
f : α → β
g : β → γ
hf : InjOn f s
⊢ BijOn (g ∘ f) s p ↔ BijOn g (f '' s) p

Tactic:
simp only [BijOn, InjOn.comp_iff, surjOn_comp_iff, mapsTo_image_iff, hf]

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

Goal state before:
pp: a : ℤ
⊢ a < a + 1

Tactic:
lia

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

Goal state before:
pp: a : ℤ
⊢ a - 1 < a

Tactic:
lia

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

Goal state before:
pp: a b✝ c d m n✝ : ℤ
motive : ℤ → Sort u_1
z b : ℤ
zero : motive b
succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)
pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)
n : ℕ
⊢ motive (b + ↑n + 1) = motive (b + ↑(n + 1))

Tactic:
lia

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

Goal state before:
pp: a b✝ c d m n✝ : ℤ
motive : ℤ → Sort u_1
z b : ℤ
zero : motive b
succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)
pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)
n : ℕ
⊢ motive (b + -[n+1] - 1) = motive (b + -[n + 1+1])

Tactic:
lia

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

Goal state before:
pp: a b✝ c d m n✝ : ℤ
motive : ℤ → Sort u_1
z b : ℤ
zero : motive b
succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)
pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)
n : ℕ
⊢ b + -[n+1] ≤ b

Tactic:
lia

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

Goal state before:
pp: a b✝ c d m n : ℤ
motive : ℤ → Sort u_1
z b : ℤ
zero : motive b
succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)
pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)
⊢ b + (z - b) = z

Tactic:
lia

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

Goal state before:
pp: motive : ℤ → Sort u_1
z b : ℤ
zero : motive b
succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)
pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)
hz : b ≤ z
⊢ z - b = ↑(z - b).toNat

Tactic:
lia

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

Goal state before:
pp: motive : ℤ → Sort u_1
z b : ℤ
zero : motive b
succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)
pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)
hz : b ≤ z
⊢ z + 1 - b = ↑((z - b).toNat + 1)

Tactic:
lia

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

Goal state before:
pp: motive : ℤ → Sort u_1
z b : ℤ
zero : motive b
succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)
pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)
hz : b ≤ z
⊢ b + ↑(z - b).toNat = z

Tactic:
lia

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

Goal state before:
pp: motive : ℤ → Sort u_1
z b : ℤ
zero : motive b
succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)
pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)
hz : z ≤ b
h✝ : z = b
⊢ z - 1 - b = -[(b - z).toNat+1]

Tactic:
lia

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

Goal state before:
pp: motive : ℤ → Sort u_1
z b : ℤ
zero : motive b
succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)
pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)
hz : z ≤ b
h✝ : z = b
⊢ z - b = 0

Tactic:
lia

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

Goal state before:
pp: motive : ℤ → Sort u_1
z b : ℤ
zero : motive b
succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)
pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)
hz : z ≤ b
h✝ : ¬z = b
⊢ z - 1 - b = -[(b - z).toNat+1]

Tactic:
lia

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

Goal state before:
pp: motive : ℤ → Sort u_1
z b : ℤ
zero : motive b
succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)
pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)
hz : z ≤ b
h✝ : ¬z = b
⊢ z - b = -[(b - z - 1).toNat+1]

Tactic:
lia

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

Goal state before:
pp: a b c d m✝ n✝ m : ℤ
motive : (n : ℤ) → m ≤ n → Sort u_1
base : motive m ⋯
succ : (n : ℤ) → (hmn : m ≤ n) → motive n hmn → motive (n + 1) ⋯
n x✝³ : ℤ
x✝² : x✝³ ≤ m
x✝¹ : (hmn : m ≤ x✝³) → motive x✝³ hmn
x✝ : m ≤ x✝³ - 1
⊢ False

Tactic:
lia

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

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
⊢ (∃ s', s' ⊆ s ∧ BijOn f s' t) → SurjOn f s t

Tactic:
· rintro ⟨s', hs', hfs'⟩
    exact hfs'.surjOn.mono hs' (Subset.refl _)

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

Goal state before:
pp: a b c d m✝ n✝ m : ℤ
motive : (n : ℤ) → m ≤ n → Sort u_1
base : motive m ⋯
succ : (n : ℤ) → (hmn : m ≤ n) → motive n hmn → motive (n + 1) ⋯
n : ℤ
hmn : m ≤ n
⊢ m ≤ n + 1

Tactic:
lia

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

Goal state before:
pp: a b c d m✝ n✝ m : ℤ
motive : (n : ℤ) → n ≤ m → Sort u_1
base : motive m ⋯
n : ℤ
hnm : n ≤ m
⊢ n - 1 ≤ m

Tactic:
lia

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

Goal state before:
pp: a b c d m✝ n✝ m : ℤ
motive : (n : ℤ) → n ≤ m → Sort u_1
base : motive m ⋯
pred : (n : ℤ) → (hnm : n ≤ m) → motive n hnm → motive (n - 1) ⋯
n x✝³ : ℤ
x✝² : m ≤ x✝³
x✝¹ : (hnm : x✝³ ≤ m) → motive x✝³ hnm
x✝ : x✝³ + 1 ≤ m
⊢ False

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Group.Hom.Basic

Goal state before:
pp: M : Type u_2
N : Type u_3
P : Type u_4
inst✝² : Mul M
inst✝¹ : CommSemigroup N
inst✝ : CommSemigroup P
g : N →ₙ* P
f₁ f₂ : M →ₙ* N
⊢ g.comp (f₁ * f₂) = g.comp f₁ * g.comp f₂

Tactic:
ext
  simp

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

Goal state before:
pp: a b c d m✝ n✝ m : ℤ
motive : (n : ℤ) → n ≤ m → Sort u_1
base : motive m ⋯
pred : (n : ℤ) → (hnm : n ≤ m) → motive n hnm → motive (n - 1) ⋯
n : ℤ
hnm : n ≤ m
⊢ n - 1 ≤ m

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Group.Hom.Basic

Goal state before:
pp: M : Type u_2
N : Type u_3
P : Type u_4
inst✝² : MulOneClass M
inst✝¹ : CommMonoid N
inst✝ : CommMonoid P
g : N →* P
f₁ f₂ : M →* N
⊢ g.comp (f₁ * f₂) = g.comp f₁ * g.comp f₂

Tactic:
ext
  simp

Goal state after:
Module: Mathlib.Algebra.Group.Hom.Basic

Goal state before:
pp: M : Type u_2
G : Type u_5
H : Type u_6
inst✝² : MulOneClass M
inst✝¹ : CommGroup G
inst✝ : CommGroup H
φ : G →* H
ψ : M →* G
⊢ φ.comp ψ⁻¹ = (φ.comp ψ)⁻¹

Tactic:
ext
  simp

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

Goal state before:
pp: a b c d m n✝ : ℤ
motive : ℤ → Sort u_1
lt : (n : ℤ) → n < m → motive n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → motive k) → motive n
n : ℤ
hnm : ¬n < m
⊢ n ≥ m

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Group.Hom.Basic

Goal state before:
pp: M : Type u_2
G : Type u_5
H : Type u_6
inst✝² : MulOneClass M
inst✝¹ : CommGroup G
inst✝ : CommGroup H
f : G →* H
g h : M →* G
⊢ f.comp (g / h) = f.comp g / f.comp h

Tactic:
ext
  simp

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

Goal state before:
pp: a b c d m n✝ : ℤ
motive : ℤ → Sort u_1
lt : (n : ℤ) → n < m → motive n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → motive k) → motive n
n : ℤ
hnm : ¬n < m
_n : ℤ
a✝¹ : m ≤ _n
ih : (k : ℤ) → k < _n → motive k
l : ℤ
a✝ : l < _n + 1
hlm : ¬l < m
⊢ l ≥ m

Tactic:
lia

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

Goal state before:
pp: a b c d m n✝ : ℤ
motive : ℤ → Sort u_1
lt : (n : ℤ) → n < m → motive n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → motive k) → motive n
n : ℤ
hnm : ¬n < m
_n : ℤ
a✝¹ : m ≤ _n
ih : (k : ℤ) → k < _n → motive k
l : ℤ
a✝ : l < _n + 1
hlm : ¬l < m
k : ℤ
x✝ : k < l
⊢ k < _n

Tactic:
lia

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

Goal state before:
pp: a b c d m n✝¹ : ℤ
motive : ℤ → Sort u_1
lt : (n : ℤ) → n < m → motive n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → motive k) → motive n
n✝ : ℤ
hnm : ¬n✝ < m
n : ℤ
x✝¹ : n ≤ m
hn : (k : ℤ) → k < n → motive k
l : ℤ
x✝ : l < n - 1
⊢ l < n

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Group.Torsion

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
inst✝ : IsMulTorsionFree M
a : M
⊢ 2 ≠ 0

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Group.Torsion

Goal state before:
pp: G : Type u_2
inst✝¹ : Group G
inst✝ : IsMulTorsionFree G
n : ℤ
a : G
hn : n ≠ 0
⊢ a ^ n = 1 ↔ a = 1

Tactic:
by
  rw [← zpow_left_inj (a := a) hn, one_zpow]

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

Goal state before:
pp: ⊢ ∀ {m n : ℤ}, m.sign = n.sign → (m + n).sign = n.sign

Tactic:
lia

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

Goal state before:
pp: m : ℤ
n : ℕ
hn : n ≠ 0
⊢ m.toNat < n ↔ m < ↑n

Tactic:
lia

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

Goal state before:
pp: m : ℤ
n : ℕ
hn : n ≠ 0
⊢ 0 < ↑n

Tactic:
lia

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a b : G
⊢ a / b = b⁻¹ ↔ a = 1

Tactic:
rw [div_eq_mul_inv, mul_eq_right]

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

Goal state before:
pp: case inr.inl
α : Type u_1
β : Type u_2
inst✝² : Monoid β
p r : α → α → Prop
inst✝¹ : Std.Total r
f : α → α → β
inst✝ : Std.Symm p
hf_swap : ∀ {a b : α}, p a b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a b → p b c → p a c → f a c = f a b * f b c
a b✝ c✝ : α
pab✝ : p a b✝
pbc✝ : p b✝ c✝
pac✝ : p a c✝
b c : α
rbc : r b c
pab : p a b
pbc : p b c
pac : p a c
rba : r b a
rac : r a c
⊢ f a b * (f b a * f a c) = f a b * f b c

Tactic:
rw [hmul rba rac (symm pab) pac pbc]

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

Goal state before:
pp: α : Type u
inst✝ : Monoid α
u₁ u₂ : αˣ
⊢ ↑(u₁ / u₂) = ↑u₁ /ₚ u₂

Tactic:
by
  rw [divp, division_def, Units.val_mul]

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

Goal state before:
pp: α : Type u
M : Type u_1
hM : Monoid M
h : ∀ (a : M), IsUnit a
a : M
⊢ ↑⋯.unit⁻¹ * a = 1

Tactic:
Units.inv_mul_eq_iff_eq_mul,

Goal state after:
α : Type u
M : Type u_1
hM : Monoid M
h : ∀ (a : M), IsUnit a
a : M
⊢ a = ↑⋯.unit * 1
Module: Mathlib.Algebra.Group.Units.Defs

Goal state before:
pp: α : Type u
M : Type u_1
hM : CommMonoid M
h : ∀ (a : M), IsUnit a
a : M
⊢ ↑⋯.unit⁻¹ * a = 1

Tactic:
Units.inv_mul_eq_iff_eq_mul,

Goal state after:
α : Type u
M : Type u_1
hM : CommMonoid M
h : ∀ (a : M), IsUnit a
a : M
⊢ a = ↑⋯.unit * 1
Module: Mathlib.Algebra.Group.Units.Hom

Goal state before:
pp: M : Type u
N : Type v
inst✝¹ : Monoid M
inst✝ : Monoid N
f : M →* N
g : M → Nˣ
h : ∀ (x : M), ↑(g x) = f x
x : M
⊢ ↑((liftRight f g h) x)⁻¹ * f x = 1

Tactic:
Units.inv_mul_eq_iff_eq_mul,

Goal state after:
M : Type u
N : Type v
inst✝¹ : Monoid M
inst✝ : Monoid N
f : M →* N
g : M → Nˣ
h : ∀ (x : M), ↑(g x) = f x
x : M
⊢ f x = ↑((liftRight f g h) x) * 1