mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.LinearDisjoint

Goal state before:
pp: case «0».«1»
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
hf : Flat R ↥M ∨ Flat R ↥N
hc : ∀ (m n : ↥(M ⊓ N)), Commute ↑m ↑n
a✝ : Nontrivial R
s : Finset ↥(M ⊓ N)
h : LinearIndependent R fun i ↦ ↑i
hs : Nontrivial ↥s
a b : ↥s
hab : a ≠ b
hij : ![a, b] ((fun i ↦ i) ⟨0, ⋯⟩) = ![a, b] ((fun i ↦ i) ⟨1, ⋯⟩)
⊢ (fun i ↦ i) ⟨0, ⋯⟩ = (fun i ↦ i) ⟨1, ⋯⟩

Tactic:
simp [hab] at hij

Goal state after:
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Injective ⇑f
x : M
h : IsAssociatedPrime (⊥.colon {x}).radical M
⊢ (⊥.colon {x}).radical = (⊥.colon {f x}).radical

Tactic:
ext r

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Injective ⇑f
x : M
h : IsAssociatedPrime (⊥.colon {x}).radical M
r : R
⊢ r ∈ (⊥.colon {x}).radical ↔ r ∈ (⊥.colon {f x}).radical
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness

Goal state before:
pp: A : Type u
inst✝² : CommRing A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
N₁ N₂ : Submodule A M
f : ↥N₂ ⧸ N₁.submoduleOf N₂ →ₗ[A] M ⧸ N₁ := (N₁.submoduleOf N₂).mapQ N₁ N₂.subtype ⋯
hf₁ : f.ker = ⊥
hf₂ : f.range = map N₁.mkQ N₂
x✝ : N₁.IsQuotientEquivQuotientPrime N₂
h : N₁ ≤ N₂
p : PrimeSpectrum A
e : (↥N₂ ⧸ N₁.submoduleOf N₂) ≃ₗ[A] A ⧸ p.asIdeal
x : M
hx : x ∈ N₂
hx' : (N₁.submoduleOf N₂).mkQ ⟨x, hx⟩ = e.symm 1
hx'' : N₁.mkQ x = f (e.symm 1)
⊢ ⊥.colon {N₁.mkQ x} = p.asIdeal

Tactic:
ext r

Goal state after:
A : Type u
inst✝² : CommRing A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
N₁ N₂ : Submodule A M
f : ↥N₂ ⧸ N₁.submoduleOf N₂ →ₗ[A] M ⧸ N₁ := (N₁.submoduleOf N₂).mapQ N₁ N₂.subtype ⋯
hf₁ : f.ker = ⊥
hf₂ : f.range = map N₁.mkQ N₂
x✝ : N₁.IsQuotientEquivQuotientPrime N₂
h : N₁ ≤ N₂
p : PrimeSpectrum A
e : (↥N₂ ⧸ N₁.submoduleOf N₂) ≃ₗ[A] A ⧸ p.asIdeal
x : M
hx : x ∈ N₂
hx' : (N₁.submoduleOf N₂).mkQ ⟨x, hx⟩ = e.symm 1
hx'' : N₁.mkQ x = f (e.symm 1)
r : A
⊢ r ∈ ⊥.colon {N₁.mkQ x} ↔ r ∈ p.asIdeal
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness

Goal state before:
pp: case refine_2.refine_3
A : Type u
inst✝² : CommRing A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
N₁ N₂ : Submodule A M
f : ↥N₂ ⧸ N₁.submoduleOf N₂ →ₗ[A] M ⧸ N₁ := (N₁.submoduleOf N₂).mapQ N₁ N₂.subtype ⋯
hf₁ : f.ker = ⊥
hf₂ : f.range = map N₁.mkQ N₂
x✝ : ∃ x, (⊥.colon {N₁.mkQ x}).IsPrime ∧ N₂ = N₁ ⊔ A ∙ x
x : M
hx : (⊥.colon {N₁.mkQ x}).IsPrime
hx' : N₂ = N₁ ⊔ A ∙ x
hxN₂ : x ∈ N₂
⊢ ((N₁.submoduleOf N₂).mkQ ∘ₗ toSpanSingleton A ↥N₂ ⟨x, hxN₂⟩).range = ⊤

Tactic:
range_comp

Goal state after:
case refine_2.refine_3
A : Type u
inst✝² : CommRing A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
N₁ N₂ : Submodule A M
f : ↥N₂ ⧸ N₁.submoduleOf N₂ →ₗ[A] M ⧸ N₁ := (N₁.submoduleOf N₂).mapQ N₁ N₂.subtype ⋯
hf₁ : f.ker = ⊥
hf₂ : f.range = map N₁.mkQ N₂
x✝ : ∃ x, (⊥.colon {N₁.mkQ x}).IsPrime ∧ N₂ = N₁ ⊔ A ∙ x
x : M
hx : (⊥.colon {N₁.mkQ x}).IsPrime
hx' : N₂ = N₁ ⊔ A ∙ x
hxN₂ : x ∈ N₂
⊢ map (N₁.submoduleOf N₂).mkQ (toSpanSingleton A ↥N₂ ⟨x, hxN₂⟩).range = ⊤
Module: Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsGCDMonoid R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
⊢ (↑↑I).IsPrincipal

Tactic:
let J : Ideal R := (I : FractionalIdeal R⁰ (FractionRing R)).num
  have hJunit : IsUnit (J : FractionalIdeal R⁰ (FractionRing R)) :=
    FractionalIdeal.isUnit_num.mpr ⟨I, rfl⟩
  have hJprin : J.IsPrincipal := isPrincipal_of_isUnit_fractionalIdeal J hJunit
  exact isPrincipal_of_isPrincipal_num
    (I : FractionalIdeal R⁰ (FractionRing R)) hJprin

Goal state after:
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
K' : Type u_3
inst✝² : Field K'
inst✝¹ : Algebra R K'
inst✝ : IsFractionRing R K'
I : (FractionalIdeal R⁰ K)ˣ
⊢ (QuotientGroup.congr (toPrincipalIdeal R (FractionRing R)).range (toPrincipalIdeal R K').range
        (Units.mapEquiv (canonicalEquiv R⁰ (FractionRing R) K').toMulEquiv) ⋯)
      ((QuotientGroup.mk' (toPrincipalIdeal R (FractionRing R)).range)
        ((Units.map ↑(canonicalEquiv R⁰ K (FractionRing R))) I)) =
    (QuotientGroup.mk' (toPrincipalIdeal R K').range) ((Units.mapEquiv ↑(canonicalEquiv R⁰ K K')) I)

Tactic:
simp only [ClassGroup, QuotientGroup.congr_mk']

Goal state after:
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)ˣ
⊢ (QuotientGroup.mk' (toPrincipalIdeal R K').range)
      ((Units.mapEquiv (canonicalEquiv R⁰ (FractionRing R) K').toMulEquiv)
        ((Units.map ↑(canonicalEquiv R⁰ K (FractionRing R))) I)) =
    (QuotientGroup.mk' (toPrincipalIdeal R K').range) ((Units.mapEquiv ↑(canonicalEquiv R⁰ K K')) 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:
rw [mulIndicator_preimage, Set.ite, Set.sdiff_eq]

Goal state after:
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✝¹] (⇑f ⁻¹' s ∩ U ∪ 1 ⁻¹' s ∩ Uᶜ)
Module: Mathlib.RingTheory.LocalRing.ResidueField.Fiber

Goal state before:
pp: case mpr
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
p✝ : Ideal R
inst✝ : p✝.IsPrime
p : PrimeSpectrum R
q₁ q₂ : ↑(comap (algebraMap R S) ⁻¹' {p})
H : q₁ ≤ q₂
x : p.asIdeal.Fiber S
r : R
hr : r ∉ p.asIdeal
s : S
hx : 1 ⊗ₜ[R] s ∈ ((preimageEquivFiber R S p) q₁).asIdeal
e : r • x = 1 ⊗ₜ[R] s
⊢ 1 ⊗ₜ[R] s ∈ ((preimageEquivFiber R S p) q₂).asIdeal

pp: case mpr
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
p✝ : Ideal R
inst✝ : p✝.IsPrime
p : PrimeSpectrum R
q₁ q₂ : ↑(comap (algebraMap R S) ⁻¹' {p})
H : q₁ ≤ q₂
x : p.asIdeal.Fiber S
r : R
hx : (algebraMap R (p.asIdeal.Fiber S)) r * x ∈ ((preimageEquivFiber R S p) q₁).asIdeal
hr : r ∉ p.asIdeal
s : S
e : r • x = 1 ⊗ₜ[R] s
⊢ (algebraMap R (p.asIdeal.Fiber S)) r ∉ ((preimageEquivFiber R S p) q₂).asIdeal

pp: case mpr
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
p✝ : Ideal R
inst✝ : p✝.IsPrime
p : PrimeSpectrum R
q₁ q₂ : ↑(comap (algebraMap R S) ⁻¹' {p})
H : q₁ ≤ q₂
x : p.asIdeal.Fiber S
hx : x ∈ ((preimageEquivFiber R S p) q₁).asIdeal
r : R
hr : r ∉ p.asIdeal
s : S
e : r • x = 1 ⊗ₜ[R] s
⊢ (algebraMap R (p.asIdeal.Fiber S)) r ∉ ((preimageEquivFiber R S p) q₁).asIdeal

Tactic:
· replace hx : s ∈ q₁.1.asIdeal := by simpa using! hx
        simpa using! H hx

Goal state after:
case mpr
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
p✝ : Ideal R
inst✝ : p✝.IsPrime
p : PrimeSpectrum R
q₁ q₂ : ↑(comap (algebraMap R S) ⁻¹' {p})
H : q₁ ≤ q₂
x : p.asIdeal.Fiber S
r : R
hx : (algebraMap R (p.asIdeal.Fiber S)) r * x ∈ ((preimageEquivFiber R S p) q₁).asIdeal
hr : r ∉ p.asIdeal
s : S
e : r • x = 1 ⊗ₜ[R] s
⊢ (algebraMap R (p.asIdeal.Fiber S)) r ∉ ((preimageEquivFiber R S p) q₂).asIdeal

case mpr
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
p✝ : Ideal R
inst✝ : p✝.IsPrime
p : PrimeSpectrum R
q₁ q₂ : ↑(comap (algebraMap R S) ⁻¹' {p})
H : q₁ ≤ q₂
x : p.asIdeal.Fiber S
hx : x ∈ ((preimageEquivFiber R S p) q₁).asIdeal
r : R
hr : r ∉ p.asIdeal
s : S
e : r • x = 1 ⊗ₜ[R] s
⊢ (algebraMap R (p.asIdeal.Fiber S)) r ∉ ((preimageEquivFiber R S p) q₁).asIdeal
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: case succ
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSimpleGroup G
x✝ : Group.IsSolvable G
n✝ : ℕ
hn : _root_.commutator G = ⊥
a b : G
⊢ a * b = b * a

Tactic:
rw [← mul_inv_eq_one, mul_inv_rev, ← mul_assoc, ← mem_bot, ← hn, commutator_eq_closure]

Goal state after:
case succ
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSimpleGroup G
x✝ : Group.IsSolvable G
n✝ : ℕ
hn : _root_.commutator G = ⊥
a b : G
⊢ a * b * a⁻¹ * b⁻¹ ∈ closure (commutatorSet G)
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
α β : E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* (Polynomial.map ιFE g).SplittingField := algebraMap E (Polynomial.map ιFE g).SplittingField
c : F
hc :
  ∀ α' ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots,
    ∀ β' ∈ (Polynomial.map (ιEE'.comp ιFE) g).roots, -(α' - ιEE' α) / (β' - ιEE' β) ≠ (ιEE'.comp ιFE) c
γ : E := α + c • β
p : (↥F⟮γ⟯)[X] :=
  EuclideanDomain.gcd
    ((Polynomial.map (algebraMap F ↥F⟮γ⟯) f).comp (C (AdjoinSimple.gen F γ) - C ⟨(algebraMap F E) c, ⋯⟩ * X))
    (Polynomial.map (algebraMap F ↥F⟮γ⟯) g)
h : E[X] := EuclideanDomain.gcd ((Polynomial.map ιFE f).comp (C γ - C (ιFE c) * X)) (Polynomial.map ιFE g)
map_g_ne_zero : Polynomial.map ιFE g ≠ 0
h_ne_zero : h ≠ 0
p_linear : Polynomial.map (algebraMap (↥F⟮γ⟯) E) p = C h.leadingCoeff * (X - C β)
finale : β = (algebraMap (↥F⟮γ⟯) E) (-p.coeff 0 / p.coeff 1)
⊢ β ∈ F⟮γ⟯

Tactic:
rw [finale]

Goal state after:
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* (Polynomial.map ιFE g).SplittingField := algebraMap E (Polynomial.map ιFE g).SplittingField
c : F
hc :
  ∀ α' ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots,
    ∀ β' ∈ (Polynomial.map (ιEE'.comp ιFE) g).roots, -(α' - ιEE' α) / (β' - ιEE' β) ≠ (ιEE'.comp ιFE) c
γ : E := α + c • β
p : (↥F⟮γ⟯)[X] :=
  EuclideanDomain.gcd
    ((Polynomial.map (algebraMap F ↥F⟮γ⟯) f).comp (C (AdjoinSimple.gen F γ) - C ⟨(algebraMap F E) c, ⋯⟩ * X))
    (Polynomial.map (algebraMap F ↥F⟮γ⟯) g)
h : E[X] := EuclideanDomain.gcd ((Polynomial.map ιFE f).comp (C γ - C (ιFE c) * X)) (Polynomial.map ιFE g)
map_g_ne_zero : Polynomial.map ιFE g ≠ 0
h_ne_zero : h ≠ 0
p_linear : Polynomial.map (algebraMap (↥F⟮γ⟯) E) p = C h.leadingCoeff * (X - C β)
finale : β = (algebraMap (↥F⟮γ⟯) E) (-p.coeff 0 / p.coeff 1)
⊢ (algebraMap (↥F⟮γ⟯) E) (-p.coeff 0 / p.coeff 1) ∈ F⟮γ⟯
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
S : Type u_7
T : Type u_8
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : R →+* S
g : S →+* T
algInst✝² : Algebra R S := f.toAlgebra
algInst✝¹ : Algebra S T := g.toAlgebra
algInst✝ : Algebra R T := (g.comp f).toAlgebra
scalarTowerInst✝ : IsScalarTower R S T := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R T))
⊢ (mapRingHom g).comp (mapRingHom f) = mapRingHom (g.comp f)

Tactic:
simp_rw [mapRingHom, mapAlgebra_comp_mapAlgebra]

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

Goal state before:
pp: case inl
α : Type u_1
IsBase : Set α → Prop
B₁ B₂ : Set α
exch : ExchangeProperty IsBase
hB₁ : IsBase B₁
hB₂ : IsBase B₂
he : B₂ \ B₁ = ∅
⊢ (B₁ \ B₂).encard ≤ (B₂ \ B₁).encard

pp: case inr.inl
α : Type u_1
IsBase : Set α → Prop
B₁ B₂ : Set α
exch : ExchangeProperty IsBase
hB₁ : IsBase B₁
hB₂ : IsBase B₂
hinf : (B₂ \ B₁).encard = ⊤
⊢ (B₁ \ B₂).encard ≤ (B₂ \ B₁).encard

pp: case inr.inr
α : Type u_1
IsBase : Set α → Prop
B₁ B₂ : Set α
exch : ExchangeProperty IsBase
hB₁ : IsBase B₁
hB₂ : IsBase B₂
e : α
he : e ∈ B₂ \ B₁
hcard : ((B₂ \ B₁) \ {e}).encard < (B₂ \ B₁).encard
⊢ (B₁ \ B₂).encard ≤ (B₂ \ B₁).encard

Tactic:
· rw [exch.antichain hB₂ hB₁ (sdiff_eq_empty.mp he)]

Goal state after:
case inr.inl
α : Type u_1
IsBase : Set α → Prop
B₁ B₂ : Set α
exch : ExchangeProperty IsBase
hB₁ : IsBase B₁
hB₂ : IsBase B₂
hinf : (B₂ \ B₁).encard = ⊤
⊢ (B₁ \ B₂).encard ≤ (B₂ \ B₁).encard

case inr.inr
α : Type u_1
IsBase : Set α → Prop
B₁ B₂ : Set α
exch : ExchangeProperty IsBase
hB₁ : IsBase B₁
hB₂ : IsBase B₂
e : α
he : e ∈ B₂ \ B₁
hcard : ((B₂ \ B₁) \ {e}).encard < (B₂ \ B₁).encard
⊢ (B₁ \ B₂).encard ≤ (B₂ \ B₁).encard
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
inst✝ : M.RankPos
hB : M.IsBase ∅
⊢ False

Tactic:
exact M.empty_not_isBase hB

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
hne : I.Nonempty
⊢ M.RankPos

Tactic:
by
  obtain ⟨B, hB, hIB⟩ := hI.exists_isBase_superset
  exact hB.rankPos_of_nonempty (hne.mono hIB)

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
E : Set α
Indep : Finset α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Finset α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I J : Finset α⦄, Indep I → Indep J → I.card < J.card → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
subset_ground : ∀ ⦃I : Finset α⦄, Indep I → ↑I ⊆ E
I J : Set α
hI : ∀ (J : Finset α), ↑J ⊆ I → Indep J
hIfin : I.Finite
hJ : ∀ (J_1 : Finset α), ↑J_1 ⊆ J → Indep J_1
hJfin : J.Finite
hIJ : hIfin.toFinset.card < J.ncard
⊢ ∃ e ∈ J, e ∉ I ∧ ∀ (J : Finset α), ↑J ⊆ insert e I → Indep J

Tactic:
ncard_eq_toFinset_card _ hJfin

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
E : Set α
Indep : Finset α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Finset α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I J : Finset α⦄, Indep I → Indep J → I.card < J.card → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
subset_ground : ∀ ⦃I : Finset α⦄, Indep I → ↑I ⊆ E
I J : Set α
hI : ∀ (J : Finset α), ↑J ⊆ I → Indep J
hIfin : I.Finite
hJ : ∀ (J_1 : Finset α), ↑J_1 ⊆ J → Indep J_1
hJfin : J.Finite
hIJ : hIfin.toFinset.card < hJfin.toFinset.card
⊢ ∃ e ∈ J, e ∉ I ∧ ∀ (J : Finset α), ↑J ⊆ insert e I → Indep J
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ : Set α
M : Matroid α
N✝ N : Matroid β
inst✝ : N.Finitary
f : α → β
I : Set α
hI : ∀ J ⊆ I, J.Finite → (N.comap f).Indep J
⊢ (∀ J ⊆ f '' I, J.Finite → N.Indep J) ∧ InjOn f I

Tactic:
simp only [forall_subset_image_iff]

Goal state after:
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ : Set α
M : Matroid α
N✝ N : Matroid β
inst✝ : N.Finitary
f : α → β
I : Set α
hI : ∀ J ⊆ I, J.Finite → (N.comap f).Indep J
⊢ (∀ t ⊆ I, (f '' t).Finite → N.Indep (f '' t)) ∧ InjOn f I
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: case inr
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
heI : e ∉ I
he : e ∈ M.closure I
h : ∀ f ∈ I, e ∉ M.closure (I \ {f})
f : α
hfI : f ∈ I
⊢ e ∈ M.E \ M.closure (I \ {f})

Tactic:
exact ⟨mem_ground_of_mem_closure he, h f hfI⟩

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

Goal state before:
pp: α : Type u_1
M : Matroid α
C R : Set α
hR : R ⊆ M.E
⊢ ¬M.Indep C →
    C ⊆ R →
      (∀ ⦃D : Set α⦄, ¬M.Indep D → D ⊆ R → D ⊆ C → D = C) →
        ((¬M.Indep C ∧ C ⊆ M.E) ∧ ∀ ⦃D : Set α⦄, ¬M.Indep D ∧ D ⊆ M.E → D ⊆ C → D = C) ∧ C ⊆ R

Tactic:
exact fun hC hCR h ↦ ⟨⟨⟨hC,hCR.trans hR⟩,fun I hI hIC ↦ h hI.1 (hIC.trans hCR) hIC⟩,hCR⟩

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
⊢ M.eRk (M.E ∪ X) = M.eRank

Tactic:
rw [union_comm, eRk_union_ground]

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

Goal state before:
pp: α : Type u_1
e : α
M : Matroid α
X Y : Set α
⊢ M.eRk (insert e (X ∩ Y)) + M.eRk (insert e (X ∪ Y)) ≤ M.eRk (insert e X) + M.eRk (insert e Y)

Tactic:
insert_inter_distrib,

Goal state after:
α : Type u_1
e : α
M : Matroid α
X Y : Set α
⊢ M.eRk (insert e X ∩ insert e Y) + M.eRk (insert e (X ∪ Y)) ≤ M.eRk (insert e X) + M.eRk (insert e Y)
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
e : α
I : Set α
he : e ∈ M.E ∧ e ∉ M.closure I
hI : M.IsBasis' I X
⊢ M.eRk (insert e X) = M.eRk X + 1

Tactic:
hI.indep.mem_closure_iff',

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
e : α
I : Set α
he : e ∈ M.E ∧ ¬(e ∈ M.E ∧ (M.Indep (insert e I) → e ∈ I))
hI : M.IsBasis' I X
⊢ M.eRk (insert e X) = M.eRk X + 1
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
hI : I.Finite
h : M.eRk I = I.encard
J : Set α
hJ : M.IsBasis' J I
⊢ M.Indep I

Tactic:
rw [← hI.eq_of_subset_of_encard_le' hJ.subset]

Goal state after:
α : Type u_1
M : Matroid α
I : Set α
hI : I.Finite
h : M.eRk I = I.encard
J : Set α
hJ : M.IsBasis' J I
⊢ M.Indep J

α : Type u_1
M : Matroid α
I : Set α
hI : I.Finite
h : M.eRk I = I.encard
J : Set α
hJ : M.IsBasis' J I
⊢ I.encard ≤ J.encard
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_2
⊢ emptyOn α = loopyOn (emptyOn α).E

Tactic:
emptyOn_ground,

Goal state after:
α : Type u_2
⊢ emptyOn α = loopyOn ∅
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
Xs : Set (Set α)
⊢ M.closure (⋃ X ∈ Xs, M.closure X) = M.closure (⋃₀ Xs)

Tactic:
rw [sUnion_eq_iUnion, biUnion_eq_iUnion, closure_iUnion_closure_eq_closure_iUnion]

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
⊢ (M ↾ X).InvariantCardinalRank

Tactic:
refine ⟨fun I J Y hI hJ ↦ ?_⟩
  rw [isBasis_restrict_iff'] at hI hJ
  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
⊢ M.cRk (X ∩ Y) + M.cRk (M.closure X ∪ M.closure Y) ≤ M.cRk X + M.cRk Y

Tactic:
← hIX.closure_eq_closure,

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
⊢ M.cRk (X ∩ Y) + M.cRk (M.closure IX ∪ M.closure Y) ≤ M.cRk X + M.cRk Y
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
I X : Set α
hIX : M.IsBasis I X
hI : (M.map f hf).IsBasis (f '' I) (f '' X)
J X' : Set α
hJX : M.IsBasis J X'
h' : f '' X = f '' X'
hJ : (M.map f hf).IsBasis (f '' J) (f '' X)
⊢ X = X'

Tactic:
InjOn.image_eq_image_iff hf hIX.subset_ground hJX.subset_ground

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 X : Set α
hIX : M.IsBasis I X
hI : (M.map f hf).IsBasis (f '' I) (f '' X)
J X' : Set α
hJX : M.IsBasis J X'
h' : X = X'
hJ : (M.map f hf).IsBasis (f '' J) (f '' X)
⊢ X = X'
Module: Mathlib.RingTheory.AlgebraicIndependent.Basic

Goal state before:
pp: ι : 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
⊢ Injective ⇑(Finsupp.linearCombination R x)

Tactic:
have : Finsupp.linearCombination R x =
      (MvPolynomial.aeval x).toLinearMap.comp (Finsupp.linearCombination R X) := by
    ext
    simp

Goal state after:
ι : 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
this : Finsupp.linearCombination R x = (aeval x).toLinearMap ∘ₗ Finsupp.linearCombination R X
⊢ Injective ⇑(Finsupp.linearCombination R x)
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 ι
i : ι
h : i ∉ s
⊢ AlgebraicIndepOn R x (insert i s) ↔ AlgebraicIndepOn R x s ∧ Transcendental (↥(adjoin R (x '' s))) (x i)

Tactic:
classical simp_rw [← algebraicIndependent_equiv (subtypeInsertEquivOption h).symm,
    AlgebraicIndepOn]

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 ι
i : ι
h : i ∉ s
⊢ AlgebraicIndependent R ((fun i_1 ↦ x ↑i_1) ∘ ⇑(subtypeInsertEquivOption h).symm) ↔
    (AlgebraicIndependent R fun i ↦ x ↑i) ∧ Transcendental (↥(adjoin R (x '' s))) (x i)
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
B : Set α
N : Matroid α
hR : N ≤r M
hN : M.Spanning N.E
⊢ N.IsBase B ↔ M.IsBase B ∧ B ⊆ N.E

Tactic:
by
  obtain ⟨R, hR : R ⊆ M.E, rfl⟩ := hR
  rw [Spanning.isBase_restrict_iff (show M.Spanning R from hN), restrict_ground_eq]

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

Goal state before:
pp: α : Type u_2
M M' : Matroid α
h : M.E = M'.E
hsp : ∀ S ⊆ M.E, M.Spanning S ↔ M'.Spanning S
S : Set α
hSE : S ⊆ M.E
⊢ M.Spanning S ↔ M'.Spanning S

Tactic:
hsp _ hSE

Goal state after:
α : Type u_2
M M' : Matroid α
h : M.E = M'.E
hsp : ∀ S ⊆ M.E, M.Spanning S ↔ M'.Spanning S
S : Set α
hSE : S ⊆ M.E
⊢ M'.Spanning S ↔ M'.Spanning S
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 ∈ (M ↾ R).closure I ↔ e ∈ M.closure I ∩ R ∪ R \ M.E

Tactic:
hI.indep.mem_closure_iff',

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 ∈ (M ↾ R).E ∧ ((M ↾ R).Indep (insert e I) → e ∈ I) ↔ e ∈ M.closure I ∩ R ∪ R \ M.E
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
β : Type u_3
M : Matroid β
f : α → β
X I : Set α
hI : (M.comap f).IsBasis' I X
hI' : M.IsBasis' (f '' I) (f '' X)
hIinj : InjOn f I
⊢ ∀ (x : α), x ∈ (M.comap f).closure I ↔ x ∈ f ⁻¹' M.closure (f '' I)

Tactic:
hI.indep.mem_closure_iff',

Goal state after:
α : Type u_2
β : Type u_3
M : Matroid β
f : α → β
X I : Set α
hI : (M.comap f).IsBasis' I X
hI' : M.IsBasis' (f '' I) (f '' X)
hIinj : InjOn f I
⊢ ∀ (x : α), x ∈ (M.comap f).E ∧ ((M.comap f).Indep (insert x I) → x ∈ I) ↔ x ∈ f ⁻¹' M.closure (f '' I)