harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Groupoid/FreeGroupoid.lean
theorem congr_comp_reverse {X Y : Paths <| Quiver.Symmetrify V} (p : X ⟶ Y) :
    Quot.mk (@Quotient.CompClosure _ _ redStep _ _) (p ≫ p.reverse) =
      Quot.mk (@Quotient.CompClosure _ _ redStep _ _) (𝟙 X)

Proof state:
case H.cons
V : Type u
inst✝ : Quiver V
X Y a b : Paths (Quiver.Symmetrify V)
q : Quiver.Path X a
f : a ⟶ b
ih : EqvGen (Quotient.CompClosure redStep) (q ≫ q.reverse) (𝟙 X)
⊢ EqvGen (Quotient.CompClosure redStep) (q.cons f ≫ (Quiver.reverse f).toPath.comp q.reverse) (𝟙 X)

Tactic:
fapply EqvGen.trans

Result:
case H.cons.y
V : Type u
inst✝ : Quiver V
X Y a b : Paths (Quiver.Symmetrify V)
q : Quiver.Path X a
f : a ⟶ b
ih : EqvGen (Quotient.CompClosure redStep) (q ≫ q.reverse) (𝟙 X)
⊢ X ⟶ X

case H.cons.a
V : Type u
inst✝ : Quiver V
X Y a b : Paths (Quiver.Symmetrify V)
q : Quiver.Path X a
f : a ⟶ b
ih : EqvGen (Quotient.CompClosure redStep) (q ≫ q.reverse) (𝟙 X)
⊢ EqvGen (Quotient.CompClosure redStep) (q.cons f ≫ (Quiver.reverse f).toPath.comp q.reverse) ?H.cons.y

case H.cons.a
V : Type u
inst✝ : Quiver V
X Y a b : Paths (Quiver.Symmetrify V)
q : Quiver.Path X a
f : a ⟶ b
ih : EqvGen (Quotient.CompClosure redStep) (q ≫ q.reverse) (𝟙 X)
⊢ EqvGen (Quotient.CompClosure redStep) ?H.cons.y (𝟙 X)

Proof state:
case H.cons.a.a.a
V : Type u
inst✝ : Quiver V
X Y a b : Paths (Quiver.Symmetrify V)
q : Quiver.Path X a
f : a ⟶ b
ih : EqvGen (Quotient.CompClosure redStep) (q ≫ q.reverse) (𝟙 X)
⊢ Quotient.CompClosure redStep (q ≫ q.reverse) (q.cons f ≫ (Quiver.reverse f).toPath.comp q.reverse)

Tactic:
have : Quotient.CompClosure redStep (q ≫ 𝟙 _ ≫ Quiver.Path.reverse q)
    (q ≫ (Quiver.Hom.toPath f ≫ Quiver.Hom.toPath (Quiver.reverse f)) ≫
      Quiver.Path.reverse q) := by
  apply Quotient.CompClosure.intro
  apply redStep.step

Result:
case H.cons.a.a.a
V : Type u
inst✝ : Quiver V
X Y a b : Paths (Quiver.Symmetrify V)
q : Quiver.Path X a
f : a ⟶ b
ih : EqvGen (Quotient.CompClosure redStep) (q ≫ q.reverse) (𝟙 X)
this : Quotient.CompClosure redStep (q ≫ 𝟙 a ≫ q.reverse) (q ≫ (f.toPath ≫ (Quiver.reverse f).toPath) ≫ q.reverse)
⊢ Quotient.CompClosure redStep (q ≫ q.reverse) (q.cons f ≫ (Quiver.reverse f).toPath.comp q.reverse)

Proof state:
case H.cons.y
V : Type u
inst✝ : Quiver V
X Y a b : Paths (Quiver.Symmetrify V)
q : Quiver.Path X a
f : a ⟶ b
ih : EqvGen (Quotient.CompClosure redStep) (q ≫ q.reverse) (𝟙 X)
⊢ X ⟶ X

Tactic:
exact q ≫ Quiver.Path.reverse q

Result:
no goals
-- Mathlib/Algebra/Polynomial/Bivariate.lean
lemma evalEval_multiset_prod (x y : R) (l : Multiset R[X][Y]) :
    l.prod.evalEval x y = (l.map <| evalEval x y).prod

Proof state:
R : Type u_1
inst✝ : CommSemiring R
x y : R
l : Multiset R[X][Y]
⊢ (Multiset.map (eval x ∘ eval (C y)) l).prod = (Multiset.map (fun x_1 => eval x (eval (C y) x_1)) l).prod

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommSemiring R
x y : R
l : Multiset R[X][Y]
⊢ evalEval x y l.prod = (Multiset.map (evalEval x y) l).prod

Tactic:
simpa only [evalEval, eval_multiset_prod, Multiset.map_map] using by rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem size_ofFn_go {n} (f : Fin n → α) (i acc) :
    (ofFn.go f i acc).size = acc.size + (n - i)

Proof state:
α : Type u_1
n : Nat
f : Fin n → α
i : Nat
acc : Array α
hin : i < n
this : 1 + (n - (i + 1)) = n - i
⊢ (if h : i < n then ofFn.go f (i + 1) (acc.push (f ⟨i, h⟩)) else acc).size = acc.size + (n - i)

Tactic:
rw [dif_pos hin, size_ofFn_go f (i+1), size_push, Nat.add_assoc, this]

Result:
no goals

Proof state:
α : Type u_1
n : Nat
f : Fin n → α
i : Nat
acc : Array α
hin : i < n
⊢ (if h : i < n then ofFn.go f (i + 1) (acc.push (f ⟨i, h⟩)) else acc).size = acc.size + (n - i)

Tactic:
have : 1 + (n - (i + 1)) = n - i :=
  Nat.sub_sub .. ▸ Nat.add_sub_cancel' (Nat.le_sub_of_add_le (Nat.add_comm .. ▸ hin))

Result:
α : Type u_1
n : Nat
f : Fin n → α
i : Nat
acc : Array α
hin : i < n
this : 1 + (n - (i + 1)) = n - i
⊢ (if h : i < n then ofFn.go f (i + 1) (acc.push (f ⟨i, h⟩)) else acc).size = acc.size + (n - i)

Proof state:
α : Type u_1
n : Nat
f : Fin n → α
i : Nat
acc : Array α
⊢ (ofFn.go f i acc).size = acc.size + (n - i)

Tactic:
if hin : i < n then
  unfold ofFn.go
  have : 1 + (n - (i + 1)) = n - i :=
    Nat.sub_sub .. ▸ Nat.add_sub_cancel' (Nat.le_sub_of_add_le (Nat.add_comm .. ▸ hin))
  rw [dif_pos hin, size_ofFn_go f (i+1), size_push, Nat.add_assoc, this]
else
  have : n - i = 0 := Nat.sub_eq_zero_of_le (Nat.le_of_not_lt hin)
  unfold ofFn.go
  simp [hin, this]

Result:
no goals

Proof state:
α : Type u_1
n : Nat
f : Fin n → α
i : Nat
acc : Array α
hin : ¬i < n
this : n - i = 0
⊢ (if h : i < n then ofFn.go f (i + 1) (acc.push (f ⟨i, h⟩)) else acc).size = acc.size + (n - i)

Tactic:
simp [hin, this]

Result:
no goals

Proof state:
α : Type u_1
n : Nat
f : Fin n → α
i : Nat
acc : Array α
hin : ¬i < n
this : n - i = 0
⊢ (ofFn.go f i acc).size = acc.size + (n - i)

Tactic:
unfold ofFn.go

Result:
α : Type u_1
n : Nat
f : Fin n → α
i : Nat
acc : Array α
hin : ¬i < n
this : n - i = 0
⊢ (if h : i < n then ofFn.go f (i + 1) (acc.push (f ⟨i, h⟩)) else acc).size = acc.size + (n - i)

Proof state:
α : Type u_1
n : Nat
f : Fin n → α
i : Nat
acc : Array α
hin : i < n
⊢ (ofFn.go f i acc).size = acc.size + (n - i)

Tactic:
unfold ofFn.go

Result:
α : Type u_1
n : Nat
f : Fin n → α
i : Nat
acc : Array α
hin : i < n
⊢ (if h : i < n then ofFn.go f (i + 1) (acc.push (f ⟨i, h⟩)) else acc).size = acc.size + (n - i)

Proof state:
α : Type u_1
n : Nat
f : Fin n → α
i : Nat
acc : Array α
hin : ¬i < n
⊢ (ofFn.go f i acc).size = acc.size + (n - i)

Tactic:
have : n - i = 0 := Nat.sub_eq_zero_of_le (Nat.le_of_not_lt hin)

Result:
α : Type u_1
n : Nat
f : Fin n → α
i : Nat
acc : Array α
hin : ¬i < n
this : n - i = 0
⊢ (ofFn.go f i acc).size = acc.size + (n - i)
-- Mathlib/Data/List/Permutation.lean
theorem nodup_permutations_iff {s : List α} : Nodup s.permutations ↔ Nodup s

Proof state:
case intro
α : Type u_1
s : List α
x : α
hs : [x, x] <+ s
l : List α
ht : s ~ [x, x] ++ l
⊢ ∃ x_1, Duplicate x_1 ([x, x] ++ l).permutations

Tactic:
use x :: x :: l

Result:
case h
α : Type u_1
s : List α
x : α
hs : [x, x] <+ s
l : List α
ht : s ~ [x, x] ++ l
⊢ Duplicate (x :: x :: l) ([x, x] ++ l).permutations

Proof state:
α : Type u_1
s : List α
x : α
hs : Duplicate x s
⊢ ¬s.permutations.Nodup

Tactic:
rw [duplicate_iff_sublist] at hs

Result:
α : Type u_1
s : List α
x : α
hs : [x, x] <+ s
⊢ ¬s.permutations.Nodup

Proof state:
case intro
α : Type u_1
s : List α
x : α
hs : [x, x] <+ s
l : List α
ht : s ~ [x, x] ++ l
⊢ ¬s.permutations.Nodup

Tactic:
rw [List.Perm.nodup_iff (List.Perm.permutations ht), ← exists_duplicate_iff_not_nodup]

Result:
case intro
α : Type u_1
s : List α
x : α
hs : [x, x] <+ s
l : List α
ht : s ~ [x, x] ++ l
⊢ ∃ x_1, Duplicate x_1 ([x, x] ++ l).permutations

Proof state:
α : Type u_1
s : List α
⊢ s.permutations.Nodup ↔ s.Nodup

Tactic:
refine ⟨?_, nodup_permutations s⟩

Result:
α : Type u_1
s : List α
⊢ s.permutations.Nodup → s.Nodup

Proof state:
α : Type u_1
s : List α
⊢ ¬s.Nodup → ¬s.permutations.Nodup

Tactic:
rw [← exists_duplicate_iff_not_nodup]

Result:
α : Type u_1
s : List α
⊢ (∃ x, Duplicate x s) → ¬s.permutations.Nodup

Proof state:
case h
α : Type u_1
s : List α
x : α
hs : [x, x] <+ s
l : List α
ht : s ~ [x, x] ++ l
⊢ take 2 (x :: x :: l).permutations <+ ([x, x] ++ l).permutations

Tactic:
exact take_sublist 2 _

Result:
no goals

Proof state:
case h
α : Type u_1
s : List α
x : α
hs : [x, x] <+ s
l : List α
ht : s ~ [x, x] ++ l
⊢ Duplicate (x :: x :: l) ([x, x] ++ l).permutations

Tactic:
rw [List.duplicate_iff_sublist, ← permutations_take_two]

Result:
case h
α : Type u_1
s : List α
x : α
hs : [x, x] <+ s
l : List α
ht : s ~ [x, x] ++ l
⊢ take 2 (x :: x :: l).permutations <+ ([x, x] ++ l).permutations

Proof state:
α : Type u_1
s : List α
⊢ (∃ x, Duplicate x s) → ¬s.permutations.Nodup

Tactic:
intro ⟨x, hs⟩

Result:
α : Type u_1
s : List α
x : α
hs : Duplicate x s
⊢ ¬s.permutations.Nodup

Proof state:
α : Type u_1
s : List α
x : α
hs : [x, x] <+ s
⊢ ¬s.permutations.Nodup

Tactic:
obtain ⟨l, ht⟩ := List.Sublist.exists_perm_append hs

Result:
case intro
α : Type u_1
s : List α
x : α
hs : [x, x] <+ s
l : List α
ht : s ~ [x, x] ++ l
⊢ ¬s.permutations.Nodup

Proof state:
α : Type u_1
s : List α
⊢ s.permutations.Nodup → s.Nodup

Tactic:
contrapose

Result:
α : Type u_1
s : List α
⊢ ¬s.Nodup → ¬s.permutations.Nodup
-- Mathlib/Logic/Godel/GodelBetaFunction.lean
lemma coprime_mul_succ {n m a} (h : n ≤ m) (ha : m - n ∣ a) : Coprime (n * a + 1) (m * a + 1) :=
  Nat.coprime_of_dvd fun p pp hn hm => by
    have : p ∣ (m - n) * a

Proof state:
n m a : ℕ
h : n ≤ m
ha : m - n ∣ a
p : ℕ
pp : Prime p
hn : p ∣ n * a + 1
hm : p ∣ m * a + 1
this : p ∣ (m - n) * a
⊢ p ∣ a

Tactic:
rcases (Nat.Prime.dvd_mul pp).mp this with (hp | hp)

Result:
case inl
n m a : ℕ
h : n ≤ m
ha : m - n ∣ a
p : ℕ
pp : Prime p
hn : p ∣ n * a + 1
hm : p ∣ m * a + 1
this : p ∣ (m - n) * a
hp : p ∣ m - n
⊢ p ∣ a

case inr
n m a : ℕ
h : n ≤ m
ha : m - n ∣ a
p : ℕ
pp : Prime p
hn : p ∣ n * a + 1
hm : p ∣ m * a + 1
this : p ∣ (m - n) * a
hp : p ∣ a
⊢ p ∣ a

Proof state:
n m a : ℕ
h : n ≤ m
ha : m - n ∣ a
p : ℕ
pp : Prime p
hn : p ∣ n * a + 1
hm : p ∣ m * a + 1
⊢ False

Tactic:
have : p ∣ (m - n) * a := by
  simpa [Nat.succ_sub_succ, ← Nat.mul_sub_right_distrib] using
    Nat.dvd_sub (Nat.succ_le_succ <| Nat.mul_le_mul_right a h) hm hn

Result:
n m a : ℕ
h : n ≤ m
ha : m - n ∣ a
p : ℕ
pp : Prime p
hn : p ∣ n * a + 1
hm : p ∣ m * a + 1
this : p ∣ (m - n) * a
⊢ False

Proof state:
case inl
n m a : ℕ
h : n ≤ m
ha : m - n ∣ a
p : ℕ
pp : Prime p
hn : p ∣ n * a + 1
hm : p ∣ m * a + 1
this : p ∣ (m - n) * a
hp : p ∣ m - n
⊢ p ∣ a

Tactic:
exact Nat.dvd_trans hp ha

Result:
no goals

Proof state:
n m a : ℕ
h : n ≤ m
ha : m - n ∣ a
p : ℕ
pp : Prime p
hn : p ∣ n * a + 1
hm : p ∣ m * a + 1
this✝ : p ∣ (m - n) * a
this : p ∣ a
⊢ False

Tactic:
apply pp.ne_one

Result:
n m a : ℕ
h : n ≤ m
ha : m - n ∣ a
p : ℕ
pp : Prime p
hn : p ∣ n * a + 1
hm : p ∣ m * a + 1
this✝ : p ∣ (m - n) * a
this : p ∣ a
⊢ p = 1

Proof state:
n m a : ℕ
h : n ≤ m
ha : m - n ∣ a
p : ℕ
pp : Prime p
hn : p ∣ n * a + 1
hm : p ∣ m * a + 1
⊢ p ∣ (m - n) * a

Tactic:
simpa [Nat.succ_sub_succ, ← Nat.mul_sub_right_distrib] using
  Nat.dvd_sub (Nat.succ_le_succ <| Nat.mul_le_mul_right a h) hm hn

Result:
no goals

Proof state:
n m a : ℕ
h : n ≤ m
ha : m - n ∣ a
p : ℕ
pp : Prime p
hn : p ∣ n * a + 1
hm : p ∣ m * a + 1
this✝ : p ∣ (m - n) * a
this : p ∣ a
⊢ p = 1

Tactic:
simpa [Nat.add_sub_cancel_left] using Nat.dvd_sub (le_add_right _ _) hn (this.mul_left n)

Result:
no goals

Proof state:
case inr
n m a : ℕ
h : n ≤ m
ha : m - n ∣ a
p : ℕ
pp : Prime p
hn : p ∣ n * a + 1
hm : p ∣ m * a + 1
this : p ∣ (m - n) * a
hp : p ∣ a
⊢ p ∣ a

Tactic:
exact hp

Result:
no goals
-- Mathlib/Computability/Primrec.lean
theorem unpair₂ {n f} (hf : @Primrec' n f) : @Primrec' n fun v => (f v).unpair.2

Proof state:
n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec' f
s : Primrec' fun v => (f v).sqrt
fss : Primrec' fun v => f v - (f v).sqrt * (f v).sqrt
v : List.Vector ℕ n
⊢ (if f v - (f v).sqrt * (f v).sqrt < (f v).sqrt then (f v).sqrt else f v - (f v).sqrt * (f v).sqrt - (f v).sqrt) =
    (unpair (f v)).2

Tactic:
simp [Nat.unpair]

Result:
n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec' f
s : Primrec' fun v => (f v).sqrt
fss : Primrec' fun v => f v - (f v).sqrt * (f v).sqrt
v : List.Vector ℕ n
⊢ (if f v - (f v).sqrt * (f v).sqrt < (f v).sqrt then (f v).sqrt else f v - (f v).sqrt * (f v).sqrt - (f v).sqrt) =
    (if f v - (f v).sqrt * (f v).sqrt < (f v).sqrt then (f v - (f v).sqrt * (f v).sqrt, (f v).sqrt)
      else ((f v).sqrt, f v - (f v).sqrt * (f v).sqrt - (f v).sqrt)).2

Proof state:
n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec' f
s : Primrec' fun v => (f v).sqrt
⊢ Primrec' fun v => (unpair (f v)).2

Tactic:
have fss := sub.comp₂ _ hf (mul.comp₂ _ s s)

Result:
n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec' f
s : Primrec' fun v => (f v).sqrt
fss : Primrec' fun v => f v - (f v).sqrt * (f v).sqrt
⊢ Primrec' fun v => (unpair (f v)).2

Proof state:
n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec' f
⊢ Primrec' fun v => (unpair (f v)).2

Tactic:
have s := sqrt.comp₁ _ hf

Result:
n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec' f
s : Primrec' fun v => (f v).sqrt
⊢ Primrec' fun v => (unpair (f v)).2

Proof state:
n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec' f
s : Primrec' fun v => (f v).sqrt
fss : Primrec' fun v => f v - (f v).sqrt * (f v).sqrt
v : List.Vector ℕ n
⊢ (if f v - (f v).sqrt * (f v).sqrt < (f v).sqrt then (f v).sqrt else f v - (f v).sqrt * (f v).sqrt - (f v).sqrt) =
    (if f v - (f v).sqrt * (f v).sqrt < (f v).sqrt then (f v - (f v).sqrt * (f v).sqrt, (f v).sqrt)
      else ((f v).sqrt, f v - (f v).sqrt * (f v).sqrt - (f v).sqrt)).2

Tactic:
split_ifs <;> rfl

Result:
no goals

Proof state:
n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec' f
s : Primrec' fun v => (f v).sqrt
fss : Primrec' fun v => f v - (f v).sqrt * (f v).sqrt
⊢ Primrec' fun v => (unpair (f v)).2

Tactic:
refine (if_lt fss s s (sub.comp₂ _ fss s)).of_eq fun v => ?_

Result:
n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec' f
s : Primrec' fun v => (f v).sqrt
fss : Primrec' fun v => f v - (f v).sqrt * (f v).sqrt
v : List.Vector ℕ n
⊢ (if f v - (f v).sqrt * (f v).sqrt < (f v).sqrt then (f v).sqrt else f v - (f v).sqrt * (f v).sqrt - (f v).sqrt) =
    (unpair (f v)).2
-- Mathlib/Topology/MetricSpace/Antilipschitz.lean
theorem mul_le_edist (hf : AntilipschitzWith K f) (x y : α) :
    (K : ℝ≥0∞)⁻¹ * edist x y ≤ edist (f x) (f y)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
x y : α
⊢ (↑K)⁻¹ * edist x y ≤ edist (f x) (f y)

Tactic:
rw [mul_comm, ← div_eq_mul_inv]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
x y : α
⊢ edist x y / ↑K ≤ edist (f x) (f y)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
x y : α
⊢ edist x y / ↑K ≤ edist (f x) (f y)

Tactic:
exact ENNReal.div_le_of_le_mul' (hf x y)

Result:
no goals
-- Mathlib/RingTheory/Ideal/GoingUp.lean
theorem exists_coeff_ne_zero_mem_comap_of_non_zero_divisor_root_mem {r : S}
    (r_non_zero_divisor : ∀ {x}, x * r = 0 → x = 0) (hr : r ∈ I) {p : R[X]} :
    p ≠ 0 → p.eval₂ f r = 0 → ∃ i, p.coeff i ≠ 0 ∧ p.coeff i ∈ I.comap f

Proof state:
case refine_2
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
I : Ideal S
r : S
r_non_zero_divisor : ∀ {x : S}, x * r = 0 → x = 0
hr : r ∈ I
p : R[X]
⊢ ∀ (p : R[X]) (a : R),
    p.coeff 0 = 0 →
      a ≠ 0 →
        (p ≠ 0 → eval₂ f r p = 0 → ∃ i, p.coeff i ≠ 0 ∧ p.coeff i ∈ comap f I) →
          p + C a ≠ 0 → eval₂ f r (p + C a) = 0 → ∃ i, (p + C a).coeff i ≠ 0 ∧ (p + C a).coeff i ∈ comap f I

Tactic:
intro p a coeff_eq_zero a_ne_zero _ _ hp

Result:
case refine_2
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
I : Ideal S
r : S
r_non_zero_divisor : ∀ {x : S}, x * r = 0 → x = 0
hr : r ∈ I
p✝ p : R[X]
a : R
coeff_eq_zero : p.coeff 0 = 0
a_ne_zero : a ≠ 0
a✝¹ : p ≠ 0 → eval₂ f r p = 0 → ∃ i, p.coeff i ≠ 0 ∧ p.coeff i ∈ comap f I
a✝ : p + C a ≠ 0
hp : eval₂ f r (p + C a) = 0
⊢ ∃ i, (p + C a).coeff i ≠ 0 ∧ (p + C a).coeff i ∈ comap f I

Proof state:
case refine_3.intro.intro.refine_1
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
I : Ideal S
r : S
r_non_zero_divisor : ∀ {x : S}, x * r = 0 → x = 0
hr : r ∈ I
p✝ p : R[X]
p_nonzero : p ≠ 0
ih : p ≠ 0 → eval₂ f r p = 0 → ∃ i, p.coeff i ≠ 0 ∧ p.coeff i ∈ comap f I
a✝ : p * X ≠ 0
hp : eval₂ f r p * r = 0
i : ℕ
hi : p.coeff i ≠ 0
mem : p.coeff i ∈ comap f I
⊢ (p * X).coeff (i + 1) ≠ 0

Tactic:
simp [hi, mem]

Result:
no goals

Proof state:
case refine_3
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
I : Ideal S
r : S
r_non_zero_divisor : ∀ {x : S}, x * r = 0 → x = 0
hr : r ∈ I
p✝ p : R[X]
p_nonzero : p ≠ 0
ih : p ≠ 0 → eval₂ f r p = 0 → ∃ i, p.coeff i ≠ 0 ∧ p.coeff i ∈ comap f I
a✝ : p * X ≠ 0
hp : eval₂ f r p * r = 0
⊢ ∃ i, (p * X).coeff i ≠ 0 ∧ (p * X).coeff i ∈ comap f I

Tactic:
obtain ⟨i, hi, mem⟩ := ih p_nonzero (r_non_zero_divisor hp)

Result:
case refine_3.intro.intro
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
I : Ideal S
r : S
r_non_zero_divisor : ∀ {x : S}, x * r = 0 → x = 0
hr : r ∈ I
p✝ p : R[X]
p_nonzero : p ≠ 0
ih : p ≠ 0 → eval₂ f r p = 0 → ∃ i, p.coeff i ≠ 0 ∧ p.coeff i ∈ comap f I
a✝ : p * X ≠ 0
hp : eval₂ f r p * r = 0
i : ℕ
hi : p.coeff i ≠ 0
mem : p.coeff i ∈ comap f I
⊢ ∃ i, (p * X).coeff i ≠ 0 ∧ (p * X).coeff i ∈ comap f I
-- Mathlib/CategoryTheory/Functor/KanExtension/Adjunction.lean
@[reassoc (attr := simp)]
lemma ι_colimitIsoColimitGrothendieck_hom (X : C) :
    colimit.ι G X ≫ (colimitIsoColimitGrothendieck L G).hom =
    colimit.ι (CostructuredArrow.grothendieckProj L ⋙ G) ⟨L.obj X, .mk (𝟙 _)⟩

Proof state:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_5, u_1} C
inst✝⁴ : Category.{u_6, u_2} D
L : C ⥤ D
H : Type u_3
inst✝³ : Category.{u_4, u_3} H
G : C ⥤ H
inst✝² : L.HasPointwiseLeftKanExtension G
inst✝¹ : HasColimitsOfShape D H
inst✝ : HasColimitsOfShape C H
X : C
⊢ colimit.ι G X =
    colimit.ι (CostructuredArrow.grothendieckProj L ⋙ G)
        { base := L.obj X, fiber := CostructuredArrow.mk (𝟙 (L.obj X)) } ≫
      (L.colimitIsoColimitGrothendieck G).inv

Tactic:
exact (ι_colimitIsoColimitGrothendieck_inv L G ⟨L.obj X, .mk (𝟙 _)⟩).symm

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_5, u_1} C
inst✝⁴ : Category.{u_6, u_2} D
L : C ⥤ D
H : Type u_3
inst✝³ : Category.{u_4, u_3} H
G : C ⥤ H
inst✝² : L.HasPointwiseLeftKanExtension G
inst✝¹ : HasColimitsOfShape D H
inst✝ : HasColimitsOfShape C H
X : C
⊢ colimit.ι G X ≫ (L.colimitIsoColimitGrothendieck G).hom =
    colimit.ι (CostructuredArrow.grothendieckProj L ⋙ G)
      { base := L.obj X, fiber := CostructuredArrow.mk (𝟙 (L.obj X)) }

Tactic:
rw [← Iso.eq_comp_inv]

Result:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_5, u_1} C
inst✝⁴ : Category.{u_6, u_2} D
L : C ⥤ D
H : Type u_3
inst✝³ : Category.{u_4, u_3} H
G : C ⥤ H
inst✝² : L.HasPointwiseLeftKanExtension G
inst✝¹ : HasColimitsOfShape D H
inst✝ : HasColimitsOfShape C H
X : C
⊢ colimit.ι G X =
    colimit.ι (CostructuredArrow.grothendieckProj L ⋙ G)
        { base := L.obj X, fiber := CostructuredArrow.mk (𝟙 (L.obj X)) } ≫
      (L.colimitIsoColimitGrothendieck G).inv
-- Mathlib/Combinatorics/SimpleGraph/Maps.lean
@[simp] lemma induce_singleton_eq_top (v : V) : G.induce {v} = ⊤

Proof state:
V : Type u_1
G : SimpleGraph V
v : V
⊢ induce {v} G = ⊤

Tactic:
rw [eq_top_iff]

Result:
V : Type u_1
G : SimpleGraph V
v : V
⊢ ⊤ ≤ induce {v} G

Proof state:
V : Type u_1
G : SimpleGraph V
v : V
⊢ ⊤ ≤ induce {v} G

Tactic:
apply le_comap_of_subsingleton

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
theorem iSup_iSup_eq_right {b : β} {f : ∀ x : β, b = x → α} : ⨆ x, ⨆ h : b = x, f x h = f b rfl :=
  (le_iSup₂ b rfl).antisymm'
    (iSup₂_le fun c => by
      rintro rfl
      rfl)

Proof state:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
b : β
f : (x : β) → b = x → α
c : β
⊢ ∀ (j : b = c), f c j ≤ f b ⋯

Tactic:
rintro rfl

Result:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
b : β
f : (x : β) → b = x → α
⊢ f b ⋯ ≤ f b ⋯

Proof state:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
b : β
f : (x : β) → b = x → α
⊢ f b ⋯ ≤ f b ⋯

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/MorphismProperty/Limits.lean
lemma colimitsOfShape_monotone {W₁ W₂ : MorphismProperty C} (h : W₁ ≤ W₂)
    (J : Type*) [Category J] :
    W₁.colimitsOfShape J ≤ W₂.colimitsOfShape J

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
W₁ W₂ : MorphismProperty C
h : W₁ ≤ W₂
J : Type u_2
inst✝ : Category.{u_3, u_2} J
⊢ W₁.colimitsOfShape J ≤ W₂.colimitsOfShape J

Tactic:
rintro _ _ _ ⟨_, _, _, _, _, h₂, f, hf⟩

Result:
case mk
C : Type u
inst✝¹ : Category.{v, u} C
W₁ W₂ : MorphismProperty C
h : W₁ ≤ W₂
J : Type u_2
inst✝ : Category.{u_3, u_2} J
X Y : C
X₁✝ X₂✝ : J ⥤ C
c₁✝ : Cocone X₁✝
c₂✝ : Cocone X₂✝
h₁✝ : IsColimit c₁✝
h₂ : IsColimit c₂✝
f : X₁✝ ⟶ X₂✝
hf : W₁.functorCategory J f
⊢ W₂.colimitsOfShape J (h₁✝.desc { pt := c₂✝.pt, ι := f ≫ c₂✝.ι })

Proof state:
case mk
C : Type u
inst✝¹ : Category.{v, u} C
W₁ W₂ : MorphismProperty C
h : W₁ ≤ W₂
J : Type u_2
inst✝ : Category.{u_3, u_2} J
X Y : C
X₁✝ X₂✝ : J ⥤ C
c₁✝ : Cocone X₁✝
c₂✝ : Cocone X₂✝
h₁✝ : IsColimit c₁✝
h₂ : IsColimit c₂✝
f : X₁✝ ⟶ X₂✝
hf : W₁.functorCategory J f
⊢ W₂.colimitsOfShape J (h₁✝.desc { pt := c₂✝.pt, ι := f ≫ c₂✝.ι })

Tactic:
exact ⟨_, _, _, _, _, h₂, f, fun j ↦ h _ (hf j)⟩

Result:
no goals
-- Mathlib/Topology/Algebra/Valued/LocallyCompact.lean
lemma isUnit_iff_norm_eq_one {u : 𝒪[K]} : IsUnit u ↔ ‖u‖ = 1

Proof state:
K : Type u_1
inst✝¹ : NontriviallyNormedField K
inst✝ : IsUltrametricDist K
u : ↥𝒪[K]
⊢ IsUnit u ↔ ‖u‖ = 1

Tactic:
simpa [← NNReal.coe_inj] using
  (Valuation.integer.integers (NormedField.valuation (K := K))).isUnit_iff_valuation_eq_one

Result:
no goals
-- Mathlib/Analysis/Seminorm.lean
theorem ball_comp (p : Seminorm 𝕜₂ E₂) (f : E →ₛₗ[σ₁₂] E₂) (x : E) (r : ℝ) :
    (p.comp f).ball x r = f ⁻¹' p.ball (f x) r

Proof state:
case h
𝕜 : Type u_3
𝕜₂ : Type u_4
E : Type u_7
E₂ : Type u_8
inst✝⁶ : SeminormedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedRing 𝕜₂
inst✝² : AddCommGroup E₂
inst✝¹ : Module 𝕜₂ E₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p : Seminorm 𝕜₂ E₂
f : E →ₛₗ[σ₁₂] E₂
x : E
r : ℝ
x✝ : E
⊢ x✝ ∈ (p.comp f).ball x r ↔ x✝ ∈ ⇑f ⁻¹' p.ball (f x) r

Tactic:
simp_rw [ball, mem_preimage, comp_apply, Set.mem_setOf_eq, map_sub]

Result:
no goals

Proof state:
𝕜 : Type u_3
𝕜₂ : Type u_4
E : Type u_7
E₂ : Type u_8
inst✝⁶ : SeminormedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedRing 𝕜₂
inst✝² : AddCommGroup E₂
inst✝¹ : Module 𝕜₂ E₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p : Seminorm 𝕜₂ E₂
f : E →ₛₗ[σ₁₂] E₂
x : E
r : ℝ
⊢ (p.comp f).ball x r = ⇑f ⁻¹' p.ball (f x) r

Tactic:
ext

Result:
case h
𝕜 : Type u_3
𝕜₂ : Type u_4
E : Type u_7
E₂ : Type u_8
inst✝⁶ : SeminormedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedRing 𝕜₂
inst✝² : AddCommGroup E₂
inst✝¹ : Module 𝕜₂ E₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p : Seminorm 𝕜₂ E₂
f : E →ₛₗ[σ₁₂] E₂
x : E
r : ℝ
x✝ : E
⊢ x✝ ∈ (p.comp f).ball x r ↔ x✝ ∈ ⇑f ⁻¹' p.ball (f x) r