mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.BinaryRec

Goal state before:
pp: b : Bool
x n : Nat
⊢ bit b x < 2 ^ (n + 1) ↔ x < 2 ^ n

Tactic:
cases b <;> simp

Goal state after:
case false
x n : Nat
⊢ 2 * x < 2 ^ (n + 1) ↔ x < 2 ^ n

case true
x n : Nat
⊢ 2 * x + 1 < 2 ^ (n + 1) ↔ x < 2 ^ n
Module: Mathlib.Order.Defs.Unbundled

Goal state before:
pp: α : Sort u_1
r : α → α → Prop
a✝ b✝ c : α
inst✝¹ : DecidableRel r
inst✝ : Antisymm r
a b : α
h₁ : Decidable.decide (r a b) = true
h₂ : Decidable.decide (r b a) = true
⊢ r b a

Tactic:
simpa using h₂

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

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

Tactic:
rw [pow_succ, ← mul_assoc, ← pow_add, ← pow_succ, Nat.add_assoc]

Goal state after:
Module: Mathlib.Logic.ExistsUnique

Goal state before:
pp: α : Sort u_1
p : α → Sort u_2
inst✝ : ∀ (x : α), Subsingleton (p x)
q : (x : α) → p x → Prop
y₁ y₂ : α
hpy₁ : p y₁
hqy₁ : q y₁ hpy₁
hpy₂ : p y₂
hqy₂ : q y₂ hpy₂
h : ∃! x, ∃ hx, q x hx
⊢ y₁ = y₂

Tactic:
exact h.unique ⟨hpy₁, hqy₁⟩ ⟨hpy₂, hqy₂⟩

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

Goal state before:
pp: α : Type u
f : α → Type (max u v)
⊢ ¬Surjective f

Tactic:
intro hf

Goal state after:
α : Type u
f : α → Type (max u v)
hf : Surjective f
⊢ False
Module: Mathlib.Logic.Relation

Goal state before:
pp: case single.refl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ζ : Type u_6
r : α → α → Prop
a✝ b c✝ : α
inst✝ : IsTrans α r
a c : α
h₂ : r a c
⊢ ReflGen r a c

Tactic:
exact single h₂

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case tail.head
α : Type u_1
r : α → α → Prop
b✝ a b c : α
a✝ : TransGen r a b
hbc : r b c
h_ih :
  ∀ {motive : (a : α) → TransGen r a b → Prop},
    (∀ {a : α} (h : r a b), motive a ⋯) →
      (∀ {a c : α} (h' : r a c) (h : TransGen r c b), motive c h → motive a ⋯) → motive a a✝
motive : (a : α) → TransGen r a c → Prop
single : ∀ {a : α} (h : r a c), motive a ⋯
head : ∀ {a c_1 : α} (h' : r a c_1) (h : TransGen r c_1 c), motive c_1 h → motive a ⋯
⊢ ∀ {a c_1 : α} (h' : r a c_1) (h : TransGen r c_1 b), motive c_1 ⋯ → motive a ⋯

Tactic:
exact fun hab hbc ↦ head hab _

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

Goal state before:
pp: α : Sort u
β : Sort v
γ : Sort w
ra : α → α → Prop
rb : β → β → Prop
e : α ≃ β
eq : ∀ (a₁ a₂ : α), ra a₁ a₂ ↔ rb (e a₁) (e a₂)
⊢ RightInverse (Quot.map ⇑e.symm ⋯) (Quot.map ⇑e ⋯)

Tactic:
rintro ⟨a⟩; simp only [Quot.map, Equiv.apply_symm_apply]

Goal state after:
Module: Mathlib.Data.Option.Defs

Goal state before:
pp: α : Type u_3
β : Type u_4
b : β
f : α → β
a : Option α
⊢ Option.elim' b f a = a.elim b f

Tactic:
cases a

Goal state after:
case none
α : Type u_3
β : Type u_4
b : β
f : α → β
⊢ Option.elim' b f none = none.elim b f

case some
α : Type u_3
β : Type u_4
b : β
f : α → β
val✝ : α
⊢ Option.elim' b f (some val✝) = (some val✝).elim b f
Module: Mathlib.Logic.IsEmpty.Basic

Goal state before:
pp: α : Sort u_1
p : α → Prop
⊢ IsEmpty (Subtype p) ↔ ∀ (x : α), ¬p x

Tactic:
by
  simp only [← not_nonempty_iff, nonempty_subtype, not_exists]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
b : β
f : α → β
a : Option α
⊢ a.casesOn' b f = a.elim b f

Tactic:
cases a

Goal state after:
case none
α : Type u_1
β : Type u_2
b : β
f : α → β
⊢ none.casesOn' b f = none.elim b f

case some
α : Type u_1
β : Type u_2
b : β
f : α → β
val✝ : α
⊢ (some val✝).casesOn' b f = (some val✝).elim b f
Module: Mathlib.Order.BoundedOrder.Basic

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

Tactic:
by
  by_cases! H : ∀ a : α, ∃ b, ¬b ≤ a
  · exact PSum.inr ⟨H⟩
  · letI : Top α := ⟨Classical.choose H⟩
    exact PSum.inl ⟨Classical.choose_spec H⟩

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

Goal state before:
pp: a b c d e m n k : ℕ
p : ℕ → Prop
lo hi : ℕ
P : ℕ → Prop
inst✝ : DecidablePred P
⊢ (∀ (x : ℕ), x < hi - lo → P (lo + x)) ↔ ∀ (x : ℕ), lo ≤ x → x < hi → P x

Tactic:
by
    refine ⟨fun al x hl hh ↦ ?_,
      fun al x h ↦ al _ (Nat.le_add_right _ _) (Nat.lt_sub_iff_add_lt'.1 h)⟩
    have := al (x - lo) ((Nat.sub_lt_sub_iff_right hl).2 hh)
    rwa [Nat.add_sub_cancel' hl] at this

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

Goal state before:
pp: n : ℕ
inst✝ : n.AtLeastTwo
⊢ n - 1 ≠ 0

Tactic:
have := prop (n := n)

Goal state after:
n : ℕ
inst✝ : n.AtLeastTwo
this : 2 ≤ n
⊢ n - 1 ≠ 0
Module: Mathlib.Data.Set.Basic

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

Tactic:
simp [mem_dite]

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

Goal state before:
pp: α : Type u_1
s : Set α
x : α
⊢ s ⊂ {x} ↔ s = ∅

Tactic:
by
  rw [ssubset_iff_subset_ne, subset_singleton_iff_eq, or_and_right, and_not_self_iff, or_false,
    and_iff_left_iff_imp]
  exact fun h => h ▸ empty_ne_singleton _

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

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

Tactic:
exact fun h => Subsingleton.intro fun a b => SetCoe.ext (h a.property b.property)

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

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b : α
h : Codisjoint a b
⊢ (b ⇨ a) ⊓ ⊤ = a

Tactic:
inf_top_eq,

Goal state after:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b : α
h : Codisjoint a b
⊢ b ⇨ a = a
Module: Mathlib.Control.EquivFunctor

Goal state before:
pp: f : Type u₀ → Type u₁
inst✝ : EquivFunctor f
α β : Type u₀
e : α ≃ β
x : f α
⊢ map e.symm (map e x) = x

Tactic:
convert! (congr_fun (EquivFunctor.map_trans' e e.symm) x).symm
    simp

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

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
s : x ⊓ y ⊔ z = x
i : x ⊓ y ⊓ z = ⊥
⊢ x \ y = z

Tactic:
conv_rhs at s => rw [← sup_inf_sdiff x y, sup_comm]
  rw [sup_comm] at s
  conv_rhs at i => rw [← inf_inf_sdiff x y, inf_comm]
  rw [inf_comm] at i
  exact (eq_of_inf_eq_sup_eq i s).symm

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 ⊓ (z ⊔ x) ⊔ z ⊓ (z ⊔ x) = y

Tactic:
inf_sup_self,

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 = y
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 : Option α
⊢ ↑((fun e ↦
            ⟨{ toFun := fun a ↦ a.casesOn' x (Subtype.val ∘ ⇑e),
                invFun := fun b ↦ if h : b = x then none else some (e.symm ⟨b, h⟩), left_inv := ⋯, right_inv := ⋯ },
              ⋯⟩)
          ((fun e ↦
              { toFun := fun a ↦ ⟨↑e (some a), ⋯⟩, invFun := fun b ↦ ((↑e).symm ↑b).get ⋯, left_inv := ⋯,
                right_inv := ⋯ })
            e))
      a =
    ↑e a

Tactic:
cases a

Goal state after:
case none
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
x : β
e : { e // e none = x }
⊢ ↑((fun e ↦
            ⟨{ toFun := fun a ↦ a.casesOn' x (Subtype.val ∘ ⇑e),
                invFun := fun b ↦ if h : b = x then none else some (e.symm ⟨b, h⟩), left_inv := ⋯, right_inv := ⋯ },
              ⋯⟩)
          ((fun e ↦
              { toFun := fun a ↦ ⟨↑e (some a), ⋯⟩, invFun := fun b ↦ ((↑e).symm ↑b).get ⋯, left_inv := ⋯,
                right_inv := ⋯ })
            e))
      none =
    ↑e none

case some
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
x : β
e : { e // e none = x }
val✝ : α
⊢ ↑((fun e ↦
            ⟨{ toFun := fun a ↦ a.casesOn' x (Subtype.val ∘ ⇑e),
                invFun := fun b ↦ if h : b = x then none else some (e.symm ⟨b, h⟩), left_inv := ⋯, right_inv := ⋯ },
              ⋯⟩)
          ((fun e ↦
              { toFun := fun a ↦ ⟨↑e (some a), ⋯⟩, invFun := fun b ↦ ((↑e).symm ↑b).get ⋯, left_inv := ⋯,
                right_inv := ⋯ })
            e))
      (some val✝) =
    ↑e (some val✝)
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (y ⊓ (x ⊓ (x ⊔ z)) ⊔ x \ z) ⊓ (x ⊓ y ⊓ z ⊔ y \ z) = x ⊓ y ⊔ x \ z ⊓ y \ z

Tactic:
inf_sup_self,

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

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

Tactic:
(sdiff_eq_bot_iff (α := α)).2 inf_le_left,

Goal state after:
α : Type u
inst✝ : GeneralizedBooleanAlgebra α
a b c : α
⊢ a ⊓ b \ c = ⊥ ⊔ (a ⊓ b) \ c
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type ?u.12
β : Option α → Type u_9
f : (a : Option α) → β a
a : Option α
⊢ (fun x a ↦ Option.casesOn a x.fst x.snd) ((fun f ↦ (f none, fun a ↦ f (some a))) f) a = f a

Tactic:
cases a

Goal state after:
case none
α✝ : 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.12
β : Option α → Type u_9
f : (a : Option α) → β a
⊢ (fun x a ↦ Option.casesOn a x.fst x.snd) ((fun f ↦ (f none, fun a ↦ f (some a))) f) none = f none

case some
α✝ : 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.12
β : Option α → Type u_9
f : (a : Option α) → β a
val✝ : α
⊢ (fun x a ↦ Option.casesOn a x.fst x.snd) ((fun f ↦ (f none, fun a ↦ f (some a))) f) (some val✝) = f (some val✝)
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x y : α
inst✝ : BooleanAlgebra α
h : x = yᶜ
⊢ IsCompl x y

Tactic:
by
    rw [h]
    exact isCompl_compl.symm

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

Goal state before:
pp: ε : Type u_9
p : ε → Prop
inst✝ : DecidablePred p
ep : Perm { a // p a }
en : Perm { a // ¬p a }
a : ε
⊢ (ep.subtypeCongr en) a = if h : p a then ↑(ep ⟨a, h⟩) else ↑(en ⟨a, h⟩)

Tactic:
by_cases h : p a

Goal state after:
case pos
ε : Type u_9
p : ε → Prop
inst✝ : DecidablePred p
ep : Perm { a // p a }
en : Perm { a // ¬p a }
a : ε
h : p a
⊢ (ep.subtypeCongr en) a = if h : p a then ↑(ep ⟨a, h⟩) else ↑(en ⟨a, h⟩)

case neg
ε : Type u_9
p : ε → Prop
inst✝ : DecidablePred p
ep : Perm { a // p a }
en : Perm { a // ¬p a }
a : ε
h : ¬p a
⊢ (ep.subtypeCongr en) a = if h : p a then ↑(ep ⟨a, h⟩) else ↑(en ⟨a, h⟩)
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: α' : Type u_9
β' : Type u_10
e : Perm α'
p : β' → Prop
inst✝ : DecidablePred p
f : α' ≃ Subtype p
a : α'
⊢ (e.extendDomain f) ↑(f a) = ↑(f (e a))

Tactic:
by
  simp [Perm.extendDomain]

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

Goal state before:
pp: α' : Type u_9
β' : Type u_10
p : β' → Prop
inst✝ : DecidablePred p
f : α' ≃ Subtype p
⊢ extendDomain (Equiv.refl α') f = Equiv.refl β'

Tactic:
by
  simp [Perm.extendDomain]

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

Goal state before:
pp: α : Sort u_1
β : Sort u_4
P : α → Sort u_9
e : α ≃ β
g : (b : β) → P (e.symm b)
b : β
⊢ (piCongrLeft' P e).symm g (e.symm b) = g b

Tactic:
by
  rw [piCongrLeft'_symm_apply, ← heq_iff_eq, eqRec_heq_iff]
  exact congr_arg_heq _ (e.apply_symm_apply _)

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
symmDiff_eq,

Goal state after:
α : Type u_2
inst✝ : BooleanAlgebra α
a b c : α
⊢ a ⊓ (b ∆ c)ᶜ ⊔ b ∆ c ⊓ aᶜ = a ⊓ (b ⊓ c ⊔ bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ
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.Nonempty ∧ t.Nonempty

Tactic:
rwa [prod_nonempty_iff] at h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
⊢ Injective (image f)

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

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
⊢ InjOn f univ ↔ Injective f

Tactic:
simp [InjOn, Injective]

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

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
inst✝ : IsMulTorsionFree M
n : ℕ
a : M
hn : n ≠ 0
⊢ a ^ n = 1 ↔ a = 1

Tactic:
rw [← pow_left_inj (a := a) hn, one_pow]

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : ¬Classical.choice n ∈ s
x : β
hx : ¬x ∈ range f
⊢ x ∈ invFun f ⁻¹' s ↔ x ∈ f '' s

Tactic:
· have : x ∉ f '' s := fun h' => hx (image_subset_range _ _ h')
    simp only [mem_preimage, invFun_neg hx, h, this]

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a : α
m n : ℕ
⊢ a ^ (↑m * ↑n) = (a ^ ↑m) ^ ↑n

Tactic:
rw [zpow_natCast, zpow_natCast, ← pow_mul, ← zpow_natCast]
    rfl

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
x : G
m n : ℤ
h : x ^ n = 1
⊢ x ^ m = x ^ (m % n + n * (m / n))

Tactic:
by rw [Int.emod_add_mul_ediv]

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

Goal state before:
pp: G : Type u_3
inst✝ : CommGroup G
a b c d : G
⊢ b⁻¹ * a = d⁻¹ * c ↔ a * d = c * b

Tactic:
by
  rw [← div_eq_inv_mul, ← div_eq_inv_mul, div_eq_div_iff_mul_eq_mul]

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 * b * d = c / d * (b * d) ↔ a * d = c * b

Tactic:
hb.div_mul_cancel,

Goal state after:
α : Type u
inst✝ : DivisionCommMonoid α
a b c d : α
hb : IsUnit b
hd : IsUnit d
⊢ a * d = c / d * (b * d) ↔ a * d = c * b
Module: Mathlib.Control.Basic

Goal state before:
pp: α β γ : Type u
F : Type u → Type v
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
x : F (α → β)
f : γ → α
y : F γ
⊢ x <*> f <$> y = (fun x ↦ x ∘ f) <$> x <*> y

Tactic:
by
  simp only [← pure_seq]
  simp only [seq_assoc, seq_pure, ← comp_map]
  simp [pure_seq]
  rfl

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

Goal state before:
pp: case right
α : Type u_7
β : Type u_8
fst✝¹ : Perm α
snd✝¹ : Perm β
fst✝ : Perm α
snd✝ : Perm β
h : (sumCongrHom α β) (fst✝¹, snd✝¹) = (sumCongrHom α β) (fst✝, snd✝)
i : β
⊢ snd✝¹ i = snd✝ i

Tactic:
· simpa using Equiv.congr_fun h (Sum.inr i)

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

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

Tactic:
rw [cast_natCast, neg_ofNat_succ]

Goal state after:
R : Type u
inst✝ : AddGroupWithOne R
n : ℕ
⊢ ↑-[n+1] = -↑(n + 1)
Module: Mathlib.Algebra.Ring.Basic

Goal state before:
pp: R : Type u_3
inst✝ : NonUnitalNonAssocRing R
⊢ [NoZeroDivisors R, ∀ {a : R}, a ≠ 0 → ∀ (x : R), a * x = 0 → x = 0, ∀ {a : R}, a ≠ 0 → ∀ (x : R), x * a = 0 → x = 0,
      ∀ {a : R}, a ≠ 0 → (∀ (x : R), a * x = 0 → x = 0) ∧ ∀ (x : R), x * a = 0 → x = 0].TFAE

Tactic:
tfae_have 1 ↔ 2 := noZeroDivisors_iff_right_eq_zero_of_mul

Goal state after:
R : Type u_3
inst✝ : NonUnitalNonAssocRing R
tfae_1_iff_2 : NoZeroDivisors R ↔ ∀ {a : R}, a ≠ 0 → ∀ (x : R), a * x = 0 → x = 0
⊢ [NoZeroDivisors R, ∀ {a : R}, a ≠ 0 → ∀ (x : R), a * x = 0 → x = 0, ∀ {a : R}, a ≠ 0 → ∀ (x : R), x * a = 0 → x = 0,
      ∀ {a : R}, a ≠ 0 → (∀ (x : R), a * x = 0 → x = 0) ∧ ∀ (x : R), x * a = 0 → x = 0].TFAE
Module: Mathlib.Algebra.Ring.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : DivisionMonoid R
inst✝ : HasDistribNeg R
⊢ -1 * -1 = 1

Tactic:
by rw [neg_mul_neg, one_mul]

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

Goal state before:
pp: R : Type u
inst✝ : NonUnitalNonAssocRing R
a x y x' y' : R
h : SemiconjBy a x y
h' : SemiconjBy a x' y'
⊢ SemiconjBy a (x - x') (y - y')

Tactic:
by
  simpa only [sub_eq_add_neg] using h.add_right h'.neg_right

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

Goal state before:
pp: case inr
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
a : M₀
h : IsUnit a⁻¹ʳ
h✝ : Nontrivial M₀
⊢ IsUnit a

Tactic:
contrapose h

Goal state after:
case inr
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
a : M₀
h✝ : Nontrivial M₀
h : ¬IsUnit a
⊢ ¬IsUnit a⁻¹ʳ
Module: Mathlib.Algebra.Group.Commute.Units

Goal state before:
pp: M : Type u_1
inst✝ : DivisionMonoid M
a b c d : M
hbd : Commute b d
hb : IsUnit b
hd : IsUnit d
⊢ a / b * b * d = c / d * (b * d) ↔ a * d = c * b

Tactic:
hb.div_mul_cancel,

Goal state after:
M : Type u_1
inst✝ : DivisionMonoid M
a b c d : M
hbd : Commute b d
hb : IsUnit b
hd : IsUnit d
⊢ a * d = c / d * (b * d) ↔ a * d = c * b
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

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

Tactic:
have h1 : m - n + n = m := Nat.sub_add_cancel h

Goal state after:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
m n : ℕ
a : G₀
ha : a ≠ 0
h : n ≤ m
h1 : m - n + n = m
⊢ a ^ (m - n) = a ^ m * (a ^ n)⁻¹
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

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

Tactic:
by
  simpa using zpow_sub₀ ha n 1

Goal state after:
Module: Mathlib.Algebra.Module.NatInt

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
z : ℕ
a : M
⊢ ↑↑z.succ • a = ↑↑z • a + a

Tactic:
simp [add_comm, add_smul]

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

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

Tactic:
rw [mul_add, add_mul, mul_one, ← add_assoc, one_mul, mul_assoc, ← mul_add, ← mul_add, ← mul_assoc,
    ← Nat.cast_two, ← Nat.cast_comm]

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 : α
⊢ a - (b + c) = a - c - b

Tactic:
rw [add_comm]
  apply tsub_add_eq_tsub_tsub

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

Goal state before:
pp: M₀ : Type u_2
inst✝² : MonoidWithZero M₀
inst✝¹ : Preorder M₀
a b : M₀
inst✝ : MulPosMono M₀
ha : a ≤ 1
hb₀ : 0 ≤ b
hb : b ≤ 1
⊢ 1 * b ≤ 1

Tactic:
by rwa [one_mul]

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 d : R
inst✝³ : AddLeftReflectLT R
inst✝² : ExistsAddOfLE R
inst✝¹ : MulPosStrictMono R
inst✝ : AddLeftStrictMono R
hba : b < a
hdc : d < c
⊢ a * d + b * c < a * c + b * d

Tactic:
by
  rw [add_comm (a * d), add_comm (a * c)]
  exact mul_add_mul_lt_mul_add_mul hba hdc

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

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : ZeroLEOneClass G₀
n : ℤ
ha : 1 ≤ a
hn : 0 ≤ n
⊢ 1 ≤ a ^ n

Tactic:
by simpa using zpow_right_mono₀ ha hn

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

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : ZeroLEOneClass G₀
n : ℤ
ha₀ : 0 < a
ha₁ : a < 1
⊢ 1 < a ^ n ↔ n < 0

Tactic:
by
  simp [← zpow_lt_zpow_iff_right_of_lt_one₀ ha₀ ha₁]

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

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : ZeroLEOneClass G₀
n : ℤ
ha₀ : 0 < a
ha₁ : a < 1
⊢ a ^ n < 1 ↔ 0 < n

Tactic:
by
  simp [← zpow_lt_zpow_iff_right_of_lt_one₀ ha₀ ha₁]

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

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : MulPosReflectLT G₀
a b : G₀
inst✝ : ZeroLEOneClass G₀
h : a ≤ b
hb : 0 ≤ b
⊢ a ≤ 1 * b

Tactic:
by rwa [one_mul]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type ?u.35
α₂ : Type ?u.38
β₁ : Type ?u.34
β₂ : Type ?u.37
r₁ : α₁ → α₁ → Prop
r₂ : α₂ → α₂ → Prop
s₁ : β₁ → β₁ → Prop
s₂ : β₂ → β₂ → Prop
a b : α₁ ⊕ α₂
f : α₁ ≃ β₁
hf : ∀ {a b : α₁}, s₁ (f a) (f b) ↔ r₁ a b
g : α₂ ≃ β₂
hg : ∀ {a b : α₂}, s₂ (g a) (g b) ↔ r₂ a b
⊢ Sum.Lex s₁ s₂ (({ toEquiv := f, map_rel_iff' := hf }.sumCongr { toEquiv := g, map_rel_iff' := hg }.toEquiv) a)
      (({ toEquiv := f, map_rel_iff' := hf }.sumCongr { toEquiv := g, map_rel_iff' := hg }.toEquiv) b) ↔
    Sum.Lex r₁ r₂ a b

Tactic:
cases a

Goal state after:
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type ?u.35
α₂ : Type ?u.38
β₁ : Type ?u.34
β₂ : Type ?u.37
r₁ : α₁ → α₁ → Prop
r₂ : α₂ → α₂ → Prop
s₁ : β₁ → β₁ → Prop
s₂ : β₂ → β₂ → Prop
b : α₁ ⊕ α₂
f : α₁ ≃ β₁
hf : ∀ {a b : α₁}, s₁ (f a) (f b) ↔ r₁ a b
g : α₂ ≃ β₂
hg : ∀ {a b : α₂}, s₂ (g a) (g b) ↔ r₂ a b
val✝ : α₁
⊢ Sum.Lex s₁ s₂
      (({ toEquiv := f, map_rel_iff' := hf }.sumCongr { toEquiv := g, map_rel_iff' := hg }.toEquiv) (Sum.inl val✝))
      (({ toEquiv := f, map_rel_iff' := hf }.sumCongr { toEquiv := g, map_rel_iff' := hg }.toEquiv) b) ↔
    Sum.Lex r₁ r₂ (Sum.inl val✝) b

case inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type ?u.35
α₂ : Type ?u.38
β₁ : Type ?u.34
β₂ : Type ?u.37
r₁ : α₁ → α₁ → Prop
r₂ : α₂ → α₂ → Prop
s₁ : β₁ → β₁ → Prop
s₂ : β₂ → β₂ → Prop
b : α₁ ⊕ α₂
f : α₁ ≃ β₁
hf : ∀ {a b : α₁}, s₁ (f a) (f b) ↔ r₁ a b
g : α₂ ≃ β₂
hg : ∀ {a b : α₂}, s₂ (g a) (g b) ↔ r₂ a b
val✝ : α₂
⊢ Sum.Lex s₁ s₂
      (({ toEquiv := f, map_rel_iff' := hf }.sumCongr { toEquiv := g, map_rel_iff' := hg }.toEquiv) (Sum.inr val✝))
      (({ toEquiv := f, map_rel_iff' := hf }.sumCongr { toEquiv := g, map_rel_iff' := hg }.toEquiv) b) ↔
    Sum.Lex r₁ r₂ (Sum.inr val✝) b
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Preorder α✝
inst✝² : Preorder β✝
α : Type ?u.13
β : Type ?u.15
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
g : β → α
h : ∀ (a : α) (b : β), cmp a (g b) = cmp (f a) b
gf : ∀ (a : α), a = g (f a)
⊢ Function.RightInverse g f

Tactic:
intro
      rw [← cmp_eq_eq_iff, ← h, cmp_self_eq_eq]

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

Goal state before:
pp: M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulLeftStrictMono M
a : M
ha : 1 < a
n : ℕ
⊢ a ^ n < a ^ n * a

Tactic:
exact lt_mul_of_one_lt_right' (a ^ n) ha

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 : G
⊢ |b|ₘ / |a|ₘ ≤ |a / b|ₘ

Tactic:
rw [mabs_div_comm]; apply mabs_div_mabs_le_mabs_div

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 α
⊢ |(a ⊔ c) / (b ⊔ c)|ₘ * |(a ⊓ c) / (b ⊓ c)|ₘ = (b ⊔ c ⊔ (a ⊔ c)) / ((b ⊔ c) ⊓ (a ⊔ c)) * |(a ⊓ c) / (b ⊓ c)|ₘ

Tactic:
by
        rw [sup_div_inf_eq_mabs_div]

Goal state after:
Module: Mathlib.Data.Option.NAry

Goal state before:
pp: α β γ : Type u
f : α → β → γ
a : Option α
b : Option β
⊢ map₂ f a b = f <$> a <*> b

Tactic:
cases a

Goal state after:
case none
α β γ : Type u
f : α → β → γ
b : Option β
⊢ map₂ f none b = f <$> none <*> b

case some
α β γ : Type u
f : α → β → γ
b : Option β
val✝ : α
⊢ map₂ f (some val✝) b = f <$> some val✝ <*> b