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

Goal state before:
pp: L : Language
M : Type w'
inst✝ : L.Structure M
iM : Infinite M
κ : Cardinal.{w}
h1 : lift.{w', max (max u v) w} (lift.{w, max u v} L.card) ≤ lift.{w', max (max u v) w} (lift.{max u v, w} κ)
h2 : lift.{max w u v, w'} #M ≤ lift.{max w' u v, w} κ
N0 : (L.elementaryDiagram M).ModelType
hN0 : lift.{max (max u w') v w, w} κ ≤ #↑N0
⊢ lift.{max (max u v) w, w'} #M ≤ lift.{max (max w' u) v, w} κ ∧
    lift.{max w' w, max u v} L.card ≤ lift.{max (max w' u) v, w} κ

Tactic:
lift_lift,

Goal state after:
L : Language
M : Type w'
inst✝ : L.Structure M
iM : Infinite M
κ : Cardinal.{w}
h1 : lift.{max w w', max u v} L.card ≤ lift.{w', max (max u v) w} (lift.{max u v, w} κ)
h2 : lift.{max w u v, w'} #M ≤ lift.{max w' u v, w} κ
N0 : (L.elementaryDiagram M).ModelType
hN0 : lift.{max (max u w') v w, w} κ ≤ #↑N0
⊢ lift.{max (max u v) w, w'} #M ≤ lift.{max (max w' u) v, w} κ ∧
    lift.{max w' w, max u v} L.card ≤ lift.{max (max w' u) v, w} κ
Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed

Goal state before:
pp: φ : Language.ring.Sentence
T0 : Finset Language.ring.Sentence
hT0 : ↑T0 ⊆ Theory.ACF 0
h : ↑T0 ⊨ᵇ φ
ψ : Language.ring.Sentence
hψ :
  ψ ∈
    (Theory.field ∪
        if 0 = 0 then (fun q ↦ ∼(eqZero q)) '' {q | Nat.Prime q} else if Nat.Prime 0 then {eqZero 0} else {⊥}) ∪
      genericMonicPolyHasRoot '' {n | 0 < n}
⊢ { s // ∀ q ∉ s, Theory.ACF ↑q ⊨ᵇ ψ }

Tactic:
Set.union_right_comm,

Goal state after:
φ : Language.ring.Sentence
T0 : Finset Language.ring.Sentence
hT0 : ↑T0 ⊆ Theory.ACF 0
h : ↑T0 ⊨ᵇ φ
ψ : Language.ring.Sentence
hψ :
  ψ ∈
    Theory.field ∪ genericMonicPolyHasRoot '' {n | 0 < n} ∪
      if 0 = 0 then (fun q ↦ ∼(eqZero q)) '' {q | Nat.Prime q} else if Nat.Prime 0 then {eqZero 0} else {⊥}
⊢ { s // ∀ q ∉ s, Theory.ACF ↑q ⊨ᵇ ψ }
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: case mpr
L : Language
T : L.Theory
φ : L.Sentence
this : DecidableEq L.Sentence := ⋯
⊢ (∀ (T0 : Finset L.Sentence), ↑T0 ⊆ T → (↑T0 ∪ {Formula.not φ}).IsSatisfiable) →
    ∀ (T0 : Finset L.Sentence), ↑T0 ⊆ T ∪ {Formula.not φ} → IsSatisfiable ↑T0

Tactic:
· intro h T0 hT0
    exact IsSatisfiable.mono (h (T0.erase (Formula.not φ))
      (by simpa using hT0)) (by simp)

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: case inr
L : Language
T : L.Theory
h : T.IsComplete
M : Type u_1
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
φ : L.BoundedFormula Empty 0
h_realize : M ⊨ φ
hT : T ⊨ᵇ Formula.not φ
⊢ T ⊨ᵇ φ

Tactic:
have : M ⊨ φ.not := hT.realize_sentence M
      rw [Sentence.realize_not] at this
      contradiction

Goal state after:
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:
rw [adjoin_eq_range_freeAlgebra_lift]
  cases subsingleton_or_nontrivial R
  · rw [rank_subsingleton]; exact one_le_aleph0.trans (le_max_right _ _)
  rw [← lift_le.{max u v}]
  refine (lift_rank_range_le (FreeAlgebra.lift R ((↑) : s → S)).toLinearMap).trans ?_
  rw [FreeAlgebra.rank_eq, lift_id'.{v, u}, lift_umax.{v, u}, lift_le, max_comm]
  exact mk_list_le_max _

Goal state after:
Module: Mathlib.FieldTheory.AxGrothendieck

Goal state before:
pp: case intro
ι : Type u_1
K : Type u_2
R : Type u_3
inst✝⁴ : Field K
inst✝³ : Finite K
inst✝² : CommRing R
inst✝¹ : Finite ι
inst✝ : Algebra K R
alg : Algebra.IsAlgebraic K R
ps : ι → MvPolynomial ι R
S : Set (ι → R)
hm : Set.MapsTo (fun v i ↦ (eval v) (ps i)) S S
hinj : Set.InjOn (fun v i ↦ (eval v) (ps i)) S
is_int : ∀ (x : R), IsIntegral K x
v : ι → R
hvS : v ∈ S
val✝ : Fintype ι
s : Finset R := (univ.biUnion fun i ↦ image (fun x ↦ coeff x (ps i)) (ps i).support) ∪ image v univ
⊢ v ∈ (fun v i ↦ (eval v) (ps i)) '' S

Tactic:
have hv : ∀ i, v i ∈ Algebra.adjoin K (s : Set R) := fun j =>
    Algebra.subset_adjoin (mem_union_right _ (mem_image.2 ⟨j, mem_univ _, rfl⟩))

Goal state after:
case intro
ι : Type u_1
K : Type u_2
R : Type u_3
inst✝⁴ : Field K
inst✝³ : Finite K
inst✝² : CommRing R
inst✝¹ : Finite ι
inst✝ : Algebra K R
alg : Algebra.IsAlgebraic K R
ps : ι → MvPolynomial ι R
S : Set (ι → R)
hm : Set.MapsTo (fun v i ↦ (eval v) (ps i)) S S
hinj : Set.InjOn (fun v i ↦ (eval v) (ps i)) S
is_int : ∀ (x : R), IsIntegral K x
v : ι → R
hvS : v ∈ S
val✝ : Fintype ι
s : Finset R := (univ.biUnion fun i ↦ image (fun x ↦ coeff x (ps i)) (ps i).support) ∪ image v univ
hv : ∀ (i : ι), v i ∈ Algebra.adjoin K ↑s
⊢ v ∈ (fun v i ↦ (eval v) (ps i)) '' S
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: case refine_2
K : Type u_1
L : Type u_2
inst✝² : CommSemiring K
inst✝¹ : CommSemiring L
i : K →+* L
p : ℕ
inst✝ : IsPRadical i p
x : K
h : ∃ n, x ^ p ^ n = 0
⊢ ∃ n, i x ^ p ^ n = 0

Tactic:
obtain ⟨n, h⟩ := h

Goal state after:
case refine_2
K : Type u_1
L : Type u_2
inst✝² : CommSemiring K
inst✝¹ : CommSemiring L
i : K →+* L
p : ℕ
inst✝ : IsPRadical i p
x : K
n : ℕ
h : x ^ p ^ n = 0
⊢ ∃ n, i x ^ p ^ n = 0
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
x : L
n : ℕ
y : K
h : i y = x ^ p ^ n
⊢ ∃ y, i y.2 = x ^ p ^ y.1

Tactic:
exact ⟨(n, y), h⟩

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

Goal state before:
pp: case inr
R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
x : R
n : ℕ
hk : Odd (-↑n)
⊢ ∃ r, x = r ^ (-↑n)

Tactic:
· rcases exists_eq_pow_of_odd x (by simpa using hk) with ⟨r, hr⟩
    exact ⟨r⁻¹, by simpa using hr⟩

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
inst✝² : ExpChar L p
inst✝¹ : IsPRadical j p
inst✝ : PerfectRing L p
x : L
⊢ (lift i i p) x = x

Tactic:
lift_self_apply

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
inst✝² : ExpChar L p
inst✝¹ : IsPRadical j p
inst✝ : PerfectRing L p
x : L
⊢ x = 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
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : K
h : ∃ z, (⇑(frobenius K p))^[(0, 0).1 + z] (0, x).2 = (⇑(frobenius K p))^[(0, x).1 + z] (0, 0).2
⊢ x ∈ pNilradical K p

Tactic:
obtain ⟨n, h⟩ := h

Goal state after:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : K
n : ℕ
h : (⇑(frobenius K p))^[(0, 0).1 + n] (0, x).2 = (⇑(frobenius K p))^[(0, x).1 + n] (0, 0).2
⊢ x ∈ pNilradical K p
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
x : D
⊢ a ^ p ^ m * x - (mulRight (↥k) a ^ p ^ m) x = 0 x

Tactic:
pow_mulRight,

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
x : D
⊢ a ^ p ^ m * x - (mulRight (↥k) (a ^ p ^ m)) x = 0 x
Module: Mathlib.RingTheory.MvPolynomial

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

Tactic:
lift_lift,

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

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
ι : Type w
x : ι → E
inst✝ : Nonempty ι
hx : IsTranscendenceBasis F x
K : IntermediateField F E := IntermediateField.adjoin F (range x)
this : Algebra.IsAlgebraic (↥K) E
⊢ max (max (lift.{v, max u w} (lift.{w, u} #F)) (lift.{v, max u w} (lift.{u, w} #ι))) (lift.{v, max u w} ℵ₀) *
      lift.{max u w, v} (Module.rank (↥K) E) =
    max (max (lift.{max v w, u} #F) (lift.{max u v, w} #ι)) ℵ₀

Tactic:
lift_lift,

Goal state after:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
ι : Type w
x : ι → E
inst✝ : Nonempty ι
hx : IsTranscendenceBasis F x
K : IntermediateField F E := IntermediateField.adjoin F (range x)
this : Algebra.IsAlgebraic (↥K) E
⊢ max (max (lift.{max w v, u} #F) (lift.{v, max u w} (lift.{u, w} #ι))) (lift.{v, max u w} ℵ₀) *
      lift.{max u w, v} (Module.rank (↥K) E) =
    max (max (lift.{max v w, u} #F) (lift.{max u v, w} #ι)) ℵ₀
Module: Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
ι : Type w
x : ι → E
inst✝ : Nonempty ι
hx : IsTranscendenceBasis F x
K : IntermediateField F E := IntermediateField.adjoin F (range x)
this : Algebra.IsAlgebraic (↥K) E
⊢ max (max (lift.{max w v, u} #F) (lift.{v, max u w} (lift.{u, w} #ι))) (lift.{v, max u w} ℵ₀) *
      lift.{max u w, v} (Module.rank (↥K) E) =
    max (max (lift.{max v w, u} #F) (lift.{max u v, w} #ι)) ℵ₀

Tactic:
lift_lift,

Goal state after:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
ι : Type w
x : ι → E
inst✝ : Nonempty ι
hx : IsTranscendenceBasis F x
K : IntermediateField F E := IntermediateField.adjoin F (range x)
this : Algebra.IsAlgebraic (↥K) E
⊢ max (max (lift.{max w v, u} #F) (lift.{max u v, w} #ι)) (lift.{v, max u w} ℵ₀) *
      lift.{max u w, v} (Module.rank (↥K) E) =
    max (max (lift.{max v w, u} #F) (lift.{max u v, w} #ι)) ℵ₀
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)
this✝ : Fact (Irreducible (X ^ n - C a)) := { out := H }
this : Algebra K K[n√a] := inferInstance
⊢ (X ^ n - C a).Separable

Tactic:
have hn := Nat.pos_iff_ne_zero.mpr (ne_zero_of_irreducible_X_pow_sub_C H)

Goal state after:
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
⊢ (X ^ n - C a).Separable
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: K : Type u
inst✝⁴ : Field K
n : ℕ
a : K
H : Irreducible (X ^ n - C a)
L : Type u_1
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : IsSplittingField K L (X ^ n - C a)
α : L
hα : α ^ n = (algebraMap K L) a
inst✝ : NeZero n
ζ : K
hζ : IsPrimitiveRoot ζ n
m : ℤ
⊢ ((autEquivZmod H L hζ).symm (Multiplicative.ofAdd ↑m)) α = ζ ^ m • α

Tactic:
have hn := Nat.pos_iff_ne_zero.mpr (ne_zero_of_irreducible_X_pow_sub_C H)

Goal state after:
K : Type u
inst✝⁴ : Field K
n : ℕ
a : K
H : Irreducible (X ^ n - C a)
L : Type u_1
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : IsSplittingField K L (X ^ n - C a)
α : L
hα : α ^ n = (algebraMap K L) a
inst✝ : NeZero n
ζ : K
hζ : IsPrimitiveRoot ζ n
m : ℤ
hn : 0 < n
⊢ ((autEquivZmod H L hζ).symm (Multiplicative.ofAdd ↑m)) α = ζ ^ m • α
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)
L : Type u_1
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ n - C a)
this✝ : FiniteDimensional K L
this : IsGalois K L
⊢ Module.finrank K L = n

Tactic:
have hn := Nat.pos_iff_ne_zero.mpr (ne_zero_of_irreducible_X_pow_sub_C H)

Goal state after:
K : Type u
inst✝³ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
L : Type u_1
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ n - C a)
this✝ : FiniteDimensional K L
this : IsGalois K L
hn : 0 < n
⊢ Module.finrank K L = n
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 : IntermediateField F E
L : Type w
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
H : A.LinearDisjoint L
halg : Algebra.IsAlgebraic F ↥A ∨ Algebra.IsAlgebraic F L
⊢ Module.rank L ↥(adjoin L ↑A) =
    Module.rank ↥(IsScalarTower.toAlgHom F L E).range
      ↥(Algebra.adjoin ↥(IsScalarTower.toAlgHom F L E).range ↑A.toSubalgebra)

Tactic:
set L' := (IsScalarTower.toAlgHom F L E).range

Goal state after:
F : Type u
E : Type v
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
A : IntermediateField F E
L : Type w
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
H : A.LinearDisjoint L
halg : Algebra.IsAlgebraic F ↥A ∨ Algebra.IsAlgebraic F L
L' : Subalgebra F E := (IsScalarTower.toAlgHom F L E).range
⊢ Module.rank L ↥(adjoin L ↑A) = Module.rank ↥L' ↥(Algebra.adjoin ↥L' ↑A.toSubalgebra)
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 : IntermediateField F E
L : Type w
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
H : A.LinearDisjoint L
halg : Algebra.IsAlgebraic F ↥A ∨ Algebra.IsAlgebraic F L
⊢ Module.rank ↥A ↥(extendScalars ⋯) =
    Module.rank ↥A.toSubalgebra ↥(Algebra.adjoin ↥A.toSubalgebra ↑(IsScalarTower.toAlgHom F L E).range)

Tactic:
set L' := (IsScalarTower.toAlgHom F L E).range

Goal state after:
F : Type u
E : Type v
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
A : IntermediateField F E
L : Type w
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
H : A.LinearDisjoint L
halg : Algebra.IsAlgebraic F ↥A ∨ Algebra.IsAlgebraic F L
L' : Subalgebra F E := (IsScalarTower.toAlgHom F L E).range
⊢ Module.rank ↥A ↥(extendScalars ⋯) = Module.rank ↥A.toSubalgebra ↥(Algebra.adjoin ↥A.toSubalgebra ↑L')
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 : IntermediateField F E
L : Type w
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
H : A.LinearDisjoint L
halg : Algebra.IsAlgebraic F ↥A ∨ Algebra.IsAlgebraic F L
L' : Subalgebra F E := (IsScalarTower.toAlgHom F L E).range
⊢ Subsemiring.closure (Set.range ⇑(algebraMap L E) ∪ ↑A) = Subsemiring.closure (Set.range ⇑(algebraMap (↥A) E) ∪ ↑L')

Tactic:
Set.union_comm

Goal state after:
F : Type u
E : Type v
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
A : IntermediateField F E
L : Type w
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
H : A.LinearDisjoint L
halg : Algebra.IsAlgebraic F ↥A ∨ Algebra.IsAlgebraic F L
L' : Subalgebra F E := (IsScalarTower.toAlgHom F L E).range
⊢ Subsemiring.closure (↑A ∪ Set.range ⇑(algebraMap L E)) = Subsemiring.closure (Set.range ⇑(algebraMap (↥A) E) ∪ ↑L')
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 : IntermediateField F E
L : Type w
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
H : A.LinearDisjoint L
halg : Algebra.IsAlgebraic F ↥A ∨ Algebra.IsAlgebraic F L
⊢ Cardinal.lift.{w, v} (Module.rank ↥A ↥(extendScalars ⋯)) = Cardinal.lift.{v, w} (Module.rank F L)

Tactic:
by
  rw [(AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)).toLinearEquiv.lift_rank_eq,
    Cardinal.lift_inj, ← Subalgebra.LinearDisjoint.adjoin_rank_eq_rank_right H]
  set L' := (IsScalarTower.toAlgHom F L E).range
  have heq : (adjoin L (A : Set E)).toSubalgebra.toSubsemiring =
      (Algebra.adjoin A (L' : Set E)).toSubsemiring := by
    rw [adjoin_intermediateField_toSubalgebra_of_isAlgebraic _ _ halg.symm,
      Algebra.adjoin_toSubsemiring, Algebra.adjoin_toSubsemiring, Set.union_comm]
    congr 2
    ext x
    simp
  refine rank_eq_of_equiv_equiv (RingHom.id A) (RingEquiv.subsemiringCongr heq).toAddEquiv
    Function.bijective_id fun ⟨a, ha⟩ ⟨x, hx⟩ ↦ ?_
  ext
  simp_rw [Algebra.smul_def]
  rfl

Goal state after:
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 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
⊢ l i = 0 i

Tactic:
let n := l.support.sup f

Goal state after:
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
⊢ l i = 0 i
Module: Mathlib.FieldTheory.LinearDisjoint

Goal state before:
pp: F : Type u
inst✝⁴ : Field F
A : Type v
inst✝³ : Field A
B : Type w
inst✝² : Field B
inst✝¹ : Algebra F A
inst✝ : Algebra F B
M : Ideal (A ⊗[F] B)
hM : M.IsMaximal
K : Type (max v w) := A ⊗[F] B ⧸ M
this : Field K := Ideal.Quotient.field M
i : A ⊗[F] B →ₐ[F] K := IsScalarTower.toAlgHom F (A ⊗[F] B) K
fa : A →ₐ[F] K := i.comp Algebra.TensorProduct.includeLeft
fb : B →ₐ[F] K := i.comp Algebra.TensorProduct.includeRight
H : Function.Injective ⇑(fa.range.mulMap fb.range)
hi :
  i =
    (fa.range.mulMap fb.range).comp
      ↑(Algebra.TensorProduct.congr (AlgEquiv.ofInjective fa ⋯) (AlgEquiv.ofInjective fb ⋯))
⊢ Function.Injective ⇑i

Tactic:
simpa only
    [hi, AlgHom.coe_comp, AlgEquiv.coe_toAlgHom, EquivLike.injective_comp, fa, this, K, fb]

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

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
q n : ℕ
hF : ExpChar F q
ι : Type u_1
v : ι → E
inst✝ : Algebra.IsSeparable F E
h : ∀ (s : Finset ι), LinearIndependent F (v ∘ Subtype.val)
⊢ ∀ (s : Finset ι), LinearIndependent F ((fun x ↦ v x ^ q ^ n) ∘ Subtype.val)

Tactic:
intro s

Goal state after:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
q n : ℕ
hF : ExpChar F q
ι : Type u_1
v : ι → E
inst✝ : Algebra.IsSeparable F E
h : ∀ (s : Finset ι), LinearIndependent F (v ∘ Subtype.val)
s : Finset ι
⊢ LinearIndependent F ((fun x ↦ v x ^ q ^ n) ∘ Subtype.val)
Module: Mathlib.FieldTheory.RatFunc.Degree

Goal state before:
pp: K : Type u
inst✝ : Field K
⊢ ↑(natDegree 0) - ↑(denom 0).natDegree = 0

Tactic:
natDegree_zero,

Goal state after:
K : Type u
inst✝ : Field K
⊢ ↑0 - ↑(denom 0).natDegree = 0
Module: Mathlib.FieldTheory.RatFunc.IntermediateField

Goal state before:
pp: K : Type u_1
inst✝ : Field K
f : K⟮X⟯
hf : ¬∃ c, f = C c
e : K[X] ≃ₐ[K] ↥K[f] := Polynomial.algEquivOfTranscendental K f ⋯
φ : K[X][X] :=
  Polynomial.map (algebraMap K K[X]) f.num - Polynomial.C Polynomial.X * Polynomial.map (algebraMap K K[X]) f.denom
φ_map : (mapEquiv e.toRingEquiv) φ = f.minpolyX ↥K[f]
⊢ Irreducible ((mapEquiv e.toRingEquiv) φ)

Tactic:
MulEquiv.irreducible_iff

Goal state after:
K : Type u_1
inst✝ : Field K
f : K⟮X⟯
hf : ¬∃ c, f = C c
e : K[X] ≃ₐ[K] ↥K[f] := Polynomial.algEquivOfTranscendental K f ⋯
φ : K[X][X] :=
  Polynomial.map (algebraMap K K[X]) f.num - Polynomial.C Polynomial.X * Polynomial.map (algebraMap K K[X]) f.denom
φ_map : (mapEquiv e.toRingEquiv) φ = f.minpolyX ↥K[f]
⊢ Irreducible φ
Module: Mathlib.FieldTheory.RatFunc.IntermediateField

Goal state before:
pp: K : Type u_1
inst✝ : Field K
f : K⟮X⟯
hf : ¬∃ c, f = C c
e : K[X] ≃ₐ[K] ↥K[f] := Polynomial.algEquivOfTranscendental K f ⋯
φ : K[X][X] :=
  Polynomial.map (algebraMap K K[X]) f.num - Polynomial.C Polynomial.X * Polynomial.map (algebraMap K K[X]) f.denom
φ_map : (mapEquiv e.toRingEquiv) φ = f.minpolyX ↥K[f]
this : φ = Bivariate.swap (Polynomial.C f.num - Polynomial.X * Polynomial.C f.denom)
⊢ Irreducible (Bivariate.swap (Polynomial.C f.num - Polynomial.X * Polynomial.C f.denom))

Tactic:
MulEquiv.irreducible_iff

Goal state after:
K : Type u_1
inst✝ : Field K
f : K⟮X⟯
hf : ¬∃ c, f = C c
e : K[X] ≃ₐ[K] ↥K[f] := Polynomial.algEquivOfTranscendental K f ⋯
φ : K[X][X] :=
  Polynomial.map (algebraMap K K[X]) f.num - Polynomial.C Polynomial.X * Polynomial.map (algebraMap K K[X]) f.denom
φ_map : (mapEquiv e.toRingEquiv) φ = f.minpolyX ↥K[f]
this : φ = Bivariate.swap (Polynomial.C f.num - Polynomial.X * Polynomial.C f.denom)
⊢ Irreducible (Polynomial.C f.num - Polynomial.X * Polynomial.C f.denom)
Module: Mathlib.Geometry.Convex.Cone.Face.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsOrderedRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
C F : PointedCone R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
hf : Function.Injective ⇑f
hF : F.IsFaceOf C
⊢ ∀ {x y : N} {a : R}, x ∈ map f C → y ∈ map f C → 0 < a → a • x + y ∈ map f F → x ∈ map f F

Tactic:
rintro _ _ a ⟨x, hx, rfl⟩ ⟨y, hy, rfl⟩ ha ⟨z, hz₁, hz₂⟩
    dsimp at hz₂
    rw [← map_smul, ← map_add] at hz₂
    exact ⟨x, hF.mem_of_smul_add_mem hx hy ha (hf hz₂ ▸ hz₁), rfl⟩

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

Goal state before:
pp: case le
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : DivisionRing R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsOrderedRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
C₁ : PointedCone R M
C₂ : PointedCone R N
F : PointedCone R (M × N)
hF : F.IsFaceOf (prod C₁ C₂)
x : M
hx : x ∈ map (LinearMap.fst R M N) F
⊢ x ∈ C₁

Tactic:
simp only [mem_map, LinearMap.fst_apply, Prod.exists, exists_and_right, exists_eq_right] at hx

Goal state after:
case le
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : DivisionRing R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsOrderedRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
C₁ : PointedCone R M
C₂ : PointedCone R N
F : PointedCone R (M × N)
hF : F.IsFaceOf (prod C₁ C₂)
x : M
hx : ∃ x_1, (x, x_1) ∈ F
⊢ x ∈ C₁
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:
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 : V
⊢ 2 • o.oangle (-x) x = 0

Tactic:
by
  by_cases hx : x = 0 <;> simp [hx]

Goal state after: