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

Goal state before:
pp: case all.h₂.refine_1
α : 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
k : ℕ
φ : L.BoundedFormula β (k + 1)
ih :
  ∀ (v : Fin (k + 1) → (a : α) → M a),
    (φ.Realize (fun i ↦ Quotient.mk' (x i)) fun i ↦ Quotient.mk' (v i)) ↔
      ∀ᶠ (a : α) in ↑u, φ.Realize (fun i ↦ x i a) fun i ↦ v i a
v : Fin k → (a : α) → M a
h' : ∀ (m : (a : α) → M a) (a : α), (fun i ↦ Fin.snoc v m i a) = Fin.snoc (fun i ↦ v i a) (m a)
h : ∀ᶠ (x_1 : α) in ↑u, ∃ x_2, ¬φ.Realize (fun i ↦ x i x_1) (Fin.snoc (fun i ↦ v i x_1) x_2)
⊢ ∃ m, ∀ᶠ (x_1 : α) in ↑u, ¬φ.Realize (fun i ↦ x i x_1) (Fin.snoc (fun i ↦ v i x_1) (m x_1))

Tactic:
refine
        ⟨fun a : α =>
          Classical.epsilon fun m : M a =>
            ¬φ.Realize (fun i => x i a) (Fin.snoc (fun i => v i a) m),
          ?_⟩

Goal state after:
case all.h₂.refine_1
α : 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
k : ℕ
φ : L.BoundedFormula β (k + 1)
ih :
  ∀ (v : Fin (k + 1) → (a : α) → M a),
    (φ.Realize (fun i ↦ Quotient.mk' (x i)) fun i ↦ Quotient.mk' (v i)) ↔
      ∀ᶠ (a : α) in ↑u, φ.Realize (fun i ↦ x i a) fun i ↦ v i a
v : Fin k → (a : α) → M a
h' : ∀ (m : (a : α) → M a) (a : α), (fun i ↦ Fin.snoc v m i a) = Fin.snoc (fun i ↦ v i a) (m a)
h : ∀ᶠ (x_1 : α) in ↑u, ∃ x_2, ¬φ.Realize (fun i ↦ x i x_1) (Fin.snoc (fun i ↦ v i x_1) x_2)
⊢ ∀ᶠ (x_1 : α) in ↑u,
    ¬φ.Realize (fun i ↦ x i x_1)
        (Fin.snoc (fun i ↦ v i x_1)
          ((fun a ↦ Classical.epsilon fun m ↦ ¬φ.Realize (fun i ↦ x i a) (Fin.snoc (fun i ↦ v i a) m)) x_1))
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case var
L : Language
α : Type u'
l✝ : List (L.Term α)
a✝ : α
l : List (α ⊕ (i : ℕ) × L.Functions i)
⊢ listDecode ((var a✝).listEncode ++ l) = var a✝ :: listDecode l

Tactic:
rw [listEncode, singleton_append, listDecode]

Goal state after:
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
n : ℕ
f : L.Functions n
x : Fin n → M
hx : ∀ (i : Fin n), x i ∈ range (Term.realize Subtype.val)
⊢ funMap f x ∈ range (Term.realize Subtype.val)

Tactic:
by
    simp only [mem_range] at *
    refine ⟨func f fun i => Classical.choose (hx i), ?_⟩
    simp only [Term.realize, fun i => Classical.choose_spec (hx i)]

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:
rw [listEncode, singleton_append, listDecode]

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case succ.mpr
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n✝ : ℕ
v : α → M
n : ℕ
ih : ∀ {φ : L.BoundedFormula α n}, φ.exs.Realize v ↔ ∃ xs, φ.Realize v xs
φ : L.BoundedFormula α (n + 1)
xs : Fin (n + 1) → M
h : φ.Realize v xs
⊢ ∃ xs a, φ.Realize v (snoc xs a)

Tactic:
rw [← Fin.snoc_init_self xs] at h

Goal state after:
case succ.mpr
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n✝ : ℕ
v : α → M
n : ℕ
ih : ∀ {φ : L.BoundedFormula α n}, φ.exs.Realize v ↔ ∃ xs, φ.Realize v xs
φ : L.BoundedFormula α (n + 1)
xs : Fin (n + 1) → M
h : φ.Realize v (snoc (init xs) (xs (last n)))
⊢ ∃ xs a, φ.Realize v (snoc xs a)
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : Finite β
φ : L.Formula (α ⊕ β)
v : α → M
v' : Fin 0 → M
⊢ Realize (Formula.iAlls β φ) v v' ↔ ∀ (i : β → M), φ.Realize fun a ↦ Sum.elim v i a

Tactic:
← Formula.realize_iAlls,

Goal state after:
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : Finite β
φ : L.Formula (α ⊕ β)
v : α → M
v' : Fin 0 → M
⊢ Realize (Formula.iAlls β φ) v v' ↔ (Formula.iAlls β φ).Realize v
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝² : L.Structure M
α : Type u₁
s : Set (α → M)
L' : Language
inst✝¹ : L'.Structure M
h : A.Definable L s
φ : L →ᴸ L'
inst✝ : φ.IsExpansionOn M
⊢ A.Definable L' s

Tactic:
obtain ⟨ψ, rfl⟩ := h
  refine ⟨(φ.addConstants A).onFormula ψ, ?_⟩
  ext x
  simp only [mem_ofPred_eq, LHom.realize_onFormula]

Goal state after:
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
β : Type u_1
f : α → β
s : Set (α → M)
h : A.Definable L s
⊢ A.Definable L ((fun g ↦ g ∘ f) ⁻¹' s)

Tactic:
obtain ⟨φ, rfl⟩ := h

Goal state after:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
β : Type u_1
f : α → β
φ : L[[↑A]].Formula α
⊢ A.Definable L ((fun g ↦ g ∘ f) ⁻¹' ofPred φ.Realize)
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
m : ℕ
s : Set (α ⊕ Fin m → M)
h : A.Definable L s
⊢ A.Definable L ((fun g ↦ g ∘ Sum.inl) '' s)

Tactic:
obtain ⟨φ, rfl⟩ := h

Goal state after:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
m : ℕ
φ : L[[↑A]].Formula (α ⊕ Fin m)
⊢ A.Definable L ((fun g ↦ g ∘ Sum.inl) '' ofPred φ.Realize)
Module: Mathlib.ModelTheory.Skolem

Goal state before:
pp: L : Language
| fun i ↦ lift.{u, max u v} #(L.BoundedFormula Empty (i + 1))

Tactic:
i

Goal state after:
L : Language
i : ℕ
| lift.{u, max u v} #(L.BoundedFormula Empty (i + 1))
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: L : Language
α : Type u'
inst✝¹ : Countable α
inst✝ : Countable L.Symbols
⊢ lift.{max u v, u'} #α + lift.{u', max u v} L.card ≤ ℵ₀

Tactic:
simp only [card, add_le_aleph0, lift_le_aleph0, mk_le_aleph0_iff]

Goal state after:
L : Language
α : Type u'
inst✝¹ : Countable α
inst✝ : Countable L.Symbols
⊢ Countable α ∧ Countable L.Symbols
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
⊢ M ⊨ L.infiniteTheory ↔ Infinite M

Tactic:
by
  simp [infiniteTheory, infinite_iff, aleph0_le]

Goal state after:
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
f : (α → M) → M
h : A.TermDefinable L f
⊢ A.Definable L (Function.tupleGraph f)

Tactic:
obtain ⟨φ, rfl⟩ := h

Goal state after:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
φ : L[[↑A]].Term α
⊢ A.Definable L (Function.tupleGraph fun v ↦ Term.realize v φ)
Module: Mathlib.RingTheory.MvPolynomial.FreeCommRing

Goal state before:
pp: ι : Type u_1
κ : Type u_2
R : Type u_3
inst✝² : DecidableEq κ
inst✝¹ : CommRing R
inst✝ : DecidableEq R
monoms : ι → Finset (κ →₀ ℕ)
p : { p // ∀ (i : ι), (p i).support ⊆ monoms i }
i : ι
m : κ →₀ ℕ
hm : m ∉ monoms i
this : m ∉ (↑p i).support
⊢ 0 = (↑p i).coeff m

Tactic:
simpa [coeff, eq_comm, MvPolynomial.mem_support_iff] using this

Goal state after:
Module: Mathlib.ModelTheory.Algebra.Ring.Definability

Goal state before:
pp: ι : Type u_1
K : Type u_2
inst✝¹ : Field K
inst✝ : CompatibleRing K
S : Finset (MvPolynomial ι K)
p' : ↥S → FreeCommRing ((i : ↥S) × ↥(↑i).support ⊕ ι) := genericPolyMap fun p ↦ (↑p).support
this✝ : DecidableEq ι := Classical.decEq ι
this : DecidableEq K := Classical.decEq K
i : ↥S
p : (i : ↥S) × ↥(↑i).support
⊢ ∃ i, ∃ (_ : i ∈ S), coeff ↑p.snd ↑p.fst ∈ (fun m ↦ coeff m i) '' ↑i.support

Tactic:
exact ⟨p.1.1, p.1.2, Set.mem_image_of_mem _ p.2.2⟩

Goal state after:
Module: Mathlib.LinearAlgebra.FreeAlgebra

Goal state before:
pp: case inr
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : Set S
h✝ : Nontrivial R
⊢ lift.{max u v, v} (Module.rank R ↥((FreeAlgebra.lift R) Subtype.val).range) ≤ lift.{max u v, v} (max #↑s ℵ₀)

Tactic:
refine (lift_rank_range_le (FreeAlgebra.lift R ((↑) : s → S)).toLinearMap).trans ?_

Goal state after:
case inr
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : Set S
h✝ : Nontrivial R
⊢ lift.{v, max u v} (Module.rank R (FreeAlgebra R { x // x ∈ s })) ≤ lift.{max u v, v} (max #↑s ℵ₀)
Module: Mathlib.GroupTheory.OreLocalization.Cardinality

Goal state before:
pp: R : Type u
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
⊢ #↥S ≤ #R

Tactic:
mk_subtype_le

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Divisibility

Goal state before:
pp: case inl
h : IsUnit 0
⊢ 0 = 1

Tactic:
exact (not_isUnit_zero h).elim

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
⊢ f.natDegree ∣ n

Tactic:
let ⟨p, hp⟩ := CharP.exists k

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
⊢ f.natDegree ∣ n
Module: Mathlib.FieldTheory.Finite.Extension

Goal state before:
pp: case inr.inl.refine_2
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
⊢ Polynomial.map (algebraMap k (Extension k p n)) (X ^ Nat.card k ^ n - X) ≠ 0

Tactic:
exact map_ne_zero (X_pow_card_pow_sub_X_ne_zero _ hn Finite.one_lt_card)

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)
⊢ (aeval a) (X ^ Nat.card k ^ f.natDegree - X) = 0

Tactic:
let ⟨p, hp⟩ := CharP.exists k

Goal state after:
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
⊢ (aeval a) (X ^ Nat.card k ^ f.natDegree - X) = 0
Module: Mathlib.FieldTheory.Finite.Polynomial

Goal state before:
pp: K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : Field K
a b : σ → K
h : a ≠ b
i : σ
hi : a i ≠ b i
⊢ 1 - (a i - b i) ^ (Fintype.card K - 1) = 0

Tactic:
rw [FiniteField.pow_card_sub_one_eq_one, sub_self]

Goal state after:
case ha
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : Field K
a b : σ → K
h : a ≠ b
i : σ
hi : a i ≠ b i
⊢ a i - b i ≠ 0
Module: Mathlib.FieldTheory.Finite.Polynomial

Goal state before:
pp: σ K : Type u
inst✝² : Fintype K
inst✝¹ : Field K
inst✝ : Finite σ
⊢ (evalᵢ σ K).range = ⊤

Tactic:
by
  rw [evalᵢ, LinearMap.range_comp, range_subtype]
  exact map_restrict_dom_evalₗ K σ

Goal state after:
Module: Mathlib.Topology.Separation.Connected

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : PreconnectedSpace X
inst✝ : DiscreteTopology X
x y : X
hxy : ¬x = y
⊢ False

Tactic:
← mem_singleton_iff,

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : PreconnectedSpace X
inst✝ : DiscreteTopology X
x y : X
hxy : x ∉ {y}
⊢ False
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
a : PerfectClosure K p
x✝ : ℕ × K
m : ℕ
x : K
⊢ 0 * Quot.mk (R K p) (m, x) = 0

Tactic:
rw [zero_def, quot_mk_eq_mk, mk_mul_mk]

Goal state after:
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
a : PerfectClosure K p
x✝ : ℕ × K
m : ℕ
x : K
⊢ mk K p ((0, 0).1 + (m, x).1, (⇑(frobenius K p))^[(m, x).1] (0, 0).2 * (⇑(frobenius K p))^[(0, 0).1] (m, x).2) =
    mk K p (0, 0)
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
a : PerfectClosure K p
x✝ : ℕ × K
m : ℕ
x : K
⊢ Quot.mk (R K p) (m, x) * 0 = 0

Tactic:
rw [zero_def, quot_mk_eq_mk, mk_mul_mk]

Goal state after:
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
a : PerfectClosure K p
x✝ : ℕ × K
m : ℕ
x : K
⊢ mk K p ((m, x).1 + (0, 0).1, (⇑(frobenius K p))^[(0, 0).1] (m, x).2 * (⇑(frobenius K p))^[(m, x).1] (0, 0).2) =
    mk K p (0, 0)
Module: Mathlib.FieldTheory.Laurent

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

Tactic:
laurentAux_div,

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) / (algebraMap R[X] R⟮X⟯) ((taylor r) 1) = RatFunc.mk ((taylor r) p) 1
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
⊢ False

Tactic:
let _ : Invertible c := ⟨c⁻¹, inv_mul_cancel₀ hb.1, mul_inv_cancel₀ hb.1⟩

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 := ⋯ }
⊢ False
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
⊢ ∃ k ∈ s, (H k).FiniteIndex

Tactic:
classical
  have ⟨j, hj⟩ : s.Nonempty := by
    by_contra! rfl
    rw [← Finset.set_biUnion_coe, Finset.coe_empty, Set.biUnion_empty] at hcovers
    exact Set.empty_ne_univ hcovers
  by_cases hcovers' : ⋃ i ∈ s.filter (H · = H j), g i • (H i : Set G) = Set.univ
  · rw [Set.iUnion₂_congr fun i hi => by rw [(Finset.mem_filter.mp hi).right]] at hcovers'
    exact ⟨j, hj, finiteIndex_of_leftCoset_cover_const hcovers'⟩
  · have ⟨i, hi, _, hfi⟩ :=
      exists_finiteIndex_of_leftCoset_cover_aux hcovers j hj hcovers'
    exact ⟨i, hi, hfi⟩

Goal state after:
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: case refine_3
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
k : κ
hkfi : (H ↑k.fst).FiniteIndex
hk : K k = D
hcovers' : ⋃ i ∈ {x | K x = D}, f i • ↑D = Set.univ
hHD : ∀ (i : ι), ¬(H i).FiniteIndex → H i ≠ D
hdensity : ∑ i ∈ s, (↑(H i).index)⁻¹ = ↑{x | K x = D}.card * (↑D.index)⁻¹
h : {x | K x = D}.card = D.index
⊢ {x | x ∈ s ∧ (H x).FiniteIndex}.PairwiseDisjoint fun i ↦ g i • ↑(H i)

Tactic:
i

Goal state after:
case refine_3
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
k : κ
hkfi : (H ↑k.fst).FiniteIndex
hk : K k = D
hcovers' : ⋃ i ∈ {x | K x = D}, f i • ↑D = Set.univ
hHD : ∀ (i : ι), ¬(H i).FiniteIndex → H i ≠ D
hdensity : ∑ i ∈ s, (↑(H i).index)⁻¹ = ↑{x | K x = D}.card * (↑D.index)⁻¹
h : {x | K x = D}.card = D.index
i : ι
⊢ i ∈ {x | x ∈ s ∧ (H x).FiniteIndex} →
    ∀ ⦃y : ι⦄, y ∈ {x | x ∈ s ∧ (H x).FiniteIndex} → i ≠ y → Function.onFun Disjoint (fun i ↦ g i • ↑(H i)) i y
Module: Mathlib.FieldTheory.Minpoly.ConjRootClass

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
⊢ carrier 0 = {0}

Tactic:
ext; rw [mem_carrier, mk_eq_zero_iff, Set.mem_singleton_iff]

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

Goal state before:
pp: k : Type u_1
inst✝¹ : Field k
p : ℕ
inst✝ : ExpChar k p
⊢ IsPurelyInseparable k (AdjoinPthRoots k)

Tactic:
obtain ⟨p, hp⟩ := ExpChar.exists k

Goal state after:
k : Type u_1
inst✝¹ : Field k
p✝ : ℕ
inst✝ : ExpChar k p✝
p : ℕ
hp : ExpChar k p
⊢ IsPurelyInseparable k (AdjoinPthRoots k)
Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure

Goal state before:
pp: case refine_1
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
i : E →ₐ[F] K
x : E
x✝ : ∃ n, i x ^ ringExpChar F ^ n ∈ (algebraMap F K).range
n : ℕ
y : F
h : (algebraMap F K) y = i x ^ ringExpChar F ^ n
⊢ (algebraMap F E) y = x ^ ringExpChar F ^ n

Tactic:
apply_fun i using i.injective

Goal state after:
case refine_1
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
i : E →ₐ[F] K
x : E
x✝ : ∃ n, i x ^ ringExpChar F ^ n ∈ (algebraMap F K).range
n : ℕ
y : F
h : (algebraMap F K) y = i x ^ ringExpChar F ^ n
⊢ i ((algebraMap F E) y) = i (x ^ ringExpChar F ^ n)
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
hi :
  i =
    (fa.range.mulMap fb.range).comp
      ↑(Algebra.TensorProduct.congr (AlgEquiv.ofInjective fa ⋯) (AlgEquiv.ofInjective fb ⋯))
H : Function.Injective ⇑(Ideal.Quotient.mk M)
⊢ M = ⊥

Tactic:
rwa [RingHom.injective_iff_ker_eq_bot, Ideal.mk_ker] at H

Goal state after:
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) / C f.denom.leadingCoeff

Tactic:
eq_div_iff ((_root_.map_ne_zero C).mpr
    (leadingCoeff_ne_zero.mpr f.denom_ne_zero)),

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
⊢ f * C f.denom.leadingCoeff = C (f.num.coeff f.denom.natDegree)
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
⊢ LinearIndependent E v

Tactic:
obtain ⟨q, _⟩ := ExpChar.exists F
  have := expChar_of_injective_algebraMap (algebraMap F K).injective q
  refine linearIndependent_iff.mpr fun l hl ↦ Finsupp.ext fun i ↦ ?_
  choose f hf using fun i ↦ (isPurelyInseparable_iff_pow_mem F q).1 ‹_› (l i)
  let n := l.support.sup f
  have := (expChar_pow_pos F q n).ne'
  replace hf (i : ι) : l i ^ q ^ n ∈ (algebraMap F E).range := by
    by_cases hs : i ∈ l.support
    · 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)]
    exact ⟨0, by rw [map_zero, Finsupp.notMem_support_iff.1 hs, zero_pow this]⟩
  choose lF hlF using hf
  let lF₀ := Finsupp.onFinset l.support lF fun i ↦ by
    contrapose
    refine fun hs ↦ (injective_iff_map_eq_zero _).mp (algebraMap F E).injective _ ?_
    rw [hlF, Finsupp.notMem_support_iff.1 hs, zero_pow this]
  replace h := linearIndependent_iff.1 (h.map_pow_expChar_pow_of_isSeparable' q n hsep :) lF₀ <| by
    replace hl := congr($hl ^ q ^ n)
    rw [Finsupp.linearCombination_apply, Finsupp.sum, sum_pow_char_pow, zero_pow this] at hl
    rw [← hl, Finsupp.linearCombination_apply,
      Finsupp.onFinset_sum _ (fun _ ↦ by exact zero_smul _ _)]
    refine Finset.sum_congr rfl fun i _ ↦ ?_
    simp_rw [Algebra.smul_def, mul_pow, IsScalarTower.algebraMap_apply F E K, hlF, map_pow]
  refine eq_zero_of_pow_eq_zero ((hlF _).symm.trans ?_)
  convert! map_zero (algebraMap F E)
  exact congr($h i)

Goal state after:
Module: Mathlib.FieldTheory.Relrank

Goal state before:
pp: E : Type v
inst✝ : Field E
A B : Subfield E
⊢ B = A ⊓ B ↔ B ≤ A

Tactic:
right_eq_inf

Goal state after:
E : Type v
inst✝ : Field E
A B : Subfield E
⊢ B ≤ A ↔ B ≤ A
Module: Mathlib.FieldTheory.RatFunc.Luroth

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
| (algebraMap K[X] K⟮X⟯) (c E).num / (algebraMap K[X] K⟮X⟯) (c E).denom

Tactic:
c_denom h,

Goal state after:
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
| (algebraMap K[X] K⟮X⟯) (c E).num / (algebraMap K[X] K⟮X⟯) 1
Module: Mathlib.FieldTheory.RatFunc.Luroth

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
this :
  (algebraMap K[X] K⟮X⟯) (c E).num / (algebraMap K[X] K⟮X⟯) (c E).denom * ↑((φ E).coeff (generatorIndex h)) =
    (algebraMap K[X] K⟮X⟯) ((Φ E).coeff (generatorIndex h))
⊢ (algebraMap K[X] K⟮X⟯) ((Φ E).coeff (generatorIndex h)) = (algebraMap K[X] K⟮X⟯) (c E).num * generator E

Tactic:
c_denom h,

Goal state after:
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
this :
  (algebraMap K[X] K⟮X⟯) (c E).num / (algebraMap K[X] K⟮X⟯) 1 * ↑((φ E).coeff (generatorIndex h)) =
    (algebraMap K[X] K⟮X⟯) ((Φ E).coeff (generatorIndex h))
⊢ (algebraMap K[X] K⟮X⟯) ((Φ E).coeff (generatorIndex h)) = (algebraMap K[X] K⟮X⟯) (c E).num * generator E
Module: Mathlib.FieldTheory.RatFunc.Luroth

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ m E ≤ (Bivariate.swap (∑ n ∈ (Φ E).support, (monomial n) ((Φ E).coeff n))).natDegree

Tactic:
map_sum

Goal state after:
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ m E ≤ (∑ x ∈ (Φ E).support, Bivariate.swap ((monomial x) ((Φ E).coeff x))).natDegree
Module: Mathlib.Geometry.Convex.Hull

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

Tactic:
← Set.Nonempty.subset_singleton_iff,

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

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