mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: F : Type u_1
M₀ : Type u_5
inst✝² : MonoidWithZero M₀
inst✝¹ : FunLike F ℚ≥0 M₀
inst✝ : MonoidWithZeroHomClass F ℚ≥0 M₀
f g : F
same_on_pnat : ∀ (n : ℕ), 0 < n → f ↑n = g ↑n
⊢ ∀ {n : ℕ},
    0 < n →
      ((MonoidWithZeroHom.ofClass f).comp (MonoidWithZeroHom.ofClass (Nat.castRingHom ℚ≥0))) n =
        ((MonoidWithZeroHom.ofClass g).comp (MonoidWithZeroHom.ofClass (Nat.castRingHom ℚ≥0))) n

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.NormNum.Pow

Goal state before:
pp: a b c b' c' : ℕ
h1 : a.pow b' = c'
hb : 2 * b' = b
hc : c' * c' = c
⊢ (Int.negOfNat a).pow b = Int.ofNat c

Tactic:
by

Goal state after:
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: F : Type u_1
M₀ : Type u_5
inst✝² : MonoidWithZero M₀
inst✝¹ : FunLike F ℚ M₀
inst✝ : MonoidWithZeroHomClass F ℚ M₀
f g : F
h : ∀ (m : ℤ), f ↑m = g ↑m
r : ℚ
⊢ f r = g r

Tactic:
by

Goal state after:
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: F : Type u_1
M₀ : Type u_5
inst✝² : MonoidWithZero M₀
inst✝¹ : FunLike F ℚ M₀
inst✝ : MonoidWithZeroHomClass F ℚ M₀
f g : F
same_on_neg_one : f (-1) = g (-1)
same_on_pnat : ∀ (n : ℕ), 0 < n → f ↑n = g ↑n
⊢ ((MonoidWithZeroHom.ofClass f).comp (MonoidWithZeroHom.ofClass (Int.castRingHom ℚ))) (-1) =
    ((MonoidWithZeroHom.ofClass g).comp (MonoidWithZeroHom.ofClass (Int.castRingHom ℚ))) (-1)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: F : Type u_1
M₀ : Type u_5
inst✝² : MonoidWithZero M₀
inst✝¹ : FunLike F ℚ M₀
inst✝ : MonoidWithZeroHomClass F ℚ M₀
f g : F
same_on_neg_one : f (-1) = g (-1)
same_on_pnat : ∀ (n : ℕ), 0 < n → f ↑n = g ↑n
⊢ ∀ (n : ℕ),
    0 < n →
      ((MonoidWithZeroHom.ofClass f).comp (MonoidWithZeroHom.ofClass (Int.castRingHom ℚ))) ↑n =
        ((MonoidWithZeroHom.ofClass g).comp (MonoidWithZeroHom.ofClass (Int.castRingHom ℚ))) ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝¹ : FunLike F α β
R : Type u_5
inst✝ : Semiring R
f g : ℚ≥0 →+* R
⊢ ∀ (n : ℕ), f ↑n = g ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.NormNum.Pow

Goal state before:
pp: a b c b' c' : ℕ
h1 : a.pow b' = c'
hb : 2 * b' + 1 = b
hc : c' * (c' * a) = c
⊢ (Int.negOfNat a).pow b = Int.negOfNat c

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.NormNum.Pow

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
n✝¹ n✝ : ℕ
⊢ ↑n✝¹ ^ ↑n✝ = ↑(n✝¹.pow n✝)

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.NormNum.Pow

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
n✝¹ : ℤ
n✝ : ℕ
⊢ ↑n✝¹ ^ ↑n✝ = ↑(n✝¹.pow n✝)

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.NormNum.Pow

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
f : α → ℕ → α
a : α
an cn : ℤ
ad b b' cd : ℕ
⊢ f = HPow.hPow → IsRat a an ad → IsNat b b' → an.pow b' = cn → ad.pow b' = cd → IsRat (f a b) cn cd

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.NormNum.Pow

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
f : α → ℕ → α
a : α
an cn ad b b' cd : ℕ
⊢ f = HPow.hPow → IsNNRat a an ad → IsNat b b' → an.pow b' = cn → ad.pow b' = cd → IsNNRat (f a b) cn cd

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.NormNum.Pow

Goal state before:
pp: α : Type u_1
inst✝ : DivisionSemiring α
a : α
b : ℤ
nb ne : ℕ
pb : IsNat b nb
pe' : IsNat (a ^ nb) ne
⊢ IsNat (a ^ b) ne

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.NormNum.Pow

Goal state before:
pp: α : Type u_1
inst✝ : DivisionSemiring α
a : α
b : ℤ
nb ne : ℕ
pb : IsInt b (Int.negOfNat nb)
pe' : IsNat (a ^ nb)⁻¹ ne
⊢ IsNat (a ^ b) ne

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.NormNum.Pow

Goal state before:
pp: α : Type u_1
inst✝ : DivisionRing α
a : α
b : ℤ
nb ne : ℕ
pb : IsNat b nb
pe' : IsInt (a ^ nb) (Int.negOfNat ne)
⊢ IsInt (a ^ b) (Int.negOfNat ne)

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.NormNum.Pow

Goal state before:
pp: α : Type u_1
inst✝ : DivisionRing α
a : α
b : ℤ
nb ne : ℕ
pb : IsInt b (Int.negOfNat nb)
pe' : IsInt (a ^ nb)⁻¹ (Int.negOfNat ne)
⊢ IsInt (a ^ b) (Int.negOfNat ne)

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.NormNum.Pow

Goal state before:
pp: α : Type u_1
inst✝ : DivisionSemiring α
a : α
b : ℤ
nb num den : ℕ
pb : IsNat b nb
pe' : IsNNRat (a ^ nb) num den
⊢ IsNNRat (a ^ b) num den

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.NormNum.Pow

Goal state before:
pp: α : Type u_1
inst✝ : DivisionSemiring α
a : α
b : ℤ
nb num den : ℕ
pb : IsInt b (Int.negOfNat nb)
pe' : IsNNRat (a ^ nb)⁻¹ num den
⊢ IsNNRat (a ^ b) num den

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.NormNum.Pow

Goal state before:
pp: α : Type u_1
inst✝ : DivisionRing α
a : α
b : ℤ
nb : ℕ
num : ℤ
den : ℕ
pb : IsNat b nb
pe' : IsRat (a ^ nb) num den
⊢ IsRat (a ^ b) num den

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.NormNum.Pow

Goal state before:
pp: α : Type u_1
inst✝ : DivisionRing α
a : α
b : ℤ
nb : ℕ
num : ℤ
den : ℕ
pb : IsInt b (Int.negOfNat nb)
pe' : IsRat (a ^ nb)⁻¹ num den
⊢ IsRat (a ^ b) num den

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Linarith.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
a b : α
ha : a = 0
hb : b = 0
⊢ a + b = 0

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Linarith.Lemmas

Goal state before:
pp: α : Type u
inst✝¹ : Semiring α
inst✝ : PartialOrder α
a b : α
ha : a = 0
hb : b ≤ 0
⊢ a + b ≤ 0

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Linarith.Lemmas

Goal state before:
pp: α : Type u
inst✝¹ : Semiring α
inst✝ : PartialOrder α
a b : α
ha : a = 0
hb : b < 0
⊢ a + b < 0

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Linarith.Lemmas

Goal state before:
pp: α : Type u
inst✝¹ : Semiring α
inst✝ : PartialOrder α
a b : α
ha : a ≤ 0
hb : b = 0
⊢ a + b ≤ 0

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Linarith.Lemmas

Goal state before:
pp: α : Type u
inst✝¹ : Semiring α
inst✝ : PartialOrder α
a b : α
ha : a < 0
hb : b = 0
⊢ a + b < 0

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Linarith.Lemmas

Goal state before:
pp: α : Type u
inst✝² : Semiring α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedRing α
a b : α
ha : a = 0
x✝ : 0 < b
⊢ b * a = 0

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Linarith.Lemmas

Goal state before:
pp: α : Type u
inst✝² : Ring α
inst✝¹ : PartialOrder α
inst✝ : IsStrictOrderedRing α
a b : α
ha : a < 0
hb : 0 < b
this : -b * a > 0
⊢ 0 < -(b * a)

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Linarith.Lemmas

Goal state before:
pp: α : Type u
inst✝² : Ring α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedRing α
a b : α
ha : a ≤ 0
hb : 0 < b
this : -b * a ≥ 0
⊢ b * a ≤ 0

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Linarith.Lemmas

Goal state before:
pp: α : Type u_1
R : α → α → Prop
inst✝ : Semiring α
a b : α
x✝ : R a 0
h : b = 0
⊢ a * b = 0

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Linarith.Lemmas

Goal state before:
pp: α : Type u_1
R : α → α → Prop
inst✝ : Semiring α
a b : α
h : a = 0
x✝ : R b 0
⊢ a * b = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a : R
n : ℕ
e : a = ↑n
⊢ a = n.rawCast + 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a : R
e : a = ↑0
⊢ a = 0

Tactic:
by

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

Goal state before:
pp: n : ℕ
R : Type u_2
inst✝ : Ring R
a : R
e : a = ↑(Int.negOfNat n)
⊢ a = (Int.negOfNat n).rawCast + 0

Tactic:
by

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

Goal state before:
pp: n d : ℕ
R : Type u_2
inst✝ : DivisionSemiring R
a : R
inv✝ : Invertible ↑d
e : a = ↑n * ⅟↑d
⊢ a = NNRat.rawCast n d + 0

Tactic:
by

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

Goal state before:
pp: n : ℤ
d : ℕ
R : Type u_2
inst✝ : DivisionRing R
a : R
inv✝ : Invertible ↑d
e : a = ↑n * ⅟↑d
⊢ a = Rat.rawCast n d + 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
n : ℕ
⊢ ↑n.rawCast = n.rawCast

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
b₁ b₃ : R
a₁ a₃ a₂ : ℕ
x✝¹ : ↑a₁ = b₁
x✝ : ↑a₃ = b₃
⊢ ↑(a₁ ^ a₂ * a₃) = b₁ ^ a₂ * b₃

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
b₁ b₂ : R
a₁ a₂ : ℕ
x✝¹ : ↑a₁ = b₁
x✝ : ↑a₂ = b₂
⊢ ↑(a₁ + a₂) = b₁ + b₂

Tactic:
by

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

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
n : ℕ
⊢ ↑n.rawCast = n.rawCast

Tactic:
by

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

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
n : ℕ
⊢ ↑(Int.negOfNat n).rawCast = (Int.negOfNat n).rawCast

Tactic:
by

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

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
b₁ b₃ : R
a₁ a₃ : ℤ
a₂ : ℕ
x✝¹ : ↑a₁ = b₁
x✝ : ↑a₃ = b₃
⊢ ↑(a₁ ^ a₂ * a₃) = b₁ ^ a₂ * b₃

Tactic:
by

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

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
b₁ b₂ : R
a₁ a₂ : ℤ
x✝¹ : ↑a₁ = b₁
x✝ : ↑a₂ = b₂
⊢ ↑(a₁ + a₂) = b₁ + b₂

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : Mul α
a a' : α
h : a = a'
b : α
⊢ a • b = a' * b

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
n n' : ℕ
r : R
hr : ↑n = r
hn : n' = n
a : R
⊢ n' • a = r * a

Tactic:
by

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

Goal state before:
pp: R : Type u_2
n n' : ℤ
r : R
inst✝ : CommRing R
hr : ↑n = r
hn : n' = n
a : R
⊢ n' • a = r * a

Tactic:
by

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

Goal state before:
pp: α β : Type u_2
inst : CSLift α β
a b : α
a' b' : β
h1 : CSLiftVal a a'
h2 : CSLiftVal b b'
h : a' = b'
⊢ CSLift.lift a = CSLift.lift b

Tactic:
by

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

Goal state before:
pp: α : Sort u_2
a b c : α
x✝¹ : a = c
x✝ : b = c
⊢ a = b

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.SimplexAlgorithm

Goal state before:
pp: matType : Nat → Nat → Type
inst✝ : UsableInSimplexAlgorithm matType
exitIdx enterIdx : Nat
s : Tableau matType
mat✝² : matType s.basic.size s.free.size := s.mat
intersectCoef : Rat := mat✝²[(exitIdx, enterIdx)]!
__s✝ : matType s.basic.size s.free.size
mat✝¹ : matType s.basic.size s.free.size := __s✝
mat✝ : matType s.basic.size s.free.size := setElem mat✝¹ exitIdx enterIdx (-1)
mat : matType s.basic.size s.free.size := divideRow mat✝ exitIdx (-intersectCoef)
newBasic : Array Nat := s.basic.set! exitIdx s.free[enterIdx]!
newFree : Array Nat := s.free.set! enterIdx s.basic[exitIdx]!
⊢ newBasic.size = s.basic.size

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.SimplexAlgorithm

Goal state before:
pp: matType : Nat → Nat → Type
inst✝ : UsableInSimplexAlgorithm matType
exitIdx enterIdx : Nat
s : Tableau matType
mat✝² : matType s.basic.size s.free.size := s.mat
intersectCoef : Rat := mat✝²[(exitIdx, enterIdx)]!
__s✝ : matType s.basic.size s.free.size
mat✝¹ : matType s.basic.size s.free.size := __s✝
mat✝ : matType s.basic.size s.free.size := setElem mat✝¹ exitIdx enterIdx (-1)
mat : matType s.basic.size s.free.size := divideRow mat✝ exitIdx (-intersectCoef)
newBasic : Array Nat := s.basic.set! exitIdx s.free[enterIdx]!
newFree : Array Nat := s.free.set! enterIdx s.basic[exitIdx]!
hb : newBasic.size = s.basic.size
⊢ newFree.size = s.free.size

Tactic:
by

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

Goal state before:
pp: α : Type u
t : BinaryTree α
⊢ map id t = t

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type u_1
γ : Type u_2
f : α → β
g : β → γ
t : BinaryTree α
⊢ map (g ∘ f) t = map g (map f t)

Tactic:
by

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

Goal state before:
pp: α : Type u
t : BinaryTree α
m : Type u → Type u_1
inst✝¹ : Applicative m
inst✝ : LawfulApplicative m
⊢ traverse pure t = pure t

Tactic:
by

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

Goal state before:
pp: α : Type u
x : BinaryTree α
⊢ x.numLeaves = x.numNodes + 1

Tactic:
by

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

Goal state before:
pp: α : Type u
x : BinaryTree α
⊢ 0 < x.numLeaves

Tactic:
by

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

Goal state before:
pp: h : nil ≠ nil
⊢ node () nil.left nil.right = nil

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.CancelDenoms.Core

Goal state before:
pp: α : Type u_1
inst✝ : CommRing α
n1 n2 k e1 e2 t1 t2 : α
h1 : n1 * e1 = t1
h2 : n2 * e2 = t2
h3 : n1 * n2 = k
⊢ k * (e1 * e2) = t1 * t2

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.CancelDenoms.Core

Goal state before:
pp: α : Type u_1
inst✝ : Field α
n1 n2 k e1 e2 t1 : α
h1 : n1 * e1 = t1
h2 : n2 / e2 = 1
h3 : n1 * n2 = k
⊢ k * (e1 / e2) = t1

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.CancelDenoms.Core

Goal state before:
pp: α : Type u_1
inst✝ : Field α
n e e' : α
h : n * e = e'
h2 : n ≠ 0
⊢ e * n = e'

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.CancelDenoms.Core

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
n e1 e2 t1 t2 : α
h1 : n * e1 = t1
h2 : n * e2 = t2
⊢ n * (e1 + e2) = t1 + t2

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.CancelDenoms.Core

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
n e1 e2 t1 t2 : α
h1 : n * e1 = t1
h2 : n * e2 = t2
⊢ n * (e1 - e2) = t1 - t2

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.CancelDenoms.Core

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
n e t : α
h1 : n * e = t
⊢ n * -e = -t

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.CancelDenoms.Core

Goal state before:
pp: α : Type u_1
inst✝ : CommRing α
n e1 t1 k l : α
e2 : ℕ
h1 : n * e1 = t1
h2 : l * n ^ e2 = k
⊢ k * e1 ^ e2 = l * t1 ^ e2

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.CancelDenoms.Core

Goal state before:
pp: α : Type u_1
inst✝ : Field α
n k e : α
h2 : e ≠ 0
h3 : n * e = k
⊢ k * e⁻¹ = n

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: $u✝ «$u» : Lean.Level
«$α» : Type u
«$sα» : CommSemiring «$α»
«$a» : «$α»
«$b» : ℕ
$expr✝ : «$α»
«$pf» : Nat.rawCast 1 = $expr✝
⊢ «$a» ^ «$b» * Nat.rawCast 1 = «$a» ^ «$b» * $expr✝

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.CancelDenoms.Core

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : 0 < ad
hbd : 0 < bd
hgcd : 0 < gcd
⊢ (a < b) = (1 / gcd * (bd * a') < 1 / gcd * (ad * b'))

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a b c x : R
e : ℕ
pq_pf : a + b = c
⊢ x ^ e * a + x ^ e * b = x ^ e * c

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a b x : R
e : ℕ
h : a + b = ↑0
⊢ x ^ e * a + x ^ e * b = ↑0

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
b : R
⊢ 0 + b = b

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a : R
⊢ a + 0 = a

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a₁ a₂ b₁ b₂ c₁ c₂ : R
x✝¹ : a₁ + b₁ = c₁
x✝ : a₂ + b₂ = c₂
⊢ a₁ + a₂ + (b₁ + b₂) = c₁ + c₂

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a₁ a₂ b₁ b₂ c : R
h : IsNat (a₁ + b₁) 0
h₄ : a₂ + b₂ = c
⊢ a₁ + a₂ + (b₁ + b₂) = c

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a₂ b c a₁ : R
x✝ : a₂ + b = c
⊢ a₁ + a₂ + b = a₁ + c

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a b₂ c b₁ : R
x✝ : a + b₂ = c
⊢ a + (b₁ + b₂) = b₁ + c

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a : R
⊢ Nat.rawCast 1 * a = a

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a : R
⊢ a * Nat.rawCast 1 = a

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Linarith.Preprocessing

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
a b : M
h : 1 * a = b
⊢ a = b

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.CancelDenoms.Core

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : 0 < ad
hbd : 0 < bd
hgcd : 0 < gcd
⊢ (a ≤ b) = (1 / gcd * (bd * a') ≤ 1 / gcd * (ad * b'))

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.CancelDenoms.Core

Goal state before:
pp: α : Type u_1
inst✝ : Field α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : ad ≠ 0
hbd : bd ≠ 0
hgcd : gcd ≠ 0
⊢ (a = b) = (1 / gcd * (bd * a') = 1 / gcd * (ad * b'))

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a₃ b c a₁ : R
a₂ : ℕ
x✝ : a₃ * b = c
⊢ a₁ ^ a₂ * a₃ * b = a₁ ^ a₂ * c

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.CancelDenoms.Core

Goal state before:
pp: α : Type u_1
inst✝ : Field α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : ad ≠ 0
hbd : bd ≠ 0
hgcd : gcd ≠ 0
⊢ (a ≠ b) = (1 / gcd * (bd * a') ≠ 1 / gcd * (ad * b'))

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a b₃ c b₁ : R
b₂ : ℕ
x✝ : a * b₃ = c
⊢ a * (b₁ ^ b₂ * b₃) = b₁ ^ b₂ * c

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a₂ b₂ c : R
ea eb e : ℕ
x : R
x✝¹ : ea + eb = e
x✝ : a₂ * b₂ = c
⊢ x ^ ea * a₂ * (x ^ eb * b₂) = x ^ e * c

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : CanonicallyOrderedAdd R
inst✝ : Nontrivial R
a : R
⊢ Odd a → 0 < a

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : LE R
inst✝ : CanonicallyOrderedAdd R
⊢ MulLeftMono R

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : LE R
inst✝ : CanonicallyOrderedAdd R
⊢ MulRightMono R

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝³ : CommSemiring R
inst✝² : PartialOrder R
inst✝¹ : CanonicallyOrderedAdd R
inst✝ : NoZeroDivisors R
a b : R
⊢ 0 < a * b ↔ 0 < a ∧ 0 < b

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝³ : CommSemiring R
inst✝² : PartialOrder R
inst✝¹ : CanonicallyOrderedAdd R
inst✝ : PosMulStrictMono R
a b c d : R
hab : a < b
hcd : c < d
⊢ a * c < b * d

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a : R
⊢ a * 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a b₁ b₂ c₁ c₂ d : R
x✝² : a * b₁ = c₁
x✝¹ : a * b₂ = c₂
x✝ : c₁ + 0 + c₂ = d
⊢ a * (b₁ + b₂) = d

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
b : R
⊢ 0 * b = 0

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a₁ a₂ b c₁ c₂ d : R
x✝² : a₁ * b = c₁
x✝¹ : a₂ * b = c₂
x✝ : c₁ + c₂ = d
⊢ (a₁ + a₂) * b = d

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
a b : R
x✝ : -1 * a = b
⊢ -a = b

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
a₁ : R
a₂ : ℕ
a₃ b : R
x✝ : -a₃ = b
⊢ -(a₁ ^ a₂ * a₃) = a₁ ^ a₂ * b

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
⊢ -0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
a₁ a₂ b₁ b₂ : R
x✝¹ : -a₁ = b₁
x✝ : -a₂ = b₂
⊢ -(a₁ + a₂) = b₁ + b₂

Tactic:
subst_vars; simp [add_comm]

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

Goal state before:
pp: R : Type u
inst✝⁵ : NonUnitalNonAssocSemiring R
inst✝⁴ : PartialOrder R
inst✝³ : CanonicallyOrderedAdd R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
a b c : R
h : AddLECancellable (a * c)
⊢ a * (b - c) = a * b - a * c

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
a₁ a₂ b₁ b₂ : R
x✝¹ : -a₁ = b₁
x✝ : -a₂ = b₂
⊢ -(a₁ + a₂) = b₁ + b₂

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
a b c d : R
x✝¹ : -b = c
x✝ : a + c = d
⊢ a - b = d

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a : R
b : ℕ
e : R
h : (a + 0) ^ b * Nat.rawCast 1 = e
⊢ a ^ b = e

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a : R
b : ℕ
e : R
h : a ^ b * Nat.rawCast 1 = e
⊢ a ^ b = e + 0

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a : R
⊢ a ^ 1 = a

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a b c : R
k : ℕ
x✝¹ : a ^ k = b
x✝ : b * b = c
⊢ a ^ Nat.mul 2 k = c

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a b c : R
k : ℕ
d : R
x✝² : a ^ k = b
x✝¹ : b * b = c
x✝ : c * a = d
⊢ a ^ (Nat.mul 2 k).add 1 = d

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a : R
b : ℕ
ha : IsNat a 1
⊢ a ^ b = a

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a₂ : R
ea₁ b : ℕ
xa₁ : R
⊢ (xa₁ ^ ea₁ * a₂) ^ b = xa₁ ^ (ea₁ * b) * a₂ ^ b

Tactic:
simp [_root_.mul_pow, pow_mul]

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

Goal state before:
pp: R : Type u
inst✝⁶ : NonUnitalNonAssocSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : CanonicallyOrderedAdd R
inst✝³ : Sub R
inst✝² : OrderedSub R
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : MulRightMono R
a b c : R
h : AddLECancellable (b * c)
⊢ (a - b) * c = a * c - b * c

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a₂ c₂ : R
ea₁ b c₁ : ℕ
xa₁ : R
x✝¹ : ea₁ * b = c₁
x✝ : a₂ ^ b = c₂
⊢ (xa₁ ^ ea₁ * a₂) ^ b = xa₁ ^ c₁ * c₂

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝⁶ : NonAssocSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : CanonicallyOrderedAdd R
inst✝³ : Sub R
inst✝² : OrderedSub R
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : AddLeftReflectLE R
a b : R
⊢ a * (b - 1) = a * b - a

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝⁷ : NonAssocSemiring R
inst✝⁶ : PartialOrder R
inst✝⁵ : CanonicallyOrderedAdd R
inst✝⁴ : Sub R
inst✝³ : OrderedSub R
inst✝² : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝¹ : MulRightMono R
inst✝ : AddLeftReflectLE R
a b : R
⊢ (a - 1) * b = a * b - b

Tactic:
by

Goal state after: