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

Goal state before:
pp: L : Language
α : Type u'
s t : Set α
h : s ⊆ t
⊢ L.distinctConstantsTheory s ⊆ L.distinctConstantsTheory t

Tactic:
unfold distinctConstantsTheory; gcongr

Goal state after:
Module: Mathlib.ModelTheory.Ultraproducts

Goal state before:
pp: α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝ : (a : α) → L.Structure (M a)
n : ℕ
r : L.Relations n
x y : Fin n → (a : α) → M a
xy : x ≈ y
⊢ RelMap r x ↔ RelMap r y

Tactic:
refine ⟨fun hx => ?_, fun hy => ?_⟩

Goal state after:
case refine_1
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝ : (a : α) → L.Structure (M a)
n : ℕ
r : L.Relations n
x y : Fin n → (a : α) → M a
xy : x ≈ y
hx : RelMap r x
⊢ RelMap r y

case refine_2
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝ : (a : α) → L.Structure (M a)
n : ℕ
r : L.Relations n
x y : Fin n → (a : α) → M a
xy : x ≈ y
hy : RelMap r y
⊢ RelMap r x
Module: Mathlib.ModelTheory.Ultraproducts

Goal state before:
pp: α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → L.Structure (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
n✝ l✝ : ℕ
R✝ : L.Relations l✝
ts✝ : Fin l✝ → L.Term (β ⊕ Fin n✝)
v : Fin n✝ → (a : α) → M a
h2 : ∀ (a : α), (Sum.elim (fun i ↦ x i a) fun i ↦ v i a) = fun i ↦ Sum.elim x v i a
| RelMap R✝ fun i ↦ Term.realize (Quotient.mk' ∘ Sum.elim x v) (ts✝ i)

Tactic:
enter [2, i]; erw [term_realize_cast]

Goal state after:
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → L.Structure (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
n✝ l✝ : ℕ
R✝ : L.Relations l✝
ts✝ : Fin l✝ → L.Term (β ⊕ Fin n✝)
v : Fin n✝ → (a : α) → M a
h2 : ∀ (a : α), (Sum.elim (fun i ↦ x i a) fun i ↦ v i a) = fun i ↦ Sum.elim x v i a
i : Fin l✝
| Quotient.mk' fun a ↦ Term.realize (fun i ↦ Sum.elim x v i a) (ts✝ i)
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case func.refine_1
L : Language
α : Type u'
l✝ : List (L.Term α)
n : ℕ
f : L.Functions n
ts : Fin n → L.Term α
ih : ∀ (a : Fin n) (l : List (α ⊕ (i : ℕ) × L.Functions i)), listDecode ((ts a).listEncode ++ l) = ts a :: listDecode l
l : List (α ⊕ (i : ℕ) × L.Functions i)
h : listDecode (flatMap (fun i ↦ (ts i).listEncode) (finRange n) ++ l) = List.map ts (finRange n) ++ listDecode l
i : Fin n
⊢ (List.map ts (finRange n) ++ listDecode l)[↑i] = ts i

Tactic:
simp only [length_map, length_finRange, is_lt, getElem_append_left, getElem_map,
      getElem_finRange, cast_mk, Fin.eta]

Goal state after:
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case refine_1
L : Language
α : Type u'
⊢ ℵ₀ * ⨆ i, #(L.Term (α ⊕ Fin i)) ≤ max ℵ₀ #(α ⊕ (i : ℕ) × L.Functions i)

Tactic:
mul_eq_max_of_aleph0_le_left le_rfl,

Goal state after:
case refine_1
L : Language
α : Type u'
⊢ max ℵ₀ (⨆ i, #(L.Term (α ⊕ Fin i))) ≤ max ℵ₀ #(α ⊕ (i : ℕ) × L.Functions i)

case refine_1
L : Language
α : Type u'
⊢ ⨆ i, #(L.Term (α ⊕ Fin i)) ≠ 0
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case refine_2
L : Language
α : Type u'
⊢ max ℵ₀ #(α ⊕ (i : ℕ) × L.Functions i) ≤ #((n : ℕ) × L.Term (α ⊕ Fin n))

Tactic:
rw [max_le_iff, ← infinite_iff]
    refine ⟨Infinite.of_injective
        (fun i => ⟨i + 1, var (Sum.inr (last i))⟩) fun i j ij => ?_, ?_⟩
    · cases ij
      rfl
    · rw [Cardinal.le_def]
      refine ⟨⟨Sum.elim (fun i => ⟨0, var (Sum.inl i)⟩)
        fun F => ⟨1, func F.2 fun _ => var (Sum.inr 0)⟩, ?_⟩⟩
      rintro (a | a) (b | b) h
      · simp only [Sum.elim_inl, Sigma.mk.inj_iff, heq_eq_eq, var.injEq, Sum.inl.injEq, true_and]
          at h
        rw [h]
      · simp only [Sum.elim_inl, Sum.elim_inr, Sigma.mk.inj_iff, false_and, reduceCtorEq] at h
      · simp only [Sum.elim_inr, Sum.elim_inl, Sigma.mk.inj_iff, false_and, reduceCtorEq] at h
      · simp only [Sum.elim_inr, Sigma.mk.inj_iff, heq_eq_eq, func.injEq, true_and] at h
        rw [Sigma.ext_iff.2 ⟨h.1, h.2.1⟩]

Goal state after:
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case falsum
L : Language
α : Type u'
l : List ((n : ℕ) × L.BoundedFormula α n)
n n✝ : ℕ
⊢ ∀ (l' : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
    listDecode (⟨n✝, falsum⟩.snd.listEncode ++ l') = ⟨n✝, falsum⟩ :: listDecode l'

Tactic:
intro l

Goal state after:
case falsum
L : Language
α : Type u'
l✝ : List ((n : ℕ) × L.BoundedFormula α n)
n n✝ : ℕ
l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
⊢ listDecode (⟨n✝, falsum⟩.snd.listEncode ++ l) = ⟨n✝, falsum⟩ :: listDecode l
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case equal
L : Language
α : Type u'
l : List ((n : ℕ) × L.BoundedFormula α n)
n n✝ : ℕ
t₁✝ t₂✝ : L.Term (α ⊕ Fin n✝)
⊢ ∀ (l' : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
    listDecode (⟨n✝, equal t₁✝ t₂✝⟩.snd.listEncode ++ l') = ⟨n✝, equal t₁✝ t₂✝⟩ :: listDecode l'

Tactic:
intro l

Goal state after:
case equal
L : Language
α : Type u'
l✝ : List ((n : ℕ) × L.BoundedFormula α n)
n n✝ : ℕ
t₁✝ t₂✝ : L.Term (α ⊕ Fin n✝)
l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
⊢ listDecode (⟨n✝, equal t₁✝ t₂✝⟩.snd.listEncode ++ l) = ⟨n✝, equal t₁✝ t₂✝⟩ :: listDecode l
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case rel
L : Language
α : Type u'
l : List ((n : ℕ) × L.BoundedFormula α n)
n φ_n φ_l : ℕ
φ_R : L.Relations φ_l
ts : Fin φ_l → L.Term (α ⊕ Fin φ_n)
⊢ ∀ (l' : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
    listDecode (⟨φ_n, rel φ_R ts⟩.snd.listEncode ++ l') = ⟨φ_n, rel φ_R ts⟩ :: listDecode l'

Tactic:
intro l

Goal state after:
case rel
L : Language
α : Type u'
l✝ : List ((n : ℕ) × L.BoundedFormula α n)
n φ_n φ_l : ℕ
φ_R : L.Relations φ_l
ts : Fin φ_l → L.Term (α ⊕ Fin φ_n)
l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
⊢ listDecode (⟨φ_n, rel φ_R ts⟩.snd.listEncode ++ l) = ⟨φ_n, rel φ_R ts⟩ :: listDecode l
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case imp
L : Language
α : Type u'
l : List ((n : ℕ) × L.BoundedFormula α n)
n n✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula α n✝
ih1 :
  ∀ (l' : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
    listDecode (⟨n✝, f₁✝⟩.snd.listEncode ++ l') = ⟨n✝, f₁✝⟩ :: listDecode l'
ih2 :
  ∀ (l' : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
    listDecode (⟨n✝, f₂✝⟩.snd.listEncode ++ l') = ⟨n✝, f₂✝⟩ :: listDecode l'
⊢ ∀ (l' : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
    listDecode (⟨n✝, f₁✝ ⟹ f₂✝⟩.snd.listEncode ++ l') = ⟨n✝, f₁✝ ⟹ f₂✝⟩ :: listDecode l'

Tactic:
intro l

Goal state after:
case imp
L : Language
α : Type u'
l✝ : List ((n : ℕ) × L.BoundedFormula α n)
n n✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula α n✝
ih1 :
  ∀ (l' : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
    listDecode (⟨n✝, f₁✝⟩.snd.listEncode ++ l') = ⟨n✝, f₁✝⟩ :: listDecode l'
ih2 :
  ∀ (l' : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
    listDecode (⟨n✝, f₂✝⟩.snd.listEncode ++ l') = ⟨n✝, f₂✝⟩ :: listDecode l'
l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
⊢ listDecode (⟨n✝, f₁✝ ⟹ f₂✝⟩.snd.listEncode ++ l) = ⟨n✝, f₁✝ ⟹ f₂✝⟩ :: listDecode l
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case all
L : Language
α : Type u'
l : List ((n : ℕ) × L.BoundedFormula α n)
n n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih :
  ∀ (l' : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
    listDecode (⟨n✝ + 1, f✝⟩.snd.listEncode ++ l') = ⟨n✝ + 1, f✝⟩ :: listDecode l'
⊢ ∀ (l' : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
    listDecode (⟨n✝, ∀' f✝⟩.snd.listEncode ++ l') = ⟨n✝, ∀' f✝⟩ :: listDecode l'

Tactic:
intro l

Goal state after:
case all
L : Language
α : Type u'
l✝ : List ((n : ℕ) × L.BoundedFormula α n)
n n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih :
  ∀ (l' : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
    listDecode (⟨n✝ + 1, f✝⟩.snd.listEncode ++ l') = ⟨n✝ + 1, f✝⟩ :: listDecode l'
l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
⊢ listDecode (⟨n✝, ∀' f✝⟩.snd.listEncode ++ l) = ⟨n✝, ∀' f✝⟩ :: listDecode l
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: case h₁
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
β : Type u_1
s : Set (β → M)
h : A.Definable L s
f : α ≃ β
⊢ Function.LeftInverse (fun g ↦ g ∘ ⇑f.symm) fun g ↦ g ∘ ⇑f

pp: case h₂
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
β : Type u_1
s : Set (β → M)
h : A.Definable L s
f : α ≃ β
⊢ Function.RightInverse (fun g ↦ g ∘ ⇑f.symm) fun g ↦ g ∘ ⇑f

Tactic:
· intro i
    ext b
    simp only [Function.comp_apply, Equiv.apply_symm_apply]

Goal state after:
case h₂
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
β : Type u_1
s : Set (β → M)
h : A.Definable L s
f : α ≃ β
⊢ Function.RightInverse (fun g ↦ g ∘ ⇑f.symm) fun g ↦ g ∘ ⇑f
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
φ : L.Formula (↑A ⊕ α)
A0 : Finset M := Finset.image Subtype.val (BoundedFormula.freeVarFinset φ).toLeft
⊢ ↑A0 ⊆ A

Tactic:
by simp [A0]

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
N : Type u_1
inst✝¹ : L.Structure M
inst✝ : L.Structure N
T : L.Theory
h : M ≅[L] N
⊢ M ⊨ T ↔ N ⊨ T

Tactic:
rw [Theory.model_iff_subset_completeTheory, Theory.model_iff_subset_completeTheory,
    h.completeTheory_eq]

Goal state after:
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 u v} L.card ≤ 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 w' w, max u v} L.card ≤ lift.{max (max w' u) v, w} κ

Tactic:
add_eq_max (aleph0_le_lift.2 (infinite_iff.1 iM)),

Goal state after:
L : Language
M : Type w'
inst✝ : L.Structure M
iM : Infinite M
κ : Cardinal.{w}
h1 : lift.{w, max u v} L.card ≤ 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
⊢ max (lift.{max (max u v) w, w'} #M) (lift.{max w' w, max u v} L.card) ≤ lift.{max (max w' u) v, w} κ
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
T : L.Theory
φ : L.Sentence
⊢ T ⊨ᵇ φ ↔ ∃ T0, ↑T0 ⊆ T ∧ ↑T0 ⊨ᵇ φ

Tactic:
simp only [models_iff_not_satisfiable]
  rw [isSatisfiable_iff_isFinitelySatisfiable, IsFinitelySatisfiable]
  contrapose!
  let := Classical.decEq (Sentence L)
  constructor
  · intro h T0 hT0
    simpa using h (T0 ∪ {Formula.not φ})
      (by
        simp only [Finset.coe_union, Finset.coe_singleton]
        exact Set.union_subset_union hT0 (Set.Subset.refl _))
  · intro h T0 hT0
    exact IsSatisfiable.mono (h (T0.erase (Formula.not φ))
      (by simpa using hT0)) (by simp)

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 + ↑1) * logDeriv a

Tactic:
Nat.cast_one,

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)) = (↑n + 1) * logDeriv a
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 : WithTop (Module.rank F E).ord.ToType
hi : IsSuccPrelimit i
f : ↑(limit (embFunctor F E) i)
h : Nonempty ↑(Iio i)
⊢ (filtration i).toSubalgebra ≤ ⨆ x, ((fun j ↦ filtration ↑j) x).toSubalgebra

Tactic:
← iSup_filtration hi,

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 : WithTop (Module.rank F E).ord.ToType
hi : IsSuccPrelimit i
f : ↑(limit (embFunctor F E) i)
h : Nonempty ↑(Iio i)
⊢ (⨆ j, filtration ↑j).toSubalgebra ≤ ⨆ x, ((fun j ↦ filtration ↑j) x).toSubalgebra
Module: Mathlib.FieldTheory.CardinalEmb

Goal state before:
pp: case pos
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
hi : IsSuccPrelimit i
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h : Nonempty ↑(Iio i)
x : E
hx : x ∈ (filtration i).toSubalgebra
⊢ ((fun f ↦ Subalgebra.iSupLift (fun x ↦ ((fun j ↦ filtration ↑j) x).toSubalgebra) ⋯ ↑f ⋯ (filtration i).toSubalgebra ⋯)
        ((fun f ↦ ⟨fun j ↦ embFunctor F E ⋯ f, ⋯⟩) f))
      ⟨x, hx⟩ =
    f ⟨x, hx⟩

Tactic:
← iSup_filtration hi,

Goal state after:
case pos
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
hi : IsSuccPrelimit i
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h : Nonempty ↑(Iio i)
x : E
hx✝ : x ∈ (filtration i).toSubalgebra
hx : x ∈ (⨆ j, filtration ↑j).toSubalgebra
⊢ ((fun f ↦ Subalgebra.iSupLift (fun x ↦ ((fun j ↦ filtration ↑j) x).toSubalgebra) ⋯ ↑f ⋯ (filtration i).toSubalgebra ⋯)
        ((fun f ↦ ⟨fun j ↦ embFunctor F E ⋯ f, ⋯⟩) f))
      ⟨x, hx✝⟩ =
    f ⟨x, hx✝⟩
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: K : Type u
inst✝² : Field K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
⊢ ((0, 0).1, (0, 0).2⁻¹) = (0, 0)

Tactic:
rw [inv_zero]

Goal state after:
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
⊢ Nontrivial (A ⊗[R] B)

Tactic:
have := ha.isDomain _

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
⊢ Nontrivial (A ⊗[R] B)
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: 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)
⊢ (minpoly K σ.toLinearMap).IsRoot ζ

Tactic:
IsGalois.card_aut_eq_finrank

Goal state after:
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 σ = finrank K L
⊢ (minpoly K σ.toLinearMap).IsRoot ζ
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
⊢ ∃ i ∈ s, (H i).FiniteIndex ∧ (H i).index ≤ s.card

Tactic:
by
  by_contra! h
  apply (one_le_sum_inv_index_of_leftCoset_cover hcovers).not_gt
  cases s.eq_empty_or_nonempty with
  | inl hs => simp only [hs, Finset.sum_empty, zero_lt_one]
  | inr hs =>
  have hs' : 0 < s.card := hs.card_pos
  have hlt : ∀ i ∈ s, ((H i).index : ℚ)⁻¹ < (s.card : ℚ)⁻¹ := fun i hi ↦ by
    cases eq_or_ne (H i).index 0 with
    | inl hindex =>
      rwa [hindex, Nat.cast_zero, inv_zero, inv_pos, Nat.cast_pos]
    | inr hindex =>
      exact inv_strictAnti₀ (by exact_mod_cast hs') (by exact_mod_cast h i hi ⟨hindex⟩)
  apply (Finset.sum_lt_sum_of_nonempty hs hlt).trans_eq
  rw [Finset.sum_const, nsmul_eq_mul, mul_inv_cancel₀ (Nat.cast_ne_zero.mpr hs'.ne')]

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
hta : Transcendental R a
b : B
htb : Transcendental R 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
⊢ False

Tactic:
have := ha.isDomain _

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
hta : Transcendental R a
b : B
htb : Transcendental R 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
⊢ False
Module: Mathlib.FieldTheory.NormalizedTrace

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
a : F
⊢ (↑1)⁻¹ • (trace F F) a = a

Tactic:
Nat.cast_one,

Goal state after:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
a : F
⊢ 1⁻¹ • (trace F F) a = 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✝ : 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'
h : {x, y} ⊆ ↑(LinearMap.rTensor (↥(toSubmodule B)) (Submodule.inclusion hM)).range
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
x✝ : ↥(toSubmodule A) ⊗[R] ↥(toSubmodule B)
hx : x✝ ∈ {x, y}
this : Submodule.inclusion hM = Submodule.inclusion hA ∘ₗ Submodule.inclusion ⋯
⊢ x✝ ∈ ↑(LinearMap.rTensor (↥(toSubmodule B)) (Submodule.inclusion hA)).range

Tactic:
rw [this, LinearMap.rTensor_comp] at h

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) ∘ₗ
          LinearMap.rTensor (↥(toSubmodule B)) (Submodule.inclusion ⋯)).range
x✝ : ↥(toSubmodule A) ⊗[R] ↥(toSubmodule B)
hx : x✝ ∈ {x, y}
this : Submodule.inclusion hM = Submodule.inclusion hA ∘ₗ Submodule.inclusion ⋯
⊢ x✝ ∈ ↑(LinearMap.rTensor (↥(toSubmodule B)) (Submodule.inclusion hA)).range
Module: Mathlib.FieldTheory.RatFunc.IntermediateField

Goal state before:
pp: case h
K : Type u_1
inst✝ : Field K
f : K⟮X⟯
hf : ↑((f.minpolyX ↥K⟮f⟯).coeff f.denom.natDegree) = 0
⊢ f = C (f.num.coeff f.denom.natDegree / f.denom.leadingCoeff)

Tactic:
rw [map_div₀, eq_div_iff ((_root_.map_ne_zero C).mpr
    (leadingCoeff_ne_zero.mpr f.denom_ne_zero)), eq_comm]

Goal state after:
case h
K : Type u_1
inst✝ : Field K
f : K⟮X⟯
hf : ↑((f.minpolyX ↥K⟮f⟯).coeff f.denom.natDegree) = 0
⊢ C (f.num.coeff f.denom.natDegree) = f * C f.denom.leadingCoeff
Module: Mathlib.FieldTheory.RatFunc.IntermediateField

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

Tactic:
exact max_le (natDegree_num_le_natDegree_minpolyX f hf) <| le_natDegree_of_ne_zero
      fun H ↦ hf (f.eq_C_of_minpolyX_coeff_eq_zero congr($(H).val))

Goal state after:
Module: Mathlib.FieldTheory.Relrank

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

Tactic:
simpa only [lift_id] using lift_relrank_map_map A B f

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_cases h : E = ⊥

Goal state after:
case pos
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E = ⊥
⊢ generator E ∈ E

case neg
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : ¬E = ⊥
⊢ generator E ∈ E
Module: Mathlib.FieldTheory.Relrank

Goal state before:
pp: E : Type v
inst✝ : Field E
A B C : Subfield E
h1 : A ≤ B
h2 : B ≤ C
⊢ A.relrank B * B.relrank C = A.relrank C

Tactic:
have h3 := h1.trans h2

Goal state after:
E : Type v
inst✝ : Field E
A B C : Subfield E
h1 : A ≤ B
h2 : B ≤ C
h3 : A ≤ C
⊢ A.relrank B * B.relrank C = A.relrank C
Module: Mathlib.FieldTheory.Relrank

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
L : Type v
inst✝¹ : Field L
inst✝ : Algebra F L
f : E →ₐ[F] L
⊢ (map f A).relrank (map f B) = A.relrank B

Tactic:
simpa only [lift_id] using lift_relrank_map_map A B f

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 ≠ ⊥
⊢ Q₀ E ≠ 0

Tactic:
by
  apply mul_ne_zero
  · exact C_ne_zero.mpr (div_ne_zero (algebraMap_ne_zero (generator E).denom_ne_zero) (c_ne_zero h))
  · exact Polynomial.map_ne_zero (q_ne_zero h)

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

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

Tactic:
by_cases h : E = ⊥

Goal state after:
case pos
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E = ⊥
⊢ E = K⟮generator E⟯

case neg
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : ¬E = ⊥
⊢ E = K⟮generator E⟯
Module: Mathlib.Geometry.Euclidean.Projection

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace 𝕜 V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace 𝕜 P
inst✝¹ : Nonempty ↥s
inst✝ : s.direction.HasOrthogonalProjection
p x : P
hx : x ∈ s
⊢ ↑(s.direction.orthogonalProjectionOnto (p -ᵥ x - (p -ᵥ ↑(Classical.arbitrary ↥s)))) = ↑(Classical.arbitrary ↥s) -ᵥ x

Tactic:
vsub_sub_vsub_cancel_left,

Goal state after:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace 𝕜 V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace 𝕜 P
inst✝¹ : Nonempty ↥s
inst✝ : s.direction.HasOrthogonalProjection
p x : P
hx : x ∈ s
⊢ ↑(s.direction.orthogonalProjectionOnto (↑(Classical.arbitrary ↥s) -ᵥ x)) = ↑(Classical.arbitrary ↥s) -ᵥ x