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)
hfrob : map (Int.castRingHom (ZMod p)) Q ^ p = map (Int.castRingHom (ZMod p)) ((expand ℤ p) Q)
⊢ map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) ∣ map (Int.castRingHom (ZMod p)) Q ^ p

Tactic:
rw [hfrob]

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
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hfrob : map (Int.castRingHom (ZMod p)) Q ^ p = map (Int.castRingHom (ZMod p)) ((expand ℤ p) Q)
⊢ map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) ∣ map (Int.castRingHom (ZMod p)) ((expand ℤ p) Q)
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: case h
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∣ n ∧ d < n
⊢ X ^ n - 1 = (X ^ d - 1) * cyclotomic n R * ∏ x ∈ n.properDivisors \ d.divisors, cyclotomic x R

Tactic:
rw [← X_pow_sub_one_mul_prod_cyclotomic_eq_X_pow_sub_one_of_dvd R h.1 h.2.ne_bot,
    ← Nat.insert_self_properDivisors, Finset.insert_sdiff_of_notMem,
    Finset.prod_insert, mul_assoc]

Goal state after:
case h
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∣ n ∧ d < n
⊢ n ∉ n.properDivisors \ d.divisors

case h.h
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∣ n ∧ d < n
⊢ n ∉ d.divisors

case h
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∣ n ∧ d < n
⊢ n ≠ 0
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots

Goal state before:
pp: n : ℕ
h : 0 < n
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
⊢ (X ^ n - 1).IsRoot ζ ↔ ∃ i ∈ n.divisors, (cyclotomic i R).IsRoot ζ

Tactic:
←
      prod_cyclotomic_eq_X_pow_sub_one h,

Goal state after:
n : ℕ
h : 0 < n
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
⊢ (∏ i ∈ n.divisors, cyclotomic i R).IsRoot ζ ↔ ∃ i ∈ n.divisors, (cyclotomic i R).IsRoot ζ
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: n : ℕ
K : Type u_2
inst✝ : Field K
ζ x y : K
hpos : 0 < n
h : IsPrimitiveRoot ζ n
⊢ x ^ n - y ^ n = ∏ ζ ∈ nthRootsFinset n 1, (x - ζ * y)

Tactic:
by_cases hy : y = 0
  · simp only [hy, zero_pow (Nat.ne_zero_of_lt hpos), sub_zero, mul_zero, prod_const]
    congr
    rw [h.card_nthRootsFinset]
  convert!
    congr_arg (eval (x / y) · * y ^ card (nthRootsFinset n (1 : K))) <|
      X_pow_sub_one_eq_prod hpos h using 1
  · simp [sub_mul, div_pow, hy, h.card_nthRootsFinset]
  · simp [eval_prod, prod_mul_pow_card, sub_mul, hy]

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

Goal state before:
pp: case h.inl.hb.inr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, 2 < m → 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
i : ℕ
hi : i ≠ 1 ∧ i ∣ n ∧ i < n
hx : 0 < x + 1
⊢ 0 ≤ eval x (cyclotomic i R)

Tactic:
rcases eq_or_ne i 2 with (rfl | hk)
      · simpa only [eval_X, eval_one, cyclotomic_two, eval_add] using hx.le
      refine (ih _ hi.2.2 (Nat.two_lt_of_ne ?_ hi.1 hk)).le
      rintro rfl
      exact hn'.ne' <| zero_dvd_iff.mp hi.2.1

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

Goal state before:
pp: S T : Set ℕ
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : IsCyclotomicExtension T A B
hS : S ⊆ T
⊢ IsCyclotomicExtension S A ↥(adjoin A {b | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1})

Tactic:
refine ⟨fun {n} hn hn' => ?_, fun b => ?_⟩
  · obtain ⟨b, hb⟩ := ((isCyclotomicExtension_iff _ _ _).1 h).1 (hS hn) hn'
    refine ⟨⟨b, subset_adjoin ⟨n, hn, hn', hb.pow_eq_one⟩⟩, ?_⟩
    rwa [← IsPrimitiveRoot.coe_submonoidClass_iff, Subtype.coe_mk]
  · convert! mem_top (R := A) (x := b)
    rw [← adjoin_adjoin_coe_preimage, preimage_ofPred_eq]
    norm_cast

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

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Finite L
inst✝ : Algebra K L
x : L
⊢ (algebraMap K L) ((Algebra.trace K L) x) = ∑ i ∈ Finset.range (Module.finrank K L), x ^ Nat.card K ^ i

Tactic:
have := Finite.of_injective _ (FaithfulSMul.algebraMap_injective K L)
  have := ofFinite K
  rw [trace_eq_sum_automorphisms, Finset.sum_range]
  exact Eq.symm <| sum_bijective _ (bijective_frobeniusAlgEquivOfAlgebraic_pow K L) _ _ <|
    fun i ↦ by rw [AlgEquiv.coe_pow, coe_frobeniusAlgEquivOfAlgebraic_iterate, card_eq_nat_card]

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

Goal state before:
pp: p : ℕ
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
k : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)
s : ℕ
hs : s ≤ k
hodd : p ≠ 2
h : p ^ (k - s + 1) = 2 ^ 1
⊢ False

Tactic:
replace h :=
    eq_of_prime_pow_eq (prime_iff.1 hpri.out) (prime_iff.1 Nat.prime_two) (k - s).succ_pos h

Goal state after:
p : ℕ
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
k : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)
s : ℕ
hs : s ≤ k
hodd : p ≠ 2
h : p = 2
⊢ False
Module: Mathlib.Data.ZMod.Units

Goal state before:
pp: case neg
n : ℕ
x : ℤ
h : IsCoprime x ↑n
hn : ¬n = 0
this : NeZero n
⊢ (↑x).val.Coprime n

Tactic:
rwa [Int.isCoprime_iff_gcd_eq_one, ← Int.gcd_emod, ← val_intCast] at h

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

Goal state before:
pp: C : Type v
inst✝¹ : CommMonoid C
n : ℕ
inst✝ : NeZero n
ψ : AddChar (ZMod n) C
hψ : ψ.IsPrimitive
a : ZMod n
h : ψ a = 1
⊢ ¬ψ.mulShift a ≠ 1

Tactic:
zmod_char_ne_one_iff n (mulShift ψ a),

Goal state after:
C : Type v
inst✝¹ : CommMonoid C
n : ℕ
inst✝ : NeZero n
ψ : AddChar (ZMod n) C
hψ : ψ.IsPrimitive
a : ZMod n
h : ψ a = 1
⊢ ¬(ψ.mulShift a) 1 ≠ 1
Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
⊢ stdAddChar.IsPrimitive

Tactic:
refine AddChar.zmod_char_primitive_of_eq_one_only_at_zero _ _ (fun t ht ↦ ?_)
  rwa [← (stdAddChar (N := N)).map_zero_eq_one, injective_stdAddChar.eq_iff] at ht

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
d : ℕ
inst✝ : NeZero n
hd : d ∣ n
x✝ : χ.FactorsThrough d
x : (ZMod n)ˣ
hx : x ∈ (ZMod.unitsMap hd).ker
w✝ : d ∣ n
χ₀ : DirichletCharacter R d
hχ₀ : χ = (changeLevel w✝) χ₀
⊢ x ∈ (toUnitHom χ).ker

pp: case refine_2
R : Type u_1
inst✝¹ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
d : ℕ
inst✝ : NeZero n
hd : d ∣ n
h : (ZMod.unitsMap hd).ker ≤ (toUnitHom χ).ker
⊢ χ.FactorsThrough d

Tactic:
· rw [MonoidHom.mem_ker, hχ₀, changeLevel_toUnitHom, MonoidHom.comp_apply, hx, map_one]

Goal state after:
case refine_2
R : Type u_1
inst✝¹ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
d : ℕ
inst✝ : NeZero n
hd : d ∣ n
h : (ZMod.unitsMap hd).ker ≤ (toUnitHom χ).ker
⊢ χ.FactorsThrough d
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoid M
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : Finite Mˣ
χ : MulChar M R
⊢ 0 < orderOf χ

Tactic:
by
  cases nonempty_fintype Mˣ
  apply IsOfFinOrder.orderOf_pos
  exact isOfFinOrder_iff_pow_eq_one.2 ⟨_, Fintype.card_pos, χ.pow_card_eq_one⟩

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

Goal state before:
pp: R : Type u_1
inst✝² : CommMonoidWithZero R
n : ℕ
inst✝¹ : Nontrivial R
m : ℕ
inst✝ : NeZero m
hm : n ∣ m
χ : DirichletCharacter R n
a : ℤ
ha : IsCoprime a ↑χ.conductor
this✝ : (changeLevel ⋯) ((changeLevel hm) χ).primitiveCharacter = χ.primitiveCharacter
this : ((changeLevel ⋯) ((changeLevel hm) χ).primitiveCharacter) ↑a = χ.primitiveCharacter ↑a
⊢ ((changeLevel hm) χ).primitiveCharacter ↑a = χ.primitiveCharacter ↑a

Tactic:
rwa [changeLevel_eq_cast_of_dvd' _ _ ha] at this

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

Goal state before:
pp: case inr
R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ ψ : DirichletCharacter R n
hn : NeZero n
h : χ.conductor.lcm ψ.conductor ∣ n
⊢ χ * ψ = (changeLevel h) (χ.primitiveCharacter.mul ψ.primitiveCharacter)

Tactic:
rw [mul, MonoidHom.map_mul, ← changeLevel_trans, ← changeLevel_trans,
    changeLevel_primitiveCharacter, changeLevel_primitiveCharacter]

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

Goal state before:
pp: N : ℕ
inst✝² : NeZero N
R : Type u_1
inst✝¹ : CommRing R
e : AddChar (ZMod N) R
inst✝ : IsDomain R
χ : DirichletCharacter R N
d : ℕ
hd : d ∣ N
he : e.mulShift ↑d = 1
h_ne : gaussSum χ e ≠ 0
⊢ χ.FactorsThrough d

Tactic:
DirichletCharacter.factorsThrough_iff_ker_unitsMap hd

Goal state after:
N : ℕ
inst✝² : NeZero N
R : Type u_1
inst✝¹ : CommRing R
e : AddChar (ZMod N) R
inst✝ : IsDomain R
χ : DirichletCharacter R N
d : ℕ
hd : d ∣ N
he : e.mulShift ↑d = 1
h_ne : gaussSum χ e ≠ 0
⊢ (ZMod.unitsMap hd).ker ≤ (MulChar.toUnitHom χ).ker
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: R : Type u_1
R' : Type u_2
inst✝³ : Field R
inst✝² : Fintype R
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
ψ : AddChar R R'
hψ : ψ ≠ 1
⊢ gaussSum 1 ψ = -1

Tactic:
simp only [gaussSum, ← add_eq_zero_iff_eq_neg]
  calc ∑ a, (1 : MulChar R R') a * ψ a + 1
  _ = ∑ a ∈ {0}ᶜ, (1 : MulChar R R') a * ψ a + 1 := by
    simp [← ({0} : Finset R).sum_compl_add_sum]
  _ = ∑ a ∈ {0}ᶜ, ψ a + ψ 0 := by
    congr! <;> aesop (add simp MulChar.one_apply)
  _ = 0 := by
    rw [← AddChar.sum_eq_zero_of_ne_one hψ, ← Finset.sum_compl_add_sum (s := {0})]
    simp

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'
p : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit ↑p
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
⊢ gaussSum (χ ^ p) (ψ ^ p) = χ ↑p * gaussSum χ ψ

Tactic:
pow_mulShift,

Goal state after:
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
p : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit ↑p
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
⊢ gaussSum (χ ^ p) (ψ.mulShift ↑p) = χ ↑p * gaussSum χ ψ
Module: Mathlib.Order.Grade

Goal state before:
pp: 𝕆 : Type u_1
ℙ : Type u_2
α : Type u_3
β : Type u_4
inst✝⁴ : Preorder 𝕆
inst✝³ : Preorder ℙ
inst✝² : Preorder α
inst✝¹ : Preorder β
n : ℕ
inst✝ : GradeMinOrder (Fin n) α
a : Fin n
h : IsMin a
⊢ IsMin ↑a

Tactic:
cases n

Goal state after:
case zero
𝕆 : Type u_1
ℙ : Type u_2
α : Type u_3
β : Type u_4
inst✝⁴ : Preorder 𝕆
inst✝³ : Preorder ℙ
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : GradeMinOrder (Fin 0) α
a : Fin 0
h : IsMin a
⊢ IsMin ↑a

case succ
𝕆 : Type u_1
ℙ : Type u_2
α : Type u_3
β : Type u_4
inst✝⁴ : Preorder 𝕆
inst✝³ : Preorder ℙ
inst✝² : Preorder α
inst✝¹ : Preorder β
n✝ : ℕ
inst✝ : GradeMinOrder (Fin (n✝ + 1)) α
a : Fin (n✝ + 1)
h : IsMin a
⊢ IsMin ↑a
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: ι : Type u_1
A : ι → Type u_2
inst✝² : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst✝¹ : DecidableEq ι
p : ℝ
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
s : Finset ι
hp : ↑(#s) * p ≤ 1
i : ι
hi : i ∉ s
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
⊢ Measurable (f ^ (1 - ↑(#s) * p) * ∏ j ∈ insert i s, (∫⋯∫⁻_{j}, f ∂μ) ^ p)

Tactic:
change Measurable (fun x ↦ _)

Goal state after:
ι : Type u_1
A : ι → Type u_2
inst✝² : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst✝¹ : DecidableEq ι
p : ℝ
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
s : Finset ι
hp : ↑(#s) * p ≤ 1
i : ι
hi : i ∉ s
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
⊢ Measurable fun x ↦ (f ^ (1 - ↑(#s) * p) * ∏ j ∈ insert i s, (∫⋯∫⁻_{j}, f ∂μ) ^ p) x
Module: Mathlib.Analysis.InnerProductSpace.Semisimple

Goal state before:
pp: case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : Module.End 𝕜 E
hT : IsSymmetric T
p : Submodule 𝕜 E
hp₁ : p ∈ T.invtSubmodule
hp₂ : Module.Finite 𝕜 ↥p
q : Submodule 𝕜 E
hq₁ : q ∈ T.invtSubmodule
hq₂ : q ≤ p
⊢ qᗮ ∈ T.invtSubmodule

Tactic:
exact orthogonalComplement_mem_invtSubmodule hT hq₁

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
S : F →ₗ.[𝕜] E
inst✝ : CompleteSpace E
hT : Dense ↑T.domain
h : T.IsFormalAdjoint S
x✝² : ↥S.domain
x✝¹ : ↥T†.domain
hxy : ↑x✝² = ↑x✝¹
x✝ : ↥T.domain
⊢ ⟪↑S x✝², ↑x✝⟫ = ⟪↑x✝¹, ↑T x✝⟫

Tactic:
h.symm,

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
S : F →ₗ.[𝕜] E
inst✝ : CompleteSpace E
hT : Dense ↑T.domain
h : T.IsFormalAdjoint S
x✝² : ↥S.domain
x✝¹ : ↥T†.domain
hxy : ↑x✝² = ↑x✝¹
x✝ : ↥T.domain
⊢ ⟪↑x✝², ↑T x✝⟫ = ⟪↑x✝¹, ↑T x✝⟫
Module: Mathlib.Analysis.InnerProductSpace.LinearPMap

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
A : E →L[𝕜] F
p : Submodule 𝕜 E
hp : Dense ↑p
⊢ ((↑A).toPMap p)† = (↑(adjoint A)).toPMap ⊤

Tactic:
ext x y hxy
  · simp only [LinearMap.toPMap_domain, Submodule.mem_top, iff_true,
      LinearPMap.mem_adjoint_domain_iff]
    exact ((innerSL 𝕜 x).comp <| A.comp <| Submodule.subtypeL _).cont
  refine LinearPMap.adjoint_apply_eq hp _ fun v => ?_
  simp only [adjoint_inner_left, LinearMap.toPMap_apply, coe_coe]

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 : A† = A
h : ¬Dense ↑A.domain
x : E
⊢ x ∈ A†.domain

Tactic:
rw [mem_adjoint_domain_iff, ← 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
x : E
⊢ Continuous ⇑((innerₛₗ 𝕜) x ∘ₗ A†.toFun)
Module: Mathlib.Analysis.InnerProductSpace.LinearPMap

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
g : Submodule 𝕜 (E × F)
x : F × E
⊢ x ∈ g.adjoint ↔ ∀ (a : E) (b : F), (a, b) ∈ g → ⟪b, x.1⟫ - ⟪a, x.2⟫ = 0

Tactic:
by
  simp only [Submodule.adjoint, mem_map, mem_orthogonal, LinearEquiv.coe_coe,
    LinearEquiv.trans_apply, LinearEquiv.skewSwap_symm_apply, coe_symm_linearEquiv, Prod.exists,
    prod_inner_apply, ofLp_fst, ofLp_snd, forall_exists_index, and_imp, coe_linearEquiv]
  constructor
  · rintro ⟨y, h1, h2⟩ a b hab
    rw [← h2, WithLp.ofLp_fst, WithLp.ofLp_snd]
    specialize h1 (toLp 2 (b, -a)) a b hab rfl
    dsimp at h1
    simp only [inner_neg_left, ← sub_eq_add_neg] at h1
    exact h1
  · intro h
    refine ⟨toLp 2 x, ?_, rfl⟩
    intro u a b hab hu
    simp [← hu, ← sub_eq_add_neg, h a b hab]

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
i : Fin (finrank 𝕜 E)
⊢ T.singularValues ↑i = √(⋯.eigenvalues ⋯ i)

Tactic:
exact Finsupp.embDomain_apply_self _ _ i

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
this : (adjoint T ∘ₗ T).ker = ⊥ ↔ ¬End.HasEigenvalue (adjoint T ∘ₗ T) 0
⊢ Function.Injective ⇑T ↔ ∀ i < finrank 𝕜 E, 0 < T.singularValues i

Tactic:
rw [← adjoint_comp_self_injective_iff, ← coe_comp, ← ker_eq_bot, ← not_iff_not, this.not_left]

Goal state after:
𝕜 : 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
this : (adjoint T ∘ₗ T).ker = ⊥ ↔ ¬End.HasEigenvalue (adjoint T ∘ₗ T) 0
⊢ End.HasEigenvalue (adjoint T ∘ₗ T) 0 ↔ ¬∀ i < finrank 𝕜 E, 0 < T.singularValues i
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
x : E ⊗[𝕜] G
⊢ ‖(LinearMap.rTensor G ↑f) x‖ ≤ ‖f‖ * ‖x‖

Tactic:
obtain ⟨n, e, g, hx⟩ := exists_sum_tmul_eq x
    obtain ⟨c, hc_supp, hc⟩ := Submodule.mem_span_set.mp
      ((span_tmul_eq_top 𝕜 E G) ▸ Submodule.mem_top (x := x))
    obtain ⟨m, A, hA⟩ := Matrix.posSemidef_iff_eq_sum_vecMulVec.mp
      (Matrix.posSemidef_opNorm_smul_gram_sub_gram e f)
    apply (sq_le_sq₀ (norm_nonneg _) (by positivity)).mp
    simp_rw [sub_eq_iff_eq_add', ← sub_eq_iff_eq_add, ← Matrix.ext_iff, Matrix.sub_apply,
      Matrix.smul_apply, Matrix.gram_apply, Function.comp_apply] at hA
    simp_rw [mul_pow, hx, map_sum, LinearMap.rTensor_tmul, coe_coe,
      ← inner_self_eq_norm_sq (𝕜 := 𝕜), inner_sum, sum_inner, inner_tmul, ← hA, sub_mul,
      Finset.sum_sub_distrib, map_sub, ← RCLike.smul_re, Finset.smul_sum, smul_mul_assoc,
      sub_le_self_iff, Matrix.sum_apply, mul_comm, Finset.mul_sum]
    simp_rw +singlePass [Finset.sum_comm_cycle, Matrix.vecMulVec, Matrix.of_apply, Pi.star_apply,
      ← mul_left_comm, ← mul_assoc, ← starRingEnd_self_apply (A _ _), ← inner_smul_left]
    simp [mul_comm, ← inner_smul_right, ← sum_inner, ← inner_sum, Finset.sum_nonneg]

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

Goal state before:
pp: F : Type u_3
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
E : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
inst✝ : FiniteDimensional ℝ F
u : E → F
s : Set E
hu : ContDiff ℝ 1 u
h2u : support u ⊆ s
p q : ℝ≥0
hp : 1 ≤ p
h2p : p < ↑(finrank ℝ E)
hpq : ↑p⁻¹ - (↑(finrank ℝ E))⁻¹ ≤ (↑q)⁻¹
hs : Bornology.IsBounded s
hq0 : ¬q = 0
p' : ℝ≥0 := (p⁻¹ - (↑(finrank ℝ E))⁻¹)⁻¹
hp' : ↑p'⁻¹ = ↑p⁻¹ - (↑(finrank ℝ E))⁻¹
this : ↑q ≤ ↑p'
t : ℝ≥0 := (μ s).toNNReal ^ (1 / ↑q - 1 / ↑p')
C : ℝ≥0 := SNormLESNormFDerivOfEqConst F μ ↑p
⊢ eLpNorm u (↑p') μ * ↑t ≤ ↑C * eLpNorm (fderiv ℝ u) (↑p) μ * ↑t

Tactic:
by
        have h2u' : HasCompactSupport u := by
          apply HasCompactSupport.of_support_subset_isCompact hs.isCompact_closure
          exact h2u.trans subset_closure
        rel [eLpNorm_le_eLpNorm_fderiv_of_eq μ hu h2u' hp (mod_cast h2p.pos) hp']

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
d₁ d₂ : ℕ
h : d₁ < d₂
s : Set X
⊢ (volume.addHaarScalarFactor μH[↑d₂] • μH[↑d₂]) s = 0 ∨ (volume.addHaarScalarFactor μH[↑d₁] • μH[↑d₁]) s = ⊤

Tactic:
obtain h | h := hausdorffMeasure_zero_or_top (show (d₁ : ℝ) < d₂ by simpa using h) s

Goal state after:
case inl
X : Type u_1
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
d₁ d₂ : ℕ
h✝ : d₁ < d₂
s : Set X
h : μH[↑d₂] s = 0
⊢ (volume.addHaarScalarFactor μH[↑d₂] • μH[↑d₂]) s = 0 ∨ (volume.addHaarScalarFactor μH[↑d₁] • μH[↑d₁]) s = ⊤

case inr
X : Type u_1
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
d₁ d₂ : ℕ
h✝ : d₁ < d₂
s : Set X
h : μH[↑d₁] s = ⊤
⊢ (volume.addHaarScalarFactor μH[↑d₂] • μH[↑d₂]) s = 0 ∨ (volume.addHaarScalarFactor μH[↑d₁] • μH[↑d₁]) s = ⊤
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
h : map ⇑(IsometryEquiv.vaddConst p) μHE[finrank ℝ V] = μHE[finrank ℝ V]
⊢ μHE[finrank ℝ V] = map (⇑(IsometryEquiv.vaddConst p)) volume

Tactic:
rw [InnerProductSpace.euclideanHausdorffMeasure_eq_volume] at h

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
p : P
h : map (⇑(IsometryEquiv.vaddConst p)) volume = μHE[finrank ℝ V]
⊢ μHE[finrank ℝ V] = map (⇑(IsometryEquiv.vaddConst p)) volume
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
f : U →ₗ[𝕜] V
⊢ [f.normDet ≠ 0, f.ker = ⊥, finrank 𝕜 ↥f.range = finrank 𝕜 U,
      Nonempty (OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥f.range), Function.Injective ⇑f].TFAE

Tactic:
tfae_have 1 ↔ 2 := f.normDet_eq_zero_iff_ker_ne_bot.not_left

Goal state after:
𝕜 : 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
f : U →ₗ[𝕜] V
tfae_1_iff_2 : f.normDet ≠ 0 ↔ f.ker = ⊥
⊢ [f.normDet ≠ 0, f.ker = ⊥, finrank 𝕜 ↥f.range = finrank 𝕜 U,
      Nonempty (OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥f.range), Function.Injective ⇑f].TFAE
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
inst✝ : SecondCountableTopology X
r : ℝ≥0
f : X → Y
hr : 0 < r
hf : ∀ (x : X), ∃ C, ∃ s ∈ 𝓝 x, HolderOnWith C r f s
x : X
x✝ : x ∈ univ
⊢ ∃ C, ∃ t ∈ 𝓝[univ] x, HolderOnWith C r f t

Tactic:
simpa only [exists_prop, nhdsWithin_univ] using hf x

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

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
inst✝ : SecondCountableTopology X
f : X → Y
hf : ∀ (x : X), ∃ C, ∃ s ∈ 𝓝 x, LipschitzOnWith C f s
x : X
x✝ : x ∈ univ
⊢ ∃ C, ∃ t ∈ 𝓝[univ] x, LipschitzOnWith C f t

Tactic:
simpa only [exists_prop, nhdsWithin_univ] using hf x

Goal state after: