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

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

Tactic:
show ζ ^ (r % n) = ζ ^ r from (IsPrimitiveRoot.eq_orderOf hζ).symm ▸ pow_mod_orderOf ..,

Goal state after:
n : ℕ
inst✝³ : NeZero n
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
hno : Odd n
ζ x : K
hζ : IsPrimitiveRoot ζ n
hx : IsOfFinOrder x
r : ℕ
hr : x = (-ζ) ^ r
⊢ x = ζ ^ r ∨ x = -ζ ^ r
Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Goal state before:
pp: case f
n : ℕ
inst✝⁴ : NeZero n
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst✝ : IsCyclotomicExtension {n} K L
h : 2 < n
hirr : Irreducible (cyclotomic n K)
this✝¹ : NeZero ↑n
E : Type v := AlgebraicClosure L
z : E
hz : (cyclotomic n E).IsRoot z
this✝ : FiniteDimensional K L := finiteDimensional {n} K L
this : IsGalois K L := isGalois {n} K L
x✝ : L →ₐ[K] E
| -(1 - x✝ ζ)

Tactic:
neg_eq_neg_one_mul

Goal state after:
case f
n : ℕ
inst✝⁴ : NeZero n
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst✝ : IsCyclotomicExtension {n} K L
h : 2 < n
hirr : Irreducible (cyclotomic n K)
this✝¹ : NeZero ↑n
E : Type v := AlgebraicClosure L
z : E
hz : (cyclotomic n E).IsRoot z
this✝ : FiniteDimensional K L := finiteDimensional {n} K L
this : IsGalois K L := isGalois {n} K L
x✝ : L →ₐ[K] E
| -1 * (1 - x✝ ζ)
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case refine_1.inr
S : Set ℕ
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
H : IsCyclotomicExtension S A B
s : ℕ
hs' : s ≠ 0
inst✝ : NeZero s
x : ℕ
hm : s * x ∈ S
hm' : s * x ≠ 0
ζ : B
hζ : IsPrimitiveRoot ζ (s * x)
h_xnz : x ≠ 0
this : IsPrimitiveRoot (ζ ^ x) (s * x / x)
⊢ IsPrimitiveRoot (ζ ^ x) s

Tactic:
mul_div_cancel_right₀ _ h_xnz

Goal state after:
case refine_1.inr
S : Set ℕ
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
H : IsCyclotomicExtension S A B
s : ℕ
hs' : s ≠ 0
inst✝ : NeZero s
x : ℕ
hm : s * x ∈ S
hm' : s * x ≠ 0
ζ : B
hζ : IsPrimitiveRoot ζ (s * x)
h_xnz : x ≠ 0
this : IsPrimitiveRoot (ζ ^ x) s
⊢ IsPrimitiveRoot (ζ ^ x) s
Module: Mathlib.FieldTheory.Finite.Trace

Goal state before:
pp: F : Type u_1
inst✝² : Field F
inst✝¹ : Finite F
inst✝ : Algebra (ZMod (ringChar F)) F
a : F
ha : a ≠ 0
this : Fact (Nat.Prime (ringChar F))
htr : (∀ (y : F), (Algebra.trace (ZMod (ringChar F)) F) (a * y) = 0) → a = 0
hf : ∀ (b : F), (Algebra.trace (ZMod (ringChar F)) F) (a * b) = 0
⊢ False

Tactic:
exact ha (htr hf)

Goal state after:
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
h : ∀ n ∈ S, n ≠ 0 → ∃ r, IsPrimitiveRoot r n
⊢ IsCyclotomicExtension S K ↥(IntermediateField.adjoin K {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})

Tactic:
by
  have key : ∀ b ∈ {b : L | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}, IsAlgebraic K b := by
    rintro b ⟨n, hn, h1, h2⟩
    exact ⟨X ^ n - 1, (monic_X_pow_sub_C (1 : K) h1).ne_zero, by simp [h2]⟩
  change IsCyclotomicExtension S K (IntermediateField.toSubalgebra _)
  rw [congr(IsCyclotomicExtension S K $(IntermediateField.adjoin_toSubalgebra_of_isAlgebraic key))]
  exact Algebra.isCyclotomicExtension_adjoin_of_exists_isPrimitiveRoot S K L h

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

Goal state before:
pp: case a
S : Set ℕ
K : Type w
L : Type z
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension S K L
M : Type u_1
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsSepClosed M
this : Algebra.IsSeparable K L
i : L →ₐ[K] M := IsSepClosed.lift
htop : IntermediateField.adjoin K {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1} = ⊤
y : L
n : ℕ
hn : n ∈ S
h1 : n ≠ 0
h2 : y ^ n = 1
⊢ i y ∈ ↑(IntermediateField.adjoin K {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})

Tactic:
exact IntermediateField.subset_adjoin K _ ⟨n, hn, h1, by simpa using congrArg i h2⟩

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

Goal state before:
pp: K : Type u_1
K' : Type u_2
inst✝³ : Field K
inst✝² : Field K'
inst✝¹ : Algebra K K'
inst✝ : Finite K'
this✝ : Finite K
this : Fintype K'ˣ
⊢ Nat.card ↥(Units.map (Algebra.norm K)).ker ≤ (Nat.card K' - 1) / (Nat.card K - 1)

Tactic:
convert!
      IsCyclic.card_pow_eq_one_le (α := K'ˣ) <|
        Nat.div_pos
            (Nat.sub_le_sub_right (Nat.card_le_card_of_injective _ (algebraMap K K').injective)
              _) <|
          Nat.sub_pos_of_lt Finite.one_lt_card

Goal state after:
K : Type u_1
K' : Type u_2
inst✝³ : Field K
inst✝² : Field K'
inst✝¹ : Algebra K K'
inst✝ : Finite K'
this✝ : Finite K
this : Fintype K'ˣ
⊢ Nat.card ↥(Units.map (Algebra.norm K)).ker = #{a | a ^ ((Nat.card K' - 1) / (Nat.card K - 1)) = 1}
Module: Mathlib.FieldTheory.Finite.GaloisField

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

Tactic:
choose n' hp' hK' using FiniteField.card K' p'

Goal state after:
p✝ : ℕ
inst✝⁴ : Fact (Nat.Prime p✝)
n✝ : ℕ
K : Type u_1
K' : Type u_2
inst✝³ : Field K
inst✝² : Field K'
inst✝¹ : Fintype K
inst✝ : Fintype K'
hKK' : Fintype.card K = Fintype.card K'
p : ℕ
_char_p_K : CharP K p
p' : ℕ
_char_p'_K' : CharP K' p'
n : ℕ+
hp : Nat.Prime p
hK : Fintype.card K = p ^ ↑n
n' : ℕ+
hp' : Nat.Prime p'
hK' : Fintype.card K' = p' ^ ↑n'
⊢ K ≃+* K'
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
⊢ IsTorsionFree A (CyclotomicField n K)

Tactic:
rw [isTorsionFree_iff_faithfulSMul, faithfulSMul_iff_algebraMap_injective,
    IsScalarTower.algebraMap_eq A K (CyclotomicField n K)]
  exact
    (Function.Injective.comp (FaithfulSMul.algebraMap_injective K (CyclotomicField n K))
      (IsFractionRing.injective A K) :)

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

Goal state before:
pp: case h
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✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : NeZero ↑n
x✝ : ↥(nonZeroDivisors (CyclotomicRing n A K))
x : CyclotomicRing n A K
hx : x ∈ nonZeroDivisors (CyclotomicRing n A K)
⊢ ↑⟨x, hx⟩ ∈ nonZeroDivisors (CyclotomicRing n A K)

Tactic:
· exact hx

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

Goal state before:
pp: n : ℕ
hn : n % 2 = 1
⊢ (if n % 4 = 1 then 1 else -1) = (-1) ^ ((n % 4 + 2 * (2 * (n / 4))) / 2)

Tactic:
Nat.add_mul_div_left _ _ zero_lt_two,

Goal state after:
n : ℕ
hn : n % 2 = 1
⊢ (if n % 4 = 1 then 1 else -1) = (-1) ^ (n % 4 / 2 + 2 * (n / 4))
Module: Mathlib.NumberTheory.MulChar.Lemmas

Goal state before:
pp: F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
R : Type u_2
inst✝ : CommRing R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
hn : n = 0
h : Fintype.card F ≤ 1
⊢ False

Tactic:
exact (Fintype.one_lt_card.trans_le h).false

Goal state after:
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
inst✝ : IsDomain B
C : Subalgebra A B
hS : ∀ n ∈ S, n ≠ 0 → ∃ r, IsPrimitiveRoot r n
h : IsCyclotomicExtension S A ↥C
this : Subalgebra.map C.val (adjoin A {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) = Subalgebra.map C.val ⊤
x✝ : B
⊢ x✝ ∈ ⇑C.val '' {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} ↔ x✝ ∈ {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}

Tactic:
simp only [Subalgebra.coe_val, ne_eq, ← Subalgebra.coe_eq_one, SubmonoidClass.coe_pow,
    Set.mem_image, Set.mem_ofPred_eq, Subtype.exists, exists_and_left, exists_prop,
    exists_eq_right_right, and_iff_left_iff_imp, forall_exists_index, and_imp]

Goal state after:
S : Set ℕ
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
C : Subalgebra A B
hS : ∀ n ∈ S, n ≠ 0 → ∃ r, IsPrimitiveRoot r n
h : IsCyclotomicExtension S A ↥C
this : Subalgebra.map C.val (adjoin A {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) = Subalgebra.map C.val ⊤
x✝ : B
⊢ ∀ x ∈ S, ¬x = 0 → x✝ ^ x = 1 → x✝ ∈ C
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: R : Type u_1
R' : Type u_2
inst✝¹ : CommRing R
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
n : ℕ
hn : Odd n
hχ : χ ^ n = 1
⊢ 1 (-1) = 1

Tactic:
exact MulChar.one_apply_coe (-1)

Goal state after:
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]

Goal state after:
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
⊢ ∑ a, 1 a * ψ a + 1 = 0
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
⊢ ∑ a ∈ {0}ᶜ, 1 a * ψ a + 1 = ∑ a ∈ {0}ᶜ, ψ a + ψ 0

Tactic:
congr! <;> aesop (add simp MulChar.one_apply)

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

Goal state before:
pp: case neg
N : ℕ
inst✝² : NeZero N
R : Type u_1
inst✝¹ : CommRing R
e : AddChar (ZMod N) R
inst✝ : IsDomain R
χ : DirichletCharacter R N
hχ : χ.IsPrimitive
a : ZMod N
ha : ¬IsUnit a
⊢ gaussSum χ (e.mulShift a) = 0

Tactic:
exact gaussSum_eq_zero_of_isPrimitive_of_not_isPrimitive _ hχ (not_isPrimitive_mulShift e ha)

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
⊢ ⟪a -ᵥ c, a -ᵥ c - (b -ᵥ c)⟫ = 0 ↔ ⟪a -ᵥ c, b -ᵥ a⟫ = 0

Tactic:
vsub_sub_vsub_cancel_right,

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
⊢ ⟪a -ᵥ c, a -ᵥ b⟫ = 0 ↔ ⟪a -ᵥ c, b -ᵥ a⟫ = 0
Module: Mathlib.Analysis.InnerProductSpace.Coalgebra

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_3
inst✝¹ : Fintype n
inst✝ : DecidableEq n
⊢ counit = adjoint (↑↑(equiv n 𝕜).symm ∘ₗ Algebra.linearMap 𝕜 (n → 𝕜)) ∘ₗ ↑↑(equiv n 𝕜).symm

Tactic:
ext
  simp [← toSpanSingleton_one_eq_algebraLinearMap, comp_toSpanSingleton,
    adjoint_toSpanSingleton, inner_eq_star_dotProduct]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : Coalgebra 𝕜 E
x y z : E
⊢ (x + y) * z = x * z + y * z

Tactic:
simp [add_tmul]

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

Goal state before:
pp: case neg
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
v : V
h : ¬0 < ‖v‖
⊢ C * ‖v‖ ≤ ‖(continuousLinearMapOfBilin B) v‖

Tactic:
have : v = 0 := by simpa using h

Goal state after:
case neg
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
v : V
h : ¬0 < ‖v‖
this : v = 0
⊢ 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
T : E ≃ₗ[𝕜] E
hT : (↑T).IsPositive
x : E
⊢ ?m.59

Tactic:
by simpa using hT.2 (T.symm.toLinearMap x)

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

Goal state before:
pp: R : Type u_1
α : Type u_2
M : Type u_3
inst✝² : DivisionSemiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : α → α
g g' : α → M
⊢ birkhoffAverage R f (g - g') = birkhoffAverage R f g - birkhoffAverage R f g'

Tactic:
by
  funext _ x
  simp [birkhoffAverage, birkhoffSum, smul_sub]

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

Tactic:
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
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
E' : Submodule 𝕜 E
F' : Submodule 𝕜 F
iE' : Module.Finite 𝕜 ↥E'
iF' : Module.Finite 𝕜 ↥F'
y : ↥E' ⊗[𝕜] ↥F'
hz : {(mapIncl E' F') y} ⊆ ↑(mapIncl E' F').range
e : OrthonormalBasis (Fin (finrank 𝕜 ↥E')) 𝕜 ↥E'
f : OrthonormalBasis (Fin (finrank 𝕜 ↥F')) 𝕜 ↥F'
hx : ∑ i, ‖((e.toBasis.tensorProduct f.toBasis).repr y) i‖ ^ 2 = 0
i : Fin (finrank 𝕜 ↥E')
j : Fin (finrank 𝕜 ↥F')
⊢ ((e.toBasis.tensorProduct f.toBasis).repr y) (i, j) = 0

Tactic:
Finset.sum_eq_zero_iff_of_nonneg fun _ _ => sq_nonneg _

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
E' : Submodule 𝕜 E
F' : Submodule 𝕜 F
iE' : Module.Finite 𝕜 ↥E'
iF' : Module.Finite 𝕜 ↥F'
y : ↥E' ⊗[𝕜] ↥F'
hz : {(mapIncl E' F') y} ⊆ ↑(mapIncl E' F').range
e : OrthonormalBasis (Fin (finrank 𝕜 ↥E')) 𝕜 ↥E'
f : OrthonormalBasis (Fin (finrank 𝕜 ↥F')) 𝕜 ↥F'
hx : ∀ i ∈ Finset.univ, ‖((e.toBasis.tensorProduct f.toBasis).repr y) i‖ ^ 2 = 0
i : Fin (finrank 𝕜 ↥E')
j : Fin (finrank 𝕜 ↥F')
⊢ ((e.toBasis.tensorProduct f.toBasis).repr y) (i, j) = 0
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
x y : E ⊗[𝕜] F
x✝³ : E
x✝² : F
x✝¹ x✝ : E ⊗[𝕜] F
h1 : inner 𝕜 ((TensorProduct.comm 𝕜 E F) (x✝³ ⊗ₜ[𝕜] x✝²)) ((TensorProduct.comm 𝕜 E F) x✝¹) = inner 𝕜 (x✝³ ⊗ₜ[𝕜] x✝²) x✝¹
h2 : inner 𝕜 ((TensorProduct.comm 𝕜 E F) (x✝³ ⊗ₜ[𝕜] x✝²)) ((TensorProduct.comm 𝕜 E F) x✝) = inner 𝕜 (x✝³ ⊗ₜ[𝕜] x✝²) x✝
⊢ inner 𝕜 ((TensorProduct.comm 𝕜 E F) (x✝³ ⊗ₜ[𝕜] x✝²)) ((TensorProduct.comm 𝕜 E F) (x✝¹ + x✝)) =
    inner 𝕜 (x✝³ ⊗ₜ[𝕜] x✝²) (x✝¹ + x✝)

Tactic:
simp only [inner_add_right, map_add, h1, h2]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : 𝕜 ⊗[𝕜] E
x✝³ : 𝕜
x✝² : E
x✝¹ x✝ : 𝕜 ⊗[𝕜] E
h1 : inner 𝕜 ((TensorProduct.lid 𝕜 E) (x✝³ ⊗ₜ[𝕜] x✝²)) ((TensorProduct.lid 𝕜 E) x✝¹) = inner 𝕜 (x✝³ ⊗ₜ[𝕜] x✝²) x✝¹
h2 : inner 𝕜 ((TensorProduct.lid 𝕜 E) (x✝³ ⊗ₜ[𝕜] x✝²)) ((TensorProduct.lid 𝕜 E) x✝) = inner 𝕜 (x✝³ ⊗ₜ[𝕜] x✝²) x✝
⊢ inner 𝕜 ((TensorProduct.lid 𝕜 E) (x✝³ ⊗ₜ[𝕜] x✝²)) ((TensorProduct.lid 𝕜 E) (x✝¹ + x✝)) =
    inner 𝕜 (x✝³ ⊗ₜ[𝕜] x✝²) (x✝¹ + x✝)

Tactic:
simp only [inner_add_right, map_add, h1, h2]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : InnerProductSpace 𝕜 G
x y : E ⊗[𝕜] F ⊗[𝕜] G
a : E ⊗[𝕜] F
x✝³ : G
c : E ⊗[𝕜] F
x✝² : G
x✝¹ : E
x✝ : F
⊢ ∀ (x : E) (y : F),
    inner 𝕜 ((TensorProduct.assoc 𝕜 E F G) (x✝¹ ⊗ₜ[𝕜] x✝ ⊗ₜ[𝕜] x✝³))
        ((TensorProduct.assoc 𝕜 E F G) (x ⊗ₜ[𝕜] y ⊗ₜ[𝕜] x✝²)) =
      inner 𝕜 (x✝¹ ⊗ₜ[𝕜] x✝ ⊗ₜ[𝕜] x✝³) (x ⊗ₜ[𝕜] y ⊗ₜ[𝕜] x✝²)

Tactic:
by simp [mul_assoc]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : InnerProductSpace 𝕜 G
x y : E ⊗[𝕜] F ⊗[𝕜] G
a : E ⊗[𝕜] F
x✝² : G
x✝¹ x✝ : E ⊗[𝕜] F ⊗[𝕜] G
h1 :
  inner 𝕜 ((TensorProduct.assoc 𝕜 E F G) (a ⊗ₜ[𝕜] x✝²)) ((TensorProduct.assoc 𝕜 E F G) x✝¹) = inner 𝕜 (a ⊗ₜ[𝕜] x✝²) x✝¹
h2 : inner 𝕜 ((TensorProduct.assoc 𝕜 E F G) (a ⊗ₜ[𝕜] x✝²)) ((TensorProduct.assoc 𝕜 E F G) x✝) = inner 𝕜 (a ⊗ₜ[𝕜] x✝²) x✝
⊢ inner 𝕜 ((TensorProduct.assoc 𝕜 E F G) (a ⊗ₜ[𝕜] x✝²)) ((TensorProduct.assoc 𝕜 E F G) (x✝¹ + x✝)) =
    inner 𝕜 (a ⊗ₜ[𝕜] x✝²) (x✝¹ + x✝)

Tactic:
simp only [inner_add_right, map_add, h1, h2]

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

Goal state before:
pp: X : Type u_2
inst✝ : EMetricSpace X
m : Set X → ℝ≥0∞
s : Set X
⊢ Tendsto (fun r ↦ (pre m r) s) (𝓝[>] 0) (𝓝 ((mkMetric' m) s))

Tactic:
rw [← tendsto_comp_coe_Ioi_atBot]

Goal state after:
X : Type u_2
inst✝ : EMetricSpace X
m : Set X → ℝ≥0∞
s : Set X
⊢ Tendsto (fun x ↦ (pre m ↑x) s) atBot (𝓝 ((mkMetric' m) s))
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
d : ℝ
hd : ↑(finrank ℝ E) < d
⊢ μH[d] = 0

Tactic:
by
  lift d to ℝ≥0 using (Nat.cast_nonneg _).trans hd.le
  rw [← measure_univ_eq_zero]
  apply hausdorffMeasure_of_dimH_lt
  rw [dimH_univ_eq_finrank]
  exact mod_cast hd

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

Goal state before:
pp: case pos
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
htr : ∀ (n : ℕ), ediam (t n) ≤ r
⊢ ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ⨅ (_ : ediam (t n) ≤ r), m (ediam (t n)) =
    ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ r), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (ediam (t n))

Tactic:
rw [iInf_eq_if, if_pos htr]

Goal state after:
case pos
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
htr : ∀ (n : ℕ), ediam (t n) ≤ r
⊢ ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ⨅ (_ : ediam (t n) ≤ r), m (ediam (t n)) =
    ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (ediam (t n))
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: case pos
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
htr : ∀ (n : ℕ), ediam (t n) ≤ r
⊢ ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ⨅ (_ : ediam (t n) ≤ r), m (ediam (t n)) =
    ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ r), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (ediam (t n))

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
htr : ¬∀ (n : ℕ), ediam (t n) ≤ r
⊢ ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ⨅ (_ : ediam (t n) ≤ r), m (ediam (t n)) =
    ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ r), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (ediam (t n))

Tactic:
· rw [iInf_eq_if, if_pos htr]
    congr 1 with n : 1
    simp only [iInf_eq_if, htr n, if_true]

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
htr : ¬∀ (n : ℕ), ediam (t n) ≤ r
⊢ ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ⨅ (_ : ediam (t n) ≤ r), m (ediam (t n)) =
    ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ r), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (ediam (t n))
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
f : U →ₗ[𝕜] V
g : V →ₗ[𝕜] W
hf : f.ker = ⊥
bu : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 U := stdOrthonormalBasis 𝕜 U
⊢ (g ∘ₗ f).normDet = (g.domRestrict f.range).normDet * f.normDet

Tactic:
obtain ⟨bv⟩ := (f.normDet_ne_zero_tfae.out 1 3).mp hf

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
f : U →ₗ[𝕜] V
g : V →ₗ[𝕜] W
hf : f.ker = ⊥
bu : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 U := stdOrthonormalBasis 𝕜 U
bv : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥f.range
⊢ (g ∘ₗ f).normDet = (g.domRestrict f.range).normDet * f.normDet
Module: Mathlib.Analysis.InnerProductSpace.NormDet

Goal state before:
pp: 𝕜 : 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
f : U →ₗ[𝕜] V
g : V →ₗ[𝕜] W
bu : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 U := stdOrthonormalBasis 𝕜 U
bv : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥f.range
hgf : ¬(g ∘ₗ f).ker = ⊥
hgf' : (g.domRestrict f.range).ker = ⊥
⊢ ¬f.rangeRestrict.ker = ⊥

Tactic:
← LinearMap.ker_comp_of_ker_eq_bot _ hgf'

Goal state after:
𝕜 : 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
f : U →ₗ[𝕜] V
g : V →ₗ[𝕜] W
bu : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 U := stdOrthonormalBasis 𝕜 U
bv : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥f.range
hgf : ¬(g ∘ₗ f).ker = ⊥
hgf' : (g.domRestrict f.range).ker = ⊥
⊢ ¬(g.domRestrict f.range ∘ₗ f.rangeRestrict).ker = ⊥