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
⊢ a * (b * x) = z * (a * b)

Tactic:
hb.eq,

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
⊢ a * (y * b) = z * (a * b)
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 * (npowRec' (2 * k') n * n)

Tactic:
← npowRec'_mul_comm (by lia),

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: G : Type u_1
inst✝ : Group G
a b : G
⊢ a * a⁻¹ * b = b

Tactic:
mul_inv_cancel,

Goal state after:
G : Type u_1
inst✝ : Group G
a b : G
⊢ 1 * b = b
Module: Mathlib.Algebra.Group.Defs

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

Tactic:
mul_inv_cancel,

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

Goal state before:
pp: p : Prop → Prop
x✝ : p False ∧ p True
h : Prop
h₁ : p False
h₂ : p True
⊢ p h

Tactic:
by by_cases H : h <;> simpa only [H]

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

Goal state before:
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' : α₃ → γ
a : α₃
h₃ : ¬∃ b, f₂₃ b = a
⊢ extend (f₂₃ ∘ f₁₂) g e' a = extend f₂₃ (extend f₁₂ g (e' ∘ f₂₃)) e' a

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

Goal state before:
pp: α : Sort u_1
r : α → α → Prop
inst✝ : Symm r
⊢ (∀ (a : α), ∃! b, r a b) ↔ ∃ f, Involutive f ∧ ∀ {a b : α}, r a b ↔ f a = b

Tactic:
simp [Std.Symm.forall_existsUnique_iff', funext_iff]

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

Goal state after:
G : Type u_3
α : Type u_5
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a : α
⊢ 1 • a = a
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 b : α
h : g • a = b
⊢ a = g⁻¹ • b

Tactic:
rw [← h, inv_smul_smul]

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

Goal state before:
pp: G : Type u_3
H : Type u_4
inst✝⁴ : Group G
inst✝³ : Group H
inst✝² : MulAction G H
inst✝¹ : SMulCommClass G H H
inst✝ : IsScalarTower G H H
g : G
a : H
⊢ (g * g⁻¹) • (a * a⁻¹) = 1

Tactic:
mul_inv_cancel,

Goal state after:
G : Type u_3
H : Type u_4
inst✝⁴ : Group G
inst✝³ : Group H
inst✝² : MulAction G H
inst✝¹ : SMulCommClass G H H
inst✝ : IsScalarTower G H H
g : G
a : H
⊢ 1 • (a * a⁻¹) = 1
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: G : Type u_3
H : Type u_4
inst✝⁴ : Group G
inst✝³ : Group H
inst✝² : MulAction G H
inst✝¹ : SMulCommClass G H H
inst✝ : IsScalarTower G H H
g : G
a : H
⊢ 1 • (a * a⁻¹) = 1

Tactic:
mul_inv_cancel,

Goal state after:
G : Type u_3
H : Type u_4
inst✝⁴ : Group G
inst✝³ : Group H
inst✝² : MulAction G H
inst✝¹ : SMulCommClass G H H
inst✝ : IsScalarTower G H H
g : G
a : H
⊢ 1 • 1 = 1
Module: Mathlib.Data.Bool.Basic

Goal state before:
pp: f : Bool → Bool
x : Bool
⊢ f (f (f x)) = f x

Tactic:
cases h₁ : f true <;> cases h₂ : f false

Goal state after:
case false.false
f : Bool → Bool
x : Bool
h₁ : f true = false
h₂ : f false = false
⊢ f (f (f x)) = f x

case false.true
f : Bool → Bool
x : Bool
h₁ : f true = false
h₂ : f false = true
⊢ f (f (f x)) = f x

case true.false
f : Bool → Bool
x : Bool
h₁ : f true = true
h₂ : f false = false
⊢ f (f (f x)) = f x

case true.true
f : Bool → Bool
x : Bool
h₁ : f true = true
h₂ : f false = true
⊢ f (f (f x)) = f x
Module: Mathlib.Data.Nat.Init

Goal state before:
pp: a b c d e m n k : ℕ
p : ℕ → Prop
P : ℕ → Sort u_1
h : (k : ℕ) → k < n → m ≤ k → P (k + 1) → P k
mn : m ≤ n
hP : P n
⊢ P m

Tactic:
induction mn using decreasingInduction with

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

Goal state before:
pp: ι : Sort u_2
α : Type u_3
f : ι → α
a : ι
b : ↑(range f)
⊢ ⟨f a, ⋯⟩ = b ↔ f a = ↑b

Tactic:
← b.coe_eta b.2,

Goal state after:
ι : Sort u_2
α : Type u_3
f : ι → α
a : ι
b : ↑(range f)
⊢ ⟨f a, ⋯⟩ = ⟨↑b, ⋯⟩ ↔ f a = ↑⟨↑b, ⋯⟩
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: α : Type u
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
a : α
⊢ ∃ f, StrictMono f ∧ f 0 = a

Tactic:
by
  choose g hg using fun x : α ↦ exists_gt x
  exact ⟨fun n ↦ Nat.recOn n a fun _ ↦ g, strictMono_nat_of_lt_succ fun n ↦ hg _, rfl⟩

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

Goal state before:
pp: α : Type u_1
x y z w : α
⊢ {x, y} = {z, w} ↔ x = z ∧ y = w ∨ x = w ∧ y = z

Tactic:
simp [subset_antisymm_iff, insert_subset_iff]

Goal state after:
α : Type u_1
x y z w : α
⊢ ((x = z ∨ x = w) ∧ (y = z ∨ y = w)) ∧ (z = x ∨ z = y) ∧ (w = x ∨ w = y) ↔ x = z ∧ y = w ∨ x = w ∧ y = z
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: f : ℕ → ℕ
mono_f : Monotone f
c : ℕ
hc : ∀ (n : ℕ), f n ≤ c
⊢ ∃ b N, ∀ (n : ℕ), n ≥ N → f n = b

Tactic:
induction c with

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

Goal state before:
pp: α : Type u
inst✝ : IsEmpty α
S : Set α
hS : S ∈ univ
⊢ S ∈ {∅}

Tactic:
by simp [Set.eq_empty_of_isEmpty S]

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

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

Tactic:
disjoint_right_comm,

Goal state after:
case a
α : Type u_2
inst✝ : HeytingAlgebra α
a b : α
⊢ Disjoint (aᶜᶜ ⊓ (aᶜᶜ ⇨ bᶜᶜ)) bᶜ
Module: Mathlib.Logic.Equiv.Option

Goal state before:
pp: case some.some
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x val✝¹ : α
h1 : e.symm (some (e.removeNoneAux x)) = some val✝¹
val✝ : β
h2 : e (some x) = some val✝
⊢ e.symm (some (e.removeNoneAux x)) = some x

Tactic:
rw [removeNoneAux_some _ ⟨_, h2⟩]

Goal state after:
case some.some
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x val✝¹ : α
h1 : e.symm (some (e.removeNoneAux x)) = some val✝¹
val✝ : β
h2 : e (some x) = some val✝
⊢ e.symm (e (some x)) = some x
Module: Mathlib.Logic.Equiv.Option

Goal state before:
pp: case some
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
x : β
e : α ≃ { y // y ≠ x }
a : α
⊢ (fun b ↦ if h : b = x then none else some (e.symm ⟨b, h⟩)) ((fun a ↦ a.casesOn' x (Subtype.val ∘ ⇑e)) (some a)) =
    some a

Tactic:
simp only [casesOn'_some, Function.comp_apply, Subtype.coe_eta,
              symm_apply_apply, dite_eq_ite]
            exact if_neg (e a).property

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : BiheytingAlgebra β
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
⊢ BiheytingAlgebra α

Tactic:
let coheytingAlgebra := e.coheytingAlgebra

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : BiheytingAlgebra β
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
⊢ BiheytingAlgebra α
Module: Mathlib.Order.BooleanAlgebra.Basic

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

Tactic:
calc
      x ⊓ y \ z ⊓ (z ⊓ x ⊔ x \ y) = x ⊓ y \ z ⊓ (z ⊓ x) ⊔ x ⊓ y \ z ⊓ x \ y := by rw [inf_sup_left]
      _ = x ⊓ (y \ z ⊓ z ⊓ x) ⊔ x ⊓ y \ z ⊓ x \ y := by ac_rfl
      _ = x ⊓ y \ z ⊓ x \ y := by rw [inf_sdiff_self_left, bot_inf_eq, inf_bot_eq, bot_sup_eq]
      _ = x ⊓ (y \ z ⊓ y) ⊓ x \ y := by conv_lhs => rw [← inf_sdiff_left]
      _ = x ⊓ (y \ z ⊓ (y ⊓ x \ y)) := by ac_rfl
      _ = ⊥ := by rw [inf_sdiff_self_right, inf_bot_eq, inf_bot_eq]

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a : α
⊢ ⊥ ∆ a = a

Tactic:
by rw [symmDiff_comm, symmDiff_bot]

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

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

Tactic:
by
  let bot := e.bot
  let sdiff := e.sdiff
  let distribLattice := e.distribLattice
  apply e.injective.generalizedBooleanAlgebra <;> intros <;>
  first | rfl | exact e.apply_symm_apply _

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

Goal state before:
pp: α₁ : Type u_9
β₁ : Type u_10
inst✝ : DecidableEq α₁
a : α₁
e : Perm β₁
ab : α₁ × β₁
⊢ ((prodExtendRight a e) ab).fst = ab.fst

Tactic:
by
  grind [prodExtendRight]

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

Goal state before:
pp: α : Sort u_1
β : Sort u_4
P : α → Sort u_9
e : α ≃ β
g : (b : β) → P (e.symm b)
b : β
⊢ (piCongrLeft' P e).symm g (e.symm b) = g b

Tactic:
rw [piCongrLeft'_symm_apply, ← heq_iff_eq, eqRec_heq_iff]
  exact congr_arg_heq _ (e.apply_symm_apply _)

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

Goal state before:
pp: α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type u_9
inst✝ : DecidableEq α
i : α
β : α → Type u_10
f : β i × ((j : { j // j ≠ i }) → β ↑j)
⊢ (fun f ↦ (f i, fun j ↦ f ↑j)) ((fun f j ↦ if h : j = i then ⋯ ▸ f.fst else f.snd ⟨j, h⟩) f) = f

Tactic:
by ext x <;> grind

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
a b : α
⊢ a ⇔ b = ⊥ ↔ IsCompl a b

Tactic:
bihimp_eq',

Goal state after:
α : Type u_2
inst✝ : BooleanAlgebra α
a b : α
⊢ a ⊓ b ⊔ aᶜ ⊓ bᶜ = ⊥ ↔ IsCompl a b
Module: Mathlib.Order.SymmDiff

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

Tactic:
bihimp_eq',

Goal state after:
α : Type u_2
inst✝ : BooleanAlgebra α
a b c : α
⊢ a ⊓ (b ⊓ c ⊔ bᶜ ⊓ cᶜ) ⊔ b ∆ c ⊓ aᶜ = a ⊓ (b ⊓ c ⊔ bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
s : Set α
⊢ f '' sᶜ = range f \ f '' s

Tactic:
← image_univ,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
s : Set α
⊢ f '' sᶜ = f '' univ \ f '' s
Module: Mathlib.Data.Set.Image

Goal state before:
pp: case mp.h₂
α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
ht : t ⊆ range f
h : f ⁻¹' s = f ⁻¹' t
⊢ t ⊆ s

Tactic:
· rw [← preimage_subset_preimage_iff ht, h]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
⊢ Sum.inl ⁻¹' range Sum.inr = ∅

Tactic:
← image_univ,

Goal state after:
α : Type u_1
β : Type u_2
⊢ Sum.inl ⁻¹' Sum.inr '' univ = ∅
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
⊢ Sum.inr ⁻¹' range Sum.inl = ∅

Tactic:
← image_univ,

Goal state after:
α : Type u_1
β : Type u_2
⊢ Sum.inr ⁻¹' Sum.inl '' univ = ∅
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: X : Type u_1
Y : Sort u_2
f : X → Y
⊢ range (toPullbackDiag f) = pullbackDiagonal f

Tactic:
← image_univ,

Goal state after:
X : Type u_1
Y : Sort u_2
f : X → Y
⊢ toPullbackDiag f '' univ = pullbackDiagonal f
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
⊢ Surjective (image f)

Tactic:
by
  intro s
  use f ⁻¹' s
  rw [hf.image_preimage]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2
⊢ ∃ f', range f = graphOn f' univ

Tactic:
refine ⟨fun h ↦ (f (hf₁ h).choose).snd, ?_⟩

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2
⊢ range f = graphOn (fun h ↦ (f ⋯.choose).2) univ
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 (a ^ 0) = f a ^ 0

Tactic:
by rw [pow_zero, pow_zero, map_one]

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 (y * y⁻¹) = 1

Tactic:
mul_inv_cancel,

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
⊢ f 1 = 1
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
s t : Set α
h : Semiconj f fa fb
ha : SurjOn fa s t
⊢ SurjOn fb (f '' s) (f '' t)

Tactic:
by
  rintro y ⟨x, hxt, rfl⟩
  rcases ha hxt with ⟨x, hxs, rfl⟩
  rw [h x]
  exact mem_image_of_mem _ (mem_image_of_mem _ hxs)

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

Goal state before:
pp: β₁ : Type u_8
β₂ : Type u_9
t₁ : Set β₁
t₂ : Set β₂
⊢ SurjOn Prod.fst (t₁ ×ˢ t₂) t₁ → t₁ = ∅ ∨ t₂.Nonempty

Tactic:
by by_contra!; aesop

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

Goal state before:
pp: β₁ : Type u_8
β₂ : Type u_9
t₁ : Set β₁
t₂ : Set β₂
⊢ SurjOn Prod.snd (t₁ ×ˢ t₂) t₂ → t₁.Nonempty ∨ t₂ = ∅

Tactic:
by by_contra!; aesop

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

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

Tactic:
rw [mul_eq_one_iff_eq_inv, eq_comm]

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_inv_cancel,

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

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

Tactic:
rw [eq_div_iff_mul_eq', mul_comm]

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

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

Tactic:
rw [mul_comm]

Goal state after:
G : Type u_3
inst✝ : CommGroup G
a b c : G
⊢ c / a * (a / b) = c / b
Module: Mathlib.Algebra.Group.Units.Defs

Goal state before:
pp: α : Type u
inst✝ : Monoid α
a : αˣ
⊢ Commute ↑a ↑a⁻¹

Tactic:
by
  rw [Commute, SemiconjBy, inv_mul, mul_inv]

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

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

Tactic:
by
  rcases h with ⟨⟨a, b, hab, _⟩, rfl⟩
  exact ⟨b, hab⟩

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 × N →* P
x : M × N
⊢ ((f.comp (inl M N)).coprod (f.comp (inr M N))) x = f x

Tactic:
simp [coprod_apply, inl_apply, inr_apply, ← map_mul]

Goal state after:
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
α : Type u_6
inst✝ : Monoid α
x y : αˣ
⊢ (↑(x * y), op ↑(x * y)⁻¹) = (↑x, op ↑x⁻¹) * (↑y, op ↑y⁻¹)

Tactic:
simp only [mul_inv_rev, op_mul, Units.val_mul, Prod.mk_mul_mk]

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

Goal state before:
pp: M₀ : Type u_2
inst✝¹ : Mul M₀
inst✝ : Zero M₀
⊢ IsCancelMulZero M₀ ↔ ∀ {a : M₀}, a ≠ 0 → IsRegular a

Tactic:
simp only [isCancelMulZero_iff, isLeftCancelMulZero_iff, isRightCancelMulZero_iff, ← forall_and]
  exact forall₂_congr fun _ _ ↦ isRegular_iff.symm

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

Goal state before:
pp: M₀ : Type u_2
inst✝¹ : Mul M₀
inst✝ : Zero M₀
⊢ IsCancelMulZero M₀ ↔ ∀ {a : M₀}, a ≠ 0 → IsRegular a

Tactic:
by
  simp only [isCancelMulZero_iff, isLeftCancelMulZero_iff, isRightCancelMulZero_iff, ← forall_and]
  exact forall₂_congr fun _ _ ↦ isRegular_iff.symm

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

Goal state before:
pp: M₀ : Type u_1
inst✝² : CommMonoidWithZero M₀
inst✝¹ : Div M₀
inst✝ : MulDivCancelClass M₀
b a : M₀
ha : a ≠ 0
⊢ a * b / a = b

Tactic:
by
  rw [mul_comm, mul_div_cancel_right₀ _ ha]

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

Goal state before:
pp: α : Type u_4
inst✝ : Group α
a : α
n : ℕ
⊢ Equiv.mulLeft a ^ n = Equiv.mulLeft (a ^ n)

Tactic:
by
  ext; simp [Perm.coe_pow]

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

Goal state before:
pp: α : Type u_4
inst✝ : Group α
a : α
n : ℕ
⊢ Equiv.mulRight a ^ n = Equiv.mulRight (a ^ n)

Tactic:
by
  ext; simp [Perm.coe_pow]

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

Goal state before:
pp: case neg
M₀ : Type u_1
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a✝ b✝ x a b : G₀
ha : ¬a = 0
hb : ¬b = 0
⊢ a * b * (b⁻¹ * a⁻¹) = 1

Tactic:
simp [mul_assoc, ha, hb]

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

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
⊢ a / (a * a) = a⁻¹⁻¹ * a⁻¹ * a⁻¹

Tactic:
simp [mul_inv_rev]

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

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
h : a ≠ 0
g : G₀
⊢ (fun g ↦ g * a) (g * a⁻¹) = g

Tactic:
simp [mul_assoc, inv_mul_cancel₀ h]

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

Goal state before:
pp: case neg
α : Type u_10
β : Type u_11
inst✝² : Group α
inst✝¹ : GroupWithZero β
inst✝ : MulDistribMulAction α β
g : α
x : β
hx : ¬x = 0
⊢ g • (x * x⁻¹) = 1

Tactic:
mul_inv_cancel₀ hx,

Goal state after:
case neg
α : Type u_10
β : Type u_11
inst✝² : Group α
inst✝¹ : GroupWithZero β
inst✝ : MulDistribMulAction α β
g : α
x : β
hx : ¬x = 0
⊢ g • 1 = 1
Module: Mathlib.Algebra.Ring.Defs

Goal state before:
pp: α : Type u
R : Type v
inst✝ : NonUnitalNonAssocRing α
a b : α
⊢ -a * b + a * b = 0

Tactic:
by rw [← right_distrib, neg_add_cancel, zero_mul]

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

Goal state before:
pp: α : Type u
inst✝ : NonUnitalNonAssocRing α
a b c : α
⊢ (a - b) * c = a * c - b * c

Tactic:
simpa only [sub_eq_add_neg, neg_mul_eq_neg_mul] using add_mul a (-b) c

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

Goal state before:
pp: α : Type u_1
inst✝ : CommSemigroup α
a b : α
h : a ∣ b
c : α
⊢ a ∣ c * b

Tactic:
rw [mul_comm]

Goal state after:
α : Type u_1
inst✝ : CommSemigroup α
a b : α
h : a ∣ b
c : α
⊢ a ∣ b * c
Module: Mathlib.Algebra.Divisibility.Basic

Goal state before:
pp: α : Type u_1
inst✝ : CommSemigroup α
a b c : α
⊢ b = c * a ↔ b = a * c

Tactic:
rw [mul_comm]

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

Goal state before:
pp: α : Type u
inst✝ : Ring α
a b : α
u : αˣ
⊢ a /ₚ u - b /ₚ u = (a - b) /ₚ u

Tactic:
rw [sub_eq_add_neg, sub_eq_add_neg, neg_divp, divp_add_divp_same]

Goal state after:
Module: Mathlib.Algebra.Order.Sub.Defs

Goal state before:
pp: α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
b c : α
hc : AddLECancellable c
h : b - c + c < b
⊢ False

Tactic:
exact h.not_ge le_tsub_add

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

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : MulLeftStrictMono α
a : α
⊢ a * 1 < a * a⁻¹ ↔ a < 1

Tactic:
mul_inv_cancel,

Goal state after:
α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : MulLeftStrictMono α
a : α
⊢ a * 1 < 1 ↔ a < 1
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : MulLeftStrictMono α
a : α
⊢ a * a⁻¹ < a * 1 ↔ 1 < a

Tactic:
mul_inv_cancel,

Goal state after:
α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : MulLeftStrictMono α
a : α
⊢ 1 < a * 1 ↔ 1 < a
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulRightMono α
a : α
⊢ a⁻¹ ≤ 1 ↔ 1 ≤ a

Tactic:
← mul_le_mul_iff_right a

Goal state after:
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulRightMono α
a : α
⊢ a⁻¹ * a ≤ 1 * a ↔ 1 ≤ a
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulRightMono α
a : α
⊢ 1 ≤ a⁻¹ ↔ a ≤ 1

Tactic:
← mul_le_mul_iff_right a

Goal state after:
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulRightMono α
a : α
⊢ 1 * a ≤ a⁻¹ * a ↔ a ≤ 1
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

Goal state before:
pp: α : Type u
inst✝³ : Group α
inst✝² : LT α
inst✝¹ : MulLeftStrictMono α
a b c d : α
inst✝ : MulRightStrictMono α
⊢ a * b⁻¹ < d⁻¹ * c ↔ d * a < c * b

Tactic:
← mul_lt_mul_iff_left d,

Goal state after:
α : Type u
inst✝³ : Group α
inst✝² : LT α
inst✝¹ : MulLeftStrictMono α
a b c d : α
inst✝ : MulRightStrictMono α
⊢ d * (a * b⁻¹) < d * (d⁻¹ * c) ↔ d * a < c * b
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: α : Type u_1
inst✝² : MulZeroClass α
a b : α
inst✝¹ : Preorder α
inst✝ : PosMulStrictMono α
ha : 0 < a
hb : 0 < b
⊢ 0 < a * b

Tactic:
simpa only [mul_zero] using mul_lt_mul_of_pos_left hb ha

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

Goal state before:
pp: α : Type u_1
inst✝² : MulZeroClass α
a b : α
inst✝¹ : Preorder α
inst✝ : PosMulStrictMono α
ha : 0 < a
hb : b < 0
⊢ a * b < 0

Tactic:
simpa only [mul_zero] using mul_lt_mul_of_pos_left hb ha

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

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
F : Type u_5
inst✝¹ : FunLike F α β
inst✝ : RelHomClass F r s
f : F
a : α
b : β
h : f a = b
⊢ Acc s b → Acc r a

Tactic:
intro ac

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
F : Type u_5
inst✝¹ : FunLike F α β
inst✝ : RelHomClass F r s
f : F
a : α
b : β
h : f a = b
ac : Acc s b
⊢ Acc r a
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ↪r s
a : α
b : β
h : f a = b
⊢ Acc s b → Acc r a

Tactic:
intro ac

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ↪r s
a : α
b : β
h : f a = b
ac : Acc s b
⊢ Acc r a
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: case mpr
α : Type u_1
x✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
a : α
⊢ Acc r a → Acc (Quotient.lift₂ r H) ⟦a⟧

Tactic:
intro ac

Goal state after:
case mpr
α : Type u_1
x✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
a : α
ac : Acc r a
⊢ Acc (Quotient.lift₂ r H) ⟦a⟧
Module: Mathlib.Algebra.Order.Group.Lattice

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
ha : 1 ≤ a ^ 2
⊢ (a ⊓ 1) * a ⊓ (a ⊓ 1) * 1 = a ⊓ 1

Tactic:
inf_mul,

Goal state after:
α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
ha : 1 ≤ a ^ 2
⊢ a * a ⊓ 1 * a ⊓ (a ⊓ 1) * 1 = a ⊓ 1
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow

Goal state before:
pp: M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulLeftStrictMono M
a : M
ha : 1 < a
n : ℕ
⊢ a ^ n < a ^ (n + 1)

Tactic:
rw [pow_succ]; exact lt_mul_of_one_lt_right' (a ^ n) ha

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.WithTop

Goal state before:
pp: case coe.coe
α : Type u
inst✝² : Add α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedAdd α
a✝¹ : α
hx : ↑a✝¹ ≠ ⊥
a✝ : α
⊢ a✝ ≤ a✝ + a✝¹

Tactic:
exact le_self_add

Goal state after: