harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/FieldTheory/Minpoly/IsIntegrallyClosed.lean
theorem ToAdjoin.injective (hx : IsIntegral R x) : Function.Injective (Minpoly.toAdjoin R x)

Proof state:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
x : S
hx : IsIntegral R x
⊢ Injective ⇑(Minpoly.toAdjoin R x)

Tactic:
refine (injective_iff_map_eq_zero _).2 fun P₁ hP₁ => ?_

Result:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
x : S
hx : IsIntegral R x
P₁ : AdjoinRoot (minpoly R x)
hP₁ : (Minpoly.toAdjoin R x) P₁ = 0
⊢ P₁ = 0

Proof state:
case intro
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
x : S
hx : IsIntegral R x
P : R[X]
hP₁ : (Minpoly.toAdjoin R x) ((AdjoinRoot.mk (minpoly R x)) P) = 0
⊢ (AdjoinRoot.mk (minpoly R x)) P = 0

Tactic:
rwa [Minpoly.toAdjoin_apply', liftHom_mk, ← Subalgebra.coe_eq_zero, aeval_subalgebra_coe,
  isIntegrallyClosed_dvd_iff hx, ← AdjoinRoot.mk_eq_zero] at hP₁

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
x : S
hx : IsIntegral R x
P₁ : AdjoinRoot (minpoly R x)
hP₁ : (Minpoly.toAdjoin R x) P₁ = 0
⊢ P₁ = 0

Tactic:
obtain ⟨P, rfl⟩ := mk_surjective P₁

Result:
case intro
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
x : S
hx : IsIntegral R x
P : R[X]
hP₁ : (Minpoly.toAdjoin R x) ((AdjoinRoot.mk (minpoly R x)) P) = 0
⊢ (AdjoinRoot.mk (minpoly R x)) P = 0
-- Mathlib/Algebra/Polynomial/Div.lean
theorem dvd_iff_isRoot : X - C a ∣ p ↔ IsRoot p a :=
  ⟨fun h => by
    rwa [← modByMonic_eq_zero_iff_dvd (monic_X_sub_C _), modByMonic_X_sub_C_eq_C_eval, ← C_0,
      C_inj] at h,
    fun h => ⟨p /ₘ (X - C a), by rw [mul_divByMonic_eq_iff_isRoot.2 h]⟩⟩

Proof state:
R : Type u
a : R
inst✝ : CommRing R
p : R[X]
h : X - C a ∣ p
⊢ p.IsRoot a

Tactic:
rwa [← modByMonic_eq_zero_iff_dvd (monic_X_sub_C _), modByMonic_X_sub_C_eq_C_eval, ← C_0,
  C_inj] at h

Result:
no goals

Proof state:
R : Type u
a : R
inst✝ : CommRing R
p : R[X]
h : p.IsRoot a
⊢ p = (X - C a) * (p /ₘ (X - C a))

Tactic:
rw [mul_divByMonic_eq_iff_isRoot.2 h]

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
lemma zero_pow_le_one [ZeroLEOneClass M₀] : ∀ n : ℕ, (0 : M₀) ^ n ≤ 1
  | 0 => (pow_zero _).le
  | n + 1 => by rw [zero_pow n.succ_ne_zero]; exact zero_le_one

Proof state:
M₀ : Type u_1
inst✝² : MonoidWithZero M₀
inst✝¹ : Preorder M₀
inst✝ : ZeroLEOneClass M₀
n : ℕ
⊢ 0 ≤ 1

Tactic:
exact zero_le_one

Result:
no goals

Proof state:
M₀ : Type u_1
inst✝² : MonoidWithZero M₀
inst✝¹ : Preorder M₀
inst✝ : ZeroLEOneClass M₀
n : ℕ
⊢ 0 ^ (n + 1) ≤ 1

Tactic:
rw [zero_pow n.succ_ne_zero]

Result:
M₀ : Type u_1
inst✝² : MonoidWithZero M₀
inst✝¹ : Preorder M₀
inst✝ : ZeroLEOneClass M₀
n : ℕ
⊢ 0 ≤ 1
-- Mathlib/RingTheory/Localization/FractionRing.lean
theorem mk'_eq_one_iff_eq {x : A} {y : nonZeroDivisors A} : mk' K x y = 1 ↔ x = y

Proof state:
A : Type u_4
inst✝³ : CommRing A
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : A
y : ↥(nonZeroDivisors A)
this : Nontrivial A
⊢ mk' K x y = 1 ↔ x = ↑y

Tactic:
refine ⟨?_, fun hxy => by rw [hxy, mk'_self']⟩

Result:
A : Type u_4
inst✝³ : CommRing A
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : A
y : ↥(nonZeroDivisors A)
this : Nontrivial A
⊢ mk' K x y = 1 → x = ↑y

Proof state:
A : Type u_4
inst✝³ : CommRing A
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : A
y : ↥(nonZeroDivisors A)
this : Nontrivial A
hxy : (algebraMap A K) x = (algebraMap A K) ↑y
hy : (algebraMap A K) ↑y ≠ 0
⊢ x = ↑y

Tactic:
exact IsFractionRing.injective A K hxy

Result:
no goals

Proof state:
A : Type u_4
inst✝³ : CommRing A
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : A
y : ↥(nonZeroDivisors A)
⊢ mk' K x y = 1 ↔ x = ↑y

Tactic:
haveI := (algebraMap A K).domain_nontrivial

Result:
A : Type u_4
inst✝³ : CommRing A
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : A
y : ↥(nonZeroDivisors A)
this : Nontrivial A
⊢ mk' K x y = 1 ↔ x = ↑y

Proof state:
A : Type u_4
inst✝³ : CommRing A
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : A
y : ↥(nonZeroDivisors A)
this : Nontrivial A
⊢ mk' K x y = 1 → x = ↑y

Tactic:
intro hxy

Result:
A : Type u_4
inst✝³ : CommRing A
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : A
y : ↥(nonZeroDivisors A)
this : Nontrivial A
hxy : mk' K x y = 1
⊢ x = ↑y

Proof state:
A : Type u_4
inst✝³ : CommRing A
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : A
y : ↥(nonZeroDivisors A)
this : Nontrivial A
hxy : mk' K x y = 1
hy : (algebraMap A K) ↑y ≠ 0
⊢ x = ↑y

Tactic:
rw [IsFractionRing.mk'_eq_div, div_eq_one_iff_eq hy] at hxy

Result:
A : Type u_4
inst✝³ : CommRing A
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : A
y : ↥(nonZeroDivisors A)
this : Nontrivial A
hxy : (algebraMap A K) x = (algebraMap A K) ↑y
hy : (algebraMap A K) ↑y ≠ 0
⊢ x = ↑y

Proof state:
A : Type u_4
inst✝³ : CommRing A
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : A
y : ↥(nonZeroDivisors A)
this : Nontrivial A
hxy : mk' K x y = 1
⊢ x = ↑y

Tactic:
have hy : (algebraMap A K) ↑y ≠ (0 : K) :=
  IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors y.property

Result:
A : Type u_4
inst✝³ : CommRing A
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : A
y : ↥(nonZeroDivisors A)
this : Nontrivial A
hxy : mk' K x y = 1
hy : (algebraMap A K) ↑y ≠ 0
⊢ x = ↑y

Proof state:
A : Type u_4
inst✝³ : CommRing A
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : A
y : ↥(nonZeroDivisors A)
this : Nontrivial A
hxy : x = ↑y
⊢ mk' K x y = 1

Tactic:
rw [hxy, mk'_self']

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Typeclasses.lean
theorem Measure.isFiniteMeasure_map {m : MeasurableSpace α} (μ : Measure α) [IsFiniteMeasure μ]
    (f : α → β) : IsFiniteMeasure (μ.map f)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace β
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → β
⊢ IsFiniteMeasure (map f μ)

Tactic:
by_cases hf : AEMeasurable f μ

Result:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace β
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → β
hf : AEMeasurable f μ
⊢ IsFiniteMeasure (map f μ)

case neg
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace β
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → β
hf : ¬AEMeasurable f μ
⊢ IsFiniteMeasure (map f μ)

Proof state:
case pos.measure_univ_lt_top
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace β
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → β
hf : AEMeasurable f μ
⊢ μ (f ⁻¹' univ) < ⊤

Tactic:
exact measure_lt_top μ _

Result:
no goals

Proof state:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace β
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → β
hf : AEMeasurable f μ
⊢ IsFiniteMeasure (map f μ)

Tactic:
constructor

Result:
case pos.measure_univ_lt_top
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace β
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → β
hf : AEMeasurable f μ
⊢ (map f μ) univ < ⊤

Proof state:
case pos.measure_univ_lt_top
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace β
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → β
hf : AEMeasurable f μ
⊢ (map f μ) univ < ⊤

Tactic:
rw [map_apply_of_aemeasurable hf MeasurableSet.univ]

Result:
case pos.measure_univ_lt_top
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace β
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → β
hf : AEMeasurable f μ
⊢ μ (f ⁻¹' univ) < ⊤

Proof state:
case neg
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace β
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → β
hf : ¬AEMeasurable f μ
⊢ IsFiniteMeasure 0

Tactic:
exact MeasureTheory.isFiniteMeasureZero

Result:
no goals

Proof state:
case neg
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace β
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → β
hf : ¬AEMeasurable f μ
⊢ IsFiniteMeasure (map f μ)

Tactic:
rw [map_of_not_aemeasurable hf]

Result:
case neg
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace β
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → β
hf : ¬AEMeasurable f μ
⊢ IsFiniteMeasure 0
-- Mathlib/Order/SupIndep.lean
theorem SupIndep.le_sup_iff (hs : s.SupIndep f) (hts : t ⊆ s) (hi : i ∈ s) (hf : ∀ i, f i ≠ ⊥) :
    f i ≤ t.sup f ↔ i ∈ t

Proof state:
α : Type u_1
ι : Type u_3
inst✝¹ : Lattice α
inst✝ : OrderBot α
s t : Finset ι
f : ι → α
i : ι
hs : s.SupIndep f
hts : t ⊆ s
hi : i ∈ s
hf : ∀ (i : ι), f i ≠ ⊥
h : f i ≤ t.sup f
⊢ i ∈ t

Tactic:
by_contra hit

Result:
α : Type u_1
ι : Type u_3
inst✝¹ : Lattice α
inst✝ : OrderBot α
s t : Finset ι
f : ι → α
i : ι
hs : s.SupIndep f
hts : t ⊆ s
hi : i ∈ s
hf : ∀ (i : ι), f i ≠ ⊥
h : f i ≤ t.sup f
hit : i ∉ t
⊢ False

Proof state:
α : Type u_1
ι : Type u_3
inst✝¹ : Lattice α
inst✝ : OrderBot α
s t : Finset ι
f : ι → α
i : ι
hs : s.SupIndep f
hts : t ⊆ s
hi : i ∈ s
hf : ∀ (i : ι), f i ≠ ⊥
h : f i ≤ t.sup f
hit : i ∉ t
⊢ False

Tactic:
exact hf i (disjoint_self.1 <| (hs hts hi hit).mono_right h)

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_3
inst✝¹ : Lattice α
inst✝ : OrderBot α
s t : Finset ι
f : ι → α
i : ι
hs : s.SupIndep f
hts : t ⊆ s
hi : i ∈ s
hf : ∀ (i : ι), f i ≠ ⊥
⊢ f i ≤ t.sup f ↔ i ∈ t

Tactic:
refine ⟨fun h => ?_, le_sup⟩

Result:
α : Type u_1
ι : Type u_3
inst✝¹ : Lattice α
inst✝ : OrderBot α
s t : Finset ι
f : ι → α
i : ι
hs : s.SupIndep f
hts : t ⊆ s
hi : i ∈ s
hf : ∀ (i : ι), f i ≠ ⊥
h : f i ≤ t.sup f
⊢ i ∈ t
-- Mathlib/Analysis/Calculus/FDeriv/Analytic.lean
theorem AnalyticAt.deriv [CompleteSpace F] (h : AnalyticAt 𝕜 f x) :
    AnalyticAt 𝕜 (deriv f) x

Proof state:
case intro.intro
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
inst✝ : CompleteSpace F
h✝ : AnalyticAt 𝕜 f x
r : ℝ
hr : 0 < r
h : AnalyticOnNhd 𝕜 f (Metric.ball x r)
⊢ AnalyticAt 𝕜 (deriv f) x

Tactic:
exact h.deriv x (by simp [hr])

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
inst✝ : CompleteSpace F
h : AnalyticAt 𝕜 f x
⊢ AnalyticAt 𝕜 (deriv f) x

Tactic:
obtain ⟨r, hr, h⟩ := h.exists_ball_analyticOnNhd

Result:
case intro.intro
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
inst✝ : CompleteSpace F
h✝ : AnalyticAt 𝕜 f x
r : ℝ
hr : 0 < r
h : AnalyticOnNhd 𝕜 f (Metric.ball x r)
⊢ AnalyticAt 𝕜 (deriv f) x

Proof state:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
inst✝ : CompleteSpace F
h✝ : AnalyticAt 𝕜 f x
r : ℝ
hr : 0 < r
h : AnalyticOnNhd 𝕜 f (Metric.ball x r)
⊢ x ∈ Metric.ball x r

Tactic:
simp [hr]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/AC.lean
theorem Context.eval_toList (ctx : Context α) (e : Expr) : evalList α ctx e.toList = eval α ctx e

Proof state:
case var
α : Sort u_1
ctx : Context α
x : Nat
⊢ evalList α ctx (Expr.var x).toList = eval α ctx (Expr.var x)

Tactic:
rfl

Result:
no goals

Proof state:
case op
α : Sort u_1
ctx : Context α
l r : Expr
ih₁ : evalList α ctx l.toList = eval α ctx l
ih₂ : evalList α ctx r.toList = eval α ctx r
⊢ evalList α ctx (l.op r).toList = eval α ctx (l.op r)

Tactic:
simp [evalList, Expr.toList, eval, ←ih₁, ←ih₂]

Result:
case op
α : Sort u_1
ctx : Context α
l r : Expr
ih₁ : evalList α ctx l.toList = eval α ctx l
ih₂ : evalList α ctx r.toList = eval α ctx r
⊢ evalList α ctx (l.toList ++ r.toList) = EvalInformation.evalOp ctx (evalList α ctx l.toList) (evalList α ctx r.toList)

Proof state:
α : Sort u_1
ctx : Context α
e : Expr
⊢ evalList α ctx e.toList = eval α ctx e

Tactic:
induction e with
| var x => rfl
| op l r ih₁ ih₂ =>
  simp [evalList, Expr.toList, eval, ←ih₁, ←ih₂]
  apply evalList_append <;> apply toList_nonEmpty

Result:
no goals

Proof state:
case op
α : Sort u_1
ctx : Context α
l r : Expr
ih₁ : evalList α ctx l.toList = eval α ctx l
ih₂ : evalList α ctx r.toList = eval α ctx r
⊢ evalList α ctx (l.toList ++ r.toList) = EvalInformation.evalOp ctx (evalList α ctx l.toList) (evalList α ctx r.toList)

Tactic:
apply evalList_append <;> apply toList_nonEmpty

Result:
no goals
-- Mathlib/Data/Multiset/AddSub.lean
theorem sub_singleton (a : α) (s : Multiset α) : s - {a} = s.erase a

Proof state:
case a
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
a✝ : α
⊢ (count a✝ s - if a✝ = a then 1 else 0) = count a✝ (s.erase a)

Tactic:
split <;> simp_all

Result:
no goals

Proof state:
case a
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
a✝ : α
⊢ count a✝ (s - {a}) = count a✝ (s.erase a)

Tactic:
simp only [count_sub, count_singleton]

Result:
case a
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
a✝ : α
⊢ (count a✝ s - if a✝ = a then 1 else 0) = count a✝ (s.erase a)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ s - {a} = s.erase a

Tactic:
ext

Result:
case a
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
a✝ : α
⊢ count a✝ (s - {a}) = count a✝ (s.erase a)
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem C_mul_monomial : C a * monomial n b = monomial n (a * b)

Proof state:
R : Type u
a b : R
n : ℕ
inst✝ : Semiring R
⊢ C a * (monomial n) b = (monomial n) (a * b)

Tactic:
simp only [← monomial_zero_left, monomial_mul_monomial, zero_add]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Connectivity/WalkDecomp.lean
theorem dropUntil_copy {u v w v' w'} (p : G.Walk v w) (hv : v = v') (hw : w = w')
    (h : u ∈ (p.copy hv hw).support) :
    (p.copy hv hw).dropUntil u h = (p.dropUntil u (by subst_vars; exact h)).copy rfl hw

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v' w' : V
p : G.Walk v' w'
h : u ∈ (p.copy ⋯ ⋯).support
⊢ (p.copy ⋯ ⋯).dropUntil u h = (p.dropUntil u ⋯).copy ⋯ ⋯

Tactic:
rfl

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
v✝ w✝ u✝ : V
inst✝ : DecidableEq V
u v w v' w' : V
p : G.Walk v w
hv : v = v'
hw : w = w'
h : u ∈ (p.copy hv hw).support
⊢ u ∈ p.support

Tactic:
subst_vars

Result:
V : Type u
G : SimpleGraph V
v w u✝ : V
inst✝ : DecidableEq V
u v' w' : V
p : G.Walk v' w'
h : u ∈ (p.copy ⋯ ⋯).support
⊢ u ∈ p.support

Proof state:
V : Type u
G : SimpleGraph V
v w u✝ : V
inst✝ : DecidableEq V
u v' w' : V
p : G.Walk v' w'
h : u ∈ (p.copy ⋯ ⋯).support
⊢ u ∈ p.support

Tactic:
exact h

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w v' w' : V
p : G.Walk v w
hv : v = v'
hw : w = w'
h : u ∈ (p.copy hv hw).support
⊢ (p.copy hv hw).dropUntil u h = (p.dropUntil u ⋯).copy ⋯ hw

Tactic:
subst_vars

Result:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v' w' : V
p : G.Walk v' w'
h : u ∈ (p.copy ⋯ ⋯).support
⊢ (p.copy ⋯ ⋯).dropUntil u h = (p.dropUntil u ⋯).copy ⋯ ⋯
-- Mathlib/Geometry/Manifold/LocalInvariantProperties.lean
theorem right_invariance {s : Set H} {x : H} {f : H → H'} {e : PartialHomeomorph H H} (he : e ∈ G)
    (hxe : x ∈ e.source) : P (f ∘ e.symm) (e.symm ⁻¹' s) (e x) ↔ P f s x

Proof state:
case refine_1
H : Type u_1
H' : Type u_3
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s : Set H
x : H
f : H → H'
e : PartialHomeomorph H H
he : e ∈ G
hxe : x ∈ e.source
h : P (f ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x)
this : P ((f ∘ ↑e.symm) ∘ ↑e) (↑e ⁻¹' (↑e.symm ⁻¹' s)) x
x' : H
hx' : x' ∈ e.source
⊢ ((f ∘ ↑e.symm) ∘ ↑e) x' = f x'

Tactic:
simp_rw [Function.comp_apply, e.left_inv hx']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Range.lean
theorem mem_zipIdx {x : α} {i : Nat} {xs : Array α} {k : Nat} (h : (x, i) ∈ xs.zipIdx k) :
    k ≤ i ∧ i < k + xs.size ∧
      x = xs[i - k]'(by have := le_snd_of_mem_zipIdx h; have := snd_lt_add_of_mem_zipIdx h; omega) :=
  ⟨le_snd_of_mem_zipIdx h, snd_lt_add_of_mem_zipIdx h, fst_eq_of_mem_zipIdx h⟩

Proof state:
α : Type ?u.29004
x : α
i : Nat
xs : Array α
k : Nat
h : (x, i) ∈ xs.zipIdx k
this : k ≤ (x, i).snd
⊢ i - k < xs.size

Tactic:
have := snd_lt_add_of_mem_zipIdx h

Result:
α : Type ?u.29004
x : α
i : Nat
xs : Array α
k : Nat
h : (x, i) ∈ xs.zipIdx k
this✝ : k ≤ (x, i).snd
this : (x, i).snd < k + xs.size
⊢ i - k < xs.size

Proof state:
α : Type ?u.29004
x : α
i : Nat
xs : Array α
k : Nat
h : (x, i) ∈ xs.zipIdx k
this✝ : k ≤ (x, i).snd
this : (x, i).snd < k + xs.size
⊢ i - k < xs.size

Tactic:
omega

Result:
no goals

Proof state:
α : Type ?u.29004
x : α
i : Nat
xs : Array α
k : Nat
h : (x, i) ∈ xs.zipIdx k
⊢ i - k < xs.size

Tactic:
have := le_snd_of_mem_zipIdx h

Result:
α : Type ?u.29004
x : α
i : Nat
xs : Array α
k : Nat
h : (x, i) ∈ xs.zipIdx k
this : k ≤ (x, i).snd
⊢ i - k < xs.size
-- Mathlib/Algebra/Group/Fin/Basic.lean
lemma coe_sub_one (a : Fin (n + 1)) : ↑(a - 1) = if a = 0 then n else a - 1

Proof state:
case neg.hc
n✝ : ℕ
a : Fin (n✝ + 1 + 1)
h : ¬a = 0
⊢ n✝ + 1 + 1 ≤ n✝ + 1 + ↑a

Tactic:
rw [Nat.add_le_add_iff_left, Nat.one_le_iff_ne_zero]

Result:
case neg.hc
n✝ : ℕ
a : Fin (n✝ + 1 + 1)
h : ¬a = 0
⊢ ↑a ≠ 0

Proof state:
n : ℕ
a : Fin (n + 1)
⊢ ↑(a - 1) = if a = 0 then n else ↑a - 1

Tactic:
cases n

Result:
case zero
a : Fin (0 + 1)
⊢ ↑(a - 1) = if a = 0 then 0 else ↑a - 1

case succ
n✝ : ℕ
a : Fin (n✝ + 1 + 1)
⊢ ↑(a - 1) = if a = 0 then n✝ + 1 else ↑a - 1

Proof state:
case neg.hc
n✝ : ℕ
a : Fin (n✝ + 1 + 1)
h : ¬a = 0
⊢ n✝ + 1 + 1 ≤ ↑a + (n✝ + 1)

Tactic:
conv_rhs => rw [Nat.add_comm]

Result:
case neg.hc
n✝ : ℕ
a : Fin (n✝ + 1 + 1)
h : ¬a = 0
⊢ n✝ + 1 + 1 ≤ n✝ + 1 + ↑a

Proof state:
case zero
a : Fin (0 + 1)
⊢ ↑(a - 1) = if a = 0 then 0 else ↑a - 1

Tactic:
simp

Result:
no goals

Proof state:
case succ
n✝ : ℕ
a : Fin (n✝ + 1 + 1)
⊢ ↑(a - 1) = if a = 0 then n✝ + 1 else ↑a - 1

Tactic:
split_ifs with h

Result:
case pos
n✝ : ℕ
a : Fin (n✝ + 1 + 1)
h : a = 0
⊢ ↑(a - 1) = n✝ + 1

case neg
n✝ : ℕ
a : Fin (n✝ + 1 + 1)
h : ¬a = 0
⊢ ↑(a - 1) = ↑a - 1

Proof state:
case neg.hc
n✝ : ℕ
a : Fin (n✝ + 1 + 1)
h : ¬a = 0
⊢ ↑a ≠ 0

Tactic:
rwa [Fin.ext_iff] at h

Result:
no goals

Proof state:
case pos
n✝ : ℕ
a : Fin (n✝ + 1 + 1)
h : a = 0
⊢ ↑(a - 1) = n✝ + 1

Tactic:
simp [h]

Result:
no goals

Proof state:
case neg
n✝ : ℕ
a : Fin (n✝ + 1 + 1)
h : ¬a = 0
⊢ ↑(a - 1) = ↑a - 1

Tactic:
rw [sub_eq_add_neg, val_add_eq_ite, coe_neg_one, if_pos, Nat.add_comm, Nat.add_sub_add_left]

Result:
case neg.hc
n✝ : ℕ
a : Fin (n✝ + 1 + 1)
h : ¬a = 0
⊢ n✝ + 1 + 1 ≤ ↑a + (n✝ + 1)
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean
@[simp]
protected lemma comp_zero {n₁ n₂ n₁₂ : ℤ} (z₁ : Cochain F G n₁)
    (h : n₁ + n₂ = n₁₂) : z₁.comp (0 : Cochain G K n₂) h = 0

Proof state:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K : CochainComplex C ℤ
n₁ n₂ n₁₂ : ℤ
z₁ : Cochain F G n₁
h : n₁ + n₂ = n₁₂
p q : ℤ
hpq : p + n₁₂ = q
⊢ (z₁.comp 0 h).v p q hpq = v 0 p q hpq

Tactic:
simp only [comp_v _ _ h p _ q rfl (by omega), zero_v, comp_zero]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K : CochainComplex C ℤ
n₁ n₂ n₁₂ : ℤ
z₁ : Cochain F G n₁
h : n₁ + n₂ = n₁₂
p q : ℤ
hpq : p + n₁₂ = q
⊢ p + n₁ + n₂ = q

Tactic:
omega

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K : CochainComplex C ℤ
n₁ n₂ n₁₂ : ℤ
z₁ : Cochain F G n₁
h : n₁ + n₂ = n₁₂
⊢ z₁.comp 0 h = 0

Tactic:
ext p q hpq

Result:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K : CochainComplex C ℤ
n₁ n₂ n₁₂ : ℤ
z₁ : Cochain F G n₁
h : n₁ + n₂ = n₁₂
p q : ℤ
hpq : p + n₁₂ = q
⊢ (z₁.comp 0 h).v p q hpq = v 0 p q hpq
-- Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean
lemma extend_finset_to_connected (Gpc : G.Preconnected) {t : Finset V} (tn : t.Nonempty) :
    ∃ (t' : Finset V), t ⊆ t' ∧ (G.induce (t' : Set V)).Connected

Proof state:
case intro.refine_2.patches.intro.intro
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
u : V
ut : u ∈ t
v w : V
wt : w ∈ t
hw : v ∈ (Nonempty.some ⋯).support
⊢ ∃ s' ⊆ ↑(t.biUnion fun v => (Nonempty.some ⋯).support.toFinset),
    ∃ (hu' : u ∈ s') (hv' : v ∈ s'), (induce s' G).Reachable ⟨u, hu'⟩ ⟨v, hv'⟩

Tactic:
refine ⟨{x | x ∈ (Gpc u w).some.support}, ?_, ?_⟩

Result:
case intro.refine_2.patches.intro.intro.refine_1
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
u : V
ut : u ∈ t
v w : V
wt : w ∈ t
hw : v ∈ (Nonempty.some ⋯).support
⊢ {x | x ∈ (Nonempty.some ⋯).support} ⊆ ↑(t.biUnion fun v => (Nonempty.some ⋯).support.toFinset)

case intro.refine_2.patches.intro.intro.refine_2
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
u : V
ut : u ∈ t
v w : V
wt : w ∈ t
hw : v ∈ (Nonempty.some ⋯).support
⊢ ∃ (hu' : u ∈ {x | x ∈ (Nonempty.some ⋯).support}) (hv' : v ∈ {x | x ∈ (Nonempty.some ⋯).support}),
    (induce {x | x ∈ (Nonempty.some ⋯).support} G).Reachable ⟨u, hu'⟩ ⟨v, hv'⟩