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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsGCDMonoid R
J : Ideal R
this : NormalizedGCDMonoid R := Classical.arbitrary (NormalizedGCDMonoid R)
K : Ideal R
hJK0 : J * K ≠ 0
hK : Submodule.IsPrincipal (J * K)
x : R
hJK : J * K = R ∙ x
hxmemJK : x ∈ J * K
S T : Finset R
hSJ : ↑S ⊆ ↑J
hTK : ↑T ⊆ ↑K
hx : x ∈ Submodule.span R (↑S * ↑T)
⊢ x ∈ J * span ↑T

Tactic:
← J.span_eq,

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsGCDMonoid R
J : Ideal R
this : NormalizedGCDMonoid R := Classical.arbitrary (NormalizedGCDMonoid R)
K : Ideal R
hJK0 : J * K ≠ 0
hK : Submodule.IsPrincipal (J * K)
x : R
hJK : J * K = R ∙ x
hxmemJK : x ∈ J * K
S T : Finset R
hSJ : ↑S ⊆ ↑J
hTK : ↑T ⊆ ↑K
hx : x ∈ Submodule.span R (↑S * ↑T)
⊢ x ∈ span ↑J * span ↑T
Module: Mathlib.RingTheory.Spectrum.Prime.TensorProduct

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing T
inst✝ : Algebra R T
hRT : (algebraMap R T).SurjectiveOnStalks
g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom
f : S ⊗[R] T
J : PrimeSpectrum (S ⊗[R] T)
hJ : f ∉ J.asIdeal
t : T
r : R
a : S
ht : r • t ∉ Ideal.comap g J.asIdeal
e : 1 ⊗ₜ[R] (r • t) * f = a ⊗ₜ[R] t
⊢ J ∈ tensorProductTo R S T ⁻¹' (basicOpen a).carrier ×ˢ (basicOpen t).carrier

Tactic:
have : a ⊗ₜ[R] (1 : T) * (1 : S) ⊗ₜ[R] t ∉ J.asIdeal := by
      rw [Algebra.TensorProduct.tmul_mul_tmul, mul_one, one_mul, ← e]
      exact J.asIdeal.primeCompl.mul_mem ht hJ

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing T
inst✝ : Algebra R T
hRT : (algebraMap R T).SurjectiveOnStalks
g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom
f : S ⊗[R] T
J : PrimeSpectrum (S ⊗[R] T)
hJ : f ∉ J.asIdeal
t : T
r : R
a : S
ht : r • t ∉ Ideal.comap g J.asIdeal
e : 1 ⊗ₜ[R] (r • t) * f = a ⊗ₜ[R] t
this : a ⊗ₜ[R] 1 * 1 ⊗ₜ[R] t ∉ J.asIdeal
⊢ J ∈ tensorProductTo R S T ⁻¹' (basicOpen a).carrier ×ˢ (basicOpen t).carrier
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: case refine_2.refine_1
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : ↥(Ideal R)⁰
x y : R
hy : y ≠ 0
h : Ideal.span {x} * ↑I = Ideal.span {y} * ↑J
hy' : y ∈ R⁰
hx : mk' (FractionRing R) x ⟨y, hy'⟩ = 0
⊢ x = 0

Tactic:
mk'_eq_iff_eq_mul,

Goal state after:
case refine_2.refine_1
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : ↥(Ideal R)⁰
x y : R
hy : y ≠ 0
h : Ideal.span {x} * ↑I = Ideal.span {y} * ↑J
hy' : y ∈ R⁰
hx : (algebraMap R (FractionRing R)) x = 0 * (algebraMap R (FractionRing R)) ↑⟨y, hy'⟩
⊢ x = 0
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
inst✝ : IsPrincipalIdealRing R
⊢ ∀ (x : ClassGroup R), x ∈ {1}

Tactic:
refine ClassGroup.induction (R := R) (FractionRing R) (fun I => ?_)
    rw [Finset.mem_singleton]
    exact ClassGroup.mk_eq_one_iff.mpr (I : FractionalIdeal R⁰ (FractionRing R)).isPrincipal

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
hf : IsLocallyConstant f
s : Set X
hs : IsPreconnected s
x y : X
hx : x ∈ s
hy : y ∈ s
⊢ f x = f y

Tactic:
by
  let U := f ⁻¹' {f y}
  suffices x ∉ Uᶜ from Classical.not_not.1 this
  intro hxV
  specialize hs U Uᶜ (hf {f y}) (hf {f y}ᶜ) _ ⟨y, ⟨hy, rfl⟩⟩ ⟨x, ⟨hx, hxV⟩⟩
  · simp only [union_compl_self, subset_univ]
  · simp only [inter_empty, Set.not_nonempty_empty, inter_compl_self] at hs

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.subtype (derivedSeries (↥H) (n + 1)), map H.subtype (derivedSeries (↥H) (n + 1))⁆ =
    map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) (n + 1))

Tactic:
ih,

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 + 1))
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: case succ
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSimpleGroup G
n : ℕ
ih : derivedSeries G n.succ = _root_.commutator G
⊢ ⁅derivedSeries G (n + 1), derivedSeries G (n + 1)⁆ = _root_.commutator G

Tactic:
ih,

Goal state after:
case succ
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSimpleGroup G
n : ℕ
ih : derivedSeries G n.succ = _root_.commutator G
⊢ ⁅_root_.commutator G, _root_.commutator G⁆ = _root_.commutator G
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Finite E
α : Eˣ
hα : ∀ (x : Eˣ), x ∈ Subgroup.zpowers α
x : E
hx : ¬x = 0
n : ℤ
hn : α ^ n = Units.mk0 x hx
⊢ x = ↑(α ^ n)

Tactic:
rw [hn, Units.val_mk0]

Goal state after:
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: F : Type u_1
inst✝² : Field F
inst✝¹ : Infinite F
E : Type u_2
inst✝ : Field E
ϕ : F →+* E
α β : E
f g : F[X]
sf : Multiset E := (Polynomial.map ϕ f).roots
sg : Multiset E := (Polynomial.map ϕ g).roots
s : Finset E := (sf.bind fun α' ↦ Multiset.map (fun β' ↦ -(α' - α) / (β' - β)) sg).toFinset
s' : Finset F := s.preimage ⇑ϕ ⋯
c : F
hc : ¬∃ a ∈ sf, ∃ a_1 ∈ sg, -(a - α) / (a_1 - β) = ϕ c
⊢ ∃ c, ∀ α' ∈ (Polynomial.map ϕ f).roots, ∀ β' ∈ (Polynomial.map ϕ g).roots, -(α' - α) / (β' - β) ≠ ϕ c

Tactic:
push Not at hc

Goal state after:
F : Type u_1
inst✝² : Field F
inst✝¹ : Infinite F
E : Type u_2
inst✝ : Field E
ϕ : F →+* E
α β : E
f g : F[X]
sf : Multiset E := (Polynomial.map ϕ f).roots
sg : Multiset E := (Polynomial.map ϕ g).roots
s : Finset E := (sf.bind fun α' ↦ Multiset.map (fun β' ↦ -(α' - α) / (β' - β)) sg).toFinset
s' : Finset F := s.preimage ⇑ϕ ⋯
c : F
hc : ∀ a ∈ sf, ∀ a_1 ∈ sg, -(a - α) / (a_1 - β) ≠ ϕ c
⊢ ∃ c, ∀ α' ∈ (Polynomial.map ϕ f).roots, ∀ β' ∈ (Polynomial.map ϕ g).roots, -(α' - α) / (β' - β) ≠ ϕ c
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
M✝ : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
A : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M✝
inst✝⁹ : AddCommMonoid N
inst✝⁸ : AddCommMonoid P
inst✝⁷ : AddCommMonoid Q
inst✝⁶ : Module R M✝
inst✝⁵ : Module R N
inst✝⁴ : Module R P
inst✝³ : Module R Q
inst✝² : Module.Invertible R M✝
inst✝¹ : Module.Invertible R N
inst✝ : IsLocalRing R
M : Type u
x✝² : AddCommMonoid M
x✝¹ : Module R M
x✝ : Module.Invertible R M
S : Finset (Dual R M × M)
hS : (Invertible.linearEquiv R M).symm 1 = ∑ i ∈ S, i.1 ⊗ₜ[R] i.2
⊢ Free R M

Tactic:
replace hS : 1 = ∑ i ∈ S, i.1 i.2 := by
    simpa [LinearEquiv.symm_apply_eq, Invertible.linearEquiv] using hS

Goal state after:
R : Type u
M✝ : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
A : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M✝
inst✝⁹ : AddCommMonoid N
inst✝⁸ : AddCommMonoid P
inst✝⁷ : AddCommMonoid Q
inst✝⁶ : Module R M✝
inst✝⁵ : Module R N
inst✝⁴ : Module R P
inst✝³ : Module R Q
inst✝² : Module.Invertible R M✝
inst✝¹ : Module.Invertible R N
inst✝ : IsLocalRing R
M : Type u
x✝² : AddCommMonoid M
x✝¹ : Module R M
x✝ : Module.Invertible R M
S : Finset (Dual R M × M)
hS : 1 = ∑ i ∈ S, i.1 i.2
⊢ Free R M
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:
IsTranscendenceBasis,

Goal state after:
R : Type u_3
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set A
⊢ (AlgebraicIndependent R Subtype.val ∧
      ∀ (s_1 : Set A), AlgebraicIndepOn R _root_.id s_1 → range Subtype.val ⊆ s_1 → range Subtype.val = s_1) ↔
    Maximal (AlgebraicIndepOn R _root_.id) s
Module: Mathlib.RingTheory.AlgebraicIndependent.Defs

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
e : ι ≃ ι'
f : ι' → A
⊢ IsTranscendenceBasis R (f ∘ ⇑e) ↔ IsTranscendenceBasis R f

Tactic:
IsTranscendenceBasis,

Goal state after:
ι : Type u_1
ι' : Type u_2
R : Type u_3
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
e : ι ≃ ι'
f : ι' → A
⊢ (AlgebraicIndependent R (f ∘ ⇑e) ∧
      ∀ (s : Set A), AlgebraicIndepOn R _root_.id s → range (f ∘ ⇑e) ⊆ s → range (f ∘ ⇑e) = s) ↔
    AlgebraicIndependent R f ∧ ∀ (s : Set A), AlgebraicIndepOn R _root_.id s → range f ⊆ s → range f = s
Module: Mathlib.FieldTheory.Normal.Basic

Goal state before:
pp: case refine_2
F : Type u_1
K : Type u_2
inst✝² : Field F
inst✝¹ : Field K
inst✝ : Algebra F K
ι : Type u_3
t : ι → IntermediateField F K
h : ∀ (i : ι), Normal F ↥(t i)
x : ↥(⨆ i, t i)
s : Finset ((i : ι) × ↥(t i))
hx : ↑x ∈ ⨆ i ∈ s, adjoin F ((minpoly F i.snd).rootSet K)
E : IntermediateField F K := ⨆ i ∈ s, adjoin F ((minpoly F i.snd).rootSet K)
i : (i : ι) × ↥(t i)
x✝ : i ∈ s
⊢ (Polynomial.map (algebraMap F K) (minpoly F i.snd)).Splits

Tactic:
· simpa [Polynomial.map_map] using! ((h i.1).splits i.2).map (algebraMap (t i.1) K)

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

Goal state before:
pp: α : Type u_1
M : Matroid α
B : Set α
hB : B ⊆ M.E
⊢ M.IsBase (M.E \ B) ↔ Maximal (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) B

Tactic:
by
  simp_rw [maximal_iff, and_iff_right hB, and_imp, forall_exists_index]
  refine ⟨fun h ↦ ⟨⟨_, h, disjoint_sdiff_right⟩,
    fun I hI B' ⟨hB', hIB'⟩ hBI ↦ hBI.antisymm ?_⟩, fun ⟨⟨B', hB', hBB'⟩,h⟩ ↦ ?_⟩
  · rw [hB'.eq_of_subset_isBase h, ← subset_compl_iff_disjoint_right, sdiff_eq, compl_inter,
      compl_compl] at hIB'
    · exact fun e he ↦ (hIB' he).elim (fun h' ↦ (h' (hI he)).elim) id
    rw [subset_sdiff, and_iff_right hB'.subset_ground, disjoint_comm]
    exact disjoint_of_subset_left hBI hIB'
  rw [h sdiff_subset B' ⟨hB', disjoint_sdiff_left⟩]
  · simpa [hB'.subset_ground]
  simp [subset_sdiff, hB, hBB']

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

Goal state before:
pp: α : Type u_1
M : Matroid α
B : Set α
e : α
hB : M.IsBase B
h : e ∈ M.E \ B
⊢ M.Dep (insert e B)

Tactic:
by
  rw [← not_indep_iff (insert_subset h.1 hB.subset_ground)]
  exact h.2 ∘ (fun hi ↦ insert_eq_self.mp (hB.eq_of_subset_indep hi (subset_insert e B)).symm)

Goal state after:
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
this : FiniteDimensional F E
α : E
hprim : F⟮α⟯ = ⊤
f : F[X] := minpoly F α
G : Type (max 0 u_2) := { g // g.Monic ∧ g ∣ Polynomial.map (algebraMap F E) f }
hfin : Finite G
g : IntermediateField F E → G := fun K ↦ ⟨Polynomial.map (algebraMap (↥K) E) (minpoly (↥K) α), ⋯⟩
K K' : IntermediateField F E
heq : g K = g K'
⊢ K = K'

Tactic:
Subtype.mk.injEq

Goal state after:
F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
this : FiniteDimensional F E
α : E
hprim : F⟮α⟯ = ⊤
f : F[X] := minpoly F α
G : Type (max 0 u_2) := { g // g.Monic ∧ g ∣ Polynomial.map (algebraMap F E) f }
hfin : Finite G
g : IntermediateField F E → G := fun K ↦ ⟨Polynomial.map (algebraMap (↥K) E) (minpoly (↥K) α), ⋯⟩
K K' : IntermediateField F E
heq : Polynomial.map (algebraMap (↥K) E) (minpoly (↥K) α) = Polynomial.map (algebraMap (↥K') E) (minpoly (↥K') α)
⊢ K = K'
Module: Mathlib.Combinatorics.Matroid.Map

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

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

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
N : Matroid α
hI : M.Indep I
hNM : N ≤r M
hIN : I ⊆ N.E
⊢ N.Indep I

Tactic:
obtain ⟨R, -, rfl⟩ := hNM; simpa [hI]

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

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

Tactic:
rw [dual_isBase_iff, sdiff_sdiff_cancel_left hB]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
B : Set α
⊢ (N.comap f).IsBasis B (N.comap f).E ↔ N.IsBasis (f '' B) (f '' f ⁻¹' N.E) ∧ InjOn f B ∧ B ⊆ f ⁻¹' N.E

Tactic:
comap_isBasis_iff

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
B : Set α
⊢ N.IsBasis (f '' B) (f '' (N.comap f).E) ∧ InjOn f B ∧ B ⊆ (N.comap f).E ↔
    N.IsBasis (f '' B) (f '' f ⁻¹' N.E) ∧ InjOn f B ∧ B ⊆ f ⁻¹' N.E
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
I X J : Set α
hI : M.Indep I
hIX : I ⊆ X
hI' : ¬M.IsBasis I X
hJ : M.IsBasis J X
⊢ ∃ e ∈ J \ I, M.Indep (insert e I)

Tactic:
by
  rw [← isBase_restrict_iff] at hI'; rw [← isBase_restrict_iff] at hJ
  obtain ⟨e, he, hi⟩ := (hI.indep_restrict_of_subset hIX).exists_insert_of_not_isBase hI' hJ
  exact ⟨e, he, (restrict_indep_iff.mp hi).1⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Matroid α
f : ↑M.E ↪ β
I : Set ↑M.E
hI : M.Indep (Subtype.val '' ⇑f ⁻¹' ⇑f '' I)
⊢ M.Indep (Subtype.val '' I)

Tactic:
by rwa [preimage_image_eq _ f.injective] at hI

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

Goal state before:
pp: case refine_2
α : Type u_1
M : Matroid α
C : Set α
hC : M.IsCircuit C
e : α
he : e ∈ C
⊢ M.IsBasis (C \ {e}) C

Tactic:
exact hC.sdiff_singleton_isBasis he

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
e : α
he : e ∈ M.closure I
⊢ {e} ⊆ M.E

Tactic:
simpa using mem_ground_of_mem_closure he

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

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

Tactic:
rwa [eq_comm, image_preimage_eq_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
B : Set β
x✝ : M.IsBase (⇑f ⁻¹' B) ∧ B ⊆ range ⇑f
h : M.IsBase (⇑f ⁻¹' B)
h' : B ⊆ range ⇑f
⊢ B = ⇑f '' ⇑f ⁻¹' B

Tactic:
rwa [eq_comm, image_preimage_eq_iff]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
tfae_1_iff_2 : M.IsLoop e ↔ e ∈ M.closure ∅
tfae_2_iff_3 : e ∈ M.closure ∅ ↔ M.IsCircuit {e}
tfae_2_iff_4 : e ∈ M.closure ∅ ↔ M.Dep {e}
h : (∀ (x : Set α), M.IsBase x → e ∈ M.E) ∧ ∀ (x : Set α), M.IsBase x → e ∉ x
hi : M.Indep {e}
⊢ False

Tactic:
obtain ⟨B, hB, heB⟩ := hi.exists_isBase_superset

Goal state after:
α : Type u_1
M : Matroid α
e : α
tfae_1_iff_2 : M.IsLoop e ↔ e ∈ M.closure ∅
tfae_2_iff_3 : e ∈ M.closure ∅ ↔ M.IsCircuit {e}
tfae_2_iff_4 : e ∈ M.closure ∅ ↔ M.Dep {e}
h : (∀ (x : Set α), M.IsBase x → e ∈ M.E) ∧ ∀ (x : Set α), M.IsBase x → e ∉ x
hi : M.Indep {e}
B : Set α
hB : M.IsBase B
heB : {e} ⊆ B
⊢ False
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
⊢ e ∈ M.E ∧ e ∉ M.loops ↔ e ∈ M.E \ M.loops

Tactic:
mem_sdiff

Goal state after:
α : Type u_1
M : Matroid α
e : α
⊢ e ∈ M.E ∧ e ∉ M.loops ↔ e ∈ M.E ∧ e ∉ M.loops
Module: Mathlib.Combinatorics.Matroid.Loop

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

Tactic:
by
  obtain (rfl | hne) := eq_or_ne e f
  · exact iff_of_true rfl (Or.inl rfl)
  simp_rw [he.closure_eq_closure_iff_isCircuit_of_ne hne, or_iff_right hne,
    isCircuit_iff_dep_forall_sdiff_singleton_indep, dep_iff, insert_subset_iff,
    singleton_subset_iff, and_iff_left hf.mem_ground, and_iff_left he.mem_ground,
    and_iff_left_iff_imp]
  rintro hi x (rfl | rfl)
  · rwa [pair_sdiff_left hne, indep_singleton]
  rwa [pair_sdiff_right hne, indep_singleton]

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

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

Tactic:
rw [← isBasis_ground_iff, isBasis_iff_indep_subset_closure, and_congr_right_iff]

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

Goal state before:
pp: α : Type u_2
M : Matroid α
I : Set α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ i ∈ Js, e ∈ M.closure i
he' : e ∉ M.closure (⋂₀ Js)
heI : e ∈ I
X : Set α
hX' : X ∈ Js
⊢ e ∈ X

Tactic:
← hI.closure_inter_eq_self_of_subset (hIs X hX')

Goal state after:
α : Type u_2
M : Matroid α
I : Set α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ i ∈ Js, e ∈ M.closure i
he' : e ∉ M.closure (⋂₀ Js)
heI : e ∈ I
X : Set α
hX' : X ∈ Js
⊢ e ∈ M.closure X ∩ I
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
i : ι
this : AlgebraicIndependent R (x ∘ ![i])
⊢ AlgebraicIndependent R ![x i]

Tactic:
rwa [← FinVec.map_eq] at this

Goal state after:
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
ι' : Type u_4
y : ι' → A
⊢ AlgebraicIndependent R (Sum.elim y x) ↔ AlgebraicIndependent R x ∧ AlgebraicIndependent (↥(adjoin R (range x))) y

Tactic:
by
  by_cases hx : AlgebraicIndependent R x; swap
  · exact ⟨fun h ↦ (hx <| by apply h.comp _ Sum.inr_injective).elim, fun h ↦ (hx h.1).elim⟩
  let e := (sumAlgEquiv R ι' ι).trans (mapAlgEquiv _ hx.aevalEquiv)
  have : aeval (Sum.elim y x) = ((aeval y).restrictScalars R).comp e.toAlgHom := by
    ext (_ | _) <;> simp [e]
  simp_rw [hx, AlgebraicIndependent, this]; simp

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

Goal state before:
pp: α : Type u_2
M : Matroid α
X R I : Set α
hI : (M ↾ R).IsBasis' I X
hI' : M.IsBasis' I (X ∩ R)
hIR : I ⊆ R
e : α
⊢ e ∈ R ∧ (M.Indep (insert e I) ∧ insert e I ⊆ R → e ∈ I) ↔
    (e ∈ M.E ∧ (M.Indep (insert e I) → e ∈ I)) ∧ e ∈ R ∨ e ∈ R \ M.E

Tactic:
mem_sdiff

Goal state after:
α : Type u_2
M : Matroid α
X R I : Set α
hI : (M ↾ R).IsBasis' I X
hI' : M.IsBasis' I (X ∩ R)
hIR : I ⊆ R
e : α
⊢ e ∈ R ∧ (M.Indep (insert e I) ∧ insert e I ⊆ R → e ∈ I) ↔
    (e ∈ M.E ∧ (M.Indep (insert e I) → e ∈ I)) ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
h : M = loopyOn M.E
⊢ M.closure ∅ = M.E

Tactic:
by rw [h, loopyOn_closure_eq, loopyOn_ground]

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

Goal state before:
pp: case refine_2.some
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
a : A
i : ι
⊢ (Polynomial.aeval a) (hx.mvPolynomialOptionEquivPolynomialAdjoin (X (some i))) =
    (aeval fun o ↦ o.elim a x) (X (some i))

Tactic:
· rw [hx.mvPolynomialOptionEquivPolynomialAdjoin_X_some, Polynomial.aeval_C,
        hx.algebraMap_aevalEquiv, aeval_X, aeval_X, Option.elim]

Goal state after:
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
inst✝¹ : FaithfulSMul R S
inst✝ : Algebra.IsIntegral R S
⊢ IsTranscendenceBasis R x ↔ IsTranscendenceBasis S x

Tactic:
IsTranscendenceBasis,

Goal state after:
ι : 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
inst✝¹ : FaithfulSMul R S
inst✝ : Algebra.IsIntegral R S
⊢ (AlgebraicIndependent R x ∧ ∀ (s : Set A), AlgebraicIndepOn R _root_.id s → Set.range x ⊆ s → Set.range x = s) ↔
    AlgebraicIndependent S x ∧ ∀ (s : Set A), AlgebraicIndepOn S _root_.id s → Set.range x ⊆ s → Set.range x = s
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
inst✝¹ : FaithfulSMul R S
inst✝ : Algebra.IsAlgebraic R S
⊢ IsTranscendenceBasis R x ↔ IsTranscendenceBasis S x

Tactic:
IsTranscendenceBasis,

Goal state after:
ι : 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
inst✝¹ : FaithfulSMul R S
inst✝ : Algebra.IsAlgebraic R S
⊢ (AlgebraicIndependent R x ∧ ∀ (s : Set A), AlgebraicIndepOn R _root_.id s → Set.range x ⊆ s → Set.range x = s) ↔
    AlgebraicIndependent S x ∧ ∀ (s : Set A), AlgebraicIndepOn S _root_.id s → Set.range x ⊆ s → Set.range x = s
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors A
hx : IsTranscendenceBasis R x
this : FaithfulSMul R A
⊢ lift.{w, u} #ι = lift.{u, w} (trdeg R A)

Tactic:
rw [← matroid_cRank_eq, ← (matroid_isBase_iff.mpr hx.to_subtype_range).cardinalMk_eq_cRank,
    lift_mk_eq'.mpr ⟨.ofInjective _ hx.1.injective⟩]

Goal state after: