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

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
p : PrimeSpectrum R
inst✝ : Module.Finite R M
s : Finset M
hs : Submodule.span R ↑s = ⊤
H : ∀ m ∈ ↑s, ∃ x, x • m = 0 ∧ x ∉ p.asIdeal
x : { a // a ∈ ↑s } → R
hx : ∀ (x_1 : { a // a ∈ ↑s }), x x_1 • ↑x_1 = 0
hx' : ∀ (x_1 : { a // a ∈ ↑s }), x x_1 ∉ p.asIdeal
⊢ s.attach.prod x ∈ annihilator R M

Tactic:
← Submodule.annihilator_top,

Goal state after:
case refine_1
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
p : PrimeSpectrum R
inst✝ : Module.Finite R M
s : Finset M
hs : Submodule.span R ↑s = ⊤
H : ∀ m ∈ ↑s, ∃ x, x • m = 0 ∧ x ∉ p.asIdeal
x : { a // a ∈ ↑s } → R
hx : ∀ (x_1 : { a // a ∈ ↑s }), x x_1 • ↑x_1 = 0
hx' : ∀ (x_1 : { a // a ∈ ↑s }), x x_1 ∉ p.asIdeal
⊢ s.attach.prod x ∈ ⊤.annihilator
Module: Mathlib.RingTheory.LocalRing.Module

Goal state before:
pp: case mp
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
N : Submodule R M
inst✝ : Module.Finite R M
hN : Submodule.map ((TensorProduct.mk R k M) 1) N = ⊤
⊢ N = ⊤

Tactic:
let : Module k (M ⧸ (𝔪 • ⊤ : Submodule R M)) :=
      inferInstanceAs (Module (R ⧸ 𝔪) (M ⧸ 𝔪 • (⊤ : Submodule R M)))

Goal state after:
case mp
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
N : Submodule R M
inst✝ : Module.Finite R M
hN : Submodule.map ((TensorProduct.mk R k M) 1) N = ⊤
this : Module k (M ⧸ 𝔪 • ⊤) :=
  { smul := map_tensorProduct_mk_eq_top._aux_1_1, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯,
    add_smul := ⋯, zero_smul := ⋯ }
⊢ N = ⊤
Module: Mathlib.LinearAlgebra.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝¹ : Nontrivial R
inst✝ : Flat R ↥N
a b : ↥(M ⊓ N)
hc : Commute ↑a ↑b
h : LinearIndependent R ![a, b]
⊢ False

Tactic:
let m : Fin 2 → M := (inclusion inf_le_left) ∘ ![a, b]
  have hm : LinearIndependent R m := h.map' _ (ker_inclusion _ _ _)
  -- need this instance otherwise it only has semigroup structure
  let : AddCommGroup (Fin 2 →₀ N) := Finsupp.instAddCommGroup
  let n : Fin 2 →₀ N := .single 0 ⟨b.1, b.2.2⟩ - .single 1 ⟨a.1, a.2.2⟩
  have hn : mulLeftMap N m n = 0 := by simp [m, n, show _ * _ = _ * _ from hc]
  rw [← LinearMap.mem_ker, H.linearIndependent_left_of_flat hm, mem_bot] at hn
  simp only [Fin.isValue, sub_eq_zero, Finsupp.single_eq_single_iff, zero_ne_one, Subtype.mk.injEq,
    SetLike.coe_eq_coe, false_and, false_or, n] at hn
  repeat rw [AddSubmonoid.mk_eq_zero, ZeroMemClass.coe_eq_zero] at hn
  exact h.ne_zero 0 hn.2

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

Goal state before:
pp: case insert.specialize_2
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : Flat R M
ι : Type u
f : ι → R
n✝ : ι
s : Finset ι
hn : n✝ ∉ s
ih : ∀ (v : ι → M), LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v) → ∑ i ∈ s, f i • v i = 0 → ∀ i ∈ s, f i = 0
v : ι → M
h : LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v)
i : ι
hi : i ∈ insert n✝ s
l : ℕ
a : ↥(insert n✝ s) → Fin l → R
y : Fin l → M
hay : ∀ (i : ↥(insert n✝ s)), (fun i ↦ v ↑i) i = ∑ j, a i j • y j
hfa : ∀ (j : Fin l), ∑ i, (fun i ↦ f ↑i) i * a i j = 0
this : v n✝ ∉ 𝔪 • ⊤
n : ↥(insert n✝ s) := ⟨n✝, ⋯⟩
n_def : n = ⟨n✝, ⋯⟩
j : Fin l
hj : IsUnit (a n j)
a' : ι → R := fun i ↦ if hi : i ∈ insert n✝ s then a ⟨i, hi⟩ j else 0
hfv : ∑ x ∈ s, f x • v x + ((-∑ i ∈ s, f i * a' i) * ↑hj.unit⁻¹) • v n✝ = 0
a_eq : ∀ (i : ↥(insert n✝ s)), a i j = a' ↑i
hfn : f ↑n = (-∑ i ∈ s, f i * a' i) * ↑hj.unit⁻¹
c : ι → R := fun i ↦ (-if i = ↑n then 0 else a' i) * ↑hj.unit⁻¹
⊢ ∑ x ∈ s, f x • v x + ∑ x ∈ s, (f x * ((-if x = ↑n then 0 else a' x) * ↑hj.unit⁻¹)) • v ↑n = 0

Tactic:
← s.sum_smul,

Goal state after:
case insert.specialize_2
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : Flat R M
ι : Type u
f : ι → R
n✝ : ι
s : Finset ι
hn : n✝ ∉ s
ih : ∀ (v : ι → M), LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v) → ∑ i ∈ s, f i • v i = 0 → ∀ i ∈ s, f i = 0
v : ι → M
h : LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v)
i : ι
hi : i ∈ insert n✝ s
l : ℕ
a : ↥(insert n✝ s) → Fin l → R
y : Fin l → M
hay : ∀ (i : ↥(insert n✝ s)), (fun i ↦ v ↑i) i = ∑ j, a i j • y j
hfa : ∀ (j : Fin l), ∑ i, (fun i ↦ f ↑i) i * a i j = 0
this : v n✝ ∉ 𝔪 • ⊤
n : ↥(insert n✝ s) := ⟨n✝, ⋯⟩
n_def : n = ⟨n✝, ⋯⟩
j : Fin l
hj : IsUnit (a n j)
a' : ι → R := fun i ↦ if hi : i ∈ insert n✝ s then a ⟨i, hi⟩ j else 0
hfv : ∑ x ∈ s, f x • v x + ((-∑ i ∈ s, f i * a' i) * ↑hj.unit⁻¹) • v n✝ = 0
a_eq : ∀ (i : ↥(insert n✝ s)), a i j = a' ↑i
hfn : f ↑n = (-∑ i ∈ s, f i * a' i) * ↑hj.unit⁻¹
c : ι → R := fun i ↦ (-if i = ↑n then 0 else a' i) * ↑hj.unit⁻¹
⊢ ∑ x ∈ s, f x • v x + (∑ i ∈ s, f i * ((-if i = ↑n then 0 else a' i) * ↑hj.unit⁻¹)) • v ↑n = 0
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

Goal state after:
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 • x ∈ f.range
⊢ b ∈ p
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
hJ : ∃ K, J * K ≠ 0 ∧ Submodule.IsPrincipal (J * K)
⊢ Submodule.IsPrincipal J

Tactic:
let : NormalizedGCDMonoid R := Classical.arbitrary _

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsGCDMonoid R
J : Ideal R
hJ : ∃ K, J * K ≠ 0 ∧ Submodule.IsPrincipal (J * K)
this : NormalizedGCDMonoid R := Classical.arbitrary (NormalizedGCDMonoid R)
⊢ Submodule.IsPrincipal J
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)
T : Finset R
hTK : ↑T ⊆ ↑K
K' : Ideal R := span ↑T
g : R := T.gcd id
hK' : K' ≤ span {g}
y : R
hyJ : y ∈ J
hJK : J * K = R ∙ y * g
hxmemJK : y * g ∈ J * K
hxT : y * g ∈ J * K'
hxJg : y * g ∈ J * span {g}
hx0 : y * g ≠ 0
this : J * span {g} = span {y} * span {g}
⊢ Submodule.IsPrincipal J

Tactic:
span_singleton_mul_left_inj

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)
T : Finset R
hTK : ↑T ⊆ ↑K
K' : Ideal R := span ↑T
g : R := T.gcd id
hK' : K' ≤ span {g}
y : R
hyJ : y ∈ J
hJK : J * K = R ∙ y * g
hxmemJK : y * g ∈ J * K
hxT : y * g ∈ J * K'
hxJg : y * g ∈ J * span {g}
hx0 : y * g ≠ 0
this : J = span {y}
⊢ Submodule.IsPrincipal J

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)
T : Finset R
hTK : ↑T ⊆ ↑K
K' : Ideal R := span ↑T
g : R := T.gcd id
hK' : K' ≤ span {g}
y : R
hyJ : y ∈ J
hJK : J * K = R ∙ y * g
hxmemJK : y * g ∈ J * K
hxT : y * g ∈ J * K'
hxJg : y * g ∈ J * span {g}
hx0 : y * g ≠ 0
this : J * span {g} = span {y} * span {g}
⊢ g ≠ 0
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)
T : Finset R
hTK : ↑T ⊆ ↑K
K' : Ideal R := span ↑T
g : R := T.gcd id
hK' : K' ≤ span {g}
y : R
hyJ : y ∈ J
hJK : J * K = R ∙ y * g
hxmemJK : y * g ∈ J * K
hxT : y * g ∈ J * K'
hxJg : y * g ∈ J * span {g}
hx0 : y * g ≠ 0
this : J * span {g} = span {y} * span {g}
⊢ g ≠ 0

Tactic:
contrapose hx0

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)
T : Finset R
hTK : ↑T ⊆ ↑K
K' : Ideal R := span ↑T
g : R := T.gcd id
hK' : K' ≤ span {g}
y : R
hyJ : y ∈ J
hJK : J * K = R ∙ y * g
hxmemJK : y * g ∈ J * K
hxT : y * g ∈ J * K'
hxJg : y * g ∈ J * span {g}
this : J * span {g} = span {y} * span {g}
hx0 : g = 0
⊢ y * g = 0
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness

Goal state before:
pp: A : Type u
inst✝³ : CommRing A
inst✝² : IsNoetherianRing A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
x✝ : Module.Finite A M
motive : (N : Type v) → [inst : AddCommGroup N] → [inst_1 : Module A N] → [Module.Finite A N] → Prop
subsingleton :
  ∀ (N : Type v) [inst : AddCommGroup N] [inst_1 : Module A N] [inst_2 : Module.Finite A N] [Subsingleton N], motive N
quotient :
  ∀ (N : Type v) [inst : AddCommGroup N] [inst_1 : Module A N] [inst_2 : Module.Finite A N] (p : PrimeSpectrum A)
    (a : N ≃ₗ[A] A ⧸ p.asIdeal), motive N
exact :
  ∀ (N₁ : Type v) [inst : AddCommGroup N₁] [inst_1 : Module A N₁] [inst_2 : Module.Finite A N₁] (N₂ : Type v)
    [inst_3 : AddCommGroup N₂] [inst_4 : Module A N₂] [inst_5 : Module.Finite A N₂] (N₃ : Type v)
    [inst_6 : AddCommGroup N₃] [inst_7 : Module A N₃] [inst_8 : Module.Finite A N₃] (f : N₁ →ₗ[A] N₂) (g : N₂ →ₗ[A] N₃),
    Function.Injective ⇑f → Function.Surjective ⇑g → Function.Exact ⇑f ⇑g → motive N₁ → motive N₃ → motive N₂
equiv :
  ∀ (N₁ : Type v) [inst : AddCommGroup N₁] [inst_1 : Module A N₁] [inst_2 : Module.Finite A N₁] (N₂ : Type v)
    [inst_3 : AddCommGroup N₂] [inst_4 : Module A N₂] [inst_5 : Module.Finite A N₂] (f : N₁ ≃ₗ[A] N₂),
    motive N₁ → motive N₂
s : RelSeries {(N₁, N₂) | N₁.IsQuotientEquivQuotientPrime N₂}
hs1 : s.head = ⊥
hs2 : s.last = ⊤
n : ℕ
h : n < s.length + 1
⊢ motive ↥(s.toFun ⟨n, h⟩)

Tactic:
induction n with

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

Goal state before:
pp: case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I J : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' J' : Ideal R
hI : ↑I = ↑I'
hJ : ↑J = ↑J'
x y : R
hx : x ≠ 0
hy : y ≠ 0
h : Ideal.span {x} * I' = Ideal.span {y} * J'
this : IsUnit (mk' (FractionRing R) x ⟨y, ⋯⟩)
⊢ ∃ x, I * (toPrincipalIdeal R (FractionRing R)) x = J

Tactic:
refine ⟨this.unit, ?_⟩

Goal state after:
case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I J : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' J' : Ideal R
hI : ↑I = ↑I'
hJ : ↑J = ↑J'
x y : R
hx : x ≠ 0
hy : y ≠ 0
h : Ideal.span {x} * I' = Ideal.span {y} * J'
this : IsUnit (mk' (FractionRing R) x ⟨y, ⋯⟩)
⊢ I * (toPrincipalIdeal R (FractionRing R)) this.unit = J
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: G : Type u_1
inst✝ : Group G
n : ℕ
⊢ (derivedSeries G n).Normal

Tactic:
induction n with

Goal state after:
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
n : ℕ
⊢ (derivedSeries G n).Characteristic

Tactic:
induction n with

Goal state after:
Module: Mathlib.GroupTheory.Solvable

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

Tactic:
induction n with

Goal state after:
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ⇑f
n : ℕ
⊢ derivedSeries G' n ≤ map f (derivedSeries G n)

Tactic:
induction n with

Goal state after:
Module: Mathlib.GroupTheory.Solvable

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

Tactic:
induction n with

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 : ℕ
⊢ map H.subtype (derivedSeries (↥H) (n + 1)) = map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) n)

Tactic:
induction n with

Goal state after:
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : IsSimpleGroup G
n : ℕ
⊢ derivedSeries G n.succ = _root_.commutator G

Tactic:
induction n with

Goal state after:
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: x : Perm (Fin 5) := { toFun := ![1, 2, 0, 3, 4], invFun := ![2, 0, 1, 3, 4], left_inv := ⋯, right_inv := ⋯ }
y : Perm (Fin 5) := { toFun := ![3, 4, 2, 0, 1], invFun := ![3, 4, 2, 0, 1], left_inv := ⋯, right_inv := ⋯ }
z : Perm (Fin 5) := { toFun := ![0, 3, 2, 1, 4], invFun := ![0, 3, 2, 1, 4], left_inv := ⋯, right_inv := ⋯ }
key : x = z * ⁅x, y * x * y⁻¹⁆ * z⁻¹
n : ℕ
⊢ x ∈ derivedSeries (Perm (Fin 5)) n

Tactic:
induction n with

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus

Goal state before:
pp: R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Flat R M
inst✝ : Module.Finite R M
p : PrimeSpectrum R
h : rankAtStalk M p = 0
⊢ Module.rank (Localization.AtPrime p.asIdeal) (LocalizedModule p.asIdeal.primeCompl M) = 0

Tactic:
dsimp [rankAtStalk] at h

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
p : PrimeSpectrum R
h : finrank (Localization.AtPrime p.asIdeal) (LocalizedModule p.asIdeal.primeCompl M) = 0
⊢ Module.rank (Localization.AtPrime p.asIdeal) (LocalizedModule p.asIdeal.primeCompl M) = 0
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
h : Function.Injective ⇑(LinearMap.lTensor M f)
⊢ Function.Injective ⇑f

Tactic:
← leftCancelEquiv_comp_lTensor_comp_symm (linearEquiv R M) f

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
h : Function.Injective ⇑(LinearMap.lTensor M f)
⊢ Function.Injective
    ⇑(↑(leftCancelEquiv P (linearEquiv R M)) ∘ₗ
        LinearMap.lTensor (Dual R M) (LinearMap.lTensor M f) ∘ₗ ↑(leftCancelEquiv N (linearEquiv R M)).symm)
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
h : Function.Surjective ⇑(LinearMap.lTensor M f)
⊢ Function.Surjective ⇑f

Tactic:
← leftCancelEquiv_comp_lTensor_comp_symm (linearEquiv R M) f

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
h : Function.Surjective ⇑(LinearMap.lTensor M f)
⊢ Function.Surjective
    ⇑(↑(leftCancelEquiv P (linearEquiv R M)) ∘ₗ
        LinearMap.lTensor (Dual R M) (LinearMap.lTensor M f) ∘ₗ ↑(leftCancelEquiv N (linearEquiv R M)).symm)
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
⊢ normalClosure F K ↥(normalClosure F K L) = ⊤

Tactic:
simp_rw [normalClosure, ← top_le_iff]

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
⊢ ⊤ ≤ ⨆ f, f.fieldRange
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 ∈ ⇑(⨆ f, f.fieldRange).val '' ↑(⨆ f, f.fieldRange)

Tactic:
coe_val,

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 ∈ ⊤
⊢ ↑x ∈ Subtype.val '' ↑(⨆ f, f.fieldRange)
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: case refine_2
R : Type u
M : Type v
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Invertible R M
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] LocalizedModule P.primeCompl M :=
  fun P [P.IsMaximal] ↦ LocalizedModule.mkLinearMap P.primeCompl M
ff : (P : Ideal R) →
  [inst : P.IsMaximal] → M ⊗[R] M →ₗ[R] LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M :=
  fun P [P.IsMaximal] ↦ map (f P) (f P)
P : Ideal R
x✝ : P.IsMaximal
⊢ ↑(TensorProduct.comm R (LocalizedModule P.primeCompl M) (LocalizedModule P.primeCompl M)) =
    (IsLocalizedModule.map P.primeCompl (ff P) (ff P)) ↑(LinearEquiv.refl R (M ⊗[R] M))

Tactic:
let Rp := Localization P.primeCompl

Goal state after:
case refine_2
R : Type u
M : Type v
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Invertible R M
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] LocalizedModule P.primeCompl M :=
  fun P [P.IsMaximal] ↦ LocalizedModule.mkLinearMap P.primeCompl M
ff : (P : Ideal R) →
  [inst : P.IsMaximal] → M ⊗[R] M →ₗ[R] LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M :=
  fun P [P.IsMaximal] ↦ map (f P) (f P)
P : Ideal R
x✝ : P.IsMaximal
Rp : Type u := Localization P.primeCompl
⊢ ↑(TensorProduct.comm R (LocalizedModule P.primeCompl M) (LocalizedModule P.primeCompl M)) =
    (IsLocalizedModule.map P.primeCompl (ff P) (ff P)) ↑(LinearEquiv.refl R (M ⊗[R] M))
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: case refine_1
α : Type u_1
M : Matroid α
B : Set α
hB : B ⊆ M.E
h : M.IsBase (M.E \ B)
I : Set α
hI : I ⊆ M.E
B' : Set α
x✝ : M.IsBase B' ∧ Disjoint I B'
hBI : B ⊆ I
hB' : M.IsBase B'
hIB' : Disjoint I B'
⊢ B' ⊆ M.E \ B

Tactic:
subset_sdiff,

Goal state after:
case refine_1
α : Type u_1
M : Matroid α
B : Set α
hB : B ⊆ M.E
h : M.IsBase (M.E \ B)
I : Set α
hI : I ⊆ M.E
B' : Set α
x✝ : M.IsBase B' ∧ Disjoint I B'
hBI : B ⊆ I
hB' : M.IsBase B'
hIB' : Disjoint I B'
⊢ B' ⊆ M.E ∧ Disjoint B' B
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
h : ∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → I = J
⊢ M.IsBase I

Tactic:
rwa [isBase_iff_maximal_indep, maximal_subset_iff, and_iff_right hI]

Goal state after:
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
⊢ FiniteDimensional F E

Tactic:
let IF := { K : IntermediateField F E // ∃ x, K = F⟮x⟯ }

Goal state after:
F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
IF : Type (max 0 u_2) := { K // ∃ x, K = F⟮x⟯ }
⊢ FiniteDimensional F E
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
B I X : Set α
hB : M.IsBase B
hBX : B ⊆ X
hIX : M.IsBasis I X
⊢ M.IsBase I

Tactic:
by
  by_contra h
  obtain ⟨e, heBI, he⟩ := hIX.indep.exists_insert_of_not_isBase h hB
  exact heBI.2 (hIX.mem_of_insert_indep (hBX heBI.1) he)

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M✝ : Matroid α
R✝ I✝ X Y : Set α
M : Matroid α
R I : Set α
hI : M.Indep I
hIY : I ⊆ R
hIn : ¬M.IsBasis I (R ∩ M.E)
B' : Set α
hB' : M.IsBase B'
hI' : M✶.IsBasis (M.E \ (B' ∪ R ∩ M.E)) (M.E \ (R ∩ M.E))
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
hBIB' : B ⊆ I ∪ B'
⊢ B ⊆ B' ∪ R ∩ M.E ∧ R ∩ M.E ⊆ B' ∪ R ∩ M.E

Tactic:
and_iff_left subset_union_right,

Goal state after:
α : Type u_1
M✝ : Matroid α
R✝ I✝ X Y : Set α
M : Matroid α
R I : Set α
hI : M.Indep I
hIY : I ⊆ R
hIn : ¬M.IsBasis I (R ∩ M.E)
B' : Set α
hB' : M.IsBase B'
hI' : M✶.IsBasis (M.E \ (B' ∪ R ∩ M.E)) (M.E \ (R ∩ M.E))
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
hBIB' : B ⊆ I ∪ B'
⊢ B ⊆ B' ∪ R ∩ M.E
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: case refine_1
α : Type u_1
M✝ : Matroid α
I B✝ X✝ : Set α
M : Matroid α
X I' : Set α
hI'E : I' ⊆ M.E
B : Set α
hB : M.IsBase B
hI'B : Disjoint I' B
hI'X : I' ⊆ X
B' : Set α
hB' : M.IsBase B'
hI : M.IsBasis (B' \ X) (M.E \ X)
hIB' : B' \ X ⊆ B'
hB'IB : B' ⊆ B' \ X ∪ B
⊢ I' ⊆ X \ B'

Tactic:
subset_sdiff,

Goal state after:
case refine_1
α : Type u_1
M✝ : Matroid α
I B✝ X✝ : Set α
M : Matroid α
X I' : Set α
hI'E : I' ⊆ M.E
B : Set α
hB : M.IsBase B
hI'B : Disjoint I' B
hI'X : I' ⊆ X
B' : Set α
hB' : M.IsBase B'
hI : M.IsBasis (B' \ X) (M.E \ X)
hIB' : B' \ X ⊆ B'
hB'IB : B' ⊆ B' \ X ∪ B
⊢ I' ⊆ X ∧ Disjoint I' B'
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
R✝ I X Y : Set α
inst✝ : M.Finitary
R : Set α
⊢ (M ↾ R).Finitary

Tactic:
by
  refine ⟨fun I hI ↦ ?_⟩
  simp only [restrict_indep_iff] at *
  rw [indep_iff_forall_finite_subset_indep]
  exact ⟨fun J hJ hJfin ↦ (hI J hJ hJfin).1,
    fun e heI ↦ singleton_subset_iff.1 (hI _ (by simpa) (toFinite _)).2⟩

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

Goal state before:
pp: α : Type u_1
E B I : Set α
hIE : I ⊆ E
⊢ (freeOn I ↾ E).IsBase B ↔ B = I

Tactic:
isBase_restrict_iff',

Goal state after:
α : Type u_1
E B I : Set α
hIE : I ⊆ E
⊢ (freeOn I).IsBasis' B E ↔ B = I
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
E I : Set α
hI : I.Finite
⊢ (uniqueBaseOn (I ∩ E) E).RankFinite

Tactic:
refine ⟨I ∩ E, ?_⟩

Goal state after:
α : Type u_1
E I : Set α
hI : I.Finite
⊢ (uniqueBaseOn (I ∩ E) E).IsBase (I ∩ E) ∧ (I ∩ E).Finite