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

Goal state before:
pp: case succ.succ
n : Nat
n0 : ¬n + 1 + 1 = 0
⊢ (if (n + 1 + 1) >>> 1 = 0 then 0 else ((n + 1 + 1) >>> 1).log2.succ) <
    if n + 1 + 1 = 0 then 0 else (n + 1 + 1).log2.succ

Tactic:
have : (n + 1 + 1) >>> 1 ≠ 0 := Nat.div_ne_zero_iff.mpr ⟨by decide, le_add_left ..⟩

Goal state after:
case succ.succ
n : Nat
n0 : ¬n + 1 + 1 = 0
this : (n + 1 + 1) >>> 1 ≠ 0
⊢ (if (n + 1 + 1) >>> 1 = 0 then 0 else ((n + 1 + 1) >>> 1).log2.succ) <
    if n + 1 + 1 = 0 then 0 else (n + 1 + 1).log2.succ
Module: Mathlib.Data.Nat.BinaryRec

Goal state before:
pp: case succ.succ
n : Nat
n0 : ¬n + 1 + 1 = 0
this : (n + 1 + 1) >>> 1 ≠ 0
⊢ (if (n + 1 + 1) >>> 1 = 0 then 0 else ((n + 1 + 1) >>> 1).log2.succ) <
    if n + 1 + 1 = 0 then 0 else (n + 1 + 1).log2.succ

Tactic:
simpa only [if_neg n0, if_neg this, log2_eq_succ_log2_shiftRight this] using lt_succ_self _

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:
by
  rw [← pow_mul, Nat.mul_comm, pow_mul]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
inst✝ : Nonempty α
q : Prop
p : α → Prop
⊢ (∀ (x : α), q ∧ p x) ↔ q ∧ ∀ (x : α), p x

Tactic:
by rw [forall_and, forall_const]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
inst✝ : Nonempty α
p : α → Prop
q : Prop
⊢ (∀ (x : α), p x ∧ q) ↔ (∀ (x : α), p x) ∧ q

Tactic:
by rw [forall_and, forall_const]

Goal state after:
Module: Mathlib.Logic.Unique

Goal state before:
pp: A : Sort u_2
B : Sort u_3
inst✝¹ : Unique A
inst✝ : Unique B
f : A → B
⊢ Function.Bijective f

Tactic:
rw [Function.bijective_iff_has_inverse]

Goal state after:
A : Sort u_2
B : Sort u_3
inst✝¹ : Unique A
inst✝ : Unique B
f : A → B
⊢ ∃ g, Function.LeftInverse g f ∧ Function.RightInverse g f
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : β → γ → Prop
q : γ → δ → Prop
a : α
d : δ
⊢ ((r ∘r p) ∘r q) a d = (r ∘r p ∘r q) a d

Tactic:
apply propext

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : β → γ → Prop
q : γ → δ → Prop
a : α
d : δ
⊢ ((r ∘r p) ∘r q) a d ↔ (r ∘r p ∘r q) a d
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : α → β → Prop
p : β → γ → Prop
c : γ
a : α
⊢ flip (r ∘r p) c a = (flip p ∘r flip r) c a

Tactic:
apply propext

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → β → Prop
p : β → γ → Prop
c : γ
a : α
⊢ flip (r ∘r p) c a ↔ (flip p ∘r flip r) c a
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝ : IsTrans α r
f : α → β
hf : ∀ (x y : α), f x = f y → r x y
⊢ IsTrans β (Relation.Map r f f)

Tactic:
refine ⟨fun _ _ _ ⟨x, y, hxy, hx, hy⟩ ⟨y', z, hyz, hy', hz⟩ ↦ ?_⟩
  exact ⟨x, z, trans_of r hxy <| trans_of r (hf y y' <| hy' ▸ hy) hyz, hx, hz⟩

Goal state after:
Module: Mathlib.Order.Max

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
a : α
inst✝ : Nontrivial α
ha : IsBot a
⊢ ¬IsMax a

Tactic:
by
  intro ha'
  obtain ⟨b, hb⟩ := exists_ne a
  exact hb <| ha'.eq_of_ge (ha.lt_of_ne hb.symm).le

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

Goal state before:
pp: b₀ b₁ : Bool
h : b₀ ≤ b₁
⊢ b₀.toNat ≤ b₁.toNat

Tactic:
cases b₀ <;> cases b₁

Goal state after:
case false.false
h : false ≤ false
⊢ false.toNat ≤ false.toNat

case false.true
h : false ≤ true
⊢ false.toNat ≤ true.toNat

case true.false
h : true ≤ false
⊢ true.toNat ≤ false.toNat

case true.true
h : true ≤ true
⊢ true.toNat ≤ true.toNat
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:
← not_lt,

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
x y : α
β : Type u_3
inst✝ : LinearOrder β
x' y' : β
h : cmp x y = cmp x' y'
⊢ ¬y < x ↔ x' ≤ y'
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderTop α
a b c : α
⊢ Codisjoint a (b ⊓ c) ↔ Codisjoint a b ∧ Codisjoint a c

Tactic:
by
  simp only [codisjoint_iff, sup_inf_left, inf_eq_top_iff]

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a b c : α
hab : Disjoint a b
hbc : Codisjoint b c
⊢ a ≤ c

Tactic:
by
  rw [← @inf_top_eq _ _ _ a, ← @bot_sup_eq _ _ _ c, ← hab.eq_bot, ← hbc.eq_top, sup_inf_right]
  exact inf_le_inf_right _ le_sup_left

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

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

pp: case neg
f : ℕ → ℕ
mono_f : Monotone f
c : ℕ
ih : (∀ (n : ℕ), f n ≤ c) → ∃ b N, ∀ (n : ℕ), n ≥ N → f n = b
hc : ∀ (n : ℕ), f n ≤ c + 1
h : ∃ n, c < f n
⊢ ∃ b N, ∀ (n : ℕ), n ≥ N → f n = b

Tactic:
· exact ih h

Goal state after:
case neg
f : ℕ → ℕ
mono_f : Monotone f
c : ℕ
ih : (∀ (n : ℕ), f n ≤ c) → ∃ b N, ∀ (n : ℕ), n ≥ N → f n = b
hc : ∀ (n : ℕ), f n ≤ c + 1
h : ∃ n, c < f n
⊢ ∃ b N, ∀ (n : ℕ), n ≥ N → f n = b
Module: Mathlib.Data.Set.Subsingleton

Goal state before:
pp: α : Type u
x : α
H : {x}.Nontrivial
⊢ False

Tactic:
rw [nontrivial_iff_exists_ne (mem_singleton x)] at H
  let ⟨y, hy, hya⟩ := H
  exact hya (mem_singleton_iff.1 hy)

Goal state after:
Module: Mathlib.Control.EquivFunctor

Goal state before:
pp: f : Type u₀ → Type u₁
inst✝¹ : Functor f
inst✝ : LawfulFunctor f
α β γ : Type u₀
k : α ≃ β
h : β ≃ γ
⊢ Functor.map ⇑(k.trans h) = Functor.map ⇑h ∘ Functor.map ⇑k

Tactic:
ext x
    apply LawfulFunctor.comp_map k h x

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

Goal state before:
pp: α : Type u_1
t s₁ s₂ s : Set α
h : s₁ ∩ s = s₂ ∩ s
⊢ t.ite s₁ s₂ ∩ s = s₁ ∩ s

Tactic:
← ite_inter,

Goal state after:
α : Type u_1
t s₁ s₂ s : Set α
h : s₁ ∩ s = s₂ ∩ s
⊢ t.ite (s₁ ∩ s) (s₂ ∩ s) = s₁ ∩ s
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:

Tactic:
x ⊓ y \ z ⊔ (z ⊓ x ⊔ x \ y) = (x ⊔ (z ⊓ x ⊔ x \ y)) ⊓ (y \ z ⊔ (z ⊓ x ⊔ x \ y)) := by
          rw [sup_inf_right]
      _ = (x ⊔ x ⊓ z ⊔ x \ y) ⊓ (y \ z ⊔ (x ⊓ z ⊔ x \ y)) := by ac_rfl
      _ = x ⊓ (y \ z ⊔ (x ⊓ z ⊔ x ⊓ y) ⊔ x \ y) := by
          rw [sup_inf_self, sup_sdiff_left, ← sup_assoc, sup_inf_left, sdiff_sup_self',
            inf_sup_right, sup_comm y, inf_sdiff_sup_right, inf_sup_left x z y]
      _ = x ⊓ (y \ z ⊔ (x ⊓ z ⊔ (x ⊓ y ⊔ x \ y))) := by ac_rfl
      _ = x := by simp

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

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
h : x < z \ y
hyz : y ≤ z
⊢ x ⊔ y < z \ y ⊔ y

Tactic:
refine lt_of_le_not_ge (by grw [h]) fun h' => h.not_ge ?_

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
h : x < z \ y
hyz : y ≤ z
h' : z \ y ⊔ y ≤ x ⊔ y
⊢ z \ y ≤ x
Module: Mathlib.Data.Set.Image

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
s : Set β
⊢ f '' f ⁻¹' s = s

Tactic:
rw [hf.image_preimage]

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s : Set α
t : Set β
f : α → β
p₁ : α → γ
p₂ : β → δ
g : γ → δ
comm : ∀ (a : α), p₂ (f a) = g (p₁ a)
hinj : InjOn g (p₁ '' s)
h1 : MapsTo f s t
h2 : InjOn f s
h3 : SurjOn f s t
a : α
ha : a ∈ s
⊢ g (p₁ a) ∈ p₂ '' t

Tactic:
exact ⟨f a, h1 ha, by rw [comm a]⟩

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

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
f : α → β
g : β → α
s : Set α
hgf : LeftInvOn g f s
ginj : InjOn g (g ⁻¹' s)
x : β
⊢ x ∈ f '' s → x ∈ g ⁻¹' s

pp: case mpr
α : Type u_1
β : Type u_2
f : α → β
g : β → α
s : Set α
hgf : LeftInvOn g f s
ginj : InjOn g (g ⁻¹' s)
x : β
⊢ x ∈ g ⁻¹' s → x ∈ f '' s

Tactic:
· rintro ⟨y, hy, rfl⟩
    rw [mem_preimage, hgf hy]; exact hy

Goal state after:
case mpr
α : Type u_1
β : Type u_2
f : α → β
g : β → α
s : Set α
hgf : LeftInvOn g f s
ginj : InjOn g (g ⁻¹' s)
x : β
⊢ x ∈ g ⁻¹' s → x ∈ f '' s
Module: Mathlib.Algebra.Group.Hom.Basic

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
G : Type u_5
H : Type u_6
F : Type u_7
inst✝¹ : CommGroup G
inst✝ : Group H
f : G →* H
hf : Function.Surjective ⇑f
⊢ ∀ (a b : H), a * b = b * a

Tactic:
by simp_rw [hf.forall₂, ← map_mul, mul_comm, implies_true]

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a b : α
⊢ (a * b) ^ (-1) = b ^ (-1) * a ^ (-1)

Tactic:
by
  simp only [zpow_neg, zpow_one, mul_inv_rev]

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
x : G
m n : ℤ
h : x ^ n = 1
⊢ x ^ (m % n + n * (m / n)) = x ^ (m % n)

Tactic:
simp [zpow_add, zpow_mul, h]

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

Goal state before:
pp: α : Type u
inst✝ : Monoid α
v i₁ : α
vi₁ : v * i₁ = 1
iv₁ : i₁ * v = 1
v' i₂ : α
vi₂ : v' * i₂ = 1
iv₂ : i₂ * v' = 1
e : ↑{ val := v, inv := i₁, val_inv := vi₁, inv_val := iv₁ } = ↑{ val := v', inv := i₂, val_inv := vi₂, inv_val := iv₂ }
⊢ { val := v, inv := i₁, val_inv := vi₁, inv_val := iv₁ } = { val := v', inv := i₂, val_inv := vi₂, inv_val := iv₂ }

Tactic:
simp only at e

Goal state after:
α : Type u
inst✝ : Monoid α
v i₁ : α
vi₁ : v * i₁ = 1
iv₁ : i₁ * v = 1
v' i₂ : α
vi₂ : v' * i₂ = 1
iv₂ : i₂ * v' = 1
e : v = v'
⊢ { val := v, inv := i₁, val_inv := vi₁, inv_val := iv₁ } = { val := v', inv := i₂, val_inv := vi₂, inv_val := iv₂ }
Module: Mathlib.Algebra.Group.Units.Basic

Goal state before:
pp: α : Type u
inst✝ : DivisionCommMonoid α
a b : α
h : IsUnit a
⊢ a / b / a = b⁻¹

Tactic:
rw [div_eq_mul_inv, div_eq_mul_inv, mul_right_comm, h.mul_inv_cancel, one_mul]

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

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
h : a ≠ 0
a_eq_0 : a⁻¹ = 0
⊢ False

Tactic:
simpa [a_eq_0] using mul_inv_cancel₀ h

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

Goal state before:
pp: M₀ : Type u_1
inst✝¹ : MonoidWithZero M₀
n : ℕ
inst✝ : Nontrivial M₀
⊢ 0 ^ n = 1 ↔ n = 0

Tactic:
zero_pow_eq,

Goal state after:
M₀ : Type u_1
inst✝¹ : MonoidWithZero M₀
n : ℕ
inst✝ : Nontrivial M₀
⊢ (if n = 0 then 1 else 0) = 1 ↔ n = 0
Module: Mathlib.Data.Nat.Cast.Defs

Goal state before:
pp: case pos
R : Type u_1
inst✝ : AddMonoidWithOne R
k : ℕ
hk : ∀ (m : ℕ), m < k + 1 → m.binCast = ↑m
h : (k + 1) % 2 = 0
⊢ ↑((k + 1) / 2) + ↑((k + 1) / 2) = ↑((k + 1) % 2 + 2 * ((k + 1) / 2))

Tactic:
← Nat.cast_add

Goal state after:
case pos
R : Type u_1
inst✝ : AddMonoidWithOne R
k : ℕ
hk : ∀ (m : ℕ), m < k + 1 → m.binCast = ↑m
h : (k + 1) % 2 = 0
⊢ ↑((k + 1) / 2 + (k + 1) / 2) = ↑((k + 1) % 2 + 2 * ((k + 1) / 2))
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: M₀ : Type u_1
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a✝ b✝ x a b : G₀
⊢ (a * b)⁻¹ = b⁻¹ * a⁻¹

Tactic:
by
    by_cases ha : a = 0
    · simp [ha]
    by_cases hb : b = 0
    · simp [hb]
    apply inv_eq_of_mul
    simp [mul_assoc, ha, hb]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : AddMonoidWithOne R
k : ℕ
hk : ∀ (m : ℕ), m < k + 1 → m.binCast = ↑m
h : ¬(k + 1) % 2 = 0
⊢ ↑((k + 1) / 2) + ↑((k + 1) / 2) + 1 = ↑((k + 1) % 2 + 2 * ((k + 1) / 2))

Tactic:
← Nat.cast_add

Goal state after:
case neg
R : Type u_1
inst✝ : AddMonoidWithOne R
k : ℕ
hk : ∀ (m : ℕ), m < k + 1 → m.binCast = ↑m
h : ¬(k + 1) % 2 = 0
⊢ ↑((k + 1) / 2 + (k + 1) / 2) + 1 = ↑((k + 1) % 2 + 2 * ((k + 1) / 2))
Module: Mathlib.Data.Nat.Cast.Defs

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoidWithOne R
⊢ ↑1 + ↑1 = 2

Tactic:
← Nat.cast_add

Goal state after:
R : Type u_1
inst✝ : AddMonoidWithOne R
⊢ ↑(1 + 1) = 2
Module: Mathlib.Data.Nat.Cast.Defs

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoidWithOne R
⊢ ↑(1 + 1) + ↑1 = 3

Tactic:
← Nat.cast_add

Goal state after:
R : Type u_1
inst✝ : AddMonoidWithOne R
⊢ ↑(1 + 1 + 1) = 3
Module: Mathlib.Data.Nat.Cast.Defs

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoidWithOne R
⊢ ↑(1 + 1 + 1) + ↑1 = 4

Tactic:
← Nat.cast_add

Goal state after:
R : Type u_1
inst✝ : AddMonoidWithOne R
⊢ ↑(1 + 1 + 1 + 1) = 4
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
⊢ a⁻¹ = 0 ↔ a = 0

Tactic:
by rw [inv_eq_iff_eq_inv, inv_zero]

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

Goal state before:
pp: n a : ℕ
⊢ a = n.sqrt ↔ a ^ 2 ≤ n ∧ n < (a + 1) ^ 2

Tactic:
simpa only [Nat.pow_two] using eq_sqrt

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

Goal state before:
pp: R : Type u_1
inst✝¹ : DivisionMonoid R
inst✝ : HasDistribNeg R
a : R
⊢ -a⁻¹ = (-a)⁻¹

Tactic:
by rw [inv_eq_one_div, inv_eq_one_div, div_neg_eq_neg_div]

Goal state after:
Module: Mathlib.Algebra.Ring.Hom.Defs

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : CommRing β
f : β →+ α
h : ∀ (x : β), f (x * x) = f x * f x
h_two : 2 ≠ 0
h_one : f 1 = 1
x y : β
hxy : f x * f x + f (y * x) + (f (x * y) + f y * f y) - (f x * f x + f x * f y + (f y * f x + f y * f y)) = 0
⊢ (↑f).toFun (x * y) = (↑f).toFun x * (↑f).toFun y

Tactic:
add_comm (f x * f x + f (y * x)),

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : CommRing β
f : β →+ α
h : ∀ (x : β), f (x * x) = f x * f x
h_two : 2 ≠ 0
h_one : f 1 = 1
x y : β
hxy : f (x * y) + f y * f y + (f x * f x + f (y * x)) - (f x * f x + f x * f y + (f y * f x + f y * f y)) = 0
⊢ (↑f).toFun (x * y) = (↑f).toFun x * (↑f).toFun y
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
a b c d : G₀
hc : c ≠ 0
hd : d ≠ 0
h : 0 = c / d
hb : b = 0
⊢ False

Tactic:
exact div_ne_zero hc hd h.symm

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

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
a b : α
u₁ u₂ : αˣ
⊢ a * ↑u₁⁻¹ + b * ↑u₂⁻¹ = a * ↑u₂ * (↑u₂⁻¹ * ↑u₁⁻¹) + ↑u₂⁻¹ * ↑u₁⁻¹ * (↑u₁ * b)

Tactic:
mul_comm b

Goal state after:
α : Type u
inst✝ : CommSemiring α
a b : α
u₁ u₂ : αˣ
⊢ a * ↑u₁⁻¹ + ↑u₂⁻¹ * b = a * ↑u₂ * (↑u₂⁻¹ * ↑u₁⁻¹) + ↑u₂⁻¹ * ↑u₁⁻¹ * (↑u₁ * b)
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs

Goal state before:
pp: case refine_1
N : Type u_2
r : N → N → Prop
inst✝ : Group N
h : Covariant N N (fun x1 x2 ↦ x1 * x2) r
a b c : N
bc : r ((fun x1 x2 ↦ x1 * x2) a b) ((fun x1 x2 ↦ x1 * x2) a c)
⊢ r b c

pp: case refine_2
N : Type u_2
r : N → N → Prop
inst✝ : Group N
h : Contravariant N N (fun x1 x2 ↦ x1 * x2) r
a b c : N
bc : r b c
⊢ r ((fun x1 x2 ↦ x1 * x2) a b) ((fun x1 x2 ↦ x1 * x2) a c)

Tactic:
· rw [← inv_mul_cancel_left a b, ← inv_mul_cancel_left a c]
    exact h a⁻¹ bc

Goal state after:
case refine_2
N : Type u_2
r : N → N → Prop
inst✝ : Group N
h : Contravariant N N (fun x1 x2 ↦ x1 * x2) r
a b c : N
bc : r b c
⊢ r ((fun x1 x2 ↦ x1 * x2) a b) ((fun x1 x2 ↦ x1 * x2) a c)
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs

Goal state before:
pp: N : Type u_2
r : N → N → Prop
mu : N → N → N
h : Std.Commutative mu
⊢ Covariant N N (flip mu) r ↔ Covariant N N mu r

Tactic:
unfold flip; simp_rw [h.comm]

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

Goal state before:
pp: N : Type u_2
r : N → N → Prop
mu : N → N → N
h : Std.Commutative mu
⊢ Contravariant N N (flip mu) r ↔ Contravariant N N mu r

Tactic:
unfold flip; simp_rw [h.comm]

Goal state after:
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✝ : AddGroupWithOne R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : R), f (x + y) = f x + f y
neg : ∀ (x : R), f (-x) = -f x
sub : ∀ (x y : R), f (x - y) = f x - f y
nsmul : ∀ (n : ℕ) (x : R), f (n • x) = n • f x
zsmul : ∀ (n : ℤ) (x : R), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f ↑n = ↑n
intCast : ∀ (n : ℤ), f ↑n = ↑n
n : ℕ
⊢ ↑(Int.negSucc n) = -↑(n + 1)

Tactic:
rw [← intCast, Int.cast_negSucc, neg, natCast]

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

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : LinearOrder G₀
a : G₀
inst✝¹ : PosMulStrictMono G₀
inst✝ : ZeroLEOneClass G₀
ha₀ : 0 ≤ a
ha₁ : a ≠ 1
n : ℤ
⊢ a ^ n = 1 ↔ n = 0

Tactic:
obtain rfl | ha₀ := ha₀.eq_or_lt

Goal state after:
case inl
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : LinearOrder G₀
inst✝¹ : PosMulStrictMono G₀
inst✝ : ZeroLEOneClass G₀
n : ℤ
ha₀ : 0 ≤ 0
ha₁ : 0 ≠ 1
⊢ 0 ^ n = 1 ↔ n = 0

case inr
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : LinearOrder G₀
a : G₀
inst✝¹ : PosMulStrictMono G₀
inst✝ : ZeroLEOneClass G₀
ha₀✝ : 0 ≤ a
ha₁ : a ≠ 1
n : ℤ
ha₀ : 0 < a
⊢ a ^ n = 1 ↔ n = 0
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : LE α
inst✝ : PartialOrder β
f : α ≃o β
x : α
y : β
hx : ∀ (x' : α), x ≤ x'
hy : ∀ (y' : β), y ≤ y'
⊢ f x = y

Tactic:
refine le_antisymm ?_ (hy _)

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : LE α
inst✝ : PartialOrder β
f : α ≃o β
x : α
y : β
hx : ∀ (x' : α), x ≤ x'
hy : ∀ (y' : β), y ≤ y'
⊢ f x ≤ y
Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs

Goal state before:
pp: case mpr
α : Type u
inst✝³ : MulOneClass α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedMul α
a : α
inst✝ : MulLeftStrictMono α
c : α
⊢ 1 < c → a ≠ a * c

Tactic:
· rw [← (self_le_mul_right a c).lt_iff_ne]
    apply lt_mul_of_one_lt_right'

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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : Semigroup R
a b : R
⊢ IsRegular a ∧ IsRegular b → IsRegular (a * b) ∧ IsRegular (b * a)

Tactic:
· rintro ⟨ha, hb⟩
    exact ⟨ha.mul hb, hb.mul ha⟩

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

Goal state before:
pp: case inr.inr
G : Type u_1
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a✝ b✝ c a b : α
ha : a ≠ ⊤
hb : b ≠ ⊤
⊢ -(a + b) = -b + -a

Tactic:
· exact left_neg_eq_right_neg (a := a + b) (by simp [neg_add_cancel_of_ne_top, *])
        (by simp [add_assoc, add_neg_cancel_of_ne_top, add_neg_cancel_left_of_ne_top, *])

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 : b ≤ c
h2 : a ≤ c - b
⊢ a + b ≤ c

Tactic:
h2,

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

Tactic:
h2,

Goal state after:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
h : a ≤ c
h2 : b ≤ c - a
⊢ a + (c - a) ≤ c
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
y : β
v : WithBot α
⊢ ↑y = map f v ↔ ∃ x, v = ↑x ∧ f x = y

Tactic:
by
  cases v <;> simp [eq_comm]

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

Goal state before:
pp: α : Type u_2
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
z : ℤ
a : α
⊢ z < ⌊a⌋ ↔ ↑z + 1 ≤ a

Tactic:
rw [← add_one_le_iff, le_floor]; norm_cast

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: case inr
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
n : ℕ
inst✝ : IsStrictOrderedRing R
hn : n ≠ 0
ha : 0 ≤ a
⊢ n ≤ ⌊a⌋₊ ↔ ↑n ≤ a

Tactic:
exact le_floor_iff ha

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
a : R
inst✝ : IsStrictOrderedRing R
⊢ ⌊a⌋₊ = 0 ↔ a < 1

Tactic:
← lt_one_iff,

Goal state after:
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
inst✝ : IsStrictOrderedRing R
⊢ ⌊a⌋₊ < 1 ↔ a < 1
Module: Mathlib.Order.WithBot

Goal state before:
pp: case mpr
α : Type u_1
inst✝¹ : LT α
inst✝ : NoMinOrder α
h : DenselyOrdered α
⊢ ∀ (a₁ a₂ : WithBot α), a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂

Tactic:
· simpa [WithBot.exists, WithBot.forall, exists_lt] using DenselyOrdered.dense

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Ring α
inst✝ : LinearOrder α
a : α
⊢ |a| ^ 2 = a ^ 2

Tactic:
simpa only [sq] using abs_mul_abs_self a

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

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

Tactic:
rintro - ⟨⟨a, ha, b, hb, rfl⟩, h⟩

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s s' : Set α
t : Set β
a : α
ha : a ∈ s
b : β
hb : b ∈ t
h : ¬f a b ∈ image2 f s' t
⊢ f a b ∈ image2 f (s \ s') t
Module: Mathlib.Data.Set.NAry

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

Tactic:
rintro - ⟨⟨a, ha, b, hb, rfl⟩, h⟩

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t t' : Set β
a : α
ha : a ∈ s
b : β
hb : b ∈ t
h : ¬f a b ∈ image2 f s t'
⊢ f a b ∈ image2 f s (t \ t')
Module: Mathlib.Order.Bounds.Image

Goal state before:
pp: α : Type u
π : α → Type u_1
inst✝ : (a : α) → Preorder (π a)
s : Set ((a : α) → π a)
f : (a : α) → π a
⊢ IsLUB s f ↔ ∀ (a : α), IsLUB (eval a '' s) (f a)

Tactic:
refine
      ⟨fun H a => ⟨(Function.monotone_eval a).mem_upperBounds_image H.1, fun b hb => ?_⟩, fun H =>
        ⟨?_, ?_⟩⟩
    · suffices h : Function.update f a b ∈ upperBounds s from Function.update_self a b f ▸ H.2 h a
      exact fun g hg => le_update_iff.2 ⟨hb <| mem_image_of_mem _ hg, fun i _ => H.1 hg i⟩
    · exact fun g hg a => (H a).1 (mem_image_of_mem _ hg)
    · exact fun g hg a => (H a).2 ((Function.monotone_eval a).mem_upperBounds_image hg)

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

Goal state before:
pp: α : Type u_3
β : Type u_4
e : α ≃ β
p : α → Prop
⊢ {b | p (e.symm b)} = ⇑e '' {a | p a}

Tactic:
by
  rw [Equiv.image_eq_preimage_symm, preimage_ofPred_eq]

Goal state after:
Module: Mathlib.Order.Bounds.Image

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Preorder β
f g : α → β
h : ∀ (a : α), f a ≤ g a
hbdd : BddAbove (range g)
⊢ BddAbove (range f)

Tactic:
by
  obtain ⟨C, hC⟩ := hbdd
  use C
  rintro - ⟨x, rfl⟩
  exact (h x).trans (hC <| mem_range_self x)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : LinearOrder β
inst✝¹ : WellFoundedLT β
inst✝ : Preorder α
f g : α ≃o β
⊢ f = g

Tactic:
change f.symm.symm = g.symm.symm

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : LinearOrder β
inst✝¹ : WellFoundedLT β
inst✝ : Preorder α
f g : α ≃o β
⊢ f.symm.symm = g.symm.symm
Module: Mathlib.Tactic.NormNum.Basic

Goal state before:
pp: α : Type ?u.3
inst✝ : Semiring α
k : ℕ
b c : α
hc1 : c * ↑k * b = 1
hc2 : ↑k * b * c = 1
⊢ Invertible b

Tactic:
rw [Nat.cast_commute k, mul_assoc, Nat.cast_commute k] at hc2

Goal state after:
α : Type ?u.3
inst✝ : Semiring α
k : ℕ
b c : α
hc1 : c * ↑k * b = 1
hc2 : b * (c * ↑k) = 1
⊢ Invertible b