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)
b : Bool
n : Nat
h : n ≠ 0
⊢ binaryRecFromOne zero one bit (Nat.bit b n) = bit b n h (binaryRecFromOne zero one bit n)

Tactic:
by
  rw [binaryRecFromOne, binaryRec'_eq _ _ (by simp [h]), dif_neg h, binaryRecFromOne]

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

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : Nontrivial α
inst✝ : DecidableEq α
x y y' : α
h : y ≠ y'
hx : ¬x = y
⊢ ∃ y, y ≠ x

Tactic:
exact ⟨y, Ne.symm hx⟩

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
b c : α
h : ∀ {a : α}, a = b ↔ a = c
⊢ b = c

Tactic:
rw [← h]

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a b c : α
hab : ReflTransGen r a b
hbc : r b c
⊢ TransGen r a c

Tactic:
induction hab generalizing c with
  | refl => exact single hbc
  | tail _ hdb IH => exact tail (IH hdb) hbc

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case single
α : Type u_1
r : α → α → Prop
a b c : α
hab : ReflTransGen r a b
b✝ : α
hbc : r b b✝
⊢ TransGen r a b✝

Tactic:
| single hbc =>

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

Goal state before:
pp: case pos
ι : Type u_1
M : ι → Type u_6
N : ι → Type u_7
O : ι → Type u_8
inst✝³ : (i : ι) → One (M i)
inst✝² : (i : ι) → One (N i)
inst✝¹ : (i : ι) → One (O i)
inst✝ : DecidableEq ι
f' : (i : ι) → M i → N i → O i
hf' : ∀ (i : ι), f' i 1 1 = 1
j : ι
x : M j
y : N j
⊢ f' j (mulSingle j x j) (mulSingle j y j) = mulSingle j (f' j x y) j

Tactic:
simp only [mulSingle_eq_same]

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
motive : α → Prop
ha : a ≤ b → motive a
hb : b ≤ a → motive b
⊢ motive (min a b)

Tactic:
rw [min_def]

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b : α
motive : α → Prop
ha : a ≤ b → motive a
hb : b ≤ a → motive b
⊢ motive (if a ≤ b then a else b)
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ min a b ≤ a

Tactic:
rw [min_def]

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ (if a ≤ b then a else b) ≤ a
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ min a b ≤ b

Tactic:
rw [min_def]

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ (if a ≤ b then a else b) ≤ b
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : α
h₁ : c ≤ a
h₂ : c ≤ b
⊢ c ≤ min a b

Tactic:
rw [min_def]

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h₁ : c ≤ a
h₂ : c ≤ b
⊢ c ≤ if a ≤ b then a else b
Module: Mathlib.Order.Basic

Goal state before:
pp: case inl
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : DenselyOrdered α
inst✝ : DenselyOrdered β
a b : α × β
h₁ : a.fst < b.fst
h₂ : a.snd ≤ b.snd
⊢ ∃ a_1,
    (a.fst < a_1.fst ∧ a.snd ≤ a_1.snd ∨ a.fst ≤ a_1.fst ∧ a.snd < a_1.snd) ∧
      (a_1.fst < b.fst ∧ a_1.snd ≤ b.snd ∨ a_1.fst ≤ b.fst ∧ a_1.snd < b.snd)

Tactic:
obtain ⟨c, ha, hb⟩ := exists_between h₁

Goal state after:
case inl
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : DenselyOrdered α
inst✝ : DenselyOrdered β
a b : α × β
h₁ : a.fst < b.fst
h₂ : a.snd ≤ b.snd
c : α
ha : a.fst < c
hb : c < b.fst
⊢ ∃ a_1,
    (a.fst < a_1.fst ∧ a.snd ≤ a_1.snd ∨ a.fst ≤ a_1.fst ∧ a.snd < a_1.snd) ∧
      (a_1.fst < b.fst ∧ a_1.snd ≤ b.snd ∨ a_1.fst ≤ b.fst ∧ a_1.snd < b.snd)
Module: Mathlib.Order.Disjoint

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

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

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

Goal state before:
pp: α : Type u_1
s t : Set α
p : α → Prop
hst : s ⊆ t
⊢ s ∩ {a | p a} = s ∩ t ∩ {a | p a}

Tactic:
← left_eq_inter.mpr hst

Goal state after:
α : Type u_1
s t : Set α
p : α → Prop
hst : s ⊆ t
⊢ s ∩ {a | p a} = s ∩ {a | p a}
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).Nonempty ↔ s.Nonempty

Tactic:
by
  rw [nonempty_iff_ne_empty, ← h2, nonempty_iff_ne_empty, hf.ne_iff]

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

Goal state before:
pp: α : Type u_1
s : Set α
a : α
⊢ (s ∩ {a}).Nonempty ↔ a ∈ s

Tactic:
rw [inter_comm, singleton_inter_nonempty]

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : Max α
inst✝² : LE α
inst✝¹ : LT α
inst✝ : SemilatticeSup β
f : α → β
hf_inj : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
a b : α
⊢ f a ≤ f (a ⊔ b)

Tactic:
map_sup

Goal state after:
α : Type u
β : Type v
inst✝³ : Max α
inst✝² : LE α
inst✝¹ : LT α
inst✝ : SemilatticeSup β
f : α → β
hf_inj : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
a b : α
⊢ f a ≤ f a ⊔ f b
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : Max α
inst✝² : LE α
inst✝¹ : LT α
inst✝ : SemilatticeSup β
f : α → β
hf_inj : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
a b : α
⊢ f b ≤ f (a ⊔ b)

Tactic:
map_sup

Goal state after:
α : Type u
β : Type v
inst✝³ : Max α
inst✝² : LE α
inst✝¹ : LT α
inst✝ : SemilatticeSup β
f : α → β
hf_inj : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
a b : α
⊢ f b ≤ f a ⊔ f b
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : Max α
inst✝² : LE α
inst✝¹ : LT α
inst✝ : SemilatticeSup β
f : α → β
hf_inj : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
a b c : α
ha : f a ≤ f c
hb : f b ≤ f c
⊢ f (a ⊔ b) ≤ f c

Tactic:
map_sup

Goal state after:
α : Type u
β : Type v
inst✝³ : Max α
inst✝² : LE α
inst✝¹ : LT α
inst✝ : SemilatticeSup β
f : α → β
hf_inj : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
a b c : α
ha : f a ≤ f c
hb : f b ≤ f c
⊢ f a ⊔ f b ≤ f c
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b : α
h : Codisjoint a b
⊢ b ⇨ a = a ⊔ b ⇨ a

Tactic:
sup_himp_self_left

Goal state after:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b : α
h : Codisjoint a b
⊢ b ⇨ a = b ⇨ a
Module: Mathlib.Logic.Equiv.Option

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
x : β
e : { e // e none = x }
a : α
⊢ some ((fun b ↦ ((↑e).symm ↑b).get ⋯) ((fun a ↦ ⟨↑e (some a), ⋯⟩) a)) = some a

Tactic:
some_get

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
x : β
e : { e // e none = x }
a : α
⊢ (↑e).symm ↑((fun a ↦ ⟨↑e (some a), ⋯⟩) a) = some a
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : Disjoint z (y \ x)
⊢ z ⊔ y ≤ y

Tactic:
rw [sup_eq_right.2 hz]

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

Goal state before:
pp: α : Type u
x y : α
inst✝ : BooleanAlgebra α
h : xᶜ = y
⊢ IsCompl x y

Tactic:
rw [← h]

Goal state after:
α : Type u
x y : α
inst✝ : BooleanAlgebra α
h : xᶜ = y
⊢ IsCompl x xᶜ
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
a b c : α
⊢ a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ aᶜ ⊓ b ⊓ cᶜ ⊔ aᶜ ⊓ bᶜ ⊓ c

Tactic:
by
      congr 1
      · congr 1
        rw [inf_comm, inf_assoc]
      · apply inf_left_right_swap

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
g' : β → γ
y : β
h : ∃ a, f a = y
⊢ g (Classical.choose h) ∈ range g ∪ g' '' (range f)ᶜ

pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
g' : β → γ
y : β
h : ¬∃ a, f a = y
⊢ g' y ∈ range g ∪ g' '' (range f)ᶜ

Tactic:
exacts [Or.inl (mem_range_self _), Or.inr (mem_image_of_mem _ h)]

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:
disjoint_image_left

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
⊢ Disjoint s (f ⁻¹' t) ↔ Disjoint s (f ⁻¹' t)
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
x : ↑(range f)
⊢ rangeFactorization f (rangeSplitting f x) = x

Tactic:
by
  ext
  simp only [rangeFactorization_coe]
  apply apply_rangeSplitting

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✝ : DecidableEq ι
a : (i : ι) → α i
i : ι
b : α i
ha : a ∈ s.pi t
⊢ a ∈ (s \ {i}).pi t

Tactic:
exact fun j hj => ha j hj.1

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
f : ι' ≃ ι
s : Set ι'
t : (i : ι) → Set (α i)
⊢ ⇑(piCongrLeft α f) ⁻¹' (⇑f '' s).pi t = s.pi fun i ↦ t (f i)

Tactic:
by
  apply Set.ext
  rw [← (f.piCongrLeft α).symm.forall_congr_right]
  simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
t : Set α
h : InjOn f s
⊢ f '' (s \ t) = f '' s \ f '' (s ∩ t)

Tactic:
refine subset_antisymm (subset_sdiff.2 ⟨image_mono sdiff_subset, ?_⟩)
    (sdiff_subset_iff.2 (by rw [← image_union, inter_union_sdiff]))

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
t : Set α
h : InjOn f s
⊢ Disjoint (f '' (s \ t)) (f '' (s ∩ t))
Module: Mathlib.Algebra.Group.InjSurj

Goal state before:
pp: M₁ : Type u_1
M₂ : Type u_2
inst✝² : Mul M₁
inst✝¹ : One M₁
inst✝ : MulOneClass M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
x : M₁
⊢ f 1 * f x = f x

Tactic:
one,

Goal state after:
M₁ : Type u_1
M₂ : Type u_2
inst✝² : Mul M₁
inst✝¹ : One M₁
inst✝ : MulOneClass M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
x : M₁
⊢ 1 * f x = f 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✝ : MulOneClass M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
x : M₁
⊢ f x * f 1 = f x

Tactic:
one,

Goal state after:
M₁ : Type u_1
M₂ : Type u_2
inst✝² : Mul M₁
inst✝¹ : One M₁
inst✝ : MulOneClass M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
x : M₁
⊢ f x * 1 = f 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✝ : Monoid M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
x : M₁
⊢ f x ^ 0 = f 1

Tactic:
one,

Goal state after:
M₁ : Type u_1
M₂ : Type u_2
inst✝³ : Mul M₁
inst✝² : One M₁
inst✝¹ : Pow M₁ ℕ
inst✝ : Monoid M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
x : M₁
⊢ f x ^ 0 = 1
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✝ : InvOneClass M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
⊢ (f 1)⁻¹ = f 1

Tactic:
one,

Goal state after:
M₁ : Type u_1
M₂ : Type u_2
inst✝⁴ : Mul M₁
inst✝³ : One M₁
inst✝² : Pow M₁ ℕ
inst✝¹ : Inv M₁
inst✝ : InvOneClass M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
⊢ 1⁻¹ = 1
Module: Mathlib.Algebra.Group.End

Goal state before:
pp: case right
α : Type u_7
β : Type u_8
fst✝¹ : Perm α
snd✝¹ : Perm β
fst✝ : Perm α
snd✝ : Perm β
h : (sumCongrHom α β) (fst✝¹, snd✝¹) = (sumCongrHom α β) (fst✝, snd✝)
i : β
⊢ snd✝¹ i = snd✝ i

Tactic:
simpa using Equiv.congr_fun h (Sum.inr i)

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

Goal state before:
pp: M₀ : Type u_1
G₀ : Type u_2
M₀' : Type u_3
G₀' : Type u_4
inst✝⁷ : GroupWithZero G₀
inst✝⁶ : Zero G₀'
inst✝⁵ : Mul G₀'
inst✝⁴ : One G₀'
inst✝³ : Inv G₀'
inst✝² : Div G₀'
inst✝¹ : Pow G₀' ℕ
inst✝ : Pow G₀' ℤ
f : G₀' → G₀
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
mul : ∀ (x y : G₀'), f (x * y) = f x * f y
inv : ∀ (x : G₀'), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : G₀'), f (x / y) = f x / f y
npow : ∀ (x : G₀') (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : G₀') (n : ℤ), f (x ^ n) = f x ^ n
x : G₀'
hx : x ≠ 0
⊢ f (x * x⁻¹) = f 1

Tactic:
one,

Goal state after:
M₀ : Type u_1
G₀ : Type u_2
M₀' : Type u_3
G₀' : Type u_4
inst✝⁷ : GroupWithZero G₀
inst✝⁶ : Zero G₀'
inst✝⁵ : Mul G₀'
inst✝⁴ : One G₀'
inst✝³ : Inv G₀'
inst✝² : Div G₀'
inst✝¹ : Pow G₀' ℕ
inst✝ : Pow G₀' ℤ
f : G₀' → G₀
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
mul : ∀ (x y : G₀'), f (x * y) = f x * f y
inv : ∀ (x : G₀'), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : G₀'), f (x / y) = f x / f y
npow : ∀ (x : G₀') (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : G₀') (n : ℤ), f (x ^ n) = f x ^ n
x : G₀'
hx : x ≠ 0
⊢ f (x * x⁻¹) = 1
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: M₀ : Type u_1
inst✝ : MonoidWithZero M₀
n : ℕ
x✝ : n + 1 ≠ 0
⊢ 0 ^ (n + 1) = 0

Tactic:
by rw [pow_succ, mul_zero]

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

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

Tactic:
by rw [div_eq_mul_inv, zero_mul]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : AddMonoid R
inst✝ : One R
n : ℕ
⊢ (n + 1).binCast = n.binCast + 1

Tactic:
let : AddMonoidWithOne R := AddMonoidWithOne.unary

Goal state after:
R : Type u_1
inst✝¹ : AddMonoid R
inst✝ : One R
n : ℕ
this : AddMonoidWithOne R := AddMonoidWithOne.unary
⊢ (n + 1).binCast = n.binCast + 1
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: case pos
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
m n : ℤ
h : a ≠ 0 ∨ m + n ≠ 0 ∨ m = 0 ∧ n = 0
hm : ¬m = 0
hn : n = 0
⊢ a ^ (m + n) = a ^ m * a ^ n

Tactic:
simp [hn]

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

Goal state before:
pp: R : Type v
inst✝² : Mul R
inst✝¹ : Add R
inst✝ : RightDistribClass R
a b c d : R
⊢ (a + b + c) * d = a * d + b * d + c * d

Tactic:
by simp [right_distrib]

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

Goal state before:
pp: α : Type u_1
inst✝ : CommSemigroup α
a b c : α
h : c * a = b
⊢ a * c = b

Tactic:
rw [mul_comm] at h

Goal state after:
α : Type u_1
inst✝ : CommSemigroup α
a b c : α
h : a * c = b
⊢ a * c = b
Module: Mathlib.Algebra.Group.Commute.Units

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

Tactic:
by rwa [← _root_.pow_succ', Nat.sub_add_cancel (Nat.succ_le_of_lt <| Nat.pos_of_ne_zero hn)]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
f✝ : S → R
hf✝ : Injective 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✝ : AddMonoidWithOne R
f : S → R
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
nsmul : ∀ (n : ℕ) (x : S), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f ↑n = ↑n
n : ℕ
⊢ ↑n + 1 = f ↑n + f 1

Tactic:
one,

Goal state after:
R : Type u_1
S : Type u_2
f✝ : S → R
hf✝ : Injective 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✝ : AddMonoidWithOne R
f : S → R
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
nsmul : ∀ (n : ℕ) (x : S), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f ↑n = ↑n
n : ℕ
⊢ ↑n + 1 = f ↑n + 1
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✝ : AddMonoidWithOne R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : R), f (x + y) = f x + f y
nsmul : ∀ (n : ℕ) (x : R), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f ↑n = ↑n
n : ℕ
⊢ f ↑n + f 1 = ↑n + 1

Tactic:
one,

Goal state after:
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✝ : AddMonoidWithOne R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : R), f (x + y) = f x + f y
nsmul : ∀ (n : ℕ) (x : R), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f ↑n = ↑n
n : ℕ
⊢ f ↑n + 1 = ↑n + 1
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝ : Ring α
⊢ Even (-2)

Tactic:
simp only [even_neg, even_two]

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

Goal state before:
pp: m n : ℕ
⊢ Even (m / n) ↔ m % (2 * n) / n = 0

Tactic:
by
  rw [even_iff_two_dvd, dvd_iff_mod_eq_zero, ← Nat.mod_mul_right_div_self, mul_comm]

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

Goal state before:
pp: α : Type u_1
inst✝⁶ : Mul α
inst✝⁵ : Zero α
inst✝⁴ : Preorder α
inst✝³ : PosMulStrictMono α
β : Type u_2
inst✝² : Zero β
inst✝¹ : Mul β
inst✝ : Preorder β
f : β → α
zero : f 0 = 0
mul : ∀ (x y : β), f (x * y) = f x * f y
lt : ∀ {x y : β}, f x < f y ↔ x < y
a : β
ha : 0 < a
b c : β
hbc : b < c
⊢ f a * f b < f a * f c

Tactic:
exact mul_lt_mul_of_pos_left (lt.2 hbc) (by rwa [← zero, lt])

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

Goal state before:
pp: α✝ : Type u_1
α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : Preorder α
mul_le_mul_left : ∀ (a b : α), a ≤ b → ∀ (c : α), a * c ≤ b * c
a b : α
h : a ≤ b
c : α
⊢ c * a ≤ c * b

Tactic:
by
    rw [mul_comm c, mul_comm c]; exact mul_le_mul_left a b h c

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✝ : PosMulStrictMono R
h : ∀ (n : ℕ), 0 ≤ a * b ^ n
this : 0 ≤ a
ha : 0 < a
⊢ 0 ≤ a * b

Tactic:
simpa only [pow_one] using h 1

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₀
n : ℤ
ha : 1 < a
hn : 0 < n
⊢ 1 < a ^ n

Tactic:
by
  simpa using zpow_right_strictMono₀ ha hn

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

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

Tactic:
by
  simpa using zpow_right_strictMono₀ ha hn

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✝ : PosMulMono G₀
⊢ a⁻¹ < 0 ↔ a < 0

Tactic:
by
  have := PosMulMono.toPosMulReflectLT (α := G₀); simp only [← not_le, inv_nonneg]

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

Goal state before:
pp: R : Type u
inst✝⁴ : Ring R
inst✝³ : LinearOrder R
a b : R
inst✝² : MulPosStrictMono R
inst✝¹ : PosMulStrictMono R
inst✝ : AddLeftMono R
x : R
h : a ≤ b
⊢ (x - a) * (x - b) ≤ 0 ↔ a ≤ x ∧ x ≤ b

Tactic:
rw [mul_nonpos_iff, sub_nonneg, sub_nonneg, sub_nonpos, sub_nonpos, or_iff_left_iff_imp, and_comm]
  exact And.imp h.trans h.trans'

Goal state after:
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✝⁷ : LE α✝
inst✝⁶ : LE β✝
inst✝⁵ : LE γ✝
inst✝⁴ : LE δ✝
α : Type ?u.19
β : Type ?u.21
γ : Type ?u.23
δ : Type ?u.25
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
f : α ≃o γ
g : β ≃o δ
p q : α →o β
⊢ { toFun := fun p ↦ (↑g).comp (p.comp ↑f.symm), invFun := fun p ↦ (↑g.symm).comp (p.comp ↑f), left_inv := ⋯,
          right_inv := ⋯ }
        p ≤
      { toFun := fun p ↦ (↑g).comp (p.comp ↑f.symm), invFun := fun p ↦ (↑g.symm).comp (p.comp ↑f), left_inv := ⋯,
          right_inv := ⋯ }
        q ↔
    p ≤ q

Tactic:
by
    simp only [Equiv.coe_fn_mk, OrderHom.le_def, OrderHom.comp_coe,
               OrderHomClass.coe_coe, Function.comp_apply, map_le_map_iff]
    exact Iff.symm f.forall_congr_left

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

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

Tactic:
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.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: case inl
α : Type u_1
inst✝³ : Group α
inst✝² : LinearOrder α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a b : α
ab : a ≤ b
⊢ max a b / min a b = |a / b|ₘ

Tactic:
max_eq_right ab,

Goal state after:
case inl
α : Type u_1
inst✝³ : Group α
inst✝² : LinearOrder α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a b : α
ab : a ≤ b
⊢ b / min a b = |a / b|ₘ
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: case top.top
G : Type u_1
α : Type u_2
inst✝² : AddCommGroup G
x y : WithTop G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedAddMonoid G
⊢ ⊤ - ⊤ = ⊤ + -⊤

Tactic:
simp [← coe_sub, ← coe_neg, sub_eq_add_neg]

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

Goal state before:
pp: case top.coe
G : Type u_1
α : Type u_2
inst✝² : AddCommGroup G
x y : WithTop G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedAddMonoid G
a✝ : G
⊢ ⊤ - ↑a✝ = ⊤ + -↑a✝

Tactic:
simp [← coe_sub, ← coe_neg, sub_eq_add_neg]

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

Goal state before:
pp: case coe.top
G : Type u_1
α : Type u_2
inst✝² : AddCommGroup G
x y : WithTop G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedAddMonoid G
a✝ : G
⊢ ↑a✝ - ⊤ = ↑a✝ + -⊤

Tactic:
simp [← coe_sub, ← coe_neg, sub_eq_add_neg]

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

Goal state before:
pp: case coe.coe
G : Type u_1
α : Type u_2
inst✝² : AddCommGroup G
x y : WithTop G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedAddMonoid G
a✝¹ a✝ : G
⊢ ↑a✝¹ - ↑a✝ = ↑a✝¹ + -↑a✝

Tactic:
simp [← coe_sub, ← coe_neg, sub_eq_add_neg]

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

Goal state before:
pp: case top
α : Type u
β : Type v
inst✝³ : Add α
F : Type u_1
inst✝² : Add β
inst✝¹ : FunLike F α β
inst✝ : AddHomClass F α β
f : F
b : WithTop α
⊢ map (⇑f) (⊤ + b) = map ⇑f ⊤ + map (⇑f) b

pp: case coe
α : Type u
β : Type v
inst✝³ : Add α
F : Type u_1
inst✝² : Add β
inst✝¹ : FunLike F α β
inst✝ : AddHomClass F α β
f : F
b : WithTop α
a✝ : α
⊢ map (⇑f) (↑a✝ + b) = map ⇑f ↑a✝ + map (⇑f) b

Tactic:
· exact (top_add _).symm

Goal state after:
case coe
α : Type u
β : Type v
inst✝³ : Add α
F : Type u_1
inst✝² : Add β
inst✝¹ : FunLike F α β
inst✝ : AddHomClass F α β
f : F
b : WithTop α
a✝ : α
⊢ map (⇑f) (↑a✝ + b) = map ⇑f ↑a✝ + map (⇑f) b
Module: Mathlib.Algebra.Order.Sub.Basic

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

Tactic:
rw [not_le] at h
      constructor <;> intro h'
      · simpa using add_le_add h' h.le
      · exact zero_le

Goal state after: