mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Commute.Defs

Goal state before:
pp: S : Type u_3
inst✝ : Semigroup S
a b : S
h : Commute a b
c : S
⊢ a * (b * c) = b * (a * c)

Tactic:
by
  simp only [← mul_assoc, h.eq]

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

Goal state before:
pp: M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
n : ℕ
m : M
⊢ npowBinRec (n + 1) m = npowBinRec n m * m

Tactic:
← npowBinRecAuto,

Goal state after:
M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
n : ℕ
m : M
⊢ npowBinRecAuto (n + 1) m = npowBinRec n m * m
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
n : ℕ
m : M
⊢ npowRecAuto (n + 1) m = npowBinRec n m * m

Tactic:
← npowBinRecAuto,

Goal state after:
M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
n : ℕ
m : M
⊢ npowRecAuto (n + 1) m = npowBinRecAuto n m * m
Module: Mathlib.Logic.Basic

Goal state before:
pp: ι : Sort u_3
inst✝ : Subsingleton ι
P : ι → ι → Prop
i : ι
⊢ (∀ (j : ι), P i j) ↔ P i i

Tactic:
have : Nonempty ι := ⟨i⟩

Goal state after:
ι : Sort u_3
inst✝ : Subsingleton ι
P : ι → ι → Prop
i : ι
this : Nonempty ι
⊢ (∀ (j : ι), P i j) ↔ P i i
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α α' : Sort u
β : α → Sort v
β' : α' → Sort v
f : (a : α) → β a
f' : (a : α') → β' a
hα : α = α'
h : ∀ (a : α) (a' : α'), a ≍ a' → f a ≍ f' a'
⊢ f ≍ f'

Tactic:
subst hα

Goal state after:
α : Sort u
β : α → Sort v
f : (a : α) → β a
β' : α → Sort v
f' : (a : α) → β' a
h : ∀ (a a' : α), a ≍ a' → f a ≍ f' a'
⊢ f ≍ f'
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: case refine_1
α : Sort u_1
β : Sort u_2
f : α → β
inst✝ : Subsingleton α
g : α → β
x y : α
h : f x = g y
z : α
⊢ f z = g z

Tactic:
Subsingleton.elim x z,

Goal state after:
case refine_1
α : Sort u_1
β : Sort u_2
f : α → β
inst✝ : Subsingleton α
g : α → β
x y z : α
h : f z = g y
⊢ f z = g z
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u
β : α → Sort v
inst✝ : DecidableEq α
f : (a : α) → β a
a : α
b : β a
p : (a : α) → β a → Prop
⊢ (∃ x, p x (update f a b x)) ↔ p a b ∨ ∃ x, x ≠ a ∧ p x (f x)

Tactic:
rw [← not_forall_not, forall_update_iff f fun a b ↦ ¬p a b]
  simp [-not_and, not_and_or]

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

Goal state before:
pp: case pos
γ : Sort u_3
α₁ : Sort u_4
α₂ : Sort u_5
α₃ : Sort u_6
f₁₂ : α₁ → α₂
h₁₂ : Injective f₁₂
f₂₃ : α₂ → α₃
h₂₃ : Injective f₂₃
g : α₁ → γ
e' : α₃ → γ
b : α₂
⊢ extend (f₂₃ ∘ f₁₂) g e' (f₂₃ b) = extend f₂₃ (extend f₁₂ g (e' ∘ f₂₃)) e' (f₂₃ b)

Tactic:
rw [Injective.extend_apply h₂₃]

Goal state after:
case pos
γ : Sort u_3
α₁ : Sort u_4
α₂ : Sort u_5
α₃ : Sort u_6
f₁₂ : α₁ → α₂
h₁₂ : Injective f₁₂
f₂₃ : α₂ → α₃
h₂₃ : Injective f₂₃
g : α₁ → γ
e' : α₃ → γ
b : α₂
⊢ extend (f₂₃ ∘ f₁₂) g e' (f₂₃ b) = extend f₁₂ g (e' ∘ f₂₃) b
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → Prop → Prop
⊢ (r ∘r fun x1 x2 ↦ x1 ↔ x2) = r

Tactic:
by
  grind [comp_eq]

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 : ReflTransGen r b c
⊢ ReflTransGen r a c

Tactic:
induction hbc with
  | refl => assumption
  | tail _ hcd hac => exact hac.tail hcd

Goal state after:
Module: Mathlib.Logic.Relation

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

Tactic:
induction hbc with
  | refl => assumption
  | tail _ hcd hac => exact hac.tail hcd

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
p : β → β → Prop
f : α → β
h : r ≤ (ReflTransGen p on f)
⊢ ReflTransGen r ≤ (ReflTransGen p on f)

Tactic:
by
  intro _ _ hab
  simpa [reflTransGen_eq_self] using hab.lift f h

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

Goal state before:
pp: α : Sort u_1
β : Sort u_2
⊢ Nonempty α ∧ IsEmpty β ↔ ¬IsEmpty α ∧ IsEmpty β

Tactic:
not_isEmpty_iff

Goal state after:
α : Sort u_1
β : Sort u_2
⊢ Nonempty α ∧ IsEmpty β ↔ Nonempty α ∧ IsEmpty β
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:
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:
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 : α
⊢ (if a ≤ b then a else b) ≤ a

Tactic:
split_ifs with h <;> simp [h, le_of_not_ge]

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

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

Tactic:
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:
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.Data.Int.Order.Basic

Goal state before:
pp: a b : ℤ
⊢ 0 < a * b ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0

Tactic:
by
  rw [Int.lt_iff_le_and_ne, Int.mul_nonneg_iff, ne_comm, Int.mul_ne_zero_iff]
  lia

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

Goal state before:
pp: m n : ℕ
⊢ ¬2 * n % 2 = (2 * m + 1) % 2

Tactic:
by rw [Nat.add_comm, add_mul_mod_self_left, mul_mod_right, mod_eq_of_lt] <;> simp

Goal state after:
Module: Mathlib.Tactic.Lift

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
coeβα : β → α
condβα : α → Prop
coeδγ : δ → γ
condδγ : γ → Prop
inst✝¹ : CanLift α β coeβα condβα
inst✝ : CanLift γ δ coeδγ condδγ
x : β
y : δ
hx : condβα (coeβα x, coeδγ y).fst
hy : condδγ (coeβα x, coeδγ y).snd
⊢ ∃ y_1, map coeβα coeδγ y_1 = (coeβα x, coeδγ y)

Tactic:
exact ⟨(x, y), by simp⟩

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

Goal state before:
pp: α : Type u
s : Set α
⊢ s ⊆ univ ∧ ¬univ ⊆ s ↔ sᶜ.Nonempty

Tactic:
Set.not_univ_subset,

Goal state after:
α : Type u
s : Set α
⊢ (s ⊆ univ ∧ ∃ a, ¬a ∈ s) ↔ sᶜ.Nonempty
Module: Mathlib.Data.Set.Basic

Goal state before:
pp: α : Type u
s : Set α
⊢ sᶜ ⊆ univ ∧ ¬univ ⊆ sᶜ ↔ s.Nonempty

Tactic:
Set.not_univ_subset,

Goal state after:
α : Type u
s : Set α
⊢ (sᶜ ⊆ univ ∧ ∃ a, ¬a ∈ sᶜ) ↔ s.Nonempty
Module: Mathlib.Order.Lattice

Goal state before:
pp: α✝ : Type u
β : Type v
α : Type u_1
inst✝ : Min α
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
inf_idem : ∀ (a : α), a ⊓ a = a
a b c : α
hac : b ⊓ a = a
hbc : c ⊓ a = a
⊢ b ⊓ c ⊓ a = a

Tactic:
rwa [inf_assoc, hbc]

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: case inl
ι : Type u_1
π : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → SemilatticeSup (π i)
f : (i : ι) → π i
j : ι
a b : π j
⊢ update f j (a ⊔ b) j = (update f j a ⊔ update f j b) j

Tactic:
simp [update_of_ne, *]

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: case inr
ι : Type u_1
π : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → SemilatticeSup (π i)
f : (i : ι) → π i
i : ι
a b : π i
j : ι
hji : j ≠ i
⊢ update f i (a ⊔ b) j = (update f i a ⊔ update f i b) j

Tactic:
simp [update_of_ne, *]

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
⊢ RightInverse (Sum.elim succ fun x ↦ 0) fun n ↦ Nat.casesOn n (inr PUnit.unit) inl

Tactic:
by rintro (_ | _) <;> rfl

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

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.13
⊢ RightInverse (Sum.elim (Prod.mk false) (Prod.mk true)) fun p ↦ if p.fst = true then inr p.snd else inl p.snd

Tactic:
by rintro (_ | _) <;> rfl

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

Goal state before:
pp: α : Type u_1
s : Set α
σ : Equiv.Perm α
hs : {a | σ a ≠ a} ⊆ s
⊢ ⇑σ '' s = s

Tactic:
ext i
  obtain hi | hi := eq_or_ne (σ i) i
  · refine ⟨?_, fun h => ⟨i, h, hi⟩⟩
    rintro ⟨j, hj, h⟩
    rwa [σ.injective (hi.trans h.symm)]
  · refine iff_of_true ⟨σ.symm i, hs fun h => hi ?_, σ.apply_symm_apply _⟩ (hs hi)
    grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
⊢ range Sum.inl = {x | x.isLeft = true}

Tactic:
ext (_ | _)

Goal state after:
case inl
α : Type u_1
β : Type u_2
val✝ : α
⊢ Sum.inl val✝ ∈ range Sum.inl ↔ Sum.inl val✝ ∈ {x | x.isLeft = true}

case inr
α : Type u_1
β : Type u_2
val✝ : β
⊢ Sum.inr val✝ ∈ range Sum.inl ↔ Sum.inr val✝ ∈ {x | x.isLeft = true}
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
⊢ range Sum.inr = {x | x.isRight = true}

Tactic:
ext (_ | _)

Goal state after:
case inl
α : Type u_1
β : Type u_2
val✝ : α
⊢ Sum.inl val✝ ∈ range Sum.inr ↔ Sum.inl val✝ ∈ {x | x.isRight = true}

case inr
α : Type u_1
β : Type u_2
val✝ : β
⊢ Sum.inr val✝ ∈ range Sum.inr ↔ Sum.inr val✝ ∈ {x | x.isRight = true}
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Set γ
f : α → γ
g : β → γ
⊢ Sum.elim f g ⁻¹' s = Sum.inl '' f ⁻¹' s ∪ Sum.inr '' g ⁻¹' s

Tactic:
ext (_ | _)

Goal state after:
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set γ
f : α → γ
g : β → γ
val✝ : α
⊢ Sum.inl val✝ ∈ Sum.elim f g ⁻¹' s ↔ Sum.inl val✝ ∈ Sum.inl '' f ⁻¹' s ∪ Sum.inr '' g ⁻¹' s

case inr
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set γ
f : α → γ
g : β → γ
val✝ : β
⊢ Sum.inr val✝ ∈ Sum.elim f g ⁻¹' s ↔ Sum.inr val✝ ∈ Sum.inl '' f ⁻¹' s ∪ Sum.inr '' g ⁻¹' s
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s : Set ι
f : (i : ι) → α i → β i
hf : ∀ (i : ι), ¬i ∈ s → Surjective (f i)
t : (i : ι) → Set (α i)
b : (i : ι) → β i
hb : b ∈ s.pi fun i ↦ f i '' t i
i : ι
hi : i ∈ s
⊢ ∃ a, f i a = b i ∧ (i ∈ s → a ∈ t i)

Tactic:
exact (hb i hi).imp fun a ⟨hat, hab⟩ ↦ ⟨hab, fun _ ↦ hat⟩

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

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
s' : Set α
hs' : s' ⊆ s
hfs' : BijOn f s' t
⊢ SurjOn f s t

Tactic:
exact hfs'.surjOn.mono hs' (Subset.refl _)

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a : G
m n : ℤ
⊢ a ^ (m - n) = a ^ m * (a ^ n)⁻¹

Tactic:
Int.sub_eq_add_neg,

Goal state after:
G : Type u_3
inst✝ : Group G
a : G
m n : ℤ
⊢ a ^ (m + -n) = a ^ m * (a ^ n)⁻¹
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: case pred
G : Type u_3
inst✝ : Group G
g : G
P : G → Prop
h_one : P 1
h_mul : ∀ (a : G), P a → P (g * a)
h_inv : ∀ (a : G), P a → P (g⁻¹ * a)
n : ℕ
ih : P (g ^ (-↑n))
⊢ P (g ^ (-↑n - 1))

Tactic:
Int.sub_eq_add_neg,

Goal state after:
case pred
G : Type u_3
inst✝ : Group G
g : G
P : G → Prop
h_one : P 1
h_mul : ∀ (a : G), P a → P (g * a)
h_inv : ∀ (a : G), P a → P (g⁻¹ * a)
n : ℕ
ih : P (g ^ (-↑n))
⊢ P (g ^ (-↑n + -1))
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
G : Type u_3
M : Type u_4
α : Type u_5
s : AddCommMonoid α
n : ℕ
a : α
⊢ n • a + 1 • a = n • a + a

Tactic:
one_nsmul

Goal state after:
α✝ : Type u_1
β : Type u_2
G : Type u_3
M : Type u_4
α : Type u_5
s : AddCommMonoid α
n : ℕ
a : α
⊢ n • a + a = n • a + a
Module: Mathlib.Algebra.Group.Units.Basic

Goal state before:
pp: α : Type u
inst✝ : Monoid α
x : α
u : αˣ
y : α
⊢ y /ₚ u = x ↔ x * ↑u = y

Tactic:
divp_eq_iff_mul_eq

Goal state after:
α : Type u
inst✝ : Monoid α
x : α
u : αˣ
y : α
⊢ x * ↑u = y ↔ x * ↑u = y
Module: Mathlib.Algebra.Group.Units.Basic

Goal state before:
pp: α : Type u
inst✝ : CommMonoid α
x y : α
ux uy : αˣ
⊢ y * ↑ux /ₚ uy = x ↔ x * ↑uy = y * ↑ux

Tactic:
divp_eq_iff_mul_eq

Goal state after:
α : Type u
inst✝ : CommMonoid α
x y : α
ux uy : αˣ
⊢ x * ↑uy = y * ↑ux ↔ x * ↑uy = y * ↑ux
Module: Mathlib.Algebra.Group.Action.Opposite

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst✝ : Monoid α
⊢ Monoid.toMulAction αᵐᵒᵖ = instMulAction

Tactic:
by
  with_reducible_and_instances rfl

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

Goal state before:
pp: M₀ : Type u_1
inst✝ : MulZeroClass M₀
⊢ NoZeroDivisors M₀ ↔ ∀ (x : M₀), x ≠ 0 → ∀ (y : M₀), y * x = 0 → y = 0

Tactic:
by
  simp only [noZeroDivisors_iff, or_iff_not_imp_right]
  exact ⟨fun h b hb a eq ↦ h eq hb, fun h a b eq hb ↦ h b hb a eq⟩

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

Goal state before:
pp: α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
f : Perm (Subtype p)
x : α
h : p x
⊢ p ((ofSubtype f) x) ↔ p x

Tactic:
by
    simpa only [h, iff_true, MonoidHom.coe_mk, ofSubtype_apply_of_mem f h] using (f ⟨x, h⟩).2

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

Goal state before:
pp: M₀ : Type u_1
a b : M₀
inst✝¹ : MulZeroOneClass M₀
inst✝ : IsLeftCancelMulZero M₀
ha : a ≠ 0
⊢ a * b = a ↔ b = 1

Tactic:
mul_eq_left₀ ha

Goal state after:
M₀ : Type u_1
a b : M₀
inst✝¹ : MulZeroOneClass M₀
inst✝ : IsLeftCancelMulZero M₀
ha : a ≠ 0
⊢ b = 1 ↔ b = 1
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: M₀✝ : Type u_1
G₀ : Type u_2
a b c : M₀✝
inst✝² : MulZeroOneClass M₀✝
M₀ : Type u_3
inst✝¹ : MonoidWithZero M₀
inst✝ : IsRightCancelMulZero M₀
a✝ b✝ : M₀
h : a✝ * b✝ = 1
⊢ b✝ * a✝ = 1

Tactic:
cases subsingleton_or_nontrivial M₀
    · exact Subsingleton.elim _ _
    exact (IsRightCancelMulZero.mul_right_cancel_of_ne_zero
      (right_ne_zero_of_mul_eq_one h)).mul_eq_one_symm h

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

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : MulZeroOneClass α
inst✝¹ : MulZeroOneClass β
inst✝ : MulZeroOneClass γ
g : β →*₀ γ
f₁ f₂ : α →*₀ β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
x : α
⊢ g (f₁ x) = g (f₂ x)

Tactic:
← comp_apply,

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : MulZeroOneClass α
inst✝¹ : MulZeroOneClass β
inst✝ : MulZeroOneClass γ
g : β →*₀ γ
f₁ f₂ : α →*₀ β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
x : α
⊢ (g.comp f₁) x = g (f₂ x)
Module: Mathlib.Algebra.GroupWithZero.Action.Defs

Goal state before:
pp: M : Type u_1
M₀ : Type u_2
M₀' : Type u_3
G₀ : Type u_4
G₀' : Type u_5
N : Type u_6
A : Type u_7
A' : Type u_8
B : Type u_9
α : Type u_10
β : Type u_11
inst✝⁵ : Zero M₀
inst✝⁴ : Zero A
inst✝³ : SMulWithZero M₀ A
a : M₀
b : A
inst✝² : Zero M₀'
inst✝¹ : Zero A'
inst✝ : SMul M₀ A'
f : ZeroHom M₀' M₀
m : A
⊢ 0 • m = 0

Tactic:
by change (f 0) • m = 0; rw [map_zero, zero_smul]

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

Goal state before:
pp: m n : ℕ
hl : m * m < n
hr : n < (m + 1) * (m + 1)
⊢ ¬∃ t, t * t = n

Tactic:
rintro ⟨t, rfl⟩
  have h1 : m < t := Nat.mul_self_lt_mul_self_iff.1 hl
  have h2 : t < m + 1 := Nat.mul_self_lt_mul_self_iff.1 hr
  grind

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
f : Multiplicative ℕ →* M
n : Multiplicative ℕ
⊢ f n = f (ofAdd 1) ^ toAdd n

Tactic:
← powersHom_symm_apply,

Goal state after:
M : Type u_1
inst✝ : Monoid M
f : Multiplicative ℕ →* M
n : Multiplicative ℕ
⊢ f n = (powersHom M).symm f ^ toAdd n
Module: Mathlib.Algebra.Ring.Hom.Defs

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : NonUnitalNonAssocSemiring β
inst✝ : NonUnitalNonAssocSemiring γ
g : β →ₙ+* γ
f₁ f₂ : α →ₙ+* β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
x : α
⊢ g (f₁ x) = g (f₂ x)

Tactic:
← comp_apply,

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : NonUnitalNonAssocSemiring β
inst✝ : NonUnitalNonAssocSemiring γ
g : β →ₙ+* γ
f₁ f₂ : α →ₙ+* β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
x : α
⊢ (g.comp f₁) x = g (f₂ x)
Module: Mathlib.Algebra.Ring.Hom.Defs

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
x✝² : NonAssocSemiring α
x✝¹ : NonAssocSemiring β
x✝ : NonAssocSemiring γ
g : β →+* γ
f₁ f₂ : α →+* β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
x : α
⊢ g (f₁ x) = g (f₂ x)

Tactic:
← comp_apply,

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
x✝² : NonAssocSemiring α
x✝¹ : NonAssocSemiring β
x✝ : NonAssocSemiring γ
g : β →+* γ
f₁ f₂ : α →+* β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
x : α
⊢ (g.comp f₁) x = g (f₂ x)
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 = 0 ∨ f (x * y) - f x * f y = 0
⊢ (↑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 : 2 = 0 ∨ f (x * y) = f x * f y
⊢ (↑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 : β
⊢ (↑f).toFun (x * y) = (↑f).toFun x * (↑f).toFun y

Tactic:
by
      have hxy := h (x + y)
      rw [mul_add, add_mul, add_mul, f.map_add, f.map_add, f.map_add, f.map_add, h x, h y, add_mul,
        mul_add, mul_add, ← sub_eq_zero, add_comm (f x * f x + f (y * x)), ← sub_sub, ← sub_sub,
        ← sub_sub, mul_comm y x, mul_comm (f y) (f x)] at hxy
      simp only [add_assoc, add_sub_assoc, add_sub_cancel] at hxy
      rw [sub_sub, ← two_mul, ← add_sub_assoc, ← two_mul, ← mul_sub, mul_eq_zero (M₀ := α),
        sub_eq_zero, or_iff_not_imp_left] at hxy
      exact hxy h_two

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

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

Tactic:
simp [ha] at h

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

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
m n : ℤ
⊢ a ^ (m - n) = a ^ m / a ^ n

Tactic:
Int.sub_eq_add_neg,

Goal state after:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
m n : ℤ
⊢ a ^ (m + -n) = a ^ m / a ^ n
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 - b = 0 ∨ a + b = 0 ↔ 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 = b ∨ a + 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 = -b ∨ a - b = 0 ↔ 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 = -b ∨ a = b ↔ a = b ∨ a = -b
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic

Goal state before:
pp: case inl
α : Type u_1
inst✝² : Mul α
inst✝¹ : PartialOrder α
inst✝ : MulRightStrictMono α
a b c : α
h' : ¬c = b
h : b ≤ c
⊢ ¬c * a = b * a

Tactic:
exact mul_lt_mul_left (h.lt_of_ne' h') a |>.ne'

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:
simp only [le_iff_eq_or_lt, inv_pos, zero_eq_inv]

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

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a : G₀
⊢ 0 ≤ a⁻¹ ↔ 0 ≤ a

Tactic:
simp only [le_iff_eq_or_lt, inv_pos, zero_eq_inv]

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
⊢ b ≤ x ∧ x ≤ a → a ≤ x ∧ x ≤ b

Tactic:
exact And.imp h.trans h.trans'

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

Goal state before:
pp: α β γ : Type u
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
h₁ : α = β
h₁' : β = γ
h₂ : r ≍ s
h₂' : s ≍ t
x : α
⊢ ((RelIso.cast h₁ h₂).trans (RelIso.cast h₁' h₂')) x = (RelIso.cast ⋯ ⋯) x

Tactic:
by subst h₁; rfl

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✝³ : Preorder α✝
inst✝² : Preorder β✝
α : Type ?u.13
β : Type ?u.15
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
e : (fun x1 x2 ↦ x1 < x2) ≃r fun x1 x2 ↦ x1 < x2
⊢ ∀ {a b : α}, e.toEquiv a ≤ e.toEquiv b ↔ a ≤ b

Tactic:
simp [le_iff_eq_or_lt, e.map_rel_iff, e.injective.eq_iff]

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

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
ha : 1 ≤ a ^ 2
⊢ a ⊓ (1 ⊓ a ^ 2) = a ⊓ 1

Tactic:
inf_of_le_left ha

Goal state after:
α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
ha : 1 ≤ a ^ 2
⊢ a ⊓ 1 = a ⊓ 1
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow

Goal state before:
pp: M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulRightMono M
n : ℕ
x : M
hn : 0 < n
h : x < 1
⊢ x ^ n < 1

Tactic:
rcases Nat.exists_eq_succ_of_ne_zero hn.ne' with ⟨k, rfl⟩

Goal state after:
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulRightMono M
x : M
h : x < 1
k : ℕ
hn : 0 < k.succ
⊢ x ^ k.succ < 1
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: case H1
x y a b : ℕ
h : 0 < a
IH :
  ∀ {s t s' t' : ℤ},
    ↑b % ↑a = ↑x * s + ↑y * t →
      ↑a = ↑x * s' + ↑y * t' →
        ↑((b % a).xgcdAux s t a s' t').1 =
          ↑x * ((b % a).xgcdAux s t a s' t').2.1 + ↑y * ((b % a).xgcdAux s t a s' t').2.2
s t s' t' : ℤ
p : ↑a = ↑x * s + ↑y * t
p' : ↑b = ↑x * s' + ↑y * t'
⊢ ↑b % ↑a = ↑x * (s' - ↑b / ↑a * s) + ↑y * (t' - ↑b / ↑a * t)

Tactic:
rw [Int.emod_def]

Goal state after:
case H1
x y a b : ℕ
h : 0 < a
IH :
  ∀ {s t s' t' : ℤ},
    ↑b % ↑a = ↑x * s + ↑y * t →
      ↑a = ↑x * s' + ↑y * t' →
        ↑((b % a).xgcdAux s t a s' t').1 =
          ↑x * ((b % a).xgcdAux s t a s' t').2.1 + ↑y * ((b % a).xgcdAux s t a s' t').2.2
s t s' t' : ℤ
p : ↑a = ↑x * s + ↑y * t
p' : ↑b = ↑x * s' + ↑y * t'
⊢ ↑b - ↑a * (↑b / ↑a) = ↑x * (s' - ↑b / ↑a * s) + ↑y * (t' - ↑b / ↑a * t)
Module: Mathlib.Algebra.Order.Ring.Int

Goal state before:
pp: case succ.succ
n p q : ℕ
dvd : (↑(p + 1)).gcd ↑(q + 1) ∣ n
le : (p + 1).pred * (q + 1).pred ≤ n
⊢ ∃ a b, a * (p + 1) + b * (q + 1) = n

Tactic:
Int.gcd_dvd_iff

Goal state after:
case succ.succ
n p q : ℕ
dvd : ∃ x y, ↑n = ↑(p + 1) * x + ↑(q + 1) * y
le : (p + 1).pred * (q + 1).pred ≤ n
⊢ ∃ a b, a * (p + 1) + b * (q + 1) = n
Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs

Goal state before:
pp: α : Type u
inst✝² : MulOneClass α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedMul α
a b : α
h : a < b
⊢ ∃ c x, a * c = b

Tactic:
obtain ⟨c, hc⟩ := le_iff_exists_mul.1 h.le
  refine ⟨c, one_lt_iff_ne_one.2 ?_, hc.symm⟩
  rintro rfl
  simp [hc] at h

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

Goal state before:
pp: case inl
α : Type u
inst✝² : Monoid α
inst✝¹ : LinearOrder α
inst✝ : CanonicallyOrderedMul α
a b c : α
hb : a ≤ b
⊢ min a (b * c) = min a (min a b * min a c)

Tactic:
simp [hb, le_mul_right]

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

Goal state before:
pp: α : Type u
inst✝² : Add α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedAdd α
x : WithBot α
hx : x ≠ ⊥
y : WithBot α
⊢ y ≤ y + x

Tactic:
induction x
  · simp at hx
  induction y
  · simp
  · rw [← WithBot.coe_add, WithBot.coe_le_coe]
    exact le_self_add

Goal state after: