mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
pp: K : Type u_1
F : Type u_2
inst✝³ : Field K
inst✝² : Fintype K
inst✝¹ : Field F
inst✝ : Algebra F K
h : (X ^ Fintype.card K - X).natDegree = Fintype.card K
⊢ (Polynomial.map (algebraMap F K) (X ^ Fintype.card K) - Polynomial.map (algebraMap F K) X).roots.card =
    (Polynomial.map (algebraMap F K) (X ^ Fintype.card K) - Polynomial.map (algebraMap F K) X).natDegree

Tactic:
Polynomial.map_pow,

Goal state after:
K : Type u_1
F : Type u_2
inst✝³ : Field K
inst✝² : Fintype K
inst✝¹ : Field F
inst✝ : Algebra F K
h : (X ^ Fintype.card K - X).natDegree = Fintype.card K
⊢ (Polynomial.map (algebraMap F K) X ^ Fintype.card K - Polynomial.map (algebraMap F K) X).roots.card =
    (Polynomial.map (algebraMap F K) X ^ Fintype.card K - Polynomial.map (algebraMap F K) X).natDegree
Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
pp: p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
h : n ≠ 0
this : Fintype (GaloisField p n)
g_poly : (ZMod p)[X] := X ^ p ^ n - X
hp : 1 < p
aux : g_poly ≠ 0
key : Fintype.card ↑(g_poly.rootSet (GaloisField p n)) = g_poly.natDegree
nat_degree_eq : g_poly.natDegree = p ^ n
⊢ Module.finrank (ZMod p) (GaloisField p n) = n

Tactic:
rw [nat_degree_eq] at key

Goal state after:
p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
h : n ≠ 0
this : Fintype (GaloisField p n)
g_poly : (ZMod p)[X] := X ^ p ^ n - X
hp : 1 < p
aux : g_poly ≠ 0
key : Fintype.card ↑(g_poly.rootSet (GaloisField p n)) = p ^ n
nat_degree_eq : g_poly.natDegree = p ^ n
⊢ Module.finrank (ZMod p) (GaloisField p n) = n
Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
pp: p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
h : n ≠ 0
this : Fintype (GaloisField p n)
g_poly : (ZMod p)[X] := X ^ p ^ n - X
hp : 1 < p
aux : g_poly ≠ 0
key : Fintype.card ↑(g_poly.rootSet (GaloisField p n)) = p ^ n
nat_degree_eq : g_poly.natDegree = p ^ n
⊢ ∀
    x ∈
      Subring.closure
        (Set.range ⇑(algebraMap (ZMod p) (GaloisField p n)) ∪ (X ^ p ^ n - X).rootSet (X ^ p ^ n - X).SplittingField),
    x ∈ (X ^ p ^ n - X).rootSet (GaloisField p n)

Tactic:
intro x hx

Goal state after:
p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
h : n ≠ 0
this : Fintype (GaloisField p n)
g_poly : (ZMod p)[X] := X ^ p ^ n - X
hp : 1 < p
aux : g_poly ≠ 0
key : Fintype.card ↑(g_poly.rootSet (GaloisField p n)) = p ^ n
nat_degree_eq : g_poly.natDegree = p ^ n
x : GaloisField p n
hx :
  x ∈
    Subring.closure
      (Set.range ⇑(algebraMap (ZMod p) (GaloisField p n)) ∪ (X ^ p ^ n - X).rootSet (X ^ p ^ n - X).SplittingField)
⊢ x ∈ (X ^ p ^ n - X).rootSet (GaloisField p n)
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case pos
n : ℕ
inst✝³ : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
hB : IsCyclotomicExtension S A B
r : B
hr : IsPrimitiveRoot r n
hn : n = 0
⊢ IsCyclotomicExtension (S ∪ {n}) A B

pp: case neg
n : ℕ
inst✝³ : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
hB : IsCyclotomicExtension S A B
r : B
hr : IsPrimitiveRoot r n
hn : ¬n = 0
⊢ IsCyclotomicExtension (S ∪ {n}) A B

Tactic:
· rwa [hn, eq_self_sdiff_zero, Set.union_sdiff_right, ← eq_self_sdiff_zero]

Goal state after:
case neg
n : ℕ
inst✝³ : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
hB : IsCyclotomicExtension S A B
r : B
hr : IsPrimitiveRoot r n
hn : ¬n = 0
⊢ IsCyclotomicExtension (S ∪ {n}) A B
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: case convert_5
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, q - 1 ≤ ‖↑q - ζ'‖
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ' ∈ primitiveRoots n ℂ, q - 1 < ‖↑q - ζ'‖
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
⊢ ∀ a ∈ primitiveRoots n ℂ, q ≤ ‖↑q - a‖ + 1 ∧ True

Tactic:
intro x hx

Goal state after:
case convert_5
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, q - 1 ≤ ‖↑q - ζ'‖
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ' ∈ primitiveRoots n ℂ, q - 1 < ‖↑q - ζ'‖
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
x : ℂ
hx : x ∈ primitiveRoots n ℂ
⊢ q ≤ ‖↑q - x‖ + 1 ∧ True
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case refine_2.inr
n : ℕ
inst✝³ : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : ∃ s ∈ S, s ≠ 0 ∧ n ∣ s
H : IsCyclotomicExtension (S ∪ {n}) A B
x : B
m : ℕ
hxpow : m ≠ 0 ∧ x ^ m = 1
hm : m ∈ S
⊢ ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1

Tactic:
exact ⟨m, ⟨hm, hxpow⟩⟩

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: case convert_5
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ < q + 1
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
⊢ ∀ a ∈ primitiveRoots n ℂ, ‖↑q - a‖ ≤ ↑(q + 1).toNNReal

Tactic:
intro x hx

Goal state after:
case convert_5
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ < q + 1
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
x : ℂ
hx : x ∈ primitiveRoots n ℂ
⊢ ‖↑q - x‖ ≤ ↑(q + 1).toNNReal
Module: Mathlib.Data.ZMod.Units

Goal state before:
pp: n m : ℕ
hm : NeZero m
h : n ∣ m
⊢ ∀ (x : ℕ), x.Coprime n → ∃ k, (x + k * n).Coprime m

Tactic:
intro x hx

Goal state after:
n m : ℕ
hm : NeZero m
h : n ∣ m
x : ℕ
hx : x.Coprime n
⊢ ∃ k, (x + k * n).Coprime m
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: n : ℕ
inst✝³ : NeZero n
S : Set ℕ
K : Type w
L : Type z
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : IsCyclotomicExtension S K L
hS : n ∈ S
⊢ (map (algebraMap K L) (X ^ n) - 1).Splits

Tactic:
Polynomial.map_pow,

Goal state after:
n : ℕ
inst✝³ : NeZero n
S : Set ℕ
K : Type w
L : Type z
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : IsCyclotomicExtension S K L
hS : n ∈ S
⊢ (map (algebraMap K L) X ^ n - 1).Splits
Module: Mathlib.Data.ZMod.Units

Goal state before:
pp: case neg
n m : ℕ
hm : NeZero m
h : n ∣ m
x : ℕ
hx : x.Coprime n
ps : Finset ℕ := {p ∈ m.primeFactors | ¬p ∣ x}
p : ℕ
pp : Nat.Prime p
hp : p ∣ x + ps.prod id * n
hpn : p ∣ m
hpx : ¬p ∣ x
⊢ False

Tactic:
have pps : p ∈ ps := Finset.mem_filter.mpr ⟨Nat.mem_primeFactors.mpr ⟨pp, hpn, hm.out⟩, hpx⟩

Goal state after:
case neg
n m : ℕ
hm : NeZero m
h : n ∣ m
x : ℕ
hx : x.Coprime n
ps : Finset ℕ := {p ∈ m.primeFactors | ¬p ∣ x}
p : ℕ
pp : Nat.Prime p
hp : p ∣ x + ps.prod id * n
hpn : p ∣ m
hpx : ¬p ∣ x
pps : p ∈ ps
⊢ False
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: n : ℕ
inst✝⁴ : NeZero n
S : Set ℕ
K : Type w
L : Type z
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension S K L
hS : n ∈ S
⊢ (map (algebraMap K L) (cyclotomic n K)).Splits

Tactic:
refine (splits_X_pow_sub_one K L hS).of_dvd
    (map_ne_zero (X_pow_sub_C_ne_zero (NeZero.pos _) _)) ((map_dvd_map' _).mpr ?_)

Goal state after:
n : ℕ
inst✝⁴ : NeZero n
S : Set ℕ
K : Type w
L : Type z
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension S K L
hS : n ∈ S
⊢ cyclotomic n K ∣ X ^ n - 1
Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter

Goal state before:
pp: R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommMonoid R'
inst✝ : Finite R
e : AddChar R R'
r : R
hr : ¬IsUnit r
⊢ ¬(e.mulShift r).IsPrimitive

Tactic:
by
  simp only [IsPrimitive, not_forall]
  simp only [isUnit_iff_mem_nonZeroDivisors_of_finite,
    mem_nonZeroDivisors_iff_right, not_forall] at hr
  rcases hr with ⟨x, h, h'⟩
  exact ⟨x, h', by simp only [mulShift_mulShift, mul_comm r, h, mulShift_zero, not_ne_iff]⟩

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter

Goal state before:
pp: C : Type v
inst✝¹ : CommMonoid C
n : ℕ
inst✝ : NeZero n
ζ : C
h : IsPrimitiveRoot ζ n
⊢ (zmodChar n ⋯).IsPrimitive

Tactic:
apply zmod_char_primitive_of_eq_one_only_at_zero
  intro a ha
  rw [zmodChar_apply, ← pow_zero ζ] at ha
  exact (ZMod.val_eq_zero a).mp (IsPrimitiveRoot.pow_inj h (ZMod.val_lt a) (NeZero.pos _) ha)

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

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
H : Set (ZMod n)ˣ
χ : DirichletCharacter R n
⊢ χ ∈ annihilator R H ↔ ∀ a ∈ H, χ ↑a = 1

Tactic:
rw [mem_annihilator_iff_mem_closure]
  refine ⟨fun h a ha ↦ h a (Submonoid.subset_closure ha), fun h x hx ↦ ?_⟩
  refine Submonoid.closure_induction h (by simp) (fun a b _ _ ha hb ↦ ?_) hx
  simp [map_mul, ha, hb]

Goal state after:
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
p n : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit ↑p
hp' : p ≠ 2
hg : gaussSum χ ψ ^ 2 = χ (-1) * ↑(Fintype.card R)
hf : gaussSum χ ψ = 0
⊢ False

Tactic:
rw [hf, zero_pow two_ne_zero, eq_comm, mul_eq_zero] at hg

Goal state after:
R : Type u
inst✝³ : CommRing R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
p n : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit ↑p
hp' : p ≠ 2
hg : χ (-1) = 0 ∨ ↑(Fintype.card R) = 0
hf : gaussSum χ ψ = 0
⊢ False
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod ↑8) F := primitiveZModChar 8 F ⋯
ψ₈char : AddChar (ZMod 8) FF := ψ₈.char
τ : FF := ψ₈char 1
τ_spec : τ ^ 4 = -1
χ : MulChar (ZMod 8) FF := χ₈.ringHomComp (Int.castRingHom FF)
hχ : χ (-1) = 1
hq : χ.IsQuadratic
h₁ : (fun a ↦ ↑(χ₈ a) * τ ^ ↑a) = fun a ↦ χ a * ψ₈char a
hg₁ : gaussSum χ ψ₈char = 2 * (τ - τ ^ 3)
hg : gaussSum χ ψ₈char ^ 2 = χ (-1) * ↑(Fintype.card (ZMod 8))
h : ↑8 ^ (Fintype.card F / 2) = χ (↑(ringChar F) ^ ↑n)
⊢ 2 ^ (Fintype.card F / 2) = ↑(χ₈ ↑(Fintype.card F))

Tactic:
← Nat.cast_pow (ringChar F),

Goal state after:
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod ↑8) F := primitiveZModChar 8 F ⋯
ψ₈char : AddChar (ZMod 8) FF := ψ₈.char
τ : FF := ψ₈char 1
τ_spec : τ ^ 4 = -1
χ : MulChar (ZMod 8) FF := χ₈.ringHomComp (Int.castRingHom FF)
hχ : χ (-1) = 1
hq : χ.IsQuadratic
h₁ : (fun a ↦ ↑(χ₈ a) * τ ^ ↑a) = fun a ↦ χ a * ψ₈char a
hg₁ : gaussSum χ ψ₈char = 2 * (τ - τ ^ 3)
hg : gaussSum χ ψ₈char ^ 2 = χ (-1) * ↑(Fintype.card (ZMod 8))
h : ↑8 ^ (Fintype.card F / 2) = χ ↑(ringChar F ^ ↑n)
⊢ 2 ^ (Fintype.card F / 2) = ↑(χ₈ ↑(Fintype.card F))
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
T : E →ₗ[𝕜] E
f : E ≃ₗᵢ[𝕜] F
x✝ : T.IsSymmetric
h : ∀ (x : F), 0 ≤ re ⟪T (f.symm x), f.symm x⟫
x : E
⊢ 0 ≤ re ⟪T x, x⟫

Tactic:
by simpa using h (f x)

Goal state after:
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: ι : Type u_1
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : Fintype ι
p : ℝ
hp : (↑#ι).HolderConjugate p
u : (ι → ℝ) → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
this : 1 ≤ ↑#ι - 1
⊢ ∫⁻ (x : ι → ℝ), ‖u x‖ₑ ^ p = ∫⁻ (x : ι → ℝ), (‖u x‖ₑ ^ (1 / (↑#ι - 1))) ^ ↑#ι

Tactic:
congr! 2 with x

Goal state after:
ι : Type u_1
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : Fintype ι
p : ℝ
hp : (↑#ι).HolderConjugate p
u : (ι → ℝ) → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
this : 1 ≤ ↑#ι - 1
x : ι → ℝ
⊢ ‖u x‖ₑ ^ p = (‖u x‖ₑ ^ (1 / (↑#ι - 1))) ^ ↑#ι
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: ι : Type u_1
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : Fintype ι
p : ℝ
hp : (↑#ι).HolderConjugate p
u : (ι → ℝ) → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
this : 1 ≤ ↑#ι - 1
⊢ ∫⁻ (x : ι → ℝ), (‖u x‖ₑ ^ (1 / (↑#ι - 1))) ^ ↑#ι = ∫⁻ (x : ι → ℝ), ∏ _i, ‖u x‖ₑ ^ (1 / (↑#ι - 1))

Tactic:
congr! 2 with x

Goal state after:
ι : Type u_1
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : Fintype ι
p : ℝ
hp : (↑#ι).HolderConjugate p
u : (ι → ℝ) → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
this : 1 ≤ ↑#ι - 1
x : ι → ℝ
⊢ (‖u x‖ₑ ^ (1 / (↑#ι - 1))) ^ ↑#ι = ∏ _i, ‖u x‖ₑ ^ (1 / (↑#ι - 1))
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
⊢ ∃ C, 0 < C ∧ ∀ (v : V), C * ‖v‖ ≤ ‖(continuousLinearMapOfBilin B) v‖

Tactic:
rcases coercive with ⟨C, C_ge_0, coercivity⟩

Goal state after:
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
C : ℝ
C_ge_0 : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ (B u) u
⊢ ∃ C, 0 < C ∧ ∀ (v : V), C * ‖v‖ ≤ ‖(continuousLinearMapOfBilin B) v‖
Module: Mathlib.Analysis.InnerProductSpace.Positive

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
f : E →L[𝕜] E
c : ℝ≥0
hc : 0 < c
h : ∀ (x : E), ‖x‖ ^ 2 * ↑c ≤ ‖⟪f x, x⟫‖
h_anti : AntilipschitzWith c⁻¹ ⇑f
⊢ ∀ x ∈ (↑f).rangeᗮ, x = 0

Tactic:
intro x hx

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
f : E →L[𝕜] E
c : ℝ≥0
hc : 0 < c
h : ∀ (x : E), ‖x‖ ^ 2 * ↑c ≤ ‖⟪f x, x⟫‖
h_anti : AntilipschitzWith c⁻¹ ⇑f
x : E
hx : x ∈ (↑f).rangeᗮ
⊢ x = 0
Module: Mathlib.Topology.Algebra.Module.LinearPMap

Goal state before:
pp: case h'
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
x : E
h1 : x ∈ (f.closure.domRestrict f.domain).domain
h2 : x ∈ f.domain
z : ↥f.closure.domain := ⟨x, ⋯⟩
hyz : x = ↑z
⊢ ↑(f.closure.domRestrict f.domain) ⟨x, h1⟩ = ↑f.closure z

Tactic:
exact domRestrict_apply hyz

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
A : E →ₗ.[𝕜] E
hA : IsSelfAdjoint A
h : ¬Dense ↑A.domain
⊢ False

Tactic:
rw [isSelfAdjoint_def] at hA

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
A : E →ₗ.[𝕜] E
hA : A† = A
h : ¬Dense ↑A.domain
⊢ False
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
⊢ ContinuousLinearMap.lTensor H f ∘SL ContinuousLinearMap.rTensor E g = mapL g f

Tactic:
by ext; simp [← LinearMap.lTensor_comp_rTensor]

Goal state after:
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
hcvx : Convex ℝ s
hne : s.Nonempty
⊢ dimH s = ↑(finrank ℝ ↥(vectorSpan ℝ s))

Tactic:
by
  have := hne.to_subtype
  let φ := AffineIsometryEquiv.constVSub ℝ
    (⟨hne.some, subset_affineSpan ℝ s hne.some_mem⟩ : affineSpan ℝ s)
  have hs_eq : s = (↑) '' ((↑) ⁻¹' s : Set (affineSpan ℝ s)) :=
    (image_preimage_eq_of_subset <| (subset_affineSpan ℝ s).trans Subtype.range_coe.superset).symm
  rw [hs_eq, isometry_subtype_coe.dimH_image, ← φ.isometry.dimH_image,
      Real.dimH_of_nonempty_interior, direction_affineSpan ℝ s, ← hs_eq]
  simp_rw [← AffineIsometryEquiv.coe_toHomeomorph, ← φ.toHomeomorph.image_interior, image_nonempty]
  simpa [intrinsicInterior] using (intrinsicInterior_nonempty hcvx).mpr hne

Goal state after:
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
p : P
v : V
hv : v ≠ 0
t : Set P
ht : MeasurableSet t
hrank : finrank ℝ ↥(AffineSubspace.mk' p (ℝ ∙ v)).direction = 1
hrank' : finrank ℝ ↥(AffineSubspace.mk' p (ℝ ∙ v)).directionᗮ = finrank ℝ V - 1
f : ℝ ≃L[ℝ] ↥(AffineSubspace.mk' p (ℝ ∙ v)).direction :=
  (ContinuousLinearEquiv.toSpanNonzeroSingleton ℝ v hv).trans
    (ContinuousLinearEquiv.ofEq (ℝ ∙ v) (AffineSubspace.mk' p (ℝ ∙ v)).direction ⋯)
hf : MeasurableEmbedding ⇑f
p' : ↥(AffineSubspace.mk' p (ℝ ∙ v)) := ⟨p, ⋯⟩
g : ℝ → ↥(AffineSubspace.mk' p (ℝ ∙ v)) := ⇑(IsometryEquiv.vaddConst p') ∘ ⇑f
hadd : MeasurableEmbedding ⇑(IsometryEquiv.vaddConst p')
hg : MeasurableEmbedding g
v' : ↥(AffineSubspace.mk' p (ℝ ∙ v)).direction := ⟨v, ⋯⟩
⊢ v' ≠ 0

Tactic:
simpa [v'] using hv

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: case a
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
x : X
⊢ μH[0] {x} ≤ 1

pp: case a
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
x : X
⊢ 1 ≤ μH[0] {x}

Tactic:
· let r : ℕ → ℝ≥0∞ := fun _ => 0
    let t : ℕ → Unit → Set X := fun _ _ => {x}
    have ht : ∀ᶠ n in atTop, ∀ i, ediam (t n i) ≤ r n := by
      simp only [t, r, imp_true_iff, ediam_singleton, eventually_atTop,
        nonpos_iff_eq_zero, exists_const]
    simpa [t, liminf_const] using hausdorffMeasure_le_liminf_sum 0 {x} r tendsto_const_nhds t ht

Goal state after:
case a
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
x : X
⊢ 1 ≤ μH[0] {x}
Module: Mathlib.Analysis.InnerProductSpace.NormDet

Goal state before:
pp: case pos
U : Type u_5
V : Type u_6
inst✝⁸ : NormedAddCommGroup U
inst✝⁷ : InnerProductSpace ℝ U
inst✝⁶ : FiniteDimensional ℝ U
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MeasurableSpace U
inst✝² : BorelSpace U
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
f : U →ₗ[ℝ] V
s : Set U
h : f.ker = ⊥
hrank : finrank ℝ ↥f.range = finrank ℝ U
bv : OrthonormalBasis (Fin (finrank ℝ U)) ℝ ↥f.range
g : U ≃ₗᵢ[ℝ] ↥f.range := (stdOrthonormalBasis ℝ U).equiv bv (Equiv.refl (Fin (finrank ℝ U)))
⊢ ENNReal.ofReal (g.symm.toLinearIsometry.normDet * f.rangeRestrict.normDet) * μH[↑(finrank ℝ U)] s =
    ENNReal.ofReal f.normDet * μH[↑(finrank ℝ U)] s

Tactic:
g.symm.toLinearIsometry.normDet_eq_one

Goal state after:
case pos
U : Type u_5
V : Type u_6
inst✝⁸ : NormedAddCommGroup U
inst✝⁷ : InnerProductSpace ℝ U
inst✝⁶ : FiniteDimensional ℝ U
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MeasurableSpace U
inst✝² : BorelSpace U
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
f : U →ₗ[ℝ] V
s : Set U
h : f.ker = ⊥
hrank : finrank ℝ ↥f.range = finrank ℝ U
bv : OrthonormalBasis (Fin (finrank ℝ U)) ℝ ↥f.range
g : U ≃ₗᵢ[ℝ] ↥f.range := (stdOrthonormalBasis ℝ U).equiv bv (Equiv.refl (Fin (finrank ℝ U)))
⊢ ENNReal.ofReal (1 * f.rangeRestrict.normDet) * μH[↑(finrank ℝ U)] s = ENNReal.ofReal f.normDet * μH[↑(finrank ℝ U)] s
Module: Mathlib.Analysis.InnerProductSpace.StandardSubspace

Goal state before:
pp: case mpr
H : Type u_1
inst✝ : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
x : H
S : ClosedSubmodule ℝ H
⊢ (∀ y ∈ S, ⟪y, x⟫.im = 0) → ∀ (u : H), -(I • u) ∈ S → inner ℝ u x = 0

Tactic:
· intro h _ hy
    have hiy := h _ hy
    simpa [inner_smul_left] using! hiy

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: ι : Type u_4
inst✝ : Fintype ι
a b : ι → ℚ
H : ∀ (i : ι), a i < b i
I : ∀ (i : ι), 0 ≤ ↑(b i) - ↑(a i)
γ : ℕ → Type u_4 := fun n ↦ (i : ι) → Fin ⌈(↑(b i) - ↑(a i)) * ↑n⌉₊
t : (n : ℕ) → γ n → Set (ι → ℝ) := fun n f ↦ univ.pi fun i ↦ Icc (↑(a i) + ↑↑(f i) / ↑n) (↑(a i) + (↑↑(f i) + 1) / ↑n)
A : Tendsto (fun n ↦ 1 / ↑n) atTop (𝓝 0)
B : ∀ᶠ (n : ℕ) in atTop, ∀ (i : γ n), ediam (t n i) ≤ 1 / ↑n
n : ℕ
hn : 1 ≤ n
npos : 0 < ↑n
⊢ (univ.pi fun i ↦ Ioo ↑(a i) ↑(b i)) ⊆ ⋃ i, t n i

Tactic:
intro x hx

Goal state after:
ι : Type u_4
inst✝ : Fintype ι
a b : ι → ℚ
H : ∀ (i : ι), a i < b i
I : ∀ (i : ι), 0 ≤ ↑(b i) - ↑(a i)
γ : ℕ → Type u_4 := fun n ↦ (i : ι) → Fin ⌈(↑(b i) - ↑(a i)) * ↑n⌉₊
t : (n : ℕ) → γ n → Set (ι → ℝ) := fun n f ↦ univ.pi fun i ↦ Icc (↑(a i) + ↑↑(f i) / ↑n) (↑(a i) + (↑↑(f i) + 1) / ↑n)
A : Tendsto (fun n ↦ 1 / ↑n) atTop (𝓝 0)
B : ∀ᶠ (n : ℕ) in atTop, ∀ (i : γ n), ediam (t n i) ≤ 1 / ↑n
n : ℕ
hn : 1 ≤ n
npos : 0 < ↑n
x : ι → ℝ
hx : x ∈ univ.pi fun i ↦ Ioo ↑(a i) ↑(b i)
⊢ x ∈ ⋃ i, t n i
Module: Mathlib.Analysis.LocallyConvex.ContinuousOfBounded

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : IsTopologicalAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : Module 𝕜 E
inst✝⁴ : ContinuousSMul 𝕜 E
inst✝³ : NormedField 𝕜'
inst✝² : Module 𝕜' F
σ : 𝕜 →+* 𝕜'
inst✝¹ : RingHomIsometric σ
inst✝ : IsTopologicalAddGroup F
f : E →ₛₗ[σ] F
U : Set F
hU : U ∈ 𝓝 0
V : Set E
hV : V ∈ 𝓝 0
h✝ : IsVonNBounded 𝕜' (⇑f '' V)
r : ℝ
hr : r > 0
x : 𝕜
h : ⇑f '' V ⊆ σ x • U
hx : r < ‖x‖
x_ne : x ≠ 0
⊢ x⁻¹ • x • ⇑f ⁻¹' U = ⇑f ⁻¹' U

Tactic:
inv_smul_smul₀ x_ne _

Goal state after:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : IsTopologicalAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : Module 𝕜 E
inst✝⁴ : ContinuousSMul 𝕜 E
inst✝³ : NormedField 𝕜'
inst✝² : Module 𝕜' F
σ : 𝕜 →+* 𝕜'
inst✝¹ : RingHomIsometric σ
inst✝ : IsTopologicalAddGroup F
f : E →ₛₗ[σ] F
U : Set F
hU : U ∈ 𝓝 0
V : Set E
hV : V ∈ 𝓝 0
h✝ : IsVonNBounded 𝕜' (⇑f '' V)
r : ℝ
hr : r > 0
x : 𝕜
h : ⇑f '' V ⊆ σ x • U
hx : r < ‖x‖
x_ne : x ≠ 0
⊢ ⇑f ⁻¹' U = ⇑f ⁻¹' U
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: 𝕜 : Type u_4
E : Type u_5
P : Type u_6
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : MeasurableSpace P
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor E P
inst✝ : BorelSpace P
d : ℝ
hd : 0 ≤ d
x : P
c : 𝕜
hc : c ≠ 0
s : Set P
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
⊢ μH[d] (c • ⇑(IsometryEquiv.vaddConst x).symm '' s) = ‖c‖₊ ^ d • μH[d] s

Tactic:
Measure.hausdorffMeasure_smul₀ hd hc,

Goal state after:
𝕜 : Type u_4
E : Type u_5
P : Type u_6
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : MeasurableSpace P
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor E P
inst✝ : BorelSpace P
d : ℝ
hd : 0 ≤ d
x : P
c : 𝕜
hc : c ≠ 0
s : Set P
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
⊢ ‖c‖₊ ^ d • μH[d] (⇑(IsometryEquiv.vaddConst x).symm '' s) = ‖c‖₊ ^ d • μH[d] s