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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : Module.Finite R M
ι : Type u_5
f : ι → M
b : Basis ι k (k ⊗[R] M)
hb : ∀ (i : ι), 1 ⊗ₜ[R] f i = b i
⊢ Submodule.span k (Set.range (⇑((TensorProduct.mk R k M) 1) ∘ f)) = Submodule.span k (Set.range ⇑b)

Tactic:
simp only [Function.comp_def, mk_apply, hb, Basis.span_eq]

Goal state after:
Module: Mathlib.RingTheory.LocalRing.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : FinitePresentation R M
ι : Type u_5
v : ι → M
hli : LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v)
hsp : Submodule.span k (Set.range (⇑((TensorProduct.mk R k M) 1) ∘ v)) = ⊤
H : Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype 𝔪))
bk : Basis ι k (k ⊗[R] M) := Basis.mk hli ⋯
this✝¹ : Finite ι
this✝ : Fintype ι := Fintype.ofFinite ι
i : (ι →₀ R) →ₗ[R] M := Finsupp.linearCombination R v
hi : Surjective ⇑i
this : Module.Finite R ↥i.ker
⊢ (ι →₀ R) ≃ₗ[R] M

Tactic:
refine LinearEquiv.ofBijective i ⟨?_, hi⟩

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : FinitePresentation R M
ι : Type u_5
v : ι → M
hli : LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v)
hsp : Submodule.span k (Set.range (⇑((TensorProduct.mk R k M) 1) ∘ v)) = ⊤
H : Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype 𝔪))
bk : Basis ι k (k ⊗[R] M) := Basis.mk hli ⋯
this✝¹ : Finite ι
this✝ : Fintype ι := Fintype.ofFinite ι
i : (ι →₀ R) →ₗ[R] M := Finsupp.linearCombination R v
hi : Surjective ⇑i
this : Module.Finite R ↥i.ker
⊢ Function.Injective ⇑i
Module: Mathlib.LinearAlgebra.LinearDisjoint

Goal state before:
pp: 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
inst✝ : Flat R ↥N
ι : Type u_1
m : ι → ↥M
hm : LinearIndependent R m
⊢ (mulLeftMap N m).ker = ⊥

Tactic:
refine LinearMap.ker_eq_bot_of_injective ?_
  classical simp_rw [mulLeftMap_eq_mulMap_comp, LinearMap.coe_comp, LinearEquiv.coe_coe,
    ← Function.comp_assoc, EquivLike.injective_comp]
  rw [LinearIndependent] at hm
  exact H.injective.comp (Module.Flat.rTensor_preserves_injective_linearMap (M := N) _ hm)

Goal state after:
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
x : ⨂[R] (i : ι), s i
⊢ Quot.out x ∈ x.lifts

Tactic:
simp [lifts, ← AddCon.quot_mk_eq_coe]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I J : Ideal R
hI : I.IsPrimary
hJ : J.IsPrime
x : R
e : J = (⊥.colon {(Ideal.Quotient.mkₐ R I) x}).radical
this : x ∉ I
h : ∀ {y : R}, y ∈ ⊥.colon {(Ideal.Quotient.mk I) x} ↔ y * x ∈ I
y : R
hy : y ∈ ⊥.colon {(Ideal.Quotient.mk I) x}
⊢ y ∈ I.radical

Tactic:
← I.colon_univ,

Goal state after:
R : Type u_1
inst✝ : CommRing R
I J : Ideal R
hI : I.IsPrimary
hJ : J.IsPrime
x : R
e : J = (⊥.colon {(Ideal.Quotient.mkₐ R I) x}).radical
this : x ∉ I
h : ∀ {y : R}, y ∈ ⊥.colon {(Ideal.Quotient.mk I) x} ↔ y * x ∈ I
y : R
hy : y ∈ ⊥.colon {(Ideal.Quotient.mk I) x}
⊢ y ∈ (colon I Set.univ).radical
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 ∈ span ↑J * span ↑T

Tactic:
span_mul_span

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 * ↑T)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsGCDMonoid R
I : Ideal R
hI : IsUnit ↑I
a : R
K : Ideal R
ha0 : a ≠ 0
h : (↑I)⁻¹ = spanSingleton R⁰ ((algebraMap R (FractionRing R)) a)⁻¹ * ↑K
hIK : I * K = span {a}
⊢ Submodule.IsPrincipal I

Tactic:
refine isPrincipal_of_exists_mul_ne_zero_isPrincipal (J := I) ?_

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsGCDMonoid R
I : Ideal R
hI : IsUnit ↑I
a : R
K : Ideal R
ha0 : a ≠ 0
h : (↑I)⁻¹ = spanSingleton R⁰ ((algebraMap R (FractionRing R)) a)⁻¹ * ↑K
hIK : I * K = span {a}
⊢ ∃ K, I * K ≠ 0 ∧ Submodule.IsPrincipal (I * K)
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

Tactic:
replace hx : s ∈ q₁.1.asIdeal := by simpa using! 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
hr : r ∉ p.asIdeal
s : S
e : r • x = 1 ⊗ₜ[R] s
hx : s ∈ (↑q₁).asIdeal
⊢ 1 ⊗ₜ[R] s ∈ ((preimageEquivFiber R S p) q₂).asIdeal
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
⊢ Free R M ↔ Nonempty (M ≃ₗ[R] R)

Tactic:
refine ⟨fun _ ↦ ?_, fun ⟨e⟩ ↦ .of_equiv e.symm⟩

Goal state after:
R : Type u
M : Type v
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Invertible R M
x✝ : Free R M
⊢ Nonempty (M ≃ₗ[R] R)
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
inst✝ : Free R M
⊢ finrank R M = 1

Tactic:
by
  rw [(free_iff_linearEquiv.mp ‹_›).some.finrank_eq, CommSemiring.finrank_self]

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
M' : Type u := Finite.reprₛ R M
⊢ ⟦SemimoduleCat.of R M'⟧ * ⟦SemimoduleCat.of R (Dual R M')⟧ = 1

Tactic:
by
    rw [← toSkeleton, ← toSkeleton, mul_comm, ← Skeleton.toSkeleton_tensorObj]
    exact Quotient.sound ⟨(Invertible.linearEquiv R _).toModuleIsoₛ⟩

Goal state after:
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
M : Pic R
⊢ M⁻¹ = Pic.mk R (Dual R M.AsModule)

Tactic:
rw [mk_dual, mk_eq_self]

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

Goal state before:
pp: F : Type u_1
L : Type u_3
inst✝³ : Field F
inst✝² : Field L
inst✝¹ : Algebra F L
inst✝ : Normal F L
K : IntermediateField F L
⊢ Normal F ↥K ↔ ∀ (σ : ↥K →ₐ[F] L), σ.fieldRange ≤ K

Tactic:
by
  rw [normal_iff_normalClosure_le, normalClosure_def, iSup_le_iff]

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
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra F L
S : Set K
splits : ∀ x ∈ S, IsIntegral F x ∧ (Polynomial.map (algebraMap F L) (minpoly F x)).Splits
x : K
hx : x ∈ adjoin F S
E : IntermediateField F L := ⨆ x, adjoin F ((minpoly F ↑x).rootSet L)
⊢ (Polynomial.map (algebraMap F L) (minpoly F x)).Splits

Tactic:
have normal : Normal F E := normal_iSup (h := fun x ↦
    Normal.of_isSplittingField (hFEp := adjoin_rootSet_isSplittingField (splits x x.2).2))

Goal state after:
F : Type u_1
K : Type u_2
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Algebra F K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra F L
S : Set K
splits : ∀ x ∈ S, IsIntegral F x ∧ (Polynomial.map (algebraMap F L) (minpoly F x)).Splits
x : K
hx : x ∈ adjoin F S
E : IntermediateField F L := ⨆ x, adjoin F ((minpoly F ↑x).rootSet L)
normal : Normal F ↥E
⊢ (Polynomial.map (algebraMap F L) (minpoly F x)).Splits
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
⊢ I ⊆ M.E

Tactic:
obtain ⟨B, hB, hIB⟩ := hI.exists_isBase_superset
  exact hIB.trans hB.subset_ground

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

Goal state before:
pp: α : Type u_1
M✝ : Matroid α
B✝ B'✝ I✝ J D X : Set α
e f : α
M : Matroid α
inst✝ : M.RankFinite
I : Set α
hI : ∀ J ⊆ I, J.Finite → M.Indep J
h : I.Infinite
B : Set α
hB : M.IsBase B
I₀ : Set α
hI₀I : I₀ ⊆ I
hI₀fin : I₀.Finite
hI₀card : I₀.ncard = B.ncard + 1
B' : Set α
hB' : M.IsBase B'
hI₀B' : I₀ ⊆ B'
hle : B.ncard + 1 ≤ B.ncard
⊢ False

Tactic:
Nat.add_one_le_iff

Goal state after:
α : Type u_1
M✝ : Matroid α
B✝ B'✝ I✝ J D X : Set α
e f : α
M : Matroid α
inst✝ : M.RankFinite
I : Set α
hI : ∀ J ⊆ I, J.Finite → M.Indep J
h : I.Infinite
B : Set α
hB : M.IsBase B
I₀ : Set α
hI₀I : I₀ ⊆ I
hI₀fin : I₀.Finite
hI₀card : I₀.ncard = B.ncard + 1
B' : Set α
hB' : M.IsBase B'
hI₀B' : I₀ ⊆ B'
hle : B.ncard < B.ncard
⊢ False
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
A : Type u_4
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
x : Aˣ
⊢ (LinearMap.toSpanSingleton R A ↑x).range = ↑((Units.map ↑(spanSingleton R)) x)

Tactic:
ext; simp [mem_span_singleton]

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
htofin : ∀ (I : Set α) (e : α), Indep I → ¬Indep (insert e I) → ∃ I₀ ⊆ I, I₀.Finite ∧ ¬Indep (insert e I₀)
I B : Set α
hI : Indep I
hImax : ¬Maximal Indep I
hBmax : Maximal Indep B
e : α
heI : e ∉ I
hins : Indep (insert e I)
heB : e ∉ B
hcon : ∀ x ∈ B \ I, ¬Indep (insert x I)
heBdep : ¬Indep (insert e B)
B₀ : Set α
hB₀B : B₀ ⊆ B
hB₀fin : B₀.Finite
hB₀e : ¬Indep (insert e B₀)
hB₀ : Indep B₀
f : ↑(B₀ \ I) → Set α
hf : ∀ (b : ↑(B₀ \ I)), f b ⊆ I ∧ (f b).Finite ∧ ¬Indep (insert (↑b) (f b))
this : Finite ↑(B₀ \ I)
x : α
x✝ : x ∈ B₀ \ (iUnion f ∪ B₀ ∩ I)
hi : Indep (insert x (iUnion f ∪ B₀ ∩ I))
hxB₀ : x ∈ B₀
hxn : x ∉ iUnion f ∪ B₀ ∩ I
⊢ False

Tactic:
have hxI : x ∉ I := fun hxI ↦ hxn <| Or.inr ⟨hxB₀, hxI⟩

Goal state after:
α : 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
htofin : ∀ (I : Set α) (e : α), Indep I → ¬Indep (insert e I) → ∃ I₀ ⊆ I, I₀.Finite ∧ ¬Indep (insert e I₀)
I B : Set α
hI : Indep I
hImax : ¬Maximal Indep I
hBmax : Maximal Indep B
e : α
heI : e ∉ I
hins : Indep (insert e I)
heB : e ∉ B
hcon : ∀ x ∈ B \ I, ¬Indep (insert x I)
heBdep : ¬Indep (insert e B)
B₀ : Set α
hB₀B : B₀ ⊆ B
hB₀fin : B₀.Finite
hB₀e : ¬Indep (insert e B₀)
hB₀ : Indep B₀
f : ↑(B₀ \ I) → Set α
hf : ∀ (b : ↑(B₀ \ I)), f b ⊆ I ∧ (f b).Finite ∧ ¬Indep (insert (↑b) (f b))
this : Finite ↑(B₀ \ I)
x : α
x✝ : x ∈ B₀ \ (iUnion f ∪ B₀ ∩ I)
hi : Indep (insert x (iUnion f ∪ B₀ ∩ I))
hxB₀ : x ∈ B₀
hxn : x ∉ iUnion f ∪ B₀ ∩ I
hxI : x ∉ I
⊢ False
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
ι : Type u_2
inst✝ : Nonempty ι
X : ι → Set α
hI : ∀ (i : ι), M.IsBasis I (X i)
⊢ M.Indep I

Tactic:
exact (hI (Classical.arbitrary ι)).indep

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

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

Tactic:
by rw [← h]; rfl

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 → Indep J → I.encard < J.encard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
indep_bdd : ∃ n, ∀ (I : Set α), Indep I → I.encard ≤ ↑n
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
I B : Set α
hI : Indep I
hImax : ¬Maximal Indep I
hBmax : Maximal Indep B
hcard : I.encard < B.encard
e : α
heB : e ∈ B
heI : e ∉ I
hi : Indep (insert e I)
⊢ ∃ x ∈ B \ I, Indep (insert x I)

Tactic:
exact ⟨e, ⟨heB, heI⟩, hi⟩

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
J : Set β
hIJ : I ⊆ f ⁻¹' J
hJ : N.Indep J
hJf : J ⊆ range f
hJX : J ⊆ f '' X
hJmax : ∀ ⦃t : Set β⦄, N.Indep t → t ⊆ range f → t ⊆ f '' X → J ⊆ t → J = t
⊢ ∃ J,
    I ⊆ J ∧ N.Indep (f '' J) ∧ InjOn f J ∧ J ⊆ X ∧ ∀ ⦃t : Set α⦄, N.Indep (f '' t) → InjOn f t → t ⊆ X → J ⊆ t → J = t

Tactic:
obtain ⟨J₀, hIJ₀, hJ₀X, hbj⟩ := hIinj.bijOn_image.exists_extend_of_subset hIX
        (image_mono hIJ) (image_subset_iff.2 <| preimage_mono hJX)

Goal state after:
α : 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
J : Set β
hIJ : I ⊆ f ⁻¹' J
hJ : N.Indep J
hJf : J ⊆ range f
hJX : J ⊆ f '' X
hJmax : ∀ ⦃t : Set β⦄, N.Indep t → t ⊆ range f → t ⊆ f '' X → J ⊆ t → J = t
J₀ : Set α
hIJ₀ : I ⊆ J₀
hJ₀X : J₀ ⊆ X
hbj : BijOn f J₀ (f '' f ⁻¹' J)
⊢ ∃ J,
    I ⊆ J ∧ N.Indep (f '' J) ∧ InjOn f J ∧ J ⊆ X ∧ ∀ ⦃t : Set α⦄, N.Indep (f '' t) → InjOn f t → t ⊆ X → J ⊆ t → J = t
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
I : Set α
N : Matroid β
hf : InjOn f (f ⁻¹' N.E)
⊢ (N.comap f).Indep I ↔ N.Indep (f '' I)

Tactic:
rw [comap_indep_iff, and_iff_left_iff_imp]
  refine fun hi ↦ hf.mono <| subset_trans ?_ (preimage_mono hi.subset_ground)
  apply subset_preimage_image

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Matroid α
f : α → β
hf : InjOn f M.E
B : Set β
⊢ (M.map f hf).IsBase B ↔ ∃ B₀, M.IsBase B₀ ∧ B = f '' B₀

Tactic:
rw [isBase_iff_maximal_indep]
  refine ⟨fun h ↦ ?_, ?_⟩
  · obtain ⟨B₀, hB₀, hbij⟩ := h.prop.exists_bijOn_of_map
    refine ⟨B₀, hB₀.isBase_of_maximal fun J hJ hB₀J ↦ ?_, hbij.image_eq.symm⟩
    rw [← hf.image_eq_image_iff hB₀.subset_ground hJ.subset_ground, hbij.image_eq]
    exact h.eq_of_subset (hJ.map f hf) (hbij.image_eq ▸ image_mono hB₀J)
  rintro ⟨B, hB, rfl⟩
  rw [maximal_subset_iff]
  refine ⟨hB.indep.map f hf, fun I hI hBI ↦ ?_⟩
  obtain ⟨I₀, hI₀, hbij⟩ := hI.exists_bijOn_of_map
  rw [← hbij.image_eq, hf.image_subset_image_iff hB.subset_ground hI₀.subset_ground] at hBI
  rw [hB.eq_of_subset_indep hI₀ hBI, hbij.image_eq]

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:
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 α
e : α
hC : M.IsCircuit C
he : e ∈ C
⊢ M.IsBasis (C \ {e}) C

Tactic:
← insert_eq_of_mem he

Goal state after:
α : Type u_1
M : Matroid α
C : Set α
e : α
hC : M.IsCircuit C
he : e ∈ C
⊢ M.IsBasis (C \ {e}) (insert e C)
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
C I : Set α
hC : M.IsCircuit C
h : M.IsBasis I C
⊢ I ≠ C

Tactic:
by rintro rfl; exact hC.dep.not_indep h.indep

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
I X : Set β
⊢ (M.mapEmbedding f).IsBasis I X ↔ M.IsBasis (⇑f ⁻¹' I) (⇑f ⁻¹' X) ∧ I ⊆ X ∧ X ⊆ range ⇑f

Tactic:
rw [mapEmbedding, map_isBasis_iff']
  refine ⟨?_, fun ⟨hb, hIX, hX⟩ ↦ ?_⟩
  · rintro ⟨I, X, hIX, rfl, rfl⟩
    simp [preimage_image_eq _ f.injective, image_mono hIX.subset, hIX]
  obtain ⟨X, rfl⟩ := subset_range_iff_exists_image_eq.1 hX
  obtain ⟨I, -, rfl⟩ := subset_image_iff.1 hIX
  exact ⟨I, X, by simpa [preimage_image_eq _ f.injective] using hb⟩

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

Goal state before:
pp: case h₂
α : Type u_1
M : Matroid α
I : Set α
e : α
R : Set α
hIR : I ⊆ R
heR : e ∈ R
hR : R ⊆ M.E
J : Set α
hJI : J ⊆ I
⊢ M.closure {e} ⊆ M.closure J → M.closure {e} ∩ R ⊆ (M ↾ R).closure J

Tactic:
intro heJ

Goal state after:
case h₂
α : Type u_1
M : Matroid α
I : Set α
e : α
R : Set α
hIR : I ⊆ R
heR : e ∈ R
hR : R ⊆ M.E
J : Set α
hJI : J ⊆ I
heJ : M.closure {e} ⊆ M.closure J
⊢ M.closure {e} ∩ R ⊆ (M ↾ R).closure J
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: case h₂
α : Type u_1
M : Matroid α
I : Set α
e : α
R : Set α
hIR : I ⊆ R
heR : e ∈ R
hR : R ⊆ M.E
J : Set α
hJI : J ⊆ I
⊢ M.closure {e} ∩ R ⊆ (M ↾ R).closure J → M.closure {e} ⊆ M.closure J

Tactic:
intro heJ

Goal state after:
case h₂
α : Type u_1
M : Matroid α
I : Set α
e : α
R : Set α
hIR : I ⊆ R
heR : e ∈ R
hR : R ⊆ M.E
J : Set α
hJI : J ⊆ I
heJ : M.closure {e} ∩ R ⊆ (M ↾ R).closure J
⊢ M.closure {e} ⊆ M.closure J
Module: Mathlib.Combinatorics.Matroid.Loop

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

Tactic:
← singleton_isCircuit

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

Goal state before:
pp: case inr.inr
α : Type u_1
M : Matroid α
e : α
he : M.IsNonloop e
x : α
hf : M.IsNonloop x
hne : e ≠ x
hi : ¬M.Indep {e, x}
⊢ M.Indep ({e, x} \ {x})

Tactic:
rwa [pair_sdiff_right hne, indep_singleton]

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

Goal state before:
pp: α : Type u_2
M : Matroid α
X : Set α
⊢ M.closure (X ∩ M.E) = M.closure X

Tactic:
closure_def,

Goal state after:
α : Type u_2
M : Matroid α
X : Set α
⊢ ⋂₀ {F | M.IsFlat F ∧ X ∩ M.E ∩ M.E ⊆ F} = ⋂₀ {F | M.IsFlat F ∧ X ∩ M.E ⊆ F}
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
X : Set α
⊢ X ∩ M.E ⊆ M.closure X

Tactic:
closure_def,

Goal state after:
α : Type u_2
M : Matroid α
X : Set α
⊢ X ∩ M.E ⊆ ⋂₀ {F | M.IsFlat F ∧ X ∩ M.E ⊆ F}
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
I : Set α
hI : M.Indep I
F : Set α := {x | M.IsBasis I (insert x I)}
hIF : M.IsBasis I F
hF : M.IsFlat F
⊢ M.closure I ⊆ F ∧ F ⊆ M.closure I

Tactic:
closure_def,

Goal state after:
α : Type u_2
M : Matroid α
I : Set α
hI : M.Indep I
F : Set α := {x | M.IsBasis I (insert x I)}
hIF : M.IsBasis I F
hF : M.IsFlat F
⊢ ⋂₀ {F | M.IsFlat F ∧ I ∩ M.E ⊆ F} ⊆ F ∧ F ⊆ ⋂₀ {F | M.IsFlat F ∧ I ∩ M.E ⊆ F}
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α✝ : Type u_1
M✝ : Matroid α✝
e✝ : α✝
α : Type u_1
M : Matroid α
e : α
R : Set α
hRE : R ⊆ M.E
heR : e ∈ R
⊢ (∀ ⦃C : Set α⦄, (M ↾ R).IsCircuit C → e ∉ C) ↔ (¬∃ C ⊆ insert e (R \ {e}), M.IsCircuit C ∧ e ∈ C) ∧ e ∈ R

Tactic:
simp only [restrict_isCircuit_iff hRE, insert_sdiff_singleton]

Goal state after:
α✝ : Type u_1
M✝ : Matroid α✝
e✝ : α✝
α : Type u_1
M : Matroid α
e : α
R : Set α
hRE : R ⊆ M.E
heR : e ∈ R
⊢ (∀ ⦃C : Set α⦄, M.IsCircuit C ∧ C ⊆ R → e ∉ C) ↔ (¬∃ C ⊆ insert e R, M.IsCircuit C ∧ e ∈ C) ∧ e ∈ R
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
I : Set α
x : α
hI : M.Indep I
⊢ x ∈ M.closure I ↔ x ∈ M.E ∧ (M.Indep (insert x I) → x ∈ I)

Tactic:
by
  rw [hI.mem_closure_iff, dep_iff, insert_subset_iff, and_iff_left hI.subset_ground,
    imp_iff_not_or]
  have := hI.subset_ground
  aesop

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

Goal state before:
pp: α : Type u_1
M : Matroid α
K x✝ : Set α
⊢ M✶.Dep x✝ ↔ (∀ (B : Set α), M.IsBase B → (x✝ ∩ B).Nonempty) ∧ x✝ ⊆ M.E

Tactic:
apply dual_dep_iff_forall

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

Goal state before:
pp: case pos
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
⊢ e ∈ M.E \ M.closure I ∨ e ∈ I ↔ e ∉ I → e ∈ M.E \ M.closure I

Tactic:
or_iff_not_imp_right

Goal state after:
case pos
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
⊢ e ∉ I → e ∈ M.E \ M.closure I ↔ e ∉ I → e ∈ M.E \ M.closure I
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
K : Set α
⊢ Minimal (fun X ↦ ¬M.Spanning (M.E \ X)) K ↔ Minimal (fun X ↦ ¬M.Spanning (M.E \ X) ∧ X ⊆ M.E) K

Tactic:
exact minimal_iff_minimal_of_imp_of_forall (fun _ h ↦ h.1)
    (fun X hX ↦ ⟨X ∩ M.E, inter_subset_left, by rwa [sdiff_inter_self_eq_sdiff],
      inter_subset_right⟩)

Goal state after:
Module: Mathlib.RingTheory.Algebraic.MvPolynomial

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommRing R
i : σ
s : Set σ
h : i ∉ s
f : R[X]
g : MvPolynomial (↑s) R[X] →ₐ[R] MvPolynomial (↑s) R[X] := mapAlgHom (Polynomial.aeval f)
hf : Function.Injective ⇑g
⊢ Function.Injective ⇑(Polynomial.aeval ((Polynomial.aeval (X i)) f))

Tactic:
let u := (Subalgebra.val _).comp
    ((optionEquivRight R s).symm |>.trans
      (renameEquiv R (Set.subtypeInsertEquivOption h).symm) |>.trans
      (supportedEquivMvPolynomial _).symm).toAlgHom |>.comp
    g |>.comp
    ((optionEquivLeft R s).symm.trans (optionEquivRight R s)).toAlgHom

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommRing R
i : σ
s : Set σ
h : i ∉ s
f : R[X]
g : MvPolynomial (↑s) R[X] →ₐ[R] MvPolynomial (↑s) R[X] := mapAlgHom (Polynomial.aeval f)
hf : Function.Injective ⇑g
u : (MvPolynomial (↑s) R)[X] →ₐ[R] MvPolynomial σ R :=
  (((supported R (insert i s)).val.comp
            ↑(((optionEquivRight R ↑s).symm.trans (renameEquiv R (Set.subtypeInsertEquivOption h).symm)).trans
                (supportedEquivMvPolynomial (insert i s)).symm)).comp
        g).comp
    ↑((optionEquivLeft R ↑s).symm.trans (optionEquivRight R ↑s))
⊢ Function.Injective ⇑(Polynomial.aeval ((Polynomial.aeval (X i)) f))
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
C K : Set α
hC : M.IsCircuit C
hK : M.IsCocircuit K
e : α
heCK : e ∈ C ∩ K
⊢ C ∩ K ≠ {e}

Tactic:
exact hC.inter_isCocircuit_ne_singleton hK

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

Goal state before:
pp: α : Type u_2
M : Matroid α
X I : Set α
⊢ M.IsBasis' I X ↔ M.IsBasis I (M.closure X) ∧ I ⊆ X

Tactic:
by
  rw [← closure_inter_ground, isBasis'_iff_isBasis_inter_ground]
  exact ⟨fun h ↦ ⟨h.isBasis_closure_right, h.subset.trans inter_subset_left⟩,
    fun h ↦ h.1.isBasis_subset (subset_inter h.2 h.1.indep.subset_ground) (M.subset_closure _)⟩

Goal state after: