mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α : Sort u
β : Sort v
γ : Sort w
δ : Sort u_1
ab : α ≃ β
cd : γ ≃ δ
⊢ (ab.equivCongr cd).symm = ab.symm.equivCongr cd.symm

Tactic:
by ext; rfl

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

Goal state before:
pp: α : Sort u
β : Sort v
γ : Sort w
p : α → Prop
q : β → Prop
e x✝ : α ≃ β
⊢ (fun f ↦ ofBijective ↑f ⋯) ((fun f ↦ ⟨⇑f, ⋯⟩) x✝) = x✝

Tactic:
by ext; rfl

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✝⁴ : SMul M α
inst✝³ : SMul N α
inst✝² : SMul Nᵐᵒᵖ α
inst✝¹ : IsCentralScalar N α
inst✝ : SMulCommClass M N α
m : M
n : Nᵐᵒᵖ
a : α
⊢ m • n • a = n • m • a

Tactic:
← unop_smul_eq_smul n (m • a),

Goal state after:
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✝⁴ : SMul M α
inst✝³ : SMul N α
inst✝² : SMul Nᵐᵒᵖ α
inst✝¹ : IsCentralScalar N α
inst✝ : SMulCommClass M N α
m : M
n : Nᵐᵒᵖ
a : α
⊢ m • n • a = MulOpposite.unop n • m • a
Module: Mathlib.Data.Prod.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Nonempty α
inst✝ : Nonempty β
f : α → γ
g : β → δ
this✝ : Nonempty γ
this : Nonempty δ
⊢ Bijective (map f g) ↔ Bijective f ∧ Bijective g

Tactic:
exact (map_injective.and map_surjective).trans and_and_and_comm

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

Goal state before:
pp: a b c : ℕ
⊢ a / b / c = a / c / b

Tactic:
by
  rw [Nat.div_div_eq_div_mul, Nat.mul_comm, ← Nat.div_div_eq_div_mul]

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

Goal state before:
pp: case inr
n m : ℕ
h : n < m
⊢ n ∣ m - n ↔ n ∣ m ∨ m ≤ n

Tactic:
simp [dvd_sub_iff_left (le_of_lt h) (Nat.dvd_refl _), h.not_ge]

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

Goal state before:
pp: case inr
k : ℕ
hk : k > 0
⊢ 2 * k ^ 2 + 1 ≤ 2 ^ (2 * k)

Tactic:
have hk0 : 0 < 2 * k ^ 2 := Nat.mul_pos Nat.two_pos (Nat.pow_pos hk)

Goal state after:
case inr
k : ℕ
hk : k > 0
hk0 : 0 < 2 * k ^ 2
⊢ 2 * k ^ 2 + 1 ≤ 2 ^ (2 * k)
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: n : ℕ
⊢ n ^ n ≤ (n + 1) ^ (n + 1)

Tactic:
rw [Nat.pow_succ]

Goal state after:
n : ℕ
⊢ n ^ n ≤ (n + 1) ^ n * (n + 1)
Module: Mathlib.Order.GaloisConnection.Defs

Goal state before:
pp: case mpr
α : Type u
β : Type v
inst✝¹ : PartialOrder α
inst✝ : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
z : α
y : β
⊢ (∀ (x : α), x ≤ z ↔ l x ≤ y) → u y = z

Tactic:
· intro H
    exact ((H <| u y).mpr (gc.l_u_le y)).antisymm ((gc _ _).mp <| (H z).mp le_rfl)

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

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b : α
⊢ a ⊔ b ⇨ a = b ⇨ a

Tactic:
by
  rw [sup_himp_distrib, himp_self, top_inf_eq]

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

Goal state before:
pp: case none.none
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x : α
h1 : e.symm (some (e.removeNoneAux x)) = none
h2 : e (some x) = none
⊢ some (e.symm.removeNoneAux (e.removeNoneAux x)) = some x

Tactic:
rw [removeNoneAux_none _ h1]
        exact (e.eq_symm_apply.mpr h2).symm

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

Goal state before:
pp: α : Type u_1
t s₁ s₂ : Set α
h : s₂ ⊆ s₁
⊢ t.ite s₁ s₂ = s₁ ∩ t ∪ s₂

Tactic:
ext x
  by_cases hx : x ∈ t <;> simp [*, Set.ite, or_iff_left_of_imp (@h x)]

Goal state after:
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:
simp_rw [symmDiff_comm a]

Goal state after:
α : Type u_2
inst✝ : BooleanAlgebra α
a b c : α
h : Disjoint b c
⊢ a ≤ b ∆ a ⊔ c ∆ a
Module: Mathlib.Data.Set.Restrict

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
j : β → γ
hf : FactorsThrough g f
hg : Injective g
⊢ InjOn (extend f g j) (range f)

Tactic:
rintro _ ⟨x, rfl⟩ _ ⟨y, rfl⟩ heq

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
j : β → γ
hf : FactorsThrough g f
hg : Injective g
x y : α
heq : extend f g j (f x) = extend f g j (f y)
⊢ f x = f y
Module: Mathlib.Data.Set.Restrict

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : MapsTo f s t
h' : SurjOn f s t
x✝ : ↑t
b : β
hb : b ∈ t
⊢ ∃ a, restrict f s t h a = ⟨b, hb⟩

Tactic:
obtain ⟨a, ha, rfl⟩ := h' hb
    exact ⟨⟨a, ha⟩, rfl⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
s : Set α
⊢ f '' sᶜ = range f \ f '' s

Tactic:
rw [← image_univ, ← image_sdiff hf, compl_eq_univ_sdiff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s t : Set β
h : Codisjoint s t
⊢ Codisjoint (f ⁻¹' s) (f ⁻¹' t)

Tactic:
by
  simp only [codisjoint_iff_le_sup, Set.sup_eq_union, top_le_iff, ← Set.preimage_union] at h ⊢
  rw [h]; rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s s₁ s₂ : Set α
f : α → β
h : InjOn f s
h₁ : s₁ ⊆ s
h₂ : s₂ ⊆ s
⊢ f '' s₁ ⊂ f '' s₂ ↔ s₁ ⊂ s₂

Tactic:
simp_rw [ssubset_def, h.image_subset_image_iff h₁ h₂, h.image_subset_image_iff h₂ h₁]

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

Goal state before:
pp: case negSucc
motive : ℤ → Prop
zero : motive 0
succ : ∀ (i : ℕ), motive ↑i → motive (↑i + 1)
pred : ∀ (i : ℕ), motive (-↑i) → motive (-↑i - 1)
i n : ℕ
⊢ motive (-↑n)

Tactic:
induction n with
    | zero => simp [zero]
    | succ n ih => simpa [natCast_succ, Int.neg_add, Int.sub_eq_add_neg] using pred _ ih

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

Goal state before:
pp: case mp.inr
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
ht : t.Nonempty
h : SurjOn f s t
this : Nonempty α
⊢ ∃ s', s' ⊆ s ∧ BijOn f s' t

Tactic:
exact ⟨_, h.mapsTo_invFunOn.image_subset, h.bijOn_subset⟩

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

Goal state before:
pp: i : ℤ
h : 0 < i
⊢ ↑(i.toNat - 1) = i - 1

Tactic:
by
  simp only [lt_toNat, Int.cast_ofNat_Int, h, natCast_pred_of_pos, Int.le_of_lt h, toNat_of_nonneg]

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a b c : α
⊢ a / (b * c) = a / c / b

Tactic:
by
  simp only [mul_assoc, mul_inv_rev, div_eq_mul_inv]

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

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

Tactic:
← div_eq_mul_inv,

Goal state after:
G : Type u_3
inst✝ : CommGroup G
a b : G
⊢ a * (b / a) = b
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: G : Type u_3
inst✝ : CommGroup G
a b c : G
⊢ c / a / (c / b) = b / a

Tactic:
← inv_div b c,

Goal state after:
G : Type u_3
inst✝ : CommGroup G
a b c : G
⊢ c / a / (b / c)⁻¹ = b / a
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: G : Type u_3
inst✝ : CommGroup G
a b c d : G
⊢ a * b⁻¹ = c * d⁻¹ ↔ a * d = c * b

Tactic:
← div_eq_mul_inv,

Goal state after:
G : Type u_3
inst✝ : CommGroup G
a b c d : G
⊢ a / b = c * d⁻¹ ↔ a * d = c * b
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: G : Type u_3
inst✝ : CommGroup G
a b c d : G
⊢ a / b = c * d⁻¹ ↔ a * d = c * b

Tactic:
← div_eq_mul_inv,

Goal state after:
G : Type u_3
inst✝ : CommGroup G
a b c d : G
⊢ a / b = c / d ↔ a * d = c * b
Module: Mathlib.Algebra.Group.Units.Hom

Goal state before:
pp: M : Type u
inst✝ : Monoid M
⊢ map (MonoidHom.id M) = MonoidHom.id Mˣ

Tactic:
by ext; rfl

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

Goal state before:
pp: α : Type u
inst✝ : DivisionCommMonoid α
a b c d : α
hb : IsUnit b
hd : IsUnit d
⊢ a * b⁻¹ = c * d⁻¹ ↔ a * d = c * b

Tactic:
← div_eq_mul_inv,

Goal state after:
α : Type u
inst✝ : DivisionCommMonoid α
a b c d : α
hb : IsUnit b
hd : IsUnit d
⊢ a / b = c * d⁻¹ ↔ a * d = c * b
Module: Mathlib.Algebra.Group.Units.Basic

Goal state before:
pp: α : Type u
inst✝ : DivisionCommMonoid α
a b c d : α
hb : IsUnit b
hd : IsUnit d
⊢ a / b = c * d⁻¹ ↔ a * d = c * b

Tactic:
← div_eq_mul_inv,

Goal state after:
α : Type u
inst✝ : DivisionCommMonoid α
a b c d : α
hb : IsUnit b
hd : IsUnit d
⊢ a / b = c / d ↔ a * d = c * b
Module: Mathlib.Algebra.NeZero

Goal state before:
pp: R : Type u_1
inst✝ : Zero R
n : R
⊢ ¬NeZero n ↔ n = 0

Tactic:
by simp [neZero_iff]

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

Goal state before:
pp: α : Type u_3
inst✝ : MonoidWithZero α
h : ∀ (a : α), a ≠ 0 → ∃ b, b * a = 1
a : α
ha : a ≠ 0
h✝ : Nontrivial α
b : α
hb : b * a = 1
c : α
hc : c * b = 1
| a * b

Tactic:
← one_mul (a * b),

Goal state after:
α : Type u_3
inst✝ : MonoidWithZero α
h : ∀ (a : α), a ≠ 0 → ∃ b, b * a = 1
a : α
ha : a ≠ 0
h✝ : Nontrivial α
b : α
hb : b * a = 1
c : α
hc : c * b = 1
| 1 * (a * b)
Module: Mathlib.Algebra.Group.End

Goal state before:
pp: A : Type u_1
M : Type u_2
G : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝² : Mul M
inst✝¹ : Group G
H : Type u_7
inst✝ : Group H
ϕ : G ≃* H
x✝ : MulAut G
⊢ (fun f ↦ ϕ.trans (MulEquiv.trans f ϕ.symm)) ((fun f ↦ ϕ.symm.trans (MulEquiv.trans f ϕ)) x✝) = x✝

Tactic:
by simp [DFunLike.ext_iff]

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

Goal state before:
pp: A : Type u_1
M : Type u_2
G : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝² : Mul M
inst✝¹ : Group G
H : Type u_7
inst✝ : Group H
ϕ : G ≃* H
x✝ : MulAut H
⊢ (fun f ↦ ϕ.symm.trans (MulEquiv.trans f ϕ)) ((fun f ↦ ϕ.trans (MulEquiv.trans f ϕ.symm)) x✝) = x✝

Tactic:
by simp [DFunLike.ext_iff]

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

Goal state before:
pp: A : Type u_1
M : Type u_2
G : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝² : Mul M
inst✝¹ : Group G
H : Type u_7
inst✝ : Group H
ϕ : G ≃* H
⊢ ∀ (x y : MulAut G),
    ϕ.symm.trans (MulEquiv.trans (x * y) ϕ) = ϕ.symm.trans (MulEquiv.trans x ϕ) * ϕ.symm.trans (MulEquiv.trans y ϕ)

Tactic:
by simp [DFunLike.ext_iff]

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

Goal state before:
pp: M : Type u_1
M₀ : Type u_2
M₀' : Type u_3
G₀ : Type u_4
G₀' : Type u_5
N : Type u_6
A : Type u_7
A' : Type u_8
B : Type u_9
α : Type u_10
β : Type u_11
inst✝³ : AddZeroClass A
inst✝² : DistribSMul M A
inst✝¹ : AddZeroClass B
inst✝ : SMul M B
f : B →+ A
hf : Injective ⇑f
smul : ∀ (c : M) (x : B), f (c • x) = c • f x
c : M
x y : B
⊢ f (c • (x + y)) = f (c • x + c • y)

Tactic:
simp only [smul, map_add, smul_add]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : AddMonoidWithOne M
inst✝ : CharZero M
⊢ 1 ≠ 0

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

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : AddMonoidWithOne M
inst✝ : CharZero M
⊢ 1 ≠ 0
Module: Mathlib.Algebra.Module.Defs

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
x : M
⊢ -r • -x = r • x

Tactic:
neg_smul,

Goal state after:
R : Type u_1
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
x : M
⊢ -(r • -x) = r • x
Module: Mathlib.Algebra.Divisibility.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
m n : ℕ
a : α
h : m ≤ n
⊢ a ^ n = a ^ m * a ^ (n - m)

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

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

Goal state before:
pp: R : Type u_1
inst✝¹ : DivisionMonoid R
inst✝ : HasDistribNeg R
a b : R
⊢ -a / -b = a / b

Tactic:
by rw [div_neg_eq_neg_div, neg_div, neg_neg]

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

Goal state before:
pp: M : Type u_1
inst✝ : DivisionMonoid M
a b c d : M
hbd : Commute b d
hb : IsUnit b
hd : IsUnit d
⊢ a * b⁻¹ = c * d⁻¹ ↔ a * d = c * b

Tactic:
← div_eq_mul_inv,

Goal state after:
M : Type u_1
inst✝ : DivisionMonoid M
a b c d : M
hbd : Commute b d
hb : IsUnit b
hd : IsUnit d
⊢ a / b = c * d⁻¹ ↔ a * d = c * b
Module: Mathlib.Algebra.Group.Commute.Units

Goal state before:
pp: M : Type u_1
inst✝ : DivisionMonoid M
a b c d : M
hbd : Commute b d
hb : IsUnit b
hd : IsUnit d
⊢ a / b = c * d⁻¹ ↔ a * d = c * b

Tactic:
← div_eq_mul_inv,

Goal state after:
M : Type u_1
inst✝ : DivisionMonoid M
a b c d : M
hbd : Commute b d
hb : IsUnit b
hd : IsUnit d
⊢ a / b = c / d ↔ a * d = c * b
Module: Mathlib.Algebra.Ring.InjSurj

Goal state before:
pp: R : Type u_1
S : Type u_2
f✝ : S → R
hf✝ : Injective 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
f : S → R
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
nsmul : ∀ (n : ℕ) (x : S), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f ↑n = ↑n
⊢ f ↑0 = f 0

Tactic:
by rw [natCast, Nat.cast_zero, zero]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
z : ℕ
a : M
⊢ ↑z.succ • a = ↑z • a + a

Tactic:
simp_rw [HSMul.hSMul, SMul.smul]

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
z : ℕ
a : M
⊢ ↑↑z.succ • a = ↑↑z • a + a
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_4
inst✝ : Semiring α
⊢ (Set.range fun x ↦ 2 * x + 1) = {a | Odd a}

Tactic:
ext x; simp [Odd, eq_comm]

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
⊢ a ^ (2 * (k + 1) + 1) + b ^ (2 * (k + 1) + 1) + b ^ (2 * k + 1) * a ^ 2 =
    (a ^ (2 * k + 1) + b ^ (2 * k + 1)) * a ^ 2 + b ^ (2 * k + 3)

Tactic:
rw [add_mul, ← pow_add, add_right_comm]

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
⊢ a ^ (2 * (k + 1) + 1) + b ^ (2 * k + 1) * a ^ 2 + b ^ (2 * (k + 1) + 1) =
    a ^ (2 * k + 1 + 2) + b ^ (2 * k + 1) * a ^ 2 + b ^ (2 * k + 3)
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝¹ : Monoid α
inst✝ : HasDistribNeg α
c : ℕ
a : α
⊢ (-a) ^ (2 * c + 1) = -a ^ (2 * c + 1)

Tactic:
simp_rw [pow_add, pow_mul, neg_sq, pow_one, mul_neg]

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

Goal state before:
pp: α : Type u_1
inst✝² : MulZeroClass α
a b : α
inst✝¹ : Preorder α
inst✝ : PosMulStrictMono α
ha : 0 < a
hb : 0 < b
⊢ 0 < a * b

Tactic:
by
  simpa only [mul_zero] using mul_lt_mul_of_pos_left hb ha

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

Goal state before:
pp: α : Type u_1
inst✝² : MulZeroClass α
a b : α
inst✝¹ : Preorder α
inst✝ : PosMulStrictMono α
ha : 0 < a
hb : b < 0
⊢ a * b < 0

Tactic:
by
  simpa only [mul_zero] using mul_lt_mul_of_pos_left hb ha

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

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝³ : MulZeroClass α
a b : α
inst✝² : LinearOrder α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
hab : 0 < a * b
ha : 0 < a
⊢ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0

Tactic:
refine Or.inl ⟨ha, lt_imp_lt_of_le_imp_le (fun hb => ?_) hab⟩
    exact mul_nonpos_of_nonneg_of_nonpos ha.le hb

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

Goal state before:
pp: α : Sort ?u.9
β : Type ?u.24
x✝ : α ≃ β
⊢ (fun f ↦ (↑f).equivOfSurjective ⋯) ((fun f ↦ ⟨f.toEmbedding, ⋯⟩) x✝) = x✝

Tactic:
by ext; rfl

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₀
a b : G₀
ha : 0 < a
⊢ 1 ≤ a⁻¹ * b ↔ a ≤ b

Tactic:
le_inv_mul_iff₀ ha,

Goal state after:
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b : G₀
ha : 0 < a
⊢ a * 1 ≤ b ↔ a ≤ b
Module: Mathlib.Logic.Embedding.Basic

Goal state before:
pp: α₁ : Sort u
α₂ : Sort v
α₃ : Sort x
γ : Sort w
inst✝ : Inhabited γ
e₁₂ : α₁ ↪ α₂
e₂₃ : α₂ ↪ α₃
⊢ e₁₂.arrowCongrLeft.trans e₂₃.arrowCongrLeft = (e₁₂.trans e₂₃).arrowCongrLeft

Tactic:
ext f a

Goal state after:
α₁ : Sort u
α₂ : Sort v
α₃ : Sort x
γ : Sort w
inst✝ : Inhabited γ
e₁₂ : α₁ ↪ α₂
e₂₃ : α₂ ↪ α₃
f : α₁ → γ
a : α₃
⊢ (e₁₂.arrowCongrLeft.trans e₂₃.arrowCongrLeft) f a = (e₁₂.trans e₂₃).arrowCongrLeft f a
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝³ : Semiring R
inst✝² : LinearOrder R
a b : R
inst✝¹ : MulPosStrictMono R
inst✝ : PosMulStrictMono R
hab : 0 ≤ a * b
⊢ ¬(¬(0 ≤ a ∧ 0 ≤ b) ∧ ¬(a ≤ 0 ∧ b ≤ 0))

Tactic:
simp only [not_and, not_le]

Goal state after:
R : Type u
inst✝³ : Semiring R
inst✝² : LinearOrder R
a b : R
inst✝¹ : MulPosStrictMono R
inst✝ : PosMulStrictMono R
hab : 0 ≤ a * b
⊢ (0 ≤ a → b < 0) → ¬(a ≤ 0 → 0 < b)
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_lt_inv₀ hb (inv_pos.2 ha), inv_inv]

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

Goal state before:
pp: case mpr
α : Type u_1
x✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
⊢ WellFounded r → WellFounded (Quotient.lift₂ r H)

Tactic:
refine fun wf => ⟨fun q => ?_⟩

Goal state after:
case mpr
α : Type u_1
x✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
wf : WellFounded r
q : Quotient x✝
⊢ Acc (Quotient.lift₂ r H) q
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
x✝ : r ≃r s
⊢ (fun f ↦ ofSurjective ↑f ⋯) ((fun f ↦ ⟨f.toRelEmbedding, ⋯⟩) x✝) = x✝

Tactic:
by ext; rfl

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✝³ : LE α
inst✝² : LE β
inst✝¹ : LE γ
inst✝ : LE δ
x✝ : α ≃o β
⊢ (fun f ↦ ofSurjective ↑f ⋯) ((fun f ↦ ⟨RelIso.toRelEmbedding f, ⋯⟩) x✝) = x✝

Tactic:
by ext; rfl

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

Goal state before:
pp: M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulRightMono M
inst✝ : MulLeftMono M
a b : M
hab : a ^ 2 ≤ b * a
n : ℕ
x✝ : n + 2 ≠ 0
⊢ a ^ (n + 1) * a ≤ b ^ n * a * a

Tactic:
by grw [pow_le_pow_mul_of_sq_le_mul hab (by lia)]; simp

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

Goal state before:
pp: G : Type u_2
inst✝² : DivInvMonoid G
inst✝¹ : Preorder G
inst✝ : MulLeftMono G
x : G
H : 1 ≤ x
n : ℤ
hn : 0 ≤ n
⊢ 1 ≤ x ^ n

Tactic:
lift n to ℕ using hn
  rw [zpow_natCast]
  apply one_le_pow_of_one_le' H

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

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoidWithOne R
h : NeZero ↑0
⊢ False

Tactic:
exact h.out Nat.cast_zero

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

Goal state before:
pp: n : ℤ
⊢ ∃ k, n = 2 * k ∨ n = 2 * k + 1

Tactic:
by
  simpa only [two_mul, exists_or, Odd, Even] using even_or_odd n

Goal state after:
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: s : ℕ
⊢ gcdB 0 s = 1

Tactic:
gcdB,

Goal state after:
s : ℕ
⊢ (xgcd 0 s).2 = 1
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: case left
M : Type u_1
inst✝ : Monoid M
a : M
m n : ℕ
hmn : a ^ m.gcd n = 1
⊢ a ^ m = 1

Tactic:
rw [← Nat.mul_div_cancel' (m.gcd_dvd_left n), pow_mul, hmn, one_pow]

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

Goal state before:
pp: case inr
G : Type u_1
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a✝ b c a : α
ha : a ≠ ⊤
⊢ - -a = a

Tactic:
· apply left_neg_eq_right_neg (a := -a) <;> simp [add_comm, add_neg_cancel_of_ne_top, ha]

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

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

Tactic:
by
  refine ((tsub_le_tsub_iff_right h).mp h2.le).lt_of_ne ?_
  rintro rfl
  exact h2.false

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

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

Tactic:
ha.le_tsub_iff_left h₁,

Goal state after:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
ha : AddLECancellable a
hc : AddLECancellable c
h₁ : a ≤ b
h₂ : c ≤ b
⊢ a ≤ b - c ↔ a + c ≤ b
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
β : Type v
inst✝ : AddMonoid α
a : WithTop α
⊢ 0 • a = 0

Tactic:
simp_rw [HSMul.hSMul, SMul.smul]

Goal state after:
α : Type u
β : Type v
inst✝ : AddMonoid α
a : WithTop α
⊢ (match a, 0 with
    | Option.some a, n => ↑(n • a)
    | none, 0 => 0
    | none, _n.succ => ⊤) =
    0
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
β : Type v
inst✝ : AddMonoid α
n : ℕ
a : WithTop α
⊢ (n + 1) • a = n • a + a

Tactic:
simp_rw [HSMul.hSMul, SMul.smul]

Goal state after:
α : Type u
β : Type v
inst✝ : AddMonoid α
n : ℕ
a : WithTop α
⊢ (match a, n + 1 with
    | Option.some a, n => ↑(n • a)
    | none, 0 => 0
    | none, _n.succ => ⊤) =
    (match a, n with
      | Option.some a, n => ↑(n • a)
      | none, 0 => 0
      | none, _n.succ => ⊤) +
      a
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
β : Type v
inst✝² : LE α
inst✝¹ : Add α
inst✝ : ExistsAddOfLE α
a✝ b✝ : WithTop α
a b : α
h : ↑a ≤ ↑b
⊢ ∃ c, ↑b = ↑a + c

Tactic:
by
      obtain ⟨c, rfl⟩ := exists_add_of_le (WithTop.coe_le_coe.1 h)
      exact ⟨c, rfl⟩

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

Goal state before:
pp: case some.none
α : Type u
inst✝¹ : Add α
a : α
inst✝ : LE α
ha : AddLECancellable a
b : α
⊢ ↑a + Option.some b ≤ ↑a + none → Option.some b ≤ none

pp: case some.some
α : Type u
inst✝¹ : Add α
a : α
inst✝ : LE α
ha : AddLECancellable a
b c : α
⊢ ↑a + Option.some b ≤ ↑a + Option.some c → Option.some b ≤ Option.some c

Tactic:
· simp [some_eq_coe, ← coe_add, none_eq_bot]

Goal state after:
case some.some
α : Type u
inst✝¹ : Add α
a : α
inst✝ : LE α
ha : AddLECancellable a
b c : α
⊢ ↑a + Option.some b ≤ ↑a + Option.some c → Option.some b ≤ Option.some c
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot
α : Type u_1
b : α
h : ⊥ ≠ ⊥
⊢ ⊥.unbot h = b ↔ ⊥ = ↑b

pp: case coe
α : Type u_1
b a✝ : α
h : ↑a✝ ≠ ⊥
⊢ (↑a✝).unbot h = b ↔ ↑a✝ = ↑b

Tactic:
· simpa using h rfl

Goal state after:
case coe
α : Type u_1
b a✝ : α
h : ↑a✝ ≠ ⊥
⊢ (↑a✝).unbot h = b ↔ ↑a✝ = ↑b
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot
α : Type u_1
a : α
h : ⊥ ≠ ⊥
⊢ a = ⊥.unbot h ↔ ↑a = ⊥

pp: case coe
α : Type u_1
a a✝ : α
h : ↑a✝ ≠ ⊥
⊢ a = (↑a✝).unbot h ↔ ↑a = ↑a✝

Tactic:
· simpa using h rfl

Goal state after:
case coe
α : Type u_1
a a✝ : α
h : ↑a✝ ≠ ⊥
⊢ a = (↑a✝).unbot h ↔ ↑a = ↑a✝
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : LinearOrderedCommMonoidWithZero α
a✝ b✝ : α
n : ℕ
a b : α
hab : a ≤ b
c : α
⊢ a * c ≤ b * c

Tactic:
by
    obtain rfl | hc := eq_or_ne c 0
    · simp
    obtain rfl | hab := hab.eq_or_lt
    · simp
    · exact (mul_lt_mul_of_pos_right hab hc.pos).le

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

Goal state before:
pp: G : Type u_3
inst✝¹ : Preorder G
inst✝ : AddGroup G
x y : WithZero (Multiplicative G)
hx : x ≠ 0
hy : y ≠ 0
⊢ x ≤ exp y.log ↔ x ≤ y

Tactic:
exp_log hy

Goal state after:
G : Type u_3
inst✝¹ : Preorder G
inst✝ : AddGroup G
x y : WithZero (Multiplicative G)
hx : x ≠ 0
hy : y ≠ 0
⊢ x ≤ y ↔ x ≤ y