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

Goal state before:
pp: M : Type u_2
inst✝ : MulOneClass M
a : M
⊢ SemiconjBy a 1 1

Tactic:
rw [SemiconjBy, mul_one, one_mul]

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

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

Tactic:
rw [h.eq, mul_inv_cancel_right]

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

Goal state before:
pp: M : Type u_2
x✝¹ : Semigroup M
x✝ : One M
k : ℕ
m : M
⊢ npowRecAuto k m = npowBinRecAuto k m

Tactic:
rw [npowBinRecAuto, npowRecAuto, npowBinRec]

Goal state after:
M : Type u_2
x✝¹ : Semigroup M
x✝ : One M
k : ℕ
m : M
⊢ npowRec k m = npowBinRec.go k 1 m
Module: Mathlib.Logic.Nontrivial.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : Nontrivial α
inst✝ : DecidableEq α
x : α
⊢ ∃ y, y ≠ x

Tactic:
by
  rcases exists_pair_ne α with ⟨y, y', h⟩
  by_cases hx : x = y
  · rw [← hx] at h
    exact ⟨y', h.symm⟩
  · exact ⟨y, Ne.symm hx⟩

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case single
α : Type u_1
r : α → α → Prop
a i✝ b✝ : α
h : r a b✝
⊢ ReflTransGen r a b✝

Tactic:
exact ReflTransGen.single h

Goal state after:
Module: Mathlib.Logic.Relation

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

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

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
⊢ Function.swap (ReflTransGen r) ≤ ReflTransGen (Function.swap r)

Tactic:
intro _ _ h
  induction h with
  | refl => rfl
  | tail _ hbc ih => exact ih.head hbc

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

Goal state before:
pp: case inr
α : Type u
f : α → α
m n : ℕ
a : α
hf : Injective f
ha : f^[m] a = f^[n] a
h : n ≤ m
⊢ f^[m - n] a = a

Tactic:
exact iterate_cancel_of_add hf (by rwa [Nat.sub_add_cancel h])

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

Goal state before:
pp: case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s✝ : β → β → Prop
x y : α × β
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Total s
x✝¹ x✝ : α × β
i : α
a : β
j : α
b : β
hji : r j i
⊢ Prod.Lex r s (i, a) (j, b) ∨ Prod.Lex r s (j, b) (i, a)

Tactic:
exact Or.inr (.left _ _ hji)

Goal state after:
Module: Mathlib.Order.OrderDual

Goal state before:
pp: α : Type u_1
inst✝ : LT α
T : Std.Trichotomous LT.lt
a b : αᵒᵈ
⊢ ¬a < b → ¬b < a → a = b

Tactic:
by rw [eq_comm]; exact T.trichotomous b a

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
a b : α
⊢ max a b = if a < b then b else a

Tactic:
by
  rw [max_comm, max_def, ← ite_not]; simp only [not_le]

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

Goal state before:
pp: case neg
α✝ : Type u
β : Type v
α : Type u_1
inst✝ : LE α
H : ∃ a, ∀ (b : α), b ≤ a
⊢ OrderTop α ⊕' NoTopOrder α

Tactic:
· letI : Top α := ⟨Classical.choose H⟩
    exact PSum.inl ⟨Classical.choose_spec H⟩

Goal state after:
Module: Mathlib.Order.PropInstances

Goal state before:
pp: case mp
ι : Type u_1
α' : ι → Type u_3
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → OrderBot (α' i)
f g : (i : ι) → α' i
⊢ Disjoint f g → ∀ (i : ι), Disjoint (f i) (g i)

Tactic:
intro h i x hf hg
    exact (update_le_iff.mp <| h (update_le_iff.mpr ⟨hf, fun _ _ => bot_le⟩)
      (update_le_iff.mpr ⟨hg, fun _ _ => bot_le⟩)).1

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
pr : α → Prop
Pinf : ∀ ⦃s t : α⦄, pr s → pr t → pr (s ⊓ t)
hbot : pr ⊥
a b : Subtype pr
this : SemilatticeInf (Subtype pr) := Subtype.semilatticeInf Pinf
⊢ Disjoint a b ↔ Disjoint ↑a ↑b

Tactic:
let : OrderBot (Subtype pr) := Subtype.orderBot hbot

Goal state after:
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
pr : α → Prop
Pinf : ∀ ⦃s t : α⦄, pr s → pr t → pr (s ⊓ t)
hbot : pr ⊥
a b : Subtype pr
this✝ : SemilatticeInf (Subtype pr) := Subtype.semilatticeInf Pinf
this : OrderBot (Subtype pr) := Subtype.orderBot hbot
⊢ Disjoint a b ↔ Disjoint ↑a ↑b
Module: Mathlib.Data.Set.Basic

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

Tactic:
rw [ssubset_def, Set.not_univ_subset, Set.nonempty_def]
  simp

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

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

Tactic:
rw [ssubset_def, Set.not_univ_subset, Set.nonempty_def]
  simp

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

Goal state before:
pp: f : ℕ → ℕ
hfmono : Antitone f
hfstab : ∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)
⊢ ∃ n, n ≤ f 0 ∧ ∀ (m : ℕ), n ≤ m → f m = f n

Tactic:
by
  induction h : f 0 using Nat.strongRecOn generalizing f with
  | ind n ih =>
    by_cases heq : f 0 = f 1
    · have flat (j : ℕ) : f j = f (j + 1) := by induction j with grind
      exact ⟨0, Nat.zero_le _, fun m _ => by induction m with grind⟩
    · have hlt : f 1 < f 0 := (hfmono (Nat.le_succ 0)).lt_of_ne' heq
      let g (i : ℕ) := f (i + 1)
      have hg_anti : Antitone g := by grind [Antitone]
      obtain ⟨p, hp, hp'⟩ := ih (f 1) (by grind) hg_anti (by grind) rfl
      refine ⟨p + 1, by omega, fun m hm => ?_⟩
      specialize hp' (m - 1) (by lia)
      grind

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
inst✝ : DistribLattice α
x y z : α
h₁ : x ⊓ z ≤ y ⊓ z
h₂ : x ⊔ z ≤ y ⊔ z
⊢ (y ⊔ x) ⊓ (z ⊔ x) = (y ⊔ x) ⊓ (x ⊔ z)

Tactic:
sup_comm x

Goal state after:
α : Type u
inst✝ : DistribLattice α
x y z : α
h₁ : x ⊓ z ≤ y ⊓ z
h₂ : x ⊔ z ≤ y ⊔ z
⊢ (y ⊔ x) ⊓ (z ⊔ x) = (y ⊔ x) ⊓ (z ⊔ x)
Module: Mathlib.Logic.Equiv.Option

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

Tactic:
cases h1 : e.symm (some (removeNoneAux e x))

Goal state after:
case none
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x : α
h1 : e.symm (some (e.removeNoneAux x)) = none
⊢ some (e.symm.removeNoneAux (e.removeNoneAux x)) = some x

case some
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x val✝ : α
h1 : e.symm (some (e.removeNoneAux x)) = some val✝
⊢ some (e.symm.removeNoneAux (e.removeNoneAux x)) = some x
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hi : Disjoint x z
hs : x ⊔ z = y
h : y ⊓ x = x
⊢ x ⊓ z = ⊥

Tactic:
hi.eq_bot

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hi : Disjoint x z
hs : x ⊔ z = y
h : y ⊓ x = x
⊢ ⊥ = ⊥
Module: Mathlib.Data.Sigma.Basic

Goal state before:
pp: α : Type u_1
β : α → Type u_4
γ : Type u_7
inst✝ : Nonempty γ
a b : α
f : γ → β a
g : γ → β b
h : mk a ∘ f = mk b ∘ g
i : γ
⊢ a = b ∧ f ≍ g

Tactic:
obtain rfl : a = b := congr_arg Sigma.fst (congr_fun h i)

Goal state after:
α : Type u_1
β : α → Type u_4
γ : Type u_7
inst✝ : Nonempty γ
a : α
f : γ → β a
i : γ
g : γ → β a
h : mk a ∘ f = mk a ∘ g
⊢ a = a ∧ f ≍ g
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
inst✝ : GeneralizedBooleanAlgebra α
a b c : α
⊢ a \ b ⊓ c = (a ⊓ c) \ (b ⊓ c)

Tactic:
inf_comm _ c,

Goal state after:
α : Type u
inst✝ : GeneralizedBooleanAlgebra α
a b c : α
⊢ c ⊓ a \ b = (c ⊓ a) \ (c ⊓ b)
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a : α
⊢ a \ ⊥ ⊔ ⊥ \ a = a

Tactic:
sdiff_bot,

Goal state after:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a : α
⊢ a ⊔ ⊥ \ a = a
Module: Mathlib.Order.SymmDiff

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

Tactic:
inf_comm _ c,

Goal state after:
α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b c : α
⊢ c ⊓ a ∆ b = (c ⊓ a) ∆ (c ⊓ b)
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ Prod.swap '' s ×ˢ t = t ×ˢ s

Tactic:
by
  rw [image_swap_eq_preimage_swap, preimage_swap_prod]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s s₁ s₂ : Set α
t t₁ t₂ : Set β
f₁ f₂ : α → β
inst✝ : (i : α) → Decidable (i ∈ s)
h₁ : MapsTo f₁ (s₁ ∩ s) (t₁ ∩ t)
h₂ : MapsTo f₂ (s₂ ∩ sᶜ) (t₂ ∩ tᶜ)
⊢ MapsTo (s.piecewise f₁ f₂) (s.ite s₁ s₂) (t.ite t₁ t₂)

Tactic:
by
  refine (h₁.congr ?_).union_union (h₂.congr ?_)
  exacts [(piecewise_eqOn s f₁ f₂).symm.mono inter_subset_right,
    (piecewise_eqOn_compl s f₁ f₂).symm.mono inter_subset_right]

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

Goal state before:
pp: case mp.h₂
α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
ht : t ⊆ range f
h : f ⁻¹' s = f ⁻¹' t
⊢ t ⊆ s

Tactic:
rw [← preimage_subset_preimage_iff ht, h]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
⊢ Injective (s.piecewise f g) ↔ InjOn f s ∧ InjOn g sᶜ ∧ ∀ (x : α), x ∈ s → ∀ (y : α), ¬y ∈ s → f x ≠ g y

Tactic:
rw [← injOn_univ, ← union_compl_self s, injOn_union (@disjoint_compl_right _ _ s),
    (piecewise_eqOn s f g).injOn_iff, (piecewise_eqOn_compl s f g).injOn_iff]
  refine and_congr Iff.rfl (and_congr Iff.rfl <| forall₄_congr fun x hx y hy => ?_)
  rw [piecewise_eq_of_mem s f g hx, piecewise_eq_of_notMem s f g hy]

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
f : ι → α
inst✝ : Unique ι
⊢ range f = {f default}

Tactic:
by
  aesop (add simp [Unique.eq_default])

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 β
p : Set γ
f : α → β
g : β → γ
h : SurjOn (g ∘ f) s p
hr : MapsTo f s t
⊢ SurjOn g t p

Tactic:
by
  intro z hz
  obtain ⟨x, hx, rfl⟩ := h hz
  exact ⟨f x, hr hx, rfl⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : ¬a ∈ s
hfa : ¬f a ∈ t
h : BijOn f (insert a s) (insert (f a) t)
⊢ BijOn f s t

Tactic:
have := congrArg (· \ {f a}) (image_insert_eq ▸ h.image_eq)

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : ¬a ∈ s
hfa : ¬f a ∈ t
h : BijOn f (insert a s) (insert (f a) t)
this : insert (f a) (f '' s) \ {f a} = insert (f a) t \ {f a}
⊢ BijOn f s t
Module: Mathlib.Data.Int.Init

Goal state before:
pp: a : ℤ
⊢ (-a.pred).pred = -a

Tactic:
by rw [neg_pred, pred_succ]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
b : β
inst✝ : Nonempty α
h : ¬∃ a, a ∈ s ∧ f a = b
⊢ invFunOn f s b = Classical.choice inst✝

Tactic:
rw [invFunOn, dif_neg h]

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
m n : ℕ
a : M
h : m ≤ n
⊢ a ^ m * a ^ (n - m) = a ^ n

Tactic:
rw [← pow_add, Nat.add_comm, Nat.sub_add_cancel h]

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✝ : InvOneClass M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
⊢ f 1⁻¹ = f 1

Tactic:
rw [inv, one, inv_one]

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

Goal state before:
pp: 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 : ℤ
⊢ P (g ^ n)

Tactic:
by
  induction n with
  | zero => rwa [zpow_zero]
  | succ n ih =>
    rw [Int.add_comm, zpow_add, zpow_one]
    exact h_mul _ ih
  | pred n ih =>
    rw [Int.sub_eq_add_neg, Int.add_comm, zpow_add, zpow_neg_one]
    exact h_inv _ ih

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

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

Tactic:
inv_mul,

Goal state after:
α : Type u
inst✝ : Monoid α
a : αˣ
⊢ ↑a * ↑a⁻¹ = 1
Module: Mathlib.Algebra.Group.Units.Defs

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

Tactic:
inv_mul,

Goal state after:
α : Type u
inst✝ : Monoid α
a : αˣ
b : α
⊢ 1 * b = b
Module: Mathlib.Algebra.Group.Units.Defs

Goal state before:
pp: α : Type u
inst✝ : Monoid α
a✝ b u : αˣ
n : ℕ
a : αˣ
⊢ a ^ (n + 1) = a ^ n * a

Tactic:
simp only [HPow.hPow, Pow.pow]; ext; simp [pow_succ]

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

Goal state before:
pp: α : Type u
inst✝ : Monoid α
a : α
u : αˣ
⊢ a * (↑u⁻¹ * ↑u) = a

Tactic:
rw [Units.inv_mul, mul_one]

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

Goal state before:
pp: α : Type u
inst✝ : DivisionMonoid α
a b : α
ha : IsUnit a
hb : IsUnit b
⊢ IsUnit (a * b⁻¹)

Tactic:
exact ha.mul hb.inv

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

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

Tactic:
inv_mul,

Goal state after:
α : Type u
inst✝ : Monoid α
a : α
b : αˣ
⊢ a * 1 = a
Module: Mathlib.Algebra.Group.Units.Basic

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

Tactic:
simpa only [mul_inv_cancel_right] using congr_arg (fun x : α => x * ↑(a⁻¹ : αˣ)) h

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

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

Tactic:
exact ⟨Eq.symm, Eq.symm⟩

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

Goal state before:
pp: M₀ : Type u_1
M₀' : Type u_3
inst✝⁴ : Mul M₀
inst✝³ : Zero M₀
inst✝² : Mul M₀'
inst✝¹ : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst✝ : IsLeftCancelMulZero M₀'
a✝ : M₀
Hne : a✝ ≠ 0
x✝¹ x✝ : M₀
He : (fun x ↦ a✝ * x) x✝¹ = (fun x ↦ a✝ * x) x✝
this : f a✝ * f x✝¹ = f a✝ * f x✝
Hfa : f a✝ = 0
⊢ f a✝ = f 0

Tactic:
Hfa,

Goal state after:
M₀ : Type u_1
M₀' : Type u_3
inst✝⁴ : Mul M₀
inst✝³ : Zero M₀
inst✝² : Mul M₀'
inst✝¹ : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst✝ : IsLeftCancelMulZero M₀'
a✝ : M₀
Hne : a✝ ≠ 0
x✝¹ x✝ : M₀
He : (fun x ↦ a✝ * x) x✝¹ = (fun x ↦ a✝ * x) x✝
this : f a✝ * f x✝¹ = f a✝ * f x✝
Hfa : f a✝ = 0
⊢ 0 = f 0
Module: Mathlib.Algebra.GroupWithZero.InjSurj

Goal state before:
pp: M₀ : Type u_1
M₀' : Type u_3
inst✝⁴ : Mul M₀
inst✝³ : Zero M₀
inst✝² : Mul M₀'
inst✝¹ : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst✝ : IsRightCancelMulZero M₀'
a✝ : M₀
Hne : a✝ ≠ 0
x✝¹ x✝ : M₀
He : (fun x ↦ x * a✝) x✝¹ = (fun x ↦ x * a✝) x✝
this : f x✝¹ * f a✝ = f x✝ * f a✝
Hfa : f a✝ = 0
⊢ f a✝ = f 0

Tactic:
Hfa,

Goal state after:
M₀ : Type u_1
M₀' : Type u_3
inst✝⁴ : Mul M₀
inst✝³ : Zero M₀
inst✝² : Mul M₀'
inst✝¹ : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst✝ : IsRightCancelMulZero M₀'
a✝ : M₀
Hne : a✝ ≠ 0
x✝¹ x✝ : M₀
He : (fun x ↦ x * a✝) x✝¹ = (fun x ↦ x * a✝) x✝
this : f x✝¹ * f a✝ = f x✝ * f a✝
Hfa : f a✝ = 0
⊢ 0 = f 0
Module: Mathlib.Data.Nat.Cast.Defs

Goal state before:
pp: case ind.succ
R : Type u_1
inst✝ : AddMonoidWithOne R
k : ℕ
hk : ∀ (m : ℕ), m < k + 1 → m.binCast = ↑m
⊢ (k + 1).binCast = ↑(k + 1)

Tactic:
Nat.binCast

Goal state after:
case ind.succ
R : Type u_1
inst✝ : AddMonoidWithOne R
k : ℕ
hk : ∀ (m : ℕ), m < k + 1 → m.binCast = ↑m
⊢ (if (k + 1) % 2 = 0 then ((k + 1) / 2).binCast + ((k + 1) / 2).binCast
    else ((k + 1) / 2).binCast + ((k + 1) / 2).binCast + 1) =
    ↑(k + 1)
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 A
inst✝² : SMulZeroClass M A
inst✝¹ : Zero B
inst✝ : SMul M B
f : ZeroHom A B
smul : ∀ (c : M) (x : A), f (c • x) = c • f x
c : M
⊢ c • 0 = 0

Tactic:
← map_zero f,

Goal state after:
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 A
inst✝² : SMulZeroClass M A
inst✝¹ : Zero B
inst✝ : SMul M B
f : ZeroHom A B
smul : ∀ (c : M) (x : A), f (c • x) = c • f x
c : M
⊢ c • f 0 = f 0
Module: Mathlib.Algebra.Ring.Defs

Goal state before:
pp: α : Type u
R : Type v
inst✝ : NonUnitalNonAssocRing α
a b : α
⊢ a * -b + a * b = 0

Tactic:
← left_distrib,

Goal state after:
α : Type u
R : Type v
inst✝ : NonUnitalNonAssocRing α
a b : α
⊢ a * (-b + b) = 0
Module: Mathlib.Algebra.Group.Int.Even

Goal state before:
pp: m✝ n✝ m n : ℤ
h : Even m
⊢ ¬Even (n + 3) ↔ Even (m ^ 2 + m + n)

Tactic:
by
  simp +decide [*, parity_simps]

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

Goal state before:
pp: M : Type u_1
inst✝ : AddMonoid M
f : ℕ →+ M
n : ℕ
⊢ f n = n • f 1

Tactic:
← multiplesHom_symm_apply,

Goal state after:
M : Type u_1
inst✝ : AddMonoid M
f : ℕ →+ M
n : ℕ
⊢ f n = n • (multiplesHom M).symm f
Module: Mathlib.Algebra.Divisibility.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
m n : ℕ
a : α
h : m ≤ n
⊢ a ^ n = a ^ m * a ^ (n - m)

Tactic:
rw [← pow_add, Nat.add_comm, Nat.sub_add_cancel h]

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

Goal state before:
pp: M₀ : Type u_2
inst✝¹ : MonoidWithZero M₀
inst✝ : Nontrivial M₀
x : M₀
⊢ x⁻¹ʳ ≠ 0 → IsUnit x

Tactic:
simpa using mt <| Ring.inverse_non_unit (x := x)

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

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
a b : α
u₁ u₂ : αˣ
⊢ a * ↑u₁⁻¹ + ↑u₂⁻¹ * b = a * 1 * ↑u₁⁻¹ + ↑u₂⁻¹ * (↑u₁⁻¹ * ↑u₁) * b

Tactic:
inv_mul,

Goal state after:
α : Type u
inst✝ : CommSemiring α
a b : α
u₁ u₂ : αˣ
⊢ a * ↑u₁⁻¹ + ↑u₂⁻¹ * b = a * 1 * ↑u₁⁻¹ + ↑u₂⁻¹ * 1 * b
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs

Goal state before:
pp: case refine_2
N : Type u_2
r : N → N → Prop
inst✝ : Group N
h : Contravariant N N (fun x1 x2 ↦ x1 * x2) r
a b c : N
bc : r b c
⊢ r ((fun x1 x2 ↦ x1 * x2) a b) ((fun x1 x2 ↦ x1 * x2) a c)

Tactic:
rw [← inv_mul_cancel_left a b, ← inv_mul_cancel_left a c] at bc

Goal state after:
case refine_2
N : Type u_2
r : N → N → Prop
inst✝ : Group N
h : Contravariant N N (fun x1 x2 ↦ x1 * x2) r
a b c : N
bc : r (a⁻¹ * (a * b)) (a⁻¹ * (a * c))
⊢ r ((fun x1 x2 ↦ x1 * x2) a b) ((fun x1 x2 ↦ x1 * x2) a c)
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic

Goal state before:
pp: α : Type u_1
inst✝² : MulOneClass α
inst✝¹ : LinearOrder α
inst✝ : MulLeftStrictMono α
a : α
⊢ ∃ b, b * b ≤ a

Tactic:
by_cases! h : a < 1
  · use a
    have : a * a < a * 1 := mul_lt_mul_right h a
    rw [mul_one] at this
    exact le_of_lt this
  · use 1
    rwa [mul_one]

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

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
n : ℕ
⊢ OfNat.ofNat n = ↑n

Tactic:
by
  match n with
  | 0 => simp
  | 1 => simp
  | n + 2 => rfl

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 : R
inst✝³ : ExistsAddOfLE R
inst✝² : PosMulStrictMono R
inst✝¹ : AddRightStrictMono R
inst✝ : AddRightReflectLT R
h : b < a
hc : c < 0
⊢ c * a < c * b

Tactic:
by
  obtain ⟨d, hcd⟩ := exists_add_of_le hc.le
  refine (add_lt_add_iff_right (d * b + d * a)).1 ?_
  calc
    _ = d * b := by rw [add_left_comm, ← add_mul, ← hcd, zero_mul, add_zero]
    _ < d * a := mul_lt_mul_of_pos_left h <| hcd.trans_lt <| add_lt_of_neg_left _ hc
    _ = _ := by rw [← add_assoc, ← add_mul, ← hcd, zero_mul, zero_add]

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 : G₀
hc : 0 < c
⊢ a < b / c ↔ c * a < b

Tactic:
by
  rw [lt_div_iff₀ hc, mul_comm]

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 : α
⊢ (a ⊓ b) ^ 2 = a * b / |b / a|ₘ

Tactic:
by
  rw [← inf_mul_sup a b, ← sup_div_inf_eq_mabs_div, div_eq_mul_inv, div_eq_mul_inv, mul_inv_rev,
    inv_inv, mul_assoc, mul_inv_cancel_comm_assoc, ← pow_two]

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

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

Tactic:
simp [hb, hc]

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

Goal state before:
pp: n p q : ℕ
dvd : ∃ x y, ↑n = ↑(p + 1) * x + ↑(q + 1) * y
le : p * q ≤ n
a_n b_n : ℤ
eq : ↑n = ↑(p + 1) * a_n + ↑(q + 1) * b_n
a : ℤ := a_n % ↑q.succ
b : ℤ := b_n + a_n / ↑q.succ * ↑p.succ
this : a * ↑p.succ + b * ↑q.succ = ↑n
hb : b ≤ -1
ha : a_n % ↑q.succ < ↑(↑q.succ).natAbs
⊢ ↑(p * q) ≤ ↑n

Tactic:
Nat.cast_le

Goal state after:
n p q : ℕ
dvd : ∃ x y, ↑n = ↑(p + 1) * x + ↑(q + 1) * y
le : p * q ≤ n
a_n b_n : ℤ
eq : ↑n = ↑(p + 1) * a_n + ↑(q + 1) * b_n
a : ℤ := a_n % ↑q.succ
b : ℤ := b_n + a_n / ↑q.succ * ↑p.succ
this : a * ↑p.succ + b * ↑q.succ = ↑n
hb : b ≤ -1
ha : a_n % ↑q.succ < ↑(↑q.succ).natAbs
⊢ p * q ≤ n
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
b : α
hb : b ≠ ⊤
a : α
⊢ a + b + -b = a

Tactic:
by
  simp [add_assoc, add_neg_cancel_of_ne_top hb]

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

Goal state before:
pp: case none.none
α : Type u
inst✝ : Add α
a : α
ha : IsAddLeftRegular a
⊢ (fun x ↦ ↑a + x) none = (fun x ↦ ↑a + x) none → none = none

Tactic:
simp [none_eq_top, some_eq_coe, ← coe_add, ha.eq_iff]

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

Goal state before:
pp: case none.some
α : Type u
inst✝ : Add α
a : α
ha : IsAddLeftRegular a
c : α
⊢ (fun x ↦ ↑a + x) none = (fun x ↦ ↑a + x) (Option.some c) → none = Option.some c

Tactic:
simp [none_eq_top, some_eq_coe, ← coe_add, ha.eq_iff]

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

Goal state before:
pp: case some.none
α : Type u
inst✝ : Add α
a : α
ha : IsAddLeftRegular a
b : α
⊢ (fun x ↦ ↑a + x) (Option.some b) = (fun x ↦ ↑a + x) none → Option.some b = none

Tactic:
simp [none_eq_top, some_eq_coe, ← coe_add, ha.eq_iff]

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

Goal state before:
pp: case some.some
α : Type u
inst✝ : Add α
a : α
ha : IsAddLeftRegular a
b c : α
⊢ (fun x ↦ ↑a + x) (Option.some b) = (fun x ↦ ↑a + x) (Option.some c) → Option.some b = Option.some c

Tactic:
simp [none_eq_top, some_eq_coe, ← coe_add, ha.eq_iff]

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

Goal state before:
pp: case none.none
α : Type u
inst✝ : Add α
a : α
ha : IsAddRightRegular a
⊢ (fun x ↦ x + ↑a) none = (fun x ↦ x + ↑a) none → none = none

Tactic:
simp [none_eq_top, some_eq_coe, ← coe_add, ha.eq_iff]

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

Goal state before:
pp: case none.some
α : Type u
inst✝ : Add α
a : α
ha : IsAddRightRegular a
c : α
⊢ (fun x ↦ x + ↑a) none = (fun x ↦ x + ↑a) (Option.some c) → none = Option.some c

Tactic:
simp [none_eq_top, some_eq_coe, ← coe_add, ha.eq_iff]

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

Goal state before:
pp: case some.none
α : Type u
inst✝ : Add α
a : α
ha : IsAddRightRegular a
b : α
⊢ (fun x ↦ x + ↑a) (Option.some b) = (fun x ↦ x + ↑a) none → Option.some b = none

Tactic:
simp [none_eq_top, some_eq_coe, ← coe_add, ha.eq_iff]

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

Goal state before:
pp: case some.some
α : Type u
inst✝ : Add α
a : α
ha : IsAddRightRegular a
b c : α
⊢ (fun x ↦ x + ↑a) (Option.some b) = (fun x ↦ x + ↑a) (Option.some c) → Option.some b = Option.some c

Tactic:
simp [none_eq_top, some_eq_coe, ← coe_add, ha.eq_iff]

Goal state after: