mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.Padics.WithVal

Goal state before:
pp: case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp0' : 0 < ↑p
hp0 : 0 < (↑p)⁻¹
hp1' : 1 < ↑p
hp1 : (↑p)⁻¹ < 1
n : ℕ
hn : Valued.v (↑p ^ n) = exp (-↑n)
x y : WithVal (Rat.padicValuation p)
x' : ℚ := (WithVal.equiv (Rat.padicValuation p)) x
hx : x' = (WithVal.equiv (Rat.padicValuation p)) x
y' : ℚ := (WithVal.equiv (Rat.padicValuation p)) y
hy : y' = (WithVal.equiv (Rat.padicValuation p)) y
h : (Rat.padicValuation p) (x' - y') < exp (-↑n)
⊢ padicNorm p ((WithVal.equiv (Rat.padicValuation p)) (x - y)) ≤ (↑(p ^ n))⁻¹

Tactic:
map_sub,

Goal state after:
case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp0' : 0 < ↑p
hp0 : 0 < (↑p)⁻¹
hp1' : 1 < ↑p
hp1 : (↑p)⁻¹ < 1
n : ℕ
hn : Valued.v (↑p ^ n) = exp (-↑n)
x y : WithVal (Rat.padicValuation p)
x' : ℚ := (WithVal.equiv (Rat.padicValuation p)) x
hx : x' = (WithVal.equiv (Rat.padicValuation p)) x
y' : ℚ := (WithVal.equiv (Rat.padicValuation p)) y
hy : y' = (WithVal.equiv (Rat.padicValuation p)) y
h : (Rat.padicValuation p) (x' - y') < exp (-↑n)
⊢ padicNorm p ((WithVal.equiv (Rat.padicValuation p)) x - (WithVal.equiv (Rat.padicValuation p)) y) ≤ (↑(p ^ n))⁻¹
Module: Mathlib.NumberTheory.Padics.WithVal

Goal state before:
pp: case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp0' : 0 < ↑p
hp0 : 0 < (↑p)⁻¹
hp1' : 1 < ↑p
hp1 : (↑p)⁻¹ < 1
γ : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ
x y : WithVal (Rat.padicValuation p)
h : ↑(padicNorm p ((WithVal.equiv (Rat.padicValuation p)) (x - y))) ≤ (↑p ^ (embedding ↑γ * exp (-1)).log.natAbs)⁻¹
x' : ℚ := (WithVal.equiv (Rat.padicValuation p)) x
hx : x' = (WithVal.equiv (Rat.padicValuation p)) x
y' : ℚ := (WithVal.equiv (Rat.padicValuation p)) y
hy : y' = (WithVal.equiv (Rat.padicValuation p)) y
⊢ Valued.v.restrict (y - x) < ↑γ

Tactic:
Valuation.map_sub_swap,

Goal state after:
case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp0' : 0 < ↑p
hp0 : 0 < (↑p)⁻¹
hp1' : 1 < ↑p
hp1 : (↑p)⁻¹ < 1
γ : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ
x y : WithVal (Rat.padicValuation p)
h : ↑(padicNorm p ((WithVal.equiv (Rat.padicValuation p)) (x - y))) ≤ (↑p ^ (embedding ↑γ * exp (-1)).log.natAbs)⁻¹
x' : ℚ := (WithVal.equiv (Rat.padicValuation p)) x
hx : x' = (WithVal.equiv (Rat.padicValuation p)) x
y' : ℚ := (WithVal.equiv (Rat.padicValuation p)) y
hy : y' = (WithVal.equiv (Rat.padicValuation p)) y
⊢ Valued.v.restrict (x - y) < ↑γ
Module: Mathlib.NumberTheory.PowModTotient

Goal state before:
pp: case succ
x k n : ℕ
hn : 1 < n
h : x.Coprime n
l : ℕ
ih : x ^ (k + l * φ n) % n = x ^ k % n
⊢ x ^ (k + (l + 1) * φ n) % n = x ^ k % n

Tactic:
| succ l ih =>

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a : Solution₁ d
h : IsFundamental a
n : ℤ
hn : 0 ≤ n
⊢ (a ^ n).y < (a ^ (n + 1)).y

Tactic:
← sub_pos,

Goal state after:
d : ℤ
a : Solution₁ d
h : IsFundamental a
n : ℤ
hn : 0 ≤ n
⊢ 0 < (a ^ (n + 1)).y - (a ^ n).y
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

Goal state before:
pp: case f
K : Type u_1
Γ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝ : IsTrivialOn K v
hlt : 1 < v X
p q : K[X]
hq : q ≠ 0
hf : (algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q ≠ 0
⊢ v ((algebraMap K[X] K⟮X⟯) p) / v ((algebraMap K[X] K⟮X⟯) q) = v X ^ p.natDegree / v X ^ q.natDegree

Tactic:
← coePolynomial_eq_algebraMap

Goal state after:
case f
K : Type u_1
Γ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝ : IsTrivialOn K v
hlt : 1 < v X
p q : K[X]
hq : q ≠ 0
hf : (algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q ≠ 0
⊢ v ↑p / v ↑q = v X ^ p.natDegree / v X ^ q.natDegree
Module: Mathlib.NumberTheory.RamificationInertia.Basic

Goal state before:
pp: case refine_1.calc_1
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
span_d : Submodule.restrictScalars R (S ∙ f A.det) ≤ M
this : Nontrivial (R ⧸ p)
i j : Fin n
⊢ (Quotient.mk p).mapMatrix (Matrix.of A' - 1) i j = (Quotient.mk p) (A' i j) - 1 i j

Tactic:
map_sub,

Goal state after:
case refine_1.calc_1
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
span_d : Submodule.restrictScalars R (S ∙ f A.det) ≤ M
this : Nontrivial (R ⧸ p)
i j : Fin n
⊢ ((Quotient.mk p).mapMatrix (Matrix.of A') - (Quotient.mk p).mapMatrix 1) i j = (Quotient.mk p) (A' i j) - 1 i j
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
⊢ (∑ d ∈ s.support, if s.prodPrimes.Coprime d then s.weights d else 0) =
    ∑ x ∈ s.support, if s.prodPrimes.gcd x = 1 then s.weights x else s.weights x * 0

Tactic:
mul_zero

Goal state after:
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

Goal state before:
pp: case left
K : Type u_1
Γ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝¹ : v.IsNontrivial
inst✝ : IsTrivialOn K v
hle : v X ≤ 1
p : K[X]
hp : p ≠ 0
π : K[X] := ⋯
hne : {p | v ↑p < 1 ∧ p ≠ 0}.Nonempty
hπirr : Irreducible π
k : ℕ
q : K[X]
hnq : ¬q % π = 0
heq : p = π ^ k * q
hπ : v ↑π < 1 ∧ ¬π = 0
⊢ v ((algebraMap K[X] K⟮X⟯) (q % π)) = 1

Tactic:
← coePolynomial_eq_algebraMap

Goal state after:
case left
K : Type u_1
Γ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝¹ : v.IsNontrivial
inst✝ : IsTrivialOn K v
hle : v X ≤ 1
p : K[X]
hp : p ≠ 0
π : K[X] := πᵥ
hne : {p | v ↑p < 1 ∧ p ≠ 0}.Nonempty
hπirr : Irreducible π
k : ℕ
q : K[X]
hnq : ¬q % π = 0
heq : p = π ^ k * q
hπ : v ↑π < 1 ∧ ¬π = 0
⊢ v ↑(q % π) = 1
Module: Mathlib.NumberTheory.SumFourSquares

Goal state before:
pp: case inr.refine_1
p : ℕ
hp : Fact (Nat.Prime p)
hodd : Odd p
a b : ℕ
ha : a ≤ p / 2
hb : b ≤ p / 2
hab : ↑a ^ 2 + ↑b ^ 2 ≡ -1 [ZMOD ↑p]
k : ℕ
hk₀ : 0 < ↑k
hk : a ^ 2 + b ^ 2 + 1 ^ 2 + 0 ^ 2 = k * p
⊢ 2 * a < p

pp: case inr.refine_2
p : ℕ
hp : Fact (Nat.Prime p)
hodd : Odd p
a b : ℕ
ha : a ≤ p / 2
hb : b ≤ p / 2
hab : ↑a ^ 2 + ↑b ^ 2 ≡ -1 [ZMOD ↑p]
k : ℕ
hk₀ : 0 < ↑k
hk : a ^ 2 + b ^ 2 + 1 ^ 2 + 0 ^ 2 = k * p
⊢ 2 * b < p

pp: case inr.refine_3
p : ℕ
hp : Fact (Nat.Prime p)
hodd : Odd p
a b : ℕ
ha : a ≤ p / 2
hb : b ≤ p / 2
hab : ↑a ^ 2 + ↑b ^ 2 ≡ -1 [ZMOD ↑p]
k : ℕ
hk₀ : 0 < ↑k
hk : a ^ 2 + b ^ 2 + 1 ^ 2 + 0 ^ 2 = k * p
⊢ 2 * 1 < p

pp: case inr.refine_4
p : ℕ
hp : Fact (Nat.Prime p)
hodd : Odd p
a b : ℕ
ha : a ≤ p / 2
hb : b ≤ p / 2
hab : ↑a ^ 2 + ↑b ^ 2 ≡ -1 [ZMOD ↑p]
k : ℕ
hk₀ : 0 < ↑k
hk : a ^ 2 + b ^ 2 + 1 ^ 2 + 0 ^ 2 = k * p
⊢ 2 * 0 < p

Tactic:
· exact (mul_le_mul' le_rfl ha).trans_lt (Nat.mul_div_lt_iff_not_dvd.2 hodd.not_two_dvd_nat)

Goal state after:
case inr.refine_2
p : ℕ
hp : Fact (Nat.Prime p)
hodd : Odd p
a b : ℕ
ha : a ≤ p / 2
hb : b ≤ p / 2
hab : ↑a ^ 2 + ↑b ^ 2 ≡ -1 [ZMOD ↑p]
k : ℕ
hk₀ : 0 < ↑k
hk : a ^ 2 + b ^ 2 + 1 ^ 2 + 0 ^ 2 = k * p
⊢ 2 * b < p

case inr.refine_3
p : ℕ
hp : Fact (Nat.Prime p)
hodd : Odd p
a b : ℕ
ha : a ≤ p / 2
hb : b ≤ p / 2
hab : ↑a ^ 2 + ↑b ^ 2 ≡ -1 [ZMOD ↑p]
k : ℕ
hk₀ : 0 < ↑k
hk : a ^ 2 + b ^ 2 + 1 ^ 2 + 0 ^ 2 = k * p
⊢ 2 * 1 < p

case inr.refine_4
p : ℕ
hp : Fact (Nat.Prime p)
hodd : Odd p
a b : ℕ
ha : a ≤ p / 2
hb : b ≤ p / 2
hab : ↑a ^ 2 + ↑b ^ 2 ≡ -1 [ZMOD ↑p]
k : ℕ
hk₀ : 0 < ↑k
hk : a ^ 2 + b ^ 2 + 1 ^ 2 + 0 ^ 2 = k * p
⊢ 2 * 0 < p
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
w : ℕ → ℝ
⊢ (∑ y ∈ s.prodPrimes.divisors,
      ∑ x ∈ s.prodPrimes.divisors,
        ∑ d2 ∈ s.prodPrimes.divisors,
          if x ∣ y.gcd d2 then (selbergTerms x)⁻¹ * (s.nu y * w y) * (s.nu d2 * w d2) else 0) =
    ∑ d1 ∈ s.prodPrimes.divisors,
      ∑ d2 ∈ s.prodPrimes.divisors,
        ∑ l ∈ s.prodPrimes.divisors,
          if l ∣ d1.gcd d2 then (selbergTerms l)⁻¹ * (s.nu d1 * w d1) * (s.nu d2 * w d2) else 0

Tactic:
sum_congr rfl fun _ _ ↦ sum_comm

Goal state after:
s : BoundingSieve
w : ℕ → ℝ
⊢ (∑ x ∈ s.prodPrimes.divisors,
      ∑ y ∈ s.prodPrimes.divisors,
        ∑ x_1 ∈ s.prodPrimes.divisors,
          if x_1 ∣ x.gcd y then (selbergTerms x_1)⁻¹ * (s.nu x * w x) * (s.nu y * w y) else 0) =
    ∑ d1 ∈ s.prodPrimes.divisors,
      ∑ d2 ∈ s.prodPrimes.divisors,
        ∑ l ∈ s.prodPrimes.divisors,
          if l ∣ d1.gcd d2 then (selbergTerms l)⁻¹ * (s.nu d1 * w d1) * (s.nu d2 * w d2) else 0
Module: Mathlib.NumberTheory.RamificationInertia.Basic

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

Tactic:
map_sub,

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

Goal state before:
pp: 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)
inst✝¹ : IsDedekindDomain S
inst✝ : P.IsPrime
hP : P ≠ ⊥
i : ℕ
hi : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
a : S
a_mem : a ∈ (fun x ↦ P ^ x) i
a_notMem : a ∉ (fun x ↦ P ^ x) i.succ
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
refine (LinearEquiv.ofBijective ?_ ⟨?_, ?_⟩).symm

Goal state after:
case refine_1
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)
inst✝¹ : IsDedekindDomain S
inst✝ : P.IsPrime
hP : P ≠ ⊥
i : ℕ
hi : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
a : S
a_mem : a ∈ (fun x ↦ P ^ x) i
a_notMem : a ∉ (fun x ↦ P ^ x) i.succ
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

case refine_2
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)
inst✝¹ : IsDedekindDomain S
inst✝ : P.IsPrime
hP : P ≠ ⊥
i : ℕ
hi : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
a : S
a_mem : a ∈ (fun x ↦ P ^ x) i
a_notMem : a ∉ (fun x ↦ P ^ x) i.succ
⊢ Function.Injective ⇑?refine_1

case refine_3
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)
inst✝¹ : IsDedekindDomain S
inst✝ : P.IsPrime
hP : P ≠ ⊥
i : ℕ
hi : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
a : S
a_mem : a ∈ (fun x ↦ P ^ x) i
a_notMem : a ∉ (fun x ↦ P ^ x) i.succ
⊢ Function.Surjective ⇑?refine_1
Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic

Goal state before:
pp: case refine_2
α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fR : ℝ[X] := map (algebraMap ℤ ℝ) f
fa : eval α fR = 0
fR0 : fR ≠ 0
ar : α ∈ ↑fR.roots.toFinset
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ ↑fR.roots.toFinset = {α}
xm : ℝ
hM : IsMaxOn (fun x ↦ |eval x (derivative fR)|) (Icc (α - ζ) (α + ζ)) xm
y : ℝ
hy : y ∈ Icc (α - ζ) (α + ζ)
⊢ |α - α| ≤ ζ

Tactic:
exact @mem_closedBall_self ℝ _ α ζ (le_of_lt z0)

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

Goal state before:
pp: case calc_2
R : Type u
inst✝¹⁶ : CommRing R
S : Type v
inst✝¹⁵ : CommRing S
inst✝¹⁴ : Algebra R S
inst✝¹³ : IsDedekindDomain S
K : Type u_1
L : Type u_2
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : IsDedekindDomain R
inst✝⁹ : Algebra R K
inst✝⁸ : IsFractionRing R K
inst✝⁷ : Algebra S L
inst✝⁶ : IsFractionRing S L
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R S L
inst✝² : IsScalarTower R K L
inst✝¹ : Module.Finite R S
p : Ideal R
inst✝ : p.IsMaximal
hp0 : p ≠ ⊥
e : Ideal S → ℕ := p.ramificationIdx'
⊢ ¬p ≤ ⊥

Tactic:
le_bot_iff

Goal state after:
case calc_2
R : Type u
inst✝¹⁶ : CommRing R
S : Type v
inst✝¹⁵ : CommRing S
inst✝¹⁴ : Algebra R S
inst✝¹³ : IsDedekindDomain S
K : Type u_1
L : Type u_2
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : IsDedekindDomain R
inst✝⁹ : Algebra R K
inst✝⁸ : IsFractionRing R K
inst✝⁷ : Algebra S L
inst✝⁶ : IsFractionRing S L
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R S L
inst✝² : IsScalarTower R K L
inst✝¹ : Module.Finite R S
p : Ideal R
inst✝ : p.IsMaximal
hp0 : p ≠ ⊥
e : Ideal S → ℕ := p.ramificationIdx'
⊢ ¬p = ⊥
Module: Mathlib.NumberTheory.Wilson

Goal state before:
pp: case refine_1.left
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
a : (ZMod p)ˣ
ha : a ∈ univ
⊢ 1 ≤ (↑a).val

Tactic:
apply Nat.pos_of_ne_zero; rw [← @val_zero p]
      intro h; apply Units.ne_zero a (val_injective p h)

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

Goal state before:
pp: n : ℕ
hn : 1 ≤ n
⊢ volume {x | ∃ᶠ (b : ℕ) in atTop, ∃ a ∈ Finset.Icc 0 ↑b, |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n)} = 0

Tactic:
generalize hr : (2 + 1 / n : ℝ) = r

Goal state after:
n : ℕ
hn : 1 ≤ n
r : ℝ
hr : 2 + 1 / ↑n = r
⊢ volume {x | ∃ᶠ (b : ℕ) in atTop, ∃ a ∈ Finset.Icc 0 ↑b, |x - ↑a / ↑b| < 1 / ↑b ^ r} = 0
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

Goal state before:
pp: case hab
p : ℝ
hp : 1 < p
M : ℤ
h : LiouvilleWith p ↑M
n : ℕ
hn : 0 < n
m : ℤ
hne : ↑M ≠ ↑m / ↑n
hlt : |↑M - ↑m / ↑n| < ↑n ^ (-1)
hn' : 0 < ↑n
⊢ M * ↑n - m ≠ 0

Tactic:
sub_ne_zero

Goal state after:
case hab
p : ℝ
hp : 1 < p
M : ℤ
h : LiouvilleWith p ↑M
n : ℕ
hn : 0 < n
m : ℤ
hne : ↑M ≠ ↑m / ↑n
hlt : |↑M - ↑m / ↑n| < ↑n ^ (-1)
hn' : 0 < ↑n
⊢ M * ↑n ≠ m
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: case mpr
δ : ℝ
x : UnitAddCircle
n : ℕ
hn : 0 < n
m : ℕ
hm₁ : m < n
hm₂ : gcd m n = 1
hx : ‖x - ↑(↑m / ↑n)‖ < δ
⊢ ∃ b, (∃ m < n, m.gcd n = 1 ∧ ↑(↑m / ↑n) = b) ∧ ‖x - b‖ < δ

Tactic:
exact ⟨↑((m : ℝ) / n), ⟨m, hm₁, hm₂, rfl⟩, hx⟩

Goal state after:
Module: Mathlib.Order.CompleteSublattice

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
f : CompleteLatticeHom α β
L✝ : CompleteSublattice α
L : CompleteSublattice β
s : Set α
hs : s ⊆ ⇑f ⁻¹' ↑L
⊢ sSup s ∈ ⇑f ⁻¹' ↑L

Tactic:
simpa only [mem_preimage, map_sSup, SetLike.mem_coe] using sSupClosed
      <| mapsTo_iff_image_subset.mp hs

Goal state after:
Module: Mathlib.Order.Concept

Goal state before:
pp: α : Type u_2
β : Type u_3
r : α → β → Prop
s s' : Set α
h : IsExtent r s
hs' : s' ⊆ s
⊢ lowerPolar r (upperPolar r s') ⊆ s

Tactic:
← h.eq

Goal state after:
α : Type u_2
β : Type u_3
r : α → β → Prop
s s' : Set α
h : IsExtent r s
hs' : s' ⊆ s
⊢ lowerPolar r (upperPolar r s') ⊆ lowerPolar r (upperPolar r s)
Module: Mathlib.Order.Concept

Goal state before:
pp: α : Type u_2
β : Type u_3
r : α → β → Prop
t t' : Set β
h : IsIntent r t
ht' : t' ⊆ t
⊢ upperPolar r (lowerPolar r t') ⊆ t

Tactic:
← h.eq

Goal state after:
α : Type u_2
β : Type u_3
r : α → β → Prop
t t' : Set β
h : IsIntent r t
ht' : t' ⊆ t
⊢ upperPolar r (lowerPolar r t') ⊆ upperPolar r (lowerPolar r t)
Module: Mathlib.Order.Completion

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : PartialOrder β
f : β ↪o α
A B : DedekindCut β
h : sSup (⇑f '' A.left) ≤ sSup (⇑f '' B.left)
x : β
hx : x ∈ A.extent
⊢ x ∈ lowerBounds B.right

Tactic:
simp_rw [le_sSup_iff, sSup_le_iff, forall_mem_image] at h

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : PartialOrder β
f : β ↪o α
A B : DedekindCut β
x : β
hx : x ∈ A.extent
h : ∀ b ∈ upperBounds (⇑f '' B.left), ∀ ⦃x : β⦄, x ∈ A.left → f x ≤ b
⊢ x ∈ lowerBounds B.right
Module: Mathlib.Order.Extension.Linear

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
⊢ ∀ c ⊆ S, IsChain (fun x1 x2 ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub

Tactic:
rintro c hc₁ hc₂ s hs

Goal state after:
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
s : α → α → Prop
hs : s ∈ c
⊢ ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
Module: Mathlib.Order.Extension.Linear

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS : ∀ c ⊆ S, IsChain (fun x1 x2 ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
s : α → α → Prop
hrs : r ≤ s
hs : Maximal (fun x ↦ x ∈ S) s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : α → α → Prop := fun x' y' ↦ s x' y' ∨ s x' x ∧ s y y'
⊢ False

Tactic:
rw [hs.eq_of_le (y := s') ?_ fun _ _ ↦ Or.inl] at h

Goal state after:
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS : ∀ c ⊆ S, IsChain (fun x1 x2 ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
s : α → α → Prop
hrs : r ≤ s
hs : Maximal (fun x ↦ x ∈ S) s
this : IsPartialOrder α s
x y : α
s' : α → α → Prop := fun x' y' ↦ s x' y' ∨ s x' x ∧ s y y'
h : ¬s' x y ∧ ¬s' y x
⊢ False

α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS : ∀ c ⊆ S, IsChain (fun x1 x2 ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
s : α → α → Prop
hrs : r ≤ s
hs : Maximal (fun x ↦ x ∈ S) s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : α → α → Prop := fun x' y' ↦ s x' y' ∨ s x' x ∧ s y y'
⊢ s' ∈ S
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
t : Set β
⊢ countableSupClosure s ×ˢ countableSupClosure t ⊆ countableSupClosure (s ×ˢ t)

Tactic:
rintro ⟨a, b⟩ ⟨ha, hb⟩
      simp only [mem_countableSupClosure_iff] at ha hb ⊢
      obtain ⟨u, hu, hu_ne, hu_c, hu_lub⟩ := ha
      obtain ⟨v, hv, hv_ne, hv_c, hv_lub⟩ := hb
      refine ⟨u ×ˢ v, by grind, by simp [hu_ne, hv_ne], hu_c.prod hv_c, ?_⟩
      exact IsLUB.prod hu_ne hv_ne hu_lub hv_lub

Goal state after:
Module: Mathlib.Order.Extension.Linear

Goal state before:
pp: case refine_2.inr.inr
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS : ∀ c ⊆ S, IsChain (fun x1 x2 ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
s : α → α → Prop
hrs : r ≤ s
hs : Maximal (fun x ↦ x ∈ S) s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : α → α → Prop := fun x' y' ↦ s x' y' ∨ s x' x ∧ s y y'
a b : α
ax : s a x
yb : s y b
bx : s b x
ya : s y a
⊢ a = b

Tactic:
· exact (h.2 (_root_.trans yb bx)).elim

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

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

Tactic:
| cons b fs ih =>

Goal state after:
Module: Mathlib.Order.Height

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
n : ℕ
h' : ¬n = 0
h : ∀ t ⊆ s, IsChain r t → t.encard < ↑n
⊢ s.chainHeight r < ↑n

Tactic:
refine iSup_lt_iff.mpr ⟨n - 1, ?_, fun m ↦ ENat.le_sub_one_of_lt <| h m.1 m.2.1 m.2.2⟩

Goal state after:
α : Type u_1
r : α → α → Prop
s : Set α
n : ℕ
h' : ¬n = 0
h : ∀ t ⊆ s, IsChain r t → t.encard < ↑n
⊢ ↑n - 1 < ↑n
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 : α}, r x y → r y z → r x z

Tactic:
intro x y z hxy hyz
  exact closed_interval h₂ h₄ (x ⊓ y ⊓ z) _ _ (x ⊔ y ⊔ z) (by simp [inf_assoc, inf_le_left])
    (by simp [sup_assoc, le_sup_left]) inf_le_right le_sup_right
    (h₃ (by simpa [inf_assoc] using inf_le_of_right_le inf_le_sup)
    (by simp [sup_assoc, le_sup_right]) (h₃
    (by simpa [inf_assoc] using inf_le_right (b := y ⊓ z)) inf_le_sup (by
      suffices r (x ⊓ y ⊓ (y ⊓ z)) ((x ⊔ y) ⊓ (y ⊓ z)) by
        rw [inf_comm x, inf_assoc]
        simpa [inf_comm x, ← inf_inf_distrib_left] using this
      exact (h₄ inf_le_sup (h₂.mp hxy)).1) (h₂.mp hyz)) (by
        simpa [sup_comm y x, sup_sup_distrib_left y x z, sup_assoc] using
          ((h₄ inf_le_sup (h₂.mp hxy)).2 : r (x ⊓ y ⊔ (y ⊔ z)) (x ⊔ y ⊔ (y ⊔ z)))))

Goal state after:
Module: Mathlib.Order.PrimeSeparator

Goal state before:
pp: α : Type u_1
inst✝ : DistribLattice α
F : PFilter α
I : Ideal α
hFI : Disjoint ↑F ↑I
S : Set (Set α) := {J | IsIdeal J ∧ ↑I ⊆ J ∧ Disjoint (↑F) J}
IinS : ↑I ∈ S
⊢ ∀ c ⊆ S, IsChain (fun x1 x2 ↦ x1 ⊆ x2) c → c.Nonempty → ∃ ub ∈ S, ∀ s ∈ c, s ⊆ ub

Tactic:
intro c

Goal state after:
α : Type u_1
inst✝ : DistribLattice α
F : PFilter α
I : Ideal α
hFI : Disjoint ↑F ↑I
S : Set (Set α) := {J | IsIdeal J ∧ ↑I ⊆ J ∧ Disjoint (↑F) J}
IinS : ↑I ∈ S
c : Set (Set α)
⊢ c ⊆ S → IsChain (fun x1 x2 ↦ x1 ⊆ x2) c → c.Nonempty → ∃ ub ∈ S, ∀ s ∈ c, s ⊆ ub