mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: case map_sup
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : GeneralizedBooleanAlgebra β
bot : Bot α := e.bot
sdiff : SDiff α := e.sdiff
distribLattice : DistribLattice α := e.distribLattice
a✝ b✝ : α
⊢ e (a✝ ⊔ b✝) = e a✝ ⊔ e b✝

Tactic:
exact e.apply_symm_apply _

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

Goal state before:
pp: case map_inf
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : GeneralizedBooleanAlgebra β
bot : Bot α := e.bot
sdiff : SDiff α := e.sdiff
distribLattice : DistribLattice α := e.distribLattice
a✝ b✝ : α
⊢ e (a✝ ⊓ b✝) = e a✝ ⊓ e b✝

Tactic:
exact e.apply_symm_apply _

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

Goal state before:
pp: case map_bot
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : GeneralizedBooleanAlgebra β
bot : Bot α := ⋯
sdiff : SDiff α := ⋯
distribLattice : DistribLattice α := ⋯
⊢ e ⊥ = ⊥

Tactic:
exact e.apply_symm_apply _

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

Goal state before:
pp: case map_sdiff
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : GeneralizedBooleanAlgebra β
bot : Bot α := e.bot
sdiff : SDiff α := e.sdiff
distribLattice : DistribLattice α := e.distribLattice
a✝ b✝ : α
⊢ e (a✝ \ b✝) = e a✝ \ e b✝

Tactic:
exact e.apply_symm_apply _

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

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

Tactic:
rw [swap_apply_of_ne_of_ne ne (ne_of_mem_of_not_mem ha hj)]

Goal state after:
case mp.inr
α : Type u_9
inst✝ : DecidableEq α
s : Set α
i j : α
hi : i ∈ s
hj : ¬j ∈ s
a : α
ha : a ∈ s
ne : a ≠ i
⊢ a ∈ insert j s \ {i}
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: case map_sup
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : BooleanAlgebra β
top : Top α := e.top
compl : Compl α := e.compl
himp : HImp α := e.himp
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := e.generalizedBooleanAlgebra
a✝ b✝ : α
⊢ e (a✝ ⊔ b✝) = e a✝ ⊔ e b✝

Tactic:
exact e.apply_symm_apply _

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

Goal state before:
pp: case map_inf
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : BooleanAlgebra β
top : Top α := e.top
compl : Compl α := e.compl
himp : HImp α := e.himp
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := e.generalizedBooleanAlgebra
a✝ b✝ : α
⊢ e (a✝ ⊓ b✝) = e a✝ ⊓ e b✝

Tactic:
exact e.apply_symm_apply _

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

Goal state before:
pp: case map_top
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : BooleanAlgebra β
top : Top α := ⋯
compl : Compl α := ⋯
himp : HImp α := ⋯
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := ⋯
⊢ e ⊤ = ⊤

Tactic:
exact e.apply_symm_apply _

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

Goal state before:
pp: case map_bot
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : BooleanAlgebra β
top : Top α := ⋯
compl : Compl α := ⋯
himp : HImp α := ⋯
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := ⋯
⊢ e ⊥ = ⊥

Tactic:
exact e.apply_symm_apply _

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

Goal state before:
pp: case map_compl
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : BooleanAlgebra β
top : Top α := e.top
compl : Compl α := e.compl
himp : HImp α := e.himp
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := e.generalizedBooleanAlgebra
a✝ : α
⊢ e a✝ᶜ = (e a✝)ᶜ

Tactic:
exact e.apply_symm_apply _

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

Goal state before:
pp: case map_sdiff
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : BooleanAlgebra β
top : Top α := e.top
compl : Compl α := e.compl
himp : HImp α := e.himp
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := e.generalizedBooleanAlgebra
a✝ b✝ : α
⊢ e (a✝ \ b✝) = e a✝ \ e b✝

Tactic:
exact e.apply_symm_apply _

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

Goal state before:
pp: case map_himp
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : BooleanAlgebra β
top : Top α := e.top
compl : Compl α := e.compl
himp : HImp α := e.himp
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := e.generalizedBooleanAlgebra
a✝ b✝ : α
⊢ e (a✝ ⇨ b✝) = e a✝ ⇨ e b✝

Tactic:
exact e.apply_symm_apply _

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

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
f : α → β
s s' : Set β
r : range f ∩ s ⊆ range f ∩ s'
x : α
⊢ x ∈ f ⁻¹' s → x ∈ f ⁻¹' s'

Tactic:
hx

Goal state after:
case mp
α : Type u_1
β : Type u_2
f : α → β
s s' : Set β
r : range f ∩ s ⊆ range f ∩ s'
x : α
hx : x ∈ f ⁻¹' s
⊢ x ∈ f ⁻¹' s'
Module: Mathlib.Data.Set.Image

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
f : α → β
s s' : Set β
r : f ⁻¹' s ⊆ f ⁻¹' s'
x : β
⊢ x ∈ range f ∩ s → x ∈ range f ∩ s'

Tactic:
hx

Goal state after:
case mpr
α : Type u_1
β : Type u_2
f : α → β
s s' : Set β
r : f ⁻¹' s ⊆ f ⁻¹' s'
x : β
hx : x ∈ range f ∩ s
⊢ x ∈ range f ∩ s'
Module: Mathlib.Data.Set.Image

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
h : f ⁻¹' s ⊆ f ⁻¹' t
x : α
⊢ x ∈ s → x ∈ t

Tactic:
hx

Goal state after:
case mp
α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
h : f ⁻¹' s ⊆ f ⁻¹' t
x : α
hx : x ∈ s
⊢ x ∈ t
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : s.Nonempty ∧ t.Nonempty
heq : s ×ˢ t = s₁ ×ˢ t₁
h₁ : s₁.Nonempty ∧ t₁.Nonempty
⊢ s = s₁ ∧ t = t₁

Tactic:
rw [← fst_image_prod s h.2, ← fst_image_prod s₁ h₁.2, heq, eq_self_iff_true, true_and, ←
      snd_image_prod h.1 t, ← snd_image_prod h₁.1 t₁, heq]

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

Goal state before:
pp: case mpr
α : Type u_1
s t u : Set α
⊢ s ∩ t ⊆ s ∩ u → val ⁻¹' t ⊆ val ⁻¹' u

Tactic:
intro h x a
    exact (h ⟨x.2, a⟩).2

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
h : Injective (image f)
x x' : α
hx : f x = f x'
⊢ {f x} = {f x'}

Tactic:
hx

Goal state after:
α : Type u
β : Type v
f : α → β
h : Injective (image f)
x x' : α
hx : f x = f x'
⊢ {f x'} = {f x'}
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:
hx

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 : α
hx : x ∈ s₁
⊢ ∀ (y : α), y ∈ s₂ → f x ≠ f y
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
a : α
b : β
⊢ BijOn f {a} {b} ↔ f a = b

Tactic:
by simp [BijOn, eq_comm]

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:
hx

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 : α
hx : x ∈ s
⊢ ¬f x = f a
Module: Mathlib.Algebra.Group.Torsion

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

Tactic:
one_zpow

Goal state after:
G : Type u_2
inst✝¹ : Group G
inst✝ : IsMulTorsionFree G
n : ℤ
a : G
hn : n ≠ 0
⊢ a ^ n = 1 ↔ a ^ n = 1
Module: Mathlib.Data.Int.Init

Goal state before:
pp: a b c : ℤ
hbc : c ∣ b
⊢ a ∣ b / c ↔ c * a ∣ b

Tactic:
simp [hbc]

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

Goal state before:
pp: case refine_3
α : 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'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
x : α
hxs : x ∈ s
y : α
hyr : y ∈ r
hxy : f x = f y
⊢ y ∈ f ⁻¹' t

Tactic:
rw [← h.image_eq]

Goal state after:
case refine_3
α : 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'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
x : α
hxs : x ∈ s
y : α
hyr : y ∈ r
hxy : f x = f y
⊢ y ∈ f ⁻¹' f '' s
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)
x : α
⊢ x ∈ f ⁻¹' s → ∀ ⦃x₂ : α⦄, x₂ ∈ f ⁻¹' s → fa x = fa x₂ → x = x₂

Tactic:
hx

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 : α
hx : x ∈ f ⁻¹' s
⊢ ∀ ⦃x₂ : α⦄, x₂ ∈ f ⁻¹' s → fa x = fa x₂ → x = x₂
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
s : Set α
t : Set β
h : ∀ (a : α), e a ∈ t ↔ a ∈ s
b : β
hb : b ∈ t
⊢ e (e.symm b) ∈ t

Tactic:
apply_symm_apply

Goal state after:
α : Type u_1
β : Type u_2
e : α ≃ β
s : Set α
t : Set β
h : ∀ (a : α), e a ∈ t ↔ a ∈ s
b : β
hb : b ∈ t
⊢ b ∈ t
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
a : M
n m : ℕ
ha : a ^ n = 1
⊢ a ^ (m % n + n * (m / n)) = a ^ (m % n)

Tactic:
by simp [pow_add, pow_mul, ha]

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 : Injective 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 : M₁
⊢ f (x ^ 0) = f 1

Tactic:
by rw [zpow, zpow_zero, one]

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a : G
n : ℕ
⊢ a ^ (Int.negSucc (n + 1) + 1) = a ^ Int.negSucc (n + 1) * a

Tactic:
rw [zpow_negSucc, pow_succ', mul_inv_rev, inv_mul_cancel_right]

Goal state after:
G : Type u_3
inst✝ : Group G
a : G
n : ℕ
⊢ a ^ (Int.negSucc (n + 1) + 1) = (a ^ (n + 1))⁻¹
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✝¹ : Semigroup M
inst✝ : Semigroup N
x✝² x✝¹ x✝ : M × N
⊢ x✝² * x✝¹ * x✝ = x✝² * (x✝¹ * x✝)

Tactic:
by ext <;> exact mul_assoc ..

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

Goal state before:
pp: M₀ : Type u_1
inst✝ : MonoidWithZero M₀
a : M₀
n✝ m✝ : ℕ
hmn : n✝.le m✝
ha : a ^ n✝ = 0
⊢ a ^ m✝.succ = 0

Tactic:
rw [pow_succ, pow_eq_zero_of_le hmn ha, zero_mul]

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

Goal state before:
pp: case inr
M₀✝ : Type u_1
G₀ : Type u_2
a b c : M₀✝
inst✝² : MulZeroOneClass M₀✝
M₀ : Type u_3
inst✝¹ : MonoidWithZero M₀
inst✝ : IsLeftCancelMulZero M₀
a✝ b✝ : M₀
h : a✝ * b✝ = 1
h✝ : Nontrivial M₀
⊢ b✝ * a✝ = 1

Tactic:
exact (IsLeftCancelMulZero.mul_left_cancel_of_ne_zero
      (left_ne_zero_of_mul_eq_one h)).mul_eq_one_symm h

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
M₀ : Type u_6
inst✝⁴ : MulZeroOneClass α
inst✝³ : MulZeroOneClass β
inst✝² : MulZeroOneClass γ
inst✝¹ : MulZeroOneClass δ
inst✝ : FunLike F α β
hnp : β →*₀ γ
hmn : α →*₀ β
⊢ hnp 0 = 0

Tactic:
map_zero

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
M₀ : Type u_6
inst✝⁴ : MulZeroOneClass α
inst✝³ : MulZeroOneClass β
inst✝² : MulZeroOneClass γ
inst✝¹ : MulZeroOneClass δ
inst✝ : FunLike F α β
hnp : β →*₀ γ
hmn : α →*₀ β
⊢ 0 = 0
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: case neg
G₀ : Type u_2
inst✝ : GroupWithZero G₀
n : ℤ
h : ¬n = 0
⊢ 0 ^ n = 0

Tactic:
zero_zpow _ h

Goal state after:
case neg
G₀ : Type u_2
inst✝ : GroupWithZero G₀
n : ℤ
h : ¬n = 0
⊢ 0 = 0
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
n : ℤ
⊢ a ^ (n - 1) = a ^ (n - 1) * a * a⁻¹

Tactic:
by rw [mul_assoc, mul_inv_cancel₀ ha, mul_one]

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

Goal state before:
pp: R : Type u
inst✝ : AddGroupWithOne R
n : ℕ
⊢ ↑(-↑(n + 1)) = -↑↑(n + 1)

Tactic:
by rw [cast_natCast, neg_ofNat_succ]; simp

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

Goal state before:
pp: α : Type u
R : Type v
inst✝ : NonUnitalNonAssocRing α
a b : α
⊢ a * -b + a * b = 0

Tactic:
by rw [← left_distrib, neg_add_cancel, mul_zero]

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

Goal state before:
pp: α : Type u_3
inst✝ : Semiring α
t : IsCancelMulZero α
⊢ Nontrivial α → IsDomain α

Tactic:
(Tactic.exact
 "exact"
 (Term.fun
  "fun"
  (Term.basicFun
   [(Term.hole "_")]
   []
   "↦"
   (choice («term{}» "{" "}") (Term.structInst "{" [] (Term.structInstFields []) (Term.optEllipsis []) [] "}")))))

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

Goal state before:
pp: R : Type u_1
inst✝¹ : DivisionMonoid R
inst✝ : HasDistribNeg R
⊢ (-1)⁻¹ = -1

Tactic:
← neg_inv,

Goal state after:
R : Type u_1
inst✝¹ : DivisionMonoid R
inst✝ : HasDistribNeg R
⊢ -1⁻¹ = -1
Module: Mathlib.Algebra.Ring.Hom.Defs

Goal state before:
pp: α : Type u_2
β : Type u_3
x✝¹ : NonAssocSemiring α
x✝ : NonAssocSemiring β
f : α →+* β
inst✝ : Nontrivial β
h : 1 = 0
⊢ f 0 = 0

Tactic:
map_zero

Goal state after:
α : Type u_2
β : Type u_3
x✝¹ : NonAssocSemiring α
x✝ : NonAssocSemiring β
f : α →+* β
inst✝ : Nontrivial β
h : 1 = 0
⊢ 0 = 0
Module: Mathlib.Algebra.GroupWithZero.Semiconj

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

Tactic:
have := mul_ne_zero ha hx
    rw [h.eq, mul_ne_zero_iff] at this
    exact @units_inv_right _ _ _ (Units.mk0 x hx) (Units.mk0 y this.1) h

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

Goal state before:
pp: α : Type u_1
inst✝ : AddMonoidWithOne α
m n : ℕ
⊢ AddCommute ↑m ↑n

Tactic:
rw [addCommute_iff_eq, ← Nat.cast_add, ← Nat.cast_add, m.add_comm]

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
⊢ Int.negSucc z • a = -1 • ↑z.succ • a

Tactic:
change (Int.negSucc z : R) • a = -1 • ((z.succ : ℤ) : R) • a

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
⊢ ↑(Int.negSucc z) • a = -1 • ↑↑z.succ • a
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝¹ : DivisionMonoid α
inst✝ : HasDistribNeg α
n : ℤ
h : Even n
⊢ 1 ^ n = 1

Tactic:
one_zpow

Goal state after:
α : Type u_2
inst✝¹ : DivisionMonoid α
inst✝ : HasDistribNeg α
n : ℤ
h : Even n
⊢ 1 = 1
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: M₀ : Type u_2
inst✝² : MonoidWithZero M₀
inst✝¹ : PartialOrder M₀
a b : M₀
inst✝ : MulPosStrictMono M₀
ha : 0 < a
hb : 1 < b
⊢ a < b * a

Tactic:
simpa using mul_lt_mul_of_pos_right hb ha

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

Goal state before:

Tactic:
_ = b * d := by rw [add_left_comm, ← mul_add, ← hcd, mul_zero, add_zero]
    _ < a * d := mul_lt_mul_of_pos_right h <| hcd.trans_lt <| add_lt_of_neg_left _ hc
    _ = _ := by rw [← add_assoc, ← mul_add, ← hcd, mul_zero, zero_add]

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

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ b / c < a ↔ b < a * c

Tactic:
by
  rw [div_eq_mul_inv, mul_inv_lt_iff₀ hc]

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

Goal state before:
pp: R : Type u
inst✝⁵ : Ring R
inst✝⁴ : LinearOrder R
a b : R
inst✝³ : PosMulStrictMono R
inst✝² : MulPosStrictMono R
inst✝¹ : AddLeftMono R
inst✝ : AddLeftReflectLE R
⊢ a * b ≤ 0 ↔ (0 < a → b ≤ 0) ∧ (b < 0 → 0 ≤ a)

Tactic:
by
  rw [← neg_nonneg, ← mul_neg, mul_nonneg_iff_pos_imp_nonneg (R := R)]
  simp only [neg_pos, neg_nonneg]

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 β
e : α ≃ β
h₁ : Monotone ⇑e
h₂ : Monotone ⇑e.symm
a✝ b✝ : α
h : e a✝ ≤ e b✝
⊢ a✝ ≤ b✝

Tactic:
simpa only [e.symm_apply_apply] using h₂ h

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : LE α
inst✝ : PartialOrder β
f : α ≃o β
x : α
y : β
hx : ∀ (x' : α), x ≤ x'
hy : ∀ (y' : β), y ≤ y'
⊢ f x = y

Tactic:
refine le_antisymm ?_ (hy _)
  rw [← f.apply_symm_apply y, f.le_iff_le]
  apply hx

Goal state after:
Module: Mathlib.Algebra.Order.Group.Lattice

Goal state before:
pp: case right
α✝ : Type u_1
inst✝⁴ : Lattice α✝
inst✝³ : CommGroup α✝
α : Type u_2
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
x y z : α
⊢ x⁻¹ * ((x ⊓ (y ⊓ z)) * ((x ⊔ y) ⊓ (x ⊔ z))) ≤ z

Tactic:
· rw [inv_mul_le_iff_le_mul, ← inf_mul_sup x z]
      exact mul_le_mul' (inf_le_inf_left _ inf_le_right) inf_le_right

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

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : Group α
a b : α
inst✝ : MulLeftMono α
ha : 1 ≤ a
hab : a ≤ b
⊢ |a|ₘ ≤ |b|ₘ

Tactic:
rwa [mabs_of_one_le ha, mabs_of_one_le (ha.trans hab)]

Goal state after:
Module: Mathlib.Algebra.Order.Group.Abs

Goal state before:
pp: G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a : G
⊢ |a|ₘ = a ↔ 1 ≤ a

Tactic:
by
  rw [mabs_eq_max_inv, max_eq_left_iff, inv_le_self_iff]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DivisionMonoid α
inst✝ : HasDistribNeg α
n : ℤ
h : Odd n
⊢ -1 ^ n = -1

Tactic:
one_zpow

Goal state after:
α : Type u_1
inst✝¹ : DivisionMonoid α
inst✝ : HasDistribNeg α
n : ℤ
h : Odd n
⊢ -1 = -1
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a : α
ha : a ≠ ⊤
b : α
⊢ a + (-a + b) = b

Tactic:
by
  simp [← add_assoc, 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 : α
h : a ≤ b
⊢ a + (b - a) = b

Tactic:
by
  refine le_antisymm ?_ le_add_tsub
  obtain ⟨c, rfl⟩ := exists_add_of_le h
  grw [add_tsub_le_left]

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

Goal state before:
pp: case neg
P Q : ℕ → Prop
inst✝¹ : DecidablePred P
inst✝ : DecidablePred Q
hPQ : ∀ (n : ℕ), P n → Q n
n : ℕ
hn : findGreatest P n ≤ findGreatest Q n
h : ¬P (n + 1)
⊢ findGreatest P n ≤ findGreatest Q (n + 1)

Tactic:
exact le_trans hn (Nat.findGreatest_mono_right _ <| le_succ _)

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

Goal state before:
pp: F : Type u_1
α✝ : Type u_2
β : Type u_3
α : Type ?u.6
inst✝³ : Ring α
inst✝² : PartialOrder α
inst✝¹ : IsOrderedRing α
inst✝ : Nontrivial α
x : α
below : ∃ n, ↑n ≤ x
above : ∃ n, x ≤ ↑n
n : { x_1 // x ≤ ↑x_1 } := Classical.indefiniteDescription (fun x_1 ↦ x ≤ ↑x_1) above
⊢ { n // ↑n ≤ x ∧ ∀ (m : ℤ), ↑m ≤ x → m ≤ n }

Tactic:
refine Int.greatestOfBdd (P := (· ≤ x)) n.1 (fun m hm ↦ ?_) below

Goal state after:
F : Type u_1
α✝ : Type u_2
β : Type u_3
α : Type ?u.6
inst✝³ : Ring α
inst✝² : PartialOrder α
inst✝¹ : IsOrderedRing α
inst✝ : Nontrivial α
x : α
below : ∃ n, ↑n ≤ x
above : ∃ n, x ≤ ↑n
n : { x_1 // x ≤ ↑x_1 } := Classical.indefiniteDescription (fun x_1 ↦ x ≤ ↑x_1) above
m : ℤ
hm : ↑m ≤ x
⊢ m ≤ ↑n
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : LinearOrder R
inst✝ : FloorSemiring R
a : R
⊢ ⌈a⌉₊ ≤ ⌊a⌋₊ + 1

Tactic:
by
  rw [ceil_le, Nat.cast_add, Nat.cast_one]
  exact (lt_floor_add_one a).le

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: R : Type u_1
inst✝⁹ : Semiring R
inst✝⁸ : LinearOrder R
inst✝⁷ : FloorSemiring R
S : Type u_3
inst✝⁶ : Semiring S
inst✝⁵ : LinearOrder S
inst✝⁴ : FloorSemiring S
F : Type u_4
inst✝³ : FunLike F R S
inst✝² : RingHomClass F R S
inst✝¹ : IsStrictOrderedRing R
inst✝ : IsStrictOrderedRing S
f : F
hf : StrictMono ⇑f
a : R
n : ℕ
⊢ ↑n ≤ f a ↔ ↑n ≤ a

Tactic:
rw [← map_natCast f, hf.le_iff_le]

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: R : Type u_1
inst✝⁷ : Semiring R
inst✝⁶ : LinearOrder R
inst✝⁵ : FloorSemiring R
S : Type u_3
inst✝⁴ : Semiring S
inst✝³ : LinearOrder S
inst✝² : FloorSemiring S
F : Type u_4
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : StrictMono ⇑f
a : R
n : ℕ
⊢ f a ≤ ↑n ↔ a ≤ ↑n

Tactic:
rw [← map_natCast f, hf.le_iff_le]

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

Goal state before:
pp: case inl
G₀ : Type u_3
M₀' : Type u_4
F' : Type u_7
inst✝³ : GroupWithZero G₀
inst✝² : MonoidWithZero M₀'
inst✝¹ : FunLike F' G₀ M₀'
inst✝ : MonoidWithZeroHomClass F' G₀ M₀'
f g : F'
h : f 0 = g 0
⊢ 0 = g 0

Tactic:
map_zero

Goal state after:
case inl
G₀ : Type u_3
M₀' : Type u_4
F' : Type u_7
inst✝³ : GroupWithZero G₀
inst✝² : MonoidWithZero M₀'
inst✝¹ : FunLike F' G₀ M₀'
inst✝ : MonoidWithZeroHomClass F' G₀ M₀'
f g : F'
h : f 0 = g 0
⊢ 0 = 0
Module: Mathlib.Algebra.Order.Ring.Basic

Goal state before:
pp: R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a b : R
inst✝ : ExistsAddOfLE R
⊢ a ^ 2 + b ^ 2 + (a * a + b * b) = 2 * (a ^ 2 + b ^ 2)

Tactic:
by simp_rw [pow_succ', pow_zero, mul_one, two_mul]

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 / c + a / c

Tactic:
mul_div_cancel_right₀ _ hc

Goal state after:
K : Type u_1
inst✝ : DivisionSemiring K
a b c : K
hc : c ≠ 0
⊢ b + a / c = b + a / c
Module: Mathlib.Algebra.Field.Basic

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝¹⁸ : Zero K
inst✝¹⁷ : Add K
inst✝¹⁶ : Neg K
inst✝¹⁵ : Sub K
inst✝¹⁴ : One K
inst✝¹³ : Mul K
inst✝¹² : Inv K
inst✝¹¹ : Div K
inst✝¹⁰ : SMul ℕ K
inst✝⁹ : SMul ℤ K
inst✝⁸ : SMul ℚ≥0 K
inst✝⁷ : SMul ℚ K
inst✝⁶ : Pow K ℕ
inst✝⁵ : Pow K ℤ
inst✝⁴ : NatCast K
inst✝³ : IntCast K
inst✝² : NNRatCast K
inst✝¹ : RatCast K
f : K → L
hf : Injective f
inst✝ : DivisionSemiring L
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : K), f (x + y) = f x + f y
mul : ∀ (x y : K), f (x * y) = f x * f y
inv : ∀ (x : K), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : K), f (x / y) = f x / f y
nsmul : ∀ (n : ℕ) (x : K), f (n • x) = n • f x
nnqsmul : ∀ (q : ℚ≥0) (x : K), f (q • x) = q • f x
npow : ∀ (x : K) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : K) (n : ℤ), f (x ^ n) = f x ^ n
natCast : ∀ (n : ℕ), f ↑n = ↑n
nnratCast : ∀ (q : ℚ≥0), f ↑q = ↑q
q : ℚ≥0
⊢ f ↑q = f (↑q.num / ↑q.den)

Tactic:
rw [nnratCast, NNRat.cast_def, div, natCast, natCast]

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 f s (t ∪ t') = image2 f s t ∪ image2 f s t'

Tactic:
by
  rw [← image2_swap, image2_union_left, image2_swap f, image2_swap f]

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
ε : Type u_9
ε' : Type u_10
s : Set α
t : Set β
u : Set γ
f : δ → γ → ε
g : α → β → δ
f' : α → ε' → ε
g' : β → γ → ε'
h_assoc : ∀ (a : α) (b : β) (c : γ), f (g a b) c = f' a (g' b c)
x✝ : Set ε
⊢ image2 f (image2 g s t) u ⊆ x✝ ↔ image2 f' s (image2 g' t u) ⊆ x✝

Tactic:
simp only [image2_subset_iff, forall_mem_image2, h_assoc]

Goal state after: