mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.BinaryRec

Goal state before:
pp: case zero.false
⊢ bit false 0 = 0 ↔ 0 = 0 ∧ false = false

Tactic:
simp [bit, Nat.two_mul, ← Nat.add_assoc]

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

Goal state before:
pp: case zero.true
⊢ bit true 0 = 0 ↔ 0 = 0 ∧ true = false

Tactic:
simp [bit, Nat.two_mul, ← Nat.add_assoc]

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

Goal state before:
pp: case succ.false
n✝ : Nat
⊢ bit false (n✝ + 1) = 0 ↔ n✝ + 1 = 0 ∧ false = false

Tactic:
simp [bit, Nat.two_mul, ← Nat.add_assoc]

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

Goal state before:
pp: case succ.true
n✝ : Nat
⊢ bit true (n✝ + 1) = 0 ↔ n✝ + 1 = 0 ∧ true = false

Tactic:
simp [bit, Nat.two_mul, ← Nat.add_assoc]

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

Goal state before:
pp: α : Sort u_1
f : α → α
⊢ (Std.Symm fun x1 x2 ↦ f x1 = x2) ↔ Involutive f

Tactic:
by
  simp [symm_def, Involutive]

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ζ : Type u_6
r : α → β → Prop
f₁ : α → γ
g₁ : β → δ
f₂ : γ → ε
g₂ : δ → ζ
⊢ Relation.Map (Relation.Map r f₁ g₁) f₂ g₂ = Relation.Map r (f₂ ∘ f₁) (g₂ ∘ g₁)

Tactic:
grind [Relation.Map]

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
f : α → β
⊢ r ≤ (Relation.Map r f f on f)

Tactic:
grind [Relation.Map]

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
r : β → β → Prop
f : α → β
⊢ Relation.Map (r on f) f f ≤ r

Tactic:
grind [Relation.Map]

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
r : β → β → Prop
f : α → β
hsurj : Surjective f
x y : β
x✝¹ : ∃ a, f a = x
x✝ : ∃ a, f a = y
⊢ Relation.Map (r on f) f f x y ↔ r x y

Tactic:
grind [Relation.Map]

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
f : α → β
⊢ Relation.Map (Relation.Map r f f on f) f f = Relation.Map r f f

Tactic:
grind [Relation.Map]

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
r : β → β → Prop
f : α → β
⊢ (Relation.Map (r on f) f f on f) = (r on f)

Tactic:
grind [Relation.Map]

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
r : β → β → Prop
f : α → β
a₁ a₂ : α
⊢ Relation.Map (r on f) f f (f a₁) (f a₂) ↔ r (f a₁) (f a₂)

Tactic:
grind [Relation.Map]

Goal state after:
Module: Mathlib.Data.Quot

Goal state before:
pp: α : Sort u_1
s : Setoid α
x : α
y : Quotient s
⊢ ⟦x⟧ = y ↔ x ≈ y.out

Tactic:
refine Iff.trans ?_ Quotient.eq

Goal state after:
α : Sort u_1
s : Setoid α
x : α
y : Quotient s
⊢ ⟦x⟧ = y ↔ ⟦x⟧ = ⟦y.out⟧
Module: Mathlib.Data.Quot

Goal state before:
pp: α : Sort u_1
s : Setoid α
x : Quotient s
y : α
⊢ x = ⟦y⟧ ↔ x.out ≈ y

Tactic:
refine Iff.trans ?_ Quotient.eq

Goal state after:
α : Sort u_1
s : Setoid α
x : Quotient s
y : α
⊢ x = ⟦y⟧ ↔ ⟦x.out⟧ = ⟦y⟧
Module: Mathlib.Algebra.Opposites

Goal state before:
pp: α : Type u_1
inst✝ : Add α
⊢ IsLeftCancelAdd αᵐᵒᵖ ∧ IsRightCancelAdd αᵐᵒᵖ ↔ IsLeftCancelAdd α ∧ IsRightCancelAdd α

Tactic:
isLeftCancelAdd_iff,

Goal state after:
α : Type u_1
inst✝ : Add α
⊢ IsLeftCancelAdd α ∧ IsRightCancelAdd αᵐᵒᵖ ↔ IsLeftCancelAdd α ∧ IsRightCancelAdd α
Module: Mathlib.Logic.Function.Iterate

Goal state before:
pp: α : Type u
f : α → α
m n : ℕ
a : α
hf : Injective f
ha : f^[m] a = f^[n] a
h : n ≤ m
⊢ f^[m - n + ?m.30] a = f^[?m.30] a

Tactic:
rwa [Nat.sub_add_cancel h]

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

Goal state before:
pp: case refine_1
R : Type u_4
A : Type u_5
inst✝² : MulOneClass A
inst✝¹ : SMul R A
inst✝ : IsScalarTower R A A
x✝ : FaithfulSMul R A
r₁ r₂ : R
hr : r₁ • 1 = r₂ • 1
h : ∀ {m₁ m₂ : R}, (∀ (a : A), m₁ • a = m₂ • a) → m₁ = m₂
a : A
⊢ r₁ • a = r₂ • a

Tactic:
← one_mul a,

Goal state after:
case refine_1
R : Type u_4
A : Type u_5
inst✝² : MulOneClass A
inst✝¹ : SMul R A
inst✝ : IsScalarTower R A A
x✝ : FaithfulSMul R A
r₁ r₂ : R
hr : r₁ • 1 = r₂ • 1
h : ∀ {m₁ m₂ : R}, (∀ (a : A), m₁ • a = m₂ • a) → m₁ = m₂
a : A
⊢ r₁ • (1 * a) = r₂ • (1 * a)
Module: Mathlib.Data.Nat.Basic

Goal state before:
pp: case refl
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Injective next
x y : C n
H : leRecOn ⋯ (fun {k} ↦ next) x = leRecOn ⋯ (fun {k} ↦ next) y
⊢ x = y

Tactic:
rwa [leRecOn_self, leRecOn_self] at H

Goal state after:
Module: Mathlib.Order.PropInstances

Goal state before:
pp: p q : Prop
⊢ p ≤ q ∨ q ≤ p

Tactic:
by by_cases h : q <;> simp [h]

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

Goal state before:
pp: case a
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
a₁ a₂ : α
h_anti : Antitone f
h_fa : f a₁ = f a₂
i : α
h₁ : a₁ ≤ i
h₂ : i ≤ a₂
⊢ f a₂ ≤ f i

Tactic:
exact h_anti h₂

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

Goal state before:
pp: α : Type u
s : Set α
p : α → Prop
⊢ {x | x ∈ s ∧ p x} = s ↔ ∀ (x : α), x ∈ s → p x

Tactic:
simp_rw [Set.ext_iff, mem_sep_iff, and_iff_left_iff_imp]

Goal state after:
Module: Mathlib.Order.Lattice

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

Tactic:
by
  rw [sup_assoc, sup_assoc, sup_comm b]

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst✝¹ : LinearOrder α
inst✝ : SemilatticeSup β
hf : MonotoneOn f s
hx : x ∈ s
hy : y ∈ s
⊢ f (max x y) = f x ⊔ f y

Tactic:
cases le_total x y

Goal state after:
case inl
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst✝¹ : LinearOrder α
inst✝ : SemilatticeSup β
hf : MonotoneOn f s
hx : x ∈ s
hy : y ∈ s
h✝ : x ≤ y
⊢ f (max x y) = f x ⊔ f y

case inr
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst✝¹ : LinearOrder α
inst✝ : SemilatticeSup β
hf : MonotoneOn f s
hx : x ∈ s
hy : y ∈ s
h✝ : y ≤ x
⊢ f (max x y) = f x ⊔ f y
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst✝¹ : LinearOrder α
inst✝ : SemilatticeInf β
hf : AntitoneOn f s
hx : x ∈ s
hy : y ∈ s
⊢ f (max x y) = f x ⊓ f y

Tactic:
cases le_total x y

Goal state after:
case inl
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst✝¹ : LinearOrder α
inst✝ : SemilatticeInf β
hf : AntitoneOn f s
hx : x ∈ s
hy : y ∈ s
h✝ : x ≤ y
⊢ f (max x y) = f x ⊓ f y

case inr
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst✝¹ : LinearOrder α
inst✝ : SemilatticeInf β
hf : AntitoneOn f s
hx : x ∈ s
hy : y ∈ s
h✝ : y ≤ x
⊢ f (max x y) = f x ⊓ f y
Module: Mathlib.Data.Set.Subsingleton

Goal state before:
pp: α : Type u
s : Set α
⊢ Nontrivial ↑s ↔ s.Nontrivial

Tactic:
simp [← nontrivial_univ_iff, Set.Nontrivial]

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

Goal state before:
pp: α : Type u_1
β : α → Type u_4
γ : (a : α) → β a → Type u_7
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
f : (i : (a : α) × β a) → γ i.fst i.snd
ia : α
ib : β ia
x : γ ⟨ia, ib⟩.fst ⟨ia, ib⟩.snd
⊢ curry (update f ⟨ia, ib⟩ x) = update (curry f) ⟨ia, ib⟩.fst (update (curry f ⟨ia, ib⟩.fst) ⟨ia, ib⟩.snd x)

Tactic:
ext ja jb

Goal state after:
α : Type u_1
β : α → Type u_4
γ : (a : α) → β a → Type u_7
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
f : (i : (a : α) × β a) → γ i.fst i.snd
ia : α
ib : β ia
x : γ ⟨ia, ib⟩.fst ⟨ia, ib⟩.snd
ja : α
jb : β ja
⊢ curry (update f ⟨ia, ib⟩ x) ja jb = update (curry f) ⟨ia, ib⟩.fst (update (curry f ⟨ia, ib⟩.fst) ⟨ia, ib⟩.snd x) ja jb
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
hs : s.Nonempty
t : Set β
a : β
⊢ s ⊆ (fun x ↦ a) ⁻¹' t ↔ a ∈ t

Tactic:
← image_subset_iff,

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
hs : s.Nonempty
t : Set β
a : β
⊢ (fun x ↦ a) '' s ⊆ t ↔ a ∈ t
Module: Mathlib.Data.Set.Image

Goal state before:
pp: case inl
α : Type u_1
s : Set α
σ : Equiv.Perm α
hs : {a | σ a ≠ a} ⊆ s
i : α
hi : σ i = i
j : α
hj : j ∈ s
h : σ j = i
⊢ i ∈ s

Tactic:
rwa [σ.injective (hi.trans h.symm)]

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

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

Tactic:
← image_subset_iff,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ f '' univ ⊆ s ↔ range f ⊆ s
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_5
β : Type u_6
γ : Type u_7
γ' : Type u_8
δ : Type u_9
δ' : Type u_10
h : β → α
f : γ → β
f₁ : γ' → α
f₂ : γ → γ'
g : δ → β
g₁ : δ' → α
g₂ : δ → δ'
hf : h ∘ f = f₁ ∘ f₂
hg : h ∘ g = g₁ ∘ g₂
hfg : range f ∪ range g = univ
s : Set β
⊢ h '' s = f₁ '' f₂ '' f ⁻¹' s ∪ g₁ '' g₂ '' g ⁻¹' s

Tactic:
rw [← image_comp, ← image_comp, ← hf, ← hg, image_comp, image_comp, image_preimage_eq_inter_range,
    image_preimage_eq_inter_range, ← image_union, ← inter_union_distrib_left, hfg, inter_univ]

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
f : ι' ≃ ι
s : Set ι'
t : (i : ι) → Set (α i)
⊢ ∀ (x : (a : ι') → α (f a)), x ∈ ⇑(piCongrLeft α f) ⁻¹' (⇑f '' s).pi t ↔ x ∈ s.pi fun i ↦ t (f i)

Tactic:
← (f.piCongrLeft α).symm.forall_congr_right

Goal state after:
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
f : ι' ≃ ι
s : Set ι'
t : (i : ι) → Set (α i)
⊢ ∀ (a : (b : ι) → α b),
    (piCongrLeft α f).symm a ∈ ⇑(piCongrLeft α f) ⁻¹' (⇑f '' s).pi t ↔ (piCongrLeft α f).symm a ∈ s.pi fun i ↦ t (f i)
Module: Mathlib.Algebra.Group.Torsion

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
inst✝ : IsMulTorsionFree M
n : ℕ
a : M
⊢ a ^ n = 1 ↔ a = 1 ∨ n = 0

Tactic:
obtain rfl | hn := eq_or_ne n 0 <;> simp [pow_eq_one_iff_left, *]

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

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)
⊢ Disjoint s r

Tactic:
and_iff_right hbij.injOn

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 : α), 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.Algebra.Group.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a : α
m n : ℤ
⊢ a ^ (m * n) = (a ^ n) ^ m

Tactic:
zpow_mul'

Goal state after:
α : Type u_1
inst✝ : DivisionMonoid α
a : α
m n : ℤ
⊢ (a ^ n) ^ m = (a ^ n) ^ m
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: case pred
G : Type u_3
inst✝ : Group G
g : G
P : G → Prop
h_one : P 1
h_mul : ∀ (a : G), P a → P (a * g)
h_inv : ∀ (a : G), P a → P (a * g⁻¹)
n : ℕ
ih : P (g ^ (-↑n))
⊢ P (g ^ (-↑n - 1))

Tactic:
rw [zpow_sub_one]

Goal state after:
case pred
G : Type u_3
inst✝ : Group G
g : G
P : G → Prop
h_one : P 1
h_mul : ∀ (a : G), P a → P (a * g)
h_inv : ∀ (a : G), P a → P (a * g⁻¹)
n : ℕ
ih : P (g ^ (-↑n))
⊢ P (g ^ (-↑n) * g⁻¹)
Module: Mathlib.Control.Basic

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

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

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

Goal state before:
pp: α : Type u_4
inst✝ : DecidableEq α
i j : α
σ : Perm α
⊢ swap i j * σ = σ ↔ i = j

Tactic:
rw [mul_eq_right, swap_eq_one_iff]

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

Goal state before:
pp: case succ
M₀ : Type u_1
G₀ : Type u_2
inst✝¹ : MonoidWithZero M₀
a✝ : M₀
n✝ : ℕ
inst✝ : NoZeroDivisors M₀
a : M₀
x✝ : IsNilpotent a
n : ℕ
ih : a ^ n = 0 → a = 0
ha : a ^ (n + 1) = 0
⊢ a = 0

Tactic:
rw [pow_succ, mul_eq_zero] at ha

Goal state after:
case succ
M₀ : Type u_1
G₀ : Type u_2
inst✝¹ : MonoidWithZero M₀
a✝ : M₀
n✝ : ℕ
inst✝ : NoZeroDivisors M₀
a : M₀
x✝ : IsNilpotent a
n : ℕ
ih : a ^ n = 0 → a = 0
ha : a ^ n = 0 ∨ a = 0
⊢ a = 0
Module: Mathlib.Algebra.GroupWithZero.Hom

Goal state before:
pp: M₀ : Type u_7
N₀ : Type u_8
inst✝⁵ : MulZeroOneClass M₀
inst✝⁴ : MulZeroOneClass N₀
inst✝³ : DecidablePred fun x ↦ x = 0
inst✝² : Nontrivial M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial N₀
x : M₀
⊢ 1 x = 0 ↔ x = 0

Tactic:
by
  rcases eq_or_ne x 0 with rfl | hx <;> simp_all [one_apply_of_ne_zero]

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

Goal state before:
pp: M₀ : Type u_7
N₀ : Type u_8
inst✝⁵ : MulZeroOneClass M₀
inst✝⁴ : MulZeroOneClass N₀
inst✝³ : DecidablePred fun x ↦ x = 0
inst✝² : Nontrivial M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial N₀
x : M₀
⊢ 1 x = 1 ↔ x ≠ 0

Tactic:
by
  rcases eq_or_ne x 0 with rfl | hx <;> simp_all [one_apply_of_ne_zero]

Goal state after:
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:
· rw [zero_zpow _ h]

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

Goal state before:
pp: case succ.succ
R : Type u_1
inst✝ : AddGroupWithOne R
H : ∀ (n : ℕ), ↑n = 0 → n = 0
m : ℕ
ih : ∀ (n : ℕ), ↑m = ↑n → m = n
n✝ : ℕ
h : ↑(m + 1) = ↑(n✝ + 1)
⊢ m + 1 = n✝ + 1

Tactic:
· simp only [Nat.cast_succ, add_right_cancel_iff] at h; rwa [ih]

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

Goal state before:
pp: α : Type u_2
inst✝ : Monoid α
n : ℕ
hn : Even n
⊢ ∀ (a : α), IsSquare (a ^ n)

Tactic:
aesop (add simp pow_add)

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

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

Tactic:
by rw [one_div_neg_one_eq_neg_one]

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 / -a = b * (-a)⁻¹

Tactic:
division_def

Goal state after:
R : Type u_1
inst✝¹ : DivisionMonoid R
inst✝ : HasDistribNeg R
a b : R
⊢ b * (-a)⁻¹ = b * (-a)⁻¹
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
a b c d : G₀
hc : c ≠ 0
hd : d ≠ 0
h : a / b = c / d
⊢ b ≠ 0

Tactic:
by
    intro hb
    rw [hb, div_zero] at h
    exact div_ne_zero hc hd h.symm

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

Goal state before:
pp: case zero
α : Type u_1
inst✝ : NonAssocSemiring α
x : α
⊢ Commute 0 x

Tactic:
exact Commute.zero_left x

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

Goal state before:
pp: α : Type u_2
inst✝¹ : Semiring α
a b : α
n : ℕ
inst✝ : IsCancelAdd α
hn : Odd n
hab : a + b = 0
⊢ a ^ n + b ^ n = 0

Tactic:
obtain ⟨k, rfl⟩ := hn
  induction k with | zero => simpa | succ k ih => ?_
  have : a ^ 2 = b ^ 2 := add_right_cancel <|
    calc
      a ^ 2 + a * b = 0 := by rw [sq, ← mul_add, hab, mul_zero]
      _ = b ^ 2 + a * b := by rw [sq, ← add_mul, add_comm, hab, zero_mul]
  refine add_right_cancel (b := b ^ (2 * k + 1) * a ^ 2) ?_
  calc
    _ = (a ^ (2 * k + 1) + b ^ (2 * k + 1)) * a ^ 2 + b ^ (2 * k + 3) := by
      rw [add_mul, ← pow_add, add_right_comm]; rfl
    _ = _ := by rw [ih, zero_mul, zero_add, zero_add, this, ← pow_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 d : R
inst✝³ : ExistsAddOfLE R
inst✝² : MulPosMono R
inst✝¹ : AddLeftMono R
inst✝ : AddLeftReflectLE R
hba : b ≤ a
hdc : d ≤ c
⊢ a * d + b * c ≤ a * c + b * d

Tactic:
rw [add_comm (a * d), add_comm (a * c)]

Goal state after:
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : PartialOrder R
a b c d : R
inst✝³ : ExistsAddOfLE R
inst✝² : MulPosMono R
inst✝¹ : AddLeftMono R
inst✝ : AddLeftReflectLE R
hba : b ≤ a
hdc : d ≤ c
⊢ b * c + a * d ≤ b * d + a * c
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
hba : b < a
hdc : d < c
⊢ a * d + b * c < a * c + b * d

Tactic:
rw [add_comm (a * d), add_comm (a * c)]

Goal state after:
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
hba : b < a
hdc : d < c
⊢ b * c + a * d < b * d + a * c
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a : G₀
ha : 0 < a
⊢ a⁻¹ < 1 ↔ 1 < a

Tactic:
by simpa using inv_mul_lt_one₀ ha (b := 1)

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

Goal state before:
pp: case mp
R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : ExistsAddOfLE R
inst✝³ : PosMulStrictMono R
inst✝² : MulPosStrictMono R
inst✝¹ : AddLeftStrictMono R
inst✝ : AddLeftReflectLT R
h : 0 < 0 * 0
⊢ False

Tactic:
rw [mul_zero] at h

Goal state after:
case mp
R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : ExistsAddOfLE R
inst✝³ : PosMulStrictMono R
inst✝² : MulPosStrictMono R
inst✝¹ : AddLeftStrictMono R
inst✝ : AddLeftReflectLT R
h : 0 < 0
⊢ False
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:
· exact sq_eq_zero_iff

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:
le_div_iff₀ hc,

Goal state after:
G₀ : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ a * c ≤ b ↔ c * a ≤ b
Module: Mathlib.Order.RelIso.Basic

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

Tactic:
constructor
  · exact RelHomClass.wellFounded (Quotient.mkRelHom H)
  · refine fun wf => ⟨fun q => ?_⟩
    obtain ⟨a, rfl⟩ := q.exists_rep
    exact acc_lift₂_iff.2 (wf.apply a)

Goal state after:
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:
by
  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.Data.Int.GCD

Goal state before:
pp: x y : ℕ
⊢ ↑(x.gcd y) = ↑x * x.gcdA y + ↑y * x.gcdB y

Tactic:
have := @xgcdAux_P x y x y 1 0 0 1 (by simp [P]) (by simp [P])
  rwa [xgcdAux_val, xgcd_val] at this

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

Goal state before:
pp: case refine_2
k n : ℕ
hk : n.gcd k < k
hk' : ↑k ≠ 0
key : n.gcd k = (↑n * n.gcdA k % ↑k).toNat
⊢ ↑n % ↑k * (n.gcdA k % ↑k) % ↑k = ↑n * n.gcdA k % ↑k

Tactic:
← Int.mul_emod

Goal state after:
case refine_2
k n : ℕ
hk : n.gcd k < k
hk' : ↑k ≠ 0
key : n.gcd k = (↑n * n.gcdA k % ↑k).toNat
⊢ ↑n * n.gcdA k % ↑k = ↑n * n.gcdA k % ↑k
Module: Mathlib.Algebra.Regular.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Monoid R
a : R
n : ℕ
rla : IsLeftRegular a
⊢ IsLeftRegular (a ^ n)

Tactic:
by
  simp only [IsLeftRegular, ← mul_left_iterate, rla.iterate n]

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 : α
ha : AddLECancellable a
h₁ : b < a
h₂ : 0 < b
h : a - b = a
⊢ False

Tactic:
exact h₂.not_ge (ha.add_le_iff_nonpos_left.1 <| add_le_of_le_tsub_left_of_le h₁.le h.ge)

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

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
n : ℤ
hx : |x| ≤ 1
hnx : 0 < n → 0 ≤ x + ↑n
hnx' : n < 0 → x + ↑n ≤ 0
⊢ 0 ≤ ↑n ∧ 0 ≤ x + ↑n ∨ ↑n ≤ 0 ∧ x + ↑n ≤ 0

Tactic:
rcases lt_trichotomy n 0 with (h | rfl | h)

Goal state after:
case inl
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
n : ℤ
hx : |x| ≤ 1
hnx : 0 < n → 0 ≤ x + ↑n
hnx' : n < 0 → x + ↑n ≤ 0
h : n < 0
⊢ 0 ≤ ↑n ∧ 0 ≤ x + ↑n ∨ ↑n ≤ 0 ∧ x + ↑n ≤ 0

case inr.inl
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
hx : |x| ≤ 1
hnx : 0 < 0 → 0 ≤ x + ↑0
hnx' : 0 < 0 → x + ↑0 ≤ 0
⊢ 0 ≤ ↑0 ∧ 0 ≤ x + ↑0 ∨ ↑0 ≤ 0 ∧ x + ↑0 ≤ 0

case inr.inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
n : ℤ
hx : |x| ≤ 1
hnx : 0 < n → 0 ≤ x + ↑n
hnx' : n < 0 → x + ↑n ≤ 0
h : 0 < n
⊢ 0 ≤ ↑n ∧ 0 ≤ x + ↑n ∨ ↑n ≤ 0 ∧ x + ↑n ≤ 0
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: case refine_3.inr
α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
x✝ : Nontrivial αˣ ∧ DenselyOrdered αˣ
H₁ : Nontrivial αˣ
H₂ : DenselyOrdered αˣ
y x : αˣ
h : ↑x < ↑y
hx : 0 < ↑x
⊢ ∃ a, ↑x < a ∧ a < ↑y

Tactic:
obtain ⟨z, hz, hz'⟩ := H₂.dense x y (Units.val_lt_val.mpr h)

Goal state after:
case refine_3.inr
α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
x✝ : Nontrivial αˣ ∧ DenselyOrdered αˣ
H₁ : Nontrivial αˣ
H₂ : DenselyOrdered αˣ
y x : αˣ
h : ↑x < ↑y
hx : 0 < ↑x
z : αˣ
hz : x < z
hz' : z < y
⊢ ∃ a, ↑x < a ∧ a < ↑y
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
x y : WithZero α
a b : α
inst✝¹ : Mul α
inst✝ : MulLeftMono α
⊢ MulLeftMono (WithZero α)

Tactic:
by
  refine ⟨fun a b c hbc => ?_⟩
  induction a; · exact zero_le
  induction b; · exact zero_le
  rcases WithZero.coe_le_iff.1 hbc with ⟨c, rfl, hbc'⟩
  rw [← coe_mul _ c, ← coe_mul, coe_le_coe]
  exact mul_le_mul_right hbc' _

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
inst✝ : IsStrictOrderedRing R
n a : ℕ
⊢ a ≤ ⌊↑n⌋₊ ↔ a ≤ n

Tactic:
le_floor_iff,

Goal state after:
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
n a : ℕ
⊢ ↑a ≤ ↑n ↔ a ≤ n

R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
n a : ℕ
⊢ 0 ≤ ↑n
Module: Mathlib.Order.Directed

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
⊢ DirectedOn r s ↔ Directed r Subtype.val

Tactic:
simp only [DirectedOn, Directed, Subtype.exists, exists_and_left, exists_prop, Subtype.forall]
  exact forall₂_congr fun x _ => by simp [And.comm, and_assoc]

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
inst✝³ : IsStrictOrderedRing R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : ExistsAddOfLE R
a : R
n : ℕ
hna : ↑n ≤ a
⊢ ⌈a - ↑n⌉₊ = ⌈a⌉₊ - n

Tactic:
refine eq_tsub_of_add_eq ?_

Goal state after:
case inr
R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : FloorSemiring R
inst✝³ : IsStrictOrderedRing R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : ExistsAddOfLE R
a : R
n : ℕ
hna : ↑n ≤ a
⊢ ⌈a - ↑n⌉₊ + n = ⌈a⌉₊
Module: Mathlib.Algebra.Ring.Invertible

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : Invertible 2
⊢ 2 * (1 - ⅟2) = 2 * ⅟2

Tactic:
by
    rw [mul_sub, mul_invOf_self, mul_one, ← one_add_one_eq_two, add_sub_cancel_right]

Goal state after: