mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: case mp
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
inst✝ : Fintype (ClassGroup R)
⊢ Fintype.card (ClassGroup R) = 1 → IsPrincipalIdealRing R

pp: case mpr
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
inst✝ : Fintype (ClassGroup R)
⊢ IsPrincipalIdealRing R → Fintype.card (ClassGroup R) = 1

Tactic:
swap

Goal state after:
case mpr
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
inst✝ : Fintype (ClassGroup R)
⊢ IsPrincipalIdealRing R → Fintype.card (ClassGroup R) = 1

case mp
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
inst✝ : Fintype (ClassGroup R)
⊢ Fintype.card (ClassGroup R) = 1 → IsPrincipalIdealRing R
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: R : Type u_1
K : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : Field K
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : IsDomain R
S : Type u_3
L : Type u_4
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
inst✝² : Field L
inst✝¹ : Algebra S L
inst✝ : IsFractionRing S L
f : R ≃+* S
⊢ Subgroup.map (Units.mapEquiv ↑(ringEquivOfRingEquiv K L f)).toMonoidHom (toPrincipalIdeal R K).range =
    (toPrincipalIdeal S L).range

Tactic:
by
  ext I
  simp only [MulEquiv.toMonoidHom_eq_coe, Subgroup.mem_map, MonoidHom.mem_range,
    toPrincipalIdeal_eq_iff, MonoidHom.coe_coe]
  refine ⟨fun ⟨u, ⟨v, huv⟩, hu⟩ ↦ ?_, fun ⟨u, hu⟩ ↦ ?_⟩
  · use Units.map (IsFractionRing.ringEquivOfRingEquiv f (K := K)
      (L := L)).toRingHom v
    rw [← hu]
    simp only [RingEquiv.toRingHom_eq_coe, Units.coe_map, MonoidHom.coe_coe, RingHom.coe_coe,
      Units.coe_mapEquiv, ← huv, RingEquiv.coe_toMulEquiv]
    rw [FractionalIdeal.ringEquivOfRingEquiv_spanSingleton]
  · use Units.mapEquiv (FractionalIdeal.ringEquivOfRingEquiv _ _ f).symm.toMulEquiv I
    refine ⟨?_, by simp [← Units.val_inj]⟩
    · use Units.map (IsFractionRing.ringEquivOfRingEquiv f (K := K)
        (L := L)).symm.toRingHom u
      simp only [IsFractionRing.ringEquivOfRingEquiv_symm, RingEquiv.toRingHom_eq_coe,
        Units.coe_map, MonoidHom.coe_coe, RingHom.coe_coe, RingEquiv.toMulEquiv_eq_coe,
        RingEquiv.coe_toMulEquiv_symm, Units.coe_mapEquiv]
      rw [← FractionalIdeal.ringEquivOfRingEquiv_spanSingleton,
        ← FractionalIdeal.ringEquivOfRingEquiv_symm_eq, hu]
      rfl

Goal state after:
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
tfae_1_to_4 : IsLocallyConstant f → ∀ (y : Y), IsOpen[inst✝] (f ⁻¹' {y})
tfae_4_to_3 : (∀ (y : Y), IsOpen[inst✝] (f ⁻¹' {y})) → ∀ (x : X), IsOpen[inst✝] {x' | f x' = f x}
tfae_3_to_2 : (∀ (x : X), IsOpen[inst✝] {x' | f x' = f x}) → ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x
tfae_2_to_5 :
  (∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x) → ∀ (x : X), ∃ U, IsOpen[inst✝] U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x
h : ∀ (x : X), ∃ U, IsOpen[inst✝] U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x
s : Set Y
x : X
hx : x ∈ f ⁻¹' s
⊢ ∃ t ⊆ f ⁻¹' s, IsOpen[inst✝] t ∧ x ∈ t

Tactic:
rcases h x with ⟨U, hU, hxU, eq⟩

Goal state after:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
tfae_1_to_4 : IsLocallyConstant f → ∀ (y : Y), IsOpen[inst✝] (f ⁻¹' {y})
tfae_4_to_3 : (∀ (y : Y), IsOpen[inst✝] (f ⁻¹' {y})) → ∀ (x : X), IsOpen[inst✝] {x' | f x' = f x}
tfae_3_to_2 : (∀ (x : X), IsOpen[inst✝] {x' | f x' = f x}) → ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x
tfae_2_to_5 :
  (∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x) → ∀ (x : X), ∃ U, IsOpen[inst✝] U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x
h : ∀ (x : X), ∃ U, IsOpen[inst✝] U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x
s : Set Y
x : X
hx : x ∈ f ⁻¹' s
U : Set X
hU : IsOpen[inst✝] U
hxU : x ∈ U
eq : ∀ x' ∈ U, f x' = f x
⊢ ∃ t ⊆ f ⁻¹' s, IsOpen[inst✝] t ∧ x ∈ t
Module: Mathlib.RingTheory.Localization.Free

Goal state before:
pp: R : Type u_4
M : Type u_5
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
S : Submonoid R
M' : Type u_1
inst✝⁹ : AddCommGroup M'
inst✝⁸ : Module R M'
f : M →ₗ[R] M'
inst✝⁷ : IsLocalizedModule S f
Rₛ : Type u_3
inst✝⁶ : CommRing Rₛ
inst✝⁵ : Algebra R Rₛ
inst✝⁴ : Module Rₛ M'
inst✝³ : IsScalarTower R Rₛ M'
inst✝² : IsLocalization S Rₛ
inst✝¹ : FinitePresentation R M
I : Type u_6
inst✝ : Finite I
b : Basis I Rₛ M'
⊢ ∃ r, ∃ (hr : r ∈ S), ∃ b', ∀ (i : I), (LocalizedModule.lift (Submonoid.powers r) f ⋯) (b' i) = b i

Tactic:
by
  have : Module.FinitePresentation R (I →₀ R) := Module.finitePresentation_of_projective _ _
  obtain ⟨r, hr, e, he⟩ := Module.FinitePresentation.exists_lift_equiv_of_isLocalizedModule S f
    (Finsupp.mapRange.linearMap (Algebra.linearMap R Rₛ)) (b.repr.restrictScalars R)
  let e' := IsLocalizedModule.iso (.powers r) (Finsupp.mapRange.linearMap (α := I)
    (Algebra.linearMap R (Localization (.powers r))))
  refine ⟨r, hr, .ofRepr (e ≪≫ₗ ?_), ?_⟩
  · exact
    { __ := e',
      toLinearMap := e'.extendScalarsOfIsLocalization (.powers r) (Localization (.powers r)) }
  · intro i
    have : e'.symm _ = _ := LinearMap.congr_fun (IsLocalizedModule.iso_symm_comp (.powers r)
      (Finsupp.mapRange.linearMap (Algebra.linearMap R (Localization (.powers r)))))
      (Finsupp.single i 1)
    simp only [Finsupp.mapRange.linearMap_apply, Finsupp.mapRange_single, Algebra.linearMap_apply,
      map_one, LocalizedModule.mkLinearMap_apply] at this
    change LocalizedModule.lift _ _ _ (e.symm (e'.symm _)) = _
    replace he := LinearMap.congr_fun he (e.symm (e'.symm (Finsupp.single i 1)))
    simp only [LinearMap.coe_comp, LinearMap.coe_restrictScalars, LinearEquiv.coe_coe,
      Function.comp_apply, LinearEquiv.apply_symm_apply, LinearEquiv.restrictScalars_apply] at he
    apply b.repr.injective
    rw [← he, Basis.repr_self, this, LocalizedModule.lift_mk]
    simp

Goal state after:
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : C(X, Y)
y : Y
h : ∀ (x : X), f x = y
x✝¹ : LocallyConstant Y Z
x✝ : X
⊢ (comap f x✝¹) x✝ = (const X (x✝¹ y)) x✝

Tactic:
simp [h]

Goal state after:
Module: Mathlib.Algebra.Module.StablyFree.FreeOfInvertible

Goal state before:
pp: case inl
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsStablyFree R M
inst✝ : Module.Invertible R M
h✝ : Subsingleton R
⊢ Free R M

Tactic:
exact Module.Free.of_subsingleton' R M

Goal state after:
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
n : ℕ
⊢ map f (derivedSeries G n) ≤ derivedSeries G' n

Tactic:
by
  induction n with
  | zero => exact le_top
  | succ n ih => simp only [derivedSeries_succ, map_commutator, commutator_mono, ih]

Goal state after:
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: case h.succ
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 ≠ ⊥
n : ℕ
ih : map H.subtype (derivedSeries (↥H) (n + 1)) = map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) n)
⊢ ⁅map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) n), map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) n)⁆ =
    map ⁅H, H⁆.subtype ⁅derivedSeries (↥⁅H, H⁆) n, derivedSeries (↥⁅H, H⁆) n⁆

Tactic:
map_commutator

Goal state after:
case h.succ
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 ≠ ⊥
n : ℕ
ih : map H.subtype (derivedSeries (↥H) (n + 1)) = map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) n)
⊢ ⁅map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) n), map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) n)⁆ =
    ⁅map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) n), map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) n)⁆
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M₁ M₂ : Matroid α
h : M₁ = M₂
⊢ M₁.E = M₂.E ∧ ∀ ⦃B : Set α⦄, B ⊆ M₁.E → (M₁.IsBase B ↔ M₂.IsBase B)

Tactic:
simp [h]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
B B' : Set α
e : α
hB : M.IsBase B
hB' : M.IsBase B'
h : B \ B' = {e}
f : α
hf : f ∈ B' \ B
hb : M.IsBase (insert f B \ {e})
hne : f ≠ e
⊢ ∃ f ∈ B' \ B, B' = insert f B \ {e}

Tactic:
refine ⟨f, hf, (hb.eq_of_subset_isBase hB' ?_).symm⟩

Goal state after:
α : Type u_1
M : Matroid α
B B' : Set α
e : α
hB : M.IsBase B
hB' : M.IsBase B'
h : B \ B' = {e}
f : α
hf : f ∈ B' \ B
hb : M.IsBase (insert f B \ {e})
hne : f ≠ e
⊢ insert f B \ {e} ⊆ B'
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
B : Set α
e f : α
hB : M.IsBase B
he : e ∈ B
hf : f ∉ B
hI : M.Indep (insert f B \ {e})
⊢ M.IsBase (insert f B \ {e})

Tactic:
have hfe : f ≠ e := ne_of_mem_of_not_mem he hf |>.symm

Goal state after:
α : Type u_1
M : Matroid α
B : Set α
e f : α
hB : M.IsBase B
he : e ∈ B
hf : f ∉ B
hI : M.Indep (insert f B \ {e})
hfe : f ≠ e
⊢ M.IsBase (insert f B \ {e})
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: case inr
F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
K : IntermediateField F E
this : FiniteDimensional F E
h✝ : Infinite F
β α : E
⊢ ∃ α_1, F⟮α_1⟯ = IntermediateField.restrictScalars F (↥F⟮α⟯)⟮β⟯

Tactic:
simp_rw [adjoin_simple_adjoin_simple, eq_comm]

Goal state after:
case inr
F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
K : IntermediateField F E
this : FiniteDimensional F E
h✝ : Infinite F
β α : E
⊢ ∃ α_1, F⟮α, β⟯ = F⟮α_1⟯
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: case mpr
R : Type u
A : Type u_4
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
I : (Submodule R A)ˣ
h : I ∈ (Units.map ↑(spanSingleton R)).range
⊢ I ∈ (unitsToPic R A).ker

Tactic:
· obtain ⟨x, rfl⟩ := h
    exact mk_eq_one_iff.mpr ⟨.symm <| (.ofInjective (LinearMap.toSpanSingleton R A x) fun _ _ eq ↦
      (faithfulSMul_iff_injective_smul_one R A).mp ‹_› <| by simpa using congr($eq * x.inv)) ≪≫ₗ
      .ofEq _ _ (by ext; simp [mem_span_singleton])⟩

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

Goal state before:
pp: α : Type u_1
E B : Set α
⊢ (freeOn E).IsBase B ↔ B = E

Tactic:
simp only [freeOn, loopyOn_ground, dual_isBase_iff', loopyOn_isBase_iff, sdiff_eq_empty,
    ← subset_antisymm_iff, eq_comm (a := E)]

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
R I X : Set α
hXR : X ⊆ R
⊢ M.IsBasis' I (X ∩ R) ∧ I ⊆ R ↔ M.IsBasis' I X

Tactic:
rw [inter_eq_self_of_subset_left hXR, and_iff_left_iff_imp]

Goal state after:
α : Type u_1
M : Matroid α
R I X : Set α
hXR : X ⊆ R
⊢ M.IsBasis' I X → I ⊆ R
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
R : Set α
h : R = M.E
⊢ M ↾ R = M

Tactic:
simp [h]

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

Goal state before:
pp: case refine_2
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
e : α
he : (e ∈ M.E ∧ e ∉ X) ∧ e ∈ B
⊢ M✶.Dep (insert e (M.E \ B ∩ (M.E \ X)))

Tactic:
dual_dep_iff_forall,

Goal state after:
case refine_2
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
e : α
he : (e ∈ M.E ∧ e ∉ X) ∧ e ∈ B
⊢ (∀ (B_1 : Set α), M.IsBase B_1 → (insert e (M.E \ B ∩ (M.E \ X)) ∩ B_1).Nonempty) ∧
    insert e (M.E \ B ∩ (M.E \ X)) ⊆ M.E
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hX : X ⊆ M.E
⊢ M.IsBasis (B ∩ X) X ↔ M✶.IsBasis (M.E \ B ∩ (M.E \ X)) (M.E \ X)

Tactic:
refine ⟨hB.compl_inter_isBasis_of_inter_isBasis, fun h ↦ ?_⟩

Goal state after:
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hX : X ⊆ M.E
h : M✶.IsBasis (M.E \ B ∩ (M.E \ X)) (M.E \ X)
⊢ M.IsBasis (B ∩ X) X
Module: Mathlib.Combinatorics.Matroid.IndepAxioms

Goal state before:
pp: α : Type u_1
Indep : Set α → Prop
M : Matroid α
h : ∀ (I : Set α), M.Indep I ↔ Indep I
⊢ ∀ (x : Set α), M.Indep x = Indep x

Tactic:
simp [h]

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

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
D₀ : Set α
hD₀ : ¬M.Indep D₀
hD₀E : D₀ ⊆ M.E
⊢ (∀ (x : Set α), M.Indep x → ¬f '' D₀ = f '' x) ∧ ∃ u ⊆ M.E, f '' u = f '' D₀

Tactic:
refine ⟨fun I hI h_eq ↦ ?_, ⟨_, hD₀E, rfl⟩⟩

Goal state after:
case mpr
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
D₀ : Set α
hD₀ : ¬M.Indep D₀
hD₀E : D₀ ⊆ M.E
I : Set α
hI : M.Indep I
h_eq : f '' D₀ = f '' I
⊢ False
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
⊢ ∀ a ⊆ M.E, ((M.map f hf).IsBase (f '' M.E \ f '' a) ∧ ∃ u ⊆ M.E, f '' u = f '' a) ↔ (M✶.map f hf).IsBase (f '' a)

Tactic:
intro B

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
B : Set α
⊢ B ⊆ M.E → (((M.map f hf).IsBase (f '' M.E \ f '' B) ∧ ∃ u ⊆ M.E, f '' u = f '' B) ↔ (M✶.map f hf).IsBase (f '' B))
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: case refine_1
α : Type u_1
M : Matroid α
C I : Set α
hC : M.IsCircuit C
h : M.IsBasis I C
⊢ ∃ e ∈ C, I = C \ {e}

Tactic:
obtain ⟨e, he⟩ := exists_of_ssubset
      (h.subset.ssubset_of_ne (by rintro rfl; exact hC.dep.not_indep h.indep))

Goal state after:
case refine_1
α : Type u_1
M : Matroid α
C I : Set α
hC : M.IsCircuit C
h : M.IsBasis I C
e : α
he : e ∈ C ∧ e ∉ I
⊢ ∃ e ∈ C, I = C \ {e}
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
K : Set α
hK : M.IsCocircuit K
he : e ∈ K
⊢ ¬M.IsCircuit {e}

Tactic:
intro he'

Goal state after:
α : Type u_1
M : Matroid α
e : α
K : Set α
hK : M.IsCocircuit K
he : e ∈ K
he' : M.IsCircuit {e}
⊢ False
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M₁ M₂ : Matroid α
h : M₁ = M₂
⊢ M₁.E = M₂.E ∧ ∀ (C : Set α), M₁.IsCircuit C ↔ M₂.IsCircuit C

Tactic:
simp [h]

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

Goal state before:
pp: α : 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ι : Nonempty ι
C' : Set α
hC'ss : C' ⊆ insert z J ∪ ⋃ i, I i
hC' : M.IsCircuit C'
hzC' : z ∈ C'
⊢ C' ⊆ J ∪ ⋃ i, I i

Tactic:
insert_eq_of_mem hzJ

Goal state after:
α : 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ι : Nonempty ι
C' : Set α
hC'ss : C' ⊆ J ∪ ⋃ i, I i
hC' : M.IsCircuit C'
hzC' : z ∈ C'
⊢ C' ⊆ J ∪ ⋃ i, I i
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : 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ι : Nonempty ι
i : ι
⊢ M.closure (I i) = M.closure (insert (x i) (I i))

Tactic:
simpa [sdiff_singleton_eq_self (hxI _)] using (hC i).closure_sdiff_singleton_eq (x i)

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

Goal state before:
pp: case inr
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hf : M.IsNonloop f
hne : e ≠ f
⊢ ((¬M.Indep {e, f} ∧ e ∈ M.E) ∧ ∀ e_1 ∈ {e, f}, M.Indep ({e, f} \ {e_1})) ↔ ¬M.Indep {e, f}

Tactic:
and_iff_left he.mem_ground,

Goal state after:
case inr
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hf : M.IsNonloop f
hne : e ≠ f
⊢ (¬M.Indep {e, f} ∧ ∀ e_1 ∈ {e, f}, M.Indep ({e, f} \ {e_1})) ↔ ¬M.Indep {e, f}
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.E) = M.closure (Y ∩ M.E)

Tactic:
← hI.isBasis_inter_ground.closure_eq_closure,

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 I = M.closure (Y ∩ M.E)
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
tfae_1_iff_2 : M.IsColoop e ↔ e ∈ M.coloops
tfae_1_iff_3 : M.IsColoop e ↔ M.IsCocircuit {e}
tfae_1_iff_4 : M.IsColoop e ↔ ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B
tfae_3_to_5 : M.IsCocircuit {e} → (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E
x✝ : (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E
B : Set α
hB : M.IsBase B
h : ∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C
heE : e ∈ M.E
heB : e ∉ B
⊢ False

Tactic:
← hB.closure_eq

Goal state after:
α : Type u_1
M : Matroid α
e : α
tfae_1_iff_2 : M.IsColoop e ↔ e ∈ M.coloops
tfae_1_iff_3 : M.IsColoop e ↔ M.IsCocircuit {e}
tfae_1_iff_4 : M.IsColoop e ↔ ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B
tfae_3_to_5 : M.IsCocircuit {e} → (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E
x✝ : (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E
B : Set α
hB : M.IsBase B
h : ∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C
heE : e ∈ M.closure B
heB : e ∉ B
⊢ False
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
he : M.IsNonloop e
⊢ M.removeLoops.IsNonloop e

Tactic:
by
  simpa

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.Finitary
⊢ ∀ ⦃B B' : Set α⦄ ⦃N : Matroid α⦄, N.Finitary → N.IsBase B → N.IsBase B' → #↑(B \ B') ≤ #↑(B' \ B)

Tactic:
intro B

Goal state after:
α : Type u
β : Type v
f : α → β
M : Matroid α
I J B✝ B' X Y : Set α
inst✝ : M.Finitary
B : Set α
⊢ ∀ ⦃B' : Set α⦄ ⦃N : Matroid α⦄, N.Finitary → N.IsBase B → N.IsBase B' → #↑(B \ B') ≤ #↑(B' \ B)
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
X Y I : Set α
hI : M.IsBasis I X
hY : I ⊆ Y
h : M.closure X = M.closure Y
hYE : Y ⊆ M.E
⊢ Y ⊆ M.closure I

Tactic:
rw [hI.closure_eq_closure, h]

Goal state after:
α : Type u_2
M : Matroid α
X Y I : Set α
hI : M.IsBasis I X
hY : I ⊆ Y
h : M.closure X = M.closure Y
hYE : Y ⊆ M.E
⊢ Y ⊆ M.closure Y
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
s : Set ι
ind : AlgebraicIndependent R fun i ↦ x ↑i
H :
  ∀ (t : Set ι),
    t.Finite → (AlgebraicIndependent R fun i ↦ x ↑i) → ∀ i ∉ s, i ∉ t → Transcendental (↥(adjoin R (x '' t))) (x i)
t : Set ι
hfin : t.Finite
a : ι
u : Set ι
ha : a ∈ t \ s
hu : u ⊆ t \ s
ha' : a ∉ u
h : AlgebraicIndependent R fun i ↦ x ↑i
⊢ AlgebraicIndependent R fun i ↦ x ↑i

Tactic:
have : a ∉ t ∩ s ∪ u := (·.elim (ha.2 ·.2) ha')

Goal state after:
ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set ι
ind : AlgebraicIndependent R fun i ↦ x ↑i
H :
  ∀ (t : Set ι),
    t.Finite → (AlgebraicIndependent R fun i ↦ x ↑i) → ∀ i ∉ s, i ∉ t → Transcendental (↥(adjoin R (x '' t))) (x i)
t : Set ι
hfin : t.Finite
a : ι
u : Set ι
ha : a ∈ t \ s
hu : u ⊆ t \ s
ha' : a ∉ u
h : AlgebraicIndependent R fun i ↦ x ↑i
this : a ∉ t ∩ s ∪ u
⊢ AlgebraicIndependent R fun i ↦ x ↑i
Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental

Goal state before:
pp: case pos
ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
ι' : Type u_4
y : ι' → A
hx : AlgebraicIndependent R x
⊢ AlgebraicIndependent R (Sum.elim y x) ↔ AlgebraicIndependent R x ∧ AlgebraicIndependent (↥(adjoin R (range x))) y

pp: case neg
ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
ι' : Type u_4
y : ι' → A
hx : ¬AlgebraicIndependent R x
⊢ AlgebraicIndependent R (Sum.elim y x) ↔ AlgebraicIndependent R x ∧ AlgebraicIndependent (↥(adjoin R (range x))) y

Tactic:
swap

Goal state after:
case neg
ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
ι' : Type u_4
y : ι' → A
hx : ¬AlgebraicIndependent R x
⊢ AlgebraicIndependent R (Sum.elim y x) ↔ AlgebraicIndependent R x ∧ AlgebraicIndependent (↥(adjoin R (range x))) y

case pos
ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
ι' : Type u_4
y : ι' → A
hx : AlgebraicIndependent R x
⊢ AlgebraicIndependent R (Sum.elim y x) ↔ AlgebraicIndependent R x ∧ AlgebraicIndependent (↥(adjoin R (range x))) y
Module: Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure

Goal state before:
pp: ι : Type u_1
R : Type u_2
A : Type u_4
x : ι → A
S : Type u_5
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✝ : NoZeroDivisors S
hx : AlgebraicIndependent R x
alg : Algebra.IsAlgebraic R S
t : Set ι
fin : t.Finite
ind : AlgebraicIndependent S fun i ↦ x ↑i
i : ι
hi : i ∉ t
Rt : Subalgebra R A := adjoin R (x '' t)
St : Subalgebra S A := adjoin S (x '' t)
x✝³ : Algebra ↥Rt ↥St := (Subalgebra.inclusion ⋯).toAlgebra
this✝³ : IsScalarTower (↥Rt) (↥St) A
this✝² : NoZeroDivisors ↥St
this✝¹ : NoZeroDivisors ↥Rt
x✝² : ↥St
y : A
hy : y ∈ St
this✝ : Nontrivial R
this : Nontrivial A
z : S
x✝¹ x✝ : R
eq : (algebraMap R ↥Rt) x✝¹ = (algebraMap R ↥Rt) x✝
⊢ x✝¹ = x✝

Tactic:
exact hx.algebraMap_injective congr($eq.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
⊢ (matroid R A).IsBasis s t ↔ s = t

Tactic:
simp_rw [Matroid.IsBasis, matroid_indep_iff, of_subsingleton, true_and,
    matroid_e, subset_univ, and_true, maximal_le_iff]

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝ : Field F
f : F[X]
hf : f ≠ 0
⊢ f.natSepDegree = f.natDegree ↔ Fintype.card ↑(f.rootSet f.SplittingField) = f.natDegree

Tactic:
rootSet_def,

Goal state after:
F : Type u
inst✝ : Field F
f : F[X]
hf : f ≠ 0
⊢ f.natSepDegree = f.natDegree ↔ Fintype.card ↑↑(f.aroots f.SplittingField).toFinset = f.natDegree
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝ : Field F
f : F[X]
hm : f.Monic
hs : f.Splits
h : f.natSepDegree = 1
h2 : f.roots.card ≠ 0
y : F
h1 : f = (f.roots.card • {X - C y}).prod
h3 : f.roots = f.roots.card • {y}
⊢ f = (X - C y) ^ f.roots.card

Tactic:
Multiset.prod_nsmul,

Goal state after:
F : Type u
inst✝ : Field F
f : F[X]
hm : f.Monic
hs : f.Splits
h : f.natSepDegree = 1
h2 : f.roots.card ≠ 0
y : F
h1 : f = {X - C y}.prod ^ f.roots.card
h3 : f.roots = f.roots.card • {y}
⊢ f = (X - C y) ^ f.roots.card
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)
inst✝ : FiniteDimensional F E
H_le : H ≤ (fixedField H).fixingSubgroup
⊢ (E →ₐ[↥(FixedPoints.subfield (↥H) E)] E) ≃ ↥(fixedField H).fixingSubgroup

Tactic:
refine (algEquivEquivAlgHom (fixedField H) E).toEquiv.symm.trans ?_

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)
inst✝ : FiniteDimensional F E
H_le : H ≤ (fixedField H).fixingSubgroup
⊢ Gal(E/↥(fixedField H)) ≃ ↥(fixedField H).fixingSubgroup