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

Goal state before:
pp: n : Nat
n0 : ¬n = 0
⊢ (if n >>> 1 = 0 then 0 else (n >>> 1).log2.succ) < if n = 0 then 0 else n.log2.succ

Tactic:
decreasing_by
  obtain _ | n := n; · exact (n0 rfl).elim
  obtain _ | n := n; · simp
  have : (n + 1 + 1) >>> 1 ≠ 0 := Nat.div_ne_zero_iff.mpr ⟨by decide, le_add_left ..⟩
  simpa only [if_neg n0, if_neg this, log2_eq_succ_log2_shiftRight this] using lt_succ_self _

Goal state after:
Module: Mathlib.Logic.Unique

Goal state before:
pp: α : Sort u
inst✝¹ : Subsingleton α
inst✝ : Nonempty α
inhabited_h : Inhabited α
⊢ Nonempty (Unique α)

Tactic:
exact ⟨Unique.mk' α⟩

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a b : α
h : ReflTransGen r a b
⊢ a = b ∨ ∃ c, r a c ∧ ReflTransGen r c b

Tactic:
induction h using Relation.ReflTransGen.head_induction_on <;> grind

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

Goal state before:
pp: α : Type u_5
β : Type u_6
a : α
⊢ Function.Injective (mk a)

Tactic:
intro b₁ b₂ h
  simpa only [true_and, Prod.mk_inj, eq_self_iff_true] using h

Goal state after:
Module: Mathlib.Order.OrderDual

Goal state before:
pp: α : Type u_1
inst✝ : LT α
T : Std.Trichotomous LT.lt
a b : αᵒᵈ
⊢ ¬a < b → ¬b < a → a = b

Tactic:
eq_comm

Goal state after:
α : Type u_1
inst✝ : LT α
T : Std.Trichotomous LT.lt
a b : αᵒᵈ
⊢ ¬a < b → ¬b < a → b = a
Module: Mathlib.Order.Lattice

Goal state before:
pp: α✝ : Type u
β : Type v
α : Type u_1
inst✝ : Max α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
sup_idem : ∀ (a : α), a ⊔ a = a
a b c : α
hac : a ⊔ c = c
hbc : b ⊔ c = c
⊢ a ⊔ b ⊔ c = c

Tactic:
by rwa [sup_assoc, hbc]

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

Goal state before:
pp: case mp
α : Type u_1
l : List α
H : l.Nodup
a : α
⊢ (∃ n, n > 0 ∧ l = List.replicate n a) → l = [a]

Tactic:
rintro ⟨n, hn, rfl⟩

Goal state after:
case mp
α : Type u_1
a : α
n : ℕ
hn : n > 0
H : (List.replicate n a).Nodup
⊢ List.replicate n a = [a]
Module: Mathlib.Data.Set.Subsingleton

Goal state before:
pp: case refine_1
α : Type u
s : Set α
⊢ (∃ a, s = {a}) → s.Nonempty ∧ s.Subsingleton

Tactic:
rintro ⟨a, rfl⟩

Goal state after:
case refine_1
α : Type u
a : α
⊢ {a}.Nonempty ∧ {a}.Subsingleton
Module: Mathlib.Order.GaloisConnection.Defs

Goal state before:
pp: case mpr
α : Type u
β : Type v
inst✝¹ : PartialOrder α
inst✝ : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
z : α
y : β
⊢ (∀ (x : α), x ≤ z ↔ l x ≤ y) → u y = z

Tactic:
intro H

Goal state after:
case mpr
α : Type u
β : Type v
inst✝¹ : PartialOrder α
inst✝ : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
z : α
y : β
H : ∀ (x : α), x ≤ z ↔ l x ≤ y
⊢ u y = z
Module: Mathlib.Order.Heyting.Basic

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

Tactic:
by
  rw [himp_inf_distrib, himp_self, inf_top_eq, h.himp_eq_right]

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedHeytingAlgebra α
a✝ b✝ c✝ d a b c : α
⊢ a ⊓ (b ⊔ c) ≤ a ⊓ b ⊔ a ⊓ c

Tactic:
inf_comm a,

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedHeytingAlgebra α
a✝ b✝ c✝ d a b c : α
⊢ (b ⊔ c) ⊓ a ≤ b ⊓ a ⊔ c ⊓ a
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x : α
inst✝ : BooleanAlgebra α
⊢ xᶜ ⊔ x = ⊤

Tactic:
by rw [sup_comm, sup_compl_eq_top]

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

Goal state before:
pp: α : Type u
β : Type u_1
x y z : α
inst✝⁶ : Max α
inst✝⁵ : Min α
inst✝⁴ : LE α
inst✝³ : LT α
inst✝² : Bot α
inst✝¹ : SDiff α
inst✝ : GeneralizedBooleanAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_bot : f ⊥ = ⊥
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
a b : α
⊢ f (a ⊓ b ⊓ a \ b) = f ⊥

Tactic:
by rw [map_inf, map_sdiff, map_inf, inf_inf_sdiff, map_bot]

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

Goal state before:
pp: α : Type u
β : Type u_1
x y z : α
inst✝⁹ : Max α
inst✝⁸ : Min α
inst✝⁷ : LE α
inst✝⁶ : LT α
inst✝⁵ : Top α
inst✝⁴ : Bot α
inst✝³ : Compl α
inst✝² : SDiff α
inst✝¹ : HImp α
inst✝ : BooleanAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
map_compl : ∀ (a : α), f aᶜ = (f a)ᶜ
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
a : α
⊢ f a ⊓ f aᶜ = f ⊥

Tactic:
rw [map_compl, inf_compl_eq_bot, map_bot]

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

Goal state before:
pp: α : Sort u_1
inst✝ : DecidableEq α
a : α
⊢ Injective fun x ↦ swap x a

Tactic:
by
  simp_rw [swap_comm _ a]
  exact swap_injective_of_left a

Goal state after:
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
β : Type u_10
γ : Type u_11
f : α ⊕ β → γ
⊢ (fun p ↦ Sum.elim p.fst p.snd) ((fun f ↦ (f ∘ inl, f ∘ inr)) f) = f

Tactic:
by ext ⟨⟩ <;> rfl

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

Goal state before:
pp: α : Type u_1
inst✝ : BooleanAlgebra α
s : Set α
⊢ compl '' compl '' s = s

Tactic:
by
  rw [← image_comp, compl_comp_compl, image_id]

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

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

Tactic:
intro H

Goal state after:
case inr.refine_3
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
st : s.Nonempty ∧ t.Nonempty
H : s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅
⊢ s ×ˢ t ⊆ s₁ ×ˢ t₁
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
ι : Sort u_4
f : ι → α
inst✝ : Nonempty ι
y : α
h : ∀ (x : ι), f x = y
x✝ : α
⊢ y = x✝ ↔ x✝ = y

Tactic:
eq_comm

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
t : Set β
x : α
⊢ x ∈ s.piecewise f g ⁻¹' t ↔ x ∈ s.ite (f ⁻¹' t) (g ⁻¹' t)

Tactic:
by_cases x ∈ s

Goal state after:
case pos
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
t : Set β
x : α
h✝ : x ∈ s
⊢ x ∈ s.piecewise f g ⁻¹' t ↔ x ∈ s.ite (f ⁻¹' t) (g ⁻¹' t)

case neg
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
t : Set β
x : α
h✝ : ¬x ∈ s
⊢ x ∈ s.piecewise f g ⁻¹' t ↔ x ∈ s.ite (f ⁻¹' t) (g ⁻¹' t)
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
⊢ diagonal α = univ ↔ Subsingleton α

Tactic:
by
  simp only [subsingleton_iff, eq_univ_iff_forall, Prod.forall, mem_diagonal_iff]

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

Goal state before:
pp: ι : Type u_1
M : Type u_2
α : ι → Type u_4
inst✝² : (i : ι) → SMul M (α i)
inst✝¹ : ∀ (i : ι), Nonempty (α i)
i : ι
inst✝ : FaithfulSMul M (α i)
m₁✝ m₂✝ : M
h : ∀ (a : (i : ι) → α i), m₁✝ • a = m₂✝ • a
a : α i
⊢ m₁✝ • a = m₂✝ • a

Tactic:
by
    classical
    simpa using
      congr_fun (h <| Function.update (fun j => Classical.choice (‹∀ i, Nonempty (α i)› j)) i a) i

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

Goal state before:
pp: case mpr
X : Type u_1
Y : Sort u_2
f : X → Y
s : Set X
x : Pullback f f
⊢ x ∈ pullbackDiagonal f ∩ Subtype.val ⁻¹' s ×ˢ s → x ∈ toPullbackDiag f '' s

Tactic:
obtain ⟨⟨x, y⟩, h⟩ := x
    rintro ⟨rfl : x = y, h2x⟩
    exact mem_image_of_mem _ h2x.1

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set (α × β)
h : InjOn Prod.fst s
f : α → β
hf : ∀ (x : α), x ∈ Prod.fst '' s → (x, f x) ∈ s
⊢ ∃ f, s = graphOn f (Prod.fst '' s)

Tactic:
forall_mem_image

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set (α × β)
h : InjOn Prod.fst s
f : α → β
hf : ∀ ⦃x : α × β⦄, x ∈ s → (x.1, f x.1) ∈ s
⊢ ∃ f, s = graphOn f (Prod.fst '' s)
Module: Mathlib.Algebra.Group.Hom.Defs

Goal state before:
pp: G : Type u_7
H : Type u_8
F : Type u_9
inst✝³ : FunLike F G H
inst✝² : DivInvMonoid G
inst✝¹ : DivInvMonoid H
inst✝ : MonoidHomClass F G H
f : F
hf : ∀ (x : G), f x⁻¹ = (f x)⁻¹
a : G
n : ℕ
⊢ f (a ^ n) = f a ^ ↑n

Tactic:
map_pow,

Goal state after:
G : Type u_7
H : Type u_8
F : Type u_9
inst✝³ : FunLike F G H
inst✝² : DivInvMonoid G
inst✝¹ : DivInvMonoid H
inst✝ : MonoidHomClass F G H
f : F
hf : ∀ (x : G), f x⁻¹ = (f x)⁻¹
a : G
n : ℕ
⊢ f a ^ n = f a ^ ↑n
Module: Mathlib.Algebra.Group.Hom.Defs

Goal state before:
pp: G : Type u_7
H : Type u_8
F : Type u_9
inst✝³ : FunLike F G H
inst✝² : DivInvMonoid G
inst✝¹ : DivInvMonoid H
inst✝ : MonoidHomClass F G H
f : F
hf : ∀ (x : G), f x⁻¹ = (f x)⁻¹
a : G
n : ℕ
⊢ (f (a ^ (n + 1)))⁻¹ = f a ^ Int.negSucc n

Tactic:
map_pow,

Goal state after:
G : Type u_7
H : Type u_8
F : Type u_9
inst✝³ : FunLike F G H
inst✝² : DivInvMonoid G
inst✝¹ : DivInvMonoid H
inst✝ : MonoidHomClass F G H
f : F
hf : ∀ (x : G), f x⁻¹ = (f x)⁻¹
a : G
n : ℕ
⊢ (f a ^ (n + 1))⁻¹ = f a ^ Int.negSucc n
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a b : G
⊢ a⁻¹ = b ↔ b = a⁻¹

Tactic:
eq_comm

Goal state after:
G : Type u_3
inst✝ : Group G
a b : G
⊢ b = a⁻¹ ↔ b = a⁻¹
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a b : G
⊢ a = b⁻¹ ↔ b⁻¹ = a

Tactic:
eq_comm

Goal state after:
G : Type u_3
inst✝ : Group G
a b : G
⊢ b⁻¹ = a ↔ b⁻¹ = a
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: G : Type u_3
inst✝ : Group G
b : G
⊢ Injective fun a ↦ b * a⁻¹

Tactic:
exact fun a a' h ↦ inv_injective (mul_right_injective b h)

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

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

Tactic:
by
  rw [pow_sub a⁻¹ h, inv_pow, inv_pow, inv_inv]

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

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

Tactic:
by
  rw [div_eq_iff_eq_mul, div_mul_eq_mul_div, div_eq_iff_eq_mul', mul_div_assoc]

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

Goal state before:
pp: A : Type u_1
M : Type u_2
G : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
p : α → Prop
f✝ f : Perm α
h : ∀ (x : α), p (f x) ↔ p x
x : { x // p x }
⊢ p (f (f⁻¹ ↑x))

Tactic:
by simpa using x.2

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

Goal state before:
pp: α : Type u_4
p : α → Prop
f : Perm α
⊢ (∀ (x : α), p (f (f⁻¹ x)) ↔ p (f⁻¹ x)) ↔ ∀ (x : α), p (f⁻¹ x) ↔ p x

Tactic:
by simp [Iff.comm]

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

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

Tactic:
add_succ,

Goal state after:
case succ
R : Type u_1
inst✝ : AddMonoidWithOne R
m n : ℕ
ih : ↑(m + n) = ↑m + ↑n
⊢ ↑(m + n).succ = ↑m + ↑(n + 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 α β
hnp : β →*₀ γ
hmn : α →*₀ β
⊢ (⇑hnp ∘ ⇑hmn) 0 = 0

Tactic:
by rw [comp_apply, map_zero, map_zero]

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

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoidWithOne R
⊢ ↑1 + ↑1 + ↑1 = 3

Tactic:
← Nat.cast_add,

Goal state after:
R : Type u_1
inst✝ : AddMonoidWithOne R
⊢ ↑(1 + 1) + ↑1 = 3
Module: Mathlib.Data.Nat.Cast.Defs

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoidWithOne R
⊢ ↑1 + ↑1 + ↑1 + ↑1 = 4

Tactic:
← Nat.cast_add,

Goal state after:
R : Type u_1
inst✝ : AddMonoidWithOne R
⊢ ↑(1 + 1) + ↑1 + ↑1 = 4
Module: Mathlib.Data.Nat.Cast.Defs

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoidWithOne R
⊢ ↑(1 + 1) + ↑1 + ↑1 = 4

Tactic:
← Nat.cast_add,

Goal state after:
R : Type u_1
inst✝ : AddMonoidWithOne R
⊢ ↑(1 + 1 + 1) + ↑1 = 4
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
⊢ a * a / a = a

Tactic:
rw [div_eq_mul_inv, mul_self_mul_inv a]

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

Goal state before:
pp: case pos
G₀ : Type u_2
inst✝ : GroupWithZero G₀
m n : ℤ
hm : ¬m = 0
hn : ¬n = 0
h : ¬m + n = 0
⊢ 0 ^ (m + n) = 0 ^ m * 0 ^ n

Tactic:
zero_zpow _ h,

Goal state after:
case pos
G₀ : Type u_2
inst✝ : GroupWithZero G₀
m n : ℤ
hm : ¬m = 0
hn : ¬n = 0
h : ¬m + n = 0
⊢ 0 = 0 ^ m * 0 ^ n
Module: Mathlib.Data.Int.Cast.Basic

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

Tactic:
← Nat.cast_add,

Goal state after:
R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
⊢ ↑(m + 1 + n) = ↑n + ↑m.succ
Module: Mathlib.Data.Int.Cast.Basic

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

Tactic:
← Nat.cast_add,

Goal state after:
R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
⊢ ↑(m + 1 + n) = ↑(n + m.succ)
Module: Mathlib.Data.Int.Cast.Basic

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

Tactic:
← Nat.cast_add,

Goal state after:
R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
⊢ -↑(m + n + 1 + 1) = -↑(n + 1 + (m + 1))
Module: Mathlib.Algebra.Group.Nat.Even

Goal state before:
pp: m✝ n m : ℕ
⊢ (∃ r, m = r * r) ↔ ∃ n, n * n = m

Tactic:
eq_comm

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

Goal state before:
pp: m✝ n m : ℤ
⊢ (∃ r, m = r * r) ↔ ∃ n, n * n = m

Tactic:
eq_comm

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

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
hab : a ∣ b
n : ℕ
x✝ : n + 1 ≠ 0
⊢ a ∣ b ^ (n + 1)

Tactic:
by rw [pow_succ']; exact hab.mul_right _

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

Goal state before:
pp: α : Type u_2
β : Type u_3
x✝¹ : NonAssocSemiring α
x✝ : NonAssocSemiring β
f : α →+* β
⊢ 0 = 1 ↔ 1 = 0

Tactic:
eq_comm

Goal state after:
α : Type u_2
β : Type u_3
x✝¹ : NonAssocSemiring α
x✝ : NonAssocSemiring β
f : α →+* β
⊢ 1 = 0 ↔ 1 = 0
Module: Mathlib.Algebra.Ring.Hom.Defs

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : CommRing β
f : β →+ α
h : ∀ (x : β), f (x * x) = f x * f x
h_two : 2 ≠ 0
h_one : f 1 = 1
x y : β
hxy : f ((x + y) * (x + y)) = f (x + y) * f (x + y)
⊢ (↑f).toFun (x * y) = (↑f).toFun x * (↑f).toFun y

Tactic:
rw [mul_add, add_mul, add_mul, f.map_add, f.map_add, f.map_add, f.map_add, h x, h y, add_mul,
        mul_add, mul_add, ← sub_eq_zero, add_comm (f x * f x + f (y * x)), ← sub_sub, ← sub_sub,
        ← sub_sub, mul_comm y x, mul_comm (f y) (f x)] at hxy

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : CommRing β
f : β →+ α
h : ∀ (x : β), f (x * x) = f x * f x
h_two : 2 ≠ 0
h_one : f 1 = 1
x y : β
hxy : f (x * y) + f y * f y + (f x * f x + f (x * y)) - f x * f x - f x * f y - f x * f y - f y * f y = 0
⊢ (↑f).toFun (x * y) = (↑f).toFun x * (↑f).toFun y
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
p : (g : G₀) → g ≠ 0 → Prop
⊢ (∃ g hg, p g hg) ↔ ∃ g hg, p ↑(mk0 g hg) ⋯

Tactic:
val_mk0

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

Goal state before:
pp: α : Type u_1
inst✝ : AddMonoidWithOne α
m n : ℕ
⊢ ↑m + ↑n = ↑n + ↑m

Tactic:
← Nat.cast_add,

Goal state after:
α : Type u_1
inst✝ : AddMonoidWithOne α
m n : ℕ
⊢ ↑(m + n) = ↑n + ↑m
Module: Mathlib.Data.Nat.Cast.Commute

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

Tactic:
← Nat.cast_add,

Goal state after:
α : Type u_1
inst✝ : AddMonoidWithOne α
m n : ℕ
⊢ ↑(m + n) = ↑(n + m)
Module: Mathlib.Algebra.Ring.Commute

Goal state before:
pp: R : Type u
inst✝ : CommRing R
a b : R
⊢ a ^ 2 + b ^ 2 - 2 * b * a = (b - a) ^ 2

Tactic:
add_comm,

Goal state after:
R : Type u
inst✝ : CommRing R
a b : R
⊢ b ^ 2 + a ^ 2 - 2 * b * a = (b - a) ^ 2
Module: Mathlib.Data.Int.Cast.Lemmas

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

Tactic:
exact (DFunLike.congr_fun h_nat x :)

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
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℤ
x : R
y : M
⊢ (n • x) • y = n • x • y

Tactic:
cases n with
    | ofNat => simp [mul_smul, Nat.cast_smul_eq_nsmul]
    | negSucc => simp [mul_smul, add_smul, Nat.cast_smul_eq_nsmul]

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✝ : AddMonoidWithOne R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : R), f (x + y) = f x + f y
nsmul : ∀ (n : ℕ) (x : R), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f ↑n = ↑n
n : ℕ
⊢ ↑(n + 1) = ↑n + 1

Tactic:
by rw [← natCast, Nat.cast_succ, add, one, natCast]

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Semiring α
inst✝² : Semiring β
a : α
inst✝¹ : FunLike F α β
inst✝ : RingHomClass F α β
f : F
⊢ Odd a → Odd (f a)

Tactic:
rintro ⟨a, rfl⟩

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Semiring α
inst✝² : Semiring β
inst✝¹ : FunLike F α β
inst✝ : RingHomClass F α β
f : F
a : α
⊢ Odd (f (2 * a + 1))
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝¹ : Semiring α
a b : α
inst✝ : IsCancelAdd α
hab : a + b = 0
k : ℕ
ih : a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0
⊢ 0 = (b + a) * b

Tactic:
add_comm,

Goal state after:
α : Type u_2
inst✝¹ : Semiring α
a b : α
inst✝ : IsCancelAdd α
hab : a + b = 0
k : ℕ
ih : a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0
⊢ 0 = (a + b) * b
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝ : Semiring α
h : ∀ (a : α), Even a
a : α
ha : 1 = 2 * a
⊢ IsUnit 2

Tactic:
eq_comm

Goal state after:
α : Type u_2
inst✝ : Semiring α
h : ∀ (a : α), Even a
a : α
ha : 2 * a = 1
⊢ IsUnit 2
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_4
f : α → α
n : ℕ
hf : Involutive f
hne : f ≠ id
H : id = f
hn : Even n
⊢ f = id

Tactic:
eq_comm

Goal state after:
α : Type u_4
f : α → α
n : ℕ
hf : Involutive f
hne : f ≠ id
H : f = id
hn : Even n
⊢ f = id
Module: Mathlib.Algebra.Order.Sub.Defs

Goal state before:
pp: α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c : α
inst✝ : AddLeftMono α
⊢ a + b - c ≤ a - c + b

Tactic:
add_comm,

Goal state after:
α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c : α
inst✝ : AddLeftMono α
⊢ b + a - c ≤ a - c + b
Module: Mathlib.Algebra.Order.Sub.Defs

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

Tactic:
add_comm,

Goal state after:
α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hb : AddLECancellable b
h : a = b + c
⊢ a = b + c
Module: Mathlib.Algebra.Order.Sub.Defs

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

Tactic:
add_comm,

Goal state after:
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c : α
inst✝ : AddLeftMono α
ha : AddLECancellable a
h : a = b + c
⊢ a = b + c
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulLeftMono α
a b : α
⊢ a / b ≤ a ↔ 1 ≤ b

Tactic:
by
  simp [div_eq_mul_inv]

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

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulLeftMono α
a b : α
⊢ a ≤ a / b ↔ b ≤ 1

Tactic:
by
  simp [div_eq_mul_inv]

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

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

Tactic:
by
  simp [div_eq_mul_inv]

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

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

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

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

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

Tactic:
add_comm,

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

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

Tactic:
rw [inv_mul_lt_iff₀ hc, mul_comm]

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

Goal state before:
pp: α : Type u_6
β : Type u_7
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
x : α
⊢ IsMax x → IsMax (f x)

Tactic:
conv_lhs => rw [← f.symm_apply_apply x]

Goal state after:
α : Type u_6
β : Type u_7
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
x : α
⊢ IsMax (f.symm (f x)) → IsMax (f x)
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: case mp
X : Type u_6
Y : Type u_7
F : Type u_8
inst✝³ : Preorder X
inst✝² : Preorder Y
inst✝¹ : EquivLike F X Y
inst✝ : OrderIsoClass F X Y
f : F
⊢ DenselyOrdered X → DenselyOrdered Y

Tactic:
intro H

Goal state after:
case mp
X : Type u_6
Y : Type u_7
F : Type u_8
inst✝³ : Preorder X
inst✝² : Preorder Y
inst✝¹ : EquivLike F X Y
inst✝ : OrderIsoClass F X Y
f : F
H : DenselyOrdered X
⊢ DenselyOrdered Y
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: case mpr
X : Type u_6
Y : Type u_7
F : Type u_8
inst✝³ : Preorder X
inst✝² : Preorder Y
inst✝¹ : EquivLike F X Y
inst✝ : OrderIsoClass F X Y
f : F
⊢ DenselyOrdered Y → DenselyOrdered X

Tactic:
intro H

Goal state after:
case mpr
X : Type u_6
Y : Type u_7
F : Type u_8
inst✝³ : Preorder X
inst✝² : Preorder Y
inst✝¹ : EquivLike F X Y
inst✝ : OrderIsoClass F X Y
f : F
H : DenselyOrdered Y
⊢ DenselyOrdered X
Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs

Goal state before:
pp: α : Type u
inst✝³ : MulOneClass α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedMul α
a b : α
inst✝ : MulLeftStrictMono α
c : α
⊢ b = a * c → (a ≠ b ↔ c > 1)

Tactic:
gt_iff_lt

Goal state after:
α : Type u
inst✝³ : MulOneClass α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedMul α
a b : α
inst✝ : MulLeftStrictMono α
c : α
⊢ b = a * c → (a ≠ b ↔ 1 < c)