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)
⊢ binaryRecFromOne zero one bit 1 = one

Tactic:
by
  rw [binaryRecFromOne, binaryRec'_one, dif_pos rfl]

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

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

Tactic:
by
  simp [h]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
P : α → Prop
⊢ (∃ a, P a) ∨ ∀ (a : α), ¬P a

Tactic:
rw [← not_exists]; exact em _

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

Goal state before:
pp: α : Type u_4
β : Sort u_5
f : α → β
I : Injective f
a : α
b : β
h : partialInv f b = some a
hpi : partialInv f b = if h : ∃ a, f a = b then some (Classical.choose h) else none
h' : ∃ a, f a = b
⊢ f a = b

Tactic:
rw [hpi, dif_pos h'] at h
            injection h with h
            subst h
            apply Classical.choose_spec h'

Goal state after:
Module: Mathlib.Logic.Relation

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

Tactic:
funext c a
  apply propext
  constructor
  · exact fun ⟨b, hab, hbc⟩ ↦ ⟨b, hbc, hab⟩
  · exact fun ⟨b, hbc, hab⟩ ↦ ⟨b, hab, hbc⟩

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case symm
α : Type u_1
r p : α → α → Prop
hrp : r ≤ p
i✝¹ i✝ a b : α
a✝ : EqvGen r a b
ih : EqvGen p a b
⊢ EqvGen p b a

Tactic:
exact EqvGen.symm _ _ ih

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

Goal state before:
pp: α : Sort u
β : Sort v
γ : Sort w
r : α → α → Prop
e : α ≃ β
x✝¹ x✝ : α
⊢ r x✝¹ x✝ ↔ r (e.symm (e x✝¹)) (e.symm (e x✝))

Tactic:
by simp only [e.symm_apply_apply]

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

Goal state before:
pp: α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
inst✝⁷ : SMul α β
inst✝⁶ : SMul α γ
inst✝⁵ : SMul β δ
inst✝⁴ : SMul α δ
inst✝³ : SMul γ δ
inst✝² : IsScalarTower α β δ
inst✝¹ : IsScalarTower α γ δ
inst✝ : SMulCommClass β γ δ
a : α
b : β
c : γ
d : δ
⊢ a • b • c • d = a • c • b • d

Tactic:
smul_comm b

Goal state after:
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
inst✝⁷ : SMul α β
inst✝⁶ : SMul α γ
inst✝⁵ : SMul β δ
inst✝⁴ : SMul α δ
inst✝³ : SMul γ δ
inst✝² : IsScalarTower α β δ
inst✝¹ : IsScalarTower α γ δ
inst✝ : SMulCommClass β γ δ
a : α
b : β
c : γ
d : δ
⊢ a • c • b • d = a • c • b • d
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) → DivInvMonoid (f i)
⊢ ∀ (n : ℕ) (a : (i : I) → f i), a ^ Int.negSucc n = (a ^ ↑n.succ)⁻¹

Tactic:
by intros; ext; exact DivInvMonoid.zpow_neg' _ _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f₁ : α → β
g₁ : γ → δ
f₂ : β → α
g₂ : δ → γ
hf : LeftInverse f₁ f₂
hg : LeftInverse g₁ g₂
a : β × δ
⊢ id a = a

Tactic:
id

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f₁ : α → β
g₁ : γ → δ
f₂ : β → α
g₂ : δ → γ
hf : LeftInverse f₁ f₂
hg : LeftInverse g₁ g₂
a : β × δ
⊢ a = a
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ (if (fun x1 x2 ↦ x1 < x2) a b then Ordering.lt
      else if (fun x1 x2 ↦ x1 < x2) b a then Ordering.gt else Ordering.eq).Compares
    a b

Tactic:
split_ifs with h1 h2

Goal state after:
case pos
α : Type u_1
inst✝ : LinearOrder α
a b : α
h1 : (fun x1 x2 ↦ x1 < x2) a b
⊢ Ordering.lt.Compares a b

case pos
α : Type u_1
inst✝ : LinearOrder α
a b : α
h1 : ¬(fun x1 x2 ↦ x1 < x2) a b
h2 : (fun x1 x2 ↦ x1 < x2) b a
⊢ Ordering.gt.Compares a b

case neg
α : Type u_1
inst✝ : LinearOrder α
a b : α
h1 : ¬(fun x1 x2 ↦ x1 < x2) a b
h2 : ¬(fun x1 x2 ↦ x1 < x2) b a
⊢ Ordering.eq.Compares a b
Module: Mathlib.Data.Nat.Basic

Goal state before:
pp: n m : ℕ
⊢ n ∣ m - n ↔ n ∣ m ∨ m ≤ n

Tactic:
rcases le_or_gt m n with h | h

Goal state after:
case inl
n m : ℕ
h : m ≤ n
⊢ n ∣ m - n ↔ n ∣ m ∨ m ≤ n

case inr
n m : ℕ
h : n < m
⊢ n ∣ m - n ↔ n ∣ m ∨ m ≤ n
Module: Mathlib.Data.Nat.Init

Goal state before:
pp: a b c d e m n k : ℕ
p : ℕ → Prop
P : ℕ → Sort u_1
h : (k : ℕ) → k < n → m ≤ k → P (k + 1) → P k
mn : m ≤ n
hP : P n
⊢ P m

Tactic:
induction mn using decreasingInduction with
  | self => exact hP
  | of_succ k hk ih =>
    exact h _ (lt_of_succ_le hk) (Nat.le_refl _)
      (ih fun k' hk' h'' => h k' hk' <| le_of_succ_le h'')

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a b x y : α
h : IsCompl x y
hle : a ≤ b ⊔ y
⊢ b ⊓ x ⊔ y ⊓ x = b ⊓ x

Tactic:
h.symm.inf_eq_bot,

Goal state after:
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a b x y : α
h : IsCompl x y
hle : a ≤ b ⊔ y
⊢ b ⊓ x ⊔ ⊥ = b ⊓ x
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a b : Complementeds α
⊢ ↑a ⊔ ↑b = ⊤ ↔ a ⊔ b = ⊤

Tactic:
← coe_sup,

Goal state after:
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a b : Complementeds α
⊢ ↑(a ⊔ b) = ⊤ ↔ a ⊔ b = ⊤
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: α : Type u_2
inst✝ : HeytingAlgebra α
a b : α
⊢ (a ⊔ b)ᶜ = aᶜ ⊓ bᶜ

Tactic:
by
  simp_rw [← himp_bot, sup_himp_distrib]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x : α
h : ∃ x', e (some x) = some x'
⊢ some (e.removeNoneAux x) = e (some x)

Tactic:
simp [removeNoneAux, Option.isSome_iff_exists.mpr h]

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

Goal state before:
pp: case some
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x : α
a : β
h : e (some x) = some a
h1 : some x = e.symm (some a)
⊢ e (some x) = e none ↔ e.symm none = some x

Tactic:
simp only [apply_eq_iff_eq, reduceCtorEq]

Goal state after:
case some
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x : α
a : β
h : e (some x) = some a
h1 : some x = e.symm (some a)
⊢ False ↔ e.symm none = some x
Module: Mathlib.Order.BooleanAlgebra.Basic

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

Tactic:
by rw [← sdiff_inf_self_right, ← sdiff_inf_self_right z y, inf_comm, h, inf_comm]

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

Goal state before:
pp: α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x \ y = y ↔ x = ⊥ ∧ y = ⊥

Tactic:
rw [disjoint_sdiff_self_left.eq_iff]

Goal state after:
α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x \ y = ⊥ ∧ y = ⊥ ↔ x = ⊥ ∧ y = ⊥
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b c : α
⊢ a ∆ b ∆ c = b ∆ a ∆ c

Tactic:
symmDiff_comm

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
symmDiff_comm

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
a b : α
⊢ a ⇔ b ⇔ a = b

Tactic:
by rw [bihimp_comm, bihimp_bihimp_cancel_left]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
⊢ Disjoint (f '' s) t ↔ Disjoint s (f ⁻¹' t)

Tactic:
by
  simp_rw [disjoint_iff_inter_eq_empty, ← not_nonempty_iff_eq_empty, image_inter_nonempty_iff]

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

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

Tactic:
by_cases h : x ∈ s

Goal state after:
case pos
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
h : x ∈ s
⊢ s.piecewise f g x ∈ f '' s ∪ g '' sᶜ

case neg
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
h : ¬x ∈ s
⊢ s.piecewise f g x ∈ f '' s ∪ g '' sᶜ
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: case inl
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
h✝ : IsEmpty (α i)
⊢ (∀ (x : α i), i ∈ s ∧ ¬x ∈ t i) ↔ IsEmpty (α i) ∨ i ∈ s ∧ t i = ∅

Tactic:
simp [*, forall_and, eq_empty_iff_forall_notMem]

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

Goal state before:
pp: case inr
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
h✝ : Nonempty (α i)
⊢ (∀ (x : α i), i ∈ s ∧ ¬x ∈ t i) ↔ IsEmpty (α i) ∨ i ∈ s ∧ t i = ∅

Tactic:
simp [*, forall_and, eq_empty_iff_forall_notMem]

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

Goal state before:
pp: case mpr
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
inst✝ : Decidable (s.pi t).Nonempty
hi : ¬i ∈ s
xᵢ : α i
x : (i : ι) → α i
hx : ∀ (i : ι), i ∈ s → x i ∈ t i
⊢ ∃ x, (∀ (i : ι), i ∈ s → x i ∈ t i) ∧ x i = xᵢ

Tactic:
refine ⟨Function.update x i xᵢ, ?_⟩

Goal state after:
case mpr
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
inst✝ : Decidable (s.pi t).Nonempty
hi : ¬i ∈ s
xᵢ : α i
x : (i : ι) → α i
hx : ∀ (i : ι), i ∈ s → x i ∈ t i
⊢ (∀ (i_1 : ι), i_1 ∈ s → update x i xᵢ i_1 ∈ t i_1) ∧ update x i xᵢ i = xᵢ
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
s t : Set β
h : Disjoint (f ⁻¹' s) (f ⁻¹' t)
⊢ Disjoint s t

Tactic:
by
  rw [disjoint_iff_inter_eq_empty, ← image_preimage_eq (_ ∩ _) hf, preimage_inter, h.inter_eq,
    image_empty]

Goal state after:
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✝¹ : Group G
H : Type u_8
inst✝ : Group H
f : G → H
map_div : ∀ (a b : G), f (a * b⁻¹) = f a * (f b)⁻¹
x y : G
⊢ f x * (f (1 * 1⁻¹ * y⁻¹))⁻¹ = f x * f y

Tactic:
{ simp only [map_div]
          simp only [mul_inv_cancel, one_mul, inv_inv] }

Goal state after:
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✝¹ : Group G
H : Type u_8
inst✝ : Group H
f : G → H
hf : ∀ (x y : G), f (x / y) = f x / f y
⊢ ∀ (a b : G), f (a * b⁻¹) = f a * (f b)⁻¹

Tactic:
simpa only [div_eq_mul_inv] using hf

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
h : IsUnit a
⊢ ∃ b, a * b = 1

Tactic:
rcases h with ⟨⟨a, b, hab, _⟩, rfl⟩

Goal state after:
M : Type u_1
inst✝ : Monoid M
a b : M
hab : a * b = 1
inv_val✝ : b * a = 1
⊢ ∃ b_1, ↑{ val := a, inv := b, val_inv := hab, inv_val := inv_val✝ } * b_1 = 1
Module: Mathlib.Algebra.Group.Units.Defs

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
h : IsUnit a
⊢ ∃ b, b * a = 1

Tactic:
by
  rcases h with ⟨⟨a, b, _, hba⟩, rfl⟩
  exact ⟨b, hba⟩

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

Goal state before:
pp: G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : DivInvMonoid G
inst✝ : DivInvMonoid H
x✝¹ : ℕ
x✝ : G × H
⊢ x✝ ^ Int.negSucc x✝¹ = (x✝ ^ ↑x✝¹.succ)⁻¹

Tactic:
ext <;> exact DivInvMonoid.zpow_neg' ..

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

Goal state before:
pp: G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : DivisionCommMonoid G
inst✝ : DivisionCommMonoid H
x✝¹ x✝ : G × H
g₁ : G
h₁ : H
fst✝ : G
snd✝ : H
⊢ (g₁, h₁) * (fst✝, snd✝) = (fst✝, snd✝) * (g₁, h₁)

Tactic:
by rw [mk_mul_mk, mul_comm g₁, mul_comm h₁]; rfl

Goal state after:
Module: Mathlib.Control.Basic

Goal state before:
pp: m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : α → m β
⊢ f >=> pure = f

Tactic:
simp +unfoldPartialApp only [(· >=> ·), functor_norm]

Goal state after:
Module: Mathlib.Control.Basic

Goal state before:
pp: m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α β : Type u
f : α → m β
⊢ pure >=> f = f

Tactic:
simp +unfoldPartialApp only [(· >=> ·), functor_norm]

Goal state after:
Module: Mathlib.Control.Basic

Goal state before:
pp: m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β γ φ : Type u
f : α → m β
g : β → m γ
h : γ → m φ
⊢ (f >=> g) >=> h = f >=> g >=> h

Tactic:
simp +unfoldPartialApp only [(· >=> ·), functor_norm]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : AddMonoidWithOne R
inst✝ : CharZero R
n : ℕ
⊢ ↑n = 1 ↔ n = 1

Tactic:
← cast_one,

Goal state after:
R : Type u_1
inst✝¹ : AddMonoidWithOne R
inst✝ : CharZero R
n : ℕ
⊢ ↑n = ↑1 ↔ n = 1
Module: Mathlib.Data.Int.Sqrt

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

Tactic:
natAbs_mul_self

Goal state after:
x : ℤ
x✝ : ∃ n, n * n = x
n : ℤ
hn : n * n = x
⊢ n * n = n * n
Module: Mathlib.Algebra.GroupWithZero.Semiconj

Goal state before:
pp: case pos
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a x y : G₀
h : SemiconjBy a x y
ha : a = 0
⊢ SemiconjBy a x⁻¹ y⁻¹

Tactic:
simp only [ha, zero_left]

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

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
a✝ : ℕ
⊢ a ≠ 0 → a ^ ↑a✝ ≠ 0

Tactic:
rw [zpow_natCast]

Goal state after:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
a✝ : ℕ
⊢ a ≠ 0 → a ^ a✝ ≠ 0
Module: Mathlib.Data.Nat.Cast.Commute

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
a x y : α
h : SemiconjBy a x y
m n : ℕ
⊢ SemiconjBy (↑m * a) (↑n * x) (↑n * y)

Tactic:
by
  simp [h]

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

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
a b : α
h : Commute a b
m n : ℕ
⊢ Commute (↑m * a) (↑n * b)

Tactic:
by
  simp [h]

Goal state after:
Module: Mathlib.Data.Int.Cast.Lemmas

Goal state before:
pp: α : Type u_3
inst✝¹ : AddGroupWithOne α
inst✝ : CharZero α
n : ℤ
⊢ ↑n = 1 ↔ n = 1

Tactic:
← cast_one,

Goal state after:
α : Type u_3
inst✝¹ : AddGroupWithOne α
inst✝ : CharZero α
n : ℤ
⊢ ↑n = ↑1 ↔ n = 1
Module: Mathlib.Data.Int.Cast.Lemmas

Goal state before:
pp: α : Type u_3
inst✝ : Ring α
a b : α
h : Commute a b
m : ℤ
⊢ Commute a (↑m * b)

Tactic:
by
  simp [h]

Goal state after:
Module: Mathlib.Data.Int.Cast.Lemmas

Goal state before:
pp: α : Type u_3
inst✝ : Ring α
a b : α
h : Commute a b
m : ℤ
⊢ Commute (↑m * a) b

Tactic:
by
  simp [h]

Goal state after:
Module: Mathlib.Algebra.Module.NatInt

Goal state before:
pp: case zero
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : R
y : M
⊢ (0 • x) • y = 0 • x • y

Tactic:
simp only [zero_smul]

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

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : MulRightStrictMono α
a : α
⊢ a⁻¹ < 1 ↔ 1 < a

Tactic:
rw [← mul_lt_mul_iff_right a, inv_mul_cancel, one_mul]

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

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : MulRightStrictMono α
a : α
⊢ 1 < a⁻¹ ↔ a < 1

Tactic:
rw [← mul_lt_mul_iff_right a, inv_mul_cancel, one_mul]

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

Goal state before:
pp: M₀ : Type u_2
inst✝⁴ : MonoidWithZero M₀
inst✝³ : Preorder M₀
a b : M₀
inst✝² : ZeroLEOneClass M₀
inst✝¹ : PosMulMono M₀
inst✝ : MulPosMono M₀
⊢ 1 ≤ a ∧ 1 < b ∨ 1 < a ∧ 1 ≤ b → 1 < a * b

Tactic:
by
  rintro (⟨ha, hb⟩ | ⟨ha, hb⟩); exacts [one_lt_mul ha hb, one_lt_mul_of_lt_of_le ha hb]

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

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : ZeroLEOneClass G₀
ha : 0 ≤ a
n : ℕ
⊢ 0 ≤ a ^ ↑n

Tactic:
rw [zpow_natCast]

Goal state after:
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : ZeroLEOneClass G₀
ha : 0 ≤ a
n : ℕ
⊢ 0 ≤ a ^ n
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : ZeroLEOneClass G₀
ha : 0 < a
n : ℕ
⊢ 0 < a ^ ↑n

Tactic:
rw [zpow_natCast]

Goal state after:
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : ZeroLEOneClass G₀
ha : 0 < a
n : ℕ
⊢ 0 < a ^ n
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₀
hb : 0 < b
⊢ a / b < 1 ↔ a < b

Tactic:
div_lt_iff₀ hb,

Goal state after:
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b : G₀
hb : 0 < b
⊢ a < 1 * b ↔ a < 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 d : G₀
hb : 0 < b
hd : 0 < d
⊢ a / b < c / d ↔ a * d < c * b

Tactic:
div_lt_iff₀ hb,

Goal state after:
G₀ : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b c d : G₀
hb : 0 < b
hd : 0 < d
⊢ a < c / d * b ↔ a * d < c * 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₀
hb : 0 < b
hc : 0 < c
⊢ a / b < c ↔ a / c < b

Tactic:
div_lt_iff₀ hb,

Goal state after:
G₀ : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b c : G₀
hb : 0 < b
hc : 0 < c
⊢ a < c * b ↔ a / c < b
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✝³ : Preorder α✝
inst✝² : Preorder β✝
α : Type ?u.13
β : Type ?u.15
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
g : β → α
h : ∀ (a : α) (b : β), cmp a (g b) = cmp (f a) b
gf : ∀ (a : α), a = g (f a)
⊢ ∀ {a b : α},
    { toFun := f, invFun := g, left_inv := ⋯, right_inv := ⋯ } a ≤
        { toFun := f, invFun := g, left_inv := ⋯, right_inv := ⋯ } b ↔
      a ≤ b

Tactic:
intro a b
      apply le_iff_le_of_cmp_eq_cmp
      convert! (h a (f b)).symm
      apply gf

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : SemilatticeSup α
inst✝² : OrderTop α
inst✝¹ : SemilatticeSup β
inst✝ : OrderTop β
a b : α
f : α ≃o β
ha : Codisjoint a b
⊢ ⊤ ≤ f a ⊔ f b

Tactic:
← f.map_sup,

Goal state after:
α : Type u_2
β : Type u_3
inst✝³ : SemilatticeSup α
inst✝² : OrderTop α
inst✝¹ : SemilatticeSup β
inst✝ : OrderTop β
a b : α
f : α ≃o β
ha : Codisjoint a b
⊢ ⊤ ≤ f (a ⊔ b)
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow

Goal state before:
pp: G : Type u_2
inst✝² : DivInvMonoid G
inst✝¹ : Preorder G
inst✝ : MulLeftMono G
x : G
H : 1 ≤ x
n : ℕ
⊢ 1 ≤ x ^ ↑n

Tactic:
rw [zpow_natCast]

Goal state after:
G : Type u_2
inst✝² : DivInvMonoid G
inst✝¹ : Preorder G
inst✝ : MulLeftMono G
x : G
H : 1 ≤ x
n : ℕ
⊢ 1 ≤ x ^ n
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow

Goal state before:
pp: G : Type u_2
inst✝² : DivInvMonoid G
inst✝¹ : Preorder G
inst✝ : MulLeftMono G
x : G
hx : 1 < x
n : ℕ
hn : 0 < ↑n
⊢ 1 < x ^ ↑n

Tactic:
rw [zpow_natCast]

Goal state after:
G : Type u_2
inst✝² : DivInvMonoid G
inst✝¹ : Preorder G
inst✝ : MulLeftMono G
x : G
hx : 1 < x
n : ℕ
hn : 0 < ↑n
⊢ 1 < x ^ n
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]
  constructor
  · apply div_le_iff_le_mul.2
    convert! mabs_mul_le (a / b) b
    rw [div_mul_cancel]
  · rw [div_eq_mul_inv, mul_inv_rev, inv_inv, mul_inv_le_iff_le_mul, mabs_div_comm]
    convert! mabs_mul_le (b / a) a
    · rw [div_mul_cancel]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Group α
inst✝ : LinearOrder α
a b : α
⊢ |a|ₘ = |b|ₘ ↔ a = b ∨ a = b⁻¹

Tactic:
refine ⟨fun h ↦ ?_, by rintro (h | h) <;> simp [h]⟩
  obtain rfl | rfl := eq_or_eq_inv_of_mabs_eq h <;>
    simpa only [inv_eq_iff_eq_inv (a := |b|ₘ), inv_inv, inv_inj, or_comm] using mabs_choice b

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✝ : CharZero α
n : ℕ
⊢ 1 < ↑n ↔ 1 < n

Tactic:
← cast_one,

Goal state after:
α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : AddLeftMono α
inst✝¹ : ZeroLEOneClass α
inst✝ : CharZero α
n : ℕ
⊢ ↑1 < ↑n ↔ 1 < n
Module: Mathlib.Data.Nat.Cast.Order.Basic

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

Tactic:
← cast_one,

Goal state after:
α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : AddLeftMono α
inst✝¹ : ZeroLEOneClass α
inst✝ : CharZero α
n : ℕ
⊢ ↑1 ≤ ↑n ↔ 1 ≤ n
Module: Mathlib.Data.Nat.Cast.Order.Basic

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : AddLeftMono α
inst✝¹ : ZeroLEOneClass α
inst✝ : CharZero α
n : ℕ
⊢ ↑n < 1 ↔ n = 0

Tactic:
← cast_one,

Goal state after:
α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : AddLeftMono α
inst✝¹ : ZeroLEOneClass α
inst✝ : CharZero α
n : ℕ
⊢ ↑n < ↑1 ↔ n = 0
Module: Mathlib.Data.Nat.Cast.Order.Basic

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

Tactic:
← cast_one,

Goal state after:
α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : AddLeftMono α
inst✝¹ : ZeroLEOneClass α
inst✝ : CharZero α
n : ℕ
⊢ ↑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:
rw [Int.neg_mul_neg]

Goal state after:
m n : ℕ
⊢ ↑((↑m).gcd -[n+1]) = ↑m * (↑m).gcdA -[n+1] + (↑n + 1) * (↑m).natAbs.gcdB n.succ
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:
rw [Int.neg_mul_neg]

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

Goal state before:
pp: case mp
a b : ℤ
n : ℕ
h : a.gcd b ∣ n
⊢ ∃ x y, a * (a.gcdA b * ↑(n / a.gcd b)) + b * (a.gcdB b * ↑(n / a.gcd b)) = a * x + b * y

Tactic:
exact ⟨_, _, rfl⟩

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

Goal state before:
pp: case neg.refine_1
α : Type u_1
inst✝ : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h✝¹ : ¬m = 0
h✝ : ¬n = 0
hb : ¬b = 0
ha : ¬a = 0
⊢ a ^ (↑m * m.gcdA n + ↑n * m.gcdB n) = (a ^ m.gcdB n * b ^ m.gcdA n) ^ n

Tactic:
simp only [zpow_add₀ ha, zpow_add₀ hb, ← zpow_natCast, (hab.zpow_zpow₀ _ _).mul_zpow,
      ← zpow_mul, mul_comm (Nat.gcdB m n), mul_comm (Nat.gcdA m n)]

Goal state after:
case neg.refine_1
α : Type u_1
inst✝ : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h✝¹ : ¬m = 0
h✝ : ¬n = 0
hb : ¬b = 0
ha : ¬a = 0
⊢ a ^ (↑m * m.gcdA n) * a ^ (↑n * m.gcdB n) = a ^ (↑n * m.gcdB n) * b ^ (↑n * m.gcdA n)