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

Goal state before:
pp: 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 k (i ∘ₗ i.ker.subtype)) x = (LinearMap.lTensor k i) ((LinearMap.lTensor (R ⧸ 𝔪) i.ker.subtype) 0)

Tactic:
rw [(LinearMap.exact_subtype_ker_map i).linearMap_comp_eq_zero]

Goal state after:
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 k 0) x = (LinearMap.lTensor k i) ((LinearMap.lTensor (R ⧸ 𝔪) i.ker.subtype) 0)
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)
motive : (⨂[R] (i : ι), s i) → Prop
z : ⨂[R] (i : ι), s i
add : ∀ (x y : ⨂[R] (i : ι), s i), motive x → motive y → motive (x + y)
smul_tprod : ∀ (r : R) (f : (i : ι) → s i), motive (tprodCoeff R r f)
⊢ motive z

Tactic:
exact PiTensorProduct.induction_on' z smul_tprod add

Goal state after:
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
r : R
x : GradedMonoid fun i ↦ ⨂[R]^i M
this : GradedMonoid.GMul.mul (algebraMap₀ r) x.snd = (cast R M ⋯) (GradedMonoid.GMul.mul x.snd (algebraMap₀ r))
⊢ (GradedMonoid.mk 0 ((↑algebraMap₀).toAddMonoidHom r) * x).snd =
    (cast R M ⋯) (x * GradedMonoid.mk 0 ((↑algebraMap₀).toAddMonoidHom r)).snd

Tactic:
exact this

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

Goal state before:
pp: case neg.refine_2
R : Type u_1
inst✝⁶ : CommSemiring 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'
M'' : Type u_4
inst✝¹ : AddCommMonoid M''
inst✝ : Module R M''
g : M' →ₗ[R] M''
hf : Function.Injective ⇑f
hfg : Function.Exact ⇑f ⇑g
p : Ideal R
toIsPrime✝ : p.IsPrime
x : M'
hx : p = (⊥.colon {x}).radical
h : ∀ a ∈ p.primeCompl, ∀ (y : M) (k : ℕ), f y ≠ a ^ k • x
b : R
x✝ : b ∈ (⊥.colon {g x}).radical
n : ℕ
hb : b ^ n ∈ ⊥.colon {g x}
⊢ b ∈ p

Tactic:
rw [mem_colon_singleton, mem_bot, ← map_smul, ← LinearMap.mem_ker,
        hfg.linearMap_ker_eq] at hb
      obtain ⟨y, hy⟩ := hb
      by_contra H
      exact h b H y n hy

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
inst✝ : IsNoetherianRing R
⊢ ⋃ p ∈ associatedPrimes R M, ↑p = {r | ∃ x, x ≠ 0 ∧ r • x = 0}

Tactic:
simp only [AssociatedPrimes.mem_iff, isAssociatedPrime_iff]
  refine subset_antisymm (Set.iUnion₂_subset ?_) ?_
  · rintro _ ⟨h, x, ⟨⟩⟩ r h'
    exact ⟨x, by simpa using h.ne_top, by simpa using h'⟩
  · intro r ⟨x, h, h'⟩
    obtain ⟨P, hP, hx⟩ := exists_le_isAssociatedPrime_of_isNoetherianRing R x h
    rw [isAssociatedPrime_iff] at hP
    exact Set.mem_iUnion₂_of_mem hP (hx (by rwa [mem_colon_singleton]))

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₂
⊢ p₁ ≤ p₂

Tactic:
by
  let g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom
  intro x hxp₁
  by_contra hxp₂
  obtain ⟨t, r, a, ht, e⟩ := hRT.exists_mul_eq_tmul x
    (p₂.asIdeal.comap g) inferInstance
  have h₁ : a ⊗ₜ[R] t ∈ p₁.asIdeal := e ▸ p₁.asIdeal.mul_mem_left (1 ⊗ₜ[R] (r • t)) hxp₁
  have h₂ : a ⊗ₜ[R] t ∉ p₂.asIdeal := e ▸ p₂.asIdeal.primeCompl.mul_mem ht hxp₂
  rw [← mul_one a, ← one_mul t, ← Algebra.TensorProduct.tmul_mul_tmul] at h₁ h₂
  have h₃ : t ∉ p₂.asIdeal.comap g := fun h ↦ h₂ (Ideal.mul_mem_left _ _ h)
  have h₄ : a ∉ p₂.asIdeal.comap (algebraMap S (S ⊗[R] T)) :=
    fun h ↦ h₂ (Ideal.mul_mem_right _ _ h)
  replace h₃ : t ∉ p₁.asIdeal.comap g := by
    rwa [show p₁.asIdeal.comap g = p₂.asIdeal.comap g from congr($h.2.1)]
  replace h₄ : a ∉ p₁.asIdeal.comap (algebraMap S (S ⊗[R] T)) := by
    rwa [show p₁.asIdeal.comap (algebraMap S (S ⊗[R] T)) = p₂.asIdeal.comap _ from congr($h.1.1)]
  exact p₁.asIdeal.primeCompl.mul_mem h₄ h₃ h₁

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

Goal state before:
pp: case mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' : Ideal R
hI : ↑I = ↑I'
⊢ (∃ x y, x ≠ 0 ∧ y ≠ 0 ∧ Ideal.span {x} * I' = Ideal.span {y} * ⊤) → ∃ x, x ≠ 0 ∧ I' = Ideal.span {x}

pp: case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' : Ideal R
hI : ↑I = ↑I'
⊢ (∃ x, x ≠ 0 ∧ I' = Ideal.span {x}) → ∃ x y, x ≠ 0 ∧ y ≠ 0 ∧ Ideal.span {x} * I' = Ideal.span {y} * ⊤

Tactic:
· rintro ⟨x, y, hx, hy, h⟩
    rw [Ideal.mul_top] at h
    rcases Ideal.mem_span_singleton_mul.mp ((Ideal.span_singleton_le_iff_mem _).mp h.ge) with
      ⟨i, _hi, rfl⟩
    rw [← Ideal.span_singleton_mul_span_singleton, Ideal.span_singleton_mul_right_inj hx] at h
    exact ⟨i, by grobner, h⟩

Goal state after:
case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' : Ideal R
hI : ↑I = ↑I'
⊢ (∃ x, x ≠ 0 ∧ I' = Ideal.span {x}) → ∃ x y, x ≠ 0 ∧ y ≠ 0 ∧ Ideal.span {x} * I' = Ideal.span {y} * ⊤
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
K' : Type u_3
inst✝² : Field K'
inst✝¹ : Algebra R K'
inst✝ : IsFractionRing R K'
I : (FractionalIdeal R⁰ K)ˣ
⊢ (QuotientGroup.mk' (toPrincipalIdeal R (FractionRing R)).range)
      (((Units.map ↑(canonicalEquiv R⁰ K' (FractionRing R))).comp (Units.map ↑(canonicalEquiv R⁰ K K'))) I) =
    (QuotientGroup.mk' (toPrincipalIdeal R (FractionRing R)).range)
      ((Units.map ↑(canonicalEquiv R⁰ K (FractionRing R))) I)

Tactic:
← Units.map_comp,

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
K' : Type u_3
inst✝² : Field K'
inst✝¹ : Algebra R K'
inst✝ : IsFractionRing R K'
I : (FractionalIdeal R⁰ K)ˣ
⊢ (QuotientGroup.mk' (toPrincipalIdeal R (FractionRing R)).range)
      ((Units.map ((↑(canonicalEquiv R⁰ K' (FractionRing R))).comp ↑(canonicalEquiv R⁰ K K'))) I) =
    (QuotientGroup.mk' (toPrincipalIdeal R (FractionRing R)).range)
      ((Units.map ↑(canonicalEquiv R⁰ K (FractionRing R))) I)
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
⊢ mk0 ⟨integralRep ↑I, ⋯⟩ = (mk (FractionRing R)) I

Tactic:
rw [← ClassGroup.mk_mk0 (FractionRing R), eq_comm, ClassGroup.mk_eq_mk]
  have fd_ne_zero : (algebraMap R (FractionRing R)) I.1.den ≠ 0 := by
    exact IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors (SetLike.coe_mem _)
  refine ⟨Units.mk0 (algebraMap R _ I.1.den) fd_ne_zero, ?_⟩
  apply Units.ext
  rw [mul_comm, val_mul, coe_toPrincipalIdeal, val_mk0]
  exact FractionalIdeal.den_mul_self_eq_num' R⁰ (FractionRing R) I

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

Goal state before:
pp: case h
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
S : Type u_3
L : Type u_4
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
inst✝² : Field L
inst✝¹ : Algebra S L
inst✝ : IsFractionRing S L
f : R ≃+* S
I : (FractionalIdeal S⁰ L)ˣ
x✝ : ∃ x, (∃ x_1, spanSingleton R⁰ ↑x_1 = ↑x) ∧ (Units.mapEquiv ↑(ringEquivOfRingEquiv K L f)) x = I
u : (FractionalIdeal R⁰ K)ˣ
v : Kˣ
huv : spanSingleton R⁰ ↑v = ↑u
hu : (Units.mapEquiv ↑(ringEquivOfRingEquiv K L f)) u = I
⊢ spanSingleton S⁰ ((IsFractionRing.ringEquivOfRingEquiv f) ↑v) = (ringEquivOfRingEquiv K L f) (spanSingleton R⁰ ↑v)

Tactic:
FractionalIdeal.ringEquivOfRingEquiv_spanSingleton

Goal state after:
case h
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
S : Type u_3
L : Type u_4
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
inst✝² : Field L
inst✝¹ : Algebra S L
inst✝ : IsFractionRing S L
f : R ≃+* S
I : (FractionalIdeal S⁰ L)ˣ
x✝ : ∃ x, (∃ x_1, spanSingleton R⁰ ↑x_1 = ↑x) ∧ (Units.mapEquiv ↑(ringEquivOfRingEquiv K L f)) x = I
u : (FractionalIdeal R⁰ K)ˣ
v : Kˣ
huv : spanSingleton R⁰ ↑v = ↑u
hu : (Units.mapEquiv ↑(ringEquivOfRingEquiv K L f)) u = I
⊢ spanSingleton S⁰ ((IsFractionRing.ringEquivOfRingEquiv f) ↑v) =
    spanSingleton S⁰ ((IsFractionRing.ringEquivOfRingEquiv f) ↑v)
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
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'
inst✝³ : Module S M'
inst✝² : Module S N'
inst✝¹ : IsScalarTower R S M'
inst✝ : IsScalarTower R S N'
f : M →ₗ[R] M'
g : N →ₗ[R] N'
hf : IsBaseChange S f
hg : IsBaseChange S g
⊢ ∀ (x : M × N), (prodRight R S S M N ≪≫ₗ hf.equiv.prodCongr hg.equiv) (1 ⊗ₜ[R] x) = (f.prodMap g) x

Tactic:
intro p

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommSemiring R
inst✝¹³ : CommSemiring S
inst✝¹² : Algebra R S
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'
inst✝³ : Module S M'
inst✝² : Module S N'
inst✝¹ : IsScalarTower R S M'
inst✝ : IsScalarTower R S N'
f : M →ₗ[R] M'
g : N →ₗ[R] N'
hf : IsBaseChange S f
hg : IsBaseChange S g
p : M × N
⊢ (prodRight R S S M N ≪≫ₗ hf.equiv.prodCongr hg.equiv) (1 ⊗ₜ[R] p) = (f.prodMap g) p
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
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ comap (algebraMap R A) ⁻¹' freeLocus R M ⊆ freeLocus A (A ⊗[R] M)

Tactic:
intro p

Goal state after:
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : PrimeSpectrum A
⊢ p ∈ comap (algebraMap R A) ⁻¹' freeLocus R M → p ∈ freeLocus A (A ⊗[R] M)
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
h : rankAtStalk M = 0
⊢ ∀ (x : PrimeSpectrum R), x ∉ support R M

Tactic:
intro p

Goal state after:
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
h : rankAtStalk M = 0
p : PrimeSpectrum R
⊢ p ∉ support R M
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
M : Type v
N : Type u_1
P : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module.Invertible R M
f : N →ₗ[R] P
⊢ Function.Injective ⇑(LinearMap.lTensor M f) ∧ Function.Surjective ⇑(LinearMap.lTensor M f) ↔
    Function.Injective ⇑f ∧ Function.Surjective ⇑f

Tactic:
lTensor_injective_iff,

Goal state after:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module.Invertible R M
f : N →ₗ[R] P
⊢ Function.Injective ⇑f ∧ Function.Surjective ⇑(LinearMap.lTensor M f) ↔ Function.Injective ⇑f ∧ Function.Surjective ⇑f
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module.Invertible R M
inst✝ : Free R M
⊢ finrank R M = 1

Tactic:
(free_iff_linearEquiv.mp ‹_›).some.finrank_eq,

Goal state after:
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module.Invertible R M
inst✝ : Free R M
⊢ finrank R R = 1
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
sf : Type (max 0 u) := (n : ℕ) × ModuleCon R (Fin n → R)
c₁ : sf
⊢ ModuleCon.Quotient (Fin c₁.fst → R) c₁.snd ≃ₗ[R] ModuleCon.Quotient (Fin c₁.fst → R) c₁.snd

Tactic:
exact .refl ..

Goal state after:
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
M✝¹ : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
A : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M✝¹
inst✝⁸ : AddCommMonoid N
inst✝⁷ : AddCommMonoid P
inst✝⁶ : AddCommMonoid Q
inst✝⁵ : Module R M✝¹
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Module R Q
inst✝¹ : Module.Invertible R M✝¹
inst✝ : Module.Invertible R N
M✝ : (Skeleton (SemimoduleCat R))ˣ
M : Skeleton (SemimoduleCat R)
⊢ ↑(Quotient.out M) ≃ₗ[R] ↑(Quotient.out M)

Tactic:
exact .refl ..

Goal state after:
Module: Mathlib.FieldTheory.Normal.Closure

Goal state before:
pp: F : Type u_1
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Normal F L
K₁ K₂ : IntermediateField F L
inst✝ : Normal F ↥K₂
⊢ normalClosure F (↥K₁) L ≤ K₂ ↔ K₁ ≤ K₂

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Goal state after:
case refine_1
F : Type u_1
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Normal F L
K₁ K₂ : IntermediateField F L
inst✝ : Normal F ↥K₂
h : normalClosure F (↥K₁) L ≤ K₂
⊢ K₁ ≤ K₂

case refine_2
F : Type u_1
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Normal F L
K₁ K₂ : IntermediateField F L
inst✝ : Normal F ↥K₂
h : K₁ ≤ K₂
⊢ normalClosure F (↥K₁) L ≤ K₂
Module: Mathlib.RingTheory.AlgebraicIndependent.Defs

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
A : Type u_5
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
f : ι' → ι
hf : Injective f
⊢ AlgebraicIndependent R (x ∘ f)

Tactic:
intro p

Goal state after:
ι : Type u_1
ι' : Type u_2
R : Type u_3
A : Type u_5
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
f : ι' → ι
hf : Injective f
p : MvPolynomial ι' R
⊢ ∀ ⦃a₂ : MvPolynomial ι' R⦄, (aeval (x ∘ f)) p = (aeval (x ∘ f)) a₂ → p = a₂
Module: Mathlib.FieldTheory.Normal.Basic

Goal state before:
pp: F : Type u_1
inst✝⁷ : Field F
K₁ : Type u_3
inst✝⁶ : Field K₁
inst✝⁵ : Algebra F K₁
E : Type u_6
inst✝⁴ : Field E
inst✝³ : Algebra F E
inst✝² : Algebra K₁ E
inst✝¹ : IsScalarTower F K₁ E
inst✝ : Normal F K₁
h1 : Group.IsSolvable Gal(K₁/F)
h2 : Group.IsSolvable Gal(E/K₁)
f : Gal(E/K₁) →* Gal(E/F) :=
  { toFun := fun ϕ ↦ AlgEquiv.ofAlgHom (AlgHom.restrictScalars F ↑ϕ) (AlgHom.restrictScalars F ↑ϕ.symm) ⋯ ⋯,
    map_one' := ⋯, map_mul' := ⋯ }
ϕ : Gal(E/F)
hϕ : ϕ ∈ (AlgEquiv.restrictNormalHom K₁).ker
x : K₁
⊢ ϕ.toFun ((algebraMap K₁ E) x) = (algebraMap K₁ E) x

Tactic:
exact Eq.trans (ϕ.restrictNormal_commutes K₁ x).symm (congr_arg _ (AlgEquiv.ext_iff.mp hϕ x))

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

Goal state before:
pp: α : Type u_1
M : Matroid α
B₁ B₂ : Set α
hB₁ : M.IsBase B₁
hB₂ : M.IsBase B₂
⊢ (B₂ \ B₁).encard.toNat = (B₂ \ B₁).ncard

Tactic:
← ncard_def

Goal state after:
α : Type u_1
M : Matroid α
B₁ B₂ : Set α
hB₁ : M.IsBase B₁
hB₂ : M.IsBase B₂
⊢ (B₂ \ B₁).ncard = (B₂ \ B₁).ncard
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
B₁ B₂ : Set α
hB₁ : M.IsBase B₁
hB₂ : M.IsBase B₂
⊢ B₂.encard.toNat = B₂.ncard

Tactic:
← ncard_def

Goal state after:
α : Type u_1
M : Matroid α
B₁ B₂ : Set α
hB₁ : M.IsBase B₁
hB₂ : M.IsBase B₂
⊢ B₂.ncard = B₂.ncard
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

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

Tactic:
restrict_ground_eq,

Goal state after:
α : Type u_1
M : Matroid α
R I X : Set α
⊢ (M.IsBasis' I (X ∩ R) ∧ I ⊆ R) ∧ X ⊆ R ↔ M.IsBasis I (X ∩ M.E) ∧ X ⊆ R
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
I E R : Set α
⊢ (uniqueBaseOn I E ↾ R).E = (uniqueBaseOn (I ∩ R ∩ E) R).E ∧
    ∀ ⦃I_1 : Set α⦄,
      I_1 ⊆ (uniqueBaseOn I E ↾ R).E → ((uniqueBaseOn I E ↾ R).Indep I_1 ↔ (uniqueBaseOn (I ∩ R ∩ E) R).Indep I_1)

Tactic:
restrict_ground_eq,

Goal state after:
α : Type u_1
I E R : Set α
⊢ R = (uniqueBaseOn (I ∩ R ∩ E) R).E ∧
    ∀ ⦃I_1 : Set α⦄, I_1 ⊆ R → ((uniqueBaseOn I E ↾ R).Indep I_1 ↔ (uniqueBaseOn (I ∩ R ∩ E) R).Indep I_1)
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:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
I X : Set α
h : (N.comap f).IsBasis I X
⊢ N.IsBasis (f '' I) (f '' X) ∧ InjOn f I ∧ I ⊆ X

case refine_2
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
I X : Set α
h : N.IsBasis (f '' I) (f '' X) ∧ InjOn f I ∧ I ⊆ X
⊢ (N.comap f).IsBasis I X
Module: Mathlib.Combinatorics.Matroid.IndepAxioms

Goal state before:
pp: α : Type u_1
E : Set α
M : Matroid α
hM : ∃ M_1, E = M_1.E ∧ ∀ (I : Set α), M_1.Indep I ↔ M.Indep I
⊢ ∀ ⦃I J : Set α⦄, M.Indep J → I ⊆ J → M.Indep I

Tactic:
exact fun I J hJ hIJ ↦ hJ.subset hIJ

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

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

Tactic:
by
  rw [comapOn, isBase_restrict_iff', comap_isBasis'_iff]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ M.IsRkFinite M.E ↔ M.RankFinite

Tactic:
IsRkFinite,

Goal state after:
α : Type u_1
M : Matroid α
⊢ (M ↾ M.E).RankFinite ↔ M.RankFinite
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: case refine_2
α : Type u_1
M : Matroid α
C I : Set α
e : α
hC : M.IsCircuit C
hI : M.Indep I
hCs : C ⊆ insert e I
heC : e ∈ C
hCeI : C \ {e} ⊆ I
hss : M.fundCircuit e I ⊆ C
heI : e ∈ I
⊢ False

Tactic:
exact hC.not_indep (hI.subset (hCs.trans (by simp [heI])))

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
I : Set α
hI : M.Indep I
h : e ∈ I
⊢ ¬M.IsLoop e

Tactic:
exact fun he ↦ (he.notMem_of_indep hI) h

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ≠ f
⊢ M.closure {e} = M.closure {f} ↔ M.IsCircuit {e, f}

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩

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}
⊢ M.IsCircuit {e, f}

case refine_2
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ≠ f
h : M.IsCircuit {e, f}
⊢ M.closure {e} = M.closure {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 ∩ Y)) ≤
    M.eRk (M.E \ insert e X) + M.eRk (M.E \ insert e Y)

Tactic:
insert_inter_distrib

Goal state after:
α : 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)
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
⊢ M.closure (X ∩ {e | M.IsNonloop e}) = M.closure X

Tactic:
setOfPred_isNonloop_eq,

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
⊢ M.closure (X ∩ (M.E \ M.loops)) = M.closure X
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
⊢ [M.IsColoop e, e ∈ M.coloops, M.IsCocircuit {e}, ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B,
      (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E, ∀ (X : Set α), e ∈ M.closure X ↔ e ∈ X,
      ¬M.Spanning (M.E \ {e})].TFAE

Tactic:
by
  tfae_have 1 ↔ 2 := Iff.rfl
  tfae_have 1 ↔ 3 := singleton_isCocircuit.symm
  tfae_have 1 ↔ 4 := by
    simp_rw [← dual_isLoop_iff_isColoop, isLoop_iff_forall_mem_compl_isBase]
    refine ⟨fun h B hB ↦ ?_, fun h B hB ↦ h hB.compl_isBase_of_dual⟩
    obtain ⟨-, heB : e ∈ B⟩ := by simpa using h (M.E \ B) hB.compl_isBase_dual
    assumption
  tfae_have 3 → 5 := fun h ↦
    ⟨fun C hC heC ↦ hC.inter_isCocircuit_ne_singleton h (e := e) (by simpa), h.subset_ground rfl⟩
  tfae_have 5 → 4 := by
    refine fun ⟨h, heE⟩ B hB ↦ by_contra fun heB ↦ ?_
    rw [← hB.closure_eq] at heE
    obtain ⟨C, -, hC, heC⟩ := (mem_closure_iff_exists_isCircuit heB).1 heE
    exact h hC heC
  tfae_have 5 ↔ 6 := by
    refine ⟨fun h X ↦ ⟨fun heX ↦ by_contra fun heX' ↦ ?_, fun heX ↦ M.mem_closure_of_mem' heX h.2⟩,
      fun h ↦ ⟨fun C hC heC ↦ ?_, M.closure_subset_ground _ <| (h {e}).2 rfl⟩⟩
    · obtain ⟨C, -, hC, heC⟩ := (mem_closure_iff_exists_isCircuit heX').1 heX
      exact h.1 hC heC
    · simpa [hC.mem_closure_sdiff_singleton_of_mem heC] using h (C \ {e})
  tfae_have 1 ↔ 7 := by
    wlog he : e ∈ M.E
    · exact iff_of_false (fun h ↦ he h.mem_ground) <| by simp [he, M.ground_spanning]
    rw [spanning_iff_compl_coindep sdiff_subset, ← dual_isLoop_iff_isColoop, ← singleton_dep,
      sdiff_sdiff_cancel_left (by simpa), ← not_indep_iff (by simpa)]
  tfae_finish

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
hX : M.Spanning X
⊢ (M ↾ X).eRk (M ↾ X).E = M.eRank

Tactic:
restrict_ground_eq,

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
hX : M.Spanning X
⊢ (M ↾ X).eRk X = M.eRank