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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a x y b : G
⊢ SemiconjBy (b * a * b⁻¹) (b * x * b⁻¹) (b * y * b⁻¹) ↔ SemiconjBy a x y

Tactic:
by
  unfold SemiconjBy
  simp only [← mul_assoc, inv_mul_cancel_right]
  repeat rw [mul_assoc]
  rw [mul_left_cancel_iff, ← mul_assoc, ← mul_assoc, mul_right_cancel_iff]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α β : Sort u
e : β = α
a : α
b : β
h : a ≍ b
⊢ a = cast e b

Tactic:
by cases h; rfl

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : BEq α
inst✝² : LawfulBEq α
inst✝¹ : BEq β
inst✝ : LawfulBEq β
a₁ a₂ : α
b₁ b₂ : β
⊢ (a₁ == a₂) = (b₁ == b₂) ↔ (a₁ = a₂ ↔ b₁ = b₂)

Tactic:
by rw [Bool.eq_iff_iff]; simp

Goal state after:
Module: Mathlib.Logic.Unique

Goal state before:
pp: case refine_1
A : Sort u_2
B : Sort u_3
inst✝¹ : Unique A
inst✝ : Unique B
f : A → B
⊢ Function.LeftInverse default f

Tactic:
intro x

Goal state after:
case refine_1
A : Sort u_2
B : Sort u_3
inst✝¹ : Unique A
inst✝ : Unique B
f : A → B
x : A
⊢ default (f x) = x
Module: Mathlib.Logic.Unique

Goal state before:
pp: case refine_2
A : Sort u_2
B : Sort u_3
inst✝¹ : Unique A
inst✝ : Unique B
f : A → B
⊢ Function.RightInverse default f

Tactic:
intro x

Goal state after:
case refine_2
A : Sort u_2
B : Sort u_3
inst✝¹ : Unique A
inst✝ : Unique B
f : A → B
x : B
⊢ f (default x) = x
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:
by
  intros a b
  simp [Option.bind_eq_some_iff, hh _, hf _]

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

Goal state before:
pp: α : Type u_3
β : Type u_4
A B : Set (α → β)
hAB : A ⊆ B
hA : A.SeparatesPoints
⊢ B.SeparatesPoints

Tactic:
intro x

Goal state after:
α : Type u_3
β : Type u_4
A B : Set (α → β)
hAB : A ⊆ B
hA : A.SeparatesPoints
x : α
⊢ ∀ ⦃y : α⦄, x ≠ y → ∃ f, f ∈ B ∧ f x ≠ f y
Module: Mathlib.Data.FunLike.Basic

Goal state before:
pp: F : Sort u_1
α : Sort u_2
β : α → Sort u_3
i : DFunLike F α β
f g : F
h : f = g
⊢ ⇑f = ⇑g

Tactic:
by cases h; rfl

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

Goal state before:
pp: α : Type u
β : Type v
P : α ⊕ β → Sort u_3
f : (i : α) → P (inl i)
g : (i : β) → P (inr i)
x y : α ⊕ β
h : x = y
⊢ rec f g x = cast ⋯ (rec f g y)

Tactic:
by cases h; rfl

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
x : α ⊕ β
c : γ
h : LiftRel r s x (inl c)
⊢ x.isLeft = true

Tactic:
by cases h; rfl

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
y : γ ⊕ δ
a : α
h : LiftRel r s (inl a) y
⊢ y.isLeft = true

Tactic:
by cases h; rfl

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
x : α ⊕ β
d : δ
h : LiftRel r s x (inr d)
⊢ x.isRight = true

Tactic:
by cases h; rfl

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
y : γ ⊕ δ
b : β
h : LiftRel r s (inr b) y
⊢ y.isRight = true

Tactic:
by cases h; rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
H : Function.Injective f
a : α
o : Option α
⊢ f a ∈ Option.map f o ↔ a ∈ o

Tactic:
by
  aesop

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
a b : α
p : α → Prop
ha : a ≤ b → p a
hb : b ≤ a → p b
⊢ p (min a b)

Tactic:
obtain hab | hba := le_total a b

Goal state after:
case inl
α : Type u_2
inst✝ : LinearOrder α
a b : α
p : α → Prop
ha : a ≤ b → p a
hb : b ≤ a → p b
hab : a ≤ b
⊢ p (min a b)

case inr
α : Type u_2
inst✝ : LinearOrder α
a b : α
p : α → Prop
ha : a ≤ b → p a
hb : b ≤ a → p b
hba : b ≤ a
⊢ p (min a b)
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
⊢ (fun x1 x2 ↦ x1 < x2)ᶜ = fun x1 x2 ↦ x1 ≥ x2

Tactic:
by simp [compl]

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
⊢ (fun x1 x2 ↦ x1 ≤ x2)ᶜ = fun x1 x2 ↦ x1 > x2

Tactic:
by simp [compl]

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
⊢ (fun x1 x2 ↦ x1 > x2)ᶜ = fun x1 x2 ↦ x1 ≤ x2

Tactic:
by simp [compl]

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
⊢ (fun x1 x2 ↦ x1 ≥ x2)ᶜ = fun x1 x2 ↦ x1 < x2

Tactic:
by simp [compl]

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

Goal state before:
pp: a : ℕ
ha : 2 ≤ a
⊢ Injective fun x ↦ a ^ x

Tactic:
simp [Injective, le_antisymm_iff, Nat.pow_le_pow_iff_right ha]

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

Goal state before:
pp: case refl
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Injective next
⊢ Injective (leRecOn ⋯ fun {k} ↦ next)

Tactic:
intro x

Goal state after:
case refl
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Injective next
x : C n
⊢ ∀ ⦃a₂ : C n⦄, leRecOn ⋯ (fun {k} ↦ next) x = leRecOn ⋯ (fun {k} ↦ next) a₂ → x = a₂
Module: Mathlib.Data.Nat.Basic

Goal state before:
pp: case step
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Injective next
m✝ : ℕ
hnm : n.le m✝
ih : Injective (leRecOn hnm fun {k} ↦ next)
⊢ Injective (leRecOn ⋯ fun {k} ↦ next)

Tactic:
intro x

Goal state after:
case step
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Injective next
m✝ : ℕ
hnm : n.le m✝
ih : Injective (leRecOn hnm fun {k} ↦ next)
x : C n
⊢ ∀ ⦃a₂ : C n⦄, leRecOn ⋯ (fun {k} ↦ next) x = leRecOn ⋯ (fun {k} ↦ next) a₂ → x = a₂
Module: Mathlib.Data.Nat.Basic

Goal state before:
pp: case refl
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Surjective next
⊢ Surjective (leRecOn ⋯ fun {k} ↦ next)

Tactic:
intro x

Goal state after:
case refl
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Surjective next
x : C n
⊢ ∃ a, leRecOn ⋯ (fun {k} ↦ next) a = x
Module: Mathlib.Data.Nat.Basic

Goal state before:
pp: case step
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Surjective next
m✝ : ℕ
hnm : n.le m✝
ih : Surjective (leRecOn hnm fun {k} ↦ next)
⊢ Surjective (leRecOn ⋯ fun {k} ↦ next)

Tactic:
intro x

Goal state after:
case step
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Surjective next
m✝ : ℕ
hnm : n.le m✝
ih : Surjective (leRecOn hnm fun {k} ↦ next)
x : C m✝.succ
⊢ ∃ a, leRecOn ⋯ (fun {k} ↦ next) a = x
Module: Mathlib.Data.Nat.Init

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

Tactic:
leRec,

Goal state after:
m n : ℕ
motive : (m : ℕ) → n ≤ m → Sort u_1
refl : motive n ⋯
le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯
h1 : n ≤ m
h2 : n ≤ m + 1
| ⋯.by_cases (fun h ↦ le_succ_of_le h (leRec refl le_succ_of_le h)) fun h ↦
    Eq.ndrec (motive := fun {n} ↦
      {motive : (m : ℕ) → n ≤ m → Sort u_1} →
        motive n ⋯ → (⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯) → (H : n ≤ m + 1) → motive (m + 1) H)
      (fun {motive} refl le_succ_of_le H ↦ refl) ⋯ refl le_succ_of_le h2
Module: Mathlib.Data.Set.Operations

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α → γ
s : Set α
t : Set β
⊢ (f '' s) ×ˢ t = (fun x ↦ (f x.fst, x.snd)) '' s ×ˢ t

Tactic:
by
  aesop

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α → γ
s : Set α
t : Set β
⊢ t ×ˢ (f '' s) = (fun x ↦ (x.fst, f x.snd)) '' t ×ˢ s

Tactic:
by
  aesop

Goal state after:
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

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 : α
⊢ ∀ ⦃b : α⦄, x < b → (fun x ↦ if p x then f x else g x) x < (fun x ↦ if p x then f x else g x) b
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: case neg
f : ℕ → ℕ
mono_f : Monotone f
c : ℕ
ih : (∀ (n : ℕ), f n ≤ c) → ∃ b N, ∀ (n : ℕ), n ≥ N → f n = b
hc : ∀ (n : ℕ), f n ≤ c + 1
N : ℕ
hN : f N = c + 1
⊢ ∃ b N, ∀ (n : ℕ), n ≥ N → f n = b

Tactic:
use c + 1, N

Goal state after:
case h
f : ℕ → ℕ
mono_f : Monotone f
c : ℕ
ih : (∀ (n : ℕ), f n ≤ c) → ∃ b N, ∀ (n : ℕ), n ≥ N → f n = b
hc : ∀ (n : ℕ), f n ≤ c + 1
N : ℕ
hN : f N = c + 1
⊢ ∀ (n : ℕ), n ≥ N → f n = c + 1
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: case neg
f : ℕ → ℕ
mono_f : Monotone f
c : ℕ
ih : (∀ (n : ℕ), f n ≤ c) → ∃ b N, ∀ (n : ℕ), n ≥ N → f n = b
hc : ∀ (n : ℕ), f n ≤ c + 1
h : ∃ n, c < f n
⊢ ∃ b N, ∀ (n : ℕ), n ≥ N → f n = b

Tactic:
· obtain ⟨N, hN⟩ := h
      replace hN : f N = c + 1 := by specialize hc N; lia
      use c + 1, N; intro n hn
      specialize mono_f hn; specialize hc n; lia

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : SemilatticeSup α
inst✝ : Preorder β
f : α → β
h : ∀ (x y : α), f x ≤ f (x ⊔ y)
⊢ Monotone f

Tactic:
intro x

Goal state after:
α : Type u
β : Type v
inst✝¹ : SemilatticeSup α
inst✝ : Preorder β
f : α → β
h : ∀ (x y : α), f x ≤ f (x ⊔ y)
x : α
⊢ ∀ ⦃b : α⦄, x ≤ b → f x ≤ f b
Module: Mathlib.Order.Heyting.Basic

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

Tactic:
rw [sup_comm, sup_sdiff_right_self]

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

Goal state before:
pp: α : Type u_2
inst✝ : HeytingAlgebra α
a : α
⊢ Disjoint a a ↔ a = ⊥

Tactic:
disjoint_self

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

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

Tactic:
compl_compl_compl

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

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

Tactic:
compl_compl_compl

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

Goal state before:
pp: α : Type u_1
s t : Set α
⊢ s ∩ t ∪ s \ t = s

Tactic:
exact sup_inf_sdiff _ _

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CoheytingAlgebra β
generalizedCoheytingAlgebra : GeneralizedCoheytingAlgebra α := e.generalizedCoheytingAlgebra
top : Top α := e.top
⊢ CoheytingAlgebra α

Tactic:
let hnot := e.hnot

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CoheytingAlgebra β
generalizedCoheytingAlgebra : GeneralizedCoheytingAlgebra α := e.generalizedCoheytingAlgebra
top : Top α := e.top
hnot : HNot α := e.hnot
⊢ CoheytingAlgebra α
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_9
β : Type u_10
f : α → β
p : α → Prop
q : β → Prop
h : ∀ (x : α), p x ↔ q (f x)
y : Subtype q
⊢ ∀ (x : α), (∃ h_1, ⟨f ↑⟨x, h_1⟩, ⋯⟩ = y) ↔ f x = ↑y

Tactic:
intro x

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_9
β : Type u_10
f : α → β
p : α → Prop
q : β → Prop
h : ∀ (x : α), p x ↔ q (f x)
y : Subtype q
x : α
⊢ (∃ h_1, ⟨f ↑⟨x, h_1⟩, ⋯⟩ = y) ↔ f 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
α : Type ?u.12
p : Option α → Type v
h : ∀ (a : p none), False
⊢ ∀ (x : Option α) (a : p x), x.isSome = true

Tactic:
intro x

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.12
p : Option α → Type v
h : ∀ (a : p none), False
x : Option α
⊢ ∀ (a : p x), x.isSome = true
Module: Mathlib.Logic.Equiv.Basic

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

Tactic:
rintro ⟨a, ha, rfl⟩

Goal state after:
case mp
α : Type u_9
inst✝ : DecidableEq α
s : Set α
i j : α
hi : i ∈ s
hj : ¬j ∈ s
a : α
ha : a ∈ s
⊢ (swap i j) a ∈ insert j s \ {i}
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: case mp.inl
α : Type u_9
inst✝ : DecidableEq α
s : Set α
j : α
hj : ¬j ∈ s
a : α
ha hi : a ∈ s
⊢ (swap a j) a ∈ insert j s \ {a}

Tactic:
rw [swap_apply_left]; exact ⟨.inl rfl, (ne_of_mem_of_not_mem hi hj).symm⟩

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

Goal state before:
pp: α : Type u_9
β : Type u_10
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
i j : α
⊢ (swap i j).sumCongr (Equiv.refl β) = swap (Sum.inl i) (Sum.inl j)

Tactic:
by
  aesop

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

Goal state before:
pp: α : Type u_9
β : Type u_10
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
i j : β
⊢ sumCongr (Equiv.refl α) (swap i j) = swap (Sum.inr i) (Sum.inr j)

Tactic:
by
  aesop

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

Goal state before:
pp: α : Sort u_1
β : Sort u_4
P : α → Sort u_9
e : α ≃ β
g : (b : β) → P (e.symm b)
b : β
⊢ (piCongrLeft' P e).symm g (e.symm b) = g b

Tactic:
rw [piCongrLeft'_symm_apply, ← heq_iff_eq, eqRec_heq_iff]

Goal state after:
α : Sort u_1
β : Sort u_4
P : α → Sort u_9
e : α ≃ β
g : (b : β) → P (e.symm b)
b : β
⊢ g (e (e.symm b)) ≍ g b
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_4
α' : Sort u_9
inst✝¹ : DecidableEq α'
inst✝ : DecidableEq α
f : α → β
g : α' ≃ α
a : α
v : β
⊢ update f a v ∘ ⇑g = update f (g (g.symm a)) v ∘ ⇑g

Tactic:
g.apply_symm_apply

Goal state after:
α : Sort u_1
β : Sort u_4
α' : Sort u_9
inst✝¹ : DecidableEq α'
inst✝ : DecidableEq α
f : α → β
g : α' ≃ α
a : α
v : β
⊢ update f a v ∘ ⇑g = update f a v ∘ ⇑g
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
a b c : α
h : Disjoint b c
⊢ a ≤ a ∆ b ⊔ a ∆ c

Tactic:
by
  simp_rw [symmDiff_comm a]
  exact h.le_symmDiff_sup_symmDiff_left

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f g : α → β
s : Set α
h : ∀ (a : α), a ∈ s → f a = g a
⊢ f '' s = g '' s

Tactic:
by
  aesop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s : Set α
t : Set β
f f' : α → γ
g g' : β → δ
h : EqOn (Prod.map f g) (Prod.map f' g') (s ×ˢ t)
x : β
hxt : x ∈ t
⊢ EqOn f f' s

Tactic:
intro x

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s : Set α
t : Set β
f f' : α → γ
g g' : β → δ
h : EqOn (Prod.map f g) (Prod.map f' g') (s ×ˢ t)
x✝ : β
hxt : x✝ ∈ t
x : α
⊢ x ∈ s → f x = f' x
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s : Set α
t : Set β
f f' : α → γ
g g' : β → δ
h : EqOn (Prod.map f g) (Prod.map f' g') (s ×ˢ t)
x : α
hxs : x ∈ s
⊢ EqOn g g' t

Tactic:
intro x

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s : Set α
t : Set β
f f' : α → γ
g g' : β → δ
h : EqOn (Prod.map f g) (Prod.map f' g') (s ×ˢ t)
x✝ : α
hxs : x✝ ∈ s
x : β
⊢ x ∈ t → g x = g' x
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
x : α
s : Set α
f : ↑(insert x s) → β
⊢ range f = insert (f ⟨x, ⋯⟩) (range fun y ↦ f ⟨↑y, ⋯⟩)

Tactic:
by
  aesop

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
⊢ s.pi t = ∅ ↔ ∃ i, IsEmpty (α i) ∨ i ∈ s ∧ t i = ∅

Tactic:
rw [← not_nonempty_iff_eq_empty, pi_nonempty_iff]
  push Not
  refine exists_congr fun i => ?_
  cases isEmpty_or_nonempty (α i) <;> simp [*, forall_and, eq_empty_iff_forall_notMem]

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

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

Tactic:
intro x

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
f : α → β
h : Disjoint s₁ s₂
H : InjOn f (s₁ ∪ s₂)
x : α
⊢ x ∈ s₁ → ∀ (y : α), y ∈ s₂ → f x ≠ f y
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
inst✝ : Nonempty β
x✝ : ∃ f, Injective f
f : ↑s → β
hf : Injective f
⊢ ∃ f, InjOn f s

Tactic:
lift f to α → β using trivial

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
inst✝ : Nonempty β
x✝ : ∃ f, Injective f
f : α → β
hf : Injective fun i ↦ f ↑i
⊢ ∃ f, InjOn f s
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

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 : β
⊢ x ∈ f '' s ∩ f '' t → x ∈ f '' (s ∩ t)
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s : Set α
t : Set β
f : α → γ
g : β → δ
⊢ graphOn f s ×ˢ graphOn g t = ⇑(Equiv.prodProdProdComm α γ β δ) ⁻¹' graphOn (Prod.map f g) (s ×ˢ t)

Tactic:
by
  aesop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s : Set α
t : Set β
f : α → γ
g : β → δ
⊢ graphOn (Prod.map f g) (s ×ˢ t) = ⇑(Equiv.prodProdProdComm α β γ δ) ⁻¹' graphOn f s ×ˢ graphOn g t

Tactic:
by
  aesop

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
M✝ : Type u_4
N : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
inst✝¹ : EquivLike F α β
ι : Type u_9
M : ι → Type u_10
inst✝ : (i : ι) → Mul (M i)
i j : ι
h : i = j
x✝¹ x✝ : M i
⊢ (Equiv.cast ⋯).toFun (x✝¹ * x✝) = (Equiv.cast ⋯).toFun x✝¹ * (Equiv.cast ⋯).toFun x✝

Tactic:
by cases h; rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
⊢ s = ∅ → BijOn f s ∅

Tactic:
rintro rfl; exact bijOn_empty f

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

Goal state before:
pp: α : Type u_1
β : Type u_2
t : Set β
f : α → β
⊢ t = ∅ → BijOn f ∅ t

Tactic:
rintro rfl; exact bijOn_empty f

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

Goal state before:
pp: case refine_2
α : 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
⊢ SurjOn g (p₁ '' s) (p₂ '' t)

Tactic:
rintro _ ⟨b, hb, rfl⟩
    obtain ⟨a, ha, rfl⟩ := h3 hb
    grind

Goal state after:
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✝ : RightCancelMonoid N
f : M →ₙ* N
⊢ f 1 = 1

Tactic:
have h : 1 * f 1 = f 1 * f 1 := by simpa using f.map_mul' 1 1
    exact (mul_right_cancel h).symm

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : ¬a ∈ s
hfa : ¬f a ∈ t
h : BijOn f (insert a s) (insert (f a) t)
this : f '' s \ {f a} = t
⊢ ∀ (x : α), x ∈ s → ¬f x = f a

Tactic:
intro x

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : ¬a ∈ s
hfa : ¬f a ∈ t
h : BijOn f (insert a s) (insert (f a) t)
this : f '' s \ {f a} = t
x : α
⊢ x ∈ s → ¬f x = f a
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 x = f x'

Tactic:
rw [← invFunOn_apply_eq (f := f) hx, he, invFunOn_apply_eq (f := f) hx']

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

Goal state before:
pp: α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
h : Semiconj f fa fb
s : Set β
hb : InjOn fb s
hf : InjOn f (f ⁻¹' s)
⊢ InjOn fa (f ⁻¹' s)

Tactic:
intro x

Goal state after:
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
h : Semiconj f fa fb
s : Set β
hb : InjOn fb s
hf : InjOn f (f ⁻¹' s)
x : α
⊢ x ∈ f ⁻¹' s → ∀ ⦃x₂ : α⦄, x₂ ∈ f ⁻¹' s → fa x = fa x₂ → x = x₂
Module: Mathlib.Algebra.Group.Basic

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

Tactic:
← div_eq_mul_inv

Goal state after:
α : Type u_1
inst✝ : DivisionMonoid α
a b : α
h : a / b = 1
⊢ a / b = 1
Module: Mathlib.Algebra.Group.Units.Defs

Goal state before:
pp: α : Type u
M : Type u_1
hM : Monoid M
h : ∀ (a : M), IsUnit a
a : M
⊢ a = ↑⋯.unit * 1

Tactic:
(h a).unit_spec,

Goal state after:
α : Type u
M : Type u_1
hM : Monoid M
h : ∀ (a : M), IsUnit a
a : M
⊢ a = a * 1
Module: Mathlib.Algebra.Group.Units.Defs

Goal state before:
pp: α : Type u
M : Type u_1
hM : CommMonoid M
h : ∀ (a : M), IsUnit a
a : M
⊢ a = ↑⋯.unit * 1

Tactic:
(h a).unit_spec,

Goal state after:
α : Type u
M : Type u_1
hM : CommMonoid M
h : ∀ (a : M), IsUnit a
a : M
⊢ a = a * 1
Module: Mathlib.Algebra.Group.Units.Basic

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

Tactic:
by
  rw [mul_comm, mul_comm _ c, mul_inv_eq_mul_inv_iff]

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

Goal state before:
pp: G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
x✝ : M × N
⊢ 1 * x✝ = x✝

Tactic:
by ext <;> exact one_mul _

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

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

Tactic:
intro x

Goal state after:
α : Type u_7
β : α → Type u_8
x : (a : α) → Perm (β a)
⊢ ∀ ⦃a₂ : (a : α) → Perm (β a)⦄, (sigmaCongrRightHom β) x = (sigmaCongrRightHom β) a₂ → x = a₂
Module: Mathlib.Algebra.Group.End

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

Tactic:
intro x

Goal state after:
α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
x : Perm (Subtype p)
⊢ ∀ ⦃a₂ : Perm (Subtype p)⦄, ofSubtype x = ofSubtype a₂ → x = a₂
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: R : Type u_3
inst✝ : MonoidWithZero R
x : R
m : ℕ
h✝ : IsNilpotent (x ^ m)
n : ℕ
h : (x ^ m) ^ n = 0
⊢ x ^ (m * n) = 0

Tactic:
rw [← h, pow_mul x m n]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : MulZeroOneClass α
inst✝¹ : MulZeroOneClass β
inst✝ : MulZeroOneClass γ
g : β →*₀ γ
f₁ f₂ : α →*₀ β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
x : α
⊢ g (f₁ x) = g (f₂ x)

Tactic:
rw [← comp_apply, h,
    comp_apply]

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

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

Tactic:
rw [← Nat.cast_one, ← Nat.cast_add]

Goal state after:
R : Type u_1
inst✝ : AddMonoidWithOne R
⊢ ↑(1 + 1) = 2