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

Goal state before:
pp: L : Language
T : L.Theory
h : T.IsFinitelySatisfiable
M : Finset ↑T → Type (max u v) := fun T0 ↦ ↑(Nonempty.some ⋯)
M' : Type (max u v) := (↑(Ultrafilter.of Filter.atTop)).Product M
φ : L.Sentence
hφ : φ ∈ T
⊢ ∀ᶠ (a : Finset ↑T) in ↑(Ultrafilter.of Filter.atTop), M a ⊨ φ

Tactic:
refine
        Filter.Eventually.filter_mono (Ultrafilter.of_le _)
          (Filter.eventually_atTop.2
            ⟨{⟨φ, hφ⟩}, fun s h' =>
              Theory.realize_sentence_of_mem (s.map (Function.Embedding.subtype fun x => x ∈ T))
                ?_⟩)

Goal state after:
L : Language
T : L.Theory
h : T.IsFinitelySatisfiable
M : Finset ↑T → Type (max u v) := fun T0 ↦ ↑(Nonempty.some ⋯)
M' : Type (max u v) := (↑(Ultrafilter.of Filter.atTop)).Product M
φ : L.Sentence
hφ : φ ∈ T
s : Finset ↑T
h' : {⟨φ, hφ⟩} ⊆ s
⊢ φ ∈ ↑(Finset.map (Function.Embedding.subtype fun x ↦ x ∈ T) s)
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
T : L.Theory
φ : L.Sentence
M : Type u_1
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
h : ¬M ⊨ φ
⊢ M ⊨ T ∪ {Formula.not φ}

Tactic:
simp only [Set.union_singleton, model_iff, Set.mem_insert_iff, forall_eq_or_imp,
      Sentence.realize_not]

Goal state after:
L : Language
T : L.Theory
φ : L.Sentence
M : Type u_1
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
h : ¬M ⊨ φ
⊢ ¬M ⊨ φ ∧ ∀ a ∈ T, M ⊨ a
Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed

Goal state before:
pp: case inr
φ : Language.ring.Sentence
T0 : Finset Language.ring.Sentence
hT0 : ↑T0 ⊆ Theory.ACF 0
h : ↑T0 ⊨ᵇ φ
p : ℕ
hp : p ∈ {q | Nat.Prime q}
⊢ ∀ q ∉ {⟨p, hp⟩}, Theory.ACF ↑q ⊨ᵇ ∼(eqZero p)

Tactic:
rintro ⟨q, _⟩ hq ⟨K⟩ _ _

Goal state after:
case inr
φ : Language.ring.Sentence
T0 : Finset Language.ring.Sentence
hT0 : ↑T0 ⊆ Theory.ACF 0
h : ↑T0 ⊨ᵇ φ
p : ℕ
hp : p ∈ {q | Nat.Prime q}
q : ℕ
property✝ : Nat.Prime q
hq : ⟨q, property✝⟩ ∉ {⟨p, hp⟩}
K : Type
struc✝ : Language.ring.Structure K
is_model✝ : K ⊨ Theory.ACF ↑⟨q, property✝⟩
nonempty'✝ : Nonempty K
v✝ : Empty → ↑{ Carrier := K, struc := struc✝, is_model := is_model✝, nonempty' := nonempty'✝ }
xs✝ : Fin 0 → ↑{ Carrier := K, struc := struc✝, is_model := is_model✝, nonempty' := nonempty'✝ }
⊢ (∼(eqZero p)).Realize v✝ xs✝
Module: Mathlib.RingTheory.Nullstellensatz

Goal state before:
pp: case e'_3
k : Type u_1
K : Type u_2
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
σ : Type u_3
x : σ → K
e_2✝ : AddMonoidAlgebra.semiring = AddMonoidAlgebra.ring.toSemiring
⊢ vanishingIdeal K {x} = RingHom.ker (aeval x)

Tactic:
ext; simp

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
T : L.Theory
h : T.IsMaximal
φ : L.Sentence
hφ : ¬IsSatisfiable (insert (Formula.not φ) T)
con : Formula.not φ ∈ T
⊢ False

Tactic:
Set.insert_eq_of_mem con

Goal state after:
L : Language
T : L.Theory
h : T.IsMaximal
φ : L.Sentence
hφ : ¬T.IsSatisfiable
con : Formula.not φ ∈ T
⊢ False
Module: Mathlib.LinearAlgebra.FreeAlgebra

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : Set S
⊢ Module.rank R ↥(adjoin R s) ≤ max #↑s ℵ₀

Tactic:
adjoin_eq_range_freeAlgebra_lift

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : Set S
⊢ Module.rank R ↥((FreeAlgebra.lift R) Subtype.val).range ≤ max #↑s ℵ₀
Module: Mathlib.SetTheory.Cardinal.Divisibility

Goal state before:
pp: case refine_1
a : Cardinal.{u}
ha : ℵ₀ ≤ a
⊢ ¬IsUnit a

Tactic:
rw [isUnit_iff]

Goal state after:
case refine_1
a : Cardinal.{u}
ha : ℵ₀ ≤ a
⊢ ¬a = 1
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
g : Gal(Extension k p n/k)
⊢ ∃ i < n, frob k p n ^ i = g

Tactic:
by
  let := Fintype.ofFinite k
  obtain ⟨⟨i, hi⟩, rfl⟩ := (FiniteField.bijective_frobeniusAlgEquivOfAlgebraic_pow k
    (Extension k p n)).2 g
  refine ⟨i, ?_, by ext; simp [frob]⟩
  rwa [finrank_extension] at hi

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

Goal state before:
pp: k : Type u_1
inst✝¹ : Field k
inst✝ : Finite k
f : k[X]
hi : Irreducible f
n : ℕ
hdvd : f.natDegree ∣ n
a : AdjoinRoot f := AdjoinRoot.root f
this✝² : NeZero f.natDegree
this✝¹ : Fact (Irreducible f)
p : ℕ
hp : CharP k p
this✝ : Fact (Nat.Prime p)
e : AdjoinRoot f ≃ₐ[k] Extension k p f.natDegree := algEquivExtension k p f.natDegree (AdjoinRoot f) ⋯
this : Fintype (Extension k p f.natDegree)
⊢ e a ^ Nat.card k ^ f.natDegree - e a = 0

Tactic:
rw [← (natCard_extension k p f.natDegree), ← Fintype.card_eq_nat_card,
      pow_card (e a), sub_self]

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

Goal state before:
pp: k : Type u_1
inst✝¹ : Field k
inst✝ : Finite k
f : k[X]
hi : Irreducible f
n : ℕ
⊢ f.natDegree ∣ n ↔ f ∣ X ^ Nat.card k ^ n - X

Tactic:
by
  refine ⟨fun hdvd ↦ dvd_trans ?_ (dvd_pow_pow_sub_self_of_dvd hdvd),
    hi.natDegree_dvd_of_dvd_X_pow_card_pow_sub_X⟩
  let a := AdjoinRoot.root f
  have : NeZero f.natDegree := NeZero.of_pos (Irreducible.natDegree_pos hi)
  have : Fact <| Irreducible f := ⟨hi⟩
  rw [← hi.dvd_iff_aeval_eq_zero (b := a) (by aesop)]
  let ⟨p, hp⟩ := CharP.exists k
  have : Fact (Nat.Prime p) := ⟨CharP.char_is_prime k p⟩
  let e := FiniteField.algEquivExtension k p f.natDegree (AdjoinRoot f)
    (finrank_quotient_span_eq_natDegree (f := f))
  have hpeval : (e a) ^ (Nat.card k) ^ f.natDegree - (e a) = 0 := by
    have := Fintype.ofFinite (Extension k p f.natDegree)
    rw [← (natCard_extension k p f.natDegree), ← Fintype.card_eq_nat_card,
      pow_card (e a), sub_self]
  apply_fun e.symm at hpeval
  simpa using hpeval

Goal state after:
Module: Mathlib.FieldTheory.Galois.NormalBasis

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : Infinite K
⊢ ∃ x, LinearIndependent K fun σ ↦ σ x

Tactic:
have e := Module.Free.chooseBasis K L

Goal state after:
K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : Infinite K
e : Module.Basis (Module.Free.ChooseBasisIndex K L) K L
⊢ ∃ x, LinearIndependent K fun σ ↦ σ x
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing K
inst✝⁷ : CommRing L
inst✝⁶ : CommRing M
inst✝⁵ : CommRing N
i : K →+* L
j : K →+* M
k : K →+* N
f : L →+* M
g : L →+* N
p : ℕ
inst✝⁴ : ExpChar M p
inst✝³ : ExpChar K p
inst✝² : PerfectRing M p
inst✝¹ : IsPRadical i p
inst✝ : ExpChar L p
⊢ i 1 = 1

Tactic:
map_one

Goal state after:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing K
inst✝⁷ : CommRing L
inst✝⁶ : CommRing M
inst✝⁵ : CommRing N
i : K →+* L
j : K →+* M
k : K →+* N
f : L →+* M
g : L →+* N
p : ℕ
inst✝⁴ : ExpChar M p
inst✝³ : ExpChar K p
inst✝² : PerfectRing M p
inst✝¹ : IsPRadical i p
inst✝ : ExpChar L p
⊢ 1 = 1
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : ℕ × K
⊢ (iterateFrobenius K p (x.1 + 0)) 1 = (iterateFrobenius K p (0 + 0)) 1

Tactic:
map_one

Goal state after:
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝¹¹ : CommRing K
inst✝¹⁰ : CommRing L
inst✝⁹ : CommRing M
inst✝⁸ : CommRing N
i : K →+* L
j : K →+* M
k : K →+* N
p : ℕ
inst✝⁷ : ExpChar M p
inst✝⁶ : ExpChar K p
inst✝⁵ : PerfectRing M p
inst✝⁴ : IsPRadical i p
inst✝³ : ExpChar L p
inst✝² : ExpChar N p
inst✝¹ : PerfectRing N p
inst✝ : IsPRadical j p
⊢ (fun f ↦ f.comp i) ((lift j k p).comp (lift i j p)) = (fun f ↦ f.comp i) (lift i k p)

Tactic:
ext; simp

Goal state after:
Module: Mathlib.FieldTheory.Laurent

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
r : R
p : R[X]
inst✝ : IsDomain R
⊢ (algebraMap R[X] R⟮X⟯) ((taylor r) p) / (algebraMap R[X] R⟮X⟯) 1 =
    (algebraMap R[X] R⟮X⟯) ((taylor r) p) / (algebraMap R[X] R⟮X⟯) 1

Tactic:
map_one

Goal state after:
R : Type u
inst✝¹ : CommRing R
r : R
p : R[X]
inst✝ : IsDomain R
⊢ (algebraMap R[X] R⟮X⟯) ((taylor r) p) / 1 = (algebraMap R[X] R⟮X⟯) ((taylor r) p) / 1
Module: Mathlib.FieldTheory.JacobsonNoether

Goal state before:
pp: D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Algebra.IsAlgebraic (↥k) D
p : ℕ
hchar : ExpChar D p
a : D
ha : a ∉ k
hinsep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
m : ℕ
hm : 1 ≤ m ∧ a ^ p ^ m ∈ k
n : ℕ
hn : p ^ m ≤ n
inter : (⇑((ad (↥k) D) a))^[p ^ m] = 0
⊢ Function.const D ((⇑((ad (↥k) D) a))^[n - p ^ m] 0) = 0

Tactic:
iterate_map_zero,

Goal state after:
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Algebra.IsAlgebraic (↥k) D
p : ℕ
hchar : ExpChar D p
a : D
ha : a ∉ k
hinsep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
m : ℕ
hm : 1 ≤ m ∧ a ^ p ^ m ∈ k
n : ℕ
hn : p ^ m ≤ n
inter : (⇑((ad (↥k) D) a))^[p ^ m] = 0
⊢ Function.const D 0 = 0
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
inst✝ : DecidablePred FiniteIndex
D : Subgroup G := ⨅ k ∈ {i ∈ s | (H i).FiniteIndex}, H k
hD : D.FiniteIndex
hD_le : ∀ {i : ι}, i ∈ s → (H i).FiniteIndex → D ≤ H i
t : (i : ι) → i ∈ s → (H i).FiniteIndex → Finset ↥(H i)
ht :
  ∀ (i : ι) (hi : i ∈ s) (hfi : (H i).FiniteIndex),
    IsComplement ↑(t i hi hfi) ↑(D.subgroupOf (H i)) ∧ ⋃ g ∈ t i hi hfi, ↑g • ↑D = ↑(H i)
κ : Type (max u_2 u_1) := (i : ↥s) × ↥(if h : (H ↑i).FiniteIndex then t ↑i ⋯ h else {1})
f : κ → G := fun k ↦ g ↑k.fst * ↑↑k.snd
K : κ → Subgroup G := fun k ↦ if (H ↑k.fst).FiniteIndex then D else H ↑k.fst
hcovers' : ⋃ k ∈ Finset.univ, f k • ↑(K k) = Set.univ
k : κ
hkfi : (H ↑k.fst).FiniteIndex
hk : K k = D
⊢ ⋃ i ∈ {x | K x = D}, f i • ↑D = Set.univ

Tactic:
rw [← hk, Set.iUnion₂_congr fun i hi => by rw [← (Finset.mem_filter.mp hi).2]]

Goal state after:
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
inst✝ : DecidablePred FiniteIndex
D : Subgroup G := ⨅ k ∈ {i ∈ s | (H i).FiniteIndex}, H k
hD : D.FiniteIndex
hD_le : ∀ {i : ι}, i ∈ s → (H i).FiniteIndex → D ≤ H i
t : (i : ι) → i ∈ s → (H i).FiniteIndex → Finset ↥(H i)
ht :
  ∀ (i : ι) (hi : i ∈ s) (hfi : (H i).FiniteIndex),
    IsComplement ↑(t i hi hfi) ↑(D.subgroupOf (H i)) ∧ ⋃ g ∈ t i hi hfi, ↑g • ↑D = ↑(H i)
κ : Type (max u_2 u_1) := (i : ↥s) × ↥(if h : (H ↑i).FiniteIndex then t ↑i ⋯ h else {1})
f : κ → G := fun k ↦ g ↑k.fst * ↑↑k.snd
K : κ → Subgroup G := fun k ↦ if (H ↑k.fst).FiniteIndex then D else H ↑k.fst
hcovers' : ⋃ k ∈ Finset.univ, f k • ↑(K k) = Set.univ
k : κ
hkfi : (H ↑k.fst).FiniteIndex
hk : K k = D
⊢ ⋃ i ∈ {x | K x = K k}, f i • ↑(K i) = Set.univ
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)
inst✝ : NeZero n
⊢ Function.RightInverse (AdjoinRootXPowSubCEquivToRootsOfUnity hζ H) (↑(autAdjoinRootXPowSubC n a)).toFun

Tactic:
intro e

Goal state after:
K : Type u
inst✝¹ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
inst✝ : NeZero n
e : K[n√a] ≃ₐ[K] K[n√a]
⊢ (↑(autAdjoinRootXPowSubC n a)).toFun (AdjoinRootXPowSubCEquivToRootsOfUnity hζ H e) = e
Module: Mathlib.RingTheory.TensorProduct.Nontrivial

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
ha : Function.Injective ⇑(algebraMap R A)
hb : Function.Injective ⇑(algebraMap R B)
inst✝¹ : IsDomain A
inst✝ : IsDomain B
this : IsDomain R
FR : Type u_1 := FractionRing R
FA : Type u_2 := FractionRing A
FB : Type u_3 := FractionRing B
fa : FR →ₐ[R] FA := IsFractionRing.liftAlgHom ⋯
⊢ Nontrivial (A ⊗[R] B)

Tactic:
let fb : FR →ₐ[R] FB := IsFractionRing.liftAlgHom (g := Algebra.ofId R FB)
    ((IsFractionRing.injective B FB).comp hb)

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
ha : Function.Injective ⇑(algebraMap R A)
hb : Function.Injective ⇑(algebraMap R B)
inst✝¹ : IsDomain A
inst✝ : IsDomain B
this : IsDomain R
FR : Type u_1 := FractionRing R
FA : Type u_2 := FractionRing A
FB : Type u_3 := FractionRing B
fa : FR →ₐ[R] FA := IsFractionRing.liftAlgHom ⋯
fb : FR →ₐ[R] FB := IsFractionRing.liftAlgHom ⋯
⊢ Nontrivial (A ⊗[R] B)
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: case refine_1
K : Type u
inst✝⁵ : Field K
L : Type u_1
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
inst✝¹ : IsGalois K L
inst✝ : IsCyclic Gal(L/K)
ζ : K
hζ : IsPrimitiveRoot ζ (finrank K L)
σ : Gal(L/K)
hσ : Function.Surjective fun x ↦ σ ^ x
hσ'✝ : orderOf σ = Nat.card Gal(L/K)
this : (minpoly K σ.toLinearMap).IsRoot ζ
v : L
hv : End.HasEigenvector σ.toLinearMap ζ v
hv' : ∀ (n : ℕ), (σ ^ n) v = ζ ^ n • v
n : ℕ
hσ' : σ ^ n ∈ OrderDual.ofDual ⊥
⊢ (↑⟨σ ^ n, hσ'⟩ • v) ^ finrank K L = v ^ finrank K L

Tactic:
AlgEquiv.smul_def,

Goal state after:
case refine_1
K : Type u
inst✝⁵ : Field K
L : Type u_1
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
inst✝¹ : IsGalois K L
inst✝ : IsCyclic Gal(L/K)
ζ : K
hζ : IsPrimitiveRoot ζ (finrank K L)
σ : Gal(L/K)
hσ : Function.Surjective fun x ↦ σ ^ x
hσ'✝ : orderOf σ = Nat.card Gal(L/K)
this : (minpoly K σ.toLinearMap).IsRoot ζ
v : L
hv : End.HasEigenvector σ.toLinearMap ζ v
hv' : ∀ (n : ℕ), (σ ^ n) v = ζ ^ n • v
n : ℕ
hσ' : σ ^ n ∈ OrderDual.ofDual ⊥
⊢ ↑⟨σ ^ n, hσ'⟩ v ^ finrank K L = v ^ finrank K L
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
a : Basis ι R ↥A
H : LinearIndependent (↥B.op) (MulOpposite.op ∘ ⇑A.val ∘ ⇑a)
⊢ A.LinearDisjoint B

Tactic:
rw [← mulLeftMap_ker_eq_bot_iff_linearIndependent_op] at H
  exact Submodule.LinearDisjoint.of_basis_left _ _ a H

Goal state after:
Module: Mathlib.FieldTheory.LinearDisjoint

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
A B : IntermediateField F E
inst✝ : Module.Finite F ↥A
h₁ : A.LinearDisjoint ↥B
h₂ : A ⊔ B = ⊤
this : finrank F ↥A * finrank (↥A) E = finrank F ↥A * finrank F ↥B
⊢ finrank (↥A) E = finrank F ↥B

Tactic:
mul_right_inj' finrank_pos.ne'

Goal state after:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
A B : IntermediateField F E
inst✝ : Module.Finite F ↥A
h₁ : A.LinearDisjoint ↥B
h₂ : A ⊔ B = ⊤
this : finrank (↥A) E = finrank F ↥B
⊢ finrank (↥A) E = finrank F ↥B
Module: Mathlib.FieldTheory.LinearDisjoint

Goal state before:
pp: F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
A B : IntermediateField F E
inst✝¹ : IsGalois F ↥A
inst✝ : FiniteDimensional F E
h₁ : A ⊔ B = ⊤
h₂ : A ⊓ B = ⊥
⊢ A.LinearDisjoint ↥B

Tactic:
apply LinearDisjoint.of_finrank_sup
  rw [h₁, finrank_top', ← Module.finrank_mul_finrank F B E, mul_comm, mul_left_inj'
    Module.finrank_pos.ne']
  have : IsGalois B E := IsGalois.sup_right A B h₁
  rw [← IsGalois.card_aut_eq_finrank, ← IsGalois.card_aut_eq_finrank]
  exact Nat.card_congr <| Equiv.ofBijective (restrictRestrictAlgEquivMapHom _ _ _ _)
    ⟨restrictRestrictAlgEquivMapHom_injective _ _ h₁,
      restrictRestrictAlgEquivMapHom_surjective _ _ h₂⟩

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

Goal state before:
pp: case pos
F : Type u
E : Type v
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Algebra F E
K : Type w
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : IsPurelyInseparable F E
ι : Type u_1
v : ι → K
hsep : ∀ (i : ι), IsSeparable F (v i)
h : LinearIndependent F v
q : ℕ
h✝ : ExpChar F q
this✝ : ExpChar K q
l : ι →₀ E
hl : (Finsupp.linearCombination E v) l = 0
i✝ : ι
f : ι → ℕ
hf : ∀ (i : ι), l i ^ q ^ f i ∈ (algebraMap F E).range
n : ℕ := l.support.sup f
this : q ^ n ≠ 0
i : ι
hs : i ∈ l.support
⊢ l i ^ q ^ n ∈ (algebraMap F E).range

pp: case neg
F : Type u
E : Type v
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Algebra F E
K : Type w
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : IsPurelyInseparable F E
ι : Type u_1
v : ι → K
hsep : ∀ (i : ι), IsSeparable F (v i)
h : LinearIndependent F v
q : ℕ
h✝ : ExpChar F q
this✝ : ExpChar K q
l : ι →₀ E
hl : (Finsupp.linearCombination E v) l = 0
i✝ : ι
f : ι → ℕ
hf : ∀ (i : ι), l i ^ q ^ f i ∈ (algebraMap F E).range
n : ℕ := l.support.sup f
this : q ^ n ≠ 0
i : ι
hs : i ∉ l.support
⊢ l i ^ q ^ n ∈ (algebraMap F E).range

Tactic:
· convert! pow_mem (hf i) (q ^ (n - f i)) using 1
      rw [← pow_mul, ← pow_add, Nat.add_sub_of_le (Finset.le_sup hs)]

Goal state after:
case neg
F : Type u
E : Type v
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Algebra F E
K : Type w
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : IsPurelyInseparable F E
ι : Type u_1
v : ι → K
hsep : ∀ (i : ι), IsSeparable F (v i)
h : LinearIndependent F v
q : ℕ
h✝ : ExpChar F q
this✝ : ExpChar K q
l : ι →₀ E
hl : (Finsupp.linearCombination E v) l = 0
i✝ : ι
f : ι → ℕ
hf : ∀ (i : ι), l i ^ q ^ f i ∈ (algebraMap F E).range
n : ℕ := l.support.sup f
this : q ^ n ≠ 0
i : ι
hs : i ∉ l.support
⊢ l i ^ q ^ n ∈ (algebraMap F E).range
Module: Mathlib.FieldTheory.RatFunc.IntermediateField

Goal state before:
pp: K : Type u_1
inst✝ : Field K
f : K⟮X⟯
hf : ¬∃ c, f = C c
this : UniqueFactorizationMonoid ↥K[f]
⊢ Irreducible (f.minpolyX ↥K[f])

Tactic:
exact f.irreducible_minpolyX' hf

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
this :
  Polynomial.C ((algebraMap K[X] K⟮X⟯) (g E)) * Polynomial.map (algebraMap (↥E) K⟮X⟯) (q E) *
      Polynomial.map (algebraMap (↥E) K⟮X⟯) (φ E) =
    Polynomial.map (algebraMap K[X] K⟮X⟯) (θ E)
⊢ Polynomial.C ((algebraMap K[X] K⟮X⟯) (g E) / c E) *
      (Polynomial.map (algebraMap (↥E) K⟮X⟯) (q E) *
        (Polynomial.C (c E) * Polynomial.map (algebraMap (↥E) K⟮X⟯) (φ E))) =
    Polynomial.map (algebraMap K[X] K⟮X⟯) (θ E)

Tactic:
← mul_assoc _ (Polynomial.C (c E)) _,

Goal state after:
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
this :
  Polynomial.C ((algebraMap K[X] K⟮X⟯) (g E)) * Polynomial.map (algebraMap (↥E) K⟮X⟯) (q E) *
      Polynomial.map (algebraMap (↥E) K⟮X⟯) (φ E) =
    Polynomial.map (algebraMap K[X] K⟮X⟯) (θ E)
⊢ Polynomial.C ((algebraMap K[X] K⟮X⟯) (g E) / c E) *
      (Polynomial.map (algebraMap (↥E) K⟮X⟯) (q E) * Polynomial.C (c E) * Polynomial.map (algebraMap (↥E) K⟮X⟯) (φ E)) =
    Polynomial.map (algebraMap K[X] K⟮X⟯) (θ E)
Module: Mathlib.Geometry.Convex.Cone.Face.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁵ : Semiring R
inst✝⁴ : PartialOrder R
inst✝³ : IsOrderedRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
C F : PointedCone R M
ι : Type u_4
inst✝ : Fintype ι
f : ι → M
c : ι → R
hF : F.IsFaceOf C
hsC : ∀ (i : ι), f i ∈ C
hc : ∀ (i : ι), 0 ≤ c i
i : ι
hs : c i • f i + ∑ x ∈ Finset.univ \ {i}, c x • f x ∈ F
hci : 0 < c i
⊢ ∑ x ∈ Finset.univ \ {i}, c x • f x ∈ C

Tactic:
exact C.sum_mem fun i _ ↦ C.smul_mem (hc i) (hsC i)

Goal state after:
Module: Mathlib.Geometry.Convex.Cone.Face.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁵ : Semiring R
inst✝⁴ : PartialOrder R
inst✝³ : IsOrderedRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
C F : PointedCone R M
ι : Type u_4
inst✝ : Fintype ι
f : ι → M
c : ι → R
hF : F.IsFaceOf C
hsC : ∀ (i : ι), f i ∈ C
hc : ∀ (i : ι), 0 ≤ c i
i : ι
hs : c i • f i + ∑ x ∈ Finset.univ \ {i}, c x • f x ∈ F
hci : 0 < c i
⊢ f i ∈ F

Tactic:
refine hF.mem_of_smul_add_mem (hsC i) ?_ hci hs
    exact C.sum_mem fun i _ ↦ C.smul_mem (hc i) (hsC i)

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
F : Type u_1 := AlgebraicClosure K
H : ¬(Polynomial.map (algebraMap K F) (Q₂ h)).degree ≤ 0
α : F
hα : (aeval α) (Q₂ h) = 0
this :
  (aeval (Polynomial.C α)) (θ E) =
    (aeval (Polynomial.C α)) (Polynomial.map Polynomial.C (Q₂ h)) * (aeval (Polynomial.C α)) (Φ E)
⊢ (algebraMap K[X] F[X]).comp Polynomial.C = Polynomial.C.comp (algebraMap K F)

Tactic:
ext; simp

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
F : Type u_1 := AlgebraicClosure K
H : ¬(Polynomial.map (algebraMap K F) (Q₂ h)).degree ≤ 0
α : F
hα : (aeval α) (Q₂ h) = 0
this :
  (algebraMap K[X] F[X]) (g E) * (aeval (Polynomial.C α)) (Polynomial.map Polynomial.C (f E)) -
      (algebraMap K[X] F[X]) (f E) * (aeval (Polynomial.C α)) (Polynomial.map Polynomial.C (g E)) =
    0
⊢ (algebraMap K[X] F[X]).comp Polynomial.C = Polynomial.C.comp (algebraMap K F)

Tactic:
ext; simp

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
F : Type u_1 := AlgebraicClosure K
H : ¬(Polynomial.map (algebraMap K F) (Q₂ h)).degree ≤ 0
α : F
hα : (aeval α) (Q₂ h) = 0
this :
  (algebraMap K[X] F[X]) (g E) * Polynomial.C ((aeval α) (f E)) -
      (algebraMap K[X] F[X]) (f E) * (aeval (Polynomial.C α)) (Polynomial.map Polynomial.C (g E)) =
    0
⊢ (algebraMap K[X] F[X]).comp Polynomial.C = Polynomial.C.comp (algebraMap K F)

Tactic:
ext; simp

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

Goal state before:
pp: case e'_2
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 : V
⊢ θ.cos • (θ.cos • x - θ.sin • o.rightAngleRotation x) + θ.sin • (θ.cos • o.rightAngleRotation x - θ.sin • -x) =
    (θ.cos ^ 2 + θ.sin ^ 2) • x

Tactic:
module

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

Goal state before:
pp: V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
θ₁ θ₂ : Real.Angle
x : V
⊢ θ₁.cos • (θ₂.cos • x + θ₂.sin • o.rightAngleRotation x) + θ₁.sin • (θ₂.cos • o.rightAngleRotation x + θ₂.sin • -x) =
    (θ₁.cos * θ₂.cos - θ₁.sin * θ₂.sin) • x + (θ₁.sin * θ₂.cos + θ₁.cos * θ₂.sin) • o.rightAngleRotation x

Tactic:
module

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

Goal state before:
pp: case mpr
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
p : P
hne : p ≠ s.points i
h : p -ᵥ s.points i ∈ (s.altitude i).direction
⊢ vectorSpan ℝ {p, s.points i} = (s.altitude i).direction

Tactic:
rw [vectorSpan_eq_span_vsub_set_left_ne ℝ (Set.mem_insert _ _),
      Set.insert_sdiff_of_mem _ (Set.mem_singleton _),
      Set.sdiff_singleton_eq_self fun h => hne (Set.mem_singleton_iff.1 h), Set.image_singleton]

Goal state after:
case mpr
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
p : P
hne : p ≠ s.points i
h : p -ᵥ s.points i ∈ (s.altitude i).direction
⊢ ℝ ∙ (p -ᵥ s.points i) = (s.altitude i).direction
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
⊢ -(∡ p₁ p₂ p₃).sign = (∡ p₁ p₃ p₂).sign

Tactic:
by
  rw [oangle_swap₁₃_sign, ← oangle_swap₁₂_sign, oangle_swap₁₃_sign]

Goal state after: