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

Goal state before:
pp: case refine_3
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
p q : Multiset (Associates α)
s t : Multiset α
hs : ∀ a ∈ map (Quot.mk ⇑(Associated.setoid α)) t, Irreducible a
ht : ∀ a ∈ map (Quot.mk ⇑(Associated.setoid α)) s, Irreducible a
eq : (map Associates.mk t).prod = (map Associates.mk s).prod
eq' : Quot.mk ⇑(Associated.setoid α) = Associates.mk
⊢ t.prod ~ᵤ s.prod

Tactic:
prod_mk,

Goal state after:
case refine_3
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
p q : Multiset (Associates α)
s t : Multiset α
hs : ∀ a ∈ map (Quot.mk ⇑(Associated.setoid α)) t, Irreducible a
ht : ∀ a ∈ map (Quot.mk ⇑(Associated.setoid α)) s, Irreducible a
eq : Associates.mk t.prod = (map Associates.mk s).prod
eq' : Quot.mk ⇑(Associated.setoid α) = Associates.mk
⊢ t.prod ~ᵤ s.prod
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: case refine_3
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
p q : Multiset (Associates α)
s t : Multiset α
hs : ∀ a ∈ map (Quot.mk ⇑(Associated.setoid α)) t, Irreducible a
ht : ∀ a ∈ map (Quot.mk ⇑(Associated.setoid α)) s, Irreducible a
eq : Associates.mk t.prod = (map Associates.mk s).prod
eq' : Quot.mk ⇑(Associated.setoid α) = Associates.mk
⊢ t.prod ~ᵤ s.prod

Tactic:
prod_mk,

Goal state after:
case refine_3
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
p q : Multiset (Associates α)
s t : Multiset α
hs : ∀ a ∈ map (Quot.mk ⇑(Associated.setoid α)) t, Irreducible a
ht : ∀ a ∈ map (Quot.mk ⇑(Associated.setoid α)) s, Irreducible a
eq : Associates.mk t.prod = Associates.mk s.prod
eq' : Quot.mk ⇑(Associated.setoid α) = Associates.mk
⊢ t.prod ~ᵤ s.prod
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : n ∈ p.support
⊢ p.content ∣ p.coeff n

Tactic:
apply Finset.gcd_dvd h

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

Goal state before:
pp: T : Type w
inst✝⁶ : CommRing T
p : T[X]
S : Type u_1
S' : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : Algebra T S
inst✝² : CommRing S'
inst✝¹ : IsDomain S'
inst✝ : Algebra T S'
hp : map (algebraMap T S') p = 0 → map (algebraMap T S) p = 0
f : S →ₐ[T] S'
x : S
hx : map (algebraMap T S) p ≠ 0 ∧ (aeval x) p = 0
⊢ map (algebraMap T S') p ≠ 0 ∧ (aeval (f x)) p = 0

Tactic:
aeval_algHom,

Goal state after:
T : Type w
inst✝⁶ : CommRing T
p : T[X]
S : Type u_1
S' : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : Algebra T S
inst✝² : CommRing S'
inst✝¹ : IsDomain S'
inst✝ : Algebra T S'
hp : map (algebraMap T S') p = 0 → map (algebraMap T S) p = 0
f : S →ₐ[T] S'
x : S
hx : map (algebraMap T S) p ≠ 0 ∧ (aeval x) p = 0
⊢ map (algebraMap T S') p ≠ 0 ∧ (f.comp (aeval x)) p = 0
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: case refine_1
k : Type y
inst✝ : Field k
p q : k[X]
hq : q.natDegree ≠ 0
hq' : q.leadingCoeff ≠ 0
⊢ q.leadingCoeff * q.leadingCoeff⁻¹ = 1

Tactic:
mul_inv_eq_one₀ hq'

Goal state after:
case refine_1
k : Type y
inst✝ : Field k
p q : k[X]
hq : q.natDegree ≠ 0
hq' : q.leadingCoeff ≠ 0
⊢ q.leadingCoeff = q.leadingCoeff
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
⊢ Associates.mk p ∈ (Associates.mk a).factors ↔ p ∣ a

Tactic:
constructor
  · rw [← mk_dvd_mk]
    apply dvd_of_mem_factors
  · apply mem_factors_of_dvd ha0 hp

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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : NoZeroDivisors R
inst✝ : WfDvdMonoid R
f : R[X]
⊢ WellFounded DvdNotUnit

Tactic:
by
    classical
      refine
        RelHomClass.wellFounded
          (⟨fun p : R[X] =>
              ((if p = 0 then ⊤ else ↑p.degree : WithTop (WithBot ℕ)), p.leadingCoeff), ?_⟩ :
            DvdNotUnit →r Prod.Lex (· < ·) DvdNotUnit)
          (wellFounded_lt.prod_lex ‹WfDvdMonoid R›.wf)
      rintro a b ⟨ane0, ⟨c, ⟨not_unit_c, rfl⟩⟩⟩
      rw [Polynomial.degree_mul, if_neg ane0]
      split_ifs with hac
      · rw [hac, Polynomial.leadingCoeff_zero]
        apply Prod.Lex.left
        exact WithTop.coe_lt_top _
      have cne0 : c ≠ 0 := right_ne_zero_of_mul hac
      simp only [Polynomial.leadingCoeff_mul]
      by_cases hdeg : c.degree = (0 : ℕ)
      · simp only [hdeg, Nat.cast_zero, add_zero]
        refine Prod.Lex.right _ ⟨?_, ⟨c.leadingCoeff, fun unit_c => not_unit_c ?_, rfl⟩⟩
        · rwa [Ne, Polynomial.leadingCoeff_eq_zero]
        rw [Polynomial.isUnit_iff, Polynomial.eq_C_of_degree_eq_zero hdeg]
        use c.leadingCoeff, unit_c
        rw [Polynomial.leadingCoeff, Polynomial.natDegree_eq_of_degree_eq_some hdeg]
      · apply Prod.Lex.left
        rw [Polynomial.degree_eq_natDegree cne0] at *
        simp only [Nat.cast_inj] at hdeg
        rw [WithTop.coe_lt_coe, Polynomial.degree_eq_natDegree ane0, ← Nat.cast_add, Nat.cast_lt]
        exact lt_add_of_pos_right _ (Nat.pos_of_ne_zero hdeg)

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
f : K[X]
a : K
h : X - C a ∣ f /ₘ (X - C a)
this : derivative f %ₘ (X - C a) = 0
⊢ eval a (derivative f) = 0

Tactic:
modByMonic_X_sub_C_eq_C_eval

Goal state after:
K : Type u_1
inst✝ : Field K
f : K[X]
a : K
h : X - C a ∣ f /ₘ (X - C a)
this : C (eval a (derivative f)) = 0
⊢ eval a (derivative f) = 0
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: case neg.inr
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a b : Associates α
hb : b ≠ 0
p : Associates α
hp : Irreducible p
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
k : ℕ
habk : k ∣ p.count (a * b).factors
ha : ¬a = 0
h : p.count b.factors = 0
⊢ k ∣ p.count a.factors

Tactic:
rw [count_mul ha hb hp, h] at habk

Goal state after:
case neg.inr
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a b : Associates α
hb : b ≠ 0
p : Associates α
hp : Irreducible p
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
k : ℕ
habk : k ∣ p.count a.factors + 0
ha : ¬a = 0
h : p.count b.factors = 0
⊢ k ∣ p.count a.factors
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
k : ℕ
a✝ : Nontrivial α
a0 : α
hz : a0 ≠ 0
ha : Associates.mk a0 ≠ 0
hk : ∀ (p : Associates α), Irreducible p → k ∣ p.count ↑(factors' a0)
p : { a // Irreducible a }
pp : p = ⟨↑p, ⋯⟩
⊢ k ∣ Multiset.count p (factors' a0)

Tactic:
pp,

Goal state after:
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
k : ℕ
a✝ : Nontrivial α
a0 : α
hz : a0 ≠ 0
ha : Associates.mk a0 ≠ 0
hk : ∀ (p : Associates α), Irreducible p → k ∣ p.count ↑(factors' a0)
p : { a // Irreducible a }
pp : p = ⟨↑p, ⋯⟩
⊢ k ∣ Multiset.count ⟨↑p, ⋯⟩ (factors' a0)
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
B : Type u_2
inst✝¹ : Ring B
inst✝ : Algebra R B
f : A →ₐ[R] B
a : A
h : IsAlgebraic R a
p : R[X]
hp : p ≠ 0
ha : (aeval a) p = 0
⊢ (aeval (f a)) p = 0

Tactic:
aeval_algHom,

Goal state after:
R : Type u
A : Type v
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Algebra R A
B : Type u_2
inst✝¹ : Ring B
inst✝ : Algebra R B
f : A →ₐ[R] B
a : A
h : IsAlgebraic R a
p : R[X]
hp : p ≠ 0
ha : (aeval a) p = 0
⊢ (f.comp (aeval a)) p = 0
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: 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]
ne_zero : p ≠ 0
aeval_eq : (aeval ↑x) p = 0
⊢ (↑x)⁻¹ ∈ A

Tactic:
rw [Subalgebra.aeval_coe, Subalgebra.coe_eq_zero] at aeval_eq

Goal state after:
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]
ne_zero : p ≠ 0
aeval_eq : (aeval x) p = 0
⊢ (↑x)⁻¹ ∈ A
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst✝¹ : LinearOrder ι
inst✝ : SuccOrder ι
equiv : (j : ↑(Iic i)) → F ↑j ≃ piLT X ↑j
e : F i⁺ ≃ F i × X i
hi : ¬IsMax i
x : F ↑⟨i⁺, ⋯⟩
⊢ (piEquivSucc equiv e hi ⟨i⁺, ⋯⟩) x ⟨i, ⋯⟩ = (e x).2

Tactic:
simp [piEquivSucc]

Goal state after:
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: case inl.refl
ι✝ : Type u_1
inst✝⁴ : Preorder ι✝
F₁ : ι✝ → Type u_2
F₂ : ι✝ → Type u_3
F✝ : ι✝ → Type u_4
X✝ : ι✝ → Type u_5
f✝ : ⦃i j : ι✝⦄ → i ≤ j → F✝ j → F✝ i
i✝ j : ι✝
h : i✝ ≤ j
ι : 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 ι
equivSucc : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
s t : Set ι
inst✝¹ : WellFoundedLT ι
inst✝ : InverseSystem f
hi : ¬IsMax i
e : PEquivOn f equivSucc (Iic i)
H : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hsj : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hj : ¬IsMax i
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
eq : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp [piEquivSucc]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
hfg : Exact ⇑f ⇑g
h : P → N
hgh : RightInverse h ⇑g
⊢ inverse_of_rightInverse Q hfg hgh ∘ₗ lTensor Q g = (lTensor Q f).range.mkQ

Tactic:
rw [LinearMap.ext_iff]

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
hfg : Exact ⇑f ⇑g
h : P → N
hgh : RightInverse h ⇑g
⊢ ∀ (x : Q ⊗[R] N), (inverse_of_rightInverse Q hfg hgh ∘ₗ lTensor Q g) x = (lTensor Q f).range.mkQ x
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
hfg : Exact ⇑f ⇑g
h : P → N
hgh : RightInverse h ⇑g
⊢ inverse_of_rightInverse Q hfg hgh ∘ₗ rTensor Q g = (rTensor Q f).range.mkQ

Tactic:
rw [LinearMap.ext_iff]

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
hfg : Exact ⇑f ⇑g
h : P → N
hgh : RightInverse h ⇑g
⊢ ∀ (x : N ⊗[R] Q), (inverse_of_rightInverse Q hfg hgh ∘ₗ rTensor Q g) x = (rTensor Q f).range.mkQ x
Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness

Goal state before:
pp: case h
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
x y : M ⊗[R] N
Sx : M →₀ N
hx : x = Sx.sum fun m n ↦ m ⊗ₜ[R] n
Sy : M →₀ N
hy : y = Sy.sum fun m n ↦ m ⊗ₜ[R] n
⊢ x + y = (Sx + Sy).sum fun m n ↦ m ⊗ₜ[R] n

Tactic:
rw [hx, hy]

Goal state after:
case h
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
x y : M ⊗[R] N
Sx : M →₀ N
hx : x = Sx.sum fun m n ↦ m ⊗ₜ[R] n
Sy : M →₀ N
hy : y = Sy.sum fun m n ↦ m ⊗ₜ[R] n
⊢ ((Sx.sum fun m n ↦ m ⊗ₜ[R] n) + Sy.sum fun m n ↦ m ⊗ₜ[R] n) = (Sx + Sy).sum fun m n ↦ m ⊗ₜ[R] n
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
S : Type u_4
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
I : Ideal B
⊢ ((lTensor S A) (↑R (Submodule.subtype I))).range = Submodule.restrictScalars S (Ideal.map includeRight I)

Tactic:
rw [← (Submodule.restrictScalars_injective R _ _).eq_iff]
  exact (I.map_includeRight_eq (R := R) (A := A)).symm

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✝⁶ : Flat R M
N : Type u_1
N' : Type u_2
N'' : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup N'
inst✝³ : AddCommGroup N''
inst✝² : Module R N
inst✝¹ : Module R N'
inst✝ : Module R N''
f : N →ₗ[R] N'
g : N' →ₗ[R] N''
exact : Function.Exact ⇑f ⇑g
π : N' →ₗ[R] N' ⧸ f.range := f.range.mkQ
ι : N' ⧸ f.range →ₗ[R] N'' := g.range.subtype ∘ₗ ↑g.quotKerEquivRange ∘ₗ ↑(f.range.quotEquivOfEq g.ker ⋯)
⊢ Function.Exact ⇑(lTensor M f) ⇑(lTensor M g)

Tactic:
suffices exact1 : Function.Exact (f.lTensor M) (π.lTensor M) by
    rw [show g = ι.comp π from rfl, lTensor_comp]
    exact exact1.comp_injective _ (lTensor_preserves_injective_linearMap ι <| by
      simpa [ι, -Subtype.val_injective] using Subtype.val_injective) (map_zero _)

Goal state after:
R : Type u
M : Type v
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : Flat R M
N : Type u_1
N' : Type u_2
N'' : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup N'
inst✝³ : AddCommGroup N''
inst✝² : Module R N
inst✝¹ : Module R N'
inst✝ : Module R N''
f : N →ₗ[R] N'
g : N' →ₗ[R] N''
exact : Function.Exact ⇑f ⇑g
π : N' →ₗ[R] N' ⧸ f.range := f.range.mkQ
ι : N' ⧸ f.range →ₗ[R] N'' := g.range.subtype ∘ₗ ↑g.quotKerEquivRange ∘ₗ ↑(f.range.quotEquivOfEq g.ker ⋯)
⊢ Function.Exact ⇑(lTensor M f) ⇑(lTensor M π)
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 : ι) → DivisionSemiring (G i)
inst✝² : DivisionSemiring C
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)
inst✝ : ∀ (i : ι), RingHomClass (H i) (G i) C
q : ℚ≥0
x✝² x✝¹ : ι
x✝ : x✝² ≤ x✝¹
x : G x✝²
⊢ (f x✝² x✝¹ x✝) (q • x) = q • (f x✝² x✝¹ x✝) x

Tactic:
simp_rw [NNRat.smul_def, map_mul, map_nnratCast]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Gaps

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
g : α → β
⊢ ((∏ i ∈ range k, g (F.intervalGapsWithin h ?m.56 ?m.57 ↑i.succ).1 / g (F.intervalGapsWithin h ?m.56 ?m.57 ↑i).2) *
        ∏ x ∈ range k, g (F.intervalGapsWithin h a b ↑x).2 / g (F.intervalGapsWithin h a b ↑x).1) *
      (g (F.intervalGapsWithin h a b ↑k).2 / g (F.intervalGapsWithin h a b ↑k).1) =
    g b / g a

pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
g : α → β
⊢ α

pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
g : α → β
⊢ α

Tactic:
← prod_mul_distrib,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
g : α → β
⊢ (∏ x ∈ range k,
        g (F.intervalGapsWithin h ?m.56 ?m.57 ↑x.succ).1 / g (F.intervalGapsWithin h ?m.56 ?m.57 ↑x).2 *
          (g (F.intervalGapsWithin h a b ↑x).2 / g (F.intervalGapsWithin h a b ↑x).1)) *
      (g (F.intervalGapsWithin h a b ↑k).2 / g (F.intervalGapsWithin h a b ↑k).1) =
    g b / g a

α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
g : α → β
⊢ α

α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
g : α → β
⊢ α
Module: Mathlib.Algebra.BigOperators.Ring.Nat

Goal state before:
pp: ι : Type u_1
s : Finset ι
f : ι → ℕ
⊢ (∑ a ∈ s, if ¬Even (f a) then f a % 2 else 0) % 2 = 0 ↔ Even #({x ∈ s | Odd (f x)})

Tactic:
simp +contextual only [Nat.not_even_iff_odd, Nat.odd_iff.mp]

Goal state after:
ι : Type u_1
s : Finset ι
f : ι → ℕ
⊢ (∑ x ∈ s, if Odd (f x) then 1 else 0) % 2 = 0 ↔ Even #({x ∈ s | Odd (f x)})
Module: Mathlib.Algebra.BigOperators.Ring.Nat

Goal state before:
pp: ι : Type u_1
s : Finset ι
f : ι → ℕ
⊢ Even (∑ i ∈ s, f i) ↔ Even #({x ∈ s | Odd (f x)})

Tactic:
by
  rw [← Finset.sum_filter_add_sum_filter_not _ (fun x ↦ Even (f x)), Nat.even_add]
  simp only [Finset.mem_filter, and_imp, imp_self, implies_true, Finset.even_sum, true_iff]
  rw [Nat.even_iff, Finset.sum_nat_mod, Finset.sum_filter]
  simp +contextual only [Nat.not_even_iff_odd, Nat.odd_iff.mp]
  simp_rw [← Finset.sum_filter, ← Nat.even_iff, Finset.card_eq_sum_ones]

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case e_m
R : Type u_1
M : Type v₁
S : Type v₃
inst✝⁴ : AddCommMonoid M
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : Module R M
s : S
x : M
⊢ s • 1 = s

Tactic:
exact mul_one _

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

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

Tactic:
by
  rw [Sym2.eq_swap] at h
  exact left_mem_of_mk_mem_sym2 h

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

Goal state before:
pp: case cons.tail
α : Type u_1
x x' : α
xs : List α
ih : x ∈ xs → map (fun y ↦ s(x, y)) xs <+ xs.sym2
h : Mem x xs
⊢ s(x, x') :: map (fun y ↦ s(x, y)) xs <+ map (fun y ↦ s(x', y)) xs ++ xs.sym2

Tactic:
← singleton_append

Goal state after:
case cons.tail
α : Type u_1
x x' : α
xs : List α
ih : x ∈ xs → map (fun y ↦ s(x, y)) xs <+ xs.sym2
h : Mem x xs
⊢ [s(x, x')] ++ map (fun y ↦ s(x, y)) xs <+ map (fun y ↦ s(x', y)) xs ++ xs.sym2
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
s : Finset α
a : α
⊢ (∀ b ∈ Sym2.diag a, b ∈ s) ↔ a ∈ s

Tactic:
rw [← mem_sym2_iff]

Goal state after:
α : Type u_1
s : Finset α
a : α
⊢ Sym2.diag a ∈ s.sym2 ↔ a ∈ s
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case refine_1
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 :
  ∀ (Q : Type (max v₁ v₂ v₃)) [inst : AddCommMonoid Q] [inst_1 : Module R Q] [inst_2 : Module S Q]
    [inst_3 : IsScalarTower R S Q] (g : M →ₗ[R] Q), ∃! g', ↑R g' ∘ₗ f = g
g : N →ₗ[S] ULift.{v₂, max v₁ v₃} (S ⊗[R] M)
f' : S ⊗[R] M →ₗ[R] N := TensorProduct.lift (↑R ((Algebra.ofId S (Module.End S (M →ₗ[R] N))).toLinearMap.flip f))
f'' : S ⊗[R] M →ₗ[S] N := { toAddHom := f'.toAddHom, map_smul' := ⋯ }
hg : ∀ (x : M), g (f x) = ↑ULift.moduleEquiv.symm (((mk R S M) 1) x)
⊢ f'' ∘ₗ ↑ULift.moduleEquiv ∘ₗ g = LinearMap.id

Tactic:
rw [← LinearMap.cancel_left (ULift.moduleEquiv : ULift.{max v₁ v₃} N ≃ₗ[S] N).symm.injective]

Goal state after:
case refine_1
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 :
  ∀ (Q : Type (max v₁ v₂ v₃)) [inst : AddCommMonoid Q] [inst_1 : Module R Q] [inst_2 : Module S Q]
    [inst_3 : IsScalarTower R S Q] (g : M →ₗ[R] Q), ∃! g', ↑R g' ∘ₗ f = g
g : N →ₗ[S] ULift.{v₂, max v₁ v₃} (S ⊗[R] M)
f' : S ⊗[R] M →ₗ[R] N := TensorProduct.lift (↑R ((Algebra.ofId S (Module.End S (M →ₗ[R] N))).toLinearMap.flip f))
f'' : S ⊗[R] M →ₗ[S] N := { toAddHom := f'.toAddHom, map_smul' := ⋯ }
hg : ∀ (x : M), g (f x) = ↑ULift.moduleEquiv.symm (((mk R S M) 1) x)
⊢ ↑ULift.moduleEquiv.symm ∘ₗ f'' ∘ₗ ↑ULift.moduleEquiv ∘ₗ g = ↑ULift.moduleEquiv.symm ∘ₗ LinearMap.id
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
_hz : z ∈ List.sym n (x :: xs)
hz' : x ::ₛ z ∈ List.sym (n + 1) xs
⊢ False

Tactic:
have := first_mem_of_cons_mem_sym 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
this : x ∈ xs
⊢ False
Module: Mathlib.Data.Opposite

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

Tactic:
exact ⟨S, ⟨equivToOpposite.symm.trans e⟩⟩

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

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
X Y X' Y' : V
f : X ⟶ Y
g : X' ⟶ Y'
hX : X = X'
hY : Y = Y'
⊢ homOfEq f hX hY ≍ g ↔ f ≍ g

Tactic:
by
  cases hX; cases hY; rfl

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

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
X Y X' Y' : V
f : X ⟶ Y
g : X' ⟶ Y'
hX : X' = X
hY : Y' = Y
⊢ f ≍ homOfEq g hX hY ↔ f ≍ g

Tactic:
by
  cases hX; cases hY; rfl

Goal state after:
Module: Mathlib.CategoryTheory.Functor.FullyFaithful

Goal state before:
pp: case mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u_1
inst✝ : Category.{v_1, u_1} E
X✝ Y✝ : C
F : C ⥤ D
X Y Z : C
hF : F.FullyFaithful
this : F.Faithful
f₁ : {X Y : C} → (F.obj X ⟶ F.obj Y) → (X ⟶ Y)
hf₁ : ∀ {X Y : C} (f : F.obj X ⟶ F.obj Y), F.map (f₁ f) = f
preimage_map✝¹ : ∀ {X Y : C} (f : X ⟶ Y), f₁ (F.map f) = f
f₂ : {X Y : C} → (F.obj X ⟶ F.obj Y) → (X ⟶ Y)
hf₂ : ∀ {X Y : C} (f : F.obj X ⟶ F.obj Y), F.map (f₂ f) = f
preimage_map✝ : ∀ {X Y : C} (f : X ⟶ Y), f₂ (F.map f) = f
x✝² x✝¹ : C
x✝ : F.obj x✝² ⟶ F.obj x✝¹
⊢ F.map (f₁ x✝) = F.map (f₂ x✝)

Tactic:
hf₁,

Goal state after:
case mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u_1
inst✝ : Category.{v_1, u_1} E
X✝ Y✝ : C
F : C ⥤ D
X Y Z : C
hF : F.FullyFaithful
this : F.Faithful
f₁ : {X Y : C} → (F.obj X ⟶ F.obj Y) → (X ⟶ Y)
hf₁ : ∀ {X Y : C} (f : F.obj X ⟶ F.obj Y), F.map (f₁ f) = f
preimage_map✝¹ : ∀ {X Y : C} (f : X ⟶ Y), f₁ (F.map f) = f
f₂ : {X Y : C} → (F.obj X ⟶ F.obj Y) → (X ⟶ Y)
hf₂ : ∀ {X Y : C} (f : F.obj X ⟶ F.obj Y), F.map (f₂ f) = f
preimage_map✝ : ∀ {X Y : C} (f : X ⟶ Y), f₂ (F.map f) = f
x✝² x✝¹ : C
x✝ : F.obj x✝² ⟶ F.obj x✝¹
⊢ x✝ = F.map (f₂ x✝)
Module: Mathlib.Combinatorics.Quiver.Push

Goal state before:
pp: case h_obj
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
⊢ ∀ (X : V), (of σ ⋙q lift σ φ τ h).obj X = φ.obj X

Tactic:
rintro X

Goal state after:
case h_obj
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X : V
⊢ (of σ ⋙q lift σ φ τ h).obj X = φ.obj X