mathlib-initiative/mathlib-tactics huggingface dataset:
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
na nb nc : ℕ
a : ⨂[R]^na M
b : ⨂[R]^nb M
c : ⨂[R]^nc M
mul : (n m : ℕ) → ⨂[R]^n M →ₗ[R] ⨂[R]^m M →ₗ[R] ⨂[R]^(n + m) M :=
  fun n m ↦ (TensorProduct.mk R (⨂[R]^n M) (⨂[R]^m M)).compr₂ ↑mulEquiv
e : ⨂[R]^(na + nb + nc) M ≃ₗ[R] ⨂[R]^(na + (nb + nc)) M := cast R M ⋯
lhs : ⨂[R]^na M →ₗ[R] ⨂[R]^nb M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M :=
  (LinearMap.llcomp R (⨂[R]^nb M) (⨂[R]^(na + nb) M) (⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M))
      ((mul (na + nb) nc).compr₂ ↑e) ∘ₗ
    mul na nb
lhs_eq :
  ∀ (a : ⨂[R]^na M) (b : ⨂[R]^nb M) (c : ⨂[R]^nc M),
    ((lhs a) b) c = e (GradedMonoid.GMul.mul (GradedMonoid.GMul.mul a b) c)
rhs : ⨂[R]^na M →ₗ[R] ⨂[R]^nb M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M :=
  (((LinearMap.llcomp R (⨂[R]^nb M) (⨂[R]^nc M →ₗ[R] ⨂[R]^na M →ₗ[R] ⨂[R]^(na + (nb + nc)) M)
          (⨂[R]^na M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M))
        ↑LinearMap.lflip)
      ((LinearMap.llcomp R (⨂[R]^nc M) (⨂[R]^(nb + nc) M) (⨂[R]^na M →ₗ[R] ⨂[R]^(na + (nb + nc)) M))
          (mul na (nb + nc)).flip ∘ₗ
        mul nb nc)).flip
rhs_eq :
  ∀ (a : ⨂[R]^na M) (b : ⨂[R]^nb M) (c : ⨂[R]^nc M), ((rhs a) b) c = GradedMonoid.GMul.mul a (GradedMonoid.GMul.mul b c)
⊢ lhs = rhs

Tactic:
ext a b c

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
na nb nc : ℕ
a✝ : ⨂[R]^na M
b✝ : ⨂[R]^nb M
c✝ : ⨂[R]^nc M
mul : (n m : ℕ) → ⨂[R]^n M →ₗ[R] ⨂[R]^m M →ₗ[R] ⨂[R]^(n + m) M :=
  fun n m ↦ (TensorProduct.mk R (⨂[R]^n M) (⨂[R]^m M)).compr₂ ↑mulEquiv
e : ⨂[R]^(na + nb + nc) M ≃ₗ[R] ⨂[R]^(na + (nb + nc)) M := cast R M ⋯
lhs : ⨂[R]^na M →ₗ[R] ⨂[R]^nb M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M :=
  (LinearMap.llcomp R (⨂[R]^nb M) (⨂[R]^(na + nb) M) (⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M))
      ((mul (na + nb) nc).compr₂ ↑e) ∘ₗ
    mul na nb
lhs_eq :
  ∀ (a : ⨂[R]^na M) (b : ⨂[R]^nb M) (c : ⨂[R]^nc M),
    ((lhs a) b) c = e (GradedMonoid.GMul.mul (GradedMonoid.GMul.mul a b) c)
rhs : ⨂[R]^na M →ₗ[R] ⨂[R]^nb M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M :=
  (((LinearMap.llcomp R (⨂[R]^nb M) (⨂[R]^nc M →ₗ[R] ⨂[R]^na M →ₗ[R] ⨂[R]^(na + (nb + nc)) M)
          (⨂[R]^na M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M))
        ↑LinearMap.lflip)
      ((LinearMap.llcomp R (⨂[R]^nc M) (⨂[R]^(nb + nc) M) (⨂[R]^na M →ₗ[R] ⨂[R]^(na + (nb + nc)) M))
          (mul na (nb + nc)).flip ∘ₗ
        mul nb nc)).flip
rhs_eq :
  ∀ (a : ⨂[R]^na M) (b : ⨂[R]^nb M) (c : ⨂[R]^nc M), ((rhs a) b) c = GradedMonoid.GMul.mul a (GradedMonoid.GMul.mul b c)
a : Fin na → M
b : Fin nb → M
c : Fin nc → M
⊢ (((((lhs.compMultilinearMap (tprod R)) a).compMultilinearMap (tprod R)) b).compMultilinearMap (tprod R)) c =
    (((((rhs.compMultilinearMap (tprod R)) a).compMultilinearMap (tprod R)) b).compMultilinearMap (tprod R)) c
Module: Mathlib.LinearAlgebra.LinearDisjoint

Goal state before:
pp: case inr
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
κ : Type u_1
ι : Type u_2
m : κ → ↥M
n : ι → ↥N
hm : LinearIndependent R m
hn : LinearIndependent R n
h✝ : Flat R ↥N
⊢ LinearIndependent R fun i ↦ ↑(m i.1) * ↑(n i.2)

Tactic:
· exact H.linearIndependent_mul_of_flat_right hm hn

Goal state after:
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ : MultilinearMap R s E
f : (i : ι) → s i
⊢ 0 • φ f = 0

Tactic:
zero_smul

Goal state after:
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝⁴ : CommSemiring R
s : ι → Type u_7
inst✝³ : (i : ι) → AddCommMonoid (s i)
inst✝² : (i : ι) → Module R (s i)
t : ι → Type u_11
inst✝¹ : (i : ι) → AddCommMonoid (t i)
inst✝ : (i : ι) → Module R (t i)
f : (i : ι) → s i ≃ₗ[R] t i
p : (i : ι) → t i
⊢ (congr f).symm ((tprod R) p) = ⨂ₜ[R] (i : ι), (f i).symm (p i)

Tactic:
simp only [congr, LinearEquiv.symm_ofLinearMap, LinearEquiv.coe_ofLinearMap, map_tprod,
    LinearEquiv.coe_coe]

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

Goal state before:
pp: case insert.inl
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 : ∀ i ∈ s, f i = 0
v : ι → M
h : LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v)
hfv : ∑ i, f ↑i • v ↑i = 0
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
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⁻¹
hi : i = n✝
⊢ f i = 0

Tactic:
rw [hi, hfn, Finset.sum_eq_zero, neg_zero, zero_mul]

Goal state after:
case insert.inl
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 : ∀ i ∈ s, f i = 0
v : ι → M
h : LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v)
hfv : ∑ i, f ↑i • v ↑i = 0
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
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⁻¹
hi : i = n✝
⊢ ∀ x ∈ s, f x * a' x = 0
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness

Goal state before:
pp: case refine_1
A : Type u
inst✝² : CommRing A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
N₁ N₂ : Submodule A M
f : ↥N₂ ⧸ N₁.submoduleOf N₂ →ₗ[A] M ⧸ N₁ := (N₁.submoduleOf N₂).mapQ N₁ N₂.subtype ⋯
hf₁ : f.ker = ⊥
hf₂ : f.range = map N₁.mkQ N₂
x✝ : N₁.IsQuotientEquivQuotientPrime N₂
h : N₁ ≤ N₂
p : PrimeSpectrum A
e : (↥N₂ ⧸ N₁.submoduleOf N₂) ≃ₗ[A] A ⧸ p.asIdeal
x : M
hx : x ∈ N₂
hx' : (N₁.submoduleOf N₂).mkQ ⟨x, hx⟩ = e.symm 1
⊢ ∃ x, (⊥.colon {N₁.mkQ x}).IsPrime ∧ N₂ = N₁ ⊔ A ∙ x

Tactic:
have hx'' : N₁.mkQ x = f (e.symm 1) := by simp [f, ← hx']

Goal state after:
case refine_1
A : Type u
inst✝² : CommRing A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
N₁ N₂ : Submodule A M
f : ↥N₂ ⧸ N₁.submoduleOf N₂ →ₗ[A] M ⧸ N₁ := (N₁.submoduleOf N₂).mapQ N₁ N₂.subtype ⋯
hf₁ : f.ker = ⊥
hf₂ : f.range = map N₁.mkQ N₂
x✝ : N₁.IsQuotientEquivQuotientPrime N₂
h : N₁ ≤ N₂
p : PrimeSpectrum A
e : (↥N₂ ⧸ N₁.submoduleOf N₂) ≃ₗ[A] A ⧸ p.asIdeal
x : M
hx : x ∈ N₂
hx' : (N₁.submoduleOf N₂).mkQ ⟨x, hx⟩ = e.symm 1
hx'' : N₁.mkQ x = f (e.symm 1)
⊢ ∃ x, (⊥.colon {N₁.mkQ x}).IsPrime ∧ N₂ = N₁ ⊔ A ∙ x
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness

Goal state before:
pp: case refine_1
A : Type u
inst✝² : CommRing A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
N₁ N₂ : Submodule A M
f : ↥N₂ ⧸ N₁.submoduleOf N₂ →ₗ[A] M ⧸ N₁ := (N₁.submoduleOf N₂).mapQ N₁ N₂.subtype ⋯
hf₁ : f.ker = ⊥
hf₂ : f.range = map N₁.mkQ N₂
x✝ : N₁.IsQuotientEquivQuotientPrime N₂
h : N₁ ≤ N₂
p : PrimeSpectrum A
e : (↥N₂ ⧸ N₁.submoduleOf N₂) ≃ₗ[A] A ⧸ p.asIdeal
⊢ ∃ x, (⊥.colon {N₁.mkQ x}).IsPrime ∧ N₂ = N₁ ⊔ A ∙ x

pp: case refine_2
A : Type u
inst✝² : CommRing A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
N₁ N₂ : Submodule A M
f : ↥N₂ ⧸ N₁.submoduleOf N₂ →ₗ[A] M ⧸ N₁ := (N₁.submoduleOf N₂).mapQ N₁ N₂.subtype ⋯
hf₁ : f.ker = ⊥
hf₂ : f.range = map N₁.mkQ N₂
x✝ : ∃ x, (⊥.colon {N₁.mkQ x}).IsPrime ∧ N₂ = N₁ ⊔ A ∙ x
x : M
hx : (⊥.colon {N₁.mkQ x}).IsPrime
hx' : N₂ = N₁ ⊔ A ∙ x
⊢ Nonempty ((↥N₂ ⧸ N₁.submoduleOf N₂) ≃ₗ[A] A ⧸ { asIdeal := ⊥.colon {N₁.mkQ x}, isPrime := hx }.asIdeal)

Tactic:
· obtain ⟨⟨x, hx⟩, hx'⟩ := Submodule.mkQ_surjective _ (e.symm 1)
    have hx'' : N₁.mkQ x = f (e.symm 1) := by simp [f, ← hx']
    refine ⟨x, ?_, ?_⟩
    · convert! p.2
      ext r
      simp [hx'', ← map_smul, Algebra.smul_def, show f _ = 0 ↔ _ from congr(_ ∈ $hf₁),
        Ideal.Quotient.eq_zero_iff_mem]
    · refine le_antisymm ?_ (sup_le h ((span_singleton_le_iff_mem _ _).mpr hx))
      have : (span A {x}).map N₁.mkQ = ((span A {1}).map e.symm.toLinearMap).map f := by
        simp only [map_span, Set.image_singleton, hx'', LinearEquiv.coe_coe]
      rw [← N₁.ker_mkQ, sup_comm, ← comap_map_eq, ← map_le_iff_le_comap, this]
      simp [hf₂, Ideal.Quotient.span_singleton_one]

Goal state after:
case refine_2
A : Type u
inst✝² : CommRing A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
N₁ N₂ : Submodule A M
f : ↥N₂ ⧸ N₁.submoduleOf N₂ →ₗ[A] M ⧸ N₁ := (N₁.submoduleOf N₂).mapQ N₁ N₂.subtype ⋯
hf₁ : f.ker = ⊥
hf₂ : f.range = map N₁.mkQ N₂
x✝ : ∃ x, (⊥.colon {N₁.mkQ x}).IsPrime ∧ N₂ = N₁ ⊔ A ∙ x
x : M
hx : (⊥.colon {N₁.mkQ x}).IsPrime
hx' : N₂ = N₁ ⊔ A ∙ x
⊢ Nonempty ((↥N₂ ⧸ N₁.submoduleOf N₂) ≃ₗ[A] A ⧸ { asIdeal := ⊥.colon {N₁.mkQ x}, isPrime := hx }.asIdeal)
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
p : PrimeSpectrum R
⊢ rankAtStalk M p = finrank (Localization.AtPrime p.asIdeal) (Localization.AtPrime p.asIdeal ⊗[R] M)

Tactic:
let e : LocalizedModule p.asIdeal.primeCompl M ≃ₗ[Localization.AtPrime p.asIdeal]
      Localization.AtPrime p.asIdeal ⊗[R] M :=
    LocalizedModule.equivTensorProduct p.asIdeal.primeCompl M

Goal state after:
R : Type uR
M : Type uM
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : PrimeSpectrum R
e : LocalizedModule p.asIdeal.primeCompl M ≃ₗ[Localization.AtPrime p.asIdeal] Localization.AtPrime p.asIdeal ⊗[R] M :=
  equivTensorProduct p.asIdeal.primeCompl M
⊢ rankAtStalk M p = finrank (Localization.AtPrime p.asIdeal) (Localization.AtPrime p.asIdeal ⊗[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
inst✝³ : Module.Invertible R M
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : Module.Invertible R A
inv : A →ₗ[R] R :=
  ↑(linearEquiv R A) ∘ₗ LinearMap.lTensor (Dual R A) (LinearMap.mul' R A) ∘ₗ ↑(leftCancelEquiv A (linearEquiv R A)).symm
s : Finset (Dual R A × A)
hs : (linearEquiv R A).symm 1 = ∑ i ∈ s, i.1 ⊗ₜ[R] i.2
⊢ (inv ∘ₗ Algebra.linearMap R A) 1 = LinearMap.id 1

Tactic:
simp [inv, hs, sum_tmul, map_sum, ← (LinearEquiv.symm_apply_eq _).1 hs]

Goal state after:
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: case h.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:
rintro x (rfl | rfl) <;> assumption

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

Goal state before:
pp: 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 ≤ normalClosure F (↥K₂) L

Tactic:
exact normalClosure_mono K₁ K₂ h

Goal state after:
Module: Mathlib.RingTheory.AlgebraicIndependent.Defs

Goal state before:
pp: R : Type u_3
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set A
⊢ (AlgebraicIndependent R Subtype.val ∧
      ∀ (s_1 : Set A), AlgebraicIndepOn R _root_.id s_1 → range Subtype.val ⊆ s_1 → range Subtype.val = s_1) ↔
    Maximal (AlgebraicIndepOn R _root_.id) s

Tactic:
maximal_iff,

Goal state after:
R : Type u_3
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set A
⊢ (AlgebraicIndependent R Subtype.val ∧
      ∀ (s_1 : Set A), AlgebraicIndepOn R _root_.id s_1 → range Subtype.val ⊆ s_1 → range Subtype.val = s_1) ↔
    AlgebraicIndepOn R _root_.id s ∧ ∀ ⦃y : Set A⦄, AlgebraicIndepOn R _root_.id y → s ⊆ y → s = y
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) ↔ Maximal (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) B

Tactic:
maximal_iff,

Goal state after:
α : 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
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: case h.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 • β⟯
αxβ_in_K : α + x • β ∈ F⟮α + x • β⟯
αyβ_in_K : α + y • β ∈ F⟮α + x • β⟯
β_in_K : β ∈ F⟮α + x • β⟯
α_in_K : α ∈ F⟮α + x • β⟯
⊢ {α, β} ⊆ ↑F⟮α + x • β⟯

Tactic:
rintro x (rfl | rfl) <;> assumption

Goal state after:
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
A : Type u_4
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
I : (Submodule R A)ˣ
T T' : Finset A
hT : ↑T ⊆ ↑↑I⁻¹
hT' : ↑T' ⊆ ↑↑I
S : Finset A := Finset.image₂ (fun x1 x2 ↦ x1 * x2) T T'
r : A → R
hr : Function.support r ⊆ ↑S ∧ ∑ a ∈ S, r a • a = 1
a : ↥S → A
ha : ∀ (i : ↥S), a i ∈ T
b : ↥S → A
hb : ∀ (i : ↥S), b i ∈ T'
eq✝ : ∀ (i : ↥S), a i * b i = ↑i
f : ↥↑I →ₗ[R] ↥S → R :=
  LinearMap.pi fun i ↦
    ↑(LinearEquiv.ofInjective (Algebra.linearMap R A) ⋯).symm ∘ₗ (LinearMap.mulRight R (r ↑i • a i)).restrict ⋯
hf : ∀ (x : ↥↑I) (i : ↥S), (algebraMap R A) (f x i) = ↑x * r ↑i • a i
g : (↥S → R) →ₗ[R] ↥↑I := (lsum R (fun a ↦ R) ℕ) fun i ↦ toSpanSingleton R ↥↑I ⟨b i, ⋯⟩
hgf : g ∘ₗ f = LinearMap.id
m : A ⊗[R] ↥↑I →ₗ[R] A := mul' R A ∘ₗ lTensor A (↑I).subtype
eq : ↑(piScalarRight R R A ↥S) ∘ₗ lTensor A f = (LinearMap.pi fun i ↦ LinearMap.mulRight R (r ↑i • a i)) ∘ₗ m
⊢ lTensor A (g ∘ₗ f) = LinearMap.id

Tactic:
hgf,

Goal state after:
R : Type u
A : Type u_4
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
I : (Submodule R A)ˣ
T T' : Finset A
hT : ↑T ⊆ ↑↑I⁻¹
hT' : ↑T' ⊆ ↑↑I
S : Finset A := Finset.image₂ (fun x1 x2 ↦ x1 * x2) T T'
r : A → R
hr : Function.support r ⊆ ↑S ∧ ∑ a ∈ S, r a • a = 1
a : ↥S → A
ha : ∀ (i : ↥S), a i ∈ T
b : ↥S → A
hb : ∀ (i : ↥S), b i ∈ T'
eq✝ : ∀ (i : ↥S), a i * b i = ↑i
f : ↥↑I →ₗ[R] ↥S → R :=
  LinearMap.pi fun i ↦
    ↑(LinearEquiv.ofInjective (Algebra.linearMap R A) ⋯).symm ∘ₗ (LinearMap.mulRight R (r ↑i • a i)).restrict ⋯
hf : ∀ (x : ↥↑I) (i : ↥S), (algebraMap R A) (f x i) = ↑x * r ↑i • a i
g : (↥S → R) →ₗ[R] ↥↑I := (lsum R (fun a ↦ R) ℕ) fun i ↦ toSpanSingleton R ↥↑I ⟨b i, ⋯⟩
hgf : g ∘ₗ f = LinearMap.id
m : A ⊗[R] ↥↑I →ₗ[R] A := mul' R A ∘ₗ lTensor A (↑I).subtype
eq : ↑(piScalarRight R R A ↥S) ∘ₗ lTensor A f = (LinearMap.pi fun i ↦ LinearMap.mulRight R (r ↑i • a i)) ∘ₗ m
⊢ lTensor A LinearMap.id = LinearMap.id
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'
f : α
hf : f ∈ B' \ B
h : B \ B' = {f}
hb : M.IsBase (insert f (B \ {f}))
⊢ False

Tactic:
exact hf.2 (h.symm.subset (mem_singleton f)).1

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

Goal state before:
pp: 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}))

Tactic:
rw [h, encard_singleton, encard_eq_one] at hcard

Goal state after:
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 : ∃ x, B' \ B = {x}
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 J X Y : Set α
hIX : M.IsBasis I X
hJY : M.IsBasis J Y
h : M.Indep (I ∪ J)
⊢ M.IsBasis (I ∪ J) (X ∪ Y)

Tactic:
by
  rw [union_eq_iUnion, union_eq_iUnion]
  refine IsBasis.iUnion_isBasis_iUnion _ _ ?_ ?_
  · simp only [Bool.forall_bool, cond_false, cond_true]; exact ⟨hJY, hIX⟩
  rwa [← union_eq_iUnion]

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

Goal state before:
pp: α : Type u_1
E : Set α
hE : E.Finite
f : Matroid α → Set α × Set (Set α) := fun M ↦ (M.E, {B | M.IsBase B})
M M' : Matroid α
hMM' : M.E = M'.E ∧ ∀ (x : Set α), x ∈ {B | M.IsBase B} ↔ x ∈ {B | M'.IsBase B}
⊢ M = M'

Tactic:
exact ext_isBase hMM'.1 (fun B _ ↦ hMM'.2 B)

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

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

Tactic:
maximal_iff,

Goal state after:
α : Type u_1
M : Matroid α
I X : Set α
hX : X ⊆ M.E
⊢ ((M ↾ X).Indep I ∧ ∀ ⦃y : Set α⦄, (M ↾ X).Indep y → I ⊆ y → I = y) ↔
    (M.Indep I ∧ I ⊆ X) ∧ ∀ ⦃y : Set α⦄, M.Indep y ∧ y ⊆ X → I ⊆ y → I = y
Module: Mathlib.Combinatorics.Matroid.IndepAxioms

Goal state before:
pp: case neg
α : 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
hcard : (insert e I₀).ncard ≤ J.ncard
⊢ False

Tactic:
rw [ncard_insert_of_notMem heI₀ hI₀fin, ← Nat.lt_iff_add_one_le] at hcard

Goal state after:
case neg
α : 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
hcard : I₀.ncard < J.ncard
⊢ False
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

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

Tactic:
maximal_iff,

Goal state after:
α : Type u_1
M : Matroid α
I X : Set α
⊢ ((M ↾ X).Indep I ∧ ∀ ⦃y : Set α⦄, (M ↾ X).Indep y → I ⊆ y → I = y) ↔
    (M.Indep I ∧ I ⊆ X) ∧ ∀ ⦃y : Set α⦄, M.Indep y ∧ y ⊆ X → I ⊆ y → I = y
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
R I X : Set α
⊢ Maximal (fun A ↦ (M ↾ R).Indep A ∧ A ⊆ X) I ↔ Maximal (fun A ↦ M.Indep A ∧ A ⊆ X ∩ R) I ∧ I ⊆ R

Tactic:
maximal_iff,

Goal state after:
α : Type u_1
M : Matroid α
R I X : Set α
⊢ (((M ↾ R).Indep I ∧ I ⊆ X) ∧ ∀ ⦃y : Set α⦄, (M ↾ R).Indep y ∧ y ⊆ X → I ⊆ y → I = y) ↔
    ((M.Indep I ∧ I ⊆ X ∩ R) ∧ ∀ ⦃y : Set α⦄, M.Indep y ∧ y ⊆ X ∩ R → I ⊆ y → I = y) ∧ I ⊆ R
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
tfae_1_iff_2 : M.IsLoop e ↔ e ∈ M.closure ∅
tfae_2_iff_3 : e ∈ M.closure ∅ ↔ M.IsCircuit {e}
tfae_2_iff_4 : e ∈ M.closure ∅ ↔ M.Dep {e}
h : (∀ (x : Set α), M.IsBase x → e ∈ M.E) ∧ ∀ (x : Set α), M.IsBase x → e ∉ x
hi : M.Indep {e}
B : Set α
hB : M.IsBase B
heB : {e} ⊆ B
⊢ e ∈ B

Tactic:
by simpa using heB

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

Goal state before:
pp: α : Type u_1
M : Matroid α
h : M.eRank = 0
B : Set α
hB : M.IsBase B
⊢ M.closure ∅ = M.E

Tactic:
rw [← hB.encard_eq_eRank, encard_eq_zero] at h

Goal state after:
α : Type u_1
M : Matroid α
B : Set α
h : B = ∅
hB : M.IsBase B
⊢ M.closure ∅ = M.E
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ M.Indep M.coloops

Tactic:
rw [← empty_union M.coloops, union_coloops_indep_iff]

Goal state after:
α : Type u_1
M : Matroid α
⊢ M.Indep ∅
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
he : e ∈ M.E
⊢ e ∉ M.closure I ↔ M.Indep (insert e I) ∧ e ∉ I

Tactic:
rw [hI.mem_closure_iff, dep_iff, insert_subset_iff, and_iff_right he,
    and_iff_left hI.subset_ground]; tauto

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M✝ N : Matroid α
e f : α
F X C I : Set α
M : Matroid α
⊢ M.removeLoops.Loopless

Tactic:
simp [loopless_iff_forall_isNonloop, removeLoops]

Goal state after: