mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f✝ : α → β
E I : Set α
M : Matroid α
N✝ N : Matroid β
f : α → β
⊢ ∀ ⦃I B : Set α⦄,
    N.Indep (f '' I) ∧ InjOn f I →
      ¬Maximal (fun I ↦ N.Indep (f '' I) ∧ InjOn f I) I →
        Maximal (fun I ↦ N.Indep (f '' I) ∧ InjOn f I) B → ∃ x ∈ B \ I, N.Indep (f '' insert x I) ∧ InjOn f (insert x I)

Tactic:
by
      rintro I B ⟨hI, hIinj⟩ hImax hBmax
      obtain ⟨I', hII', hI', hI'inj⟩ := (not_maximal_subset_iff ⟨hI, hIinj⟩).1 hImax
      have h₁ : ¬(N ↾ range f).IsBase (f '' I) := by
        refine fun hB ↦ hII'.ne ?_
        have h_im := hB.eq_of_subset_indep (by simpa) (image_mono hII'.subset)
        rwa [hI'inj.image_eq_image_iff hII'.subset Subset.rfl] at h_im
      have h₂ : (N ↾ range f).IsBase (f '' B) := by
        refine Indep.isBase_of_forall_insert (by simpa using hBmax.1.1) ?_
        rintro _ ⟨⟨e, heB, rfl⟩, hfe⟩ hi
        rw [restrict_indep_iff, ← image_insert_eq] at hi
        have hinj : InjOn f (insert e B) := by
          rw [injOn_insert (fun heB ↦ hfe (mem_image_of_mem f heB))]
          exact ⟨hBmax.1.2, hfe⟩
        refine hBmax.not_prop_of_ssuperset (t := insert e B) (ssubset_insert ?_) ⟨hi.1, hinj⟩
        exact fun heB ↦ hfe <| mem_image_of_mem f heB
      obtain ⟨_, ⟨⟨e, he, rfl⟩, he'⟩, hei⟩ := Indep.exists_insert_of_not_isBase (by simpa) h₁ h₂
      have heI : e ∉ I := fun heI ↦ he' (mem_image_of_mem f heI)
      rw [← image_insert_eq, restrict_indep_iff] at hei
      exact ⟨e, ⟨he, heI⟩, hei.1, (injOn_insert heI).2 ⟨hIinj, he'⟩⟩

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Rank.Finite

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
e : α
⊢ M.IsRkFinite (X \ {e}) ↔ M.IsRkFinite X

Tactic:
by
  rw [isRkFinite_singleton.isRkFinite_sdiff_iff]

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
C : Set α
⊢ (M.Dep C ∧ ∀ ⦃t : Set α⦄, t ⊂ C → ¬M.Dep t) ↔ M.Dep C ∧ ∀ ⦃I : Set α⦄, I ⊂ C → M.Indep I

Tactic:
and_congr_right_iff

Goal state after:
α : Type u_1
M : Matroid α
C : Set α
⊢ M.Dep C → ((∀ ⦃t : Set α⦄, t ⊂ C → ¬M.Dep t) ↔ ∀ ⦃I : Set α⦄, I ⊂ C → M.Indep I)
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
heI : e ∉ I
he : e ∈ M.closure I
h : ∀ f ∈ I, e ∉ M.closure (I \ {f})
⊢ ∀ e_1 ∈ insert e I, M.Indep (insert e I \ {e_1})

Tactic:
rintro f (rfl | hfI)

Goal state after:
case inl
α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
f : α
heI : f ∉ I
he : f ∈ M.closure I
h : ∀ f_1 ∈ I, f ∉ M.closure (I \ {f_1})
⊢ M.Indep (insert f I \ {f})

case inr
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
heI : e ∉ I
he : e ∈ M.closure I
h : ∀ f ∈ I, e ∉ M.closure (I \ {f})
f : α
hfI : f ∈ I
⊢ M.Indep (insert e I \ {f})
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
C I : Set α
hC : M.IsCircuit C
⊢ (∃ e ∈ C, I = C \ {e}) ↔ ∃ e ∈ C \ I, C = insert e I

Tactic:
refine ⟨fun ⟨e, he, hI⟩ ↦ ⟨e, ⟨he, fun heI ↦ (hI.subset heI).2 rfl⟩, ?_⟩,
    fun ⟨e, he, hC⟩ ↦ ⟨e, he.1, ?_⟩⟩

Goal state after:
case refine_1
α : Type u_1
M : Matroid α
C I : Set α
hC : M.IsCircuit C
x✝ : ∃ e ∈ C, I = C \ {e}
e : α
he : e ∈ C
hI : I = C \ {e}
⊢ C = insert e I

case refine_2
α : Type u_1
M : Matroid α
C I : Set α
hC✝ : M.IsCircuit C
x✝ : ∃ e ∈ C \ I, C = insert e I
e : α
he : e ∈ C \ I
hC : C = insert e I
⊢ I = C \ {e}
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
I : Set β
⊢ (∃ I₀, M.Indep I₀ ∧ I = ⇑f '' I₀) ↔ M.Indep (⇑f ⁻¹' I) ∧ I ⊆ range ⇑f

Tactic:
refine ⟨?_, fun ⟨h,h'⟩ ↦ ⟨f ⁻¹' I, h, by rwa [eq_comm, image_preimage_eq_iff]⟩⟩

Goal state after:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
I : Set β
⊢ (∃ I₀, M.Indep I₀ ∧ I = ⇑f '' I₀) → M.Indep (⇑f ⁻¹' I) ∧ I ⊆ range ⇑f
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: case refine_1
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h₁ : ∀ (C : Set α), M₁.IsCircuit C → ¬M₂.Indep C
h₂ : ∀ (C : Set α), M₂.IsCircuit C → ¬M₁.Indep C
C : Set α
hCE : C ⊆ M₁.E
hC : M₁.IsCircuit C
⊢ M₂.IsCircuit C

Tactic:
obtain ⟨C', hC'C, hC'⟩ := ((not_indep_iff (by rwa [← hE])).1 (h₁ C hC)).exists_isCircuit_subset

Goal state after:
case refine_1
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h₁ : ∀ (C : Set α), M₁.IsCircuit C → ¬M₂.Indep C
h₂ : ∀ (C : Set α), M₂.IsCircuit C → ¬M₁.Indep C
C : Set α
hCE : C ⊆ M₁.E
hC : M₁.IsCircuit C
C' : Set α
hC'C : C' ⊆ C
hC' : M₂.IsCircuit C'
⊢ M₂.IsCircuit C
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: case inr
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ∈ M.closure {f}
h : f ∈ M.E → f ∈ M.loops
hf : f ∉ M.E
⊢ M.closure {f} = M.loops

Tactic:
← closure_inter_ground,

Goal state after:
case inr
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ∈ M.closure {f}
h : f ∈ M.E → f ∈ M.loops
hf : f ∉ M.E
⊢ M.closure ({f} ∩ M.E) = M.loops
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: case inl
α : Type u_1
M : Matroid α
ι : Type u_2
J : Set α
x : ι → α
I : ι → Set α
z : α
hxI : ∀ (i : ι), x i ∉ I i
hC : ∀ (i : ι), M.IsCircuit (insert (x i) (I i))
hJx : M.IsCircuit (J ∪ range x)
hzJ : z ∈ J
hzI : ∀ (i : ι), z ∉ I i
hι : IsEmpty ι
⊢ ∃ C' ⊆ J ∪ ⋃ i, I i, M.IsCircuit C' ∧ z ∈ C'

Tactic:
exact ⟨J, by simp, by simpa [range_eq_empty] using hJx, hzJ⟩

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
he : M.IsNonloop e
⊢ ∃ K, M.IsCocircuit K ∧ e ∈ K

Tactic:
by
  obtain ⟨B, hB, heB⟩ := he.exists_mem_isBase
  exact ⟨_, fundCocircuit_isCocircuit heB hB, mem_fundCocircuit M e B⟩

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
X Y : Set α
hX : M.IsRkFinite X
hXY : X ⊆ Y
I : Set α
hI : M.IsBasis' I X
J : Set α
hr : J.encard ≤ I.encard
hJ : M.IsBasis' J Y
hIJ : I ⊆ J
⊢ M.closure X = M.closure Y

Tactic:
← closure_inter_ground,

Goal state after:
α : Type u_1
M : Matroid α
X Y : Set α
hX : M.IsRkFinite X
hXY : X ⊆ Y
I : Set α
hI : M.IsBasis' I X
J : Set α
hr : J.encard ≤ I.encard
hJ : M.IsBasis' J Y
hIJ : I ⊆ J
⊢ M.closure (X ∩ M.E) = M.closure Y
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
e : α
heI : e ∉ I
hC : M.IsCircuit (insert e I)
hI : M.IsBasis I (insert e I)
heC : e ∈ insert e I
⊢ I.encard + 1 = (insert e I).encard

Tactic:
encard_insert_of_notMem heI

Goal state after:
α : Type u_1
M : Matroid α
I : Set α
e : α
heI : e ∉ I
hC : M.IsCircuit (insert e I)
hI : M.IsBasis I (insert e I)
heC : e ∈ insert e I
⊢ I.encard + 1 = I.encard + 1
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: case pos
α : Type u_1
M : Matroid α
e : α
inst✝ : M✶.RankPos
he : e ∈ M.E
⊢ M.IsColoop e ↔ ∀ (C : Set α), M.IsCircuit C → e ∈ M.E \ C

pp: case neg
α : Type u_1
M : Matroid α
e : α
inst✝ : M✶.RankPos
he : e ∉ M.E
⊢ M.IsColoop e ↔ ∀ (C : Set α), M.IsCircuit C → e ∈ M.E \ C

Tactic:
· simp [isColoop_iff_forall_notMem_isCircuit, he]

Goal state after:
case neg
α : Type u_1
M : Matroid α
e : α
inst✝ : M✶.RankPos
he : e ∉ M.E
⊢ M.IsColoop e ↔ ∀ (C : Set α), M.IsCircuit C → e ∈ M.E \ C
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
x✝ : (∀ X ⊆ M.E, e ∈ M.closure X ↔ e ∈ X) ∧ e ∈ M.E
h : ∀ X ⊆ M.E, e ∈ M.closure X ↔ e ∈ X
he : e ∈ M.E
X : Set α
⊢ e ∈ M.closure X ↔ e ∈ X

Tactic:
← closure_inter_ground,

Goal state after:
α : Type u_1
M : Matroid α
e : α
x✝ : (∀ X ⊆ M.E, e ∈ M.closure X ↔ e ∈ X) ∧ e ∈ M.E
h : ∀ X ⊆ M.E, e ∈ M.closure X ↔ e ∈ X
he : e ∈ M.E
X : Set α
⊢ e ∈ M.closure (X ∩ M.E) ↔ e ∈ X
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
⊢ M.closure univ = M.E

Tactic:
← closure_inter_ground,

Goal state after:
α : Type u_2
M : Matroid α
⊢ M.closure (univ ∩ M.E) = M.E
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: case inl
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.loops = M₂.loops
hc : M₁.coloops = M₂.coloops
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.loops ∪ M₁.coloops) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
hdj : Disjoint I M₁.loops
⊢ Disjoint (I \ M₁.coloops) (M₁.loops ∪ M₁.coloops)

Tactic:
disjoint_union_right

Goal state after:
case inl
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.loops = M₂.loops
hc : M₁.coloops = M₂.coloops
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.loops ∪ M₁.coloops) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
hdj : Disjoint I M₁.loops
⊢ Disjoint (I \ M₁.coloops) M₁.loops ∧ Disjoint (I \ M₁.coloops) M₁.coloops
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
B : Set α
⊢ M.Indep B ∧ B ⊆ M.E ∧ M.E ⊆ M.closure B ↔ M.Indep B ∧ M.closure B = M.E

Tactic:
and_congr_right_iff

Goal state after:
α : Type u_2
M : Matroid α
B : Set α
⊢ M.Indep B → (B ⊆ M.E ∧ M.E ⊆ M.closure B ↔ M.closure B = M.E)
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
X I : Set α
⊢ M.IsBasis' I X ↔ M.IsBasis I (M.closure X) ∧ I ⊆ X

Tactic:
← closure_inter_ground,

Goal state after:
α : Type u_2
M : Matroid α
X I : Set α
⊢ M.IsBasis' I X ↔ M.IsBasis I (M.closure (X ∩ M.E)) ∧ I ⊆ X
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: α : Type u
M : Matroid α
⊢ toENat M.cRank = M.eRank

Tactic:
by
  obtain h | h := M.rankFinite_or_rankInfinite
  · obtain ⟨B, hB⟩ := M.exists_isBase
    rw [← hB.cardinalMk_eq_cRank, ← hB.encard_eq_eRank, toENat_cardinalMk]
  simp [rankInfinite_iff_aleph0_le_cRank.1 h]

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
X : Set α
⊢ M.Indep ∅ ∧ X ⊆ M.closure ∅ ∧ ∅ ⊆ X ↔ X ⊆ M.closure ∅

Tactic:
and_iff_right M.empty_indep,

Goal state after:
α : Type u_2
M : Matroid α
X : Set α
⊢ X ⊆ M.closure ∅ ∧ ∅ ⊆ X ↔ X ⊆ M.closure ∅
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: case refine_1
α : Type u_2
M : Matroid α
I : Set α
h : ∀ ⦃e : α⦄, e ∈ I → M.closure (I \ {e}) ≠ M.closure I
e : α
heI : e ∈ I
heE : e ∉ M.E
⊢ M.closure (I \ {e}) = M.closure I

Tactic:
← closure_inter_ground,

Goal state after:
case refine_1
α : Type u_2
M : Matroid α
I : Set α
h : ∀ ⦃e : α⦄, e ∈ I → M.closure (I \ {e}) ≠ M.closure I
e : α
heI : e ∈ I
heE : e ∉ M.E
⊢ M.closure (I \ {e} ∩ M.E) = M.closure I
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
X : Set α
e f : α
he : e ∉ M.closure (X ∩ M.E)
hef : e ∈ M.closure (insert f (X ∩ M.E))
hfE : f ∈ M.E
heE : e ∈ M.E
⊢ f ∈ M.closure (insert e X ∩ M.E)

Tactic:
rw [insert_inter_of_mem heE]

Goal state after:
α : Type u_2
M : Matroid α
X : Set α
e f : α
he : e ∉ M.closure (X ∩ M.E)
hef : e ∈ M.closure (insert f (X ∩ M.E))
hfE : f ∈ M.E
heE : e ∈ M.E
⊢ f ∈ M.closure (insert e (X ∩ M.E))
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
X Y : Set α
h : Y ⊆ M.closure (X \ Y)
⊢ M.closure (X \ Y) = M.closure X

Tactic:
rw [← sdiff_union_inter X Y, ← closure_union_closure_left_eq,
    union_eq_self_of_subset_right (inter_subset_right.trans h), closure_closure, sdiff_union_inter]

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
S T : Set α
hS : M.Spanning S
hST : S ⊆ T
⊢ M.closure T = M.E

Tactic:
← closure_inter_ground,

Goal state after:
α : Type u_2
M : Matroid α
S T : Set α
hS : M.Spanning S
hST : S ⊆ T
⊢ M.closure (T ∩ M.E) = M.E
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
β : Type u_3
M : Matroid β
f : α → β
X : Set α
⊢ (M.comap f).closure X = f ⁻¹' M.closure (f '' X)

Tactic:
by
  -- Use a choice of basis and extensionality to change the goal to a statement about independence.
  obtain ⟨I, hI⟩ := (M.comap f).exists_isBasis' X
  obtain ⟨hI', hIinj, -⟩ := comap_isBasis'_iff.1 hI
  simp_rw [← hI.closure_eq_closure, ← hI'.closure_eq_closure, Set.ext_iff,
    hI.indep.mem_closure_iff', comap_ground_eq, mem_preimage, hI'.indep.mem_closure_iff',
    comap_indep_iff, and_imp, mem_image, and_congr_right_iff, ← image_insert_eq]
  -- the lemma now easily follows by considering elements/non-elements of `I` separately.
  intro x hxE
  by_cases hxI : x ∈ I
  · simp [hxI, show ∃ y ∈ I, f y = f x from ⟨x, hxI, rfl⟩]
  simp [hxI, injOn_insert hxI, hIinj]

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
aux : ∀ ⦃I : Set α⦄, M.Indep I → (M.map f hf).closure (f '' I) = f '' M.closure I
I : Set α
hI : M.IsBasis I (f ⁻¹' X ∩ M.E)
⊢ (M.map f hf).closure X = f '' M.closure (f ⁻¹' X)

Tactic:
← closure_inter_ground,

Goal state after:
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
aux : ∀ ⦃I : Set α⦄, M.Indep I → (M.map f hf).closure (f '' I) = f '' M.closure I
I : Set α
hI : M.IsBasis I (f ⁻¹' X ∩ M.E)
⊢ (M.map f hf).closure (X ∩ (M.map f hf).E) = f '' M.closure (f ⁻¹' X)
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: R : Type u_1
S : Type v
A : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : IsDomain S
inst✝ : NoZeroDivisors A
ι : Type u_2
v : ι → A
hv : IsTranscendenceBasis R v
H : ∀ (i : ι), IsAlgebraic S (v i)
Rv : Subalgebra R A := adjoin R (range v)
Sv : Subalgebra S A := adjoin S (range v)
this : Algebra.IsAlgebraic S ↥Sv
le : Rv ≤ Subalgebra.restrictScalars R Sv
⊢ Algebra.IsAlgebraic S A

Tactic:
let : Algebra Rv Sv := (Subalgebra.inclusion le).toAlgebra

Goal state after:
R : Type u_1
S : Type v
A : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : IsDomain S
inst✝ : NoZeroDivisors A
ι : Type u_2
v : ι → A
hv : IsTranscendenceBasis R v
H : ∀ (i : ι), IsAlgebraic S (v i)
Rv : Subalgebra R A := adjoin R (range v)
Sv : Subalgebra S A := adjoin S (range v)
this✝ : Algebra.IsAlgebraic S ↥Sv
le : Rv ≤ Subalgebra.restrictScalars R Sv
this : Algebra ↥Rv ↥Sv := (Subalgebra.inclusion le).toAlgebra
⊢ Algebra.IsAlgebraic S A
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
halg : IsAlgebraic F α
this : FiniteDimensional F ↥F⟮α⟯
⊢ finSepDegree F ↥F⟮α⟯ ≤ finrank F ↥F⟮α⟯

Tactic:
exact Nat.le_of_dvd finrank_pos <| finSepDegree_adjoin_simple_dvd_finrank F E α

Goal state after:
Module: Mathlib.FieldTheory.KrullTopology

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsIntegral K L
f g : Gal(L/K)
hfg : f ≠ g
φ : Gal(L/K) := f⁻¹ * g
x : L
hx : f x ≠ g x
hφx : φ x ≠ x
⊢ (fun x y ↦ ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v) f g

Tactic:
(Tactic.tacticLet__
 "let"
 (Term.letConfig [])
 (Term.letDecl
  (Term.letIdDecl
   (Term.letId `E)
   []
   [(Term.typeSpec ":" (Term.app `IntermediateField [`K `L]))]
   ":="
   (Term.app
    `IntermediateField.adjoin
    [`K
     (choice
      («term{_}» "{" [`x] "}")
      (Term.structInst
       "{"
       []
       (Term.structInstFields [(Term.structInstField (Term.structInstLVal `x []) [])])
       (Term.optEllipsis [])
       []
       "}"))]))))

Goal state after:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsIntegral K L
f g : Gal(L/K)
hfg : f ≠ g
φ : Gal(L/K) := f⁻¹ * g
x : L
hx : f x ≠ g x
hφx : φ x ≠ x
E : IntermediateField K L := K⟮x⟯
⊢ (fun x y ↦ ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v) f g
Module: Mathlib.FieldTheory.Galois.GaloisClosure

Goal state before:
pp: k : Type u_1
K : Type u_2
inst✝⁴ : Field k
inst✝³ : Field K
inst✝² : Algebra k K
inst✝¹ : IsGalois k K
f : K →ₐ[k] K
s : Set K
inst✝ : Finite ↑s
⊢ normalClosure k (↥(IntermediateField.adjoin k (⇑f '' s))) K = normalClosure k (↥(IntermediateField.adjoin k s)) K

Tactic:
← IntermediateField.adjoin_map,

Goal state after:
k : Type u_1
K : Type u_2
inst✝⁴ : Field k
inst✝³ : Field K
inst✝² : Algebra k K
inst✝¹ : IsGalois k K
f : K →ₐ[k] K
s : Set K
inst✝ : Finite ↑s
⊢ normalClosure k (↥(map f (IntermediateField.adjoin k s))) K = normalClosure k (↥(IntermediateField.adjoin k s)) K
Module: Mathlib.FieldTheory.Galois.Infinite

Goal state before:
pp: k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
H : ClosedSubgroup Gal(K/k)
inst✝ : IsGalois k K
σ : Gal(K/k)
hσ : σ ∈ (fixedField ↑H).fixingSubgroup
h : σ ∉ ↑H
nhds : (↑H).carrierᶜ ∈ _root_.nhds σ
⊢ False

Tactic:
GroupFilterBasis.nhds_eq (x₀ := σ) (galGroupBasis k K)

Goal state after:
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
H : ClosedSubgroup Gal(K/k)
inst✝ : IsGalois k K
σ : Gal(K/k)
hσ : σ ∈ (fixedField ↑H).fixingSubgroup
h : σ ∉ ↑H
nhds : (↑H).carrierᶜ ∈ (galGroupBasis k K).N σ
⊢ False
Module: Mathlib.RingTheory.DedekindDomain.IntegralClosure

Goal state before:
pp: A : Type u_1
K : Type u_2
inst✝¹⁴ : CommRing A
inst✝¹³ : Field K
inst✝¹² : Algebra A K
inst✝¹¹ : IsFractionRing A K
L : Type u_3
inst✝¹⁰ : Field L
C : Type u_4
inst✝⁹ : CommRing C
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra A L
inst✝⁶ : IsScalarTower A K L
inst✝⁵ : Algebra C L
inst✝⁴ : IsIntegralClosure C A L
inst✝³ : Algebra A C
inst✝² : IsScalarTower A C L
inst✝¹ : IsDomain A
inst✝ : Algebra.IsAlgebraic K L
this✝ : IsDomain C
this : IsTorsionFree A L
⊢ IsLocalization (algebraMapSubmonoid C A⁰) L

Tactic:
have : IsTorsionFree A C := IsIntegralClosure.isTorsionFree A L

Goal state after:
A : Type u_1
K : Type u_2
inst✝¹⁴ : CommRing A
inst✝¹³ : Field K
inst✝¹² : Algebra A K
inst✝¹¹ : IsFractionRing A K
L : Type u_3
inst✝¹⁰ : Field L
C : Type u_4
inst✝⁹ : CommRing C
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra A L
inst✝⁶ : IsScalarTower A K L
inst✝⁵ : Algebra C L
inst✝⁴ : IsIntegralClosure C A L
inst✝³ : Algebra A C
inst✝² : IsScalarTower A C L
inst✝¹ : IsDomain A
inst✝ : Algebra.IsAlgebraic K L
this✝¹ : IsDomain C
this✝ : IsTorsionFree A L
this : IsTorsionFree A C
⊢ IsLocalization (algebraMapSubmonoid C A⁰) L
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: case neg
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
F : Type u_6
inst✝¹ : Field F
inst✝ : Algebra K F
x : L
hf : (Polynomial.map (algebraMap K F) (minpoly K x)).Splits
injKxL : Function.Injective ⇑(algebraMap (↥K⟮x⟯) L)
hx : ¬IsIntegral K x
⊢ (algebraMap K F) ((Algebra.trace K ↥K⟮x⟯) (gen K x)) = ((minpoly K x).aroots F).sum

pp: case pos
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
F : Type u_6
inst✝¹ : Field F
inst✝ : Algebra K F
x : L
hf : (Polynomial.map (algebraMap K F) (minpoly K x)).Splits
injKxL : Function.Injective ⇑(algebraMap (↥K⟮x⟯) L)
hx : IsIntegral K x
⊢ (algebraMap K F) ((Algebra.trace K ↥K⟮x⟯) (gen K x)) = ((minpoly K x).aroots F).sum

Tactic:
· simp [minpoly.eq_zero hx, trace_gen_eq_zero hx, aroots_def]

Goal state after:
case pos
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
F : Type u_6
inst✝¹ : Field F
inst✝ : Algebra K F
x : L
hf : (Polynomial.map (algebraMap K F) (minpoly K x)).Splits
injKxL : Function.Injective ⇑(algebraMap (↥K⟮x⟯) L)
hx : IsIntegral K x
⊢ (algebraMap K F) ((Algebra.trace K ↥K⟮x⟯) (gen K x)) = ((minpoly K x).aroots F).sum
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: n : ℕ
a b : ZMod n
⊢ |a.valMinAbs| = |b.valMinAbs| ↔ a = b ∨ a = -b

Tactic:
rw [← natAbs_valMinAbs_eq_natAbs_valMinAbs, Int.abs_eq_natAbs, Int.abs_eq_natAbs]

Goal state after:
n : ℕ
a b : ZMod n
⊢ ↑a.valMinAbs.natAbs = ↑b.valMinAbs.natAbs ↔ a.valMinAbs.natAbs = b.valMinAbs.natAbs
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : ¬Algebra.IsSeparable K L
p : ℕ
hp : ExpChar K p
this✝ : p ≠ 0
x : L
h₀ : FiniteDimensional K L
hx : ¬IsSeparable K x
g : K[X]
hg₁ : g.Separable
n : ℕ
hg₂ : (expand K (p ^ (n + 1))) g = minpoly K x
h : p ^ (n + 1) ∣ g.natDegree * p ^ (n + 1) - 1
this : p ^ (n + 1) = 1
⊢ g = minpoly K x

Tactic:
by simpa [this] using hg₂

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

Goal state before:
pp: G : Type u_1
inst✝⁸ : Group G
A : Type u_5
B : Type u_6
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
inst✝³ : FaithfulSMul A B
inst✝² : MulSemiringAction G B
inst✝¹ : IsGaloisGroup G A B
inst✝ : Finite G
⊢ Nat.card G = finrank A B

Tactic:
have := IsDomain.of_faithfulSMul A B
  let := FractionRing.liftAlgebra A (FractionRing B)
  let := IsFractionRing.mulSemiringAction G B (FractionRing B)
  rw [IsGaloisGroup.card_eq_finrank G (FractionRing A) (FractionRing B),
    IsFractionRing.finrank_eq A (FractionRing A) B (FractionRing B)]

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

Goal state before:
pp: G : Type u_1
inst✝¹⁹ : Group G
A : Type u_5
B : Type u_6
C : Type u_7
inst✝¹⁸ : CommRing A
inst✝¹⁷ : CommRing B
inst✝¹⁶ : CommRing C
inst✝¹⁵ : IsDomain C
inst✝¹⁴ : Algebra A B
inst✝¹³ : Algebra A C
inst✝¹² : Algebra B C
inst✝¹¹ : FaithfulSMul A B
inst✝¹⁰ : FaithfulSMul B C
inst✝⁹ : IsScalarTower A B C
inst✝⁸ : Finite G
N : Subgroup G
inst✝⁷ : N.Normal
inst✝⁶ : MulSemiringAction G C
hG : IsGaloisGroup G A C
inst✝⁵ : MulSemiringAction G B
inst✝⁴ : MulSemiringAction (G ⧸ N) B
inst✝³ : SMulCommClass (G ⧸ N) A B
inst✝² : SMulDistribClass G B C
inst✝¹ : IsScalarTower G (G ⧸ N) B
inst✝ : IsGaloisGroup (↥N) B C
g₁✝ g₂✝ : G ⧸ N
g₁ g₂ : G
this✝¹ : FaithfulSMul A C
h' : ∀ (g : G), (∀ (x : B), g • x = x) → g ∈ N
this✝ : ∀ {g : G}, Quotient.mk'' g = (QuotientGroup.mk' N) g
h : ∀ (a : B), (g₂⁻¹ * g₁) • a = a
this : g₂⁻¹ * g₁ ∈ N
⊢ g₂⁻¹ * g₁⁻¹⁻¹ ∈ N

Tactic:
inv_inv

Goal state after:
G : Type u_1
inst✝¹⁹ : Group G
A : Type u_5
B : Type u_6
C : Type u_7
inst✝¹⁸ : CommRing A
inst✝¹⁷ : CommRing B
inst✝¹⁶ : CommRing C
inst✝¹⁵ : IsDomain C
inst✝¹⁴ : Algebra A B
inst✝¹³ : Algebra A C
inst✝¹² : Algebra B C
inst✝¹¹ : FaithfulSMul A B
inst✝¹⁰ : FaithfulSMul B C
inst✝⁹ : IsScalarTower A B C
inst✝⁸ : Finite G
N : Subgroup G
inst✝⁷ : N.Normal
inst✝⁶ : MulSemiringAction G C
hG : IsGaloisGroup G A C
inst✝⁵ : MulSemiringAction G B
inst✝⁴ : MulSemiringAction (G ⧸ N) B
inst✝³ : SMulCommClass (G ⧸ N) A B
inst✝² : SMulDistribClass G B C
inst✝¹ : IsScalarTower G (G ⧸ N) B
inst✝ : IsGaloisGroup (↥N) B C
g₁✝ g₂✝ : G ⧸ N
g₁ g₂ : G
this✝¹ : FaithfulSMul A C
h' : ∀ (g : G), (∀ (x : B), g • x = x) → g ∈ N
this✝ : ∀ {g : G}, Quotient.mk'' g = (QuotientGroup.mk' N) g
h : ∀ (a : B), (g₂⁻¹ * g₁) • a = a
this : g₂⁻¹ * g₁ ∈ N
⊢ g₂⁻¹ * g₁ ∈ N
Module: Mathlib.LinearAlgebra.Quotient.Pi

Goal state before:
pp: case h₁
ι : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
Ms : ι → Type u_3
inst✝⁵ : (i : ι) → AddCommGroup (Ms i)
inst✝⁴ : (i : ι) → Module R (Ms i)
N : Type u_4
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (Ms i)
q : Submodule R N
f : (i : ι) → Ms i →ₗ[R] N
hf : ∀ (i : ι), p i ≤ comap (f i) q
i : ι
x : Ms i ⧸ p i
⊢ i ∉ Finset.univ → ((p i).mapQ q (f i) ⋯) (Pi.single i x i) = 0

Tactic:
intros

Goal state after:
case h₁
ι : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
Ms : ι → Type u_3
inst✝⁵ : (i : ι) → AddCommGroup (Ms i)
inst✝⁴ : (i : ι) → Module R (Ms i)
N : Type u_4
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (Ms i)
q : Submodule R N
f : (i : ι) → Ms i →ₗ[R] N
hf : ∀ (i : ι), p i ≤ comap (f i) q
i : ι
x : Ms i ⧸ p i
a✝ : i ∉ Finset.univ
⊢ ((p i).mapQ q (f i) ⋯) (Pi.single i x i) = 0