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

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

Tactic:
exact (n0 rfl).elim

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

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
a : M
⊢ a ^ 1 = a

Tactic:
by rw [pow_succ, pow_zero, one_mul]

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

Goal state before:
pp: α : Type u_1
⊢ ¬Nontrivial α ↔ Subsingleton α

Tactic:
simp only [nontrivial_iff, subsingleton_iff, not_exists, Classical.not_not]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Nontrivial β
f : α → β
hf : Surjective f
⊢ Nontrivial α

Tactic:
rcases exists_pair_ne β with ⟨x, y, h⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : Nontrivial β
f : α → β
hf : Surjective f
x y : β
h : x ≠ y
⊢ Nontrivial α
Module: Mathlib.Logic.Unique

Goal state before:
pp: α : Sort u_1
inst✝ : Unique α
p : α → Prop
h : p default
x : α
⊢ p x

Tactic:
rwa [Unique.eq_default x]

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

Goal state before:
pp: case neg
γ : Sort u_3
α₁ : Sort u_4
α₂ : Sort u_5
α₃ : Sort u_6
f₁₂ : α₁ → α₂
h₁₂ : Injective f₁₂
f₂₃ : α₂ → α₃
h₂₃ : Injective f₂₃
g : α₁ → γ
e' : α₃ → γ
b : α₂
h₂ : ¬∃ c, f₁₂ c = b
⊢ extend (f₂₃ ∘ f₁₂) g e' (f₂₃ b) = extend f₁₂ g (e' ∘ f₂₃) b

Tactic:
rw [extend_apply' _ _ _ h₂, extend_apply', comp_apply]

Goal state after:
case neg.hb
γ : Sort u_3
α₁ : Sort u_4
α₂ : Sort u_5
α₃ : Sort u_6
f₁₂ : α₁ → α₂
h₁₂ : Injective f₁₂
f₂₃ : α₂ → α₃
h₂₃ : Injective f₂₃
g : α₁ → γ
e' : α₃ → γ
b : α₂
h₂ : ¬∃ c, f₁₂ c = b
⊢ ¬∃ a, (f₂₃ ∘ f₁₂) a = f₂₃ b
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Type u_1
α' : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f : α × α' → β
aa' : α × α'
b : β
a : α
a' : α'
a₂ : α
a₂' : α'
⊢ curry (update f (a₂, a₂') b) a a' =
    update (curry f) (a₂, a₂').fst (update (curry f (a₂, a₂').fst) (a₂, a₂').snd b) a a'

Tactic:
obtain rfl | ha := eq_or_ne a a₂ <;> obtain rfl | ha' := eq_or_ne a' a₂' <;> simp [*]

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
⊢ ReflTransGen (TransGen r) = ReflTransGen r

Tactic:
by
  simp only [← reflGen_transGen, transGen_eq_self]

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

Goal state before:
pp: α : Type u
f : α → α
n : ℕ
hn : 0 < n
⊢ f ∘ f^[n.pred] = f^[n]

Tactic:
by
  rw [← iterate_succ', Nat.succ_pred_eq_of_pos hn]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
f : (i : ι) → α i → α i
n : ℕ
⊢ (Pi.map f)^[n] = Pi.map fun i ↦ (f i)^[n]

Tactic:
induction n

Goal state after:
case zero
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → α i → α i
⊢ (Pi.map f)^[0] = Pi.map fun i ↦ (f i)^[0]

case succ
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → α i → α i
n✝ : ℕ
a✝ : (Pi.map f)^[n✝] = Pi.map fun i ↦ (f i)^[n✝]
⊢ (Pi.map f)^[n✝ + 1] = Pi.map fun i ↦ (f i)^[n✝ + 1]
Module: Mathlib.Algebra.Group.Action.Faithful

Goal state before:
pp: case refine_2
G : Type u_2
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
h : ∀ (g : G), (∀ (a : α), g • a = a) → g = 1
a₁ a₂ : G
h' : ∀ (a : α), a₁ • a = a₂ • a
⊢ a₁ = a₂

Tactic:
rw [← inv_inv a₂, eq_inv_of_mul_eq_one_left (h (a₂⁻¹ * a₁) ?_), inv_inv]

Goal state after:
G : Type u_2
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
h : ∀ (g : G), (∀ (a : α), g • a = a) → g = 1
a₁ a₂ : G
h' : ∀ (a : α), a₁ • a = a₂ • a
⊢ ∀ (a : α), (a₂⁻¹ * a₁) • a = a
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: G : Type u_3
α : Type u_5
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a b : α
h : a = g • b
⊢ g⁻¹ • a = b

Tactic:
rw [h, inv_smul_smul]

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✝³ : Group H
inst✝² : MulAction G H
inst✝¹ : SMulCommClass G H H
inst✝ : IsScalarTower G H H
g : G
a : H
⊢ g • a * g⁻¹ • a⁻¹ = 1

Tactic:
rw [smul_mul_smul_comm, mul_inv_cancel, mul_inv_cancel, one_smul]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → α
g : β → β
n : ℕ
⊢ (map f g)^[n] = map f^[n] g^[n]

Tactic:
induction n

Goal state after:
case zero
α : Type u_1
β : Type u_2
f : α → α
g : β → β
⊢ (map f g)^[0] = map f^[0] g^[0]

case succ
α : Type u_1
β : Type u_2
f : α → α
g : β → β
n✝ : ℕ
a✝ : (map f g)^[n✝] = map f^[n✝] g^[n✝]
⊢ (map f g)^[n✝ + 1] = map f^[n✝ + 1] g^[n✝ + 1]
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
⊢ (fun x1 x2 ↦ x1 < x2)ᶜ = fun x1 x2 ↦ x1 ≥ x2

Tactic:
simp [compl]

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
⊢ (fun x1 x2 ↦ x1 ≤ x2)ᶜ = fun x1 x2 ↦ x1 > x2

Tactic:
simp [compl]

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
⊢ (fun x1 x2 ↦ x1 > x2)ᶜ = fun x1 x2 ↦ x1 ≤ x2

Tactic:
simp [compl]

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
⊢ (fun x1 x2 ↦ x1 ≥ x2)ᶜ = fun x1 x2 ↦ x1 < x2

Tactic:
simp [compl]

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
x✝¹ x✝ : α
⊢ (fun x1 x2 ↦ x1 ≠ x2)ᶜ = Eq

Tactic:
simp [compl]

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝⁸ : LinearOrder β
inst✝⁷ : LE α
inst✝⁶ : LT α
inst✝⁵ : Max α
inst✝⁴ : Min α
inst✝³ : Ord α
inst✝² : DecidableEq α
inst✝¹ : DecidableLE α
inst✝ : DecidableLT α
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
min : ∀ (x y : α), f (x ⊓ y) = Min.min (f x) (f y)
max : ∀ (x y : α), f (x ⊔ y) = Max.max (f x) (f y)
compare : ∀ (x y : α), Ord.compare (f x) (f y) = Ord.compare x y
x✝¹ x✝ : α
⊢ Ord.compare x✝¹ x✝ = compareOfLessAndEq x✝¹ x✝

Tactic:
← compare,

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝⁸ : LinearOrder β
inst✝⁷ : LE α
inst✝⁶ : LT α
inst✝⁵ : Max α
inst✝⁴ : Min α
inst✝³ : Ord α
inst✝² : DecidableEq α
inst✝¹ : DecidableLE α
inst✝ : DecidableLT α
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
min : ∀ (x y : α), f (x ⊓ y) = Min.min (f x) (f y)
max : ∀ (x y : α), f (x ⊔ y) = Max.max (f x) (f y)
compare : ∀ (x y : α), Ord.compare (f x) (f y) = Ord.compare x y
x✝¹ x✝ : α
⊢ Ord.compare (f x✝¹) (f x✝) = compareOfLessAndEq x✝¹ x✝
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
⊢ x = y ∨ y = z ∨ x = z

Tactic:
by_contra hne
  simp only [not_or, ← Ne.eq_def] at hne
  rcases hne.1.lt_or_gt with h₁ | h₁ <;>
  rcases hne.2.1.lt_or_gt with h₂ | h₂ <;>
  rcases hne.2.2.lt_or_gt with h₃ | h₃
  exacts [h h₁ h₂, h h₂ h₃, h h₃ h₂, h h₃ h₁, h h₁ h₃, h h₂ h₃, h h₁ h₃, h h₂ h₁]

Goal state after:
Module: Mathlib.Order.Compare

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ (cmp a b).Compares a b

Tactic:
obtain h | h | h := lt_trichotomy a b <;> simp [cmp, cmpUsing, h, h.not_gt]

Goal state after:
Module: Mathlib.Order.RelClasses

Goal state before:
pp: case inr.inr
α : Type u
β : Type v
r✝ : α → α → Prop
s : β → β → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a b c : α
hab : r a b
hbc : r b c
hca : r c a
⊢ r a c

Tactic:
exact IsWellFounded.wf.asymmetric₃ a b c hab hbc hca |>.elim

Goal state after:
Module: Mathlib.Order.RelClasses

Goal state before:
pp: α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
x✝¹ x✝ : α × β
a₁ : α
a₂ : β
b₁ : α
b₂ : β
hab : ¬Prod.Lex r s (a₁, a₂) (b₁, b₂)
hba : ¬Prod.Lex r s (b₁, b₂) (a₁, a₂)
⊢ (a₁, a₂) = (b₁, b₂)

Tactic:
by
    obtain rfl := Std.Trichotomous.trichotomous a₁ b₁
      (mt (Prod.Lex.left a₂ b₂) hab) (mt (Prod.Lex.left b₂ a₂) hba)
    obtain rfl := Std.Trichotomous.trichotomous a₂ b₂
      (mt (Prod.Lex.right a₁) hab) (mt (Prod.Lex.right a₁) hba)
    rfl

Goal state after:
Module: Mathlib.Order.RelClasses

Goal state before:
pp: α : Type u
r : α → α → Prop
s : Set α
⊢ ¬Unbounded r s ↔ Bounded r s

Tactic:
not_iff_comm,

Goal state after:
α : Type u
r : α → α → Prop
s : Set α
⊢ ¬Bounded r s ↔ Unbounded r s
Module: Mathlib.Order.PropInstances

Goal state before:
pp: case mpr
ι : Type u_1
α' : ι → Type u_3
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → OrderBot (α' i)
f g : (i : ι) → α' i
h : ∀ (i : ι), Disjoint (f i) (g i)
x : (i : ι) → α' i
hf : x ≤ f
hg : x ≤ g
i : ι
⊢ x i ≤ ⊥ i

Tactic:
apply h i (hf i) (hg i)

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
inst✝ : Lattice α
a b : α
⊢ a ⊓ b = a ⊔ b ↔ a = b

Tactic:
by rw [← inf_le_sup.ge_iff_eq, sup_le_inf]

Goal state after:
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:
rw [← Option.ne_none_iff_isSome]
        intro hn
        rw [Option.not_isSome_iff_eq_none, ← hn] at h
        exact Option.some_ne_none _ (e.injective h)

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

Goal state before:
pp: α : Type u_1
a b : α
hab : a ≠ b
⊢ {a, b} \ {a} = {b}

Tactic:
by
  rw [insert_sdiff_of_mem _ (mem_singleton a), sdiff_singleton_eq_self (by simpa)]

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

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

Tactic:
← inf_sdiff_left

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
| x ⊓ (y \ z ⊓ y) ⊓ x \ y
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:
by
  rw [sdiff_sdiff_right', inf_eq_right.2 h]

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

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
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
a : α
⊢ Option.elim' default Subtype.val ((fun a ↦ if h : a = default then none else some ⟨a, h⟩) a) = a

Tactic:
dsimp only

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
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
a : α
⊢ Option.elim' default Subtype.val (if h : a = default then none else some ⟨a, h⟩) = a
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
β : Type u_1
x y z : α
inst✝ : BooleanAlgebra α
a b : α
⊢ a ⊓ b ⊔ a \ b = a

Tactic:
rw [sdiff_eq, ← inf_sup_left, sup_compl_eq_top, inf_top_eq]

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
p : α → Prop
inst✝ : DecidablePred p
x₀ : { a // p a } → β
x✝ : { x // x ∘ Subtype.val = x₀ }
x : α → β
hx : x ∘ Subtype.val = x₀
a : α
⊢ ↑((fun x ↦ ⟨fun a ↦ if h : p a then x₀ ⟨a, h⟩ else x ⟨a, h⟩, ⋯⟩) ((fun x a ↦ ↑x ↑a) ⟨x, hx⟩)) a = ↑⟨x, hx⟩ a

Tactic:
dsimp only

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
p : α → Prop
inst✝ : DecidablePred p
x₀ : { a // p a } → β
x✝ : { x // x ∘ Subtype.val = x₀ }
x : α → β
hx : x ∘ Subtype.val = x₀
a : α
⊢ (if h : p a then x₀ ⟨a, h⟩ else x a) = x a
Module: Mathlib.Order.BooleanAlgebra.Basic

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

Tactic:
compl_compl,

Goal state after:
α : Type u
x y : α
inst✝ : BooleanAlgebra α
⊢ xᶜ ⊔ y = y ⊔ xᶜ
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
p : α → Prop
inst✝ : DecidablePred p
x₀ : { a // p a } → β
x : { a // ¬p a } → β
x✝ : { a // ¬p a }
a : α
h : ¬p a
⊢ (if h_1 : p a then x₀ ⟨↑⟨a, h⟩, h_1⟩ else x ⟨↑⟨a, h⟩, h_1⟩) = x ⟨a, h⟩

Tactic:
dsimp only

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
p : α → Prop
inst✝ : DecidablePred p
x₀ : { a // p a } → β
x : { a // ¬p a } → β
x✝ : { a // ¬p a }
a : α
h : ¬p a
⊢ (if h : p a then x₀ ⟨a, h⟩ else x ⟨a, h⟩) = x ⟨a, h⟩
Module: Mathlib.Logic.Equiv.Basic

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

Tactic:
swap_comm _ a

Goal state after:
α : Sort u_1
inst✝ : DecidableEq α
a : α
⊢ Injective fun x ↦ swap a x
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
p : α × β → Prop
⊢ (∃ x, x ∈ s ×ˢ t ∧ p x) ↔ ∃ x, x ∈ s ∧ ∃ y, y ∈ t ∧ p (x, y)

Tactic:
simp [and_assoc]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
s : Set α
⊢ range f \ f '' s = f '' sᶜ

Tactic:
by
  rw [image_compl_eq_range_sdiff_image hf]

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

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : s.Nonempty ∧ t.Nonempty
heq : s ×ˢ t = s₁ ×ˢ t₁
h₁ : s₁.Nonempty ∧ t₁.Nonempty
⊢ s = s₁ ∧ t = t₁

Tactic:
← fst_image_prod s h.2,

Goal state after:
case mp
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : s.Nonempty ∧ t.Nonempty
heq : s ×ˢ t = s₁ ×ˢ t₁
h₁ : s₁.Nonempty ∧ t₁.Nonempty
⊢ Prod.fst '' s ×ˢ t = s₁ ∧ t = t₁
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : s ×ˢ t = ∅
⊢ s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅) ↔ s ×ˢ t = s₁ ×ˢ t₁

Tactic:
simp_rw [h, @eq_comm _ ∅, prod_eq_empty_iff, prod_eq_empty_iff.mp h, true_and,
      or_iff_right_iff_imp]
    rintro ⟨rfl, rfl⟩
    exact prod_eq_empty_iff.mp h

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
h : Surjective (image f)
y : β
s : Set α
hs : f '' s = {y}
this : y ∈ f '' s
⊢ ∃ a, f a = y

Tactic:
rcases this with ⟨x, _, hx⟩

Goal state after:
α : Type u
β : Type v
f : α → β
h : Surjective (image f)
y : β
s : Set α
hs : f '' s = {y}
x : α
left✝ : x ∈ s
hx : f x = y
⊢ ∃ a, f a = y
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
s : Set β
t : Set γ
hf : Surjective f
hg : SurjOn g s t
⊢ SurjOn (g ∘ f) (f ⁻¹' s) t

Tactic:
by
  rwa [SurjOn, image_comp g f, image_preimage_eq _ hf]

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

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

Tactic:
by simpa using h.mapsTo

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
F : Type u_9
inst✝ : MulOne M
n : ℕ
f : Monoid.End M
⊢ (⇑f)^[n] = ⇑(npowRec n f)

Tactic:
induction n

Goal state after:
case zero
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
F : Type u_9
inst✝ : MulOne M
f : Monoid.End M
⊢ (⇑f)^[0] = ⇑(npowRec 0 f)

case succ
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
F : Type u_9
inst✝ : MulOne M
f : Monoid.End M
n✝ : ℕ
a✝ : (⇑f)^[n✝] = ⇑(npowRec n✝ f)
⊢ (⇑f)^[n✝ + 1] = ⇑(npowRec (n✝ + 1) f)
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
h : Semiconj f fa fb
ha : Surjective fa
⊢ SurjOn fb (range f) (range f)

Tactic:
rw [← image_univ]
  exact h.surjOn_image ha.surjOn

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

Goal state before:
pp: α : Type u_1
inst✝ : DivInvMonoid α
x✝¹ : ℕ
x✝ : αᵐᵒᵖ
⊢ unop (x✝ ^ ↑x✝¹.succ) = unop (x✝ ^ ↑x✝¹ * x✝)

Tactic:
by
    simp_rw [HPow.hPow, Pow.pow]
    rw [unop_op, zpow_natCast, pow_succ', unop_mul, unop_op, zpow_natCast]

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

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

Tactic:
mul_inv_eq_one,

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a : G
m n : ℤ
⊢ a ^ (n + m) = a ^ n * a ^ m

Tactic:
zpow_add

Goal state after:
G : Type u_3
inst✝ : Group G
a : G
m n : ℤ
⊢ a ^ n * a ^ m = a ^ n * a ^ m
Module: Mathlib.Algebra.Group.Basic

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

Tactic:
rw [← inv_div, mul_div_cancel_left]

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

Goal state before:
pp: α : Type u
inst✝ : Monoid α
a✝ b u a : αˣ
⊢ a ^ 0 = 1

Tactic:
by simp only [HPow.hPow, Pow.pow]; ext; simp

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

Goal state before:
pp: G₀ : Type u_4
G₀' : Type u_5
inst✝⁴ : GroupWithZero G₀
inst✝³ : GroupWithZero G₀'
inst✝² : MulActionWithZero G₀ G₀'
inst✝¹ : SMulCommClass G₀ G₀' G₀'
inst✝ : IsScalarTower G₀ G₀' G₀'
c : G₀
x : G₀'
⊢ (c • x)⁻¹ = c⁻¹ • x⁻¹

Tactic:
obtain rfl | hc := eq_or_ne c 0
  · simp only [inv_zero, zero_smul]
  obtain rfl | hx := eq_or_ne x 0
  · simp only [inv_zero, smul_zero]
  · refine inv_eq_of_mul_eq_one_left ?_
    rw [smul_mul_smul_comm, inv_mul_cancel₀ hc, inv_mul_cancel₀ hx, one_smul]

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

Goal state before:
pp: case zero
R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
e : n - m = 0
⊢ ↑(match 0 with
      | 0 => ofNat (m - n)
      | k.succ => -[k+1]) =
    ↑m - ↑n

pp: case succ
R : Type u
inst✝ : AddGroupWithOne R
m n n✝ : ℕ
e : n - m = n✝ + 1
⊢ ↑(match n✝ + 1 with
      | 0 => ofNat (m - n)
      | k.succ => -[k+1]) =
    ↑m - ↑n

Tactic:
· simp [Nat.le_of_sub_eq_zero e]

Goal state after:
case succ
R : Type u
inst✝ : AddGroupWithOne R
m n n✝ : ℕ
e : n - m = n✝ + 1
⊢ ↑(match n✝ + 1 with
      | 0 => ofNat (m - n)
      | k.succ => -[k+1]) =
    ↑m - ↑n
Module: Mathlib.Data.Nat.Sqrt

Goal state before:
pp: a n : ℕ
h : a ≤ n + n
⊢ (n ^ 2 + a).sqrt = n

Tactic:
by
  simpa [Nat.pow_two] using sqrt_add_eq n h

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

Goal state before:
pp: α : Type u_2
inst✝ : Monoid α
n : ℕ
hn : Even n
⊢ ∀ (a : α), IsSquare (a ^ n)

Tactic:
by aesop (add simp pow_add)

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
f : Multiplicative ℕ →* M
n : Multiplicative ℕ
⊢ f n = (powersHom M).symm f ^ toAdd n

Tactic:
← powersHom_apply,

Goal state after:
M : Type u_1
inst✝ : Monoid M
f : Multiplicative ℕ →* M
n : Multiplicative ℕ
⊢ f n = ((powersHom M) ((powersHom M).symm f)) n
Module: Mathlib.Data.Nat.Cast.Basic

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

Tactic:
induction n

Goal state after:
case zero
α : Type u_1
inst✝ : NonAssocSemiring α
m : ℕ
⊢ ↑(m * 0) = ↑m * ↑0

case succ
α : Type u_1
inst✝ : NonAssocSemiring α
m n✝ : ℕ
a✝ : ↑(m * n✝) = ↑m * ↑n✝
⊢ ↑(m * (n✝ + 1)) = ↑m * ↑(n✝ + 1)
Module: Mathlib.Algebra.Ring.Basic

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

Tactic:
rw [neg_inv]

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
x✝² : NonAssocSemiring α
x✝¹ : NonAssocSemiring β
x✝ : NonAssocSemiring γ
n : ℕ
f : α →+* α
⊢ (⇑f)^[n] = ⇑(npowRec n f)

Tactic:
induction n

Goal state after:
case zero
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
x✝² : NonAssocSemiring α
x✝¹ : NonAssocSemiring β
x✝ : NonAssocSemiring γ
f : α →+* α
⊢ (⇑f)^[0] = ⇑(npowRec 0 f)

case succ
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
x✝² : NonAssocSemiring α
x✝¹ : NonAssocSemiring β
x✝ : NonAssocSemiring γ
f : α →+* α
n✝ : ℕ
a✝ : (⇑f)^[n✝] = ⇑(npowRec n✝ f)
⊢ (⇑f)^[n✝ + 1] = ⇑(npowRec (n✝ + 1) f)
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
      rw [Ring.inverse_non_unit _ h]
      exact not_isUnit_zero

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
n : ℕ
⊢ (-1) ^ n = (-1) ^ (n % 2)

Tactic:
rw [← Nat.mod_add_div n 2, pow_add, pow_mul]; simp [sq]

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

Goal state before:
pp: α : Type u_2
inst✝ : Semiring α
a : α
ha : Even a
n : ℕ
x✝ : n + 1 ≠ 0
⊢ Even (a ^ (n + 1))

Tactic:
rw [pow_succ]

Goal state after:
α : Type u_2
inst✝ : Semiring α
a : α
ha : Even a
n : ℕ
x✝ : n + 1 ≠ 0
⊢ Even (a ^ n * a)
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: case succ
α : Type u_2
inst✝ : Semiring α
a : α
ha : Odd a
n : ℕ
hrec : Odd (a ^ n)
⊢ Odd (a ^ (n + 1))

Tactic:
rw [pow_succ]

Goal state after:
case succ
α : Type u_2
inst✝ : Semiring α
a : α
ha : Odd a
n : ℕ
hrec : Odd (a ^ n)
⊢ Odd (a ^ n * a)
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: case inl
α : Type u_1
inst✝³ : MulZeroClass α
a b : α
inst✝² : LinearOrder α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
hab : 0 < a * b
ha : a < 0
⊢ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0

Tactic:
refine Or.inr ⟨ha, lt_imp_lt_of_le_imp_le (fun hb => ?_) hab⟩

Goal state after:
case inl
α : Type u_1
inst✝³ : MulZeroClass α
a b : α
inst✝² : LinearOrder α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
hab : 0 < a * b
ha : a < 0
hb : 0 ≤ b
⊢ a * b ≤ 0
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: M₀ : Type u_2
inst✝³ : MonoidWithZero M₀
inst✝² : Preorder M₀
a : M₀
inst✝¹ : ZeroLEOneClass M₀
inst✝ : PosMulMono M₀
h : 1 ≤ a
n : ℕ
⊢ a ^ n ≤ a ^ (n + 1)

Tactic:
rw [pow_succ]

Goal state after:
M₀ : Type u_2
inst✝³ : MonoidWithZero M₀
inst✝² : Preorder M₀
a : M₀
inst✝¹ : ZeroLEOneClass M₀
inst✝ : PosMulMono M₀
h : 1 ≤ a
n : ℕ
⊢ a ^ n ≤ a ^ n * a
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: M₀ : Type u_2
inst✝³ : MonoidWithZero M₀
inst✝² : LinearOrder M₀
inst✝¹ : PosMulStrictMono M₀
a : M₀
inst✝ : ZeroLEOneClass M₀
ha₀ : 0 < a
ha₁ : a ≠ 1
⊢ Injective fun x ↦ a ^ x

Tactic:
obtain ha₁ | ha₁ := ha₁.lt_or_gt

Goal state after:
case inl
M₀ : Type u_2
inst✝³ : MonoidWithZero M₀
inst✝² : LinearOrder M₀
inst✝¹ : PosMulStrictMono M₀
a : M₀
inst✝ : ZeroLEOneClass M₀
ha₀ : 0 < a
ha₁✝ : a ≠ 1
ha₁ : a < 1
⊢ Injective fun x ↦ a ^ x

case inr
M₀ : Type u_2
inst✝³ : MonoidWithZero M₀
inst✝² : LinearOrder M₀
inst✝¹ : PosMulStrictMono M₀
a : M₀
inst✝ : ZeroLEOneClass M₀
ha₀ : 0 < a
ha₁✝ : a ≠ 1
ha₁ : 1 < a
⊢ Injective fun x ↦ a ^ x
Module: Mathlib.Logic.Embedding.Basic

Goal state before:
pp: α : Type u_1
p q : α → Prop
inst✝ : DecidablePred p
x y : { x // p x ∨ q x }
⊢ (fun x ↦ if h : p ↑x then Sum.inl ⟨↑x, h⟩ else Sum.inr ⟨↑x, ⋯⟩) x =
      (fun x ↦ if h : p ↑x then Sum.inl ⟨↑x, h⟩ else Sum.inr ⟨↑x, ⋯⟩) y →
    x = y

Tactic:
dsimp only

Goal state after:
α : Type u_1
p q : α → Prop
inst✝ : DecidablePred p
x y : { x // p x ∨ q x }
⊢ ((if h : p ↑x then Sum.inl ⟨↑x, h⟩ else Sum.inr ⟨↑x, ⋯⟩) = if h : p ↑y then Sum.inl ⟨↑y, h⟩ else Sum.inr ⟨↑y, ⋯⟩) →
    x = y
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✝¹ : AddLeftReflectLE R
inst✝ : AddLeftMono R
a b : R
⊢ 4 * a * b ≤ (a + b) ^ 2

Tactic:
calc 4 * a * b
    _ = 2 * a * b + 2 * a * b := by rw [mul_assoc, two_add_two_eq_four.symm, add_mul, mul_assoc]
    _ ≤ a ^ 2 + b ^ 2 + 2 * a * b := by gcongr; exact two_mul_le_add_sq _ _
    _ = a ^ 2 + 2 * a * b + b ^ 2 := by rw [add_right_comm]
    _ = (a + b) ^ 2 := (add_sq a b).symm

Goal state after: