mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Defs.Unbundled

Goal state before:
pp: case inr.inr
α : Sort u_1
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : Std.Trichotomous r
a b c : α
h₁ : r a b
h₂ : ¬r c b
h₃ : r c b
⊢ r a c

Tactic:
exact absurd h₃ h₂

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

Goal state before:
pp: M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
m : M
k' k : ℕ
ih : ∀ (m_1 : ℕ), m_1 < k + 1 → npowRec (m_1 + 1) m = 1 * npowRec' (m_1 + 1) m
⊢ npowRec (k + 1 + 1) m = 1 * npowRec' (k + 1 + 1) m

Tactic:
rw [npowRec, npowRec'_succ k.succ_ne_zero, ← mul_assoc]

Goal state after:
M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
m : M
k' k : ℕ
ih : ∀ (m_1 : ℕ), m_1 < k + 1 → npowRec (m_1 + 1) m = 1 * npowRec' (m_1 + 1) m
⊢ npowRec (k + 1) m * m = 1 * npowRec' k.succ m * m
Module: Mathlib.Logic.Basic

Goal state before:
pp: p : Prop → Prop
x✝ : ∃ h, p h
h₁ : Prop
h₂ : p h₁
H : h₁
⊢ p True

Tactic:
simpa only [H] using h₂

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: p : Prop → Prop
x✝ : ∃ h, p h
h₁ : Prop
h₂ : p h₁
H : ¬h₁
⊢ p False

Tactic:
simpa only [H] using h₂

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

Goal state before:
pp: α : Sort u_1
β : Sort u_2
inst✝ : Nonempty α
f : α → β
g : β → α
hf : Injective f
hg : RightInverse g f
b : β
⊢ f (invFun f b) = b

Tactic:
exact invFun_eq ⟨g b, hg b⟩

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

Goal state before:
pp: case refine_1
α : Sort u_1
β : Sort u_2
r : α → β → Prop
h : ∀ (a : α), ∃! b, r a b
⊢ ∃ f, ∀ {a : α} {b : β}, r a b ↔ f a = b

Tactic:
refine ⟨fun a ↦ (h a).choose, fun hr ↦ ?_, fun h' ↦ h' ▸ ?_⟩

Goal state after:
case refine_1.refine_1
α : Sort u_1
β : Sort u_2
r : α → β → Prop
h : ∀ (a : α), ∃! b, r a b
a✝ : α
b✝ : β
hr : r a✝ b✝
⊢ (fun a ↦ Exists.choose ⋯) a✝ = b✝

case refine_1.refine_2
α : Sort u_1
β : Sort u_2
r : α → β → Prop
h : ∀ (a : α), ∃! b, r a b
a✝ : α
b✝ : β
h' : (fun a ↦ Exists.choose ⋯) a✝ = b✝
⊢ r a✝ ((fun a ↦ Exists.choose ⋯) a✝)
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
⊢ ReflTransGen (SymmGen r) = EqvGen r

Tactic:
rw [← eqvGen_eq_reflTransGen, eqvGen_symmGen]

Goal state after:
Module: Mathlib.Algebra.Notation.Pi.Basic

Goal state before:
pp: ι : Type u_1
M : ι → Type u_6
inst✝¹ : (i : ι) → One (M i)
inst✝ : DecidableEq ι
i : ι
x : M i
⊢ mulSingle i x = 1 ↔ x = 1

Tactic:
refine ⟨fun h => ?_, fun h => h.symm ▸ mulSingle_one i⟩
  rw [← mulSingle_eq_same i x, h, one_apply]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f₁ : α → β
g₁ : γ → δ
f₂ : β → α
g₂ : δ → γ
hf : LeftInverse f₁ f₂
hg : LeftInverse g₁ g₂
a : β × δ
⊢ map f₁ g₁ (map f₂ g₂ a) = a

Tactic:
by rw [Prod.map_map, hf.comp_eq_id, hg.comp_eq_id, map_id, id]

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: case neg
α : Type u_2
β : Type u_3
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : f a = f b
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ False

Tactic:
have : ¬ f a = f b := by rename_i h; exact inj.ne h
    contradiction

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝¹ : (i : ι) → Preorder (π i)
inst✝ : ∀ (i : ι), DenselyOrdered (π i)
a b : (i : ι) → π i
hab : a ≤ b
i : ι
hi : a i < b i
⊢ ∃ a_1, (a ≤ a_1 ∧ ∃ i, a i < a_1 i) ∧ a_1 ≤ b ∧ ∃ i, a_1 i < b i

Tactic:
obtain ⟨c, ha, hb⟩ := exists_between hi

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝¹ : (i : ι) → Preorder (π i)
inst✝ : ∀ (i : ι), DenselyOrdered (π i)
a b : (i : ι) → π i
hab : a ≤ b
i : ι
hi : a i < b i
c : π i
ha : a i < c
hb : c < b i
⊢ ∃ a_1, (a ≤ a_1 ∧ ∃ i, a i < a_1 i) ∧ a_1 ≤ b ∧ ∃ i, a_1 i < b i
Module: Mathlib.Order.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝¹ : (i : ι) → Preorder (π i)
inst✝ : ∀ (i : ι), DenselyOrdered (π i)
a b : (i : ι) → π i
hab : a ≤ b
i : ι
hi : a i < b i
c : π i
ha : a i < c
hb : c < b i
⊢ a i < update a i c i

Tactic:
rwa [update_self]

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝¹ : (i : ι) → Preorder (π i)
inst✝ : ∀ (i : ι), DenselyOrdered (π i)
a b : (i : ι) → π i
hab : a ≤ b
i : ι
hi : a i < b i
c : π i
ha : a i < c
hb : c < b i
⊢ update a i c i < b i

Tactic:
rwa [update_self]

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

Goal state before:
pp: a b : ℤ
⊢ 0 ≤ a * b → 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0

Tactic:
grind [Int.mul_comm, Int.mul_nonneg_iff_of_pos_right]

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

Goal state before:
pp: a : ℕ
ha : a ≠ 1
b : ℕ
⊢ a * b ≤ a ^ b

Tactic:
by
  cases b with
  | zero => exact Nat.zero_le _
  | succ b =>
      obtain rfl | ha0 : a = 0 ∨ a > 0 := a.eq_zero_or_pos
      · rw [Nat.zero_mul]; exact Nat.zero_le _
      · have ha1 : a > 1 := Nat.lt_of_le_of_ne ha0 ha.symm
        rw [Nat.pow_succ']; exact Nat.mul_le_mul_left a (Nat.lt_pow_self ha1)

Goal state after:
Module: Mathlib.Order.GaloisConnection.Defs

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

Tactic:
constructor
  · rintro rfl x
    exact (gc x y).symm
  · 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✝ : GeneralizedCoheytingAlgebra α
a b : α
h : b ≤ a
⊢ a \ b ⊔ b = a

Tactic:
rw [sup_comm, sup_sdiff_cancel_right h]

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

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
s : x ⊓ y ⊔ z = x \ y ⊔ x ⊓ y
i : x ⊓ y ⊓ z = ⊥
⊢ x \ y = z

Tactic:
rw [sup_comm] at s

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
s : z ⊔ x ⊓ y = x \ y ⊔ x ⊓ y
i : x ⊓ y ⊓ z = ⊥
⊢ x \ y = z
Module: Mathlib.Logic.Equiv.Option

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
x : β
e : { e // e none = x }
b : { y // y ≠ x }
⊢ (fun a ↦ ⟨↑e (some a), ⋯⟩) ((fun b ↦ ((↑e).symm ↑b).get ⋯) b) = b

Tactic:
by
        ext
        simp

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

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : y = z ⊔ y \ x
| y

Tactic:
rw [← sup_sdiff_cancel_right hx]

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : y = z ⊔ y \ x
| x ⊔ y \ x
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
inst✝ : GeneralizedBooleanAlgebra α
x y z : α
⊢ x \ z ⊓ y = (x ⊓ y) \ z

Tactic:
inf_comm x,

Goal state after:
α : Type u
inst✝ : GeneralizedBooleanAlgebra α
x y z : α
⊢ x \ z ⊓ y = (y ⊓ x) \ z
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
β : Type u_1
x y z : α
inst✝ : BooleanAlgebra α
a b : α
⊢ a ⊓ (b ⊔ bᶜ) = a

Tactic:
sup_compl_eq_top,

Goal state after:
α : Type u
β : Type u_1
x y z : α
inst✝ : BooleanAlgebra α
a b : α
⊢ a ⊓ ⊤ = a
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
β : Type u_1
x y z : α
inst✝⁹ : Max α
inst✝⁸ : Min α
inst✝⁷ : LE α
inst✝⁶ : LT α
inst✝⁵ : Top α
inst✝⁴ : Bot α
inst✝³ : Compl α
inst✝² : SDiff α
inst✝¹ : HImp α
inst✝ : BooleanAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
map_compl : ∀ (a : α), f aᶜ = (f a)ᶜ
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
a : α
⊢ f a ⊔ (f a)ᶜ = f ⊤

Tactic:
sup_compl_eq_top,

Goal state after:
α : Type u
β : Type u_1
x y z : α
inst✝⁹ : Max α
inst✝⁸ : Min α
inst✝⁷ : LE α
inst✝⁶ : LT α
inst✝⁵ : Top α
inst✝⁴ : Bot α
inst✝³ : Compl α
inst✝² : SDiff α
inst✝¹ : HImp α
inst✝ : BooleanAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
map_compl : ∀ (a : α), f aᶜ = (f a)ᶜ
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
a : α
⊢ ⊤ = f ⊤
Module: Mathlib.Order.SymmDiff

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

Tactic:
sdiff_symmDiff,

Goal state after:
α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b c : α
⊢ c ⊓ a ⊓ b ⊔ c \ a ⊓ c \ b = c ⊓ a ⊓ b ⊔ c \ (a ⊔ b)
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_4
P : α → Sort u_9
e : α ≃ β
g : (b : β) → P (e.symm b)
b : β
⊢ ⋯ ▸ g (e (e.symm b)) ≍ g b

Tactic:
eqRec_heq_iff

Goal state after:
α : Sort u_1
β : Sort u_4
P : α → Sort u_9
e : α ≃ β
g : (b : β) → P (e.symm b)
b : β
⊢ g (e (e.symm b)) ≍ g b
Module: Mathlib.Data.Set.Restrict

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s t : Set α
⊢ s.domRestrict f '' Subtype.val ⁻¹' t = f '' (t ∩ s)

Tactic:
domRestrict_eq,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s t : Set α
⊢ f ∘ Subtype.val '' Subtype.val ⁻¹' t = f '' (t ∩ s)
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
⊢ f ⁻¹' s ⊆ f ⁻¹' t ↔ s ⊆ t

Tactic:
constructor
  · intro h x hx
    rcases hs hx with ⟨y, rfl⟩
    exact h hx
  intro h x; apply h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
ht : t ⊆ range f
⊢ f ⁻¹' s = f ⁻¹' t ↔ s = t

Tactic:
constructor
  · intro h
    apply Subset.antisymm
    · rw [← preimage_subset_preimage_iff hs, h]
    · rw [← preimage_subset_preimage_iff ht, h]
  rintro rfl; rfl

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
⊢ s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅) ↔ s = s₁ ∧ t = t₁

Tactic:
rw [nonempty_iff_ne_empty, Ne, prod_eq_empty_iff] at h

Goal state after:
case inr
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : ¬(s = ∅ ∨ t = ∅)
⊢ s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅) ↔ s = s₁ ∧ t = t₁
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
s : Set α
⊢ ¬s.offDiag.Nonempty ↔ ¬s.Nontrivial

Tactic:
offDiag_nonempty.not

Goal state after:
α : Type u_1
s : Set α
⊢ ¬s.Nontrivial ↔ ¬s.Nontrivial
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
⊢ Injective (image f)

Tactic:
intro s t h
  rw [← preimage_image_eq s hf, ← preimage_image_eq t hf, h]

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
F : Type u_9
inst✝¹ : Mul M
inst✝ : Mul N
f : M →ₙ* N
g : N → M
h₁ : LeftInverse g ⇑f
h₂ : RightInverse g ⇑f
x y : N
⊢ g (x * y) = g (f (g x) * f (g y))

Tactic:
by rw [h₂ x, h₂ y]

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 s t
⊢ BijOn f (insert a s) (insert (f a) t)

Tactic:
insert_eq

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 s t
⊢ BijOn f ({a} ∪ s) (insert (f a) t)
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 s t
⊢ BijOn f ({a} ∪ s) (insert (f a) t)

Tactic:
insert_eq

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 s t
⊢ BijOn f ({a} ∪ s) ({f a} ∪ t)
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 s t
⊢ BijOn f ({a} ∪ s) ({f a} ∪ t)

Tactic:
insert_eq

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 s t
⊢ BijOn f ({a} ∪ s) ({f a} ∪ t)
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
s s₁ : Set α
f : α → β
f' : β → α
hf : LeftInvOn f' f s
⊢ f' ⁻¹' s₁ ∩ f '' s = f' ⁻¹' (s₁ ∩ s) ∩ f '' s

Tactic:
refine Subset.antisymm ?_ (inter_subset_inter_left _ (preimage_mono inter_subset_left))

Goal state after:
α : Type u_1
β : Type u_2
s s₁ : Set α
f : α → β
f' : β → α
hf : LeftInvOn f' f s
⊢ f' ⁻¹' s₁ ∩ f '' s ⊆ f' ⁻¹' (s₁ ∩ s) ∩ f '' s
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
b : β
inst✝ : Nonempty α
h : ∃ a, a ∈ s ∧ f a = b
⊢ (if h : ∃ a, a ∈ s ∧ f a = b then Classical.choose h else Classical.choice inst✝) ∈ s ∧
    f (if h : ∃ a, a ∈ s ∧ f a = b then Classical.choose h else Classical.choice inst✝) = b

Tactic:
dif_pos h

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
b : β
inst✝ : Nonempty α
h : ∃ a, a ∈ s ∧ f a = b
⊢ Classical.choose h ∈ s ∧ f (Classical.choose h) = b
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
inst✝ : Nonempty α
h : SurjOn f s t
⊢ BijOn f (invFunOn f s '' t) t

Tactic:
by
  refine h.invOn_invFunOn.bijOn ?_ (mapsTo_image _ _)
  rintro _ ⟨y, hy, rfl⟩
  rwa [h.rightInvOn_invFunOn hy]

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

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
G : Type u_5
H : Type u_6
F : Type u_7
inst✝¹ : Group G
inst✝ : CommGroup H
f : G →* H
hf : Function.Injective ⇑f
⊢ ∀ (a b : G), a * b = b * a

Tactic:
by simp_rw [← hf.eq_iff, map_mul, mul_comm, implies_true]

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

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

Tactic:
Int.negSucc_mul_negSucc,

Goal state after:
α : Type u_1
inst✝ : DivisionMonoid α
a : α
m n : ℕ
⊢ a ^ (↑m.succ * ↑n.succ) = ((a ^ (m + 1))⁻¹ ^ (n + 1))⁻¹
Module: Mathlib.Algebra.Group.Units.Basic

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

Tactic:
by
  rw [← div_eq_inv_mul, ← div_eq_inv_mul, hb.div_eq_div_iff hd]

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

Goal state before:
pp: M₀ : Type u_1
M₀' : Type u_2
inst✝¹ : MulZeroOneClass M₀
inst✝ : Nontrivial M₀
h : 1 = 0
x y : M₀
hx : x ≠ y
⊢ 1 * x = 0

Tactic:
by rw [h, zero_mul]

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

Goal state before:
pp: M₀ : Type u_1
M₀' : Type u_2
inst✝¹ : MulZeroOneClass M₀
inst✝ : Nontrivial M₀
h : 1 = 0
x y : M₀
hx : x ≠ y
⊢ 0 = 1 * y

Tactic:
by rw [h, zero_mul]

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

Goal state before:
pp: M₀ : Type u_1
inst✝ : MulZeroClass M₀
⊢ NoZeroDivisors M₀ ↔ ∀ (x : M₀), x ≠ 0 → (∀ (y : M₀), x * y = 0 → y = 0) ∧ ∀ (y : M₀), y * x = 0 → y = 0

Tactic:
simp only [forall_and, ← noZeroDivisors_iff_right_eq_zero_of_mul,
    ← noZeroDivisors_iff_left_eq_zero_of_mul, and_self]

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

Goal state before:
pp: α : Type u_4
inst✝ : Group α
a : α
n : ℕ
x✝ : α
⊢ (Equiv.mulLeft a ^ n) x✝ = (Equiv.mulLeft (a ^ n)) x✝

Tactic:
simp [Perm.coe_pow]

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

Goal state before:
pp: α : Type u_4
inst✝ : Group α
a : α
n : ℕ
x✝ : α
⊢ (Equiv.mulRight a ^ n) x✝ = (Equiv.mulRight (a ^ n)) x✝

Tactic:
simp [Perm.coe_pow]

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

Goal state before:
pp: case neg
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
h : ¬a = 0
⊢ a * (a * a⁻¹) = a

Tactic:
mul_inv_cancel₀ h,

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

Goal state before:
pp: case neg
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
h : ¬a = 0
⊢ a * a⁻¹ * a = a

Tactic:
mul_inv_cancel₀ h,

Goal state after:
case neg
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
h : ¬a = 0
⊢ 1 * a = a
Module: Mathlib.Algebra.GroupWithZero.Action.Defs

Goal state before:
pp: case neg
α : Type u_10
β : Type u_11
inst✝² : Group α
inst✝¹ : GroupWithZero β
inst✝ : MulDistribMulAction α β
g : α
x : β
hx : ¬x = 0
⊢ g • x⁻¹ = (g • x)⁻¹

Tactic:
apply eq_inv_of_mul_eq_one_right
    rw [← smul_mul', mul_inv_cancel₀ hx, smul_one]

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

Goal state before:
pp: α : Type u
inst✝ : NonAssocSemiring α
n : ℕ
a : α
⊢ n • a = ↑n * a

Tactic:
by
  induction n with
  | zero => rw [zero_nsmul, Nat.cast_zero, zero_mul]
  | succ n ih => rw [succ_nsmul, ih, Nat.cast_succ, add_mul, one_mul]

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

Goal state before:
pp: x : ℤ
x✝ : ∃ n, n * n = x
n : ℤ
hn : n * n = x
⊢ ↑n.natAbs * ↑n.natAbs = n * n

Tactic:
← Int.natCast_mul,

Goal state after:
x : ℤ
x✝ : ∃ n, n * n = x
n : ℤ
hn : n * n = x
⊢ ↑(n.natAbs * n.natAbs) = n * n
Module: Mathlib.Data.List.TFAE

Goal state before:
pp: case cons
c : Prop
l : List Prop
a b : Prop
IH : ∀ {a b : Prop}, (a → b) ∧ IsChain (fun x1 x2 ↦ x1 → x2) (b :: l) → (l.getLastD b → a) → (a ↔ b) ∧ (b :: l).TFAE
h_last : l.getLastD c → a
ab : a → b
bc : b → c
ch : IsChain (fun x1 x2 ↦ x1 → x2) (c :: l)
this : (b ↔ c) ∧ (c :: l).TFAE
⊢ (a ↔ b) ∧ (b ↔ c) ∧ (c :: l).TFAE

Tactic:
exact ⟨⟨ab, h_last ∘ (this.2 c (.head _) _ getLastD_mem_cons).1 ∘ bc⟩, this⟩

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:
rw [← div_eq_mul_inv, ← div_eq_mul_inv, hbd.div_eq_div_iff_of_isUnit hb hd]

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

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
m n : ℕ
⊢ a ^ (↑m - ↑n) = a ^ m / a ^ n

Tactic:
by
  simpa using zpow_sub₀ ha m n

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

Goal state before:
pp: M : Type u_3
M₂ : Type u_4
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
F : Type u_5
inst✝⁵ : FunLike F M M₂
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst✝³ : Ring R
inst✝² : Ring S
inst✝¹ : Module R M
inst✝ : Module S M₂
x : ℤ
a : M
⊢ f (↑x • a) = ↑x • f a

Tactic:
simp only [Int.cast_smul_eq_zsmul, map_zsmul]

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

Goal state before:
pp: case refine_1
N : Type u_2
r : N → N → Prop
inst✝ : Group N
h : Covariant N N (fun x1 x2 ↦ x1 * x2) r
a b c : N
bc : r ((fun x1 x2 ↦ x1 * x2) a b) ((fun x1 x2 ↦ x1 * x2) a c)
⊢ r (a⁻¹ * (a * b)) c

Tactic:
← inv_mul_cancel_left a c

Goal state after:
case refine_1
N : Type u_2
r : N → N → Prop
inst✝ : Group N
h : Covariant N N (fun x1 x2 ↦ x1 * x2) r
a b c : N
bc : r ((fun x1 x2 ↦ x1 * x2) a b) ((fun x1 x2 ↦ x1 * x2) a c)
⊢ r (a⁻¹ * (a * b)) (a⁻¹ * (a * c))
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs

Goal state before:
pp: case refine_2
N : Type u_2
r : N → N → Prop
inst✝ : Group N
h : Contravariant N N (fun x1 x2 ↦ x1 * x2) r
a b c : N
bc : r (a⁻¹ * (a * b)) c
⊢ r ((fun x1 x2 ↦ x1 * x2) a b) ((fun x1 x2 ↦ x1 * x2) a c)

Tactic:
← inv_mul_cancel_left a c

Goal state after:
case refine_2
N : Type u_2
r : N → N → Prop
inst✝ : Group N
h : Contravariant N N (fun x1 x2 ↦ x1 * x2) r
a b c : N
bc : r (a⁻¹ * (a * b)) (a⁻¹ * (a * c))
⊢ r ((fun x1 x2 ↦ x1 * x2) a b) ((fun x1 x2 ↦ x1 * x2) a c)
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) + b ^ (2 * k + 1)) * a ^ 2 + b ^ (2 * k + 3) = 0 + b ^ (2 * k + 1) * a ^ 2

Tactic:
by rw [ih, zero_mul, zero_add, zero_add, this, ← pow_add]

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

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

Tactic:
pow_one,

Goal state after:
α : Type u_2
inst✝¹ : Monoid α
inst✝ : HasDistribNeg α
c : ℕ
a : α
⊢ (a ^ 2) ^ c * -a = -((a ^ 2) ^ c * a)
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic

Goal state before:
pp: case inr.inr.inr.inl
α : Type u_1
inst✝³ : Mul α
inst✝² : LinearOrder α
a b c : α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
hca : c < a
h : a * b = c * b
⊢ a = c ∧ b = b ∨ a < c ∨ b < b

Tactic:
exact False.elim <| ne_of_lt (mul_lt_mul_left hca b) h.symm

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
a : α
⊢ a * a < 1 ↔ a < 1

Tactic:
contrapose!; exact one_le_mul_self_iff

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

Goal state before:
pp: M₀ : Type u_2
inst✝² : MonoidWithZero M₀
inst✝¹ : Preorder M₀
inst✝ : ZeroLEOneClass M₀
n : ℕ
⊢ 0 ^ (n + 1) ≤ 1

Tactic:
rw [zero_pow n.succ_ne_zero]

Goal state after:
M₀ : Type u_2
inst✝² : MonoidWithZero M₀
inst✝¹ : Preorder M₀
inst✝ : ZeroLEOneClass M₀
n : ℕ
⊢ 0 ≤ 1
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ↪r s
⊢ r = ⇑f ⁻¹'o s

Tactic:
by
  ext a b
  exact f.map_rel_iff.symm

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

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

Tactic:
rw [lt_mul_inv_iff₀ hc, mul_comm]

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

Goal state before:
pp: X : Type u_6
Y : Type u_7
F : Type u_8
inst✝² : LinearOrder X
inst✝¹ : Preorder Y
inst✝ : EquivLike F X Y
f : F
hf : StrictAnti ⇑f
⊢ DenselyOrdered X ↔ DenselyOrdered Y

Tactic:
rw [← denselyOrdered_orderDual]

Goal state after:
X : Type u_6
Y : Type u_7
F : Type u_8
inst✝² : LinearOrder X
inst✝¹ : Preorder Y
inst✝ : EquivLike F X Y
f : F
hf : StrictAnti ⇑f
⊢ DenselyOrdered Xᵒᵈ ↔ DenselyOrdered Y
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : Group α
a b : α
⊢ |(a / b)⁻¹|ₘ = |b / a|ₘ

Tactic:
inv_div

Goal state after:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : Group α
a b : α
⊢ |b / a|ₘ = |b / a|ₘ
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ ||a|ₘ / |b|ₘ|ₘ ≤ |a / b|ₘ

Tactic:
by
  rw [mabs, sup_le_iff]
  constructor
  · apply div_le_iff_le_mul.2
    convert! mabs_mul_le (a / b) b
    rw [div_mul_cancel]
  · rw [div_eq_mul_inv, mul_inv_rev, inv_inv, mul_inv_le_iff_le_mul, mabs_div_comm]
    convert! mabs_mul_le (b / a) a
    · rw [div_mul_cancel]

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
a b c : G
hac : a ≤ b
hcd : b ≤ c
d : G
h : b ≤ d
⊢ (b / d)⁻¹ ≤ max (c / d) (d / a)

Tactic:
inv_div

Goal state after:
case inr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b c : G
hac : a ≤ b
hcd : b ≤ c
d : G
h : b ≤ d
⊢ d / b ≤ max (c / d) (d / a)
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

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

Tactic:
sup_comm (b := _ / _),

Goal state after:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ b / a ⊔ (b / a)⁻¹ ⊔ 1 = |b / a|ₘ
Module: Mathlib.Data.Nat.Cast.NeZero

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

Tactic:
rintro rfl; exact h.out Nat.cast_zero

Goal state after: