mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.Galois.Abelian

Goal state before:
pp: K : Type u_1
L : Type u_2
M : Type u_3
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
inst✝⁴ : Field M
inst✝³ : Algebra K M
inst✝² : Algebra L M
inst✝¹ : IsScalarTower K L M
inst✝ : IsAbelianGalois K M
this : IsGalois K L
x y : Gal(L/K)
⊢ x * y = y * x

Tactic:
obtain ⟨x, rfl⟩ := AlgEquiv.restrictNormalHom_surjective M x
      obtain ⟨y, rfl⟩ := AlgEquiv.restrictNormalHom_surjective M y
      rw [← map_mul, ← map_mul, mul_comm]

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

Goal state before:
pp: G : Type u_7
G' : Type u_8
inst✝³ : Group G
inst✝² : IsCyclic G
inst✝¹ : Finite G
inst✝ : CommGroup G'
hG' : ∃ ζ, IsPrimitiveRoot ζ (Nat.card G)
a : G
ha : a ≠ 1
⊢ ∃ φ, φ a ≠ 1

Tactic:
let inst : Fintype G := Fintype.ofFinite _
  obtain ⟨ζ, hζ⟩ := hG'
  -- pick a generator `g` of `G`
  obtain ⟨g, hg⟩ := IsCyclic.exists_generator (α := G)
  have hζg : orderOf ζ ∣ orderOf g := by
    rw [← hζ.eq_orderOf, orderOf_eq_card_of_forall_mem_zpowers hg, Nat.card_eq_fintype_card]
  -- use the homomorphism `φ` given by `g ↦ ζ`
  let φ := monoidHomOfForallMemZpowers hg hζg
  have hφg : IsPrimitiveRoot (φ g) (Nat.card G) := by
    rwa [monoidHomOfForallMemZpowers_apply_gen hg hζg]
  use φ
  contrapose ha
  specialize hg a
  rw [← mem_powers_iff_mem_zpowers, Submonoid.mem_powers_iff] at hg
  obtain ⟨k, hk⟩ := hg
  rw [← hk, map_pow] at ha
  obtain ⟨l, rfl⟩ := (hφg.pow_eq_one_iff_dvd k).mp ha
  rw [← hk, pow_mul, Nat.card_eq_fintype_card, pow_card_eq_one, one_pow]

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

Goal state before:
pp: n : ℕ
hn : 2 < n
R : Type u_1
inst✝² : CommRing R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
this✝ : NeZero n
this : 0 < eval (↑(-1)) (cyclotomic n ℝ)
⊢ 0 < eval (↑(-1)) (cyclotomic n ℤ)

Tactic:
by
    rw [← map_cyclotomic_int n ℝ, eval_intCast_map, Int.coe_castRingHom] at this
    simpa only [Int.cast_pos] using this

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 s : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)
hs : s ≤ k
htwo : p ^ (k - s + 1) ≠ 2
hirr₁ : Irreducible (cyclotomic (p ^ (k - s + 1)) K)
η : L := ζ ^ p ^ s - 1
η₁ : ↥K⟮η⟯ := IntermediateField.AdjoinSimple.gen K η
⊢ p ^ (k + 1) = p ^ (k + 1 - s + s)

Tactic:
Nat.sub_add_cancel (le_trans hs (Nat.le_succ k))

Goal state after:
p : ℕ
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)
hs : s ≤ k
htwo : p ^ (k - s + 1) ≠ 2
hirr₁ : Irreducible (cyclotomic (p ^ (k - s + 1)) K)
η : L := ζ ^ p ^ s - 1
η₁ : ↥K⟮η⟯ := IntermediateField.AdjoinSimple.gen K η
⊢ p ^ (k + 1) = p ^ k.succ
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: case refine_2
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
h : ζ.re ≤ 0 ∧ ζ.im = 0
hζ₀ : ζ ≠ 0
this : ζ.re < 0 ∧ ζ.im = 0
⊢ False

Tactic:
← Complex.arg_eq_pi_iff,

Goal state after:
case refine_2
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
h : ζ.re ≤ 0 ∧ ζ.im = 0
hζ₀ : ζ ≠ 0
this : ζ.arg = Real.pi
⊢ False
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case mem
S : Set ℕ
A : Type u
B : Type v
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : IsCyclotomicExtension S A B
inst✝ : IsDomain B
f g : B ≃ₐ[A] B
H : ∀ n ∈ S, n ≠ 0 → ∃ r, IsPrimitiveRoot r n ∧ f r = g r
x y : B
n : ℕ
hn : n ∈ S
h1 : n ≠ 0
h2 : y ^ n = 1
r : B
hr1 : IsPrimitiveRoot r n
hr2 : f r = g r
⊢ f y = g y

Tactic:
have := NeZero.mk h1

Goal state after:
case mem
S : Set ℕ
A : Type u
B : Type v
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : IsCyclotomicExtension S A B
inst✝ : IsDomain B
f g : B ≃ₐ[A] B
H : ∀ n ∈ S, n ≠ 0 → ∃ r, IsPrimitiveRoot r n ∧ f r = g r
x y : B
n : ℕ
hn : n ∈ S
h1 : n ≠ 0
h2 : y ^ n = 1
r : B
hr1 : IsPrimitiveRoot r n
hr2 : f r = g r
this : NeZero n
⊢ f y = g y
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case right
S : Set ℕ
A : Type u
B : Type v
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : IsCyclotomicExtension S A B
inst✝ : IsDomain B
f g : B ≃ₐ[A] B
n : ℕ
hn : n ∈ S
h1 : n ≠ 0
r : B
hr : IsPrimitiveRoot r n
⊢ f (g r) = g (f r)

Tactic:
have := NeZero.mk h1

Goal state after:
case right
S : Set ℕ
A : Type u
B : Type v
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : IsCyclotomicExtension S A B
inst✝ : IsDomain B
f g : B ≃ₐ[A] B
n : ℕ
hn : n ∈ S
h1 : n ≠ 0
r : B
hr : IsPrimitiveRoot r n
this : NeZero n
⊢ f (g r) = g (f r)
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: A : Type u
B : Type v
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
n : ℕ
inst✝¹ : NeZero n
inst✝ : IsDomain B
ζ : B
hζ : IsPrimitiveRoot ζ n
⊢ adjoin A ((cyclotomic n A).rootSet B) = A[ζ]

Tactic:
refine le_antisymm (adjoin_le fun x hx => ?_) (adjoin_mono fun x hx => ?_)

Goal state after:
case refine_1
A : Type u
B : Type v
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
n : ℕ
inst✝¹ : NeZero n
inst✝ : IsDomain B
ζ : B
hζ : IsPrimitiveRoot ζ n
x : B
hx : x ∈ (cyclotomic n A).rootSet B
⊢ x ∈ ↑A[ζ]

case refine_2
A : Type u
B : Type v
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
n : ℕ
inst✝¹ : NeZero n
inst✝ : IsDomain B
ζ : B
hζ : IsPrimitiveRoot ζ n
x : B
hx : x ∈ {ζ}
⊢ x ∈ (cyclotomic n A).rootSet B
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: S : Set ℕ
K : Type w
L : Type z
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension S K L
this : Algebra.IsIntegral K L
h : (IntermediateField.adjoin K {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}).toSubalgebra = ⊤.toSubalgebra
b : L
n : ℕ
hn : n ∈ S
h1 : n ≠ 0
h2 : b ^ n = 1
⊢ IsSeparable K b

Tactic:
have := NeZero.mk h1

Goal state after:
S : Set ℕ
K : Type w
L : Type z
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension S K L
this✝ : Algebra.IsIntegral K L
h : (IntermediateField.adjoin K {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}).toSubalgebra = ⊤.toSubalgebra
b : L
n : ℕ
hn : n ∈ S
h1 : n ≠ 0
h2 : b ^ n = 1
this : NeZero n
⊢ IsSeparable K b
Module: Mathlib.FieldTheory.Finite.GaloisField

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

Tactic:
simp only [aeval_X_pow, aeval_X, map_sub, mul_pow, sub_eq_zero]

Goal state after:
case succ.refine_6
n : ℕ
h : n ≠ 0
n✝ : ℕ
h_prime : Fact (Nat.Prime (n✝ + 1))
this : Fintype (GaloisField (n✝ + 1) n)
g_poly : (ZMod (n✝ + 1))[X] := X ^ (n✝ + 1) ^ n - X
hp : 1 < n✝ + 1
aux : X ^ (n✝ + 1) ^ n - X ≠ 0
key : Fintype.card ↑(g_poly.rootSet (GaloisField (n✝ + 1) n)) = (n✝ + 1) ^ n
nat_degree_eq : g_poly.natDegree = (n✝ + 1) ^ n
x : GaloisField (n✝ + 1) n
hx :
  x ∈
    Subring.closure
      (Set.range ⇑(algebraMap (ZMod (n✝ + 1)) (GaloisField (n✝ + 1) n)) ∪
        (X ^ (n✝ + 1) ^ n - X).rootSet (X ^ (n✝ + 1) ^ n - X).SplittingField)
⊢ ∀ (x y : GaloisField (n✝ + 1) n),
    x ∈
        Subring.closure
          (Set.range ⇑(algebraMap (ZMod (n✝ + 1)) (GaloisField (n✝ + 1) n)) ∪
            (X ^ (n✝ + 1) ^ n - X).rootSet (X ^ (n✝ + 1) ^ n - X).SplittingField) →
      y ∈
          Subring.closure
            (Set.range ⇑(algebraMap (ZMod (n✝ + 1)) (GaloisField (n✝ + 1) n)) ∪
              (X ^ (n✝ + 1) ^ n - X).rootSet (X ^ (n✝ + 1) ^ n - X).SplittingField) →
        x ^ (n✝ + 1) ^ n = x → y ^ (n✝ + 1) ^ n = y → x ^ (n✝ + 1) ^ n * y ^ (n✝ + 1) ^ n = x * y
Module: Mathlib.Data.ZMod.Units

Goal state before:
pp: m : ℕ
n : ℤ
h : IsUnit ↑n
⊢ IsUnit (↑n)⁻¹

Tactic:
by
  rw [isUnit_iff_exists]
  exact ⟨n, inv_mul_of_unit _ h, mul_inv_of_unit _ h⟩

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
x✝ : ↥(rootsOfUnity n ℂ)
w : ℂˣ
hw : w ∈ rootsOfUnity n ℂ
j : ℕ
hj1 : j < n
hj2 : cexp (2 * ↑π * I * (↑j / ↑n)) = ↑w
⊢ (⇑(rootsOfUnityCircleEquiv n) ∘ ⇑(ZMod.rootsOfUnityAddChar n)) ↑j = ⟨w, hw⟩

Tactic:
by simp [Units.ext_iff, Subtype.ext_iff, ← hj2, ZMod.toCircle_natCast, mul_div_assoc]

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

Goal state before:
pp: case succ
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
a : Rˣ
n : ℕ
ih : (χ ^ n) ↑a = χ ↑a ^ n
⊢ (χ ^ n) ↑a * χ ↑a = χ ↑a ^ n * χ ↑a

Tactic:
ih

Goal state after:
case succ
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
a : Rˣ
n : ℕ
ih : (χ ^ n) ↑a = χ ↑a ^ n
⊢ χ ↑a ^ n * χ ↑a = χ ↑a ^ n * χ ↑a
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
n : ℕ
a : Rˣ
⊢ (χ ^ n) ↑a = χ ↑a ^ n

Tactic:
by
  induction n with
  | zero => rw [pow_zero, pow_zero, one_apply_coe]
  | succ n ih => rw [pow_succ, pow_succ, mul_apply, ih]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ₁ χ₂ : MulChar R R'
a : Rˣ
⊢ ↑((equivToUnitHom (χ₁ * χ₂)) a) = ↑((equivToUnitHom χ₁) a) * ↑((equivToUnitHom χ₂) a)

Tactic:
coe_equivToUnitHom,

Goal state after:
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ₁ χ₂ : MulChar R R'
a : Rˣ
⊢ (χ₁ * χ₂) ↑a = χ₁ ↑a * χ₂ ↑a
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
inst✝ : NeZero n
hχ : χ.conductor = 1
h' : χ.conductor ∣ n
χ₀ : DirichletCharacter R χ.conductor
h : χ = (changeLevel h') χ₀
⊢ χ = 1

Tactic:
exact (level_one' χ₀ hχ ▸ h).trans <| changeLevel_one h'

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

Goal state before:
pp: R : Type u_1
inst✝² : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
inst✝¹ : NeZero n
inst✝ : Nontrivial R
p : ℕ
hp : Fact (Nat.Prime p)
⊢ χ ∈ subgroupOfPrimitiveMapToOne R n p ↔ χ.primitiveCharacter ↑p = 1

Tactic:
have : NeZero (n / p ^ n.factorization p) := ⟨(Nat.ordCompl_pos p (NeZero.ne n)).ne'⟩

Goal state after:
R : Type u_1
inst✝² : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
inst✝¹ : NeZero n
inst✝ : Nontrivial R
p : ℕ
hp : Fact (Nat.Prime p)
this : NeZero (n / p ^ n.factorization p)
⊢ χ ∈ subgroupOfPrimitiveMapToOne R n p ↔ χ.primitiveCharacter ↑p = 1
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'
H : ∀ (k : ℕ) (x' : X), d x' x ≤ 2 * ε ∧ 2 ^ k * ϕ x ≤ ϕ x' → ∃ y, d x' y ≤ ε / 2 ^ k ∧ 2 * ϕ x' < ϕ y
⊢ False

Tactic:
have : Nonempty X := ⟨x⟩

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'
H : ∀ (k : ℕ) (x' : X), d x' x ≤ 2 * ε ∧ 2 ^ k * ϕ x ≤ ϕ x' → ∃ y, d x' y ≤ ε / 2 ^ k ∧ 2 * ϕ x' < ϕ y
this : Nonempty X
⊢ False
Module: Mathlib.Analysis.InnerProductSpace.ExteriorPower

Goal state before:
pp: n : ℕ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x : Fin n → E
⊢ (innerProductForm ((ιMulti ℝ n) x)) ((ιMulti ℝ n) x) = (gram ℝ x).det

Tactic:
simp [gram, innerProductForm_ιMulti_ιMulti, real_inner_comm]

Goal state after:
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
T : E →L[𝕜] E
⊢ T.IsPositive ↔ IsSelfAdjoint T ∧ ∀ (x : E), 0 ≤ T.reApplyInnerSelf x

Tactic:
by
  simp [IsPositive, isSelfAdjoint_iff_isSymmetric, LinearMap.IsSymmetric]

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
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p : ℝ
hp✝ : (↑(finrank ℝ E)).HolderConjugate p
C : ℝ≥0 := lintegralPowLePowLIntegralFDerivConst μ p
ι : Type := Fin (finrank ℝ E)
hιcard : #ι = finrank ℝ E
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this
hp : (↑#ι).HolderConjugate p
h0p : 0 ≤ p
c : ℝ≥0 := μ.addHaarScalarFactor (Measure.map (⇑e.symm) volume)
hc : 0 < c
h2c : μ = c • Measure.map (⇑e.symm) volume
h3c : ↑c ≠ 0
h0C : C = c * ‖↑e.symm‖₊ ^ p * (c ^ p)⁻¹
hC : C * c ^ p = c * ‖↑e.symm‖₊ ^ p
v : (ι → ℝ) → F := u ∘ ⇑e.symm
hv : ContDiff ℝ 1 v
h2v : HasCompactSupport v
⊢ ↑(‖↑e.symm‖₊ ^ p) * (∫⁻ (y : ι → ℝ), ‖fderiv ℝ u (e.symm y)‖ₑ) ^ p =
    ↑(‖↑e.symm‖₊ ^ p) * (∫⁻ (x : E), ‖fderiv ℝ u x‖ₑ ∂Measure.map (⇑e.symm) volume) ^ p

Tactic:
by
        congr
        rw [lintegral_map _ e.symm.continuous.measurable]
        fun_prop

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

Goal state before:
pp: E : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
inst✝³ : FiniteDimensional ℝ E
μ : Measure E
inst✝² : μ.IsAddHaarMeasure
F' : Type u_5
inst✝¹ : NormedAddCommGroup F'
inst✝ : InnerProductSpace ℝ F'
u : E → F'
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p p' : ℝ≥0
hp : 1 ≤ p
hp'0 : ¬p' = 0
n : ℕ := finrank ℝ E
hn✝ : 0 < n
hp' : (↑p')⁻¹ = ↑p⁻¹ - (↑n)⁻¹
n' : ℝ≥0 := (↑n).conjExponent
h2p : ↑p < ↑n
h0n : 2 ≤ n
hn : (↑n).HolderConjugate n'
h1n : 1 ≤ ↑n
⊢ 1 < ↑n

Tactic:
exact hn.coe.lt

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

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
ι : Type u_6
ι' : Type u_7
inst✝¹ : Fintype ι
inst✝ : Fintype ι'
x : E ⊗[𝕜] F
e : OrthonormalBasis ι 𝕜 E
f : OrthonormalBasis ι' 𝕜 F
⊢ inner 𝕜 x x = ↑(∑ i, ‖((e.toBasis.tensorProduct f.toBasis).repr x) i‖ ^ 2)

Tactic:
have : x = ∑ i : ι, ∑ j : ι', (e.toBasis.tensorProduct f.toBasis).repr x (i, j) • e i ⊗ₜ f j := by
    conv_lhs => rw [← (e.toBasis.tensorProduct f.toBasis).sum_repr x]
    simp [← Finset.sum_product', Basis.tensorProduct_apply']
  conv_lhs => rw [this]
  simp only [inner_def, map_sum, LinearMap.sum_apply]
  simp [OrthonormalBasis.inner_eq_ite, ← Finset.sum_product', RCLike.mul_conj]

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

Goal state before:
pp: case neg
X : Type u_2
inst✝ : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
t : Set X
ht : t ∈ {s | IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s}
s : Set X
S : ℕ → Set X := fun n ↦ {x | x ∈ s ∧ (↑n)⁻¹ ≤ infEDist x t}
Ssep : ∀ (n : ℕ), AreSeparated (S n) t
Ssep' : ∀ (n : ℕ), AreSeparated (S n) (s ∩ t)
S_sub : ∀ (n : ℕ), S n ⊆ s \ t
hSs : ∀ (n : ℕ), μ (s ∩ t) + μ (S n) ≤ μ s
iUnion_S : ⋃ n, S n = s \ t
htop : ¬μ (s \ t) = ∞
r : ℕ
⊢ ⨆ i, ∑ a ∈ Finset.range i, μ (S (2 * a + 1 + r) \ S (2 * a + r)) ≤ μ (⋃ n, S n)

Tactic:
iSup_le_iff

Goal state after:
case neg
X : Type u_2
inst✝ : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
t : Set X
ht : t ∈ {s | IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s}
s : Set X
S : ℕ → Set X := fun n ↦ {x | x ∈ s ∧ (↑n)⁻¹ ≤ infEDist x t}
Ssep : ∀ (n : ℕ), AreSeparated (S n) t
Ssep' : ∀ (n : ℕ), AreSeparated (S n) (s ∩ t)
S_sub : ∀ (n : ℕ), S n ⊆ s \ t
hSs : ∀ (n : ℕ), μ (s ∩ t) + μ (S n) ≤ μ s
iUnion_S : ⋃ n, S n = s \ t
htop : ¬μ (s \ t) = ∞
r : ℕ
⊢ ∀ (i : ℕ), ∑ a ∈ Finset.range i, μ (S (2 * a + 1 + r) \ S (2 * a + r)) ≤ μ (⋃ n, S n)
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
s : Set X
d : ℝ≥0
h : μH[↑d] s = ∞
⊢ ↑d ≤ dimH s

Tactic:
dimH_def

Goal state after:
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
s : Set X
d : ℝ≥0
h : μH[↑d] s = ∞
⊢ ↑d ≤ ⨆ d, ⨆ (_ : μH[↑d] s = ∞), ↑d
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
s : Set X
d : ℝ≥0
h : dimH s < ↑d
⊢ μH[↑d] s = 0

Tactic:
dimH_def

Goal state after:
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
s : Set X
d : ℝ≥0
h : ⨆ d, ⨆ (_ : μH[↑d] s = ∞), ↑d < ↑d
⊢ μH[↑d] s = 0
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: case a
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
s : Set X
⊢ dimH s ≤ ⨅ d, ⨅ (_ : μH[↑d] s = 0), ↑d

Tactic:
dimH_def

Goal state after:
case a
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
s : Set X
⊢ ⨆ d, ⨆ (_ : μH[↑d] s = ∞), ↑d ≤ ⨅ d, ⨅ (_ : μH[↑d] s = 0), ↑d
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:
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.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: case neg
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
s : Set X
r : ℝ≥0∞
x✝ : r > 0
t : ℕ → Set X
ht : s ⊆ iUnion t
n : ℕ
hn : r < ediam (t n)
⊢ ⨆ (_ : (t n).Nonempty), ⨅ (_ : ediam (t n) ≤ r), m (ediam (t n)) = ∞

Tactic:
iSup_eq_if,

Goal state after:
case neg
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
s : Set X
r : ℝ≥0∞
x✝ : r > 0
t : ℕ → Set X
ht : s ⊆ iUnion t
n : ℕ
hn : r < ediam (t n)
⊢ (if (t n).Nonempty then ⨅ (_ : ediam (t n) ≤ r), m (ediam (t n)) else ⊥) = ∞
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
d₁ d₂ : ℝ
h : d₁ < d₂
s : Set X
H : μH[d₂] s ≠ 0 ∧ μH[d₁] s ≠ ∞
this : ∀ (c : ℝ≥0), c ≠ 0 → μH[d₂] s ≤ ↑c * μH[d₁] s
⊢ False

Tactic:
rcases ENNReal.exists_nnreal_pos_mul_lt H.2 H.1 with ⟨c, hc0, hc⟩
    exact hc.not_ge (this c (pos_iff_ne_zero.1 hc0))

Goal state after:
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 = ⊥
⊢ μH[↑(finrank ℝ U)] (⇑f '' s) = ENNReal.ofReal f.normDet * μH[↑(finrank ℝ U)] s

Tactic:
have hrank : finrank ℝ ↥f.range = finrank ℝ U := (f.normDet_ne_zero_tfae.out 1 2).mp h
    obtain ⟨bv⟩ := (f.normDet_ne_zero_tfae.out 1 3).mp h
    let g : U ≃ₗᵢ[ℝ] f.range := (stdOrthonormalBasis ℝ U).equiv bv (Equiv.refl _)
    suffices μH[finrank ℝ U] ((f.range.subtypeₗᵢ.comp g.toLinearIsometry) ''
        ((g.symm.toLinearIsometry.toLinearMap ∘ₗ f.rangeRestrict) '' s)) =
        ENNReal.ofReal f.normDet * μH[finrank ℝ U] s by
      simpa [Set.image_image]
    rw [(LinearIsometry.isometry _).hausdorffMeasure_image (by simp),
      addHaar_image_linearMap μH[finrank ℝ U], ← normDet_eq_abs_det,
      normDet_comp_of_finrank_eq _ _ hrank.symm, g.symm.toLinearIsometry.normDet_eq_one]
    simp

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

Goal state before:
pp: case neg
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 = ⊥
⊢ μH[↑(finrank ℝ U)] (⇑f '' s) = ENNReal.ofReal f.normDet * μH[↑(finrank ℝ U)] s

Tactic:
· suffices μH[finrank ℝ U] (f.range.subtypeₗᵢ '' (f.rangeRestrict '' s)) = 0 by
      simpa [(f.normDet_eq_zero_tfae.out 1 0).mp h, Set.image_image]
    rw [(LinearIsometry.isometry _).hausdorffMeasure_image (by simp)]
    have h : (finrank ℝ f.range : ℝ) < finrank ℝ U := by
      exact_mod_cast (f.normDet_eq_zero_tfae.out 1 3).mp h
    simp [Real.hausdorffMeasure_of_finrank_lt h]

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

Goal state before:
pp: H : Type u_1
inst✝ : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
x : H
S : ClosedSubmodule ℝ H
⊢ x ∈ S.symplComp ↔ ∀ y ∈ S, ⟪y, x⟫.im = 0

Tactic:
simp only [mem_orthogonal, mem_mapEquiv_iff, scalarSMulCLE_symm_apply, Units.smul_def,
    Units.val_inv_eq_inv_val, val_UnitI, inv_I, neg_smul]

Goal state after:
H : Type u_1
inst✝ : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
x : H
S : ClosedSubmodule ℝ H
⊢ (∀ (u : H), -(I • u) ∈ S → inner ℝ u x = 0) ↔ ∀ y ∈ S, ⟪y, x⟫.im = 0
Module: Mathlib.Analysis.InnerProductSpace.StandardSubspace

Goal state before:
pp: H : Type u_1
inst✝ : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
S T : ClosedSubmodule ℝ H
⊢ (S ⊔ T).symplComp = S.symplComp ⊓ T.symplComp

Tactic:
rw [symplComp, symplComp, symplComp, mulI_sup]
  exact Eq.symm (inf_orthogonal S.mulI T.mulI)

Goal state after: