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

Goal state before:
pp: M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
k : ℕ
k0 : k ≠ 0
m : M
⊢ m * npowRec' k m = npowRec' k m * m

Tactic:
by
  induction k using Nat.strongRecOn with
  | ind k' ih =>
    match k' with
    | 1 => simp [npowRec']
    | k + 2 => simp [npowRec', ← mul_assoc, ih]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a✝ b✝ a b : G
⊢ (a * b)⁻¹ = b⁻¹ * a⁻¹

Tactic:
apply inv_eq_of_mul
    rw [mul_assoc, mul_inv_cancel_left, mul_inv_cancel]

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

Goal state before:
pp: α : Sort u
β : α → Sort v
f : (a : α) → β a
β' : α → Sort v
f' : (a : α) → β' a
h : ∀ (a a' : α), a ≍ a' → f a ≍ f' a'
this : ∀ (a : α), f a ≍ f' a
a : α
⊢ β a = β' a

Tactic:
exact type_eq_of_heq (this a)

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

Goal state before:
pp: α : Type u
f : α → Type (max u v)
hf : Surjective f
T : Type (max u v) := Sigma f
U : α
hU : f U = Set T
g : Set T → T := fun s ↦ ⟨U, cast ⋯ s⟩
s t : Set T
h : g s = g t
this : s = t
⊢ s = t

Tactic:
assumption

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

Goal state before:
pp: ι : Sort u_1
α : ι → Sort u_2
β : ι → Sort u_3
inst✝ : ∀ (i : ι), Nonempty (α i)
f : (i : ι) → α i → β i
h : Injective (Pi.map f)
i : ι
x y : α i
hxy : f i x = f i y
⊢ x = y

Tactic:
by
    classical
    have : Inhabited (∀ i, α i) := ⟨fun _ => Classical.choice inferInstance⟩
    replace h := @h (Function.update default i x) (Function.update default i y) ?_
    · simpa using congrFun h i
    rw [Pi.map_update, Pi.map_update, hxy]

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case refl
α : Type u_1
r : α → α → Prop
a b c : α
hab : ReflTransGen r a b
⊢ ReflTransGen r a b

Tactic:
assumption

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
motive : {a b : α} → ReflTransGen r a b → Prop
a b : α
h : ReflTransGen r a b
refl : ∀ (a : α), motive ⋯
single : ∀ {a b : α} (h : r a b), motive ⋯
trans : ∀ {a b c : α} (h₁ : ReflTransGen r a b) (h₂ : ReflTransGen r b c), motive h₁ → motive h₂ → motive ⋯
⊢ motive h

Tactic:
induction h with
  | refl => exact refl a
  | tail hab hbc ih => exact trans hab (.single hbc) ih (single hbc)

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case refl
α : Type u_1
r : α → α → Prop
a b c : α
hab : TransGen r a b
⊢ TransGen r a b

Tactic:
assumption

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
⊢ ReflGen (TransGen r) = ReflTransGen r

Tactic:
by
  ext x y
  simp_rw [reflTransGen_iff_eq_or_transGen, reflGen_iff]

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case refine_2
α : Type u_1
r : α → α → Prop
x y : α
h : ReflTransGen r x y
⊢ TransGen (ReflGen r) x y

Tactic:
obtain (rfl | h) := reflTransGen_iff_eq_or_transGen.mp h

Goal state after:
case refine_2.inl
α : Type u_1
r : α → α → Prop
y : α
h : ReflTransGen r y y
⊢ TransGen (ReflGen r) y y

case refine_2.inr
α : Type u_1
r : α → α → Prop
x y : α
h✝ : ReflTransGen r x y
h : TransGen r x y
⊢ TransGen (ReflGen r) x y
Module: Mathlib.Logic.Relation

Goal state before:
pp: case rel
α : Type u_1
r : α → α → Prop
a b : α
h : Equivalence r
x✝ y✝ : α
a✝ : r x✝ y✝
⊢ r x✝ y✝

Tactic:
assumption

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case symm
α : Type u_1
r : α → α → Prop
a b : α
h : Equivalence r
x✝ y✝ : α
a✝ : EqvGen r x✝ y✝
a_ih✝ : r x✝ y✝
⊢ r x✝ y✝

Tactic:
assumption

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f g : α → β
h : Option.map f = Option.map g
x : α
⊢ some (f x) = some (g x)

Tactic:
by simp only [← map_some, h]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h₁ : c ≤ a
h₂ : c ≤ b
h✝ : a ≤ b
⊢ c ≤ a

Tactic:
assumption

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h₁ : c ≤ a
h₂ : c ≤ b
h✝ : ¬a ≤ b
⊢ c ≤ b

Tactic:
assumption

Goal state after:
Module: Mathlib.Order.OrderDual

Goal state before:
pp: α : Type u_1
inst✝ : LT α
T : Std.Trichotomous LT.lt
a b : αᵒᵈ
⊢ ¬a < b → ¬b < a → a = b

Tactic:
rw [eq_comm]

Goal state after:
α : Type u_1
inst✝ : LT α
T : Std.Trichotomous LT.lt
a b : αᵒᵈ
⊢ ¬a < b → ¬b < a → b = a
Module: Mathlib.Data.Nat.Basic

Goal state before:
pp: case succ.inl
b : ℕ
ha : 0 ≠ 1
⊢ 0 * (b + 1) ≤ 0 ^ (b + 1)

Tactic:
rw [Nat.zero_mul]

Goal state after:
case succ.inl
b : ℕ
ha : 0 ≠ 1
⊢ 0 ≤ 0 ^ (b + 1)
Module: Mathlib.Data.Nat.Init

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

Tactic:
dsimp only [decreasingInduction]; rw [leRec_succ]

Goal state after:
Module: Mathlib.Order.Compare

Goal state before:
pp: case eq
α : Type u_1
inst✝ : LT α
a b : α
⊢ eq.swap.Compares a b ↔ eq.Compares b a

pp: case gt
α : Type u_1
inst✝ : LT α
a b : α
⊢ gt.swap.Compares a b ↔ gt.Compares b a

Tactic:
· exact eq_comm

Goal state after:
case gt
α : Type u_1
inst✝ : LT α
a b : α
⊢ gt.swap.Compares a b ↔ gt.Compares b a
Module: Mathlib.Order.Monotone.Defs

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
δ : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
f : α → γ
g : β → δ
hf : StrictMono f
hg : StrictMono g
a b : α × β
⊢ a < b → Prod.map f g a < Prod.map f g b

Tactic:
simp only [Prod.lt_iff]
  exact Or.imp (And.imp hf.imp hg.monotone.imp) (And.imp hf.monotone.imp hg.imp)

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
a b : α
ha : a ≠ ⊥
hab : Disjoint a b
h : a = b
⊢ Disjoint a a

Tactic:
rwa [← h] at hab

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
pr : α → Prop
Pinf : ∀ ⦃s t : α⦄, pr s → pr t → pr (s ⊓ t)
hbot : pr ⊥
a b : Subtype pr
this✝ : SemilatticeInf (Subtype pr) := Subtype.semilatticeInf Pinf
this : OrderBot (Subtype pr) := Subtype.orderBot hbot
⊢ Disjoint a b ↔ Disjoint ↑a ↑b

Tactic:
rw [disjoint_iff, disjoint_iff, ← Subtype.coe_inf Pinf, ← Subtype.coe_bot hbot]

Goal state after:
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
pr : α → Prop
Pinf : ∀ ⦃s t : α⦄, pr s → pr t → pr (s ⊓ t)
hbot : pr ⊥
a b : Subtype pr
this✝ : SemilatticeInf (Subtype pr) := Subtype.semilatticeInf Pinf
this : OrderBot (Subtype pr) := Subtype.orderBot hbot
⊢ a ⊓ b = ⊥ ↔ ↑(a ⊓ b) = ↑⊥
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : Subsingleton α
⊢ ComplementedLattice α

Tactic:
refine ⟨fun a ↦ ⟨⊥, disjoint_bot_right, ?_⟩⟩

Goal state after:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : Subsingleton α
a : α
⊢ Codisjoint a ⊥
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: case neg
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)
hg_anti : Antitone g
⊢ ∃ n_1, n_1 ≤ n ∧ ∀ (m : ℕ), n_1 ≤ m → f m = f n_1

Tactic:
obtain ⟨p, hp, hp'⟩ := ih (f 1) (by grind) hg_anti (by grind) rfl

Goal state after:
case neg
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)
hg_anti : Antitone g
p : ℕ
hp : p ≤ f 1
hp' : ∀ (m : ℕ), p ≤ m → g m = g p
⊢ ∃ n_1, n_1 ≤ n ∧ ∀ (m : ℕ), n_1 ≤ m → f m = f n_1
Module: Mathlib.Data.Set.Basic

Goal state before:
pp: α : Type u
s t : Set α
a b : α
p : α → Prop
inst✝ : Decidable (p a)
⊢ Decidable (a ∈ {a | p a})

Tactic:
assumption

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
inst✝ : Lattice α
a b : α
⊢ a ⊔ b ≤ a ⊓ b ↔ a = b

Tactic:
simp [le_antisymm_iff, and_comm]

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: case inl.refine_3
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst✝¹ : LinearOrder α
inst✝ : SemilatticeSup β
hf : MonotoneOn f s
hx : x ∈ s
hy : y ∈ s
h✝ : x ≤ y
this : f x ≤ f y
⊢ f (max x y) = f x ⊔ f y

Tactic:
assumption

Goal state after:
case inl.refine_3
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst✝¹ : LinearOrder α
inst✝ : SemilatticeSup β
hf : MonotoneOn f s
hx : x ∈ s
hy : y ∈ s
h✝ : x ≤ y
this : f x ≤ f y
⊢ f (max x y) = f x ⊔ f y
Module: Mathlib.Order.Lattice

Goal state before:
pp: case inl.refine_1
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst✝¹ : LinearOrder α
inst✝ : SemilatticeSup β
hf : MonotoneOn f s
hx : x ∈ s
hy : y ∈ s
h✝ : x ≤ y
⊢ x ∈ s

Tactic:
assumption

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: case inl.refine_2
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst✝¹ : LinearOrder α
inst✝ : SemilatticeSup β
hf : MonotoneOn f s
hx : x ∈ s
hy : y ∈ s
h✝ : x ≤ y
⊢ y ∈ s

Tactic:
assumption

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: case inr.refine_3
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst✝¹ : LinearOrder α
inst✝ : SemilatticeSup β
hf : MonotoneOn f s
hx : x ∈ s
hy : y ∈ s
h✝ : y ≤ x
this : f y ≤ f x
⊢ f (max x y) = f x ⊔ f y

Tactic:
assumption

Goal state after:
case inr.refine_3
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst✝¹ : LinearOrder α
inst✝ : SemilatticeSup β
hf : MonotoneOn f s
hx : x ∈ s
hy : y ∈ s
h✝ : y ≤ x
this : f y ≤ f x
⊢ f (max x y) = f x ⊔ f y
Module: Mathlib.Order.Lattice

Goal state before:
pp: case inr.refine_1
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst✝¹ : LinearOrder α
inst✝ : SemilatticeSup β
hf : MonotoneOn f s
hx : x ∈ s
hy : y ∈ s
h✝ : y ≤ x
⊢ y ∈ s

Tactic:
assumption

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: case inr.refine_2
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst✝¹ : LinearOrder α
inst✝ : SemilatticeSup β
hf : MonotoneOn f s
hx : x ∈ s
hy : y ∈ s
h✝ : y ≤ x
⊢ x ∈ s

Tactic:
assumption

Goal state after:
Module: Mathlib.Order.Lattice

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

Tactic:
assumption

Goal state after:
case inl.refine_3
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst✝¹ : LinearOrder α
inst✝ : SemilatticeInf β
hf : AntitoneOn f s
hx : x ∈ s
hy : y ∈ s
h✝ : x ≤ y
this : f y ≤ f x
⊢ f (max x y) = f x ⊓ f y
Module: Mathlib.Order.Lattice

Goal state before:
pp: case inl.refine_1
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst✝¹ : LinearOrder α
inst✝ : SemilatticeInf β
hf : AntitoneOn f s
hx : x ∈ s
hy : y ∈ s
h✝ : x ≤ y
⊢ x ∈ s

Tactic:
assumption

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: case inl.refine_2
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst✝¹ : LinearOrder α
inst✝ : SemilatticeInf β
hf : AntitoneOn f s
hx : x ∈ s
hy : y ∈ s
h✝ : x ≤ y
⊢ y ∈ s

Tactic:
assumption

Goal state after:
Module: Mathlib.Order.Lattice

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

Tactic:
assumption

Goal state after:
case inr.refine_3
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst✝¹ : LinearOrder α
inst✝ : SemilatticeInf β
hf : AntitoneOn f s
hx : x ∈ s
hy : y ∈ s
h✝ : y ≤ x
this : f x ≤ f y
⊢ f (max x y) = f x ⊓ f y
Module: Mathlib.Order.Lattice

Goal state before:
pp: case inr.refine_1
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst✝¹ : LinearOrder α
inst✝ : SemilatticeInf β
hf : AntitoneOn f s
hx : x ∈ s
hy : y ∈ s
h✝ : y ≤ x
⊢ y ∈ s

Tactic:
assumption

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: case inr.refine_2
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst✝¹ : LinearOrder α
inst✝ : SemilatticeInf β
hf : AntitoneOn f s
hx : x ∈ s
hy : y ∈ s
h✝ : y ≤ x
⊢ x ∈ s

Tactic:
assumption

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

Goal state before:
pp: α : Type u
a : α
s : Set α
ha : a ∈ s
⊢ s.Subsingleton ∨ s.Nontrivial

Tactic:
exact s.subsingleton_or_nontrivial

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

Goal state before:
pp: α : Type u
inst✝ : IsEmpty α
S : Set α
hS : S ∈ univ
⊢ S ∈ {∅}

Tactic:
simp [Set.eq_empty_of_isEmpty S]

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 }
⊢ (fun e ↦ { toFun := fun a ↦ ⟨↑e (some a), ⋯⟩, invFun := fun b ↦ ((↑e).symm ↑b).get ⋯, left_inv := ⋯, right_inv := ⋯ })
      ((fun e ↦
          ⟨{ toFun := fun a ↦ a.casesOn' x (Subtype.val ∘ ⇑e),
              invFun := fun b ↦ if h : b = x then none else some (e.symm ⟨b, h⟩), left_inv := ⋯, right_inv := ⋯ },
            ⋯⟩)
        e) =
    e

Tactic:
by
    ext a
    rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
x : β
e : { e // e none = x }
b : { y // y ≠ x }
⊢ some (((optionSubtype x) e).symm b) = (↑e).symm ↑b

Tactic:
dsimp only [optionSubtype]

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
x : β
e : { e // e none = x }
b : { y // y ≠ x }
⊢ some
      (({
              toFun := fun e ↦
                { toFun := fun a ↦ ⟨↑e (some a), ⋯⟩, invFun := fun b ↦ ((↑e).symm ↑b).get ⋯, left_inv := ⋯,
                  right_inv := ⋯ },
              invFun := fun e ↦
                ⟨{ toFun := fun a ↦ a.casesOn' x (Subtype.val ∘ ⇑e),
                    invFun := fun b ↦ if h : b = x then none else some (e.symm ⟨b, h⟩), left_inv := ⋯, right_inv := ⋯ },
                  ⋯⟩,
              left_inv := ⋯, right_inv := ⋯ }
            e).symm
        b) =
    (↑e).symm ↑b
Module: Mathlib.Data.Sigma.Basic

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

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

Goal state after:
α₁ : Type u_2
α₂ : Type u_3
β₁ : α₁ → Type u_5
β₂ : α₂ → Type u_6
f₁ : α₁ → α₂
f₂ : (a : α₁) → β₁ a → β₂ (f₁ a)
h₁ : Injective f₁
h₂ : ∀ (a : α₁), Injective (f₂ a)
i : α₁
x y : β₁ i
h : Sigma.map f₁ f₂ ⟨i, x⟩ = Sigma.map f₁ f₂ ⟨i, y⟩
⊢ ⟨i, x⟩ = ⟨i, y⟩
Module: Mathlib.Order.BooleanAlgebra.Basic

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

Tactic:
refine le_of_inf_le_sup_le ?_ H.le

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : x ⊔ y \ x = z ⊔ y \ x
⊢ x ⊓ y \ x ≤ z ⊓ y \ x
Module: Mathlib.Order.BooleanAlgebra.Basic

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

Tactic:
rw [sup_comm, inf_comm, ← inf_assoc, sup_inf_inf_sdiff]

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x \ (y \ z) = z ⊓ x ⊔ x \ y
Module: Mathlib.Order.BooleanAlgebra.Basic

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

Tactic:
rw [sdiff_sdiff_right, inf_idem, sdiff_self, bot_sup_eq]

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
by
  rw [symmDiff_eq_sup_sdiff_inf, sdiff_eq, compl_inf]

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

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

Tactic:
refine ⟨?_, fun h => ⟨i, h, hi⟩⟩
    rintro ⟨j, hj, h⟩
    rwa [σ.injective (hi.trans h.symm)]

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : ¬(s = ∅ ∨ t = ∅)
⊢ s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅) ↔ s = s₁ ∧ t = t₁

Tactic:
simp_rw [h, false_and, or_false]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
inst✝ : Nonempty α
h : s ⊆ invFunOn f s '' f '' s
x : α
hx' : x ∈ s
hx : invFunOn f s (f x) ∈ s
⊢ invFunOn f s (f (invFunOn f s (f x))) = invFunOn f s (f x)

Tactic:
invFunOn_apply_eq (f := f) hx'

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
inst✝ : Nonempty α
h : s ⊆ invFunOn f s '' f '' s
x : α
hx' : x ∈ s
hx : invFunOn f s (f x) ∈ s
⊢ invFunOn f s (f x) = invFunOn f s (f x)
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Nonempty α
f : α → β
s : Set α
x : α
hx : x ∈ s
x' : α
hx' : x' ∈ s
he : invFunOn f s (f x) = invFunOn f s (f x')
⊢ f (invFunOn f s (f x')) = f x'

Tactic:
invFunOn_apply_eq (f := f) hx'

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : Nonempty α
f : α → β
s : Set α
x : α
hx : x ∈ s
x' : α
hx' : x' ∈ s
he : invFunOn f s (f x) = invFunOn f s (f x')
⊢ f x' = f x'
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Nonempty α
f : α → β
s : Set α
⊢ InjOn (invFunOn f s) (f '' s)

Tactic:
rintro _ ⟨x, hx, rfl⟩ _ ⟨x', hx', rfl⟩ he
  rw [← invFunOn_apply_eq (f := f) hx, he, invFunOn_apply_eq (f := f) hx']

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
a : M
n : ℕ
⊢ (fun x ↦ x * a)^[n + 1] = fun x ↦ x * a ^ (n + 1)

Tactic:
by simp [pow_succ', mul_right_iterate]

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

Goal state before:
pp: case succ
G : Type u_3
inst✝ : Group G
g : G
P : G → Prop
h_one : P 1
h_mul : ∀ (a : G), P a → P (a * g)
h_inv : ∀ (a : G), P a → P (a * g⁻¹)
n : ℕ
ih : P (g ^ ↑n)
⊢ P (g ^ (↑n + 1))

Tactic:
rw [zpow_add_one]
    exact h_mul _ ih

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

Goal state before:
pp: α : Type u
inst✝ : DivisionCommMonoid α
a : α
h : IsUnit a
b : α
⊢ a / (a * b) = 1 / b

Tactic:
rw [mul_comm, h.div_mul_left]

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✝¹ : ℕ
x✝ : G × H
⊢ (x✝ ^ Int.negSucc x✝¹).1 = (x✝ ^ ↑x✝¹.succ)⁻¹.1

Tactic:
exact DivInvMonoid.zpow_neg' ..

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✝¹ : ℕ
x✝ : G × H
⊢ (x✝ ^ Int.negSucc x✝¹).2 = (x✝ ^ ↑x✝¹.succ)⁻¹.2

Tactic:
exact DivInvMonoid.zpow_neg' ..

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

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
⊢ a⁻¹ = 0 ↔ a = 0

Tactic:
rw [inv_eq_iff_eq_inv, inv_zero]

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

Goal state before:
pp: R : Type u_5
inst✝¹ : Semiring R
M : Type u_6
inst✝ : AddCommMonoid M
P Q : Module R M
w : ∀ (r : R) (m : M), r • m = r • m
⊢ P = Q

Tactic:
by
  ext
  exact w _ _

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
f : Multiplicative ℕ →* M
n : Multiplicative ℕ
⊢ f n = f (ofAdd 1) ^ toAdd n

Tactic:
by
  rw [← powersHom_symm_apply, ← powersHom_apply, Equiv.apply_symm_apply]

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

Goal state before:
pp: A : Type u_3
F : Type u_5
inst✝² : FunLike F ℕ A
inst✝¹ : AddMonoidWithOne A
inst✝ : AddMonoidHomClass F ℕ A
f : F
h1 : f 1 = 1
n : ℕ
⊢ f (n + 1) = ↑(n + 1)

Tactic:
by rw [map_add, h1, eq_natCast' f h1 n, Nat.cast_add_one]

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

Goal state before:
pp: α : 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
⊢ b ^ (2 * k + 3) = b ^ (2 * k + 1) * b ^ 2

Tactic:
← pow_add

Goal state after:
α : 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
⊢ b ^ (2 * k + 3) = b ^ (2 * k + 1 + 2)
Module: Mathlib.Algebra.Order.Sub.Defs

Goal state before:
pp: case bc
α : Type u_1
inst✝⁵ : PartialOrder α
inst✝⁴ : AddCommSemigroup α
inst✝³ : Sub α
inst✝² : OrderedSub α
inst✝¹ : AddLeftMono α
inst✝ : AddLeftReflectLE α
a c b : α
⊢ a + ?bc.c ≤ a + c - (b + c) + (b + ?bc.c)

pp: case bc.c
α : Type u_1
inst✝⁵ : PartialOrder α
inst✝⁴ : AddCommSemigroup α
inst✝³ : Sub α
inst✝² : OrderedSub α
inst✝¹ : AddLeftMono α
inst✝ : AddLeftReflectLE α
a c b : α
⊢ α

Tactic:
exact le_tsub_add

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

Goal state before:
pp: case pos
α : Type u_1
inst✝² : MulOneClass α
inst✝¹ : LinearOrder α
inst✝ : MulLeftStrictMono α
a : α
h : a < 1
⊢ ∃ b, b * b ≤ a

Tactic:
use a
    have : a * a < a * 1 := mul_lt_mul_right h a
    rw [mul_one] at this
    exact le_of_lt this

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

Goal state before:
pp: case ha
R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : Preorder R
a b c d : R
inst✝⁴ : ExistsAddOfLE R
inst✝³ : MulPosMono R
inst✝² : PosMulMono R
inst✝¹ : AddRightMono R
inst✝ : AddRightReflectLE R
hca : c ≤ a
hbd : b ≤ d
hc : 0 ≤ c
hb : b ≤ 0
⊢ 0 ≤ c

Tactic:
assumption

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

Goal state before:
pp: M₀ : Type u_2
inst✝² : MonoidWithZero M₀
inst✝¹ : PartialOrder M₀
a : M₀
n : ℕ
inst✝ : PosMulStrictMono M₀
h₀ : 0 < a
h₁ : a < 1
hn : 1 < n
⊢ a ^ n < a

Tactic:
simpa only [pow_one] using pow_lt_pow_right_of_lt_one₀ h₀ h₁ hn

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

Goal state before:
pp: case ha
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : PartialOrder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : MulPosMono R
inst✝¹ : AddLeftMono R
inst✝ : AddLeftReflectLE R
hab : a ≤ b
d : R
hd : 0 ≤ d
hcd : c ≤ c + d
⊢ 0 ≤ d

Tactic:
assumption

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₀
inst✝ : MulPosReflectLT G₀
a b : G₀
ha : 0 < a
hb : 0 < b
⊢ a ≤ b⁻¹ ↔ b ≤ a⁻¹

Tactic:
rw [← inv_le_inv₀ (inv_pos.2 hb) ha, inv_inv]

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

Goal state before:
pp: case hb
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosReflectLT G₀
a b c d : G₀
hac : a < c
hdb : d ≤ b
hc : 0 ≤ c
hd : 0 < d
⊢ 0 < d

Tactic:
assumption

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

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : LinearOrder G₀
a : G₀
inst✝ : PosMulMono G₀
⊢ a⁻¹ < 0 ↔ a < 0

Tactic:
have := PosMulMono.toPosMulReflectLT (α := G₀)

Goal state after:
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : LinearOrder G₀
a : G₀
inst✝ : PosMulMono G₀
this : PosMulReflectLT G₀
⊢ a⁻¹ < 0 ↔ a < 0