mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case neg.refine_2
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
⊢ ⊤ ≤ adjoin A {b | ∃ n_1 ∈ S ∪ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1}

Tactic:
rw [← ((iff_adjoin_eq_top _ _ _).mp hB).2]

Goal state after:
case neg.refine_2
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
⊢ adjoin A {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} ≤ adjoin A {b | ∃ n_1 ∈ S ∪ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1}
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case refine_2
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 A B
x : B
hx : ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1
⊢ ∃ n_1, (n_1 = n ∨ n_1 ∈ S) ∧ n_1 ≠ 0 ∧ x ^ n_1 = 1

Tactic:
obtain ⟨m, hm, hm'⟩ := hx

Goal state after:
case refine_2
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 A B
x : B
m : ℕ
hm : m ∈ S
hm' : m ≠ 0 ∧ x ^ m = 1
⊢ ∃ n_1, (n_1 = n ∨ n_1 ∈ S) ∧ n_1 ≠ 0 ∧ x ^ n_1 = 1
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: S : Set ℕ
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : ∀ n ∈ S, n ≠ 0 → ∃ r, IsPrimitiveRoot r n
n : ℕ
hn1 : n ∈ S
hn2 : n ≠ 0
r : B
hr1 : r ^ n = 1
hr2 : ∀ (l : ℕ), r ^ l = 1 → n ∣ l
⊢ ∃ r, IsPrimitiveRoot r n

Tactic:
exact ⟨⟨r, subset_adjoin ⟨n, hn1, hn2, hr1⟩⟩, Subtype.val_injective hr1,
      fun l hl ↦ hr2 l congr($hl.1)⟩

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)
⊢ (Algebra.norm K) (ζ ^ p ^ s - 1) = ↑p ^ p ^ s

Tactic:
set η := ζ ^ p ^ s - 1

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
⊢ (Algebra.norm K) η = ↑p ^ p ^ s
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: 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
⊢ False

Tactic:
have : ζ.re < 0 ∧ ζ.im = 0 := ⟨h.1.lt_of_ne ?_, h.2⟩

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 : ζ.re < 0 ∧ ζ.im = 0
⊢ False

case refine_1
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
⊢ ζ.re ≠ 0
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: n : ℕ
inst✝⁴ : NeZero n
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
h : IsCyclotomicExtension {n} A B
⊢ (Subalgebra.toSubmodule ⊤).FG

Tactic:
← ((iff_adjoin_eq_top _ _ _).1 h).2

Goal state after:
n : ℕ
inst✝⁴ : NeZero n
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
h : IsCyclotomicExtension {n} A B
⊢ (Subalgebra.toSubmodule (adjoin A {b | ∃ n_1 ∈ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1})).FG
Module: Mathlib.Data.ZMod.Units

Goal state before:
pp: case inr
n : ℤ
m : ℕ
hm : m ≠ 0
this : NeZero m
u : (ZMod m)ˣ
hu : ↑u = ↑n
h_coprime : n.gcd ↑m = 1
⊢ IsCoprime (↑m) n

Tactic:
isCoprime_comm,

Goal state after:
case inr
n : ℤ
m : ℕ
hm : m ≠ 0
this : NeZero m
u : (ZMod m)ˣ
hu : ↑u = ↑n
h_coprime : n.gcd ↑m = 1
⊢ IsCoprime n ↑m
Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter

Goal state before:
pp: F : Type u_1
F' : Type u_2
inst✝² : Field F
inst✝¹ : Finite F
inst✝ : Field F'
h : ringChar F' ≠ ringChar F
p : ℕ := ringChar F
hp : Fact (Nat.Prime p)
pp : ℕ+ := p.toPNat ⋯
hp₂ : ¬ringChar F' ∣ p
ψ : PrimitiveAddChar (ZMod ↑pp) F' := primitiveZModChar pp F' ⋯
this : Algebra (ZMod p) F := ZMod.algebra F p
ψ' : AddChar F (CyclotomicField (↑ψ.n) F') := ψ.char.compAddMonoidHom (Algebra.trace (ZMod p) F).toAddMonoidHom
a : F
ha : (Algebra.trace (ZMod (ringChar F)) F) a ≠ 0
⊢ ψ' ≠ 1

Tactic:
exact ne_one_iff.2
      ⟨a, fun hf => ha <| (ψ.prim.zmod_char_eq_one_iff pp <| Algebra.trace (ZMod p) F a).mp hf⟩

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

Goal state before:
pp: n : ℕ
inst✝¹⁰ : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : IsFractionRing A K
inst✝ : NeZero ↑n
x✝ : n ≠ 0
⊢ ∃ r, IsPrimitiveRoot r n

Tactic:
have := NeZero.of_faithfulSMul A K n

Goal state after:
n : ℕ
inst✝¹⁰ : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : IsFractionRing A K
inst✝ : NeZero ↑n
x✝ : n ≠ 0
this : NeZero ↑n
⊢ ∃ r, IsPrimitiveRoot r n
Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
j : ℕ
⊢ ↑(toCircle ↑j) = cexp (2 * ↑π * I * ↑j / ↑N)

Tactic:
by
  simpa using toCircle_intCast (N := N) j

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
x : ZMod n
⊢ ↑↑((rootsOfUnityAddChar n) x) = toCircle x

Tactic:
by
  rfl

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
d : ℕ
inst✝ : NeZero n
h : χ.FactorsThrough d
⊢ ∃! χ', χ = (changeLevel ⋯) χ'

Tactic:
rcases h with ⟨hd, χ₂, rfl⟩

Goal state after:
R : Type u_1
inst✝¹ : CommMonoidWithZero R
n d : ℕ
inst✝ : NeZero n
hd : d ∣ n
χ₂ : DirichletCharacter R d
⊢ ∃! χ', (changeLevel hd) χ₂ = (changeLevel ⋯) χ'
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: case pos
R' : Type u_2
inst✝¹ : CommMonoidWithZero R'
R : Type u_3
inst✝ : CommMonoidWithZero R
χ : MulChar R R'
a : R
ha : IsUnit a
h : IsUnit (χ a)
⊢ (χ a)⁻¹ʳ = χ a⁻¹ʳ

Tactic:
apply_fun (χ a * ·) using IsUnit.mul_right_injective h

Goal state after:
case pos
R' : Type u_2
inst✝¹ : CommMonoidWithZero R'
R : Type u_3
inst✝ : CommMonoidWithZero R
χ : MulChar R R'
a : R
ha : IsUnit a
h : IsUnit (χ a)
⊢ (fun x ↦ χ a * x) (χ a)⁻¹ʳ = (fun x ↦ χ a * x) (χ a⁻¹ʳ)
Module: Mathlib.NumberTheory.MulChar.Lemmas

Goal state before:
pp: case h
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
R : Type u_2
inst✝ : CommRing R
n : ℕ
h : n ∣ Fintype.card F - 1
ζ : R
hζ : IsPrimitiveRoot ζ n
hn₀ : 0 < n
e : MulChar F R ≃* ↥(rootsOfUnity (Fintype.card Fˣ) R) := equiv_rootsOfUnity F R
ζ' : Rˣ := ⋯.unit
h' : ζ' ^ Fintype.card Fˣ = 1
⊢ orderOf ⟨ζ', ⋯⟩ = n

Tactic:
orderOf_eq_iff hn₀

Goal state after:
case h
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
R : Type u_2
inst✝ : CommRing R
n : ℕ
h : n ∣ Fintype.card F - 1
ζ : R
hζ : IsPrimitiveRoot ζ n
hn₀ : 0 < n
e : MulChar F R ≃* ↥(rootsOfUnity (Fintype.card Fˣ) R) := equiv_rootsOfUnity F R
ζ' : Rˣ := ⋯.unit
h' : ζ' ^ Fintype.card Fˣ = 1
⊢ ⟨ζ', ⋯⟩ ^ n = 1 ∧ ∀ m < n, 0 < m → ⟨ζ', ⋯⟩ ^ m ≠ 1
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommMonoid R
R' : Type u_2
inst✝¹ : CommRing R'
R'' : Type u_3
inst✝ : CommRing R''
f : R' →+* R''
⊢ ringHomComp 1 f = 1

Tactic:
by
  ext1
  simp only [MulChar.ringHomComp_apply, MulChar.one_apply_coe, map_one]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
⊢ conductor 1 ∣ n

Tactic:
rw [(isPrimitive_def _).mp isPrimitive_one_level_one]
  apply one_dvd _

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

Goal state before:
pp: case pos
R : Type u_1
inst✝³ : CommMonoid R
inst✝² : Fintype R
R' : Type u_2
inst✝¹ : CommRing R'
inst✝ : DecidableEq R
a : R
x✝ : a ∈ Finset.univ
h : IsUnit a
⊢ 1 a = 1

pp: case neg
R : Type u_1
inst✝³ : CommMonoid R
inst✝² : Fintype R
R' : Type u_2
inst✝¹ : CommRing R'
inst✝ : DecidableEq R
a : R
x✝ : a ∈ Finset.univ
h : ¬IsUnit a
⊢ 1 a = 0

Tactic:
· exact one_apply_coe h.unit

Goal state after:
case neg
R : Type u_1
inst✝³ : CommMonoid R
inst✝² : Fintype R
R' : Type u_2
inst✝¹ : CommRing R'
inst✝ : DecidableEq R
a : R
x✝ : a ∈ Finset.univ
h : ¬IsUnit a
⊢ 1 a = 0
Module: Mathlib.Analysis.Fourier.ZMod

Goal state before:
pp: N : ℕ
inst✝² : NeZero N
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
Φ : ZMod N → E
j : ZMod N
h1 : ∀ (t : ZMod N), ∑ i, stdAddChar (t * i) = if t = 0 then ↑N else 0
⊢ ∑ x, (∑ i, stdAddChar (-(j + x) * i)) • Φ x = ↑N • Φ (-j)

Tactic:
have h2 (x j : ZMod N) : -(j + x) = 0 ↔ x = -j := by
    rw [neg_add, add_comm, add_eq_zero_iff_neg_eq, neg_neg]

Goal state after:
N : ℕ
inst✝² : NeZero N
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
Φ : ZMod N → E
j : ZMod N
h1 : ∀ (t : ZMod N), ∑ i, stdAddChar (t * i) = if t = 0 then ↑N else 0
h2 : ∀ (x j : ZMod N), -(j + x) = 0 ↔ x = -j
⊢ ∑ x, (∑ i, stdAddChar (-(j + x) * i)) • Φ x = ↑N • Φ (-j)
Module: Mathlib.Data.Finset.Interval

Goal state before:
pp: case pos.mpr
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s t u : Finset α
hst : s ⊆ t
⊢ s ⊆ u ∧ u ⊆ t → ∃ a ⊆ t, Disjoint a s ∧ a ∪ s = u

Tactic:
· rintro ⟨hsu, hut⟩
          exact ⟨u \ s, sdiff_subset.trans hut, disjoint_sdiff_self_left, sdiff_union_of_subset hsu⟩

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

Goal state before:
pp: V : Type u_2
P : Type u_3
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c : P
t₁ t₂ : ℝ
h_inner : ⟪b -ᵥ a, c -ᵥ a⟫ = 0
hvec : (AffineMap.lineMap a b) t₁ -ᵥ (AffineMap.lineMap a c) t₂ = t₁ • (b -ᵥ a) - t₂ • (c -ᵥ a)
⊢ ‖t₁ • (b -ᵥ a) - t₂ • (c -ᵥ a)‖ ^ 2 = t₁ ^ 2 * dist a b ^ 2 + t₂ ^ 2 * dist a c ^ 2

Tactic:
norm_sub_sq_real,

Goal state after:
V : Type u_2
P : Type u_3
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c : P
t₁ t₂ : ℝ
h_inner : ⟪b -ᵥ a, c -ᵥ a⟫ = 0
hvec : (AffineMap.lineMap a b) t₁ -ᵥ (AffineMap.lineMap a c) t₂ = t₁ • (b -ᵥ a) - t₂ • (c -ᵥ a)
⊢ ‖t₁ • (b -ᵥ a)‖ ^ 2 - 2 * ⟪t₁ • (b -ᵥ a), t₂ • (c -ᵥ a)⟫ + ‖t₂ • (c -ᵥ a)‖ ^ 2 =
    t₁ ^ 2 * dist a b ^ 2 + t₂ ^ 2 * dist a c ^ 2
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 ι
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
p : ℝ
hp₀ : 0 ≤ p
hp : (↑#ι - 1) * p ≤ 1
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (x : (i : ι) → A i), f x ^ (1 - (↑#ι - 1) * p) * ∏ i, (∫⁻ (xᵢ : A i), f (update x i xᵢ) ∂μ i) ^ p ∂Measure.pi μ ≤
    (∫⁻ (x : (i : ι) → A i), f x ∂Measure.pi μ) ^ (1 + p)

Tactic:
by
  cases isEmpty_or_nonempty (∀ i, A i)
  · simp
  inhabit ∀ i, A i
  have H : (∅ : Finset ι) ≤ Finset.univ := Finset.empty_subset _
  simpa [lmarginal_univ] using GridLines.T_lmarginal_antitone μ hp₀ hp hf H default

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
p : E →ₗ[𝕜] E
hp : p.IsSymmetricProjection
a : E
ha : a ∈ p.range
hh : ∀ {T : E →ₗ[𝕜] E}, T.IsSymmetricProjection → re ⟪T a, a⟫ = ‖T a‖ ^ 2
U : Submodule 𝕜 E
w✝ : U.HasOrthogonalProjection
hq : (↑U.starProjection).IsSymmetricProjection
x✝ : p ≤ ↑U.starProjection
h1 : (↑U.starProjection - p).IsSymmetric
h2 : ‖a‖ ≤ ‖↑U.starProjection a‖
⊢ a ∈ (↑U.starProjection).range

Tactic:
simpa [Submodule.toLinearMap_starProjection_eq_isComplProjection] using
    U.mem_iff_norm_starProjection _ |>.mpr <| le_antisymm (U.norm_starProjection_apply_le a) h2

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✝ : FiniteDimensional 𝕜 E
T : E →L[𝕜] E
⊢ T.IsPositive ↔ ∃ m u, T = ∑ i, ((rankOne 𝕜) (u i)) (u i)

Tactic:
by
  refine ⟨fun hT ↦ ?_, fun ⟨m, u, hT⟩ ↦ hT ▸ isPositive_sum _ fun _ _ ↦ isPositive_rankOne_self _⟩
  let a (i : Fin (Module.finrank 𝕜 E)) : E :=
    ((hT.isSymmetric.eigenvalues rfl i).sqrt : 𝕜) • hT.isSymmetric.eigenvectorBasis rfl i
  refine ⟨Module.finrank 𝕜 E, a, ext fun _ ↦ ?_⟩
  simp_rw [_root_.sum_apply, rankOne_apply, a, inner_smul_left, smul_smul, mul_assoc, conj_ofReal,
    mul_comm (⟪_, _⟫_𝕜), ← mul_assoc, ← ofReal_mul,
    ← Real.sqrt_mul (hT.toLinearMap.nonneg_eigenvalues rfl _),
    Real.sqrt_mul_self (hT.toLinearMap.nonneg_eigenvalues rfl _), mul_comm _ (⟪_, _⟫_𝕜),
    ← smul_eq_mul, smul_assoc, ← hT.isSymmetric.apply_eigenvectorBasis, ← map_smul, ← map_sum,
    ← OrthonormalBasis.repr_apply_apply, OrthonormalBasis.sum_repr, coe_coe]

Goal state after:
Module: Mathlib.Topology.Algebra.Module.LinearPMap

Goal state before:
pp: case mp
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
f : E →ₗ.[R] F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
hf : f.toFun.ker = ⊥
hf' : f.IsClosable
f' : F →ₗ.[R] E
h : f.inverse.graph.topologicalClosure = f'.graph
⊢ ∀ (m : ↥f.closure.domain), f.closure.toFun m = 0 → m = 0

Tactic:
intro ⟨x, hx⟩

Goal state after:
case mp
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
f : E →ₗ.[R] F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
hf : f.toFun.ker = ⊥
hf' : f.IsClosable
f' : F →ₗ.[R] E
h : f.inverse.graph.topologicalClosure = f'.graph
x : E
hx : x ∈ f.closure.domain
⊢ f.closure.toFun ⟨x, hx⟩ = 0 → ⟨x, hx⟩ = 0
Module: Mathlib.Topology.Algebra.Module.LinearPMap

Goal state before:
pp: case mpr
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
f : E →ₗ.[R] F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
hf : f.toFun.ker = ⊥
hf' : f.IsClosable
⊢ f.closure.toFun.ker = ⊥ → f.inverse.IsClosable

Tactic:
· intro h
    use f.closure.inverse
    exact (closure_inverse_graph hf hf' h).symm

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

Goal state before:
pp: case neg.inr
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
h2n : 0 < ↑n - 1
hnp : 0 < ↑n - ↑p
hp : 1 < p
q : ℝ := (↑p).conjExponent
hq : (↑p).HolderConjugate q
h0p : p ≠ 0
⊢ eLpNorm u (↑p') μ ≤ ↑(eLpNormLESNormFDerivOfEqInnerConst μ ↑p) * eLpNorm (fderiv ℝ u) (↑p) μ

Tactic:
have h1p : (p : ℝ) ≠ 1 := hq.lt.ne'

Goal state after:
case neg.inr
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
h2n : 0 < ↑n - 1
hnp : 0 < ↑n - ↑p
hp : 1 < p
q : ℝ := (↑p).conjExponent
hq : (↑p).HolderConjugate q
h0p : p ≠ 0
h1p : ↑p ≠ 1
⊢ eLpNorm u (↑p') μ ≤ ↑(eLpNormLESNormFDerivOfEqInnerConst μ ↑p) * eLpNorm (fderiv ℝ u) (↑p) μ
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
n : ℕ
e : Fin n → E
g : Fin n → G
hx : x = ∑ j, e j ⊗ₜ[𝕜] g j
c : E ⊗[𝕜] G →₀ 𝕜
hc_supp : ↑c.support ⊆ {t | ∃ m n, m ⊗ₜ[𝕜] n = t}
hc : (c.sum fun mi r ↦ r • mi) = x
m : ℕ
A : Fin m → Fin n → 𝕜
hA :
  ∀ (i j : Fin n),
    ‖f‖ ^ 2 • inner 𝕜 (e i) (e j) - (∑ i, Matrix.vecMulVec (A i) (star (A i))) i j = inner 𝕜 (f (e i)) (f (e j))
⊢ 0 ≤ RCLike.re (∑ x, ∑ x_1, ∑ i, inner 𝕜 (g x_1) (g x) * Matrix.vecMulVec (A i) (star (A i)) x_1 x)

Tactic:
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]

Goal state after:
𝕜 : 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
n : ℕ
e : Fin n → E
g : Fin n → G
hx : x = ∑ j, e j ⊗ₜ[𝕜] g j
c : E ⊗[𝕜] G →₀ 𝕜
hc_supp : ↑c.support ⊆ {t | ∃ m n, m ⊗ₜ[𝕜] n = t}
hc : (c.sum fun mi r ↦ r • mi) = x
m : ℕ
A : Fin m → Fin n → 𝕜
hA :
  ∀ (i j : Fin n),
    ‖f‖ ^ 2 • inner 𝕜 (e i) (e j) - (∑ i, Matrix.vecMulVec (A i) (star (A i))) i j = inner 𝕜 (f (e i)) (f (e j))
⊢ 0 ≤
    RCLike.re
      (∑ x,
        ∑ x_1,
          ∑ x_2,
            inner 𝕜 ((starRingEnd 𝕜) (A x x_2) • g x_2) (g x_1) * star ((starRingEnd 𝕜) ((starRingEnd 𝕜) (A x x_1))))
Module: Mathlib.Geometry.Euclidean.Volume.Measure

Goal state before:
pp: X : Type u_1
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
d : ℕ
⊢ μHE[d] = volume.addHaarScalarFactor μH[↑d] • μH[↑d]

Tactic:
by
  rfl

Goal state after:
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:
by
  rw [dimH_def] at h
  rcases ENNReal.lt_iff_exists_nnreal_btwn.1 h with ⟨d', hsd', hd'd⟩
  rw [ENNReal.coe_lt_coe, ← NNReal.coe_lt_coe] at hd'd
  exact (hausdorffMeasure_zero_or_top hd'd s).resolve_right fun h₂ => hsd'.not_ge <|
    le_iSup₂ (α := ℝ≥0∞) d' h₂

Goal state after:
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
i : ℝ≥0
hi : μH[↑i] s = 0
j : ℝ≥0
hj : μH[↑j] s = ∞
hij : i < j
⊢ False

Tactic:
simpa [hi, hj] using hausdorffMeasure_mono hij.le s

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

Goal state before:
pp: X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : OpensMeasurableSpace X
m : Set X → ℝ≥0∞
hcl : ∀ (s : Set X), m (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) = m s
r : ℝ≥0∞
⊢ (pre m r).trim = pre m r

Tactic:
refine le_antisymm (le_pre.2 fun s hs => ?_) (le_trim _)

Goal state after:
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : OpensMeasurableSpace X
m : Set X → ℝ≥0∞
hcl : ∀ (s : Set X), m (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) = m s
r : ℝ≥0∞
s : Set X
hs : ediam s ≤ r
⊢ (pre m r).trim s ≤ m s
Module: Mathlib.Analysis.InnerProductSpace.OfNorm

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x y : E
hI : ¬I = 0
hI' : I * I = -1
I_smul : ∀ (v : E), ‖I • v‖ = ‖v‖
⊢ 4⁻¹ *
      (↑‖x + y‖ * ↑‖x + y‖ - ↑‖x - y‖ * ↑‖x - y‖ + -I * ↑‖I • y + x‖ * ↑‖I • y + x‖ -
        -I * ↑‖I • y - x‖ * ↑‖I • y - x‖) =
    4⁻¹ *
      (𝓚 ‖x + y‖ * 𝓚 ‖x + y‖ - 𝓚 ‖x - y‖ * 𝓚 ‖x - y‖ + I * 𝓚 ‖I • x + y‖ * 𝓚 ‖I • x + y‖ -
        I * 𝓚 ‖I • x - y‖ * 𝓚 ‖I • x - y‖)

Tactic:
have h₁ : ‖(I : 𝕜) • y - x‖ = ‖(I : 𝕜) • x + y‖ := by
    convert I_smul ((I : 𝕜) • x + y)
    linear_combination (norm := module) -hI' • x

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x y : E
hI : ¬I = 0
hI' : I * I = -1
I_smul : ∀ (v : E), ‖I • v‖ = ‖v‖
h₁ : ‖I • y - x‖ = ‖I • x + y‖
⊢ 4⁻¹ *
      (↑‖x + y‖ * ↑‖x + y‖ - ↑‖x - y‖ * ↑‖x - y‖ + -I * ↑‖I • y + x‖ * ↑‖I • y + x‖ -
        -I * ↑‖I • y - x‖ * ↑‖I • y - x‖) =
    4⁻¹ *
      (𝓚 ‖x + y‖ * 𝓚 ‖x + y‖ - 𝓚 ‖x - y‖ * 𝓚 ‖x - y‖ + I * 𝓚 ‖I • x + y‖ * 𝓚 ‖I • x + y‖ -
        I * 𝓚 ‖I • x - y‖ * 𝓚 ‖I • x - y‖)
Module: Mathlib.Analysis.InnerProductSpace.NormDet

Goal state before:
pp: case pos
𝕜 : Type u_1
U : Type u_2
V : Type u_3
W : Type u_4
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NormedAddCommGroup U
inst✝⁶ : InnerProductSpace 𝕜 U
inst✝⁵ : FiniteDimensional 𝕜 U
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace 𝕜 V
inst✝² : NormedAddCommGroup W
inst✝¹ : InnerProductSpace 𝕜 W
inst✝ : FiniteDimensional 𝕜 V
f : U →ₗ[𝕜] V
g : V →ₗ[𝕜] W
h : finrank 𝕜 U = finrank 𝕜 V
htop : f.range = ⊤
⊢ (g ∘ₗ f).normDet = g.normDet * f.normDet

Tactic:
normDet_comp

Goal state after:
case pos
𝕜 : Type u_1
U : Type u_2
V : Type u_3
W : Type u_4
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NormedAddCommGroup U
inst✝⁶ : InnerProductSpace 𝕜 U
inst✝⁵ : FiniteDimensional 𝕜 U
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace 𝕜 V
inst✝² : NormedAddCommGroup W
inst✝¹ : InnerProductSpace 𝕜 W
inst✝ : FiniteDimensional 𝕜 V
f : U →ₗ[𝕜] V
g : V →ₗ[𝕜] W
h : finrank 𝕜 U = finrank 𝕜 V
htop : f.range = ⊤
⊢ (g.domRestrict f.range).normDet * f.normDet = g.normDet * f.normDet
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
p : Submodule 𝕜 V
f : U →ₗ[𝕜] V
h : ∀ (c : U), f c ∈ p
this : f = p.subtype ∘ₗ codRestrict p f h
⊢ (codRestrict p f h).normDet = (p.subtype ∘ₗ codRestrict p f h).normDet

Tactic:
normDet_comp

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
p : Submodule 𝕜 V
f : U →ₗ[𝕜] V
h : ∀ (c : U), f c ∈ p
this : f = p.subtype ∘ₗ codRestrict p f h
⊢ (codRestrict p f h).normDet = (p.subtype.domRestrict (codRestrict p f h).range).normDet * (codRestrict p f h).normDet