mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.NumberField.DirichletDensity

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
S : Set (HeightOneSpectrum (𝓞 K))
h : ∀ (δ : ℝ), ¬HasDirichletDensity S δ
⊢ dirichletDensity S = 0

Tactic:
rw [dirichletDensity, dif_neg (not_exists.mpr h)]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Ideal.Asymptotics

Goal state before:
pp: case mpr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
C : ClassGroup (𝓞 K)
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
x : 𝓞 K
hx₂ : x ∈ ↑J
hx₃ : mixedEmbedding.norm ((mixedEmbedding K) ↑x) ≤ s
hx₁ : (mixedEmbedding K) ↑x ∈ fundamentalCone K
⊢ ∃ x_1,
    (x_1 ∈ {x | (toMixed K) x ∈ fundamentalCone K ∧ mixedEmbedding.norm ((toMixed K) x) ≤ s} ∧
        ∃ y ∈ ↑↑↑J, (mixedEmbedding K) y = ↑↑(toMixed K) x_1) ∧
      (↑(toMixed K)).toEquiv x_1 = (mixedEmbedding K) ↑x

Tactic:
exact ⟨(toMixed K).symm (mixedEmbedding K x), ⟨⟨hx₁, hx₃⟩, ⟨(x : K), by simp [hx₂], rfl⟩⟩, rfl⟩

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
n : ℤ
⊢ ↑(padicNorm p ↑n) ≤ 1

Tactic:
exact_mod_cast padicNorm.of_int n

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean

Goal state before:
pp: G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : IsUniformGroup G
inst✝ : NonarchimedeanGroup G
f : ℕ → G
hf : Tendsto (fun n ↦ f (n + 1) / f n) atTop (𝓝 1)
⊢ CauchySeq f

Tactic:
suffices Tendsto (fun p : ℕ × ℕ ↦ f p.2 / f p.1) atTop (𝓝 1) by simpa [CauchySeq,
      cauchy_map_iff, prod_atTop_atTop_eq, uniformity_eq_comap_nhds_one G, atTop_neBot]

Goal state after:
G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : IsUniformGroup G
inst✝ : NonarchimedeanGroup G
f : ℕ → G
hf : Tendsto (fun n ↦ f (n + 1) / f n) atTop (𝓝 1)
⊢ Tendsto (fun p ↦ f p.2 / f p.1) atTop (𝓝 1)
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: case calc_5
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
inst✝² : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
Apos : 0 ≤ A
this : 0 ≤ c K
kr : α × (K →+* ℂ)
lu : β × (K →+* ℂ)
⊢ c K * A * house ((algebraMap (𝓞 K) K) ((newBasis K) lu.2)) ≤ c K * A * supOfBasis K

Tactic:
gcongr
      simp only [supOfBasis, le_sup'_iff, mem_univ]; use lu.2

Goal state after:
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 : (if x' - y' = 0 then 0 else exp (-padicValRat p (x' - y'))) < exp (-↑n)
⊢ (if x' - y' = 0 then 0 else (↑p ^ padicValRat p (x' - y'))⁻¹) ≤ (↑p ^ n)⁻¹

Tactic:
split_ifs with H

Goal state after:
case pos
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 : (if x' - y' = 0 then 0 else exp (-padicValRat p (x' - y'))) < exp (-↑n)
H : x' - y' = 0
⊢ 0 ≤ (↑p ^ n)⁻¹

case neg
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 : (if x' - y' = 0 then 0 else exp (-padicValRat p (x' - y'))) < exp (-↑n)
H : ¬x' - y' = 0
⊢ (↑p ^ padicValRat p (x' - 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)
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 : (if x' - y' = 0 then 0 else (↑p ^ padicValRat p (x' - y'))⁻¹) ≤ (↑p ^ (embedding ↑γ * exp (-1)).log.natAbs)⁻¹
⊢ (if x' - y' = 0 then 0 else exp (-padicValRat p (x' - y'))) < embedding ↑γ

Tactic:
split_ifs with H

Goal state after:
case pos
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)
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 : (if x' - y' = 0 then 0 else (↑p ^ padicValRat p (x' - y'))⁻¹) ≤ (↑p ^ (embedding ↑γ * exp (-1)).log.natAbs)⁻¹
H : x' - y' = 0
⊢ 0 < embedding ↑γ

case neg
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)
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 : (if x' - y' = 0 then 0 else (↑p ^ padicValRat p (x' - y'))⁻¹) ≤ (↑p ^ (embedding ↑γ * exp (-1)).log.natAbs)⁻¹
H : ¬x' - y' = 0
⊢ exp (-padicValRat p (x' - y')) < embedding ↑γ
Module: Mathlib.Topology.Separation.DisjointCover

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
S : Set (X × X)
hS : S ∈ 𝓝ˢ (diagonal X)
x : X
⊢ ∃ U, IsOpen[inst✝] U ∧ x ∈ U ∧ U ×ˢ U ⊆ S

Tactic:
have : S ∈ 𝓝 (x, x) := mem_nhdsSet_iff_forall.mp hS _ rfl
  obtain ⟨u, v, huo, hux, hvo, hvx, H⟩ := by rwa [mem_nhds_prod_iff'] at this
  exact ⟨_, huo.inter hvo, ⟨hux, hvx⟩, fun p hp ↦ H ⟨hp.1.1, hp.2.2⟩⟩

Goal state after:
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
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) = ⊤
⊢ p • ⊤ = Submodule.map M.mkQ (p • ⊤)

Tactic:
rw [Submodule.map_smul'', Submodule.map_top, M.range_mkQ]

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

Goal state before:
pp: case refine_2
K : Type u_2
L : Type u_3
B : Type u_4
inst✝¹⁵ : Field K
inst✝¹⁴ : Field L
inst✝¹³ : Algebra K L
inst✝¹² : CommRing B
P : Ideal B
D : Type u_5
inst✝¹¹ : Field D
inst✝¹⁰ : Algebra D L
inst✝⁹ : MulSemiringAction Gal(L/K) B
G : Type u_7
inst✝⁸ : Group G
inst✝⁷ : Finite G
inst✝⁶ : MulSemiringAction G L
inst✝⁵ : IsGaloisGroup G K L
inst✝⁴ : MulSemiringAction G B
inst✝³ : Algebra B L
inst✝² : IsFractionRing B L
inst✝¹ : SMulDistribClass Gal(L/K) B L
inst✝ : SMulDistribClass G B L
h : IsGaloisGroup (↥(stabilizer G P)) D L
x✝ : ↥(stabilizer Gal(L/K) P)
x : L
⊢ (P.stabilizerEquiv (IsGaloisGroup.mulEquivAlgEquiv G K L) ⋯).symm x✝ • x = x✝ • x

Tactic:
obtain ⟨y, z, _, rfl⟩ := IsFractionRing.div_surjective B x
    simp_rw [smul_div₀', subgroup_smul_def, ← algebraMap.smul', ← subgroup_smul_def,
      stabilizerEquiv_symm_apply_smul]

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
⊢ ∃! a₁, 1 < a₁.x ∧ 0 < a₁.y ∧ ∀ (a : Solution₁ d), ∃ n, a = a₁ ^ n ∨ a = -a₁ ^ n

Tactic:
by
  obtain ⟨a₁, ha₁⟩ := IsFundamental.exists_of_not_isSquare h₀ hd
  refine ⟨a₁, ⟨ha₁.1, ha₁.2.1, ha₁.eq_zpow_or_neg_zpow⟩, fun a (H : 1 < _ ∧ _) => ?_⟩
  obtain ⟨Hx, Hy, H⟩ := H
  obtain ⟨n₁, hn₁⟩ := H a₁
  obtain ⟨n₂, hn₂⟩ := ha₁.eq_zpow_or_neg_zpow a
  rcases hn₂ with (rfl | rfl)
  · rw [← zpow_mul, eq_comm, @eq_comm _ a₁, ← mul_inv_eq_one, ← @mul_inv_eq_one _ _ _ a₁, ←
      zpow_neg_one, neg_mul, ← zpow_add, ← sub_eq_add_neg] at hn₁
    rcases hn₁ with hn₁ | hn₁
    · 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)
    · rw [← zpow_zero a₁, eq_comm] at hn₁
      exact False.elim (ha₁.zpow_ne_neg_zpow hn₁)
  · rw [x_neg, lt_neg] at Hx
    have := (x_zpow_pos (zero_lt_one.trans ha₁.1) n₂).trans Hx
    norm_num at this

Goal state after:
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
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
⊢ Submodule.span K (⇑(algebraMap S L) '' b) = ⊤

Tactic:
have span_d : (Submodule.span S ({algebraMap R S A.det} : Set S)).restrictScalars R ≤ M := by
    intro x hx
    rw [Submodule.restrictScalars_mem] at hx
    obtain ⟨x', rfl⟩ := Submodule.mem_span_singleton.mp hx
    rw [smul_eq_mul, mul_comm, ← Algebra.smul_def] at hx ⊢
    rw [← Submodule.Quotient.mk_eq_zero, Submodule.Quotient.mk_smul]
    obtain ⟨a', _, quot_x_eq⟩ := exists_sum (Submodule.Quotient.mk x')
    rw [← quot_x_eq, Finset.smul_sum]
    conv =>
      lhs; congr; next => skip
      intro x; rw [smul_comm A.det, d_smul, smul_zero]
    exact Finset.sum_const_zero

Goal state after:
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
⊢ Submodule.span K (⇑(algebraMap S L) '' b) = ⊤
Module: Mathlib.NumberTheory.SumFourSquares

Goal state before:
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 hb).trans_lt (Nat.mul_div_lt_iff_not_dvd.2 hodd.not_two_dvd_nat)

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

Goal state before:
pp: m a b c d : ℤ
h : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = 2 * m
this :
  ∀ (f : Fin 4 → ZMod 2),
    f 0 ^ 2 + f 1 ^ 2 + f 2 ^ 2 + f 3 ^ 2 = 0 →
      ∃ i, f i ^ 2 + f ((swap i 0) 1) ^ 2 = 0 ∧ f ((swap i 0) 2) ^ 2 + f ((swap i 0) 3) ^ 2 = 0
f : Fin 4 → ℤ := ![a, b, c, d]
i : Fin 4
σ : Perm (Fin 4) := swap i 0
hσ : ↑(f i) ^ 2 + ↑(f (σ 1)) ^ 2 = 0 ∧ ↑(f (σ 2)) ^ 2 + ↑(f (σ 3)) ^ 2 = 0
x : ℤ
hx : f (σ 0) ^ 2 + f (σ 1) ^ 2 = 2 * x
y : ℤ
hy : f (σ 2) ^ 2 + f (σ 3) ^ 2 = 2 * y
⊢ ((f (σ 0) - f (σ 1)) / 2) ^ 2 + ((f (σ 0) + f (σ 1)) / 2) ^ 2 + ((f (σ 2) - f (σ 3)) / 2) ^ 2 +
      ((f (σ 2) + f (σ 3)) / 2) ^ 2 =
    m

Tactic:
← Int.sq_add_sq_of_two_mul_sq_add_sq hx.symm,

Goal state after:
m a b c d : ℤ
h : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = 2 * m
this :
  ∀ (f : Fin 4 → ZMod 2),
    f 0 ^ 2 + f 1 ^ 2 + f 2 ^ 2 + f 3 ^ 2 = 0 →
      ∃ i, f i ^ 2 + f ((swap i 0) 1) ^ 2 = 0 ∧ f ((swap i 0) 2) ^ 2 + f ((swap i 0) 3) ^ 2 = 0
f : Fin 4 → ℤ := ![a, b, c, d]
i : Fin 4
σ : Perm (Fin 4) := swap i 0
hσ : ↑(f i) ^ 2 + ↑(f (σ 1)) ^ 2 = 0 ∧ ↑(f (σ 2)) ^ 2 + ↑(f (σ 3)) ^ 2 = 0
x : ℤ
hx : f (σ 0) ^ 2 + f (σ 1) ^ 2 = 2 * x
y : ℤ
hy : f (σ 2) ^ 2 + f (σ 3) ^ 2 = 2 * y
⊢ x + ((f (σ 2) - f (σ 3)) / 2) ^ 2 + ((f (σ 2) + f (σ 3)) / 2) ^ 2 = m
Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt

Goal state before:
pp: x : ℤ[i]
⊢ 0 < norm x ↔ x ≠ 0

Tactic:
by
  rw [lt_iff_le_and_ne, Ne, eq_comm, norm_eq_zero]; simp [norm_nonneg]

Goal state after:
Module: Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp2 : p = 2
this : ↑p = { re := 1, im := 1 } * { re := 1, im := -1 } → IsUnit { re := 1, im := 1 } ∨ IsUnit { re := 1, im := -1 }
⊢ p % 4 = 3

Tactic:
simp [hp2, Zsqrtd.ext_iff, ← norm_eq_one_iff, norm_def] at this

Goal state after:
Module: Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
k : ZMod p
hk : -1 = k * k
⊢ ∃ k', ∃ (_ : k' < p), ↑k' = k

Tactic:
by
        exact ⟨k.val, k.val_lt, ZMod.natCast_zmod_val k⟩

Goal state after:
Module: Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
k : ℕ
k_lt_p : k < p
hk : -1 = ↑k * ↑k
⊢ -1 + 1 = 0

Tactic:
neg_add_cancel

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
k : ℕ
k_lt_p : k < p
hk : -1 = ↑k * ↑k
⊢ 0 = 0
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: p n : ℕ
hp : p ∈ n.primeFactors
hs : IsSquare (-1)
y : ZMod p
h : y ^ 2 = -1 ^ 2
this : Fact (Prime p)
⊢ p % 4 ≠ 3

Tactic:
exact ZMod.mod_four_ne_three_of_sq_eq_neg_sq' one_ne_zero h

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

Goal state before:
pp: x : ℝ
lx : Liouville x
⊢ Transcendental ℤ x

Tactic:
rintro ⟨f : ℤ[X], f0, ef0⟩
  -- Change `aeval x f = 0` to `eval (map _ f) = 0`, who knew.
  replace ef0 : (f.map (algebraMap ℤ ℝ)).eval x = 0 := by
    rwa [← eval_map_algebraMap] at ef0
  -- There is a "large" real number `A` such that `(b + 1) ^ (deg f) * |f (x - a / (b + 1))| * A`
  -- is at least one.  This is obtained from lemma `exists_pos_real_of_irrational_root`.
  obtain ⟨A, hA, h⟩ : ∃ A : ℝ, 0 < A ∧ ∀ (a : ℤ) (b : ℕ),
      (1 : ℝ) ≤ ((b : ℝ) + 1) ^ f.natDegree * (|x - a / (b + 1)| * A) :=
    exists_pos_real_of_irrational_root lx.irrational f0 ef0
  -- Since the real numbers are Archimedean, a power of `2` exceeds `A`: `hn : A < 2 ^ r`.
  rcases pow_unbounded_of_one_lt A (lt_add_one 1) with ⟨r, hn⟩
  -- Use the Liouville property, with exponent `r + deg f`.
  obtain ⟨a, b, b1, -, a1⟩ : ∃ a b : ℤ, 1 < b ∧ x ≠ a / b ∧
      |x - a / b| < 1 / (b : ℝ) ^ (r + f.natDegree) :=
    lx (r + f.natDegree)
  have b0 : (0 : ℝ) < b := zero_lt_one.trans (by rw [← Int.cast_one]; exact Int.cast_lt.mpr b1)
  -- Prove that `b ^ f.nat_degree * abs (x - a / b)` is strictly smaller than itself
  -- recall, this is a proof by contradiction!
  refine lt_irrefl ((b : ℝ) ^ f.natDegree * |x - ↑a / ↑b|) ?_
  -- clear denominators at `a1`
  rw [lt_div_iff₀' (pow_pos b0 _), pow_add, mul_assoc] at a1
  -- split the inequality via `1 / A`.
  refine (?_ : (b : ℝ) ^ f.natDegree * |x - a / b| < 1 / A).trans_le ?_
  -- This branch of the proof uses the Liouville condition and the Archimedean property
  · refine (lt_div_iff₀' hA).mpr ?_
    refine lt_of_le_of_lt ?_ a1
    gcongr
    refine hn.le.trans ?_
    rw [one_add_one_eq_two]
    gcongr
    norm_cast
  -- this branch of the proof exploits the "integrality" of evaluations of polynomials
  -- at ratios of integers.
  · lift b to ℕ using zero_le_one.trans b1.le
    specialize h a b.pred
    rwa [← Nat.cast_succ, Nat.succ_pred_eq_of_pos (zero_lt_one.trans _), ← mul_assoc, ←
      div_le_iff₀ hA] at h
    exact Int.ofNat_lt.mp b1

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

Goal state before:
pp: case refine_1
⊢ IsGδ {x | x ∈ ⋂ n, ⋃ a, ⋃ b, ⋃ (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n)}

Tactic:
exact .iInter fun n => IsOpen.isGδ <|
          isOpen_iUnion fun a => isOpen_iUnion fun b => isOpen_iUnion fun _hb => isOpen_ball

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

Goal state after:
case refine_1.left
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
a : (ZMod p)ˣ
ha : a ∈ univ
⊢ (↑a).val ≠ 0
Module: Mathlib.NumberTheory.Wilson

Goal state before:
pp: case refine_3
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
b : ℕ
hb : 0 < b ∧ b < (p - 1).succ
⊢ ∃ a, ∃ (_ : a ∈ univ), (↑a).val = b

Tactic:
← succ_sub hp,

Goal state after:
case refine_3
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
b : ℕ
hb : 0 < b ∧ b < p.succ - succ 0
⊢ ∃ a, ∃ (_ : a ∈ univ), (↑a).val = b
Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure

Goal state before:
pp: p : ℝ
hp : p > 2
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
x : ℝ
hxp : LiouvilleWith p x
hx01 : x ∈ Ico 0 1
b : ℕ
a : ℤ
hlt : |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n.succ)
hb : 1 ≤ ↑b
hb0 : 0 < ↑b
⊢ 2 ≤ 2 + 1 / ↑(n + 1)

Tactic:
simpa using n.cast_add_one_pos.le

Goal state after:
Module: Mathlib.NumberTheory.Wilson

Goal state before:
pp: case inr
n : ℕ
h : ↑(n - 1)! = -1
h0 : n ≠ 0
h1 : 1 < n
h2 : ¬Prime n
m : ℕ
hm1 : m ∣ n
hm2 : 1 < m
hm3 : m < n
hm : m ∣ (n - 1)!
⊢ -1 + 1 = 0

Tactic:
neg_add_cancel

Goal state after:
case inr
n : ℕ
h : ↑(n - 1)! = -1
h0 : n ≠ 0
h1 : 1 < n
h2 : ¬Prime n
m : ℕ
hm1 : m ∣ n
hm2 : 1 < m
hm3 : m < n
hm : m ∣ (n - 1)!
⊢ 0 = 0
Module: Mathlib.Order.Concept

Goal state before:
pp: α : Type u_2
r' : α → α → Prop
c' : Concept α α r'
inst✝ : IsTrans α r'
x y : α
hy : r' y x
hx : x ∈ c'.extent
⊢ y ∈ c'.extent

Tactic:
rw [← lowerPolar_intent]
  exact fun z hz ↦ _root_.trans hy (rel_extent_intent hx hz)

Goal state after:
Module: Mathlib.Order.Concept

Goal state before:
pp: α : Type u_6
inst✝ : PartialOrder α
c : Concept α α fun x1 x2 ↦ x1 < x2
a : α
⊢ ∀ ⦃b : α⦄, b ≤ a → a ∈ c.extent → b ∈ c.extent

Tactic:
b

Goal state after:
α : Type u_6
inst✝ : PartialOrder α
c : Concept α α fun x1 x2 ↦ x1 < x2
a b : α
⊢ b ≤ a → a ∈ c.extent → b ∈ c.extent
Module: Mathlib.Order.Concept

Goal state before:
pp: α : Type u_6
inst✝ : PartialOrder α
c : Concept α α fun x1 x2 ↦ x1 < x2
a : α
⊢ ∀ ⦃b : α⦄, a ≤ b → a ∈ c.intent → b ∈ c.intent

Tactic:
b

Goal state after:
α : Type u_6
inst✝ : PartialOrder α
c : Concept α α fun x1 x2 ↦ x1 < x2
a b : α
⊢ a ≤ b → a ∈ c.intent → b ∈ c.intent
Module: Mathlib.Order.Completion

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : PartialOrder β
x : DedekindCut α
⊢ principalEmbedding.toFun ((factorEmbedding (RelIso.toRelEmbedding (OrderIso.refl α))) x) = x

Tactic:
simp [factorEmbedding]

Goal state after:
Module: Mathlib.Order.Completion

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : DenselyOrdered α
a b : DedekindCut α
h : a < b
⊢ ∃ a_1, a < a_1 ∧ a_1 < b

Tactic:
by
    obtain ⟨c, hac, hcb⟩ := lt_iff_exists.mp h
    obtain ⟨d, had, hdc⟩ := lt_iff_exists'.mp hac
    simp only [principal_lt_principal] at hdc
    obtain ⟨u, _, _⟩ := DenselyOrdered.dense d c hdc
    exact ⟨principal u, had.trans_lt (by simpa), hcb.trans_lt' (by simpa)⟩

Goal state after:
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: case refine_3
ι : Sort u_1
α : Type u_2
β : Type u_3
S : Set (Set α)
s✝ t : Set α
a b : α
inst✝ : Preorder α
s A : Set α
hA_ne : A.Nonempty
hAc : A.Countable
x : α
hx : IsLUB A x
B : ⦃a : α⦄ → a ∈ A → Set α
hB : ∀ ⦃a : α⦄ (a_1 : a ∈ A), B a_1 ⊆ s
hB_ne : ∀ ⦃a : α⦄ (a_1 : a ∈ A), (B a_1).Nonempty
hBc : ∀ ⦃a : α⦄ (a_1 : a ∈ A), (B a_1).Countable
hB_lub : ∀ ⦃a : α⦄ (a_1 : a ∈ A), IsLUB (B a_1) a
⊢ IsLUB (⋃ a, B ⋯) x

Tactic:
have : Nonempty A := Set.nonempty_coe_sort.mpr hA_ne
      rw [← isLUB_iUnion_iff_of_isLUB (u := fun a : A ↦ a.1) (fun a ↦ hB_lub a.2)]
      simpa

Goal state after:
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: α : Type u_2
inst✝ : Preorder α
s : Set α
a : α
ha : a ∈ upperBounds s
⊢ a ∈ upperBounds (countableSupClosure s)

Tactic:
b

Goal state after:
α : Type u_2
inst✝ : Preorder α
s : Set α
a : α
ha : a ∈ upperBounds s
b : α
⊢ b ∈ countableSupClosure s → b ≤ a
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
t : Set β
a : α
b : β
u : Set α
hu : u ⊆ s
hu_ne : u.Nonempty
hu_c : u.Countable
hu_lub : IsLUB u a
v : Set β
hv : v ⊆ t
hv_ne : v.Nonempty
hv_c : v.Countable
hv_lub : IsLUB v b
⊢ IsLUB (u ×ˢ v) (a, b)

Tactic:
exact IsLUB.prod hu_ne hv_ne hu_lub hv_lub

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

Goal state before:
pp: case mpr
α : Type u
β : Type v
r : SetRel α β
l₁ : Filter α
l₂ : Filter β
⊢ (∀ s ∈ l₂, r.preimage s ∈ l₁) →
    l₁ ≤
      { sets := SetRel.image {(s, t) | r.preimage s ⊆ t} l₂.sets, univ_sets := ⋯, sets_of_superset := ⋯,
        inter_sets := ⋯ }

Tactic:
· simpa [le_def, SetRel.mem_image] using fun h s t ht => mem_of_superset (h t ht)

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

Goal state before:
pp: α : Type u
c : Cardinal.{u}
hreg✝ hreg : c.IsRegular
s : Set (Set α)
hS : #↑s < c
hSc : ∀ s_1 ∈ s, s_1 ∈ {s | #↑s < c}
⊢ #↑s < c.ord.cof

Tactic:
rwa [hreg.cof_ord]

Goal state after: