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

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
a : M
m : ℕ
⊢ a ^ (m * 0) = (a ^ m) ^ 0

Tactic:
rw [Nat.mul_zero, pow_zero, pow_zero]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
P : α → Prop
⊢ (∀ (a : α), P a) ∨ ∃ a, ¬P a

Tactic:
by
  rw [← not_forall]; exact em _

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: P : Prop
inst✝ : Decidable P
Q : P → Prop
R : ¬P → Prop
⊢ dite P Q R ↔ (∃ p, Q p) ∨ ∃ p, R p

Tactic:
by_cases h : P <;> simp [h, exists_prop_of_false, exists_prop_of_true]

Goal state after:
Module: Mathlib.Data.Quot

Goal state before:
pp: α : Sort u_3
r : α → α → Prop
iseqv✝¹ : Equivalence r
p : α → α → Prop
iseqv✝ : Equivalence p
Eq : ∀ (a b : α), { r := r, iseqv := iseqv✝¹ } a b ↔ { r := p, iseqv := iseqv✝ } a b
⊢ { r := r, iseqv := iseqv✝¹ } = { r := p, iseqv := iseqv✝ }

Tactic:
by have : r = p := funext fun a ↦ funext fun b ↦ propext <| Eq a b
     subst this
     rfl

Goal state after:
Module: Mathlib.Data.Quot

Goal state before:
pp: ι : Type u_3
α : ι → Sort u_4
s : (i : ι) → Setoid (α i)
p : ((i : ι) → Quotient (s i)) → Prop
f : (i : ι) → Quotient (s i)
h : ∀ (a : (i : ι) → α i), p fun i ↦ ⟦a i⟧
⊢ p f

Tactic:
← (funext fun i ↦ Quotient.out_eq (f i) : (fun i ↦ ⟦(f i).out⟧) = f)

Goal state after:
ι : Type u_3
α : ι → Sort u_4
s : (i : ι) → Setoid (α i)
p : ((i : ι) → Quotient (s i)) → Prop
f : (i : ι) → Quotient (s i)
h : ∀ (a : (i : ι) → α i), p fun i ↦ ⟦a i⟧
⊢ p fun i ↦ ⟦(f i).out⟧
Module: Mathlib.Data.Option.Basic

Goal state before:
pp: p : Prop
inst✝ : Decidable p
u : Unit
⊢ _root_.guard p = some u ↔ p

Tactic:
by
  grind [cases Option, _root_.guard]

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ compare a b = Ordering.eq ↔ a = b

Tactic:
rw [LinearOrder.compare_eq_compareOfLessAndEq, compareOfLessAndEq_eq_eq le_refl not_le]

Goal state after:
Module: Mathlib.Tactic.Push

Goal state before:
pp: p q : Prop
⊢ ¬p ∧ q ∨ ¬¬p ∧ ¬q ↔ p ∧ ¬q ∨ ¬p ∧ q

Tactic:
not_not,

Goal state after:
p q : Prop
⊢ ¬p ∧ q ∨ p ∧ ¬q ↔ p ∧ ¬q ∨ ¬p ∧ q
Module: Mathlib.Order.BoundedOrder.Basic

Goal state before:
pp: α✝ : Type u
β : Type v
α : Type u_1
inst✝ : LE α
⊢ OrderTop α ⊕' NoTopOrder α

Tactic:
by_cases! H : ∀ a : α, ∃ b, ¬b ≤ a

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

case neg
α✝ : Type u
β : Type v
α : Type u_1
inst✝ : LE α
H : ∃ a, ∀ (b : α), b ≤ a
⊢ OrderTop α ⊕' NoTopOrder α
Module: Mathlib.Order.Disjoint

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
x y : α × β
⊢ Disjoint x y → Disjoint x.fst y.fst ∧ Disjoint x.snd y.snd

pp: case mpr
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
x y : α × β
⊢ Disjoint x.fst y.fst ∧ Disjoint x.snd y.snd → Disjoint x y

Tactic:
· intro h
    refine ⟨fun a hx hy ↦ (@h (a, ⊥) ⟨hx, ?_⟩ ⟨hy, ?_⟩).1,
      fun b hx hy ↦ (@h (⊥, b) ⟨?_, hx⟩ ⟨?_, hy⟩).2⟩
    all_goals exact bot_le

Goal state after:
case mpr
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
x y : α × β
⊢ Disjoint x.fst y.fst ∧ Disjoint x.snd y.snd → Disjoint x y
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: n : ℕ
ih :
  ∀ (m : ℕ),
    m < n →
      ∀ {f : ℕ → ℕ},
        Antitone f →
          (∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)) → f 0 = m → ∃ n, n ≤ m ∧ ∀ (m : ℕ), n ≤ m → f m = f n
f : ℕ → ℕ
hfmono : Antitone f
hfstab : ∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)
h : f 0 = n
heq : f 0 = f 1
flat : ∀ (j : ℕ), f j = f (j + 1)
m : ℕ
x✝ : 0 ≤ m
⊢ f m = f 0

Tactic:
by induction m with grind

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

Goal state before:
pp: α : Type u
p : Prop
inst✝ : Decidable p
t : p → Set α
x : α
⊢ (∀ (h : p), x ∈ t h) ∧ p ↔ ∃ h, x ∈ t h

Tactic:
exact ⟨fun h => ⟨h.2, h.1 h.2⟩, fun ⟨h₁, h₂⟩ => ⟨fun _ => h₂, h₁⟩⟩

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

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

Tactic:
simp only [Set.Nonempty, mem_inter_iff, mem_singleton_iff, exists_eq_left]

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α✝ : Type u
β : Type v
α : Type u_1
inst✝¹ : Max α
inst✝ : Min α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
sup_inf_self : ∀ (a b : α), a ⊔ a ⊓ b = a
inf_sup_self : ∀ (a b : α), a ⊓ (a ⊔ b) = a
sup_idem : ∀ (b : α), b ⊔ b = b
inf_idem : ∀ (b : α), b ⊓ b = b
semilatt_inf_inst : SemilatticeInf α := SemilatticeInf.mk' inf_comm inf_assoc inf_idem
semilatt_sup_inst : SemilatticeSup α := SemilatticeSup.mk' sup_comm sup_assoc sup_idem
partial_order_eq : semilatt_sup_inst.toPartialOrder = semilatt_inf_inst.toPartialOrder
a b c : α
⊢ a ≤ b → a ≤ c → a ≤ SemilatticeInf.inf b c

Tactic:
by
      rw [partial_order_eq]
      apply le_inf

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

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

Tactic:
rw [himp_himp, inf_idem]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
e₁ : α ≃ β
e₂ : β ≃ γ
⊢ (e₁.trans e₂).optionCongr = e₁.optionCongr.trans e₂.optionCongr

Tactic:
by
  ext x : 1
  symm
  apply Option.map_map

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

Goal state before:
pp: α : Type u_1
β : α → Type u_4
h : ∀ (a : α), Subsingleton (β a)
⊢ Injective fst

Tactic:
rintro ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ (rfl : a₁ = a₂)

Goal state after:
α : Type u_1
β : α → Type u_4
h : ∀ (a : α), Subsingleton (β a)
a₁ : α
b₁ b₂ : β a₁
⊢ ⟨a₁, b₁⟩ = ⟨a₁, b₂⟩
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x \ y ≤ x ∧ ¬x \ y = x ↔ ¬Disjoint y x

Tactic:
sdiff_eq_self_iff_disjoint,

Goal state after:
α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x \ y ≤ x ∧ ¬Disjoint y x ↔ ¬Disjoint y x
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ a ⊔ b ≤ (a ∆ b ⊔ a) ⊓ (a ∆ b ⊔ b)

Tactic:
symmDiff

Goal state after:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ a ⊔ b ≤ (a \ b ⊔ b \ a ⊔ a) ⊓ (a \ b ⊔ b \ a ⊔ b)
Module: Mathlib.Order.SymmDiff

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

Tactic:
rw [← symmDiff_sdiff_inf a, sdiff_symmDiff_eq_sup, symmDiff_sup_inf]

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c : α
⊢ a \ b ⊔ b \ a ⊔ (b \ c ⊔ c \ b) = a \ b ⊔ b \ a ⊔ b ∆ c

Tactic:
symmDiff

Goal state after:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c : α
⊢ a \ b ⊔ b \ a ⊔ (b \ c ⊔ c \ b) = a \ b ⊔ b \ a ⊔ (b \ c ⊔ c \ b)
Module: Mathlib.Data.Set.Image

Goal state before:
pp: case mp
α : Type u_1
s u v : Set α
hsuv : s ⊆ u ∪ v
H : s ∩ (u ∩ v) = ∅
x : α
x_in_s : x ∈ s
⊢ ⟨x, x_in_s⟩ ∈ Subtype.val ⁻¹' u → ⟨x, x_in_s⟩ ∈ (Subtype.val ⁻¹' v)ᶜ

Tactic:
intro x_in_u x_in_v
    exact eq_empty_iff_forall_notMem.mp H x ⟨x_in_s, ⟨x_in_u, x_in_v⟩⟩

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

Goal state before:
pp: case succ
α : Type u_1
f : α → α
n : ℕ
ih : image f^[n] = (image f)^[n]
⊢ image f^[n + 1] = (image f)^[n + 1]

Tactic:
rw [iterate_succ', iterate_succ', ← ih, image_comp_eq]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
g' : β → γ
⊢ (range f)ᶜ.domRestrict (extend f g g') = g' ∘ Subtype.val

Tactic:
classical
  exact domRestrict_dite_compl _ _

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

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

Tactic:
or_iff_left

Goal state after:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
⊢ s ⊆ s₁ ∧ t ⊆ t₁ ↔ s ⊆ s₁ ∧ t ⊆ t₁

α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
⊢ ¬(s = ∅ ∨ t = ∅)
Module: Mathlib.Data.Set.Piecewise

Goal state before:
pp: α : Type u_1
δ : α → Sort u_7
s : Set α
f : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
⊢ s.piecewise f f = f

Tactic:
ext x
  by_cases hx : x ∈ s <;> simp [hx]

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

Goal state before:
pp: α : Type u_5
β : Type u_6
γ : Type u_7
γ' : Type u_8
δ : Type u_9
δ' : Type u_10
h : β → α
f : γ → β
f₁ : γ' → α
f₂ : γ → γ'
g : δ → β
g₁ : δ' → α
g₂ : δ → δ'
hf : h ∘ f = f₁ ∘ f₂
hg : h ∘ g = g₁ ∘ g₂
hfg : range f ∪ range g = univ
s : Set β
⊢ h '' s = h '' (s ∩ univ)

Tactic:
inter_univ

Goal state after:
α : Type u_5
β : Type u_6
γ : Type u_7
γ' : Type u_8
δ : Type u_9
δ' : Type u_10
h : β → α
f : γ → β
f₁ : γ' → α
f₂ : γ → γ'
g : δ → β
g₁ : δ' → α
g₂ : δ → δ'
hf : h ∘ f = f₁ ∘ f₂
hg : h ∘ g = g₁ ∘ g₂
hfg : range f ∪ range g = univ
s : Set β
⊢ h '' s = h '' s
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: X : Type u_1
Y : Sort u_2
f : X → Y
⊢ pullbackDiagonal f ∩ univ = pullbackDiagonal f

Tactic:
inter_univ

Goal state after:
X : Type u_1
Y : Sort u_2
f : X → Y
⊢ pullbackDiagonal f = pullbackDiagonal f
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
hfs : SurjOn f s t
⊢ ∃ u, u ⊆ s ∧ InjOn f u ∧ f '' u = t

Tactic:
by
  choose x hmem heq using hfs
  exact ⟨range (fun a : t ↦ x a.2), by grind, fun _ ↦ by grind, by aesop⟩

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

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

Tactic:
by
  rw [← mul_assoc, mul_inv, one_mul]

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

Goal state before:
pp: α : Type u
inst✝ : DivisionCommMonoid α
a b : α
h : IsUnit a
⊢ a / (a / b) = b

Tactic:
by
  rw [div_div_eq_mul_div, h.mul_div_cancel_left]

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

Goal state before:
pp: case neg
α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
f : Perm α
h₁ : ∀ (x : α), p (f x) ↔ p x
h₂ : ∀ (x : α), f x ≠ x → p x
x : α
hx : ¬p x
⊢ x = f x

Tactic:
exact not_not.mp fun h => hx (h₂ x (Ne.symm h))

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

Goal state before:
pp: case pos
α : Type u_4
inst✝ : DecidableEq α
f : Perm α
x y z : α
h✝¹ : f z = x
h✝ : z = f⁻¹ x
⊢ y = f (f⁻¹ y)

Tactic:
simp_all [eq_symm_apply]

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

Goal state before:
pp: case pos
α : Type u_4
inst✝ : DecidableEq α
f : Perm α
x y z : α
h✝² : f z = x
h✝¹ : ¬z = f⁻¹ x
h✝ : z = f⁻¹ y
⊢ y = f (f⁻¹ x)

Tactic:
simp_all [eq_symm_apply]

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

Goal state before:
pp: case neg
α : Type u_4
inst✝ : DecidableEq α
f : Perm α
x y z : α
h✝² : f z = x
h✝¹ : ¬z = f⁻¹ x
h✝ : ¬z = f⁻¹ y
⊢ y = f z

Tactic:
simp_all [eq_symm_apply]

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

Goal state before:
pp: case pos
α : Type u_4
inst✝ : DecidableEq α
f : Perm α
x y z : α
h✝² : ¬f z = x
h✝¹ : f z = y
h✝ : z = f⁻¹ x
⊢ x = f (f⁻¹ y)

Tactic:
simp_all [eq_symm_apply]

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

Goal state before:
pp: case pos
α : Type u_4
inst✝ : DecidableEq α
f : Perm α
x y z : α
h✝³ : ¬f z = x
h✝² : f z = y
h✝¹ : ¬z = f⁻¹ x
h✝ : z = f⁻¹ y
⊢ x = f (f⁻¹ x)

Tactic:
simp_all [eq_symm_apply]

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

Goal state before:
pp: case neg
α : Type u_4
inst✝ : DecidableEq α
f : Perm α
x y z : α
h✝³ : ¬f z = x
h✝² : f z = y
h✝¹ : ¬z = f⁻¹ x
h✝ : ¬z = f⁻¹ y
⊢ x = f z

Tactic:
simp_all [eq_symm_apply]

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

Goal state before:
pp: case pos
α : Type u_4
inst✝ : DecidableEq α
f : Perm α
x y z : α
h✝² : ¬f z = x
h✝¹ : ¬f z = y
h✝ : z = f⁻¹ x
⊢ f z = f (f⁻¹ y)

Tactic:
simp_all [eq_symm_apply]

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

Goal state before:
pp: case pos
α : Type u_4
inst✝ : DecidableEq α
f : Perm α
x y z : α
h✝³ : ¬f z = x
h✝² : ¬f z = y
h✝¹ : ¬z = f⁻¹ x
h✝ : z = f⁻¹ y
⊢ f z = f (f⁻¹ x)

Tactic:
simp_all [eq_symm_apply]

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

Goal state before:
pp: case neg
α : Type u_4
inst✝ : DecidableEq α
f : Perm α
x y z : α
h✝³ : ¬f z = x
h✝² : ¬f z = y
h✝¹ : ¬z = f⁻¹ x
h✝ : ¬z = f⁻¹ y
⊢ f z = f z

Tactic:
simp_all [eq_symm_apply]

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

Goal state before:
pp: case succ
R : Type u_1
inst✝ : AddMonoidWithOne R
m n : ℕ
ih : ↑(m + n) = ↑m + ↑n
⊢ ↑m + ↑n + 1 = ↑m + (↑n + 1)

Tactic:
add_assoc

Goal state after:
case succ
R : Type u_1
inst✝ : AddMonoidWithOne R
m n : ℕ
ih : ↑(m + n) = ↑m + ↑n
⊢ ↑m + (↑n + 1) = ↑m + (↑n + 1)
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: M₀ : Type u_1
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a b x✝ x : G₀
hx : x ≠ 0
y z : G₀
h : (fun x_1 ↦ x * x_1) y = (fun x_1 ↦ x * x_1) z
⊢ y = z

Tactic:
dsimp only at h; rw [← inv_mul_cancel_left₀ hx y, h, inv_mul_cancel_left₀ hx z]

Goal state after:
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 A' A
hf : Injective ⇑f
smul : ∀ (a : M₀) (b : A'), f (a • b) = a • f b
a : M₀
⊢ f (a • 0) = f 0

Tactic:
by simp [smul]

Goal state after:
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 A' A
hf : Injective ⇑f
smul : ∀ (a : M₀) (b : A'), f (a • b) = a • f b
a : A'
⊢ f (0 • a) = f 0

Tactic:
by simp [smul]

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

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
n : ℤ
⊢ a ^ (n - 1) * a * a⁻¹ = a ^ n * a⁻¹

Tactic:
by rw [← zpow_add_one₀ ha, Int.sub_add_cancel]

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

Goal state before:
pp: R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
h : m ≤ n
⊢ ↑(n - m) + ↑m = ↑n

Tactic:
by rw [← cast_add, Nat.sub_add_cancel h]

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

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
a b : α
⊢ a ^ 2 + (b ^ 2 + 2 * a * b) = a ^ 2 + b ^ 2 + 2 * a * b

Tactic:
add_assoc

Goal state after:
α : Type u
inst✝ : CommSemiring α
a b : α
⊢ a ^ 2 + (b ^ 2 + 2 * a * b) = a ^ 2 + (b ^ 2 + 2 * a * b)
Module: Mathlib.Data.Nat.Sqrt

Goal state before:
pp: a b c : ℕ
h : a = b * c
⊢ b ≤ a.sqrt ∨ c ≤ a.sqrt

Tactic:
by
  rcases le_total b c with bc | cb
  · exact Or.inl <| le_sqrt.mpr <| h ▸ mul_le_mul_left b bc
  · exact Or.inr <| le_sqrt.mpr <| h ▸ mul_le_mul_right c cb

Goal state after:
Module: Mathlib.Algebra.Group.Int.Even

Goal state before:
pp: m✝ n m : ℤ
⊢ IsSquare m ↔ sqrt m * sqrt m = m

Tactic:
← exists_mul_self m,

Goal state after:
m✝ n m : ℤ
⊢ IsSquare m ↔ ∃ n, n * n = m
Module: Mathlib.Data.Nat.Cast.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
m n : ℕ
⊢ ↑(m ^ (n + 1)) = ↑m ^ (n + 1)

Tactic:
rw [_root_.pow_succ', _root_.pow_succ', cast_mul, cast_pow m n]

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

Goal state before:
pp: M₀ : Type u_2
inst✝ : MonoidWithZero M₀
⊢ 0⁻¹ʳ = 0

Tactic:
nontriviality
  exact inverse_non_unit _ not_isUnit_zero

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

Goal state before:
pp: case ofNat
M : Type u_5
inst✝ : Monoid M
f g : ℤ →* M
h_neg_one : f (-1) = g (-1)
h_nat : f.comp ↑ofNatHom = g.comp ↑ofNatHom
x : ℕ
⊢ f (ofNat x) = g (ofNat x)

pp: case negSucc
M : Type u_5
inst✝ : Monoid M
f g : ℤ →* M
h_neg_one : f (-1) = g (-1)
h_nat : f.comp ↑ofNatHom = g.comp ↑ofNatHom
x : ℕ
⊢ f -[x+1] = g -[x+1]

Tactic:
· exact (DFunLike.congr_fun h_nat x :)

Goal state after:
case negSucc
M : Type u_5
inst✝ : Monoid M
f g : ℤ →* M
h_neg_one : f (-1) = g (-1)
h_nat : f.comp ↑ofNatHom = g.comp ↑ofNatHom
x : ℕ
⊢ f -[x+1] = g -[x+1]
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝ : Semiring α
a : α
⊢ Even a ↔ ∃ b, a = 2 * b

Tactic:
simp [even_iff_exists_two_nsmul]

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

Goal state before:
pp: α : Type u_2
inst✝ : Semiring α
a b : α
⊢ 2 * a + (2 * b + 1) = 2 * a + 2 * b + 1

Tactic:
add_assoc

Goal state after:
α : Type u_2
inst✝ : Semiring α
a b : α
⊢ 2 * a + (2 * b + 1) = 2 * a + (2 * b + 1)
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs

Goal state before:
pp: M : Type u_1
N : Type u_2
μ : M → N → N
inst✝ : PartialOrder N
h : Contravariant M N μ fun x1 x2 ↦ x1 ≤ x2
a : M
b : N
bc : μ a b < μ a b
⊢ False

Tactic:
exact lt_irrefl _ bc

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

Goal state before:
pp: α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hb : AddLECancellable b
h : a = b + c
⊢ a = c + b

Tactic:
rw [add_comm, h]

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c : α
inst✝ : AddLeftMono α
ha : AddLECancellable a
h : a = b + c
⊢ a = c + b

Tactic:
rw [add_comm, h]

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

Goal state before:
pp: case bc
α : Type u_1
inst✝⁵ : PartialOrder α
inst✝⁴ : AddCommSemigroup α
inst✝³ : Sub α
inst✝² : OrderedSub α
inst✝¹ : AddLeftMono α
inst✝ : AddLeftReflectLE α
a c b : α
⊢ a + ?a ≤ a + c - (b + c) + b + ?a

pp: case a
α : Type u_1
inst✝⁵ : PartialOrder α
inst✝⁴ : AddCommSemigroup α
inst✝³ : Sub α
inst✝² : OrderedSub α
inst✝¹ : AddLeftMono α
inst✝ : AddLeftReflectLE α
a c b : α
⊢ α

Tactic:
add_assoc

Goal state after:
case bc
α : Type u_1
inst✝⁵ : PartialOrder α
inst✝⁴ : AddCommSemigroup α
inst✝³ : Sub α
inst✝² : OrderedSub α
inst✝¹ : AddLeftMono α
inst✝ : AddLeftReflectLE α
a c b : α
⊢ a + ?bc.c ≤ a + c - (b + c) + (b + ?bc.c)

case bc.c
α : Type u_1
inst✝⁵ : PartialOrder α
inst✝⁴ : AddCommSemigroup α
inst✝³ : Sub α
inst✝² : OrderedSub α
inst✝¹ : AddLeftMono α
inst✝ : AddLeftReflectLE α
a c b : α
⊢ α
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

Goal state before:
pp: α : Type u
inst✝³ : Group α
inst✝² : LT α
inst✝¹ : MulLeftStrictMono α
a b : α
inst✝ : MulRightStrictMono α
⊢ a⁻¹ < b ↔ b⁻¹ < a

Tactic:
← inv_lt_inv_iff,

Goal state after:
α : Type u
inst✝³ : Group α
inst✝² : LT α
inst✝¹ : MulLeftStrictMono α
a b : α
inst✝ : MulRightStrictMono α
⊢ b⁻¹ < a⁻¹⁻¹ ↔ b⁻¹ < a
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

Goal state before:
pp: α : Type u
inst✝³ : Group α
inst✝² : LT α
inst✝¹ : MulLeftStrictMono α
a b : α
inst✝ : MulRightStrictMono α
⊢ a < b⁻¹ ↔ b < a⁻¹

Tactic:
← inv_lt_inv_iff,

Goal state after:
α : Type u
inst✝³ : Group α
inst✝² : LT α
inst✝¹ : MulLeftStrictMono α
a b : α
inst✝ : MulRightStrictMono α
⊢ b⁻¹⁻¹ < a⁻¹ ↔ b < a⁻¹
Module: Mathlib.Algebra.Order.Monoid.NatCast

Goal state before:
pp: α : Type u_1
inst✝³ : AddMonoidWithOne α
inst✝² : Preorder α
inst✝¹ : ZeroLEOneClass α
inst✝ : AddLeftMono α
⊢ 0 ≤ 4

Tactic:
rw [← three_add_one_eq_four]

Goal state after:
α : Type u_1
inst✝³ : AddMonoidWithOne α
inst✝² : Preorder α
inst✝¹ : ZeroLEOneClass α
inst✝ : AddLeftMono α
⊢ 0 ≤ 3 + 1
Module: Mathlib.Algebra.Order.Monoid.NatCast

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : ZeroLEOneClass α
inst✝¹ : NeZero 1
inst✝ : AddLeftMono α
⊢ 0 < 4

Tactic:
rw [← three_add_one_eq_four]

Goal state after:
α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : ZeroLEOneClass α
inst✝¹ : NeZero 1
inst✝ : AddLeftMono α
⊢ 0 < 3 + 1
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic

Goal state before:
pp: α : Type u_1
inst✝² : Mul α
inst✝¹ : IsMulCommutative α
inst✝ : PartialOrder α
a : α
ha : MulLECancellable a
b c : α
h : (fun x ↦ x * a) b = (fun x ↦ x * a) c
⊢ (fun x ↦ a * x) b = (fun x ↦ a * x) c

Tactic:
dsimp; rwa [mul_comm' a, mul_comm' a]

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

Goal state before:
pp: α : Type u_1
inst✝³ : MulZeroClass α
a b : α
inst✝² : Preorder α
inst✝¹ : PosMulStrictMono α
inst✝ : PosMulReflectLT α
h : 0 < a
⊢ 0 < a * b ↔ 0 < b

Tactic:
by simpa using mul_lt_mul_iff_right₀ (b := 0) h

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MulZeroClass α
inst✝ : PartialOrder α
h : CovariantClass α>0 α (fun x y ↦ y * ↑x) fun x1 x2 ↦ x1 ≤ x2
a : α
ha : 0 ≤ a
b c : α
hbc : b ≤ c
⊢ b * a ≤ c * a

Tactic:
obtain ha | ha := ha.eq_or_lt
        · simp [← ha]
        · exact @CovariantClass.elim α>0 α (fun x y => y * x) (· ≤ ·) _ ⟨_, ha⟩ _ _ hbc

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

Goal state before:
pp: R : Type u
inst✝⁴ : Semiring R
inst✝³ : Preorder R
a b : R
inst✝² : ZeroLEOneClass R
inst✝¹ : MulPosMono R
inst✝ : AddLeftMono R
a2 : 2 ≤ a
b0 : 0 ≤ b
⊢ a + (a + a * b) ≤ a + a + a * b

Tactic:
add_assoc

Goal state after:
R : Type u
inst✝⁴ : Semiring R
inst✝³ : Preorder R
a b : R
inst✝² : ZeroLEOneClass R
inst✝¹ : MulPosMono R
inst✝ : AddLeftMono R
a2 : 2 ≤ a
b0 : 0 ≤ b
⊢ a + (a + a * b) ≤ a + (a + a * b)
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: M₀ : Type u_2
inst✝² : MonoidWithZero M₀
inst✝¹ : PartialOrder M₀
a : M₀
inst✝ : PosMulStrictMono M₀
h₀ : 0 < a
h₁ : a < 1
n : ℕ
this : ZeroLEOneClass M₀
⊢ a ^ (n + 1) < a ^ n

Tactic:
simpa only [pow_succ, mul_one] using mul_lt_mul_of_pos_left h₁ (pow_pos h₀ n)

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₀
inst✝ : MulPosMono G₀
⊢ Contravariant { x // 0 < x } G₀ (fun x y ↦ y * ↑x) fun x1 x2 ↦ x1 ≤ x2

Tactic:
rintro ⟨a, ha⟩ b c h
    simpa [ha.ne'] using mul_le_mul_of_nonneg_right h (inv_nonneg.2 ha.le)

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

Goal state before:
pp: R : Type u
inst✝⁴ : Semiring R
inst✝³ : LinearOrder R
inst✝² : ExistsAddOfLE R
inst✝¹ : PosMulMono R
inst✝ : AddLeftMono R
a : R
ha : a < 0
b : R
hab : 0 = a + b
hb : 0 < b
⊢ a * a + a * b + b * b = a * a + (a * b + b * b)

Tactic:
add_assoc

Goal state after:
R : Type u
inst✝⁴ : Semiring R
inst✝³ : LinearOrder R
inst✝² : ExistsAddOfLE R
inst✝¹ : PosMulMono R
inst✝ : AddLeftMono R
a : R
ha : a < 0
b : R
hab : 0 = a + b
hb : 0 < b
⊢ a * a + (a * b + b * b) = a * a + (a * b + b * b)
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosReflectLT G₀
a b : G₀
ha : 0 < a
hb : 0 < b
⊢ a⁻¹ < b⁻¹ ↔ b < a

Tactic:
by
  rw [inv_lt_iff_one_lt_mul₀' ha, lt_mul_inv_iff₀ hb, one_mul]

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✝³ : PosMulStrictMono R
inst✝² : MulPosStrictMono R
inst✝¹ : AddLeftReflectLT R
inst✝ : AddLeftStrictMono R
⊢ a * b < 0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b

Tactic:
rw [← neg_pos, neg_mul_eq_mul_neg, mul_pos_iff (R := R), neg_pos, neg_lt_zero]

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

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : Group α
a b : α
inst✝ : MulLeftMono α
ha : 1 ≤ a
hab : a ≤ b
⊢ a ≤ |b|ₘ

Tactic:
mabs_of_one_le (ha.trans hab)

Goal state after:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : Group α
a b : α
inst✝ : MulLeftMono α
ha : 1 ≤ a
hab : a ≤ b
⊢ a ≤ b