mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.ContinuousPreimage

Goal state before:
pp: X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝¹⁰ : TopologicalSpace X
inst✝⁹ : MeasurableSpace X
inst✝⁸ : BorelSpace X
inst✝⁷ : R1Space X
inst✝⁶ : TopologicalSpace Y
inst✝⁵ : MeasurableSpace Y
inst✝⁴ : BorelSpace Y
inst✝³ : R1Space Y
inst✝² : TopologicalSpace Z
μ : Measure X
ν : Measure Y
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : IsLocallyFiniteMeasure ν
f : Z → C(X, Y)
hf : Continuous[inst✝², _] f
hfm : ∀ (z : Z), MeasurePreserving (⇑(f z)) μ ν
s : Set X
t : Set Y
htm : NullMeasurableSet t ν
ht : ν t ≠ ∞
z : Z
hz : ∀ᶠ (ε : ℝ≥0∞) in 𝓝 0, ε < μ ((⇑(f z) ⁻¹' t) ∆ s)
w : Z
hw : μ ((⇑(f w) ⁻¹' t) ∆ (⇑(f z) ⁻¹' t)) < μ ((⇑(f z) ⁻¹' t) ∆ s)
hw' : ⇑(f w) ⁻¹' t =ᵐ[μ] s
⊢ False

Tactic:
measure_congr (hw'.symmDiff (ae_eq_refl _)),

Goal state after:
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝¹⁰ : TopologicalSpace X
inst✝⁹ : MeasurableSpace X
inst✝⁸ : BorelSpace X
inst✝⁷ : R1Space X
inst✝⁶ : TopologicalSpace Y
inst✝⁵ : MeasurableSpace Y
inst✝⁴ : BorelSpace Y
inst✝³ : R1Space Y
inst✝² : TopologicalSpace Z
μ : Measure X
ν : Measure Y
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : IsLocallyFiniteMeasure ν
f : Z → C(X, Y)
hf : Continuous[inst✝², _] f
hfm : ∀ (z : Z), MeasurePreserving (⇑(f z)) μ ν
s : Set X
t : Set Y
htm : NullMeasurableSet t ν
ht : ν t ≠ ∞
z : Z
hz : ∀ᶠ (ε : ℝ≥0∞) in 𝓝 0, ε < μ ((⇑(f z) ⁻¹' t) ∆ s)
w : Z
hw : μ (s ∆ (⇑(f z) ⁻¹' t)) < μ ((⇑(f z) ⁻¹' t) ∆ s)
hw' : ⇑(f w) ⁻¹' t =ᵐ[μ] s
⊢ False
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
this : SigmaFinite (ν.withDensity f)
⊢ μ.rnDeriv (ν.withDensity f) =ᵐ[ν] fun x ↦ (f x)⁻¹ * μ.rnDeriv ν x

Tactic:
refine (withDensity_absolutelyContinuous' hf hf_ne_zero).ae_eq ?_

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
this : SigmaFinite (ν.withDensity f)
⊢ μ.rnDeriv (ν.withDensity f) =ᵐ[ν.withDensity f] fun x ↦ (f x)⁻¹ * μ.rnDeriv ν x
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: case h₁
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen[inst✝] n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure[inst✝] (image2 ϕ v s) ⊆ c
k : Set β := closure[inst✝] (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u ↦ (closure[inst✝] (image2 ϕ (u ∩ v) s))ᶜ
hj₁ : ∀ u ∈ f, IsOpen[inst✝] (j u)
hj₂ : k \ n ⊆ ⋃ u ∈ f, j u
g : Set (Set τ)
hg₁ : ∀ u ∈ g, u ∈ f
hg₂ : g.Finite
hg₃ : k \ n ⊆ ⋃ i ∈ g, j i
w : Set τ := (⋂ u ∈ g, u) ∩ v
hw₂ : w ∈ f
u : Set τ
hu : u ∈ g
⊢ u ⊆ u

Tactic:
all_goals exact Subset.rfl

Goal state after:
Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj

Goal state before:
pp: X : Type u_1
Y : Type u_2
s F : Set X
V : SetRel Y Y
S : X → X
T : Y → Y
φ : X → Y
n : ℕ
h : Semiconj φ S T
h' : IsDynCoverOf S F (map φ φ ⁻¹' V) n s
x : X
hx : x ∈ F
y : X
hy : y ∈ s
hxy : (x, y) ∈ dynEntourage S (map φ φ ⁻¹' V) n
⊢ (x, y) ∈ map φ φ ⁻¹' dynEntourage T V n

Tactic:
rwa [h.preimage_dynEntourage V n]

Goal state after:
Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy

Goal state before:
pp: X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
U : SetRel X X
⊢ 0 ≤ netEntropyInfEntourage T F U

Tactic:
apply Monotone.expGrowthInf_nonneg

Goal state after:
case h
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
U : SetRel X X
⊢ Monotone fun n ↦ ↑(netMaxcard T F U n)

case h'
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
U : SetRel X X
⊢ (fun n ↦ ↑(netMaxcard T F U n)) ≠ 0
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

Goal state before:
pp: X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
U : SetRel X X
⊢ 0 ≤ coverEntropyInfEntourage T F U

Tactic:
apply Monotone.expGrowthInf_nonneg

Goal state after:
case h
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
U : SetRel X X
⊢ Monotone fun n ↦ ↑(coverMincard T F U n)

case h'
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
U : SetRel X X
⊢ (fun n ↦ ↑(coverMincard T F U n)) ≠ 0
Module: Mathlib.ModelTheory.LanguageMap

Goal state before:
pp: case refine_1.inr
L : Language
L' : Language
M : Type w
inst✝² : L.Structure M
α : Type u_1
inst✝¹ : (constantsOn α).Structure M
A B : Set M
h : A ⊆ B
N : Type w'
inst✝ : L.Structure N
f : M ↪[L] N
n : ℕ
x : Fin n → M
c : (constantsOn ↑A).Functions n
⊢ f.toFun (funMap (Sum.inr c) x) = funMap (Sum.inr c) (f.toFun ∘ x)

Tactic:
cases n with
      | zero => rfl
      | succ n => exact isEmptyElim c

Goal state after:
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
motive : (x : E) → x ∈ solvableByRad F E → Prop
mem : ∀ (x : F), motive ((algebraMap F E) x) ⋯
add :
  ∀ (x y : E) (hx : x ∈ solvableByRad F E) (hy : y ∈ solvableByRad F E), motive x hx → motive y hy → motive (x + y) ⋯
mul :
  ∀ (x y : E) (hx : x ∈ solvableByRad F E) (hy : y ∈ solvableByRad F E), motive x hx → motive y hy → motive (x * y) ⋯
rad : ∀ (n : ℕ) (x : E) (hn : n ≠ 0) (hx : x ^ n ∈ solvableByRad F E), motive (x ^ n) hx → motive x ⋯
x : E
hx : x ∈ solvableByRad F E
⊢ motive x hx

Tactic:
let s : Subalgebra F E :=
  { carrier := {x | ∃ hx : x ∈ solvableByRad F E, motive x hx}
    algebraMap_mem' a := ⟨algebraMap_mem _ a, mem a⟩
    add_mem' := fun ⟨ha, ha'⟩ ⟨hb, hb'⟩ ↦ ⟨add_mem ha hb, add _ _ ha hb ha' hb'⟩
    mul_mem' := fun ⟨ha, ha'⟩ ⟨hb, hb'⟩ ↦ ⟨mul_mem ha hb, mul _ _ ha hb ha' hb'⟩ }
  let t : IntermediateField F E := Subalgebra.IsAlgebraic.toIntermediateField (S := s) <| by
    rintro x ⟨hx, hx'⟩
    apply isAlgebraic_solvableByRad
    exact hx
  have ht (x n) (hn : n ≠ 0) : x ^ n ∈ t → x ∈ t := by
    rintro ⟨hx, hx'⟩
    exact ⟨rad_mem hn hx, rad _ _ hn hx hx'⟩
  obtain ⟨_, h⟩ := solvableByRad_le (s := t) ht hx
  exact h

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case func
L : Language
L' : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
inst✝¹ : L'.Structure M
φ : L →ᴸ L'
inst✝ : φ.IsExpansionOn M
v : α → M
l✝ : ℕ
f : L.Functions l✝
ts : Fin l✝ → L.Term α
ih : ∀ (a : Fin l✝), Term.realize v (φ.onTerm (ts a)) = Term.realize v (ts a)
⊢ Term.realize v (φ.onTerm (func f ts)) = Term.realize v (func f ts)

Tactic:
simp only [Term.realize, LHom.onTerm, LHom.map_onFunction, ih]

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case succ.mp
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 a, φ.Realize v (snoc xs a)) → ∃ xs, φ.Realize v xs

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, φ.Realize v xs) → ∃ xs a, φ.Realize v (snoc xs a)

Tactic:
· rintro ⟨xs, x, h⟩
      exact ⟨_, 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, φ.Realize v xs) → ∃ xs a, φ.Realize v (snoc xs a)
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
α : Type w
T : L.Theory
s : Set α
M : Type w'
inst✝² : Nonempty M
inst✝¹ : L.Structure M
inst✝ : M ⊨ T
h : Nonempty (↑s ↪ M)
this✝ : Inhabited M
this : (constantsOn α).Structure M := constantsOn.structure (Function.extend Subtype.val (⇑h.some) default)
⊢ M ⊨ (L.lhomWithConstants α).onTheory T ∪ L.distinctConstantsTheory s

Tactic:
refine ((LHom.onTheory_model _ _).2 inferInstance).union ?_

Goal state after:
L : Language
α : Type w
T : L.Theory
s : Set α
M : Type w'
inst✝² : Nonempty M
inst✝¹ : L.Structure M
inst✝ : M ⊨ T
h : Nonempty (↑s ↪ M)
this✝ : Inhabited M
this : (constantsOn α).Structure M := constantsOn.structure (Function.extend Subtype.val (⇑h.some) default)
⊢ M ⊨ L.distinctConstantsTheory s
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
α : Type w
T : L.Theory
s : Set α
M : Type w'
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
⊢ ((L.lhomWithConstants α).onTheory T ∪ L.distinctConstantsTheory s).IsSatisfiable

Tactic:
distinctConstantsTheory_eq_iUnion,

Goal state after:
L : Language
α : Type w
T : L.Theory
s : Set α
M : Type w'
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
⊢ ((L.lhomWithConstants α).onTheory T ∪
      ⋃ t, L.distinctConstantsTheory ↑(Finset.map (Function.Embedding.subtype fun x ↦ x ∈ s) t)).IsSatisfiable
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: case mp
L : Language
T : L.Theory
φ : L.Sentence
this : DecidableEq L.Sentence := ⋯
⊢ (∀ (T0 : Finset L.Sentence), ↑T0 ⊆ T ∪ {Formula.not φ} → IsSatisfiable ↑T0) →
    ∀ (T0 : Finset L.Sentence), ↑T0 ⊆ T → (↑T0 ∪ {Formula.not φ}).IsSatisfiable

pp: case mpr
L : Language
T : L.Theory
φ : L.Sentence
this : DecidableEq L.Sentence := ⋯
⊢ (∀ (T0 : Finset L.Sentence), ↑T0 ⊆ T → (↑T0 ∪ {Formula.not φ}).IsSatisfiable) →
    ∀ (T0 : Finset L.Sentence), ↑T0 ⊆ T ∪ {Formula.not φ} → IsSatisfiable ↑T0

Tactic:
· intro h T0 hT0
    simpa using h (T0 ∪ {Formula.not φ})
      (by
        simp only [Finset.coe_union, Finset.coe_singleton]
        exact Set.union_subset_union hT0 (Set.Subset.refl _))

Goal state after:
case mpr
L : Language
T : L.Theory
φ : L.Sentence
this : DecidableEq L.Sentence := ⋯
⊢ (∀ (T0 : Finset L.Sentence), ↑T0 ⊆ T → (↑T0 ∪ {Formula.not φ}).IsSatisfiable) →
    ∀ (T0 : Finset L.Sentence), ↑T0 ⊆ T ∪ {Formula.not φ} → IsSatisfiable ↑T0
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
T : L.Theory
h : T.IsComplete
M : Type u_1
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
⊢ {φ | T ⊨ᵇ φ} = L.completeTheory M

Tactic:
by
  ext φ
  simp only [Set.mem_ofPred_eq, L.mem_completeTheory]
  refine ⟨fun h_models => h_models.realize_sentence M, fun h_realize => ?_⟩
  cases h.2 φ with
  | inl hT => exact hT
  | inr hT =>
      have : M ⊨ φ.not := hT.realize_sentence M
      rw [Sentence.realize_not] at this
      contradiction

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

Goal state before:
pp: a : ℕ
h✝ : ¬ℵ₀ ≤ ↑a
x✝ : ∃ n, ↑a = ↑n ∧ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
n : ℕ
han : ↑a = ↑n
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
h : p ^ k = n
⊢ ↑p ^ k = ↑a

Tactic:
by rw [han]; exact mod_cast h

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

Goal state before:
pp: case intro
σ K : Type u
inst✝² : Fintype K
inst✝¹ : Field K
inst✝ : Finite σ
val✝ : Fintype σ
⊢ FiniteDimensional K (R σ K)

Tactic:
FiniteDimensional,

Goal state after:
case intro
σ K : Type u
inst✝² : Fintype K
inst✝¹ : Field K
inst✝ : Finite σ
val✝ : Fintype σ
⊢ Module.Finite K (R σ K)
Module: Mathlib.FieldTheory.Galois.Profinite

Goal state before:
pp: case e'_4
k : Type u_3
K : Type u_4
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
L : (FiniteGaloisIntermediateField k K)ᵒᵖ
e_2✝ : ↑((asProfiniteGaloisGroupFunctor k K).obj L).toProfinite.toTop = Gal(↥(unop L).toIntermediateField/k)
⊢ ((asProfiniteGaloisGroupFunctor k K).obj L).toProfinite.toTop.str = krullTopology k ↥(unop L).toIntermediateField

Tactic:
exact (DiscreteTopology.eq_bot (α := L.unop ≃ₐ[k] L.unop)).symm

Goal state after:
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ ProfiniteGrp.{max v u}
cone : Limits.Cone F
m : cone.pt ⟶ (limitCone F).pt
h : ∀ (j : J), m ≫ (limitCone F).π.app j = cone.π.app j
⊢ m =
    ofHom
      (let __src :=
        TopCat.Hom.hom
          ((Profinite.limitConeIsLimit (F ⋙ forget₂ ProfiniteGrp.{max u v} Profinite)).lift
              ((forget₂ ProfiniteGrp.{max u v} Profinite).mapCone cone)).hom;
      { toFun := __src.toFun, map_one' := ⋯, map_mul' := ⋯, continuous_toFun := ⋯ })

Tactic:
apply (forget₂ ProfiniteGrp Profinite).map_injective

Goal state after:
J : Type v
inst✝ : SmallCategory J
F : J ⥤ ProfiniteGrp.{max v u}
cone : Limits.Cone F
m : cone.pt ⟶ (limitCone F).pt
h : ∀ (j : J), m ≫ (limitCone F).π.app j = cone.π.app j
⊢ (forget₂ ProfiniteGrp.{max u v} Profinite).map m =
    (forget₂ ProfiniteGrp.{max u v} Profinite).map
      (ofHom
        (let __src :=
          TopCat.Hom.hom
            ((Profinite.limitConeIsLimit (F ⋙ forget₂ ProfiniteGrp.{max u v} Profinite)).lift
                ((forget₂ ProfiniteGrp.{max u v} Profinite).mapCone cone)).hom;
        { toFun := __src.toFun, map_one' := ⋯, map_mul' := ⋯, continuous_toFun := ⋯ }))
Module: Mathlib.FieldTheory.IsRealClosed.Basic

Goal state before:
pp: case h.inr
R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
n : ℕ
ih : ∀ m < n, ∀ {x : R}, IsSquare x → m ≠ 0 → ∃ r, x = r ^ m
x : R
hx : IsSquare x
hn : n ≠ 0
odd : Odd n
⊢ ∃ r, x = r ^ n

Tactic:
exact exists_eq_pow_of_odd x odd

Goal state after:
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
g : L →+* N
p : ℕ
inst✝⁷ : ExpChar M p
inst✝⁶ : ExpChar K p
inst✝⁵ : PerfectRing M p
inst✝⁴ : IsPRadical i p
inst✝³ : ExpChar L p
inst✝² : ExpChar N p
inst✝¹ : IsPRadical g p
inst✝ : IsPRadical (g.comp i) p
⊢ lift g (lift i j p) p = lift (g.comp i) j p

Tactic:
by
  refine IsPRadical.injective_comp_of_perfect _ (g.comp i) p ?_
  simp_rw [← RingHom.comp_assoc _ _ (lift g _ p), lift_comp]

Goal state after:
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: case mp
G : Type u_1
inst✝¹ : Group G
D H : Subgroup G
inst✝ : D.FiniteIndex
hD_le_H : D ≤ H
t : Set ↥H
ht : IsComplement t ↑(D.subgroupOf H) ∧ 1 ∈ t
hf : t.Finite
x : G
⊢ (∃ y ∈ t, ∃ d ∈ D, ↑y * d = x) → x ∈ H

pp: case mpr
G : Type u_1
inst✝¹ : Group G
D H : Subgroup G
inst✝ : D.FiniteIndex
hD_le_H : D ≤ H
t : Set ↥H
ht : IsComplement t ↑(D.subgroupOf H) ∧ 1 ∈ t
hf : t.Finite
x : G
⊢ x ∈ H → ∃ y ∈ t, ∃ d ∈ D, ↑y * d = x

Tactic:
· rintro ⟨⟨y, hy⟩, -, d, h, rfl⟩
    exact H.mul_mem hy (hD_le_H h)

Goal state after:
case mpr
G : Type u_1
inst✝¹ : Group G
D H : Subgroup G
inst✝ : D.FiniteIndex
hD_le_H : D ≤ H
t : Set ↥H
ht : IsComplement t ↑(D.subgroupOf H) ∧ 1 ∈ t
hf : t.Finite
x : G
⊢ x ∈ H → ∃ y ∈ t, ∃ d ∈ D, ↑y * d = x
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
j : ι
hj : j ∈ s
⊢ ∃ k ∈ s, (H k).FiniteIndex

Tactic:
by_cases hcovers' : ⋃ i ∈ s.filter (H · = H j), g i • (H i : Set G) = Set.univ

Goal state after:
case pos
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
j : ι
hj : j ∈ s
hcovers' : ⋃ i ∈ {x ∈ s | H x = H j}, g i • ↑(H i) = Set.univ
⊢ ∃ k ∈ s, (H k).FiniteIndex

case neg
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
j : ι
hj : j ∈ s
hcovers' : ¬⋃ i ∈ {x ∈ s | H x = H j}, g i • ↑(H i) = Set.univ
⊢ ∃ k ∈ s, (H k).FiniteIndex
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
hζ : (primitiveRoots n K).Nonempty
H : Irreducible (X ^ n - C a)
hα : α ^ n = (algebraMap K L) a
this✝ : Fact (Irreducible (X ^ n - C a))
this : IsSplittingField K K[n√a] (X ^ n - C a) := isSplittingField_AdjoinRoot_X_pow_sub_C hζ H
⊢ Function.Surjective ⇑(liftAlgHom (X ^ n - C a) (Algebra.ofId K L) α ⋯)

Tactic:
← AlgHom.range_eq_top,

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
hζ : (primitiveRoots n K).Nonempty
H : Irreducible (X ^ n - C a)
hα : α ^ n = (algebraMap K L) a
this✝ : Fact (Irreducible (X ^ n - C a))
this : IsSplittingField K K[n√a] (X ^ n - C a) := isSplittingField_AdjoinRoot_X_pow_sub_C hζ H
⊢ (liftAlgHom (X ^ n - C a) (Algebra.ofId K L) α ⋯).range = ⊤
Module: Mathlib.FieldTheory.PurelyInseparable.Exponent

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsPurelyInseparable K L
a : L
h : a ∈ (algebraMap K L).range
⊢ elemExponent K a = 0

Tactic:
by
  classical
  apply (Nat.find_eq_zero _).mpr
  rw [pow_zero, pow_one]
  obtain ⟨y, hy⟩ := h
  exact ⟨y, hy ▸ minpoly.eq_X_sub_C L y⟩

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

Goal state before:
pp: case prime
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : IsPurelyInseparable K L
inst✝ : FiniteDimensional K L
p : ℕ
h✝ : ExpChar K p
hp : Nat.Prime p
hchar✝ : CharP K p
e : ℕ := Nat.log (ringExpChar K) (Module.finrank K L)
a : L
h_elemexp_bound : ∀ (a : L), elemExponent K a ≤ e
⊢ a ^ ringExpChar K ^ (elemExponent K a + (e - elemExponent K a)) = a ^ ringExpChar K ^ e

Tactic:
Nat.add_sub_cancel' (h_elemexp_bound a)

Goal state after:
case prime
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : IsPurelyInseparable K L
inst✝ : FiniteDimensional K L
p : ℕ
h✝ : ExpChar K p
hp : Nat.Prime p
hchar✝ : CharP K p
e : ℕ := Nat.log (ringExpChar K) (Module.finrank K L)
a : L
h_elemexp_bound : ∀ (a : L), elemExponent K a ≤ e
⊢ a ^ ringExpChar K ^ e = a ^ ringExpChar K ^ e
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
H : Function.Injective ⇑(fa.range.mulMap fb.range)
⊢ i =
    (fa.range.mulMap fb.range).comp
      ↑(Algebra.TensorProduct.congr (AlgEquiv.ofInjective fa ⋯) (AlgEquiv.ofInjective fb ⋯))

Tactic:
ext <;> simp [fa, fb]

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
q n : ℕ
hF : ExpChar F q
ι : Type u_1
v : ι → E
inst✝ : Algebra.IsSeparable F E
h : ∀ (s : Finset ι), LinearIndependent F (v ∘ Subtype.val)
s : Finset ι
E' : IntermediateField F E := adjoin F ↑(Finset.image v s)
⊢ LinearIndependent F ((fun x ↦ v x ^ q ^ n) ∘ Subtype.val)

Tactic:
have : FiniteDimensional F E' := finiteDimensional_adjoin
    fun x _ ↦ Algebra.IsIntegral.isIntegral x

Goal state after:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
q n : ℕ
hF : ExpChar F q
ι : Type u_1
v : ι → E
inst✝ : Algebra.IsSeparable F E
h : ∀ (s : Finset ι), LinearIndependent F (v ∘ Subtype.val)
s : Finset ι
E' : IntermediateField F E := adjoin F ↑(Finset.image v s)
this : FiniteDimensional F ↥E'
⊢ LinearIndependent F ((fun x ↦ v x ^ q ^ n) ∘ Subtype.val)
Module: Mathlib.FieldTheory.RatFunc.IntermediateField

Goal state before:
pp: K : Type u_1
inst✝ : Field K
f : K⟮X⟯
⊢ (algebraMap K[X] K⟮X⟯) f.num - f * (algebraMap K[X] K⟮X⟯) f.denom = 0

Tactic:
nth_rw 2 [← num_div_denom f]

Goal state after:
K : Type u_1
inst✝ : Field K
f : K⟮X⟯
⊢ (algebraMap K[X] K⟮X⟯) f.num -
      (algebraMap K[X] K⟮X⟯) f.num / (algebraMap K[X] K⟮X⟯) f.denom * (algebraMap K[X] K⟮X⟯) f.denom =
    0
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
S : Set K
inst✝¹ : IsPurelyInseparable F E
M : IntermediateField F K := adjoin F S
inst✝ : Algebra.IsAlgebraic F ↥M
L : IntermediateField E K := adjoin E S
E' : IntermediateField F K := (IsScalarTower.toAlgHom F E K).fieldRange
⊢ sepDegree E ↥L = sepDegree F ↥M

Tactic:
let j : E ≃ₐ[F] E' := AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F E K)

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
inst✝³ : Algebra E K
inst✝² : IsScalarTower F E K
S : Set K
inst✝¹ : IsPurelyInseparable F E
M : IntermediateField F K := adjoin F S
inst✝ : Algebra.IsAlgebraic F ↥M
L : IntermediateField E K := adjoin E S
E' : IntermediateField F K := (IsScalarTower.toAlgHom F E K).fieldRange
j : E ≃ₐ[F] ↥E' := AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F E K)
⊢ sepDegree E ↥L = sepDegree F ↥M
Module: Mathlib.FieldTheory.Relrank

Goal state before:
pp: E : Type v
inst✝ : Field E
A B : Subfield E
h : A ≤ B
⊢ A.relrank B = Module.rank ↥A ↥(extendScalars h)

Tactic:
by
  rw [relrank]
  have := inf_of_le_left h
  congr!

Goal state after:
Module: Mathlib.FieldTheory.Relrank

Goal state before:
pp: E : Type v
inst✝ : Field E
A B : Subfield E
h : A ≤ B
⊢ A.relrank B * Module.rank (↥B) E = Module.rank (↥A) E

Tactic:
rw [relrank_eq_rank_of_le h]

Goal state after:
E : Type v
inst✝ : Field E
A B : Subfield E
h : A ≤ B
⊢ Module.rank ↥A ↥(extendScalars h) * Module.rank (↥B) E = Module.rank (↥A) E
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
⊢ Module.rank F ↥A * A.relrank B = Module.rank F ↥B

Tactic:
rw [relrank_eq_rank_of_le h]

Goal state after:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
A B : IntermediateField F E
h : A ≤ B
⊢ Module.rank F ↥A * Module.rank ↥A ↥(extendScalars h) = Module.rank F ↥B
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation

Goal state before:
pp: V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x✝ : V
⊢ (o.rotation 0) x✝ = (LinearIsometryEquiv.refl ℝ V) x✝

Tactic:
simp [rotation]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation

Goal state before:
pp: V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
⊢ (o.rotation ↑π) x = (LinearIsometryEquiv.neg ℝ) x

Tactic:
simp [rotation]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation

Goal state before:
pp: V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
⊢ (o.rotation ↑(π / 2)) x = o.rightAngleRotation x

Tactic:
simp [rotation]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

Goal state before:
pp: V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
hr : 0 < r
⊢ o.oangle (r • x) y = o.oangle x y

Tactic:
simp [oangle, Complex.arg_real_mul _ hr]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

Goal state before:
pp: V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
hr : 0 < r
⊢ o.oangle x (r • y) = o.oangle x y

Tactic:
simp [oangle, Complex.arg_real_mul _ hr]

Goal state after: