mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: case refine_1
α : Sort u_1
β : Sort u_2
f : α → β
γ : Type u_4
inst✝ : Nontrivial γ
not_surj : ¬Surjective f
inj : Injective fun g ↦ g ∘ f
c c' : γ
b₀ : β
hb : ¬∃ a, f a = b₀
a : α
⊢ (fun g ↦ g ∘ f) (fun x ↦ c) a = (fun g ↦ g ∘ f) (fun x ↦ if x = b₀ then c' else c) a

Tactic:
simp only [comp_apply, if_neg fun h ↦ hb ⟨a, h⟩]

Goal state after:
Module: Mathlib.Data.Subtype

Goal state before:
pp: α : Sort u_5
β : α → Type u_4
ne : ∀ (a : α), Nonempty (β a)
p : α → Prop
⊢ Surjective fun f ↦ restrict p f

Tactic:
by
  classical
  exact fun f ↦ ⟨fun x ↦ if h : p x then f ⟨x, h⟩ else Nonempty.some (ne x), by grind⟩

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case tail.single
α : Type u_1
r : α → α → Prop
a✝² b✝¹ c : α
h : ∀ (a b c : α), r a b → r a c → ∃ d, ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a✝² c
d e : α
a✝¹ : ReflTransGen r a✝² d
hde : r d e
b✝ f b : α
a✝ : ReflTransGen r d f
hfb : r f b
a : α
hea : ReflTransGen r e a
hfa : r f a
⊢ ∃ a, ReflTransGen r e a ∧ ReflGen r b a

Tactic:
| single hfa =>

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:
rw [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.Data.Option.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
h : α → β
f : γ → α
x : α
i : Option γ
⊢ (i.elim (h x) fun j ↦ h (f j)) = h (i.elim x f)

Tactic:
by cases i <;> rfl

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: case inl.inl.inl
α : Type u_2
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : x < y
h₂ : y < z
h₃ : x < z
⊢ False

pp: case inl.inl.inr
α : Type u_2
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : x < y
h₂ : y < z
h₃ : z < x
⊢ False

pp: case inl.inr.inl
α : Type u_2
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : x < y
h₂ : z < y
h₃ : x < z
⊢ False

pp: case inl.inr.inr
α : Type u_2
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : x < y
h₂ : z < y
h₃ : z < x
⊢ False

pp: case inr.inl.inl
α : Type u_2
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : y < x
h₂ : y < z
h₃ : x < z
⊢ False

pp: case inr.inl.inr
α : Type u_2
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : y < x
h₂ : y < z
h₃ : z < x
⊢ False

pp: case inr.inr.inl
α : Type u_2
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : y < x
h₂ : z < y
h₃ : x < z
⊢ False

pp: case inr.inr.inr
α : Type u_2
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : y < x
h₂ : z < y
h₃ : z < x
⊢ False

Tactic:
exacts [h h₁ h₂, h h₂ h₃, h h₃ h₂, h h₃ h₁, h h₁ h₃, h h₂ h₃, h h₁ h₃, h h₂ h₁]

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

Goal state before:
pp: case refl
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Injective next
x y : C n
H : leRecOn ⋯ (fun {k} ↦ next) x = leRecOn ⋯ (fun {k} ↦ next) y
⊢ x = y

Tactic:
leRecOn_self,

Goal state after:
case refl
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Injective next
x y : C n
H : x = leRecOn ⋯ (fun {k} ↦ next) y
⊢ x = y
Module: Mathlib.Order.Compare

Goal state before:
pp: case inr.inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, o.Compares a b → o.Compares a' b'
o : Ordering
ho : o.Compares a' b'
hab : a = b
⊢ o.Compares a b

Tactic:
have hab : Compares Ordering.eq a b := hab
    rwa [ho.inj (h hab)]

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : Subsingleton α
⊢ ComplementedLattice α

Tactic:
refine ⟨fun a ↦ ⟨⊥, disjoint_bot_right, ?_⟩⟩
  rw [Subsingleton.elim ⊥ ⊤]
  exact codisjoint_top_right

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Set α → Set β
hf : Injective f
h2 : f ∅ = ∅
s : Set α
⊢ f s ≠ ∅ ↔ s.Nonempty

Tactic:
← h2,

Goal state after:
α : Type u_1
β : Type u_2
f : Set α → Set β
hf : Injective f
h2 : f ∅ = ∅
s : Set α
⊢ f s ≠ f ∅ ↔ s.Nonempty
Module: Mathlib.Control.EquivFunctor

Goal state before:
pp: f : Type u₀ → Type u₁
inst✝¹ : Functor f
inst✝ : LawfulFunctor f
α : Type u₀
⊢ Functor.map ⇑(Equiv.refl α) = id

Tactic:
by
    ext
    apply LawfulFunctor.id_map

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
x : β
e : α ≃ { y // y ≠ x }
⊢ (fun e ↦ { toFun := fun a ↦ ⟨↑e (some a), ⋯⟩, invFun := fun b ↦ ((↑e).symm ↑b).get ⋯, left_inv := ⋯, right_inv := ⋯ })
      ((fun e ↦
          ⟨{ toFun := fun a ↦ a.casesOn' x (Subtype.val ∘ ⇑e),
              invFun := fun b ↦ if h : b = x then none else some (e.symm ⟨b, h⟩), left_inv := ⋯, right_inv := ⋯ },
            ⋯⟩)
        e) =
    e

Tactic:
ext a
    rfl

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

Goal state before:
pp: α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
hx : y ≤ x
hy : y ≠ ⊥
⊢ x \ y < x

Tactic:
refine sdiff_le.lt_of_ne fun h => hy ?_
  rw [sdiff_eq_left, disjoint_iff] at h
  rw [← h, inf_eq_right.mpr hx]

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

Goal state before:

Tactic:
x ⊓ y \ z ⊓ (z ⊓ x ⊔ x \ y) = x ⊓ y \ z ⊓ (z ⊓ x) ⊔ x ⊓ y \ z ⊓ x \ y := by rw [inf_sup_left]
      _ = x ⊓ (y \ z ⊓ z ⊓ x) ⊔ x ⊓ y \ z ⊓ x \ y := by ac_rfl
      _ = x ⊓ y \ z ⊓ x \ y := by rw [inf_sdiff_self_left, bot_inf_eq, inf_bot_eq, bot_sup_eq]
      _ = x ⊓ (y \ z ⊓ y) ⊓ x \ y := by conv_lhs => rw [← inf_sdiff_left]
      _ = x ⊓ (y \ z ⊓ (y ⊓ x \ y)) := by ac_rfl
      _ = ⊥ := by rw [inf_sdiff_self_right, inf_bot_eq, inf_bot_eq]

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

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

Tactic:
rw [inf_sdiff_self_right, inf_bot_eq, bot_inf_eq]

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

Tactic:
by
  rw [← sdiff_sup_cancel hyz]
  refine lt_of_le_not_ge (by grw [h]) fun h' => h.not_ge ?_
  rw [← sdiff_idem]
  exact (sdiff_le_sdiff_of_sup_le_sup_right h').trans sdiff_le

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
γ : (a : α) → β a → Type u_11
p : (a : α) × β a → Prop
uniq : Unique { ab // p ab }
a : α
b : β a
h : p ⟨a, b⟩
s : (a : α) × (b : β a) × γ a b
⊢ (match s with
    | ⟨a, ⟨b, c⟩⟩ => p ⟨a, b⟩) ↔
    p ((sigmaAssoc γ).symm s).fst

Tactic:
simp [sigmaAssoc]

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

Goal state before:
pp: case succ
α : Type u_1
f : α → α
n : ℕ
ih : preimage f^[n] = (preimage f)^[n]
⊢ preimage f^[n + 1] = (preimage f)^[n + 1]

Tactic:
rw [iterate_succ, iterate_succ', preimage_comp_eq, ih]

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

Goal state before:
pp: α : Type u_1
s t : Set α
h : Disjoint s t
⊢ (s ∪ t).offDiag = s.offDiag ∪ t.offDiag ∪ s ×ˢ t ∪ t ×ˢ s

Tactic:
ext x
  simp only [mem_offDiag, mem_union, ne_eq, mem_prod]
  constructor
  · rintro ⟨h0 | h0, h1 | h1, h2⟩ <;> simp [h0, h1, h2]
  · rintro (((⟨h0, h1, h2⟩ | ⟨h0, h1, h2⟩) | ⟨h0, h1⟩) | ⟨h0, h1⟩) <;>
      simp [*, h.ne_of_mem, Ne.symm]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), Nonempty (α i)
⊢ s.pi t = ∅ ↔ ∃ i, i ∈ s ∧ t i = ∅

Tactic:
simp [pi_eq_empty_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
h : InjOn f s
s₁ : Set α
hs₁ : s₁ ∈ 𝒫 s
s₂ : Set α
hs₂ : s₂ ∈ 𝒫 s
h' : f '' s₁ = f '' s₂
⊢ s₁ = s₂

Tactic:
by rw [← h.preimage_image_inter hs₁, h', h.preimage_image_inter hs₂]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
f : α → β
g₁ g₂ : β → γ
hf : EqOn (g₁ ∘ f) (g₂ ∘ f) s
hf' : SurjOn f s t
b : β
hb : b ∈ t
⊢ g₁ b = g₂ b

Tactic:
obtain ⟨a, ha, rfl⟩ := hf' hb

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
f : α → β
g₁ g₂ : β → γ
hf : EqOn (g₁ ∘ f) (g₂ ∘ f) s
hf' : SurjOn f s t
a : α
ha : a ∈ s
hb : f a ∈ t
⊢ g₁ (f a) = g₂ (f a)
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
h : Semiconj f fa fb
s : Set β
hb : InjOn fb s
hf : InjOn f (f ⁻¹' s)
⊢ InjOn fa (f ⁻¹' s)

Tactic:
intro x hx y hy H
  have := congr_arg f H
  rw [h.eq, h.eq] at this
  exact hf hx hy (hb hx hy this)

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a b : G
⊢ a / b = a ↔ b = 1

Tactic:
by rw [div_eq_mul_inv, mul_eq_left, inv_eq_one]

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

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

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

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✝ : G × H
⊢ x✝ ^ 0 = 1

Tactic:
ext <;> exact DivInvMonoid.zpow_zero' _

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:
by ext <;> exact DivInvMonoid.zpow_neg' ..

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

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoidWithOne R
m n : ℕ
⊢ ↑(m + n) = ↑m + ↑n

Tactic:
induction n with
  | zero => simp
  | succ n ih => rw [add_succ, cast_succ, ih, cast_succ, add_assoc]

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

Goal state before:
pp: case refine_3
m n✝ : ℤ
P : ℤ → Sort u_1
lt : (n : ℤ) → n < m → P n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → P k) → P n
n : ℤ
x✝¹ : n ≥ m
hn : m ≤ n
k : ℤ
hkm : k ≤ m
ih' :
  (∀ (k_1 : ℤ), k_1 < k → ∀ (hn : m ≤ k_1), Int.strongRec lt ge k_1 = ge k_1 hn fun k x ↦ Int.strongRec lt ge k) →
    (Int.inductionOn' (motive := fun x ↦ (k : ℤ) → k < x → P k) k m lt
        (fun _n a ih l a_1 ↦ if hlm : l < m then lt l hlm else ge l ⋯ fun k x ↦ ih k ⋯) fun n x hn l x_1 ↦ hn l ⋯) =
      fun k_1 x ↦ Int.strongRec lt ge k_1
x✝ : ∀ (k_1 : ℤ), k_1 < k - 1 → ∀ (hn : m ≤ k_1), Int.strongRec lt ge k_1 = ge k_1 hn fun k x ↦ Int.strongRec lt ge k
l : ℤ
hl : l < k - 1
⊢ ∀ (k_1 : ℤ), k_1 < k → ∀ (hn : m ≤ k_1), Int.strongRec lt ge k_1 = ge k_1 hn fun k x ↦ Int.strongRec lt ge k

Tactic:
exact fun l hlk hml ↦ (Int.not_lt.mpr hkm <| Int.lt_of_le_of_lt hml hlk).elim

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)
⊢ (↑f).toFun (x * y) = (↑f).toFun x * (↑f).toFun y

Tactic:
← sub_eq_zero,

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 * 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
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 : 2 * (f (x * y) - f x * f y) = 0
⊢ (↑f).toFun (x * y) = (↑f).toFun x * (↑f).toFun y

Tactic:
mul_eq_zero (M₀ := α),

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 : 2 = 0 ∨ f (x * y) - f x * f y = 0
⊢ (↑f).toFun (x * y) = (↑f).toFun x * (↑f).toFun y
Module: Mathlib.Algebra.Group.Commute.Units

Goal state before:
pp: M : Type u_1
inst✝ : DivisionMonoid M
a b c d : M
hbd : Commute b d
hb : IsUnit b
hd : IsUnit d
⊢ a * b⁻¹ = c * d⁻¹ ↔ a * d = c * b

Tactic:
by
  rw [← div_eq_mul_inv, ← div_eq_mul_inv, hbd.div_eq_div_iff_of_isUnit hb hd]

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

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
⊢ a / a = 1 → a ≠ 0

Tactic:
contrapose!

Goal state after:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
⊢ a = 0 → a / a ≠ 1
Module: Mathlib.Algebra.Ring.Commute

Goal state before:
pp: R : Type u
inst✝¹ : NonUnitalNonAssocRing R
inst✝ : NoZeroDivisors R
a b : R
h : Commute a b
⊢ a * a = b * b ↔ a = b ∨ a = -b

Tactic:
← sub_eq_zero,

Goal state after:
R : Type u
inst✝¹ : NonUnitalNonAssocRing R
inst✝ : NoZeroDivisors R
a b : R
h : Commute a b
⊢ a * a - b * b = 0 ↔ a = b ∨ a = -b
Module: Mathlib.Algebra.Ring.Commute

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
a b : R
inst✝ : NoZeroDivisors R
h : Commute a b
⊢ a ^ 2 = b ^ 2 ↔ a = b ∨ a = -b

Tactic:
← sub_eq_zero,

Goal state after:
R : Type u
inst✝¹ : Ring R
a b : R
inst✝ : NoZeroDivisors R
h : Commute a b
⊢ a ^ 2 - b ^ 2 = 0 ↔ a = b ∨ a = -b
Module: Mathlib.Data.Int.Cast.Lemmas

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

Tactic:
← sub_eq_zero,

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

Goal state before:
pp: α : Type u_3
inst✝ : NonAssocRing α
a : α
n : ℕ
⊢ ↑n • a = ↑↑n * a

Tactic:
rw [natCast_zsmul, nsmul_eq_mul, Int.cast_natCast]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DivisionMonoid α
inst✝ : HasDistribNeg α
n : ℤ
h : Even n
⊢ (-1) ^ n = 1

Tactic:
h.neg_zpow,

Goal state after:
α : Type u_2
inst✝¹ : DivisionMonoid α
inst✝ : HasDistribNeg α
n : ℤ
h : Even n
⊢ 1 ^ n = 1
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

Goal state before:
pp: α : Type u
inst✝² : CommGroup α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
a b c d : α
⊢ a / d < b / c → a < b ∨ c < d

Tactic:
contrapose!

Goal state after:
α : Type u
inst✝² : CommGroup α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
a b c d : α
⊢ b ≤ a ∧ d ≤ c → b / c ≤ a / d
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

Goal state before:
pp: α : Type u
inst✝³ : Group α
inst✝² : LinearOrder α
inst✝¹ : MulLeftMono α
a b : α
inst✝ : MulRightMono α
⊢ a / b ≤ a⁻¹ * b ↔ a ≤ b

Tactic:
rw [div_eq_mul_inv, mul_inv_le_inv_mul_iff]

Goal state after:
α : Type u
inst✝³ : Group α
inst✝² : LinearOrder α
inst✝¹ : MulLeftMono α
a b : α
inst✝ : MulRightMono α
⊢ a * a ≤ b * b ↔ a ≤ b
Module: Mathlib.Algebra.Order.Monoid.Defs

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
a : α
⊢ a * a ≤ 1 ↔ a ≤ 1

Tactic:
contrapose!

Goal state after:
α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
a : α
⊢ 1 < a * a ↔ 1 < a
Module: Mathlib.Algebra.Order.Monoid.Defs

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
a : α
⊢ a * a < 1 ↔ a < 1

Tactic:
contrapose!

Goal state after:
α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
a : α
⊢ 1 ≤ a * a ↔ 1 ≤ a
Module: Mathlib.Algebra.Order.Monoid.Unbundled.MinMax

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

Tactic:
contrapose!

Goal state after:
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : Mul α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a₁ a₂ b₁ b₂ : α
⊢ a₂ ≤ a₁ ∧ b₂ ≤ b₁ → a₂ * b₂ ≤ a₁ * b₁
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!

Goal state after:
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : Mul α
inst✝¹ : MulLeftMono α
inst✝ : MulRightStrictMono α
a₁ a₂ b₁ b₂ : α
⊢ a₂ < a₁ ∧ b₂ ≤ b₁ → a₂ * b₂ < a₁ * b₁
Module: Mathlib.Algebra.Order.Monoid.Unbundled.MinMax

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

Tactic:
contrapose!

Goal state after:
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : Mul α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightMono α
a₁ a₂ b₁ b₂ : α
⊢ a₂ ≤ a₁ ∧ b₂ < b₁ → a₂ * b₂ < a₁ * b₁
Module: Mathlib.Algebra.Order.Monoid.Unbundled.MinMax

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

Tactic:
contrapose!

Goal state after:
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : Mul α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a₁ a₂ b₁ b₂ : α
⊢ a₂ < a₁ ∧ b₂ < b₁ → a₂ * b₂ < a₁ * b₁
Module: Mathlib.Algebra.Order.Group.Defs

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

Tactic:
contrapose!

Goal state after:
α : Type u
inst✝² : CommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
a : α
⊢ a⁻¹ < a ↔ 1 < a
Module: Mathlib.Algebra.Order.Group.Defs

Goal state before:
pp: α : Type u
inst✝² : CommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
a : α
⊢ a < a⁻¹ ↔ a < 1

Tactic:
contrapose!

Goal state after:
α : Type u
inst✝² : CommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
a : α
⊢ a⁻¹ ≤ a ↔ 1 ≤ a
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:
by
  simpa only [pow_one] using pow_le_pow_right₀ ha <| Nat.pos_iff_ne_zero.2 hn

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

Goal state before:
pp: R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : PartialOrder R
a b c d : R
inst✝³ : ExistsAddOfLE R
inst✝² : MulPosMono R
inst✝¹ : AddLeftMono R
inst✝ : AddLeftReflectLE R
hab : a ≤ b
hcd : c ≤ d
⊢ a * d + b * c ≤ a * c + b * d

Tactic:
obtain ⟨d, hd, rfl⟩ := exists_nonneg_add_of_le hcd
  rw [mul_add, add_right_comm, mul_add, ← add_assoc]
  gcongr
  assumption

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

Goal state before:
pp: R : Type u
inst✝³ : Semiring R
inst✝² : LinearOrder R
a b : R
inst✝¹ : MulPosStrictMono R
inst✝ : PosMulStrictMono R
hab : 0 ≤ a * b
⊢ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0

Tactic:
refine Decidable.or_iff_not_not_and_not.2 ?_

Goal state after:
R : Type u
inst✝³ : Semiring R
inst✝² : LinearOrder R
a b : R
inst✝¹ : MulPosStrictMono R
inst✝ : PosMulStrictMono R
hab : 0 ≤ a * b
⊢ ¬(¬(0 ≤ a ∧ 0 ≤ b) ∧ ¬(a ≤ 0 ∧ b ≤ 0))
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: case a
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ a * b ≤ |a|ₘ * |b|ₘ

Tactic:
exact mul_le_mul' (le_mabs_self a) (le_mabs_self b)

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 c : α
this : DistribLattice α := CommGroup.toDistribLattice α
⊢ (b ⊔ a ⊔ c) * ((b ⊔ a) ⊓ c) / ((b ⊓ a ⊔ c) * (b ⊓ a ⊓ c)) = (b ⊔ a) * c / ((b ⊓ a) * c)

Tactic:
by
        rw [mul_comm, inf_mul_sup, mul_comm (b ⊓ a ⊔ c), inf_mul_sup]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DivisionMonoid α
inst✝ : HasDistribNeg α
n : ℤ
h : Odd n
⊢ (-1) ^ n = -1

Tactic:
h.neg_zpow,

Goal state after:
α : Type u_1
inst✝¹ : DivisionMonoid α
inst✝ : HasDistribNeg α
n : ℤ
h : Odd n
⊢ -1 ^ n = -1
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: case inr
α : Type u_1
inst✝³ : Group α
inst✝² : LinearOrder α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a b : α
ba : b ≤ a
⊢ 1 ≤ a / b

Tactic:
rwa [one_le_div']

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

Goal state before:
pp: q n : ℕ
dvd : gcd 0 q ∣ n
le : pred 0 * q.pred ≤ n
b : ℕ
eq : n = q * b
⊢ 0 * 0 + b * q = n

Tactic:
by simpa [mul_comm, eq_comm] using eq

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

Goal state before:
pp: n p : ℕ
dvd : (p + 1).gcd 0 ∣ n
le : (p + 1).pred * pred 0 ≤ n
a : ℕ
eq : n = (p.gcd 0 + 1).gcd 0 * a
⊢ a * (p + 1) + 0 * 0 = n

Tactic:
by simpa [mul_comm, eq_comm] using eq

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

Goal state before:
pp: α : Type u
inst✝³ : MulOneClass α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedMul α
a b : α
inst✝ : MulLeftStrictMono α
⊢ a < b ↔ ∃ c, c > 1 ∧ b = a * c

Tactic:
rw [lt_iff_le_and_ne, le_iff_exists_mul, ← exists_and_right]

Goal state after:
α : Type u
inst✝³ : MulOneClass α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedMul α
a b : α
inst✝ : MulLeftStrictMono α
⊢ (∃ x, b = a * x ∧ a ≠ b) ↔ ∃ c, c > 1 ∧ b = a * c
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 = (a ^ m.gcdB n * b ^ m.gcdA n) ^ n

Tactic:
· refine (pow_one _).symm.trans ?_
    conv_lhs => rw [← zpow_natCast, ← hmn, Nat.gcd_eq_gcd_ab]
    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)]
    simp only [zpow_mul, zpow_natCast, h]
    exact ((Commute.pow_pow (by aesop) _ _).zpow_zpow₀ _ _).symm

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

Goal state before:
pp: case neg.refine_2
α : 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
⊢ b = (a ^ m.gcdB n * b ^ m.gcdA n) ^ m

Tactic:
· refine (pow_one _).symm.trans ?_
    conv_lhs => rw [← zpow_natCast, ← hmn, Nat.gcd_eq_gcd_ab]
    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)]
    simp only [zpow_mul, zpow_natCast, h]
    exact ((Commute.pow_pow (by aesop) _ _).zpow_zpow₀ _ _).symm

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DivInvMonoid α
n : ℕ
⊢ none ^ ↑n.succ = none ^ ↑n * none

Tactic:
by change 0 ^ _ = 0 ^ _ * 0; simp only [mul_zero]; rfl

Goal state after: