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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
⊢ μ.rnDeriv (μ + ν) =ᵐ[ν] fun x ↦ μ.rnDeriv ν x / (μ.rnDeriv ν x + 1)

Tactic:
have h_add : (μ + ν).rnDeriv (μ + ν) =ᵐ[ν] μ.rnDeriv (μ + ν) + ν.rnDeriv (μ + ν) :=
    (ae_add_measure_iff.mp (μ.rnDeriv_add' ν (μ + ν))).2
  have h_one_add := (ae_add_measure_iff.mp (μ + ν).rnDeriv_self).2
  have : (μ.rnDeriv (μ + ν)) =ᵐ[ν] fun x ↦ 1 - (μ.rnDeriv ν x + 1)⁻¹ := by
    filter_upwards [h_add, h_one_add, rnDeriv_add_self ν μ] with a h4 h5 h6
    rw [h5, Pi.add_apply] at h4
    nth_rw 1 [h4, h6]
    simp
  filter_upwards [this, μ.rnDeriv_lt_top ν] with a ha ha_lt_top
  rw [ha, div_eq_mul_inv]
  refine ENNReal.sub_eq_of_eq_add (by simp) ?_
  nth_rewrite 2 [← one_mul (μ.rnDeriv ν a + 1)⁻¹]
  have h := add_mul (μ.rnDeriv ν a) 1 (μ.rnDeriv ν a + 1)⁻¹
  rwa [ENNReal.mul_inv_cancel (by simp) (by simp [ha_lt_top.ne])] at h

Goal state after:
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case pos
F : Type u_1
inst✝ : Field F
n : ℕ
hn : n = 0
⊢ Group.IsSolvable (X ^ n - 1).Gal

Tactic:
rw [hn, pow_zero, sub_self]
    exact gal_zero_isSolvable

Goal state after:
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case neg
F : Type u_1
inst✝ : Field F
n : ℕ
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - 1 ≠ 0
⊢ Group.IsSolvable (X ^ n - 1).Gal

Tactic:
apply Group.isSolvable_of_comm

Goal state after:
case neg
F : Type u_1
inst✝ : Field F
n : ℕ
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - 1 ≠ 0
⊢ ∀ (a b : (X ^ n - 1).Gal), a * b = b * a
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
this✝¹ : SigmaFinite (map f ν)
this✝ : SigmaFinite (map f (μ.singularPart ν))
this : SigmaFinite (map f (ν.withDensity (μ.rnDeriv ν)))
h_add :
  ∀ᵐ (x : β) ∂map f ν,
    (map f (μ.singularPart ν) + map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν) x =
      ((map f (μ.singularPart ν)).rnDeriv (map f ν) + (map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν)) x
⊢ (fun x ↦ (map f (μ.singularPart ν) + map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν) (f x)) =ᵐ[ν]
    (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv ν

Tactic:
hf.ae_map_iff,

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
this✝¹ : SigmaFinite (map f ν)
this✝ : SigmaFinite (map f (μ.singularPart ν))
this : SigmaFinite (map f (ν.withDensity (μ.rnDeriv ν)))
h_add :
  ∀ᵐ (x : α) ∂ν,
    (map f (μ.singularPart ν) + map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν) (f x) =
      ((map f (μ.singularPart ν)).rnDeriv (map f ν) + (map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν)) (f x)
⊢ (fun x ↦ (map f (μ.singularPart ν) + map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν) (f x)) =ᵐ[ν]
    (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv ν
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case neg
F : Type u_1
inst✝ : Field F
n : ℕ
a : F
h : (map (RingHom.id F) (X ^ n - 1)).Splits
ha : ¬a = 0
ha' : (algebraMap F (X ^ n - C a).SplittingField) a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - C a ≠ 0
hn''' : X ^ n - 1 ≠ 0
mem_range : ∀ {c : (X ^ n - C a).SplittingField}, c ^ n = 1 → ∃ d, (algebraMap F (X ^ n - C a).SplittingField) d = c
⊢ Group.IsSolvable (X ^ n - C a).Gal

Tactic:
apply Group.isSolvable_of_comm

Goal state after:
case neg
F : Type u_1
inst✝ : Field F
n : ℕ
a : F
h : (map (RingHom.id F) (X ^ n - 1)).Splits
ha : ¬a = 0
ha' : (algebraMap F (X ^ n - C a).SplittingField) a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - C a ≠ 0
hn''' : X ^ n - 1 ≠ 0
mem_range : ∀ {c : (X ^ n - C a).SplittingField}, c ^ n = 1 → ∃ d, (algebraMap F (X ^ n - C a).SplittingField) d = c
⊢ ∀ (a_1 b : (X ^ n - C a).Gal), a_1 * b = b * a_1
Module: Mathlib.FieldTheory.IsAlgClosed.Classification

Goal state before:
pp: K : Type u
L : Type v
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
inst✝¹ : CharZero K
inst✝ : CharZero L
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
s : Set K
hs : IsTranscendenceBasis ℤ Subtype.val
t : Set L
ht : IsTranscendenceBasis ℤ Subtype.val
⊢ ℵ₀ < Cardinal.lift.{u, v} #L

Tactic:
← lift_mk_eq'.2 hKL,

Goal state after:
K : Type u
L : Type v
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
inst✝¹ : CharZero K
inst✝ : CharZero L
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
s : Set K
hs : IsTranscendenceBasis ℤ Subtype.val
t : Set L
ht : IsTranscendenceBasis ℤ Subtype.val
⊢ ℵ₀ < Cardinal.lift.{v, u} #K
Module: Mathlib.FieldTheory.IsAlgClosed.Classification

Goal state before:
pp: K : Type u
L : Type v
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : IsAlgClosed K
inst✝³ : IsAlgClosed L
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP K p
inst✝ : CharP L p
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
this✝ : Algebra (ZMod p) K := ZMod.algebra K p
this : Algebra (ZMod p) L := ZMod.algebra L p
s : Set K
hs : IsTranscendenceBasis (ZMod p) Subtype.val
t : Set L
ht : IsTranscendenceBasis (ZMod p) Subtype.val
⊢ ℵ₀ < Cardinal.lift.{u, v} #L

Tactic:
← lift_mk_eq'.2 hKL,

Goal state after:
K : Type u
L : Type v
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : IsAlgClosed K
inst✝³ : IsAlgClosed L
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP K p
inst✝ : CharP L p
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
this✝ : Algebra (ZMod p) K := ZMod.algebra K p
this : Algebra (ZMod p) L := ZMod.algebra L p
s : Set K
hs : IsTranscendenceBasis (ZMod p) Subtype.val
t : Set L
ht : IsTranscendenceBasis (ZMod p) Subtype.val
⊢ ℵ₀ < Cardinal.lift.{v, u} #K
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case hq.refine_2
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
hx : x ∈ solvableByRad F E
n : ℕ
hn : n ≠ 0
hα : Group.IsSolvable (minpoly F (x ^ n)).Gal
p : F[X] := minpoly F (x ^ n)
hp : p.comp (X ^ n) ≠ 0
s : Multiset p.SplittingField
hs :
  map (algebraMap F p.SplittingField) p =
    C (map (algebraMap F p.SplittingField) p).leadingCoeff * (Multiset.map (fun x ↦ X - C x) s).prod
q : p.SplittingField
left✝ : q ∈ s
⊢ Group.IsSolvable ((X - C q).comp (X ^ n)).Gal

Tactic:
rw [sub_comp, X_comp, C_comp]

Goal state after:
case hq.refine_2
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
hx : x ∈ solvableByRad F E
n : ℕ
hn : n ≠ 0
hα : Group.IsSolvable (minpoly F (x ^ n)).Gal
p : F[X] := minpoly F (x ^ n)
hp : p.comp (X ^ n) ≠ 0
s : Multiset p.SplittingField
hs :
  map (algebraMap F p.SplittingField) p =
    C (map (algebraMap F p.SplittingField) p).leadingCoeff * (Multiset.map (fun x ↦ X - C x) s).prod
q : p.SplittingField
left✝ : q ∈ s
⊢ Group.IsSolvable (X ^ n - C q).Gal
Module: Mathlib.ModelTheory.Ultraproducts

Goal state before:
pp: case refine_2
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝ : (a : α) → L.Structure (M a)
n : ℕ
r : L.Relations n
x y : Fin n → (a : α) → M a
xy : x ≈ y
hy : RelMap r y
⊢ RelMap r x

Tactic:
refine mem_of_superset (inter_mem hy (iInter_mem.2 xy)) ?_

Goal state after:
case refine_2
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝ : (a : α) → L.Structure (M a)
n : ℕ
r : L.Relations n
x y : Fin n → (a : α) → M a
xy : x ≈ y
hy : RelMap r y
⊢ {x | (fun a ↦ RelMap r fun i ↦ y i a) x} ∩ ⋂ i, {x_1 | (fun a ↦ x i a = y i a) x_1} ⊆
    {x_1 | (fun a ↦ RelMap r fun i ↦ x i a) x_1}
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
l : ℕ
θ : L.BoundedFormula α l.succ
v : α → M
xs : Fin l → M
⊢ (∼(∀' ∼θ)).Realize v xs ↔ ∃ a, θ.Realize v (snoc xs a)

Tactic:
realize_not,

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
l : ℕ
θ : L.BoundedFormula α l.succ
v : α → M
xs : Fin l → M
⊢ ¬(∀' ∼θ).Realize v xs ↔ ∃ a, θ.Realize v (snoc xs a)
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
l : ℕ
θ : L.BoundedFormula α l.succ
v : α → M
xs : Fin l → M
⊢ (∃ x, ¬(∼θ).Realize v (snoc xs x)) ↔ ∃ a, θ.Realize v (snoc xs a)

Tactic:
realize_not,

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
l : ℕ
θ : L.BoundedFormula α l.succ
v : α → M
xs : Fin l → M
⊢ (∃ x, ¬¬θ.Realize v (snoc xs x)) ↔ ∃ a, θ.Realize v (snoc xs a)
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case cons
L : Language
α : Type u'
h : ∀ (t : L.Term α) (l : List (α ⊕ (i : ℕ) × L.Functions i)), listDecode (t.listEncode ++ l) = t :: listDecode l
t : L.Term α
l : List (L.Term α)
lih : listDecode (flatMap listEncode l) = l
⊢ listDecode (flatMap listEncode (t :: l)) = t :: l

Tactic:
rw [flatMap_cons, h t (l.flatMap listEncode), lih]

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case all
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : DecidableEq α
n : ℕ
v : β → M
v' : α → M
n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 :
  ∀ {f : ↥f✝.freeVarFinset → β} {xs : Fin (n✝ + 1) → M},
    (∀ (a : ↥f✝.freeVarFinset), v (f a) = v' ↑a) → ((f✝.restrictFreeVar f).Realize v xs ↔ f✝.Realize v' xs)
f : ↥(∀' f✝).freeVarFinset → β
xs : Fin n✝ → M
hv' : ∀ (a : ↥(∀' f✝).freeVarFinset), v (f a) = v' ↑a
⊢ (∀ (x : M), (f✝.restrictFreeVar f).Realize v (snoc xs x)) ↔ ∀ (x : M), f✝.Realize v' (snoc xs x)

Tactic:
refine forall_congr' (fun _ => ?_)

Goal state after:
case all
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : DecidableEq α
n : ℕ
v : β → M
v' : α → M
n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 :
  ∀ {f : ↥f✝.freeVarFinset → β} {xs : Fin (n✝ + 1) → M},
    (∀ (a : ↥f✝.freeVarFinset), v (f a) = v' ↑a) → ((f✝.restrictFreeVar f).Realize v xs ↔ f✝.Realize v' xs)
f : ↥(∀' f✝).freeVarFinset → β
xs : Fin n✝ → M
hv' : ∀ (a : ↥(∀' f✝).freeVarFinset), v (f a) = v' ↑a
x✝ : M
⊢ (f✝.restrictFreeVar f).Realize v (snoc xs x✝) ↔ f✝.Realize v' (snoc xs x✝)
Module: Mathlib.ModelTheory.Substructures

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

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

Goal state after:
Module: Mathlib.ModelTheory.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
inst✝ : Small.{u, w} ↑s
⊢ Small.{u, w} ↥((closure L).toFun s)

Tactic:
by
  rw [← SetLike.coe_sort_coe, Substructure.coe_closure_eq_range_term_realize]
  exact small_range _

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
⊢ Small.{u, w} ↥⊥

Tactic:
rw [← closure_empty]

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
⊢ Small.{u, w} ↥((closure L).toFun ∅)
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
N : Type u_1
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M →[L] N
⊢ ↑f.range = ↑⊤ ↔ Function.Surjective ⇑f

Tactic:
range_coe,

Goal state after:
L : Language
M : Type w
N : Type u_1
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M →[L] N
⊢ Set.range ⇑f = ↑⊤ ↔ Function.Surjective ⇑f
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
p : L.Substructure N
f : M ↪[L] N
h : ∀ (c : M), f c ∈ p
n : ℕ
r : L.Relations n
x : Fin n → M
⊢ RelMap r (⇑(Hom.codRestrict p f.toHom h) ∘ x) ↔ RelMap r x

Tactic:
by
    rw [← p.subtype.map_rel]
    change RelMap r (Hom.comp p.subtype.toHom (f.toHom.codRestrict p h) ∘ x) ↔ _
    rw [Hom.subtype_comp_codRestrict, ← f.map_rel]
    rfl

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:
definableFun_iff_empty_definableFun_with_params

Goal state after:
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
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type u_1
L : Language
inst✝¹ : L.Structure M
α : Type u_2
β : Type u_3
A : Set M
f : (α → M) → M
inst✝ : Finite α
g : (β → M) → α → M
hg : DefinableMap L A g
hf : DefinableFun L A f
G : (Option β → M) → Option α → M :=
  fun w j ↦
    match j with
    | none => w none
    | some i => g (w ∘ some) i
i : Option α
⊢ DefinableFun L A fun x ↦ G x i

Tactic:
cases i with

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
n : ℕ
⊢ M ⊨ Sentence.cardGe L n ↔ ↑n ≤ #M

Tactic:
by
  rw [← lift_mk_fin, ← lift_le.{0}, lift_lift, lift_mk_le, Sentence.cardGe, Sentence.Realize,
    BoundedFormula.realize_exs]
  simp_rw [BoundedFormula.realize_foldr_inf]
  simp only [Function.comp_apply, List.mem_map, Prod.exists, Ne, List.mem_product,
    List.mem_finRange, forall_exists_index, and_imp, List.mem_filter, true_and]
  refine ⟨?_, fun xs => ⟨xs.some, ?_⟩⟩
  · rintro ⟨xs, h⟩
    refine ⟨⟨xs, fun i j ij => ?_⟩⟩
    contrapose! ij
    exact h _ i j (by simpa using ij) rfl
  · rintro _ i j ij rfl
    simpa using ij

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
T : L.Theory
κ : Cardinal.{w}
M : Type w'
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
N : ((L.lhomWithConstants (Quotient.out κ)).onTheory T ∪ L.distinctConstantsTheory Set.univ).ModelType
⊢ lift.{max u v w, w} κ ≤ #↑(ModelType.reduct (L.lhomWithConstants (Quotient.out κ)) ⋯.bundled)

Tactic:
have : N ⊨ distinctConstantsTheory _ _ := N.is_model.mono Set.subset_union_right

Goal state after:
L : Language
T : L.Theory
κ : Cardinal.{w}
M : Type w'
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
N : ((L.lhomWithConstants (Quotient.out κ)).onTheory T ∪ L.distinctConstantsTheory Set.univ).ModelType
this : ↑N ⊨ L.distinctConstantsTheory Set.univ
⊢ lift.{max u v w, w} κ ≤ #↑(ModelType.reduct (L.lhomWithConstants (Quotient.out κ)) ⋯.bundled)
Module: Mathlib.ModelTheory.Satisfiability

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

Tactic:
exact Set.union_subset_union hT0 (Set.Subset.refl _)

Goal state after:
Module: Mathlib.GroupTheory.OreLocalization.Cardinality

Goal state before:
pp: R : Type u
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type v
inst✝ : MulAction R X
hc : ∀ (s s' : ↥S), Commute s s'
h✝ : Infinite X
key : ∀ (x : X) (s s' : ↥S), s • x = s' • x → Commute s s' → x /ₒ s = x /ₒ s'
i : X × ↥S → OreLocalization S X := fun x ↦ x.1 /ₒ x.2
hsurj : Surjective i
hi : RightInverse (surjInv hsurj) i
j : OreLocalization S X → X × X := (fun x ↦ (x.1, x.2 • x.1)) ∘ surjInv hsurj
this : Injective j
⊢ #(OreLocalization S X) ≤ lift.{u, v} #X

Tactic:
have := lift_mk_le_lift_mk_of_injective this
    rwa [lift_umax.{v, u}, lift_id', mk_prod, lift_id, lift_mul, mul_eq_self (by simp)] at this

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

Goal state before:
pp: case refine_2.inr.inr.inr.hbc
a : Cardinal.{u}
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this : ∀ {a : Cardinal.{u}}, ℵ₀ ≤ a → ∀ (b c : Cardinal.{u}), a ∣ b * c → b * c ≠ 0 → c ≤ b → a ∣ b ∨ a ∣ c
h : ¬c ≤ b
h✝ : b ≤ c
⊢ a ∣ c * b

pp: case refine_2.inr.inr.inr.hz
a : Cardinal.{u}
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this : ∀ {a : Cardinal.{u}}, ℵ₀ ≤ a → ∀ (b c : Cardinal.{u}), a ∣ b * c → b * c ≠ 0 → c ≤ b → a ∣ b ∨ a ∣ c
h : ¬c ≤ b
h✝ : b ≤ c
⊢ c * b ≠ 0

Tactic:
all_goals rwa [mul_comm]

Goal state after:
Module: Mathlib.FieldTheory.FinTrdeg

Goal state before:
pp: case mp
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E : IntermediateField K L
fg : E.FG
alg : Algebra.IsAlgebraic (↥E) L
⊢ Algebra.trdeg K ↥E < Cardinal.aleph0

Tactic:
← essFiniteType_iff,

Goal state after:
case mp
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E : IntermediateField K L
fg : Algebra.EssFiniteType K ↥E
alg : Algebra.IsAlgebraic (↥E) L
⊢ Algebra.trdeg K ↥E < Cardinal.aleph0
Module: Mathlib.FieldTheory.Differential.Basic

Goal state before:
pp: R : Type u_1
inst✝⁹ : Field R
inst✝⁸ : Differential R
a✝ b : R
F : Type u_2
inst✝⁷ : Field F
inst✝⁶ : Differential F
inst✝⁵ : CharZero F
K : Type u_3
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Differential K
inst✝¹ : DifferentialAlgebra F K
B : IntermediateField F K
inst✝ : FiniteDimensional F ↥B
a : ↥B
⊢ (B.val a)′ = B.val a′

Tactic:
rw [algHom_deriv']

Goal state after:
case hf
R : Type u_1
inst✝⁹ : Field R
inst✝⁸ : Differential R
a✝ b : R
F : Type u_2
inst✝⁷ : Field F
inst✝⁶ : Differential F
inst✝⁵ : CharZero F
K : Type u_3
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Differential K
inst✝¹ : DifferentialAlgebra F K
B : IntermediateField F K
inst✝ : FiniteDimensional F ↥B
a : ↥B
⊢ Function.Injective ⇑B.val
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
h : ∀ (b : Module.Free.ChooseBasisIndex K L → K), (MvPolynomial.eval (⇑(algebraMap K L) ∘ b)) M.det = 0
x : Module.Free.ChooseBasisIndex K L → K
hx : Pi.map (fun x ↦ ⇑(algebraMap K L)) x ∈ Set.univ.pi fun x ↦ Set.range ⇑(algebraMap K L)
⊢ (MvPolynomial.eval (Pi.map (fun x ↦ ⇑(algebraMap K L)) x)) M.det =
    (MvPolynomial.eval (Pi.map (fun x ↦ ⇑(algebraMap K L)) x)) 0

Tactic:
simpa using! h x

Goal state after:
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 : ⋃ i ∈ s, g i • ↑H = Set.univ
⊢ H.FiniteIndex

Tactic:
leftCoset_cover_const_iff_surjOn

Goal state after:
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
⊢ H.FiniteIndex
Module: Mathlib.FieldTheory.Isaacs

Goal state before:
pp: case inl
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
alg : Algebra.IsAlgebraic F E
h : ∀ (x : E), ∃ y, (aeval y) (minpoly F x) = 0
S : Finset E
p : K[X] := ∏ x ∈ S, Polynomial.map (algebraMap F K) (minpoly F x)
K' : Type u_3 := p.SplittingField
splits : ∀ s ∈ S, (Polynomial.map (algebraMap F K') (minpoly F s)).Splits
K₀ : IntermediateField F K' := restrictScalars F ⊥
FS : IntermediateField F E := adjoin F ↑S
Ω : Type (max u_2 u_3) := ↥FS →ₐ[F] K'
this✝ : FiniteDimensional F ↥(adjoin F ↑S)
M : Ω → Submodule F ↥FS := fun ω ↦ Subalgebra.toSubmodule (comap ω K₀).toSubalgebra
this : ⋃ ω, ↑(M ω) = Set.univ
h✝ : Finite F
α : ↥FS
hα : F⟮α⟯ = ⊤
ω : Ω
hω : α ∈ ↑(M ω)
⊢ ∃ ω, ⊤ ≤ M ω

Tactic:
exact ⟨ω, show ⊤ ≤ K₀.comap ω by rwa [← hα, adjoin_simple_le_iff]⟩

Goal state after:
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq (Subgroup G)
n : ℕ
ih :
  ∀ m < n,
    ∀ {ι : Type u_2} {H : ι → Subgroup G} {g : ι → G} {s : Finset ι},
      ⋃ i ∈ s, g i • ↑(H i) = Set.univ →
        ∀ j ∈ s,
          ⋃ i ∈ {x ∈ s | H x = H j}, g i • ↑(H i) ≠ Set.univ →
            m = (Finset.image H s).card → ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex
ι : 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
hn : n = (Finset.image H s).card
x : G
hx : ∀ i ∈ s, H i = H j → ↑(g i) ≠ ↑x
⊢ ∀ (y : G), y • ↑(H j) ⊆ ⋃ i ∈ {x ∈ s | H x ≠ H j}, (y * x⁻¹ * g i) • ↑(H i)

Tactic:
intro y z hz

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq (Subgroup G)
n : ℕ
ih :
  ∀ m < n,
    ∀ {ι : Type u_2} {H : ι → Subgroup G} {g : ι → G} {s : Finset ι},
      ⋃ i ∈ s, g i • ↑(H i) = Set.univ →
        ∀ j ∈ s,
          ⋃ i ∈ {x ∈ s | H x = H j}, g i • ↑(H i) ≠ Set.univ →
            m = (Finset.image H s).card → ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex
ι : 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
hn : n = (Finset.image H s).card
x : G
hx : ∀ i ∈ s, H i = H j → ↑(g i) ≠ ↑x
y z : G
hz : z ∈ y • ↑(H j)
⊢ z ∈ ⋃ i ∈ {x ∈ s | H x ≠ H j}, (y * x⁻¹ * g i) • ↑(H i)
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))
h2 : lift.{max u v, v} #F ≤ Module.rank F K
⊢ max (max (lift.{u, v} #F) (lift.{v, u} #σ)) ℵ₀ ≤ Module.rank F (FractionRing (MvPolynomial σ F))

Tactic:
lift_umax.{v, u}

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.{u, v} #F ≤ 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
e : α ^ n = a
x✝ : n = 0 ∨ n > 0
⊢ (X ^ n - C a).Splits

Tactic:
cases n.eq_zero_or_pos with

Goal state after:
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
a : K
α : L
ha : α ^ finrank K L = (algebraMap K L) a
hα : K⟮α⟯ = ⊤
⊢ ∀ (q : K [X]), q.Monic → (aeval α) q = 0 → (X ^ finrank K L - C a).degree ≤ q.degree

Tactic:
intro q hq hq'
      refine le_trans ?_ (degree_le_of_dvd (minpoly.dvd _ _ hq') hq.ne_zero)
      rw [degree_X_pow_sub_C finrank_pos,
        degree_eq_natDegree (minpoly.ne_zero (IsIntegral.of_finite K α)),
        ← IntermediateField.adjoin.finrank (IsIntegral.of_finite K α), hα, Nat.cast_le]
      exact (finrank_top K L).ge

Goal state after:
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
A B : Subalgebra R S
inst✝³ : Free R ↥A
inst✝² : Free R ↥B
inst✝¹ : Module.Finite R ↥A
inst✝ : Module.Finite R ↥B
H : finrank R ↥(A ⊔ B) = finrank R ↥A * finrank R ↥B
a✝ : Nontrivial R
⊢ A.LinearDisjoint B

Tactic:
rw [← Module.finrank_tensorProduct] at H

Goal state after:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
A B : Subalgebra R S
inst✝³ : Free R ↥A
inst✝² : Free R ↥B
inst✝¹ : Module.Finite R ↥A
inst✝ : Module.Finite R ↥B
H : finrank R ↥(A ⊔ B) = finrank R (↥A ⊗[R] ↥B)
a✝ : Nontrivial R
⊢ A.LinearDisjoint B