mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness

Goal state before:
pp: case zero
A : Type u
inst✝³ : CommRing A
inst✝² : IsNoetherianRing A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
x✝ : Module.Finite A M
motive : (N : Type v) → [inst : AddCommGroup N] → [inst_1 : Module A N] → [Module.Finite A N] → Prop
subsingleton :
  ∀ (N : Type v) [inst : AddCommGroup N] [inst_1 : Module A N] [inst_2 : Module.Finite A N] [Subsingleton N], motive N
quotient :
  ∀ (N : Type v) [inst : AddCommGroup N] [inst_1 : Module A N] [inst_2 : Module.Finite A N] (p : PrimeSpectrum A)
    (a : N ≃ₗ[A] A ⧸ p.asIdeal), motive N
exact :
  ∀ (N₁ : Type v) [inst : AddCommGroup N₁] [inst_1 : Module A N₁] [inst_2 : Module.Finite A N₁] (N₂ : Type v)
    [inst_3 : AddCommGroup N₂] [inst_4 : Module A N₂] [inst_5 : Module.Finite A N₂] (N₃ : Type v)
    [inst_6 : AddCommGroup N₃] [inst_7 : Module A N₃] [inst_8 : Module.Finite A N₃] (f : N₁ →ₗ[A] N₂) (g : N₂ →ₗ[A] N₃),
    Function.Injective ⇑f → Function.Surjective ⇑g → Function.Exact ⇑f ⇑g → motive N₁ → motive N₃ → motive N₂
equiv :
  ∀ (N₁ : Type v) [inst : AddCommGroup N₁] [inst_1 : Module A N₁] [inst_2 : Module.Finite A N₁] (N₂ : Type v)
    [inst_3 : AddCommGroup N₂] [inst_4 : Module A N₂] [inst_5 : Module.Finite A N₂] (f : N₁ ≃ₗ[A] N₂),
    motive N₁ → motive N₂
s : RelSeries {(N₁, N₂) | N₁.IsQuotientEquivQuotientPrime N₂}
hs1 : s.head = ⊥
hs2 : s.last = ⊤
h : 0 < s.length + 1
⊢ motive ↥s.head

Tactic:
hs1

Goal state after:
case zero
A : Type u
inst✝³ : CommRing A
inst✝² : IsNoetherianRing A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
x✝ : Module.Finite A M
motive : (N : Type v) → [inst : AddCommGroup N] → [inst_1 : Module A N] → [Module.Finite A N] → Prop
subsingleton :
  ∀ (N : Type v) [inst : AddCommGroup N] [inst_1 : Module A N] [inst_2 : Module.Finite A N] [Subsingleton N], motive N
quotient :
  ∀ (N : Type v) [inst : AddCommGroup N] [inst_1 : Module A N] [inst_2 : Module.Finite A N] (p : PrimeSpectrum A)
    (a : N ≃ₗ[A] A ⧸ p.asIdeal), motive N
exact :
  ∀ (N₁ : Type v) [inst : AddCommGroup N₁] [inst_1 : Module A N₁] [inst_2 : Module.Finite A N₁] (N₂ : Type v)
    [inst_3 : AddCommGroup N₂] [inst_4 : Module A N₂] [inst_5 : Module.Finite A N₂] (N₃ : Type v)
    [inst_6 : AddCommGroup N₃] [inst_7 : Module A N₃] [inst_8 : Module.Finite A N₃] (f : N₁ →ₗ[A] N₂) (g : N₂ →ₗ[A] N₃),
    Function.Injective ⇑f → Function.Surjective ⇑g → Function.Exact ⇑f ⇑g → motive N₁ → motive N₃ → motive N₂
equiv :
  ∀ (N₁ : Type v) [inst : AddCommGroup N₁] [inst_1 : Module A N₁] [inst_2 : Module.Finite A N₁] (N₂ : Type v)
    [inst_3 : AddCommGroup N₂] [inst_4 : Module A N₂] [inst_5 : Module.Finite A N₂] (f : N₁ ≃ₗ[A] N₂),
    motive N₁ → motive N₂
s : RelSeries {(N₁, N₂) | N₁.IsQuotientEquivQuotientPrime N₂}
hs1 : s.head = ⊥
hs2 : s.last = ⊤
h : 0 < s.length + 1
⊢ motive ↥⊥
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I J : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' J' : Ideal R
hI : ↑I = ↑I'
hJ : ↑J = ↑J'
x y : R
hx : x ≠ 0
hy : y ≠ 0
h : Ideal.span {x} * I' = Ideal.span {y} * J'
this : IsUnit (mk' (FractionRing R) x ⟨y, ⋯⟩)
⊢ (toPrincipalIdeal R (FractionRing R)) this.unit * I = J

Tactic:
← Units.val_inj,

Goal state after:
case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I J : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' J' : Ideal R
hI : ↑I = ↑I'
hJ : ↑J = ↑J'
x y : R
hx : x ≠ 0
hy : y ≠ 0
h : Ideal.span {x} * I' = Ideal.span {y} * J'
this : IsUnit (mk' (FractionRing R) x ⟨y, ⋯⟩)
⊢ ↑((toPrincipalIdeal R (FractionRing R)) this.unit * I) = ↑J
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: case e_6
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
K' : Type u_3
inst✝² : Field K'
inst✝¹ : Algebra R K'
inst✝ : IsFractionRing R K'
I : (FractionalIdeal R⁰ K)ˣ
⊢ (Units.mapEquiv (canonicalEquiv R⁰ (FractionRing R) K').toMulEquiv)
      ((Units.map ↑(canonicalEquiv R⁰ K (FractionRing R))) I) =
    (Units.mapEquiv ↑(canonicalEquiv R⁰ K K')) I

Tactic:
← Units.val_inj,

Goal state after:
case e_6
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
K' : Type u_3
inst✝² : Field K'
inst✝¹ : Algebra R K'
inst✝ : IsFractionRing R K'
I : (FractionalIdeal R⁰ K)ˣ
⊢ ↑((Units.mapEquiv (canonicalEquiv R⁰ (FractionRing R) K').toMulEquiv)
        ((Units.map ↑(canonicalEquiv R⁰ K (FractionRing R))) I)) =
    ↑((Units.mapEquiv ↑(canonicalEquiv R⁰ K K')) I)
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: case refine_1
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
I : (FractionalIdeal S⁰ L)ˣ
x✝ : ∃ x, (∃ x_1, spanSingleton R⁰ ↑x_1 = ↑x) ∧ (Units.mapEquiv ↑(ringEquivOfRingEquiv K L f)) x = I
u : (FractionalIdeal R⁰ K)ˣ
v : Kˣ
huv : spanSingleton R⁰ ↑v = ↑u
hu : (Units.mapEquiv ↑(ringEquivOfRingEquiv K L f)) u = I
⊢ ∃ x, spanSingleton S⁰ ↑x = ↑I

pp: case refine_2
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
I : (FractionalIdeal S⁰ L)ˣ
x✝ : ∃ x, spanSingleton S⁰ ↑x = ↑I
u : Lˣ
hu : spanSingleton S⁰ ↑u = ↑I
⊢ ∃ x, (∃ x_1, spanSingleton R⁰ ↑x_1 = ↑x) ∧ (Units.mapEquiv ↑(ringEquivOfRingEquiv K L f)) x = I

Tactic:
· 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]

Goal state after:
case refine_2
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
I : (FractionalIdeal S⁰ L)ˣ
x✝ : ∃ x, spanSingleton S⁰ ↑x = ↑I
u : Lˣ
hu : spanSingleton S⁰ ↑u = ↑I
⊢ ∃ x, (∃ x_1, spanSingleton R⁰ ↑x_1 = ↑x) ∧ (Units.mapEquiv ↑(ringEquivOfRingEquiv K L f)) x = I
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
R : Type u_5
inst✝ : One R
U : Set X
f : LocallyConstant X R
hU : IsClopen U
s : Set R
⊢ IsOpen[inst✝¹] (U.mulIndicator ⇑f ⁻¹' s)

Tactic:
by
    rw [mulIndicator_preimage, Set.ite, Set.sdiff_eq]
    exact ((f.2 s).inter hU.isOpen).union ((IsLocallyConstant.const 1 s).inter hU.compl.isOpen)

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
N : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
n : ℕ
bN : Module.Basis (Fin n) R N
c : R
x : M × N
x✝ : Fin n → M × N
⊢ ((bN.det.compLinearMap (LinearMap.snd R M N)).smulRight (c • x).1) x✝ =
    ((RingHom.id R) c • (bN.det.compLinearMap (LinearMap.snd R M N)).smulRight x.1) x✝

Tactic:
simp [smul_smul, mul_comm]

Goal state after:
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
⊢ ⁅_root_.commutator G, _root_.commutator G⁆ = _root_.commutator G

Tactic:
_root_.commutator

Goal state after:
case succ
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSimpleGroup G
n : ℕ
ih : derivedSeries G n.succ = _root_.commutator G
⊢ ⁅⁅⊤, ⊤⁆, ⁅⊤, ⊤⁆⁆ = ⁅⊤, ⊤⁆
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
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : PrimeSpectrum S
⊢ rankAtStalk (S ⊗[R] M) p = rankAtStalk M (comap (algebraMap R S) p)

Tactic:
let q : PrimeSpectrum R := p.comap (algebraMap R S)
  let := Localization.AtPrime.algebraOfLiesOver q.asIdeal p.asIdeal
  let e : LocalizedModule p.asIdeal.primeCompl (S ⊗[R] M) ≃ₗ[Localization.AtPrime p.asIdeal]
      Localization.AtPrime p.asIdeal ⊗[Localization.AtPrime q.asIdeal]
        LocalizedModule q.asIdeal.primeCompl M :=
    LocalizedModule.equivTensorProduct _ _ ≪≫ₗ
      (AlgebraTensorModule.cancelBaseChange R S _ _ M) ≪≫ₗ
      (AlgebraTensorModule.cancelBaseChange R _ _ _ M).symm ≪≫ₗ
      (AlgebraTensorModule.congr (LinearEquiv.refl _ _)
        (LocalizedModule.equivTensorProduct _ M).symm)
  rw [rankAtStalk, e.finrank_eq]
  apply Module.finrank_baseChange

Goal state after:
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
⊢ Free R M

Tactic:
by
  obtain ⟨S, hS⟩ := ((Invertible.linearEquiv R M).symm 1).exists_finset
  replace hS : 1 = ∑ i ∈ S, i.1 i.2 := by
    simpa [LinearEquiv.symm_apply_eq, Invertible.linearEquiv] using hS
  obtain ⟨⟨f, m⟩, mem, hfm⟩ := IsLocalRing.exists_of_isUnit_sum (hS ▸ isUnit_one)
  exact .of_equiv <| .symm <| .ofBijective f (Invertible.bijective_of_surjective <|
    LinearMap.range_eq_top.mp <| Ideal.eq_top_of_isUnit_mem _ ⟨m, rfl⟩ hfm)

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

Goal state before:
pp: 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)
hF : Normal F ↥E
i : (i : ι) × ↥(t i)
x✝ : i ∈ s
⊢ adjoin F ((minpoly F i.snd).rootSet K) ≤ t i.fst

Tactic:
adjoin_le_iff,

Goal state after:
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)
hF : Normal F ↥E
i : (i : ι) × ↥(t i)
x✝ : i ∈ s
⊢ (minpoly F i.snd).rootSet K ⊆ ↑(t i.fst)
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✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
I✝ J✝ I J : (Submodule R A)ˣ
⊢ Pic.mk R ↥↑(I * J) = Pic.mk R ↥↑I * Pic.mk R ↥↑J

Tactic:
rw [← mk_tensor, mk_eq_mk_iff]; exact ⟨(tensorEquivMul I J).symm⟩

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
⊢ B ∩ X ⊆ I

Tactic:
rw [hI.eq_of_subset_indep (hB.indep.inter_right X) (subset_inter hIB hI.subset)
    inter_subset_right]

Goal state after:
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
A : Type u_4
inst✝³ : CommSemiring R
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
M : Pic R
h : M ∈ relPic R A
e : A ⊗[R] M.AsModule ≃ₗ[A] A
f : A ⊗[R] M⁻¹.AsModule ≃ₗ[A] A
⊢ M * M⁻¹ = 1

Tactic:
mul_inv_cancel

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
f : α → β
I : Set α
N : Matroid β
hI : N.Indep (f '' I) ∧ ¬InjOn f I
⊢ (N.Indep (f '' I) → ¬InjOn f I) ∧ I ⊆ f ⁻¹' N.E

Tactic:
iff_true_intro hI.1,

Goal state after:
case inr
α : Type u_1
β : Type u_2
f : α → β
I : Set α
N : Matroid β
hI : N.Indep (f '' I) ∧ ¬InjOn f I
⊢ (True → ¬InjOn f I) ∧ I ⊆ f ⁻¹' N.E
Module: Mathlib.Combinatorics.Matroid.IndepAxioms

Goal state before:
pp: α : Type u_1
E : Set α
IsBase : Set α → Prop
isBase_exchange : ExchangeProperty IsBase
subset_ground : ∀ (B : Set α), IsBase B → B ⊆ E
B : Set α
hB : IsBase B
hfin : B.Finite
X : Set α
x✝¹ : X ⊆ E
Y : Set α
x✝ : ∃ B, IsBase B ∧ Y ⊆ B
B' : Set α
hB' : IsBase B'
hYB' : Y ⊆ B'
⊢ Y.encard ≤ ↑B.ncard

Tactic:
rw [hfin.cast_ncard_eq, isBase_exchange.encard_isBase_eq hB hB']

Goal state after:
α : Type u_1
E : Set α
IsBase : Set α → Prop
isBase_exchange : ExchangeProperty IsBase
subset_ground : ∀ (B : Set α), IsBase B → B ⊆ E
B : Set α
hB : IsBase B
hfin : B.Finite
X : Set α
x✝¹ : X ⊆ E
Y : Set α
x✝ : ∃ B, IsBase B ∧ Y ⊆ B
B' : Set α
hB' : IsBase B'
hYB' : Y ⊆ B'
⊢ Y.encard ≤ B'.encard
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
I X Y J : Set α
hI : M.IsBasis I X
hJ : M.IsBasis J Y
hJX : J ⊆ X
hIY : I ⊆ Y
⊢ M.IsBasis I Y

Tactic:
by
  have hI' := hI.isBasis_subset (subset_inter hI.subset hIY) inter_subset_left
  have hJ' := hJ.isBasis_subset (subset_inter hJX hJ.subset) inter_subset_right
  exact hI'.transfer hJ' inter_subset_right hJ

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

Goal state before:
pp: α : Type u_1
E : Set α
IsBase : Set α → Prop
exists_finite_base : ∃ B, IsBase B ∧ B.Finite
isBase_exchange : ExchangeProperty IsBase
subset_ground : ∀ (B : Set α), IsBase B → B ⊆ E
⊢ (Matroid.ofExistsFiniteIsBase E IsBase exists_finite_base isBase_exchange subset_ground).RankFinite

Tactic:
obtain ⟨B, hB, hfin⟩ := exists_finite_base
  exact Matroid.IsBase.rankFinite_of_finite (by simpa) hfin

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

Goal state before:
pp: case refine_1
α : Type u_1
M : Matroid α
X : Set α
n : ℕ∞
h : n ≤ M.eRk X
⊢ ∃ I ⊆ X, M.Indep I ∧ I.encard = n

Tactic:
obtain ⟨J, hJ⟩ := M.exists_isBasis' X

Goal state after:
case refine_1
α : Type u_1
M : Matroid α
X : Set α
n : ℕ∞
h : n ≤ M.eRk X
J : Set α
hJ : M.IsBasis' J X
⊢ ∃ I ⊆ X, M.Indep I ∧ I.encard = n
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
⊢ [M.IsColoop e, e ∈ M.coloops, M.IsCocircuit {e}, ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B,
      (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E, ∀ (X : Set α), e ∈ M.closure X ↔ e ∈ X,
      ¬M.Spanning (M.E \ {e})].TFAE

Tactic:
tfae_have 1 ↔ 3 := singleton_isCocircuit.symm

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}
⊢ [M.IsColoop e, e ∈ M.coloops, M.IsCocircuit {e}, ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B,
      (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E, ∀ (X : Set α), e ∈ M.closure X ↔ e ∈ X,
      ¬M.Spanning (M.E \ {e})].TFAE
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
inst✝ : M.RankFinite
hX : M.Dep X
⊢ M.eRk X < X.encard

Tactic:
refine (M.eRk_le_encard X).lt_of_ne ?_

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
inst✝ : M.RankFinite
hX : M.Dep X
⊢ M.eRk X ≠ X.encard
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
R : Set α
hRE : R ⊆ M.E
⊢ (M ↾ R).IsColoop e ↔ e ∉ M.closure (R \ {e}) ∧ e ∈ R

Tactic:
wlog heR : e ∈ R

Goal state after:
case inr
α : Type u_1
M : Matroid α
e : α
R : Set α
hRE : R ⊆ M.E
this :
  ∀ {α : Type u_1} {M : Matroid α} {e : α} {R : Set α},
    R ⊆ M.E → e ∈ R → ((M ↾ R).IsColoop e ↔ e ∉ M.closure (R \ {e}) ∧ e ∈ R)
heR : e ∉ R
⊢ (M ↾ R).IsColoop e ↔ e ∉ M.closure (R \ {e}) ∧ e ∈ R

α✝ : Type u_1
M✝ : Matroid α✝
e✝ : α✝
α : Type u_1
M : Matroid α
e : α
R : Set α
hRE : R ⊆ M.E
heR : e ∈ R
⊢ (M ↾ R).IsColoop e ↔ e ∉ M.closure (R \ {e}) ∧ e ∈ R
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
C : Set α
inst✝ : M.Finitary
hC : M.IsCircuit C
J : Set α
hJC : J ⊆ C
hJfin : J.Finite
hJ : ¬M.Indep J
⊢ C.Finite

Tactic:
← hC.eq_of_not_indep_subset hJ hJC

Goal state after:
α : Type u_1
M : Matroid α
C : Set α
inst✝ : M.Finitary
hC : M.IsCircuit C
J : Set α
hJC : J ⊆ C
hJfin : J.Finite
hJ : ¬M.Indep J
⊢ J.Finite
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
X I : Set α
h : M.IsBasis' I X
⊢ M.closure I = M.closure X

Tactic:
by
  rw [← closure_inter_ground _ X, h.isBasis_inter_ground.closure_eq_closure]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ M ↾ {e | M.IsNonloop e} ↾ M.E = M

Tactic:
ext_iff_indep

Goal state after:
α : Type u_1
M : Matroid α
⊢ (M ↾ {e | M.IsNonloop e} ↾ M.E).E = M.E ∧
    ∀ ⦃I : Set α⦄, I ⊆ (M ↾ {e | M.IsNonloop e} ↾ M.E).E → ((M ↾ {e | M.IsNonloop e} ↾ M.E).Indep I ↔ M.Indep I)
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: α : Type u
β : Type v
f : α → β
M✝ : Matroid α
I J B B' X Y : Set α
M : Matroid α
inst✝ : M.InvariantCardinalRank
hf : InjOn f M.E
⊢ (M.map f hf).InvariantCardinalRank

Tactic:
refine ⟨fun I J X hI hJ ↦ ?_⟩

Goal state after:
α : Type u
β : Type v
f : α → β
M✝ : Matroid α
I✝ J✝ B B' X✝ Y : Set α
M : Matroid α
inst✝ : M.InvariantCardinalRank
hf : InjOn f M.E
I J X : Set β
hI : (M.map f hf).IsBasis I X
hJ : (M.map f hf).IsBasis J X
⊢ #↑(I \ J) = #↑(J \ I)
Module: Mathlib.RingTheory.Algebraic.MvPolynomial

Goal state before:
pp: case refine_2
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Nontrivial R
i : σ
s : Set σ
f : R[X]
h : Transcendental (↥(supported R s)) ((Polynomial.aeval (X i)) f)
x✝¹ x✝ : R
heq : (algebraMap R ↥(supported R s)) x✝¹ = (algebraMap R ↥(supported R s)) x✝
⊢ (algebraMap R (MvPolynomial σ R)) x✝¹ = (algebraMap R (MvPolynomial σ R)) x✝

Tactic:
exact congr($(heq).1)

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 α
M : Matroid β
inst✝ : M.InvariantCardinalRank
f : α → β
⊢ (M.comap f).InvariantCardinalRank

Tactic:
refine ⟨fun I J X hI hJ ↦ ?_⟩

Goal state after:
α : Type u
β : Type v
f✝ : α → β
M✝ : Matroid α
I✝ J✝ B B' X✝ Y : Set α
M : Matroid β
inst✝ : M.InvariantCardinalRank
f : α → β
I J X : Set α
hI : (M.comap f).IsBasis I X
hJ : (M.comap f).IsBasis J X
⊢ #↑(I \ J) = #↑(J \ I)
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: case inr.inr.inr
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : M✶.Indep (insert f (M✶.E \ B) \ {e})
hne : e ≠ f
hB'✝ : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
hfB : f ∈ B
heE : e ∈ M.E
heB : e ∉ B
hB' : M.IsBase (M.E \ (insert f (M✶.E \ B) \ {e}))
⊢ insert e B ⊆ insert e (insert f ((M.E \ (M.E \ B)) \ {f}))

Tactic:
sdiff_sdiff_cancel_left hB.subset_ground

Goal state after:
case inr.inr.inr
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : M✶.Indep (insert f (M✶.E \ B) \ {e})
hne : e ≠ f
hB'✝ : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
hfB : f ∈ B
heE : e ∈ M.E
heB : e ∉ B
hB' : M.IsBase (M.E \ (insert f (M✶.E \ B) \ {e}))
⊢ insert e B ⊆ insert e (insert f (B \ {f}))
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M₁ M₂ : Matroid α
h : ∀ (X : Set α), M₁.closure X = M₂.closure X
⊢ M₁.E = M₂.E

Tactic:
by simpa using h univ

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

Goal state before:
pp: α : Type u_2
M : Matroid α
R S : Set α
⊢ (M ↾ R).Spanning S ↔ R ∩ M.E ⊆ M.closure S ∧ S ⊆ R

Tactic:
rw [spanning_iff, restrict_closure_eq', restrict_ground_eq, and_congr_left_iff,
    sdiff_eq_compl_inter, ← union_inter_distrib_right, inter_eq_right, union_comm,
    ← sdiff_subset_iff, sdiff_compl]
  intro hSR
  rw [inter_eq_self_of_subset_left hSR]

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

Goal state before:
pp: R : Type u_2
A : Type v
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set (Set A)
hsn : s.Nonempty
hs : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) s
h : ∀ a ∈ s, AlgebraicIndependent R Subtype.val
⊢ AlgebraicIndependent R Subtype.val

Tactic:
let : Nonempty s := Nonempty.to_subtype hsn

Goal state after:
R : Type u_2
A : Type v
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set (Set A)
hsn : s.Nonempty
hs : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) s
h : ∀ a ∈ s, AlgebraicIndependent R Subtype.val
this : Nonempty ↑s := Nonempty.to_subtype hsn
⊢ AlgebraicIndependent R Subtype.val
Module: Mathlib.GroupTheory.GroupAction.FixedPoints

Goal state before:
pp: α : Type u_1
M : Type u_3
inst✝¹ : Monoid M
inst✝ : MulAction M α
m₁ m₂ : M
a : α
h₁ : a ∈ fixedBy α m₁
h₂ : a ∈ fixedBy α m₂
⊢ a ∈ fixedBy α (m₁ * m₂)

Tactic:
rw [mem_fixedBy, mul_smul, h₂, h₁]

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.FixedPoints

Goal state before:
pp: α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g : G
s_ss_fixedBy : s ⊆ fixedBy α g
⊢ s ∈ fixedBy (Set α) g

Tactic:
rw [← fixedBy_inv]

Goal state after:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g : G
s_ss_fixedBy : s ⊆ fixedBy α g
⊢ s ∈ fixedBy (Set α) g⁻¹
Module: Mathlib.GroupTheory.GroupAction.FixedPoints

Goal state before:
pp: α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g : G
s_subset : (fixedBy α g)ᶜ ⊆ s
⊢ s ∈ fixedBy (Set α) g

Tactic:
rw [← fixedBy_inv]

Goal state after:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g : G
s_subset : (fixedBy α g)ᶜ ⊆ s
⊢ s ∈ fixedBy (Set α) g⁻¹
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: case mpr
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
i : AlgebraicIndependent R x
p : ∀ (κ : Type w) (w : κ → A), AlgebraicIndependent R w → ∀ (j : ι → κ), w ∘ j = x → Surjective j
⊢ IsTranscendenceBasis R x

Tactic:
use i

Goal state after:
case right
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
i : AlgebraicIndependent R x
p : ∀ (κ : Type w) (w : κ → A), AlgebraicIndependent R w → ∀ (j : ι → κ), w ∘ j = x → Surjective j
⊢ ∀ (s : Set A), AlgebraicIndepOn R _root_.id s → range x ⊆ s → range x = s
Module: Mathlib.GroupTheory.GroupAction.FixedPoints

Goal state before:
pp: α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g h : G
comm : Commute g h
⊢ (fixedBy α g)ᶜ ∈ fixedBy (Set α) h

Tactic:
rw [mem_fixedBy, Set.smul_set_compl, fixedBy_mem_fixedBy_of_commute comm]

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✝ : IsDomain A
s : Set A
⊢ (matroid R A).IsFlat s ↔ ∃ S, ↑S = s ∧ ∀ (a : A), IsAlgebraic (↥S) a → a ∈ s

Tactic:
rw [Matroid.isFlat_iff_closure_eq, matroid_closure_eq]
  set S := algebraicClosure (adjoin R s) A
  refine ⟨fun eq ↦ ⟨S.restrictScalars R, eq, fun a (h : IsAlgebraic S _) ↦ ?_⟩, ?_⟩
  · rw [← eq]; exact h.restrictScalars (adjoin R s)
  rintro ⟨s, rfl, hs⟩
  refine Set.ext fun a ↦ ⟨(hs _ <| adjoin_eq s ▸ ·), fun h ↦ ?_⟩
  exact isAlgebraic_algebraMap (A := A) (by exact (⟨a, subset_adjoin h⟩ : adjoin R s))

Goal state after: