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

Goal state before:
pp: 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'
⊢ (mk (FractionRing R)) I = (mk (FractionRing R)) J ↔ ∃ x y, x ≠ 0 ∧ y ≠ 0 ∧ Ideal.span {x} * I' = Ideal.span {y} * J'

Tactic:
ClassGroup.mk_eq_mk

Goal state after:
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, I * (toPrincipalIdeal R (FractionRing R)) x = J) ↔
    ∃ x y, x ≠ 0 ∧ y ≠ 0 ∧ Ideal.span {x} * I' = Ideal.span {y} * J'
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
⊢ ClassGroup R ≃* (FractionalIdeal R⁰ K)ˣ ⧸ (toPrincipalIdeal R K).range

Tactic:
haveI : Subgroup.map
    (Units.mapEquiv (canonicalEquiv R⁰ (FractionRing R) K).toMulEquiv).toMonoidHom
    (toPrincipalIdeal R (FractionRing R)).range = (toPrincipalIdeal R K).range := by
    ext I
    simp only [Subgroup.mem_map, mem_principal_ideals_iff]
    constructor
    · rintro ⟨I, ⟨x, hx⟩, rfl⟩
      refine ⟨FractionRing.algEquiv R K x, ?_⟩
      simp only [RingEquiv.toMulEquiv_eq_coe, MulEquiv.coe_toMonoidHom, coe_mapEquiv, ← hx,
        RingEquiv.coe_toMulEquiv, canonicalEquiv_spanSingleton]
      rfl
    · rintro ⟨x, hx⟩
      refine ⟨Units.mapEquiv (canonicalEquiv R⁰ K (FractionRing R)).toMulEquiv I,
        ⟨(FractionRing.algEquiv R K).symm x, ?_⟩, Units.ext ?_⟩
      · simp only [RingEquiv.toMulEquiv_eq_coe, coe_mapEquiv, ← hx, RingEquiv.coe_toMulEquiv,
          canonicalEquiv_spanSingleton]
        rfl
      · simp only [RingEquiv.toMulEquiv_eq_coe, MulEquiv.coe_toMonoidHom, coe_mapEquiv,
          RingEquiv.coe_toMulEquiv, canonicalEquiv_canonicalEquiv, canonicalEquiv_self,
          RingEquiv.refl_apply]
  exact QuotientGroup.congr (toPrincipalIdeal R (FractionRing R)).range (toPrincipalIdeal R K).range
    (Units.mapEquiv (FractionalIdeal.canonicalEquiv R⁰ (FractionRing R) K).toMulEquiv) this

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
⊢ (mk (FractionRing R)) I = (mk (FractionRing R)) ((FractionalIdeal.mk0 (FractionRing R)) ⟨integralRep ↑I, ⋯⟩)

Tactic:
ClassGroup.mk_eq_mk

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
⊢ ∃ x, I * (toPrincipalIdeal R (FractionRing R)) x = (FractionalIdeal.mk0 (FractionRing R)) ⟨integralRep ↑I, ⋯⟩
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
I : (FractionalIdeal R⁰ K)ˣ
hI : (↑↑I).IsPrincipal
x : K
hx : ↑↑I = R ∙ x
⊢ ↑I = spanSingleton R⁰ x

Tactic:
apply Subtype.coe_injective

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
I : (FractionalIdeal R⁰ K)ˣ
hI : (↑↑I).IsPrincipal
x : K
hx : ↑↑I = R ∙ x
⊢ (fun a ↦ ↑a) ↑I = (fun a ↦ ↑a) (spanSingleton R⁰ x)
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
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

Tactic:
rw [← q₂.2] at hr

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 ∉ (comap (algebraMap R S) ↑q₂).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)⁻¹ = 1

Tactic:
mul_inv_rev,

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⁻¹) = 1
Module: Mathlib.FieldTheory.Normal.Closure

Goal state before:
pp: F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra F K
inst✝¹ : Algebra F L
inst✝ : Algebra.IsAlgebraic F K
⊢ IsNormalClosure F K L ↔ (∀ (x : K), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits) ∧ normalClosure F K L = ⊤

Tactic:
by
  refine ⟨fun ⟨splits, h⟩ ↦ ⟨splits, ?_⟩, fun ⟨splits, h⟩ ↦ ⟨splits, ?_⟩⟩ <;>
    simpa only [normalClosure_eq_iSup_adjoin_of_splits splits] using h

Goal state after:
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Invertible R M
f : R →ₗ[R] M
hf : Function.Surjective ⇑f
r₁ r₂ : R
eq : f r₁ = f r₂
r : R
⊢ f (r • r₁) = f (r • r₂)

Tactic:
map_smul,

Goal state after:
R : Type u
M : Type v
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Invertible R M
f : R →ₗ[R] M
hf : Function.Surjective ⇑f
r₁ r₂ : R
eq : f r₁ = f r₂
r : R
⊢ r • f r₁ = r • f r₂
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 • β
β_in_Fγ : β ∈ F⟮γ⟯
⊢ ∃ γ, F⟮α, β⟯ = F⟮γ⟯

Tactic:
by
    use γ
    apply le_antisymm
    · rw [adjoin_le_iff]
      have α_in_Fγ : α ∈ F⟮γ⟯ := by
        rw [← add_sub_cancel_right α (c • β)]
        exact F⟮γ⟯.sub_mem (mem_adjoin_simple_self F γ) (F⟮γ⟯.toSubalgebra.smul_mem β_in_Fγ c)
      rintro x (rfl | rfl) <;> assumption
    · rw [adjoin_simple_le_iff]
      have α_in_Fαβ : α ∈ F⟮α, β⟯ := subset_adjoin F {α, β} (Set.mem_insert α {β})
      have β_in_Fαβ : β ∈ F⟮α, β⟯ := subset_adjoin F {α, β} (Set.mem_insert_of_mem α rfl)
      exact F⟮α, β⟯.add_mem α_in_Fαβ (F⟮α, β⟯.smul_mem β_in_Fαβ)

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

Goal state before:
pp: case inr
F : Type u_1
inst✝² : Field F
E : Type u_3
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
this : FiniteDimensional F E
hx : IsIntegral F x
L : Type u_1 := (p * minpoly F x).SplittingField
hL1 : (Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) p).Splits
j : E →ₐ[F] L := IsSplittingField.lift E p hL1
hL2 : (Polynomial.map (↑j) (Polynomial.map (algebraMap F E) (minpoly F x))).Splits
a : L
ha : a ∈ (Polynomial.map (algebraMap F L) (minpoly F x)).roots
⊢ a ∈ (↑j).range

Tactic:
let : Algebra F⟮x⟯ L := ((algHomAdjoinIntegralEquiv F hx).symm ⟨a, ha⟩).toRingHom.toAlgebra

Goal state after:
case inr
F : Type u_1
inst✝² : Field F
E : Type u_3
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
this✝ : FiniteDimensional F E
hx : IsIntegral F x
L : Type u_1 := (p * minpoly F x).SplittingField
hL1 : (Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) p).Splits
j : E →ₐ[F] L := IsSplittingField.lift E p hL1
hL2 : (Polynomial.map (↑j) (Polynomial.map (algebraMap F E) (minpoly F x))).Splits
a : L
ha : a ∈ (Polynomial.map (algebraMap F L) (minpoly F x)).roots
this : Algebra (↥F⟮x⟯) L := ((algHomAdjoinIntegralEquiv F hx).symm ⟨a, ha⟩).toAlgebra
⊢ a ∈ (↑j).range
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
h : M.RankFinite
⊢ ¬¬M.RankFinite

Tactic:
by simpa

Goal state after:
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: case neg.refine_1
F✝ : Type u_1
E✝ : Type u_2
inst✝⁵ : Field F✝
inst✝⁴ : Field E✝
inst✝³ : Algebra F✝ E✝
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
heq : F⟮α ^ m⟯ = F⟮α ^ n⟯
hmn : m < n
r s : F[X]
h : α ^ m * (aeval (α ^ n)) s - (aeval (α ^ n)) r = 0
hm : 0 < m
hzero : s ≠ 0
f : F[X] := X ^ m * (expand F n) s - (expand F n) r
⊢ f ≠ 0

Tactic:
have : f.coeff (n * s.natDegree + m) ≠ 0 := by
      have hn : 0 < n := by linarith only [hm, hmn]
      have hndvd : ¬ n ∣ n * s.natDegree + m := by
        rw [← Nat.dvd_add_iff_right (n.dvd_mul_right s.natDegree)]
        exact Nat.not_dvd_of_pos_of_lt hm hmn
      simp only [f, coeff_sub, coeff_X_pow_mul, s.coeff_expand_mul' hn, coeff_natDegree,
        coeff_expand hn r, hndvd, ite_false, sub_zero]
      exact leadingCoeff_ne_zero.2 hzero

Goal state after:
case neg.refine_1
F✝ : Type u_1
E✝ : Type u_2
inst✝⁵ : Field F✝
inst✝⁴ : Field E✝
inst✝³ : Algebra F✝ E✝
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
heq : F⟮α ^ m⟯ = F⟮α ^ n⟯
hmn : m < n
r s : F[X]
h : α ^ m * (aeval (α ^ n)) s - (aeval (α ^ n)) r = 0
hm : 0 < m
hzero : s ≠ 0
f : F[X] := X ^ m * (expand F n) s - (expand F n) r
this : f.coeff (n * s.natDegree + m) ≠ 0
⊢ f ≠ 0
Module: Mathlib.Combinatorics.Matroid.IndepAxioms

Goal state before:
pp: α : Type u_1
E : Set α
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I B : Set α⦄, Indep I → ¬Maximal Indep I → Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I)
indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
⊢ ∀ (I : Set α),
    (∀ J ⊆ I,
        J.Finite →
          (IndepMatroid.ofFinitary E Indep indep_empty indep_subset indep_aug indep_compact subset_ground).matroid.Indep
            J) →
      (IndepMatroid.ofFinitary E Indep indep_empty indep_subset indep_aug indep_compact subset_ground).matroid.Indep I

Tactic:
by simpa

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

Goal state before:
pp: α : Type u_1
E I X : Set α
⊢ I = ∅ ∧ X ⊆ E → (loopyOn E).IsBasis I X

Tactic:
by rintro ⟨rfl, hX⟩; rw [isBasis_iff]; simp

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

Goal state before:
pp: α : Type u_1
M✝ : Matroid α
I B✝ X✝ : Set α
M : Matroid α
X I' : Set α
hI'E : I' ⊆ M.E
B : Set α
hB : M.IsBase B
hI'B : Disjoint I' B
hI'X : I' ⊆ X
B' : Set α
hB' : M.IsBase B'
hI : M.IsBasis (B' \ X) (M.E \ X)
hIB' : B' \ X ⊆ B'
hB'IB : B' ⊆ B' \ X ∪ B
J : Set α
hJE : J ⊆ M.E
B'' : Set α
hB'' : M.IsBase B''
hdj : Disjoint J B''
hJX : J ⊆ X
hXJ : X \ B' ∩ M.E ⊆ J
⊢ B'' ∩ X ⊆ B' ∧ B' \ X ⊆ B'

Tactic:
and_iff_left sdiff_subset,

Goal state after:
α : Type u_1
M✝ : Matroid α
I B✝ X✝ : Set α
M : Matroid α
X I' : Set α
hI'E : I' ⊆ M.E
B : Set α
hB : M.IsBase B
hI'B : Disjoint I' B
hI'X : I' ⊆ X
B' : Set α
hB' : M.IsBase B'
hI : M.IsBasis (B' \ X) (M.E \ X)
hIB' : B' \ X ⊆ B'
hB'IB : B' ⊆ B' \ X ∪ B
J : Set α
hJE : J ⊆ M.E
B'' : Set α
hB'' : M.IsBase B''
hdj : Disjoint J B''
hJX : J ⊆ X
hXJ : X \ B' ∩ M.E ⊆ J
⊢ B'' ∩ X ⊆ B'
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
R✝ I✝ X Y : Set α
inst✝ : M.Finitary
R I : Set α
hI : ∀ J ⊆ I, J.Finite → M.Indep J ∧ J ⊆ R
e : α
heI : e ∈ I
⊢ {e} ⊆ I

Tactic:
by simpa

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

Goal state before:
pp: α : Type u_1
M : Matroid α
E B I✝ X R J I : Set α
h : ∀ J ⊆ I, J.Finite → J ⊆ E
e : α
heI : e ∈ I
⊢ {e} ⊆ I

Tactic:
by simpa

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

Goal state before:
pp: α : Type u_1
E : Set α
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug :
  ∀ ⦃I J : Set α⦄, Indep I → I.Finite → Indep J → J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
⊢ ∀ (I : Set α),
    (∀ J ⊆ I,
        J.Finite →
          (IndepMatroid.ofFinitaryCardAugment E Indep indep_empty indep_subset indep_aug indep_compact
                  subset_ground).matroid.Indep
            J) →
      (IndepMatroid.ofFinitaryCardAugment E Indep indep_empty indep_subset indep_aug indep_compact
              subset_ground).matroid.Indep
        I

Tactic:
by simpa

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

Goal state before:
pp: α : Type u_1
M✝ : Matroid α
I B X : Set α
M : Matroid α
⊢ ∀ X ⊆ M.E, ExistsMaximalSubsetProperty (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) X

Tactic:
by
    rintro X - I' ⟨hI'E, B, hB, hI'B⟩ hI'X
    obtain ⟨I, hI⟩ := M.exists_isBasis (M.E \ X)
    obtain ⟨B', hB', hIB', hB'IB⟩ := hI.indep.exists_isBase_subset_union_isBase hB
    obtain rfl : I = B' \ X := hI.eq_of_subset_indep (hB'.indep.sdiff _)
      (subset_sdiff.2 ⟨hIB', (subset_sdiff.1 hI.subset).2⟩)
      (sdiff_subset_sdiff_left hB'.subset_ground)
    simp_rw [maximal_subset_iff']
    refine ⟨(X \ B') ∩ M.E, ?_, ⟨⟨inter_subset_right, ?_⟩, ?_⟩, ?_⟩
    · rw [subset_inter_iff, and_iff_left hI'E, subset_sdiff, and_iff_right hI'X]
      exact Disjoint.mono_right hB'IB <| disjoint_union_right.2
        ⟨disjoint_sdiff_right.mono_left hI'X, hI'B⟩
    · exact ⟨B', hB', (disjoint_sdiff_left (t := X)).mono_left inter_subset_left⟩
    · exact inter_subset_left.trans sdiff_subset
    simp only [subset_inter_iff, subset_sdiff, and_imp, forall_exists_index]
    refine fun J hJE B'' hB'' hdj hJX hXJ ↦ ⟨⟨hJX, ?_⟩, hJE⟩
    have hI' : (B'' ∩ X) ∪ (B' \ X) ⊆ B' := by
      rw [union_subset_iff, and_iff_left sdiff_subset, ← union_sdiff_cancel hJX,
        inter_union_distrib_left, hdj.symm.inter_eq, empty_union, sdiff_eq, ← inter_assoc,
        ← sdiff_eq, sdiff_subset_comm, sdiff_eq, inter_assoc, ← sdiff_eq, inter_comm]
      exact subset_trans (inter_subset_inter_right _ hB''.subset_ground) hXJ
    obtain ⟨B₁, hB₁, hI'B₁, hB₁I⟩ := (hB'.indep.subset hI').exists_isBase_subset_union_isBase hB''
    rw [union_comm, ← union_assoc, union_eq_self_of_subset_right inter_subset_left] at hB₁I
    obtain rfl : B₁ = B' := by
      refine hB₁.eq_of_subset_indep hB'.indep (fun e he ↦ ?_)
      refine (hB₁I he).elim (fun heB'' ↦ ?_) (fun h ↦ h.1)
      refine (em (e ∈ X)).elim (fun heX ↦ hI' (Or.inl ⟨heB'', heX⟩)) (fun heX ↦ hIB' ?_)
      refine hI.mem_of_insert_indep ⟨hB₁.subset_ground he, heX⟩ ?_
      exact hB₁.indep.subset (insert_subset he (subset_union_right.trans hI'B₁))
    by_contra hdj'
    obtain ⟨e, heJ, heB'⟩ := not_disjoint_iff.mp hdj'
    obtain (heB'' | ⟨-, heX⟩) := hB₁I heB'
    · exact hdj.ne_of_mem heJ heB'' rfl
    exact heX (hJX heJ)

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

Goal state before:
pp: α : Type u_1
M : Matroid α
E B I X R J K : Set α
hK : ∀ J ⊆ K, J.Finite → J ⊆ I ∩ E
e : α
heK : e ∈ K
⊢ {e} ⊆ K

Tactic:
by simpa

Goal state after:
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 α
hI : N.Indep (f '' I)
hIinj : InjOn f I
hImax : ¬Maximal (fun I ↦ N.Indep (f '' I) ∧ InjOn f I) I
hBmax : Maximal (fun I ↦ N.Indep (f '' I) ∧ InjOn f I) B
I' : Set α
hII' : I ⊂ I'
hI' : N.Indep (f '' I')
hI'inj : InjOn f I'
hB : (N ↾ range f).IsBase (f '' I)
⊢ (N ↾ range f).Indep (f '' I')

Tactic:
by simpa

Goal state after:
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 α
hI : N.Indep (f '' I)
hIinj : InjOn f I
hImax : ¬Maximal (fun I ↦ N.Indep (f '' I) ∧ InjOn f I) I
hBmax : Maximal (fun I ↦ N.Indep (f '' I) ∧ InjOn f I) B
I' : Set α
hII' : I ⊂ I'
hI' : N.Indep (f '' I')
hI'inj : InjOn f I'
h₁ : ¬(N ↾ range f).IsBase (f '' I)
h₂ : (N ↾ range f).IsBase (f '' B)
⊢ (N ↾ range f).Indep (f '' I)

Tactic:
by simpa

Goal state after:
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 : α → β
X I : Set α
hI : N.Indep (f '' I)
hIinj : InjOn f I
hIX : I ⊆ X
⊢ (N ↾ range f).Indep (f '' I)

Tactic:
by simpa

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 < hJfin.toFinset.card
e : α
heJ : e ∈ J
heI : e ∉ I
hi : Indep (insert e hIfin.toFinset)
K : Finset α
hK : ↑K ⊆ insert e I
⊢ ↑K ⊆ ↑(insert e hIfin.toFinset)

Tactic:
by simpa

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
R : Set α
hIN : I ⊆ (M ↾ R).E
⊢ (M ↾ R).Indep I

Tactic:
simpa [hI]

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 : Set α
hI : ∀ (J : Finset α), ↑J ⊆ I → Indep J
x : α
hxI : x ∈ I
⊢ ↑{x} ⊆ I

Tactic:
by simpa

Goal state after:
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
⊢ (Matroid.ofExistsFiniteIsBase E IsBase ⋯ isBase_exchange subset_ground).IsBase B

Tactic:
by simpa

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

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

Tactic:
by simpa

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
h : M.IsRkFinite X
I : Set α
hI : M.IsBasis' I X
hIfin : I.Finite
⊢ M.IsBasis' (↑hIfin.toFinset) X

Tactic:
by simpa

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

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

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

Tactic:
and_iff_left sdiff_subset,

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

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

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

Tactic:
by simpa

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

Goal state before:
pp: α : Type u_1
β : Type u_2
I : Set α
M : Matroid α
X : Set α
hIX : M.IsBasis I X
f : α → β
hf : InjOn f M.E
e : α
he : e ∈ X
he' : f e ∉ f '' I
hss : insert e I ⊆ M.E
⊢ insert (f e) (f '' I) ⊆ (M.map f hf).E

Tactic:
by simpa [← image_insert_eq] using image_mono hss

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

Goal state before:
pp: α : Type u_1
M : Matroid α
C : Set α
⊢ M.IsCircuit C ↔ M.Dep C ∧ ∀ e ∈ C, M.Indep (C \ {e})

Tactic:
wlog hCE : C ⊆ M.E

Goal state after:
case inr
α : Type u_1
M : Matroid α
C : Set α
this : ∀ {α : Type u_1} {M : Matroid α} {C : Set α}, C ⊆ M.E → (M.IsCircuit C ↔ M.Dep C ∧ ∀ e ∈ C, M.Indep (C \ {e}))
hCE : ¬C ⊆ M.E
⊢ M.IsCircuit C ↔ M.Dep C ∧ ∀ e ∈ C, M.Indep (C \ {e})

α✝ : Type u_1
M✝ : Matroid α✝
C✝ : Set α✝
α : Type u_1
M : Matroid α
C : Set α
hCE : C ⊆ M.E
⊢ M.IsCircuit C ↔ M.Dep C ∧ ∀ e ∈ C, M.Indep (C \ {e})
Module: Mathlib.Combinatorics.Matroid.Circuit

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

Tactic:
by simpa

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ : Set α
M : Matroid α
N : Matroid β
inst✝ : M.Finitary
f : α → β
hf : InjOn f M.E
I : Set β
hI : ∀ J ⊆ I, J.Finite → (M.map f hf).Indep J
e : β
he : e ∈ I
⊢ {e} ⊆ I

Tactic:
by simpa

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
e : α
heX : e ∉ M.E
⊢ ∀ a ∈ X, (∀ t ⊆ X, M.closure {e} ⊆ M.closure t → a ∈ t) → a = e

Tactic:
simp_rw [← M.closure_inter_ground {e}, singleton_inter_eq_empty.2 heX]

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
e : α
heX : e ∉ M.E
⊢ ∀ a ∈ X, (∀ t ⊆ X, M.closure ∅ ⊆ M.closure t → a ∈ t) → a = e
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
⊢ I ∈ {J | J ⊆ I ∧ e ∈ M.closure J}

Tactic:
by simpa

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
aux : ⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J} ⊆ I
⊢ I ∈ {J | J ⊆ I ∧ e ∈ M.closure J}

Tactic:
by simpa

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 : ¬M.Indep {e} ∧ e ∈ M.E
B : Set α
hB : M.IsBase B
heB : e ∈ B
⊢ {e} ⊆ B

Tactic:
by simpa

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
e : α
R : Set α
hIR : I ⊆ R
heR : e ∈ R
hR : R ⊆ M.E
⊢ {e} ⊆ R

Tactic:
by simpa

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
e : α
R : Set α
hIR : I ⊆ R
heR : e ∈ R
hR : R ⊆ M.E
⊢ insert e (I ∩ ⋂₀ {J | J ⊆ I ∧ (M ↾ R).closure {e} ⊆ (M ↾ R).closure J}) =
    insert e (I ∩ ⋂₀ {J | J ⊆ I ∧ M.closure {e} ⊆ M.closure J})

Tactic:
M.restrict_closure_eq (R := R) (X := {e}) (by simpa)

Goal state after:
α : Type u_1
M : Matroid α
I : Set α
e : α
R : Set α
hIR : I ⊆ R
heR : e ∈ R
hR : R ⊆ M.E
⊢ insert e (I ∩ ⋂₀ {J | J ⊆ I ∧ M.closure {e} ∩ R ⊆ (M ↾ R).closure J}) =
    insert e (I ∩ ⋂₀ {J | J ⊆ I ∧ M.closure {e} ⊆ M.closure J})
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
⊢ ¬M.Dep I ∧ I ⊆ M.E ↔ (∀ C ⊆ I, ¬M.IsCircuit C) ∧ I ⊆ M.E

Tactic:
dep_iff_superset_isCircuit'

Goal state after:
α : Type u_1
M : Matroid α
I : Set α
⊢ ¬((∃ C ⊆ I, M.IsCircuit C) ∧ I ⊆ M.E) ∧ I ⊆ M.E ↔ (∀ C ⊆ I, ¬M.IsCircuit C) ∧ I ⊆ M.E