mathlib-initiative/mathlib-tactics huggingface dataset:
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''
f : P.Hom P'
g : P'.Hom P''
x : P.CotangentSpace
⊢ (CotangentSpace.map (g.comp f)) x = (↑S (CotangentSpace.map g) ∘ₗ CotangentSpace.map f) x

Tactic:
induction x using TensorProduct.induction_on with
  | zero =>
    simp only [map_zero]
  | add =>
    simp only [map_add, LinearMap.coe_comp, LinearMap.coe_restrictScalars, Function.comp_apply, *]
  | tmul x y =>
    obtain ⟨y, rfl⟩ := KaehlerDifferential.tensorProductTo_surjective _ _ y
    induction y with
    | zero => simp only [map_zero, tmul_zero]
    | add => simp only [map_add, tmul_add, LinearMap.coe_comp, LinearMap.coe_restrictScalars,
      Function.comp_apply, *]
    | tmul => simp only [Derivation.tensorProductTo_tmul, tmul_smul, smul_tmul', map_tmul,
        Hom.toAlgHom_apply, Hom.comp_toRingHom, RingHom.coe_comp, Function.comp_apply,
        LinearMap.coe_comp, LinearMap.coe_restrictScalars,
        ← IsScalarTower.algebraMap_apply S S' S'']

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
ι : Type w
ι' : Type u_1
P : Generators R S ι
S' : Type u_2
inst✝⁹ : CommRing S'
inst✝⁸ : Algebra R S'
T : Type w
inst✝⁷ : CommRing T
inst✝⁶ : Algebra R T
inst✝⁵ : Algebra S T
inst✝⁴ : IsScalarTower R S T
inst✝³ : Algebra S' T
inst✝² : IsScalarTower R S' T
inst✝¹ : FinitePresentation R S
inst✝ : Projective S Ω[S⁄R]
⊢ Module.Finite S (H1Cotangent R S)

Tactic:
let P := Algebra.Presentation.ofFinitePresentation R S
  have : Algebra.FiniteType R P.toExtension.Ring := by simp [P]; infer_instance
  suffices Module.Finite S P.toExtension.H1Cotangent from
    .of_surjective P.equivH1Cotangent.toLinearMap P.equivH1Cotangent.surjective
  rw [Module.finite_def, Submodule.fg_top, ← LinearMap.ker_rangeRestrict]
  have := Extension.Cotangent.finite P.fg_ker
  have : Module.FinitePresentation S (LinearMap.range P.toExtension.cotangentComplex) := by
    rw [← LinearMap.exact_iff.mp P.toExtension.exact_cotangentComplex_toKaehler]
    exact Module.finitePresentation_of_projective_of_exact
      _ _ (Subtype.val_injective) P.toExtension.toKaehler_surjective
      (LinearMap.exact_subtype_ker_map _)
  exact Module.FinitePresentation.fg_ker (N := LinearMap.range P.toExtension.cotangentComplex)
    _ P.toExtension.cotangentComplex.surjective_rangeRestrict

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
inst✝ : Module.Finite R M
I : Ideal R
p : PrimeSpectrum R
hp₁ : Nontrivial (LocalizedModule p.asIdeal.primeCompl M)
hp₂ : p ∈ zeroLocus ↑I
Rₚ : Type u_1 := Localization.AtPrime p.asIdeal
Mₚ : Type (max u_1 u_2) := LocalizedModule p.asIdeal.primeCompl M
Mₚ' : Type (max u_1 u_2) := LocalizedModule p.asIdeal.primeCompl (M ⧸ I • ⊤)
Mₚ'' : Type (max u_1 u_2) := Mₚ ⧸ Ideal.map (algebraMap R Rₚ) I • ⊤
⊢ Ideal.map (algebraMap R (Localization p.asIdeal.primeCompl)) I •
      Submodule.localized' (Localization p.asIdeal.primeCompl) p.asIdeal.primeCompl
        (LocalizedModule.mkLinearMap p.asIdeal.primeCompl M) ⊤ =
    Ideal.map (algebraMap R Rₚ) I • ⊤

Tactic:
Submodule.localized'_top

Goal state after:
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
p : PrimeSpectrum R
hp₁ : Nontrivial (LocalizedModule p.asIdeal.primeCompl M)
hp₂ : p ∈ zeroLocus ↑I
Rₚ : Type u_1 := Localization.AtPrime p.asIdeal
Mₚ : Type (max u_1 u_2) := LocalizedModule p.asIdeal.primeCompl M
Mₚ' : Type (max u_1 u_2) := LocalizedModule p.asIdeal.primeCompl (M ⧸ I • ⊤)
Mₚ'' : Type (max u_1 u_2) := Mₚ ⧸ Ideal.map (algebraMap R Rₚ) I • ⊤
⊢ Ideal.map (algebraMap R (Localization p.asIdeal.primeCompl)) I • ⊤ = Ideal.map (algebraMap R Rₚ) I • ⊤
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:
classical
  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.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
n : ℕ
f : M [⋀^Fin (n + 1)]→ₗ[R] N
p : Fin (n + 1)
x : M
v : Fin n → M
⊢ (-1) ^ ↑p • f (p.insertNth x v) = f (Matrix.vecCons x v)

Tactic:
by
  rw [map_insertNth, smul_smul, ← pow_add, Even.neg_one_pow, one_smul]
  use p

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 • 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_add_cancel

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
⊢ 0 = 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.ExteriorPower.Pairing

Goal state before:
pp: case neg
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₁ : ∀ (i : ι), (f i) (x i) = 1
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → (f i) (x j) = 0
n : ℕ
a : Fin n ↪o ι
i j : Fin n
hij : ¬i = j
⊢ (f (a j)) (x (a i)) = 1 i j

Tactic:
h₀ (by simpa using Ne.symm hij),

Goal state after:
case neg
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₁ : ∀ (i : ι), (f i) (x i) = 1
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → (f i) (x j) = 0
n : ℕ
a : Fin n ↪o ι
i j : Fin n
hij : ¬i = j
⊢ 0 = 1 i j
Module: Mathlib.LinearAlgebra.TensorPower.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ιι : Type u_3
ι : ιι → Type u_4
ai : ιι
a : ⨂[R] (x : ι ai), M
bi : ιι
b : ⨂[R] (x : ι bi), M
hi : ai = bi
h : (reindex R (fun x ↦ M) (Equiv.cast ⋯)) a = b
⊢ ⟨ai, a⟩ = ⟨bi, b⟩

Tactic:
subst hi

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ιι : Type u_3
ι : ιι → Type u_4
ai : ιι
a b : ⨂[R] (x : ι ai), M
h : (reindex R (fun x ↦ M) (Equiv.cast ⋯)) a = b
⊢ ⟨ai, a⟩ = ⟨ai, b⟩
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)
t : ι → Type u_11
t' : ι → Type u_12
inst✝³ : (i : ι) → AddCommMonoid (t i)
inst✝² : (i : ι) → Module R (t i)
inst✝¹ : (i : ι) → AddCommMonoid (t' i)
inst✝ : (i : ι) → Module R (t' i)
f : (i : ι) → s i →ₗ[R] t i →ₗ[R] t' i
a : (i : ι) → s i
b : (i : ι) → t i
⊢ ((piTensorHomMap₂ ((tprod R) f)) ((tprod R) a)) ((tprod R) b) = ⨂ₜ[R] (i : ι), ((f i) (a i)) (b i)

Tactic:
simp [piTensorHomMapFun₂, piTensorHomMap₂]

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
I : Ideal R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
h : IsAssociatedPrime I M
hf : Function.Injective ⇑f
⊢ IsAssociatedPrime I M'

Tactic:
by
  obtain ⟨x, rfl⟩ := h.2
  refine ⟨h.1, ⟨f x, ?_⟩⟩
  ext r
  simp_rw [Ideal.mem_radical_iff, mem_colon_singleton, mem_bot, ← map_smul, map_eq_zero_iff f hf]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
H : IsNoetherianRing R
x : M
hx : x ≠ 0
y : M
h₃ : ∀ I ∈ {P | ⊥.colon {x} ≤ P ∧ P ≠ ⊤ ∧ ∃ y, P = ⊥.colon {y}}, ¬⊥.colon {y} < I
l : ⊥.colon {x} ≤ ⊥.colon {y}
h₁ : ⊥.colon {y} ≠ ⊤
a : R
⊢ ∀ {y_1 : R}, a * y_1 ∈ ⊥.colon {y} → a ∈ ⊥.colon {y} ∨ y_1 ∈ ⊥.colon {y}

Tactic:
b

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
H : IsNoetherianRing R
x : M
hx : x ≠ 0
y : M
h₃ : ∀ I ∈ {P | ⊥.colon {x} ≤ P ∧ P ≠ ⊤ ∧ ∃ y, P = ⊥.colon {y}}, ¬⊥.colon {y} < I
l : ⊥.colon {x} ≤ ⊥.colon {y}
h₁ : ⊥.colon {y} ≠ ⊤
a b : R
⊢ a * b ∈ ⊥.colon {y} → a ∈ ⊥.colon {y} ∨ b ∈ ⊥.colon {y}
Module: Mathlib.RingTheory.LocalRing.Module

Goal state before:
pp: 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)
this✝ : Projective R ↥l.range
l' : M →ₗ[R] ↥l.ker
this : Module.Finite R ↥l.ker
hl' : LinearMap.lTensor k (l' ∘ₗ l.ker.subtype) = LinearMap.lTensor k LinearMap.id
⊢ Function.Injective ⇑(LinearMap.lTensor k l.ker.subtype)

Tactic:
rw [LinearMap.lTensor_comp, LinearMap.lTensor_id] at hl'

Goal state after:
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)
this✝ : Projective R ↥l.range
l' : M →ₗ[R] ↥l.ker
this : Module.Finite R ↥l.ker
hl' : LinearMap.lTensor k l' ∘ₗ LinearMap.lTensor k l.ker.subtype = LinearMap.id
⊢ Function.Injective ⇑(LinearMap.lTensor k l.ker.subtype)
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : C(X, Y)
hfs : Function.Surjective f.toFun
a : LocallyConstant Y Z
⊢ ∀ ⦃a₂ : LocallyConstant Y Z⦄, comap f a = comap f a₂ → a = a₂

Tactic:
b

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : C(X, Y)
hfs : Function.Surjective f.toFun
a b : LocallyConstant Y Z
⊢ comap f a = comap f b → a = b
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
inst✝² : IsLocalRing R
inst✝¹ : IsLocalRing S
inst✝ : IsLocalHom (algebraMap R S)
eSp : ResidueField R ⊗[R] S ≃ₐ[R] S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R) :=
  (Algebra.TensorProduct.comm R (ResidueField R) S).trans
    (AlgEquiv.restrictScalars R (quotIdealMapEquivTensorQuot S (maximalIdeal R)).symm)
⊢ Nontrivial (ResidueField R ⊗[R] S)

Tactic:
by
    rw [eSp.nontrivial_congr, Ideal.Quotient.nontrivial_iff]
    exact ((((local_hom_TFAE (algebraMap R S)).out 0 2 rfl rfl).mp inferInstance).trans_lt
      (inferInstance : (maximalIdeal S).IsMaximal).lt_top).ne

Goal state after:
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
⊢ 1 ⊗ₜ[R] (algebraMap R p.ResidueField) (r * y) * x = a ⊗ₜ[R] (algebraMap R p.ResidueField) y

Tactic:
simpa [← tmul_smul, Submonoid.smul_def, ← smul_mul_assoc, smul_comm _ r,
    ← IsLocalRing.ResidueField.algebraMap_eq, ← algebraMap.coe_smul,
    ← IsScalarTower.algebraMap_apply] using congr(t • $e)

Goal state after:
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: case h
G : Type u_1
inst✝¹ : Group G
inst✝ : WellFoundedLT (Subgroup G)
h : ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H
H : Subgroup G
hH : ∀ y < H, IsSolvable ↥y
h' : H ≠ ⊥
n : ℕ
hn : map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) n) = map ⁅H, H⁆.subtype ⊥
⊢ map H.subtype (derivedSeries (↥H) (n + 1)) = map H.subtype ⊥

Tactic:
Subgroup.map_bot

Goal state after:
case h
G : Type u_1
inst✝¹ : Group G
inst✝ : WellFoundedLT (Subgroup G)
h : ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H
H : Subgroup G
hH : ∀ y < H, IsSolvable ↥y
h' : H ≠ ⊥
n : ℕ
hn : map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) n) = ⊥
⊢ map H.subtype (derivedSeries (↥H) (n + 1)) = ⊥
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: case zero
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSimpleGroup G
x✝ : Group.IsSolvable G
hn : derivedSeries G 0 = ⊥
a : G
⊢ ∀ (b : G), a * b = b * a

Tactic:
b

Goal state after:
case zero
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSimpleGroup G
x✝ : Group.IsSolvable G
hn : derivedSeries G 0 = ⊥
a b : G
⊢ a * b = b * a
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: case succ
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSimpleGroup G
x✝ : Group.IsSolvable G
n✝ : ℕ
hn : _root_.commutator G = ⊥
a : G
⊢ ∀ (b : G), a * b = b * a

Tactic:
b

Goal state after:
case succ
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSimpleGroup G
x✝ : Group.IsSolvable G
n✝ : ℕ
hn : _root_.commutator G = ⊥
a b : G
⊢ a * b = b * a
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
A✝ : Type u_4
inst✝¹³ : CommSemiring R
inst✝¹² : AddCommMonoid M
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : AddCommMonoid P
inst✝⁹ : AddCommMonoid Q
inst✝⁸ : Module R M
inst✝⁷ : Module R N
inst✝⁶ : Module R P
inst✝⁵ : Module R Q
inst✝⁴ : Module.Invertible R M
inst✝³ : Module.Invertible R N
A : Type u_5
B : Type u_6
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : Algebra R A
x✝¹ x✝ : Pic R
⊢ Pic.mk A (A ⊗[R] (x✝¹ * x✝).AsModule) = Pic.mk A (A ⊗[R] x✝¹.AsModule) * Pic.mk A (A ⊗[R] x✝.AsModule)

Tactic:
← mk_tensor,

Goal state after:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
A✝ : Type u_4
inst✝¹³ : CommSemiring R
inst✝¹² : AddCommMonoid M
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : AddCommMonoid P
inst✝⁹ : AddCommMonoid Q
inst✝⁸ : Module R M
inst✝⁷ : Module R N
inst✝⁶ : Module R P
inst✝⁵ : Module R Q
inst✝⁴ : Module.Invertible R M
inst✝³ : Module.Invertible R N
A : Type u_5
B : Type u_6
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : Algebra R A
x✝¹ x✝ : Pic R
⊢ Pic.mk A (A ⊗[R] (x✝¹ * x✝).AsModule) = Pic.mk A (A ⊗[R] x✝¹.AsModule ⊗[A] (A ⊗[R] x✝.AsModule))
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
inst✝ : FaithfulSMul R A
I✝ J✝ I J : (Submodule R A)ˣ
⊢ Pic.mk R ↥↑(I * J) = Pic.mk R ↥↑I * Pic.mk R ↥↑J

Tactic:
← mk_tensor,

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
inst✝ : FaithfulSMul R A
I✝ J✝ I J : (Submodule R A)ˣ
⊢ Pic.mk R ↥↑(I * J) = Pic.mk R (↥↑I ⊗[R] ↥↑J)
Module: Mathlib.Combinatorics.Matroid.IndepAxioms

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
E : Set α
Indep : Finset α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Finset α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I J : Finset α⦄, Indep I → Indep J → I.card < J.card → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
subset_ground : ∀ ⦃I : Finset α⦄, Indep I → ↑I ⊆ E
I : Finset α
⊢ (IndepMatroid.ofFinitaryCardAugment E (fun I ↦ ∀ (J : Finset α), ↑J ⊆ I → Indep J) ⋯ ⋯ ⋯ ⋯ ⋯).Indep ↑I ↔ Indep I

Tactic:
exact ⟨fun h ↦ h _ Subset.rfl, fun h J hJI ↦ indep_subset h hJI⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
E B : Set α
h : BijOn f E N.E
⊢ B ⊆ E → ((N.comapOn E f).IsBase B ↔ N.IsBase (f '' B))

Tactic:
suffices h' : B ⊆ E → InjOn f B from fun hB ↦
    by simp [hB, comapOn_isBase_iff_of_surjOn h.surjOn, h']

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
E B : Set α
h : BijOn f E N.E
⊢ B ⊆ E → InjOn f B
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 α
E : Set β
e : ↑M.E ≃ ↑E
⊢ E = (M.mapSetEmbedding (e.toEmbedding.trans (Embedding.subtype fun x ↦ x ∈ E))).E ∧
    ∀ (I : Set β),
      (M.mapSetEmbedding (e.toEmbedding.trans (Embedding.subtype fun x ↦ x ∈ E))).Indep I ↔
        M.Indep (Subtype.val '' ⇑e.symm '' E ↓∩ I) ∧ I ⊆ E

Tactic:
by
    have hrw : ∀ I : Set β, Subtype.val ∘ ⇑e ⁻¹' I = ⇑e.symm '' E ↓∩ I := fun I ↦ by ext; simp
    simp [Equiv.toEmbedding, Embedding.subtype, Embedding.trans, hrw]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
X : Set α
⊢ M.eRk (insert e (M.closure X)) = M.eRk (insert e X)

Tactic:
rw [← union_singleton, eRk_union_closure_left_eq, union_singleton]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
inst✝ : M.RankFinite
⊢ M.Indep I ↔ M.eRk I = I.encard

Tactic:
refine ⟨Indep.eRk_eq_encard, fun h ↦ ?_⟩
  obtain hfin | hinf := I.finite_or_infinite
  · rwa [indep_iff_eRk_eq_encard_of_finite hfin]
  rw [hinf.encard_eq] at h
  exact False.elim <| (M.isRkFinite_set I).eRk_lt_top.ne h

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
B : Set α
hB : M.IsBase B
he : e ∈ B
h : ∀ x ∈ M.E \ B, e ∉ M.fundCircuit x B
h' : M.E \ {e} ⊆ M.closure (B \ {e})
⊢ e ∉ M.closure (M.E \ {e})

Tactic:
exact notMem_subset (M.closure_subset_closure_of_subset_closure h') <|
    hB.indep.notMem_closure_sdiff_of_mem he

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

Goal state before:
pp: α : Type u
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
I : Set α
⊢ M.IsBasis' I X → #↑I ≤ M.cRk Y

Tactic:
hIX

Goal state after:
α : Type u
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
I : Set α
hIX : M.IsBasis' I X
⊢ #↑I ≤ M.cRk Y
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: α : Type u
β : Type v
f : α → β
M✝ : Matroid α
I✝ J✝ B B' X✝ Y : Set α
M : Matroid α
inst✝ : M.InvariantCardinalRank
hf : InjOn f M.E
I X : Set α
hIX : M.IsBasis I X
hI : (M.map f hf).IsBasis (f '' I) (f '' X)
J : Set α
hJ : (M.map f hf).IsBasis (f '' J) (f '' X)
hJX : M.IsBasis J X
h' : f '' X = f '' X
⊢ #↑(f '' I \ f '' J) = #↑(f '' J \ f '' I)

Tactic:
have hcard := hIX.cardinalMk_sdiff_comm hJX

Goal state after:
α : Type u
β : Type v
f : α → β
M✝ : Matroid α
I✝ J✝ B B' X✝ Y : Set α
M : Matroid α
inst✝ : M.InvariantCardinalRank
hf : InjOn f M.E
I X : Set α
hIX : M.IsBasis I X
hI : (M.map f hf).IsBasis (f '' I) (f '' X)
J : Set α
hJ : (M.map f hf).IsBasis (f '' J) (f '' X)
hJX : M.IsBasis J X
h' : f '' X = f '' X
hcard : #↑(I \ J) = #↑(J \ I)
⊢ #↑(f '' I \ f '' J) = #↑(f '' J \ f '' I)
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
heI : e ∈ I
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
⊢ M.fundCocircuit e B ∩ I ⊆ {e}

Tactic:
← M.fundCocircuit_inter_eq (hIB heI)

Goal state after:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
heI : e ∈ I
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
⊢ M.fundCocircuit e B ∩ I ⊆ M.fundCocircuit e B ∩ B
Module: Mathlib.RingTheory.AlgebraicIndependent.Basic

Goal state before:
pp: ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
f : ι → MvPolynomial ι R
hf : AlgebraicIndependent R f
⊢ AlgebraicIndependent R fun i ↦ (aeval x) (f i)

Tactic:
algebraicIndependent_iff

Goal state after:
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : ∀ (p : MvPolynomial ι R), (aeval x) p = 0 → p = 0
f : ι → MvPolynomial ι R
hf : ∀ (p : MvPolynomial ι R), (aeval f) p = 0 → p = 0
⊢ ∀ (p : MvPolynomial ι R), (aeval fun i ↦ (aeval x) (f i)) p = 0 → p = 0
Module: Mathlib.RingTheory.AlgebraicIndependent.Basic

Goal state before:
pp: ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : ι → MvPolynomial ι R
H : AlgebraicIndependent R fun i ↦ (aeval x) (f i)
⊢ AlgebraicIndependent R f

Tactic:
algebraicIndependent_iff

Goal state after:
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : ι → MvPolynomial ι R
H : ∀ (p : MvPolynomial ι R), (aeval fun i ↦ (aeval x) (f i)) p = 0 → p = 0
⊢ ∀ (p : MvPolynomial ι R), (aeval f) p = 0 → p = 0