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

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
a x y : M
h : SemiconjBy a x y
n : ℕ
⊢ SemiconjBy a (x ^ n) (y ^ n)

Tactic:
by
  induction n with
  | zero =>
    rw [pow_zero, pow_zero]
    exact SemiconjBy.one_right _
  | succ n ih =>
    rw [pow_succ, pow_succ]
    exact ih.mul_right h

Goal state after:
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:
by simpa using irrefl a

Goal state after:
Module: Mathlib.Logic.ExistsUnique

Goal state before:
pp: α : Sort u_1
a' : α
⊢ ∃! a, a = a'

Tactic:
simp only [eq_comm, ExistsUnique, and_self, forall_eq', exists_eq']

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: ι : Sort u_3
inst✝ : Subsingleton ι
P : ι → ι → Prop
i : ι
this : Nonempty ι
⊢ (∀ (j : ι), P i j) ↔ P i i

Tactic:
simp [Subsingleton.elim _ i]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
a b : α
inst✝ : Decidable Q
⊢ (if P ∧ Q then a else b) = if P then if Q then a else b else b

Tactic:
by
  by_cases hp : P <;> by_cases hq : Q <;> simp [hp, hq]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
a b : α
inst✝ : Decidable Q
⊢ (if P ∨ Q then a else b) = if P then a else if Q then a else b

Tactic:
by
  by_cases hp : P <;> by_cases hq : Q <;> simp [hp, hq]

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

Goal state before:
pp: α : Type u_4
β : Type u_5
γ : Sort u_6
f : α → β
g : β → Option α
h : β → γ
i : γ → Option β
hf : IsPartialInv f g
hh : IsPartialInv h i
⊢ IsPartialInv (h ∘ f) fun x ↦ (i x).bind g

Tactic:
intros a b

Goal state after:
α : Type u_4
β : Type u_5
γ : Sort u_6
f : α → β
g : β → Option α
h : β → γ
i : γ → Option β
hf : IsPartialInv f g
hh : IsPartialInv h i
a : α
b : γ
⊢ (fun x ↦ (i x).bind g) b = some a ↔ (h ∘ f) a = b
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: case refl
α : Sort u_3
⊢ Bijective ⋯.mp

Tactic:
exact ⟨fun _ _ ↦ id, fun x ↦ ⟨x, rfl⟩⟩

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

Goal state before:
pp: case refl
α : Sort u_3
⊢ Bijective ⋯.mpr

Tactic:
exact ⟨fun _ _ ↦ id, fun x ↦ ⟨x, rfl⟩⟩

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

Goal state before:
pp: case refl
α : Sort u_3
⊢ Bijective (cast ⋯)

Tactic:
exact ⟨fun _ _ ↦ id, fun x ↦ ⟨x, rfl⟩⟩

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → β → Prop
p : β → γ → Prop
c : γ
a : α
⊢ (flip p ∘r flip r) c a → flip (r ∘r p) c a

Tactic:
· exact fun ⟨b, hbc, hab⟩ ↦ ⟨b, hab, hbc⟩

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case tail
α : Type u_1
r : α → α → Prop
a✝¹ b✝ c : α
h : ∀ (a b c : α), r a b → r a c → ∃ d, ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a✝¹ c
d e : α
a✝ : ReflTransGen r a✝¹ d
hde : r d e
b : α
hdb : ReflTransGen r d b
hcb : ReflTransGen r c b
a : α
hea : ReflTransGen r e a
hba : ReflGen r b a
⊢ Join (ReflTransGen r) e c

Tactic:
cases hba with

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

Goal state before:
pp: α : Sort u
β : Sort v
γ : Sort w
f : α ≃ β
g : α → γ
e' : β → γ
b : β
⊢ extend (⇑f) g e' (f (f.symm b)) = g (f.symm (f (f.symm b)))

Tactic:
f.injective.extend_apply,

Goal state after:
α : Sort u
β : Sort v
γ : Sort w
f : α ≃ β
g : α → γ
e' : β → γ
b : β
⊢ g (f.symm b) = g (f.symm (f (f.symm b)))
Module: Mathlib.Algebra.Notation.Pi.Basic

Goal state before:
pp: ι : Type u_1
M : ι → Type u_6
inst✝¹ : (i : ι) → One (M i)
inst✝ : DecidableEq ι
i : ι
x : M i
h : mulSingle i x = 1
⊢ x = 1

Tactic:
← mulSingle_eq_same i x,

Goal state after:
ι : Type u_1
M : ι → Type u_6
inst✝¹ : (i : ι) → One (M i)
inst✝ : DecidableEq ι
i : ι
x : M i
h : mulSingle i x = 1
⊢ mulSingle i x i = 1
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 • 1 • x = s • r • 1 • x

Tactic:
← smul_assoc s 1 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.Algebra.Group.Pi.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Mul γ
f : α → β
g₁ g₂ : α → γ
e₁ e₂ : β → γ
⊢ extend f (g₁ * g₂) (e₁ * e₂) = extend f g₁ e₁ * extend f g₂ e₂

Tactic:
by
  classical
  funext x
  simp [Function.extend_def, apply_dite₂]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Div γ
f : α → β
g₁ g₂ : α → γ
e₁ e₂ : β → γ
⊢ extend f (g₁ / g₂) (e₁ / e₂) = extend f g₁ e₁ / extend f g₂ e₂

Tactic:
by
  classical
  funext x
  simp [Function.extend_def, apply_dite₂]

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

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

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

Tactic:
· simpa using le_of_eq <| (·.symm) <| compare_eq_iff_eq.1 h

Goal state after:
case gt
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.gt
⊢ Ordering.gt ≠ Ordering.lt ↔ b ≤ a
Module: Mathlib.Order.RelClasses

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝ : IsOrderConnected α r
a b c : α
h₁ : ¬r a b
h₂ : ¬r b c
⊢ ¬(r a b ∨ r b c)

Tactic:
simp [h₁, h₂]

Goal state after:
Module: Mathlib.Order.RelClasses

Goal state before:
pp: α : Type u
β : Type v
r✝ : α → α → Prop
s : β → β → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a b c : α
hab : r a b
hbc : r b c
⊢ r a c

Tactic:
by
    rcases trichotomous_of r a c with (hac | rfl | hca)
    · exact hac
    · exact asymm_of r hab hbc |>.elim
    · exact IsWellFounded.wf.asymmetric₃ a b c hab hbc hca |>.elim

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

Goal state before:
pp: 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
hlt : f 1 < f 0
g : ℕ → ℕ := fun i ↦ f (i + 1)
⊢ Antitone g

Tactic:
grind [Antitone]

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst✝¹ : LinearOrder α
inst✝ : SemilatticeInf β
hf : AntitoneOn f s
hx : x ∈ s
hy : y ∈ s
⊢ f (max x y) = f x ⊓ f y

Tactic:
by
  cases le_total x y <;> have := hf ?_ ?_ ‹_› <;>
    first
    | assumption
    | simp only [*, sup_of_le_left, sup_of_le_right, inf_of_le_left, inf_of_le_right]

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

Goal state before:
pp: ι : Type u_1
α✝ : Type u_2
β : Type u_3
inst✝¹ : GeneralizedHeytingAlgebra α✝
a b c d : α✝
α : ι → Type u_4
inst✝ : (i : ι) → GeneralizedHeytingAlgebra (α i)
i : (i : ι) → α i
⊢ ∀ (b c : (i : ι) → α i), i ≤ b ⇨ c ↔ i ⊓ b ≤ c

Tactic:
simp [le_def]

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

Goal state before:
pp: ι : Type u_1
α✝ : Type u_2
β : Type u_3
inst✝¹ : GeneralizedCoheytingAlgebra α✝
a b c d : α✝
α : ι → Type u_4
inst✝ : (i : ι) → GeneralizedCoheytingAlgebra (α i)
i : (i : ι) → α i
⊢ ∀ (b c : (i : ι) → α i), i \ b ≤ c ↔ i ≤ b ⊔ c

Tactic:
simp [le_def]

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

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

Tactic:
by
  simp_rw [← le_compl_iff_disjoint_right, compl_compl_compl]

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

Goal state before:
pp: α : Type u
β : Type u_1
x✝ y✝ z✝ : α
inst✝ : GeneralizedBooleanAlgebra α
y x z : α
h : y ≤ x ⊔ z
⊢ x ⊔ z ⊔ x ≤ z ⊔ x

Tactic:
rw [sup_assoc, sup_comm, sup_assoc, sup_idem]

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

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

Tactic:
rw [sup_inf_sdiff, h, sup_inf_sdiff]

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

Goal state before:
pp: α : Type u_9
β : Type u_10
γ : α → β → Type u_11
a : α
b : β
s : { s // s.fst = a ∧ s.snd.fst = b }
⊢ (sigmaSigmaSubtypeEq a b) s = cast ⋯ (↑s).snd.snd

Tactic:
by
  simp [sigmaSigmaSubtypeEq]

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

Goal state before:
pp: α : Type u_9
β : Type u_10
γ : α → β → Type u_11
a : α
b : β
c : γ a b
⊢ (sigmaSigmaSubtypeEq a b).symm c = ⟨⟨a, ⟨b, c⟩⟩, ⋯⟩

Tactic:
by
  simp [sigmaSigmaSubtypeEq]

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

Goal state before:
pp: α₁ : Type u_9
β₁ : Type u_10
inst✝ : DecidableEq α₁
e : Perm β₁
a a' : α₁
b : β₁
h : (prodExtendRight a e) (a', b) ≠ (a', b)
⊢ a' = a

Tactic:
contrapose! h
  exact prodExtendRight_apply_ne _ h _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
t : Set β
f : α → β
u : Set ↑t
⊢ t.restrictPreimage f ⁻¹' u = Subtype.val ⁻¹' Subtype.val '' t.restrictPreimage f ⁻¹' u

Tactic:
preimage_image_eq _ Subtype.val_injective

Goal state after:
α : Type u_1
β : Type u_2
t : Set β
f : α → β
u : Set ↑t
⊢ t.restrictPreimage f ⁻¹' u = t.restrictPreimage f ⁻¹' u
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
⊢ range Sum.inl = {x | x.isLeft = true}

Tactic:
ext (_ | _) <;> simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
⊢ range Sum.inr = {x | x.isRight = true}

Tactic:
ext (_ | _) <;> simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Set γ
f : α → γ
g : β → γ
⊢ Sum.elim f g ⁻¹' s = Sum.inl '' f ⁻¹' s ∪ Sum.inr '' g ⁻¹' s

Tactic:
ext (_ | _) <;> simp

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

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
δ : α → Type u_8
t : Set α
t' : (i : α) → Set (δ i)
f g : (i : α) → δ i
hf : f ∈ t.pi t'
hg : g ∈ t.pi t'
⊢ s.piecewise f g ∈ t.pi t'

Tactic:
intro i ht

Goal state after:
α : Type u_1
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
δ : α → Type u_8
t : Set α
t' : (i : α) → Set (δ i)
f g : (i : α) → δ i
hf : f ∈ t.pi t'
hg : g ∈ t.pi t'
i : α
ht : i ∈ t
⊢ s.piecewise f g i ∈ t' i
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s : Set ι
f : (i : ι) → α i → β i
hf : ∀ (i : ι), ¬i ∈ s → Surjective (f i)
t : (i : ι) → Set (α i)
b : (i : ι) → β i
hb : b ∈ s.pi fun i ↦ f i '' t i
i : ι
hi : ¬i ∈ s
⊢ ∃ a, f i a = b i ∧ (i ∈ s → a ∈ t i)

Tactic:
exact (hf i hi (b i)).imp fun a ha ↦ ⟨ha, (absurd · hi)⟩

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
h : s.pi t₁ ⊆ s.pi t₂
⊢ (s.pi t₁).Nonempty → ∀ (i : ι), i ∈ s → t₁ i ⊆ t₂ i

Tactic:
intro hne

Goal state after:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
h : s.pi t₁ ⊆ s.pi t₂
hne : (s.pi t₁).Nonempty
⊢ ∀ (i : ι), i ∈ s → t₁ i ⊆ t₂ i
Module: Mathlib.Data.Set.Function

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
f : α → β
h : Disjoint s₁ s₂
h₁ : InjOn f s₁
h₂ : InjOn f s₂
h₁₂ : ∀ (x : α), x ∈ s₁ → ∀ (y : α), y ∈ s₂ → f x ≠ f y
⊢ InjOn f (s₁ ∪ s₂)

Tactic:
rintro x (hx | hx) y (hy | hy) hxy

Goal state after:
case refine_2.inl.inl
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
f : α → β
h : Disjoint s₁ s₂
h₁ : InjOn f s₁
h₂ : InjOn f s₂
h₁₂ : ∀ (x : α), x ∈ s₁ → ∀ (y : α), y ∈ s₂ → f x ≠ f y
x : α
hx : x ∈ s₁
y : α
hy : y ∈ s₁
hxy : f x = f y
⊢ x = y

case refine_2.inl.inr
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
f : α → β
h : Disjoint s₁ s₂
h₁ : InjOn f s₁
h₂ : InjOn f s₂
h₁₂ : ∀ (x : α), x ∈ s₁ → ∀ (y : α), y ∈ s₂ → f x ≠ f y
x : α
hx : x ∈ s₁
y : α
hy : y ∈ s₂
hxy : f x = f y
⊢ x = y

case refine_2.inr.inl
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
f : α → β
h : Disjoint s₁ s₂
h₁ : InjOn f s₁
h₂ : InjOn f s₂
h₁₂ : ∀ (x : α), x ∈ s₁ → ∀ (y : α), y ∈ s₂ → f x ≠ f y
x : α
hx : x ∈ s₂
y : α
hy : y ∈ s₁
hxy : f x = f y
⊢ x = y

case refine_2.inr.inr
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
f : α → β
h : Disjoint s₁ s₂
h₁ : InjOn f s₁
h₂ : InjOn f s₂
h₁₂ : ∀ (x : α), x ∈ s₁ → ∀ (y : α), y ∈ s₂ → f x ≠ f y
x : α
hx : x ∈ s₂
y : α
hy : y ∈ s₂
hxy : f x = f y
⊢ x = y
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s t u : Set α
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
⊢ f '' s ∩ f '' t ⊆ f '' (s ∩ t)

Tactic:
intro x ⟨⟨y, ys, hy⟩, ⟨z, zt, hz⟩⟩

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s t u : Set α
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
x : β
y : α
ys : y ∈ s
hy : f y = x
z : α
zt : z ∈ t
hz : f z = x
⊢ x ∈ f '' (s ∩ t)
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
⊢ InjOn Prod.fst (graphOn f s)

Tactic:
aesop (add simp InjOn)

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

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

Tactic:
intro b

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
f : α → β
g₁ g₂ : β → γ
hf : EqOn (g₁ ∘ f) (g₂ ∘ f) s
hf' : SurjOn f s t
b : β
⊢ b ∈ t → g₁ b = g₂ b
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s : Set α
t : Set β
f : α → β
p₁ : α → γ
p₂ : β → δ
g : γ → δ
comm : ∀ (a : α), p₂ (f a) = g (p₁ a)
hinj : InjOn g (p₁ '' s)
h1 : MapsTo f s t
h2 : InjOn f s
h3 : SurjOn f s t
a : α
ha : a ∈ s
⊢ p₂ (f a) = g (p₁ a)

Tactic:
comm a

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s : Set α
t : Set β
f : α → β
p₁ : α → γ
p₂ : β → δ
g : γ → δ
comm : ∀ (a : α), p₂ (f a) = g (p₁ a)
hinj : InjOn g (p₁ '' s)
h1 : MapsTo f s t
h2 : InjOn f s
h3 : SurjOn f s t
a : α
ha : a ∈ s
⊢ g (p₁ a) = g (p₁ a)
Module: Mathlib.Algebra.Group.Hom.Defs

Goal state before:
pp: ι : 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
F : Type u_9
inst✝⁵ : MulOne M✝
inst✝⁴ : MulOne N✝
inst✝³ : FunLike F M✝ N✝
inst✝² : MonoidHomClass F M✝ N✝
M : Type u_10
N : Type u_11
inst✝¹ : Monoid M
inst✝ : LeftCancelMonoid N
f : M →ₙ* N
⊢ f 1 = 1

Tactic:
have h : f 1 * 1 = f 1 * f 1 := by simpa using f.map_mul' 1 1

Goal state after:
ι : 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
F : Type u_9
inst✝⁵ : MulOne M✝
inst✝⁴ : MulOne N✝
inst✝³ : FunLike F M✝ N✝
inst✝² : MonoidHomClass F M✝ N✝
M : Type u_10
N : Type u_11
inst✝¹ : Monoid M
inst✝ : LeftCancelMonoid N
f : M →ₙ* N
h : f 1 * 1 = f 1 * f 1
⊢ f 1 = 1
Module: Mathlib.Data.Set.Function

Goal state before:
pp: case e'_5
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
h₁ : BijOn f s t
h₂ : a ∈ s
⊢ t \ {f a} = f '' (s \ {a})

Tactic:
simp [h₁.injOn.image_sdiff, h₁.image_eq, h₂, inter_eq_self_of_subset_right]

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

Goal state before:
pp: case h₂
α : Type u_1
β : Type u_2
s s₁ : Set α
f : α → β
f' : β → α
hf : LeftInvOn f' f s
x : α
h : x ∈ s
h₁ : f x ∈ f' ⁻¹' s₁
⊢ f x ∈ f '' (s₁ ∩ s)

Tactic:
exact mem_image_of_mem _ ⟨by rwa [← hf h], h⟩

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

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

Tactic:
rw [b.sub_self, ← cast_eq_iff_heq]; rfl

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

Goal state before:
pp: ι : Type u_1
inst✝¹ : DecidableEq ι
M : ι → Type u_2
inst✝ : (i : ι) → AddMonoid (M i)
i : ι
a : M i
j : ι
⊢ mulSingle i (ofAdd a) j = ofAdd (single i a j)

Tactic:
rcases eq_or_ne j i with rfl | h
  · simp only [mulSingle_eq_same, single_eq_same]
  · simp only [mulSingle, ne_eq, h, not_false_eq_true, Function.update_of_ne, one_apply, single,
      zero_apply, ofAdd_zero]

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

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

Tactic:
by rw [div_eq_mul_inv, one_div]

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

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

Tactic:
by rw [h, inv_mul_cancel]

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

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

Tactic:
intro b

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
u : Mˣ
x✝ : IsUnit (a * ↑u)
v : Mˣ
hv : ↑v = a * ↑u
⊢ IsUnit a

Tactic:
by
      have : IsUnit (a * ↑u * ↑u⁻¹) := by exists v * u⁻¹; rw [← hv, Units.val_mul]
      rwa [mul_assoc, Units.mul_inv, mul_one] at this

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

Goal state before:
pp: M : Type u
N : Type v
inst✝¹ : Monoid M
inst✝ : Monoid N
f : M →* N
g : M → Nˣ
h : ∀ (x : M), ↑(g x) = f x
x : M
⊢ ↑((liftRight f g h) x)⁻¹ * f x = 1

Tactic:
rw [Units.inv_mul_eq_iff_eq_mul, mul_one, coe_liftRight]

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

Goal state before:
pp: case ofNat
α : Type u_4
p : α → Prop
f : Perm α
hf : ∀ (x : α), p (f x) ↔ p x
n : ℕ
⊢ f.subtypePerm hf ^ Int.ofNat n = (f ^ Int.ofNat n).subtypePerm ⋯

Tactic:
exact subtypePerm_pow _ _ _

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

Goal state before:
pp: R : Type u_1
inst✝¹ : AddMonoid R
inst✝ : One R
n : ℕ
this : AddMonoidWithOne R := AddMonoidWithOne.unary
⊢ (n + 1).binCast = n.binCast + 1

Tactic:
rw [Nat.binCast_eq, Nat.binCast_eq, Nat.cast_succ]

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

Goal state before:
pp: M : Type u_1
M₀ : Type u_2
M₀' : Type u_3
G₀ : Type u_4
G₀' : Type u_5
N : Type u_6
A : Type u_7
A' : Type u_8
B : Type u_9
α : Type u_10
β : Type u_11
inst✝⁵ : Zero M₀
inst✝⁴ : Zero A
inst✝³ : SMulWithZero M₀ A
a : M₀
b : A
inst✝² : Zero M₀'
inst✝¹ : Zero A'
inst✝ : SMul M₀ A'
f : ZeroHom A A'
hf : Surjective ⇑f
smul : ∀ (a : M₀) (b : A), f (a • b) = a • f b
c : M₀
⊢ c • 0 = 0

Tactic:
by rw [← f.map_zero, ← smul, smul_zero]

Goal state after:
Module: Mathlib.Algebra.Group.Int.Even

Goal state before:
pp: n : ℤ
x✝ : Even n
m : ℤ
hm : n = m + m
⊢ n % 2 = 0

Tactic:
by simp [← Int.two_mul, hm]

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

Goal state before:
pp: a : Prop
l : List Prop
⊢ (a :: a :: l).TFAE ↔ (a :: l).TFAE

Tactic:
simp [tfae_cons_cons]

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
u : Mˣ
x : M
⊢ ↑u * x = ↑u * x * ↑u⁻¹ * ↑u

Tactic:
Units.inv_mul_cancel_right

Goal state after:
M : Type u_1
inst✝ : Monoid M
u : Mˣ
x : M
⊢ ↑u * x = ↑u * x
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
m n : ℕ
a : G₀
ha : a ≠ 0
h : n ≤ m
h1 : m - n + n = m
⊢ a ^ (m - n) * a ^ n = a ^ m

Tactic:
rw [← pow_add, h1]

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

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
m n : ℕ
a : G₀
h : n < m
⊢ a⁻¹ ^ (m - n) = (a ^ m)⁻¹ * a ^ n

Tactic:
rw [pow_sub_of_lt a⁻¹ h, inv_pow, inv_pow, inv_inv]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
a : R
n : ℕ
⊢ (-1) ^ n * a = 0 ↔ a = 0

Tactic:
by
  rcases neg_one_pow_eq_or R n with h | h <;> simp [h]

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
a : R
inst✝ : NoZeroDivisors R
⊢ a ^ 2 = 1 ↔ a = 1 ∨ a = -1

Tactic:
by
  rw [← (Commute.one_right a).sq_eq_sq_iff_eq_or_eq_neg, one_pow]

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

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

Tactic:
rw [← inv_mul_cancel_left a b, ← inv_mul_cancel_left a c]

Goal state after:
case refine_1
N : Type u_2
r : N → N → Prop
inst✝ : Group N
h : Covariant N N (fun x1 x2 ↦ x1 * x2) r
a b c : N
bc : r ((fun x1 x2 ↦ x1 * x2) a b) ((fun x1 x2 ↦ x1 * x2) a c)
⊢ r (a⁻¹ * (a * b)) (a⁻¹ * (a * c))
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: case succ
α : Type u_2
inst✝¹ : Semiring α
a b : α
inst✝ : IsCancelAdd α
hab : a + b = 0
k : ℕ
ih : a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0
⊢ a ^ (2 * (k + 1) + 1) + b ^ (2 * (k + 1) + 1) = 0

Tactic:
have : a ^ 2 = b ^ 2 := add_right_cancel <|
    calc
      a ^ 2 + a * b = 0 := by rw [sq, ← mul_add, hab, mul_zero]
      _ = b ^ 2 + a * b := by rw [sq, ← add_mul, add_comm, hab, zero_mul]

Goal state after:
case succ
α : Type u_2
inst✝¹ : Semiring α
a b : α
inst✝ : IsCancelAdd α
hab : a + b = 0
k : ℕ
ih : a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0
this : a ^ 2 = b ^ 2
⊢ a ^ (2 * (k + 1) + 1) + b ^ (2 * (k + 1) + 1) = 0
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝¹ : DivisionMonoid α
inst✝ : HasDistribNeg α
n : ℤ
⊢ (-1) ^ n = if Even n then 1 else -1

Tactic:
obtain ⟨n, _⟩ := n.eq_nat_or_neg
  aesop (add safe (by rw [neg_one_pow_eq_ite]))

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

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

Tactic:
by
  rw [lt_iff_le_and_ne, ← tsub_le_iff_left]
  refine ⟨h.le, ?_⟩
  rintro rfl
  simp [hb] at h

Goal state after:
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 : 0 ≤ a
n : ℕ
⊢ 0 ≤ a ^ n

Tactic:
exact pow_nonneg ha _

Goal state after:
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 : 0 ≤ a
n : ℕ
⊢ 0 ≤ a ^ (n + 1)

Tactic:
exact pow_nonneg ha _

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
⊢ ∀ {a b : α × β →o γ},
    { toFun := fun f ↦ { toFun := fun x ↦ { toFun := Function.curry (⇑f) x, monotone' := ⋯ }, monotone' := ⋯ },
            invFun := fun f ↦ { toFun := Function.uncurry fun x ↦ ⇑(f x), monotone' := ⋯ }, left_inv := ⋯,
            right_inv := ⋯ }
          a ≤
        { toFun := fun f ↦ { toFun := fun x ↦ { toFun := Function.curry (⇑f) x, monotone' := ⋯ }, monotone' := ⋯ },
            invFun := fun f ↦ { toFun := Function.uncurry fun x ↦ ⇑(f x), monotone' := ⋯ }, left_inv := ⋯,
            right_inv := ⋯ }
          b ↔
      a ≤ b

Tactic:
simp [le_def]

Goal state after: