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)
⊢ binaryRec' zero
      (fun b n h ih ↦
        if h' : n = 0 then
          have this := ⋯;
          ⋯ ▸ one
        else bit b n h' ih)
      1 =
    one

Tactic:
binaryRec'_one,

Goal state after:
motive : Nat → Sort u
zero : motive 0
one : motive 1
bit : (b : Bool) → (n : Nat) → n ≠ 0 → motive n → motive (Nat.bit b n)
⊢ (if h' : 0 = 0 then
      have this := ⋯;
      ⋯ ▸ one
    else bit true 0 h' zero) =
    one
Module: Mathlib.Order.Defs.Unbundled

Goal state before:
pp: α : Sort u_1
r : α → α → Prop
a✝ b✝ c : α
inst✝¹ : DecidableRel r
inst✝ : Antisymm r
a b : α
h₁ : Decidable.decide (r a b) = true
h₂ : Decidable.decide (r b a) = true
⊢ r a b

Tactic:
simpa using h₁

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a b : G
⊢ a / b * b = a

Tactic:
rw [div_eq_mul_inv, inv_mul_cancel_right a b]

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ζ : Type u_6
r : α → α → Prop
a b c : α
inst✝ : Std.Symm r
x y : α
h : ReflTransGen r x y
⊢ ReflTransGen r y x

Tactic:
by
    induction h with
    | refl => rfl
    | tail _ b c => apply c.head <| symm b

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case single
α : Type u_1
r : α → α → Prop
a c : α
hac : r a c
⊢ ∃ b, ReflTransGen r a b ∧ r b c

Tactic:
exact ⟨_, by rfl, hac⟩

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

Goal state before:
pp: α : Sort u
β : Sort v
γ : Sort w
e₁ e₂ : α ≃ β
h₁ : e₁.toFun = e₂.toFun
h₂ : e₁.invFun = e₂.invFun
⊢ e₁ = e₂

Tactic:
cases e₁; cases e₂; congr

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

Goal state before:
pp: case inr
α : Type u
f : α → α
m n : ℕ
a : α
hf : Injective f
ha : f^[m] a = f^[n] a
h : n ≤ m
⊢ f^[m - n] a = a

Tactic:
{ exact iterate_cancel_of_add hf (by rwa [Nat.sub_add_cancel h]) }

Goal state after:
Module: Mathlib.Algebra.Group.Action.Faithful

Goal state before:
pp: G : Type u_2
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
⊢ FaithfulSMul G α ↔ ∀ (g : G), (∀ (a : α), g • a = a) → g = 1

Tactic:
by
  refine ⟨fun h a ha ↦ h.eq_of_smul_eq_smul ?_, fun h ↦ ⟨fun {a₁ a₂} h' ↦ ?_⟩⟩
  · simpa only [one_smul]
  · rw [← inv_inv a₂, eq_inv_of_mul_eq_one_left (h (a₂⁻¹ * a₁) ?_), inv_inv]
    simpa only [mul_smul, inv_smul_eq_iff] using h'

Goal state after:
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
⊢ FaithfulSMul R S

Tactic:
faithfulSMul_iff_injective_smul_one

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 r ↦ r • 1
Module: Mathlib.Logic.IsEmpty.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_2
⊢ IsEmpty (α → β) ↔ ¬IsEmpty α ∧ IsEmpty β

Tactic:
isEmpty_fun,

Goal state after:
α : Sort u_1
β : Sort u_2
⊢ Nonempty α ∧ IsEmpty β ↔ ¬IsEmpty α ∧ IsEmpty β
Module: Mathlib.Order.Basic

Goal state before:
pp: ι : Type u_1
π : ι → Type u_4
inst✝ : (i : ι) → Preorder (π i)
x y : (i : ι) → π i
⊢ x < y ↔ x ≤ y ∧ ∃ i, x i < y i

Tactic:
by
  simp +contextual [lt_iff_le_not_ge, Pi.le_def]

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
x y : α × β
h₁ : x.fst < y.fst
h₂ : x.snd ≤ y.snd
⊢ x < y

Tactic:
by simp [lt_iff, *]

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
x y : α × β
h₁ : x.fst ≤ y.fst
h₂ : x.snd < y.snd
⊢ x < y

Tactic:
by simp [lt_iff, *]

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

Goal state before:
pp: n m : Nat
h : n ≤ m
x✝ : Decidable (n = 0)
⊢ (!decide (n = 0)) ≤ !decide (m = 0)

Tactic:
cases Nat.decEq n 0 with

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

Goal state before:
pp: α : Type u
ι : Sort u_1
f : ι → α
⊢ Function.Injective (rangeFactorization f) ↔ Function.Injective f

Tactic:
by
  simp [Function.Injective, rangeFactorization]

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α✝ : Type u
β : Type v
α : Type u_1
inst✝¹ : Max α
inst✝ : Min α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
sup_inf_self : ∀ (a b : α), a ⊔ a ⊓ b = a
inf_sup_self : ∀ (a b : α), a ⊓ (a ⊔ b) = a
sup_idem : ∀ (b : α), b ⊔ b = b
inf_idem : ∀ (b : α), b ⊓ b = b
semilatt_inf_inst : SemilatticeInf α := SemilatticeInf.mk' inf_comm inf_assoc inf_idem
semilatt_sup_inst : SemilatticeSup α := SemilatticeSup.mk' sup_comm sup_assoc sup_idem
partial_order_eq : semilatt_sup_inst.toPartialOrder = semilatt_inf_inst.toPartialOrder
a b : α
⊢ SemilatticeInf.inf a b ≤ b

Tactic:
apply inf_le_right

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α✝ : Type u
β : Type v
α : Type u_1
inst✝¹ : Max α
inst✝ : Min α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
sup_inf_self : ∀ (a b : α), a ⊔ a ⊓ b = a
inf_sup_self : ∀ (a b : α), a ⊓ (a ⊔ b) = a
sup_idem : ∀ (b : α), b ⊔ b = b
inf_idem : ∀ (b : α), b ⊓ b = b
semilatt_inf_inst : SemilatticeInf α := SemilatticeInf.mk' inf_comm inf_assoc inf_idem
semilatt_sup_inst : SemilatticeSup α := SemilatticeSup.mk' sup_comm sup_assoc sup_idem
partial_order_eq : semilatt_sup_inst.toPartialOrder = semilatt_inf_inst.toPartialOrder
a b : α
⊢ SemilatticeInf.inf a b ≤ b

Tactic:
by
      rw [partial_order_eq]
      apply inf_le_right

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

Goal state before:
pp: α : Type u
s : Set α
⊢ ¬s.Subsingleton ↔ s.Nontrivial

Tactic:
Set.Subsingleton,

Goal state after:
α : Type u
s : Set α
⊢ (¬∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x = y) ↔ s.Nontrivial
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c : α
⊢ a \ c ≤ a \ b ⊔ b \ c

Tactic:
rw [sdiff_le_iff, sup_left_comm, ← sdiff_le_iff]
  exact sdiff_sdiff_le.trans le_sup_sdiff

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

Goal state before:
pp: α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
hx : y ≤ x
hy : y ≠ ⊥
h : x ⊓ y = ⊥
⊢ y = ⊥

Tactic:
rw [← h, inf_eq_right.mpr hx]

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

Goal state before:
pp: ε : Type u_9
p : ε → Prop
inst✝ : DecidablePred p
ep ep' : Perm { a // p a }
en en' : Perm { a // ¬p a }
⊢ Equiv.trans (ep.subtypeCongr en) (ep'.subtypeCongr en') = subtypeCongr (Equiv.trans ep ep') (Equiv.trans en en')

Tactic:
by
  grind [eq_def, coe_trans]

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

Goal state before:
pp: α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
p : α → Prop
inst✝ : DecidablePred p
x₀ : { a // p a } → β
x✝ : { x // x ∘ Subtype.val = x₀ }
x : α → β
hx : x ∘ Subtype.val = x₀
a : α
⊢ ↑((fun x ↦ ⟨fun a ↦ if h : p a then x₀ ⟨a, h⟩ else x ⟨a, h⟩, ⋯⟩) ((fun x a ↦ ↑x ↑a) ⟨x, hx⟩)) a = ↑⟨x, hx⟩ a

Tactic:
dsimp only
        split_ifs
        · rw [← hx]; rfl
        · rfl

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

Goal state before:
pp: α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
p : α → Prop
inst✝ : DecidablePred p
x₀ : { a // p a } → β
x✝ : { x // x ∘ Subtype.val = x₀ }
x : α → β
hx : x ∘ Subtype.val = x₀
a : α
⊢ ↑((fun x ↦ ⟨fun a ↦ if h : p a then x₀ ⟨a, h⟩ else x ⟨a, h⟩, ⋯⟩) ((fun x a ↦ ↑x ↑a) ⟨x, hx⟩)) a = ↑⟨x, hx⟩ a

Tactic:
by
        dsimp only
        split_ifs
        · rw [← hx]; rfl
        · rfl

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

Goal state before:
pp: α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type u_9
β : Type u_10
f : α → β
p : α → Prop
q : β → Prop
h : ∀ (x : α), p x ↔ q (f x)
y : Subtype q
⊢ { x // ⟨f ↑x, ⋯⟩ = y } ≃ { x // f x = ↑y }

Tactic:
refine (subtypeSubtypeEquivSubtypeExists _ _).trans (subtypeEquivRight ?_)

Goal state after:
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type u_9
β : Type u_10
f : α → β
p : α → Prop
q : β → Prop
h : ∀ (x : α), p x ↔ q (f x)
y : Subtype q
⊢ ∀ (x : α), (∃ h_1, ⟨f ↑⟨x, h_1⟩, ⋯⟩ = y) ↔ f x = ↑y
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c : α
⊢ a ∆ b \ c = a \ (b ⊔ c) ⊔ b \ (a ⊔ c)

Tactic:
by
  rw [symmDiff, sup_sdiff_distrib, sdiff_sdiff_left, sdiff_sdiff_left]

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ a ∆ b \ (a ⊓ b) = a ∆ b

Tactic:
rw [symmDiff_sdiff]

Goal state after:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ a \ (b ⊔ a ⊓ b) ⊔ b \ (a ⊔ a ⊓ b) = a ∆ b
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b : α
h : a ≤ a ∆ b
⊢ Disjoint a b

Tactic:
rw [symmDiff_eq_sup_sdiff_inf] at h

Goal state after:
α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b : α
h : a ≤ (a ⊔ b) \ (a ⊓ b)
⊢ Disjoint a b
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
β : Type u_1
x y z : α
inst✝⁹ : Max α
inst✝⁸ : Min α
inst✝⁷ : LE α
inst✝⁶ : LT α
inst✝⁵ : Top α
inst✝⁴ : Bot α
inst✝³ : Compl α
inst✝² : SDiff α
inst✝¹ : HImp α
inst✝ : BooleanAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
map_compl : ∀ (a : α), f aᶜ = (f a)ᶜ
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
a b : α
⊢ f a ⊓ (f b)ᶜ = f (a ⊓ bᶜ)

Tactic:
by rw [map_inf, map_compl]

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

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

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

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
⊢ Injective (preimage f) ↔ Surjective f

Tactic:
rw [← Injective.of_comp_iff Set.mem_injective, ← Injective.of_comp_iff' _ Set.ofPred_bijective]
  exact injective_comp_right_iff_surjective

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

Goal state before:
pp: case inr.refine_1
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
st : s.Nonempty ∧ t.Nonempty
H : s ×ˢ t ⊆ s₁ ×ˢ t₁
⊢ s ⊆ s₁

Tactic:
have := image_mono (f := Prod.fst) H
    rwa [fst_image_prod _ st.2, fst_image_prod _ (h.mono H).snd] at this

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
f : α → β
h : Disjoint s₁ s₂
H : InjOn f (s₁ ∪ s₂)
⊢ ∀ (x : α), x ∈ s₁ → ∀ (y : α), y ∈ s₂ → f x ≠ f y

pp: case refine_2
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
f : α → β
h : Disjoint s₁ s₂
⊢ (InjOn f s₁ ∧ InjOn f s₂ ∧ ∀ (x : α), x ∈ s₁ → ∀ (y : α), y ∈ s₂ → f x ≠ f y) → InjOn f (s₁ ∪ s₂)

Tactic:
· intro x hx y hy hxy
    obtain rfl : x = y := H (Or.inl hx) (Or.inr hy) hxy
    exact h.le_bot ⟨hx, hy⟩

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
f : α → β
h : Disjoint s₁ s₂
⊢ (InjOn f s₁ ∧ InjOn f s₂ ∧ ∀ (x : α), x ∈ s₁ → ∀ (y : α), y ∈ s₂ → f x ≠ f y) → InjOn f (s₁ ∪ s₂)
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g₁ g₂ : Perm α
s : Set α
h : LeftInvOn (⇑g₁) (⇑g₂) s
⊢ LeftInvOn (⇑(g₁.extendDomain f)) (⇑(g₂.extendDomain f)) (Subtype.val ∘ ⇑f '' s)

Tactic:
rintro _ ⟨a, ha, rfl⟩; simp_rw [Function.comp_apply, extendDomain_apply_image, h ha]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g₁ g₂ : Perm α
t : Set α
h : RightInvOn (⇑g₁) (⇑g₂) t
⊢ RightInvOn (⇑(g₁.extendDomain f)) (⇑(g₂.extendDomain f)) (Subtype.val ∘ ⇑f '' t)

Tactic:
rintro _ ⟨a, ha, rfl⟩; simp_rw [Function.comp_apply, extendDomain_apply_image, h ha]

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

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

Tactic:
by ext; simp [pow_iterate, Nat.pow_succ', pow_mul]

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

Goal state before:
pp: G : Type u_3
inst✝ : CommGroup G
a b c : G
h : a = b * c
⊢ a / b = c

Tactic:
rw [h, div_eq_mul_inv, mul_comm, inv_mul_cancel_left]

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

Goal state before:
pp: α : Type u
inst✝ : Monoid α
u₁ u₂ : αˣ
⊢ u₂.inv * ↑u₂ = 1

Tactic:
inv_val

Goal state after:
α : Type u
inst✝ : Monoid α
u₁ u₂ : αˣ
⊢ 1 = 1
Module: Mathlib.Algebra.Group.Units.Basic

Goal state before:
pp: α : Type u
inst✝ : CommMonoid α
x y : α
ux uy : αˣ
⊢ y /ₚ uy * ↑ux = x ↔ x * ↑uy = y * ↑ux

Tactic:
divp_mul_eq_mul_divp,

Goal state after:
α : Type u
inst✝ : CommMonoid α
x y : α
ux uy : αˣ
⊢ y * ↑ux /ₚ uy = x ↔ x * ↑uy = y * ↑ux
Module: Mathlib.Algebra.Group.Units.Basic

Goal state before:
pp: α : Type u
inst✝ : CommMonoid α
x y : α
ux uy : αˣ
⊢ x /ₚ ux * (y /ₚ uy) = x * y /ₚ (ux * uy)

Tactic:
divp_mul_eq_mul_divp,

Goal state after:
α : Type u
inst✝ : CommMonoid α
x y : α
ux uy : αˣ
⊢ x * (y /ₚ uy) /ₚ ux = x * y /ₚ (ux * uy)
Module: Mathlib.Algebra.GroupWithZero.InjSurj

Goal state before:
pp: M₀ : Type u_1
M₀' : Type u_3
inst✝⁴ : Mul M₀
inst✝³ : Zero M₀
inst✝² : Mul M₀'
inst✝¹ : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst✝ : IsRightCancelMulZero M₀'
a✝ : M₀
Hne : a✝ ≠ 0
x✝¹ x✝ : M₀
He : (fun x ↦ x * a✝) x✝¹ = (fun x ↦ x * a✝) x✝
this : f x✝¹ * f a✝ = f x✝ * f a✝
⊢ x✝¹ = x✝

Tactic:
exact hf (mul_right_cancel₀ (fun Hfa => Hne <| hf <| by rw [Hfa, zero]) this)

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

Goal state before:
pp: α : Type u_4
p : α → Prop
f : Perm α
n : ℕ
hf : ∀ (x : α), p (f x) ↔ p x
⊢ f.subtypePerm hf ^ n = (f ^ n).subtypePerm ⋯

Tactic:
induction n with
  | zero => simp
  | succ n ih => simp_rw [pow_succ', ih, subtypePerm_mul]

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

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

Tactic:
rintro ⟨a, rfl⟩; 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 k : α
hk : a = 2 * k + 1
⊢ Odd (-a)

Tactic:
use -(k + 1)

Goal state after:
case h
α : Type u_2
inst✝ : Ring α
a k : α
hk : a = 2 * k + 1
⊢ -a = 2 * -(k + 1) + 1
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_4
f : α → α
hf : Involutive f
n : ℕ
⊢ f^[2]^[n] = id

Tactic:
involutive_iff_iter_2_eq_id.1 hf,

Goal state after:
α : Type u_4
f : α → α
hf : Involutive f
n : ℕ
⊢ id^[n] = id
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: R : Type u_4
inst✝¹ : Monoid R
inst✝ : HasDistribNeg R
n : ℕ
x✝ : Even n ∨ Odd n
⊢ (-1) ^ n = if Even n then 1 else -1

Tactic:
cases even_or_odd n with

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

Goal state before:
pp: α : Type u_1
inst✝³ : Preorder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
⊢ a - b ≤ c ↔ a ≤ b + c

Tactic:
tsub_le_iff_right,

Goal state after:
α : Type u_1
inst✝³ : Preorder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
⊢ a ≤ c + b ↔ a ≤ b + c
Module: Mathlib.Algebra.Order.Monoid.Unbundled.MinMax

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
inst✝² : Mul α
inst✝¹ : MulLeftMono α
inst✝ : MulRightStrictMono α
a₁ a₂ b₁ b₂ : α
⊢ a₁ * b₁ ≤ a₂ * b₂ → a₁ ≤ a₂ ∨ b₁ < b₂

Tactic:
contrapose!
  exact fun h => mul_lt_mul_of_lt_of_le h.1 h.2

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

Goal state before:
pp: case inl
α : Type u
inst✝³ : CommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedMonoid α
inst✝ : Nontrivial α
y : α
hy : y ≠ 1
h : y < 1
⊢ ∃ a, 1 < a

Tactic:
exact ⟨y⁻¹, one_lt_inv'.mpr h⟩

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝⁵ : MulZeroClass α
a b c d : α
inst✝⁴ : PartialOrder α
inst✝³ : PosMulReflectLE α
inst✝² : MulPosReflectLE α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
ha : 0 < a
hc : 0 < c
hab : a ≤ b
hcd : c ≤ d
h : b * d ≤ a * c
⊢ b ≤ a

Tactic:
grw [hcd] at h
    · exact le_of_mul_le_mul_of_pos_right h <| hc.trans_le hcd
    · exact ha.le

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
x : α
y : β
⊢ x < e.symm y ↔ e x < y

Tactic:
by
  rw [← e.lt_iff_lt, e.apply_symm_apply]

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

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

Tactic:
← mul_le_mul_iff_left (x ⊓ (y ⊓ z)),

Goal state after:
α✝ : 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 ⊓ (y ⊓ z)) * (x ⊔ y ⊓ z)
Module: Mathlib.Algebra.Order.Group.Abs

Goal state before:
pp: G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
⊢ |a|ₘ = |a / b * b|ₘ

Tactic:
rw [div_mul_cancel]

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

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

Tactic:
rw [div_mul_cancel]

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

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

Tactic:
rw [div_mul_cancel]

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:
rw [Int.neg_mul_neg, Int.neg_mul_neg]

Goal state after:
m n : ℕ
⊢ ↑(-[m+1].gcd -[n+1]) = (↑m + 1) * m.succ.gcdA -[n+1].natAbs + (↑n + 1) * -[m+1].natAbs.gcdB n.succ
Module: Mathlib.Algebra.Order.Ring.Int

Goal state before:
pp: n p q : ℕ
dvd : ∃ x y, ↑n = ↑(p + 1) * x + ↑(q + 1) * y
le : p * q ≤ n
a_n b_n : ℤ
eq : ↑n = ↑(p + 1) * a_n + ↑(q + 1) * b_n
a : ℤ := a_n % ↑q.succ
b : ℤ := b_n + a_n / ↑q.succ * ↑p.succ
this : a * ↑p.succ + b * ↑q.succ = ↑n
hb : b ≤ -1
ha : a_n % ↑q.succ < ↑(↑q.succ).natAbs
⊢ ↑q * ↑p.succ + -1 * ↑q.succ = ↑p * ↑q - 1

Tactic:
simp_rw [Nat.cast_succ, mul_add, mul_comm]; lia

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 : α
h : c ≤ b
⊢ a - c ≤ b - c ↔ a ≤ b

Tactic:
tsub_le_iff_right,

Goal state after:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
h : c ≤ b
⊢ a ≤ b - c + c ↔ a ≤ b
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 : α
hc : AddLECancellable c
h : c ≤ b
⊢ a < b - c ↔ c + a < b

Tactic:
by
  rw [add_comm]
  exact hc.lt_tsub_iff_right_of_le h

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : AddCommGroupWithOne R
inst✝³ : PartialOrder R
inst✝² : AddLeftMono R
inst✝¹ : ZeroLEOneClass R
inst✝ : NeZero 1
m n : ℤ
⊢ 0 ≤ n - m ↔ m ≤ n

Tactic:
sub_nonneg

Goal state after:
R : Type u_1
inst✝⁴ : AddCommGroupWithOne R
inst✝³ : PartialOrder R
inst✝² : AddLeftMono R
inst✝¹ : ZeroLEOneClass R
inst✝ : NeZero 1
m n : ℤ
⊢ m ≤ n ↔ m ≤ n
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case coe.bot
α : Type u
β : Type v
inst✝³ : Add α
F : Type u_1
inst✝² : Add β
inst✝¹ : FunLike F α β
inst✝ : AddHomClass F α β
f : F
a✝ : α
⊢ map (⇑f) (↑a✝ + ⊥) = map ⇑f ↑a✝ + map ⇑f ⊥

Tactic:
exact (add_bot _).symm

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
inst✝³ : IsStrictOrderedRing R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : ExistsAddOfLE R
a : R
n : ℕ
⊢ ⌈a - ↑n⌉₊ = ⌈a⌉₊ - n

Tactic:
obtain han | hna := le_total a n
  · rwa [ceil_eq_zero.2 (tsub_nonpos_of_le han), eq_comm, tsub_eq_zero_iff_le, Nat.ceil_le]
  · refine eq_tsub_of_add_eq ?_
    rw [← ceil_add_natCast, tsub_add_cancel_of_le hna]
    exact le_tsub_of_add_le_left ((add_zero _).trans_le hna)

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
inst✝³ : IsStrictOrderedRing R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : ExistsAddOfLE R
a : R
n : ℕ
⊢ ⌈a - ↑n⌉₊ = ⌈a⌉₊ - n

Tactic:
by
  obtain han | hna := le_total a n
  · rwa [ceil_eq_zero.2 (tsub_nonpos_of_le han), eq_comm, tsub_eq_zero_iff_le, Nat.ceil_le]
  · refine eq_tsub_of_add_eq ?_
    rw [← ceil_add_natCast, tsub_add_cancel_of_le hna]
    exact le_tsub_of_add_le_left ((add_zero _).trans_le hna)

Goal state after:
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
h2 : 0 ≤ x + y
⊢ x ^ (k + 1 + 1) + y ^ (k + 1 + 1) ≤ (x + y) ^ (k + 1 + 1)

Tactic:
calc
      x ^ (n + 1) + y ^ (n + 1) ≤ x * x ^ n + y * y ^ n + (x * y ^ n + y * x ^ n) := by
        rw [pow_succ' _ n, pow_succ' _ n]
        exact le_add_of_nonneg_right h1
      _ = (x + y) * (x ^ n + y ^ n) := by
        rw [add_mul, mul_add, mul_add, add_comm (y * x ^ n), ← add_assoc, ← add_assoc,
          add_assoc (x * x ^ n) (x * y ^ n), add_comm (x * y ^ n) (y * y ^ n), ← add_assoc]
      _ ≤ (x + y) ^ (n + 1) := by
        rw [pow_succ' _ n]
        gcongr; exact ih (Nat.succ_ne_zero k)

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
⊢ StrictAntiOn f (insert a s) ↔ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s

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

Goal state after:
Module: Mathlib.Order.WellFounded

Goal state before:
pp: α : Sort u_1
r : α → α → Prop
x : α
⊢ Acc r x ↔ IsEmpty { f // f 0 = x ∧ ∀ (n : ℕ), r (f (n + 1)) (f n) }

Tactic:
contrapose!
  rw [nonempty_subtype]
  exact not_acc_iff_exists_descending_chain

Goal state after: