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

Goal state before:
pp: S : Type u_1
inst✝ : Semigroup S
a b x y z : S
ha : SemiconjBy a y z
hb : SemiconjBy b x y
⊢ z * a * b = z * (a * b)

Tactic:
mul_assoc

Goal state after:
S : Type u_1
inst✝ : Semigroup S
a b x y z : S
ha : SemiconjBy a y z
hb : SemiconjBy b x y
⊢ z * (a * b) = z * (a * b)
Module: Mathlib.Algebra.Group.Semiconj.Defs

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

Tactic:
mul_assoc

Goal state after:
G : Type u_3
inst✝ : Group G
a x y b : G
⊢ b * a * (x * b⁻¹) = b * y * a * b⁻¹ ↔ a * x = y * a
Module: Mathlib.Algebra.Group.Semiconj.Defs

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a x y b : G
⊢ b * a * (x * b⁻¹) = b * y * a * b⁻¹ ↔ a * x = y * a

Tactic:
mul_assoc

Goal state after:
G : Type u_3
inst✝ : Group G
a x y b : G
⊢ b * (a * (x * b⁻¹)) = b * y * a * b⁻¹ ↔ a * x = y * a
Module: Mathlib.Algebra.Group.Semiconj.Defs

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a x y b : G
⊢ b * (a * (x * b⁻¹)) = b * y * a * b⁻¹ ↔ a * x = y * a

Tactic:
mul_assoc

Goal state after:
G : Type u_3
inst✝ : Group G
a x y b : G
⊢ b * (a * (x * b⁻¹)) = b * y * (a * b⁻¹) ↔ a * x = y * a
Module: Mathlib.Algebra.Group.Semiconj.Defs

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a x y b : G
⊢ b * (a * (x * b⁻¹)) = b * y * (a * b⁻¹) ↔ a * x = y * a

Tactic:
mul_assoc

Goal state after:
G : Type u_3
inst✝ : Group G
a x y b : G
⊢ b * (a * (x * b⁻¹)) = b * (y * (a * b⁻¹)) ↔ a * x = y * a
Module: Mathlib.Algebra.Group.Semiconj.Defs

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a x y b : G
⊢ b * (a * (x * b⁻¹)) = b * (y * (a * b⁻¹)) ↔ a * x = y * a

Tactic:
mul_assoc

Goal state after:
G : Type u_3
inst✝ : Group G
a x y b : G
⊢ b * (a * (x * b⁻¹)) = b * (y * (a * b⁻¹)) ↔ a * x = y * a
Module: Mathlib.Algebra.Group.Defs

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

Tactic:
unfold go

Goal state after:
M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
k : ℕ
m n : M
⊢ Nat.binaryRec (motive := fun x ↦ M → M → M) (fun y x ↦ y) (fun bn _n fn y x ↦ fn (bif bn then y * x else y) (x * x))
      (k + 1) m n =
    m * npowRec' (k + 1) n
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: case bit.true
M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
k k' : ℕ
k'0 : k' ≠ 0
ih :
  ∀ (m n : M),
    k' ≠ 0 →
      Nat.binaryRec (motive := fun x ↦ M → M → M) (fun y x ↦ y)
          (fun bn _n fn y x ↦ fn (bif bn then y * x else y) (x * x)) k' m n =
        m * npowRec' k' n
m n : M
hk : Nat.bit true k' ≠ 0
⊢ m * n * npowRec' (2 * k') n = m * (n * npowRec' (2 * k') n)

Tactic:
mul_assoc

Goal state after:
case bit.true
M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
k k' : ℕ
k'0 : k' ≠ 0
ih :
  ∀ (m n : M),
    k' ≠ 0 →
      Nat.binaryRec (motive := fun x ↦ M → M → M) (fun y x ↦ y)
          (fun bn _n fn y x ↦ fn (bif bn then y * x else y) (x * x)) k' m n =
        m * npowRec' k' n
m n : M
hk : Nat.bit true k' ≠ 0
⊢ m * (n * npowRec' (2 * k') n) = m * (n * npowRec' (2 * k') n)
Module: Mathlib.Algebra.Group.Defs

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

Tactic:
mul_assoc

Goal state after:
M : Type u_2
inst✝ : Monoid M
a : M
n : ℕ
⊢ a * (a ^ n * a) = a * (a ^ n * a)
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: G : Type u_1
inst✝ : DivInvMonoid G
a b c : G
⊢ a * b * c⁻¹ = a * (b * c⁻¹)

Tactic:
mul_assoc

Goal state after:
G : Type u_1
inst✝ : DivInvMonoid G
a b c : G
⊢ a * (b * c⁻¹) = a * (b * c⁻¹)
Module: Mathlib.Logic.Nontrivial.Defs

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝ : Nontrivial α
f : α → β
hf : Injective f
y : β
x₁ x₂ : α
hx : x₁ ≠ x₂
h : f x₂ = y
⊢ ∃ x, f x ≠ y

Tactic:
exact ⟨x₁, (hf.ne_iff' h).2 hx⟩

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

Goal state before:
pp: α : Sort u
β : α → Sort v
inst✝ : DecidableEq α
f : (a : α) → β a
a' : α
v v' : β a'
h : update f a' v = update f a' v'
⊢ v = v'

Tactic:
have := congr_fun h a'
  rwa [update_self, update_self] at this

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

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

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

Tactic:
· obtain ⟨c, rfl⟩ := h₂
      rw [h₁₂.extend_apply]
      exact (h₂₃.comp h₁₂).extend_apply _ _ _

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

Goal state before:
pp: case tail.single
α : Type u_1
r : α → α → Prop
a✝² b✝¹ c : α
h : ∀ (a b c : α), r a b → r a c → ∃ d, ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a✝² c
d e : α
a✝¹ : ReflTransGen r a✝² d
hde : r d e
b✝ f b : α
a✝ : ReflTransGen r d f
hfb : r f b
a : α
hea : ReflTransGen r e a
hfa : r f a
⊢ ∃ a, ReflTransGen r e a ∧ ReflGen r b a

Tactic:
rcases h _ _ _ hfb hfa with ⟨c, hbc, hac⟩
          exact ⟨c, hea.trans hac, hbc⟩

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

Goal state before:
pp: case succ
α : Type u
f : α → α
g : ℕ → α → α
H : ∀ (n : ℕ), Semiconj f (g n) (g (n + 1))
n : ℕ
ihn : ∀ (k : ℕ), Semiconj f^[n] (g k) (g (n + k))
k : ℕ
⊢ Semiconj f^[n + 1] (g k) (g (n + (k + 1)))

Tactic:
exact (H k).trans (ihn (k + 1))

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

Goal state before:
pp: M : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
inst✝³ : SMul M α
inst✝² : SMul M β
inst✝¹ : SMul α β
inst✝ : IsScalarTower M α β
g : N → M
this : SMul N α
⊢ Sort ?u.25

Tactic:
haveI := comp β g

Goal state after:
M : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
inst✝³ : SMul M α
inst✝² : SMul M β
inst✝¹ : SMul α β
inst✝ : IsScalarTower M α β
g : N → M
this✝ : SMul N α
this : SMul N β
⊢ Sort ?u.25
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: M : Type u_9
N : Type u_10
inst✝¹ : Monoid N
inst✝ : SMul M N
H : ∀ (x : M) (y : N), y * x • 1 = x • y
x : M
y z : N
⊢ y * z * x • 1 = y * (z * x • 1)

Tactic:
mul_assoc

Goal state after:
M : Type u_9
N : Type u_10
inst✝¹ : Monoid N
inst✝ : SMul M N
H : ∀ (x : M) (y : N), y * x • 1 = x • y
x : M
y z : N
⊢ y * (z * x • 1) = y * (z * x • 1)
Module: Mathlib.Logic.IsEmpty.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_2
⊢ ¬Nonempty (α → β) ↔ ¬(IsEmpty α ∨ Nonempty β)

Tactic:
not_or,

Goal state after:
α : Sort u_1
β : Sort u_2
⊢ ¬Nonempty (α → β) ↔ ¬IsEmpty α ∧ ¬Nonempty β
Module: Mathlib.Data.Prod.Basic

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

Tactic:
simp [*, Prod.map_comp_map]

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

Goal state before:
pp: case succ
α : Type u_1
β : Type u_2
f : α → α
g : β → β
n✝ : ℕ
a✝ : (map f g)^[n✝] = map f^[n✝] g^[n✝]
⊢ (map f g)^[n✝ + 1] = map f^[n✝ + 1] g^[n✝ + 1]

Tactic:
simp [*, Prod.map_comp_map]

Goal state after:
Module: Mathlib.Order.Basic

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

Tactic:
by
  have h := LinearOrder.compare_eq_compareOfLessAndEq (f a) (f b)
  simp only [h, compareOfLessAndEq]
  split_ifs <;> try (first | rfl | contradiction)
  · have : ¬ f a = f b := by rename_i h; exact inj.ne h
    contradiction
  · grind

Goal state after:
Module: Mathlib.Order.Compare

Goal state before:
pp: case inl
α : 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'
hab✝ : a < b
hab : lt.Compares a b
⊢ o.Compares a b

Tactic:
ho.inj (h hab)

Goal state after:
case inl
α : 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'
hab✝ : a < b
hab : lt.Compares a b
⊢ lt.Compares a b
Module: Mathlib.Order.Compare

Goal state before:
pp: case inr.inl
α : 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'
hab✝ : a = b
hab : eq.Compares a b
⊢ o.Compares a b

Tactic:
ho.inj (h hab)

Goal state after:
case inr.inl
α : 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'
hab✝ : a = b
hab : eq.Compares a b
⊢ eq.Compares a b
Module: Mathlib.Order.Compare

Goal state before:
pp: case inr.inr
α : 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'
hab✝ : b < a
hab : gt.Compares a b
⊢ o.Compares a b

Tactic:
ho.inj (h hab)

Goal state after:
case inr.inr
α : 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'
hab✝ : b < a
hab : gt.Compares a b
⊢ gt.Compares a b
Module: Mathlib.Order.Heyting.Basic

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

Tactic:
inf_himp,

Goal state after:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b : α
⊢ a ⊓ b = b ⊓ a
Module: Mathlib.Order.Heyting.Basic

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

Tactic:
by
  simpa using @himp_le_himp_himp_himp

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

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

Tactic:
rw [← sdiff_inf_self_left (b := c)]

Goal state after:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c : α
hinf : a ⊓ c ≤ b
hsup : b ≤ a ⊔ c
⊢ a \ b ≤ a \ (a ⊓ c)
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:
by simpa using (congr_arg e.symm h).symm

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedHeytingAlgebra β
lattice : Lattice α := e.lattice
⊢ GeneralizedHeytingAlgebra α

Tactic:
let top := e.top

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedHeytingAlgebra β
lattice : Lattice α := e.lattice
top : Top α := e.top
⊢ GeneralizedHeytingAlgebra α
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CoheytingAlgebra β
generalizedCoheytingAlgebra : GeneralizedCoheytingAlgebra α := e.generalizedCoheytingAlgebra
⊢ CoheytingAlgebra α

Tactic:
let top := e.top

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CoheytingAlgebra β
generalizedCoheytingAlgebra : GeneralizedCoheytingAlgebra α := e.generalizedCoheytingAlgebra
top : Top α := e.top
⊢ CoheytingAlgebra α
Module: Mathlib.Logic.Equiv.Sum

Goal state before:
pp: α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
ι : Type ?u.20
α : ι → Type u_9
β : ι → Type u_10
p : (i : ι) × (α i ⊕ β i)
⊢ Sum.elim (Sigma.map id fun x ↦ inl) (Sigma.map id fun x ↦ inr)
      ((fun p ↦ Sum.map (Sigma.mk p.fst) (Sigma.mk p.fst) p.snd) p) =
    p

Tactic:
rcases p with ⟨i, a | b⟩ <;> rfl

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

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

Tactic:
simp_rw [inf_comm _ c, inf_sdiff_distrib_left]

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

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

Tactic:
by
  unfold swapCore; split_ifs <;> grind

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

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

Tactic:
by
  unfold swapCore; split_ifs <;> grind

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

Goal state before:
pp: α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : BooleanAlgebra β
⊢ BooleanAlgebra α

Tactic:
let top := e.top

Goal state after:
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : BooleanAlgebra β
top : Top α := e.top
⊢ BooleanAlgebra α
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
inst✝ : BooleanAlgebra α
t : α
s : Set α
⊢ t ∈ compl '' s ↔ tᶜ ∈ s

Tactic:
by
  simp [← preimage_compl_eq_image_compl]

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

Goal state before:
pp: α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst✝¹ : (j : α) → Decidable (j ∈ s)
inst✝ : (i : α) → Decidable (i ∈ sᶜ)
x : α
hx : x ∈ s
⊢ sᶜ.piecewise f g x = s.piecewise g f x

Tactic:
by simp [hx]

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

Goal state before:
pp: α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst✝¹ : (j : α) → Decidable (j ∈ s)
inst✝ : (i : α) → Decidable (i ∈ sᶜ)
x : α
hx : ¬x ∈ s
⊢ sᶜ.piecewise f g x = s.piecewise g f x

Tactic:
by simp [hx]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s s₁ s₂ : Set α
f : α → β
h : InjOn f s
h₁ : s₁ ⊆ s
h₂ : s₂ ⊆ s
h' : f '' s₁ ⊆ f '' s₂
⊢ s₁ ⊆ s₂

Tactic:
← h.preimage_image_inter h₁,

Goal state after:
α : Type u_1
β : Type u_2
s s₁ s₂ : Set α
f : α → β
h : InjOn f s
h₁ : s₁ ⊆ s
h₂ : s₂ ⊆ s
h' : f '' s₁ ⊆ f '' s₂
⊢ f ⁻¹' f '' s₁ ∩ s ⊆ s₂
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f₁ f₂ : α → β
h : SurjOn f₁ s t
H : EqOn f₁ f₂ s
⊢ SurjOn f₂ s t

Tactic:
SurjOn,

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f₁ f₂ : α → β
h : SurjOn f₁ s t
H : EqOn f₁ f₂ s
⊢ t ⊆ f₂ '' s
Module: Mathlib.Data.Set.Function

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

Tactic:
SurjOn,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
f : α → β
hf : SurjOn f s t
g : β → γ
⊢ g '' t ⊆ g ∘ f '' s
Module: Mathlib.Data.Set.Function

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

Tactic:
SurjOn,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
s : Set β
t : Set γ
hf : Surjective f
hg : SurjOn g s t
⊢ t ⊆ g ∘ f '' f ⁻¹' s
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
⊢ SurjOn f univ univ ↔ Surjective f

Tactic:
simp [Surjective, SurjOn, subset_def]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : ¬a ∈ s
hfa : ¬f a ∈ t
h : BijOn f (insert a s) (insert (f a) t)
this : f '' s \ {f a} = t
x : α
hx : x ∈ s
⊢ x ∈ insert a s

Tactic:
by simp [hx]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : ¬a ∈ s
hfa : ¬f a ∈ t
h : BijOn f s t
⊢ InjOn f ({a} ∪ s)

Tactic:
simp only [singleton_union, injOn_insert fun x ↦ (hfa (h.mapsTo x)), h.injOn, mem_image,
      not_exists, not_and, true_and]

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : ¬a ∈ s
hfa : ¬f a ∈ t
h : BijOn f s t
⊢ ∀ (x : α), x ∈ s → ¬f x = f a
Module: Mathlib.Algebra.Group.Basic

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

Tactic:
mul_assoc

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

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

Tactic:
mul_assoc

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

Goal state before:
pp: M₁ : Type u_1
M₂ : Type u_2
inst✝¹ : Mul M₁
inst✝ : Semigroup M₂
f : M₁ → M₂
hf : Injective f
mul : ∀ (x y : M₁), f (x * y) = f x * f y
x y z : M₁
⊢ f x * f y * f z = f x * (f y * f z)

Tactic:
mul_assoc

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

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

Tactic:
by 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
⊢ a * (b * (b⁻¹ * c)) = a * c

Tactic:
← mul_assoc b,

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝² : Monoid β
p r : α → α → Prop
inst✝¹ : Std.Total r
f : α → α → β
inst✝ : Std.Symm p
hf_swap : ∀ {a b : α}, p a b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a b → p b c → p a c → f a c = f a b * f b c
a b✝ c✝ : α
pab✝ : p a b✝
pbc✝ : p b✝ c✝
pac✝ : p a c✝
b c : α
rbc : r b c
pab : p a b
pbc : p b c
pac : p a c
rba : r b a
⊢ f a b * f b a * f a c = f a b * f b c

Tactic:
mul_assoc

Goal state after:
case inr
α : Type u_1
β : Type u_2
inst✝² : Monoid β
p r : α → α → Prop
inst✝¹ : Std.Total r
f : α → α → β
inst✝ : Std.Symm p
hf_swap : ∀ {a b : α}, p a b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a b → p b c → p a c → f a c = f a b * f b c
a b✝ c✝ : α
pab✝ : p a b✝
pbc✝ : p b✝ c✝
pac✝ : p a c✝
b c : α
rbc : r b c
pab : p a b
pbc : p b c
pac : p a c
rba : r b a
⊢ f a b * (f b a * f a c) = f a b * f b c
Module: Mathlib.Algebra.Group.Units.Defs

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
inst✝ : IsDedekindFiniteMonoid M
x y : M
hu : IsUnit (x * y)
z : M
hz : z * (x * y) = 1
⊢ z * x * y = 1

Tactic:
mul_assoc

Goal state after:
M : Type u_1
inst✝¹ : Monoid M
inst✝ : IsDedekindFiniteMonoid M
x y : M
hu : IsUnit (x * y)
z : M
hz : z * (x * y) = 1
⊢ z * (x * y) = 1
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✝ : IsLeftCancelMulZero M₀'
a✝ : M₀
Hne : a✝ ≠ 0
x✝¹ x✝ : M₀
He : (fun x ↦ a✝ * x) x✝¹ = (fun x ↦ a✝ * x) x✝
⊢ x✝¹ = x✝

Tactic:
have := congr_arg f He
    rw [mul, mul] at this
    exact hf (mul_left_cancel₀ (fun Hfa => Hne <| hf <| by rw [Hfa, zero]) this)

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

Goal state before:
pp: α : Type u_3
inst✝ : MonoidWithZero α
h : ∀ (a : α), a ≠ 0 → ∃ b, b * a = 1
a : α
ha : a ≠ 0
h✝ : Nontrivial α
b : α
hb : b * a = 1
c : α
hc : c * b = 1
| c * (b * (a * b))

Tactic:
← mul_assoc b,

Goal state after:
α : Type u_3
inst✝ : MonoidWithZero α
h : ∀ (a : α), a ≠ 0 → ∃ b, b * a = 1
a : α
ha : a ≠ 0
h✝ : Nontrivial α
b : α
hb : b * a = 1
c : α
hc : c * b = 1
| c * (b * a * b)
Module: Mathlib.Algebra.GroupWithZero.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
M₀ : Type u_6
inst✝³ : MulZeroOneClass α
inst✝² : MulZeroOneClass β
inst✝¹ : MulZeroOneClass γ
inst✝ : MulZeroOneClass δ
f g : α →*₀ β
h : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g
⊢ f = g

Tactic:
by obtain ⟨⟨_, _⟩, _⟩ := f; obtain ⟨⟨_, _⟩, _⟩ := g; congr

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₀
hb : b ≠ 0
⊢ a * b = b ↔ a = 1

Tactic:
by
  rw [Iff.comm, ← mul_left_inj' hb, one_mul]

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

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoidWithOne R
n : ℕ
⊢ ↑(1 + n) = 1 + ↑n

Tactic:
by
  rw [Nat.cast_add, Nat.cast_one]

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

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

Tactic:
rw [cast_negSucc, ← e, Nat.cast_sub <| _root_.le_of_lt <| Nat.lt_of_sub_eq_succ e, neg_sub]

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

Goal state before:
pp: m n : ℤ
⊢ (m % n).gcd n = m.gcd n

Tactic:
conv_rhs => rw [← m.emod_add_mul_ediv n, gcd_add_mul_left_left]

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

Goal state before:
pp: case h
α : Type u_1
inst✝ : Semigroup α
b a d : α
⊢ a * (b * d) = a * b * d

Tactic:
mul_assoc

Goal state after:
case h
α : Type u_1
inst✝ : Semigroup α
b a d : α
⊢ a * (b * d) = a * (b * d)
Module: Mathlib.Algebra.Divisibility.Basic

Goal state before:
pp: case h
α : Type u_1
inst✝ : Semigroup α
b a d : α
⊢ d * b * a = d * (b * a)

Tactic:
mul_assoc

Goal state after:
case h
α : Type u_1
inst✝ : Semigroup α
b a d : α
⊢ d * (b * a) = d * (b * a)
Module: Mathlib.Algebra.Group.Hom.Instances

Goal state before:
pp: M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
mM : MulOneClass M
mN : MulOneClass N
mP : CommMonoid P
f : M →* N →* P
y : N
x₁ x₂ : M
⊢ (f (x₁ * x₂)) y = (f x₁) y * (f x₂) y

Tactic:
by simp [f.map_mul, mul_apply]

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

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

Tactic:
rw [mul_neg, mul_one]

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
u : Mˣ
a : M
⊢ ↑u⁻¹ * a * ↑u = a ↔ ↑u⁻¹ * (a * ↑u) = a

Tactic:
mul_assoc

Goal state after:
M : Type u_1
inst✝ : Monoid M
u : Mˣ
a : M
⊢ ↑u⁻¹ * (a * ↑u) = a ↔ ↑u⁻¹ * (a * ↑u) = a
Module: Mathlib.Algebra.Group.Commute.Units

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
u : Mˣ
a : M
⊢ Commute (↑u) a ↔ ↑u⁻¹ * (a * ↑u) = a

Tactic:
rw [u.commute_iff_inv_mul_cancel, mul_assoc]

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
u : Mˣ
a : M
⊢ ↑u * a * ↑u⁻¹ = a ↔ ↑u * (a * ↑u⁻¹) = a

Tactic:
mul_assoc

Goal state after:
M : Type u_1
inst✝ : Monoid M
u : Mˣ
a : M
⊢ ↑u * (a * ↑u⁻¹) = a ↔ ↑u * (a * ↑u⁻¹) = a
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: case more
R : Type u_4
inst✝ : AddMonoidWithOne R
h : 2 = 0
n : ℕ
a✝¹ : (Even n → ↑n = 0) ∧ (Odd n → ↑n = 1)
a✝ : (Even (n + 1) → ↑(n + 1) = 0) ∧ (Odd (n + 1) → ↑(n + 1) = 1)
⊢ (Even (n + 2) → ↑(n + 2) = 0) ∧ (Odd (n + 2) → ↑(n + 2) = 1)

Tactic:
simpa [add_assoc, Nat.even_add_one, Nat.odd_add_one, h]

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic

Goal state before:
pp: α : Type u_1
inst✝² : LE α
inst✝¹ : Semigroup α
inst✝ : MulLeftMono α
a b : α
h : MulLECancellable (a * b)
c d : α
hcd : b * c ≤ b * d
⊢ a * (b * c) ≤ a * b * d

Tactic:
mul_assoc

Goal state after:
α : Type u_1
inst✝² : LE α
inst✝¹ : Semigroup α
inst✝ : MulLeftMono α
a b : α
h : MulLECancellable (a * b)
c d : α
hcd : b * c ≤ b * d
⊢ a * (b * c) ≤ a * (b * d)
Module: Mathlib.Algebra.Order.Monoid.Defs

Goal state before:
pp: α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : LinearOrder α
hmul : ∀ (a b c : α), b < c → a * b < a * c
a b c : α
h : a * b ≤ a * c
⊢ b ≤ c

Tactic:
contrapose! h
    exact hmul _ _ _ h

Goal state after: