mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: ι✝ : 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✝¹ : PartialOrder ι
inst✝ : DecidableEq ι
f : (j : ↑(Iic i)) → X ↑j
⊢ (fun f j ↦ if h : ↑j = i then ⋯ ▸ f.2 else f.1 ⟨↑j, ⋯⟩) ((fun f ↦ (fun j ↦ f ⟨↑j, ⋯⟩, f ⟨i, ⋯⟩)) f) = f

Tactic:
by grind

Goal state after:
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: ι✝ : 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
equiv : (j : ↑(Iio i)) → F ↑j ≃ piLT X ↑j
nat : IsNatEquiv f equiv
t : ↑(limit f i)
⊢ (fun t ↦ ⟨fun l ↦ (equiv l).symm (↑t l), ⋯⟩) ((fun t ↦ ⟨fun l ↦ (equiv l) (↑t l), ⋯⟩) t) = t

Tactic:
ext; apply Equiv.left_inv

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

Goal state before:
pp: σ : Type u
R : Type v
inst✝¹ : CommSemiring R
p m : ℕ
inst✝ : ExpChar R p
⊢ ExpChar (MvPolynomial σ R) p

Tactic:
cases ‹ExpChar R p›

Goal state after:
case zero
σ : Type u
R : Type v
inst✝¹ : CommSemiring R
m : ℕ
inst✝ : CharZero R
⊢ ExpChar (MvPolynomial σ R) 1

case prime
σ : Type u
R : Type v
inst✝ : CommSemiring R
p m : ℕ
hprime✝ : Nat.Prime p
hchar✝ : CharP R p
⊢ ExpChar (MvPolynomial σ R) p
Module: Mathlib.RingTheory.Flat.Basic

Goal state before:
pp: R : Type u
M : Type v
N : Type u_1
P : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
inst✝² : AddCommMonoid P
inst✝¹ : Module R P
inst✝ : Flat R M
f : N →ₗ[R] P
hf : Injective ⇑f
⊢ Injective ⇑(rTensor M f)

Tactic:
by
  refine rTensor_injective_of_fg fun N P Nfg Pfg le ↦ ?_
  rw [← Finite.iff_fg] at Nfg Pfg
  have := Finite.small R P
  let se := (Shrink.linearEquiv R P).symm
  have := Module.Finite.equiv se
  rw [rTensor_injective_iff_subtype (fun _ _ ↦ (Subtype.ext <| hf <| Subtype.ext_iff.mp ·)) se]
  exact (flat_iff R M).mp ‹_› _ (Finite.iff_fg.mp inferInstance)

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

Goal state before:
pp: α : Type u_2
inst✝ : Fintype α
s t : Finset α
h : Disjoint s t
⊢ ↑(#s + #t) / ↑(Fintype.card α) = ↑(#s) / ↑(Fintype.card α) + ↑(#t) / ↑(Fintype.card α)

Tactic:
Nat.cast_add,

Goal state after:
α : Type u_2
inst✝ : Fintype α
s t : Finset α
h : Disjoint s t
⊢ (↑(#s) + ↑(#t)) / ↑(Fintype.card α) = ↑(#s) / ↑(Fintype.card α) + ↑(#t) / ↑(Fintype.card α)
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 : ι) → Group (G i)
inst✝² : Group C
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)
inst✝ : ∀ (i : ι), MonoidHomClass (H i) (G i) C
i : ι
x✝¹ x✝ : G i
⊢ map₂ f f f (fun x x1 x2 ↦ x1 / x2) ⋯ ⟦⟨i, x✝¹⟩⟧ ⟦⟨i, x✝⟩⟧ = ⟦⟨i, x✝¹⟩⟧ * map f f (fun x x_1 ↦ x_1⁻¹) ⋯ ⟦⟨i, x✝⟩⟧

Tactic:
map₂_def,

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 : ι) → Group (G i)
inst✝² : Group C
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)
inst✝ : ∀ (i : ι), MonoidHomClass (H i) (G i) C
i : ι
x✝¹ x✝ : G i
⊢ ⟦⟨i, x✝¹ / x✝⟩⟧ = ⟦⟨i, x✝¹⟩⟧ * map f f (fun x x_1 ↦ x_1⁻¹) ⋯ ⟦⟨i, x✝⟩⟧
Module: Mathlib.Data.Finset.Density

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

Tactic:
by
  rw [add_comm, dens_sdiff_add_dens_inter]

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 : ι) → GroupWithZero (G i)
inst✝² : GroupWithZero C
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), MonoidWithZeroHomClass (T h) (G i) (G j)
inst✝ : ∀ (i : ι), MonoidWithZeroHomClass (H i) (G i) C
i : ι
x✝¹ x✝ : G i
⊢ map₂ f f f (fun x x1 x2 ↦ x1 / x2) ⋯ ⟦⟨i, x✝¹⟩⟧ ⟦⟨i, x✝⟩⟧ = ⟦⟨i, x✝¹⟩⟧ * map f f (fun x x_1 ↦ x_1⁻¹) ⋯ ⟦⟨i, x✝⟩⟧

Tactic:
map₂_def,

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 : ι) → GroupWithZero (G i)
inst✝² : GroupWithZero C
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), MonoidWithZeroHomClass (T h) (G i) (G j)
inst✝ : ∀ (i : ι), MonoidWithZeroHomClass (H i) (G i) C
i : ι
x✝¹ x✝ : G i
⊢ ⟦⟨i, x✝¹ / x✝⟩⟧ = ⟦⟨i, x✝¹⟩⟧ * map f f (fun x x_1 ↦ x_1⁻¹) ⋯ ⟦⟨i, x✝⟩⟧
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
⊢ ⟦⟨Classical.arbitrary ι, ↑q⟩⟧ = ⟦⟨Classical.arbitrary ι, ↑q.num / ↑q.den⟩⟧

Tactic:
NNRat.cast_def

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 : ι) → 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
⊢ ⟦⟨Classical.arbitrary ι, ↑q.num / ↑q.den⟩⟧ = ⟦⟨Classical.arbitrary ι, ↑q.num / ↑q.den⟩⟧
Module: Mathlib.Order.Interval.Finset.Gaps

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
⊢ (F.intervalGapsWithin h a b 0).1 = a

Tactic:
by
  simp [intervalGapsWithin, intervalGapsWithin.fst]

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

Goal state before:
pp: case inl
ι : Type u_1
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module ℚ≥0 M
f : ι → M
⊢ #∅ • 𝔼 i ∈ ∅, f i = ∑ i ∈ ∅, f i

pp: case inr
ι : Type u_1
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module ℚ≥0 M
s : Finset ι
f : ι → M
hs : s.Nonempty
⊢ #s • 𝔼 i ∈ s, f i = ∑ i ∈ s, f i

Tactic:
· simp

Goal state after:
case inr
ι : Type u_1
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module ℚ≥0 M
s : Finset ι
f : ι → M
hs : s.Nonempty
⊢ #s • 𝔼 i ∈ s, f i = ∑ i ∈ s, f i
Module: Mathlib.Order.Interval.Finset.Gaps

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j✝ : ℕ
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
j : ℕ
hj✝ : j < k + 1
hj : ¬j = 0
⊢ j - 1 ∈ Iio k

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j✝ : ℕ
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
j : ℕ
hj✝ : j < k + 1
hj : ¬j = k
⊢ j ∈ Iio k

Tactic:
by grind

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

Goal state before:
pp: case ih
R : Type u_1
ι : 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✝⁶ : Semiring R
inst✝⁵ : (i : ι) → AddCommMonoid (G i)
inst✝⁴ : (i : ι) → Module R (G i)
inst✝³ : ∀ (i j : ι) (h : i ≤ j), LinearMapClass (T h) R (G i) (G j)
inst✝² : Nonempty ι
P : Type u_7
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
g₁ g₂ : DirectLimit G f →ₗ[R] P
h : ∀ (i : ι), g₁ ∘ₗ of R ι G f i = g₂ ∘ₗ of R ι G f i
i : ι
x : G i
⊢ g₁ ⟦⟨i, x⟩⟧ = g₂ ⟦⟨i, x⟩⟧

Tactic:
| _ i x
   => 

Goal state after:
case ih
R : Type u_1
ι : 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✝⁶ : Semiring R
inst✝⁵ : (i : ι) → AddCommMonoid (G i)
inst✝⁴ : (i : ι) → Module R (G i)
inst✝³ : ∀ (i j : ι) (h : i ≤ j), LinearMapClass (T h) R (G i) (G j)
inst✝² : Nonempty ι
P : Type u_7
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
g₁ g₂ : DirectLimit G f →ₗ[R] P
h : ∀ (i : ι), g₁ ∘ₗ of R ι G f i = g₂ ∘ₗ of R ι G f i
i : ι
x : G i
⊢ g₁ ⟦⟨i, x⟩⟧ = g₂ ⟦⟨i, x⟩⟧
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 : α
f : α → α → β
p : Fin (k + 1) → α × α := F.intervalGapsWithin h a b
i : ℕ
x✝ : i ∈ range k
⊢ i ∈ Set.Iio k

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j : ℕ
a b : α
hab : a ≤ b
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hF : (↑F).PairwiseDisjoint fun z ↦ Icc z.1 z.2
this : ∀ j < k + 1, (F.intervalGapsWithin h a b ↑j).1 ≤ (F.intervalGapsWithin h a b ↑j).2
hj : ¬j < k + 1
⊢ ↑↑j < k + 1

Tactic:
by grind

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

Goal state before:
pp: case ih
ι : 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✝³ : (i : ι) → NonUnitalNonAssocSemiring (G i)
inst✝² : ∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)
inst✝¹ : Nonempty ι
P : Type u_7
inst✝ : NonUnitalNonAssocSemiring P
g₁ g₂ : DirectLimit G f →ₙ+* P
h : ∀ (i : ι), g₁.comp (of G f i) = g₂.comp (of G f i)
i : ι
x : G i
⊢ g₁ ⟦⟨i, x⟩⟧ = g₂ ⟦⟨i, x⟩⟧

Tactic:
| _ i x
   => 

Goal state after:
case ih
ι : 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✝³ : (i : ι) → NonUnitalNonAssocSemiring (G i)
inst✝² : ∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)
inst✝¹ : Nonempty ι
P : Type u_7
inst✝ : NonUnitalNonAssocSemiring P
g₁ g₂ : DirectLimit G f →ₙ+* P
h : ∀ (i : ι), g₁.comp (of G f i) = g₂.comp (of G f i)
i : ι
x : G i
⊢ g₁ ⟦⟨i, x⟩⟧ = g₂ ⟦⟨i, x⟩⟧
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 : α
f : α → α → β
p : Fin (k + 1) → α × α := F.intervalGapsWithin h a b
z : α × α
hz : z ∈ F
i : ℕ
hi₁ : i ∈ Set.Iio k
hi₂ : (fun j ↦ ((F.intervalGapsWithin h a b ↑j).2, (F.intervalGapsWithin h a b ↑j.succ).1)) i = z
⊢ i ∈ range k

Tactic:
by grind

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

Goal state before:
pp: case ih
ι : 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✝³ : (i : ι) → NonAssocSemiring (G i)
inst✝² : ∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)
inst✝¹ : Nonempty ι
P : Type u_7
inst✝ : NonAssocSemiring P
g₁ g₂ : DirectLimit G f →+* P
h : ∀ (i : ι), g₁.comp (of G f i) = g₂.comp (of G f i)
i : ι
x : G i
⊢ g₁ ⟦⟨i, x⟩⟧ = g₂ ⟦⟨i, x⟩⟧

Tactic:
| _ i x
   => 

Goal state after:
case ih
ι : 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✝³ : (i : ι) → NonAssocSemiring (G i)
inst✝² : ∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)
inst✝¹ : Nonempty ι
P : Type u_7
inst✝ : NonAssocSemiring P
g₁ g₂ : DirectLimit G f →+* P
h : ∀ (i : ι), g₁.comp (of G f i) = g₂.comp (of G f i)
i : ι
x : G i
⊢ g₁ ⟦⟨i, x⟩⟧ = g₂ ⟦⟨i, x⟩⟧
Module: Mathlib.Algebra.BigOperators.Group.Finset.Gaps

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
f : α → α → β
p : Fin (k + 1) → α × α := ⋯
⊢ ∀ a ∈ range k, f (p ↑a).2 (p ↑a.succ).1 = f ((p ↑a).2, (p ↑a.succ).1).1 ((p ↑a).2, (p ↑a.succ).1).2

Tactic:
· simp

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

Goal state before:
pp: case ih
ι : 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✝⁶ : (i : ι) → NonUnitalNonAssocSemiring (G i)
inst✝⁵ : ∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)
inst✝⁴ : (i : ι) → StarRing (G i)
inst✝³ : ∀ (i j : ι) (h : i ≤ j), StarHomClass (T h) (G i) (G j)
inst✝² : Nonempty ι
P : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring P
inst✝ : StarRing P
g₁ g₂ : DirectLimit G f →⋆ₙ+* P
h : ∀ (i : ι), g₁.comp (of G f i) = g₂.comp (of G f i)
i : ι
x : G i
⊢ g₁ ⟦⟨i, x⟩⟧ = g₂ ⟦⟨i, x⟩⟧

Tactic:
| _ i x
   => 

Goal state after:
case ih
ι : 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✝⁶ : (i : ι) → NonUnitalNonAssocSemiring (G i)
inst✝⁵ : ∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)
inst✝⁴ : (i : ι) → StarRing (G i)
inst✝³ : ∀ (i j : ι) (h : i ≤ j), StarHomClass (T h) (G i) (G j)
inst✝² : Nonempty ι
P : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring P
inst✝ : StarRing P
g₁ g₂ : DirectLimit G f →⋆ₙ+* P
h : ∀ (i : ι), g₁.comp (of G f i) = g₂.comp (of G f i)
i : ι
x : G i
⊢ g₁ ⟦⟨i, x⟩⟧ = g₂ ⟦⟨i, x⟩⟧
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: case ih
R : Type u_1
ι : 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✝⁶ : 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 ι
P : Type u_7
inst✝¹ : Semiring P
inst✝ : Algebra R P
g₁ g₂ : DirectLimit G f →ₐ[R] P
h : ∀ (i : ι), g₁.comp (of G f i) = g₂.comp (of G f i)
i : ι
x : G i
⊢ g₁ ⟦⟨i, x⟩⟧ = g₂ ⟦⟨i, x⟩⟧

Tactic:
| _ i x
   => 

Goal state after:
case ih
R : Type u_1
ι : 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✝⁶ : 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 ι
P : Type u_7
inst✝¹ : Semiring P
inst✝ : Algebra R P
g₁ g₂ : DirectLimit G f →ₐ[R] P
h : ∀ (i : ι), g₁.comp (of G f i) = g₂.comp (of G f i)
i : ι
x : G i
⊢ g₁ ⟦⟨i, x⟩⟧ = g₂ ⟦⟨i, x⟩⟧
Module: Mathlib.Order.Interval.Finset.Gaps

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

Tactic:
by grind

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

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

Tactic:
by grind

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

Goal state before:
pp: case ih
R : Type u_1
ι : 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✝⁶ : CommSemiring R
inst✝⁵ : (i : ι) → NonUnitalNonAssocSemiring (G i)
inst✝⁴ : (i : ι) → DistribMulAction R (G i)
inst✝³ : ∀ (i j : ι) (h : i ≤ j), NonUnitalAlgHomClass (T h) R (G i) (G j)
inst✝² : Nonempty ι
P : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring P
inst✝ : DistribMulAction R P
g₁ g₂ : DirectLimit G f →ₙₐ[R] P
h : ∀ (i : ι), g₁.comp (of G f i) = g₂.comp (of G f i)
i : ι
x : G i
⊢ g₁ ⟦⟨i, x⟩⟧ = g₂ ⟦⟨i, x⟩⟧

Tactic:
| _ i x
   => 

Goal state after:
case ih
R : Type u_1
ι : 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✝⁶ : CommSemiring R
inst✝⁵ : (i : ι) → NonUnitalNonAssocSemiring (G i)
inst✝⁴ : (i : ι) → DistribMulAction R (G i)
inst✝³ : ∀ (i j : ι) (h : i ≤ j), NonUnitalAlgHomClass (T h) R (G i) (G j)
inst✝² : Nonempty ι
P : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring P
inst✝ : DistribMulAction R P
g₁ g₂ : DirectLimit G f →ₙₐ[R] P
h : ∀ (i : ι), g₁.comp (of G f i) = g₂.comp (of G f i)
i : ι
x : G i
⊢ g₁ ⟦⟨i, x⟩⟧ = g₂ ⟦⟨i, x⟩⟧
Module: Mathlib.Data.Int.Interval

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

Tactic:
Function.Embedding.trans_apply,

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

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

Tactic:
Function.Embedding.trans_apply,

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

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

Tactic:
Function.Embedding.trans_apply,

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

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

Tactic:
Function.Embedding.trans_apply,

Goal state after:
a b x : ℤ
⊢ (∃ a_1 < (b - a - 1).toNat, (addLeftEmbedding (a + 1)) (Nat.castEmbedding a_1) = x) ↔ a < x ∧ x < b
Module: Mathlib.Algebra.BigOperators.Group.Finset.Interval

Goal state before:
pp: case succ
α : Type u_1
inst✝ : CommGroup α
f : ℤ → α
hf : Function.Even f
N : ℕ
ih : ∏ m ∈ Icc (-↑N) ↑N, f m = (∏ m ∈ range (N + 1), f ↑m) ^ 2 / f 0
⊢ ∏ m ∈ Icc (-↑(N + 1)) ↑(N + 1), f m = (∏ m ∈ range (N + 1 + 1), f ↑m) ^ 2 / f 0

Tactic:
Nat.cast_add,

Goal state after:
case succ
α : Type u_1
inst✝ : CommGroup α
f : ℤ → α
hf : Function.Even f
N : ℕ
ih : ∏ m ∈ Icc (-↑N) ↑N, f m = (∏ m ∈ range (N + 1), f ↑m) ^ 2 / f 0
⊢ ∏ m ∈ Icc (-(↑N + ↑1)) (↑N + ↑1), f m = (∏ m ∈ range (N + 1 + 1), f ↑m) ^ 2 / f 0
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: case inl
n : ℤ
h : 0 ≤ 0
⊢ image (fun x ↦ x % 0) (Ico n (n + 0)) = Ico 0 0

pp: case inr
n a : ℤ
h : 0 ≤ a
ha : 0 < a
⊢ image (fun x ↦ x % a) (Ico n (n + a)) = Ico 0 a

Tactic:
· simp

Goal state after:
case inr
n a : ℤ
h : 0 ≤ a
ha : 0 < a
⊢ image (fun x ↦ x % a) (Ico n (n + a)) = Ico 0 a
Module: Mathlib.Algebra.BigOperators.Group.Finset.Interval

Goal state before:
pp: α : Type u_1
inst✝ : CommGroup α
f : ℤ → α
b : ℕ
ihb : ∏ n ∈ Ico (-↑b) ↑b, f n / f (n + 1) = f (-↑b) / f ↑b
⊢ -(↑b + 1) ∉ {↑b}

Tactic:
by grind

Goal state after:
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
⊢ i + a + a * (n / a) = i + a * (n / a + 1)

Tactic:
by grind

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

Goal state before:

Tactic:
i + a * (n / a + 1) < n % a + a * (n / a + 1) := by gcongr
        _ = n + a := by rw [mul_add, mul_one, ← add_assoc, hn]

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
j : ℕ
hj : j < k + 1
j' : ℕ
hj' : j' < k + 1
hjj' : j ≠ j'
hij' : j < j'
this : (F.intervalGapsWithin h a b ↑j).2 ≤ (F.intervalGapsWithin h a b ↑j').1
⊢ Ioc (F.intervalGapsWithin h a b ↑j).1 (F.intervalGapsWithin h a b ↑j).2 ∩
      Ioc (F.intervalGapsWithin h a b ↑j').1 (F.intervalGapsWithin h a b ↑j').2 =
    ∅

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
j : ℕ
hj : j < k + 1
j' : ℕ
hj' : j' < k + 1
hjj' : j ≠ j'
hij' : j < j'
hj'₀ : j' - 1 + 1 = j'
⊢ j' - 1 ∈ Iio k

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
j : ℕ
hj : j < k + 1
j' : ℕ
hj' : j' < k + 1
hjj' : j ≠ j'
hij' : j < j'
hj'₀ : j' - 1 + 1 = j'
this : (F.intervalGapsWithin h a b ↑(j' - 1)).2 ≤ (F.intervalGapsWithin h a b ↑j').1
⊢ ⟨j, ⋯⟩ ≤ ⟨j' - 1, ⋯⟩

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
x : α
xs : List α
z : Sym2 α
⊢ z ∈ (x :: xs).sym2 ↔ z = s(x, x) ∨ (∃ y ∈ xs, z = s(x, y)) ∨ z ∈ xs.sym2

Tactic:
simp only [List.sym2, map_cons, cons_append, mem_cons, mem_append, mem_map]

Goal state after:
α : Type u_1
x : α
xs : List α
z : Sym2 α
⊢ z = s(x, x) ∨ (∃ a ∈ xs, s(x, a) = z) ∨ z ∈ xs.sym2 ↔ z = s(x, x) ∨ (∃ y ∈ xs, z = s(x, y)) ∨ z ∈ xs.sym2
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
s : Finset α
a b : α
⊢ s(a, b) ∈ s.sym2.val ↔ a ∈ s ∧ b ∈ s

Tactic:
sym2_val,

Goal state after:
α : Type u_1
s : Finset α
a b : α
⊢ s(a, b) ∈ s.val.sym2 ↔ a ∈ s ∧ b ∈ s