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

Goal state before:
pp: case refine_5.refine_1
L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
    φ.Realize default (Fin.snoc (⇑f ∘ x) a) → ∃ b, φ.Realize default (Fin.snoc (⇑f ∘ x) (f b))
n✝ : ℕ
φ✝ : L.BoundedFormula Empty n✝
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
ih : ∀ (xs : Fin (n + 1) → M), φ.Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ φ.Realize default xs
xs : Fin n → M
h : ∀ (a : N), φ.Realize (⇑f ∘ default) (Fin.snoc (⇑f ∘ xs) a)
a : M
⊢ φ.Realize default (Fin.snoc xs a)

Tactic:
← ih,

Goal state after:
case refine_5.refine_1
L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
    φ.Realize default (Fin.snoc (⇑f ∘ x) a) → ∃ b, φ.Realize default (Fin.snoc (⇑f ∘ x) (f b))
n✝ : ℕ
φ✝ : L.BoundedFormula Empty n✝
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
ih : ∀ (xs : Fin (n + 1) → M), φ.Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ φ.Realize default xs
xs : Fin n → M
h : ∀ (a : N), φ.Realize (⇑f ∘ default) (Fin.snoc (⇑f ∘ xs) a)
a : M
⊢ φ.Realize (⇑f ∘ default) (⇑f ∘ Fin.snoc xs a)
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
n : ℕ
inst✝ : Finite β
f : β → L.BoundedFormula α n
v : α → M
v' : Fin n → M
⊢ (iSup f).Realize v v' ↔ ∃ b, (f b).Realize v v'

Tactic:
simp only [iSup, realize_foldr_sup, List.mem_map, Finset.mem_toList, Finset.mem_univ, true_and,
    exists_exists_eq_and]

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
r : L.Relations 2
⊢ M ⊨ r.reflexive ↔ Std.Refl fun x y ↦ RelMap r ![x, y]

Tactic:
refl_def

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
r : L.Relations 2
⊢ M ⊨ r.reflexive ↔ ∀ ⦃a : M⦄, RelMap r ![a, a]
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type u_1
L : Language
inst✝ : L.Structure M
A : Set M
a : M
γ : Type u_4
ha : a ∈ A
⊢ DefinableFun L A fun x ↦ a

Tactic:
rw [definableFun_iff_empty_definableFun_with_params]
  exact ((L.con (⟨a,ha⟩ : ↑A)).term).definableFun_realize

Goal state after:
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type u_1
L : Language
inst✝ : L.Structure M
A : Set M
a : M
γ : Type u_4
ha : a ∈ A
⊢ DefinableFun L A fun x ↦ a

Tactic:
by
  rw [definableFun_iff_empty_definableFun_with_params]
  exact ((L.con (⟨a,ha⟩ : ↑A)).term).definableFun_realize

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: case refine_2
L : Language
T : L.Theory
α : Type w
φ : L.Formula α
h : (L.lhomWithConstants α).onTheory T ⊨ᵇ Formula.equivSentence φ
M : T.ModelType
v : α → ↑M
this✝ : (constantsOn α).Structure ↑M := constantsOn.structure v
this : ↑M ⊨ (L.lhomWithConstants α).onTheory T
⊢ φ.Realize v

Tactic:
exact (Formula.realize_equivSentence _ _).1 (h.realize_sentence M)

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
T : L.Theory
α : Type w
φ : L.Formula α
h : (L.lhomWithConstants α).onTheory T ⊨ᵇ Formula.equivSentence φ
M : Type u_1
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
v : α → M
this✝ : (constantsOn α).Structure M := constantsOn.structure v
this : M ⊨ (L.lhomWithConstants α).onTheory T
⊢ φ.Realize v

Tactic:
exact (Formula.realize_equivSentence _ _).1 (h.realize_sentence M)

Goal state after:
Module: Mathlib.RingTheory.Localization.Cardinality

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
L : Type v
inst✝² : CommRing L
inst✝¹ : Algebra R L
S : Submonoid R
inst✝ : IsLocalization S L
hS : S ≤ R⁰
⊢ Cardinal.lift.{u, v} #L = Cardinal.lift.{v, u} #R

Tactic:
by
  have := Localization.cardinalMk hS
  rwa [← lift_inj.{u, v}, lift_mk_eq'.2 ⟨(Localization.algEquiv S L).toEquiv⟩] at this

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

Goal state before:
pp: a : Cardinal.{u}
ha : ℵ₀ ≤ a
⊢ Prime a

Tactic:
refine ⟨(aleph0_pos.trans_le ha).ne', ?_, fun b c hbc => ?_⟩
  · rw [isUnit_iff]
    exact (one_lt_aleph0.trans_le ha).ne'
  rcases eq_or_ne (b * c) 0 with hz | hz
  · rcases mul_eq_zero.mp hz with (rfl | rfl) <;> simp
  wlog h : c ≤ b
  · cases le_total c b <;> [solve_by_elim; rw [or_comm]]
    apply_assumption
    assumption'
    all_goals rwa [mul_comm]
  left
  have habc := le_of_dvd hz hbc
  rwa [mul_eq_max' <| ha.trans <| habc, max_def', if_pos h] at hbc

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

Goal state before:
pp: case succ
k : Type u_1
inst✝⁴ : Field k
inst✝³ : Finite k
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP k p
n : ℕ
inst✝ : NeZero n
i : ℕ
ih : ∀ {x : Extension k p n}, (frob k p n ^ i) x = x ^ Nat.card k ^ i
x : Extension k p n
⊢ (frob k p n ^ (i + 1)) x = x ^ Nat.card k ^ (i + 1)

Tactic:
| succ i ih =>

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

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : Infinite K
e : Module.Basis (Module.Free.ChooseBasisIndex K L) K L
M : Matrix Gal(L/K) Gal(L/K) (MvPolynomial (Module.Free.ChooseBasisIndex K L) L) :=
  Matrix.of fun i j ↦ ∑ k, i.symm (j (e k)) • MvPolynomial.X k
hq : Submodule.span L (Set.range fun k j ↦ j (e k)) = ⊤
c : Module.Free.ChooseBasisIndex K L → L
hc : (MvPolynomial.eval c) M.det = 1
hM : M.det ≠ 0
⊢ ∃ b, (MvPolynomial.eval (⇑(algebraMap K L) ∘ b)) M.det ≠ 0

Tactic:
by_contra! h

Goal state after:
K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : Infinite K
e : Module.Basis (Module.Free.ChooseBasisIndex K L) K L
M : Matrix Gal(L/K) Gal(L/K) (MvPolynomial (Module.Free.ChooseBasisIndex K L) L) :=
  Matrix.of fun i j ↦ ∑ k, i.symm (j (e k)) • MvPolynomial.X k
hq : Submodule.span L (Set.range fun k j ↦ j (e k)) = ⊤
c : Module.Free.ChooseBasisIndex K L → L
hc : (MvPolynomial.eval c) M.det = 1
hM : M.det ≠ 0
h : ∀ (b : Module.Free.ChooseBasisIndex K L → K), (MvPolynomial.eval (⇑(algebraMap K L) ∘ b)) M.det = 0
⊢ False
Module: Mathlib.FieldTheory.Differential.Liouville

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝⁹ : Field F
inst✝⁸ : Field K
inst✝⁷ : Differential F
inst✝⁶ : Differential K
inst✝⁵ : Algebra F K
inst✝⁴ : DifferentialAlgebra F K
inst✝³ : CharZero F
inst✝² : FiniteDimensional F K
inst✝¹ : IsGalois F K
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc : ∀ (x : ι), (c x)′ = 0
u : ι → K
v : K
h : ↑a = ∑ x, ↑(c x) * logDeriv (u x) + v′
this : CharZero K
ffb : fixedField ⊤ = ⊥
⊢ (algebraMap F K) a * ↑(Fintype.card Gal(K/F)) = ∑ x, ↑a

Tactic:
simp [mul_comm]

Goal state after:
Module: Mathlib.FieldTheory.Differential.Liouville

Goal state before:
pp: case e'_5
F : Type u_1
K : Type u_2
inst✝⁹ : Field F
inst✝⁸ : Field K
inst✝⁷ : Differential F
inst✝⁶ : Differential K
inst✝⁵ : Algebra F K
inst✝⁴ : DifferentialAlgebra F K
inst✝³ : CharZero F
inst✝² : FiniteDimensional F K
inst✝¹ : IsGalois F K
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc : ∀ (x : ι), (c x)′ = 0
u : ι → K
v : K
this : CharZero K
ffb : fixedField ⊤ = ⊥
e : Gal(K/F)
h : (algebraMap F K) a = ∑ x, (algebraMap F K) (c x) * e (logDeriv (u x)) + e v′
⊢ ∑ x, ↑(c x) * logDeriv (e (u x)) = ∑ x, (algebraMap F K) (c x) * e (logDeriv (u x))

Tactic:
rcongr x

Goal state after:
case e'_5.e_f.e_a
F : Type u_1
K : Type u_2
inst✝⁹ : Field F
inst✝⁸ : Field K
inst✝⁷ : Differential F
inst✝⁶ : Differential K
inst✝⁵ : Algebra F K
inst✝⁴ : DifferentialAlgebra F K
inst✝³ : CharZero F
inst✝² : FiniteDimensional F K
inst✝¹ : IsGalois F K
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc : ∀ (x : ι), (c x)′ = 0
u : ι → K
v : K
this : CharZero K
ffb : fixedField ⊤ = ⊥
e : Gal(K/F)
h : (algebraMap F K) a = ∑ x, (algebraMap F K) (c x) * e (logDeriv (u x)) + e v′
x : ι
⊢ logDeriv (e (u x)) = e (logDeriv (u x))
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
⊢ Continuous ⇑(algEquivToLimit k K)

Tactic:
continuous_induced_rng

Goal state after:
k : Type u_3
K : Type u_4
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
⊢ Continuous (Subtype.val ∘ ⇑(algEquivToLimit k K))
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: case mpr
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
m : ℕ
x : K
n : ℕ
y : K
z : ℕ
H : (⇑(frobenius K p))^[n + z] x = (⇑(frobenius K p))^[m + z] y
⊢ mk K p (m, x) = mk K p (n, y)

Tactic:
rw [R.sound K p (n + z) m x _ rfl, R.sound K p (m + z) n y _ rfl, H]

Goal state after:
case mpr
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
m : ℕ
x : K
n : ℕ
y : K
z : ℕ
H : (⇑(frobenius K p))^[n + z] x = (⇑(frobenius K p))^[m + z] y
⊢ mk K p (n + z + m, (⇑(frobenius K p))^[m + z] y) = mk K p (m + z + n, (⇑(frobenius K p))^[m + z] y)
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
inst✝⁷ : CommRing L
inst✝⁶ : CommRing M
inst✝⁵ : CommRing N
i : K →+* L
j : K →+* M
k : K →+* N
f : L →+* M
g : L →+* N
p : ℕ
inst✝⁴ : ExpChar M p
inst✝³ : ExpChar K p
inst✝² : PerfectRing M p
inst✝¹ : IsPRadical i p
inst✝ : ExpChar L p
x1 x2 : L
⊢ liftAux i j p (x1 * x2) = liftAux i j p x1 * liftAux i j p x2

Tactic:
obtain ⟨n1, y1, h1⟩ := IsPRadical.pow_mem i p x1
    obtain ⟨n2, y2, h2⟩ := IsPRadical.pow_mem i p x2
    rw [liftAux_apply i j p _ _ _ h1, liftAux_apply i j p _ _ _ h2,
      liftAux_apply i j p (x1 * x2) (n1 + n2) (y1 ^ p ^ n2 * y2 ^ p ^ n1) (by rw [map_mul,
        map_pow, map_pow, h1, h2, ← pow_mul, ← pow_add, ← pow_mul, ← pow_add,
        add_comm n2, mul_pow]),
      map_mul, map_pow, map_pow, map_mul, ← iterateFrobeniusEquiv_def]
    nth_rw 1 [iterateFrobeniusEquiv_symm_add_apply]
    rw [RingEquiv.symm_apply_apply, add_comm n1, iterateFrobeniusEquiv_symm_add_apply,
      ← iterateFrobeniusEquiv_def, RingEquiv.symm_apply_apply]

Goal state after:
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
x : K
n : ℕ
ih : (⇑(frobenius (PerfectClosure K p) p))^[n] (mk K p (n, x)) = (of K p) x
⊢ (⇑(frobenius (PerfectClosure K p) p))^[n] ((frobenius (PerfectClosure K p) p) (mk K p (n + 1, x))) = (of K p) x

Tactic:
← ih,

Goal state after:
case succ
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : K
n : ℕ
ih : (⇑(frobenius (PerfectClosure K p) p))^[n] (mk K p (n, x)) = (of K p) x
⊢ (⇑(frobenius (PerfectClosure K p) p))^[n] ((frobenius (PerfectClosure K p) p) (mk K p (n + 1, x))) =
    (⇑(frobenius (PerfectClosure K p) p))^[n] (mk K p (n, x))
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: G : Type u_1
inst✝ : Group G
ι : Type u_2
s : Finset ι
H : Subgroup G
g : ι → G
hcovers : Set.SurjOn (fun x ↦ ↑(g x)) (↑s) Set.univ
this : Finite (G ⧸ H)
⊢ H.FiniteIndex

Tactic:
exact H.finiteIndex_of_finite_quotient

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
hb : (⇑((ad (↥k) D) a))^[n] b ≠ 0 ∧ (⇑((ad (↥k) D) a))^[n + 1] b = 0
⊢ False

Tactic:
set c := (ad k D a)^[n] b with hc_def

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
⊢ 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
inst✝ : DecidableEq (Subgroup G)
j : ι
hj : j ∈ s
hcovers' : ⋃ i ∈ {x ∈ s | H x = H j}, g i • ↑(H i) ≠ Set.univ
n : ℕ
hn : n = (Finset.image H s).card
⊢ ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex

Tactic:
induction n using Nat.strongRec generalizing ι with

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
⊢ c⁻¹ * a * ((⇑((ad (↥k) D) a))^[n - 1] b * a) = a * (c⁻¹ * (⇑((ad (↥k) D) a))^[n - 1] b * a)

Tactic:
hc',

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.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
hcovers' : ⋃ k ∈ Finset.univ, f k • ↑(K k) = Set.univ
k : κ
hkfi : (H ↑k.fst).FiniteIndex
hk : K k = D
⊢ ⋃ i ∈ {x | K x = K k}, f i • ↑(K i) = Set.univ

Tactic:
by_contra! h

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
hcovers' : ⋃ k ∈ Finset.univ, f k • ↑(K k) = Set.univ
k : κ
hkfi : (H ↑k.fst).FiniteIndex
hk : K k = D
h : ⋃ i ∈ {x | K x = K k}, f i • ↑(K i) ≠ Set.univ
⊢ False
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
⊢ K⟮α⟯ = ⊤

Tactic:
refine (IntermediateField.eq_adjoin_of_eq_algebra_adjoin _ _ _ ?_).symm

Goal state after:
K : Type u
inst✝³ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
L : Type u_1
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ n - C a)
α : L
hα : α ^ n = (algebraMap K L) a
⊢ ⊤.toSubalgebra = K [α]
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)
this : (minpoly K σ.toLinearMap).IsRoot ζ
v : L
hv : End.HasEigenvector σ.toLinearMap ζ v
hv' : ∀ (n : ℕ), (σ.toLinearMap ^ n) v = ζ ^ n • v
⊢ ∃ α, α ^ finrank K L ∈ Set.range ⇑(algebraMap K L) ∧ K⟮α⟯ = ⊤

Tactic:
← AlgEquiv.pow_toLinearMap,

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 σ = Nat.card Gal(L/K)
this : (minpoly K σ.toLinearMap).IsRoot ζ
v : L
hv : End.HasEigenvector σ.toLinearMap ζ v
hv' : ∀ (n : ℕ), (σ ^ n).toLinearMap v = ζ ^ n • v
⊢ ∃ α, α ^ finrank K L ∈ Set.range ⇑(algebraMap K L) ∧ K⟮α⟯ = ⊤
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_contra! h

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
h : ∀ i ∈ s, (H i).FiniteIndex → s.card < (H i).index
⊢ False
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
H : IsField (A ⊗[R] B)
⊢ Algebra.IsAlgebraic R A ∨ Algebra.IsAlgebraic R B

Tactic:
by_contra! h

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
H : IsField (A ⊗[R] B)
h : ¬Algebra.IsAlgebraic R A ∧ ¬Algebra.IsAlgebraic R B
⊢ False
Module: Mathlib.FieldTheory.LinearDisjoint

Goal state before:
pp: case e_a
F : Type u
E : Type v
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
A : IntermediateField F E
L : Type w
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
H : A.LinearDisjoint L
halg : Algebra.IsAlgebraic F ↥A ∨ Algebra.IsAlgebraic F L
L' : Subalgebra F E := (IsScalarTower.toAlgHom F L E).range
i : L ≃ₐ[F] ↥L' := AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)
x : E
⊢ (∃ y, (algebraMap L E) y = x) ↔ ∃ a, ∃ (b : a ∈ L'), (algebraMap (↥L') E) ⟨a, b⟩ = x

Tactic:
exact ⟨fun ⟨y, h⟩ ↦ ⟨x, ⟨y, h⟩, rfl⟩, fun ⟨a, ⟨y, h1⟩, h2⟩ ↦ ⟨y, h1.trans h2⟩⟩

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

Goal state before:
pp: F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
K : Type w
inst✝¹ : Field K
inst✝ : Algebra F K
i : E →ₐ[F] K
x : E
⊢ i x ∈ perfectClosure F K ↔ x ∈ perfectClosure F E

Tactic:
simp_rw [mem_perfectClosure_iff]

Goal state after:
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
K : Type w
inst✝¹ : Field K
inst✝ : Algebra F K
i : E →ₐ[F] K
x : E
⊢ (∃ n, i x ^ ringExpChar F ^ n ∈ (algebraMap F K).range) ↔ ∃ n, x ^ ringExpChar F ^ n ∈ (algebraMap F E).range
Module: Mathlib.FieldTheory.RatFunc.Degree

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

Tactic:
num_C,

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

Goal state before:
pp: case neg
K : Type u
inst✝ : Field K
x y : K⟮X⟯
hy : y ≠ 0
hxy : x + y ≠ 0
hx : ¬x = 0
⊢ ↑(x.num * y.denom + x.denom * y.num).natDegree - ↑(x.denom * y.denom).natDegree ≤
      ↑(x.num * y.denom).natDegree - ↑(x.denom * y.denom).natDegree ∨
    ↑(x.num * y.denom + x.denom * y.num).natDegree - ↑(x.denom * y.denom).natDegree ≤
      ↑(y.num * x.denom).natDegree - ↑(x.denom * y.denom).natDegree

Tactic:
sub_le_sub_iff_right,

Goal state after:
case neg
K : Type u
inst✝ : Field K
x y : K⟮X⟯
hy : y ≠ 0
hxy : x + y ≠ 0
hx : ¬x = 0
⊢ ↑(x.num * y.denom + x.denom * y.num).natDegree ≤ ↑(x.num * y.denom).natDegree ∨
    ↑(x.num * y.denom + x.denom * y.num).natDegree - ↑(x.denom * y.denom).natDegree ≤
      ↑(y.num * x.denom).natDegree - ↑(x.denom * y.denom).natDegree
Module: Mathlib.FieldTheory.RatFunc.Degree

Goal state before:
pp: case neg
K : Type u
inst✝ : Field K
x y : K⟮X⟯
hy : y ≠ 0
hxy : x + y ≠ 0
hx : ¬x = 0
⊢ (x.num * y.denom + x.denom * y.num).natDegree ≤ (x.num * y.denom).natDegree ∨
    ↑(x.num * y.denom + x.denom * y.num).natDegree - ↑(x.denom * y.denom).natDegree ≤
      ↑(y.num * x.denom).natDegree - ↑(x.denom * y.denom).natDegree

Tactic:
sub_le_sub_iff_right,

Goal state after:
case neg
K : Type u
inst✝ : Field K
x y : K⟮X⟯
hy : y ≠ 0
hxy : x + y ≠ 0
hx : ¬x = 0
⊢ (x.num * y.denom + x.denom * y.num).natDegree ≤ (x.num * y.denom).natDegree ∨
    ↑(x.num * y.denom + x.denom * y.num).natDegree ≤ ↑(y.num * x.denom).natDegree
Module: Mathlib.Geometry.Convex.Cone.DualFinite

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsOrderedRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : M →ₗ[R] N →ₗ[R] R
C : PointedCone R N
s : Finset M
hs : dual p ↑s = C
⊢ ∃ D, Submodule.FG D ∧ dual p ↑D = C

Tactic:
exact ⟨_, Submodule.fg_span s.finite_toSet, by simp [hs]⟩

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁵ : Semiring R
inst✝⁴ : PartialOrder R
inst✝³ : IsOrderedRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
C F : PointedCone R M
ι : Type u_4
inst✝ : Fintype ι
f : ι → M
c : ι → R
hF : F.IsFaceOf C
hsC : ∀ (i : ι), f i ∈ C
hc : ∀ (i : ι), 0 ≤ c i
i : ι
hs : c i • f i + ∑ x ∈ Finset.univ \ {i}, c x • f x ∈ F
hci : 0 < c i
⊢ f i ∈ F

Tactic:
refine hF.mem_of_smul_add_mem (hsC i) ?_ hci hs

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁵ : Semiring R
inst✝⁴ : PartialOrder R
inst✝³ : IsOrderedRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
C F : PointedCone R M
ι : Type u_4
inst✝ : Fintype ι
f : ι → M
c : ι → R
hF : F.IsFaceOf C
hsC : ∀ (i : ι), f i ∈ C
hc : ∀ (i : ι), 0 ≤ c i
i : ι
hs : c i • f i + ∑ x ∈ Finset.univ \ {i}, c x • f x ∈ F
hci : 0 < c i
⊢ ∑ x ∈ Finset.univ \ {i}, c x • f x ∈ 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
h : A ≤ B
this : Algebra ↥A ↥B := (inclusion h).toAlgebra
⊢ Module.rank F ↥A * Module.rank ↥A ↥(extendScalars h) = Module.rank F ↥B

Tactic:
exact rank_mul_rank F A B

Goal state after: