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

Goal state before:
pp: case zero
R : Type u
inst✝³ : CommSemiring R
inst✝² : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
inst✝¹ : CharZero R
inst✝ : ExpChar R 1
⊢ contract 1 f = f

Tactic:
contract_one

Goal state after:
case zero
R : Type u
inst✝³ : CommSemiring R
inst✝² : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
inst✝¹ : CharZero R
inst✝ : ExpChar R 1
⊢ f = f
Module: Mathlib.Algebra.Polynomial.Eval.SMul

Goal state before:
pp: R : Type u
S : Type v
inst✝² : Semiring R
inst✝¹ : SMulZeroClass S R
inst✝ : IsScalarTower S R R
s : S
p q : R[X]
⊢ (s • 1) • eval₂ C q p = s • eval₂ C q p

Tactic:
smul_assoc,

Goal state after:
R : Type u
S : Type v
inst✝² : Semiring R
inst✝¹ : SMulZeroClass S R
inst✝ : IsScalarTower S R R
s : S
p q : R[X]
⊢ s • 1 • eval₂ C q p = s • eval₂ C q p
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
h✝ : q ∣ p
a✝ : Nontrivial R
r : R[X]
hr : p = q * r
hpq0 : ¬p %ₘ q = 0
hmod : p %ₘ q = q * (r - p /ₘ q)
this : (q * (r - p /ₘ q)).degree < q.degree
h : (r - p /ₘ q).leadingCoeff = 0
⊢ (q * 0).leadingCoeff = 0

Tactic:
mul_zero,

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
h✝ : q ∣ p
a✝ : Nontrivial R
r : R[X]
hr : p = q * r
hpq0 : ¬p %ₘ q = 0
hmod : p %ₘ q = q * (r - p /ₘ q)
this : (q * (r - p /ₘ q)).degree < q.degree
h : (r - p /ₘ q).leadingCoeff = 0
⊢ leadingCoeff 0 = 0
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hmo : q.Monic
a✝ : Nontrivial R
⊢ degree 0 < q.degree

Tactic:
degree_zero

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
hmo : q.Monic
a✝ : Nontrivial R
⊢ ⊥ < q.degree
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH : (⇑derivative)^[n] (p * q) = ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q)
⊢ ∑ x ∈ range (n + 1),
      ↑(n.choose x) *
        (derivative ((⇑derivative)^[n - x] p) * (⇑derivative)^[x] q +
          (⇑derivative)^[n - x] p * derivative ((⇑derivative)^[x] q)) =
    ∑ x ∈ range (n + 1), ↑(n.choose x) * (derivative ((⇑derivative)^[n - x] p) * (⇑derivative)^[x] q) +
      ∑ x ∈ range (n + 1), ↑(n.choose x) * ((⇑derivative)^[n - x] p * derivative ((⇑derivative)^[x] q))

Tactic:
mul_add,

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH : (⇑derivative)^[n] (p * q) = ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q)
⊢ ∑ x ∈ range (n + 1),
      (↑(n.choose x) * (derivative ((⇑derivative)^[n - x] p) * (⇑derivative)^[x] q) +
        ↑(n.choose x) * ((⇑derivative)^[n - x] p * derivative ((⇑derivative)^[x] q))) =
    ∑ x ∈ range (n + 1), ↑(n.choose x) * (derivative ((⇑derivative)^[n - x] p) * (⇑derivative)^[x] q) +
      ∑ x ∈ range (n + 1), ↑(n.choose x) * ((⇑derivative)^[n - x] p * derivative ((⇑derivative)^[x] q))
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p₁ p₂ q : R[X]
hq : q.Monic
a✝ : Nontrivial R
f : R[X]
sub_eq : p₁ - p₂ = q * f
⊢ p₂ %ₘ q + q * (p₂ /ₘ q + f) = q * f + p₂

Tactic:
mul_add,

Goal state after:
R : Type u
inst✝ : CommRing R
p₁ p₂ q : R[X]
hq : q.Monic
a✝ : Nontrivial R
f : R[X]
sub_eq : p₁ - p₂ = q * f
⊢ p₂ %ₘ q + (q * (p₂ /ₘ q) + q * f) = q * f + p₂
Module: Mathlib.Order.Filter.CountablyGenerated

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Sort u_5
f g : Filter α
inst✝¹ : f.IsCountablyGenerated
inst✝ : g.IsCountablyGenerated
⊢ (f ⊔ g).IsCountablyGenerated

Tactic:
rcases f.exists_antitone_basis with ⟨s, hs⟩
  rcases g.exists_antitone_basis with ⟨t, ht⟩
  exact HasCountableBasis.isCountablyGenerated ⟨hs.1.sup ht.1, Set.to_countable _⟩

Goal state after:
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : CommRing R
q p₁ p₂ : R[X]
hq : q.Monic
hR : Nontrivial R
⊢ p₁ %ₘ q + p₂ %ₘ q + q * (p₁ /ₘ q + p₂ /ₘ q) = p₁ + p₂

Tactic:
mul_add,

Goal state after:
R : Type u
inst✝ : CommRing R
q p₁ p₂ : R[X]
hq : q.Monic
hR : Nontrivial R
⊢ p₁ %ₘ q + p₂ %ₘ q + (q * (p₁ /ₘ q) + q * (p₂ /ₘ q)) = p₁ + p₂
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : CommRing R
q p₁ p₂ : R[X]
⊢ (p₁ + p₂) %ₘ q = p₁ %ₘ q + p₂ %ₘ q

Tactic:
by_cases hq : q.Monic
  · rcases subsingleton_or_nontrivial R with hR | hR
    · simp only [eq_iff_true_of_subsingleton]
    · exact
      (div_modByMonic_unique (p₁ /ₘ q + p₂ /ₘ q) _ hq
          ⟨by
            rw [mul_add, add_left_comm, add_assoc, modByMonic_add_div, ← add_assoc,
              add_comm (q * _), modByMonic_add_div],
            (degree_add_le _ _).trans_lt
              (max_lt (degree_modByMonic_lt _ hq) (degree_modByMonic_lt _ hq))⟩).2
  · simp_rw [modByMonic_eq_of_not_monic _ hq]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
p : R[X]
inst✝ : IsDomain R
hi : Irreducible p
x : R
hx : p.IsRoot x
g : R[X]
hg : p = (X - C x) * g
this : IsUnit (X - C x) ∨ IsUnit g
h : IsUnit (X - C x)
⊢ p.degree = 1

Tactic:
have h₁ : degree (X - C x) = 1 := degree_X_sub_C x

Goal state after:
R : Type u
inst✝¹ : CommRing R
p : R[X]
inst✝ : IsDomain R
hi : Irreducible p
x : R
hx : p.IsRoot x
g : R[X]
hg : p = (X - C x) * g
this : IsUnit (X - C x) ∨ IsUnit g
h : IsUnit (X - C x)
h₁ : (X - C x).degree = 1
⊢ p.degree = 1
Module: Mathlib.Order.Filter.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
β : ι → Type u_3
m : (i : ι) → α i → β i
s : Set ((i : ι) → β i)
h : ∀ (i : ι), ∃ t₁, m i ⁻¹' t₁ ∈ f i ∧ eval i ⁻¹' t₁ ⊆ s
i : ι
t : Set (β i)
H : m i ⁻¹' t ∈ f i
hH : eval i ⁻¹' t ⊆ s
⊢ ∃ t₁ ∈ f i, eval i ⁻¹' t₁ ⊆ (fun k i ↦ m i (k i)) ⁻¹' s

Tactic:
exact ⟨{ x : α i | m i x ∈ t }, H, fun x hx => hH hx⟩

Goal state after:
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
g : Filter β
h : Filter γ
⊢ map (⇑(Equiv.prodAssoc α β γ).symm) (f ×ˢ g ×ˢ h) = (f ×ˢ g) ×ˢ h

Tactic:
by
  simp_rw [map_equiv_symm, prod_eq_inf, comap_inf, comap_comap, inf_assoc,
    Function.comp_def, Equiv.prodAssoc_apply]

Goal state after:
Module: Mathlib.Order.Filter.Cofinite

Goal state before:
pp: case refine_4.refine_3
α : Type u_2
f : Filter α
q : Set α × Filter α
hq : (fun p ↦ p.2 ≤ cofinite ∧ Disjoint (𝓟 p.1) p.2 ∧ f = 𝓟 p.1 ⊔ p.2) q
hqk : f.ker = q.1
⊢ Coheyting.boundary f ≤ q.2

Tactic:
· grw [hq.2.2, Coheyting.boundary_sup_le, boundary_principal, bot_sup_eq]
      exact Coheyting.boundary_le

Goal state after:
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: case neg
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp0 : ¬p = 0
⊢ p.roots.card ≤ p.natDegree

Tactic:
exact WithBot.coe_le_coe.1 (le_trans (card_roots hp0) (le_of_eq <| degree_eq_natDegree hp0))

Goal state after:
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: case succ
σ : Type u_5
s : Set ℕ
n : ℕ
hn : n + 1 ≠ 0
⊢ ⇑degree ⁻¹' ((n + 1) • s) = (n + 1) • ⇑degree ⁻¹' s

Tactic:
induction n <;> simp_all [succ_nsmul, degree_preimage_add]

Goal state after:
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝ : Field R
p q : R[X]
hq0 : q ≠ 0
h : p / q = 0
this : q * 0 + p % q = p
⊢ p.degree < q.degree

Tactic:
mul_zero,

Goal state after:
R : Type u
inst✝ : Field R
p q : R[X]
hq0 : q ≠ 0
h : p / q = 0
this : 0 + p % q = p
⊢ p.degree < q.degree
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
s t : Associates α
d : Associates α
eq : t = s * d
⊢ s.factors ≤ t.factors

Tactic:
by rw [eq, factors_mul]; exact le_add_of_nonneg_right bot_le

Goal state after:
Module: Mathlib.RingTheory.Polynomial.UniqueFactorization

Goal state before:
pp: case neg
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : NoZeroDivisors R
inst✝ : WfDvdMonoid R
f a : R[X]
ane0 : a ≠ 0
c : R[X]
not_unit_c : ¬IsUnit c
hac : ¬a * c = 0
cne0 : c ≠ 0
hdeg : ¬c.natDegree = 0
⊢ a.natDegree < a.natDegree + c.natDegree

Tactic:
exact lt_add_of_pos_right _ (Nat.pos_of_ne_zero hdeg)

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

Goal state before:
pp: case neg
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
p a : Associates α
hp : Irreducible p
n : ℕ
h✝ : a ∣ p ^ n
a✝ : Nontrivial α
hph : p ^ n ≠ 0
ha : a ≠ 0
eq_zero_of_ne : ∀ (q : Associates α), Irreducible q → q ≠ p → q.count a.factors = 0
q : Associates α
hq : Irreducible q
h : ¬q = p
⊢ q.count a.factors = p.count a.factors * 0

Tactic:
mul_zero,

Goal state after:
case neg
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
p a : Associates α
hp : Irreducible p
n : ℕ
h✝ : a ∣ p ^ n
a✝ : Nontrivial α
hph : p ^ n ≠ 0
ha : a ≠ 0
eq_zero_of_ne : ∀ (q : Associates α), Irreducible q → q ≠ p → q.count a.factors = 0
q : Associates α
hq : Irreducible q
h : ¬q = p
⊢ q.count a.factors = 0
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
h : Subsingleton R
⊢ ¬IsAlgebraic R a

Tactic:
apply is_transcendental_of_subsingleton

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

Goal state before:
pp: case e'_3
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
p : K[X]
aeval_eq : (aeval x) p = 0
coeff_zero_ne : p.coeff 0 ≠ 0
⊢ -((aeval x) p.divX / (algebraMap K L) (p.coeff 0)) = (aeval x) p.divX / ((aeval x) p - (algebraMap K L) (p.coeff 0))

Tactic:
rw [aeval_eq, zero_sub, div_neg]

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

Goal state before:
pp: case refine_3
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : ↥A
p : K[X]
⊢ ∀ (p : K[X]), p ≠ 0 → (p ≠ 0 → (aeval x) p = 0 → (↑x)⁻¹ ∈ A) → p * X ≠ 0 → (aeval x) (p * X) = 0 → (↑x)⁻¹ ∈ A

Tactic:
intro p hp ih _ne_zero aeval_eq

Goal state after:
case refine_3
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : ↥A
p✝ p : K[X]
hp : p ≠ 0
ih : p ≠ 0 → (aeval x) p = 0 → (↑x)⁻¹ ∈ A
_ne_zero : p * X ≠ 0
aeval_eq : (aeval x) (p * X) = 0
⊢ (↑x)⁻¹ ∈ A
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: ι : Type u_6
inst✝ : LinearOrder ι
X : ι → Type u_7
i : ι
hi : IsSuccPrelimit i
f : ↑(limit piLTProj i)
k l : ↑(Iio i)
hl : ↑l < ↑k
⊢ (piLTLim hi).symm f l = ↑f k ⟨↑l, hl⟩

Tactic:
by
  conv_rhs => rw [← (piLTLim hi).right_inv f]
  rfl

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

Goal state before:
pp: case add
R : Type u_1
inst✝⁶ : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : AddCommMonoid Q
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : N →ₗ[R] P
hg : Function.Surjective ⇑g
x y : Q ⊗[R] P
hx : ∃ a, (lTensor Q g) a = x
hy : ∃ a, (lTensor Q g) a = y
⊢ ∃ a, (lTensor Q g) a = x + y

Tactic:
obtain ⟨x, rfl⟩ := hx
    obtain ⟨y, rfl⟩ := hy
    exact ⟨x + y, map_add _ _ _⟩

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

Goal state before:
pp: case add
R : Type u_1
inst✝⁶ : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : AddCommMonoid Q
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : N →ₗ[R] P
hg : Function.Surjective ⇑g
x y : P ⊗[R] Q
hx : ∃ a, (rTensor Q g) a = x
hy : ∃ a, (rTensor Q g) a = y
⊢ ∃ a, (rTensor Q g) a = x + y

Tactic:
obtain ⟨x, rfl⟩ := hx
    obtain ⟨y, rfl⟩ := hy
    exact ⟨x + y, map_add _ _ _⟩

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P Q : Submodule R M
smallP : Small.{u, u_2} ↥P
smallQ : Small.{u, u_2} ↥Q
⊢ Small.{u, u_2} ↥(P ⊔ Q)

Tactic:
rw [Submodule.sup_eq_range]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P Q : Submodule R M
smallP : Small.{u, u_2} ↥P
smallQ : Small.{u, u_2} ↥Q
⊢ Small.{u, u_2} ↥(P.subtype.coprod Q.subtype).range
Module: Mathlib.RingTheory.MvPolynomial.Basic

Goal state before:
pp: σ : Type u
R : Type v
inst✝ : CommSemiring R
m : ℕ
p : MvPolynomial σ R
⊢ p ∈ restrictTotalDegree σ R m ↔ p.totalDegree ≤ m

Tactic:
by
  rw [totalDegree, Finset.sup_le_iff]
  rfl

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

Goal state before:
pp: case a.refine_4.zero
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
⊢ ∃ y,
    (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) y =
      0 • (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) x

Tactic:
use 0
        simp only [map_zero, smul_eq_mul, zero_mul]

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

Goal state before:
pp: case a.refine_4.zero
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)
⊢ ∃ y,
    (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) y =
      0 • (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) x

Tactic:
use 0
        simp only [map_zero, smul_eq_mul, zero_mul]

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

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
A : Type u_6
B : Type u_7
C : Type u_8
D : Type u_9
inst✝¹¹ : Ring A
inst✝¹⁰ : Ring B
inst✝⁹ : Ring C
inst✝⁸ : Ring D
inst✝⁷ : Algebra R A
inst✝⁶ : Algebra R B
inst✝⁵ : Algebra R C
inst✝⁴ : Algebra R D
inst✝³ : Algebra S A
inst✝² : Algebra S B
inst✝¹ : IsScalarTower R S A
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
g : C →ₐ[R] D
hf : Function.Surjective ⇑f
hg : Function.Surjective ⇑g
this : map f g = (map f (AlgHom.id R D)).comp (map (AlgHom.id S A) g)
⊢ RingHom.ker ((↑(map f (AlgHom.id R D))).comp ↑(map (AlgHom.id S A) g)) =
    Ideal.map includeLeft (RingHom.ker ↑f) ⊔ Ideal.map includeRight (RingHom.ker ↑g)

Tactic:
← RingHom.comap_ker

Goal state after:
R : Type u_4
S : Type u_5
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
A : Type u_6
B : Type u_7
C : Type u_8
D : Type u_9
inst✝¹¹ : Ring A
inst✝¹⁰ : Ring B
inst✝⁹ : Ring C
inst✝⁸ : Ring D
inst✝⁷ : Algebra R A
inst✝⁶ : Algebra R B
inst✝⁵ : Algebra R C
inst✝⁴ : Algebra R D
inst✝³ : Algebra S A
inst✝² : Algebra S B
inst✝¹ : IsScalarTower R S A
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
g : C →ₐ[R] D
hf : Function.Surjective ⇑f
hg : Function.Surjective ⇑g
this : map f g = (map f (AlgHom.id R D)).comp (map (AlgHom.id S A) g)
⊢ Ideal.comap (↑(map (AlgHom.id S A) g)) (RingHom.ker ↑(map f (AlgHom.id R D))) =
    Ideal.map includeLeft (RingHom.ker ↑f) ⊔ Ideal.map includeRight (RingHom.ker ↑g)
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
⊢ Flat R M ↔
    ∀ ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P), Injective ⇑(lTensor M N.subtype)

Tactic:
iff_rTensor_injectiveₛ,

Goal state after:
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ (∀ ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P),
      Injective ⇑(rTensor M N.subtype)) ↔
    ∀ ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P), Injective ⇑(lTensor M N.subtype)
Module: Mathlib.RingTheory.Flat.Basic

Goal state before:
pp: R : Type u
M : Type v
N : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : ∀ ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P), Injective ⇑(rTensor M N.subtype)
i : N →ₗ[R] M
r : M →ₗ[R] N
h : r ∘ₗ i = LinearMap.id
P : Type u
x✝¹ : AddCommMonoid P
x✝ : Module R P
Q : Submodule R P
⊢ Injective ⇑(lTensor P i ∘ₗ rTensor N Q.subtype)

Tactic:
lTensor_comp_rTensor,

Goal state after:
R : Type u
M : Type v
N : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : ∀ ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P), Injective ⇑(rTensor M N.subtype)
i : N →ₗ[R] M
r : M →ₗ[R] N
h : r ∘ₗ i = LinearMap.id
P : Type u
x✝¹ : AddCommMonoid P
x✝ : Module R P
Q : Submodule R P
⊢ Injective ⇑(TensorProduct.map Q.subtype i)
Module: Mathlib.RingTheory.Flat.Basic

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
ι : Type v
M : ι → Type w
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
⊢ Flat R (⨁ (i : ι), M i) ↔ ∀ (i : ι), Flat R (M i)

Tactic:
iff_rTensor_injectiveₛ,

Goal state after:
R : Type u
inst✝² : CommSemiring R
ι : Type v
M : ι → Type w
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
⊢ (∀ ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P),
      Injective ⇑(rTensor (⨁ (i : ι), M i) N.subtype)) ↔
    ∀ (i : ι) ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P),
      Injective ⇑(rTensor (M i) N.subtype)
Module: Mathlib.RingTheory.Flat.Basic

Goal state before:
pp: R : Type u_1
A : Type u_3
B : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
inst✝ : Module.Flat R B
ha : Function.Injective ⇑(algebraMap R A)
⊢ Function.Injective ⇑includeRight

Tactic:
convert!
    Module.Flat.rTensor_preserves_injective_linearMap (M := B) (Algebra.linearMap R A) ha |>.comp
      (_root_.TensorProduct.lid R B).symm.injective
  ext; simp

Goal state after:
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝⁷ : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁶ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁵ : (i : ι) → FunLike (H i) (G i) C
inst✝⁴ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝³ : IsDirectedOrder ι
inst✝² : Nonempty ι
inst✝¹ : (i : ι) → AddMonoidWithOne (G i)
inst✝ : ∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass (T h) (G i) (G j)
n : ℕ
⊢ ⟦⟨Classical.arbitrary ι, ↑(n + 1)⟩⟧ = ⟦⟨Classical.arbitrary ι, ↑n⟩⟧ + ⟦⟨Classical.arbitrary ι, 1⟩⟧

Tactic:
Nat.cast_succ,

Goal state after:
R : Type u_1
ι : Type u_2
inst✝⁷ : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁶ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁵ : (i : ι) → FunLike (H i) (G i) C
inst✝⁴ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝³ : IsDirectedOrder ι
inst✝² : Nonempty ι
inst✝¹ : (i : ι) → AddMonoidWithOne (G i)
inst✝ : ∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass (T h) (G i) (G j)
n : ℕ
⊢ ⟦⟨Classical.arbitrary ι, ↑n + 1⟩⟧ = ⟦⟨Classical.arbitrary ι, ↑n⟩⟧ + ⟦⟨Classical.arbitrary ι, 1⟩⟧
Module: Mathlib.Algebra.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
M : Type u_4
N : Type u_5
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module ℚ≥0 M
inst✝³ : AddCommMonoid N
inst✝² : Module ℚ≥0 N
F : Type u_6
inst✝¹ : FunLike F M N
inst✝ : LinearMapClass F ℚ≥0 M N
g : F
f : ι → M
s : Finset ι
⊢ g (𝔼 i ∈ s, f i) = 𝔼 i ∈ s, g (f i)

Tactic:
by simp only [expect, map_smul, map_sum]

Goal state after:
Module: Mathlib.Algebra.Group.EvenFunction

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝² : AddCommGroup β
inst✝¹ : IsAddTorsionFree β
f : α → β
inst✝ : Neg α
he : Function.Even f
ho : Function.Odd f
r : α
⊢ -f r = f r

Tactic:
← ho,

Goal state after:
α : Type u_3
β : Type u_4
inst✝² : AddCommGroup β
inst✝¹ : IsAddTorsionFree β
f : α → β
inst✝ : Neg α
he : Function.Even f
ho : Function.Odd f
r : α
⊢ f (-r) = f r
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hi₀ : 0 ≤ i
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ n % a + a * (n / a + 1) = n + a

Tactic:
mul_add,

Goal state after:
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hi₀ : 0 ≤ i
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ n % a + (a * (n / a) + a * 1) = n + a
Module: Mathlib.Algebra.BigOperators.Group.Finset.Powerset

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
a : α
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
ha : a ∉ s
f : Finset α → β
⊢ Disjoint s.powerset (image (insert a) s.powerset)

Tactic:
· aesop (add simp [disjoint_left, insert_subset_iff])

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

Goal state before:
pp: n : ℕ
s : Multiset ℕ
h : ∀ x ∈ s, x ≡ 1 [MOD n]
⊢ s.prod ≡ 1 [MOD n]

Tactic:
by
  simpa using multisetProd_map_one h

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

Goal state before:
pp: n : ℤ
s : Multiset ℤ
h : ∀ x ∈ s, x ≡ 1 [ZMOD n]
⊢ s.prod ≡ 1 [ZMOD n]

Tactic:
by
  simpa using multisetProd_map_one h

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
f : M →ₗ[R] N
h : IsBaseChange S f
Q : Type u_3
inst✝³ : AddCommMonoid Q
inst✝² : Module S Q
inst✝¹ : Module R Q
inst✝ : IsScalarTower R S Q
g : M →ₗ[R] Q
x : M
⊢ (h.lift g) (f x) = g x

Tactic:
have hF : ∀ (s : S) (m : M), h.lift g (s • f m) = s • g m := h.lift_eq _
  convert! hF 1 x <;> rw [one_smul]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
a b₁✝ b₁ : α
h : (fun b ↦ s(a, b)) b₁✝ = (fun b ↦ s(a, b)) b₁
⊢ b₁✝ = b₁

Tactic:
by
    simp only [Sym2.eq, Sym2.rel_iff', Prod.mk.injEq, true_and, Prod.swap_prod_mk] at h
    obtain rfl | ⟨rfl, rfl⟩ := h <;> rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f g : α → β
s : Sym2 α
h : ∀ x ∈ s, f x = g x
y : β
⊢ (∃ a ∈ s, f a = y) ↔ ∃ a ∈ s, g a = y

Tactic:
constructor <;>
    · rintro ⟨w, hw, rfl⟩
      exact ⟨w, hw, by simp [hw, h]⟩

Goal state after:
Module: Mathlib.Data.Opposite

Goal state before:
pp: α : Sort u
X : Type v
inst✝ : Small.{u, v} X
⊢ Small.{u, v} Xᵒᵖ

Tactic:
obtain ⟨S, ⟨e⟩⟩ := Small.equiv_small (α := X)

Goal state after:
α : Sort u
X : Type v
inst✝ : Small.{u, v} X
S : Type u
e : X ≃ S
⊢ Small.{u, v} Xᵒᵖ
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
⊢ Set.range diag = diagSet

Tactic:
by
  ext ⟨a, b⟩; simp [diag, eq_comm]

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
S : Type v₃
inst✝¹³ : CommSemiring R
inst✝¹² : CommSemiring S
inst✝¹¹ : Algebra R S
R' : Type u_6
S' : Type u_7
inst✝¹⁰ : CommSemiring R'
inst✝⁹ : CommSemiring S'
inst✝⁸ : Algebra R R'
inst✝⁷ : Algebra S S'
inst✝⁶ : Algebra R' S'
inst✝⁵ : Algebra R S'
inst✝⁴ : IsScalarTower R R' S'
inst✝³ : IsScalarTower R S S'
inst✝² : IsPushout R S R' S'
A : Type u_8
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : S →ₐ[R] A
g : R' →ₐ[R] A
H : ∀ (x : S) (y : R'), f x * g y = g y * f x
x : S
⊢ (pushoutDesc S' f g H) ((algebraMap S S') x) = f x

Tactic:
by
  simp [Algebra.pushoutDesc_apply]

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

Goal state before:
pp: C : Type u
inst✝ : CategoryStruct.{v, u} C
ι : Type u'
X : ι → C
P : ObjectProperty C
h : ∀ (i : ι), P (X i)
⊢ ofObj X ≤ P

Tactic:
rintro _ ⟨i⟩; exact h i

Goal state after: