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

Goal state before:
pp: n : Nat
⊢ (bif decide (n % 2 = 1) then 2 * (n / 2) + 1 else 2 * (n / 2)) = n

Tactic:
cases mod_two_eq_zero_or_one n with | _ h => simpa [h] using Nat.div_add_mod n 2

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

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
a b c : M
hba : b * a = 1
hac : a * c = 1
⊢ b = c

Tactic:
by
  rw [← one_mul c, ← hba, mul_assoc, hac, mul_one b]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_3
p : α → Prop
b : Prop
ha : Nonempty α
a : α
⊢ (∀ (x : α), p x) → b ↔ ∃ x, p x → b

Tactic:
refine ⟨fun h ↦ not_forall_not.1 fun h' ↦ ?_, fun ⟨x, hx⟩ h ↦ hx (h x)⟩

Goal state after:
α : Sort u_3
p : α → Prop
b : Prop
ha : Nonempty α
a : α
h : (∀ (x : α), p x) → b
h' : ∀ (x : α), ¬(p x → b)
⊢ False
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Type u
f : α → Type (max u v)
hf : Surjective f
T : Type (max u v) := Sigma f
U : α
hU : f U = Set T
g : Set T → T := fun s ↦ ⟨U, cast ⋯ s⟩
s t : Set T
h : g s = g t
this : cast hU (g s).snd = cast hU (g t).snd
⊢ s = t

Tactic:
by
      simp only [g, cast_cast, cast_eq] at this
      assumption

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

Goal state before:
pp: α : Type u_4
β : Sort u_5
f : α → β
I : Injective f
a : α
b : β
hpi : partialInv f b = if h : ∃ a, f a = b then some (Classical.choose h) else none
h' : ∃ a, f a = b
h : some (Classical.choose h') = some a
⊢ f a = b

Tactic:
injection h with h

Goal state after:
α : Type u_4
β : Sort u_5
f : α → β
I : Injective f
a : α
b : β
hpi : partialInv f b = if h : ∃ a, f a = b then some (Classical.choose h) else none
h' : ∃ a, f a = b
h : Classical.choose h' = a
⊢ f a = b
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
motive : {a b : α} → ReflTransGen r a b → Prop
a b : α
h : ReflTransGen r a b
refl : ∀ (a : α), motive ⋯
single : ∀ {a b : α} (h : r a b), motive ⋯
trans : ∀ {a b c : α} (h₁ : ReflTransGen r a b) (h₂ : ReflTransGen r b c), motive h₁ → motive h₂ → motive ⋯
⊢ motive h

Tactic:
by
  induction h with
  | refl => exact refl a
  | tail hab hbc ih => exact trans hab (.single hbc) ih (single hbc)

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
⊢ TransGen r ≤ ReflTransGen r

Tactic:
by
  intro a _ h
  induction h with
  | single h => exact ReflTransGen.single h
  | tail _ bc ab => exact ReflTransGen.tail ab bc

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.Function.Iterate

Goal state before:
pp: α : Type u
f : α → α
m n : ℕ
a : α
hf : Injective f
⊢ f^[m + n] a = f^[n] a ↔ f^[n] (f^[m] a) = f^[n] a

Tactic:
← iterate_add_apply,

Goal state after:
α : Type u
f : α → α
m n : ℕ
a : α
hf : Injective f
⊢ f^[m + n] a = f^[n] a ↔ f^[n + m] a = f^[n] a
Module: Mathlib.Algebra.Group.Action.Faithful

Goal state before:
pp: M : Type u_4
N : Type u_5
P : Type u_6
Q : Type u_7
inst✝⁹ : SMul M N
inst✝⁸ : SMul M P
inst✝⁷ : SMul M Q
inst✝⁶ : SMul N P
inst✝⁵ : SMul N Q
inst✝⁴ : SMul P Q
inst✝³ : FaithfulSMul P Q
inst✝² : IsScalarTower M N Q
inst✝¹ : IsScalarTower M P Q
inst✝ : IsScalarTower N P Q
m : M
n : N
p : P
⊢ (m • n) • p = m • n • p

Tactic:
← (smul_left_injective' (α := Q)).eq_iff,

Goal state after:
M : Type u_4
N : Type u_5
P : Type u_6
Q : Type u_7
inst✝⁹ : SMul M N
inst✝⁸ : SMul M P
inst✝⁷ : SMul M Q
inst✝⁶ : SMul N P
inst✝⁵ : SMul N Q
inst✝⁴ : SMul P Q
inst✝³ : FaithfulSMul P Q
inst✝² : IsScalarTower M N Q
inst✝¹ : IsScalarTower M P Q
inst✝ : IsScalarTower N P Q
m : M
n : N
p : P
⊢ (fun x2 ↦ ((m • n) • p) • x2) = fun x2 ↦ (m • n • p) • x2
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: M : Type u_9
N : Type u_10
P : Type u_11
Q : Type u_12
inst✝⁹ : SMul M N
inst✝⁸ : SMul M P
inst✝⁷ : SMul M Q
inst✝⁶ : SMul N P
inst✝⁵ : SMul N Q
inst✝⁴ : Monoid P
inst✝³ : MulAction P Q
inst✝² : IsScalarTower M N P
inst✝¹ : IsScalarTower M P Q
inst✝ : IsScalarTower N P Q
m : M
n : N
q : Q
⊢ m • (n • 1) • q = m • n • q

Tactic:
smul_one_smul

Goal state after:
M : Type u_9
N : Type u_10
P : Type u_11
Q : Type u_12
inst✝⁹ : SMul M N
inst✝⁸ : SMul M P
inst✝⁷ : SMul M Q
inst✝⁶ : SMul N P
inst✝⁵ : SMul N Q
inst✝⁴ : Monoid P
inst✝³ : MulAction P Q
inst✝² : IsScalarTower M N P
inst✝¹ : IsScalarTower M P Q
inst✝ : IsScalarTower N P Q
m : M
n : N
q : Q
⊢ m • n • q = m • n • q
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: M : Type u_9
N : Type u_10
P : Type u_11
Q : Type u_12
inst✝⁹ : SMul M N
inst✝⁸ : SMul M P
inst✝⁷ : SMul M Q
inst✝⁶ : SMul P Q
inst✝⁵ : Monoid N
inst✝⁴ : MulAction N P
inst✝³ : MulAction N Q
inst✝² : IsScalarTower M N P
inst✝¹ : IsScalarTower M N Q
inst✝ : IsScalarTower N P Q
m : M
p : P
q : Q
⊢ (m • 1) • p • q = m • p • q

Tactic:
smul_one_smul

Goal state after:
M : Type u_9
N : Type u_10
P : Type u_11
Q : Type u_12
inst✝⁹ : SMul M N
inst✝⁸ : SMul M P
inst✝⁷ : SMul M Q
inst✝⁶ : SMul P Q
inst✝⁵ : Monoid N
inst✝⁴ : MulAction N P
inst✝³ : MulAction N Q
inst✝² : IsScalarTower M N P
inst✝¹ : IsScalarTower M N Q
inst✝ : IsScalarTower N P Q
m : M
p : P
q : Q
⊢ m • p • q = m • p • q
Module: Mathlib.Algebra.Group.Pi.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : One γ
f : α → β
x✝ : β
⊢ extend f 1 1 x✝ = 1 x✝

Tactic:
by apply ite_self

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Inv γ
f : α → β
g : α → γ
e : β → γ
⊢ extend f g⁻¹ e⁻¹ = (extend f g e)⁻¹

Tactic:
by
  classical
  funext x
  simp [Function.extend_def, apply_dite Inv.inv]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
x y : α × β
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Trichotomous s
⊢ ∀ {a b : α × β}, Prod.Lex r s a b ∨ a = b ∨ Prod.Lex r s b a

Tactic:
by
    intro ⟨i, a⟩ ⟨j, b⟩
    obtain hij | rfl | hji := trichotomous_of r i j
    { exact Or.inl (Lex.left _ _ hij) }
    { exact (trichotomous_of (s) a b).imp3 (Lex.right _) (congr_arg _) (Lex.right _) }
    { exact Or.inr (Or.inr <| Lex.left _ _ hji) }

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ min a (min b c) = min b (min a c)

Tactic:
← min_assoc,

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ min (min a b) c = min b (min a c)
Module: Mathlib.Data.Nat.Init

Goal state before:
pp: a b c d e m n k : ℕ
p : ℕ → Prop
P : ℕ → Sort u_1
h : (k : ℕ) → k < n → m ≤ k → P (k + 1) → P k
mn : m ≤ n
hP : P n
⊢ P m

Tactic:
by
  induction mn using decreasingInduction with
  | self => exact hP
  | of_succ k hk ih =>
    exact h _ (lt_of_succ_le hk) (Nat.le_refl _)
      (ih fun k' hk' h'' => h k' hk' <| le_of_succ_le h'')

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : BoundedOrder α
x : α
h : IsCompl x ⊥
⊢ x = ⊤

Tactic:
← sup_bot_eq x,

Goal state after:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : BoundedOrder α
x : α
h : IsCompl x ⊥
⊢ x ⊔ ⊥ = ⊤
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
inst✝² : SemilatticeSup α
inst✝¹ : DecidableLE α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
x y : α
⊢ x ⊔ y = maxDefault x y

Tactic:
unfold maxDefault

Goal state after:
α : Type u
inst✝² : SemilatticeSup α
inst✝¹ : DecidableLE α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
x y : α
⊢ x ⊔ y = if x ≤ y then y else x
Module: Mathlib.Order.Heyting.Basic

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

Tactic:
← top_le_iff,

Goal state after:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b : α
⊢ ⊤ ≤ a ⇨ b ↔ a ≤ b
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c : α
⊢ a \ c ≤ a \ b ⊔ b \ c

Tactic:
rw [sdiff_le_iff, sup_left_comm, ← sdiff_le_iff]

Goal state after:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c : α
⊢ a \ (a \ b) ≤ c ⊔ b \ c
Module: Mathlib.Logic.Equiv.Option

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
e : Option α ≃ Option β
x : α
h : ¬(e (some x)).isSome = true
⊢ (e none).isSome = true

Tactic:
← Option.ne_none_iff_isSome

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
e : Option α ≃ Option β
x : α
h : ¬(e (some x)).isSome = true
⊢ e none ≠ none
Module: Mathlib.Order.BooleanAlgebra.Set

Goal state before:
pp: α : Type u_1
t s s' : Set α
⊢ s ∩ tᶜ ∪ s' \ tᶜ = s' ∩ t ∪ s \ t

Tactic:
sdiff_compl,

Goal state after:
α : Type u_1
t s s' : Set α
⊢ s ∩ tᶜ ∪ s' ∩ t = s' ∩ t ∪ s \ t
Module: Mathlib.Data.Sigma.Basic

Goal state before:
pp: α : Type u_1
β : α → Type u_4
γ : (a : α) → β a → Type u_7
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
i : (a : α) × β a
f : (i : (a : α) × β a) → γ i.fst i.snd
x : γ i.fst i.snd
⊢ curry (update f i x) = update (curry f) i.fst (update (curry f i.fst) i.snd x)

Tactic:
obtain ⟨ia, ib⟩ := i

Goal state after:
α : Type u_1
β : α → Type u_4
γ : (a : α) → β a → Type u_7
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
f : (i : (a : α) × β a) → γ i.fst i.snd
ia : α
ib : β ia
x : γ ⟨ia, ib⟩.fst ⟨ia, ib⟩.snd
⊢ curry (update f ⟨ia, ib⟩ x) = update (curry f) ⟨ia, ib⟩.fst (update (curry f ⟨ia, ib⟩.fst) ⟨ia, ib⟩.snd x)
Module: Mathlib.Data.Sigma.Basic

Goal state before:
pp: α : Type u_1
β : α → Type u_4
γ : (a : α) → β a → Type u_7
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
f : (i : (a : α) × β a) → γ i.fst i.snd
ia : α
ib : β ia
x : γ ⟨ia, ib⟩.fst ⟨ia, ib⟩.snd
ja : α
jb : β ja
⊢ curry (update f ⟨ia, ib⟩ x) ja jb = update (curry f) ⟨ia, ib⟩.fst (update (curry f ⟨ia, ib⟩.fst) ⟨ia, ib⟩.snd x) ja jb

Tactic:
unfold Sigma.curry

Goal state after:
α : Type u_1
β : α → Type u_4
γ : (a : α) → β a → Type u_7
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
f : (i : (a : α) × β a) → γ i.fst i.snd
ia : α
ib : β ia
x : γ ⟨ia, ib⟩.fst ⟨ia, ib⟩.snd
ja : α
jb : β ja
⊢ update f ⟨ia, ib⟩ x ⟨ja, jb⟩ =
    update (fun x y ↦ f ⟨x, y⟩) ⟨ia, ib⟩.fst (update (fun y ↦ f ⟨⟨ia, ib⟩.fst, y⟩) ⟨ia, ib⟩.snd x) ja jb
Module: Mathlib.Order.BooleanAlgebra.Basic

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

Tactic:
sdiff_sdiff_right',

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

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

Tactic:
sdiff_compl,

Goal state after:
α : Type u
x y : α
inst✝ : BooleanAlgebra α
⊢ xᶜ ⊓ y = y \ x
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b : α
⊢ b ≤ a ∆ b ↔ Disjoint a b

Tactic:
by
  rw [symmDiff_comm, le_symmDiff_iff_left, disjoint_comm]

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

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

Tactic:
image_sdiff hf

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
p : Set β → Prop
⊢ (∃ s, s ⊆ range f ∧ p s) ↔ ∃ s, p (f '' s)

Tactic:
← exists_range_iff,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
p : Set β → Prop
⊢ (∃ s, s ⊆ range f ∧ p s) ↔ ∃ a, a ∈ range (image f) ∧ p a
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : β → α
g : γ → α
s : Set β
t : Set γ
h : ∀ (b : β), b ∈ s → ∀ (c : γ), c ∈ t → f b ≠ g c
⊢ f '' s ⊓ g '' t ⊆ ⊥

Tactic:
rintro a ⟨⟨b, hb, eq⟩, c, hc, rfl⟩; exact h b hb c hc eq

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set β
h : f ⁻¹' s = ∅
⊢ Disjoint s (range f)

Tactic:
simp only [eq_empty_iff_forall_notMem, mem_preimage] at h ⊢
    grind

Goal state after:
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:
by
  intro y hy
  rcases h₁ hy.1 with ⟨x₁, hx₁, rfl⟩
  rcases h₂ hy.2 with ⟨x₂, hx₂, heq⟩
  obtain rfl : x₁ = x₂ := h (Or.inl hx₁) (Or.inr hx₂) heq.symm
  exact mem_image_of_mem f ⟨hx₁, hx₂⟩

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

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
f : α → β
g : β → α
s : Set α
hgf : LeftInvOn g f s
ginj : InjOn g (g ⁻¹' s)
y : α
hy : y ∈ s
⊢ f y ∈ g ⁻¹' s

Tactic:
rw [mem_preimage, hgf hy]

Goal state after:
case mp
α : Type u_1
β : Type u_2
f : α → β
g : β → α
s : Set α
hgf : LeftInvOn g f s
ginj : InjOn g (g ⁻¹' s)
y : α
hy : y ∈ s
⊢ y ∈ s
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
r : Set α
hinj : InjOn f r
hrs : r ⊆ s
⊢ ∃ u, r ⊆ u ∧ u ⊆ s ∧ f '' u = f '' s ∧ InjOn f u

Tactic:
obtain ⟨u, hru, hus, h⟩ := hinj.bijOn_image.exists_extend_of_subset hrs
    (image_mono hrs) Subset.rfl

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
r : Set α
hinj : InjOn f r
hrs : r ⊆ s
u : Set α
hru : r ⊆ u
hus : u ⊆ s
h : BijOn f u (f '' s)
⊢ ∃ u, r ⊆ u ∧ u ⊆ s ∧ f '' u = f '' s ∧ InjOn f u
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 % n + n * (m / n)) = x ^ (m % n)

Tactic:
by simp [zpow_add, zpow_mul, h]

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

Goal state before:
pp: G : Type u_3
inst✝ : CommGroup G
a b c : G
⊢ a / b * (c / a) = c / b

Tactic:
rw [mul_comm]; apply div_mul_div_cancel

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

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

Tactic:
val_inj

Goal state after:
α : Type u
inst✝ : Monoid α
a : αˣ
⊢ a = 1 ↔ a = 1
Module: Mathlib.Algebra.GroupWithZero.Defs

Goal state before:
pp: M₀ : Type u_1
inst✝¹ : MulZeroClass M₀
inst✝ : IsRightCancelMulZero M₀
a b c : M₀
⊢ a * c = b * c ↔ a = b ∨ c = 0

Tactic:
by_cases hc : c = 0 <;> [simp only [hc, mul_zero, or_true]; simp [mul_left_inj', hc]]

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

Goal state before:
pp: R : Type u_5
inst✝¹ : Zero R
inst✝ : Pow R ℕ
h : ¬IsReduced R
⊢ ∃ x, x ≠ 0 ∧ IsNilpotent x

Tactic:
by
  simpa [isReduced_iff, not_forall, and_comm] using h

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

Goal state before:
pp: case inr
α : Type u_3
inst✝ : MonoidWithZero α
h : ∀ (a : α), a ≠ 0 → ∃ b, b * a = 1
a : α
ha : a ≠ 0
h✝ : Nontrivial α
⊢ ∃ b, a * b = 1

Tactic:
obtain ⟨b, hb⟩ := h a ha

Goal state after:
case inr
α : Type u_3
inst✝ : MonoidWithZero α
h : ∀ (a : α), a ≠ 0 → ∃ b, b * a = 1
a : α
ha : a ≠ 0
h✝ : Nontrivial α
b : α
hb : b * a = 1
⊢ ∃ b, a * b = 1
Module: Mathlib.Algebra.GroupWithZero.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β✝ : Type u_3
γ : Type u_4
δ : Type u_5
M₀ : Type u_6
inst✝⁵ : MulZeroOneClass α
inst✝⁴ : MulZeroOneClass β✝
inst✝³ : MulZeroOneClass γ
inst✝² : MulZeroOneClass δ
inst✝¹ : FunLike F α β✝
β : Type ?u.21
inst✝ : CommMonoidWithZero β
f g : α →*₀ β
⊢ f 0 * g 0 = 0

Tactic:
rw [map_zero, zero_mul]

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

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

Tactic:
induction n using Nat.strongRecOn with | ind k hk => ?_
  cases k with
  | zero => rw [Nat.binCast, Nat.cast_zero]
  | succ k =>
      rw [Nat.binCast]
      by_cases h : (k + 1) % 2 = 0
      · conv => rhs; rw [← Nat.mod_add_div (k + 1) 2]
        rw [if_pos h, hk _ <| Nat.div_lt_self (Nat.succ_pos k) (Nat.le_refl 2), ← Nat.cast_add]
        rw [h, Nat.zero_add, Nat.succ_mul, Nat.one_mul]
      · conv => rhs; rw [← Nat.mod_add_div (k + 1) 2]
        rw [if_neg h, hk _ <| Nat.div_lt_self (Nat.succ_pos k) (Nat.le_refl 2), ← Nat.cast_add]
        have h1 := Or.resolve_left (Nat.mod_two_eq_zero_or_one (succ k)) h
        rw [h1, Nat.add_comm 1, Nat.succ_mul, Nat.one_mul]
        simp only [Nat.cast_add, Nat.cast_one]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : AddMonoid R
inst✝ : One R
n : ℕ
this : AddMonoidWithOne R := AddMonoidWithOne.unary
⊢ (n + 1).binCast = n.binCast + 1

Tactic:
Nat.binCast_eq,

Goal state after:
R : Type u_1
inst✝¹ : AddMonoid R
inst✝ : One R
n : ℕ
this : AddMonoidWithOne R := AddMonoidWithOne.unary
⊢ ↑(n + 1) = n.binCast + 1
Module: Mathlib.Data.Nat.Cast.Defs

Goal state before:
pp: R : Type u_1
inst✝¹ : AddMonoid R
inst✝ : One R
n : ℕ
this : AddMonoidWithOne R := AddMonoidWithOne.unary
⊢ ↑(n + 1) = n.binCast + 1

Tactic:
Nat.binCast_eq,

Goal state after:
R : Type u_1
inst✝¹ : AddMonoid R
inst✝ : One R
n : ℕ
this : AddMonoidWithOne R := AddMonoidWithOne.unary
⊢ ↑(n + 1) = ↑n + 1
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 : Surjective ⇑f
smul : ∀ (a : M₀) (b : A), f (a • b) = a • f b
c : M₀
⊢ c • 0 = 0

Tactic:
← f.map_zero,

Goal state after:
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 : Surjective ⇑f
smul : ∀ (a : M₀) (b : A), f (a • b) = a • f b
c : M₀
⊢ c • f 0 = f 0
Module: Mathlib.Algebra.Module.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
r s : R
x✝ : M
inst✝¹ : AddCommMonoid M₂
inst✝ : SMul R M₂
f : M →+ M₂
hf : Surjective ⇑f
smul : ∀ (c : R) (x : M), f (c • x) = c • f x
x : M
⊢ 0 • f x = 0

Tactic:
← f.map_zero,

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
r s : R
x✝ : M
inst✝¹ : AddCommMonoid M₂
inst✝ : SMul R M₂
f : M →+ M₂
hf : Surjective ⇑f
smul : ∀ (c : R) (x : M), f (c • x) = c • f x
x : M
⊢ 0 • f x = f 0
Module: Mathlib.Algebra.Ring.Defs

Goal state before:
pp: case zero
α : Type u
inst✝ : NonAssocSemiring α
a : α
⊢ 0 • a = ↑0 * a

Tactic:
zero_nsmul,

Goal state after:
case zero
α : Type u
inst✝ : NonAssocSemiring α
a : α
⊢ 0 = ↑0 * a
Module: Mathlib.Algebra.Ring.Defs

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

Tactic:
by
  simp only [sq, add_mul_self_eq]

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

Goal state before:
pp: R : Type u_3
inst✝ : NonUnitalNonAssocRing R
r : R
h : IsLeftRegular r
r' : R
eq : r * r' = 0
⊢ (fun x ↦ r * x) r' = (fun x ↦ r * x) 0

Tactic:
by simp_rw [eq, mul_zero]

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

Goal state before:
pp: case zero
α : Type u_1
inst✝ : NonAssocSemiring α
a : α
⊢ 0 • a = a * ↑0

Tactic:
zero_nsmul,

Goal state after:
case zero
α : Type u_1
inst✝ : NonAssocSemiring α
a : α
⊢ 0 = a * ↑0
Module: Mathlib.Algebra.Ring.Basic

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

Tactic:
rw [one_div_mul_one_div_rev]

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
n : ℕ
a✝ b✝ : M
u✝ u₁ u₂ u : Mˣ
a b : M
hu : a * b = ↑u
hc : Commute a b
⊢ b * ↑u⁻¹ * a = 1

Tactic:
by
    have : Commute a u := hu ▸ (Commute.refl _).mul_right hc
    rw [← this.units_inv_right.right_comm, ← hc.eq, hu, u.mul_inv]

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

Goal state before:
pp: case inr.inl
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
a b : M₀
h : IsUnit a ∨ IsUnit b
ha : ¬IsUnit a
hb : IsUnit b
⊢ (a * b)⁻¹ʳ = b⁻¹ʳ * a⁻¹ʳ

Tactic:
have : ¬ IsUnit (a * b) := by simpa [hb.mul_right_iff]

Goal state after:
case inr.inl
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
a b : M₀
h : IsUnit a ∨ IsUnit b
ha : ¬IsUnit a
hb : IsUnit b
this : ¬IsUnit (a * b)
⊢ (a * b)⁻¹ʳ = b⁻¹ʳ * a⁻¹ʳ
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

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

Tactic:
by
  rw [pow_sub₀ _ (inv_ne_zero ha) h, inv_pow, inv_pow, inv_inv]

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

Goal state before:
pp: α : Type u
inst✝¹ : Monoid α
inst✝ : HasDistribNeg α
a : αˣ
⊢ ↑a = ↑(-1) ↔ a = -1

Tactic:
val_inj

Goal state after:
α : Type u
inst✝¹ : Monoid α
inst✝ : HasDistribNeg α
a : αˣ
⊢ a = -1 ↔ a = -1
Module: Mathlib.Algebra.Ring.Commute

Goal state before:
pp: R : Type u
inst✝¹ : Monoid R
inst✝ : HasDistribNeg R
a : R
⊢ (-a) ^ 2 = a ^ 2

Tactic:
by simp [sq]

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
u : Rˣ
⊢ u⁻¹ = u ↔ u = 1 ∨ u = -1

Tactic:
by
  rw [inv_eq_iff_mul_eq_one]
  simp only [Units.ext_iff]
  push_cast
  exact mul_self_eq_one_iff

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
a : M
⊢ -1 • a + a = 0

Tactic:
nth_rw 2 [← one_smul R a]
      rw [← add_smul, neg_add_cancel, zero_smul]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
f : R → S
hf : Surjective f
inst✝¹² : Add S
inst✝¹¹ : Mul S
inst✝¹⁰ : Zero S
inst✝⁹ : One S
inst✝⁸ : Neg S
inst✝⁷ : Sub S
inst✝⁶ : SMul ℕ S
inst✝⁵ : SMul ℤ S
inst✝⁴ : Pow S ℕ
inst✝³ : NatCast S
inst✝² : IntCast S
inst✝¹ : Mul R
inst✝ : HasDistribNeg R
neg : ∀ (a : R), f (-a) = -f a
mul : ∀ (a b : R), f (a * b) = f a * f b
x y : R
⊢ -f x * f y = -(f x * f y)

Tactic:
← neg,

Goal state after:
R : Type u_1
S : Type u_2
f : R → S
hf : Surjective f
inst✝¹² : Add S
inst✝¹¹ : Mul S
inst✝¹⁰ : Zero S
inst✝⁹ : One S
inst✝⁸ : Neg S
inst✝⁷ : Sub S
inst✝⁶ : SMul ℕ S
inst✝⁵ : SMul ℤ S
inst✝⁴ : Pow S ℕ
inst✝³ : NatCast S
inst✝² : IntCast S
inst✝¹ : Mul R
inst✝ : HasDistribNeg R
neg : ∀ (a : R), f (-a) = -f a
mul : ∀ (a b : R), f (a * b) = f a * f b
x y : R
⊢ f (-x) * f y = -(f x * f y)
Module: Mathlib.Algebra.Ring.InjSurj

Goal state before:
pp: R : Type u_1
S : Type u_2
f : R → S
hf : Surjective f
inst✝¹² : Add S
inst✝¹¹ : Mul S
inst✝¹⁰ : Zero S
inst✝⁹ : One S
inst✝⁸ : Neg S
inst✝⁷ : Sub S
inst✝⁶ : SMul ℕ S
inst✝⁵ : SMul ℤ S
inst✝⁴ : Pow S ℕ
inst✝³ : NatCast S
inst✝² : IntCast S
inst✝¹ : Mul R
inst✝ : HasDistribNeg R
neg : ∀ (a : R), f (-a) = -f a
mul : ∀ (a b : R), f (a * b) = f a * f b
x y : R
⊢ f x * -f y = -(f x * f y)

Tactic:
← neg,

Goal state after:
R : Type u_1
S : Type u_2
f : R → S
hf : Surjective f
inst✝¹² : Add S
inst✝¹¹ : Mul S
inst✝¹⁰ : Zero S
inst✝⁹ : One S
inst✝⁸ : Neg S
inst✝⁷ : Sub S
inst✝⁶ : SMul ℕ S
inst✝⁵ : SMul ℤ S
inst✝⁴ : Pow S ℕ
inst✝³ : NatCast S
inst✝² : IntCast S
inst✝¹ : Mul R
inst✝ : HasDistribNeg R
neg : ∀ (a : R), f (-a) = -f a
mul : ∀ (a b : R), f (a * b) = f a * f b
x y : R
⊢ f x * f (-y) = -(f x * f y)
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:

Tactic:
_ = d * b := by rw [add_left_comm, ← add_mul, ← hcd, zero_mul, add_zero]
    _ < d * a := mul_lt_mul_of_pos_left h <| hcd.trans_lt <| add_lt_of_neg_left _ hc
    _ = _ := by rw [← add_assoc, ← add_mul, ← hcd, zero_mul, zero_add]

Goal state after: