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

Goal state before:
pp: L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
n✝ : ℕ
φ : L[[α]].BoundedFormula β n✝
v : β → M
xs✝ : Fin n✝ → M
n : ℕ
R : L[[α]].Relations n
xs : Fin n → M
⊢ RelMap ((L.lhomWithConstants α).onRelation ((Equiv.sumEmpty (L.Relations n) ((constantsOn α).Relations n)) R)) xs =
    RelMap R xs

Tactic:
rcongr

Goal state after:
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
n✝ : ℕ
φ : L[[α]].BoundedFormula β n✝
v : β → M
xs✝ : Fin n✝ → M
n : ℕ
R : L[[α]].Relations n
xs : Fin n → M
⊢ RelMap ((L.lhomWithConstants α).onRelation ((Equiv.sumEmpty (L.Relations n) ((constantsOn α).Relations n)) R)) xs ↔
    RelMap R xs
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
ι : Type u_3
hι : Nonempty ι
S : ι → L.Substructure M
hS : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x : M
⊢ x ∈ ⨆ i, S i ↔ ∃ i, x ∈ S i

Tactic:
refine ⟨?_, fun ⟨i, hi⟩ ↦ le_iSup S i hi⟩

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
ι : Type u_3
hι : Nonempty ι
S : ι → L.Substructure M
hS : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x : M
⊢ x ∈ ⨆ i, S i → ∃ i, x ∈ S i
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
β : Type v'
φ : L.Formula α
g : α → β
v : β → M
⊢ (relabel g φ).Realize v ↔ φ.Realize (v ∘ g)

Tactic:
rw [Realize, Realize, relabel, BoundedFormula.realize_relabel, iff_eq_eq, Fin.castAdd_zero]
  exact congr rfl (funext finZeroElim)

Goal state after:
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : L.Structure M
inst✝¹ : L.Structure N
inst✝ : L.Structure P
S✝ : L.Substructure M
s : Set M
φ : M →[L] N
S : L.Substructure N
n : ℕ
f : L.Functions n
x : Fin n → M
hx : ∀ (i : Fin n), x i ∈ ⇑φ ⁻¹' ↑S
⊢ φ (funMap f x) ∈ ↑S

Tactic:
φ.map_fun

Goal state after:
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : L.Structure M
inst✝¹ : L.Structure N
inst✝ : L.Structure P
S✝ : L.Substructure M
s : Set M
φ : M →[L] N
S : L.Substructure N
n : ℕ
f : L.Functions n
x : Fin n → M
hx : ∀ (i : Fin n), x i ∈ ⇑φ ⁻¹' ↑S
⊢ funMap f (⇑φ ∘ x) ∈ ↑S
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
e : β ≃ Fin (Classical.choose ⋯) := Classical.choice ⋯
⊢ (relabel (fun a ↦ Sum.map id (⇑(Classical.choice ⋯)) a) φ).alls.Realize v ↔
    ∀ (i : β → M), φ.Realize fun a ↦ Sum.elim v i a

Tactic:
simp only [Nat.add_zero, realize_alls, realize_relabel, Function.comp_def,
    castAdd_zero, Sum.elim_map, id_eq]

Goal state after:
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : Finite β
φ : L.Formula (α ⊕ β)
v : α → M
e : β ≃ Fin (Classical.choose ⋯) := Classical.choice ⋯
⊢ (∀ (xs : Fin (Classical.choose ⋯) → M),
      Realize φ (fun x ↦ Sum.elim (fun x ↦ v x) (fun x ↦ xs (Fin.cast ⋯ ((Classical.choice ⋯) x))) x) fun x ↦
        xs (natAdd (Classical.choose ⋯) x)) ↔
    ∀ (i : β → M), φ.Realize fun a ↦ Sum.elim v i a
Module: Mathlib.ModelTheory.Skolem

Goal state before:
pp: case refine_1
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
κ : Cardinal.{w'}
h3 : lift.{w', max u v} L.card ≤ lift.{max u v, w'} κ
h4 : lift.{w, w'} κ ≤ lift.{w', w} #M
s' : Set (ULift.{w', w} M)
h2 : lift.{w', w} #↑s ≤ #↑s'
h1 : ℵ₀ ≤ #↑s'
hs' : #↑s' = lift.{w, w'} κ
this : Nonempty M
h : lift.{w', w} #↑(⇑Equiv.ulift '' s') = #↑s'
⊢ #↑s + #↑(⇑Equiv.ulift '' s') ≤ #↑(⇑Equiv.ulift '' s')

pp: case refine_2
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
κ : Cardinal.{w'}
h3 : lift.{w', max u v} L.card ≤ lift.{max u v, w'} κ
h4 : lift.{w, w'} κ ≤ lift.{w', w} #M
s' : Set (ULift.{w', w} M)
h2 : lift.{w', w} #↑s ≤ #↑s'
h1 : ℵ₀ ≤ #↑s'
hs' : #↑s' = lift.{w, w'} κ
this : Nonempty M
h : lift.{w', w} #↑(⇑Equiv.ulift '' s') = #↑s'
⊢ lift.{w, max v u} (max ℵ₀ L.card) ≤ lift.{max u v, w} #↑(⇑Equiv.ulift '' s')

Tactic:
· rw [← lift_le, lift_add, h, add_comm, add_eq_max h1]
      exact max_le le_rfl h2

Goal state after:
case refine_2
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
κ : Cardinal.{w'}
h3 : lift.{w', max u v} L.card ≤ lift.{max u v, w'} κ
h4 : lift.{w, w'} κ ≤ lift.{w', w} #M
s' : Set (ULift.{w', w} M)
h2 : lift.{w', w} #↑s ≤ #↑s'
h1 : ℵ₀ ≤ #↑s'
hs' : #↑s' = lift.{w, w'} κ
this : Nonempty M
h : lift.{w', w} #↑(⇑Equiv.ulift '' s') = #↑s'
⊢ lift.{w, max v u} (max ℵ₀ L.card) ≤ lift.{max u v, w} #↑(⇑Equiv.ulift '' s')
Module: Mathlib.ModelTheory.Semantics

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

Tactic:
by
  simp only [nonemptyTheory, Theory.model_iff, Set.mem_singleton_iff, forall_eq,
    Sentence.realize_cardGe, Nat.cast_one, Cardinal.one_le_iff_ne_zero, mk_ne_zero_iff]

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
α : Type u'
M : Type w
inst✝ : L[[α]].Structure M
s : Set α
⊢ (∀ (φ : L[[α]].Sentence) (x x_1 : α),
      (x, x_1) ∈ s ×ˢ s ∩ (Set.diagonal α)ᶜ → ((L.con x).term.equal (L.con x_1).term).not = φ → M ⊨ φ) ↔
    Set.InjOn (fun i ↦ ↑(L.con i)) s

Tactic:
refine ⟨fun h a as b bs ab => ?_, ?_⟩

Goal state after:
case refine_1
L : Language
α : Type u'
M : Type w
inst✝ : L[[α]].Structure M
s : Set α
h :
  ∀ (φ : L[[α]].Sentence) (x x_1 : α),
    (x, x_1) ∈ s ×ˢ s ∩ (Set.diagonal α)ᶜ → ((L.con x).term.equal (L.con x_1).term).not = φ → M ⊨ φ
a : α
as : a ∈ s
b : α
bs : b ∈ s
ab : (fun i ↦ ↑(L.con i)) a = (fun i ↦ ↑(L.con i)) b
⊢ a = b

case refine_2
L : Language
α : Type u'
M : Type w
inst✝ : L[[α]].Structure M
s : Set α
⊢ Set.InjOn (fun i ↦ ↑(L.con i)) s →
    ∀ (φ : L[[α]].Sentence) (x x_1 : α),
      (x, x_1) ∈ s ×ˢ s ∩ (Set.diagonal α)ᶜ → ((L.con x).term.equal (L.con x_1).term).not = φ → M ⊨ φ
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: case refine_2
L : Language
T : L.Theory
α : Type w
n : ℕ
φ : L.BoundedFormula α n
⊢ T ⊨ᵇ φ → T ⊨ᵇ φ.toFormula

Tactic:
simp only [models_formula_iff, BoundedFormula.realize_toFormula]
    exact fun h M v => h M _ _

Goal state after:
Module: Mathlib.RingTheory.Nullstellensatz

Goal state before:
pp: k : Type u_1
K : Type u_2
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
σ : Type u_3
x : σ → K
⊢ Function.Surjective ⇑(aeval x)

Tactic:
intro z; use C z; simp

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: case inl
L : Language
T : L.Theory
h : T.IsComplete
φ : L.Sentence
M : Type u_1
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
hφ : T ⊨ᵇ φ
⊢ M ⊨ φ ↔ T ⊨ᵇ φ

pp: case inr
L : Language
T : L.Theory
h : T.IsComplete
φ : L.Sentence
M : Type u_1
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
hφn : T ⊨ᵇ Formula.not φ
⊢ M ⊨ φ ↔ T ⊨ᵇ φ

Tactic:
· exact iff_of_true (hφ.realize_sentence M) hφ

Goal state after:
case inr
L : Language
T : L.Theory
h : T.IsComplete
φ : L.Sentence
M : Type u_1
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
hφn : T ⊨ᵇ Formula.not φ
⊢ M ⊨ φ ↔ T ⊨ᵇ φ
Module: Mathlib.SetTheory.Cardinal.Divisibility

Goal state before:
pp: a : Cardinal.{u}
ha : ℵ₀ ≤ a
⊢ ¬¬IsUnit a ∨ ¬∀ ⦃a_1 b : Cardinal.{u}⦄, a = a_1 * b → IsUnit a_1 ∨ IsUnit b

Tactic:
refine Or.inr fun h => ?_

Goal state after:
a : Cardinal.{u}
ha : ℵ₀ ≤ a
h : ∀ ⦃a_1 b : Cardinal.{u}⦄, a = a_1 * b → IsUnit a_1 ∨ IsUnit b
⊢ False
Module: Mathlib.SetTheory.Cardinal.Divisibility

Goal state before:
pp: case inr.inr
n m k : ℕ
hk : ↑m = ↑n * ↑k
⊢ n ∣ m

Tactic:
exact ⟨k, mod_cast hk⟩

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
inst✝ : Algebra (ZMod p) k
⊢ Module.finrank (ZMod p) (Extension k p n) = Module.finrank (ZMod p) k * n

Tactic:
let := ZMod.algebra k p
  unfold Extension
  convert!
    GaloisField.finrank p (n := Module.finrank (ZMod p) k * n) <|
      mul_ne_zero Module.finrank_pos.ne' <| NeZero.ne n
  subsingleton

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

Goal state before:
pp: K : Type u_1
σ : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Finite σ
⊢ Submodule.map (evalₗ K σ) (restrictDegree σ K (Fintype.card K - 1)) = ⊤

Tactic:
cases nonempty_fintype σ
  refine top_unique (SetLike.le_def.2 fun e _ => mem_map.2 ?_)
  classical
  refine ⟨∑ n : σ → K, e n • indicator n, ?_, ?_⟩
  · exact sum_mem fun c _ => smul_mem _ _ (indicator_mem_restrictDegree _)
  · ext n
    simp only [evalₗ_apply, map_sum, smul_eval]
    rw [Finset.sum_eq_single n] <;>
      aesop (add simp [eval_indicator_apply_eq_zero, eval_indicator_apply_eq_one, eq_comm])

Goal state after:
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
hi : ¬Nonempty ↑(Iio i)
⊢ filtration i = ⊥

Tactic:
cases i
  · have := mk_ne_zero_iff.mp (rank_pos.trans_eq (mk_ord_toType <| Module.rank F E).symm).ne'
    rw [← range_coe] at hi; exact (hi inferInstance).elim
  · exact bot_unique <| adjoin_le_iff.mpr fun _ ⟨j, hj, _⟩ ↦ (hi ⟨j, coe_lt_coe.mpr hj⟩).elim

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

Goal state before:
pp: k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : Normal k ↥L
⊢ ∀ A ∈ nhds ((AlgEquiv.restrictNormalHom ↥L) 1), ⇑(AlgEquiv.restrictNormalHom ↥L) ⁻¹' A ∈ nhds 1

Tactic:
intro N hN

Goal state after:
k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : Normal k ↥L
N : Set Gal(↥L/k)
hN : N ∈ nhds ((AlgEquiv.restrictNormalHom ↥L) 1)
⊢ ⇑(AlgEquiv.restrictNormalHom ↥L) ⁻¹' N ∈ nhds 1
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: case succ
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
ih : mk K p (n, 0) = 0
⊢ mk K p (n + 1, 0) = 0

Tactic:
← ih

Goal state after:
case succ
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
ih : mk K p (n, 0) = 0
⊢ mk K p (n + 1, 0) = mk K p (n, 0)
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✝ : PerfectClosure K p
x : ℕ × K
⊢ (of K p) x.2 = mk K p x ^ p ^ x.1

Tactic:
← iterate_frobenius,

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✝ : PerfectClosure K p
x : ℕ × K
⊢ (of K p) x.2 = (⇑(frobenius (PerfectClosure K p) p))^[x.1] (mk K p x)
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
D H : Subgroup G
inst✝ : D.FiniteIndex
hD_le_H : D ≤ H
⊢ ∃ t, IsComplement ↑t ↑(D.subgroupOf H) ∧ ⋃ g ∈ t, ↑g • ↑D = ↑H

Tactic:
have ⟨t, ht⟩ := (D.subgroupOf H).exists_isComplement_left 1
  have hf : t.Finite := ht.1.finite_left_iff.mpr inferInstance
  refine ⟨hf.toFinset, hf.coe_toFinset.symm ▸ ht.1, ?_⟩
  ext x
  suffices (∃ y ∈ t, ∃ d ∈ D, y * d = x) ↔ x ∈ H by simpa using! this
  constructor
  · rintro ⟨⟨y, hy⟩, -, d, h, rfl⟩
    exact H.mul_mem hy (hD_le_H h)
  · intro hx
    exact ⟨_, (ht.1.toLeftFun ⟨x, hx⟩).2, _,
      ht.1.inv_toLeftFun_mul_mem ⟨x, hx⟩, mul_inv_cancel_left _ _⟩

Goal state after:
Module: Mathlib.FieldTheory.MvRatFunc.Rank

Goal state before:
pp: case refine_2
σ : Type u
F : Type v
inst✝¹ : Field F
inst✝ : Nonempty σ
R : Type (max v u) := MvPolynomial σ F
K : Type (max u v) := FractionRing R
hinj : Function.Injective ⇑(algebraMap R K)
h1 : lift.{v, u} #σ ≤ Module.rank F K ∧ ℵ₀ ≤ Module.rank F K
i : σ
hx : Transcendental F ((algebraMap R K) (MvPolynomial.X i))
⊢ max (max (lift.{u, v} #F) (lift.{v, u} #σ)) ℵ₀ ≤ Module.rank F (FractionRing (MvPolynomial σ F))

Tactic:
have h2 := hx.linearIndependent_sub_inv.cardinal_lift_le_rank

Goal state after:
case refine_2
σ : Type u
F : Type v
inst✝¹ : Field F
inst✝ : Nonempty σ
R : Type (max v u) := MvPolynomial σ F
K : Type (max u v) := FractionRing R
hinj : Function.Injective ⇑(algebraMap R K)
h1 : lift.{v, u} #σ ≤ Module.rank F K ∧ ℵ₀ ≤ Module.rank F K
i : σ
hx : Transcendental F ((algebraMap R K) (MvPolynomial.X i))
h2 : lift.{max u v, v} #F ≤ lift.{v, max u v} (Module.rank F K)
⊢ max (max (lift.{u, v} #F) (lift.{v, u} #σ)) ℵ₀ ≤ Module.rank F (FractionRing (MvPolynomial σ F))
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: K : Type u
inst✝ : Field K
n : ℕ
ζ : K
hζ : IsPrimitiveRoot ζ n
α a : K
hn : 0 < n
e : α ^ n = a
⊢ X ^ n - C a = ∏ i ∈ Finset.range n, (X - C (ζ ^ i * α))

Tactic:
by
  rw [(X_pow_sub_C_splits_of_isPrimitiveRoot hζ e).eq_prod_roots_of_monic
    (monic_X_pow_sub_C _ hn.ne'), ← nthRoots, hζ.nthRoots_eq e, Multiset.map_map]
  rfl

Goal state after:
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: case hx
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
inst✝ : DecidablePred FiniteIndex
hcovers : ⋃ i ∈ {i ∈ s | (H i).FiniteIndex} ∪ {a ∈ s | ¬(H a).FiniteIndex}, g i • ↑(H i) = Set.univ
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
⊢ ⋃ x, ⋃ (hx : x ∈ s), ⋃ a, ⋃ (_ : ⟨⟨x, hx⟩, a⟩ ∈ {k | (H ↑k.fst).FiniteIndex}), f ⟨⟨x, hx⟩, a⟩ • ↑(K ⟨⟨x, hx⟩, a⟩) =
    ⋃ x ∈ {i ∈ s | (H i).FiniteIndex}, g x • ↑(H x)

Tactic:
refine Set.iUnion_congr fun i => ?_

Goal state after:
case hx
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
inst✝ : DecidablePred FiniteIndex
hcovers : ⋃ i ∈ {i ∈ s | (H i).FiniteIndex} ∪ {a ∈ s | ¬(H a).FiniteIndex}, g i • ↑(H i) = Set.univ
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
i : ι
⊢ ⋃ (hx : i ∈ s), ⋃ a, ⋃ (_ : ⟨⟨i, hx⟩, a⟩ ∈ {k | (H ↑k.fst).FiniteIndex}), f ⟨⟨i, hx⟩, a⟩ • ↑(K ⟨⟨i, hx⟩, a⟩) =
    ⋃ (_ : i ∈ {i ∈ s | (H i).FiniteIndex}), g i • ↑(H i)
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: case hy
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
inst✝ : DecidablePred FiniteIndex
hcovers : ⋃ i ∈ {i ∈ s | (H i).FiniteIndex} ∪ {a ∈ s | ¬(H a).FiniteIndex}, g i • ↑(H i) = Set.univ
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
⊢ ⋃ x, ⋃ (hx : x ∈ s), ⋃ a, ⋃ (_ : ⟨⟨x, hx⟩, a⟩ ∈ {a | ¬(H ↑a.fst).FiniteIndex}), f ⟨⟨x, hx⟩, a⟩ • ↑(K ⟨⟨x, hx⟩, a⟩) =
    ⋃ x ∈ {a ∈ s | ¬(H a).FiniteIndex}, g x • ↑(H x)

Tactic:
refine Set.iUnion_congr fun i => ?_

Goal state after:
case hy
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
inst✝ : DecidablePred FiniteIndex
hcovers : ⋃ i ∈ {i ∈ s | (H i).FiniteIndex} ∪ {a ∈ s | ¬(H a).FiniteIndex}, g i • ↑(H i) = Set.univ
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
i : ι
⊢ ⋃ (hx : i ∈ s), ⋃ a, ⋃ (_ : ⟨⟨i, hx⟩, a⟩ ∈ {a | ¬(H ↑a.fst).FiniteIndex}), f ⟨⟨i, hx⟩, a⟩ • ↑(K ⟨⟨i, hx⟩, a⟩) =
    ⋃ (_ : i ∈ {a ∈ s | ¬(H a).FiniteIndex}), g i • ↑(H i)
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: case pos
K : Type u
inst✝¹ : Field K
a : K
h : a = 0
hζ : (primitiveRoots 1 K).Nonempty
H : Irreducible (X ^ 1 - C a)
inst✝ : NeZero 1
__spread✝⁻⁰ : ↥(rootsOfUnity 1 K) →* Gal(K[1√a]/K) := autAdjoinRootXPowSubC 1 a
η : ↥(rootsOfUnity 1 K)
this✝¹ : Fact (Irreducible (X ^ 1 - C a))
this✝ : IsDomain K[1√a]
this : Algebra K K[1√a] := inferInstance
⊢ 1 = (of (X ^ 1 - C a)) ↑↑η

Tactic:
have : (η : Kˣ) = 1 := (pow_one _).symm.trans η.prop

Goal state after:
case pos
K : Type u
inst✝¹ : Field K
a : K
h : a = 0
hζ : (primitiveRoots 1 K).Nonempty
H : Irreducible (X ^ 1 - C a)
inst✝ : NeZero 1
__spread✝⁻⁰ : ↥(rootsOfUnity 1 K) →* Gal(K[1√a]/K) := autAdjoinRootXPowSubC 1 a
η : ↥(rootsOfUnity 1 K)
this✝² : Fact (Irreducible (X ^ 1 - C a))
this✝¹ : IsDomain K[1√a]
this✝ : Algebra K K[1√a] := inferInstance
this : ↑η = 1
⊢ 1 = (of (X ^ 1 - C a)) ↑↑η
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
inst✝ : DecidablePred FiniteIndex
D : Subgroup G := ⨅ k ∈ {i ∈ s | (H i).FiniteIndex}, H k
hD : D.FiniteIndex
hD_le : ∀ {i : ι}, i ∈ s → (H i).FiniteIndex → D ≤ H i
t : (i : ι) → i ∈ s → (H i).FiniteIndex → Finset ↥(H i)
ht :
  ∀ (i : ι) (hi : i ∈ s) (hfi : (H i).FiniteIndex),
    IsComplement ↑(t i hi hfi) ↑(D.subgroupOf (H i)) ∧ ⋃ g ∈ t i hi hfi, ↑g • ↑D = ↑(H i)
κ : Type (max u_2 u_1) := (i : ↥s) × ↥(if h : (H ↑i).FiniteIndex then t ↑i ⋯ h else {1})
f : κ → G := fun k ↦ g ↑k.fst * ↑↑k.snd
K : κ → Subgroup G := fun k ↦ if (H ↑k.fst).FiniteIndex then D else H ↑k.fst
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
⊢ ∑ i ∈ s.attach, ∑ s_1, ↑(if K ⟨i, s_1⟩ = D then 1 else 0) = ∑ x ∈ s.attach, (↑(H ↑x).index)⁻¹ * ↑D.index

Tactic:
refine Finset.sum_congr rfl fun i _ => ?_

Goal state after:
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
inst✝ : DecidablePred FiniteIndex
D : Subgroup G := ⨅ k ∈ {i ∈ s | (H i).FiniteIndex}, H k
hD : D.FiniteIndex
hD_le : ∀ {i : ι}, i ∈ s → (H i).FiniteIndex → D ≤ H i
t : (i : ι) → i ∈ s → (H i).FiniteIndex → Finset ↥(H i)
ht :
  ∀ (i : ι) (hi : i ∈ s) (hfi : (H i).FiniteIndex),
    IsComplement ↑(t i hi hfi) ↑(D.subgroupOf (H i)) ∧ ⋃ g ∈ t i hi hfi, ↑g • ↑D = ↑(H i)
κ : Type (max u_2 u_1) := (i : ↥s) × ↥(if h : (H ↑i).FiniteIndex then t ↑i ⋯ h else {1})
f : κ → G := fun k ↦ g ↑k.fst * ↑↑k.snd
K : κ → Subgroup G := fun k ↦ if (H ↑k.fst).FiniteIndex then D else H ↑k.fst
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
i : ↥s
x✝ : i ∈ s.attach
⊢ ∑ s_1, ↑(if K ⟨i, s_1⟩ = D then 1 else 0) = (↑(H ↑i).index)⁻¹ * ↑D.index
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: case refine_1
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)⁻¹
⊢ ⋃ k ∈ {i ∈ s | (H i).FiniteIndex}, g k • ↑(H k) =
    ⋃ x, ⋃ (hx : x ∈ s), ⋃ a, ⋃ (_ : ⟨⟨x, hx⟩, a⟩ ∈ {x | K x = D}), f ⟨⟨x, hx⟩, a⟩ • ↑D

Tactic:
refine Set.iUnion_congr fun i => ?_

Goal state after:
case refine_1
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)⁻¹
i : ι
⊢ ⋃ (_ : i ∈ {i ∈ s | (H i).FiniteIndex}), g i • ↑(H i) =
    ⋃ (hx : i ∈ s), ⋃ a, ⋃ (_ : ⟨⟨i, hx⟩, a⟩ ∈ {x | K x = D}), f ⟨⟨i, hx⟩, a⟩ • ↑D
Module: Mathlib.FieldTheory.KummerExtension

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

Tactic:
one_pow

Goal state after:
case refine_2
K : Type u
inst✝⁵ : Field K
L : Type u_1
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
inst✝¹ : IsGalois K L
inst✝ : IsCyclic Gal(L/K)
ζ : K
hζ : IsPrimitiveRoot ζ (finrank K L)
σ : Gal(L/K)
hσ : Function.Surjective fun x ↦ σ ^ x
hσ'✝ : orderOf σ = Nat.card Gal(L/K)
this✝ : (minpoly K σ.toLinearMap).IsRoot ζ
v : L
hv : End.HasEigenvector σ.toLinearMap ζ v
hv' : ∀ (n : ℕ), (σ ^ n) v = ζ ^ n • v
k : ℕ
hσ' : σ ^ (finrank K L * k) ∈ IsGalois.intermediateFieldEquivSubgroup K⟮v⟯
this : ζ ^ (finrank K L * k) • v = 1 • v
⊢ 1 ∈ ⊤