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

Goal state before:
pp: motive : Nat → Sort u
zero : motive 0
bit : (b : Bool) → (n : Nat) → motive n → motive (Nat.bit b n)
h : bit false 0 zero = zero ∨ (0 = 0 → false = true)
h' : Nat.bit false 0 = 0
⊢ binaryRec zero bit (Nat.bit false 0) = bit false 0 (binaryRec zero bit 0)

Tactic:
simp only [Bool.false_eq_true, imp_false, not_true_eq_false, or_false] at h

Goal state after:
motive : Nat → Sort u
zero : motive 0
bit : (b : Bool) → (n : Nat) → motive n → motive (Nat.bit b n)
h' : Nat.bit false 0 = 0
h : bit false 0 zero = zero
⊢ binaryRec zero bit (Nat.bit false 0) = bit false 0 (binaryRec zero bit 0)
Module: Mathlib.Algebra.Group.Defs

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

Tactic:
rw [pow_succ, one_pow, one_mul]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
inst✝ : DecidableEq α
a : α
p : α → Prop
⊢ (p a ∧ ∀ (b : α), b ≠ a → p b) ↔ ∀ (b : α), p b

Tactic:
simp only [← @forall_eq _ p a, ← forall_and, ← or_imp, Decidable.em, forall_const]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Membership α β
p : Prop
inst✝ : Decidable p
a : α
s : p → β
t : ¬p → β
⊢ (a ∈ if h : p then s h else t h) ↔ (∀ (h : p), a ∈ s h) ∧ ∀ (h : ¬p), a ∈ t h

Tactic:
by
  by_cases h : p <;> simp [h]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Membership α β
p : Prop
inst✝ : Decidable p
a : p → α
b : ¬p → α
s : β
⊢ (if h : p then a h else b h) ∈ s ↔ (∀ (h : p), a h ∈ s) ∧ ∀ (h : ¬p), b h ∈ s

Tactic:
by
  by_cases h : p <;> simp [h]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Type u_1
inst1 inst2 : BEq α
h : ∀ (x y : α), (x == y) = (x == y)
⊢ inst1 = inst2

Tactic:
have ⟨beq1⟩ := inst1

Goal state after:
α : Type u_1
inst1 inst2 : BEq α
beq1 : α → α → Bool
h : ∀ (x y : α), (x == y) = (x == y)
⊢ { beq := beq1 } = inst2
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_2
f✝ : α → β
γ : Type u_4
inst✝ : Nontrivial γ
surj : Surjective fun g ↦ g ∘ f✝
c c' : γ
not_inj : ∃ x x_1 x_2, ¬x = x_1
a₁ a₂ : α
eq : f✝ a₁ = f✝ a₂
ne : ¬a₁ = a₂
f : β → γ
hf : (fun g ↦ g ∘ f✝) f = fun x ↦ if x = a₂ then c else c'
h₁ : (fun g ↦ g ∘ f✝) f a₁ = if a₁ = a₂ then c else c'
h₂ : (fun g ↦ g ∘ f✝) f a₂ = if a₂ = a₂ then c else c'
⊢ c = c'

Tactic:
simp only [comp_apply, if_neg ne, reduceIte] at h₁ h₂

Goal state after:
α : Sort u_1
β : Sort u_2
f✝ : α → β
γ : Type u_4
inst✝ : Nontrivial γ
surj : Surjective fun g ↦ g ∘ f✝
c c' : γ
not_inj : ∃ x x_1 x_2, ¬x = x_1
a₁ a₂ : α
eq : f✝ a₁ = f✝ a₂
ne : ¬a₁ = a₂
f : β → γ
hf : (fun g ↦ g ∘ f✝) f = fun x ↦ if x = a₂ then c else c'
h₁ : f (f✝ a₁) = c'
h₂ : f (f✝ a₂) = c
⊢ c = c'
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: case refine_1.refine_1
α : Sort u_1
β : Sort u_2
r : α → β → Prop
h : ∀ (a : α), ∃! b, r a b
a✝ : α
b✝ : β
hr : r a✝ b✝
⊢ (fun a ↦ Exists.choose ⋯) a✝ = b✝

pp: case refine_1.refine_2
α : Sort u_1
β : Sort u_2
r : α → β → Prop
h : ∀ (a : α), ∃! b, r a b
a✝ : α
b✝ : β
h' : (fun a ↦ Exists.choose ⋯) a✝ = b✝
⊢ r a✝ ((fun a ↦ Exists.choose ⋯) a✝)

Tactic:
exacts [((h _).choose_spec.2 _ hr).symm, (h _).choose_spec.1]

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

Goal state before:
pp: G : Type u_3
H : Type u_4
inst✝⁴ : Group G
inst✝³ : Mul H
inst✝² : MulAction G H
inst✝¹ : SMulCommClass G H H
inst✝ : IsScalarTower G H H
a b x : H
r : G
h : SemiconjBy (r • x) a b
⊢ SemiconjBy x a b

Tactic:
by simpa using h.smul_left r⁻¹

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

Goal state before:
pp: p : Prop
⊢ IsEmpty p ↔ ¬p

Tactic:
by
  simp only [← not_nonempty_iff, nonempty_prop]

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

Goal state before:
pp: α : Type u_4
β : Type u_5
⊢ IsEmpty (α × β) ↔ IsEmpty α ∨ IsEmpty β

Tactic:
simp only [← not_nonempty_iff, nonempty_prod, not_and_or]

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

Goal state before:
pp: case inl
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h₁ : a < b
h₂ : a < c
h✝ : b ≤ c
⊢ a < min b c

Tactic:
simp [min_eq_left, min_eq_right, *]

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

Goal state before:
pp: case inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h₁ : a < b
h₂ : a < c
h✝ : c ≤ b
⊢ a < min b c

Tactic:
simp [min_eq_left, min_eq_right, *]

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: case inl
α : Type u_2
inst✝ : LinearOrder α
a b : α
p : α → Prop
ha : a ≤ b → p a
hb : b ≤ a → p b
hab : a ≤ b
⊢ p (min a b)

Tactic:
simp [min_eq_left, min_eq_right, *]

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: case inr
α : Type u_2
inst✝ : LinearOrder α
a b : α
p : α → Prop
ha : a ≤ b → p a
hb : b ≤ a → p b
hba : b ≤ a
⊢ p (min a b)

Tactic:
simp [min_eq_left, min_eq_right, *]

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ Injective fun a ↦ a ^ n

Tactic:
simp [Injective, le_antisymm_iff, Nat.pow_le_pow_iff_left hn]

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
δ : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
f : α → γ
g : β → δ
hf : StrictAnti f
hg : StrictAnti g
a b : α × β
⊢ a.fst < b.fst ∧ a.snd ≤ b.snd ∨ a.fst ≤ b.fst ∧ a.snd < b.snd →
    (Prod.map f g b).fst < (Prod.map f g a).fst ∧ (Prod.map f g b).snd ≤ (Prod.map f g a).snd ∨
      (Prod.map f g b).fst ≤ (Prod.map f g a).fst ∧ (Prod.map f g b).snd < (Prod.map f g a).snd

Tactic:
exact Or.imp (And.imp hf.imp hg.antitone.imp) (And.imp hf.antitone.imp hg.imp)

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
a b : α
ha : a ≠ ⊥
hab : Disjoint a b
h : a = b
⊢ Disjoint a a

Tactic:
by rwa [← h] at hab

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

Goal state before:
pp: case mp
α : Type u_1
l : List α
H : l.Nodup
a : α
⊢ {x | x ∈ l} = {a} → l = [a]

Tactic:
rw [ofPred_mem_list_eq_replicate]
    rintro ⟨n, hn, rfl⟩
    simp only [List.nodup_replicate] at H
    simp [show n = 1 by lia]

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

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

Tactic:
rw [inf_comm, inf_sdiff_self_right]

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

Goal state before:
pp: α : Type u_1
t s s' : Set α
⊢ s ∩ (t ∩ t) ∪ ∅ = s ∩ t

Tactic:
inter_self,

Goal state after:
α : Type u_1
t s s' : Set α
⊢ s ∩ t ∪ ∅ = s ∩ t
Module: Mathlib.Order.BooleanAlgebra.Basic

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

Tactic:
by rw [inf_sdiff_self_left, bot_inf_eq, inf_bot_eq, bot_sup_eq]

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

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

Tactic:
rw [inf_assoc, ← inf_sup_left, sup_inf_sdiff]

Goal state after:
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_9
β : Type u_10
f : α → β
p : α → Prop
q : β → Prop
h : ∀ (x : α), p x ↔ q (f x)
⊢ (a : Subtype q) → { x // f x = ↑a } ≃ { x // ⟨f ↑x, ⋯⟩ = a }

Tactic:
intro y

Goal state after:
α✝ : 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
β : Type u_10
f : α → β
p : α → Prop
q : β → Prop
h : ∀ (x : α), p x ↔ q (f x)
y : Subtype q
⊢ { x // f x = ↑y } ≃ { x // ⟨f ↑x, ⋯⟩ = y }
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: α : Sort u_1
inst✝ : DecidableEq α
r a b : α
⊢ (if (if r = a then b else if r = b then a else r) = a then b
    else if (if r = a then b else if r = b then a else r) = b then a else if r = a then b else if r = b then a else r) =
    r

Tactic:
split_ifs <;> grind

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

Goal state before:
pp: α : Sort u_1
inst✝ : DecidableEq α
r a b : α
⊢ (if r = a then b else if r = b then a else r) = if r = b then a else if r = a then b else r

Tactic:
split_ifs <;> grind

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

Goal state before:
pp: α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : BooleanAlgebra β
top : Top α := e.top
compl : Compl α := e.compl
himp : HImp α := e.himp
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := e.generalizedBooleanAlgebra
⊢ BooleanAlgebra α

Tactic:
apply e.injective.booleanAlgebra

Goal state after:
case le
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : BooleanAlgebra β
top : Top α := ⋯
compl : Compl α := ⋯
himp : HImp α := ⋯
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := ⋯
⊢ ∀ {x y : α}, e x ≤ e y ↔ x ≤ y

case lt
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : BooleanAlgebra β
top : Top α := ⋯
compl : Compl α := ⋯
himp : HImp α := ⋯
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := ⋯
⊢ ∀ {x y : α}, e x < e y ↔ x < y

case map_sup
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : BooleanAlgebra β
top : Top α := ⋯
compl : Compl α := ⋯
himp : HImp α := ⋯
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := ⋯
⊢ ∀ (a b : α), e (a ⊔ b) = e a ⊔ e b

case map_inf
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : BooleanAlgebra β
top : Top α := ⋯
compl : Compl α := ⋯
himp : HImp α := ⋯
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := ⋯
⊢ ∀ (a b : α), e (a ⊓ b) = e a ⊓ e b

case map_top
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : BooleanAlgebra β
top : Top α := ⋯
compl : Compl α := ⋯
himp : HImp α := ⋯
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := ⋯
⊢ e ⊤ = ⊤

case map_bot
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : BooleanAlgebra β
top : Top α := ⋯
compl : Compl α := ⋯
himp : HImp α := ⋯
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := ⋯
⊢ e ⊥ = ⊥

case map_compl
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : BooleanAlgebra β
top : Top α := ⋯
compl : Compl α := ⋯
himp : HImp α := ⋯
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := ⋯
⊢ ∀ (a : α), e aᶜ = (e a)ᶜ

case map_sdiff
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : BooleanAlgebra β
top : Top α := ⋯
compl : Compl α := ⋯
himp : HImp α := ⋯
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := ⋯
⊢ ∀ (a b : α), e (a \ b) = e a \ e b

case map_himp
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : BooleanAlgebra β
top : Top α := ⋯
compl : Compl α := ⋯
himp : HImp α := ⋯
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := ⋯
⊢ ∀ (a b : α), e (a ⇨ b) = e a ⇨ e b
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.14
ι' : Type ?u.13
π : ι ⊕ ι' → Type u_9
f : (i : ι ⊕ ι') → π i
⊢ (fun g t ↦ Sum.rec g.fst g.snd t) ((fun f ↦ (fun i ↦ f (inl i), fun i' ↦ f (inr i'))) f) = f

Tactic:
by ext (i | i) <;> rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
⊢ Injective (preimage f) ↔ Surjective f

Tactic:
by
  rw [← Injective.of_comp_iff Set.mem_injective, ← Injective.of_comp_iff' _ Set.ofPred_bijective]
  exact injective_comp_right_iff_surjective

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
⊢ Disjoint t (f '' s) ↔ Disjoint (f ⁻¹' t) s

Tactic:
rw [disjoint_comm, disjoint_comm (b := s), disjoint_image_left]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s t u : Set α
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
x : β
y : α
ys : y ∈ s
hy : f y = x
z : α
zt : z ∈ t
hz : f z = x
⊢ f y = f z

Tactic:
rwa [← hz] at hy

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s t u : Set α
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
x : β
y : α
ys : y ∈ s
hy : f y = x
z : α
zt : z ∈ t
hz : f z = x
this : y = z
⊢ x ∈ f '' (s ∩ t)

Tactic:
rw [← this] at zt

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s t u : Set α
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
x : β
y : α
ys : y ∈ s
hy : f y = x
z : α
zt : y ∈ t
hz : f z = x
this : y = z
⊢ x ∈ f '' (s ∩ t)
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t₁ t₂ : Set β
f : α → β
h₁ : SurjOn f s₁ t₁
h₂ : SurjOn f s₂ t₂
h : InjOn f (s₁ ∪ s₂)
⊢ SurjOn f (s₁ ∩ s₂) (t₁ ∩ t₂)

Tactic:
intro y

Goal state after:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t₁ t₂ : Set β
f : α → β
h₁ : SurjOn f s₁ t₁
h₂ : SurjOn f s₂ t₂
h : InjOn f (s₁ ∪ s₂)
y : β
⊢ y ∈ t₁ ∩ t₂ → y ∈ f '' (s₁ ∩ s₂)
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
h : BijOn f s ∅
⊢ s = ∅

Tactic:
simpa using h.mapsTo

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

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
f : α → β
g : β → α
s : Set α
hgf : LeftInvOn g f s
ginj : InjOn g (g ⁻¹' s)
x : β
hx : x ∈ g ⁻¹' s
⊢ MapsTo f s (g ⁻¹' s)

Tactic:
intro y

Goal state after:
case mpr
α : Type u_1
β : Type u_2
f : α → β
g : β → α
s : Set α
hgf : LeftInvOn g f s
ginj : InjOn g (g ⁻¹' s)
x : β
hx : x ∈ g ⁻¹' s
y : α
⊢ y ∈ s → f y ∈ g ⁻¹' s
Module: Mathlib.Algebra.Group.Units.Hom

Goal state before:
pp: M : Type u
N : Type v
P : Type w
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
f : M →* N
val inv : M
val_inv : val * inv = 1
inv_val : inv * val = 1
⊢ f inv * f val = 1

Tactic:
simp [← map_mul, inv_val]

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

Goal state before:
pp: F : Type u_1
M : Type u_3
N : Type u_4
inst✝³ : FunLike F M N
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : MonoidHomClass F M N
f : F
x : M
h : IsUnit x
⊢ IsUnit (f x)

Tactic:
by
  rcases h with ⟨y, rfl⟩; exact (Units.map (f : M →* N) y).isUnit

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

Goal state before:
pp: case zero
M₀ : Type u_1
inst✝¹ : MonoidWithZero M₀
M : Type u_2
inst✝ : Monoid M
f : M₀ → M
x : M₀
hx : ∀ (y : M₀), f (x * y) = f x * f y
⊢ ∀ (y : M₀), f (x ^ 0 * y) = f x ^ 0 * f y

Tactic:
intro y

Goal state after:
case zero
M₀ : Type u_1
inst✝¹ : MonoidWithZero M₀
M : Type u_2
inst✝ : Monoid M
f : M₀ → M
x : M₀
hx : ∀ (y : M₀), f (x * y) = f x * f y
y : M₀
⊢ f (x ^ 0 * y) = f x ^ 0 * f y
Module: Mathlib.Algebra.GroupWithZero.Defs

Goal state before:
pp: case succ
M₀ : Type u_1
inst✝¹ : MonoidWithZero M₀
M : Type u_2
inst✝ : Monoid M
f : M₀ → M
x : M₀
hx : ∀ (y : M₀), f (x * y) = f x * f y
n : ℕ
hn : ∀ (y : M₀), f (x ^ n * y) = f x ^ n * f y
⊢ ∀ (y : M₀), f (x ^ (n + 1) * y) = f x ^ (n + 1) * f y

Tactic:
intro y

Goal state after:
case succ
M₀ : Type u_1
inst✝¹ : MonoidWithZero M₀
M : Type u_2
inst✝ : Monoid M
f : M₀ → M
x : M₀
hx : ∀ (y : M₀), f (x * y) = f x * f y
n : ℕ
hn : ∀ (y : M₀), f (x ^ n * y) = f x ^ n * f y
y : M₀
⊢ f (x ^ (n + 1) * y) = f x ^ (n + 1) * f y
Module: Mathlib.Algebra.GroupWithZero.InjSurj

Goal state before:
pp: M₀ : Type u_1
M₀' : Type u_3
inst✝⁴ : Mul M₀
inst✝³ : Zero M₀
inst✝² : Mul M₀'
inst✝¹ : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst✝ : NoZeroDivisors M₀'
a b : M₀
H : a * b = 0
⊢ f a * f b = 0

Tactic:
by rw [← mul, H, zero]

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

Goal state before:
pp: M₀ : Type u_1
M₀' : Type u_3
inst✝⁴ : Mul M₀
inst✝³ : Zero M₀
inst✝² : Mul M₀'
inst✝¹ : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst✝ : NoZeroDivisors M₀'
a b : M₀
H✝ : a * b = 0
this : f a * f b = 0
H : f a = 0
⊢ f a = f 0

Tactic:
rwa [zero]

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

Goal state before:
pp: M₀ : Type u_1
M₀' : Type u_3
inst✝⁴ : Mul M₀
inst✝³ : Zero M₀
inst✝² : Mul M₀'
inst✝¹ : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst✝ : NoZeroDivisors M₀'
a b : M₀
H✝ : a * b = 0
this : f a * f b = 0
H : f b = 0
⊢ f b = f 0

Tactic:
rwa [zero]

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
h1 : k.succ % 2 = 1
⊢ ↑((k + 1) / 2 + (k + 1) / 2) + 1 = ↑((k + 1) % 2 + 2 * ((k + 1) / 2))

Tactic:
rw [h1, Nat.add_comm 1, Nat.succ_mul, Nat.one_mul]

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
h1 : k.succ % 2 = 1
⊢ ↑((k + 1) / 2 + (k + 1) / 2) + 1 = ↑((k + 1) / 2 + (k + 1) / 2 + 1)
Module: Mathlib.Data.Nat.Cast.Defs

Goal state before:
pp: A : Type u_2
inst✝ : AddMonoidWithOne A
⊢ 0 • 1 = ↑0

Tactic:
by simp [zero_nsmul]

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

Goal state before:
pp: α : Type u
inst✝² : MulZeroClass α
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b : α
⊢ ((if P then a else 0) * if Q then b else 0) = if P ∧ Q then a * b else 0

Tactic:
by
  simp only [← ite_and, ite_mul, mul_ite, mul_zero, zero_mul, and_comm]

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
a b : Rˣ
⊢ ↑a = ↑b ∨ ↑a = -↑b ↔ ↑a = ↑b ∨ ↑a = ↑(-b)

Tactic:
Units.val_neg

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

Goal state before:
pp: α : Type u_4
f : α → α
hf : Involutive f
n : ℕ
⊢ f^[2 * n + 1] = f

Tactic:
by
  rw [iterate_succ, hf.iterate_two_mul, id_comp]

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
hab : a < b
hcd : c < d
⊢ a * d + b * c < a * c + b * d

Tactic:
obtain ⟨d, hd, rfl⟩ := exists_pos_add_of_lt' hcd

Goal state after:
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : PartialOrder R
a b c : R
inst✝³ : AddLeftReflectLT R
inst✝² : ExistsAddOfLE R
inst✝¹ : MulPosStrictMono R
inst✝ : AddLeftStrictMono R
hab : a < b
d : R
hd : 0 < d
hcd : c < c + d
⊢ a * (c + d) + b * c < a * c + b * (c + d)
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁶ : CommSemiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : ExistsAddOfLE R
inst✝³ : MulPosStrictMono R
inst✝² : PosMulStrictMono R
inst✝¹ : AddLeftReflectLE R
inst✝ : AddLeftMono R
a b r : R
ha : 0 ≤ a
hb : 0 ≤ b
ht : r ^ 2 ≤ a * b
⊢ 2 * r ≤ a + b

Tactic:
apply nonneg_le_nonneg_of_sq_le_sq (Left.add_nonneg ha hb)
  rw [mul_mul_mul_comm, ← pow_two r, two_mul, two_add_two_eq_four]
  grw [mul_le_mul_of_nonneg_left ht zero_le_four, ← mul_assoc, four_mul_le_sq_add a b, sq]

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

Goal state before:
pp: G₀ : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ a < b / c ↔ c * a < b

Tactic:
rw [lt_div_iff₀ hc, mul_comm]

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

Goal state before:
pp: case inr.inl.inl
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
hab : a ≤ b
ha : a < 1
hb : 1 ≤ b
this : (|a * b|ₘ = a⁻¹ * b ↔ b ≤ 1) ↔ (|a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1)
h : a⁻¹ * b⁻¹ = a⁻¹ * b
ab : a * b ≤ 1
⊢ b⁻¹ = b

Tactic:
mul_right_inj

Goal state after:
case inr.inl.inl
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
hab : a ≤ b
ha : a < 1
hb : 1 ≤ b
this : (|a * b|ₘ = a⁻¹ * b ↔ b ≤ 1) ↔ (|a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1)
h : b⁻¹ = b
ab : a * b ≤ 1
⊢ b⁻¹ = b
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: case inr
M₀ : Type u_1
N₀ : Type u_2
G₀ : Type u_3
inst✝⁵ : MulZeroOneClass M₀
inst✝⁴ : Nontrivial M₀
inst✝³ : NoZeroDivisors M₀
inst✝² : MulZeroOneClass N₀
inst✝¹ : MulZeroOneClass G₀
inst✝ : DecidablePred fun x ↦ x = 0
f : N₀ →*₀ G₀
x : M₀
hx : x ≠ 0
⊢ f (1 x) = 1 x

Tactic:
one_apply_of_ne_zero hx,

Goal state after:
case inr
M₀ : Type u_1
N₀ : Type u_2
G₀ : Type u_3
inst✝⁵ : MulZeroOneClass M₀
inst✝⁴ : Nontrivial M₀
inst✝³ : NoZeroDivisors M₀
inst✝² : MulZeroOneClass N₀
inst✝¹ : MulZeroOneClass G₀
inst✝ : DecidablePred fun x ↦ x = 0
f : N₀ →*₀ G₀
x : M₀
hx : x ≠ 0
⊢ f 1 = 1 x
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: case inr
M₀ : Type u_1
N₀ : Type u_2
G₀ : Type u_3
inst✝⁵ : MulZeroOneClass M₀
inst✝⁴ : Nontrivial M₀
inst✝³ : NoZeroDivisors M₀
inst✝² : MulZeroOneClass N₀
inst✝¹ : MulZeroOneClass G₀
inst✝ : DecidablePred fun x ↦ x = 0
f : N₀ →*₀ G₀
x : M₀
hx : x ≠ 0
⊢ f 1 = 1 x

Tactic:
one_apply_of_ne_zero hx,

Goal state after:
case inr
M₀ : Type u_1
N₀ : Type u_2
G₀ : Type u_3
inst✝⁵ : MulZeroOneClass M₀
inst✝⁴ : Nontrivial M₀
inst✝³ : NoZeroDivisors M₀
inst✝² : MulZeroOneClass N₀
inst✝¹ : MulZeroOneClass G₀
inst✝ : DecidablePred fun x ↦ x = 0
f : N₀ →*₀ G₀
x : M₀
hx : x ≠ 0
⊢ f 1 = 1
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: case coe.zero.coe
α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddZeroClass α
inst✝ : AddLeftMono α
h : ∀ (a : α), 0 ≤ a
a✝¹ a✝ : α
hbc : 0 ≤ ↑a✝
⊢ ↑a✝¹ ≤ ↑a✝¹ + ↑a✝

Tactic:
rw [← coe_add, coe_le_coe]
      exact le_add_of_nonneg_right (h _)

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

Goal state before:
pp: F : Type u_1
α✝ : Type u_2
β : Type u_3
α : Type ?u.6
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedRing α
floor : α → ℤ
gc_coe_floor : GaloisConnection Int.cast floor
a : α
z : ℤ
⊢ (fun a ↦ -floor (-a)) a ≤ z ↔ a ≤ ↑z

Tactic:
neg_le,

Goal state after:
F : Type u_1
α✝ : Type u_2
β : Type u_3
α : Type ?u.6
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedRing α
floor : α → ℤ
gc_coe_floor : GaloisConnection Int.cast floor
a : α
z : ℤ
⊢ -z ≤ floor (-a) ↔ a ≤ ↑z
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: case inr
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
n : ℕ
hn : n ≠ 0
a : R
ha : 0 ≤ a
m : ℕ
⊢ m ≤ ⌊a * ↑n⌋₊ / n ↔ m ≤ ⌊a⌋₊

Tactic:
le_div_iff_mul_le (zero_lt_of_ne_zero hn),

Goal state after:
case inr
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
n : ℕ
hn : n ≠ 0
a : R
ha : 0 ≤ a
m : ℕ
⊢ m * n ≤ ⌊a * ↑n⌋₊ ↔ m ≤ ⌊a⌋₊
Module: Mathlib.Order.Directed

Goal state before:
pp: case inl.inl
α : Type u_1
r : α → α → Prop
inst✝ : Std.Refl r
s : Set α
hd : DirectedOn r s
y : α
ha : ∀ b ∈ s, ∃ c ∈ s, r y c ∧ r b c
⊢ ∃ z ∈ insert y s, r y z ∧ r y z

pp: case inl.inr
α : Type u_1
r : α → α → Prop
inst✝ : Std.Refl r
s : Set α
hd : DirectedOn r s
x : α
ha : ∀ b ∈ s, ∃ c ∈ s, r x c ∧ r b c
y : α
hy : y ∈ s
⊢ ∃ z ∈ insert x s, r x z ∧ r y z

pp: case inr.inl
α : Type u_1
r : α → α → Prop
inst✝ : Std.Refl r
s : Set α
hd : DirectedOn r s
x : α
hx : x ∈ s
y : α
ha : ∀ b ∈ s, ∃ c ∈ s, r y c ∧ r b c
⊢ ∃ z ∈ insert y s, r x z ∧ r y z

pp: case inr.inr
α : Type u_1
r : α → α → Prop
inst✝ : Std.Refl r
a : α
s : Set α
hd : DirectedOn r s
ha : ∀ b ∈ s, ∃ c ∈ s, r a c ∧ r b c
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ ∃ z ∈ insert a s, r x z ∧ r y z

Tactic:
· exact ⟨y, Set.mem_insert _ _, refl _, refl _⟩

Goal state after:
case inl.inr
α : Type u_1
r : α → α → Prop
inst✝ : Std.Refl r
s : Set α
hd : DirectedOn r s
x : α
ha : ∀ b ∈ s, ∃ c ∈ s, r x c ∧ r b c
y : α
hy : y ∈ s
⊢ ∃ z ∈ insert x s, r x z ∧ r y z

case inr.inl
α : Type u_1
r : α → α → Prop
inst✝ : Std.Refl r
s : Set α
hd : DirectedOn r s
x : α
hx : x ∈ s
y : α
ha : ∀ b ∈ s, ∃ c ∈ s, r y c ∧ r b c
⊢ ∃ z ∈ insert y s, r x z ∧ r y z

case inr.inr
α : Type u_1
r : α → α → Prop
inst✝ : Std.Refl r
a : α
s : Set α
hd : DirectedOn r s
ha : ∀ b ∈ s, ∃ c ∈ s, r a c ∧ r b c
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ ∃ z ∈ insert a s, r x z ∧ r y z