mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
T : L.Theory
φ : L.Sentence
⊢ (¬∀ (T0 : Finset L.Sentence), ↑T0 ⊆ T ∪ {Formula.not φ} → IsSatisfiable ↑T0) ↔
    ∃ T0, ↑T0 ⊆ T ∧ ¬(↑T0 ∪ {Formula.not φ}).IsSatisfiable

Tactic:
contrapose!

Goal state after:
L : Language
T : L.Theory
φ : L.Sentence
⊢ (∀ (T0 : Finset L.Sentence), ↑T0 ⊆ T ∪ {Formula.not φ} → IsSatisfiable ↑T0) ↔
    ∀ (T0 : Finset L.Sentence), ↑T0 ⊆ T → (↑T0 ∪ {Formula.not φ}).IsSatisfiable
Module: Mathlib.GroupTheory.OreLocalization.Cardinality

Goal state before:
pp: case inr
R : Type u
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type v
inst✝¹ : MulAction R X
inst✝ : Finite ↥S
x : X
s : ↥S
i j : ℕ
hne : i ≠ j
heq : s ^ i = s ^ j
this : ∀ (i j : ℕ), i ≠ j → s ^ i = s ^ j → j < i → ∃ a, (fun x ↦ x /ₒ 1) a = x /ₒ s
hlt : i ≤ j
⊢ ∃ a, (fun x ↦ x /ₒ 1) a = x /ₒ s

Tactic:
exact this j i hne.symm heq.symm (hne.lt_of_le hlt)

Goal state after:
Module: Mathlib.GroupTheory.OreLocalization.Cardinality

Goal state before:
pp: case inr
R : Type u
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type v
inst✝¹ : MulAction R X
inst✝ : Finite X
x : X
s : ↥S
i j : ℕ
hne : i ≠ j
heq : s ^ i • x = s ^ j • x
this : ∀ (i j : ℕ), i ≠ j → s ^ i • x = s ^ j • x → j < i → ∃ a, (fun x ↦ x /ₒ 1) a = x /ₒ s
hlt : i ≤ j
⊢ ∃ a, (fun x ↦ x /ₒ 1) a = x /ₒ s

Tactic:
exact this j i hne.symm heq.symm (hne.lt_of_le hlt)

Goal state after:
Module: Mathlib.FieldTheory.Differential.Basic

Goal state before:
pp: case succ.inr
R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
a : R
n : ℕ
h2 : logDeriv (a ^ n) = ↑n * logDeriv a
hb : a ≠ 0
⊢ logDeriv (a ^ (n + 1)) = ↑n * logDeriv a + logDeriv a

Tactic:
← h2,

Goal state after:
case succ.inr
R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
a : R
n : ℕ
h2 : logDeriv (a ^ n) = ↑n * logDeriv a
hb : a ≠ 0
⊢ logDeriv (a ^ (n + 1)) = logDeriv (a ^ n) + logDeriv a
Module: Mathlib.FieldTheory.Finite.Extension

Goal state before:
pp: k : Type u_1
inst✝⁶ : Field k
inst✝⁵ : Finite k
p : ℕ
inst✝⁴ : Fact (Nat.Prime p)
inst✝³ : CharP k p
n : ℕ
inst✝² : NeZero n
l : Type u_2
inst✝¹ : Field l
inst✝ : Algebra k l
h : Module.finrank k l = n
this✝¹ : Module.Finite k l
this✝ : Finite l
this : Fintype l
⊢ Nonempty (l ≃ₐ[k] Extension k p n)

Tactic:
have : IsSplittingField k l (X ^ Nat.card k ^ n - X) := by
    rw [← h, ← Module.natCard_eq_pow_finrank, ← Fintype.card_eq_nat_card]
    exact FiniteField.isSplittingField_sub l k

Goal state after:
k : Type u_1
inst✝⁶ : Field k
inst✝⁵ : Finite k
p : ℕ
inst✝⁴ : Fact (Nat.Prime p)
inst✝³ : CharP k p
n : ℕ
inst✝² : NeZero n
l : Type u_2
inst✝¹ : Field l
inst✝ : Algebra k l
h : Module.finrank k l = n
this✝² : Module.Finite k l
this✝¹ : Finite l
this✝ : Fintype l
this : IsSplittingField k l (X ^ Nat.card k ^ n - X)
⊢ Nonempty (l ≃ₐ[k] Extension k p n)
Module: Mathlib.Topology.Separation.Connected

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s : Set X
h : IsPreconnected s
hs : s.Nontrivial
⊢ s.Infinite

Tactic:
refine mt (fun hf => (subsingleton_coe s).mp ?_) (not_subsingleton_iff.mpr hs)
  have := @Finite.instDiscreteTopology s _ _ hf.to_subtype
  exact @PreconnectedSpace.trivial_of_discrete _ _ (Subtype.preconnectedSpace h) _

Goal state after:
Module: Mathlib.FieldTheory.CardinalEmb

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.ToType
ih : (y : (Module.rank F E).ord.ToType) → y < i → (Module.rank F E).ord.ToType
s : Set E := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ False

Tactic:
rw [adjoin_basis_eq_top, ← eq_top_iff] at this

Goal state after:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.ToType
ih : (y : (Module.rank F E).ord.ToType) → y < i → (Module.rank F E).ord.ToType
s : Set E := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this : adjoin F s = ⊤
⊢ False
Module: Mathlib.FieldTheory.CardinalEmb

Goal state before:
pp: case coe
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
i : WithTop (Module.rank F E).ord.ToType
a✝ : (Module.rank F E).ord.ToType
h : i < ↑a✝
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
obtain ⟨i, rfl⟩ := ne_top_iff_exists.mp (h.trans <| coe_lt_top _).ne

Goal state after:
case coe
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
a✝ i : (Module.rank F E).ord.ToType
h : ↑i < ↑a✝
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : CommSemiring K
inst✝¹ : CommSemiring L
i : K →+* L
p : ℕ
inst✝ : IsPRadical i p
⊢ Ideal.comap i (pNilradical L p) = pNilradical K p

Tactic:
refine le_antisymm (fun x h ↦ mem_pNilradical.2 ?_) (fun x h ↦ ?_)
  · obtain ⟨n, h⟩ := mem_pNilradical.1 <| Ideal.mem_comap.1 h
    obtain ⟨m, h⟩ := mem_pNilradical.1 <| ker_le i p ((map_pow i x _).symm ▸ h)
    exact ⟨n + m, by rwa [pow_add, pow_mul]⟩
  simp only [Ideal.mem_comap, mem_pNilradical] at h ⊢
  obtain ⟨n, h⟩ := h
  exact ⟨n, by simpa only [map_pow, map_zero] using congr(i $h)⟩

Goal state after:
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: K : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing K
inst✝⁵ : CommRing L
inst✝⁴ : CommRing M
i : K →+* L
j : K →+* M
p : ℕ
inst✝³ : ExpChar M p
inst✝² : ExpChar K p
inst✝¹ : PerfectRing M p
inst✝ : IsPRadical i p
x : L
n : ℕ
y : K
n' : ℕ := (Classical.choose ⋯).1
h' : i (Classical.choose ⋯).2 = x ^ p ^ n'
h : i ((Classical.choose ⋯).2 ^ p ^ n) = i (y ^ p ^ n')
⊢ (iterateFrobeniusEquiv M p n').symm (j (Classical.choose ⋯).2) = (iterateFrobeniusEquiv M p n).symm (j y)

Tactic:
← sub_eq_zero,

Goal state after:
K : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing K
inst✝⁵ : CommRing L
inst✝⁴ : CommRing M
i : K →+* L
j : K →+* M
p : ℕ
inst✝³ : ExpChar M p
inst✝² : ExpChar K p
inst✝¹ : PerfectRing M p
inst✝ : IsPRadical i p
x : L
n : ℕ
y : K
n' : ℕ := (Classical.choose ⋯).1
h' : i (Classical.choose ⋯).2 = x ^ p ^ n'
h : i ((Classical.choose ⋯).2 ^ p ^ n) - i (y ^ p ^ n') = 0
⊢ (iterateFrobeniusEquiv M p n').symm (j (Classical.choose ⋯).2) = (iterateFrobeniusEquiv M p n).symm (j y)
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: K : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing K
inst✝⁵ : CommRing L
inst✝⁴ : CommRing M
i : K →+* L
j : K →+* M
p : ℕ
inst✝³ : ExpChar M p
inst✝² : ExpChar K p
inst✝¹ : PerfectRing M p
inst✝ : IsPRadical i p
x : L
n : ℕ
y : K
n' : ℕ := (Classical.choose ⋯).1
h' : i (Classical.choose ⋯).2 = x ^ p ^ n'
h✝ : (Classical.choose ⋯).2 ^ p ^ n - y ^ p ^ n' ∈ RingHom.ker i
m : ℕ
h : ((Classical.choose ⋯).2 ^ p ^ n - y ^ p ^ n') ^ p ^ m = 0
⊢ j (Classical.choose ⋯).2 ^ p ^ (m + n) = j y ^ p ^ (m + n')

Tactic:
← sub_eq_zero,

Goal state after:
K : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing K
inst✝⁵ : CommRing L
inst✝⁴ : CommRing M
i : K →+* L
j : K →+* M
p : ℕ
inst✝³ : ExpChar M p
inst✝² : ExpChar K p
inst✝¹ : PerfectRing M p
inst✝ : IsPRadical i p
x : L
n : ℕ
y : K
n' : ℕ := (Classical.choose ⋯).1
h' : i (Classical.choose ⋯).2 = x ^ p ^ n'
h✝ : (Classical.choose ⋯).2 ^ p ^ n - y ^ p ^ n' ∈ RingHom.ker i
m : ℕ
h : ((Classical.choose ⋯).2 ^ p ^ n - y ^ p ^ n') ^ p ^ m = 0
⊢ j (Classical.choose ⋯).2 ^ p ^ (m + n) - j y ^ p ^ (m + n') = 0
Module: Mathlib.FieldTheory.IsRealClosed.Basic

Goal state before:
pp: case h.inl
R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
n : ℕ
ih : ∀ m < n, ∀ {x : R}, IsSquare x → m ≠ 0 → ∃ r, x = r ^ m
x : R
hx : IsSquare x
hn : n ≠ 0
even : Even n
⊢ ∃ r, x = r ^ n

Tactic:
rcases even with ⟨m, hm⟩

Goal state after:
case h.inl
R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
n : ℕ
ih : ∀ m < n, ∀ {x : R}, IsSquare x → m ≠ 0 → ∃ r, x = r ^ m
x : R
hx : IsSquare x
hn : n ≠ 0
m : ℕ
hm : n = m + m
⊢ ∃ r, x = r ^ n
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq (Subgroup G)
n : ℕ
ih :
  ∀ m < n,
    ∀ {ι : Type u_2} {H : ι → Subgroup G} {g : ι → G} {s : Finset ι},
      ⋃ i ∈ s, g i • ↑(H i) = Set.univ →
        ∀ j ∈ s,
          ⋃ i ∈ {x ∈ s | H x = H j}, g i • ↑(H i) ≠ Set.univ →
            m = (Finset.image H s).card → ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
j : ι
hj : j ∈ s
hcovers' : ⋃ i ∈ {x ∈ s | H x = H j}, g i • ↑(H i) ≠ Set.univ
hn : n = (Finset.image H s).card
x : G
hx : ∀ (y : G), y • ↑(H j) ⊆ ⋃ i ∈ {x ∈ s | H x ≠ H j}, (y * x⁻¹ * g i) • ↑(H i)
κ : Type u_2 := ↥({x ∈ s | H x ≠ H j}) × Option ↥({x ∈ s | H x = H j})
f : κ → G :=
  fun x_1 ↦
    match x_1 with
    | (k₁, some k₂) => g ↑k₂ * x⁻¹ * g ↑k₁
    | (k₁, none) => g ↑k₁
K : κ → Subgroup G := fun k ↦ H ↑k.1
hK' : ∀ (k : κ), K k ∈ (Finset.image H s).erase (H j)
hK : ∀ (k : κ), K k ≠ H j
y : G
⊢ ∃ i, ∃ (_ : i ∈ Finset.univ), y ∈ f i • ↑(K i)

Tactic:
rw [← s.filter_union_filter_not_eq (H · = H j), Finset.set_biUnion_union] at hcovers
      cases (Set.mem_union _ _ _).mp (hcovers.superset (Set.mem_univ y)) with
      | inl hy =>
        have ⟨k, hk, hy⟩ := Set.mem_iUnion₂.mp hy
        have hk' : H k = H j := And.right <| by simpa using hk
        have ⟨i, hi, hy⟩ := Set.mem_iUnion₂.mp (hx (g k) (hk' ▸ hy))
        exact ⟨⟨⟨i, hi⟩, some ⟨k, hk⟩⟩, Finset.mem_univ _, hy⟩
      | inr hy =>
        have ⟨i, hi, hy⟩ := Set.mem_iUnion₂.mp hy
        exact ⟨⟨⟨i, hi⟩, none⟩, Finset.mem_univ _, hy⟩

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial

Goal state before:
pp: K : Type v
inst✝¹ : CommRing K
inst✝ : Nontrivial K
σ : Type v
⊢ lift.{?u.17, v} (Module.rank K (MvPolynomial σ K)) = lift.{?u.17, v} #(σ →₀ ℕ)

Tactic:
← (basisMonomials σ K).mk_eq_rank

Goal state after:
K : Type v
inst✝¹ : CommRing K
inst✝ : Nontrivial K
σ : Type v
⊢ lift.{v, v} #(σ →₀ ℕ) = lift.{v, v} #(σ →₀ ℕ)
Module: Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality

Goal state before:
pp: case pos
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
A B : IntermediateField F E
hA : ¬Algebra.IsAlgebraic F ↥A
hB : Algebra.IsAlgebraic F ↥B
⊢ Module.rank F ↥(A ⊔ B) ≤ Module.rank F ↥A * Module.rank F ↥B

Tactic:
exact rank_sup_le_of_isAlgebraic A B (Or.inr hB)

Goal state after:
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: case neg
K : Type u
inst✝ : Field K
n : ℕ
hζ✝ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
this✝ : Fact (Irreducible (X ^ n - C a)) := { out := H }
this : Algebra K K[n√a] := inferInstance
hn : 0 < n
hn' : ¬n = 1
ζ : K
hζ : IsPrimitiveRoot ζ n
⊢ (X ^ n - C ((algebraMap K K[n√a]) a)).Separable

Tactic:
AdjoinRoot.algebraMap_eq,

Goal state after:
case neg
K : Type u
inst✝ : Field K
n : ℕ
hζ✝ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
this✝ : Fact (Irreducible (X ^ n - C a)) := { out := H }
this : Algebra K K[n√a] := inferInstance
hn : 0 < n
hn' : ¬n = 1
ζ : K
hζ : IsPrimitiveRoot ζ n
⊢ (X ^ n - C ((of (X ^ n - C a)) a)).Separable
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: K : Type u
inst✝ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
η : ↥(rootsOfUnity n K)
this : ↑↑η ^ n = 1
⊢ (algebraMap K K[n√a]) ↑↑η ^ n * (of (X ^ n - C a)) a - (algebraMap K K[n√a]) a = 0

Tactic:
AdjoinRoot.algebraMap_eq,

Goal state after:
K : Type u
inst✝ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
η : ↥(rootsOfUnity n K)
this : ↑↑η ^ n = 1
⊢ (of (X ^ n - C a)) ↑↑η ^ n * (of (X ^ n - C a)) a - (of (X ^ n - C a)) a = 0
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: case adjoin_rootSet'
K : Type u
inst✝ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
this✝¹ : Fact (Irreducible (X ^ n - C a))
this✝ : Algebra K K[n√a] := inferInstance
this : n ≠ 0
⊢ eval₂ (algebraMap K K[n√a]) (root (X ^ n - C a)) (X ^ n - C a) = 0

Tactic:
AdjoinRoot.algebraMap_eq,

Goal state after:
case adjoin_rootSet'
K : Type u
inst✝ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
this✝¹ : Fact (Irreducible (X ^ n - C a))
this✝ : Algebra K K[n√a] := inferInstance
this : n ≠ 0
⊢ eval₂ (of (X ^ n - C a)) (root (X ^ n - C a)) (X ^ n - C a) = 0
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
A B : Subalgebra R S
ι : Type u_1
b : ι → ↥B
⊢ Function.Injective ⇑((toSubmodule A).mulRightMap b) ↔
    Function.Injective ⇑(Finsupp.linearCombination (↥A) (⇑B.val ∘ b))

Tactic:
let i : (ι →₀ A) →ₗ[R] S := Submodule.mulRightMap (toSubmodule A) (N := toSubmodule B) b

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
A B : Subalgebra R S
ι : Type u_1
b : ι → ↥B
i : (ι →₀ ↥A) →ₗ[R] S := (toSubmodule A).mulRightMap b
⊢ Function.Injective ⇑((toSubmodule A).mulRightMap b) ↔
    Function.Injective ⇑(Finsupp.linearCombination (↥A) (⇑B.val ∘ b))
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
A B : Subalgebra R S
ι : Type u_1
b : ι → ↥B
⊢ ((toSubmodule A).mulRightMap b).ker = ⊥ ↔ LinearIndependent (↥A) (⇑B.val ∘ b)

Tactic:
by
  simp_rw [LinearIndependent, LinearMap.ker_eq_bot]
  let i : (ι →₀ A) →ₗ[R] S := Submodule.mulRightMap (toSubmodule A) (N := toSubmodule B) b
  let j : (ι →₀ A) →ₗ[R] S := (Finsupp.linearCombination A (B.val ∘ b)).restrictScalars R
  suffices i = j by change Function.Injective i ↔ Function.Injective j; rw [this]
  ext
  simp only [LinearMap.coe_comp, Function.comp_apply, Finsupp.lsingle_apply, coe_val,
    LinearMap.coe_restrictScalars, Finsupp.linearCombination_single, i, j]
  exact Submodule.mulRightMap_apply_single _ _ _

Goal state after:
Module: Mathlib.FieldTheory.NormalizedTrace

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
a : F
⊢ (normalizedTrace F F) a = a

Tactic:
dsimp [normalizedTrace]
  rw [normalizedTraceAux_eq_of_finiteDimensional F a, Module.finrank_self F,
    Nat.cast_one, inv_one, one_smul, trace_self_apply]

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.Exponent

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsPurelyInseparable K L
a : L
⊢ (X ^ ringExpChar K ^ elemExponent K a - C (elemReduct K a)).natDegree = ringExpChar K ^ elemExponent K a

Tactic:
natDegree_sub_C,

Goal state after:
K : Type u_2
L : Type u_3
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsPurelyInseparable K L
a : L
⊢ (X ^ ringExpChar K ^ elemExponent K a).natDegree = ringExpChar K ^ elemExponent K a
Module: Mathlib.FieldTheory.PurelyInseparable.Exponent

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsPurelyInseparable K L
a : L
n : ℕ
h : a ^ ringExpChar K ^ n ∈ (algebraMap K L).range
p : ℕ
h✝ : ExpChar K p
hp : Nat.Prime p
hchar✝ : CharP K p
y : K
hy : (algebraMap K L) y = a ^ ringExpChar K ^ n
f : K[X] := X ^ ringExpChar K ^ n - C y
hf₁ : (aeval a) f = 0
hf₂ : f.Monic
⊢ f.natDegree = ringExpChar K ^ n

Tactic:
natDegree_sub_C,

Goal state after:
K : Type u_2
L : Type u_3
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsPurelyInseparable K L
a : L
n : ℕ
h : a ^ ringExpChar K ^ n ∈ (algebraMap K L).range
p : ℕ
h✝ : ExpChar K p
hp : Nat.Prime p
hchar✝ : CharP K p
y : K
hy : (algebraMap K L) y = a ^ ringExpChar K ^ n
f : K[X] := X ^ ringExpChar K ^ n - C y
hf₁ : (aeval a) f = 0
hf₂ : f.Monic
⊢ (X ^ ringExpChar K ^ n).natDegree = ringExpChar K ^ n
Module: Mathlib.FieldTheory.PurelyInseparable.Exponent

Goal state before:
pp: F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra K L
inst✝⁶ : HasExponent K L
p : ℕ
inst✝⁵ : ExpChar K p
inst✝⁴ : Field F
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : IsScalarTower F K L
inst✝ : ExpChar F p
n : ℕ
hn : exponent K L ≤ n
r : F
a : L
⊢ IsPurelyInseparable.iterateFrobeniusAux✝ K L p n (r • a) =
    (_root_.iterateFrobenius F p n) r • IsPurelyInseparable.iterateFrobeniusAux✝ K L p n a

Tactic:
rw [Algebra.smul_def _ (iterateFrobeniusAux K L p n a)]

Goal state after:
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra K L
inst✝⁶ : HasExponent K L
p : ℕ
inst✝⁵ : ExpChar K p
inst✝⁴ : Field F
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : IsScalarTower F K L
inst✝ : ExpChar F p
n : ℕ
hn : exponent K L ≤ n
r : F
a : L
⊢ IsPurelyInseparable.iterateFrobeniusAux✝ K L p n (r • a) =
    (algebraMap F K) ((_root_.iterateFrobenius F p n) r) * IsPurelyInseparable.iterateFrobeniusAux✝ K L p n a
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
A B : Subalgebra R S
inst✝³ : Free R ↥A
inst✝² : Free R ↥B
inst✝¹ : Module.Finite R ↥A
inst✝ : Module.Finite R ↥B
H : finrank R ↥(A ⊔ B) = finrank R (↥A ⊗[R] ↥B)
a✝ : Nontrivial R
j : Fin (finrank R (↥A ⊗[R] ↥B)) → ↥(A ⊔ B)
hj : Function.Injective ⇑(Finsupp.linearCombination R j)
⊢ A.LinearDisjoint B

Tactic:
let j' := Finsupp.linearCombination R j ∘ₗ
    (LinearEquiv.ofFinrankEq (A ⊗[R] B) _ (by simp)).toLinearMap

Goal state after:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
A B : Subalgebra R S
inst✝³ : Free R ↥A
inst✝² : Free R ↥B
inst✝¹ : Module.Finite R ↥A
inst✝ : Module.Finite R ↥B
H : finrank R ↥(A ⊔ B) = finrank R (↥A ⊗[R] ↥B)
a✝ : Nontrivial R
j : Fin (finrank R (↥A ⊗[R] ↥B)) → ↥(A ⊔ B)
hj : Function.Injective ⇑(Finsupp.linearCombination R j)
j' : ↥A ⊗[R] ↥B →ₗ[R] ↥(A ⊔ B) :=
  Finsupp.linearCombination R j ∘ₗ ↑(LinearEquiv.ofFinrankEq (↥A ⊗[R] ↥B) (Fin (finrank R (↥A ⊗[R] ↥B)) →₀ R) ⋯)
⊢ A.LinearDisjoint B
Module: Mathlib.FieldTheory.PurelyInseparable.Tower

Goal state before:
pp: F : Type u
E : Type v
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Algebra F E
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : Algebra.IsSeparable F E
⊢ Module.rank F E * sepDegree E K = sepDegree F K

Tactic:
simpa only [Cardinal.lift_id] using lift_rank_mul_lift_sepDegree_of_isSeparable F E K

Goal state after:
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: case e_6
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
A B : Subalgebra R S
inst✝ : Algebra.IsIntegral R ↥A
H : ∀ A' ≤ A, ∀ [Module.Finite R ↥A'], A'.LinearDisjoint B
x y : ↥(toSubmodule A) ⊗[R] ↥(toSubmodule B)
hxy : ((toSubmodule A).mulMap (toSubmodule B)) x = ((toSubmodule A).mulMap (toSubmodule B)) y
M' : Submodule R S
hM : M' ≤ toSubmodule A
hf : Module.Finite R ↥M'
s : Finset S
hs : Submodule.span R ↑s = M'
hs' : ↑s ⊆ ↑A
A' : Subalgebra R S := ⋯
hf' : Module.Finite R ↥A'
hA : toSubmodule A' ≤ toSubmodule A
h : {x, y} ⊆ ↑(LinearMap.rTensor (↥(toSubmodule B)) (Submodule.inclusion hA)).range
x' : ↥(toSubmodule A') ⊗[R] ↥(toSubmodule B)
hx' : (LinearMap.rTensor (↥(toSubmodule B)) (Submodule.inclusion hA)) x' = x
y' : ↥(toSubmodule A') ⊗[R] ↥(toSubmodule B)
hy' : (LinearMap.rTensor (↥(toSubmodule B)) (Submodule.inclusion hA)) y' = y
⊢ x' = y'

Tactic:
exact (H A' hA).injective (by simp [← Submodule.mulMap_comp_rTensor _ hA, hx', hy', hxy])

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.IntermediateField

Goal state before:
pp: case neg
K : Type u_1
inst✝ : Field K
f : K⟮X⟯
hf : ¬∃ c, f = C c
⊢ (Polynomial.C (f.minpolyX ↥K⟮f⟯).leadingCoeff⁻¹ * f.minpolyX ↥K⟮f⟯).natDegree = max f.num.natDegree f.denom.natDegree

Tactic:
natDegree_C_mul <| inv_ne_zero <| leadingCoeff_ne_zero.mpr fun H ↦
    hf ((minpolyX_eq_zero_iff f).mp H),

Goal state after:
case neg
K : Type u_1
inst✝ : Field K
f : K⟮X⟯
hf : ¬∃ c, f = C c
⊢ (f.minpolyX ↥K⟮f⟯).natDegree = max f.num.natDegree f.denom.natDegree
Module: Mathlib.Geometry.Convex.Cone.DualFinite

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsOrderedRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : M →ₗ[R] N →ₗ[R] R
C D : PointedCone R N
hC : DualFG p C
hD : DualFG p D
⊢ DualFG p (C ⊓ D)

Tactic:
obtain ⟨S, rfl⟩ := hC; obtain ⟨T, rfl⟩ := hD
  use S ∪ T; rw [Finset.coe_union, dual_union]

Goal state after:
Module: Mathlib.Geometry.Convex.Hull

Goal state before:
pp: R : Type u_1
X : Type u_2
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R X
s : Set X
x : X
hs : (convexHull R) s = {x}
⊢ s = {x}

Tactic:
rw [← Set.Nonempty.subset_singleton_iff, ← hs]

Goal state after:
R : Type u_1
X : Type u_2
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R X
s : Set X
x : X
hs : (convexHull R) s = {x}
⊢ s ⊆ (convexHull R) s

R : Type u_1
X : Type u_2
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R X
s : Set X
x : X
hs : (convexHull R) s = {x}
⊢ s.Nonempty
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation

Goal state before:
pp: V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
⊢ ∀ (x y : V),
    ⟪(θ.cos • LinearMap.id + θ.sin • ↑o.rightAngleRotation.toLinearEquiv) x,
        (θ.cos • LinearMap.id + θ.sin • ↑o.rightAngleRotation.toLinearEquiv) y⟫ =
      ⟪x, y⟫

Tactic:
by
      intro x y
      simp only [RCLike.conj_to_real, id, LinearMap.smul_apply, LinearMap.add_apply,
        LinearMap.id_coe, LinearEquiv.coe_coe, LinearIsometryEquiv.coe_toLinearEquiv,
        Orientation.areaForm_rightAngleRotation_left, Orientation.inner_rightAngleRotation_left,
        Orientation.inner_rightAngleRotation_right, inner_add_left, inner_smul_left,
        inner_add_right, inner_smul_right]
      linear_combination ⟪x, y⟫ * θ.cos_sq_add_sin_sq

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

Goal state before:
pp: V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
⊢ o.oangle x y + o.oangle y x = 0

Tactic:
by
  simp [o.oangle_rev y x]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Altitude

Goal state before:
pp: case «1»
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Simplex ℝ P 1
⊢ s.height ((fun i ↦ i) ⟨1, ⋯⟩) = dist (s.points 0) (s.points 1)

Tactic:
· rw [dist_comm]
    simp [height]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

Goal state before:
pp: V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
r₁ r₂ : ℝ
hr₁ : 0 ≤ r₁
hr₂ : 0 ≤ r₂
⊢ o.oangle (r₁ • x) (r₂ • x) = 0

Tactic:
rcases hr₁.lt_or_eq with (h | h)
  · simp [h, hr₂]
  · simp [h.symm]

Goal state after: