mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.RamificationInertia.HilbertTheory

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝³⁴ : Field K
inst✝³³ : Field L
inst✝³² : Algebra K L
inst✝³¹ : CommRing A
inst✝³⁰ : CommRing B
inst✝²⁹ : Algebra A B
p : Ideal A
P : Ideal B
inst✝²⁸ : Algebra A K
inst✝²⁷ : IsFractionRing A K
inst✝²⁶ : Algebra A L
inst✝²⁵ : IsScalarTower A K L
inst✝²⁴ : Algebra B L
inst✝²³ : IsScalarTower A B L
inst✝²² : IsFractionRing B L
inst✝²¹ : MulSemiringAction Gal(L/K) B
inst✝²⁰ : SMulDistribClass Gal(L/K) B L
D : Type u_5
𝓞D : Type u_6
inst✝¹⁹ : Field D
inst✝¹⁸ : Algebra D L
inst✝¹⁷ : IsDecompositionField K L P D
inst✝¹⁶ : CommRing 𝓞D
inst✝¹⁵ : Algebra 𝓞D D
inst✝¹⁴ : IsFractionRing 𝓞D D
inst✝¹³ : Algebra 𝓞D B
inst✝¹² : Algebra 𝓞D L
inst✝¹¹ : IsScalarTower 𝓞D D L
inst✝¹⁰ : IsScalarTower 𝓞D B L
𝓟D : Ideal 𝓞D
inst✝⁹ : IsGalois K L
inst✝⁸ : IsDedekindDomain A
inst✝⁷ : IsDedekindDomain B
inst✝⁶ : Module.Finite A B
inst✝⁵ : Module.IsTorsionFree A B
inst✝⁴ : Algebra A 𝓞D
inst✝³ : Module.Finite A 𝓞D
inst✝² : IsScalarTower A 𝓞D B
inst✝¹ : IsDedekindDomain 𝓞D
inst✝ : 𝓟D.LiesOver p
hp : p ≠ ⊥
inst₁ : Module.Finite 𝓞D B
⊢ Module.IsTorsionFree 𝓞D B

Tactic:
rw [Module.isTorsionFree_iff_faithfulSMul]

Goal state after:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝³⁴ : Field K
inst✝³³ : Field L
inst✝³² : Algebra K L
inst✝³¹ : CommRing A
inst✝³⁰ : CommRing B
inst✝²⁹ : Algebra A B
p : Ideal A
P : Ideal B
inst✝²⁸ : Algebra A K
inst✝²⁷ : IsFractionRing A K
inst✝²⁶ : Algebra A L
inst✝²⁵ : IsScalarTower A K L
inst✝²⁴ : Algebra B L
inst✝²³ : IsScalarTower A B L
inst✝²² : IsFractionRing B L
inst✝²¹ : MulSemiringAction Gal(L/K) B
inst✝²⁰ : SMulDistribClass Gal(L/K) B L
D : Type u_5
𝓞D : Type u_6
inst✝¹⁹ : Field D
inst✝¹⁸ : Algebra D L
inst✝¹⁷ : IsDecompositionField K L P D
inst✝¹⁶ : CommRing 𝓞D
inst✝¹⁵ : Algebra 𝓞D D
inst✝¹⁴ : IsFractionRing 𝓞D D
inst✝¹³ : Algebra 𝓞D B
inst✝¹² : Algebra 𝓞D L
inst✝¹¹ : IsScalarTower 𝓞D D L
inst✝¹⁰ : IsScalarTower 𝓞D B L
𝓟D : Ideal 𝓞D
inst✝⁹ : IsGalois K L
inst✝⁸ : IsDedekindDomain A
inst✝⁷ : IsDedekindDomain B
inst✝⁶ : Module.Finite A B
inst✝⁵ : Module.IsTorsionFree A B
inst✝⁴ : Algebra A 𝓞D
inst✝³ : Module.Finite A 𝓞D
inst✝² : IsScalarTower A 𝓞D B
inst✝¹ : IsDedekindDomain 𝓞D
inst✝ : 𝓟D.LiesOver p
hp : p ≠ ⊥
inst₁ : Module.Finite 𝓞D B
⊢ FaithfulSMul 𝓞D B
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: case inl
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
n₁ n₂ : ℤ
Hx : 1 < (a₁ ^ n₂).x
Hy : 0 < (a₁ ^ n₂).y
H : ∀ (a : Solution₁ d), ∃ n, a = (a₁ ^ n₂) ^ n ∨ a = -(a₁ ^ n₂) ^ n
hn₁ : a₁ ^ (n₂ * n₁) = a₁ ∨ a₁ = -a₁ ^ (n₂ * n₁)
⊢ a₁ ^ n₂ = a₁

Tactic:
@eq_comm _ a₁,

Goal state after:
case inl
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
n₁ n₂ : ℤ
Hx : 1 < (a₁ ^ n₂).x
Hy : 0 < (a₁ ^ n₂).y
H : ∀ (a : Solution₁ d), ∃ n, a = (a₁ ^ n₂) ^ n ∨ a = -(a₁ ^ n₂) ^ n
hn₁ : a₁ ^ (n₂ * n₁) = a₁ ∨ -a₁ ^ (n₂ * n₁) = a₁
⊢ a₁ ^ n₂ = a₁
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: case inl.inl
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
n₁ n₂ : ℤ
Hx : 1 < (a₁ ^ n₂).x
Hy : 0 < (a₁ ^ n₂).y
H : ∀ (a : Solution₁ d), ∃ n, a = (a₁ ^ n₂) ^ n ∨ a = -(a₁ ^ n₂) ^ n
hn₁ : a₁ ^ (n₂ * n₁ - 1) = 1
⊢ a₁ ^ n₂ = a₁

Tactic:
rcases Int.isUnit_iff.mp
          (.of_mul_eq_one _ <|
            sub_eq_zero.mp <| (ha₁.zpow_eq_one_iff (n₂ * n₁ - 1)).mp hn₁) with
        (rfl | rfl)
      · rw [zpow_one]
      · rw [zpow_neg_one, y_inv, lt_neg, neg_zero] at Hy
        exact False.elim (lt_irrefl _ <| ha₁.2.1.trans Hy)

Goal state after:
Module: Mathlib.NumberTheory.Padics.Hensel

Goal state before:
pp: p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2
n k : ℕ
hnk : n ≤ k
⊢ ‖newton_seq k - newton_seq n‖ ≤ ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n

Tactic:
have hex : ∃ m, k = n + m := Nat.exists_eq_add_of_le hnk

Goal state after:
p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2
n k : ℕ
hnk : n ≤ k
hex : ∃ m, k = n + m
⊢ ‖newton_seq k - newton_seq n‖ ≤ ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n
Module: Mathlib.NumberTheory.RamificationInertia.Basic

Goal state before:
pp: case f
R : Type u
inst✝¹⁶ : CommRing R
S : Type v
inst✝¹⁵ : CommRing S
inst✝¹⁴ : Algebra R S
p : Ideal R
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : Algebra R K
L : Type u_2
inst✝¹¹ : Field L
inst✝¹⁰ : Algebra S L
inst✝⁹ : IsFractionRing S L
inst✝⁸ : IsDomain R
inst✝⁷ : IsDomain S
inst✝⁶ : Algebra K L
inst✝⁵ : Module.Finite R S
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R S L
inst✝² : IsScalarTower R K L
inst✝¹ : Algebra.IsAlgebraic R S
inst✝ : IsTorsionFree R K
hp : p ≠ ⊤
b : Set S
hb' : Submodule.span R b ⊔ Submodule.restrictScalars R (map f p) = ⊤
hRL : Function.Injective ⇑(algebraMap R L)
M : Submodule R S := Submodule.span R b
n : ℕ
a : Fin n → S ⧸ M
ha : Submodule.span R (Set.range a) = ⊤
smul_top_eq : p • ⊤ = ⊤
exists_sum : ∀ (x : S ⧸ M), ∃ a', (∀ (i : Fin n), a' i ∈ p) ∧ ∑ i, a' i • a i = x
A' : Fin n → Fin n → R
hA'p : ∀ (i i_1 : Fin n), A' i i_1 ∈ p
hA' : ∀ (i : Fin n), ∑ i_1, A' i i_1 • a i_1 = a i
A : Matrix (Fin n) (Fin n) R := Matrix.of A' - 1
B : Matrix (Fin n) (Fin n) R := A.adjugate
A_smul : ∀ (i : Fin n), ∑ j, A i j • a j = 0
d_smul : ∀ (i : Fin n), A.det • a i = 0
x' : S
hx : A.det • x' ∈ S ∙ f A.det
a' : Fin n → R
left✝ : ∀ (i : Fin n), a' i ∈ p
quot_x_eq : ∑ i, a' i • a i = Submodule.Quotient.mk x'
x : Fin n
| a' x • 0

Tactic:
smul_zero

Goal state after:
case f
R : Type u
inst✝¹⁶ : CommRing R
S : Type v
inst✝¹⁵ : CommRing S
inst✝¹⁴ : Algebra R S
p : Ideal R
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : Algebra R K
L : Type u_2
inst✝¹¹ : Field L
inst✝¹⁰ : Algebra S L
inst✝⁹ : IsFractionRing S L
inst✝⁸ : IsDomain R
inst✝⁷ : IsDomain S
inst✝⁶ : Algebra K L
inst✝⁵ : Module.Finite R S
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R S L
inst✝² : IsScalarTower R K L
inst✝¹ : Algebra.IsAlgebraic R S
inst✝ : IsTorsionFree R K
hp : p ≠ ⊤
b : Set S
hb' : Submodule.span R b ⊔ Submodule.restrictScalars R (map f p) = ⊤
hRL : Function.Injective ⇑(algebraMap R L)
M : Submodule R S := Submodule.span R b
n : ℕ
a : Fin n → S ⧸ M
ha : Submodule.span R (Set.range a) = ⊤
smul_top_eq : p • ⊤ = ⊤
exists_sum : ∀ (x : S ⧸ M), ∃ a', (∀ (i : Fin n), a' i ∈ p) ∧ ∑ i, a' i • a i = x
A' : Fin n → Fin n → R
hA'p : ∀ (i i_1 : Fin n), A' i i_1 ∈ p
hA' : ∀ (i : Fin n), ∑ i_1, A' i i_1 • a i_1 = a i
A : Matrix (Fin n) (Fin n) R := Matrix.of A' - 1
B : Matrix (Fin n) (Fin n) R := A.adjugate
A_smul : ∀ (i : Fin n), ∑ j, A i j • a j = 0
d_smul : ∀ (i : Fin n), A.det • a i = 0
x' : S
hx : A.det • x' ∈ S ∙ f A.det
a' : Fin n → R
left✝ : ∀ (i : Fin n), a' i ∈ p
quot_x_eq : ∑ i, a' i • a i = Submodule.Quotient.mk x'
x : Fin n
| 0
Module: Mathlib.NumberTheory.Padics.Hensel

Goal state before:
pp: p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2
hnsol : (Polynomial.aeval a) F ≠ 0
n : ℕ
this : 2 ≤ 2 ^ (n + 1)
⊢ ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ * ‖(Polynomial.aeval a) F‖ /
      ‖↑((Polynomial.aeval a) (Polynomial.derivative F) * (Polynomial.aeval a) (Polynomial.derivative F))‖ =
    ‖(Polynomial.aeval a) F‖ / ‖(Polynomial.aeval a) (Polynomial.derivative F)‖

Tactic:
PadicInt.coe_mul,

Goal state after:
p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2
hnsol : (Polynomial.aeval a) F ≠ 0
n : ℕ
this : 2 ≤ 2 ^ (n + 1)
⊢ ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ * ‖(Polynomial.aeval a) F‖ /
      ‖↑((Polynomial.aeval a) (Polynomial.derivative F)) * ↑((Polynomial.aeval a) (Polynomial.derivative F))‖ =
    ‖(Polynomial.aeval a) F‖ / ‖(Polynomial.aeval a) (Polynomial.derivative F)‖
Module: Mathlib.NumberTheory.Rayleigh

Goal state before:
pp: case inl
r : ℝ
j : ℤ
h : r > 0
h✝ : (↑⌈(↑j + 1) / r⌉ - 1) * r < ↑j
⊢ (↑⌈(↑j + 1) / r⌉ - 1) * r < ↑j ∧ (↑j + 1) / r ≤ ↑⌈(↑j + 1) / r⌉

Tactic:
exact ⟨‹_›, Int.le_ceil _⟩

Goal state after:
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
d : ℕ
⊢ multSum d = s.nu d * s.totalMass + (multSum d - s.nu d * s.totalMass)

Tactic:
ring

Goal state after:
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: case e_f
s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
d : ℕ
⊢ muPlus d * multSum d = s.totalMass * (muPlus d * s.nu d) + muPlus d * (multSum d - s.nu d * s.totalMass)

Tactic:
ring

Goal state after:
Module: Mathlib.NumberTheory.SumFourSquares

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b c d x y z w : R
⊢ (a * x - b * y - c * z - d * w) ^ 2 + (a * y + b * x + c * w - d * z) ^ 2 + (a * z - b * w + c * x + d * y) ^ 2 +
      (a * w + b * z - c * y + d * x) ^ 2 =
    (a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2) * (x ^ 2 + y ^ 2 + z ^ 2 + w ^ 2)

Tactic:
ring

Goal state after:
Module: Mathlib.NumberTheory.SumFourSquares

Goal state before:
pp: m x y : ℤ
h : 2 * m = x ^ 2 + y ^ 2
this : Even (x ^ 2 + y ^ 2)
⊢ 2 * (x ^ 2 + y ^ 2) = (x - y) ^ 2 + (x + y) ^ 2

Tactic:
ring

Goal state after:
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: case a
s : BoundingSieve
d : ℕ
hd : d ∣ s.prodPrimes
l : ℕ
hl : (l ∣ s.prodPrimes ∧ ¬s.prodPrimes = 0) ∧ l ∣ d
⊢ selbergTerms d / selbergTerms l = selbergTerms d * (selbergTerms l)⁻¹

Tactic:
ring

Goal state after:
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ s.prodPrimes.divisors
d2 : ℕ
hd2 : d2 ∈ s.prodPrimes.divisors
h : d1.lcm d2 ∣ s.prodPrimes
⊢ w d1 * w d2 * (s.nu d1 * s.nu d2 / s.nu (d1.gcd d2)) = s.nu d1 * w d1 * s.nu d2 * w d2 * (s.nu (d1.gcd d2))⁻¹

Tactic:
ring

Goal state after:
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: case a.a.e_f
s : BoundingSieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ s.prodPrimes.divisors
d2 : ℕ
hd2 : d2 ∈ s.prodPrimes.divisors
hgcd_dvd : d1.gcd d2 ∣ s.prodPrimes
l : ℕ
⊢ s.nu d1 * w d1 * s.nu d2 * w d2 * (selbergTerms l)⁻¹ = (selbergTerms l)⁻¹ * (s.nu d1 * w d1) * (s.nu d2 * w d2)

Tactic:
ring

Goal state after:
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b x y u v : R
ha : a = x ^ 2 + y ^ 2
hb : b = u ^ 2 + v ^ 2
⊢ (x ^ 2 + y ^ 2) * (u ^ 2 + v ^ 2) = (x * u - y * v) ^ 2 + (x * v + y * u) ^ 2

Tactic:
ring

Goal state after:
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: p n : ℕ
hp : p ∈ n.primeFactors
hs : IsSquare (-1)
y : ZMod p
h : y ^ 2 = -1
⊢ -1 = -1 ^ 2

Tactic:
ring

Goal state after:
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: n x y : ℕ
h : n = x ^ 2 + y ^ 2
hxy : ¬(x = 0 ∧ y = 0)
hg : 0 < x.gcd y
g x₁ y₁ : ℕ
left✝ : 0 < g
h₂ : x₁.Coprime y₁
h₃ : x = x₁ * g
h₄ : y = y₁ * g
⊢ (x₁ * g) ^ 2 + (y₁ * g) ^ 2 = g ^ 2 * (x₁ ^ 2 + y₁ ^ 2)

Tactic:
ring

Goal state after:
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: n a b : ℕ
h₁ : n = a ^ 2 * b
h₂ : IsSquare (-1)
x' y' : ℕ
h : b = x' ^ 2 + y' ^ 2
⊢ a ^ 2 * (x' ^ 2 + y' ^ 2) = (a * x') ^ 2 + (a * y') ^ 2

Tactic:
ring

Goal state after:
Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart

Goal state before:
pp: case e'_9
p : ℂ[X]
s : ℂ
x : ℝ
h₀ : HasDerivAt (fun y ↦ y • s) (1 • s) x
h₁ : HasDerivAt (fun x ↦ cexp (-(x • s))) (cexp (-(x • s)) * -(1 • s)) x
h₂ : HasDerivAt ((fun x ↦ eval x (sumIDeriv p)) ∘ fun y ↦ y • s) (eval (x • s) (derivative (sumIDeriv p)) * 1 • s) x
⊢ s * (cexp (-(x • s)) * eval (x • s) p) =
    -(cexp (-(x • s)) * -s * (eval (x • s) p + eval (x • s) (derivative (sumIDeriv p))) +
        cexp (-(x • s)) * (eval (x • s) (derivative (sumIDeriv p)) * s))

Tactic:
ring

Goal state after:
Module: Mathlib.NumberTheory.SumFourSquares

Goal state before:
pp: p : ℕ
hp : Prime p
this✝ : Fact (Prime p)
natAbs_iff :
  ∀ {a b c d : ℤ} {k : ℕ},
    a.natAbs ^ 2 + b.natAbs ^ 2 + c.natAbs ^ 2 + d.natAbs ^ 2 = k ↔ a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = ↑k
hm✝ : ∃ m < p, 0 < m ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p
m : ℕ
hmin : ∀ m_1 < m, ¬(m_1 < p ∧ 0 < m_1 ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m_1 * p)
hmp : m < p
hm₀ : 0 < m
hm₁ : 1 < m
this : NeZero m
hm : ¬2 ∣ m
f : ℕ → ℤ
hf_lt : ∀ (x : ℕ), 2 * (f x).natAbs < m
hf_mod : ∀ (x : ℕ), ↑(f x) = ↑x
a b c d : ℕ
habcd : (m * a) ^ 2 + (m * b) ^ 2 + (m * c) ^ 2 + (m * d) ^ 2 = m * p
hr : f (m * a) = 0 ∧ f (m * b) = 0 ∧ f (m * c) = 0 ∧ f (m * d) = 0
⊢ (m * a) ^ 2 + (m * b) ^ 2 + (m * c) ^ 2 + (m * d) ^ 2 = m * m * (a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2)

Tactic:
ring

Goal state after:
Module: Mathlib.NumberTheory.RamificationInertia.Basic

Goal state before:
pp: case h
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : Ideal R
P : Ideal S
hfp : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
i : ℕ
a : S
a_mem : a ∈ P ^ i
x : R
y : S
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
ring

Goal state after:
Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic

Goal state before:
pp: case hbc
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
h : ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ f.natDegree * (|x - ↑a / (↑b + 1)| * A)
r : ℕ
hn : A < (1 + 1) ^ r
a b : ℤ
b1 : 1 < b
a1 : ↑b ^ r * (↑b ^ f.natDegree * |x - ↑a / ↑b|) < 1
b0 : 0 < ↑b
⊢ (1 + 1) ^ r ≤ ↑b ^ r

Tactic:
one_add_one_eq_two

Goal state after:
case hbc
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
h : ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ f.natDegree * (|x - ↑a / (↑b + 1)| * A)
r : ℕ
hn : A < (1 + 1) ^ r
a b : ℤ
b1 : 1 < b
a1 : ↑b ^ r * (↑b ^ f.natDegree * |x - ↑a / ↑b|) < 1
b0 : 0 < ↑b
⊢ 2 ^ r ≤ ↑b ^ r
Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart

Goal state before:
pp: f : ℤ[X]
hf : eval 0 f ≠ 0
c' : ℂ → ℝ
c'0 : ∀ (s : ℂ), c' s ≥ 0
Pp'_le : ∀ (s : ℂ) (p : ℕ), p ≠ 0 → ‖P (map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p)) s‖ ≤ c' s ^ p
p : ℕ
p_gt : p > (eval 0 f).natAbs
prime_p : Nat.Prime p
gp' : ℤ[X]
h' : eval 0 (sumIDeriv (X ^ (p - 1) * f ^ p)) = (p - 1)! • eval 0 (f ^ p) + p ! • eval 0 gp'
gp : ℤ[X]
gp'_le : gp.natDegree ≤ (X ^ (p - 1) * f ^ p).natDegree - p
r : ℂ
h : (aeval r) (sumIDeriv (X ^ (p - 1) * f ^ p)) = ↑p ! * (aeval r) gp
hr : r ∈ f.aroots ℂ
⊢ ((↑(eval 0 f) ^ p + ↑p * ↑(eval 0 gp')) * cexp r - ↑p * (aeval r) gp) * ↑(p - 1)! =
    ↑(eval 0 f) ^ p * cexp r * ↑(p - 1)! + ↑p * ↑(p - 1)! * (↑(eval 0 gp') * cexp r - (aeval r) gp)

Tactic:
ring

Goal state after:
Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart

Goal state before:
pp: f : ℤ[X]
hf : eval 0 f ≠ 0
c' : ℂ → ℝ
c'0 : ∀ (s : ℂ), c' s ≥ 0
Pp'_le : ∀ (s : ℂ) (p : ℕ), p ≠ 0 → ‖P (map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p)) s‖ ≤ c' s ^ p
p : ℕ
p_gt : p > (eval 0 f).natAbs
prime_p : Nat.Prime p
gp' : ℤ[X]
h' : eval 0 (sumIDeriv (X ^ (p - 1) * f ^ p)) = (p - 1)! • eval 0 (f ^ p) + p ! • eval 0 gp'
gp : ℤ[X]
gp'_le : gp.natDegree ≤ (X ^ (p - 1) * f ^ p).natDegree - p
r : ℂ
h : (aeval r) (sumIDeriv (X ^ (p - 1) * f ^ p)) = ↑p ! * (aeval r) gp
hr : r ∈ f.aroots ℂ
this :
  (↑(eval 0 f ^ p + ↑p * eval 0 gp') * cexp r - ↑p * (aeval r) gp) * ↑(p - 1)! =
    ↑(eval 0 f) ^ p * cexp r * ↑(p - 1)! + ↑(p * (p - 1)!) * (↑(eval 0 gp') * cexp r - (aeval r) gp)
⊢ ↑(eval 0 f) ^ p * cexp r * ↑(p - 1)! +
      (↑p ! * (↑(eval 0 gp') * cexp r) - (aeval r) (sumIDeriv (X ^ (p - 1) * f ^ p))) =
    (↑(p - 1)! * ↑(eval 0 f) ^ p + ↑p ! * ↑(eval 0 gp')) * cexp r - (aeval r) (sumIDeriv (X ^ (p - 1) * f ^ p))

Tactic:
ring

Goal state after:
Module: Mathlib.NumberTheory.Wilson

Goal state before:
pp: case refine_4
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
⊢ ∀ a ∈ univ, ↑a = ↑(↑a).val

Tactic:
rintro a -; simp only [cast_id, natCast_val]

Goal state after:
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

Goal state before:
pp: p x : ℝ
r : ℚ
⊢ LiouvilleWith p (↑r + x) ↔ LiouvilleWith p x

Tactic:
by rw [add_comm, add_rat_iff]

Goal state after:
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

Goal state before:
pp: p x C : ℝ
hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
⊢ -↑m / ↑n - -x = x - ↑m / ↑n

Tactic:
ring

Goal state after:
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

Goal state before:
pp: case inl
p : ℝ
hp : 1 < p
h : LiouvilleWith p ↑0
⊢ False

Tactic:
refine h.ne_cast_int hp 0 ?_

Goal state after:
case inl
p : ℝ
hp : 1 < p
h : LiouvilleWith p ↑0
⊢ ↑0 = ↑0
Module: Mathlib.Order.CompleteSublattice

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
L : CompleteSublattice α
ι : Sort u_3
f : ι → ↥L
⊢ ↑(iSup f) = ⨆ i, ↑(f i)

Tactic:
rw [iSup, coe_sSup', iSup_range]

Goal state after:
Module: Mathlib.Order.Concept

Goal state before:
pp: α : Type u_2
β : Type u_3
r : α → β → Prop
c d : Concept α β r
h : c.intent = d.intent
⊢ c = d

Tactic:
obtain ⟨s₁, t₁, _, rfl⟩ := c

Goal state after:
α : Type u_2
β : Type u_3
r : α → β → Prop
d : Concept α β r
t₁ : Set β
upperPolar_extent✝ : upperPolar r (lowerPolar r t₁) = t₁
h :
  { extent := lowerPolar r t₁, intent := t₁, upperPolar_extent := upperPolar_extent✝, lowerPolar_intent := ⋯ }.intent =
    d.intent
⊢ { extent := lowerPolar r t₁, intent := t₁, upperPolar_extent := upperPolar_extent✝, lowerPolar_intent := ⋯ } = d
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: α : Type u_2
s : Set α
inst✝ : CompleteLattice α
hs : CountableSupClosed s
A : Set α
hA_c : A.Countable
hA_ne : A.Nonempty
hA : ∀ a ∈ A, a ∈ s
⊢ sSup A ∈ s

Tactic:
by
  rw [sSup_eq_iSup']
  have : Countable A := hA_c
  have : Nonempty A := nonempty_coe_sort.mpr hA_ne
  exact hs.iSup_mem fun a ↦ hA a a.2

Goal state after:
Module: Mathlib.Order.Filter.ListTraverse

Goal state before:
pp: case mp
α β : Type u
f : β → Filter α
fs : List β
t : Set (List α)
⊢ t ∈ traverse f fs → ∃ us, Forall₂ (fun b s ↦ s ∈ f b) fs us ∧ sequence us ⊆ t

Tactic:
induction fs generalizing t with

Goal state after:
Module: Mathlib.Order.Fin.InsertNth

Goal state before:
pp: case inr.inl
n : ℕ
α : Type u_1
inst✝ : Preorder α
f : Fin (n + 1) → α
hf : Monotone f
i : Fin n
x : α
hx₁ : f i.castSucc ≤ x
hx₂ : x ≤ f i.succ
⊢ i.castSucc.succ.insertNth x f i.castSucc.castSucc ≤ i.castSucc.succ.insertNth x f i.castSucc.succ

Tactic:
← succAbove_succ_self i.castSucc,

Goal state after:
case inr.inl
n : ℕ
α : Type u_1
inst✝ : Preorder α
f : Fin (n + 1) → α
hf : Monotone f
i : Fin n
x : α
hx₁ : f i.castSucc ≤ x
hx₂ : x ≤ f i.succ
⊢ i.castSucc.succ.insertNth x f (i.castSucc.succ.succAbove i.castSucc) ≤ i.castSucc.succ.insertNth x f i.castSucc.succ
Module: Mathlib.Order.Fin.InsertNth

Goal state before:
pp: case inr.inl
n : ℕ
α : Type u_1
inst✝ : Preorder α
f : Fin (n + 1) → α
hf : Monotone f
i : Fin n
x : α
hx₁ : f i.castSucc ≤ x
hx₂ : x ≤ f i.succ
⊢ i.castSucc.succ.insertNth x f i.castSucc.castSucc ≤ i.castSucc.succ.insertNth x f i.castSucc.succ

pp: case inr.inr
n : ℕ
α : Type u_1
inst✝ : Preorder α
f : Fin (n + 1) → α
hf : Monotone f
i : Fin n
x : α
hx₁ : f i.castSucc ≤ x
hx₂ : x ≤ f i.succ
j : Fin (n + 1)
hj : i.castSucc < j
⊢ i.castSucc.succ.insertNth x f j.castSucc ≤ i.castSucc.succ.insertNth x f j.succ

Tactic:
· rwa [← succAbove_succ_self i.castSucc, insertNth_apply_succAbove, insertNth_apply_same]

Goal state after:
case inr.inr
n : ℕ
α : Type u_1
inst✝ : Preorder α
f : Fin (n + 1) → α
hf : Monotone f
i : Fin n
x : α
hx₁ : f i.castSucc ≤ x
hx₂ : x ≤ f i.succ
j : Fin (n + 1)
hj : i.castSucc < j
⊢ i.castSucc.succ.insertNth x f j.castSucc ≤ i.castSucc.succ.insertNth x f j.succ
Module: Mathlib.Order.Fin.InsertNth

Goal state before:
pp: case inr.inl
n : ℕ
α : Type u_1
inst✝ : Preorder α
f : Fin (n + 1) → α
hf : ∀ (i : Fin n), f i.castSucc < f i.succ
i : Fin n
x : α
hx₁ : f i.castSucc < x
hx₂ : x < f i.succ
⊢ i.castSucc.succ.insertNth x f i.castSucc.castSucc < i.castSucc.succ.insertNth x f i.castSucc.succ

Tactic:
← succAbove_succ_self i.castSucc,

Goal state after:
case inr.inl
n : ℕ
α : Type u_1
inst✝ : Preorder α
f : Fin (n + 1) → α
hf : ∀ (i : Fin n), f i.castSucc < f i.succ
i : Fin n
x : α
hx₁ : f i.castSucc < x
hx₂ : x < f i.succ
⊢ i.castSucc.succ.insertNth x f (i.castSucc.succ.succAbove i.castSucc) < i.castSucc.succ.insertNth x f i.castSucc.succ
Module: Mathlib.Order.Fin.InsertNth

Goal state before:
pp: case inr.inl
n : ℕ
α : Type u_1
inst✝ : Preorder α
f : Fin (n + 1) → α
hf : ∀ (i : Fin n), f i.castSucc < f i.succ
i : Fin n
x : α
hx₁ : f i.castSucc < x
hx₂ : x < f i.succ
⊢ i.castSucc.succ.insertNth x f i.castSucc.castSucc < i.castSucc.succ.insertNth x f i.castSucc.succ

pp: case inr.inr
n : ℕ
α : Type u_1
inst✝ : Preorder α
f : Fin (n + 1) → α
hf : ∀ (i : Fin n), f i.castSucc < f i.succ
i : Fin n
x : α
hx₁ : f i.castSucc < x
hx₂ : x < f i.succ
j : Fin (n + 1)
hj : i.castSucc < j
⊢ i.castSucc.succ.insertNth x f j.castSucc < i.castSucc.succ.insertNth x f j.succ

Tactic:
· rwa [← succAbove_succ_self i.castSucc, insertNth_apply_succAbove, insertNth_apply_same]

Goal state after:
case inr.inr
n : ℕ
α : Type u_1
inst✝ : Preorder α
f : Fin (n + 1) → α
hf : ∀ (i : Fin n), f i.castSucc < f i.succ
i : Fin n
x : α
hx₁ : f i.castSucc < x
hx₂ : x < f i.succ
j : Fin (n + 1)
hj : i.castSucc < j
⊢ i.castSucc.succ.insertNth x f j.castSucc < i.castSucc.succ.insertNth x f j.succ
Module: Mathlib.Order.Height

Goal state before:
pp: α : Type u_1
s : Set α
r : α → α → Prop
hc :
  ((⇑(Subtype.relEmbedding (fun x1 x2 ↦ r x1 x2) fun x ↦ x ∈ s) '' univ).chainHeight fun x1 x2 ↦ r x1 x2) =
    univ.chainHeight (Subtype.val ⁻¹'o fun x1 x2 ↦ r x1 x2)
⊢ (univ.chainHeight fun x1 x2 ↦ r ↑x1 ↑x2) = s.chainHeight r

Tactic:
have hs : Subtype.val ⁻¹'o (r · ·) = (fun x y : s ↦ r x y) := by funext; simp

Goal state after:
α : Type u_1
s : Set α
r : α → α → Prop
hc :
  ((⇑(Subtype.relEmbedding (fun x1 x2 ↦ r x1 x2) fun x ↦ x ∈ s) '' univ).chainHeight fun x1 x2 ↦ r x1 x2) =
    univ.chainHeight (Subtype.val ⁻¹'o fun x1 x2 ↦ r x1 x2)
hs : (Subtype.val ⁻¹'o fun x1 x2 ↦ r x1 x2) = fun x y ↦ r ↑x ↑y
⊢ (univ.chainHeight fun x1 x2 ↦ r ↑x1 ↑x2) = s.chainHeight r
Module: Mathlib.Order.Lattice.Congruence

Goal state before:
pp: α : Type u_2
inst✝ : Lattice α
r : α → α → Prop
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₃ : ∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
x y z : α
hxy : r x y
hyz : r y z
⊢ x ≤ x ⊔ y ⊔ z

Tactic:
by simp [sup_assoc, le_sup_left]

Goal state after:
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝ : Frame X
n m : Nucleus X
x y : X
a : ↑(range ⇑n)
s : Set ↑(range ⇑n)
⊢ ↑a ⊓ n (sSup (Subtype.val '' s)) ≤ ↑(rangeFactorization (⇑n) (sSup (Subtype.val '' range fun x ↦ a ⊓ ↑x)))

Tactic:
← mem_range.1 a.prop,

Goal state after:
X : Type u_1
inst✝ : Frame X
n m : Nucleus X
x y : X
a : ↑(range ⇑n)
s : Set ↑(range ⇑n)
⊢ n ↑a ⊓ n (sSup (Subtype.val '' s)) ≤ ↑(rangeFactorization (⇑n) (sSup (Subtype.val '' range fun x ↦ a ⊓ ↑x)))
Module: Mathlib.Order.SuccPred.Tree

Goal state before:
pp: case right
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
hr : r ≠ ⊥
⊢ ∀ b < findAtom r, b = ⊥

Tactic:
intro b hb
    apply Order.le_pred_of_lt at hb
    simpa using hb

Goal state after:
Module: Mathlib.Probability.Process.Adapted

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
β : Type u_3
u : ι → Ω → β
mi : MeasurableSpace ι
mβ : MeasurableSpace β
h : IsProgressive f u
⊢ Adapted f u

Tactic:
by
  intro i
  have : u i = (fun p : Set.Iic i × Ω => u p.1 p.2) ∘ fun x => (⟨i, Set.mem_Iic.mpr le_rfl⟩, x) :=
    rfl
  rw [this]
  exact (h i).comp measurable_prodMk_left

Goal state after: