mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Defs.Unbundled

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

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

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

Tactic:
· exact _root_.trans h₁ h₃

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

case inr.inr
α : Sort u_1
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : Std.Trichotomous r
a b c : α
h₁ : r a b
h₂ : ¬r c b
h₃ : r c b
⊢ r a c
Module: Mathlib.Algebra.Group.Defs

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

Tactic:
by rw [Nat.add_zero, pow_zero, mul_one]

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

Goal state before:
pp: α : Sort u_1
r : α → α → Prop
inst✝ : Symm r
h : ∀ (a : α), ∃! b, r a b
⊢ ∃ f, Involutive f ∧ r = fun x1 x2 ↦ f x1 = x2

Tactic:
rcases forall_existsUnique_iff'.1 h with ⟨f, rfl : r = _⟩

Goal state after:
α : Sort u_1
f : α → α
inst✝ : Symm fun x1 x2 ↦ f x1 = x2
h : ∀ (a : α), ∃! b, (fun x1 x2 ↦ f x1 = x2) a b
⊢ ∃ f_1, Involutive f_1 ∧ (fun x1 x2 ↦ f x1 = x2) = fun x1 x2 ↦ f_1 x1 = x2
Module: Mathlib.Data.Quot

Goal state before:
pp: α : Sort u_1
s : Setoid α
x y : Quotient s
⊢ x.out ≈ y.out ↔ x = y

Tactic:
← Quotient.eq_mk_iff_out,

Goal state after:
α : Sort u_1
s : Setoid α
x y : Quotient s
⊢ x = ⟦y.out⟧ ↔ x = y
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α : Sort u
β : Sort v
p : α → Prop
q : β → Prop
e : { a // p a } ≃ { b // q b }
⊢ (∃ a, p a) ↔ ∃ b, q b

Tactic:
by
  simp [← nonempty_subtype, nonempty_congr e]

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

Goal state before:
pp: α : Sort u_5
E : α → Sort u_4
⊢ IsEmpty (PSigma E) ↔ ∀ (a : α), IsEmpty (E a)

Tactic:
simp only [← not_nonempty_iff, nonempty_psigma, not_exists]

Goal state after:
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:
by intros; ext; exact DivInvMonoid.zpow_succ' _ _

Goal state after:
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) → Group (f i)
a✝ : (i : I) → f i
x✝ : I
⊢ (a✝⁻¹ * a✝) x✝ = 1 x✝

Tactic:
exact inv_mul_cancel _

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

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

Tactic:
rcases le_or_gt n m with h | h
  · simp [h]
  · rcases eq_or_ne m 0 with rfl | hm
    · simp
    · simp only [hm, h.not_ge, or_self, iff_false]
      refine not_dvd_of_pos_of_lt ?_ ?_ <;>
      grind

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

Goal state before:
pp: m n : ℕ
motive : (m : ℕ) → m ≤ n → Sort u_1
of_succ : (k : ℕ) → (h : k < n) → motive (k + 1) h → motive k ⋯
self : motive n ⋯
smn : m + 1 ≤ n
mn : m ≤ n
⊢ decreasingInduction of_succ self mn = of_succ m smn (decreasingInduction of_succ self smn)

Tactic:
Subsingleton.elim mn (Nat.le_trans (le_succ m) smn),

Goal state after:
m n : ℕ
motive : (m : ℕ) → m ≤ n → Sort u_1
of_succ : (k : ℕ) → (h : k < n) → motive (k + 1) h → motive k ⋯
self : motive n ⋯
smn : m + 1 ≤ n
mn : m ≤ n
⊢ decreasingInduction of_succ self ⋯ = of_succ m smn (decreasingInduction of_succ self smn)
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: f : ℕ → ℕ
hf : StrictMono f
m n : ℕ
⊢ f n + m ≤ f (n + m)

Tactic:
induction m with
  | zero => rw [Nat.add_zero, Nat.add_zero]
  | succ m ih =>
    rw [← Nat.add_assoc, ← Nat.add_assoc, Nat.succ_le_iff]
    exact ih.trans_lt (hf (n + m).lt_succ_self)

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a b c : α
hab : Disjoint a b
hbc : Codisjoint b c
⊢ a ⊓ ⊤ ≤ c

Tactic:
← @bot_sup_eq _ _ _ c,

Goal state after:
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a b c : α
hab : Disjoint a b
hbc : Codisjoint b c
⊢ a ⊓ ⊤ ≤ ⊥ ⊔ c
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: case pos
n : ℕ
ih :
  ∀ (m : ℕ),
    m < n →
      ∀ {f : ℕ → ℕ},
        Antitone f →
          (∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)) → f 0 = m → ∃ n, n ≤ m ∧ ∀ (m : ℕ), n ≤ m → f m = f n
f : ℕ → ℕ
hfmono : Antitone f
hfstab : ∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)
h : f 0 = n
heq : f 0 = f 1
⊢ ∃ n_1, n_1 ≤ n ∧ ∀ (m : ℕ), n_1 ≤ m → f m = f n_1

Tactic:
have flat (j : ℕ) : f j = f (j + 1) := by induction j with grind
      exact ⟨0, Nat.zero_le _, fun m _ => by induction m with grind⟩

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

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

Tactic:
rintro ⟨a, rfl⟩
    exact ⟨singleton_nonempty a, subsingleton_singleton⟩

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

Goal state before:
pp: x : Prop
⊢ x ∈ {True, False}

Tactic:
rw [mem_insert_iff, mem_singleton_iff]
    exact Classical.propComplete x

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedHeytingAlgebra α
a✝ b✝ c✝ d : α
a b c : αᵒᵈ
⊢ toDual (ofDual b ⇨ ofDual a) ≤ c ↔ a ≤ c ⊔ b

Tactic:
exact le_himp_iff

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

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
s : x ⊓ y ⊔ z = x
i : x ⊓ y ⊓ z = ⊥
| x

Tactic:
← sup_inf_sdiff x y,

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
s : x ⊓ y ⊔ z = x
i : x ⊓ y ⊓ z = ⊥
| x ⊓ y ⊔ x \ y
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : HeytingAlgebra α
a✝ b✝ : α
a b c : αᵒᵈ
⊢ toDual (ofDual b ⇨ ofDual a) ≤ c ↔ a ≤ c ⊔ b

Tactic:
exact le_himp_iff

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

Goal state before:
pp: α : Type u_1
s : Set α
a : α
ha : a ∈ s
⊢ insert a (s \ {a}) = s

Tactic:
by
  ext; simp +contextual [or_and_left, em, ha]

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

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

Tactic:
rw [inf_inf_sdiff, h, inf_inf_sdiff]

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : HeytingAlgebra β
generalizedHeytingAlgebra : GeneralizedHeytingAlgebra α := e.generalizedHeytingAlgebra
bot : Bot α := e.bot
compl : Compl α := e.compl
⊢ HeytingAlgebra α

Tactic:
apply e.injective.heytingAlgebra

Goal state after:
case le
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : HeytingAlgebra β
generalizedHeytingAlgebra : GeneralizedHeytingAlgebra α := ⋯
bot : Bot α := ⋯
compl : Compl α := ⋯
⊢ ∀ {x y : α}, e x ≤ e y ↔ x ≤ y

case lt
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : HeytingAlgebra β
generalizedHeytingAlgebra : GeneralizedHeytingAlgebra α := ⋯
bot : Bot α := ⋯
compl : Compl α := ⋯
⊢ ∀ {x y : α}, e x < e y ↔ x < y

case map_sup
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : HeytingAlgebra β
generalizedHeytingAlgebra : GeneralizedHeytingAlgebra α := ⋯
bot : Bot α := ⋯
compl : Compl α := ⋯
⊢ ∀ (a b : α), e (a ⊔ b) = e a ⊔ e b

case map_inf
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : HeytingAlgebra β
generalizedHeytingAlgebra : GeneralizedHeytingAlgebra α := ⋯
bot : Bot α := ⋯
compl : Compl α := ⋯
⊢ ∀ (a b : α), e (a ⊓ b) = e a ⊓ e b

case map_top
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : HeytingAlgebra β
generalizedHeytingAlgebra : GeneralizedHeytingAlgebra α := ⋯
bot : Bot α := ⋯
compl : Compl α := ⋯
⊢ e ⊤ = ⊤

case map_bot
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : HeytingAlgebra β
generalizedHeytingAlgebra : GeneralizedHeytingAlgebra α := ⋯
bot : Bot α := ⋯
compl : Compl α := ⋯
⊢ e ⊥ = ⊥

case map_compl
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : HeytingAlgebra β
generalizedHeytingAlgebra : GeneralizedHeytingAlgebra α := ⋯
bot : Bot α := ⋯
compl : Compl α := ⋯
⊢ ∀ (a : α), e aᶜ = (e a)ᶜ

case map_himp
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : HeytingAlgebra β
generalizedHeytingAlgebra : GeneralizedHeytingAlgebra α := ⋯
bot : Bot α := ⋯
compl : Compl α := ⋯
⊢ ∀ (a b : α), e (a ⇨ b) = e a ⇨ e b
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: case mp.inr
α : Type u_9
inst✝ : DecidableEq α
s : Set α
i j : α
hi : i ∈ s
hj : ¬j ∈ s
a : α
ha : a ∈ s
ne : a ≠ i
⊢ (swap i j) a ∈ insert j s \ {i}

Tactic:
rw [swap_apply_of_ne_of_ne ne (ne_of_mem_of_not_mem ha hj)]; exact ⟨.inr ha, ne⟩

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

Goal state before:
pp: α : Type u_1
p : α → Prop
⊢ p ⁻¹' {True} = {a | p a}

Tactic:
ext; simp

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

Goal state before:
pp: α : Type u_1
p : α → Prop
⊢ p ⁻¹' {False} = {a | ¬p a}

Tactic:
ext; simp

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

Goal state before:
pp: α : Type u_1
⊢ image id = id

Tactic:
ext; simp

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

Goal state before:
pp: case mp
α : Type u_1
s t u : Set α
⊢ val ⁻¹' t ⊆ val ⁻¹' u → val '' val ⁻¹' t ⊆ val '' val ⁻¹' u

Tactic:
exact image_mono

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Option α → β
⊢ Injective f ↔ Injective (f ∘ some) ∧ ¬f none ∈ range (f ∘ some)

Tactic:
by
  simp only [mem_range, not_exists, (· ∘ ·)]
  refine
    ⟨fun hf => ⟨hf.comp (Option.some_injective _), fun x => hf.ne <| Option.some_ne_none _⟩, ?_⟩
  rintro ⟨h_some, h_none⟩ (_ | a) (_ | b) hab
  exacts [rfl, (h_none _ hab.symm).elim, (h_none _ hab).elim, congr_arg some (h_some hab)]

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
h : Injective (image f)
x x' : α
hx : f x = f x'
⊢ f '' {x} = f '' {x'}

Tactic:
rw [image_singleton, image_singleton, hx]

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
f : ι' ≃ ι
s : Set ι'
t : (i : ι) → Set (α i)
⊢ (⇑(piCongrLeft α f).symm ⁻¹' s.pi fun i' ↦ t (f i')) = (⇑f '' s).pi t

Tactic:
ext; simp

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
N : Type u_5
F : Type u_9
inst✝³ : Mul M
inst✝² : Mul N
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
f : F
g h : ι → M
⊢ ⇑f ∘ (g * h) = ⇑f ∘ g * ⇑f ∘ h

Tactic:
ext; simp

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

Goal state before:
pp: M : Type u_4
N : Type u_5
F : Type u_9
inst✝³ : MulOne M
inst✝² : MulOne N
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
f : F
a b : M
h : a * b = 1
⊢ f 1 = 1

Tactic:
map_one

Goal state after:
M : Type u_4
N : Type u_5
F : Type u_9
inst✝³ : MulOne M
inst✝² : MulOne N
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
f : F
a b : M
h : a * b = 1
⊢ 1 = 1
Module: Mathlib.Algebra.Group.Hom.Defs

Goal state before:
pp: ι : Type u_1
G : Type u_7
H : Type u_8
F : Type u_9
inst✝³ : FunLike F G H
inst✝² : Group G
inst✝¹ : DivisionMonoid H
inst✝ : MonoidHomClass F G H
f : F
g : ι → G
⊢ ⇑f ∘ g⁻¹ = (⇑f ∘ g)⁻¹

Tactic:
ext; simp

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

Goal state before:
pp: M : Type u_4
N : Type u_5
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
e : M ≃* N
⊢ (↑e).comp ↑e.symm = MonoidHom.id N

Tactic:
ext; simp

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

Goal state before:
pp: M : Type u_4
N : Type u_5
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
e : M ≃* N
⊢ (↑e.symm).comp ↑e = MonoidHom.id M

Tactic:
ext; simp

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

Goal state before:
pp: ι : Type u_1
G : Type u_7
H : Type u_8
F : Type u_9
inst✝³ : FunLike F G H
inst✝² : Group G
inst✝¹ : DivisionMonoid H
inst✝ : MonoidHomClass F G H
f : F
g h : ι → G
⊢ ⇑f ∘ (g / h) = ⇑f ∘ g / ⇑f ∘ h

Tactic:
ext; simp

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

Goal state before:
pp: G : Type u_7
H : Type u_8
F : Type u_9
inst✝³ : FunLike F G H
inst✝² : Monoid G
inst✝¹ : Monoid H
inst✝ : MonoidHomClass F G H
f : F
a : G
⊢ f 1 = 1

Tactic:
map_one

Goal state after:
G : Type u_7
H : Type u_8
F : Type u_9
inst✝³ : FunLike F G H
inst✝² : Monoid G
inst✝¹ : Monoid H
inst✝ : MonoidHomClass F G H
f : F
a : G
⊢ 1 = 1
Module: Mathlib.Algebra.Group.Hom.Defs

Goal state before:
pp: ι : Type u_1
G : Type u_7
H : Type u_8
F : Type u_9
inst✝³ : FunLike F G H
inst✝² : Monoid G
inst✝¹ : Monoid H
inst✝ : MonoidHomClass F G H
f : F
g : ι → G
n : ℕ
⊢ ⇑f ∘ (g ^ n) = ⇑f ∘ g ^ n

Tactic:
ext; simp

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

Goal state before:
pp: M : Type u_4
N : Type u_5
F : Type u_9
inst✝⁴ : MulOne M
inst✝³ : MulOne N
inst✝² : FunLike F M N
inst✝¹ : MonoidHomClass F M N
f : F
hf : Injective ⇑f
inst✝ : IsDedekindFiniteMonoid N
a✝ b✝ : M
eq : a✝ * b✝ = 1
⊢ f (b✝ * a✝) = f 1

Tactic:
simpa [mul_eq_one_comm] using congr_arg f eq

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
f' : β → α
h : LeftInvOn f' f s
hf : SurjOn f s t
y : β
hy : y ∈ t
⊢ f' y ∈ s

Tactic:
let ⟨x, hs, hx⟩ := hf hy
  rwa [← hx, h hs]

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionCommMonoid α
⊢ invMonoidHom.comp invMonoidHom = MonoidHom.id α

Tactic:
ext; simp

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

Goal state before:
pp: F : Type u_7
G : Type u_8
H : Type u_9
inst✝³ : Group G
inst✝² : MulOneClass H
inst✝¹ : FunLike F G H
inst✝ : MonoidHomClass F G H
f : F
h : ∀ (a : G), f a = 1 → a = 1
x y : G
hxy : f x = f y
⊢ f 1 = 1

Tactic:
map_one

Goal state after:
F : Type u_7
G : Type u_8
H : Type u_9
inst✝³ : Group G
inst✝² : MulOneClass H
inst✝¹ : FunLike F G H
inst✝ : MonoidHomClass F G H
f : F
h : ∀ (a : G), f a = 1 → a = 1
x y : G
hxy : f x = f y
⊢ 1 = 1
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
a : M
⊢ (fun x ↦ a * x)^[0] = fun x ↦ a ^ 0 * x

Tactic:
ext; simp

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
a : M
⊢ (fun x ↦ x * a)^[0] = fun x ↦ x * a ^ 0

Tactic:
ext; simp

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
k : ℕ
⊢ (fun x ↦ x ^ k)^[0] = fun x ↦ x ^ k ^ 0

Tactic:
ext; simp

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) = f 1

Tactic:
npow,

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₁
⊢ f x ^ 0 = f 1
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
n : ℕ
x : M₁
⊢ f (x ^ (n + 1)) = f (x ^ n * x)

Tactic:
npow,

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
n : ℕ
x : M₁
⊢ f x ^ (n + 1) = f (x ^ n * x)
Module: Mathlib.Algebra.Group.Basic

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

Tactic:
rw [div_eq_mul_inv, eq_mul_inv_iff_mul_eq]

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

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

Tactic:
by simp only [← Int.natCast_succ, zpow_natCast, pow_succ]

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a : G
n : ℕ
⊢ a ^ (↑n - 1) = a ^ n / a

Tactic:
by
  simpa [div_eq_mul_inv] using zpow_sub a n 1

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

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

Tactic:
u.mul_inv

Goal state after:
α : Type u
inst✝ : Monoid α
u : αˣ
a : α
h : ↑u = a
⊢ 1 = 1
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
⊢ c (f ^ 0) = (c f)^[0]

Tactic:
rw [pow_zero, h1]
    rfl

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
M✝ : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N✝ : Type u_8
N₁ : Type u_9
N₂ : Type u_10
N₃ : Type u_11
P✝ : Type u_12
Q✝ : Type u_13
G : Type u_14
H : Type u_15
inst✝² : EquivLike F α β
M : Type u_16
N : Type u_17
P : Type u_18
Q : Type u_19
inst✝¹ : Mul P
inst✝ : Mul Q
f : M ≃ N
g : P ≃* Q
h : M → P
⊢ (fun k m ↦ g.symm (k (f m))) ((fun h n ↦ g (h (f.symm n))) h) = h

Tactic:
ext; simp

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
M✝ : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N✝ : Type u_8
N₁ : Type u_9
N₂ : Type u_10
N₃ : Type u_11
P✝ : Type u_12
Q✝ : Type u_13
G : Type u_14
H : Type u_15
inst✝² : EquivLike F α β
M : Type u_16
N : Type u_17
P : Type u_18
Q : Type u_19
inst✝¹ : Mul P
inst✝ : Mul Q
f : M ≃ N
g : P ≃* Q
k : N → Q
⊢ (fun h n ↦ g (h (f.symm n))) ((fun k m ↦ g.symm (k (f m))) k) = k

Tactic:
ext; simp

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
M✝ : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N✝ : Type u_8
N₁ : Type u_9
N₂ : Type u_10
N₃ : Type u_11
P✝ : Type u_12
Q✝ : Type u_13
G : Type u_14
H : Type u_15
inst✝² : EquivLike F α β
M : Type u_16
N : Type u_17
P : Type u_18
Q : Type u_19
inst✝¹ : Mul P
inst✝ : Mul Q
f : M ≃ N
g : P ≃* Q
h k : M → P
⊢ (fun n ↦ g ((h * k) (f.symm n))) = (fun n ↦ g (h (f.symm n))) * fun n ↦ g (k (f.symm n))

Tactic:
ext; simp

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N : Type u_8
N₁ : Type u_9
N₂ : Type u_10
N₃ : Type u_11
P : Type u_12
Q : Type u_13
G : Type u_14
H : Type u_15
inst✝⁸ : EquivLike F α β
inst✝⁷ : MulOneClass M
inst✝⁶ : MulOneClass M₁
inst✝⁵ : MulOneClass M₂
inst✝⁴ : MulOneClass M₃
inst✝³ : Monoid N
inst✝² : Monoid N₁
inst✝¹ : Monoid N₂
inst✝ : Monoid N₃
e : M₁ ≃* M₂
f : M₁ →* N
⊢ (fun f ↦ f.comp e.toMonoidHom) ((fun f ↦ f.comp e.symm.toMonoidHom) f) = f

Tactic:
ext; simp

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N : Type u_8
N₁ : Type u_9
N₂ : Type u_10
N₃ : Type u_11
P : Type u_12
Q : Type u_13
G : Type u_14
H : Type u_15
inst✝⁸ : EquivLike F α β
inst✝⁷ : MulOneClass M
inst✝⁶ : MulOneClass M₁
inst✝⁵ : MulOneClass M₂
inst✝⁴ : MulOneClass M₃
inst✝³ : Monoid N
inst✝² : Monoid N₁
inst✝¹ : Monoid N₂
inst✝ : Monoid N₃
e : M₁ ≃* M₂
f : M₂ →* N
⊢ (fun f ↦ f.comp e.symm.toMonoidHom) ((fun f ↦ f.comp e.toMonoidHom) f) = f

Tactic:
ext; simp

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N : Type u_8
N₁ : Type u_9
N₂ : Type u_10
N₃ : Type u_11
P : Type u_12
Q : Type u_13
G : Type u_14
H : Type u_15
inst✝⁸ : EquivLike F α β
inst✝⁷ : MulOneClass M
inst✝⁶ : MulOneClass M₁
inst✝⁵ : MulOneClass M₂
inst✝⁴ : MulOneClass M₃
inst✝³ : Monoid N
inst✝² : Monoid N₁
inst✝¹ : Monoid N₂
inst✝ : Monoid N₃
e : N₁ ≃* N₂
f : M →* N₁
⊢ e.symm.toMonoidHom.comp (e.toMonoidHom.comp f) = f

Tactic:
ext; simp

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N : Type u_8
N₁ : Type u_9
N₂ : Type u_10
N₃ : Type u_11
P : Type u_12
Q : Type u_13
G : Type u_14
H : Type u_15
inst✝⁸ : EquivLike F α β
inst✝⁷ : MulOneClass M
inst✝⁶ : MulOneClass M₁
inst✝⁵ : MulOneClass M₂
inst✝⁴ : MulOneClass M₃
inst✝³ : Monoid N
inst✝² : Monoid N₁
inst✝¹ : Monoid N₂
inst✝ : Monoid N₃
e : N₁ ≃* N₂
f : M →* N₂
⊢ e.toMonoidHom.comp (e.symm.toMonoidHom.comp f) = f

Tactic:
ext; simp

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N : Type u_8
N₁ : Type u_9
N₂ : Type u_10
N₃ : Type u_11
P : Type u_12
Q : Type u_13
G : Type u_14
H : Type u_15
inst✝⁸ : EquivLike F α β
inst✝⁷ : MulOneClass M
inst✝⁶ : MulOneClass M₁
inst✝⁵ : MulOneClass M₂
inst✝⁴ : MulOneClass M₃
inst✝³ : CommMonoid N
inst✝² : CommMonoid N₁
inst✝¹ : CommMonoid N₂
inst✝ : CommMonoid N₃
e : M₁ ≃* M₂
f g : M₁ →* N
⊢ e.monoidHomCongrLeftEquiv.toFun (f * g) = e.monoidHomCongrLeftEquiv.toFun f * e.monoidHomCongrLeftEquiv.toFun g

Tactic:
ext; simp

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N : Type u_8
N₁ : Type u_9
N₂ : Type u_10
N₃ : Type u_11
P : Type u_12
Q : Type u_13
G : Type u_14
H : Type u_15
inst✝⁸ : EquivLike F α β
inst✝⁷ : MulOneClass M
inst✝⁶ : MulOneClass M₁
inst✝⁵ : MulOneClass M₂
inst✝⁴ : MulOneClass M₃
inst✝³ : CommMonoid N
inst✝² : CommMonoid N₁
inst✝¹ : CommMonoid N₂
inst✝ : CommMonoid N₃
e : N₁ ≃* N₂
f g : M →* N₁
⊢ e.monoidHomCongrRightEquiv.toFun (f * g) = e.monoidHomCongrRightEquiv.toFun f * e.monoidHomCongrRightEquiv.toFun g

Tactic:
ext; simp

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

Goal state before:
pp: case fst
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : Group G
inst✝ : Group H
x✝ : G × H
⊢ (x✝⁻¹ * x✝).1 = 1.1

Tactic:
exact inv_mul_cancel _

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

Goal state before:
pp: case snd
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : Group G
inst✝ : Group H
x✝ : G × H
⊢ (x✝⁻¹ * x✝).2 = 1.2

Tactic:
exact inv_mul_cancel _

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

Goal state before:
pp: M₀ : Type u_2
inst✝¹ : Mul M₀
inst✝ : Zero M₀
⊢ (∀ (x : M₀), x ≠ 0 → IsLeftRegular x ∧ IsRightRegular x) ↔ ∀ {a : M₀}, a ≠ 0 → IsRegular a

Tactic:
exact forall₂_congr fun _ _ ↦ isRegular_iff.symm

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

Goal state before:
pp: M₀ : Type u_1
M₀' : Type u_3
inst✝⁴ : Mul M₀
inst✝³ : Zero M₀
inst✝² : Mul M₀'
inst✝¹ : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst✝ : NoZeroDivisors M₀'
a b : M₀
H : a * b = 0
⊢ f 0 = 0

Tactic:
zero

Goal state after:
M₀ : Type u_1
M₀' : Type u_3
inst✝⁴ : Mul M₀
inst✝³ : Zero M₀
inst✝² : Mul M₀'
inst✝¹ : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst✝ : NoZeroDivisors M₀'
a b : M₀
H : a * b = 0
⊢ 0 = 0