mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Semiconj.Defs

Goal state before:
pp: case zero
M : Type u_2
inst✝ : Monoid M
a x y : M
h : SemiconjBy a x y
⊢ SemiconjBy a 1 (y ^ 0)

Tactic:
pow_zero

Goal state after:
case zero
M : Type u_2
inst✝ : Monoid M
a x y : M
h : SemiconjBy a x y
⊢ SemiconjBy a 1 1
Module: Mathlib.Order.Defs.Unbundled

Goal state before:
pp: α : Sort u_1
r : α → α → Prop
inst✝¹ : Std.Symm r
inst✝ : IsTrans α r
a b c d : α
h₁ : r a b
h₂ : r c d
⊢ r b c ↔ r b d

Tactic:
rel_congr_right h₂

Goal state after:
α : Sort u_1
r : α → α → Prop
inst✝¹ : Std.Symm r
inst✝ : IsTrans α r
a b c d : α
h₁ : r a b
h₂ : r c d
⊢ r b d ↔ r b d
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
a : M
m : ℕ
⊢ 1 = (a ^ m) ^ 0

Tactic:
pow_zero

Goal state after:
M : Type u_2
inst✝ : Monoid M
a : M
m : ℕ
⊢ 1 = 1
Module: Mathlib.Logic.Basic

Goal state before:
pp: a b : Prop
⊢ Xor a b ↔ (a ∨ b) ∧ ¬(a ∧ b)

Tactic:
rw [Xor, or_and_right, not_and_or, and_or_left, and_not_self_iff, false_or,
    and_or_left, and_not_self_iff, or_false]

Goal state after:
Module: Mathlib.Logic.Unique

Goal state before:
pp: α✝ : Sort u_1
ι : Sort u_2
α : ι → Sort u_3
inst✝ : Unique ι
x : α default
i : ι
⊢ α i

Tactic:
rw [Unique.eq_default i]

Goal state after:
α✝ : Sort u_1
ι : Sort u_2
α : ι → Sort u_3
inst✝ : Unique ι
x : α default
i : ι
⊢ α default
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_2
inst✝ : Nonempty α
f : α → β
b : β
h : ∃ a, f a = b
⊢ f (invFun f b) = b

Tactic:
by
  simp only [invFun, dif_pos h, h.choose_spec]

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case single
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ζ : Type u_6
r : α → α → Prop
a b c : α
inst✝ : Std.Symm r
x y b✝ : α
i : r x b✝
⊢ TransGen r b✝ x

Tactic:
| single i =>

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
p : β → β → Prop
f : α → β
h : r ≤ (p on f)
⊢ TransGen r ≤ (TransGen p on f)

Tactic:
intro a _ hab

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
p : β → β → Prop
f : α → β
h : r ≤ (p on f)
a i✝ : α
hab : TransGen r a i✝
⊢ (TransGen p on f) a i✝
Module: Mathlib.Logic.Function.Iterate

Goal state before:
pp: case cons
α : Type u
β : Type v
f : α → α
b : β
l : List β
H : ∀ (a : α), foldl (fun b x ↦ f b) a l = f^[l.length] a
a : α
⊢ foldl (fun b x ↦ f b) a (b :: l) = f^[l.length + 1] a

Tactic:
foldl,

Goal state after:
case cons
α : Type u
β : Type v
f : α → α
b : β
l : List β
H : ∀ (a : α), foldl (fun b x ↦ f b) a l = f^[l.length] a
a : α
⊢ foldl (fun b x ↦ f b) (f a) l = f^[l.length + 1] a
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: M : Type u_9
α : Type u_10
inst✝² : SMul M α
inst✝¹ : SMul Mᵐᵒᵖ α
inst✝ : IsCentralScalar M α
m : Mᵐᵒᵖ
a : α
⊢ MulOpposite.unop m • a = m • a

Tactic:
by
  induction m; exact (IsCentralScalar.op_smul_eq_smul _ a).symm

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

Goal state before:
pp: α : Type u_5
β : Type u_6
inst✝⁵ : Mul α
inst✝⁴ : Mul β
inst✝³ : SMul α β
inst✝² : IsScalarTower α β β
inst✝¹ : IsScalarTower α α β
inst✝ : SMulCommClass α β β
a : α
b : β
c : α
d : β
this : SMulCommClass β α β
⊢ a • b * c • d = (a * c) • (b * d)

Tactic:
exact smul_smul_smul_comm a b c d

Goal state after:
Module: Mathlib.Lean.Meta.CongrTheorems

Goal state before:
pp: α β : Sort u
inst✝ : FastSubsingleton α
h₂ : α = β
a : α
b : β
⊢ a ≍ b

Tactic:
by
  have : Subsingleton α := FastSubsingleton.inst
  exact Subsingleton.helim h₂ a b

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: case refine_2.inl
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
x y : α × β
h₁ : x.fst < y.fst
h₂ : x.snd ≤ y.snd
⊢ x < y

pp: case refine_2.inr
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
x y : α × β
h₁ : x.fst ≤ y.fst
h₂ : x.snd < y.snd
⊢ x < y

Tactic:
· exact ⟨⟨h₁.le, h₂⟩, fun h ↦ h₁.not_ge h.1⟩

Goal state after:
case refine_2.inr
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
x y : α × β
h₁ : x.fst ≤ y.fst
h₂ : x.snd < y.snd
⊢ x < y
Module: Mathlib.Data.Nat.Basic

Goal state before:
pp: case zero
a : ℕ
ha : a ≠ 1
⊢ a * 0 ≤ a ^ 0

Tactic:
exact Nat.zero_le _

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

Goal state before:
pp: case succ.inl
b : ℕ
ha : 0 ≠ 1
⊢ 0 ≤ 0 ^ (b + 1)

Tactic:
exact Nat.zero_le _

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

Goal state before:
pp: m 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) ⋯
h1 : n ≤ m
h2 : n ≤ m + 1
| leRec refl le_succ_of_le h2 = le_succ_of_le h1 (leRec refl le_succ_of_le h1)

Tactic:
lhs

Goal state after:
m 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) ⋯
h1 : n ≤ m
h2 : n ≤ m + 1
| leRec refl le_succ_of_le h2
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
pr : α → Prop
Pinf : ∀ ⦃s t : α⦄, pr s → pr t → pr (s ⊓ t)
hbot : pr ⊥
a b : Subtype pr
this✝ : SemilatticeInf (Subtype pr) := Subtype.semilatticeInf Pinf
this : OrderBot (Subtype pr) := Subtype.orderBot hbot
⊢ a ⊓ b = ⊥ ↔ ↑(a ⊓ b) = ⊥

Tactic:
← Subtype.coe_bot hbot

Goal state after:
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
pr : α → Prop
Pinf : ∀ ⦃s t : α⦄, pr s → pr t → pr (s ⊓ t)
hbot : pr ⊥
a b : Subtype pr
this✝ : SemilatticeInf (Subtype pr) := Subtype.semilatticeInf Pinf
this : OrderBot (Subtype pr) := Subtype.orderBot hbot
⊢ a ⊓ b = ⊥ ↔ ↑(a ⊓ b) = ↑⊥
Module: Mathlib.Data.Set.Subsingleton

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

Tactic:
refine ⟨?_, fun h => ?_⟩

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

case refine_2
α : Type u
s : Set α
h : s.Nonempty ∧ s.Subsingleton
⊢ ∃ a, s = {a}
Module: Mathlib.Order.BooleanAlgebra.Basic

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

Tactic:
ac_rfl

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

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

Tactic:
ac_rfl

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

Goal state before:
pp: α : Type u_1
s t : Set α
hst : s ⊆ t
hs : s.Nonempty
⊢ t \ s ⊂ t

Tactic:
by
  simpa [inter_eq_self_of_subset_right hst]

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

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

Tactic:
ac_rfl

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

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

Tactic:
ac_rfl

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:
ite_inter_inter,

Goal state after:
α : Type u_1
t s₁ s₂ s : Set α
⊢ t.ite s₁ s₂ ∩ t.ite s s = t.ite s₁ s₂ ∩ s
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : Disjoint z (y \ x)
⊢ z ⊔ y \ x ≤ y

Tactic:
sdiff_le

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : Disjoint z (y \ x)
⊢ z ⊔ y ≤ y
Module: Mathlib.Order.BooleanAlgebra.Basic

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

Tactic:
ac_rfl

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

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

Tactic:
ac_rfl

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

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

Tactic:
ac_rfl

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

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

Tactic:
ac_rfl

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

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

Tactic:
ac_rfl

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

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

Tactic:
ac_rfl

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

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

Tactic:
ac_rfl

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

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

Tactic:
ac_rfl

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

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

Tactic:
ac_rfl

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

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

Tactic:
ac_rfl

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

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

Tactic:
ac_rfl

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

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

Tactic:
ac_rfl

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

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

Tactic:
ac_rfl

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

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

Tactic:
ac_rfl

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

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

Tactic:
ac_rfl

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
refine ⟨fun h => ?_, Disjoint.symmDiff_eq_sup⟩

Goal state after:
α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b : α
h : a ∆ b = a ⊔ b
⊢ Disjoint a b
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b c : α
⊢ a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ⊔ (c \ (a ⊔ b) ⊔ c ⊓ a ⊓ b) = a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ⊔ c \ (a ⊔ b) ⊔ a ⊓ b ⊓ c

Tactic:
ac_rfl

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b c : α
⊢ a \ (b ⊔ c) ⊔ a ⊓ b ⊓ c ⊔ (b \ (c ⊔ a) ⊔ c \ (b ⊔ a)) = a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ⊔ c \ (a ⊔ b) ⊔ a ⊓ b ⊓ c

Tactic:
ac_rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
⊢ MapsTo.restrict f (f ⁻¹' t) t ⋯ '' Subtype.val ⁻¹' s = Subtype.val ⁻¹' f '' s

Tactic:
rw [← (Subtype.coe_injective).image_injective.eq_iff, ← image_comp, MapsTo.restrict_commutes,
    image_comp, Subtype.image_preimage_coe, Subtype.image_preimage_coe, image_preimage_inter]

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : MapsTo f s t
h' : Surjective (restrict f s t h)
b : β
hb : b ∈ t
⊢ b ∈ f '' s

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

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : MapsTo f s t
h' : Surjective (restrict f s t h)
b : β
hb : b ∈ t
a : α
ha : a ∈ s
ha' : restrict f s t h ⟨a, ha⟩ = ⟨b, hb⟩
⊢ b ∈ f '' s
Module: Mathlib.Data.Int.Init

Goal state before:
pp: motive : ℤ → Sort u_1
z b : ℤ
zero : motive b
succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)
pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)
hz : z ≤ b
| cast ⋯
      (match z - 1 - b with
      | ofNat n => inductionOn'.pos b zero succ n
      | -[n+1] => inductionOn'.neg b zero pred n) =
    pred z hz
      (cast ⋯
        (match z - b with
        | ofNat n => inductionOn'.pos b zero succ n
        | -[n+1] => inductionOn'.neg b zero pred n))

Tactic:
lhs

Goal state after:
motive : ℤ → Sort u_1
z b : ℤ
zero : motive b
succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)
pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)
hz : z ≤ b
| cast ⋯
    (match z - 1 - b with
    | ofNat n => inductionOn'.pos b zero succ n
    | -[n+1] => inductionOn'.neg b zero pred n)
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
b : β
inst✝ : Nonempty α
h : ∃ a, a ∈ s ∧ f a = b
⊢ Classical.choose h ∈ s ∧ f (Classical.choose h) = b

Tactic:
exact Classical.choose_spec h

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

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
⊢ SurjOn f s t → ∃ s', s' ⊆ s ∧ BijOn f s' t

Tactic:
rcases eq_empty_or_nonempty t with (rfl | ht)

Goal state after:
case mp.inl
α : Type u_1
β : Type u_2
s : Set α
f : α → β
⊢ SurjOn f s ∅ → ∃ s', s' ⊆ s ∧ BijOn f s' ∅

case mp.inr
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
ht : t.Nonempty
⊢ SurjOn f s t → ∃ s', s' ⊆ s ∧ BijOn f s' t
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
s t : Set α
h : SurjOn (⇑g) s t
⊢ SurjOn (⇑(g.extendDomain f)) (Subtype.val ∘ ⇑f '' s) (Subtype.val ∘ ⇑f '' t)

Tactic:
by
  rintro _ ⟨a, ha, rfl⟩
  obtain ⟨b, hb, rfl⟩ := h ha
  exact ⟨_, ⟨_, hb, rfl⟩, by simp_rw [Function.comp_apply, extendDomain_apply_image]⟩

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
a : M
n m : ℕ
ha : a ^ n = 1
⊢ a ^ m = a ^ (m % n + n * (m / n))

Tactic:
rw [Nat.mod_add_div]

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✝¹ : Pow M₁ ℕ
inst✝ : Monoid M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
x : M₁
⊢ f x ^ 0 = 1

Tactic:
pow_zero

Goal state after:
M₁ : Type u_1
M₂ : Type u_2
inst✝³ : Mul M₁
inst✝² : One M₁
inst✝¹ : Pow M₁ ℕ
inst✝ : Monoid M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
x : M₁
⊢ 1 = 1
Module: Mathlib.Algebra.Group.Basic

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

Tactic:
simp [h.symm]

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

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

Tactic:
simp [h.symm]

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 * c⁻¹ = b
⊢ a = b * c

Tactic:
simp [h.symm]

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✝⁴ : Pow M₁ ℕ
inst✝³ : Inv M₁
inst✝² : Div M₁
inst✝¹ : Pow M₁ ℤ
inst✝ : DivisionMonoid M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
x y : M₁
h : x * y = 1
⊢ f x * ?m.113 = 1

Tactic:
rw [← mul, h, one]

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

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

Tactic:
simp [h.symm]

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

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

Tactic:
simp [h.symm]

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

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

Tactic:
rw [div_eq_inv_mul, inv_mul_cancel_left]

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:
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.Basic

Goal state before:
pp: M : Type u_4
F : Type u_5
inst✝ : Monoid F
c : F → M → M
h1 : c 1 = id
hmul : ∀ (f g : F), c (f * g) = c f ∘ c g
f : F
n : ℕ
⊢ c (f ^ n * f) = (c f)^[n] ∘ c f

Tactic:
hmul,

Goal state after:
M : Type u_4
F : Type u_5
inst✝ : Monoid F
c : F → M → M
h1 : c 1 = id
hmul : ∀ (f g : F), c (f * g) = c f ∘ c g
f : F
n : ℕ
⊢ c (f ^ n) ∘ c f = (c f)^[n] ∘ c f
Module: Mathlib.Algebra.Group.Prod

Goal state before:
pp: G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : IsMulTorsionFree M
inst✝ : IsMulTorsionFree N
n : ℕ
hn : n ≠ 0
a b : M × N
hab : (fun a ↦ a ^ n) a = (fun a ↦ a ^ n) b
⊢ a = b

Tactic:
ext <;> apply pow_left_injective hn; exacts [congr(($hab).1), congr(($hab).2)]

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

Goal state before:
pp: M : Type u_3
N : Type u_4
P : Type u_5
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : CommMonoid P
f : M →* P
g : N →* P
x : M
⊢ ((f.coprod g).comp (inl M N)) x = f x

Tactic:
by simp [coprod_apply]

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

Goal state before:
pp: M : Type u_3
N : Type u_4
P : Type u_5
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : CommMonoid P
f : M →* P
g : N →* P
x : N
⊢ ((f.coprod g).comp (inr M N)) x = g x

Tactic:
by simp [coprod_apply]

Goal state after:
Module: Mathlib.Control.Basic

Goal state before:
pp: α β γ : Type u
e : Type v
⊢ ∀ {α β : Type u} (g : α → β) (x : e ⊕ α), pure g <*> x = g <$> x

Tactic:
intros
    rfl

Goal state after:
Module: Mathlib.Control.Basic

Goal state before:
pp: α β γ : Type u
e : Type v
⊢ ∀ {α β : Type u} (x : α) (f : α → e ⊕ β), pure x >>= f = f x

Tactic:
intros
    rfl

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

Goal state before:
pp: case pos
M₀ : Type u_1
inst✝ : MonoidWithZero M₀
n : ℕ
h : n = 0
⊢ 0 ^ 0 = 1

Tactic:
pow_zero

Goal state after:
case pos
M₀ : Type u_1
inst✝ : MonoidWithZero M₀
n : ℕ
h : n = 0
⊢ 1 = 1
Module: Mathlib.Data.Int.Cast.Lemmas

Goal state before:
pp: 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
⊢ f = g

Tactic:
by
  ext (x | x)
  · exact (DFunLike.congr_fun h_nat x :)
  · rw [Int.negSucc_eq, ← neg_one_mul, f.map_mul, g.map_mul]
    congr 1
    exact mod_cast (DFunLike.congr_fun h_nat (x + 1) :)

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

Goal state before:
pp: α : Type u_2
inst✝ : Semiring α
a b : α
⊢ a + a + 1 + (b + b + 1) = a + b + 1 + (a + b + 1)

Tactic:
ac_rfl

Goal state after:
Module: Mathlib.Logic.OpClass

Goal state before:
pp: α : Sort u
β : Sort v
f : α → α → α
hc : Std.Commutative f
ha : Std.Associative f
a b c : α
⊢ f (f b a) c = f b (f a c)

Tactic:
ha.assoc

Goal state after:
α : Sort u
β : Sort v
f : α → α → α
hc : Std.Commutative f
ha : Std.Associative f
a b c : α
⊢ f b (f a c) = f b (f a c)
Module: Mathlib.Logic.OpClass

Goal state before:
pp: α : Sort u
β : Sort v
f : α → α → α
hc : Std.Commutative f
ha : Std.Associative f
a b c : α
⊢ f a (f c b) = f (f a c) b

Tactic:
ha.assoc

Goal state after:
α : Sort u
β : Sort v
f : α → α → α
hc : Std.Commutative f
ha : Std.Associative f
a b c : α
⊢ f a (f c b) = f a (f 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 - b ≤ c ∧ a ≠ b + c

Tactic:
refine ⟨h.le, ?_⟩

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 : α
hc : AddLECancellable c
h : a - c < b
⊢ a - c ≤ b ∧ a ≠ b + c

Tactic:
refine ⟨h.le, ?_⟩

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

Goal state before:
pp: α : Type u_1
inst✝⁶ : Mul α
inst✝⁵ : Zero α
inst✝⁴ : Preorder α
inst✝³ : PosMulStrictMono α
β : Type u_2
inst✝² : Zero β
inst✝¹ : Mul β
inst✝ : Preorder β
f : β → α
zero : f 0 = 0
mul : ∀ (x y : β), f (x * y) = f x * f y
lt : ∀ {x y : β}, f x < f y ↔ x < y
a : β
ha : 0 < a
b c : β
hbc : b < c
⊢ a * b < a * c

Tactic:
rw [← lt, mul, mul]

Goal state after:
α : Type u_1
inst✝⁶ : Mul α
inst✝⁵ : Zero α
inst✝⁴ : Preorder α
inst✝³ : PosMulStrictMono α
β : Type u_2
inst✝² : Zero β
inst✝¹ : Mul β
inst✝ : Preorder β
f : β → α
zero : f 0 = 0
mul : ∀ (x y : β), f (x * y) = f x * f y
lt : ∀ {x y : β}, f x < f y ↔ x < y
a : β
ha : 0 < a
b c : β
hbc : b < c
⊢ f a * f b < f a * f c
Module: Mathlib.Algebra.Order.GroupWithZero.Defs

Goal state before:
pp: α : Type u_1
inst✝⁶ : Mul α
inst✝⁵ : Zero α
inst✝⁴ : Preorder α
inst✝³ : MulPosStrictMono α
β : Type u_2
inst✝² : Zero β
inst✝¹ : Mul β
inst✝ : Preorder β
f : β → α
zero : f 0 = 0
mul : ∀ (x y : β), f (x * y) = f x * f y
lt : ∀ {x y : β}, f x < f y ↔ x < y
a : β
ha : 0 < a
b c : β
hbc : b < c
⊢ b * a < c * a

Tactic:
rw [← lt, mul, mul]

Goal state after:
α : Type u_1
inst✝⁶ : Mul α
inst✝⁵ : Zero α
inst✝⁴ : Preorder α
inst✝³ : MulPosStrictMono α
β : Type u_2
inst✝² : Zero β
inst✝¹ : Mul β
inst✝ : Preorder β
f : β → α
zero : f 0 = 0
mul : ∀ (x y : β), f (x * y) = f x * f y
lt : ∀ {x y : β}, f x < f y ↔ x < y
a : β
ha : 0 < a
b c : β
hbc : b < c
⊢ f b * f a < f c * f a
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic

Goal state before:
pp: case pos
α : Type u_1
inst✝² : MulOneClass α
inst✝¹ : LinearOrder α
inst✝ : MulLeftStrictMono α
a : α
h : a < 1
⊢ ∃ b, b * b ≤ a

pp: case neg
α : Type u_1
inst✝² : MulOneClass α
inst✝¹ : LinearOrder α
inst✝ : MulLeftStrictMono α
a : α
h : 1 ≤ a
⊢ ∃ b, b * b ≤ a

Tactic:
· use a
    have : a * a < a * 1 := mul_lt_mul_right h a
    rw [mul_one] at this
    exact le_of_lt this

Goal state after:
case neg
α : Type u_1
inst✝² : MulOneClass α
inst✝¹ : LinearOrder α
inst✝ : MulLeftStrictMono α
a : α
h : 1 ≤ a
⊢ ∃ b, b * b ≤ a
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: M₀ : Type u_2
inst✝⁴ : MonoidWithZero M₀
inst✝³ : PartialOrder M₀
a : M₀
inst✝² : PosMulStrictMono M₀
inst✝¹ : ZeroLEOneClass M₀
ha : 0 < a
inst✝ : Nontrivial M₀
⊢ 0 < a ^ 0

Tactic:
pow_zero

Goal state after:
M₀ : Type u_2
inst✝⁴ : MonoidWithZero M₀
inst✝³ : PartialOrder M₀
a : M₀
inst✝² : PosMulStrictMono M₀
inst✝¹ : ZeroLEOneClass M₀
ha : 0 < a
inst✝ : Nontrivial M₀
⊢ 0 < 1