mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : WellFoundedLT (Subgroup G)
h : ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H
⊢ IsSolvable G

Tactic:
suffices h : IsSolvable (⊤ : Subgroup G) from
    isSolvable_of_surjective (MonoidHom.range_eq_top.mp (range_subtype ⊤))

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : WellFoundedLT (Subgroup G)
h : ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H
⊢ IsSolvable ↥⊤
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: case ind.inr
G : Type u_1
inst✝¹ : Group G
inst✝ : WellFoundedLT (Subgroup G)
h : ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H
H : Subgroup G
hH : ∀ y < H, IsSolvable ↥y
h' : H ≠ ⊥
⊢ IsSolvable ↥H

Tactic:
obtain ⟨n, hn⟩ := hH ⁅H, H⁆ (h H h')
    use n + 1
    rw [← map_subtype_inj, Subgroup.map_bot] at hn ⊢
    rw [← hn]
    clear hn
    induction n with
    | zero =>
      rw [derivedSeries_succ, derivedSeries_zero, derivedSeries_zero, map_commutator,
        ← MonoidHom.range_eq_map, ← MonoidHom.range_eq_map, range_subtype, range_subtype]
    | succ n ih => rw [derivedSeries_succ, map_commutator, ih, derivedSeries_succ, map_commutator]

Goal state after:
Module: Mathlib.RingTheory.LocalRing.ResidueField.Fiber

Goal state before:
pp: R✝ : Type u_1
S✝ : Type u_2
inst✝⁶ : CommRing R✝
inst✝⁵ : CommRing S✝
inst✝⁴ : Algebra R✝ S✝
p✝ : Ideal R✝
inst✝³ : p✝.IsPrime
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : PrimeSpectrum R
H : Topology.IsEmbedding ⇑(preimageOrderIsoFiber R S p).symm := preimageHomeomorphFiber._proof_1 R S p
x : ↑(comap (algebraMap R S) ⁻¹' {p})
⊢ (preimageOrderIsoFiber R S p).toFun x = (H.toHomeomorphOfSurjective ⋯).symm x

Tactic:
obtain ⟨x, rfl⟩ := (H.toHomeomorphOfSurjective
        (preimageOrderIsoFiber R S p).symm.surjective).surjective x

Goal state after:
R✝ : Type u_1
S✝ : Type u_2
inst✝⁶ : CommRing R✝
inst✝⁵ : CommRing S✝
inst✝⁴ : Algebra R✝ S✝
p✝ : Ideal R✝
inst✝³ : p✝.IsPrime
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : PrimeSpectrum R
H : Topology.IsEmbedding ⇑(preimageOrderIsoFiber R S p).symm := preimageHomeomorphFiber._proof_1 R S p
x : PrimeSpectrum (p.asIdeal.Fiber S)
⊢ (preimageOrderIsoFiber R S p).toFun ((H.toHomeomorphOfSurjective ⋯) x) =
    (H.toHomeomorphOfSurjective ⋯).symm ((H.toHomeomorphOfSurjective ⋯) x)
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Invertible R M
N : Type (max v u) := Dual R M
e : M ⊗[R] N ≃ₗ[R] R := TensorProduct.comm R M N ≪≫ₗ linearEquiv R M
S : Finset (M × N)
hS : e.symm 1 = ∑ i ∈ S, i.1 ⊗ₜ[R] i.2
f : (↥S →₀ N) →ₗ[R] R := (Finsupp.lsum R) fun i ↦ ↑e ∘ₗ (TensorProduct.mk R M N) (↑i).1
this : Function.Surjective ⇑f
g : R →ₗ[R] ↥S →₀ N
hg : f ∘ₗ g = LinearMap.id
aux : M ⊗[R] (↥S →₀ N) ≃ₗ[R] ↥S →₀ R := finsuppRight R R M N ↥S ≪≫ₗ Finsupp.mapRange.linearEquiv e
⊢ Module.Finite R M ∧ Projective R M

Tactic:
let f' : (S →₀ R) →ₗ[R] M := TensorProduct.rid R M ∘ₗ f.lTensor M ∘ₗ aux.symm

Goal state after:
R : Type u
M : Type v
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Invertible R M
N : Type (max v u) := Dual R M
e : M ⊗[R] N ≃ₗ[R] R := TensorProduct.comm R M N ≪≫ₗ linearEquiv R M
S : Finset (M × N)
hS : e.symm 1 = ∑ i ∈ S, i.1 ⊗ₜ[R] i.2
f : (↥S →₀ N) →ₗ[R] R := (Finsupp.lsum R) fun i ↦ ↑e ∘ₗ (TensorProduct.mk R M N) (↑i).1
this : Function.Surjective ⇑f
g : R →ₗ[R] ↥S →₀ N
hg : f ∘ₗ g = LinearMap.id
aux : M ⊗[R] (↥S →₀ N) ≃ₗ[R] ↥S →₀ R := finsuppRight R R M N ↥S ≪≫ₗ Finsupp.mapRange.linearEquiv e
f' : (↥S →₀ R) →ₗ[R] M := ↑(TensorProduct.rid R M) ∘ₗ LinearMap.lTensor M f ∘ₗ ↑aux.symm
⊢ Module.Finite R M ∧ Projective R M
Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus

Goal state before:
pp: R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Flat R M
inst✝ : Module.Finite R M
q : PrimeSpectrum R
S : Type uR := Localization.AtPrime q.asIdeal
P : PrimeSpectrum S
hpq : comap (algebraMap R S) P ≤ q
⊢ rankAtStalk (LocalizedModule q.asIdeal.primeCompl M) P = rankAtStalk M q

Tactic:
rankAtStalk_eq_finrank_of_free

Goal state after:
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Flat R M
inst✝ : Module.Finite R M
q : PrimeSpectrum R
S : Type uR := Localization.AtPrime q.asIdeal
P : PrimeSpectrum S
hpq : comap (algebraMap R S) P ≤ q
⊢ ↑(finrank (Localization q.asIdeal.primeCompl) (LocalizedModule q.asIdeal.primeCompl M)) P = rankAtStalk M q
Module: Mathlib.RingTheory.AlgebraicIndependent.Defs

Goal state before:
pp: R : Type u_3
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set A
⊢ IsTranscendenceBasis R Subtype.val ↔ Maximal (AlgebraicIndepOn R _root_.id) s

Tactic:
rw [IsTranscendenceBasis, maximal_iff, Subtype.range_val]; rfl

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

Goal state before:
pp: α : Type u_1
M : Matroid α
B₁ B₂ : Set α
hB₁ : M.IsBase B₁
hB₂ : M.IsBase B₂
⊢ B₁.encard = B₂.encard

Tactic:
M.isBase_exchange.encard_isBase_eq hB₁ hB₂

Goal state after:
α : Type u_1
M : Matroid α
B₁ B₂ : Set α
hB₁ : M.IsBase B₁
hB₂ : M.IsBase B₂
⊢ B₂.encard = B₂.encard
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: case inr
α : Type u_1
M : Matroid α
B : Set α
e f : α
hB : M.IsBase B
hf : f ∉ B
hI : M.Indep (insert f (B \ {e}))
B' : Set α
hB' : M.IsBase B'
hfB : f ∈ B'
h : B \ B' = {e}
hx : B' \ B = {f}
⊢ M.IsBase (insert f (B \ {e}))

Tactic:
simp_rw [← h, ← singleton_union, ← hx, _root_.sdiff_sdiff_right_self, inf_eq_inter, inter_comm B,
    sdiff_union_inter]

Goal state after:
case inr
α : Type u_1
M : Matroid α
B : Set α
e f : α
hB : M.IsBase B
hf : f ∉ B
hI : M.Indep (insert f (B \ {e}))
B' : Set α
hB' : M.IsBase B'
hfB : f ∈ B'
h : B \ B' = {e}
hx : B' \ B = {f}
⊢ M.IsBase B'
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
B I : Set α
hI : M.Indep I
hI' : ¬M.IsBase I
hB : M.IsBase B
B' : Set α
hB' : M.IsBase B'
hIB' : I ⊆ B'
⊢ I ≠ B'

Tactic:
rintro rfl; exact hI' hB'

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

Goal state before:
pp: α : Type u_1
M✝ : Matroid α
I✝ B✝ X✝ : Set α
M : Matroid α
I X : Set α
hIE : I ⊆ M.E
B : Set α
hB : M.IsBase B
hIB : Disjoint I B
hI_not_max : ¬Maximal (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) I
hX_max : Maximal (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) X
hXE : X ⊆ M.E
B' : Set α := M.E \ X
hB' : M.IsBase B'
hX : B' = M.E \ X
hI : ¬M.IsBase (M.E \ I)
B'' : Set α
hB'' : M.IsBase B''
hB''₁ : B' \ I ⊆ B''
hB''₂ : (B' \ I ∪ B)ᶜ ⊆ B''ᶜ
⊢ ∃ x ∈ X \ I, insert x I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint (insert x I) B

Tactic:
← hIB.sdiff_eq_right,

Goal state after:
α : Type u_1
M✝ : Matroid α
I✝ B✝ X✝ : Set α
M : Matroid α
I X : Set α
hIE : I ⊆ M.E
B : Set α
hB : M.IsBase B
hIB : Disjoint I B
hI_not_max : ¬Maximal (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) I
hX_max : Maximal (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) X
hXE : X ⊆ M.E
B' : Set α := M.E \ X
hB' : M.IsBase B'
hX : B' = M.E \ X
hI : ¬M.IsBase (M.E \ I)
B'' : Set α
hB'' : M.IsBase B''
hB''₁ : B' \ I ⊆ B''
hB''₂ : (B' \ I ∪ B \ I)ᶜ ⊆ B''ᶜ
⊢ ∃ x ∈ X \ I, insert x I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint (insert x I) B
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
B : Set α
⊢ Maximal M.Indep B ∧ B ⊆ M.E ↔ Maximal M.Indep B

Tactic:
and_iff_left_of_imp (fun h ↦ h.1.subset_ground)

Goal state after:
α : Type u_1
M : Matroid α
B : Set α
⊢ Maximal M.Indep B ↔ Maximal M.Indep B
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
⊢ M.IsBasis I {x | M.IsBasis I (insert x I)}

Tactic:
refine hI.isBasis_of_forall_insert (fun e he ↦ (?_ : M.IsBasis _ _))
    (fun e he ↦ ⟨fun hu ↦ he.2 ?_, he.1.subset_ground⟩)

Goal state after:
case refine_1
α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
e : α
he : e ∈ I
⊢ M.IsBasis I (insert e I)

case refine_2
α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
e : α
he : e ∈ {x | M.IsBasis I (insert x I)} \ I
hu : M.Indep (insert e I)
⊢ e ∈ I
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
I X Y : Set α
hIX : M.IsBasis I X
hIY : M.IsBasis I Y
⊢ M.IsBasis I (X ∪ Y)

Tactic:
convert! hIX.union_isBasis_union hIY _ <;> rw [union_self]

Goal state after:
α : Type u_1
M : Matroid α
I X Y : Set α
hIX : M.IsBasis I X
hIY : M.IsBasis I Y
⊢ M.Indep I
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
E : Set α
hE : E.Finite
⊢ {M | M.E ⊆ E}.Finite

Tactic:
set f : Matroid α → Set α × (Set (Set α)) := fun M ↦ ⟨M.E, {B | M.IsBase B}⟩
  have hf : f.Injective := by
    refine fun M M' hMM' ↦ ?_
    rw [Prod.mk.injEq, and_comm, Set.ext_iff, and_comm] at hMM'
    exact ext_isBase hMM'.1 (fun B _ ↦ hMM'.2 B)
  rw [← Set.finite_image_iff hf.injOn]
  refine (hE.finite_subsets.prod hE.finite_subsets.finite_subsets).subset ?_
  rintro _ ⟨M, hE : M.E ⊆ E, rfl⟩
  simp only [Set.mem_prod, Set.mem_ofPred_eq]
  exact ⟨hE, fun B hB ↦ hB.subset_ground.trans hE⟩

Goal state after:
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u_5
inst✝³ : CommRing R
inst✝² : IsFractionRing R R
I J : Ideal R
inst✝¹ : Module.Invertible R ↥I
inst✝ : Module.Invertible R ↥J
h : Pic.mk R (↥I ⊗[R] ↥J) = 1
⊢ I = ⊤ ∧ J = ⊤

Tactic:
by
  have ⟨e⟩ := mk_eq_one_iff.mp h
  have e := e.symm ≪≫ₗ Submodule.LinearDisjoint.mulMap
    (.of_left_le_one_of_flat I J <| le_top.trans one_eq_top.ge)
  have : IsUnit (e 1 : R) := IsFractionRing.self_iff_nonZeroDivisors_le_isUnit.mp ‹_› <|
      IsRegular.mem_nonZeroDivisors <| isRightRegular_iff_isRegular.mp <| by
    rw [IsRightRegular]
    convert! Subtype.val_injective.comp e.injective using 2
    rw [← smul_eq_mul, ← Submodule.coe_smul, ← map_smul, smul_eq_mul, mul_one, Function.comp_apply]
  constructor <;> refine eq_top_of_isUnit_mem _ ?_ this
  exacts [mul_le_left (e 1).2, mul_le_right (e 1).2]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
E B : Set α
h : BijOn f E N.E
⊢ (N.comapOn E f).IsBase B ∧ B ⊆ (N.comapOn E f).E ↔ N.IsBase (f '' B) ∧ B ⊆ E

Tactic:
comapOn_ground_eq,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
E B : Set α
h : BijOn f E N.E
⊢ (N.comapOn E f).IsBase B ∧ B ⊆ E ↔ N.IsBase (f '' B) ∧ B ⊆ E
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
E : Set α
h : BijOn f E N.E
B : Set α
hB : B ⊆ (N.comapOn E f)✶.E
⊢ N.IsBase (f '' ((N.comapOn E f).E \ B)) ∧ (N.comapOn E f).E \ B ⊆ E ↔ N.IsBase (N.E \ f '' B) ∧ B ⊆ E

pp: α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
E : Set α
h : BijOn f E N.E
B : Set α
hB : B ⊆ (N.comapOn E f)✶.E
⊢ f '' B ⊆ N.E

Tactic:
comapOn_ground_eq,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
E : Set α
h : BijOn f E N.E
B : Set α
hB : B ⊆ (N.comapOn E f)✶.E
⊢ N.IsBase (f '' (E \ B)) ∧ E \ B ⊆ E ↔ N.IsBase (N.E \ f '' B) ∧ B ⊆ E

α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
E : Set α
h : BijOn f E N.E
B : Set α
hB : B ⊆ (N.comapOn E f)✶.E
⊢ f '' B ⊆ N.E
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Matroid α
I X : Set α
f : α → β
hf : InjOn f M.E
hI : I ⊆ M.E
hX : X ⊆ M.E
h : (M.map f hf).IsBasis (f '' I) (f '' X)
I' : Set α
hI' : M.Indep I'
hII' : f '' I = f '' I'
⊢ M.IsBasis I X

Tactic:
rw [hf.image_eq_image_iff hI hI'.subset_ground] at hII'

Goal state after:
α : Type u_1
β : Type u_2
M : Matroid α
I X : Set α
f : α → β
hf : InjOn f M.E
hI : I ⊆ M.E
hX : X ⊆ M.E
h : (M.map f hf).IsBasis (f '' I) (f '' X)
I' : Set α
hI' : M.Indep I'
hII' : I = I'
⊢ M.IsBasis I X
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: case inl
α : Type u_1
M : Matroid α
e : α
he hf : M.IsNonloop e
⊢ M.closure {e} = M.closure {e} ↔ e = e ∨ ¬M.Indep {e, e}

pp: case inr
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hf : M.IsNonloop f
hne : e ≠ f
⊢ M.closure {e} = M.closure {f} ↔ e = f ∨ ¬M.Indep {e, f}

Tactic:
· exact iff_of_true rfl (Or.inl rfl)

Goal state after:
case inr
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hf : M.IsNonloop f
hne : e ≠ f
⊢ M.closure {e} = M.closure {f} ↔ e = f ∨ ¬M.Indep {e, f}
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
inst✝ : M.RankFinite
hX : X ⊆ M.E
⊢ M.Spanning X ↔ M.eRank ≤ M.eRk X

Tactic:
by
  rw [spanning_iff_eRk_le', and_iff_left hX]

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
M : Matroid α
Xs Ys : ι → Set α
h : ∀ (i : ι), M.closure (Xs i) = M.closure (Ys i)
⊢ M.closure (⋃ i, Xs i) = M.closure (⋃ i, Ys i)

Tactic:
simp [h, ← M.closure_iUnion_closure_eq_closure_iUnion]

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

Goal state before:
pp: α : 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
⊢ M₁.Indep I ↔ M₂.Indep I

Tactic:
rw [← sdiff_coloops_indep_iff, ← @sdiff_coloops_indep_iff _ M₂, ← hc]

Goal state after:
α : 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
⊢ M₁.Indep (I \ M₁.coloops) ↔ M₂.Indep (I \ M₁.coloops)
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: case inr
α : 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
hndj : ¬Disjoint I M₁.loops
e : α
heI : e ∈ I
hel : e ∈ M₂.loops
⊢ ¬M₂.Indep (I \ M₁.coloops)

Tactic:
← isLoop_iff

Goal state after:
case inr
α : 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
hndj : ¬Disjoint I M₁.loops
e : α
heI : e ∈ I
hel : M₂.IsLoop e
⊢ ¬M₂.Indep (I \ M₁.coloops)
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ ∀ ⦃I : Set α⦄, I ⊆ M.E → ((M.Indep I ∧ I ⊆ {e | M.IsNonloop e}) ∧ I ⊆ M.E ↔ M.Indep I)

Tactic:
exact fun I hIE ↦ ⟨ fun hI ↦ hI.1.1, fun hI ↦ ⟨⟨hI,fun e heI ↦ hI.isNonloop_of_mem heI⟩, hIE⟩⟩

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
M : Matroid α
I✝ J✝ B B' X Y✝ : Set α
inst✝ : M.InvariantCardinalRank
I J Y : Set α
hI : M.IsBasis I (Y ∩ M.E) ∧ Y ⊆ X
hJ : M.IsBasis J (Y ∩ M.E) ∧ Y ⊆ X
⊢ #↑(I \ J) = #↑(J \ I)

Tactic:
exact hI.1.cardinalMk_sdiff_comm hJ.1

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

Goal state before:
pp: α : Type u
M : Matroid α
inst✝ : M.InvariantCardinalRank
X Y Ii : Set α
hIi : M.IsBasis' Ii (X ∩ Y)
IX : Set α
hIX : M.IsBasis' IX X
hIX' : Ii ⊆ IX
IY : Set α
hIY : M.IsBasis' IY Y
hIY' : Ii ⊆ IY
⊢ #↑Ii + M.cRk (IX ∪ IY) ≤ #↑IX + #↑IY

Tactic:
← mk_union_add_mk_inter,

Goal state after:
α : Type u
M : Matroid α
inst✝ : M.InvariantCardinalRank
X Y Ii : Set α
hIi : M.IsBasis' Ii (X ∩ Y)
IX : Set α
hIX : M.IsBasis' IX X
hIX' : Ii ⊆ IX
IY : Set α
hIY : M.IsBasis' IY Y
hIY' : Ii ⊆ IY
⊢ #↑Ii + M.cRk (IX ∪ IY) ≤ #↑(IX ∪ IY) + #↑(IX ∩ IY)
Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental

Goal state before:
pp: ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
a : A
⊢ (AlgebraicIndependent R fun o ↦ o.elim a x) ↔ Transcendental (↥(adjoin R (range x))) a

Tactic:
rw [algebraicIndependent_iff_injective_aeval, transcendental_iff_injective,
    ← AlgHom.coe_toRingHom, ← hx.aeval_comp_mvPolynomialOptionEquivPolynomialAdjoin,
    RingHom.coe_comp]
  exact Injective.of_comp_iff' (Polynomial.aeval a)
    (mvPolynomialOptionEquivPolynomialAdjoin hx).bijective

Goal state after:
Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental

Goal state before:
pp: case e'_2
ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set ι
i : ι
h : i ∉ s
⊢ Transcendental (↥(adjoin R (x '' s))) (x i) ↔ Transcendental (↥(adjoin R (range fun i ↦ x ↑i))) (x i)

Tactic:
Set.image_eq_range

Goal state after:
case e'_2
ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set ι
i : ι
h : i ∉ s
⊢ Transcendental (↥(adjoin R (range fun x_1 ↦ x ↑x_1))) (x i) ↔ Transcendental (↥(adjoin R (range fun i ↦ x ↑i))) (x i)
Module: Mathlib.RingTheory.Polynomial.SeparableDegree

Goal state before:
pp: case h
F : Type u_1
inst✝ : CommSemiring F
q : ℕ
g : F[X]
m : ℕ
hf : IsSeparableContraction q ((expand F (q ^ m)) g) g
⊢ g.natDegree * q ^ m = ((expand F (q ^ m)) g).natDegree

Tactic:
natDegree_expand

Goal state after:
case h
F : Type u_1
inst✝ : CommSemiring F
q : ℕ
g : F[X]
m : ℕ
hf : IsSeparableContraction q ((expand F (q ^ m)) g) g
⊢ g.natDegree * q ^ m = g.natDegree * q ^ m
Module: Mathlib.RingTheory.AlgebraicIndependent.Basic

Goal state before:
pp: case refine_1
R : Type u_2
A : Type v
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s t : Set A
hst : s ⊆ t
hs : AlgebraicIndepOn R _root_.id s
c : Set (Set A)
hc : c ⊆ {u | AlgebraicIndependent R Subtype.val ∧ u ⊆ t}
chainc : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
hcn : c.Nonempty
⊢ AlgebraicIndependent R Subtype.val

Tactic:
exact algebraicIndependent_sUnion_of_directed hcn chainc.directedOn (fun x hxc ↦ (hc hxc).1)

Goal state after:
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : Subsingleton A
s t : Set A
this : Subsingleton R
⊢ Maximal (fun A_1 ↦ A_1 ⊆ t) s ↔ s = t

Tactic:
maximal_le_iff

Goal state after:
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: case pos
R : Type u_1
A : Type w
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
s : Set A
inst✝ : NoZeroDivisors A
alg : Algebra.IsAlgebraic (↥(adjoin R s)) A
h : Injective ⇑(algebraMap R A)
⊢ trdeg R A ≤ #↑s

Tactic:
have := isDomain_of_adjoin_range R s

Goal state after:
case pos
R : Type u_1
A : Type w
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
s : Set A
inst✝ : NoZeroDivisors A
alg : Algebra.IsAlgebraic (↥(adjoin R s)) A
h : Injective ⇑(algebraMap R A)
this : IsDomain A
⊢ trdeg R A ≤ #↑s
Module: Mathlib.FieldTheory.SeparableDegree

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✝
H : Algebra.Transcendental F E
ι : Type v
x : ι → E
hx : IsTranscendenceBasis F x
this : Algebra.IsAlgebraic (↥(adjoin F (Set.range x))) E
i : ι
K : Type (max u v) := FractionRing (MvPolynomial ι F)
i1 : MvPolynomial ι F →ₐ[F] AlgebraicClosure K := IsScalarTower.toAlgHom F (MvPolynomial ι F) (AlgebraicClosure K)
hi1 : Function.Injective ⇑i1
n : ℕ
⊢ Function.Injective ⇑↑(MvPolynomial.aeval fun i ↦ MvPolynomial.X i ^ (n + 1))

Tactic:
by
      simpa [algebraicIndependent_iff_injective_aeval] using
        MvPolynomial.algebraicIndependent_polynomial_aeval_X _
          fun i : ι ↦ (Polynomial.transcendental_X F).pow n.succ_pos

Goal state after:
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: R✝ : Type u
inst✝¹ : Ring R✝
B✝ : RingFilterBasis R✝
R : Type u
inst✝ : Ring R
B : RingFilterBasis R
B' : AddGroupFilterBasis R := B.toAddGroupFilterBasis
this✝ : TopologicalSpace R := B'.topology
basis : (𝓝 0).HasBasis (fun V ↦ V ∈ B') id
basis' : (𝓝 0 ×ˢ 𝓝 0).HasBasis (fun i ↦ i.1 ∈ B' ∧ i.2 ∈ B') fun i ↦ id i.1 ×ˢ id i.2
this : IsTopologicalAddGroup R
⊢ IsTopologicalRing R

Tactic:
apply IsTopologicalRing.of_addGroup_of_nhds_zero

Goal state after:
case hmul
R✝ : Type u
inst✝¹ : Ring R✝
B✝ : RingFilterBasis R✝
R : Type u
inst✝ : Ring R
B : RingFilterBasis R
B' : AddGroupFilterBasis R := ⋯
this✝ : TopologicalSpace R := ⋯
basis : (𝓝 0).HasBasis (fun V ↦ V ∈ B') id
basis' : (𝓝 0 ×ˢ 𝓝 0).HasBasis (fun i ↦ i.1 ∈ B' ∧ i.2 ∈ B') fun i ↦ id i.1 ×ˢ id i.2
this : IsTopologicalAddGroup R
⊢ Tendsto (uncurry fun x1 x2 ↦ x1 * x2) (𝓝 0 ×ˢ 𝓝 0) (𝓝 0)

case hmul_left
R✝ : Type u
inst✝¹ : Ring R✝
B✝ : RingFilterBasis R✝
R : Type u
inst✝ : Ring R
B : RingFilterBasis R
B' : AddGroupFilterBasis R := ⋯
this✝ : TopologicalSpace R := ⋯
basis : (𝓝 0).HasBasis (fun V ↦ V ∈ B') id
basis' : (𝓝 0 ×ˢ 𝓝 0).HasBasis (fun i ↦ i.1 ∈ B' ∧ i.2 ∈ B') fun i ↦ id i.1 ×ˢ id i.2
this : IsTopologicalAddGroup R
⊢ ∀ (x₀ : R), Tendsto (fun x ↦ x₀ * x) (𝓝 0) (𝓝 0)

case hmul_right
R✝ : Type u
inst✝¹ : Ring R✝
B✝ : RingFilterBasis R✝
R : Type u
inst✝ : Ring R
B : RingFilterBasis R
B' : AddGroupFilterBasis R := ⋯
this✝ : TopologicalSpace R := ⋯
basis : (𝓝 0).HasBasis (fun V ↦ V ∈ B') id
basis' : (𝓝 0 ×ˢ 𝓝 0).HasBasis (fun i ↦ i.1 ∈ B' ∧ i.2 ∈ B') fun i ↦ id i.1 ×ˢ id i.2
this : IsTopologicalAddGroup R
⊢ ∀ (x₀ : R), Tendsto (fun x ↦ x * x₀) (𝓝 0) (𝓝 0)
Module: Mathlib.FieldTheory.SeparableClosure

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
h : separableClosure E K = ⊥
⊢ IntermediateField.map (IsScalarTower.toAlgHom F E K) (separableClosure F E) = separableClosure F K

Tactic:
by
  refine le_antisymm (map_le_of_algHom _) (fun x hx ↦ ?_)
  obtain ⟨y, rfl⟩ := mem_bot.1 <| h ▸ mem_separableClosure_iff.2
    (IsSeparable.tower_top E <| mem_separableClosure_iff.1 hx)
  exact ⟨y, (map_mem_separableClosure_iff <| IsScalarTower.toAlgHom F E K).mp hx, rfl⟩

Goal state after:
Module: Mathlib.FieldTheory.SeparableClosure

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
ι : Type u_1
t : ι → IntermediateField F E
h : ∀ (i : ι), Algebra.IsSeparable F ↥(t i)
⊢ Algebra.IsSeparable F ↥(⨆ i, t i)

Tactic:
by
  simp_rw [← le_separableClosure_iff] at h ⊢
  exact iSup_le h

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

Goal state before:
pp: F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
H : Subgroup Gal(E/F)
K✝ : IntermediateField F E
inst✝¹ : FiniteDimensional F E
inst✝ : IsGalois F E
K L : IntermediateField F E
⊢ { toFun := ⇑OrderDual.toDual ∘ IntermediateField.fixingSubgroup, invFun := fixedField ∘ ⇑OrderDual.ofDual,
          left_inv := ⋯, right_inv := ⋯ }
        K ≤
      { toFun := ⇑OrderDual.toDual ∘ IntermediateField.fixingSubgroup, invFun := fixedField ∘ ⇑OrderDual.ofDual,
          left_inv := ⋯, right_inv := ⋯ }
        L ↔
    K ≤ L

Tactic:
rw [← fixedField_fixingSubgroup L, IntermediateField.le_iff_le, fixedField_fixingSubgroup L]

Goal state after:
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
H : Subgroup Gal(E/F)
K✝ : IntermediateField F E
inst✝¹ : FiniteDimensional F E
inst✝ : IsGalois F E
K L : IntermediateField F E
⊢ { toFun := ⇑OrderDual.toDual ∘ IntermediateField.fixingSubgroup, invFun := fixedField ∘ ⇑OrderDual.ofDual,
          left_inv := ⋯, right_inv := ⋯ }
        K ≤
      { toFun := ⇑OrderDual.toDual ∘ IntermediateField.fixingSubgroup, invFun := fixedField ∘ ⇑OrderDual.ofDual,
          left_inv := ⋯, right_inv := ⋯ }
        L ↔
    L.fixingSubgroup ≤ K.fixingSubgroup
Module: Mathlib.FieldTheory.Galois.Basic

Goal state before:
pp: case adjoin_rootSet'
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : FiniteDimensional F E
inst✝ : IsGalois F E
α : E
h1 : F⟮α⟯ = ⊤
⊢ {α} ⊆ (minpoly F α).rootSet E

Tactic:
Set.singleton_subset_iff,

Goal state after:
case adjoin_rootSet'
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : FiniteDimensional F E
inst✝ : IsGalois F E
α : E
h1 : F⟮α⟯ = ⊤
⊢ α ∈ (minpoly F α).rootSet E