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

Goal state before:
pp: S : Type u_3
inst✝ : Semigroup S
a b : S
reg : IsRightRegular a
⊢ Commute (b * a) a ↔ Commute a b

Tactic:
by
  simp [commute_iff_eq, ← mul_assoc, reg.eq_iff, eq_comm]

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

Goal state before:
pp: ⊢ @npowRecAuto = @npowBinRecAuto

Tactic:
by
  funext M _ _ k m
  rw [npowBinRecAuto, npowRecAuto, npowBinRec]
  match k with
  | 0 => rw [npowRec, npowBinRec.go, Nat.binaryRec_zero]
  | k + 1 => rw [npowBinRec.go_spec, npowRec_eq]

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

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
ex : ∀ (x y : M), x * y = 1 → ∃ z, y * z = 1
x y : M
h : x * y = 1
z : M
hz : y * z = 1
⊢ x = z

Tactic:
simpa [← mul_assoc, h] using congr_arg (x * ·) hz.symm

Goal state after:
Module: Mathlib.Logic.Unique

Goal state before:
pp: α : Sort u_1
inst✝ : Unique α
β : α → Sort v
f : (a : α) → β a
i x✝¹ : α
x✝ : i ≍ x✝¹
⊢ f i ≍ Function.const α (f default) x✝¹

Tactic:
rw [Subsingleton.elim i default]; rfl

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

Goal state before:
pp: case neg
γ : Sort u_3
α₁ : Sort u_4
α₂ : Sort u_5
α₃ : Sort u_6
f₁₂ : α₁ → α₂
h₁₂ : Injective f₁₂
f₂₃ : α₂ → α₃
h₂₃ : Injective f₂₃
g : α₁ → γ
e' : α₃ → γ
a : α₃
h₃ : ¬∃ b, f₂₃ b = a
⊢ extend (f₂₃ ∘ f₁₂) g e' a = extend f₂₃ (extend f₁₂ g (e' ∘ f₂₃)) e' a

Tactic:
rw [extend_apply' _ _ _ h₃, extend_apply']

Goal state after:
case neg.hb
γ : Sort u_3
α₁ : Sort u_4
α₂ : Sort u_5
α₃ : Sort u_6
f₁₂ : α₁ → α₂
h₁₂ : Injective f₁₂
f₂₃ : α₂ → α₃
h₂₃ : Injective f₂₃
g : α₁ → γ
e' : α₃ → γ
a : α₃
h₃ : ¬∃ b, f₂₃ b = a
⊢ ¬∃ a_1, (f₂₃ ∘ f₁₂) a_1 = a
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_2
f✝ : α → β
γ : Type u_4
inst✝ : Nontrivial γ
surj : Surjective fun g ↦ g ∘ f✝
c c' : γ
not_inj : ∃ x x_1 x_2, ¬x = x_1
a₁ a₂ : α
eq : f✝ a₁ = f✝ a₂
ne : ¬a₁ = a₂
f : β → γ
hf : (fun g ↦ g ∘ f✝) f = fun x ↦ if x = a₂ then c else c'
h₁ : f (f✝ a₁) = c'
h₂ : f (f✝ a₂) = c
⊢ c = c'

Tactic:
← h₁,

Goal state after:
α : Sort u_1
β : Sort u_2
f✝ : α → β
γ : Type u_4
inst✝ : Nontrivial γ
surj : Surjective fun g ↦ g ∘ f✝
c c' : γ
not_inj : ∃ x x_1 x_2, ¬x = x_1
a₁ a₂ : α
eq : f✝ a₁ = f✝ a₂
ne : ¬a₁ = a₂
f : β → γ
hf : (fun g ↦ g ∘ f✝) f = fun x ↦ if x = a₂ then c else c'
h₁ : f (f✝ a₁) = c'
h₂ : f (f✝ a₂) = c
⊢ c = f (f✝ a₁)
Module: Mathlib.Logic.Relation

Goal state before:
pp: case refl
α : Type u_1
r p : α → α → Prop
hrp : r ≤ p
i✝¹ i✝ x✝ : α
⊢ EqvGen p x✝ x✝

Tactic:
exact EqvGen.refl _

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
    | refl => exact ⟨b, hea, hcb⟩
    | single hba => exact ⟨a, hea, hcb.tail hba⟩

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

Goal state before:
pp: I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f i
i : I
inst✝ : (i : I) → DivInvMonoid (f i)
a✝ : (i : I) → f i
x✝ : I
⊢ (a✝ ^ 0) x✝ = 1 x✝

Tactic:
exact DivInvMonoid.zpow_zero' _

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

Goal state before:
pp: I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f i
i : I
inst✝ : (i : I) → InvolutiveInv (f i)
⊢ ∀ (x : (i : I) → f i), x⁻¹⁻¹ = x

Tactic:
by intros; ext; exact inv_inv _

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a : α
⊢ min a a = a

Tactic:
rw [min_def, ite_id]

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝¹ : (i : ι) → Preorder (π i)
inst✝ : ∀ (i : ι), DenselyOrdered (π i)
a b : (i : ι) → π i
hab : a ≤ b
i : ι
hi : a i < b i
c : π i
ha : a i < c
hb : c < b i
⊢ ∃ a_1, (a ≤ a_1 ∧ ∃ i, a i < a_1 i) ∧ a_1 ≤ b ∧ ∃ i, a_1 i < b i

Tactic:
exact
        ⟨Function.update a i c,
          ⟨le_update_iff.2 ⟨ha.le, fun _ _ ↦ le_rfl⟩, i, by rwa [update_self]⟩,
          update_le_iff.2 ⟨hb.le, fun _ _ ↦ hab _⟩, i, by rwa [update_self]⟩

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

Goal state before:
pp: m n : ℕ
motive : (m : ℕ) → m ≤ n → Sort u_1
of_succ : (k : ℕ) → (h : k < n) → motive (k + 1) h → motive k ⋯
self : motive n ⋯
smn : m + 1 ≤ n
mn : m ≤ n
⊢ decreasingInduction of_succ self mn = of_succ m smn (decreasingInduction of_succ self smn)

Tactic:
by
  rw [Subsingleton.elim mn (Nat.le_trans (le_succ m) smn),
    decreasingInduction_trans (n := m + 1) (Nat.le_succ m),
    decreasingInduction_succ']

Goal state after:
Module: Mathlib.Order.Compare

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, o.Compares a b → o.Compares a' b'
o : Ordering
ho : o.Compares a' b'
⊢ o.Compares a b

Tactic:
rcases lt_trichotomy a b with hab | hab | hab

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, o.Compares a b → o.Compares a' b'
o : Ordering
ho : o.Compares a' b'
hab : a < b
⊢ o.Compares a b

case inr.inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, o.Compares a b → o.Compares a' b'
o : Ordering
ho : o.Compares a' b'
hab : a = b
⊢ o.Compares a b

case inr.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, o.Compares a b → o.Compares a' b'
o : Ordering
ho : o.Compares a' b'
hab : b < a
⊢ o.Compares a b
Module: Mathlib.Order.BoundedOrder.Lattice

Goal state before:
pp: case ind
α : Type u_1
inst✝² : Preorder α
inst✝¹ : WellFoundedGT α
inst✝ : OrderTop α
P : α → Prop
hind : ∀ (N : α), N ≠ ⊤ → P N → ∃ M, M > N ∧ P M
hexists : ¬P ⊤
x : α
IH : ∀ (y : α), x < y → ¬P y
⊢ ¬P x

Tactic:
by_cases hx : x = ⊤

Goal state after:
case pos
α : Type u_1
inst✝² : Preorder α
inst✝¹ : WellFoundedGT α
inst✝ : OrderTop α
P : α → Prop
hind : ∀ (N : α), N ≠ ⊤ → P N → ∃ M, M > N ∧ P M
hexists : ¬P ⊤
x : α
IH : ∀ (y : α), x < y → ¬P y
hx : x = ⊤
⊢ ¬P x

case neg
α : Type u_1
inst✝² : Preorder α
inst✝¹ : WellFoundedGT α
inst✝ : OrderTop α
P : α → Prop
hind : ∀ (N : α), N ≠ ⊤ → P N → ∃ M, M > N ∧ P M
hexists : ¬P ⊤
x : α
IH : ∀ (y : α), x < y → ¬P y
hx : ¬x = ⊤
⊢ ¬P x
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
β : Type v
e : α ≃ β
inst✝ : PartialOrder β
preorder : Preorder α := e.preorder
⊢ PartialOrder α

Tactic:
apply e.injective.partialOrder

Goal state after:
case le
α : Type u
β : Type v
e : α ≃ β
inst✝ : PartialOrder β
preorder : Preorder α := ⋯
⊢ ∀ {x y : α}, e x ≤ e y ↔ x ≤ y

case lt
α : Type u
β : Type v
e : α ≃ β
inst✝ : PartialOrder β
preorder : Preorder α := ⋯
⊢ ∀ {x y : α}, e x < e y ↔ x < y
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c : α
h : a ⊔ c ≤ b ⊔ c
⊢ a \ c ≤ b \ c

Tactic:
by
  rw [← sup_sdiff_right_self, ← @sup_sdiff_right_self _ _ b]
  exact sdiff_le_sdiff_right h

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

Goal state before:
pp: α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
hx : y ≤ x
hy : y ≠ ⊥
h : x \ y = x
⊢ y = ⊥

Tactic:
sdiff_eq_left,

Goal state after:
α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
hx : y ≤ x
hy : y ≠ ⊥
h : Disjoint x y
⊢ y = ⊥
Module: Mathlib.Order.BooleanAlgebra.Basic

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

Tactic:
inf_sdiff_self_left,

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ (⊥ ⊓ x) ⊔ x ⊓ y \ z ⊓ x \ y = x ⊓ y \ z ⊓ x \ y
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
α β : Type ?u.15
s : (b : Bool) × bif b then β else α
⊢ (fun s ↦ Sum.elim (fun x ↦ ⟨false, x⟩) (fun x ↦ ⟨true, x⟩) s)
      ((fun s ↦
          match s with
          | ⟨false, a⟩ => inl a
          | ⟨true, b⟩ => inr b)
        s) =
    s

Tactic:
rcases s with ⟨_ | _, _⟩

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.15
snd✝ : bif false then β else α
⊢ (fun s ↦ Sum.elim (fun x ↦ ⟨false, x⟩) (fun x ↦ ⟨true, x⟩) s)
      ((fun s ↦
          match s with
          | ⟨false, a⟩ => inl a
          | ⟨true, b⟩ => inr b)
        ⟨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.15
snd✝ : bif true then β else α
⊢ (fun s ↦ Sum.elim (fun x ↦ ⟨false, x⟩) (fun x ↦ ⟨true, x⟩) s)
      ((fun s ↦
          match s with
          | ⟨false, a⟩ => inl a
          | ⟨true, b⟩ => inr b)
        ⟨true, snd✝⟩) =
    ⟨true, snd✝⟩
Module: Mathlib.Order.BooleanAlgebra.Basic

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

Tactic:
refine (sup_le_sup_left h.le _).lt_of_not_ge fun h' => h.not_ge ?_

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
h : y < z \ x
hxz : x ≤ z
h' : x ⊔ z \ x ≤ x ⊔ y
⊢ z \ x ≤ y
Module: Mathlib.Logic.Equiv.Basic

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
p : α → Prop
q : β → Prop
r : γ → Prop
e : α ≃ β
f : β ≃ γ
h : ∀ (a : α), p a ↔ q (e a)
h' : ∀ (b : β), q b ↔ r (f b)
⊢ ∀ (a : α), p a ↔ r ((e.trans f) a)

Tactic:
as_aux_lemma => exact fun a => (h a).trans (h' <| e a)

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

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.23
π : ι → Type u_9
f : { f // ∀ (i : ι), (f i).fst = i }
i : ι
⊢ π i

Tactic:
← f.2 i

Goal state after:
α : 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.23
π : ι → Type u_9
f : { f // ∀ (i : ι), (f i).fst = i }
i : ι
⊢ π (↑f i).fst
Module: Mathlib.Logic.Equiv.Basic

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
β : α → Sort v
p : (a : α) → β a → Prop
⊢ LeftInverse (fun f ↦ ⟨fun a ↦ ↑(f a), ⋯⟩) fun f a ↦ ⟨↑f a, ⋯⟩

Tactic:
by
    rintro ⟨f, h⟩
    rfl

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

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
p₁ : α → Prop
s₁ : Setoid α
s₂ : Setoid (Subtype p₁)
p₂ : Quotient s₁ → Prop
hp₂ : ∀ (a : α), p₁ a ↔ p₂ ⟦a⟧
h : ∀ (x y : Subtype p₁), s₂ x y ↔ s₁ ↑x ↑y
a : Quotient s₂
⊢ (fun a ↦ Quotient.hrecOn (motive := fun x ↦ p₂ x → Quotient s₂) (↑a) (fun a h ↦ ⟦⟨a, ⋯⟩⟧) ⋯ ⋯)
      ((fun a ↦ a.liftOn (fun a ↦ ⟨⟦↑a⟧, ⋯⟩) ⋯) a) =
    a

Tactic:
by induction a using Quotient.inductionOn; rfl

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

Goal state before:
pp: α : Sort u_1
β : Sort u_4
inst✝ : DecidableEq α
f : α ≃ β
a : α
b : β
⊢ (f.setValue a b) a = b

Tactic:
by
  simp [setValue, swap_apply_left]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
s : Set β
⊢ ∃ a, f '' a = s

Tactic:
use f ⁻¹' s

Goal state after:
case h
α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
s : Set β
⊢ f '' f ⁻¹' s = s
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s₁ s₂ : Set ι
t : (i : ι) → Set (α i)
⊢ (s₁ ∪ s₂).pi t = s₁.pi t ∩ s₂.pi t

Tactic:
by
  simp [pi, or_imp, forall_and, ofPred_and]

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

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

Tactic:
refine ⟨fun H => ⟨H.mono subset_union_left, H.mono subset_union_right, ?_⟩, ?_⟩
  · intro x hx y hy hxy
    obtain rfl : x = y := H (Or.inl hx) (Or.inr hy) hxy
    exact h.le_bot ⟨hx, hy⟩
  · rintro ⟨h₁, h₂, h₁₂⟩
    rintro x (hx | hx) y (hy | hy) hxy
    exacts [h₁ hx hy hxy, (h₁₂ _ hx _ hy hxy).elim, (h₁₂ _ hy _ hx hxy.symm).elim, h₂ hx hy hxy]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
f' : β → α
h : LeftInvOn f' f s
hf : SurjOn f s t
y : β
hy : y ∈ t
⊢ f' y ∈ s

Tactic:
let ⟨x, hs, hx⟩ := hf hy

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
f' : β → α
h : LeftInvOn f' f s
hf : SurjOn f s t
y : β
hy : y ∈ t
x : α
hs : x ∈ s
hx : f x = y
⊢ f' y ∈ s
Module: Mathlib.Data.Int.Init

Goal state before:
pp: case pos
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 : z ≤ b
h✝ : z = b
⊢ cast ⋯
      (match z - 1 - b with
      | ofNat n => inductionOn'.pos b zero succ n
      | -[n+1] =>
        match n with
        | 0 => pred b ⋯ zero
        | n.succ => cast ⋯ (pred (b + -[n+1]) ⋯ (inductionOn'.neg b zero pred n))) =
    pred z hz
      (cast ⋯
        (match z - b with
        | ofNat n => inductionOn'.pos b zero succ n
        | -[n+1] => inductionOn'.neg b zero pred n))

Tactic:
rw! [show z - 1 - b = -[(b - z).toNat+1] by lia, show z - b = 0 by lia]
    grind [inductionOn'.pos]

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a b : α
h : a * b = 1
⊢ b = 1 / a

Tactic:
rw [eq_inv_of_mul_eq_one_right h, one_div]

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

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

Tactic:
by rw [← h, mul_inv_cancel_right]

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

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

Tactic:
by rw [← h, mul_inv_cancel_right]

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

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

Tactic:
by rw [← h, mul_inv_cancel_right]

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

Goal state before:
pp: case fst
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : DivInvMonoid G
inst✝ : DivInvMonoid H
x✝ : G × H
⊢ (x✝ ^ 0).1 = 1.1

Tactic:
exact DivInvMonoid.zpow_zero' _

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

Goal state before:
pp: case snd
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : DivInvMonoid G
inst✝ : DivInvMonoid H
x✝ : G × H
⊢ (x✝ ^ 0).2 = 1.2

Tactic:
exact DivInvMonoid.zpow_zero' _

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

Goal state before:
pp: α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
⊢ Function.Injective ⇑ofSubtype

Tactic:
by
  intro x y h
  rw [Perm.ext_iff] at h ⊢
  intro a
  specialize h a
  rwa [ofSubtype_apply_coe, ofSubtype_apply_coe, SetCoe.ext_iff] at h

Goal state after:
Module: Mathlib.Algebra.Module.NatInt

Goal state before:
pp: R✝ : Type u_1
S : Type u_2
M✝ : Type u_3
M₂ : Type u_4
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℤ
x : R
y : M
⊢ (n • x) • y = n • x • y

Tactic:
by
    cases n with
    | ofNat => simp [mul_smul, Nat.cast_smul_eq_nsmul]
    | negSucc => simp [mul_smul, add_smul, Nat.cast_smul_eq_nsmul]

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

Goal state before:
pp: case inr
M : Type u_1
N : Type u_2
μ : M → N → N
inst✝ : PartialOrder N
h : Covariant M N μ fun x1 x2 ↦ x1 < x2
a : M
b c : N
bc✝ : b ≤ c
bc : b < c
⊢ μ a b ≤ μ a c

Tactic:
exact (h _ bc).le

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

Goal state before:
pp: case refine_3
M : Type u_1
N : Type u_2
μ : M → N → N
inst✝ : PartialOrder N
h : (Contravariant M N μ fun x1 x2 ↦ x1 < x2) ∧ Contravariant M N μ fun x1 x2 ↦ x1 = x2
a : M
b c : N
bc : (fun x1 x2 ↦ x1 ≤ x2) (μ a b) (μ a c)
⊢ (fun x1 x2 ↦ x1 ≤ x2) b c

Tactic:
exact bc.lt_or_eq.elim (fun bc ↦ (h.1 a bc).le) (fun bc ↦ (h.2 a bc).le)

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

Goal state before:
pp: M : Type u_1
N : Type u_2
μ : M → N → N
inst✝ : PartialOrder N
⊢ (Contravariant M N μ fun x1 x2 ↦ x1 ≤ x2) ↔
    (Contravariant M N μ fun x1 x2 ↦ x1 < x2) ∧ Contravariant M N μ fun x1 x2 ↦ x1 = x2

Tactic:
refine ⟨fun h ↦ ⟨fun a b c bc ↦ ?_, fun a b c bc ↦ ?_⟩, fun h ↦ fun a b c bc ↦ ?_⟩
  · exact (h a bc.le).lt_of_ne (by rintro rfl; exact lt_irrefl _ bc)
  · exact (h a bc.le).antisymm (h a bc.ge)
  · exact bc.lt_or_eq.elim (fun bc ↦ (h.1 a bc).le) (fun bc ↦ (h.2 a bc).le)

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

Goal state before:
pp: α : Type u_4
f : α → α
hf : Involutive f
n : ℕ
⊢ id^[n] = id

Tactic:
iterate_id

Goal state after:
α : Type u_4
f : α → α
hf : Involutive f
n : ℕ
⊢ id = id
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: R : Type u_4
inst✝ : AddMonoidWithOne R
n : ℕ
h : 2 = 0
⊢ (Even n → ↑n = 0) ∧ (Odd n → ↑n = 1)

Tactic:
induction n using Nat.twoStepInduction with

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝⁵ : MulZeroClass α
a b c d : α
inst✝⁴ : PartialOrder α
inst✝³ : PosMulReflectLE α
inst✝² : MulPosReflectLE α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
ha : 0 < a
hc : 0 < c
hab : a ≤ b
hcd : c ≤ d
h : b * d ≤ a * c
⊢ d ≤ c

Tactic:
grw [hab] at h

Goal state after:
case refine_2
α : Type u_1
inst✝⁵ : MulZeroClass α
a b c d : α
inst✝⁴ : PartialOrder α
inst✝³ : PosMulReflectLE α
inst✝² : MulPosReflectLE α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
ha : 0 < a
hc : 0 < c
hab : a ≤ b
hcd : c ≤ d
h : b * d ≤ b * c
⊢ d ≤ c

case ha
α : Type u_1
inst✝⁵ : MulZeroClass α
a b c d : α
inst✝⁴ : PartialOrder α
inst✝³ : PosMulReflectLE α
inst✝² : MulPosReflectLE α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
ha : 0 < a
hc : 0 < c
hab : a ≤ b
hcd : c ≤ d
h : b * d ≤ a * c
⊢ 0 ≤ c
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:
by
  simp only [← not_le, pow_le_one_iff_of_nonneg ha hn]

Goal state after:
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a : α
⊢ a - ⊤ = ⊤

Tactic:
by simp [sub_eq_add_neg]

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

Goal state before:
pp: α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hc : AddLECancellable c
h : c ≤ b
⊢ a < b - c ↔ a + c < b

Tactic:
exact hc.lt_tsub_iff_right_of_le h

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
⊢ ¬a - b = 0 ↔ ¬a ≤ b

Tactic:
tsub_eq_zero_iff_le

Goal state after:
α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
⊢ ¬a ≤ b ↔ ¬a ≤ b
Module: Mathlib.Algebra.Order.Sub.Basic

Goal state before:
pp: case inl
α : Type u_1
inst✝⁵ : AddCommMonoid α
inst✝⁴ : LinearOrder α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : AddLeftReflectLE α
a b : α
h : a ≤ b
⊢ a + a - (b + b) = a - b + (a - b)

Tactic:
rw [tsub_eq_zero_of_le h, tsub_eq_zero_of_le (add_le_add h h), add_zero]

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
H : DenselyOrdered α
x y : αˣ
h : x < y
z : α
hz : ↑x < z ∧ z < ↑y
⊢ x < Units.mk0 z ⋯ ∧ Units.mk0 z ⋯ < y

Tactic:
by simp [← Units.val_lt_val, hz]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
x y : WithZero α
a b : α
inst✝¹ : Mul α
inst✝ : MulLeftMono α
⊢ MulLeftMono (WithZero α)

Tactic:
refine ⟨fun a b c hbc => ?_⟩
  induction a; · exact zero_le
  induction b; · exact zero_le
  rcases WithZero.coe_le_iff.1 hbc with ⟨c, rfl, hbc'⟩
  rw [← coe_mul _ c, ← coe_mul, coe_le_coe]
  exact mul_le_mul_right hbc' _

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

Goal state before:
pp: case pos
P Q : ℕ → Prop
inst✝¹ : DecidablePred P
inst✝ : DecidablePred Q
hPQ : ∀ (n : ℕ), P n → Q n
n : ℕ
hn : findGreatest P n ≤ findGreatest Q n
h : P (n + 1)
⊢ n + 1 ≤ findGreatest Q (n + 1)

Tactic:
findGreatest_eq (hPQ _ h)

Goal state after:
case pos
P Q : ℕ → Prop
inst✝¹ : DecidablePred P
inst✝ : DecidablePred Q
hPQ : ∀ (n : ℕ), P n → Q n
n : ℕ
hn : findGreatest P n ≤ findGreatest Q n
h : P (n + 1)
⊢ n + 1 ≤ n + 1
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: case inr.inl
R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : FloorSemiring R
inst✝³ : IsStrictOrderedRing R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : ExistsAddOfLE R
a : R
n : ℕ
ha : 0 ≤ a
h : a ≤ ↑n
⊢ ⌊a⌋₊ - n = 0

Tactic:
tsub_eq_zero_iff_le

Goal state after:
case inr.inl
R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : FloorSemiring R
inst✝³ : IsStrictOrderedRing R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : ExistsAddOfLE R
a : R
n : ℕ
ha : 0 ≤ a
h : a ≤ ↑n
⊢ ⌊a⌋₊ ≤ n
Module: Mathlib.Algebra.Order.Ring.Basic

Goal state before:
pp: R : Type u_3
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
x y : R
hx : 0 ≤ x
hy : 0 ≤ y
k : ℕ
ih : k + 1 ≠ 0 → x ^ (k + 1) + y ^ (k + 1) ≤ (x + y) ^ (k + 1)
hn : k + 1 + 1 ≠ 0
n : ℕ := k.succ
h1 : 0 ≤ x * y ^ n + y * x ^ n
h2 : 0 ≤ x + y
⊢ x * x ^ n + y * y ^ n + (x * y ^ n + y * x ^ n) = (x + y) * (x ^ n + y ^ n)

Tactic:
by
        rw [add_mul, mul_add, mul_add, add_comm (y * x ^ n), ← add_assoc, ← add_assoc,
          add_assoc (x * x ^ n) (x * y ^ n), add_comm (x * y ^ n) (y * y ^ n), ← add_assoc]

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

Goal state before:
pp: K : Type u_1
inst✝ : DivisionSemiring K
a b : K
h : b ≠ 0
⊢ (b + a) / b = 1 + a / b

Tactic:
rw [← div_self h, add_div]

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

Goal state before:
pp: K : Type u_1
inst✝ : DivisionSemiring K
a b : K
h : b ≠ 0
⊢ (a + b) / b = a / b + 1

Tactic:
rw [← div_self h, add_div]

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

Goal state before:
pp: R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a : R
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Odd n
⊢ a ^ n < 0 ↔ a < 0

Tactic:
refine ⟨lt_imp_lt_of_le_imp_le (pow_nonneg · _), fun ha ↦ ?_⟩

Goal state after:
R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a : R
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Odd n
ha : a < 0
⊢ a ^ n < 0
Module: Mathlib.Data.Set.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s s' : Set α
t t' : Set β
⊢ image2 f (s ∪ s') (t ∩ t') ⊆ image2 f s t ∪ image2 f s' t'

Tactic:
image2_union_left

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s s' : Set α
t t' : Set β
⊢ image2 f s (t ∩ t') ∪ image2 f s' (t ∩ t') ⊆ image2 f s t ∪ image2 f s' t'