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

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
a : M
⊢ a ^ 1 = a

Tactic:
rw [pow_succ, pow_zero, one_mul]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a✝ b✝ a b c : G
h : (fun x ↦ a * x) b = (fun x ↦ a * x) c
⊢ b = c

Tactic:
← inv_mul_cancel_left a b,

Goal state after:
G : Type u_1
inst✝ : Group G
a✝ b✝ a b c : G
h : (fun x ↦ a * x) b = (fun x ↦ a * x) c
⊢ a⁻¹ * (a * b) = c
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
a b : α
p : Prop
⊢ p ∧ a = b ↔ p ∧ b = a

Tactic:
by simp [eq_comm]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
a b : α
p : Prop
⊢ a = b ∧ p ↔ b = a ∧ p

Tactic:
by simp [eq_comm]

Goal state after:
Module: Mathlib.Logic.Relation

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

Tactic:
exact .rel _ _ h

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

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

Tactic:
obtain h | h := Nat.le_total m n

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

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
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: α : Type u_5
β : Type u_6
inst✝⁵ : Mul α
inst✝⁴ : Mul β
inst✝³ : SMul α β
inst✝² : IsScalarTower α β β
inst✝¹ : IsScalarTower α α β
inst✝ : SMulCommClass α β β
a : α
b : β
c : α
d : β
⊢ a • b * c • d = (a * c) • (b * d)

Tactic:
have : SMulCommClass β α β := .symm ..; exact smul_smul_smul_comm a b c d

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

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

Tactic:
exact (trichotomous_of (s) a b).imp3 (Lex.right _) (congr_arg _) (Lex.right _)

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
A B : PartialOrder α
H : ∀ (x y : α), x < y ↔ x < y
x y : α
⊢ x ≤ y ↔ x < y ∨ x = y

Tactic:
@le_iff_lt_or_eq _ A,

Goal state after:
α : Type u_2
A B : PartialOrder α
H : ∀ (x y : α), x < y ↔ x < y
x y : α
⊢ x < y ∨ x = y ↔ x < y ∨ x = y
Module: Mathlib.Order.Basic

Goal state before:
pp: case inr
ι : 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₂
      exact ⟨(_, c), Or.inr ⟨h₁, ha⟩, Or.inr ⟨le_rfl, hb⟩⟩

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

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

Tactic:
· simp [dvd_sub_iff_left (le_of_lt h) (Nat.dvd_refl _), h.not_ge]

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

Goal state before:
pp: case succ
a : ℕ
ha : a ≠ 1
b : ℕ
⊢ a * (b + 1) ≤ a ^ (b + 1)

Tactic:
obtain rfl | ha0 : a = 0 ∨ a > 0 := a.eq_zero_or_pos

Goal state after:
case succ.inl
b : ℕ
ha : 0 ≠ 1
⊢ 0 * (b + 1) ≤ 0 ^ (b + 1)

case succ.inr
a : ℕ
ha : a ≠ 1
b : ℕ
ha0 : a > 0
⊢ a * (b + 1) ≤ a ^ (b + 1)
Module: Mathlib.Order.RelClasses

Goal state before:
pp: α : Type u
β : Type v
r✝ : α → α → Prop
s : β → β → Prop
r : α → α → Prop
inst✝ : IsStrictOrder α r
x y : α
h : r x y
e : y = x
⊢ False

Tactic:
e

Goal state after:
α : Type u
β : Type v
r✝ : α → α → Prop
s : β → β → Prop
r : α → α → Prop
inst✝ : IsStrictOrder α r
x y : α
h : r x x
e : y = x
⊢ False
Module: Mathlib.Order.RelClasses

Goal state before:
pp: α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝³ : Preorder α
inst✝² : WellFoundedLT α
inst✝¹ : Preorder β
inst✝ : WellFoundedLT β
a a' : α
ha : a' ≤ a
b : β
⊢ Acc (fun x1 x2 ↦ x1 < x2) (a', b)

Tactic:
induction a using WellFoundedLT.induction generalizing a' b with | ind a iha
     =>  _ 

Goal state after:
case ind
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝³ : Preorder α
inst✝² : WellFoundedLT α
inst✝¹ : Preorder β
inst✝ : WellFoundedLT β
a : α
iha : ∀ (y : α), y < a → ∀ (a' : α), a' ≤ y → ∀ (b : β), Acc (fun x1 x2 ↦ x1 < x2) (a', b)
a' : α
ha : a' ≤ a
b : β
⊢ Acc (fun x1 x2 ↦ x1 < x2) (a', b)
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
h : Disjoint f g
i : ι
⊢ Disjoint (f i) (g i)

Tactic:
x

Goal state after:
case mp
ι : Type u_1
α' : ι → Type u_3
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → OrderBot (α' i)
f g : (i : ι) → α' i
h : Disjoint f g
i : ι
x : α' i
⊢ x ≤ f i → x ≤ g i → x ≤ ⊥
Module: Mathlib.Order.PropInstances

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

Tactic:
x

Goal state after:
case mpr
ι : Type u_1
α' : ι → Type u_3
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → OrderBot (α' i)
f g : (i : ι) → α' i
h : ∀ (i : ι), Disjoint (f i) (g i)
x : (i : ι) → α' i
⊢ x ≤ f → x ≤ g → x ≤ ⊥
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: α : Type u
inst✝ : Preorder α
f : ℕ → α
k : ℕ
⊢ (Monotone fun n ↦ f (n + k)) ↔ MonotoneOn f {x | k ≤ x}

Tactic:
refine ⟨fun h x hx y hy hle ↦ ?_, fun h x y hle ↦ ?_⟩
  · rw [← Nat.sub_add_cancel hx, ← Nat.sub_add_cancel hy]
    rw [← Nat.sub_le_sub_iff_right hy] at hle
    exact h hle
  · rw [← Nat.add_le_add_iff_right] at hle
    exact h (Nat.le_add_left k x) (Nat.le_add_left k y) hle

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

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

Tactic:
contrapose! hfb
    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
    exact ⟨b + 1, strictMono _ le_rfl⟩

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

Goal state before:
pp: case mp
α : Type u
s : Set α
⊢ Subsingleton ↑s → s.Subsingleton

Tactic:
intro h a ha b hb
    exact SetCoe.ext_iff.2 (@Subsingleton.elim s h ⟨a, ha⟩ ⟨b, hb⟩)

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

Goal state before:
pp: α : Type u_1
s t : Set α
h : t ⊆ s
⊢ sᶜ ⊆ tᶜ

Tactic:
by gcongr

Goal state after:
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)) <;> cases h2 : e (some x)
      · rw [removeNoneAux_none _ h1]
        exact (e.eq_symm_apply.mpr h2).symm
      · rw [removeNoneAux_some _ ⟨_, h2⟩] at h1
        simp at h1
      · rw [removeNoneAux_none _ h2] at h1
        simp at h1
      · rw [removeNoneAux_some _ ⟨_, h1⟩]
        rw [removeNoneAux_some _ ⟨_, h2⟩]
        simp

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedHeytingAlgebra β
lattice : Lattice α := e.lattice
top : Top α := e.top
himp : HImp α := e.himp
⊢ GeneralizedHeytingAlgebra α

Tactic:
apply e.injective.generalizedHeytingAlgebra <;> intros

Goal state after:
case le
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedHeytingAlgebra β
lattice : Lattice α := e.lattice
top : Top α := e.top
himp : HImp α := e.himp
x✝ y✝ : α
⊢ e x✝ ≤ e y✝ ↔ x✝ ≤ y✝

case lt
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedHeytingAlgebra β
lattice : Lattice α := e.lattice
top : Top α := e.top
himp : HImp α := e.himp
x✝ y✝ : α
⊢ e x✝ < e y✝ ↔ x✝ < y✝

case map_sup
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedHeytingAlgebra β
lattice : Lattice α := e.lattice
top : Top α := e.top
himp : HImp α := e.himp
a✝ b✝ : α
⊢ e (a✝ ⊔ b✝) = e a✝ ⊔ e b✝

case map_inf
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedHeytingAlgebra β
lattice : Lattice α := e.lattice
top : Top α := e.top
himp : HImp α := e.himp
a✝ b✝ : α
⊢ e (a✝ ⊓ b✝) = e a✝ ⊓ e b✝

case map_top
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedHeytingAlgebra β
lattice : Lattice α := ⋯
top : Top α := ⋯
himp : HImp α := ⋯
⊢ e ⊤ = ⊤

case map_himp
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedHeytingAlgebra β
lattice : Lattice α := e.lattice
top : Top α := e.top
himp : HImp α := e.himp
a✝ b✝ : α
⊢ e (a✝ ⇨ b✝) = e a✝ ⇨ e b✝
Module: Mathlib.Order.SymmDiff

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

Tactic:
compl_sdiff_compl,

Goal state after:
α : Type u_2
inst✝ : BooleanAlgebra α
a b : α
⊢ a \ b ⊔ b \ a = a ∆ b
Module: Mathlib.Data.Set.Image

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
f : α → β
s s' : Set β
r : range f ∩ s ⊆ range f ∩ s'
⊢ f ⁻¹' s ⊆ f ⁻¹' s'

Tactic:
x

Goal state after:
case mp
α : Type u_1
β : Type u_2
f : α → β
s s' : Set β
r : range f ∩ s ⊆ range f ∩ s'
x : α
⊢ x ∈ f ⁻¹' s → x ∈ f ⁻¹' s'
Module: Mathlib.Data.Set.Image

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
f : α → β
s s' : Set β
r : f ⁻¹' s ⊆ f ⁻¹' s'
⊢ range f ∩ s ⊆ range f ∩ s'

Tactic:
x

Goal state after:
case mpr
α : Type u_1
β : Type u_2
f : α → β
s s' : Set β
r : f ⁻¹' s ⊆ f ⁻¹' s'
x : β
⊢ x ∈ range f ∩ s → x ∈ range f ∩ s'
Module: Mathlib.Data.Set.Image

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

Tactic:
x

Goal state after:
case mp
α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
h : f ⁻¹' s ⊆ f ⁻¹' t
x : α
⊢ x ∈ s → x ∈ t
Module: Mathlib.Data.Set.Image

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

Tactic:
x

Goal state after:
case mpr
α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
h : s ⊆ t
x : β
⊢ x ∈ f ⁻¹' s → x ∈ f ⁻¹' t
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
⊢ s ×ˢ t = s₁ ×ˢ t₁ ↔ s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅)

Tactic:
symm
  rcases eq_empty_or_nonempty (s ×ˢ t) with h | h
  · simp_rw [h, @eq_comm _ ∅, prod_eq_empty_iff, prod_eq_empty_iff.mp h, true_and,
      or_iff_right_iff_imp]
    rintro ⟨rfl, rfl⟩
    exact prod_eq_empty_iff.mp h
  rw [prod_eq_prod_iff_of_nonempty h]
  rw [nonempty_iff_ne_empty, Ne, prod_eq_empty_iff] at h
  simp_rw [h, false_and, or_false]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set (α ⊕ β)
⊢ Sum.inl '' Sum.inl ⁻¹' s ∪ Sum.inr '' Sum.inr ⁻¹' s = s

Tactic:
rw [← preimage_sumElim, Sum.elim_inl_inr, preimage_id]

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

Goal state before:
pp: case mpr
α : Type u_1
s t u : Set α
h : s ∩ t ⊆ s ∩ u
⊢ val ⁻¹' t ⊆ val ⁻¹' u

Tactic:
x

Goal state after:
case mpr
α : Type u_1
s t u : Set α
h : s ∩ t ⊆ s ∩ u
x : ↑s
⊢ x ∈ val ⁻¹' t → x ∈ val ⁻¹' u
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: case refine_2.inr
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
inst✝ : DecidableEq ι
f : (i : ι) → α i
hi : i ∈ s
hf : ∀ (j : ι), j ∈ s → j ≠ i → f j ∈ t j
x : α i
hx : x ∈ t i
j : ι
hj : j ∈ s
h : j ≠ i
⊢ update f i x j ∈ t j

Tactic:
· rw [update_of_ne h]
      exact hf j hj h

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

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

Tactic:
intro b hb

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
f : α → β
g₁ g₂ : β → γ
hf : EqOn (g₁ ∘ f) (g₂ ∘ f) s
hf' : SurjOn f s t
b : β
hb : b ∈ t
⊢ g₁ b = g₂ b
Module: Mathlib.Algebra.Group.Hom.Defs

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
F : Type u_9
inst✝¹ : One M
inst✝ : One N
f : OneHom M N
g : N → M
h₁ : LeftInverse g ⇑f
⊢ g 1 = 1

Tactic:
by rw [← f.map_one, h₁]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
inst✝ : Nonempty α
h : SurjOn f s t
⊢ BijOn f (invFunOn f s '' t) t

Tactic:
refine h.invOn_invFunOn.bijOn ?_ (mapsTo_image _ _)

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
inst✝ : Nonempty α
h : SurjOn f s t
⊢ MapsTo f (invFunOn f s '' t) 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✝¹ : 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
n : ℕ
x : M₁
⊢ f (x ^ (n + 1)) = f (x ^ n * x)

Tactic:
by rw [npow, pow_succ, mul, npow]

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⁻¹ * b = c
⊢ b = a * c

Tactic:
rw [← h, mul_inv_cancel_left]

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

Goal state before:
pp: α : Type u
inst✝ : Monoid α
u₁ u₂ : αˣ
⊢ u₂.inv * (u₁.inv * (↑u₁ * ↑u₂)) = 1

Tactic:
← mul_assoc u₁.inv,

Goal state after:
α : Type u
inst✝ : Monoid α
u₁ u₂ : αˣ
⊢ u₂.inv * (u₁.inv * ↑u₁ * ↑u₂) = 1
Module: Mathlib.Algebra.Group.Units.Defs

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

Tactic:
rw [← h, mul_inv_cancel_left]

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

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

Tactic:
rw [← mul_inv_eq_one, inv_inv]

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✝² : MulZeroClass M₀
inst✝¹ : Mul M₀'
inst✝ : Zero M₀'
f : M₀' → M₀
hf : Injective f
zero : f 0 = 0
mul : ∀ (a b : M₀'), f (a * b) = f a * f b
a : M₀'
⊢ f (a * 0) = f 0

Tactic:
simp only [mul, zero, mul_zero]

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

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

Tactic:
Nat.cast_one

Goal state after:
R : Type u_1
inst✝ : AddMonoidWithOne R
n : ℕ
⊢ 1 + ↑n = 1 + ↑n
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✝⁶ : MonoidWithZero M₀
inst✝⁵ : MonoidWithZero M₀'
inst✝⁴ : Zero A
inst✝³ : MulActionWithZero M₀ A
inst✝² : Zero A'
inst✝¹ : SMul M₀ A'
p : Prop
inst✝ : Decidable p
f : M₀' →*₀ M₀
r s : M₀'
m : A
⊢ (r * s) • m = r • s • m

Tactic:
change f (r * s) • m = f r • f s • m; simp [mul_smul]

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

Goal state before:
pp: R : Type u
inst✝ : AddGroupWithOne R
n : ℕ
x✝ : 0 < n + 1
⊢ ↑(n + 1 - 1) = ↑(n + 1) - 1

Tactic:
by rw [cast_succ, add_sub_cancel_right, Nat.add_sub_cancel_right]

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

Goal state before:
pp: R : Type u
inst✝ : AddGroupWithOne R
⊢ ↑1 = 1

Tactic:
Nat.cast_one

Goal state after:
R : Type u
inst✝ : AddGroupWithOne R
⊢ 1 = 1
Module: Mathlib.Algebra.Group.Even

Goal state before:
pp: α : Type u_2
inst✝ : Group α
n : ℤ
⊢ Even n → ∀ (a : α), IsSquare (a ^ n)

Tactic:
aesop (add simp zpow_add)

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝ : Inhabited α
h : ¬Nontrivial α
x : α
⊢ x = default

Tactic:
by
          by_contra H
          exact h ⟨_, _, H⟩

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

Goal state before:
pp: M₀ : Type u_2
inst✝ : MonoidWithZero M₀
x y : M₀
h : IsUnit x
⊢ y * x⁻¹ʳ * x = y

Tactic:
rw [mul_assoc, inverse_mul_cancel x h, mul_one]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
a b : R
h : Commute a b
⊢ a * a - b * b = (a + b) * (a - b)

Tactic:
h.mul_self_sub_mul_self_eq

Goal state after:
R : Type u
inst✝ : Ring R
a b : R
h : Commute a b
⊢ (a + b) * (a - b) = (a + b) * (a - b)
Module: Mathlib.Algebra.Ring.Commute

Goal state before:
pp: R : Type u
inst✝ : CommRing R
a b : R
⊢ a ^ 2 + 2 * a * -b + (-b) ^ 2 = a ^ 2 - 2 * a * b + b ^ 2

Tactic:
neg_sq,

Goal state after:
R : Type u
inst✝ : CommRing R
a b : R
⊢ a ^ 2 + 2 * a * -b + b ^ 2 = a ^ 2 - 2 * a * b + b ^ 2
Module: Mathlib.Algebra.Ring.Commute

Goal state before:
pp: R : Type u
inst✝ : CommRing R
a b : R
⊢ a ^ 2 + (-b) ^ 2 + 2 * a * -b = a ^ 2 + b ^ 2 - 2 * a * b

Tactic:
neg_sq,

Goal state after:
R : Type u
inst✝ : CommRing R
a b : R
⊢ a ^ 2 + b ^ 2 + 2 * a * -b = a ^ 2 + b ^ 2 - 2 * a * b
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs

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

Tactic:
← inv_mul_cancel_left a b,

Goal state after:
case refine_1
N : Type u_2
r : N → N → Prop
inst✝ : Group N
h : Covariant N N (fun x1 x2 ↦ x1 * x2) r
a b c : N
bc : r ((fun x1 x2 ↦ x1 * x2) a b) ((fun x1 x2 ↦ x1 * x2) a c)
⊢ r (a⁻¹ * (a * b)) c
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:
← inv_mul_cancel_left a b,

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)) c
⊢ r ((fun x1 x2 ↦ x1 * x2) a b) ((fun x1 x2 ↦ x1 * x2) a c)
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝¹ : Monoid α
inst✝ : HasDistribNeg α
c : ℕ
a : α
⊢ ((-a) ^ 2) ^ c * (-a) ^ 1 = -((a ^ 2) ^ c * a ^ 1)

Tactic:
neg_sq,

Goal state after:
α : Type u_2
inst✝¹ : Monoid α
inst✝ : HasDistribNeg α
c : ℕ
a : α
⊢ (a ^ 2) ^ c * (-a) ^ 1 = -((a ^ 2) ^ c * a ^ 1)
Module: Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE

Goal state before:
pp: α : Type u
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : Monoid α
inst✝¹ : ExistsMulOfLE α
inst✝ : MulLeftReflectLT α
a b : α
h : ∀ (ε : α), 1 < ε → a ≤ b * ε
x : α
hxb : b < x
⊢ a ≤ x

Tactic:
obtain ⟨ε, rfl⟩ := exists_mul_of_le hxb.le

Goal state after:
α : Type u
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : Monoid α
inst✝¹ : ExistsMulOfLE α
inst✝ : MulLeftReflectLT α
a b : α
h : ∀ (ε : α), 1 < ε → a ≤ b * ε
ε : α
hxb : b < b * ε
⊢ a ≤ b * ε
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic

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

pp: case inr.inr.inr.inr
α : Type u_1
inst✝³ : Mul α
inst✝² : LinearOrder α
a b c d : α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
h : a * b = c * d
hca : c < a
hdb : d < b
⊢ a = c ∧ b = d ∨ a < c ∨ b < d

Tactic:
· exact False.elim <| ne_of_lt (mul_lt_mul_left hca b) h.symm

Goal state after:
case inr.inr.inr.inr
α : Type u_1
inst✝³ : Mul α
inst✝² : LinearOrder α
a b c d : α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
h : a * b = c * d
hca : c < a
hdb : d < b
⊢ a = c ∧ b = d ∨ a < c ∨ b < d
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝² : LE R
inst✝¹ : NonAssocSemiring R
inst✝ : AddLeftMono R
a : R
a1 : 1 ≤ a
⊢ a + 1 ≤ a + a

Tactic:
by gcongr

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✝³ : ZeroLEOneClass R
inst✝² : NeZero 1
inst✝¹ : MulPosStrictMono R
inst✝ : AddLeftMono R
a2 : 2 ≤ a
ab : a ≤ b
this : 0 < b
⊢ a + b ≤ b + b

Tactic:
by gcongr

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✝³ : ZeroLEOneClass R
inst✝² : NeZero 1
inst✝¹ : AddLeftMono R
inst✝ : PosMulStrictMono R
b2 : 2 ≤ b
ba : b ≤ a
this : 0 < a
⊢ a + b ≤ a + a

Tactic:
by gcongr

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
f : α ↪o β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
a₁ a₂ : α
h : Disjoint (f a₁) (f a₂)
⊢ Disjoint a₁ a₂

Tactic:
x

Goal state after:
α : Type u_2
β : Type u_3
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
f : α ↪o β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
a₁ a₂ : α
h : Disjoint (f a₁) (f a₂)
x : α
⊢ x ≤ a₁ → x ≤ a₂ → x ≤ ⊥
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

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

Tactic:
apply le_sup_right

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
hac : a ≤ b
hcd : b ≤ c
d : G
⊢ |b / d|ₘ ≤ max (c / d) (d / a)

Tactic:
rcases le_total d b with h | h
  · rw [mabs_of_one_le <| one_le_div'.mpr h]
    exact le_max_of_le_left <| div_le_div_right' hcd _
  · rw [mabs_of_le_one <| div_le_one'.mpr h, inv_div]
    exact le_max_of_le_right <| div_le_div_left' hac _

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a : G
n : ℤ
⊢ a ^ |n| = 1 ↔ a ^ n = 1

Tactic:
by
  rw [← Int.natCast_natAbs, zpow_natCast, pow_natAbs_eq_one]

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

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b c : α
this : DistribLattice α := CommGroup.toDistribLattice α
⊢ (b ⊔ a) * c / ((b ⊓ a ⊔ c) * (b ⊓ a ⊓ c)) = (b ⊔ a) * c / ((b ⊓ a) * c)

Tactic:
mul_comm (b ⊓ a ⊔ c),

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)
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
β : Type v
inst✝² : Add α
w x y z : WithTop α
a b : α
inst✝¹ : LE α
inst✝ : AddLeftMono α
a✝² a✝¹ a✝ : α
x✝ : a✝¹ ≤ a✝
⊢ a✝² + a✝¹ ≤ a✝² + a✝

Tactic:
by gcongr

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

Goal state before:
pp: α : Type u
β : Type v
inst✝² : Add α
w x y z : WithTop α
a b : α
inst✝¹ : LE α
inst✝ : AddRightMono α
a✝² a✝¹ a✝ : α
x✝ : a✝¹ ≤ a✝
⊢ a✝¹ + a✝² ≤ a✝ + a✝²

Tactic:
by gcongr

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

Goal state before:
pp: α : Type u
inst✝² : Add α
inst✝¹ : LT α
inst✝ : AddLeftStrictMono α
x a✝¹ a✝ : α
x✝ : a✝¹ < a✝
⊢ x + a✝¹ < x + a✝

Tactic:
by gcongr

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

Goal state before:
pp: α : Type u
inst✝² : Add α
inst✝¹ : LT α
inst✝ : AddRightStrictMono α
z a✝¹ a✝ : α
x✝ : a✝¹ < a✝
⊢ a✝¹ + z < a✝ + z

Tactic:
by gcongr

Goal state after: