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

Goal state before:
pp: S : Type u_1
inst✝ : Semigroup S
a x y x' y' : S
h : SemiconjBy a x y
h' : SemiconjBy a x' y'
⊢ SemiconjBy a (x * x') (y * y')

Tactic:
unfold SemiconjBy
  -- TODO this could be done using `assoc_rw` if/when this is ported to mathlib4
  rw [← mul_assoc, h.eq, mul_assoc, h'.eq, ← mul_assoc]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: A : Prop
B : A → Prop
⊢ (A → ∀ (h : A), B h) ↔ ∀ (h : A), B h

Tactic:
by
  by_cases h : A <;> simp [h]

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

Goal state before:
pp: α : Type u_1
α' : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f : α × α' → β
aa' : α × α'
b : β
⊢ curry (update f aa' b) = update (curry f) aa'.fst (update (curry f aa'.fst) aa'.snd b)

Tactic:
ext a a'

Goal state after:
α : Type u_1
α' : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f : α × α' → β
aa' : α × α'
b : β
a : α
a' : α'
⊢ curry (update f aa' b) a a' = update (curry f) aa'.fst (update (curry f aa'.fst) aa'.snd b) a a'
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
le✝ A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), le✝ a a
le_trans✝¹ : ∀ (a b c : α), le✝ a b → le✝ b c → le✝ a c
A_iff : ∀ (a b : α), A_lt a b ↔ le✝ a b ∧ ¬le✝ b a
B_lt : α → α → Prop
le_refl✝ : ∀ (a : α), le✝ a a
le_trans✝ : ∀ (a b c : α), le✝ a b → le✝ b c → le✝ a c
B_iff : ∀ (a b : α), B_lt a b ↔ le✝ a b ∧ ¬le✝ b a
⊢ A_lt = B_lt

Tactic:
funext a b

Goal state after:
α : Type u_2
le✝ A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), le✝ a a
le_trans✝¹ : ∀ (a b c : α), le✝ a b → le✝ b c → le✝ a c
A_iff : ∀ (a b : α), A_lt a b ↔ le✝ a b ∧ ¬le✝ b a
B_lt : α → α → Prop
le_refl✝ : ∀ (a : α), le✝ a a
le_trans✝ : ∀ (a b c : α), le✝ a b → le✝ b c → le✝ a c
B_iff : ∀ (a b : α), B_lt a b ↔ le✝ a b ∧ ¬le✝ b a
a b : α
⊢ A_lt a b = B_lt a b
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
A_le A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), A_le a a
le_trans✝¹ : ∀ (a b c : α), A_le a b → A_le b c → A_le a c
lt_iff_le_not_ge✝¹ : ∀ (a b : α), A_lt a b ↔ A_le a b ∧ ¬A_le b a
le_antisymm✝¹ : ∀ (a b : α), A_le a b → A_le b a → a = b
A_min A_max : α → α → α
A_compare : α → α → Ordering
le_total✝¹ : ∀ (a b : α), A_le a b ∨ A_le b a
A_decidableLE : DecidableLE α
A_decidableEq : DecidableEq α
A_decidableLT : DecidableLT α
A_min_def : ∀ (a b : α), A_min a b = if A_le a b then a else b
A_max_def : ∀ (a b : α), A_max a b = if A_le a b then b else a
A_compare_canonical : ∀ (a b : α), A_compare a b = compareOfLessAndEq a b
B_min B_max : α → α → α
B_compare : α → α → Ordering
le_refl✝ : ∀ (a : α), A_le a a
le_trans✝ : ∀ (a b c : α), A_le a b → A_le b c → A_le a c
le_antisymm✝ : ∀ (a b : α), A_le a b → A_le b a → a = b
le_total✝ : ∀ (a b : α), A_le a b ∨ A_le b a
lt_iff_le_not_ge✝ : ∀ (a b : α), A_lt a b ↔ A_le a b ∧ ¬A_le b a
B_min_def : ∀ (a b : α), B_min a b = if A_le a b then a else b
B_max_def : ∀ (a b : α), B_max a b = if A_le a b then b else a
B_compare_canonical : ∀ (a b : α), B_compare a b = compareOfLessAndEq a b
⊢ A_min = B_min

Tactic:
funext a b

Goal state after:
α : Type u_2
A_le A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), A_le a a
le_trans✝¹ : ∀ (a b c : α), A_le a b → A_le b c → A_le a c
lt_iff_le_not_ge✝¹ : ∀ (a b : α), A_lt a b ↔ A_le a b ∧ ¬A_le b a
le_antisymm✝¹ : ∀ (a b : α), A_le a b → A_le b a → a = b
A_min A_max : α → α → α
A_compare : α → α → Ordering
le_total✝¹ : ∀ (a b : α), A_le a b ∨ A_le b a
A_decidableLE : DecidableLE α
A_decidableEq : DecidableEq α
A_decidableLT : DecidableLT α
A_min_def : ∀ (a b : α), A_min a b = if A_le a b then a else b
A_max_def : ∀ (a b : α), A_max a b = if A_le a b then b else a
A_compare_canonical : ∀ (a b : α), A_compare a b = compareOfLessAndEq a b
B_min B_max : α → α → α
B_compare : α → α → Ordering
le_refl✝ : ∀ (a : α), A_le a a
le_trans✝ : ∀ (a b c : α), A_le a b → A_le b c → A_le a c
le_antisymm✝ : ∀ (a b : α), A_le a b → A_le b a → a = b
le_total✝ : ∀ (a b : α), A_le a b ∨ A_le b a
lt_iff_le_not_ge✝ : ∀ (a b : α), A_lt a b ↔ A_le a b ∧ ¬A_le b a
B_min_def : ∀ (a b : α), B_min a b = if A_le a b then a else b
B_max_def : ∀ (a b : α), B_max a b = if A_le a b then b else a
B_compare_canonical : ∀ (a b : α), B_compare a b = compareOfLessAndEq a b
a b : α
⊢ A_min a b = B_min a b
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
A_le A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), A_le a a
le_trans✝¹ : ∀ (a b c : α), A_le a b → A_le b c → A_le a c
lt_iff_le_not_ge✝¹ : ∀ (a b : α), A_lt a b ↔ A_le a b ∧ ¬A_le b a
le_antisymm✝¹ : ∀ (a b : α), A_le a b → A_le b a → a = b
A_min A_max : α → α → α
A_compare : α → α → Ordering
le_total✝¹ : ∀ (a b : α), A_le a b ∨ A_le b a
A_decidableLE : DecidableLE α
A_decidableEq : DecidableEq α
A_decidableLT : DecidableLT α
A_min_def : ∀ (a b : α), A_min a b = if A_le a b then a else b
A_max_def : ∀ (a b : α), A_max a b = if A_le a b then b else a
A_compare_canonical : ∀ (a b : α), A_compare a b = compareOfLessAndEq a b
B_max : α → α → α
B_compare : α → α → Ordering
le_refl✝ : ∀ (a : α), A_le a a
le_trans✝ : ∀ (a b c : α), A_le a b → A_le b c → A_le a c
le_antisymm✝ : ∀ (a b : α), A_le a b → A_le b a → a = b
le_total✝ : ∀ (a b : α), A_le a b ∨ A_le b a
lt_iff_le_not_ge✝ : ∀ (a b : α), A_lt a b ↔ A_le a b ∧ ¬A_le b a
B_max_def : ∀ (a b : α), B_max a b = if A_le a b then b else a
B_compare_canonical : ∀ (a b : α), B_compare a b = compareOfLessAndEq a b
B_min_def : ∀ (a b : α), A_min a b = if A_le a b then a else b
⊢ A_max = B_max

Tactic:
funext a b

Goal state after:
α : Type u_2
A_le A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), A_le a a
le_trans✝¹ : ∀ (a b c : α), A_le a b → A_le b c → A_le a c
lt_iff_le_not_ge✝¹ : ∀ (a b : α), A_lt a b ↔ A_le a b ∧ ¬A_le b a
le_antisymm✝¹ : ∀ (a b : α), A_le a b → A_le b a → a = b
A_min A_max : α → α → α
A_compare : α → α → Ordering
le_total✝¹ : ∀ (a b : α), A_le a b ∨ A_le b a
A_decidableLE : DecidableLE α
A_decidableEq : DecidableEq α
A_decidableLT : DecidableLT α
A_min_def : ∀ (a b : α), A_min a b = if A_le a b then a else b
A_max_def : ∀ (a b : α), A_max a b = if A_le a b then b else a
A_compare_canonical : ∀ (a b : α), A_compare a b = compareOfLessAndEq a b
B_max : α → α → α
B_compare : α → α → Ordering
le_refl✝ : ∀ (a : α), A_le a a
le_trans✝ : ∀ (a b c : α), A_le a b → A_le b c → A_le a c
le_antisymm✝ : ∀ (a b : α), A_le a b → A_le b a → a = b
le_total✝ : ∀ (a b : α), A_le a b ∨ A_le b a
lt_iff_le_not_ge✝ : ∀ (a b : α), A_lt a b ↔ A_le a b ∧ ¬A_le b a
B_max_def : ∀ (a b : α), B_max a b = if A_le a b then b else a
B_compare_canonical : ∀ (a b : α), B_compare a b = compareOfLessAndEq a b
B_min_def : ∀ (a b : α), A_min a b = if A_le a b then a else b
a b : α
⊢ A_max a b = B_max a b
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
A_le A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), A_le a a
le_trans✝¹ : ∀ (a b c : α), A_le a b → A_le b c → A_le a c
lt_iff_le_not_ge✝¹ : ∀ (a b : α), A_lt a b ↔ A_le a b ∧ ¬A_le b a
le_antisymm✝¹ : ∀ (a b : α), A_le a b → A_le b a → a = b
A_min A_max : α → α → α
A_compare : α → α → Ordering
le_total✝¹ : ∀ (a b : α), A_le a b ∨ A_le b a
A_decidableLE : DecidableLE α
A_decidableEq : DecidableEq α
A_decidableLT : DecidableLT α
A_min_def : ∀ (a b : α), A_min a b = if A_le a b then a else b
A_max_def : ∀ (a b : α), A_max a b = if A_le a b then b else a
A_compare_canonical : ∀ (a b : α), A_compare a b = compareOfLessAndEq a b
B_compare : α → α → Ordering
le_refl✝ : ∀ (a : α), A_le a a
le_trans✝ : ∀ (a b c : α), A_le a b → A_le b c → A_le a c
le_antisymm✝ : ∀ (a b : α), A_le a b → A_le b a → a = b
le_total✝ : ∀ (a b : α), A_le a b ∨ A_le b a
lt_iff_le_not_ge✝ : ∀ (a b : α), A_lt a b ↔ A_le a b ∧ ¬A_le b a
B_compare_canonical : ∀ (a b : α), B_compare a b = compareOfLessAndEq a b
B_min_def : ∀ (a b : α), A_min a b = if A_le a b then a else b
B_max_def : ∀ (a b : α), A_max a b = if A_le a b then b else a
⊢ A_compare = B_compare

Tactic:
funext a b

Goal state after:
α : Type u_2
A_le A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), A_le a a
le_trans✝¹ : ∀ (a b c : α), A_le a b → A_le b c → A_le a c
lt_iff_le_not_ge✝¹ : ∀ (a b : α), A_lt a b ↔ A_le a b ∧ ¬A_le b a
le_antisymm✝¹ : ∀ (a b : α), A_le a b → A_le b a → a = b
A_min A_max : α → α → α
A_compare : α → α → Ordering
le_total✝¹ : ∀ (a b : α), A_le a b ∨ A_le b a
A_decidableLE : DecidableLE α
A_decidableEq : DecidableEq α
A_decidableLT : DecidableLT α
A_min_def : ∀ (a b : α), A_min a b = if A_le a b then a else b
A_max_def : ∀ (a b : α), A_max a b = if A_le a b then b else a
A_compare_canonical : ∀ (a b : α), A_compare a b = compareOfLessAndEq a b
B_compare : α → α → Ordering
le_refl✝ : ∀ (a : α), A_le a a
le_trans✝ : ∀ (a b c : α), A_le a b → A_le b c → A_le a c
le_antisymm✝ : ∀ (a b : α), A_le a b → A_le b a → a = b
le_total✝ : ∀ (a b : α), A_le a b ∨ A_le b a
lt_iff_le_not_ge✝ : ∀ (a b : α), A_lt a b ↔ A_le a b ∧ ¬A_le b a
B_compare_canonical : ∀ (a b : α), B_compare a b = compareOfLessAndEq a b
B_min_def : ∀ (a b : α), A_min a b = if A_le a b then a else b
B_max_def : ∀ (a b : α), A_max a b = if A_le a b then b else a
a b : α
⊢ A_compare a b = B_compare a b
Module: Mathlib.Data.Int.Order.Basic

Goal state before:
pp: a b : ℤ
⊢ a * b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b

Tactic:
by
  rw [← not_iff_not, not_le, Int.mul_pos_iff]
  lia

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

Goal state before:
pp: α : Type u
s t : Set α
⊢ Disjoint t s ↔ ∀ ⦃a : α⦄, a ∈ t → ¬a ∈ s

Tactic:
disjoint_left

Goal state after:
α : Type u
s t : Set α
⊢ (∀ ⦃a : α⦄, a ∈ t → ¬a ∈ s) ↔ ∀ ⦃a : α⦄, a ∈ t → ¬a ∈ s
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : Max α
inst✝² : LE α
inst✝¹ : LT α
inst✝ : SemilatticeSup β
f : α → β
hf_inj : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
a b c : α
ha : f a ≤ f c
hb : f b ≤ f c
⊢ f a ⊔ f b ≤ f c

Tactic:
exact sup_le ha hb

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

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
h : x < z \ y
hyz : y ≤ z
⊢ x ⊔ y < z

Tactic:
← sdiff_sup_cancel hyz

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
h : x < z \ y
hyz : y ≤ z
⊢ x ⊔ y < z \ y ⊔ y
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x y : α
inst✝ : BooleanAlgebra α
⊢ x ⊓ yᶜᶜ = x ⊓ y

Tactic:
compl_compl

Goal state after:
α : Type u
x y : α
inst✝ : BooleanAlgebra α
⊢ x ⊓ y = x ⊓ y
Module: Mathlib.Order.BooleanAlgebra.Basic

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

Tactic:
compl_compl

Goal state after:
α : Type u
x y : α
inst✝ : BooleanAlgebra α
⊢ y ≤ x ↔ y ≤ x
Module: Mathlib.Order.BooleanAlgebra.Basic

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

Tactic:
compl_compl

Goal state after:
α : Type u
x y : α
inst✝ : BooleanAlgebra α
⊢ x ≤ y ↔ x ≤ y
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.18
β : Type ?u.17
γ : Type ?u.15
⊢ LeftInverse (fun s ↦ Sum.elim (Prod.map inl id) (Prod.map inr id) s) fun p ↦
    Sum.map (fun x ↦ (x, p.snd)) (fun x ↦ (x, p.snd)) p.fst

Tactic:
rintro ⟨_ | _, _⟩

Goal state after:
case inl
α✝ : 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.18
β : Type ?u.17
γ : Type ?u.15
snd✝ : γ
val✝ : α
⊢ (fun s ↦ Sum.elim (Prod.map inl id) (Prod.map inr id) s)
      ((fun p ↦ Sum.map (fun x ↦ (x, p.snd)) (fun x ↦ (x, p.snd)) p.fst) (inl val✝, snd✝)) =
    (inl val✝, snd✝)

case inr
α✝ : 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.18
β : Type ?u.17
γ : Type ?u.15
snd✝ : γ
val✝ : β
⊢ (fun s ↦ Sum.elim (Prod.map inl id) (Prod.map inr id) s)
      ((fun p ↦ Sum.map (fun x ↦ (x, p.snd)) (fun x ↦ (x, p.snd)) p.fst) (inr val✝, snd✝)) =
    (inr val✝, snd✝)
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.13
⊢ LeftInverse (Sum.elim (Prod.mk false) (Prod.mk true)) fun p ↦ if p.fst = true then inr p.snd else inl p.snd

Tactic:
rintro ⟨_ | _, _⟩

Goal state after:
case false
α✝ : 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.13
snd✝ : α
⊢ Sum.elim (Prod.mk false) (Prod.mk true) ((fun p ↦ if p.fst = true then inr p.snd else inl p.snd) (false, snd✝)) =
    (false, snd✝)

case true
α✝ : 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.13
snd✝ : α
⊢ Sum.elim (Prod.mk false) (Prod.mk true) ((fun p ↦ if p.fst = true then inr p.snd else inl p.snd) (true, snd✝)) =
    (true, snd✝)
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
inst✝ : BooleanAlgebra α
s : Set α
⊢ compl '' compl '' s = s

Tactic:
rw [← image_comp, compl_comp_compl, image_id]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
p : Set β → Prop
⊢ (∃ s, s ⊆ range f ∧ p s) ↔ ∃ a, a ∈ range (image f) ∧ p a

Tactic:
range_image

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
p : Set β → Prop
⊢ (∃ s, s ⊆ range f ∧ p s) ↔ ∃ a, a ∈ 𝒫 range f ∧ p a
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
p : Set β → Prop
⊢ (∀ (s : Set β), s ⊆ range f → p s) ↔ ∀ (a : Set β), a ∈ range (image f) → p a

Tactic:
range_image

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
p : Set β → Prop
⊢ (∀ (s : Set β), s ⊆ range f → p s) ↔ ∀ (a : Set β), a ∈ 𝒫 range f → p a
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ f '' (univ \ f ⁻¹' s) = range f \ s

Tactic:
image_sdiff_preimage,

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
x : ↑(range f)
⊢ rangeFactorization f (rangeSplitting f x) = x

Tactic:
ext
  simp only [rangeFactorization_coe]
  apply apply_rangeSplitting

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
f : α → β
t' : Set β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r (f '' ((s₁ ∩ f ⁻¹' t') \ f ⁻¹' t))
⊢ ∃ s', s ⊆ s' ∧ s' ⊆ s₁ ∧ BijOn f s' t'

Tactic:
image_sdiff_preimage,

Goal state after:
α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
f : α → β
t' : Set β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r (f '' (s₁ ∩ f ⁻¹' t') \ t)
⊢ ∃ s', s ⊆ s' ∧ s' ⊆ s₁ ∧ BijOn f s' t'
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✝³ : Inv M₁
inst✝² : Div M₁
inst✝¹ : Pow M₁ ℤ
inst✝ : DivInvMonoid M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
x : M₁
⊢ f x ^ 0 = f 1

Tactic:
zpow_zero,

Goal state after:
M₁ : Type u_1
M₂ : Type u_2
inst✝⁶ : Mul M₁
inst✝⁵ : One M₁
inst✝⁴ : Pow M₁ ℕ
inst✝³ : Inv M₁
inst✝² : Div M₁
inst✝¹ : Pow M₁ ℤ
inst✝ : DivInvMonoid M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
x : M₁
⊢ 1 = f 1
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:
mul_inv_eq_iff_eq_mul

Goal state after:
G : Type u_3
inst✝ : Group 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✝⁵ : One M₂
inst✝⁴ : Pow M₂ ℕ
inst✝³ : Inv M₂
inst✝² : Div M₂
inst✝¹ : Pow M₂ ℤ
inst✝ : DivInvMonoid M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
x : M₁
⊢ f (x ^ 0) = 1

Tactic:
zpow_zero,

Goal state after:
M₁ : Type u_1
M₂ : Type u_2
inst✝⁶ : Mul M₂
inst✝⁵ : One M₂
inst✝⁴ : Pow M₂ ℕ
inst✝³ : Inv M₂
inst✝² : Div M₂
inst✝¹ : Pow M₂ ℤ
inst✝ : DivInvMonoid M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
x : M₁
⊢ f 1 = 1
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
a b : G₀
h : a * b = 1
⊢ a⁻¹ = b

Tactic:
rw [← inv_mul_cancel_left₀ (left_ne_zero_of_mul_eq_one h) b, h, mul_one]

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

Goal state before:
pp: case refine_2
m n✝ : ℤ
P : ℤ → Sort u_1
lt : (n : ℤ) → n < m → P n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → P k) → P n
n : ℤ
x✝ : n ≥ m
hn : m ≤ n
k : ℤ
hmk : m ≤ k
ih' :
  (∀ (k_1 : ℤ), k_1 < k → ∀ (hn : m ≤ k_1), Int.strongRec lt ge k_1 = ge k_1 hn fun k x ↦ Int.strongRec lt ge k) →
    (Int.inductionOn' (motive := fun x ↦ (k : ℤ) → k < x → P k) k m lt
        (fun _n a ih l a_1 ↦ if hlm : l < m then lt l hlm else ge l ⋯ fun k x ↦ ih k ⋯) fun n x hn l x_1 ↦ hn l ⋯) =
      fun k_1 x ↦ Int.strongRec lt ge k_1
ih : ∀ (k_1 : ℤ), k_1 < k + 1 → ∀ (hn : m ≤ k_1), Int.strongRec lt ge k_1 = ge k_1 hn fun k x ↦ Int.strongRec lt ge k
l : ℤ
hl : l < k + 1
⊢ Int.inductionOn' (motive := fun x ↦ (k : ℤ) → k < x → P k) (k + 1) m lt
      (fun _n a ih l a_1 ↦ if hlm : l < m then lt l hlm else ge l ⋯ fun k x ↦ ih k ⋯) (fun n x hn l x_1 ↦ hn l ⋯) l hl =
    Int.strongRec lt ge l

Tactic:
rw [inductionOn'_add_one hmk]

Goal state after:
case refine_2
m n✝ : ℤ
P : ℤ → Sort u_1
lt : (n : ℤ) → n < m → P n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → P k) → P n
n : ℤ
x✝ : n ≥ m
hn : m ≤ n
k : ℤ
hmk : m ≤ k
ih' :
  (∀ (k_1 : ℤ), k_1 < k → ∀ (hn : m ≤ k_1), Int.strongRec lt ge k_1 = ge k_1 hn fun k x ↦ Int.strongRec lt ge k) →
    (Int.inductionOn' (motive := fun x ↦ (k : ℤ) → k < x → P k) k m lt
        (fun _n a ih l a_1 ↦ if hlm : l < m then lt l hlm else ge l ⋯ fun k x ↦ ih k ⋯) fun n x hn l x_1 ↦ hn l ⋯) =
      fun k_1 x ↦ Int.strongRec lt ge k_1
ih : ∀ (k_1 : ℤ), k_1 < k + 1 → ∀ (hn : m ≤ k_1), Int.strongRec lt ge k_1 = ge k_1 hn fun k x ↦ Int.strongRec lt ge k
l : ℤ
hl : l < k + 1
⊢ (if hlm : l < m then lt l hlm
    else
      ge l ⋯ fun k_1 x ↦
        Int.inductionOn' (motive := fun x ↦ (k : ℤ) → k < x → P k) k m lt
          (fun _n a ih l a_1 ↦ if hlm : l < m then lt l hlm else ge l ⋯ fun k x ↦ ih k ⋯) (fun n x hn l x_1 ↦ hn l ⋯)
          k_1 ⋯) =
    Int.strongRec lt ge l
Module: Mathlib.Logic.Nontrivial.Basic

Goal state before:
pp: I : Type u_3
f : I → Type u_4
i' : I
inst : ∀ (i : I), Nonempty (f i)
inst✝ : Nontrivial (f i')
⊢ Nontrivial ((i : I) → f i)

Tactic:
by
  classical
  let := Classical.decEq (∀ i : I, f i)
  exact (Function.update_injective (fun i ↦ Classical.choice (inst i)) i').nontrivial

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

Goal state before:
pp: G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
a b : G₀
h : b = 0 → a = 0
⊢ a / b * b = a

Tactic:
div_mul_cancel_of_imp h

Goal state after:
G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
a b : G₀
h : b = 0 → a = 0
⊢ a = a
Module: Mathlib.Algebra.Module.NatInt

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoidWithOne M
inst✝¹ : CharZero M
inst✝ : Module R M
m n : ℕ
h : ↑m = ↑n
⊢ m • 1 = n • 1

Tactic:
← Nat.cast_smul_eq_nsmul R,

Goal state after:
R : Type u_1
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoidWithOne M
inst✝¹ : CharZero M
inst✝ : Module R M
m n : ℕ
h : ↑m = ↑n
⊢ ↑m • 1 = n • 1
Module: Mathlib.Algebra.Module.NatInt

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoidWithOne M
inst✝¹ : CharZero M
inst✝ : Module R M
m n : ℕ
h : ↑m = ↑n
⊢ ↑m • 1 = n • 1

Tactic:
← Nat.cast_smul_eq_nsmul R,

Goal state after:
R : Type u_1
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoidWithOne M
inst✝¹ : CharZero M
inst✝ : Module R M
m n : ℕ
h : ↑m = ↑n
⊢ ↑m • 1 = ↑n • 1
Module: Mathlib.Logic.OpClass

Goal state before:
pp: α : Sort u
β : Sort v
f : α → α → α
hc : Std.Commutative f
ha : Std.Associative f
a b c : α
⊢ f a (f b c) = f (f a c) b

Tactic:
hc.comm b,

Goal state after:
α : Sort u
β : Sort v
f : α → α → α
hc : Std.Commutative f
ha : Std.Associative f
a b c : α
⊢ f a (f c b) = f (f a c) b
Module: Mathlib.Algebra.Order.Monoid.NatCast

Goal state before:
pp: α : Type u_1
inst✝³ : AddMonoidWithOne α
inst✝² : Preorder α
inst✝¹ : ZeroLEOneClass α
inst✝ : AddLeftMono α
⊢ 0 ≤ 2

Tactic:
rw [← one_add_one_eq_two]
  exact add_nonneg zero_le_one zero_le_one

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

Goal state before:
pp: α✝ : Type u_1
α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : Preorder α
mul_le_mul_left : ∀ (a b : α), a ≤ b → ∀ (c : α), a * c ≤ b * c
mul_le_mul_right : ∀ (a b : α), a ≤ b → ∀ (c : α), c * a ≤ c * b
toIsOrderedMonoid : IsOrderedMonoid α := { mul_le_mul_left := mul_le_mul_left }
le_of_mul_le_mul_left : ∀ (a b c : α), a * b ≤ a * c → b ≤ c
a b c : α
h : a * b ≤ a * c
⊢ b ≤ c

Tactic:
exact le_of_mul_le_mul_left a b c h

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝³ : MulZeroClass α
a b c d : α
inst✝² : PartialOrder α
inst✝¹ : PosMulStrictMono α
inst✝ : MulPosStrictMono α
hab✝ : a ≤ b
hcd : c ≤ d
a0 : 0 < a
d0 : 0 < d
h : a * c = b * d
hab : a < b
⊢ a * c < b * d

pp: case refine_2
α : Type u_1
inst✝³ : MulZeroClass α
a b c d : α
inst✝² : PartialOrder α
inst✝¹ : PosMulStrictMono α
inst✝ : MulPosStrictMono α
hab : a ≤ b
hcd✝ : c ≤ d
a0 : 0 < a
d0 : 0 < d
h : a * c = b * d
hcd : c < d
⊢ a * c < b * d

Tactic:
· exact (mul_le_mul_of_nonneg_left hcd a0.le).trans_lt (mul_lt_mul_of_pos_right hab d0)

Goal state after:
case refine_2
α : Type u_1
inst✝³ : MulZeroClass α
a b c d : α
inst✝² : PartialOrder α
inst✝¹ : PosMulStrictMono α
inst✝ : MulPosStrictMono α
hab : a ≤ b
hcd✝ : c ≤ d
a0 : 0 < a
d0 : 0 < d
h : a * c = b * d
hcd : c < d
⊢ a * c < b * d
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: M₀ : Type u_2
inst✝² : MonoidWithZero M₀
inst✝¹ : PartialOrder M₀
a : M₀
inst✝ : PosMulStrictMono M₀
ha : 0 < a
⊢ 0 < a ^ (0 + 1)

Tactic:
simpa using ha

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

Goal state before:
pp: G₀ : Type u_3
inst✝¹ : GroupWithZero G₀
inst✝ : Preorder G₀
a b : G₀
hb : 0 ≤ b
⊢ a * (a⁻¹ * b) ≤ b

Tactic:
obtain rfl | ha := eq_or_ne a 0 <;> simp [*]

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

Goal state before:
pp: G₀ : Type u_3
inst✝¹ : GroupWithZero G₀
inst✝ : Preorder G₀
a b : G₀
hb : b ≤ 0
⊢ b ≤ a * (a⁻¹ * b)

Tactic:
obtain rfl | ha := eq_or_ne a 0 <;> simp [*]

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

Goal state before:
pp: G₀ : Type u_3
inst✝¹ : GroupWithZero G₀
inst✝ : Preorder G₀
a b : G₀
hb : 0 ≤ b
⊢ a⁻¹ * (a * b) ≤ b

Tactic:
obtain rfl | ha := eq_or_ne a 0 <;> simp [*]

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

Goal state before:
pp: G₀ : Type u_3
inst✝¹ : GroupWithZero G₀
inst✝ : Preorder G₀
a b : G₀
hb : b ≤ 0
⊢ b ≤ a⁻¹ * (a * b)

Tactic:
obtain rfl | ha := eq_or_ne a 0 <;> simp [*]

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

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : Preorder G₀
inst✝ : ZeroLEOneClass G₀
a : G₀
⊢ a / a ≤ 1

Tactic:
obtain rfl | ha := eq_or_ne a 0 <;> simp [*]

Goal state after: