mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: case refine_2.refine_2.refine_1
R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : NormalizationMonoid R
r : R
hr : r ≠ 0
i : Ideal R
hi : i ∈ {I | I ∈ normalizedFactors (span {r})}
this : i.IsPrime
⊢ Submodule.IsPrincipal.generator i ∣ r

Tactic:
exact (Submodule.IsPrincipal.mem_iff_generator_dvd i).mp
          ((show span {r} ≤ i from dvd_iff_le.mp (dvd_of_mem_normalizedFactors hi))
            (mem_span_singleton.mpr (dvd_refl r)))

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.PDeriv

Goal state before:
pp: case pos
R : Type u
σ : Type v
inst✝ : CommSemiring R
i : σ
m n : σ →₀ ℕ
a : R
h : ¬n = m + single i 1
hn : n i = 0
⊢ (if n - single i 1 = m then a * ↑(n i) else 0) = 0

Tactic:
simp [hn]

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

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
ι : Type u_1
s : ι → P.Ring
hs : Ideal.span (Set.range s) = P.ker
⊢ Submodule.span S (Set.range fun i ↦ mk ⟨s i, ⋯⟩) = ⊤

Tactic:
rw [Ideal.span, ← Submodule.span_range_subtype_eq_top_iff] at hs
  · apply Submodule.span_eq_top_of_span_eq_top (R := P.Ring)
    rw [← Function.comp_def, Set.range_comp, ← Submodule.map_span, hs, Submodule.map_top,
      LinearMap.range_eq_top_of_surjective _ mk_surjective]
  · simp [← hs, Ideal.mem_span_range_self]

Goal state after:
Module: Mathlib.RingTheory.Extension.Generators

Goal state before:
pp: R : Type u
S : Type v
ι : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
P✝ P : Generators R S ι
T : Type u_1
inst✝¹ : CommRing T
inst✝ : Algebra R T
e : S ≃ₐ[R] T
t : T
⊢ (aeval (⇑e ∘ P.val)) ((P.σ ∘ ⇑e.symm) t) = t

Tactic:
by
    rw [Function.comp_def, ← AlgHom.coe_coe e, ← MvPolynomial.comp_aeval_apply]
    simp

Goal state after:
Module: Mathlib.RingTheory.Extension.Cotangent.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝²³ : CommRing R
inst✝²² : CommRing S
inst✝²¹ : Algebra R S
P : Extension R S
R' : Type u'
S' : Type v'
inst✝²⁰ : CommRing R'
inst✝¹⁹ : CommRing S'
inst✝¹⁸ : Algebra R' S'
P' : Extension R' S'
inst✝¹⁷ : Algebra R R'
inst✝¹⁶ : Algebra S S'
inst✝¹⁵ : Algebra R S'
inst✝¹⁴ : IsScalarTower R R' S'
R'' : Type u''
S'' : Type v''
inst✝¹³ : CommRing R''
inst✝¹² : CommRing S''
inst✝¹¹ : Algebra R'' S''
P'' : Extension R'' S''
inst✝¹⁰ : Algebra R R''
inst✝⁹ : Algebra S S''
inst✝⁸ : Algebra R S''
inst✝⁷ : IsScalarTower R R'' S''
inst✝⁶ : Algebra R' R''
inst✝⁵ : Algebra S' S''
inst✝⁴ : Algebra R' S''
inst✝³ : IsScalarTower R' R'' S''
inst✝² : IsScalarTower R R' R''
inst✝¹ : IsScalarTower S S' S''
inst✝ : IsScalarTower R S S'
f : P.Hom P'
⊢ P.H1Cotangent →ₗ[S] P'.H1Cotangent

Tactic:
refine (Cotangent.map f).restrict (p := LinearMap.ker P.cotangentComplex)
    (q := (LinearMap.ker P'.cotangentComplex).restrictScalars S) fun x hx ↦ ?_
  simp only [LinearMap.mem_ker, Submodule.restrictScalars_mem] at hx ⊢
  apply_fun (CotangentSpace.map f) at hx
  rw [CotangentSpace.map_cotangentComplex] at hx
  rw [hx]
  exact LinearMap.map_zero _

Goal state after:
Module: Mathlib.RingTheory.Support

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
hf : Function.Injective ⇑f
x : PrimeSpectrum R
m : M
hm : ∀ r ∉ x.asIdeal, r • m ≠ 0
r : R
hr : r ∉ x.asIdeal
⊢ r • f m ≠ 0

Tactic:
simpa using hf.ne (hm r hr)

Goal state after:
Module: Mathlib.RingTheory.Flat.EquationalCriterion

Goal state before:
pp: case h
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Flat R M
P : Type u_3
inst✝² : AddCommGroup P
inst✝¹ : Module R P
inst✝ : FinitePresentation R P
h₁ : P →ₗ[R] M
w✝ : ℕ
K : Submodule R (Fin w✝ → R)
ϕ : P ≃ₗ[R] (Fin w✝ → R) ⧸ K
hK : K.FG
this✝ : Module.Finite R ↥K
this : (h₁ ∘ₗ ↑ϕ.symm ∘ₗ K.mkQ) ∘ₗ K.subtype = 0
k : ℕ
a : (Fin w✝ → R) →ₗ[R] Fin k →₀ R
y : (Fin k →₀ R) →ₗ[R] M
hay : h₁ ∘ₗ ↑ϕ.symm ∘ₗ K.mkQ = y ∘ₗ a
ha : a ∘ₗ K.subtype = 0
⊢ h₁ = y ∘ₗ K.liftQ a ⋯ ∘ₗ ↑ϕ

Tactic:
apply (cancel_right ϕ.symm.surjective).mp

Goal state after:
case h
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Flat R M
P : Type u_3
inst✝² : AddCommGroup P
inst✝¹ : Module R P
inst✝ : FinitePresentation R P
h₁ : P →ₗ[R] M
w✝ : ℕ
K : Submodule R (Fin w✝ → R)
ϕ : P ≃ₗ[R] (Fin w✝ → R) ⧸ K
hK : K.FG
this✝ : Module.Finite R ↥K
this : (h₁ ∘ₗ ↑ϕ.symm ∘ₗ K.mkQ) ∘ₗ K.subtype = 0
k : ℕ
a : (Fin w✝ → R) →ₗ[R] Fin k →₀ R
y : (Fin k →₀ R) →ₗ[R] M
hay : h₁ ∘ₗ ↑ϕ.symm ∘ₗ K.mkQ = y ∘ₗ a
ha : a ∘ₗ K.subtype = 0
⊢ h₁ ∘ₗ ↑ϕ.symm = (y ∘ₗ K.liftQ a ⋯ ∘ₗ ↑ϕ) ∘ₗ ↑ϕ.symm
Module: Mathlib.Algebra.Module.SpanRankOperations

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
fg : N.FG
⊢ (baseChange A N).spanFinrank ≤ N.spanFinrank

Tactic:
grw [spanFinrank, spanRank_baseChange_le, Cardinal.toNat_lift, spanFinrank]
  simp [Cardinal.lift_lt_aleph0, spanRank_finite_iff_fg.mpr fg]

Goal state after:
Module: Mathlib.LinearAlgebra.Alternating.Uncurry.Fin

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
m : ℕ
f : M [⋀^Fin (m + 1)]→ₗ[R] N
v : Fin (m + 1 + 1) → M
j : Fin (m + 1 + 1)
i : Fin (m + 1)
hvij : v (j.succAbove i) = v j
hij : j.succAbove i ≠ j
⊢ -((-1) ^ ↑j • ((-1) ^ 2) ^ ↑i • f (j.removeNth v)) + (-1) ^ ↑j • f (j.removeNth v) = 0

pp: R : Type u_1
M : Type u_2
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
m : ℕ
f : M [⋀^Fin (m + 1)]→ₗ[R] N
v : Fin (m + 1 + 1) → M
j : Fin (m + 1 + 1)
i : Fin (m + 1)
hvij : v (j.succAbove i) = v j
hij : j.succAbove i ≠ j
⊢ v j = j.removeNth v i

Tactic:
neg_one_pow_two,

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
m : ℕ
f : M [⋀^Fin (m + 1)]→ₗ[R] N
v : Fin (m + 1 + 1) → M
j : Fin (m + 1 + 1)
i : Fin (m + 1)
hvij : v (j.succAbove i) = v j
hij : j.succAbove i ≠ j
⊢ -((-1) ^ ↑j • 1 ^ ↑i • f (j.removeNth v)) + (-1) ^ ↑j • f (j.removeNth v) = 0

R : Type u_1
M : Type u_2
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
m : ℕ
f : M [⋀^Fin (m + 1)]→ₗ[R] N
v : Fin (m + 1 + 1) → M
j : Fin (m + 1 + 1)
i : Fin (m + 1)
hvij : v (j.succAbove i) = v j
hij : j.succAbove i ≠ j
⊢ v j = j.removeNth v i
Module: Mathlib.LinearAlgebra.TensorProduct.Submodule

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M : Submodule R S
m : ↥M
r : ↥⊥
x : R
h : (algebraMap R ↥⊥) x = r
⊢ ↑(TensorProduct.comm R ↥M ↥⊥ ≪≫ₗ M.lTensorOne) (m ⊗ₜ[R] r) = ↑M.rTensorOne (m ⊗ₜ[R] r)

Tactic:
rw [← h]

Goal state after:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M : Submodule R S
m : ↥M
r : ↥⊥
x : R
h : (algebraMap R ↥⊥) x = r
⊢ ↑(TensorProduct.comm R ↥M ↥⊥ ≪≫ₗ M.lTensorOne) (m ⊗ₜ[R] (algebraMap R ↥⊥) x) =
    ↑M.rTensorOne (m ⊗ₜ[R] (algebraMap R ↥⊥) x)
Module: Mathlib.LinearAlgebra.TensorProduct.Submodule

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M : Submodule R S
r : ↥⊥
m : ↥M
x : R
h : (algebraMap R ↥⊥) x = r
⊢ ↑(TensorProduct.comm R ↥⊥ ↥M ≪≫ₗ M.rTensorOne) (r ⊗ₜ[R] m) = ↑M.lTensorOne (r ⊗ₜ[R] m)

Tactic:
rw [← h]

Goal state after:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M : Submodule R S
r : ↥⊥
m : ↥M
x : R
h : (algebraMap R ↥⊥) x = r
⊢ ↑(TensorProduct.comm R ↥⊥ ↥M ≪≫ₗ M.rTensorOne) ((algebraMap R ↥⊥) x ⊗ₜ[R] m) =
    ↑M.lTensorOne ((algebraMap R ↥⊥) x ⊗ₜ[R] m)
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝¹⁴ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝¹³ : (i : ι) → AddCommMonoid (s i)
inst✝¹² : (i : ι) → Module R (s i)
M : Type u_8
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
E : Type u_9
inst✝⁹ : AddCommMonoid E
inst✝⁸ : Module R E
F : Type u_10
inst✝⁷ : AddCommMonoid F
inst✝⁶ : Monoid R₁
inst✝⁵ : DistribMulAction R₁ R
inst✝⁴ : SMulCommClass R₁ R R
inst✝³ : Monoid R₂
inst✝² : DistribMulAction R₂ R
inst✝¹ : SMulCommClass R₂ R R
r : R₁
inst✝ : DecidableEq ι
r' : R
f : (i : ι) → s i
i : ι
m₁ m₂ : s i
⊢ tprodCoeff R (r • (r', update f i m₁).1) (r', update f i m₁).2 +
      tprodCoeff R (r • (r', update f i m₂).1) (r', update f i m₂).2 =
    tprodCoeff R (r • (r', update f i (m₁ + m₂)).1) (r', update f i (m₁ + m₂)).2

Tactic:
by simp [add_tprodCoeff]

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
H : Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype 𝔪))
⊢ Free R M

Tactic:
obtain ⟨_, _, b, _⟩ := exists_basis_of_span_of_maximalIdeal_rTensor_injective H id (by simp)

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
H : Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype 𝔪))
w✝¹ : Type u_2
w✝ : w✝¹ → M
b : Basis w✝¹ R M
h✝ : ∀ (i : w✝¹), b i = id (w✝ i)
⊢ Free R M
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝¹⁰ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁹ : (i : ι) → AddCommMonoid (s i)
inst✝⁸ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
E : Type u_9
inst✝⁵ : AddCommMonoid E
inst✝⁴ : Module R E
F : Type u_10
inst✝³ : AddCommMonoid F
inst✝² : Semiring R₁
inst✝¹ : Module R₁ R
inst✝ : SMulCommClass R₁ R R
r✝ r' : R₁
x : ⨂[R] (i : ι), s i
r : R
f : (i : ι) → s i
⊢ (r✝ + r') • tprodCoeff R r f = r✝ • tprodCoeff R r f + r' • tprodCoeff R r f

Tactic:
by simp_rw [smul_tprodCoeff', add_smul, add_tprodCoeff']

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
p : FreeAddMonoid (R × ((i : ι) → s i))
h : (List.map (fun x ↦ x.1 • ⨂ₜ[R] (i : ι), x.2 i) (FreeAddMonoid.toList p)).sum = x
a : R
⊢ (List.map (fun x ↦ x.1 • ⨂ₜ[R] (i : ι), x.2 i)
        (FreeAddMonoid.toList ((FreeAddMonoid.map fun y ↦ (a * y.1, y.2)) p))).sum =
    a • x

Tactic:
rw [← h]

Goal state after:
ι : 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
p : FreeAddMonoid (R × ((i : ι) → s i))
h : (List.map (fun x ↦ x.1 • ⨂ₜ[R] (i : ι), x.2 i) (FreeAddMonoid.toList p)).sum = x
a : R
⊢ (List.map (fun x ↦ x.1 • ⨂ₜ[R] (i : ι), x.2 i)
        (FreeAddMonoid.toList ((FreeAddMonoid.map fun y ↦ (a * y.1, y.2)) p))).sum =
    a • (List.map (fun x ↦ x.1 • ⨂ₜ[R] (i : ι), x.2 i) (FreeAddMonoid.toList p)).sum
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)
T : Finset R
hTK : ↑T ⊆ ↑K
K' : Ideal R := span ↑T
g : R := T.gcd id
hK' : K' ≤ span {g}
y : R
hyJ : y ∈ J
hJK : J * K = R ∙ y * g
hxmemJK : y * g ∈ J * K
hxT : y * g ∈ J * K'
hxJg : y * g ∈ J * span {g}
this : J * span {g} = span {y} * span {g}
hx0 : g = 0
⊢ y * g = 0

Tactic:
hx0,

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)
T : Finset R
hTK : ↑T ⊆ ↑K
K' : Ideal R := span ↑T
g : R := T.gcd id
hK' : K' ≤ span {g}
y : R
hyJ : y ∈ J
hJK : J * K = R ∙ y * g
hxmemJK : y * g ∈ J * K
hxT : y * g ∈ J * K'
hxJg : y * g ∈ J * span {g}
this : J * span {g} = span {y} * span {g}
hx0 : g = 0
⊢ y * 0 = 0
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
I : (FractionalIdeal R⁰ K)ˣ
x : Kˣ
hx : spanSingleton R⁰ ↑x = ↑I
⊢ ∃ x, spanSingleton R⁰ x = ↑I

pp: case mpr
R : Type u_1
K : Type u_2
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I : (FractionalIdeal R⁰ K)ˣ
x : K
hx : spanSingleton R⁰ x = ↑I
⊢ ∃ x, spanSingleton R⁰ ↑x = ↑I

Tactic:
· exact ⟨x, hx⟩

Goal state after:
case mpr
R : Type u_1
K : Type u_2
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I : (FractionalIdeal R⁰ K)ˣ
x : K
hx : spanSingleton R⁰ x = ↑I
⊢ ∃ x, spanSingleton R⁰ ↑x = ↑I
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, ⋯⟩)
⊢ spanSingleton R⁰ ↑this.unit * ↑I = ↑J

Tactic:
convert!
      (mk'_mul_coeIdeal_eq_coeIdeal (FractionRing R) <| mem_nonZeroDivisors_of_ne_zero hy).2 h

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : ↥(Ideal R)⁰
x y : R
hy : y ∈ R⁰
hz : mk' (FractionRing R) x ⟨y, hy⟩ ≠ 0
h : spanSingleton R⁰ (mk' (FractionRing R) x ⟨y, hy⟩) * ↑↑I = ↑↑J
⊢ ∃ x y, ∃ (_ : x ≠ 0) (_ : y ≠ 0), Ideal.span {x} * ↑I = Ideal.span {y} * ↑J

Tactic:
refine ⟨x, y, ?_, mem_nonZeroDivisors_iff_ne_zero.mp hy, ?_⟩

Goal state after:
case refine_1.refine_1
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : ↥(Ideal R)⁰
x y : R
hy : y ∈ R⁰
hz : mk' (FractionRing R) x ⟨y, hy⟩ ≠ 0
h : spanSingleton R⁰ (mk' (FractionRing R) x ⟨y, hy⟩) * ↑↑I = ↑↑J
⊢ x ≠ 0

case refine_1.refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : ↥(Ideal R)⁰
x y : R
hy : y ∈ R⁰
hz : mk' (FractionRing R) x ⟨y, hy⟩ ≠ 0
h : spanSingleton R⁰ (mk' (FractionRing R) x ⟨y, hy⟩) * ↑↑I = ↑↑J
⊢ Ideal.span {x} * ↑I = Ideal.span {y} * ↑J
Module: Mathlib.GroupTheory.Perm.ViaEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
e : Perm α
ι : α ↪ β
x : α
⊢ (e.viaEmbedding ι) (ι x) = ι (e x)

Tactic:
classical
  exact extendDomain_apply_image e (ofInjective ι.1 ι.2) x

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
S : Submonoid R
p : PrimeSpectrum (Localization S)
p' : Ideal R := Ideal.comap (algebraMap R (Localization S)) p.asIdeal
hp' : S ≤ p'.primeCompl
Rₚ : Type uR := Localization.AtPrime p'
Mₚ : Type (max uR uM) := LocalizedModule p'.primeCompl M
this✝⁵ : Algebra (Localization S) Rₚ :=
  IsLocalization.localizationAlgebraOfSubmonoidLe (Localization S) Rₚ S p'.primeCompl hp'
this✝⁴ : IsScalarTower R (Localization S) Rₚ
this✝³ : IsLocalization.AtPrime Rₚ p.asIdeal
this✝² : Module (Localization S) Mₚ := compHom Mₚ (algebraMap (Localization S) Rₚ)
this✝¹ : IsScalarTower R (Localization S) Mₚ
this✝ : IsScalarTower (Localization S) Rₚ Mₚ
l : LocalizedModule S M →ₗ[Localization S] LocalizedModule p'.primeCompl M :=
  LinearMap.extendScalarsOfIsLocalization S (Localization S)
    (IsLocalizedModule.liftOfLE S p'.primeCompl hp' (LocalizedModule.mkLinearMap S M)
      (LocalizedModule.mkLinearMap p'.primeCompl M))
this : IsLocalizedModule p.asIdeal.primeCompl l
⊢ p ∈ freeLocus (Localization S) (LocalizedModule S M) ↔ comap (algebraMap R (Localization S)) p ∈ freeLocus R M

Tactic:
rw [mem_freeLocus_of_isLocalization (R := Localization S) p Rₚ Mₚ l]

Goal state after:
R : Type uR
M : Type uM
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submonoid R
p : PrimeSpectrum (Localization S)
p' : Ideal R := Ideal.comap (algebraMap R (Localization S)) p.asIdeal
hp' : S ≤ p'.primeCompl
Rₚ : Type uR := Localization.AtPrime p'
Mₚ : Type (max uR uM) := LocalizedModule p'.primeCompl M
this✝⁵ : Algebra (Localization S) Rₚ :=
  IsLocalization.localizationAlgebraOfSubmonoidLe (Localization S) Rₚ S p'.primeCompl hp'
this✝⁴ : IsScalarTower R (Localization S) Rₚ
this✝³ : IsLocalization.AtPrime Rₚ p.asIdeal
this✝² : Module (Localization S) Mₚ := compHom Mₚ (algebraMap (Localization S) Rₚ)
this✝¹ : IsScalarTower R (Localization S) Mₚ
this✝ : IsScalarTower (Localization S) Rₚ Mₚ
l : LocalizedModule S M →ₗ[Localization S] LocalizedModule p'.primeCompl M :=
  LinearMap.extendScalarsOfIsLocalization S (Localization S)
    (IsLocalizedModule.liftOfLE S p'.primeCompl hp' (LocalizedModule.mkLinearMap S M)
      (LocalizedModule.mkLinearMap p'.primeCompl M))
this : IsLocalizedModule p.asIdeal.primeCompl l
⊢ Free Rₚ Mₚ ↔ comap (algebraMap R (Localization S)) p ∈ freeLocus R M
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: case refine_1
α : Type u_1
M : Matroid α
I B : Set α
hI : M.Indep I
hB : M.Indep B ∧ ∀ ⦃t : Set α⦄, M.Indep t → B ⊆ t → B = t
hIb : M.IsBase I
I' : Set α
hII' : M.Indep I'
hI' : I ⊆ I'
hne : ¬I = I'
⊢ False

Tactic:
exact hne <| hIb.eq_of_subset_indep hII' hI'

Goal state after:
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
K : IntermediateField F E
this : FiniteDimensional F E
h✝ : Finite F
α : ↥K
h : F⟮α⟯ = ⊤
⊢ F⟮↑α⟯ = K

Tactic:
by simpa only [lift_adjoin_simple, lift_top] using congr_arg lift h

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hI : M.Indep I
hIX : I ⊆ X
hmax : ∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → J ⊆ X → J ⊆ I
hX : X ⊆ M.E
⊢ ∀ (J : Set α), M.Indep J → I ⊆ J → J ⊆ X → I = J

Tactic:
exact fun J hJ hIJ hJX ↦ hIJ.antisymm (hmax hJ hIJ hJX)

Goal state after:
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:
by
  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.RingTheory.PicardGroup

Goal state before:
pp: R : Type u_5
inst✝³ : CommRing R
inst✝² : IsFractionRing R R
I J : Ideal R
inst✝¹ : Module.Invertible R ↥I
inst✝ : Module.Invertible R ↥J
h : Pic.mk R (↥I ⊗[R] ↥J) = 1
e✝ : ↥I ⊗[R] ↥J ≃ₗ[R] R
e : R ≃ₗ[R] ↥(I * J)
this : IsUnit ↑(e 1)
⊢ I = ⊤ ∧ J = ⊤

Tactic:
constructor <;> refine eq_top_of_isUnit_mem _ ?_ this

Goal state after:
case left
R : Type u_5
inst✝³ : CommRing R
inst✝² : IsFractionRing R R
I J : Ideal R
inst✝¹ : Module.Invertible R ↥I
inst✝ : Module.Invertible R ↥J
h : Pic.mk R (↥I ⊗[R] ↥J) = 1
e✝ : ↥I ⊗[R] ↥J ≃ₗ[R] R
e : R ≃ₗ[R] ↥(I * J)
this : IsUnit ↑(e 1)
⊢ ↑(e 1) ∈ I

case right
R : Type u_5
inst✝³ : CommRing R
inst✝² : IsFractionRing R R
I J : Ideal R
inst✝¹ : Module.Invertible R ↥I
inst✝ : Module.Invertible R ↥J
h : Pic.mk R (↥I ⊗[R] ↥J) = 1
e✝ : ↥I ⊗[R] ↥J ≃ₗ[R] R
e : R ≃ₗ[R] ↥(I * J)
this : IsUnit ↑(e 1)
⊢ ↑(e 1) ∈ J
Module: Mathlib.Combinatorics.Matroid.Dual

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

Tactic:
by
  simp_rw [dep_iff, dual_indep_iff_exists', dual_ground, and_congr_left_iff, not_and,
    not_exists, not_and, not_disjoint_iff_nonempty_inter, Classical.imp_iff_right_iff,
    iff_true_intro Or.inl]

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:
rw [← h]

Goal state after:
α : Type u_1
M : Matroid α
R : Set α
h : M ↾ R = M
⊢ R = (M ↾ R).E
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 J : Set α
hI : Indep I
hJ : Indep J
hIJ : I.encard < J.encard
⊢ I.ncard < J.ncard

Tactic:
← Nat.cast_lt (α := ℕ∞),

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 J : Set α
hI : Indep I
hJ : Indep J
hIJ : I.encard < J.encard
⊢ ↑I.ncard < ↑J.ncard
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ : Set α
M✝ : Matroid α
N : Matroid β
M : Matroid α
f : α → β
hf : InjOn f M.E
I : Set β
⊢ (∃ I₀, M.Indep (Subtype.val '' I₀) ∧ I = ⇑{ toFun := M.E.domRestrict f, inj' := ⋯ } '' I₀) ↔
    ∃ I₀, M.Indep I₀ ∧ I = f '' I₀

Tactic:
Embedding.coeFn_mk,

Goal state after:
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ : Set α
M✝ : Matroid α
N : Matroid β
M : Matroid α
f : α → β
hf : InjOn f M.E
I : Set β
⊢ (∃ I₀, M.Indep (Subtype.val '' I₀) ∧ I = (fun a ↦ M.E.domRestrict f a) '' I₀) ↔ ∃ I₀, M.Indep I₀ ∧ I = f '' I₀
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

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

Tactic:
obtain ⟨I, hI⟩ := M.exists_isBasis' X
  rw [← hI.eRk_eq_eRk, hI.isBasis_inter_ground.eRk_eq_eRk]

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

Goal state before:
pp: case inr
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ∈ M.closure {f}
h : f ∈ M.E → f ∈ M.loops
hf : f ∉ M.E
⊢ M.closure (M.E ∩ {f}) = M.loops

Tactic:
inter_singleton_eq_empty.mpr hf,

Goal state after:
case inr
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ∈ M.closure {f}
h : f ∈ M.E → f ∈ M.loops
hf : f ∉ M.E
⊢ M.closure ∅ = M.loops
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ≠ f
h : M.closure {e} = M.closure {f}
⊢ e ∈ M.closure {?m.32}

Tactic:
rw [← h]

Goal state after:
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ≠ f
h : M.closure {e} = M.closure {f}
⊢ e ∈ M.closure {e}
Module: Mathlib.Combinatorics.Matroid.Loop

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

Tactic:
indep_singleton

Goal state after:
case inr.inl
α : Type u_1
M : Matroid α
f : α
hf : M.IsNonloop f
x : α
he : M.IsNonloop x
hne : x ≠ f
hi : ¬M.Indep {x, f}
⊢ M.IsNonloop f
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

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

Tactic:
exact M.eRk_compl_union_add_eRk_compl_inter_le (insert e X) (insert e Y)

Goal state after:
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}

Tactic:
indep_singleton

Goal state after:
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.IsNonloop e