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

Goal state before:
pp: n : Nat
⊢ bit (decide (n % 2 = 1)) (n >>> 1) = n

Tactic:
by
  simp only [bit, shiftRight_one]
  cases mod_two_eq_zero_or_one n with | _ h => simpa [h] using Nat.div_add_mod n 2

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a x y b : G
⊢ SemiconjBy (b * a * b⁻¹) (b * x * b⁻¹) (b * y * b⁻¹) ↔ SemiconjBy a x y

Tactic:
unfold SemiconjBy
  simp only [← mul_assoc, inv_mul_cancel_right]
  repeat rw [mul_assoc]
  rw [mul_left_cancel_iff, ← mul_assoc, ← mul_assoc, mul_right_cancel_iff]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: case pos
P Q R : Prop
inst✝ : Decidable P
p : P
⊢ (if P then Q else R) ↔ P ∧ Q ∨ ¬P ∧ R

Tactic:
simp [p]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: case neg
P Q R : Prop
inst✝ : Decidable P
p : ¬P
⊢ (if P then Q else R) ↔ P ∧ Q ∨ ¬P ∧ R

Tactic:
simp [p]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: case pos
P Q R : Prop
inst✝ : Decidable P
p : P
⊢ (if P then Q else R) ↔ (P → Q) ∧ (¬P → R)

Tactic:
simp [p]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: case neg
P Q R : Prop
inst✝ : Decidable P
p : ¬P
⊢ (if P then Q else R) ↔ (P → Q) ∧ (¬P → R)

Tactic:
simp [p]

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

Goal state before:
pp: α : Sort u_1
β : Sort u_2
f : α → β
⊢ ¬Injective f ↔ ∃ a b, f a = f b ∧ a ≠ b

Tactic:
by
  simp only [Injective, not_forall, exists_prop]

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

Goal state before:
pp: α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : α → γ
inst✝ : Nonempty γ
hf : FactorsThrough g f
x : α
⊢ g x = (extend f g (const β (Classical.arbitrary γ)) ∘ f) x

Tactic:
by simp only [comp_apply, hf.extend_apply]

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

Goal state before:
pp: case inr
n m : ℕ
h : m < n
⊢ n ∣ n - m ↔ m = 0 ∨ n ≤ m

Tactic:
· rcases eq_or_ne m 0 with rfl | hm
    · simp
    · simp only [hm, h.not_ge, or_self, iff_false]
      refine not_dvd_of_pos_of_lt ?_ ?_ <;>
      grind

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : γ → α
g : γ → β
⊢ (Monotone fun x ↦ (f x, g x)) ↔ Monotone f ∧ Monotone g

Tactic:
Monotone,

Goal state after:
α : Type u
β : Type v
γ : Type w
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : γ → α
g : γ → β
⊢ (∀ ⦃a b : γ⦄, a ≤ b → (f a, g a) ≤ (f b, g b)) ↔ (∀ ⦃a b : γ⦄, a ≤ b → f a ≤ f b) ∧ ∀ ⦃a b : γ⦄, a ≤ b → g a ≤ g b
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: f : ℕ → ℕ
b n : ℕ
hfmono : Monotone f
hfstab : ∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)
hbn : b ≤ n
hfb : ∀ (m : ℕ), m ≤ b → f m ≠ f (m + 1)
⊢ ∃ m, b < f m

Tactic:
let rec strictMono : ∀ m ≤ b + 1, m ≤ f m
    | 0, _ => Nat.zero_le _
    | m + 1, hmb => (strictMono _ <| m.le_succ.trans hmb).trans_lt <| (hfmono m.le_succ).lt_of_ne <|
        hfb _ <| Nat.le_of_succ_le_succ hmb

Goal state after:
f : ℕ → ℕ
b n : ℕ
hfmono : Monotone f
hfstab : ∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)
hbn : b ≤ n
hfb : ∀ (m : ℕ), m ≤ b → f m ≠ f (m + 1)
⊢ ∃ m, b < f m
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b c d : α
⊢ d ⊓ a ⊓ b ≤ c ↔ d ⊓ (a ⊓ b) ≤ c

Tactic:
inf_assoc

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

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b c : α
⊢ c ⊓ b ⊓ a ≤ c

Tactic:
inf_assoc

Goal state after:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b c : α
⊢ c ⊓ (b ⊓ a) ≤ c
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
β : Type u_1
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
a : α
⊢ a ⊓ a ⊓ a \ a ≤ a

Tactic:
inf_assoc

Goal state after:
α : Type u
β : Type u_1
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
a : α
⊢ a ⊓ (a ⊓ a \ a) ≤ a
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedCoheytingAlgebra α
a✝ b✝ c✝ d : α
a b c : αᵒᵈ
⊢ a ≤ toDual (ofDual c \ ofDual b) ↔ a ⊓ b ≤ c

Tactic:
rw [inf_comm]; exact sdiff_le_iff

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

Goal state before:
pp: α : Type u_2
inst✝ : HeytingAlgebra α
a b : α
⊢ a ⇨ bᶜ = b ⇨ aᶜ

Tactic:
simp_rw [← himp_bot, himp_left_comm]

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

Goal state before:
pp: ι : Type u_1
α✝ : Type u_2
β : Type u_3
inst✝¹ : HeytingAlgebra α✝
a✝ b✝ : α✝
α : Type u_2
inst✝ : CoheytingAlgebra α
a b c : αᵒᵈ
⊢ a ≤ toDual (ofDual c \ ofDual b) ↔ a ⊓ b ≤ c

Tactic:
rw [inf_comm]; exact sdiff_le_iff

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

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hx : x ≤ z
hy : y ≤ z
h : z \ x ≤ z \ y
⊢ y ≤ x

Tactic:
← sdiff_sdiff_eq_self hx,

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hx : x ≤ z
hy : y ≤ z
h : z \ x ≤ z \ y
⊢ y ≤ z \ (z \ x)
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
p : α → Prop
q : Subtype p → Prop
a : Subtype q
⊢ q ⟨↑↑a, ⋯⟩

Tactic:
rcases a with ⟨⟨a, hap⟩, haq⟩

Goal state after:
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
p : α → Prop
q : Subtype p → Prop
a : α
hap : p a
haq : q ⟨a, hap⟩
⊢ q ⟨↑↑⟨⟨a, hap⟩, haq⟩, ⋯⟩
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: case e_a
α : Type u_2
inst✝ : BooleanAlgebra α
a b c : α
⊢ aᶜ ⊓ (b ⊓ cᶜ) = aᶜ ⊓ b ⊓ cᶜ

Tactic:
inf_assoc

Goal state after:
case e_a
α : Type u_2
inst✝ : BooleanAlgebra α
a b c : α
⊢ aᶜ ⊓ (b ⊓ cᶜ) = aᶜ ⊓ (b ⊓ cᶜ)
Module: Mathlib.Data.Set.Restrict

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : MapsTo f s t
⊢ Surjective (restrict f s t h) ↔ SurjOn f s t

Tactic:
by
  refine ⟨fun h' b hb ↦ ?_, fun h' ⟨b, hb⟩ ↦ ?_⟩
  · obtain ⟨⟨a, ha⟩, ha'⟩ := h' ⟨b, hb⟩
    replace ha' : f a = b := by simpa [Subtype.ext_iff] using ha'
    rw [← ha']
    exact mem_image_of_mem f ha
  · obtain ⟨a, ha, rfl⟩ := h' hb
    exact ⟨⟨a, ha⟩, rfl⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
⊢ Sum.inr ⁻¹' range Sum.inl = ∅

Tactic:
by
  rw [← image_univ, preimage_inr_image_inl]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s : Set ι
i : ι
inst✝ : DecidableEq ι
hi : i ∈ s
f : (j : ι) → α j
a : α i
t : (j : ι) → α j → Set (β j)
⊢ (({i} ∪ s \ {i}).pi fun j ↦ t j (update f i a j)) = {x | x i ∈ t i a} ∩ (s \ {i}).pi fun j ↦ t j (f j)

Tactic:
rw [union_pi, singleton_pi', update_self, pi_update_of_notMem]

Goal state after:
case hi
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s : Set ι
i : ι
inst✝ : DecidableEq ι
hi : i ∈ s
f : (j : ι) → α j
a : α i
t : (j : ι) → α j → Set (β j)
⊢ ¬i ∈ s \ {i}
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u
β : Type v
f : α → β
hf : Bijective f
s : Set β
t : Set α
⊢ f ⁻¹' s = t ↔ s = f '' t

Tactic:
← image_eq_image hf.1,

Goal state after:
α : Type u
β : Type v
f : α → β
hf : Bijective f
s : Set β
t : Set α
⊢ f '' f ⁻¹' s = f '' t ↔ s = f '' t
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u
β : Type v
f : α → β
hf : Bijective f
s : Set α
t : Set β
⊢ s = f ⁻¹' t ↔ f '' s = t

Tactic:
← image_eq_image hf.1,

Goal state after:
α : Type u
β : Type v
f : α → β
hf : Bijective f
s : Set α
t : Set β
⊢ f '' s = f '' f ⁻¹' t ↔ f '' s = t
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
t : (i : ι) → Set (α i)
a : (i : ι) → α i
x✝ : a ∈ univ.pi t ∧ ∀ (x : (i : ι) → α i), x ∈ univ.pi t → x = a
i : ι
h₁ : a ∈ univ.pi t
h₂ : ∀ (x : (i : ι) → α i), x ∈ univ.pi t → x = a
x : α i
hx : x ∈ t i
⊢ x = a i

Tactic:
rw [← h₂ _ fun j _ => (update_mem_pi_iff_of_mem h₁).mpr (fun _ => hx) j trivial, update_self]

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

Goal state before:
pp: M : Type u_4
N : Type u_5
F : Type u_9
inst✝⁴ : One M
inst✝³ : One N
inst✝² : FunLike F M N
inst✝¹ : Subsingleton M
inst✝ : OneHomClass F M N
f g : F
x : M
⊢ f x = g x

Tactic:
by simp [Subsingleton.elim x 1]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf₂ : Surjective (Prod.snd ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
e₁ : β → γ
he₁ : range f = graphOn e₁ univ
e₂ : γ → β
he₂ : range (⇑(Equiv.prodComm β γ) ∘ f) = graphOn e₂ univ
he₁₂ : ∀ (h : β) (i : γ), e₁ h = i ↔ e₂ i = h
i : γ
⊢ e₁ (e₂ i) = i

Tactic:
by rw [he₁₂]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
inst✝ : Nonempty α
h : s ⊆ invFunOn f s '' f '' s
x : α
hx' : x ∈ s
hx : invFunOn f s (f x) ∈ s
⊢ invFunOn f s (f (invFunOn f s (f x))) = invFunOn f s (f x)

Tactic:
rw [invFunOn_apply_eq (f := f) hx']

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
r : Set α
hinj : InjOn f r
hrs : r ⊆ s
⊢ ∃ u, r ⊆ u ∧ u ⊆ s ∧ f '' u = f '' s ∧ InjOn f u

Tactic:
by
  obtain ⟨u, hru, hus, h⟩ := hinj.bijOn_image.exists_extend_of_subset hrs
    (image_mono hrs) Subset.rfl
  exact ⟨u, hru, hus, h.image_eq, h.injOn⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : Mul α
a x y : αᵐᵒᵖ
| SemiconjBy a x y

Tactic:
rw [← op_unop a, ← op_unop x, ← op_unop y, semiconjBy_op]

Goal state after:
α : Type u_1
inst✝ : Mul α
a x y : αᵐᵒᵖ
| SemiconjBy (unop a) (unop y) (unop x)
Module: Mathlib.Algebra.Group.InjSurj

Goal state before:
pp: M₁ : Type u_1
M₂ : Type u_2
inst✝⁶ : Mul M₁
inst✝⁵ : One M₁
inst✝⁴ : Pow M₁ ℕ
inst✝³ : Inv M₁
inst✝² : Div M₁
inst✝¹ : Pow M₁ ℤ
inst✝ : DivisionMonoid M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
x y : M₁
⊢ (f y)⁻¹ * (f x)⁻¹ = (f y)⁻¹ * f x⁻¹

Tactic:
inv

Goal state after:
M₁ : Type u_1
M₂ : Type u_2
inst✝⁶ : Mul M₁
inst✝⁵ : One M₁
inst✝⁴ : Pow M₁ ℕ
inst✝³ : Inv M₁
inst✝² : Div M₁
inst✝¹ : Pow M₁ ℤ
inst✝ : DivisionMonoid M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
x y : M₁
⊢ (f y)⁻¹ * (f x)⁻¹ = (f y)⁻¹ * (f x)⁻¹
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a b c : G
h : a = c * b
⊢ a * b⁻¹ = c

Tactic:
rw [h, mul_inv_cancel_right]

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a b c : G
h : a = c * b
⊢ a * b⁻¹ = c

Tactic:
by rw [h, mul_inv_cancel_right]

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

Goal state before:
pp: α : Type u
inst✝ : Monoid α
a : αˣ
⊢ ↑a = 1 ↔ a = 1

Tactic:
rw [← Units.val_one, val_inj]

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

Goal state before:
pp: α : Type u
inst✝ : Monoid α
x : α
u₁ u₂ : αˣ
⊢ x /ₚ u₁ /ₚ u₂ = x /ₚ (u₂ * u₁)

Tactic:
by
  simp only [divp, mul_inv_rev, Units.val_mul, mul_assoc]

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

Goal state before:
pp: M₁ : Type u_1
M₂ : Type u_2
inst✝⁶ : Mul M₂
inst✝⁵ : One M₂
inst✝⁴ : Pow M₂ ℕ
inst✝³ : Inv M₂
inst✝² : Div M₂
inst✝¹ : Pow M₂ ℤ
inst✝ : DivInvMonoid M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
n : ℕ
x : M₁
⊢ f (x ^ (n + 1))⁻¹ = (f (x ^ n.succ))⁻¹

Tactic:
inv

Goal state after:
M₁ : Type u_1
M₂ : Type u_2
inst✝⁶ : Mul M₂
inst✝⁵ : One M₂
inst✝⁴ : Pow M₂ ℕ
inst✝³ : Inv M₂
inst✝² : Div M₂
inst✝¹ : Pow M₂ ℤ
inst✝ : DivInvMonoid M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
n : ℕ
x : M₁
⊢ (f (x ^ (n + 1)))⁻¹ = (f (x ^ n.succ))⁻¹
Module: Mathlib.Algebra.Group.Units.Basic

Goal state before:
pp: α : Type u
inst✝ : Monoid α
b : αˣ
a c : α
h : a = c * ↑b
⊢ a * ↑b⁻¹ = c

Tactic:
rw [h, mul_inv_cancel_right]

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

Goal state before:
pp: α : Type u
inst✝ : Monoid α
b : αˣ
a c : α
h : a = c * ↑b
⊢ a * ↑b⁻¹ = c

Tactic:
by rw [h, mul_inv_cancel_right]

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✝¹ : CancelMonoid M
inst✝ : CancelMonoid N
x✝¹ x✝ : M × N
⊢ ∀ ⦃a₂ : M × N⦄, (fun x ↦ x * x✝¹) x✝ = (fun x ↦ x * x✝¹) a₂ → x✝ = a₂

Tactic:
by simp only [mul_left_inj, imp_self, forall_const]

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

Goal state before:
pp: M₀ : Type u_1
inst✝ : MonoidWithZero M₀
a b : M₀
m n : ℕ
hmn : m ≤ n
h : a ^ m * b = 0
⊢ a ^ n * b = 0

Tactic:
rw [show n = n - m + m by lia, pow_add, mul_assoc, h]
  simp

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : FunLike F α β
inst✝¹ : ZeroHomClass F α β
a : α
f : F
hf : Injective ⇑f
inst✝ : NeZero a
⊢ f a ≠ 0

Tactic:
rw [← ZeroHomClass.map_zero f]

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : FunLike F α β
inst✝¹ : ZeroHomClass F α β
a : α
f : F
hf : Injective ⇑f
inst✝ : NeZero a
⊢ f a ≠ f 0
Module: Mathlib.Data.Nat.Sqrt

Goal state before:
pp: m n : ℕ
⊢ m ^ 2 < n → n < (m + 1) ^ 2 → ¬∃ t, t ^ 2 = n

Tactic:
by
  simpa only [Nat.pow_two] using not_exists_sq

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

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

Tactic:
rw [neg_eq_neg_one_mul, mul_div_assoc, ← neg_eq_neg_one_mul]

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

Goal state before:
pp: case neg.inr
M₀ : Type u_1
inst✝ : MonoidWithZero M₀
a b : M₀
h : Commute a b
hab : ¬IsUnit (a * b)
hb : ¬IsUnit b
⊢ 0 = b⁻¹ʳ * a⁻¹ʳ

Tactic:
inverse_non_unit _ hb,

Goal state after:
case neg.inr
M₀ : Type u_1
inst✝ : MonoidWithZero M₀
a b : M₀
h : Commute a b
hab : ¬IsUnit (a * b)
hb : ¬IsUnit b
⊢ 0 = 0 * a⁻¹ʳ
Module: Mathlib.Algebra.Module.NatInt

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : M
⊢ ↑0 • a = 0

Tactic:
Int.cast_zero

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : M
⊢ 0 • a = 0
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝² : Add α
inst✝¹ : Mul α
a : α
inst✝ : LeftDistribClass α
ha : Even a
b : α
⊢ Even (b * a)

Tactic:
by
  rcases ha with ⟨k, rfl⟩
  use b * k
  rw [mul_add]

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

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulRightMono α
a b : α
⊢ 1 ≤ a / b ↔ b ≤ a

Tactic:
by
  rw [← mul_le_mul_iff_right b, one_mul, div_eq_mul_inv, inv_mul_cancel_right]

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

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulRightMono α
a b : α
⊢ a / b ≤ 1 ↔ a ≤ b

Tactic:
by
  rw [← mul_le_mul_iff_right b, one_mul, div_eq_mul_inv, inv_mul_cancel_right]

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

Goal state before:
pp: α : Type u_1
inst✝³ : Mul α
inst✝² : LinearOrder α
a b c d : α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
h : a * b = c * d
⊢ a = c ∧ b = d ∨ a < c ∨ b < d

Tactic:
obtain hac | rfl | hca := lt_trichotomy a c
  · grind
  · left; simpa using mul_right_inj_of_comparable (le_total d b) |>.1 h
  · obtain hbd | rfl | hdb := lt_trichotomy b d
    · grind
    · exact False.elim <| ne_of_lt (mul_lt_mul_left hca b) h.symm
    · exact False.elim <| ne_of_lt (mul_lt_mul_of_lt_of_lt hca hdb) h.symm

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₀
⊢ 0 < a⁻¹ ↔ 0 < a

Tactic:
suffices ∀ a : G₀, 0 < a → 0 < a⁻¹ from ⟨fun h ↦ inv_inv a ▸ this _ h, this a⟩
  intro a ha
  apply lt_of_mul_lt_mul_left _ ha.le
  apply lt_of_mul_lt_mul_left _ ha.le
  simpa [ha.ne']

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
ab : 0 ≤ a → b < 0
⊢ ¬(a ≤ 0 → 0 < b)

Tactic:
nab

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
ab : 0 ≤ a → b < 0
nab : a ≤ 0 → 0 < b
⊢ False
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
f g : r →r s
h : (fun o ↦ o.toFun) f = (fun o ↦ o.toFun) g
⊢ f = g

Tactic:
by
    cases f
    cases g
    congr

Goal state after:
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:
rw [div_lt_iff₀ hb, ← mul_div_right_comm, lt_div_iff₀ hd]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
x : α
y : β
⊢ r x (e.symm y) ↔ s (e x) y

Tactic:
← e.map_rel_iff,

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
x : α
y : β
⊢ s (e x) (e (e.symm y)) ↔ s (e x) y
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
x : β
y : α
⊢ r (e.symm x) y ↔ s x (e y)

Tactic:
← e.map_rel_iff,

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
x : β
y : α
⊢ s (e (e.symm x)) (e y) ↔ s x (e y)
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 β
f : α →o β
g : β →o α
h₁ : f.comp g = OrderHom.id
h₂ : g.comp f = OrderHom.id
a✝ b✝ : α
h :
  { toFun := ⇑f, invFun := ⇑g, left_inv := ⋯, right_inv := ⋯ } a✝ ≤
    { toFun := ⇑f, invFun := ⇑g, left_inv := ⋯, right_inv := ⋯ } b✝
⊢ a✝ ≤ b✝

Tactic:
simpa [h₂] using show g.comp f _ ≤ g.comp f _ from map_rel g h

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

Goal state before:
pp: case inl.inr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
hab : a ≤ b
ha : 1 ≤ a
hb : b < 1
⊢ |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1

pp: case inr.inl
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
hab : a ≤ b
ha : a < 1
hb : 1 ≤ b
⊢ |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1

pp: case inr.inr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
hab : a ≤ b
ha : a < 1
hb : b < 1
⊢ |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1

Tactic:
· exact (lt_irrefl (1 : G) <| ha.trans_lt <| hab.trans_lt hb).elim

Goal state after:
case inr.inl
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
hab : a ≤ b
ha : a < 1
hb : 1 ≤ b
⊢ |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1

case inr.inr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
hab : a ≤ b
ha : a < 1
hb : b < 1
⊢ |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow

Goal state before:
pp: β : Type u_1
M : Type u_3
inst✝⁴ : Monoid M
inst✝³ : Preorder M
inst✝² : Preorder β
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
f : β → M
hf : Monotone f
n : ℕ
⊢ Monotone fun a ↦ f a ^ n * f a

Tactic:
exact (Monotone.pow_const hf _).mul' hf

Goal state after:
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 c : G
⊢ a < b * c ∧ b < a * c ↔ a < b * c ∧ b / a < c

Tactic:
div_lt_iff_lt_mul'

Goal state after:
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b c : G
⊢ a < b * c ∧ b < a * c ↔ a < b * c ∧ b < a * c
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 c : G
⊢ |a * b|ₘ * |c|ₘ ≤ |a|ₘ * |b|ₘ * |c|ₘ

Tactic:
mabs_mul_le

Goal state after:
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b c : G
⊢ |a|ₘ * |b|ₘ * |c|ₘ ≤ |a|ₘ * |b|ₘ * |c|ₘ
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) * (((b ⊔ a) ⊓ c) / (b ⊓ a ⊓ c))

Tactic:
inf_assoc

Goal state after:
α : 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) * (((b ⊔ a) ⊓ c) / (b ⊓ (a ⊓ c)))
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: s t : ℤ
r' : ℕ
s' t' : ℤ
⊢ xgcdAux 0 s t r' s' t' = (r', s', t')

Tactic:
xgcdAux,

Goal state after:
s t : ℤ
r' : ℕ
s' t' : ℤ
⊢ Nat.strongRec (motive := fun x ↦ ℤ → ℤ → ℕ → ℤ → ℤ → ℕ × ℤ × ℤ)
      (fun n ih s t r' s' t' ↦
        match n, ih with
        | 0, ih => (r', s', t')
        | k.succ, ih =>
          have q := r' / k.succ;
          ih (r' % k.succ) ⋯ (s' - ↑q * s) (t' - ↑q * t) k.succ s t)
      0 s t r' s' t' =
    (r', s', t')
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: s t : ℤ
r' : ℕ
s' t' : ℤ
r : ℕ
h : 0 < r.succ
⊢ r.succ.xgcdAux s t r' s' t' = (r' % r.succ).xgcdAux (s' - ↑r' / ↑r.succ * s) (t' - ↑r' / ↑r.succ * t) r.succ s t

Tactic:
xgcdAux,

Goal state after:
s t : ℤ
r' : ℕ
s' t' : ℤ
r : ℕ
h : 0 < r.succ
⊢ Nat.strongRec (motive := fun x ↦ ℤ → ℤ → ℕ → ℤ → ℤ → ℕ × ℤ × ℤ)
      (fun n ih s t r' s' t' ↦
        match n, ih with
        | 0, ih => (r', s', t')
        | k.succ, ih =>
          have q := r' / k.succ;
          ih (r' % k.succ) ⋯ (s' - ↑q * s) (t' - ↑q * t) k.succ s t)
      r.succ s t r' s' t' =
    (r' % r.succ).xgcdAux (s' - ↑r' / ↑r.succ * s) (t' - ↑r' / ↑r.succ * t) r.succ s t
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: s : ℕ
⊢ (xgcdAux 0 1 0 s 0 1).2.1 = 0

Tactic:
xgcdAux,

Goal state after:
s : ℕ
⊢ (Nat.strongRec (motive := fun x ↦ ℤ → ℤ → ℕ → ℤ → ℤ → ℕ × ℤ × ℤ)
          (fun n ih s t r' s' t' ↦
            match n, ih with
            | 0, ih => (r', s', t')
            | k.succ, ih =>
              have q := r' / k.succ;
              ih (r' % k.succ) ⋯ (s' - ↑q * s) (t' - ↑q * t) k.succ s t)
          0 1 0 s 0 1).2.1 =
    0
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: s : ℕ
⊢ (xgcdAux 0 1 0 s 0 1).2.2 = 1

Tactic:
xgcdAux,

Goal state after:
s : ℕ
⊢ (Nat.strongRec (motive := fun x ↦ ℤ → ℤ → ℕ → ℤ → ℤ → ℕ × ℤ × ℤ)
          (fun n ih s t r' s' t' ↦
            match n, ih with
            | 0, ih => (r', s', t')
            | k.succ, ih =>
              have q := r' / k.succ;
              ih (r' % k.succ) ⋯ (s' - ↑q * s) (t' - ↑q * t) k.succ s t)
          0 1 0 s 0 1).2.2 =
    1