mathlib-initiative/mathlib-tactics huggingface dataset:
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 ι
R' : Type u_1
S' : Type u_2
ι' : Type u_3
inst✝¹⁴ : CommRing R'
inst✝¹³ : CommRing S'
inst✝¹² : Algebra R' S'
P' : Generators R' S' ι'
R'' : Type u_4
S'' : Type u_5
ι'' : Type u_6
inst✝¹¹ : CommRing R''
inst✝¹⁰ : CommRing S''
inst✝⁹ : Algebra R'' S''
P'' : Generators R'' S'' ι''
inst✝⁸ : Algebra R R'
inst✝⁷ : Algebra R' R''
inst✝⁶ : Algebra R' S''
inst✝⁵ : Algebra S S'
inst✝⁴ : Algebra S' S''
inst✝³ : Algebra S S''
inst✝² : IsScalarTower R' R'' S''
inst✝¹ : IsScalarTower R' S' S''
inst✝ : IsScalarTower S S' S''
f : P'.Hom P''
g : P.Hom P'
x : ι
⊢ (aeval P''.val) ((aeval f.val) (g.val x)) = (algebraMap S S'') (P.val x)

Tactic:
rw [IsScalarTower.algebraMap_apply S S' S'', ← g.aeval_val]
    induction g.val x using MvPolynomial.induction_on with
    | C r => simp [← IsScalarTower.algebraMap_apply]
    | add x y hx hy => simp only [map_add, hx, hy]
    | mul_X p i hp => simp only [map_mul, hp, aeval_X, aeval_val]

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

Goal state before:
pp: R : Type u
S : Type v
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Extension R S
R' : Type u'
S' : Type v'
inst✝⁶ : CommRing R'
inst✝⁵ : CommRing S'
inst✝⁴ : Algebra R' S'
P' : Extension R' S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : Algebra R S'
inst✝ : IsScalarTower R R' S'
f : P.Hom P'
x : S
y : P.Ring
⊢ (CotangentSpace.map f) (x ⊗ₜ[P.Ring] (D R P.Ring) y) = (algebraMap S S') x ⊗ₜ[P'.Ring] (D R' P'.Ring) (f.toAlgHom y)

Tactic:
simp only [CotangentSpace.map, AlgHom.toRingHom_eq_coe, LinearMap.liftBaseChange_tmul,
    LinearMap.coe_comp, LinearMap.coe_restrictScalars, Function.comp_apply, map_D, mk_apply]
  rw [smul_tmul', ← Algebra.algebraMap_eq_smul_one]
  rfl

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Vanishing

Goal state before:
pp: case mpr
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
h : ∀ (M' : Submodule R M), M'.FG → Injective ⇑(rTensor N M'.subtype)
k : ℕ
m : Fin k → M
n : Fin k → N
hmn : ∑ i, m i ⊗ₜ[R] n i = 0
⊢ VanishesTrivially R m n

Tactic:
exact vanishesTrivially_of_sum_tmul_eq_zero_of_rTensor_injective R
      (h _ (fg_span (Set.finite_range _))) hmn

Goal state after:
Module: Mathlib.RingTheory.Localization.Finiteness

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
M : Submonoid R
S' : Type u_4
inst✝⁵ : CommSemiring S'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R S
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsLocalization (Submonoid.map (algebraMap R S) M) S'
x : S
s : Finset S'
hx : (algebraMap S S') x ∈ Submodule.span R ↑s
g : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') ⋯
g_apply : ∀ (x : S), g x = (algebraMap S S') x
y : ↥(Submonoid.map (algebraMap R S) M) := commonDenomOfFinset (Submonoid.map (algebraMap R S) M) s
hx₁ : ↑y • ↑s = ⇑g '' ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s)
y' : R
hy' : y' ∈ ↑M
e : (algebraMap R S) y' = ↑y
⊢ ∃ m, m • x ∈ Submodule.span R ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s)

Tactic:
have : algebraMap R S y' • (s : Set S') = y' • (s : Set S') := by
    simp_rw [Algebra.algebraMap_eq_smul_one, smul_assoc, one_smul]

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
M : Submonoid R
S' : Type u_4
inst✝⁵ : CommSemiring S'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R S
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsLocalization (Submonoid.map (algebraMap R S) M) S'
x : S
s : Finset S'
hx : (algebraMap S S') x ∈ Submodule.span R ↑s
g : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') ⋯
g_apply : ∀ (x : S), g x = (algebraMap S S') x
y : ↥(Submonoid.map (algebraMap R S) M) := commonDenomOfFinset (Submonoid.map (algebraMap R S) M) s
hx₁ : ↑y • ↑s = ⇑g '' ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s)
y' : R
hy' : y' ∈ ↑M
e : (algebraMap R S) y' = ↑y
this : (algebraMap R S) y' • ↑s = y' • ↑s
⊢ ∃ m, m • x ∈ Submodule.span R ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s)
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
p : PrimeSpectrum R
hp : p ∈ support R M
⊢ annihilator R M ≤ p.asIdeal

Tactic:
by
  obtain ⟨m, hm⟩ := mem_support_iff_exists_annihilator.mp hp
  exact le_trans ((Submodule.subtype _).annihilator_le_of_injective Subtype.val_injective) hm

Goal state after:
Module: Mathlib.RingTheory.Localization.Finiteness

Goal state before:
pp: R : Type u
inst✝¹¹ : CommSemiring R
S : Submonoid R
Rₚ : Type v
inst✝¹⁰ : CommSemiring Rₚ
inst✝⁹ : Algebra R Rₚ
inst✝⁸ : IsLocalization S Rₚ
M : Type w
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
Mₚ : Type t
inst✝⁵ : AddCommMonoid Mₚ
inst✝⁴ : Module R Mₚ
inst✝³ : Module Rₚ Mₚ
inst✝² : IsScalarTower R Rₚ Mₚ
f : M →ₗ[R] Mₚ
inst✝¹ : IsLocalizedModule S f
inst✝ : Module.Finite R M
⊢ Module.Finite Rₚ Mₚ

Tactic:
classical
  obtain ⟨T, hT⟩ := ‹Module.Finite R M›
  use T.image f
  simpa using span_eq_top_of_isLocalizedModule Rₚ S f hT

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

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

Tactic:
apply (cancel_right K.mkQ_surjective).mp

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

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝¹ : Monoid R
inst✝ : HasDistribNeg R
i : Fin (n + 1)
j : Fin n
⊢ Odd (↑i + ↑j) ↔ Even (↑i + ↑j + 1)

Tactic:
Nat.even_add_one,

Goal state after:
n : ℕ
R : Type u_1
inst✝¹ : Monoid R
inst✝ : HasDistribNeg R
i : Fin (n + 1)
j : Fin n
⊢ Odd (↑i + ↑j) ↔ ¬Even (↑i + ↑j)
Module: Mathlib.LinearAlgebra.ExteriorPower.Pairing

Goal state before:
pp: 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 j : ι⦄, i ≠ j → (f i) (x j) = 0
n : ℕ
a b : Fin n ↪o ι
h : a ≠ b
x✝¹ : 1 ∈ Finset.univ
h' : ¬∏ i, (f (a i)) (x (b (1 i))) = 0
this : ⇑a = ⇑b ∘ ⇑1
hσ : Monotone ⇑1
hσ' : Monotone ⇑(Equiv.symm 1)
x✝ : Fin n
⊢ a x✝ = b x✝

Tactic:
apply congr_fun this

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
⊢ ∀ (i : Fin n), Matrix.of (fun i j ↦ (b.coord ((ofFinEmbEquiv.symm s) j)) ((⇑b ∘ ⇑(ofFinEmbEquiv.symm t)) i)) i k = 0

Tactic:
simp_rw [Matrix.of_apply, Basis.coord_apply, Function.comp_apply, Basis.repr_self]

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
⊢ ∀ (i : Fin n), (Finsupp.single ((ofFinEmbEquiv.symm t) i) 1) ((ofFinEmbEquiv.symm s) k) = 0
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 : ⊤ ≤ Submodule.span R (Set.range (⇑((TensorProduct.mk R k M) 1) ∘ v))
⊢ ∃ κ a b, ∀ (i : κ), b i = v (a i)

Tactic:
← SetLike.coe_subset_coe,

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 : ↑⊤ ⊆ ↑(Submodule.span R (Set.range (⇑((TensorProduct.mk R k M) 1) ∘ v)))
⊢ ∃ κ 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 𝔪))
ι : 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)))
⊢ ⊤ ≤ Submodule.span k (Set.range (⇑((TensorProduct.mk R k M) 1) ∘ v))

Tactic:
exact Set.Subset.trans this (Submodule.span_subset_span _ _ _)

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : FinitePresentation R M
H : Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype 𝔪))
ι : 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)) = ⊤
hli : LinearIndependent k ((⇑((TensorProduct.mk R k M) 1) ∘ v) ∘ a)
⊢ ∃ κ a b, ∀ (i : κ), b i = v (a i)

Tactic:
obtain ⟨b, hb⟩ := exists_basis_of_basis_baseChange (v ∘ a) hli hsp H

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)) = ⊤
hli : LinearIndependent k ((⇑((TensorProduct.mk R k M) 1) ∘ v) ∘ a)
b : Basis κ R M
hb : ∀ (i : κ), b i = (v ∘ a) i
⊢ ∃ κ a b, ∀ (i : κ), b i = v (a i)
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
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
⊢ False

Tactic:
obtain ⟨s, hs⟩ : (⊤ : Submodule R K).FG := Module.Finite.fg_top

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
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 = ⊤
⊢ False
Module: Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsGCDMonoid R
J : Ideal R
this✝ : NormalizedGCDMonoid R := Classical.arbitrary (NormalizedGCDMonoid R)
K : Ideal R
hJK0 : J * K ≠ 0
hK : Submodule.IsPrincipal (J * K)
x : R
hJK : J * K = R ∙ x
hxmemJK : x ∈ J * K
this : ∃ T, ↑T ⊆ ↑K ∧ x ∈ J * span ↑T
⊢ Submodule.IsPrincipal J

Tactic:
obtain ⟨T, hTK, hxT⟩ := this

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsGCDMonoid R
J : Ideal R
this : NormalizedGCDMonoid R := Classical.arbitrary (NormalizedGCDMonoid R)
K : Ideal R
hJK0 : J * K ≠ 0
hK : Submodule.IsPrincipal (J * K)
x : R
hJK : J * K = R ∙ x
hxmemJK : x ∈ J * K
T : Finset R
hTK : ↑T ⊆ ↑K
hxT : x ∈ J * span ↑T
⊢ Submodule.IsPrincipal J
Module: Mathlib.RingTheory.LocalProperties.Projective

Goal state before:
pp: R : Type u_1
M : Type uM
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
H : ∀ (I : Ideal R) (x : I.IsMaximal), Projective (Localization.AtPrime I) (LocalizedModule I.primeCompl M)
inst✝ : FinitePresentation R M
s : Finset M
hs : Submodule.span R ↑s = ⊤
N : Type (max u_1 uM) := ↥s →₀ R
f : N →ₗ[R] M := Finsupp.linearCombination R Subtype.val
hf : Function.Surjective ⇑f
this : ∀ (I : Ideal R) (hI : I.IsMaximal), ∃ h, (LocalizedModule.map I.primeCompl) f ∘ₗ h = LinearMap.id
g : M →ₗ[R] N
hg : f ∘ₗ g = LinearMap.id
⊢ Projective R M

Tactic:
exact Module.Projective.of_split _ _ hg

Goal state after:
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✝
X : Type u_5
inst✝¹ : TopologicalSpace X
U : Set X
inst✝ : (x : X) → Decidable (x ∈ U)
hU : IsClopen U
x✝ : X
⊢ x✝ ∈ (fun x ↦ if x ∈ U then 0 else 1) ⁻¹' {0} ↔ x✝ ∈ U

Tactic:
simp only [mem_singleton_iff, Fin.one_eq_zero_iff, mem_preimage, ite_eq_left_iff,
        Nat.succ_succ_ne_one]

Goal state after:
X✝ : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝² : TopologicalSpace X✝
X : Type u_5
inst✝¹ : TopologicalSpace X
U : Set X
inst✝ : (x : X) → Decidable (x ∈ U)
hU : IsClopen U
x✝ : X
⊢ x✝ ∉ U → False ↔ x✝ ∈ U
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
C₀ C₁ C₂ : Set X
h₀ : C₀ ⊆ C₁ ∪ C₂
h₁ : IsClosed[inst✝¹] C₁
h₂ : IsClosed[inst✝¹] C₂
f₁ : LocallyConstant (↑C₁) Z
f₂ : LocallyConstant (↑C₂) Z
inst✝ : DecidablePred fun x ↦ x ∈ C₁
hf : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f₁ ⟨x, ⋯⟩ = f₂ ⟨x, ⋯⟩
this : (j : ↑C₀) → Decidable (j ∈ Subtype.val ⁻¹' C₁) := fun j ↦ decidable_of_iff (↑j ∈ C₁) ⋯
x : X
hx₀ : x ∈ C₀
hx₁ : x ∈ C₁
hx₂ : x ∈ C₂
⊢ (comap { toFun := C₁.restrictPreimage Subtype.val, continuous_toFun := ⋯ } f₁) ⟨⟨x, hx₀⟩, ⋯⟩ =
    (comap { toFun := C₂.restrictPreimage Subtype.val, continuous_toFun := ⋯ } f₂) ⟨⟨x, hx₀⟩, ⋯⟩

Tactic:
simpa using hf x ⟨hx₁, hx₂⟩

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsStablyFree R M
inst✝ : Module.Invertible R M
⊢ Free R M

Tactic:
rcases subsingleton_or_nontrivial R with _ | _
  · exact Module.Free.of_subsingleton' R M
  obtain ⟨N, _, _, _, _, _⟩ := IsStablyFree.exist_free_prod R M
  let n := Module.finrank R N
  have hp : Module.finrank R (M × N) = n + 1 := by
    let 𝔭 : PrimeSpectrum R := Nonempty.some inferInstance
    have h1 : rankAtStalk M 𝔭 = 1 := by simp [rankAtStalk, Invertible.finrank_eq_one]
    have heq := congr($(rankAtStalk_prod M N) 𝔭)
    simp only [rankAtStalk_eq_finrank_of_free, Pi.natCast_apply, Pi.add_apply, h1] at heq
    grind
  let e : R ≃ₗ[R] ⋀[R]^(n + 1) (M × N) :=
    (Module.nonempty_linearEquiv_of_finrank_eq_one <| by simp [exteriorPower.finrank_eq, hp]).some
  let bN : Module.Basis (Fin n) R N := Module.finBasis R N
  let f : R →ₗ[R] M := exteriorPower.cofactorToLeft bN ∘ₗ e
  exact Module.Free.of_equiv <| LinearEquiv.ofBijective f <| Invertible.bijective_of_surjective <|
    fun x ↦ ⟨e.symm (exteriorPower.ιMulti R (n + 1) (Fin.cons (x, 0) fun i ↦ (0, bN i))), by
      simp [f, exteriorPower.cofactorToLeft_ιMulti_cons]⟩

Goal state after:
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
⊢ Function.Bijective ⇑↑((LinearEquiv.rTensor N (linearEquivDual e)).symm ≪≫ₗ e)

Tactic:
apply LinearEquiv.bijective

Goal state after:
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
N : Type (max v u) := Dual R M
e : M ⊗[R] N ≃ₗ[R] R := TensorProduct.comm R M N ≪≫ₗ linearEquiv R M
S : Finset (M × N)
hS : e.symm 1 = ∑ i ∈ S, i.1 ⊗ₜ[R] i.2
f : (↥S →₀ N) →ₗ[R] R := (Finsupp.lsum R) fun i ↦ ↑e ∘ₗ (TensorProduct.mk R M N) (↑i).1
this : Function.Surjective ⇑f
g : R →ₗ[R] ↥S →₀ N
hg : f ∘ₗ g = LinearMap.id
⊢ Module.Finite R M ∧ Projective R M

Tactic:
let aux := finsuppRight R _ M N S ≪≫ₗ Finsupp.mapRange.linearEquiv e
  let f' : (S →₀ R) →ₗ[R] M := TensorProduct.rid R M ∘ₗ f.lTensor M ∘ₗ aux.symm
  let g' : M →ₗ[R] S →₀ R := aux ∘ₗ g.lTensor M ∘ₗ (TensorProduct.rid R M).symm
  have : Function.Surjective f' := by simpa [f'] using LinearMap.lTensor_surjective _ this
  refine ⟨.of_surjective f' this, .of_split g' f' <| LinearMap.ext fun m ↦ ?_⟩
  simp [f', g', show f (g 1) = 1 from DFunLike.congr_fun hg 1]

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

Goal state before:
pp: case right
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
splits : ∀ (x : K), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits
x : ↥(⨆ f, f.fieldRange)
x✝ : x ∈ ⊤
⊢ (⨆ f, f.fieldRange).val x ∈ ↑(⨆ i, IntermediateField.map (⨆ f, f.fieldRange).val i.fieldRange)

Tactic:
refine (iSup_le fun f ↦ ?_ : normalClosure F K L ≤ _) x.2

Goal state after:
case right
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
splits : ∀ (x : K), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits
x : ↥(⨆ f, f.fieldRange)
x✝ : x ∈ ⊤
f : K →ₐ[F] L
⊢ f.fieldRange ≤ ⨆ i, IntermediateField.map (⨆ f, f.fieldRange).val i.fieldRange
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: case a
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* (Polynomial.map ιFE g).SplittingField := algebraMap E (Polynomial.map ιFE g).SplittingField
c : F
hc :
  ∀ α' ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots,
    ∀ β' ∈ (Polynomial.map (ιEE'.comp ιFE) g).roots, -(α' - ιEE' α) / (β' - ιEE' β) ≠ (ιEE'.comp ιFE) c
γ : E := α + c • β
β_in_Fγ : β ∈ F⟮γ⟯
α_in_Fαβ : α ∈ F⟮α, β⟯
⊢ γ ∈ F⟮α, β⟯

Tactic:
have β_in_Fαβ : β ∈ F⟮α, β⟯ := subset_adjoin F {α, β} (Set.mem_insert_of_mem α rfl)

Goal state after:
case a
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* (Polynomial.map ιFE g).SplittingField := algebraMap E (Polynomial.map ιFE g).SplittingField
c : F
hc :
  ∀ α' ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots,
    ∀ β' ∈ (Polynomial.map (ιEE'.comp ιFE) g).roots, -(α' - ιEE' α) / (β' - ιEE' β) ≠ (ιEE'.comp ιFE) c
γ : E := α + c • β
β_in_Fγ : β ∈ F⟮γ⟯
α_in_Fαβ : α ∈ F⟮α, β⟯
β_in_Fαβ : β ∈ F⟮α, β⟯
⊢ γ ∈ F⟮α, β⟯
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 : IntermediateField F L
σ : L →ₐ[F] L
⊢ normalClosure F (↥(map σ K)) L = normalClosure F (↥K) L

Tactic:
by
  have (σ : Gal(L/F)) : normalClosure F (K.map (σ : L →ₐ[F] L)) L = normalClosure F K L := by
    simp_rw [normalClosure_def'', map_map]
    exact (Equiv.mulRight σ).iSup_congr fun _ ↦ rfl
  exact this ((Algebra.IsAlgebraic.algEquivEquivAlgHom _ _).symm σ)

Goal state after:
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: case a
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
f : F → IntermediateField F E := fun x ↦ F⟮α + x • β⟯
x y : F
hneq : x ≠ y
heq : f x = f y
α_in_Fαβ : α ∈ F⟮α, β⟯
⊢ α + x • β ∈ F⟮α, β⟯

Tactic:
have β_in_Fαβ : β ∈ F⟮α, β⟯ := subset_adjoin F {α, β} (Set.mem_insert_of_mem α rfl)

Goal state after:
case a
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
f : F → IntermediateField F E := fun x ↦ F⟮α + x • β⟯
x y : F
hneq : x ≠ y
heq : f x = f y
α_in_Fαβ : α ∈ F⟮α, β⟯
β_in_Fαβ : β ∈ F⟮α, β⟯
⊢ α + x • β ∈ F⟮α, β⟯
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' = ∅ ∨ B \ B' = {e})
hcard : (B' \ B).encard = (B \ B').encard
⊢ M.IsBase (insert f (B \ {e}))

Tactic:
obtain ⟨hfB, (h | h)⟩ := hIB'

Goal state after:
case inl
α : 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'
hcard : (B' \ B).encard = (B \ B').encard
hfB : f ∈ B'
h : B \ B' = ∅
⊢ M.IsBase (insert f (B \ {e}))

case inr
α : 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'
hcard : (B' \ B).encard = (B \ B').encard
hfB : f ∈ B'
h : B \ B' = {e}
⊢ M.IsBase (insert f (B \ {e}))
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hX : X ⊆ M.E
⊢ M.IsBasis I X ↔ Maximal (fun I ↦ M.Indep I ∧ I ⊆ X) I

Tactic:
rw [IsBasis, and_iff_left hX]

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

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

Tactic:
and_assoc,

Goal state after:
α : Type u_1
M : Matroid α
I : Set α
⊢ M.Indep I ∧ (∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → J ⊆ I → I = J) ∧ I ⊆ M.E ↔ M.Indep I
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
e : A ⊗[R] M ≃ₗ[A] A
inst✝¹ : Flat R M
inst✝ : FaithfulSMul R A
I : Submodule R A
⊢ ↥I ⊗[R] ↥(submoduleAlgebra e) ≃ₗ[R] ↥(I * submoduleAlgebra e)

Tactic:
by
  refine .ofBijective _ ⟨.of_comp (f := Submodule.subtype _) ?_, Submodule.mulMap'_surjective _ _⟩
  convert!
    ((tensorSubmoduleAlgebraEquiv e).restrictScalars R).injective.comp
      (Flat.rTensor_preserves_injective_linearMap _ I.subtype_injective)
  simp_rw [← LinearEquiv.coe_toLinearMap, ← LinearMap.coe_comp]
  congr 1; ext; rfl

Goal state after: