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

Goal state before:
pp: M : Type u_2
inst✝ : MulOneClass M
a : M
⊢ a = 1 * a

Tactic:
one_mul

Goal state after:
M : Type u_2
inst✝ : MulOneClass M
a : M
⊢ a = a
Module: Mathlib.Order.Defs.Unbundled

Goal state before:
pp: case inr.inl
α : Sort u_1
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : Std.Trichotomous r
a c : α
h₁ : ¬r a a
h₂ : r a c
⊢ r a c

Tactic:
exact h₂

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

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
a b : M
h : Commute a b
⊢ 1 = 1 * 1

Tactic:
one_mul

Goal state after:
M : Type u_2
inst✝ : Monoid M
a b : M
h : Commute a b
⊢ 1 = 1
Module: Mathlib.Algebra.Group.Defs

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

Tactic:
by
  induction k using Nat.strongRecOn with
  | ind k' ih =>
    match k' with
    | 0 => rfl
    | k + 1 =>
      rw [npowRec, npowRec'_succ k.succ_ne_zero, ← mul_assoc]
      congr
      simp [ih]

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

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

Tactic:
one_mul

Goal state after:
M : Type u_2
inst✝ : Monoid M
a : M
⊢ a = a
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
n : ℕ
⊢ 1 * 1 = 1

Tactic:
one_mul

Goal state after:
M : Type u_2
inst✝ : Monoid M
n : ℕ
⊢ 1 = 1
Module: Mathlib.Algebra.Group.Defs

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

Tactic:
rw [Nat.mul_comm, pow_mul]

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

Goal state before:
pp: G : Type u_1
inst✝ : DivInvMonoid G
a : G
n : ℕ
⊢ a ^ Int.negSucc n = (a ^ ↑(n + 1))⁻¹

Tactic:
exact DivInvMonoid.zpow_neg' n a

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

Goal state before:
pp: G : Type u_1
inst✝ : DivInvMonoid G
x : G
⊢ x⁻¹ = 1 * x⁻¹

Tactic:
one_mul

Goal state after:
G : Type u_1
inst✝ : DivInvMonoid G
x : G
⊢ x⁻¹ = x⁻¹
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a b : G
⊢ 1 * b = b

Tactic:
one_mul

Goal state after:
G : Type u_1
inst✝ : Group G
a b : G
⊢ b = b
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_3
p : α → Prop
b : Prop
ha : Nonempty α
a : α
h : (∀ (x : α), p x) → b
h' : ∀ (x : α), ¬(p x → b)
⊢ False

Tactic:
exact if hb : b then h' a fun _ ↦ hb else hb <| h fun x ↦ (Classical.not_imp.1 (h' x)).1

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : BEq α
inst✝² : LawfulBEq α
inst✝¹ : BEq β
inst✝ : LawfulBEq β
a₁ a₂ : α
b₁ b₂ : β
⊢ (a₁ == a₂) = (b₁ == b₂) ↔ (a₁ = a₂ ↔ b₁ = b₂)

Tactic:
rw [Bool.eq_iff_iff]; simp

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

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

Tactic:
ext a
  by_cases h₃ : ∃ b, f₂₃ b = a
  · obtain ⟨b, rfl⟩ := h₃
    rw [Injective.extend_apply h₂₃]
    by_cases h₂ : ∃ c, f₁₂ c = b
    · obtain ⟨c, rfl⟩ := h₂
      rw [h₁₂.extend_apply]
      exact (h₂₃.comp h₁₂).extend_apply _ _ _
    · rw [extend_apply' _ _ _ h₂, extend_apply', comp_apply]
      exact fun h ↦ h₂ (Exists.casesOn h fun c hc ↦ Exists.intro c (h₂₃ hc))
  · rw [extend_apply' _ _ _ h₃, extend_apply']
    exact fun h ↦ h₃ (Exists.casesOn h fun c hc ↦ Exists.intro (f₁₂ c) (hc))

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
⊢ Std.Refl r ↔ Eq ≤ r

Tactic:
unfold Pi.hasLe Prop.le

Goal state after:
α : Type u_1
r : α → α → Prop
⊢ Std.Refl r ↔ Eq ≤ r
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
⊢ Std.Irrefl r ↔ r ≤ Ne

Tactic:
unfold Pi.hasLe Prop.le

Goal state after:
α : Type u_1
r : α → α → Prop
⊢ Std.Irrefl r ↔ r ≤ Ne
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝ : Std.Refl r
f : α → β
hf : Surjective f
y : α
⊢ Relation.Map r f f (f y) (f y)

Tactic:
exact ⟨y, y, refl y, rfl, rfl⟩

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
f : α → β
⊢ r ≤ (Relation.Map r f f on f)

Tactic:
unfold Pi.hasLe Prop.le

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
f : α → β
⊢ r ≤ (Relation.Map r f f on f)
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
r : β → β → Prop
f : α → β
⊢ Relation.Map (r on f) f f ≤ r

Tactic:
unfold Pi.hasLe Prop.le

Goal state after:
α : Type u_1
β : Type u_2
r : β → β → Prop
f : α → β
⊢ Relation.Map (r on f) f f ≤ r
Module: Mathlib.Data.Subtype

Goal state before:
pp: β : Sort u_2
γ : Sort u_3
p : β → Prop
g : { x // p x } → γ
j : β → γ
b : β
hb : ¬p b
⊢ extend val g j b = j b

Tactic:
grind [Function.extend]

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case refine_1
α : Type u_1
r : α → α → Prop
a b : α
h : ReflTransGen r a b
⊢ b = a ∨ TransGen r a b

Tactic:
cases h with
    | refl => exact Or.inl rfl
    | tail hac hcb => exact Or.inr (TransGen.tail' hac hcb)

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

Goal state before:
pp: α : Type u_5
β : Type u_6
inst✝² : DivInvMonoid β
inst✝¹ : SMul α β
inst✝ : IsScalarTower α β β
r : α
x y : β
⊢ r • x / y = r • (x / y)

Tactic:
by simp [div_eq_mul_inv, smul_mul_assoc]

Goal state after:
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 : α
⊢ g⁻¹ • g • a = a

Tactic:
by rw [smul_smul, inv_mul_cancel, one_smul]

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

Goal state before:
pp: M : Type u_9
N : Type u_10
inst✝² : MulOneClass N
inst✝¹ : SMul M N
inst✝ : IsScalarTower M N N
x : M
y : N
⊢ x • (1 * y) = x • y

Tactic:
one_mul

Goal state after:
M : Type u_9
N : Type u_10
inst✝² : MulOneClass N
inst✝¹ : SMul M N
inst✝ : IsScalarTower M N N
x : M
y : N
⊢ x • y = x • y
Module: Mathlib.Algebra.Group.Pi.Basic

Goal state before:
pp: I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f i
i : I
inst✝ : (i : I) → DivInvMonoid (f i)
⊢ ∀ (n : ℕ) (a : (i : I) → f i), a ^ ↑n.succ = a ^ ↑n * a

Tactic:
intros; ext; exact DivInvMonoid.zpow_succ' _ _

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

Goal state before:
pp: case inl
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a < b
⊢ min a b = if b ≤ a then b else a

Tactic:
simp [le_of_lt, not_le_of_gt, h, min_def]

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

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a = b
⊢ min a b = if b ≤ a then b else a

Tactic:
simp [le_of_lt, not_le_of_gt, h, min_def]

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

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : b < a
⊢ min a b = if b ≤ a then b else a

Tactic:
simp [le_of_lt, not_le_of_gt, h, min_def]

Goal state after:
Module: Mathlib.Order.Compare

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, o.Compares a b → o.Compares a' b'
o : Ordering
⊢ o.Compares a b ↔ o.Compares a' b'

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

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, o.Compares a b → o.Compares a' b'
o : Ordering
ho : o.Compares a' b'
⊢ o.Compares a b
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: case a
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
a₁ a₂ : α
h_mon : Monotone f
h_fa : f a₁ = f a₂
i : α
h₁ : a₁ ≤ i
h₂ : i ≤ a₂
⊢ f i ≤ f a₁

pp: case a
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
a₁ a₂ : α
h_mon : Monotone f
h_fa : f a₁ = f a₂
i : α
h₁ : a₁ ≤ i
h₂ : i ≤ a₂
⊢ f a₁ ≤ f i

Tactic:
· rw [h_fa]; exact h_mon h₂

Goal state after:
case a
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
a₁ a₂ : α
h_mon : Monotone f
h_fa : f a₁ = f a₂
i : α
h₁ : a₁ ≤ i
h₂ : i ≤ a₂
⊢ f a₁ ≤ f i
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: case succ
β : Type v
r : β → β → Prop
inst✝ : IsTrans β r
f : ℤ → β
h : ∀ (n : ℤ), r (f n) (f (n + 1))
a : ℤ
n : ℕ
ihn : r (f a) (f (a + ↑n.succ))
⊢ r (f a) (f (a + ↑(n + 1) + 1))

Tactic:
exact _root_.trans ihn (h _)

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α✝ : Type u
β : Type v
α : Type u_1
inst✝ : Min α
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
inf_idem : ∀ (a : α), a ⊓ a = a
a b : α
⊢ b ⊓ (a ⊓ b) = a ⊓ b

Tactic:
rw [inf_comm, inf_assoc, inf_idem]

Goal state after:
Module: Mathlib.Order.Lattice

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

Tactic:
ext x y
  unfold maxDefault
  split_ifs with h'
  exacts [sup_of_le_right h', sup_of_le_left <| (total_of (· ≤ ·) x y).resolve_left h']

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst✝¹ : LinearOrder α
inst✝ : SemilatticeInf β
hf : AntitoneOn f s
hx : x ∈ s
hy : y ∈ s
⊢ f (max x y) = f x ⊓ f y

Tactic:
cases le_total x y <;> have := hf ?_ ?_ ‹_› <;>
    first
    | assumption
    | simp only [*, sup_of_le_left, sup_of_le_right, inf_of_le_left, inf_of_le_right]

Goal state after:
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
    exact ((H <| u y).mpr (gc.l_u_le y)).antisymm ((gc _ _).mp <| (H z).mp le_rfl)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x : α
⊢ some (e.symm.removeNoneAux (e.removeNoneAux x)) = some x

Tactic:
by
      cases h1 : e.symm (some (removeNoneAux e x)) <;> cases h2 : e (some x)
      · rw [removeNoneAux_none _ h1]
        exact (e.eq_symm_apply.mpr h2).symm
      · rw [removeNoneAux_some _ ⟨_, h2⟩] at h1
        simp at h1
      · rw [removeNoneAux_none _ h2] at h1
        simp at h1
      · rw [removeNoneAux_some _ ⟨_, h1⟩]
        rw [removeNoneAux_some _ ⟨_, h2⟩]
        simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
e : Option α ≃ Option β
h : e none = none
⊢ e.symm none = none

Tactic:
simpa using (congr_arg e.symm h).symm

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

Goal state before:
pp: case none
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x : α
h : e (some x) = none
⊢ e none = e none ↔ e.symm none = some x

Tactic:
simpa using (congr_arg e.symm h).symm

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

Goal state before:
pp: α : Type u
β : Type u_1
x y z : α
inst✝ : BooleanAlgebra α
a b c : α
⊢ a ≤ b ⇨ c ↔ a ⊓ b ≤ c

Tactic:
rw [himp_eq, isCompl_compl.le_sup_right_iff_inf_left_le]

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

Goal state before:
pp: case pos
α : 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 : α
h✝ : p a
⊢ x₀ ⟨a, h✝⟩ = x a

Tactic:
rw [← hx]; rfl

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
by
  rw [symmDiff, h.sdiff_eq_left, h.sdiff_eq_right]

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
ι : Type ?u.23
π : ι → Type u_9
f : { f // ∀ (i : ι), (f i).fst = i }
i : ι
⊢ π (↑f i).fst

Tactic:
exact (f.1 i).2

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
simp only [(· ⇔ ·), himp_eq]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
t : Set β
a : α
⊢ {a} ×ˢ t = Prod.mk a '' t

Tactic:
ext ⟨x, y⟩
  simp [and_left_comm, eq_comm]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
b : β
⊢ s ×ˢ {b} = (fun a ↦ (a, b)) '' s

Tactic:
ext ⟨x, y⟩
  simp [and_left_comm, eq_comm]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t t₁ : Set β
h : s.Nonempty
⊢ s ×ˢ t ⊆ s ×ˢ t₁ ↔ t ⊆ t₁

Tactic:
by
  simp +contextual [prod_subset_prod_iff, or_comm (a := s = ∅), or_iff_left h.ne_empty]

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

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

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

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s t : Set β
hf : Surjective f
⊢ s ⊆ univ

Tactic:
apply subset_univ

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

Goal state before:
pp: α : Type u_1
s : Set α
t : Set ↑s
x : α
x✝ : x ∈ val '' t
y : { x // x ∈ s }
left✝ : y ∈ t
yvaleq : ↑y = x
⊢ x ∈ s

Tactic:
rw [← yvaleq]; exact y.property

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

Goal state before:
pp: case mk.mk
ι : 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
inst✝ : MulOne N
toOneHom✝¹ : OneHom M N
map_mul'✝¹ : ∀ (x y : M), toOneHom✝¹.toFun (x * y) = toOneHom✝¹.toFun x * toOneHom✝¹.toFun y
toOneHom✝ : OneHom M N
map_mul'✝ : ∀ (x y : M), toOneHom✝.toFun (x * y) = toOneHom✝.toFun x * toOneHom✝.toFun y
h :
  (fun f ↦ f.toFun) { toOneHom := toOneHom✝¹, map_mul' := map_mul'✝¹ } =
    (fun f ↦ f.toFun) { toOneHom := toOneHom✝, map_mul' := map_mul'✝ }
⊢ toOneHom✝¹ = toOneHom✝

Tactic:
apply DFunLike.coe_injective

Goal state after:
case mk.mk
ι : 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
inst✝ : MulOne N
toOneHom✝¹ : OneHom M N
map_mul'✝¹ : ∀ (x y : M), toOneHom✝¹.toFun (x * y) = toOneHom✝¹.toFun x * toOneHom✝¹.toFun y
toOneHom✝ : OneHom M N
map_mul'✝ : ∀ (x y : M), toOneHom✝.toFun (x * y) = toOneHom✝.toFun x * toOneHom✝.toFun y
h :
  (fun f ↦ f.toFun) { toOneHom := toOneHom✝¹, map_mul' := map_mul'✝¹ } =
    (fun f ↦ f.toFun) { toOneHom := toOneHom✝, map_mul' := map_mul'✝ }
⊢ ⇑toOneHom✝¹ = ⇑toOneHom✝
Module: Mathlib.Algebra.Group.Equiv.Defs

Goal state before:
pp: F : 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
inst✝³ : EquivLike F M N
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulEquivClass F M N
e : F
⊢ e (1 * EquivLike.inv e 1) = e (EquivLike.inv e 1)

Tactic:
one_mul

Goal state after:
F : 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
inst✝³ : EquivLike F M N
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulEquivClass F M N
e : F
⊢ e (EquivLike.inv e 1) = e (EquivLike.inv e 1)
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✝¹ : Group G
inst✝ : MulOneClass M
f : M → G
map_mul : ∀ (a b : M), f (a * b) = f a * f b
⊢ f 1 = 1 * f 1

Tactic:
one_mul

Goal state after:
ι : 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✝¹ : Group G
inst✝ : MulOneClass M
f : M → G
map_mul : ∀ (a b : M), f (a * b) = f a * f b
⊢ f 1 = f 1
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)
⊢ InjOn fb (f '' s)

Tactic:
rintro _ ⟨x, hx, rfl⟩ _ ⟨y, hy, rfl⟩ H
  simp only [← h.eq] at H
  exact congr_arg f (ha hx hy <| hf (mem_image_of_mem fa hx) (mem_image_of_mem fa hy) H)

Goal state after:
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 : MapsTo (⇑g) s t
a : α
ha : a ∈ s
⊢ (Subtype.val ∘ ⇑f) (g a) = (g.extendDomain f) ((Subtype.val ∘ ⇑f) a)

Tactic:
by simp_rw [Function.comp_apply, extendDomain_apply_image]

Goal state after:
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
b : α
hb : b ∈ s
ha : g b ∈ t
⊢ (g.extendDomain f) ((Subtype.val ∘ ⇑f) b) = (Subtype.val ∘ ⇑f) (g b)

Tactic:
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✝ : CommMonoid M
a b : M
⊢ 1 = 1 * 1

Tactic:
one_mul

Goal state after:
M : Type u_4
inst✝ : CommMonoid M
a b : M
⊢ 1 = 1
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: M : Type u_4
inst✝¹ : Monoid M
inst✝ : IsRightCancelMul M
a b : M
⊢ a * b = b ↔ a * b = 1 * b

Tactic:
one_mul

Goal state after:
M : Type u_4
inst✝¹ : Monoid M
inst✝ : IsRightCancelMul M
a b : M
⊢ a * b = b ↔ a * b = b
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a : α
n : ℤ
⊢ (a ^ n)⁻¹ = a ^ (-n)

Tactic:
zpow_neg

Goal state after:
α : Type u_1
inst✝ : DivisionMonoid α
a : α
n : ℤ
⊢ (a ^ n)⁻¹ = (a ^ n)⁻¹
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 : Injective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
x : M₁
⊢ 1 * f x = f x

Tactic:
one_mul

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

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

Tactic:
one_mul

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

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

Tactic:
by rw [zpow_add, zpow_one]

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 * a ^ (-n) = a ^ m * (a ^ n)⁻¹

Tactic:
zpow_neg

Goal state after:
G : Type u_3
inst✝ : Group G
a : G
m n : ℤ
⊢ a ^ m * (a ^ n)⁻¹ = a ^ m * (a ^ n)⁻¹
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 (1 * x) = f x

Tactic:
one_mul

Goal state after:
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 = f x
Module: Mathlib.Algebra.Group.Units.Defs

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

Tactic:
one_mul

Goal state after:
α : Type u
inst✝ : Monoid α
a : αˣ
b : α
⊢ b = b
Module: Mathlib.Algebra.Group.Units.Defs

Goal state before:
pp: M : Type u_3
inst✝ : Monoid M
u : Mˣ
a : M
x✝ : IsUnit (↑u * a)
v : Mˣ
hv : ↑v = ↑u * a
this : IsUnit (1 * a)
⊢ IsUnit a

Tactic:
one_mul

Goal state after:
M : Type u_3
inst✝ : Monoid M
u : Mˣ
a : M
x✝ : IsUnit (↑u * a)
v : Mˣ
hv : ↑v = ↑u * a
this : IsUnit a
⊢ IsUnit a
Module: Mathlib.Algebra.Group.Units.Basic

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

Tactic:
one_mul

Goal state after:
α : Type u
inst✝ : Monoid α
u : αˣ
a : α
h : a * ↑u = 1
⊢ ↑u⁻¹ = ↑u⁻¹
Module: Mathlib.Algebra.Group.Units.Basic

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

Tactic:
one_mul

Goal state after:
α : Type u
inst✝ : Monoid α
a : α
u : αˣ
⊢ a = ↑u ↔ a = ↑u
Module: Mathlib.Algebra.Group.Units.Basic

Goal state before:
pp: α : Type u
inst✝¹ : LeftCancelMonoid α
inst✝ : Subsingleton αˣ
a b : α
h : 1 * b = 1
⊢ b = 1

Tactic:
one_mul

Goal state after:
α : Type u
inst✝¹ : LeftCancelMonoid α
inst✝ : Subsingleton αˣ
a b : α
h : b = 1
⊢ b = 1
Module: Mathlib.Algebra.Group.Units.Basic

Goal state before:
pp: α : Type u
inst✝¹ : RightCancelMonoid α
inst✝ : Subsingleton αˣ
a b : α
h : 1 * b = 1
⊢ b = 1

Tactic:
one_mul

Goal state after:
α : Type u
inst✝¹ : RightCancelMonoid α
inst✝ : Subsingleton αˣ
a b : α
h : b = 1
⊢ b = 1
Module: Mathlib.Algebra.Group.Units.Basic

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a b : M
h : IsUnit b
⊢ a * b = b ↔ a * b = 1 * b

Tactic:
one_mul

Goal state after:
M : Type u_1
inst✝ : Monoid M
a b : M
h : IsUnit b
⊢ a * b = b ↔ a * b = b
Module: Mathlib.Algebra.Group.Units.Basic

Goal state before:
pp: α : Type u
inst✝ : DivisionCommMonoid α
a b : α
h : IsUnit a
⊢ 1 * b⁻¹ = b⁻¹

Tactic:
one_mul

Goal state after:
α : Type u
inst✝ : DivisionCommMonoid α
a b : α
h : IsUnit a
⊢ b⁻¹ = b⁻¹
Module: Mathlib.Algebra.GroupWithZero.NeZero

Goal state before:
pp: M₀ : Type u_1
M₀' : Type u_2
inst✝¹ : MulZeroOneClass M₀
inst✝ : Nontrivial M₀
h : 1 = 0
x y : M₀
hx : x ≠ y
⊢ x = 1 * x

Tactic:
one_mul

Goal state after:
M₀ : Type u_1
M₀' : Type u_2
inst✝¹ : MulZeroOneClass M₀
inst✝ : Nontrivial M₀
h : 1 = 0
x y : M₀
hx : x ≠ y
⊢ x = x
Module: Mathlib.Algebra.GroupWithZero.NeZero

Goal state before:
pp: M₀ : Type u_1
M₀' : Type u_2
inst✝¹ : MulZeroOneClass M₀
inst✝ : Nontrivial M₀
h : 1 = 0
x y : M₀
hx : x ≠ y
⊢ 1 * y = y

Tactic:
one_mul

Goal state after:
M₀ : Type u_1
M₀' : Type u_2
inst✝¹ : MulZeroOneClass M₀
inst✝ : Nontrivial M₀
h : 1 = 0
x y : M₀
hx : x ≠ y
⊢ y = y
Module: Mathlib.Algebra.GroupWithZero.Defs

Goal state before:
pp: case zero
M₀ : Type u_1
inst✝¹ : MonoidWithZero M₀
M : Type u_2
inst✝ : Monoid M
f : M₀ → M
x : M₀
hx : ∀ (y : M₀), f (x * y) = f x * f y
y : M₀
⊢ f y = 1 * f y

Tactic:
one_mul

Goal state after:
case zero
M₀ : Type u_1
inst✝¹ : MonoidWithZero M₀
M : Type u_2
inst✝ : Monoid M
f : M₀ → M
x : M₀
hx : ∀ (y : M₀), f (x * y) = f x * f y
y : M₀
⊢ f y = f y
Module: Mathlib.Algebra.Group.Action.Opposite

Goal state before:
pp: case h
M✝ : Type u_1
N✝ : Type u_2
α : Type u_3
β : Type u_4
M : Type u_5
N : Type u_6
inst✝² : Mul N
inst✝¹ : SMul M N
inst✝ : IsScalarTower M N N
x : M
z X✝ : N
⊢ x • op X✝ • z = op X✝ • x • z

Tactic:
simp only [smul_mul_assoc, MulOpposite.smul_eq_mul_unop]

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

Goal state before:
pp: G₀ : Type u
M₀ : Type u_1
inst✝ : GroupWithZero G₀
a✝ a b : G₀
hb : b ≠ 0
⊢ a * b / b = a

Tactic:
by rw [div_eq_mul_inv, mul_assoc, mul_inv_cancel₀ hb, mul_one]

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

Goal state before:
pp: M₀ : Type u_1
a b : M₀
inst✝¹ : MulZeroOneClass M₀
inst✝ : IsRightCancelMulZero M₀
⊢ a * b = b ↔ a * b = 1 * b

Tactic:
one_mul

Goal state after:
M₀ : Type u_1
a b : M₀
inst✝¹ : MulZeroOneClass M₀
inst✝ : IsRightCancelMulZero M₀
⊢ a * b = b ↔ a * b = b
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: M₀ : Type u_1
a b : M₀
inst✝¹ : MulZeroOneClass M₀
inst✝ : IsRightCancelMulZero M₀
hb : b ≠ 0
⊢ a * b = 1 * b ↔ a * b = b

Tactic:
one_mul

Goal state after:
M₀ : Type u_1
a b : M₀
inst✝¹ : MulZeroOneClass M₀
inst✝ : IsRightCancelMulZero M₀
hb : b ≠ 0
⊢ a * b = b ↔ a * b = b