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

Goal state before:
pp: R : Type u_2
inst✝ : Mul R
⊢ IsCancelMul R ↔ ∀ (r : R), IsRegular r

Tactic:
by
  rw [isCancelMul_iff, isLeftCancelMul_iff, isRightCancelMul_iff, ← forall_and]
  exact forall_congr' fun _ ↦ isRegular_iff.symm

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

Goal state before:
pp: α : Sort u
β : α → Sort v
inst✝ : DecidableEq α
f : (a : α) → β a
a : α
b : β a
p : (a : α) → β a → Prop
⊢ (∃ x, p x (update f a b x)) ↔ p a b ∨ ∃ x, x ≠ a ∧ p x (f x)

Tactic:
by
  rw [← not_forall_not, forall_update_iff f fun a b ↦ ¬p a b]
  simp [-not_and, not_and_or]

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

Goal state before:
pp: case neg
γ : Sort u_3
α₁ : Sort u_4
α₂ : Sort u_5
α₃ : Sort u_6
f₁₂ : α₁ → α₂
h₁₂ : Injective f₁₂
f₂₃ : α₂ → α₃
h₂₃ : Injective f₂₃
g : α₁ → γ
e' : α₃ → γ
b : α₂
h₂ : ¬∃ c, f₁₂ c = b
⊢ extend (f₂₃ ∘ f₁₂) g e' (f₂₃ b) = (e' ∘ f₂₃) b

Tactic:
extend_apply',

Goal state after:
case neg
γ : Sort u_3
α₁ : Sort u_4
α₂ : Sort u_5
α₃ : Sort u_6
f₁₂ : α₁ → α₂
h₁₂ : Injective f₁₂
f₂₃ : α₂ → α₃
h₂₃ : Injective f₂₃
g : α₁ → γ
e' : α₃ → γ
b : α₂
h₂ : ¬∃ c, f₁₂ c = b
⊢ e' (f₂₃ b) = (e' ∘ f₂₃) b

case neg.hb
γ : Sort u_3
α₁ : Sort u_4
α₂ : Sort u_5
α₃ : Sort u_6
f₁₂ : α₁ → α₂
h₁₂ : Injective f₁₂
f₂₃ : α₂ → α₃
h₂₃ : Injective f₂₃
g : α₁ → γ
e' : α₃ → γ
b : α₂
h₂ : ¬∃ c, f₁₂ c = b
⊢ ¬∃ a, (f₂₃ ∘ f₁₂) a = f₂₃ b
Module: Mathlib.Logic.Relation

Goal state before:
pp: case tail
α : Type u_1
r : α → α → Prop
i✝¹ i✝ b✝ c✝ : α
a✝ : TransGen r i✝ b✝
hbc : r b✝ c✝
ih : TransGen (Function.swap r) b✝ i✝
⊢ TransGen (Function.swap r) c✝ i✝

Tactic:
exact ih.head hbc

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case tail
α : Type u_1
r : α → α → Prop
i✝¹ i✝ b✝ c✝ : α
a✝ : ReflTransGen r i✝ b✝
hbc : r b✝ c✝
ih : ReflTransGen (Function.swap r) b✝ i✝
⊢ ReflTransGen (Function.swap r) c✝ i✝

Tactic:
exact ih.head hbc

Goal state after:
Module: Mathlib.Algebra.Group.Action.Faithful

Goal state before:
pp: case refine_2
R : Type u_4
A : Type u_5
inst✝² : MulOneClass A
inst✝¹ : SMul R A
inst✝ : IsScalarTower R A A
h : Injective fun r ↦ r • 1
r₁ r₂ : R
hr : ∀ (a : A), r₁ • a = r₂ • a
⊢ (fun r ↦ r • 1) r₁ = (fun r ↦ r • 1) r₂

Tactic:
· simpa using hr 1

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f₁ : α → β
f₂ : α → γ
g₁ : β → δ
g₂ : γ → δ
h : g₁ ∘ f₁ = g₂ ∘ f₂
a : α
⊢ Option.map (g₂ ∘ f₂) (some a) = Option.map g₂ (Option.map f₂ (some a))

Tactic:
← map_map

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f₁ : α → β
f₂ : α → γ
g₁ : β → δ
g₂ : γ → δ
h : g₁ ∘ f₁ = g₂ ∘ f₂
a : α
⊢ Option.map g₂ (Option.map f₂ (some a)) = Option.map g₂ (Option.map f₂ (some a))
Module: Mathlib.Data.Prod.Basic

Goal state before:
pp: case inr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s✝ : β → β → Prop
x y : α × β
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Total s
x✝¹ x✝ : α × β
i : α
a b : β
⊢ Prod.Lex r s (i, a) (i, b) ∨ Prod.Lex r s (i, b) (i, a)

pp: case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s✝ : β → β → Prop
x y : α × β
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Total s
x✝¹ x✝ : α × β
i : α
a : β
j : α
b : β
hji : r j i
⊢ Prod.Lex r s (i, a) (j, b) ∨ Prod.Lex r s (j, b) (i, a)

Tactic:
· exact (total_of s a b).imp (.right _) (.right _)

Goal state after:
case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s✝ : β → β → Prop
x y : α × β
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Total s
x✝¹ x✝ : α × β
i : α
a : β
j : α
b : β
hji : r j i
⊢ Prod.Lex r s (i, a) (j, b) ∨ Prod.Lex r s (j, b) (i, a)
Module: Mathlib.Order.Max

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : NoMinOrder α
x✝ : α × β
a : α
b : β
⊢ ∃ b_1, b_1 < (a, b)

Tactic:
by
    obtain ⟨c, h⟩ := exists_lt a
    exact ⟨(c, b), Prod.mk_lt_mk_iff_left.2 h⟩

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
inst✝ : SemilatticeSup α
a b c d : α
⊢ a ⊔ (c ⊔ (b ⊔ d)) = a ⊔ c ⊔ (b ⊔ d)

Tactic:
← sup_assoc

Goal state after:
α : Type u
inst✝ : SemilatticeSup α
a b c d : α
⊢ a ⊔ c ⊔ (b ⊔ d) = a ⊔ c ⊔ (b ⊔ d)
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x y : α
inst✝ : BooleanAlgebra α
⊢ x ⊓ y ⊔ x \ y = x

Tactic:
sup_inf_sdiff _ _

Goal state after:
α : Type u
x y : α
inst✝ : BooleanAlgebra α
⊢ x = x
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c : α
⊢ a ∆ b ≤ c ↔ a ≤ b ⊔ c ∧ b ≤ a ⊔ c

Tactic:
by
  simp_rw [symmDiff, sup_le_iff, sdiff_le_iff]

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

Goal state before:
pp: α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
p₁ : α → Prop
s₁ : Setoid α
s₂ : Setoid (Subtype p₁)
p₂ : Quotient s₁ → Prop
hp₂ : ∀ (a : α), p₁ a ↔ p₂ ⟦a⟧
h : ∀ (x y : Subtype p₁), s₂ x y ↔ s₁ ↑x ↑y
a✝ : { x // p₂ x }
a b : α
hab : a ≈ b
⊢ p₂ ⟦a⟧ = p₂ ⟦b⟧

Tactic:
by rw [Quotient.sound hab]

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

Goal state before:
pp: α : Type u_1
ι : Sort u_5
f : ι → α
s : Set α
h : ∀ (x : ι), f x ∈ s
⊢ Surjective (codRestrict f s h) ↔ range f = s

Tactic:
by
  simp [← range_eq_univ, Subset.antisymm_iff (a := range f), range_subset_iff, h]

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✝ : α
hxs : x✝ ∈ s
x : β
⊢ x ∈ t → g x = g' x

Tactic:
hxt

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
⊢ Surjective (image f) ↔ Surjective f

Tactic:
by
  refine ⟨fun h y => ?_, Surjective.image_surjective⟩
  rcases h {y} with ⟨s, hs⟩
  have := mem_singleton y; rw [← hs] at this; rcases this with ⟨x, _, hx⟩
  exact ⟨x, hx⟩

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
⊢ BijOn f s t

Tactic:
sdiff_singleton_eq_self

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 = t
⊢ BijOn f s t

α : 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
⊢ ¬f a ∈ f '' s
Module: Mathlib.Data.Set.Function

Goal state before:
pp: case refine_2
α : 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)
⊢ t ∪ (f '' s₁ ∩ t') \ t ⊆ t'

Tactic:
union_subset_iff

Goal state after:
case refine_2
α : 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)
⊢ t ⊆ t' ∧ (f '' s₁ ∩ t') \ t ⊆ t'
Module: Mathlib.Data.Set.Function

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : Classical.choice n ∈ s
x : β
hx : ¬x ∈ range f
⊢ x ∈ invFun f ⁻¹' s ↔ x ∈ f '' s ∪ (range f)ᶜ

Tactic:
· simp only [mem_preimage, invFun_neg hx, h, hx, mem_union, mem_compl_iff, not_false_iff, or_true]

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

Goal state before:
pp: ι : Type u_1
inst✝¹ : DecidableEq ι
M : ι → Type u_2
inst✝ : (i : ι) → AddMonoid (M i)
i : ι
a : M i
j : ι
⊢ mulSingle i (ofAdd a) j = ofAdd (single i a j)

Tactic:
by
  rcases eq_or_ne j i with rfl | h
  · simp only [mulSingle_eq_same, single_eq_same]
  · simp only [mulSingle, ne_eq, h, not_false_eq_true, Function.update_of_ne, one_apply, single,
      zero_apply, ofAdd_zero]

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

Goal state before:
pp: α : Type u
inst✝ : DivisionMonoid α
a : α
u : αˣ
hu : ↑u = a
⊢ IsUnit a⁻¹

Tactic:
← hu,

Goal state after:
α : Type u
inst✝ : DivisionMonoid α
a : α
u : αˣ
hu : ↑u = a
⊢ IsUnit (↑u)⁻¹
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: M₀ : Type u_1
inst✝ : MulZeroClass M₀
a b : M₀
h : a ≠ 0 → b = 0
this : Decidable (a = 0)
ha : ¬a = 0
⊢ a * b = 0

Tactic:
h ha,

Goal state after:
M₀ : Type u_1
inst✝ : MulZeroClass M₀
a b : M₀
h : a ≠ 0 → b = 0
this : Decidable (a = 0)
ha : ¬a = 0
⊢ a * 0 = 0
Module: Mathlib.Algebra.Ring.Int.Defs

Goal state before:
pp: case inl
α : Type u_1
inst✝ : NonAssocRing α
m : ℕ
⊢ ∀ (n : ℤ), ↑(↑m * n) = ↑↑m * ↑n

Tactic:
induction m with
    | zero => simp
    | succ m ih => simp_all [add_mul]

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

Goal state before:
pp: case inr
α : Type u_1
inst✝ : NonAssocRing α
m : ℕ
⊢ ∀ (n : ℤ), ↑(-↑m * n) = ↑(-↑m) * ↑n

Tactic:
induction m with
    | zero => simp
    | succ m ih => simp_all [add_mul]

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
⊢ b * -(1 / a) = -(b * (1 / a))

Tactic:
rw [neg_mul_eq_mul_neg]

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
x y : Mˣ
h : SemiconjBy a ↑x ↑y
n : ℕ
⊢ SemiconjBy a ↑(x ^ ↑n) ↑(y ^ ↑n)

Tactic:
by simp only [zpow_natCast, Units.val_pow_eq_pow_val, h, pow_right]

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
hx : ¬IsUnit a
n : ℕ
⊢ IsUnit (a ^ n) ↔ n = 0

Tactic:
rcases n with (_ | n)

Goal state after:
case zero
M : Type u_1
inst✝ : Monoid M
a : M
hx : ¬IsUnit a
⊢ IsUnit (a ^ 0) ↔ 0 = 0

case succ
M : Type u_1
inst✝ : Monoid M
a : M
hx : ¬IsUnit a
n : ℕ
⊢ IsUnit (a ^ (n + 1)) ↔ n + 1 = 0
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝ : Semiring α
h : IsUnit 2
a : α
u : αˣ
hu : ↑u = 2
⊢ a = ↑u⁻¹ * (2 * a)

Tactic:
← hu,

Goal state after:
α : Type u_2
inst✝ : Semiring α
h : IsUnit 2
a : α
u : αˣ
hu : ↑u = 2
⊢ a = ↑u⁻¹ * (↑u * a)
Module: Mathlib.Algebra.Ring.Parity

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

Tactic:
rw [iterate_add, hf.iterate_two_mul, id_comp, iterate_one]

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

Goal state before:
pp: α : Type u
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : MulLeftStrictMono α
a b c d : α
hab : a < b
hcd : c < d
⊢ a / d < b / c

Tactic:
rw [div_eq_mul_inv, div_eq_mul_inv, mul_comm b, mul_inv_lt_inv_mul_iff, mul_comm]

Goal state after:
α : Type u
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : MulLeftStrictMono α
a b c d : α
hab : a < b
hcd : c < d
⊢ a * c < b * d
Module: Mathlib.Algebra.Order.Monoid.Defs

Goal state before:
pp: α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : LinearOrder α
hmul : ∀ (a b c : α), b < c → a * b < a * c
a b c : α
h : c < b
⊢ a * c < a * b

Tactic:
exact hmul _ _ _ h

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

Goal state before:
pp: R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : Preorder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : PosMulMono R
inst✝¹ : AddRightMono R
inst✝ : AddRightReflectLE R
h : b ≤ a
hc : c ≤ 0
d : R
hcd : 0 = c + d
⊢ d * a = c * b + (d * b + d * a)

Tactic:
by rw [← add_assoc, ← add_mul, ← hcd, zero_mul, zero_add]

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 : R
inst✝³ : ExistsAddOfLE R
inst✝² : PosMulStrictMono R
inst✝¹ : AddRightStrictMono R
inst✝ : AddRightReflectLT R
h : b < a
hc : c < 0
d : R
hcd : 0 = c + d
⊢ d * a = c * b + (d * b + d * a)

Tactic:
by rw [← add_assoc, ← add_mul, ← hcd, zero_mul, zero_add]

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

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
ha : 1 ≤ a ^ 2
⊢ a * a ⊓ 1 * a ⊓ (a ⊓ 1) * 1 = a ⊓ 1

Tactic:
← pow_two,

Goal state after:
α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
ha : 1 ≤ a ^ 2
⊢ a ^ 2 ⊓ 1 * a ⊓ (a ⊓ 1) * 1 = a ⊓ 1
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
⊢ 1 ≤ a * a ⊔ a⁻¹ * a ⊔ (a ⊔ a⁻¹) * a⁻¹

Tactic:
← pow_two,

Goal state after:
α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
⊢ 1 ≤ a ^ 2 ⊔ a⁻¹ * a ⊔ (a ⊔ a⁻¹) * a⁻¹
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
⊢ 1 ≤ (a ⊔ a⁻¹) * a⁻¹ ⊔ (a ^ 2 ⊔ 1)

Tactic:
← sup_assoc

Goal state after:
α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
⊢ 1 ≤ (a ⊔ a⁻¹) * a⁻¹ ⊔ a ^ 2 ⊔ 1
Module: Mathlib.Algebra.Order.Group.Abs

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

Tactic:
simp only [mabs_inv, mabs_of_one_le hb]

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

Goal state before:
pp: case inr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
b : G
hb : 1 ≤ b
⊢ |b⁻¹|ₘ = b

Tactic:
simp only [mabs_inv, mabs_of_one_le hb]

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 b c : G
⊢ |a * b * c|ₘ ≤ |a|ₘ * |b|ₘ * |c|ₘ

Tactic:
mabs_mul_le,

Goal state after:
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b c : G
⊢ |a * b|ₘ * |c|ₘ ≤ |a|ₘ * |b|ₘ * |c|ₘ
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ (a ⊔ b) ^ 2 = (a ⊓ b)⁻¹ * ((a ⊓ b) * ((a ⊔ b) * (a ⊔ b)))

Tactic:
← pow_two,

Goal state after:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ (a ⊔ b) ^ 2 = (a ⊓ b)⁻¹ * ((a ⊓ b) * (a ⊔ b) ^ 2)
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ (a ⊔ b) ^ 2 = a * b * |b / a|ₘ

Tactic:
rw [← inf_mul_sup a b, ← sup_div_inf_eq_mabs_div, div_eq_mul_inv, ← mul_assoc, mul_comm,
     mul_assoc, ← pow_two, inv_mul_cancel_left]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Group α
inst✝ : LinearOrder α
a b : α
h : |a|ₘ = b
⊢ a = b ∨ a = b⁻¹

Tactic:
simpa only [← h, eq_comm (a := |a|ₘ), inv_eq_iff_eq_inv] using mabs_choice a

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

Goal state before:
pp: case H1
x y a b : ℕ
h : 0 < a
IH : ∀ {s t s' t' : ℤ}, x.P y (b % a, s, t) → x.P y (a, s', t') → x.P y ((b % a).xgcdAux s t a s' t')
s t s' t' : ℤ
p : x.P y (a, s, t)
⊢ x.P y (b, s', t') → x.P y (a.xgcdAux s t b s' t')

Tactic:
p'

Goal state after:
case H1
x y a b : ℕ
h : 0 < a
IH : ∀ {s t s' t' : ℤ}, x.P y (b % a, s, t) → x.P y (a, s', t') → x.P y ((b % a).xgcdAux s t a s' t')
s t s' t' : ℤ
p : x.P y (a, s, t)
p' : x.P y (b, s', t')
⊢ x.P y (a.xgcdAux s t b s' t')
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Group α
inst✝ : Group β
e : WithZero α ≃* WithZero β
x : α
⊢ e ↑x ≠ 0

Tactic:
simp [ne_eq, ← e.eq_symm_apply]

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

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

Tactic:
by ext x; cases x <;> simp

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hc : AddLECancellable c
h : c ≤ a
⊢ a - c < b - c ↔ a < b

Tactic:
rw [hc.lt_tsub_iff_left, add_tsub_cancel_of_le h]

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

Goal state before:
pp: α : 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

Tactic:
cases a <;> simp [zero_nsmul]

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

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
n : ℕ
⊢ Nat.find h ≤ n ↔ ∃ m, m ≤ n ∧ p m

Tactic:
simp only [← Nat.lt_succ_iff, find_lt_iff]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case some
α : Type u_1
inst✝¹ : Preorder α
y : WithBot α
inst✝ : NoBotOrder α
a : α
⊢ (∀ (a_1 : α), ↑a_1 ≤ Option.some a → ↑a_1 ≤ y) ↔ Option.some a ≤ y

Tactic:
· exact ⟨fun h ↦ h _ le_rfl, fun hay b ↦ hay.trans'⟩

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
x y : WithZero α
inst✝ : NoMinOrder α
hx : x ≠ 0
hy : y ≠ 0
z' : WithZero α
hnz' : z' ≠ 0
hzx : z' ≤ x
hzy : z' ≤ y
z : WithZero α
hnz : z ≠ 0
hlt : z < z'
⊢ ∃ z, z ≠ 0 ∧ z < x ∧ z < y

Tactic:
use z, hnz

Goal state after:
case right
α : Type u_1
inst✝¹ : LinearOrder α
x y : WithZero α
inst✝ : NoMinOrder α
hx : x ≠ 0
hy : y ≠ 0
z' : WithZero α
hnz' : z' ≠ 0
hzx : z' ≤ x
hzy : z' ≤ y
z : WithZero α
hnz : z ≠ 0
hlt : z < z'
⊢ z < x ∧ z < y
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
n : ℕ
hn : n ≠ 0
a : R
⊢ ⌊a * ↑n⌋₊ / n = ⌊a⌋₊

Tactic:
rcases le_total a 0 with ha | ha

Goal state after:
case inl
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
n : ℕ
hn : n ≠ 0
a : R
ha : a ≤ 0
⊢ ⌊a * ↑n⌋₊ / n = ⌊a⌋₊

case inr
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
n : ℕ
hn : n ≠ 0
a : R
ha : 0 ≤ a
⊢ ⌊a * ↑n⌋₊ / n = ⌊a⌋₊
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: case refine_1
R : Type u_1
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
a : R
ha : 0 ≤ a
⊢ -1 ≤ a - ↑⌊a⌋₊

Tactic:
simpa using (floor_le ha).trans (le_add_of_nonneg_right zero_le_one)

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

Goal state before:
pp: α : Type u
inst✝¹ : Monoid α
a b c : α
inst✝ : Invertible c
⊢ a * c = b ↔ a = b * ⅟c

Tactic:
rw [← mul_left_inj_of_invertible (c := ⅟c), mul_invOf_cancel_right]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : LT α
x : WithTop αᵒᵈ
y : WithBot α
⊢ x < WithBot.toDual y ↔ y < WithTop.ofDual x

Tactic:
by cases x <;> cases y <;> simp [lt_toDual]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : LT α
x : WithTop α
y : WithBot αᵒᵈ
⊢ x < WithBot.ofDual y ↔ y < WithTop.toDual x

Tactic:
by cases x <;> cases y <;> simp [lt_toDual]

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

Goal state before:
pp: G₀ : Type u_3
G₀' : Type u_5
F : Type u_6
inst✝³ : GroupWithZero G₀
inst✝² : GroupWithZero G₀'
inst✝¹ : FunLike F G₀ G₀'
inst✝ : MonoidWithZeroHomClass F G₀ G₀'
f : F
a : G₀
⊢ f a⁻¹ = (f a)⁻¹

Tactic:
by
  by_cases h : a = 0
  · simp [h, map_zero f]
  · apply eq_inv_of_mul_eq_one_left
    rw [← map_mul, inv_mul_cancel₀ h, map_one]

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

Goal state before:
pp: K : Type u_1
inst✝ : DivisionRing K
a : K
h : a ≠ 0
⊢ -a / a = -1

Tactic:
by rw [neg_div, div_self h]

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

Goal state before:
pp: case inr
K : Type u_1
inst✝ : DivisionRing K
a : K
ha : a ≠ 0
⊢ a * a = 1 ↔ a = -1 ∨ a = 0 ∨ a = 1

Tactic:
← pow_two,

Goal state after:
case inr
K : Type u_1
inst✝ : DivisionRing K
a : K
ha : a ≠ 0
⊢ a ^ 2 = 1 ↔ a = -1 ∨ a = 0 ∨ a = 1
Module: Mathlib.Algebra.Field.Basic

Goal state before:
pp: case neg
K : Type u_1
L : Type u_2
inst✝ : Field K
a : K
n : ℕ
h : ¬a = 0
⊢ a ^ (↑n + 1) = a ^ ↑n * a

Tactic:
rw [zpow_add_one₀ h]

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

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedRing α
a b : α
⊢ a * b = |a| * |b| ∨ a * b = -(|a| * |b|)

Tactic:
rcases le_total a 0 with ha | ha

Goal state after:
case inl
α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedRing α
a b : α
ha : a ≤ 0
⊢ a * b = |a| * |b| ∨ a * b = -(|a| * |b|)

case inr
α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedRing α
a b : α
ha : 0 ≤ a
⊢ a * b = |a| * |b| ∨ a * b = -(|a| * |b|)
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 : β), Monotone (swap f b)
h₁ : ∀ (a : α), Antitone (f a)
⊢ BddAbove s → BddBelow t → BddAbove (image2 f s t)

Tactic:
by
  rintro ⟨a, ha⟩ ⟨b, hb⟩
  exact ⟨f a b, mem_upperBounds_image2_of_mem_upperBounds_of_mem_lowerBounds h₀ h₁ ha hb⟩

Goal state after:
Module: Mathlib.Order.Bounds.Image

Goal state before:
pp: case refine_1
α : Type u
π : α → Type u_1
inst✝ : (a : α) → Preorder (π a)
s : Set ((a : α) → π a)
f : (a : α) → π a
H : IsLUB s f
a : α
b : π a
hb : b ∈ upperBounds (eval a '' s)
⊢ f a ≤ b

Tactic:
suffices h : Function.update f a b ∈ upperBounds s from Function.update_self a b f ▸ H.2 h a

Goal state after:
case refine_1
α : Type u
π : α → Type u_1
inst✝ : (a : α) → Preorder (π a)
s : Set ((a : α) → π a)
f : (a : α) → π a
H : IsLUB s f
a : α
b : π a
hb : b ∈ upperBounds (eval a '' s)
⊢ update f a b ∈ upperBounds s
Module: Mathlib.Order.Bounds.OrderIso

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
s : Set β
x : β
⊢ IsLUB (⇑f ⁻¹' s) (f.symm x) ↔ IsLUB s x

Tactic:
by
  rw [isLUB_preimage, f.apply_symm_apply]

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

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ Icc a b \ {a, b} = Ioo a b

Tactic:
by
  rw [insert_eq, ← sdiff_sdiff, Icc_sdiff_left, Ioc_sdiff_right]

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

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a : α
s : Set α
ho : Iio a ⊆ s
hc : s ⊆ Iic a
h : a ∈ s
⊢ Iio a ∪ {a} ⊆ s

Tactic:
union_subset_iff

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
a : α
s : Set α
ho : Iio a ⊆ s
hc : s ⊆ Iic a
h : a ∈ s
⊢ Iio a ⊆ s ∧ {a} ⊆ s
Module: Mathlib.Order.Bounds.Basic

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Set α
a b : α
h : IsLUB s a
⊢ b < a ↔ ∃ c ∈ s, b < c

Tactic:
simp_rw [← not_le, isLUB_le_iff h, mem_upperBounds, not_forall, not_le, exists_prop]

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

Goal state before:
pp: α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a b : α
inst✝ : IsStrictOrderedRing α
⊢ (a + b) / 2 < b ↔ a < b

Tactic:
by simp [div_lt_iff₀, mul_two]

Goal state after: