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

Goal state before:
pp: α : Sort u_1
r : α → α → Prop
a✝ b c : α
inst✝¹ : DecidableRel r
inst✝ : Irrefl r
a : α
⊢ ¬Decidable.decide (r a a) = true

Tactic:
simpa using irrefl a

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

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

Tactic:
by
  induction n with
  | zero => simp
  | succ n ih => simp [pow_succ', ← ih, mul_assoc]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_3
β : Sort u_4
γ : Sort u_5
f : α → β → γ
P : Prop
inst✝ : Decidable P
a : P → α
b : ¬P → α
c : P → β
d : ¬P → β
⊢ f (dite P a b) (dite P c d) = if h : P then f (a h) (c h) else f (b h) (d h)

Tactic:
by_cases h : P

Goal state after:
case pos
α : Sort u_3
β : Sort u_4
γ : Sort u_5
f : α → β → γ
P : Prop
inst✝ : Decidable P
a : P → α
b : ¬P → α
c : P → β
d : ¬P → β
h : P
⊢ f (dite P a b) (dite P c d) = if h : P then f (a h) (c h) else f (b h) (d h)

case neg
α : Sort u_3
β : Sort u_4
γ : Sort u_5
f : α → β → γ
P : Prop
inst✝ : Decidable P
a : P → α
b : ¬P → α
c : P → β
d : ¬P → β
h : ¬P
⊢ f (dite P a b) (dite P c d) = if h : P then f (a h) (c h) else f (b h) (d h)
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
σ : α → Sort u_2
P : Prop
inst✝ : Decidable P
f : P → (a : α) → σ a
g : ¬P → (a : α) → σ a
a : α
⊢ dite P f g a = if h : P then f h a else g h a

Tactic:
by_cases h : P

Goal state after:
case pos
α : Sort u_1
σ : α → Sort u_2
P : Prop
inst✝ : Decidable P
f : P → (a : α) → σ a
g : ¬P → (a : α) → σ a
a : α
h : P
⊢ dite P f g a = if h : P then f h a else g h a

case neg
α : Sort u_1
σ : α → Sort u_2
P : Prop
inst✝ : Decidable P
f : P → (a : α) → σ a
g : ¬P → (a : α) → σ a
a : α
h : ¬P
⊢ dite P f g a = if h : P then f h a else g h a
Module: Mathlib.Logic.Basic

Goal state before:
pp: P : Prop
inst✝ : Decidable P
Q : P → Prop
R : ¬P → Prop
⊢ dite P Q R ↔ (∃ p, Q p) ∨ ∃ p, R p

Tactic:
by_cases h : P

Goal state after:
case pos
P : Prop
inst✝ : Decidable P
Q : P → Prop
R : ¬P → Prop
h : P
⊢ dite P Q R ↔ (∃ p, Q p) ∨ ∃ p, R p

case neg
P : Prop
inst✝ : Decidable P
Q : P → Prop
R : ¬P → Prop
h : ¬P
⊢ dite P Q R ↔ (∃ p, Q p) ∨ ∃ p, R p
Module: Mathlib.Logic.Basic

Goal state before:
pp: P : Prop
inst✝ : Decidable P
Q : P → Prop
R : ¬P → Prop
⊢ dite P Q R ↔ (∀ (h : P), Q h) ∧ ∀ (h : ¬P), R h

Tactic:
by_cases h : P

Goal state after:
case pos
P : Prop
inst✝ : Decidable P
Q : P → Prop
R : ¬P → Prop
h : P
⊢ dite P Q R ↔ (∀ (h : P), Q h) ∧ ∀ (h : ¬P), R h

case neg
P : Prop
inst✝ : Decidable P
Q : P → Prop
R : ¬P → Prop
h : ¬P
⊢ dite P Q R ↔ (∀ (h : P), Q h) ∧ ∀ (h : ¬P), R h
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_3
β : Sort u_4
p : β → Prop
inst✝ : DecidablePred p
g : β → α
hg : Injective g
f : β → α
hf : Injective f
h : ∀ (x y : β), g x = f y → x = y
x y : β
x✝ : (fun x ↦ if p x then g x else f x) x = (fun x ↦ if p x then g x else f x) y
⊢ x = y

Tactic:
rcases em (p x) with (hx | hx) <;> rcases em (p y) with (hy | hy) <;> grind

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

Goal state before:
pp: α : Sort u_1
f : α → α
⊢ (Std.Symm fun x1 x2 ↦ f x1 = x2) ↔ Involutive f

Tactic:
simp [symm_def, Involutive]

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case trans
α : Type u_1
r : α → α → Prop
i✝¹ i✝ a✝ b✝ c✝ : α
h₁✝ : TransGen r a✝ b✝
h₂✝ : TransGen r b✝ c✝
h1 : EqvGen r a✝ b✝
h2 : EqvGen r b✝ c✝
⊢ EqvGen r a✝ c✝

Tactic:
| trans _ _ h1 h2 =>

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case trans
α : Type u_1
r : α → α → Prop
i✝¹ i✝ a✝ b✝ c✝ : α
h₁✝ : ReflTransGen r a✝ b✝
h₂✝ : ReflTransGen r b✝ c✝
h1 : EqvGen r a✝ b✝
h2 : EqvGen r b✝ c✝
⊢ EqvGen r a✝ c✝

Tactic:
| trans _ _ h1 h2 =>

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:
rw [smul_smul, mul_inv_cancel, one_smul]

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

Goal state before:
pp: A : Type u_9
B : Type u_10
G : Type u_11
inst✝⁴ : CommMonoid G
inst✝³ : SMul A G
inst✝² : SMul B G
inst✝¹ : IsScalarTower A G G
inst✝ : IsScalarTower B G G
r : A
s : B
x : G
⊢ (r • 1) • s • x = s • r • x

Tactic:
← one_smul G x,

Goal state after:
A : Type u_9
B : Type u_10
G : Type u_11
inst✝⁴ : CommMonoid G
inst✝³ : SMul A G
inst✝² : SMul B G
inst✝¹ : IsScalarTower A G G
inst✝ : IsScalarTower B G G
r : A
s : B
x : G
⊢ (r • 1) • s • 1 • x = s • r • 1 • x
Module: Mathlib.Order.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : DenselyOrdered α
inst✝ : DenselyOrdered β
a b : α × β
⊢ a < b → ∃ a_2, a < a_2 ∧ a_2 < b

Tactic:
simp_rw [Prod.lt_iff]

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : DenselyOrdered α
inst✝ : DenselyOrdered β
a b : α × β
⊢ a.fst < b.fst ∧ a.snd ≤ b.snd ∨ a.fst ≤ b.fst ∧ a.snd < b.snd →
    ∃ a_2,
      (a.fst < a_2.fst ∧ a.snd ≤ a_2.snd ∨ a.fst ≤ a_2.fst ∧ a.snd < a_2.snd) ∧
        (a_2.fst < b.fst ∧ a_2.snd ≤ b.snd ∨ a_2.fst ≤ b.fst ∧ a_2.snd < b.snd)
Module: Mathlib.Data.Nat.Init

Goal state before:
pp: n : ℕ
motive : (m : ℕ) → n ≤ m → Sort u_1
refl : motive n ⋯
le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯
⊢ le_succ_of_le ?h1 (leRec refl le_succ_of_le ?h1) = le_succ_of_le ⋯ refl

pp: case h1
n : ℕ
motive : (m : ℕ) → n ≤ m → Sort u_1
refl : motive n ⋯
le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯
⊢ n ≤ n

Tactic:
leRec_self

Goal state after:
n : ℕ
motive : (m : ℕ) → n ≤ m → Sort u_1
refl : motive n ⋯
le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯
⊢ le_succ_of_le ?h1 refl = le_succ_of_le ⋯ refl

case h1
n : ℕ
motive : (m : ℕ) → n ≤ m → Sort u_1
refl : motive n ⋯
le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯
⊢ n ≤ n
Module: Mathlib.Data.Nat.Init

Goal state before:
pp: case refl
n m k : ℕ
motive : (m : ℕ) → n ≤ m → Sort u_1
refl : motive n ⋯
le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯
hnm : n ≤ m
⊢ leRec refl le_succ_of_le ⋯ = leRec (leRec refl (fun x h ↦ le_succ_of_le h) hnm) (fun x h ↦ le_succ_of_le ⋯) ⋯

Tactic:
leRec_self

Goal state after:
case refl
n m k : ℕ
motive : (m : ℕ) → n ≤ m → Sort u_1
refl : motive n ⋯
le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯
hnm : n ≤ m
⊢ leRec refl le_succ_of_le ⋯ = leRec refl (fun x h ↦ le_succ_of_le h) hnm
Module: Mathlib.Data.Nat.Init

Goal state before:
pp: n : ℕ
motive : (m : ℕ) → m ≤ n → Sort u_1
of_succ : (k : ℕ) → (h : k < n) → motive (k + 1) h → motive k ⋯
self : motive n ⋯
⊢ leRec (motive := fun {n_1} mn ↦
      {motive : (m : ℕ) → m ≤ n_1 → Sort u_1} →
        ((k : ℕ) → (h : k < n_1) → motive (k + 1) h → motive k ⋯) → motive n_1 ⋯ → motive n mn)
      (fun {motive} of_succ self ↦ self)
      (fun ⦃k⦄ h ih {motive} of_succ self ↦ ih (fun i hi ↦ of_succ i ⋯) (of_succ k ⋯ self)) ⋯ of_succ self =
    self

Tactic:
leRec_self

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

Goal state before:
pp: α : Type u_3
inst✝³ : Preorder α
inst✝² : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝¹ : DecidableLE α
inst✝ : DecidableLT α
x y : α
⊢ cmpLE x y = cmp x y

Tactic:
by_cases xy : x ≤ y <;> by_cases yx : y ≤ x <;> simp [cmpLE, lt_iff_le_not_ge, *, cmp, cmpUsing]

Goal state after:
case neg
α : Type u_3
inst✝³ : Preorder α
inst✝² : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝¹ : DecidableLE α
inst✝ : DecidableLT α
x y : α
xy : ¬x ≤ y
yx : ¬y ≤ x
⊢ False
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
⊢ MonotoneOn (⇑toDual ∘ f ∘ ⇑ofDual) s ↔ MonotoneOn f s

Tactic:
monotoneOn_toDual_comp_iff,

Goal state after:
α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
⊢ AntitoneOn (f ∘ ⇑ofDual) s ↔ MonotoneOn f s
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: α : Type u
inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
⊢ ∃ f, StrictMono f

Tactic:
inhabit α
  rcases Nat.exists_strictMono' (default : α) with ⟨f, hf, hf₀⟩
  rcases Nat.exists_strictAnti' (default : α) with ⟨g, hg, hg₀⟩
  refine ⟨fun n ↦ Int.casesOn n f fun n ↦ g (n + 1), strictMono_int_of_lt_succ ?_⟩
  rintro (n | _ | n)
  · exact hf n.lt_succ_self
  · change g 1 < f 0
    rw [hf₀, ← hg₀]
    exact hg Nat.zero_lt_one
  · exact hg (Nat.lt_succ_self _)

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

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

Tactic:
exact ⟨0, Nat.zero_le _, fun m _ => by induction m with grind⟩

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

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

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

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

Goal state before:
pp: α : Type u_2
inst✝ : HeytingAlgebra α
a b : α
⊢ (a ⊔ b)ᶜ = aᶜ ⊓ bᶜ

Tactic:
← himp_bot,

Goal state after:
α : Type u_2
inst✝ : HeytingAlgebra α
a b : α
⊢ a ⊔ b ⇨ ⊥ = (a ⇨ ⊥) ⊓ (b ⇨ ⊥)
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: α : Type u_2
inst✝ : HeytingAlgebra α
a : α
⊢ a ⇨ aᶜ = aᶜ

Tactic:
← himp_bot,

Goal state after:
α : Type u_2
inst✝ : HeytingAlgebra α
a : α
⊢ a ⇨ a ⇨ ⊥ = a ⇨ ⊥
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: α : Type u_2
inst✝ : HeytingAlgebra α
a b : α
⊢ a ⇨ bᶜ = b ⇨ aᶜ

Tactic:
← himp_bot,

Goal state after:
α : Type u_2
inst✝ : HeytingAlgebra α
a b : α
⊢ a ⇨ b ⇨ ⊥ = b ⇨ a ⇨ ⊥
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: α : Type u_2
inst✝ : HeytingAlgebra α
a b : α
⊢ a ≤ bᶜ ↔ Disjoint a b

Tactic:
← himp_bot,

Goal state after:
α : Type u_2
inst✝ : HeytingAlgebra α
a b : α
⊢ a ≤ b ⇨ ⊥ ↔ Disjoint a b
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: α : Type u_2
inst✝ : HeytingAlgebra α
a b : α
⊢ a ≤ bᶜ ↔ b ≤ aᶜ

Tactic:
by
  rw [le_compl_iff_disjoint_right, le_compl_iff_disjoint_left]

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

Goal state before:
pp: α : Type u_2
inst✝ : HeytingAlgebra α
⊢ ⊥ᶜ = ⊤

Tactic:
← himp_bot,

Goal state after:
α : Type u_2
inst✝ : HeytingAlgebra α
⊢ ⊥ ⇨ ⊥ = ⊤
Module: Mathlib.Order.Heyting.Basic

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

Tactic:
←
      le_compl_iff_disjoint_right

Goal state after:
case a
α : Type u_2
inst✝ : HeytingAlgebra α
a b : α
⊢ aᶜᶜ ⊓ (aᶜᶜ ⇨ bᶜᶜ) ≤ bᶜᶜ
Module: Mathlib.Order.BooleanAlgebra.Set

Goal state before:
pp: α : Type u_1
s : Set α
⊢ s ∪ sᶜ = univ

Tactic:
union_compl_self

Goal state after:
α : Type u_1
s : Set α
⊢ univ = univ
Module: Mathlib.Order.BooleanAlgebra.Set

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

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

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

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

Tactic:
by_cases h : b = x

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

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

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : y = z ⊔ y \ x
⊢ x ≤ z

Tactic:
conv_lhs at H => rw [← sup_sdiff_cancel_right hx]
    refine le_of_inf_le_sup_le ?_ H.le
    rw [inf_sdiff_self_right]
    exact bot_le

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

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

Tactic:
by rw [sup_inf_self, sup_inf_self, inf_idem]

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

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

Tactic:
rw [sup_inf_right]

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

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
f : α → β
s s' : Set β
⊢ range f ∩ s ⊆ range f ∩ s' → f ⁻¹' s ⊆ f ⁻¹' s'

pp: case mpr
α : Type u_1
β : Type u_2
f : α → β
s s' : Set β
⊢ f ⁻¹' s ⊆ f ⁻¹' s' → range f ∩ s ⊆ range f ∩ s'

Tactic:
all_goals
    intro r x hx
    simp_all only [subset_inter_iff, inter_subset_left, true_and, mem_preimage,
      mem_inter_iff, mem_range, true_and]
    aesop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t₁ t₂ : Set β
⊢ s ×ˢ (t₁ ∩ t₂) = s ×ˢ t₁ ∩ s ×ˢ t₂

Tactic:
by
  ext ⟨x, y⟩
  simp only [← and_and_left, mem_inter_iff, mem_prod]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
s t : Set α
⊢ f '' (s \ t ∪ t \ s) = f '' s \ f '' t ∪ f '' t \ f '' s

Tactic:
image_union,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
s t : Set α
⊢ f '' (s \ t) ∪ f '' (t \ s) = f '' s \ f '' t ∪ f '' t \ f '' s
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: case mp
α : Type u_1
s t : Set α
h : Disjoint s t
x : α × α
⊢ (x.1 ∈ s ∨ x.1 ∈ t) ∧ (x.2 ∈ s ∨ x.2 ∈ t) ∧ ¬x.1 = x.2 →
    ((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

Tactic:
rintro ⟨h0 | h0, h1 | h1, h2⟩ <;> simp [h0, h1, h2]

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

Goal state before:
pp: ι : Type u_1
β : ι → Type u_3
inst✝ : DecidableEq ι
x : (i : ι) → β i
i : ι
s : Set (β i)
y : (a : ι) → β a
⊢ y ∈ update x i '' s ↔ y ∈ univ.pi (update (fun j ↦ {x j}) i s)

Tactic:
simp only [mem_image, update_eq_iff, ne_eq, and_left_comm (a := _ ∈ s), exists_eq_left, mem_pi,
    mem_univ, true_implies]

Goal state after:
ι : Type u_1
β : ι → Type u_3
inst✝ : DecidableEq ι
x : (i : ι) → β i
i : ι
s : Set (β i)
y : (a : ι) → β a
⊢ (y i ∈ s ∧ ∀ (x_1 : ι), ¬x_1 = i → x x_1 = y x_1) ↔ ∀ (i_1 : ι), y i_1 ∈ update (fun j ↦ {x j}) i s i_1
Module: Mathlib.Algebra.Group.Equiv.Defs

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
inst✝³ : EquivLike F α β
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
f g : M ≃* N
h₁ : f.toFun = g.toFun
h₂ : f.invFun = g.invFun
⊢ f = g

Tactic:
by
    cases f
    cases g
    congr
    apply Equiv.coe_fn_injective h₁

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

Goal state before:
pp: case refine_2
α : 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₁ ∩ t') \ t)
⊢ f '' (s ∪ r) ⊆ t'

Tactic:
image_union,

Goal state after:
case refine_2
α : 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₁ ∩ t') \ t)
⊢ f '' s ∪ f '' r ⊆ t'
Module: Mathlib.Algebra.Group.Torsion

Goal state before:
pp: G : Type u_2
inst✝¹ : Group G
inst✝ : IsMulTorsionFree G
n : ℕ
x✝ : Int.negSucc n ≠ 0
⊢ Injective fun a ↦ a ^ Int.negSucc n

Tactic:
simpa using! inv_injective.comp (pow_left_injective n.succ_ne_zero)

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

Goal state before:
pp: case refine_4
α : 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₁ ∩ t') \ t)
y : β
hyt' : y ∈ t'
⊢ y ∈ f '' (s ∪ r)

Tactic:
image_union,

Goal state after:
case refine_4
α : 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₁ ∩ t') \ t)
y : β
hyt' : y ∈ t'
⊢ y ∈ f '' s ∪ f '' r
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
s : Set α
h : Semiconj f fa fb
ha : InjOn fa s
hf : InjOn f (fa '' s)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
H : f (fa x) = f (fa y)
⊢ f x = f y

Tactic:
exact congr_arg f (ha hx hy <| hf (mem_image_of_mem fa hx) (mem_image_of_mem fa hy) H)

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

Goal state before:
pp: M : Type u_4
inst✝¹ : MulOneClass M
P : Prop
inst✝ : Decidable P
a b : M
⊢ (if P then a * b else 1) = (if P then a else 1) * if P then b else 1

Tactic:
by_cases h : P

Goal state after:
case pos
M : Type u_4
inst✝¹ : MulOneClass M
P : Prop
inst✝ : Decidable P
a b : M
h : P
⊢ (if P then a * b else 1) = (if P then a else 1) * if P then b else 1

case neg
M : Type u_4
inst✝¹ : MulOneClass M
P : Prop
inst✝ : Decidable P
a b : M
h : ¬P
⊢ (if P then a * b else 1) = (if P then a else 1) * if P then b else 1
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: M : Type u_4
inst✝¹ : MulOneClass M
P : Prop
inst✝ : Decidable P
a b : M
⊢ (if P then 1 else a * b) = (if P then 1 else a) * if P then 1 else b

Tactic:
by_cases h : P

Goal state after:
case pos
M : Type u_4
inst✝¹ : MulOneClass M
P : Prop
inst✝ : Decidable P
a b : M
h : P
⊢ (if P then 1 else a * b) = (if P then 1 else a) * if P then 1 else b

case neg
M : Type u_4
inst✝¹ : MulOneClass M
P : Prop
inst✝ : Decidable P
a b : M
h : ¬P
⊢ (if P then 1 else a * b) = (if P then 1 else a) * if P then 1 else 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₂✝ ℕ
M₂ : Type u_3
inst✝¹ : Inv M₂
inst✝ : InvolutiveInv M₁
f : M₁ → M₂
hf : Surjective f
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
x : M₁
⊢ (f x)⁻¹⁻¹ = f x

Tactic:
by rw [← inv, ← inv, inv_inv]

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

Goal state before:
pp: M₁ : Type u_1
M₂ : Type u_2
inst✝⁶ : Mul M₂
inst✝⁵ : One M₂
inst✝⁴ : Pow M₂ ℕ
inst✝³ : 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
n : ℕ
x : M₁
⊢ f x ^ Int.negSucc n = (f x ^ ↑n.succ)⁻¹

Tactic:
by
      rw [← zpow, ← zpow, zpow_negSucc, zpow_natCast, inv]

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

Goal state before:
pp: M₀ : Type u_1
a b : M₀
inst✝¹ : MulZeroOneClass M₀
inst✝ : IsLeftCancelMulZero M₀
ha : a ≠ 0
⊢ b = 1 ↔ a * b = a

Tactic:
← mul_right_inj' ha,

Goal state after:
M₀ : Type u_1
a b : M₀
inst✝¹ : MulZeroOneClass M₀
inst✝ : IsLeftCancelMulZero M₀
ha : a ≠ 0
⊢ a * b = a * 1 ↔ a * b = a
Module: Mathlib.Data.Nat.Cast.Defs

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoidWithOne R
⊢ 3 + 1 = 4

Tactic:
← two_add_one_eq_three,

Goal state after:
R : Type u_1
inst✝ : AddMonoidWithOne R
⊢ 2 + 1 + 1 = 4
Module: Mathlib.Algebra.Ring.Int.Defs

Goal state before:
pp: α : Type u_1
inst✝ : NonAssocRing α
m : ℤ
⊢ ∀ (n : ℤ), ↑(m * n) = ↑m * ↑n

Tactic:
obtain ⟨m, rfl | rfl⟩ := Int.eq_nat_or_neg m

Goal state after:
case inl
α : Type u_1
inst✝ : NonAssocRing α
m : ℕ
⊢ ∀ (n : ℤ), ↑(↑m * n) = ↑↑m * ↑n

case inr
α : Type u_1
inst✝ : NonAssocRing α
m : ℕ
⊢ ∀ (n : ℤ), ↑(-↑m * n) = ↑(-↑m) * ↑n
Module: Mathlib.Algebra.Group.Nat.Hom

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
a b : M
n : Multiplicative ℕ
⊢ ((powersHom M).toFun (a * b)) n = ((powersHom M).toFun a * (powersHom M).toFun b) n

Tactic:
simp [mul_pow]

Goal state after:
Module: Mathlib.Data.List.TFAE

Goal state before:
pp: case tail.head
a b : Prop
l : List Prop
h : b ∈ l
ab : a ↔ b
H : l.TFAE
p : Prop
hp : Mem p l
⊢ p ↔ a

Tactic:
exact (ab.trans (H _ h _ hp)).symm

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

Goal state before:
pp: M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹ : MulOneClass M
inst✝ : CommMonoid N
f : M →* N
n : ℕ
x y : M
⊢ (⇑f ^ n) (x * y) = (⇑f ^ n) x * (⇑f ^ n) y

Tactic:
simp [mul_pow]

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

Goal state before:
pp: G₀ : Type u_1
inst✝ : GroupWithZero G₀
a x y x' y' : G₀
h : SemiconjBy a x y
h' : SemiconjBy a x' y'
⊢ SemiconjBy a (x * x'⁻¹) (y * y'⁻¹)

Tactic:
exact h.mul_right h'.inv_right₀

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

Goal state before:
pp: α : Type u_2
inst✝² : Add α
inst✝¹ : Mul α
a : α
inst✝ : LeftDistribClass α
ha : Even a
b : α
⊢ Even (b * a)

Tactic:
rcases ha with ⟨k, rfl⟩

Goal state after:
α : Type u_2
inst✝² : Add α
inst✝¹ : Mul α
inst✝ : LeftDistribClass α
b k : α
⊢ Even (b * (k + k))
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝² : Add α
inst✝¹ : Mul α
a : α
inst✝ : RightDistribClass α
ha : Even a
b : α
⊢ Even (a * b)

Tactic:
rcases ha with ⟨k, rfl⟩

Goal state after:
α : Type u_2
inst✝² : Add α
inst✝¹ : Mul α
inst✝ : RightDistribClass α
b k : α
⊢ Even ((k + k) * b)
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

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

Tactic:
← mul_le_mul_iff_left a,

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

Goal state before:
pp: α : Type u
inst✝² : CommGroup α
inst✝¹ : LE α
inst✝ : MulLeftMono α
a b c : α
⊢ c⁻¹ * a ≤ b ↔ a ≤ b * c

Tactic:
by rw [inv_mul_le_iff_le_mul, mul_comm]

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

Goal state before:
pp: α : Type u
inst✝² : CommGroup α
inst✝¹ : LE α
inst✝ : MulLeftMono α
a b c : α
⊢ a / b ≤ c ↔ a ≤ b * c

Tactic:
rw [div_le_iff_le_mul, mul_comm]

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

Goal state before:
pp: α : 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
⊢ a * c = b * d ↔ a = b ∧ c = d

Tactic:
refine ⟨fun h ↦ ?_, by rintro ⟨rfl, rfl⟩; rfl⟩
  simp only [eq_iff_le_not_lt, hab, hcd, true_and]
  refine ⟨fun hab ↦ h.not_lt ?_, fun hcd ↦ h.not_lt ?_⟩
  · exact (mul_le_mul_of_nonneg_left hcd a0.le).trans_lt (mul_lt_mul_of_pos_right hab d0)
  · exact (mul_lt_mul_of_pos_left hcd a0).trans_le (mul_le_mul_of_nonneg_right hab d0.le)

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
⊢ 1 ≤ a ^ n ↔ 1 ≤ a

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ one_le_pow₀ h⟩

Goal state after:
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
h : 1 ≤ a ^ n
⊢ 1 ≤ a
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b : G₀
ha : 0 < a
⊢ a⁻¹ ≤ b ↔ 1 ≤ b * a

Tactic:
by
  rw [← mul_inv_le_iff₀ ha, one_mul]

Goal state after: