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

Goal state before:
pp: case map_compl
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : BiheytingAlgebra β
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
a✝ : α
⊢ e a✝ᶜ = (e a✝)ᶜ

Tactic:
first | rfl | exact e.apply_symm_apply _

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

Goal state before:
pp: case map_hnot
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : BiheytingAlgebra β
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
a✝ : α
⊢ e (￢a✝) = ￢e a✝

Tactic:
first | rfl | exact e.apply_symm_apply _

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

Goal state before:
pp: case map_himp
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : BiheytingAlgebra β
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
a✝ b✝ : α
⊢ e (a✝ ⇨ b✝) = e a✝ ⇨ e b✝

Tactic:
first | rfl | exact e.apply_symm_apply _

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

Goal state before:
pp: case map_sdiff
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : BiheytingAlgebra β
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
a✝ b✝ : α
⊢ e (a✝ \ b✝) = e a✝ \ e b✝

Tactic:
first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
by
  rw [symmDiff_comm, symmDiff_sdiff_eq_sup, sup_comm]

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

Goal state before:
pp: α : Sort u_1
inst✝ : DecidableEq α
a b x : α
π : Perm α
⊢ (Equiv.trans π (swap a b)) x = if π x = a then b else if π x = b then a else π x

Tactic:
by
  cases π
  rfl

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

Goal state before:
pp: case le
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : GeneralizedBooleanAlgebra β
bot : Bot α := e.bot
sdiff : SDiff α := e.sdiff
distribLattice : DistribLattice α := e.distribLattice
x✝ y✝ : α
⊢ e x✝ ≤ e y✝ ↔ x✝ ≤ y✝

Tactic:
first | rfl | exact e.apply_symm_apply _

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

Goal state before:
pp: case lt
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : GeneralizedBooleanAlgebra β
bot : Bot α := e.bot
sdiff : SDiff α := e.sdiff
distribLattice : DistribLattice α := e.distribLattice
x✝ y✝ : α
⊢ e x✝ < e y✝ ↔ x✝ < y✝

Tactic:
first | rfl | exact e.apply_symm_apply _

Goal state after:
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:
first | rfl | 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:
first | rfl | 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:
first | rfl | 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:
first | rfl | exact e.apply_symm_apply _

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

Goal state before:
pp: case le
α : 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
x✝ y✝ : α
⊢ e x✝ ≤ e y✝ ↔ x✝ ≤ y✝

Tactic:
first | rfl | exact e.apply_symm_apply _

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

Goal state before:
pp: case lt
α : 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
x✝ y✝ : α
⊢ e x✝ < e y✝ ↔ x✝ < y✝

Tactic:
first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
simp [symmDiff_assoc]

Goal state after:
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:
first | rfl | 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:
first | rfl | 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:
first | rfl | 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:
first | rfl | 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:
first | rfl | 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:
first | rfl | 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:
first | rfl | exact e.apply_symm_apply _

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
x : α
inst✝¹ : (y : α) → Decidable (y ∈ {x})
inst✝ : DecidableEq α
f g : α → β
y : α
hy : y = x
⊢ {x}.piecewise f g y = update g x (f x) y

Tactic:
subst y

Goal state after:
case pos
α : Type u_1
β : Type u_2
x : α
inst✝¹ : (y : α) → Decidable (y ∈ {x})
inst✝ : DecidableEq α
f g : α → β
⊢ {x}.piecewise f g x = update g x (f x) x
Module: Mathlib.Data.Set.Piecewise

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
t : Set β
x : α
⊢ x ∈ s.piecewise f g ⁻¹' t ↔ x ∈ s.ite (f ⁻¹' t) (g ⁻¹' t)

Tactic:
by_cases x ∈ s <;> simp [*, Set.ite]

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
x : α
⊢ x ∈ s → f x = f' x

Tactic:
hxs

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 : α
hxs : x ∈ s
⊢ f x = f' x
Module: Mathlib.Algebra.Group.Action.Pi

Goal state before:
pp: ι : Type u_1
M : Type u_7
α : Type u_8
β : Type u_9
inst✝ : SMul M β
r : M
f : ι → α
g : ι → β
e : α → β
x : α
⊢ extend f (r • g) (r • e) x = (r • extend f g e) x

Tactic:
simp only [extend_def, Pi.smul_apply]
  split_ifs <;> rfl

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

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

Tactic:
← image_preimage_coe

Goal state after:
case mp
α : Type u_1
s t u : Set α
⊢ val ⁻¹' t ⊆ val ⁻¹' u → val '' val ⁻¹' t ⊆ val '' val ⁻¹' u
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
f : α → α
s : Set α
h : MapsTo f s s
n : ℕ
⊢ (restrict f s s h)^[n] = restrict f^[n] s s ⋯

Tactic:
by
  ext
  simpa using coe_iterate_restrict _ _ _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s t u : Set α
f : α → β
h : s ∩ t = ∅
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
⊢ f '' s ∩ f '' t = ∅

Tactic:
rw [← hf.image_inter hs ht, h, image_empty]

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⟩

Goal state after:
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
b : β
hb : b ∈ t
⊢ p₂ b ∈ g '' p₁ '' s
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)
⊢ InjOn f (s ∪ r)

Tactic:
injOn_union,

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)
⊢ InjOn f s ∧ InjOn f r ∧ ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ r → f x ≠ f y

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)
⊢ Disjoint s r
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
h : Semiconj f fa fb
ha : Surjective fa
⊢ SurjOn fb (range f) (range f)

Tactic:
by
  rw [← image_univ]
  exact h.surjOn_image ha.surjOn

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
n : ℕ
a : M
⊢ (fun x ↦ x * a)^[n] 1 = a ^ n

Tactic:
by simp [mul_right_iterate]

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a : α
n : ℕ
⊢ a⁻¹ ^ Int.negSucc n = (a ^ Int.negSucc n)⁻¹

Tactic:
rw [zpow_negSucc, zpow_negSucc, inv_pow]

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₁✝ ℕ
M₁ : Type u_3
inst✝¹ : Inv M₁
inst✝ : InvolutiveInv M₂
f : M₁ → M₂
hf : Injective f
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
x : M₁
⊢ f x⁻¹⁻¹ = f x

Tactic:
rw [inv, inv, inv_inv]

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a b c : G
h : a * c = b
⊢ a = b * c⁻¹

Tactic:
by simp [h.symm]

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a b c : G
h : b * a = c
⊢ a = b⁻¹ * c

Tactic:
by simp [h.symm]

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a b c : G
h : a * c⁻¹ = b
⊢ a = b * c

Tactic:
by simp [h.symm]

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

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

Tactic:
by simp [h.symm]

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

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

Tactic:
by simp [h.symm]

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

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

Tactic:
by
  rw [mul_assoc, mul_div_cancel]

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

Goal state before:
pp: α : Type u
inst✝ : DivisionMonoid α
a b c : α
h : IsUnit c
⊢ a = b / c ↔ a * c = b

Tactic:
by
  rw [div_eq_mul_inv, h.eq_mul_inv_iff_mul_eq]

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

Goal state before:
pp: case fst
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : CommMagma M
inst✝ : CommMagma N
x✝¹ x✝ : M × N
⊢ (x✝¹ * x✝).1 = (x✝ * x✝¹).1

Tactic:
apply mul_comm

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

Goal state before:
pp: case snd
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : CommMagma M
inst✝ : CommMagma N
x✝¹ x✝ : M × N
⊢ (x✝¹ * x✝).2 = (x✝ * x✝¹).2

Tactic:
apply mul_comm

Goal state after:
Module: Mathlib.Control.Basic

Goal state before:
pp: α β γ : Type u
e : Type v
⊢ LawfulFunctor (Sum e)

Tactic:
constructor <;> intros <;> (try casesm Sum _ _)

Goal state after:
case map_const
α β γ : Type u
e : Type v
α✝ β✝ : Type u
⊢ Functor.mapConst = Functor.map ∘ Function.const β✝

case id_map.inl
α β γ : Type u
e : Type v
α✝ : Type u
x✝ : e
⊢ id <$> inl x✝ = inl x✝

case id_map.inr
α β γ : Type u
e : Type v
α✝ : Type u
x✝ : α✝
⊢ id <$> inr x✝ = inr x✝

case comp_map.inl
α β γ : Type u
e : Type v
α✝ β✝ γ✝ : Type u
g✝ : α✝ → β✝
h✝ : β✝ → γ✝
x✝ : e
⊢ (h✝ ∘ g✝) <$> inl x✝ = h✝ <$> g✝ <$> inl x✝

case comp_map.inr
α β γ : Type u
e : Type v
α✝ β✝ γ✝ : Type u
g✝ : α✝ → β✝
h✝ : β✝ → γ✝
x✝ : α✝
⊢ (h✝ ∘ g✝) <$> inr x✝ = h✝ <$> g✝ <$> inr x✝
Module: Mathlib.Logic.Nontrivial.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Nonempty α
⊢ Nontrivial (Option α)

Tactic:
by
  inhabit α
  exact ⟨none, some default, nofun⟩

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

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
a b c : G₀
hb : b ≠ 0
h : b = a⁻¹ * c
⊢ a * b = c

Tactic:
rwa [← eq_inv_mul_iff_mul_eq₀]; rintro rfl; simp [hb] at h

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

Goal state before:
pp: R : Type u
inst✝ : NonUnitalNonAssocRing R
a b : R
h : Commute a b
⊢ a * a - b * b = (a + b) * (a - b)

Tactic:
by
  rw [add_mul, mul_sub, mul_sub, h.eq, sub_add_sub_cancel]

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

Goal state before:
pp: α : Type u_4
f : α → α
hf : Involutive f
m : ℕ
⊢ id ∘ f^[1] = f

Tactic:
id_comp,

Goal state after:
α : Type u_4
f : α → α
hf : Involutive f
m : ℕ
⊢ f^[1] = f
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 - a - (c - b) ≤ b - a

Tactic:
by
  grw [tsub_le_iff_left, tsub_le_iff_left, add_left_comm, ← le_add_tsub, ← le_tsub_add]

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 : α
hb : AddLECancellable b
⊢ a ≤ a + b - b

Tactic:
by
  rw [add_comm]
  exact hb.le_add_tsub_swap

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a₁ a₂ b₁ b₂ : α
ha✝ : a₁ ≤ a₂
hb : b₁ ≤ b₂
this✝ : MulLeftMono α
this : MulRightMono α
h : a₂ * b₂ ≤ a₁ * b₁
ha : a₁ < a₂
⊢ a₁ * b₁ < a₂ * b₂

pp: case refine_2
α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a₁ a₂ b₁ b₂ : α
ha : a₁ ≤ a₂
hb✝ : b₁ ≤ b₂
this✝ : MulLeftMono α
this : MulRightMono α
h : a₂ * b₂ ≤ a₁ * b₁
hb : b₁ < b₂
⊢ a₁ * b₁ < a₂ * b₂

Tactic:
exacts [mul_lt_mul_of_lt_of_le ha hb, mul_lt_mul_of_le_of_lt ha hb]

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

Goal state before:
pp: α : Type u_1
inst✝² : LE α
inst✝¹ : Semigroup α
inst✝ : MulLeftMono α
a b : α
h : MulLECancellable (a * b)
c d : α
hcd : b * c ≤ b * d
⊢ a * (b * c) ≤ a * (b * d)

Tactic:
exact mul_le_mul_right hcd _

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

Goal state before:
pp: R : Type u
inst✝³ : Ring R
inst✝² : PartialOrder R
inst✝¹ : IsOrderedAddMonoid R
inst✝ : ZeroLEOneClass R
mul_nonneg : ∀ (a b : R), 0 ≤ a → 0 ≤ b → 0 ≤ a * b
a : R
ha : 0 ≤ a
b c : R
hbc : b ≤ c
⊢ b * a ≤ c * a

Tactic:
simpa only [sub_mul, sub_nonneg] using mul_nonneg _ _ (sub_nonneg.2 hbc) ha

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

Goal state before:
pp: R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : PartialOrder R
a b c d : R
inst✝³ : AddLeftReflectLT R
inst✝² : ExistsAddOfLE R
inst✝¹ : MulPosStrictMono R
inst✝ : AddLeftStrictMono R
hab : a < b
hcd : c < d
⊢ a * d + b * c < a * c + b * d

Tactic:
by
  obtain ⟨d, hd, rfl⟩ := exists_pos_add_of_lt' hcd
  rw [mul_add, add_right_comm, mul_add, ← add_assoc]
  gcongr
  exact hd

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

Goal state before:
pp: R : Type u
inst✝² : Semiring R
inst✝¹ : LinearOrder R
a b : R
inst✝ : PosMulStrictMono R
h : ∀ (n : ℕ), 0 ≤ a * b ^ n
⊢ a = 0 ∨ 0 < a ∧ 0 ≤ b

Tactic:
have : 0 ≤ a := by simpa only [pow_zero, mul_one] using h 0
  refine this.eq_or_lt'.imp_right fun ha ↦ ⟨ha, nonneg_of_mul_nonneg_right ?_ ha⟩
  simpa only [pow_one] using h 1

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
⊢ 0 ≤ a ^ 2

Tactic:
obtain ha | ha := le_or_gt 0 a
  · exact pow_succ_nonneg ha _
  obtain ⟨b, hab⟩ := exists_add_of_le ha.le
  have hb : 0 < b := not_le.1 fun hb ↦ (add_neg_of_neg_of_nonpos ha hb).ne' hab
  calc
    0 ≤ b ^ 2 := pow_succ_nonneg hb.le _
    _ = b ^ 2 + a * (a + b) := by rw [← hab, mul_zero, add_zero]
    _ = a ^ 2 + (a + b) * b := by rw [add_mul, mul_add, sq, sq, add_comm, add_assoc]
    _ = a ^ 2 := by rw [← hab, zero_mul, add_zero]

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
inst✝ : NoZeroDivisors R
r : R
⊢ r ^ 2 ≤ 0 ↔ r = 0

Tactic:
by
  trans r ^ 2 = 0
  · rw [le_antisymm_iff, and_iff_left (sq_nonneg r)]
  · exact sq_eq_zero_iff

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
r : α → α → Prop
a b : α
s : α → α → Prop
h₂ : r ≍ s
⊢ s ((Equiv.cast ⋯) a) ((Equiv.cast ⋯) b) ↔ r a b

Tactic:
rw [eq_of_heq h₂]

Goal state after:
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α✝ → α✝ → Prop
s✝ : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α : Type u
r : α → α → Prop
a b : α
s : α → α → Prop
h₂ : r ≍ s
⊢ s ((Equiv.cast ⋯) a) ((Equiv.cast ⋯) b) ↔ s a b
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: M : Type u_4
a : M
⊢ exp a ≠ 0

Tactic:
by simp [exp]

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 ≤ b + a - c → c ≤ b

Tactic:
hc.le_tsub_iff_right (h.trans le_add_self),

Goal state after:
α : 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 ≤ b + a → c ≤ b
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : LT α
x y : WithBot α
⊢ x < y ↔ ∃ b, y = ↑b ∧ x < ↑b

Tactic:
cases y <;> simp

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

Goal state before:
pp: k : ℕ
P : ℕ → Prop
inst✝ : DecidablePred P
⊢ findGreatest P k = 0 ↔ ∀ ⦃n : ℕ⦄, 0 < n → n ≤ k → ¬P n

Tactic:
by
  simp [findGreatest_eq_iff]

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

Goal state before:
pp: case coe.bot
α : Type u
β : Type v
inst✝³ : Add α
F : Type u_1
inst✝² : Add β
inst✝¹ : FunLike F α β
inst✝ : AddHomClass F α β
f : F
a✝ : α
⊢ map (⇑f) (↑a✝ + ⊥) = map ⇑f ↑a✝ + map ⇑f ⊥

pp: case coe.coe
α : Type u
β : Type v
inst✝³ : Add α
F : Type u_1
inst✝² : Add β
inst✝¹ : FunLike F α β
inst✝ : AddHomClass F α β
f : F
a✝¹ a✝ : α
⊢ map (⇑f) (↑a✝¹ + ↑a✝) = map ⇑f ↑a✝¹ + map ⇑f ↑a✝

Tactic:
· exact (add_bot _).symm

Goal state after:
case coe.coe
α : Type u
β : Type v
inst✝³ : Add α
F : Type u_1
inst✝² : Add β
inst✝¹ : FunLike F α β
inst✝ : AddHomClass F α β
f : F
a✝¹ a✝ : α
⊢ map (⇑f) (↑a✝¹ + ↑a✝) = map ⇑f ↑a✝¹ + map ⇑f ↑a✝
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: G : Type u_3
inst✝ : Preorder G
a b : G
⊢ exp a ≤ exp b ↔ a ≤ b

Tactic:
by simp [exp]

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

Goal state before:
pp: G : Type u_3
inst✝ : Preorder G
a b : G
⊢ exp a < exp b ↔ a < b

Tactic:
by simp [exp]

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

Goal state before:
pp: G : Type u_3
inst✝ : Preorder G
a : G
⊢ 0 < exp a

Tactic:
by simp [exp]

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

Goal state before:
pp: case inr
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
inst✝ : IsStrictOrderedRing R
ha : 0 ≤ a
b d : ℕ
hb : b ≤ b + d
⊢ ↑b ≤ a + ↑(b + d) ↔ b ≤ ⌊a⌋₊ + (b + d)

Tactic:
rw [Nat.cast_add, add_left_comm _ b, add_left_comm _ (b : R)]

Goal state after:
case inr
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
inst✝ : IsStrictOrderedRing R
ha : 0 ≤ a
b d : ℕ
hb : b ≤ b + d
⊢ ↑b ≤ ↑b + (a + ↑d) ↔ b ≤ b + (⌊a⌋₊ + d)
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
inst✝ : IsStrictOrderedRing R
ha : 0 ≤ a
n b : ℕ
⊢ b ≤ ⌊a + ↑n⌋₊ ↔ b ≤ ⌊a⌋₊ + n

Tactic:
rw [le_floor_iff (add_nonneg ha n.cast_nonneg)]
    obtain hb | hb := le_total n b
    · obtain ⟨d, rfl⟩ := exists_add_of_le hb
      rw [Nat.cast_add, add_comm n, add_comm (n : R), add_le_add_iff_right, add_le_add_iff_right,
        le_floor_iff ha]
    · obtain ⟨d, rfl⟩ := exists_add_of_le hb
      rw [Nat.cast_add, add_left_comm _ b, add_left_comm _ (b : R)]
      refine iff_of_true ?_ le_self_add
      exact le_add_of_nonneg_right <| ha.trans <| le_add_of_nonneg_right d.cast_nonneg

Goal state after: