mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Ring.InjSurj

Goal state before:
pp: R : Type u_1
S : Type u_2
f : R → S
hf : Surjective f
inst✝¹¹ : Add S
inst✝¹⁰ : Mul S
inst✝⁹ : Zero S
inst✝⁸ : One S
inst✝⁷ : Neg S
inst✝⁶ : Sub S
inst✝⁵ : SMul ℕ S
inst✝⁴ : SMul ℤ S
inst✝³ : Pow S ℕ
inst✝² : NatCast S
inst✝¹ : IntCast S
inst✝ : AddMonoidWithOne R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : R), f (x + y) = f x + f y
nsmul : ∀ (n : ℕ) (x : R), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f ↑n = ↑n
n : ℕ
⊢ ↑(n + 1) = ↑n + 1

Tactic:
← natCast,

Goal state after:
R : Type u_1
S : Type u_2
f : R → S
hf : Surjective f
inst✝¹¹ : Add S
inst✝¹⁰ : Mul S
inst✝⁹ : Zero S
inst✝⁸ : One S
inst✝⁷ : Neg S
inst✝⁶ : Sub S
inst✝⁵ : SMul ℕ S
inst✝⁴ : SMul ℤ S
inst✝³ : Pow S ℕ
inst✝² : NatCast S
inst✝¹ : IntCast S
inst✝ : AddMonoidWithOne R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : R), f (x + y) = f x + f y
nsmul : ∀ (n : ℕ) (x : R), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f ↑n = ↑n
n : ℕ
⊢ f ↑(n + 1) = ↑n + 1
Module: Mathlib.Algebra.Ring.Parity

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

Tactic:
| more n _ _ =>

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 c : α
inst✝ : AddLeftMono α
⊢ a ≤ c + (b - c) + (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 ≤ 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 α
⊢ c ≤ c - b + (a + (b - a))

Tactic:
← le_add_tsub,

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : AddLeftReflectLE α
h : a + d = c + b
⊢ a + d - d - b = c + b - b - d

Tactic:
rw [h, tsub_right_comm]

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

Goal state before:
pp: G₀ : Type u_3
inst✝¹ : GroupWithZero G₀
inst✝ : Preorder G₀
a b : G₀
ha : 0 ≤ a
⊢ a * b * b⁻¹ ≤ a

Tactic:
obtain rfl | hb := eq_or_ne b 0 <;> simp [*]

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

Goal state before:
pp: G₀ : Type u_3
inst✝¹ : GroupWithZero G₀
inst✝ : Preorder G₀
a b : G₀
ha : a ≤ 0
⊢ a ≤ a * b * b⁻¹

Tactic:
obtain rfl | hb := eq_or_ne b 0 <;> simp [*]

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

Goal state before:
pp: G₀ : Type u_3
inst✝¹ : GroupWithZero G₀
inst✝ : Preorder G₀
a b : G₀
ha : 0 ≤ a
⊢ a * b⁻¹ * b ≤ a

Tactic:
obtain rfl | hb := eq_or_ne b 0 <;> simp [*]

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

Goal state before:
pp: G₀ : Type u_3
inst✝¹ : GroupWithZero G₀
inst✝ : Preorder G₀
a b : G₀
ha : a ≤ 0
⊢ a ≤ a * b⁻¹ * b

Tactic:
obtain rfl | hb := eq_or_ne b 0 <;> simp [*]

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

Goal state before:
pp: R : Type u
inst✝⁴ : Semiring R
inst✝³ : LinearOrder R
inst✝² : ExistsAddOfLE R
inst✝¹ : PosMulMono R
inst✝ : AddLeftMono R
a : R
ha : a < 0
b : R
hab : 0 = a + b
hb : 0 < b
⊢ b ^ 2 + a * (a + b) = a ^ 2 + (a + b) * b

Tactic:
rw [add_mul, mul_add, sq, sq, add_comm, add_assoc]

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

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : LinearOrder G₀
a b : G₀
inst✝ : PosMulMono G₀
ha : 0 ≤ a
hb : b ≤ 0
⊢ a * b⁻¹ ≤ 0

Tactic:
exact mul_nonpos_of_nonneg_of_nonpos ha (inv_nonpos.2 hb)

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

Goal state before:
pp: case inl
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : LinearOrder G₀
inst✝¹ : PosMulStrictMono G₀
inst✝ : ZeroLEOneClass G₀
n : ℤ
ha₀ : 0 ≤ 0
ha₁ : 0 ≠ 1
⊢ 0 ^ n = 1 ↔ n = 0

Tactic:
exact zero_zpow_eq_one₀

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

Goal state before:
pp: G₀ : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ b * c⁻¹ ≤ a ↔ b ≤ c * a

Tactic:
by
  rw [mul_inv_le_iff₀ hc, mul_comm]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Asymm s
f : α → β
H : ∀ (a b : α), r a b → s (f a) (f b)
⊢ r ↪r s

Tactic:
haveI := @Std.Asymm.irrefl β s _
  refine ⟨⟨f, fun a b e => ?_⟩, @fun a b => ⟨fun h => ?_, H _ _⟩⟩
  · apply Std.Trichotomous.trichotomous (r := r) a b
    · exact fun h => irrefl (r := s) (f a) (by simpa [e] using H _ _ h)
    · exact fun h => irrefl (r := s) (f b) (by simpa [e] using H _ _ h)
  · refine Not.imp_symm (Std.Trichotomous.trichotomous a b · fun h' ↦ asymm (H _ _ h') h) ?_
    exact (irrefl _ <| · ▸ h)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type ?u.51
β₁ : Type ?u.54
α₂ : Type ?u.50
β₂ : Type ?u.53
r₁ : α₁ → α₁ → Prop
s₁ : β₁ → β₁ → Prop
r₂ : α₂ → α₂ → Prop
s₂ : β₂ → β₂ → Prop
e₁ : r₁ ≃r r₂
e₂ : s₁ ≃r s₂
f₁ : r₁ →r s₁
⊢ (fun f₂ ↦ e₂.symm.toRelEmbedding.toRelHom.comp (f₂.comp e₁.toRelEmbedding.toRelHom))
      ((fun f₁ ↦ e₂.toRelEmbedding.toRelHom.comp (f₁.comp e₁.symm.toRelEmbedding.toRelHom)) f₁) =
    f₁

Tactic:
by ext; simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type ?u.51
β₁ : Type ?u.54
α₂ : Type ?u.50
β₂ : Type ?u.53
r₁ : α₁ → α₁ → Prop
s₁ : β₁ → β₁ → Prop
r₂ : α₂ → α₂ → Prop
s₂ : β₂ → β₂ → Prop
e₁ : r₁ ≃r r₂
e₂ : s₁ ≃r s₂
f₂ : r₂ →r s₂
⊢ (fun f₁ ↦ e₂.toRelEmbedding.toRelHom.comp (f₁.comp e₁.symm.toRelEmbedding.toRelHom))
      ((fun f₂ ↦ e₂.symm.toRelEmbedding.toRelHom.comp (f₂.comp e₁.toRelEmbedding.toRelHom)) f₂) =
    f₂

Tactic:
by ext; simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type ?u.51
β₁ : Type ?u.54
α₂ : Type ?u.50
β₂ : Type ?u.53
r₁ : α₁ → α₁ → Prop
s₁ : β₁ → β₁ → Prop
r₂ : α₂ → α₂ → Prop
s₂ : β₂ → β₂ → Prop
e₁ : r₁ ≃r r₂
e₂ : s₁ ≃r s₂
f₁ : r₁ ↪r s₁
⊢ (fun f₂ ↦ (e₁.toRelEmbedding.trans f₂).trans e₂.symm.toRelEmbedding)
      ((fun f₁ ↦ (e₁.symm.toRelEmbedding.trans f₁).trans e₂.toRelEmbedding) f₁) =
    f₁

Tactic:
by ext; simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type ?u.51
β₁ : Type ?u.54
α₂ : Type ?u.50
β₂ : Type ?u.53
r₁ : α₁ → α₁ → Prop
s₁ : β₁ → β₁ → Prop
r₂ : α₂ → α₂ → Prop
s₂ : β₂ → β₂ → Prop
e₁ : r₁ ≃r r₂
e₂ : s₁ ≃r s₂
f₂ : r₂ ↪r s₂
⊢ (fun f₁ ↦ (e₁.symm.toRelEmbedding.trans f₁).trans e₂.toRelEmbedding)
      ((fun f₂ ↦ (e₁.toRelEmbedding.trans f₂).trans e₂.symm.toRelEmbedding) f₂) =
    f₂

Tactic:
by ext; simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type ?u.51
β₁ : Type ?u.54
α₂ : Type ?u.50
β₂ : Type ?u.53
r₁ : α₁ → α₁ → Prop
s₁ : β₁ → β₁ → Prop
r₂ : α₂ → α₂ → Prop
s₂ : β₂ → β₂ → Prop
e₁ : r₁ ≃r r₂
e₂ : s₁ ≃r s₂
f₁ : r₁ ≃r s₁
⊢ (fun f₂ ↦ (e₁.trans f₂).trans e₂.symm) ((fun f₁ ↦ (e₁.symm.trans f₁).trans e₂) f₁) = f₁

Tactic:
by ext; simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type ?u.51
β₁ : Type ?u.54
α₂ : Type ?u.50
β₂ : Type ?u.53
r₁ : α₁ → α₁ → Prop
s₁ : β₁ → β₁ → Prop
r₂ : α₂ → α₂ → Prop
s₂ : β₂ → β₂ → Prop
e₁ : r₁ ≃r r₂
e₂ : s₁ ≃r s₂
f₂ : r₂ ≃r s₂
⊢ (fun f₁ ↦ (e₁.symm.trans f₁).trans e₂) ((fun f₂ ↦ (e₁.trans f₂).trans e₂.symm) f₂) = f₂

Tactic:
by ext; simp

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

Goal state before:
pp: F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Preorder α✝
inst✝² : Preorder β✝
α : Type u_6
β : Type u_7
inst✝¹ : Unique α
inst✝ : Preorder β
⊢ ∀ {a b : α → β}, (Equiv.funUnique α β) a ≤ (Equiv.funUnique α β) b ↔ a ≤ b

Tactic:
by simp [Pi.le_def, Unique.forall_iff]

Goal state after:
Module: Mathlib.Algebra.Order.Group.Unbundled.Int

Goal state before:
pp: a : ℤ
⊢ a.sign * ↑a.natAbs = a

Tactic:
sign_mul_natAbs a

Goal state after:
a : ℤ
⊢ a = a
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Group α
inst✝ : Group β
x✝ : α ≃* β
⊢ (fun e ↦ { toFun := fun x ↦ unzero ⋯, invFun := fun x ↦ unzero ⋯, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ })
      ((fun e ↦ { toFun := ⇑(map' ↑e), invFun := ⇑(map' ↑e.symm), left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }) x✝) =
    x✝

Tactic:
by ext; simp

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 c : α
ha : AddLECancellable a
hc : AddLECancellable c
h : c ≤ a
⊢ a + c ≤ a + b → c ≤ b

Tactic:
apply ha

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

Goal state before:
pp: α : Type u
β : Type v
M : Type u_1
N : Type u_2
inst✝¹ : One M
inst✝ : One N
f : OneHom M N
⊢ map (⇑f) 1 = 1

Tactic:
WithBot.map_one,

Goal state after:
α : Type u
β : Type v
M : Type u_1
N : Type u_2
inst✝¹ : One M
inst✝ : One N
f : OneHom M N
⊢ ↑(f 1) = 1
Module: Mathlib.Algebra.Group.Invertible.Basic

Goal state before:
pp: α : Type u
inst✝² : Monoid α
a b : α
inst✝¹ : Invertible (a * b)
inst✝ : Invertible b
⊢ a * (b * ⅟(a * b)) = 1

Tactic:
rw [← mul_assoc, mul_invOf_self]

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

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

Tactic:
rw [add_div, mul_div_cancel_right₀ _ hc]

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

Goal state before:
pp: α : Type u_1
inst✝ : NonUnitalRing α
a b c : α
⊢ a ∣ b - c ↔ a ∣ c - b

Tactic:
by rw [← dvd_neg, neg_sub]

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

Goal state before:
pp: u v : ℤ
h : u * v = -1
⊢ u = 1 ∧ v = -1 ∨ u = -1 ∧ v = 1

Tactic:
obtain rfl | rfl := isUnit_eq_one_or (IsUnit.mul_iff.mp (Int.isUnit_iff.mpr (Or.inr h))).1
  · exact Or.inl ⟨rfl, one_mul v ▸ h⟩
  · simpa [Int.neg_mul] using h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → x ≤ a
b : α
hb : b ∈ s
hab : a < b
⊢ f a < f b

Tactic:
cases (ha _ hb).not_gt hab

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → a ≤ x
b : α
hb : b ∈ s
hab : b < a
⊢ f b < f a

Tactic:
cases (ha _ hb).not_gt hab

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → x ≤ a
b : α
hb : b ∈ s
hab : a < b
⊢ f b < f a

Tactic:
cases (ha _ hb).not_gt hab

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → a ≤ x
b : α
hb : b ∈ s
hab : b < a
⊢ f a < f b

Tactic:
cases (ha _ hb).not_gt hab

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t t' : Set β
⊢ image2 (fun b a ↦ f a b) t s ∪ image2 (fun b a ↦ f a b) t' s = image2 (fun a b ↦ f b a) t s ∪ image2 f s t'

Tactic:
image2_swap f

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t t' : Set β
⊢ image2 (fun b a ↦ f a b) t s ∪ image2 (fun b a ↦ f a b) t' s =
    image2 (fun a b ↦ f b a) t s ∪ image2 (fun a b ↦ f b a) t' s
Module: Mathlib.Data.Set.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
δ' : Type u_8
ε : Type u_9
s : Set α
t : Set β
u : Set γ
f : α → δ → ε
g : β → γ → δ
f' : α → γ → δ'
g' : β → δ' → ε
h_left_comm : ∀ (a : α) (b : β) (c : γ), f a (g b c) = g' b (f' a c)
⊢ image2 f s (image2 g t u) = image2 g' t (image2 (fun a b ↦ f' b a) u s)

Tactic:
image2_swap f

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
δ' : Type u_8
ε : Type u_9
s : Set α
t : Set β
u : Set γ
f : α → δ → ε
g : β → γ → δ
f' : α → γ → δ'
g' : β → δ' → ε
h_left_comm : ∀ (a : α) (b : β) (c : γ), f a (g b c) = g' b (f' a c)
⊢ image2 (fun a b ↦ f b a) (image2 g t u) s = image2 g' t (image2 (fun a b ↦ f' b a) u s)
Module: Mathlib.Data.Set.NAry

Goal state before:
pp: α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
f : α → β → γ
s : Set α
t : Set β
g : γ → δ
f' : β' → α' → δ
g₁ : β → β'
g₂ : α → α'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ b) (g₂ a)
⊢ g '' image2 f s t = image2 f' (g₁ '' t) (g₂ '' s)

Tactic:
image2_swap f

Goal state after:
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
f : α → β → γ
s : Set α
t : Set β
g : γ → δ
f' : β' → α' → δ
g₁ : β → β'
g₂ : α → α'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ b) (g₂ a)
⊢ g '' image2 (fun a b ↦ f b a) t s = image2 f' (g₁ '' t) (g₂ '' s)
Module: Mathlib.Order.Bounds.Image

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
h₀ : ∀ (b : β), Antitone (swap f b)
h₁ : ∀ (a : α), Monotone (f a)
a : α
ha : a ∈ lowerBounds s
b : β
hb : b ∈ upperBounds t
⊢ BddAbove (image2 f s t)

Tactic:
exact ⟨f a b, mem_upperBounds_image2_of_mem_upperBounds_of_mem_upperBounds h₀ h₁ ha hb⟩

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

Goal state before:
pp: α✝¹ : Sort u
β✝ : Sort v
γ : Sort w
α✝ : Type u_1
β : Type u_2
α : Type ?u.8
S : Set α
x : Set ↑S
⊢ (fun x ↦ Subtype.val ⁻¹' ↑x) ((fun x ↦ ⟨Subtype.val '' x, ⋯⟩) x) = x

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
⊢ Ico a b = ∅ ↔ ¬a < b

Tactic:
by
  contrapose!; exact nonempty_Ico

Goal state after:
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : One α
inst✝ : IsBotOneClass α
⊢ Ici 1 = univ

Tactic:
by ext; simp

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

Goal state before:
pp: α : Type u_4
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
h : 0 < a
b : α
this : 0 < a / max (b + 1) 1
⊢ b * (a / max (b + 1) 1) < a

Tactic:
← lt_div_iff₀ this,

Goal state after:
α : Type u_4
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
h : 0 < a
b : α
this : 0 < a / max (b + 1) 1
⊢ b < a / (a / max (b + 1) 1)
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b c : α
ha : b < c
⊢ AntitoneOn (fun x ↦ (x - c)⁻¹) (Set.Icc a b)

Tactic:
by_cases hab : a ≤ b
  · exact sub_inv_antitoneOn_Iio.mono <| (Set.Icc_subset_Iio_iff hab).mpr ha
  · simp [hab, Set.Subsingleton.antitoneOn]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
R S : α → β → Prop
H : ∀ (a : α) (b : β), R a b → S a b
l₁ : List α
l₂ : List β
h : Forall₂ R l₁ l₂
⊢ Forall₂ S l₁ l₂

Tactic:
induction h <;> constructor

Goal state after:
case cons.a
α : Type u_1
β : Type u_2
R S : α → β → Prop
H : ∀ (a : α) (b : β), R a b → S a b
l₁ : List α
l₂ : List β
a✝² : α
b✝ : β
l₁✝ : List α
l₂✝ : List β
a✝¹ : R a✝² b✝
a✝ : Forall₂ R l₁✝ l₂✝
a_ih✝ : Forall₂ S l₁✝ l₂✝
⊢ S a✝² b✝

case cons.a
α : Type u_1
β : Type u_2
R S : α → β → Prop
H : ∀ (a : α) (b : β), R a b → S a b
l₁ : List α
l₂ : List β
a✝² : α
b✝ : β
l₁✝ : List α
l₂✝ : List β
a✝¹ : R a✝² b✝
a✝ : Forall₂ R l₁✝ l₂✝
a_ih✝ : Forall₂ S l₁✝ l₂✝
⊢ Forall₂ S l₁✝ l₂✝
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: case cons
M : Type u_4
inst✝ : Monoid M
y z : M
l : List M
IH : (∀ (x : M), x ∈ l → Commute y x) → Commute y l.prod
h : ∀ (x : M), x ∈ z :: l → Commute y x
⊢ Commute y (z :: l).prod

Tactic:
rw [List.forall_mem_cons] at h
    rw [List.prod_cons]
    exact Commute.mul_right h.1 (IH h.2)

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: case pos
α : Type u_1
inst✝ : CommGroupWithZero α
n : ℤ
a b : α
ha : ¬a = 0
hb : b = 0
⊢ zpow' (a * b) n = zpow' a n * zpow' b n

pp: case neg
α : Type u_1
inst✝ : CommGroupWithZero α
n : ℤ
a b : α
ha : ¬a = 0
hb : ¬b = 0
⊢ zpow' (a * b) n = zpow' a n * zpow' b n

Tactic:
· simp [hb]

Goal state after:
case neg
α : Type u_1
inst✝ : CommGroupWithZero α
n : ℤ
a b : α
ha : ¬a = 0
hb : ¬b = 0
⊢ zpow' (a * b) n = zpow' a n * zpow' b n
Module: Mathlib.Algebra.Order.Nonneg.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : AddMonoidWithOne α
inst✝² : PartialOrder α
inst✝¹ : AddLeftMono α
inst✝ : ZeroLEOneClass α
⊢ ↑0 = 0

Tactic:
by ext; simp

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

Goal state before:
pp: α : Type u_1
inst✝³ : AddMonoidWithOne α
inst✝² : PartialOrder α
inst✝¹ : AddLeftMono α
inst✝ : ZeroLEOneClass α
x✝ : ℕ
⊢ ↑(x✝ + 1) = ↑x✝ + 1

Tactic:
by ext; simp

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

Goal state before:
pp: α : Type u
p : α → Prop
x : α
l : List α
⊢ p x ∧ Forall p l ↔ p x ∧ ∀ (x : α), x ∈ l → p x

Tactic:
forall_iff_forall_mem

Goal state after:
α : Type u
p : α → Prop
x : α
l : List α
⊢ (p x ∧ ∀ (x : α), x ∈ l → p x) ↔ p x ∧ ∀ (x : α), x ∈ l → p x
Module: Mathlib.Algebra.Ring.Rat

Goal state before:
pp: q : ℚ
⊢ q * ↑q.den = ↑q.num

Tactic:
mul_den_eq_num

Goal state after:
q : ℚ
⊢ ↑q.num = ↑q.num
Module: Mathlib.Algebra.Order.Ring.Unbundled.Rat

Goal state before:
pp: a : ℤ
b : ℕ
hb : b ≠ 0
⊢ mkRat a b ≤ 0 ↔ a ≤ 0

Tactic:
by
  grind [mkRat_pos_iff]

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

Goal state before:
pp: ⊢ 0⁻¹ = 0

Tactic:
by ext; simp

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a x y : G
h : SemiconjBy a x y
n : ℕ
⊢ SemiconjBy a (x ^ Int.negSucc n) (y ^ Int.negSucc n)

Tactic:
simp only [zpow_negSucc, inv_right_iff]
    apply pow_right h

Goal state after:
Module: Mathlib.Data.NNRat.Defs

Goal state before:
pp: q : ℚ≥0
⊢ q * ↑q.den = ↑q.num

Tactic:
mul_den_eq_num

Goal state after:
q : ℚ≥0
⊢ ↑q.num = ↑q.num
Module: Mathlib.Algebra.GroupWithZero.Divisibility

Goal state before:
pp: α : Type u_1
inst✝¹ : MonoidWithZero α
inst✝ : IsLeftCancelMulZero α
a b c : α
ha : a ≠ 0
d : α
⊢ a * c = a * (b * d) ↔ c = b * d

Tactic:
mul_right_inj' ha

Goal state after:
α : Type u_1
inst✝¹ : MonoidWithZero α
inst✝ : IsLeftCancelMulZero α
a b c : α
ha : a ≠ 0
d : α
⊢ c = b * d ↔ c = b * d
Module: Mathlib.Algebra.Divisibility.Units

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
x y z : α
H : IsRelPrime x (y * z)
⊢ IsRelPrime x y

Tactic:
rw [isRelPrime_comm] at H ⊢
  exact H.of_mul_left_left

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

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
a : α
m n : ℕ
ha₀ : a ≠ 0
ha : ¬IsUnit a
h : a ^ n ∣ a ^ m
hmn : m < n
⊢ False

Tactic:
apply ha

Goal state after:
case mp
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
a : α
m n : ℕ
ha₀ : a ≠ 0
ha : ¬IsUnit a
h : a ^ n ∣ a ^ m
hmn : m < n
⊢ IsUnit a
Module: Mathlib.Tactic.CancelDenoms.Core

Goal state before:
pp: α : Type u_1
inst✝ : CommRing α
n1 n2 k e1 e2 t1 t2 : α
h1 : n1 * e1 = t1
h2 : n2 * e2 = t2
h3 : n1 * n2 = k
⊢ n2 * (n1 * e1 * e2) = t1 * t2

Tactic:
h1,

Goal state after:
α : Type u_1
inst✝ : CommRing α
n1 n2 k e1 e2 t1 t2 : α
h1 : n1 * e1 = t1
h2 : n2 * e2 = t2
h3 : n1 * n2 = k
⊢ n2 * (t1 * e2) = t1 * t2
Module: Mathlib.Tactic.CancelDenoms.Core

Goal state before:
pp: α : Type u_1
inst✝ : Field α
n1 n2 k e1 e2 t1 : α
h1 : n1 * e1 = t1
h2 : n2 / e2 = 1
h3 : n1 * n2 = k
⊢ n1 * e1 * 1 = t1

Tactic:
h1,

Goal state after:
α : Type u_1
inst✝ : Field α
n1 n2 k e1 e2 t1 : α
h1 : n1 * e1 = t1
h2 : n2 / e2 = 1
h3 : n1 * n2 = k
⊢ t1 * 1 = t1
Module: Mathlib.Algebra.Order.Ring.Canonical

Goal state before:
pp: R : Type u
inst✝⁵ : NonUnitalNonAssocSemiring R
inst✝⁴ : PartialOrder R
inst✝³ : CanonicallyOrderedAdd R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
a b c : R
h : AddLECancellable (a * c)
⊢ a * (b - c) = a * b - a * c

Tactic:
obtain (hbc | hcb) := total_of (· ≤ ·) b c

Goal state after:
case inl
R : Type u
inst✝⁵ : NonUnitalNonAssocSemiring R
inst✝⁴ : PartialOrder R
inst✝³ : CanonicallyOrderedAdd R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
a b c : R
h : AddLECancellable (a * c)
hbc : b ≤ c
⊢ a * (b - c) = a * b - a * c

case inr
R : Type u
inst✝⁵ : NonUnitalNonAssocSemiring R
inst✝⁴ : PartialOrder R
inst✝³ : CanonicallyOrderedAdd R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
a b c : R
h : AddLECancellable (a * c)
hcb : c ≤ b
⊢ a * (b - c) = a * b - a * c
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
s : Set α
h_sup : sSup s = ⊥
hne : s.Nonempty
⊢ s = {⊥}

Tactic:
Set.eq_singleton_iff_nonempty_unique_mem

Goal state after:
α : Type u_1
inst✝ : CompleteLattice α
s : Set α
h_sup : sSup s = ⊥
hne : s.Nonempty
⊢ s.Nonempty ∧ ∀ x ∈ s, x = ⊥
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
ι' : Sort u_5
inst✝ : SupSet α
f : ι → ι'
hf : Surjective f
g : ι' → α
⊢ (range fun x ↦ g (f x)) = range fun y ↦ g y

Tactic:
exact hf.range_comp g

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

Goal state before:
pp: β : Type u_2
ι : Sort u_5
inst✝ : Nonempty ι
x : β
t : ι → Set β
⊢ insert x (⋃ i, t i) = ⋃ i, insert x (t i)

Tactic:
← union_singleton,

Goal state after:
β : Type u_2
ι : Sort u_5
inst✝ : Nonempty ι
x : β
t : ι → Set β
⊢ (⋃ i, t i) ∪ {x} = ⋃ i, t i ∪ {x}
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: β : Type u_2
ι : Sort u_5
x : β
t : ι → Set β
⊢ insert x (⋂ i, t i) = ⋂ i, insert x (t i)

Tactic:
← union_singleton,

Goal state after:
β : Type u_2
ι : Sort u_5
x : β
t : ι → Set β
⊢ (⋂ i, t i) ∪ {x} = ⋂ i, t i ∪ {x}
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: β : Type u_2
ι : Sort u_5
inst✝ : Nonempty ι
s : Set β
t : ι → Set β
⊢ s \ ⋃ i, t i = ⋂ i, s \ t i

Tactic:
simp only [sdiff_eq, compl_iUnion, inter_iInter]

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

Goal state before:
pp: β : Type u_2
ι : Type u_12
x : ι → β
t : ι → Set β
⊢ ⋃ i, insert (x i) (t i) = range x ∪ ⋃ i, t i

Tactic:
← union_singleton,

Goal state after:
β : Type u_2
ι : Type u_12
x : ι → β
t : ι → Set β
⊢ ⋃ i, t i ∪ {x i} = range x ∪ ⋃ i, t i
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
inst✝ : Frame α
ι : Type u_1
ι' : Type u_2
f : ι → α
g : ι' → α
s : Set ι
t : Set ι'
⊢ ⨆ i, f ↑i.1 ⊓ g ↑i.2 = ⨆ x, f (↑x).1 ⊓ g (↑x).2

Tactic:
exact (Equiv.surjective _).iSup_congr (Equiv.Set.prod s t).symm fun x => rfl

Goal state after: