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

Goal state before:
pp: G : Type u_2
inst✝ : SubNegMonoid G
a : G
n : ℕ
⊢ Int.negSucc n • a = -(↑(n + 1) • a)

Tactic:
exact SubNegMonoid.zsmul_neg' n a

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

Goal state before:
pp: α : Type u
f : α → Type (max u v)
hf : Surjective f
T : Type (max u v) := Sigma f
U : α
hU : f U = Set T
g : Set T → T := fun s ↦ ⟨U, cast ⋯ s⟩
⊢ Injective g

Tactic:
intro s t h

Goal state after:
α : Type u
f : α → Type (max u v)
hf : Surjective f
T : Type (max u v) := Sigma f
U : α
hU : f U = Set T
g : Set T → T := fun s ↦ ⟨U, cast ⋯ s⟩
s t : Set T
h : g s = g t
⊢ s = t
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_2
inst✝ : Nonempty α
f : α → β
g : β → α
hf : Injective f
hg : RightInverse g f
b : β
⊢ f (invFun f b) = f (g b)

Tactic:
rw [hg b]

Goal state after:
α : Sort u_1
β : Sort u_2
inst✝ : Nonempty α
f : α → β
g : β → α
hf : Injective f
hg : RightInverse g f
b : β
⊢ f (invFun f b) = b
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Type u_1
α' : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f : α → α' → β
a : α
a' : α'
b : β
⊢ curry (uncurry (update f a (update (f a) a' b))) = curry (update (uncurry f) (a, a') b)

Tactic:
simp [curry_update]

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

Goal state before:
pp: α : Type u_1
α' : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f : α → α' → β
a : α
a' : α'
b : β
⊢ uncurry (update f a (update (f a) a' b)) = update (uncurry f) (a, a') b

Tactic:
apply curry_injective
  simp [curry_update]

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a b : α
h : SymmGen r b a
⊢ SymmGen (Function.swap r) a b

Tactic:
by
  induction h with
  | inl hba => exact of_rel hba
  | inr hab => exact of_rel_symm hab

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
i✝¹ i✝ : α
h : Function.swap (ReflTransGen r) i✝¹ i✝
⊢ ReflTransGen (Function.swap r) i✝¹ i✝

Tactic:
induction h with
  | refl => rfl
  | tail _ hbc ih => exact ih.head hbc

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
i✝¹ i✝ : α
h : TransGen r i✝¹ i✝
⊢ EqvGen r i✝¹ i✝

Tactic:
induction h using TransGen.trans_induction_on with

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

Goal state before:
pp: I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f i
i : I
inst✝ : (i : I) → Monoid (f i)
⊢ ∀ (x : (i : I) → f i), x ^ 0 = 1

Tactic:
by intros; ext; exact Monoid.npow_zero _

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

Goal state before:
pp: α : Type u_5
β : Type u_6
a : α
b₁ : β
⊢ ∀ ⦃a₂ : β⦄, (a, b₁) = (a, a₂) → b₁ = a₂

Tactic:
b₂

Goal state after:
α : Type u_5
β : Type u_6
a : α
b₁ b₂ : β
⊢ (a, b₁) = (a, b₂) → b₁ = b₂
Module: Mathlib.Data.Prod.Basic

Goal state before:
pp: α : Type u_5
β : Type u_6
b : β
b₁ : α
⊢ ∀ ⦃a₂ : α⦄, (fun a ↦ (a, b)) b₁ = (fun a ↦ (a, b)) a₂ → b₁ = a₂

Tactic:
b₂

Goal state after:
α : Type u_5
β : Type u_6
b : β
b₁ b₂ : α
⊢ (fun a ↦ (a, b)) b₁ = (fun a ↦ (a, b)) b₂ → b₁ = b₂
Module: Mathlib.Data.Nat.Init

Goal state before:
pp: case le_succ_of_le
a b c d e m✝ n✝ k✝ : ℕ
p : ℕ → Prop
n m k : ℕ
h✝ : m ≤ k
ih :
  {motive : (m : ℕ) → m ≤ k → Sort u_1} →
    ((k_1 : ℕ) → (h : k_1 < k) → motive (k_1 + 1) h → motive k_1 ⋯) → motive k ⋯ → motive m h✝
motive : (m : ℕ) → m ≤ k + 1 → Sort u_1
of_succ : (k_1 : ℕ) → (h : k_1 < k + 1) → motive (k_1 + 1) h → motive k_1 ⋯
self : motive (k + 1) ⋯
⊢ motive m ⋯

Tactic:
| @le_succ_of_le k _ ih =>

Goal state after:
Module: Mathlib.Order.Compare

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
x y : α
β : Type u_3
inst✝ : LinearOrder β
x' y' : β
h : cmp x y = cmp x' y'
⊢ x = y ↔ x' = y'

Tactic:
rw [le_antisymm_iff, le_antisymm_iff, le_iff_le_of_cmp_eq_cmp h,
      le_iff_le_of_cmp_eq_cmp (cmp_eq_cmp_symm.1 h)]

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
inst✝ : SemilatticeSup α
a b c x : α
⊢ a ⊔ b ⊔ c ≤ x ↔ a ⊔ (b ⊔ c) ≤ x

Tactic:
by simp only [sup_le_iff]; rw [and_assoc]

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

Goal state before:
pp: α : Type u_1
s t : Set α
a : α
⊢ ¬a ∈ s ∧ Disjoint t s ↔ ¬a ∈ s ∧ Disjoint s t

Tactic:
disjoint_comm

Goal state after:
α : Type u_1
s t : Set α
a : α
⊢ ¬a ∈ s ∧ Disjoint s t ↔ ¬a ∈ s ∧ Disjoint s t
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
inst✝ : DistribLattice α
a b c : α
⊢ (a ⊓ b ⊔ a) ⊓ (a ⊓ b ⊔ c) = a ⊓ b ⊔ a ⊓ c

Tactic:
by rw [sup_inf_left]

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
β : Type v
e : α ≃ β
inst✝ : Lattice β
⊢ Lattice α

Tactic:
let semilatticeSup := e.semilatticeSup
  let semilatticeInf := e.semilatticeInf
  apply e.injective.lattice <;> intros <;> first | rfl | exact e.apply_symm_apply _

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

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

Tactic:
by rw [sup_inf_left]

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b : α
⊢ Disjoint b a ↔ Disjoint a b

Tactic:
disjoint_comm

Goal state after:
α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b : α
⊢ Disjoint a b ↔ Disjoint a b
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ᶜ

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

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

Goal state after:
case mpr
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
y : β
⊢ y ∈ f '' s ∪ g '' sᶜ → y ∈ range (s.piecewise f g)
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
⊢ Injective (image f)

Tactic:
intro s t h

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
s t : Set α
h : f '' s = f '' t
⊢ s = t
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
s t : Set α
h : t ⊆ s
x : α
⊢ x ∈ val '' {x | ↑x ∈ t} ↔ x ∈ t

Tactic:
mem_image

Goal state after:
α : Type u_1
s t : Set α
h : t ⊆ s
x : α
⊢ (∃ x_1, x_1 ∈ {x | ↑x ∈ t} ∧ ↑x_1 = x) ↔ x ∈ t
Module: Mathlib.Algebra.Group.Hom.Defs

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
F : Type u_9
inst✝ : MulOne M
n : ℕ
f : Monoid.End M
⊢ (⇑f)^[n] = ⇑(npowRec n f)

Tactic:
by induction n <;> simp [npowRec, *] <;> rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
f' : β → α
hf : LeftInvOn f' f s
⊢ f' '' f '' s = s

Tactic:
Set.image_image,

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
f' : β → α
hf : LeftInvOn f' f s
⊢ (fun x ↦ f' (f x)) '' s = s
Module: Mathlib.Data.Int.Init

Goal state before:
pp: m n : ℕ
h : n.succ ≤ m
⊢ ofNat m + -[n+1] = ofNat (m - n.succ)

Tactic:
rw [negSucc_eq, ofNat_eq_natCast, ofNat_eq_natCast, ← Int.natCast_one, ← Int.natCast_add,
    ← Int.sub_eq_add_neg, ← Int.natCast_sub h]

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

Goal state before:
pp: α : 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 : α}, r b c → p a b → p b c → p a c → f a c = f a b * f b c

Tactic:
intro b c rbc pab pbc pac

Goal state after:
α : 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
⊢ f a c = f a b * f b c
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:
hmul rba rac (symm pab) pac pbc

Goal state after:
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 a * f a c)
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: case hf_swap
α : Type u_1
β : Type u_2
inst✝¹ : Monoid β
r : α → α → Prop
inst✝ : Std.Total r
f : α → α → β
p : α → Prop
hswap : ∀ {a b : α}, p a → p b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a → p b → p c → f a c = f a b * f b c
a b c : α
pa : p a
pb : p b
pc : p c
this : Std.Symm fun x1 x2 ↦ p x1 ∧ p x2
⊢ ∀ {a b : α}, p a → p b → f a b * f b a = 1

Tactic:
exact @hswap

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

Goal state before:
pp: α : Type u
inst✝ : DivisionMonoid α
a : α
h : IsUnit a
⊢ a / a = 1

Tactic:
rw [div_eq_mul_inv, h.mul_inv_cancel]

Goal state after:
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
hf : Bijective ⇑f
⊢ Bijective ⇑(map f)

Tactic:
refine ⟨map_injective hf.injective, ?_⟩

Goal state after:
M : Type u
N : Type v
inst✝¹ : Monoid M
inst✝ : Monoid N
f : M →* N
hf : Bijective ⇑f
⊢ Surjective ⇑(map f)
Module: Mathlib.Algebra.Group.Units.Basic

Goal state before:
pp: α : Type u
inst✝ : DivisionCommMonoid α
a b c d : α
hb : IsUnit b
hd : IsUnit d
⊢ a / b = c / d ↔ a * d = c * b

Tactic:
hb.div_eq_div_iff hd

Goal state after:
α : Type u
inst✝ : DivisionCommMonoid α
a b c d : α
hb : IsUnit b
hd : IsUnit d
⊢ a * d = c * b ↔ a * d = c * b
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: n : ℕ
S : Type u_5
inst✝ : MonoidWithZero S
x : S
hx : IsNilpotent x
N : ℕ
hN : x ^ N = 0
⊢ (x ^ n.succ) ^ N = 0

Tactic:
by rw [← pow_mul, Nat.succ_mul, pow_add, hN, mul_zero]

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

Goal state before:
pp: A : Type u_2
inst✝ : AddMonoidWithOne A
n : ℕ
⊢ (n + 1) • 1 = ↑(n + 1)

Tactic:
simp [succ_nsmul, nsmul_one n]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Defs

Goal state before:
pp: M : Type u_1
M₀ : Type u_2
M₀' : Type u_3
G₀ : Type u_4
G₀' : Type u_5
N : Type u_6
A : Type u_7
A' : Type u_8
B : Type u_9
α : Type u_10
β : Type u_11
inst✝⁵ : Zero M₀
inst✝⁴ : Zero A
inst✝³ : SMulWithZero M₀ A
a : M₀
b : A
inst✝² : Zero M₀'
inst✝¹ : Zero A'
inst✝ : SMul M₀ A'
f : ZeroHom A A'
hf : Surjective ⇑f
smul : ∀ (a : M₀) (b : A), f (a • b) = a • f b
m : A'
⊢ 0 • m = 0

Tactic:
rcases hf m with ⟨x, rfl⟩
    simp [← smul]

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

Goal state before:
pp: I : Type u_3
f : I → Type u_4
i' : I
inst : ∀ (i : I), Nonempty (f i)
inst✝ : Nontrivial (f i')
⊢ Nontrivial ((i : I) → f i)

Tactic:
classical
  let := Classical.decEq (∀ i : I, f i)
  exact (Function.update_injective (fun i ↦ Classical.choice (inst i)) i').nontrivial

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
n✝ : ℕ
a b : M
u✝ u₁ u₂ u : Mˣ
x : M
n : ℕ
hn : n ≠ 0
hu : x ^ n = ↑u
⊢ x * x ^ (n - 1) = ↑u

Tactic:
← _root_.pow_succ',

Goal state after:
M : Type u_1
inst✝ : Monoid M
n✝ : ℕ
a b : M
u✝ u₁ u₂ u : Mˣ
x : M
n : ℕ
hn : n ≠ 0
hu : x ^ n = ↑u
⊢ x ^ (n - 1 + 1) = ↑u
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:
by
  rintro ⟨a, rfl⟩; exact ⟨f a, by simp [two_mul]⟩

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

Goal state before:
pp: α : Type u
inst✝⁴ : MulOneClass α
inst✝³ : Preorder α
inst✝² : ExistsMulOfLE α
a b : α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulLeftReflectLT α
⊢ (∃ c, 1 < c ∧ a * c = b) → a < b

Tactic:
rintro ⟨c, hc, rfl⟩; exact lt_mul_of_one_lt_right' _ hc

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

Goal state before:
pp: case pos
α : Type u_1
inst✝² : MulOneClass α
inst✝¹ : LinearOrder α
inst✝ : MulLeftStrictMono α
a : α
h : a < 1
⊢ ∃ b, b * b ≤ a

Tactic:
use a

Goal state after:
case h
α : Type u_1
inst✝² : MulOneClass α
inst✝¹ : LinearOrder α
inst✝ : MulLeftStrictMono α
a : α
h : a < 1
⊢ a * a ≤ a
Module: Mathlib.Algebra.Order.Monoid.Unbundled.MinMax

Goal state before:
pp: case inl
α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : Mul α
inst✝³ : MulLeftMono α
inst✝² : MulRightMono α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a₁ a₂ b₁ b₂ : α
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
ha' : a₁ < a₂
⊢ a₁ * b₁ < a₂ * b₂

Tactic:
exact mul_lt_mul_of_lt_of_le ha' hb

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

Goal state before:
pp: α : Type u_1
inst✝³ : MulZeroClass α
a b : α
inst✝² : Preorder α
inst✝¹ : MulPosStrictMono α
inst✝ : MulPosReflectLT α
h : 0 < b
⊢ 0 < a * b ↔ 0 < a

Tactic:
simpa using mul_lt_mul_iff_left₀ (b := 0) h

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₀
n : ℕ
inst✝¹ : ZeroLEOneClass M₀
inst✝ : PosMulMono M₀
ha : 1 ≤ a
hn : n ≠ 0
⊢ a ≤ a ^ n

Tactic:
simpa only [pow_one] using pow_le_pow_right₀ ha <| Nat.pos_iff_ne_zero.2 hn

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

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b : G₀
ha : 0 < a
⊢ a⁻¹ < b ↔ 1 < b * a

Tactic:
by
  rw [← mul_inv_lt_iff₀ ha, one_mul]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
F : Type u_5
inst✝¹ : FunLike F α β
inst✝ : RelHomClass F r s
f : F
a : α
⊢ Acc s (f a) → Acc r a

Tactic:
generalize h : f a = b
  intro ac
  induction ac generalizing a with | intro _ H IH => ?_
  subst h
  exact ⟨_, fun a' h => IH (f a') (map_rel f h) _ rfl⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
x✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
x y : Quotient x✝
⊢ r ((Embedding.quotientOut α) x) ((Embedding.quotientOut α) y) ↔ Quotient.lift₂ r H x y

Tactic:
induction x, y using Quotient.inductionOn₂

Goal state after:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
x✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
a✝ b✝ : α
⊢ r ((Embedding.quotientOut α) ⟦a✝⟧) ((Embedding.quotientOut α) ⟦b✝⟧) ↔ Quotient.lift₂ r H ⟦a✝⟧ ⟦b✝⟧
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α β : Type u
r : α → α → Prop
s : β → β → Prop
h₁ : α = β
h₂ : r ≍ s
a b : α
⊢ s ((Equiv.cast h₁) a) ((Equiv.cast h₁) b) ↔ r a b

Tactic:
subst h₁

Goal state after:
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α✝ → α✝ → Prop
s✝ : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α : Type u
r : α → α → Prop
a b : α
s : α → α → Prop
h₂ : r ≍ s
⊢ s ((Equiv.cast ⋯) a) ((Equiv.cast ⋯) b) ↔ r a b
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α β γ : Type u
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
h₁ : α = β
h₁' : β = γ
h₂ : r ≍ s
h₂' : s ≍ t
x : α
⊢ ((RelIso.cast h₁ h₂).trans (RelIso.cast h₁' h₂')) x = (RelIso.cast ⋯ ⋯) x

Tactic:
subst h₁

Goal state after:
α γ : Type u
r : α → α → Prop
t : γ → γ → Prop
x : α
s : α → α → Prop
h₁' : α = γ
h₂ : r ≍ s
h₂' : s ≍ t
⊢ ((RelIso.cast ⋯ h₂).trans (RelIso.cast h₁' h₂')) x = (RelIso.cast ⋯ ⋯) x
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
ha : 1 ≤ a
k : ℕ
⊢ 1 ≤ a ^ (k + 1)

Tactic:
by
    rw [pow_succ]
    exact one_le_mul (one_le_pow_of_le ha k) ha

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|ₘ / |b|ₘ|ₘ ≤ |a / b|ₘ

Tactic:
rw [mabs, sup_le_iff]

Goal state after:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ |a|ₘ / |b|ₘ ≤ |a / b|ₘ ∧ (|a|ₘ / |b|ₘ)⁻¹ ≤ |a / b|ₘ
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 n : G
one_le_a : 1 ≤ a
a_le_n : a ≤ n
one_le_b : 1 ≤ b
b_le_n : b ≤ n
⊢ a ≤ n * b ∧ b / a ≤ n

Tactic:
div_le_iff_le_mul

Goal state after:
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b n : G
one_le_a : 1 ≤ a
a_le_n : a ≤ n
one_le_b : 1 ≤ b
b_le_n : b ≤ n
⊢ a ≤ n * b ∧ b ≤ n * a
Module: Mathlib.Algebra.Order.Group.Abs

Goal state before:
pp: G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a : G
⊢ a ≤ a⁻¹ ↔ a ≤ 1

Tactic:
le_inv_self_iff

Goal state after:
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a : G
⊢ a ≤ 1 ↔ a ≤ 1
Module: Mathlib.Algebra.Ring.Int.Parity

Goal state before:
pp: case mpr
n x : ℕ
h : n = x * x
⊢ IsSquare ↑n

Tactic:
· exact ⟨x, mod_cast h⟩

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

Goal state before:
pp: case H1
x y a b : ℕ
h : 0 < a
IH :
  ∀ {s t s' t' : ℤ},
    ↑b % ↑a = ↑x * s + ↑y * t →
      ↑a = ↑x * s' + ↑y * t' →
        ↑((b % a).xgcdAux s t a s' t').1 =
          ↑x * ((b % a).xgcdAux s t a s' t').2.1 + ↑y * ((b % a).xgcdAux s t a s' t').2.2
s t s' t' : ℤ
p : ↑a = ↑x * s + ↑y * t
p' : ↑b = ↑x * s' + ↑y * t'
k : ℤ
⊢ ↑x * s' + ↑y * t' - (↑x * s * k + ↑y * t * k) = ↑x * s' + (↑y * t' - ↑y * t * k) - ↑x * s * k

Tactic:
add_comm (x * s * k),

Goal state after:
case H1
x y a b : ℕ
h : 0 < a
IH :
  ∀ {s t s' t' : ℤ},
    ↑b % ↑a = ↑x * s + ↑y * t →
      ↑a = ↑x * s' + ↑y * t' →
        ↑((b % a).xgcdAux s t a s' t').1 =
          ↑x * ((b % a).xgcdAux s t a s' t').2.1 + ↑y * ((b % a).xgcdAux s t a s' t').2.2
s t s' t' : ℤ
p : ↑a = ↑x * s + ↑y * t
p' : ↑b = ↑x * s' + ↑y * t'
k : ℤ
⊢ ↑x * s' + ↑y * t' - (↑y * t * k + ↑x * s * k) = ↑x * s' + (↑y * t' - ↑y * t * k) - ↑x * s * k
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f : α →* β
h : ∀ (b : β), ∃ a, f a = b
b : β
a : α
ha : f a = b
⊢ ∃ a, (map' f) a = ↑b

Tactic:
use a

Goal state after:
case h
α : Type u_1
β : Type u_2
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f : α →* β
h : ∀ (b : β), ∃ a, f a = b
b : β
a : α
ha : f a = b
⊢ (map' f) ↑a = ↑b
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a b : α
⊢ a + b ≠ ⊤ ↔ a ≠ ⊤ ∧ b ≠ ⊤

Tactic:
by simp [← isAddUnit_iff]

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
⊢ a - b + min a b = a

Tactic:
rw [← tsub_min, @tsub_add_cancel_of_le]
  apply min_le_left

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

Goal state before:
pp: case neg
α : Type u_1
inst✝³ : AddCommMonoid α
inst✝² : LinearOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : AddRightReflectLE α
a b c : α
h : a < b
⊢ 0 ≤ c ↔ a ≤ c + b

Tactic:
constructor <;> intro h'

Goal state after:
case neg.mp
α : Type u_1
inst✝³ : AddCommMonoid α
inst✝² : LinearOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : AddRightReflectLE α
a b c : α
h : a < b
h' : 0 ≤ c
⊢ a ≤ c + b

case neg.mpr
α : Type u_1
inst✝³ : AddCommMonoid α
inst✝² : LinearOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : AddRightReflectLE α
a b c : α
h : a < b
h' : a ≤ c + b
⊢ 0 ≤ c
Module: Mathlib.Data.Nat.Find

Goal state before:
pp: m✝¹ n✝ k✝ : ℕ
p q : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
n : ℕ
pn : p n
m✝ m : ℕ
IH : ∀ (k : ℕ), n ≤ k + m → Acc lbp k
k : ℕ
kn : n ≤ k + m.succ
y : ℕ
r : y.lbp k
_a : ∀ (k_1 : ℕ), k_1 ≤ k → ¬p k_1
⊢ n ≤ k + 1 + m

Tactic:
rw [Nat.add_right_comm]

Goal state after:
m✝¹ n✝ k✝ : ℕ
p q : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
n : ℕ
pn : p n
m✝ m : ℕ
IH : ∀ (k : ℕ), n ≤ k + m → Acc lbp k
k : ℕ
kn : n ≤ k + m.succ
y : ℕ
r : y.lbp k
_a : ∀ (k_1 : ℕ), k_1 ≤ k → ¬p k_1
⊢ n ≤ k + m + 1
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoBotOrder α
y : α
h : ∀ (b : α), ↑y ≤ ↑b
⊢ False

Tactic:
exact not_isBot y fun z => coe_le_coe.1 (h z)

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

Goal state before:
pp: case pos
P : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
hk : P (k + 1)
⊢ findGreatest P (k + 1) = m ↔ m ≤ k + 1 ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k + 1 → ¬P n

Tactic:
rw [findGreatest_eq hk]

Goal state after:
case pos
P : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
hk : P (k + 1)
⊢ k + 1 = m ↔ m ≤ k + 1 ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k + 1 → ¬P n
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 <;> norm_cast at * <;>
    aesop (add simp WithTop.add_le_add_iff_right)

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

Goal state before:
pp: case neg
P Q : ℕ → Prop
inst✝¹ : DecidablePred P
inst✝ : DecidablePred Q
hPQ : ∀ (n : ℕ), P n → Q n
n : ℕ
hn : findGreatest P n ≤ findGreatest Q n
h : ¬P (n + 1)
⊢ findGreatest P (n + 1) ≤ findGreatest Q (n + 1)

Tactic:
findGreatest_of_not h

Goal state after:
case neg
P Q : ℕ → Prop
inst✝¹ : DecidablePred P
inst✝ : DecidablePred Q
hPQ : ∀ (n : ℕ), P n → Q n
n : ℕ
hn : findGreatest P n ≤ findGreatest Q n
h : ¬P (n + 1)
⊢ findGreatest P n ≤ findGreatest Q (n + 1)
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
inst✝ : IsStrictOrderedRing R
ha : 0 ≤ a
n b : ℕ
⊢ ⌈a + ↑n⌉₊ ≤ b ↔ ⌈a⌉₊ + n ≤ b

Tactic:
contrapose!
    rw [lt_ceil]
    obtain hb | hb := le_or_gt n b
    · obtain ⟨d, rfl⟩ := exists_add_of_le hb
      rw [Nat.cast_add, add_comm n, add_comm (n : R), add_lt_add_iff_right, add_lt_add_iff_right,
        lt_ceil]
    · exact iff_of_true (lt_add_of_nonneg_of_lt ha <| cast_lt.2 hb) (Nat.lt_add_left _ hb)

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

Goal state before:
pp: α : Type u
inst✝ : Monoid α
a b : α
x✝ : Invertible a
⊢ a * (⅟a * b) = b

Tactic:
rw [← mul_assoc, mul_invOf_self, one_mul]

Goal state after: