mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Localization.Finiteness

Goal state before:
pp: R : Type u
inst✝¹⁰ : CommSemiring R
M : Type w
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
t : Finset R
ht : Ideal.span ↑t = ⊤
Mₚ : ↥t → Type u_1
inst✝⁷ : (g : ↥t) → AddCommMonoid (Mₚ g)
inst✝⁶ : (g : ↥t) → Module R (Mₚ g)
Rₚ : ↥t → Type u_2
inst✝⁵ : (g : ↥t) → CommSemiring (Rₚ g)
inst✝⁴ : (g : ↥t) → Algebra R (Rₚ g)
inst✝³ : ∀ (g : ↥t), IsLocalization.Away (↑g) (Rₚ g)
inst✝² : (g : ↥t) → Module (Rₚ g) (Mₚ g)
inst✝¹ : ∀ (g : ↥t), IsScalarTower R (Rₚ g) (Mₚ g)
f : (g : ↥t) → M →ₗ[R] Mₚ g
inst✝ : ∀ (g : ↥t), IsLocalizedModule.Away (↑g) (f g)
H : ∀ (g : ↥t), Module.Finite (Rₚ g) (Mₚ g)
⊢ Module.Finite R M

Tactic:
constructor
  choose s₁ s₂ using (fun g ↦ (H g).1)
  let sf := fun x : t ↦
    IsLocalizedModule.finsetIntegerMultiple (Submonoid.powers x.val) (f x) (s₁ x)
  use t.attach.biUnion sf
  rw [Submodule.span_attach_biUnion, eq_top_iff]
  rintro x -
  refine Submodule.mem_of_span_eq_top_of_smul_pow_mem _ (t : Set R) ht _ (fun r ↦ ?_)
  set S : Submonoid R := Submonoid.powers r.val
  obtain ⟨⟨_, n₁, rfl⟩, hn₁⟩ := multiple_mem_span_of_mem_localization_span S (Rₚ r)
    (s₁ r : Set (Mₚ r)) (IsLocalizedModule.mk' (f r) x (1 : S)) (by rw [s₂ r]; trivial)
  rw [Submonoid.smul_def, ← IsLocalizedModule.mk'_smul, IsLocalizedModule.mk'_one] at hn₁
  obtain ⟨⟨_, n₂, rfl⟩, hn₂⟩ := IsLocalizedModule.smul_mem_finsetIntegerMultiple_span
    S (f r) _ (s₁ r) hn₁
  rw [Submonoid.smul_def] at hn₂
  use n₂ + n₁
  apply le_iSup (fun x : t ↦ Submodule.span R (sf x : Set M)) r
  rw [pow_add, mul_smul]
  exact hn₂

Goal state after:
Module: Mathlib.Algebra.Module.StablyFree.Basic

Goal state before:
pp: R : Type u
inst✝⁵ : Ring R
M : Type v
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type w
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsStablyFree R M
⊢ Projective R M

Tactic:
by
  obtain ⟨N, _, _, _, _, _⟩ := IsStablyFree.exist_free_prod R M
  exact Projective.of_split (LinearMap.inl R M N) (LinearMap.fst R M N) (LinearMap.ext fun _ ↦ rfl)

Goal state after:
Module: Mathlib.Data.Fin.Parity

Goal state before:
pp: n : ℕ
k : Fin n
inst✝ : NeZero n
hn : Even n
⊢ ¬Odd k ↔ Even k

Tactic:
by
  rw [even_iff_of_even hn, odd_iff_of_even hn]
  exact Nat.not_odd_iff_even

Goal state after:
Module: Mathlib.Algebra.Module.SpanRankOperations

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsLocalRing R
N : Submodule R M
fg : N.FG
⊢ N.spanFinrank = Module.finrank (R ⧸ maximalIdeal R) (↥N ⧸ maximalIdeal R • ⊤)

Tactic:
let : Module 𝓀 (N ⧸ maximalIdeal R • (⊤ : Submodule R N)) :=
    inferInstanceAs (Module (R ⧸ maximalIdeal R) _)
  let : IsScalarTower R 𝓀 (N ⧸ maximalIdeal R • (⊤ : Submodule R N)) :=
    inferInstanceAs (IsScalarTower R (R ⧸ maximalIdeal R) _)
  rw [← spanFinrank_top_eq_of_residueField N fg, ← Module.finrank_eq_spanFinrank_of_free]
  let e : 𝓀 ⊗[R] N ≃ₗ[𝓀] N ⧸ (maximalIdeal R) • (⊤ : Submodule R N) :=
    (quotTensorEquivQuotSMul N (maximalIdeal R)).extendScalarsOfSurjective residue_surjective
  exact e.finrank_eq

Goal state after:
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
I : Type u_5
inst✝ : LinearOrder I
b : Basis I R M
s t : ↑(powersetCard I n)
hst : s ≠ t
k : Fin n
his : (ofFinEmbEquiv.symm s) k ∈ s
hit : (ofFinEmbEquiv.symm s) k ∉ t
j : Fin n
h : (ofFinEmbEquiv.symm s) k = (ofFinEmbEquiv.symm t) j
⊢ (ofFinEmbEquiv.symm s) k ∈ t

Tactic:
rw [h, powersetCard.ofFinEmbEquiv_symm_apply, ← powersetCard.mem_coe_iff]

Goal state after:
R : Type u_1
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Type u_5
inst✝ : LinearOrder I
b : Basis I R M
s t : ↑(powersetCard I n)
hst : s ≠ t
k : Fin n
his : (ofFinEmbEquiv.symm s) k ∈ s
hit : (ofFinEmbEquiv.symm s) k ∉ t
j : Fin n
h : (ofFinEmbEquiv.symm s) k = (ofFinEmbEquiv.symm t) j
⊢ ((↑t).orderEmbOfFin ⋯) j ∈ ↑t
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 𝔪))
ι : Type u
v : ι → M
hv : Submodule.span R (Set.range v) = ⊤
this✝ : Set.univ ⊆ ↑(Submodule.span R (Set.range (⇑((TensorProduct.mk R k M) 1) ∘ v)))
this : Submodule.span k (Set.range (⇑((TensorProduct.mk R k M) 1) ∘ v)) = ⊤
⊢ ∃ κ a b, ∀ (i : κ), b i = v (a i)

Tactic:
obtain ⟨κ, a, ha, hsp, hli⟩ := exists_linearIndependent' k (TensorProduct.mk R k M 1 ∘ v)

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 𝔪))
ι : Type u
v : ι → M
hv : Submodule.span R (Set.range v) = ⊤
this✝ : Set.univ ⊆ ↑(Submodule.span R (Set.range (⇑((TensorProduct.mk R k M) 1) ∘ v)))
this : Submodule.span k (Set.range (⇑((TensorProduct.mk R k M) 1) ∘ v)) = ⊤
κ : Type u
a : κ → ι
ha : Function.Injective a
hsp :
  Submodule.span k (Set.range ((⇑((TensorProduct.mk R k M) 1) ∘ v) ∘ a)) =
    Submodule.span k (Set.range (⇑((TensorProduct.mk R k M) 1) ∘ v))
hli : LinearIndependent k ((⇑((TensorProduct.mk R k M) 1) ∘ v) ∘ a)
⊢ ∃ κ a b, ∀ (i : κ), b i = v (a i)
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 𝔪))
w✝¹ : Type u_2
w✝ : w✝¹ → M
b : Basis w✝¹ R M
h✝ : ∀ (i : w✝¹), b i = id (w✝ i)
⊢ Free R M

Tactic:
exact Free.of_basis b

Goal state after:
Module: Mathlib.LinearAlgebra.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝ : Flat R ↥N
κ : Type u_1
ι : Type u_2
m : κ → ↥M
n : ι → ↥N
hm : Function.Injective ⇑(Finsupp.linearCombination R m)
hn : Function.Injective ⇑(Finsupp.linearCombination R n)
i0 : (κ × ι →₀ R) ≃ₗ[R] (κ →₀ R) ⊗[R] (ι →₀ R) := (finsuppTensorFinsupp' R κ ι).symm
i1 : (κ →₀ R) ⊗[R] (ι →₀ R) →ₗ[R] (κ →₀ R) ⊗[R] ↥N := LinearMap.lTensor (κ →₀ R) (Finsupp.linearCombination R n)
⊢ Function.Injective ⇑(Finsupp.linearCombination R fun i ↦ ↑(m i.1) * ↑(n i.2))

Tactic:
let i2 := LinearMap.rTensor N (Finsupp.linearCombination R m)

Goal state after:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝ : Flat R ↥N
κ : Type u_1
ι : Type u_2
m : κ → ↥M
n : ι → ↥N
hm : Function.Injective ⇑(Finsupp.linearCombination R m)
hn : Function.Injective ⇑(Finsupp.linearCombination R n)
i0 : (κ × ι →₀ R) ≃ₗ[R] (κ →₀ R) ⊗[R] (ι →₀ R) := (finsuppTensorFinsupp' R κ ι).symm
i1 : (κ →₀ R) ⊗[R] (ι →₀ R) →ₗ[R] (κ →₀ R) ⊗[R] ↥N := LinearMap.lTensor (κ →₀ R) (Finsupp.linearCombination R n)
i2 : (κ →₀ R) ⊗[R] ↥N →ₗ[R] ↥M ⊗[R] ↥N := LinearMap.rTensor (↥N) (Finsupp.linearCombination R m)
⊢ Function.Injective ⇑(Finsupp.linearCombination R fun i ↦ ↑(m i.1) * ↑(n i.2))
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
⊢ x.lifts.Nonempty

Tactic:
existsi Quot.out x

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
⊢ Quot.out x ∈ x.lifts
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: case refine_1
ι : 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)
E : Type u_9
inst✝¹ : AddCommMonoid E
inst✝ : Module R E
φ : MultilinearMap R s E
r : R
x : ⨂[R] (i : ι), s i
z : R
f : (i : ι) → s i
⊢ (liftAux φ) (tprodCoeff R (r • z) f) = r • (liftAux φ) (tprodCoeff R z f)

Tactic:
liftAux_tprodCoeff,

Goal state after:
case refine_1
ι : 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)
E : Type u_9
inst✝¹ : AddCommMonoid E
inst✝ : Module R E
φ : MultilinearMap R s E
r : R
x : ⨂[R] (i : ι), s i
z : R
f : (i : ι) → s i
⊢ (r • z) • φ f = r • (liftAux φ) (tprodCoeff R z f)
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: case refine_1
ι : 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)
E : Type u_9
inst✝¹ : AddCommMonoid E
inst✝ : Module R E
φ : MultilinearMap R s E
r : R
x : ⨂[R] (i : ι), s i
z : R
f : (i : ι) → s i
⊢ (r • z) • φ f = r • (liftAux φ) (tprodCoeff R z f)

Tactic:
liftAux_tprodCoeff,

Goal state after:
case refine_1
ι : 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)
E : Type u_9
inst✝¹ : AddCommMonoid E
inst✝ : Module R E
φ : MultilinearMap R s E
r : R
x : ⨂[R] (i : ι), s i
z : R
f : (i : ι) → s i
⊢ (r • z) • φ f = r • z • φ f
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:
by
  use linearIndependent_of_flat _ h.1
  rw [← LinearMap.range_eq_top, range_linearCombination]
  refine span_eq_top_of_tmul_eq_basis _ (.mk h.1 ?_) fun _ ↦ ?_
  · simpa only [top_le_iff, ← range_linearCombination, LinearMap.range_eq_top] using h.2
  · simp

Goal state after:
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Colon

Goal state before:
pp: case pos
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
hz : z ∉ I
hz' : K * Ideal.span {z} ≤ ann
hK : I ^ (n - 1) * (J * Ideal.span {z}) ≤ ann ∧ ¬J * Ideal.span {z} ≤ I
hn' : n - 1 = 0
⊢ False

Tactic:
simp [K, show n = 1 by grind] at hz'

Goal state after:
case pos
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
hz : z ∉ I
hK : I ^ (n - 1) * (J * Ideal.span {z}) ≤ ann ∧ ¬J * Ideal.span {z} ≤ I
hn' : n - 1 = 0
hz' : J * Ideal.span {z} ≤ ann
⊢ False
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝ : TopologicalSpace X
⊢ Function.Injective LocallyConstant.toFun

Tactic:
rintro ⟨_, _⟩ ⟨_, _⟩ _

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝ : TopologicalSpace X
toFun✝¹ : X → Y
isLocallyConstant✝¹ : IsLocallyConstant toFun✝¹
toFun✝ : X → Y
isLocallyConstant✝ : IsLocallyConstant toFun✝
a✝ :
  { toFun := toFun✝¹, isLocallyConstant := isLocallyConstant✝¹ }.toFun =
    { toFun := toFun✝, isLocallyConstant := isLocallyConstant✝ }.toFun
⊢ { toFun := toFun✝¹, isLocallyConstant := isLocallyConstant✝¹ } =
    { toFun := toFun✝, isLocallyConstant := isLocallyConstant✝ }
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X : Type u_5
inst✝¹ : TopologicalSpace X
U : Set X
inst✝ : (x : X) → Decidable (x ∈ U)
hU : IsClopen U
x✝ : X
⊢ x✝ ∈ ⇑(ofIsClopen hU) ⁻¹' {1} ↔ x✝ ∈ Uᶜ

Tactic:
simp only [ofIsClopen, mem_singleton_iff, coe_mk, Fin.zero_eq_one_iff, mem_preimage,
    ite_eq_right_iff, mem_compl_iff, Nat.succ_succ_ne_one]

Goal state after:
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: case refine_2
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
C₁ C₂ : Set X
h₁ : IsClosed[inst✝¹] C₁
h₂ : IsClosed[inst✝¹] C₂
h✝ : C₁ ∪ C₂ = univ
h : (⋃ b, bif b then C₁ else C₂) = univ
inst✝ : DecidablePred fun x ↦ x ∈ C₁
dZ : TopologicalSpace Z := ⊥
this : DiscreteTopology Z
f : ↑C₁ → Z
hf✝ : IsLocallyConstant f
hf : Continuous[instTopologicalSpaceSubtype, dZ] f
g : ↑C₂ → Z
hg✝ : IsLocallyConstant g
hg : Continuous[instTopologicalSpaceSubtype, dZ] g
hfg :
  ∀ (x : X) (hx : x ∈ C₁ ∩ C₂),
    { toFun := f, isLocallyConstant := hf✝ } ⟨x, ⋯⟩ = { toFun := g, isLocallyConstant := hg✝ } ⟨x, ⋯⟩
i : Bool
⊢ ContinuousOn (fun i ↦ if hi : i ∈ C₁ then f ⟨i, hi⟩ else g ⟨i, ⋯⟩) (bif i then C₁ else C₂)

Tactic:
· cases i <;> rw [continuousOn_iff_continuous_domRestrict]
      · convert! hg
        ext x
        simp only [cond_false, domRestrict_apply, Subtype.coe_eta, dite_eq_right_iff]
        exact fun hx ↦ hfg x ⟨hx, x.prop⟩
      · simp only [cond_true, domRestrict_dite, Subtype.coe_eta]
        exact hf

Goal state after:
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : Nontrivial G
n : ℕ
hn : _root_.commutator G = ⊤
⊢ derivedSeries G n ≠ ⊥

Tactic:
refine ne_of_eq_of_ne ?_ top_ne_bot

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : Nontrivial G
n : ℕ
hn : _root_.commutator G = ⊤
⊢ derivedSeries G n = ⊤
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
M : Type v
N : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
e : M ⊗[R] N ≃ₗ[R] R
⊢ contractLeft R N = ↑e ∘ₗ ↑(LinearEquiv.rTensor N (linearEquivDual e)).symm

Tactic:
LinearEquiv.eq_comp_toLinearMap_symm

Goal state after:
R : Type u
M : Type v
N : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
e : M ⊗[R] N ≃ₗ[R] R
⊢ contractLeft R N ∘ₗ ↑(LinearEquiv.rTensor N (linearEquivDual e)) = ↑e
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: ⊢ ¬Group.IsSolvable (Perm (Fin 5))

Tactic:
let x : Equiv.Perm (Fin 5) := ⟨![1, 2, 0, 3, 4], ![2, 0, 1, 3, 4], by decide, by decide⟩
  let y : Equiv.Perm (Fin 5) := ⟨![3, 4, 2, 0, 1], ![3, 4, 2, 0, 1], by decide, by decide⟩
  let z : Equiv.Perm (Fin 5) := ⟨![0, 3, 2, 1, 4], ![0, 3, 2, 1, 4], by decide, by decide⟩
  have key : x = z * ⁅x, y * x * y⁻¹⁆ * z⁻¹ := by unfold x y z; decide
  refine not_isSolvable_of_mem_derivedSeries (show x ≠ 1 by decide) fun n => ?_
  induction n with
  | zero => exact mem_top x
  | succ n ih =>
    rw [key, (derivedSeries_normal _ _).mem_comm_iff, inv_mul_cancel_left]
    exact commutator_mem_commutator ih ((derivedSeries_normal _ _).conj_mem _ ih _)

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✝¹ : Flat R M
inst✝ : Module.Finite R M
p : PrimeSpectrum R
h : finrank (Localization.AtPrime p.asIdeal) (LocalizedModule p.asIdeal.primeCompl M) = 0
⊢ Module.rank (Localization.AtPrime p.asIdeal) (LocalizedModule p.asIdeal.primeCompl M) = 0

Tactic:
simp [← finrank_eq_rank, h]

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
inst✝² : Algebra.IsAlgebraic F K
h✝ : ∀ (x : K), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits
L' : Type u_4
inst✝¹ : Field L'
inst✝ : Algebra F L'
φ : ↥(⨆ x, IntermediateField.adjoin F ((minpoly F x).rootSet L')) →ₐ[F] L := ⋯.some
φ' : ↥(normalClosure F K L') →ₐ[F] L := φ.comp (inclusion ⋯)
x✝¹ x✝ : K →ₐ[F] L'
h : (φ'.comp ∘ ⇑(normalClosure.algHomEquiv F K L').symm) x✝¹ = (φ'.comp ∘ ⇑(normalClosure.algHomEquiv F K L').symm) x✝
⊢ (normalClosure.algHomEquiv F K L').symm x✝¹ = (normalClosure.algHomEquiv F K L').symm x✝

Tactic:
by
      rw [DFunLike.ext'_iff] at h ⊢
      exact φ'.injective.comp_left h

Goal state after:
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
h : ∀ (a : Type u) (b : AddCommMonoid a) (c : Module R a) (d : Module.Invertible R a), Pic.mk R a = 1
M N : Pic R
⊢ M = N

Tactic:
rw [← mk_eq_self (M := M), ← mk_eq_self (M := N), h, h]

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

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

Tactic:
dep_iff,

Goal state after:
α : Type u_1
M : Matroid α
I : Set α
⊢ M.Indep I ↔ ¬(¬M.Indep I ∧ I ⊆ M.E) ∧ I ⊆ M.E
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
B : Set α
e f : α
hB : M.IsBase B
hf : f ∉ B
hI : M.Indep (insert f (B \ {e}))
B' : Set α
hB' : M.IsBase B'
hIB' : f ∈ B' ∧ B \ B' ⊆ {e}
hcard : (B' \ B).encard = (B \ B').encard
⊢ M.IsBase (insert f (B \ {e}))

Tactic:
subset_singleton_iff_eq

Goal state after:
α : Type u_1
M : Matroid α
B : Set α
e f : α
hB : M.IsBase B
hf : f ∉ B
hI : M.Indep (insert f (B \ {e}))
B' : Set α
hB' : M.IsBase B'
hIB' : f ∈ B' ∧ (B \ B' = ∅ ∨ B \ B' = {e})
hcard : (B' \ B).encard = (B \ B').encard
⊢ M.IsBase (insert f (B \ {e}))
Module: Mathlib.Combinatorics.Matroid.IndepAxioms

Goal state before:
pp: α : Type u_1
M : IndepMatroid α
B B' : Set α
hB : Maximal M.Indep B
hB' : Maximal M.Indep B'
e : α
he : e ∈ B \ B'
⊢ ∃ b ∈ B' \ B, Maximal M.Indep (insert b (B \ {e}))

Tactic:
have hnotmax : ¬ Maximal M.Indep (B \ {e}) :=
      fun h ↦ h.not_prop_of_ssuperset (sdiff_singleton_ssubset.2 he.1) hB.prop

Goal state after:
α : Type u_1
M : IndepMatroid α
B B' : Set α
hB : Maximal M.Indep B
hB' : Maximal M.Indep B'
e : α
he : e ∈ B \ B'
hnotmax : ¬Maximal M.Indep (B \ {e})
⊢ ∃ b ∈ B' \ B, Maximal M.Indep (insert b (B \ {e}))
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 B : Set α⦄, Indep I → ¬Maximal Indep I → Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I)
indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
X : Set α
x✝¹ : X ⊆ E
I : Set α
hI : Indep I
hIX : I ⊆ X
Is : Set (Set α)
hIs : Is ⊆ {Y | Indep Y ∧ Y ⊆ X}
hchain : IsChain (fun x1 x2 ↦ x1 ⊆ x2) Is
x✝ : Is.Nonempty
J : Set α
hJ : J ⊆ ⋃₀ Is
hJfin : J.Finite
f : α → Set α
hf : ∀ e ∈ J, f e ∈ Is ∧ e ∈ f e
hne : J.Nonempty
⊢ Indep J

Tactic:
obtain ⟨x, hxJ, hxmax⟩ := Finite.exists_maximalFor f _ hJfin hne

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 B : Set α⦄, Indep I → ¬Maximal Indep I → Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I)
indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
X : Set α
x✝¹ : X ⊆ E
I : Set α
hI : Indep I
hIX : I ⊆ X
Is : Set (Set α)
hIs : Is ⊆ {Y | Indep Y ∧ Y ⊆ X}
hchain : IsChain (fun x1 x2 ↦ x1 ⊆ x2) Is
x✝ : Is.Nonempty
J : Set α
hJ : J ⊆ ⋃₀ Is
hJfin : J.Finite
f : α → Set α
hf : ∀ e ∈ J, f e ∈ Is ∧ e ∈ f e
hne : J.Nonempty
x : α
hxJ : x ∈ J
hxmax : ∀ ⦃j : α⦄, (fun x ↦ x ∈ J) j → f x ⊆ f j → f j ⊆ f x
⊢ Indep J
Module: Mathlib.Combinatorics.Matroid.Basic

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

Tactic:
rw [IsBasis', IsBasis, and_iff_left inter_subset_right, maximal_iff_maximal_of_imp_of_forall]
  · exact fun I hI ↦ ⟨hI.1, hI.2.trans inter_subset_left⟩
  exact fun I hI ↦ ⟨I, rfl.le, hI.1, subset_inter hI.2 hI.1.subset_ground⟩

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
⊢ (∀ e_1 ∈ insert e I \ I, M.Dep (insert e_1 I)) ↔ M.Dep (insert e I) ∨ e ∈ I

Tactic:
dep_iff,

Goal state after:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
⊢ (∀ e_1 ∈ insert e I \ I, ¬M.Indep (insert e_1 I) ∧ insert e_1 I ⊆ M.E) ↔
    ¬M.Indep (insert e I) ∧ insert e I ⊆ M.E ∨ e ∈ I
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:
dep_iff,

Goal state after:
α : Type u_1
M : Matroid α
I : Set α
⊢ ¬M✶.Indep I ∧ I ⊆ M✶.E ↔ (∀ (B : Set α), M.IsBase B → (I ∩ B).Nonempty) ∧ I ⊆ M.E
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
hIJ : I.encard < J.encard
he : ∀ e ∈ J \ I, ¬M.Indep (insert e I)
⊢ ∀ e ∈ J, e ∉ I → M.Dep (insert e I)

Tactic:
dep_iff,

Goal state after:
α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
hIJ : I.encard < J.encard
he : ∀ e ∈ J \ I, ¬M.Indep (insert e I)
⊢ ∀ e ∈ J, e ∉ I → ¬M.Indep (insert e I) ∧ insert e I ⊆ M.E
Module: Mathlib.Combinatorics.Matroid.Rank.Finite

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
hX : M.IsRkFinite X
e : α
⊢ M.IsRkFinite (Insert.insert e X)

Tactic:
rw [← union_singleton]

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
hX : M.IsRkFinite X
e : α
⊢ M.IsRkFinite (X ∪ {e})
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.IsBasis I X
⊢ ∃ I₀ X₀, M.IsBasis I₀ X₀ ∧ f '' I = f '' I₀ ∧ f '' X = f '' X₀

Tactic:
exact ⟨I, X, h, rfl, rfl⟩

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

Goal state before:
pp: α : Type u_1
M : Matroid α
C R : Set α
hCR : C ⊆ R
hC : M.Dep C ∧ ∀ ⦃D : Set α⦄, M.Dep D → D ⊆ C → D = C
⊢ (¬M.Indep C ∧ C ⊆ R) ∧ ∀ ⦃D : Set α⦄, ¬M.Indep D ∧ D ⊆ R → D ⊆ C → D = C

Tactic:
dep_iff,

Goal state after:
α : Type u_1
M : Matroid α
C R : Set α
hCR : C ⊆ R
hC : (¬M.Indep C ∧ C ⊆ M.E) ∧ ∀ ⦃D : Set α⦄, ¬M.Indep D ∧ D ⊆ M.E → D ⊆ C → D = C
⊢ (¬M.Indep C ∧ C ⊆ R) ∧ ∀ ⦃D : Set α⦄, ¬M.Indep D ∧ D ⊆ R → D ⊆ C → D = C
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
tfae_1_iff_2 : M.IsLoop e ↔ e ∈ M.closure ∅
tfae_2_iff_3 : e ∈ M.closure ∅ ↔ M.IsCircuit {e}
tfae_2_iff_4 : e ∈ M.closure ∅ ↔ M.Dep {e}
h : (∀ (x : Set α), M.IsBase x → e ∈ M.E) ∧ ∀ (x : Set α), M.IsBase x → e ∉ x
hi : M.Indep {e}
B : Set α
hB : M.IsBase B
heB : {e} ⊆ B
⊢ e ∈ B

Tactic:
simpa using heB

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
C : Set α
he : M.IsLoop e
hC : M.IsCircuit C
h : e ∈ C
⊢ C = {e}

Tactic:
he.isCircuit.eq_of_subset_isCircuit hC (singleton_subset_iff.mpr h)

Goal state after:
α : Type u_1
M : Matroid α
e : α
C : Set α
he : M.IsLoop e
hC : M.IsCircuit C
h : e ∈ C
⊢ C = C
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
⊢ M.Indep {e} ↔ ¬M.Dep {e} ∧ e ∈ M.E

Tactic:
dep_iff,

Goal state after:
α : Type u_1
M : Matroid α
e : α
⊢ M.Indep {e} ↔ ¬(¬M.Indep {e} ∧ {e} ⊆ M.E) ∧ e ∈ M.E
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: case refine_1
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ≠ f
h : M.closure {e} = M.closure {f}
hf : M.IsNonloop f
⊢ M.Dep {e, f} ∧ ∀ e_1 ∈ {e, f}, M.Indep ({e, f} \ {e_1})

Tactic:
dep_iff,

Goal state after:
case refine_1
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ≠ f
h : M.closure {e} = M.closure {f}
hf : M.IsNonloop f
⊢ (¬M.Indep {e, f} ∧ {e, f} ⊆ M.E) ∧ ∀ e_1 ∈ {e, f}, M.Indep ({e, f} \ {e_1})