mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.RootsOfUnity.Minpoly

Goal state before:
pp: n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
Q : ℤ[X] := minpoly ℤ (μ ^ p)
⊢ map (Int.castRingHom (ZMod p)) Q ^ p = map (Int.castRingHom (ZMod p)) ((expand ℤ p) Q)

Tactic:
rw [← ZMod.expand_card, map_expand]

Goal state after:
Module: Mathlib.RingTheory.RootsOfUnity.Minpoly

Goal state before:
pp: n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : P.Monic
Qmonic : Q.Monic
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : (P * Q).IsPrimitive
⊢ P * Q ∣ X ^ n - 1

Tactic:
IsPrimitive.Int.dvd_iff_map_cast_dvd_map_cast (P * Q) (X ^ n - 1) PQprim,

Goal state after:
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : P.Monic
Qmonic : Q.Monic
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : (P * Q).IsPrimitive
⊢ map (Int.castRingHom ℚ) (P * Q) ∣ map (Int.castRingHom ℚ) (X ^ n - 1)
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: case mp
R : Type u_4
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : DecidableEq R
n : ℕ
inst✝ : NeZero n
x : R
H : x ^ n = 1
⊢ ∃ a, a ∣ n ∧ x ∈ primitiveRoots a R

Tactic:
obtain ⟨k, hk, hx⟩ := exists_pos H (NeZero.ne n)

Goal state after:
case mp
R : Type u_4
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : DecidableEq R
n : ℕ
inst✝ : NeZero n
x : R
H : x ^ n = 1
k : ℕ
hk : k > 0
hx : IsPrimitiveRoot x k
⊢ ∃ a, a ∣ n ∧ x ∈ primitiveRoots a R
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots

Goal state before:
pp: n : ℕ
hpos : 0 < n
⊢ IsIntegral ℤ (cexp (2 * ↑Real.pi * I / ↑n))

Tactic:
exact (isPrimitiveRoot_exp n hpos.ne').isIntegral hpos

Goal state after:
Module: Mathlib.RingTheory.Adjoin.PowerBasis

Goal state before:
pp: case hsp
K : Type u_1
S : Type u_2
inst✝² : Field K
inst✝¹ : CommRing S
inst✝ : Algebra K S
x : S
hx : IsIntegral K x
hST : Function.Injective ⇑(algebraMap (↥K[x]) S)
hx' : IsIntegral K ⟨x, ⋯⟩
y : S
hy : y ∈ K[x]
a✝ : ⟨y, hy⟩ ∈ ⊤
this : (∃ f, ⟨y, hy⟩ = (aeval ⟨x, ⋯⟩) f) → ⟨y, hy⟩ ∈ Submodule.span K (Set.range fun i ↦ ⟨x, ⋯⟩ ^ ↑i)
⊢ ∃ f, ⟨y, hy⟩ = (aeval ⟨x, ⋯⟩) f

Tactic:
rw [adjoin_singleton_eq_range_aeval] at hy

Goal state after:
case hsp
K : Type u_1
S : Type u_2
inst✝² : Field K
inst✝¹ : CommRing S
inst✝ : Algebra K S
x : S
hx : IsIntegral K x
hST : Function.Injective ⇑(algebraMap (↥K[x]) S)
hx' : IsIntegral K ⟨x, ⋯⟩
y : S
hy✝ : y ∈ K[x]
hy : y ∈ (aeval x).range
a✝ : ⟨y, hy✝⟩ ∈ ⊤
this : (∃ f, ⟨y, hy✝⟩ = (aeval ⟨x, ⋯⟩) f) → ⟨y, hy✝⟩ ∈ Submodule.span K (Set.range fun i ↦ ⟨x, ⋯⟩ ^ ↑i)
⊢ ∃ f, ⟨y, hy✝⟩ = (aeval ⟨x, ⋯⟩) f
Module: Mathlib.RingTheory.Adjoin.PowerBasis

Goal state before:
pp: case neg
S : Type u_2
inst✝⁶ : CommRing S
R : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : Algebra R S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
i : Fin B.dim
a✝ : Nontrivial S
Q : R[X] := X ^ n %ₘ minpoly R B.gen
this : B.gen ^ n = (aeval B.gen) Q
hQ : ¬Q = 0
hlt : Q.natDegree < B.dim
j : ℕ
hj : j < B.dim
⊢ IsIntegral R (Q.coeff j • if ⟨j, hj⟩ = i then 1 else 0)

Tactic:
by_cases hij : (⟨j, hj⟩ : Fin _) = i

Goal state after:
case pos
S : Type u_2
inst✝⁶ : CommRing S
R : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : Algebra R S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
i : Fin B.dim
a✝ : Nontrivial S
Q : R[X] := X ^ n %ₘ minpoly R B.gen
this : B.gen ^ n = (aeval B.gen) Q
hQ : ¬Q = 0
hlt : Q.natDegree < B.dim
j : ℕ
hj : j < B.dim
hij : ⟨j, hj⟩ = i
⊢ IsIntegral R (Q.coeff j • if ⟨j, hj⟩ = i then 1 else 0)

case neg
S : Type u_2
inst✝⁶ : CommRing S
R : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : Algebra R S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
i : Fin B.dim
a✝ : Nontrivial S
Q : R[X] := X ^ n %ₘ minpoly R B.gen
this : B.gen ^ n = (aeval B.gen) Q
hQ : ¬Q = 0
hlt : Q.natDegree < B.dim
j : ℕ
hj : j < B.dim
hij : ¬⟨j, hj⟩ = i
⊢ IsIntegral R (Q.coeff j • if ⟨j, hj⟩ = i then 1 else 0)
Module: Mathlib.RingTheory.Adjoin.PowerBasis

Goal state before:
pp: K : Type u_1
S : Type u_2
inst✝⁶ : Field K
inst✝⁵ : CommRing S
inst✝⁴ : Algebra K S
R : Type u_3
inst✝³ : CommRing R
inst✝² : Algebra R S
inst✝¹ : Algebra R K
inst✝ : IsScalarTower R K S
B B' : PowerBasis K S
P : R[X]
h : (aeval B.gen) P = B'.gen
hB : IsIntegral R B.gen
hmin : minpoly K B.gen = Polynomial.map (algebraMap R K) (minpoly R B.gen)
i✝ : Fin B.dim
j : Fin B'.dim
i : Fin B.dim
⊢ IsIntegral R (∑ k ∈ Finset.range (P.natDegree + 1), (B.basis.repr (P.coeff k • B.gen ^ k)) i)

Tactic:
refine IsIntegral.sum _ fun n _ => ?_

Goal state after:
K : Type u_1
S : Type u_2
inst✝⁶ : Field K
inst✝⁵ : CommRing S
inst✝⁴ : Algebra K S
R : Type u_3
inst✝³ : CommRing R
inst✝² : Algebra R S
inst✝¹ : Algebra R K
inst✝ : IsScalarTower R K S
B B' : PowerBasis K S
P : R[X]
h : (aeval B.gen) P = B'.gen
hB : IsIntegral R B.gen
hmin : minpoly K B.gen = Polynomial.map (algebraMap R K) (minpoly R B.gen)
i✝ : Fin B.dim
j : Fin B'.dim
i : Fin B.dim
n : ℕ
x✝ : n ∈ Finset.range (P.natDegree + 1)
⊢ IsIntegral R ((B.basis.repr (P.coeff n • B.gen ^ n)) i)
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand

Goal state before:
pp: case inr.refine_2
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
⊢ n.totient * p ≤ n.totient * (p - 1).succ

Tactic:
Nat.sub_one,

Goal state after:
case inr.refine_2
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
⊢ n.totient * p ≤ n.totient * p.pred.succ
Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Goal state before:
pp: n : ℕ
inst✝³ : NeZero n
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
hno : Odd n
ζ x : K
hζ : IsPrimitiveRoot ζ n
hx : IsOfFinOrder x
hnegζ : IsPrimitiveRoot (-ζ) (2 * n)
⊢ ∃ r, x = (-ζ) ^ r

Tactic:
obtain ⟨k, hkpos, hkn⟩ := isOfFinOrder_iff_pow_eq_one.1 hx

Goal state after:
n : ℕ
inst✝³ : NeZero n
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
hno : Odd n
ζ x : K
hζ : IsPrimitiveRoot ζ n
hx : IsOfFinOrder x
hnegζ : IsPrimitiveRoot (-ζ) (2 * n)
k : ℕ
hkpos : 0 < k
hkn : x ^ k = 1
⊢ ∃ r, x = (-ζ) ^ r
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case neg
S : Set ℕ
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
hS : ¬∃ s ∈ S, s ≠ 0
⊢ IsCyclotomicExtension ∅ A B ↔ IsCyclotomicExtension ({1} \ {0}) A B

Tactic:
show {1} \ {0} = {1} by simp

Goal state after:
case neg
S : Set ℕ
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
hS : ¬∃ s ∈ S, s ≠ 0
⊢ IsCyclotomicExtension ∅ A B ↔ IsCyclotomicExtension {1} A B
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case neg.refine_2
S : Set ℕ
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
hS : ¬∃ s ∈ S, s ≠ 0
H : IsCyclotomicExtension {1} A B
⊢ adjoin A {b | ∃ n ∈ ∅, n ≠ 0 ∧ b ^ n = 1} = ⊤

Tactic:
simp [singleton_one]

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

Goal state before:
pp: K : Type w
L : Type z
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsIntegral K L
n : ℕ
inst✝ : NeZero n
ζ : L
hζ : IsPrimitiveRoot ζ n
⊢ IsCyclotomicExtension {n} K ↥K⟮ζ⟯

Tactic:
by
  change IsCyclotomicExtension {n} K (IntermediateField.adjoin K {ζ}).toSubalgebra
  rw [IntermediateField.adjoin_simple_toSubalgebra_of_isAlgebraic (IsAlgebraic.isAlgebraic ζ)]
  exact hζ.adjoin_isCyclotomicExtension K

Goal state after:
Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
pp: p✝ : ℕ
inst✝⁴ : Fact (Nat.Prime p✝)
n✝ : ℕ
K : Type u_1
K' : Type u_2
inst✝³ : Field K
inst✝² : Field K'
inst✝¹ : Fintype K
inst✝ : Fintype K'
hKK' : Fintype.card K = Fintype.card K'
p : ℕ
_char_p_K : CharP K p
p' : ℕ
_char_p'_K' : CharP K' p'
n : ℕ+
hp : Nat.Prime p
hK : Fintype.card K = p ^ ↑n
n' : ℕ+
hp' : Nat.Prime p'
hK' : Fintype.card K' = p' ^ ↑n'
hne : ¬p = p'
⊢ False

Tactic:
simpa [← hK, hK', hKK', hp'.ne_one] using Nat.coprime_pow_primes n n' hp hp' hne

Goal state after:
Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
pp: case refine_1
F : Type u_3
K : Type u_4
L : Type u_5
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Field L
inst✝¹ : Algebra F L
inst✝ : Finite L
h : Module.finrank F K ∣ Module.finrank F L
this✝⁴ : Finite F
this✝³ : Fintype F
this✝² : Module.Finite F K
this✝¹ : Finite K
this✝ : Fintype K
this : Fintype L
⊢ Polynomial.map (algebraMap F L) (X ^ Fintype.card L - X) ≠ 0

pp: case refine_2
F : Type u_3
K : Type u_4
L : Type u_5
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Field L
inst✝¹ : Algebra F L
inst✝ : Finite L
h : Module.finrank F K ∣ Module.finrank F L
this✝⁴ : Finite F
this✝³ : Fintype F
this✝² : Module.Finite F K
this✝¹ : Finite K
this✝ : Fintype K
this : Fintype L
⊢ Polynomial.map (algebraMap F L) (X ^ Fintype.card K - X) ∣ Polynomial.map (algebraMap F L) (X ^ Fintype.card L - X)

Tactic:
· exact map_ne_zero (FiniteField.X_pow_card_sub_X_ne_zero _ Fintype.one_lt_card)

Goal state after:
case refine_2
F : Type u_3
K : Type u_4
L : Type u_5
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Field L
inst✝¹ : Algebra F L
inst✝ : Finite L
h : Module.finrank F K ∣ Module.finrank F L
this✝⁴ : Finite F
this✝³ : Fintype F
this✝² : Module.Finite F K
this✝¹ : Finite K
this✝ : Fintype K
this : Fintype L
⊢ Polynomial.map (algebraMap F L) (X ^ Fintype.card K - X) ∣ Polynomial.map (algebraMap F L) (X ^ Fintype.card L - X)
Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar

Goal state before:
pp: N : ℕ
inst✝¹ : NeZero N
n : ℕ
inst✝ : NeZero n
x✝¹ x✝ : ZMod n
⊢ ⟨toUnits (toCircle (x✝¹ + x✝)), ⋯⟩ = ⟨toUnits (toCircle x✝¹), ⋯⟩ * ⟨toUnits (toCircle x✝), ⋯⟩

Tactic:
ext; simp [AddChar.map_add_eq_mul]

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝¹ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
m : ℕ
inst✝ : NeZero n
ψ : DirichletCharacter R m
h : (changeLevel ⋯) χ = (changeLevel ⋯) ψ
x : (ZMod n)ˣ
hx : x ∈ (ZMod.unitsMap ⋯).ker
this : (↑x).val ≡ 1 [MOD n.gcd m]
z : ℕ
hz₁ : z ≡ (↑x).val [MOD n]
hz₂ : z ≡ 1 [MOD m]
⊢ ↑z = ↑x

pp: case refine_2
R : Type u_1
inst✝¹ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
m : ℕ
inst✝ : NeZero n
ψ : DirichletCharacter R m
h : (changeLevel ⋯) χ = (changeLevel ⋯) ψ
x : (ZMod n)ˣ
hx : x ∈ (ZMod.unitsMap ⋯).ker
this : (↑x).val ≡ 1 [MOD n.gcd m]
z : ℕ
hz₁ : z ≡ (↑x).val [MOD n]
hz₂ : z ≡ 1 [MOD m]
⊢ ↑z = 1

Tactic:
· simpa [← ZMod.natCast_eq_natCast_iff] using hz₁

Goal state after:
case refine_2
R : Type u_1
inst✝¹ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
m : ℕ
inst✝ : NeZero n
ψ : DirichletCharacter R m
h : (changeLevel ⋯) χ = (changeLevel ⋯) ψ
x : (ZMod n)ˣ
hx : x ∈ (ZMod.unitsMap ⋯).ker
this : (↑x).val ≡ 1 [MOD n.gcd m]
z : ℕ
hz₁ : z ≡ (↑x).val [MOD n]
hz₂ : z ≡ 1 [MOD m]
⊢ ↑z = 1
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
n : ℕ
⊢ χ ^ (2 * n) * χ = χ

Tactic:
hχ.pow_even (even_two_mul _),

Goal state after:
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
n : ℕ
⊢ 1 * χ = χ
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: case refine_2
M : Type u_4
R : Type u_5
inst✝³ : CommMonoid M
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
χ : MulChar M R
h : χ ^ 2 = 1
x : M
⊢ χ x = 0 ∨ χ x = 1 ∨ χ x = -1

Tactic:
by_cases hx : IsUnit x
    · refine .inr <| sq_eq_one_iff.mp ?_
      rw [← χ.pow_apply' two_ne_zero, h, MulChar.one_apply hx]
    · exact .inl <| map_nonunit χ hx

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

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
⊢ χ⁻¹⁻¹.conductor ∣ (χ ^ (-1)).conductor

Tactic:
← zpow_neg_one,

Goal state after:
R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
⊢ (χ⁻¹ ^ (-1)).conductor ∣ (χ ^ (-1)).conductor
Module: Mathlib.Analysis.Fourier.ZMod

Goal state before:
pp: case pos
N : ℕ
inst✝² : NeZero N
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
Φ : ZMod N → E
j t : ZMod N
h : t = 0
⊢ ∑ i, stdAddChar (t * i) = ↑N

Tactic:
simp only [h, zero_mul, map_zero_eq_one, sum_const, card_univ, card,
        nsmul_eq_mul, mul_one]

Goal state after:
Module: Mathlib.Analysis.Hofer

Goal state before:
pp: X : Type u_1
inst✝¹ : MetricSpace X
inst✝ : CompleteSpace X
x : X
ε : ℝ
ε_pos : 0 < ε
ϕ : X → ℝ
cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ϕ
nonneg : ∀ (y : X), 0 ≤ ϕ y
reformulation : ∀ (x' : X) (k : ℕ), ε * ϕ x ≤ ε / 2 ^ k * ϕ x' ↔ 2 ^ k * ϕ x ≤ ϕ x'
this : Nonempty X
F : ℕ → X → X
hF : ∀ (k : ℕ) (x' : X), d x' x ≤ 2 * ε ∧ 2 ^ k * ϕ x ≤ ϕ x' → d x' (F k x') ≤ ε / 2 ^ k ∧ 2 * ϕ x' < ϕ (F k x')
u : ℕ → X := fun n ↦ Nat.recOn n x F
hu :
  ∀ (n : ℕ), d (u n) x ≤ 2 * ε ∧ 2 ^ n * ϕ x ≤ ϕ (u n) → d (u n) (u (n + 1)) ≤ ε / 2 ^ n ∧ 2 * ϕ (u n) < ϕ (u (n + 1))
key : ∀ (n : ℕ), d (u n) (u (n + 1)) ≤ ε / 2 ^ n ∧ 2 * ϕ (u n) < ϕ (u (n + 1))
key₁ : ∀ (x : ℕ), d (u x) (u (x + 1)) ≤ ε / 2 ^ x
key₂ : ∀ (x : ℕ), 2 * ϕ (u x) < ϕ (u (x + 1))
cauchy_u : CauchySeq u
⊢ False

Tactic:
obtain ⟨y, limy⟩ : ∃ y, Tendsto u atTop (𝓝 y) := CompleteSpace.complete cauchy_u

Goal state after:
X : Type u_1
inst✝¹ : MetricSpace X
inst✝ : CompleteSpace X
x : X
ε : ℝ
ε_pos : 0 < ε
ϕ : X → ℝ
cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ϕ
nonneg : ∀ (y : X), 0 ≤ ϕ y
reformulation : ∀ (x' : X) (k : ℕ), ε * ϕ x ≤ ε / 2 ^ k * ϕ x' ↔ 2 ^ k * ϕ x ≤ ϕ x'
this : Nonempty X
F : ℕ → X → X
hF : ∀ (k : ℕ) (x' : X), d x' x ≤ 2 * ε ∧ 2 ^ k * ϕ x ≤ ϕ x' → d x' (F k x') ≤ ε / 2 ^ k ∧ 2 * ϕ x' < ϕ (F k x')
u : ℕ → X := fun n ↦ Nat.recOn n x F
hu :
  ∀ (n : ℕ), d (u n) x ≤ 2 * ε ∧ 2 ^ n * ϕ x ≤ ϕ (u n) → d (u n) (u (n + 1)) ≤ ε / 2 ^ n ∧ 2 * ϕ (u n) < ϕ (u (n + 1))
key : ∀ (n : ℕ), d (u n) (u (n + 1)) ≤ ε / 2 ^ n ∧ 2 * ϕ (u n) < ϕ (u (n + 1))
key₁ : ∀ (x : ℕ), d (u x) (u (x + 1)) ≤ ε / 2 ^ x
key₂ : ∀ (x : ℕ), 2 * ϕ (u x) < ϕ (u (x + 1))
cauchy_u : CauchySeq u
y : X
limy : Tendsto u atTop (𝓝 y)
⊢ False
Module: Mathlib.Analysis.InnerProductSpace.Coalgebra

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_3
inst✝¹ : Fintype n
inst✝ : DecidableEq n
i✝ : n
⊢ (comul ∘ₗ LinearMap.single 𝕜 (fun i ↦ 𝕜) i✝) 1 =
    ((map ↑↑(equiv n 𝕜) ↑↑(equiv n 𝕜) ∘ₗ
          adjoint (↑↑(equiv n 𝕜).symm ∘ₗ mul' 𝕜 (n → 𝕜) ∘ₗ map ↑↑(equiv n 𝕜) ↑↑(equiv n 𝕜)) ∘ₗ ↑↑(equiv n 𝕜).symm) ∘ₗ
        LinearMap.single 𝕜 (fun i ↦ 𝕜) i✝)
      1

Tactic:
simp only [comp_apply, ← toLinearMap_congr, LinearEquiv.coe_coe, ← LinearEquiv.symm_apply_eq]

Goal state after:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_3
inst✝¹ : Fintype n
inst✝ : DecidableEq n
i✝ : n
⊢ (TensorProduct.congr ↑(equiv n 𝕜) ↑(equiv n 𝕜)).symm (comul ((LinearMap.single 𝕜 (fun i ↦ 𝕜) i✝) 1)) =
    (adjoint (↑↑(equiv n 𝕜).symm ∘ₗ mul' 𝕜 (n → 𝕜) ∘ₗ ↑(TensorProduct.congr ↑(equiv n 𝕜) ↑(equiv n 𝕜))))
      (↑(equiv n 𝕜).symm ((LinearMap.single 𝕜 (fun i ↦ 𝕜) i✝) 1))
Module: Mathlib.Analysis.InnerProductSpace.ExteriorPower

Goal state before:
pp: n : ℕ
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : FiniteDimensional ℝ E
x : ↥(⋀[ℝ]^n E)
h : (innerProductForm x) x = 0
⊢ x = 0

Tactic:
rw [innerProductForm_self x (stdOrthonormalBasis ℝ E),
      Finset.sum_eq_zero_iff_of_nonneg (fun _ _ ↦ sq_nonneg _)] at h

Goal state after:
n : ℕ
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : FiniteDimensional ℝ E
x : ↥(⋀[ℝ]^n E)
h : ∀ i ∈ Finset.univ, ((Module.Basis.exteriorPower n (stdOrthonormalBasis ℝ E).toBasis).repr x) i ^ 2 = 0
⊢ x = 0
Module: Mathlib.Analysis.InnerProductSpace.Positive

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
S : E →L[𝕜] F
⊢ (S ∘SL adjoint S).IsPositive

Tactic:
simpa using! isPositive_one.conj_adjoint S

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.LaxMilgram

Goal state before:
pp: V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
⊢ (↑(continuousLinearMapOfBilin B)).range = ⊤

Tactic:
have := coercive.isClosed_range.completeSpace_coe
  rw [← B♯.range.orthogonal_orthogonal]
  rw [Submodule.eq_top_iff']
  intro v w mem_w_orthogonal
  rcases coercive with ⟨C, C_pos, coercivity⟩
  obtain rfl : w = 0 := by
    rw [← norm_eq_zero, ← mul_self_eq_zero, ← mul_right_inj' C_pos.ne', mul_zero, ←
      mul_assoc]
    apply le_antisymm
    · calc
        C * ‖w‖ * ‖w‖ ≤ B w w := coercivity w
        _ = ⟪B♯ w, w⟫_ℝ := (continuousLinearMapOfBilin_apply B w w).symm
        _ = 0 := mem_w_orthogonal _ ⟨w, rfl⟩
    · positivity
  exact inner_zero_left _

Goal state after:
Module: Mathlib.Dynamics.BirkhoffSum.NormedSpace

Goal state before:
pp: 𝕜 : Type u_1
X : Type u_2
E : Type u_3
inst✝³ : PseudoEMetricSpace X
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : X → X
g : X → E
hf : LipschitzWith 1 f
hg : UniformContinuous g
ε : ℝ
hε : 0 < ε
δ : ℝ≥0∞
hδ₀ : 0 < δ
hδε : ∀ (x y : X), (x, y) ∈ {p | edist p.1 p.2 ≤ δ} → (g x, g y) ∈ {p | dist p.1 p.2 ≤ ε}
x y : X
h : edist x y < δ
n : ℕ
⊢ (∑ k ∈ Finset.range n, dist (g (f^[k] x)) (g (f^[k] y))) / ↑n ≤ (∑ _k ∈ Finset.range n, ε) / ↑n

Tactic:
gcongr
      refine hδε _ _ ?_
      simpa using (hf.iterate _).edist_le_mul_of_le h.le

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.SingularValues

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : FiniteDimensional 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : FiniteDimensional 𝕜 F
T : E →ₗ[𝕜] F
⊢ finrank 𝕜 ↥T.range ∉ Finset.range (finrank 𝕜 ↥T.range)

Tactic:
exact Finset.notMem_range_self

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.TensorProduct

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace 𝕜 H
f : E →L[𝕜] F
g : G →L[𝕜] H
⊢ mapL f g ∘SL ↑↑(commIsometry 𝕜 G E) = ↑↑(commIsometry 𝕜 H F) ∘SL mapL g f

Tactic:
by ext; simp [map_comm]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Volume.Measure

Goal state before:
pp: X : Type u_1
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
basis : OrthonormalBasis (Fin 0) ℝ (EuclideanSpace ℝ (Fin 0)) := EuclideanSpace.basisFun (Fin 0) ℝ
heq : {0} = parallelepiped ⇑basis
h✝ : volume = volume.addHaarScalarFactor μH[↑0] • μH[↑0]
h : volume.addHaarScalarFactor μH[0] • 1 = 1
⊢ μHE[0] = μH[0]

Tactic:
ENNReal.smul_def,

Goal state after:
X : Type u_1
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
basis : OrthonormalBasis (Fin 0) ℝ (EuclideanSpace ℝ (Fin 0)) := EuclideanSpace.basisFun (Fin 0) ℝ
heq : {0} = parallelepiped ⇑basis
h✝ : volume = volume.addHaarScalarFactor μH[↑0] • μH[↑0]
h : ↑(volume.addHaarScalarFactor μH[0]) • 1 = 1
⊢ μHE[0] = μH[0]
Module: Mathlib.Geometry.Euclidean.Volume.Measure

Goal state before:
pp: V : Type u_3
P : Type u_4
inst✝⁸ : NormedAddCommGroup V
inst✝⁷ : InnerProductSpace ℝ V
inst✝⁶ : MeasurableSpace V
inst✝⁵ : BorelSpace V
inst✝⁴ : FiniteDimensional ℝ V
inst✝³ : MetricSpace P
inst✝² : MeasurableSpace P
inst✝¹ : BorelSpace P
inst✝ : NormedAddTorsor V P
s : Submodule ℝ V
p : P
⊢ MeasurePreserving
    (⇑(s.orthogonalDecomposition.toHomeomorph.toMeasurableEquiv.trans (MeasurableEquiv.toLp 2 (↥s × ↥sᗮ)).symm)) volume
    volume

Tactic:
refine s.orthogonalDecomposition.measurePreserving.trans ?_

Goal state after:
V : Type u_3
P : Type u_4
inst✝⁸ : NormedAddCommGroup V
inst✝⁷ : InnerProductSpace ℝ V
inst✝⁶ : MeasurableSpace V
inst✝⁵ : BorelSpace V
inst✝⁴ : FiniteDimensional ℝ V
inst✝³ : MetricSpace P
inst✝² : MeasurableSpace P
inst✝¹ : BorelSpace P
inst✝ : NormedAddTorsor V P
s : Submodule ℝ V
p : P
⊢ MeasurePreserving (⇑(MeasurableEquiv.toLp 2 (↥s × ↥sᗮ)).symm) volume volume
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: X : Type u_2
inst✝ : EMetricSpace X
m : ℝ≥0∞ → ℝ≥0∞
c : ℝ≥0
hc : c ≠ 0
⊢ mkMetric (c • m) = c • mkMetric m

Tactic:
ENNReal.smul_def,

Goal state after:
X : Type u_2
inst✝ : EMetricSpace X
m : ℝ≥0∞ → ℝ≥0∞
c : ℝ≥0
hc : c ≠ 0
⊢ mkMetric (↑c • m) = c • mkMetric m
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: X : Type u_2
inst✝ : EMetricSpace X
m : ℝ≥0∞ → ℝ≥0∞
c : ℝ≥0
hc : c ≠ 0
⊢ mkMetric (↑c • m) = c • mkMetric m

Tactic:
ENNReal.smul_def,

Goal state after:
X : Type u_2
inst✝ : EMetricSpace X
m : ℝ≥0∞ → ℝ≥0∞
c : ℝ≥0
hc : c ≠ 0
⊢ mkMetric (↑c • m) = ↑c • mkMetric m
Module: Mathlib.Analysis.InnerProductSpace.NormDet

Goal state before:
pp: 𝕜 : Type u_1
U : Type u_2
V : Type u_3
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup U
inst✝⁵ : InnerProductSpace 𝕜 U
inst✝⁴ : FiniteDimensional 𝕜 U
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace 𝕜 V
ι : Type u_5
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : U →ₗ[𝕜] V
b : OrthonormalBasis ι 𝕜 U
⊢ ↑(f.normDet ^ 2) = (Matrix.gram 𝕜 fun x ↦ f (b x)).det

Tactic:
by
  suffices ↑(f.normDet ^ 2) = (Matrix.gram 𝕜 (f.rangeRestrict <| b ·)).det by
    simpa
  by_cases h : f.ker = ⊥
  · let bv := orthonormalBasis_range h b
    rw [Matrix.gram_eq_conjTranspose_mul bv, Matrix.det_mul, Matrix.det_conjTranspose]
    rw [RCLike.star_def, RCLike.conj_mul, f.normDet_eq_norm_det_toMatrix_rangeRestrict b bv]
    simp only [map_pow]
    congr
    ext i j
    simp [LinearMap.toMatrix_apply]
  · trans 0
    · simp [show f.normDet = 0 from (f.normDet_eq_zero_tfae.out 1 0).mp h]
    have hrank := (f.normDet_eq_zero_tfae.out 1 3).mp h
    symm
    contrapose! hrank with h0
    rw [finrank_eq_card_basis b.toBasis]
    exact (Matrix.linearIndependent_of_det_gram_ne_zero h0).fintype_card_le_finrank

Goal state after: