mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Lie.Weights.IsSimple

Goal state before:
pp: case mp
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : FiniteDimensional K L
inst✝² : IsKilling K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
q : Submodule K (Dual K ↥H)
hq : ∀ (i : ↥LieSubalgebra.root), q ∈ End.invtSubmodule ↑((rootSystem H).reflection i)
α : ↥LieSubalgebra.root
J : LieIdeal K L := ⋯
⊢ α ∈ J.rootSet → (rootSystem H).root α ∈ q

Tactic:
intro hα_mem

Goal state after:
case mp
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : FiniteDimensional K L
inst✝² : IsKilling K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
q : Submodule K (Dual K ↥H)
hq : ∀ (i : ↥LieSubalgebra.root), q ∈ End.invtSubmodule ↑((rootSystem H).reflection i)
α : ↥LieSubalgebra.root
J : LieIdeal K L := invtSubmoduleToLieIdeal q hq
hα_mem : α ∈ J.rootSet
⊢ (rootSystem H).root α ∈ q
Module: Mathlib.RingTheory.Extension.Presentation.Basic

Goal state before:
pp: case a
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_1
inst✝¹ : CommRing T
inst✝ : Algebra R T
P : Presentation R S ι σ
x : MvPolynomial ι T
y : σ
hy : (fun i ↦ (MvPolynomial.map (algebraMap R T)) (P.relation i)) y = x
Z : TensorProduct.includeRight ((aeval P.val) (P.relation y)) = TensorProduct.includeRight 0
⊢ x ∈ ↑(RingHom.ker (aeval (Generators.baseChange T P.toGenerators).val))

Tactic:
rw [map_zero] at Z

Goal state after:
case a
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_1
inst✝¹ : CommRing T
inst✝ : Algebra R T
P : Presentation R S ι σ
x : MvPolynomial ι T
y : σ
hy : (fun i ↦ (MvPolynomial.map (algebraMap R T)) (P.relation i)) y = x
Z : TensorProduct.includeRight ((aeval P.val) (P.relation y)) = 0
⊢ x ∈ ↑(RingHom.ker (aeval (Generators.baseChange T P.toGenerators).val))
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
r : R
x : P.Cotangent
⊢ (r • x).val = r • x.val

Tactic:
rw [← algebraMap_smul P.Ring, val_smul', algebraMap_smul]

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 : Generators R S ι
s : Set S
hs : adjoin R s = ⊤
⊢ adjoin R (Set.range Subtype.val) = ⊤

Tactic:
Subtype.range_coe_subtype,

Goal state after:
R : Type u
S : Type v
ι : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Generators R S ι
s : Set S
hs : adjoin R s = ⊤
⊢ adjoin R {x | x ∈ s} = ⊤
Module: Mathlib.Algebra.Module.Presentation.Differentials

Goal state before:
pp: R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S ι σ
φ : (σ →₀ S) →ₗ[pres.Ring] pres.toExtension.Cotangent := { toFun := ⇑(hom₁ pres), map_add' := ⋯, map_smul' := ⋯ }
⊢ Function.Surjective ⇑(hom₁ pres)

Tactic:
change Function.Surjective φ

Goal state after:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S ι σ
φ : (σ →₀ S) →ₗ[pres.Ring] pres.toExtension.Cotangent := { toFun := ⇑(hom₁ pres), map_add' := ⋯, map_smul' := ⋯ }
⊢ Function.Surjective ⇑φ
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 : Generators R S ι
ι' : Type u_1
T : Type ?u.18
inst✝¹ : CommRing T
inst✝ : Algebra R T
σ : Type u_2
I : Ideal (MvPolynomial σ R)
s✝ : MvPolynomial σ R ⧸ I → MvPolynomial σ R
hs✝ : ∀ (x : MvPolynomial σ R ⧸ I), (Ideal.Quotient.mk I) (s✝ x) = x
s : MvPolynomial σ R ⧸ I → MvPolynomial σ R
hs : ∀ (x : MvPolynomial σ R ⧸ I), (Ideal.Quotient.mk I) (s x) = x
x : MvPolynomial σ R ⧸ I
| x

Tactic:
rw [← hs x, ← Ideal.Quotient.mkₐ_eq_mk R, aeval_unique (Ideal.Quotient.mkₐ _ I)]

Goal state after:
R : Type u
S : Type v
ι : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Generators R S ι
ι' : Type u_1
T : Type ?u.18
inst✝¹ : CommRing T
inst✝ : Algebra R T
σ : Type u_2
I : Ideal (MvPolynomial σ R)
s✝ : MvPolynomial σ R ⧸ I → MvPolynomial σ R
hs✝ : ∀ (x : MvPolynomial σ R ⧸ I), (Ideal.Quotient.mk I) (s✝ x) = x
s : MvPolynomial σ R ⧸ I → MvPolynomial σ R
hs : ∀ (x : MvPolynomial σ R ⧸ I), (Ideal.Quotient.mk I) (s x) = x
x : MvPolynomial σ R ⧸ I
| (aeval (⇑(Ideal.Quotient.mkₐ R I) ∘ X)) (s x)
Module: Mathlib.LinearAlgebra.TensorProduct.Vanishing

Goal state before:
pp: case refine_1
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : Fintype ι
m : ι → M
n : ι → N
hm : span R (Set.range m) = ⊤
hmn : ∑ i, m i ⊗ₜ[R] n i = 0
G : (ι →₀ R) →ₗ[R] M := linearCombination R m
hG : G = linearCombination R m
G_basis_eq : ∀ (i : ι), G (Finsupp.single i 1) = m i
G_surjective : Surjective ⇑G
en : (ι →₀ R) ⊗[R] N := ∑ i, Finsupp.single i 1 ⊗ₜ[R] n i
hen : en = ∑ i, Finsupp.single i 1 ⊗ₜ[R] n i
en_mem_ker : en ∈ (rTensor N G).ker
exact_ker_subtype : Exact ⇑G.ker.subtype ⇑G
exact_rTensor_ker_subtype : Exact ⇑(rTensor N G.ker.subtype) ⇑(rTensor N G)
ma : Finset (↥G.ker × N)
hkn : (rTensor N G.ker.subtype) (∑ kj ∈ ma, kj.1 ⊗ₜ[R] kj.2) = en
i : ι
⊢ n i =
    ∑ j,
      (match j with
        | ⟨(kj, snd), property⟩ => ↑kj i) •
        match j with
        | ⟨(fst, yj), property⟩ => yj

Tactic:
apply_fun finsuppScalarLeft R N ι at hkn
    apply_fun (· i) at hkn
    symm at hkn
    simp only [map_sum, finsuppScalarLeft_apply_tmul, zero_smul, Finsupp.single_zero,
      Finsupp.sum_single_index, one_smul, Finsupp.finsetSum_apply, Finsupp.single_apply,
      Finset.sum_ite_eq', Finset.mem_univ, ↓reduceIte, rTensor_tmul, coe_subtype, Finsupp.sum_apply,
      Finsupp.sum_ite_eq', Finsupp.mem_support_iff, ne_eq, ite_not, en] at hkn
    simp only [Finset.univ_eq_attach, Finset.sum_attach ma (fun x ↦ (x.1 : ι →₀ R) i • x.2)]
    convert! hkn using 2 with x _
    split
    · next h'x => rw [h'x, zero_smul]
    · rfl

Goal state after:
Module: Mathlib.RingTheory.Support

Goal state before:
pp: case a.refine_2
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
I : Ideal R
⊢ I ≤ annihilator R (M ⧸ I • ⊤)

Tactic:
rw [Submodule.annihilator_quotient]

Goal state after:
case a.refine_2
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
I : Ideal R
⊢ I ≤ (I • ⊤).colon Set.univ
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
⊢ ⊤.spanRank ≤ Cardinal.lift.{u_2, u_3} N.spanRank

Tactic:
← Submodule.baseChange_top,

Goal state after:
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
⊢ (baseChange A ⊤).spanRank ≤ Cardinal.lift.{u_2, u_3} N.spanRank
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
⊢ ⊤.spanFinrank ≤ N.spanFinrank

Tactic:
← Submodule.baseChange_top,

Goal state after:
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 ⊤).spanFinrank ≤ N.spanFinrank
Module: Mathlib.LinearAlgebra.ExteriorPower.Basis

Goal state before:
pp: R : Type u_1
M : Type u_3
n : ℕ
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Nontrivial R
inst✝¹ : Free R M
inst✝ : Module.Finite R M
⊢ finrank R ↥(⋀[R]^n M) = (finrank R M).choose n

Tactic:
by
  classical
  let : LinearOrder (Module.Free.ChooseBasisIndex R M) := linearOrderOfSTO WellOrderingRel
  let B := (Module.Free.chooseBasis R M).exteriorPower n
  rw [Module.finrank_eq_card_basis (Module.Free.chooseBasis R M), Module.finrank_eq_card_basis B,
    Fintype.card_eq_nat_card, powersetCard.card, Fintype.card_eq_nat_card]

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

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

Tactic:
refine lTensor_injective_of_exact_of_exact_of_rTensor_injective
      (N₁ := LinearMap.ker i) (N₂ := ι →₀ R) (N₃ := M)
      (f₁ := (𝔪).subtype) (f₂ := Submodule.mkQ 𝔪)
      (g₁ := (LinearMap.ker i).subtype) (g₂ := i) (LinearMap.exact_subtype_mkQ 𝔪)
      (Submodule.mkQ_surjective _) (LinearMap.exact_subtype_ker_map i) hi H ?_ ?_

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

case refine_2
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : FinitePresentation R M
ι : Type u_5
v : ι → M
hli : LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v)
hsp : Submodule.span k (Set.range (⇑((TensorProduct.mk R k M) 1) ∘ v)) = ⊤
H : Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype 𝔪))
bk : Basis ι k (k ⊗[R] M) := Basis.mk hli ⋯
this✝² : Finite ι
this✝¹ : Fintype ι := Fintype.ofFinite ι
i : (ι →₀ R) →ₗ[R] M := Finsupp.linearCombination R v
hi : Surjective ⇑i
this✝ : Module.Finite R ↥i.ker
this : Surjective ⇑(LinearMap.baseChange k i)
hi' : Function.Bijective ⇑(LinearMap.baseChange k i)
x : k ⊗[R] ↥i.ker
⊢ (LinearMap.lTensor (R ⧸ 𝔪) i.ker.subtype) x = (LinearMap.lTensor (R ⧸ 𝔪) i.ker.subtype) 0
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
hI : I ∈ (N.colon {x}).minimalPrimes
hx : x ∉ N
⊢ ∃ x', I = N.colon {x'}

Tactic:
(Mathlib.Tactic.setTactic
 "set"
 []
 (Mathlib.Tactic.setArgsRest
  (Lean.binderIdent `ann)
  []
  ":="
  (Term.app
   `colon
   [`N
    (choice
     («term{_}» "{" [`x] "}")
     (Term.structInst
      "{"
      []
      (Term.structInstFields [(Term.structInstField (Term.structInstLVal `x []) [])])
      (Term.optEllipsis [])
      []
      "}"))])
  []))

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
⊢ ∃ x', I = N.colon {x'}
Module: Mathlib.RingTheory.LocalRing.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsLocalRing R
inst✝¹ : Module.Finite R M
inst✝ : Flat R M
ι : Type u
v : ι → M
h : Function.Bijective ⇑(linearCombination k (⇑((TensorProduct.mk R k M) 1) ∘ v))
⊢ Function.Bijective ⇑(linearCombination R v)

Tactic:
use linearIndependent_of_flat _ h.1

Goal state after:
case right
R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsLocalRing R
inst✝¹ : Module.Finite R M
inst✝ : Flat R M
ι : Type u
v : ι → M
h : Function.Bijective ⇑(linearCombination k (⇑((TensorProduct.mk R k M) 1) ∘ v))
⊢ Surjective ⇑(linearCombination R v)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup

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

Tactic:
· simpa [hIK] using (inferInstance : (Ideal.span {a}).IsPrincipal)

Goal state after:
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
p₁ p₂ : PrimeSpectrum (S ⊗[R] T)
h : tensorProductTo R S T p₁ = tensorProductTo R S T p₂
g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom
⊢ p₁ ≤ p₂

Tactic:
intro x hxp₁

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
p₁ p₂ : PrimeSpectrum (S ⊗[R] T)
h : tensorProductTo R S T p₁ = tensorProductTo R S T p₂
g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom
x : S ⊗[R] T
hxp₁ : x ∈ p₁.asIdeal
⊢ x ∈ p₂.asIdeal
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
I : (FractionalIdeal R⁰ K)ˣ
⊢ (↑↑I).IsPrincipal → ∃ x, spanSingleton R⁰ ↑x = ↑I

Tactic:
intro hI

Goal state after:
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⁰ K)ˣ
hI : (↑↑I).IsPrincipal
⊢ ∃ x, spanSingleton R⁰ ↑x = ↑I
Module: Mathlib.RingTheory.Localization.Free

Goal state before:
pp: R : Type u_4
M : Type u_5
inst✝¹³ : CommRing R
inst✝¹² : AddCommGroup M
inst✝¹¹ : Module R M
S : Submonoid R
M' : Type u_1
inst✝¹⁰ : AddCommGroup M'
inst✝⁹ : Module R M'
f : M →ₗ[R] M'
inst✝⁸ : IsLocalizedModule S f
Rₛ : Type u_3
inst✝⁷ : CommRing Rₛ
inst✝⁶ : Algebra R Rₛ
inst✝⁵ : Module Rₛ M'
inst✝⁴ : IsScalarTower R Rₛ M'
inst✝³ : Nontrivial Rₛ
inst✝² : IsLocalization S Rₛ
inst✝¹ : FinitePresentation R M
inst✝ : Free Rₛ M'
⊢ ∃ r ∈ S,
    Free (Localization (Submonoid.powers r)) (LocalizedModule.Away r M) ∧
      finrank (Localization (Submonoid.powers r)) (LocalizedModule.Away r M) = finrank Rₛ M'

Tactic:
let I := Module.Free.ChooseBasisIndex Rₛ M'

Goal state after:
R : Type u_4
M : Type u_5
inst✝¹³ : CommRing R
inst✝¹² : AddCommGroup M
inst✝¹¹ : Module R M
S : Submonoid R
M' : Type u_1
inst✝¹⁰ : AddCommGroup M'
inst✝⁹ : Module R M'
f : M →ₗ[R] M'
inst✝⁸ : IsLocalizedModule S f
Rₛ : Type u_3
inst✝⁷ : CommRing Rₛ
inst✝⁶ : Algebra R Rₛ
inst✝⁵ : Module Rₛ M'
inst✝⁴ : IsScalarTower R Rₛ M'
inst✝³ : Nontrivial Rₛ
inst✝² : IsLocalization S Rₛ
inst✝¹ : FinitePresentation R M
inst✝ : Free Rₛ M'
I : Type u_1 := Free.ChooseBasisIndex Rₛ M'
⊢ ∃ r ∈ S,
    Free (Localization (Submonoid.powers r)) (LocalizedModule.Away r M) ∧
      finrank (Localization (Submonoid.powers r)) (LocalizedModule.Away r M) = finrank Rₛ M'
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
M : Type u_3
N : Type u_4
M' : Type u_5
N' : Type u_6
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R M
inst✝⁶ : Module R N
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid N'
inst✝³ : Module R M'
inst✝² : Module R N'
f : M →ₗ[R] M'
g : N →ₗ[R] N'
inst✝¹ : IsLocalizedModule S f
inst✝ : IsLocalizedModule S g
this : Module (Localization S) M' := module S f
⊢ IsLocalizedModule S (f.prodMap g)

Tactic:
let : Module (Localization S) N' := IsLocalizedModule.module S g

Goal state after:
R : Type u_1
S✝ : Type u_2
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S✝
inst✝¹⁰ : Algebra R S✝
S : Submonoid R
M : Type u_3
N : Type u_4
M' : Type u_5
N' : Type u_6
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R M
inst✝⁶ : Module R N
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid N'
inst✝³ : Module R M'
inst✝² : Module R N'
f : M →ₗ[R] M'
g : N →ₗ[R] N'
inst✝¹ : IsLocalizedModule S f
inst✝ : IsLocalizedModule S g
this✝ : Module (Localization S) M' := module S f
this : Module (Localization S) N' := module S g
⊢ IsLocalizedModule S (f.prodMap g)
Module: Mathlib.FieldTheory.Minpoly.Finite

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
inst✝ : Module.Finite A B
x : B
⊢ (minpoly A x).natDegree ≤ ⊤.spanFinrank

Tactic:
rcases LinearMap.exists_monic_and_natDegree_eq_and_aeval_eq_zero _ (Algebra.lmul A _ x) with
    ⟨f, f_monic, f_deg, f_aeval⟩

Goal state after:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
inst✝ : Module.Finite A B
x : B
f : A[X]
f_monic : f.Monic
f_deg : f.natDegree = ⊤.spanFinrank
f_aeval : (Polynomial.aeval ((Algebra.lmul A B) x)) f = 0
⊢ (minpoly A x).natDegree ≤ ⊤.spanFinrank
Module: Mathlib.RingTheory.LocalRing.ResidueField.Fiber

Goal state before:
pp: case mpr
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
p✝ : Ideal R
inst✝ : p✝.IsPrime
p : PrimeSpectrum R
q₁ q₂ : ↑(comap (algebraMap R S) ⁻¹' {p})
H : q₁ ≤ q₂
x : p.asIdeal.Fiber S
r : R
hr : r ∉ p.asIdeal
s : S
hx : 1 ⊗ₜ[R] s ∈ ((preimageEquivFiber R S p) q₁).asIdeal
e : r • x = 1 ⊗ₜ[R] s
⊢ 1 ⊗ₜ[R] s ∈ ((preimageEquivFiber R S p) q₂).asIdeal

Tactic:
replace hx : s ∈ q₁.1.asIdeal := by simpa using! hx
        simpa using! H hx

Goal state after:
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
S : Type u_7
T : Type u_8
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : R →+* S
g : S →+* T
⊢ (mapRingHom g).comp (mapRingHom f) = mapRingHom (g.comp f)

Tactic:
algebraize [f, g, g.comp f]

Goal state after:
R : Type u
inst✝² : CommSemiring R
S : Type u_7
T : Type u_8
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : R →+* S
g : S →+* T
algInst✝² : Algebra R S := f.toAlgebra
algInst✝¹ : Algebra S T := g.toAlgebra
algInst✝ : Algebra R T := (g.comp f).toAlgebra
scalarTowerInst✝ : IsScalarTower R S T := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R T))
⊢ (mapRingHom g).comp (mapRingHom f) = mapRingHom (g.comp f)
Module: Mathlib.FieldTheory.Normal.Basic

Goal state before:
pp: case inr.refine_1
F : Type u_1
inst✝² : Field F
E : Type u_3
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
this✝ : FiniteDimensional F E
hx : IsIntegral F x
L : Type u_1 := (p * minpoly F x).SplittingField
hL1 : (Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) p).Splits
j : E →ₐ[F] L := IsSplittingField.lift E p hL1
hL2 : (Polynomial.map (↑j) (Polynomial.map (algebraMap F E) (minpoly F x))).Splits
a : L
ha : a ∈ (Polynomial.map (algebraMap F L) (minpoly F x)).roots
this : Algebra (↥F⟮x⟯) L := ((algHomAdjoinIntegralEquiv F hx).symm ⟨a, ha⟩).toAlgebra
⊢ (Polynomial.map (algebraMap (↥F⟮x⟯) L) (Polynomial.map (algebraMap F ↥F⟮x⟯) p)).Splits

Tactic:
· rwa [Polynomial.map_map, ← IsScalarTower.algebraMap_eq]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.E
⊢ ¬M.Dep X ↔ M.Indep X

Tactic:
by
  rw [Dep, and_iff_left hX, not_not]

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

Goal state before:
pp: α : Type u_1
M✝ : Matroid α
B B' I✝ J D X : Set α
e f : α
M : Matroid α
inst✝ : M.RankFinite
I : Set α
hI : ∀ J ⊆ I, J.Finite → M.Indep J
⊢ M.Indep I

Tactic:
refine I.finite_or_infinite.elim (hI _ Subset.rfl) (fun h ↦ False.elim ?_)

Goal state after:
α : Type u_1
M✝ : Matroid α
B B' I✝ J D X : Set α
e f : α
M : Matroid α
inst✝ : M.RankFinite
I : Set α
hI : ∀ J ⊆ I, J.Finite → M.Indep J
h : I.Infinite
⊢ False
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
X Y : Set α
M : Matroid α
hXY : X ⊆ Y
hY : Y ⊆ M.E
I : Set α
hI : M.IsBasis I X
J : Set α
hJ : M.IsBasis J Y
hIJ : I ⊆ J
⊢ ∃ I J, M.IsBasis I X ∧ M.IsBasis J Y ∧ I ⊆ J

Tactic:
exact ⟨_, _, hI, hJ, hIJ⟩

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

Goal state before:
pp: α : Type u_1
E : Set α
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I J : Set α⦄, Indep I → Indep J → I.encard < J.encard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
indep_bdd : ∃ n, ∀ (I : Set α), Indep I → I.encard ≤ ↑n
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
I B : Set α
hI : Indep I
hImax : ¬Maximal Indep I
hBmax : Maximal Indep B
hcard : I.encard < B.encard
⊢ ∃ x ∈ B \ I, Indep (insert x I)

Tactic:
obtain ⟨e, heB, heI, hi⟩ := indep_aug hI hBmax.prop hcard

Goal state after:
α : Type u_1
E : Set α
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I J : Set α⦄, Indep I → Indep J → I.encard < J.encard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
indep_bdd : ∃ n, ∀ (I : Set α), Indep I → I.encard ≤ ↑n
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
I B : Set α
hI : Indep I
hImax : ¬Maximal Indep I
hBmax : Maximal Indep B
hcard : I.encard < B.encard
e : α
heB : e ∈ B
heI : e ∉ I
hi : Indep (insert e I)
⊢ ∃ x ∈ B \ I, Indep (insert x I)
Module: Mathlib.Combinatorics.Matroid.IndepAxioms

Goal state before:
pp: α : Type u_1
E : Set α
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I J : Set α⦄, Indep I → Indep J → I.encard < J.encard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
I B : Set α
hI : Indep I
hImax : ¬Maximal Indep I
hBmax : Maximal Indep B
hle : B.encard ≤ I.encard
x : α
hxnot : x ∉ I
hxI : Indep (insert x I)
n : ℕ
hn : ∀ (I : Set α), Indep I → I.encard ≤ ↑n
⊢ I.Finite

Tactic:
exact finite_of_encard_le_coe (hn _ hI)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
I X : Set α
⊢ (N.comap f).IsBasis' I X ↔ N.IsBasis' (f '' I) (f '' X) ∧ InjOn f I ∧ I ⊆ X

Tactic:
simp only [isBasis'_iff_isBasis_inter_ground, comap_ground_eq, comap_isBasis_iff,
    image_inter_preimage, subset_inter_iff, ← and_assoc, and_iff_left_iff_imp,
    and_imp]
  exact fun h _ _ ↦ (image_subset_iff.1 h.indep.subset_ground)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
N : Matroid β
f : α → β
⊢ N.comapOn (f ⁻¹' N.E) f = N.comap f

Tactic:
rw [comapOn, restrict_eq_self_iff]; rfl

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
I : Set α
hI : I ⊆ M.E
X : Set α
hX : X ⊆ M.E
h : (M.map f hf).IsBasis (f '' I) (f '' X)
⊢ ∃ I₀ X₀, M.IsBasis I₀ X₀ ∧ f '' I = f '' I₀ ∧ f '' X = f '' X₀

Tactic:
map_isBasis_iff _ _ hI hX

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
I : Set α
hI : I ⊆ M.E
X : Set α
hX : X ⊆ M.E
h : M.IsBasis I X
⊢ ∃ I₀ X₀, M.IsBasis I₀ X₀ ∧ f '' I = f '' I₀ ∧ f '' X = f '' X₀