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'
f g : P.Hom P'
x y : P.Ring
this : Algebra P.Ring S' := ((algebraMap S S').comp (algebraMap P.Ring S)).toAlgebra
⊢ (f.toAlgHom x - P'.σ ((algebraMap P.Ring S') x)) * (f.toAlgHom y - g.toAlgHom y) +
      (g.toAlgHom y - P'.σ ((algebraMap P.Ring S') y)) * (f.toAlgHom x - g.toAlgHom x) ∈
    P'.ker * P'.ker

Tactic:
refine Ideal.add_mem _ (Ideal.mul_mem_mul ?_ ?_) (Ideal.mul_mem_mul ?_ ?_)

Goal state after:
case refine_1
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 g : P.Hom P'
x y : P.Ring
this : Algebra P.Ring S' := ((algebraMap S S').comp (algebraMap P.Ring S)).toAlgebra
⊢ f.toAlgHom x - P'.σ ((algebraMap P.Ring S') x) ∈ P'.ker

case refine_2
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 g : P.Hom P'
x y : P.Ring
this : Algebra P.Ring S' := ((algebraMap S S').comp (algebraMap P.Ring S)).toAlgebra
⊢ f.toAlgHom y - g.toAlgHom y ∈ P'.ker

case refine_3
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 g : P.Hom P'
x y : P.Ring
this : Algebra P.Ring S' := ((algebraMap S S').comp (algebraMap P.Ring S)).toAlgebra
⊢ g.toAlgHom y - P'.σ ((algebraMap P.Ring S') y) ∈ P'.ker

case refine_4
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 g : P.Hom P'
x y : P.Ring
this : Algebra P.Ring S' := ((algebraMap S S').comp (algebraMap P.Ring S)).toAlgebra
⊢ f.toAlgHom x - g.toAlgHom x ∈ P'.ker
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 g : P.Hom P'
⊢ P.Ring →ₗ[R] ↥P'.ker

Tactic:
refine ((f.toAlgHom.toLinearMap - g.toAlgHom.toLinearMap).codRestrict
    (P'.ker.restrictScalars R) ?_)
  intro x
  simp only [LinearMap.sub_apply, AlgHom.toLinearMap_apply, ker,
    Submodule.restrictScalars_mem, RingHom.mem_ker, map_sub, algebraMap_toRingHom,
    sub_self, toAlgHom_apply]

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
e : S ≃ₐ[R] S'
this✝⁴ : Algebra S S' := e.toRingEquiv.toRingHom.toAlgebra
this✝³ : Algebra S' S := e.symm.toRingEquiv.toRingHom.toAlgebra
this✝² : IsScalarTower R S S'
this✝¹ : IsScalarTower R S' S
this✝ : IsScalarTower S S' S
this : IsScalarTower S' S S'
x : H1Cotangent R S
⊢ (↑S (map R R S' S) ∘ₗ map R R S S') x = x

Tactic:
rw [map, map, ← Extension.H1Cotangent.map_comp, Extension.H1Cotangent.map_eq,
        Extension.H1Cotangent.map_id, LinearMap.id_apply]

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
e : S ≃ₐ[R] S'
this✝⁴ : Algebra S S' := e.toRingEquiv.toRingHom.toAlgebra
this✝³ : Algebra S' S := e.symm.toRingEquiv.toRingHom.toAlgebra
this✝² : IsScalarTower R S S'
this✝¹ : IsScalarTower R S' S
this✝ : IsScalarTower S S' S
this : IsScalarTower S' S S'
x : H1Cotangent R S'
⊢ (↑S' (map R R S S') ∘ₗ map R R S' S) x = x

Tactic:
rw [map, map, ← Extension.H1Cotangent.map_comp, Extension.H1Cotangent.map_eq,
        Extension.H1Cotangent.map_id, LinearMap.id_apply]

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
N₁ N₂ : Submodule R M
h : N₁ ≤ N₂
h' : N₂.FG
hN : Submodule.map (𝔪 • N₂).mkQ N₁ = Submodule.map (𝔪 • N₂).mkQ N₂
this : N₂ ≤ N₁ ⊔ 𝔪 • N₂
⊢ 𝔪 ≤ ⊥.jacobson

Tactic:
rw [jacobson_eq_maximalIdeal]; exact bot_ne_top

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 t) j ∈ t

Tactic:
powersetCard.ofFinEmbEquiv_symm_apply,

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.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
R : Type u_5
inst✝ : One R
U : Set X
f : LocallyConstant X R
hU : IsClopen U
s : Set R
⊢ IsOpen[inst✝¹] (⇑f ⁻¹' s ∩ U ∪ 1 ⁻¹' s ∩ Uᶜ)

Tactic:
exact ((f.2 s).inter hU.isOpen).union ((IsLocallyConstant.const 1 s).inter hU.compl.isOpen)

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
p : PrimeSpectrum R
q : PrimeSpectrum (p.asIdeal.Fiber S)
x : p.asIdeal.Fiber S
r : R
hr : r ∉ p.asIdeal
s : S
e : r • x = 1 ⊗ₜ[R] s
this : ∀ {R : Type ?u.120} [inst : CommSemiring R] (self : PrimeSpectrum R), self.asIdeal.IsPrime
⊢ x ∈
      ((fun q ↦
            {
              asIdeal :=
                RingHom.ker
                  (Algebra.TensorProduct.lift (Ideal.ResidueField.mapₐ p.asIdeal (↑q).asIdeal (ofId R S) ⋯)
                      (IsScalarTower.toAlgHom R S (↑q).asIdeal.ResidueField) ⋯).toRingHom,
              isPrime := ⋯ })
          ((fun q ↦ ⟨comap includeRight.toRingHom q, ⋯⟩) q)).asIdeal ↔
    x ∈ q.asIdeal

Tactic:
← Ideal.IsPrime.mul_mem_left_iff (x := algebraMap _ _ r),

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
p✝ : Ideal R
inst✝ : p✝.IsPrime
p : PrimeSpectrum R
q : PrimeSpectrum (p.asIdeal.Fiber S)
x : p.asIdeal.Fiber S
r : R
hr : r ∉ p.asIdeal
s : S
e : r • x = 1 ⊗ₜ[R] s
this : ∀ {R : Type (max u_1 u_2)} [inst : CommSemiring R] (self : PrimeSpectrum R), self.asIdeal.IsPrime
⊢ (algebraMap R (p.asIdeal.Fiber S)) r * x ∈
      ((fun q ↦
            {
              asIdeal :=
                RingHom.ker
                  (Algebra.TensorProduct.lift (Ideal.ResidueField.mapₐ p.asIdeal (↑q).asIdeal (ofId R S) ⋯)
                      (IsScalarTower.toAlgHom R S (↑q).asIdeal.ResidueField) ⋯).toRingHom,
              isPrime := ⋯ })
          ((fun q ↦ ⟨comap includeRight.toRingHom q, ⋯⟩) q)).asIdeal ↔
    x ∈ q.asIdeal

R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
p✝ : Ideal R
inst✝ : p✝.IsPrime
p : PrimeSpectrum R
q : PrimeSpectrum (p.asIdeal.Fiber S)
x : p.asIdeal.Fiber S
r : R
hr : r ∉ p.asIdeal
s : S
e : r • x = 1 ⊗ₜ[R] s
this : ∀ {R : Type (max u_1 u_2)} [inst : CommSemiring R] (self : PrimeSpectrum R), self.asIdeal.IsPrime
⊢ (algebraMap R (p.asIdeal.Fiber S)) r ∉
    ((fun q ↦
          {
            asIdeal :=
              RingHom.ker
                (Algebra.TensorProduct.lift (Ideal.ResidueField.mapₐ p.asIdeal (↑q).asIdeal (ofId R S) ⋯)
                    (IsScalarTower.toAlgHom R S (↑q).asIdeal.ResidueField) ⋯).toRingHom,
            isPrime := ⋯ })
        ((fun q ↦ ⟨comap includeRight.toRingHom q, ⋯⟩) q)).asIdeal
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: case zero
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
⊢ map f (derivedSeries G 0) ≤ derivedSeries G' 0

Tactic:
exact le_top

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

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

Tactic:
← Ideal.IsPrime.mul_mem_left_iff (x := algebraMap _ _ r),

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

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

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

Goal state before:
pp: case succ
G : Type u_1
inst✝² : Group G
G' : Type u_3
G'' : Type u_4
inst✝¹ : Group G'
inst✝ : Group G''
f : G' →* G
g : G →* G''
hfg : g.ker ≤ f.range
hG' : IsSolvable G'
hG'' : IsSolvable G''
n : ℕ
hn : derivedSeries G'' n = ⊥
m : ℕ
hm : derivedSeries G (n + m) ≤ map f (derivedSeries G' m)
⊢ derivedSeries G (n + (m + 1)) ≤ map f (derivedSeries G' (m + 1))

Tactic:
| succ m hm =>

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✝ : FinitePresentation R M
f : R
⊢ ↑(basicOpen f) ⊆ freeLocus R M ↔ comap (algebraMap R (Localization (Submonoid.powers f))) ⁻¹' freeLocus R M = Set.univ

Tactic:
Set.preimage_eq_univ_iff,

Goal state after:
R : Type uR
M : Type uM
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : FinitePresentation R M
f : R
⊢ ↑(basicOpen f) ⊆ freeLocus R M ↔ Set.range (comap (algebraMap R (Localization (Submonoid.powers f)))) ⊆ freeLocus R M
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
e : M ⊗[R] N ≃ₗ[R] R
x✝ : P ⊗[R] M →ₗ[R] Q ⊗[R] M
⊢ (rTensorInv P Q e) ((LinearMap.rTensorHom M).toFun ((rTensorInv P Q e) x✝)) = (rTensorInv P Q e) x✝

Tactic:
rw [LinearMap.toFun_eq_coe, rTensorInv_leftInverse]

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
ne : Nonempty (K →ₐ[F] L)
h : Normal F L
φ : K →ₐ[F] L
⊢ IsNormalClosure F K ↥(normalClosure F K L)

Tactic:
apply (h.toIsAlgebraic.of_injective φ φ.injective).isNormalClosure_normalClosure

Goal state after:
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
ne : Nonempty (K →ₐ[F] L)
h : Normal F L
φ : K →ₐ[F] L
⊢ ∀ (x : K), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits
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
inst✝¹ : Module.Invertible R M
inst✝ : Module.Invertible R N
⊢ ↑(Units.mkOfMulEqOne ⟦SemimoduleCat.of R (Finite.reprₛ R (M ⊗[R] N))⟧
        ⟦SemimoduleCat.of R (Dual R (Finite.reprₛ R (M ⊗[R] N)))⟧ ⋯) =
    ↑((equivShrink (Skeleton (SemimoduleCat R))ˣ).symm.toFun
          ((equivShrink (Skeleton (SemimoduleCat R))ˣ)
            (Units.mkOfMulEqOne ⟦SemimoduleCat.of R (Finite.reprₛ R M)⟧ ⟦SemimoduleCat.of R (Dual R (Finite.reprₛ R M))⟧
              ⋯)) *
        (equivShrink (Skeleton (SemimoduleCat R))ˣ).symm.toFun
          ((equivShrink (Skeleton (SemimoduleCat R))ˣ)
            (Units.mkOfMulEqOne ⟦SemimoduleCat.of R (Finite.reprₛ R N)⟧ ⟦SemimoduleCat.of R (Dual R (Finite.reprₛ R N))⟧
              ⋯)))

Tactic:
Equiv.toFun_as_coe,

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
inst✝¹ : Module.Invertible R M
inst✝ : Module.Invertible R N
⊢ ↑(Units.mkOfMulEqOne ⟦SemimoduleCat.of R (Finite.reprₛ R (M ⊗[R] N))⟧
        ⟦SemimoduleCat.of R (Dual R (Finite.reprₛ R (M ⊗[R] N)))⟧ ⋯) =
    ↑((equivShrink (Skeleton (SemimoduleCat R))ˣ).symm
          ((equivShrink (Skeleton (SemimoduleCat R))ˣ)
            (Units.mkOfMulEqOne ⟦SemimoduleCat.of R (Finite.reprₛ R M)⟧ ⟦SemimoduleCat.of R (Dual R (Finite.reprₛ R M))⟧
              ⋯)) *
        (equivShrink (Skeleton (SemimoduleCat R))ˣ).symm
          ((equivShrink (Skeleton (SemimoduleCat R))ˣ)
            (Units.mkOfMulEqOne ⟦SemimoduleCat.of R (Finite.reprₛ R N)⟧ ⟦SemimoduleCat.of R (Dual R (Finite.reprₛ R N))⟧
              ⋯)))
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
⊢ ↑(Units.mkOfMulEqOne ⟦SemimoduleCat.of R (Finite.reprₛ R (Dual R M))⟧
        ⟦SemimoduleCat.of R (Dual R (Finite.reprₛ R (Dual R M)))⟧ ⋯) =
    ↑((equivShrink (Skeleton (SemimoduleCat R))ˣ).symm.toFun
          ((equivShrink (Skeleton (SemimoduleCat R))ˣ)
            (Units.mkOfMulEqOne ⟦SemimoduleCat.of R (Finite.reprₛ R M)⟧ ⟦SemimoduleCat.of R (Dual R (Finite.reprₛ R M))⟧
              ⋯)))⁻¹

Tactic:
Equiv.toFun_as_coe,

Goal state after:
R : Type u
M : Type v
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Invertible R M
⊢ ↑(Units.mkOfMulEqOne ⟦SemimoduleCat.of R (Finite.reprₛ R (Dual R M))⟧
        ⟦SemimoduleCat.of R (Dual R (Finite.reprₛ R (Dual R M)))⟧ ⋯) =
    ↑((equivShrink (Skeleton (SemimoduleCat R))ˣ).symm
          ((equivShrink (Skeleton (SemimoduleCat R))ˣ)
            (Units.mkOfMulEqOne ⟦SemimoduleCat.of R (Finite.reprₛ R M)⟧ ⟦SemimoduleCat.of R (Dual R (Finite.reprₛ R M))⟧
              ⋯)))⁻¹
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: case inr.inr
α : Type u_1
IsBase : Set α → Prop
B₁ B₂ : Set α
exch : ExchangeProperty IsBase
hB₁ : IsBase B₁
hB₂ : IsBase B₂
e : α
he : e ∈ B₂ \ B₁
hcard : ((B₂ \ B₁) \ {e}).encard < (B₂ \ B₁).encard
f : α
hf : f ∈ B₁ \ B₂
hB' : IsBase (insert f (B₂ \ {e}))
this : (insert f (B₂ \ {e}) \ B₁).encard < (B₂ \ B₁).encard
hencard : ((B₁ \ B₂) \ {f}).encard ≤ ((B₂ \ B₁) \ {e}).encard
⊢ ((B₁ \ B₂) \ {f}).encard + 1 ≤ ((B₂ \ B₁) \ {e}).encard + 1

Tactic:
gcongr

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

Goal state before:
pp: α : Type u_1
M : Matroid α
B : Set α
hB : B ⊆ M.E
⊢ M.IsBase (M.E \ B) ↔
    (B ⊆ M.E ∧ ∃ B_1, M.IsBase B_1 ∧ Disjoint B B_1) ∧
      ∀ ⦃y : Set α⦄, (y ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint y B) → B ⊆ y → B = y

Tactic:
and_iff_right hB,

Goal state after:
α : Type u_1
M : Matroid α
B : Set α
hB : B ⊆ M.E
⊢ M.IsBase (M.E \ B) ↔
    (∃ B_1, M.IsBase B_1 ∧ Disjoint B B_1) ∧ ∀ ⦃y : Set α⦄, (y ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint y B) → B ⊆ y → B = y
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: case pos
F✝ : Type u_1
E✝ : Type u_2
inst✝⁵ : Field F✝
inst✝⁴ : Field E✝
inst✝³ : Algebra F✝ E✝
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
heq : F⟮α ^ m⟯ = F⟮α ^ n⟯
hmn : m < n
hm : ¬m = 0
r s : F[X]
h : α ^ m = (aeval (α ^ n)) r / (aeval (α ^ n)) s
hzero : (aeval (α ^ n)) s = 0
⊢ IsAlgebraic F α

Tactic:
simp only [hzero, div_zero, pow_eq_zero_iff hm] at h
    exact h.symm ▸ isAlgebraic_zero

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

Goal state before:
pp: α : Type u_1
M✝ M : Matroid α
E : Set α
IsBase Indep : Set α → Prop
hE : E = M.E
hB : ∀ (B : Set α), IsBase B ↔ M.IsBase B
hI : ∀ (I : Set α), Indep I ↔ M.Indep I
⊢ ∀ X ⊆ E, ExistsMaximalSubsetProperty Indep X

Tactic:
by
    simp_rw [hE, show Indep = M.Indep from funext (by simp [hI])]
    exact M.maximality

Goal state after:
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
A : Type u_4
inst✝³ : CommSemiring R
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
⊢ (unitsToPic R A).range = relPic R A

Tactic:
by
  ext M; constructor <;> intro h
  · obtain ⟨I, rfl⟩ := h
    exact mk_eq_one_iff.mpr ⟨AlgebraTensorModule.congr (.refl ..) (unitsToPicEquiv I) ≪≫ₗ
      .ofBijective ((Algebra.TensorProduct.lmul'' R).toLinearMap ∘ₗ AlgebraTensorModule.lTensor A A
        I.1.subtype) (projective_units_and_mul'_comp_lTensor_bijective I).2⟩
  have e := (mk_eq_one_iff.mp h).some
  have f := (mk_eq_one_iff.mp (inv_mem h)).some
  refine ⟨(isUnit_of_mul_isUnit_left (x := submoduleAlgebra e) (y := submoduleAlgebra f) ?_).unit,
    mk_eq_iff.mpr ⟨submoduleAlgebraEquiv e⟩⟩
  have := eq_span_singleton_of_surjective <| LinearEquiv.surjective <|
    (congr (submoduleAlgebraEquiv e) (submoduleAlgebraEquiv f) ≪≫ₗ
    (mk_eq_one_iff.mp <| by simp_rw [mk_tensor, mk_eq_self, mul_inv_cancel]).some).symm ≪≫ₗ
    tensorSubmoduleAlgebraEquivMul f (submoduleAlgebra e)
  rw [this]
  apply_fun (⊤ * ·) at this
  simp_rw [← mul_assoc, top_mul_submoduleAlgebra] at this
  obtain ⟨a, -, eq⟩ := mem_mul_span_singleton.mp (this ▸ mem_top (x := 1))
  exact .map (spanSingleton R).toMonoidHom (.of_mul_eq_one_right _ eq)

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

Goal state before:
pp: α : Type u_1
E : Set α
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug :
  ∀ ⦃I J : Set α⦄, Indep I → I.Finite → Indep J → J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
htofin : ∀ (I : Set α) (e : α), Indep I → ¬Indep (insert e I) → ∃ I₀ ⊆ I, I₀.Finite ∧ ¬Indep (insert e I₀)
I B : Set α
hI : Indep I
hImax : ¬Maximal Indep I
hBmax : Maximal Indep B
e : α
heI : e ∉ I
hins : Indep (insert e I)
heB : e ∉ B
hcon : ∀ x ∈ B \ I, ¬Indep (insert x I)
heBdep : ¬Indep (insert e B)
B₀ : Set α
hB₀B : B₀ ⊆ B
hB₀fin : B₀.Finite
hB₀e : ¬Indep (insert e B₀)
hB₀ : Indep B₀
I₀ : Set α
hI₀I : I₀ ⊆ I
hI₀fin : I₀.Finite
hI₀ : ∀ x ∈ B₀ \ I₀, ¬Indep (insert x I₀)
E₀ : Set α := insert e (I₀ ∪ B₀)
hE₀fin : E₀.Finite
J : Set α
hJmax : ∀ ⦃j : Set α⦄, (fun x ↦ x ∈ {J | B₀ ⊆ J ∧ Indep J ∧ J ⊆ E₀}) j → id J ⊆ id j → id j ⊆ id J
hB₀J : B₀ ⊆ J
hJ : Indep J
hJss : J ⊆ E₀
heI₀ : e ∉ I₀
heI₀i : Indep (insert e I₀)
heJ : e ∉ J
hJfin : J.Finite
hlt : J.ncard < (insert e I₀).ncard
f : α
hfI : f ∈ insert e I₀
hfJ : f ∉ J
hfi : Indep (insert f J)
hfE₀ : f ∈ E₀
⊢ False

Tactic:
exact hfJ <| insert_eq_self.1 <| le_imp_eq_iff_le_imp_ge'.2 (hJmax
          ⟨hB₀J.trans <| subset_insert _ _, hfi, insert_subset hfE₀ hJss⟩) (subset_insert _ _)

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

Goal state before:
pp: α : Type u_1
I E : Set α
⊢ (uniqueBaseOn (I ∩ E) E)✶ = uniqueBaseOn (E \ I) E

Tactic:
refine ext_isBase rfl (fun B (hB : B ⊆ E) ↦ ?_)

Goal state after:
α : Type u_1
I E B : Set α
hB : B ⊆ E
⊢ (uniqueBaseOn (I ∩ E) E)✶.IsBase B ↔ (uniqueBaseOn (E \ I) E).IsBase B
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: α : Type u_1
M✝ : Matroid α
I B X : Set α
M : Matroid α
⊢ ∀ (I : Set α), (I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) → I ⊆ M.E

Tactic:
by tauto

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

Goal state before:
pp: α : Type u_1
E : Set α
hE : E.Finite
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I J : Set α⦄, Indep I → Indep J → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
subset_ground : ∀ ⦃I : Set α⦄, Indep I → I ⊆ E
⊢ ∀ ⦃I J : Set α⦄, Indep I → Indep J → I.encard < J.encard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)

Tactic:
refine fun {I J} hI hJ hIJ ↦ indep_aug hI hJ ?_

Goal state after:
α : Type u_1
E : Set α
hE : E.Finite
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I J : Set α⦄, Indep I → Indep J → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
subset_ground : ∀ ⦃I : Set α⦄, Indep I → I ⊆ E
I J : Set α
hI : Indep I
hJ : Indep J
hIJ : I.encard < J.encard
⊢ I.ncard < J.ncard
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
R : Set α
h : M ↾ R <r M
⊢ (M ↾ R).E ⊂ M.E

Tactic:
refine h.isRestriction.subset.ssubset_of_ne (fun h' ↦ h.2 ⟨R, Subset.rfl, ?_⟩)

Goal state after:
α : Type u_1
M : Matroid α
R : Set α
h : M ↾ R <r M
h' : (M ↾ R).E = M.E
⊢ M = M ↾ R ↾ R