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

Goal state before:
pp: S : Type u_3
inst✝ : Semigroup S
b c : S
hbc : Commute b c
a d : S
⊢ a * b * (c * d) = a * c * (b * d)

Tactic:
by simp only [hbc.left_comm, mul_assoc]

Goal state after:
Module: Mathlib.Logic.Nontrivial.Defs

Goal state before:
pp: α : Type u_1
⊢ Subsingleton α → ∀ (x y : α), x = y

Tactic:
intro h
    exact Subsingleton.elim

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

Goal state before:
pp: α : 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

Tactic:
exact ⟨f, symm_apply_eq_iff.1 ‹_›, rfl⟩

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ζ : Type u_6
r : α → α → Prop
a✝ b✝ c✝ : α
inst✝ : IsTrans α r
a b c : α
h₁ : ReflGen r a b
h₂ : ReflGen r b c
⊢ ReflGen r a c

Tactic:
by
    obtain (rfl | h₂) := h₂
    · exact h₁
    obtain (rfl | h₁) := h₁
    · exact single h₂
    exact single (trans_of r h₁ h₂)

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a c : α
⊢ TransGen r a c ↔ ∃ b, r a b ∧ ReflTransGen r b c

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨b, hab, hbc⟩ ↦ head' hab hbc⟩
  induction h with
  | single hac => exact ⟨_, hac, by rfl⟩
  | tail _ hbc IH =>
  rcases IH with ⟨d, had, hdb⟩
  exact ⟨_, had, hdb.tail hbc⟩

Goal state after:
Module: Mathlib.Data.Quot

Goal state before:
pp: α✝ : Sort u_1
β : Sort u_2
ι : Type u_3
α : ι → Sort u_4
S : (i : ι) → Setoid (α i)
q : Quotient inferInstance
i : ι
x✝¹ x✝ : (i : ι) → α i
h : x✝¹ ≈ x✝
⊢ x✝¹ i ≈ x✝ i

Tactic:
exact h i

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

Goal state before:
pp: α : Sort u
β✝ : Sort v
γ : Sort w
inst✝ : Unique α
β : α → Sort u_1
f : (i : α) → β i
⊢ uniqueElim ((fun f ↦ f default) f) = f

Tactic:
ext i

Goal state after:
α : Sort u
β✝ : Sort v
γ : Sort w
inst✝ : Unique α
β : α → Sort u_1
f : (i : α) → β i
i : α
⊢ uniqueElim ((fun f ↦ f default) f) i = f i
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 N α
inst✝² : SMul Nᵐᵒᵖ α
inst✝¹ : IsCentralScalar N α
inst✝ : SMulCommClass M N α
m : M
n : Nᵐᵒᵖ
a : α
⊢ m • n • a = n • m • a

Tactic:
rw [← unop_smul_eq_smul n (m • a), ← unop_smul_eq_smul n a, smul_comm]

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

Goal state before:
pp: case lt
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.lt
⊢ Ordering.lt ≠ Ordering.gt ↔ a ≤ b

Tactic:
simpa using le_of_lt <| compare_lt_iff_lt.1 h

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

Goal state before:
pp: α : Type u
inst✝¹ : Preorder α
inst✝ : OrderTop α
a : α
⊢ a < ⊤ ↔ ¬⊤ ≤ a

Tactic:
by
  simp [lt_iff_le_not_ge]

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

Goal state before:
pp: m n k : ℕ
motive : (m : ℕ) → m ≤ k → Sort u_1
hmn : m ≤ n
hnk : n ≤ k
of_succ : (k_1 : ℕ) → (h : k_1 < k) → motive (k_1 + 1) h → motive k_1 ⋯
self : motive k ⋯
⊢ decreasingInduction of_succ self ⋯ =
    decreasingInduction (fun x x_1 ↦ of_succ x ⋯) (decreasingInduction of_succ self hnk) hmn

Tactic:
induction hnk with

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
⊢ f ∘ rangeSplitting f = Subtype.val

Tactic:
ext
  simp only [Function.comp_apply]
  apply apply_rangeSplitting

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
⊢ f ∘ rangeSplitting f = Subtype.val

Tactic:
by
  ext
  simp only [Function.comp_apply]
  apply apply_rangeSplitting

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

Goal state before:
pp: α : Type u
s : Set α
⊢ ¬IsEmpty ↑s ↔ ¬s = ∅

Tactic:
by simpa using! nonempty_iff_ne_empty

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α✝ : Type u
β : Type v
α : Type u_1
inst✝ : Max α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
sup_idem : ∀ (a : α), a ⊔ a = a
a b c : α
hac : a ⊔ c = c
hbc : b ⊔ c = c
⊢ a ⊔ b ⊔ c = c

Tactic:
rwa [sup_assoc, hbc]

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
inst✝ : SemilatticeSup α
a b c : α
⊢ a ⊔ (b ⊔ c) = a ⊔ b ⊔ (a ⊔ c)

Tactic:
by
  rw [sup_sup_sup_comm, sup_idem]

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
inst✝ : SemilatticeSup α
a b c : α
⊢ a ⊔ b ⊔ c = a ⊔ c ⊔ (b ⊔ c)

Tactic:
by
  rw [sup_sup_sup_comm, sup_idem]

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α✝ : Type u
β : Type v
α : Type u_1
inst✝¹ : Max α
inst✝ : Min α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
sup_inf_self : ∀ (a b : α), a ⊔ a ⊓ b = a
inf_sup_self : ∀ (a b : α), a ⊓ (a ⊔ b) = a
sup_idem : ∀ (b : α), b ⊔ b = b
inf_idem : ∀ (b : α), b ⊓ b = b
semilatt_inf_inst : SemilatticeInf α := SemilatticeInf.mk' inf_comm inf_assoc inf_idem
semilatt_sup_inst : SemilatticeSup α := SemilatticeSup.mk' sup_comm sup_assoc sup_idem
partial_order_eq : semilatt_sup_inst.toPartialOrder = semilatt_inf_inst.toPartialOrder
a b c : α
⊢ a ≤ b → a ≤ c → a ≤ SemilatticeInf.inf b c

Tactic:
apply le_inf

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

Goal state before:
pp: α : Type u_1
t s s' : Set α
⊢ (s ∩ t ∪ s' \ t) ∩ t = s ∩ t

Tactic:
union_inter_distrib_right,

Goal state after:
α : Type u_1
t s s' : Set α
⊢ s ∩ t ∩ t ∪ s' \ t ∩ t = s ∩ t
Module: Mathlib.Data.Sigma.Basic

Goal state before:
pp: α : Type u_1
β : α → Type u_4
h : ∀ (a : α), Subsingleton (β a)
⊢ Injective fst

Tactic:
by
  rintro ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ (rfl : a₁ = a₂)
  exact congr_arg (mk a₁) <| Subsingleton.elim _ _

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

Goal state before:
pp: α₁ : Type u_2
α₂ : Type u_3
β₁ : α₁ → Type u_5
β₂ : α₂ → Type u_6
f₁ : α₁ → α₂
f₂ : (a : α₁) → β₁ a → β₂ (f₁ a)
h₁ : Injective f₁
h₂ : ∀ (a : α₁), Injective (f₂ a)
i : α₁
x : β₁ i
j : α₁
y : β₁ j
h : Sigma.map f₁ f₂ ⟨i, x⟩ = Sigma.map f₁ f₂ ⟨j, y⟩
⊢ ⟨i, x⟩ = ⟨j, y⟩

Tactic:
obtain rfl : i = j := h₁ (Sigma.mk.inj_iff.mp h).1
    obtain rfl : x = y := h₂ i (sigma_mk_injective h)
    rfl

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

Goal state before:
pp: α₁ : Type u_9
α₂ : Type u_10
β₁ : Type u_11
β₂ : Type u_12
γ₁ : Type u_13
γ₂ : Type u_14
e : α₁ ≃ β₁
f : α₂ ≃ β₂
g : β₁ ≃ γ₁
h : β₂ ≃ γ₂
⊢ (e.sumCongr f).trans (g.sumCongr h) = (e.trans g).sumCongr (f.trans h)

Tactic:
ext i

Goal state after:
α₁ : Type u_9
α₂ : Type u_10
β₁ : Type u_11
β₂ : Type u_12
γ₁ : Type u_13
γ₂ : Type u_14
e : α₁ ≃ β₁
f : α₂ ≃ β₂
g : β₁ ≃ γ₁
h : β₂ ≃ γ₂
i : α₁ ⊕ α₂
⊢ ((e.sumCongr f).trans (g.sumCongr h)) i = ((e.trans g).sumCongr (f.trans h)) i
Module: Mathlib.Logic.Equiv.Sum

Goal state before:
pp: α : Type u_9
β : Type u_10
⊢ (Equiv.refl α).sumCongr (Equiv.refl β) = Equiv.refl (α ⊕ β)

Tactic:
ext i

Goal state after:
α : Type u_9
β : Type u_10
i : α ⊕ β
⊢ ((Equiv.refl α).sumCongr (Equiv.refl β)) i = (Equiv.refl (α ⊕ β)) i
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
s : PUnit ⊕ PUnit
⊢ (fun b ↦ Bool.casesOn b (inl PUnit.unit) (inr PUnit.unit)) (Sum.elim (fun x ↦ false) (fun x ↦ true) s) = s

Tactic:
rcases s with (⟨⟨⟩⟩ | ⟨⟨⟩⟩) <;> rfl

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

Goal state before:
pp: α : Type u
x y : α
inst✝ : BooleanAlgebra α
⊢ Disjoint x yᶜ ↔ x ≤ y

Tactic:
by
  rw [← le_compl_iff_disjoint_right, compl_compl]

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
by simp [symmDiff_assoc]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
t : Set β
⊢ univ ×ˢ t = Prod.snd ⁻¹' t

Tactic:
by simp [prod_eq]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
⊢ s ×ˢ univ = Prod.fst ⁻¹' s

Tactic:
by simp [prod_eq]

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

Goal state before:
pp: α : Type u_1
s : Set α
σ : Equiv.Perm α
hs : {a | σ a ≠ a} ⊆ s
⊢ ⇑σ '' s = s

Tactic:
ext i

Goal state after:
α : Type u_1
s : Set α
σ : Equiv.Perm α
hs : {a | σ a ≠ a} ⊆ s
i : α
⊢ i ∈ ⇑σ '' s ↔ i ∈ s
Module: Mathlib.Data.Set.Piecewise

Goal state before:
pp: α : Type u_1
δ : α → Sort u_7
f g : (i : α) → δ i
inst✝ : (i : α) → Decidable (i ∈ ∅)
⊢ ∅.piecewise f g = g

Tactic:
ext i

Goal state after:
α : Type u_1
δ : α → Sort u_7
f g : (i : α) → δ i
inst✝ : (i : α) → Decidable (i ∈ ∅)
i : α
⊢ ∅.piecewise f g i = g i
Module: Mathlib.Data.Set.Piecewise

Goal state before:
pp: α : Type u_1
δ : α → Sort u_7
f g : (i : α) → δ i
inst✝ : (i : α) → Decidable (i ∈ univ)
⊢ univ.piecewise f g = f

Tactic:
ext i

Goal state after:
α : Type u_1
δ : α → Sort u_7
f g : (i : α) → δ i
inst✝ : (i : α) → Decidable (i ∈ univ)
i : α
⊢ univ.piecewise f g i = f i
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✝¹ : DecidableEq α
j : α
inst✝ : (i : α) → Decidable (i ∈ insert j s)
⊢ (fun i ↦ if i = j ∨ i ∈ s then f i else g i) = update (fun i ↦ if i ∈ s then f i else g i) j (f j)

Tactic:
ext i

Goal state after:
α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst✝² : (j : α) → Decidable (j ∈ s)
inst✝¹ : DecidableEq α
j : α
inst✝ : (i : α) → Decidable (i ∈ insert j s)
i : α
⊢ (if i = j ∨ i ∈ s then f i else g i) = update (fun i ↦ if i ∈ s then f i else g i) j (f j) i
Module: Mathlib.Data.Set.Image

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

Tactic:
by
  rw [← image_univ, preimage_inl_image_inr]

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

Goal state before:
pp: case mpr
α : Type u_1
s t : Set α
h : Disjoint s t
x : α × α
⊢ ((x.1 ∈ s ∧ x.2 ∈ s ∧ ¬x.1 = x.2 ∨ x.1 ∈ t ∧ x.2 ∈ t ∧ ¬x.1 = x.2) ∨ x.1 ∈ s ∧ x.2 ∈ t) ∨ x.1 ∈ t ∧ x.2 ∈ s →
    (x.1 ∈ s ∨ x.1 ∈ t) ∧ (x.2 ∈ s ∨ x.2 ∈ t) ∧ ¬x.1 = x.2

Tactic:
rintro (((⟨h0, h1, h2⟩ | ⟨h0, h1, h2⟩) | ⟨h0, h1⟩) | ⟨h0, h1⟩)

Goal state after:
case mpr.inl.inl.inl
α : Type u_1
s t : Set α
h : Disjoint s t
x : α × α
h0 : x.1 ∈ s
h1 : x.2 ∈ s
h2 : ¬x.1 = x.2
⊢ (x.1 ∈ s ∨ x.1 ∈ t) ∧ (x.2 ∈ s ∨ x.2 ∈ t) ∧ ¬x.1 = x.2

case mpr.inl.inl.inr
α : Type u_1
s t : Set α
h : Disjoint s t
x : α × α
h0 : x.1 ∈ t
h1 : x.2 ∈ t
h2 : ¬x.1 = x.2
⊢ (x.1 ∈ s ∨ x.1 ∈ t) ∧ (x.2 ∈ s ∨ x.2 ∈ t) ∧ ¬x.1 = x.2

case mpr.inl.inr
α : Type u_1
s t : Set α
h : Disjoint s t
x : α × α
h0 : x.1 ∈ s
h1 : x.2 ∈ t
⊢ (x.1 ∈ s ∨ x.1 ∈ t) ∧ (x.2 ∈ s ∨ x.2 ∈ t) ∧ ¬x.1 = x.2

case mpr.inr
α : Type u_1
s t : Set α
h : Disjoint s t
x : α × α
h0 : x.1 ∈ t
h1 : x.2 ∈ s
⊢ (x.1 ∈ s ∨ x.1 ∈ t) ∧ (x.2 ∈ s ∨ x.2 ∈ t) ∧ ¬x.1 = x.2
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
s t u : Set α
⊢ val ⁻¹' t ⊆ val ⁻¹' u ↔ s ∩ t ⊆ s ∩ u

Tactic:
by
  constructor
  · rw [← image_preimage_coe, ← image_preimage_coe]
    exact image_mono
  · intro h x a
    exact (h ⟨x.2, a⟩).2

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

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

Tactic:
show z - b = (z - b).toNat by lia,

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

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

Tactic:
by simp +contextual [or_imp, prod_surjOn_fst]

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

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

Tactic:
mul_left_comm,

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Monoid β
r : α → α → Prop
inst✝ : Std.Total r
f : α → α → β
p : α → Prop
hswap : ∀ {a b : α}, p a → p b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a → p b → p c → f a c = f a b * f b c
a b c : α
pa : p a
pb : p b
pc : p c
this : Std.Symm fun x1 x2 ↦ p x1 ∧ p x2
⊢ f a c = f a b * f b c

Tactic:
apply multiplicative_of_symm_of_total (p · ∧ p ·) r f

Goal state after:
case hf_swap
α : Type u_1
β : Type u_2
inst✝¹ : Monoid β
r : α → α → Prop
inst✝ : Std.Total r
f : α → α → β
p : α → Prop
hswap : ∀ {a b : α}, p a → p b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a → p b → p c → f a c = f a b * f b c
a b c : α
pa : p a
pb : p b
pc : p c
this : Std.Symm fun x1 x2 ↦ p x1 ∧ p x2
⊢ ∀ {a b : α}, p a ∧ p b → f a b * f b a = 1

case hmul
α : Type u_1
β : Type u_2
inst✝¹ : Monoid β
r : α → α → Prop
inst✝ : Std.Total r
f : α → α → β
p : α → Prop
hswap : ∀ {a b : α}, p a → p b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a → p b → p c → f a c = f a b * f b c
a b c : α
pa : p a
pb : p b
pc : p c
this : Std.Symm fun x1 x2 ↦ p x1 ∧ p x2
⊢ ∀ {a b c : α}, r a b → r b c → p a ∧ p b → p b ∧ p c → p a ∧ p c → f a c = f a b * f b c

case pab
α : Type u_1
β : Type u_2
inst✝¹ : Monoid β
r : α → α → Prop
inst✝ : Std.Total r
f : α → α → β
p : α → Prop
hswap : ∀ {a b : α}, p a → p b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a → p b → p c → f a c = f a b * f b c
a b c : α
pa : p a
pb : p b
pc : p c
this : Std.Symm fun x1 x2 ↦ p x1 ∧ p x2
⊢ p a ∧ p b

case pbc
α : Type u_1
β : Type u_2
inst✝¹ : Monoid β
r : α → α → Prop
inst✝ : Std.Total r
f : α → α → β
p : α → Prop
hswap : ∀ {a b : α}, p a → p b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a → p b → p c → f a c = f a b * f b c
a b c : α
pa : p a
pb : p b
pc : p c
this : Std.Symm fun x1 x2 ↦ p x1 ∧ p x2
⊢ p b ∧ p c

case pac
α : Type u_1
β : Type u_2
inst✝¹ : Monoid β
r : α → α → Prop
inst✝ : Std.Total r
f : α → α → β
p : α → Prop
hswap : ∀ {a b : α}, p a → p b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a → p b → p c → f a c = f a b * f b c
a b c : α
pa : p a
pb : p b
pc : p c
this : Std.Symm fun x1 x2 ↦ p x1 ∧ p x2
⊢ p a ∧ p c
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
G : Type u_3
M : Type u_4
α : Type u_5
s : AddCommMonoid α
n : ℕ
a : α
⊢ (n + 1) • a = n • a + a

Tactic:
rw [add_nsmul, one_nsmul]

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

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

Tactic:
by
  rw [mul_assoc, mul_inv, mul_one]

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

Goal state before:
pp: case left
α : Type u_7
β : Type u_8
fst✝¹ : Perm α
snd✝¹ : Perm β
fst✝ : Perm α
snd✝ : Perm β
h : (sumCongrHom α β) (fst✝¹, snd✝¹) = (sumCongrHom α β) (fst✝, snd✝)
⊢ fst✝¹ = fst✝

Tactic:
ext i

Goal state after:
case left
α : Type u_7
β : Type u_8
fst✝¹ : Perm α
snd✝¹ : Perm β
fst✝ : Perm α
snd✝ : Perm β
h : (sumCongrHom α β) (fst✝¹, snd✝¹) = (sumCongrHom α β) (fst✝, snd✝)
i : α
⊢ fst✝¹ i = fst✝ i
Module: Mathlib.Algebra.Group.End

Goal state before:
pp: case right
α : Type u_7
β : Type u_8
fst✝¹ : Perm α
snd✝¹ : Perm β
fst✝ : Perm α
snd✝ : Perm β
h : (sumCongrHom α β) (fst✝¹, snd✝¹) = (sumCongrHom α β) (fst✝, snd✝)
⊢ snd✝¹ = snd✝

Tactic:
ext i

Goal state after:
case right
α : Type u_7
β : Type u_8
fst✝¹ : Perm α
snd✝¹ : Perm β
fst✝ : Perm α
snd✝ : Perm β
h : (sumCongrHom α β) (fst✝¹, snd✝¹) = (sumCongrHom α β) (fst✝, snd✝)
i : β
⊢ snd✝¹ i = snd✝ i
Module: Mathlib.Algebra.Group.End

Goal state before:
pp: case left
α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
fst✝¹ : Perm { a // p a }
snd✝¹ : Perm { a // ¬p a }
fst✝ : Perm { a // p a }
snd✝ : Perm { a // ¬p a }
h : (subtypeCongrHom p) (fst✝¹, snd✝¹) = (subtypeCongrHom p) (fst✝, snd✝)
⊢ fst✝¹ = fst✝

Tactic:
ext i

Goal state after:
case left
α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
fst✝¹ : Perm { a // p a }
snd✝¹ : Perm { a // ¬p a }
fst✝ : Perm { a // p a }
snd✝ : Perm { a // ¬p a }
h : (subtypeCongrHom p) (fst✝¹, snd✝¹) = (subtypeCongrHom p) (fst✝, snd✝)
i : { a // p a }
⊢ ↑(fst✝¹ i) = ↑(fst✝ i)
Module: Mathlib.Algebra.Group.End

Goal state before:
pp: case right
α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
fst✝¹ : Perm { a // p a }
snd✝¹ : Perm { a // ¬p a }
fst✝ : Perm { a // p a }
snd✝ : Perm { a // ¬p a }
h : (subtypeCongrHom p) (fst✝¹, snd✝¹) = (subtypeCongrHom p) (fst✝, snd✝)
⊢ snd✝¹ = snd✝

Tactic:
ext i

Goal state after:
case right
α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
fst✝¹ : Perm { a // p a }
snd✝¹ : Perm { a // ¬p a }
fst✝ : Perm { a // p a }
snd✝ : Perm { a // ¬p a }
h : (subtypeCongrHom p) (fst✝¹, snd✝¹) = (subtypeCongrHom p) (fst✝, snd✝)
i : { a // ¬p a }
⊢ ↑(snd✝¹ i) = ↑(snd✝ i)
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: M₀ : Type u_1
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a b x✝ x : G₀
hx : x ≠ 0
y z : G₀
h : y * x = z * x
⊢ z * x * x⁻¹ = z

Tactic:
mul_inv_cancel_right₀ hx z

Goal state after:
M₀ : Type u_1
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a b x✝ x : G₀
hx : x ≠ 0
y z : G₀
h : y * x = z * x
⊢ z = z
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
n : ℕ
h : ↑n ≠ 0
⊢ 0 ^ ↑n = 0

Tactic:
rw [zpow_natCast, zero_pow]

Goal state after:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
n : ℕ
h : ↑n ≠ 0
⊢ n ≠ 0
Module: Mathlib.Data.Nat.Sqrt

Goal state before:
pp: case inl
a b c : ℕ
h : a = b * c
bc : b ≤ c
⊢ b ≤ a.sqrt ∨ c ≤ a.sqrt

Tactic:
exact Or.inl <| le_sqrt.mpr <| h ▸ mul_le_mul_left b bc

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

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
a b : M
n : ℕ
⊢ ((multiplesHom M).toFun (a + b)) n = ((multiplesHom M).toFun a + (multiplesHom M).toFun b) n

Tactic:
simp [nsmul_add]

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : CommRing β
f : β →+ α
h : ∀ (x : β), f (x * x) = f x * f x
h_two : 2 ≠ 0
h_one : f 1 = 1
x y : β
hxy : f (x * x + y * x + (x * y + y * y)) = f (x + y) * f (x + y)
⊢ (↑f).toFun (x * y) = (↑f).toFun x * (↑f).toFun y

Tactic:
f.map_add,

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : CommRing β
f : β →+ α
h : ∀ (x : β), f (x * x) = f x * f x
h_two : 2 ≠ 0
h_one : f 1 = 1
x y : β
hxy : f (x * x + y * x) + f (x * y + y * y) = f (x + y) * f (x + y)
⊢ (↑f).toFun (x * y) = (↑f).toFun x * (↑f).toFun y
Module: Mathlib.Algebra.Ring.Hom.Defs

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : CommRing β
f : β →+ α
h : ∀ (x : β), f (x * x) = f x * f x
h_two : 2 ≠ 0
h_one : f 1 = 1
x y : β
hxy : f (x * x + y * x) + f (x * y + y * y) = f (x + y) * f (x + y)
⊢ (↑f).toFun (x * y) = (↑f).toFun x * (↑f).toFun y

Tactic:
f.map_add,

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : CommRing β
f : β →+ α
h : ∀ (x : β), f (x * x) = f x * f x
h_two : 2 ≠ 0
h_one : f 1 = 1
x y : β
hxy : f (x * x) + f (y * x) + f (x * y + y * y) = f (x + y) * f (x + y)
⊢ (↑f).toFun (x * y) = (↑f).toFun x * (↑f).toFun y
Module: Mathlib.Algebra.Ring.Hom.Defs

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : CommRing β
f : β →+ α
h : ∀ (x : β), f (x * x) = f x * f x
h_two : 2 ≠ 0
h_one : f 1 = 1
x y : β
hxy : f (x * x) + f (y * x) + f (x * y + y * y) = f (x + y) * f (x + y)
⊢ (↑f).toFun (x * y) = (↑f).toFun x * (↑f).toFun y

Tactic:
f.map_add,

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : CommRing β
f : β →+ α
h : ∀ (x : β), f (x * x) = f x * f x
h_two : 2 ≠ 0
h_one : f 1 = 1
x y : β
hxy : f (x * x) + f (y * x) + (f (x * y) + f (y * y)) = f (x + y) * f (x + y)
⊢ (↑f).toFun (x * y) = (↑f).toFun x * (↑f).toFun y
Module: Mathlib.Algebra.Ring.Hom.Defs

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : CommRing β
f : β →+ α
h : ∀ (x : β), f (x * x) = f x * f x
h_two : 2 ≠ 0
h_one : f 1 = 1
x y : β
hxy : f (x * x) + f (y * x) + (f (x * y) + f (y * y)) = f (x + y) * f (x + y)
⊢ (↑f).toFun (x * y) = (↑f).toFun x * (↑f).toFun y

Tactic:
f.map_add,

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : CommRing β
f : β →+ α
h : ∀ (x : β), f (x * x) = f x * f x
h_two : 2 ≠ 0
h_one : f 1 = 1
x y : β
hxy : f (x * x) + f (y * x) + (f (x * y) + f (y * y)) = (f x + f y) * (f x + f y)
⊢ (↑f).toFun (x * y) = (↑f).toFun x * (↑f).toFun y
Module: Mathlib.Algebra.Ring.Units

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : Ring α
F : Type u_1
inst✝² : Ring β
inst✝¹ : FunLike F α β
inst✝ : RingHomClass F α β
f : F
⊢ (map ↑f) (-1) = -1

Tactic:
simp only [Units.map_neg, map_one]

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

Goal state before:
pp: case refine_2
N : Type u_2
r : N → N → Prop
inst✝ : Group N
h : Contravariant N N (fun x1 x2 ↦ x1 * x2) r
a b c : N
bc : r b c
⊢ r ((fun x1 x2 ↦ x1 * x2) a b) ((fun x1 x2 ↦ x1 * x2) a c)

Tactic:
· rw [← inv_mul_cancel_left a b, ← inv_mul_cancel_left a c] at bc
    exact h a⁻¹ bc

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

Goal state before:
pp: M₀ : Type u_2
inst✝³ : MonoidWithZero M₀
inst✝² : LinearOrder M₀
inst✝¹ : PosMulStrictMono M₀
a : M₀
n : ℕ
inst✝ : ZeroLEOneClass M₀
ha : 0 ≤ a
hn : n ≠ 0
⊢ a ^ n ≤ 1 ↔ a ≤ 1

Tactic:
refine ⟨fun h ↦ ?_, pow_le_one₀ ha⟩
  contrapose! h
  exact one_lt_pow₀ h hn

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

Goal state before:
pp: R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : PartialOrder R
a b c d : R
inst✝³ : ExistsAddOfLE R
inst✝² : MulPosMono R
inst✝¹ : AddLeftMono R
inst✝ : AddLeftReflectLE R
hba : b ≤ a
hdc : d ≤ c
⊢ a * d + b * c ≤ a * c + b * d

Tactic:
add_comm (a * d),

Goal state after:
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : PartialOrder R
a b c d : R
inst✝³ : ExistsAddOfLE R
inst✝² : MulPosMono R
inst✝¹ : AddLeftMono R
inst✝ : AddLeftReflectLE R
hba : b ≤ a
hdc : d ≤ c
⊢ b * c + a * d ≤ a * c + b * d
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : PartialOrder R
a b c d : R
inst✝³ : AddLeftReflectLT R
inst✝² : ExistsAddOfLE R
inst✝¹ : MulPosStrictMono R
inst✝ : AddLeftStrictMono R
hba : b < a
hdc : d < c
⊢ a * d + b * c < a * c + b * d

Tactic:
add_comm (a * d),

Goal state after:
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : PartialOrder R
a b c d : R
inst✝³ : AddLeftReflectLT R
inst✝² : ExistsAddOfLE R
inst✝¹ : MulPosStrictMono R
inst✝ : AddLeftStrictMono R
hba : b < a
hdc : d < c
⊢ b * c + a * d < a * c + b * d
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : ZeroLEOneClass G₀
ha : 1 < a
n : ℤ
⊢ a ^ n < a ^ n * a

Tactic:
exact lt_mul_of_one_lt_right (zpow_pos (zero_lt_one.trans ha) _) ha

Goal state after: