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

Goal state before:
pp: case h
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
f : M → M
h✝ : TermDefinable₁ L f
t : L[[↑A]].Formula (Option Unit)
h : (Function.tupleGraph fun v ↦ f (v ())) = ofPred t.Realize
⊢ {x | (x 0, x 1) ∈ Function.graph f} = ofPred (Formula.relabel (fun x ↦ x.elim 1 fun x ↦ 0) t).Realize

Tactic:
ext v

Goal state after:
case h
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
f : M → M
h✝ : TermDefinable₁ L f
t : L[[↑A]].Formula (Option Unit)
h : (Function.tupleGraph fun v ↦ f (v ())) = ofPred t.Realize
v : Fin 2 → M
⊢ v ∈ {x | (x 0, x 1) ∈ Function.graph f} ↔ v ∈ ofPred (Formula.relabel (fun x ↦ x.elim 1 fun x ↦ 0) t).Realize
Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed

Goal state before:
pp: case refine_2
p : ℕ
κ : Cardinal.{u_2}
hκ : ℵ₀ < κ
M : Type u_2
struc✝¹ : Language.ring.Structure M
is_model✝¹ : M ⊨ Theory.ACF p
nonempty'✝¹ : Nonempty M
N : Type u_2
struc✝ : Language.ring.Structure N
is_model✝ : N ⊨ Theory.ACF p
nonempty'✝ : Nonempty N
hM : #↑{ Carrier := M, struc := struc✝¹, is_model := is_model✝¹, nonempty' := nonempty'✝¹ } = κ
hN : #↑{ Carrier := N, struc := struc✝, is_model := is_model✝, nonempty' := nonempty'✝ } = κ
x✝³ : Field M := fieldOfModelACF p M
this✝⁴ : M ⊨ Theory.field
x✝² : CompatibleRing M := compatibleRingOfModelField M
this✝³ : IsAlgClosed M
this✝² : CharP M p
x✝¹ : Field N := fieldOfModelACF p N
this✝¹ : N ⊨ Theory.field
x✝ : CompatibleRing N := compatibleRingOfModelField N
this✝ : IsAlgClosed N
this : CharP N p
⊢ Nonempty
    (↑{ Carrier := M, struc := struc✝¹, is_model := is_model✝¹, nonempty' := nonempty'✝¹ } ≃
      ↑{ Carrier := N, struc := struc✝, is_model := is_model✝, nonempty' := nonempty'✝ })

Tactic:
rw [← Cardinal.eq, hM, hN]

Goal state after:
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
⊢ Nat.card (Extension k p n) = Nat.card k ^ n

Tactic:
by
  let := ZMod.algebra k p
  rw [← pow_finrank_eq_natCard p, ← pow_finrank_eq_natCard p, finrank_zmod_extension, pow_mul]

Goal state after:
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
this : IsSplittingField k l (X ^ Nat.card k ^ n - X)
⊢ (X ^ Nat.card k ^ n - X).SplittingField ≃ₐ[k] Extension k p n

Tactic:
exact (IsSplittingField.algEquiv _ (X ^ (Nat.card k ^ n) - X)).symm

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

Goal state before:
pp: case inr.inl
k : Type u_1
inst✝ : Field k
f : k[X]
hi : Irreducible f
n : ℕ
h : f ∣ X ^ Nat.card k ^ n - X
hn : n ≠ 0
h✝ : Finite k
p : ℕ
hp : CharP k p
this✝ : Fact (Nat.Prime p)
this : NeZero n
⊢ f.natDegree ∣ n

Tactic:
← finrank_extension k p n

Goal state after:
case inr.inl
k : Type u_1
inst✝ : Field k
f : k[X]
hi : Irreducible f
n : ℕ
h : f ∣ X ^ Nat.card k ^ n - X
hn : n ≠ 0
h✝ : Finite k
p : ℕ
hp : CharP k p
this✝ : Fact (Nat.Prime p)
this : NeZero n
⊢ f.natDegree ∣ Module.finrank k (Extension k p n)
Module: Mathlib.FieldTheory.CardinalEmb

Goal state before:
pp: case refine_1
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
⊢ φ '' Iio i ⊆ Iio (φ i)

Tactic:
rintro _ ⟨j, hj, rfl⟩

Goal state after:
case refine_1
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 j : (Module.rank F E).ord.ToType
hj : j ∈ Iio i
⊢ φ j ∈ Iio (φ i)
Module: Mathlib.FieldTheory.CardinalEmb

Goal state before:
pp: case refine_2
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
⊢ ⇑b '' Iio (φ i) ⊆ ↑(adjoin F (⇑b ∘ φ '' Iio i))

Tactic:
rintro _ ⟨j, hj, rfl⟩

Goal state after:
case refine_2
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 j : (Module.rank F E).ord.ToType
hj : j ∈ Iio (φ i)
⊢ b j ∈ ↑(adjoin F (⇑b ∘ φ '' Iio i))
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
a✝ : (Module.rank F E).ord.ToType
hi : IsSuccPrelimit ↑a✝
⊢ ⇑b ∘ φ '' Iio a✝ ⊆ ↑(⨆ j, filtration ↑j)

Tactic:
rintro _ ⟨j, hj, rfl⟩

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✝ : (Module.rank F E).ord.ToType
hi : IsSuccPrelimit ↑a✝
j : (Module.rank F E).ord.ToType
hj : j ∈ Iio a✝
⊢ (⇑b ∘ φ) j ∈ ↑(⨆ j, filtration ↑j)
Module: Mathlib.FieldTheory.CardinalEmb

Goal state before:
pp: case neg
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
h : Module.rank F E < ℵ₀
⊢ #(Emb F E) = Module.rank F E

Tactic:
← IsNoetherian.iff_rank_lt_aleph0

Goal state after:
case neg
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
h : IsNoetherian F E
⊢ #(Emb F E) = Module.rank F E
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: case pos
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
j : ι
hj : j ∈ s
hcovers' : ⋃ i ∈ {x ∈ s | H x = H j}, g i • ↑(H j) = Set.univ
⊢ ∃ k ∈ s, (H k).FiniteIndex

Tactic:
exact ⟨j, hj, finiteIndex_of_leftCoset_cover_const hcovers'⟩

Goal state after:
Module: Mathlib.FieldTheory.JacobsonNoether

Goal state before:
pp: D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Algebra.IsAlgebraic (↥k) D
H : k ≠ ⊤
p : ℕ
hp : ExpChar D p
insep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
a : D
ha : a ∉ k
ha₀ : a ≠ 0
b : D
hb1 : ((ad (↥k) D) a) b ≠ 0
n : ℕ
hn : 0 < n
c : D := (⇑((ad (↥k) D) a))^[n] b
hb : c ≠ 0 ∧ (⇑((ad (↥k) D) a))^[n + 1] b = 0
hc_def : c = (⇑((ad (↥k) D) a))^[n] b
x✝ : Invertible c := { invOf := c⁻¹, invOf_mul_self := ⋯, mul_invOf_self := ⋯ }
hc : a * c = c * a
d : D := c⁻¹ * a * (⇑((ad (↥k) D) a))^[n - 1] b
hd_def : d = c⁻¹ * a * (⇑((ad (↥k) D) a))^[n - 1] b
hc' : c⁻¹ * a = a * c⁻¹
c_eq : a * (⇑((ad (↥k) D) a))^[n - 1] b - (⇑((ad (↥k) D) a))^[n - 1] b * a = c
eq1 : c⁻¹ * a * (⇑((ad (↥k) D) a))^[n - 1] b - c⁻¹ * (⇑((ad (↥k) D) a))^[n - 1] b * a = 1
⊢ a * c⁻¹ * (⇑((ad (↥k) D) a))^[n - 1] b * a = a * (c⁻¹ * (⇑((ad (↥k) D) a))^[n - 1] b) * a

Tactic:
← mul_assoc

Goal state after:
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Algebra.IsAlgebraic (↥k) D
H : k ≠ ⊤
p : ℕ
hp : ExpChar D p
insep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
a : D
ha : a ∉ k
ha₀ : a ≠ 0
b : D
hb1 : ((ad (↥k) D) a) b ≠ 0
n : ℕ
hn : 0 < n
c : D := (⇑((ad (↥k) D) a))^[n] b
hb : c ≠ 0 ∧ (⇑((ad (↥k) D) a))^[n + 1] b = 0
hc_def : c = (⇑((ad (↥k) D) a))^[n] b
x✝ : Invertible c := { invOf := c⁻¹, invOf_mul_self := ⋯, mul_invOf_self := ⋯ }
hc : a * c = c * a
d : D := c⁻¹ * a * (⇑((ad (↥k) D) a))^[n - 1] b
hd_def : d = c⁻¹ * a * (⇑((ad (↥k) D) a))^[n - 1] b
hc' : c⁻¹ * a = a * c⁻¹
c_eq : a * (⇑((ad (↥k) D) a))^[n - 1] b - (⇑((ad (↥k) D) a))^[n - 1] b * a = c
eq1 : c⁻¹ * a * (⇑((ad (↥k) D) a))^[n - 1] b - c⁻¹ * (⇑((ad (↥k) D) a))^[n - 1] b * a = 1
⊢ a * c⁻¹ * (⇑((ad (↥k) D) a))^[n - 1] b * a = a * c⁻¹ * (⇑((ad (↥k) D) a))^[n - 1] b * a
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: case isFalse
K : Type u
inst✝¹ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
inst✝ : NeZero n
σ : Gal(K[n√a]/K)
this✝¹ : Fact (Irreducible (X ^ n - C a)) := { out := H }
this✝ : IsDomain K[n√a] := inferInstance
this : DecidableEq K := Classical.decEq K
h✝ : ¬a = 0
⊢ (σ (root (X ^ n - C a)) / root (X ^ n - C a)) ^ n = 1

Tactic:
rw [div_pow, ← map_pow]

Goal state after:
case isFalse
K : Type u
inst✝¹ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
inst✝ : NeZero n
σ : Gal(K[n√a]/K)
this✝¹ : Fact (Irreducible (X ^ n - C a)) := { out := H }
this✝ : IsDomain K[n√a] := inferInstance
this : DecidableEq K := Classical.decEq K
h✝ : ¬a = 0
⊢ σ (root (X ^ n - C a) ^ n) / root (X ^ n - C a) ^ n = 1
Module: Mathlib.FieldTheory.JacobsonNoether

Goal state before:
pp: L : Type u_2
D : Type u_3
inst✝⁴ : Field L
inst✝³ : DivisionRing D
inst✝² : Algebra L D
inst✝¹ : Algebra.IsAlgebraic L D
inst✝ : IsCentral L D
hneq : ⊥ ≠ ⊤
hcenter : Subalgebra.center L D = ⊥
ntrivial : k ≠ ⊤
φ : ↥⊥ ≃ₐ[L] ↥(Subalgebra.center L D) := ⊥.equivOfEq (Subalgebra.center L D) ⋯
equiv : L ≃+* ↥k := ((botEquiv L D).symm.trans φ).toRingEquiv
⊢ ∃ x ∉ ⊥, IsSeparable L x

Tactic:
let _ : Algebra L (center D) := equiv.toRingHom.toAlgebra

Goal state after:
L : Type u_2
D : Type u_3
inst✝⁴ : Field L
inst✝³ : DivisionRing D
inst✝² : Algebra L D
inst✝¹ : Algebra.IsAlgebraic L D
inst✝ : IsCentral L D
hneq : ⊥ ≠ ⊤
hcenter : Subalgebra.center L D = ⊥
ntrivial : k ≠ ⊤
φ : ↥⊥ ≃ₐ[L] ↥(Subalgebra.center L D) := ⊥.equivOfEq (Subalgebra.center L D) ⋯
equiv : L ≃+* ↥k := ((botEquiv L D).symm.trans φ).toRingEquiv
x✝ : Algebra L ↥k := equiv.toRingHom.toAlgebra
⊢ ∃ x ∉ ⊥, IsSeparable L x
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)
α : L
hα : α ^ n = (algebraMap K L) a
⊢ (adjoinRootXPowSubCEquiv hζ H hα) (root (X ^ n - C a)) = α

Tactic:
rw [adjoinRootXPowSubCEquiv, AlgEquiv.coe_ofBijective, liftAlgHom_root]

Goal state after:
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: case inl
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
h : ∀ i ∈ s, (H i).FiniteIndex → s.card < (H i).index
hs : s.Nonempty
hs' : 0 < s.card
i : ι
hi : i ∈ s
hindex : (H i).index = 0
⊢ (↑(H i).index)⁻¹ < (↑s.card)⁻¹

Tactic:
hindex,

Goal state after:
case inl
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
h : ∀ i ∈ s, (H i).FiniteIndex → s.card < (H i).index
hs : s.Nonempty
hs' : 0 < s.card
i : ι
hi : i ∈ s
hindex : (H i).index = 0
⊢ (↑0)⁻¹ < (↑s.card)⁻¹
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 : Type v
inst✝³ : Ring A
B : Type w
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
H : IsField (A ⊗[R] B)
fa : A →ₐ[R] S
fb : B →ₐ[R] S
hfa : Function.Injective ⇑fa
hfb : Function.Injective ⇑fb
⊢ fa.range.LinearDisjoint fb.range

Tactic:
apply of_isField

Goal state after:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
A : Type v
inst✝³ : Ring A
B : Type w
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
H : IsField (A ⊗[R] B)
fa : A →ₐ[R] S
fb : B →ₐ[R] S
hfa : Function.Injective ⇑fa
hfb : Function.Injective ⇑fb
⊢ IsField (↥fa.range ⊗[R] ↥fb.range)
Module: Mathlib.FieldTheory.LinearDisjoint

Goal state before:
pp: case e'_7
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 (IsScalarTower.toAlgHom F L E).range
K : Type u_1
inst✝⁶ : Field K
inst✝⁵ : Algebra F K
inst✝⁴ : Algebra L K
inst✝³ : IsScalarTower F L K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : IsScalarTower L E K
this :
  (Subalgebra.map (IsScalarTower.toAlgHom F E K) A.toSubalgebra).LinearDisjoint
    ((IsScalarTower.toAlgHom F E K).comp (IsScalarTower.toAlgHom F L E)).range
x✝ : L
⊢ (IsScalarTower.toAlgHom F L K) x✝ = ((IsScalarTower.toAlgHom F E K).comp (IsScalarTower.toAlgHom F L E)) x✝

Tactic:
exact IsScalarTower.algebraMap_apply L E K _

Goal state after:
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
inst✝⁸ : CommRing R
A : Type v
inst✝⁷ : CommRing A
B : Type w
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : Flat R A
inst✝² : Flat R B
inst✝¹ : Algebra.Transcendental R A
inst✝ : Algebra.Transcendental R B
H : IsField (A ⊗[R] B)
this✝⁴ : Field (A ⊗[R] B) := H.toField
a : A
b : B
ha : Function.Injective ⇑(algebraMap R A)
hb : Function.Injective ⇑(algebraMap R B)
fa : A →ₐ[R] A ⊗[R] B := Algebra.TensorProduct.includeLeft
fb : B →ₐ[R] A ⊗[R] B := Algebra.TensorProduct.includeRight
hfa : Function.Injective ⇑fa
hfb : Function.Injective ⇑fb
this✝³ : IsDomain A
this✝² : IsDomain B
this✝¹ : IsDomain R
this✝ : Flat R ↥(toSubmodule fa.range)
key1 : Module.rank R ↥(fa.range ⊓ fb.range) ≤ 1
ga : R[X] →ₐ[R] A := aeval a
gb : R[X] →ₐ[R] B := aeval b
gab : R[X] →ₐ[R] A ⊗[R] B := fa.comp ga
hta : Function.Injective ⇑ga
htb : Function.Injective ⇑gb
htab : Function.Injective ⇑gab
algInst✝¹ : Algebra R[X] A := ga.toAlgebra
algInst✝ : Algebra R[X] B := gb.toAlgebra
f : A ⊗[R] B →ₐ[R] A ⊗[R[X]] B := Algebra.TensorProduct.mapOfCompatibleSMul R[X] R R A B
this : Nontrivial (A ⊗[R[X]] B)
hf : Function.Injective ⇑f
⊢ a ⊗ₜ[R] 1 ∈ ↑fa.range ∩ ↑fb.range

Tactic:
Set.mem_inter_iff,

Goal state after:
R : Type u
inst✝⁸ : CommRing R
A : Type v
inst✝⁷ : CommRing A
B : Type w
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : Flat R A
inst✝² : Flat R B
inst✝¹ : Algebra.Transcendental R A
inst✝ : Algebra.Transcendental R B
H : IsField (A ⊗[R] B)
this✝⁴ : Field (A ⊗[R] B) := H.toField
a : A
b : B
ha : Function.Injective ⇑(algebraMap R A)
hb : Function.Injective ⇑(algebraMap R B)
fa : A →ₐ[R] A ⊗[R] B := Algebra.TensorProduct.includeLeft
fb : B →ₐ[R] A ⊗[R] B := Algebra.TensorProduct.includeRight
hfa : Function.Injective ⇑fa
hfb : Function.Injective ⇑fb
this✝³ : IsDomain A
this✝² : IsDomain B
this✝¹ : IsDomain R
this✝ : Flat R ↥(toSubmodule fa.range)
key1 : Module.rank R ↥(fa.range ⊓ fb.range) ≤ 1
ga : R[X] →ₐ[R] A := aeval a
gb : R[X] →ₐ[R] B := aeval b
gab : R[X] →ₐ[R] A ⊗[R] B := fa.comp ga
hta : Function.Injective ⇑ga
htb : Function.Injective ⇑gb
htab : Function.Injective ⇑gab
algInst✝¹ : Algebra R[X] A := ga.toAlgebra
algInst✝ : Algebra R[X] B := gb.toAlgebra
f : A ⊗[R] B →ₐ[R] A ⊗[R[X]] B := Algebra.TensorProduct.mapOfCompatibleSMul R[X] R R A B
this : Nontrivial (A ⊗[R[X]] B)
hf : Function.Injective ⇑f
⊢ a ⊗ₜ[R] 1 ∈ ↑fa.range ∧ a ⊗ₜ[R] 1 ∈ ↑fb.range
Module: Mathlib.FieldTheory.RatFunc.Degree

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

Tactic:
Polynomial.natDegree_one,

Goal state after:
K : Type u
inst✝ : Field K
⊢ ↑1 - ↑0 = 1
Module: Mathlib.FieldTheory.RatFunc.Degree

Goal state before:
pp: K : Type u
inst✝ : Field K
p : K[X]
⊢ ↑p.natDegree - ↑(natDegree 1) = ↑p.natDegree

Tactic:
Polynomial.natDegree_one,

Goal state after:
K : Type u
inst✝ : Field K
p : K[X]
⊢ ↑p.natDegree - ↑0 = ↑p.natDegree
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✝ : 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 := Algebra.adjoin 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:
← hx',

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✝ : 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 := Algebra.adjoin 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
⊢ (LinearMap.rTensor (↥(toSubmodule B)) (Submodule.inclusion hA)) x' = y
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✝ : Algebra.IsSeparable F E
⊢ insepDegree F K = insepDegree E K

Tactic:
rw [insepDegree, insepDegree, separableClosure.eq_restrictScalars_of_isSeparable F E K]
  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
f : F[X]
hsep : f.Separable
hirr : Irreducible f
inst✝ : IsPurelyInseparable F E
⊢ Irreducible (Polynomial.map (algebraMap F E) f)

Tactic:
by
  let K := AlgebraicClosure E
  obtain ⟨x, hx⟩ := IsAlgClosed.exists_aeval_eq_zero K f
    (natDegree_pos_iff_degree_pos.1 hirr.natDegree_pos).ne'
  have ha : Associated f (minpoly F x) := by
    have := isUnit_C.2 (leadingCoeff_ne_zero.2 hirr.ne_zero).isUnit.inv
    exact ⟨this.unit, by rw [IsUnit.unit_spec, minpoly.eq_of_irreducible hirr hx]⟩
  have ha' : Associated (f.map (algebraMap F E)) ((minpoly F x).map (algebraMap F E)) :=
    ha.map (mapRingHom (algebraMap F E)).toMonoidHom
  have heq := minpoly.map_eq_of_isSeparable_of_isPurelyInseparable E x (ha.separable hsep)
  rw [ha'.irreducible_iff, heq]
  exact minpoly.irreducible (Algebra.IsIntegral.isIntegral x)

Goal state after:
Module: Mathlib.FieldTheory.Relrank

Goal state before:
pp: E : Type v
inst✝¹ : Field E
L : Type w
inst✝ : Field L
A : Subfield E
f : L →+* E
B : Subfield L
⊢ map f (comap f A) ⊓ map f B = A ⊓ map f B

Tactic:
rw [map_comap_eq, f.fieldRange_eq_map, inf_assoc, ← map_inf, top_inf_eq]

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
⊢ generator E ∈ E

Tactic:
by
  by_cases h : E = ⊥
  · rw [generator_eq_zero h]
    exact E.zero_mem
  · rw [generator_eq_coeff h]
    exact SetLike.coe_mem _

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

Goal state before:
pp: case mem_of_smul_add_mem
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 y : M} {a : R},
    x ∈ C₁ → y ∈ C₁ → 0 < a → a • x + y ∈ map (LinearMap.fst R M N) F → x ∈ map (LinearMap.fst R M N) F

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

Goal state after:
case mem_of_smul_add_mem
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 y : M} {a : R}, x ∈ C₁ → y ∈ C₁ → 0 < a → ∀ (x_1 : N), (a • x + y, x_1) ∈ F → ∃ x_2, (x, x_2) ∈ F
Module: Mathlib.Geometry.Convex.Cone.Face.Basic

Goal state before:
pp: case mem_of_smul_add_mem.refine_1
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 y : M
a : R
hx : x ∈ C₁
hy : y ∈ C₁
ha : 0 < a
z : N
h : (a • x + y, z) ∈ F
⊢ (x, 0) ∈ prod C₁ C₂

pp: case mem_of_smul_add_mem.refine_2
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 y : M
a : R
hx : x ∈ C₁
hy : y ∈ C₁
ha : 0 < a
z : N
h : (a • x + y, z) ∈ F
⊢ (y, z) ∈ prod C₁ C₂

Tactic:
· exact mem_prod.mp ⟨hx, zero_mem C₂⟩

Goal state after:
case mem_of_smul_add_mem.refine_2
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 y : M
a : R
hx : x ∈ C₁
hy : y ∈ C₁
ha : 0 < a
z : N
h : (a • x + y, z) ∈ F
⊢ (y, z) ∈ prod C₁ C₂
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
  rw [o.oangle_rev (-x), oangle_neg_left_eq_neg_right, add_neg_cancel]

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
f : V ≃ₗᵢ[ℝ] ℂ
hf : (map (Fin 2) f.toLinearEquiv) o = Complex.orientation
x : V
⊢ f ((o.rotation θ) x) = f ((o.rotation θ) (f.symm (f x)))

Tactic:
LinearIsometryEquiv.symm_apply_apply

Goal state after:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
f : V ≃ₗᵢ[ℝ] ℂ
hf : (map (Fin 2) f.toLinearEquiv) o = Complex.orientation
x : V
⊢ f ((o.rotation θ) x) = f ((o.rotation θ) x)
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

Goal state before:
pp: case refine_1.inr
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : SameRay ℝ x (-y)
⊢ x = 0 ∨ ∃ r, y = r • x

Tactic:
by_cases hx : x = 0; · simp [hx]
      obtain ⟨r, -, hy⟩ := h.exists_nonneg_left hx
      refine Or.inr ⟨-r, ?_⟩
      simp [hy]

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 ≠ 0 ∧ o.oangle x y ≠ ↑π ↔ LinearIndependent ℝ ![x, y]

Tactic:
contrapose! +distrib; exact oangle_eq_zero_or_eq_pi_iff_not_linearIndependent o

Goal state after: