mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ Submodule.IsPrincipal I

Tactic:
obtain ⟨a, K, ha0, h⟩ := exists_eq_spanSingleton_mul (I : FractionalIdeal R⁰ (FractionRing R))⁻¹

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
⊢ Submodule.IsPrincipal I
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 : ↑I * (↑I)⁻¹ = 1
a : R
K : Ideal R
ha0 : a ≠ 0
ha0' :
  spanSingleton R⁰ ((algebraMap R (FractionRing R)) a) * (spanSingleton R⁰ ((algebraMap R (FractionRing R)) a))⁻¹ = 1
h : 1 * (↑I * ↑K) = spanSingleton R⁰ ((algebraMap R (FractionRing R)) a) * ↑I * (↑I)⁻¹
⊢ ↑I * ↑K = spanSingleton R⁰ ((algebraMap R (FractionRing R)) a)

Tactic:
one_mul,

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsGCDMonoid R
I : Ideal R
hI : ↑I * (↑I)⁻¹ = 1
a : R
K : Ideal R
ha0 : a ≠ 0
ha0' :
  spanSingleton R⁰ ((algebraMap R (FractionRing R)) a) * (spanSingleton R⁰ ((algebraMap R (FractionRing R)) a))⁻¹ = 1
h : ↑I * ↑K = spanSingleton R⁰ ((algebraMap R (FractionRing R)) a) * ↑I * (↑I)⁻¹
⊢ ↑I * ↑K = spanSingleton R⁰ ((algebraMap R (FractionRing R)) a)
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: case mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' J' : Ideal R
hI : ↑I = ↑I'
x : (FractionRing R)ˣ
hJ : ↑I' * spanSingleton R⁰ ↑x = ↑J'
⊢ ∃ x y, x ≠ 0 ∧ y ≠ 0 ∧ Ideal.span {x} * I' = Ideal.span {y} * J'

Tactic:
mul_comm,

Goal state after:
case mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' J' : Ideal R
hI : ↑I = ↑I'
x : (FractionRing R)ˣ
hJ : spanSingleton R⁰ ↑x * ↑I' = ↑J'
⊢ ∃ x y, x ≠ 0 ∧ y ≠ 0 ∧ Ideal.span {x} * I' = Ideal.span {y} * J'
Module: Mathlib.RingTheory.ClassGroup.Basic

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

Tactic:
mul_comm,

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

Goal state before:
pp: case refine_1
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
x : PrimeSpectrum (S ⊗[R] T)
hx₁ : a ⊗ₜ[R] 1 ∉ x.asIdeal
hx₂ : 1 ⊗ₜ[R] t ∉ x.asIdeal
hx₃ : f ∈ x.asIdeal
⊢ a ⊗ₜ[R] (1 * t) ∈ ↑x.asIdeal

Tactic:
one_mul,

Goal state after:
case refine_1
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
x : PrimeSpectrum (S ⊗[R] T)
hx₁ : a ⊗ₜ[R] 1 ∉ x.asIdeal
hx₂ : 1 ⊗ₜ[R] t ∉ x.asIdeal
hx₃ : f ∈ x.asIdeal
⊢ a ⊗ₜ[R] t ∈ ↑x.asIdeal
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 : T
r : R
a : S
ht : r • t ∉ Ideal.comap g J.asIdeal
e : 1 ⊗ₜ[R] (r • t) * f = a ⊗ₜ[R] t
⊢ a ⊗ₜ[R] (1 * t) ∉ J.asIdeal

Tactic:
one_mul,

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
⊢ a ⊗ₜ[R] t ∉ J.asIdeal
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: case mp
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⁰ (FractionRing R))ˣ
x : FractionRing R
hx : spanSingleton R⁰ x = ↑I
⊢ spanSingleton R⁰ ((FractionRing.algEquiv R K) x) =
    ↑((Units.mapEquiv (canonicalEquiv R⁰ (FractionRing R) K).toMulEquiv).toMonoidHom I)

Tactic:
simp only [RingEquiv.toMulEquiv_eq_coe, MulEquiv.coe_toMonoidHom, coe_mapEquiv, ← hx,
        RingEquiv.coe_toMulEquiv, canonicalEquiv_spanSingleton]

Goal state after:
case mp
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⁰ (FractionRing R))ˣ
x : FractionRing R
hx : spanSingleton R⁰ x = ↑I
⊢ spanSingleton R⁰ ((FractionRing.algEquiv R K) x) = spanSingleton R⁰ ((IsLocalization.map K (RingHom.id R) ⋯) x)
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))ˣ
fd_ne_zero : (algebraMap R (FractionRing R)) ↑(↑I).den ≠ 0
⊢ ↑(I * (toPrincipalIdeal R (FractionRing R)) (Units.mk0 ((algebraMap R (FractionRing R)) ↑(↑I).den) fd_ne_zero)) =
    ↑((FractionalIdeal.mk0 (FractionRing R)) ⟨integralRep ↑I, ⋯⟩)

Tactic:
mul_comm,

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
fd_ne_zero : (algebraMap R (FractionRing R)) ↑(↑I).den ≠ 0
⊢ ↑((toPrincipalIdeal R (FractionRing R)) (Units.mk0 ((algebraMap R (FractionRing R)) ↑(↑I).den) fd_ne_zero) * I) =
    ↑((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
inst✝ : Subsingleton (ClassGroup R)
I : Ideal R
hI : IsUnit ↑I
⊢ Submodule.IsPrincipal I

Tactic:
have hsub :
      ((I : FractionalIdeal R⁰ K) : Submodule R K).IsPrincipal :=
    ClassGroup.isPrincipal_coeSubmodule_of_isUnit (I := (I : FractionalIdeal R⁰ K)) hI
  exact (IsFractionRing.coeSubmodule_isPrincipal (R := R) (K := K) (I := I)).1
    (by simpa using hsub)

Goal state after:
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
N : Type u_1
inst✝¹ : AddCommGroup N
inst✝ : Module R N
e : M ≃ₗ[R] N
p : PrimeSpectrum R
⊢ rankAtStalk M p = rankAtStalk N p

Tactic:
exact IsLocalizedModule.mapEquiv p.asIdeal.primeCompl
    (LocalizedModule.mkLinearMap p.asIdeal.primeCompl M)
    (LocalizedModule.mkLinearMap p.asIdeal.primeCompl N) _ e |>.finrank_eq

Goal state after:
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
h : Normal F L
⊢ Normal F ↥(normalClosure F K L)

Tactic:
obtain _ | φ := isEmpty_or_nonempty (K →ₐ[F] L)
  · rw [normalClosure, iSup_of_empty]; exact Normal.of_algEquiv (botEquiv F L).symm
  · exact (isNormalClosure_normalClosure F K L).normal

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
⊢ toSkeleton (SemimoduleCat.of R M') * toSkeleton (SemimoduleCat.of R (Dual R M')) = 1

Tactic:
mul_comm,

Goal state after:
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
⊢ toSkeleton (SemimoduleCat.of R (Dual R M')) * toSkeleton (SemimoduleCat.of R M') = 1
Module: Mathlib.FieldTheory.Normal.Closure

Goal state before:
pp: case refine_1
F : Type u_1
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Normal F L
K₁ K₂ : IntermediateField F L
inst✝ : Normal F ↥K₂
h : normalClosure F (↥K₁) L ≤ K₂
⊢ K₁ ≤ K₂

pp: case refine_2
F : Type u_1
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Normal F L
K₁ K₂ : IntermediateField F L
inst✝ : Normal F ↥K₂
h : K₁ ≤ K₂
⊢ normalClosure F (↥K₁) L ≤ K₂

Tactic:
· rw [normalClosure_le_iff] at h
    simpa only [fieldRange_val] using h K₁.val

Goal state after:
case refine_2
F : Type u_1
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Normal F L
K₁ K₂ : IntermediateField F L
inst✝ : Normal F ↥K₂
h : K₁ ≤ K₂
⊢ normalClosure F (↥K₁) L ≤ K₂
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 : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] LocalizedModule P.primeCompl M :=
  fun P [P.IsMaximal] ↦ LocalizedModule.mkLinearMap P.primeCompl M
ff : (P : Ideal R) →
  [inst : P.IsMaximal] → M ⊗[R] M →ₗ[R] LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M :=
  fun P [P.IsMaximal] ↦ map (f P) (f P)
P : Ideal R
x✝ : P.IsMaximal
Rp : Type u := Localization P.primeCompl
e✝ : LocalizedModule P.primeCompl M ≃ₗ[Rp] Rp
e : LocalizedModule P.primeCompl M ≃ₗ[R] Rp
x y : LocalizedModule P.primeCompl M
| 1 ⊗ₜ[Rp] (e y * e x)

Tactic:
mul_comm,

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 : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] LocalizedModule P.primeCompl M :=
  fun P [P.IsMaximal] ↦ LocalizedModule.mkLinearMap P.primeCompl M
ff : (P : Ideal R) →
  [inst : P.IsMaximal] → M ⊗[R] M →ₗ[R] LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M :=
  fun P [P.IsMaximal] ↦ map (f P) (f P)
P : Ideal R
x✝ : P.IsMaximal
Rp : Type u := Localization P.primeCompl
e✝ : LocalizedModule P.primeCompl M ≃ₗ[Rp] Rp
e : LocalizedModule P.primeCompl M ≃ₗ[R] Rp
x y : LocalizedModule P.primeCompl M
| 1 ⊗ₜ[Rp] (e x * e y)
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hI : M.Indep I
hIX : I ⊆ X
⊢ (∀ x ∉ I, M.Indep (insert x I) → x ∉ X) ∧ X ⊆ M.E ↔ ∀ e ∈ X, e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E

Tactic:
exact ⟨fun h e heX heI ↦ ⟨fun hi ↦ h.1 e heI hi heX, h.2 heX⟩,
    fun h ↦ ⟨fun e heI hi heX ↦ (h e heX heI).1 hi,
      fun e heX ↦ (em (e ∈ I)).elim (fun h ↦ hI.subset_ground h) fun heI ↦ (h _ heX heI).2 ⟩⟩

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

Goal state before:
pp: α : Type u_1
M : Matroid α
ι : Type u_2
X I : ι → Set α
hI : ∀ (i : ι), M.IsBasis (I i) (X i)
h_ind : M.Indep (⋃ i, I i)
e : α
he' : ∀ (x : ι), e ∉ I x
i : ι
hes : e ∈ X i
⊢ e ∈ M.E ∧ ∀ (i : ι), I i ⊆ M.E

Tactic:
and_iff_left (fun i ↦ (hI i).indep.subset_ground)

Goal state after:
α : Type u_1
M : Matroid α
ι : Type u_2
X I : ι → Set α
hI : ∀ (i : ι), M.IsBasis (I i) (X i)
h_ind : M.Indep (⋃ i, I i)
e : α
he' : ∀ (x : ι), e ∉ I x
i : ι
hes : e ∈ X i
⊢ e ∈ M.E
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: case h
α : Type u_1
M✝ : Matroid α
R✝ I✝ X Y : Set α
M : Matroid α
R A : Set α
hAR : A ⊆ R
I : Set α
hI : M.Indep I
right✝ : I ⊆ R
hIA : I ⊆ A
J : Set α
hJ : M.IsBasis' J A
hIJ : I ⊆ J
⊢ I ⊆ J ∧ Maximal (fun K ↦ (fun I ↦ M.Indep I ∧ I ⊆ R) K ∧ K ⊆ A) J

Tactic:
simp only [hIJ, and_assoc, maximal_subset_iff, hJ.indep, hJ.subset, and_imp, true_and,
      hJ.subset.trans hAR]

Goal state after:
case h
α : Type u_1
M✝ : Matroid α
R✝ I✝ X Y : Set α
M : Matroid α
R A : Set α
hAR : A ⊆ R
I : Set α
hI : M.Indep I
right✝ : I ⊆ R
hIA : I ⊆ A
J : Set α
hJ : M.IsBasis' J A
hIJ : I ⊆ J
⊢ ∀ ⦃t : Set α⦄, M.Indep t → t ⊆ R → t ⊆ A → J ⊆ t → J = t
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
R I X : Set α
⊢ (M ↾ R).IsBasis I X ↔ M.IsBasis I (X ∩ M.E) ∧ X ⊆ R

Tactic:
isBasis_iff_isBasis'_subset_ground,

Goal state after:
α : Type u_1
M : Matroid α
R I X : Set α
⊢ (M ↾ R).IsBasis' I X ∧ X ⊆ (M ↾ R).E ↔ M.IsBasis I (X ∩ M.E) ∧ X ⊆ R
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
I X Y J : Set α
hIX : M.IsBasis I X
hJX : M.IsBasis J X
hXY : X ⊆ Y
hJY : M.IsBasis J Y
⊢ M.IsBasis I Y

Tactic:
by
  rw [← isBase_restrict_iff]; rw [← isBase_restrict_iff] at hJY
  exact hJY.isBase_of_isBasis_superset hJX.subset (hIX.isBasis_restrict_of_subset hXY)

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I X J : Set α
hI : M.Indep I
hIX : I ⊆ X
hJ : M.IsBasis J X
⊢ ∃ I', M.IsBasis I' X ∧ I ⊆ I' ∧ I' ⊆ I ∪ J

Tactic:
by
  obtain ⟨I', hI', hII', hI'IJ⟩ :=
    (hI.indep_restrict_of_subset hIX).exists_isBase_subset_union_isBase (IsBasis.isBase_restrict hJ)
  rw [isBase_restrict_iff] at hI'
  exact ⟨I', hI', hII', hI'IJ⟩

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X Y : Set α
hX : M.IsRkFinite X
⊢ M.IsRkFinite (Y \ X) ↔ M.IsRkFinite Y

Tactic:
by
  rw [← hX.isRkFinite_union_iff, union_sdiff_self, hX.isRkFinite_union_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
B : Set α
hB : B ⊆ M.E
x✝ : ∃ B₀, M.IsBase B₀ ∧ f '' B = f '' B₀
J : Set α
hJ : M.IsBase J
hIJ : f '' B = f '' J
⊢ M.IsBase B

Tactic:
hf.image_eq_image_iff hB hJ.subset_ground

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
B : Set α
hB : B ⊆ M.E
x✝ : ∃ B₀, M.IsBase B₀ ∧ f '' B = f '' B₀
J : Set α
hJ : M.IsBase J
hIJ : B = J
⊢ M.IsBase B
Module: Mathlib.Combinatorics.Matroid.Circuit

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

Tactic:
closure_subset_closure_iff_subset_closure
    (show {e} ⊆ M.E by simpa using mem_ground_of_mem_closure he),

Goal state after:
α : Type u_1
M : Matroid α
I : Set α
e : α
he : e ∈ M.closure I
⊢ insert e (I ∩ ⋂₀ {J | J ⊆ I ∧ {e} ⊆ M.closure J}) = insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J})
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
E✝ I✝ : Set α
M✝ : Matroid α
N : Matroid β
E X I : Set α
M : Matroid α
inst✝ : M.RankPos
B : Set ↑M.E
hB : (M.restrictSubtype M.E).IsBase B
hB' : M.IsBase (Subtype.val '' B)
⊢ (M.restrictSubtype M.E).RankPos

Tactic:
exact hB.rankPos_of_nonempty <| by simpa using hB'.nonempty

Goal state after:
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.eRk I ≤ J.encard

Tactic:
← hJ.eRk_eq_encard

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.eRk I ≤ M.eRk I
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
Xs : Set (Set α)
⊢ M.closure (⋃ x, M.closure ↑x) = M.closure (⋃ i, ↑i)

Tactic:
closure_iUnion_closure_eq_closure_iUnion

Goal state after:
α : Type u_2
M : Matroid α
Xs : Set (Set α)
⊢ M.closure (⋃ i, ↑i) = M.closure (⋃ i, ↑i)
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 ∪ 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 ∪ M.closure Y) = M.closure (X ∪ Y')
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
⊢ M.Dep (insert e I) ↔ M.Dep (insert e I) ∧ e ∉ I ∨ e ∈ I ∧ e ∉ I

Tactic:
and_not_self_iff,

Goal state after:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
⊢ M.Dep (insert e I) ↔ M.Dep (insert e I) ∧ e ∉ I ∨ False
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: case inl
α : Type u_1
M : Matroid α
x✝ : ∃ x, M.IsCircuit x ∧ x.Subsingleton
hC : M.IsCircuit ∅
hCs : ∅.Subsingleton
⊢ ∃ x ∈ M.E, M.IsLoop x

pp: case inr
α : Type u_1
M : Matroid α
x✝ : ∃ x, M.IsCircuit x ∧ x.Subsingleton
e : α
hC : M.IsCircuit {e}
hCs : {e}.Subsingleton
⊢ ∃ x ∈ M.E, M.IsLoop x

Tactic:
· simpa using hC.nonempty

Goal state after:
case inr
α : Type u_1
M : Matroid α
x✝ : ∃ x, M.IsCircuit x ∧ x.Subsingleton
e : α
hC : M.IsCircuit {e}
hCs : {e}.Subsingleton
⊢ ∃ x ∈ M.E, M.IsLoop x
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
I J Y : Set α
hI : (M ↾ X).IsBasis I Y
hJ : (M ↾ X).IsBasis J Y
⊢ #↑(I \ J) = #↑(J \ I)

Tactic:
isBasis_restrict_iff'

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

Goal state before:
pp: α : Type u_1
M : Matroid α
C : Set α
e : α
K : Set α
hC : M.IsCircuit C
he : C ∩ K = {e}
heC : e ∈ C
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃t : Set α⦄, t ⊂ K → M.Spanning (M.E \ t)
hKe : M.Spanning (M.E \ (K \ {e}))
⊢ False

Tactic:
apply hK.1

Goal state after:
α : Type u_1
M : Matroid α
C : Set α
e : α
K : Set α
hC : M.IsCircuit C
he : C ∩ K = {e}
heC : e ∈ C
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃t : Set α⦄, t ⊂ K → M.Spanning (M.E \ t)
hKe : M.Spanning (M.E \ (K \ {e}))
⊢ M.Spanning (M.E \ K)
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

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

Tactic:
refine ⟨fun I J X hI hJ ↦ ?_⟩
  obtain ⟨hI, hfI, hIX⟩ := comap_isBasis_iff.1 hI
  obtain ⟨hJ, hfJ, hJX⟩ := comap_isBasis_iff.1 hJ
  rw [← lift_inj.{u, v}, ← mk_image_eq_of_injOn_lift _ _ (hfI.mono sdiff_subset),
    ← mk_image_eq_of_injOn_lift _ _ (hfJ.mono sdiff_subset), lift_inj, hfI.image_sdiff,
    hfJ.image_sdiff, ← sdiff_union_sdiff_cancel inter_subset_left (image_inter_subset f I J),
    inter_comm, sdiff_inter_self_eq_sdiff, mk_union_of_disjoint, hI.cardinalMk_sdiff_comm hJ,
    ← sdiff_union_sdiff_cancel inter_subset_left (image_inter_subset f J I), inter_comm,
    sdiff_inter_self_eq_sdiff, mk_union_of_disjoint, inter_comm J I] <;>
  exact disjoint_sdiff_left.mono_right (sdiff_subset.trans inter_subset_left)

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

Goal state before:
pp: α : Type u_2
M : Matroid α
I : Set α
hI : I ⊆ M.E
⊢ M.Indep I ↔ ∀ ⦃e : α⦄, e ∈ I → e ∉ M.closure (I \ {e})

Tactic:
by
  use fun h e heI he ↦ ((h.closure_inter_eq_self_of_subset sdiff_subset).subset ⟨he, heI⟩).2 rfl
  intro h
  obtain ⟨J, hJ⟩ := M.exists_isBasis I
  convert! hJ.indep
  refine hJ.subset.antisymm' (fun e he ↦ by_contra fun heJ ↦ h he ?_)
  exact mem_of_mem_of_subset
    (hJ.subset_closure he) (M.closure_subset_closure (subset_sdiff_singleton hJ.subset heJ))

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

Goal state before:
pp: α : Type u_2
M : Matroid α
I : Set α
hI : I ⊆ M.E
h : ∀ ⦃J : Set α⦄, J ⊂ I → M.closure J ⊂ M.closure I
e : α
heI : e ∈ I
hecl : e ∈ M.closure (I \ {e})
⊢ M.closure (I \ {e}) = M.closure I

Tactic:
show I = insert e (I \ {e}) by simp [heI],

Goal state after:
α : Type u_2
M : Matroid α
I : Set α
hI : I ⊆ M.E
h : ∀ ⦃J : Set α⦄, J ⊂ I → M.closure J ⊂ M.closure I
e : α
heI : e ∈ I
hecl : e ∈ M.closure (I \ {e})
⊢ M.closure (insert e (I \ {e}) \ {e}) = M.closure (insert e (I \ {e}))
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
I : Set α
hI : I ⊆ M.E
h : ∀ ⦃J : Set α⦄, J ⊂ I → M.closure J ⊂ M.closure I
e : α
heI : e ∈ I
hecl : e ∈ M.closure (I \ {e})
⊢ M.closure (I \ {e}) = M.closure I

Tactic:
rw [show I = insert e (I \ {e}) by simp [heI], ← closure_insert_closure_eq_closure_insert,
    insert_eq_of_mem hecl]

Goal state after:
α : Type u_2
M : Matroid α
I : Set α
hI : I ⊆ M.E
h : ∀ ⦃J : Set α⦄, J ⊂ I → M.closure J ⊂ M.closure I
e : α
heI : e ∈ I
hecl : e ∈ M.closure (I \ {e})
⊢ M.closure (insert e (I \ {e}) \ {e}) = M.closure (M.closure (I \ {e}))
Module: Mathlib.RingTheory.Polynomial.SeparableDegree

Goal state before:
pp: F : Type u_1
inst✝ : Field F
q : ℕ
hF : ExpChar F q
f : F[X]
irred : Irreducible f
⊢ HasSeparableContraction q f

Tactic:
cases hF

Goal state after:
case zero
F : Type u_1
inst✝¹ : Field F
f : F[X]
irred : Irreducible f
inst✝ : CharZero F
⊢ HasSeparableContraction 1 f

case prime
F : Type u_1
inst✝ : Field F
q : ℕ
f : F[X]
irred : Irreducible f
hprime✝ : Nat.Prime q
hchar✝ : CharP F q
⊢ HasSeparableContraction q f
Module: Mathlib.RingTheory.Polynomial.SeparableDegree

Goal state before:
pp: case prime
F : Type u_1
inst✝ : Field F
q : ℕ
f : F[X]
irred : Irreducible f
hprime✝ : Nat.Prime q
hchar✝ : CharP F q
n : ℕ
g : F[X]
hgs : g.Separable
hge : (expand F (q ^ n)) g = f
⊢ HasSeparableContraction q f

Tactic:
exact ⟨g, hgs, n, hge⟩

Goal state after:
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
S : Type u_3
B : Type u_4
FRS : Type u_5
FAB : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : CommRing B
inst✝⁴ : Algebra S B
inst✝³ : FunLike FRS R S
inst✝² : RingHomClass FRS R S
inst✝¹ : FunLike FAB A B
inst✝ : RingHomClass FAB A B
f : FRS
g : FAB
H : ∀ (p : MvPolynomial ι R), (aeval x) p = 0 → p = 0
hf : Surjective ⇑f
hg : Injective ⇑g
h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A)
q : MvPolynomial ι R
hp : (aeval (⇑g ∘ x)) ((MvPolynomial.map ↑f) q) = 0
⊢ g ((aeval x) q) = g 0

Tactic:
rwa [map_zero, ← RingHom.coe_coe g, map_aeval, ← h, ← eval₂Hom_map_hom,
    ← aeval_eq_eval₂Hom]

Goal state after: