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✝ : Flat R M
ι : Type u
f : ι → R
n✝ : ι
s : Finset ι
hn : n✝ ∉ s
ih : ∀ (v : ι → M), LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v) → ∑ i ∈ s, f i • v i = 0 → ∀ i ∈ s, f i = 0
v : ι → M
h : LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v)
hfv : ∑ i, f ↑i • v ↑i = 0
i : ι
hi : i ∈ insert n✝ s
l : ℕ
a : ↥(insert n✝ s) → Fin l → R
y : Fin l → M
hay : ∀ (i : ↥(insert n✝ s)), (fun i ↦ v ↑i) i = ∑ j, a i j • y j
hfa : ∀ (j : Fin l), ∑ i, (fun i ↦ f ↑i) i * a i j = 0
this : v n✝ ∉ 𝔪 • ⊤
n : ↥(insert n✝ s) := ⟨n✝, ⋯⟩
n_def : n = ⟨n✝, ⋯⟩
j : Fin l
hj : IsUnit (a n j)
a' : ι → R := fun i ↦ if hi : i ∈ insert n✝ s then a ⟨i, hi⟩ j else 0
a_eq : ∀ (i : ↥(insert n✝ s)), a i j = a' ↑i
⊢ f ↑n * a n j = (-∑ i ∈ s, f i * a' i) * (↑hj.unit⁻¹ * a n j)

Tactic:
hj.val_inv_mul,

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✝ : Flat R M
ι : Type u
f : ι → R
n✝ : ι
s : Finset ι
hn : n✝ ∉ s
ih : ∀ (v : ι → M), LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v) → ∑ i ∈ s, f i • v i = 0 → ∀ i ∈ s, f i = 0
v : ι → M
h : LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v)
hfv : ∑ i, f ↑i • v ↑i = 0
i : ι
hi : i ∈ insert n✝ s
l : ℕ
a : ↥(insert n✝ s) → Fin l → R
y : Fin l → M
hay : ∀ (i : ↥(insert n✝ s)), (fun i ↦ v ↑i) i = ∑ j, a i j • y j
hfa : ∀ (j : Fin l), ∑ i, (fun i ↦ f ↑i) i * a i j = 0
this : v n✝ ∉ 𝔪 • ⊤
n : ↥(insert n✝ s) := ⟨n✝, ⋯⟩
n_def : n = ⟨n✝, ⋯⟩
j : Fin l
hj : IsUnit (a n j)
a' : ι → R := fun i ↦ if hi : i ∈ insert n✝ s then a ⟨i, hi⟩ j else 0
a_eq : ∀ (i : ↥(insert n✝ s)), a i j = a' ↑i
⊢ f ↑n * a n j = (-∑ i ∈ s, f i * a' i) * 1
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Colon

Goal state before:
pp: case neg
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
N : Submodule R M
I : Ideal R
x : M
inst✝ : IsNoetherianRing R
hx : x ∉ N
ann : Ideal R := N.colon {x}
hI : I ∈ ann.minimalPrimes
key : ∃ n, n ≠ 0 ∧ ∃ J, I ^ n * J ≤ ann ∧ ¬J ≤ I
J : Ideal R
hJI : ¬J ≤ I
n : ℕ := Nat.find key
hJ : I ^ n * J ≤ ann
K : Ideal R := I ^ (n - 1) * J
step1 : ∀ y ∈ K, I ≤ N.colon {y • x}
f : ↥K → R
g : ∀ (y : ↥K), f y ∈ N.colon {y • x}
h : ∀ (y : ↥K), f y ∉ I
s : Finset ↥K
hs : span R ↑s = ⊤
⊢ False

Tactic:
let z := ∏ y ∈ s, f y

Goal state after:
case neg
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
N : Submodule R M
I : Ideal R
x : M
inst✝ : IsNoetherianRing R
hx : x ∉ N
ann : Ideal R := N.colon {x}
hI : I ∈ ann.minimalPrimes
key : ∃ n, n ≠ 0 ∧ ∃ J, I ^ n * J ≤ ann ∧ ¬J ≤ I
J : Ideal R
hJI : ¬J ≤ I
n : ℕ := Nat.find key
hJ : I ^ n * J ≤ ann
K : Ideal R := I ^ (n - 1) * J
step1 : ∀ y ∈ K, I ≤ N.colon {y • x}
f : ↥K → R
g : ∀ (y : ↥K), f y ∈ N.colon {y • x}
h : ∀ (y : ↥K), f y ∉ I
s : Finset ↥K
hs : span R ↑s = ⊤
z : R := ∏ y ∈ s, f y
⊢ False
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⟩
    have : l'.lTensor (ResidueField R) ∘ₗ l.lTensor (ResidueField R) = .id := by
      rw [← LinearMap.lTensor_comp, hl, LinearMap.lTensor_id]
    exact Function.HasLeftInverse.injective ⟨_, LinearMap.congr_fun this⟩

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

Goal state before:
pp: case mpr
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)
⊢ ∃ l', l' ∘ₗ l = LinearMap.id

Tactic:
have := Module.free_of_lTensor_residueField_injective l (LinearMap.range l).mkQ
      (Submodule.mkQ_surjective _) l.exact_map_mkQ_range h

Goal state after:
case mpr
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)
⊢ ∃ l', l' ∘ₗ l = LinearMap.id
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
x✝¹ : I.IsPrime
x✝ : ∃ x, I = ⊥.colon {x}
x : M
h : I = ⊥.colon {x}
⊢ I = (toSpanSingleton R M x).ker

Tactic:
simp [h, SetLike.ext_iff]

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

Goal state before:
pp: 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 = (toSpanSingleton R M x).ker
⊢ ∃ f, Function.Injective ⇑f

Tactic:
exact ⟨liftQ _ _ h.le, ker_eq_bot.mp (ker_liftQ_eq_bot' _ _ h)⟩

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

Goal state before:
pp: A : Type u
inst✝¹ : CommRing A
inst✝ : IsNoetherianRing A
I : Ideal A
h✝ : Disjoint ↑I ↑(nonZeroDivisors A)
P : Ideal A
h : P ∈ associatedPrimes A A
hP : I ≤ P
⊢ ⊥ < Module.annihilator A ↥I

Tactic:
rw [AssociatedPrimes.mem_iff, isAssociatedPrime_iff] at h

Goal state after:
A : Type u
inst✝¹ : CommRing A
inst✝ : IsNoetherianRing A
I : Ideal A
h✝ : Disjoint ↑I ↑(nonZeroDivisors A)
P : Ideal A
h : P.IsPrime ∧ ∃ x, P = ⊥.colon {x}
hP : I ≤ P
⊢ ⊥ < Module.annihilator A ↥I
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: case inr
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✝¹ : IsDedekindDomain R
inst✝ : Fintype (ClassGroup R)
n : ℕ
hn : n.Coprime (Fintype.card (ClassGroup R))
u : (FractionalIdeal R⁰ K)ˣ
hI : (↑(↑u ^ n)).IsPrincipal
⊢ orderOf ((ClassGroup.mk K) u) ∣ n ∧ orderOf ((ClassGroup.mk K) u) ∣ Fintype.card (ClassGroup R)

Tactic:
refine ⟨?_, orderOf_dvd_card⟩

Goal state after:
case inr
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✝¹ : IsDedekindDomain R
inst✝ : Fintype (ClassGroup R)
n : ℕ
hn : n.Coprime (Fintype.card (ClassGroup R))
u : (FractionalIdeal R⁰ K)ˣ
hI : (↑(↑u ^ n)).IsPrincipal
⊢ orderOf ((ClassGroup.mk K) u) ∣ n
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: case neg
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
inst✝ : Fintype (ClassGroup R)
n : ℕ
hn : n.Coprime (Fintype.card (ClassGroup R))
I : Ideal R
hI0 : ¬I = 0
hI : ClassGroup.mk0 ⟨I ^ n, ⋯⟩ = 1
⊢ orderOf (ClassGroup.mk0 ⟨I, ⋯⟩) ∣ n ∧ orderOf (ClassGroup.mk0 ⟨I, ⋯⟩) ∣ Fintype.card (ClassGroup R)

Tactic:
refine ⟨?_, orderOf_dvd_card⟩

Goal state after:
case neg
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
inst✝ : Fintype (ClassGroup R)
n : ℕ
hn : n.Coprime (Fintype.card (ClassGroup R))
I : Ideal R
hI0 : ¬I = 0
hI : ClassGroup.mk0 ⟨I ^ n, ⋯⟩ = 1
⊢ orderOf (ClassGroup.mk0 ⟨I, ⋯⟩) ∣ n
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : ↥(Ideal R)⁰
⊢ mk0 I = (mk0 J)⁻¹ ↔ ∃ x, x ≠ 0 ∧ ↑I * ↑J = Ideal.span {x}

Tactic:
rw [eq_inv_iff_mul_eq_one, ← map_mul, ClassGroup.mk0_eq_one_iff,
    Submodule.isPrincipal_iff, Submonoid.coe_mul]

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : ↥(Ideal R)⁰
⊢ (∃ a, ↑I * ↑J = R ∙ a) ↔ ∃ x, x ≠ 0 ∧ ↑I * ↑J = Ideal.span {x}
Module: Mathlib.RingTheory.LocalProperties.Projective

Goal state before:
pp: R : Type u_1
M : Type uM
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_4
inst✝⁷ : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)
inst✝⁶ : (P : Ideal R) → [inst : P.IsMaximal] → Algebra R (Rₚ P)
inst✝⁵ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5
inst✝⁴ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommGroup (Mₚ P)
inst✝³ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → Module (Rₚ P) (Mₚ P)
inst✝¹ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsScalarTower R (Rₚ P) (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
H : ∀ (I : Ideal R) (x : I.IsMaximal), Projective (Rₚ I) (Mₚ I)
inst✝ : FinitePresentation R M
P : Ideal R
hP : P.IsMaximal
e : Rₚ P ≃+* Localization.AtPrime P :=
  (IsLocalization.algEquiv P.primeCompl (Rₚ P) (Localization.AtPrime P)).toRingEquiv
⊢ Projective (Localization.AtPrime P) (LocalizedModule P.primeCompl M)

Tactic:
refine Module.Projective.of_equiv (M := Mₚ P) (R := Rₚ P)
    (σ := e)
    { __ := IsLocalizedModule.linearEquiv P.primeCompl (f P)
        (LocalizedModule.mkLinearMap P.primeCompl M)
      map_smul' := ?_ }

Goal state after:
R : Type u_1
M : Type uM
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_4
inst✝⁷ : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)
inst✝⁶ : (P : Ideal R) → [inst : P.IsMaximal] → Algebra R (Rₚ P)
inst✝⁵ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5
inst✝⁴ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommGroup (Mₚ P)
inst✝³ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → Module (Rₚ P) (Mₚ P)
inst✝¹ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsScalarTower R (Rₚ P) (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
H : ∀ (I : Ideal R) (x : I.IsMaximal), Projective (Rₚ I) (Mₚ I)
inst✝ : FinitePresentation R M
P : Ideal R
hP : P.IsMaximal
e : Rₚ P ≃+* Localization.AtPrime P :=
  (IsLocalization.algEquiv P.primeCompl (Rₚ P) (Localization.AtPrime P)).toRingEquiv
⊢ ∀ (m : Rₚ P) (x : Mₚ P),
    (↑(IsLocalizedModule.linearEquiv P.primeCompl (f P) (LocalizedModule.mkLinearMap P.primeCompl M))).toFun (m • x) =
      ↑e m • (↑(IsLocalizedModule.linearEquiv P.primeCompl (f P) (LocalizedModule.mkLinearMap P.primeCompl M))).toFun x
Module: Mathlib.RingTheory.TensorProduct.IsBaseChangePi

Goal state before:
pp: R : Type u_1
S✝ : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S✝
inst✝⁶ : Algebra R S✝
S : Submonoid R
ι : Type u_3
inst✝⁵ : Finite ι
M : ι → Type u_4
M' : ι → Type u_5
inst✝⁴ : (i : ι) → AddCommMonoid (M i)
inst✝³ : (i : ι) → AddCommMonoid (M' i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : (i : ι) → Module R (M' i)
f : (i : ι) → M i →ₗ[R] M' i
inst✝ : ∀ (i : ι), IsLocalizedModule S (f i)
this : (i : ι) → Module (Localization S) (M' i) := fun i ↦ module S (f i)
⊢ IsBaseChange (Localization S) (LinearMap.pi fun i ↦ f i ∘ₗ LinearMap.proj i)

Tactic:
apply IsBaseChange.pi

Goal state after:
R : Type u_1
S✝ : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S✝
inst✝⁶ : Algebra R S✝
S : Submonoid R
ι : Type u_3
inst✝⁵ : Finite ι
M : ι → Type u_4
M' : ι → Type u_5
inst✝⁴ : (i : ι) → AddCommMonoid (M i)
inst✝³ : (i : ι) → AddCommMonoid (M' i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : (i : ι) → Module R (M' i)
f : (i : ι) → M i →ₗ[R] M' i
inst✝ : ∀ (i : ι), IsLocalizedModule S (f i)
this : (i : ι) → Module (Localization S) (M' i) := ⋯
⊢ ∀ (i : ι), IsBaseChange (Localization S) (f i)
Module: Mathlib.RingTheory.LocalRing.ResidueField.Fiber

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
p : Ideal R
inst✝ : p.IsPrime
x : S ⊗[R] p.ResidueField
r : R
a : S
y : R
t : ↥p.primeCompl
e :
  1 ⊗ₜ[R]
        (r •
          (IsLocalRing.residue (Localization.AtPrime p))
            ((fun x ↦
                match x with
                | (r, m) => IsLocalization.mk' (Localization.AtPrime p) r m)
              (y, t))) *
      x =
    a ⊗ₜ[R]
      (IsLocalRing.residue (Localization.AtPrime p))
        ((fun x ↦
            match x with
            | (r, m) => IsLocalization.mk' (Localization.AtPrime p) r m)
          (y, t))
hrt : r ∉ p ∧ y ∉ p
⊢ includeRight ((algebraMap R p.ResidueField) (r * y)) * x = a ⊗ₜ[R] (algebraMap R p.ResidueField) y

Tactic:
Algebra.TensorProduct.includeRight_apply

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
p : Ideal R
inst✝ : p.IsPrime
x : S ⊗[R] p.ResidueField
r : R
a : S
y : R
t : ↥p.primeCompl
e :
  1 ⊗ₜ[R]
        (r •
          (IsLocalRing.residue (Localization.AtPrime p))
            ((fun x ↦
                match x with
                | (r, m) => IsLocalization.mk' (Localization.AtPrime p) r m)
              (y, t))) *
      x =
    a ⊗ₜ[R]
      (IsLocalRing.residue (Localization.AtPrime p))
        ((fun x ↦
            match x with
            | (r, m) => IsLocalization.mk' (Localization.AtPrime p) r m)
          (y, t))
hrt : r ∉ p ∧ y ∉ p
⊢ 1 ⊗ₜ[R] (algebraMap R p.ResidueField) (r * y) * x = a ⊗ₜ[R] (algebraMap R p.ResidueField) y
Module: Mathlib.RingTheory.LocalRing.ResidueField.Fiber

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
p : Ideal R
inst✝ : p.IsPrime
x : p.Fiber S
⊢ ∃ r ∉ p, ∃ s, r • x = 1 ⊗ₜ[R] s

Tactic:
obtain ⟨r, hr, s, e⟩ := Ideal.ResidueField.exists_smul_eq_tmul_one _
    (Algebra.TensorProduct.comm _ _ _ x)
  refine ⟨r, hr, s, by simpa using congr((Algebra.TensorProduct.comm _ _ _).symm $e)⟩

Goal state after:
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: case succ.inr
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSimpleGroup G
n : ℕ
ih : derivedSeries G n.succ = _root_.commutator G
h : ⁅⊤, ⊤⁆ = ⊤
⊢ ⁅⁅⊤, ⊤⁆, ⁅⊤, ⊤⁆⁆ = ⁅⊤, ⊤⁆

Tactic:
rwa [h]

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
inst✝ : Subsingleton M
⊢ rankAtStalk M = 0

Tactic:
by
  ext p
  exact Module.finrank_zero_of_subsingleton

Goal state after:
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: case neg
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Finite E
α : Eˣ
hα : ∀ (x : Eˣ), x ∈ Subgroup.zpowers α
x : E
hx : ¬x = 0
⊢ x ∈ F⟮↑α⟯

Tactic:
· obtain ⟨n, hn⟩ := Set.mem_range.mp (hα (Units.mk0 x hx))
    rw [show x = α ^ n by norm_cast; rw [hn, Units.val_mk0]]
    exact zpow_mem (mem_adjoin_simple_self F (E := E) ↑α) n

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

Goal state before:
pp: case refine_1
α : Type u_1
M : Matroid α
B : Set α
hB : B ⊆ M.E
h : M.IsBase (M.E \ B)
I : Set α
hI : I ⊆ M.E
B' : Set α
x✝ : M.IsBase B' ∧ Disjoint I B'
hBI : B ⊆ I
hB' : M.IsBase B'
hIB' : I ⊆ M.Eᶜ ∪ Bᶜᶜ
⊢ I ⊆ B

pp: case refine_1
α : Type u_1
M : Matroid α
B : Set α
hB : B ⊆ M.E
h : M.IsBase (M.E \ B)
I : Set α
hI : I ⊆ M.E
B' : Set α
x✝ : M.IsBase B' ∧ Disjoint I B'
hBI : B ⊆ I
hB' : M.IsBase B'
hIB' : Disjoint I B'
⊢ B' ⊆ M.E \ B

Tactic:
compl_compl

Goal state after:
case refine_1
α : Type u_1
M : Matroid α
B : Set α
hB : B ⊆ M.E
h : M.IsBase (M.E \ B)
I : Set α
hI : I ⊆ M.E
B' : Set α
x✝ : M.IsBase B' ∧ Disjoint I B'
hBI : B ⊆ I
hB' : M.IsBase B'
hIB' : I ⊆ M.Eᶜ ∪ B
⊢ I ⊆ B

case refine_1
α : Type u_1
M : Matroid α
B : Set α
hB : B ⊆ M.E
h : M.IsBase (M.E \ B)
I : Set α
hI : I ⊆ M.E
B' : Set α
x✝ : M.IsBase B' ∧ Disjoint I B'
hBI : B ⊆ I
hB' : M.IsBase B'
hIB' : Disjoint I B'
⊢ B' ⊆ M.E \ B
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: case pos
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h : ∀ ⦃I : Set α⦄, I ⊆ M₁.E → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
⊢ M₁.Indep I ↔ M₂.Indep I

Tactic:
rwa [h]

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✝³ : Semiring A
inst✝² : Algebra R A
e : A ⊗[R] M ≃ₗ[A] A
inst✝¹ : Flat R M
inst✝ : FaithfulSMul R A
I : Submodule R A
⊢ ⇑(I * submoduleAlgebra e).subtype ∘ ⇑(I.mulMap' (submoduleAlgebra e)) =
    ⇑(LinearEquiv.restrictScalars R (tensorSubmoduleAlgebraEquiv e)) ∘
      ⇑(LinearMap.rTensor (↥(submoduleAlgebra e)) I.subtype)

Tactic:
simp_rw [← LinearEquiv.coe_toLinearMap, ← LinearMap.coe_comp]

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✝³ : Semiring A
inst✝² : Algebra R A
e : A ⊗[R] M ≃ₗ[A] A
inst✝¹ : Flat R M
inst✝ : FaithfulSMul R A
I : Submodule R A
⊢ ⇑((I * submoduleAlgebra e).subtype ∘ₗ I.mulMap' (submoduleAlgebra e)) =
    ⇑(↑(LinearEquiv.restrictScalars R (tensorSubmoduleAlgebraEquiv e)) ∘ₗ
        LinearMap.rTensor (↥(submoduleAlgebra e)) I.subtype)
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: case mp
R : Type u
A : Type u_4
inst✝³ : CommSemiring R
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
M : Pic R
h : M ∈ (unitsToPic R A).range
⊢ M ∈ relPic R A

Tactic:
obtain ⟨I, rfl⟩ := h

Goal state after:
case mp
R : Type u
A : Type u_4
inst✝³ : CommSemiring R
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
I : (Submodule R A)ˣ
⊢ (unitsToPic R A) I ∈ relPic R A
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
e : α
hI : M.IsBasis I X
h : M.Indep (insert e I)
⊢ M.IsBasis (insert e I) (insert e X)

Tactic:
simp_rw [← union_singleton] at *

Goal state after:
α : Type u_1
M : Matroid α
I X : Set α
e : α
hI : M.IsBasis I X
h : M.Indep (I ∪ {e})
⊢ M.IsBasis (I ∪ {e}) (X ∪ {e})
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
N : Matroid α
hI : N.IsBasis I X
hNM : N ≤r M
⊢ M.IsBasis I X

Tactic:
by
  obtain ⟨R, hR, rfl⟩ := hNM; exact ((isBasis_restrict_iff hR).1 hI).1

Goal state after:
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.Indep (f '' I) → InjOn f I

Tactic:
refine fun hi ↦ hf.mono <| subset_trans ?_ (preimage_mono hi.subset_ground)

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
I : Set α
N : Matroid β
hf : InjOn f (f ⁻¹' N.E)
hi : N.Indep (f '' I)
⊢ I ⊆ f ⁻¹' f '' I
Module: Mathlib.Combinatorics.Matroid.Rank.Finite

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

Tactic:
rw [← isRkFinite_inter_ground_iff (X := X)]

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
⊢ M.IsRkFinite (M.closure X) ↔ M.IsRkFinite (X ∩ M.E)
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Matroid α
I X : Set α
f : α → β
hf : InjOn f M.E
hI : I ⊆ M.E
hX : X ⊆ M.E
h : (M.map f hf).IsBasis (f '' I) (f '' X)
hI' : M.Indep I
hss : I ⊆ X
J : Set α
hJ : M.Indep J
hIJ : I ⊆ J
hJX : J ⊆ X
⊢ J ⊆ I

Tactic:
have hIJ' := h.eq_of_subset_indep (hJ.map f hf) (image_mono hIJ) (image_mono hJX)

Goal state after:
α : Type u_1
β : Type u_2
M : Matroid α
I X : Set α
f : α → β
hf : InjOn f M.E
hI : I ⊆ M.E
hX : X ⊆ M.E
h : (M.map f hf).IsBasis (f '' I) (f '' X)
hI' : M.Indep I
hss : I ⊆ X
J : Set α
hJ : M.Indep J
hIJ : I ⊆ J
hJX : J ⊆ X
hIJ' : f '' I = f '' J
⊢ J ⊆ I
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: case refine_2
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ≠ f
h : M.IsCircuit {e, f}
hclosure : M.closure ({e, f} \ {e}) = M.closure ({e, f} \ {f})
⊢ M.closure {e} = M.closure {f}

Tactic:
pair_sdiff_left hef,

Goal state after:
case refine_2
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ≠ f
h : M.IsCircuit {e, f}
hclosure : M.closure {f} = M.closure ({e, f} \ {f})
⊢ M.closure {e} = M.closure {f}
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

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

Tactic:
rw [← sdiff_inter_sdiff, sdiff_inter]
  apply M.eRk_submod

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

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

Tactic:
rw [← eRk_inter_ground, eRank_def, union_sdiff_self,
    union_inter_cancel_right]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X Y : Set α
hX : M.IsRkFinite X
hXY : X ⊆ Y
hr : M.eRk Y ≤ M.eRk X
I : Set α
hI : M.IsBasis' I X
J : Set α
hJ : M.IsBasis' J Y
hIJ : I ⊆ J
⊢ M.closure X = M.closure Y

Tactic:
rw [hI.eRk_eq_encard, hJ.eRk_eq_encard] at hr

Goal state after:
α : Type u_1
M : Matroid α
X Y : Set α
hX : M.IsRkFinite X
hXY : X ⊆ Y
I : Set α
hI : M.IsBasis' I X
J : Set α
hr : J.encard ≤ I.encard
hJ : M.IsBasis' J Y
hIJ : I ⊆ J
⊢ M.closure X = M.closure Y
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: case refine_4
α : Type u_1
M : Matroid α
ι : Type u_2
C₀ : Set α
hC₀ : M.IsCircuit C₀
x : ι → α
C : ι → Set α
z : α
hC : ∀ (i : ι), M.IsCircuit (C i)
h_mem_C₀ : ∀ (i : ι), x i ∈ C₀
h_mem : ∀ (i : ι), x i ∈ C i
h_unique : ∀ ⦃i i' : ι⦄, x i ∈ C i' → i = i'
hzC₀ : z ∈ C₀
hzC : ∀ (i : ι), z ∉ C i
⊢ ∀ (i : ι), z ∈ C i → z = x i

Tactic:
exact fun i hzi ↦ (hzC i hzi).elim

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hIfin : I.Finite
x✝ : I ⊆ X ∧ M.Indep I ∧ I.encard = M.eRk X
hIX : I ⊆ X
hI : M.Indep I
hcard : I.encard = M.eRk X
J : Set α
hJ : M.IsBasis' J X
hIJ : I ⊆ J
⊢ M.IsBasis' I X

Tactic:
hIfin.eq_of_subset_of_encard_le hIJ (hJ.encard_eq_eRk.trans hcard.symm).le

Goal state after:
α : Type u_1
M : Matroid α
I X : Set α
hIfin : I.Finite
x✝ : I ⊆ X ∧ M.Indep I ∧ I.encard = M.eRk X
hIX : I ⊆ X
hI : M.Indep I
hcard : I.encard = M.eRk X
J : Set α
hJ : M.IsBasis' J X
hIJ : I ⊆ J
⊢ M.IsBasis' J X
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
he : e ∈ M.E
h : M.closure (M.E \ {e}) = M.E
⊢ e ∈ M.closure (M.E \ {e})

Tactic:
rwa [h]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
K X : Set α
hK : K ⊆ M.coloops
⊢ M.closure X ∩ M.coloops ∩ K = X ∩ K

Tactic:
closure_inter_coloops_eq,

Goal state after:
α : Type u_1
M : Matroid α
K X : Set α
hK : K ⊆ M.coloops
⊢ X ∩ M.coloops ∩ K = X ∩ K
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
K X : Set α
hK : K ⊆ M.coloops
⊢ M.closure (X ∪ K) = M.closure X ∪ K

Tactic:
by
  rw [← closure_union_closure_left_eq, subset_antisymm_iff, and_iff_left (M.subset_closure _),
    ← sdiff_eq_empty, eq_empty_iff_forall_notMem]
  refine fun e ⟨hecl, he⟩ ↦ he (.inl ?_)
  obtain ⟨C, hCss, hC, heC⟩ := (mem_closure_iff_exists_isCircuit he).1 hecl
  rw [← singleton_union, ← union_assoc, union_comm, ← sdiff_subset_iff,
    (hC.disjoint_coloops.mono_right hK).sdiff_eq_left, singleton_union] at hCss
  exact M.closure_subset_closure_of_subset_closure (by simpa) <|
    hC.mem_closure_sdiff_singleton_of_mem heC

Goal state after: