mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Tactic.AdaptationNote

Goal state before:
pp: ⊢ True

Tactic:
by
  #adaptation_note /-- This is a test -/
  trivial

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

Goal state before:
pp: motive : Nat → Sort u
zero : motive 0
bit : (b : Bool) → (n : Nat) → (n = 0 → b = true) → motive n → motive (Nat.bit b n)
⊢ (if h : 0 = 0 → true = true then bit true 0 h zero
    else
      have this := ⋯;
      ⋯ ▸ zero) =
    bit true 0 binaryRec'_one._proof_1 zero

Tactic:
dif_pos

Goal state after:
motive : Nat → Sort u
zero : motive 0
bit : (b : Bool) → (n : Nat) → (n = 0 → b = true) → motive n → motive (Nat.bit b n)
⊢ bit true 0 ?hc zero = bit true 0 binaryRec'_one._proof_1 zero

case hc
motive : Nat → Sort u
zero : motive 0
bit : (b : Bool) → (n : Nat) → (n = 0 → b = true) → motive n → motive (Nat.bit b n)
⊢ 0 = 0 → true = true
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
n : ℕ
m : M
⊢ npowBinRec (n + 1) m = npowBinRec n m * m

Tactic:
iterate 2 rw [← npowBinRecAuto, ← npowRec_eq_npowBinRec]

Goal state after:
M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
n : ℕ
m : M
⊢ npowRecAuto (n + 1) m = npowRecAuto n m * m
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
n : ℕ
m : M
⊢ npowBinRec (n + 1) m = npowBinRec n m * m

Tactic:
by
  iterate 2 rw [← npowBinRecAuto, ← npowRec_eq_npowBinRec]
  rfl

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

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

Tactic:
rw [pow_succ _ n, pow_succ, pow_succ', mul_assoc]

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

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

Tactic:
induction n with
  | zero => simp
  | succ n ih => simp [pow_succ', ← ih, mul_assoc]

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

Goal state before:
pp: G : Type u_1
inst✝ : CommGroup G
a b : G
⊢ a⁻¹ * b * a = b

Tactic:
by
  rw [mul_comm, mul_inv_cancel_left]

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

Goal state before:
pp: α : Sort u
f : α → α
h : Involutive f
P : Prop
inst✝ : Decidable P
x : α
⊢ f (if P then x else f x) = if ¬P then x else f x

Tactic:
rw [apply_ite f, h, ite_not]

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

Goal state before:
pp: α : Type u_3
β : Type u_4
A B : Set (α → β)
hAB : A ⊆ B
hA : A.SeparatesPoints
⊢ B.SeparatesPoints

Tactic:
intro x y hne

Goal state after:
α : Type u_3
β : Type u_4
A B : Set (α → β)
hAB : A ⊆ B
hA : A.SeparatesPoints
x y : α
hne : x ≠ y
⊢ ∃ f, f ∈ B ∧ f x ≠ f y
Module: Mathlib.Logic.Relation

Goal state before:
pp: case refl
α : Type u_1
r : α → α → Prop
a b c : α
U : Relator.RightUnique r
ac : ReflTransGen r a c
⊢ ReflTransGen r a c ∨ ReflTransGen r c a

Tactic:
exact Or.inl ac

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case tail
α : Type u_1
r : α → α → Prop
a b c : α
U : Relator.RightUnique r
ac : ReflTransGen r a c
b✝ c✝ : α
a✝ : ReflTransGen r a b✝
bd : r b✝ c✝
IH : ReflTransGen r b✝ c ∨ ReflTransGen r c b✝
⊢ ReflTransGen r c✝ c ∨ ReflTransGen r c c✝

Tactic:
rcases IH with (IH | IH)

Goal state after:
case tail.inl
α : Type u_1
r : α → α → Prop
a b c : α
U : Relator.RightUnique r
ac : ReflTransGen r a c
b✝ c✝ : α
a✝ : ReflTransGen r a b✝
bd : r b✝ c✝
IH : ReflTransGen r b✝ c
⊢ ReflTransGen r c✝ c ∨ ReflTransGen r c c✝

case tail.inr
α : Type u_1
r : α → α → Prop
a b c : α
U : Relator.RightUnique r
ac : ReflTransGen r a c
b✝ c✝ : α
a✝ : ReflTransGen r a b✝
bd : r b✝ c✝
IH : ReflTransGen r c b✝
⊢ ReflTransGen r c✝ c ∨ ReflTransGen r c c✝
Module: Mathlib.Logic.Relation

Goal state before:
pp: case tail
α : Type u_1
r : α → α → Prop
a b c : α
U : Relator.RightUnique r
ac : ReflTransGen r a c
b✝ c✝ : α
a✝ : ReflTransGen r a b✝
bd : r b✝ c✝
IH : ReflTransGen r b✝ c ∨ ReflTransGen r c b✝
⊢ ReflTransGen r c✝ c ∨ ReflTransGen r c c✝

Tactic:
| tail _ bd IH =>

Goal state after:
Module: Mathlib.Algebra.Opposites

Goal state before:
pp: α : Type u_1
inst✝ : Add α
⊢ IsCancelAdd αᵐᵒᵖ ↔ IsCancelAdd α

Tactic:
simp_rw [isCancelAdd_iff, isLeftCancelAdd_iff, isRightCancelAdd_iff]

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

Goal state before:
pp: α : Type u
f : α → α
m n : ℕ
⊢ f^[m * (n + 1)] = f^[m]^[n + 1]

Tactic:
by simp only [Nat.mul_succ, iterate_one, iterate_add, iterate_mul m n]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
a a' : α → γ
b b' : β → γ
inst✝ : Mul γ
x : α ⊕ β
⊢ Sum.elim (a * a') (b * b') x = (Sum.elim a b * Sum.elim a' b') x

Tactic:
cases x <;> rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
a a' : α → γ
b b' : β → γ
inst✝ : Div γ
x : α ⊕ β
⊢ Sum.elim (a / a') (b / b') x = (Sum.elim a b / Sum.elim a' b') x

Tactic:
cases x <;> rfl

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

Goal state before:
pp: case lt
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.lt
⊢ Ordering.lt ≠ Ordering.lt ↔ b ≤ a

Tactic:
simpa using compare_lt_iff_lt.1 h

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : LinearOrder α
a b : α
h1 : ¬(fun x1 x2 ↦ x1 < x2) a b
h2 : (fun x1 x2 ↦ x1 < x2) b a
⊢ Ordering.gt.Compares a b

Tactic:
exact h2

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: case pos
α : Type u_2
β : Type u_3
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝¹ : f a < f b
h✝ : a < b
⊢ Ordering.lt = Ordering.lt

Tactic:
try (first | rfl | contradiction)

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: case pos
α : Type u_2
β : Type u_3
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝² : f a < f b
h✝¹ : ¬a < b
h✝ : a = b
⊢ False

Tactic:
try (first | rfl | contradiction)

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: case neg
α : Type u_2
β : Type u_3
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝² : f a < f b
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ False

Tactic:
try (first | rfl | contradiction)

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: case pos
α : Type u_2
β : Type u_3
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝² : ¬f a < f b
h✝¹ : f a = f b
h✝ : a < b
⊢ False

Tactic:
try (first | rfl | contradiction)

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: case pos
α : Type u_2
β : Type u_3
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : f a = f b
h✝¹ : ¬a < b
h✝ : a = b
⊢ Ordering.eq = Ordering.eq

Tactic:
try (first | rfl | contradiction)

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: case neg
α : Type u_2
β : Type u_3
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : f a = f b
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ False

Tactic:
try (first | rfl | contradiction)

Goal state after:
case neg
α : Type u_2
β : Type u_3
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : f a = f b
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ False
Module: Mathlib.Order.Basic

Goal state before:
pp: case pos
α : Type u_2
β : Type u_3
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝² : ¬f a < f b
h✝¹ : ¬f a = f b
h✝ : a < b
⊢ False

Tactic:
try (first | rfl | contradiction)

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: case pos
α : Type u_2
β : Type u_3
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : ¬f a = f b
h✝¹ : ¬a < b
h✝ : a = b
⊢ False

Tactic:
try (first | rfl | contradiction)

Goal state after:
case pos
α : Type u_2
β : Type u_3
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : ¬f a = f b
h✝¹ : ¬a < b
h✝ : a = b
⊢ False
Module: Mathlib.Order.Basic

Goal state before:
pp: case neg
α : Type u_2
β : Type u_3
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : ¬f a = f b
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ Ordering.gt = Ordering.gt

Tactic:
try (first | rfl | contradiction)

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

Goal state before:
pp: case inr
n m : ℕ
h : m < n
⊢ n ∣ n - m ↔ m = 0 ∨ n ≤ m

Tactic:
rcases eq_or_ne m 0 with rfl | hm

Goal state after:
case inr.inl
n : ℕ
h : 0 < n
⊢ n ∣ n - 0 ↔ 0 = 0 ∨ n ≤ 0

case inr.inr
n m : ℕ
h : m < n
hm : m ≠ 0
⊢ n ∣ n - m ↔ m = 0 ∨ n ≤ m
Module: Mathlib.Data.Nat.Init

Goal state before:
pp: n : ℕ
motive : (m : ℕ) → n ≤ m → Sort u_1
refl : motive n ⋯
le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯
⊢ leRec refl le_succ_of_le ⋯ = le_succ_of_le ⋯ refl

Tactic:
leRec_succ,

Goal state after:
n : ℕ
motive : (m : ℕ) → n ≤ m → Sort u_1
refl : motive n ⋯
le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯
⊢ le_succ_of_le ?h1 (leRec refl le_succ_of_le ?h1) = le_succ_of_le ⋯ refl

case h1
n : ℕ
motive : (m : ℕ) → n ≤ m → Sort u_1
refl : motive n ⋯
le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯
⊢ n ≤ n
Module: Mathlib.Order.Compare

Goal state before:
pp: α : Type u_1
inst✝ : LT α
a b : α
o : Ordering
⊢ o.swap.Compares a b ↔ o.Compares b a

Tactic:
cases o
  · exact Iff.rfl
  · exact eq_comm
  · exact Iff.rfl

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
p : β → Prop
h : ∀ (a : α), p (f a)
⊢ range (Subtype.coind f h) = Subtype.val ⁻¹' range f

Tactic:
simp [Set.ext_iff, Subtype.ext_iff]

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

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

Tactic:
by
  split_ifs <;> simp_all

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

Goal state before:
pp: α : Type u_1
s : Set α
a b : α
hs : s.Nonempty
⊢ ¬s = ∅

Tactic:
exact hs.ne_empty

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

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

Tactic:
rw [sdiff_le_iff, sup_comm]

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

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b c d : α
⊢ d ≤ a ⇨ b ⊓ c ↔ d ≤ (a ⇨ b) ⊓ (a ⇨ c)

Tactic:
simp_rw [le_himp_iff, le_inf_iff, le_himp_iff]

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

Goal state before:
pp: α : Type u_2
inst✝ : HeytingAlgebra α
a b : α
⊢ (a ⊓ b)ᶜᶜ = aᶜᶜ ⊓ bᶜᶜ

Tactic:
by
  refine ((compl_anti compl_sup_compl_le).trans (compl_sup_distrib _ _).le).antisymm ?_
  rw [le_compl_iff_disjoint_right, disjoint_assoc, disjoint_compl_compl_left_iff,
    disjoint_left_comm, disjoint_compl_compl_left_iff, ← disjoint_assoc, inf_comm]
  exact disjoint_compl_right

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

Goal state before:
pp: case neg
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : LinearOrder α
inst✝ : BoundedOrder α
a b c : α
h : ¬b ≤ c
⊢ a ≤ c ↔ min a b ≤ c

Tactic:
rw [inf_le_iff, or_iff_left h]

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

Goal state before:
pp: α : Type u_1
t s₁ s₂ s : Set α
⊢ t.ite (s₁ ∩ s) (s₂ ∩ s) = t.ite s₁ s₂ ∩ s

Tactic:
rw [ite_inter_inter, ite_same]

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

Goal state before:
pp: case inl
α✝ : 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
p : α → Prop
inst✝ : DecidablePred p
x : α
hx : p x
⊢ (if h : p x then Sum.inl ⟨x, h⟩ else Sum.inr ⟨x, h⟩) = Sum.inl ⟨x, hx⟩

Tactic:
dif_pos

Goal state after:
case inl
α✝ : 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
p : α → Prop
inst✝ : DecidablePred p
x : α
hx : p x
⊢ Sum.inl ⟨x, ?inl.hc⟩ = Sum.inl ⟨x, hx⟩

case inl.hc
α✝ : 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
p : α → Prop
inst✝ : DecidablePred p
x : α
hx : p x
⊢ p x
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
h : y < z \ x
hxz : x ≤ z
⊢ x ⊔ y < z

Tactic:
rw [← sup_sdiff_cancel_right hxz]

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
h : y < z \ x
hxz : x ≤ z
⊢ x ⊔ y < x ⊔ z \ x
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: α : Sort u_1
inst✝ : DecidableEq α
r a : α
⊢ swapCore a a r = r

Tactic:
by
  unfold swapCore
  split_ifs <;> simp [*]

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
symmDiff_right_inj

Goal state after:
α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b : α
⊢ b = ⊥ ↔ 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:
ext (i | i) <;> rfl

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b c : α
ha : a ≤ c
⊢ a ∆ b = c ↔ c \ a = b

Tactic:
rw [← symmDiff_of_le ha]

Goal state after:
α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b c : α
ha : a ≤ c
⊢ a ∆ b = c ↔ a ∆ c = b
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
a b c : α
h : Disjoint a b
⊢ c ≤ a ∆ c ⊔ b ∆ c

Tactic:
trans c \ (a ⊓ b)
  · rw [h.eq_bot, sdiff_bot]
  · rw [sdiff_inf]
    exact sup_le_sup le_sup_right le_sup_right

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
g : β → α
hfg : LeftInverse g f
s : Set α
x : α
⊢ f x ∈ g ⁻¹' s ↔ x ∈ s

Tactic:
rw [Set.mem_preimage, hfg x]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
⊢ ⊤ ⊆ range Sum.inl ⊔ range Sum.inr

Tactic:
rintro (x | y) - <;> [left; right] <;> exact mem_range_self _

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

Goal state before:
pp: M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
g : N →ₙ* P
f₁ f₂ : M →ₙ* N
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
x : M
⊢ g (f₁ x) = g (f₂ x)

Tactic:
by rw [← MulHom.comp_apply, h, MulHom.comp_apply]

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

Goal state before:
pp: m : ℤ
motive : (n : ℤ) → m ≤ n → Sort u_1
base : motive m ⋯
succ : (n : ℤ) → (hmn : m ≤ n) → motive n hmn → motive (n + 1) ⋯
n : ℤ
hmn : m ≤ n
⊢ Int.leInduction base succ (n + 1) ⋯ = succ n hmn (Int.leInduction base succ n hmn)

Tactic:
rw [Int.leInduction, inductionOn'_add_one hmn]

Goal state after:
m : ℤ
motive : (n : ℤ) → m ≤ n → Sort u_1
base : motive m ⋯
succ : (n : ℤ) → (hmn : m ≤ n) → motive n hmn → motive (n + 1) ⋯
n : ℤ
hmn : m ≤ n
⊢ succ n hmn
      (Int.inductionOn' (motive := fun x ↦ (hmn : m ≤ x) → motive x hmn) n m (fun x ↦ base)
        (fun k hle ih x ↦ succ k hle (ih hle)) (fun x x_1 x_2 x_3 ↦ ⋯.elim) hmn) =
    succ n hmn (Int.leInduction base succ n hmn)
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
s : Set α
h : Semiconj f fa fb
ha : InjOn fa s
hf : InjOn f (fa '' s)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
H : fb (f x) = fb (f y)
⊢ f x = f y

Tactic:
simp only [← h.eq] at H

Goal state after:
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
s : Set α
h : Semiconj f fa fb
ha : InjOn fa s
hf : InjOn f (fa '' s)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
H : f (fa x) = f (fa y)
⊢ f x = f y
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
a b : M
n : ℕ
h : a * b = 1
⊢ a ^ n * (a * b) * b ^ n = 1

Tactic:
by simp [h, pow_mul_pow_eq_one]

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

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

Tactic:
rw [Int.mul_comm, zpow_mul]

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

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

Tactic:
rw [← h, inv_mul_cancel_right]

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

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

Tactic:
by
  induction n with
  | zero => simp
  | succ n ihn => simp only [← Int.add_assoc, zpow_add_one, ihn, mul_assoc]
  | pred n ihn => rw [zpow_sub_one, ← mul_assoc, ← ihn, ← zpow_sub_one, Int.add_sub_assoc]

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

Goal state before:
pp: M₁ : Type u_1
M₂ : Type u_2
inst✝² : Mul M₂
inst✝¹ : One M₂
inst✝ : MulOneClass M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
x : M₁
⊢ f x * 1 = f x

Tactic:
by rw [← one, ← mul, mul_one]

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:
by
  rw [mul_comm]; apply div_mul_div_cancel

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 * d = c * b

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

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

Goal state before:
pp: α : Type u
inst✝ : DivisionMonoid α
a b : α
ha : IsUnit a
hb : IsUnit b
⊢ IsUnit (a / b)

Tactic:
by
  rw [div_eq_mul_inv]; exact ha.mul hb.inv

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

Goal state before:
pp: α : Type u
inst✝ : Monoid α
b : αˣ
a c : α
h : a * ↑b⁻¹ = c
⊢ a = c * ↑b

Tactic:
rw [← h, inv_mul_cancel_right]

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

Goal state before:
pp: α : Type u
inst✝ : CommMonoid α
x y : α
ux uy : αˣ
⊢ x * (y /ₚ uy) /ₚ ux = x * y /ₚ (ux * uy)

Tactic:
← divp_assoc,

Goal state after:
α : Type u
inst✝ : CommMonoid α
x y : α
ux uy : αˣ
⊢ x * y /ₚ uy /ₚ ux = x * y /ₚ (ux * uy)
Module: Mathlib.Algebra.Group.Units.Basic

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
h : Bijective fun x ↦ x * a
⊢ (fun x ↦ x * a) (a * ⋯.choose) = (fun x ↦ x * a) 1

Tactic:
simpa [mul_assoc] using congr_arg (a * ·) (h.2 1).choose_spec

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

Goal state before:
pp: α : Type u_7
β : α → Type u_8
⊢ Function.Injective ⇑(sigmaCongrRightHom β)

Tactic:
intro x y h
  ext a b
  simpa using Equiv.congr_fun h ⟨a, b⟩

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

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

Tactic:
Nat.cast_zero,

Goal state after:
R : Type u_1
inst✝ : AddMonoidWithOne R
⊢ 0 + 1 = 1
Module: Mathlib.Algebra.Ring.Defs

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

Tactic:
Nat.cast_zero,

Goal state after:
case zero
α : Type u
inst✝ : NonAssocSemiring α
a : α
⊢ 0 = 0 * a
Module: Mathlib.Data.Nat.Sqrt

Goal state before:
pp: a b c : ℕ
h : a = b * c
⊢ b ≤ a.sqrt ∨ c ≤ a.sqrt

Tactic:
rcases le_total b c with bc | cb

Goal state after:
case inl
a b c : ℕ
h : a = b * c
bc : b ≤ c
⊢ b ≤ a.sqrt ∨ c ≤ a.sqrt

case inr
a b c : ℕ
h : a = b * c
cb : c ≤ b
⊢ b ≤ a.sqrt ∨ c ≤ a.sqrt
Module: Mathlib.Algebra.Group.Even

Goal state before:
pp: case mp
α : Type u_2
inst✝ : DivisionMonoid α
a : α
h : IsSquare a⁻¹
⊢ IsSquare a

Tactic:
simpa using (isSquare_op_iff.mpr h).map (MulEquiv.inv' α).symm

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

Goal state before:
pp: case mpr
α : Type u_2
inst✝ : DivisionMonoid α
a : α
h : IsSquare a
⊢ IsSquare a⁻¹

Tactic:
simpa using (isSquare_op_iff.mpr h).map (MulEquiv.inv' α).symm

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

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

Tactic:
Nat.cast_zero,

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 b : R
⊢ -(b / a) = -b / a

Tactic:
by rw [neg_div]

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

Goal state before:
pp: G₀ : Type u_1
inst✝ : MulZeroClass G₀
a : G₀
⊢ SemiconjBy a 0 0

Tactic:
simp only [SemiconjBy, mul_zero, zero_mul]

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

Goal state before:
pp: G₀ : Type u_1
inst✝ : MulZeroClass G₀
x y : G₀
⊢ SemiconjBy 0 x y

Tactic:
simp only [SemiconjBy, mul_zero, zero_mul]

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

Goal state before:
pp: β : Type u_4
inst✝ : AddGroup β
f : ℤ →+ β
n : ℤ
⊢ f n = n • f 1

Tactic:
← zmultiplesHom_symm_apply,

Goal state after:
β : Type u_4
inst✝ : AddGroup β
f : ℤ →+ β
n : ℤ
⊢ f n = n • (zmultiplesHom β).symm f
Module: Mathlib.Algebra.Ring.InjSurj

Goal state before:
pp: R : Type u_1
S : Type u_2
f✝ : S → R
hf✝ : Injective 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
f : S → R
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
nsmul : ∀ (n : ℕ) (x : S), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f ↑n = ↑n
⊢ ↑0 = f 0

Tactic:
Nat.cast_zero,

Goal state after:
R : Type u_1
S : Type u_2
f✝ : S → R
hf✝ : Injective 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
f : S → R
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
nsmul : ∀ (n : ℕ) (x : S), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f ↑n = ↑n
⊢ 0 = f 0
Module: Mathlib.Algebra.Module.NatInt

Goal state before:
pp: case zero
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : M
⊢ ↑0 • b = 0 • b

Tactic:
Nat.cast_zero,

Goal state after:
case zero
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : M
⊢ 0 • b = 0 • b