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

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoidWithZero α
p : Associates α
hp : Irreducible p
l : Multiset { a // Irreducible a }
⊢ (if hp : Irreducible p then BfactorSetMem ⟨p, hp⟩ ↑l else False) ↔ l.Mem ⟨p, hp⟩

Tactic:
split_ifs

Goal state after:
α : Type u_1
inst✝ : CommMonoidWithZero α
p : Associates α
hp : Irreducible p
l : Multiset { a // Irreducible a }
⊢ BfactorSetMem ⟨p, hp⟩ ↑l ↔ l.Mem ⟨p, hp⟩
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : NormalizationMonoid R
a✝ : R[X]
u : R[X]ˣ
h : a✝ ≠ 0
w : Rˣ
h2 : C ↑w = ↑u
⊢ C ↑(normUnit (a✝ * ↑u).leadingCoeff) = ↑u⁻¹ * C ↑(normUnit a✝.leadingCoeff)

Tactic:
leadingCoeff_mul,

Goal state after:
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : NormalizationMonoid R
a✝ : R[X]
u : R[X]ˣ
h : a✝ ≠ 0
w : Rˣ
h2 : C ↑w = ↑u
⊢ C ↑(normUnit (a✝.leadingCoeff * (↑u).leadingCoeff)) = ↑u⁻¹ * C ↑(normUnit a✝.leadingCoeff)
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : NormalizationMonoid R
a✝ : R[X]
u : R[X]ˣ
h : a✝ ≠ 0
w : Rˣ
h2 : C ↑w = ↑u
⊢ C ↑w * C ↑w⁻¹ * C ↑(normUnit a✝.leadingCoeff) = C ↑(normUnit a✝.leadingCoeff)

Tactic:
← C_mul

Goal state after:
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : NormalizationMonoid R
a✝ : R[X]
u : R[X]ˣ
h : a✝ ≠ 0
w : Rˣ
h2 : C ↑w = ↑u
⊢ C (↑w * ↑w⁻¹) * C ↑(normUnit a✝.leadingCoeff) = C ↑(normUnit a✝.leadingCoeff)
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : StrongNormalizationMonoid R
a✝ b✝ : R[X]
hp0 : ¬a✝.leadingCoeff = 0
hq0 : ¬b✝.leadingCoeff = 0
⊢ C ↑(normUnit (a✝ * b✝).leadingCoeff) = C ↑(normUnit a✝.leadingCoeff) * C ↑(normUnit b✝.leadingCoeff)

Tactic:
leadingCoeff_mul,

Goal state after:
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : StrongNormalizationMonoid R
a✝ b✝ : R[X]
hp0 : ¬a✝.leadingCoeff = 0
hq0 : ¬b✝.leadingCoeff = 0
⊢ C ↑(normUnit (a✝.leadingCoeff * b✝.leadingCoeff)) = C ↑(normUnit a✝.leadingCoeff) * C ↑(normUnit b✝.leadingCoeff)
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case neg.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
a✝ : Nontrivial R
n : ℕ
ih : ∀ (p q : R[X]), (p * q).degree < ↑n → Associated (p * q).content (p.content * q.content)
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.primPart.degree + q.primPart.degree = ↑n
⊢ gcd (q.primPart * p.primPart).leadingCoeff (q.primPart * p.primPart).eraseLead.content ∣ 1

Tactic:
leadingCoeff_mul,

Goal state after:
case neg.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
a✝ : Nontrivial R
n : ℕ
ih : ∀ (p q : R[X]), (p * q).degree < ↑n → Associated (p * q).content (p.content * q.content)
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.primPart.degree + q.primPart.degree = ↑n
⊢ gcd (q.primPart.leadingCoeff * p.primPart.leadingCoeff) (q.primPart * p.primPart).eraseLead.content ∣ 1
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝ : Field R
p q : R[X]
⊢ (p / q).degree ≤ p.degree

Tactic:
by
  by_cases hq : q = 0
  · simp [hq]
  · rw [div_def, mul_comm, degree_mul_leadingCoeff_inv _ hq]; exact degree_divByMonic_le _ _

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
h0 : ¬C (p * q).content = 0
| C p.content * C q.content * (p.primPart * q.primPart)

Tactic:
← C_mul

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
h0 : ¬C (p * q).content = 0
| C (p.content * q.content) * (p.primPart * q.primPart)
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝ : Field R
u : R[X]ˣ
n : ℕ
⊢ (1 / if n = 0 then (↑u).coeff 0 else 0) = if n = 0 then (↑u⁻¹).coeff 0 else 0

Tactic:
split_ifs

Goal state after:
case pos
R : Type u
inst✝ : Field R
u : R[X]ˣ
n : ℕ
h✝ : n = 0
⊢ 1 / (↑u).coeff 0 = (↑u⁻¹).coeff 0

case neg
R : Type u
inst✝ : Field R
u : R[X]ˣ
n : ℕ
h✝ : ¬n = 0
⊢ 1 / 0 = 0
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝¹ : Field R
p : R[X]
inst✝ : DecidableEq R
hp0 : IsUnit p.leadingCoeff
⊢ (normalize p).leadingCoeff = 1

Tactic:
leadingCoeff_normalize,

Goal state after:
R : Type u
inst✝¹ : Field R
p : R[X]
inst✝ : DecidableEq R
hp0 : IsUnit p.leadingCoeff
⊢ normalize p.leadingCoeff = 1
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: case neg
R : Type u
inst✝ : Field R
p q : R[X]
hpq : q.degree ≤ p.degree
hq : ¬q = 0
⊢ (C q.leadingCoeff⁻¹ * (p /ₘ (q * C q.leadingCoeff⁻¹))).leadingCoeff = p.leadingCoeff / q.leadingCoeff

Tactic:
leadingCoeff_mul,

Goal state after:
case neg
R : Type u
inst✝ : Field R
p q : R[X]
hpq : q.degree ≤ p.degree
hq : ¬q = 0
⊢ (C q.leadingCoeff⁻¹).leadingCoeff * (p /ₘ (q * C q.leadingCoeff⁻¹)).leadingCoeff = p.leadingCoeff / q.leadingCoeff
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝ : Field R
p : R[X]
hp0 : p ≠ 0
hpu : ¬IsUnit p
⊢ p * C p.leadingCoeff⁻¹ ≠ 1

Tactic:
contrapose hpu

Goal state after:
R : Type u
inst✝ : Field R
p : R[X]
hp0 : p ≠ 0
hpu : p * C p.leadingCoeff⁻¹ = 1
⊢ IsUnit p
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : Associates α
ha : a ≠ 0
hb : b ≠ 0
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
k : ℕ
a✝ : Nontrivial α
hk0 : ¬k = 0
p : Associates α
hp : Irreducible p
h : a * b = 0 ^ k
⊢ False

Tactic:
zero_pow hk0

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : Associates α
ha : a ≠ 0
hb : b ≠ 0
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
k : ℕ
a✝ : Nontrivial α
hk0 : ¬k = 0
p : Associates α
hp : Irreducible p
h : a * b = 0
⊢ False
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
h : Transcendental R s
f : R[X]
⊢ (algEquivOfTranscendental R s h).symm ((aeval ⟨s, ⋯⟩) f) = f

Tactic:
by
  apply (algEquivOfTranscendental R s h).toEquiv.injective
  simp

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
h : Transcendental R s
⊢ (algEquivOfTranscendental R s h).symm ⟨s, ⋯⟩ = X

Tactic:
by
  apply (algEquivOfTranscendental R s h).toEquiv.injective
  simp

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
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
this : g = g.range.subtype ∘ₗ g.rangeRestrict
⊢ Function.Surjective ⇑(lTensor Q g.rangeRestrict)

Tactic:
apply lTensor_surjective

Goal state after:
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
this : g = g.range.subtype ∘ₗ g.rangeRestrict
⊢ Function.Surjective ⇑g.rangeRestrict
Module: Mathlib.RingTheory.Flat.Basic

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommSemiring R
M : Type u_2
N : Type u_3
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R M
inst✝⁶ : Module R N
P : Type u_4
Q : Type u_5
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
f : P →ₗ[R] M
g : Q →ₗ[R] N
inst✝¹ : Module.Flat R P
inst✝ : Module.Flat R N
hf : Function.Injective ⇑f
hg : Function.Injective ⇑g
⊢ Function.Injective ⇑(map f g)

Tactic:
by
  rw [← LinearMap.rTensor_comp_lTensor]
  exact (Module.Flat.rTensor_preserves_injective_linearMap f hf).comp
    (Module.Flat.lTensor_preserves_injective_linearMap g hg)

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 : ι) → MulOneClass (G i)
inst✝ : ∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)
i : ι
x✝ : G i
⊢ ⟦⟨i, x✝⟩⟧ * 1 = ⟦⟨i, x✝⟩⟧

Tactic:
by simp_rw [one_def i, mul_def, mul_one]

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 : ι) → NonUnitalNonAssocSemiring (G i)
inst✝ : ∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)
i : ι
x✝² x✝¹ x✝ : G i
⊢ ⟦⟨i, x✝²⟩⟧ * (⟦⟨i, x✝¹⟩⟧ + ⟦⟨i, x✝⟩⟧) = ⟦⟨i, x✝²⟩⟧ * ⟦⟨i, x✝¹⟩⟧ + ⟦⟨i, x✝²⟩⟧ * ⟦⟨i, x✝⟩⟧

Tactic:
simp_rw [add_def, mul_def, left_distrib, add_def]

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

Goal state before:
pp: ι : Type u_1
G : Type u_4
inst✝² : Fintype ι
inst✝¹ : AddCommGroup G
inst✝ : Module ℚ≥0 G
⊢ balance 0 = 0

Tactic:
by simp [balance]

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 ι
f₁ f₂ g₁ g₂ : ι → M
⊢ 𝔼 i ∈ s, (f₁ i + f₂ i) + 𝔼 i ∈ s, (g₁ i + g₂ i) = 𝔼 i ∈ s, (f₁ i + g₁ i) + 𝔼 i ∈ s, (f₂ i + g₂ i)

Tactic:
by
  simp_rw [expect_add_distrib, add_add_add_comm]

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 ι
p : ι → Prop
inst✝ : DecidablePred p
h : ∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j
a : M
⊢ (𝔼 i ∈ s, if p i then a else 0) = if ∃ i ∈ s, p i then (↑(#s))⁻¹ • a else 0

Tactic:
split_ifs

Goal state after:
case pos
ι : Type u_1
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Module ℚ≥0 M
s : Finset ι
p : ι → Prop
inst✝ : DecidablePred p
h : ∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j
a : M
h✝ : ∃ i ∈ s, p i
⊢ (𝔼 i ∈ s, if p i then a else 0) = (↑(#s))⁻¹ • a

case neg
ι : Type u_1
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Module ℚ≥0 M
s : Finset ι
p : ι → Prop
inst✝ : DecidablePred p
h : ∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j
a : M
h✝ : ¬∃ i ∈ s, p i
⊢ (𝔼 i ∈ s, if p i then a else 0) = 0
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

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

case neg
ι : Type u_1
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Module ℚ≥0 M
s : Finset ι
inst✝ : DecidableEq ι
i : ι
f : (j : ι) → i = j → M
h✝ : i ∉ s
⊢ (𝔼 j ∈ s, if h : i = j then f j h else 0) = 0
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

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

case neg
ι : Type u_1
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Module ℚ≥0 M
s : Finset ι
inst✝ : DecidableEq ι
i : ι
f : (j : ι) → j = i → M
h✝ : i ∉ s
⊢ (𝔼 j ∈ s, if h : j = i then f j h else 0) = 0
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

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

case neg
ι : Type u_1
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Module ℚ≥0 M
s : Finset ι
inst✝ : DecidableEq ι
i : ι
f : ι → M
h✝ : i ∉ s
⊢ (𝔼 j ∈ s, if i = j then f j else 0) = 0
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

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

case neg
ι : Type u_1
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Module ℚ≥0 M
s : Finset ι
inst✝ : DecidableEq ι
i : ι
f : ι → M
h✝ : i ∉ s
⊢ (𝔼 j ∈ s, if j = i then f j else 0) = 0
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 ι
hs : s.Nonempty
a : M
⊢ 𝔼 _i ∈ s, a = a

Tactic:
by
  rw [expect, sum_const, ← Nat.cast_smul_eq_nsmul ℚ≥0, inv_smul_smul₀]
  exact mod_cast hs.card_ne_zero

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✝⁴ : CommSemiring R
inst✝³ : (i : ι) → Semiring (G i)
inst✝² : (i : ι) → Algebra R (G i)
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), AlgHomClass (T h) R (G i) (G j)
inst✝ : Nonempty ι
i : ι
r : R
⊢ ⟦⟨i, (algebraMap R (G i)) r⟩⟧ = (algebraMap R (DirectLimit G f)) r

Tactic:
by rw [algebraMap_def i]

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

Goal state before:
pp: case inr.mpr.inr
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hi₀ : 0 ≤ i
hia : i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
⊢ ∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i

Tactic:
refine ⟨i + a * (n / a), ⟨?_, ?_⟩, ?_⟩
    · exact hn.symm.le.trans (add_le_add_left hi _)
    · rw [add_comm n a]
      refine add_lt_add_of_lt_of_le hia (le_trans ?_ hn.le)
      simp only [le_add_iff_nonneg_left]
      exact Int.emod_nonneg n (ne_of_gt ha)
    · rw [Int.add_mul_emod_self_left, Int.emod_eq_of_lt hi₀ hia]

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

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ image (Function.uncurry Sym2.mk) (s ×ˢ s) = s.sym2

Tactic:
sym2_eq_image

Goal state after:
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ image (Function.uncurry Sym2.mk) (s ×ˢ s) = image (Function.uncurry Sym2.mk) (s ×ˢ s)
Module: Mathlib.Data.List.Sym

Goal state before:
pp: α : Type u_1
xs✝ ys : List α
x y : α
xs : List α
| s(y, x)

Tactic:
rw [Sym2.eq_swap]

Goal state after:
α : Type u_1
xs✝ ys : List α
x y : α
xs : List α
| s(x, y)
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
n : ℕ
k : Sym α n
s : Finset α
hk : k ∈ s.sym n
⊢ (↑k).prod = ∏ d ∈ s, d ^ Multiset.count d ↑k

Tactic:
Finset.prod_multiset_count_of_subset _ s

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
n : ℕ
k : Sym α n
s : Finset α
hk : k ∈ s.sym n
⊢ ∏ i ∈ s, i ^ Multiset.count i ↑k = ∏ d ∈ s, d ^ Multiset.count d ↑k

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
n : ℕ
k : Sym α n
s : Finset α
hk : k ∈ s.sym n
⊢ (↑k).toFinset ⊆ s
Module: Mathlib.Data.List.Sym

Goal state before:
pp: case disj
α : Type u_1
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
h : (x :: xs).Nodup
⊢ (map (fun p ↦ x ::ₛ p) (List.sym n (x :: xs))).Disjoint (List.sym (n + 1) xs)

Tactic:
case disj =>
      intro z hz hz'
      rw [mem_map] at hz
      obtain ⟨z, _hz, rfl⟩ := hz
      have := first_mem_of_cons_mem_sym hz'
      simp only [nodup_cons, this, not_true_eq_false, false_and] at h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
⊢ ∀ ⦃a b : α × α⦄, Rel α a b → Rel β (Prod.map f f a) (Prod.map f f b)

Tactic:
intro _ _ h

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
a✝ b✝ : α × α
h : Rel α a✝ b✝
⊢ Rel β (Prod.map f f a✝) (Prod.map f f b✝)
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α✝
f✝ : α✝ → β
α : Type ?u.43
R : Type ?u.14
N : Type ?u.13
inst✝ : SMul R N
f : { f // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }
g : { g // ∀ (a₁ a₂ : α), g a₁ a₂ = g a₂ a₁ }
x✝¹ x✝ : α
⊢ (↑f • ↑g) x✝¹ x✝ = (↑f • ↑g) x✝ x✝¹

Tactic:
rw [Pi.smul_apply', Pi.smul_apply', Pi.smul_apply', Pi.smul_apply', f.prop, g.prop]

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

Goal state before:
pp: α : Type u_1
s : Set α
⊢ s.sym2 = uncurry Sym2.mk '' s ×ˢ s

Tactic:
by ext ⟨x, y⟩; aesop

Goal state after:
Module: Mathlib.CategoryTheory.Iso

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
α : X ≅ Y
β : Y ≅ X
⊢ α.hom = β.inv ↔ β.hom = α.inv

Tactic:
← symm_inv,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
α : X ≅ Y
β : Y ≅ X
⊢ α.symm.inv = β.inv ↔ β.hom = α.inv
Module: Mathlib.Logic.Lemmas

Goal state before:
pp: α : Sort u_1
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
a : p → α
b : ¬p → q → α
c : ¬p → ¬q → α
⊢ (dite p a fun hp ↦ dite q (b hp) (c hp)) = if hq : q then dite p a fun hp ↦ b hp hq else dite p a fun hp ↦ c hp hq

Tactic:
split_ifs

Goal state after:
case pos
α : Sort u_1
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
a : p → α
b : ¬p → q → α
c : ¬p → ¬q → α
h✝¹ : p
h✝ : q
⊢ a h✝¹ = a h✝¹

case neg
α : Sort u_1
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
a : p → α
b : ¬p → q → α
c : ¬p → ¬q → α
h✝¹ : p
h✝ : ¬q
⊢ a h✝¹ = a h✝¹

case pos
α : Sort u_1
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
a : p → α
b : ¬p → q → α
c : ¬p → ¬q → α
h✝¹ : ¬p
h✝ : q
⊢ b h✝¹ h✝ = b h✝¹ ⋯

case neg
α : Sort u_1
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
a : p → α
b : ¬p → q → α
c : ¬p → ¬q → α
h✝¹ : ¬p
h✝ : ¬q
⊢ c h✝¹ h✝ = c h✝¹ ⋯
Module: Mathlib.Logic.Lemmas

Goal state before:
pp: α : Sort u_1
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
a : p → q → α
b : p → ¬q → α
c : ¬p → α
⊢ dite p (fun hp ↦ dite q (a hp) (b hp)) c = if hq : q then dite p (fun hp ↦ a hp hq) c else dite p (fun hp ↦ b hp hq) c

Tactic:
split_ifs

Goal state after:
case pos
α : Sort u_1
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
a : p → q → α
b : p → ¬q → α
c : ¬p → α
h✝¹ : p
h✝ : q
⊢ a h✝¹ h✝ = a h✝¹ ⋯

case neg
α : Sort u_1
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
a : p → q → α
b : p → ¬q → α
c : ¬p → α
h✝¹ : p
h✝ : ¬q
⊢ b h✝¹ h✝ = b h✝¹ ⋯

case pos
α : Sort u_1
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
a : p → q → α
b : p → ¬q → α
c : ¬p → α
h✝¹ : ¬p
h✝ : q
⊢ c h✝¹ = c h✝¹

case neg
α : Sort u_1
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
a : p → q → α
b : p → ¬q → α
c : ¬p → α
h✝¹ : ¬p
h✝ : ¬q
⊢ c h✝¹ = c h✝¹
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: case cons.cons
V : Type u
inst✝ : Quiver V
a b c : V
p₁ p₂ : Path a b
b✝¹ c✝ : V
q₁ : Path b b✝¹
f₁ : b✝¹ ⟶ c✝
ih : ∀ {q₂ : Path b b✝¹}, q₁.length = q₂.length → p₁.comp q₁ = p₂.comp q₂ → p₁ = p₂ ∧ q₁ = q₂
b✝ : V
q₂ : Path b b✝
f₂ : b✝ ⟶ c✝
hq : (q₁.cons f₁).length = (q₂.cons f₂).length
h : p₁.comp (q₁.cons f₁) = p₂.comp (q₂.cons f₂)
⊢ p₁ = p₂ ∧ q₁.cons f₁ = q₂.cons f₂

Tactic:
simp only [comp_cons, cons.injEq] at h

Goal state after:
case cons.cons
V : Type u
inst✝ : Quiver V
a b c : V
p₁ p₂ : Path a b
b✝¹ c✝ : V
q₁ : Path b b✝¹
f₁ : b✝¹ ⟶ c✝
ih : ∀ {q₂ : Path b b✝¹}, q₁.length = q₂.length → p₁.comp q₁ = p₂.comp q₂ → p₁ = p₂ ∧ q₁ = q₂
b✝ : V
q₂ : Path b b✝
f₂ : b✝ ⟶ c✝
hq : (q₁.cons f₁).length = (q₂.cons f₂).length
h : b✝¹ = b✝ ∧ p₁.comp q₁ ≍ p₂.comp q₂ ∧ f₁ ≍ f₂
⊢ p₁ = p₂ ∧ q₁.cons f₁ = q₂.cons f₂
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: case cons.zero
V : Type u
inst✝ : Quiver V
a b c d : V
p : Path a c
q : c ⟶ d
h : ∀ {n : ℕ}, p.length = n + 1 → ∃ c_1 f q x, p = f.toPath.comp q
hp : (p.cons q).length = 0 + 1
⊢ ∃ c_1 f q_1 x, p.cons q = f.toPath.comp q_1

Tactic:
rw [length_cons, Nat.zero_add, Nat.add_eq_right] at hp
      obtain rfl := eq_of_length_zero p hp
      obtain rfl := eq_nil_of_length_zero p hp
      exact ⟨d, q, nil, rfl, rfl⟩

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

Goal state before:
pp: case refine_1.cons
V : Type u_1
inst✝ : Quiver V
a b b✝ : V
p' : Path a b✝
e : b✝ ⟶ b
h : (p'.cons e).length ≠ 0
⊢ ∃ c p'_1 e_1, p'.cons e = p'_1.cons e_1

Tactic:
exact ⟨_, p', e, rfl⟩

Goal state after:
Module: Mathlib.CategoryTheory.EssentialImage

Goal state before:
pp: C : Type u₁
D : Type u₂
E : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
F : D ⥤ E
L : C ⥤ D
inst✝ : L.EssSurj
h : ∀ ⦃X₁ X₂ : C⦄ (φ : F.obj (L.obj X₁) ⟶ F.obj (L.obj X₂)), ∃ f, F.map f = φ
⊢ ∀ {X Y : D}, Function.Surjective F.map

Tactic:
intro X₁

Goal state after:
C : Type u₁
D : Type u₂
E : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
F : D ⥤ E
L : C ⥤ D
inst✝ : L.EssSurj
h : ∀ ⦃X₁ X₂ : C⦄ (φ : F.obj (L.obj X₁) ⟶ F.obj (L.obj X₂)), ∃ f, F.map f = φ
X₁ : D
⊢ ∀ {Y : D}, Function.Surjective F.map
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
⊢ e.unit.app (e.inverse.obj Y) ≫
      (e.inverse.map (e.counitInv.app (e.functor.obj (e.inverse.obj Y))) ≫
          e.unitIso.hom.app (e.inverse.1 (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y))))) ≫
            e.unitIso.inv.app (e.inverse.1 (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y))))) ≫
              e.inverse.map (e.functor.map (e.unitInv.app (e.inverse.obj Y)))) ≫
        e.inverse.map (e.counit.app Y) =
    𝟙 (e.inverse.obj Y)

Tactic:
slice_lhs 2 3 => rw [← e.unit_naturality]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
⊢ e.unit.app (e.inverse.obj Y) ≫
      (((e.unit.app (e.inverse.obj (e.functor.obj (e.inverse.obj Y))) ≫
              e.inverse.map (e.functor.map (e.inverse.map (e.counitInv.app (e.functor.obj (e.inverse.obj Y)))))) ≫
            e.unitIso.inv.app (e.inverse.1 (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))) ≫
          e.inverse.map (e.functor.map (e.unitInv.app (e.inverse.obj Y)))) ≫
        e.inverse.map (e.counit.app Y) =
    𝟙 (e.inverse.obj Y)
Module: Mathlib.CategoryTheory.Discrete.Basic

Goal state before:
pp: J : Type v₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
F : Discrete J ⥤ C
j : Discrete J
f : j ⟶ j
⊢ F.map f = 𝟙 (F.obj j)

Tactic:
have h : f = 𝟙 j := by cat_disch
  rw [h]
  simp

Goal state after: