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

Goal state before:
pp: motive : Nat → Sort u
zero : motive 0
one : motive 1
bit : (b : Bool) → (n : Nat) → n ≠ 0 → motive n → motive (Nat.bit b n)
b : Bool
n : Nat
h : n = 0 → b = true
ih : motive n
h' : n = 0
⊢ Nat.bit b n = Nat.bit true 0

Tactic:
rw [h', h h']

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

Goal state before:
pp: M : Type u
inst✝¹ : One M
inst✝ : Semigroup M
n : ℕ
hn : n ≠ 0
a : M
ha : 1 * a = a
⊢ npowRec (n + 1) a = a * npowRec n a

Tactic:
rw [Nat.add_comm, npowRec_add 1 n hn a ha, npowRec, npowRec, ha]

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
⊢ go (k + 1) m n = m * npowRec' (k + 1) n

Tactic:
by
  unfold go
  generalize hk : k + 1 = k'
  replace hk : k' ≠ 0 := by lia
  induction k' using Nat.binaryRecFromOne generalizing n m with
  | zero => simp at hk
  | one => simp [npowRec']
  | bit b k' k'0 ih =>
    rw [Nat.binaryRec_eq _ _ (Or.inl rfl), ih _ _ k'0]
    cases b <;> simp only [Nat.bit, cond_false, cond_true, npowRec'_two_mul]
    rw [npowRec'_succ (by lia), npowRec'_two_mul, ← npowRec'_two_mul,
      ← npowRec'_mul_comm (by lia), mul_assoc]

Goal state after:
Module: Mathlib.Logic.ExistsUnique

Goal state before:
pp: α : Sort u_1
p : α → Sort u_2
inst✝ : ∀ (x : α), Subsingleton (p x)
q : (x : α) → p x → Prop
b : Prop
h₂ : ∃! x, ∃! h, q x h
h₁ : ∀ (x : α) (h : p x), q x h → (∀ (y : α) (hy : p y), q y hy → y = x) → b
⊢ b

Tactic:
by
  simp only [existsUnique_iff_exists] at h₂
  apply h₂.elim
  exact fun x ⟨hxp, hxq⟩ H ↦ h₁ x hxp hxq fun y hyp hyq ↦ H y ⟨hyp, hyq⟩

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_3
p : α → Prop
b : Prop
ha : Nonempty α
⊢ (∀ (x : α), p x) → b ↔ ∃ x, p x → b

Tactic:
let ⟨a⟩ := ha
  refine ⟨fun h ↦ not_forall_not.1 fun h' ↦ ?_, fun ⟨x, hx⟩ h ↦ hx (h x)⟩
  exact if hb : b then h' a fun _ ↦ hb else hb <| h fun x ↦ (Classical.not_imp.1 (h' x)).1

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

Goal state before:
pp: case pos
γ : Sort u_3
α₁ : Sort u_4
α₂ : Sort u_5
α₃ : Sort u_6
f₁₂ : α₁ → α₂
h₁₂ : Injective f₁₂
f₂₃ : α₂ → α₃
h₂₃ : Injective f₂₃
g : α₁ → γ
e' : α₃ → γ
c : α₁
⊢ extend (f₂₃ ∘ f₁₂) g e' (f₂₃ (f₁₂ c)) = extend f₁₂ g (e' ∘ f₂₃) (f₁₂ c)

Tactic:
rw [h₁₂.extend_apply]

Goal state after:
case pos
γ : Sort u_3
α₁ : Sort u_4
α₂ : Sort u_5
α₃ : Sort u_6
f₁₂ : α₁ → α₂
h₁₂ : Injective f₁₂
f₂₃ : α₂ → α₃
h₂₃ : Injective f₂₃
g : α₁ → γ
e' : α₃ → γ
c : α₁
⊢ extend (f₂₃ ∘ f₁₂) g e' (f₂₃ (f₁₂ c)) = g c
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u
f : α → α
h : Involutive f
g : α → α
hg : LeftInverse g f
x : α
⊢ g (f (f x)) = f (f (f x))

Tactic:
hg,

Goal state after:
α : Sort u
f : α → α
h : Involutive f
g : α → α
hg : LeftInverse g f
x : α
⊢ f x = f (f (f x))
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a c : α
⊢ TransGen r a c ↔ ∃ b, ReflTransGen r a b ∧ r b c

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨b, hab, hbc⟩ ↦ tail' hab hbc⟩
  cases h with
  | single hac => exact ⟨_, by rfl, hac⟩
  | tail hab hbc => exact ⟨_, hab.to_reflTransGen, hbc⟩

Goal state after:
Module: Mathlib.Logic.Function.Iterate

Goal state before:
pp: α : Type u
f g : α → α
hg : LeftInverse g f
n✝ n : ℕ
ihn : LeftInverse g^[n] f^[n]
⊢ LeftInverse g^[n.succ] f^[n.succ]

Tactic:
rw [iterate_succ', iterate_succ]

Goal state after:
α : Type u
f g : α → α
hg : LeftInverse g f
n✝ n : ℕ
ihn : LeftInverse g^[n] f^[n]
⊢ LeftInverse (g ∘ g^[n]) (f^[n] ∘ f)
Module: Mathlib.Algebra.Group.Action.Faithful

Goal state before:
pp: R : Type u_4
S : Type u_5
T : Type u_6
inst✝⁸ : Monoid S
inst✝⁷ : MulOneClass T
inst✝⁶ : SMul R S
inst✝⁵ : SMul R T
inst✝⁴ : MulAction S T
inst✝³ : IsScalarTower R S S
inst✝² : IsScalarTower R T T
inst✝¹ : IsScalarTower R S T
inst✝ : FaithfulSMul R T
⊢ Injective fun r ↦ r • 1

Tactic:
refine .of_comp (f := (· • (1 : T))) ?_

Goal state after:
R : Type u_4
S : Type u_5
T : Type u_6
inst✝⁸ : Monoid S
inst✝⁷ : MulOneClass T
inst✝⁶ : SMul R S
inst✝⁵ : SMul R T
inst✝⁴ : MulAction S T
inst✝³ : IsScalarTower R S S
inst✝² : IsScalarTower R T T
inst✝¹ : IsScalarTower R S T
inst✝ : FaithfulSMul R T
⊢ Injective ((fun x ↦ x • 1) ∘ fun r ↦ r • 1)
Module: Mathlib.Logic.IsEmpty.Basic

Goal state before:
pp: α : Sort u_5
E : α → Sort u_4
⊢ IsEmpty (PSigma E) ↔ ∀ (a : α), IsEmpty (E a)

Tactic:
by
  simp only [← not_nonempty_iff, nonempty_psigma, not_exists]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a ≤ b
⊢ a ≤ a

Tactic:
simp [h, le_of_not_ge]

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : ¬a ≤ b
⊢ b ≤ a

Tactic:
simp [h, le_of_not_ge]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : PartialOrder α
⊢ ∀ (a b : OrderBot α), a = b

Tactic:
rintro @⟨⟨a⟩, ha⟩ @⟨⟨b⟩, hb⟩; congr; exact le_antisymm (ha _) (hb _)

Goal state after:
Module: Mathlib.Order.PropInstances

Goal state before:
pp: P Q : Prop
⊢ ¬(P ∧ Q) ∧ (P ∨ Q) ↔ ¬(P ↔ Q)

Tactic:
not_iff

Goal state after:
P Q : Prop
⊢ ¬(P ∧ Q) ∧ (P ∨ Q) ↔ (¬P ↔ Q)
Module: Mathlib.Data.Set.Basic

Goal state before:
pp: α : Type u
s : Set α
⊢ (∀ (x : α), ¬x ∈ s) ↔ s = ∅

Tactic:
eq_empty_iff_forall_notMem

Goal state after:
α : Type u
s : Set α
⊢ (∀ (x : α), ¬x ∈ s) ↔ ∀ (x : α), ¬x ∈ s
Module: Mathlib.Data.Set.Insert

Goal state before:
pp: α : Type u_1
s : Set α
x : α
⊢ s = ∅ → s ≠ {x}

Tactic:
exact fun h => h ▸ empty_ne_singleton _

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
inst✝ : DistribLattice α
x y z : α
⊢ x ⊓ (y ⊔ z) ≤ x ⊓ y ⊔ x ⊓ z

Tactic:
rw [inf_sup_left]

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

Goal state before:
pp: α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ (y ⊓ x ⊔ y \ x) ⊓ x \ y = (x ⊓ (y ⊓ x) ⊔ x ⊓ y \ x) ⊓ x \ y

Tactic:
rw [inf_sup_left]

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

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ y \ z ⊓ (z ⊓ x ⊔ x \ y) = x ⊓ y \ z ⊓ (z ⊓ x) ⊔ x ⊓ y \ z ⊓ x \ y

Tactic:
rw [inf_sup_left]

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a : α
⊢ a ∆ a = ⊥

Tactic:
by rw [symmDiff, sup_idem, sdiff_self]

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
a b : α
⊢ a ⊓ b = ⊥ ∧ a ⊔ b = ⊤ ↔ a ⊓ b = ⊥ ∧ Codisjoint a b

Tactic:
codisjoint_iff

Goal state after:
α : Type u_2
inst✝ : BooleanAlgebra α
a b : α
⊢ a ⊓ b = ⊥ ∧ a ⊔ b = ⊤ ↔ a ⊓ b = ⊥ ∧ a ⊔ b = ⊤
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t : Set β
⊢ (s₁ ∪ s₂) ×ˢ t = s₁ ×ˢ t ∪ s₂ ×ˢ t

Tactic:
by
  ext ⟨x, y⟩
  simp [or_and_right]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s t : Set α
⊢ f '' Subtype.val '' Subtype.val ⁻¹' t = f '' (t ∩ s)

Tactic:
image_preimage_eq_inter_range,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s t : Set α
⊢ f '' (t ∩ range Subtype.val) = f '' (t ∩ s)
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s : Set α
t : Set β
f f' : α → γ
g g' : β → δ
h : EqOn (Prod.map f g) (Prod.map f' g') (s ×ˢ t)
x : β
hxt : x ∈ t
⊢ EqOn f f' s

Tactic:
intro x hxs

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s : Set α
t : Set β
f f' : α → γ
g g' : β → δ
h : EqOn (Prod.map f g) (Prod.map f' g') (s ×ˢ t)
x✝ : β
hxt : x✝ ∈ t
x : α
hxs : x ∈ s
⊢ f x = f' x
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
s : Set α
⊢ (Prod.map (fun x ↦ ↑x) fun x ↦ ↑x) ⁻¹' diagonal α = diagonal ↑s

Tactic:
ext ⟨⟨x, hx⟩, ⟨y, hy⟩⟩
  simp [Set.diagonal]

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

Goal state before:
pp: α : Type u_5
β : Type u_6
γ : Type u_7
γ' : Type u_8
δ : Type u_9
δ' : Type u_10
h : β → α
f : γ → β
f₁ : γ' → α
f₂ : γ → γ'
g : δ → β
g₁ : δ' → α
g₂ : δ → δ'
hf : h ∘ f = f₁ ∘ f₂
hg : h ∘ g = g₁ ∘ g₂
hfg : range f ∪ range g = univ
s : Set β
⊢ h '' s = h '' f '' f ⁻¹' s ∪ h '' g '' g ⁻¹' s

Tactic:
image_preimage_eq_inter_range,

Goal state after:
α : Type u_5
β : Type u_6
γ : Type u_7
γ' : Type u_8
δ : Type u_9
δ' : Type u_10
h : β → α
f : γ → β
f₁ : γ' → α
f₂ : γ → γ'
g : δ → β
g₁ : δ' → α
g₂ : δ → δ'
hf : h ∘ f = f₁ ∘ f₂
hg : h ∘ g = g₁ ∘ g₂
hfg : range f ∪ range g = univ
s : Set β
⊢ h '' s = h '' (s ∩ range f) ∪ h '' g '' g ⁻¹' s
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_5
β : Type u_6
γ : Type u_7
γ' : Type u_8
δ : Type u_9
δ' : Type u_10
h : β → α
f : γ → β
f₁ : γ' → α
f₂ : γ → γ'
g : δ → β
g₁ : δ' → α
g₂ : δ → δ'
hf : h ∘ f = f₁ ∘ f₂
hg : h ∘ g = g₁ ∘ g₂
hfg : range f ∪ range g = univ
s : Set β
⊢ h '' s = h '' (s ∩ range f) ∪ h '' g '' g ⁻¹' s

Tactic:
image_preimage_eq_inter_range,

Goal state after:
α : Type u_5
β : Type u_6
γ : Type u_7
γ' : Type u_8
δ : Type u_9
δ' : Type u_10
h : β → α
f : γ → β
f₁ : γ' → α
f₂ : γ → γ'
g : δ → β
g₁ : δ' → α
g₂ : δ → δ'
hf : h ∘ f = f₁ ∘ f₂
hg : h ∘ g = g₁ ∘ g₂
hfg : range f ∪ range g = univ
s : Set β
⊢ h '' s = h '' (s ∩ range f) ∪ h '' (s ∩ range g)
Module: Mathlib.Algebra.Group.Hom.Defs

Goal state before:
pp: ι : Type u_1
G : Type u_7
H : Type u_8
F : Type u_9
inst✝³ : FunLike F G H
inst✝² : DivInvMonoid G
inst✝¹ : DivInvMonoid H
inst✝ : MulHomClass F G H
f : F
hf : ∀ (a : G), f a⁻¹ = (f a)⁻¹
g h : ι → G
⊢ ⇑f ∘ (g / h) = ⇑f ∘ g / ⇑f ∘ h

Tactic:
ext; simp [map_div' f hf]

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
a : M
n : ℕ
⊢ (fun x ↦ a * x)^[n + 1] = fun x ↦ a ^ (n + 1) * x

Tactic:
simp [pow_succ, mul_left_iterate]

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a b : G
n : ℕ
⊢ (a * b) ^ Int.negSucc n * a = a * (b * a) ^ Int.negSucc n

Tactic:
simp [inv_mul_eq_iff_eq_mul, eq_mul_inv_iff_mul_eq, mul_assoc, mul_pow_mul]

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

Goal state before:

Tactic:
x = 1 * x := by rw [one_mul]
    _ = 0 := by rw [h, zero_mul]
    _ = 1 * y := by rw [h, zero_mul]
    _ = y := by rw [one_mul]

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

Goal state before:
pp: α : Type u_4
inst✝ : DecidableEq α
f : Perm α
x y z : α
⊢ (swap x y * f) z = (f * swap (f⁻¹ x) (f⁻¹ y)) z

Tactic:
simp only [Perm.mul_apply, swap_apply_def]; split_ifs <;> simp_all [eq_symm_apply]

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

Goal state before:
pp: α : Type u_4
inst✝ : DecidableEq α
x y z : α
hxy : x ≠ y
hxz : x ≠ z
⊢ swap y z * swap x y * (swap y z)⁻¹ = swap z x

Tactic:
rw [← swap_apply_apply, swap_apply_left, swap_apply_of_ne_of_ne hxy hxz, swap_comm]

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

Goal state before:
pp: x : ℤ
x✝ : ∃ n, n * n = x
n : ℤ
hn : n * n = x
⊢ sqrt (n * n) * sqrt (n * n) = n * n

Tactic:
sqrt_eq,

Goal state after:
x : ℤ
x✝ : ∃ n, n * n = x
n : ℤ
hn : n * n = x
⊢ ↑n.natAbs * ↑n.natAbs = n * n
Module: Mathlib.Algebra.Group.Nat.Hom

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
f g : Multiplicative ℕ →* M
h : f (ofAdd 1) = g (ofAdd 1)
n : Multiplicative ℕ
⊢ f n = g n

Tactic:
rw [f.apply_mnat, g.apply_mnat, h]

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

Goal state before:
pp: α : Type u_3
inst✝¹ : Nontrivial α
inst✝ : LinearOrder α
⊢ ∃ x y, x < y

Tactic:
rcases exists_pair_ne α with ⟨x, y, hxy⟩
  cases lt_or_gt_of_ne hxy <;> exact ⟨_, _, ‹_›⟩

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

Goal state before:
pp: α : Type u_1
p : α → Prop
x : Subtype p
⊢ Nontrivial (Subtype p) ↔ ∃ y x_1, y ≠ x.val

Tactic:
simp only [_root_.nontrivial_iff_exists_ne x, Subtype.exists, Ne, Subtype.ext_iff]

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
x y : Mˣ
h : SemiconjBy a ↑x ↑y
n : ℕ
⊢ SemiconjBy a ↑(x ^ -[n+1]) ↑(y ^ -[n+1])

Tactic:
by simp only [zpow_negSucc, Units.val_pow_eq_pow_val, units_inv_right, h, pow_right]

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

Goal state before:
pp: α : Type u
inst✝ : Semiring α
a b : α
u : αˣ
⊢ a /ₚ u + b /ₚ u = (a + b) /ₚ u

Tactic:
by
  simp only [divp, add_mul]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
f✝ : S → R
hf✝ : Injective f✝
inst✝¹¹ : Add S
inst✝¹⁰ : Mul S
inst✝⁹ : Zero S
inst✝⁸ : One S
inst✝⁷ : Neg S
inst✝⁶ : Sub S
inst✝⁵ : SMul ℕ S
inst✝⁴ : SMul ℤ S
inst✝³ : Pow S ℕ
inst✝² : NatCast S
inst✝¹ : IntCast S
inst✝ : AddMonoidWithOne R
f : S → R
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
nsmul : ∀ (n : ℕ) (x : S), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f ↑n = ↑n
n : ℕ
⊢ ↑n + 1 = f (↑n + 1)

Tactic:
add,

Goal state after:
R : Type u_1
S : Type u_2
f✝ : S → R
hf✝ : Injective f✝
inst✝¹¹ : Add S
inst✝¹⁰ : Mul S
inst✝⁹ : Zero S
inst✝⁸ : One S
inst✝⁷ : Neg S
inst✝⁶ : Sub S
inst✝⁵ : SMul ℕ S
inst✝⁴ : SMul ℤ S
inst✝³ : Pow S ℕ
inst✝² : NatCast S
inst✝¹ : IntCast S
inst✝ : AddMonoidWithOne R
f : S → R
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
nsmul : ∀ (n : ℕ) (x : S), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f ↑n = ↑n
n : ℕ
⊢ ↑n + 1 = f ↑n + f 1
Module: Mathlib.Algebra.Ring.InjSurj

Goal state before:
pp: R : Type u_1
S : Type u_2
f : R → S
hf : Surjective f
inst✝¹¹ : Add S
inst✝¹⁰ : Mul S
inst✝⁹ : Zero S
inst✝⁸ : One S
inst✝⁷ : Neg S
inst✝⁶ : Sub S
inst✝⁵ : SMul ℕ S
inst✝⁴ : SMul ℤ S
inst✝³ : Pow S ℕ
inst✝² : NatCast S
inst✝¹ : IntCast S
inst✝ : AddMonoidWithOne R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : R), f (x + y) = f x + f y
nsmul : ∀ (n : ℕ) (x : R), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f ↑n = ↑n
n : ℕ
⊢ f (↑n + 1) = ↑n + 1

Tactic:
add,

Goal state after:
R : Type u_1
S : Type u_2
f : R → S
hf : Surjective f
inst✝¹¹ : Add S
inst✝¹⁰ : Mul S
inst✝⁹ : Zero S
inst✝⁸ : One S
inst✝⁷ : Neg S
inst✝⁶ : Sub S
inst✝⁵ : SMul ℕ S
inst✝⁴ : SMul ℤ S
inst✝³ : Pow S ℕ
inst✝² : NatCast S
inst✝¹ : IntCast S
inst✝ : AddMonoidWithOne R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : R), f (x + y) = f x + f y
nsmul : ∀ (n : ℕ) (x : R), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f ↑n = ↑n
n : ℕ
⊢ f ↑n + f 1 = ↑n + 1
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Semiring α
inst✝² : Semiring β
inst✝¹ : FunLike F α β
inst✝ : RingHomClass F α β
f : F
a : α
⊢ Odd (f (2 * a + 1))

Tactic:
exact ⟨f a, by simp [two_mul]⟩

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

Goal state before:
pp: α : Type u_2
inst✝ : Ring α
a b : α
ha : Even a
hb : Odd b
⊢ Odd (a - b)

Tactic:
rw [sub_eq_add_neg]; exact ha.add_odd hb.neg

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

Goal state before:
pp: α : Type u_2
inst✝ : Ring α
a b : α
ha : Odd a
hb : Odd b
⊢ Even (a - b)

Tactic:
rw [sub_eq_add_neg]; exact ha.add_odd hb.neg

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

Goal state before:
pp: M₀ : Type u_2
inst✝³ : MonoidWithZero M₀
inst✝² : Preorder M₀
a : M₀
inst✝¹ : ZeroLEOneClass M₀
inst✝ : PosMulMono M₀
h : 1 ≤ a
n : ℕ
⊢ a ^ n ≤ a ^ n * a

Tactic:
exact le_mul_of_one_le_right (pow_nonneg (zero_le_one.trans h) _) h

Goal state after:
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 + b + b * c ≤ c
⊢ 1 + (a + (b + b * c)) ≤ 1 + c

Tactic:
← add_assoc a

Goal state after:
R : Type u
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b c : R
h : a + b + b * c ≤ c
⊢ 1 + (a + b + b * c) ≤ 1 + 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 : a + c + b * c ≤ b
⊢ 1 + (a + (c + b * c)) ≤ 1 + b

Tactic:
← add_assoc a

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 + c + b * c) ≤ 1 + b
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : LinearOrder R
a b : R
inst✝³ : NoZeroDivisors R
inst✝² : ExistsAddOfLE R
inst✝¹ : PosMulMono R
inst✝ : AddLeftMono R
⊢ a * a + b * b = 0 ↔ a = 0 ∧ b = 0

Tactic:
add_eq_zero_iff_of_nonneg,

Goal state after:
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : LinearOrder R
a b : R
inst✝³ : NoZeroDivisors R
inst✝² : ExistsAddOfLE R
inst✝¹ : PosMulMono R
inst✝ : AddLeftMono R
⊢ a * a = 0 ∧ b * b = 0 ↔ a = 0 ∧ b = 0

case ha
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : LinearOrder R
a b : R
inst✝³ : NoZeroDivisors R
inst✝² : ExistsAddOfLE R
inst✝¹ : PosMulMono R
inst✝ : AddLeftMono R
⊢ 0 ≤ a * a

case hb
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : LinearOrder R
a b : R
inst✝³ : NoZeroDivisors R
inst✝² : ExistsAddOfLE R
inst✝¹ : PosMulMono R
inst✝ : AddLeftMono R
⊢ 0 ≤ b * 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 : G₀
hc : 0 < c
⊢ a < c⁻¹ * b ↔ a * c < b

Tactic:
lt_inv_mul_iff₀ hc,

Goal state after:
G₀ : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ c * a < b ↔ a * c < b
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
f : α ↪o β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
a₁ a₂ : α
h : Disjoint (f a₁) (f a₂)
x : α
h₁ : f x ≤ f a₁
h₂ : f x ≤ f a₂
⊢ f x ≤ f ⊥

Tactic:
calc
    f x ≤ ⊥ := h h₁ h₂
    _ ≤ f ⊥ := bot_le

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : LE α
inst✝² : LE β
inst✝¹ : LE γ
inst✝ : LE δ
e : α ≃ β
map_rel_iff' : ∀ {a b : α}, e a ≤ e b ↔ a ≤ b
⊢ ∀ {a b : β}, e.symm a ≤ e.symm b ↔ a ≤ b

Tactic:
by simp [← map_rel_iff']

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

Goal state before:
pp: X : Type u_6
Y : Type u_7
F : Type u_8
inst✝³ : Preorder X
inst✝² : Preorder Y
inst✝¹ : EquivLike F X Y
inst✝ : OrderIsoClass F X Y
f : F
⊢ DenselyOrdered X ↔ DenselyOrdered Y

Tactic:
by
  constructor
  · intro H
    refine ⟨fun a b h ↦ ?_⟩
    obtain ⟨c, hc⟩ := exists_between ((map_inv_lt_map_inv_iff f).mpr h)
    exact ⟨f c, by simpa using hc⟩
  · intro H
    refine ⟨fun a b h ↦ ?_⟩
    obtain ⟨c, hc⟩ := exists_between ((map_lt_map_iff f).mpr h)
    exact ⟨EquivLike.inv f c, by simpa using hc⟩

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_self_eq_natAbs]

Goal state after:
Module: Mathlib.Data.Nat.Cast.Order.Basic

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : AddLeftMono α
inst✝¹ : ZeroLEOneClass α
inst✝ : NeZero 1
n : ℕ
⊢ 1 ≤ ↑n + 1

Tactic:
convert! (@mono_cast α _).imp (?_ : 1 ≤ n + 1)

Goal state after:
case e'_3
α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : AddLeftMono α
inst✝¹ : ZeroLEOneClass α
inst✝ : NeZero 1
n : ℕ
⊢ 1 = ↑1

case e'_4
α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : AddLeftMono α
inst✝¹ : ZeroLEOneClass α
inst✝ : NeZero 1
n : ℕ
⊢ ↑n + 1 = ↑(n + 1)

α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : AddLeftMono α
inst✝¹ : ZeroLEOneClass α
inst✝ : NeZero 1
n : ℕ
⊢ 1 ≤ n + 1
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: m n : ℕ
⊢ ↑((↑m).gcd -[n+1]) = ↑m * (↑m).gcdA -[n+1] + (↑n + 1) * (↑m).natAbs.gcdB n.succ

Tactic:
apply Nat.gcd_eq_gcd_ab

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

Goal state before:
pp: m n : ℕ
⊢ ↑(-[m+1].gcd ↑n) = (↑m + 1) * m.succ.gcdA (↑n).natAbs + ↑n * -[m+1].gcdB ↑n

Tactic:
apply Nat.gcd_eq_gcd_ab

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

Goal state before:
pp: m n : ℕ
⊢ ↑(-[m+1].gcd -[n+1]) = (↑m + 1) * m.succ.gcdA -[n+1].natAbs + (↑n + 1) * -[m+1].natAbs.gcdB n.succ

Tactic:
apply Nat.gcd_eq_gcd_ab

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a : α
ha : a ≠ ⊤
⊢ -a + a = 0

Tactic:
simp [add_comm, add_neg_cancel_of_ne_top ha]

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

Goal state before:
pp: α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hab : AddLECancellable (a - b)
h₁ : b ≤ a
h₂ : c ≤ a
h₃ : a - b = a - c
⊢ b = c

Tactic:
rw [← hab.inj]

Goal state after:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hab : AddLECancellable (a - b)
h₁ : b ≤ a
h₂ : c ≤ a
h₃ : a - b = a - c
⊢ a - b + b = a - b + c
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u_1
inst✝³ : Add α
inst✝² : LE α
inst✝¹ : AddRightMono α
inst✝ : AddRightReflectLE α
a b c : WithBot (WithTop α)
hc : c ≠ ⊥
hc' : c ≠ ⊤
⊢ a + c ≤ b + c ↔ a ≤ b

Tactic:
induction a <;> induction b <;> induction c

Goal state after:
case bot.bot.bot
α : Type u_1
inst✝³ : Add α
inst✝² : LE α
inst✝¹ : AddRightMono α
inst✝ : AddRightReflectLE α
hc : ⊥ ≠ ⊥
hc' : ⊥ ≠ ⊤
⊢ ⊥ + ⊥ ≤ ⊥ + ⊥ ↔ ⊥ ≤ ⊥

case bot.bot.coe
α : Type u_1
inst✝³ : Add α
inst✝² : LE α
inst✝¹ : AddRightMono α
inst✝ : AddRightReflectLE α
a✝ : WithTop α
hc : ↑a✝ ≠ ⊥
hc' : ↑a✝ ≠ ⊤
⊢ ⊥ + ↑a✝ ≤ ⊥ + ↑a✝ ↔ ⊥ ≤ ⊥

case bot.coe.bot
α : Type u_1
inst✝³ : Add α
inst✝² : LE α
inst✝¹ : AddRightMono α
inst✝ : AddRightReflectLE α
a✝ : WithTop α
hc : ⊥ ≠ ⊥
hc' : ⊥ ≠ ⊤
⊢ ⊥ + ⊥ ≤ ↑a✝ + ⊥ ↔ ⊥ ≤ ↑a✝

case bot.coe.coe
α : Type u_1
inst✝³ : Add α
inst✝² : LE α
inst✝¹ : AddRightMono α
inst✝ : AddRightReflectLE α
a✝¹ a✝ : WithTop α
hc : ↑a✝ ≠ ⊥
hc' : ↑a✝ ≠ ⊤
⊢ ⊥ + ↑a✝ ≤ ↑a✝¹ + ↑a✝ ↔ ⊥ ≤ ↑a✝¹

case coe.bot.bot
α : Type u_1
inst✝³ : Add α
inst✝² : LE α
inst✝¹ : AddRightMono α
inst✝ : AddRightReflectLE α
a✝ : WithTop α
hc : ⊥ ≠ ⊥
hc' : ⊥ ≠ ⊤
⊢ ↑a✝ + ⊥ ≤ ⊥ + ⊥ ↔ ↑a✝ ≤ ⊥

case coe.bot.coe
α : Type u_1
inst✝³ : Add α
inst✝² : LE α
inst✝¹ : AddRightMono α
inst✝ : AddRightReflectLE α
a✝¹ a✝ : WithTop α
hc : ↑a✝ ≠ ⊥
hc' : ↑a✝ ≠ ⊤
⊢ ↑a✝¹ + ↑a✝ ≤ ⊥ + ↑a✝ ↔ ↑a✝¹ ≤ ⊥

case coe.coe.bot
α : Type u_1
inst✝³ : Add α
inst✝² : LE α
inst✝¹ : AddRightMono α
inst✝ : AddRightReflectLE α
a✝¹ a✝ : WithTop α
hc : ⊥ ≠ ⊥
hc' : ⊥ ≠ ⊤
⊢ ↑a✝¹ + ⊥ ≤ ↑a✝ + ⊥ ↔ ↑a✝¹ ≤ ↑a✝

case coe.coe.coe
α : Type u_1
inst✝³ : Add α
inst✝² : LE α
inst✝¹ : AddRightMono α
inst✝ : AddRightReflectLE α
a✝² a✝¹ a✝ : WithTop α
hc : ↑a✝ ≠ ⊥
hc' : ↑a✝ ≠ ⊤
⊢ ↑a✝² + ↑a✝ ≤ ↑a✝¹ + ↑a✝ ↔ ↑a✝² ≤ ↑a✝¹
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: case inr
R : Type u_3
inst✝¹ : Semiring R
inst✝ : LinearOrder R
H₁ H₂ : FloorSemiring R
this : FloorSemiring.ceil = FloorSemiring.ceil
a : R
h : 0 ≤ a
⊢ FloorSemiring.floor a = FloorSemiring.floor a

Tactic:
refine eq_of_forall_le_iff fun n => ?_
      rw [H₁.gc_floor, H₂.gc_floor] <;> exact h

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : LE α
x : WithBot α
y : WithTop αᵒᵈ
⊢ WithBot.toDual x ≤ y ↔ WithTop.ofDual y ≤ x

Tactic:
cases x <;> cases y <;> simp [toDual_le]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : LE α
x : WithBot αᵒᵈ
y : WithTop α
⊢ WithBot.ofDual x ≤ y ↔ WithTop.toDual y ≤ x

Tactic:
cases x <;> cases y <;> simp [toDual_le]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → a ≤ x
⊢ StrictMonoOn f (insert a s) ↔ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s

Tactic:
by
  rw [strictMonoOn_insert_iff]
  have : ∀ b ∈ s, b < a → f b < f a := by
    intro b hb hab
    cases (ha _ hb).not_gt hab
  tauto

Goal state after: