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

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

Tactic:
intro a

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a✝ : Associates α
h : ¬a✝ = 0
a : α
⊢ ∀ (b : α), a ≈ b → (fun x ↦ ↑(factors' a)) ≍ fun x ↦ ↑(factors' b)
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:
rw [eq, factors_mul]; exact le_add_of_nonneg_right bot_le

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

Goal state before:
pp: case neg
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : IsDomain A
inst✝ : DecidableEq B
p : A[X]
f : A →+* B
hf : Function.Injective ⇑f
b : B
hp0 : ¬p = 0
⊢ count b (Multiset.map (⇑f) p.roots) ≤ rootMultiplicity b (map f p)

Tactic:
· exact count_map_roots ((Polynomial.map_ne_zero_iff hf).mpr hp0) b

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
⊢ Prod.Lex (fun x1 x2 ↦ x1 < x2) DvdNotUnit (↑a.degree, a.leadingCoeff)
    (↑(a.degree + c.degree), a.leadingCoeff * c.leadingCoeff)

Tactic:
by_cases hdeg : c.degree = (0 : ℕ)

Goal state after:
case pos
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.degree = ↑0
⊢ Prod.Lex (fun x1 x2 ↦ x1 < x2) DvdNotUnit (↑a.degree, a.leadingCoeff)
    (↑(a.degree + c.degree), a.leadingCoeff * c.leadingCoeff)

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.degree = ↑0
⊢ Prod.Lex (fun x1 x2 ↦ x1 < x2) DvdNotUnit (↑a.degree, a.leadingCoeff)
    (↑(a.degree + c.degree), a.leadingCoeff * c.leadingCoeff)
Module: Mathlib.RingTheory.Polynomial.UniqueFactorization

Goal state before:
pp: case zero
σ : Type v
D : Type u
inst✝² : CommRing D
inst✝¹ : UniqueFactorizationMonoid D
inst✝ : Finite σ
this : Fintype σ
⊢ UniqueFactorizationMonoid (MvPolynomial (Fin 0) D)

Tactic:
| zero =>

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

Goal state before:
pp: σ : Type v
D : Type u
inst✝¹ : CommRing D
inst✝ : UniqueFactorizationMonoid D
d : ℕ
⊢ ∀ (a : MvPolynomial σ D), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ Associated f.prod a

Tactic:
intro a

Goal state after:
σ : Type v
D : Type u
inst✝¹ : CommRing D
inst✝ : UniqueFactorizationMonoid D
d : ℕ
a : MvPolynomial σ D
⊢ a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ Associated f.prod a
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: case zero
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
a : Associates α
⊢ (a ^ 0).factors = 0 • a.factors

Tactic:
| zero =>

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

Goal state before:
pp: case zero
α : Type u_1
inst✝⁴ : CommMonoidWithZero α
inst✝³ : UniqueFactorizationMonoid α
inst✝² : DecidableEq (Associates α)
inst✝¹ : (p : Associates α) → Decidable (Irreducible p)
inst✝ : Nontrivial α
a : Associates α
ha : a ≠ 0
p : Associates α
hp : Irreducible p
⊢ p.count (a ^ 0).factors = 0 * p.count a.factors

Tactic:
| zero =>

Goal state after:
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
r : A
f : R[X]
H : IsAlgebraic R ((aeval r) f)
hf : Transcendental R f
⊢ IsAlgebraic R r

Tactic:
by
  contrapose H
  exact Transcendental.aeval_of_transcendental H hf

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
inst✝¹ : Nontrivial R
M : Submonoid R
inst✝ : IsLocalization M S
x : S
⊢ IsAlgebraic R x

Tactic:
by
    obtain rfl | hx := eq_or_ne x 0
    · exact isAlgebraic_zero
    have ⟨⟨r, m⟩, h⟩ := surj M x
    refine ⟨C m.1 * X - C r, fun eq ↦ hx ?_, by simpa [sub_eq_zero, mul_comm x] using h⟩
    rwa [← eq_mk'_iff_mul_eq, show r = 0 by simpa using congr(coeff $eq 0), mk'_zero] at h

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

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommSemiring R
ι : Type u_2
inst✝⁶ : DecidableEq ι
inst✝⁵ : Preorder ι
G : ι → Type u_3
inst✝⁴ : (i : ι) → AddCommMonoid (G i)
inst✝³ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
x✝⁴ x✝³ x✝² : ι
x✝¹ : x✝² ≤ x✝³
x✝ : x✝³ ≤ x✝⁴
x : G x✝² ⊗[R] M
⊢ (LinearMap.rTensor M (f x✝³ x✝⁴ x✝)) ((LinearMap.rTensor M (f x✝² x✝³ x✝¹)) x) = (LinearMap.rTensor M (f x✝² x✝⁴ ⋯)) x

Tactic:
convert! ← (LinearMap.rTensor_comp_apply M _ _ x).symm

Goal state after:
case e'_3
R : Type u_1
inst✝⁷ : CommSemiring R
ι : Type u_2
inst✝⁶ : DecidableEq ι
inst✝⁵ : Preorder ι
G : ι → Type u_3
inst✝⁴ : (i : ι) → AddCommMonoid (G i)
inst✝³ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
x✝⁴ x✝³ x✝² : ι
x✝¹ : x✝² ≤ x✝³
x✝ : x✝³ ≤ x✝⁴
x : G x✝² ⊗[R] M
⊢ f x✝³ x✝⁴ x✝ ∘ₗ f x✝² x✝³ x✝¹ = f x✝² x✝⁴ ⋯
Module: Mathlib.Algebra.Colimit.TensorProduct

Goal state before:
pp: R : Type u_1
M : Type u_2
P : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
N : { x // x.FG }
x y : ↥↑N ⊗[R] M
eq✝ :
  (Module.DirectLimit.of R { N // N.FG } (fun i ↦ ↥↑i ⊗[R] M)
        (fun i j h ↦ LinearMap.rTensor M (Module.fgSystem R P i j h)) N)
      x =
    (Module.DirectLimit.of R { N // N.FG } (fun i ↦ ↥↑i ⊗[R] M)
        (fun i j h ↦ LinearMap.rTensor M (Module.fgSystem R P i j h)) N)
      y
N' : { N // N.FG }
le : N ≤ N'
eq : (LinearMap.rTensor M (Module.fgSystem R P N N' le)) x = (LinearMap.rTensor M (Module.fgSystem R P N N' le)) y
⊢ ∃ N', N'.FG ∧ ∃ (h : ↑N ≤ N'), (LinearMap.rTensor M (inclusion h)) x = (LinearMap.rTensor M (inclusion h)) y

Tactic:
exact ⟨_, N'.2, le, eq⟩

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

Goal state before:
pp: case zero
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
⊢ ∃ a, (lTensor Q g) a = 0

Tactic:
| zero =>

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

Goal state before:
pp: case zero
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
⊢ ∃ a, (rTensor Q g) a = 0

Tactic:
| zero =>

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

Goal state before:
pp: σ : Type u
R : Type v
inst✝ : CommSemiring R
p m✝ : ℕ
s : Set (σ →₀ ℕ)
hs : IsUpperSet s
x y : MvPolynomial σ R
hy : y ∈ (restrictSupport R s).carrier
m : σ →₀ ℕ
hm : ¬∑ x_1 ∈ Finset.antidiagonal m, coeff x_1.1 x * coeff x_1.2 y = 0
i j : σ →₀ ℕ
hij : (i, j) ∈ Finset.antidiagonal m
e : coeff (i, j).1 x * coeff (i, j).2 y ≠ 0
⊢ j ≤ m

Tactic:
by simp_all [eq_comm]

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

Goal state before:
pp: case zero
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
⊢ ∃ S, 0 = (Multiset.map (fun i ↦ i.1 ⊗ₜ[R] i.2) S).sum

Tactic:
| zero =>

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

Goal state before:
pp: case zero
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
⊢ ∃ S, 0 = S.sum fun m n ↦ m ⊗ₜ[R] n

Tactic:
| zero =>

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:
| zero =>

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

Goal state before:
pp: case a.refine_4.tmul.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)))
a : A
b : B
⊢ ∃ y,
    (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) y =
      a ⊗ₜ[R] b • (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) 0

Tactic:
| zero =>

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

Goal state before:
pp: case a.refine_4.tmul.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
x✝ : A ⊗[R] B
hx : x✝ ∈ ↑(Submodule.restrictScalars R (Submodule.span (A ⊗[R] B) (⇑includeLeft '' ↑I)))
a : A
b : B
x : ↥(Submodule.restrictScalars R I)
y : B
⊢ ∃ y_1,
    (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) y_1 =
      a ⊗ₜ[R] b • (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) (x ⊗ₜ[R] y)

Tactic:
use (a • x) ⊗ₜ[R] (b * y)
          simp only [smul_eq_mul]
          with_unfolding_all rfl

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

Goal state before:
pp: case a.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
⊢ (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) 0 ∈ ↑(Submodule.restrictScalars R (map includeLeft I))

Tactic:
| zero =>

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:
| zero =>

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

Goal state before:
pp: case a.refine_4.tmul.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)))
a : A
b : B
⊢ ∃ y,
    (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) y =
      a ⊗ₜ[R] b • (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) 0

Tactic:
| zero =>

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

Goal state before:
pp: case a.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
⊢ (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) 0 ∈ ↑(Submodule.restrictScalars R (map includeRight I))

Tactic:
| zero =>

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

Goal state before:
pp: 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
a : A
b : ↥(Submodule.restrictScalars R I)
this : a ⊗ₜ[R] ↑b = a ⊗ₜ[R] 1 * 1 ⊗ₜ[R] ↑b
⊢ 1 ⊗ₜ[R] ↑b ∈ map includeRight I

Tactic:
apply Ideal.mem_map_of_mem includeRight

Goal state after:
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
a : A
b : ↥(Submodule.restrictScalars R I)
this : a ⊗ₜ[R] ↑b = a ⊗ₜ[R] 1 * 1 ⊗ₜ[R] ↑b
⊢ ↑b ∈ I
Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness

Goal state before:
pp: case zero
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
⊢ ∃ k m n, 0 = ∑ j, m j ⊗ₜ[R] n j

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Algebra.Central.TensorProduct

Goal state before:
pp: case zero
K : Type u_1
B : Type u_2
C : Type u_3
inst✝⁴ : CommSemiring K
inst✝³ : Semiring B
inst✝² : Semiring C
inst✝¹ : Algebra K B
inst✝ : Algebra K C
b : B
hb0 : ∀ (b_1 : B), b_1 * b = b * b_1
⊢ 0 * includeLeft b = includeLeft b * 0

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Algebra.Central.TensorProduct

Goal state before:
pp: case zero
K : Type u_1
B : Type u_2
C : Type u_3
inst✝⁴ : CommSemiring K
inst✝³ : Semiring B
inst✝² : Semiring C
inst✝¹ : Algebra K B
inst✝ : Algebra K C
c : C
hc0 : ∀ (b : C), b * c = c * b
⊢ 0 * includeRight c = includeRight c * 0

Tactic:
| zero =>

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
S : Type u_4
inst✝² : Semiring S
inst✝¹ : Algebra R S
inst✝ : Flat R S
ι : Type u_5
v : ι → M
hv : LinearIndependent R v
⊢ LinearIndependent S fun x ↦ 1 ⊗ₜ[R] v x

Tactic:
classical rw [LinearIndependent, ← LinearMap.coe_restrictScalars R,
    Finsupp.linearCombination_one_tmul]

Goal state after:
R : Type u
M : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Semiring S
inst✝¹ : Algebra R S
inst✝ : Flat R S
ι : Type u_5
v : ι → M
hv : LinearIndependent R v
⊢ Injective ⇑(lTensor S (Finsupp.linearCombination R v) ∘ₗ ↑(finsuppScalarRight R R S ι).symm)
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: ι : Type u_2
inst✝⁶ : Preorder ι
G : ι → Type u_3
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✝⁴ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝³ : IsDirectedOrder ι
inst✝² : Nonempty ι
inst✝¹ : (i : ι) → One (G i)
inst✝ : ∀ (i j : ι) (h : i ≤ j), OneHomClass (T h) (G i) (G j)
x : (i : ι) × G i
⊢ ⟦x⟧ = 1 ↔ ∃ i, ∃ (h : x.fst ≤ i), (f x.fst i h) x.snd = 1

Tactic:
rw [one_def x.1, Quotient.eq]

Goal state after:
ι : Type u_2
inst✝⁶ : Preorder ι
G : ι → Type u_3
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✝⁴ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝³ : IsDirectedOrder ι
inst✝² : Nonempty ι
inst✝¹ : (i : ι) → One (G i)
inst✝ : ∀ (i j : ι) (h : i ≤ j), OneHomClass (T h) (G i) (G j)
x : (i : ι) × G i
⊢ (setoid f) x ⟨x.fst, 1⟩ ↔ ∃ i, ∃ (h : x.fst ≤ i), (f x.fst i h) x.snd = 1
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' N'' : Type v'⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : AddCommGroup N'']
      [inst_3 : Module R N] [inst_4 : Module R N'] [inst_5 : Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄,
      Function.Exact ⇑f ⇑g → Function.Exact ⇑(lTensor M f) ⇑(lTensor M g)

Tactic:
by
  refine ⟨fun _ ↦ lTensor_exact _, fun H ↦ iff_lTensor_preserves_injective_linearMap'.mpr
    fun N' N'' _ _ _ _ L hL ↦ LinearMap.ker_eq_bot |>.mp <| eq_bot_iff |>.mpr
      fun x (hx : _ = 0) ↦ ?_⟩
  simpa [Eq.comm] using @H PUnit N' N'' _ _ _ _ _ _ 0 L (fun x ↦ by
    simp_rw [Set.mem_range, LinearMap.zero_apply, exists_const]
    exact (L.map_eq_zero_iff hL).trans eq_comm) x |>.mp hx

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

Goal state before:
pp: α : Type u_2
inst✝¹ : Fintype α
s t : Finset α
inst✝ : DecidableEq α
h : #s = #t
⊢ (s \ t).dens + t.dens = (t \ s).dens + t.dens

Tactic:
dens_sdiff_add_dens,

Goal state after:
α : Type u_2
inst✝¹ : Fintype α
s t : Finset α
inst✝ : DecidableEq α
h : #s = #t
⊢ (s ∪ t).dens = (t \ s).dens + t.dens
Module: Mathlib.Algebra.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Module ℚ≥0 M
s : Finset ι
inst✝ : DecidableEq ι
i : ι
f : (j : ι) → i = j → M
⊢ (𝔼 j ∈ s, if h : i = j then f j h else 0) = if i ∈ s then (↑(#s))⁻¹ • f i ⋯ else 0

Tactic:
split_ifs <;> simp [expect, *]

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Module ℚ≥0 M
s : Finset ι
inst✝ : DecidableEq ι
i : ι
f : (j : ι) → j = i → M
⊢ (𝔼 j ∈ s, if h : j = i then f j h else 0) = if i ∈ s then (↑(#s))⁻¹ • f i ⋯ else 0

Tactic:
split_ifs <;> simp [expect, *]

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Module ℚ≥0 M
s : Finset ι
inst✝ : DecidableEq ι
i : ι
f : ι → M
⊢ (𝔼 j ∈ s, if i = j then f j else 0) = if i ∈ s then (↑(#s))⁻¹ • f i else 0

Tactic:
split_ifs <;> simp [expect, *]

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Module ℚ≥0 M
s : Finset ι
inst✝ : DecidableEq ι
i : ι
f : ι → M
⊢ (𝔼 j ∈ s, if j = i then f j else 0) = if i ∈ s then (↑(#s))⁻¹ • f i else 0

Tactic:
split_ifs <;> simp [expect, *]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Neg α
γ : Type u_3
inst✝ : Neg β
f : β → γ
hf : Function.Even f
g : α → β
hg : Function.Odd g
⊢ Function.Even (f ∘ g)

Tactic:
intro a

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Neg α
γ : Type u_3
inst✝ : Neg β
f : β → γ
hf : Function.Even f
g : α → β
hg : Function.Odd g
a : α
⊢ (f ∘ g) (-a) = (f ∘ g) a
Module: Mathlib.Algebra.Group.EvenFunction

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Neg α
γ : Type u_3
inst✝¹ : Neg β
inst✝ : Neg γ
f : β → γ
hf : Function.Odd f
g : α → β
hg : Function.Odd g
⊢ Function.Odd (f ∘ g)

Tactic:
intro a

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Neg α
γ : Type u_3
inst✝¹ : Neg β
inst✝ : Neg γ
f : β → γ
hf : Function.Odd f
g : α → β
hg : Function.Odd g
a : α
⊢ (f ∘ g) (-a) = -(f ∘ g) a
Module: Mathlib.Algebra.Group.EvenFunction

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Neg α
inst✝ : Add β
f g : α → β
hf : Function.Even f
hg : Function.Even g
⊢ Function.Even (f + g)

Tactic:
intro a

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Neg α
inst✝ : Add β
f g : α → β
hf : Function.Even f
hg : Function.Even g
a : α
⊢ (f + g) (-a) = (f + g) a
Module: Mathlib.Algebra.Group.EvenFunction

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Neg α
inst✝ : SubtractionCommMonoid β
f g : α → β
hf : Function.Odd f
hg : Function.Odd g
⊢ Function.Odd (f + g)

Tactic:
intro a

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Neg α
inst✝ : SubtractionCommMonoid β
f g : α → β
hf : Function.Odd f
hg : Function.Odd g
a : α
⊢ (f + g) (-a) = -(f + g) a
Module: Mathlib.Algebra.Group.EvenFunction

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Neg α
γ : Type u_3
f : α → β
g : α → γ
inst✝ : SMul β γ
hf : Function.Even f
hg : Function.Even g
⊢ Function.Even (f • g)

Tactic:
intro a

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Neg α
γ : Type u_3
f : α → β
g : α → γ
inst✝ : SMul β γ
hf : Function.Even f
hg : Function.Even g
a : α
⊢ (f • g) (-a) = (f • g) a
Module: Mathlib.Algebra.Group.EvenFunction

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Neg α
γ : Type u_3
f : α → β
g : α → γ
inst✝² : Monoid β
inst✝¹ : AddGroup γ
inst✝ : DistribMulAction β γ
hf : Function.Even f
hg : Function.Odd g
⊢ Function.Odd (f • g)

Tactic:
intro a

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : Neg α
γ : Type u_3
f : α → β
g : α → γ
inst✝² : Monoid β
inst✝¹ : AddGroup γ
inst✝ : DistribMulAction β γ
hf : Function.Even f
hg : Function.Odd g
a : α
⊢ (f • g) (-a) = -(f • g) a
Module: Mathlib.Algebra.Group.EvenFunction

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Neg α
γ : Type u_3
f : α → β
g : α → γ
inst✝² : Ring β
inst✝¹ : AddCommGroup γ
inst✝ : Module β γ
hf : Function.Odd f
hg : Function.Even g
⊢ Function.Odd (f • g)

Tactic:
intro a

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : Neg α
γ : Type u_3
f : α → β
g : α → γ
inst✝² : Ring β
inst✝¹ : AddCommGroup γ
inst✝ : Module β γ
hf : Function.Odd f
hg : Function.Even g
a : α
⊢ (f • g) (-a) = -(f • g) a
Module: Mathlib.Algebra.Group.EvenFunction

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Neg α
γ : Type u_3
f : α → β
g : α → γ
inst✝² : Ring β
inst✝¹ : AddCommGroup γ
inst✝ : Module β γ
hf : Function.Odd f
hg : Function.Odd g
⊢ Function.Even (f • g)

Tactic:
intro a

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : Neg α
γ : Type u_3
f : α → β
g : α → γ
inst✝² : Ring β
inst✝¹ : AddCommGroup γ
inst✝ : Module β γ
hf : Function.Odd f
hg : Function.Odd g
a : α
⊢ (f • g) (-a) = (f • g) a
Module: Mathlib.Algebra.Group.EvenFunction

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Neg α
γ : Type u_3
g : α → γ
inst✝ : SMul β γ
hg : Function.Even g
r : β
⊢ Function.Even (r • g)

Tactic:
intro a

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Neg α
γ : Type u_3
g : α → γ
inst✝ : SMul β γ
hg : Function.Even g
r : β
a : α
⊢ (r • g) (-a) = (r • g) a
Module: Mathlib.Algebra.Group.EvenFunction

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Neg α
γ : Type u_3
g : α → γ
inst✝² : Monoid β
inst✝¹ : AddGroup γ
inst✝ : DistribMulAction β γ
hg : Function.Odd g
r : β
⊢ Function.Odd (r • g)

Tactic:
intro a

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : Neg α
γ : Type u_3
g : α → γ
inst✝² : Monoid β
inst✝¹ : AddGroup γ
inst✝ : DistribMulAction β γ
hg : Function.Odd g
r : β
a : α
⊢ (r • g) (-a) = -(r • g) a
Module: Mathlib.Algebra.Group.EvenFunction

Goal state before:
pp: α : Type u_1
inst✝¹ : Neg α
R : Type u_3
inst✝ : Mul R
f g : α → R
hf : Function.Even f
hg : Function.Even g
⊢ Function.Even (f * g)

Tactic:
intro a

Goal state after:
α : Type u_1
inst✝¹ : Neg α
R : Type u_3
inst✝ : Mul R
f g : α → R
hf : Function.Even f
hg : Function.Even g
a : α
⊢ (f * g) (-a) = (f * g) a
Module: Mathlib.Algebra.Group.EvenFunction

Goal state before:
pp: α : Type u_1
inst✝² : Neg α
R : Type u_3
inst✝¹ : Mul R
f g : α → R
inst✝ : HasDistribNeg R
hf : Function.Even f
hg : Function.Odd g
⊢ Function.Odd (f * g)

Tactic:
intro a

Goal state after:
α : Type u_1
inst✝² : Neg α
R : Type u_3
inst✝¹ : Mul R
f g : α → R
inst✝ : HasDistribNeg R
hf : Function.Even f
hg : Function.Odd g
a : α
⊢ (f * g) (-a) = -(f * g) a
Module: Mathlib.Algebra.Group.EvenFunction

Goal state before:
pp: α : Type u_1
inst✝² : Neg α
R : Type u_3
inst✝¹ : Mul R
f g : α → R
inst✝ : HasDistribNeg R
hf : Function.Odd f
hg : Function.Even g
⊢ Function.Odd (f * g)

Tactic:
intro a

Goal state after:
α : Type u_1
inst✝² : Neg α
R : Type u_3
inst✝¹ : Mul R
f g : α → R
inst✝ : HasDistribNeg R
hf : Function.Odd f
hg : Function.Even g
a : α
⊢ (f * g) (-a) = -(f * g) a