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

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

Tactic:
by
  rw [← pow_add, ← pow_add, Nat.add_comm]

Goal state after:
Module: Mathlib.Logic.Unique

Goal state before:
pp: α : Sort u
x✝ : Nonempty (Unique α)
u : Unique α
⊢ Subsingleton α ∧ Nonempty α

Tactic:
by constructor <;> exact inferInstance

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case tail.refl
α : 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✝ f b : α
a✝ : ReflTransGen r d f
hfb : r f b
hea : ReflTransGen r e f
⊢ ∃ a, ReflTransGen r e a ∧ ReflGen r b a

Tactic:
exact ⟨b, hea.tail hfb, ReflGen.refl⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
ga : α → α → α
gb : β → β → β
inst✝ : Std.IdempotentOp ga
h : Semiconj₂ f ga gb
h_surj : Surjective f
x : α
⊢ gb (f x) (f x) = f x

Tactic:
by simp only [← h.eq, Std.IdempotentOp.idempotent (op := ga)]

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

Goal state before:
pp: M✝ : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
inst✝⁴ : Monoid M✝
inst✝³ : MulAction M✝ α
a : M✝
R : Type u_9
M : Type u_10
inst✝² : CommMonoid M
inst✝¹ : SMul R M
inst✝ : IsScalarTower R M M
r : R
s x : M
⊢ r • s • x = s • r • x

Tactic:
rw [← one_smul M (s • x), ← smul_assoc, smul_comm, smul_assoc, one_smul]

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

Goal state before:
pp: case step
m n k : ℕ
hmn : m ≤ n
m✝ : ℕ
hnk : n.le m✝
ih :
  ∀ {motive : (m : ℕ) → m ≤ m✝ → Sort u_1} (of_succ : (k : ℕ) → (h : k < m✝) → motive (k + 1) h → motive k ⋯)
    (self : motive m✝ ⋯),
    decreasingInduction of_succ self ⋯ =
      decreasingInduction (fun x x_1 ↦ of_succ x ⋯) (decreasingInduction of_succ self hnk) hmn
motive : (m : ℕ) → m ≤ m✝.succ → Sort u_1
of_succ : (k : ℕ) → (h : k < m✝.succ) → motive (k + 1) h → motive k ⋯
self : motive m✝.succ ⋯
⊢ decreasingInduction (fun x x_1 ↦ of_succ x ⋯) (decreasingInduction (fun x x_1 ↦ of_succ x ⋯) (of_succ m✝ ⋯ self) hnk)
      hmn =
    decreasingInduction (fun x x_1 ↦ of_succ x ⋯) (decreasingInduction of_succ self ⋯) hmn

Tactic:
decreasingInduction_succ

Goal state after:
case step
m n k : ℕ
hmn : m ≤ n
m✝ : ℕ
hnk : n.le m✝
ih :
  ∀ {motive : (m : ℕ) → m ≤ m✝ → Sort u_1} (of_succ : (k : ℕ) → (h : k < m✝) → motive (k + 1) h → motive k ⋯)
    (self : motive m✝ ⋯),
    decreasingInduction of_succ self ⋯ =
      decreasingInduction (fun x x_1 ↦ of_succ x ⋯) (decreasingInduction of_succ self hnk) hmn
motive : (m : ℕ) → m ≤ m✝.succ → Sort u_1
of_succ : (k : ℕ) → (h : k < m✝.succ) → motive (k + 1) h → motive k ⋯
self : motive m✝.succ ⋯
⊢ decreasingInduction (fun x x_1 ↦ of_succ x ⋯) (decreasingInduction (fun x x_1 ↦ of_succ x ⋯) (of_succ m✝ ⋯ self) hnk)
      hmn =
    decreasingInduction (fun x x_1 ↦ of_succ x ⋯)
      (decreasingInduction (fun x x_1 ↦ of_succ x ⋯) (of_succ m✝ ⋯ self) ?step.mn) hmn

case step.mn
m n k : ℕ
hmn : m ≤ n
m✝ : ℕ
hnk : n.le m✝
ih :
  ∀ {motive : (m : ℕ) → m ≤ m✝ → Sort u_1} (of_succ : (k : ℕ) → (h : k < m✝) → motive (k + 1) h → motive k ⋯)
    (self : motive m✝ ⋯),
    decreasingInduction of_succ self ⋯ =
      decreasingInduction (fun x x_1 ↦ of_succ x ⋯) (decreasingInduction of_succ self hnk) hmn
motive : (m : ℕ) → m ≤ m✝.succ → Sort u_1
of_succ : (k : ℕ) → (h : k < m✝.succ) → motive (k + 1) h → motive k ⋯
self : motive m✝.succ ⋯
⊢ n ≤ m✝
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝² : Preorder α
inst✝¹ : Preorder β
f g : α → β
hf : StrictMono f
hg : StrictMono g
p : α → Prop
inst✝ : DecidablePred p
hp : ∀ ⦃x y : α⦄, x < y → p y → p x
hfg : ∀ ⦃x y : α⦄, p x → ¬p y → x < y → f x < g y
⊢ StrictMono fun x ↦ if p x then f x else g x

Tactic:
intro x y h

Goal state after:
α : Type u
β : Type v
inst✝² : Preorder α
inst✝¹ : Preorder β
f g : α → β
hf : StrictMono f
hg : StrictMono g
p : α → Prop
inst✝ : DecidablePred p
hp : ∀ ⦃x y : α⦄, x < y → p y → p x
hfg : ∀ ⦃x y : α⦄, p x → ¬p y → x < y → f x < g y
x y : α
h : x < y
⊢ (fun x ↦ if p x then f x else g x) x < (fun x ↦ if p x then f x else g x) y
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
x y x' y' : α
h : IsCompl x y
h' : IsCompl x' y'
⊢ (x ⊔ x') ⊓ (y ⊓ y') = ⊥

Tactic:
by rw [inf_sup_right, ← inf_assoc, h.inf_eq_bot, bot_inf_eq, bot_sup_eq, inf_left_comm,
      h'.inf_eq_bot, inf_bot_eq]

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
x y x' y' : α
h : IsCompl x y
h' : IsCompl x' y'
⊢ x ⊔ x' ⊔ y ⊓ y' = ⊤

Tactic:
sup_inf_left,

Goal state after:
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
x y x' y' : α
h : IsCompl x y
h' : IsCompl x' y'
⊢ (x ⊔ x' ⊔ y) ⊓ (x ⊔ x' ⊔ y') = ⊤
Module: Mathlib.Data.Set.Basic

Goal state before:
pp: α : Type u_1
s t : Set α
⊢ ¬s ⊆ t ↔ ∃ x, x ∈ s ∧ ¬x ∈ t

Tactic:
simp [subset_def]

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

Goal state before:
pp: α : Type u
p : Prop
inst✝ : Decidable p
t : p → Set α
x : α
⊢ (x ∈ if h : p then t h else univ) ↔ ∀ (h : p), x ∈ t h

Tactic:
by
  simp [mem_dite]

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: case mk.mk.refl
α : Type u_1
toSemilatticeSup✝ : SemilatticeSup α
inf✝¹ : α → α → α
inf_le_left✝¹ : ∀ (a b : α), inf✝¹ a b ≤ a
inf_le_right✝¹ : ∀ (a b : α), inf✝¹ a b ≤ b
le_inf✝¹ : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ inf✝¹ b c
inf✝ : α → α → α
inf_le_left✝ : ∀ (a b : α), inf✝ a b ≤ a
inf_le_right✝ : ∀ (a b : α), inf✝ a b ≤ b
le_inf✝ : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ inf✝ b c
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ { toSemilatticeSup := toSemilatticeSup✝, inf := inf✝¹, inf_le_left := inf_le_left✝¹, inf_le_right := inf_le_right✝¹,
      le_inf := le_inf✝¹ } =
    {
      toSemilatticeSup :=
        { toSemilatticeSup := toSemilatticeSup✝, inf := inf✝¹, inf_le_left := inf_le_left✝¹,
            inf_le_right := inf_le_right✝¹, le_inf := le_inf✝¹ }.toSemilatticeSup,
      inf := inf✝, inf_le_left := inf_le_left✝, inf_le_right := inf_le_right✝, le_inf := le_inf✝ }

Tactic:
cases SemilatticeInf.ext H

Goal state after:
case mk.mk.refl.refl
α : Type u_1
toSemilatticeSup✝ : SemilatticeSup α
inf✝ : α → α → α
inf_le_left✝¹ : ∀ (a b : α), inf✝ a b ≤ a
inf_le_right✝¹ : ∀ (a b : α), inf✝ a b ≤ b
le_inf✝¹ : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ inf✝ b c
inf_le_left✝ : ∀ (a b : α), inf✝ a b ≤ a
inf_le_right✝ : ∀ (a b : α), inf✝ a b ≤ b
le_inf✝ : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ inf✝ b c
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ { toSemilatticeSup := toSemilatticeSup✝, inf := inf✝, inf_le_left := inf_le_left✝¹, inf_le_right := inf_le_right✝¹,
      le_inf := le_inf✝¹ } =
    {
      toSemilatticeSup :=
        { toSemilatticeSup := toSemilatticeSup✝, inf := inf✝, inf_le_left := inf_le_left✝¹,
            inf_le_right := inf_le_right✝¹, le_inf := le_inf✝¹ }.toSemilatticeSup,
      inf := inf✝, inf_le_left := inf_le_left✝, inf_le_right := inf_le_right✝, le_inf := le_inf✝ }
Module: Mathlib.Data.Set.Subsingleton

Goal state before:
pp: α : Type u
⊢ univ = {∅} ↔ IsEmpty α

Tactic:
by
  refine ⟨fun h ↦ ?_, fun _ ↦ by simp⟩
  suffices @univ α ∈ univ by aesop
  simp

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

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ (a ⊔ b) \ b = a \ b

Tactic:
by rw [sup_sdiff, sdiff_self, sup_bot_eq]

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 }
a : Option α
⊢ (fun b ↦ if h : b = x then none else some (e.symm ⟨b, h⟩)) ((fun a ↦ a.casesOn' x (Subtype.val ∘ ⇑e)) a) = a

Tactic:
by
          cases a with
          | none => simp
          | some a =>
            simp only [casesOn'_some, Function.comp_apply, Subtype.coe_eta,
              symm_apply_apply, dite_eq_ite]
            exact if_neg (e a).property

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

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

Tactic:
sup_inf_left,

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (y ⊓ (x ⊔ z) ⊔ y \ x) ⊓ (y ⊓ (x ⊔ z) ⊔ y \ z) = (y ⊓ x ⊔ y ⊓ z ⊔ y \ x) ⊓ (y ⊓ x ⊔ y ⊓ z ⊔ y \ z)
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:
by rw [inf_inf_sdiff, h, inf_inf_sdiff]

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

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

Tactic:
sup_inf_left,

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

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hx : x ≤ z
hy : y ≤ z
h : z \ x ≤ z \ y
⊢ y ≤ z \ (z \ x)

Tactic:
← sdiff_sdiff_eq_self hy

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hx : x ≤ z
hy : y ≤ z
h : z \ x ≤ z \ y
⊢ z \ (z \ y) ≤ z \ (z \ x)
Module: Mathlib.Order.BooleanAlgebra.Basic

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

Tactic:
sup_inf_left,

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

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

Tactic:
sup_inf_left,

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

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

Tactic:
sup_inf_left,

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

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ a ⊔ b ≤ a ∆ b ⊔ a ⊓ b

Tactic:
sup_inf_left,

Goal state after:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ a ⊔ b ≤ (a ∆ b ⊔ a) ⊓ (a ∆ b ⊔ b)
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b : α
⊢ a ∆ b \ b = a \ b

Tactic:
by rw [symmDiff_comm, symmDiff_sdiff_left]

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

Goal state before:
pp: case mpr
α : Type u_9
inst✝ : DecidableEq α
s : Set α
i j : α
hi : i ∈ s
hj : ¬j ∈ s
a : α
⊢ a ∈ insert j s \ {i} → a ∈ Set.image (⇑(swap i j)) s

Tactic:
rintro ⟨rfl | has, hai⟩

Goal state after:
case mpr.inl
α : Type u_9
inst✝ : DecidableEq α
s : Set α
i : α
hi : i ∈ s
a : α
hai : ¬a ∈ {i}
hj : ¬a ∈ s
⊢ a ∈ Set.image (⇑(swap i a)) s

case mpr.inr
α : Type u_9
inst✝ : DecidableEq α
s : Set α
i j : α
hi : i ∈ s
hj : ¬j ∈ s
a : α
hai : ¬a ∈ {i}
has : a ∈ s
⊢ a ∈ Set.image (⇑(swap i j)) s
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
⊢ Surjective (Membership.mem ∘ preimage f ∘ ofPred) ↔ Injective f

Tactic:
exact surjective_comp_right_iff_injective

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
hf : Injective f
g : α → γ
g' : β → γ
x : α
⊢ g x ∈ range (extend f g g')

pp: case inr
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
hf : Injective f
g : α → γ
g' : β → γ
y : β
hy : y ∈ (range f)ᶜ
⊢ g' y ∈ range (extend f g g')

Tactic:
exacts [⟨f x, hf.extend_apply _ _ _⟩, ⟨y, extend_apply' _ _ _ hy⟩]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
W : Set γ
f : α × β → γ
⊢ s ×ˢ t ⊆ f ⁻¹' W ↔ ∀ (a : α) (b : β), a ∈ s → b ∈ t → f (a, b) ∈ W

Tactic:
simp [subset_def]

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 = (fun a ↦ f ↑a) ⁻¹' Subtype.val '' u

Tactic:
rw [← preimage_preimage (g := f) (f := Subtype.val), ← image_val_preimage_restrictPreimage,
    preimage_image_eq _ Subtype.val_injective]

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

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
f : α → β
s : Set α
x✝ : β
⊢ (x✝ ∈ range fun x ↦ f ↑x) → x✝ ∈ f '' s

Tactic:
rintro ⟨⟨x, h1⟩, h2⟩
    exact ⟨x, h1, h2⟩

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

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
s : Set β
⊢ f '' f ⁻¹' s = s

Tactic:
hf.image_preimage

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
s : Set β
⊢ (?m.10 '' f ⁻¹' s).Nonempty ↔ s.Nonempty

pp: α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
s : Set β
⊢ Type ?u.17

pp: α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
s : Set β
⊢ α → ?m.9

Tactic:
hf.image_preimage

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
s : Set β
⊢ s.Nonempty ↔ s.Nonempty
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
s t : Set β
h : Disjoint (f ⁻¹' s) (f ⁻¹' t)
⊢ s ∩ t = ∅

Tactic:
← image_preimage_eq (_ ∩ _) hf,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
s t : Set β
h : Disjoint (f ⁻¹' s) (f ⁻¹' t)
⊢ f '' f ⁻¹' (s ∩ t) = ∅
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : SurjOn f s t
⊢ s.Nonempty ∨ t = ∅

Tactic:
by_contra!
  exact (h.comap_nonempty this.2).ne_empty this.1

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
f' : β → α
hf : LeftInvOn f' f s
⊢ f' '' f '' s = s

Tactic:
rw [Set.image_image, image_congr hf, image_id']

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

Goal state before:
pp: G : Type u_2
inst✝¹ : Group G
inst✝ : IsMulTorsionFree G
n : ℤ
a : G
⊢ a ^ n = 1 ↔ a = 1 ∨ n = 0

Tactic:
obtain rfl | hn := eq_or_ne n 0 <;> simp [zpow_eq_one_iff_left, *]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
f : α → β
t' : Set β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
⊢ ∃ s', s ⊆ s' ∧ s' ⊆ s₁ ∧ BijOn f s' t'

Tactic:
by
  obtain ⟨r, hrss, hbij⟩ := exists_subset_bijOn ((s₁ ∩ f ⁻¹' t') \ f ⁻¹' t) f
  rw [image_sdiff_preimage, image_inter_preimage] at hbij
  refine ⟨s ∪ r, subset_union_left, ?_, ?_, ?_, fun y hyt' ↦ ?_⟩
  · exact union_subset hss₁ <| hrss.trans <| sdiff_subset.trans inter_subset_left
  · rw [mapsTo_iff_image_subset, image_union, hbij.image_eq, h.image_eq, union_subset_iff]
    exact ⟨htt', sdiff_subset.trans inter_subset_right⟩
  · rw [injOn_union, and_iff_right h.injOn, and_iff_right hbij.injOn]
    · refine fun x hxs y hyr hxy ↦ (hrss hyr).2 ?_
      rw [← h.image_eq]
      exact ⟨x, hxs, hxy⟩
    exact (subset_sdiff.1 hrss).2.symm.mono_left h.mapsTo
  rw [image_union, h.image_eq, hbij.image_eq, union_sdiff_self]
  exact .inr ⟨ht' hyt', hyt'⟩

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
x y : M₁
⊢ f x / f y = f x * (f y)⁻¹

Tactic:
by rw [← inv, ← mul, ← div, div_eq_mul_inv]

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

Goal state before:
pp: case hf_swap
α : Type u_1
β : Type u_2
inst✝¹ : Monoid β
r : α → α → Prop
inst✝ : Std.Total r
f : α → α → β
p : α → Prop
hswap : ∀ {a b : α}, p a → p b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a → p b → p c → f a c = f a b * f b c
a b c : α
pa : p a
pb : p b
pc : p c
this : Std.Symm fun x1 x2 ↦ p x1 ∧ p x2
⊢ ∀ {a b : α}, p a ∧ p b → f a b * f b a = 1

Tactic:
and_imp

Goal state after:
case hf_swap
α : Type u_1
β : Type u_2
inst✝¹ : Monoid β
r : α → α → Prop
inst✝ : Std.Total r
f : α → α → β
p : α → Prop
hswap : ∀ {a b : α}, p a → p b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a → p b → p c → f a c = f a b * f b c
a b c : α
pa : p a
pb : p b
pc : p c
this : Std.Symm fun x1 x2 ↦ p x1 ∧ p x2
⊢ ∀ {a b : α}, p a → p b → f a b * f b a = 1
Module: Mathlib.Algebra.Group.End

Goal state before:
pp: α : Type u_7
β : α → Type u_8
⊢ Function.Injective ⇑(sigmaCongrRightHom β)

Tactic:
intro x y h

Goal state after:
α : Type u_7
β : α → Type u_8
x y : (a : α) → Perm (β a)
h : (sigmaCongrRightHom β) x = (sigmaCongrRightHom β) y
⊢ x = y
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: M₀ : Type u_1
inst✝ : MulZeroClass M₀
a b : M₀
h : a ≠ 0 → b = 0
⊢ a * b = 0

Tactic:
by
  have : Decidable (a = 0) := Classical.propDecidable (a = 0)
  exact if ha : a = 0 then by rw [ha, zero_mul] else by rw [h ha, mul_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:
intro x y h

Goal state after:
α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
x y : Perm (Subtype p)
h : ofSubtype x = ofSubtype y
⊢ x = y
Module: Mathlib.Algebra.Ring.Hom.Defs

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : CommRing β
f : β →+ α
h : ∀ (x : β), f (x * x) = f x * f x
h_two : 2 ≠ 0
h_one : f 1 = 1
x y : β
hxy : f (x * y) + (f (x * y) - 2 * (f x * f y)) = 0
⊢ (↑f).toFun (x * y) = (↑f).toFun x * (↑f).toFun y

Tactic:
← add_sub_assoc,

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : CommRing β
f : β →+ α
h : ∀ (x : β), f (x * x) = f x * f x
h_two : 2 ≠ 0
h_one : f 1 = 1
x y : β
hxy : f (x * y) + f (x * y) - 2 * (f x * f y) = 0
⊢ (↑f).toFun (x * y) = (↑f).toFun x * (↑f).toFun y
Module: Mathlib.Algebra.GroupWithZero.Semiconj

Goal state before:
pp: case pos
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a x y : G₀
h : SemiconjBy a x y
ha : a = 0
⊢ SemiconjBy a x⁻¹ y⁻¹

pp: case neg
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a x y : G₀
h : SemiconjBy a x y
ha : ¬a = 0
⊢ SemiconjBy a x⁻¹ y⁻¹

Tactic:
· simp only [ha, zero_left]

Goal state after:
case neg
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a x y : G₀
h : SemiconjBy a x y
ha : ¬a = 0
⊢ SemiconjBy a x⁻¹ y⁻¹
Module: Mathlib.Algebra.GroupWithZero.Semiconj

Goal state before:
pp: G₀ : Type u_1
inst✝ : GroupWithZero G₀
a x y : G₀
h : SemiconjBy a x y
n : ℕ
⊢ SemiconjBy a (x ^ ↑n) (y ^ ↑n)

Tactic:
simp [h.pow_right n]

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
hx : ¬IsUnit a
n : ℕ
⊢ IsUnit (a ^ n) ↔ n = 0

Tactic:
by
  rcases n with (_ | n) <;>
  simp [hx]

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

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
a b : G₀
ha : a ≠ 0
hb : b ≠ 0
⊢ a / b ≠ 0

Tactic:
rw [div_eq_mul_inv]
  exact mul_ne_zero ha (inv_ne_zero hb)

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

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

Tactic:
by
  rw [iterate_mul, involutive_iff_iter_2_eq_id.1 hf, iterate_id]

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b : α
inst✝ : AddLeftMono α
h : a ≤ b
c : α
⊢ c ≤ a + (c - a)

Tactic:
← le_add_tsub

Goal state after:
α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b : α
inst✝ : AddLeftMono α
h : a ≤ b
c : α
⊢ c ≤ c
Module: Mathlib.Algebra.Order.Sub.Defs

Goal state before:
pp: α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c : α
inst✝ : AddLeftMono α
⊢ a + b ≤ a + (c + (b - c))

Tactic:
← le_add_tsub

Goal state after:
α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c : α
inst✝ : AddLeftMono α
⊢ a + b ≤ a + b
Module: Mathlib.Algebra.Order.Sub.Defs

Goal state before:
pp: α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c : α
inst✝ : AddLeftMono α
⊢ a ≤ b + (a - b)

Tactic:
← le_add_tsub

Goal state after:
α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c : α
inst✝ : AddLeftMono α
⊢ a ≤ a
Module: Mathlib.Algebra.Order.Sub.Defs

Goal state before:
pp: α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : AddLeftMono α
a b c : α
⊢ a - b + b ≤ a - b + (c + (b - c))

Tactic:
← le_add_tsub

Goal state after:
α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : AddLeftMono α
a b c : α
⊢ a - b + b ≤ a - b + b
Module: Mathlib.Algebra.Order.Sub.Defs

Goal state before:
pp: α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c : α
inst✝ : AddLeftMono α
⊢ a + c ≤ b + (a - b) + c

Tactic:
← le_add_tsub

Goal state after:
α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c : α
inst✝ : AddLeftMono α
⊢ a + c ≤ a + c
Module: Mathlib.Algebra.Ring.GrindInstances

Goal state before:
pp: α : Type u_1
s : Semiring α
⊢ ∀ (a : α), a * 1 = a

Tactic:
by simp [mul_one]

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

Goal state before:
pp: M₀ : Type u_2
inst✝² : MonoidWithZero M₀
inst✝¹ : Preorder M₀
inst✝ : ZeroLEOneClass M₀
n : ℕ
⊢ 0 ^ (n + 1) ≤ 1

Tactic:
rw [zero_pow n.succ_ne_zero]; exact zero_le_one

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

Goal state before:
pp: R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : Preorder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : PosMulMono R
inst✝¹ : AddRightMono R
inst✝ : AddRightReflectLE R
h : b ≤ a
hc : c ≤ 0
d : R
hcd : 0 = c + d
⊢ d * a = c * b + (d * b + d * a)

Tactic:
rw [← add_assoc, ← add_mul, ← hcd, zero_mul, zero_add]

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

Goal state before:
pp: R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : Preorder R
a b : R
inst✝³ : ExistsAddOfLE R
inst✝² : PosMulMono R
inst✝¹ : AddRightMono R
inst✝ : AddRightReflectLE R
ha : a ≤ 0
h : b ≤ 1
⊢ a ≤ a * b

Tactic:
by
  simpa only [mul_one] using mul_le_mul_of_nonpos_left h ha

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

Goal state before:
pp: R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : Preorder R
a b : R
inst✝³ : ExistsAddOfLE R
inst✝² : PosMulMono R
inst✝¹ : AddRightMono R
inst✝ : AddRightReflectLE R
ha : a ≤ 0
h : 1 ≤ b
⊢ a * b ≤ a

Tactic:
by
  simpa only [mul_one] using mul_le_mul_of_nonpos_left h ha

Goal state after: