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

Goal state before:
pp: b : Bool
n : Nat
⊢ bit b n / 2 = n

Tactic:
bit_val,

Goal state after:
b : Bool
n : Nat
⊢ (2 * n + b.toNat) / 2 = n
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: R : Type u_2
inst✝ : Mul R
⊢ ((∀ (a : R), IsLeftRegular a) ∧ ∀ (a : R), IsRightRegular a) ↔ ∀ (r : R), IsRegular r

Tactic:
← forall_and

Goal state after:
R : Type u_2
inst✝ : Mul R
⊢ (∀ (x : R), IsLeftRegular x ∧ IsRightRegular x) ↔ ∀ (r : R), IsRegular r
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: ⊢ @npowRecAuto = @npowBinRecAuto

Tactic:
funext M _ _ k m

Goal state after:
M : Type u_2
x✝¹ : Semigroup M
x✝ : One M
k : ℕ
m : M
⊢ npowRecAuto k m = npowBinRecAuto k m
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
a : M
m n : ℕ
⊢ a ^ (m * n) * a ^ m = (a ^ m) ^ n * a ^ m

Tactic:
pow_mul

Goal state after:
M : Type u_2
inst✝ : Monoid M
a : M
m n : ℕ
⊢ (a ^ m) ^ n * a ^ m = (a ^ m) ^ n * a ^ m
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
a : M
m n : ℕ
⊢ a ^ (n * m) = (a ^ n) ^ m

Tactic:
pow_mul

Goal state after:
M : Type u_2
inst✝ : Monoid M
a : M
m n : ℕ
⊢ (a ^ n) ^ m = (a ^ n) ^ m
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: G : Type u_2
inst✝ : SubNegMonoid G
a : G
n : ℕ
⊢ Int.negSucc n • a = -((n + 1) • a)

Tactic:
by
  rw [← natCast_zsmul]
  exact SubNegMonoid.zsmul_neg' n a

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

Goal state before:
pp: α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : γ → α
I : Injective (f ∘ g)
hg : Surjective g
x y : α
h : f x = f y
⊢ x = y

Tactic:
obtain ⟨x, rfl⟩ := hg x
  obtain ⟨y, rfl⟩ := hg y
  exact congr_arg g (I h)

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a b : α
h : ∀ (b : α), ¬r a b
⊢ ReflTransGen r a b ↔ b = a

Tactic:
by
  rw [cases_head_iff]; simp [h, eq_comm]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
ga : α → α → α
gb : β → β → β
inst✝ : Std.IdempotentOp gb
h : Semiconj₂ f ga gb
h_inj : Injective f
x : α
⊢ f (ga x x) = f x

Tactic:
rw [h.eq, Std.IdempotentOp.idempotent (op := gb)]

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

Goal state before:
pp: α : Type u_4
β : Type u_5
R : α → β → Prop
inst✝ : IsEmpty α
⊢ RightTotal R ↔ IsEmpty β

Tactic:
simp only [RightTotal, IsEmpty.exists_iff, isEmpty_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Nonempty α
inst✝ : Nonempty β
f : α → γ
g : β → δ
h : Injective (map f g)
a₁ a₂ : α
ha : f a₁ = f a₂
⊢ a₁ = a₂

Tactic:
inhabit β
      injection
        @h (a₁, default) (a₂, default) (congr_arg (fun c : γ => Prod.mk c (g default)) ha :)

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
inst✝ : PartialOrder α
f : α → α → α
comm : Std.Commutative f
assoc : ∀ (a b c : α), f (f a b) c ≤ f a (f b c)
a b c : α
⊢ f a (f b c) ≤ f (f a b) c

Tactic:
rw [comm.comm, comm.comm b, comm.comm _ c, comm.comm a]
      exact assoc ..

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

Goal state before:
pp: f : Bool → Bool
x : Bool
⊢ f (f (f x)) = f x

Tactic:
cases h₁ : f true

Goal state after:
case false
f : Bool → Bool
x : Bool
h₁ : f true = false
⊢ f (f (f x)) = f x

case true
f : Bool → Bool
x : Bool
h₁ : f true = true
⊢ f (f (f x)) = f x
Module: Mathlib.Data.Nat.Basic

Goal state before:
pp: n m : ℕ
⊢ n ∣ n - m ↔ m = 0 ∨ n ≤ m

Tactic:
by
  rcases le_or_gt n m with h | h
  · simp [h]
  · rcases eq_or_ne m 0 with rfl | hm
    · simp
    · simp only [hm, h.not_ge, or_self, iff_false]
      refine not_dvd_of_pos_of_lt ?_ ?_ <;>
      grind

Goal state after:
Module: Mathlib.Order.Compare

Goal state before:
pp: case inr.inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, o.Compares a b → o.Compares a' b'
o : Ordering
ho : o.Compares a' b'
hab : a = b
⊢ o.Compares a b

pp: case inr.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, o.Compares a b → o.Compares a' b'
o : Ordering
ho : o.Compares a' b'
hab : b < a
⊢ o.Compares a b

Tactic:
· have hab : Compares Ordering.eq a b := hab
    rwa [ho.inj (h hab)]

Goal state after:
case inr.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, o.Compares a b → o.Compares a' b'
o : Ordering
ho : o.Compares a' b'
hab : b < a
⊢ o.Compares a b
Module: Mathlib.Order.PropInstances

Goal state before:
pp: ι : Type u_1
α' : ι → Type u_3
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → BoundedOrder (α' i)
f g : (i : ι) → α' i
⊢ IsCompl f g ↔ ∀ (i : ι), IsCompl (f i) (g i)

Tactic:
by
  simp_rw [_root_.isCompl_iff, disjoint_iff, codisjoint_iff, forall_and]

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:
· rw [h_fa]; exact h_anti h₂

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a b c : α
hab : Disjoint a b
hbc : Codisjoint b c
⊢ a ≤ c

Tactic:
rw [← @inf_top_eq _ _ _ a, ← @bot_sup_eq _ _ _ c, ← hab.eq_bot, ← hbc.eq_top, sup_inf_right]
  exact inf_le_inf_right _ le_sup_left

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

Goal state before:
pp: P : ℕ → Prop
h : ∀ (N : ℕ), ∃ n, n > N ∧ P n
this : NoMaxOrder { n // P n }
⊢ ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), P (φ n)

Tactic:
obtain ⟨f, hf, _⟩ := Nat.exists_strictMono' (⟨(h 0).choose, (h 0).choose_spec.2⟩ : {n // P n})

Goal state after:
P : ℕ → Prop
h : ∀ (N : ℕ), ∃ n, n > N ∧ P n
this : NoMaxOrder { n // P n }
f : ℕ → { n // P n }
hf : StrictMono f
right✝ : f 0 = ⟨⋯.choose, ⋯⟩
⊢ ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), P (φ n)
Module: Mathlib.Data.Set.Disjoint

Goal state before:
pp: α : Type u_1
s t : Set α
h : Disjoint s t
x : α
⊢ x ∈ s ∪ t ↔ Xor (x ∈ s) (x ∈ t)

Tactic:
by
  grind [Xor]

Goal state after:
Module: Mathlib.Control.EquivFunctor

Goal state before:
pp: f : Type u₀ → Type u₁
inst✝ : EquivFunctor f
α β : Type u₀
e : α ≃ β
y : f β
⊢ map e (map e.symm y) = y

Tactic:
by
    convert! (congr_fun (EquivFunctor.map_trans' e.symm e) y).symm
    simp

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

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

Tactic:
← inf_comm x y,

Goal state after:
α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ y ⊓ x \ y ⊔ x ⊓ y \ x ⊓ x \ y = x ⊓ y \ x ⊓ x \ y
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁶ : Max α
inst✝⁵ : Min α
inst✝⁴ : LE α
inst✝³ : LT α
inst✝² : Bot α
inst✝¹ : SDiff α
inst✝ : GeneralizedCoheytingAlgebra β
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_bot : f ⊥ = ⊥
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
a : α
⊢ f ⊥ ≤ f a

Tactic:
map_bot

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁶ : Max α
inst✝⁵ : Min α
inst✝⁴ : LE α
inst✝³ : LT α
inst✝² : Bot α
inst✝¹ : SDiff α
inst✝ : GeneralizedCoheytingAlgebra β
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_bot : f ⊥ = ⊥
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
a : α
⊢ ⊥ ≤ f a
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁸ : Max α
inst✝⁷ : Min α
inst✝⁶ : LE α
inst✝⁵ : LT α
inst✝⁴ : Top α
inst✝³ : Bot α
inst✝² : Compl α
inst✝¹ : HImp α
inst✝ : HeytingAlgebra β
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_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
a : α
⊢ f ⊥ ≤ f a

Tactic:
map_bot

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁸ : Max α
inst✝⁷ : Min α
inst✝⁶ : LE α
inst✝⁵ : LT α
inst✝⁴ : Top α
inst✝³ : Bot α
inst✝² : Compl α
inst✝¹ : HImp α
inst✝ : HeytingAlgebra β
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_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
a : α
⊢ ⊥ ≤ f a
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x y z : α
inst✝ : BooleanAlgebra α
⊢ x ⇨ y ≤ z ↔ y ≤ z ∧ Codisjoint x z

Tactic:
rw [himp_eq, sup_le_iff, and_congr_right_iff]

Goal state after:
α : Type u
x y z : α
inst✝ : BooleanAlgebra α
⊢ y ≤ z → (xᶜ ≤ z ↔ Codisjoint x z)
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✝² : Bot α
inst✝¹ : SDiff α
inst✝ : GeneralizedBooleanAlgebra β
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_bot : f ⊥ = ⊥
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
a b : α
⊢ ⊥ = f ⊥

Tactic:
map_bot

Goal state after:
α : Type u
β : Type u_1
x y z : α
inst✝⁶ : Max α
inst✝⁵ : Min α
inst✝⁴ : LE α
inst✝³ : LT α
inst✝² : Bot α
inst✝¹ : SDiff α
inst✝ : GeneralizedBooleanAlgebra β
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_bot : f ⊥ = ⊥
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
a b : α
⊢ ⊥ = ⊥
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: case refine_1
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ a ≤ a \ b ⊔ b \ a ⊔ b

Tactic:
rw [sup_right_comm]
    exact le_sup_of_le_left le_sdiff_sup

Goal state after:
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 ⊥

Tactic:
map_bot

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 : α
⊢ ⊥ = ⊥
Module: Mathlib.Data.Set.Restrict

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : MapsTo f s t
h' : Surjective (restrict f s t h)
b : β
hb : b ∈ t
a : α
ha : a ∈ s
ha' : restrict f s t h ⟨a, ha⟩ = ⟨b, hb⟩
⊢ f a = b

Tactic:
simpa [Subtype.ext_iff] using ha'

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ f ⁻¹' f '' f ⁻¹' s = f ⁻¹' s

Tactic:
by
  rw [image_preimage_eq_range_inter, preimage_range_inter]

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)
hs : s.Nonempty
⊢ EqOn g g' t

Tactic:
by
  obtain ⟨x, hxs⟩ := hs
  intro x hxt
  have h' := h <| mk_mem_prod hxs hxt
  grind

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
hβ : Nonempty β
f : α → β
hf : f ∈ {f | ∀ (x y : α), f x = f y}
h : IsEmpty α
⊢ ∃ a, const α a = f

pp: case inr
α : Type u_1
β : Type u_2
hβ : Nonempty β
f : α → β
hf : f ∈ {f | ∀ (x y : α), f x = f y}
a : α
⊢ ∃ a, const α a = f

Tactic:
· exact hβ.elim fun b ↦ ⟨b, Subsingleton.elim _ _⟩

Goal state after:
case inr
α : Type u_1
β : Type u_2
hβ : Nonempty β
f : α → β
hf : f ∈ {f | ∀ (x y : α), f x = f y}
a : α
⊢ ∃ a, const α a = f
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
t : Set α
p : Set α → Prop
⊢ (∃ s, p (val '' s)) ↔ ∃ s, s ⊆ t ∧ p s

Tactic:
by
  rw [← exists_subset_range_and_iff, range_coe]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s s₁ s₂ : Set α
f : α → β
h : InjOn f s
h₁ : s₁ ⊆ s
h₂ : s₂ ⊆ s
h' : f '' s₁ ⊆ f '' s₂
⊢ s₁ ⊆ s₂

Tactic:
rw [← h.preimage_image_inter h₁, ← h.preimage_image_inter h₂]

Goal state after:
α : Type u_1
β : Type u_2
s s₁ s₂ : Set α
f : α → β
h : InjOn f s
h₁ : s₁ ⊆ s
h₂ : s₂ ⊆ s
h' : f '' s₁ ⊆ f '' s₂
⊢ f ⁻¹' f '' s₁ ∩ s ⊆ f ⁻¹' f '' s₂ ∩ s
Module: Mathlib.Algebra.Group.Hom.Defs

Goal state before:
pp: G : Type u_7
H : Type u_8
F : Type u_9
inst✝³ : FunLike F G H
inst✝² : DivInvMonoid G
inst✝¹ : DivInvMonoid H
inst✝ : MulHomClass F G H
f : F
hf : ∀ (a : G), f a⁻¹ = (f a)⁻¹
a b : G
⊢ f (a / b) = f a / f b

Tactic:
by
  grind [div_eq_mul_inv]

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

Tactic:
have := congrArg (· \ {f a}) (image_insert_eq ▸ h.image_eq)
    simp only [mem_singleton_iff, insert_sdiff_of_mem] at this
    rw [sdiff_singleton_eq_self hfa, sdiff_singleton_eq_self] at this
    · exact ⟨by simp [← this, mapsTo_iff_image_subset], h.injOn.mono (subset_insert ..),
        by simp [← this, surjOn_image]⟩
    simp only [mem_image, not_exists, not_and]
    intro x hx
    rw [h.injOn.eq_iff (by simp [hx]) (by simp)]
    exact ha ∘ (· ▸ hx)

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

Goal state before:
pp: case refine_2
a b c d m n✝ : ℤ
motive : ℤ → Sort u_1
lt : (n : ℤ) → n < m → motive n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → motive k) → motive n
n : ℤ
hnm : ¬n < m
⊢ (k : ℤ) → k ≤ m → ((k_1 : ℤ) → k_1 < k → motive k_1) → (k_1 : ℤ) → k_1 < k - 1 → motive k_1

Tactic:
· exact fun n _ hn l _ ↦ hn l (by lia)

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
a b : M
n : ℕ
h : a * b = 1
⊢ a ^ n.succ * b ^ n.succ = a ^ n * a * (b * b ^ n)

Tactic:
by rw [pow_succ, pow_succ']

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 rw [← h, inv_mul_cancel_left]

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

Goal state before:
pp: α : Type u
inst✝ : Monoid α
u : αˣ
a : α
h : ↑u = a
⊢ a * ↑u⁻¹ = 1

Tactic:
by rw [← h, u.mul_inv]

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

Goal state before:
pp: α : Type u
inst✝ : Monoid α
b : αˣ
a c : α
h : ↑b * a = c
⊢ a = ↑b⁻¹ * c

Tactic:
by rw [← h, inv_mul_cancel_left]

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

Goal state before:
pp: α : Type u
inst✝ : Monoid α
u : αˣ
a : α
h : ↑u * a = 1
⊢ ↑u⁻¹ * 1 = a

Tactic:
by rw [← h, inv_mul_cancel_left]

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

Goal state before:
pp: α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
⊢ Function.Injective ⇑(subtypeCongrHom p)

Tactic:
rintro ⟨⟩ ⟨⟩ h
  rw [Prod.mk_inj]
  constructor <;> ext i <;> simpa using Equiv.congr_fun h i

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

Goal state before:
pp: R : Type u_5
inst✝¹ : Zero R
inst✝ : Pow R ℕ
h : ¬IsReduced R
⊢ ∃ x, x ≠ 0 ∧ IsNilpotent x

Tactic:
simpa [isReduced_iff, not_forall, and_comm] using h

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

Goal state before:
pp: M : Type u_1
A : Type u_7
inst✝¹ : AddGroup A
inst✝ : DistribSMul M A
r : M
x y : A
⊢ r • (x + -y) = r • x + -(r • y)

Tactic:
smul_add,

Goal state after:
M : Type u_1
A : Type u_7
inst✝¹ : AddGroup A
inst✝ : DistribSMul M A
r : M
x y : A
⊢ r • x + r • -y = r • x + -(r • y)
Module: Mathlib.Algebra.Module.Defs

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
x : M
⊢ -r • x + r • x = 0

Tactic:
by rw [← add_smul, neg_add_cancel, zero_smul]

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

Goal state before:
pp: α : Type u
inst✝ : NonAssocRing α
a b : α
⊢ (a - 1) * b = a * b - b

Tactic:
sub_mul,

Goal state after:
α : Type u
inst✝ : NonAssocRing α
a b : α
⊢ a * b - 1 * b = a * b - b
Module: Mathlib.Algebra.Ring.Defs

Goal state before:
pp: α : Type u
inst✝ : NonAssocRing α
a b : α
⊢ (1 - a) * b = b - a * b

Tactic:
sub_mul,

Goal state after:
α : Type u
inst✝ : NonAssocRing α
a b : α
⊢ 1 * b - a * b = b - a * b
Module: Mathlib.Algebra.Ring.Basic

Goal state before:
pp: R : Type u_3
inst✝ : NonUnitalNonAssocRing R
r : R
h : ∀ (x : R), x * r = 0 → x = 0
r₁ r₂ : R
eq : (fun x ↦ x * r) r₁ = (fun x ↦ x * r) r₂
⊢ (r₁ - r₂) * r = 0

Tactic:
sub_mul,

Goal state after:
R : Type u_3
inst✝ : NonUnitalNonAssocRing R
r : R
h : ∀ (x : R), x * r = 0 → x = 0
r₁ r₂ : R
eq : (fun x ↦ x * r) r₁ = (fun x ↦ x * r) r₂
⊢ r₁ * r - r₂ * r = 0
Module: Mathlib.Algebra.Ring.Basic

Goal state before:
pp: α : Type u_3
inst✝ : Ring α
⊢ IsDomain α ↔ NoZeroDivisors α ∧ Nontrivial α

Tactic:
rw [← isCancelMulZero_iff_noZeroDivisors, isDomain_iff_cancelMulZero_and_nontrivial]

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 / a)

Tactic:
mul_one_div

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

Goal state before:
pp: α : Type u
inst✝¹ : Monoid α
inst✝ : HasDistribNeg α
a : α
u : αˣ
⊢ -(a /ₚ u) = -a /ₚ u

Tactic:
simp only [divp, neg_mul]

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

Goal state before:
pp: α : Type u
inst✝ : Ring α
a b : α
u : αˣ
⊢ a /ₚ u - b = (a - b * ↑u) /ₚ u

Tactic:
by
  simp only [divp, sub_mul, sub_right_inj]
  rw [mul_assoc, Units.mul_inv, mul_one]

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 + (a - b) * b

Tactic:
sub_mul,

Goal state after:
R : Type u
inst✝ : NonUnitalNonAssocRing R
a b : R
h : Commute a b
⊢ a * a - b * b = a * a - b * a + (a - b) * b
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 * a - b * a + (a - b) * b

Tactic:
sub_mul,

Goal state after:
R : Type u
inst✝ : NonUnitalNonAssocRing R
a b : R
h : Commute a b
⊢ a * a - b * b = a * a - b * a + (a * b - b * b)
Module: Mathlib.Algebra.Ring.Commute

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

Tactic:
rw [sq, sq, h.mul_self_sub_mul_self_eq]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
n : ℕ
⊢ (-1) ^ (n % 2) * (-1) ^ (2 * (n / 2)) = (-1) ^ ((n % 2 + 2 * (n / 2)) % 2)

Tactic:
pow_mul

Goal state after:
R : Type u
inst✝ : Ring R
n : ℕ
⊢ (-1) ^ (n % 2) * ((-1) ^ 2) ^ (n / 2) = (-1) ^ ((n % 2 + 2 * (n / 2)) % 2)
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic

Goal state before:
pp: α : 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 α
⊢ a₂ * b₂ ≤ a₁ * b₁ ↔ a₁ = a₂ ∧ b₁ = b₂

Tactic:
refine ⟨fun h ↦ ?_, by rintro ⟨rfl, rfl⟩; rfl⟩

Goal state after:
α : 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₁
⊢ a₁ = a₂ ∧ b₁ = b₂
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : MulZeroClass α
a b c d : α
inst✝² : PartialOrder α
inst✝¹ : PosMulStrictMono α
inst✝ : MulPosStrictMono α
hab : a ≤ b
hcd : c ≤ d
a0 : 0 < a
d0 : 0 < d
⊢ a * c = b * d ↔ a = b ∧ c = d

Tactic:
refine ⟨fun h ↦ ?_, by rintro ⟨rfl, rfl⟩; rfl⟩

Goal state after:
α : Type u_1
inst✝³ : MulZeroClass α
a b c d : α
inst✝² : PartialOrder α
inst✝¹ : PosMulStrictMono α
inst✝ : MulPosStrictMono α
hab : a ≤ b
hcd : c ≤ d
a0 : 0 < a
d0 : 0 < d
h : a * c = b * d
⊢ a = b ∧ c = d
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : MulZeroClass α
a b c d : α
inst✝² : PartialOrder α
inst✝¹ : PosMulStrictMono α
inst✝ : MulPosStrictMono α
hab : a ≤ b
hcd : c ≤ d
b0 : 0 < b
c0 : 0 < c
⊢ a * c = b * d ↔ a = b ∧ c = d

Tactic:
refine ⟨fun h ↦ ?_, by rintro ⟨rfl, rfl⟩; rfl⟩

Goal state after:
α : Type u_1
inst✝³ : MulZeroClass α
a b c d : α
inst✝² : PartialOrder α
inst✝¹ : PosMulStrictMono α
inst✝ : MulPosStrictMono α
hab : a ≤ b
hcd : c ≤ d
b0 : 0 < b
c0 : 0 < c
h : a * c = b * d
⊢ a = b ∧ c = d
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✝² : MulPosMono R
inst✝¹ : AddRightMono R
inst✝ : AddRightReflectLE R
h : b ≤ a
hc : c ≤ 0
d : R
hcd : 0 = c + d
⊢ a * c ≤ b * c

Tactic:
refine le_of_add_le_add_right (a := b * d + a * d) ?_

Goal state after:
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : Preorder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : MulPosMono R
inst✝¹ : AddRightMono R
inst✝ : AddRightReflectLE R
h : b ≤ a
hc : c ≤ 0
d : R
hcd : 0 = c + d
⊢ a * c + (b * d + a * d) ≤ b * c + (b * d + a * d)
Module: Mathlib.Logic.Embedding.Basic

Goal state before:
pp: one : Type u_1
α : Type u_2
inst✝ : Unique one
a : α
x y : one
h : (fun x ↦ a) x = (fun x ↦ a) y
⊢ x = y

Tactic:
by simp [Unique.uniq inferInstance]

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

Goal state before:

Tactic:
4 * a * b
    _ = 2 * a * b + 2 * a * b := by rw [mul_assoc, two_add_two_eq_four.symm, add_mul, mul_assoc]
    _ ≤ a ^ 2 + b ^ 2 + 2 * a * b := by gcongr; exact two_mul_le_add_sq _ _
    _ = a ^ 2 + 2 * a * b + b ^ 2 := by rw [add_right_comm]
    _ = (a + b) ^ 2 := (add_sq a b).symm

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
f g : r ↪r s
h : (fun x ↦ x.toFun) f = (fun x ↦ x.toFun) g
⊢ f = g

Tactic:
rcases f with ⟨⟨⟩⟩
    rcases g with ⟨⟨⟩⟩
    congr

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

Goal state before:
pp: F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ✝ : Type u_4
δ✝ : Type u_5
inst✝⁷ : LE α✝
inst✝⁶ : LE β✝
inst✝⁵ : LE γ✝
inst✝⁴ : LE δ✝
α : Type ?u.19
β : Type ?u.21
γ : Type ?u.23
δ : Type ?u.25
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
f : α ≃o γ
g : β ≃o δ
p : α →o β
⊢ (⇑g.symm ∘ ⇑g) ∘ ⇑p ∘ ⇑f.symm ∘ ⇑f = ⇑p

Tactic:
simp only [← OrderIso.coe_trans, Function.id_comp,
               OrderIso.self_trans_symm, OrderIso.coe_refl, Function.comp_id]

Goal state after: