mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.ModelTheory.FinitelyGenerated

Goal state before:
pp: L : Language
M : Type u_1
inst✝¹ : L.Structure M
N : Type u_2
inst✝ : L.Structure N
h : FG L M
f : M →[L] N
hs : f.range = ⊤
⊢ ⊤.FG

Tactic:
← hs

Goal state after:
L : Language
M : Type u_1
inst✝¹ : L.Structure M
N : Type u_2
inst✝ : L.Structure N
h : FG L M
f : M →[L] N
hs : f.range = ⊤
⊢ f.range.FG
Module: Mathlib.ModelTheory.FinitelyGenerated

Goal state before:
pp: L : Language
M : Type u_1
inst✝¹ : L.Structure M
N : Type u_2
inst✝ : L.Structure N
h : CG L M
f : M →[L] N
hs : f.range = ⊤
⊢ ⊤.CG

Tactic:
← hs

Goal state after:
L : Language
M : Type u_1
inst✝¹ : L.Structure M
N : Type u_2
inst✝ : L.Structure N
h : CG L M
f : M →[L] N
hs : f.range = ⊤
⊢ f.range.CG
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: M : Type u_1
ι : Type u_3
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Finite ι
F : Type u_5
G : Type u_6
inst✝³ : FunLike F (ι → ℕ) M
inst✝² : AddMonoidHomClass F (ι → ℕ) M
inst✝¹ : FunLike G (ι → ℕ) M
inst✝ : AddMonoidHomClass G (ι → ℕ) M
a b : M
f : F
g : G
x : ι → ℕ
hx : x ∈ {x | a + f x = b + g x}
y z : ι → ℕ
hy : x + y ∈ {x | a + f x = b + g x}
⊢ x + z ∈ {x | a + f x = b + g x} → x + y + z ∈ {x | a + f x = b + g x}

Tactic:
hz

Goal state after:
M : Type u_1
ι : Type u_3
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Finite ι
F : Type u_5
G : Type u_6
inst✝³ : FunLike F (ι → ℕ) M
inst✝² : AddMonoidHomClass F (ι → ℕ) M
inst✝¹ : FunLike G (ι → ℕ) M
inst✝ : AddMonoidHomClass G (ι → ℕ) M
a b : M
f : F
g : G
x : ι → ℕ
hx : x ∈ {x | a + f x = b + g x}
y z : ι → ℕ
hy : x + y ∈ {x | a + f x = b + g x}
hz : x + z ∈ {x | a + f x = b + g x}
⊢ x + y + z ∈ {x | a + f x = b + g x}
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: case refine_2
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
h : ∀ (S : L.Substructure M), S.FG → ∀ (f : ↥S ↪[L] N) (m : M), ∃ g, f = g.comp (Substructure.inclusion ⋯)
x✝ : L.FGEquiv M N
m : M
f : M ≃ₚ[L] N
f_FG : f.dom.FG
⊢ ∃ g, m ∈ (↑g).dom ∧ ⟨f, f_FG⟩ ≤ g

Tactic:
· obtain ⟨f', eq_f'⟩ := h f.dom f_FG f.toEmbedding m
    refine ⟨⟨⟨closure L {m} ⊔ f.dom, f'.toHom.range, f'.equivRange⟩,
      (fg_closure_singleton _).sup f_FG⟩,
      subset_closure.trans (le_sup_left : (closure L) {m} ≤ _) (mem_singleton m),
      ⟨le_sup_right, Embedding.ext (fun _ => ?_)⟩⟩
    rw [PartialEquiv.toEmbedding] at eq_f'
    simp only [Embedding.comp_apply, Substructure.coe_inclusion, Equiv.coe_toEmbedding, coe_subtype,
      Embedding.equivRange_apply, eq_f']

Goal state after:
Module: Mathlib.ModelTheory.DirectLimit

Goal state before:
pp: case refine_2.refine_1
L : Language
ι : Type u_1
inst✝⁵ : Countable ι
inst✝⁴ : Preorder ι
inst✝³ : IsDirectedOrder ι
inst✝² : Nonempty ι
G : ι → Type w
inst✝¹ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
h : ∀ (i : ι), CG L (G i)
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
S : L.Substructure (DirectLimit G f)
hS : ∀ (i : ι), Substructure.map (of L ι G f i).toHom ((Substructure.closure L).toFun (Classical.choose ⋯)) ≤ S
x : DirectLimit G f
a✝ : x ∈ ⊤
out : Quotient (setoid G f) → Σˣ f := Quotient.out
⊢ (out x).snd ∈ ↑((Substructure.closure L).toFun (Classical.choose ⋯))

Tactic:
rw [(Classical.choose_spec (h (out x).1).out).2]
      trivial

Goal state after:
Module: Mathlib.ModelTheory.Graph

Goal state before:
pp: V : Type u
n : ℕ
G : SimpleGraph V
this : Language.graph.Structure V := G.structure
⊢ V ⊨ Theory.simpleGraph

Tactic:
Theory.simpleGraph_model_iff

Goal state after:
V : Type u
n : ℕ
G : SimpleGraph V
this : Language.graph.Structure V := G.structure
⊢ (Std.Irrefl fun x y ↦ RelMap adj ![x, y]) ∧ Std.Symm fun x y ↦ RelMap adj ![x, y]
Module: Mathlib.Order.CountableDenseLinearOrder

Goal state before:
pp: case inl.inr
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
a : α
f : PartialIso α β
b : β
a_b : ∀ p ∈ ↑f, cmp p.1 a = cmp p.2 b
q : α × β
qf : q ∈ ↑f
⊢ cmp q.1 (a, b).1 = cmp q.2 (a, b).2

Tactic:
exact a_b _ qf

Goal state after:
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: case mp
L : Language
M : Type w
inst✝ : L.Structure M
M_CG : Structure.CG L M
M_homog : L.IsUltrahomogeneous M
⊢ L.IsExtensionPair M M

Tactic:
⟨f, f_FG⟩

Goal state after:
case mp
L : Language
M : Type w
inst✝ : L.Structure M
M_CG : Structure.CG L M
M_homog : L.IsUltrahomogeneous M
f : M ≃ₚ[L] M
f_FG : f.dom.FG
⊢ ∀ (m : M), ∃ g, m ∈ (↑g).dom ∧ ⟨f, f_FG⟩ ≤ g
Module: Mathlib.Topology.Baire.LocallyCompactRegular

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
s : Set X
inst✝¹ : R1Space X
inst✝ : LocallyCompactSpace X
hG : IsGδ s
this : LocallyCompactSpace ↑(closure s)
⊢ BaireSpace ↑s

Tactic:
have : BaireSpace (closure s) := .of_t2Space_locallyCompactSpace

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
s : Set X
inst✝¹ : R1Space X
inst✝ : LocallyCompactSpace X
hG : IsGδ s
this✝ : LocallyCompactSpace ↑(closure s)
this : BaireSpace ↑(closure s)
⊢ BaireSpace ↑s
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: case h
R : Type u_1
inst✝ : CommSemiring R
p : ℕ
u v : R
hp : Nat.Prime p
hvu : v ∣ u
hpuv : ↑p * u * v ∣ u ^ p
x : R
m✝ m : ℕ
y : R
hy : (1 + u * x) ^ p = 1 + ↑p * u * (x + v * y)
z : R
hz : (1 + ↑p * u * (x + v * y)) ^ p ^ m = 1 + ↑p ^ m * (↑p * u) * (x + v * y + ↑p * v * z)
⊢ (1 + ↑p * u * (x + v * y)) ^ p ^ m = 1 + ↑p ^ (m + 1) * u * (x + v * (y + ↑p * z))

Tactic:
hz

Goal state after:
case h
R : Type u_1
inst✝ : CommSemiring R
p : ℕ
u v : R
hp : Nat.Prime p
hvu : v ∣ u
hpuv : ↑p * u * v ∣ u ^ p
x : R
m✝ m : ℕ
y : R
hy : (1 + u * x) ^ p = 1 + ↑p * u * (x + v * y)
z : R
hz : (1 + ↑p * u * (x + v * y)) ^ p ^ m = 1 + ↑p ^ m * (↑p * u) * (x + v * y + ↑p * v * z)
⊢ 1 + ↑p ^ m * (↑p * u) * (x + v * y + ↑p * v * z) = 1 + ↑p ^ (m + 1) * u * (x + v * (y + ↑p * z))
Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt

Goal state before:
pp: n : ℕ
⊢ Λ (n + 1) ≤ Real.log ↑(n + 1)

Tactic:
rw [← vonMangoldt_sum]
    exact single_le_sum (by exact fun _ _ => vonMangoldt_nonneg)
      (mem_divisors_self _ n.succ_ne_zero)

Goal state after:
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: n : ℕ
⊢ IsCyclic (ZMod (4 * n))ˣ ↔ n = 0 ∨ n = 1

Tactic:
by
  obtain rfl | hn0 := eq_or_ne n 0
  · simp [isCyclic_units_zero]
  obtain rfl | hn1 := eq_or_ne n 1
  · simp [isCyclic_units_four]
  refine iff_of_false ?_ (by simp [hn0, hn1])
  obtain ⟨n, rfl⟩ | h2n := em (2 ∣ n)
  · rw [← mul_assoc]
    have : NeZero n := ⟨by simpa using hn0⟩
    refine mt (fun _ ↦ ?_) not_isCyclic_units_eight
    exact isCyclic_of_surjective _ (ZMod.unitsMap_surjective (m := 4 * 2 * n) (dvd_mul_right 8 _))
  have : Nat.Coprime 4 n := (Nat.prime_two.coprime_iff_not_dvd.mpr h2n).pow_left 2
  rw [((Units.mapEquiv (chineseRemainder this).toMulEquiv).trans .prodUnits).isCyclic,
    Group.isCyclic_prod_iff]
  rintro ⟨-, -, h⟩
  have : NeZero n := ⟨hn0⟩
  have : Odd (φ n) := by simpa [show φ 4 = 2 from rfl] using h
  rw [Nat.odd_totient_iff] at this
  lia

Goal state after:
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: ⊢ bernoulli 1 = X - C 2⁻¹

Tactic:
by
  simp [bernoulli, ← smul_X_eq_monomial, sum_range_succ, ← C_1, -map_one, neg_div, sub_eq_add_neg]

Goal state after:
Module: Mathlib.NumberTheory.PrimeCounting

Goal state before:
pp: n : ℕ
⊢ count Prime n = 0 ↔ n ≤ 2

Tactic:
Nat.count_eq_zero ⟨_, Nat.prime_two⟩,

Goal state after:
n : ℕ
⊢ n ≤ nth Prime 0 ↔ n ≤ 2
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: ⊢ bernoulli' 2 = 1 / 6

Tactic:
rw [bernoulli'_def]
  norm_num [sum_range_succ, sum_range_succ, sum_range_zero]

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: ⊢ bernoulli' 3 = 0

Tactic:
rw [bernoulli'_def]
  norm_num [sum_range_succ, sum_range_succ, sum_range_zero]

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ (∑ p ∈ antidiagonal n, bernoulli' p.1 / ↑p.1! * ((↑p.2 + 1) * ↑p.2!)⁻¹) * ↑n ! = 1

Tactic:
rw [sum_mul]

Goal state after:
case succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ ∑ i ∈ antidiagonal n, bernoulli' i.1 / ↑i.1! * ((↑i.2 + 1) * ↑i.2!)⁻¹ * ↑n ! = 1
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: n p : ℕ
f : ℕ → ℚ := fun i ↦ bernoulli i * ↑(p.succ.succ.choose i) * ↑n ^ (p.succ.succ - i) / ↑p.succ.succ
f' : ℕ → ℚ := fun i ↦ bernoulli' i * ↑(p.succ.succ.choose i) * ↑n ^ (p.succ.succ - i) / ↑p.succ.succ
hle : 1 ≤ n + 1
hne : ↑p + 1 + 1 ≠ 0
h1 : ∀ (r : ℚ), r * (↑p + 1 + 1) * ↑n ^ p.succ / (↑p + 1 + 1) = r * ↑n ^ p.succ
h2 : f 1 + ↑n ^ p.succ = 1 / 2 * ↑n ^ p.succ
this :
  ∑ i ∈ range p, bernoulli (i + 2) * ↑((p + 2).choose (i + 2)) * ↑n ^ (p - i) / ↑(p + 2) =
    ∑ i ∈ range p, bernoulli' (i + 2) * ↑((p + 2).choose (i + 2)) * ↑n ^ (p - i) / ↑(p + 2)
⊢ ∑ i ∈ range p, f i.succ.succ + (f 1 + ↑n ^ p.succ) + f 0 = ∑ i ∈ range p, f i.succ.succ + 1 / 2 * ↑n ^ p.succ + f 0

Tactic:
by rw [h2]

Goal state after:
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleAbs

Goal state before:
pp: case refine_2
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : 0 < ↑|b|
hbε : 0 < |b| • ε
hfloor : ∀ (i : Fin n), 0 ≤ ⌊↑(A i % b) / |b| • ε⌋
i₀ i₁ : Fin n
hi✝¹ : (fun i ↦ ⟨⌊↑(A i % b) / |b| • ε⌋.natAbs, ⋯⟩) i₀ = (fun i ↦ ⟨⌊↑(A i % b) / |b| • ε⌋.natAbs, ⋯⟩) i₁
hi✝ : ⌊↑(A i₀ % b) / |b| • ε⌋ = ⌊↑(A i₁ % b) / |b| • ε⌋
hi : |↑(A i₁ % b) - ↑(A i₀ % b)| < |b| • ε
⊢ ↑|A i₁ % b - A i₀ % b| < |b| • ε

Tactic:
Int.cast_abs,

Goal state after:
case refine_2
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : 0 < ↑|b|
hbε : 0 < |b| • ε
hfloor : ∀ (i : Fin n), 0 ≤ ⌊↑(A i % b) / |b| • ε⌋
i₀ i₁ : Fin n
hi✝¹ : (fun i ↦ ⟨⌊↑(A i % b) / |b| • ε⌋.natAbs, ⋯⟩) i₀ = (fun i ↦ ⟨⌊↑(A i % b) / |b| • ε⌋.natAbs, ⋯⟩) i₁
hi✝ : ⌊↑(A i₀ % b) / |b| • ε⌋ = ⌊↑(A i₁ % b) / |b| • ε⌋
hi : |↑(A i₁ % b) - ↑(A i₀ % b)| < |b| • ε
⊢ |↑(A i₁ % b - A i₀ % b)| < |b| • ε
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case refine_2
n p : ℕ
hp : Prime p
this : 1 < p
⊢ log p n ≤ (Icc 1 n).sup fun a ↦ (id a).factorization p

Tactic:
rcases le_or_gt p n with _ | h

Goal state after:
case refine_2.inl
n p : ℕ
hp : Prime p
this : 1 < p
h✝ : p ≤ n
⊢ log p n ≤ (Icc 1 n).sup fun a ↦ (id a).factorization p

case refine_2.inr
n p : ℕ
hp : Prime p
this : 1 < p
h : n < p
⊢ log p n ≤ (Icc 1 n).sup fun a ↦ (id a).factorization p
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case succ.zero
k p : ℕ
hk : k > 0
inst✝ : Fact (Nat.Prime p)
ih : ∀ (m : ℕ), 0 < m → m < k → pIntegral p (bernoulli (2 * m) + vonStaudtIndicator (2 * m) p / ↑p)
hi : 0 + 1 < 2 * k
⊢ (Rat.padicValuation p) (bernoulli (0 + 1) * ↑((2 * k + 1).choose (0 + 1)) * ↑p ^ (2 * k - (0 + 1)) / (2 * ↑k + 1)) ≤ 1

Tactic:
rw [zero_add, Nat.choose_one_right, bernoulli_one]
    push_cast
    field_simp
    obtain rfl | hp2 := eq_or_ne p 2
    · push_cast
      rw [show 2 * k - 1 = (2 * k - 2) + 1 by lia, pow_succ, mul_div_cancel_right₀ _ two_ne_zero]
      exact_mod_cast Int.padicValuation_le_one ..
    · rw [Valuation.map_neg]
      refine pIntegral_pow_div two_ne_zero <|
         (factorization_eq_zero_of_lt ?_).trans_le (by lia)
      exact (Prime.odd_iff Fact.out).mp <| Prime.odd_of_ne_two Fact.out hp2

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: n : ℕ
⊢ ↑n * log 2 - log (↑n + 1) ≤ ψ ↑n

Tactic:
tsub_le_iff_left,

Goal state after:
n : ℕ
⊢ ↑n * log 2 ≤ log (↑n + 1) + ψ ↑n
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case succ
x : ℝ
N : ℕ
ih :
  ∑ n ∈ Icc 1 (1 + 6 * N), b x n =
    b x 1 + ∑ n ∈ Icc 1 (3 * N), b x (2 * n) + ∑ n ∈ Icc 1 (2 * N), b x (3 * n) + ∑ n ∈ Icc 1 N, c x n
⊢ ∑ n ∈ Icc 1 (1 + 6 * N + 1 + 1 + 1 + 1 + 1 + 1), b x n =
    b x 1 + ∑ n ∈ Icc 1 (3 * (N + 1)), b x (2 * n) + ∑ n ∈ Icc 1 (2 * (N + 1)), b x (3 * n) + ∑ n ∈ Icc 1 (N + 1), c x n

Tactic:
show 3 * (N + 1) = 3 * N + 1 + 1 + 1 by ring,

Goal state after:
case succ
x : ℝ
N : ℕ
ih :
  ∑ n ∈ Icc 1 (1 + 6 * N), b x n =
    b x 1 + ∑ n ∈ Icc 1 (3 * N), b x (2 * n) + ∑ n ∈ Icc 1 (2 * N), b x (3 * n) + ∑ n ∈ Icc 1 N, c x n
⊢ ∑ n ∈ Icc 1 (1 + 6 * N + 1 + 1 + 1 + 1 + 1 + 1), b x n =
    b x 1 + ∑ n ∈ Icc 1 (3 * N + 1 + 1 + 1), b x (2 * n) + ∑ n ∈ Icc 1 (2 * (N + 1)), b x (3 * n) +
      ∑ n ∈ Icc 1 (N + 1), c x n
Module: Mathlib.NumberTheory.ClassNumber.Finite

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁹ : EuclideanDomain R
inst✝⁸ : CommRing S
inst✝⁷ : IsDomain S
inst✝⁶ : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst✝³ : Infinite R
inst✝² : DecidableEq R
inst✝¹ : IsDedekindDomain S
inst✝ : Algebra.IsAlgebraic R S
I : ↥(Ideal S)⁰
M : R := ⋯
hM : (algebraMap R S) M ≠ 0
b : S
b_mem : b ∈ ↑I
b_ne_zero : b ≠ 0
b_min : ∀ c ∈ ↑I, abv ((Algebra.norm R) c) < abv ((Algebra.norm R) b) → c = 0
J : Ideal S
hJ : Ideal.span {(algebraMap R S) M} * ↑I = Ideal.span {b} * J
⊢ Ideal.span {b} * ↑⟨J, ⋯⟩ ∣ Ideal.span {b} * Ideal.span {(algebraMap R S) M}

Tactic:
Subtype.coe_mk,

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁹ : EuclideanDomain R
inst✝⁸ : CommRing S
inst✝⁷ : IsDomain S
inst✝⁶ : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst✝³ : Infinite R
inst✝² : DecidableEq R
inst✝¹ : IsDedekindDomain S
inst✝ : Algebra.IsAlgebraic R S
I : ↥(Ideal S)⁰
M : R := ∏ m ∈ finsetApprox bS adm, m
hM : (algebraMap R S) M ≠ 0
b : S
b_mem : b ∈ ↑I
b_ne_zero : b ≠ 0
b_min : ∀ c ∈ ↑I, abv ((Algebra.norm R) c) < abv ((Algebra.norm R) b) → c = 0
J : Ideal S
hJ : Ideal.span {(algebraMap R S) M} * ↑I = Ideal.span {b} * J
⊢ Ideal.span {b} * J ∣ Ideal.span {b} * Ideal.span {(algebraMap R S) M}
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ (toZMod x).cast = ↑x.zmodRepr

Tactic:
dsimp [toZMod, toZModHom]

Goal state after:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ (↑x.zmodRepr).cast = ↑x.zmodRepr
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: case mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
h : x - 0 ∈ maximalIdeal ℤ_[p]
⊢ toZMod x = 0

Tactic:
dsimp [toZMod, toZModHom]

Goal state after:
case mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
h : x - 0 ∈ maximalIdeal ℤ_[p]
⊢ ↑x.zmodRepr = 0
Module: Mathlib.NumberTheory.NumberField.Discriminant.Defs

Goal state before:
pp: ⊢ discr ℚ = 1

Tactic:
let b : Basis (Fin 1) ℤ (𝓞 ℚ) :=
    Basis.map (Basis.singleton (Fin 1) ℤ) ringOfIntegersEquiv.toAddEquiv.toIntLinearEquiv.symm

Goal state after:
b : Basis (Fin 1) ℤ (𝓞 ℚ) := (Basis.singleton (Fin 1) ℤ).map ringOfIntegersEquiv.toAddEquiv.toIntLinearEquiv.symm
⊢ discr ℚ = 1
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: K : Type u
L : Type v
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
inst✝⁷ : Module.Finite K L
R : Type z
inst✝⁶ : CommRing R
inst✝⁵ : Algebra R K
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R K L
inst✝² : Algebra.IsSeparable K L
inst✝¹ : IsIntegrallyClosed R
inst✝ : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
hinv : IsUnit (traceMatrix K ⇑B.basis).det
H :
  (traceMatrix K ⇑B.basis).det • traceMatrix K ⇑B.basis *ᵥ B.basis.equivFun z =
    (traceMatrix K ⇑B.basis).det • fun i ↦ (trace K L) (z * B.basis i)
i : Fin B.dim
cramer :
  ((traceMatrix K ⇑B.basis).cramer fun i ↦ (trace K L) (z * B.basis i)) =
    1 *ᵥ (traceMatrix K ⇑B.basis).det • B.basis.equivFun z
⊢ ((traceMatrix K ⇑B.basis).det • B.basis.equivFun z) i ∈ ⊥

Tactic:
one_mulVec

Goal state after:
K : Type u
L : Type v
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
inst✝⁷ : Module.Finite K L
R : Type z
inst✝⁶ : CommRing R
inst✝⁵ : Algebra R K
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R K L
inst✝² : Algebra.IsSeparable K L
inst✝¹ : IsIntegrallyClosed R
inst✝ : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
hinv : IsUnit (traceMatrix K ⇑B.basis).det
H :
  (traceMatrix K ⇑B.basis).det • traceMatrix K ⇑B.basis *ᵥ B.basis.equivFun z =
    (traceMatrix K ⇑B.basis).det • fun i ↦ (trace K L) (z * B.basis i)
i : Fin B.dim
cramer :
  ((traceMatrix K ⇑B.basis).cramer fun i ↦ (trace K L) (z * B.basis i)) =
    (traceMatrix K ⇑B.basis).det • B.basis.equivFun z
⊢ ((traceMatrix K ⇑B.basis).det • B.basis.equivFun z) i ∈ ⊥
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d : ℤ
a b : ℤ√d
⊢ star (a * b) = star b * star a

Tactic:
by ext <;> simp <;> ring

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

Goal state before:
pp: d : ℤ
a b : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : b ∣ a
z : ℤ
hz : z ∈ nonunits ℤ
hzdvdu : z ∣ b.re
hzdvdv : z ∣ b.im
⊢ z ∣ b.re ∧ z ∣ b.im

Tactic:
exact ⟨hzdvdu, hzdvdv⟩

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

Goal state before:
pp: d : ℕ
a : ℤ√↑d
n : ℕ
ha✝ : a.Nonneg
x y : ℕ
ha : { re := -↑x, im := ↑y }.Nonneg
⊢ (↑↑n * { re := -↑x, im := ↑y }).Nonneg

Tactic:
by
      rw [smul_val]; simpa using! nonnegg_neg_pos.2 (sqLe_smul n <| nonnegg_neg_pos.1 ha)

Goal state after:
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: case refine_2
α : Type u
S S' : Set (α → ℕ)
β : Type u
p : Poly (α ⊕ β)
pe : ∀ (v : α → ℕ), v ∈ S ↔ ∃ t, p (v ⊗ t) = 0
γ : Type u
q : Poly (α ⊕ γ)
qe : ∀ (v : α → ℕ), v ∈ S' ↔ ∃ t, q (v ⊗ t) = 0
v : α → ℕ
⊢ (∃ t, q (v ⊗ t) = 0) ↔ ∃ x, q ((v ⊗ x) ∘ (inl ⊗ inr ∘ inr)) = 0

Tactic:
· -- Porting note: putting everything on the same line fails
        refine inject_dummies_lem _ ((fun _ => none) ⊗ some) ?_ _ _
        exact fun _ => by simp only [elim_inr]

Goal state after:
Module: Mathlib.NumberTheory.MulChar.Duality

Goal state before:
pp: M : Type u_1
R : Type u_2
inst✝⁴ : CommMonoid M
inst✝³ : CommRing R
inst✝² : Finite M
inst✝¹ : HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)
inst✝ : Nontrivial R
a : M
ha : a ≠ 1
⊢ ∃ χ, χ a ≠ 1

Tactic:
by
  by_cases hu : IsUnit a
  · refine (exists_apply_ne_one_iff_exists_monoidHom hu.unit).mpr ?_
    refine CommGroup.exists_apply_ne_one_of_hasEnoughRootsOfUnity Mˣ R ?_
    contrapose ha
    rw [← hu.unit_spec, ha, Units.val_eq_one]
  · exact ⟨1, by simpa only [map_nonunit _ hu] using zero_ne_one⟩

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a k x y : ℕ
x✝ :
  1 < a ∧
    k ≤ y ∧
      (x = 1 ∧ y = 0 ∨
        ∃ u v s t b,
          x * x - (a * a - 1) * y * y = 1 ∧
            u * u - (a * a - 1) * v * v = 1 ∧
              s * s - (b * b - 1) * t * t = 1 ∧
                1 < b ∧ b ≡ 1 [MOD 4 * y] ∧ b ≡ a [MOD u] ∧ 0 < v ∧ y * y ∣ v ∧ s ≡ x [MOD u] ∧ t ≡ k [MOD 4 * y])
a1 : 1 < a
ky : k ≤ y
o :
  x = 1 ∧ y = 0 ∨
    ∃ u v s t b,
      x * x - (a * a - 1) * y * y = 1 ∧
        u * u - (a * a - 1) * v * v = 1 ∧
          s * s - (b * b - 1) * t * t = 1 ∧
            1 < b ∧ b ≡ 1 [MOD 4 * y] ∧ b ≡ a [MOD u] ∧ 0 < v ∧ y * y ∣ v ∧ s ≡ x [MOD u] ∧ t ≡ k [MOD 4 * y]
x1 : x = 1
y0 : y = 0
⊢ xn a1 k = x ∧ yn a1 k = y

Tactic:
y0

Goal state after:
a k x y : ℕ
x✝ :
  1 < a ∧
    k ≤ y ∧
      (x = 1 ∧ y = 0 ∨
        ∃ u v s t b,
          x * x - (a * a - 1) * y * y = 1 ∧
            u * u - (a * a - 1) * v * v = 1 ∧
              s * s - (b * b - 1) * t * t = 1 ∧
                1 < b ∧ b ≡ 1 [MOD 4 * y] ∧ b ≡ a [MOD u] ∧ 0 < v ∧ y * y ∣ v ∧ s ≡ x [MOD u] ∧ t ≡ k [MOD 4 * y])
a1 : 1 < a
ky : k ≤ 0
o :
  x = 1 ∧ y = 0 ∨
    ∃ u v s t b,
      x * x - (a * a - 1) * y * y = 1 ∧
        u * u - (a * a - 1) * v * v = 1 ∧
          s * s - (b * b - 1) * t * t = 1 ∧
            1 < b ∧ b ≡ 1 [MOD 4 * y] ∧ b ≡ a [MOD u] ∧ 0 < v ∧ y * y ∣ v ∧ s ≡ x [MOD u] ∧ t ≡ k [MOD 4 * y]
x1 : x = 1
y0 : y = 0
⊢ xn a1 k = x ∧ yn a1 k = y
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a k x y : ℕ
x✝ :
  1 < a ∧
    k ≤ y ∧
      (x = 1 ∧ y = 0 ∨
        ∃ u v s t b,
          x * x - (a * a - 1) * y * y = 1 ∧
            u * u - (a * a - 1) * v * v = 1 ∧
              s * s - (b * b - 1) * t * t = 1 ∧
                1 < b ∧ b ≡ 1 [MOD 4 * y] ∧ b ≡ a [MOD u] ∧ 0 < v ∧ y * y ∣ v ∧ s ≡ x [MOD u] ∧ t ≡ k [MOD 4 * y])
a1 : 1 < a
ky : k ≤ 0
o :
  x = 1 ∧ y = 0 ∨
    ∃ u v s t b,
      x * x - (a * a - 1) * y * y = 1 ∧
        u * u - (a * a - 1) * v * v = 1 ∧
          s * s - (b * b - 1) * t * t = 1 ∧
            1 < b ∧ b ≡ 1 [MOD 4 * y] ∧ b ≡ a [MOD u] ∧ 0 < v ∧ y * y ∣ v ∧ s ≡ x [MOD u] ∧ t ≡ k [MOD 4 * y]
x1 : x = 1
y0 : y = 0
⊢ xn a1 0 = 1 ∧ yn a1 0 = y

Tactic:
y0

Goal state after:
a k x y : ℕ
x✝ :
  1 < a ∧
    k ≤ y ∧
      (x = 1 ∧ y = 0 ∨
        ∃ u v s t b,
          x * x - (a * a - 1) * y * y = 1 ∧
            u * u - (a * a - 1) * v * v = 1 ∧
              s * s - (b * b - 1) * t * t = 1 ∧
                1 < b ∧ b ≡ 1 [MOD 4 * y] ∧ b ≡ a [MOD u] ∧ 0 < v ∧ y * y ∣ v ∧ s ≡ x [MOD u] ∧ t ≡ k [MOD 4 * y])
a1 : 1 < a
ky : k ≤ 0
o :
  x = 1 ∧ y = 0 ∨
    ∃ u v s t b,
      x * x - (a * a - 1) * y * y = 1 ∧
        u * u - (a * a - 1) * v * v = 1 ∧
          s * s - (b * b - 1) * t * t = 1 ∧
            1 < b ∧ b ≡ 1 [MOD 4 * y] ∧ b ≡ a [MOD u] ∧ 0 < v ∧ y * y ∣ v ∧ s ≡ x [MOD u] ∧ t ≡ k [MOD 4 * y]
x1 : x = 1
y0 : y = 0
⊢ xn a1 0 = 1 ∧ yn a1 0 = 0
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: n k : ℕ
hk : 0 < k
hn : 0 < n
w : ℕ := max n k
nw : n ≤ w
kw : k ≤ w
wpos : 0 < w
w1 : 1 < w + 1
a : ℕ := xn w1 w
a1 : 1 < a
na : n ≤ a
x : ℕ := xn a1 k
y : ℕ := yn a1 k
z : ℕ
ze : yn w1 w = w * z
⊢ n ^ k < a

Tactic:
calc
        n ^ k ≤ n ^ w := Nat.pow_le_pow_right hn kw
        _ < (w + 1) ^ w := Nat.pow_lt_pow_left (Nat.lt_succ_of_le nw) wpos.ne'
        _ ≤ a := xn_ge_a_pow w1 w

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: case mpr.inr.inr
m n k : ℕ
hk0 : 0 < k
hn0 : 0 < n
w a t z : ℕ
a1 : 1 < a
tm : xn a1 k ≡ yn a1 k * (a - n) + m [MOD t]
ta : 2 * a * n = t + (n * n + 1)
mt : m < t
nw : n ≤ w
kw : k ≤ w
zp : a * a - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1
hw0 : 0 < w
⊢ n ^ k = m

Tactic:
have hw1 : 1 < w + 1 := Nat.succ_lt_succ hw0

Goal state after:
case mpr.inr.inr
m n k : ℕ
hk0 : 0 < k
hn0 : 0 < n
w a t z : ℕ
a1 : 1 < a
tm : xn a1 k ≡ yn a1 k * (a - n) + m [MOD t]
ta : 2 * a * n = t + (n * n + 1)
mt : m < t
nw : n ≤ w
kw : k ≤ w
zp : a * a - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1
hw0 : 0 < w
hw1 : 1 < w + 1
⊢ n ^ k = m
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: case e'_3
ξ : ℝ
u : ℤ
ih : ∀ m < 1, ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = ξ.convergent n
left✝ : IsCoprime u ↑1
h₂ : |ξ - ↑u / ↑↑1| < (↑↑1 * (2 * ↑↑1 - 1))⁻¹
ht : ξ < ↑u
h₁ : ↑u + -(1 / 2) < ξ
hξ₁ : ⌊ξ⌋ = u - 1
Hξ : ξ ≠ ↑⌊ξ⌋
⊢ ↑u - (1 - 2⁻¹) = ↑u + -(1 / 2)

Tactic:
rw [sub_eq_add_neg]

Goal state after:
case e'_3
ξ : ℝ
u : ℤ
ih : ∀ m < 1, ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = ξ.convergent n
left✝ : IsCoprime u ↑1
h₂ : |ξ - ↑u / ↑↑1| < (↑↑1 * (2 * ↑↑1 - 1))⁻¹
ht : ξ < ↑u
h₁ : ↑u + -(1 / 2) < ξ
hξ₁ : ⌊ξ⌋ = u - 1
Hξ : ξ ≠ ↑⌊ξ⌋
⊢ ↑u + -(1 - 2⁻¹) = ↑u + -(1 / 2)
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: ξ : ℝ
q : ℚ
h : |ξ - ↑q| < 1 / (2 * ↑q.den ^ 2)
⊢ ∃ n, q = ξ.convergent n

Tactic:
refine q.num_div_den ▸ exists_rat_eq_convergent' ⟨?_, fun hd => ?_, ?_⟩

Goal state after:
case refine_1
ξ : ℝ
q : ℚ
h : |ξ - ↑q| < 1 / (2 * ↑q.den ^ 2)
⊢ IsCoprime q.num ↑q.den

case refine_2
ξ : ℝ
q : ℚ
h : |ξ - ↑q| < 1 / (2 * ↑q.den ^ 2)
hd : ↑q.den = 1
⊢ -(1 / 2) < ξ - ↑q.num

case refine_3
ξ : ℝ
q : ℚ
h : |ξ - ↑q| < 1 / (2 * ↑q.den ^ 2)
⊢ |ξ - ↑q.num / ↑↑q.den| < (↑↑q.den * (2 * ↑↑q.den - 1))⁻¹