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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
x : GradedMonoid fun i ↦ ⨂[R]^i M
this :
  (cast R M ⋯) (GradedMonoid.GMul.mul (algebraMap₀ r) x.snd) =
    (cast R M ⋯) (GradedMonoid.GMul.mul x.snd (algebraMap₀ r))
⊢ (GradedMonoid.mk 0 ((↑algebraMap₀).toAddMonoidHom r) * x).snd =
    (cast R M ⋯) (x * GradedMonoid.mk 0 ((↑algebraMap₀).toAddMonoidHom r)).snd

Tactic:
rw [← LinearEquiv.eq_symm_apply, cast_symm, cast_cast] at this

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
x : GradedMonoid fun i ↦ ⨂[R]^i M
this : GradedMonoid.GMul.mul (algebraMap₀ r) x.snd = (cast R M ⋯) (GradedMonoid.GMul.mul x.snd (algebraMap₀ r))
⊢ (GradedMonoid.mk 0 ((↑algebraMap₀).toAddMonoidHom r) * x).snd =
    (cast R M ⋯) (x * GradedMonoid.mk 0 ((↑algebraMap₀).toAddMonoidHom r)).snd
Module: Mathlib.RingTheory.LocalRing.Module

Goal state before:
pp: case mp
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R M
inst✝¹ : Module.Finite R N
inst✝ : Free R N
l : M →ₗ[R] N
⊢ (∃ l', l' ∘ₗ l = LinearMap.id) → Function.Injective ⇑(LinearMap.lTensor k l)

Tactic:
intro ⟨l', hl⟩

Goal state after:
case mp
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R M
inst✝¹ : Module.Finite R N
inst✝ : Free R N
l : M →ₗ[R] N
l' : N →ₗ[R] M
hl : l' ∘ₗ l = LinearMap.id
⊢ Function.Injective ⇑(LinearMap.lTensor k l)
Module: Mathlib.RingTheory.LocalRing.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R M
inst✝¹ : Module.Finite R N
inst✝ : Free R N
l : M →ₗ[R] N
h : Function.Injective ⇑(LinearMap.lTensor k l)
this✝¹ : Free R (N ⧸ l.range)
this✝ : Projective R ↥l.range
l' : M →ₗ[R] ↥l.ker
hl' : l' ∘ₗ l.ker.subtype = LinearMap.id
this : Module.Finite R ↥l.ker
H : Function.Injective ⇑(LinearMap.lTensor k l.ker.subtype)
⊢ Subsingleton (k ⊗[R] ↥l.ker)

Tactic:
refine (subsingleton_iff_forall_eq 0).mpr fun y ↦ H (h ?_)

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R M
inst✝¹ : Module.Finite R N
inst✝ : Free R N
l : M →ₗ[R] N
h : Function.Injective ⇑(LinearMap.lTensor k l)
this✝¹ : Free R (N ⧸ l.range)
this✝ : Projective R ↥l.range
l' : M →ₗ[R] ↥l.ker
hl' : l' ∘ₗ l.ker.subtype = LinearMap.id
this : Module.Finite R ↥l.ker
H : Function.Injective ⇑(LinearMap.lTensor k l.ker.subtype)
y : k ⊗[R] ↥l.ker
⊢ (LinearMap.lTensor k l) ((LinearMap.lTensor k l.ker.subtype) y) =
    (LinearMap.lTensor k l) ((LinearMap.lTensor k l.ker.subtype) 0)
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
I : Ideal R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherianRing R
⊢ I.IsPrime → ((∃ x, I = ⊥.colon {x}) ↔ ∃ f, Function.Injective ⇑f)

Tactic:
refine fun _ ↦ ⟨fun ⟨x, h⟩ ↦ ?_, fun ⟨f, h⟩ ↦ ⟨(f ∘ₗ mkQ I) 1, ?_⟩⟩

Goal state after:
case refine_1
R : Type u_1
inst✝³ : CommRing R
I : Ideal R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherianRing R
x✝¹ : I.IsPrime
x✝ : ∃ x, I = ⊥.colon {x}
x : M
h : I = ⊥.colon {x}
⊢ ∃ f, Function.Injective ⇑f

case refine_2
R : Type u_1
inst✝³ : CommRing R
I : Ideal R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherianRing R
x✝¹ : I.IsPrime
x✝ : ∃ f, Function.Injective ⇑f
f : R ⧸ I →ₗ[R] M
h : Function.Injective ⇑f
⊢ I = ⊥.colon {(f ∘ₗ mkQ I) 1}
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
⊢ ∃ T, ↑T ⊆ ↑K ∧ x ∈ J * span ↑T

Tactic:
obtain ⟨S, T, hSJ, hTK, hx⟩ := Submodule.mem_span_mul_finite_of_mem_mul hxmemJK

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)
⊢ ∃ T, ↑T ⊆ ↑K ∧ x ∈ J * span ↑T
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness

Goal state before:
pp: 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 : motive ↥s.last
⊢ motive M

Tactic:
hs2

Goal state after:
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 : motive ↥⊤
⊢ motive M
Module: Mathlib.RingTheory.Spectrum.Prime.TensorProduct

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing T
inst✝ : Algebra R T
hRT : (algebraMap R T).SurjectiveOnStalks
g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom
f : S ⊗[R] T
J : PrimeSpectrum (S ⊗[R] T)
hJ : f ∉ J.asIdeal
⊢ ∃ t ⊆ ↑(basicOpen f), IsOpen[TopologicalSpace.induced (tensorProductTo R S T) instTopologicalSpaceProd] t ∧ J ∈ t

Tactic:
obtain ⟨t, r, a, ht, e⟩ := hRT.exists_mul_eq_tmul f
    (J.asIdeal.comap g) inferInstance

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing T
inst✝ : Algebra R T
hRT : (algebraMap R T).SurjectiveOnStalks
g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom
f : S ⊗[R] T
J : PrimeSpectrum (S ⊗[R] T)
hJ : f ∉ J.asIdeal
t : T
r : R
a : S
ht : r • t ∉ Ideal.comap g J.asIdeal
e : 1 ⊗ₜ[R] (r • t) * f = a ⊗ₜ[R] t
⊢ ∃ t ⊆ ↑(basicOpen f), IsOpen[TopologicalSpace.induced (tensorProductTo R S T) instTopologicalSpaceProd] t ∧ J ∈ t
Module: Mathlib.RingTheory.LocalRing.ResidueField.Fiber

Goal state before:
pp: case mp
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₂ : PrimeSpectrum (p.asIdeal.Fiber S)
⊢ (preimageEquivFiber R S p) ((preimageEquivFiber R S p).symm q₁) ≤
      (preimageEquivFiber R S p) ((preimageEquivFiber R S p).symm q₂) →
    (preimageEquivFiber R S p).symm q₁ ≤ (preimageEquivFiber R S p).symm q₂

Tactic:
simpa using! Ideal.comap_mono

Goal state after:
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: case zero
G : Type u_1
inst✝¹ : Group G
inst✝ : Nontrivial G
hn : _root_.commutator G = ⊤
⊢ derivedSeries G 0 = ⊤

Tactic:
exact derivedSeries_zero G

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
N : Type (max v u) := Dual R M
e : M ⊗[R] N ≃ₗ[R] R := TensorProduct.comm R M N ≪≫ₗ linearEquiv R M
S : Finset (M × N)
hS : e.symm 1 = ∑ i ∈ S, i.1 ⊗ₜ[R] i.2
f : (↥S →₀ N) →ₗ[R] R := (Finsupp.lsum R) fun i ↦ ↑e ∘ₗ (TensorProduct.mk R M N) (↑i).1
this : Function.Surjective ⇑f
⊢ Module.Finite R M ∧ Projective R M

Tactic:
have ⟨g, hg⟩ := projective_lifting_property f .id this

Goal state after:
R : Type u
M : Type v
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Invertible R M
N : Type (max v u) := Dual R M
e : M ⊗[R] N ≃ₗ[R] R := TensorProduct.comm R M N ≪≫ₗ linearEquiv R M
S : Finset (M × N)
hS : e.symm 1 = ∑ i ∈ S, i.1 ⊗ₜ[R] i.2
f : (↥S →₀ N) →ₗ[R] R := (Finsupp.lsum R) fun i ↦ ↑e ∘ₗ (TensorProduct.mk R M N) (↑i).1
this : Function.Surjective ⇑f
g : R →ₗ[R] ↥S →₀ N
hg : f ∘ₗ g = LinearMap.id
⊢ Module.Finite R M ∧ Projective R M
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
Mₛ : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : AddCommGroup Mₛ
inst✝² : Module R Mₛ
inst✝¹ : Module S Mₛ
inst✝ : IsScalarTower R S Mₛ
f : M →ₗ[R] Mₛ
hf : IsBaseChange S f
p : PrimeSpectrum S
⊢ rankAtStalk Mₛ p = rankAtStalk M (comap (algebraMap R S) p)

Tactic:
simp [rankAtStalk_eq_of_equiv hf.equiv.symm, rankAtStalk_baseChange]

Goal state after:
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: F : Type u_1
inst✝² : Field F
inst✝¹ : Infinite F
E : Type u_2
inst✝ : Field E
ϕ : F →+* E
α β : E
f g : F[X]
sf : Multiset E := (Polynomial.map ϕ f).roots
sg : Multiset E := (Polynomial.map ϕ g).roots
⊢ ∃ c, ∀ α' ∈ (Polynomial.map ϕ f).roots, ∀ β' ∈ (Polynomial.map ϕ g).roots, -(α' - α) / (β' - β) ≠ ϕ c

Tactic:
classical
  let s := (sf.bind fun α' => sg.map fun β' => -(α' - α) / (β' - β)).toFinset
  let s' := s.preimage ϕ fun x _ y _ h => ϕ.injective h
  obtain ⟨c, hc⟩ := Infinite.exists_notMem_finset s'
  simp_rw [s', s, Finset.mem_preimage, Multiset.mem_toFinset, Multiset.mem_bind, Multiset.mem_map]
    at hc
  push Not at hc
  exact ⟨c, hc⟩

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
hE : E ≤ ⨆ i, t i
this : (Polynomial.map (algebraMap F ↥E) (minpoly F ↑⟨↑x, hx⟩)).Splits
⊢ (Polynomial.map (algebraMap F ↥(⨆ i, t i)) (minpoly F x)).Splits

Tactic:
Subtype.coe_mk,

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
hE : E ≤ ⨆ i, t i
this : (Polynomial.map (algebraMap F ↥E) (minpoly F ↑x)).Splits
⊢ (Polynomial.map (algebraMap F ↥(⨆ i, t i)) (minpoly F x)).Splits
Module: Mathlib.FieldTheory.Normal.Basic

Goal state before:
pp: case h
K : Type u_6
L : Type u_7
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Normal K L
x y : L
hy : IsAlgebraic K y
h_ev : (Polynomial.aeval x) (minpoly K y) = 0
σ : Gal(L/K)
hσ : σ x = y
⊢ σ.symm (σ x) = x

Tactic:
symm_apply_apply

Goal state after:
case h
K : Type u_6
L : Type u_7
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Normal K L
x y : L
hy : IsAlgebraic K y
h_ev : (Polynomial.aeval x) (minpoly K y) = 0
σ : Gal(L/K)
hσ : σ x = y
⊢ x = x
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
B X : Set α
hX : X ⊆ M.E
hB : M.IsBase B
hBX : B ⊆ X
⊢ M.IsBasis B X

Tactic:
rw [isBasis_iff, and_iff_right hB.indep, and_iff_right hBX]
  exact fun J hJ hBJ _ ↦ hB.eq_of_subset_indep hJ hBJ

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

Goal state before:
pp: α : Type u_1
E : Set α
hE : E.Finite
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.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
subset_ground : ∀ ⦃I : Set α⦄, Indep I → I ⊆ E
I : Set α
hI : Indep I
⊢ I.encard ≤ ↑E.ncard

Tactic:
rw [hE.cast_ncard_eq]

Goal state after:
α : Type u_1
E : Set α
hE : E.Finite
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.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
subset_ground : ∀ ⦃I : Set α⦄, Indep I → I ⊆ E
I : Set α
hI : Indep I
⊢ I.encard ≤ E.encard
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M N : Matroid α
h : N ≤r M
hne : N.E ≠ M.E
⊢ N <r M

Tactic:
by
  rw [← h.eq_restrict]
  exact restrict_isStrictRestriction (h.subset.ssubset_of_ne hne)

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 ⊆ f ⁻¹' N.E, ExistsMaximalSubsetProperty (fun I ↦ N.Indep (f '' I) ∧ InjOn f I) X

Tactic:
rintro X - I ⟨hI, hIinj⟩ hIX
      obtain ⟨J, hJ⟩ := (N ↾ range f).existsMaximalSubsetProperty_indep (f '' X) (by simp)
        (f '' I) (by simpa) (image_mono hIX)
      simp only [restrict_indep_iff, image_subset_iff, maximal_subset_iff, and_imp,
        and_assoc] at hJ ⊢
      obtain ⟨hIJ, hJ, hJf, hJX, hJmax⟩ := hJ
      obtain ⟨J₀, hIJ₀, hJ₀X, hbj⟩ := hIinj.bijOn_image.exists_extend_of_subset hIX
        (image_mono hIJ) (image_subset_iff.2 <| preimage_mono hJX)
      obtain rfl : f '' J₀ = J := by rw [← image_preimage_eq_of_subset hJf, hbj.image_eq]
      refine ⟨J₀, hIJ₀, hJ, hbj.injOn, hJ₀X, fun K hK hKinj hKX hJ₀K ↦ ?_⟩
      rw [← hKinj.image_eq_image_iff hJ₀K Subset.rfl, hJmax hK (image_subset_range _ _)
        (image_mono hKX) (image_mono hJ₀K)]

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
f✝ : α → β
E I : Set α
M✝ : Matroid α
N : Matroid β
M : Matroid α
f : ↑M.E ↪ β
e : α
he : e ∈ M.E
x✝¹ : Nonempty ↑M.E
x✝ : Nonempty α
⊢ ∀ (I : Set β),
    (M.comapOn (range ⇑f) fun x ↦ ↑(invFunOn (⇑f) univ x)).Indep I ↔ M.Indep (Subtype.val '' ⇑f ⁻¹' I) ∧ I ⊆ range ⇑f

Tactic:
comapOn_indep_iff,

Goal state after:
case inr
α : Type u_1
β : Type u_2
f✝ : α → β
E I : Set α
M✝ : Matroid α
N : Matroid β
M : Matroid α
f : ↑M.E ↪ β
e : α
he : e ∈ M.E
x✝¹ : Nonempty ↑M.E
x✝ : Nonempty α
⊢ ∀ (I : Set β),
    M.Indep ((fun x ↦ ↑(invFunOn (⇑f) univ x)) '' I) ∧ InjOn (fun x ↦ ↑(invFunOn (⇑f) univ x)) I ∧ I ⊆ range ⇑f ↔
      M.Indep (Subtype.val '' ⇑f ⁻¹' I) ∧ I ⊆ range ⇑f
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₀E : I₀ ⊆ M.E
hI : ∀ J ⊆ f '' I₀, J.Finite → (M.map f hf).Indep J
h' : f '' I₀ ⊆ f '' M.E
J₀ : Set α
hJ₀I₀ : J₀ ⊆ I₀
hJ₀ : J₀.Finite
⊢ M.Indep J₀

Tactic:
specialize hI (f '' J₀) (image_mono hJ₀I₀) (hJ₀.image _)

Goal state after:
α : 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₀E : I₀ ⊆ M.E
h' : f '' I₀ ⊆ f '' M.E
J₀ : Set α
hI : (M.map f hf).Indep (f '' J₀)
hJ₀I₀ : J₀ ⊆ I₀
hJ₀ : J₀.Finite
⊢ M.Indep J₀
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ (M.restrictSubtype M.E)✶ = M✶.restrictSubtype M.E

Tactic:
rw [restrictSubtype, ← comapOn_preimage_eq, comapOn_dual_eq_of_bijOn, restrict_ground_eq_self,
    ← dual_ground, comapOn_preimage_eq, restrictSubtype, restrict_ground_eq_self]

Goal state after:
α : Type u_1
M : Matroid α
⊢ BijOn Subtype.val (M.E ↓∩ (M ↾ M.E).E) (M ↾ M.E).E
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
R : Set α
hR : R ⊆ M.E
⊢ (M ↾ R).loops = M.loops ∩ R

Tactic:
rw [restrict_loops_eq', sdiff_eq_empty.2 hR, union_empty]

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

Goal state before:
pp: α : Type u_1
I : Set α
e : α
M : Matroid α
⊢ (M ↾ univ).fundCircuit e I = M.fundCircuit e I

Tactic:
have aux (A B) : M.closure A ⊆ B ∪ univ \ M.E ↔ M.closure A ⊆ B := by
    refine ⟨fun h ↦ ?_, fun h ↦ h.trans subset_union_left⟩
    refine (subset_inter h (M.closure_subset_ground A)).trans ?_
    simp [union_inter_distrib_right]

Goal state after:
α : Type u_1
I : Set α
e : α
M : Matroid α
aux : ∀ (A B : Set α), M.closure A ⊆ B ∪ univ \ M.E ↔ M.closure A ⊆ B
⊢ (M ↾ univ).fundCircuit e I = M.fundCircuit e I
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: case refine_1
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h₁ : ∀ (C : Set α), M₁.IsCircuit C → ¬M₂.Indep C
h₂ : ∀ (C : Set α), M₂.IsCircuit C → ¬M₁.Indep C
C : Set α
hCE : C ⊆ M₁.E
hC : M₁.IsCircuit C
⊢ M₂.IsCircuit C

Tactic:
obtain ⟨C', hC'C, hC'⟩ := ((not_indep_iff (by rwa [← hE])).1 (h₁ C hC)).exists_isCircuit_subset
    rwa [← hC.eq_of_not_indep_subset (h₂ C' hC') hC'C]

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

Goal state before:
pp: case neg
α : Type u_1
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
hY : ∀ e ∈ Y \ X, M.eRk (insert e X) ≤ M.eRk X
hX : ¬M.IsRkFinite X
⊢ M.eRk X = M.eRk Y

Tactic:
eRk_eq_top_iff.2 hX,

Goal state after:
case neg
α : Type u_1
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
hY : ∀ e ∈ Y \ X, M.eRk (insert e X) ≤ M.eRk X
hX : ¬M.IsRkFinite X
⊢ ⊤ = M.eRk Y
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
e f : α
C₁ C₂ : Set α
hC₁ : M.IsCircuit C₁
hC₂ : M.IsCircuit C₂
heC₁ : e ∈ C₁
heC₂ : e ∈ C₂
hfC₁ : f ∈ C₁
hfC₂ : f ∉ C₂
⊢ ∃ C ⊆ (C₁ ∪ C₂) \ {e}, M.IsCircuit C ∧ f ∈ C

Tactic:
obtain ⟨C, hCs, hC, hfC⟩ := hC₁.strong_multi_elimination (fun i : Unit ↦ e) (fun _ ↦ C₂) f
    (by simpa) (by simpa) (by simpa) (by simp) (by simpa) (by simpa)
  exact ⟨C, hCs.trans (sdiff_subset_sdiff (by simp) (by simp)), hC, hfC⟩

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

Goal state before:
pp: α : Type u_2
M : Matroid α
X Y Y' : Set α
h : M.closure Y = M.closure Y'
⊢ M.closure (X ∪ M.closure Y') = M.closure (X ∪ Y')

Tactic:
M.closure_union_closure_right_eq

Goal state after:
α : Type u_2
M : Matroid α
X Y Y' : Set α
h : M.closure Y = M.closure Y'
⊢ M.closure (X ∪ Y') = M.closure (X ∪ Y')
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
⊢ M✶.eRk X + M.eRank = M.eRk (M.E \ X) + (X ∩ M.E).encard

Tactic:
← sdiff_inter_self_eq_sdiff,

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
⊢ M✶.eRk X + M.eRank = M.eRk (M.E \ (X ∩ M.E)) + (X ∩ M.E).encard
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: α : Type u
M : Matroid α
X : Set α
κ : Cardinal.{u}
⊢ M.cRk X ≤ κ ↔ ∀ ⦃I : Set α⦄, M.IsBasis' I X → #↑I ≤ κ

Tactic:
by
  simp_rw [cRk, cRank_le_iff, isBase_restrict_iff']

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

Goal state before:
pp: case neg
α : Type u
β : Type v
f : α → β
M : Matroid α
I J B✝ B'✝ X Y : Set α
inst✝ : M.Finitary
B B' : Set α
N : Matroid α
hfin : N.Finitary
hB : N.IsBase B
hB' : N.IsBase B'
h : Infinite ↑(B' \ B)
S : (a : α) → a ∈ B' \ B → Set α
S_fin : ∀ (a : α) (ha : a ∈ B' \ B), Finite ↑(S a ha)
hSB : ∀ (a : α) (ha : a ∈ B' \ B), S a ha ⊆ B
dep : ∀ (a : α) (ha : a ∈ B' \ B), ¬N.Indep (insert a (S a ha))
U : Set α := ⋃ a, S ↑a ⋯
⊢ B \ B' ⊆ U

Tactic:
← sdiff_inter_self_eq_sdiff,

Goal state after:
case neg
α : Type u
β : Type v
f : α → β
M : Matroid α
I J B✝ B'✝ X Y : Set α
inst✝ : M.Finitary
B B' : Set α
N : Matroid α
hfin : N.Finitary
hB : N.IsBase B
hB' : N.IsBase B'
h : Infinite ↑(B' \ B)
S : (a : α) → a ∈ B' \ B → Set α
S_fin : ∀ (a : α) (ha : a ∈ B' \ B), Finite ↑(S a ha)
hSB : ∀ (a : α) (ha : a ∈ B' \ B), S a ha ⊆ B
dep : ∀ (a : α) (ha : a ∈ B' \ B), ¬N.Indep (insert a (S a ha))
U : Set α := ⋃ a, S ↑a ⋯
⊢ B \ (B' ∩ B) ⊆ U
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : e ∈ M.fundCocircuit f B
hne : e ≠ f
hB' : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
hfB : f ∈ B
⊢ e ∈ M.E \ B

Tactic:
simpa [hne] using (M.fundCocircuit_subset_insert_compl f B) he

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

Goal state before:
pp: ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Unique ι
⊢ AlgebraicIndependent R x ↔ Injective ⇑(Polynomial.aeval (x default))

Tactic:
algebraicIndependent_iff_injective_aeval

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
inst✝ : Unique ι
⊢ Injective ⇑(aeval x) ↔ Injective ⇑(Polynomial.aeval (x default))
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
n : ℕ
H : ∀ (s : Finset A), (AlgebraicIndependent R fun i ↦ ↑i) → s.card ≤ n
⊢ ∀ (s : Set A), AlgebraicIndependent R Subtype.val → Cardinal.mk ↑s ≤ ↑n

Tactic:
intro s li
  apply Cardinal.card_le_of
  intro t
  rw [← Finset.card_map (Embedding.subtype (· ∈ s))]
  apply H
  apply algebraicIndependent_finset_map_embedding_subtype _ li

Goal state after: