mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
⊢ derivativeFinsupp (map f p) = Finsupp.mapRange (fun x ↦ map f x) ⋯ (derivativeFinsupp p)

Tactic:
ext i : 1

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
i : ℕ
⊢ (derivativeFinsupp (map f p)) i = (Finsupp.mapRange (fun x ↦ map f x) ⋯ (derivativeFinsupp p)) i
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ derivativeFinsupp (derivative p) = Finsupp.comapDomain Nat.succ (derivativeFinsupp p) ⋯

Tactic:
ext i : 1

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
⊢ (derivativeFinsupp (derivative p)) i = (Finsupp.comapDomain Nat.succ (derivativeFinsupp p) ⋯) i
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case inr
R : Type u
inst✝¹ : Semiring R
p : R[X]
inst✝ : IsAddTorsionFree R
hp : derivative p = 0
hp' : p ≠ 0
f_nat_degree_pos : 0 < p.natDegree
m : ℕ := p.natDegree - 1
hm : m + 1 = p.natDegree
⊢ False

Tactic:
have h2 := coeff_derivative p m

Goal state after:
case inr
R : Type u
inst✝¹ : Semiring R
p : R[X]
inst✝ : IsAddTorsionFree R
hp : derivative p = 0
hp' : p ≠ 0
f_nat_degree_pos : 0 < p.natDegree
m : ℕ := p.natDegree - 1
hm : m + 1 = p.natDegree
h2 : (derivative p).coeff m = p.coeff (m + 1) * (↑m + 1)
⊢ False
Module: Mathlib.Order.Filter.CountablyGenerated

Goal state before:
pp: case a
α : Type u_1
s : ℕ → Set α
i : ℕ
⊢ ⨅ i, 𝓟 (⋂ m, ⋂ (_ : m ≤ i), s m) ≤ 𝓟 (s i)

Tactic:
refine iInf_le_of_le i (principal_mono.2 <| iInter₂_subset i ?_)

Goal state after:
case a
α : Type u_1
s : ℕ → Set α
i : ℕ
⊢ i ≤ i
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
n : ℕ
⊢ rootMultiplicity a p ≤ n ↔ ¬(X - C a) ^ (n + 1) ∣ p

Tactic:
← (le_rootMultiplicity_iff p0).not,

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
n : ℕ
⊢ rootMultiplicity a p ≤ n ↔ ¬n + 1 ≤ rootMultiplicity a p
Module: Mathlib.RingTheory.EuclideanDomain

Goal state before:
pp: R : Type u_1
inst✝¹ : EuclideanDomain R
inst✝ : GCDMonoid R
p q : R
hq : q ≠ 0
r : R
hr : q = GCDMonoid.gcd p q * r
⊢ q / GCDMonoid.gcd p q ≠ 0

Tactic:
obtain ⟨pq0, r0⟩ : GCDMonoid.gcd p q ≠ 0 ∧ r ≠ 0 := mul_ne_zero_iff.mp (hr ▸ hq)

Goal state after:
R : Type u_1
inst✝¹ : EuclideanDomain R
inst✝ : GCDMonoid R
p q : R
hq : q ≠ 0
r : R
hr : q = GCDMonoid.gcd p q * r
pq0 : GCDMonoid.gcd p q ≠ 0
r0 : r ≠ 0
⊢ q / GCDMonoid.gcd p q ≠ 0
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x : α
hx : IsUnit x
⊢ factors x = 0

Tactic:
by
  simpa using factors_rel_of_associated (associated_one_iff_isUnit.mpr hx)

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

Goal state before:
pp: case h.left
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a✝¹ a : R
a_unit : IsUnit a
a✝ : a ≠ 0
b : R
⊢ IsRelPrime a b

pp: case h.right
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a✝¹ a : R
a_unit : IsUnit a
a✝ : a ≠ 0
b : R
⊢ 1 * a = a ∧ 1 * b = b

Tactic:
· intro p p_dvd_a _
      exact isUnit_of_dvd_unit p_dvd_a a_unit

Goal state after:
case h.right
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a✝¹ a : R
a_unit : IsUnit a
a✝ : a ≠ 0
b : R
⊢ 1 * a = a ∧ 1 * b = b
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : NormalizedGCDMonoid R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : IsDomain S
f : R →+* S
hinj : Function.Injective ⇑f
p : R[X]
s : S
hpzero : p ≠ 0
hp : f p.content * eval₂ f s p.primPart = 0
⊢ f p.content ≠ 0

Tactic:
hinj.ne_iff' (map_zero _),

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : NormalizedGCDMonoid R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : IsDomain S
f : R →+* S
hinj : Function.Injective ⇑f
p : R[X]
s : S
hpzero : p ≠ 0
hp : f p.content * eval₂ f s p.primPart = 0
⊢ p.content ≠ 0
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Finite

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝² : CommMonoidWithZero M
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : Fintype Mˣ
y : M
hy : y ≠ 0
this✝² : Nontrivial M
this✝¹ : StrongNormalizationMonoid M
this✝ : DecidableEq M
this : DecidableEq (Associates M)
x : M
h : x ∣ y
⊢ x ≠ 0

Tactic:
refine mt (fun hx => ?_) hy

Goal state after:
α : Type u_1
M : Type u_2
inst✝² : CommMonoidWithZero M
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : Fintype Mˣ
y : M
hy : y ≠ 0
this✝² : Nontrivial M
this✝¹ : StrongNormalizationMonoid M
this✝ : DecidableEq M
this : DecidableEq (Associates M)
x : M
h : x ∣ y
hx : x = 0
⊢ y = 0
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a✝ : Associates α
h : ¬a✝ = 0
a b : α
hab : a ≈ b
⊢ (fun x ↦ ↑(factors' a)) ≍ fun x ↦ ↑(factors' b)

Tactic:
apply Function.hfunext

Goal state after:
case hα
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a✝ : Associates α
h : ¬a✝ = 0
a b : α
hab : a ≈ b
⊢ (¬⟦a⟧ = 0) = ¬⟦b⟧ = 0

case h
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a✝ : Associates α
h : ¬a✝ = 0
a b : α
hab : a ≈ b
⊢ ∀ (a_1 : ¬⟦a⟧ = 0) (a' : ¬⟦b⟧ = 0), a_1 ≍ a' → ↑(factors' a) ≍ ↑(factors' b)
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: case mp
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
p_monic : p.Monic
p_1 : p ≠ 1
⊢ (∀ (q : R[X]), q.Monic → 0 < q.degree → q.degree ≤ ↑(p.natDegree / 2) → ¬q ∣ p) →
    ∀ (q : R[X]), q.degree ≤ ↑(p.natDegree / 2) → q ∣ p → IsUnit q

pp: case mpr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
p_monic : p.Monic
p_1 : p ≠ 1
⊢ (∀ (q : R[X]), q.degree ≤ ↑(p.natDegree / 2) → q ∣ p → IsUnit q) →
    ∀ (q : R[X]), q.Monic → 0 < q.degree → q.degree ≤ ↑(p.natDegree / 2) → ¬q ∣ p

Tactic:
· rintro h q deg_le dvd
    by_contra q_unit
    have := degree_pos_of_not_isUnit_of_dvd_monic p_monic q_unit dvd
    have hu := p_monic.isUnit_leadingCoeff_of_dvd dvd
    refine (h _ (monic_of_isUnit_leadingCoeff_inv_smul hu) ?_ ?_ (dvd_trans ?_ dvd)).elim
    · rwa [degree_smul_of_smul_regular _ (isSMulRegular_of_group _)]
    · rwa [degree_smul_of_smul_regular _ (isSMulRegular_of_group _)]
    · rw [Units.smul_def, Polynomial.smul_eq_C_mul, (isUnit_C.mpr (Units.isUnit _)).mul_left_dvd]

Goal state after:
case mpr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
p_monic : p.Monic
p_1 : p ≠ 1
⊢ (∀ (q : R[X]), q.degree ≤ ↑(p.natDegree / 2) → q ∣ p → IsUnit q) →
    ∀ (q : R[X]), q.Monic → 0 < q.degree → q.degree ≤ ↑(p.natDegree / 2) → ¬q ∣ p
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
⊢ IsUnit (p.content * q.content)

Tactic:
hp.content_eq_one,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
⊢ IsUnit (1 * q.content)
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: case neg
R : Type u
k : Type y
inst✝¹ : Field R
inst✝ : Field k
f : R →+* k
x y : R[X]
H : ¬x = 0
⊢ map f x * C (f x.leadingCoeff⁻¹) ∣ map f y ↔ x * C x.leadingCoeff⁻¹ ∣ y

Tactic:
← map_C,

Goal state after:
case neg
R : Type u
k : Type y
inst✝¹ : Field R
inst✝ : Field k
f : R →+* k
x y : R[X]
H : ¬x = 0
⊢ map f x * map f (C x.leadingCoeff⁻¹) ∣ map f y ↔ x * C x.leadingCoeff⁻¹ ∣ y
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝¹ : Field R
inst✝ : DecidableEq R
a : R[X]
⊢ C a.leadingCoeff * (normalizedFactors a).prod = a

Tactic:
by
  by_cases ha : a = 0
  · simp [ha]
  rw [prod_normalizedFactors_eq, normalize_apply, coe_normUnit, CommGroupWithZero.coe_normUnit,
    mul_comm, mul_assoc, ← map_mul, inv_mul_cancel₀] <;>
  simp_all

Goal state after:
Module: Mathlib.Algebra.AlgebraicCard

Goal state before:
pp: R : Type u
A : Type v
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra R A
inst✝ : Module.IsTorsionFree R A
⊢ lift.{u, v} #{ x // IsAlgebraic R x } ≤ lift.{v, u} #R[X] * ℵ₀

Tactic:
← mk_uLift,

Goal state after:
R : Type u
A : Type v
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra R A
inst✝ : Module.IsTorsionFree R A
⊢ #(ULift.{u, v} { x // IsAlgebraic R x }) ≤ lift.{v, u} #R[X] * ℵ₀
Module: Mathlib.Algebra.Central.Basic

Goal state before:
pp: k : Type u_1
K : Type u_2
D : Type u_3
inst✝⁸ : Field k
inst✝⁷ : Field K
inst✝⁶ : Ring D
inst✝⁵ : Nontrivial D
inst✝⁴ : Algebra k K
inst✝³ : Algebra K D
inst✝² : Algebra k D
inst✝¹ : IsScalarTower k K D
inst✝ : IsCentral k D
⊢ Function.Bijective ⇑(algebraMap k K)

Tactic:
have : IsCentral K D :=
  { out := fun x ↦ show x ∈ Subalgebra.center k D → _ by
      simp only [center_eq_bot, mem_bot, Set.mem_range, forall_exists_index]
      rintro x rfl
      exact ⟨algebraMap k K x, by simp [algebraMap_eq_smul_one, smul_assoc]⟩ }

Goal state after:
k : Type u_1
K : Type u_2
D : Type u_3
inst✝⁸ : Field k
inst✝⁷ : Field K
inst✝⁶ : Ring D
inst✝⁵ : Nontrivial D
inst✝⁴ : Algebra k K
inst✝³ : Algebra K D
inst✝² : Algebra k D
inst✝¹ : IsScalarTower k K D
inst✝ : IsCentral k D
this : IsCentral K D
⊢ Function.Bijective ⇑(algebraMap k K)
Module: Mathlib.Algebra.Central.Basic

Goal state before:
pp: k : Type u_1
K : Type u_2
D : Type u_3
inst✝⁸ : Field k
inst✝⁷ : Field K
inst✝⁶ : Ring D
inst✝⁵ : Nontrivial D
inst✝⁴ : Algebra k K
inst✝³ : Algebra K D
inst✝² : Algebra k D
inst✝¹ : IsScalarTower k K D
inst✝ : IsCentral k D
this : IsCentral K D
x : K
x' : k
H : (algebraMap k D) x' = (algebraMap K D) x
⊢ ∃ a, (algebraMap k K) a = x

Tactic:
exact ⟨x', (algebraMap K D).injective <| by simp [← H, algebraMap_eq_smul_one]⟩

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

Goal state before:
pp: R : Type u
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : Function.Injective ⇑(algebraMap R S)
⊢ (∀ (x : S), IsAlgebraic (↥⊥) x) ↔ ∀ (x : S), IsAlgebraic R x

Tactic:
isAlgebraic_bot_iff h

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : S
hs : s ∈ S⁰
p : R[X]
hp0 : p ≠ 0
hp : (aeval s) p = 0
⊢ ∃ q, q.coeff 0 ≠ 0 ∧ (aeval s) q = 0

Tactic:
obtain ⟨q, hpq, hq⟩ := exists_eq_pow_rootMultiplicity_mul_and_not_dvd p hp0 0

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : S
hs : s ∈ S⁰
p : R[X]
hp0 : p ≠ 0
hp : (aeval s) p = 0
q : R[X]
hpq : p = (X - C 0) ^ rootMultiplicity 0 p * q
hq : ¬X - C 0 ∣ q
⊢ ∃ q, q.coeff 0 ≠ 0 ∧ (aeval s) q = 0
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: case inr
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst✝² : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst✝¹ : SuccOrder ι
equiv : (j : ↑(Iic i)) → F ↑j ≃ piLT X ↑j
e : F i⁺ ≃ F i × X i
hi : ¬IsMax i
inst✝ : InverseSystem f
H : ∀ (x : F i⁺), (e x).1 = f ⋯ x
nat : IsNatEquiv f equiv
j k : ι
hj✝ : j ∈ Iic i⁺
hk : k ∈ Iic i⁺
h : k ≤ j
x : F j
lt_succ : ∀ {j : ι}, j ≤ i → j < i⁺
hj : j ≤ i
⊢ piLTProj h ((equiv ⟨j, hj⟩) x) =
    piLTProj h
      ((piSplitLE
          (fun j ↦ equiv ⟨↑j, ⋯⟩,
            e.trans (((equiv ⟨i, ⋯⟩).prodCongr (Equiv.refl (X i))).trans (piSplitLE.trans (Equiv.piCongrSet ⋯))))
          ⟨j, hj✝⟩)
        x)

Tactic:
piSplitLE_lt (lt_succ hj)

Goal state after:
case inr
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst✝² : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst✝¹ : SuccOrder ι
equiv : (j : ↑(Iic i)) → F ↑j ≃ piLT X ↑j
e : F i⁺ ≃ F i × X i
hi : ¬IsMax i
inst✝ : InverseSystem f
H : ∀ (x : F i⁺), (e x).1 = f ⋯ x
nat : IsNatEquiv f equiv
j k : ι
hj✝ : j ∈ Iic i⁺
hk : k ∈ Iic i⁺
h : k ≤ j
x : F j
lt_succ : ∀ {j : ι}, j ≤ i → j < i⁺
hj : j ≤ i
⊢ piLTProj h ((equiv ⟨j, hj⟩) x) =
    piLTProj h
      (((fun j ↦ equiv ⟨↑j, ⋯⟩,
              e.trans (((equiv ⟨i, ⋯⟩).prodCongr (Equiv.refl (X i))).trans (piSplitLE.trans (Equiv.piCongrSet ⋯)))).1
          ⟨j, ⋯⟩)
        x)
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst✝¹ : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
equiv : (j : ↑(Iio i)) → F ↑j ≃ piLT X ↑j
nat : IsNatEquiv f equiv
equivLim : F i ≃ ↑(limit f i)
hi : IsSuccPrelimit i
inst✝ : InverseSystem f
H : ∀ (x : F i) (l : ↑(Iio i)), ↑(equivLim x) l = f ⋯ x
j k : ι
hj : j ∈ Iic i
hk : k ∈ Iic i
h : k ≤ j
t : F j
⊢ (piEquivLim nat equivLim hi ⟨k, hk⟩) (f h t) = piLTProj h ((piEquivLim nat equivLim hi ⟨j, hj⟩) t)

Tactic:
by
  obtain rfl | hj := hj.eq_or_lt
  · obtain rfl | hk := hk.eq_or_lt
    · simp [InverseSystem.map_self]
    · funext l
      simp_rw [piEquivLim, piSplitLE_lt hk, piSplitLE_eq, Equiv.trans_apply]
      rw [piLTProj, piLTLim_symm_apply hi ⟨k, hk⟩ (by exact l.2), invLimEquiv_apply_coe, H]
  · rw [piEquivLim, piSplitLE_lt (h.trans_lt hj), piSplitLE_lt hj]; apply nat

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
N : Type u_3
P : Type u_4
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : Module R N
inst✝² : Module R P
g : N →ₗ[R] P
A : Type u_6
inst✝¹ : Semiring A
inst✝ : Algebra R A
hg : Function.Surjective ⇑g
⊢ Function.Surjective ⇑(baseChange A g)

Tactic:
rw [LinearMap.baseChange_eq_ltensor]

Goal state after:
R : Type u_1
inst✝⁶ : CommSemiring R
N : Type u_3
P : Type u_4
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : Module R N
inst✝² : Module R P
g : N →ₗ[R] P
A : Type u_6
inst✝¹ : Semiring A
inst✝ : Algebra R A
hg : Function.Surjective ⇑g
⊢ Function.Surjective ⇑(lTensor A g)
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: case h
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_2
B : Type u_3
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal A
x✝ : A ⊗[R] B
hx : x✝ ∈ ↑(Submodule.restrictScalars R (Submodule.span (A ⊗[R] B) (⇑includeLeft '' ↑I)))
x : ↥(Submodule.restrictScalars R I) ⊗[R] B
⊢ (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) 0 =
    0 • (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) x

Tactic:
simp only [map_zero, smul_eq_mul, zero_mul]

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

Goal state before:
pp: case a.tmul
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_2
B : Type u_3
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal A
a : ↥(Submodule.restrictScalars R I)
b : B
⊢ (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) (a ⊗ₜ[R] b) ∈
    ↑(Submodule.restrictScalars R (map includeLeft I))

Tactic:
simp only [LinearMap.rTensor_tmul, Submodule.coe_subtype]

Goal state after:
case a.tmul
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_2
B : Type u_3
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal A
a : ↥(Submodule.restrictScalars R I)
b : B
⊢ ↑a ⊗ₜ[R] b ∈ ↑(Submodule.restrictScalars R (map includeLeft I))
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: case h
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_2
B : Type u_3
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal B
x✝ : A ⊗[R] B
hx : x✝ ∈ ↑(Submodule.restrictScalars R (Submodule.span (A ⊗[R] B) (⇑includeRight '' ↑I)))
x : A ⊗[R] ↥(Submodule.restrictScalars R I)
⊢ (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) 0 =
    0 • (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) x

Tactic:
simp only [map_zero, smul_eq_mul, zero_mul]

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

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Small.{v', u} R
⊢ Flat R M →
    ∀ ⦃N N' : Type v'⦄ [inst : AddCommMonoid N] [inst_1 : AddCommMonoid N'] [inst_2 : Module R N] [inst_3 : Module R N']
      (f : N →ₗ[R] N'), Injective ⇑f → Injective ⇑(rTensor M f)

Tactic:
by introv _; apply rTensor_preserves_injective_linearMap

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

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Small.{v', u} R
⊢ Flat R M →
    ∀ ⦃N N' : Type v'⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : Module R N] [inst_3 : Module R N']
      (f : N →ₗ[R] N'), Injective ⇑f → Injective ⇑(rTensor M f)

Tactic:
by introv _; apply rTensor_preserves_injective_linearMap

Goal state after:
Module: Mathlib.Algebra.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module ℚ≥0 M
s : Finset ι
f : ι → M
t : Finset κ
g : κ → M
i : ι → κ
hi : ∀ a ∈ s, i a ∈ t
h : ∀ a ∈ s, f a = g (i a)
i_inj : Set.InjOn i ↑s
i_surj : Set.SurjOn i ↑s ↑t
⊢ 𝔼 i ∈ s, f i = 𝔼 i ∈ t, g i

Tactic:
by
  simp_rw [expect, card_nbij i hi i_inj i_surj, sum_nbij i hi i_inj i_surj h]

Goal state after:
Module: Mathlib.Order.Interval.Finset.Gaps

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
j : ℕ
hj : j < k
this : ↑j.succ = ⟨j, hj⟩.succ
⊢ (F.intervalGapsWithin h a b ↑j.succ).1 = ((F.orderEmbOfFin h) ⟨j, hj⟩).2

Tactic:
grind [intervalGapsWithin, intervalGapsWithin.fst]

Goal state after:
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: a b x : ℤ
⊢ (∃ a_1 < (b + 1 - a).toNat, (addLeftEmbedding a) ↑a_1 = x) ↔ a ≤ x ∧ x ≤ b

Tactic:
addLeftEmbedding_apply

Goal state after:
a b x : ℤ
⊢ (∃ a_1 < (b + 1 - a).toNat, a + ↑a_1 = x) ↔ a ≤ x ∧ x ≤ b
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: a b x : ℤ
⊢ (∃ a_1 < (b - a).toNat, (addLeftEmbedding a) ↑a_1 = x) ↔ a ≤ x ∧ x < b

Tactic:
addLeftEmbedding_apply

Goal state after:
a b x : ℤ
⊢ (∃ a_1 < (b - a).toNat, a + ↑a_1 = x) ↔ a ≤ x ∧ x < b
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: a b x : ℤ
⊢ (∃ a_1 < (b - a).toNat, (addLeftEmbedding (a + 1)) ↑a_1 = x) ↔ a < x ∧ x ≤ b

Tactic:
addLeftEmbedding_apply

Goal state after:
a b x : ℤ
⊢ (∃ a_1 < (b - a).toNat, a + 1 + ↑a_1 = x) ↔ a < x ∧ x ≤ b
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: a b x : ℤ
⊢ (∃ a_1 < (b - a - 1).toNat, (addLeftEmbedding (a + 1)) ↑a_1 = x) ↔ a < x ∧ x < b

Tactic:
addLeftEmbedding_apply

Goal state after:
a b x : ℤ
⊢ (∃ a_1 < (b - a - 1).toNat, a + 1 + ↑a_1 = x) ↔ a < x ∧ x < b
Module: Mathlib.Order.Interval.Finset.Gaps

Goal state before:
pp: case neg
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j✝ : ℕ
a b : α
hab : a ≤ b
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hF : (↑F).PairwiseDisjoint fun z ↦ Icc z.1 z.2
j : ℕ
hj : j < k + 1
hj₁ : ¬j = 0
hk : k - 1 + 1 = k
hj₂ : ¬j = k
⊢ ((F.orderEmbOfFin h) ⟨j - 1, ⋯⟩).2 ≤ ((F.orderEmbOfFin h) ⟨j, ⋯⟩).1

Tactic:
have hj₃ : (⟨j - 1, by omega⟩ : Fin k) ≠ ⟨j, by omega⟩ := by grind

Goal state after:
case neg
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j✝ : ℕ
a b : α
hab : a ≤ b
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hF : (↑F).PairwiseDisjoint fun z ↦ Icc z.1 z.2
j : ℕ
hj : j < k + 1
hj₁ : ¬j = 0
hk : k - 1 + 1 = k
hj₂ : ¬j = k
hj₃ : ⟨j - 1, ⋯⟩ ≠ ⟨j, ⋯⟩
⊢ ((F.orderEmbOfFin h) ⟨j - 1, ⋯⟩).2 ≤ ((F.orderEmbOfFin h) ⟨j, ⋯⟩).1
Module: Mathlib.Data.List.Sym

Goal state before:
pp: case mpr
α : Type u_1
xs : List α
a b : α
⊢ a ∈ xs ∧ b ∈ xs → s(a, b) ∈ xs.sym2

Tactic:
rintro ⟨ha, hb⟩

Goal state after:
case mpr
α : Type u_1
xs : List α
a b : α
ha : a ∈ xs
hb : b ∈ xs
⊢ s(a, b) ∈ xs.sym2
Module: Mathlib.Data.List.Sym

Goal state before:
pp: α : Type u_1
x : α
xs : List α
h : x ∈ xs
⊢ map (fun y ↦ s(x, y)) xs <+ xs.sym2

Tactic:
by
  induction xs with
  | nil => simp
  | cons x' xs ih =>
    simp only [map_cons, List.sym2, cons_append]
    cases h with
    | head =>
      exact (sublist_append_left _ _).cons_cons _
    | tail _ h =>
      refine .cons _ ?_
      rw [← singleton_append]
      refine .append ?_ (ih h)
      rw [singleton_sublist, mem_map]
      exact ⟨_, h, Sym2.eq_swap⟩

Goal state after:
Module: Mathlib.Data.List.Sym

Goal state before:
pp: α : Type u_1
x : α
xs : List α
h : x ∉ xs
⊢ (map (fun y ↦ s(x, y)) xs).Disjoint xs.sym2

Tactic:
induction xs with
  | nil => simp
  | cons x' xs ih => aesop (add simp mk_mem_sym2_iff, unfold safe List.Disjoint)

Goal state after:
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : DecidableEq α
n : ℕ
h : s.Nonempty
⊢ (s.sym n).Nonempty

Tactic:
exact h.sym _

Goal state after:
Module: Mathlib.Data.List.Sym

Goal state before:
pp: α : Type u_1
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
h : (x :: xs).Nodup
z : Sym α (n + 1)
hz : ∃ a ∈ List.sym n (x :: xs), x ::ₛ a = z
hz' : z ∈ List.sym (n + 1) xs
⊢ False

Tactic:
obtain ⟨z, _hz, rfl⟩ := hz

Goal state after:
α : Type u_1
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
h : (x :: xs).Nodup
z : Sym α n
_hz : z ∈ List.sym n (x :: xs)
hz' : x ::ₛ z ∈ List.sym (n + 1) xs
⊢ False
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
g : β → γ
f : α → β
x : Sym2 α
⊢ map g (map f x) = map (g ∘ f) x

Tactic:
by
  induction x; aesop

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
e : Sym2 α
⊢ e = s((Quot.out e).1, (Quot.out e).2)

Tactic:
by rw [Sym2.mk, e.out_eq]

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝²³ : AddCommMonoid M
inst✝²² : AddCommMonoid N
inst✝²¹ : CommSemiring R
inst✝²⁰ : CommSemiring S
inst✝¹⁹ : Algebra R S
inst✝¹⁸ : Module R M
inst✝¹⁷ : Module R N
inst✝¹⁶ : Module S N
inst✝¹⁵ : IsScalarTower R S N
T : Type u_4
O : Type u_5
inst✝¹⁴ : CommSemiring T
inst✝¹³ : Algebra R T
inst✝¹² : Algebra S T
inst✝¹¹ : IsScalarTower R S T
inst✝¹⁰ : AddCommMonoid O
inst✝⁹ : Module R O
inst✝⁸ : Module S O
inst✝⁷ : Module T O
inst✝⁶ : IsScalarTower S T O
inst✝⁵ : IsScalarTower R S O
inst✝⁴ : IsScalarTower R T O
f : M →ₗ[R] N
hf : IsBaseChange S f
g : N →ₗ[S] O
hg : IsBaseChange T g
Q : Type (max v₁ u_5 u_4)
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
inst✝¹ : Module T Q
inst✝ : IsScalarTower R T Q
i : M →ₗ[R] Q
this : Module S Q := Module.compHom Q (algebraMap S T)
x : S
y : T
z : Q
⊢ (x • y) • z = x • y • z

Tactic:
by
      rw [Algebra.smul_def, mul_smul]
      rfl

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
x y : α
h : diag x = diag y
⊢ x = y

Tactic:
cases Sym2.exact h

Goal state after:
case refl
α : Type u_1
x : α
h : diag x = diag x
⊢ x = x

case swap
α : Type u_1
x : α
h : diag x = diag x
⊢ x = x
Module: Mathlib.CategoryTheory.ObjectProperty.Basic

Goal state before:
pp: C : Type u
D : Type u'
inst✝¹ : Category.{v, u} C
inst✝ : Category.{v', u'} D
P : ObjectProperty C
F : C ⥤ D
X : C
hX : P X
⊢ P.map F (F.obj X)

Tactic:
exact ⟨X, hX, ⟨Iso.refl _⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Discrete.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : IsDiscrete C
⊢ ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y), X = Y

Tactic:
rintro ⟨_⟩ ⟨_⟩ ⟨f⟩

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : IsDiscrete C
unop✝¹ unop✝ : C
f : Opposite.unop (Opposite.op unop✝) ⟶ Opposite.unop (Opposite.op unop✝¹)
⊢ Opposite.op unop✝¹ = Opposite.op unop✝
Module: Mathlib.CategoryTheory.CommSq

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
A B X Y : C
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
l : sq.LiftStruct
⊢ l.l.op ≫ i.op = f.op

Tactic:
rw [← op_comp, l.fac_left]

Goal state after:
Module: Mathlib.CategoryTheory.Types.Basic

Goal state before:
pp: case mp
X Y : Type u
f : X → Y
⊢ Epi (↾f) → Function.Surjective f

Tactic:
rintro ⟨H⟩

Goal state after:
case mp
X Y : Type u
f : X → Y
H : ∀ {Z : Type u} (g h : Y ⟶ Z), ↾f ≫ g = ↾f ≫ h → g = h
⊢ Function.Surjective f