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

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
ex : ∀ (x y : M), x * y = 1 → ∃ z, y * z = 1
x y : M
h : x * y = 1
⊢ y * x = 1

Tactic:
have ⟨z, hz⟩ := ex x y h
    rwa [show x = z by simpa [← mul_assoc, h] using congr_arg (x * ·) hz.symm]

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

Goal state before:
pp: G : Type u_2
inst✝ : SubNegMonoid G
a : G
n : ℕ
⊢ Int.negSucc n • a = -((n + 1) • a)

Tactic:
← natCast_zsmul

Goal state after:
G : Type u_2
inst✝ : SubNegMonoid G
a : G
n : ℕ
⊢ Int.negSucc n • a = -(↑(n + 1) • a)
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
a b : α
inst✝ : Decidable Q
⊢ (if P ∧ Q then a else b) = if P then if Q then a else b else b

Tactic:
by_cases hp : P <;> by_cases hq : Q

Goal state after:
case pos
α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
a b : α
inst✝ : Decidable Q
hp : P
hq : Q
⊢ (if P ∧ Q then a else b) = if P then if Q then a else b else b

case neg
α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
a b : α
inst✝ : Decidable Q
hp : P
hq : ¬Q
⊢ (if P ∧ Q then a else b) = if P then if Q then a else b else b

case pos
α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
a b : α
inst✝ : Decidable Q
hp : ¬P
hq : Q
⊢ (if P ∧ Q then a else b) = if P then if Q then a else b else b

case neg
α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
a b : α
inst✝ : Decidable Q
hp : ¬P
hq : ¬Q
⊢ (if P ∧ Q then a else b) = if P then if Q then a else b else b
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
a b : α
inst✝ : Decidable Q
⊢ (if P ∨ Q then a else b) = if P then a else if Q then a else b

Tactic:
by_cases hp : P <;> by_cases hq : Q

Goal state after:
case pos
α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
a b : α
inst✝ : Decidable Q
hp : P
hq : Q
⊢ (if P ∨ Q then a else b) = if P then a else if Q then a else b

case neg
α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
a b : α
inst✝ : Decidable Q
hp : P
hq : ¬Q
⊢ (if P ∨ Q then a else b) = if P then a else if Q then a else b

case pos
α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
a b : α
inst✝ : Decidable Q
hp : ¬P
hq : Q
⊢ (if P ∨ Q then a else b) = if P then a else if Q then a else b

case neg
α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
a b : α
inst✝ : Decidable Q
hp : ¬P
hq : ¬Q
⊢ (if P ∨ Q then a else b) = if P then a else if Q then a else b
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Type u_1
inst1 inst2 : BEq α
inst✝¹ : LawfulBEq α
inst✝ : LawfulBEq α
⊢ inst1 = inst2

Tactic:
by
  ext
  simp

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

Goal state before:
pp: α : Sort u_1
β : Sort u_2
f : α → β
γ : Type u_4
inst✝ : Nontrivial γ
⊢ (Surjective fun g ↦ g ∘ f) ↔ Injective f

Tactic:
classical
  refine ⟨not_imp_not.mp fun not_inj surj ↦ not_subsingleton γ ⟨fun c c' ↦ ?_⟩,
    (·.surjective_comp_right)⟩
  simp only [Injective, not_forall] at not_inj
  have ⟨a₁, a₂, eq, ne⟩ := not_inj
  have ⟨f, hf⟩ := surj (if · = a₂ then c else c')
  have h₁ := congr_fun hf a₁
  have h₂ := congr_fun hf a₂
  simp only [comp_apply, if_neg ne, reduceIte] at h₁ h₂
  rw [← h₁, eq, h₂]

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

Goal state before:
pp: α : Sort u_1
β : Sort u_2
r : α → β → Prop
⊢ (∀ (a : α), ∃! b, r a b) ↔ ∃ f, ∀ {a : α} {b : β}, r a b ↔ f a = b

Tactic:
by
  refine ⟨fun h ↦ ?_, ?_⟩
  · refine ⟨fun a ↦ (h a).choose, fun hr ↦ ?_, fun h' ↦ h' ▸ ?_⟩
    exacts [((h _).choose_spec.2 _ hr).symm, (h _).choose_spec.1]
  · rintro ⟨f, hf⟩
    simp [hf]

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a b c : α
h : ∀ (a b c : α), r a b → r a c → ∃ d, ReflGen r b d ∧ ReflTransGen r c d
hab : ReflTransGen r a b
hac : ReflTransGen r a c
⊢ Join (ReflTransGen r) b c

Tactic:
induction hab with
  | refl => exact ⟨c, hac, refl⟩
  | @tail d e _ hde ih =>
    rcases ih with ⟨b, hdb, hcb⟩
    have : ∃ a, ReflTransGen r e a ∧ ReflGen r b a := by
      clear hcb
      induction hdb with
      | refl => exact ⟨e, refl, ReflGen.single hde⟩
      | @tail f b _ hfb ih =>
        rcases ih with ⟨a, hea, hfa⟩
        cases hfa with
        | refl => exact ⟨b, hea.tail hfb, ReflGen.refl⟩
        | single hfa =>
          rcases h _ _ _ hfb hfa with ⟨c, hbc, hac⟩
          exact ⟨c, hea.trans hac, hbc⟩
    rcases this with ⟨a, hea, hba⟩
    cases hba with
    | refl => exact ⟨b, hea, hcb⟩
    | single hba => exact ⟨a, hea, hcb.tail hba⟩

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

Goal state before:
pp: ι : Type u_1
inst✝¹ : DecidableEq ι
M : Type u_9
inst✝ : One M
i : ι
x : M
j : ι
⊢ mulSingle i x j = mulSingle j x i

Tactic:
by simp [mulSingle_apply, eq_comm]

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

Goal state before:
pp: M : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
inst✝⁴ : SMul M α
inst✝³ : SMul Mᵐᵒᵖ α
inst✝² : IsCentralScalar M α
inst✝¹ : SMul N α
inst✝ : SMulCommClass M N α
m : Mᵐᵒᵖ
n : N
a : α
⊢ m • n • a = n • m • a

Tactic:
← unop_smul_eq_smul m (n • a),

Goal state after:
M : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
inst✝⁴ : SMul M α
inst✝³ : SMul Mᵐᵒᵖ α
inst✝² : IsCentralScalar M α
inst✝¹ : SMul N α
inst✝ : SMulCommClass M N α
m : Mᵐᵒᵖ
n : N
a : α
⊢ MulOpposite.unop m • n • a = n • m • a
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: M : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
inst✝⁴ : SMul M α
inst✝³ : SMul Mᵐᵒᵖ α
inst✝² : IsCentralScalar M α
inst✝¹ : SMul N α
inst✝ : SMulCommClass M N α
m : Mᵐᵒᵖ
n : N
a : α
⊢ MulOpposite.unop m • n • a = n • m • a

Tactic:
← unop_smul_eq_smul m a,

Goal state after:
M : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
inst✝⁴ : SMul M α
inst✝³ : SMul Mᵐᵒᵖ α
inst✝² : IsCentralScalar M α
inst✝¹ : SMul N α
inst✝ : SMulCommClass M N α
m : Mᵐᵒᵖ
n : N
a : α
⊢ MulOpposite.unop m • n • a = n • MulOpposite.unop m • a
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: M : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
inst✝⁷ : SMul M α
inst✝⁶ : SMul Mᵐᵒᵖ α
inst✝⁵ : IsCentralScalar M α
inst✝⁴ : SMul M N
inst✝³ : SMul Mᵐᵒᵖ N
inst✝² : IsCentralScalar M N
inst✝¹ : SMul N α
inst✝ : IsScalarTower M N α
m : Mᵐᵒᵖ
n : N
a : α
⊢ (m • n) • a = m • n • a

Tactic:
← unop_smul_eq_smul m (n • a),

Goal state after:
M : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
inst✝⁷ : SMul M α
inst✝⁶ : SMul Mᵐᵒᵖ α
inst✝⁵ : IsCentralScalar M α
inst✝⁴ : SMul M N
inst✝³ : SMul Mᵐᵒᵖ N
inst✝² : IsCentralScalar M N
inst✝¹ : SMul N α
inst✝ : IsScalarTower M N α
m : Mᵐᵒᵖ
n : N
a : α
⊢ (m • n) • a = MulOpposite.unop m • n • a
Module: Mathlib.Data.Sum.Basic

Goal state before:
pp: α : Type u
β : Type v
x : α ⊕ β
a : α
⊢ x = inl a ↔ ∃ h, x.getLeft h = a

Tactic:
by
  cases x <;> simp

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

Goal state before:
pp: α : Type u
β : Type v
x : α ⊕ β
b : β
⊢ x = inr b ↔ ∃ h, x.getRight h = b

Tactic:
by
  cases x <;> simp

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: case neg
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
x y : α × β
h : x < y
h₁ : ¬y.fst ≤ x.fst
⊢ x.fst < y.fst ∧ x.snd ≤ y.snd ∨ x.fst ≤ y.fst ∧ x.snd < y.snd

Tactic:
exact Or.inl ⟨LE.le.lt_of_not_ge h.1.1 h₁, h.1.2⟩

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝¹ : (i : ι) → Preorder (π i)
inst✝ : ∀ (i : ι), DenselyOrdered (π i)
a b : (i : ι) → π i
⊢ a < b → ∃ a_2, a < a_2 ∧ a_2 < b

Tactic:
Pi.lt_def

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝¹ : (i : ι) → Preorder (π i)
inst✝ : ∀ (i : ι), DenselyOrdered (π i)
a b : (i : ι) → π i
⊢ (a ≤ b ∧ ∃ i, a i < b i) → ∃ a_2, (a ≤ a_2 ∧ ∃ i, a i < a_2 i) ∧ a_2 ≤ b ∧ ∃ i, a_2 i < b i
Module: Mathlib.Data.Nat.Basic

Goal state before:
pp: x a : ℕ
hx : x ≠ 0
ha : a ≠ 0
⊢ x ^ a / x ^ 1 = x ^ a / x

Tactic:
Nat.pow_one

Goal state after:
x a : ℕ
hx : x ≠ 0
ha : a ≠ 0
⊢ x ^ a / x = x ^ a / x
Module: Mathlib.Data.Nat.Basic

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

Tactic:
| succ b =>

Goal state after:
Module: Mathlib.Order.PropInstances

Goal state before:
pp: ι : Type u_1
α' : ι → Type u_3
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → BoundedOrder (α' i)
f g : (i : ι) → α' i
⊢ IsCompl f g ↔ ∀ (i : ι), IsCompl (f i) (g i)

Tactic:
_root_.isCompl_iff,

Goal state after:
ι : Type u_1
α' : ι → Type u_3
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → BoundedOrder (α' i)
f g : (i : ι) → α' i
⊢ Disjoint f g ∧ Codisjoint f g ↔ ∀ (i : ι), Disjoint (f i) (g i) ∧ Codisjoint (f i) (g i)
Module: Mathlib.Order.PropInstances

Goal state before:
pp: P Q : Prop
⊢ IsCompl P Q ↔ ¬(P ↔ Q)

Tactic:
_root_.isCompl_iff,

Goal state after:
P Q : Prop
⊢ Disjoint P Q ∧ Codisjoint P Q ↔ ¬(P ↔ Q)
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
x y x' y' : α
h : IsCompl x y
h' : IsCompl x' y'
⊢ (x ⊔ x' ⊔ y) ⊓ (x ⊔ x' ⊔ y') = ⊤

Tactic:
sup_comm x,

Goal state after:
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
x y x' y' : α
h : IsCompl x y
h' : IsCompl x' y'
⊢ (x' ⊔ x ⊔ y) ⊓ (x' ⊔ x ⊔ y') = ⊤
Module: Mathlib.Order.BooleanAlgebra.Set

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

Tactic:
simp [inter_union_distrib_right]

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

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

Tactic:
simp [inter_union_distrib_right]

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

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

Tactic:
exact symm_apply_apply (e : Option α ≃ β) a

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

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hd : Disjoint x z
hz : z ≤ y
hs : (x ⊔ z) ⊓ y = y
⊢ y ⊓ (x ⊔ z) ⊔ z ⊓ (x ⊔ z) = y

Tactic:
sup_comm x,

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hd : Disjoint x z
hz : z ≤ y
hs : (x ⊔ z) ⊓ y = y
⊢ y ⊓ (z ⊔ x) ⊔ z ⊓ (z ⊔ x) = y
Module: Mathlib.Order.BooleanAlgebra.Basic

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

Tactic:
rw [sup_sdiff_cancel_right hx]
        grw [sdiff_le]
        rw [sup_eq_right.2 hz]

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

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
h : y < z \ x
hxz : x ≤ z
h' : x ⊔ z \ x ≤ x ⊔ y
⊢ z \ x ≤ y

Tactic:
← sdiff_idem

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
h : y < z \ x
hxz : x ≤ z
h' : x ⊔ z \ x ≤ x ⊔ y
⊢ (z \ x) \ x ≤ y
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
h : x < z \ y
hyz : y ≤ z
h' : z \ y ⊔ y ≤ x ⊔ y
⊢ z \ y ≤ x

Tactic:
← sdiff_idem

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
h : x < z \ y
hyz : y ≤ z
h' : z \ y ⊔ y ≤ x ⊔ y
⊢ (z \ y) \ y ≤ x
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_9
inst✝ : DecidableEq α
i : α
β : α → Type u_10
f : β i × ((j : { j // j ≠ i }) → β ↑j)
⊢ (fun f ↦ (f i, fun j ↦ f ↑j)) ((fun f j ↦ if h : j = i then ⋯ ▸ f.fst else f.snd ⟨j, h⟩) f) = f

Tactic:
ext x <;> grind

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

Goal state before:
pp: α : Type u_1
s : Set α
⊢ (fun x ↦ x) '' s = s

Tactic:
by
  ext
  simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s t : Set α
f : α → β
hf : Injective f
eq : f '' s = f '' t
⊢ s = t

Tactic:
by
      rw [← preimage_image_eq s hf, ← preimage_image_eq t hf, eq]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
t : Set β
f : α → β
u : Set ↑t
⊢ Subtype.val '' t.restrictPreimage f ⁻¹' u = f ⁻¹' Subtype.val '' u

Tactic:
by
  ext
  simp

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

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

Tactic:
by
  ext
  simp

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

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

Tactic:
by
  ext
  simp

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
inst✝ : Decidable (s.pi t).Nonempty
hi : ¬i ∈ s
⊢ eval i '' s.pi t = if (s.pi t).Nonempty then univ else ∅

Tactic:
ext xᵢ
  simp only [eval, mem_image, mem_pi, Set.Nonempty, mem_ite_empty_right, mem_univ, and_true]
  constructor
  · rintro ⟨x, hx, rfl⟩
    exact ⟨x, hx⟩
  · rintro ⟨x, hx⟩
    refine ⟨Function.update x i xᵢ, ?_⟩
    simpa +contextual [(ne_of_mem_of_not_mem · hi)]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
i : ι
inst✝ : DecidableEq ι
s : Set (α i)
⊢ eval i ⁻¹' s = {i}.pi (update (fun x ↦ univ) i s)

Tactic:
by
  ext
  simp

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
π : ι ⊕ ι' → Type u_4
t : (i : ι ⊕ ι') → Set (π i)
⊢ ⇑(sumPiEquivProdPi π).symm ⁻¹' univ.pi t = (univ.pi fun i ↦ t (Sum.inl i)) ×ˢ univ.pi fun i ↦ t (Sum.inr i)

Tactic:
by
  ext
  simp

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

Goal state before:
pp: M : Type u_2
N : Type u_3
P : Type u_4
inst✝² : Mul M
inst✝¹ : CommSemigroup N
inst✝ : CommSemigroup P
g : N →ₙ* P
f₁ f₂ : M →ₙ* N
⊢ g.comp (f₁ * f₂) = g.comp f₁ * g.comp f₂

Tactic:
by
  ext
  simp

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

Goal state before:
pp: M : Type u_2
N : Type u_3
P : Type u_4
inst✝² : MulOneClass M
inst✝¹ : CommMonoid N
inst✝ : CommMonoid P
g : N →* P
f₁ f₂ : M →* N
⊢ g.comp (f₁ * f₂) = g.comp f₁ * g.comp f₂

Tactic:
by
  ext
  simp

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

Goal state before:
pp: M : Type u_2
G : Type u_5
H : Type u_6
inst✝² : MulOneClass M
inst✝¹ : CommGroup G
inst✝ : CommGroup H
φ : G →* H
ψ : M →* G
⊢ φ.comp ψ⁻¹ = (φ.comp ψ)⁻¹

Tactic:
by
  ext
  simp

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

Goal state before:
pp: M : Type u_2
G : Type u_5
H : Type u_6
inst✝² : MulOneClass M
inst✝¹ : CommGroup G
inst✝ : CommGroup H
f : G →* H
g h : M →* G
⊢ f.comp (g / h) = f.comp g / f.comp h

Tactic:
by
  ext
  simp

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

Goal state before:
pp: β₁ : Type u_8
β₂ : Type u_9
t₁ : Set β₁
t₂ : Set β₂
⊢ t₁.Nonempty ∨ t₂ = ∅ → SurjOn Prod.snd (t₁ ×ˢ t₂) t₂

Tactic:
simp +contextual [or_imp, prod_surjOn_snd]

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

Goal state before:
pp: α : Type u_1
inst✝ : MulOne α
⊢ (∀ (a a_1 : α), opEquiv a * opEquiv a_1 = 1 → opEquiv a_1 * opEquiv a = 1) ↔ ∀ {a b : α}, a * b = 1 → b * a = 1

Tactic:
simpa [← op_one, ← op_mul] using forall_comm

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

Goal state before:
pp: M₁ : Type u_1
M₂ : Type u_2
inst✝¹ : Mul M₂
inst✝ : Semigroup M₁
f : M₁ → M₂
hf : Surjective f
mul : ∀ (x y : M₁), f (x * y) = f x * f y
x y z : M₁
⊢ f x * f y * f z = f x * (f y * f z)

Tactic:
simp only [← mul, mul_assoc]

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

Goal state before:
pp: α : Type u
inst✝¹ : RightCancelMonoid α
inst✝ : Subsingleton αˣ
a b : α
h : a * b = 1
⊢ b * a = 1

Tactic:
by
    rw [← mul_right_cancel_iff (a := b), mul_assoc, h, one_mul, mul_one]

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

Goal state before:
pp: α : Type u
inst✝¹ : RightCancelMonoid α
inst✝ : Subsingleton αˣ
a b : α
h : a * b = 1
⊢ b = 1

Tactic:
by
  rwa [RightCancelMonoid.eq_one_of_mul_right h, one_mul] at h

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

Goal state before:
pp: α : Type u
inst✝ : DivisionCommMonoid α
a b c d : α
hb : IsUnit b
hd : IsUnit d
⊢ a * b⁻¹ = c * d⁻¹ ↔ a * d = c * b

Tactic:
by
  rw [← div_eq_mul_inv, ← div_eq_mul_inv, hb.div_eq_div_iff hd]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : AddMonoidWithOne R
k : ℕ
hk : ∀ (m : ℕ), m < k + 1 → m.binCast = ↑m
h : ¬(k + 1) % 2 = 0
⊢ (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) % 2 + 2 * ((k + 1) / 2))

Tactic:
rw [if_neg h, hk _ <| Nat.div_lt_self (Nat.succ_pos k) (Nat.le_refl 2), ← Nat.cast_add]

Goal state after:
case neg
R : Type u_1
inst✝ : AddMonoidWithOne R
k : ℕ
hk : ∀ (m : ℕ), m < k + 1 → m.binCast = ↑m
h : ¬(k + 1) % 2 = 0
⊢ ↑((k + 1) / 2 + (k + 1) / 2) + 1 = ↑((k + 1) % 2 + 2 * ((k + 1) / 2))
Module: Mathlib.Data.Int.Basic

Goal state before:
pp: case inl
n : ℤ
m : ℕ
hn : n = ↑n.natAbs
⊢ ↑m ∣ ↑n.natAbs ↔ m ∣ (↑n.natAbs).natAbs

Tactic:
simp [← natCast_dvd_natCast, Int.dvd_neg]

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

Goal state before:
pp: case inr
n : ℤ
m : ℕ
hn : n = -↑n.natAbs
⊢ ↑m ∣ -↑n.natAbs ↔ m ∣ (-↑n.natAbs).natAbs

Tactic:
simp [← natCast_dvd_natCast, Int.dvd_neg]

Goal state after:
Module: Mathlib.Data.List.TFAE

Goal state before:
pp: case cons
c : Prop
l : List Prop
IH : ∀ {a b : Prop}, IsChain (fun x1 x2 ↦ x1 → x2) (a :: b :: l) → (l.getLastD b → a) → (a :: b :: l).TFAE
a b : Prop
h_chain : IsChain (fun x1 x2 ↦ x1 → x2) (a :: b :: c :: l)
h_last : (c :: l).getLastD b → a
⊢ (a :: b :: c :: l).TFAE

Tactic:
simp only [tfae_cons_cons, getLastD_cons, isChain_cons_cons] at *
    rcases h_chain with ⟨ab, ⟨bc, ch⟩⟩
    have := IH ⟨bc, ch⟩ (ab ∘ h_last)
    exact ⟨⟨ab, h_last ∘ (this.2 c (.head _) _ getLastD_mem_cons).1 ∘ bc⟩, this⟩

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

Goal state before:
pp: α : Type u_3
inst✝ : NonUnitalCommRing α
b c x : α
h : x * x - b * x + c = 0
⊢ ∃ y, y * y - b * y + c = 0 ∧ x + y = b ∧ x * y = c

Tactic:
by
  have : c = x * (b - x) := (eq_neg_of_add_eq_zero_right h).trans (by simp [mul_sub, mul_comm])
  refine ⟨b - x, ?_, by simp, by rw [this]⟩
  rw [this, sub_add, ← sub_mul, sub_self]

Goal state after:
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 : β →ₙ+* γ
⊢ g.comp 0 = 0

Tactic:
by
  ext
  simp

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

Goal state before:
pp: case inr
G₀ : Type u_3
inst✝ : GroupWithZero G₀
m n : ℕ
a : G₀
h : n < m
ha : a ≠ 0
⊢ a ^ (m - n) = a ^ m * (a ^ n)⁻¹

Tactic:
exact pow_sub₀ _ ha <| Nat.le_of_lt h

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

Goal state before:
pp: G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
a b c d : G₀
hb : b ≠ 0
hc : c ≠ 0
⊢ a / b = c / d ↔ a / c = b / d

Tactic:
conv_lhs => rw [← mul_left_inj' hb, div_mul_cancel₀ _ hb]
  conv_rhs => rw [← mul_left_inj' hc, div_mul_cancel₀ _ hc]
  rw [mul_comm _ c, div_mul_eq_mul_div, mul_div_assoc]

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

Goal state before:
pp: α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
inst✝¹ : MonoidWithZero M₀
M : Type u_4
inst✝ : Nontrivial M
hM : MonoidWithZero M
h : ∀ (a : M), IsUnit a ∨ a = 0
a : M
h0 : a ≠ 0
⊢ (a * if h0 : a = 0 then 0 else ↑⋯.unit⁻¹) = 1

Tactic:
by
      change (a * if h0 : a = 0 then 0 else ↑((h a).resolve_right h0).unit⁻¹) = 1
      rw [dif_neg h0, Units.mul_inv_eq_iff_eq_mul, one_mul, IsUnit.unit_spec]

Goal state after:
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₀
inst✝ : ZeroLEOneClass M₀
ha : 0 < a
⊢ 0 < a ^ 0

Tactic:
nontriviality; rw [pow_zero]; exact zero_lt_one

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

Goal state before:
pp: α₁ : Sort u_1
β₁ : Sort u_2
γ₁ : Sort u_3
α₂ : Sort u_4
β₂ : Sort u_5
γ₂ : Sort u_6
ea : α₁ ≃ α₂
eb : β₁ ≃ β₂
ec : γ₁ ≃ γ₂
f : α₁ ↪ β₁
g : β₁ ↪ γ₁
⊢ (ea.embeddingCongr ec) (f.trans g) = ((ea.embeddingCongr eb) f).trans ((eb.embeddingCongr ec) g)

Tactic:
by
  ext
  simp

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✝⁴ : ExistsAddOfLE R
inst✝³ : PosMulStrictMono R
inst✝² : MulPosStrictMono R
inst✝¹ : AddLeftMono R
inst✝ : AddLeftReflectLE R
⊢ 0 ≤ a * b ↔ (0 < a → 0 ≤ b) ∧ (0 < b → 0 ≤ a)

Tactic:
refine mul_nonneg_iff.trans ?_

Goal state after:
R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
a b : R
inst✝⁴ : ExistsAddOfLE R
inst✝³ : PosMulStrictMono R
inst✝² : MulPosStrictMono R
inst✝¹ : AddLeftMono R
inst✝ : AddLeftReflectLE R
⊢ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 ↔ (0 < a → 0 ≤ b) ∧ (0 < b → 0 ≤ a)
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: case inr
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
⊢ 0 ≤ a ^ 2

Tactic:
calc
    0 ≤ b ^ 2 := pow_succ_nonneg hb.le _
    _ = b ^ 2 + a * (a + b) := by rw [← hab, mul_zero, add_zero]
    _ = a ^ 2 + (a + b) * b := by rw [add_mul, mul_add, sq, sq, add_comm, add_assoc]
    _ = a ^ 2 := by rw [← hab, zero_mul, add_zero]

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

Tactic:
by
  rw [div_lt_iff₀ hb, div_lt_iff₀' hc]

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

Goal state before:
pp: α : Type u_6
β : Type u_7
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
e : α ≃o β
⊢ ofRelIsoLT e.toRelIsoLT = e

Tactic:
by
  ext
  simp

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

Goal state before:
pp: α : Type u_6
β : Type u_7
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
e : (fun x1 x2 ↦ x1 < x2) ≃r fun x1 x2 ↦ x1 < x2
⊢ (ofRelIsoLT e).toRelIsoLT = e

Tactic:
by
  ext
  simp

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

Goal state before:
pp: n : ℤ
⊢ ∃ k, Xor (n = 2 * k) (n = 2 * k + 1)

Tactic:
by
  rcases even_or_odd n with (⟨k, rfl⟩ | ⟨k, rfl⟩) <;>
  · use k
    grind

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

Goal state before:
pp: α : Type u
inst✝² : Semigroup α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedMul α
a b c : α
hbc : (fun x1 x2 ↦ x1 ≤ x2) b c
⊢ (fun x1 x2 ↦ x1 ≤ x2) ((fun x1 x2 ↦ x1 * x2) a b) ((fun x1 x2 ↦ x1 * x2) a c)

Tactic:
obtain ⟨c, hc, rfl⟩ := exists_mul_of_le hbc

Goal state after:
α : Type u
inst✝² : Semigroup α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedMul α
a b c : α
hbc : b ≤ b * c
⊢ (fun x1 x2 ↦ x1 * x2) a b ≤ (fun x1 x2 ↦ x1 * x2) a (b * c)
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: case inr
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a : α
ha : a ≠ ⊤
⊢ 0 ≤ a - a

Tactic:
· rw [sub_self_eq_zero_of_ne_top ha]

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

Goal state before:
pp: α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hac : AddLECancellable (a - c)
h : c ≤ a
⊢ a + b = b + c + (a - c)

Tactic:
by rw [add_assoc, add_tsub_cancel_of_le h, add_comm]

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

Goal state before:
pp: R : Type u_1
inst✝³ : AddCommGroupWithOne R
inst✝² : PartialOrder R
inst✝¹ : AddLeftMono R
inst✝ : ZeroLEOneClass R
m n : ℤ
h : m ≤ n
⊢ ↑m ≤ ↑n

Tactic:
← sub_nonneg

Goal state after:
R : Type u_1
inst✝³ : AddCommGroupWithOne R
inst✝² : PartialOrder R
inst✝¹ : AddLeftMono R
inst✝ : ZeroLEOneClass R
m n : ℤ
h : 0 ≤ n - m
⊢ ↑m ≤ ↑n